    module Contravariant.Extras.ContrazipLifting where

    import Contravariant.Extras.Contrazip
    import Contravariant.Extras.Prelude

    contrazipLifting2 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> f (a1, a2)
    contrazipLifting2 :: forall (f :: * -> *) (g :: * -> *) a1 a2.
    Divisible f =>
    (forall x. g x -> f x) -> g a1 -> g a2 -> f (a1, a2)
    contrazipLifting2 forall x. g x -> f x
    fn g a1
    a g a2
    b = f a1 -> f a2 -> f (a1, a2)
    forall (f :: * -> *) a1 a2.
    Divisible f =>
    f a1 -> f a2 -> f (a1, a2)
    contrazip2 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b)

    contrazipLifting3 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> f (a1, a2, a3)
    contrazipLifting3 :: forall (f :: * -> *) (g :: * -> *) a1 a2 a3.
    Divisible f =>
    (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> f (a1, a2, a3)
    contrazipLifting3 forall x. g x -> f x
    fn g a1
    a g a2
    b g a3
    c = f a1 -> f a2 -> f a3 -> f (a1, a2, a3)
    forall (f :: * -> *) a1 a2 a3.
    Divisible f =>
    f a1 -> f a2 -> f a3 -> f (a1, a2, a3)
    contrazip3 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b) (g a3 -> f a3
    forall x. g x -> f x
    fn g a3
    c)

    contrazipLifting4 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> f (a1, a2, a3, a4)
    contrazipLifting4 :: forall (f :: * -> *) (g :: * -> *) a1 a2 a3 a4.
    Divisible f =>
    (forall x. g x -> f x)
    -> g a1 -> g a2 -> g a3 -> g a4 -> f (a1, a2, a3, a4)
    contrazipLifting4 forall x. g x -> f x
    fn g a1
    a g a2
    b g a3
    c g a4
    d = f a1 -> f a2 -> f a3 -> f a4 -> f (a1, a2, a3, a4)
    forall (f :: * -> *) a1 a2 a3 a4.
    Divisible f =>
    f a1 -> f a2 -> f a3 -> f a4 -> f (a1, a2, a3, a4)
    contrazip4 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b) (g a3 -> f a3
    forall x. g x -> f x
    fn g a3
    c) (g a4 -> f a4
    forall x. g x -> f x
    fn g a4
    d)

    contrazipLifting5 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> f (a1, a2, a3, a4, a5)
    contrazipLifting5 :: forall (f :: * -> *) (g :: * -> *) a1 a2 a3 a4 a5.
    Divisible f =>
    (forall x. g x -> f x)
    -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> f (a1, a2, a3, a4, a5)
    contrazipLifting5 forall x. g x -> f x
    fn g a1
    a g a2
    b g a3
    c g a4
    d g a5
    e = f a1 -> f a2 -> f a3 -> f a4 -> f a5 -> f (a1, a2, a3, a4, a5)
    forall (f :: * -> *) a1 a2 a3 a4 a5.
    Divisible f =>
    f a1 -> f a2 -> f a3 -> f a4 -> f a5 -> f (a1, a2, a3, a4, a5)
    contrazip5 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b) (g a3 -> f a3
    forall x. g x -> f x
    fn g a3
    c) (g a4 -> f a4
    forall x. g x -> f x
    fn g a4
    d) (g a5 -> f a5
    forall x. g x -> f x
    fn g a5
    e)

    contrazipLifting6 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> g a6 -> f (a1, a2, a3, a4, a5, a6)
    contrazipLifting6 :: forall (f :: * -> *) (g :: * -> *) a1 a2 a3 a4 a5 a6.
    Divisible f =>
    (forall x. g x -> f x)
    -> g a1
    -> g a2
    -> g a3
    -> g a4
    -> g a5
    -> g a6
    -> f (a1, a2, a3, a4, a5, a6)
    contrazipLifting6 forall x. g x -> f x
    fn g a1
    a g a2
    b g a3
    c g a4
    d g a5
    e g a6
    f = f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f (a1, a2, a3, a4, a5, a6)
    forall (f :: * -> *) a1 a2 a3 a4 a5 a6.
    Divisible f =>
    f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f (a1, a2, a3, a4, a5, a6)
    contrazip6 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b) (g a3 -> f a3
    forall x. g x -> f x
    fn g a3
    c) (g a4 -> f a4
    forall x. g x -> f x
    fn g a4
    d) (g a5 -> f a5
    forall x. g x -> f x
    fn g a5
    e) (g a6 -> f a6
    forall x. g x -> f x
    fn g a6
    f)

    contrazipLifting7 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> g a6 -> g a7 -> f (a1, a2, a3, a4, a5, a6, a7)
    contrazipLifting7 :: forall (f :: * -> *) (g :: * -> *) a1 a2 a3 a4 a5 a6 a7.
    Divisible f =>
    (forall x. g x -> f x)
    -> g a1
    -> g a2
    -> g a3
    -> g a4
    -> g a5
    -> g a6
    -> g a7
    -> f (a1, a2, a3, a4, a5, a6, a7)
    contrazipLifting7 forall x. g x -> f x
    fn g a1
    a g a2
    b g a3
    c g a4
    d g a5
    e g a6
    f g a7
    g = f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f a7
    -> f (a1, a2, a3, a4, a5, a6, a7)
    forall (f :: * -> *) a1 a2 a3 a4 a5 a6 a7.
    Divisible f =>
    f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f a7
    -> f (a1, a2, a3, a4, a5, a6, a7)
    contrazip7 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b) (g a3 -> f a3
    forall x. g x -> f x
    fn g a3
    c) (g a4 -> f a4
    forall x. g x -> f x
    fn g a4
    d) (g a5 -> f a5
    forall x. g x -> f x
    fn g a5
    e) (g a6 -> f a6
    forall x. g x -> f x
    fn g a6
    f) (g a7 -> f a7
    forall x. g x -> f x
    fn g a7
    g)

    contrazipLifting8 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> g a6 -> g a7 -> g a8 -> f (a1, a2, a3, a4, a5, a6, a7, a8)
    contrazipLifting8 :: forall (f :: * -> *) (g :: * -> *) a1 a2 a3 a4 a5 a6 a7 a8.
    Divisible f =>
    (forall x. g x -> f x)
    -> g a1
    -> g a2
    -> g a3
    -> g a4
    -> g a5
    -> g a6
    -> g a7
    -> g a8
    -> f (a1, a2, a3, a4, a5, a6, a7, a8)
    contrazipLifting8 forall x. g x -> f x
    fn g a1
    a g a2
    b g a3
    c g a4
    d g a5
    e g a6
    f g a7
    g g a8
    h = f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f a7
    -> f a8
    -> f (a1, a2, a3, a4, a5, a6, a7, a8)
    forall (f :: * -> *) a1 a2 a3 a4 a5 a6 a7 a8.
    Divisible f =>
    f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f a7
    -> f a8
    -> f (a1, a2, a3, a4, a5, a6, a7, a8)
    contrazip8 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b) (g a3 -> f a3
    forall x. g x -> f x
    fn g a3
    c) (g a4 -> f a4
    forall x. g x -> f x
    fn g a4
    d) (g a5 -> f a5
    forall x. g x -> f x
    fn g a5
    e) (g a6 -> f a6
    forall x. g x -> f x
    fn g a6
    f) (g a7 -> f a7
    forall x. g x -> f x
    fn g a7
    g) (g a8 -> f a8
    forall x. g x -> f x
    fn g a8
    h)

    contrazipLifting9 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> g a6 -> g a7 -> g a8 -> g a9 -> f (a1, a2, a3, a4, a5, a6, a7, a8, a9)
    contrazipLifting9 :: forall (f :: * -> *) (g :: * -> *) a1 a2 a3 a4 a5 a6 a7 a8 a9.
    Divisible f =>
    (forall x. g x -> f x)
    -> g a1
    -> g a2
    -> g a3
    -> g a4
    -> g a5
    -> g a6
    -> g a7
    -> g a8
    -> g a9
    -> f (a1, a2, a3, a4, a5, a6, a7, a8, a9)
    contrazipLifting9 forall x. g x -> f x
    fn g a1
    a g a2
    b g a3
    c g a4
    d g a5
    e g a6
    f g a7
    g g a8
    h g a9
    i = f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f a7
    -> f a8
    -> f a9
    -> f (a1, a2, a3, a4, a5, a6, a7, a8, a9)
    forall (f :: * -> *) a1 a2 a3 a4 a5 a6 a7 a8 a9.
    Divisible f =>
    f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f a7
    -> f a8
    -> f a9
    -> f (a1, a2, a3, a4, a5, a6, a7, a8, a9)
    contrazip9 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b) (g a3 -> f a3
    forall x. g x -> f x
    fn g a3
    c) (g a4 -> f a4
    forall x. g x -> f x
    fn g a4
    d) (g a5 -> f a5
    forall x. g x -> f x
    fn g a5
    e) (g a6 -> f a6
    forall x. g x -> f x
    fn g a6
    f) (g a7 -> f a7
    forall x. g x -> f x
    fn g a7
    g) (g a8 -> f a8
    forall x. g x -> f x
    fn g a8
    h) (g a9 -> f a9
    forall x. g x -> f x
    fn g a9
    i)

    contrazipLifting10 :: (Divisible f) => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> g a6 -> g a7 -> g a8 -> g a9 -> g a10 -> f (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)
    contrazipLifting10 :: forall (f :: * -> *) (g :: * -> *) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
    Divisible f =>
    (forall x. g x -> f x)
    -> g a1
    -> g a2
    -> g a3
    -> g a4
    -> g a5
    -> g a6
    -> g a7
    -> g a8
    -> g a9
    -> g a10
    -> f (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)
    contrazipLifting10 forall x. g x -> f x
    fn g a1
    a g a2
    b g a3
    c g a4
    d g a5
    e g a6
    f g a7
    g g a8
    h g a9
    i g a10
    j = f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f a7
    -> f a8
    -> f a9
    -> f a10
    -> f (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)
    forall (f :: * -> *) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
    Divisible f =>
    f a1
    -> f a2
    -> f a3
    -> f a4
    -> f a5
    -> f a6
    -> f a7
    -> f a8
    -> f a9
    -> f a10
    -> f (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)
    contrazip10 (g a1 -> f a1
    forall x. g x -> f x
    fn g a1
    a) (g a2 -> f a2
    forall x. g x -> f x
    fn g a2
    b) (g a3 -> f a3
    forall x. g x -> f x
    fn g a3
    c) (g a4 -> f a4
    forall x. g x -> f x
    fn g a4
    d) (g a5 -> f a5
    forall x. g x -> f x
    fn g a5
    e) (g a6 -> f a6
    forall x. g x -> f x
    fn g a6
    f) (g a7 -> f a7
    forall x. g x -> f x
    fn g a7
    g) (g a8 -> f a8
    forall x. g x -> f x
    fn g a8
    h) (g a9 -> f a9
    forall x. g x -> f x
    fn g a9
    i) (g a10 -> f a10
    forall x. g x -> f x
    fn g a10
    j)