Equality In HoTT, equality type of a coinductive type is Bisimulation. References damato2025-formalizing-containers