{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
module Data.Universal where
import Prelude hiding (Functor (..))
import Control.Categorical.Functor
import Control.Category.Const2
import Data.Functor.Const
class Functor s t f => Universal (s :: α -> α -> *) (t :: β -> β -> *) (x :: β) (f :: α -> β) where
type Element s t x f :: α
morphism :: Const (t x (f (Element s t x f))) s
universal :: t x (f a) -> s (Element s t x f) a
instance Universal (Const2 () :: () -> () -> *) (->) () (Const ()) where
type Element (Const2 ()) (->) () (Const ()) = '()
morphism = Const Const
universal = \ _ -> Const2 ()