From 32b9ce2ea894dce473fcac7520f0019717dc9481 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 22 Feb 2018 15:31:54 +0100 Subject: [PATCH 01/20] Use new syntax in cat --- src/Cat/Categories/Cat.agda | 117 +++++++++++++++++++----------------- 1 file changed, 63 insertions(+), 54 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 1ec9acb..441bd92 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -18,7 +18,7 @@ open Equality.Data.Product open Functor open IsFunctor -open Category hiding (_∘_) +open Category using (Object ; 𝟙) -- The category of categories module _ (ℓ ℓ' : Level) where @@ -45,7 +45,7 @@ module _ (ℓ ℓ' : Level) where ] assc : H ∘f (G ∘f F) ≡ (H ∘f G) ∘f F - assc = Functor≡ eq* eq→ (IsFunctor≡ eqI eqD) + assc = Functor≡ eq* eq→ module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where module _ where @@ -55,7 +55,7 @@ module _ (ℓ ℓ' : Level) where -- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f eq→ : PathP (λ i → - {x y : Object ℂ} → Arrow ℂ x y → Arrow 𝔻 (func* F x) (func* F y)) + {x y : Object ℂ} → ℂ [ x , y ] → 𝔻 [ func* F x , func* F y ]) (func→ (F ∘f identity)) (func→ F) eq→ = refl postulate @@ -69,14 +69,14 @@ module _ (ℓ ℓ' : Level) where eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ]) ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib) ident-r : F ∘f identity ≡ F - ident-r = Functor≡ eq* eq→ (IsFunctor≡ eqI-r eqD-r) + ident-r = Functor≡ eq* eq→ module _ where private postulate - eq* : (identity ∘f F) .func* ≡ F .func* + eq* : func* (identity ∘f F) ≡ func* F eq→ : PathP (λ i → {x y : Object ℂ} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ]) - ((identity ∘f F) .func→) (F .func→) + (func→ (identity ∘f F)) (func→ F) eqI : (λ i → ∀ {A : Object ℂ} → eq→ i (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {eq* i A}) [ ((identity ∘f F) .isFunctor .ident) ≡ (F .isFunctor .ident) ] eqD : PathP (λ i → {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} @@ -84,7 +84,7 @@ module _ (ℓ ℓ' : Level) where ((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib) -- (λ z → eq* i z) (eq→ i) ident-l : identity ∘f F ≡ F - ident-l = Functor≡ eq* eq→ λ i → record { ident = eqI i ; distrib = eqD i } + ident-l = Functor≡ eq* eq→ RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') RawCat = @@ -104,11 +104,11 @@ module _ (ℓ ℓ' : Level) where :isCategory: : IsCategory RawCat assoc :isCategory: {f = F} {G} {H} = assc {F = F} {G = G} {H = H} ident :isCategory: = ident-r , ident-l - arrow-is-set :isCategory: = {!!} + arrowIsSet :isCategory: = {!!} univalent :isCategory: = {!!} Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') - raw Cat = RawCat + Category.raw Cat = RawCat module _ {ℓ ℓ' : Level} where module _ (ℂ 𝔻 : Category ℓ ℓ') where @@ -116,7 +116,7 @@ module _ {ℓ ℓ' : Level} where Catt = Cat ℓ ℓ' :Object: = Object ℂ × Object 𝔻 :Arrow: : :Object: → :Object: → Set ℓ' - :Arrow: (c , d) (c' , d') = Arrow ℂ c c' × Arrow 𝔻 d d' + :Arrow: (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] :𝟙: : {o : :Object:} → :Arrow: o o :𝟙: = 𝟙 ℂ , 𝟙 𝔻 _:⊕:_ : @@ -132,8 +132,8 @@ module _ {ℓ ℓ' : Level} where RawCategory.𝟙 :rawProduct: = :𝟙: RawCategory._∘_ :rawProduct: = _:⊕:_ - module C = IsCategory (ℂ .isCategory) - module D = IsCategory (𝔻 .isCategory) + module C = Category ℂ + module D = Category 𝔻 postulate issSet : {A B : RawCategory.Object :rawProduct:} → isSet (RawCategory.Arrow :rawProduct: A B) instance @@ -150,17 +150,23 @@ module _ {ℓ ℓ' : Level} where IsCategory.ident :isCategory: = Σ≡ (fst C.ident) (fst D.ident) , Σ≡ (snd C.ident) (snd D.ident) - IsCategory.arrow-is-set :isCategory: = issSet + IsCategory.arrowIsSet :isCategory: = issSet IsCategory.univalent :isCategory: = {!!} :product: : Category ℓ ℓ' - raw :product: = :rawProduct: + Category.raw :product: = :rawProduct: proj₁ : Catt [ :product: , ℂ ] - proj₁ = record { func* = fst ; func→ = fst ; isFunctor = record { ident = refl ; distrib = refl } } + proj₁ = record + { raw = record { func* = fst ; func→ = fst } + ; isFunctor = record { ident = refl ; distrib = refl } + } proj₂ : Catt [ :product: , 𝔻 ] - proj₂ = record { func* = snd ; func→ = snd ; isFunctor = record { ident = refl ; distrib = refl } } + proj₂ = record + { raw = record { func* = snd ; func→ = snd } + ; isFunctor = record { ident = refl ; distrib = refl } + } module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where open Functor @@ -232,7 +238,7 @@ module _ (ℓ : Level) where :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻} :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 - :func*: (F , A) = F .func* A + :func*: (F , A) = func* F A module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where private @@ -247,27 +253,27 @@ module _ (ℓ : Level) where B = proj₂ cod :func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ]) - → 𝔻 [ F .func* A , G .func* B ] + → 𝔻 [ func* F A , func* G B ] :func→: ((θ , θNat) , f) = result where - θA : 𝔻 [ F .func* A , G .func* A ] + θA : 𝔻 [ func* F A , func* G A ] θA = θ A - θB : 𝔻 [ F .func* B , G .func* B ] + θB : 𝔻 [ func* F B , func* G B ] θB = θ B - F→f : 𝔻 [ F .func* A , F .func* B ] - F→f = F .func→ f - G→f : 𝔻 [ G .func* A , G .func* B ] - G→f = G .func→ f - l : 𝔻 [ F .func* A , G .func* B ] + F→f : 𝔻 [ func* F A , func* F B ] + F→f = func→ F f + G→f : 𝔻 [ func* G A , func* G B ] + G→f = func→ G f + l : 𝔻 [ func* F A , func* G B ] l = 𝔻 [ θB ∘ F→f ] - r : 𝔻 [ F .func* A , G .func* B ] + r : 𝔻 [ func* F A , func* G B ] r = 𝔻 [ G→f ∘ θA ] -- There are two choices at this point, -- but I suppose the whole point is that -- by `θNat f` we have `l ≡ r` -- lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ] -- lem = θNat f - result : 𝔻 [ F .func* A , G .func* B ] + result : 𝔻 [ func* F A , func* G B ] result = l _×p_ = product @@ -285,16 +291,16 @@ module _ (ℓ : Level) where -- where -- open module 𝔻 = IsCategory (𝔻 .isCategory) -- Unfortunately the equational version has some ambigous arguments. - :ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {o = proj₂ c}) ≡ 𝟙 𝔻 + :ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 :ident: = begin :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩ :func→: {c} {c} (identityNat F , 𝟙 ℂ) ≡⟨⟩ - 𝔻 [ identityTrans F C ∘ F .func→ (𝟙 ℂ)] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F .func→ (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.ident ⟩ - F .func→ (𝟙 ℂ) ≡⟨ F.ident ⟩ + 𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩ + 𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.ident ⟩ + func→ F (𝟙 ℂ) ≡⟨ F.ident ⟩ 𝟙 𝔻 ∎ where - open module 𝔻 = IsCategory (𝔻 .isCategory) + open module 𝔻 = Category 𝔻 open module F = IsFunctor (F .isFunctor) module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where @@ -331,35 +337,38 @@ module _ (ℓ : Level) where ηθNat = proj₂ ηθNT :distrib: : - 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F .func→ ( ℂ [ g ∘ f ] ) ] - ≡ 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ] + 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] + ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] :distrib: = begin - 𝔻 [ (ηθ C) ∘ F .func→ (ℂ [ g ∘ f ]) ] + 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ - 𝔻 [ H .func→ (ℂ [ g ∘ f ]) ∘ (ηθ A) ] + 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ - 𝔻 [ 𝔻 [ H .func→ g ∘ H .func→ f ] ∘ (ηθ A) ] + 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] ≡⟨ sym assoc ⟩ - 𝔻 [ H .func→ g ∘ 𝔻 [ H .func→ f ∘ ηθ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) assoc ⟩ - 𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ H .func→ f ∘ η A ] ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩ - 𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ η B ∘ G .func→ f ] ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (sym assoc) ⟩ - 𝔻 [ H .func→ g ∘ 𝔻 [ η B ∘ 𝔻 [ G .func→ f ∘ θ A ] ] ] ≡⟨ assoc ⟩ - 𝔻 [ 𝔻 [ H .func→ g ∘ η B ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ G .func→ f ∘ θ A ] ]) (sym (ηNat g)) ⟩ - 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ φ ]) (sym (θNat f)) ⟩ - 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ] ∎ + 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) assoc ⟩ + 𝔻 [ 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) ⟩ + 𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ] + ≡⟨ assoc ⟩ + 𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩ + 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩ + 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎ where - open IsCategory (𝔻 .isCategory) - open module H = IsFunctor (H .isFunctor) + open Category 𝔻 + module H = IsFunctor (H .isFunctor) :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 :eval: = record - { func* = :func*: - ; func→ = λ {dom} {cod} → :func→: {dom} {cod} + { raw = record + { func* = :func*: + ; func→ = λ {dom} {cod} → :func→: {dom} {cod} + } ; isFunctor = record { ident = λ {o} → :ident: {o} ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} @@ -371,7 +380,7 @@ module _ (ℓ : Level) where postulate transpose : Functor 𝔸 :obj: - eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F + eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F -- eq' : (Catℓ [ :eval: ∘ -- (record { product = product } HasProducts.|×| transpose) From a87d404aad2511c694c46a8c604a975bf67ae167 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 10:34:37 +0100 Subject: [PATCH 02/20] Refactor category of categories No longer actually define the category. Just define the raw category and a few results about it. --- src/Cat/Categories/Cat.agda | 290 ++++++++++++++++++------------------ 1 file changed, 148 insertions(+), 142 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 441bd92..e31221c 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -86,34 +86,43 @@ module _ (ℓ ℓ' : Level) where ident-l : identity ∘f F ≡ F ident-l = Functor≡ eq* eq→ - RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') - RawCat = - record - { Object = Category ℓ ℓ' - ; Arrow = Functor - ; 𝟙 = identity - ; _∘_ = _∘f_ - -- What gives here? Why can I not name the variables directly? - -- ; isCategory = record - -- { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H} - -- ; ident = ident-r , ident-l - -- } - } - open IsCategory - instance - :isCategory: : IsCategory RawCat - assoc :isCategory: {f = F} {G} {H} = assc {F = F} {G = G} {H = H} - ident :isCategory: = ident-r , ident-l - arrowIsSet :isCategory: = {!!} - univalent :isCategory: = {!!} + RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') + RawCat = + record + { Object = Category ℓ ℓ' + ; Arrow = Functor + ; 𝟙 = identity + ; _∘_ = _∘f_ + -- What gives here? Why can I not name the variables directly? + -- ; isCategory = record + -- { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H} + -- ; ident = ident-r , ident-l + -- } + } + private + open RawCategory + assoc : IsAssociative RawCat + assoc {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 RawCat identity + ident' = ident-r , ident-l + -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, + -- however, form a groupoid! Therefore there is no (1-)category of + -- categories. There does, however, exist a 2-category of 1-categories. - Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') - Category.raw Cat = RawCat + -- Because of the note above there is not category of categories. + Cat : (unprovable : IsCategory RawCat) → Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') + Category.raw (Cat _) = RawCat + Category.isCategory (Cat unprovable) = unprovable + -- Category.raw Cat _ = RawCat + -- Category.isCategory Cat unprovable = unprovable -module _ {ℓ ℓ' : Level} where +-- The following to some extend depends on the category of categories being a +-- category. In some places it may not actually be needed, however. +module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where module _ (ℂ 𝔻 : Category ℓ ℓ') where private - Catt = Cat ℓ ℓ' + Catt = Cat ℓ ℓ' unprovable :Object: = Object ℂ × Object 𝔻 :Arrow: : :Object: → :Object: → Set ℓ' :Arrow: (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] @@ -131,27 +140,23 @@ module _ {ℓ ℓ' : Level} where RawCategory.Arrow :rawProduct: = :Arrow: RawCategory.𝟙 :rawProduct: = :𝟙: RawCategory._∘_ :rawProduct: = _:⊕:_ + open RawCategory :rawProduct: module C = Category ℂ module D = Category 𝔻 postulate - issSet : {A B : RawCategory.Object :rawProduct:} → isSet (RawCategory.Arrow :rawProduct: A B) + issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B) + ident' : IsIdentity :𝟙: + ident' + = Σ≡ (fst C.ident) (fst D.ident) + , Σ≡ (snd C.ident) (snd D.ident) + postulate univalent : Univalence.Univalent :rawProduct: ident' instance :isCategory: : IsCategory :rawProduct: - -- :isCategory: = record - -- { assoc = Σ≡ C.assoc D.assoc - -- ; ident - -- = Σ≡ (fst C.ident) (fst D.ident) - -- , Σ≡ (snd C.ident) (snd D.ident) - -- ; arrow-is-set = issSet - -- ; univalent = {!!} - -- } IsCategory.assoc :isCategory: = Σ≡ C.assoc D.assoc - IsCategory.ident :isCategory: - = Σ≡ (fst C.ident) (fst D.ident) - , Σ≡ (snd C.ident) (snd D.ident) + IsCategory.ident :isCategory: = ident' IsCategory.arrowIsSet :isCategory: = issSet - IsCategory.univalent :isCategory: = {!!} + IsCategory.univalent :isCategory: = univalent :product: : Category ℓ ℓ' Category.raw :product: = :rawProduct: @@ -209,32 +214,33 @@ module _ {ℓ ℓ' : Level} where uniq = x , isUniq instance - isProduct : IsProduct (Cat ℓ ℓ') proj₁ proj₂ + isProduct : IsProduct Catt proj₁ proj₂ isProduct = uniq - product : Product {ℂ = (Cat ℓ ℓ')} ℂ 𝔻 + product : Product {ℂ = Catt} ℂ 𝔻 product = record { obj = :product: ; proj₁ = proj₁ ; proj₂ = proj₂ } -module _ {ℓ ℓ' : Level} where +module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where + Catt = Cat ℓ ℓ' unprovable instance - hasProducts : HasProducts (Cat ℓ ℓ') - hasProducts = record { product = product } + hasProducts : HasProducts Catt + hasProducts = record { product = product unprovable } -- Basically proves that `Cat ℓ ℓ` is cartesian closed. -module _ (ℓ : Level) where +module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where private open Data.Product open import Cat.Categories.Fun Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ) - Catℓ = Cat ℓ ℓ + Catℓ = Cat ℓ ℓ unprovable module _ (ℂ 𝔻 : Category ℓ ℓ) where private - :obj: : Object (Cat ℓ ℓ) + :obj: : Object Catℓ :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻} :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 @@ -276,7 +282,7 @@ module _ (ℓ : Level) where result : 𝔻 [ func* F A , func* G B ] result = l - _×p_ = product + _×p_ = product unprovable module _ {c : Functor ℂ 𝔻 × Object ℂ} where private @@ -303,109 +309,109 @@ module _ (ℓ : Level) where open module 𝔻 = Category 𝔻 open module F = IsFunctor (F .isFunctor) - module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where - F = F×A .proj₁ - A = F×A .proj₂ - G = G×B .proj₁ - B = G×B .proj₂ - H = H×C .proj₁ - C = H×C .proj₂ - -- Not entirely clear what this is at this point: - _P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {F×A} {G×B} {H×C} - module _ - -- NaturalTransformation F G × ℂ .Arrow A B - {θ×f : NaturalTransformation F G × ℂ [ A , B ]} - {η×g : NaturalTransformation G H × ℂ [ B , C ]} where - private - θ : Transformation F G - θ = proj₁ (proj₁ θ×f) - θNat : Natural F G θ - θNat = proj₂ (proj₁ θ×f) - f : ℂ [ A , B ] - f = proj₂ θ×f - η : Transformation G H - η = proj₁ (proj₁ η×g) - ηNat : Natural G H η - ηNat = proj₂ (proj₁ η×g) - g : ℂ [ B , C ] - g = proj₂ η×g + -- module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where + -- F = F×A .proj₁ + -- A = F×A .proj₂ + -- G = G×B .proj₁ + -- B = G×B .proj₂ + -- H = H×C .proj₁ + -- C = H×C .proj₂ + -- -- Not entirely clear what this is at this point: + -- _P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {F×A} {G×B} {H×C} + -- module _ + -- -- NaturalTransformation F G × ℂ .Arrow A B + -- {θ×f : NaturalTransformation F G × ℂ [ A , B ]} + -- {η×g : NaturalTransformation G H × ℂ [ B , C ]} where + -- private + -- θ : Transformation F G + -- θ = proj₁ (proj₁ θ×f) + -- θNat : Natural F G θ + -- θNat = proj₂ (proj₁ θ×f) + -- f : ℂ [ A , B ] + -- f = proj₂ θ×f + -- η : Transformation G H + -- η = proj₁ (proj₁ η×g) + -- ηNat : Natural G H η + -- ηNat = proj₂ (proj₁ η×g) + -- g : ℂ [ B , C ] + -- g = proj₂ η×g - ηθNT : NaturalTransformation F H - ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat) + -- ηθNT : NaturalTransformation F H + -- ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat) - ηθ = proj₁ ηθNT - ηθNat = proj₂ ηθNT + -- ηθ = proj₁ ηθNT + -- ηθNat = proj₂ ηθNT - :distrib: : - 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] - ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] - :distrib: = begin - 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] - ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ - 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] - ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ - 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] - ≡⟨ sym assoc ⟩ - 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) assoc ⟩ - 𝔻 [ 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) ⟩ - 𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ] - ≡⟨ assoc ⟩ - 𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩ - 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩ - 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎ - where - open Category 𝔻 - module H = IsFunctor (H .isFunctor) + -- :distrib: : + -- 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] + -- ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] + -- :distrib: = begin + -- 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] + -- ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ + -- 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] + -- ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ + -- 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] + -- ≡⟨ sym assoc ⟩ + -- 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] + -- ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) assoc ⟩ + -- 𝔻 [ 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) ⟩ + -- 𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ] + -- ≡⟨ assoc ⟩ + -- 𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] + -- ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩ + -- 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] + -- ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩ + -- 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎ + -- where + -- open Category 𝔻 + -- module H = IsFunctor (H .isFunctor) - :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 - :eval: = record - { raw = record - { func* = :func*: - ; func→ = λ {dom} {cod} → :func→: {dom} {cod} - } - ; isFunctor = record - { ident = λ {o} → :ident: {o} - ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} - } - } + -- :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 + -- :eval: = record + -- { raw = record + -- { func* = :func*: + -- ; func→ = λ {dom} {cod} → :func→: {dom} {cod} + -- } + -- ; isFunctor = record + -- { ident = λ {o} → :ident: {o} + -- ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} + -- } + -- } - module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where - open HasProducts (hasProducts {ℓ} {ℓ}) renaming (_|×|_ to parallelProduct) + -- module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where + -- open HasProducts (hasProducts {ℓ} {ℓ}) renaming (_|×|_ to parallelProduct) - postulate - transpose : Functor 𝔸 :obj: - eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F - -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F - -- eq' : (Catℓ [ :eval: ∘ - -- (record { product = product } HasProducts.|×| transpose) - -- (𝟙 Catℓ) - -- ]) - -- ≡ F + -- postulate + -- transpose : Functor 𝔸 :obj: + -- eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F + -- -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F + -- -- eq' : (Catℓ [ :eval: ∘ + -- -- (record { product = product } HasProducts.|×| transpose) + -- -- (𝟙 Catℓ) + -- -- ]) + -- -- ≡ F - -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758` - -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [ - -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose = - -- transpose , eq + -- -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758` + -- -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [ + -- -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose = + -- -- transpose , eq - :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: - :isExponential: = {!catTranspose!} - where - open HasProducts (hasProducts {ℓ} {ℓ}) using (_|×|_) - -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F + -- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: + -- :isExponential: = {!catTranspose!} + -- where + -- open HasProducts (hasProducts {ℓ} {ℓ}) using (_|×|_) + -- -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F - -- :exponent: : Exponential (Cat ℓ ℓ) A B - :exponent: : Exponential Catℓ ℂ 𝔻 - :exponent: = record - { obj = :obj: - ; eval = :eval: - ; isExponential = :isExponential: - } + -- -- :exponent: : Exponential (Cat ℓ ℓ) A B + -- :exponent: : Exponential Catℓ ℂ 𝔻 + -- :exponent: = record + -- { obj = :obj: + -- ; eval = :eval: + -- ; isExponential = :isExponential: + -- } - hasExponentials : HasExponentials (Cat ℓ ℓ) - hasExponentials = record { exponent = :exponent: } + -- hasExponentials : HasExponentials (Cat ℓ ℓ) + -- hasExponentials = record { exponent = :exponent: } From cc1ddaac9f3cadbcc5f86e9a969d23de7664cdb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 10:35:42 +0100 Subject: [PATCH 03/20] Add new type-synonym --- src/Cat/Category.agda | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 686ae76..536f0b7 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -49,6 +49,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where IsIdentity id = {A B : Object} {f : Arrow A B} → f ∘ id ≡ f × id ∘ f ≡ f + ArrowsAreSets : Set (ℓa ⊔ ℓb) + ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B) + IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙 @@ -100,7 +103,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc field assoc : IsAssociative ident : IsIdentity 𝟙 - arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B) + arrowIsSet : ArrowsAreSets univalent : Univalent ident -- `IsCategory` is a mere proposition. @@ -162,8 +165,13 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ] ident = propIsIdentity x X.ident Y.ident done : x ≡ y - U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univalent a) → Set _ - U eqwal bbb = (λ i → Univalent (eqwal i)) [ X.univalent ≡ bbb ] + U : ∀ {a : IsIdentity 𝟙} + → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] + → (b : Univalent a) + → Set _ + U eqwal bbb = + (λ i → Univalent (eqwal i)) + [ X.univalent ≡ bbb ] P : (y : IsIdentity 𝟙) → (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _ P y eq = ∀ (b' : Univalent y) → U eq b' From 3032dc61303522e9bbe2561be96e5081dd8af68c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 10:36:59 +0100 Subject: [PATCH 04/20] Make explicit argument --- src/Cat/Category/Functor.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 484cfdc..b9e72b4 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -50,7 +50,7 @@ open Functor module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} - {F : RawFunctor ℂ 𝔻} + (F : RawFunctor ℂ 𝔻) where private module 𝔻 = IsCategory (isCategory 𝔻) @@ -77,7 +77,7 @@ module _ IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i) IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻} - (\ F → propIsFunctor {F = F}) (\ i → F i) + (\ F → propIsFunctor F) (\ i → F i) where open import Cubical.NType.Properties using (lemPropF) From 9a4d79fa4eb369aeb3ee5f9ec7017d309fe1ef07 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 10:44:23 +0100 Subject: [PATCH 05/20] Readd commented code --- src/Cat/Categories/Cat.agda | 193 ++++++++++++++++++------------------ 1 file changed, 97 insertions(+), 96 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index e31221c..2d58cf1 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -309,109 +309,110 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where open module 𝔻 = Category 𝔻 open module F = IsFunctor (F .isFunctor) - -- module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where - -- F = F×A .proj₁ - -- A = F×A .proj₂ - -- G = G×B .proj₁ - -- B = G×B .proj₂ - -- H = H×C .proj₁ - -- C = H×C .proj₂ - -- -- Not entirely clear what this is at this point: - -- _P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {F×A} {G×B} {H×C} - -- module _ - -- -- NaturalTransformation F G × ℂ .Arrow A B - -- {θ×f : NaturalTransformation F G × ℂ [ A , B ]} - -- {η×g : NaturalTransformation G H × ℂ [ B , C ]} where - -- private - -- θ : Transformation F G - -- θ = proj₁ (proj₁ θ×f) - -- θNat : Natural F G θ - -- θNat = proj₂ (proj₁ θ×f) - -- f : ℂ [ A , B ] - -- f = proj₂ θ×f - -- η : Transformation G H - -- η = proj₁ (proj₁ η×g) - -- ηNat : Natural G H η - -- ηNat = proj₂ (proj₁ η×g) - -- g : ℂ [ B , C ] - -- g = proj₂ η×g + module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where + F = F×A .proj₁ + A = F×A .proj₂ + G = G×B .proj₁ + B = G×B .proj₂ + H = H×C .proj₁ + C = H×C .proj₂ + -- Not entirely clear what this is at this point: + _P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {F×A} {G×B} {H×C} + module _ + -- NaturalTransformation F G × ℂ .Arrow A B + {θ×f : NaturalTransformation F G × ℂ [ A , B ]} + {η×g : NaturalTransformation G H × ℂ [ B , C ]} where + private + θ : Transformation F G + θ = proj₁ (proj₁ θ×f) + θNat : Natural F G θ + θNat = proj₂ (proj₁ θ×f) + f : ℂ [ A , B ] + f = proj₂ θ×f + η : Transformation G H + η = proj₁ (proj₁ η×g) + ηNat : Natural G H η + ηNat = proj₂ (proj₁ η×g) + g : ℂ [ B , C ] + g = proj₂ η×g - -- ηθNT : NaturalTransformation F H - -- ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat) + ηθNT : NaturalTransformation F H + ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat) - -- ηθ = proj₁ ηθNT - -- ηθNat = proj₂ ηθNT + ηθ = proj₁ ηθNT + ηθNat = proj₂ ηθNT - -- :distrib: : - -- 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] - -- ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] - -- :distrib: = begin - -- 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] - -- ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ - -- 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] - -- ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ - -- 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] - -- ≡⟨ sym assoc ⟩ - -- 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] - -- ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) assoc ⟩ - -- 𝔻 [ 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) ⟩ - -- 𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ] - -- ≡⟨ assoc ⟩ - -- 𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] - -- ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩ - -- 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] - -- ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩ - -- 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎ - -- where - -- open Category 𝔻 - -- module H = IsFunctor (H .isFunctor) + :distrib: : + 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] + ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] + :distrib: = begin + 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] + ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ + 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] + ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ + 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] + ≡⟨ sym assoc ⟩ + 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) assoc ⟩ + 𝔻 [ 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) ⟩ + 𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ] + ≡⟨ assoc ⟩ + 𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩ + 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩ + 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎ + where + open Category 𝔻 + module H = IsFunctor (H .isFunctor) - -- :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 - -- :eval: = record - -- { raw = record - -- { func* = :func*: - -- ; func→ = λ {dom} {cod} → :func→: {dom} {cod} - -- } - -- ; isFunctor = record - -- { ident = λ {o} → :ident: {o} - -- ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} - -- } - -- } + :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 + :eval: = record + { raw = record + { func* = :func*: + ; func→ = λ {dom} {cod} → :func→: {dom} {cod} + } + ; isFunctor = record + { ident = λ {o} → :ident: {o} + ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} + } + } - -- module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where - -- open HasProducts (hasProducts {ℓ} {ℓ}) renaming (_|×|_ to parallelProduct) + module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where + open HasProducts (hasProducts {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct) - -- postulate - -- transpose : Functor 𝔸 :obj: - -- eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F - -- -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F - -- -- eq' : (Catℓ [ :eval: ∘ - -- -- (record { product = product } HasProducts.|×| transpose) - -- -- (𝟙 Catℓ) - -- -- ]) - -- -- ≡ F + postulate + transpose : Functor 𝔸 :obj: + eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F + -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F + -- eq' : (Catℓ [ :eval: ∘ + -- (record { product = product } HasProducts.|×| transpose) + -- (𝟙 Catℓ) + -- ]) + -- ≡ F - -- -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758` - -- -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [ - -- -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose = - -- -- transpose , eq + -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758` + -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [ + -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose = + -- transpose , eq - -- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: - -- :isExponential: = {!catTranspose!} - -- where - -- open HasProducts (hasProducts {ℓ} {ℓ}) using (_|×|_) - -- -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F + postulate :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: + -- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: + -- :isExponential: = {!catTranspose!} + -- where + -- open HasProducts (hasProducts {ℓ} {ℓ} unprovable) using (_|×|_) + -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F - -- -- :exponent: : Exponential (Cat ℓ ℓ) A B - -- :exponent: : Exponential Catℓ ℂ 𝔻 - -- :exponent: = record - -- { obj = :obj: - -- ; eval = :eval: - -- ; isExponential = :isExponential: - -- } + -- :exponent: : Exponential (Cat ℓ ℓ) A B + :exponent: : Exponential Catℓ ℂ 𝔻 + :exponent: = record + { obj = :obj: + ; eval = :eval: + ; isExponential = :isExponential: + } - -- hasExponentials : HasExponentials (Cat ℓ ℓ) - -- hasExponentials = record { exponent = :exponent: } + hasExponentials : HasExponentials Catℓ + hasExponentials = record { exponent = :exponent: } From bc2129b8fc05ca85a5b5f41b230f7e28fe483d90 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 10:53:11 +0100 Subject: [PATCH 06/20] Readd yoneda embedding --- src/Cat/Category/Exponential.agda | 1 + src/Cat/Category/Properties.agda | 135 ++++++++++++++---------------- 2 files changed, 64 insertions(+), 72 deletions(-) diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda index 137e501..1e443ce 100644 --- a/src/Cat/Category/Exponential.agda +++ b/src/Cat/Category/Exponential.agda @@ -35,5 +35,6 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} transpose A f = proj₁ (isExponential A f) record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where + open Exponential public field exponent : (A B : Object ℂ) → Exponential ℂ A B diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index b001344..a1860dc 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -41,82 +41,73 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso -{- -epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f) -epi-mono-is-not-iso f = - let k = f {!!} {!!} {!!} {!!} - in {!!} --} +-- TODO: We want to avoid defining the yoneda embedding going through the +-- category of categories (since it doesn't exist). +open import Cat.Categories.Cat using (RawCat) -open import Cat.Category -open Category -open Functor +module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat ℓ ℓ)) where + open import Cat.Categories.Fun + open import Cat.Categories.Sets + module Cat = Cat.Categories.Cat + open import Cat.Category.Exponential + open Functor + 𝓢 = Sets ℓ + private + Catℓ : Category _ _ + Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable} + prshf = presheaf {ℂ = ℂ} + module ℂ = Category ℂ --- module _ {ℓ : Level} {ℂ : Category ℓ ℓ} --- {isSObj : isSet (ℂ .Object)} --- {isz2 : ∀ {ℓ} → {A B : Set ℓ} → isSet (Sets [ A , B ])} where --- -- open import Cat.Categories.Cat using (Cat) --- open import Cat.Categories.Fun --- open import Cat.Categories.Sets --- -- module Cat = Cat.Categories.Cat --- open import Cat.Category.Exponential --- private --- Catℓ = Cat ℓ ℓ --- prshf = presheaf {ℂ = ℂ} --- module ℂ = IsCategory (ℂ .isCategory) + _⇑_ : (A B : Category.Object Catℓ) → Category.Object Catℓ + A ⇑ B = (exponent A B) .obj + where + open HasExponentials (Cat.hasExponentials ℓ unprovable) --- -- Exp : Set (lsuc (lsuc ℓ)) --- -- Exp = Exponential (Cat (lsuc ℓ) ℓ) --- -- Sets (Opposite ℂ) + module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where + :func→: : NaturalTransformation (prshf A) (prshf B) + :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc --- _⇑_ : (A B : Catℓ .Object) → Catℓ .Object --- A ⇑ B = (exponent A B) .obj --- where --- open HasExponentials (Cat.hasExponentials ℓ) + module _ {c : Category.Object ℂ} where + eqTrans : (λ _ → Transformation (prshf c) (prshf c)) + [ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ] + eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂ --- module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where --- :func→: : NaturalTransformation (prshf A) (prshf B) --- :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc + eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i)) + [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)] + eqNat = λ i {A} {B} f → + let + open Category 𝓢 + lemm : (𝓢 [ eqTrans i B ∘ func→ (prshf c) f ]) ≡ + (𝓢 [ func→ (prshf c) f ∘ eqTrans i A ]) + lemm = {!!} + lem : (λ _ → 𝓢 [ Functor.func* (prshf c) A , func* (prshf c) B ]) + [ 𝓢 [ eqTrans i B ∘ func→ (prshf c) f ] + ≡ 𝓢 [ func→ (prshf c) f ∘ eqTrans i A ] ] + lem + = arrowIsSet _ _ lemm _ i + -- (Sets [ eqTrans i B ∘ prshf c .func→ f ]) + -- (Sets [ prshf c .func→ f ∘ eqTrans i A ]) + -- lemm + -- _ i + in + lem + -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] → + -- let + -- k : ℂ [ {!!} , {!!} ] + -- k = ℂ[A,c] + -- in {!ℂ [ ? ∘ ? ]!} --- module _ {c : ℂ .Object} where --- eqTrans : (λ _ → Transformation (prshf c) (prshf c)) --- [ (λ _ x → ℂ [ ℂ .𝟙 ∘ x ]) ≡ identityTrans (prshf c) ] --- eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂ + :ident: : (:func→: (ℂ.𝟙 {c})) ≡ (Category.𝟙 Fun {A = prshf c}) + :ident: = Σ≡ eqTrans eqNat --- eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i)) --- [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)] --- eqNat = λ i {A} {B} f → --- let --- open IsCategory (Sets .isCategory) --- lemm : (Sets [ eqTrans i B ∘ prshf c .func→ f ]) ≡ --- (Sets [ prshf c .func→ f ∘ eqTrans i A ]) --- lemm = {!!} --- lem : (λ _ → Sets [ Functor.func* (prshf c) A , prshf c .func* B ]) --- [ Sets [ eqTrans i B ∘ prshf c .func→ f ] --- ≡ Sets [ prshf c .func→ f ∘ eqTrans i A ] ] --- lem --- = isz2 _ _ lemm _ i --- -- (Sets [ eqTrans i B ∘ prshf c .func→ f ]) --- -- (Sets [ prshf c .func→ f ∘ eqTrans i A ]) --- -- lemm --- -- _ i --- in --- lem --- -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] → --- -- let --- -- k : ℂ [ {!!} , {!!} ] --- -- k = ℂ[A,c] --- -- in {!ℂ [ ? ∘ ? ]!} - --- :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c}) --- :ident: = Σ≡ eqTrans eqNat - --- yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}}) --- yoneda = record --- { func* = prshf --- ; func→ = :func→: --- ; isFunctor = record --- { ident = :ident: --- ; distrib = {!!} --- } --- } + yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢}) + yoneda = record + { raw = record + { func* = prshf + ; func→ = :func→: + } + ; isFunctor = record + { ident = :ident: + ; distrib = {!!} + } + } From 954a89f8d13167be0712121e37e12ddc18a90bc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 11:12:27 +0100 Subject: [PATCH 07/20] Expose `naturalIsProp` --- src/Cat/Categories/Fun.agda | 94 +++++++++++++++++-------------------- 1 file changed, 44 insertions(+), 50 deletions(-) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index ba492d0..b5a33c8 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -38,9 +38,6 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat → (f : ℂ [ A , B ]) → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ] - -- naturalIsProp : ∀ θ → isProp (Natural θ) - -- naturalIsProp θ x y = {!funExt!} - NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') NaturalTransformation = Σ Transformation Natural @@ -100,59 +97,56 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat NatComp = _:⊕:_ private - module _ {F G : Functor ℂ 𝔻} where - module 𝔻 = Category 𝔻 + module 𝔻 = Category 𝔻 - transformationIsSet : isSet (Transformation F G) - transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C) (λ l → q l C) i j - IsSet' : {ℓ : Level} (A : Set ℓ) → Set ℓ - IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q + 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 - 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 + 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 - naturalTransformationIsSets : isSet (NaturalTransformation F G) - naturalTransformationIsSets = sigPresSet transformationIsSet - λ θ → ntypeCommulative - (s≤s {n = Nat.suc Nat.zero} z≤n) - (naturalIsProp θ) + naturalTransformationIsSets : isSet (NaturalTransformation F G) + naturalTransformationIsSets = sigPresSet transformationIsSet + λ θ → ntypeCommulative + (s≤s {n = Nat.suc Nat.zero} z≤n) + (naturalIsProp θ) - module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B} - {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where - private - θ = proj₁ θ' - η = proj₁ η' - ζ = proj₁ ζ' - θNat = proj₂ θ' - ηNat = proj₂ η' - ζNat = proj₂ ζ' - L : NaturalTransformation A D - L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) - R : NaturalTransformation A D - 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)) - where - open Category 𝔻 + module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B} + {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where + private + θ = proj₁ θ' + η = proj₁ η' + ζ = proj₁ ζ' + θNat = proj₂ θ' + ηNat = proj₂ η' + ζNat = proj₂ ζ' + L : NaturalTransformation A D + L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) + R : NaturalTransformation A D + 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)) + where + open Category 𝔻 + private module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where - private - allNatural = naturalIsProp {F = A} {B} - f' = proj₁ f - module 𝔻Data = Category 𝔻 - eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C - eq-r C = begin - 𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩ - 𝔻 [ f' C ∘ 𝔻Data.𝟙 ] ≡⟨ proj₁ (𝔻.ident {A} {B}) ⟩ - f' C ∎ - eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C - eq-l C = proj₂ (𝔻.ident {A} {B}) + allNatural = naturalIsProp {F = A} {B} + f' = proj₁ f + 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 ∎ + eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C + eq-l C = proj₂ 𝔻.ident 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 From de1d19c442581fe60ef833c371f515431af664e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 11:23:21 +0100 Subject: [PATCH 08/20] Readd stuff about the yoneda embedding --- src/Cat/Category/Properties.agda | 34 +++++++------------------------- 1 file changed, 7 insertions(+), 27 deletions(-) diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index a1860dc..f8b60f8 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -72,33 +72,13 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat [ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ] eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂ - eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i)) - [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)] - eqNat = λ i {A} {B} f → - let - open Category 𝓢 - lemm : (𝓢 [ eqTrans i B ∘ func→ (prshf c) f ]) ≡ - (𝓢 [ func→ (prshf c) f ∘ eqTrans i A ]) - lemm = {!!} - lem : (λ _ → 𝓢 [ Functor.func* (prshf c) A , func* (prshf c) B ]) - [ 𝓢 [ eqTrans i B ∘ func→ (prshf c) f ] - ≡ 𝓢 [ func→ (prshf c) f ∘ eqTrans i A ] ] - lem - = arrowIsSet _ _ lemm _ i - -- (Sets [ eqTrans i B ∘ prshf c .func→ f ]) - -- (Sets [ prshf c .func→ f ∘ eqTrans i A ]) - -- lemm - -- _ i - in - lem - -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] → - -- let - -- k : ℂ [ {!!} , {!!} ] - -- k = ℂ[A,c] - -- in {!ℂ [ ? ∘ ? ]!} - - :ident: : (:func→: (ℂ.𝟙 {c})) ≡ (Category.𝟙 Fun {A = prshf c}) - :ident: = Σ≡ eqTrans eqNat + open import Cubical.NType.Properties + open import Cat.Categories.Fun + :ident: : :func→: (ℂ.𝟙 {c}) ≡ Category.𝟙 Fun {A = prshf c} + :ident: = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq + where + eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) + eq = funExt λ A → funExt λ B → proj₂ ℂ.ident yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢}) yoneda = record From 3f3247c8703e1bad45c42cbc5e99456322f02790 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:05:38 +0100 Subject: [PATCH 09/20] Remove commented code --- src/Cat/Categories/Free.agda | 8 -------- src/Cat/Equality.agda | 25 ------------------------- 2 files changed, 33 deletions(-) diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 326152a..19cabeb 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -9,14 +9,6 @@ open import Cat.Category open IsCategory --- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where --- emptyPath : {a : A} → Path a a --- concatenate : {a b c : A} → Path a b → Path b c → Path a b - --- import Data.List --- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ') --- P = {!Data.List.List ?!} --- Generalized paths: data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where empty : {a : A} → Path R a a cons : {a b c : A} → R b c → Path R a b → Path R a c diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda index c3c333d..d6b3dc0 100644 --- a/src/Cat/Equality.agda +++ b/src/Cat/Equality.agda @@ -20,28 +20,3 @@ module Equality where Σ≡ : a ≡ b proj₁ (Σ≡ i) = proj₁≡ i proj₂ (Σ≡ i) = proj₂≡ i - - -- Remark 2.7.1: This theorem: - -- - -- (x , u) ≡ (x , v) → u ≡ v - -- - -- does *not* hold! We can only conclude that there *exists* `p : x ≡ x` - -- such that - -- - -- p* u ≡ v - -- thm : isSet A → (∀ {a} → isSet (B a)) → isSet (Σ A B) - -- thm sA sB (x , y) (x' , y') p q = res - -- where - -- x≡x'0 : x ≡ x' - -- x≡x'0 = λ i → proj₁ (p i) - -- x≡x'1 : x ≡ x' - -- x≡x'1 = λ i → proj₁ (q i) - -- someP : x ≡ x' - -- someP = {!!} - -- tricky : {!y!} ≡ y' - -- tricky = {!!} - -- -- res' : (λ _ → Σ A B) [ (x , y) ≡ (x' , y') ] - -- res' : ({!!} , {!!}) ≡ ({!!} , {!!}) - -- res' = {!!} - -- res : p ≡ q - -- res i = {!res'!} From 885fd8fa69c006347e7b2d249846867275343084 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:15:16 +0100 Subject: [PATCH 10/20] Drastically simplify proofs --- src/Cat/Categories/Cat.agda | 75 +++++-------------------------------- 1 file changed, 9 insertions(+), 66 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 2d58cf1..4d6054c 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -24,67 +24,15 @@ open Category using (Object ; 𝟙) module _ (ℓ ℓ' : Level) where private module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where - private - eq* : func* (H ∘f (G ∘f F)) ≡ func* ((H ∘f G) ∘f F) - eq* = refl - eq→ : PathP - (λ i → {A B : Object 𝔸} → 𝔸 [ A , B ] → 𝔻 [ eq* i A , eq* i B ]) - (func→ (H ∘f (G ∘f F))) (func→ ((H ∘f G) ∘f F)) - eq→ = refl - postulate - eqI - : (λ i → ∀ {A : Object 𝔸} → eq→ i (𝟙 𝔸 {A}) ≡ 𝟙 𝔻 {eq* i A}) - [ (H ∘f (G ∘f F)) .isFunctor .ident - ≡ ((H ∘f G) ∘f F) .isFunctor .ident - ] - eqD - : (λ i → ∀ {A B C} {f : 𝔸 [ A , B ]} {g : 𝔸 [ B , C ]} - → eq→ i (𝔸 [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ]) - [ (H ∘f (G ∘f F)) .isFunctor .distrib - ≡ ((H ∘f G) ∘f F) .isFunctor .distrib - ] - assc : H ∘f (G ∘f F) ≡ (H ∘f G) ∘f F - assc = Functor≡ eq* eq→ + assc = Functor≡ refl refl module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where - module _ where - private - eq* : (func* F) ∘ (func* (identity {C = ℂ})) ≡ func* F - eq* = refl - -- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f - eq→ : PathP - (λ i → - {x y : Object ℂ} → ℂ [ x , y ] → 𝔻 [ func* F x , func* F y ]) - (func→ (F ∘f identity)) (func→ F) - eq→ = refl - postulate - eqI-r - : (λ i → {c : Object ℂ} → (λ _ → 𝔻 [ func* F c , func* F c ]) - [ func→ F (𝟙 ℂ) ≡ 𝟙 𝔻 ]) - [(F ∘f identity) .isFunctor .ident ≡ F .isFunctor .ident ] - eqD-r : PathP - (λ i → - {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} → - eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ]) - ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib) - ident-r : F ∘f identity ≡ F - ident-r = Functor≡ eq* eq→ - module _ where - private - postulate - eq* : func* (identity ∘f F) ≡ func* F - eq→ : PathP - (λ i → {x y : Object ℂ} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ]) - (func→ (identity ∘f F)) (func→ F) - eqI : (λ i → ∀ {A : Object ℂ} → eq→ i (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {eq* i A}) - [ ((identity ∘f F) .isFunctor .ident) ≡ (F .isFunctor .ident) ] - eqD : PathP (λ i → {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} - → eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ]) - ((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib) - -- (λ z → eq* i z) (eq→ i) - ident-l : identity ∘f F ≡ F - ident-l = Functor≡ eq* eq→ + ident-r : F ∘f identity ≡ F + ident-r = Functor≡ refl refl + + ident-l : identity ∘f F ≡ F + ident-l = Functor≡ refl refl RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') RawCat = @@ -93,18 +41,13 @@ module _ (ℓ ℓ' : Level) where ; Arrow = Functor ; 𝟙 = identity ; _∘_ = _∘f_ - -- What gives here? Why can I not name the variables directly? - -- ; isCategory = record - -- { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H} - -- ; ident = ident-r , ident-l - -- } } private - open RawCategory - assoc : IsAssociative RawCat + open RawCategory RawCat + assoc : IsAssociative assoc {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 RawCat identity + ident' : IsIdentity identity ident' = ident-r , ident-l -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- however, form a groupoid! Therefore there is no (1-)category of From e46edf1f6867d0835adfbf7cfe1e57465b41e0fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:21:16 +0100 Subject: [PATCH 11/20] Chain reexport things in Functor --- src/Cat/Category/Functor.agda | 20 ++++++-------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index b9e72b4..09d7731 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -24,7 +24,7 @@ module _ {ℓc ℓc' ℓd ℓd'} func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ] record IsFunctor (F : RawFunctor) : 𝓤 where - open RawFunctor F + open RawFunctor F public field ident : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c} distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} @@ -35,16 +35,8 @@ module _ {ℓc ℓc' ℓd ℓd'} raw : RawFunctor {{isFunctor}} : IsFunctor raw - private - module R = RawFunctor raw + open IsFunctor isFunctor public - func* : Object ℂ → Object 𝔻 - func* = R.func* - - func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ] - func→ = R.func→ - -open IsFunctor open Functor module _ @@ -108,8 +100,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] dist = begin (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩ - F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (G .isFunctor .distrib)⟩ - F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ F .isFunctor .distrib ⟩ + F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (distrib G) ⟩ + F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ distrib F ⟩ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎ _∘fr_ : RawFunctor A C @@ -120,8 +112,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F isFunctor' = record { ident = begin (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩ - F→ (G→ (𝟙 A)) ≡⟨ cong F→ (G .isFunctor .ident)⟩ - F→ (𝟙 B) ≡⟨ F .isFunctor .ident ⟩ + F→ (G→ (𝟙 A)) ≡⟨ cong F→ (ident G)⟩ + F→ (𝟙 B) ≡⟨ ident F ⟩ 𝟙 C ∎ ; distrib = dist } From 34dec9406d9ed310289431a63d4abc017c74b442 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:29:10 +0100 Subject: [PATCH 12/20] Do not mention `IsFunctor` outside the module that defines it --- src/Cat/Categories/Cat.agda | 59 ++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 33 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 4d6054c..6623936 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -17,7 +17,6 @@ open import Cat.Equality open Equality.Data.Product open Functor -open IsFunctor open Category using (Object ; 𝟙) -- The category of categories @@ -117,38 +116,32 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where } module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where - open Functor + x : Functor X :product: + x = record + { raw = record + { func* = λ x → x₁ .func* x , x₂ .func* x + ; func→ = λ x → func→ x₁ x , func→ x₂ x + } + ; isFunctor = record + { ident = Σ≡ x₁.ident x₂.ident + ; distrib = Σ≡ x₁.distrib x₂.distrib + } + } + where + open module x₁ = Functor x₁ + open module x₂ = Functor x₂ - postulate x : Functor X :product: - -- x = record - -- { func* = λ x → x₁ .func* x , x₂ .func* x - -- ; func→ = λ x → func→ x₁ x , func→ x₂ x - -- ; isFunctor = record - -- { ident = Σ≡ x₁.ident x₂.ident - -- ; distrib = Σ≡ x₁.distrib x₂.distrib - -- } - -- } - -- where - -- open module x₁ = IsFunctor (x₁ .isFunctor) - -- open module x₂ = IsFunctor (x₂ .isFunctor) + isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁ + isUniqL = Functor≡ eq* eq→ + where + eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func* + eq* = refl + eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → ℂ [ eq* i A , eq* i B ]) + [ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ] + eq→ = refl - -- Turned into postulate after: - -- > commit e8215b2c051062c6301abc9b3f6ec67106259758 (HEAD -> dev, github/dev) - -- > Author: Frederik Hanghøj Iversen - -- > Date: Mon Feb 5 14:59:53 2018 +0100 - postulate isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁ - -- isUniqL = Functor≡ eq* eq→ {!!} - -- where - -- eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func* - -- eq* = {!refl!} - -- eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → ℂ [ eq* i A , eq* i B ]) - -- [ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ] - -- eq→ = refl - -- postulate eqIsF : (Catt [ proj₁ ∘ x ]) .isFunctor ≡ x₁ .isFunctor - -- eqIsF = IsFunctor≡ {!refl!} {!!} - - postulate isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂ - -- isUniqR = Functor≡ refl refl {!!} {!!} + isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂ + isUniqR = Functor≡ refl refl isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂ isUniq = isUniqL , isUniqR @@ -250,7 +243,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where 𝟙 𝔻 ∎ where open module 𝔻 = Category 𝔻 - open module F = IsFunctor (F .isFunctor) + open module F = Functor F module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where F = F×A .proj₁ @@ -310,7 +303,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎ where open Category 𝔻 - module H = IsFunctor (H .isFunctor) + module H = Functor H :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 :eval: = record From a57f45d93f53b672ca61b34c7657e705831576d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:33:20 +0100 Subject: [PATCH 13/20] Remove yet another postulate --- src/Cat/Categories/Cat.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 6623936..02f4838 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -86,8 +86,9 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where module C = Category ℂ module D = Category 𝔻 - postulate - issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B) + open import Cubical.Sigma + issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B) + issSet = setSig {sA = C.arrowIsSet} {sB = λ x → D.arrowIsSet} ident' : IsIdentity :𝟙: ident' = Σ≡ (fst C.ident) (fst D.ident) From 852056cc4468ca4aa4d22cf08b8f55b7ed16d7a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:41:15 +0100 Subject: [PATCH 14/20] Add type-synonyms in functor --- src/Cat/Categories/Cat.agda | 2 +- src/Cat/Category/Functor.agda | 14 ++++++++++---- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 02f4838..08516cf 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -16,7 +16,7 @@ open import Cat.Category.Exponential open import Cat.Equality open Equality.Data.Product -open Functor +open Functor using (func→ ; func*) open Category using (Object ; 𝟙) -- The category of categories diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 09d7731..aac423c 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -7,7 +7,7 @@ open import Function open import Cat.Category -open Category hiding (_∘_ ; raw) +open Category hiding (_∘_ ; raw ; IsIdentity) module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') @@ -23,12 +23,18 @@ module _ {ℓc ℓc' ℓd ℓd'} func* : Object ℂ → Object 𝔻 func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ] + IsIdentity : Set _ + IsIdentity = {A : Object ℂ} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A} + + IsDistributive : Set _ + IsDistributive = {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} + → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ] + record IsFunctor (F : RawFunctor) : 𝓤 where open RawFunctor F public field - ident : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c} - distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} - → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ] + ident : IsIdentity + distrib : IsDistributive record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where field 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 15/20] 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)) From 6446435a49a738e470998a7ed50e56224cd2d517 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:49:41 +0100 Subject: [PATCH 16/20] Rename `ident` to `isIdentity` --- src/Cat/Categories/Cat.agda | 20 +++++++++--------- src/Cat/Categories/Fam.agda | 6 +++--- src/Cat/Categories/Free.agda | 2 +- src/Cat/Categories/Fun.agda | 10 ++++----- src/Cat/Categories/Rel.agda | 2 +- src/Cat/Categories/Sets.agda | 8 +++---- src/Cat/Category.agda | 36 ++++++++++++++++---------------- src/Cat/Category/Functor.agda | 12 +++++------ src/Cat/Category/Properties.agda | 14 ++++++------- 9 files changed, 55 insertions(+), 55 deletions(-) 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 = {!!} } } 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 17/20] 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 From 7787a8f0be55e3fbf50036251e7fcc83944c6d62 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:52:14 +0100 Subject: [PATCH 18/20] Indentation --- src/Cat/Category.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 6c3172e..cec311d 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -102,9 +102,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc open Univalence ℂ public field isAssociative : IsAssociative - isIdentity : IsIdentity 𝟙 + isIdentity : IsIdentity 𝟙 arrowsAreSets : ArrowsAreSets - univalent : Univalent isIdentity + univalent : Univalent isIdentity -- `IsCategory` is a mere proposition. module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where From 4874ed0795559026fdf5cc6a781f8ea4916ec077 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:53:35 +0100 Subject: [PATCH 19/20] Rename `distrib` to `isDistributive` --- src/Cat/Categories/Cat.agda | 14 +++++++------- src/Cat/Categories/Sets.agda | 4 ++-- src/Cat/Category/Functor.agda | 14 +++++++------- src/Cat/Category/Properties.agda | 2 +- 4 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index b1a1bfb..b7e306e 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -107,13 +107,13 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where proj₁ : Catt [ :product: , ℂ ] proj₁ = record { raw = record { func* = fst ; func→ = fst } - ; isFunctor = record { isIdentity = refl ; distrib = refl } + ; isFunctor = record { isIdentity = refl ; isDistributive = refl } } proj₂ : Catt [ :product: , 𝔻 ] proj₂ = record { raw = record { func* = snd ; func→ = snd } - ; isFunctor = record { isIdentity = refl ; distrib = refl } + ; isFunctor = record { isIdentity = refl ; isDistributive = refl } } module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where @@ -125,7 +125,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where } ; isFunctor = record { isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity - ; distrib = Σ≡ x₁.distrib x₂.distrib + ; isDistributive = Σ≡ x₁.isDistributive x₂.isDistributive } } where @@ -279,14 +279,14 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where ηθ = proj₁ ηθNT ηθNat = proj₂ ηθNT - :distrib: : + :isDistributive: : 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] - :distrib: = begin + :isDistributive: = begin 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] - ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ + ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩ 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] ≡⟨ sym isAssociative ⟩ 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] @@ -314,7 +314,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where } ; isFunctor = record { isIdentity = λ {o} → :ident: {o} - ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} + ; isDistributive = λ {f u n k y} → :isDistributive: {f} {u} {n} {k} {y} } } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index f9e26e0..bc0fd81 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -99,7 +99,7 @@ module _ {ℓa ℓb : Level} where } ; isFunctor = record { isIdentity = funExt λ _ → proj₂ isIdentity - ; distrib = funExt λ x → sym isAssociative + ; isDistributive = funExt λ x → sym isAssociative } } where @@ -114,7 +114,7 @@ module _ {ℓa ℓb : Level} where } ; isFunctor = record { isIdentity = funExt λ x → proj₁ isIdentity - ; distrib = funExt λ x → isAssociative + ; isDistributive = funExt λ x → isAssociative } } where diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index ee643ce..0269df9 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -33,8 +33,8 @@ module _ {ℓc ℓc' ℓd ℓd'} record IsFunctor (F : RawFunctor) : 𝓤 where open RawFunctor F public field - isIdentity : IsIdentity - distrib : IsDistributive + isIdentity : IsIdentity + isDistributive : IsDistributive record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where field @@ -56,7 +56,7 @@ module _ propIsFunctor : isProp (IsFunctor _ _ F) propIsFunctor isF0 isF1 i = record { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i - ; distrib = 𝔻.arrowsAreSets _ _ isF0.distrib isF1.distrib i + ; isDistributive = 𝔻.arrowsAreSets _ _ isF0.isDistributive isF1.isDistributive i } where module isF0 = IsFunctor isF0 @@ -106,8 +106,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] dist = begin (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩ - F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (distrib G) ⟩ - F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ distrib F ⟩ + F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (isDistributive G) ⟩ + F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ isDistributive F ⟩ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎ _∘fr_ : RawFunctor A C @@ -121,7 +121,7 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩ F→ (𝟙 B) ≡⟨ isIdentity F ⟩ 𝟙 C ∎ - ; distrib = dist + ; isDistributive = dist } _∘f_ : Functor A C @@ -136,6 +136,6 @@ identity = record } ; isFunctor = record { isIdentity = refl - ; distrib = refl + ; isDistributive = refl } } diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 2f3c1e9..190592e 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -88,6 +88,6 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat } ; isFunctor = record { isIdentity = :ident: - ; distrib = {!!} + ; isDistributive = {!!} } } From 002badd98d2ae43fdd93b4227fb8c37ab74531b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 12:57:10 +0100 Subject: [PATCH 20/20] Update changelog --- CHANGELOG.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index cc79e6c..56020da 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,23 @@ Changelog ========= +Version 1.2.0 +------------- +This version is mainly a huge refactor. + +I've renamed + +* `distrib` to `isDistributive` +* `arrowIsSet` to `arrowsAreSets` +* `ident` to `isIdentity` +* `assoc` to `isAssociative` + +And added "type-synonyms" for all of these. Their names should now match their +type. So e.g. `isDistributive` has type `IsDistributive`. + +I've also changed how names are exported in `Functor` to be in line with +`Category`. + Version 1.1.0 ------------- In this version categories have been refactored - there's now a notion of a raw