Congruence Rule with Heterogeneous Equality in Agda

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