### changeset 796:472a615c6e09ccc

fix
author Shinji KONO Tue, 23 Apr 2019 05:12:42 +0900 030c5b87ed78 6a47f0030adf limit-to.agda 1 files changed, 5 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
```--- 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₁) ```