Mercurial > hg > Members > kono > Proof > category

changeset 270:8ba03259a177

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 19:49:38 +0900
parents 6056a995964b
children 28278175d696
files pullback.agda
diffstat 1 files changed, 31 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Sun Sep 22 18:48:12 2013 +0900
+++ b/pullback.agda	Sun Sep 22 19:49:38 2013 +0900
@@ -155,6 +155,10 @@
          A [ A [ TMap t0 i o  limit a t ]  ≈ TMap t i ]
      limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ∀ ( i : Obj I ) →
          A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] → A [ limit a t ≈ f ]
+  A0 : Obj A
+  A0 = a0
+  T0 : NTrans I A ( K I a0 ) Γ 
+  T0 = t0
 
 --------------------------------
 --
@@ -232,17 +236,32 @@
 
 open import Function
 
-lim-ε : ( a0 : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ )
-     ( lim : Limit I Γ a0 t0 ) → (b : Obj ( A ^ I )) → NTrans I A (FObj (KI I) a0) b
-lim-ε a0 t0 lim b = {!!} 
+limit2adjoint : 
+     ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 )
+     → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 :  ( b : Functor I A ) → NTrans I A ( K I (a0 b) ) b )
+     →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) )  ( λ b → T0 ( lim b {a0 b} {t0 b} ) )
+limit2adjoint lim a0 t0 = record {
+       _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ;
+       iscoUniversalMapping = record {
+           couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; 
+           couniquness = λ {b a f g } → couniquness1 {b} {a} {f} {g}
+       }
+  } where
+   couniversalMapping1 :  {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} →
+        A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ]
+   couniversalMapping1 {b} {a} {f} {i} = let  open ≈-Reasoning (A) in begin
+            TMap (T0 (lim b {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i 
+        ≈⟨⟩
+            TMap (t0 b) i o (limit (lim b) a f)
+        ≈⟨ t0f=t (lim b) ⟩
+            TMap f i  -- i comes from   ∀{i} → B [ TMap f i  ≈  TMap g i  ]
+        ∎
+   couniquness1 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (A0 (lim b {a0 b} {t0 b} ))} →
+        A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b} ) o FMap (KI I) g ] ≈ f ] → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ]
+   couniquness1 {b} {a} {f} {g} lim-g=f =  let  open ≈-Reasoning (A) in begin
+            limit (lim b {a0 b} {t0 b} ) a f
+        ≈⟨ limit-uniqueness ( lim b ) ? lim-g=f ⟩
+            g
+        ∎
 
-limit2adjoint : ( a0 : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) 
-     ( lim : Limit I Γ a0 t0 ) →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → a0 ) (lim-ε a0 t0 lim)
-limit2adjoint a0 t0 lim = record {
-       _*' = λ {b} {a} k → limit lim a ? ;
-       iscoUniversalMapping = record {
-           couniversalMapping = {!!} ; 
-           couniquness = {!!}
-       }
-  }