diff OD.agda @ 226:176ff97547b4

set theortic function definition using sup
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2019 13:05:17 +0900
parents 2e1f19c949dc
children 49736efc822b
line wrap: on
line diff
--- a/OD.agda	Sun Aug 11 08:10:13 2019 +0900
+++ b/OD.agda	Sun Aug 11 13:05:17 2019 +0900
@@ -477,3 +477,9 @@
          choice : (X : OD  ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimul A not
 
+_,_ = ZF._,_ OD→ZF
+Union = ZF.Union OD→ZF
+Power = ZF.Power OD→ZF
+Select = ZF.Select OD→ZF
+Replace = ZF.Replace OD→ZF
+isZF = ZF.isZF  OD→ZF