Rewriting arrows and paths along vertex equalities #
This files defines Hom.cast
and Path.cast
(and associated lemmas) in order to allow
rewriting arrows and paths along equalities of their endpoints.
Rewriting arrows along equalities of vertices #
@[simp]
Rewriting paths along equalities of vertices #
@[simp]