Proposition. (MetaCatSet_coequalizer_gen)
∀Obj : set → prop, (∀X, Obj X → ∀Q ⊆ X, Obj Q) → ∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) quot canonmap fac
In Proofgold the corresponding term root is fbab5c... and proposition id is 5bbc15...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_coequalizer)
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) quot canonmap fac
In Proofgold the corresponding term root is e96f8c... and proposition id is 330460...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatHFSet_coequalizer)
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) quot canonmap fac
In Proofgold the corresponding term root is ecf041... and proposition id is ef69d0...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSmallSet_coequalizer)
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) quot canonmap fac
In Proofgold the corresponding term root is 6f1bce... and proposition id is 049917...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_equalizer_gen)
∀Obj : set → prop, (∀X, Obj X → ∀Q ⊆ X, Obj Q) → ∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_p Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) quot canonmap fac
In Proofgold the corresponding term root is ddd882... and proposition id is ae25cd...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatHFSet_equalizer_gen)
∀Obj : set → prop, (∀X, Obj X → ∀Q ⊆ X, Obj Q) → ∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_p (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) quot canonmap fac
In Proofgold the corresponding term root is 418e35... and proposition id is 037068...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSmallSet_equalizer_gen)
∀Obj : set → prop, (∀X, Obj X → ∀Q ⊆ X, Obj Q) → ∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_p (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) quot canonmap fac
In Proofgold the corresponding term root is 01368d... and proposition id is 3d3ca0...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_pullback_gen)
∀Obj : set → prop, MetaCat Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) → (∀X, Obj X → ∀Q ⊆ X, Obj Q) → (∀X, Obj X → ∀Y, Obj Y → Obj (setprod X Y)) → ∃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 SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) pb pi0 pi1 pair
In Proofgold the corresponding term root is a58587... and proposition id is a53be4...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_pullback)
∃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 (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) pb pi0 pi1 pair
In Proofgold the corresponding term root is 9e7eef... and proposition id is fcaeef...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatHFSet_pullback)
∃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 (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) pb pi0 pi1 pair
In Proofgold the corresponding term root is a3e374... and proposition id is 2e08de...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSmallSet_pullback)
∃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 (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) pb pi0 pi1 pair
In Proofgold the corresponding term root is 361c48... and proposition id is 596e35...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_pushout_gen)
∀Obj : set → prop, MetaCat Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) → (∀X, Obj X → ∀Q ⊆ X, Obj Q) → (∀X, Obj X → ∀Y, Obj Y → Obj (setsum X Y)) → ∃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 SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) po i0 i1 copair
In Proofgold the corresponding term root is 29a640... and proposition id is 8381c7...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_pushout)
∃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 (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) po i0 i1 copair
In Proofgold the corresponding term root is 90aa49... and proposition id is 156182...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatHFSet_pushout)
∃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 (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) po i0 i1 copair
In Proofgold the corresponding term root is 3eb6cc... and proposition id is bfc422...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSmallSet_pushout)
∃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 (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) po i0 i1 copair
In Proofgold the corresponding term root is 4222d5... and proposition id is b3083e...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_product_exponent_gen_setprod_setexp)
∀Obj : set → prop, (∀X, Obj X → ∀Y, Obj Y → Obj (setprod X Y)) → (∀X, Obj X → ∀Y, Obj Y → Obj (YX)) → product_exponent_constr_p Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) setprod (λX Y ⇒ (λz ∈ X ⨯ Y ⇒ z 0)) (λX Y ⇒ (λz ∈ X ⨯ Y ⇒ z 1)) (λX Y W h k ⇒ (λw ∈ W ⇒ (h w,k w))) (λX Y ⇒ YX) (λX Y ⇒ (λfx ∈ (YX) ⨯ X ⇒ fx 0 (fx 1))) (λX Y W f ⇒ (λw ∈ W ⇒ λx ∈ X ⇒ f (w,x)))
In Proofgold the corresponding term root is f79156... and proposition id is 37ab03...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_product_exponent_gen)
∀Obj : set → prop, (∀X, Obj X → ∀Y, Obj Y → Obj (setprod X Y)) → (∀X, Obj X → ∀Y, Obj Y → Obj (YX)) → ∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, ∃exp : set → set → set, ∃a : set → set → set, ∃lm : set → set → set → set → set, product_exponent_constr_p Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) prod pi0 pi1 pair exp a lm
In Proofgold the corresponding term root is d378b2... and proposition id is 32b3d6...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_product_exponent)
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, ∃exp : set → set → set, ∃a : set → set → set, ∃lm : set → set → set → set → set, product_exponent_constr_p (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) prod pi0 pi1 pair exp a lm
In Proofgold the corresponding term root is 72326f... and proposition id is 1810cf...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatHFSet_product_exponent)
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, ∃exp : set → set → set, ∃a : set → set → set, ∃lm : set → set → set → set → set, product_exponent_constr_p (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) prod pi0 pi1 pair exp a lm
In Proofgold the corresponding term root is b7e68e... and proposition id is 29786e...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_monic_inj_gen)
∀Obj : set → prop, ∀X Y, ∀f : set, monic Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) X Y f → ∀u v ∈ X, f u = f v → u = v
In Proofgold the corresponding term root is 682652... and proposition id is 5b8590...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_subobject_classifier_gen)
∀Obj : set → prop, Obj 1 → Obj 2 → subobject_classifier_p Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) 1 (λX : set ⇒ (λx ∈ X ⇒ 0)) 2 (λ_ ∈ 1 ⇒ 1) (λX Y : set ⇒ λm : set ⇒ (λy ∈ Y ⇒ if (∃x ∈ X, m x = y) then 1 else 0)) (λX Y : set ⇒ λm : set ⇒ λW : set ⇒ λh k : set ⇒ (λw ∈ W ⇒ inv X (λx ⇒ m x) (k w)))
In Proofgold the corresponding term root is 37ccac... and proposition id is bd9cda...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_subobject_classifier_gen_ex)
∀Obj : set → prop, Obj 1 → Obj 2 → ∃one : set, ∃uniqa : set → set, ∃Omega : set, ∃tru : set, ∃ch : set → set → set → set, ∃constr : set → set → set → set → set → set → set, subobject_classifier_p Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) one uniqa Omega tru ch constr
In Proofgold the corresponding term root is b1a3c9... and proposition id is e5b470...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_subobject_classifier)
∃one : set, ∃uniqa : set → set, ∃Omega : set, ∃tru : set, ∃ch : set → set → set → set, ∃constr : set → set → set → set → set → set → set, subobject_classifier_p (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) one uniqa Omega tru ch constr
In Proofgold the corresponding term root is 2f3ca6... and proposition id is 25c261...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatHFSet_subobject_classifier)
∃one : set, ∃uniqa : set → set, ∃Omega : set, ∃tru : set, ∃ch : set → set → set → set, ∃constr : set → set → set → set → set → set → set, subobject_classifier_p (λX ⇒ X ∈ UnivOf Empty) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) one uniqa Omega tru ch constr
In Proofgold the corresponding term root is 4f5685... and proposition id is 341a1e...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSmallSet_subobject_classifier)
∃one : set, ∃uniqa : set → set, ∃Omega : set, ∃tru : set, ∃ch : set → set → set → set, ∃constr : set → set → set → set → set → set → set, subobject_classifier_p (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) one uniqa Omega tru ch constr
In Proofgold the corresponding term root is 368ed5... and proposition id is 7223ac...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_nno_gen)
∀Obj : set → prop, Obj 1 → Obj omega → nno_p Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) 1 (λX : set ⇒ (λx ∈ X ⇒ 0)) omega (λ_ ∈ 1 ⇒ 0) (λn ∈ omega ⇒ ordsucc n) (λX : set ⇒ λx f : set ⇒ (λn ∈ omega ⇒ nat_primrec (x 0) (λ_ v ⇒ f v) n))
In Proofgold the corresponding term root is b6c627... and proposition id is ea037f...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_nno_gen_ex)
∀Obj : set → prop, Obj 1 → Obj omega → ∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p Obj SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) one uniqa N zer suc rec
In Proofgold the corresponding term root is 39316c... and proposition id is 1051b9...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSet_nno)
∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) one uniqa N zer suc rec
In Proofgold the corresponding term root is 2297b4... and proposition id is 0e5634...
Proof:
The rest of the proof is missing.

Proposition. (MetaCatSmallSet_nno)
∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p (λX ⇒ X ∈ UnivOf (UnivOf Empty)) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ lam_comp X f g) one uniqa N zer suc rec
In Proofgold the corresponding term root is 1603ee... and proposition id is 833b6b...
Proof:
The rest of the proof is missing.