Congruence rule plays an important role in reasoning in Agda, and things become mystery as working under heterogeneous equality. In the standard library of Agda2, the type of Relation.Binary.HeterogeneousEquality.cong is

`∀{a b} (f : a → b) {i : a} {j : a} → i ≅ j → f i ≅ f j`

Since i and j are the same type, the equality between i and j becomes propositional instead of heterogeneous. Continue reading