Not signed in (Sign In)

Start a new discussion

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 beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology 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 foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus graph graphs gravity grothendieck group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration-theory internal-categories k-theory kan lie lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology nonassociative noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar 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 string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeOct 26th 2018

    Created page with some basic definitions.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 26th 2018

    Holy cow, Mike!! I quickly looked at all your recent pages – thanks so much!!

    I’ll probably be needing to take a harder look at the Plan and see how much I “get”. I will resist the temptation to say more now, before having that look.

    • CommentRowNumber3.
    • CommentAuthorKarol Szumiło
    • CommentTimeOct 26th 2018

    Here is a very basic question: application has the form App x:A.B(M,N)App^{x:A.B}(M,N). I’m guessing that AA and BB are supposed to be the types of MM and NN. But why do we need to mention the variable xx in such term?

    • CommentRowNumber4.
    • CommentAuthormaxsnew
    • CommentTimeOct 26th 2018

    The type annotation x:A.Bx:A.B here is to note that the type of MM is Π x:AB\Pi_{x:A} B (in a well typed term at least), so the xx is needed because it is bound in BB. For instance MM could be λx:A.refl(x)\lambda x:A. refl(x) which has type Π x:Ax=x\Pi_{x:A} x = x

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeOct 26th 2018

    Right. Although actually MM would have to be λ(x:A.x=x).refl(x)\lambda(x:A.x=x) .refl(x), since as was pointed out on the other thread the codomains of abstractions also have to be annotated in general.

    • CommentRowNumber6.
    • CommentAuthorJohn Dougherty
    • CommentTimeOct 26th 2018

    Added a first attempt at alpha-equivalence and capture-avoiding substitution.

    diff, v3, current

    • CommentRowNumber7.
    • CommentAuthorKarol Szumiło
    • CommentTimeOct 27th 2018

    The type annotation x:A.Bx:A.B here is to note that the type of MM is Π x:AB\Pi_{x:A} B (in a well typed term at least), so the xx is needed because it is bound in BB.

    Oh, of course. That makes sense. When we mod out α\alpha-equivalence, will there be a notational distinction between a raw term and its equivalence class?

    • CommentRowNumber8.
    • CommentAuthoratmacen
    • CommentTimeOct 27th 2018

    No substitutions for constants. (I think.) Only for variables.

    diff, v4, current

    • CommentRowNumber9.
    • CommentAuthoratmacen
    • CommentTimeOct 27th 2018
    I see three problems with substitutions and alpha equivalence, which I might get around to fixing:

    You need multiple simultaneous substitutions. With variable names, I don't think this can always be mimicked one at a time, even throwing in alpha conversions.

    The alpha equivalence as currently defined is not a congruence. You can only rename a variable bound in the outermost term constructor.

    Most insidiously, the renaming currently used in alpha equivalence doesn't avoid capture. For example (eliding annotations), you could convert (λx.λy.Ap(x,y)) to (λx.λx.Ap(x,x)). You can only rename to a variable that isn't already free. The other possible bad renaming, to (λy.λy.Ap(y,y)), was already avoided because substitution is partial.
    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2018

    Thanks for working on this, everyone! I wonder whether we could do this at a higher level of abstraction, so that we wouldn’t need to add new clauses to the definition of substitution and α\alpha-equivalence every time we add new type formers. For instance, I was just looking at Bob Harper’s Practical foundations of programming languages, and he defines a general notion of “abstract binding tree” that seems to support substitution and α\alpha-equivalence for “any term system one could give”, although I don’t completely understand it.

    • CommentRowNumber11.
    • CommentAuthoratmacen
    • CommentTimeOct 27th 2018

    which I might get around to fixing

    Oh, maybe I shouldn’t. I don’t want to steal John Dougherty’s job.

    • CommentRowNumber12.
    • CommentAuthorJohn Dougherty
    • CommentTimeOct 27th 2018

    Please do fix them, if you like! I put my name next to this task on the Initiality Project page because I was volunteering; I didn’t mean to claim this page as mine or anything.

    Also, thanks for pointing out these issues. I think I might have a look at Harper’s discussion of abstract binding trees before trying to fix these problems (if you don’t fix them first). It’s true that it would be a pain to redefine all this with each new type former.

    • CommentRowNumber13.
    • CommentAuthorMichael_Bachtold
    • CommentTimeOct 28th 2018
    • (edited Oct 28th 2018)

    An elementary question: are Π\Pi, λ\lambda, App\mathrm{App} and the colon :: considered to be constants? (I’m assuming parenthesis and the other punctuation marks like , and . are not constants of the raw syntax). If none of the above are constant, then what would be an example of a constant in the type theory under consideration?

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeOct 28th 2018

    No, those are not constants. Π\Pi, λ\lambda, and AppApp are “constructors” of the raw syntax, i.e. labels that can be put on a node of an abstract syntax tree. The colon is like the other punctuation marks, part of how we notate abstract syntax trees and judgments in concrete syntax but has no independent meaning. In the language of n-theories, Π,λ,App\Pi, \lambda, App are part of the “doctrine”, while the constants are what specify a particular “theory” in that doctrine. For instance, if we wanted to study categories inside dependent type theory, we might consider a theory (or “signature”) containing a type constant OO, another type constant x:O,y:OA(x,y)typex:O, y:O \vdash A(x,y) \, type, a composition constant x:O,y:O,z:O,f:A(x,y),g:A(y,z)comp(x,y,z,f,g):A(x,z)x:O,y:O,z:O,f:A(x,y),g:A(y,z) \vdash comp(x,y,z,f,g) : A(x,z), and so on. We can also use constants to implement axioms, such as function extensionality or univalence.

  1. I see, thanks for clarifying.

    • CommentRowNumber16.
    • CommentAuthoratmacen
    • CommentTimeOct 28th 2018
    I've thought about Harper's abstract binding trees before. I could try to answer questions.
    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeOct 28th 2018

    We should include some examples somewhere. I wonder whether they should be interspersed, or collected all in one place?

    • CommentRowNumber18.
    • CommentAuthorraghu
    • CommentTimeOct 30th 2018

    I wonder if it is better to say something else, such as “preterm”, instead of “raw term”. It would enable us to avoid the non-subsective adjective “raw” in the phrase “raw term”: a raw term is not a term. I like the remark of Gerard Debreu [Theory of value, 1959, chapter 1, page 27, note 1], explaining why he prefers to say “correspondence” instead of “multi-valued function”:

    A correspondence (N. Bourbaki’s term) has often been called a multi-valued function. Locutions such as these, where the object named by a noun and an adjective is not in the class of objects named by the noun alone, have been avoided here.

    The usage “preterm” has precedents, as in Sørensen and Urzyczyn [Lectures on the Curry-Howard isomorphism, Section 1.2].

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2018

    I think one can argue that a raw term is a term. It’s just not necessarily a well-typed term.

    • CommentRowNumber20.
    • CommentAuthorraghu
    • CommentTimeOct 30th 2018

    a raw term is a term.

    Can you please explain? According to the last paragraph of the page, a term is an α\alpha-equivalence class of raw terms. I don’t understand how a raw term is an α\alpha-equivalence class of raw terms.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2018

    Hmm, I didn’t write that paragraph. I’m not sure I would agree with it. To me “raw” indicates possibly-ill-typed-ness, not the presence of variable names, and I would rather not introduce a clumsy word like “preterm” merely to be pedantic about α\alpha-equivalence.

    But in any case I would rather not argue about terminology at this point in the project, when there are so many better arguments to have. (-: Are you actually confused by the mathematics, or just not liking the terminology?

    • CommentRowNumber22.
    • CommentAuthorraghu
    • CommentTimeOct 30th 2018
    • (edited Oct 30th 2018)

    Hmm, I didn’t write that paragraph. I’m not sure I would agree with it. To me “raw” indicates possibly-ill-typed-ness, not the presence of variable names

    I will wait for someone to rewrite the page according to what you are saying.

    I would rather not introduce a clumsy word like “preterm” merely to be pedantic about α\alpha-equivalence.

    But in any case I would rather not argue about terminology at this point in the project, when there are so many better arguments to have. (-: Are you actually confused by the mathematics, or just not liking the terminology?

    I don’t mean to be contrary; I am only trying to say that the overview of the project seems to start from the basics of type theory, and I think there was some mention of explaining the subject to mathematicians who don’t know anything about it. If one is explaining the basics of something to a novice, perhaps it is better to be precise even if it is pedantic. I understand it is a matter of personal taste, but I find the Bourbaki style of exposition very satisfying; I wonder if it is considered pedantic.

    In any case, I feel uneasy when people ask me to identify things, especially at an early stage of learning a subject. A germ is a function. An element of L 2(R)L^2(\R) is a function. Sure, but it takes me a while to get used to such identifications.

    In the present context, I am afraid that we will slip into identifying a raw term with an α\alpha-equivalence class of raw terms as in several books that I have tried to read, and hand-wave verifications of invariance of various operations under α\alpha-equivalence.

    As you can see, my confusion is due to a mixture of ignorance and a difficulty with the accounts of type theory that I have tried to learn from.

    Reading what I have written, I feel that I am not very clear. Anyway, it will do for now.

    Thank you for doing so much work for this project, and for making it open to everyone.

    • CommentRowNumber23.
    • CommentAuthoratmacen
    • CommentTimeOct 30th 2018

    It looks like there’s just been a misunderstanding about what’s “raw” about “raw terms”. There are three types involved:

    • What John called RawTmRawTm, which have bound variables names
    • What John called TmTm, the quotient, which prevents you from looking at bound variable names
    • Those TmTm that are valid in some sense defined by the judgments

    I would also say that raw terms are terms—the “raw” is just for emphasis—but I usually use de Bruijn indexes, so I don’t usually need to worry about whatevers that remember variable names.

    Proposal: “nominal terms”, “terms”, and “valid terms”

    Speaking of arguing about terminology, I’m actually not so happy about calling that presheaf TmTm. Those guys generally aren’t syntax. Is there a problem with ElEl?

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2018

    I don’t think we need a special name for α\alpha-equivalence classes of terms. We can just say that we consider terms up to α\alpha-equivalence. Just like we don’t have a special word for “set up to isomorphism” when regarding sets “structurally” as objects of the category SetSet.

    And I think TmTm and TyTy are pretty standard for the presheaves in a CwF. They’re “semantic terms”. (-:

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2018

    Separate raw terms and raw types.

    diff, v6, current

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2018

    Correct definition of α\alpha-equivalence: the variable xx in App (x:A).B(M,P)App^{(x:A).B}(M,P) is bound in BB, not in MM and PP; and the new bound variable must not already occur freely in its scope-to-be.

    diff, v6, current

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2018

    Correct definition of capture-avoiding substitution: when substituting for a bound variable, we still have to carry out the substitution in the parts of the term that the binder doesn’t scope over; and when substituting into AppApp we do have to do it in all the subterms (not sure why that was treated differently).

    diff, v6, current

    • CommentRowNumber28.
    • CommentAuthoratmacen
    • CommentTimeOct 30th 2018

    Just like we don’t have a special word for “set up to isomorphism” when regarding sets “structurally” as objects of the category SetSet.

    I didn’t realize that was analogous, since a “higher quotient” is normally not available, to formalize working up to isomorphism. And when it is, I didn’t think SetSet was defined as a higher quotient.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2018

    The point is that we do just fine in practice without a higher quotient, and we so can similarly do without “lower quotients”.

    When higher quotients are available, as in HoTT, the category SetSet whose objects are h-sets doesn’t usually need to be quotiented (i.e. Rezk-completed) because univalence makes it already Rezk-complete. But if we defined it based on some stricter notion of set, for instance ZF-like sets built inside HoTT, then we would need to Rezk-complete it to obtain something that behaves like the usual category of sets.

    • CommentRowNumber30.
    • CommentAuthoratmacen
    • CommentTimeOct 31st 2018
    • (edited Oct 31st 2018)

    Argh! The example substitution was all wrong. We can’t everybody just use de Bruijn indices????

    diff, v7, current

    • CommentRowNumber31.
    • CommentAuthoratmacen
    • CommentTimeOct 31st 2018
    So are we switching to fresh-renaming-style nominal terms? (Like with Harper's ABTs?) Either way, it remains to make alpha equivalence a congruence.
    • CommentRowNumber32.
    • CommentAuthormaxsnew
    • CommentTimeOct 31st 2018

    I think we should get rid of the 3 cases with side condition y=xy = x, and just make the substitution operation undefined in those cases. Once we move to α\alpha-equivalence classes, we can always assume that yxy \neq x since it can be renamed to something different from xx. As it stands we have to prove that these 2 cases do the same thing on α\alpha-equivalent terms to show we respect the quotient, so the extra cases are just unnecessary work. You can always prove after the fact that those cases are correct and well-defined for α\alpha-equivalence classes of raw terms. This is the usual way of doing things, it’s called the “Barendregt convention”: any bound variable is always different from any free variable. If that sounds reasonable to others I’ll delete the extra cases.

    Then I would separately define the notion of renaming a single variable, which is used in the definition of α\alpha equivalence currently, to avoid intertangling the definition of α\alpha equivalence with our general substitution function.

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2018

    Re #32 that sounds reasonable to me. I don’t understand the jargon in #31, can you explain?

    • CommentRowNumber34.
    • CommentAuthoratmacen
    • CommentTimeOct 31st 2018

    Full side condition on ww in the substitution example.

    diff, v8, current

    • CommentRowNumber35.
    • CommentAuthoratmacen
    • CommentTimeOct 31st 2018
    • (edited Oct 31st 2018)

    Re #33: We are currently defining “FV” sets. This is leaves-to-root propagation of variable information, analogous to Andromeda’s context joining. The approach usually favored for formalization of nominal expressions mostly/entirely avoids “FV” and keeps track of reserved variables on the way to the leaves, analogous to the usual context propagation. Variables not currently reserved can be safely considered fresh for the current subexpression, so you don’t need “FV” in side conditions. (This requires knowing the FV of the expression at the outset, to reserve them, but you usually start from closed expressions. You know. Same argument as for root-to-leaves context propagation.) Once you have a working notion of freshness, you can rename bound variables to fresh variables (edit: and then reserve them) as you enter binders. This is what I meant by “fresh-renaming-style”. All of this root-to-leaves stuff is used by Harper’s ABTs (and multiple other developments).

    As for alpha equivalence not being a congruence, that was just a reminder of the same bug report from #9.

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2018

    Okay, I think I sort of see. I don’t really have an opinion, if that way is considered better then I’m fine with it.

    #9 also mentioned simultaneous substitutions; do we need those defined separately? I’m thinking right now that I want to collapse the “weakening/exchange/contraction” and “substitution” lemmas at Initiality Project - Substitution into one lemma about simultaneous substitution (i.e. along a “context morphism”), to avoid doing the same work twice.

    • CommentRowNumber37.
    • CommentAuthormaxsnew
    • CommentTimeOct 31st 2018

    Define re-naming, redefine alpha-equivalence and remove redundant cases of substitution.

    diff, v9, current

    • CommentRowNumber38.
    • CommentAuthoratmacen
    • CommentTimeOct 31st 2018

    I’m worried about the “x=yx = y or x=zx = z” cases in the new definition of renaming. In case x=zx = z and xyx \neq y, it doesn’t seem right to say the body doesn’t need to be renamed. It should give up. I think the old definition of renaming as a special case of partial substitution did this right, and I don’t see why we need renaming to be separate.

    Thanks for finally (mostly?) fixing alpha equivalence, Max.

    • CommentRowNumber39.
    • CommentAuthoratmacen
    • CommentTimeOct 31st 2018

    Fixes (I think) for alpha equivalence.

    diff, v10, current

    • CommentRowNumber40.
    • CommentAuthormaxsnew
    • CommentTimeOct 31st 2018

    Oof yeah not sure what I was thinking with that side condition.

    • CommentRowNumber41.
    • CommentAuthoratmacen
    • CommentTimeOct 31st 2018

    Add alpha equivalence case for constants.

    diff, v10, current

    • CommentRowNumber42.
    • CommentAuthormaxsnew
    • CommentTimeNov 1st 2018

    Correct definition of alpha-equivalence, I think :).

    We define substitution as a partial function, then in the definition of substitution, we make sure that “fresh” variables are different from all free and bound variables in the term, so that it is clear that our use of substitution is well defined.

    diff, v11, current

    • CommentRowNumber43.
    • CommentAuthoratmacen
    • CommentTimeNov 4th 2018
    • (edited Nov 4th 2018)

    For substitution, “yFV(N)y \notin FV(N)” —> “xFV(N)x \notin FV(N)”. xx is the bound variable, that could potentially capture.

    diff, v12, current

    • CommentRowNumber44.
    • CommentAuthorColin Tan
    • CommentTime6 days ago

    Tried to rewrite the definition of raw terms and raw types so that the elements of RawTmRawTm and RawTyRawTy are well-founded rooted trees themselves and not a linear representation C(M 1,...,M n)C(M_1,..., M_n) that refers to the actual tree.

    diff, v13, current

    • CommentRowNumber45.
    • CommentAuthorColin Tan
    • CommentTime6 days ago
    I am trying to understand the abstract syntax representation of raw terms and raw types. It is written "for instance, C(D(x), y) represents a tree with four nodes: a root with two children, one of which itself has two children."

    Let's start from D(x). Is D(x) the tree:
    D -> x?
    So that C(D(x), y) is the tree
    y <- C -> D -> x?
    If so, then shouldn't the node D have only one child?

    Am I right to say that "C(D(x), y) represents a tree with four nodes, whose root has two children, each of which is the root of the tree representing D(x) and y respectively, so that the former child has *exactly one* child?"
    • CommentRowNumber46.
    • CommentAuthorGuest
    • CommentTime6 days ago
    Is every variable secretly just a 0-ary term constant?

    Suppose for the moment that our variables are x_1, x_2, ... Assuming we are only doing Pi-types, could we then regard TyCst = {Pi} and TmCst = {lambda, App, x_1, x_2, ...} so that a more formal definition of raw terms and raw types as rooted trees labelled by constants would go like this:

    For each i, the tree with a single node labelled by x_i is a raw term, denoted also by x_i;
    Given raw terms A and B and i = 1,2,....., the tree whose root (labeled by Pi) that has three children, which are roots of x_i, A and B, is a raw type, denoted by ;
    Given raw terms A, B, M and i = 1,2,....., the tree whose root (labelled by lambda) that has four children, which are roots of x_i, A, B and M, is a raw term, denoted by lambda(x_i:A.B).M;
    Given raw terms A, B, M, N and i = 1,2,....., the tree whose root (labelled by App) that has five children, which are roots of x_i, A, B, M and N, is a raw term, denoted by App^{x:A.B}(M, N);

    Is seems to me that in these abstract syntax trees, the children of a given node have to be (linearly) ordered.
    • CommentRowNumber47.
    • CommentAuthoratmacen
    • CommentTime5 days ago

    Is every variable secretly just a 0-ary term constant?

    No, and in fact, Π\Pi, λ\lambda, and AppApp are not constants either. A raw term node is either a variable, an instantiated term constant, or an instantiated primitive term operator. A raw type node is either an instantiated type constant or an instantiated primitive type operator.

    The definition currently “hard-codes” the primitive operators. This may change in the future. The definition is parameterized by the sets of variables, term constants, and type constants.

    One reason why it’s not a good idea to treat variables as constants is because substitution handles variables and constants differently. In general, variables and constants are understood differently.

    so that a more formal definition of raw terms and raw types as rooted trees labelled by constants would go like this…

    It’s also not a good idea to treat the binding sites as subtrees, since they’re never handled that way.

    Is seems to me that in these abstract syntax trees, the children of a given node have to be (linearly) ordered.

    Since we’re adding operators as we go, there’s technically nothing preventing us from adding an operator so that the node’s subtrees are not in any particular order. But I don’t expect that to happen.

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTime5 days ago

    shouldn’t the node D have only one child?

    Yes, that must be a typo; I’ve fixed it.

    I don’t see what change you made in #44 though?

    • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTime4 days ago

    A new proposal: ABTs with strong scoping and local Barendregt convention

    diff, v15, current

    • CommentRowNumber50.
    • CommentAuthorMike Shulman
    • CommentTime4 days ago

    Unsurprisingly, I got the variable numbers in the de Bruijn example wrong…

    diff, v15, current

    • CommentRowNumber51.
    • CommentAuthordlicata335
    • CommentTime3 days ago
    • (edited 3 days ago)

    In the definition of X VX^V, should the later freshenings be with respect to the previous x ix_i (what’s written now) or the freshened versions of the previous x ix_i? (e.g. x 2 Vfr(V,x 1)x_2^{V \cup {fr(V,x_1)}} )?

    • CommentRowNumber52.
    • CommentAuthoratmacen
    • CommentTime3 days ago
    • (edited 3 days ago)

    Dan’s alternative sounds right to me, unless the English description is confusing me.

    () [V](\cdot)^{[V]} \coloneqq \cdot
    (x::X) [V]letxx [V]inx::X [V{x}](x\,::\,X)^{[V]} \coloneqq let x' \coloneqq x^{[V]} in x'\,::\,X^{[V \cup \{x'\}]}

    • CommentRowNumber53.
    • CommentAuthoratmacen
    • CommentTime3 days ago

    I’m guessing the scoping relation of an operator should be decidable.

    diff, v17, current

    • CommentRowNumber54.
    • CommentAuthoratmacen
    • CommentTime3 days ago
    • (edited 3 days ago)

    Changed the metavariable names in the operator case of the definition of RawRaw to match the definition of generalized arity. (And thus fixed a mismatch where it was already using that naming.)

    diff, v18, current

    • CommentRowNumber55.
    • CommentAuthorMike Shulman
    • CommentTime2 days ago

    Thanks for catching those typos.

    • CommentRowNumber56.
    • CommentAuthoratmacen
    • CommentTime2 days ago
    OK, it looks right to me. Sooner or later we’re probably going to need to prove a bunch of equations about renaming and substitution.
Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)