From 04144db606c9418db73bb1a0c7d8d2b2f5091281 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 9 Apr 2018 18:02:39 +0200 Subject: [PATCH] Simplifications and renaming --- src/Cat/Category.agda | 80 +++++++++++++++++-------------------------- 1 file changed, 31 insertions(+), 49 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index abc7830..bb26526 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -121,9 +121,6 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Univalent : Set (ℓa ⊔ ℓb) Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (idToIso A B) - import Cat.Equivalence as E - open E public using () renaming (Isomorphism to TypeIsomorphism) - univalenceFromIsomorphism : {A B : Object} → TypeIsomorphism (idToIso A B) → isEquiv (A ≡ B) (A ≅ B) (idToIso A B) univalenceFromIsomorphism = fromIso _ _ @@ -305,6 +302,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where iso-to-id : (A ≅ B) → (A ≡ B) iso-to-id = fst (toIso _ _ univalent) + asTypeIso : TypeIsomorphism (idToIso A B) + asTypeIso = toIso _ _ univalent + -- | All projections are propositions. module Propositionality where -- | Terminal objects are propositional - a.k.a uniqueness of terminal @@ -333,10 +333,8 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where right = Yprop _ _ iso : X ≅ Y iso = X→Y , Y→X , left , right - fromIso' : X ≅ Y → X ≡ Y - fromIso' = fst (toIso (X ≡ Y) (X ≅ Y) univalent) p0 : X ≡ Y - p0 = fromIso' iso + p0 = iso-to-id iso p1 : (λ i → IsTerminal (p0 i)) [ Xit ≡ Yit ] p1 = lemPropF propIsTerminal p0 res : Xt ≡ Yt @@ -365,14 +363,8 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where right = Xprop _ _ iso : X ≅ Y iso = Y→X , X→Y , right , left - fromIso' : X ≅ Y → X ≡ Y - fromIso' = fst (toIso (X ≡ Y) (X ≅ Y) univalent) - p0 : X ≡ Y - p0 = fromIso' iso - p1 : (λ i → IsInitial (p0 i)) [ Xii ≡ Yii ] - p1 = lemPropF propIsInitial p0 res : Xi ≡ Yi - res i = p0 i , p1 i + res = lemSig propIsInitial _ _ (iso-to-id iso) module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where open RawCategory ℂ @@ -495,72 +487,62 @@ module Opposite {ℓa ℓb : Level} where module _ {A B : ℂ.Object} where k : Equivalence.Isomorphism (ℂ.idToIso A B) k = toIso _ _ ℂ.univalent - open Σ k renaming (fst to f ; snd to inv) - open AreInverses inv + open Σ k renaming (fst to η ; snd to inv-η) + open AreInverses inv-η _⊙_ = Function._∘_ infixr 9 _⊙_ - -- f : A ℂ.≅ B → A ≡ B - flipDem : A ≅ B → A ℂ.≅ B - flipDem (f , g , inv) = g , f , inv + genericly : {ℓa ℓb ℓc : Level} {a : Set ℓa} {b : Set ℓb} {c : Set ℓc} + → a × b × c → b × a × c + genericly (a , b , c) = (b , a , c) - flopDem : A ℂ.≅ B → A ≅ B - flopDem (f , g , inv) = g , f , inv + shuffle : A ≅ B → A ℂ.≅ B + shuffle (f , g , inv) = g , f , inv + + shuffle~ : A ℂ.≅ B → A ≅ B + shuffle~ (f , g , inv) = g , f , inv -- Shouldn't be necessary to use `arrowsAreSets` here, but we have it, -- so why not? - lem : (p : A ≡ B) → idToIso A B p ≡ flopDem (ℂ.idToIso A B p) - lem p i = l≡r i + lem : (p : A ≡ B) → idToIso A B p ≡ shuffle~ (ℂ.idToIso A B p) + lem p = Σ≡ refl (Σ≡ refl (Σ≡ (ℂ.arrowsAreSets _ _ l-l r-l) (ℂ.arrowsAreSets _ _ l-r r-r))) where l = idToIso A B p - r = flopDem (ℂ.idToIso A B p) + r = shuffle~ (ℂ.idToIso A B p) open Σ l renaming (fst to l-obv ; snd to l-areInv) open Σ l-areInv renaming (fst to l-invs ; snd to l-iso) open Σ l-iso renaming (fst to l-l ; snd to l-r) open Σ r renaming (fst to r-obv ; snd to r-areInv) open Σ r-areInv renaming (fst to r-invs ; snd to r-iso) open Σ r-iso renaming (fst to r-l ; snd to r-r) - l-obv≡r-obv : l-obv ≡ r-obv - l-obv≡r-obv = refl - l-invs≡r-invs : l-invs ≡ r-invs - l-invs≡r-invs = refl - l-l≡r-l : l-l ≡ r-l - l-l≡r-l = ℂ.arrowsAreSets _ _ l-l r-l - l-r≡r-r : l-r ≡ r-r - l-r≡r-r = ℂ.arrowsAreSets _ _ l-r r-r - l≡r : l ≡ r - l≡r i = l-obv≡r-obv i , l-invs≡r-invs i , l-l≡r-l i , l-r≡r-r i - ff : A ≅ B → A ≡ B - ff = f ⊙ flipDem + ζ : A ≅ B → A ≡ B + ζ = η ⊙ shuffle -- inv : AreInverses (ℂ.idToIso A B) f - invv : AreInverses (idToIso A B) ff + inv-ζ : AreInverses (idToIso A B) ζ -- recto-verso : ℂ.idToIso A B ∘ f ≡ idFun (A ℂ.≅ B) - invv = record + inv-ζ = record { verso-recto = funExt (λ x → begin - (ff ⊙ idToIso A B) x ≡⟨⟩ - (f ⊙ flipDem ⊙ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → f ⊙ flipDem ⊙ φ) (funExt lem)) ⟩ - (f ⊙ flipDem ⊙ flopDem ⊙ ℂ.idToIso A B) x ≡⟨⟩ - (f ⊙ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩ + (ζ ⊙ idToIso A B) x ≡⟨⟩ + (η ⊙ shuffle ⊙ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ + (η ⊙ shuffle ⊙ shuffle~ ⊙ ℂ.idToIso A B) x ≡⟨⟩ + (η ⊙ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩ x ∎) ; recto-verso = funExt (λ x → begin - (idToIso A B ⊙ f ⊙ flipDem) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ⊙ f ⊙ flipDem) (funExt lem)) ⟩ - (flopDem ⊙ ℂ.idToIso A B ⊙ f ⊙ flipDem) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → flopDem ⊙ φ ⊙ flipDem) recto-verso) ⟩ - (flopDem ⊙ flipDem) x ≡⟨⟩ + (idToIso A B ⊙ η ⊙ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ⊙ η ⊙ shuffle) (funExt lem)) ⟩ + (shuffle~ ⊙ ℂ.idToIso A B ⊙ η ⊙ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ⊙ φ ⊙ shuffle) recto-verso) ⟩ + (shuffle~ ⊙ shuffle) x ≡⟨⟩ x ∎) } h : Equivalence.Isomorphism (idToIso A B) - h = ff , invv - univalent : isEquiv (A ≡ B) (A ≅ B) - (Univalence.idToIso (swap ℂ.isIdentity) A B) - univalent = fromIso _ _ h + h = ζ , inv-ζ isCategory : IsCategory opRaw IsCategory.isPreCategory isCategory = isPreCategory - IsCategory.univalent isCategory = univalent + IsCategory.univalent isCategory = univalenceFromIsomorphism h opposite : Category ℓa ℓb Category.raw opposite = opRaw