Mercurial > hg > Members > kono > Proof > category

comparison limit-to.agda @ 361:e9d4e6ab6cd1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jun 2015 19:18:57 +0900 (2015-06-26)
parents 29e0f0bd4d2c
children c18b209a662a
comparison
equal deleted inserted replaced
360:29e0f0bd4d2c 361:e9d4e6ab6cd1
106 106
107 Two-id : (a : Two ) -> Two-Hom a a 107 Two-id : (a : Two ) -> Two-Hom a a
108 Two-id t0 = record { Map = id-0 ; isMap = refl } 108 Two-id t0 = record { Map = id-0 ; isMap = refl }
109 Two-id t1 = record { Map = id-1 ; isMap = refl } 109 Two-id t1 = record { Map = id-1 ; isMap = refl }
110 110
111 -- arrow composition
112
113 _×_ : {A B C : Two} → Two-Hom B C → Two-Hom A B → Two-Hom A C
114 _×_ {t0} {t0} {t0} a b = {!!}
115 _×_ {t0} {t0} {t1} a b = {!!}
116 _×_ {t0} {t1} {t0} a b = {!!}
117 _×_ {t0} {t1} {t1} a b = {!!}
118 _×_ {t1} {t0} {t1} a b = {!!}
119 _×_ {t1} {t0} {t0} a b = {!!}
120 _×_ {t1} {t1} {t1} a b = {!!}
121 _×_ {t1} {t1} {t0} a b = {!!}
122
123
111 open Two-Hom 124 open Two-Hom
112 125
113 twocat : Category c₁ _ (ℓ ⊔ (suc c₂ ⊔ c₁)) 126 twocat : Category c₁ _ (ℓ ⊔ (suc c₂ ⊔ c₁))
114 twocat = record { 127 twocat = record {
115 Obj = Two ; 128 Obj = Two ;
116 Hom = λ a b → Two-Hom a b ; 129 Hom = λ a b → Two-Hom a b ;
117 _o_ = {!!} ; 130 _o_ = _×_ ;
118 _≈_ = _≡_; 131 _≈_ = _≡_;
119 Id = \{a} -> Two-id a ; 132 Id = \{a} -> Two-id a ;
120 isCategory = record { 133 isCategory = record {
121 isEquivalence = {!!} ; 134 isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym};
122 identityL = {!!} ; 135 identityL = {!!} ;
123 identityR = {!!} ; 136 identityR = {!!} ;
124 o-resp-≈ = {!!} ; 137 o-resp-≈ = {!!} ;
125 associative = {!!} 138 associative = {!!}
126 } 139 }