Proofgold Address

Param pack_u^pack_u : ι → (ι → ι) → ι
Param setsum^setsum : ι → ι → ι
Param combine_funcs^{combine_funcs} : ι → ι → (ι → ι) → (ι → ι) → ι → ι
Param Inj1^Inj1 : ι → ι
Definition 47c33.. := λ x0 . pack_u (setsum x0 x0) (combine_funcs x0 x0 Inj1 Inj1)
Param lam^Sigma : ι → (ι → ι) → ι
Param Inj0^Inj0 : ι → ι
Param ap^ap : ι → ι → ι
Definition 2e027.. := λ x0 x1 x2 . lam (setsum x0 x0) (combine_funcs x0 x0 (λ x3 . Inj0 (ap x2 x3)) (λ x3 . Inj1 (ap x2 x3)))
Definition f3f54.. := λ x0 . lam x0 Inj0
Param unpack_u_i^unpack_u_i : ι → (ι → (ι → ι) → ι) → ι
Definition daacd.. := λ x0 . unpack_u_i x0 (λ x1 . λ x2 : ι → ι . lam (setsum x1 x1) (combine_funcs x1 x1 (λ x3 . x3) x2))
Param MetaAdjunction_strict^{MetaAdjunction_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Param True^True : ο
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Definition HomSet^SetHom := λ x0 x1 x2 . x2 ∈ setexp x1 x0
Definition lam_id^lam_id := λ x0 . lam x0 (λ x1 . x1)
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition struct_u^struct_u := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . x4 ∈ x2 ⟶ x3 x4 ∈ x2) ⟶ x1 (pack_u x2 x3)) ⟶ x1 x0
Param unpack_u_o^unpack_u_o : ι → (ι → (ι → ι) → ο) → ο
Definition 9f253..^{struct_u_idem} := λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . λ x2 : ι → ι . ∀ x3 . x3 ∈ x1 ⟶ x2 (x2 x3) = x2 x3))
Param UnaryFuncHom^Hom_struct_u : ι → ι → ι → ο
Definition struct_id^struct_id := λ x0 . lam_id (ap x0 0)
Definition struct_comp^struct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Param MetaFunctor_strict^{MetaFunctor_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → ο
Param MetaFunctor^MetaFunctor : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → ο
Param MetaNatTrans^MetaNatTrans : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → ο
Param MetaAdjunction^{MetaAdjunction} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
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
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
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 31a6e..^{MetaCat_struct_u_idem} : MetaCat 9f253.. UnaryFuncHom struct_id struct_comp
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 andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known pack_struct_u_I^{pack_struct_u_I} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ struct_u (pack_u x0 x1)
Known unpack_u_o_eq^{unpack_u_o_eq} : ∀ x0 : ι → (ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_u_o (pack_u x1 x2) x0 = x0 x1 x2
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known setsum_Inj_inv^{setsum_Inj_inv} : ∀ x0 x1 x2 . x2 ∈ setsum x0 x1 ⟶ or (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = Inj0 x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x2 = Inj1 x4) ⟶ x3) ⟶ x3)
Known combine_funcs_eq1^{combine_funcs_eq1} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known combine_funcs_eq2^{combine_funcs_eq2} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known 66c4c..^{Hom_struct_u_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . UnaryFuncHom (pack_u x0 x2) (pack_u x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ ap x4 (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 Inj0_setsum^Inj0_setsum : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ Inj0 x2 ∈ setsum x0 x1
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known Inj1_setsum^Inj1_setsum : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ Inj1 x2 ∈ setsum x0 x1
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known pack_u_0_eq2^pack_u_0_eq2 : ∀ x0 . ∀ x1 : ι → ι . x0 = ap (pack_u x0 x1) 0
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known 3605e..^{MetaCat_struct_u_idem_Forgetful} : MetaFunctor 9f253.. UnaryFuncHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
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 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
Known unpack_u_i_eq^{unpack_u_i_eq} : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_u_i (pack_u x1 x2) x0 = x0 x1 x2
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem ddbae.. : MetaAdjunction_strict (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) 9f253.. UnaryFuncHom struct_id struct_comp 47c33.. 2e027.. (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) f3f54.. daacd.. (proof)
Theorem 49304..^{MetaCat_struct_u_idem_left_adjoint_forgetful} : ∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) 9f253.. UnaryFuncHom 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)
Param MetaCat_initial_p^initial_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
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
Known 09501.. : ∀ 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 . ∀ x15 : ι → ι . MetaCat_initial_p x0 x1 x2 x3 x14 x15 ⟶ ∀ x16 : ο . (∀ x17 : ι → ι . MetaCat_initial_p x4 x5 x6 x7 (x8 x14) x17 ⟶ x16) ⟶ x16
Theorem 2fd91..^{MetaCat_struct_u_idem_initial} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p 9f253.. UnaryFuncHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)