package object types {

  import scala.language.reflectiveCalls
  import scala.language.higherKinds

  // quantifiers aka (co)ends
  type Forall[+F[_]] = { def apply[X]: F[X] }
  type Exists[+F[_]] = F[_]

  // basic categorical notions
  type ~>[-F[_], +G[_]] = Forall[λ[ X => (F[X]=>G[X]) ]]
  type Id[+X] = X
  type Comp  [F[ _], G[ _],  X] = F[G[X]]
  type CompPP[F[+_], G[+_], +X] = F[G[X]]
  type CompPM[F[+_], G[-_], -X] = F[G[X]]
  type CompMP[F[-_], G[+_], -X] = F[G[X]]
  type CompMM[F[-_], G[-_], +X] = F[G[X]]

  // Kan extensions
  type Ran[-G[_], +H[_], +A] = Forall[λ[ B => ((A=>G[B])=>H[B]) ]]
  type Lan[-G[_], +H[_], +A] = Exists[λ[ B =>  (G[B]=>A, H[B])  ]]

  // TODO: Kan lifts, http://ncatlab.org/nlab/show/Kan+lift

  // conversions to functor
  type Yoneda[+F[_], +A]   = Ran[Id, F, A]
  type Coyoneda[+F[_], +A] = Lan[Id, F, A]

  // monads via Kan exts
  type Codensity[F[_], +A] = Ran[F, F, A]
  type Density  [F[_], +A] = Lan[F, F, A]

  // basic (co)limit objects
  type Initial  = Forall[Id] // = `Nothing`
  type Terminal = Exists[Id] // sorry, not `Unit` but `Any` (terminal in cat of subtypes)

  // (co)inductive types, general
  type FreeMonad    [+F[_], +A] = Forall[λ[ X => ((A=>X, F[X]=>X)=>X) ]]
  type CofreeComonad[+F[_], +A] = Exists[λ[ X =>  (X=>A, X=>F[X], X)  ]]

  // (co)inductive types, basic
  //  type InitialAlg[+F[_]] = FreeMonad[F, Initial]
  //  type TerminalCoalg[+F[_]] = CofreeComonad[F, Terminal]
  type InitialAlg   [+F[_]] = Forall[λ[ X => ((F[X]=>X)=>X) ]]
  type TerminalCoalg[+F[_]] = Exists[λ[ X =>  (X=>F[X], X)  ]]

}