diff options
Diffstat (limited to 'Univalence-to-funext.agda')
| -rw-r--r-- | Univalence-to-funext.agda | 239 |
1 files changed, 239 insertions, 0 deletions
diff --git a/Univalence-to-funext.agda b/Univalence-to-funext.agda new file mode 100644 index 0000000..c2935b2 --- /dev/null +++ b/Univalence-to-funext.agda @@ -0,0 +1,239 @@ +{-# OPTIONS --without-K --rewriting #-} + +module Univalence-to-funext where + +open import lib.Base +open import lib.Equivalence +open import lib.Function +open import lib.PathGroupoid +open import lib.PathFunctor +open import lib.NType + +--============================================================================-- +-- Generic paths in Σ types + +module _ {i j} {A : Type i} {B : A → Type j} where + Σ-path-pair : (v w : Σ A B) → Type (lmax i j) + Σ-path-pair v w = Σ (fst v == fst w) + (λ p → transport B p (snd v) == snd w) + + pair→Σ= : {v w : Σ A B} → Σ-path-pair v w → v == w + pair→Σ= (idp , idp) = idp + + Σ=→pair : {v w : Σ A B} → v == w → Σ-path-pair v w + Σ=→pair idp = (idp , idp) + + Σ=→pair→Σ= : {v w : Σ A B} (p : v == w) → pair→Σ= (Σ=→pair p) == p + Σ=→pair→Σ= idp = idp + + pair→Σ=→pair : {v w : Σ A B} (z : Σ-path-pair v w) → + Σ=→pair (pair→Σ= z) == z + pair→Σ=→pair (idp , idp) = idp + + Σ=≃pair : {v w : Σ A B} → (v == w) ≃ (Σ-path-pair v w) + Σ=≃pair = equiv Σ=→pair pair→Σ= pair→Σ=→pair Σ=→pair→Σ= + + +--============================================================================-- +-- Univalence + +idtoeqv : ∀ {i} {A B : Type i} → (A == B) → (A ≃ B) +idtoeqv {A = A} idp = ide A + +postulate + ua : ∀ {i} {A B : Type i} → (A ≃ B) → (A == B) + idtoeqv-ua-β : ∀ {i} {A B : Type i} (e : A ≃ B) → idtoeqv (ua e) == e + +eqv-post∘ : ∀ {i} {A B : Type i} {C : Type i} (p : A == B) → + fst (idtoeqv (ap (λ T → (C → T)) p)) == _∘_ (fst (idtoeqv p)) +eqv-post∘ idp = idp + +--============================================================================-- +-- Happly and lemmas + +module _ {i j} {A : Type i} {B : A → Type j} {f g : Π A B} where + idh : f ∼ f + idh a = idp + + happly : f == g → f ∼ g + happly p a = ap (λ k → k a) p + + tr-happly-lemma : (p : f == g) → + transport (λ k → f ∼ k) p (idh) == happly p + tr-happly-lemma idp = idp + + fib-happly-lemma : (h : f ∼ g) → ((f , idh) == (g , h)) ≃ hfiber happly h + fib-happly-lemma h = (equiv from to α β) ∘e Σ=≃pair + where + to : hfiber happly h → Σ-path-pair (f , idh) (g , h) + to (p , q) = (p , tr-happly-lemma p ∙ q) + + from : Σ-path-pair (f , idh) (g , h) → hfiber happly h + from (p , q) = (p , ! (tr-happly-lemma p) ∙ q) + + β : (b : Σ-path-pair (f , idh) (g , h)) → to (from b) == b + β (p , q) = pair→Σ= (idp , ! (∙-assoc (tr-happly-lemma p) + (! (tr-happly-lemma p)) q) ∙ + !-inv-r (tr-happly-lemma p) ∙2 idp) + + α : (a : hfiber happly h) → from (to a) == a + α (p , q) = pair→Σ= (idp , + ! (∙-assoc (! (tr-happly-lemma p)) + (tr-happly-lemma p) q) ∙ + !-inv-l (tr-happly-lemma p) ∙2 idp) + +--============================================================================-- +-- Equivalences and contractibility + +contr-retract : ∀ {i} {A B : Type i} + (r : A → B) (s : B → A) → + (r ∘ s ∼ (idf B)) → + is-contr A → is-contr B +contr-retract r s h p = has-level-in + ((r (fst c)) , λ y → ap r (snd c (s y)) ∙ h y) + where c = has-level-apply p + +module _ {i j} {A : Type i} {B : Type j} where + is-contr-map : (f : A → B) → Type (lmax i j) + is-contr-map f = (y : B) → is-contr (hfiber f y) + + tr-ap-lemma : (f : A → B) {a' a : A} {b : B} + (p : a' == a) (q : f a' == b) → + transport (λ x → f x == b) p q == ! (ap f p) ∙ q + tr-ap-lemma f idp idp = idp + + nat-lemma : {k l : B → B} {a b : B} (p : a == b )(h : k ∼ l) → + ap k p ∙ h b == h a ∙ ap l p + nat-lemma {a = a} idp h = ! (∙-unit-r (h a)) + + contr-map-is-equiv : {f : A → B} → (is-contr-map f → is-equiv f) + contr-map-is-equiv {f = f} c = snd (equiv f g α β) + where + g : B → A + g b = fst (fst (has-level-apply (c b))) + + α : f ∘ g ∼ (idf B) + α b = snd (fst (has-level-apply (c b))) + + β : g ∘ f ∼ (idf A) + β a = fst (Σ=→pair (snd (has-level-apply (c (f a))) (a , idp))) + + + + equiv-is-contr-map : {f : A → B} → (is-equiv f → is-contr-map f) + equiv-is-contr-map {f = f} e b = + has-level-in (hf , λ y → pair→Σ= (fc y , sc y)) + where + g : B → A + g = is-equiv.g e + + α : g ∘ f ∼ (idf A) + α = is-equiv.g-f e + + β : f ∘ g ∼ (idf B) + β = is-equiv.f-g e + + hf : hfiber f b + hf = ((g b) , (β b)) + + fc : (y : hfiber f b) → (g b) == fst y + fc (a , p) = ap (g) (! p) ∙ α a + + sc : (y : hfiber f b) → + transport (λ x → f x == b) (fc (fst y , snd y)) (β b) == snd y + sc (a , p) = + transport (λ x → f x == b) (fc (a , p)) (β b) + =⟨ tr-ap-lemma f (fc (a , p)) (β b) ⟩ + ! (ap f (fc (a , p))) ∙ (β b) + =⟨ ap ! (ap-∙ f (ap g (! p)) (α a)) ∙2 idp ⟩ + ! (ap f (ap g (! p)) ∙ ap f (α a)) ∙ (β b) + =⟨ ap ! (idp ∙2 is-equiv.adj e a) ∙2 idp {a = β b}⟩ + ! (ap f (ap g (! p)) ∙ (β (f a))) ∙ (β b) + =⟨ ap ! (∘-ap f g (! p) ∙2 idp) ∙2 idp ⟩ + ! (ap (f ∘ g) (! p) ∙ (β (f a))) ∙ (β b) + =⟨ !-∙ (ap (f ∘ g) (! p)) (β (f a)) ∙2 idp ⟩ + (! (β (f a)) ∙ ! (ap (λ x → f (g x)) (! p))) ∙ (β b) + =⟨ (idp ∙2 !-ap (f ∘ g) (! p)) ∙2 idp {a = β b}⟩ + (! (β (f a)) ∙ (ap (f ∘ g) (! (! p)))) ∙ (β b) + =⟨ (idp ∙2 ap (ap (f ∘ g)) (!-! p)) ∙2 idp {a = β b} ⟩ + (! (β (f a)) ∙ (ap (f ∘ g) p)) ∙ (β b) + =⟨ ∙-assoc (! (β (f a))) (ap (f ∘ g) p) (β b) ⟩ + ! (β (f a)) ∙ (ap (f ∘ g) p ∙ (β b)) + =⟨ idp {a = ! (β (f a))} ∙2 (nat-lemma p β ∙ (idp ∙2 ap-idf p)) ⟩ + ! (β (f a)) ∙ (β (f a) ∙ p) + =⟨ ! (∙-assoc (! (β (f a))) (β (f a)) p) ⟩ + (! (β (f a)) ∙ β (f a)) ∙ p + =⟨ !-inv-l (β (f a)) ∙2 idp ⟩ + p + =∎ + + + +--============================================================================-- +-- Univalence implies funext + +module _ {i} {A : Type i} {B : A → Type i} {f : Π A B} where + image : A → Type i + image a = Σ (B a) (λ b → f a == b) + + graphType : Type i + graphType = Σ A image + + prA : graphType → A + prA = fst + + prA-is-equiv : graphType ≃ A + prA-is-equiv = equiv prA (λ x → (x , f x , idp)) (λ b → idp) β + where + tr-post-concat : ∀ {i} {X : Type i} {x y z : X} {p : x == y} + (q : z == x) → transport (_==_ z) p q == q ∙ p + tr-post-concat {p = idp} idp = idp + + β : (a : graphType) → (fst a , f (fst a), idp) == a + β (a , b , p) = pair→Σ= (idp , (pair→Σ= (p , (tr-post-concat idp)))) + + fibreOverId : Type i + fibreOverId = hfiber (_∘_ prA) (idf A) + + fibreOverId-is-contr : is-contr fibreOverId + fibreOverId-is-contr = prA∘-is-equiv (idf A) + where + p : graphType == A + p = ua prA-is-equiv + + pβ : fst (idtoeqv p) == prA + pβ = ap fst (idtoeqv-ua-β prA-is-equiv) + + prA∘-is-equiv : is-contr-map (λ g → prA ∘ g) + prA∘-is-equiv = transport is-contr-map + (eqv-post∘ p ∙ ap (λ x → _∘_ x) pβ) + (equiv-is-contr-map + (snd (idtoeqv (ap (λ T → (A → T)) p)))) + + homotopyType : Type i + homotopyType = Σ (Π A B) (λ g → f ∼ g) + + -- We crucially make use of the η-rule for functions here + s : homotopyType → fibreOverId + s (g , h) = ((λ a → (a , g a , h a)) , idp) + + r : fibreOverId → homotopyType + r (func , p) = fst ∘ img , snd ∘ img + where + img : (a : A) → image a + img a = transport image (happly p a) (snd (func a)) + + -- and here + var-funext : is-prop homotopyType + var-funext = contr-is-prop (contr-retract r s (λ _ → idp) + fibreOverId-is-contr) + +module _ {i} {A : Type i} {B : A → Type i} {f g : Π A B} where + pre-funext : (h : f ∼ g) → is-contr ((f , idh {g = g}) == (g , h)) + pre-funext h = has-level-apply var-funext (f , idh {g = g}) (g , h) + + funext : is-equiv (happly {f = f}{g = g}) + funext = contr-map-is-equiv + λ h → equiv-preserves-level + (fib-happly-lemma h) + ⦃ pre-funext h ⦄ |