Representation

Sums

data Void p1 p0

data family N dc :: * -> * -> *

data (a :+: b) p1 p0

data C dc r p1 p0

Products

data U p1 p0

data (a :*: b) p1 p0

Fields

data T0 v t p1 p0

data T1 v t a p1 p0

data T2 v t b a p1 p0

data Variety

data Par1 p1 p0

data Par0 p1 p0

Conversions to and from fields-of-products structure

type family Rep t :: * -> * -> *

class Generic dc

Auxilliaries

class WN dc

class FoldPlusW' s

type family DistMaybePlus a b :: Maybe (* -> * -> *)

type family Tag dc :: Digit

type family Codomain dc :: k

type family Codomain0 dcs :: *

type family Codomain1 dcs :: * -> *

type family Codomain2 dcs :: * -> * -> *

data DTPos k

type family DTs t :: DTPos k

type NumDTs t

type family NumDTs' t :: Nat

type SiblingDTs t

type family SiblingDTs' t dpos :: [k]

class DC dc

type family DCs t :: * -> * -> *

class DT t

type family Eval r :: *

data SubstSpec star

type family Subst spec r :: * -> * -> *

type Subst0 t p0

type Subst1 t p1

type Subst10 t p1 p0

Building fields type consumers

Operations on disbanded data types

disbanded

class AreDCsOf t dcs

band

precise_case0

Operations on sums of fields types

type family sum :-: sum2 :: * -> * -> *

class Embed sub sup

class Partition sup subL subR

Forgetting `yoko`'s extra structure

reps

class EachGeneric sum

type family EachRep sum :: * -> * -> *

ig_from