Mercurial > hg > Members > kono > Proof > category
changeset 427:531b739a1d7c
add Nil
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 26 Mar 2016 12:31:14 +0900 |
| parents | 1290d6876129 |
| children | 7f8b9f1f1bba |
| files | limit-to.agda |
| diffstat | 1 files changed, 93 insertions(+), 104 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Sat Mar 26 10:16:05 2016 +0900 +++ b/limit-to.agda Sat Mar 26 12:31:14 2016 +0900 @@ -289,87 +289,6 @@ hom ( i × g ) ∎ - -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 - fobj : Obj I -> Obj A - fobj t0 = a - fobj t1 = b - fmap : {x y : Obj I } -> (TwoHom {c₁} {c₂} x y ) -> Hom MA (fobj x) (fobj y) - fmap {x} {y} h with hom h - fmap {t0} {t0} h | just id-t0 = id1 MA a - fmap {t1} {t1} h | just id-t1 = id1 MA b - fmap {t0} {t1} h | just arrow-f = record { hom = just f } - fmap {t0} {t1} h | just arrow-g = record { hom = just g } - fmap {_} {_} h | _ = record { hom = nothing } - ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → MA [ fmap f ≈ fmap g ] - ≈-cong {a} {b} {f1} {g1} f≈g with hom f1 | hom g1 - ≈-cong {t0} {t0} {f1} {g1} nothing | nothing | nothing = nothing - ≈-cong {t0} {t1} {f1} {g1} nothing | nothing | nothing = nothing - ≈-cong {t1} {t0} {f1} {g1} nothing | nothing | nothing = nothing - ≈-cong {t1} {t1} {f1} {g1} nothing | nothing | nothing = nothing - ≈-cong {t0} {t0} {f1} {g1} (just refl) | just id-t0 | just id-t0 = let open ≡≡-Reasoning A in ≡≡-refl - ≈-cong {t1} {t1} {f1} {g1} (just refl) | just id-t1 | just id-t1 = let open ≡≡-Reasoning A in ≡≡-refl - ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-f | just arrow-f = let open ≡≡-Reasoning A in ≡≡-refl - ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-g | just arrow-g = let open ≡≡-Reasoning A in ≡≡-refl - ≈-cong {t1} {t0} {f1} {g1} (just refl) | just inv-f | just inv-f = let open ≡≡-Reasoning A in ≡≡-refl - open ≈-Reasoning (MA) - identity : {x : Obj I} → MA [ fmap ( id1 I x ) ≈ id1 MA (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} → - MA [ fmap (I [ g₁ o f₁ ]) ≈ MA [ fmap g₁ o fmap f₁ ] ] - distr1 {a1} {b1} {c1} {f1} {g1} with hom g1 | hom f1 - distr1 {t0} {t0} {t0} {f1} {g1} | nothing | nothing = nothing - distr1 {t0} {t0} {t1} {f1} {g1} | nothing | nothing = nothing - distr1 {t0} {t1} {t0} {f1} {g1} | nothing | nothing = nothing - distr1 {t0} {t1} {t1} {f1} {g1} | nothing | nothing = nothing - distr1 {t1} {t0} {t0} {f1} {g1} | nothing | nothing = nothing - distr1 {t1} {t0} {t1} {f1} {g1} | nothing | nothing = nothing - distr1 {t1} {t1} {t0} {f1} {g1} | nothing | nothing = nothing - distr1 {t1} {t1} {t1} {f1} {g1} | nothing | nothing = nothing - distr1 {t0} {t0} {t0} {f1} {g1} | nothing | just id-t0 = nothing - distr1 {t0} {t0} {t1} {f1} {g1} | nothing | just id-t0 = nothing - distr1 {t1} {t1} {t0} {f1} {g1} | nothing | just id-t1 = nothing - distr1 {t1} {t1} {t1} {f1} {g1} | nothing | just id-t1 = nothing - distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-f = nothing - distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-f = nothing - distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-g = nothing - distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-g = nothing - distr1 {t1} {t0} {t0} {f1} {g1} | nothing | just inv-f = nothing - distr1 {t1} {t0} {t1} {f1} {g1} | nothing | just inv-f = nothing - distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | nothing = nothing - distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | nothing = nothing - distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | nothing = nothing - distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | nothing = nothing - distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | nothing = nothing - distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-f | nothing = nothing - distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | nothing = nothing - distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-g | nothing = nothing - distr1 {t0} {t1} {t0} {f1} {g1} | just inv-f | nothing = nothing - distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | nothing = nothing - distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | just id-t0 = sym idL - distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | just inv-f = sym idL - distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | just id-t0 = sym idR - distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | just id-t0 = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | just id-t1 = sym idL - distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-f = sym idL - distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-g = sym idL - distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | just id-t1 = sym idL - distr1 {t0} {t1} {t0} {_} {_} | (just inv-f) | (just _) = nothing - distr1 {t1} {t0} {t1} {_} {_} | (just arrow-f) | (just _) = nothing - distr1 {t1} {t0} {t1} {_} {_} | (just arrow-g) | (just _) = nothing - record Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where field nil : {a b : Obj A } -> Hom A a b @@ -409,6 +328,86 @@ ≈-cong {a} {b} {f} {g} (just eq) | just _ | just _ = eq +indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) -> Functor (TwoCat {c₁} {c₂} {c₂} ) A +indexFunctor {c₁} {c₂} {ℓ} A none 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₂} {ℓ} + fobj : Obj I -> Obj A + fobj t0 = a + fobj t1 = b + fmap : {x y : Obj I } -> (TwoHom {c₁} {c₂} x y ) -> Hom A (fobj x) (fobj y) + fmap {x} {y} h with hom h + fmap {t0} {t0} h | just id-t0 = id1 A a + fmap {t1} {t1} h | just id-t1 = id1 A b + fmap {t0} {t1} h | just arrow-f = f + fmap {t0} {t1} h | just arrow-g = g + fmap {_} {_} h | _ = nil none + open ≈-Reasoning A + ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ] + ≈-cong {a} {b} {f1} {g1} f≈g with hom f1 | hom g1 + ≈-cong {t0} {t0} {f1} {g1} nothing | nothing | nothing = refl-hom + ≈-cong {t0} {t1} {f1} {g1} nothing | nothing | nothing = refl-hom + ≈-cong {t1} {t0} {f1} {g1} nothing | nothing | nothing = refl-hom + ≈-cong {t1} {t1} {f1} {g1} nothing | nothing | nothing = refl-hom + ≈-cong {t0} {t0} {f1} {g1} (just refl) | just id-t0 | just id-t0 = refl-hom + ≈-cong {t1} {t1} {f1} {g1} (just refl) | just id-t1 | just id-t1 = refl-hom + ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-f | just arrow-f = refl-hom + ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-g | just arrow-g = refl-hom + ≈-cong {t1} {t0} {f1} {g1} (just refl) | just inv-f | just inv-f = refl-hom + 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 {a1} {b1} {c1} {f1} {g1} with hom g1 | hom f1 + distr1 {t0} {t0} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) + distr1 {t0} {t0} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) + distr1 {t0} {t1} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) + distr1 {t0} {t1} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) + distr1 {t1} {t0} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) + distr1 {t1} {t0} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) + distr1 {t1} {t1} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) + distr1 {t1} {t1} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) + distr1 {t0} {t0} {t0} {f1} {g1} | nothing | just id-t0 = sym ( nil-idL none ) + distr1 {t0} {t0} {t1} {f1} {g1} | nothing | just id-t0 = sym ( nil-idL none ) + distr1 {t1} {t1} {t0} {f1} {g1} | nothing | just id-t1 = sym ( nil-idL none ) + distr1 {t1} {t1} {t1} {f1} {g1} | nothing | just id-t1 = sym ( nil-idL none ) + distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-f = sym ( nil-idL none ) + distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-f = sym ( nil-idL none ) + distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-g = sym ( nil-idL none ) + distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-g = sym ( nil-idL none ) + distr1 {t1} {t0} {t0} {f1} {g1} | nothing | just inv-f = sym ( nil-idL none ) + distr1 {t1} {t0} {t1} {f1} {g1} | nothing | just inv-f = sym ( nil-idL none ) + distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | nothing = sym ( nil-idR none ) + distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | nothing = sym ( nil-idR none ) + distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | nothing = sym ( nil-idR none ) + distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | nothing = sym ( nil-idR none ) + distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | nothing = sym ( nil-idR none ) + distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-f | nothing = sym ( nil-idR none ) + distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | nothing = sym ( nil-idR none ) + distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-g | nothing = sym ( nil-idR none ) + distr1 {t0} {t1} {t0} {f1} {g1} | just inv-f | nothing = sym ( nil-idR none ) + distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | nothing = sym ( nil-idR none ) + distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | just id-t0 = sym idL + distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | just inv-f = sym idL + distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | just id-t0 = sym idR + distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | just id-t0 = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | just id-t1 = sym idL + distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-f = sym idL + distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-g = sym idL + distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | just id-t1 = sym ( nil-idL none ) + distr1 {t0} {t1} {t0} {_} {_} | (just inv-f) | (just _) = sym ( nil-idL none ) + distr1 {t1} {t0} {t1} {_} {_} | (just arrow-f) | (just _) = sym ( nil-idR none ) + distr1 {t1} {t0} {t1} {_} {_} | (just arrow-g) | (just _) = sym ( nil-idR none ) + + --- Equalizer --- f @@ -434,36 +433,28 @@ I' : {c₁ c₂ ℓ : Level} -> Category c₁ c₂ c₂ I' {c₁} {c₂} {ℓ} = TwoCat {c₁} {c₂} {ℓ} -MA' : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) -MA' {c₁} {c₂} {ℓ} {A} = MaybeCat A -lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - (lim : ( Γ : Functor (I' {c₁} {c₂} {ℓ}) (MA' {c₁} {c₂} {ℓ} {A}) ) → {a0 : Obj A } - {u : NTrans I' MA' ( K MA' I' a0 ) Γ } → Limit MA' I' Γ a0 u ) -- completeness +lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( none : Nil A ) + (lim : ( Γ : Functor (I' {c₁} {c₂} {ℓ}) 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 { +lim-to-equ {c₁} {c₂} {ℓ } A none 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 - MA = MA' {c₁} {c₂} {ℓ} {A} I = I' {c₁} {c₂} {ℓ} - mf : Hom MA a b - mf = record { hom = just f } - mg : Hom MA a b - mg = record { hom = just g } - Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g - nmap : (x : Obj I ) ( d : Obj (MA) ) (h : Hom MA d a ) -> Hom MA (FObj (K MA I d) x) (FObj Γ x) - nmap x d h with x | MaybeHom.hom h - ... | _ | nothing = record { hom = nothing } - ... | t0 | just jh = record { hom = just jh } - ... | t1 | just jh = record { hom = just ( A [ f o jh ] ) } - commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj MA) (h : Hom MA d a ) -> MA [ MA [ mf o h ] ≈ MA [ mg o h ] ] - → MA [ MA [ FMap Γ f' o nmap x d h ] ≈ MA [ nmap y d h o FMap (K MA I d) f' ] ] + Γ = indexFunctor {c₁} {c₂} {ℓ} A none a b f g + 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 with x + ... | t0 = h + ... | t1 = A [ f o 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 MA) → (h : Hom MA d a ) → MA [ MA [ mf o h ] ≈ MA [ mg o h ] ] → NTrans I MA (K MA I d) Γ + 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 { @@ -471,9 +462,7 @@ } } 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 with MaybeHom.hom ( limit (lim Γ {c} {nat c (record { hom = just e}) (just fe=ge) }) d (nat d (record { hom = just h }) (just fh=gh) ) ) - k {d} h fh=gh | nothing = {!!} - k {d} h fh=gh | just f = f + k {d} h fh=gh = limit (lim Γ {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 ] ] ) ->