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

comparison OPair.agda @ 365:7f919d6b045b

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 Sat, 18 Jul 2020 12:29:38 +0900
parents aad9249d1e8f
children f74681db63c7
comparison
equal deleted inserted replaced
364:67580311cc8e 365:7f919d6b045b
25 open _∧_ 25 open _∧_
26 open _∨_ 26 open _∨_
27 open Bool 27 open Bool
28 28
29 open _==_ 29 open _==_
30
31 _=h=_ : (x y : HOD) → Set n
32 x =h= y = od x == od y
33 30
34 <_,_> : (x y : HOD) → HOD 31 <_,_> : (x y : HOD) → HOD
35 < x , y > = (x , x ) , (x , y ) 32 < x , y > = (x , x ) , (x , y )
36 33
37 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x ) 34 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )