Mercurial > hg > Members > kono > Proof > category

diff freyd2.agda @ 663:855e497a9c8f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
introducd HeterogeneousEquality https://stackoverflow.com/questions/44456608/two-fields-record-congruence-in-agda
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Oct 2017 22:42:56 +0900
parents e1d54c0f73a7
children fb9fc9652c04
line wrap: on
line diff
--- a/freyd2.agda	Sat Aug 12 16:35:58 2017 +0900
+++ b/freyd2.agda	Sun Oct 22 22:42:56 2017 +0900
@@ -368,9 +368,9 @@
 
 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
-     ( i :  (b : Obj B) → Obj ( K B A b ↓ U) )
+     (i :  (b : Obj B) → Obj ( K B A b ↓ U) )
      (In :  (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) 
-     (LP :  LimitPreserve A I B U  ) where
+        where
 
    tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))
    tmap-η  y = hom (i y)