L1
Definition. We define True to be ∀p : prop, p → p of type prop.
In Proofgold the corresponding term root is f81b39... and object id is 94e6a7...
L1
Definition. We define False to be ∀p : prop, p of type prop.
In Proofgold the corresponding term root is 1db705... and object id is 266ad5...
L2
Axiom. (FalseE) We take the following as an axiom:
False → ∀p : prop, p
In Proofgold the corresponding term root is 0dcfe3... and proposition id is f9a230...
L4
Definition. We define not to be λA : prop ⇒ A → False of type prop → prop.
In Proofgold the corresponding term root is f30435... and object id is 0dc3c7...
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
L9
Definition. We define and to be λA B : prop ⇒ ∀p : prop, (A → B → p) → p of type prop → prop → prop.
In Proofgold the corresponding term root is 2ba7d0... and object id is 37da83...
Notation. We use ∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
L14
Axiom. (andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
In Proofgold the corresponding term root is 3c4f59... and proposition id is 3bf198...
L16
Definition. We define or to be λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p of type prop → prop → prop.
In Proofgold the corresponding term root is 957746... and object id is 86ae64...
Notation. We use ∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
Beginning of Section Eq
L23
Variable A : SType
L24
Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.
L25
Definition. We define neq to be λx y : A ⇒ ¬ eq x y of type A → A → prop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use ≠ as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section Ex
L33
Variable A : SType
L34
Definition. We define ex to be λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type (A → prop) → prop.
End of Section Ex
L36
Axiom. (prop_ext_2) We take the following as an axiom:
∀p q : prop, (p → q) → (q → p) → p = q
In Proofgold the corresponding term root is a9ede2... and proposition id is a56fc7...
Primitive. The name In is a term of type set → set → prop.
Notation. We use ∈ as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write ∀ x ∈ A, B to mean ∀ x : set, x ∈ A → B.
L40
Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x ∈ B of type set → set → prop.
In Proofgold the corresponding term root is 81c0ef... and object id is 317007...
Notation. We use ⊆ as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
L45
Definition. We define nIn to be λx X ⇒ ¬ In x X of type set → set → prop.
In Proofgold the corresponding term root is 36808c... and object id is 253451...
Notation. We use ∉ as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
Primitive. The name Empty is a term of type set.
L53
Axiom. (EmptyE) We take the following as an axiom:
∀x : set, x ∉ Empty
In Proofgold the corresponding term root is 93a77a... and proposition id is 8349ab...
Primitive. The name Sing is a term of type set → set.
In Proofgold the corresponding term root is bd01a8... and object id is b7dfc1...
Notation. {x} is notation for Sing x.
L59
Axiom. (SingE) We take the following as an axiom:
∀x y : set, y ∈ {x} → y = x
In Proofgold the corresponding term root is 9341fe... and proposition id is 3b0dd8...
Primitive. The name ordsucc is a term of type set → set.
In Proofgold the corresponding term root is 65d883... and object id is 1452f7...
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
L66
Axiom. (neq_ordsucc_0) We take the following as an axiom:
∀a : set, ordsucc a ≠ 0
In Proofgold the corresponding term root is 9b391e... and proposition id is 346ee0...
L68
Axiom. (eq_1_Sing0) We take the following as an axiom:
1 = {0}
In Proofgold the corresponding term root is 5e5996... and proposition id is 264f38...
Primitive. The name nat_p is a term of type set → prop.
In Proofgold the corresponding term root is 458be3... and object id is cfd8eb...
L72
Axiom. (nat_0) We take the following as an axiom:
nat_p 0
In Proofgold the corresponding term root is 1617bc... and proposition id is 457a72...
L74
Axiom. (nat_1) We take the following as an axiom:
nat_p 1
In Proofgold the corresponding term root is 2f83fa... and proposition id is 672d0d...
L75
Axiom. (nat_inv) We take the following as an axiom:
∀n, nat_p n → n = 0 ∨ ∃x, nat_p x ∧ n = ordsucc x
In Proofgold the corresponding term root is 5d4296... and proposition id is 4f4167...
Primitive. The name omega is a term of type set.
In Proofgold the corresponding term root is 6fc30a... and object id is ad9ad8...
L79
Axiom. (omega_nat_p) We take the following as an axiom:
∀n ∈ omega, nat_p n
In Proofgold the corresponding term root is f44a30... and proposition id is c2c61b...
L81
Axiom. (nat_p_omega) We take the following as an axiom:
∀n : set, nat_p n → n ∈ omega
In Proofgold the corresponding term root is 6a1b44... and proposition id is d5080f...
L82
Axiom. (omega_ordsucc) We take the following as an axiom:
∀n ∈ omega, ordsucc n ∈ omega
In Proofgold the corresponding term root is 246d63... and proposition id is 17fb64...
Primitive. The name nat_primrec is a term of type set → (set → set → set) → set → set.
In Proofgold the corresponding term root is 3be1c5... and object id is 1a64d5...
Primitive. The name If_i is a term of type prop → set → set → set.
In Proofgold the corresponding term root is b8ff52... and object id is 76c4c0...
Notation. if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T.
L91
Axiom. (If_i_0) We take the following as an axiom:
∀p : prop, ∀x y : set, ¬ p → (if p then x else y) = y
In Proofgold the corresponding term root is fde1a8... and proposition id is a9abd3...
L94
Axiom. (If_i_1) We take the following as an axiom:
∀p : prop, ∀x y : set, p → (if p then x else y) = x
In Proofgold the corresponding term root is b1aa3f... and proposition id is a93c2c...
Primitive. The name lam is a term of type set → (set → set) → set.
In Proofgold the corresponding term root is 8acbb2... and object id is d64bcb...
L100
Definition. We define setprod to be λX Y : set ⇒ lam X (λ_ ⇒ Y) of type set → set → set.
In Proofgold the corresponding term root is fc0b60... and object id is 107b6b...
Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Primitive. The name ap is a term of type set → set → set.
In Proofgold the corresponding term root is c7aaa6... and object id is a4d82c...
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ x ∈ A ⇒ B is notation for the set lam A (λ x : set ⇒ B).
Notation. We now use n-tuple notation (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
L111
Axiom. (beta) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
In Proofgold the corresponding term root is 95991d... and proposition id is b5182d...
L113
Definition. We define lam_id to be λX ⇒ lam X (λx ⇒ x) of type set → set.
In Proofgold the corresponding term root is 627186... and object id is 86ccd7...
L115
Definition. We define lam_comp to be λX g f ⇒ lam X (λx : set ⇒ g (f x)) of type set → set → set → set.
In Proofgold the corresponding term root is 29d9e2... and object id is f47cda...
L118
Definition. We define struct_id to be λX ⇒ lam_id (X 0) of type set → set.
In Proofgold the corresponding term root is ac22e9... and object id is a097c8...
L120
Definition. We define struct_comp to be λX Y Z f g ⇒ lam_comp (X 0) f g of type set → set → set → set → set → set.
In Proofgold the corresponding term root is 1d1c1c... and object id is 9cd035...
L122
Axiom. (lam_ext) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → (λx ∈ X ⇒ F x) = (λx ∈ X ⇒ G x)
In Proofgold the corresponding term root is 2a894a... and proposition id is 15b712...
Primitive. The name Pi is a term of type set → (set → set) → set.
In Proofgold the corresponding term root is 40f1c3... and object id is a7b1b0...
Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
L130
Axiom. (lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)
In Proofgold the corresponding term root is c0b88f... and proposition id is 3733f8...
L133
Axiom. (ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x
In Proofgold the corresponding term root is 7c3617... and proposition id is cb962e...
L134
Definition. We define setexp to be λY X : set ⇒ ∏x ∈ X, Y of type set → set → set.
In Proofgold the corresponding term root is 1de7fc... and object id is 021ae0...
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
L139
Definition. We define HomSet to be λX Y f ⇒ f ∈ YX of type set → set → set → prop.
In Proofgold the corresponding term root is de8fdf... and object id is af2f63...
L141
Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.
In Proofgold the corresponding term root is 76bef6... and object id is f7d93b...
L149
Axiom. (bijI) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → bij X Y f
In Proofgold the corresponding term root is a9064f... and proposition id is 3229f9...
L155
Axiom. (bijE) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → ∀p : prop, ((∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → p) → p
In Proofgold the corresponding term root is 2cf278... and proposition id is cf0759...
Primitive. The name inv is a term of type set → (set → set) → set → set.
In Proofgold the corresponding term root is 896fa9... and object id is f3a015...
L167
Axiom. (surj_rinv) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀w ∈ Y, ∃u ∈ X, f u = w) → ∀y ∈ Y, inv X f y ∈ X ∧ f (inv X f y) = y
In Proofgold the corresponding term root is ebf371... and proposition id is 6489d2...
L169
Axiom. (inj_linv) We take the following as an axiom:
∀X, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x
In Proofgold the corresponding term root is 18ecce... and proposition id is d16557...
L171
Axiom. (bij_inv) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → bij Y X (inv X f)
In Proofgold the corresponding term root is ff1332... and proposition id is 69c537...
L173
Axiom. (ap0_lam) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ Y x) → (z 0) ∈ X
In Proofgold the corresponding term root is 861a79... and proposition id is 1affcc...
L175
Axiom. (ap1_lam) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ Y x) → (z 1) ∈ (Y (z 0))
In Proofgold the corresponding term root is ad3bfe... and proposition id is 520af5...
L177
Axiom. (tuple_2_inj) We take the following as an axiom:
∀x y w z : set, (x,y) = (w,z) → x = w ∧ y = z
In Proofgold the corresponding term root is 5a5be1... and proposition id is 8feace...
L179
Axiom. (tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y
In Proofgold the corresponding term root is e907b8... and proposition id is 1f9d7f...
L180
Axiom. (tuple_lam_eta) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z ∈ (λx ∈ X ⇒ Y x), (z 0,z 1) = z
In Proofgold the corresponding term root is 7cc266... and proposition id is d965e0...
Beginning of Section Tuples
L183
Variable x0 x1 : set
L185
Axiom. (tuple_2_0_eq) We take the following as an axiom:
(x0,x1) 0 = x0
In Proofgold the corresponding term root is 42d452... and proposition id is ad9037...
L186
Axiom. (tuple_2_1_eq) We take the following as an axiom:
(x0,x1) 1 = x1
In Proofgold the corresponding term root is 596569... and proposition id is 2c0ad1...
End of Section Tuples
Primitive. The name ordinal is a term of type set → prop.
In Proofgold the corresponding term root is ee28d9... and object id is 53ee8f...
L193
Axiom. (ordinal_Empty) We take the following as an axiom:
ordinal Empty
In Proofgold the corresponding term root is ce6bea... and proposition id is 7d95d1...
L195
Axiom. (nat_p_ordinal) We take the following as an axiom:
∀n : set, nat_p n → ordinal n
In Proofgold the corresponding term root is 274fc4... and proposition id is 47cd49...
L196
Axiom. (ordinal_ordsucc) We take the following as an axiom:
∀alpha : set, ordinal alpha → ordinal (ordsucc alpha)
In Proofgold the corresponding term root is 0ba97f... and proposition id is ab0f7f...
Primitive. The name SNo is a term of type set → prop.
In Proofgold the corresponding term root is 11faa7... and object id is 116b76...
Primitive. The name SNoLt is a term of type set → set → prop.
In Proofgold the corresponding term root is 46e7ed... and object id is 8c8aa9...
Primitive. The name SNoLe is a term of type set → set → prop.
In Proofgold the corresponding term root is ddf7d3... and object id is 54f405...
Primitive. The name minus_SNo is a term of type set → set.
In Proofgold the corresponding term root is 268a6c... and object id is 8a6d85...
Primitive. The name add_SNo is a term of type set → set → set.
In Proofgold the corresponding term root is 127d04... and object id is f62f9a...
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use <= as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
L214
Axiom. (SNoLt_irref) We take the following as an axiom:
∀x, ¬ (x < x)
In Proofgold the corresponding term root is d5ecf9... and proposition id is 06fac5...
L216
Axiom. (SNoLt_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < y → y < z → x < z
In Proofgold the corresponding term root is ac0e24... and proposition id is ccfdf7...
L217
Axiom. (SNoLeE) We take the following as an axiom:
∀x y, SNo x → SNo y → x <= y → x < y ∨ x = y
In Proofgold the corresponding term root is 1c9c62... and proposition id is 23cc47...
L219
Axiom. (SNo_0) We take the following as an axiom:
SNo 0
In Proofgold the corresponding term root is c8204b... and proposition id is 94a310...
L221
Axiom. (SNo_1) We take the following as an axiom:
SNo 1
In Proofgold the corresponding term root is ac50d7... and proposition id is 9a733a...
L222
Axiom. (SNoLt_0_1) We take the following as an axiom:
0 < 1
In Proofgold the corresponding term root is dd6047... and proposition id is cb6392...
L224
Axiom. (SNo_minus_SNo) We take the following as an axiom:
∀x, SNo x → SNo (- x)
In Proofgold the corresponding term root is 5cf7d9... and proposition id is 744cc2...
L226
Axiom. (SNo_add_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x + y)
In Proofgold the corresponding term root is c4a9a6... and proposition id is a57095...
L227
Axiom. (minus_SNo_0) We take the following as an axiom:
- 0 = 0
In Proofgold the corresponding term root is 77bc67... and proposition id is 3fcc57...
L229
Axiom. (minus_SNo_invol) We take the following as an axiom:
∀x, SNo x → - - x = x
In Proofgold the corresponding term root is 44bfe8... and proposition id is cc64ee...
L230
Axiom. (add_SNo_0R) We take the following as an axiom:
∀x, SNo x → x + 0 = x
In Proofgold the corresponding term root is d8a186... and proposition id is 1a7fa1...
L231
Axiom. (add_SNo_com) We take the following as an axiom:
∀x y, SNo x → SNo y → x + y = y + x
In Proofgold the corresponding term root is 548814... and proposition id is f017e5...
L232
Axiom. (add_SNo_Lt2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z
In Proofgold the corresponding term root is 6ad464... and proposition id is 6f0941...
L233
Axiom. (add_SNo_Lt2_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y < x + z → y < z
In Proofgold the corresponding term root is 9ecfc8... and proposition id is d4afbd...
L234
Axiom. (add_SNo_cancel_L) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y = x + z → y = z
In Proofgold the corresponding term root is 014096... and proposition id is 781256...
L236
Axiom. (add_SNo_cancel_R) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y = z + y → x = z
In Proofgold the corresponding term root is 3de43c... and proposition id is e62801...
L238
Axiom. (add_SNo_minus_SNo_rinv) We take the following as an axiom:
∀x, SNo x → x + - x = 0
In Proofgold the corresponding term root is 9e8c44... and proposition id is b2f9cf...
L240
Axiom. (minus_add_SNo_distr) We take the following as an axiom:
∀x y, SNo x → SNo y → - (x + y) = (- x) + (- y)
In Proofgold the corresponding term root is 57ec9d... and proposition id is da8d5a...
L241
Axiom. (add_SNo_minus_SNo_prop2) We take the following as an axiom:
∀x y, SNo x → SNo y → x + - x + y = y
In Proofgold the corresponding term root is 632a4d... and proposition id is a8450d...
L243
Axiom. (add_SNo_minus_R2') We take the following as an axiom:
∀x y, SNo x → SNo y → (x + - y) + y = x
In Proofgold the corresponding term root is 4f9468... and proposition id is 43b4d1...
L245
Axiom. (minus_SNo_Lt_contra) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y → - y < - x
In Proofgold the corresponding term root is 5ce52d... and proposition id is 3ebf6e...
L247
Axiom. (minus_SNo_Lt_contra3) We take the following as an axiom:
∀x y, SNo x → SNo y → - x < - y → y < x
In Proofgold the corresponding term root is 30b6d6... and proposition id is 20ebc3...
L248
Axiom. (ordinal_SNo) We take the following as an axiom:
∀alpha, ordinal alpha → SNo alpha
In Proofgold the corresponding term root is ac39bc... and proposition id is 1eea33...
L250
Axiom. (ordinal_SNoLt_In) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha < beta → alpha ∈ beta
In Proofgold the corresponding term root is d6f066... and proposition id is de775b...
L251
Axiom. (ordinal_ordsucc_SNo_eq) We take the following as an axiom:
∀alpha, ordinal alpha → ordsucc alpha = 1 + alpha
In Proofgold the corresponding term root is f0596d... and proposition id is 36bf6d...
Primitive. The name int is a term of type set.
In Proofgold the corresponding term root is 90ee85... and object id is 331669...
L256
Axiom. (nat_p_int) We take the following as an axiom:
∀n, nat_p n → n ∈ int
In Proofgold the corresponding term root is 2292ee... and proposition id is be344c...
L258
Axiom. (int_SNo) We take the following as an axiom:
∀x ∈ int, SNo x
In Proofgold the corresponding term root is 19fdd2... and proposition id is 6089ec...
L259
Axiom. (Subq_omega_int) We take the following as an axiom:
omega ⊆ int
In Proofgold the corresponding term root is 405dda... and proposition id is b1bb2b...
L260
Axiom. (int_minus_SNo) We take the following as an axiom:
∀x ∈ int, - x ∈ int
In Proofgold the corresponding term root is 00e714... and proposition id is b2c591...
L261
Axiom. (int_add_SNo) We take the following as an axiom:
∀x y ∈ int, x + y ∈ int
In Proofgold the corresponding term root is d66975... and proposition id is 1036d9...
Primitive. The name pack_u is a term of type set → (set → set) → set.
In Proofgold the corresponding term root is 119d13... and object id is 3c7a50...
Primitive. The name unpack_u_i is a term of type set → (set → (set → set) → set) → set.
In Proofgold the corresponding term root is 111dc5... and object id is 9b53a2...
L268
Axiom. (unpack_u_i_eq) We take the following as an axiom:
∀Phi : set → (set → set) → set, ∀X, ∀F : set → set, (∀F' : set → set, (∀x ∈ X, F x = F' x) → Phi X F' = Phi X F) → unpack_u_i (pack_u X F) Phi = Phi X F
In Proofgold the corresponding term root is 8381e9... and proposition id is 133f42...
Primitive. The name unpack_u_o is a term of type set → (set → (set → set) → prop) → prop.
In Proofgold the corresponding term root is eb32c2... and object id is 8b490c...
L277
Axiom. (unpack_u_o_eq) We take the following as an axiom:
∀Phi : set → (set → set) → prop, ∀X, ∀F : set → set, (∀F' : set → set, (∀x ∈ X, F x = F' x) → Phi X F' = Phi X F) → unpack_u_o (pack_u X F) Phi = Phi X F
In Proofgold the corresponding term root is a862c1... and proposition id is 3daff9...
L283
Axiom. (pack_u_0_eq2) We take the following as an axiom:
∀X, ∀F : set → set, X = pack_u X F 0
In Proofgold the corresponding term root is 079fb3... and proposition id is 7eff94...
L285
Definition. We define struct_u to be λS ⇒ ∀q : set → prop, (∀X, ∀F : set → set, (∀x ∈ X, F x ∈ X) → q (pack_u X F)) → q S of type set → prop.
In Proofgold the corresponding term root is df1429... and object id is df0642...
L287
Axiom. (pack_struct_u_I) We take the following as an axiom:
∀X, ∀F : set → set, (∀x ∈ X, F x ∈ X) → struct_u (pack_u X F)
In Proofgold the corresponding term root is 9ac1bf... and proposition id is 9556db...
Primitive. The name Hom_struct_u is a term of type set → set → set → prop.
In Proofgold the corresponding term root is 957911... and object id is 44b620...
L292
Axiom. (Hom_struct_u_pack) We take the following as an axiom:
∀X Y, ∀opX opY : set → set, ∀f, (Hom_struct_u (pack_u X opX) (pack_u Y opY) f) = (f ∈ YX ∧ (∀x ∈ X, f (opX x) = opY (f x)))
In Proofgold the corresponding term root is c0506b... and proposition id is 66c4c4...
L298
Definition. We define struct_u_bij to be λX ⇒ struct_u X ∧ unpack_u_o X (λX' h ⇒ bij X' X' (λx ⇒ h x)) of type set → prop.
In Proofgold the corresponding term root is 4f4ed8... and object id is e29a29...
Primitive. The name MetaCat is a term of type (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → prop.
In Proofgold the corresponding term root is fd9743... and object id is 1fb9aa...
L304
Axiom. (MetaCatSet) We take the following as an axiom:
MetaCat (λ_ ⇒ True) HomSet (λX ⇒ lam_id X) (λX Y Z g f ⇒ lam_comp X g f)
In Proofgold the corresponding term root is dcf573... and proposition id is e41257...
L306
Axiom. (MetaCat_struct_u_bij) We take the following as an axiom:
MetaCat struct_u_bij Hom_struct_u struct_id struct_comp
In Proofgold the corresponding term root is 97a117... and proposition id is 17fce1...
Primitive. The name MetaFunctor is a term of type (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → set) → (set → set → set → set) → prop.
In Proofgold the corresponding term root is f35b67... and object id is c80743...
L310
Axiom. (MetaFunctor_I) We take the following as an axiom:
∀C0 : set → prop, ∀C1 : set → set → set → prop, ∀idC : set → set, ∀compC : set → set → set → set → set → set, ∀D0 : set → prop, ∀D1 : set → set → set → prop, ∀idD : set → set, ∀compD : set → set → set → set → set → set, ∀F0 : set → set, ∀F1 : set → set → set → set, (∀X, C0 X → D0 (F0 X)) → (∀X Y f, C0 X → C0 Y → C1 X Y f → D1 (F0 X) (F0 Y) (F1 X Y f)) → (∀X, C0 X → F1 X X (idC X) = idD (F0 X)) → (∀X Y Z f g, C0 X → C0 Y → C0 Z → C1 X Y f → C1 Y Z g → F1 X Z (compC X Y Z g f) = compD (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)) → MetaFunctor C0 C1 idC compC D0 D1 idD compD F0 F1
In Proofgold the corresponding term root is 795e29... and proposition id is 2cb62d...
L323
Axiom. (MetaCat_struct_u_bij_Forgetful) We take the following as an axiom:
MetaFunctor struct_u_bij Hom_struct_u struct_id struct_comp (λ_ ⇒ True) HomSet (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
In Proofgold the corresponding term root is 35386a... and proposition id is ac3641...
Primitive. The name MetaFunctor_strict is a term of type (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → set) → (set → set → set → set) → prop.
In Proofgold the corresponding term root is 8085cf... and object id is 070aeb...
L332
Axiom. (MetaFunctor_strict_I) We take the following as an axiom:
∀C0 : set → prop, ∀C1 : set → set → set → prop, ∀idC : set → set, ∀compC : set → set → set → set → set → set, ∀D0 : set → prop, ∀D1 : set → set → set → prop, ∀idD : set → set, ∀compD : set → set → set → set → set → set, ∀F0 : set → set, ∀F1 : set → set → set → set, MetaCat C0 C1 idC compC → MetaCat D0 D1 idD compD → MetaFunctor C0 C1 idC compC D0 D1 idD compD F0 F1 → MetaFunctor_strict C0 C1 idC compC D0 D1 idD compD F0 F1
In Proofgold the corresponding term root is 3d0579... and proposition id is 5cbb4a...
Primitive. The name MetaNatTrans is a term of type (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → set) → (set → set → set → set) → (set → set) → (set → set → set → set) → (set → set) → prop.
In Proofgold the corresponding term root is cf0ad1... and object id is 08be86...
L346
Axiom. (MetaNatTrans_I) We take the following as an axiom:
∀C0 : set → prop, ∀C1 : set → set → set → prop, ∀idC : set → set, ∀compC : set → set → set → set → set → set, ∀D0 : set → prop, ∀D1 : set → set → set → prop, ∀idD : set → set, ∀compD : set → set → set → set → set → set, ∀F0 : set → set, ∀F1 : set → set → set → set, ∀G0 : set → set, ∀G1 : set → set → set → set, ∀eta : set → set, (∀X, C0 X → D1 (F0 X) (G0 X) (eta X)) → (∀X Y f, C0 X → C0 Y → C1 X Y f → compD (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X) = compD (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f)) → MetaNatTrans C0 C1 idC compC D0 D1 idD compD F0 F1 G0 G1 eta
In Proofgold the corresponding term root is 8286b8... and proposition id is c1d681...
Primitive. The name MetaAdjunction is a term of type (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → set) → (set → set → set → set) → (set → set) → (set → set → set → set) → (set → set) → (set → set) → prop.
In Proofgold the corresponding term root is e8b6c4... and object id is bda632...
L362
Axiom. (MetaAdjunction_I) We take the following as an axiom:
∀C0 : set → prop, ∀C1 : set → set → set → prop, ∀idC : set → set, ∀compC : set → set → set → set → set → set, ∀D0 : set → prop, ∀D1 : set → set → set → prop, ∀idD : set → set, ∀compD : set → set → set → set → set → set, ∀F0 : set → set, ∀F1 : set → set → set → set, ∀G0 : set → set, ∀G1 : set → set → set → set, ∀eta eps : set → set, (∀X, C0 X → compD (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = idD (F0 X)) → (∀Y, D0 Y → compC (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = idC (G0 Y)) → MetaAdjunction C0 C1 idC compC D0 D1 idD compD F0 F1 G0 G1 eta eps
In Proofgold the corresponding term root is 1ed388... and proposition id is fd4945...
Primitive. The name MetaAdjunction_strict is a term of type (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → (set → set) → (set → set → set → set) → (set → set) → (set → set → set → set) → (set → set) → (set → set) → prop.
In Proofgold the corresponding term root is c8ed7d... and object id is 3ab943...
L377
Axiom. (MetaAdjunction_strict_I) We take the following as an axiom:
∀C0 : set → prop, ∀C1 : set → set → set → prop, ∀idC : set → set, ∀compC : set → set → set → set → set → set, ∀D0 : set → prop, ∀D1 : set → set → set → prop, ∀idD : set → set, ∀compD : set → set → set → set → set → set, ∀F0 : set → set, ∀F1 : set → set → set → set, ∀G0 : set → set, ∀G1 : set → set → set → set, ∀eta eps : set → set, MetaFunctor_strict C0 C1 idC compC D0 D1 idD compD F0 F1 → MetaFunctor D0 D1 idD compD C0 C1 idC compC G0 G1 → MetaNatTrans C0 C1 idC compC C0 C1 idC compC (λX : set ⇒ X) (λX Y f : set ⇒ f) (λX : set ⇒ G0 (F0 X)) (λX Y f : set ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta → MetaNatTrans D0 D1 idD compD D0 D1 idD compD (λA : set ⇒ F0 (G0 A)) (λA B h : set ⇒ F1 (G0 A) (G0 B) (G1 A B h)) (λA : set ⇒ A) (λA B h : set ⇒ h) eps → MetaAdjunction C0 C1 idC compC D0 D1 idD compD F0 F1 G0 G1 eta eps → MetaAdjunction_strict C0 C1 idC compC D0 D1 idD compD F0 F1 G0 G1 eta eps
In Proofgold the corresponding term root is 712520... and proposition id is d6aa5e...
L392
Definition. We define omega_iterate to be λn h x ⇒ nat_primrec x (λ_ r ⇒ h r) n of type set → (set → set) → set → set.
In Proofgold the corresponding term root is 6ba41b... and object id is 1319be...
L395
Axiom. (omega_iterate_0) We take the following as an axiom:
∀h : set → set, ∀x, omega_iterate 0 h x = x
In Proofgold the corresponding term root is 039fc8... and proposition id is 761089...
L397
Axiom. (omega_iterate_S_out) We take the following as an axiom:
∀n ∈ omega, ∀h : set → set, ∀x, omega_iterate (ordsucc n) h x = h (omega_iterate n h x)
In Proofgold the corresponding term root is 002dbe... and proposition id is 99a2b6...
L399
Axiom. (omega_iterate_In) We take the following as an axiom:
∀X, ∀x ∈ X, ∀h : set → set, (∀x ∈ X, h x ∈ X) → ∀n, nat_p n → omega_iterate n h x ∈ X
In Proofgold the corresponding term root is 634dfe... and proposition id is acd4e8...
L403
Axiom. (omega_iterate_ext) We take the following as an axiom:
∀X, ∀x ∈ X, ∀h h' : set → set, (∀x ∈ X, h x ∈ X) → (∀x ∈ X, h x = h' x) → ∀n, nat_p n → omega_iterate n h x = omega_iterate n h' x
In Proofgold the corresponding term root is 26b5ab... and proposition id is c6fca2...
L407
Axiom. (omega_iterate_comm) We take the following as an axiom:
∀X, ∀x ∈ X, ∀h k : set → set, (∀x ∈ X, h x ∈ X) → ∀f : set → set, (∀x ∈ X, f (h x) = k (f x)) → ∀n, nat_p n → f (omega_iterate n h x) = omega_iterate n k (f x)
In Proofgold the corresponding term root is 180838... and proposition id is 9bb872...
L412
Axiom. (omega_iterate_pair_count1) We take the following as an axiom:
∀x, ∀n, nat_p n → omega_iterate n (λu ⇒ (ordsucc (u 0),u 1)) (0,x) = (n,x)
In Proofgold the corresponding term root is 346637... and proposition id is 60ada3...
L415
Axiom. (omega_iterate_pair_countback1) We take the following as an axiom:
∀x, ∀n, nat_p n → omega_iterate n (λu ⇒ (u 0 + - 1,u 1)) (0,x) = (- n,x)
In Proofgold the corresponding term root is e4081c... and proposition id is 7c549e...
L418
Definition. We define MetaCat_struct_u_forgetfree_eta to be λX ⇒ λx ∈ X ⇒ (0,x) of type set → set.
In Proofgold the corresponding term root is e04b99... and object id is 139e88...
L421
Axiom. (int_neg_or_nonneg) We take the following as an axiom:
∀x ∈ int, ∀p : prop, (x < 0 → - x ∈ omega → p) → (0 <= x → ¬ (x < 0) → x ∈ omega → p) → p
In Proofgold the corresponding term root is e922d3... and proposition id is cfaa74...
L427
Definition. We define MetaCat_struct_u_bij_free0 to be λX ⇒ pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) of type set → set.
In Proofgold the corresponding term root is fca8b5... and object id is 24e110...
L430
Definition. We define MetaCat_struct_u_bij_free1 to be λX Y h ⇒ λu ∈ int ⨯ X ⇒ (u 0,h (u 1)) of type set → set → set → set.
In Proofgold the corresponding term root is b4463b... and object id is f471c2...
L433
Definition. We define MetaCat_struct_u_bij_forgetfree_eps to be λA ⇒ unpack_u_i A (λX h ⇒ λu ∈ int ⨯ X ⇒ if u 0 < 0 then omega_iterate (- (u 0)) (inv X h) (u 1) else omega_iterate (u 0) h (u 1)) of type set → set.
In Proofgold the corresponding term root is 3777f1... and object id is 580fd3...
L436
Theorem. (MetaCat_struct_u_bij_forgetfree)
MetaAdjunction_strict (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_u_bij Hom_struct_u struct_id struct_comp MetaCat_struct_u_bij_free0 MetaCat_struct_u_bij_free1 (λX ⇒ X 0) (λX Y f ⇒ f) MetaCat_struct_u_forgetfree_eta MetaCat_struct_u_bij_forgetfree_eps
In Proofgold the corresponding term root is 3abf27... and proposition id is e50245...
Proof:
Proof not loaded.
L1312
Proposition. (MetaCat_struct_u_bij_left_adjoint_forgetful)
∃F0 : set → set, ∃F1 : set → set → set → set, ∃eta eps : set → set, MetaAdjunction_strict (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_u_bij Hom_struct_u struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps
In Proofgold the corresponding term root is 062a21... and proposition id is a69df3...
Proof:
Proof not loaded.