As mentioned by Andrej, this is an instance of transporting along an equivalence of families and display maps. In this specific case, we have an equivalence of graphs and relations.
open import Function
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Level renaming (zero to lzero; suc to lsuc)
-- type of relations on a ...
OCaml and Scala are popular choices for types systems, but they are by no means the only languages you can write a compiler, interpreter, typechecker, or type system in.
Type-checking involves traversing syntax trees representing terms and types. Languages with some form of algebraic data type make this easy, since these traversals can be defined using ...