Mercurial > hg > Members > kono > Proof > category
diff cat-utility.agda @ 101:0f7086b6a1a6
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 31 Jul 2013 15:17:15 +0900 |
| parents | 4fa718e4fd77 |
| children | 5f331dfc000b |
line wrap: on
line diff
--- a/cat-utility.agda Tue Jul 30 17:58:20 2013 +0900 +++ b/cat-utility.agda Wed Jul 31 15:17:15 2013 +0900 @@ -19,10 +19,10 @@ ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → - A [ A [ FMap U ( f * ) o η a' ] ≈ f ] - uniquness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (F a') b' } → - A [ A [ FMap U g o η a' ] ≈ f ] → B [ f * ≈ g ] + universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → + A [ A [ FMap U ( f * ) o η a ] ≈ f ] + uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } → + A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ] record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A )