Mercurial > hg > Members > kono > Proof > category
comparison cat-utility.agda @ 253:24e83b8b81be
fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 11 Sep 2013 20:26:48 +0900 |
parents | 58ee98bbb333 |
children | a87d3ea9efe4 |
comparison
equal
deleted
inserted
replaced
252:e0835b8dd51b | 253:24e83b8b81be |
---|---|
9 | 9 |
10 open Functor | 10 open Functor |
11 | 11 |
12 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a | 12 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a |
13 id1 A a = (Id {_} {_} {_} {A} a) | 13 id1 A a = (Id {_} {_} {_} {A} a) |
14 -- We cannot make A implicit | |
14 | 15 |
15 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | 16 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
16 ( U : Functor B A ) | 17 ( U : Functor B A ) |
17 ( F : Obj A → Obj B ) | 18 ( F : Obj A → Obj B ) |
18 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | 19 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) |