Search for blocks/addresses/...

Proofgold Asset

asset id
ce1fbd6aeea749b76a0850f1a1588d8bf7aeb55a2e78aecb5df46d11cee6564b
asset hash
528b2b0561fbb1dbca9f767d51aa5bf25e479abe4f671a634b4dbf40ce0b8eac
bday / block
9687
tx
63d1b..
preasset
doc published by PrCx1..
Param MetaFunctorMetaFunctor : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → ο
Known 2cb62..MetaFunctorI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . (∀ x10 . x0 x10x4 (x8 x10))(∀ x10 x11 x12 . x0 x10x0 x11x1 x10 x11 x12x5 (x8 x10) (x8 x11) (x9 x10 x11 x12))(∀ x10 . x0 x10x9 x10 x10 (x2 x10) = x6 (x8 x10))(∀ x10 x11 x12 x13 x14 . x0 x10x0 x11x0 x12x1 x10 x11 x13x1 x11 x12 x14x9 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 MetaCatMetaCat : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ο
Param MetaFunctor_strictMetaFunctor_strict : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → ο
Known 5cbb4..MetaFunctor_strict_I : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaCat x0 x1 x2 x3MetaCat x4 x5 x6 x7MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
Theorem 2447d..MetaCat_IdFunctor_strict : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3MetaFunctor_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 x11x4 (x8 x11))(∀ x11 x12 x13 . x0 x11x0 x12x1 x11 x12 x13x5 (x8 x11) (x8 x12) (x9 x11 x12 x13))(∀ x11 . x0 x11x9 x11 x11 (x2 x11) = x6 (x8 x11))(∀ x11 x12 x13 x14 x15 . x0 x11x0 x12x0 x13x1 x11 x12 x14x1 x12 x13 x15x9 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 x13MetaFunctor x4 x5 x6 x7 x8 x9 x10 x11 x14 x15MetaFunctor 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 x3MetaCat x4 x5 x6 x7MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9x10)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 x13MetaFunctor_strict x4 x5 x6 x7 x8 x9 x10 x11 x14 x15MetaFunctor_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 andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition MetaNatTransMetaNatTrans := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . λ x10 : ι → ι . λ x11 : ι → ι → ι → ι . λ x12 : ι → ι . and (∀ x13 . x0 x13x5 (x8 x13) (x10 x13) (x12 x13)) (∀ x13 x14 x15 . x0 x13x0 x14x1 x13 x14 x15x7 (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 andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem c1d68..MetaNatTransI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . (∀ x13 . x0 x13x5 (x8 x13) (x10 x13) (x12 x13))(∀ x13 x14 x15 . x0 x13x0 x14x1 x13 x14 x15x7 (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 x14x5 (x8 x14) (x10 x14) (x12 x14))(∀ x14 x15 x16 . x0 x14x0 x15x1 x14 x15 x16x7 (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_strictMetaNatTrans_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 and5Iand5I : ∀ x0 x1 x2 x3 x4 : ο . x0x1x2x3x4and (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 x3MetaCat x4 x5 x6 x7MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12MetaNatTrans_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 (proof)
Known and5Eand5E : ∀ x0 x1 x2 x3 x4 : ο . and (and (and (and x0 x1) x2) x3) x4∀ x5 : ο . (x0x1x2x3x4x5)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 x3MetaCat x4 x5 x6 x7MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x13)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 x13MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x14 x15MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x12 x13 x14 x15 x18MetaFunctor x4 x5 x6 x7 x8 x9 x10 x11 x16 x17MetaNatTrans 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 x18MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x16 x17MetaNatTrans 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 MetaMonadMetaMonad := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ι . λ x5 : ι → ι → ι → ι . λ x6 x7 : ι → ι . and (and (∀ x8 . x0 x8x3 (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 x8x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x6 (x4 x8)) = x2 (x4 x8))) (∀ x8 . x0 x8x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 x8 (x4 x8) (x6 x8)) = x2 (x4 x8))
Definition MetaMonad_strictMetaMonad_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 and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Theorem 46096..MetaMonadI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ι → ι . ∀ x6 x7 : ι → ι . (∀ x8 . x0 x8x3 (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 x8x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x6 (x4 x8)) = x2 (x4 x8))(∀ x8 . x0 x8x3 (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 and3Eand3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2∀ x3 : ο . (x0x1x2x3)x3
Theorem f4ba2..MetaMonadE : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ι → ι . ∀ x6 x7 : ι → ι . MetaMonad x0 x1 x2 x3 x4 x5 x6 x7∀ x8 : ο . ((∀ x9 . x0 x9x3 (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 x9x3 (x4 x9) (x4 (x4 x9)) (x4 x9) (x7 x9) (x6 (x4 x9)) = x2 (x4 x9))(∀ x9 . x0 x9x3 (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 x6MetaNatTrans_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 x7MetaMonad x0 x1 x2 x3 x4 x5 x6 x7MetaMonad_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 x6MetaNatTrans_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 x7MetaMonad x0 x1 x2 x3 x4 x5 x6 x7x8)x8 (proof)
Definition MetaAdjunctionMetaAdjunction := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . λ x10 : ι → ι . λ x11 : ι → ι → ι → ι . λ x12 x13 : ι → ι . and (∀ x14 . x0 x14x7 (x8 x14) (x8 (x10 (x8 x14))) (x8 x14) (x13 (x8 x14)) (x9 x14 (x10 (x8 x14)) (x12 x14)) = x6 (x8 x14)) (∀ x14 . x4 x14x3 (x10 x14) (x10 (x8 (x10 x14))) (x10 x14) (x11 (x8 (x10 x14)) x14 (x13 x14)) (x12 (x10 x14)) = x2 (x10 x14))
Definition MetaAdjunction_strictMetaAdjunction_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 x14x7 (x8 x14) (x8 (x10 (x8 x14))) (x8 x14) (x13 (x8 x14)) (x9 x14 (x10 (x8 x14)) (x12 x14)) = x6 (x8 x14))(∀ x14 . x4 x14x3 (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 x15x7 (x8 x15) (x8 (x10 (x8 x15))) (x8 x15) (x13 (x8 x15)) (x9 x15 (x10 (x8 x15)) (x12 x15)) = x6 (x8 x15))(∀ x15 . x4 x15x3 (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 x9MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11MetaNatTrans 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)) x12MetaNatTrans 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) x13MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13MetaAdjunction_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 x9MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11MetaNatTrans 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)) x12MetaNatTrans 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) x13MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13x14)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 x9MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11MetaNatTrans 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)) x12MetaNatTrans 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) x13MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13MetaMonad 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 x13MetaMonad_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)