From 32d1833d517a9c1aceee97bfcafedbfa5c01fbfc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 11:26:48 +0100 Subject: [PATCH] [WIP] A long way towards proving univalence in the category of hSets --- src/Cat/Categories/Sets.agda | 86 ++++++++++++++++++++++++++++-------- src/Cat/Equivalence.agda | 44 +++++++++++++++++- 2 files changed, 110 insertions(+), 20 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 8aaa025..cc3d655 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -15,7 +15,7 @@ open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product open import Cat.Wishlist -open import Cat.Equivalence as Eqv renaming (module NoEta to Eeq) using (AreInverses) +open import Cat.Equivalence as Eqv renaming (module NoEta to Eeq) using (AreInverses ; module Equiv≃) module Equivalence = Eeq.Equivalence′ @@ -27,12 +27,33 @@ sym≃ = Equivalence.symmetry infixl 10 _⊙_ -inv-coe : {ℓ : Level} {A B : Set ℓ} {a : A} - → (p : A ≡ B) → coe (sym p) (coe p a) ≡ a -inv-coe = {!!} -inv-coe' : {ℓ : Level} {A B : Set ℓ} {a : A} - → (p : B ≡ A) → coe p (coe (sym p) a) ≡ a -inv-coe' = {!!} +module _ {ℓ : Level} {A : Set ℓ} {a : A} where + id-coe : coe refl a ≡ a + id-coe = begin + coe refl a ≡⟨ {!!} ⟩ + a ∎ + +module _ {ℓ : Level} {A B : Set ℓ} {a : A} where + inv-coe : (p : A ≡ B) → coe (sym p) (coe p a) ≡ a + inv-coe p = + let + D : (y : Set ℓ) → _ ≡ y → Set _ + D _ q = coe (sym q) (coe q a) ≡ a + d : D A refl + d = begin + coe (sym refl) (coe refl a) ≡⟨⟩ + coe refl (coe refl a) ≡⟨ id-coe ⟩ + coe refl a ≡⟨ id-coe ⟩ + a ∎ + in pathJ D d B p + inv-coe' : (p : B ≡ A) → coe p (coe (sym p) a) ≡ a + inv-coe' p = + let + D : (y : Set ℓ) → _ ≡ y → Set _ + D _ q = coe (sym q) (coe q a) ≡ a + k : coe p (coe (sym p) a) ≡ a + k = pathJ D (trans id-coe id-coe) B (sym p) + in k module _ (ℓ : Level) where private @@ -125,8 +146,8 @@ module _ (ℓ : Level) where iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q) iso = f , g , inv - lem3 : {Q : A → Set ℓb} → ((a : A) → P a ≃ Q a) - → Σ A P ≃ Σ A Q + lem3 : {Q : A → Set ℓb} + → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q lem3 {Q} eA = res where P→Q : ∀ {a} → P a ≡ Q a @@ -165,9 +186,25 @@ module _ (ℓ : Level) where res = Eeq.fromIsomorphism iso module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where - postulate - lem4 : isSet A → isSet B → (f : A → B) - → isEquiv A B f ≃ isIso f + lem4 : isSet A → isSet B → (f : A → B) + → isEquiv A B f ≃ isIso f + lem4 sA sB f = + let + obv : isEquiv A B f → isIso f + obv = Equiv≃.toIso A B + inv : isIso f → isEquiv A B f + inv = Equiv≃.fromIso A B + re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x + re-ve = Equiv≃.inverse-from-to-iso A B + ve-re : (x : isIso f) → (obv ∘ inv) x ≡ x + ve-re = Equiv≃.inverse-to-from-iso A B + iso : isEquiv A B f Eqv.≅ isIso f + iso = obv , inv , + record + { verso-recto = funExt re-ve + ; recto-verso = funExt ve-re + } + in Eeq.fromIsomorphism iso module _ {hA hB : Object} where private @@ -176,13 +213,24 @@ module _ (ℓ : Level) where B = proj₁ hB sB = proj₂ hB - postulate - -- lem3 and the equivalence from lem4 - step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) - -- univalence - step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) - -- lem2 with propIsSet - step2 : (A ≡ B) ≃ (hA ≡ hB) + + -- lem3 and the equivalence from lem4 + step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) + step0 = lem3 (λ f → sym≃ (lem4 sA sB f)) + -- univalence + step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) + step1 = + let + h : (A ≃ B) ≃ (A ≡ B) + h = sym≃ (univalence {A = A} {B}) + k : Σ _ (isEquiv (A ≃ B) (A ≡ B)) + k = Eqv.doEta h + in {!!} + + -- lem2 with propIsSet + step2 : (A ≡ B) ≃ (hA ≡ hB) + step2 = sym≃ (lem2 (λ A → isSetIsProp) hA hB) + -- Go from an isomorphism on sets to an isomorphism on homotopic sets trivial? : (hA ≅ hB) ≃ Σ (A → B) isIso trivial? = sym≃ (Eeq.fromIsomorphism res) diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index 795a25a..c047330 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -58,6 +58,23 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where _~_ : Set ℓa → Set ℓb → Set _ A ~ B = Σ _ iseqv + inverse-from-to-iso : ∀ {f} (x : _) → (fromIso {f} ∘ toIso {f}) x ≡ x + inverse-from-to-iso x = begin + (fromIso ∘ toIso) x ≡⟨⟩ + fromIso (toIso x) ≡⟨ propIsEquiv _ (fromIso (toIso x)) x ⟩ + x ∎ + + -- `toIso` is abstract - so I probably can't close this proof. + -- inverse-to-from-iso : ∀ {f} → toIso {f} ∘ fromIso {f} ≡ idFun _ + -- inverse-to-from-iso = funExt (λ x → begin + -- (toIso ∘ fromIso) x ≡⟨⟩ + -- toIso (fromIso x) ≡⟨ cong toIso (propIsEquiv _ (fromIso x) y) ⟩ + -- toIso y ≡⟨ {!!} ⟩ + -- x ∎) + -- where + -- y : iseqv _ + -- y = {!!} + fromIsomorphism : A ≅ B → A ~ B fromIsomorphism (f , iso) = f , fromIso iso @@ -130,7 +147,26 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where where import Cubical.NType.Properties as P - module Equiv≃ = Equiv ≃isEquiv + module Equiv≃ where + open Equiv ≃isEquiv public + inverse-to-from-iso : ∀ {f} (x : _) → (toIso {f} ∘ fromIso {f}) x ≡ x + inverse-to-from-iso {f} x = begin + (toIso ∘ fromIso) x ≡⟨⟩ + toIso (fromIso x) ≡⟨ cong toIso (propIsEquiv _ (fromIso x) y) ⟩ + toIso y ≡⟨ py ⟩ + x ∎ + where + helper : (x : Isomorphism _) → Σ _ λ y → toIso y ≡ x + helper (f~ , inv) = y , py + where + module inv = AreInverses inv + y : isEquiv _ _ f + y = {!!} + py : toIso y ≡ (f~ , inv) + py = {!!} + y : isEquiv _ _ _ + y = fst (helper x) + py = snd (helper x) module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open Cubical.PathPrelude using (_≃_) @@ -210,6 +246,12 @@ module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where symmetry : B ≃ A symmetry = deEta (Equivalence.symmetry (doEta e)) + -- fromIso : {f : A → B} → Isomorphism f → isEquiv f + -- fromIso = ? + + -- toIso : {f : A → B} → isEquiv f → Isomorphism f + -- toIso = ? + fromIsomorphism : A ≅ B → A ≃ B fromIsomorphism (f , iso) = _≃_.con f (Equiv≃.fromIso _ _ iso)