Definition. We define True to be ∀p : prop, p → p of type prop.
Definition. We define False to be ∀p : prop, p of type prop.
Definition. We define not to be λA : prop ⇒ A → False of type prop → prop.
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.
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
Definition. We define iff to be λA B : prop ⇒ (A → B) ∧ (B → A) of type prop → prop → prop.
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.
Definition. We define lam_id to be λX ⇒ lam X (λx ⇒ x) of type set → set.
Primitive. The name ap is a term of type set → set → set.
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.
Primitive. The name Pi is a term of type set → (set → set) → set.
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 λX Y : set ⇒ ∏y ∈ Y, X of type set → set → set.
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.
Axiom. (lam_id_exp_In) We take the following as an axiom:
∀X, lam_id X ∈ XX
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
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
Primitive. The name ordsucc is a term of type set → set.
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.
Definition. We define struct_comp to be λA B C : set ⇒ lam_comp (A 0) of type set → set → set → set → set → set.
Primitive. The name pack_r is a term of type set → (set → set → prop) → set.
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.
Axiom. (pack_r_0_eq2) We take the following as an axiom:
∀X, ∀R : set → set → prop, X = pack_r X R 0
Primitive. The name BinRelnHom is a term of type set → set → set → prop.
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))
Primitive. The name IrrPartOrd is a term of type set → prop.
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)
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
Primitive. The name MetaCat is a term of type (set → prop) → (set → set → set → prop) → (set → set) → (set → set → set → set → set → set) → prop.
Axiom. (MetaCat_Set) We take the following as an axiom:
MetaCat (λ_ ⇒ True) HomSet lam_id (λX _ _ ⇒ lam_comp X)
Axiom. (MetaCat_IrrPartOrd) We take the following as an axiom:
MetaCat IrrPartOrd BinRelnHom struct_id struct_comp
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.
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
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)
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.
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
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.
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
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.
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
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.
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
Theorem. (MetaCat_struct_r_partialord_left_adjoint_forgetful) The following is provable:
∃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
Proof:
Set F0 to be the term λX : set ⇒ pack_r X (λ_ _ ⇒ False).
Set F1 to be the term λX Y f : set ⇒ f.
Set eta to be the term λX : set ⇒ lam_id X.
Set eps to be the term λA : set ⇒ lam_id (A 0).
We use F0 to witness the existential quantifier.
We use F1 to witness the existential quantifier.
We use eta to witness the existential quantifier.
We use eps to witness the existential quantifier.
We will prove 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.
We prove the intermediate claim L1: ∀X, X = F0 X 0.
Let X be given.
An exact proof term for the current goal is pack_r_0_eq2 X (λ_ _ ⇒ False).
We prove the intermediate claim L2: ∀X Y f, HomSet X Y f → BinRelnHom (F0 X) (F0 Y) f.
Let X, Y and f be given.
Assume H1: f ∈ YX.
We will prove BinRelnHom (F0 X) (F0 Y) f.
We will prove BinRelnHom (pack_r X (λ_ _ ⇒ False)) (pack_r Y (λ_ _ ⇒ False)) f.
rewrite the current goal using BinRelnHom_eq (from left to right).
Apply andI to the current goal.
We will prove f ∈ YX.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
Assume H2: False.
An exact proof term for the current goal is H2.
We prove the intermediate claim L3: ∀X, ∀R : set → set → prop, eps (pack_r X R) = lam_id X.
Let X and R be given.
We will prove lam_id (pack_r X R 0) = lam_id X.
rewrite the current goal using pack_r_0_eq2 X R (from right to left).
Use reflexivity.
Apply MetaAdjunction_strict_I to the current goal.
We will prove MetaFunctor_strict (λX : set ⇒ True) HomSet lam_id (λX Y Z : set ⇒ lam_comp X) IrrPartOrd BinRelnHom struct_id struct_comp F0 F1.
Apply MetaFunctor_strict_I to the current goal.
We will prove MetaCat (λX : set ⇒ True) HomSet lam_id (λX Y Z : set ⇒ lam_comp X).
An exact proof term for the current goal is MetaCat_Set.
We will prove MetaCat IrrPartOrd BinRelnHom struct_id struct_comp.
An exact proof term for the current goal is MetaCat_IrrPartOrd.
We will prove MetaFunctor (λX : set ⇒ True) HomSet lam_id (λX Y Z : set ⇒ lam_comp X) IrrPartOrd BinRelnHom struct_id struct_comp F0 F1.
Apply MetaFunctor_I to the current goal.
Let X be given.
Assume _.
We will prove IrrPartOrd (F0 X).
We will prove IrrPartOrd (pack_r X (λ_ _ ⇒ False)).
Apply IrrPartOrd_I to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hxx: False.
An exact proof term for the current goal is Hxx.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Let z be given.
Assume Hz.
Assume Hxy: False.
We will prove False.
An exact proof term for the current goal is Hxy.
Let X, Y and f be given.
Assume _ _.
Assume Hf: HomSet X Y f.
We will prove BinRelnHom (F0 X) (F0 Y) (F1 X Y f).
An exact proof term for the current goal is L2 X Y f Hf.
Let X be given.
Assume _.
We will prove F1 X X (lam_id X) = struct_id (F0 X).
We will prove lam_id X = lam_id (F0 X 0).
rewrite the current goal using L1 (from right to left).
Use reflexivity.
Let X, Y, Z, f and g be given.
Assume _ _ _.
Assume Hf: f ∈ YX.
Assume Hg: g ∈ ZY.
We will prove F1 X Z (lam_comp X g f) = struct_comp (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f).
We will prove lam_comp X g f = struct_comp (F0 X) (F0 Y) (F0 Z) g f.
We will prove lam_comp X g f = lam_comp (F0 X 0) g f.
rewrite the current goal using L1 (from right to left).
Use reflexivity.
We will prove MetaFunctor IrrPartOrd BinRelnHom struct_id struct_comp (λX : set ⇒ True) HomSet lam_id (λX Y Z : set ⇒ lam_comp X) (λA : set ⇒ A 0) (λA B f : set ⇒ f).
An exact proof term for the current goal is MetaFunctor_IrrPartOrd_forgetful.
We will prove MetaNatTrans (λX : set ⇒ True) HomSet lam_id (λX Y Z : set ⇒ lam_comp X) (λX : set ⇒ True) HomSet lam_id (λX Y Z : set ⇒ lam_comp X) (λX : set ⇒ X) (λX Y f : set ⇒ f) (λX : set ⇒ F0 X 0) (λX Y f : set ⇒ F1 X Y f) eta.
Apply MetaNatTrans_I to the current goal.
Let X be given.
Assume _.
We will prove HomSet X (F0 X 0) (eta X).
rewrite the current goal using L1 (from right to left).
We will prove HomSet X X (lam_id X).
We will prove lam_id X ∈ XX.
An exact proof term for the current goal is lam_id_exp_In X.
Let X, Y and f be given.
Assume _ _.
Assume Hf: HomSet X Y f.
We will prove lam_comp X f (eta X) = lam_comp X (eta Y) f.
We will prove lam_comp X f (lam_id X) = lam_comp X (lam_id Y) f.
rewrite the current goal using lam_comp_id_L X Y f Hf (from left to right).
We will prove lam_comp X f (lam_id X) = f.
An exact proof term for the current goal is lam_comp_id_R X Y f Hf.
We will prove MetaNatTrans IrrPartOrd BinRelnHom struct_id struct_comp IrrPartOrd BinRelnHom struct_id struct_comp (λA : set ⇒ F0 (A 0)) (λA B h : set ⇒ h) (λA : set ⇒ A) (λA B h : set ⇒ h) eps.
Apply MetaNatTrans_I to the current goal.
Let A be given.
Assume HA: IrrPartOrd A.
We will prove BinRelnHom (F0 (A 0)) A (eps A).
Apply IrrPartOrd_E A HA to the current goal.
Let X and R be given.
Assume HRirr: ∀x ∈ X, ¬ R x x.
Assume HRtra: ∀x y z ∈ X, R x y → R y z → R x z.
We will prove BinRelnHom (F0 (pack_r X R 0)) (pack_r X R) (eps (pack_r X R)).
rewrite the current goal using pack_r_0_eq2 (from right to left).
We will prove BinRelnHom (pack_r X (λ_ _ ⇒ False)) (pack_r X R) (eps (pack_r X R)).
rewrite the current goal using BinRelnHom_eq (from left to right).
Apply andI to the current goal.
We will prove eps (pack_r X R) ∈ XX.
rewrite the current goal using L3 (from left to right).
We will prove lam_id X ∈ XX.
An exact proof term for the current goal is lam_id_exp_In X.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Assume Hxy: False.
We will prove False.
An exact proof term for the current goal is Hxy.
Let A, B and h be given.
Assume HA: IrrPartOrd A.
Assume HB: IrrPartOrd B.
We will prove BinRelnHom A B h → struct_comp (F0 (A 0)) A B h (eps A) = struct_comp (F0 (A 0)) (F0 (B 0)) B (eps B) h.
Apply IrrPartOrd_E A HA to the current goal.
Let X and R be given.
Assume HRirr: ∀x ∈ X, ¬ R x x.
Assume HRtra: ∀x y z ∈ X, R x y → R y z → R x z.
We will prove BinRelnHom (pack_r X R) B h → struct_comp (F0 (pack_r X R 0)) (pack_r X R) B h (eps (pack_r X R)) = struct_comp (F0 (pack_r X R 0)) (F0 (B 0)) B (eps B) h.
rewrite the current goal using pack_r_0_eq2 (from right to left).
We will prove BinRelnHom (pack_r X R) B h → struct_comp (F0 X) (pack_r X R) B h (eps (pack_r X R)) = struct_comp (F0 X) (F0 (B 0)) B (eps B) h.
Apply IrrPartOrd_E B HB to the current goal.
Let Y and Q be given.
Assume HQirr: ∀x ∈ Y, ¬ Q x x.
Assume HQtra: ∀x y z ∈ Y, Q x y → Q y z → Q x z.
We will prove BinRelnHom (pack_r X R) (pack_r Y Q) h → struct_comp (F0 X) (pack_r X R) (pack_r Y Q) h (eps (pack_r X R)) = struct_comp (F0 X) (F0 (pack_r Y Q 0)) (pack_r Y Q) (eps (pack_r Y Q)) h.
rewrite the current goal using BinRelnHom_eq (from left to right).
Assume Hh.
Apply Hh to the current goal.
Assume Hh1: h ∈ YX.
Assume Hh2: ∀x y ∈ X, R x y → Q (h x) (h y).
We will prove lam_comp (F0 X 0) h (eps (pack_r X R)) = lam_comp (F0 X 0) (eps (pack_r Y Q)) h.
rewrite the current goal using L1 (from right to left).
We will prove lam_comp X h (eps (pack_r X R)) = lam_comp X (eps (pack_r Y Q)) h.
rewrite the current goal using L3 (from left to right).
rewrite the current goal using L3 (from left to right).
We will prove lam_comp X h (lam_id X) = lam_comp X (lam_id Y) h.
rewrite the current goal using lam_comp_id_L X Y h Hh1 (from left to right).
An exact proof term for the current goal is lam_comp_id_R X Y h Hh1.
We will prove MetaAdjunction (λ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.
We prove the intermediate claim L4: ∀X, lam_comp X (lam_id X) (lam_id X) = lam_id X.
Let X be given.
Apply lam_comp_id_L to the current goal.
We will prove lam_id X ∈ XX.
An exact proof term for the current goal is lam_id_exp_In X.
Apply MetaAdjunction_I to the current goal.
Let X be given.
Assume _.
We will prove struct_comp (F0 X) (F0 (F0 X 0)) (F0 X) (eps (F0 X)) (F1 X (F0 X 0) (eta X)) = struct_id (F0 X).
We will prove lam_comp (F0 X 0) (eps (F0 X)) (eta X) = lam_id (F0 X 0).
We will prove lam_comp (F0 X 0) (lam_id (F0 X 0)) (eta X) = lam_id (F0 X 0).
rewrite the current goal using L1 (from right to left).
We will prove lam_comp X (lam_id X) (lam_id X) = lam_id X.
An exact proof term for the current goal is L4 X.
Let A be given.
Assume HA.
We will prove lam_comp (A 0) (eps A) (eta (A 0)) = lam_id (A 0).
Apply IrrPartOrd_E A HA to the current goal.
Let X and R be given.
Assume HRirr: ∀x ∈ X, ¬ R x x.
Assume HRtra: ∀x y z ∈ X, R x y → R y z → R x z.
We will prove lam_comp (pack_r X R 0) (eps (pack_r X R)) (eta (pack_r X R 0)) = lam_id (pack_r X R 0).
rewrite the current goal using pack_r_0_eq2 X R (from right to left).
We will prove lam_comp X (eps (pack_r X R)) (eta X) = lam_id X.
rewrite the current goal using L3 (from left to right).
We will prove lam_comp X (lam_id X) (lam_id X) = lam_id X.
An exact proof term for the current goal is L4 X.
∎