Mercurial > hg > Members > kono > Proof > category
diff SetsCompleteness.agda @ 781:340708e8d54f
fix for 2.5.4.2
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 08 Mar 2019 17:46:59 +0900 |
parents | 984518c56e96 |
children |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Oct 08 16:48:27 2018 +0900 +++ b/SetsCompleteness.agda Fri Mar 08 17:46:59 2019 +0900 @@ -13,6 +13,8 @@ ≡cong = Relation.Binary.PropositionalEquality.cong +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → Sets [ f ≈ g ] → (x : a ) → f x ≡ g x lemma1 refl x = refl