Good syntax/approach for small category theory example?

Stream: lean4

[Mark Wilhelm]

-- Trying to encode the example in:
-- Section 3.4.1 Pulling Back Data along a Functor
-- From "Seven Sketches in Compositionality"
-- https://arxiv.org/pdf/1803.05316.pdf
-- They show a small example of an instance functor on the category of Discrete Dynamica Systems getting
-- pulled back to the category of Graphs

-- I'm not sure what to use for the type of the output of last function shown below
-- and/or I think I'm just not approaching this in the right way
-- Would love some pointers if anybody has time to look -- thanks!

-- I believe there is no category theory in mathlib4 yet, but all I'm trying to do at the moment
-- is make the types that could be used to "fill out" a particular instance of Category for this
-- small example (not trying to define the category typeclass itself). I run into an issue with
-- the definition of the morphism portion of the instance functor, shown below.

-- Object in the Graph category
inductive GrObj where
| Arrow
| Vertex
open GrObj

-- Morphism in the Graph category
inductive GrMor: GrObj -> GrObj -> Type where
| id_Arrow: GrMor Arrow Arrow
| id_Vertex: GrMor Vertex Vertex
| source: GrMor Arrow Vertex
| target: GrMor Arrow Vertex
| gcom: GrMor Arrow Vertex -> GrMor Arrow Vertex -> GrMor Arrow Vertex
infixl:65   " ;_gr " => GrMor.gcom
open GrMor

-- Object in the Discrete Dynamical System category
inductive DDSObj where
| State
open DDSObj

-- Morphism in the Discrete Dynamical System category
inductive DDSMor: DDSObj -> DDSObj -> Type where
| id_State: DDSMor State State
| next: DDSMor State State
| dcom: DDSMor State State -> DDSMor State State -> DDSMor State State
infixl:65   " ;_dds " => DDSMor.dcom
open DDSMor

-- I think no Set in lean4, so try just using an imagined category of Lists of Strings...
-- Object in the List Of Strings category
def ListObj := List String

-- Morphism in the List Of Strings category
inductive ListMor: ListObj -> ListObj -> (String -> String) -> Type where
| lid: (l: ListObj) -> ListMor l l λ s => s
| lfn: (l1: ListObj) -> (l2: ListObj) -> (f: String -> String) -> ListMor l1 l2 f
| lcom: ListMor l1 l2 f -> ListMor l2 l3 g -> ListMor l1 l3 λ s => g (f s)
infixl:65   " ;_lst " => ListMor.lcom
open ListMor

-- Object part of an Instance functor from Graph -> ListOfStrings
def IObj (d: DDSObj): ListObj :=
  match d with
  | State => ["one", "two", "three", "four", "five", "six", "seven"]

-- Morphism part of an Instance functor from Graph -> ListOfStrings (incomplete, has error)
-- def IMor {d1 d2: DDSObj} (f: DDSMor d1 d2): ListMor (IObj d1) (IObj d2) (String -> String) :=
def IMor {d1 d2: DDSObj} {sfn: String -> String} (f: DDSMor d1 d2): ListMor (IObj d1) (IObj d2) sfn :=
  let l1: ListObj := IObj d1
  let l2: ListObj := IObj d2
  match f with
  | id_State => ListMor.lid l1

-- error message --
-- d1d2: DDSObj
-- sfn: String → String
-- f: DDSMor d1 d2
-- l1: ListObj
-- l2: ListObj
-- ⊢ ListObj
-- Messages (1)
-- pullback.lean:60:16
-- type mismatch
--   lid l1
-- has type
--   ListMor l1 l1 fun s => s : Type
-- but is expected to have type
--   ListMor (IObj d1) (IObj d2) sfn : Type