Definition. We define struct_c_T1_topology to be λX ⇒ struct_c X ∧ unpack_c_o X (λX' Open ⇒ Open (λx ⇒ x ∈ X') ∧ (∀U V : set → prop, Open U → Open V → Open (λx ⇒ U x ∧ U x)) ∧ (∀C : (set → prop) → prop, (∀U : set → prop, C U → Open U) → Open (λx ⇒ ∃U : set → prop, C U ∧ U x)) ∧ (∀a b ∈ X', a ≠ b → ∃U : set → prop, Open U ∧ exactly1of2 (U a) (U b))) of type set → prop.
In Proofgold the corresponding term root is e0b6a5... and object id is a585fa...
Theorem. (MetaCat_struct_c_T1_topology)
MetaCat struct_c_T1_topology Hom_struct_c struct_id struct_comp
In Proofgold the corresponding term root is 0414e9... and proposition id is 4f8053...
Proof:
We prove the intermediate claim L1: ∀X, struct_c_T1_topology X → struct_c X.
Let X be given.
Assume HX.
Apply HX to the current goal.
Assume H _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is MetaCat_struct_c_gen struct_c_T1_topology L1.
∎
Theorem. (MetaCat_struct_c_T1_topology_Forgetful)
MetaFunctor struct_c_T1_topology Hom_struct_c struct_id struct_comp (λ_ ⇒ 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 3f0ca0... and proposition id is 2136f6...
Proof:
We prove the intermediate claim L1: ∀X, struct_c_T1_topology X → struct_c X.
Let X be given.
Assume HX.
Apply HX to the current goal.
Assume H _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is MetaCat_struct_c_Forgetful_gen struct_c_T1_topology L1.
∎
Proposition. (MetaCat_struct_c_T1_topology_initial)
∃Y : set, ∃uniqa : set → set, initial_p struct_c_T1_topology Hom_struct_c struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is 3cbf3e... and proposition id is 0f1048...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_terminal)
∃Y : set, ∃uniqa : set → set, terminal_p struct_c_T1_topology Hom_struct_c struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is 9f97ff... and proposition id is b43a8f...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_coproduct_constr)
∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p struct_c_T1_topology Hom_struct_c struct_id struct_comp coprod i0 i1 copair
In Proofgold the corresponding term root is 4b0bb6... and proposition id is 06f53a...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_product_constr)
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p struct_c_T1_topology Hom_struct_c struct_id struct_comp prod pi0 pi1 pair
In Proofgold the corresponding term root is 5764cf... and proposition id is 2981a7...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_coequalizer_constr)
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p struct_c_T1_topology Hom_struct_c struct_id struct_comp quot canonmap fac
In Proofgold the corresponding term root is e25a2e... and proposition id is bad2fc...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_equalizer_constr)
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_p struct_c_T1_topology Hom_struct_c struct_id struct_comp quot canonmap fac
In Proofgold the corresponding term root is a29b62... and proposition id is 3bbfb5...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_pushout_constr)
∃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 struct_c_T1_topology Hom_struct_c struct_id struct_comp po i0 i1 copair
In Proofgold the corresponding term root is 093d56... and proposition id is ad30de...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_pullback_constr)
∃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 struct_c_T1_topology Hom_struct_c struct_id struct_comp pb pi0 pi1 pair
In Proofgold the corresponding term root is 0ea4c1... and proposition id is fec4ca...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_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 struct_c_T1_topology Hom_struct_c struct_id struct_comp prod pi0 pi1 pair exp a lm
In Proofgold the corresponding term root is 0b2a22... and proposition id is 485ba0...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_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 struct_c_T1_topology Hom_struct_c struct_id struct_comp one uniqa Omega tru ch constr
In Proofgold the corresponding term root is 4ee08d... and proposition id is 9e065c...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_nno)
∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_c_T1_topology Hom_struct_c struct_id struct_comp one uniqa N zer suc rec
In Proofgold the corresponding term root is b508a0... and proposition id is 74694d...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_c_T1_topology_left_adjoint_forgetful)
∃F0 : set → set, ∃F1 : set → set → set → set, ∃eta eps : set → set, MetaAdjunction_strict (λ_ ⇒ True) SetHom (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_c_T1_topology Hom_struct_c struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps
In Proofgold the corresponding term root is 88973d... and proposition id is ed0798...
Proof:
The rest of the proof is missing.