-title: Constructing ZF Set Theory in Agda --author: Shinji KONO --ZF in Agda zf.agda axiom of ZF zfc.agda axiom of choice Ordinals.agda axiom of Ordinals ordinal.agda countable model of Ordinals OD.agda model of ZF based on Ordinal Definable Set with assumptions ODC.agda Law of exclude middle from axiom of choice assumptions LEMC.agda model of choice with assumption of the Law of exclude middle OPair.agda ordered pair on OD BAlgbra.agda Boolean algebra on OD (not yet done) filter.agda Filter on OD (not yet done) cardinal.agda Caedinal number on OD (not yet done) logic.agda some basics on logic nat.agda some basics on Nat --Programming Mathematics Programming is processing data structure with λ terms. We are going to handle Mathematics in intuitionistic logic with λ terms. Mathematics is a functional programming which values are proofs. Programming ZF Set Theory in Agda --Target Describe ZF axioms in Agda Construction a Model of ZF Set Theory in Agda Show necessary assumptions for the model Show validities of ZF axioms on the model This shows consistency of Set Theory (with some assumptions), without circulating ZF Theory assumption. ZF in Agda https://github.com/shinji-kono/zf-in-agda --Why Set Theory If we can formulate Set theory, it suppose to work on any mathematical theory. Set Theory is a difficult point for beginners especially axiom of choice. It has some amount of difficulty and self circulating discussion. I'm planning to do it in my old age, but I'm enough age now. if you familier with Agda, you can skip to there --Agda and Intuitionistic Logic Curry Howard Isomorphism Proposition : Proof ⇔ Type : Value which means   constructing a typed lambda calculus which corresponds a logic Typed lambda calculus which allows complex type as a value of a variable (System FC)   First class Type / Dependent Type Agda is a such a programming language which has similar syntax of Haskell Coq is specialized in proof assistance such as command and tactics . --Introduction of Agda A length of a list of type A. length : {A : Set } → List A → Nat length [] = zero length (_ ∷ t) = suc ( length t ) Simple functional programming language. Type declaration is mandatory. A colon means type, an equal means value. Indentation based. Set is a base type (which may have a level ). {} means implicit variable which can be omitted if Agda infers its value. --data ( Sum type ) A data type which as exclusive multiple constructors. A similar one as union in C or case class in Scala. It has a similar syntax as Haskell but it has a slight difference. data List (A : Set ) : Set where [] : List A _∷_ : A → List A → List A _∷_ means infix operator. If use explicit _, it can be used in a normal function syntax. Natural number can be defined as a usual way. data Nat : Set where zero : Nat suc : Nat → Nat -- A → B means "A implies B" In Agda, a type can be a value of a variable, which is usually called dependent type. Type has a name Set in Agda. ex3 : {A B : Set} → Set ex3 {A}{B} = A → B ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B. A type is a formula, the value is the proof A value of A → B can be interpreted as an inference from the formula A to the formula B, which can be a function from a proof of A to a proof of B. --introduction と elimination For a logical operator, there are two types of inference, an introduction and an elimination. intro creating symbol / constructor / introduction elim using symbolic / accessors / elimination In Natural deduction, this can be written in proof schema. A : B A A → B ------------- →intro ------------------ →elim A → B B In Agda, this is a pair of type and value as follows. Introduction of → uses λ. →intro : {A B : Set } → A → B → ( A → B ) →intro _ b = λ x → b →elim : {A B : Set } → A → ( A → B ) → B →elim a f = f a Important {A B : Set } → A → B → ( A → B ) is {A B : Set } → ( A → ( B → ( A → B ) )) This makes currying of function easy. -- To prove A → B Make a left type as an argument. (intros in Coq) ex5 : {A B C : Set } → A → B → C → ? ex5 a b c = ? ? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole. We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red), insufficient proof or instance (Yellow), Non-termination, the proof is completed. -- A ∧ B Well known conjunction's introduction and elimination is as follow. A B A ∧ B A ∧ B ------------- ----------- proj1 ---------- proj2 A ∧ B A B We can introduce a corresponding structure in our functional programming language. -- record record _∧_ A B : Set field proj1 : A proj2 : B _∧_ means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) ) This a type which constructed from type A and type B. You may think this as an object or struct. record { proj1 = x ; proj2 = y } is a constructor of _∧_. ex3 : {A B : Set} → A → B → ( A ∧ B ) ex3 a b = record { proj1 = a ; proj2 = b } ex1 : {A B : Set} → ( A ∧ B ) → A ex1 a∧b = proj1 a∧b a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols except parenthesis or colons. A symbol requires space separation such as a type defining colon. Defining record can be recursively, but we don't use the recursion here. -- Mathematical structure We have types of elements and the relationship in a mathematical structure. logical relation has no ordering there is a natural ordering in arguments and a value in a function So we have typical definition style of mathematical structure with records. record IsOrdinals {n : Level} (ord : Set n) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where field Otrans : {x y z : ord } → x o< y → y o< z → x o< z record Ordinals {n : Level} : Set (suc (suc n)) where field ord : Set n _o<_ : ord → ord → Set n isOrdinal : IsOrdinals ord _o<_ In IsOrdinals, axioms are written in flat way. In Ordinal, we may have inputs and outputs are put in the field including IsOrdinal. Fields of Ordinal is existential objects in the mathematical structure. -- Limit Ordinal If an ordinal is not a succesor of other, it is called limit ordinal. We need predicate to decide it. not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) An ordinal may have an imeditate limit ordinal, we call it next x. Axiom of nrext is this. record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where field x ⊥ -> A ⊥-elim () () means no match argument nor value. A negation can be defined using ⊥ like this. ¬_ : Set → Set ¬ A = A → ⊥ --Equality All the value in Agda are terms. If we have the same normalized form, two terms are equal. If we have variables in the terms, we will perform an unification. unifiable terms are equal. We don't go further on the unification. { x : A } x ≡ y f x y --------------- ≡-intro --------------------- ≡-elim x ≡ x f x x equality _≡_ can be defined as a data. data _≡_ {A : Set } : A → A → Set where refl : {x : A} → x ≡ x The elimination of equality is a substitution in a term. subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y subst {A} {x} {y} f refl fx = fx ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y --Equivalence relation refl' : {A : Set} {x : A } → x ≡ x refl' = ? sym : {A : Set} {x y : A } → x ≡ y → y ≡ x sym = ? trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z trans = ? cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y cong = ? --Ordering Relation is a predicate on two value which has a same type. A → A → Set Defining order is the definition of this type with predicate or a data. data _≤_ : Rel ℕ 0ℓ where z≤n : ∀ {n} → zero ≤ n s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n --Quantifier Handling quantifier in an intuitionistic logic requires special cares. In the input of a function, there are no restriction on it, that is, it has a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it) There is no ∃ in agda, the one way is using negation like this.  ∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) ) On the another way, f : A can be used like this. p f If we use a function which can be defined globally which has stronger meaning the usage of ∃ x in a logical expression. --Can we do math in this way? Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support). In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF). define mathematical structure as a record program inferences as if we have proofs in variables --Things which Agda cannot prove The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which leads uniqueness of a functor in Category Theory. Functional extensionality cannot be proved. (∀ x → f x ≡ g x) → f ≡ g Agda has no law of exclude middle. a ∨ ( ¬ a ) For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot. It also other problems such as termination, type inference or unification which we may overcome with efforts or devices or may not. If we cannot prove something, we can safely postulate it unless it leads a contradiction. --Classical story of ZF Set Theory Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads a relative consistency proof of the Set Theory. Ordinal number is used in the flow. In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD). We need some non constructive assumptions in the construction. A model of Set theory is constructed based on these assumptions.
--Ordinals Ordinals are our intuition of infinite things, which has ∅ and orders on the things. It also has a successor osuc. record Ordinals {n : Level} : Set (suc (suc n)) where field ord : Set n o∅ : ord osuc : ord → ord _o<_ : ord → ord → Set n isOrdinal : IsOrdinals ord o∅ osuc _o<_ It is different from natural numbers in way. The order of Ordinals is not defined in terms of successor. It is given from outside, which make it possible to have higher order infinity. --Axiom of Ordinals Properties of infinite things. We request a transfinite induction, which states that if some properties are satisfied below all possible ordinals, the properties are true on all ordinals. Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals which is not a successor of any ordinals. It is called limit ordinal. Any two ordinal can be compared, that is less, equal or more, that is total order. record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where field Otrans : {x y z : ord } → x o< y → y o< z → x o< z OTri : Trichotomous {n} _≡_ _o<_ ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) TransFinite : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x --Concrete Ordinals or Countable Ordinals We can define a list like structure with level, which is a kind of two dimensional infinite array. data OrdinalD {n : Level} : (lv : Nat) → Set n where Φ : (lv : Nat) → OrdinalD lv OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv The order of the OrdinalD can be defined in this way. data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y This is a simple data structure, it has no abstract assumptions, and it is countable many data structure. Φ 0 OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2))) Osuc 0 (Φ 0) d< Φ 1 --Model of Ordinals It is easy to show OrdinalD and its order satisfies the axioms of Ordinals. So our Ordinals has a mode. This means axiom of Ordinals are consistent. --Debugging axioms using Model Whether axiom is correct or not can be checked by a validity on a mode. If not, we may fix the axioms or the model, such as the definitions of the order. We can also ask whether the inputs exist. --Countable Ordinals can contains uncountable set? Yes, the ordinals contains any level of infinite Set in the axioms. If we handle real-number in the model, only countable number of real-number is used. from the outside view point, it is countable from the internal view point, it is uncountable The definition of countable/uncountable is the same, but the properties are different depending on the context. We don't show the definition of cardinal number here. --What is Set The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?). From naive point view, a set i a list, but in Agda, elements have all the same type. A set in ZF may contain other Sets in ZF, which not easy to implement it as a list. Finite set may be written in finite series of ∨, but ... --We don't ask the contents of Set. It can be anything. From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on, and all of them, and again we repeat this. φ {φ} {φ,{φ}}, {φ,{φ},...} It is called V. This operation can be performed within a ZF Set theory. Classical Set Theory assumes ZF, so this kind of thing is allowed. But in our case, we have no ZF theory, so we are going to use Ordinals. The idea is to use an ordinal as a pointer to a record which defines a Set. If the recored defines a series of Ordinals which is a pointer to the Set. This record looks like a Set. --Ordinal Definable Set We can define a sbuset of Ordinals using predicates. What is a subset? a predicate has an Ordinal argument is an Ordinal Definable Set (OD). In Agda, OD is defined as follows. record OD : Set (suc n ) where field def : (x : Ordinal ) → Set n Ordinals itself is not a set in a ZF Set theory but a class. In OD, data One : Set n where OneObj : One record { def = λ x → One } means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set. You can say OD is a class in ZF Set Theory term. --OD is not ZF Set If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like a Set. The idea is to use an ordinal as a pointer to OD. Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like ¬OD-order : ( & : OD → Ordinal ) → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥ ¬OD-order & * c<→o< = ? Actualy we can prove this contrdction, so we need some restrctions on OD. This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself. -- HOD : Hereditarily Ordinal Definable What we need is a bounded OD, the containment is limited by an ordinal. record HOD : Set (suc n) where field od : OD odmax : Ordinal --Order preserving in the mapping of OD and Ordinal Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ). def (od y) ( & x ) An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements have to be smaller than the corresponding ordinal of the containing OD. We also assumes subset is always smaller. This is necessary to make a limit of Power Set. c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) If wa assumes reverse order preservation, o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (* y) x ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model.
--Various Sets In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate. Ordinal / things satisfies axiom of Ordinal / extension of natural number V / hierarchical construction of Set from φ L / hierarchical predicate definable construction of Set from φ HOD / Hereditarily Ordinal Definable OD / equational formula on Ordinals Agda Set / Type / it also has a level --Fixing ZF axom to fit intuitionistic logic We use ODs as Sets in ZF, and defines record ZF, that is, we have to define ZF axioms in Agda. It may not valid in our model. We have to debug it. Fixes are depends on axioms.
ZFのrecord --Pure logical axioms empty, pair, select, ε-induction??infinity These are logical relations among OD. empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ ) infinity∅ : ∅ ∈ infinite infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite ε-induction : { ψ : OD → Set (suc n)} → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) → (x : OD ) → ψ x finitely can be define by Agda data. data infinite-d : ( x : Ordinal ) → Set n where iφ : infinite-d o∅ isuc : {x : Ordinal } → infinite-d x → infinite-d (& ( Union (* x , (* x , * x ) ) )) Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. --Axiom of Pair In the Tanaka's book, axiom of pair is as follows. ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y) We have fix ∃ z, a function (x , y) is defined, which is _,_ . _,_ : ( A B : ZFSet ) → ZFSet using this, we can define two directions in separates axioms, like this. pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t This is already written in Agda, so we use these as axioms. All inputs have ∀. --pair in OD OD is an equation on Ordinals, we can simply write axiom of pair in the OD. _,_ : HOD → HOD → HOD x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = ? ; Agda Data Strucure as a data in Agda. Ex. 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 } pi1 : { p : Ordinal } → ord-pair p → Ordinal pi1 ( pair x y) = x π1 : { p : HOD } → def ZFProduct (& p) → HOD π1 lt = * (pi1 lt ) p-iso : { x : HOD } → (p : def ZFProduct (& x) ) → < π1 p , π2 p > ≡ x p-iso {x} p = ord≡→≡ (op-iso p) --HOD Ordrinal mapping We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger. The address of HOD can be larger at least it have to be larger than the content's address. We only have a relative ordering such as pair-xx --Possible restriction on HOD We need some restriction on the HOD-Ordinal mapping. Simple one is this. ωmax : Ordinal <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax It depends on infinite-d and put no assuption on the other similar construction. A more general one may be hod-ord< : {x : HOD } → Set n hod-ord< {x} = & x o< next (odmax x) next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and its bound. In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound. This is the reason of necessity of Axiom of infinite. --increment pase of address of HOD Assuming, hod-ord< , we have pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x) pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where lemmab0 : next (odmax (x , x)) ≡ next (& x) So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove infinite-bound : ({x : HOD} → & x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅ We also notice that if we have & (x , x) ≡ osuc (& x), c<→o< can be drived from ⊆→o≤ . ⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) ) → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) ) → {x y : HOD } → def (od y) ( & x ) → & x o< & y --Non constructive assumptions so far & : HOD → Ordinal * : Ordinal → HOD c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) oiso : {x : HOD } → * ( & x ) ≡ x diso : {x : Ordinal } → & ( * x ) ≡ x ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ --Axiom which have negation form Union, Selection These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )). Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive. Power Set axiom requires double negation, power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. --Union The original form of the Axiom of Union is ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃. 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 ))) The definition of Union in HOD is like this. Union : HOD → HOD Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x))) } ; odmax = osuc (& U) ; --Non constructive assumption in our model mapping between HOD and Ordinals & : HOD → Ordinal * : Ordinal → OD oiso : {x : HOD } → * ( & x ) ≡ x diso : {x : Ordinal } → & ( * x ) ≡ x c<→o< : {x y : HOD } → def y ( & x ) → & x o< & y ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) Equivalence on OD ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y Upper bound sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ In order to have bounded ω, hod-ord< : {x : HOD} → & x o< next (odmax x) Axiom of choice and strong axiom of regularity. minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) ) minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) ) --V The cumulative hierarchy V 0 := ∅ V α + 1 := P ( V α ) V α := ⋃ { V β | β < α } Using TransFinite induction V : ( β : Ordinal ) → HOD V β = TransFinite V1 β where V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD V1 x V0 with trio< x o∅ V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅ V1 x V0 | tri> ¬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; https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/ Foundation of axiomatic set theory (in Japanese)
https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf Agda
https://agda.readthedocs.io/en/v2.6.0.1/ ZF-in-Agda source
https://github.com/shinji-kono/zf-in-agda.git Category theory in Agda source
https://github.com/shinji-kono/category-exercise-in-agda