Mercurial > hg > Members > kono > Proof > category

comparison cat-utility.agda @ 731:117e5b392673

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generalize Free Theorem
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Nov 2017 14:42:49 +0900
parents 7a6ee564e3a8
children
comparison
equal deleted inserted replaced
730:e4ef69bae044 731:117e5b392673
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 -- We cannot make A implicit
15
16 record Iso {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
17 (x y : Obj C )
18 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
19 field
20 ≅→ : Hom C x y
21 ≅← : Hom C y x
22 iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ]
23 iso← : C [ C [ ≅→ o ≅← ] ≈ id1 C y ]
24
15 25
16 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 26 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
17 ( U : Functor B A ) 27 ( U : Functor B A )
18 ( F : Obj A → Obj B ) 28 ( F : Obj A → Obj B )
19 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) 29 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )