# HG changeset patch # User Shinji KONO # Date 1608513817 -32400 # Node ID a5f8084b8368d1d38ffe873530ab19d794badffe # Parent 28c7be8f252cd08e6ee714bf2914e7cb277cf421 reorganiztion for apkg diff -r 28c7be8f252c -r a5f8084b8368 BAlgbra.agda --- a/BAlgbra.agda Sun Dec 20 12:37:07 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,122 +0,0 @@ -open import Level -open import Ordinals -module BAlgbra {n : Level } (O : Ordinals {n}) where - -open import zf -open import logic -import OrdUtil -import OD -import ODUtil -import ODC - -open import Relation.Nullary -open import Relation.Binary -open import Data.Empty -open import Relation.Binary -open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ ) - -open inOrdinal O -open Ordinals.Ordinals O -open Ordinals.IsOrdinals isOrdinal -open Ordinals.IsNext isNext -open OrdUtil O -open ODUtil O - -open OD O -open OD.OD -open ODAxiom odAxiom -open HOD - -open _∧_ -open _∨_ -open Bool - ---_∩_ : ( A B : HOD ) → HOD ---A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; --- odmax = omin (odmax A) (odmax B) ; axiom of choice ---- -record choiced ( X : Ordinal ) : Set n where - field - a-choice : Ordinal - is-in : odef (* X) a-choice - -open choiced - --- ∋→d : ( a : HOD ) { x : HOD } → * (& a) ∋ x → X ∋ * (a-choice (choice-func X not)) --- ∋→d a lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt - -oo∋ : { a : HOD} { x : Ordinal } → odef (* (& a)) x → a ∋ * x -oo∋ lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt - -∋oo : { a : HOD} { x : Ordinal } → a ∋ * x → odef (* (& a)) x -∋oo lt = subst₂ (λ j k → odef j k ) (sym *iso) &iso lt - -OD→ZFC : ZFC -OD→ZFC = record { - ZFSet = HOD - ; _∋_ = _∋_ - ; _≈_ = _=h=_ - ; ∅ = od∅ - ; Select = Select - ; isZFC = isZFC - } where - -- infixr 200 _∈_ - -- infixr 230 _∩_ _∪_ - isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select - isZFC = record { - choice-func = λ A {X} not A∋X → * (a-choice (choice-func X not) ); - choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not)) - } where - -- - -- the axiom choice from LEM and OD ordering - -- - choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (& X) - choice-func X not = have_to_find where - ψ : ( ox : Ordinal ) → Set n - ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (& X) - lemma-ord : ( ox : Ordinal ) → ψ ox - lemma-ord ox = TransFinite0 {ψ} induction ox where - ∀-imply-or : {A : Ordinal → Set n } {B : Set n } - → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B - ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM - ∀-imply-or {A} {B} ∀AB | case1 t = case1 t - ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x not )) where - lemma : ¬ ((x : Ordinal ) → A x) → B - lemma not with p∨¬p B - lemma not | case1 b = b - lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) - induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x - induction x prev with ∋-p X ( * x) - ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo p } ) - ... | no ¬p = lemma where - lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (& X) - lemma1 y with ∋-p X (* y) - lemma1 y | yes y - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - Preamble - - The GNU General Public License is a free, copyleft license for -software and other kinds of works. - - The licenses for most software and other practical works are designed -to take away your freedom to share and change the works. By contrast, -the GNU General Public License is intended to guarantee your freedom to -share and change all versions of a program--to make sure it remains free -software for all its users. We, the Free Software Foundation, use the -GNU General Public License for most of our software; it applies also to -any other work released this way by its authors. You can apply it to -your programs, too. - - When we speak of free software, we are referring to freedom, not -price. Our General Public Licenses are designed to make sure that you -have the freedom to distribute copies of free software (and charge for -them if you wish), that you receive source code or can get it if you -want it, that you can change the software or use pieces of it in new -free programs, and that you know you can do these things. - - To protect your rights, we need to prevent others from denying you -these rights or asking you to surrender the rights. Therefore, you have -certain responsibilities if you distribute copies of the software, or if -you modify it: responsibilities to respect the freedom of others. - - For example, if you distribute copies of such a program, whether -gratis or for a fee, you must pass on to the recipients the same -freedoms that you received. You must make sure that they, too, receive -or can get the source code. And you must show them these terms so they -know their rights. - - Developers that use the GNU GPL protect your rights with two steps: -(1) assert copyright on the software, and (2) offer you this License -giving you legal permission to copy, distribute and/or modify it. - - For the developers' and authors' protection, the GPL clearly explains -that there is no warranty for this free software. For both users' and -authors' sake, the GPL requires that modified versions be marked as -changed, so that their problems will not be attributed erroneously to -authors of previous versions. - - Some devices are designed to deny users access to install or run -modified versions of the software inside them, although the manufacturer -can do so. This is fundamentally incompatible with the aim of -protecting users' freedom to change the software. The systematic -pattern of such abuse occurs in the area of products for individuals to -use, which is precisely where it is most unacceptable. Therefore, we -have designed this version of the GPL to prohibit the practice for those -products. If such problems arise substantially in other domains, we -stand ready to extend this provision to those domains in future versions -of the GPL, as needed to protect the freedom of users. - - Finally, every program is threatened constantly by software patents. -States should not allow patents to restrict development and use of -software on general-purpose computers, but in those that do, we wish to -avoid the special danger that patents applied to a free program could -make it effectively proprietary. To prevent this, the GPL assures that -patents cannot be used to render the program non-free. - - The precise terms and conditions for copying, distribution and -modification follow. - - TERMS AND CONDITIONS - - 0. Definitions. - - "This License" refers to version 3 of the GNU General Public License. - - "Copyright" also means copyright-like laws that apply to other kinds of -works, such as semiconductor masks. - - "The Program" refers to any copyrightable work licensed under this -License. Each licensee is addressed as "you". "Licensees" and -"recipients" may be individuals or organizations. - - To "modify" a work means to copy from or adapt all or part of the work -in a fashion requiring copyright permission, other than the making of an -exact copy. The resulting work is called a "modified version" of the -earlier work or a work "based on" the earlier work. - - A "covered work" means either the unmodified Program or a work based -on the Program. - - To "propagate" a work means to do anything with it that, without -permission, would make you directly or secondarily liable for -infringement under applicable copyright law, except executing it on a -computer or modifying a private copy. Propagation includes copying, -distribution (with or without modification), making available to the -public, and in some countries other activities as well. - - To "convey" a work means any kind of propagation that enables other -parties to make or receive copies. Mere interaction with a user through -a computer network, with no transfer of a copy, is not conveying. - - An interactive user interface displays "Appropriate Legal Notices" -to the extent that it includes a convenient and prominently visible -feature that (1) displays an appropriate copyright notice, and (2) -tells the user that there is no warranty for the work (except to the -extent that warranties are provided), that licensees may convey the -work under this License, and how to view a copy of this License. If -the interface presents a list of user commands or options, such as a -menu, a prominent item in the list meets this criterion. - - 1. Source Code. - - The "source code" for a work means the preferred form of the work -for making modifications to it. "Object code" means any non-source -form of a work. - - A "Standard Interface" means an interface that either is an official -standard defined by a recognized standards body, or, in the case of -interfaces specified for a particular programming language, one that -is widely used among developers working in that language. - - The "System Libraries" of an executable work include anything, other -than the work as a whole, that (a) is included in the normal form of -packaging a Major Component, but which is not part of that Major -Component, and (b) serves only to enable use of the work with that -Major Component, or to implement a Standard Interface for which an -implementation is available to the public in source code form. A -"Major Component", in this context, means a major essential component -(kernel, window system, and so on) of the specific operating system -(if any) on which the executable work runs, or a compiler used to -produce the work, or an object code interpreter used to run it. - - The "Corresponding Source" for a work in object code form means all -the source code needed to generate, install, and (for an executable -work) run the object code and to modify the work, including scripts to -control those activities. However, it does not include the work's -System Libraries, or general-purpose tools or generally available free -programs which are used unmodified in performing those activities but -which are not part of the work. For example, Corresponding Source -includes interface definition files associated with source files for -the work, and the source code for shared libraries and dynamically -linked subprograms that the work is specifically designed to require, -such as by intimate data communication or control flow between those -subprograms and other parts of the work. - - The Corresponding Source need not include anything that users -can regenerate automatically from other parts of the Corresponding -Source. - - The Corresponding Source for a work in source code form is that -same work. - - 2. Basic Permissions. - - All rights granted under this License are granted for the term of -copyright on the Program, and are irrevocable provided the stated -conditions are met. This License explicitly affirms your unlimited -permission to run the unmodified Program. The output from running a -covered work is covered by this License only if the output, given its -content, constitutes a covered work. This License acknowledges your -rights of fair use or other equivalent, as provided by copyright law. - - You may make, run and propagate covered works that you do not -convey, without conditions so long as your license otherwise remains -in force. You may convey covered works to others for the sole purpose -of having them make modifications exclusively for you, or provide you -with facilities for running those works, provided that you comply with -the terms of this License in conveying all material for which you do -not control copyright. Those thus making or running the covered works -for you must do so exclusively on your behalf, under your direction -and control, on terms that prohibit them from making any copies of -your copyrighted material outside their relationship with you. - - Conveying under any other circumstances is permitted solely under -the conditions stated below. Sublicensing is not allowed; section 10 -makes it unnecessary. - - 3. Protecting Users' Legal Rights From Anti-Circumvention Law. - - No covered work shall be deemed part of an effective technological -measure under any applicable law fulfilling obligations under article -11 of the WIPO copyright treaty adopted on 20 December 1996, or -similar laws prohibiting or restricting circumvention of such -measures. - - When you convey a covered work, you waive any legal power to forbid -circumvention of technological measures to the extent such circumvention -is effected by exercising rights under this License with respect to -the covered work, and you disclaim any intention to limit operation or -modification of the work as a means of enforcing, against the work's -users, your or third parties' legal rights to forbid circumvention of -technological measures. - - 4. Conveying Verbatim Copies. - - You may convey verbatim copies of the Program's source code as you -receive it, in any medium, provided that you conspicuously and -appropriately publish on each copy an appropriate copyright notice; -keep intact all notices stating that this License and any -non-permissive terms added in accord with section 7 apply to the code; -keep intact all notices of the absence of any warranty; and give all -recipients a copy of this License along with the Program. - - You may charge any price or no price for each copy that you convey, -and you may offer support or warranty protection for a fee. - - 5. Conveying Modified Source Versions. - - You may convey a work based on the Program, or the modifications to -produce it from the Program, in the form of source code under the -terms of section 4, provided that you also meet all of these conditions: - - a) The work must carry prominent notices stating that you modified - it, and giving a relevant date. - - b) The work must carry prominent notices stating that it is - released under this License and any conditions added under section - 7. This requirement modifies the requirement in section 4 to - "keep intact all notices". - - c) You must license the entire work, as a whole, under this - License to anyone who comes into possession of a copy. This - License will therefore apply, along with any applicable section 7 - additional terms, to the whole of the work, and all its parts, - regardless of how they are packaged. This License gives no - permission to license the work in any other way, but it does not - invalidate such permission if you have separately received it. - - d) If the work has interactive user interfaces, each must display - Appropriate Legal Notices; however, if the Program has interactive - interfaces that do not display Appropriate Legal Notices, your - work need not make them do so. - - A compilation of a covered work with other separate and independent -works, which are not by their nature extensions of the covered work, -and which are not combined with it such as to form a larger program, -in or on a volume of a storage or distribution medium, is called an -"aggregate" if the compilation and its resulting copyright are not -used to limit the access or legal rights of the compilation's users -beyond what the individual works permit. Inclusion of a covered work -in an aggregate does not cause this License to apply to the other -parts of the aggregate. - - 6. Conveying Non-Source Forms. - - You may convey a covered work in object code form under the terms -of sections 4 and 5, provided that you also convey the -machine-readable Corresponding Source under the terms of this License, -in one of these ways: - - a) Convey the object code in, or embodied in, a physical product - (including a physical distribution medium), accompanied by the - Corresponding Source fixed on a durable physical medium - customarily used for software interchange. - - b) Convey the object code in, or embodied in, a physical product - (including a physical distribution medium), accompanied by a - written offer, valid for at least three years and valid for as - long as you offer spare parts or customer support for that product - model, to give anyone who possesses the object code either (1) a - copy of the Corresponding Source for all the software in the - product that is covered by this License, on a durable physical - medium customarily used for software interchange, for a price no - more than your reasonable cost of physically performing this - conveying of source, or (2) access to copy the - Corresponding Source from a network server at no charge. - - c) Convey individual copies of the object code with a copy of the - written offer to provide the Corresponding Source. This - alternative is allowed only occasionally and noncommercially, and - only if you received the object code with such an offer, in accord - with subsection 6b. - - d) Convey the object code by offering access from a designated - place (gratis or for a charge), and offer equivalent access to the - Corresponding Source in the same way through the same place at no - further charge. You need not require recipients to copy the - Corresponding Source along with the object code. If the place to - copy the object code is a network server, the Corresponding Source - may be on a different server (operated by you or a third party) - that supports equivalent copying facilities, provided you maintain - clear directions next to the object code saying where to find the - Corresponding Source. Regardless of what server hosts the - Corresponding Source, you remain obligated to ensure that it is - available for as long as needed to satisfy these requirements. - - e) Convey the object code using peer-to-peer transmission, provided - you inform other peers where the object code and Corresponding - Source of the work are being offered to the general public at no - charge under subsection 6d. - - A separable portion of the object code, whose source code is excluded -from the Corresponding Source as a System Library, need not be -included in conveying the object code work. - - A "User Product" is either (1) a "consumer product", which means any -tangible personal property which is normally used for personal, family, -or household purposes, or (2) anything designed or sold for incorporation -into a dwelling. In determining whether a product is a consumer product, -doubtful cases shall be resolved in favor of coverage. For a particular -product received by a particular user, "normally used" refers to a -typical or common use of that class of product, regardless of the status -of the particular user or of the way in which the particular user -actually uses, or expects or is expected to use, the product. A product -is a consumer product regardless of whether the product has substantial -commercial, industrial or non-consumer uses, unless such uses represent -the only significant mode of use of the product. - - "Installation Information" for a User Product means any methods, -procedures, authorization keys, or other information required to install -and execute modified versions of a covered work in that User Product from -a modified version of its Corresponding Source. The information must -suffice to ensure that the continued functioning of the modified object -code is in no case prevented or interfered with solely because -modification has been made. - - If you convey an object code work under this section in, or with, or -specifically for use in, a User Product, and the conveying occurs as -part of a transaction in which the right of possession and use of the -User Product is transferred to the recipient in perpetuity or for a -fixed term (regardless of how the transaction is characterized), the -Corresponding Source conveyed under this section must be accompanied -by the Installation Information. But this requirement does not apply -if neither you nor any third party retains the ability to install -modified object code on the User Product (for example, the work has -been installed in ROM). - - The requirement to provide Installation Information does not include a -requirement to continue to provide support service, warranty, or updates -for a work that has been modified or installed by the recipient, or for -the User Product in which it has been modified or installed. Access to a -network may be denied when the modification itself materially and -adversely affects the operation of the network or violates the rules and -protocols for communication across the network. - - Corresponding Source conveyed, and Installation Information provided, -in accord with this section must be in a format that is publicly -documented (and with an implementation available to the public in -source code form), and must require no special password or key for -unpacking, reading or copying. - - 7. Additional Terms. - - "Additional permissions" are terms that supplement the terms of this -License by making exceptions from one or more of its conditions. -Additional permissions that are applicable to the entire Program shall -be treated as though they were included in this License, to the extent -that they are valid under applicable law. If additional permissions -apply only to part of the Program, that part may be used separately -under those permissions, but the entire Program remains governed by -this License without regard to the additional permissions. - - When you convey a copy of a covered work, you may at your option -remove any additional permissions from that copy, or from any part of -it. (Additional permissions may be written to require their own -removal in certain cases when you modify the work.) You may place -additional permissions on material, added by you to a covered work, -for which you have or can give appropriate copyright permission. - - Notwithstanding any other provision of this License, for material you -add to a covered work, you may (if authorized by the copyright holders of -that material) supplement the terms of this License with terms: - - a) Disclaiming warranty or limiting liability differently from the - terms of sections 15 and 16 of this License; or - - b) Requiring preservation of specified reasonable legal notices or - author attributions in that material or in the Appropriate Legal - Notices displayed by works containing it; or - - c) Prohibiting misrepresentation of the origin of that material, or - requiring that modified versions of such material be marked in - reasonable ways as different from the original version; or - - d) Limiting the use for publicity purposes of names of licensors or - authors of the material; or - - e) Declining to grant rights under trademark law for use of some - trade names, trademarks, or service marks; or - - f) Requiring indemnification of licensors and authors of that - material by anyone who conveys the material (or modified versions of - it) with contractual assumptions of liability to the recipient, for - any liability that these contractual assumptions directly impose on - those licensors and authors. - - All other non-permissive additional terms are considered "further -restrictions" within the meaning of section 10. If the Program as you -received it, or any part of it, contains a notice stating that it is -governed by this License along with a term that is a further -restriction, you may remove that term. If a license document contains -a further restriction but permits relicensing or conveying under this -License, you may add to a covered work material governed by the terms -of that license document, provided that the further restriction does -not survive such relicensing or conveying. - - If you add terms to a covered work in accord with this section, you -must place, in the relevant source files, a statement of the -additional terms that apply to those files, or a notice indicating -where to find the applicable terms. - - Additional terms, permissive or non-permissive, may be stated in the -form of a separately written license, or stated as exceptions; -the above requirements apply either way. - - 8. Termination. - - You may not propagate or modify a covered work except as expressly -provided under this License. Any attempt otherwise to propagate or -modify it is void, and will automatically terminate your rights under -this License (including any patent licenses granted under the third -paragraph of section 11). - - However, if you cease all violation of this License, then your -license from a particular copyright holder is reinstated (a) -provisionally, unless and until the copyright holder explicitly and -finally terminates your license, and (b) permanently, if the copyright -holder fails to notify you of the violation by some reasonable means -prior to 60 days after the cessation. - - Moreover, your license from a particular copyright holder is -reinstated permanently if the copyright holder notifies you of the -violation by some reasonable means, this is the first time you have -received notice of violation of this License (for any work) from that -copyright holder, and you cure the violation prior to 30 days after -your receipt of the notice. - - Termination of your rights under this section does not terminate the -licenses of parties who have received copies or rights from you under -this License. If your rights have been terminated and not permanently -reinstated, you do not qualify to receive new licenses for the same -material under section 10. - - 9. Acceptance Not Required for Having Copies. - - You are not required to accept this License in order to receive or -run a copy of the Program. Ancillary propagation of a covered work -occurring solely as a consequence of using peer-to-peer transmission -to receive a copy likewise does not require acceptance. However, -nothing other than this License grants you permission to propagate or -modify any covered work. These actions infringe copyright if you do -not accept this License. Therefore, by modifying or propagating a -covered work, you indicate your acceptance of this License to do so. - - 10. Automatic Licensing of Downstream Recipients. - - Each time you convey a covered work, the recipient automatically -receives a license from the original licensors, to run, modify and -propagate that work, subject to this License. You are not responsible -for enforcing compliance by third parties with this License. - - An "entity transaction" is a transaction transferring control of an -organization, or substantially all assets of one, or subdividing an -organization, or merging organizations. If propagation of a covered -work results from an entity transaction, each party to that -transaction who receives a copy of the work also receives whatever -licenses to the work the party's predecessor in interest had or could -give under the previous paragraph, plus a right to possession of the -Corresponding Source of the work from the predecessor in interest, if -the predecessor has it or can get it with reasonable efforts. - - You may not impose any further restrictions on the exercise of the -rights granted or affirmed under this License. For example, you may -not impose a license fee, royalty, or other charge for exercise of -rights granted under this License, and you may not initiate litigation -(including a cross-claim or counterclaim in a lawsuit) alleging that -any patent claim is infringed by making, using, selling, offering for -sale, or importing the Program or any portion of it. - - 11. Patents. - - A "contributor" is a copyright holder who authorizes use under this -License of the Program or a work on which the Program is based. The -work thus licensed is called the contributor's "contributor version". - - A contributor's "essential patent claims" are all patent claims -owned or controlled by the contributor, whether already acquired or -hereafter acquired, that would be infringed by some manner, permitted -by this License, of making, using, or selling its contributor version, -but do not include claims that would be infringed only as a -consequence of further modification of the contributor version. For -purposes of this definition, "control" includes the right to grant -patent sublicenses in a manner consistent with the requirements of -this License. - - Each contributor grants you a non-exclusive, worldwide, royalty-free -patent license under the contributor's essential patent claims, to -make, use, sell, offer for sale, import and otherwise run, modify and -propagate the contents of its contributor version. - - In the following three paragraphs, a "patent license" is any express -agreement or commitment, however denominated, not to enforce a patent -(such as an express permission to practice a patent or covenant not to -sue for patent infringement). To "grant" such a patent license to a -party means to make such an agreement or commitment not to enforce a -patent against the party. - - If you convey a covered work, knowingly relying on a patent license, -and the Corresponding Source of the work is not available for anyone -to copy, free of charge and under the terms of this License, through a -publicly available network server or other readily accessible means, -then you must either (1) cause the Corresponding Source to be so -available, or (2) arrange to deprive yourself of the benefit of the -patent license for this particular work, or (3) arrange, in a manner -consistent with the requirements of this License, to extend the patent -license to downstream recipients. "Knowingly relying" means you have -actual knowledge that, but for the patent license, your conveying the -covered work in a country, or your recipient's use of the covered work -in a country, would infringe one or more identifiable patents in that -country that you have reason to believe are valid. - - If, pursuant to or in connection with a single transaction or -arrangement, you convey, or propagate by procuring conveyance of, a -covered work, and grant a patent license to some of the parties -receiving the covered work authorizing them to use, propagate, modify -or convey a specific copy of the covered work, then the patent license -you grant is automatically extended to all recipients of the covered -work and works based on it. - - A patent license is "discriminatory" if it does not include within -the scope of its coverage, prohibits the exercise of, or is -conditioned on the non-exercise of one or more of the rights that are -specifically granted under this License. You may not convey a covered -work if you are a party to an arrangement with a third party that is -in the business of distributing software, under which you make payment -to the third party based on the extent of your activity of conveying -the work, and under which the third party grants, to any of the -parties who would receive the covered work from you, a discriminatory -patent license (a) in connection with copies of the covered work -conveyed by you (or copies made from those copies), or (b) primarily -for and in connection with specific products or compilations that -contain the covered work, unless you entered into that arrangement, -or that patent license was granted, prior to 28 March 2007. - - Nothing in this License shall be construed as excluding or limiting -any implied license or other defenses to infringement that may -otherwise be available to you under applicable patent law. - - 12. No Surrender of Others' Freedom. - - If conditions are imposed on you (whether by court order, agreement or -otherwise) that contradict the conditions of this License, they do not -excuse you from the conditions of this License. If you cannot convey a -covered work so as to satisfy simultaneously your obligations under this -License and any other pertinent obligations, then as a consequence you may -not convey it at all. For example, if you agree to terms that obligate you -to collect a royalty for further conveying from those to whom you convey -the Program, the only way you could satisfy both those terms and this -License would be to refrain entirely from conveying the Program. - - 13. Use with the GNU Affero General Public License. - - Notwithstanding any other provision of this License, you have -permission to link or combine any covered work with a work licensed -under version 3 of the GNU Affero General Public License into a single -combined work, and to convey the resulting work. The terms of this -License will continue to apply to the part which is the covered work, -but the special requirements of the GNU Affero General Public License, -section 13, concerning interaction through a network will apply to the -combination as such. - - 14. Revised Versions of this License. - - The Free Software Foundation may publish revised and/or new versions of -the GNU General Public License from time to time. Such new versions will -be similar in spirit to the present version, but may differ in detail to -address new problems or concerns. - - Each version is given a distinguishing version number. If the -Program specifies that a certain numbered version of the GNU General -Public License "or any later version" applies to it, you have the -option of following the terms and conditions either of that numbered -version or of any later version published by the Free Software -Foundation. If the Program does not specify a version number of the -GNU General Public License, you may choose any version ever published -by the Free Software Foundation. - - If the Program specifies that a proxy can decide which future -versions of the GNU General Public License can be used, that proxy's -public statement of acceptance of a version permanently authorizes you -to choose that version for the Program. - - Later license versions may give you additional or different -permissions. However, no additional obligations are imposed on any -author or copyright holder as a result of your choosing to follow a -later version. - - 15. Disclaimer of Warranty. - - THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY -APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT -HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY -OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, -THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR -PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM -IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF -ALL NECESSARY SERVICING, REPAIR OR CORRECTION. - - 16. Limitation of Liability. - - IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING -WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS -THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY -GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE -USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF -DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD -PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), -EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF -SUCH DAMAGES. - - 17. Interpretation of Sections 15 and 16. - - If the disclaimer of warranty and limitation of liability provided -above cannot be given local legal effect according to their terms, -reviewing courts shall apply local law that most closely approximates -an absolute waiver of all civil liability in connection with the -Program, unless a warranty or assumption of liability accompanies a -copy of the Program in return for a fee. - - END OF TERMS AND CONDITIONS - - How to Apply These Terms to Your New Programs - - If you develop a new program, and you want it to be of the greatest -possible use to the public, the best way to achieve this is to make it -free software which everyone can redistribute and change under these terms. - - To do so, attach the following notices to the program. It is safest -to attach them to the start of each source file to most effectively -state the exclusion of warranty; and each file should have at least -the "copyright" line and a pointer to where the full notice is found. - - - Copyright (C) - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . - -Also add information on how to contact you by electronic and paper mail. - - If the program does terminal interaction, make it output a short -notice like this when it starts in an interactive mode: - - Copyright (C) - This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. - This is free software, and you are welcome to redistribute it - under certain conditions; type `show c' for details. - -The hypothetical commands `show w' and `show c' should show the appropriate -parts of the General Public License. Of course, your program's commands -might be different; for a GUI interface, you would use an "about box". - - You should also get your employer (if you work as a programmer) or school, -if any, to sign a "copyright disclaimer" for the program, if necessary. -For more information on this, and how to apply and follow the GNU GPL, see -. - - The GNU General Public License does not permit incorporating your program -into proprietary programs. If your program is a subroutine library, you -may consider it more useful to permit linking proprietary applications with -the library. If this is what you want to do, use the GNU Lesser General -Public License instead of this License. But first, please read -. diff -r 28c7be8f252c -r a5f8084b8368 LICENSE.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/LICENSE.md Mon Dec 21 10:23:37 2020 +0900 @@ -0,0 +1,19 @@ +Copyright (c) 2020 + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff -r 28c7be8f252c -r a5f8084b8368 OD.agda --- a/OD.agda Sun Dec 20 12:37:07 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,618 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} -open import Level -open import Ordinals -module OD {n : Level } (O : Ordinals {n} ) where - -open import zf -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) -open import Data.Nat.Properties -open import Data.Empty -open import Relation.Nullary -open import Relation.Binary hiding (_⇔_) -open import Relation.Binary.Core hiding (_⇔_) - -open import logic -import OrdUtil -open import nat - -open Ordinals.Ordinals O -open Ordinals.IsOrdinals isOrdinal -open Ordinals.IsNext isNext -open OrdUtil O - --- Ordinal Definable Set - -record OD : Set (suc n ) where - field - def : (x : Ordinal ) → Set n - -open OD - -open _∧_ -open _∨_ -open Bool - -record _==_ ( a b : OD ) : Set n where - field - eq→ : ∀ { x : Ordinal } → def a x → def b x - eq← : ∀ { x : Ordinal } → def b x → def a x - -==-refl : { x : OD } → x == x -==-refl {x} = record { eq→ = λ x → x ; eq← = λ x → x } - -open _==_ - -==-trans : { x y z : OD } → x == y → y == z → x == z -==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) } - -==-sym : { x y : OD } → x == y → y == x -==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } - - -⇔→== : { x y : OD } → ( {z : Ordinal } → (def x z ⇔ def y z)) → x == y -eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m -eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m - --- next assumptions are our axiom --- --- OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one --- correspondence to the OD then the OD looks like a ZF Set. --- --- If all ZF Set have supreme upper bound, the solutions of OD have to be bounded, i.e. --- bbounded ODs are ZF Set. Unbounded ODs are classes. --- --- In classical Set Theory, HOD is used, as a subset of OD, --- HOD = { x | TC x ⊆ OD } --- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x. --- This is not possible because we don't have V yet. So we assumes HODs are bounded OD. --- --- We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks. --- There two contraints on the HOD order, one is ∋, the other one is ⊂. --- ODs have an ovbious maximum, but Ordinals are not, but HOD has no maximum because there is an aribtrary --- bound on each HOD. --- --- In classical Set Theory, sup is defined by Uion, since we are working on constructive logic, --- we need explict assumption on sup. --- --- ==→o≡ is necessary to prove axiom of extensionality. - --- Ordinals in OD , the maximum -Ords : OD -Ords = record { def = λ x → One } - -record HOD : Set (suc n) where - field - od : OD - odmax : Ordinal - <-osuc (sup-o< next-ord (sup-o next-ord)) where - next-ord : Ordinal → Ordinal - next-ord x = osuc x - --- Ordinal in OD ( and ZFSet ) Transitive Set -Ord : ( a : Ordinal ) → HOD -Ord a = record { od = record { def = λ y → y o< a } ; odmax = a ; ¬a ¬b c = no ¬b - --- the pair -_,_ : HOD → HOD → HOD -x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x) (& y) ; ¬a ¬b c = - ⊥-elim ( o<> (⊆→o≤ {x , x} {y} y⊆x,x ) lemma1 ) where - lemma : {z : Ordinal} → (z ≡ & x) ∨ (z ≡ & x) → & x ≡ z - lemma (case1 refl) = refl - lemma (case2 refl) = refl - y⊆x,x : {z : Ordinal} → def (od (x , x)) z → def (od y) z - y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x - lemma1 : osuc (& y) o< & (x , x) - lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c ) - -ε-induction : { ψ : HOD → Set (suc n)} - → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) - → (x : HOD ) → ψ x -ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc ) where - induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox) - induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) - ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy) - ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy - -Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD -Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; u ¬a ¬b c = ⊥-elim (not c) -_∈_ : ( A B : HOD ) → Set n -A ∈ B = B ∋ A - -OPwr : (A : HOD ) → HOD -OPwr A = Ord ( sup-o (Ord (osuc (& A))) ( λ x A∋x → & ( A ∩ (* x)) ) ) - -Power : HOD → HOD -Power A = Replace (OPwr (Ord (& A))) ( λ x → A ∩ x ) --- ｛_｝ : ZFSet → ZFSet --- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly - -union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z -union→ X z u xx not = ⊥-elim ( not (& u) ( ⟪ proj1 xx - , subst ( λ k → odef k (& z)) (sym *iso) (proj2 xx) ⟫ )) -union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) -union← X z UX∋z = FExists _ lemma UX∋z where - lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) - lemma {y} xx not = not (* y) ⟪ d→∋ X (proj1 xx) , proj2 xx ⟫ - -data infinite-d : ( x : Ordinal ) → Set n where - iφ : infinite-d o∅ - isuc : {x : Ordinal } → infinite-d x → - infinite-d (& ( Union (* x , (* x , * x ) ) )) - --- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair. --- We simply assumes infinite-d y has a maximum. --- --- This means that many of OD may not be HODs because of the & mapping divergence. --- We should have some axioms to prevent this such as & x o< next (odmax x). --- --- postulate --- ωmax : Ordinal --- <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax --- --- infinite : HOD --- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; ¬a ¬b c with (incl lt) (o<-subst c (sym &iso) refl ) -... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl )) - -ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y -ψiso {ψ} t refl = t -selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) -selection {ψ} {X} {y} = ⟪ - ( λ cond → ⟪ proj1 cond , ψiso {ψ} (proj2 cond) (sym *iso) ⟫ ) - , ( λ select → ⟪ proj1 select , ψiso {ψ} (proj2 select) *iso ⟫ ) - ⟫ - -selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y -selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt) - -sup-c< : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → & (ψ x) o< (sup-o X (λ y X∋y → & (ψ (* y)))) -sup-c< ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o< X lt ) -replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x -replacement← {ψ} X x lt = ⟪ sup-c< ψ {X} {x} lt , lemma ⟫ where - lemma : def (in-codomain X ψ) (& (ψ x)) - lemma not = ⊥-elim ( not ( & x ) ⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ ) -replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) -replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where - lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((& x) ≡ & (ψ (* y)))) - → ¬ ((y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y))) - lemma2 not not2 = not ( λ y d → not2 y ⟪ proj1 d , lemma3 (proj2 d)⟫) where - lemma3 : {y : Ordinal } → (& x ≡ & (ψ (* y))) → (* (& x) =h= ψ (* y)) - lemma3 {y} eq = subst (λ k → * (& x) =h= k ) *iso (o≡→== eq ) - lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)) ) - lemma not y not2 = not (* y) (subst (λ k → k =h= ψ (* y)) *iso ( proj2 not2 )) - ---- ---- Power Set ---- ---- First consider ordinals in HOD ---- ---- A ∩ x = record { def = λ y → odef A y ∧ odef x y } subset of A --- --- -∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a ) -∩-≡ {a} {b} inc = record { - eq→ = λ {x} x ¬a ¬b c = yes c - -open import zfc - -HOD→ZFC : ZFC -HOD→ZFC = record { - ZFSet = HOD - ; _∋_ = _∋_ - ; _≈_ = _=h=_ - ; ∅ = od∅ - ; Select = Select - ; isZFC = isZFC - } where - -- infixr 200 _∈_ - -- infixr 230 _∩_ _∪_ - isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select - isZFC = record { - choice-func = choice-func ; - choice = choice - } where - -- Axiom of choice ( is equivalent to the existence of minimal in our case ) - -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] - choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD - choice-func X {x} not X∋x = minimal x not - choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A - choice X {A} X∋A not = x∋minimal A not - diff -r 28c7be8f252c -r a5f8084b8368 ODUtil.agda --- a/ODUtil.agda Sun Dec 20 12:37:07 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,179 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} -open import Level -open import Ordinals -module ODUtil {n : Level } (O : Ordinals {n} ) where - -open import zf -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) -open import Data.Nat.Properties -open import Data.Empty -open import Relation.Nullary -open import Relation.Binary hiding ( _⇔_ ) - -open import logic -open import nat - -open Ordinals.Ordinals O -open Ordinals.IsOrdinals isOrdinal -open Ordinals.IsNext isNext -import OrdUtil -open OrdUtil O - -import OD -open OD O -open OD.OD -open ODAxiom odAxiom - -open HOD -open _⊆_ -open _∧_ -open _==_ - -cseq : HOD → HOD -cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osucz → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z))) - -subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A ) -subset-lemma {A} {x} = record { - proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } - ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫ - } - - -ω (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k ) - (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c) - -ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x -ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫ - -ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) ≡ od∅ ) -ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → & y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) ) - -nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i -nat→ω-iso {i} = ε-induction {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where - ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) → - (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x - ind {x} prev lt = ind1 lt *iso where - ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x - ind1 {o∅} iφ refl = sym o∅≡od∅ - ind1 (isuc {x₁} ltd) ox=x = begin - nat→ω (ω→nato (isuc ltd) ) - ≡⟨⟩ - Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd))) - ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩ - Union (* x₁ , (* x₁ , * x₁)) - ≡⟨ trans ( sym *iso) ox=x ⟩ - x - ∎ where - open ≡-Reasoning - lemma0 : x ∋ * x₁ - lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not - (& (* x₁ , * x₁)) ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ ) - lemma1 : infinite ∋ * x₁ - lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd - lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1 - lemma3 iφ iφ refl = HE.refl - lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) ))) - lemma3 (isuc {y} ltd) iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) ))) - lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq)) - ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t - lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1 - lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq) where - lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1 - lemma6 refl HE.refl = refl - lemma : nat→ω (ω→nato ltd) ≡ * x₁ - lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd) &iso ) ) ( prev {* x₁} lemma0 lemma1 ) - -ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i -ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where - lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡ nat→ω i → ω→nato ltd ≡ i - lemma {x} Zero iφ eq = refl - lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅ - lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅ ) *iso eq )) - lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) ) where -- * x ≡ nat→ω i - lemma1 : * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i - lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k) - ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym - (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq )))))) - diff -r 28c7be8f252c -r a5f8084b8368 OPair.agda --- a/OPair.agda Sun Dec 20 12:37:07 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,213 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} - -open import Level -open import Ordinals -module OPair {n : Level } (O : Ordinals {n}) where - -open import zf -open import logic -import OD -import ODUtil -import OrdUtil - -open import Relation.Nullary -open import Relation.Binary -open import Data.Empty -open import Relation.Binary -open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) - -open OD O -open OD.OD -open OD.HOD -open ODAxiom odAxiom - -open Ordinals.Ordinals O -open Ordinals.IsOrdinals isOrdinal -open Ordinals.IsNext isNext -open OrdUtil O -open ODUtil O - -open _∧_ -open _∨_ -open Bool - -open _==_ - -<_,_> : (x y : HOD) → HOD -< x , y > = (x , x ) , (x , y ) - -exg-pair : { x y : HOD } → (x , y ) =h= ( y , x ) -exg-pair {x} {y} = record { eq→ = left ; eq← = right } where - left : {z : Ordinal} → odef (x , y) z → odef (y , x) z - left (case1 t) = case2 t - left (case2 t) = case1 t - right : {z : Ordinal} → odef (y , x) z → odef (x , y) z - right (case1 t) = case2 t - right (case2 t) = case1 t - -ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y -ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq ) - -od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y -od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq ) - -eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > -eq-prod refl refl = refl - -xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y -xx=zy→x=y {x} {y} eq with trio< (& x) (& y) -xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) -xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) -xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) -xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b -xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl) -xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) -xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) - -prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) -prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where - lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y - lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq ) where - lemma3 : ( x , x ) =h= ( y , z ) - lemma3 = ==-trans eq exg-pair - lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y - lemma1 {x} {y} eq with eq← eq {& y} (case2 refl) - lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) - lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) - lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z - lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl) - lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z - ... | refl with lemma2 (==-sym eq ) - ... | refl = refl - lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z - lemmax : x ≡ x' - lemmax with eq→ eq {& (x , x)} (case1 refl) - lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') - lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' - ... | refl = lemma1 (ord→== s ) - lemmay : y ≡ y' - lemmay with lemmax - ... | refl with lemma4 eq -- with (x,y)≡(x,y') - ... | eq1 = lemma4 (ord→== (cong (λ k → & k ) eq1 )) - --- --- unlike ordered pair, ZFProduct is not a HOD - -data ord-pair : (p : Ordinal) → Set n where - pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) ) - -ZFProduct : OD -ZFProduct = record { def = λ x → ord-pair x } - --- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) --- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y' --- eq-pair refl refl = HE.refl - -pi1 : { p : Ordinal } → ord-pair p → Ordinal -pi1 ( pair x y) = x - -π1 : { p : HOD } → def ZFProduct (& p) → HOD -π1 lt = * (pi1 lt ) - -pi2 : { p : Ordinal } → ord-pair p → Ordinal -pi2 ( pair x y ) = y - -π2 : { p : HOD } → def ZFProduct (& p) → HOD -π2 lt = * (pi2 lt ) - -op-cons : { ox oy : Ordinal } → def ZFProduct (& ( < * ox , * oy > )) -op-cons {ox} {oy} = pair ox oy - -def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x -def-subst df refl refl = df - -p-cons : ( x y : HOD ) → def ZFProduct (& ( < x , y >)) -p-cons x y = def-subst {_} {_} {ZFProduct} {& (< x , y >)} (pair (& x) ( & y )) refl ( - let open ≡-Reasoning in begin - & < * (& x) , * (& y) > - ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩ - & < x , y > - ∎ ) - -op-iso : { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op -op-iso (pair ox oy) = refl - -p-iso : { x : HOD } → (p : def ZFProduct (& x) ) → < π1 p , π2 p > ≡ x -p-iso {x} p = ord≡→≡ (op-iso p) - -p-pi1 : { x y : HOD } → (p : def ZFProduct (& < x , y >) ) → π1 p ≡ x -p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) )) - -p-pi2 : { x y : HOD } → (p : def ZFProduct (& < x , y >) ) → π2 p ≡ y -p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p))) - -ω-pair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & (x , y) o< next m -ω-pair lx ly = next< (omax o< next m -ω-opair {x} {y} {m} lx ly = lemma0 where - lemma0 : & < x , y > o< next m - lemma0 = osucprev (begin - osuc (& < x , y >) - <⟨ osuc ) )) - -product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b > -product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >))) - ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where - lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >))) - lemma1 = replacement← B b B∋b - lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >) - lemma2 = replacement← A a A∋a - -x ¬a ¬b c = ordtrans (ω-opair (x ¬a ¬b c = ¬b eq - -o<> : {x y : Ordinal } → y o< x → x o< y → ⊥ -o<> {ox} {oy} lt tl with trio< ox oy -o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt -o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl -o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl - -osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥ -osuc-< {x} {y} y x x < osuc x -> y = x ∨ x < y → ⊥ -osucc {ox} {oy} oy ¬a ¬b c with osuc-≡< c -osucc {ox} {oy} oy ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy ¬a ¬b c = ⊥-elim (o<> (osucc c) oy ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) - -maxα : Ordinal → Ordinal → Ordinal -maxα x y with trio< x y -maxα x y | tri< a ¬b ¬c = y -maxα x y | tri> ¬a ¬b c = x -maxα x y | tri≈ ¬a refl ¬c = x - -omin : Ordinal → Ordinal → Ordinal -omin x y with trio< x y -omin x y | tri< a ¬b ¬c = x -omin x y | tri> ¬a ¬b c = y -omin x y | tri≈ ¬a refl ¬c = x - -min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y -min1 {x} {y} {z} z ¬a ¬b c = z ¬a ¬b c = osuc x -omax x y | tri≈ ¬a refl ¬c = osuc x - -omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y -omax< x y lt with trio< x y -omax< x y lt | tri< a ¬b ¬c = refl -omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) -omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) - -omax≤ : ( x y : Ordinal ) → x o≤ y → osuc y ≡ omax x y -omax≤ x y le with trio< x y -omax≤ x y le | tri< a ¬b ¬c = refl -omax≤ x y le | tri≈ ¬a refl ¬c = refl -omax≤ x y le | tri> ¬a ¬b c with osuc-≡< le -omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq) -omax≤ x y le | tri> ¬a ¬b c | case2 x ¬a ¬b c = ⊥-elim (¬b eq ) - -omax-x : ( x y : Ordinal ) → x o< omax x y -omax-x x y with trio< x y -omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc -omax-x x y | tri> ¬a ¬b c = <-osuc -omax-x x y | tri≈ ¬a refl ¬c = <-osuc - -omax-y : ( x y : Ordinal ) → y o< omax x y -omax-y x y with trio< x y -omax-y x y | tri< a ¬b ¬c = <-osuc -omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc -omax-y x y | tri≈ ¬a refl ¬c = <-osuc - -omxx : ( x : Ordinal ) → omax x x ≡ osuc x -omxx x with trio< x x -omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) -omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) -omxx x | tri≈ ¬a refl ¬c = refl - -omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x) -omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) - -open _∧_ - -o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j -o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc -OrdTrans : Transitive _o≤_ -OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c -OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc -OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc -OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc -OrdTrans a≤b b≤c | case2 a ¬a ¬b c = ⊥-elim ( ¬x<0 c ) - -next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z -next< {x} {y} {z} x ¬a ¬b c = ⊥-elim (¬nx osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x -nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ... -nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx ¬a ¬b c = -- x < y < next y < next x - ⊥-elim ( ¬nx ¬a ¬b c with osuc-≡< x≤y -≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl -- x = y < next x -≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x ¬a ¬b c = o≤-refl (sym ( x ¬a ¬b c = subst (λ k → osuc x o< k ) nexto≡ (osuc ¬a ¬b c = osuc ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx - -record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where - field - os→ : (x : Ordinal) → x o< maxordinal → Ordinal - os← : Ordinal → Ordinal - os←limit : (x : Ordinal) → os← x o< maxordinal - os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x - os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x - -module o≤-Reasoning {n : Level} (O : Ordinals {n} ) where - - -- open inOrdinal O - - resp-o< : _o<_ Respects₂ _≡_ - resp-o< = resp₂ _o<_ - - trans1 : {i j k : Ordinal} → i o< j → j o< osuc k → i o< k - trans1 {i} {j} {k} i ¬a ¬b c with Oprev-p x - V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) - V1 x V0 | tri> ¬a ¬b c | no ¬p = - record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (V0 y lt) x ) } ; odmax = x; ¬a ¬b c with Oprev-p x - L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) - L1 x L0 | tri> ¬a ¬b c | no ¬p = - record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (L0 y lt) x ) } ; odmax = x; ) )) - -Func : OD -Func = record { def = λ x → def ZFProduct x - ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) → b ≡ c ) } - -FuncP : ( A B : HOD ) → HOD -FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x - ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } - ; odmax = odmax (ZFP A B) ; + + +
+    record ZF {n m : Level } : Set (suc (n ⊔ m)) where
+      field
+         ZFSet : Set n
+         _∋_ : ( A x : ZFSet  ) → Set m
+         _≈_ : ( A B : ZFSet  ) → Set m
+         ∅  : ZFSet
+         _,_ : ( A B : ZFSet  ) → ZFSet
+         Union : ( A : ZFSet  ) → ZFSet
+         Power : ( A : ZFSet  ) → ZFSet
+         Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet
+         Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
+         infinite : ZFSet
+         isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite
+    record IsZF {n m : Level }
+         (ZFSet : Set n)
+         (_∋_ : ( A x : ZFSet  ) → Set m)
+         (_≈_ : Rel ZFSet m)
+         (∅  : ZFSet)
+         (_,_ : ( A B : ZFSet  ) → ZFSet)
+         (Union : ( A : ZFSet  ) → ZFSet)
+         (Power : ( A : ZFSet  ) → ZFSet)
+         (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
+         (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
+         (infinite : ZFSet)
+           : Set (suc (n ⊔ m)) where
+      field
+         isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
+         pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y )
+         pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t
+         union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z  
+         union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+         empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
+         power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x}
+         power← : ∀( A t : ZFSet  ) → ( ∀ {x}  →  _⊆_ t A {x})  → Power A ∋ t 
+         extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
+         regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
+         minimal : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 
+         regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimal x not  ∈ x ∧  (  minimal x not  ∩ x  ≈ ∅ ) )
+         ε-induction : { ψ : ZFSet → Set m}
+                  → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
+                  → (x : ZFSet ) → ψ x
+         infinity∅ :  ∅ ∈ infinite
+         infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite
+         selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ )
+         replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ
+         replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
+         choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
+         choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
+
+
 Shinji KONO  /  Fri Jan 10 12:24:29 2020
+
diff -r 28c7be8f252c -r a5f8084b8368 fig/zf-record.ind
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/zf-record.ind	Mon Dec 21 10:23:37 2020 +0900
@@ -0,0 +1,50 @@
+    record ZF {n m : Level } : Set (suc (n ⊔ m)) where
+      field
+         ZFSet : Set n
+         _∋_ : ( A x : ZFSet  ) → Set m
+         _≈_ : ( A B : ZFSet  ) → Set m
+         ∅  : ZFSet
+         _,_ : ( A B : ZFSet  ) → ZFSet
+         Union : ( A : ZFSet  ) → ZFSet
+         Power : ( A : ZFSet  ) → ZFSet
+         Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet
+         Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
+         infinite : ZFSet
+         isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite
+
+    record IsZF {n m : Level }
+         (ZFSet : Set n)
+         (_∋_ : ( A x : ZFSet  ) → Set m)
+         (_≈_ : Rel ZFSet m)
+         (∅  : ZFSet)
+         (_,_ : ( A B : ZFSet  ) → ZFSet)
+         (Union : ( A : ZFSet  ) → ZFSet)
+         (Power : ( A : ZFSet  ) → ZFSet)
+         (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
+         (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
+         (infinite : ZFSet)
+           : Set (suc (n ⊔ m)) where
+      field
+         isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
+         pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y )
+         pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t
+         union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z  
+         union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+         empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
+         power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x}
+         power← : ∀( A t : ZFSet  ) → ( ∀ {x}  →  _⊆_ t A {x})  → Power A ∋ t 
+         extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
+         regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
+         minimal : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 
+         regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimal x not  ∈ x ∧  (  minimal x not  ∩ x  ≈ ∅ ) )
+         ε-induction : { ψ : ZFSet → Set m}
+                  → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
+                  → (x : ZFSet ) → ψ x
+         infinity∅ :  ∅ ∈ infinite
+         infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite
+         selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ )
+         replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ
+         replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
+         choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
+         choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
+
diff -r 28c7be8f252c -r a5f8084b8368 filter.agda
--- a/filter.agda	Sun Dec 20 12:37:07 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-open import Level
-open import Ordinals
-module filter {n : Level } (O : Ordinals {n})   where
-
-open import zf
-open import logic
-import OD 
-
-open import Relation.Nullary 
-open import Data.Empty 
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality
-import BAlgbra 
-
-open BAlgbra O
-
-open inOrdinal O
-open OD O
-open OD.OD
-open ODAxiom odAxiom
-
-import OrdUtil
-import ODUtil
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
-open OrdUtil O
-open ODUtil O
-
-
-import ODC
-open ODC O
-
-open _∧_
-open _∨_
-open Bool
-
--- Kunen p.76 and p.53, we use ⊆
-record Filter  ( L : HOD  ) : Set (suc n) where
-   field
-       filter : HOD   
-       f⊆PL :  filter ⊆ Power L 
-       filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
-       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
-
-open Filter
-
-record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
-   field
-       proper  : ¬ (filter P ∋ od∅)
-       prime   : {p q : HOD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
-
-record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
-   field
-       proper  : ¬ (filter P ∋ od∅)
-       ultra   : {p : HOD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
-
-open _⊆_
-
-∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
-∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
-
-∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
-∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
-
-∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
-∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
-
-q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
-q∩q⊆q = record { incl = λ lt → proj1 lt } 
-
-open HOD
-
------
---
---  ultra filter is prime
---
-
-filter-lemma1 :  {L : HOD} → (P : Filter L)  → ∀ {p q : HOD } → ultra-filter P  → prime-filter P 
-filter-lemma1 {L} P u = record {
-         proper = ultra-filter.proper u
-       ; prime = lemma3
-    } where
-  lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
-  lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
-  ... | case1 p∈P  = case1 p∈P
-  ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
-    lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
-    lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt  ⟫
-       ;  eq← = λ {x} lt → ⟪  case2 (proj1 lt) , proj2 lt ⟫
-      } where
-         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
-         lemma4 x lt with proj1 lt
-         lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
-         lemma4 x lt | case2 qx = qx
-    lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
-    lemma6 = filter2 P lt ¬p∈P
-    lemma7 : filter P ∋ (q ∩ (L ＼ p))
-    lemma7 =  subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
-    lemma8 : (q ∩ (L ＼ p)) ⊆ q
-    lemma8 = q∩q⊆q
-
------
---
---  if Filter contains L, prime filter is ultra
---
-
-filter-lemma2 :  {L : HOD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
-filter-lemma2 {L} P f∋L prime = record {
-         proper = prime-filter.proper prime
-       ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
-   } where
-        open _==_
-        p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
-        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
-        eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
-        lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
-        lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
-
-record Dense  (P : HOD ) : Set (suc n) where
-   field
-       dense : HOD
-       d⊆P :  dense ⊆ Power P 
-       dense-f : HOD → HOD
-       dense-d :  { p : HOD} → p ⊆ P → dense ∋ dense-f p  
-       dense-p :  { p : HOD} → p ⊆ P → p ⊆ (dense-f p) 
-
-record Ideal  ( L : HOD  ) : Set (suc n) where
-   field
-       ideal : HOD   
-       i⊆PL :  ideal ⊆ Power L 
-       ideal1 : { p q : HOD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
-       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)
-
-open Ideal
-
-proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
-proper-ideal {L} P {p} = ideal P ∋ od∅
-
-prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
-prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
-
-----
---
--- Filter/Ideal without ZF 
---     L have to be a Latice
---
-
-record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-   field
-       filter : L → Set n
-       f⊆P :  PL filter 
-       filter1 : { p q : L } → PL (λ x → q ⊆ x )  → filter p →  p ⊆ q  → filter q
-       filter2 : { p q : L } → filter p →  filter q  → filter (p ∩ q)
-
-Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
-Filter-is-F {L} f = record {
-       filter = λ x → Lift (suc n) ((filter f) ∋ x)
-     ; f⊆P = λ x f∋x →  power→⊆ _ _ (incl ( f⊆PL f  ) (lower f∋x ))
-     ; filter1 = λ {p} {q} q⊆L f∋p  p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q)
-     ; filter2 = λ {p} {q} f∋p f∋q  → lift ( filter2 f (lower f∋p) (lower f∋q)) 
-    }
-
-record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-   field
-       dense : L → Set n
-       d⊆P :  PL dense 
-       dense-f : L → L 
-       dense-d :  { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p  )
-       dense-p :  { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) 
-
-Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
-Dense-is-F {L} f = record {
-       dense =  λ x → Lift (suc n) ((dense f) ∋ x)
-    ;  d⊆P = λ x f∋x →  power→⊆ _ _ (incl ( d⊆P f  ) (lower f∋x ))
-    ;  dense-f = λ x → dense-f f x
-    ;  dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) )
-    ;  dense-p = λ {p} d → dense-p f (d p refl-⊆) 
-  } where open Dense
-
-       
-record GenericFilter (P : HOD) : Set (suc n) where
-    field
-       genf : Filter P
-       generic : (D : Dense P ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
-
-record F-GenericFilter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-    field
-       GFilter : F-Filter L PL _⊆_ _∩_
-       Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x →  L
-       Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) →  F-Filter.filter GFilter (Intersection D y )
-
diff -r 28c7be8f252c -r a5f8084b8368 generic-filter.agda
--- a/generic-filter.agda	Sun Dec 20 12:37:07 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,263 +0,0 @@
-open import Level
-open import Ordinals
-module generic-filter {n : Level } (O : Ordinals {n})   where
-
-import filter 
-open import zf
-open import logic
--- open import partfunc {n} O
-import OD 
-
-open import Relation.Nullary 
-open import Relation.Binary 
-open import Data.Empty 
-open import Relation.Binary
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-import BAlgbra 
-
-open BAlgbra O
-
-open inOrdinal O
-open OD O
-open OD.OD
-open ODAxiom odAxiom
-import OrdUtil
-import ODUtil
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
-open OrdUtil O
-open ODUtil O
-
-
-import ODC
-
-open filter O
-
-open _∧_
-open _∨_
-open Bool
-
-
-open HOD
-
--------
---    the set of finite partial functions from ω to 2
---
---
-
-open import Data.List hiding (filter)
-open import Data.Maybe 
-
-import OPair
-open OPair O
-
-ODSuc : (y : HOD) → infinite ∋ y → HOD
-ODSuc y lt = Union (y , (y , y)) 
-
-data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
-  hφ :  Hω2 0 o∅
-  h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 0 >) ,  * x )))
-  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 1 >) ,  * x )))
-  he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) x
-
-record  Hω2r (x : Ordinal) : Set n where
-  field
-    count : Nat
-    hω2 : Hω2 count x
-
-open Hω2r
-
-HODω2 :  HOD
-HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ;  , ( list→hod t (Suc i) )) 
-   list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) 
-   list→hod (nothing ∷ t) i = list→hod t (Suc i ) 
-
-Hω2→3 : (x :  HOD) → HODω2 ∋ x → List (Maybe Two) 
-Hω2→3 x = lemma where
-   lemma : { y : Ordinal } →  Hω2r y → List (Maybe Two)
-   lemma record { count = 0 ; hω2 = hφ } = []
-   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 =  hω3 }
-   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 =  hω3 }
-   lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 =  hω3 }
-
-ω→2 : HOD
-ω→2 = Power infinite
-
-ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
-ω→2f x lt n with ODC.∋-p O x (nat→ω n)
-ω→2f x lt n | yes p = i1
-ω→2f x lt n | no ¬p = i0
-
-fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
-fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (&  x) ) → f (ω→nat x lt) ≡ i1 )
-
-fω→2 : (Nat → Two) → HOD
-fω→2 f = Select infinite (fω→2-sel f)
-
-open _==_
-
-import Axiom.Extensionality.Propositional
-postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
-
-ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
-ω2∋f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
-
-ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
-ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
-ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
-
-open _⊆_
-
--- someday ...
--- postulate 
---    ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
---    fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
-
-record CountableOrdinal : Set (suc (suc n)) where
-   field
-       ctl→ : Nat → Ordinal
-       ctl← : Ordinal → Nat
-       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
-       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
-
-record CountableHOD : Set (suc (suc n)) where
-   field
-       mhod : HOD
-       mtl→ : Nat → Ordinal
-       mtl→∈P : (i : Nat) → odef mhod (mtl→ i)
-       mtl← : (x : Ordinal) → odef mhod x → Nat
-       mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x 
-       mtl-iso← : { x : Nat }  → mtl← (mtl→ x ) (mtl→∈P x) ≡ x
-   
-       
-open CountableOrdinal 
-open CountableHOD
-
-----
---   a(n) ∈ M
---   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q    
---
-PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
-PGHOD i C P p = record { od = record { def = λ x  →
-       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
-   ; odmax = odmax (Power P)  ;  }
---
---   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }
---
-
-
-
diff -r 28c7be8f252c -r a5f8084b8368 logic.agda
--- a/logic.agda	Sun Dec 20 12:37:07 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-module logic where
-
-open import Level
-open import Relation.Nullary
-open import Relation.Binary hiding (_⇔_ )
-open import Data.Empty
-
-data One {n : Level } : Set n where
-  OneObj : One
-
-data Two : Set where
-   i0 : Two
-   i1 : Two
-
-data Bool : Set where
-   true : Bool
-   false : Bool
-
-record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
-   constructor ⟪_,_⟫
-   field
-      proj1 : A
-      proj2 : B
-
-data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
-   case1 : A → A ∨ B
-   case2 : B → A ∨ B
-
-_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
-_⇔_ A B =  ( A → B ) ∧ ( B → A )
-
-contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
-contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
-
-double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
-double-neg A notnot = notnot A
-
-double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
-double-neg2 notnot A = notnot ( double-neg A )
-
-de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
-de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
-de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
-
-dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
-dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
-dont-or {A} {B} (case2 b) ¬A = b
-
-dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
-dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
-dont-orb {A} {B} (case1 a) ¬B = a
-
-
-infixr  130 _∧_
-infixr  140 _∨_
-infixr  150 _⇔_
-
diff -r 28c7be8f252c -r a5f8084b8368 nat.agda
--- a/nat.agda	Sun Dec 20 12:37:07 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-module nat where
-
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-open import Data.Empty
-open import Relation.Nullary
-open import  Relation.Binary.PropositionalEquality
-open import  logic
-
-
-nat-<> : { x y : Nat } → x < y → y < x → ⊥
-nat-<>  (s≤s x x→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
->→¬< (s≤s x→¬< x : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
-trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
-trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
-
-d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
-d<→lv Φ< = refl
-d<→lv (s< lt) = refl
-
-o∅ : {n : Level} → Ordinal {n}
-o∅  = record { lv = Zero ; ord = Φ Zero }
-
-open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
-
-ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
-      lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
-ordinal-cong refl refl = refl
-
-≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
-≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
-
-trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
-trio<≡ refl = ≡→¬d<
-
-trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
-trio>≡ refl = ≡→¬d<
-
-triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
-triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
-triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
-triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
-triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
-triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
-triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
-triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> (  λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
-
-osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
-osuc record { lv = lx ; ord = ox } = record { lv = lx ; ord = OSuc lx ox }
-
-<-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
-<-osuc {n} {record { lv = lx ; ord = Φ .lx }} =  case2 Φ<
-<-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s : {n : Level} →  {x y : Ordinal {n}  }  →  y o< x → x o< y → ⊥
-o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<>  x₁ x₂
-o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁
-o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂
-o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) (case2 ())
-o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y (case2 y x₂ x₁
-osuc-< {n} {x} {y} y (case2 x ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
-   lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
-   lemma1 (case1 x) = ¬a x
-   lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) c  )
-trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
-trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
-   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
-   lemma1 refl = refl
-   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
-   lemma2 (case1 x) = ¬a x
-   lemma2 (case2 x) = trio<> x a
-trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
-   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
-   lemma1 refl = refl
-   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
-   lemma2 (case1 x) = ¬a x
-   lemma2 (case2 x) = trio<> x c
-trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
-   lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
-   lemma1 (case1 x) = ¬a x
-   lemma1 (case2 x) = ≡→¬d< x
-
-
-open _∧_
-
-TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
-  → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
-  → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
-  →  ∀ (x : Ordinal)  → ψ x
-TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where
-  TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
-  TransFinite1 Zero (Φ 0) = ⟪  caseΦ Zero lemma , lemma1 ⟫ where
-      lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
-      lemma x (case1 ())
-      lemma x (case2 ())
-      lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
-      lemma1 x (case1 ())
-      lemma1 x (case2 ())
-  TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where
-      lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
-      lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
-      lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
-      lemma lx1 ox1            (case1 lt) with <-∨ lt
-      lemma lx (Φ lx)          (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
-      lemma lx (Φ lx)          (case1 lt) | case2 lt1 = lemma0  lx (Φ lx) (case1 lt1)
-      lemma lx (OSuc lx ox1)   (case1 lt) | case1 refl = caseOSuc lx ox1 lemma2 where
-          lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx ox1) → ψ y
-          lemma2 y lt1 with osuc-≡< lt1
-          lemma2 y lt1 | case1 refl = lemma lx ox1 (case1 a axiom of choice
+---
+record choiced  ( X : Ordinal ) : Set n where
+  field
+     a-choice : Ordinal
+     is-in : odef (* X) a-choice
+
+open choiced
+
+-- ∋→d : ( a : HOD  ) { x : HOD } → * (& a) ∋ x → X ∋ * (a-choice (choice-func X not))
+-- ∋→d a lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt
+
+oo∋ : { a : HOD} {  x : Ordinal } → odef (* (& a)) x → a ∋ * x
+oo∋ lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt
+
+∋oo : { a : HOD} {  x : Ordinal } → a ∋ * x → odef (* (& a)) x 
+∋oo lt = subst₂ (λ j k → odef j k ) (sym *iso) &iso lt 
+
+OD→ZFC : ZFC
+OD→ZFC   = record { 
+    ZFSet = HOD 
+    ; _∋_ = _∋_ 
+    ; _≈_ = _=h=_ 
+    ; ∅  = od∅
+    ; Select = Select
+    ; isZFC = isZFC
+ } where
+    -- infixr  200 _∈_
+    -- infixr  230 _∩_ _∪_
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
+    isZFC = record {
+       choice-func = λ A {X} not A∋X → * (a-choice (choice-func X not) );
+       choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not))
+     } where
+         --
+         -- the axiom choice from LEM and OD ordering
+         --
+         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (& X)
+         choice-func  X not = have_to_find where
+                 ψ : ( ox : Ordinal ) → Set n
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced (& X)
+                 lemma-ord : ( ox : Ordinal  ) → ψ ox
+                 lemma-ord  ox = TransFinite0 {ψ} induction ox where
+                    ∀-imply-or :  {A : Ordinal  → Set n } {B : Set n }
+                        → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
+                    ∀-imply-or  {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
+                    ∀-imply-or  {A} {B} ∀AB | case1 t = case1 t
+                    ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x not )) where
+                         lemma : ¬ ((x : Ordinal ) → A x) →  B
+                         lemma not with p∨¬p B
+                         lemma not | case1 b = b
+                         lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
+                    induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
+                    induction x prev with ∋-p X ( * x) 
+                    ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo  p } )
+                    ... | no ¬p = lemma where
+                         lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (& X)
+                         lemma1 y with ∋-p X (* y)
+                         lemma1 y | yes y <-osuc (sup-o< next-ord (sup-o next-ord)) where
+   next-ord : Ordinal → Ordinal
+   next-ord x = osuc x
+
+-- Ordinal in OD ( and ZFSet ) Transitive Set
+Ord : ( a : Ordinal  ) → HOD 
+Ord  a = record { od = record { def = λ y → y o< a } ; odmax = a ;  ¬a ¬b c = no ¬b
+
+-- the pair
+_,_ : HOD  → HOD  → HOD  
+x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x)  (& y) ;  ¬a ¬b c =
+  ⊥-elim ( o<> (⊆→o≤ {x , x} {y} y⊆x,x ) lemma1 ) where
+    lemma : {z : Ordinal} → (z ≡ & x) ∨ (z ≡ & x) → & x ≡ z
+    lemma (case1 refl) = refl
+    lemma (case2 refl) = refl
+    y⊆x,x : {z : Ordinal} → def (od (x , x)) z → def (od y) z
+    y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x 
+    lemma1 : osuc (& y) o< & (x , x)
+    lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c ) 
+
+ε-induction : { ψ : HOD  → Set (suc n)}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
+ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) 
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
+     ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy
+
+Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
+Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ;  u ¬a ¬b c = ⊥-elim (not c)
+_∈_ : ( A B : HOD  ) → Set n
+A ∈ B = B ∋ A
+
+OPwr :  (A :  HOD ) → HOD 
+OPwr  A = Ord ( sup-o (Ord (osuc (& A))) ( λ x A∋x → & ( A ∩ (* x)) ) )   
+
+Power : HOD  → HOD 
+Power A = Replace (OPwr (Ord (& A))) ( λ x → A ∩ x )
+-- ｛_｝ : ZFSet → ZFSet
+-- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
+
+union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+union→ X z u xx not = ⊥-elim ( not (& u) ( ⟪ proj1 xx
+    , subst ( λ k → odef k (& z)) (sym *iso) (proj2 xx) ⟫ ))
+union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+union← X z UX∋z =  FExists _ lemma UX∋z where
+    lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
+    lemma {y} xx not = not (* y) ⟪ d→∋ X (proj1 xx) , proj2 xx ⟫
+
+data infinite-d  : ( x : Ordinal  ) → Set n where
+    iφ :  infinite-d o∅
+    isuc : {x : Ordinal  } →   infinite-d  x  →
+            infinite-d  (& ( Union (* x , (* x , * x ) ) ))
+
+-- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
+-- We simply assumes infinite-d y has a maximum.
+-- 
+-- This means that many of OD may not be HODs because of the & mapping divergence.
+-- We should have some axioms to prevent this such as & x o< next (odmax x).
+-- 
+-- postulate
+--     ωmax : Ordinal
+--     <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
+-- 
+-- infinite : HOD 
+-- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ;  ¬a ¬b c with (incl lt)  (o<-subst c (sym &iso) refl )
+... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl ))
+
+ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
+ψiso {ψ} t refl = t
+selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+selection {ψ} {X} {y} = ⟪
+     ( λ cond → ⟪ proj1 cond , ψiso {ψ} (proj2 cond) (sym *iso)  ⟫ )
+  ,  ( λ select → ⟪ proj1 select  , ψiso {ψ} (proj2 select) *iso  ⟫ )
+  ⟫
+
+selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y 
+selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt)
+
+sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → & (ψ x) o< (sup-o X (λ y X∋y → & (ψ (* y))))
+sup-c< ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o< X lt )
+replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
+replacement← {ψ} X x lt = ⟪ sup-c< ψ {X} {x} lt , lemma ⟫ where 
+    lemma : def (in-codomain X ψ) (& (ψ x))
+    lemma not = ⊥-elim ( not ( & x ) ⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ )
+replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
+replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((& x) ≡ & (ψ (* y))))
+            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)))
+    lemma2 not not2  = not ( λ y d →  not2 y ⟪ proj1 d , lemma3 (proj2 d)⟫) where
+        lemma3 : {y : Ordinal } → (& x ≡ & (ψ (*  y))) → (* (& x) =h= ψ (* y))  
+        lemma3 {y} eq = subst (λ k  → * (& x) =h= k ) *iso (o≡→== eq )
+    lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)) )
+    lemma not y not2 = not (* y) (subst (λ k → k =h= ψ (* y)) *iso  ( proj2 not2 ))
+
+---
+--- Power Set
+---
+---    First consider ordinals in HOD
+---
+--- A ∩ x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
+--
+--
+∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
+∩-≡ {a} {b} inc = record {
+   eq→ = λ {x} x ¬a ¬b c = yes c
+
+open import zfc
+
+HOD→ZFC : ZFC
+HOD→ZFC   = record { 
+    ZFSet = HOD 
+    ; _∋_ = _∋_ 
+    ; _≈_ = _=h=_ 
+    ; ∅  = od∅
+    ; Select = Select
+    ; isZFC = isZFC
+ } where
+    -- infixr  200 _∈_
+    -- infixr  230 _∩_ _∪_
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
+    isZFC = record {
+       choice-func = choice-func ;
+       choice = choice
+     } where
+         -- Axiom of choice ( is equivalent to the existence of minimal in our case )
+         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 
+         choice-func : (X : HOD  ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
+         choice-func X {x} not X∋x = minimal x not
+         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A 
+         choice X {A} X∋A not = x∋minimal A not
+
diff -r 28c7be8f252c -r a5f8084b8368 src/ODUtil.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ODUtil.agda	Mon Dec 21 10:23:37 2020 +0900
@@ -0,0 +1,179 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+open import Level
+open import Ordinals
+module ODUtil {n : Level } (O : Ordinals {n} ) where
+
+open import zf
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.Nat.Properties 
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary hiding ( _⇔_ )
+
+open import logic
+open import nat
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+import OrdUtil
+open OrdUtil O
+
+import OD
+open OD O
+open OD.OD
+open ODAxiom odAxiom
+
+open HOD
+open _⊆_
+open _∧_
+open _==_
+
+cseq :  HOD  →  HOD 
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ;  ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osucz  → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z)))
+
+subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
+subset-lemma  {A} {x} = record {
+      proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
+    ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫
+   } 
+
+
+ω (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k )
+        (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
+
+ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
+ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫
+
+ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
+ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
+
+nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
+nat→ω-iso {i} = ε-induction {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
+     ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
+                                            (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
+     ind {x} prev lt = ind1 lt *iso where
+         ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
+         ind1 {o∅} iφ refl = sym o∅≡od∅
+         ind1 (isuc {x₁} ltd) ox=x = begin
+              nat→ω (ω→nato (isuc ltd) )         
+           ≡⟨⟩
+              Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
+           ≡⟨ cong (λ k → Union (k , (k , k ))) lemma  ⟩
+              Union (* x₁ , (* x₁ , * x₁))
+           ≡⟨ trans ( sym *iso) ox=x ⟩
+              x 
+           ∎ where
+               open ≡-Reasoning 
+               lemma0 :  x ∋ * x₁
+               lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not 
+                  (& (* x₁ , * x₁))  ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ )
+               lemma1 : infinite ∋ * x₁
+               lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
+               lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
+               lemma3 iφ iφ refl = HE.refl
+               lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
+               lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
+               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
+               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t  
+               lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
+               lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
+                   lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
+                   lemma6 refl HE.refl = refl
+               lemma :  nat→ω (ω→nato ltd) ≡ * x₁
+               lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
+
+ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
+ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where
+   lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡  nat→ω i → ω→nato ltd ≡ i
+   lemma {x} Zero iφ eq = refl
+   lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
+   lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅  ) *iso eq ))
+   lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- * x ≡ nat→ω i
+           lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
+           lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
+                ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
+                    (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
+
diff -r 28c7be8f252c -r a5f8084b8368 src/OPair.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/OPair.agda	Mon Dec 21 10:23:37 2020 +0900
@@ -0,0 +1,213 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Level
+open import Ordinals
+module OPair {n : Level } (O : Ordinals {n})   where
+
+open import zf
+open import logic
+import OD 
+import ODUtil
+import OrdUtil
+
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+open import Relation.Binary
+open import Relation.Binary.Core
+open import  Relation.Binary.PropositionalEquality
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+
+open OD O
+open OD.OD
+open OD.HOD
+open ODAxiom odAxiom
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
+open _∧_
+open _∨_
+open Bool
+
+open _==_
+
+<_,_> : (x y : HOD) → HOD
+< x , y > = (x , x ) , (x , y )
+
+exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
+exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
+    left : {z : Ordinal} → odef (x , y) z → odef (y , x) z 
+    left (case1 t) = case2 t
+    left (case2 t) = case1 t
+    right : {z : Ordinal} → odef (y , x) z → odef (x , y) z 
+    right (case1 t) = case2 t
+    right (case2 t) = case1 t
+
+ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
+ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )
+
+od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
+od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq )
+
+eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
+eq-prod refl refl = refl
+
+xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
+xx=zy→x=y {x} {y} eq with trio< (& x) (& y) 
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) 
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
+xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c  with eq← eq {& y} (case2 refl) 
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
+
+prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
+prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where
+    lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
+    lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq )  where
+        lemma3 : ( x , x ) =h= ( y , z )
+        lemma3 = ==-trans eq exg-pair
+    lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
+    lemma1 {x} {y} eq with eq← eq {& y} (case2 refl)
+    lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
+    lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
+    lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
+    lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl)
+    lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
+    ... | refl with lemma2 (==-sym eq )
+    ... | refl = refl
+    lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
+    lemmax : x ≡ x'
+    lemmax with eq→ eq {& (x , x)} (case1 refl) 
+    lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
+    lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
+    ... | refl = lemma1 (ord→== s )
+    lemmay : y ≡ y'
+    lemmay with lemmax
+    ... | refl with lemma4 eq -- with (x,y)≡(x,y')
+    ... | eq1 = lemma4 (ord→== (cong (λ  k → & k )  eq1 ))
+
+--
+-- unlike ordered pair, ZFProduct is not a HOD
+
+data ord-pair : (p : Ordinal) → Set n where
+   pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
+
+ZFProduct : OD
+ZFProduct = record { def = λ x → ord-pair x }
+
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
+-- eq-pair refl refl = HE.refl
+
+pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi1 ( pair x y) = x
+
+π1 : { p : HOD } → def ZFProduct (& p) → HOD
+π1 lt = * (pi1 lt )
+
+pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi2 ( pair x y ) = y
+
+π2 : { p : HOD } → def ZFProduct (& p) → HOD
+π2 lt = * (pi2 lt )
+
+op-cons :  { ox oy  : Ordinal } → def ZFProduct (& ( < * ox , * oy >   ))
+op-cons {ox} {oy} = pair ox oy
+
+def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
+def-subst df refl refl = df
+
+p-cons :  ( x y  : HOD ) → def ZFProduct (& ( < x , y >))
+p-cons x y = def-subst {_} {_} {ZFProduct} {& (< x , y >)} (pair (& x) ( & y )) refl (
+   let open ≡-Reasoning in begin
+       & < * (& x) , * (& y) >
+   ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩
+       & < x , y >
+   ∎ ) 
+
+op-iso :  { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op
+op-iso (pair ox oy) = refl
+
+p-iso :  { x  : HOD } → (p : def ZFProduct (&  x) ) → < π1 p , π2 p > ≡ x
+p-iso {x} p = ord≡→≡ (op-iso p) 
+
+p-pi1 :  { x y : HOD } → (p : def ZFProduct (&  < x , y >) ) →  π1 p ≡ x
+p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
+
+p-pi2 :  { x y : HOD } → (p : def ZFProduct (&  < x , y >) ) →  π2 p ≡ y
+p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
+
+ω-pair :  {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & (x , y) o< next m
+ω-pair lx ly = next< (omax o< next m
+ω-opair {x} {y} {m} lx ly = lemma0 where
+    lemma0 : & < x , y > o< next m
+    lemma0 = osucprev (begin
+         osuc (& < x , y >)
+       <⟨ osuc ) ))
+
+product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
+product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >)))
+             ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where
+    lemma1 :  odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >)))
+    lemma1 = replacement← B b B∋b
+    lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
+    lemma2 = replacement← A a A∋a
+
+x ¬a ¬b c = ordtrans (ω-opair  (x ¬a ¬b c = ¬b eq
+
+o<> :   {x y : Ordinal   }  →  y o< x → x o< y → ⊥
+o<> {ox} {oy} lt tl with trio< ox oy
+o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt
+o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
+o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
+
+osuc-< :  { x y : Ordinal  } → y o< osuc x  → x o< y → ⊥
+osuc-< {x} {y} y x x < osuc x   -> y = x ∨ x < y → ⊥
+osucc {ox} {oy} oy ¬a ¬b c with  osuc-≡< c
+osucc {ox} {oy} oy ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy ¬a ¬b c = ⊥-elim (o<> (osucc c) oy ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c )  )
+
+maxα :   Ordinal  →  Ordinal  → Ordinal
+maxα x y with trio< x y
+maxα x y | tri< a ¬b ¬c = y
+maxα x y | tri> ¬a ¬b c = x
+maxα x y | tri≈ ¬a refl ¬c = x
+
+omin :    Ordinal  →  Ordinal  → Ordinal
+omin  x y with trio<  x  y
+omin x y | tri< a ¬b ¬c = x
+omin x y | tri> ¬a ¬b c = y
+omin x y | tri≈ ¬a refl ¬c = x
+
+min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< omin x y
+min1  {x} {y} {z} z ¬a ¬b c = z ¬a ¬b c = osuc x
+omax  x y | tri≈ ¬a refl ¬c  = osuc x
+
+omax< :  ( x y : Ordinal  ) → x o< y → osuc y ≡ omax x y
+omax<  x y lt with trio< x y
+omax<  x y lt | tri< a ¬b ¬c = refl
+omax<  x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
+omax<  x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
+
+omax≤ :  ( x y : Ordinal  ) → x o≤ y → osuc y ≡ omax x y
+omax≤  x y le with trio< x y
+omax≤  x y le | tri< a ¬b ¬c = refl
+omax≤  x y le | tri≈ ¬a refl ¬c = refl
+omax≤  x y le | tri> ¬a ¬b c with osuc-≡< le
+omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq)
+omax≤ x y le | tri> ¬a ¬b c | case2 x ¬a ¬b c = ⊥-elim (¬b eq )
+
+omax-x :  ( x y : Ordinal  ) → x o< omax x y
+omax-x  x y with trio< x y
+omax-x  x y | tri< a ¬b ¬c = ordtrans a <-osuc
+omax-x  x y | tri> ¬a ¬b c = <-osuc
+omax-x  x y | tri≈ ¬a refl ¬c = <-osuc
+
+omax-y :  ( x y : Ordinal  ) → y o< omax x y
+omax-y  x y with  trio< x y
+omax-y  x y | tri< a ¬b ¬c = <-osuc
+omax-y  x y | tri> ¬a ¬b c = ordtrans c <-osuc
+omax-y  x y | tri≈ ¬a refl ¬c = <-osuc
+
+omxx :  ( x : Ordinal  ) → omax x x ≡ osuc x
+omxx  x with  trio< x x
+omxx  x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
+omxx  x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
+omxx  x | tri≈ ¬a refl ¬c = refl
+
+omxxx :  ( x : Ordinal  ) → omax x (omax x x ) ≡ osuc (osuc x)
+omxxx  x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
+
+open _∧_
+
+o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
+o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
+OrdTrans :  Transitive  _o≤_
+OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
+OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
+OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
+OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
+OrdTrans a≤b b≤c | case2 a ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+
+next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+next< {x} {y} {z} x ¬a ¬b c = ⊥-elim (¬nx  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
+nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
+nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx ¬a ¬b c =          -- x < y < next y < next x
+     ⊥-elim ( ¬nx ¬a ¬b c with osuc-≡< x≤y
+≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl   -- x = y < next x
+≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x ¬a ¬b c = o≤-refl (sym ( x ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc ¬a ¬b c = osuc ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
+
+record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
+  field
+    os→ : (x : Ordinal) → x o< maxordinal → Ordinal
+    os← : Ordinal → Ordinal
+    os←limit : (x : Ordinal) → os← x o< maxordinal
+    os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
+    os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
+
+module o≤-Reasoning {n : Level}  (O : Ordinals {n} )  where
+
+    -- open inOrdinal O
+
+    resp-o< : _o<_ Respects₂ _≡_
+    resp-o< =  resp₂ _o<_
+
+    trans1 : {i j k : Ordinal} → i o< j → j o< osuc  k → i o< k
+    trans1 {i} {j} {k} i ¬a ¬b c with Oprev-p  x
+   V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
+   V1 x V0 | tri> ¬a ¬b c | no ¬p = 
+        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (V0 y lt) x ) } ; odmax = x;  ¬a ¬b c with Oprev-p  x
+   L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
+   L1 x L0 | tri> ¬a ¬b c | no ¬p = 
+        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (L0 y lt) x ) } ; odmax = x;  ) ))
+
+Func :  OD
+Func = record { def = λ x → def ZFProduct x
+    ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) →  b ≡  c ) }  
+
+FuncP :  ( A B : HOD ) → HOD
+FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
+    ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } 
+       ; odmax = odmax (ZFP A B) ; ) ,  * x )))
+  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 1 >) ,  * x )))
+  he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) x
+
+record  Hω2r (x : Ordinal) : Set n where
+  field
+    count : Nat
+    hω2 : Hω2 count x
+
+open Hω2r
+
+HODω2 :  HOD
+HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ;  , ( list→hod t (Suc i) )) 
+   list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) 
+   list→hod (nothing ∷ t) i = list→hod t (Suc i ) 
+
+Hω2→3 : (x :  HOD) → HODω2 ∋ x → List (Maybe Two) 
+Hω2→3 x = lemma where
+   lemma : { y : Ordinal } →  Hω2r y → List (Maybe Two)
+   lemma record { count = 0 ; hω2 = hφ } = []
+   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 =  hω3 }
+
+ω→2 : HOD
+ω→2 = Power infinite
+
+ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
+ω→2f x lt n with ODC.∋-p O x (nat→ω n)
+ω→2f x lt n | yes p = i1
+ω→2f x lt n | no ¬p = i0
+
+fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
+fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (&  x) ) → f (ω→nat x lt) ≡ i1 )
+
+fω→2 : (Nat → Two) → HOD
+fω→2 f = Select infinite (fω→2-sel f)
+
+open _==_
+
+import Axiom.Extensionality.Propositional
+postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
+
+ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
+ω2∋f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
+
+ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
+ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
+ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
+
+open _⊆_
+
+-- someday ...
+-- postulate 
+--    ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
+--    fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
+
+record CountableOrdinal : Set (suc (suc n)) where
+   field
+       ctl→ : Nat → Ordinal
+       ctl← : Ordinal → Nat
+       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
+       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
+
+record CountableHOD : Set (suc (suc n)) where
+   field
+       mhod : HOD
+       mtl→ : Nat → Ordinal
+       mtl→∈P : (i : Nat) → odef mhod (mtl→ i)
+       mtl← : (x : Ordinal) → odef mhod x → Nat
+       mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x 
+       mtl-iso← : { x : Nat }  → mtl← (mtl→ x ) (mtl→∈P x) ≡ x
+   
+       
+open CountableOrdinal 
+open CountableHOD
+
+----
+--   a(n) ∈ M
+--   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q    
+--
+PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
+PGHOD i C P p = record { od = record { def = λ x  →
+       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
+   ; odmax = odmax (Power P)  ;  }
+--
+--   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }
+--
+
+
+
diff -r 28c7be8f252c -r a5f8084b8368 src/logic.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/logic.agda	Mon Dec 21 10:23:37 2020 +0900
@@ -0,0 +1,57 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary hiding (_⇔_ )
+open import Data.Empty
+
+data One {n : Level } : Set n where
+  OneObj : One
+
+data Two : Set where
+   i0 : Two
+   i1 : Two
+
+data Bool : Set where
+   true : Bool
+   false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   constructor ⟪_,_⟫
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
diff -r 28c7be8f252c -r a5f8084b8368 src/nat.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/nat.agda	Mon Dec 21 10:23:37 2020 +0900
@@ -0,0 +1,46 @@
+module nat where
+
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Empty
+open import Relation.Nullary
+open import  Relation.Binary.PropositionalEquality
+open import  logic
+
+
+nat-<> : { x y : Nat } → x < y → y < x → ⊥
+nat-<>  (s≤s x x→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
+>→¬< (s≤s x→¬< x : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
+trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
+trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
+
+d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
+d<→lv Φ< = refl
+d<→lv (s< lt) = refl
+
+o∅ : {n : Level} → Ordinal {n}
+o∅  = record { lv = Zero ; ord = Φ Zero }
+
+open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
+
+ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
+      lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
+ordinal-cong refl refl = refl
+
+≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
+≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
+
+trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
+trio<≡ refl = ≡→¬d<
+
+trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
+trio>≡ refl = ≡→¬d<
+
+triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
+triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
+triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
+triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> (  λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
+
+osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
+osuc record { lv = lx ; ord = ox } = record { lv = lx ; ord = OSuc lx ox }
+
+<-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
+<-osuc {n} {record { lv = lx ; ord = Φ .lx }} =  case2 Φ<
+<-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s : {n : Level} →  {x y : Ordinal {n}  }  →  y o< x → x o< y → ⊥
+o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<>  x₁ x₂
+o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁
+o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂
+o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) (case2 ())
+o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y (case2 y x₂ x₁
+osuc-< {n} {x} {y} y (case2 x ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
+   lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
+   lemma1 (case1 x) = ¬a x
+   lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) c  )
+trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
+   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
+   lemma1 refl = refl
+   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
+   lemma2 (case1 x) = ¬a x
+   lemma2 (case2 x) = trio<> x a
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
+   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
+   lemma1 refl = refl
+   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
+   lemma2 (case1 x) = ¬a x
+   lemma2 (case2 x) = trio<> x c
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
+   lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
+   lemma1 (case1 x) = ¬a x
+   lemma1 (case2 x) = ≡→¬d< x
+
+
+open _∧_
+
+TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
+  → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
+  → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
+  →  ∀ (x : Ordinal)  → ψ x
+TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where
+  TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
+  TransFinite1 Zero (Φ 0) = ⟪  caseΦ Zero lemma , lemma1 ⟫ where
+      lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
+      lemma x (case1 ())
+      lemma x (case2 ())
+      lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
+      lemma1 x (case1 ())
+      lemma1 x (case2 ())
+  TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where
+      lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
+      lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
+      lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
+      lemma lx1 ox1            (case1 lt) with <-∨ lt
+      lemma lx (Φ lx)          (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
+      lemma lx (Φ lx)          (case1 lt) | case2 lt1 = lemma0  lx (Φ lx) (case1 lt1)
+      lemma lx (OSuc lx ox1)   (case1 lt) | case1 refl = caseOSuc lx ox1 lemma2 where
+          lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx ox1) → ψ y
+          lemma2 y lt1 with osuc-≡< lt1
+          lemma2 y lt1 | case1 refl = lemma lx ox1 (case1 a