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