# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1620435874 -32400
# Node ID 849f85e543f1a8cb2e164209f04e703628c27939
# Parent  4e58611b1fb149d3468c2886f7a7a137ea92b270
char-cong

diff -r 4e58611b1fb1 -r 849f85e543f1 src/CCC.agda
--- a/src/CCC.agda	Thu Apr 29 11:16:18 2021 +0900
+++ b/src/CCC.agda	Sat May 08 10:04:34 2021 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Category
 module CCC where
@@ -206,15 +207,40 @@
 
 open Mono
 
+iso-mono :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {m : Hom A a b}  ( mono : Mono A m ) (i : Iso A a c ) → Mono A (A [ m o Iso.≅← i ] )
+iso-mono A {a} {b} {c} {m} mono i = record { isMono = λ {d} f g → im  f g } where
+     im : {d : Obj A} (f g : Hom A d c ) →   A [ A [ A [ m o Iso.≅← i ]  o f ] ≈ A [  A [ m o Iso.≅← i ] o g ] ] → A [ f ≈ g ]
+     im {d} f g mf=mg = begin
+       f ≈↑⟨ idL ⟩
+       id1 A _  o f ≈↑⟨ car (Iso.iso← i)  ⟩
+       ( Iso.≅→ i o Iso.≅← i) o f ≈↑⟨ assoc ⟩
+        Iso.≅→ i o (Iso.≅← i  o f) ≈⟨ cdr ( Mono.isMono mono _ _ (if=ig mf=mg) ) ⟩
+        Iso.≅→ i o (Iso.≅← i  o g) ≈⟨ assoc ⟩
+       ( Iso.≅→ i o Iso.≅← i) o g ≈⟨ car (Iso.iso← i) ⟩
+       id1 A _  o g ≈⟨ idL ⟩
+       g ∎  where
+          open ≈-Reasoning A
+          if=ig : ( m o Iso.≅← i ) o f  ≈ ( m o Iso.≅← i ) o g  →  m o (Iso.≅← i o f ) ≈  m o ( Iso.≅← i o g ) 
+          if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) ) 
+
+
 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) 
         ( Ω : Obj A )
         ( ⊤ : Hom A (CCC.１ c) Ω )
         (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ]))
         (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
-         char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  (m :  Hom A b a) → (mono : Mono A m)  
+         char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  
              → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
+         char-cong  : {a b : Obj A } { m m' :  Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
+             → A [ m  ≈  m'  ] → A [ char m mono ≈ char m' mono'  ]
          ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ])
+     char-iso  : {a b c : Obj A } {m : Hom A a b}  {h : Hom A  b Ω}( mono : Mono A m ) → ( i : Iso A a (equalizer-c (Ker h))  )
+             → A [ char (A [ m o Iso.≅← i ]) (iso-mono A mono i) ≈ h ]
+     char-iso  {a} {b} {c} {m} {h} mono i = begin
+            char ( m o Iso.≅← i ) (iso-mono A mono i) ≈⟨ char-cong {!!} ⟩
+            char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h) }) ≈⟨ char-uniqueness {b} {a} {h} ⟩
+            h ∎  where   open ≈-Reasoning A
      ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
      ker h = equalizer (Ker h)
      char-m=⊤ :  {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m) → A [ A [ char m mono  o m ] ≈ A [ ⊤ o CCC.○ c b ] ]
diff -r 4e58611b1fb1 -r 849f85e543f1 src/CCCSets.agda
--- a/src/CCCSets.agda	Thu Apr 29 11:16:18 2021 +0900
+++ b/src/CCCSets.agda	Sat May 08 10:04:34 2021 +0900
@@ -136,7 +136,7 @@
       ;  Ker = tker
       ;  char = λ m mono → tchar m mono
       ;  isTopos = record {
-                 char-uniqueness  = λ {a} {b} {h} m mono →  extensionality Sets ( λ x → uniq h m mono x )
+                 char-uniqueness  = λ {a} {b} {h} →  extensionality Sets ( λ x → uniq h x )
               ;  ker-m = λ m mono → equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) 
          }
     } where
@@ -165,9 +165,9 @@
         ... | case2 f = false
         -- imequ   : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true ) o CCC.○ sets a ])
         -- imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono)
-        uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) →
+        uniq : {a : Obj (Sets {c})}  (h : Hom Sets a Bool)   (y : a) →
                tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y
-        uniq {a} {b} h m mono y with h y  | inspect h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y
+        uniq {a}  h y with h y  | inspect h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y
         ... | true  | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1 
         ... | true  | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy)))
         ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq })
diff -r 4e58611b1fb1 -r 849f85e543f1 src/ToposIL.agda
--- a/src/ToposIL.agda	Thu Apr 29 11:16:18 2021 +0900
+++ b/src/ToposIL.agda	Sat May 08 10:04:34 2021 +0900
@@ -104,37 +104,34 @@
      _⊢_  {a} {b}  p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙  h  ≈  (Topos.⊤ t) ∙  ○  c  ]
          → A [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
 --
---     iso          ○ b
---  e ⇐====⇒  b -----------→ 1     
+--     iso          ○ c
+--  e ⇐====⇒  c -----------→ 1     
 --  |         |              |
 --  |       h |              | ⊤
 --  |         ↓    char h    ↓    
---  + ------→ 1 -----------→ Ω    
+--  + ------→ b -----------→ Ω    
 --     ker h       fp / fq
 --
-     tl01 : {a b : Obj A}  (p : Poly a  (Topos.Ω t) b ) (q : Poly a  (Topos.Ω t) b )
+     tl01 : {a b : Obj A}  (p q : Poly a  (Topos.Ω t) b ) 
         → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
      tl01 {a} {b} p q p<q q<p = begin
           Poly.f p ≈↑⟨ tt p ⟩
           char t (equalizer (Ker t (Poly.f p))) (mm p)  ≈⟨   {!!} ⟩
           char t (equalizer (Ker t (Poly.f q))) (mm q)  ≈⟨   tt q ⟩
           Poly.f q ∎  where
-        ek : (h : Hom A (equalizer-c (Ker t (Poly.f p))) (equalizer-c (Ker t (Poly.f q))) )
-            → A [ IsEqualizer.k (Equalizer.isEqualizer (Ker t (Poly.f p))) (equalizer (Ker t (Poly.f q)) ∙ h) {!!} ≈  id1 A _ ]
-        ek = {!!}
         pm : {c : Obj A} (h : Hom A c b ) → A [   Poly.f p ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] → A [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
         pm h = p<q h
         qm : {c : Obj A} (h : Hom A c b ) → A [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] → A [   Poly.f p ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
         qm h = q<p h
-        idmono : {a : Obj A } → Mono A (id1 A a)
-        idmono = record { isMono = λ f g eq → trans-hom ( trans-hom (sym idL) eq ) idL }
         pp : Hom A b (Topos.Ω t)
         pp =  Poly.f q
         open import equalizer using ( monic )
+        ee : A [ equalizer (Ker t (Poly.f p)) ∙ {!!} ≈ equalizer (Ker t (Poly.f q  ))  ]
+        ee = IsEqualizer.ek=h (Equalizer.isEqualizer (Ker t (Poly.f p))) {{!!}} {{!!}} {{!!}} 
         mm : (q : Poly a  (Topos.Ω t) b ) → Mono A  (equalizer (Ker t (Poly.f q)))
         mm q = record { isMono = λ f g →  monic (Ker t (Poly.f q)) }
         tt :  (q : Poly a  (Topos.Ω t) b ) → A [ char t (equalizer (Ker t (Poly.f q))) (mm q) ≈  Poly.f q ]
-        tt q = IsTopos.char-uniqueness (Topos.isTopos t) {b} (equalizer (Ker t (Poly.f q))) (mm q)
+        tt q = IsTopos.char-uniqueness (Topos.isTopos t) {b} {a} 
 
   module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P) (t : Topos A c) where
      open InternalLanguage il
diff -r 4e58611b1fb1 -r 849f85e543f1 src/cat-utility.agda
--- a/src/cat-utility.agda	Thu Apr 29 11:16:18 2021 +0900
+++ b/src/cat-utility.agda	Sat May 08 10:04:34 2021 +0900
@@ -22,36 +22,8 @@
                  iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
                  iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]
 
-        record IsoR  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
-                 {a b c : Obj C }
-                 ( f :  Hom C a b )
-                 ( g :  Hom C a c )
-                : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
-           field
-                 iso-R   : Iso C b c
-                 iso≈R  :  C [ C [ Iso.≅→ iso-R  o f  ] ≈  g ]
-           R≈iso  :  C [ C [ Iso.≅← iso-R o g ] ≈  f ]
-           R≈iso  = begin  Iso.≅← iso-R o g ≈↑⟨ cdr iso≈R ⟩
-                Iso.≅← iso-R  o (Iso.≅→ iso-R o f) ≈⟨ assoc ⟩
-                (Iso.≅← iso-R  o Iso.≅→ iso-R ) o f ≈⟨ car (Iso.iso→ iso-R ) ⟩
-                id1 C _  o f  ≈⟨ idL ⟩
-                f ∎  where open ≈-Reasoning C
-
-        record IsoL  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
-                 {a b c : Obj C }
-                 ( f :  Hom C b a )
-                 ( g :  Hom C c a )
-                : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
-           field
-                 iso-L   : Iso C b c
-                 iso≈L  :  C [ C [ f o Iso.≅← iso-L ] ≈  g ]
-           L≈iso  :  C [ C [ g o Iso.≅→ iso-L ] ≈  f ]
-           L≈iso  = begin  g o Iso.≅→ iso-L ≈↑⟨ car iso≈L ⟩
-                (f o Iso.≅← iso-L ) o Iso.≅→ iso-L ≈↑⟨ assoc ⟩
-                f  o (Iso.≅← iso-L  o Iso.≅→ iso-L ) ≈⟨ cdr (Iso.iso→ iso-L ) ⟩
-                f  o id1 C _ ≈⟨ idR ⟩
-                f ∎  where open ≈-Reasoning C
-
+        ≡-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (x : Obj C ) → Iso C x x
+        ≡-iso C x = record { ≅→ = id1 C _ ; ≅← = id1 C _ ; iso→  = ≈-Reasoning.idL C ; iso←  =  ≈-Reasoning.idL C }
 
         record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                          ( U : Functor B A )
diff -r 4e58611b1fb1 -r 849f85e543f1 src/equalizer.agda
--- a/src/equalizer.agda	Thu Apr 29 11:16:18 2021 +0900
+++ b/src/equalizer.agda	Sat May 08 10:04:34 2021 +0900
@@ -115,16 +115,18 @@
 --         c'
 
 equalizer+iso : {a b c' : Obj A } {f g : Hom A a b } →
-                ( eqa : Equalizer A f g ) →
-                (h-1 : Hom A c' (equalizer-c eqa) ) → (h : Hom A (equalizer-c eqa) c' ) →
-                A [ A [ h o h-1 ]  ≈ id1 A c' ] → A [ A [ h-1  o h ]  ≈ id1 A (equalizer-c eqa) ] 
-           → IsEqualizer A (A [ equalizer eqa  o h-1  ] ) f g
-equalizer+iso  {a} {b} {c'} {f} {g} eqa h-1 h  hh-1=1 h-1h=1  =  record {
+                ( eqa : Equalizer A f g ) → (iso : Iso A c' (equalizer-c eqa) )
+           → IsEqualizer A (A [ equalizer eqa  o Iso.≅→ iso ] ) f g   -- h-1
+equalizer+iso  {a} {b} {c'} {f} {g} eqa iso =  record {
       fe=ge = fe=ge1 ;
       k = λ j eq → A [ h o k (isEqualizer eqa) j eq ] ;
       ek=h = ek=h1 ;
       uniqueness = uniqueness1
   } where
+      h-1 : Hom A c' (equalizer-c eqa)
+      h-1 = Iso.≅→ iso
+      h : Hom A (equalizer-c eqa) c' 
+      h =  Iso.≅← iso
       e = equalizer eqa
       fe=ge1 :  A [ A [ f o  A [ e  o h-1  ]  ]  ≈ A [ g o  A [ e  o h-1  ]  ] ]
       fe=ge1 = f1=gh ( fe=ge (isEqualizer eqa) )
@@ -137,7 +139,7 @@
                     e o ( h-1  o ( h  o k (isEqualizer eqa) j eq  ) )
              ≈⟨ cdr assoc ⟩
                     e o (( h-1  o  h)  o k (isEqualizer eqa) j eq  ) 
-             ≈⟨ cdr (car h-1h=1 )  ⟩
+             ≈⟨ cdr (car ( Iso.iso← iso) )  ⟩
                     e o (id1 A (equalizer-c eqa)  o k (isEqualizer eqa) j eq  ) 
              ≈⟨ cdr idL  ⟩
                     e o  k (isEqualizer eqa) j eq  
@@ -160,7 +162,7 @@
                    h o  ( h-1 o j )
              ≈⟨ assoc  ⟩
                    (h o   h-1 ) o j 
-             ≈⟨ car hh-1=1  ⟩
+             ≈⟨ car (Iso.iso→ iso)  ⟩
                    id c' o j 
              ≈⟨ idL ⟩
                    j
@@ -168,55 +170,53 @@
 
 
 equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g )
-   → (m :  Hom A c a) 
-   → ( ker-iso : IsoL A m (equalizer equ) )
+   → (m :  Hom A c a) → ( iso : Iso A c (equalizer-c equ))
+   → ( mm : A [ A [ equalizer equ o Iso.≅→ iso ] ≈  m ] ) 
    → IsEqualizer A m f g
-equalizerIso {a} {b} {c} f g equ m ker-iso = record {
+equalizerIso {a} {b} {c} f g equ m iso mm = record {
      fe=ge = fe-ge
-   ; k = λ {d} h eq  → A [ Iso.≅← (IsoL.iso-L ker-iso) o  IsEqualizer.k (Equalizer.isEqualizer equ) h eq  ]
+   ; k = λ {d} h eq  → A [ Iso.≅← iso o  IsEqualizer.k (Equalizer.isEqualizer equ) h eq  ]
    ; ek=h = ek=h1
    ; uniqueness = uniqueness1 } where
      ker : Hom A ( equalizer-c equ ) a
      ker  = equalizer equ
-     mm : A [ A [ equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso ) ] ≈  m ]
-     mm = IsoL.L≈iso  ker-iso 
      fe-ge : A [ A [ f o m ] ≈ A [ g o m ] ]
      fe-ge = begin
         f o m ≈↑⟨ cdr mm ⟩
-        f o (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) ≈⟨ assoc ⟩
-        (f o equalizer equ) o Iso.≅→ (IsoL.iso-L ker-iso) ≈⟨ car ( IsEqualizer.fe=ge (Equalizer.isEqualizer equ) )  ⟩
-        (g o equalizer equ ) o Iso.≅→ (IsoL.iso-L ker-iso) ≈↑⟨ assoc ⟩
-        g o (equalizer equ  o Iso.≅→ (IsoL.iso-L ker-iso)) ≈⟨ cdr mm  ⟩
+        f o (equalizer equ o Iso.≅→ iso) ≈⟨ assoc ⟩
+        (f o equalizer equ) o Iso.≅→ iso ≈⟨ car ( IsEqualizer.fe=ge (Equalizer.isEqualizer equ) )  ⟩
+        (g o equalizer equ ) o Iso.≅→ iso ≈↑⟨ assoc ⟩
+        g o (equalizer equ  o Iso.≅→ iso) ≈⟨ cdr mm  ⟩
         g o m ∎  where   open ≈-Reasoning A 
      ek=h1 : {d : Obj A} {h : Hom A d a}
            {eq : A [ A [ f o h ] ≈ A [ g o h ] ]} →
-            A [ A [ m o (A Category.o Iso.≅← (IsoL.iso-L ker-iso)) (IsEqualizer.k (isEqualizer equ) h eq) ] ≈ h ]
+            A [ A [ m o (A Category.o Iso.≅← iso) (IsEqualizer.k (isEqualizer equ) h eq) ] ≈ h ]
      ek=h1  {d} {h} {eq} = begin
-            m o (  Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ car mm ⟩
-            (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) o (  Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ assoc ⟩
-            _ o (Iso.≅→ (IsoL.iso-L ker-iso) o (  Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq )) ≈⟨ cdr assoc ⟩
-            equalizer equ o ((Iso.≅→ (IsoL.iso-L ker-iso) o   Iso.≅← (IsoL.iso-L ker-iso)) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈⟨ cdr (car (Iso.iso←  (IsoL.iso-L ker-iso))) ⟩
+            m o (  Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ car mm ⟩
+            (equalizer equ o Iso.≅→ iso) o (  Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ assoc ⟩
+            _ o (Iso.≅→ iso o (  Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h eq )) ≈⟨ cdr assoc ⟩
+            equalizer equ o ((Iso.≅→ iso o   Iso.≅← iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈⟨ cdr (car (Iso.iso←  iso)) ⟩
             equalizer equ o (id1 A _ o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈⟨ cdr idL ⟩
             equalizer equ o IsEqualizer.k (Equalizer.isEqualizer equ) h eq  ≈⟨ IsEqualizer.ek=h (isEqualizer equ) ⟩
             h ∎  where   open ≈-Reasoning A
      uniqueness1 : {d : Obj A} {h : Hom A d a}
             {eq : A [ A [ f o h ] ≈ A [ g o h ] ]}
             {k' : Hom A d c} → A [ A [ m o k' ] ≈ h ]
-               → A [ (A Category.o Iso.≅← (IsoL.iso-L ker-iso)) (IsEqualizer.k (isEqualizer equ) h eq) ≈ k' ]
+               → A [ (A Category.o Iso.≅← iso) (IsEqualizer.k (isEqualizer equ) h eq) ≈ k' ]
      uniqueness1  {d} {h} {eq} {k'} eqk = begin
-            Iso.≅← (IsoL.iso-L ker-iso)  o  (IsEqualizer.k (isEqualizer equ) h eq) ≈⟨ cdr ( IsEqualizer.uniqueness (Equalizer.isEqualizer equ) (  begin
-             equalizer equ o ((Iso.≅→ (IsoL.iso-L ker-iso))  o k' ) ≈⟨ assoc  ⟩
-             (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso))  o k'  ≈⟨ car mm  ⟩
+            Iso.≅← iso  o  (IsEqualizer.k (isEqualizer equ) h eq) ≈⟨ cdr ( IsEqualizer.uniqueness (Equalizer.isEqualizer equ) (  begin
+             equalizer equ o ((Iso.≅→ iso)  o k' ) ≈⟨ assoc  ⟩
+             (equalizer equ o Iso.≅→ iso)  o k'  ≈⟨ car mm  ⟩
              m o k' ≈⟨ eqk  ⟩
              h ∎ ))   ⟩
-            Iso.≅← (IsoL.iso-L ker-iso) o ( Iso.≅→ (IsoL.iso-L ker-iso) o k' ) ≈⟨ assoc ⟩
-            (Iso.≅← (IsoL.iso-L ker-iso) o  Iso.≅→ (IsoL.iso-L ker-iso) ) o k'  ≈⟨ car (Iso.iso→  (IsoL.iso-L ker-iso) )⟩
+            Iso.≅← iso o ( Iso.≅→ iso o k' ) ≈⟨ assoc ⟩
+            (Iso.≅← iso o  Iso.≅→ iso ) o k'  ≈⟨ car (Iso.iso→  iso )⟩
             id1 A _ o k' ≈⟨  idL ⟩
             k' ∎  where   open ≈-Reasoning A
      mequ : Equalizer A f g
      mequ = record { equalizer-c = c ; equalizer =  m ; isEqualizer = record {
            fe=ge = fe-ge 
-         ; k = λ {d} h fh=gh → A [ Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h fh=gh ]
+         ; k = λ {d} h fh=gh → A [ Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h fh=gh ]
          ; ek=h = ek=h1 
          ; uniqueness = uniqueness1 
          } }