Pullbacks in (dependent) haskell

Pullback.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE GADTs #-}
module Pullbacks where

import Data.Kind

---------------------------
-- Singleton boilerplate --
---------------------------

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@

type family Sing :: k -> Type

---------------------
-- Natural Numbers --
---------------------

data Nat = Z | S Nat
data SNat n where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

type instance Sing = SNat

type family (+) (a :: Nat) (b :: Nat) :: Nat where
    Z + m     = m
    (S n) + m = S (n + m)

type family (*) (a :: Nat) (b :: Nat) :: Nat where
    Z * m     = Z
    (S n) * m = m + (n * m)

data Plus2 :: Nat ~> Nat
data Times2 :: Nat ~> Nat

type Two = 'S ('S 'Z)

type instance Apply Plus2 n = Two + n
type instance Apply Times2 n = Two * n


plus :: Sing n -> Sing m -> Sing (n + m)
plus SZ n = n
plus (SS n) m = SS (n `plus` m)   

times :: Sing n -> Sing m -> Sing (n * m)
times SZ n = SZ
times (SS n) m = m `plus` (n `times` m)

-------------------
-- Identity type --
-------------------

data (a :: k) :~: (b :: k) where
    Refl :: a :~: a

------------------------------
-- Pullbacks and Equalizers --
------------------------------

data Equalizer (a :: Type) (b :: Type) (f :: a ~> b) (g :: a ~> b) :: Type where
    Equalizer :: forall a b f g e. Sing (e :: a) -> (f @@ e) :~: (g @@ e) -> Equalizer a b f g

type family Fst (e :: (a, b)) :: a where
    Fst '(a,b) = a

type family Snd (e :: (a, b)) :: b where
    Snd '(a,b) = b

data Pullback (a :: Type) (b :: Type) (c :: Type) (f :: a ~> c) (g :: b ~> c) :: Type where
    Pullback :: forall a b c f g e. Sing (e :: (a, b)) -> (f @@ (Fst e)) :~: (g @@ (Snd e)) -> Pullback a b c f g


-- CaTeGoRy tHeOrY Is sO SiMpLe
eq :: Equalizer Nat Nat Plus2 Times2
eq = Equalizer (SS (SS SZ)) Refl