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

comparison README.md @ 431:a5f8084b8368

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganiztion for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 10:23:37 +0900
parents 5e22b23ee3fd
children 42000f20fdbe
comparison
equal deleted inserted replaced
430:28c7be8f252c 431:a5f8084b8368
76 ``` 76 ```
77 _∋_ : ( A x : HOD ) → Set n 77 _∋_ : ( A x : HOD ) → Set n
78 _∋_ A x = def (od A) ( od→ord x ) 78 _∋_ A x = def (od A) ( od→ord x )
79 79
80 ``` 80 ```
81 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then 81 In ψ : Ordinal → Set, if A is a record { od = { def = λ x → ψ x } ...} , then
82 82
83 A x = def A ( od→ord x ) = ψ (od→ord x) 83 A ∋ x = def (od A) ( od→ord x ) = ψ (od→ord x)
84 84
85 They say the existing of the mappings can be proved in Classical Set Theory, but we 85 They say the existing of the mappings can be proved in Classical Set Theory, but we
86 simply assumes these non constructively. 86 simply assumes these non constructively.
87 87