Propositional equality works but sometimes it obscures some structure about
the types we are manipulating, in particular, we are going to prove facts
about indexed types and in this situation, it is helpful to define a bespoke
type of equalities between indexed types.
should this replace be a transport?
If you do that everything breaks
Definition
Indexed propositional equality is in habited provided the indexed type is the
same on both sides and we have a proof that the index is the same.
data (≡≡) : {0 a : Type} -> {0 p : a -> Type} -> {0 i, j : a} -> p i -> p j -> Type where IRefl : {0 i, j : a} -> {0 v : p i} -> (0 prf : i === j) -> (≡≡) {i} {j} v (replace {p} prf v)