Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff src/HODBase.agda @ 1464:484f83b04b5d default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Jan 2024 19:29:23 +0900
parents 76df157f6a3f
children
line wrap: on
line diff
--- a/src/HODBase.agda	Wed Jan 03 11:05:21 2024 +0900
+++ b/src/HODBase.agda	Wed Jan 03 19:29:23 2024 +0900
@@ -100,3 +100,14 @@
   &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → (& x) ≡ (& y)
 
+==-Setoid : Setoid (suc n) n
+==-Setoid = record { _≈_ = λ x y → od x == od y ; Carrier = HOD 
+   ; isEquivalence = record { refl = ==-refl ; sym = ==-sym ; trans = ==-trans } }
+
+-- use as open 
+-- import Relation.Binary.EqReasoning as EqR
+-- open EqR ==-Setoid
+
+
+
+