Beginning of Section MetaCat

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Definition. We define idT to be ∀X : set, Obj X → Hom X X (id X) of type prop.

In Proofgold the corresponding term root is 5b5295... and object id is 6e71b7...

Definition. We define compT to be ∀X Y Z : set, ∀f g : set, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → Hom X Z (comp X Y Z g f) of type prop.

In Proofgold the corresponding term root is fd3b02... and object id is b651ec...

Definition. We define idL to be ∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X X Y f (id X) = f of type prop.

In Proofgold the corresponding term root is 8bf949... and object id is 274215...

Definition. We define idR to be ∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X Y Y (id Y) f = f of type prop.

In Proofgold the corresponding term root is e0f11c... and object id is 9fe6a5...

Definition. We define compAssoc to be ∀X Y Z W : set, ∀f g h : set, Obj X → Obj Y → Obj Z → Obj W → Hom X Y f → Hom Y Z g → Hom Z W h → comp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f) of type prop.

In Proofgold the corresponding term root is 6fdbfa... and object id is 67897c...

Definition. We define MetaCat to be (idT ∧ compT) ∧ (idL ∧ idR) ∧ compAssoc of type prop.

In Proofgold the corresponding term root is fd9743... and object id is 1fb9aa...

Theorem. (MetaCat_I)

idT → compT → (∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X X Y f (id X) = f) → (∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X Y Y (id Y) f = f) → (∀X Y Z W : set, ∀f g h : set, Obj X → Obj Y → Obj Z → Obj W → Hom X Y f → Hom Y Z g → Hom Z W h → comp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f)) → MetaCat

In Proofgold the corresponding term root is fc5379... and proposition id is 047c95...

Proof:
Proof not loaded.

Theorem. (MetaCat_E)

MetaCat → ∀p : prop, (idT → compT → (∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X X Y f (id X) = f) → (∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X Y Y (id Y) f = f) → (∀X Y Z W : set, ∀f g h : set, Obj X → Obj Y → Obj Z → Obj W → Hom X Y f → Hom Y Z g → Hom Z W h → comp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f)) → p) → p

In Proofgold the corresponding term root is d158dd... and proposition id is 7da4b2...

Proof:
Proof not loaded.

End of Section MetaCat

Beginning of Section MetaCatOp

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Theorem. (MetaCatOp)

MetaCat Obj Hom id comp → MetaCat Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f)

In Proofgold the corresponding term root is e74d2a... and proposition id is 6f34fb...

Proof:
Proof not loaded.

End of Section MetaCatOp

Beginning of Section LimsCoLims

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Definition. We define monic to be λX Y f ⇒ Obj X ∧ Obj Y ∧ Hom X Y f ∧ ∀Z : set, Obj Z → ∀g h : set, Hom Z X g → Hom Z X h → comp Z X Y f g = comp Z X Y f h → g = h of type set → set → set → prop.

In Proofgold the corresponding term root is bb42af... and object id is 4204ac...

Definition. We define terminal_p to be λY h ⇒ Obj Y ∧ ∀X : set, Obj X → Hom X Y (h X) ∧ ∀h' : set, Hom X Y h' → h' = h X of type set → (set → set) → prop.

In Proofgold the corresponding term root is fdae77... and object id is fc25a5...

Definition. We define initial_p to be λY h ⇒ Obj Y ∧ ∀X : set, Obj X → Hom Y X (h X) ∧ ∀h' : set, Hom Y X h' → h' = h X of type set → (set → set) → prop.

In Proofgold the corresponding term root is a7ed72... and object id is f206b9...

Definition. We define product_p to be λX Y Z pi0 pi1 pair ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom Z X pi0 ∧ Hom Z Y pi1 ∧ ∀W : set, Obj W → ∀h k : set, Hom W X h → Hom W Y k → Hom W Z (pair W h k) ∧ comp W Z X pi0 (pair W h k) = h ∧ comp W Z Y pi1 (pair W h k) = k ∧ ∀u : set, Hom W Z u → comp W Z X pi0 u = h → comp W Z Y pi1 u = k → u = pair W h k of type set → set → set → set → set → (set → set → set → set) → prop.

In Proofgold the corresponding term root is 493d09... and object id is c575e7...

Definition. We define product_constr_p to be λprod pi0 pi1 pair ⇒ ∀X Y : set, Obj X → Obj Y → product_p X Y (prod X Y) (pi0 X Y) (pi1 X Y) (pair X Y) of type (set → set → set) → (set → set → set) → (set → set → set) → (set → set → set → set → set → set) → prop.

In Proofgold the corresponding term root is 8627a9... and object id is a34635...

Definition. We define coproduct_p to be λX Y Z i0 i1 comb ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom X Z i0 ∧ Hom Y Z i1 ∧ ∀W : set, Obj W → ∀h k : set, Hom X W h → Hom Y W k → Hom Z W (comb W h k) ∧ comp X Z W (comb W h k) i0 = h ∧ comp Y Z W (comb W h k) i1 = k ∧ ∀hk : set, Hom Z W hk → comp X Z W hk i0 = h → comp Y Z W hk i1 = k → hk = comb W h k of type set → set → set → set → set → (set → set → set → set) → prop.

In Proofgold the corresponding term root is 1aca76... and object id is 545d6c...

Definition. We define coproduct_constr_p to be λcoprod i0 i1 copair ⇒ ∀X Y : set, Obj X → Obj Y → coproduct_p X Y (coprod X Y) (i0 X Y) (i1 X Y) (copair X Y) of type (set → set → set) → (set → set → set) → (set → set → set) → (set → set → set → set → set → set) → prop.

In Proofgold the corresponding term root is 9283ca... and object id is a3944e...

Definition. We define equalizer_p to be λX Y f g Q q fac ⇒ Obj X ∧ Obj Y ∧ Hom X Y f ∧ Hom X Y g ∧ Obj Q ∧ Hom Q X q ∧ comp Q X Y f q = comp Q X Y g q ∧ ∀W : set, Obj W → ∀h : set, Hom W X h → comp W X Y f h = comp W X Y g h → Hom W Q (fac W h) ∧ comp W Q X q (fac W h) = h ∧ ∀u : set, Hom W Q u → comp W Q X q u = h → u = fac W h of type set → set → set → set → set → set → (set → set → set) → prop.

In Proofgold the corresponding term root is e54193... and object id is 067f6a...

Definition. We define equalizer_constr_p to be λquot canonmap fac ⇒ ∀X Y : set, Obj X → Obj Y → ∀f g : set, Hom X Y f → Hom X Y g → equalizer_p X Y f g (quot X Y f g) (canonmap X Y f g) (fac X Y f g) of type (set → set → set → set → set) → (set → set → set → set → set) → (set → set → set → set → set → set → set) → prop.

In Proofgold the corresponding term root is 57caf1... and object id is 1c082c...

Definition. We define coequalizer_p to be λX Y f g Q q fac ⇒ Obj X ∧ Obj Y ∧ Hom X Y f ∧ Hom X Y g ∧ Obj Q ∧ Hom Y Q q ∧ comp X Y Q q f = comp X Y Q q g ∧ ∀W : set, Obj W → ∀h : set, Hom Y W h → comp X Y W h f = comp X Y W h g → Hom Q W (fac W h) ∧ comp Y Q W (fac W h) q = h ∧ ∀u : set, Hom Q W u → comp Y Q W u q = h → u = fac W h of type set → set → set → set → set → set → (set → set → set) → prop.

In Proofgold the corresponding term root is 7f834d... and object id is dfe3bc...

Definition. We define coequalizer_constr_p to be λquot canonmap fac ⇒ ∀X Y : set, Obj X → Obj Y → ∀f g : set, Hom X Y f → Hom X Y g → coequalizer_p X Y f g (quot X Y f g) (canonmap X Y f g) (fac X Y f g) of type (set → set → set → set → set) → (set → set → set → set → set) → (set → set → set → set → set → set → set) → prop.

In Proofgold the corresponding term root is 1d8fdb... and object id is bfc97c...

Definition. We define pullback_p to be λX Y Z f g P pi0 pi1 pair ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom X Z f ∧ Hom Y Z g ∧ Obj P ∧ Hom P X pi0 ∧ Hom P Y pi1 ∧ comp 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 k → comp W X Z f h = comp W Y Z g k → Hom W P (pair W h k) ∧ comp W P X pi0 (pair W h k) = h ∧ comp W P Y pi1 (pair W h k) = k ∧ ∀u : set, Hom W P u → comp W P X pi0 u = h → comp W P Y pi1 u = k → u = pair W h k of type set → set → set → set → set → set → set → set → (set → set → set → set) → prop.

In Proofgold the corresponding term root is aa77e5... and object id is 86c867...

Definition. We define pullback_constr_p to be λpb pi0 pi1 pair ⇒ ∀X Y Z : set, Obj X → Obj Y → Obj Z → ∀f g : set, Hom X Z f → Hom Y Z g → pullback_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 (set → set → set → set → set → set) → (set → set → set → set → set → set) → (set → set → set → set → set → set) → (set → set → set → set → set → set → set → set → set) → prop.

In Proofgold the corresponding term root is c0b415... and object id is 39fb29...

Definition. We define pushout_p to be λX Y Z f g P i0 i1 copair ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom Z X f ∧ Hom Z Y g ∧ Obj P ∧ Hom X P i0 ∧ Hom Y P i1 ∧ comp 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 k → comp Z X W h f = comp Z Y W k g → Hom P W (copair W h k) ∧ comp X P W (copair W h k) i0 = h ∧ comp Y P W (copair W h k) i1 = k ∧ ∀u : set, Hom P W u → comp X P W u i0 = h → comp Y P W u i1 = k → u = copair W h k of type set → set → set → set → set → set → set → set → (set → set → set → set) → prop.

In Proofgold the corresponding term root is a2ad18... and object id is 062995...

Definition. We define pushout_constr_p to be λpo i0 i1 copair ⇒ ∀X Y Z : set, Obj X → Obj Y → Obj Z → ∀f g : set, Hom Z X f → Hom Z Y g → pushout_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 (set → set → set → set → set → set) → (set → set → set → set → set → set) → (set → set → set → set → set → set) → (set → set → set → set → set → set → set → set → set) → prop.

In Proofgold the corresponding term root is 6b9515... and object id is 455559...

Definition. We define exponent_p to be λprod pi0 pi1 pair X Y Z a lm ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom (prod Z X) Y a ∧ ∀W : set, Obj W → ∀f : set, Hom (prod W X) Y f → Hom 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 g → comp (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)) = f → g = lm W f of type (set → set → set) → (set → set → set) → (set → set → set) → (set → set → set → set → set → set) → set → set → set → set → (set → set → set) → prop.

In Proofgold the corresponding term root is 7f9d1d... and object id is 900ac5...

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 X → Obj Y → exponent_p prod pi0 pi1 pair X Y (exp X Y) (a X Y) (lm X Y) of type (set → set → set) → (set → set → set) → (set → set → set) → (set → set → set → set → set → set) → (set → set → set) → (set → set → set) → (set → set → set → set → set) → prop.

In Proofgold the corresponding term root is b618df... and object id is fbdca4...

Definition. We define subobject_classifier_p to be λone uniqa Omega tru ch constr_p ⇒ terminal_p one uniqa ∧ Obj Omega ∧ Hom one Omega tru ∧ ∀X Y : set, ∀m : set, monic X Y m → Hom 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 → (set → set) → set → set → (set → set → set → set) → (set → set → set → set → set → set → set) → prop.

In Proofgold the corresponding term root is 23398d... and object id is b2f9d5...

Definition. We define nno_p to be λone uniqa N zer suc rec ⇒ terminal_p one uniqa ∧ Obj N ∧ Hom one N zer ∧ Hom N N suc ∧ ∀X : set, ∀x : set, ∀f : set, Obj X → Hom one X x → Hom X X f → Hom N X (rec X x f) ∧ comp one N X (rec X x f) zer = x ∧ comp N N X (rec X x f) suc = comp N X X f (rec X x f) ∧ ∀u : set, Hom N X u → comp one N X u zer = x → comp N N X u suc = comp N X X f u → u = rec X x f of type set → (set → set) → set → set → set → (set → set → set → set) → prop.

In Proofgold the corresponding term root is 037a74... and object id is b05ec9...

End of Section LimsCoLims

Beginning of Section LimsCoLims2

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Theorem. (product_coproduct_Op)

∀X Y Z : set, ∀pi0 pi1 : set, ∀pair : set → set → set → set, product_p Obj Hom id comp X Y Z pi0 pi1 pair → coproduct_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

In Proofgold the corresponding term root is 38cf5b... and proposition id is 9dd4bb...

Proof:
Proof not loaded.

Theorem. (product_coproduct_constr_Op)

∀prod : set → set → set, ∀pi0 pi1 : set → set → set, ∀pair : set → set → set → set → set → set, product_constr_p Obj Hom id comp prod pi0 pi1 pair → coproduct_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) prod pi0 pi1 pair

In Proofgold the corresponding term root is 5f1c74... and proposition id is 31c777...

Proof:
Proof not loaded.

Theorem. (coproduct_product_Op)

∀X Y Z : set, ∀i0 i1 : set, ∀copair : set → set → set → set, coproduct_p Obj Hom id comp X Y Z i0 i1 copair → product_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

In Proofgold the corresponding term root is 84a847... and proposition id is df89e7...

Proof:
Proof not loaded.

Theorem. (coproduct_product_constr_Op)

∀coprod : set → set → set, ∀i0 i1 : set → set → set, ∀copair : set → set → set → set → set → set, coproduct_constr_p Obj Hom id comp coprod i0 i1 copair → product_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) coprod i0 i1 copair

In Proofgold the corresponding term root is 3e498f... and proposition id is 2bad67...

Proof:
Proof not loaded.

Theorem. (equalizer_coequalizer_Op)

∀X Y : set, ∀f g : set, ∀Q : set, ∀q : set, ∀fac : set → set → set, equalizer_p Obj Hom id comp X Y f g Q q fac → coequalizer_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

In Proofgold the corresponding term root is 6fb40a... and proposition id is 434dd4...

Proof:
Proof not loaded.

Theorem. (equalizer_coequalizer_constr_Op)

∀quot : set → set → set → set → set, ∀canonmap : set → set → set → set → set, ∀fac : set → set → set → set → set → set → set, equalizer_constr_p Obj Hom id comp quot canonmap fac → coequalizer_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)

In Proofgold the corresponding term root is ebf9a6... and proposition id is 71f1f9...

Proof:
Proof not loaded.

Theorem. (coequalizer_equalizer_Op)

∀X Y : set, ∀f g : set, ∀Q : set, ∀q : set, ∀fac : set → set → set, coequalizer_p Obj Hom id comp X Y f g Q q fac → equalizer_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

In Proofgold the corresponding term root is 23000b... and proposition id is ed80d2...

Proof:
Proof not loaded.

Theorem. (coequalizer_equalizer_constr_Op)

∀quot : set → set → set → set → set, ∀canonmap : set → set → set → set → set, ∀fac : set → set → set → set → set → set → set, coequalizer_constr_p Obj Hom id comp quot canonmap fac → equalizer_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)

In Proofgold the corresponding term root is 20c134... and proposition id is 466a77...

Proof:
Proof not loaded.

Theorem. (pullback_pushout_Op)

∀X Y Z : set, ∀f g : set, ∀P : set, ∀pi0 pi1 : set, ∀pair : set → set → set → set, pullback_p Obj Hom id comp X Y Z f g P pi0 pi1 pair → pushout_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

In Proofgold the corresponding term root is a1e515... and proposition id is 038557...

Proof:
Proof not loaded.

Theorem. (pullback_pushout_constr_Op)

∀pb : set → set → set → set → set → set, ∀pi0 pi1 : set → set → set → set → set → set, ∀pair : set → set → set → set → set → set → set → set → set, pullback_constr_p Obj Hom id comp pb pi0 pi1 pair → pushout_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) pb pi0 pi1 pair

In Proofgold the corresponding term root is c883c5... and proposition id is 9b6aee...

Proof:
Proof not loaded.

Theorem. (pushout_pullback_Op)

∀X Y Z : set, ∀f g : set, ∀P : set, ∀i0 i1 : set, ∀copair : set → set → set → set, pushout_p Obj Hom id comp X Y Z f g P i0 i1 copair → pullback_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

In Proofgold the corresponding term root is ce8d4a... and proposition id is 4e78ad...

Proof:
Proof not loaded.

Theorem. (pushout_pullback_constr_Op)

∀po : set → set → set → set → set → set, ∀i0 i1 : set → set → set → set → set → set, ∀copair : set → set → set → set → set → set → set → set → set, pushout_constr_p Obj Hom id comp po i0 i1 copair → pullback_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) po i0 i1 copair

In Proofgold the corresponding term root is 340ba6... and proposition id is d2ca56...

Proof:
Proof not loaded.

Theorem. (product_equalizer_pullback_constr)

MetaCat Obj Hom id comp → ∀quot : set → set → set → set → set, ∀canonmap : set → set → set → set → set, ∀fac : set → set → set → set → set → set → set, equalizer_constr_p Obj Hom id comp quot canonmap fac → ∀prod : set → set → set, ∀pi0 : set → set → set, ∀pi1 : set → set → set, ∀pair : set → set → set → set → set → set, product_constr_p Obj Hom id comp prod pi0 pi1 pair → pullback_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))

In Proofgold the corresponding term root is 1c512a... and proposition id is 1abd16...

Proof:
Proof not loaded.

Theorem. (product_equalizer_pullback_constr_ex)

MetaCat Obj Hom id comp → (∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_p Obj Hom id comp quot canonmap fac) → (∃prod : set → set → set, ∃pi0 : set → set → set, ∃pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p Obj Hom id comp prod pi0 pi1 pair) → ∃pb : set → set → set → set → set → set, ∃pi0 : set → set → set → set → set → set, ∃pi1 : set → set → set → set → set → set, ∃pair : set → set → set → set → set → set → set → set → set, pullback_constr_p Obj Hom id comp pb pi0 pi1 pair

In Proofgold the corresponding term root is 9a59ec... and proposition id is ed2b0e...

Proof:
Proof not loaded.

End of Section LimsCoLims2

Beginning of Section LimsCoLims3

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Theorem. (coproduct_coequalizer_pushout_constr_ex)

MetaCat Obj Hom id comp → (∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p Obj Hom id comp quot canonmap fac) → (∃coprod : set → set → set, ∃i0 : set → set → set, ∃i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p Obj Hom id comp coprod i0 i1 copair) → ∃po : set → set → set → set → set → set, ∃i0 : set → set → set → set → set → set, ∃i1 : set → set → set → set → set → set, ∃copair : set → set → set → set → set → set → set → set → set, pushout_constr_p Obj Hom id comp po i0 i1 copair

In Proofgold the corresponding term root is 70eb6d... and proposition id is b0aadc...

Proof:
Proof not loaded.

End of Section LimsCoLims3

Definition. We define SetHom to be λX Y f ⇒ f ∈ Y^X of type set → set → set → prop.

In Proofgold the corresponding term root is de8fdf... and object id is af2f63...

Theorem. (MetaCatSet_initial_gen)

∀Obj : set → prop, Obj 0 → ∃Y : set, ∃uniqa : set → set, initial_p Obj SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa

In Proofgold the corresponding term root is 31dcb8... and proposition id is fa807d...

Proof:
Proof not loaded.

Theorem. (MetaCatSet_initial)

∃Y : set, ∃uniqa : set → set, initial_p (λ_ ⇒ True) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa

In Proofgold the corresponding term root is 648295... and proposition id is 80cab9...

Proof:
Proof not loaded.

Theorem. (MetaCatSet_terminal_gen)

∀Obj : set → prop, Obj 1 → ∃Y : set, ∃uniqa : set → set, terminal_p Obj SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa

In Proofgold the corresponding term root is b6fb54... and proposition id is 4cd1b7...

Proof:
Proof not loaded.

Theorem. (MetaCatSet_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p (λ_ ⇒ True) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa

In Proofgold the corresponding term root is bf7783... and proposition id is 370ea7...

Proof:
Proof not loaded.

Theorem. (MetaCatSet_coproduct_gen)

∀Obj : set → prop, (∀X, Obj X → ∀Y, Obj Y → Obj (setsum X Y)) → ∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p Obj SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) coprod i0 i1 copair

In Proofgold the corresponding term root is 7e8001... and proposition id is 3c078b...

Proof:
Proof not loaded.

Theorem. (MetaCatSet_coproduct)

∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p (λ_ ⇒ True) SetHom (λX ⇒ λx ∈ X ⇒ x) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) coprod i0 i1 copair

In Proofgold the corresponding term root is 2c4f22... and proposition id is c28eaa...

Proof:
Proof not loaded.

Theorem. (MetaCatSet_product_gen)

∀Obj : set → prop, (∀X, Obj X → ∀Y, Obj Y → Obj (setprod X Y)) → ∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p Obj SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) prod pi0 pi1 pair

In Proofgold the corresponding term root is 2d427e... and proposition id is 21e789...

Proof:
Proof not loaded.

Theorem. (MetaCatSet_product)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p (λ_ ⇒ True) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) prod pi0 pi1 pair

In Proofgold the corresponding term root is 8c56c9... and proposition id is 14d110...

Proof:
Proof not loaded.

Theorem. (UnivOf_Subq_closed)

∀N, ∀X ∈ UnivOf N, ∀Q ⊆ X, Q ∈ UnivOf N

In Proofgold the corresponding term root is 1bcb03... and proposition id is 6aa34e...

Proof:
Proof not loaded.

Definition. We define famunion_closed to be λU : set ⇒ ∀X ∈ U, ∀F : set → set, (∀x ∈ X, F x ∈ U) → famunion X F ∈ U of type set → prop.

In Proofgold the corresponding term root is caf77a... and object id is f8891c...

Theorem. (Union_Repl_famunion_closed)

∀U : set, Union_closed U → Repl_closed U → famunion_closed U

In Proofgold the corresponding term root is 35501a... and proposition id is 345f8f...

Proof:
Proof not loaded.

Theorem. (ZF_closed_0)

∀U X, TransSet U → ZF_closed U → X ∈ U → 0 ∈ U

In Proofgold the corresponding term root is e747e5... and proposition id is 1037dc...

Proof:
Proof not loaded.

Theorem. (ZF_Inj1_closed)

∀U, TransSet U → ZF_closed U → ∀X ∈ U, Inj1 X ∈ U

In Proofgold the corresponding term root is 617147... and proposition id is 7eedbc...

Proof:
Proof not loaded.

Theorem. (ZF_Inj0_closed)

∀U, TransSet U → ZF_closed U → ∀X ∈ U, Inj0 X ∈ U

In Proofgold the corresponding term root is 219267... and proposition id is 1045a1...

Proof:
Proof not loaded.

Theorem. (ZF_setsum_closed)

∀U, TransSet U → ZF_closed U → ∀X Y ∈ U, (X + Y) ∈ U

In Proofgold the corresponding term root is 527cc5... and proposition id is 32cb89...

Proof:
Proof not loaded.

Theorem. (ZF_Sigma_closed)

∀U, TransSet U → ZF_closed U → ∀X ∈ U, ∀Y : set → set, (∀x ∈ X, Y x ∈ U) → (∑x ∈ X, Y x) ∈ U

In Proofgold the corresponding term root is d9ae82... and proposition id is c59b39...

Proof:
Proof not loaded.

Theorem. (ZF_setprod_closed)

∀U, TransSet U → ZF_closed U → ∀X Y ∈ U, (X ⨯ Y) ∈ U

In Proofgold the corresponding term root is 168889... and proposition id is ecfb59...

Proof:
Proof not loaded.

Theorem. (ZF_Pi_closed)

∀U, TransSet U → ZF_closed U → ∀X ∈ U, ∀Y : set → set, (∀x ∈ X, Y x ∈ U) → (∏x ∈ X, Y x) ∈ U

In Proofgold the corresponding term root is 632304... and proposition id is 43ba53...

Proof:
Proof not loaded.

Theorem. (ZF_setexp_closed)

∀U, TransSet U → ZF_closed U → ∀X Y ∈ U, (Y^X) ∈ U

In Proofgold the corresponding term root is 248526... and proposition id is 331185...

Proof:
Proof not loaded.

Theorem. (MetaCatHFSet_initial)

∃Y : set, ∃uniqa : set → set, initial_p (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa

In Proofgold the corresponding term root is 0741fe... and proposition id is 6694e8...

Proof:
Proof not loaded.

Theorem. (MetaCatSmallSet_initial)

∃Y : set, ∃uniqa : set → set, initial_p (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa

In Proofgold the corresponding term root is 964635... and proposition id is 4e15ce...

Proof:
Proof not loaded.

Theorem. (MetaCatHFSet_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa

In Proofgold the corresponding term root is 703b92... and proposition id is d36462...

Proof:
Proof not loaded.

Theorem. (MetaCatSmallSet_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa

In Proofgold the corresponding term root is 1f7930... and proposition id is b5da2c...

Proof:
Proof not loaded.

Theorem. (MetaCatHFSet_coproduct)

∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ λx ∈ X ⇒ x) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) coprod i0 i1 copair

In Proofgold the corresponding term root is df899b... and proposition id is 5604f1...

Proof:
Proof not loaded.

Theorem. (MetaCatSmallSet_coproduct)

∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) coprod i0 i1 copair

In Proofgold the corresponding term root is 15e47c... and proposition id is 002eee...

Proof:
Proof not loaded.

Theorem. (MetaCatHFSet_product)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) prod pi0 pi1 pair

In Proofgold the corresponding term root is 2bef5b... and proposition id is 8ae2a3...

Proof:
Proof not loaded.

Theorem. (MetaCatSmallSet_product)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) prod pi0 pi1 pair

In Proofgold the corresponding term root is 2285d1... and proposition id is 4281ba...

Proof:
Proof not loaded.

Beginning of Section MetaFunctor

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Variable Obj' : set → prop

Variable Hom' : set → set → set → prop

Variable id' : set → set

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

Variable F0 : set → set

Variable F1 : set → set → set → set

Definition. We define MetaFunctor to be (∀X, Obj X → Obj' (F0 X)) ∧ (∀X Y f, Obj X → Obj Y → Hom X Y f → Hom' (F0 X) (F0 Y) (F1 X Y f)) ∧ (∀X, Obj X → F1 X X (id X) = id' (F0 X)) ∧ (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → F1 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.

In Proofgold the corresponding term root is f35b67... and object id is c80743...

Theorem. (MetaFunctorI)

(∀X, Obj X → Obj' (F0 X)) → (∀X Y f, Obj X → Obj Y → Hom X Y f → Hom' (F0 X) (F0 Y) (F1 X Y f)) → (∀X, Obj X → F1 X X (id X) = id' (F0 X)) → (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → F1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)) → MetaFunctor

In Proofgold the corresponding term root is 795e29... and proposition id is 2cb62d...

Proof:
Proof not loaded.

Theorem. (MetaFunctorE)

MetaFunctor → ∀p : prop, ((∀X, Obj X → Obj' (F0 X)) → (∀X Y f, Obj X → Obj Y → Hom X Y f → Hom' (F0 X) (F0 Y) (F1 X Y f)) → (∀X, Obj X → F1 X X (id X) = id' (F0 X)) → (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → F1 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

In Proofgold the corresponding term root is d4b40e... and proposition id is 973e25...

Proof:
Proof not loaded.

Definition. We define MetaFunctor_strict to be MetaCat Obj Hom id comp ∧ MetaCat Obj' Hom' id' comp' ∧ MetaFunctor of type prop.

In Proofgold the corresponding term root is 8085cf... and object id is 070aeb...

Theorem. (MetaFunctor_strict_I)

MetaCat Obj Hom id comp → MetaCat Obj' Hom' id' comp' → MetaFunctor → MetaFunctor_strict

In Proofgold the corresponding term root is 3d0579... and proposition id is 5cbb4a...

Proof:
Proof not loaded.

Theorem. (MetaFunctor_strict_E)

MetaFunctor_strict → ∀p : prop, (MetaCat Obj Hom id comp → MetaCat Obj' Hom' id' comp' → MetaFunctor → p) → p

In Proofgold the corresponding term root is b9f4ec... and proposition id is 953054...

Proof:
Proof not loaded.

End of Section MetaFunctor

Beginning of Section IdFunctor

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Theorem. (MetaCat_IdFunctor)

MetaFunctor Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f)

In Proofgold the corresponding term root is ee743b... and proposition id is b7eb16...

Proof:
Proof not loaded.

Theorem. (MetaCat_IdFunctor_strict)

MetaCat Obj Hom id comp → MetaFunctor_strict Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f)

In Proofgold the corresponding term root is 73c677... and proposition id is 2447d9...

Proof:
Proof not loaded.

End of Section IdFunctor

Beginning of Section CompFunctors

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Variable Obj' : set → prop

Variable Hom' : set → set → set → prop

Variable id' : set → set

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

Variable Obj'' : set → prop

Variable Hom'' : set → set → set → prop

Variable id'' : set → set

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

Variable F0 : set → set

Variable F1 : set → set → set → set

Variable G0 : set → set

Variable G1 : set → set → set → set

Theorem. (MetaCat_CompFunctors)

MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1 → MetaFunctor Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1 → MetaFunctor Obj Hom id comp Obj'' Hom'' id'' comp'' (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f))

In Proofgold the corresponding term root is 830254... and proposition id is d7211d...

Proof:
Proof not loaded.

Theorem. (MetaCat_CompFunctors_strict)

MetaFunctor_strict Obj Hom id comp Obj' Hom' id' comp' F0 F1 → MetaFunctor_strict Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1 → MetaFunctor_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))

In Proofgold the corresponding term root is 7ad5e2... and proposition id is 1eb285...

Proof:
Proof not loaded.

End of Section CompFunctors

Beginning of Section MetaNatTrans

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Variable Obj' : set → prop

Variable Hom' : set → set → set → prop

Variable id' : set → set

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

Variable F0 : set → set

Variable F1 : set → set → set → set

Variable G0 : set → set

Variable G1 : set → set → set → set

Variable eta : set → set

Definition. We define MetaNatTrans to be (∀X, Obj X → Hom' (F0 X) (G0 X) (eta X)) ∧ (∀X Y f, Obj X → Obj Y → Hom X Y f → comp' (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.

In Proofgold the corresponding term root is cf0ad1... and object id is 08be86...

Theorem. (MetaNatTransI)

(∀X, Obj X → Hom' (F0 X) (G0 X) (eta X)) → (∀X Y f, Obj X → Obj Y → Hom X Y f → comp' (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

In Proofgold the corresponding term root is 8286b8... and proposition id is c1d681...

Proof:
Proof not loaded.

Theorem. (MetaNatTransE)

MetaNatTrans → ∀p : prop, ((∀X, Obj X → Hom' (F0 X) (G0 X) (eta X)) → (∀X Y f, Obj X → Obj Y → Hom X Y f → comp' (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

In Proofgold the corresponding term root is 60c5d3... and proposition id is aa53ac...

Proof:
Proof not loaded.

Definition. We define MetaNatTrans_strict to be 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 of type prop.

In Proofgold the corresponding term root is 1b6ee9... and object id is bd2de2...

Theorem. (MetaNatTrans_strict_I)

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 → MetaNatTrans_strict

In Proofgold the corresponding term root is fea59f... and proposition id is 59a372...

Proof:
Proof not loaded.

Theorem. (MetaNatTrans_strict_E)

MetaNatTrans_strict → ∀p : prop, (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 → p) → p

In Proofgold the corresponding term root is db0322... and proposition id is b8f26b...

Proof:
Proof not loaded.

End of Section MetaNatTrans

Beginning of Section CompFunctorNatTrans

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Variable Obj' : set → prop

Variable Hom' : set → set → set → prop

Variable id' : set → set

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

Variable Obj'' : set → prop

Variable Hom'' : set → set → set → prop

Variable id'' : set → set

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

Variable F0 : set → set

Variable F1 : set → set → set → set

Variable G0 : set → set

Variable G1 : set → set → set → set

Variable H0 : set → set

Variable H1 : set → set → set → set

Variable eta : set → set

Theorem. (MetaCat_CompFunctorNatTrans)

MetaFunctor 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' F0 F1 G0 G1 eta → MetaFunctor Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' H0 H1 → MetaNatTrans 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))

In Proofgold the corresponding term root is e1978b... and proposition id is d7aeb3...

Proof:
Proof not loaded.

End of Section CompFunctorNatTrans

Beginning of Section CompNatTransFunctor

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Variable Obj' : set → prop

Variable Hom' : set → set → set → prop

Variable id' : set → set

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

Variable Obj'' : set → prop

Variable Hom'' : set → set → set → prop

Variable id'' : set → set

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

Variable F0 : set → set

Variable F1 : set → set → set → set

Variable G0 : set → set

Variable G1 : set → set → set → set

Variable H0 : set → set

Variable H1 : set → set → set → set

Variable eta : set → set

Theorem. (MetaCat_CompNatTransFunctor)

MetaNatTrans Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' F0 F1 G0 G1 eta → MetaFunctor Obj Hom id comp Obj' Hom' id' comp' H0 H1 → MetaNatTrans 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))

In Proofgold the corresponding term root is b7392d... and proposition id is b8a6b7...

Proof:
Proof not loaded.

End of Section CompNatTransFunctor

Beginning of Section MetaMonad

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Variable T0 : set → set

Variable T1 : set → set → set → set

Variable eta : set → set

Variable mu : set → set

Definition. We define MetaMonad to be (∀X, Obj X → 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))) ∧ (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X)) ∧ (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)) of type prop.

In Proofgold the corresponding term root is bb95d4... and object id is 7c9f95...

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 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 of type prop.

In Proofgold the corresponding term root is 8e3f5c... and object id is ce28f9...

Theorem. (MetaMonadI)

(∀X, Obj X → 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))) → (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X)) → (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)) → MetaMonad

In Proofgold the corresponding term root is 7671e5... and proposition id is 46096c...

Proof:
Proof not loaded.

Theorem. (MetaMonadE)

MetaMonad → (∀p : prop, ((∀X, Obj X → 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))) → (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X)) → (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)) → p) → p)

In Proofgold the corresponding term root is 40a66b... and proposition id is f4ba21...

Proof:
Proof not loaded.

Theorem. (MetaMonad_strict_I)

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 → MetaMonad_strict

In Proofgold the corresponding term root is 73fd1c... and proposition id is 163090...

Proof:
Proof not loaded.

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 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 → p) → p

In Proofgold the corresponding term root is 84fe03... and proposition id is 80e837...

Proof:
Proof not loaded.

End of Section MetaMonad

Beginning of Section MetaAdjunction

Variable Obj : set → prop

Variable Hom : set → set → set → prop

Variable id : set → set

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

Variable Obj' : set → prop

Variable Hom' : set → set → set → prop

Variable id' : set → set

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

Variable F0 : set → set

Variable F1 : set → set → set → set

Variable G0 : set → set

Variable G1 : set → set → set → set

Variable eta : set → set

Variable eps : set → set

Definition. We define MetaAdjunction to be (∀X, Obj X → comp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X)) ∧ (∀Y, Obj' Y → comp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y)) of type prop.

In Proofgold the corresponding term root is e8b6c4... and object id is bda632...

Definition. We define MetaAdjunction_strict to be 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 of type prop.

In Proofgold the corresponding term root is c8ed7d... and object id is 3ab943...

Theorem. (MetaAdjunctionI)

(∀X, Obj X → comp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X)) → (∀Y, Obj' Y → comp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y)) → MetaAdjunction

In Proofgold the corresponding term root is 1ed388... and proposition id is fd4945...

Proof:
Proof not loaded.

Theorem. (MetaAdjunctionE)

MetaAdjunction → ∀p : prop, ((∀X, Obj X → comp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X)) → (∀Y, Obj' Y → comp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y)) → p) → p

In Proofgold the corresponding term root is 67ed42... and proposition id is e6292b...

Proof:
Proof not loaded.

Theorem. (MetaAdjunction_strict_I)

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 → MetaAdjunction_strict

In Proofgold the corresponding term root is 712520... and proposition id is d6aa5e...

Proof:
Proof not loaded.

Theorem. (MetaAdjunction_strict_E)

MetaAdjunction_strict → ∀p : prop, (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 → p) → p

In Proofgold the corresponding term root is 9a5dd9... and proposition id is 296719...

Proof:
Proof not loaded.

Theorem. (MetaAdjunctionMonad)

MetaFunctor 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 → MetaMonad 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)))

In Proofgold the corresponding term root is 19ca69... and proposition id is db40a9...

Proof:
Proof not loaded.

Theorem. (MetaAdjunctionMonad_strict)

MetaAdjunction_strict → MetaMonad_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)))

In Proofgold the corresponding term root is 8f71ab... and proposition id is 07be67...

Proof:
Proof not loaded.

End of Section MetaAdjunction

Beginning of Section MetaCatConcrete

Variable Obj : set → prop

Variable U : set → set

Variable Hom : set → set → set → prop

Theorem. (MetaCatConcrete)

(∀X Y f, Obj X → Obj Y → Hom X Y f → f ∈ U Y^{U X}) → (∀X, Obj X → Hom X X (lam_id (U X))) → (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → Hom 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)

In Proofgold the corresponding term root is 1db157... and proposition id is 081b4e...

Proof:
Proof not loaded.

Theorem. (MetaCatConcreteForgetful)

(∀X Y f, Obj X → Obj Y → Hom X Y f → f ∈ U Y^{U 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)

In Proofgold the corresponding term root is cb7abf... and proposition id is b606c5...

Proof:
Proof not loaded.

End of Section MetaCatConcrete

Theorem. (MetaCatSet)

MetaCat (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z g f ⇒ lam_comp X g f)

In Proofgold the corresponding term root is dcf573... and proposition id is e41257...

Proof:
Proof not loaded.

Theorem. (MetaCatHFSet)

MetaCat (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g))

In Proofgold the corresponding term root is 3e43f7... and proposition id is 2fb6ad...

Proof:
Proof not loaded.

Theorem. (MetaCatSmallSet)

MetaCat (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g))

In Proofgold the corresponding term root is ea08c8... and proposition id is 689787...

Proof:
Proof not loaded.

Theorem. (MetaCatConcreteForgetful_strict)

∀Obj : set → prop, ∀U : set → set, ∀Hom : set → set → set → prop, (∀X Y f, Obj X → Obj Y → Hom X Y f → f ∈ U Y^{U X}) → (∀X, Obj X → Hom X X (lam_id (U X))) → (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → Hom 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)

In Proofgold the corresponding term root is b158c7... and proposition id is ec1a3b...

Proof:
Proof not loaded.

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 set → set → set → prop.

In Proofgold the corresponding term root is d6f688... and object id is 0f5046...

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' ∧ ∀x ∈ X', f (uX x) = uY (f x))) of type set → set → set → prop.

In Proofgold the corresponding term root is 957911... and object id is 44b620...

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 y ∈ X', f (opX x y) = opY (f x) (f y))) of type set → set → set → prop.

In Proofgold the corresponding term root is e81578... and object id is 9b88c8...

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' ∧ ∀x ∈ X', pX x → pY (f x))) of type set → set → set → prop.

In Proofgold the corresponding term root is 5d0201... and object id is 8f474b...

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 y ∈ X', rX x y → rY (f x) (f y))) of type set → set → set → prop.

In Proofgold the corresponding term root is acf0f0... and object id is 3f6068...

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 : set → prop, (∀y, U y → y ∈ Y') → CY U → CX (λx ⇒ x ∈ X' ∧ U (f x)))) of type set → set → set → prop.

In Proofgold the corresponding term root is 9dfc2a... and object id is 4ebd3f...

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 y ∈ X', f (opX x y) = opY (f x) (f y)) ∧ (∀x y ∈ X', f (op2X x y) = op2Y (f x) (f y)) ∧ f eX = eY)) of type set → set → set → prop.

In Proofgold the corresponding term root is 070862... and object id is 26f87b...

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 y ∈ X', f (opX x y) = opY (f x) (f y)) ∧ (∀x y ∈ X', f (op2X x y) = op2Y (f x) (f y)) ∧ f eX = eY ∧ f e2X = e2Y)) of type set → set → set → prop.

In Proofgold the corresponding term root is a11d43... and object id is a8f5c0...

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 y ∈ X', f (opX x y) = opY (f x) (f y)) ∧ (∀x y ∈ X', f (op2X x y) = op2Y (f x) (f y)) ∧ (∀x y ∈ X', rX x y → rY (f x) (f y)) ∧ f eX = eY ∧ f e2X = e2Y)) of type set → set → set → prop.

In Proofgold the corresponding term root is d75651... and object id is a6f30d...

Theorem. (Hom_struct_e_pack)

∀X Y eX eY f, (Hom_struct_e (pack_e X eX) (pack_e Y eY) f) = (f ∈ Y^X ∧ f eX = eY)

In Proofgold the corresponding term root is 266cf3... and proposition id is f65a35...

Proof:
Proof not loaded.

Theorem. (Hom_struct_u_pack)

∀X Y, ∀opX opY : set → set, ∀f, (Hom_struct_u (pack_u X opX) (pack_u Y opY) f) = (f ∈ Y^X ∧ (∀x ∈ X, f (opX x) = opY (f x)))

In Proofgold the corresponding term root is c0506b... and proposition id is 66c4c4...

Proof:
Proof not loaded.

Theorem. (Hom_struct_b_pack)

∀X Y, ∀opX opY : set → set → set, ∀f, (Hom_struct_b (pack_b X opX) (pack_b Y opY) f) = (f ∈ Y^X ∧ (∀x y ∈ X, f (opX x y) = opY (f x) (f y)))

In Proofgold the corresponding term root is 7ee20a... and proposition id is 2cd8d7...

Proof:
Proof not loaded.

Theorem. (Hom_struct_p_pack)

∀X Y, ∀pX pY : set → prop, ∀f, (Hom_struct_p (pack_p X pX) (pack_p Y pY) f) = (f ∈ Y^X ∧ (∀x ∈ X, pX x → pY (f x)))

In Proofgold the corresponding term root is 63c01b... and proposition id is 55fb5e...

Proof:
Proof not loaded.

Theorem. (Hom_struct_r_pack)

∀X Y, ∀rX rY : set → set → prop, ∀f, (Hom_struct_r (pack_r X rX) (pack_r Y rY) f) = (f ∈ Y^X ∧ (∀x y ∈ X, rX x y → rY (f x) (f y)))

In Proofgold the corresponding term root is 4e4867... and proposition id is c84abf...

Proof:
Proof not loaded.

Theorem. (Hom_struct_c_pack)

∀X Y, ∀CX CY : (set → prop) → prop, ∀f, (Hom_struct_c (pack_c X CX) (pack_c Y CY) f) = (f ∈ Y^X ∧ (∀U : set → prop, (∀y, U y → y ∈ Y) → CY U → CX (λx ⇒ x ∈ X ∧ U (f x))))

In Proofgold the corresponding term root is 147946... and proposition id is 5059f2...

Proof:
Proof not loaded.

Theorem. (Hom_struct_b_b_e_pack)

∀X Y, ∀opX op2X opY op2Y : set → set → set, ∀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 ∈ Y^X ∧ (∀x y ∈ X, f (opX x y) = opY (f x) (f y)) ∧ (∀x y ∈ X, f (op2X x y) = op2Y (f x) (f y)) ∧ f eX = eY)

In Proofgold the corresponding term root is 10267d... and proposition id is 024cda...

Proof:
Proof not loaded.

Theorem. (Hom_struct_b_b_e_e_pack)

∀X Y, ∀opX op2X opY op2Y : set → set → set, ∀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 ∈ Y^X ∧ (∀x y ∈ X, f (opX x y) = opY (f x) (f y)) ∧ (∀x y ∈ X, f (op2X x y) = op2Y (f x) (f y)) ∧ f eX = eY ∧ f e2X = e2Y)

In Proofgold the corresponding term root is c390c3... and proposition id is 4ba5a3...

Proof:
Proof not loaded.

Theorem. (Hom_struct_b_b_r_e_e_pack)

∀X Y, ∀opX op2X opY op2Y : set → set → set, ∀rX rY : set → set → prop, ∀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 ∈ Y^X ∧ (∀x y ∈ X, f (opX x y) = opY (f x) (f y)) ∧ (∀x y ∈ X, f (op2X x y) = op2Y (f x) (f y)) ∧ (∀x y ∈ X, rX x y → rY (f x) (f y)) ∧ f eX = eY ∧ f e2X = e2Y)

In Proofgold the corresponding term root is 3b7da8... and proposition id is 3e8fcc...

Proof:
Proof not loaded.

Beginning of Section MetaCatStruct

Variable Obj : set → prop

Theorem. (MetaCat_struct_e_gen)

(∀X, Obj X → struct_e X) → MetaCat Obj Hom_struct_e (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)

In Proofgold the corresponding term root is f2377b... and proposition id is 1c0e13...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_e_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is 7938f4... and proposition id is 0f4ef6...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_p_gen)

(∀X, Obj X → struct_p X) → MetaCat Obj Hom_struct_p (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)

In Proofgold the corresponding term root is 8e7946... and proposition id is 5387a7...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_p_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is 59e3f3... and proposition id is 57ba03...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_r_gen)

(∀X, Obj X → struct_r X) → MetaCat Obj Hom_struct_r (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)

In Proofgold the corresponding term root is cbfb7b... and proposition id is 626580...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_r_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is 8faf0f... and proposition id is 45945b...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_u_gen)

(∀X, Obj X → struct_u X) → MetaCat Obj Hom_struct_u (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)

In Proofgold the corresponding term root is 137f84... and proposition id is 7ce95d...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_u_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is 6809a8... and proposition id is 6eadb3...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_b_gen)

(∀X, Obj X → struct_b X) → MetaCat Obj Hom_struct_b (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)

In Proofgold the corresponding term root is be2503... and proposition id is 125f16...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_b_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is 5ef6db... and proposition id is 79957c...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_c_gen)

(∀X, Obj X → struct_c X) → MetaCat Obj Hom_struct_c (λX ⇒ lam_id (X 0)) (λX Y Z g f ⇒ lam_comp (X 0) g f)

In Proofgold the corresponding term root is a1cc13... and proposition id is dd75cc...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_c_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is c43bbf... and proposition id is 58a40d...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_b_b_e_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is c7aff8... and proposition id is 5f5c51...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_b_b_e_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is f8aa78... and proposition id is 9c6b91...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_b_b_e_e_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is d57683... and proposition id is 936d91...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_b_b_e_e_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is 45b449... and proposition id is 72690d...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_b_b_r_e_e_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is d69e51... and proposition id is dc6cf0...

Proof:
Proof not loaded.

Theorem. (MetaCat_struct_b_b_r_e_e_Forgetful_gen)

(∀X, Obj X → struct_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)

In Proofgold the corresponding term root is de2d15... and proposition id is 49006a...

Proof:
Proof not loaded.

End of Section MetaCatStruct