Mercurial > hg > Members > kono > Proof > category
changeset 414:28249d32b700
Maybe does not help conflict ...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 23 Mar 2016 17:16:29 +0900 |
parents | e08af559efb9 |
children | dd086f5fb29f |
files | limit-to.agda |
diffstat | 1 files changed, 30 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Wed Mar 23 16:25:23 2016 +0900 +++ b/limit-to.agda Wed Mar 23 17:16:29 2016 +0900 @@ -40,9 +40,11 @@ _×_ nothing _ = nothing _×_ (just _) nothing = nothing _×_ {c₁} {c₂} {t1} {t1} {t1} _ f = f +_×_ {c₁} {c₂} {t0} {t0} {t0} f _ = f _×_ {c₁} {c₂} {t0} {t1} {t1} _ f = f -_×_ {c₁} {c₂} {t0} {t0} {t0} _ f = f _×_ {c₁} {c₂} {t0} {t0} {t1} f _ = f +-- _×_ {c₁} {c₂} {t1} {t0} {t0} _ f = f +-- _×_ {c₁} {c₂} {t1} {t1} {t0} f _ = f _×_ {c₁} {c₂} {a} {b} {c} (just f) (just g) = nothing @@ -62,6 +64,7 @@ ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z) ==trans nothing nothing = nothing + module ==-Reasoning {c₁ c₂ : Level} where infixr 2 _∎ @@ -128,6 +131,12 @@ open import maybeCat +-- identityL {c₁} {c₂} {_} {b} {nothing} = let open ==-Reasoning {c₁} {c₂} in +-- begin +-- (TwoId b × nothing) +-- ==⟨ {!!} ⟩ +-- nothing +-- ∎ open import Relation.Binary TwoCat : {c₁ c₂ ℓ : Level } -> Category c₁ c₂ c₂ @@ -146,20 +155,30 @@ } } where identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) == f - identityL {_} {_} {_} {_} {nothing} = {!!} - identityL {_} {_} {t0} {t0} {just f} = ==refl + identityL {c₁} {c₂} {t0} {t0} {nothing} = ==refl + identityL {c₁} {c₂} {t0} {t1} {nothing} = ==refl + identityL {c₁} {c₂} {t1} {t0} {nothing} = ==refl + identityL {c₁} {c₂} {t1} {t1} {nothing} = ==refl identityL {_} {_} {t0} {t1} {just f} = ==refl identityL {_} {_} {t1} {t1} {just f} = ==refl - identityL {c₁} {c₂} {t1} {t0} {just f} = let open ==-Reasoning {c₁} {c₂} in - begin - (TwoId t0 × just f) + identityL {_} {_} {t0} {t0} {just f} = {!!} + identityL {_} {_} {t1} {t0} {just f} = {!!} + identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) == f + identityR {c₁} {c₂} {t0} {t0} {nothing} = ==refl + identityR {c₁} {c₂} {t0} {t1} {nothing} = ==refl + identityR {c₁} {c₂} {t1} {t0} {nothing} = ==refl + identityR {c₁} {c₂} {t1} {t1} {nothing} = ==refl + identityR {_} {_} {t0} {t0} {just f} = ==refl + identityR {_} {_} {t0} {t1} {just f} = ==refl + identityR {c₁} {c₂} {t1} {t0} {just f} = let open ==-Reasoning {c₁} {c₂} in + begin + (just f × TwoId t1) ==⟨⟩ - nothing + nothing ==⟨ {!!} ⟩ - just f - ∎ - identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) == f - identityR {_} {_} {a} {b} {f} = {!!} + just f + ∎ + identityR {_} {_} {t1} {t1} {just f} = {!!} o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : Maybe ( TwoHom {c₁} {c₂ } A B)} {h i : Maybe ( TwoHom B C)} → f == g → h == i → ( h × f ) == ( i × g ) o-resp-≈ {_} {_} {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = {!!}