Beginning of Section MetaCat
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Definition. We define idT to be ∀X : set, Obj XHom X X (id X) of type prop.
Definition. We define compT to be ∀X Y Z : set, ∀f g : set, Obj XObj YObj ZHom X Y fHom Y Z gHom X Z (comp X Y Z g f) of type prop.
Definition. We define idL to be ∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X X Y f (id X) = f of type prop.
Definition. We define idR to be ∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X Y Y (id Y) f = f of type prop.
Definition. We define compAssoc to be ∀X Y Z W : set, ∀f g h : set, Obj XObj YObj ZObj WHom X Y fHom Y Z gHom Z W hcomp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f) of type prop.
Definition. We define MetaCat to be (idTcompT)(idLidR)compAssoc of type prop.
Theorem. (MetaCat_I)
idTcompT(∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X X Y f (id X) = f)(∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X Y Y (id Y) f = f)(∀X Y Z W : set, ∀f g h : set, Obj XObj YObj ZObj WHom X Y fHom Y Z gHom Z W hcomp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f))MetaCat
Proof:
Assume H1 H2 H3 H4 H5.
We will prove (idTcompT)(idLidR)compAssoc.
Apply and3I to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
Theorem. (MetaCat_E)
MetaCat∀p : prop, (idTcompT(∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X X Y f (id X) = f)(∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X Y Y (id Y) f = f)(∀X Y Z W : set, ∀f g h : set, Obj XObj YObj ZObj WHom X Y fHom Y Z gHom Z W hcomp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f))p)p
Proof:
Assume HC.
Let p be given.
Assume Hp.
Apply HC to the current goal.
Assume H14 H5.
Apply H14 to the current goal.
Assume H12 H34.
Apply H12 to the current goal.
Assume H1 H2.
Apply H34 to the current goal.
Assume H3 H4.
An exact proof term for the current goal is Hp H1 H2 H3 H4 H5.
End of Section MetaCat
Beginning of Section MetaCatOp
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Theorem. (MetaCatOp)
MetaCat Obj Hom id compMetaCat Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f)
Proof:
Assume HC.
Apply MetaCat_E Obj Hom id comp HC to the current goal.
Assume HC1: ∀X : set, Obj XHom X X (id X).
Assume HC2: ∀X Y Z : set, ∀f g : set, Obj XObj YObj ZHom X Y fHom Y Z gHom X Z (comp X Y Z g f).
Assume HC3: ∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X X Y f (id X) = f.
Assume HC4: ∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X Y Y (id Y) f = f.
Assume HC5: ∀X Y Z W : set, ∀f g h : set, Obj XObj YObj ZObj WHom X Y fHom Y Z gHom Z W hcomp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f).
Apply MetaCat_I to the current goal.
An exact proof term for the current goal is HC1.
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
An exact proof term for the current goal is HC2 Z Y X g f HZ HY HX Hg Hf.
Let X, Y and f be given.
Assume HX HY Hf.
An exact proof term for the current goal is HC4 Y X f HY HX Hf.
Let X, Y and f be given.
Assume HX HY Hf.
An exact proof term for the current goal is HC3 Y X f HY HX Hf.
Let X, Y, Z, W, f, g and h be given.
Assume HX HY HZ HW Hf Hg Hh.
We will prove comp W Y X f (comp W Z Y g h) = comp W Z X (comp Z Y X f g) h.
Use symmetry.
An exact proof term for the current goal is HC5 W Z Y X h g f HW HZ HY HX Hh Hg Hf.
End of Section MetaCatOp
Beginning of Section LimsCoLims
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Definition. We define monic to be λX Y f ⇒ Obj XObj YHom X Y f∀Z : set, Obj Z∀g h : set, Hom Z X gHom Z X hcomp Z X Y f g = comp Z X Y f hg = h of type setsetsetprop.
Definition. We define terminal_p to be λY h ⇒ Obj Y∀X : set, Obj XHom X Y (h X)∀h' : set, Hom X Y h'h' = h X of type set(setset)prop.
Definition. We define initial_p to be λY h ⇒ Obj Y∀X : set, Obj XHom Y X (h X)∀h' : set, Hom Y X h'h' = h X of type set(setset)prop.
Definition. We define product_p to be λX Y Z pi0 pi1 pair ⇒ Obj XObj YObj ZHom Z X pi0Hom Z Y pi1∀W : set, Obj W∀h k : set, Hom W X hHom W Y kHom W Z (pair W h k)comp W Z X pi0 (pair W h k) = hcomp W Z Y pi1 (pair W h k) = k∀u : set, Hom W Z ucomp W Z X pi0 u = hcomp W Z Y pi1 u = ku = pair W h k of type setsetsetsetset(setsetsetset)prop.
Definition. We define product_constr_p to be λprod pi0 pi1 pair ⇒ ∀X Y : set, Obj XObj Yproduct_p X Y (prod X Y) (pi0 X Y) (pi1 X Y) (pair X Y) of type (setsetset)(setsetset)(setsetset)(setsetsetsetsetset)prop.
Definition. We define coproduct_p to be λX Y Z i0 i1 comb ⇒ Obj XObj YObj ZHom X Z i0Hom Y Z i1∀W : set, Obj W∀h k : set, Hom X W hHom Y W kHom Z W (comb W h k)comp X Z W (comb W h k) i0 = hcomp Y Z W (comb W h k) i1 = k∀hk : set, Hom Z W hkcomp X Z W hk i0 = hcomp Y Z W hk i1 = khk = comb W h k of type setsetsetsetset(setsetsetset)prop.
Definition. We define coproduct_constr_p to be λcoprod i0 i1 copair ⇒ ∀X Y : set, Obj XObj Ycoproduct_p X Y (coprod X Y) (i0 X Y) (i1 X Y) (copair X Y) of type (setsetset)(setsetset)(setsetset)(setsetsetsetsetset)prop.
Definition. We define equalizer_p to be λX Y f g Q q fac ⇒ Obj XObj YHom X Y fHom X Y gObj QHom Q X qcomp Q X Y f q = comp Q X Y g q∀W : set, Obj W∀h : set, Hom W X hcomp W X Y f h = comp W X Y g hHom W Q (fac W h)comp W Q X q (fac W h) = h∀u : set, Hom W Q ucomp W Q X q u = hu = fac W h of type setsetsetsetsetset(setsetset)prop.
Definition. We define equalizer_constr_p to be λquot canonmap fac ⇒ ∀X Y : set, Obj XObj Y∀f g : set, Hom X Y fHom X Y gequalizer_p X Y f g (quot X Y f g) (canonmap X Y f g) (fac X Y f g) of type (setsetsetsetset)(setsetsetsetset)(setsetsetsetsetsetset)prop.
Definition. We define coequalizer_p to be λX Y f g Q q fac ⇒ Obj XObj YHom X Y fHom X Y gObj QHom Y Q qcomp X Y Q q f = comp X Y Q q g∀W : set, Obj W∀h : set, Hom Y W hcomp X Y W h f = comp X Y W h gHom Q W (fac W h)comp Y Q W (fac W h) q = h∀u : set, Hom Q W ucomp Y Q W u q = hu = fac W h of type setsetsetsetsetset(setsetset)prop.
Definition. We define coequalizer_constr_p to be λquot canonmap fac ⇒ ∀X Y : set, Obj XObj Y∀f g : set, Hom X Y fHom X Y gcoequalizer_p X Y f g (quot X Y f g) (canonmap X Y f g) (fac X Y f g) of type (setsetsetsetset)(setsetsetsetset)(setsetsetsetsetsetset)prop.
Definition. We define pullback_p to be λX Y Z f g P pi0 pi1 pair ⇒ Obj XObj YObj ZHom X Z fHom Y Z gObj PHom P X pi0Hom P Y pi1comp P X Z f pi0 = comp P Y Z g pi1∀W : set, Obj W∀h : set, Hom W X h∀k : set, Hom W Y kcomp W X Z f h = comp W Y Z g kHom W P (pair W h k)comp W P X pi0 (pair W h k) = hcomp W P Y pi1 (pair W h k) = k∀u : set, Hom W P ucomp W P X pi0 u = hcomp W P Y pi1 u = ku = pair W h k of type setsetsetsetsetsetsetset(setsetsetset)prop.
Definition. We define pullback_constr_p to be λpb pi0 pi1 pair ⇒ ∀X Y Z : set, Obj XObj YObj Z∀f g : set, Hom X Z fHom Y Z gpullback_p X Y Z f g (pb X Y Z f g) (pi0 X Y Z f g) (pi1 X Y Z f g) (pair X Y Z f g) of type (setsetsetsetsetset)(setsetsetsetsetset)(setsetsetsetsetset)(setsetsetsetsetsetsetsetset)prop.
Definition. We define pushout_p to be λX Y Z f g P i0 i1 copair ⇒ Obj XObj YObj ZHom Z X fHom Z Y gObj PHom X P i0Hom Y P i1comp Z X P i0 f = comp Z Y P i1 g∀W : set, Obj W∀h : set, Hom X W h∀k : set, Hom Y W kcomp Z X W h f = comp Z Y W k gHom P W (copair W h k)comp X P W (copair W h k) i0 = hcomp Y P W (copair W h k) i1 = k∀u : set, Hom P W ucomp X P W u i0 = hcomp Y P W u i1 = ku = copair W h k of type setsetsetsetsetsetsetset(setsetsetset)prop.
Definition. We define pushout_constr_p to be λpo i0 i1 copair ⇒ ∀X Y Z : set, Obj XObj YObj Z∀f g : set, Hom Z X fHom Z Y gpushout_p X Y Z f g (po X Y Z f g) (i0 X Y Z f g) (i1 X Y Z f g) (copair X Y Z f g) of type (setsetsetsetsetset)(setsetsetsetsetset)(setsetsetsetsetset)(setsetsetsetsetsetsetsetset)prop.
Definition. We define exponent_p to be λprod pi0 pi1 pair X Y Z a lm ⇒ Obj XObj YObj ZHom (prod Z X) Y a∀W : set, Obj W∀f : set, Hom (prod W X) Y fHom W Z (lm W f)comp (prod W X) (prod Z X) Y a (pair Z X (prod W X) (comp (prod W X) W Z (lm W f) (pi0 W X)) (pi1 W X)) = f∀g : set, Hom W Z gcomp (prod W X) (prod Z X) Y a (pair Z X (prod W X) (comp (prod W X) W Z g (pi0 W X)) (pi1 W X)) = fg = lm W f of type (setsetset)(setsetset)(setsetset)(setsetsetsetsetset)setsetsetset(setsetset)prop.
Definition. We define product_exponent_constr_p to be λprod pi0 pi1 pair exp a lm ⇒ product_constr_p prod pi0 pi1 pair∀X Y : set, Obj XObj Yexponent_p prod pi0 pi1 pair X Y (exp X Y) (a X Y) (lm X Y) of type (setsetset)(setsetset)(setsetset)(setsetsetsetsetset)(setsetset)(setsetset)(setsetsetsetset)prop.
Definition. We define subobject_classifier_p to be λone uniqa Omega tru ch constr_p ⇒ terminal_p one uniqaObj OmegaHom one Omega tru∀X Y : set, ∀m : set, monic X Y mHom Y Omega (ch X Y m)pullback_p one Y Omega tru (ch X Y m) X (uniqa X) m (constr_p X Y m) of type set(setset)setset(setsetsetset)(setsetsetsetsetsetset)prop.
Definition. We define nno_p to be λone uniqa N zer suc rec ⇒ terminal_p one uniqaObj NHom one N zerHom N N suc∀X : set, ∀x : set, ∀f : set, Obj XHom one X xHom X X fHom N X (rec X x f)comp one N X (rec X x f) zer = xcomp N N X (rec X x f) suc = comp N X X f (rec X x f)∀u : set, Hom N X ucomp one N X u zer = xcomp N N X u suc = comp N X X f uu = rec X x f of type set(setset)setsetset(setsetsetset)prop.
End of Section LimsCoLims
Beginning of Section LimsCoLims2
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Theorem. (product_coproduct_Op)
∀X Y Z : set, ∀pi0 pi1 : set, ∀pair : setsetsetset, product_p Obj Hom id comp X Y Z pi0 pi1 paircoproduct_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) X Y Z pi0 pi1 pair
Proof:
Let X, Y, Z, pi0, pi1 and pair be given.
Assume H1.
An exact proof term for the current goal is H1.
Theorem. (product_coproduct_constr_Op)
∀prod : setsetset, ∀pi0 pi1 : setsetset, ∀pair : setsetsetsetsetset, product_constr_p Obj Hom id comp prod pi0 pi1 paircoproduct_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) prod pi0 pi1 pair
Proof:
Let prod, pi0, pi1 and pair be given.
Assume H1.
An exact proof term for the current goal is H1.
Theorem. (coproduct_product_Op)
∀X Y Z : set, ∀i0 i1 : set, ∀copair : setsetsetset, coproduct_p Obj Hom id comp X Y Z i0 i1 copairproduct_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) X Y Z i0 i1 copair
Proof:
Let X, Y, Z, i0, i1 and copair be given.
Assume H1.
An exact proof term for the current goal is H1.
Theorem. (coproduct_product_constr_Op)
∀coprod : setsetset, ∀i0 i1 : setsetset, ∀copair : setsetsetsetsetset, coproduct_constr_p Obj Hom id comp coprod i0 i1 copairproduct_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) coprod i0 i1 copair
Proof:
Let coprod, i0, i1 and copair be given.
Assume H1.
An exact proof term for the current goal is H1.
Theorem. (equalizer_coequalizer_Op)
∀X Y : set, ∀f g : set, ∀Q : set, ∀q : set, ∀fac : setsetset, equalizer_p Obj Hom id comp X Y f g Q q faccoequalizer_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) Y X f g Q q fac
Proof:
Let X, Y, f, g, Q, q and fac be given.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE1: Obj X.
Assume HE2: Obj Y.
Assume HE3: Hom X Y f.
Assume HE4: Hom X Y g.
Assume HE5: Obj Q.
Assume HE6: Hom Q X q.
Assume HE7: comp Q X Y f q = comp Q X Y g q.
Assume HE8: ∀W : set, Obj W∀h : set, Hom W X hcomp W X Y f h = comp W X Y g hHom W Q (fac W h)comp W Q X q (fac W h) = h∀u : set, Hom W Q ucomp W Q X q u = hu = fac W h.
We will prove Obj YObj XHom X Y fHom X Y gObj QHom Q X qcomp Q X Y f q = comp Q X Y g q∀W : set, Obj W∀h : set, Hom W X hcomp W X Y f h = comp W X Y g hHom W Q (fac W h)comp W Q X q (fac W h) = h∀u : set, Hom W Q ucomp W Q X q u = hu = fac W h.
Apply and8I to the current goal.
An exact proof term for the current goal is HE2.
An exact proof term for the current goal is HE1.
An exact proof term for the current goal is HE3.
An exact proof term for the current goal is HE4.
An exact proof term for the current goal is HE5.
An exact proof term for the current goal is HE6.
An exact proof term for the current goal is HE7.
An exact proof term for the current goal is HE8.
Theorem. (equalizer_coequalizer_constr_Op)
∀quot : setsetsetsetset, ∀canonmap : setsetsetsetset, ∀fac : setsetsetsetsetsetset, equalizer_constr_p Obj Hom id comp quot canonmap faccoequalizer_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) (λX Y f g ⇒ quot Y X f g) (λX Y f g ⇒ canonmap Y X f g) (λX Y f g ⇒ fac Y X f g)
Proof:
Let quot, canonmap and fac be given.
Assume HE.
Let X and Y be given.
Assume HX HY.
Let f and g be given.
Assume Hf Hg.
An exact proof term for the current goal is equalizer_coequalizer_Op Y X f g (quot Y X f g) (canonmap Y X f g) (fac Y X f g) (HE Y X HY HX f g Hf Hg).
Theorem. (coequalizer_equalizer_Op)
∀X Y : set, ∀f g : set, ∀Q : set, ∀q : set, ∀fac : setsetset, coequalizer_p Obj Hom id comp X Y f g Q q facequalizer_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) Y X f g Q q fac
Proof:
Let X, Y, f, g, Q, q and fac be given.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE1: Obj X.
Assume HE2: Obj Y.
Assume HE3: Hom X Y f.
Assume HE4: Hom X Y g.
Assume HE5: Obj Q.
Assume HE6: Hom Y Q q.
Assume HE7: comp X Y Q q f = comp X Y Q q g.
Assume HE8: ∀W : set, Obj W∀h : set, Hom Y W hcomp X Y W h f = comp X Y W h gHom Q W (fac W h)comp Y Q W (fac W h) q = h∀u : set, Hom Q W ucomp Y Q W u q = hu = fac W h.
We will prove Obj YObj XHom X Y fHom X Y gObj QHom Y Q qcomp X Y Q q f = comp X Y Q q g∀W : set, Obj W∀h : set, Hom Y W hcomp X Y W h f = comp X Y W h gHom Q W (fac W h)comp Y Q W (fac W h) q = h∀u : set, Hom Q W ucomp Y Q W u q = hu = fac W h.
Apply and8I to the current goal.
An exact proof term for the current goal is HE2.
An exact proof term for the current goal is HE1.
An exact proof term for the current goal is HE3.
An exact proof term for the current goal is HE4.
An exact proof term for the current goal is HE5.
An exact proof term for the current goal is HE6.
An exact proof term for the current goal is HE7.
An exact proof term for the current goal is HE8.
Theorem. (coequalizer_equalizer_constr_Op)
∀quot : setsetsetsetset, ∀canonmap : setsetsetsetset, ∀fac : setsetsetsetsetsetset, coequalizer_constr_p Obj Hom id comp quot canonmap facequalizer_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) (λX Y f g ⇒ quot Y X f g) (λX Y f g ⇒ canonmap Y X f g) (λX Y f g ⇒ fac Y X f g)
Proof:
Let quot, canonmap and fac be given.
Assume HE.
Let X and Y be given.
Assume HX HY.
Let f and g be given.
Assume Hf Hg.
An exact proof term for the current goal is coequalizer_equalizer_Op Y X f g (quot Y X f g) (canonmap Y X f g) (fac Y X f g) (HE Y X HY HX f g Hf Hg).
Theorem. (pullback_pushout_Op)
∀X Y Z : set, ∀f g : set, ∀P : set, ∀pi0 pi1 : set, ∀pair : setsetsetset, pullback_p Obj Hom id comp X Y Z f g P pi0 pi1 pairpushout_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) X Y Z f g P pi0 pi1 pair
Proof:
Let X, Y, Z, f, g, P, pi0, pi1 and pair be given.
Assume HP.
An exact proof term for the current goal is HP.
Theorem. (pullback_pushout_constr_Op)
∀pb : setsetsetsetsetset, ∀pi0 pi1 : setsetsetsetsetset, ∀pair : setsetsetsetsetsetsetsetset, pullback_constr_p Obj Hom id comp pb pi0 pi1 pairpushout_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) pb pi0 pi1 pair
Proof:
Let pb, pi0, pi1 and pair be given.
Assume HP.
An exact proof term for the current goal is HP.
Theorem. (pushout_pullback_Op)
∀X Y Z : set, ∀f g : set, ∀P : set, ∀i0 i1 : set, ∀copair : setsetsetset, pushout_p Obj Hom id comp X Y Z f g P i0 i1 copairpullback_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) X Y Z f g P i0 i1 copair
Proof:
Let X, Y, Z, f, g, P, i0, i1 and copair be given.
Assume HP.
An exact proof term for the current goal is HP.
Theorem. (pushout_pullback_constr_Op)
∀po : setsetsetsetsetset, ∀i0 i1 : setsetsetsetsetset, ∀copair : setsetsetsetsetsetsetsetset, pushout_constr_p Obj Hom id comp po i0 i1 copairpullback_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) po i0 i1 copair
Proof:
Let po, i0, i1 and copair be given.
Assume HP.
An exact proof term for the current goal is HP.
Theorem. (product_equalizer_pullback_constr)
MetaCat Obj Hom id comp∀quot : setsetsetsetset, ∀canonmap : setsetsetsetset, ∀fac : setsetsetsetsetsetset, equalizer_constr_p Obj Hom id comp quot canonmap fac∀prod : setsetset, ∀pi0 : setsetset, ∀pi1 : setsetset, ∀pair : setsetsetsetsetset, product_constr_p Obj Hom id comp prod pi0 pi1 pairpullback_constr_p Obj Hom id comp (λX Y Z f g ⇒ quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) (λX Y Z f g ⇒ comp (quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)))) (λX Y Z f g ⇒ comp (quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)))) (λX Y Z f g W h k ⇒ fac (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)) W (pair X Y W h k))
Proof:
Assume HC.
Apply MetaCat_E Obj Hom id comp HC to the current goal.
Assume HC1: ∀X : set, Obj XHom X X (id X).
Assume HC2: ∀X Y Z : set, ∀f g : set, Obj XObj YObj ZHom X Y fHom Y Z gHom X Z (comp X Y Z g f).
Assume HC3: ∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X X Y f (id X) = f.
Assume HC4: ∀X Y : set, ∀f : set, Obj XObj YHom X Y fcomp X Y Y (id Y) f = f.
Assume HC5: ∀X Y Z W : set, ∀f g h : set, Obj XObj YObj ZObj WHom X Y fHom Y Z gHom Z W hcomp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f).
Let quot, canonmap and fac be given.
Assume HE: equalizer_constr_p Obj Hom id comp quot canonmap fac.
Let prod, pi0, pi1 and pair be given.
Assume HP: product_constr_p Obj Hom id comp prod pi0 pi1 pair.
Let X, Y and Z be given.
Assume HX: Obj X.
Assume HY: Obj Y.
Assume HZ: Obj Z.
Let f and g be given.
Assume Hf: Hom X Z f.
Assume Hg: Hom Y Z g.
Set pi0f to be the term comp (prod X Y) X Z f (pi0 X Y).
Set pi1g to be the term comp (prod X Y) Y Z g (pi1 X Y).
Set P to be the term quot (prod X Y) Z pi0f pi1g.
Set pi0P to be the term comp P (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z pi0f pi1g).
Set pi1P to be the term comp P (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z pi0f pi1g).
Set pairP to be the term (λW : setλh k : setfac (prod X Y) Z pi0f pi1g W (pair X Y W h k)).
Apply HP X Y HX HY to the current goal.
Assume HP1.
Apply HP1 to the current goal.
Assume HP1.
Apply HP1 to the current goal.
Assume HP1.
Apply HP1 to the current goal.
Assume HP1.
Apply HP1 to the current goal.
Assume _ _.
Assume HP1: Obj (prod X Y).
Assume HP2: Hom (prod X Y) X (pi0 X Y).
Assume HP3: Hom (prod X Y) Y (pi1 X Y).
Assume HP4: ∀W : set, Obj W∀h k : set, Hom W X hHom W Y kHom W (prod X Y) (pair X Y W h k)comp W (prod X Y) X (pi0 X Y) (pair X Y W h k) = hcomp W (prod X Y) Y (pi1 X Y) (pair X Y W h k) = k∀u : set, Hom W (prod X Y) ucomp W (prod X Y) X (pi0 X Y) u = hcomp W (prod X Y) Y (pi1 X Y) u = ku = pair X Y W h k.
We prove the intermediate claim Lpi0f: Hom (prod X Y) Z pi0f.
An exact proof term for the current goal is HC2 (prod X Y) X Z (pi0 X Y) f HP1 HX HZ HP2 Hf.
We prove the intermediate claim Lpi1g: Hom (prod X Y) Z pi1g.
An exact proof term for the current goal is HC2 (prod X Y) Y Z (pi1 X Y) g HP1 HY HZ HP3 Hg.
Apply HE (prod X Y) Z HP1 HZ pi0f pi1g Lpi0f Lpi1g to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume _ _ _ _.
Assume HE1: Obj P.
Assume HE2: Hom P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g).
Assume HE3: comp P (prod X Y) Z pi0f (canonmap (prod X Y) Z pi0f pi1g) = comp P (prod X Y) Z pi1g (canonmap (prod X Y) Z pi0f pi1g).
Assume HE4: ∀W : set, Obj W∀h : set, Hom W (prod X Y) hcomp W (prod X Y) Z pi0f h = comp W (prod X Y) Z pi1g hHom W P (fac (prod X Y) Z pi0f pi1g W h)comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) (fac (prod X Y) Z pi0f pi1g W h) = h∀u : set, Hom W P ucomp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u = hu = fac (prod X Y) Z pi0f pi1g W h.
We prove the intermediate claim Lpi0P: Hom P X pi0P.
An exact proof term for the current goal is HC2 P (prod X Y) X (canonmap (prod X Y) Z pi0f pi1g) (pi0 X Y) HE1 HP1 HX HE2 HP2.
We prove the intermediate claim Lpi1P: Hom P Y pi1P.
An exact proof term for the current goal is HC2 P (prod X Y) Y (canonmap (prod X Y) Z pi0f pi1g) (pi1 X Y) HE1 HP1 HY HE2 HP3.
We will prove pullback_p Obj Hom id comp X Y Z f g P pi0P pi1P pairP.
We will prove Obj XObj YObj ZHom X Z fHom Y Z gObj PHom P X pi0PHom P Y pi1Pcomp P X Z f pi0P = comp P Y Z g pi1P∀W : set, Obj W∀h : set, Hom W X h∀k : set, Hom W Y kcomp W X Z f h = comp W Y Z g kHom W P (pairP W h k)comp W P X pi0P (pairP W h k) = hcomp W P Y pi1P (pairP W h k) = k∀u : set, Hom W P ucomp W P X pi0P u = hcomp W P Y pi1P u = ku = pairP W h k.
Apply and10I to the current goal.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is HZ.
An exact proof term for the current goal is Hf.
An exact proof term for the current goal is Hg.
We will prove Obj P.
An exact proof term for the current goal is HE1.
We will prove Hom P X pi0P.
An exact proof term for the current goal is Lpi0P.
We will prove Hom P Y pi1P.
An exact proof term for the current goal is Lpi1P.
We will prove comp P X Z f pi0P = comp P Y Z g pi1P.
We will prove comp P X Z f (comp P (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z pi0f pi1g)) = comp P Y Z g (comp P (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z pi0f pi1g)).
Use transitivity with comp P (prod X Y) Z pi0f (canonmap (prod X Y) Z pi0f pi1g), and comp P (prod X Y) Z pi1g (canonmap (prod X Y) Z pi0f pi1g).
Use symmetry.
Apply HC5 to the current goal.
An exact proof term for the current goal is HE1.
An exact proof term for the current goal is HP1.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HZ.
An exact proof term for the current goal is HE2.
An exact proof term for the current goal is HP2.
An exact proof term for the current goal is Hf.
We will prove comp P (prod X Y) Z pi0f (canonmap (prod X Y) Z pi0f pi1g) = comp P (prod X Y) Z pi1g (canonmap (prod X Y) Z pi0f pi1g).
An exact proof term for the current goal is HE3.
Apply HC5 to the current goal.
An exact proof term for the current goal is HE1.
An exact proof term for the current goal is HP1.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is HZ.
An exact proof term for the current goal is HE2.
An exact proof term for the current goal is HP3.
An exact proof term for the current goal is Hg.
Let W be given.
Assume HW: Obj W.
Let h be given.
Assume Hh: Hom W X h.
Let k be given.
Assume Hk: Hom W Y k.
Assume Hhk: comp W X Z f h = comp W Y Z g k.
Apply HP4 W HW h k Hh Hk to the current goal.
Assume HP4a.
Apply HP4a to the current goal.
Assume HP4a.
Apply HP4a to the current goal.
Assume HP4a: Hom W (prod X Y) (pair X Y W h k).
Assume HP4b: comp W (prod X Y) X (pi0 X Y) (pair X Y W h k) = h.
Assume HP4c: comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k) = k.
Assume HP4d: ∀u : set, Hom W (prod X Y) ucomp W (prod X Y) X (pi0 X Y) u = hcomp W (prod X Y) Y (pi1 X Y) u = ku = pair X Y W h k.
We prove the intermediate claim LP1: comp W (prod X Y) Z pi0f (pair X Y W h k) = comp W (prod X Y) Z pi1g (pair X Y W h k).
Use transitivity with comp W X Z f (comp W (prod X Y) X (pi0 X Y) (pair X Y W h k)), and comp W Y Z g (comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k)).
An exact proof term for the current goal is HC5 W (prod X Y) X Z (pair X Y W h k) (pi0 X Y) f HW HP1 HX HZ HP4a HP2 Hf.
We will prove comp W X Z f (comp W (prod X Y) X (pi0 X Y) (pair X Y W h k)) = comp W Y Z g (comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k)).
rewrite the current goal using HP4b (from left to right).
rewrite the current goal using HP4c (from left to right).
We will prove comp W X Z f h = comp W Y Z g k.
An exact proof term for the current goal is Hhk.
Use symmetry.
An exact proof term for the current goal is HC5 W (prod X Y) Y Z (pair X Y W h k) (pi1 X Y) g HW HP1 HY HZ HP4a HP3 Hg.
Apply HE4 W HW (pair X Y W h k) HP4a LP1 to the current goal.
Assume HE4a.
Apply HE4a to the current goal.
Assume HE4a: Hom W P (fac (prod X Y) Z pi0f pi1g W (pair X Y W h k)).
Assume HE4b: comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) (fac (prod X Y) Z pi0f pi1g W (pair X Y W h k)) = pair X Y W h k.
Assume HE4c: ∀u : set, Hom W P ucomp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u = pair X Y W h ku = fac (prod X Y) Z pi0f pi1g W (pair X Y W h k).
We prove the intermediate claim Lhk: Hom W P (pairP W h k).
An exact proof term for the current goal is HE4a.
Apply and4I to the current goal.
We will prove Hom W P (pairP W h k).
An exact proof term for the current goal is Lhk.
We will prove comp W P X pi0P (pairP W h k) = h.
Use transitivity with and comp W (prod X Y) X (pi0 X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) (fac (prod X Y) Z pi0f pi1g W (pair X Y W h k))).
An exact proof term for the current goal is HC5 W P (prod X Y) X (pairP W h k) (canonmap (prod X Y) Z pi0f pi1g) (pi0 X Y) HW HE1 HP1 HX HE4a HE2 HP2.
rewrite the current goal using HE4b (from left to right).
We will prove comp W (prod X Y) X (pi0 X Y) (pair X Y W h k) = h.
An exact proof term for the current goal is HP4b.
We will prove comp W P Y pi1P (pairP W h k) = k.
Use transitivity with and comp W (prod X Y) Y (pi1 X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) (fac (prod X Y) Z pi0f pi1g W (pair X Y W h k))).
An exact proof term for the current goal is HC5 W P (prod X Y) Y (pairP W h k) (canonmap (prod X Y) Z pi0f pi1g) (pi1 X Y) HW HE1 HP1 HY HE4a HE2 HP3.
rewrite the current goal using HE4b (from left to right).
We will prove comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k) = k.
An exact proof term for the current goal is HP4c.
Let u be given.
Assume Hu: Hom W P u.
Assume Huh: comp W P X pi0P u = h.
Assume Huk: comp W P Y pi1P u = k.
We will prove u = pairP W h k.
We will prove u = fac (prod X Y) Z pi0f pi1g W (pair X Y W h k).
Apply HE4c u Hu to the current goal.
We will prove comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u = pair X Y W h k.
Apply HP4d (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u) to the current goal.
We will prove Hom W (prod X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u).
An exact proof term for the current goal is HC2 W P (prod X Y) u (canonmap (prod X Y) Z pi0f pi1g) HW HE1 HP1 Hu HE2.
We will prove comp W (prod X Y) X (pi0 X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u) = h.
rewrite the current goal using HC5 W P (prod X Y) X u (canonmap (prod X Y) Z pi0f pi1g) (pi0 X Y) HW HE1 HP1 HX Hu HE2 HP2 (from right to left).
We will prove comp W P X (comp P (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z pi0f pi1g)) u = h.
An exact proof term for the current goal is Huh.
We will prove comp W (prod X Y) Y (pi1 X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u) = k.
rewrite the current goal using HC5 W P (prod X Y) Y u (canonmap (prod X Y) Z pi0f pi1g) (pi1 X Y) HW HE1 HP1 HY Hu HE2 HP3 (from right to left).
We will prove comp W P Y (comp P (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z pi0f pi1g)) u = k.
An exact proof term for the current goal is Huk.
Theorem. (product_equalizer_pullback_constr_ex)
MetaCat Obj Hom id comp(∃quot : setsetsetsetset, ∃canonmap : setsetsetsetset, ∃fac : setsetsetsetsetsetset, equalizer_constr_p Obj Hom id comp quot canonmap fac)(∃prod : setsetset, ∃pi0 : setsetset, ∃pi1 : setsetset, ∃pair : setsetsetsetsetset, product_constr_p Obj Hom id comp prod pi0 pi1 pair)∃pb : setsetsetsetsetset, ∃pi0 : setsetsetsetsetset, ∃pi1 : setsetsetsetsetset, ∃pair : setsetsetsetsetsetsetsetset, pullback_constr_p Obj Hom id comp pb pi0 pi1 pair
Proof:
Assume HC HE HP.
Apply HE to the current goal.
Let quot be given.
Assume HE.
Apply HE to the current goal.
Let canonmap be given.
Assume HE.
Apply HE to the current goal.
Let fac be given.
Assume HE: equalizer_constr_p Obj Hom id comp quot canonmap fac.
Apply HP to the current goal.
Let prod be given.
Assume HP.
Apply HP to the current goal.
Let pi0 be given.
Assume HP.
Apply HP to the current goal.
Let pi1 be given.
Assume HP.
Apply HP to the current goal.
Let pair be given.
Assume HP: product_constr_p Obj Hom id comp prod pi0 pi1 pair.
We use (λX Y Z f g ⇒ quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) to witness the existential quantifier.
We use (λX Y Z f g ⇒ comp (quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)))) to witness the existential quantifier.
We use (λX Y Z f g ⇒ comp (quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)))) to witness the existential quantifier.
We use (λX Y Z f g W h k ⇒ fac (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)) W (pair X Y W h k)) to witness the existential quantifier.
An exact proof term for the current goal is product_equalizer_pullback_constr HC quot canonmap fac HE prod pi0 pi1 pair HP.
End of Section LimsCoLims2
Beginning of Section LimsCoLims3
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Theorem. (coproduct_coequalizer_pushout_constr_ex)
MetaCat Obj Hom id comp(∃quot : setsetsetsetset, ∃canonmap : setsetsetsetset, ∃fac : setsetsetsetsetsetset, coequalizer_constr_p Obj Hom id comp quot canonmap fac)(∃coprod : setsetset, ∃i0 : setsetset, ∃i1 : setsetset, ∃copair : setsetsetsetsetset, coproduct_constr_p Obj Hom id comp coprod i0 i1 copair)∃po : setsetsetsetsetset, ∃i0 : setsetsetsetsetset, ∃i1 : setsetsetsetsetset, ∃copair : setsetsetsetsetsetsetsetset, pushout_constr_p Obj Hom id comp po i0 i1 copair
Proof:
Assume HC HE HP.
We prove the intermediate claim LC: MetaCat Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f).
An exact proof term for the current goal is MetaCatOp Obj Hom id comp HC.
We will prove ∃pb : setsetsetsetsetset, ∃pi0 : setsetsetsetsetset, ∃pi1 : setsetsetsetsetset, ∃pair : setsetsetsetsetsetsetsetset, pullback_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) pb pi0 pi1 pair.
Apply product_equalizer_pullback_constr_ex Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) LC to the current goal.
Apply HE to the current goal.
Let quot be given.
Assume HE.
Apply HE to the current goal.
Let canonmap be given.
Assume HE.
Apply HE to the current goal.
Let fac be given.
Assume HE: coequalizer_constr_p Obj Hom id comp quot canonmap fac.
We use (λX Y : setquot Y X) to witness the existential quantifier.
We use (λX Y : setcanonmap Y X) to witness the existential quantifier.
We use (λX Y : setfac Y X) to witness the existential quantifier.
An exact proof term for the current goal is coequalizer_equalizer_constr_Op Obj Hom id comp quot canonmap fac HE.
An exact proof term for the current goal is HP.
End of Section LimsCoLims3
Definition. We define SetHom to be λX Y f ⇒ f YX of type setsetsetprop.
Theorem. (MetaCatSet_initial_gen)
∀Obj : setprop, Obj 0∃Y : set, ∃uniqa : setset, initial_p Obj SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) Y uniqa
Proof:
Let Obj be given.
Assume HO.
We use 0 to witness the existential quantifier.
We use (λX ⇒ (λx ∈ 00)) to witness the existential quantifier.
We will prove Obj 0∀X : set, Obj XSetHom 0 X (λx ∈ 00)∀h' : set, SetHom 0 X h'h' = (λx ∈ 00).
Apply andI to the current goal.
An exact proof term for the current goal is HO.
Let X be given.
Assume HX.
Apply andI to the current goal.
We will prove SetHom 0 X (λx ∈ 00).
We will prove (λx ∈ 00) ∏x ∈ 0, X.
Apply lam_Pi to the current goal.
Let x be given.
Assume Hx: x 0.
We will prove False.
An exact proof term for the current goal is EmptyE x Hx.
Let h be given.
Assume Hh: h ∏x ∈ 0, X.
We will prove h = (λx ∈ 00).
Use transitivity with and (λx ∈ 0h x).
Use symmetry.
An exact proof term for the current goal is Pi_eta 0 (λ_ ⇒ X) h Hh.
Apply lam_ext to the current goal.
Let x be given.
Assume Hx: x 0.
We will prove False.
An exact proof term for the current goal is EmptyE x Hx.
Theorem. (MetaCatSet_initial)
∃Y : set, ∃uniqa : setset, initial_p (λ_ ⇒ True) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) Y uniqa
Proof:
An exact proof term for the current goal is MetaCatSet_initial_gen (λ_ ⇒ True) TrueI.
Theorem. (MetaCatSet_terminal_gen)
∀Obj : setprop, Obj 1∃Y : set, ∃uniqa : setset, terminal_p Obj SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) Y uniqa
Proof:
Let Obj be given.
Assume HO.
We use 1 to witness the existential quantifier.
We use (λX ⇒ (λx ∈ X0)) to witness the existential quantifier.
We will prove Obj 1∀X : set, Obj XSetHom X 1 (λx ∈ X0)∀h' : set, SetHom X 1 h'h' = (λx ∈ X0).
Apply andI to the current goal.
An exact proof term for the current goal is HO.
Let X be given.
Assume HX.
Apply andI to the current goal.
We will prove SetHom X 1 (λx ∈ X0).
We will prove (λx ∈ X0) ∏x ∈ X, 1.
Apply lam_Pi to the current goal.
Let x be given.
Assume Hx: x X.
An exact proof term for the current goal is In_0_1.
Let h be given.
Assume Hh: h ∏x ∈ X, 1.
We will prove h = (λx ∈ X0).
Use transitivity with and (λx ∈ Xh x).
Use symmetry.
An exact proof term for the current goal is Pi_eta X (λ_ ⇒ 1) h Hh.
Apply lam_ext to the current goal.
Let x be given.
Assume Hx: x X.
We will prove h x = 0.
Apply SingE 0 (h x) to the current goal.
We will prove h x {0}.
rewrite the current goal using eq_1_Sing0 (from right to left).
We will prove h x 1.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ 1) h x Hh Hx.
Theorem. (MetaCatSet_terminal)
∃Y : set, ∃uniqa : setset, terminal_p (λ_ ⇒ True) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) Y uniqa
Proof:
An exact proof term for the current goal is MetaCatSet_terminal_gen (λ_ ⇒ True) TrueI.
Theorem. (MetaCatSet_coproduct_gen)
∀Obj : setprop, (∀X, Obj X∀Y, Obj YObj (setsum X Y))∃coprod : setsetset, ∃i0 i1 : setsetset, ∃copair : setsetsetsetsetset, coproduct_constr_p Obj SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) coprod i0 i1 copair
Proof:
Let Obj be given.
Assume HO: ∀X, Obj X∀Y, Obj YObj (setsum X Y).
We use setsum to witness the existential quantifier.
We use (λX Y ⇒ λx ∈ XInj0 x) to witness the existential quantifier.
We use (λX Y ⇒ λy ∈ YInj1 y) to witness the existential quantifier.
We use (λX Y W h k ⇒ (λz ∈ X + Ycombine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z)) to witness the existential quantifier.
Let X and Y be given.
Assume HX: Obj X.
Assume HY: Obj Y.
Set Z to be the term X + Y.
Set i0 to be the term (λx ∈ XInj0 x).
Set i1 to be the term (λy ∈ YInj1 y).
Set comb to be the term λW : setλh k : set(λz ∈ X + Ycombine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z).
We will prove Obj XObj YObj ZSetHom X Z i0SetHom Y Z i1∀W, Obj W∀h k : set, SetHom X W hSetHom Y W kSetHom Z W (comb W h k)(λx ∈ Xcomb W h k (i0 x)) = h(λy ∈ Ycomb W h k (i1 y)) = k∀hk : set, SetHom Z W hk(λx ∈ Xhk (i0 x)) = h(λy ∈ Yhk (i1 y)) = khk = comb W h k.
Apply and6I to the current goal.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is HO X HX Y HY.
We will prove SetHom X Z i0.
We will prove i0 ∏x ∈ X, Z.
Apply lam_Pi to the current goal.
Let x be given.
Assume Hx.
We will prove Inj0 x X + Y.
An exact proof term for the current goal is Inj0_setsum X Y x Hx.
We will prove SetHom Y Z i1.
We will prove i1 ∏y ∈ Y, Z.
Apply lam_Pi to the current goal.
Let y be given.
Assume Hy.
We will prove Inj1 y X + Y.
An exact proof term for the current goal is Inj1_setsum X Y y Hy.
Let W be given.
Assume HW: Obj W.
Let h and k be given.
Assume Hh: SetHom X W h.
Assume Hk: SetHom Y W k.
We will prove SetHom Z W (comb W h k)(λx ∈ Xcomb W h k (i0 x)) = h(λy ∈ Ycomb W h k (i1 y)) = k∀hk : set, SetHom Z W hk(λx ∈ Xhk (i0 x)) = h(λy ∈ Yhk (i1 y)) = khk = comb W h k.
Apply and4I to the current goal.
We will prove SetHom Z W (comb W h k).
We will prove (λz ∈ X + Ycombine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z) ∏z ∈ Z, W.
Apply lam_Pi to the current goal.
Let z be given.
Assume Hz: z X + Y.
We will prove (combine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z) W.
Apply setsum_Inj_inv X Y z Hz to the current goal.
Assume H1.
Apply H1 to the current goal.
Let x be given.
Assume H2.
Apply H2 to the current goal.
Assume Hx: x X.
Assume H2: z = Inj0 x.
rewrite the current goal using H2 (from left to right).
We will prove (combine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) (Inj0 x)) W.
rewrite the current goal using combine_funcs_eq1 X Y (λx ⇒ h x) (λy ⇒ k y) x (from left to right).
We will prove h x W.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ W) h x Hh Hx.
Assume H1.
Apply H1 to the current goal.
Let y be given.
Assume H2.
Apply H2 to the current goal.
Assume Hy: y Y.
Assume H2: z = Inj1 y.
rewrite the current goal using H2 (from left to right).
We will prove (combine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) (Inj1 y)) W.
rewrite the current goal using combine_funcs_eq2 X Y (λx ⇒ h x) (λy ⇒ k y) y (from left to right).
We will prove k y W.
An exact proof term for the current goal is ap_Pi Y (λ_ ⇒ W) k y Hk Hy.
We will prove (λx ∈ Xcomb W h k (i0 x)) = h.
Use transitivity with and (λx ∈ Xh x).
Apply lam_ext to the current goal.
Let x be given.
Assume Hx.
We will prove comb W h k (i0 x) = h x.
We will prove (λz ∈ X + Ycombine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z) ((λx ∈ XInj0 x) x) = h x.
rewrite the current goal using beta X Inj0 x Hx (from left to right).
We will prove (λz ∈ X + Ycombine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z) (Inj0 x) = h x.
rewrite the current goal using beta (X + Y) (λz ⇒ combine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z) (Inj0 x) (Inj0_setsum X Y x Hx) (from left to right).
Apply combine_funcs_eq1 to the current goal.
An exact proof term for the current goal is Pi_eta X (λ_ ⇒ W) h Hh.
We will prove (λy ∈ Ycomb W h k (i1 y)) = k.
Use transitivity with and (λy ∈ Yk y).
Apply lam_ext to the current goal.
Let y be given.
Assume Hy.
We will prove comb W h k (i1 y) = k y.
We will prove (λz ∈ X + Ycombine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z) ((λy ∈ YInj1 y) y) = k y.
rewrite the current goal using beta Y Inj1 y Hy (from left to right).
We will prove (λz ∈ X + Ycombine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z) (Inj1 y) = k y.
rewrite the current goal using beta (X + Y) (λz ⇒ combine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z) (Inj1 y) (Inj1_setsum X Y y Hy) (from left to right).
Apply combine_funcs_eq2 to the current goal.
An exact proof term for the current goal is Pi_eta Y (λ_ ⇒ W) k Hk.
Let hk be given.
Assume Hhk: SetHom Z W hk.
Assume Hhkh: (λx ∈ Xhk (i0 x)) = h.
Assume Hhkk: (λy ∈ Yhk (i1 y)) = k.
We will prove hk = comb W h k.
Use transitivity with and (λz ∈ Zhk z).
Use symmetry.
An exact proof term for the current goal is Pi_eta Z (λ_ ⇒ W) hk Hhk.
We will prove (λz ∈ Zhk z) = (λz ∈ X + Ycombine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z).
Apply lam_ext to the current goal.
Let z be given.
Assume Hz.
We will prove hk z = combine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) z.
Apply setsum_Inj_inv X Y z Hz to the current goal.
Assume H1.
Apply H1 to the current goal.
Let x be given.
Assume H2.
Apply H2 to the current goal.
Assume Hx: x X.
Assume H2: z = Inj0 x.
rewrite the current goal using H2 (from left to right).
We will prove hk (Inj0 x) = combine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) (Inj0 x).
rewrite the current goal using combine_funcs_eq1 (from left to right).
We will prove hk (Inj0 x) = h x.
rewrite the current goal using Hhkh (from right to left).
rewrite the current goal using beta X (λx ⇒ hk (i0 x)) x Hx (from left to right).
We will prove hk (Inj0 x) = hk (i0 x).
Use f_equal.
We will prove Inj0 x = (λx ∈ XInj0 x) x.
rewrite the current goal using beta X Inj0 x Hx (from left to right).
Use reflexivity.
Assume H1.
Apply H1 to the current goal.
Let y be given.
Assume H2.
Apply H2 to the current goal.
Assume Hy: y Y.
Assume H2: z = Inj1 y.
rewrite the current goal using H2 (from left to right).
We will prove hk (Inj1 y) = combine_funcs X Y (λx ⇒ h x) (λy ⇒ k y) (Inj1 y).
rewrite the current goal using combine_funcs_eq2 (from left to right).
We will prove hk (Inj1 y) = k y.
rewrite the current goal using Hhkk (from right to left).
rewrite the current goal using beta Y (λy ⇒ hk (i1 y)) y Hy (from left to right).
We will prove hk (Inj1 y) = hk (i1 y).
Use f_equal.
We will prove Inj1 y = (λy ∈ YInj1 y) y.
rewrite the current goal using beta Y Inj1 y Hy (from left to right).
Use reflexivity.
Theorem. (MetaCatSet_coproduct)
∃coprod : setsetset, ∃i0 i1 : setsetset, ∃copair : setsetsetsetsetset, coproduct_constr_p (λ_ ⇒ True) SetHom (λX ⇒ λx ∈ Xx) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) coprod i0 i1 copair
Proof:
We prove the intermediate claim L1: ∀X, True∀Y, TrueTrue.
An exact proof term for the current goal is (λ_ _ _ _ ⇒ TrueI).
An exact proof term for the current goal is MetaCatSet_coproduct_gen (λ_ ⇒ True) L1.
Theorem. (MetaCatSet_product_gen)
∀Obj : setprop, (∀X, Obj X∀Y, Obj YObj (setprod X Y))∃prod : setsetset, ∃pi0 pi1 : setsetset, ∃pair : setsetsetsetsetset, product_constr_p Obj SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) prod pi0 pi1 pair
Proof:
Let Obj be given.
Assume HO: ∀X, Obj X∀Y, Obj YObj (XY).
We use setprod to witness the existential quantifier.
We use (λX Y ⇒ (λz ∈ XYz 0)) to witness the existential quantifier.
We use (λX Y ⇒ (λz ∈ XYz 1)) to witness the existential quantifier.
We use (λX Y W h k ⇒ (λw ∈ W(h w,k w))) to witness the existential quantifier.
Let X and Y be given.
Assume HX: Obj X.
Assume HY: Obj Y.
Set Z to be the term XY.
Set pi0 to be the term (λz ∈ Zz 0).
Set pi1 to be the term (λz ∈ Zz 1).
Set pair to be the term λW : setλh k : set(λw ∈ W(h w,k w)).
We will prove product_p Obj SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) X Y Z pi0 pi1 pair.
We will prove Obj XObj YObj ZSetHom Z X pi0SetHom Z Y pi1∀W, Obj W∀h k : set, SetHom W X hSetHom W Y kSetHom W Z (pair W h k)(λw ∈ Wpi0 (pair W h k w)) = h(λw ∈ Wpi1 (pair W h k w)) = k∀u : set, SetHom W Z u(λw ∈ Wpi0 (u w)) = h(λw ∈ Wpi1 (u w)) = ku = pair W h k.
Apply and6I to the current goal.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is HO X HX Y HY.
We will prove SetHom Z X pi0.
We will prove pi0 ∏z ∈ Z, X.
Apply lam_Pi to the current goal.
An exact proof term for the current goal is ap0_Sigma X (λ_ ⇒ Y).
We will prove SetHom Z Y pi1.
We will prove pi1 ∏z ∈ Z, Y.
Apply lam_Pi to the current goal.
An exact proof term for the current goal is ap1_Sigma X (λ_ ⇒ Y).
Let W be given.
Assume HW: Obj W.
Let h and k be given.
Assume Hh: SetHom W X h.
Assume Hk: SetHom W Y k.
We prove the intermediate claim L1: ∀wW, (h w,k w) Z.
Let w be given.
Assume Hw: w W.
We will prove (h w,k w) XY.
Apply tuple_2_setprod to the current goal.
An exact proof term for the current goal is ap_Pi W (λ_ ⇒ X) h w Hh Hw.
An exact proof term for the current goal is ap_Pi W (λ_ ⇒ Y) k w Hk Hw.
We prove the intermediate claim L2: (λw ∈ W(h w,k w)) ∏w ∈ W, Z.
We will prove (λw ∈ W(h w,k w)) ∏w ∈ W, Z.
Apply lam_Pi to the current goal.
An exact proof term for the current goal is L1.
We will prove SetHom W Z (pair W h k)(λw ∈ Wpi0 (pair W h k w)) = h(λw ∈ Wpi1 (pair W h k w)) = k∀u : set, SetHom W Z u(λw ∈ Wpi0 (u w)) = h(λw ∈ Wpi1 (u w)) = ku = pair W h k.
Apply and4I to the current goal.
We will prove SetHom W Z (pair W h k).
An exact proof term for the current goal is L2.
We will prove (λw ∈ Wpi0 (pair W h k w)) = h.
Use transitivity with and (λw ∈ Wh w).
Apply lam_ext to the current goal.
Let w be given.
Assume Hw.
We will prove pi0 ((λw ∈ W(h w,k w)) w) = h w.
rewrite the current goal using beta W (λw ⇒ (h w,k w)) w Hw (from left to right).
We will prove (λz ∈ Zz 0) (h w,k w) = h w.
rewrite the current goal using beta Z (λz ⇒ z 0) (h w,k w) (L1 w Hw) (from left to right).
We will prove (h w,k w) 0 = h w.
Apply tuple_2_0_eq to the current goal.
We will prove (λw ∈ Wh w) = h.
An exact proof term for the current goal is Pi_eta W (λ_ ⇒ X) h Hh.
We will prove (λw ∈ Wpi1 (pair W h k w)) = k.
Use transitivity with and (λw ∈ Wk w).
Apply lam_ext to the current goal.
Let w be given.
Assume Hw.
We will prove pi1 ((λw ∈ W(h w,k w)) w) = k w.
rewrite the current goal using beta W (λw ⇒ (h w,k w)) w Hw (from left to right).
We will prove (λz ∈ Zz 1) (h w,k w) = k w.
rewrite the current goal using beta Z (λz ⇒ z 1) (h w,k w) (L1 w Hw) (from left to right).
We will prove (h w,k w) 1 = k w.
Apply tuple_2_1_eq to the current goal.
We will prove (λw ∈ Wk w) = k.
An exact proof term for the current goal is Pi_eta W (λ_ ⇒ Y) k Hk.
Let u be given.
Assume Hu: SetHom W Z u.
Assume Huh: (λw ∈ Wpi0 (u w)) = h.
Assume Huk: (λw ∈ Wpi1 (u w)) = k.
We will prove u = pair W h k.
Use transitivity with and (λw ∈ Wu w).
Use symmetry.
An exact proof term for the current goal is Pi_eta W (λ_ ⇒ Z) u Hu.
We will prove (λw ∈ Wu w) = (λw ∈ W(h w,k w)).
Apply lam_ext to the current goal.
Let w be given.
Assume Hw.
We will prove u w = (h w,k w).
We prove the intermediate claim L3: u w Z.
An exact proof term for the current goal is ap_Pi W (λ_ ⇒ Z) u w Hu Hw.
rewrite the current goal using tuple_Sigma_eta X (λ_ ⇒ Y) (u w) L3 (from right to left).
We will prove (u w 0,u w 1) = (h w,k w).
We prove the intermediate claim L4: u w 0 = h w.
rewrite the current goal using Huh (from right to left).
We will prove u w 0 = (λw ∈ Wpi0 (u w)) w.
Use transitivity with and pi0 (u w).
We will prove u w 0 = (λz ∈ Zz 0) (u w).
Use symmetry.
An exact proof term for the current goal is beta Z (λz ⇒ z 0) (u w) L3.
Use symmetry.
An exact proof term for the current goal is beta W (λw ⇒ pi0 (u w)) w Hw.
We prove the intermediate claim L5: u w 1 = k w.
rewrite the current goal using Huk (from right to left).
We will prove u w 1 = (λw ∈ Wpi1 (u w)) w.
Use transitivity with and pi1 (u w).
We will prove u w 1 = (λz ∈ Zz 1) (u w).
Use symmetry.
An exact proof term for the current goal is beta Z (λz ⇒ z 1) (u w) L3.
Use symmetry.
An exact proof term for the current goal is beta W (λw ⇒ pi1 (u w)) w Hw.
rewrite the current goal using L4 (from left to right).
rewrite the current goal using L5 (from left to right).
Use reflexivity.
Theorem. (MetaCatSet_product)
∃prod : setsetset, ∃pi0 pi1 : setsetset, ∃pair : setsetsetsetsetset, product_constr_p (λ_ ⇒ True) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) prod pi0 pi1 pair
Proof:
We prove the intermediate claim L1: ∀X, True∀Y, TrueTrue.
An exact proof term for the current goal is (λ_ _ _ _ ⇒ TrueI).
An exact proof term for the current goal is MetaCatSet_product_gen (λ_ ⇒ True) L1.
Theorem. (UnivOf_Subq_closed)
∀N, ∀XUnivOf N, ∀QX, Q UnivOf N
Proof:
Let N and X be given.
Assume HX: X UnivOf N.
Let Q be given.
Assume HQ: Q X.
We prove the intermediate claim LZ: ZF_closed (UnivOf N).
An exact proof term for the current goal is UnivOf_ZF_closed N.
We prove the intermediate claim LQ: Q 𝒫 X.
An exact proof term for the current goal is PowerI X Q HQ.
An exact proof term for the current goal is UnivOf_TransSet N (𝒫 X) (ZF_Power_closed (UnivOf N) LZ X HX) Q LQ.
Definition. We define famunion_closed to be λU : set∀XU, ∀F : setset, (∀xX, F x U)famunion X F U of type setprop.
Theorem. (Union_Repl_famunion_closed)
∀U : set, Union_closed URepl_closed Ufamunion_closed U
Proof:
Let U be given.
Assume HU: Union_closed U.
Assume HR: Repl_closed U.
Let X be given.
Assume HX: X U.
Let F be given.
Assume HF: ∀xX, F x U.
We will prove famunion X F U.
We will prove {F x|x ∈ X} U.
Apply HU to the current goal.
We will prove {F x|x ∈ X} U.
An exact proof term for the current goal is HR X HX F HF.
Theorem. (ZF_closed_0)
∀U X, TransSet UZF_closed UX U0 U
Proof:
Let U and X be given.
Assume H1 H2 H3.
Apply ZF_closed_E U H2 to the current goal.
Assume HU HP HR.
We prove the intermediate claim L1: 𝒫 X U.
Apply HP to the current goal.
An exact proof term for the current goal is H3.
Apply H1 (𝒫 X) L1 0 to the current goal.
We will prove 0 𝒫 X.
Apply Empty_In_Power to the current goal.
Theorem. (ZF_Inj1_closed)
∀U, TransSet UZF_closed U∀XU, Inj1 X U
Proof:
Let U be given.
Assume HUT: TransSet U.
Assume HU: ZF_closed U.
Apply In_ind to the current goal.
Let X be given.
Assume IH: ∀xX, x UInj1 x U.
Assume HX: X U.
rewrite the current goal using Inj1_eq (from left to right).
We will prove ({Empty}{Inj1 x|x ∈ X}) U.
Apply ZF_binunion_closed U HU to the current goal.
Apply ZF_Sing_closed U HU to the current goal.
Apply HUT (𝒫 X) (ZF_Power_closed U HU X HX) Empty (Empty_In_Power X) to the current goal.
Apply ZF_Repl_closed U HU X HX to the current goal.
Let x be given.
Assume Hx: x X.
Apply IH x Hx to the current goal.
We will prove x U.
An exact proof term for the current goal is HUT X HX x Hx.
Theorem. (ZF_Inj0_closed)
∀U, TransSet UZF_closed U∀XU, Inj0 X U
Proof:
Let U be given.
Assume HUT: TransSet U.
Assume HU: ZF_closed U.
Let X be given.
Assume HX: X U.
We will prove {Inj1 x|x ∈ X} U.
Apply ZF_Repl_closed U HU X HX to the current goal.
Let x be given.
Assume Hx: x X.
Apply ZF_Inj1_closed U HUT HU x to the current goal.
We will prove x U.
An exact proof term for the current goal is HUT X HX x Hx.
Theorem. (ZF_setsum_closed)
∀U, TransSet UZF_closed U∀X YU, (X + Y) U
Proof:
Let U be given.
Assume HUT: TransSet U.
Assume HU: ZF_closed U.
Let X be given.
Assume HX: X U.
Let Y be given.
Assume HY: Y U.
We will prove ({Inj0 x|x ∈ X}{Inj1 y|y ∈ Y}) U.
Apply ZF_binunion_closed U HU to the current goal.
We will prove {Inj0 x|x ∈ X} U.
Apply ZF_Repl_closed U HU X HX Inj0 to the current goal.
Let x be given.
Assume Hx: x X.
We will prove Inj0 x U.
Apply ZF_Inj0_closed U HUT HU x to the current goal.
We will prove x U.
An exact proof term for the current goal is HUT X HX x Hx.
Apply ZF_Repl_closed U HU Y HY Inj1 to the current goal.
Let y be given.
Assume Hy: y Y.
We will prove Inj1 y U.
Apply ZF_Inj1_closed U HUT HU y to the current goal.
We will prove y U.
An exact proof term for the current goal is HUT Y HY y Hy.
Theorem. (ZF_Sigma_closed)
∀U, TransSet UZF_closed U∀XU, ∀Y : setset, (∀xX, Y x U)(∑x ∈ X, Y x) U
Proof:
Let U be given.
Assume HUT: TransSet U.
Assume HU: ZF_closed U.
Apply ZF_closed_E U HU to the current goal.
Assume HUU HUP HUR.
Let X be given.
Assume HX: X U.
Let Y be given.
Assume HY: ∀xX, Y x U.
We will prove (x ∈ X{setsum x y|y ∈ Y x}) U.
We prove the intermediate claim L1: famunion_closed U.
Apply Union_Repl_famunion_closed to the current goal.
An exact proof term for the current goal is HUU.
An exact proof term for the current goal is HUR.
Apply L1 X HX (λx ⇒ {setsum x y|y ∈ Y x}) to the current goal.
Let x be given.
Assume Hx: x X.
We will prove {setsum x y|y ∈ Y x} U.
Apply HUR (Y x) (HY x Hx) (λy ⇒ setsum x y) to the current goal.
Let y be given.
Assume Hy: y Y x.
We will prove setsum x y U.
Apply ZF_setsum_closed U HUT HU to the current goal.
We will prove x U.
An exact proof term for the current goal is HUT X HX x Hx.
We will prove y U.
An exact proof term for the current goal is HUT (Y x) (HY x Hx) y Hy.
Theorem. (ZF_setprod_closed)
∀U, TransSet UZF_closed U∀X YU, (XY) U
Proof:
Let U be given.
Assume HUT HU.
Let X be given.
Assume HX.
Let Y be given.
Assume HY.
An exact proof term for the current goal is ZF_Sigma_closed U HUT HU X HX (λ_ ⇒ Y) (λ_ _ ⇒ HY).
Theorem. (ZF_Pi_closed)
∀U, TransSet UZF_closed U∀XU, ∀Y : setset, (∀xX, Y x U)(∏x ∈ X, Y x) U
Proof:
Let U be given.
Assume HUT: TransSet U.
Assume HU: ZF_closed U.
Apply ZF_closed_E U HU to the current goal.
Assume HUU HUP HUR.
Let X be given.
Assume HX: X U.
Let Y be given.
Assume HY: ∀xX, Y x U.
We will prove (∏x ∈ X, Y x) U.
We prove the intermediate claim L1: (∏x ∈ X, Y x) 𝒫 (𝒫 (∑x ∈ X, (Y x))).
An exact proof term for the current goal is Sep_In_Power (𝒫 (∑x ∈ X, (Y x))) (λf ⇒ ∀xX, f x Y x).
We prove the intermediate claim L2: (𝒫 (𝒫 (∑x ∈ X, (Y x)))) U.
Apply HUP to the current goal.
Apply HUP to the current goal.
Apply ZF_Sigma_closed U HUT HU X HX (λx ⇒ (Y x)) to the current goal.
Let x be given.
Assume Hx: x X.
We will prove (Y x) U.
Apply HUU to the current goal.
An exact proof term for the current goal is HY x Hx.
An exact proof term for the current goal is HUT (𝒫 (𝒫 (∑x ∈ X, (Y x)))) L2 (∏x ∈ X, Y x) L1.
Theorem. (ZF_setexp_closed)
∀U, TransSet UZF_closed U∀X YU, (YX) U
Proof:
Let U be given.
Assume HUT HU.
Let X be given.
Assume HX.
Let Y be given.
Assume HY.
An exact proof term for the current goal is ZF_Pi_closed U HUT HU X HX (λ_ ⇒ Y) (λx Hx ⇒ HY).
Theorem. (MetaCatHFSet_initial)
∃Y : set, ∃uniqa : setset, initial_p (λX ⇒ X UnivOf Empty) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) Y uniqa
Proof:
An exact proof term for the current goal is MetaCatSet_initial_gen (λX ⇒ X UnivOf Empty) (UnivOf_In Empty).
Theorem. (MetaCatSmallSet_initial)
∃Y : set, ∃uniqa : setset, initial_p (λX ⇒ X UnivOf (UnivOf Empty)) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) Y uniqa
Proof:
We prove the intermediate claim L1: 0 UnivOf (UnivOf Empty).
An exact proof term for the current goal is ZF_closed_0 (UnivOf (UnivOf Empty)) (UnivOf Empty) (UnivOf_TransSet (UnivOf Empty)) (UnivOf_ZF_closed (UnivOf Empty)) (UnivOf_In (UnivOf Empty)).
An exact proof term for the current goal is MetaCatSet_initial_gen (λX ⇒ X UnivOf (UnivOf Empty)) L1.
Theorem. (MetaCatHFSet_terminal)
∃Y : set, ∃uniqa : setset, terminal_p (λX ⇒ X UnivOf Empty) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) Y uniqa
Proof:
We prove the intermediate claim L1: 1 UnivOf Empty.
Apply ZF_ordsucc_closed to the current goal.
An exact proof term for the current goal is UnivOf_ZF_closed Empty.
An exact proof term for the current goal is ZF_closed_0 (UnivOf Empty) Empty (UnivOf_TransSet Empty) (UnivOf_ZF_closed Empty) (UnivOf_In Empty).
An exact proof term for the current goal is MetaCatSet_terminal_gen (λX ⇒ X UnivOf Empty) L1.
Theorem. (MetaCatSmallSet_terminal)
∃Y : set, ∃uniqa : setset, terminal_p (λX ⇒ X UnivOf (UnivOf Empty)) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) Y uniqa
Proof:
We prove the intermediate claim L1: 1 UnivOf (UnivOf Empty).
Apply ZF_ordsucc_closed to the current goal.
An exact proof term for the current goal is UnivOf_ZF_closed (UnivOf Empty).
An exact proof term for the current goal is ZF_closed_0 (UnivOf (UnivOf Empty)) (UnivOf Empty) (UnivOf_TransSet (UnivOf Empty)) (UnivOf_ZF_closed (UnivOf Empty)) (UnivOf_In (UnivOf Empty)).
An exact proof term for the current goal is MetaCatSet_terminal_gen (λX ⇒ X UnivOf (UnivOf Empty)) L1.
Theorem. (MetaCatHFSet_coproduct)
∃coprod : setsetset, ∃i0 i1 : setsetset, ∃copair : setsetsetsetsetset, coproduct_constr_p (λX ⇒ X UnivOf Empty) SetHom (λX ⇒ λx ∈ Xx) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) coprod i0 i1 copair
Proof:
We prove the intermediate claim L1: ∀X YUnivOf Empty, X + Y UnivOf Empty.
An exact proof term for the current goal is ZF_setsum_closed (UnivOf Empty) (UnivOf_TransSet Empty) (UnivOf_ZF_closed Empty).
An exact proof term for the current goal is MetaCatSet_coproduct_gen (λX ⇒ X UnivOf Empty) L1.
Theorem. (MetaCatSmallSet_coproduct)
∃coprod : setsetset, ∃i0 i1 : setsetset, ∃copair : setsetsetsetsetset, coproduct_constr_p (λX ⇒ X UnivOf (UnivOf Empty)) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) coprod i0 i1 copair
Proof:
We prove the intermediate claim L1: ∀X YUnivOf (UnivOf Empty), X + Y UnivOf (UnivOf Empty).
An exact proof term for the current goal is ZF_setsum_closed (UnivOf (UnivOf Empty)) (UnivOf_TransSet (UnivOf Empty)) (UnivOf_ZF_closed (UnivOf Empty)).
An exact proof term for the current goal is MetaCatSet_coproduct_gen (λX ⇒ X UnivOf (UnivOf Empty)) L1.
Theorem. (MetaCatHFSet_product)
∃prod : setsetset, ∃pi0 pi1 : setsetset, ∃pair : setsetsetsetsetset, product_constr_p (λX ⇒ X UnivOf Empty) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) prod pi0 pi1 pair
Proof:
We prove the intermediate claim L1: ∀X YUnivOf Empty, XY UnivOf Empty.
An exact proof term for the current goal is ZF_setprod_closed (UnivOf Empty) (UnivOf_TransSet Empty) (UnivOf_ZF_closed Empty).
An exact proof term for the current goal is MetaCatSet_product_gen (λX ⇒ X UnivOf Empty) L1.
Theorem. (MetaCatSmallSet_product)
∃prod : setsetset, ∃pi0 pi1 : setsetset, ∃pair : setsetsetsetsetset, product_constr_p (λX ⇒ X UnivOf (UnivOf Empty)) SetHom (λX ⇒ (λx ∈ Xx)) (λX Y Z f g ⇒ (λx ∈ Xf (g x))) prod pi0 pi1 pair
Proof:
We prove the intermediate claim L1: ∀X YUnivOf (UnivOf Empty), XY UnivOf (UnivOf Empty).
An exact proof term for the current goal is ZF_setprod_closed (UnivOf (UnivOf Empty)) (UnivOf_TransSet (UnivOf Empty)) (UnivOf_ZF_closed (UnivOf Empty)).
An exact proof term for the current goal is MetaCatSet_product_gen (λX ⇒ X UnivOf (UnivOf Empty)) L1.
Beginning of Section MetaFunctor
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Variable Obj' : setprop
Variable Hom' : setsetsetprop
Variable id' : setset
Variable comp' : setsetsetsetsetset
Variable F0 : setset
Variable F1 : setsetsetset
Definition. We define MetaFunctor to be (∀X, Obj XObj' (F0 X))(∀X Y f, Obj XObj YHom X Y fHom' (F0 X) (F0 Y) (F1 X Y f))(∀X, Obj XF1 X X (id X) = id' (F0 X))(∀X Y Z f g, Obj XObj YObj ZHom X Y fHom Y Z gF1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)) of type prop.
Theorem. (MetaFunctorI)
(∀X, Obj XObj' (F0 X))(∀X Y f, Obj XObj YHom X Y fHom' (F0 X) (F0 Y) (F1 X Y f))(∀X, Obj XF1 X X (id X) = id' (F0 X))(∀X Y Z f g, Obj XObj YObj ZHom X Y fHom Y Z gF1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f))MetaFunctor
Proof:
An exact proof term for the current goal is and4I (∀X, Obj XObj' (F0 X)) (∀X Y f, Obj XObj YHom X Y fHom' (F0 X) (F0 Y) (F1 X Y f)) (∀X, Obj XF1 X X (id X) = id' (F0 X)) (∀X Y Z f g, Obj XObj YObj ZHom X Y fHom Y Z gF1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)).
Theorem. (MetaFunctorE)
MetaFunctor∀p : prop, ((∀X, Obj XObj' (F0 X))(∀X Y f, Obj XObj YHom X Y fHom' (F0 X) (F0 Y) (F1 X Y f))(∀X, Obj XF1 X X (id X) = id' (F0 X))(∀X Y Z f g, Obj XObj YObj ZHom X Y fHom Y Z gF1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f))p)p
Proof:
An exact proof term for the current goal is and4E (∀X, Obj XObj' (F0 X)) (∀X Y f, Obj XObj YHom X Y fHom' (F0 X) (F0 Y) (F1 X Y f)) (∀X, Obj XF1 X X (id X) = id' (F0 X)) (∀X Y Z f g, Obj XObj YObj ZHom X Y fHom Y Z gF1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)).
Definition. We define MetaFunctor_strict to be MetaCat Obj Hom id compMetaCat Obj' Hom' id' comp'MetaFunctor of type prop.
Theorem. (MetaFunctor_strict_I)
MetaCat Obj Hom id compMetaCat Obj' Hom' id' comp'MetaFunctorMetaFunctor_strict
Proof:
An exact proof term for the current goal is and3I (MetaCat Obj Hom id comp) (MetaCat Obj' Hom' id' comp') MetaFunctor.
Theorem. (MetaFunctor_strict_E)
MetaFunctor_strict∀p : prop, (MetaCat Obj Hom id compMetaCat Obj' Hom' id' comp'MetaFunctorp)p
Proof:
An exact proof term for the current goal is and3E (MetaCat Obj Hom id comp) (MetaCat Obj' Hom' id' comp') MetaFunctor.
End of Section MetaFunctor
Beginning of Section IdFunctor
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Theorem. (MetaCat_IdFunctor)
MetaFunctor Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f)
Proof:
Apply MetaFunctorI to the current goal.
Let X be given.
Assume HX.
An exact proof term for the current goal is HX.
Let X, Y and f be given.
Assume HX HY Hf.
An exact proof term for the current goal is Hf.
Let X be given.
Assume HX.
Use reflexivity.
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
Use reflexivity.
Theorem. (MetaCat_IdFunctor_strict)
MetaCat Obj Hom id compMetaFunctor_strict Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f)
Proof:
Assume HC.
Apply MetaFunctor_strict_I to the current goal.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is MetaCat_IdFunctor.
End of Section IdFunctor
Beginning of Section CompFunctors
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Variable Obj' : setprop
Variable Hom' : setsetsetprop
Variable id' : setset
Variable comp' : setsetsetsetsetset
Variable Obj'' : setprop
Variable Hom'' : setsetsetprop
Variable id'' : setset
Variable comp'' : setsetsetsetsetset
Variable F0 : setset
Variable F1 : setsetsetset
Variable G0 : setset
Variable G1 : setsetsetset
Theorem. (MetaCat_CompFunctors)
MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1MetaFunctor Obj Hom id comp Obj'' Hom'' id'' comp'' (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f))
Proof:
Assume HF HG.
Apply MetaFunctorE Obj Hom id comp Obj' Hom' id' comp' F0 F1 HF to the current goal.
Assume HF1 HF2 HF3 HF4.
Apply MetaFunctorE Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1 HG to the current goal.
Assume HG1 HG2 HG3 HG4.
Apply MetaFunctorI to the current goal.
Let X be given.
Assume HX.
We will prove Obj'' (G0 (F0 X)).
Apply HG1 to the current goal.
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
Let X, Y and f be given.
Assume HX HY Hf.
We will prove Hom'' (G0 (F0 X)) (G0 (F0 Y)) (G1 (F0 X) (F0 Y) (F1 X Y f)).
Apply HG2 to the current goal.
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
Apply HF1 to the current goal.
An exact proof term for the current goal is HY.
Apply HF2 to the current goal.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is Hf.
Let X be given.
Assume HX.
We will prove G1 (F0 X) (F0 X) (F1 X X (id X)) = id'' (G0 (F0 X)).
Use transitivity with and G1 (F0 X) (F0 X) (id' (F0 X)).
Use f_equal.
An exact proof term for the current goal is HF3 X HX.
An exact proof term for the current goal is HG3 (F0 X) (HF1 X HX).
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
We will prove G1 (F0 X) (F0 Z) (F1 X Z (comp X Y Z g f)) = comp'' (G0 (F0 X)) (G0 (F0 Y)) (G0 (F0 Z)) (G1 (F0 Y) (F0 Z) (F1 Y Z g)) (G1 (F0 X) (F0 Y) (F1 X Y f)).
Use transitivity with and G1 (F0 X) (F0 Z) (comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)).
Use f_equal.
An exact proof term for the current goal is HF4 X Y Z f g HX HY HZ Hf Hg.
Apply HG4 (F0 X) (F0 Y) (F0 Z) (F1 X Y f) (F1 Y Z g) (HF1 X HX) (HF1 Y HY) (HF1 Z HZ) to the current goal.
An exact proof term for the current goal is HF2 X Y f HX HY Hf.
An exact proof term for the current goal is HF2 Y Z g HY HZ Hg.
Theorem. (MetaCat_CompFunctors_strict)
MetaFunctor_strict Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor_strict Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1MetaFunctor_strict Obj Hom id comp Obj'' Hom'' id'' comp'' (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f))
Proof:
Assume HF HG.
Apply MetaFunctor_strict_E Obj Hom id comp Obj' Hom' id' comp' F0 F1 HF to the current goal.
Assume HC _ HF.
Apply MetaFunctor_strict_E Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1 HG to the current goal.
Assume _ HC'' HG.
Apply MetaFunctor_strict_I to the current goal.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HC''.
Apply MetaCat_CompFunctors to the current goal.
An exact proof term for the current goal is HF.
An exact proof term for the current goal is HG.
End of Section CompFunctors
Beginning of Section MetaNatTrans
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Variable Obj' : setprop
Variable Hom' : setsetsetprop
Variable id' : setset
Variable comp' : setsetsetsetsetset
Variable F0 : setset
Variable F1 : setsetsetset
Variable G0 : setset
Variable G1 : setsetsetset
Variable eta : setset
Definition. We define MetaNatTrans to be (∀X, Obj XHom' (F0 X) (G0 X) (eta X))(∀X Y f, Obj XObj YHom X Y fcomp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X) = comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f)) of type prop.
Theorem. (MetaNatTransI)
(∀X, Obj XHom' (F0 X) (G0 X) (eta X))(∀X Y f, Obj XObj YHom X Y fcomp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X) = comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f))MetaNatTrans
Proof:
An exact proof term for the current goal is andI (∀X, Obj XHom' (F0 X) (G0 X) (eta X)) (∀X Y f, Obj XObj YHom X Y fcomp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X) = comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f)).
Theorem. (MetaNatTransE)
MetaNatTrans∀p : prop, ((∀X, Obj XHom' (F0 X) (G0 X) (eta X))(∀X Y f, Obj XObj YHom X Y fcomp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X) = comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f))p)p
Proof:
Assume H.
An exact proof term for the current goal is H.
Definition. We define MetaNatTrans_strict to be MetaCat Obj Hom id compMetaCat Obj' Hom' id' comp'MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj Hom id comp Obj' Hom' id' comp' G0 G1MetaNatTrans of type prop.
Theorem. (MetaNatTrans_strict_I)
MetaCat Obj Hom id compMetaCat Obj' Hom' id' comp'MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj Hom id comp Obj' Hom' id' comp' G0 G1MetaNatTransMetaNatTrans_strict
Proof:
An exact proof term for the current goal is and5I (MetaCat Obj Hom id comp) (MetaCat Obj' Hom' id' comp') (MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1) (MetaFunctor Obj Hom id comp Obj' Hom' id' comp' G0 G1) MetaNatTrans.
Theorem. (MetaNatTrans_strict_E)
MetaNatTrans_strict∀p : prop, (MetaCat Obj Hom id compMetaCat Obj' Hom' id' comp'MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj Hom id comp Obj' Hom' id' comp' G0 G1MetaNatTransp)p
Proof:
Assume H.
An exact proof term for the current goal is and5E (MetaCat Obj Hom id comp) (MetaCat Obj' Hom' id' comp') (MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1) (MetaFunctor Obj Hom id comp Obj' Hom' id' comp' G0 G1) MetaNatTrans H.
End of Section MetaNatTrans
Beginning of Section CompFunctorNatTrans
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Variable Obj' : setprop
Variable Hom' : setsetsetprop
Variable id' : setset
Variable comp' : setsetsetsetsetset
Variable Obj'' : setprop
Variable Hom'' : setsetsetprop
Variable id'' : setset
Variable comp'' : setsetsetsetsetset
Variable F0 : setset
Variable F1 : setsetsetset
Variable G0 : setset
Variable G1 : setsetsetset
Variable H0 : setset
Variable H1 : setsetsetset
Variable eta : setset
Theorem. (MetaCat_CompFunctorNatTrans)
MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj Hom id comp Obj' Hom' id' comp' G0 G1MetaNatTrans Obj Hom id comp Obj' Hom' id' comp' F0 F1 G0 G1 etaMetaFunctor Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' H0 H1MetaNatTrans Obj Hom id comp Obj'' Hom'' id'' comp'' (λX ⇒ H0 (F0 X)) (λX Y f ⇒ H1 (F0 X) (F0 Y) (F1 X Y f)) (λX ⇒ H0 (G0 X)) (λX Y f ⇒ H1 (G0 X) (G0 Y) (G1 X Y f)) (λX ⇒ H1 (F0 X) (G0 X) (eta X))
Proof:
Assume HF HG Heta HH.
Apply MetaFunctorE Obj Hom id comp Obj' Hom' id' comp' F0 F1 HF to the current goal.
Assume HF1 HF2 HF3 HF4.
Apply MetaFunctorE Obj Hom id comp Obj' Hom' id' comp' G0 G1 HG to the current goal.
Assume HG1 HG2 HG3 HG4.
Apply MetaNatTransE Obj Hom id comp Obj' Hom' id' comp' F0 F1 G0 G1 eta Heta to the current goal.
Assume Heta1 Heta2.
Apply MetaFunctorE Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' H0 H1 HH to the current goal.
Assume HH1 HH2 HH3 HH4.
Apply MetaNatTransI to the current goal.
Let X be given.
Assume HX.
We will prove Hom'' (H0 (F0 X)) (H0 (G0 X)) (H1 (F0 X) (G0 X) (eta X)).
Apply HH2 to the current goal.
We will prove Obj' (F0 X).
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
We will prove Obj' (G0 X).
Apply HG1 to the current goal.
An exact proof term for the current goal is HX.
We will prove Hom' (F0 X) (G0 X) (eta X).
Apply Heta1 to the current goal.
An exact proof term for the current goal is HX.
Let X, Y and f be given.
Assume HX HY Hf.
We will prove comp'' (H0 (F0 X)) (H0 (G0 X)) (H0 (G0 Y)) (H1 (G0 X) (G0 Y) (G1 X Y f)) (H1 (F0 X) (G0 X) (eta X)) = comp'' (H0 (F0 X)) (H0 (F0 Y)) (H0 (G0 Y)) (H1 (F0 Y) (G0 Y) (eta Y)) (H1 (F0 X) (F0 Y) (F1 X Y f)).
Use transitivity with H1 (F0 X) (G0 Y) (comp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X)), and H1 (F0 X) (G0 Y) (comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f)).
Use symmetry.
Apply HH4 to the current goal.
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
Apply HG1 to the current goal.
An exact proof term for the current goal is HX.
Apply HG1 to the current goal.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is Heta1 X HX.
An exact proof term for the current goal is HG2 X Y f HX HY Hf.
Use f_equal.
An exact proof term for the current goal is Heta2 X Y f HX HY Hf.
Apply HH4 to the current goal.
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
Apply HF1 to the current goal.
An exact proof term for the current goal is HY.
Apply HG1 to the current goal.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is HF2 X Y f HX HY Hf.
An exact proof term for the current goal is Heta1 Y HY.
End of Section CompFunctorNatTrans
Beginning of Section CompNatTransFunctor
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Variable Obj' : setprop
Variable Hom' : setsetsetprop
Variable id' : setset
Variable comp' : setsetsetsetsetset
Variable Obj'' : setprop
Variable Hom'' : setsetsetprop
Variable id'' : setset
Variable comp'' : setsetsetsetsetset
Variable F0 : setset
Variable F1 : setsetsetset
Variable G0 : setset
Variable G1 : setsetsetset
Variable H0 : setset
Variable H1 : setsetsetset
Variable eta : setset
Theorem. (MetaCat_CompNatTransFunctor)
MetaNatTrans Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' F0 F1 G0 G1 etaMetaFunctor Obj Hom id comp Obj' Hom' id' comp' H0 H1MetaNatTrans Obj Hom id comp Obj'' Hom'' id'' comp'' (λX ⇒ F0 (H0 X)) (λX Y f ⇒ F1 (H0 X) (H0 Y) (H1 X Y f)) (λX ⇒ G0 (H0 X)) (λX Y f ⇒ G1 (H0 X) (H0 Y) (H1 X Y f)) (λX ⇒ eta (H0 X))
Proof:
Assume Heta HH.
Apply MetaNatTransE Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' F0 F1 G0 G1 eta Heta to the current goal.
Assume Heta1 Heta2.
Apply MetaFunctorE Obj Hom id comp Obj' Hom' id' comp' H0 H1 HH to the current goal.
Assume HH1 HH2 HH3 HH4.
Apply MetaNatTransI to the current goal.
Let X be given.
Assume HX.
We will prove Hom'' (F0 (H0 X)) (G0 (H0 X)) (eta (H0 X)).
Apply Heta1 to the current goal.
We will prove Obj' (H0 X).
Apply HH1 to the current goal.
An exact proof term for the current goal is HX.
Let X, Y and f be given.
Assume HX HY Hf.
We will prove comp'' (F0 (H0 X)) (G0 (H0 X)) (G0 (H0 Y)) (G1 (H0 X) (H0 Y) (H1 X Y f)) (eta (H0 X)) = comp'' (F0 (H0 X)) (F0 (H0 Y)) (G0 (H0 Y)) (eta (H0 Y)) (F1 (H0 X) (H0 Y) (H1 X Y f)).
Apply Heta2 (H0 X) (H0 Y) (H1 X Y f) to the current goal.
Apply HH1 to the current goal.
An exact proof term for the current goal is HX.
Apply HH1 to the current goal.
An exact proof term for the current goal is HY.
Apply HH2 to the current goal.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is Hf.
End of Section CompNatTransFunctor
Beginning of Section MetaMonad
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Variable T0 : setset
Variable T1 : setsetsetset
Variable eta : setset
Variable mu : setset
Definition. We define MetaMonad to be (∀X, Obj Xcomp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)))(∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X))(∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)) of type prop.
Definition. We define MetaMonad_strict to be MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) T0 T1 etaMetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ T0 (T0 X)) (λX Y f ⇒ T1 (T0 X) (T0 Y) (T1 X Y f)) T0 T1 muMetaMonad of type prop.
Theorem. (MetaMonadI)
(∀X, Obj Xcomp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)))(∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X))(∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X))MetaMonad
Proof:
An exact proof term for the current goal is and3I (∀X, Obj Xcomp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X))) (∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X)) (∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)).
Theorem. (MetaMonadE)
MetaMonad(∀p : prop, ((∀X, Obj Xcomp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)))(∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X))(∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X))p)p)
Proof:
An exact proof term for the current goal is and3E (∀X, Obj Xcomp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X))) (∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X)) (∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)).
Theorem. (MetaMonad_strict_I)
MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) T0 T1 etaMetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ T0 (T0 X)) (λX Y f ⇒ T1 (T0 X) (T0 Y) (T1 X Y f)) T0 T1 muMetaMonadMetaMonad_strict
Proof:
An exact proof term for the current goal is and3I (MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) T0 T1 eta) (MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ T0 (T0 X)) (λX Y f ⇒ T1 (T0 X) (T0 Y) (T1 X Y f)) T0 T1 mu) MetaMonad.
Theorem. (MetaMonad_strict_E)
MetaMonad_strict∀p : prop, (MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) T0 T1 etaMetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ T0 (T0 X)) (λX Y f ⇒ T1 (T0 X) (T0 Y) (T1 X Y f)) T0 T1 muMetaMonadp)p
Proof:
An exact proof term for the current goal is and3E (MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) T0 T1 eta) (MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ T0 (T0 X)) (λX Y f ⇒ T1 (T0 X) (T0 Y) (T1 X Y f)) T0 T1 mu) MetaMonad.
End of Section MetaMonad
Beginning of Section MetaAdjunction
Variable Obj : setprop
Variable Hom : setsetsetprop
Variable id : setset
Variable comp : setsetsetsetsetset
Variable Obj' : setprop
Variable Hom' : setsetsetprop
Variable id' : setset
Variable comp' : setsetsetsetsetset
Variable F0 : setset
Variable F1 : setsetsetset
Variable G0 : setset
Variable G1 : setsetsetset
Variable eta : setset
Variable eps : setset
Definition. We define MetaAdjunction to be (∀X, Obj Xcomp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X))(∀Y, Obj' Ycomp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y)) of type prop.
Definition. We define MetaAdjunction_strict to be MetaFunctor_strict Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj' Hom' id' comp' Obj Hom id comp G0 G1MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) etaMetaNatTrans Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) epsMetaAdjunction of type prop.
Theorem. (MetaAdjunctionI)
(∀X, Obj Xcomp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X))(∀Y, Obj' Ycomp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y))MetaAdjunction
Proof:
An exact proof term for the current goal is andI (∀X, Obj Xcomp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X)) (∀Y, Obj' Ycomp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y)).
Theorem. (MetaAdjunctionE)
MetaAdjunction∀p : prop, ((∀X, Obj Xcomp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X))(∀Y, Obj' Ycomp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y))p)p
Proof:
An exact proof term for the current goal is (λH ⇒ H).
Theorem. (MetaAdjunction_strict_I)
MetaFunctor_strict Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj' Hom' id' comp' Obj Hom id comp G0 G1MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) etaMetaNatTrans Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) epsMetaAdjunctionMetaAdjunction_strict
Proof:
An exact proof term for the current goal is and5I (MetaFunctor_strict Obj Hom id comp Obj' Hom' id' comp' F0 F1) (MetaFunctor Obj' Hom' id' comp' Obj Hom id comp G0 G1) (MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta) (MetaNatTrans Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) eps) MetaAdjunction.
Theorem. (MetaAdjunction_strict_E)
MetaAdjunction_strict∀p : prop, (MetaFunctor_strict Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj' Hom' id' comp' Obj Hom id comp G0 G1MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) etaMetaNatTrans Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) epsMetaAdjunctionp)p
Proof:
An exact proof term for the current goal is and5E (MetaFunctor_strict Obj Hom id comp Obj' Hom' id' comp' F0 F1) (MetaFunctor Obj' Hom' id' comp' Obj Hom id comp G0 G1) (MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta) (MetaNatTrans Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) eps) MetaAdjunction.
Theorem. (MetaAdjunctionMonad)
MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1MetaFunctor Obj' Hom' id' comp' Obj Hom id comp G0 G1MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) etaMetaNatTrans Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) epsMetaAdjunctionMetaMonad Obj Hom id comp (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta (λX ⇒ G1 (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)))
Proof:
Assume HF.
Apply MetaFunctorE Obj Hom id comp Obj' Hom' id' comp' F0 F1 HF to the current goal.
Assume HF1 HF2 HF3 HF4.
Assume HG.
Apply MetaFunctorE Obj' Hom' id' comp' Obj Hom id comp G0 G1 HG to the current goal.
Assume HG1 HG2 HG3 HG4.
Assume Heta.
Apply MetaNatTransE Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta Heta to the current goal.
Assume Heta1 Heta2.
Assume Heps.
Apply MetaNatTransE Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) eps Heps to the current goal.
Assume Heps1: ∀X, Obj' XHom' (F0 (G0 X)) X (eps X).
Assume Heps2: ∀X Y f, Obj' XObj' YHom' X Y fcomp' (F0 (G0 X)) X Y f (eps X) = comp' (F0 (G0 X)) (F0 (G0 Y)) Y (eps Y) (F1 (G0 X) (G0 Y) (G1 X Y f)).
Assume HA.
Apply MetaAdjunctionE HA to the current goal.
Assume HA1 HA2.
Set T0 to be the term λX ⇒ G0 (F0 X) of type setset.
Set T1 to be the term λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f) of type setsetsetset.
Set mu to be the term λX ⇒ G1 (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) of type setset.
We prove the intermediate claim LT: MetaFunctor Obj Hom id comp Obj Hom id comp T0 T1.
An exact proof term for the current goal is MetaCat_CompFunctors Obj Hom id comp Obj' Hom' id' comp' Obj Hom id comp F0 F1 G0 G1 HF HG.
Apply MetaFunctorE Obj Hom id comp Obj Hom id comp T0 T1 LT to the current goal.
Assume HT01 HT02 HT03 HT04.
Apply MetaMonadI to the current goal.
We will prove ∀X, Obj Xcomp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)).
Let X be given.
Assume HX.
We prove the intermediate claim LFX: Obj' (F0 X).
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
We prove the intermediate claim LTX: Obj (T0 X).
An exact proof term for the current goal is HT01 X HX.
We prove the intermediate claim LFTX: Obj' (F0 (T0 X)).
Apply HF1 to the current goal.
An exact proof term for the current goal is LTX.
We prove the intermediate claim LTTX: Obj (T0 (T0 X)).
An exact proof term for the current goal is HT01 (T0 X) LTX.
We prove the intermediate claim LFTTX: Obj' (F0 (T0 (T0 X))).
Apply HF1 to the current goal.
An exact proof term for the current goal is LTTX.
We prove the intermediate claim LepsFX: Hom' (F0 (T0 X)) (F0 X) (eps (F0 X)).
An exact proof term for the current goal is Heps1 (F0 X) LFX.
We prove the intermediate claim LmuX: Hom (T0 (T0 X)) (T0 X) (mu X).
An exact proof term for the current goal is HG2 (F0 (T0 X)) (F0 X) (eps (F0 X)) LFTX LFX LepsFX.
We prove the intermediate claim LFmuX: Hom' (F0 (T0 (T0 X))) (F0 (T0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X)).
An exact proof term for the current goal is HF2 (T0 (T0 X)) (T0 X) (mu X) LTTX LTX LmuX.
We will prove comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)).
Use transitivity with G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X))), and G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (eps (F0 (T0 X)))).
We will prove comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X))).
Use symmetry.
An exact proof term for the current goal is HG4 (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (F1 (T0 (T0 X)) (T0 X) (mu X)) (eps (F0 X)) LFTTX LFTX LFX LFmuX LepsFX.
We will prove G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X))) = G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (eps (F0 (T0 X)))).
Use f_equal.
Use symmetry.
We will prove comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (eps (F0 (T0 X))) = comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X)).
An exact proof term for the current goal is Heps2 (F0 (T0 X)) (F0 X) (eps (F0 X)) LFTX LFX LepsFX.
We will prove G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (eps (F0 (T0 X)))) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)).
An exact proof term for the current goal is HG4 (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 (T0 X))) (eps (F0 X)) LFTTX LFTX LFX (Heps1 (F0 (T0 X)) LFTX) LepsFX.
We will prove ∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X).
Let X be given.
Assume HX.
We will prove comp (G0 (F0 X)) (G0 (F0 (G0 (F0 X)))) (G0 (F0 X)) (G1 (F0 (G0 (F0 X))) (F0 X) (eps (F0 X))) (eta (G0 (F0 X))) = id (G0 (F0 X)).
An exact proof term for the current goal is HA2 (F0 X) (HF1 X HX).
We will prove ∀X, Obj Xcomp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X).
Let X be given.
Assume HX.
We will prove comp (G0 (F0 X)) (G0 (F0 (T0 X))) (G0 (F0 X)) (G1 (F0 (T0 X)) (F0 X) (eps (F0 X))) (G1 (F0 X) (F0 (T0 X)) (F1 X (T0 X) (eta X))) = id (T0 X).
We prove the intermediate claim LFX: Obj' (F0 X).
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
We prove the intermediate claim LTX: Obj (T0 X).
An exact proof term for the current goal is HT01 X HX.
We prove the intermediate claim LFTX: Obj' (F0 (T0 X)).
Apply HF1 to the current goal.
An exact proof term for the current goal is LTX.
Use transitivity with G1 (F0 X) (F0 X) (comp' (F0 X) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 X (T0 X) (eta X))), and G1 (F0 X) (F0 X) (id' (F0 X)).
We will prove comp (G0 (F0 X)) (G0 (F0 (T0 X))) (G0 (F0 X)) (G1 (F0 (T0 X)) (F0 X) (eps (F0 X))) (G1 (F0 X) (F0 (T0 X)) (F1 X (T0 X) (eta X))) = G1 (F0 X) (F0 X) (comp' (F0 X) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 X (T0 X) (eta X))).
Use symmetry.
Apply HG4 (F0 X) (F0 (T0 X)) (F0 X) (F1 X (T0 X) (eta X)) (eps (F0 X)) to the current goal.
An exact proof term for the current goal is LFX.
An exact proof term for the current goal is LFTX.
An exact proof term for the current goal is LFX.
We will prove Hom' (F0 X) (F0 (T0 X)) (F1 X (T0 X) (eta X)).
An exact proof term for the current goal is HF2 X (T0 X) (eta X) HX LTX (Heta1 X HX).
We will prove Hom' (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)).
An exact proof term for the current goal is Heps1 (F0 X) (HF1 X HX).
We will prove G1 (F0 X) (F0 X) (comp' (F0 X) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 X (T0 X) (eta X))) = G1 (F0 X) (F0 X) (id' (F0 X)).
Use f_equal.
An exact proof term for the current goal is HA1 X HX.
We will prove G1 (F0 X) (F0 X) (id' (F0 X)) = id (T0 X).
An exact proof term for the current goal is HG3 (F0 X) LFX.
Theorem. (MetaAdjunctionMonad_strict)
MetaAdjunction_strictMetaMonad_strict Obj Hom id comp (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta (λX ⇒ G1 (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)))
Proof:
Assume HA.
Apply MetaAdjunction_strict_E HA to the current goal.
Assume HA1 HG Heta Heps HA5.
Apply MetaFunctor_strict_E Obj Hom id comp Obj' Hom' id' comp' F0 F1 HA1 to the current goal.
Assume HC HC' HF.
Set T0 to be the term λX ⇒ G0 (F0 X) of type setset.
Set T1 to be the term λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f) of type setsetsetset.
Set mu to be the term λX ⇒ G1 (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) of type setset.
We prove the intermediate claim LT: MetaFunctor Obj Hom id comp Obj Hom id comp T0 T1.
An exact proof term for the current goal is MetaCat_CompFunctors Obj Hom id comp Obj' Hom' id' comp' Obj Hom id comp F0 F1 G0 G1 HF HG.
We prove the intermediate claim LTT: MetaFunctor Obj Hom id comp Obj Hom id comp (λX ⇒ T0 (T0 X)) (λX Y f ⇒ T1 (T0 X) (T0 Y) (T1 X Y f)).
An exact proof term for the current goal is MetaCat_CompFunctors Obj Hom id comp Obj Hom id comp Obj Hom id comp T0 T1 T0 T1 LT LT.
We prove the intermediate claim LFT: MetaFunctor Obj Hom id comp Obj' Hom' id' comp' (λX ⇒ F0 (T0 X)) (λX Y f ⇒ F1 (T0 X) (T0 Y) (T1 X Y f)).
An exact proof term for the current goal is MetaCat_CompFunctors Obj Hom id comp Obj Hom id comp Obj' Hom' id' comp' T0 T1 F0 F1 LT HF.
We prove the intermediate claim LepsF: MetaNatTrans Obj Hom id comp Obj' Hom' id' comp' (λX ⇒ F0 (G0 (F0 X))) (λX Y f ⇒ F1 (G0 (F0 X)) (G0 (F0 Y)) (G1 (F0 X) (F0 Y) (F1 X Y f))) F0 F1 (λX ⇒ eps (F0 X)).
An exact proof term for the current goal is MetaCat_CompNatTransFunctor Obj Hom id comp Obj' Hom' id' comp' Obj' Hom' id' comp' (λX ⇒ F0 (G0 X)) (λX Y f ⇒ F1 (G0 X) (G0 Y) (G1 X Y f)) (λX ⇒ X) (λX Y f ⇒ f) F0 F1 eps Heps HF.
We prove the intermediate claim Lmu: MetaNatTrans Obj Hom id comp Obj Hom id comp (λY ⇒ T0 (T0 Y)) (λX Y g ⇒ T1 (T0 X) (T0 Y) (T1 X Y g)) T0 T1 mu.
An exact proof term for the current goal is MetaCat_CompFunctorNatTrans Obj Hom id comp Obj' Hom' id' comp' Obj Hom id comp (λX ⇒ F0 (G0 (F0 X))) (λX Y f ⇒ F1 (G0 (F0 X)) (G0 (F0 Y)) (G1 (F0 X) (F0 Y) (F1 X Y f))) F0 F1 G0 G1 (λX ⇒ eps (F0 X)) LFT HF LepsF HG.
Apply MetaMonad_strict_I to the current goal.
Apply MetaNatTrans_strict_I to the current goal.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is MetaCat_IdFunctor Obj Hom id comp.
An exact proof term for the current goal is LT.
We will prove MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta.
An exact proof term for the current goal is Heta.
Apply MetaNatTrans_strict_I to the current goal.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is LTT.
An exact proof term for the current goal is LT.
We will prove MetaNatTrans Obj Hom id comp Obj Hom id comp (λY ⇒ T0 (T0 Y)) (λX Y g ⇒ T1 (T0 X) (T0 Y) (T1 X Y g)) T0 T1 mu.
An exact proof term for the current goal is Lmu.
An exact proof term for the current goal is MetaAdjunctionMonad HF HG Heta Heps HA5.
End of Section MetaAdjunction
Beginning of Section MetaCatConcrete
Variable Obj : setprop
Variable U : setset
Variable Hom : setsetsetprop
Theorem. (MetaCatConcrete)
(∀X Y f, Obj XObj YHom X Y ff U YU X)(∀X, Obj XHom X X (lam_id (U X)))(∀X Y Z f g, Obj XObj YObj ZHom X Y fHom Y Z gHom X Z (lam_comp (U X) g f))MetaCat Obj Hom (λX ⇒ lam_id (U X)) (λX Y Z g f ⇒ lam_comp (U X) g f)
Proof:
Assume H1 H2 H3.
Apply MetaCat_I to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
Let X, Y and f be given.
Assume HX HY Hf.
We will prove lam_comp (U X) f (lam_id (U X)) = f.
An exact proof term for the current goal is lam_comp_id_R (U X) (U Y) f (H1 X Y f HX HY Hf).
Let X, Y and f be given.
Assume HX HY Hf.
We will prove lam_comp (U X) (lam_id (U Y)) f = f.
An exact proof term for the current goal is lam_comp_id_L (U X) (U Y) f (H1 X Y f HX HY Hf).
Let X, Y, Z, W, f, g and h be given.
Assume HX HY HZ HW Hf Hg Hh.
Use symmetry.
An exact proof term for the current goal is lam_comp_assoc (U X) (U Y) f (H1 X Y f HX HY Hf) g h.
Theorem. (MetaCatConcreteForgetful)
(∀X Y f, Obj XObj YHom X Y ff U YU X)MetaFunctor Obj Hom (λX ⇒ lam_id (U X)) (λX Y Z f g ⇒ (lam_comp (U X) f g)) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) U (λX Y f ⇒ f)
Proof:
Assume H1.
Set F0 to be the term U.
Set F1 to be the term λX Y f : setf.
Apply MetaFunctorI to the current goal.
Let X be given.
Assume _.
An exact proof term for the current goal is TrueI.
An exact proof term for the current goal is H1.
Let X be given.
Assume _.
Use reflexivity.
Let X, Y, Z, f and g be given.
Assume _ _ _ _ _.
Use reflexivity.
End of Section MetaCatConcrete
Theorem. (MetaCatSet)
MetaCat (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z g f ⇒ lam_comp X g f)
Proof:
Apply MetaCatConcrete (λ_ ⇒ True) (λX ⇒ X) SetHom to the current goal.
Let X, Y and f be given.
Assume HX HY Hf.
An exact proof term for the current goal is Hf.
Let X be given.
Assume HX.
An exact proof term for the current goal is lam_id_exp_In X.
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
An exact proof term for the current goal is lam_comp_exp_In X Y Z f Hf g Hg.
Theorem. (MetaCatHFSet)
MetaCat (λX ⇒ X UnivOf Empty) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g))
Proof:
Apply MetaCatConcrete (λX ⇒ X UnivOf Empty) (λX ⇒ X) SetHom to the current goal.
Let X, Y and f be given.
Assume HX HY Hf.
An exact proof term for the current goal is Hf.
Let X be given.
Assume HX.
An exact proof term for the current goal is lam_id_exp_In X.
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
An exact proof term for the current goal is lam_comp_exp_In X Y Z f Hf g Hg.
Theorem. (MetaCatSmallSet)
MetaCat (λX ⇒ X UnivOf (UnivOf Empty)) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g))
Proof:
Apply MetaCatConcrete (λX ⇒ X UnivOf (UnivOf Empty)) (λX ⇒ X) SetHom to the current goal.
Let X, Y and f be given.
Assume HX HY Hf.
An exact proof term for the current goal is Hf.
Let X be given.
Assume HX.
An exact proof term for the current goal is lam_id_exp_In X.
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
An exact proof term for the current goal is lam_comp_exp_In X Y Z f Hf g Hg.
Theorem. (MetaCatConcreteForgetful_strict)
∀Obj : setprop, ∀U : setset, ∀Hom : setsetsetprop, (∀X Y f, Obj XObj YHom X Y ff U YU X)(∀X, Obj XHom X X (lam_id (U X)))(∀X Y Z f g, Obj XObj YObj ZHom X Y fHom Y Z gHom X Z (lam_comp (U X) g f))MetaFunctor_strict Obj Hom (λX ⇒ lam_id (U X)) (λX Y Z f g ⇒ (lam_comp (U X) f g)) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) U (λX Y f ⇒ f)
Proof:
Let Obj, U and Hom be given.
Assume H1 H2 H3.
Apply MetaFunctor_strict_I to the current goal.
An exact proof term for the current goal is MetaCatConcrete Obj U Hom H1 H2 H3.
An exact proof term for the current goal is MetaCatSet.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj U Hom H1.
Definition. We define Hom_struct_e to be λX Y f ⇒ unpack_e_o X (λX' eX ⇒ unpack_e_o Y (λY' eY ⇒ f Y'X'f eX = eY)) of type setsetsetprop.
Definition. We define Hom_struct_u to be λX Y f ⇒ unpack_u_o X (λX' uX ⇒ unpack_u_o Y (λY' uY ⇒ f Y'X'∀xX', f (uX x) = uY (f x))) of type setsetsetprop.
Definition. We define Hom_struct_b to be λX Y f ⇒ unpack_b_o X (λX' opX ⇒ unpack_b_o Y (λY' opY ⇒ f Y'X'∀x yX', f (opX x y) = opY (f x) (f y))) of type setsetsetprop.
Definition. We define Hom_struct_p to be λX Y f ⇒ unpack_p_o X (λX' pX ⇒ unpack_p_o Y (λY' pY ⇒ f Y'X'∀xX', pX xpY (f x))) of type setsetsetprop.
Definition. We define Hom_struct_r to be λX Y f ⇒ unpack_r_o X (λX' rX ⇒ unpack_r_o Y (λY' rY ⇒ f Y'X'∀x yX', rX x yrY (f x) (f y))) of type setsetsetprop.
Definition. We define Hom_struct_c to be λX Y f ⇒ unpack_c_o X (λX' CX ⇒ unpack_c_o Y (λY' CY ⇒ f Y'X'∀U : setprop, (∀y, U yy Y')CY UCX (λx ⇒ x X'U (f x)))) of type setsetsetprop.
Definition. We define Hom_struct_b_b_e to be λX Y f ⇒ unpack_b_b_e_o X (λX' opX op2X eX ⇒ unpack_b_b_e_o Y (λY' opY op2Y eY ⇒ f Y'X'(∀x yX', f (opX x y) = opY (f x) (f y))(∀x yX', f (op2X x y) = op2Y (f x) (f y))f eX = eY)) of type setsetsetprop.
Definition. We define Hom_struct_b_b_e_e to be λX Y f ⇒ unpack_b_b_e_e_o X (λX' opX op2X eX e2X ⇒ unpack_b_b_e_e_o Y (λY' opY op2Y eY e2Y ⇒ f Y'X'(∀x yX', f (opX x y) = opY (f x) (f y))(∀x yX', f (op2X x y) = op2Y (f x) (f y))f eX = eYf e2X = e2Y)) of type setsetsetprop.
Definition. We define Hom_struct_b_b_r_e_e to be λX Y f ⇒ unpack_b_b_r_e_e_o X (λX' opX op2X rX eX e2X ⇒ unpack_b_b_r_e_e_o Y (λY' opY op2Y rY eY e2Y ⇒ f Y'X'(∀x yX', f (opX x y) = opY (f x) (f y))(∀x yX', f (op2X x y) = op2Y (f x) (f y))(∀x yX', rX x yrY (f x) (f y))f eX = eYf e2X = e2Y)) of type setsetsetprop.
Theorem. (Hom_struct_e_pack)
∀X Y eX eY f, (Hom_struct_e (pack_e X eX) (pack_e Y eY) f) = (f YXf eX = eY)
Proof:
Let X, Y, eX, eY and f be given.
Set Phi to be the term λX eX Y eY ⇒ f YXf eX = eY of type setsetsetsetprop.
Set PhiX to be the term λX eX ⇒ unpack_e_o (pack_e Y eY) (λY' eY ⇒ Phi X eX Y' eY) of type setsetprop.
We will prove unpack_e_o (pack_e X eX) PhiX = Phi X eX Y eY.
Use transitivity with and PhiX X eX.
An exact proof term for the current goal is unpack_e_o_eq PhiX X eX.
We will prove unpack_e_o (pack_e Y eY) (Phi X eX) = Phi X eX Y eY.
An exact proof term for the current goal is unpack_e_o_eq (Phi X eX) Y eY.
Theorem. (Hom_struct_u_pack)
∀X Y, ∀opX opY : setset, ∀f, (Hom_struct_u (pack_u X opX) (pack_u Y opY) f) = (f YX(∀xX, f (opX x) = opY (f x)))
Proof:
Let X, Y, opX, opY and f be given.
Set Phi to be the term λX opX Y opY ⇒ f YX(∀xX, f (opX x) = opY (f x)) of type set(setset)set(setset)prop.
Set PhiX to be the term λX opX ⇒ unpack_u_o (pack_u Y opY) (λY' opY ⇒ Phi X opX Y' opY) of type set(setset)prop.
We will prove unpack_u_o (pack_u X opX) PhiX = Phi X opX Y opY.
We prove the intermediate claim L1: ∀opX : setset, ∀opY' : setset, (∀xY, opY x = opY' x)Phi X opX Y opY' = Phi X opX Y opY.
Let opX be given.
Let opY' be given.
Assume HopY'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀xX, f (opX x) = opY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
rewrite the current goal using HopY' (f x) (Lf x Hx) (from left to right).
An exact proof term for the current goal is H2 x Hx.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀xX, f (opX x) = opY' (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
rewrite the current goal using HopY' (f x) (Lf x Hx) (from right to left).
An exact proof term for the current goal is H2 x Hx.
We prove the intermediate claim L2: ∀opX' : setset, (∀xX, opX x = opX' x)PhiX X opX' = PhiX X opX.
Let opX' be given.
Assume HopX'.
We will prove PhiX X opX' = PhiX X opX.
We will prove unpack_u_o (pack_u Y opY) (λY' opY ⇒ Phi X opX' Y' opY) = unpack_u_o (pack_u Y opY) (λY' opY ⇒ Phi X opX Y' opY).
Use transitivity with Phi X opX' Y opY, and Phi X opX Y opY.
We will prove unpack_u_o (pack_u Y opY) (Phi X opX') = Phi X opX' Y opY.
An exact proof term for the current goal is unpack_u_o_eq (Phi X opX') Y opY (L1 opX').
We will prove Phi X opX' Y opY = Phi X opX Y opY.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀xX, f (opX x) = opY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
rewrite the current goal using HopX' x Hx (from left to right).
An exact proof term for the current goal is H2 x Hx.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀xX, f (opX' x) = opY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
rewrite the current goal using HopX' x Hx (from right to left).
An exact proof term for the current goal is H2 x Hx.
Use symmetry.
An exact proof term for the current goal is unpack_u_o_eq (Phi X opX) Y opY (L1 opX).
Use transitivity with and PhiX X opX.
An exact proof term for the current goal is unpack_u_o_eq PhiX X opX L2.
We will prove unpack_u_o (pack_u Y opY) (Phi X opX) = Phi X opX Y opY.
An exact proof term for the current goal is unpack_u_o_eq (Phi X opX) Y opY (L1 opX).
Theorem. (Hom_struct_b_pack)
∀X Y, ∀opX opY : setsetset, ∀f, (Hom_struct_b (pack_b X opX) (pack_b Y opY) f) = (f YX(∀x yX, f (opX x y) = opY (f x) (f y)))
Proof:
Let X, Y, opX, opY and f be given.
Set Phi to be the term λX opX Y opY ⇒ f YX(∀x yX, f (opX x y) = opY (f x) (f y)) of type set(setsetset)set(setsetset)prop.
Set PhiX to be the term λX opX ⇒ unpack_b_o (pack_b Y opY) (λY' opY ⇒ Phi X opX Y' opY) of type set(setsetset)prop.
We will prove unpack_b_o (pack_b X opX) PhiX = Phi X opX Y opY.
We prove the intermediate claim L1: ∀opX : setsetset, ∀opY' : setsetset, (∀x yY, opY x y = opY' x y)Phi X opX Y opY' = Phi X opX Y opY.
Let opX be given.
Let opY' be given.
Assume HopY'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, f (opX x y) = opY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopY' (f x) (Lf x Hx) (f y) (Lf y Hy) (from left to right).
An exact proof term for the current goal is H2 x Hx y Hy.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, f (opX x y) = opY' (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopY' (f x) (Lf x Hx) (f y) (Lf y Hy) (from right to left).
An exact proof term for the current goal is H2 x Hx y Hy.
We prove the intermediate claim L2: ∀opX' : setsetset, (∀x yX, opX x y = opX' x y)PhiX X opX' = PhiX X opX.
Let opX' be given.
Assume HopX'.
We will prove PhiX X opX' = PhiX X opX.
We will prove unpack_b_o (pack_b Y opY) (λY' opY ⇒ Phi X opX' Y' opY) = unpack_b_o (pack_b Y opY) (λY' opY ⇒ Phi X opX Y' opY).
Use transitivity with Phi X opX' Y opY, and Phi X opX Y opY.
We will prove unpack_b_o (pack_b Y opY) (Phi X opX') = Phi X opX' Y opY.
An exact proof term for the current goal is unpack_b_o_eq (Phi X opX') Y opY (L1 opX').
We will prove Phi X opX' Y opY = Phi X opX Y opY.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀x yX, f (opX x y) = opY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopX' x Hx y Hy (from left to right).
An exact proof term for the current goal is H2 x Hx y Hy.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀x yX, f (opX' x y) = opY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopX' x Hx y Hy (from right to left).
An exact proof term for the current goal is H2 x Hx y Hy.
Use symmetry.
An exact proof term for the current goal is unpack_b_o_eq (Phi X opX) Y opY (L1 opX).
Use transitivity with and PhiX X opX.
An exact proof term for the current goal is unpack_b_o_eq PhiX X opX L2.
We will prove unpack_b_o (pack_b Y opY) (Phi X opX) = Phi X opX Y opY.
An exact proof term for the current goal is unpack_b_o_eq (Phi X opX) Y opY (L1 opX).
Theorem. (Hom_struct_p_pack)
∀X Y, ∀pX pY : setprop, ∀f, (Hom_struct_p (pack_p X pX) (pack_p Y pY) f) = (f YX(∀xX, pX xpY (f x)))
Proof:
Let X, Y, pX, pY and f be given.
Set Phi to be the term λX pX Y pY ⇒ f YX(∀xX, pX xpY (f x)) of type set(setprop)set(setprop)prop.
Set PhiX to be the term λX pX ⇒ unpack_p_o (pack_p Y pY) (λY' pY ⇒ Phi X pX Y' pY) of type set(setprop)prop.
We will prove unpack_p_o (pack_p X pX) PhiX = Phi X pX Y pY.
We prove the intermediate claim L1: ∀pX : setprop, ∀pY' : setprop, (∀xY, pY xpY' x)Phi X pX Y pY' = Phi X pX Y pY.
Let pX be given.
Let pY' be given.
Assume HpY'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀xX, pX xpY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx H7.
Apply iffER (pY (f x)) (pY' (f x)) (HpY' (f x) (Lf x Hx)) to the current goal.
An exact proof term for the current goal is H2 x Hx H7.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀xX, pX xpY' (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx H7.
Apply iffEL (pY (f x)) (pY' (f x)) (HpY' (f x) (Lf x Hx)) to the current goal.
An exact proof term for the current goal is H2 x Hx H7.
We prove the intermediate claim L2: ∀pX' : setprop, (∀xX, pX xpX' x)PhiX X pX' = PhiX X pX.
Let pX' be given.
Assume HpX'.
We will prove PhiX X pX' = PhiX X pX.
We will prove unpack_p_o (pack_p Y pY) (λY' pY ⇒ Phi X pX' Y' pY) = unpack_p_o (pack_p Y pY) (λY' pY ⇒ Phi X pX Y' pY).
Use transitivity with Phi X pX' Y pY, and Phi X pX Y pY.
We will prove unpack_p_o (pack_p Y pY) (Phi X pX') = Phi X pX' Y pY.
An exact proof term for the current goal is unpack_p_o_eq (Phi X pX') Y pY (L1 pX').
We will prove Phi X pX' Y pY = Phi X pX Y pY.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀xX, pX xpY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx H7.
Apply H2 x Hx to the current goal.
Apply iffEL (pX x) (pX' x) (HpX' x Hx) to the current goal.
An exact proof term for the current goal is H7.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀xX, pX' xpY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx H7.
Apply H2 x Hx to the current goal.
Apply iffER (pX x) (pX' x) (HpX' x Hx) to the current goal.
An exact proof term for the current goal is H7.
Use symmetry.
An exact proof term for the current goal is unpack_p_o_eq (Phi X pX) Y pY (L1 pX).
Use transitivity with and PhiX X pX.
An exact proof term for the current goal is unpack_p_o_eq PhiX X pX L2.
We will prove unpack_p_o (pack_p Y pY) (Phi X pX) = Phi X pX Y pY.
An exact proof term for the current goal is unpack_p_o_eq (Phi X pX) Y pY (L1 pX).
Theorem. (Hom_struct_r_pack)
∀X Y, ∀rX rY : setsetprop, ∀f, (Hom_struct_r (pack_r X rX) (pack_r Y rY) f) = (f YX(∀x yX, rX x yrY (f x) (f y)))
Proof:
Let X, Y, rX, rY and f be given.
Set Phi to be the term λX rX Y rY ⇒ f YX(∀x yX, rX x yrY (f x) (f y)) of type set(setsetprop)set(setsetprop)prop.
Set PhiX to be the term λX rX ⇒ unpack_r_o (pack_r Y rY) (λY' rY ⇒ Phi X rX Y' rY) of type set(setsetprop)prop.
We will prove unpack_r_o (pack_r X rX) PhiX = Phi X rX Y rY.
We prove the intermediate claim L1: ∀rX : setsetprop, ∀rY' : setsetprop, (∀x yY, rY x yrY' x y)Phi X rX Y rY' = Phi X rX Y rY.
Let rX be given.
Let rY' be given.
Assume HrY'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, rX x yrY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply iffER (rY (f x) (f y)) (rY' (f x) (f y)) (HrY' (f x) (Lf x Hx) (f y) (Lf y Hy)) to the current goal.
An exact proof term for the current goal is H2 x Hx y Hy H7.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, rX x yrY' (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply iffEL (rY (f x) (f y)) (rY' (f x) (f y)) (HrY' (f x) (Lf x Hx) (f y) (Lf y Hy)) to the current goal.
An exact proof term for the current goal is H2 x Hx y Hy H7.
We prove the intermediate claim L2: ∀rX' : setsetprop, (∀x yX, rX x yrX' x y)PhiX X rX' = PhiX X rX.
Let rX' be given.
Assume HrX'.
We will prove PhiX X rX' = PhiX X rX.
We will prove unpack_r_o (pack_r Y rY) (λY' rY ⇒ Phi X rX' Y' rY) = unpack_r_o (pack_r Y rY) (λY' rY ⇒ Phi X rX Y' rY).
Use transitivity with Phi X rX' Y rY, and Phi X rX Y rY.
We will prove unpack_r_o (pack_r Y rY) (Phi X rX') = Phi X rX' Y rY.
An exact proof term for the current goal is unpack_r_o_eq (Phi X rX') Y rY (L1 rX').
We will prove Phi X rX' Y rY = Phi X rX Y rY.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀x yX, rX x yrY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply H2 x Hx y Hy to the current goal.
Apply iffEL (rX x y) (rX' x y) (HrX' x Hx y Hy) to the current goal.
An exact proof term for the current goal is H7.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀x yX, rX' x yrY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply H2 x Hx y Hy to the current goal.
Apply iffER (rX x y) (rX' x y) (HrX' x Hx y Hy) to the current goal.
An exact proof term for the current goal is H7.
Use symmetry.
An exact proof term for the current goal is unpack_r_o_eq (Phi X rX) Y rY (L1 rX).
Use transitivity with and PhiX X rX.
An exact proof term for the current goal is unpack_r_o_eq PhiX X rX L2.
We will prove unpack_r_o (pack_r Y rY) (Phi X rX) = Phi X rX Y rY.
An exact proof term for the current goal is unpack_r_o_eq (Phi X rX) Y rY (L1 rX).
Theorem. (Hom_struct_c_pack)
∀X Y, ∀CX CY : (setprop)prop, ∀f, (Hom_struct_c (pack_c X CX) (pack_c Y CY) f) = (f YX(∀U : setprop, (∀y, U yy Y)CY UCX (λx ⇒ x XU (f x))))
Proof:
Let X, Y, CX, CY and f be given.
Set Phi to be the term λX CX Y CY ⇒ f YX(∀U : setprop, (∀y, U yy Y)CY UCX (λx ⇒ x XU (f x))) of type set((setprop)prop)set((setprop)prop)prop.
Set PhiX to be the term λX CX ⇒ unpack_c_o (pack_c Y CY) (λY' CY ⇒ Phi X CX Y' CY) of type set((setprop)prop)prop.
We will prove unpack_c_o (pack_c X CX) PhiX = Phi X CX Y CY.
We prove the intermediate claim L1: ∀CX : (setprop)prop, ∀CY' : (setprop)prop, (∀U : setprop, (∀y, U yy Y)(CY UCY' U))Phi X CX Y CY' = Phi X CX Y CY.
Let CX be given.
Let CY' be given.
Assume HCY'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀U : setprop, (∀y, U yy Y)CY UCX (λx ⇒ x XU (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let U be given.
Assume HU1 HU2.
We will prove CX (λx ⇒ x XU (f x)).
Apply H2 to the current goal.
An exact proof term for the current goal is HU1.
We will prove CY' U.
An exact proof term for the current goal is iffEL (CY U) (CY' U) (HCY' U HU1) HU2.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀U : setprop, (∀y, U yy Y)CY' UCX (λx ⇒ x XU (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let U be given.
Assume HU1 HU2.
We will prove CX (λx ⇒ x XU (f x)).
Apply H2 to the current goal.
An exact proof term for the current goal is HU1.
We will prove CY U.
An exact proof term for the current goal is iffER (CY U) (CY' U) (HCY' U HU1) HU2.
We prove the intermediate claim L2: ∀CX' : (setprop)prop, (∀U : setprop, (∀x, U xx X)(CX UCX' U))PhiX X CX' = PhiX X CX.
Let CX' be given.
Assume HCX'.
We will prove PhiX X CX' = PhiX X CX.
We will prove unpack_c_o (pack_c Y CY) (λY' CY ⇒ Phi X CX' Y' CY) = unpack_c_o (pack_c Y CY) (λY' CY ⇒ Phi X CX Y' CY).
Use transitivity with Phi X CX' Y CY, and Phi X CX Y CY.
We will prove unpack_c_o (pack_c Y CY) (Phi X CX') = Phi X CX' Y CY.
An exact proof term for the current goal is unpack_c_o_eq (Phi X CX') Y CY (L1 CX').
We will prove Phi X CX' Y CY = Phi X CX Y CY.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1: f YX.
Assume H2: ∀U : setprop, (∀y, U yy Y)CY UCX' (λx ⇒ x XU (f x)).
We will prove f YX(∀U : setprop, (∀y, U yy Y)CY UCX (λx ⇒ x XU (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let U be given.
Assume HU1: ∀y, U yy Y.
Assume HU2: CY U.
We prove the intermediate claim LU: ∀x, x XU (f x)x X.
Let x be given.
An exact proof term for the current goal is andEL (x X) (U (f x)).
Apply iffER (CX (λx ⇒ x XU (f x))) (CX' (λx ⇒ x XU (f x))) (HCX' (λx ⇒ x XU (f x)) LU) to the current goal.
An exact proof term for the current goal is H2 U HU1 HU2.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f YX(∀U : setprop, (∀y, U yy Y)CY UCX' (λx ⇒ x XU (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let U be given.
Assume HU1: ∀y, U yy Y.
Assume HU2: CY U.
We prove the intermediate claim LU: ∀x, x XU (f x)x X.
Let x be given.
An exact proof term for the current goal is andEL (x X) (U (f x)).
Apply iffEL (CX (λx ⇒ x XU (f x))) (CX' (λx ⇒ x XU (f x))) (HCX' (λx ⇒ x XU (f x)) LU) to the current goal.
An exact proof term for the current goal is H2 U HU1 HU2.
Use symmetry.
An exact proof term for the current goal is unpack_c_o_eq (Phi X CX) Y CY (L1 CX).
Use transitivity with and PhiX X CX.
An exact proof term for the current goal is unpack_c_o_eq PhiX X CX L2.
We will prove unpack_c_o (pack_c Y CY) (Phi X CX) = Phi X CX Y CY.
An exact proof term for the current goal is unpack_c_o_eq (Phi X CX) Y CY (L1 CX).
Theorem. (Hom_struct_b_b_e_pack)
∀X Y, ∀opX op2X opY op2Y : setsetset, ∀eX eY f, (Hom_struct_b_b_e (pack_b_b_e X opX op2X eX) (pack_b_b_e Y opY op2Y eY) f) = (f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))f eX = eY)
Proof:
Let X, Y, opX, op2X, opY, op2Y, eX, eY and f be given.
Set Phi to be the term λX opX op2X eX Y opY op2Y eY ⇒ f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))f eX = eY of type set(setsetset)(setsetset)setset(setsetset)(setsetset)setprop.
Set PhiX to be the term λX opX op2X eX ⇒ unpack_b_b_e_o (pack_b_b_e Y opY op2Y eY) (λY' opY op2Y eY ⇒ Phi X opX op2X eX Y' opY op2Y eY) of type set(setsetset)(setsetset)setprop.
We will prove unpack_b_b_e_o (pack_b_b_e X opX op2X eX) PhiX = Phi X opX op2X eX Y opY op2Y eY.
We prove the intermediate claim L1: ∀opX op2X : setsetset, ∀opY' : setsetset, (∀x yY, opY x y = opY' x y)∀op2Y' : setsetset, (∀x yY, op2Y x y = op2Y' x y)Phi X opX op2X eX Y opY' op2Y' eY = Phi X opX op2X eX Y opY op2Y eY.
Let opX and op2X be given.
Let opY' be given.
Assume HopY'.
Let op2Y' be given.
Assume Hop2Y'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply and4E (f YX) (∀x yX, f (opX x y) = opY' (f x) (f y)) (∀x yX, f (op2X x y) = op2Y' (f x) (f y)) (f eX = eY) H to the current goal.
Assume H1 H2 H3 H4.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))f eX = eY.
Apply and4I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopY' (f x) (Lf x Hx) (f y) (Lf y Hy) (from left to right).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2Y' (f x) (Lf x Hx) (f y) (Lf y Hy) (from left to right).
An exact proof term for the current goal is H3 x Hx y Hy.
An exact proof term for the current goal is H4.
Assume H.
Apply and4E (f YX) (∀x yX, f (opX x y) = opY (f x) (f y)) (∀x yX, f (op2X x y) = op2Y (f x) (f y)) (f eX = eY) H to the current goal.
Assume H1 H2 H3 H4.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, f (opX x y) = opY' (f x) (f y))(∀x yX, f (op2X x y) = op2Y' (f x) (f y))f eX = eY.
Apply and4I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopY' (f x) (Lf x Hx) (f y) (Lf y Hy) (from right to left).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2Y' (f x) (Lf x Hx) (f y) (Lf y Hy) (from right to left).
An exact proof term for the current goal is H3 x Hx y Hy.
An exact proof term for the current goal is H4.
We prove the intermediate claim L2: ∀opX' : setsetset, (∀x yX, opX x y = opX' x y)∀op2X' : setsetset, (∀x yX, op2X x y = op2X' x y)PhiX X opX' op2X' eX = PhiX X opX op2X eX.
Let opX' be given.
Assume HopX'.
Let op2X' be given.
Assume Hop2X'.
We will prove PhiX X opX' op2X' eX = PhiX X opX op2X eX.
We will prove unpack_b_b_e_o (pack_b_b_e Y opY op2Y eY) (λY' opY op2Y eY ⇒ Phi X opX' op2X' eX Y' opY op2Y eY) = unpack_b_b_e_o (pack_b_b_e Y opY op2Y eY) (λY' opY op2Y eY ⇒ Phi X opX op2X eX Y' opY op2Y eY).
Use transitivity with Phi X opX' op2X' eX Y opY op2Y eY, and Phi X opX op2X eX Y opY op2Y eY.
We will prove unpack_b_b_e_o (pack_b_b_e Y opY op2Y eY) (Phi X opX' op2X' eX) = Phi X opX' op2X' eX Y opY op2Y eY.
An exact proof term for the current goal is unpack_b_b_e_o_eq (Phi X opX' op2X' eX) Y opY op2Y eY (L1 opX' op2X').
We will prove Phi X opX' op2X' eX Y opY op2Y eY = Phi X opX op2X eX Y opY op2Y eY.
Apply prop_ext_2 to the current goal.
Assume H.
Apply and4E (f YX) (∀x yX, f (opX' x y) = opY (f x) (f y)) (∀x yX, f (op2X' x y) = op2Y (f x) (f y)) (f eX = eY) H to the current goal.
Assume H1 H2 H3 H4.
We will prove f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))f eX = eY.
Apply and4I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopX' x Hx y Hy (from left to right).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2X' x Hx y Hy (from left to right).
An exact proof term for the current goal is H3 x Hx y Hy.
An exact proof term for the current goal is H4.
Assume H.
Apply and4E (f YX) (∀x yX, f (opX x y) = opY (f x) (f y)) (∀x yX, f (op2X x y) = op2Y (f x) (f y)) (f eX = eY) H to the current goal.
Assume H1 H2 H3 H4.
We will prove f YX(∀x yX, f (opX' x y) = opY (f x) (f y))(∀x yX, f (op2X' x y) = op2Y (f x) (f y))f eX = eY.
Apply and4I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopX' x Hx y Hy (from right to left).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2X' x Hx y Hy (from right to left).
An exact proof term for the current goal is H3 x Hx y Hy.
An exact proof term for the current goal is H4.
Use symmetry.
An exact proof term for the current goal is unpack_b_b_e_o_eq (Phi X opX op2X eX) Y opY op2Y eY (L1 opX op2X).
Use transitivity with and PhiX X opX op2X eX.
An exact proof term for the current goal is unpack_b_b_e_o_eq PhiX X opX op2X eX L2.
We will prove unpack_b_b_e_o (pack_b_b_e Y opY op2Y eY) (Phi X opX op2X eX) = Phi X opX op2X eX Y opY op2Y eY.
An exact proof term for the current goal is unpack_b_b_e_o_eq (Phi X opX op2X eX) Y opY op2Y eY (L1 opX op2X).
Theorem. (Hom_struct_b_b_e_e_pack)
∀X Y, ∀opX op2X opY op2Y : setsetset, ∀eX e2X eY e2Y f, (Hom_struct_b_b_e_e (pack_b_b_e_e X opX op2X eX e2X) (pack_b_b_e_e Y opY op2Y eY e2Y) f) = (f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))f eX = eYf e2X = e2Y)
Proof:
Let X, Y, opX, op2X, opY, op2Y, eX, e2X, eY, e2Y and f be given.
Set Phi to be the term λX opX op2X eX e2X Y opY op2Y eY e2Y ⇒ f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))f eX = eYf e2X = e2Y of type set(setsetset)(setsetset)setsetset(setsetset)(setsetset)setsetprop.
Set PhiX to be the term λX opX op2X eX e2X ⇒ unpack_b_b_e_e_o (pack_b_b_e_e Y opY op2Y eY e2Y) (λY' opY op2Y eY e2Y ⇒ Phi X opX op2X eX e2X Y' opY op2Y eY e2Y) of type set(setsetset)(setsetset)setsetprop.
We will prove unpack_b_b_e_e_o (pack_b_b_e_e X opX op2X eX e2X) PhiX = Phi X opX op2X eX e2X Y opY op2Y eY e2Y.
We prove the intermediate claim L1: ∀opX op2X : setsetset, ∀opY' : setsetset, (∀x yY, opY x y = opY' x y)∀op2Y' : setsetset, (∀x yY, op2Y x y = op2Y' x y)Phi X opX op2X eX e2X Y opY' op2Y' eY e2Y = Phi X opX op2X eX e2X Y opY op2Y eY e2Y.
Let opX and op2X be given.
Let opY' be given.
Assume HopY'.
Let op2Y' be given.
Assume Hop2Y'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply and5E (f YX) (∀x yX, f (opX x y) = opY' (f x) (f y)) (∀x yX, f (op2X x y) = op2Y' (f x) (f y)) (f eX = eY) (f e2X = e2Y) H to the current goal.
Assume H1 H2 H3 H4 H5.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))f eX = eYf e2X = e2Y.
Apply and5I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopY' (f x) (Lf x Hx) (f y) (Lf y Hy) (from left to right).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2Y' (f x) (Lf x Hx) (f y) (Lf y Hy) (from left to right).
An exact proof term for the current goal is H3 x Hx y Hy.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
Assume H.
Apply and5E (f YX) (∀x yX, f (opX x y) = opY (f x) (f y)) (∀x yX, f (op2X x y) = op2Y (f x) (f y)) (f eX = eY) (f e2X = e2Y) H to the current goal.
Assume H1 H2 H3 H4 H5.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, f (opX x y) = opY' (f x) (f y))(∀x yX, f (op2X x y) = op2Y' (f x) (f y))f eX = eYf e2X = e2Y.
Apply and5I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopY' (f x) (Lf x Hx) (f y) (Lf y Hy) (from right to left).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2Y' (f x) (Lf x Hx) (f y) (Lf y Hy) (from right to left).
An exact proof term for the current goal is H3 x Hx y Hy.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
We prove the intermediate claim L2: ∀opX' : setsetset, (∀x yX, opX x y = opX' x y)∀op2X' : setsetset, (∀x yX, op2X x y = op2X' x y)PhiX X opX' op2X' eX e2X = PhiX X opX op2X eX e2X.
Let opX' be given.
Assume HopX'.
Let op2X' be given.
Assume Hop2X'.
We will prove PhiX X opX' op2X' eX e2X = PhiX X opX op2X eX e2X.
We will prove unpack_b_b_e_e_o (pack_b_b_e_e Y opY op2Y eY e2Y) (λY' opY op2Y eY e2Y ⇒ Phi X opX' op2X' eX e2X Y' opY op2Y eY e2Y) = unpack_b_b_e_e_o (pack_b_b_e_e Y opY op2Y eY e2Y) (λY' opY op2Y eY e2Y ⇒ Phi X opX op2X eX e2X Y' opY op2Y eY e2Y).
Use transitivity with Phi X opX' op2X' eX e2X Y opY op2Y eY e2Y, and Phi X opX op2X eX e2X Y opY op2Y eY e2Y.
We will prove unpack_b_b_e_e_o (pack_b_b_e_e Y opY op2Y eY e2Y) (Phi X opX' op2X' eX e2X) = Phi X opX' op2X' eX e2X Y opY op2Y eY e2Y.
An exact proof term for the current goal is unpack_b_b_e_e_o_eq (Phi X opX' op2X' eX e2X) Y opY op2Y eY e2Y (L1 opX' op2X').
We will prove Phi X opX' op2X' eX e2X Y opY op2Y eY e2Y = Phi X opX op2X eX e2X Y opY op2Y eY e2Y.
Apply prop_ext_2 to the current goal.
Assume H.
Apply and5E (f YX) (∀x yX, f (opX' x y) = opY (f x) (f y)) (∀x yX, f (op2X' x y) = op2Y (f x) (f y)) (f eX = eY) (f e2X = e2Y) H to the current goal.
Assume H1 H2 H3 H4 H5.
We will prove f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))f eX = eYf e2X = e2Y.
Apply and5I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopX' x Hx y Hy (from left to right).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2X' x Hx y Hy (from left to right).
An exact proof term for the current goal is H3 x Hx y Hy.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
Assume H.
Apply and5E (f YX) (∀x yX, f (opX x y) = opY (f x) (f y)) (∀x yX, f (op2X x y) = op2Y (f x) (f y)) (f eX = eY) (f e2X = e2Y) H to the current goal.
Assume H1 H2 H3 H4 H5.
We will prove f YX(∀x yX, f (opX' x y) = opY (f x) (f y))(∀x yX, f (op2X' x y) = op2Y (f x) (f y))f eX = eYf e2X = e2Y.
Apply and5I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopX' x Hx y Hy (from right to left).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2X' x Hx y Hy (from right to left).
An exact proof term for the current goal is H3 x Hx y Hy.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
Use symmetry.
An exact proof term for the current goal is unpack_b_b_e_e_o_eq (Phi X opX op2X eX e2X) Y opY op2Y eY e2Y (L1 opX op2X).
Use transitivity with and PhiX X opX op2X eX e2X.
An exact proof term for the current goal is unpack_b_b_e_e_o_eq PhiX X opX op2X eX e2X L2.
We will prove unpack_b_b_e_e_o (pack_b_b_e_e Y opY op2Y eY e2Y) (Phi X opX op2X eX e2X) = Phi X opX op2X eX e2X Y opY op2Y eY e2Y.
An exact proof term for the current goal is unpack_b_b_e_e_o_eq (Phi X opX op2X eX e2X) Y opY op2Y eY e2Y (L1 opX op2X).
Theorem. (Hom_struct_b_b_r_e_e_pack)
∀X Y, ∀opX op2X opY op2Y : setsetset, ∀rX rY : setsetprop, ∀eX e2X eY e2Y f, (Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X opX op2X rX eX e2X) (pack_b_b_r_e_e Y opY op2Y rY eY e2Y) f) = (f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))(∀x yX, rX x yrY (f x) (f y))f eX = eYf e2X = e2Y)
Proof:
Let X, Y, opX, op2X, opY, op2Y, rX, rY, eX, e2X, eY, e2Y and f be given.
Set Phi to be the term λX opX op2X rX eX e2X Y opY op2Y rY eY e2Y ⇒ f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))(∀x yX, rX x yrY (f x) (f y))f eX = eYf e2X = e2Y of type set(setsetset)(setsetset)(setsetprop)setsetset(setsetset)(setsetset)(setsetprop)setsetprop.
Set PhiX to be the term λX opX op2X rX eX e2X ⇒ unpack_b_b_r_e_e_o (pack_b_b_r_e_e Y opY op2Y rY eY e2Y) (λY' opY op2Y rY eY e2Y ⇒ Phi X opX op2X rX eX e2X Y' opY op2Y rY eY e2Y) of type set(setsetset)(setsetset)(setsetprop)setsetprop.
We will prove unpack_b_b_r_e_e_o (pack_b_b_r_e_e X opX op2X rX eX e2X) PhiX = Phi X opX op2X rX eX e2X Y opY op2Y rY eY e2Y.
We prove the intermediate claim L1: ∀opX op2X : setsetset, ∀rX : setsetprop, ∀opY' : setsetset, (∀x yY, opY x y = opY' x y)∀op2Y' : setsetset, (∀x yY, op2Y x y = op2Y' x y)∀rY' : setsetprop, (∀x yY, rY x yrY' x y)Phi X opX op2X rX eX e2X Y opY' op2Y' rY' eY e2Y = Phi X opX op2X rX eX e2X Y opY op2Y rY eY e2Y.
Let opX, op2X and rX be given.
Let opY' be given.
Assume HopY'.
Let op2Y' be given.
Assume Hop2Y'.
Let rY' be given.
Assume HrY'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply and6E (f YX) (∀x yX, f (opX x y) = opY' (f x) (f y)) (∀x yX, f (op2X x y) = op2Y' (f x) (f y)) (∀x yX, rX x yrY' (f x) (f y)) (f eX = eY) (f e2X = e2Y) H to the current goal.
Assume H1 H2 H3 H4 H5 H6.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))(∀x yX, rX x yrY (f x) (f y))f eX = eYf e2X = e2Y.
Apply and6I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopY' (f x) (Lf x Hx) (f y) (Lf y Hy) (from left to right).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2Y' (f x) (Lf x Hx) (f y) (Lf y Hy) (from left to right).
An exact proof term for the current goal is H3 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply iffER (rY (f x) (f y)) (rY' (f x) (f y)) (HrY' (f x) (Lf x Hx) (f y) (Lf y Hy)) to the current goal.
An exact proof term for the current goal is H4 x Hx y Hy H7.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
Assume H.
Apply and6E (f YX) (∀x yX, f (opX x y) = opY (f x) (f y)) (∀x yX, f (op2X x y) = op2Y (f x) (f y)) (∀x yX, rX x yrY (f x) (f y)) (f eX = eY) (f e2X = e2Y) H to the current goal.
Assume H1 H2 H3 H4 H5 H6.
We prove the intermediate claim Lf: ∀xX, f x Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will prove f YX(∀x yX, f (opX x y) = opY' (f x) (f y))(∀x yX, f (op2X x y) = op2Y' (f x) (f y))(∀x yX, rX x yrY' (f x) (f y))f eX = eYf e2X = e2Y.
Apply and6I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopY' (f x) (Lf x Hx) (f y) (Lf y Hy) (from right to left).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2Y' (f x) (Lf x Hx) (f y) (Lf y Hy) (from right to left).
An exact proof term for the current goal is H3 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply iffEL (rY (f x) (f y)) (rY' (f x) (f y)) (HrY' (f x) (Lf x Hx) (f y) (Lf y Hy)) to the current goal.
An exact proof term for the current goal is H4 x Hx y Hy H7.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
We prove the intermediate claim L2: ∀opX' : setsetset, (∀x yX, opX x y = opX' x y)∀op2X' : setsetset, (∀x yX, op2X x y = op2X' x y)∀rX' : setsetprop, (∀x yX, rX x yrX' x y)PhiX X opX' op2X' rX' eX e2X = PhiX X opX op2X rX eX e2X.
Let opX' be given.
Assume HopX'.
Let op2X' be given.
Assume Hop2X'.
Let rX' be given.
Assume HrX'.
We will prove PhiX X opX' op2X' rX' eX e2X = PhiX X opX op2X rX eX e2X.
We will prove unpack_b_b_r_e_e_o (pack_b_b_r_e_e Y opY op2Y rY eY e2Y) (λY' opY op2Y rY eY e2Y ⇒ Phi X opX' op2X' rX' eX e2X Y' opY op2Y rY eY e2Y) = unpack_b_b_r_e_e_o (pack_b_b_r_e_e Y opY op2Y rY eY e2Y) (λY' opY op2Y rY eY e2Y ⇒ Phi X opX op2X rX eX e2X Y' opY op2Y rY eY e2Y).
Use transitivity with Phi X opX' op2X' rX' eX e2X Y opY op2Y rY eY e2Y, and Phi X opX op2X rX eX e2X Y opY op2Y rY eY e2Y.
We will prove unpack_b_b_r_e_e_o (pack_b_b_r_e_e Y opY op2Y rY eY e2Y) (Phi X opX' op2X' rX' eX e2X) = Phi X opX' op2X' rX' eX e2X Y opY op2Y rY eY e2Y.
An exact proof term for the current goal is unpack_b_b_r_e_e_o_eq (Phi X opX' op2X' rX' eX e2X) Y opY op2Y rY eY e2Y (L1 opX' op2X' rX').
We will prove Phi X opX' op2X' rX' eX e2X Y opY op2Y rY eY e2Y = Phi X opX op2X rX eX e2X Y opY op2Y rY eY e2Y.
Apply prop_ext_2 to the current goal.
Assume H.
Apply and6E (f YX) (∀x yX, f (opX' x y) = opY (f x) (f y)) (∀x yX, f (op2X' x y) = op2Y (f x) (f y)) (∀x yX, rX' x yrY (f x) (f y)) (f eX = eY) (f e2X = e2Y) H to the current goal.
Assume H1 H2 H3 H4 H5 H6.
We will prove f YX(∀x yX, f (opX x y) = opY (f x) (f y))(∀x yX, f (op2X x y) = op2Y (f x) (f y))(∀x yX, rX x yrY (f x) (f y))f eX = eYf e2X = e2Y.
Apply and6I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopX' x Hx y Hy (from left to right).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2X' x Hx y Hy (from left to right).
An exact proof term for the current goal is H3 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply H4 x Hx y Hy to the current goal.
Apply iffEL (rX x y) (rX' x y) (HrX' x Hx y Hy) to the current goal.
An exact proof term for the current goal is H7.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
Assume H.
Apply and6E (f YX) (∀x yX, f (opX x y) = opY (f x) (f y)) (∀x yX, f (op2X x y) = op2Y (f x) (f y)) (∀x yX, rX x yrY (f x) (f y)) (f eX = eY) (f e2X = e2Y) H to the current goal.
Assume H1 H2 H3 H4 H5 H6.
We will prove f YX(∀x yX, f (opX' x y) = opY (f x) (f y))(∀x yX, f (op2X' x y) = op2Y (f x) (f y))(∀x yX, rX' x yrY (f x) (f y))f eX = eYf e2X = e2Y.
Apply and6I to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using HopX' x Hx y Hy (from right to left).
An exact proof term for the current goal is H2 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using Hop2X' x Hx y Hy (from right to left).
An exact proof term for the current goal is H3 x Hx y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply H4 x Hx y Hy to the current goal.
Apply iffER (rX x y) (rX' x y) (HrX' x Hx y Hy) to the current goal.
An exact proof term for the current goal is H7.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
Use symmetry.
An exact proof term for the current goal is unpack_b_b_r_e_e_o_eq (Phi X opX op2X rX eX e2X) Y opY op2Y rY eY e2Y (L1 opX op2X rX).
Use transitivity with and PhiX X opX op2X rX eX e2X.
An exact proof term for the current goal is unpack_b_b_r_e_e_o_eq PhiX X opX op2X rX eX e2X L2.
We will prove unpack_b_b_r_e_e_o (pack_b_b_r_e_e Y opY op2Y rY eY e2Y) (Phi X opX op2X rX eX e2X) = Phi X opX op2X rX eX e2X Y opY op2Y rY eY e2Y.
An exact proof term for the current goal is unpack_b_b_r_e_e_o_eq (Phi X opX op2X rX eX e2X) Y opY op2Y rY eY e2Y (L1 opX op2X rX).
Beginning of Section MetaCatStruct
Variable Obj : setprop
Theorem. (MetaCat_struct_e_gen)
(∀X, Obj Xstruct_e X)MetaCat Obj Hom_struct_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_e to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_e u Y ff Y 0u 0) to the current goal.
Let X' and eX be given.
Assume HeX.
Apply HO Y HY (λu ⇒ Hom_struct_e (pack_e X' eX) u ff u 0pack_e X' eX 0) to the current goal.
Let Y' and eY be given.
Assume HeY.
We will prove Hom_struct_e (pack_e X' eX) (pack_e Y' eY) ff pack_e Y' eY 0pack_e X' eX 0.
rewrite the current goal using Hom_struct_e_pack (from left to right).
Assume Hf: f Y'X'f eX = eY.
Apply Hf to the current goal.
Assume Hf1 Hf2.
rewrite the current goal using pack_e_0_eq2 (from right to left).
rewrite the current goal using pack_e_0_eq2 (from right to left).
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_e u u (lam_id (u 0))) to the current goal.
Let X' and eX be given.
Assume HeX.
We will prove Hom_struct_e (pack_e X' eX) (pack_e X' eX) (lam_id (pack_e X' eX 0)).
rewrite the current goal using pack_e_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_e_pack (from left to right).
We will prove lam_id X' X'X'lam_id X' eX = eX.
Apply andI to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
We will prove (λx ∈ X'x) eX = eX.
An exact proof term for the current goal is beta X' (λx ⇒ x) eX HeX.
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_e u Y fHom_struct_e Y Z gHom_struct_e u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and eX be given.
Assume HeX.
We will prove Hom_struct_e (pack_e X' eX) Y fHom_struct_e Y Z gHom_struct_e (pack_e X' eX) Z (lam_comp (pack_e X' eX 0) g f).
rewrite the current goal using pack_e_0_eq2 (from right to left).
We will prove Hom_struct_e (pack_e X' eX) Y fHom_struct_e Y Z gHom_struct_e (pack_e X' eX) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_e (pack_e X' eX) u fHom_struct_e u Z gHom_struct_e (pack_e X' eX) Z (lam_comp X' g f)) to the current goal.
Let Y' and eY be given.
Assume HeY.
We will prove Hom_struct_e (pack_e X' eX) (pack_e Y' eY) fHom_struct_e (pack_e Y' eY) Z gHom_struct_e (pack_e X' eX) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_e_pack (from left to right).
Assume Hf: f Y'X'f eX = eY.
Apply HO Z HZ (λu ⇒ Hom_struct_e (pack_e Y' eY) u gHom_struct_e (pack_e X' eX) u (lam_comp X' g f)) to the current goal.
Let Z' and eZ be given.
Assume HeZ.
We will prove Hom_struct_e (pack_e Y' eY) (pack_e Z' eZ) gHom_struct_e (pack_e X' eX) (pack_e Z' eZ) (lam_comp X' g f).
rewrite the current goal using Hom_struct_e_pack (from left to right).
rewrite the current goal using Hom_struct_e_pack (from left to right).
Assume Hg: g Z'Y'g eY = eZ.
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply Hg to the current goal.
Assume Hg1 Hg2.
We will prove lam_comp X' g f Z'X'lam_comp X' g f eX = eZ.
Apply andI to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
We will prove (λx ∈ X'g (f x)) eX = eZ.
rewrite the current goal using beta X' (λx ⇒ g (f x)) eX HeX (from left to right).
We will prove g (f eX) = eZ.
rewrite the current goal using Hf2 (from left to right).
An exact proof term for the current goal is Hg2.
Theorem. (MetaCat_struct_e_Forgetful_gen)
(∀X, Obj Xstruct_e X)MetaFunctor Obj Hom_struct_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_e X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_e u Y ff Y 0u 0) to the current goal.
Let X' and eX be given.
Assume HeX.
Apply HO Y HY (λu ⇒ Hom_struct_e (pack_e X' eX) u ff u 0pack_e X' eX 0) to the current goal.
Let Y' and eY be given.
Assume HeY.
We will prove Hom_struct_e (pack_e X' eX) (pack_e Y' eY) ff pack_e Y' eY 0pack_e X' eX 0.
rewrite the current goal using Hom_struct_e_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_e_0_eq2 (from right to left).
rewrite the current goal using pack_e_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_e L1.
Theorem. (MetaCat_struct_p_gen)
(∀X, Obj Xstruct_p X)MetaCat Obj Hom_struct_p (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_p to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_p u Y ff Y 0u 0) to the current goal.
Let X' and pX be given.
Apply HO Y HY (λu ⇒ Hom_struct_p (pack_p X' pX) u ff u 0pack_p X' pX 0) to the current goal.
Let Y' and pY be given.
We will prove Hom_struct_p (pack_p X' pX) (pack_p Y' pY) ff pack_p Y' pY 0pack_p X' pX 0.
rewrite the current goal using Hom_struct_p_pack (from left to right).
Assume Hf: f Y'X'(∀xX', pX xpY (f x)).
Apply Hf to the current goal.
Assume Hf1 Hf2.
rewrite the current goal using pack_p_0_eq2 (from right to left).
rewrite the current goal using pack_p_0_eq2 (from right to left).
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_p u u (lam_id (u 0))) to the current goal.
Let X' and pX be given.
We will prove Hom_struct_p (pack_p X' pX) (pack_p X' pX) (lam_id (pack_p X' pX 0)).
rewrite the current goal using pack_p_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_p_pack (from left to right).
We will prove lam_id X' X'X'(∀xX', pX xpX (lam_id X' x)).
Apply andI to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
Let x be given.
Assume Hx Hx2.
We will prove pX ((λx ∈ X'x) x).
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
An exact proof term for the current goal is Hx2.
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_p u Y fHom_struct_p Y Z gHom_struct_p u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and pX be given.
We will prove Hom_struct_p (pack_p X' pX) Y fHom_struct_p Y Z gHom_struct_p (pack_p X' pX) Z (lam_comp (pack_p X' pX 0) g f).
rewrite the current goal using pack_p_0_eq2 (from right to left).
We will prove Hom_struct_p (pack_p X' pX) Y fHom_struct_p Y Z gHom_struct_p (pack_p X' pX) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_p (pack_p X' pX) u fHom_struct_p u Z gHom_struct_p (pack_p X' pX) Z (lam_comp X' g f)) to the current goal.
Let Y' and pY be given.
We will prove Hom_struct_p (pack_p X' pX) (pack_p Y' pY) fHom_struct_p (pack_p Y' pY) Z gHom_struct_p (pack_p X' pX) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_p_pack (from left to right).
Assume Hf: f Y'X'(∀xX', pX xpY (f x)).
Apply HO Z HZ (λu ⇒ Hom_struct_p (pack_p Y' pY) u gHom_struct_p (pack_p X' pX) u (lam_comp X' g f)) to the current goal.
Let Z' and pZ be given.
We will prove Hom_struct_p (pack_p Y' pY) (pack_p Z' pZ) gHom_struct_p (pack_p X' pX) (pack_p Z' pZ) (lam_comp X' g f).
rewrite the current goal using Hom_struct_p_pack (from left to right).
rewrite the current goal using Hom_struct_p_pack (from left to right).
Assume Hg: g Z'Y'(∀yY', pY ypZ (g y)).
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply Hg to the current goal.
Assume Hg1 Hg2.
We will prove lam_comp X' g f Z'X'(∀xX', pX xpZ (lam_comp X' g f x)).
Apply andI to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
Let x be given.
Assume Hx Hx2.
We will prove pZ ((λx ∈ X'g (f x)) x).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
We will prove pZ (g (f x)).
Apply Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) to the current goal.
Apply Hf2 x Hx to the current goal.
An exact proof term for the current goal is Hx2.
Theorem. (MetaCat_struct_p_Forgetful_gen)
(∀X, Obj Xstruct_p X)MetaFunctor Obj Hom_struct_p (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_p X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_p u Y ff Y 0u 0) to the current goal.
Let X' and pX be given.
Apply HO Y HY (λu ⇒ Hom_struct_p (pack_p X' pX) u ff u 0pack_p X' pX 0) to the current goal.
Let Y' and pY be given.
We will prove Hom_struct_p (pack_p X' pX) (pack_p Y' pY) ff pack_p Y' pY 0pack_p X' pX 0.
rewrite the current goal using Hom_struct_p_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_p_0_eq2 (from right to left).
rewrite the current goal using pack_p_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_p L1.
Theorem. (MetaCat_struct_r_gen)
(∀X, Obj Xstruct_r X)MetaCat Obj Hom_struct_r (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_r to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_r u Y ff Y 0u 0) to the current goal.
Let X' and rX be given.
Apply HO Y HY (λu ⇒ Hom_struct_r (pack_r X' rX) u ff u 0pack_r X' rX 0) to the current goal.
Let Y' and rY be given.
We will prove Hom_struct_r (pack_r X' rX) (pack_r Y' rY) ff pack_r Y' rY 0pack_r X' rX 0.
rewrite the current goal using Hom_struct_r_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', rX x x'rY (f x) (f x')).
Apply Hf to the current goal.
Assume Hf1 Hf2.
rewrite the current goal using pack_r_0_eq2 (from right to left).
rewrite the current goal using pack_r_0_eq2 (from right to left).
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_r u u (lam_id (u 0))) to the current goal.
Let X' and rX be given.
We will prove Hom_struct_r (pack_r X' rX) (pack_r X' rX) (lam_id (pack_r X' rX 0)).
rewrite the current goal using pack_r_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_r_pack (from left to right).
We will prove lam_id X' X'X'(∀x x'X', rX x x'rX (lam_id X' x) (lam_id X' x')).
Apply andI to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx' Hx2.
We will prove rX ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is Hx2.
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_r u Y fHom_struct_r Y Z gHom_struct_r u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and rX be given.
We will prove Hom_struct_r (pack_r X' rX) Y fHom_struct_r Y Z gHom_struct_r (pack_r X' rX) Z (lam_comp (pack_r X' rX 0) g f).
rewrite the current goal using pack_r_0_eq2 (from right to left).
We will prove Hom_struct_r (pack_r X' rX) Y fHom_struct_r Y Z gHom_struct_r (pack_r X' rX) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_r (pack_r X' rX) u fHom_struct_r u Z gHom_struct_r (pack_r X' rX) Z (lam_comp X' g f)) to the current goal.
Let Y' and rY be given.
We will prove Hom_struct_r (pack_r X' rX) (pack_r Y' rY) fHom_struct_r (pack_r Y' rY) Z gHom_struct_r (pack_r X' rX) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_r_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', rX x x'rY (f x) (f x')).
Apply HO Z HZ (λu ⇒ Hom_struct_r (pack_r Y' rY) u gHom_struct_r (pack_r X' rX) u (lam_comp X' g f)) to the current goal.
Let Z' and rZ be given.
We will prove Hom_struct_r (pack_r Y' rY) (pack_r Z' rZ) gHom_struct_r (pack_r X' rX) (pack_r Z' rZ) (lam_comp X' g f).
rewrite the current goal using Hom_struct_r_pack (from left to right).
rewrite the current goal using Hom_struct_r_pack (from left to right).
Assume Hg: g Z'Y'(∀y y'Y', rY y y'rZ (g y) (g y')).
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply Hg to the current goal.
Assume Hg1 Hg2.
We will prove lam_comp X' g f Z'X'(∀x x'X', rX x x'rZ (lam_comp X' g f x) (lam_comp X' g f x')).
Apply andI to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx' Hx2.
We will prove rZ ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove rZ (g (f x)) (g (f x')).
Apply Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') to the current goal.
Apply Hf2 x Hx x' Hx' to the current goal.
An exact proof term for the current goal is Hx2.
Theorem. (MetaCat_struct_r_Forgetful_gen)
(∀X, Obj Xstruct_r X)MetaFunctor Obj Hom_struct_r (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_r X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_r u Y ff Y 0u 0) to the current goal.
Let X' and rX be given.
Apply HO Y HY (λu ⇒ Hom_struct_r (pack_r X' rX) u ff u 0pack_r X' rX 0) to the current goal.
Let Y' and rY be given.
We will prove Hom_struct_r (pack_r X' rX) (pack_r Y' rY) ff pack_r Y' rY 0pack_r X' rX 0.
rewrite the current goal using Hom_struct_r_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_r_0_eq2 (from right to left).
rewrite the current goal using pack_r_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_r L1.
Theorem. (MetaCat_struct_u_gen)
(∀X, Obj Xstruct_u X)MetaCat Obj Hom_struct_u (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_u to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_u u Y ff Y 0u 0) to the current goal.
Let X' and uX be given.
Assume HuX.
Apply HO Y HY (λu ⇒ Hom_struct_u (pack_u X' uX) u ff u 0pack_u X' uX 0) to the current goal.
Let Y' and uY be given.
Assume HuY.
We will prove Hom_struct_u (pack_u X' uX) (pack_u Y' uY) ff pack_u Y' uY 0pack_u X' uX 0.
rewrite the current goal using Hom_struct_u_pack (from left to right).
Assume Hf: f Y'X'(∀xX', f (uX x) = uY (f x)).
Apply Hf to the current goal.
Assume Hf1 Hf2.
rewrite the current goal using pack_u_0_eq2 (from right to left).
rewrite the current goal using pack_u_0_eq2 (from right to left).
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_u u u (lam_id (u 0))) to the current goal.
Let X' and uX be given.
Assume HuX.
We will prove Hom_struct_u (pack_u X' uX) (pack_u X' uX) (lam_id (pack_u X' uX 0)).
rewrite the current goal using pack_u_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_u_pack (from left to right).
We will prove lam_id X' X'X'(∀xX', lam_id X' (uX x) = uX (lam_id X' x)).
Apply andI to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
Let x be given.
Assume Hx.
We will prove lam_id X' (uX x) = uX ((λx ∈ X'x) x).
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
An exact proof term for the current goal is beta X' (λx ⇒ x) (uX x) (HuX x Hx).
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_u u Y fHom_struct_u Y Z gHom_struct_u u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and uX be given.
Assume HuX.
We will prove Hom_struct_u (pack_u X' uX) Y fHom_struct_u Y Z gHom_struct_u (pack_u X' uX) Z (lam_comp (pack_u X' uX 0) g f).
rewrite the current goal using pack_u_0_eq2 (from right to left).
We will prove Hom_struct_u (pack_u X' uX) Y fHom_struct_u Y Z gHom_struct_u (pack_u X' uX) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_u (pack_u X' uX) u fHom_struct_u u Z gHom_struct_u (pack_u X' uX) Z (lam_comp X' g f)) to the current goal.
Let Y' and uY be given.
Assume HuY.
We will prove Hom_struct_u (pack_u X' uX) (pack_u Y' uY) fHom_struct_u (pack_u Y' uY) Z gHom_struct_u (pack_u X' uX) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_u_pack (from left to right).
Assume Hf: f Y'X'(∀xX', f (uX x) = uY (f x)).
Apply HO Z HZ (λu ⇒ Hom_struct_u (pack_u Y' uY) u gHom_struct_u (pack_u X' uX) u (lam_comp X' g f)) to the current goal.
Let Z' and uZ be given.
Assume HuZ.
We will prove Hom_struct_u (pack_u Y' uY) (pack_u Z' uZ) gHom_struct_u (pack_u X' uX) (pack_u Z' uZ) (lam_comp X' g f).
rewrite the current goal using Hom_struct_u_pack (from left to right).
rewrite the current goal using Hom_struct_u_pack (from left to right).
Assume Hg: g Z'Y'(∀yY', g (uY y) = uZ (g y)).
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply Hg to the current goal.
Assume Hg1 Hg2.
We will prove lam_comp X' g f Z'X'(∀xX', lam_comp X' g f (uX x) = uZ (lam_comp X' g f x)).
Apply andI to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
Let x be given.
Assume Hx.
We will prove lam_comp X' g f (uX x) = uZ ((λx ∈ X'g (f x)) x).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
We will prove (λx ∈ X'g (f x)) (uX x) = uZ (g (f x)).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (uX x) (HuX x Hx) (from left to right).
We will prove g (f (uX x)) = uZ (g (f x)).
rewrite the current goal using Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (from right to left).
We will prove g (f (uX x)) = g (uY (f x)).
Use f_equal.
An exact proof term for the current goal is Hf2 x Hx.
Theorem. (MetaCat_struct_u_Forgetful_gen)
(∀X, Obj Xstruct_u X)MetaFunctor Obj Hom_struct_u (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_u X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_u u Y ff Y 0u 0) to the current goal.
Let X' and uX be given.
Assume HuX.
Apply HO Y HY (λu ⇒ Hom_struct_u (pack_u X' uX) u ff u 0pack_u X' uX 0) to the current goal.
Let Y' and uY be given.
Assume HuY.
We will prove Hom_struct_u (pack_u X' uX) (pack_u Y' uY) ff pack_u Y' uY 0pack_u X' uX 0.
rewrite the current goal using Hom_struct_u_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_u_0_eq2 (from right to left).
rewrite the current goal using pack_u_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_u L1.
Theorem. (MetaCat_struct_b_gen)
(∀X, Obj Xstruct_b X)MetaCat Obj Hom_struct_b (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_b to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_b u Y ff Y 0u 0) to the current goal.
Let X' and bX be given.
Assume HbX.
Apply HO Y HY (λu ⇒ Hom_struct_b (pack_b X' bX) u ff u 0pack_b X' bX 0) to the current goal.
Let Y' and bY be given.
Assume HbY.
We will prove Hom_struct_b (pack_b X' bX) (pack_b Y' bY) ff pack_b Y' bY 0pack_b X' bX 0.
rewrite the current goal using Hom_struct_b_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', f (bX x x') = bY (f x) (f x')).
Apply Hf to the current goal.
Assume Hf1 Hf2.
rewrite the current goal using pack_b_0_eq2 (from right to left).
rewrite the current goal using pack_b_0_eq2 (from right to left).
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_b u u (lam_id (u 0))) to the current goal.
Let X' and bX be given.
Assume HbX.
We will prove Hom_struct_b (pack_b X' bX) (pack_b X' bX) (lam_id (pack_b X' bX 0)).
rewrite the current goal using pack_b_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_b_pack (from left to right).
We will prove lam_id X' X'X'(∀x x'X', lam_id X' (bX x x') = bX (lam_id X' x) (lam_id X' x')).
Apply andI to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_id X' (bX x x') = bX ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is beta X' (λx ⇒ x) (bX x x') (HbX x Hx x' Hx').
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_b u Y fHom_struct_b Y Z gHom_struct_b u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and bX be given.
Assume HbX.
We will prove Hom_struct_b (pack_b X' bX) Y fHom_struct_b Y Z gHom_struct_b (pack_b X' bX) Z (lam_comp (pack_b X' bX 0) g f).
rewrite the current goal using pack_b_0_eq2 (from right to left).
We will prove Hom_struct_b (pack_b X' bX) Y fHom_struct_b Y Z gHom_struct_b (pack_b X' bX) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_b (pack_b X' bX) u fHom_struct_b u Z gHom_struct_b (pack_b X' bX) Z (lam_comp X' g f)) to the current goal.
Let Y' and bY be given.
Assume HbY.
We will prove Hom_struct_b (pack_b X' bX) (pack_b Y' bY) fHom_struct_b (pack_b Y' bY) Z gHom_struct_b (pack_b X' bX) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_b_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', f (bX x x') = bY (f x) (f x')).
Apply HO Z HZ (λu ⇒ Hom_struct_b (pack_b Y' bY) u gHom_struct_b (pack_b X' bX) u (lam_comp X' g f)) to the current goal.
Let Z' and bZ be given.
Assume HbZ.
We will prove Hom_struct_b (pack_b Y' bY) (pack_b Z' bZ) gHom_struct_b (pack_b X' bX) (pack_b Z' bZ) (lam_comp X' g f).
rewrite the current goal using Hom_struct_b_pack (from left to right).
rewrite the current goal using Hom_struct_b_pack (from left to right).
Assume Hg: g Z'Y'(∀y y'Y', g (bY y y') = bZ (g y) (g y')).
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply Hg to the current goal.
Assume Hg1 Hg2.
We will prove lam_comp X' g f Z'X'(∀x x'X', lam_comp X' g f (bX x x') = bZ (lam_comp X' g f x) (lam_comp X' g f x')).
Apply andI to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_comp X' g f (bX x x') = bZ ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove (λx ∈ X'g (f x)) (bX x x') = bZ (g (f x)) (g (f x')).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (bX x x') (HbX x Hx x' Hx') (from left to right).
We will prove g (f (bX x x')) = bZ (g (f x)) (g (f x')).
rewrite the current goal using Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') (from right to left).
We will prove g (f (bX x x')) = g (bY (f x) (f x')).
Use f_equal.
An exact proof term for the current goal is Hf2 x Hx x' Hx'.
Theorem. (MetaCat_struct_b_Forgetful_gen)
(∀X, Obj Xstruct_b X)MetaFunctor Obj Hom_struct_b (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_b X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_b u Y ff Y 0u 0) to the current goal.
Let X' and bX be given.
Assume HbX.
Apply HO Y HY (λu ⇒ Hom_struct_b (pack_b X' bX) u ff u 0pack_b X' bX 0) to the current goal.
Let Y' and bY be given.
Assume HbY.
We will prove Hom_struct_b (pack_b X' bX) (pack_b Y' bY) ff pack_b Y' bY 0pack_b X' bX 0.
rewrite the current goal using Hom_struct_b_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_b_0_eq2 (from right to left).
rewrite the current goal using pack_b_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_b L1.
Theorem. (MetaCat_struct_c_gen)
(∀X, Obj Xstruct_c X)MetaCat Obj Hom_struct_c (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_c to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_c u Y ff Y 0u 0) to the current goal.
Let X' and CX be given.
Apply HO Y HY (λu ⇒ Hom_struct_c (pack_c X' CX) u ff u 0pack_c X' CX 0) to the current goal.
Let Y' and CY be given.
We will prove Hom_struct_c (pack_c X' CX) (pack_c Y' CY) ff pack_c Y' CY 0pack_c X' CX 0.
rewrite the current goal using Hom_struct_c_pack (from left to right).
Assume Hf: f Y'X'(∀U : setprop, (∀y, U yy Y')CY UCX (λx ⇒ x X'U (f x))).
Apply Hf to the current goal.
Assume Hf1 Hf2.
rewrite the current goal using pack_c_0_eq2 (from right to left).
rewrite the current goal using pack_c_0_eq2 (from right to left).
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_c u u (lam_id (u 0))) to the current goal.
Let X' and CX be given.
We will prove Hom_struct_c (pack_c X' CX) (pack_c X' CX) (lam_id (pack_c X' CX 0)).
rewrite the current goal using pack_c_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_c_pack (from left to right).
We will prove lam_id X' X'X'(∀U : setprop, (∀y, U yy X')CX UCX (λx ⇒ x X'U (lam_id X' x))).
Apply andI to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
Let U be given.
Assume HU1 HU2.
We prove the intermediate claim L1: U = (λx ⇒ x X'U (lam_id X' x)).
Apply pred_ext_2 to the current goal.
Let x be given.
Assume Hx.
We will prove x X'U (lam_id X' x).
Apply andI to the current goal.
An exact proof term for the current goal is HU1 x Hx.
We will prove U ((λx ∈ X'x) x).
rewrite the current goal using beta X' (λx ⇒ x) x (HU1 x Hx) (from left to right).
An exact proof term for the current goal is Hx.
Let x be given.
Assume Hx.
Apply Hx to the current goal.
Assume Hx1.
We will prove U ((λx ∈ X'x) x)U x.
rewrite the current goal using beta X' (λx ⇒ x) x Hx1 (from left to right).
Assume Hx2.
An exact proof term for the current goal is Hx2.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is HU2.
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_c u Y fHom_struct_c Y Z gHom_struct_c u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and CX be given.
We will prove Hom_struct_c (pack_c X' CX) Y fHom_struct_c Y Z gHom_struct_c (pack_c X' CX) Z (lam_comp (pack_c X' CX 0) g f).
rewrite the current goal using pack_c_0_eq2 (from right to left).
We will prove Hom_struct_c (pack_c X' CX) Y fHom_struct_c Y Z gHom_struct_c (pack_c X' CX) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_c (pack_c X' CX) u fHom_struct_c u Z gHom_struct_c (pack_c X' CX) Z (lam_comp X' g f)) to the current goal.
Let Y' and CY be given.
We will prove Hom_struct_c (pack_c X' CX) (pack_c Y' CY) fHom_struct_c (pack_c Y' CY) Z gHom_struct_c (pack_c X' CX) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_c_pack (from left to right).
Assume Hf: f Y'X'(∀U : setprop, (∀y, U yy Y')CY UCX (λx ⇒ x X'U (f x))).
Apply HO Z HZ (λu ⇒ Hom_struct_c (pack_c Y' CY) u gHom_struct_c (pack_c X' CX) u (lam_comp X' g f)) to the current goal.
Let Z' and CZ be given.
We will prove Hom_struct_c (pack_c Y' CY) (pack_c Z' CZ) gHom_struct_c (pack_c X' CX) (pack_c Z' CZ) (lam_comp X' g f).
rewrite the current goal using Hom_struct_c_pack (from left to right).
rewrite the current goal using Hom_struct_c_pack (from left to right).
Assume Hg: g Z'Y'(∀U : setprop, (∀z, U zz Z')CZ UCY (λy ⇒ y Y'U (g y))).
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply Hg to the current goal.
Assume Hg1 Hg2.
We will prove lam_comp X' g f Z'X'(∀U : setprop, (∀z, U zz Z')CZ UCX (λx ⇒ x X'U (lam_comp X' g f x))).
Apply andI to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
Let U be given.
Assume HU1: ∀z, U zz Z'.
Assume HU2: CZ U.
We prove the intermediate claim L2: CY (λy ⇒ y Y'U (g y)).
An exact proof term for the current goal is Hg2 U HU1 HU2.
We prove the intermediate claim L3: ∀y, y Y'U (g y)y Y'.
Let y be given.
An exact proof term for the current goal is andEL (y Y') (U (g y)).
We prove the intermediate claim L4: CX (λx ⇒ x X'(f x Y'U (g (f x)))).
An exact proof term for the current goal is Hf2 (λy ⇒ y Y'U (g y)) L3 L2.
We prove the intermediate claim L5: (λx : setx X'(f x Y'U (g (f x)))) = (λx : setx X'U (lam_comp X' g f x)).
Apply pred_ext_2 to the current goal.
Let x be given.
Assume Hx.
Apply Hx to the current goal.
Assume Hx1 Hx23.
Apply Hx23 to the current goal.
Assume Hx2 Hx3.
We will prove x X'U (lam_comp X' g f x).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove U ((λx ∈ X'g (f x)) x).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx1 (from left to right).
An exact proof term for the current goal is Hx3.
Let x be given.
Assume Hx.
Apply Hx to the current goal.
Assume Hx1.
We will prove U ((λx ∈ X'g (f x)) x)x X'(f x Y'U (g (f x))).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx1 (from left to right).
Assume Hx2.
We will prove x X'(f x Y'U (g (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
Apply andI to the current goal.
An exact proof term for the current goal is ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx1.
An exact proof term for the current goal is Hx2.
rewrite the current goal using L5 (from right to left).
An exact proof term for the current goal is L4.
Theorem. (MetaCat_struct_c_Forgetful_gen)
(∀X, Obj Xstruct_c X)MetaFunctor Obj Hom_struct_c (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_c X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_c u Y ff Y 0u 0) to the current goal.
Let X' and CX be given.
Apply HO Y HY (λu ⇒ Hom_struct_c (pack_c X' CX) u ff u 0pack_c X' CX 0) to the current goal.
Let Y' and CY be given.
We will prove Hom_struct_c (pack_c X' CX) (pack_c Y' CY) ff pack_c Y' CY 0pack_c X' CX 0.
rewrite the current goal using Hom_struct_c_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_c_0_eq2 (from right to left).
rewrite the current goal using pack_c_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_c L1.
Theorem. (MetaCat_struct_b_b_e_gen)
(∀X, Obj Xstruct_b_b_e X)MetaCat Obj Hom_struct_b_b_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_b_b_e to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_b_b_e u Y ff Y 0u 0) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let eX be given.
Assume HeX.
Apply HO Y HY (λu ⇒ Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) u ff u 0pack_b_b_e X' bX b2X eX 0) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let eY be given.
Assume HeY.
We will prove Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) (pack_b_b_e Y' bY b2Y eY) ff pack_b_b_e Y' bY b2Y eY 0pack_b_b_e X' bX b2X eX 0.
rewrite the current goal using Hom_struct_b_b_e_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', f (bX x x') = bY (f x) (f x'))(∀x x'X', f (b2X x x') = b2Y (f x) (f x'))f eX = eY.
Apply and4E (f Y'X') (∀x x'X', f (bX x x') = bY (f x) (f x')) (∀x x'X', f (b2X x x') = b2Y (f x) (f x')) (f eX = eY) Hf to the current goal.
Assume Hf1: f Y'X'.
Assume Hf2: ∀x x'X', f (bX x x') = bY (f x) (f x').
Assume Hf3: ∀x x'X', f (b2X x x') = b2Y (f x) (f x').
Assume Hf4: f eX = eY.
We will prove f pack_b_b_e Y' bY b2Y eY 0pack_b_b_e X' bX b2X eX 0.
rewrite the current goal using pack_b_b_e_0_eq2 (from right to left).
rewrite the current goal using pack_b_b_e_0_eq2 (from right to left).
We will prove f Y'X'.
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_b_b_e u u (lam_id (u 0))) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let eX be given.
Assume HeX.
We will prove Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) (pack_b_b_e X' bX b2X eX) (lam_id (pack_b_b_e X' bX b2X eX 0)).
rewrite the current goal using pack_b_b_e_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_b_b_e_pack (from left to right).
We will prove lam_id X' X'X'(∀x x'X', lam_id X' (bX x x') = bX (lam_id X' x) (lam_id X' x'))(∀x x'X', lam_id X' (b2X x x') = b2X (lam_id X' x) (lam_id X' x'))lam_id X' eX = eX.
Apply and4I to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_id X' (bX x x') = bX ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is beta X' (λx ⇒ x) (bX x x') (HbX x Hx x' Hx').
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_id X' (b2X x x') = b2X ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is beta X' (λx ⇒ x) (b2X x x') (Hb2X x Hx x' Hx').
We will prove (λx ∈ X'x) eX = eX.
An exact proof term for the current goal is beta X' (λx ⇒ x) eX HeX.
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_b_b_e u Y fHom_struct_b_b_e Y Z gHom_struct_b_b_e u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let eX be given.
Assume HeX.
We will prove Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) Y fHom_struct_b_b_e Y Z gHom_struct_b_b_e (pack_b_b_e X' bX b2X eX) Z (lam_comp (pack_b_b_e X' bX b2X eX 0) g f).
rewrite the current goal using pack_b_b_e_0_eq2 (from right to left).
We will prove Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) Y fHom_struct_b_b_e Y Z gHom_struct_b_b_e (pack_b_b_e X' bX b2X eX) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) u fHom_struct_b_b_e u Z gHom_struct_b_b_e (pack_b_b_e X' bX b2X eX) Z (lam_comp X' g f)) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let eY be given.
Assume HeY.
We will prove Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) (pack_b_b_e Y' bY b2Y eY) fHom_struct_b_b_e (pack_b_b_e Y' bY b2Y eY) Z gHom_struct_b_b_e (pack_b_b_e X' bX b2X eX) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_b_b_e_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', f (bX x x') = bY (f x) (f x'))(∀x x'X', f (b2X x x') = b2Y (f x) (f x'))f eX = eY.
Apply HO Z HZ (λu ⇒ Hom_struct_b_b_e (pack_b_b_e Y' bY b2Y eY) u gHom_struct_b_b_e (pack_b_b_e X' bX b2X eX) u (lam_comp X' g f)) to the current goal.
Let Z' and bZ be given.
Assume HbZ.
Let b2Z be given.
Assume Hb2Z.
Let eZ be given.
Assume HeZ.
We will prove Hom_struct_b_b_e (pack_b_b_e Y' bY b2Y eY) (pack_b_b_e Z' bZ b2Z eZ) gHom_struct_b_b_e (pack_b_b_e X' bX b2X eX) (pack_b_b_e Z' bZ b2Z eZ) (lam_comp X' g f).
rewrite the current goal using Hom_struct_b_b_e_pack (from left to right).
rewrite the current goal using Hom_struct_b_b_e_pack (from left to right).
Assume Hg: g Z'Y'(∀y y'Y', g (bY y y') = bZ (g y) (g y'))(∀y y'Y', g (b2Y y y') = b2Z (g y) (g y'))g eY = eZ.
Apply and4E (f Y'X') (∀x x'X', f (bX x x') = bY (f x) (f x')) (∀x x'X', f (b2X x x') = b2Y (f x) (f x')) (f eX = eY) Hf to the current goal.
Assume Hf1: f Y'X'.
Assume Hf2: ∀x x'X', f (bX x x') = bY (f x) (f x').
Assume Hf3: ∀x x'X', f (b2X x x') = b2Y (f x) (f x').
Assume Hf4: f eX = eY.
Apply and4E (g Z'Y') (∀y y'Y', g (bY y y') = bZ (g y) (g y')) (∀y y'Y', g (b2Y y y') = b2Z (g y) (g y')) (g eY = eZ) Hg to the current goal.
Assume Hg1: g Z'Y'.
Assume Hg2: ∀y y'Y', g (bY y y') = bZ (g y) (g y').
Assume Hg3: ∀y y'Y', g (b2Y y y') = b2Z (g y) (g y').
Assume Hg4: g eY = eZ.
We will prove lam_comp X' g f Z'X'(∀x x'X', lam_comp X' g f (bX x x') = bZ (lam_comp X' g f x) (lam_comp X' g f x'))(∀x x'X', lam_comp X' g f (b2X x x') = b2Z (lam_comp X' g f x) (lam_comp X' g f x'))lam_comp X' g f eX = eZ.
Apply and4I to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_comp X' g f (bX x x') = bZ ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove (λx ∈ X'g (f x)) (bX x x') = bZ (g (f x)) (g (f x')).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (bX x x') (HbX x Hx x' Hx') (from left to right).
We will prove g (f (bX x x')) = bZ (g (f x)) (g (f x')).
rewrite the current goal using Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') (from right to left).
We will prove g (f (bX x x')) = g (bY (f x) (f x')).
Use f_equal.
An exact proof term for the current goal is Hf2 x Hx x' Hx'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_comp X' g f (b2X x x') = b2Z ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove (λx ∈ X'g (f x)) (b2X x x') = b2Z (g (f x)) (g (f x')).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (b2X x x') (Hb2X x Hx x' Hx') (from left to right).
We will prove g (f (b2X x x')) = b2Z (g (f x)) (g (f x')).
rewrite the current goal using Hg3 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') (from right to left).
We will prove g (f (b2X x x')) = g (b2Y (f x) (f x')).
Use f_equal.
An exact proof term for the current goal is Hf3 x Hx x' Hx'.
We will prove (λx ∈ X'g (f x)) eX = eZ.
rewrite the current goal using beta X' (λx ⇒ g (f x)) eX HeX (from left to right).
We will prove g (f eX) = eZ.
rewrite the current goal using Hf4 (from left to right).
An exact proof term for the current goal is Hg4.
Theorem. (MetaCat_struct_b_b_e_Forgetful_gen)
(∀X, Obj Xstruct_b_b_e X)MetaFunctor Obj Hom_struct_b_b_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_b_b_e X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_b_b_e u Y ff Y 0u 0) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let eX be given.
Assume HeX.
Apply HO Y HY (λu ⇒ Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) u ff u 0pack_b_b_e X' bX b2X eX 0) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let eY be given.
Assume HeY.
We will prove Hom_struct_b_b_e (pack_b_b_e X' bX b2X eX) (pack_b_b_e Y' bY b2Y eY) ff pack_b_b_e Y' bY b2Y eY 0pack_b_b_e X' bX b2X eX 0.
rewrite the current goal using Hom_struct_b_b_e_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_b_b_e_0_eq2 (from right to left).
rewrite the current goal using pack_b_b_e_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_b_b_e L1.
Theorem. (MetaCat_struct_b_b_e_e_gen)
(∀X, Obj Xstruct_b_b_e_e X)MetaCat Obj Hom_struct_b_b_e_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_b_b_e_e to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_b_b_e_e u Y ff Y 0u 0) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let eX be given.
Assume HeX.
Let e2X be given.
Assume He2X.
Apply HO Y HY (λu ⇒ Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) u ff u 0pack_b_b_e_e X' bX b2X eX e2X 0) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let eY be given.
Assume HeY.
Let e2Y be given.
Assume He2Y.
We will prove Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) (pack_b_b_e_e Y' bY b2Y eY e2Y) ff pack_b_b_e_e Y' bY b2Y eY e2Y 0pack_b_b_e_e X' bX b2X eX e2X 0.
rewrite the current goal using Hom_struct_b_b_e_e_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', f (bX x x') = bY (f x) (f x'))(∀x x'X', f (b2X x x') = b2Y (f x) (f x'))f eX = eYf e2X = e2Y.
Apply and5E (f Y'X') (∀x x'X', f (bX x x') = bY (f x) (f x')) (∀x x'X', f (b2X x x') = b2Y (f x) (f x')) (f eX = eY) (f e2X = e2Y) Hf to the current goal.
Assume Hf1: f Y'X'.
Assume Hf2: ∀x x'X', f (bX x x') = bY (f x) (f x').
Assume Hf3: ∀x x'X', f (b2X x x') = b2Y (f x) (f x').
Assume Hf4: f eX = eY.
Assume Hf5: f e2X = e2Y.
We will prove f pack_b_b_e_e Y' bY b2Y eY e2Y 0pack_b_b_e_e X' bX b2X eX e2X 0.
rewrite the current goal using pack_b_b_e_e_0_eq2 (from right to left).
rewrite the current goal using pack_b_b_e_e_0_eq2 (from right to left).
We will prove f Y'X'.
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_b_b_e_e u u (lam_id (u 0))) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let eX be given.
Assume HeX.
Let e2X be given.
Assume He2X.
We will prove Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) (pack_b_b_e_e X' bX b2X eX e2X) (lam_id (pack_b_b_e_e X' bX b2X eX e2X 0)).
rewrite the current goal using pack_b_b_e_e_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_b_b_e_e_pack (from left to right).
We will prove lam_id X' X'X'(∀x x'X', lam_id X' (bX x x') = bX (lam_id X' x) (lam_id X' x'))(∀x x'X', lam_id X' (b2X x x') = b2X (lam_id X' x) (lam_id X' x'))lam_id X' eX = eXlam_id X' e2X = e2X.
Apply and5I to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_id X' (bX x x') = bX ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is beta X' (λx ⇒ x) (bX x x') (HbX x Hx x' Hx').
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_id X' (b2X x x') = b2X ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is beta X' (λx ⇒ x) (b2X x x') (Hb2X x Hx x' Hx').
We will prove (λx ∈ X'x) eX = eX.
An exact proof term for the current goal is beta X' (λx ⇒ x) eX HeX.
We will prove (λx ∈ X'x) e2X = e2X.
An exact proof term for the current goal is beta X' (λx ⇒ x) e2X He2X.
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_b_b_e_e u Y fHom_struct_b_b_e_e Y Z gHom_struct_b_b_e_e u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let eX be given.
Assume HeX.
Let e2X be given.
Assume He2X.
We will prove Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) Y fHom_struct_b_b_e_e Y Z gHom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) Z (lam_comp (pack_b_b_e_e X' bX b2X eX e2X 0) g f).
rewrite the current goal using pack_b_b_e_e_0_eq2 (from right to left).
We will prove Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) Y fHom_struct_b_b_e_e Y Z gHom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) u fHom_struct_b_b_e_e u Z gHom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) Z (lam_comp X' g f)) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let eY be given.
Assume HeY.
Let e2Y be given.
Assume He2Y.
We will prove Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) (pack_b_b_e_e Y' bY b2Y eY e2Y) fHom_struct_b_b_e_e (pack_b_b_e_e Y' bY b2Y eY e2Y) Z gHom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_b_b_e_e_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', f (bX x x') = bY (f x) (f x'))(∀x x'X', f (b2X x x') = b2Y (f x) (f x'))f eX = eYf e2X = e2Y.
Apply HO Z HZ (λu ⇒ Hom_struct_b_b_e_e (pack_b_b_e_e Y' bY b2Y eY e2Y) u gHom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) u (lam_comp X' g f)) to the current goal.
Let Z' and bZ be given.
Assume HbZ.
Let b2Z be given.
Assume Hb2Z.
Let eZ be given.
Assume HeZ.
Let e2Z be given.
Assume He2Z.
We will prove Hom_struct_b_b_e_e (pack_b_b_e_e Y' bY b2Y eY e2Y) (pack_b_b_e_e Z' bZ b2Z eZ e2Z) gHom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) (pack_b_b_e_e Z' bZ b2Z eZ e2Z) (lam_comp X' g f).
rewrite the current goal using Hom_struct_b_b_e_e_pack (from left to right).
rewrite the current goal using Hom_struct_b_b_e_e_pack (from left to right).
Assume Hg: g Z'Y'(∀y y'Y', g (bY y y') = bZ (g y) (g y'))(∀y y'Y', g (b2Y y y') = b2Z (g y) (g y'))g eY = eZg e2Y = e2Z.
Apply and5E (f Y'X') (∀x x'X', f (bX x x') = bY (f x) (f x')) (∀x x'X', f (b2X x x') = b2Y (f x) (f x')) (f eX = eY) (f e2X = e2Y) Hf to the current goal.
Assume Hf1: f Y'X'.
Assume Hf2: ∀x x'X', f (bX x x') = bY (f x) (f x').
Assume Hf3: ∀x x'X', f (b2X x x') = b2Y (f x) (f x').
Assume Hf4: f eX = eY.
Assume Hf5: f e2X = e2Y.
Apply and5E (g Z'Y') (∀y y'Y', g (bY y y') = bZ (g y) (g y')) (∀y y'Y', g (b2Y y y') = b2Z (g y) (g y')) (g eY = eZ) (g e2Y = e2Z) Hg to the current goal.
Assume Hg1: g Z'Y'.
Assume Hg2: ∀y y'Y', g (bY y y') = bZ (g y) (g y').
Assume Hg3: ∀y y'Y', g (b2Y y y') = b2Z (g y) (g y').
Assume Hg4: g eY = eZ.
Assume Hg5: g e2Y = e2Z.
We will prove lam_comp X' g f Z'X'(∀x x'X', lam_comp X' g f (bX x x') = bZ (lam_comp X' g f x) (lam_comp X' g f x'))(∀x x'X', lam_comp X' g f (b2X x x') = b2Z (lam_comp X' g f x) (lam_comp X' g f x'))lam_comp X' g f eX = eZlam_comp X' g f e2X = e2Z.
Apply and5I to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_comp X' g f (bX x x') = bZ ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove (λx ∈ X'g (f x)) (bX x x') = bZ (g (f x)) (g (f x')).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (bX x x') (HbX x Hx x' Hx') (from left to right).
We will prove g (f (bX x x')) = bZ (g (f x)) (g (f x')).
rewrite the current goal using Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') (from right to left).
We will prove g (f (bX x x')) = g (bY (f x) (f x')).
Use f_equal.
An exact proof term for the current goal is Hf2 x Hx x' Hx'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_comp X' g f (b2X x x') = b2Z ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove (λx ∈ X'g (f x)) (b2X x x') = b2Z (g (f x)) (g (f x')).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (b2X x x') (Hb2X x Hx x' Hx') (from left to right).
We will prove g (f (b2X x x')) = b2Z (g (f x)) (g (f x')).
rewrite the current goal using Hg3 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') (from right to left).
We will prove g (f (b2X x x')) = g (b2Y (f x) (f x')).
Use f_equal.
An exact proof term for the current goal is Hf3 x Hx x' Hx'.
We will prove (λx ∈ X'g (f x)) eX = eZ.
rewrite the current goal using beta X' (λx ⇒ g (f x)) eX HeX (from left to right).
We will prove g (f eX) = eZ.
rewrite the current goal using Hf4 (from left to right).
An exact proof term for the current goal is Hg4.
We will prove (λx ∈ X'g (f x)) e2X = e2Z.
rewrite the current goal using beta X' (λx ⇒ g (f x)) e2X He2X (from left to right).
We will prove g (f e2X) = e2Z.
rewrite the current goal using Hf5 (from left to right).
An exact proof term for the current goal is Hg5.
Theorem. (MetaCat_struct_b_b_e_e_Forgetful_gen)
(∀X, Obj Xstruct_b_b_e_e X)MetaFunctor Obj Hom_struct_b_b_e_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_b_b_e_e X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_b_b_e_e u Y ff Y 0u 0) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let eX be given.
Assume HeX.
Let e2X be given.
Assume He2X.
Apply HO Y HY (λu ⇒ Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) u ff u 0pack_b_b_e_e X' bX b2X eX e2X 0) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let eY be given.
Assume HeY.
Let e2Y be given.
Assume He2Y.
We will prove Hom_struct_b_b_e_e (pack_b_b_e_e X' bX b2X eX e2X) (pack_b_b_e_e Y' bY b2Y eY e2Y) ff pack_b_b_e_e Y' bY b2Y eY e2Y 0pack_b_b_e_e X' bX b2X eX e2X 0.
rewrite the current goal using Hom_struct_b_b_e_e_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_b_b_e_e_0_eq2 (from right to left).
rewrite the current goal using pack_b_b_e_e_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_b_b_e_e L1.
Theorem. (MetaCat_struct_b_b_r_e_e_gen)
(∀X, Obj Xstruct_b_b_r_e_e X)MetaCat Obj Hom_struct_b_b_r_e_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)
Proof:
Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_b_b_r_e_e to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_b_b_r_e_e u Y ff Y 0u 0) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let rX and eX be given.
Assume HeX.
Let e2X be given.
Assume He2X.
Apply HO Y HY (λu ⇒ Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) u ff u 0pack_b_b_r_e_e X' bX b2X rX eX e2X 0) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let rY and eY be given.
Assume HeY.
Let e2Y be given.
Assume He2Y.
We will prove Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) (pack_b_b_r_e_e Y' bY b2Y rY eY e2Y) ff pack_b_b_r_e_e Y' bY b2Y rY eY e2Y 0pack_b_b_r_e_e X' bX b2X rX eX e2X 0.
rewrite the current goal using Hom_struct_b_b_r_e_e_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', f (bX x x') = bY (f x) (f x'))(∀x x'X', f (b2X x x') = b2Y (f x) (f x'))(∀x x'X', rX x x'rY (f x) (f x'))f eX = eYf e2X = e2Y.
Apply and6E (f Y'X') (∀x x'X', f (bX x x') = bY (f x) (f x')) (∀x x'X', f (b2X x x') = b2Y (f x) (f x')) (∀x x'X', rX x x'rY (f x) (f x')) (f eX = eY) (f e2X = e2Y) Hf to the current goal.
Assume Hf1: f Y'X'.
Assume Hf2: ∀x x'X', f (bX x x') = bY (f x) (f x').
Assume Hf3: ∀x x'X', f (b2X x x') = b2Y (f x) (f x').
Assume Hf4: ∀x x'X', rX x x'rY (f x) (f x').
Assume Hf5: f eX = eY.
Assume Hf6: f e2X = e2Y.
We will prove f pack_b_b_r_e_e Y' bY b2Y rY eY e2Y 0pack_b_b_r_e_e X' bX b2X rX eX e2X 0.
rewrite the current goal using pack_b_b_r_e_e_0_eq2 (from right to left).
rewrite the current goal using pack_b_b_r_e_e_0_eq2 (from right to left).
We will prove f Y'X'.
An exact proof term for the current goal is Hf1.
Let X be given.
Assume HX.
Apply HO X HX (λu ⇒ Hom_struct_b_b_r_e_e u u (lam_id (u 0))) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let rX and eX be given.
Assume HeX.
Let e2X be given.
Assume He2X.
We will prove Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) (pack_b_b_r_e_e X' bX b2X rX eX e2X) (lam_id (pack_b_b_r_e_e X' bX b2X rX eX e2X 0)).
rewrite the current goal using pack_b_b_r_e_e_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_b_b_r_e_e_pack (from left to right).
We will prove lam_id X' X'X'(∀x x'X', lam_id X' (bX x x') = bX (lam_id X' x) (lam_id X' x'))(∀x x'X', lam_id X' (b2X x x') = b2X (lam_id X' x) (lam_id X' x'))(∀x x'X', rX x x'rX (lam_id X' x) (lam_id X' x'))lam_id X' eX = eXlam_id X' e2X = e2X.
Apply and6I to the current goal.
An exact proof term for the current goal is lam_id_exp_In X'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_id X' (bX x x') = bX ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is beta X' (λx ⇒ x) (bX x x') (HbX x Hx x' Hx').
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_id X' (b2X x x') = b2X ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is beta X' (λx ⇒ x) (b2X x x') (Hb2X x Hx x' Hx').
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx' Hxx'.
We will prove rX ((λx ∈ X'x) x) ((λx ∈ X'x) x').
rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ x) x' Hx' (from left to right).
An exact proof term for the current goal is Hxx'.
We will prove (λx ∈ X'x) eX = eX.
An exact proof term for the current goal is beta X' (λx ⇒ x) eX HeX.
We will prove (λx ∈ X'x) e2X = e2X.
An exact proof term for the current goal is beta X' (λx ⇒ x) e2X He2X.
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_b_b_r_e_e u Y fHom_struct_b_b_r_e_e Y Z gHom_struct_b_b_r_e_e u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let rX and eX be given.
Assume HeX.
Let e2X be given.
Assume He2X.
We will prove Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) Y fHom_struct_b_b_r_e_e Y Z gHom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) Z (lam_comp (pack_b_b_r_e_e X' bX b2X rX eX e2X 0) g f).
rewrite the current goal using pack_b_b_r_e_e_0_eq2 (from right to left).
We will prove Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) Y fHom_struct_b_b_r_e_e Y Z gHom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) u fHom_struct_b_b_r_e_e u Z gHom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) Z (lam_comp X' g f)) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let rY and eY be given.
Assume HeY.
Let e2Y be given.
Assume He2Y.
We will prove Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) (pack_b_b_r_e_e Y' bY b2Y rY eY e2Y) fHom_struct_b_b_r_e_e (pack_b_b_r_e_e Y' bY b2Y rY eY e2Y) Z gHom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_b_b_r_e_e_pack (from left to right).
Assume Hf: f Y'X'(∀x x'X', f (bX x x') = bY (f x) (f x'))(∀x x'X', f (b2X x x') = b2Y (f x) (f x'))(∀x x'X', rX x x'rY (f x) (f x'))f eX = eYf e2X = e2Y.
Apply HO Z HZ (λu ⇒ Hom_struct_b_b_r_e_e (pack_b_b_r_e_e Y' bY b2Y rY eY e2Y) u gHom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) u (lam_comp X' g f)) to the current goal.
Let Z' and bZ be given.
Assume HbZ.
Let b2Z be given.
Assume Hb2Z.
Let rZ and eZ be given.
Assume HeZ.
Let e2Z be given.
Assume He2Z.
We will prove Hom_struct_b_b_r_e_e (pack_b_b_r_e_e Y' bY b2Y rY eY e2Y) (pack_b_b_r_e_e Z' bZ b2Z rZ eZ e2Z) gHom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) (pack_b_b_r_e_e Z' bZ b2Z rZ eZ e2Z) (lam_comp X' g f).
rewrite the current goal using Hom_struct_b_b_r_e_e_pack (from left to right).
rewrite the current goal using Hom_struct_b_b_r_e_e_pack (from left to right).
Assume Hg: g Z'Y'(∀y y'Y', g (bY y y') = bZ (g y) (g y'))(∀y y'Y', g (b2Y y y') = b2Z (g y) (g y'))(∀y y'Y', rY y y'rZ (g y) (g y'))g eY = eZg e2Y = e2Z.
Apply and6E (f Y'X') (∀x x'X', f (bX x x') = bY (f x) (f x')) (∀x x'X', f (b2X x x') = b2Y (f x) (f x')) (∀x x'X', rX x x'rY (f x) (f x')) (f eX = eY) (f e2X = e2Y) Hf to the current goal.
Assume Hf1: f Y'X'.
Assume Hf2: ∀x x'X', f (bX x x') = bY (f x) (f x').
Assume Hf3: ∀x x'X', f (b2X x x') = b2Y (f x) (f x').
Assume Hf4: ∀x x'X', rX x x'rY (f x) (f x').
Assume Hf5: f eX = eY.
Assume Hf6: f e2X = e2Y.
Apply and6E (g Z'Y') (∀y y'Y', g (bY y y') = bZ (g y) (g y')) (∀y y'Y', g (b2Y y y') = b2Z (g y) (g y')) (∀y y'Y', rY y y'rZ (g y) (g y')) (g eY = eZ) (g e2Y = e2Z) Hg to the current goal.
Assume Hg1: g Z'Y'.
Assume Hg2: ∀y y'Y', g (bY y y') = bZ (g y) (g y').
Assume Hg3: ∀y y'Y', g (b2Y y y') = b2Z (g y) (g y').
Assume Hg4: ∀y y'Y', rY y y'rZ (g y) (g y').
Assume Hg5: g eY = eZ.
Assume Hg6: g e2Y = e2Z.
We will prove lam_comp X' g f Z'X'(∀x x'X', lam_comp X' g f (bX x x') = bZ (lam_comp X' g f x) (lam_comp X' g f x'))(∀x x'X', lam_comp X' g f (b2X x x') = b2Z (lam_comp X' g f x) (lam_comp X' g f x'))(∀x x'X', rX x x'rZ (lam_comp X' g f x) (lam_comp X' g f x'))lam_comp X' g f eX = eZlam_comp X' g f e2X = e2Z.
Apply and6I to the current goal.
An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_comp X' g f (bX x x') = bZ ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove (λx ∈ X'g (f x)) (bX x x') = bZ (g (f x)) (g (f x')).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (bX x x') (HbX x Hx x' Hx') (from left to right).
We will prove g (f (bX x x')) = bZ (g (f x)) (g (f x')).
rewrite the current goal using Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') (from right to left).
We will prove g (f (bX x x')) = g (bY (f x) (f x')).
Use f_equal.
An exact proof term for the current goal is Hf2 x Hx x' Hx'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
We will prove lam_comp X' g f (b2X x x') = b2Z ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove (λx ∈ X'g (f x)) (b2X x x') = b2Z (g (f x)) (g (f x')).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (b2X x x') (Hb2X x Hx x' Hx') (from left to right).
We will prove g (f (b2X x x')) = b2Z (g (f x)) (g (f x')).
rewrite the current goal using Hg3 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') (from right to left).
We will prove g (f (b2X x x')) = g (b2Y (f x) (f x')).
Use f_equal.
An exact proof term for the current goal is Hf3 x Hx x' Hx'.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx' Hxx'.
We will prove rZ (lam_comp X' g f x) (lam_comp X' g f x').
We will prove rZ ((λx ∈ X'g (f x)) x) ((λx ∈ X'g (f x)) x').
rewrite the current goal using beta X' (λx ⇒ g (f x)) x Hx (from left to right).
rewrite the current goal using beta X' (λx ⇒ g (f x)) x' Hx' (from left to right).
We will prove rZ (g (f x)) (g (f x')).
Apply Hg4 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') to the current goal.
An exact proof term for the current goal is Hf4 x Hx x' Hx' Hxx'.
We will prove (λx ∈ X'g (f x)) eX = eZ.
rewrite the current goal using beta X' (λx ⇒ g (f x)) eX HeX (from left to right).
We will prove g (f eX) = eZ.
rewrite the current goal using Hf5 (from left to right).
An exact proof term for the current goal is Hg5.
We will prove (λx ∈ X'g (f x)) e2X = e2Z.
rewrite the current goal using beta X' (λx ⇒ g (f x)) e2X He2X (from left to right).
We will prove g (f e2X) = e2Z.
rewrite the current goal using Hf6 (from left to right).
An exact proof term for the current goal is Hg6.
Theorem. (MetaCat_struct_b_b_r_e_e_Forgetful_gen)
(∀X, Obj Xstruct_b_b_r_e_e X)MetaFunctor Obj Hom_struct_b_b_r_e_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f) (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
Proof:
Assume HO.
We prove the intermediate claim L1: ∀X Y f, Obj XObj YHom_struct_b_b_r_e_e X Y ff Y 0X 0.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_b_b_r_e_e u Y ff Y 0u 0) to the current goal.
Let X' and bX be given.
Assume HbX.
Let b2X be given.
Assume Hb2X.
Let rX and eX be given.
Assume HeX.
Let e2X be given.
Assume He2X.
Apply HO Y HY (λu ⇒ Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) u ff u 0pack_b_b_r_e_e X' bX b2X rX eX e2X 0) to the current goal.
Let Y' and bY be given.
Assume HbY.
Let b2Y be given.
Assume Hb2Y.
Let rY and eY be given.
Assume HeY.
Let e2Y be given.
Assume He2Y.
We will prove Hom_struct_b_b_r_e_e (pack_b_b_r_e_e X' bX b2X rX eX e2X) (pack_b_b_r_e_e Y' bY b2Y rY eY e2Y) ff pack_b_b_r_e_e Y' bY b2Y rY eY e2Y 0pack_b_b_r_e_e X' bX b2X rX eX e2X 0.
rewrite the current goal using Hom_struct_b_b_r_e_e_pack (from left to right).
Assume Hf.
rewrite the current goal using pack_b_b_r_e_e_0_eq2 (from right to left).
rewrite the current goal using pack_b_b_r_e_e_0_eq2 (from right to left).
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf _.
Apply Hf to the current goal.
Assume Hf1 _.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is MetaCatConcreteForgetful Obj (λX ⇒ X 0) Hom_struct_b_b_r_e_e L1.
End of Section MetaCatStruct