# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1458798589 -32400
# Node ID 98811e927d4a723b044e208d24dee06a7c54c3ff
# Parent  4329525f5085ab24116eb912eef06a55157806ed
define MA and I

diff -r 4329525f5085 -r 98811e927d4a limit-to.agda
--- a/limit-to.agda	Thu Mar 24 14:12:53 2016 +0900
+++ b/limit-to.agda	Thu Mar 24 14:49:49 2016 +0900
@@ -386,14 +386,14 @@
 
 open Limit
 
-I :  {c₁ c₂ ℓ : Level} ->  Category   c₁  c₂  c₂
-I {c₁} {c₂} {ℓ} = TwoCat {c₁} {c₂} {ℓ}
-MA :  {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } ->  Category   c₁ (ℓ ⊔ c₂)  (ℓ ⊔ c₂)
-MA {c₁} {c₂} {ℓ} {A} = MaybeCat A
+I' :  {c₁ c₂ ℓ : Level} ->  Category   c₁  c₂  c₂
+I' {c₁} {c₂} {ℓ} = TwoCat {c₁} {c₂} {ℓ}
+MA' :  {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } ->  Category   c₁ (ℓ ⊔ c₂)  (ℓ ⊔ c₂)
+MA' {c₁} {c₂} {ℓ} {A} = MaybeCat A
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  
-      (lim :  ( Γ : Functor (I {c₁} {c₂} {ℓ}) (MA {c₁} {c₂} {ℓ} {A})  ) → {a0 : Obj A } 
-               {u : NTrans I MA ( K MA  I a0 )  Γ } → Limit MA I Γ a0 u ) -- completeness
+      (lim :  ( Γ : Functor (I' {c₁} {c₂} {ℓ}) (MA' {c₁} {c₂} {ℓ} {A})  ) → {a0 : Obj A } 
+               {u : NTrans I' MA' ( K MA'  I' a0 )  Γ } → Limit MA' I' Γ a0 u ) -- completeness
         →  {a b c : Obj A}      (f g : Hom A  a b )
         → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
 lim-to-equ  {c₁} {c₂} {ℓ } A  lim {a} {b} {c}  f g e fe=ge = record {
@@ -402,10 +402,14 @@
         ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
      } where
+         MA = MA'   {c₁} {c₂} {ℓ} {A}
+         I = I'   {c₁} {c₂} {ℓ} 
+         mf : Hom MA a b
          mf = record { hom = just f }
+         mg : Hom MA a b
          mg = record { hom = just g }
          Γ = indexFunctor  {c₁} {c₂} {ℓ} A  a b f g
-         nmap :  (x : Obj (I {c₁} {c₂} {ℓ}) ) ( d : Obj (MA  {c₁} {c₂} {ℓ} {A})  ) (h : Hom MA d a ) -> Hom MA (FObj (K MA I d) x) (FObj Γ x)
+         nmap :  (x : Obj I ) ( d : Obj (MA)  ) (h : Hom MA d a ) -> Hom MA (FObj (K MA I d) x) (FObj Γ x)
          nmap x d h = {!!}
          commute1 : {x y : Obj I}  {f' : Hom I x y} (d : Obj MA) (h : Hom MA d a ) ->  MA [ MA [ mf  o  h ] ≈ MA [ mg  o h ] ]
                  → MA [ MA [ FMap Γ f' o nmap x d h ] ≈ MA [ nmap y d h o FMap (K MA I d) f' ] ]