# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1379901459 -32400
# Node ID 7ae58263d45b7aecea53d1d80fe68113a4a46076
# Parent  8df8e74e63167c5c6d979080674975e2de6c4452
univ2limit done.

diff -r 8df8e74e6316 -r 7ae58263d45b pullback.agda
--- 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 = {!!}