Mercurial > hg > Members > kono > Proof > category
diff Comma.agda @ 623:bed3be9a4168
One
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Jun 2017 19:11:36 +0900 |
| parents | c7b8017bcd4d |
| children |
line wrap: on
line diff
--- a/Comma.agda Fri Jun 23 10:07:34 2017 +0900 +++ b/Comma.agda Fri Jun 23 19:11:36 2017 +0900 @@ -1,6 +1,6 @@ open import Level open import Category -module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} +module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁'' c₂'' ℓ''} {C : Category c₁' c₂' ℓ'} ( F : Functor A C ) ( G : Functor B C ) where open import HomReasoning @@ -13,7 +13,7 @@ open Functor -record CommaObj : Set ( c₁ ⊔ c₂' ) where +record CommaObj : Set ( c₁ ⊔ c₁'' ⊔ c₂' ) where field obj : Obj A objb : Obj B @@ -21,7 +21,7 @@ open CommaObj -record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ ℓ' ) where +record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ c₂'' ⊔ ℓ' ) where field arrow : Hom A ( obj a ) ( obj b ) arrowg : Hom B ( objb a ) ( objb b ) @@ -29,7 +29,7 @@ open CommaHom -record _⋍_ { a b : CommaObj } ( f g : CommaHom a b ) : Set ℓ where +record _⋍_ { a b : CommaObj } ( f g : CommaHom a b ) : Set (ℓ ⊔ ℓ'' ) where field eqa : A [ arrow f ≈ arrow g ] eqb : B [ arrowg f ≈ arrowg g ] @@ -103,7 +103,7 @@ } } -CommaCategory : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ +CommaCategory : Category (c₂' ⊔ c₁ ⊔ c₁'') (ℓ' ⊔ c₂ ⊔ c₂'') (ℓ ⊔ ℓ'' ) CommaCategory = record { Obj = CommaObj ; Hom = CommaHom ; _o_ = _∙_