pub fn modal_mor_as_identity(mor: &ModalMor) -> Option<&ModalOb>Expand description
If mor is an identity morphism (Composite(Path::Id(ob))), returns the
object it is the identity on.
Instance-term normalization uses this to keep terms in their flat normal
form: an identity mor means the term denotes its base
directly, so a nested application whose argument is a pure base of
generators need not introduce a Composite/List wrapper.