Data.Singletons.Prelude.Functor

Defines the promoted and singled versions of the Functor type class.

Documentation

class PFunctor f

Associated Types

type Fmap (arg :: (~>) a b) (arg :: f a) :: f b

type (arg :: a) <$ (arg :: f b) :: f a infixl 4

type a <$ a = Apply (Apply TFHelper_6989586621679559676Sym0 a) a

Instances

PFunctor []

Defined in Data.Singletons.Prelude.Monad.Internal

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Maybe

Defined in Data.Singletons.Prelude.Monad.Internal

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Min

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Max

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor First

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Last

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Option

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Identity

Defined in Data.Singletons.Prelude.Identity

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor First

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Last

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Dual

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Sum

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Product

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor Down

Defined in Data.Singletons.Prelude.Functor

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor NonEmpty

Defined in Data.Singletons.Prelude.Monad.Internal

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor (Either a)

Defined in Data.Singletons.Prelude.Monad.Internal

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor ((,) a)

Defined in Data.Singletons.Prelude.Functor

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor (Arg a)

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor (Proxy :: Type -> Type)

Defined in Data.Singletons.Prelude.Proxy

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

PFunctor (Const m :: Type -> Type)

Defined in Data.Singletons.Prelude.Const

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

class SFunctor f where

Minimal complete definition

sFmap

Methods

sFmap :: forall a b (t :: (~>) a b) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t :: f b)

(%<$) :: forall a b (t :: a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a) infixl 4

default (%<$) :: forall a b (t :: a) (t :: f b). (Apply (Apply (<$@#@$) t) t :: f a) ~ Apply (Apply TFHelper_6989586621679559676Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a)

Instances

SFunctor []

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sFmap :: forall a b (t :: a ~> b) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: [b]). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Maybe

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Maybe b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Min

Defined in Data.Singletons.Prelude.Semigroup

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Min b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Max

Defined in Data.Singletons.Prelude.Semigroup

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Max b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor First

Defined in Data.Singletons.Prelude.Semigroup

Methods

sFmap :: forall a b (t :: a ~> b) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: First b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Last

Defined in Data.Singletons.Prelude.Semigroup

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Last b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Option

Defined in Data.Singletons.Prelude.Semigroup

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Option b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Identity

Defined in Data.Singletons.Prelude.Identity

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Identity b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor First

Defined in Data.Singletons.Prelude.Monoid

Methods

sFmap :: forall a b (t :: a ~> b) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: First b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Last

Defined in Data.Singletons.Prelude.Monoid

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Last b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Dual

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Dual b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Sum

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Sum b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Product

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Product b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor Down

Defined in Data.Singletons.Prelude.Functor

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Down b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor NonEmpty

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sFmap :: forall a b (t :: a ~> b) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: NonEmpty b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor (Either a)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sFmap :: forall a0 b (t :: a0 ~> b) (t :: Either a a0). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a0 b (t :: a0) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor ((,) a)

Defined in Data.Singletons.Prelude.Functor

Methods

sFmap :: forall a0 b (t :: a0 ~> b) (t :: (a, a0)). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a0 b (t :: a0) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor (Arg a)

Defined in Data.Singletons.Prelude.Semigroup

Methods

sFmap :: forall a0 b (t :: a0 ~> b) (t :: Arg a a0). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a0 b (t :: a0) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor (Proxy :: Type -> Type)

Defined in Data.Singletons.Prelude.Proxy

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Proxy a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Proxy b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

SFunctor (Const m :: Type -> Type)

Defined in Data.Singletons.Prelude.Const

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Const m a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Const m b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

type family a $> a where ... infixl 4

Equations

a_6989586621679731605 $> a_6989586621679731607 = Apply (Apply (Apply FlipSym0 (<$@#@$)) a_6989586621679731605) a_6989586621679731607

(%$>) :: forall f a b (t :: f a) (t :: b). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply ($>@#@$) t) t :: f b) infixl 4

type family a <$> a where ... infixl 4

Equations

a_6989586621679731623 <$> a_6989586621679731625 = Apply (Apply FmapSym0 a_6989586621679731623) a_6989586621679731625

(%<$>) :: forall a b f (t :: (~>) a b) (t :: f a). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<$>@#@$) t) t :: f b) infixl 4

type family a <&> a where ... infixl 1

Equations

as <&> f = Apply (Apply (<$>@#@$) f) as

(%<&>) :: forall f a b (t :: f a) (t :: (~>) a b). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<&>@#@$) t) t :: f b) infixl 1

type family Void a where ...

Equations

Void x = Apply (Apply (<$@#@$) Tuple0Sym0) x

sVoid :: forall f a (t :: f a). SFunctor f => Sing t -> Sing (Apply VoidSym0 t :: f ())

Defunctionalization symbols

data FmapSym0 a6989586621679559667

Instances

SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing FmapSym0

SuppressUnusedWarnings (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

suppressUnusedWarnings :: ()

type Apply (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679559667 :: a ~> b)

Defined in Data.Singletons.Prelude.Monad.Internal

type Apply (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679559667 :: a ~> b) = FmapSym1 a6989586621679559667 :: TyFun (f a) (f b) -> Type

data FmapSym1 a6989586621679559667 a6989586621679559668

Instances

(SFunctor f, SingI d) => SingI (FmapSym1 d :: TyFun (f a) (f b) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (FmapSym1 d)

SuppressUnusedWarnings (FmapSym1 a6989586621679559667 :: TyFun (f a) (f b) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

suppressUnusedWarnings :: ()

type Apply (FmapSym1 a6989586621679559667 :: TyFun (f a) (f b) -> Type) (a6989586621679559668 :: f a)

Defined in Data.Singletons.Prelude.Monad.Internal

type Apply (FmapSym1 a6989586621679559667 :: TyFun (f a) (f b) -> Type) (a6989586621679559668 :: f a) = FmapSym2 a6989586621679559667 a6989586621679559668

type FmapSym2 (a6989586621679559667 :: (~>) a b) (a6989586621679559668 :: f a) = Fmap a6989586621679559667 a6989586621679559668 :: f b

data (<$@#@$) a6989586621679559672 infixl 4

Instances

SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<$@#@$)

SuppressUnusedWarnings ((<$@#@$) :: TyFun a (f b ~> f a) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

suppressUnusedWarnings :: ()

type Apply ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) (a6989586621679559672 :: a)

Defined in Data.Singletons.Prelude.Monad.Internal

type Apply ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) (a6989586621679559672 :: a) = (<$@#@$$) a6989586621679559672 :: TyFun (f b) (f a) -> Type

data a6989586621679559672 <$@#@$$ a6989586621679559673 infixl 4

Instances

(SFunctor f, SingI d) => SingI ((<$@#@$$) d :: TyFun (f b) (f a) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((<$@#@$$) d)

SuppressUnusedWarnings ((<$@#@$$) a6989586621679559672 :: TyFun (f b) (f a) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

suppressUnusedWarnings :: ()

type Apply ((<$@#@$$) a6989586621679559672 :: TyFun (f b) (f a) -> Type) (a6989586621679559673 :: f b)

Defined in Data.Singletons.Prelude.Monad.Internal

type Apply ((<$@#@$$) a6989586621679559672 :: TyFun (f b) (f a) -> Type) (a6989586621679559673 :: f b) = a6989586621679559672 <$@#@$$$ a6989586621679559673

type (<$@#@$$$) (a6989586621679559672 :: a) (a6989586621679559673 :: f b) = (<$) a6989586621679559672 a6989586621679559673 :: f a infixl 4

data ($>@#@$) a6989586621679731612 infixl 4

Instances

SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing ($>@#@$)

SuppressUnusedWarnings (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

suppressUnusedWarnings :: ()

type Apply (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) (a6989586621679731612 :: f a)

Defined in Data.Singletons.Prelude.Functor

type Apply (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) (a6989586621679731612 :: f a) = ($>@#@$$) a6989586621679731612 :: TyFun b (f b) -> Type

data a6989586621679731612 $>@#@$$ a6989586621679731613 infixl 4

Instances

(SFunctor f, SingI d) => SingI (($>@#@$$) d :: TyFun b (f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (($>@#@$$) d)

SuppressUnusedWarnings (($>@#@$$) a6989586621679731612 :: TyFun b (f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

suppressUnusedWarnings :: ()

type Apply (($>@#@$$) a6989586621679731612 :: TyFun b (f b) -> Type) (a6989586621679731613 :: b)

Defined in Data.Singletons.Prelude.Functor

type Apply (($>@#@$$) a6989586621679731612 :: TyFun b (f b) -> Type) (a6989586621679731613 :: b) = a6989586621679731612 $>@#@$$$ a6989586621679731613

type ($>@#@$$$) (a6989586621679731612 :: f a) (a6989586621679731613 :: b) = ($>) a6989586621679731612 a6989586621679731613 :: f b infixl 4

data (<$>@#@$) a6989586621679731630 infixl 4

Instances

SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (<$>@#@$)

SuppressUnusedWarnings ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

suppressUnusedWarnings :: ()

type Apply ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679731630 :: a ~> b)

Defined in Data.Singletons.Prelude.Functor

type Apply ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679731630 :: a ~> b) = (<$>@#@$$) a6989586621679731630 :: TyFun (f a) (f b) -> Type

data a6989586621679731630 <$>@#@$$ a6989586621679731631 infixl 4

Instances

(SFunctor f, SingI d) => SingI ((<$>@#@$$) d :: TyFun (f a) (f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing ((<$>@#@$$) d)

SuppressUnusedWarnings ((<$>@#@$$) a6989586621679731630 :: TyFun (f a) (f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

suppressUnusedWarnings :: ()

type Apply ((<$>@#@$$) a6989586621679731630 :: TyFun (f a) (f b) -> Type) (a6989586621679731631 :: f a)

Defined in Data.Singletons.Prelude.Functor

type Apply ((<$>@#@$$) a6989586621679731630 :: TyFun (f a) (f b) -> Type) (a6989586621679731631 :: f a) = a6989586621679731630 <$>@#@$$$ a6989586621679731631

type (<$>@#@$$$) (a6989586621679731630 :: (~>) a b) (a6989586621679731631 :: f a) = (<$>) a6989586621679731630 a6989586621679731631 :: f b infixl 4

data (<&>@#@$) a6989586621679731619 infixl 1

Instances

SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (<&>@#@$)

SuppressUnusedWarnings ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

suppressUnusedWarnings :: ()

type Apply ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) (a6989586621679731619 :: f a)

Defined in Data.Singletons.Prelude.Functor

type Apply ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) (a6989586621679731619 :: f a) = (<&>@#@$$) a6989586621679731619 :: TyFun (a ~> b) (f b) -> Type

data a6989586621679731619 <&>@#@$$ a6989586621679731620 infixl 1

Instances

(SFunctor f, SingI d) => SingI ((<&>@#@$$) d :: TyFun (a ~> b) (f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing ((<&>@#@$$) d)

SuppressUnusedWarnings ((<&>@#@$$) a6989586621679731619 :: TyFun (a ~> b) (f b) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

suppressUnusedWarnings :: ()

type Apply ((<&>@#@$$) a6989586621679731619 :: TyFun (a ~> b) (f b) -> Type) (a6989586621679731620 :: a ~> b)

Defined in Data.Singletons.Prelude.Functor

type Apply ((<&>@#@$$) a6989586621679731619 :: TyFun (a ~> b) (f b) -> Type) (a6989586621679731620 :: a ~> b) = a6989586621679731619 <&>@#@$$$ a6989586621679731620

type (<&>@#@$$$) (a6989586621679731619 :: f a) (a6989586621679731620 :: (~>) a b) = (<&>) a6989586621679731619 a6989586621679731620 :: f b infixl 1

data VoidSym0 a6989586621679731603

Instances

SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing VoidSym0

SuppressUnusedWarnings (VoidSym0 :: TyFun (f a) (f ()) -> Type)

Defined in Data.Singletons.Prelude.Functor

Methods

suppressUnusedWarnings :: ()

type Apply (VoidSym0 :: TyFun (f a) (f ()) -> Type) (a6989586621679731603 :: f a)

Defined in Data.Singletons.Prelude.Functor

type Apply (VoidSym0 :: TyFun (f a) (f ()) -> Type) (a6989586621679731603 :: f a) = VoidSym1 a6989586621679731603

type VoidSym1 (a6989586621679731603 :: f a) = Void a6989586621679731603 :: f ()

Orphan instances

SFunctor Down

Methods

sFmap :: forall a b (t :: a ~> b) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a b (t :: a) (t :: Down b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

PFunctor Down

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a

SFunctor ((,) a)

Methods

sFmap :: forall a0 b (t :: a0 ~> b) (t :: (a, a0)). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t)

(%<$) :: forall a0 b (t :: a0) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t)

PFunctor ((,) a)

Associated Types

type Fmap arg arg :: f b

type arg <$ arg :: f a