A. Corradini and F. Gadducci, An algebraic presentation of term graphs, via gsmonoidal categories, Applied Categorical Structures, vol.7, issue.4, pp.299-331, 1999.

A. Corradini and F. Rossi, Hyperedge replacement jungle rewriting for termrewriting systems and logic programming, Theoret. Comput. Sci, vol.109, issue.1-2, pp.7-48, 1993.

N. A. Danielsson and M. Daggit, Agda standard library, 2018.

B. Hoffmann and D. Plump, Dependently-typed formalisation of typed term graphs, Proc. of 6th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2011, EPTCS, vol.25, pp.38-53, 1991.

W. , Categories of coalgebras with monadic homomorphisms, CMCS 2014, vol.8446, pp.151-167, 2014.

W. , Graph transformation with symbolic attributes via monadic coalgebra homomorphisms. ECEASST, 71:5.1-5, vol.17, 2015.

W. Kahl and Y. Zhao, Dependently-typed formalisation of typed term graphs, Proc. Tenth International Workshop on Computing with Terms and Graphs, TERMGRAPH 2018, EPTCS, vol.288, pp.26-37, 2019.

U. , Towards a Practical Programming Language Based on Dependent Type Theory, Dept. Comp. Sci. and Eng, 2007.

A. M. Pitts, Categorical logic, Handbook of Logic in Computer Science, vol.5, pp.39-128, 2001.

Y. Zhao, A Machine-checked Categorial Formalisation of Term Graph Rewriting with Semantics Preservation, 2018.

Y. Zhao, A Formalisation of Term Graph Rewriting in Agda -TGR1. Mechanically checked Agda development, 2018.