In general I think people do study this sort of rule; Noam can probably say more. It’s tricky because not all type formers are covariant, e.g. function types are contravariant in one argument. The way coercions are implemented in Coq, which is the one I’m most familiar with, this would *not* be allowed.

I was wondering over here about something like:

$\frac {\vdash a, b: A \;\;\; \vdash p:Id_A(a,b) \;\;\; \vdash A \lt_{c} B : Type}{\vdash p: Id_B (a, b)}?$In general, with a $c: A \to B$, there would be a type $Id_B(c(a), c(b))$. With coercion, I’m allowed to rewrite this as $Id_B(a, b))$?

Then term elimination should allow me to pass from $p:Id_A(a,b)$ to $J(p): Id_B(a, b)$, for some function $J$?

Then I could coerce from $Id_A(a,b)$ to $Id_B(a, b)$, so call the $J(p)$ simply $p$?

]]>Thanks!

]]>I went ahead and inserted this (slightly augmented) material into the Idea section, and also added a sketch of Reynolds’ proof of coherence.

]]>Great! By all means, paste this into the entry.

]]>Re: #4, I would put things a little differently, and I would actually delay speaking of dependent types and HoTT until after the Idea section.

First, coherence is something that can hold for a particular style of *semantics* of a type system, rather than for a type system itself. In particular, whenever you have a type system with a non-trivial subtyping relation, it is pertinent to consider the meaning of the subsumption rule:

One potential reading is that the types $A$ and $B$ denote *properties* of terms, in which case the rule is read as applying an entailment between properties $A \le B$ to go from the fact that $e$ satisfies $A$ to the fact that $e$ also satisfies $B$. This is what Reynolds calls an “extrinsic semantics” of the type system, since terms have a meaning independently of types. Under such a style of semantics the question of coherence does not arise, but it commits you to interpreting “untyped” terms, which might not be what you want to do (I put “untyped” in quotes because that’s the traditional way of putting things, but as usual, it can be taken to mean “uni-typed”, or better, “more coarsely-typed”).

On the other hand, in what Reynolds calls an “intrinsic semantics”, meanings are assigned to typing judgments rather than to untyped terms. Under this style of semantics, the subsumption rule is seen as introducing an implicit coercion — or more formally, the rule is interpreted as constructing a generalized element $[[e:B]]$ of $[[B]]$, by composing a generalized element $[[e:A]]$ of $[[A]]$ with a map $[[A\le B]] : [[A]]\to [[B]]$. Since both of these actually come from interpreting *derivations* of the premises $e:A$ and $A \le B$, this is where the question of coherence arises – if the type system allows for multiple derivations of the same judgment, we better make sure that their meanings are identified by the intrinsic semantics.

In the 2000 paper, Reynolds gave a very elegant proof of coherence for an intrinsic semantics of a language with subtyping, by showing how it can be factored by way of an extrinsic semantics (this is his “bracketing theorem”, Theorem 5.7 on p.28).

I believe that this perspective on the general problem of coherence should be compatible with the specific kind of system of coercions described by Luo in those references cited in the article, though I disagree strongly with some of the things written there (e.g., in the SALT 2010 paper, “subsumptive subtyping is incompatible with canonicity and cannot be employed in a modern type theory”). On the other hand, what makes this trickier to apply to dependent types is that as far as I know nothing like Reynolds’ bracketing theorem has been considered in that setting.

]]>Do people also think of $Prop$ and $Set$ within $Type$ as a coercion?

]]>Ok – there’s nothing specific to HoTT about that, but we could certainly mention that the inclusion of a smaller universe in a larger one is often a coercion.

]]>I just meant the appearance of coercion in the HoTT book, e.g.,

]]>coercion, universe-raising, 54

What do you mean by “coercion in universes in HoTT”?

]]>Could we summarise what’s said in #2 and #3 as

All the coercions of a type system must be coherent in the sense that any two typing derivations of one type as a subtype of another must agree.

I’m sure you experts could say it properly.

Is it worth a mention of coercion in universes in HoTT?

]]>To put it a bit more abstractly, for a coercive semantics of a language with subtyping, the general property that you want is *coherence*: any two typing derivations of the same typing judgment have the same interpretation. A paper I highly recommend exploring these issues is John Reynolds’ The Meaning of Types: From Intrinsic to Extrinsic Semantics (see in particular his Definition 2.2).

I don’t think it’s anything about $c$ itself; you just want the collection of *all* coercions to form a commutative diagram, so there is no ambiguity.

Thought I should put some content into coercion. I’m sure it could be much better phrased. What should be said about the kind of $c:(A \to B)$ that can be used to coerce?

]]>