Mercurial > hg > Members > kono > Proof > category

changeset 280:7ae58263d45b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
univ2limit done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 10:57:39 +0900
parents 8df8e74e6316
children dbd2044add2a
files pullback.agda
diffstat 1 files changed, 3 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Mon Sep 23 03:31:24 2013 +0900
+++ b/pullback.agda	Mon Sep 23 10:57:39 2013 +0900
@@ -293,8 +293,8 @@
      t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
             TMap (ε Γ) i o limit1 a t
         ≈⟨⟩
-            TMap (ε Γ) i o _*' univ {{!!}} {{!!}} t
-        ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {{!!}} {{!!}} {{!!}}  ⟩
+            TMap (ε Γ) i o _*' univ {Γ} {a} t
+        ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩
             TMap t i
         ∎
      limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a (U Γ)} 
@@ -305,9 +305,6 @@
             f
         ∎
 
-
-
- 
 limit-from :  
       ( prod : (a b ab  : Obj A) ( π1 : Hom A ab a )  ( π2 : Hom A ab b ) 
                   →  Product A a b ab π1 π2 ) 
@@ -317,4 +314,4 @@
      ( U : Obj (A ^ I ) → Obj A ) 
      ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K I (U b)) b ) →
      ( Γ : Functor I A ) →   Limit I Γ (U Γ) (ε Γ)
-limit-from = ?
+limit-from proc eqa = {!!}