Proofgold Address

Param MetaAdjunction_strict^{MetaAdjunction_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition MetaCat_initial_p^initial_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . and (x0 x4) (∀ x6 . x0 x6 ⟶ and (x1 x4 x6 (x5 x6)) (∀ x7 . x1 x4 x6 x7 ⟶ x7 = x5 x6))
Param MetaFunctor_strict^{MetaFunctor_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → ο
Param MetaFunctor^MetaFunctor : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → ο
Param MetaNatTrans^MetaNatTrans : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → ο
Param MetaAdjunction^{MetaAdjunction} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Known 29671..^{MetaAdjunction_strict_E} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaAdjunction_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . (MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11 ⟶ MetaNatTrans x0 x1 x2 x3 x0 x1 x2 x3 (λ x15 . x15) (λ x15 x16 x17 . x17) (λ x15 . x10 (x8 x15)) (λ x15 x16 x17 . x11 (x8 x15) (x8 x16) (x9 x15 x16 x17)) x12 ⟶ MetaNatTrans x4 x5 x6 x7 x4 x5 x6 x7 (λ x15 . x8 (x10 x15)) (λ x15 x16 x17 . x9 (x10 x15) (x10 x16) (x11 x15 x16 x17)) (λ x15 . x15) (λ x15 x16 x17 . x17) x13 ⟶ MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ x14) ⟶ x14
Known e6292..^{MetaAdjunctionE} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . ((∀ x15 . x0 x15 ⟶ x7 (x8 x15) (x8 (x10 (x8 x15))) (x8 x15) (x13 (x8 x15)) (x9 x15 (x10 (x8 x15)) (x12 x15)) = x6 (x8 x15)) ⟶ (∀ x15 . x4 x15 ⟶ x3 (x10 x15) (x10 (x8 (x10 x15))) (x10 x15) (x11 (x8 (x10 x15)) x15 (x13 x15)) (x12 (x10 x15)) = x2 (x10 x15)) ⟶ x14) ⟶ x14
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known 95305..^{MetaFunctor_strict_E} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ ∀ x10 : ο . (MetaCat x0 x1 x2 x3 ⟶ MetaCat x4 x5 x6 x7 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ x10) ⟶ x10
Param MetaFunctor_prop1^idT : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Definition MetaFunctor_prop2^compT := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 x7 x8 . x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x1 x4 x5 x7 ⟶ x1 x5 x6 x8 ⟶ x1 x4 x6 (x3 x4 x5 x6 x8 x7)
Known 7da4b..^MetaCat_E : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ ∀ x4 : ο . (MetaFunctor_prop1 x0 x1 x2 x3 ⟶ MetaFunctor_prop2 x0 x1 x2 x3 ⟶ (∀ x5 x6 x7 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 x6 x7 ⟶ x3 x5 x5 x6 x7 (x2 x5) = x7) ⟶ (∀ x5 x6 x7 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 x6 x7 ⟶ x3 x5 x6 x6 (x2 x6) x7 = x7) ⟶ (∀ x5 x6 x7 x8 x9 x10 x11 . x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x5 x6 x9 ⟶ x1 x6 x7 x10 ⟶ x1 x7 x8 x11 ⟶ x3 x5 x6 x8 (x3 x6 x7 x8 x11 x10) x9 = x3 x5 x7 x8 x11 (x3 x5 x6 x7 x10 x9)) ⟶ x4) ⟶ x4
Known 973e2..^MetaFunctorE : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ ∀ x10 : ο . ((∀ x11 . x0 x11 ⟶ x4 (x8 x11)) ⟶ (∀ x11 x12 x13 . x0 x11 ⟶ x0 x12 ⟶ x1 x11 x12 x13 ⟶ x5 (x8 x11) (x8 x12) (x9 x11 x12 x13)) ⟶ (∀ x11 . x0 x11 ⟶ x9 x11 x11 (x2 x11) = x6 (x8 x11)) ⟶ (∀ x11 x12 x13 x14 x15 . x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x1 x11 x12 x14 ⟶ x1 x12 x13 x15 ⟶ x9 x11 x13 (x3 x11 x12 x13 x15 x14) = x7 (x8 x11) (x8 x12) (x8 x13) (x9 x12 x13 x15) (x9 x11 x12 x14)) ⟶ x10) ⟶ x10
Known aa53a..^{MetaNatTransE} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ ∀ x13 : ο . ((∀ x14 . x0 x14 ⟶ x5 (x8 x14) (x10 x14) (x12 x14)) ⟶ (∀ x14 x15 x16 . x0 x14 ⟶ x0 x15 ⟶ x1 x14 x15 x16 ⟶ x7 (x8 x14) (x10 x14) (x10 x15) (x11 x14 x15 x16) (x12 x14) = x7 (x8 x14) (x8 x15) (x10 x15) (x12 x15) (x9 x14 x15 x16)) ⟶ x13) ⟶ x13
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Param pack_p^pack_p : ι → (ι → ο) → ι
Definition struct_p^struct_p := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . x1 (pack_p x2 x3)) ⟶ x1 x0
Param UnaryPredHom^Hom_struct_p : ι → ι → ι → ο
Param lam^Sigma : ι → (ι → ι) → ι
Definition lam_id^lam_id := λ x0 . lam x0 (λ x1 . x1)
Param ap^ap : ι → ι → ι
Definition struct_id^struct_id := λ x0 . lam_id (ap x0 0)
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition struct_comp^struct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Known caa5e..^{MetaCat_struct_p} : MetaCat struct_p UnaryPredHom struct_id struct_comp
Definition True^True := ∀ x0 : ο . x0 ⟶ x0
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Definition HomSet^SetHom := λ x0 x1 x2 . x2 ∈ setexp x1 x0
Known 40bbd..^{MetaCat_struct_p_Forgetful} : MetaFunctor struct_p UnaryPredHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Definition False^False := ∀ x0 : ο . x0
Known pack_struct_p_I^{pack_struct_p_I} : ∀ x0 . ∀ x1 : ι → ο . struct_p (pack_p x0 x1)
Known 55fb5..^{Hom_struct_p_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 . UnaryPredHom (pack_p x0 x2) (pack_p x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ x2 x6 ⟶ x3 (ap x4 x6))
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Definition MetaCat_terminal_p^terminal_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . and (x0 x4) (∀ x6 . x0 x6 ⟶ and (x1 x6 x4 (x5 x6)) (∀ x7 . x1 x6 x4 x7 ⟶ x7 = x5 x6))
Param ordsucc^ordsucc : ι → ι
Known pack_p_0_eq2^pack_p_0_eq2 : ∀ x0 . ∀ x1 : ι → ο . x0 = ap (pack_p x0 x1) 0
Known In_0_1^In_0_1 : 0 ∈ 1
Known TrueI^TrueI : True
Param Sing^Sing : ι → ι
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known eq_1_Sing0^eq_1_Sing0 : 1 = Sing 0
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known d6aa5..^{MetaAdjunction_strict_I} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11 ⟶ MetaNatTrans x0 x1 x2 x3 x0 x1 x2 x3 (λ x14 . x14) (λ x14 x15 x16 . x16) (λ x14 . x10 (x8 x14)) (λ x14 x15 x16 . x11 (x8 x14) (x8 x15) (x9 x14 x15 x16)) x12 ⟶ MetaNatTrans x4 x5 x6 x7 x4 x5 x6 x7 (λ x14 . x8 (x10 x14)) (λ x14 x15 x16 . x9 (x10 x14) (x10 x15) (x11 x14 x15 x16)) (λ x14 . x14) (λ x14 x15 x16 . x16) x13 ⟶ MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ MetaAdjunction_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
Known 5cbb4..^{MetaFunctor_strict_I} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ MetaCat x4 x5 x6 x7 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
Known e4125..^MetaCatSet : MetaCat (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Known 2cb62..^MetaFunctorI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . (∀ x10 . x0 x10 ⟶ x4 (x8 x10)) ⟶ (∀ x10 x11 x12 . x0 x10 ⟶ x0 x11 ⟶ x1 x10 x11 x12 ⟶ x5 (x8 x10) (x8 x11) (x9 x10 x11 x12)) ⟶ (∀ x10 . x0 x10 ⟶ x9 x10 x10 (x2 x10) = x6 (x8 x10)) ⟶ (∀ x10 x11 x12 x13 x14 . x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x1 x10 x11 x13 ⟶ x1 x11 x12 x14 ⟶ x9 x10 x12 (x3 x10 x11 x12 x14 x13) = x7 (x8 x10) (x8 x11) (x8 x12) (x9 x11 x12 x14) (x9 x10 x11 x13)) ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
Known c1d68..^{MetaNatTransI} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . (∀ x13 . x0 x13 ⟶ x5 (x8 x13) (x10 x13) (x12 x13)) ⟶ (∀ x13 x14 x15 . x0 x13 ⟶ x0 x14 ⟶ x1 x13 x14 x15 ⟶ x7 (x8 x13) (x10 x13) (x10 x14) (x11 x13 x14 x15) (x12 x13) = x7 (x8 x13) (x8 x14) (x10 x14) (x12 x14) (x9 x13 x14 x15)) ⟶ MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12
Known lam_id_exp_In^{lam_id_exp_In} : ∀ x0 . lam_id x0 ∈ setexp x0 x0
Known lam_comp_id_R^{lam_comp_id_R} : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ lam_comp x0 x2 (lam_id x0) = x2
Known lam_comp_id_L^{lam_comp_id_L} : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ lam_comp x0 (lam_id x1) x2 = x2
Known fd494..^{MetaAdjunctionI} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . (∀ x14 . x0 x14 ⟶ x7 (x8 x14) (x8 (x10 (x8 x14))) (x8 x14) (x13 (x8 x14)) (x9 x14 (x10 (x8 x14)) (x12 x14)) = x6 (x8 x14)) ⟶ (∀ x14 . x4 x14 ⟶ x3 (x10 x14) (x10 (x8 (x10 x14))) (x10 x14) (x11 (x8 (x10 x14)) x14 (x13 x14)) (x12 (x10 x14)) = x2 (x10 x14)) ⟶ MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
Param unpack_p_o^unpack_p_o : ι → (ι → (ι → ο) → ο) → ο
Definition PtdPred^{struct_p_nonempty} := λ x0 . and (struct_p x0) (unpack_p_o x0 (λ x1 . λ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x2 x4) ⟶ x3) ⟶ x3))
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known unpack_p_o_eq^{unpack_p_o_eq} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ο . (∀ x3 : ι → ο . (∀ x4 . x4 ∈ x1 ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_p_o (pack_p x1 x2) x0 = x0 x1 x2
Known aef2e..^{MetaCat_struct_p_nonempty} : MetaCat PtdPred UnaryPredHom struct_id struct_comp
Known 0322a..^{MetaCat_struct_p_nonempty_Forgetful} : MetaFunctor PtdPred UnaryPredHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known In_1_2^In_1_2 : 1 ∈ 2
Known In_0_2^In_0_2 : 0 ∈ 2
Known 80cab..^{MetaCatSet_initial} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p (λ x4 . True) HomSet (λ x4 . lam x4 (λ x5 . x5)) (λ x4 x5 x6 x7 x8 . lam x4 (λ x9 . ap x7 (ap x8 x9))) x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param pack_e^pack_e : ι → ι → ι
Definition struct_e^struct_e := λ x0 . ∀ x1 : ι → ο . (∀ x2 x3 . x3 ∈ x2 ⟶ x1 (pack_e x2 x3)) ⟶ x1 x0
Param PtdSetHom^Hom_struct_e : ι → ι → ι → ο
Param unpack_e_i^unpack_e_i : ι → CT2 ι
Known unpack_e_i_eq^{unpack_e_i_eq} : ∀ x0 : ι → ι → ι . ∀ x1 x2 . unpack_e_i (pack_e x1 x2) x0 = x0 x1 x2
Known f65a3..^{Hom_struct_e_pack} : ∀ x0 x1 x2 x3 x4 . PtdSetHom (pack_e x0 x2) (pack_e x1 x3) x4 = and (x4 ∈ setexp x1 x0) (ap x4 x2 = x3)
Known pack_e_0_eq2^pack_e_0_eq2 : ∀ x0 x1 . x0 = ap (pack_e x0 x1) 0
Param pack_r^pack_r : ι → (ι → ι → ο) → ι
Definition struct_r^struct_r := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x1 (pack_r x2 x3)) ⟶ x1 x0
Param BinRelnHom^Hom_struct_r : ι → ι → ι → ο
Known 6955f..^{MetaCat_struct_r} : MetaCat struct_r BinRelnHom struct_id struct_comp
Known 07626..^{MetaCat_struct_r_Forgetful} : MetaFunctor struct_r BinRelnHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Known pack_struct_r_I^{pack_struct_r_I} : ∀ x0 . ∀ x1 : ι → ι → ο . struct_r (pack_r x0 x1)
Known c84ab..^{Hom_struct_r_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . BinRelnHom (pack_r x0 x2) (pack_r x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x2 x6 x7 ⟶ x3 (ap x4 x6) (ap x4 x7))
Known pack_r_0_eq2^pack_r_0_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . x2 x0 (ap (pack_r x0 x1) 0) ⟶ x2 (ap (pack_r x0 x1) 0) x0
Param unpack_r_o^unpack_r_o : ι → (ι → (ι → ι → ο) → ο) → ο
Definition PER^struct_r_per := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)))
Known unpack_r_o_eq^{unpack_r_o_eq} : ∀ x0 : ι → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_r_o (pack_r x1 x2) x0 = x0 x1 x2
Known 259fb..^{MetaCat_struct_r_per} : MetaCat PER BinRelnHom struct_id struct_comp
Known 1b780..^{MetaCat_struct_r_per_Forgetful} : MetaFunctor PER BinRelnHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Definition EquivReln^{struct_r_equivreln} := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (and (∀ x3 . x3 ∈ x1 ⟶ x2 x3 x3) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)))
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known ca919..^{MetaCat_struct_r_equivreln} : MetaCat EquivReln BinRelnHom struct_id struct_comp
Known a8025..^{MetaCat_struct_r_equivreln_Forgetful} : MetaFunctor EquivReln BinRelnHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Definition IrreflexiveTransitiveReln^{struct_r_partialord} := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)))
Known c6620..^{MetaCat_struct_r_partialord} : MetaCat IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp
Known c7aa1..^{MetaCat_struct_r_partialord_Forgetful} : MetaFunctor IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Definition IrreflexiveSymmetricReln^{struct_r_graph} := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3)))
Known 71675..^{MetaCat_struct_r_graph} : MetaCat IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp
Known 1299d..^{MetaCat_struct_r_graph_Forgetful} : MetaFunctor IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Param pack_c^pack_c : ι → ((ι → ο) → ο) → ι
Definition struct_c^struct_c := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . x1 (pack_c x2 x3)) ⟶ x1 x0
Param PreContinuousHom^Hom_struct_c : ι → ι → ι → ο
Known ed6b5..^{MetaCat_struct_c} : MetaCat struct_c PreContinuousHom struct_id struct_comp
Known 803c1..^{MetaCat_struct_c_Forgetful} : MetaFunctor struct_c PreContinuousHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Known pack_struct_c_I^{pack_struct_c_I} : ∀ x0 . ∀ x1 : (ι → ο) → ο . struct_c (pack_c x0 x1)
Known pack_c_0_eq2^pack_c_0_eq2 : ∀ x0 . ∀ x1 : (ι → ο) → ο . x0 = ap (pack_c x0 x1) 0
Known 5059f..^{Hom_struct_c_pack} : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 . PreContinuousHom (pack_c x0 x2) (pack_c x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ x7 ∈ x1) ⟶ x3 x6 ⟶ x2 (λ x7 . and (x7 ∈ x0) (x6 (ap x4 x7))))
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition 90aea..^struct_r_ord := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ or (x2 x3 x4) (x2 x4 x3))) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)))
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem daa87.. : ∀ x0 . ∀ x1 : ι → ι → ο . unpack_r_o (pack_r x0 x1) (λ x3 . λ x4 : ι → ι → ο . and (and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ or (x4 x5 x6) (x4 x6 x5))) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x7 ⟶ x4 x5 x7)) = and (and (∀ x3 . x3 ∈ x0 ⟶ not (x1 x3 x3)) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ or (x1 x3 x4) (x1 x4 x3))) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x3 x4 ⟶ x1 x4 x5 ⟶ x1 x3 x5) (proof)
Theorem b8e11.. : ∀ x0 . ∀ x1 : ι → ι → ο . x0 = 0 ⟶ 90aea.. (pack_r x0 x1) (proof)
Known Empty_eq^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Theorem c0e29.. : ∀ x0 . 90aea.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x2 = 0 ⟶ x1 (pack_r x2 x3)) ⟶ x1 x0 (proof)
Param setsum^setsum : ι → ι → ι
Known lamE^lamE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x1 x4) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Param pair_p^pair_p : ι → ο
Known PiI^PiI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . x3 ∈ x2 ⟶ and (pair_p x3) (ap x3 0 ∈ x0)) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3) ⟶ x2 ∈ Pi x0 x1
Theorem b891d.. : ∀ x0 x1 x2 . 90aea.. x0 ⟶ 90aea.. x1 ⟶ BinRelnHom x0 x1 x2 = (x2 = 0) (proof)
Theorem d7052.. : ∀ x0 x1 x2 . 90aea.. x0 ⟶ 90aea.. x1 ⟶ x2 = 0 ⟶ BinRelnHom x0 x1 x2 (proof)
Theorem be0ef.. : ∀ x0 x1 . 90aea.. x0 ⟶ 90aea.. x1 ⟶ BinRelnHom x0 x1 0 (proof)
Theorem 6632f.. : ∀ x0 x1 x2 . 90aea.. x0 ⟶ 90aea.. x1 ⟶ BinRelnHom x0 x1 x2 ⟶ x2 = 0 (proof)
Theorem caa7a.. : ∀ x0 x1 x2 x3 . 90aea.. x0 ⟶ 90aea.. x1 ⟶ BinRelnHom x0 x1 x2 ⟶ BinRelnHom x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 9a5dc.. : ∀ x0 x1 x2 x3 x4 . 90aea.. x0 ⟶ struct_comp x0 x1 x2 x3 x4 = 0 (proof)
Theorem a206e.. : 90aea.. (pack_r 0 (λ x0 x1 . False)) (proof)
Theorem adce2..^{MetaCat_struct_r_ord_initial} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem dd155.. : MetaCat_terminal_p 90aea.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x0 x1 . False)) (λ x0 . 0) (proof)
Theorem 18ea9..^{MetaCat_struct_r_ord_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_coproduct_p^coproduct_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (∀ x10 . x0 x10 ⟶ ∀ x11 x12 . x1 x4 x10 x11 ⟶ x1 x5 x10 x12 ⟶ and (and (and (x1 x6 x10 (x9 x10 x11 x12)) (x3 x4 x6 x10 (x9 x10 x11 x12) x7 = x11)) (x3 x5 x6 x10 (x9 x10 x11 x12) x8 = x12)) (∀ x13 . x1 x6 x10 x13 ⟶ x3 x4 x6 x10 x13 x7 = x11 ⟶ x3 x5 x6 x10 x13 x8 = x12 ⟶ x13 = x9 x10 x11 x12))
Definition MetaCat_coproduct_constr_p^{coproduct_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 x9 . x0 x8 ⟶ x0 x9 ⟶ MetaCat_coproduct_p x0 x1 x2 x3 x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9)
Known and6I^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem ebfe1..^{MetaCat_struct_r_ord_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_product_p^product_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x6 x4 x7)) (x1 x6 x5 x8)) (∀ x10 . x0 x10 ⟶ ∀ x11 x12 . x1 x10 x4 x11 ⟶ x1 x10 x5 x12 ⟶ and (and (and (x1 x10 x6 (x9 x10 x11 x12)) (x3 x10 x6 x4 x7 (x9 x10 x11 x12) = x11)) (x3 x10 x6 x5 x8 (x9 x10 x11 x12) = x12)) (∀ x13 . x1 x10 x6 x13 ⟶ x3 x10 x6 x4 x7 x13 = x11 ⟶ x3 x10 x6 x5 x8 x13 = x12 ⟶ x13 = x9 x10 x11 x12))
Definition MetaCat_product_constr_p^{product_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 x9 . x0 x8 ⟶ x0 x9 ⟶ MetaCat_product_p x0 x1 x2 x3 x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9)
Theorem 06552.. : MetaCat_product_constr_p 90aea.. BinRelnHom struct_id struct_comp (λ x0 x1 . pack_r 0 (λ x2 x3 . False)) (λ x0 x1 . 0) (λ x0 x1 . 0) (λ x0 x1 x2 x3 x4 . 0) (proof)
Theorem e28a3..^{MetaCat_struct_r_ord_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_coequalizer_p^{coequalizer_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x5 x8 x9)) (x3 x4 x5 x8 x9 x6 = x3 x4 x5 x8 x9 x7)) (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x5 x11 x12 ⟶ x3 x4 x5 x11 x12 x6 = x3 x4 x5 x11 x12 x7 ⟶ and (and (x1 x8 x11 (x10 x11 x12)) (x3 x5 x8 x11 (x10 x11 x12) x9 = x12)) (∀ x13 . x1 x8 x11 x13 ⟶ x3 x5 x8 x11 x13 x9 = x12 ⟶ x13 = x10 x11 x12))
Definition MetaCat_coequalizer_struct_p^{coequalizer_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 : ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 x8 . x0 x7 ⟶ x0 x8 ⟶ ∀ x9 x10 . x1 x7 x8 x9 ⟶ x1 x7 x8 x10 ⟶ MetaCat_coequalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
Known 41253..^and8I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7
Theorem df039..^{MetaCat_struct_r_ord_coequalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_equalizer_p^equalizer_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x8 x4 x9)) (x3 x8 x4 x5 x6 x9 = x3 x8 x4 x5 x7 x9)) (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x11 x4 x12 ⟶ x3 x11 x4 x5 x6 x12 = x3 x11 x4 x5 x7 x12 ⟶ and (and (x1 x11 x8 (x10 x11 x12)) (x3 x11 x8 x4 x9 (x10 x11 x12) = x12)) (∀ x13 . x1 x11 x8 x13 ⟶ x3 x11 x8 x4 x9 x13 = x12 ⟶ x13 = x10 x11 x12))
Definition MetaCat_equalizer_struct_p^{equalizer_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 : ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 x8 . x0 x7 ⟶ x0 x8 ⟶ ∀ x9 x10 . x1 x7 x8 x9 ⟶ x1 x7 x8 x10 ⟶ MetaCat_equalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
Theorem 788ee..^{MetaCat_struct_r_ord_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_pushout_p^pushout_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι . and (and (and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x6 x4 x7)) (x1 x6 x5 x8)) (x0 x9)) (x1 x4 x9 x10)) (x1 x5 x9 x11)) (x3 x6 x4 x9 x10 x7 = x3 x6 x5 x9 x11 x8)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 x4 x13 x14 ⟶ ∀ x15 . x1 x5 x13 x15 ⟶ x3 x6 x4 x13 x14 x7 = x3 x6 x5 x13 x15 x8 ⟶ and (and (and (x1 x9 x13 (x12 x13 x14 x15)) (x3 x4 x9 x13 (x12 x13 x14 x15) x10 = x14)) (x3 x5 x9 x13 (x12 x13 x14 x15) x11 = x15)) (∀ x16 . x1 x9 x13 x16 ⟶ x3 x4 x9 x13 x16 x10 = x14 ⟶ x3 x5 x9 x13 x16 x11 = x15 ⟶ x16 = x12 x13 x14 x15))
Definition MetaCat_pushout_constr_p^{pushout_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x8 x9 x10 . x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ ∀ x11 x12 . x1 x10 x8 x11 ⟶ x1 x10 x9 x12 ⟶ MetaCat_pushout_p x0 x1 x2 x3 x8 x9 x10 x11 x12 (x4 x8 x9 x10 x11 x12) (x5 x8 x9 x10 x11 x12) (x6 x8 x9 x10 x11 x12) (x7 x8 x9 x10 x11 x12)
Known 19e22..^and10I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9
Theorem e5c69..^{MetaCat_struct_r_ord_pushout_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_pullback_p^pullback_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι . and (and (and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (x0 x9)) (x1 x9 x4 x10)) (x1 x9 x5 x11)) (x3 x9 x4 x6 x7 x10 = x3 x9 x5 x6 x8 x11)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 x13 x4 x14 ⟶ ∀ x15 . x1 x13 x5 x15 ⟶ x3 x13 x4 x6 x7 x14 = x3 x13 x5 x6 x8 x15 ⟶ and (and (and (x1 x13 x9 (x12 x13 x14 x15)) (x3 x13 x9 x4 x10 (x12 x13 x14 x15) = x14)) (x3 x13 x9 x5 x11 (x12 x13 x14 x15) = x15)) (∀ x16 . x1 x13 x9 x16 ⟶ x3 x13 x9 x4 x10 x16 = x14 ⟶ x3 x13 x9 x5 x11 x16 = x15 ⟶ x16 = x12 x13 x14 x15))
Definition MetaCat_pullback_struct_p^{pullback_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x8 x9 x10 . x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ ∀ x11 x12 . x1 x8 x10 x11 ⟶ x1 x9 x10 x12 ⟶ MetaCat_pullback_p x0 x1 x2 x3 x8 x9 x10 x11 x12 (x4 x8 x9 x10 x11 x12) (x5 x8 x9 x10 x11 x12) (x6 x8 x9 x10 x11 x12) (x7 x8 x9 x10 x11 x12)
Theorem 95edd..^{MetaCat_struct_r_ord_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_exp_p^exponent_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 x9 x10 x11 . λ x12 : ι → ι → ι . and (and (and (and (x0 x8) (x0 x9)) (x0 x10)) (x1 (x4 x10 x8) x9 x11)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 (x4 x13 x8) x9 x14 ⟶ and (and (x1 x13 x10 (x12 x13 x14)) (x3 (x4 x13 x8) (x4 x10 x8) x9 x11 (x7 x10 x8 (x4 x13 x8) (x3 (x4 x13 x8) x13 x10 (x12 x13 x14) (x5 x13 x8)) (x6 x13 x8)) = x14)) (∀ x15 . x1 x13 x10 x15 ⟶ x3 (x4 x13 x8) (x4 x10 x8) x9 x11 (x7 x10 x8 (x4 x13 x8) (x3 (x4 x13 x8) x13 x10 x15 (x5 x13 x8)) (x6 x13 x8)) = x14 ⟶ x15 = x12 x13 x14))
Definition MetaCat_exp_constr_p^{product_exponent_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 x9 : ι → ι → ι . λ x10 : ι → ι → ι → ι → ι . and (MetaCat_product_constr_p x0 x1 x2 x3 x4 x5 x6 x7) (∀ x11 x12 . x0 x11 ⟶ x0 x12 ⟶ MetaCat_exp_p x0 x1 x2 x3 x4 x5 x6 x7 x11 x12 (x8 x11 x12) (x9 x11 x12) (x10 x11 x12))
Known and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Theorem d432e..^{MetaCat_struct_r_ord_product_exponent} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13 ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_monic_p^monic := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 . and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (∀ x7 . x0 x7 ⟶ ∀ x8 x9 . x1 x7 x4 x8 ⟶ x1 x7 x4 x9 ⟶ x3 x7 x4 x5 x6 x8 = x3 x7 x4 x5 x6 x9 ⟶ x8 = x9)
Definition MetaCat_subobject_classifier_p^{subobject_classifier_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . λ x6 x7 . λ x8 : ι → ι → ι → ι . λ x9 : ι → ι → ι → ι → ι → ι → ι . and (and (and (MetaCat_terminal_p x0 x1 x2 x3 x4 x5) (x0 x6)) (x1 x4 x6 x7)) (∀ x10 x11 x12 . MetaCat_monic_p x0 x1 x2 x3 x10 x11 x12 ⟶ and (x1 x11 x6 (x8 x10 x11 x12)) (MetaCat_pullback_p x0 x1 x2 x3 x4 x11 x6 x7 (x8 x10 x11 x12) x10 (x5 x10) x12 (x9 x10 x11 x12)))
Theorem 568d6..^{MetaCat_struct_r_ord_subobject_classifier} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition MetaCat_nno_p^nno_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . λ x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (MetaCat_terminal_p x0 x1 x2 x3 x4 x5) (x0 x6)) (x1 x4 x6 x7)) (x1 x6 x6 x8)) (∀ x10 x11 x12 . x0 x10 ⟶ x1 x4 x10 x11 ⟶ x1 x10 x10 x12 ⟶ and (and (and (x1 x6 x10 (x9 x10 x11 x12)) (x3 x4 x6 x10 (x9 x10 x11 x12) x7 = x11)) (x3 x6 x6 x10 (x9 x10 x11 x12) x8 = x3 x6 x10 x10 x12 (x9 x10 x11 x12))) (∀ x13 . x1 x6 x10 x13 ⟶ x3 x4 x6 x10 x13 x7 = x11 ⟶ x3 x6 x6 x10 x13 x8 = x3 x6 x10 x10 x12 x13 ⟶ x13 = x9 x10 x11 x12))
Theorem 1a527..^{MetaCat_struct_r_ord_nno} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p 90aea.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 0eec1.. : not (∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) 90aea.. BinRelnHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0) (proof)
Definition 8b17e..^{struct_r_wellord} := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (and (and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ or (x2 x3 x4) (x2 x4 x3))) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)) (∀ x3 : ι → ο . (∀ x4 . x4 ∈ x1 ⟶ (∀ x5 . x5 ∈ x1 ⟶ x2 x5 x4 ⟶ x3 x5) ⟶ x3 x4) ⟶ ∀ x4 . x4 ∈ x1 ⟶ x3 x4)))
Theorem a6627.. : ∀ x0 . ∀ x1 : ι → ι → ο . unpack_r_o (pack_r x0 x1) (λ x3 . λ x4 : ι → ι → ο . and (and (and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ or (x4 x5 x6) (x4 x6 x5))) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x7 ⟶ x4 x5 x7)) (∀ x5 : ι → ο . (∀ x6 . x6 ∈ x3 ⟶ (∀ x7 . x7 ∈ x3 ⟶ x4 x7 x6 ⟶ x5 x7) ⟶ x5 x6) ⟶ ∀ x6 . x6 ∈ x3 ⟶ x5 x6)) = and (and (and (∀ x3 . x3 ∈ x0 ⟶ not (x1 x3 x3)) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ or (x1 x3 x4) (x1 x4 x3))) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x3 x4 ⟶ x1 x4 x5 ⟶ x1 x3 x5)) (∀ x3 : ι → ο . (∀ x4 . x4 ∈ x0 ⟶ (∀ x5 . x5 ∈ x0 ⟶ x1 x5 x4 ⟶ x3 x5) ⟶ x3 x4) ⟶ ∀ x4 . x4 ∈ x0 ⟶ x3 x4) (proof)
Theorem 71a48.. : ∀ x0 . ∀ x1 : ι → ι → ο . x0 = 0 ⟶ 8b17e.. (pack_r x0 x1) (proof)
Theorem 700c1.. : ∀ x0 . 8b17e.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x2 = 0 ⟶ x1 (pack_r x2 x3)) ⟶ x1 x0 (proof)
Theorem e6e14.. : ∀ x0 x1 x2 . 8b17e.. x0 ⟶ 8b17e.. x1 ⟶ BinRelnHom x0 x1 x2 = (x2 = 0) (proof)
Theorem 19844.. : ∀ x0 x1 x2 . 8b17e.. x0 ⟶ 8b17e.. x1 ⟶ x2 = 0 ⟶ BinRelnHom x0 x1 x2 (proof)
Theorem 66e9d.. : ∀ x0 x1 . 8b17e.. x0 ⟶ 8b17e.. x1 ⟶ BinRelnHom x0 x1 0 (proof)
Theorem 68a11.. : ∀ x0 x1 x2 . 8b17e.. x0 ⟶ 8b17e.. x1 ⟶ BinRelnHom x0 x1 x2 ⟶ x2 = 0 (proof)
Theorem c3477.. : ∀ x0 x1 x2 x3 . 8b17e.. x0 ⟶ 8b17e.. x1 ⟶ BinRelnHom x0 x1 x2 ⟶ BinRelnHom x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 0dd18.. : ∀ x0 x1 x2 x3 x4 . 8b17e.. x0 ⟶ struct_comp x0 x1 x2 x3 x4 = 0 (proof)
Theorem 54f6a.. : 8b17e.. (pack_r 0 (λ x0 x1 . False)) (proof)
Theorem 105dd..^{MetaCat_struct_r_wellord_initial} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 71659.. : MetaCat_terminal_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x0 x1 . False)) (λ x0 . 0) (proof)
Theorem 49763..^{MetaCat_struct_r_wellord_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 17458..^{MetaCat_struct_r_wellord_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem b2d5d.. : MetaCat_product_constr_p 8b17e.. BinRelnHom struct_id struct_comp (λ x0 x1 . pack_r 0 (λ x2 x3 . False)) (λ x0 x1 . 0) (λ x0 x1 . 0) (λ x0 x1 x2 x3 x4 . 0) (proof)
Theorem 71d59..^{MetaCat_struct_r_wellord_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 10b92..^{MetaCat_struct_r_wellord_coequalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem d27a8..^{MetaCat_struct_r_wellord_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem d4e5c..^{MetaCat_struct_r_wellord_pushout_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem ee3b3..^{MetaCat_struct_r_wellord_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 9460d..^{MetaCat_struct_r_wellord_product_exponent} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13 ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem d2cf4..^{MetaCat_struct_r_wellord_subobject_classifier} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem d6d09..^{MetaCat_struct_r_wellord_nno} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 2fd7e.. : not (∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) 8b17e.. BinRelnHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0) (proof)