This is the artefact of the paper "Time Aware Compilation Verified: A Category-Theoretic Approach in Rocq" invited at MEMOCODE 2025.

It consists of Rocq source files with a Makefile. 
Just type  make in the source directory to compile.

This has been tested with Rocq version 9.0.0.

####
List of files:

Monoid.v
TimeDomain.v

Category.v: About Cateogies
Ens.v: About the category of Set
NT.v: About natural transformations
Op.v: About operators on category
Functor.v: About functors

Comonad.v: About Comonads
Monad.v: About Monads
MonadEns.v: About Monads in the Ens category
Kleisli.v: About Kleisli category
Falgebra.v: About Falgebra and EilenbergMoore category
Fcoalgebra.v: About Fcoalgebra and CoEilenbergMoore category

MActionFunctor.v: Functor for the delay monad
MActionMonad.v: Delay Monad 

EvolutionFunctor.v: About the Evolution functor
EvolutionComonad.v: About the Evolution comonad

Wcoalgebra.v: About W-coalgebras
Malgebra.v: About M-algberas
DistrLawMW.v: About N distributive law
Bialgebra.v: About N-bialgebra

DistrLawMActEvolution.v: About distributive law of the Delay monad over the Evolution comonad
BiAction.v: BiAlgebra for the Delay denotational semantics and the Evolution operational semantics


