From aa52bc8f077a39abc117d9b1627417f6ed0c9de5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 23 Apr 2018 17:04:27 +0200 Subject: [PATCH] Move lemmas about equivalences to that module --- src/Cat/Categories/Sets.agda | 85 +++-------------------------------- src/Cat/Category.agda | 27 ++++------- src/Cat/Category/Product.agda | 3 -- src/Cat/Equivalence.agda | 67 ++++++++++++++++++++++++++- src/Cat/Prelude.agda | 4 +- 5 files changed, 82 insertions(+), 104 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index ccf3e05..af52c8b 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -42,91 +42,16 @@ module _ (ℓ : Level) where IsPreCategory.isIdentity isPreCat {A} {B} = isIdentity {A} {B} IsPreCategory.arrowsAreSets isPreCat {A} {B} = arrowsAreSets {A} {B} - open IsPreCategory isPreCat hiding (_<<<_) - - isIso = TypeIsomorphism - module _ {hA hB : hSet ℓ} where - open Σ hA renaming (fst to A ; snd to sA) - open Σ hB renaming (fst to B ; snd to sB) - lem1 : (f : A → B) → isSet A → isSet B → isProp (isIso f) - lem1 f sA sB = res - where - module _ (x y : isIso f) where - module x = Σ x renaming (fst to inverse ; snd to areInverses) - module y = Σ y renaming (fst to inverse ; snd to areInverses) - -- I had a lot of difficulty using the corresponding proof where - -- AreInverses is defined. This is sadly a bit anti-modular. The - -- reason for my troubles is probably related to the type of objects - -- being hSet's rather than sets. - p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g) - p {f} g xx yy i = ve-re , re-ve - where - ve-re : g ∘ f ≡ idFun _ - ve-re = arrowsAreSets {A = hA} {B = hA} _ _ (fst xx) (fst yy) i - re-ve : f ∘ g ≡ idFun _ - re-ve = arrowsAreSets {A = hB} {B = hB} _ _ (snd xx) (snd yy) i - 1eq : x.inverse ≡ y.inverse - 1eq = begin - x.inverse ≡⟨⟩ - x.inverse ∘ idFun _ ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym (snd y.areInverses)) ⟩ - x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩ - (x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) (fst x.areInverses) ⟩ - idFun _ ∘ y.inverse ≡⟨⟩ - y.inverse ∎ - 2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ] - 2eq = lemPropF p 1eq - res : x ≡ y - res i = 1eq i , 2eq i - module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where - lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P) - → (p ≡ q) ≃ (fst p ≡ fst q) - lem2 pA p q = fromIsomorphism _ _ iso - where - f : ∀ {p q} → p ≡ q → fst p ≡ fst q - f e i = fst (e i) - g : ∀ {p q} → fst p ≡ fst q → p ≡ q - g {p} {q} = lemSig pA p q - ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e - ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e) - (\ i j → p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .snd) (λ i → p .snd) i j ) q - re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e - re-ve e = refl - inv : AreInverses (f {p} {q}) (g {p} {q}) - inv = funExt ve-re , funExt re-ve - iso : (p ≡ q) ≅ (fst p ≡ fst q) - iso = f , g , inv - - 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 - lem4 sA sB f = - let - obv : isEquiv A B f → isIso f - obv = toIso A B - inv : isIso f → isEquiv A B f - inv = fromIso A B - re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x - re-ve = inverse-from-to-iso A B - ve-re : (x : isIso f) → (obv ∘ inv) x ≡ x - ve-re = inverse-to-from-iso A B sA sB - iso : isEquiv A B f ≅ isIso f - iso = obv , inv , funExt re-ve , funExt ve-re - in fromIsomorphism _ _ iso - + open IsPreCategory isPreCat module _ {hA hB : Object} where open Σ hA renaming (fst to A ; snd to sA) open Σ hB renaming (fst to B ; snd to sB) - -- lem3 and the equivalence from lem4 - step0 : Σ (A → B) (isEquiv A B) ≃ Σ (A → B) isIso - step0 = equivSig (lem4 sA sB) - - -- lem2 with propIsSet - step2 : (hA ≡ hB) ≃ (A ≡ B) - step2 = lem2 (λ A → isSetIsProp) hA hB - univ≃ : (hA ≡ hB) ≃ (hA ≊ hB) - univ≃ = step2 ⊙ univalence ⊙ step0 + univ≃ + = equivSigProp (λ A → isSetIsProp) + ⊙ univalence + ⊙ equivSig {P = isEquiv A B} {Q = TypeIsomorphism} (equiv≃iso sA sB) univalent : Univalent univalent = univalenceFrom≃ univ≃ diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 26a3b02..9394089 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -119,7 +119,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where -- -- [HoTT §9.1.4] idToIso : (A B : Object) → A ≡ B → A ≊ B - idToIso A B eq = transp (\ i → A ≊ eq i) (idIso A) + idToIso A B eq = subst eq (idIso A) Univalent : Set (ℓa ⊔ ℓb) Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≊ B) (idToIso A B) @@ -348,7 +348,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where coe refl f ≡⟨ id-coe ⟩ f ≡⟨ sym rightIdentity ⟩ f <<< identity ≡⟨ cong (f <<<_) (sym subst-neutral) ⟩ - f <<< _ ∎) a' p + f <<< _ ≡⟨ {!!} ⟩ _ ∎) a' p module _ {b' : Object} (p : b ≡ b') where private @@ -431,28 +431,17 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where coe-dom : {f : Arrow A X} → coe p-dom f ≡ f <<< ι~ coe-dom {f} = begin - coe p-dom f - ≡⟨ 9-1-9 p refl f ⟩ - fst (idToIso _ _ refl) <<< f <<< fst (snd (idToIso _ _ p)) - ≡⟨ cong (λ φ → φ <<< f <<< fst (snd (idToIso _ _ p))) subst-neutral ⟩ - identity <<< f <<< fst (snd (idToIso _ _ p)) - ≡⟨ cong (λ φ → identity <<< f <<< φ) (cong (λ x → (fst (snd x))) lem) ⟩ - identity <<< f <<< ι~ - ≡⟨ cong (_<<< ι~) leftIdentity ⟩ + coe p-dom f ≡⟨ 9-1-9-left f p ⟩ + f <<< fst (snd (idToIso _ _ (isoToId iso))) ≡⟨⟩ + f <<< fst (snd (idToIso _ _ p)) ≡⟨ cong (f <<<_) (cong (fst ∘ snd) lem) ⟩ f <<< ι~ ∎ coe-cod : {f : Arrow X A} → coe p-cod f ≡ ι <<< f coe-cod {f} = begin coe p-cod f - ≡⟨ 9-1-9 refl p f ⟩ - fst (idToIso _ _ p) <<< f <<< fst (snd (idToIso _ _ refl)) - ≡⟨ cong (λ φ → fst (idToIso _ _ p) <<< f <<< φ) subst-neutral ⟩ - fst (idToIso _ _ p) <<< f <<< identity - ≡⟨ cong (λ φ → φ <<< f <<< identity) (cong fst lem) ⟩ - ι <<< f <<< identity - ≡⟨ sym isAssociative ⟩ - ι <<< (f <<< identity) - ≡⟨ cong (ι <<<_) rightIdentity ⟩ + ≡⟨ 9-1-9-right f p ⟩ + fst (idToIso _ _ p) <<< f + ≡⟨ cong (λ φ → φ <<< f) (cong fst lem) ⟩ ι <<< f ∎ module _ {f : Arrow A X} {g : Arrow B X} (q : PathP (λ i → p-dom i) f g) where diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index be77ec8..757c5cc 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -7,7 +7,6 @@ open import Cat.Equivalence open import Cat.Category module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where - open Category ℂ module _ (A B : Object) where @@ -18,8 +17,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where fst : ℂ [ object , A ] snd : ℂ [ object , B ] - -- FIXME Not sure this is actually a proposition - so this name is - -- misleading. record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where open RawProduct raw public field diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index a6a8582..6c96f1b 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -7,7 +7,10 @@ open import Cubical.PathPrelude hiding (inverse) open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public open import Cubical.GradLemma hiding (isoToPath) -open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; propSig ; id-coe) +open import Cat.Prelude using + ( lemPropF ; setPi ; lemSig ; propSet + ; Preorder ; equalityIsEquivalence ; propSig ; id-coe + ; Setoid ) import Cubical.Univalence as U @@ -327,6 +330,48 @@ preorder≅ ℓ = record k = pathJ D (trans id-coe id-coe) B (sym p) in k +setoid≅ : (ℓ : Level) → Setoid _ _ +setoid≅ ℓ = record + { Carrier = Set ℓ + ; _≈_ = _≅_ + ; isEquivalence = record + { refl = idFun _ , idFun _ , (funExt λ _ → refl) , (funExt λ _ → refl) + ; sym = symmetryIso + ; trans = composeIso + } + } + +setoid≃ : (ℓ : Level) → Setoid _ _ +setoid≃ ℓ = record + { Carrier = Set ℓ + ; _≈_ = _≃_ + ; isEquivalence = record + { refl = idEquiv + ; sym = Equivalence.symmetry + ; trans = λ x x₁ → Equivalence.compose x x₁ + } + } + +-- If the second component of a pair is propositional, then equality of such +-- pairs is equivalent to equality of their first components. +module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where + equivSigProp : ((x : A) → isProp (P x)) → {p q : Σ A P} + → (p ≡ q) ≃ (fst p ≡ fst q) + equivSigProp pA {p} {q} = fromIsomorphism _ _ iso + where + f : ∀ {p q} → p ≡ q → fst p ≡ fst q + f = cong fst + g : ∀ {p q} → fst p ≡ fst q → p ≡ q + g = lemSig pA _ _ + ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e + ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e) + (\ i j → p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .snd) (λ i → p .snd) i j ) q + re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e + re-ve e = refl + inv : AreInverses (f {p} {q}) (g {p} {q}) + inv = funExt ve-re , funExt re-ve + iso : (p ≡ q) ≅ (fst p ≡ fst q) + iso = f , g , inv module _ {ℓ : Level} {A B : Set ℓ} where isoToPath : (A ≅ B) → (A ≡ B) @@ -347,6 +392,24 @@ module _ {ℓ : Level} {A B : Set ℓ} where aux : (A U.≃ B) ≃ (A ≃ B) aux = fromIsomorphism _ _ (doEta , deEta , funExt (λ{ (U.con _ _) → refl}) , refl) + -- Equivalence is equivalent to isomorphism when the equivalence (resp. + -- isomorphism) acts on sets. + module _ (sA : isSet A) (sB : isSet B) where + equiv≃iso : (f : A → B) → isEquiv A B f ≃ Isomorphism f + equiv≃iso f = + let + obv : isEquiv A B f → Isomorphism f + obv = toIso A B + inv : Isomorphism f → isEquiv A B f + inv = fromIso A B + re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x + re-ve = inverse-from-to-iso A B + ve-re : (x : Isomorphism f) → (obv ∘ inv) x ≡ x + ve-re = inverse-to-from-iso A B sA sB + iso : isEquiv A B f ≅ Isomorphism f + iso = obv , inv , funExt re-ve , funExt ve-re + in fromIsomorphism _ _ iso + -- A few results that I have not generalized to work with both the eta and no-eta variable of ≃ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where -- Equality on sigma's whose second component is a proposition is equivalent @@ -438,6 +501,8 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where in fromIsomorphism _ _ iso module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where + -- Equivalence of pairs whose first components are identitical can be obtained + -- from an equivalence of their seecond components. equivSig : {ℓc : Level} {Q : A → Set ℓc} → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q equivSig {Q = Q} eA = res diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index bedad50..0c0bec0 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -76,7 +76,9 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B} snd (Σ≡ i) = snd≡ i import Relation.Binary -open Relation.Binary public using (Preorder ; Transitive ; IsEquivalence ; Rel) +open Relation.Binary public using + ( Preorder ; Transitive ; IsEquivalence ; Rel + ; Setoid ) equalityIsEquivalence : {ℓ : Level} {A : Set ℓ} → IsEquivalence {A = A} _≡_ IsEquivalence.refl equalityIsEquivalence = refl