# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1472378380 -32400
# Node ID 9f014f34b988cb2f86de56a32ab92c1089b0d4da
# Parent  3fdf0aedc21d931fa5e0c8ec3257f09e6976fc23
f=g if equalizer k has right inverse

diff -r 3fdf0aedc21d -r 9f014f34b988 freyd.agda
--- a/freyd.agda	Sun Mar 27 09:18:01 2016 +0900
+++ b/freyd.agda	Sun Aug 28 18:59:40 2016 +0900
@@ -35,8 +35,6 @@
       initial :  ∀( a : Obj A ) →  Hom A i a
       uniqueness  : ( a : Obj A ) →  ( f : Hom A i a ) → A [ f ≈  initial a ]
 
-
-
 -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory
 
 open NTrans
@@ -47,10 +45,11 @@
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
       (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
+      ( equ : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g )
       (SFS : SmallFullSubcategory A F FMap← ) → 
       (PI : PreInitial A F ) → { a0 : Obj A } → { u : (a : Obj A) → NTrans A A (K A A a) F }
           → HasInitialObject A a0
-initialFromPreInitialFullSubcategory A F  FMap← lim SFS PI {a0} {u} = record {
+initialFromPreInitialFullSubcategory A F  FMap← lim equ SFS PI {a0} {u} = record {
       initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f
     } where
@@ -66,4 +65,26 @@
              ≈⟨ {!!} ⟩
                  f
              ∎  )
-
+      -- if equalizer has right inverse, f = g
+      lemma2 :  (a b c : Obj A) ( f g : Hom A a b ) (e : Hom A c a ) (e' : Hom A a c ) ( equ : Equalizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] )
+           -> A [ f ≈ g ]
+      lemma2 a b c f g e e' equ inv-e = let open ≈-Reasoning (A) in
+            let open Equalizer in
+            begin
+                f
+               ≈↑⟨ idR ⟩
+                 f o  id1 A a 
+               ≈↑⟨ cdr inv-e ⟩
+                 f o  (  e o e'  ) 
+               ≈⟨ assoc  ⟩
+                 ( f o  e ) o e'  
+               ≈⟨ car ( fe=ge equ ) ⟩
+                 ( g o  e ) o e'  
+               ≈↑⟨ assoc  ⟩
+                 g o  (  e o e'  ) 
+               ≈⟨ cdr inv-e   ⟩
+                 g o  id1 A a
+               ≈⟨ idR ⟩
+                g
+            ∎
+