Mercurial > hg > Members > kono > Proof > category
changeset 392:61ec02585597
trying ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 15 Mar 2016 16:11:37 +0900 |
| parents | 2ee1496b31d7 |
| children | 15d28525e756 |
| files | limit-to.agda |
| diffstat | 1 files changed, 35 insertions(+), 49 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Tue Mar 15 14:52:28 2016 +0900 +++ b/limit-to.agda Tue Mar 15 16:11:37 2016 +0900 @@ -27,10 +27,11 @@ data Arrow {ℓ : Level } : Set ℓ where id-t0 : Arrow - id-t1 : Arrow arrow-f : Arrow arrow-g : Arrow - nil : Arrow -- inconsitent hom + reverse-f : Arrow + reverse-g : Arrow + nil : Arrow record RawHom {c₁ ℓ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set (c₁ ⊔ ℓ) where field @@ -38,67 +39,48 @@ 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 } -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 } +arrow2hom : {c₁ ℓ : Level} -> {a : TwoObject {c₁} } {b : TwoObject {c₁} } -> Arrow {ℓ } -> RawHom { c₁} {ℓ } a b +arrow2hom id-t0 = record { RawMap = id-t0 } +arrow2hom arrow-f = record { RawMap = arrow-f } +arrow2hom arrow-g = record { RawMap = arrow-g } +arrow2hom reverse-f = record { RawMap = reverse-f } +arrow2hom reverse-g = record { RawMap = reverse-g } +arrow2hom nil = record { RawMap = nil } record Two-Hom { c₁ ℓ : Level } (a : TwoObject { c₁} ) (b : TwoObject { c₁} ) : Set (c₁ ⊔ ℓ) where field hom : RawHom { c₁} {ℓ } a b - arrow-iso : arrow2hom a b ( RawMap hom ) ≡ hom + arrow-iso : arrow2hom ( RawMap hom ) ≡ hom Map : Arrow Map = RawMap hom Two-id : {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) -> Two-Hom {c₁} { ℓ} a a -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 } - arrow-iso t0 t0 = refl - arrow-iso t0 t1 = refl - arrow-iso t1 t0 = refl - arrow-iso t1 t1 = refl +Two-id _ = record { hom = record { RawMap = id-t0 } ; arrow-iso = refl } -- arrow composition twocomp : {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Arrow {ℓ } twocomp id-t0 f = f twocomp f id-t0 = f +twocomp arrow-f reverse-f = id-t0 +twocomp arrow-g reverse-g = id-t0 +twocomp reverse-f arrow-f = id-t0 +twocomp reverse-g arrow-g = id-t0 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 = arrow ; - arrow-iso = arrow-iso a c (RawMap arrow ) } + arrow-iso = arrow-iso (RawMap arrow ) } where - 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 + arrow = arrow2hom {c₁ } {ℓ } {a} {c} ( twocomp {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) ) + arrow-iso : (f : Arrow { ℓ} ) -> + arrow2hom {c₁} {ℓ } {a} {c} f ≡ record { RawMap = f } + arrow-iso id-t0 = refl + arrow-iso arrow-f = refl + arrow-iso arrow-g = refl + arrow-iso reverse-f = refl + arrow-iso reverse-g = refl + arrow-iso nil = refl open Two-Hom @@ -123,10 +105,14 @@ identityL : {A B : TwoObject} {f : Two-Hom A B} → Map ( Two-id B × f ) ≡ Map 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 + identityL {t1} {t0} {f} | id-t0 = refl + identityL {t0} {t0} {f} | nil = refl + identityL {t0} {t1} {f} | nil = refl + identityL {t1} {t0} {f} | nil = refl + identityL {t1} {t1} {f} | nil = refl + identityL {a} {t1} {f} | id-t0 = let open ≡-Reasoning in begin - {!!} + {!!} ≡⟨ {!!} ⟩ id-t0 ∎ @@ -139,9 +125,9 @@ o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = let open ≡-Reasoning in begin Map (h × f) - ≡⟨ ≡-cong (\x -> RawMap ( arrow2hom a c ( twocomp (Map h) x )) ) f≡g ⟩ + ≡⟨ ≡-cong (\x -> RawMap ( arrow2hom ( twocomp (Map h) x ) ) ) f≡g ⟩ Map (h × g) - ≡⟨ ≡-cong (\x -> RawMap ( arrow2hom a c ( twocomp x (Map g) )) ) h≡i ⟩ + ≡⟨ ≡-cong (\x -> RawMap ( arrow2hom ( 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 )