diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index e5608bc..8856ba3 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -91,13 +91,13 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where issSet = setSig {sA = C.arrowIsSet} {sB = λ x → D.arrowIsSet} ident' : IsIdentity :𝟙: ident' - = Σ≡ (fst C.ident) (fst D.ident) - , Σ≡ (snd C.ident) (snd D.ident) + = Σ≡ (fst C.isIdentity) (fst D.isIdentity) + , Σ≡ (snd C.isIdentity) (snd D.isIdentity) postulate univalent : Univalence.Univalent :rawProduct: ident' instance :isCategory: : IsCategory :rawProduct: IsCategory.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative - IsCategory.ident :isCategory: = ident' + IsCategory.isIdentity :isCategory: = ident' IsCategory.arrowIsSet :isCategory: = issSet IsCategory.univalent :isCategory: = univalent @@ -107,13 +107,13 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where proj₁ : Catt [ :product: , ℂ ] proj₁ = record { raw = record { func* = fst ; func→ = fst } - ; isFunctor = record { ident = refl ; distrib = refl } + ; isFunctor = record { isIdentity = refl ; distrib = refl } } proj₂ : Catt [ :product: , 𝔻 ] proj₂ = record { raw = record { func* = snd ; func→ = snd } - ; isFunctor = record { ident = refl ; distrib = refl } + ; isFunctor = record { isIdentity = refl ; distrib = refl } } module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where @@ -124,7 +124,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where ; func→ = λ x → func→ x₁ x , func→ x₂ x } ; isFunctor = record - { ident = Σ≡ x₁.ident x₂.ident + { isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity ; distrib = Σ≡ x₁.distrib x₂.distrib } } @@ -230,7 +230,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where -- NaturalTransformation F G × ℂ .Arrow A B -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙 - -- :ident: = trans (proj₂ 𝔻.ident) (F .ident) + -- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity) -- where -- open module 𝔻 = IsCategory (𝔻 .isCategory) -- Unfortunately the equational version has some ambigous arguments. @@ -239,8 +239,8 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩ :func→: {c} {c} (identityNat F , 𝟙 ℂ) ≡⟨⟩ 𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.ident ⟩ - func→ F (𝟙 ℂ) ≡⟨ F.ident ⟩ + 𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩ + func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩ 𝟙 𝔻 ∎ where open module 𝔻 = Category 𝔻 @@ -313,7 +313,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where ; func→ = λ {dom} {cod} → :func→: {dom} {cod} } ; isFunctor = record - { ident = λ {o} → :ident: {o} + { isIdentity = λ {o} → :ident: {o} ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} } } diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index 2ea1dc1..5e19a8f 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -29,8 +29,8 @@ module _ (ℓa ℓb : Level) where isAssociative = Σ≡ refl refl module _ {A B : Obj'} {f : Arr A B} where - ident : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f - ident = (Σ≡ refl refl) , Σ≡ refl refl + isIdentity : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f + isIdentity = (Σ≡ refl refl) , Σ≡ refl refl RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb) @@ -45,7 +45,7 @@ module _ (ℓa ℓb : Level) where isCategory : IsCategory RawFam isCategory = record { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h} - ; ident = λ {A} {B} {f} → ident {A} {B} {f = f} + ; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f} ; arrowIsSet = {!!} ; univalent = {!!} } diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index d618990..7aa9526 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -58,7 +58,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where RawIsCategoryFree : IsCategory RawFree RawIsCategoryFree = record { isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}} - ; ident = ident-r , ident-l + ; isIdentity = ident-r , ident-l ; arrowIsSet = {!!} ; univalent = {!!} } diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 16e5124..827fb5a 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -60,8 +60,8 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F) identityNatural F {A = A} {B = B} f = begin 𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.ident ⟩ - F→ f ≡⟨ sym (proj₁ 𝔻.ident) ⟩ + 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩ + F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩ 𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩ 𝔻 [ F→ f ∘ identityTrans F A ] ∎ where @@ -143,10 +143,10 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C eq-r C = begin 𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩ - 𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ proj₁ 𝔻.ident ⟩ + 𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ proj₁ 𝔻.isIdentity ⟩ f' C ∎ eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C - eq-l C = proj₂ 𝔻.ident + eq-l C = proj₂ 𝔻.isIdentity ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f ident-r = lemSig allNatural _ _ (funExt eq-r) ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f @@ -169,7 +169,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat :isCategory: : IsCategory RawFun :isCategory: = record { isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D} - ; ident = λ {A B} → :ident: {A} {B} + ; isIdentity = λ {A B} → :ident: {A} {B} ; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G} ; univalent = {!!} } diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index a43b5e1..7afe5a1 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -165,7 +165,7 @@ RawRel = record RawIsCategoryRel : IsCategory RawRel RawIsCategoryRel = record { isAssociative = funExt is-isAssociative - ; ident = funExt ident-l , funExt ident-r + ; isIdentity = funExt ident-l , funExt ident-r ; arrowIsSet = {!!} ; univalent = {!!} } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 80398e4..76593bc 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -26,8 +26,8 @@ module _ (ℓ : Level) where SetsIsCategory : IsCategory SetsRaw isAssociative SetsIsCategory = refl - proj₁ (ident SetsIsCategory) = funExt λ _ → refl - proj₂ (ident SetsIsCategory) = funExt λ _ → refl + proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl + proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s univalent SetsIsCategory = {!!} @@ -98,7 +98,7 @@ module _ {ℓa ℓb : Level} where ; func→ = ℂ [_∘_] } ; isFunctor = record - { ident = funExt λ _ → proj₂ ident + { isIdentity = funExt λ _ → proj₂ isIdentity ; distrib = funExt λ x → sym isAssociative } } @@ -113,7 +113,7 @@ module _ {ℓa ℓb : Level} where ; func→ = λ f g → ℂ [ g ∘ f ] } ; isFunctor = record - { ident = funExt λ x → proj₁ ident + { isIdentity = funExt λ x → proj₁ isIdentity ; distrib = funExt λ x → isAssociative } } diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 7cbc52b..db70306 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -83,9 +83,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where -- Univalence is indexed by a raw category as well as an identity proof. module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where open RawCategory ℂ - module _ (ident : IsIdentity 𝟙) where + module _ (isIdentity : IsIdentity 𝟙) where idIso : (A : Object) → A ≅ A - idIso A = 𝟙 , (𝟙 , ident) + idIso A = 𝟙 , (𝟙 , isIdentity) -- Lemma 9.1.4 in [HoTT] id-to-iso : (A B : Object) → A ≡ B → A ≅ B @@ -102,9 +102,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc open Univalence ℂ public field isAssociative : IsAssociative - ident : IsIdentity 𝟙 + isIdentity : IsIdentity 𝟙 arrowIsSet : ArrowsAreSets - univalent : Univalent ident + univalent : Univalent isIdentity -- `IsCategory` is a mere proposition. module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where @@ -142,14 +142,14 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where open Cubical.NType.Properties geq : g ≡ g' geq = begin - g ≡⟨ sym (fst ident) ⟩ + g ≡⟨ sym (fst isIdentity) ⟩ g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩ g ∘ (f ∘ g') ≡⟨ isAssociative ⟩ (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩ - 𝟙 ∘ g' ≡⟨ snd ident ⟩ + 𝟙 ∘ g' ≡⟨ snd isIdentity ⟩ g' ∎ - propUnivalent : isProp (Univalent ident) + propUnivalent : isProp (Univalent isIdentity) propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i private @@ -162,27 +162,27 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where -- projections of `IsCategory` - I've arbitrarily chosed to use this -- result from `x : IsCategory C`. I don't know which (if any) possibly -- adverse effects this may have. - ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ] - ident = propIsIdentity x X.ident Y.ident + isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ] + isIdentity = propIsIdentity x X.isIdentity Y.isIdentity done : x ≡ y U : ∀ {a : IsIdentity 𝟙} - → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] + → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ] → (b : Univalent a) → Set _ U eqwal bbb = (λ i → Univalent (eqwal i)) [ X.univalent ≡ bbb ] P : (y : IsIdentity 𝟙) - → (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _ + → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _ P y eq = ∀ (b' : Univalent y) → U eq b' - helper : ∀ (b' : Univalent X.ident) - → (λ _ → Univalent X.ident) [ X.univalent ≡ b' ] + helper : ∀ (b' : Univalent X.isIdentity) + → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ] helper univ = propUnivalent x X.univalent univ - foo = pathJ P helper Y.ident ident - eqUni : U ident Y.univalent + foo = pathJ P helper Y.isIdentity isIdentity + eqUni : U isIdentity Y.univalent eqUni = foo Y.univalent IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i - IC.ident (done i) = ident i + IC.isIdentity (done i) = isIdentity i IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i IC.univalent (done i) = eqUni i @@ -217,7 +217,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where OpIsCategory : IsCategory OpRaw IsCategory.isAssociative OpIsCategory = sym isAssociative - IsCategory.ident OpIsCategory = swap ident + IsCategory.isIdentity OpIsCategory = swap isIdentity IsCategory.arrowIsSet OpIsCategory = arrowIsSet IsCategory.univalent OpIsCategory = {!!} @@ -243,7 +243,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where module IsCat = IsCategory (ℂ .isCategory) rawIsCat : (i : I) → IsCategory (rawOp i) isAssociative (rawIsCat i) = IsCat.isAssociative - ident (rawIsCat i) = IsCat.ident + isIdentity (rawIsCat i) = IsCat.isIdentity arrowIsSet (rawIsCat i) = IsCat.arrowIsSet univalent (rawIsCat i) = IsCat.univalent diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index aac423c..caa2131 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -33,7 +33,7 @@ module _ {ℓc ℓc' ℓd ℓd'} record IsFunctor (F : RawFunctor) : 𝓤 where open RawFunctor F public field - ident : IsIdentity + isIdentity : IsIdentity distrib : IsDistributive record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where @@ -55,7 +55,7 @@ module _ propIsFunctor : isProp (IsFunctor _ _ F) propIsFunctor isF0 isF1 i = record - { ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i + { isIdentity = 𝔻.arrowIsSet _ _ isF0.isIdentity isF1.isIdentity i ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i } where @@ -116,10 +116,10 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F instance isFunctor' : IsFunctor A C _∘fr_ isFunctor' = record - { ident = begin + { isIdentity = begin (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩ - F→ (G→ (𝟙 A)) ≡⟨ cong F→ (ident G)⟩ - F→ (𝟙 B) ≡⟨ ident F ⟩ + F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩ + F→ (𝟙 B) ≡⟨ isIdentity F ⟩ 𝟙 C ∎ ; distrib = dist } @@ -135,7 +135,7 @@ identity = record ; func→ = λ x → x } ; isFunctor = record - { ident = refl + { isIdentity = refl ; distrib = refl } } diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 03dd529..2f3c1e9 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -17,25 +17,25 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object iso-is-epi : Isomorphism f → Epimorphism {X = X} f iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin - g₀ ≡⟨ sym (proj₁ ident) ⟩ + g₀ ≡⟨ sym (proj₁ isIdentity) ⟩ g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩ (g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩ (g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩ g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩ - g₁ ∘ 𝟙 ≡⟨ proj₁ ident ⟩ + g₁ ∘ 𝟙 ≡⟨ proj₁ isIdentity ⟩ g₁ ∎ iso-is-mono : Isomorphism f → Monomorphism {X = X} f iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq = begin - g₀ ≡⟨ sym (proj₂ ident) ⟩ + g₀ ≡⟨ sym (proj₂ isIdentity) ⟩ 𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩ f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩ f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩ (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩ - 𝟙 ∘ g₁ ≡⟨ proj₂ ident ⟩ + 𝟙 ∘ g₁ ≡⟨ proj₂ isIdentity ⟩ g₁ ∎ iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f @@ -70,7 +70,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat module _ {c : Category.Object ℂ} where eqTrans : (λ _ → Transformation (prshf c) (prshf c)) [ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ] - eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂ + eqTrans = funExt λ x → funExt λ x → ℂ.isIdentity .proj₂ open import Cubical.NType.Properties open import Cat.Categories.Fun @@ -78,7 +78,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat :ident: = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq where eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) - eq = funExt λ A → funExt λ B → proj₂ ℂ.ident + eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢}) yoneda = record @@ -87,7 +87,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat ; func→ = :func→: } ; isFunctor = record - { ident = :ident: + { isIdentity = :ident: ; distrib = {!!} } }