{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Structure.Some.Stream where

import Pandora.Core.Functor (type (:=), type (:=>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), twosome)
import Pandora.Paradigm.Primary.Algebraic (extract)
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, (.-+))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate), premorph, rotate)
import Pandora.Paradigm.Structure.Ability.Zipper (Zippable (Breadcrumbs))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Primary.Algebraic (point)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (!))

type Stream = Construction Identity

instance Zippable (Construction Identity) where
	type Breadcrumbs (Construction Identity) = Stream <:.:> Stream := (:*:)

instance Morphable (Rotate Left) (Identity <:.:> (Stream <:.:> Stream := (:*:)) := (:*:)) where
	type Morphing (Rotate Left) (Identity <:.:> (Stream <:.:> Stream := (:*:)) := (:*:)) =
		Identity <:.:> (Stream <:.:> Stream := (:*:)) := (:*:)
	morphing :: (<::>)
  (Tagged ('Rotate 'Left))
  ((Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   := (:*:))
  a
-> Morphing
     ('Rotate 'Left)
     ((Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      := (:*:))
     a
morphing ((:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
-> Identity a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Construction Identity)
         (Construction Identity)
         a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> Identity a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Construction Identity)
          (Construction Identity)
          a)
-> ((<::>)
      (Tagged ('Rotate 'Left))
      ((Identity
        <:.:> ((Construction Identity <:.:> Construction Identity)
               := (:*:)))
       := (:*:))
      a
    -> (:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a)
-> (<::>)
     (Tagged ('Rotate 'Left))
     ((Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      := (:*:))
     a
-> Identity a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Construction Identity)
         (Construction Identity)
         a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>)
  (Tagged ('Rotate 'Left))
  ((Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   := (:*:))
  a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Identity a
x :*: T_U (Construction Identity a
bs :*: Construction Identity a
fs)) = Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Identity)
      (Construction Identity)
      a
 -> (:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
-> Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall a. a -> Identity a
Identity (Construction Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Identity a
bs)
		(T_U
   Covariant
   Covariant
   (:*:)
   (Construction Identity)
   (Construction Identity)
   a
 -> (:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Identity a
-> Construction Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Identity a
 -> Construction Identity a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Identity)
      (Construction Identity)
      a)
-> Construction Identity a
-> Construction Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity (Construction Identity a) -> Construction Identity a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction Identity a -> Identity (Construction Identity a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Identity a
bs) (Construction Identity a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Identity)
      (Construction Identity)
      a)
-> Construction Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity (Construction Identity a) -> Construction Identity a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Construction Identity a -> Identity (Construction Identity a)
forall (t :: * -> *) a. Pointable t => a -> t a
point Construction Identity a
fs)

instance Morphable (Rotate Right) (Identity <:.:> (Stream <:.:> Stream := (:*:)) := (:*:)) where
	type Morphing (Rotate Right) (Identity <:.:> (Stream <:.:> Stream := (:*:)) := (:*:)) = Identity <:.:> (Stream <:.:> Stream := (:*:)) := (:*:)
	morphing :: (<::>)
  (Tagged ('Rotate 'Right))
  ((Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   := (:*:))
  a
-> Morphing
     ('Rotate 'Right)
     ((Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      := (:*:))
     a
morphing ((:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
-> Identity a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Construction Identity)
         (Construction Identity)
         a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> Identity a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Construction Identity)
          (Construction Identity)
          a)
-> ((<::>)
      (Tagged ('Rotate 'Right))
      ((Identity
        <:.:> ((Construction Identity <:.:> Construction Identity)
               := (:*:)))
       := (:*:))
      a
    -> (:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a)
-> (<::>)
     (Tagged ('Rotate 'Right))
     ((Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      := (:*:))
     a
-> Identity a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Construction Identity)
         (Construction Identity)
         a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>)
  (Tagged ('Rotate 'Right))
  ((Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   := (:*:))
  a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Identity a
x :*: T_U (Construction Identity a
bs :*: Construction Identity a
fs)) = Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Identity)
      (Construction Identity)
      a
 -> (:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
-> Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall a. a -> Identity a
Identity (Construction Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Identity a
fs)
		(T_U
   Covariant
   Covariant
   (:*:)
   (Construction Identity)
   (Construction Identity)
   a
 -> (:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Identity a
-> Construction Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Identity a
 -> Construction Identity a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Identity)
      (Construction Identity)
      a)
-> Construction Identity a
-> Construction Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a
-> ((Identity :. Construction Identity) := a)
-> Construction Identity a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Construction Identity a -> (Identity :. Construction Identity) := a
forall (t :: * -> *) a. Pointable t => a -> t a
point Construction Identity a
bs) (Construction Identity a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Identity)
      (Construction Identity)
      a)
-> Construction Identity a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Identity)
     (Construction Identity)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# ((Identity :. Construction Identity) := a)
-> Construction Identity a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction Identity a -> (Identity :. Construction Identity) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Identity a
fs)

instance {-# OVERLAPS #-} Extendable (->) (Identity <:.:> (Stream <:.:> Stream := (:*:)) := (:*:)) where
	(:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
-> b
f <<= :: ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> b)
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     b
<<= (:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
z = let move :: ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> (:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
move (:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
rtt = Identity
  (Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a))
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity
   (Construction
      Identity
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a))
 -> Construction
      Identity
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a))
-> (Construction
      Identity
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a)
    -> Identity
         (Construction
            Identity
            ((:=)
               (Identity
                <:.:> ((Construction Identity <:.:> Construction Identity)
                       := (:*:)))
               (:*:)
               a)))
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
  Identity
  ((:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a)
-> Identity
     (Construction
        Identity
        ((:=)
           (Identity
            <:.:> ((Construction Identity <:.:> Construction Identity)
                   := (:*:)))
           (:*:)
           a))
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction
   Identity
   ((:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
 -> Construction
      Identity
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a))
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
-> Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall (t :: * -> *) a. Pointable t => a -> t a
point ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> Identity
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a))
-> ((:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a
    -> (:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a)
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
-> Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
rtt ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> Identity
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a))
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a
   :=> Construction Identity
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a :=> t) -> a :=> Construction t
.-+ (:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
z
		in (:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
-> b
f ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> b)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Construction Identity <:.:> Construction Identity) := (:*:))
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
-> (:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (Identity
   ((:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
 :*: (:=)
       (Construction Identity <:.:> Construction Identity)
       (:*:)
       ((:=)
          (Identity
           <:.:> ((Construction Identity <:.:> Construction Identity)
                  := (:*:)))
          (:*:)
          a))
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Construction Identity <:.:> Construction Identity) := (:*:))
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
-> Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall a. a -> Identity a
Identity (:=)
  (Identity
   <:.:> ((Construction Identity <:.:> Construction Identity)
          := (:*:)))
  (:*:)
  a
z Identity
  ((:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a)
-> (:=)
     (Construction Identity <:.:> Construction Identity)
     (:*:)
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
-> Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
   :*: (:=)
         (Construction Identity <:.:> Construction Identity)
         (:*:)
         ((:=)
            (Identity
             <:.:> ((Construction Identity <:.:> Construction Identity)
                    := (:*:)))
            (:*:)
            a)
forall s a. s -> a -> s :*: a
:*: Construction
  Identity
  ((:=)
     (Identity
      <:.:> ((Construction Identity <:.:> Construction Identity)
             := (:*:)))
     (:*:)
     a)
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
-> (:=)
     (Construction Identity <:.:> Construction Identity)
     (:*:)
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction
   Identity
   ((:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
 -> Construction
      Identity
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a)
 -> (:=)
      (Construction Identity <:.:> Construction Identity)
      (:*:)
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a))
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
-> (:=)
     (Construction Identity <:.:> Construction Identity)
     (:*:)
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> (:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
move (forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate 'Left) struct =>
struct ~> Morphing ('Rotate 'Left) struct
rotate @Left) (Construction
   Identity
   ((:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
 -> (:=)
      (Construction Identity <:.:> Construction Identity)
      (:*:)
      ((:=)
         (Identity
          <:.:> ((Construction Identity <:.:> Construction Identity)
                 := (:*:)))
         (:*:)
         a))
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
-> (:=)
     (Construction Identity <:.:> Construction Identity)
     (:*:)
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# ((:=)
   (Identity
    <:.:> ((Construction Identity <:.:> Construction Identity)
           := (:*:)))
   (:*:)
   a
 -> (:=)
      (Identity
       <:.:> ((Construction Identity <:.:> Construction Identity)
              := (:*:)))
      (:*:)
      a)
-> Construction
     Identity
     ((:=)
        (Identity
         <:.:> ((Construction Identity <:.:> Construction Identity)
                := (:*:)))
        (:*:)
        a)
move (forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate 'Right) struct =>
struct ~> Morphing ('Rotate 'Right) struct
rotate @Right))

repeat :: a :=> Stream
repeat :: a :=> Construction Identity
repeat a
x = a
-> ((Identity :. Construction Identity) := a)
-> Construction Identity a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Identity :. Construction Identity) := a)
 -> Construction Identity a)
-> (Construction Identity a
    -> (Identity :. Construction Identity) := a)
-> Construction Identity a
-> Construction Identity a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Identity a -> (Identity :. Construction Identity) := a
forall a. a -> Identity a
Identity (Construction Identity a -> Construction Identity a)
-> Construction Identity a -> Construction Identity a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a :=> Construction Identity
forall a. a :=> Construction Identity
repeat a
x