Mercurial > hg > Members > kono > Proof > category
changeset 391:2ee1496b31d7
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 15 Mar 2016 14:52:28 +0900 |
| parents | 1301270b8942 |
| children | 61ec02585597 |
| files | limit-to.agda |
| diffstat | 1 files changed, 47 insertions(+), 30 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Tue Mar 15 11:45:43 2016 +0900 +++ b/limit-to.agda Tue Mar 15 14:52:28 2016 +0900 @@ -35,16 +35,15 @@ record RawHom {c₁ ℓ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set (c₁ ⊔ ℓ) where field RawMap : Arrow {ℓ } - isNull : TwoObject {c₁} open RawHom arrow2hom : {c₁ ℓ : Level} -> (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) -> Arrow {ℓ } -> RawHom { c₁} {ℓ } a b -arrow2hom t0 t0 id-t0 = record { RawMap = id-t0 ; isNull = t0 } -arrow2hom t1 t1 id-t1 = record { RawMap = id-t1 ; isNull = t0 } -arrow2hom t0 t1 arrow-f = record { RawMap = arrow-f ; isNull = t0 } -arrow2hom t0 t1 arrow-g = record { RawMap = arrow-g ; isNull = t0 } -arrow2hom _ _ f = record { RawMap = f ; isNull = t1 } +arrow2hom t0 t0 id-t0 = record { RawMap = id-t0 } +arrow2hom t1 t1 id-t1 = record { RawMap = id-t1 } +arrow2hom t0 t1 arrow-f = record { RawMap = arrow-f } +arrow2hom t0 t1 arrow-g = record { RawMap = arrow-g } +arrow2hom _ _ f = record { RawMap = f } record Two-Hom { c₁ ℓ : Level } (a : TwoObject { c₁} ) (b : TwoObject { c₁} ) : Set (c₁ ⊔ ℓ) where field @@ -54,13 +53,13 @@ Map = RawMap hom Two-id : {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) -> Two-Hom {c₁} { ℓ} a a -Two-id t0 = record { hom = record { isNull = t0 ;RawMap = id-t0 } ; arrow-iso = refl } -Two-id t1 = record { hom = record { isNull = t0 ;RawMap = id-t1 } ; arrow-iso = refl } +Two-id t0 = record { hom = record { RawMap = id-t0 } ; arrow-iso = refl } +Two-id t1 = record { hom = record { RawMap = id-t1 } ; arrow-iso = refl } Two-nothing : {c₁ ℓ : Level } -> ( a b : TwoObject {c₁} ) -> Two-Hom {c₁} { ℓ} a b Two-nothing a b = record { hom = record { RawMap = nil } ; arrow-iso = arrow-iso a b } where - arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject {c₁} ) -> arrow2hom {c₁} {ℓ } a b nil ≡ record { RawMap = nil ; isNull = t1 } + arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject {c₁} ) -> arrow2hom {c₁} {ℓ } a b nil ≡ record { RawMap = nil } arrow-iso t0 t0 = refl arrow-iso t0 t1 = refl arrow-iso t1 t0 = refl @@ -74,20 +73,32 @@ twocomp _ _ = nil _×_ : { c₁ ℓ : Level } -> {A B C : TwoObject { c₁} } → Two-Hom { c₁} {ℓ} B C → Two-Hom { c₁} {ℓ} A B → Two-Hom { c₁} {ℓ} A C -_×_ { c₁} {ℓ} {a} {b} {c} f g = record { hom = - record { RawMap = arrow ; isNull = nul } ; - arrow-iso = arrow-iso a c ( arrow ) nul } +_×_ { c₁} {ℓ} {a} {b} {c} f g = record { hom = arrow ; + arrow-iso = arrow-iso a c (RawMap arrow ) } where - arrow = twocomp {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) - nul = isNull ( arrow2hom a b arrow ) - arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject {c₁} ) -> (f : Arrow { ℓ} ) -> ( n : TwoObject {c₁} ) -> - arrow2hom {c₁} {ℓ } a b f ≡ record { RawMap = f ; isNull = n } - arrow-iso t0 t0 id-t0 t0 = refl - arrow-iso t1 t1 id-t1 t0 = refl - arrow-iso t0 t1 arrow-f t0 = refl - arrow-iso t0 t1 arrow-g t0 = refl - arrow-iso _ _ _ t0 = {!!} - arrow-iso _ _ _ t1 = ? + arrow = arrow2hom a c ( twocomp {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) ) + arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject {c₁} ) -> (f : Arrow { ℓ} ) -> + arrow2hom {c₁} {ℓ } a b f ≡ record { RawMap = f } + arrow-iso t0 t0 id-t0 = refl + arrow-iso t1 t1 id-t1 = refl + arrow-iso t0 t1 arrow-f = refl + arrow-iso t0 t1 arrow-g = refl + arrow-iso t0 t0 nil = refl + arrow-iso t0 t1 nil = refl + arrow-iso t1 t0 nil = refl + arrow-iso t1 t1 nil = refl + arrow-iso t0 t1 id-t0 = refl + arrow-iso t1 t0 id-t0 = refl + arrow-iso t1 t1 id-t0 = refl + arrow-iso t0 t1 id-t1 = refl + arrow-iso t1 t0 id-t1 = refl + arrow-iso t0 t0 id-t1 = refl + arrow-iso t1 t0 arrow-f = refl + arrow-iso t1 t1 arrow-f = refl + arrow-iso t0 t0 arrow-f = refl + arrow-iso t1 t0 arrow-g = refl + arrow-iso t1 t1 arrow-g = refl + arrow-iso t0 t0 arrow-g = refl open Two-Hom @@ -110,7 +121,17 @@ open import Relation.Binary.PropositionalEquality ≡-cong = Relation.Binary.PropositionalEquality.cong identityL : {A B : TwoObject} {f : Two-Hom A B} → Map ( Two-id B × f ) ≡ Map f - identityL {a} {b} {f} = {!!} + identityL {a} {b} {f} with Map f + identityL {t0} {t0} {f} | id-t0 = refl + identityL {t0} {t0} {f} | id-t1 = refl + identityL {_} {t0} {f} | id-t0 = let open ≡-Reasoning in + begin + {!!} + ≡⟨ {!!} ⟩ + id-t0 + ∎ + identityL {_} {_} {f} | _ = {!!} + identityR : {A B : TwoObject} {f : Two-Hom A B} → Map ( f × Two-id A ) ≡ Map f identityR {a} {b} {f} = {!!} o-resp-≈ : {A B C : TwoObject} {f g : Two-Hom A B} {h i : Two-Hom B C} → @@ -118,13 +139,9 @@ o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = let open ≡-Reasoning in begin Map (h × f) - ≡⟨⟩ - twocomp (Map h) (Map f) - ≡⟨ ≡-cong (\x -> twocomp (Map h) x ) f≡g ⟩ - twocomp (Map h) (Map g) - ≡⟨ ≡-cong (\x -> twocomp x (Map g) ) h≡i ⟩ - twocomp (Map i) (Map g) - ≡⟨⟩ + ≡⟨ ≡-cong (\x -> RawMap ( arrow2hom a c ( twocomp (Map h) x )) ) f≡g ⟩ + Map (h × g) + ≡⟨ ≡-cong (\x -> RawMap ( arrow2hom a c ( twocomp x (Map g) )) ) h≡i ⟩ Map (i × g) ∎ associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h )