gistfile1.txt

data o:Category where
  s:o ~> t:o
  f:b~>c ⚬ g:a~>b -> a~>c | x⚬y ⚬ z == x ⚬ y⚬z
  identity: a~>a | identity⚬f == f == f⚬identity

hask:Category where
  hask = Type
  (~>) = (->)
  (⚬) = (.)
  identity = id

cat:Category where
  cat = Category
  c~>d : Category where
    c~>d = F: c->d where
      F: a~>b -> F a ~> F b | F f⚬g == F f ⚬ F g && F identity == identity
    F:s~>t ≈> G:s~>t = η: F x ~> G x | η⚬f == f⚬η
    (~>) = (≈>)
  (⚬) = (.)
  identity = id

opposite c : Category where
  opposite = id
  (~>) = flip (~>)
  (⚬) = flip (⚬)
  identity = identity

yoneda: C ~> opposite C ~> hask where
  yoneda = flip (->) : C -> opposite C ~> hask where
    yoneda = flip (⚬) : a~>b -> b~>c -> a~>c
  yoneda = (⚬) : c~>d -> yoneda c ≈> yoneda d