Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: coercion

Bottom of Page

1 to 14 of 14

  1.  
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 6th 2015

    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→B)c:(A \to B) that can be used to coerce?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 6th 2015

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

  3. 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).

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 7th 2015

    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?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 7th 2015

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

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 7th 2015

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

    coercion, universe-raising, 54

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 8th 2015

    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.

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 8th 2015

    Do people also think of PropProp and SetSet within TypeType as a coercion?

    • CommentRowNumber9.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeFeb 8th 2015
    • (edited Feb 8th 2015)

    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:

    e:AA≤Be:B\frac{e:A \qquad A \le B}{e:B}

    One potential reading is that the types AA and BB denote properties of terms, in which case the rule is read as applying an entailment between properties A≤BA \le B to go from the fact that ee satisfies AA to the fact that ee also satisfies BB. 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]][[e:B]] of [[B]][[B]], by composing a generalized element [[e:A]][[e:A]] of [[A]][[A]] with a map [[A≤B]]:[[A]]→[[B]][[A\le B]] : [[A]]\to [[B]]. Since both of these actually come from interpreting derivations of the premises e:Ae:A and A≤BA \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.

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 8th 2015

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

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

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 9th 2015

    Thanks!

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 13th 2015
    • (edited Feb 13th 2015)

    I was wondering over here about something like:

    ⊢a,b:A⊢p:Id A(a,b)⊢A< cB:Type⊢p:Id B(a,b)? \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→Bc: A \to B, there would be a type Id B(c(a),c(b))Id_B(c(a), c(b)). With coercion, I’m allowed to rewrite this as Id B(a,b))Id_B(a, b))?

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

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

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2015

    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.

1 to 14 of 14

  1.