Post #3183684

If A is subtype of A', let a : A, and define f : A' := a, should f : A hold judgmentally? How would you implement this? (subtyping can show up if you have subtyping-based cumulative universe)