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

comparison 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
comparison
equal deleted inserted replaced
273:9ccf8514c323 274:29a85a427ed2
314 ; union← = union← 314 ; union← = union←
315 ; empty = empty 315 ; empty = empty
316 ; power→ = power→ 316 ; power→ = power→
317 ; power← = power← 317 ; power← = power←
318 ; extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 318 ; extensionality = λ {A} {B} {w} → extensionality {A} {B} {w}
319 -- ; ε-induction = {!!} 319 ; ε-induction = ε-induction
320 ; infinity∅ = infinity∅ 320 ; infinity∅ = infinity∅
321 ; infinity = infinity 321 ; infinity = infinity
322 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} 322 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
323 ; replacement← = replacement← 323 ; replacement← = replacement←
324 ; replacement→ = replacement→ 324 ; replacement→ = replacement→
325 ; choice-func = choice-func 325 -- ; choice-func = choice-func
326 ; choice = choice 326 -- ; choice = choice
327 } where 327 } where
328 328
329 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) 329 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
330 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x )) 330 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x ))
331 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y )) 331 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y ))