PresheafExample.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wall -Werror #-}

-- | Take the category with 2 objects 1 and 2 and one arrow between then 1 -> 2 .
--
-- This is equivalent to the poset 1 <= 2 .
--
-- Take a presheaf that sends 2 to the set of strings {\"cat\"}  and 1  to the set of strings {\"animal\", \"vegetable\"} .
--
-- The restriction function is defined so that \"cat\" | 1 = \"animal\"  .
--
-- How can we define this in haskell?
module Data.Valuation.Example.PresheafExample where

import Data.Kind (Type)
import Data.Semigroupoid (Semigroupoid (..))
import Data.Valuation.Presheaf (Presheaf (..), runPresheaf)

-- Objects of the category
data Obj = One | Two deriving (Eq, Show)

-- Morphisms (finite category)
data Cat :: Obj -> Obj -> Type where
  Id1 :: Cat 'One 'One
  Id2 :: Cat 'Two 'Two
  OneToTwo :: Cat 'One 'Two

instance Semigroupoid Cat where
  Id1 `o` Id1 = Id1
  Id2 `o` Id2 = Id2
  OneToTwo `o` Id1 = OneToTwo
  Id2 `o` OneToTwo = OneToTwo

-- Values associated with each object
data OneVal = Animal | Vegetable deriving (Eq, Show)

data TwoVal = Cat deriving (Eq, Show)

-- GADT for the presheaf object mapping
data F :: Obj -> Type where
  FOne :: OneVal -> F 'One
  FTwo :: TwoVal -> F 'Two

-- Example presheaf
presheafExample :: Presheaf Cat (->) F
presheafExample = Presheaf go
  where
    go :: Cat a b -> F b -> F a
    -- identities
    go Id1 x = x
    go Id2 x = x
    -- restriction along One -> Two
    go OneToTwo (FTwo Cat) = FOne Animal

-- Add Show instance for F
instance Show (F 'One) where
  show (FOne x) = show x

instance Show (F 'Two) where
  show (FTwo x) = show x

-- Example usage
example :: F 'One
example = runPresheaf presheafExample OneToTwo (FTwo Cat)