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 iff to be λA B : prop ⇒ (A → B) ∧ (B → A) of type prop → prop → prop.
In Proofgold the corresponding term root is 98aaaf... and object id is 6588e5...
Notation. We use ↔ as an infix operator with priority 805 and no associativity corresponding to applying term iff.
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.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
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
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using 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.
Primitive. The name Empty is a term of type set.
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 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...
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.
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...
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.
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...
Axiom. (lam_id_exp_In) We take the following as an axiom:
∀X, lam_id X ∈ XX
In Proofgold the corresponding term root is a328f1... and proposition id is 025740...
Axiom. (lam_comp_id_R) We take the following as an axiom:
∀X Y f, f ∈ YX → lam_comp X f (lam_id X) = f
In Proofgold the corresponding term root is 0acec2... and proposition id is b8b0cd...
Axiom. (lam_comp_id_L) We take the following as an axiom:
∀X Y f, f ∈ YX → lam_comp X (lam_id Y) f = f
In Proofgold the corresponding term root is e63b27... and proposition id is 647503...
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.
Definition. We define struct_id to be λA : set ⇒ lam_id (A 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 λA B C : set ⇒ lam_comp (A 0) of type set → set → set → set → set → set.
In Proofgold the corresponding term root is 1d1c1c... and object id is 9cd035...
Primitive. The name pack_r is a term of type set → (set → set → prop) → set.
In Proofgold the corresponding term root is 217a7f... and object id is 653348...
Definition. We define struct_r to be λS ⇒ ∀q : set → prop, (∀X : set, ∀R : set → set → prop, q (pack_r X R)) → q S of type set → prop.
In Proofgold the corresponding term root is 2c3944... and object id is 62b6df...
Axiom. (pack_r_0_eq2) We take the following as an axiom:
∀X, ∀R : set → set → prop, X = pack_r X R 0
In Proofgold the corresponding term root is e9f379... and proposition id is 09249b...
Primitive. The name BinRelnHom is a term of type set → set → set → prop.
In Proofgold the corresponding term root is acf0f0... and object id is 3f6068...
Axiom. (BinRelnHom_eq) We take the following as an axiom:
∀X Y, ∀R Q : set → set → prop, ∀h, BinRelnHom (pack_r X R) (pack_r Y Q) h = (h ∈ YX ∧ ∀x y ∈ X, R x y → Q (h x) (h y))
In Proofgold the corresponding term root is 4e4867... and proposition id is c84abf...
Primitive. The name IrrPartOrd is a term of type set → prop.
In Proofgold the corresponding term root is 64673b... and object id is adb47f...
Axiom. (IrrPartOrd_I) We take the following as an axiom:
∀X, ∀R : set → set → prop, (∀x ∈ X, ¬ R x x) → (∀x y z ∈ X, R x y → R y z → R x z) → IrrPartOrd (pack_r X R)
In Proofgold the corresponding term root is dbb637... and proposition id is b25e75...
Axiom. (IrrPartOrd_E) We take the following as an axiom:
∀A, IrrPartOrd A → ∀q : set → prop, (∀X, ∀R : set → set → prop, (∀x ∈ X, ¬ R x x) → (∀x y z ∈ X, R x y → R y z → R x z) → q (pack_r X R)) → q A
In Proofgold the corresponding term root is 2d7c7a... and proposition id is af4aa9...
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. (MetaCat_Set) We take the following as an axiom:
MetaCat (λ_ ⇒ True) HomSet lam_id (λX _ _ ⇒ lam_comp X)
In Proofgold the corresponding term root is dcf573... and proposition id is e41257...
Axiom. (MetaCat_IrrPartOrd) We take the following as an axiom:
MetaCat IrrPartOrd BinRelnHom struct_id struct_comp
In Proofgold the corresponding term root is 3cfb35... and proposition id is c6620b...
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. (MetaFunctor_IrrPartOrd_forgetful) We take the following as an axiom:
MetaFunctor IrrPartOrd BinRelnHom struct_id struct_comp (λ_ ⇒ True) HomSet lam_id (λX _ _ ⇒ lam_comp X) (λA ⇒ ap A 0) (λX Y f ⇒ f)
In Proofgold the corresponding term root is 347730... and proposition id is c7aa16...
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...
Theorem. (MetaCat_struct_r_partialord_left_adjoint_forgetful)
∃F0 : set → set, ∃F1 : set → set → set → set, ∃eta : set → set, ∃eps : set → set, MetaAdjunction_strict (λX : set ⇒ True) HomSet lam_id (λX Y Z : set ⇒ lam_comp X) IrrPartOrd BinRelnHom struct_id struct_comp F0 F1 (λA : set ⇒ A 0) (λA B f : set ⇒ f) eta eps
In Proofgold the corresponding term root is 921e16... and proposition id is 123cf0...
Proof:
Proof not loaded.