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.Core 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 data Arrow {ℓ : Level } : Set ℓ where id-t0 : Arrow arrow-f : Arrow arrow-g : Arrow reverse-f : Arrow reverse-g : Arrow nil : Arrow record RawHom {c₁ ℓ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set (c₁ ⊔ ℓ) where field RawMap : Arrow {ℓ } open RawHom 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 ( RawMap hom ) ≡ hom Map : Arrow Map = RawMap hom Two-id : {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) -> Two-Hom {c₁} { ℓ} a a 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 (RawMap arrow ) } where 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 TwoCat : { c₁ c₂ ℓ : Level } -> Category c₁ (ℓ ⊔ c₁) ℓ TwoCat {c₁} {c₂} {ℓ} = record { Obj = TwoObject {c₁} ; Hom = λ a b → Two-Hom {c₁ } { ℓ} a b ; _o_ = _×_ { c₁} {ℓ} ; _≈_ = λ a b → Map a ≡ Map b ; Id = \{a} -> Two-id a ; isCategory = record { isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym}; identityL = \{a b f} -> identityL {a} {b} {f} ; identityR = \{a b f} -> identityR {a} {b} {f} ; o-resp-≈ = \{a b c f g h i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; associative = \{a b c d f g h } -> associative {a} {b} {c} {d} {f} {g} {h} } } where open import Relation.Binary.PropositionalEquality ≡-cong = Relation.Binary.PropositionalEquality.cong 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 {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 ∎ identityL {_} {_} {f} | _ = {!!} identityR : {A B : TwoObject} {f : Two-Hom A B} → Map ( f × Two-id A ) ≡ Map f identityR {a} {b} {f} = {!!} o-resp-≈ : {A B C : TwoObject} {f g : Two-Hom A B} {h i : Two-Hom B C} → Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g ) 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 ( twocomp (Map h) x ) ) ) f≡g ⟩ Map (h × g) ≡⟨ ≡-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 ) associative {_} {_} {_} {_} {f} {g} {h} = {!!} indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A ) ( f g : Hom A a b ) ( nf : Hom A a b ) ( nf-rev : Hom A b a ) ( nidA : Hom A a a ) ( nidB : Hom A b b ) -> Functor (TwoCat {c₁} {c₂} {ℓ} ) A indexFunctor {c₁} {c₂} {ℓ} A a b f g nf nf-rev nidA nidB = record { FObj = λ a → fobj a ; FMap = λ f → fmap f ; isFunctor = record { identity = \{x} -> identity {x} ; distr = \ {a} {b} {c} {f} {g} -> distr1 {a} {b} {c} {f} {g} ; ≈-cong = {!!} } } where I = TwoCat {c₁} {c₂} {ℓ} fobj : Obj I -> Obj A fobj t0 = a fobj t1 = b fmap1 : {x y : Obj I } -> Hom I x y -> Arrow -> Hom A (fobj x) (fobj y) fmap1 {_} {_} x f = {!!} fmap : {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y) fmap {x} {y} f = fmap1 {x} {y} f ( Map f) open ≈-Reasoning (A) identity : {x : Obj I} → A [ fmap (id1 I x) ≈ id1 A (fobj x) ] identity {t0} = refl-hom identity {t1} = refl-hom distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ] distr1 = {!!} ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ] ≈-cong {_} {_} {f1} {g1} f≈g = {!!} -- ≡-cong f≈g (\x -> fmap1 g1 x) --- 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} ( nf : Hom A a b ) ( nf-rev : Hom A b a ) ( nidA : Hom A a a ) ( nidB : Hom A b b ) (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} nf nf-rev nidA nidB 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₂} {ℓ } Γ = indexFunctor A a b f g nf nf-rev nidA nidB 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 = {!!}