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

Discussion Tag Cloud

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).
    • CommentRowNumber1.
    • CommentAuthorZhen Lin
    • CommentTimeSep 9th 2011

    I started an article about Martin-Löf dependent type theory. I hope there aren't any major mistakes!

    One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?

    • CommentRowNumber2.
    • CommentAuthorNeel Krishnaswami
    • CommentTimeSep 9th 2011
    • (edited Sep 9th 2011)
    This comment is invalid XML; displaying source. Dear Zhen Lin,<br /><br />In programming languages research (closely connected to, but not quite the same as, type theory) $\mathrm{case}$ is the usual name of the finite sum type. However, the dependent sum type is usually given a projective elimination:<br /><br /><img src="/extensions/vLaTeX/cache/latex_e347ec5f74fb4fb8e72ac63ece801330.png" title="\begin{matrix}<br />\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}<br /> {\Gamma \;\vdash\; \pi_1(t) \;:\; A}<br />\\<br />\\<br />\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}<br /> {\Gamma \;\vdash\; \pi_2(t) \;:\; B[\pi_1(t)/a]}<br />\end{matrix}<br />" style="vertical-align:-20%;" class="tex" alt="\begin{matrix}<br />\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}<br /> {\Gamma \;\vdash\; \pi_1(t) \;:\; A}<br />\\<br />\\<br />\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}<br /> {\Gamma \;\vdash\; \pi_2(t) \;:\; B[\pi_1(t)/a]}<br />\end{matrix}<br />" /><br /><br />My understanding is that this formulation is equivalent to, but has a slightly simpler metatheory than, the $\mathrm{cases}$ form given in your article.
  1. This comment worked in the preview...?
    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeSep 9th 2011
    • (edited Sep 9th 2011)

    Here’s Neel’s comment:

    Dear Zhen Lin,

    In programming languages research (closely connected to, but not quite the same as, type theory) case\mathrm{case} is the usual name of the finite sum type. However, the dependent sum type is usually given a projective elimination:

    Γt:Σa:A.BΓπ 1(t):A\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}{\Gamma \;\vdash\; \pi_1(t) \;:\; A}

     

    Γt:Σa:A.BΓπ 2(t):B[π 1(t)/a]\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}{\Gamma \;\vdash\; \pi_2(t) \;:\; B[\pi_1(t)/a]}

    My understanding is that this formulation is equivalent to, but has a slightly simpler metatheory than, the cases\mathrm{cases} form given in your article.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeSep 9th 2011

    @Zhen: Thanks!! I added the unit and empty types, which Martin-Lof obtains as special cases of finite types, and added a remark about how to get the other finite types from those. I also added some links and some comments about identity types and AC. Finally, I changed your remark about ex falso quodlibet to refer to excluded middle, since ex falso is just the eliminator of the empty type (Martin-Lof actually mentions this in the reference, when he gives the \bot-elimination rule).

    There are, of course, more type constructors in Martin-Lof’s paper than you’ve given here: he describes natural numbers, lists, W-types, and universes. Did you plan to expand this article to include those, and possibly more general inductive types and families? I’m not entirely sure exactly what collection of type-formers is officially called “Martin-Lof type theory”.

    @Neel: I suspect that Zhen wanted to stay close to the choices made in Martin-Lof’s original paper, where he uses the “cases” eliminator for dependent sums. I don’t have a problem with using the same name for the eliminators of binary sums and dependent sums, since both are after all special cases of inductive types.

    @Zhen and Neel: I think math tends to give the best results on the forum if you use the “Markdown+Itex” filter.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeSep 9th 2011

    There is an important difference between eliminating sum types through cases and eliminating them through projections. (This difference disappears in the presence of identity types, however, so possibly only I care about it.) This is analogous to the difference between the inductive types in Thierry Coquand’s Calculus of Inductive Constructions (perhaps best known through its implementation in the theorem prover Coq) and Martin-Löf’s WW-types (although the equivalence between these is more complicated).

    Categorially, at least when restricted to a sum of a constant family, the difference is that between a copower (a kind of colimit, elimination through cases) and a product (a kind of limit, elimination through the projection operators of the cone).

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeSep 9th 2011

    @Toby: I care about that too. I’ve gathered that it matters in syntactic study of type theory as well, e.g. the theory of “logical relations” has to treat the two cases differently (maybe one is called “positive” and the other “negative”, though I can never remember which is which). Maybe that is part of the “metatheory” Neel was referring to.

    I thought that Martin-Lof’s W-types were literally a special case of CiC’s inductive types, though — why do you say that that difference is analogous?

    • CommentRowNumber8.
    • CommentAuthorZhen Lin
    • CommentTimeSep 10th 2011

    @Mike:

    Is that (reflexivity, symmetry, and transitivity) a rule we are giving, or an assertion we are making about derivability?

    Hmmm. I’m not very sure. I believe it is derivable for the equality judgement in the presence of substitution rules (which I have omitted). On the other hand, in Maietti’s 2005 paper, Modular correspondence between dependent type theories and categories including pretopoi and topoi, she says

    […] we need to add all the inference rules that express the reflexivity, symmetry and transitivity of the equality between types and terms […] The structural rules of weakening, substitution and of a suitable exchange are not added since they are derivable.

    This is also the approach taken by Nordström, Petersson and Smith in their article Martin-Löf’s type theory. So perhaps it’s a matter of taste? As for distinguishing between the equality type and equality judgement, I must defer to the expertise of others here; I thought it might be neater to get rid of the equality judgement given that ‘I(A,a,b)trueI(A, a, b) \; \mathrm{true} is a judgement, which will turn out to be equivalent to a=bAa = b \in A’, according to Martin-Löf [1984].

    @Neel, @Toby:

    Maietti [2005] states,

    […] we will refer to an equivalent formulation of the lex calculus in which the elimination and conversion rules for the indexed sum type are replaced by projections satisfying β\beta and η\eta conversions. This formulation with projections is equivalent to that of the indexed sum type given previously, but only because of the presence of the extension equality type (see Martin-Löf (1984) for a proof of the equivalence), that is, the equivalence does not hold in the intensional version of Martin-Löf’s type theory […]

    Question: Why do we demand that the (extensional) equality type has at most one canonical inhabitant? This seems to be one of the differences between the equality type and the (intensional) identity type.

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeSep 10th 2011

    I thought that Martin-Lof’s W-types were literally a special case of CiC’s inductive types, though — why do you say that that difference is analogous?

    That is true; in fact, identity types and dependents sums are both themselves examples of CiC inductive types, and for that matter so is everything else other than dependent products. But I meant to focus only on those CiC inductive types that correspond directly to WW-types.

    On the other hand, I think that it was too strong to say that this is analogous. The elimination rule for all CiC inductive types is basically the same; they’re all eliminated by case analysis on the constructors, and Martin-Löf’s WW-type elimination rule is different, and correct only via using the identity types. However, it’s not really analogous to elimination by projection, so the analogy falls apart there.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeSep 10th 2011

    This formulation with projections is equivalent to that of the indexed sum type given previously, but only because of the presence of the extension equality type (see Martin-Löf (1984) for a proof of the equivalence), that is, the equivalence does not hold in the intensional version of Martin-Löf’s type theory

    That seems too strong to me; I’ll have to review the equivalence, which I thought worked even in the intensional version.

    Why do we demand that the (extensional) equality type has at most one canonical inhabitant?

    Because we’re not doing homotopy type theory, I guess!

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011
    • (edited Sep 10th 2011)

    Here’s what Martin-Lof gives as the W-elimination rule (p44 in my copy, p81 in the Bibliopolis version). I’ll write WW for the W-type defined from a dependent type x:AB(x):Typex\colon A \vdash B(x)\colon Type, which Martin-Lof writes as (𝒲xA)B(x)(\mathcal{W}x\in A)B(x), and sup for the constructor x:A,y:B(x)Wsup(x,y):Wx\colon A, y\colon B(x) \to W \vdash sup(x,y) \colon W. Here C is a type dependent on W.

    c:Wx:A,y:B(x)W,z:Π v:B(x)C(y(v))d(x,y,z):C(sup(x,y))something:C(c)\frac{\vdash c \colon W \qquad x\colon A, y\colon B(x) \to W, z\colon \Pi_{v\colon B(x)} C(y(v)) \vdash d(x,y,z)\colon C(sup(x,y)) }{ something \colon C(c) }

    Here’s some Coq:

    Parameter A : Type.
    Parameter B : A -> Type.
    
    Inductive W : Type :=
    | sup : forall a:A, (B a -> W) -> W.
    
    Check W_rect.
    

    which prints

    forall P : W -> Type,
      (forall (a : A) (w : B a -> W),
        (forall b : B a, P (w b)) -> P (sup a w)) -> 
      forall w : W, P w
    

    from which, applying some alpha-equivalence, we get

    forall C : W -> Type,
      (forall (x : A) (y : B x -> W),
        (forall v : B x, C (y v)) -> C (sup x y)) -> 
      forall c : W, C c
    

    which looks the same as Martin-Lof’s eliminator to me.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011

    Why do we demand that the (extensional) equality type has at most one canonical inhabitant?

    I would say that’s more or less the definition of “extensional”.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeSep 10th 2011

    Sorry, Mike, that’s my faulty memory. It’s not the WW-types per se, but those WW-types that CiC can implement without thinking of them as WW-types (that is, without having a constructor with “->” in it).

    For example, to construct \mathbb{N} (if you don’t already have it by hand) as a WW-type, you take (following your notation above) AA to be 1+11 + 1 and BB to be defined by cases, first 00 and next 11. So the eliminator is

    c:;x:1+1,y:B(x),z:Π v:B(x)C(y(v))d(x,y,z):C(sup(x,y))something:C(c). \frac {\vdash c\colon \mathbb{N}; \qquad x\colon 1 + 1, y\colon B(x) \to \mathbb{N}, z\colon \Pi_{v\colon B(x)} C(y(v)) \vdash d(x,y,z)\colon C(sup(x,y)) } { something \colon C(c) } .

    But a much simpler eliminator is

    c:;d:C(0);y:e(y):C(y +)something:C(c). \frac {\vdash c\colon \mathbb{N}; \qquad d\colon C(0); \qquad y\colon \mathbb{N} \vdash e(y)\colon C(y^+) } { something \colon C(c) } .

    And now I see no clear analogy, except this: I want to think of the latter eliminator as correct, and (IIRC) we need identity types to prove them equivalent.

    I should probably look at this in more detail, lest more of my memory be wrong.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011

    Toby: Ah, yes, I see. I didn’t realize you needed identity types for that equivalence. I just tried messing around in Coq, and I was able to prove without using equality that the CiC eliminator implies the W-type eliminator. But I couldn’t see how to do the other direction without assuming not just identity types but function extensionality!

    Gee, that’s bothersome. If that’s correct, it makes me much less happy about W-types. Maybe we ought to consider initial joint-algebras for finite families of polynomial endofunctors all the time instead.

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeSep 11th 2011

    without assuming not just identity types but function extensionality

    That fits with the quotation from Maietti above, even though I didn’t remember the need for extensionality.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2011

    I have edited the sub-section structure at Martin-Löf dependent type theory. Originally the section “Equality type” had lots of subsections, which I think was unintentional.

    Also I created a Properties-subsection, made “Axiom of choise” be subordinate to that and created a new subordinate section “Models” with a very brief remark on models for the extensional and the intensional version.

    Finally I added in the References a pointer to chapter 1 in Michael Warren’s PhD thesis, which I am finding a useful text to read.

    • CommentRowNumber17.
    • CommentAuthorbss
    • CommentTimeMay 22nd 2020
    Under "Binary Sum Types" the presentation looks untagged ("a : A + B" and "b : A + B"), I looked at one of the PDFs in the references section and it had tags ("i(a) : A + B" and "j(b) : A + B"). I'm new, should I try to make changes myself, or should I generally spark a discussion first and look for someone's approval? [See: https://twitter.com/DaTwinkDaddy/status/1263357410007117825 for more context.]
    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMay 22nd 2020

    This looks like a mistake to me; there should be tags. (Common tags are “inl” and “inr”.) If you can fix it that would be great!

    In general, I would say that whether to ask first or just make the edit depends on how confident you are that your change is correct! It’s never wrong to ask for approval first, although you can’t be guaranteed that someone will answer. If you’re pretty confident the change is right, you can go ahead and make it, but be sure to enter a changelog message so that people here will be notified in case someone disagrees.

    • CommentRowNumber19.
    • CommentAuthormaxsnew
    • CommentTimeDec 24th 2020

    Add explicit injections σ 0,σ 1\sigma_0,\sigma_1 to the binary sums.

    diff, v25, current

    • CommentRowNumber20.
    • CommentAuthormaxsnew
    • CommentTimeDec 24th 2020

    More (similar) binary sum edits.

    diff, v25, current

    • CommentRowNumber21.
    • CommentAuthorGuest
    • CommentTimeFeb 26th 2021
    The equality type I(A,a,b) in Martin-Löf was, in fact, actually meant as an internalization of the equality judgement a = b ∈ A, which is equivalent to the judgement r ∈ I(A,a,b), where "r" is the distinguished constant that Martin-Löf uses to represent the sole inhabitant of all inhabited equality types.

    This shows that the typed equality judgement, itself, actually isn't needed in the formalism since it is already subsumed by the equality type. Once you realize this, then you begin to see a much larger, more interesting and clearer picture which also shows a significant gap in the formalism - which when filled, directly links Martin-Löf theory to n-categories ... and exposes the true nature of the type theory that's been hiding in disguise.

    The first gap is that since the typed equality relation is already subsumed by the equality judgement, then there should also be a equality type for type judgements, so that types A = B if and only if the judgement type I(A,B) is inhabited. It's not clear why Martin-Löf failed to include this in his formalism; but I think it was just an oversight.

    Once it is included, then there is no longer a need to have any equality judgements in the theory, at all. Everything is reduced to type membership judgements.

    Second, Martin-Löf makes clear that the equality relation is to be reflexive, symmetric, transitive and is to also be a congruence. When expressed in terms of the equality types, these first set of conditions become:

    A type │ 1 ∈ I(A,A)
    A type, B type │ f ∈ I(A,B) ⇒ f⁻¹ ∈ I(B,A)
    A type, B type, C type │ f ∈ I(B,C), g ∈ I(A,B) ⇒ f∘g ∈ I(A,C)

    with a similar set of constructors for the reflexive, symmetric and transitive relations for typed judgements.

    This shows that we are actually dealing with a family of categories. First: the master category of all types whose objects are the types, themselves, and whose morphisms f: A→B are the members f ∈ I(A,B), for types A and B; Second, there is a category for each type A, whose objects are the members a∈A, and whose morphisms f: a→b, for a, b ∈ A are the members f ∈ I(A,a,b). So, overall, the master category has categories as its objects - it is a 2-category.

    The fact that it is a congruence, with the substitution of equals for equals rule shows that each of the operators in the Martin-Löf formalism is actually a functor. For instance, consider the following.

    If A is a type and B(x) is a type for each x ∈ A, then Σ(A,B) is a type. In this type, there is the pairing operator (a ∈ A, b ∈ B(a) ↦ (a,b) ∈ Σ(A,B)).

    The congruence rule states that if a=a' ∈ A, b=b' ∈ B(a), then (a,b)=(a',b') ∈ Σ(A,B). Expressed in terms of the equality types, it states that the pairing operator is actually a functor which applies also to the morphisms f ∈ I(A,a,a') and g ∈ I(B(a),b,b') to yield the morphism (f,g) ∈ I(Σ(A,B),(a,b),(a',b')). That is: if f: a → a' in A, and g: b → b' in B(a), then (f,g): (a,b) → (a',b') in Σ(A,B).

    The symmetry condition makes the arrows of each category reversible; so each category is also a groupoid. So, it's also a 2-groupoid if symmetry is included. If we eliminate symmetry, then this reduces to a category whose morphisms are the "reduction" relations of a reduction algebra.

    Martin-Löf requires that each equality type I(A,a,b) have at most one member (this member being called "r"). This corresponds to a "coherence condition" that if f: a→b and g: a→b then f = g. We could also extend this to include a set of coherence conditions for the equality types I(A,B).

    All of this reveals another gap: the usual categorical identities are absent; e.g. f∘1 = f = 1∘f ∈ I(A,B), for f ∈ I(A,B). Representing these in terms of the equality types gives us the elements of a monoidal category; λ(f) ∈ I(I(A,B),1∘f,f), ρ(f) ∈ I(I(A,b),f∘1,f) for f ∈ I(A,B); and α(f,g,h) ∈ I(I(A,D),f∘(g∘h), (f∘g)∘h), for f ∈ I(C,D), g ∈ I(B,C) and h ∈ I(A,B). For the composition, for coherence, we would then also add in the Triangle Diagram and Pentagon Diagram as "coherence identities".

    But the objects of the monoidal category are the morphisms, themselves and the product is the composition. So, reiterating the earlier observation: this is actually a 2-category in disguise.

    Since the I's can be nested to arbitrary depth, then this may even ramify up to 3-categories, 4-categories, etc.

    -- Lydia Marie Williamson
    • CommentRowNumber22.
    • CommentAuthorGuest
    • CommentTimeFeb 26th 2021
    A minor correction: in my last comment, I wrote ρ(f) ∈ I(I(A,b),f∘1,f). This should be ρ(f) ∈ I(I(A,B),f∘1,f).

    To answer Zhen-Lin's question: Martin-Löf used D.

    All of the non-canonical operators and canonical operators were given names by Martin-Löf. Excluding the universe types; this includes:
    ∙ λb = (λx)b(x) ∈ Π(A,B)
    ∙ (a,b) ∈ Σ(A,B)
    ∙ sup(a,b) ∈ W(A,B)
    ∙ i(a), j(b) ∈ A+B
    ∙ r ∈ I(A,a,b)
    ∙ 0 ∈ N,
    ∙ n ∈ N ↦ n' ∈ N
    ∙ m_n ∈ N_n, where 0 ≤ m < n ∈ N
    for canonical objects and operators; and
    ∙ Ap(c,d) = cd, for the type Π(A,B)
    ∙ E(c,d) for the type Σ(A,B)
    ∙ T(c,d) for the type W(A,B)
    ∙ D(c,d,e) for the type A+B
    ∙ J(c,d) for the type I(A,a,b) (this changed from version to version)
    ∙ R(c,
    • CommentRowNumber23.
    • CommentAuthoratmacen
    • CommentTimeFeb 27th 2021

    Re #21,22:

    Hello Lydia,

    I think you’re mostly rediscovering existing ideas, except there’s a well-known problem you’ve missed, which splits your proposal into two incompatible styles of type system.

    I will call equality expressed with a judgment “judgmental equality”, and equality expressed with the equality/identity types “typal equality”. (It has traditionally been called “propositional equality”, but that was arguably a bad idea.)

    The equality type I(A,a,b) in Martin-Löf was, in fact, actually meant as an internalization of the equality judgement a = b ∈ A,

    I believe you’re correct about this, but…

    which is equivalent to the judgement r ∈ I(A,a,b), where “r” is the distinguished constant that Martin-Löf uses to represent the sole inhabitant of all inhabited equality types.

    This is only true for variants of type theory with equality reflection. I will refer to these variants as having “reflective equality”. (They have traditionally been called “extensional type theories”, but that was arguably a bad idea. :))

    For a while, Martin-Löf wrote about versions of his type theory that included an equality reflection rule, making equality reflective by fiat. It turns out that this style of type theory is not amenable to the sort of direct implementation that Martin-Löf wanted. When he found out, he abandoned the equality reflection rule.

    Most proof assistants implementing type theory implement a variant without reflective equality. The basic starting point for most of these variants is called “intensional type theory”, since judgmental equality ends up being rather intensional. (And with equality reflection, judgmental equality is more extensional, hence the term “extensional type theory”. But equality reflection doesn’t imply any of the usual extensionality principles from set theory.)

    This shows that the typed equality judgement, itself, actually isn’t needed in the formalism since it is already subsumed by the equality type.

    You mean that judgmental equality implies typal equality? That is not enough to eliminate the equality judgment from the formal system, because it’s used in premises of rules, and typal equality does not provide a way to derive those premises. Only when typal equality also implies judgmental equality—which is exactly equality reflection—can you eliminate the equality judgment form.

    Even when studying type theory with reflective equality, it’s technically convenient to keep both judgmental and typal equality, as two ways of saying the same thing.

    But Nuprl formally has no equality judgments. All equality rules are about the equality types. This was from the mid 80’s, inspired my Martin-Löf’s type theory with equality reflection.

    […] a much larger, more interesting and clearer picture […] directly links Martin-Löf theory to n-categories … and exposes the true nature of the type theory that’s been hiding in disguise.

    Have you seen homotopy type theory? Yeah yeah, only \infty-groupoids. They’re working on it.

    The first gap is that since the typed equality relation is already subsumed by the equality judgement, then there should also be a equality type for type judgements, so that types A = B if and only if the judgement type I(A,B) is inhabited. It’s not clear why Martin-Löf failed to include this in his formalism; but I think it was just an oversight.

    Nuprl has added a type equality type constructor relatively recently. (2014, I think.) It’s not as straightforward as it might look. The problem is that now you have types like (I(A,B)N 0I(A,B) \to N_0), which ostensibly get you judgments you didn’t have before (in this case, that AA and BB are not equal), risking making the formal system too strong or inconsistent. The Nuprl guys avoided that issue in a slick and somehow disappointing way.

    Meanwhile, with universes, you already have that I(U n,A,B)I(U_n,A,B) corresponds to (A=BU nA = B \in U_n), which implies (A=BA = B) (with Russell-style universes, which is what Martin-Löf used at the time, and Nuprl uses).

    There’s also “extensional” type equality: the property that elements of one type are elements of the other. (So, a conversion-focused equality.) This turns out to be definable in Nuprl for reasons that might be considered awesome or horrifying.

    Once it is included, then there is no longer a need to have any equality judgements in the theory, at all. Everything is reduced to type membership judgements.

    By the way, it turns out that the type equality judgments aren’t actually all that important, formally. The important use case for them is the “conversion” rule:

    A=BtAtB\frac{A = B \qquad t \in A}{t \in B}

    So you can metamathematically consider types equal when you can derive all the consequent conversion instances. Then you look at all the ways of deriving type equality, other than with other type equalities, and make sure you can derive all the conversions without going through type equality.

    So in other words, using a type equality judgment form is the straightforward way, but there are shortcuts.

    If all (definable) types are contained in some universe, it’s particularly obvious that type equality isn’t needed. But it turns out you don’t really need universes. Nuprl has only type membership judgments.

    Second, Martin-Löf makes clear that the equality relation is to be reflexive, symmetric, transitive and is to also be a congruence. When expressed in terms of the equality types, these first set of conditions become […]

    This is where I think you’re mistaken. The implication that reflective equality is a useful way of talking about morphisms. With the JJ rule, equality reflection, and rules for judgmental equality, you can prove, internally, that any element of any equality is just the canonical rr constant. (I noticed you used your proposed type equality types, but I’m pretending you used universes. It shouldn’t make much difference, since you expect reflection for type equality.)

    So you can use elements of equality types as morphisms, but with equality reflection, they’re all trivial. All your categories are discrete categories (“sets”). In fact, equality reflection is not the key thing trivializing the categories; it’s just that any two elements of any equality type are actually equal. This property is called uniqueness of identity proofs (UIP).

    But do take a look at homotopy type theory (HoTT), where elements of equality types can be nontrivial, and correspond to morphisms and higher cells of \infty-groupoids. That includes nn-groupoids, sets, and propositions as degenerate cases. But no equality reflection.

    Some people around here are very hyped about HoTT. (And I’m probably the only one here who likes Nuprl…)

    There’s actually a way, two-level type theory, to combine reflective equality and HoTT equality into a single system. But they remain different notions of equality. There are restrictions to ensure that the UIP principle of reflective equality doesn’t spread to HoTT equality. To my intuition, HoTT is always essentially two-level; the difference is whether the equality with trivial proofs is axiomatized as intensional judgmental equality, or typal equality satisfying UIP. You need (at least) two notions of equality (not counting syntactic equality) in any case.

    The fact that it is a congruence, with the substitution of equals for equals rule shows that each of the operators in the Martin-Löf formalism is actually a functor. For instance, consider the following. […]

    Yeah, the HoTT people have worked out a lot of really nice higher categorical interpretations for constructions in type theory.

    If we eliminate symmetry,

    This turns out to be pretty tricky, axiomatically. There are a few approaches in the works, to get more general higher categories, but I don’t know much about them.

    Martin-Löf requires that each equality type I(A,a,b) have at most one member (this member being called “r”). This corresponds to a “coherence condition” that if f: a→b and g: a→b then f = g.

    OK, so you know about this. And yeah, it’s technically a coherence condition, but that’s kind of like calling “0 = 1” an equational constraint.

    All of this reveals another gap: the usual categorical identities are absent; e.g. f∘1 = f = 1∘f ∈ I(A,B), for f ∈ I(A,B).

    No, those equations are already provable. (For element equality, including universe elements.) And much much more.

    • CommentRowNumber24.
    • CommentAuthorGuest
    • CommentTimeFeb 27th 2021
    Wow. You are progressing fast, my padawan, Lydia! In a few paragraphs you went from Martin-Loef's 1979 and 1980 presentations to 2012 and beyond. The 2nd reply, clipped off, was the names he used in 1980.

    Yes, atmacen, by the way, ML explicitly stated that the equality relations were to be reflexive, symmetric and transitive in his 1979 and 1980 treatments.

    Items, directly relevant to this, that may be of interest are the following:

    Homotopy Type Theory (HoTT):
    The code: https://github.com/HoTT/HoTT/blob/master/README.md
    The book: https://github.com/HoTT/book

    Univalent Foundations (aka the post-2012 state of Martin-Loef): https://en.wikipedia.org/wiki/Univalent_foundations
    Yes, Martin-Loef was in on this.

    Homotopy Type Theory ... the Wikipedia link. There's also the link, in this forum, cited by atmacen
    https://en.wikipedia.org/wiki/Homotopy_type_theory

    Setoids - what you need to formalize and digitize higher-order analysis
    https://en.wikipedia.org/wiki/Setoid

    The idea of linking this directly to n-categories ... I don't yet see in any of this. This may represent a different way to approach the issue. But it almost looks like you can use ML as The Language for n-categories.

    -- Darth Ninja (aka MW Hopkins)
    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    added full publication data and DOI for:

    • Per Martin-Löf, An intuitionistic theory of types: predicative part, H. E. Rose, J. C. Shepherdson (eds.) Logic Colloquium ’73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 Pages 73-118, Elsevier 1975 ((doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

    diff, v26, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021
    • (edited May 12th 2021)

    added publication data and pdf-link for:

    • Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) (pdf)

    diff, v26, current

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    added this pointer:

    • Bengt Nordström, Kent Petersson, Jan M. Smith, Programming in Martin-Löf’s Type Theory, Oxford University Press 1990 (webpage, pdf)

    diff, v26, current

  2. replaced existing syntax section, which was incomplete (lacking structural rules, identity types and a natural numbers type) and somewhat poorly explained - especially when it came to the different notions of equality, with two different formal presentations of Martin-Löf type theory in the language of natural deduction.

    Anonymous

    diff, v35, current

  3. added section on propositional reflection in the second presentation of Martin-Löf dependent type theory

    Anonymous

    diff, v36, current

  4. readding section on propositions as types

    Anonymous

    diff, v36, current

  5. I believe \mapsto rather than \to was intended in these two locations (uniqueness rules for function types).

    SteveDunham

    diff, v39, current

  6. split contexts not needed in second presentation

    Anonymous

    diff, v40, current

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2023

    added pointer to:

    diff, v44, current

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeJan 31st 2023

    added pointer to:

    diff, v46, current

    • CommentRowNumber35.
    • CommentAuthorGuest
    • CommentTimeMar 16th 2023
    Why does Γ,x:A⊢b(x):B(x) appear in the premise for both dependent product types and dependent sum types? The premises for the latter should be weaker than the former, for otherwise we'd be able to inhabit a "for all" proposition from the premises of a "there exists" one. I think the correct premise for dependent sums should start with Γ,x:A⊢B(x):U where U is the universe containing A. This is how I've seen it in other references.

    --Simeon
    • CommentRowNumber36.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 16th 2023

    Re #35, you’re right. Removed that premise.

    The Γ,x:AB(x):U\Gamma,x:A \vdash B(x):U you mention is there as a premise for the formation rule.

    diff, v47, current

    • CommentRowNumber37.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 16th 2023

    So the computation rules there needed correcting too.

    diff, v47, current

    • CommentRowNumber38.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 16th 2023

    We have individual entries to link to, such as dependent sum type, but not tonight.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2023

    added (here) a table with a pretty-printed form of the structural rules together with their categorical semantics.

    I also tried to add references, but have trouble finding original ones:

    In Martin-Löf’s and in Hofmann’s original articles and also in Thompson’s textbook I see shadows of the rules scattered throughout the text, but not in a form that could be cited. (Or maybe I have missed it.)

    The textbook Jacobs (1998) mentions at least two structural rules briefly on p. 122 (and apologizes for doing so).

    The number and form of the rules which our entry used to be referring to all along is shown in Lecture 1 Rijke (2018) but without any referencing.

    My impression is that somewhere along the way from 1998 to 2018 the notion of “structural rules” became canonized. What’s a canonical reference?

    diff, v48, current

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2023
    • (edited Mar 26th 2023)

    I have touched the section “Judgements and Contexts” (here), trying to make it flow a little better. Also added a table showing the intended categorical semantics.

    Still, this section suffers from the common disease of our type theoretic entries: It’s content will be trivial to expert and mysterious to everybody else, since type-theoretical concepts are mostly not explained but just named.

    Eventually it would be nice to improve on this. On the other hand, the fact that nobody seems worried about this probably just means that humans, just as contemporary AI, learn not by logical rules but by osmosis of the mysterious.

    diff, v48, current

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2023
    • (edited Mar 26th 2023)

    While I am looking at this entry:

    The organization into “Presentation 1” and “Presentation 2” is not helpful but is irritating.

    The problem is that both sections are very large and yet almost complete duplicates of each other, leaving it to the reader to hunt for potential minute differences.

    (This duplication was introduced by “Anonymous” in rev 31 on 3rd Nov 2022 — a move which was not recognizable as such from the edit log in comment #28.)

    Instead of “Presentation 2” repeating all material verbatim except for silent exceptions, it should just point out explicitly which changes need to be made to Presentation 1!

    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2023

    added the proceedings/conference name and the link to the book collection to this item:

    following a suggestion in another thread (here)

    diff, v49, current