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...
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
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.
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.
Primitive. The name Empty is a term of type set.
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_0_1) We take the following as an axiom:
0 ≠ 1
In Proofgold the corresponding term root is 9630fd... and proposition id is 74867a...
Axiom. (In_0_2) We take the following as an axiom:
0 ∈ 2
In Proofgold the corresponding term root is 56dc2c... and proposition id is 5a202e...
Axiom. (In_1_2) We take the following as an axiom:
1 ∈ 2
In Proofgold the corresponding term root is 8704b3... and proposition id is 431e9e...
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_2) We take the following as an axiom:
nat_p 2
In Proofgold the corresponding term root is a8be15... and proposition id is 9112e9...
Axiom. (nat_p_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, nat_p m
In Proofgold the corresponding term root is e88449... and proposition id is 03b874...
Axiom. (cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
In Proofgold the corresponding term root is 4693b2... and proposition id is 74563a...
Primitive. The name omega is a term of type set.
In Proofgold the corresponding term root is 6fc30a... and object id is ad9ad8...
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...
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).
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...
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...
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...
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 mul_SNo is a term of type set → set → set.
In Proofgold the corresponding term root is 48d054... and object id is b14730...
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Axiom. (omega_SNo) We take the following as an axiom:
∀n ∈ omega, SNo n
In Proofgold the corresponding term root is d32269... and proposition id is d0f9c6...
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. (mul_SNo_zeroL) We take the following as an axiom:
∀x, SNo x → 0 * x = 0
In Proofgold the corresponding term root is ddc2f5... and proposition id is aaf0da...
Axiom. (mul_SNo_oneL) We take the following as an axiom:
∀x, SNo x → 1 * x = x
In Proofgold the corresponding term root is 6f8b10... and proposition id is 1b25c9...
Axiom. (mul_SNo_oneR) We take the following as an axiom:
∀x, SNo x → x * 1 = x
In Proofgold the corresponding term root is 1d2f1d... and proposition id is 5477a4...
Axiom. (mul_SNo_assoc) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x * (y * z) = (x * y) * z
In Proofgold the corresponding term root is 71a504... and proposition id is d322c1...
Beginning of Section Initial
Variable Obj : set → prop
Variable Hom : set → set → set → prop
Variable id : set → set
Variable comp : set → set → set → set → set → set
Definition. We define initial_p to be λY h ⇒ Obj Y ∧ ∀X : set, Obj X → Hom Y X (h X) ∧ ∀h' : set, Hom Y X h' → h' = h X of type set → (set → set) → prop.
In Proofgold the corresponding term root is a7ed72... and object id is f206b9...
End of Section Initial
Primitive. The name pack_b is a term of type set → (set → set → set) → set.
In Proofgold the corresponding term root is 855387... and object id is 965d60...
Definition. We define struct_b to be λS ⇒ ∀q : set → prop, (∀X : set, ∀F : set → set → set, (∀x y ∈ X, F x y ∈ X) → q (pack_b X F)) → q S of type set → prop.
In Proofgold the corresponding term root is 54dbd3... and object id is ec21da...
Axiom. (pack_struct_b_I) We take the following as an axiom:
∀X, ∀F : set → set → set, (∀x y ∈ X, F x y ∈ X) → struct_b (pack_b X F)
In Proofgold the corresponding term root is 83f82c... and proposition id is 0ca86f...
Primitive. The name unpack_b_o is a term of type set → (set → (set → set → set) → prop) → prop.
In Proofgold the corresponding term root is 0601c1... and object id is bea455...
Axiom. (unpack_b_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → prop, ∀X, ∀F : set → set → set, (∀F' : set → set → set, (∀x y ∈ X, F x y = F' x y) → Phi X F' = Phi X F) → unpack_b_o (pack_b X F) Phi = Phi X F
In Proofgold the corresponding term root is 362492... and proposition id is d10e77...
Primitive. The name Hom_struct_b is a term of type set → set → set → prop.
In Proofgold the corresponding term root is e81578... and object id is 9b88c8...
Axiom. (Hom_struct_b_pack) We take the following as an axiom:
∀X Y, ∀opX opY : set → set → set, ∀f, (Hom_struct_b (pack_b X opX) (pack_b Y opY) f) = (f ∈ YX ∧ (∀x y ∈ X, f (opX x y) = opY (f x) (f y)))
In Proofgold the corresponding term root is 7ee20a... and proposition id is 2cd8d7...
Definition. We define struct_b_monoid to be λX ⇒ struct_b X ∧ unpack_b_o X (λX' op ⇒ (∀x y z ∈ X', op (op x y) z = op x (op y z)) ∧ (∃e ∈ X', ∀x ∈ X', op x e = x ∧ op e x = x)) of type set → prop.
In Proofgold the corresponding term root is 8d1ba8... and object id is 63485b...
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_initial) We take the following as an axiom:
∃Y : set, ∃uniqa : set → set, initial_p (λ_ ⇒ True) HomSet (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa
In Proofgold the corresponding term root is 648295... and proposition id is 80cab9...
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. (LeftAdjointsPreserveInitial) We take the following as an axiom:
∀Obj : set → prop, ∀x1 : set → set → set → prop, ∀Id : set → set, ∀Comp : set → set → set → set → set → set, ∀Obj' : set → prop, ∀Hom' : set → set → set → prop, ∀Id' : set → set, ∀Comp' : 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, MetaAdjunction_strict Obj x1 Id Comp Obj' Hom' Id' Comp' F0 F1 G0 G1 eta eps → ∀Init, ∀uniq : set → set, initial_p Obj x1 Id Comp Init uniq → ∃uniq' : set → set, initial_p Obj' Hom' Id' Comp' (F0 Init) uniq'
In Proofgold the corresponding term root is 9e4a4e... and proposition id is 09501d...
Axiom. (struct_b_monoid_Phi) We take the following as an axiom:
∀X, ∀F : set → set → set, (∀x y ∈ X, F x y ∈ X) → ∀F' : set → set → set, (∀x y ∈ X, F x y = F' x y) → ((∀x y z ∈ X, F' (F' x y) z = F' x (F' y z)) ∧ (∃e ∈ X, ∀x ∈ X, F' x e = x ∧ F' e x = x)) = ((∀x y z ∈ X, F (F x y) z = F x (F y z)) ∧ (∃e ∈ X, ∀x ∈ X, F x e = x ∧ F e x = x))
In Proofgold the corresponding term root is 57c1a3... and proposition id is 271557...
Proposition. (MetaCat_struct_b_monoid_initial_neg)
¬ ∃Y : set, ∃uniqa : set → set, initial_p struct_b_monoid Hom_struct_b struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is 4b5c92... and proposition id is 872404...
Proof:
Proof not loaded.
Proposition. (MetaCat_struct_b_monoid_left_adjoint_forgetful_neg)
¬ ∃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_b_monoid Hom_struct_b struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps
In Proofgold the corresponding term root is cbb885... and proposition id is 62ee62...
Proof:
Proof not loaded.