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...
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...
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...
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.
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.
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...
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
Variable A : SType
Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.
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
Variable A : SType
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
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.
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.
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.
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.
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.
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...
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...
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...
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...
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...
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...
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...
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.
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...
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...
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.
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...
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...
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...
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...
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...
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.
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...
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...
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.
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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
Variable x0 x1 : set
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...
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...
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...
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...
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.
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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.
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.