Mercurial > hg > Members > kono > Proof > category
view limit-to.agda @ 363:cf9ee72f9b0e
two cat
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 05 Mar 2016 07:20:03 +0900 |
parents | c18b209a662a |
children | e8e98be4ce57 |
line wrap: on
line source
open import Category -- https://github.com/konn/category-agda open import Level module limit-to {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where open import cat-utility open import HomReasoning open import Relation.Binary.Core open import Category.Sets open Functor open import Data.Nat hiding ( _⊔_ ) renaming ( suc to succ ) open import Data.Bool open import Data.Fin as Fin using (Fin; Fin′; #_; toℕ) renaming (_ℕ-ℕ_ to _-_ ; zero to Fzero ; suc to Fsuc ) -- If we have limit then we have equalizer --- two objects category --- --- f --- ------> --- 0 1 --- ------> --- g data TwoObject {c₁} : Set c₁ where t0 : TwoObject t1 : TwoObject record TwoCat {ℓ c₁ c₂ : Level } (Two : Category c₁ c₂ ℓ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where field hom→ : Obj Two -> TwoObject {ℓ} hom← : TwoObject {ℓ} -> Obj Two hom-iso : {a : Obj Two} -> hom← ( hom→ a) ≡ a hom-rev : {a : TwoObject {ℓ} } -> hom→ ( hom← a) ≡ a open Limit lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (two : TwoCat A ) (lim : ( Γ : 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₁} A I two 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} → {!!} ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!} } where Γobj : {!!} → Obj A Γobj t0 = a Γobj t1 = b Γmap : {!!} → Hom A a b Γmap t0 = f Γmap t1 = g Γ : Functor I A Γ = record { FObj = λ x → Γobj {!!} ; FMap = λ f → {!!} ; isFunctor = record { ≈-cong = {!!} ; identity = {!!} ; distr = {!!} } } nat : (d : Obj A) → NTrans I A (K A I d) Γ nat d = record { TMap = λ x → {!!} ; isNTrans = record { commute = {!!} } } 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 Γ {c} {nat c}) d (nat d)