Mercurial > hg > Members > kono > Proof > category

comparison CCC.agda @ 781:340708e8d54f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for 2.5.4.2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 08 Mar 2019 17:46:59 +0900
parents b44c1c6ce646
children bded2347efa4
comparison
equal deleted inserted replaced
780:b44c1c6ce646 781:340708e8d54f
43 lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f 43 lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f
44 lemma {a} {b} {f} with f 44 lemma {a} {b} {f} with f
45 ... | OneObj = refl 45 ... | OneObj = refl
46 46
47 47
48 record isCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A) 48 record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A)
49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where 49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
50 field 50 field
51 ccc-1 : {a : Obj A} → -- Hom A a one ≅ {*} 51 ccc-1 : {a : Obj A} → -- Hom A a one ≅ {*}
52 IsoS A OneCat a one OneObj OneObj 52 IsoS A OneCat a one OneObj OneObj
53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b ) 53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
54 IsoS A (A × A) c (a * b) (c , c) (a , b) 54 IsoS A (A × A) c (a * b) (c , c) (a , b)
55 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c 55 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
56 IsoS A A a (c ^ b) (a * b) c 56 IsoS A A a (c ^ b) (a * b) c
57 57
58 58
59 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
60 field
61 one : Obj A
62 _*_ : Obj A → Obj A → Obj A
63 _^_ : Obj A → Obj A → Obj A
64 isCCC : IsCCC A one _*_ _^_
59 65
66 record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A) ( oneT : ( a : Obj A ) → Hom A a one )
67 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
68 field
69 e2 : {a : Obj A} { f : Hom A a one } → A [ f ≈ oneT a ]
70 e3a : {!!}
71