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.

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...

Beginning of Section Eq

L18

Variable A : SType

L19

Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.

L20

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

L28

Variable A : SType

L29

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.

L43

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...

L45

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...

L46

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...

L50

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...

L52

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...

L53

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...

L58

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...

L63

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).

L74

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...

L76

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...

L78

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...

L81

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...

L83

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.

L91

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...

L94

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.

L98

Definition. We define HomSet to be λX Y f ⇒ f ∈ Y^X 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.

L108

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...

L110

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...

L112

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...

L113

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...

L115

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...

L116

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...

L117

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

L121

Variable Obj : set → prop

L123

Variable Hom : set → set → set → prop

L124

Variable id : set → set

L125

Variable comp : set → set → set → set → set → set

L126

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...

L137

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...

L139

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...

L144

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...

L153

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 ∈ Y^X ∧ (∀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...

L159

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...

L170

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...

L175

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...

L195

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...

L202

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.

L334

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.