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

diff OD.agda @ 274:29a85a427ed2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ε-induction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 Apr 2020 15:09:07 +0900
parents 985a1af11bce
children 6f10c47e4e7a
line wrap: on
line diff
--- a/OD.agda	Sat Jan 11 20:11:51 2020 +0900
+++ b/OD.agda	Sat Apr 25 15:09:07 2020 +0900
@@ -316,14 +316,14 @@
        ;   power→ = power→  
        ;   power← = power← 
        ;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 
-       -- ;   ε-induction = {!!}
+       ;   ε-induction = ε-induction 
        ;   infinity∅ = infinity∅
        ;   infinity = infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement← = replacement←
        ;   replacement→ = replacement→
-       ;   choice-func = choice-func
-       ;   choice = choice
+       -- ;   choice-func = choice-func
+       -- ;   choice = choice
      } where
 
          pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y )