From c23c2716a59cb6871ebd56c1f67a0fd22f70f54f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 11 Apr 2018 12:27:33 +0200 Subject: [PATCH] Move lemma to equivalence-module --- src/Cat/Categories/Sets.agda | 57 ++--------------------------------- src/Cat/Category.agda | 5 ++- src/Cat/Category/Product.agda | 46 +++++++++------------------- src/Cat/Equivalence.agda | 54 +++++++++++++++++++++++++++++++++ 4 files changed, 75 insertions(+), 87 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index b2ae61f..a0982fd 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -106,59 +106,6 @@ module _ (ℓ : Level) where iso : (p ≡ q) ≈ (fst p ≡ fst q) iso = f , g , inv - lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)} - → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q - lem3 {Q = Q} eA = res - where - f : Σ A P → Σ A Q - f (a , pA) = a , fst (eA a) pA - g : Σ A Q → Σ A P - g (a , qA) = a , g' qA - where - k : TypeIsomorphism _ - k = toIso _ _ (snd (eA a)) - open Σ k renaming (fst to g') - ve-re : (x : Σ A P) → (g ∘ f) x ≡ x - ve-re x i = fst x , eq i - where - eq : snd ((g ∘ f) x) ≡ snd x - eq = begin - snd ((g ∘ f) x) ≡⟨⟩ - snd (g (f (a , pA))) ≡⟨⟩ - g' (fst (eA a) pA) ≡⟨ lem ⟩ - pA ∎ - where - open Σ x renaming (fst to a ; snd to pA) - k : TypeIsomorphism _ - k = toIso _ _ (snd (eA a)) - open Σ k renaming (fst to g' ; snd to inv) - module A = AreInverses inv - -- anti-funExt - lem : (g' ∘ (fst (eA a))) pA ≡ pA - lem i = A.verso-recto i pA - re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x - re-ve x i = fst x , eq i - where - open Σ x renaming (fst to a ; snd to qA) - eq = begin - snd ((f ∘ g) x) ≡⟨⟩ - fst (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩ - qA ∎ - where - k : TypeIsomorphism _ - k = toIso _ _ (snd (eA a)) - open Σ k renaming (fst to g' ; snd to inv) - module A = AreInverses inv - inv : AreInverses f g - inv = record - { verso-recto = funExt ve-re - ; recto-verso = funExt re-ve - } - iso : Σ A P ≈ Σ A Q - iso = f , g , inv - res : Σ A P ≃ Σ A Q - res = fromIsomorphism _ _ iso - module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where lem4 : isSet A → isSet B → (f : A → B) → isEquiv A B f ≃ isIso f @@ -186,7 +133,7 @@ module _ (ℓ : Level) where -- lem3 and the equivalence from lem4 step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) - step0 = lem3 {ℓc = lzero} (λ f → sym≃ (lem4 sA sB f)) + step0 = equivSig (λ f → sym≃ (lem4 sA sB f)) -- univalence step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) @@ -219,7 +166,7 @@ module _ (ℓ : Level) where open Σ hA renaming (fst to A) eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB) - eq1 = ua (lem3 (\ hB → univ≃)) + eq1 = ua (equivSig (\ hB → univ≃)) univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB) univalent[Contr] = subst {P = isContr} (sym eq1) tres diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 428d357..8f39dac 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -147,8 +147,11 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where from[Andrea] = from[Contr] ∘ step where module _ (f : Univalent[Andrea]) (A : Object) where + lem : Σ Object (A ≅_) ≃ Σ Object (A ≡_) + lem = equivSig {ℓa} {ℓb} {Object} {A ≅_} {_} {A ≡_} (f A) + aux : isContr (Σ[ B ∈ Object ] A ≡ B) - aux = {!!} + aux = {!Σ Object (A ≡_)!} step : isContr (Σ Object (A ≅_)) step = {!subst {P = isContr} {!!} aux!} diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 6ec32ba..663503f 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -172,32 +172,15 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} open IsPreCategory isPreCat univalent : Univalent - univalent {(X , xa , xb)} {(Y , ya , yb)} = univalenceFromIsomorphism res - where - open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≈_) - -- open import Relation.Binary.PreorderReasoning (Cat.Equivalence.preorder≅ {!!}) using () - -- renaming - -- ( _∼⟨_⟩_ to _≈⟨_⟩_ - -- ; begin_ to begin!_ - -- ; _∎ to _∎! ) - -- lawl - -- : ((X , xa , xb) ≡ (Y , ya , yb)) - -- ≈ (Σ[ iso ∈ (X ℂ.≅ Y) ] let p = ℂ.isoToId iso in (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)) - -- lawl = {!begin! ? ≈⟨ ? ⟩ ? ∎!!} - -- Problem with the above approach: Preorders only work for heterogeneous equaluties. + univalent {(X , xa , xb)} {(Y , ya , yb)} = {!!} - -- (X , xa , xb) ≡ (Y , ya , yb) - -- ≅ - -- Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb) - -- ≅ - -- Σ (X ℂ.≅ Y) (λ iso - -- → let p = ℂ.isoToId iso - -- in - -- ( PathP (λ i → ℂ.Arrow (p i) A) xa ya) - -- × PathP (λ i → ℂ.Arrow (p i) B) xb yb - -- ) - -- ≅ - -- (X , xa , xb) ≅ (Y , ya , yb) + -- module _ {(X , xa , xb) : Object} {(Y , ya , yb) : Object} where + module _ (𝕏 𝕐 : Object) where + open Σ 𝕏 renaming (fst to X ; snd to x) + open Σ x renaming (fst to xa ; snd to xb) + open Σ 𝕐 renaming (fst to Y ; snd to y) + open Σ y renaming (fst to ya ; snd to yb) + open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≈_) step0 : ((X , xa , xb) ≡ (Y , ya , yb)) ≈ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)) @@ -287,7 +270,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} let iso : X ℂ.≅ Y iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~ - helper : PathP (λ i → ℂ.Arrow (ℂ.isoToId ? i) A) xa ya + helper : PathP (λ i → ℂ.Arrow (ℂ.isoToId {!!} i) A) xa ya helper = {!!} in iso , helper , {!!}}) , record @@ -315,12 +298,13 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} : ((X , xa , xb) ≡ (Y , ya , yb)) ≃ ((X , xa , xb) ≅ (Y , ya , yb)) equiv1 = _ , fromIso _ _ (snd iso) + equiv4reel + : ((X , xa , xb) ≅ (Y , ya , yb)) + ≃ ((X , xa , xb) ≡ (Y , ya , yb)) + equiv4reel = {!!} - res : TypeIsomorphism (idToIso (X , xa , xb) (Y , ya , yb)) - res = {!snd equiv1!} - - univalent2 : ∀ X Y → (X ≅ Y) ≃ (X ≡ Y) - univalent2 = {!!} + univalent' : Univalent + univalent' = from[Andrea] equiv4reel isCat : IsCategory raw IsCategory.isPreCategory isCat = isPreCat diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index 4ca5a93..dbdc2aa 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -445,3 +445,57 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where ; recto-verso = funExt ve-re } in fromIsomorphism _ _ iso + +module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where + equivSig : {ℓc : Level} {Q : A → Set ℓc} + → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q + equivSig {Q = Q} eA = res + where + f : Σ A P → Σ A Q + f (a , pA) = a , fst (eA a) pA + g : Σ A Q → Σ A P + g (a , qA) = a , g' qA + where + k : Isomorphism _ + k = toIso _ _ (snd (eA a)) + open Σ k renaming (fst to g') + ve-re : (x : Σ A P) → (g ∘ f) x ≡ x + ve-re x i = fst x , eq i + where + eq : snd ((g ∘ f) x) ≡ snd x + eq = begin + snd ((g ∘ f) x) ≡⟨⟩ + snd (g (f (a , pA))) ≡⟨⟩ + g' (fst (eA a) pA) ≡⟨ lem ⟩ + pA ∎ + where + open Σ x renaming (fst to a ; snd to pA) + k : Isomorphism _ + k = toIso _ _ (snd (eA a)) + open Σ k renaming (fst to g' ; snd to inv) + module A = AreInverses inv + -- anti-funExt + lem : (g' ∘ (fst (eA a))) pA ≡ pA + lem i = A.verso-recto i pA + re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x + re-ve x i = fst x , eq i + where + open Σ x renaming (fst to a ; snd to qA) + eq = begin + snd ((f ∘ g) x) ≡⟨⟩ + fst (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩ + qA ∎ + where + k : Isomorphism _ + k = toIso _ _ (snd (eA a)) + open Σ k renaming (fst to g' ; snd to inv) + module A = AreInverses inv + inv : AreInverses f g + inv = record + { verso-recto = funExt ve-re + ; recto-verso = funExt re-ve + } + iso : Σ A P ≅ Σ A Q + iso = f , g , inv + res : Σ A P ≃ Σ A Q + res = fromIsomorphism _ _ iso