{-# OPTIONS --without-K --rewriting #-}
module Interval where
open import Equality.Propositional as Eq hiding (elim)
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Equivalence equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J using (ext⁻¹)
postulate
I : Set
[0] [1] : I
0≡1 : [0] ≡ [1]
module _ {p}
(P : I → Set p)
(p₀ : P [0])
(p₁ : P [1])
(p₀≡p₁ : subst P 0≡1 p₀ ≡ p₁)
where
postulate
elim : (x : I) → P x
elim-[0] : elim [0] ≡ p₀
elim-[1] : elim [1] ≡ p₁
{-# REWRITE elim-[0] #-}
{-# REWRITE elim-[1] #-}
postulate
elim-0≡1 : dependent-cong elim 0≡1 ≡ p₀≡p₁
rec : ∀ {p} {P : Set p}
(p₀ p₁ : P)
(p₀≡p₁ : p₀ ≡ p₁) →
I → P
rec p₀ p₁ p₀≡p₁ =
elim _ p₀ p₁ (
subst (const _) 0≡1 p₀ ≡⟨ subst-const 0≡1 ⟩
p₀ ≡⟨ p₀≡p₁ ⟩∎
p₁ ∎)
rec-0≡1 :
∀ {p} {P : Set p}
(p₀ p₁ : P)
(p₀≡p₁ : p₀ ≡ p₁) →
cong (rec p₀ p₁ p₀≡p₁) 0≡1 ≡ p₀≡p₁
rec-0≡1 p₀ p₁ p₀≡p₁ =
cong (rec p₀ p₁ p₀≡p₁) 0≡1 ≡⟨⟩
cong (elim _ p₀ p₁ (trans (subst-const 0≡1) p₀≡p₁)) 0≡1 ≡⟨ sym $ trans-sym-[trans] _ _ ⟩
trans (sym $ subst-const 0≡1)
(trans (subst-const 0≡1)
(cong (elim _ p₀ p₁ (trans (subst-const 0≡1) p₀≡p₁)) 0≡1)) ≡⟨ cong (trans _) $ sym $ dependent-cong-subst-const-cong _ 0≡1 ⟩
trans (sym $ subst-const 0≡1)
(dependent-cong (elim _ p₀ p₁ (trans (subst-const 0≡1) p₀≡p₁)) 0≡1) ≡⟨ cong (trans _) $ elim-0≡1 _ _ _ _ ⟩
trans (sym $ subst-const 0≡1) (trans (subst-const 0≡1) p₀≡p₁) ≡⟨ trans-sym-[trans] _ _ ⟩∎
p₀≡p₁ ∎
interval-contractible : Contractible I
interval-contractible = [1] , sym ∘ f
where
f : (x : I) → x ≡ [1]
f = elim (_≡ [1]) 0≡1 refl
(subst (_≡ [1]) 0≡1 0≡1 ≡⟨ cong (λ p → subst (_≡ [1]) p 0≡1)
(sym $ sym-sym 0≡1) ⟩
subst (_≡ [1]) (sym (sym 0≡1)) 0≡1 ≡⟨ subst-trans (sym 0≡1) ⟩
trans (sym 0≡1) 0≡1 ≡⟨ trans-symˡ 0≡1 ⟩∎
refl ∎)
rec-const :
∀ {p} {P : Set p} (p : P) (p≡p : p ≡ p) i →
rec p p p≡p i ≡ p
rec-const p p≡p i =
rec p p p≡p i ≡⟨ cong (rec p p p≡p) (_⇔_.to propositional⇔irrelevant (mono₁ 0 interval-contractible) i [0]) ⟩∎
rec p p p≡p [0] ∎
abstract
private
ext-helper :
∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
(∀ x → f x ≡ g x) → I → (x : A) → B x
ext-helper {f = f} {g} f≡g i =
λ x → rec (f x) (g x) (f≡g x) i
ext′ : ∀ {a b} → Extensionality a b
ext′ {f = f} {g = g} f≡g =
f ≡⟨⟩
ext-helper f≡g [0] ≡⟨ cong (ext-helper f≡g) 0≡1 ⟩∎
ext-helper f≡g [1] ∎
ext : ∀ {a b} → Extensionality a b
ext = good-ext ext′
ext-is-equivalence :
∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
Is-equivalence {A = ∀ x → f x ≡ g x} ext
ext-is-equivalence = good-ext-is-equivalence ext′
ext-refl :
∀ {a b} {A : Set a} {B : A → Set b} (f : (x : A) → B x) →
ext (λ x → refl {x = f x}) ≡ refl {x = f}
ext-refl = good-ext-refl ext′
cong-ext :
∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x}
(f≡g : ∀ x → f x ≡ g x) {x} →
cong (_$ x) (ext f≡g) ≡ f≡g x
cong-ext = cong-good-ext ext′
subst-ext :
∀ {a b p} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} {x}
(P : B x → Set p) {p} (f≡g : ∀ x → f x ≡ g x) →
subst (λ f → P (f x)) (ext f≡g) p ≡ subst P (f≡g x) p
subst-ext = subst-good-ext ext′
elim-ext :
∀ {a b p} {A : Set a} {B : A → Set b} {x : A}
(P : B x → B x → Set p)
(p : (y : B x) → P y y)
{f g : (x : A) → B x}
(f≡g : ∀ x → f x ≡ g x) →
Eq.elim (λ {f g} _ → P (f x) (g x)) (p ∘ (_$ x)) (ext f≡g) ≡
Eq.elim (λ {x y} _ → P x y) p (f≡g x)
elim-ext = elim-good-ext ext′
ext-sym :
∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x}
(f≡g : ∀ x → f x ≡ g x) →
ext (sym ∘ f≡g) ≡ sym (ext f≡g)
ext-sym = good-ext-sym ext′
ext-trans :
∀ {a b} {A : Set a} {B : A → Set b} {f g h : (x : A) → B x}
(f≡g : ∀ x → f x ≡ g x) (g≡h : ∀ x → g x ≡ h x) →
ext (λ x → trans (f≡g x) (g≡h x)) ≡ trans (ext f≡g) (ext g≡h)
ext-trans = good-ext-trans ext′
cong-post-∘-ext :
∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
{f g : A → B} {h : B → C}
(f≡g : ∀ x → f x ≡ g x) →
cong (h ∘_) (ext f≡g) ≡ ext (cong h ∘ f≡g)
cong-post-∘-ext = cong-post-∘-good-ext ext′ ext′
cong-pre-∘-ext :
∀ {a b c} {A : Set a} {B : Set b} {C : B → Set c}
{f g : (x : B) → C x} {h : A → B}
(f≡g : ∀ x → f x ≡ g x) →
cong (_∘ h) (ext f≡g) ≡ ext (f≡g ∘ h)
cong-pre-∘-ext = cong-pre-∘-good-ext ext′ ext′