Test.idr

module Main

import Interfaces.Verified as V
import Control.Isomorphism

%hide Category
%hide Control.Category.Category
%default total

interface Category (cat : t -> t -> Type) where
  id  : cat a a
  (.) : cat b c -> cat a b -> cat a c

interface Category cat => Groupoid (cat : t -> t -> Type) where
  flip : cat a b -> cat b a

interface Category cat => HasInitialObject (cat : t -> t -> Type) where
  initial : t
  initiate : cat initial a

interface Category cat => HasTerminalObject (cat : t -> t -> Type) where
  terminal : t
  terminate : cat a terminal

data NatT : (f : t -> Type) -> (g : t -> Type) -> Type where
  MkNatT : ((a : t) -> f a -> g a) -> NatT f g

-- implementation Category NatT where
--   id = MkNatT (\a, x => x)
--   (.) x y = ?Category_rhs_2

implementation Category Iso where
  id    = isoRefl
  x . y = isoTrans y x

implementation Groupoid Iso where
  flip = isoSym

data FreeAlt : (f: Type -> Type) -> (a : Type) -> Type where
  Pure : a -> FreeAlt f a
  Ap   : f b -> (f b -> a) -> FreeAlt f a
  Alt  : List (f b) -> (f b -> a) -> FreeAlt f a

implementation Functor (FreeAlt f) where
  map f (Pure x) = Pure (f x)
  map f (Ap y g) = Ap y (f . g)
  map f (Alt xs g) = Alt xs (f . g)

implementation Applicative (FreeAlt f) where
  pure a = Pure a
  (<*>) (Pure f) fa = ?holeApplyApplicative_1
  (<*>) (Ap y f) fa = ?holeApplyApplicative_2
  (<*>) (Alt xs f) fa = ?holeApplyApplicative_3