Proofgold Address

Param MetaFunctor^MetaFunctor : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → ο
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
Theorem b7eb1..^{MetaCat_IdFunctor} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaFunctor x0 x1 x2 x3 x0 x1 x2 x3 (λ x4 . x4) (λ x4 x5 x6 . x6) (proof)
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Param MetaFunctor_strict^{MetaFunctor_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → ο
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
Theorem 2447d..^{MetaCat_IdFunctor_strict} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ MetaFunctor_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x4 . x4) (λ x4 x5 x6 . x6) (proof)
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
Theorem d7211..^{MetaCat_CompFunctors} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ο . ∀ x9 : ι → ι → ι → ο . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι → ι → ι . ∀ x12 : ι → ι . ∀ x13 : ι → ι → ι → ι . ∀ x14 : ι → ι . ∀ x15 : ι → ι → ι → ι . MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x12 x13 ⟶ MetaFunctor x4 x5 x6 x7 x8 x9 x10 x11 x14 x15 ⟶ MetaFunctor x0 x1 x2 x3 x8 x9 x10 x11 (λ x16 . x14 (x12 x16)) (λ x16 x17 x18 . x15 (x12 x16) (x12 x17) (x13 x16 x17 x18)) (proof)
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
Theorem 1eb28..^{MetaCat_CompFunctors_strict} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ο . ∀ x9 : ι → ι → ι → ο . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι → ι → ι . ∀ x12 : ι → ι . ∀ x13 : ι → ι → ι → ι . ∀ x14 : ι → ι . ∀ x15 : ι → ι → ι → ι . MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x12 x13 ⟶ MetaFunctor_strict x4 x5 x6 x7 x8 x9 x10 x11 x14 x15 ⟶ MetaFunctor_strict x0 x1 x2 x3 x8 x9 x10 x11 (λ x16 . x14 (x12 x16)) (λ x16 x17 x18 . x15 (x12 x16) (x12 x17) (x13 x16 x17 x18)) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition MetaNatTrans^MetaNatTrans := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . λ x10 : ι → ι . λ x11 : ι → ι → ι → ι . λ x12 : ι → ι . and (∀ 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))
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 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 (proof)
Theorem 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 (proof)
Definition MetaNatTrans_strict^{MetaNatTrans_strict} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . λ x10 : ι → ι . λ x11 : ι → ι → ι → ι . λ x12 : ι → ι . and (and (and (and (MetaCat x0 x1 x2 x3) (MetaCat x4 x5 x6 x7)) (MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) (MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11)) (MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 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 59a37..^{MetaNatTrans_strict_I} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . MetaCat x0 x1 x2 x3 ⟶ MetaCat x4 x5 x6 x7 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11 ⟶ MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ MetaNatTrans_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 (proof)
Known and5E^and5E : ∀ x0 x1 x2 x3 x4 : ο . and (and (and (and x0 x1) x2) x3) x4 ⟶ ∀ x5 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5) ⟶ x5
Theorem b8f26..^{MetaNatTrans_strict_E} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . MetaNatTrans_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ ∀ x13 : ο . (MetaCat x0 x1 x2 x3 ⟶ MetaCat x4 x5 x6 x7 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11 ⟶ MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x13) ⟶ x13 (proof)
Theorem d7aeb..^{MetaCat_CompFunctorNatTrans} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ο . ∀ x9 : ι → ι → ι → ο . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι → ι → ι . ∀ x12 : ι → ι . ∀ x13 : ι → ι → ι → ι . ∀ x14 : ι → ι . ∀ x15 : ι → ι → ι → ι . ∀ x16 : ι → ι . ∀ x17 : ι → ι → ι → ι . ∀ x18 : ι → ι . MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x12 x13 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x14 x15 ⟶ MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x12 x13 x14 x15 x18 ⟶ MetaFunctor x4 x5 x6 x7 x8 x9 x10 x11 x16 x17 ⟶ MetaNatTrans x0 x1 x2 x3 x8 x9 x10 x11 (λ x19 . x16 (x12 x19)) (λ x19 x20 x21 . x17 (x12 x19) (x12 x20) (x13 x19 x20 x21)) (λ x19 . x16 (x14 x19)) (λ x19 x20 x21 . x17 (x14 x19) (x14 x20) (x15 x19 x20 x21)) (λ x19 . x17 (x12 x19) (x14 x19) (x18 x19)) (proof)
Theorem b8a6b..^{MetaCat_CompNatTransFunctor} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ο . ∀ x9 : ι → ι → ι → ο . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι → ι → ι . ∀ x12 : ι → ι . ∀ x13 : ι → ι → ι → ι . ∀ x14 : ι → ι . ∀ x15 : ι → ι → ι → ι . ∀ x16 : ι → ι . ∀ x17 : ι → ι → ι → ι . ∀ x18 : ι → ι . MetaNatTrans x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x18 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x16 x17 ⟶ MetaNatTrans x0 x1 x2 x3 x8 x9 x10 x11 (λ x19 . x12 (x16 x19)) (λ x19 x20 x21 . x13 (x16 x19) (x16 x20) (x17 x19 x20 x21)) (λ x19 . x14 (x16 x19)) (λ x19 x20 x21 . x15 (x16 x19) (x16 x20) (x17 x19 x20 x21)) (λ x19 . x18 (x16 x19)) (proof)
Definition MetaMonad^MetaMonad := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ι . λ x5 : ι → ι → ι → ι . λ x6 x7 : ι → ι . and (and (∀ x8 . x0 x8 ⟶ x3 (x4 (x4 (x4 x8))) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 (x4 (x4 x8)) (x4 x8) (x7 x8)) = x3 (x4 (x4 (x4 x8))) (x4 (x4 x8)) (x4 x8) (x7 x8) (x7 (x4 x8))) (∀ x8 . x0 x8 ⟶ x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x6 (x4 x8)) = x2 (x4 x8))) (∀ x8 . x0 x8 ⟶ x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 x8 (x4 x8) (x6 x8)) = x2 (x4 x8))
Definition MetaMonad_strict^{MetaMonad_strict} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ι . λ x5 : ι → ι → ι → ι . λ x6 x7 : ι → ι . and (and (MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x8 . x8) (λ x8 x9 x10 . x10) x4 x5 x6) (MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x8 . x4 (x4 x8)) (λ x8 x9 x10 . x5 (x4 x8) (x4 x9) (x5 x8 x9 x10)) x4 x5 x7)) (MetaMonad x0 x1 x2 x3 x4 x5 x6 x7)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 46096..^MetaMonadI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ι → ι . ∀ x6 x7 : ι → ι . (∀ x8 . x0 x8 ⟶ x3 (x4 (x4 (x4 x8))) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 (x4 (x4 x8)) (x4 x8) (x7 x8)) = x3 (x4 (x4 (x4 x8))) (x4 (x4 x8)) (x4 x8) (x7 x8) (x7 (x4 x8))) ⟶ (∀ x8 . x0 x8 ⟶ x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x6 (x4 x8)) = x2 (x4 x8)) ⟶ (∀ x8 . x0 x8 ⟶ x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 x8 (x4 x8) (x6 x8)) = x2 (x4 x8)) ⟶ MetaMonad x0 x1 x2 x3 x4 x5 x6 x7 (proof)
Known and3E^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem f4ba2..^MetaMonadE : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ι → ι . ∀ x6 x7 : ι → ι . MetaMonad x0 x1 x2 x3 x4 x5 x6 x7 ⟶ ∀ x8 : ο . ((∀ x9 . x0 x9 ⟶ x3 (x4 (x4 (x4 x9))) (x4 (x4 x9)) (x4 x9) (x7 x9) (x5 (x4 (x4 x9)) (x4 x9) (x7 x9)) = x3 (x4 (x4 (x4 x9))) (x4 (x4 x9)) (x4 x9) (x7 x9) (x7 (x4 x9))) ⟶ (∀ x9 . x0 x9 ⟶ x3 (x4 x9) (x4 (x4 x9)) (x4 x9) (x7 x9) (x6 (x4 x9)) = x2 (x4 x9)) ⟶ (∀ x9 . x0 x9 ⟶ x3 (x4 x9) (x4 (x4 x9)) (x4 x9) (x7 x9) (x5 x9 (x4 x9) (x6 x9)) = x2 (x4 x9)) ⟶ x8) ⟶ x8 (proof)
Theorem 16309..^{MetaMonad_strict_I} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ι → ι . ∀ x6 x7 : ι → ι . MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x8 . x8) (λ x8 x9 x10 . x10) x4 x5 x6 ⟶ MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x8 . x4 (x4 x8)) (λ x8 x9 x10 . x5 (x4 x8) (x4 x9) (x5 x8 x9 x10)) x4 x5 x7 ⟶ MetaMonad x0 x1 x2 x3 x4 x5 x6 x7 ⟶ MetaMonad_strict x0 x1 x2 x3 x4 x5 x6 x7 (proof)
Theorem 80e83..^{MetaMonad_strict_E} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ι → ι . ∀ x6 x7 : ι → ι . MetaMonad_strict x0 x1 x2 x3 x4 x5 x6 x7 ⟶ ∀ x8 : ο . (MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x9 . x9) (λ x9 x10 x11 . x11) x4 x5 x6 ⟶ MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x9 . x4 (x4 x9)) (λ x9 x10 x11 . x5 (x4 x9) (x4 x10) (x5 x9 x10 x11)) x4 x5 x7 ⟶ MetaMonad x0 x1 x2 x3 x4 x5 x6 x7 ⟶ x8) ⟶ x8 (proof)
Definition MetaAdjunction^{MetaAdjunction} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . λ x10 : ι → ι . λ x11 : ι → ι → ι → ι . λ x12 x13 : ι → ι . and (∀ 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))
Definition MetaAdjunction_strict^{MetaAdjunction_strict} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . λ x10 : ι → ι . λ x11 : ι → ι → ι → ι . λ x12 x13 : ι → ι . and (and (and (and (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)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem db40a..^{MetaAdjunctionMonad} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaFunctor 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 ⟶ MetaMonad x0 x1 x2 x3 (λ x14 . x10 (x8 x14)) (λ x14 x15 x16 . x11 (x8 x14) (x8 x15) (x9 x14 x15 x16)) x12 (λ x14 . x11 (x8 (x10 (x8 x14))) (x8 x14) (x13 (x8 x14))) (proof)
Theorem 07be6..^{MetaAdjunctionMonad_strict} : ∀ 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 ⟶ MetaMonad_strict x0 x1 x2 x3 (λ x14 . x10 (x8 x14)) (λ x14 x15 x16 . x11 (x8 x14) (x8 x15) (x9 x14 x15 x16)) x12 (λ x14 . x11 (x8 (x10 (x8 x14))) (x8 x14) (x13 (x8 x14))) (proof)