From 5cbc409770a33717f931e29731eb9859dedeb53c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:43:49 +0100 Subject: [PATCH] Rename assoc to isAssociative --- src/Cat/Categories/Cat.agda | 14 +++++++------- src/Cat/Categories/Fam.agda | 6 +++--- src/Cat/Categories/Free.agda | 10 +++++----- src/Cat/Categories/Fun.agda | 14 +++++++------- src/Cat/Categories/Rel.agda | 8 ++++---- src/Cat/Categories/Sets.agda | 6 +++--- src/Cat/Category.agda | 10 +++++----- src/Cat/Category/Properties.agda | 10 +++++----- 8 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 08516cf..e5608bc 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -43,8 +43,8 @@ module _ (ℓ ℓ' : Level) where } private open RawCategory RawCat - assoc : IsAssociative - assoc {f = F} {G} {H} = assc {F = F} {G = G} {H = H} + isAssociative : IsAssociative + isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H} -- TODO: Rename `ident'` to `ident` after changing how names are exposed in Functor. ident' : IsIdentity identity ident' = ident-r , ident-l @@ -96,7 +96,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where postulate univalent : Univalence.Univalent :rawProduct: ident' instance :isCategory: : IsCategory :rawProduct: - IsCategory.assoc :isCategory: = Σ≡ C.assoc D.assoc + IsCategory.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative IsCategory.ident :isCategory: = ident' IsCategory.arrowIsSet :isCategory: = issSet IsCategory.univalent :isCategory: = univalent @@ -288,15 +288,15 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] - ≡⟨ sym assoc ⟩ + ≡⟨ sym isAssociative ⟩ 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) assoc ⟩ + ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) isAssociative ⟩ 𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ func→ H f ∘ η A ] ∘ θ A ] ] ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩ 𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ η B ∘ func→ G f ] ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (sym assoc) ⟩ + ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (sym isAssociative) ⟩ 𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ] - ≡⟨ assoc ⟩ + ≡⟨ isAssociative ⟩ 𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index 83f19b0..2ea1dc1 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -25,8 +25,8 @@ module _ (ℓa ℓb : Level) where c ⟨ g ∘ f ⟩ = _∘_ {c = c} g f module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where - assoc : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩ - assoc = Σ≡ refl refl + isAssociative : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩ + isAssociative = Σ≡ refl refl module _ {A B : Obj'} {f : Arr A B} where ident : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f @@ -44,7 +44,7 @@ module _ (ℓa ℓb : Level) where instance isCategory : IsCategory RawFam isCategory = record - { assoc = λ {A} {B} {C} {D} {f} {g} {h} → assoc {D = D} {f} {g} {h} + { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h} ; ident = λ {A} {B} {f} → ident {A} {B} {f = f} ; arrowIsSet = {!!} ; univalent = {!!} diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 19cabeb..d618990 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -26,16 +26,16 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where open Category ℂ private - p-assoc : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D} + p-isAssociative : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D} → p ++ (q ++ r) ≡ (p ++ q) ++ r - p-assoc {r = r} {q} {empty} = refl - p-assoc {A} {B} {C} {D} {r = r} {q} {cons x p} = begin + p-isAssociative {r = r} {q} {empty} = refl + p-isAssociative {A} {B} {C} {D} {r = r} {q} {cons x p} = begin cons x p ++ (q ++ r) ≡⟨ cong (cons x) lem ⟩ cons x ((p ++ q) ++ r) ≡⟨⟩ (cons x p ++ q) ++ r ∎ where lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r) - lem = p-assoc {r = r} {q} {p} + lem = p-isAssociative {r = r} {q} {p} ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p ident-r {p = empty} = refl @@ -57,7 +57,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where } RawIsCategoryFree : IsCategory RawFree RawIsCategoryFree = record - { assoc = λ { {f = f} {g} {h} → p-assoc {r = f} {g} {h}} + { isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}} ; ident = ident-r , ident-l ; arrowIsSet = {!!} ; univalent = {!!} diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index b5a33c8..16e5124 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -84,11 +84,11 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin 𝔻 [ (θ ∘nt η) B ∘ F.func→ f ] ≡⟨⟩ - 𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym assoc ⟩ + 𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym isAssociative ⟩ 𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩ - 𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ assoc ⟩ + 𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ isAssociative ⟩ 𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩ - 𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩ + 𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym isAssociative ⟩ 𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩ 𝔻 [ H.func→ f ∘ (θ ∘nt η) A ] ∎ where @@ -130,9 +130,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ') _g⊕f_ = _:⊕:_ {A} {B} {C} _h⊕g_ = _:⊕:_ {B} {C} {D} - :assoc: : L ≡ R - :assoc: = lemSig (naturalIsProp {F = A} {D}) - L R (funExt (λ x → assoc)) + :isAssociative: : L ≡ R + :isAssociative: = lemSig (naturalIsProp {F = A} {D}) + L R (funExt (λ x → isAssociative)) where open Category 𝔻 @@ -168,7 +168,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat instance :isCategory: : IsCategory RawFun :isCategory: = record - { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D} + { isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D} ; ident = λ {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 8a93274..a43b5e1 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -149,10 +149,10 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) equi = fwd Cubical.FromStdLib., isequiv - -- assocc : Q + (R + S) ≡ (Q + R) + S - is-assoc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) + -- isAssociativec : Q + (R + S) ≡ (Q + R) + S + is-isAssociative : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) - is-assoc = equivToPath equi + is-isAssociative = equivToPath equi RawRel : RawCategory (lsuc lzero) (lsuc lzero) RawRel = record @@ -164,7 +164,7 @@ RawRel = record RawIsCategoryRel : IsCategory RawRel RawIsCategoryRel = record - { assoc = funExt is-assoc + { isAssociative = funExt is-isAssociative ; ident = funExt ident-l , funExt ident-r ; arrowIsSet = {!!} ; univalent = {!!} diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index d6c1329..80398e4 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -25,7 +25,7 @@ module _ (ℓ : Level) where _∘_ SetsRaw = Function._∘′_ SetsIsCategory : IsCategory SetsRaw - assoc SetsIsCategory = refl + isAssociative SetsIsCategory = refl proj₁ (ident SetsIsCategory) = funExt λ _ → refl proj₂ (ident SetsIsCategory) = funExt λ _ → refl arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s @@ -99,7 +99,7 @@ module _ {ℓa ℓb : Level} where } ; isFunctor = record { ident = funExt λ _ → proj₂ ident - ; distrib = funExt λ x → sym assoc + ; distrib = funExt λ x → sym isAssociative } } where @@ -114,7 +114,7 @@ module _ {ℓa ℓb : Level} where } ; isFunctor = record { ident = funExt λ x → proj₁ ident - ; distrib = funExt λ x → assoc + ; distrib = funExt λ x → isAssociative } } where diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 536f0b7..7cbc52b 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -101,7 +101,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc open RawCategory ℂ open Univalence ℂ public field - assoc : IsAssociative + isAssociative : IsAssociative ident : IsIdentity 𝟙 arrowIsSet : ArrowsAreSets univalent : Univalent ident @@ -144,7 +144,7 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where geq = begin g ≡⟨ sym (fst ident) ⟩ g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩ - g ∘ (f ∘ g') ≡⟨ assoc ⟩ + g ∘ (f ∘ g') ≡⟨ isAssociative ⟩ (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩ 𝟙 ∘ g' ≡⟨ snd ident ⟩ g' ∎ @@ -181,7 +181,7 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where foo = pathJ P helper Y.ident ident eqUni : U ident Y.univalent eqUni = foo Y.univalent - IC.assoc (done i) = propIsAssociative x X.assoc Y.assoc i + IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i IC.ident (done i) = ident i IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i IC.univalent (done i) = eqUni i @@ -216,7 +216,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where RawCategory._∘_ OpRaw = Function.flip _∘_ OpIsCategory : IsCategory OpRaw - IsCategory.assoc OpIsCategory = sym assoc + IsCategory.isAssociative OpIsCategory = sym isAssociative IsCategory.ident OpIsCategory = swap ident IsCategory.arrowIsSet OpIsCategory = arrowIsSet IsCategory.univalent OpIsCategory = {!!} @@ -242,7 +242,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where open IsCategory module IsCat = IsCategory (ℂ .isCategory) rawIsCat : (i : I) → IsCategory (rawOp i) - assoc (rawIsCat i) = IsCat.assoc + isAssociative (rawIsCat i) = IsCat.isAssociative ident (rawIsCat i) = IsCat.ident arrowIsSet (rawIsCat i) = IsCat.arrowIsSet univalent (rawIsCat i) = IsCat.univalent diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index f8b60f8..03dd529 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -19,9 +19,9 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin g₀ ≡⟨ sym (proj₁ ident) ⟩ g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ - g₀ ∘ (f ∘ f-) ≡⟨ assoc ⟩ + g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩ (g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩ - (g₁ ∘ f) ∘ f- ≡⟨ sym assoc ⟩ + (g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩ g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩ g₁ ∘ 𝟙 ≡⟨ proj₁ ident ⟩ g₁ ∎ @@ -31,9 +31,9 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object begin g₀ ≡⟨ sym (proj₂ ident) ⟩ 𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ - (f- ∘ f) ∘ g₀ ≡⟨ sym assoc ⟩ + (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩ f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩ - f- ∘ (f ∘ g₁) ≡⟨ assoc ⟩ + f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩ (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩ 𝟙 ∘ g₁ ≡⟨ proj₂ ident ⟩ g₁ ∎ @@ -65,7 +65,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where :func→: : NaturalTransformation (prshf A) (prshf B) - :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc + :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative module _ {c : Category.Object ℂ} where eqTrans : (λ _ → Transformation (prshf c) (prshf c))