Mercurial > hg > Members > kono > Proof > category
view discrete.agda @ 455:55a9b6177ed4
on going ...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 02 Mar 2017 14:58:40 +0900 |
parents | 2f07f4dd9a6d |
children | 4d97955ea419 |
line wrap: on
line source
open import Category -- https://github.com/konn/category-agda open import Level module discrete where open import Relation.Binary.Core open import Relation.Nullary open import Data.Empty open import Data.Unit open import Data.Maybe open import cat-utility open import HomReasoning open Functor data TwoObject {c₁ : Level} : Set c₁ where t0 : TwoObject t1 : TwoObject -- If we have limit then we have equalizer --- two objects category --- --- f --- -----→ --- 0 1 --- -----→ --- g data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where id-t0 : TwoHom t0 t0 id-t1 : TwoHom t1 t1 arrow-f : TwoHom t0 t1 arrow-g : TwoHom t0 t1 comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → TwoHom {c₁} {c₂} b c → TwoHom {c₁} {c₂} a b → TwoHom {c₁} {c₂} a c comp {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f comp {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g comp {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1 comp {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f comp {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g comp {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0 open TwoHom _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c ) _×_ {c₁} {c₂} {a} {b} {c} f g = comp {c₁} {c₂} {a} {b} {c} f g -- f g h -- d <- c <- b <- a -- -- It can be proved without TwoHom constraints assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } {f : (TwoHom {c₁} {c₂ } c d )} → {g : (TwoHom {c₁} {c₂ } b c )} → {h : (TwoHom {c₁} {c₂ } a b )} → ( f × (g × h)) ≡ ((f × g) × h ) assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with f | g | h assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0 | id-t0 | id-t0 = refl assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0 | id-t0 = refl assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0 | id-t0 = refl assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-f | id-t0 = refl assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-g | id-t0 = refl assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-f = refl assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-g = refl assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1 | id-t1 | id-t1 = refl TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) TwoId {_} {_} t0 = id-t0 TwoId {_} {_} t1 = id-t1 open import Relation.Binary open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ TwoCat {c₁} {c₂} = record { Obj = TwoObject {c₁} ; Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ; _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ; _≈_ = λ x y → x ≡ y ; 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 : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f identityL {c₁} {c₂} {a} {b} {f} with f identityL {c₁} {c₂} {t1} {t1} | id-t1 = refl identityL {c₁} {c₂} {t0} {t0} | id-t0 = refl identityL {c₁} {c₂} {t0} {t1} | arrow-f = refl identityL {c₁} {c₂} {t0} {t1} | arrow-g = refl identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f identityR {c₁} {c₂} {_} {_} {f} with f identityR {c₁} {c₂} {t1} {t1} | id-t1 = refl identityR {c₁} {c₂} {t0} {t0} | id-t0 = refl identityR {c₁} {c₂} {t0} {t1} | arrow-f = refl identityR {c₁} {c₂} {t0} {t1} | arrow-g = refl o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin ( h × f ) ≡⟨ refl ⟩ comp (h) (f) ≡⟨ cong (λ x → comp ( h ) x ) f==g ⟩ comp (h) (g) ≡⟨ cong (λ x → comp x ( g ) ) h==i ⟩ comp (i) (g) ≡⟨ refl ⟩ ( i × g ) ∎ indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) 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 T = TwoCat {c₁} {c₂} fobj : Obj T → Obj A fobj t0 = a fobj t1 = b fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y) fmap {t0} {t0} id-t0 = id1 A a fmap {t1} {t1} id-t1 = id1 A b fmap {t0} {t1} arrow-f = f fmap {t0} {t1} arrow-g = g ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ] ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ] identity t0 = let open ≈-Reasoning A in refl-hom identity t1 = let open ≈-Reasoning A in refl-hom distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} → A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ] distr1 {a} {b} {c} {f} {g} with f | g distr1 {t0} {t0} {t0} {f} {g} | id-t0 | id-t0 = let open ≈-Reasoning A in sym-hom idL distr1 {t1} {t1} {t1} {f} {g} | id-t1 | id-t1 = let open ≈-Reasoning A in begin id1 A b ≈↑⟨ idL ⟩ id1 A b o id1 A b ∎ distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-f = let open ≈-Reasoning A in begin fmap (comp arrow-f id-t0) ≈⟨⟩ fmap arrow-f ≈↑⟨ idR ⟩ fmap arrow-f o id1 A a ∎ distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-g = let open ≈-Reasoning A in begin fmap (comp arrow-g id-t0) ≈⟨⟩ fmap arrow-g ≈↑⟨ idR ⟩ fmap arrow-g o id1 A a ∎ distr1 {t0} {t1} {t1} {f} {g} | arrow-f | id-t1 = let open ≈-Reasoning A in begin fmap (comp id-t1 arrow-f) ≈⟨⟩ fmap arrow-f ≈↑⟨ idL ⟩ id1 A b o fmap arrow-f ∎ distr1 {t0} {t1} {t1} {f} {g} | arrow-g | id-t1 = let open ≈-Reasoning A in begin fmap (comp id-t1 arrow-g) ≈⟨⟩ fmap arrow-g ≈↑⟨ idL ⟩ id1 A b o fmap arrow-g ∎ --- Equalizer --- f --- e -----→ --- c -----→ a b --- ^ / -----→ --- |k h g --- | / --- | / ^ --- | / | --- |/ | Γ --- d _ | --- |\ | --- \ K af --- \ -----→ --- \ t0 t1 --- -----→ --- ag --- --- open Complete open Limit open NTrans equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A (TwoCat {c₁} {c₂} )) -> Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a equlimit A f g comp = {!!} lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A (TwoCat {c₁} {c₂} ) ) → {a b : Obj A} (f g : Hom A a b ) → (fe=ge : A [ A [ f o (equlimit A f g comp ) ] ≈ A [ g o (equlimit A f g comp ) ] ] ) → IsEqualizer A (equlimit A f g comp ) f g lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g 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₂} Γ : Functor I A Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g eqlim = isLimit comp Γ c = limit-c comp Γ e = equlimit A f g comp 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 = {!!} 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 = {!!} uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ] uniq-nat = {!!} 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 {!!} ≈ k' ] uniquness = {!!}