From 48423cc8168b83aed29a708227e6e556097fe5d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:51:44 +0100 Subject: [PATCH] Rename arrowIsSet to arrowsAreSets --- src/Cat/Categories/Cat.agda | 4 ++-- src/Cat/Categories/Fam.agda | 2 +- src/Cat/Categories/Free.agda | 2 +- src/Cat/Categories/Fun.agda | 6 +++--- src/Cat/Categories/Rel.agda | 2 +- src/Cat/Categories/Sets.agda | 6 +++--- src/Cat/Category.agda | 18 +++++++++--------- src/Cat/Category/Functor.agda | 4 ++-- 8 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 8856ba3..b1a1bfb 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -88,7 +88,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where module D = Category 𝔻 open import Cubical.Sigma issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B) - issSet = setSig {sA = C.arrowIsSet} {sB = λ x → D.arrowIsSet} + issSet = setSig {sA = C.arrowsAreSets} {sB = λ x → D.arrowsAreSets} ident' : IsIdentity :𝟙: ident' = Σ≡ (fst C.isIdentity) (fst D.isIdentity) @@ -98,7 +98,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where :isCategory: : IsCategory :rawProduct: IsCategory.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative IsCategory.isIdentity :isCategory: = ident' - IsCategory.arrowIsSet :isCategory: = issSet + IsCategory.arrowsAreSets :isCategory: = issSet IsCategory.univalent :isCategory: = univalent :product: : Category ℓ ℓ' diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index 5e19a8f..6150dd2 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -46,7 +46,7 @@ module _ (ℓa ℓb : Level) where isCategory = record { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h} ; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f} - ; arrowIsSet = {!!} + ; arrowsAreSets = {!!} ; univalent = {!!} } diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 7aa9526..5441abc 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -59,6 +59,6 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where RawIsCategoryFree = record { isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}} ; isIdentity = ident-r , ident-l - ; arrowIsSet = {!!} + ; arrowsAreSets = {!!} ; univalent = {!!} } diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 827fb5a..3e4dcbf 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -101,13 +101,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat module _ {F G : Functor ℂ 𝔻} where transformationIsSet : isSet (Transformation F G) - transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C) (λ l → q l C) i j + transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C) (λ l → q l C) i j naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ) naturalIsProp θ θNat θNat' = lem where lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ] - lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i + lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i naturalTransformationIsSets : isSet (NaturalTransformation F G) naturalTransformationIsSets = sigPresSet transformationIsSet @@ -170,7 +170,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat :isCategory: = record { isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D} ; isIdentity = λ {A B} → :ident: {A} {B} - ; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G} + ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G} ; univalent = {!!} } diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 7afe5a1..de3d1f2 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -166,6 +166,6 @@ RawIsCategoryRel : IsCategory RawRel RawIsCategoryRel = record { isAssociative = funExt is-isAssociative ; isIdentity = funExt ident-l , funExt ident-r - ; arrowIsSet = {!!} + ; arrowsAreSets = {!!} ; univalent = {!!} } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 76593bc..f9e26e0 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -28,7 +28,7 @@ module _ (ℓ : Level) where isAssociative SetsIsCategory = refl proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl - arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s + arrowsAreSets SetsIsCategory {B = (_ , s)} = setPi λ _ → s univalent SetsIsCategory = {!!} 𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ @@ -94,7 +94,7 @@ module _ {ℓa ℓb : Level} where representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ representable {ℂ = ℂ} A = record { raw = record - { func* = λ B → ℂ [ A , B ] , arrowIsSet + { func* = λ B → ℂ [ A , B ] , arrowsAreSets ; func→ = ℂ [_∘_] } ; isFunctor = record @@ -109,7 +109,7 @@ module _ {ℓa ℓb : Level} where presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ presheaf {ℂ = ℂ} B = record { raw = record - { func* = λ A → ℂ [ A , B ] , arrowIsSet + { func* = λ A → ℂ [ A , B ] , arrowsAreSets ; func→ = λ f g → ℂ [ g ∘ f ] } ; isFunctor = record diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index db70306..6c3172e 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -103,7 +103,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc field isAssociative : IsAssociative isIdentity : IsIdentity 𝟙 - arrowIsSet : ArrowsAreSets + arrowsAreSets : ArrowsAreSets univalent : Univalent isIdentity -- `IsCategory` is a mere proposition. @@ -115,12 +115,12 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where open import Cubical.NType.Properties propIsAssociative : isProp IsAssociative - propIsAssociative x y i = arrowIsSet _ _ x y i + propIsAssociative x y i = arrowsAreSets _ _ x y i propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f) propIsIdentity a b i - = arrowIsSet _ _ (fst a) (fst b) i - , arrowIsSet _ _ (snd a) (snd b) i + = arrowsAreSets _ _ (fst a) (fst b) i + , arrowsAreSets _ _ (snd a) (snd b) i propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B)) propArrowIsSet a b i = isSetIsProp a b i @@ -129,9 +129,9 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where propIsInverseOf x y = λ i → let h : fst x ≡ fst y - h = arrowIsSet _ _ (fst x) (fst y) + h = arrowsAreSets _ _ (fst x) (fst y) hh : snd x ≡ snd y - hh = arrowIsSet _ _ (snd x) (snd y) + hh = arrowsAreSets _ _ (snd x) (snd y) in h i , hh i module _ {A B : Object} {f : Arrow A B} where @@ -183,7 +183,7 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where eqUni = foo Y.univalent IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i IC.isIdentity (done i) = isIdentity i - IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i + IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i IC.univalent (done i) = eqUni i propIsCategory : isProp (IsCategory C) @@ -218,7 +218,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where OpIsCategory : IsCategory OpRaw IsCategory.isAssociative OpIsCategory = sym isAssociative IsCategory.isIdentity OpIsCategory = swap isIdentity - IsCategory.arrowIsSet OpIsCategory = arrowIsSet + IsCategory.arrowsAreSets OpIsCategory = arrowsAreSets IsCategory.univalent OpIsCategory = {!!} Opposite : Category ℓa ℓb @@ -244,7 +244,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where rawIsCat : (i : I) → IsCategory (rawOp i) isAssociative (rawIsCat i) = IsCat.isAssociative isIdentity (rawIsCat i) = IsCat.isIdentity - arrowIsSet (rawIsCat i) = IsCat.arrowIsSet + arrowsAreSets (rawIsCat i) = IsCat.arrowsAreSets univalent (rawIsCat i) = IsCat.univalent Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index caa2131..ee643ce 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -55,8 +55,8 @@ module _ propIsFunctor : isProp (IsFunctor _ _ F) propIsFunctor isF0 isF1 i = record - { isIdentity = 𝔻.arrowIsSet _ _ isF0.isIdentity isF1.isIdentity i - ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i + { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i + ; distrib = 𝔻.arrowsAreSets _ _ isF0.distrib isF1.distrib i } where module isF0 = IsFunctor isF0