azul on Nostr: not saying that this is what you're looking for, but, this reminds me of why i like ...

not saying that this is what you're looking for, but, this reminds me of why i like OTT (observational type theory). it's an intensional type theory with function extensionality (actually, the type (f = g : A -> B) reduces to (x: A) -> (f x = g x : B) depending on the version of OTT, iirc) and equality is proof irrelevant (and that simplification is part of why OTT works. type coercion is free because equality is based on observational equality and is proof irrelevant).