Mercurial > hg > Members > kono > Proof > category

changeset 796:472a615c6e09 ccc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Apr 2019 05:12:42 +0900
parents 030c5b87ed78
children 6a47f0030adf
files limit-to.agda
diffstat 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₁)