# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1555963962 -32400
# Node ID 472a615c6e092e884425dca8a7545bbae552027a
# Parent  030c5b87ed78375d666f25a6f25588f17157c94c
fix

diff -r 030c5b87ed78 -r 472a615c6e09 limit-to.agda
--- a/limit-to.agda	Mon Apr 22 18:00:03 2019 +0900
+++ b/limit-to.agda	Tue Apr 23 05:12:42 2019 +0900
@@ -6,6 +6,8 @@
 open import cat-utility
 open import HomReasoning
 open import Relation.Binary.Core
+open  import  Relation.Binary.PropositionalEquality hiding ([_])
+
 
 open import discrete
 
@@ -59,7 +61,7 @@
           fmap  {t0} {t1} arrow-f = f
           fmap  {t0} {t1} arrow-g = g
           ≈-cong :  {a : Obj T} {b : Obj T} {f g : Hom T a b}  → T [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
-          ≈-cong  {a} {b} {f} {.f} refl = let open  ≈-Reasoning A in refl-hom
+          ≈-cong  {a} {b} {f} {_} refl = let open  ≈-Reasoning A in refl-hom
           identity : (x : Obj T ) →  A [ fmap (id1 T x) ≈  id1 A (fobj x) ]
           identity t0  = let open  ≈-Reasoning A in refl-hom
           identity t1  = let open  ≈-Reasoning A in refl-hom
@@ -242,6 +244,8 @@
 
 ---  Product  from Limit ( given Discrete→A functor Γ and  pnat :  K →　Γ)
 
+open  import  Relation.Binary.PropositionalEquality
+
 open DiscreteHom
 
 plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set  c₁)