{-# 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