Mercurial > hg > Members > kono > Proof > category
view limit-to.agda @ 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 |
line wrap: on
line source
open import Category -- https://github.com/konn/category-agda open import Level module limit-to where open import cat-utility open import HomReasoning open import Relation.Binary.Core open import Data.Maybe open Functor -- If we have limit then we have equalizer --- two objects category --- --- f --- ------> --- 0 1 --- ------> --- g data TwoObject {c₁ : Level} : Set c₁ where t0 : TwoObject t1 : TwoObject record TwoHom {c₁ c₂ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set c₂ where field hom : TwoObject {c₂ } open TwoHom -- arrow composition _×_ : ∀ {c₁ c₂} -> {a b c : TwoObject {c₁}} → Maybe ( TwoHom {c₁} {c₂} b c ) → Maybe ( TwoHom {c₁} {c₂} a b ) → Maybe ( TwoHom {c₁} {c₂} a c ) _×_ 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} {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 _==_ : ∀{c₁ c₂ } { a b : TwoObject {c₁} } -> Rel (Maybe (TwoHom {c₁} {c₂ } a b )) (c₂) _==_ = Eq _≡_ ==refl : ∀{ c₁ c₂ } { a b : TwoObject {c₁} } -> ∀ {x : Maybe (TwoHom {c₁} {c₂ } a b )} → x == x ==refl {_} {_} {_} {_} {just x} = just refl ==refl {_} {_} {_} {_} {nothing} = nothing ==sym : ∀{ c₁ c₂ } { a b : TwoObject {c₁} } -> ∀ {x y : Maybe (TwoHom {c₁} {c₂ } a b )} → _==_ x y → _==_ y x ==sym (just x≈y) = just (≡-sym x≈y) ==sym nothing = nothing ==trans : ∀{ c₁ c₂ } { a b : TwoObject {c₁} } -> ∀ {x y z : Maybe (TwoHom {c₁} {c₂ } a b ) } → x == y → y == z → x == z ==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 _∎ infixr 2 _==⟨_⟩_ _==⟨⟩_ infix 1 begin_ data _IsRelatedTo_ { a b : TwoObject {c₁} } (x y : (Maybe (TwoHom {c₁} {c₂ } a b ))) : Set c₂ where relTo : (x≈y : x == y ) → x IsRelatedTo y begin_ : { a b : TwoObject {c₁} } {x : Maybe (TwoHom {c₁} {c₂ } a b ) } {y : Maybe (TwoHom {c₁} {c₂ } a b )} → x IsRelatedTo y → x == y begin relTo x≈y = x≈y _==⟨_⟩_ : { a b : TwoObject {c₁} } (x : Maybe (TwoHom {c₁} {c₂ } a b )) {y z : Maybe (TwoHom {c₁} {c₂ } a b ) } → x == y → y IsRelatedTo z → x IsRelatedTo z _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z) _==⟨⟩_ : { a b : TwoObject {c₁} }(x : Maybe (TwoHom {c₁} {c₂ } a b )) {y : Maybe (TwoHom {c₁} {c₂ } a b )} → x IsRelatedTo y → x IsRelatedTo y _ ==⟨⟩ x≈y = x≈y _∎ : { a b : TwoObject {c₁} }(x : Maybe (TwoHom {c₁} {c₂ } a b )) → x IsRelatedTo x _∎ _ = relTo ==refl -- f g h -- d <- c <- b <- a assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } {f : Maybe (TwoHom {c₁} {c₂ } c d )} → {g : Maybe (TwoHom {c₁} {c₂ } b c )} → {h : Maybe (TwoHom {c₁} {c₂ } a b )} → ( f × (g × h)) == ((f × g) × h ) assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} with (just f × just g) assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} | nothing = ==refl assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} | just h = ==refl assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t0} {t0} {t1} {t1} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {just _} = ==refl assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {just _} = ==refl TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) -> Maybe (TwoHom {c₁} {c₂ } a a ) TwoId {_} {_} t0 = just record { hom = t0 } TwoId {_} {_} t1 = just record { hom = t1 } 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₂ TwoCat {c₁} {c₂} {ℓ} = record { Obj = TwoObject {c₁} ; Hom = λ a b → Maybe ( TwoHom {c₁} {c₂ } a b ) ; _o_ = \{a} {b} {c} x y -> _×_ {c₁ } { c₂} {a} {b} {c} x y ; _≈_ = Eq _≡_ ; Id = \{a} -> TwoId {c₁ } { c₂} a ; isCategory = record { isEquivalence = record {refl = ==refl ; trans = ==trans ; sym = ==sym } ; identityL = \{a b f} -> identityL {c₁} {c₂ } {a} {b} {f} ; identityR = \{a b f} -> identityR {c₁} {c₂ } {a} {b} {f} ; o-resp-≈ = \{a b c f g h i} -> o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ; associative = \{a b c d f g h } -> assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} } } where identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) == f 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 {_} {_} {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 ==⟨ {!!} ⟩ 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 = {!!} indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) -> Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat A ) indexFunctor {c₁} {c₂} {ℓ} A a b f g = record { FObj = λ a → fobj a ; FMap = λ {a} {b} f → fmap {a} {b} f ; isFunctor = record { identity = \{x} -> identity {x} ; distr = \ {a} {b} {c} {f} {g} -> distr1 {a} {b} {c} {f} {g} ; ≈-cong = \ {a} {b} {c} {f} -> ≈-cong {a} {b} {c} {f} } } where I = TwoCat {c₁} {c₂} {ℓ} MA = MaybeCat A open ≈-Reasoning (MA) fobj : Obj I -> Obj A fobj t0 = a fobj t1 = b fmap : {x y : Obj I } -> Maybe (TwoHom {c₁} {c₂} x y ) -> Hom MA (fobj x) (fobj y) fmap = {!!} open ≈-Reasoning (A) identity : {x : Obj I} → {!!} identity {t0} = {!!} identity {t1} = {!!} distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → {!!} distr1 {a1} {b1} {c} {f1} {g1} = {!!} ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → _[_≈_] I f g → {!!} ≈-cong {_} {_} {f1} {g1} f≈g = {!!} --- Equalizer --- f --- e ------> --- c ------> a b --- ^ / ------> --- |k h g --- | / --- | / --- | / --- |/ --- d open Limit lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → {a0 : Obj A } {u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness → {a b c : Obj A} (f g : Hom A a b ) → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g lim-to-equ {c₁} {c₂} {ℓ } A lim {a} {b} {c} f g e fe=ge = record { fe=ge = fe=ge ; k = λ {d} h fh=gh → k {d} h fh=gh ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where I = TwoCat {c₁} {c₂} {ℓ } Γ = {!!} nmap : (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x) nmap x d h = {!!} commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) -> A [ A [ f o h ] ≈ A [ g o h ] ] → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ] commute1 {x} {y} {f'} d h fh=gh = {!!} nat : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ nat d h fh=gh = record { TMap = λ x → nmap x d h ; isNTrans = record { commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh } } k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c k {d} h fh=gh = {!!} -- limit (lim I Γ {c} {nat c e fe=ge }) d (nat d h fh=gh ) ek=h : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> A [ A [ e o k h fh=gh ] ≈ h ] ek=h d h fh=gh = {!!} uniquness : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> ( k' : Hom A d c ) -> A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] uniquness d h fh=gh = {!!}