Mercurial > hg > Members > kono > Proof > category

changeset 424:4329525f5085

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix imit-to-edu for MaybeCat / TwoCat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 14:12:53 +0900
parents b5519e954b57
children 98811e927d4a
files limit-to.agda
diffstat 1 files changed, 18 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 24 13:44:27 2016 +0900
+++ b/limit-to.agda	Thu Mar 24 14:12:53 2016 +0900
@@ -27,6 +27,8 @@
    t0 : TwoObject
    t1 : TwoObject
 
+-- constrainted arrow
+--    we need inverse of f to complete cases
 data Arrow {c₁ c₂ : Level } ( t00 t11 :  TwoObject {c₁} ) : TwoObject {c₁}  -> TwoObject {c₁} -> Set c₂ where
    id-t0 : Arrow t00 t11 t00 t00
    id-t1 : Arrow t00 t11 t11 t11
@@ -181,7 +183,7 @@
 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-f = ==refl
 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-g = ==refl
 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just id-t1  = ==refl
---  remaining all failure case
+--  remaining all failure case (except inf-f case )
 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
@@ -384,8 +386,14 @@
 
 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
+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
         →  {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 {
@@ -394,14 +402,15 @@
         ; 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)
+         mf = record { hom = just f }
+         mg = record { hom = just g }
+         Γ = indexFunctor  {c₁} {c₂} {ℓ} A  a b f g
+         nmap :  (x : Obj (I {c₁} {c₂} {ℓ}) ) ( d : Obj (MA  {c₁} {c₂} {ℓ} {A})  ) (h : Hom MA d a ) -> Hom MA (FObj (K MA 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 : 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' ] ]
          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 : 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 h fh=gh = record {
             TMap = λ x → nmap x d h ;
             isNTrans = record {