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) ) )