IrrelevantMatchRefl.agda:59,11-15
D != D → D of type Set
when checking that the expression refl has type K∞ ≡ abs (λ y → K∞)