Mercurial > hg > Members > kono > Proof > category

diff pullback.agda @ 693:984518c56e96

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Nov 2017 12:39:30 +0900
parents 3ca3b5a4ab45
children 6b4bd02efd80
line wrap: on
line diff
--- a/pullback.agda	Sun Nov 12 10:01:06 2017 +0900
+++ b/pullback.agda	Mon Nov 13 12:39:30 2017 +0900
@@ -240,8 +240,7 @@
        U = λ b → a0 ( lim b) ;
        ε = λ b → t0 (lim b) ;
        _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; 
-       iscoUniversalMapping = record {
-           couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
+       iscoUniversalMapping = record { couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
            couniquness = couniquness2
        }
   } where
@@ -263,8 +262,6 @@
             g
         ∎
 
-open import Category.Cat
-
 univ2limit :
      ( univ :   coUniversalMapping A (A ^ I) (KI I) ) →
      ( Γ : Functor I A ) →   Limit I A Γ