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.
    • CommentAuthorUrs
    • CommentTimeApr 7th 2011
    • (edited Oct 30th 2012)
    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2011

    Have added to homotopy type theory a paragraph on machine implementation and some more links in the References-section. Also started a page Coq, but more than stubby for the moment.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeOct 31st 2011

    I linked the Coq wiki.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2011

    uploaded a pdf with the basic HoTT-Coq code documentation, linked to now from homotopy type theory.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2011
    • (edited Nov 10th 2011)

    Added to the References/Code section at homotopy type theory a pointer to the Proviola-HoTT archive which offers HTML-functionality that displays the proofs in the code (which otherwise is only visible when loading the code into Coq itself).

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeNov 25th 2011

    I have further brushed up and expanded the dictionary, now with more comments on identity types.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2011

    I edited the Idea section at homotopy type theory some.

    By the way, Urs, I’m really grateful for all the stuff you’ve been writing on the nLab about HoTT! I’ve just been too caught up with figuring stuff out to read it carefully. But I’m going to try to find some time to look it over and make tweaks.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2011

    Thanks!

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeDec 12th 2011

    I’ve edited homotopy type theory some more, clarifying the dictionary a bit and adding a section “Advantages” after a discussion on the HoTT mailing list.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 12th 2011

    discussion on the HoTT mailing list.

    Is this a public list? I once tried to find it, but all I ended up finding was a Coq mailing list and the HoTT Google-group. If you don’t mean one of these two, could you tell me if there is a way for me to subscribe to “the HoTT mailing list”?

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 12th 2011

    I mean the google group. You can configure google groups to act like mailing lists.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 12th 2011

    Ah, okay, thanks. Yes, I am subscribed to the HoTT google list by email, so I know that one. Thanks.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • (edited May 10th 2012)

    Mike,

    a question out of curiosity, concerning the triple of correspondences on slide 4, part I of your Swansea notes:

    evidently there is one item missing to complete the picture: what would be the text in red to go in item 1?

    What is the homotopy-version of “A programming language”?

    I did ask somebody else this question. He wasn’t entirely sure but did make an educated guess that sounded interesting. But I have entirely forgotten now what that answer was, unfortunately.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2012

    The reason it’s missing is that I don’t know the answer!

    • CommentRowNumber15.
    • CommentAuthorSridharRamesh
    • CommentTimeMay 10th 2012

    Another question: In the same set of slides, you say at one point “Diagonals in higher categories are not monic!”. How do I square this with my naive, 1-categorical style of thought “But, diagonals followed by projections are identity, and thus diagonals must surely be (split) monic…”?

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • (edited May 10th 2012)

    While many statements from ordinary category theory generalize essentially verbatim to (,1)(\infty,1)-category theory, the notions of monomorphisms and epimorphisms form the big exception. Instead of generalizing straightforwardly, these notions split up each into a tower of notions: a monomorphism f:ABf : A \to B is a (-1)-truncated object in the slice over BB. Similarly an \infty-truncated object in the slice is just any old morphism. So the nn-truncated objects in the slice are close to being monomorphisms (“nn steps close”!) but are not quite monomorphisms.

    What does generalize is the following characterization of monos: in ordinary category theory a morphism f:ABf : A \to B is a mono precisely if its diagonal AA× BAA \to A \times_B A is an isomorphism. Now, isomorphisms are the (-2)-truncated morphisms. So this says that a morphism is (-1)-truncated if its diagonal is (-2)-truncated.

    This does generalize to a recursive characterization: a morphisms is nn-truncated precisely if its diagonal is (n-1)-truncated.

    [edit: for the discussion of the recursion principle see here]

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • (edited May 10th 2012)

    Ah, I forgot state the punchline:

    so if XX is an nn-truncated object, then X*X \to * is nn-truncated, and so the diagonal XX×XX \to X \times X is (n-1)-truncated.

    So the diagonal on an object XX is a mono precisely if the object is 0-truncated (is an h-set)!

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2012

    Also to address Sridhar’s last question directly: in a higher category, a “split monic” (a morphism admitting a retraction) is not necessarily a monic!

    • CommentRowNumber20.
    • CommentAuthorSridharRamesh
    • CommentTimeMay 11th 2012
    • (edited May 11th 2012)

    Ah, I see now. Between sets, a functor admitting a retraction must be full and faithful, but between nontrivial groupoids, this needn’t be the case (e.g., the map from 1 into the delooping of Z). So in a 1-category, “split monics” are monics, but in a higher category, they needn’t be.

    • CommentRowNumber21.
    • CommentAuthorSridharRamesh
    • CommentTimeMay 11th 2012
    • (edited May 11th 2012)

    (Incidentally, there are separate articles fully faithful (infinity,1)-functor and full and faithful (infinity,1)-functor, both describing, I believe, the same concept…)

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2012

    Thanks for noticing that! Discuss here.

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeMay 13th 2012

    So how truncated is a split mono in an (,1)(\infty,1)-category, and why don’t we call that a mono instead?

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeMay 13th 2012

    In general, I don’t see any reason for it to be at all truncated, although I can’t think of a counterexample off the top of my head.

    Of course there’s a choice for what we want to call a “mono” in an (,1)(\infty,1)-category. (1)(-1)-truncated morphisms have many of the usual properties of monomorphisms, and are the natural way to interpret propositions as some types in HoTT, so that’s some justification for giving them the unadorned name.

    • CommentRowNumber25.
    • CommentAuthorTobyBartels
    • CommentTimeMay 13th 2012

    A split monomorphism is an (n,1)(n,1)-category will be (n2)(n-2)-truncated, so in an (,1)(\infty,1)-category, that tells us nothing, is that right?

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeMay 13th 2012

    @Toby: that seems right.

    • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeMay 13th 2012

    In particular, a split mono in a (0,1)(0,1)-category (a poset) is (2)(-2)-truncated (an iso). Good, that makes me feel happy about it.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeMay 14th 2012

    I’ve added a remark along these lines to split monomorphism.

    • CommentRowNumber29.
    • CommentAuthorTobyBartels
    • CommentTimeMay 14th 2012

    Cool. Can I proselytise that a (0,1)(0,1)-category is a poset while a proset is a strict (0,1)(0,1)-category?

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeMay 14th 2012

    Sure.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeOct 30th 2012

    added a pointer to the recent

    to the list of references at homotopy type theory.

    • CommentRowNumber32.
    • CommentAuthorTobias Fritz
    • CommentTimeFeb 5th 2013
    I fixed a broken link pointing to Mike's old webpage.
    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2014
    • (edited Jan 3rd 2014)

    Added to the list of References at homotopy type theory a pointer to the new

    • Vladimir Voevodsky, Experimental library of univalent formalization of mathematics (arXiv:1401.0053)

    Earlier I had added more pointers at univalence on univalence in the cubical set model by Coquand and Huber.

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2014
    • (edited Mar 27th 2014)

    Added to the references a pointer to Voevodsky’s latest talk (pdf)

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2014

    Of course I have added

    to a bunch of related entries (including homotopy type theory, cubical set, univalence, relation between category theory and type theory)

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2016

    have added pointer to Shulman 16

    • CommentRowNumber37.
    • CommentAuthorAnthony Bordg
    • CommentTimeDec 17th 2017
    I added Dan Grayson's preprint "An introduction to univalent foundations for mathematicians" in the References section.
    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeApr 3rd 2018

    Added pointer to Mike’s “Homotopy type theory: the logic of space”.

    diff, v98, current

    • CommentRowNumber39.
    • CommentAuthorErnesto
    • CommentTimeMay 8th 2018
    I don't know if this is the right place to ask questions I have about HoTT book. Any way, here I go:
    In chapter 9, Category theory, page 314, Lemma 9.2.9. states that composition of functors is associative. Why do we need the coherence of this lemma? I am not sure what is the meaning of 'coherence' here and why the pentagon of equalities that follows should commutes.
    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeMay 8th 2018

    Welcome Ernesto! Coherence here is meant in the same sense as coherence in a monoidal category or bicategory: associativity doesn’t hold on the nose, but coherence of the isomorphisms/paths witnessing associativity means that we don’t usually need to worry about applying them explicitly. MacLane’s coherence theorem for monoidal categories (there is a similar theorem for bicategories etc.) says that once that pentagon and triangle commute, then “all diagrams” of associativity and unit isomorphisms also commute. Thus, whenever we have two composites that differ from each other by some reassociations, we don’t need to worry about how we do the reassociation to get from one to the other; there is an essentially unique way to do it.

    In general, a good place to ask questions about the HoTT book is the hott-cafe mailing list.

    • CommentRowNumber41.
    • CommentAuthorErnesto
    • CommentTimeMay 9th 2018
    Thank you Mike, sorry to bother you in this forum. I'll keep asking question about the same subject in hott-cafe mailing list.
    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeMay 9th 2018

    I didn’t mean that the nForum was a bad place to ask questions; I’m sorry if it sounded that way. This particular thread is mainly for discussion about the nLab page homotopy type theory, but the nForum as a whole is for talking about all kinds of “Math, physics, and philosophy” and this sort of question is fine here. I just mentioned hott-cafe because it’s more focused on the particular subject and on exactly this sort of question, so you may find more people there than here who have helpful things to say.

    • CommentRowNumber43.
    • CommentAuthorErnesto
    • CommentTimeMay 10th 2018
    Thank you very much, I am very grateful for your answer.. I begun asking questions in hott cafe about composition of functors but I rephrased it here;

    I want to know if this is neccesary (coherence) because of the way functors and their composition were defined, or if there is a way to define functors and their composition in homotopy type theory in such a way that we do not have to worry about coherence. For instance, if functors were simple functions with an additional condition we have associativity automatically without going into coherence once we check that the composition satisfies the additiional condition, or not? ( Composition of functions is associative and therefore composition of linear functions is associative because composition of linear functions is a linear function).
    • CommentRowNumber44.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2018

    Composition of functions is associative and therefore composition of linear functions is associative because composition of linear functions is a linear function

    Right, but it’s not associative up to definitional equality, because the proof of linearity is carried along as part of the notion of “linear function”. Any two proofs of linearity are equal, because being linear is a proposition, but not necessarily definitionally equal. The situation is the same for functors: the function on objects and the function on morphisms have definitionally associative composition, but the proofs of functoriality don’t. The reason coherence doesn’t arise for linear functions is that vector spaces are sets (0-types), so coherence holds automatically: any diagram of equalities in a vector space commutes.

    • CommentRowNumber45.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 20th 2018

    Added the point that classically inconsistent axioms may be added to HoTT.

    diff, v100, current

  1. Fixed a tiny typo: ‘if -> If’. Caps count!

    anqurvanillapy

    diff, v102, current

    • CommentRowNumber47.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 29th 2018

    Hey anqurvanillapy – thanks for your attention to blemishes and for repairing them. Just a friendly note to say that small typo corrections really don’t need to be announced at the nForum. You can leave the description box blank when you make such corrections at the nLab.

    • CommentRowNumber48.
    • CommentAuthorColin Tan
    • CommentTimeNov 29th 2018

    What is Axiom R? The link to Shulman 15 doesn’t work. It seems to link to some subsection in cohesive homotopy type theory.

    • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2018

    Someone typed a slash instead of a #, I’ve fixed it.

  2. Adding wiwikwlhott

    Auke Booij

    diff, v104, current

    • CommentRowNumber51.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2019

    That last comment mystified me. It means to refer to What I Wish I Knew When Learning HoTT

    • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2019

    added pointer to

    diff, v107, current

    • CommentRowNumber53.
    • CommentAuthorUrs
    • CommentTimeAug 22nd 2019

    added pointer to

    diff, v110, current

    • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    added pointer to:

    • Dan Licata, Programming in Homotopy Type Theory, Talk at IFIP Wroking Group 2.8 meeting, November, 2012 (pdf, pdf)

    (as a public service, I optimized the pdf-file: this pdf is no less than 99% smaller but looks just the same)

    diff, v121, current

    • CommentRowNumber55.
    • CommentAuthorUrs
    • CommentTimeJun 9th 2022

    I have !include-ed the list homotopy theory in homotopy type theory – references into the References-subsection, which seems to be closer to what Anonynous has intended here

    diff, v125, current

  3. added various forums for homotopy type theory

    Anonymous

    diff, v126, current

  4. added additional sources/introductions to HoTT to the references section

    Anonymous

    diff, v126, current

  5. adding CMU blog on HoTT

    Anonymous

    diff, v126, current

    • CommentRowNumber59.
    • CommentAuthorUrs
    • CommentTimeJun 15th 2022

    Fixed your link to Bob Harper, by making it redirect to Robert Harper

    diff, v127, current

  6. added link to HoTTEST

    Anonymous

    diff, v128, current

    • CommentRowNumber61.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2022
    • (edited Jun 17th 2022)

    added pointer to:

    diff, v130, current

    • CommentRowNumber62.
    • CommentAuthorUrs
    • CommentTimeJun 24th 2022

    I have added publication data for:

    I came to this while updating the list of references on the universal Kan fibration. It’s curious that the above article was published in 2021 but does not cite standard textbook accounts of the universal Kan fibration from the years before. The first one is due to Lurie 09, Prop. 3.3.2.7; then there is Cisinski 2019, Sec. 5.2.

    diff, v133, current

  7. editing first paragraph to indicate that homotopy type theory is not just a Martin-Löf type theory.

    Anonymous

    diff, v134, current

  8. also added “path types” to the first sentence as they are different from identity types in cubical type theory

    Anonymous

    diff, v134, current

    • CommentRowNumber65.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2022
    • (edited Sep 4th 2022)

    I have added DOI-links and other niceties to a couple of bibitems.

    In particular, I added the proper publication data for

    which some previous author had tried but failed with.

    diff, v136, current

  9. added link to book HoTT

    Anonymous

    diff, v139, current

    • CommentRowNumber67.
    • CommentAuthorUrs
    • CommentTimeJan 2nd 2023

    added pointer to:

    diff, v140, current

    • CommentRowNumber68.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2023

    The Wikipedia page “Homotopy type theory” knows that

    Advocates claim that HoTT allows […] However, these claims aren’t universally accepted

    What’s good citable (at least linkable) examples of HoTT heretics?

    I am aware of a couple of rants by Buzzard (e.g. Where is the fashion? or Is HoTT the way?) but his complaint is focused on doing mathematics (as opposed to practical computer programming, and be it certification of practical programs) and his complaint is mainly sociological (choice of research priorities) rather than technical.

    So how about HoTT as a potential tool in actual computing theory: Are there any good heretic writings of computer scientists complaining about HoTT? Anyone arguing that higher homotopy data types are never going to solve any industry-relevant problems (contrary to hopes such as expressed e.g.by Ghani et al. here)?

    (I am not asking for discussion or debate, just for interesting links to contrarian arguments.)

    • CommentRowNumber69.
    • CommentAuthorGuest
    • CommentTimeJan 5th 2023

    There is essentially nobody in industry using functional programming languages, never mind dependently typed languages or HoTT.

    • CommentRowNumber70.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2023

    Maybe tangential to my question, but how about stuff like this (Hedera calls itself “enterprise-level”, if not “industry-level” – I may not know the difference, if any):


    Verification of (blockchain-like) hashgraph consensus algorithms:

    Background:

    • Pierre Tholoniat, Vincent Gramoli, Formal Verification of Blockchain Byzantine Fault Tolerance, in Handbook on Blockchain, Optimization and Its Applications 194 (2022) [arXiv:1909.07453, doi:10.1007/978-3-031-07535-3_12]

    • Leemon Baird, Mance Harmon, and Paul Madsen, Hedera: A Public Hashgraph Network & Governing Council, (last update 2020) [pdf]

    With Coq:

    With Agda:

    • Harold Carr, Christopher Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva, Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version [arXiv:2203.14711]

    • CommentRowNumber71.
    • CommentAuthorGuest
    • CommentTimeJan 6th 2023

    Apologies for distracting a little from your question. What I meant was that in practise only a trivial amount of companies are using even Haskell, say, and it is only a trivial part even of those companies’ codebases. There are certainly one or two things; if one searches, there is a claim that a few large companies do use a little Haskell, say. But I can assure you that the scale is unbelievably tiny. In the country I work in, I have never seen a job offer mention a dependently typed language, and never seen one require a functional programming language; very occasionally, the latter are mentioned as good to be familiar with.

    Of course functional programming ideas have had influence in other types of languages, they are not useless, but they are not used in industry directly and I doubt ever will be, because electronics and low-level programming are fundamentally non-functional. No dependently typed language can do I/O, and that makes them unusable in industry (proof verification is not a part of industry except in an unbelievably tiny percentage; zero as far as I know in the country in which I live for example).

    • CommentRowNumber72.
    • CommentAuthorGuest
    • CommentTimeJan 6th 2023

    Most approaches to homotopy type theory do not attempt to include a type of all propositions, the type theoretic equivalent of the set of truth values in set theory. This means that one is forced to include an entire universe in the dependent type theory in order to get a power set on a type for certain areas of mathematics, which is overkill for stuff like real analysis or complex analysis where one only needs a type of propositions rather than an entire universe. In practice, if one is doing something like real analysis, one really only needs a type of all propositions to construct the Dedekind real numbers, and afterwards one only really quantifies over the real numbers, tuples of real numbers, sequences of real numbers, and functions of real numbers, none of which requires an entire universe and the complex set of rules which come with having a universe in the type theory. Furthermore, the resulting “power set” constructed from universes would also only be locally small relative to the universe, so doesn’t exactly behave as a true power set in the type theory from the perspective of the categorical semantics.

    Certain branches of mathematics like set theory or algebra require quantification over certain structured types, such as sets or rings, which means that a universe is indeed required. But most homotopy type theory includes multiple universes, where one universe suffices. If there are multiple universes in the type theory, there is the issue in having to distinguish between, for example, different “locally small power sets” or “locally small Dedekind real numbers” for different universes, and the bureaucratic requirements to keep track of the different universes becomes a nightmare in practice. It becomes even worse in the HoTT book and in Agda, Lean, and Coq, where their infinite hierarchy of universes corresponds to having an infinite series of inaccessible cardinals in set theory, which is simply overkill for a foundations of mathematics.

    Personally, I believe that one should only include the bare minimum amount of type formers in the theory in order to do whatever mathematics you set out to do so. If one is doing elementary number theory, for example, including James constructions in the theory is not necessary at all. Indeed, while I view higher inductive types as quite necessary for mathematics in dependent type theory/homotopy type theory, as propositional truncations are necessary to define predicate logic in the theory and quotient sets are often used, a lot of mathematics could be done without resorting to universes at all, and much of the rest could be done using only one universe maximum.

    Different guest

    • CommentRowNumber73.
    • CommentAuthorUrs
    • CommentTimeJan 7th 2023
    • (edited Jan 7th 2023)

    Thanks for the chat!

    Maybe we are not quite communicating yet, as I am not sure how your comments really pertain to my original question #68 (clearly software verification is a thing?!) nor to my followup reply #70 refuting (I thought :-) the claim in #69.

    Incidentally, I found it fascinating to watch the talk by Leemon Baird that I linked to [YT]: a vision of a future of type-theory-savvy crypto-finance CEOs.

    \,

    But allow me to use the occasion to pick up the claim in #71 — that industry is all about low-level electronic hardware-aware programming — and try something on you:

    Let’s take this seriously and ask what programming language infrastructure really reflects the notion of computation at the physical hardware (electronics) level (or as close as any language can get to it).

    This question is currently being re-asked in quantum computation, a perspective which may help take the necessary step back to look at this ancient question afresh.

    I think that real close to the physical hardware level, computation is not described by imperative programming languages either – it’s not described by any “language” as such:

    Real close to the realistic physical hardware level, computation is described by the circuit model.

    In classical computation this may have been forgotten, but in quantum computation, where all these fundamental questions are resurfacing now, it is clear as day.

    And if we are really to talk physics and foundations here, then I go one step further and say that real close to the realistic physical hardware level, computation is given by the reversible circuit model.

    If we accept that (? :-) then we need to ask: What is the circuit model of computation, fundamentally?

    So let’s see: in the circuit model we have

    1. a generating set of labels of reversible operations (gate names)

    2. for each such a corresponding operation on a state space.

    3. A program is a path of (labels of) gates (namely in the HIT generated by the gate labels)

    4. its execution on any input data is the corresponding lifting of that path through the corresponding fibration.

    (For fun and exposition I recently produced some schematic illustration of what I am saying here: pp. 60 here and also pp. 60 here (to be viewed on full screen). Some related references are compiled in the entry Computation – References – As path lifting.)

    Therefore – my argument now goes – if we are really serious about understanding programming at the physical hardware level, and formal verification of that – then what we need is a high-level language in which path lifting is a native operation.

    This leads us full circle back to… HoTT. From a completely different direction than usually (or ever before) advertised.

  10. Let’s take this seriously and ask what programming language infrastructure really reflects the notion of computation at the physical hardware (electronics) level (or as close as any language can get to it).

    I think for that one has hardware description languages like Verilog, at least in the classical case.

    • CommentRowNumber75.
    • CommentAuthorGuest
    • CommentTimeJan 8th 2023

    [The same person as in #69 and #71]

    I am not sure how your comments really pertain to my original question #68 (clearly software verification is a thing?!) nor to my followup reply #70 refuting (I thought :-) the claim in #69.

    In #68, ’practical computer programming’ and ’industry-relevant problems’ were mentioned. What I was asserting was that even the most well-known functional programming languages have the most miniscule presence in the actual programming industry. Proof verification is an extremely tiny proportion of that industry as a whole. These assertions are based on first-hand knowledge of the industry; it cannot be refuted by listing a handful of examples of use. Amongst the millions of lines of code written every day, perhaps a few thousand are written in functional programming languages in industry, perhaps a few hundred in dependently typed languages, and perhaps a dozen in HoTT by some lost soul. These are trivial amounts. In #71 I gave a different metric (job advertisements), quite easily verified, indicating how minimal their use is.

    My intention was to contribute your sharpening your main question: one can certainly ask whether computer scientists think HoTT helps solve their problems, but one should divorce this matter from the programming industry as a whole.

    that industry is all about low-level electronic hardware-aware programming

    This was not what I wrote. The overwhelming majority of the industry uses high-level languages. Even embedded software almost always does not go lower than C.

    But my point was that computers are based on 0s and 1s. It is essential to turn one into the other, i.e. have mutability. In high-level programming languages, it is all well and good to abstract away the details and write ’immutably’, etc, but cannot get the smallest thing done on any actual computer if one tried to do that at a low-level. Therefore it is necessary to have languages like C which reflect that reality more closely, which higher-level programming languages build further upon. Haskell for example is totally reliant on C in its implementation, as are essentially all modern languages (older languages such as Fortran and Forth are not, but are as equally fundamental mutable).

    It may be difficult to appreciate if one doesn’t have experience with low-level programming, but mutability is absolutely unavoidable with today’s machines. That is true whether one programs really close to the electronics, say with an FPGA, in assembly, in C, or whatever. To able to do anything, one has to able to be handle interupts, i.e. signals, i.e. changes from 0s to 1s. Memory is about changes from 0s to 1s. If every single process was left sitting in memory after it was run, the computer would be useless in a few hours of use at once.

    Of course one can dream as much as one likes about other possible ways of doing things, but binary numbers are the simplest possible ways to express change, and Ockham’s Razor almost always applies in the end. Only if something came along which rendered current computers as useful in practise as the abacus in comparison would there likely be a fundamental change. Society as we know it might collapse before that. Who knows.

    • CommentRowNumber76.
    • CommentAuthorRodMcGuire
    • CommentTimeJan 8th 2023

    Urs
    Since you found out you have the power to delete comments from the nForum, have you been posting comments to this thread and then deleting them?

    Something is making the nForum forget how much I’ve read in threads. Just now this thread appeared at the top of the All Discussions page (indicating it had new content) but when I open It I am taken to a Jun 15th 2022 posting and I have to scroll to the bottom. This has happened several times in this thread and as I recall some other ones you are posting in. But not in any other threads.

    • CommentRowNumber77.
    • CommentAuthorUrs
    • CommentTimeJan 8th 2023
    • (edited Jan 8th 2023)

    Am coming back online only now after a long flight.

    have you been posting comments to this thread and then deleting them?

    I did delete & repost #73 right after posting the first version, because the first version ended up appearing without my signature.

    Afterwards i was trying to see if the technical team can help us fixing this issue that the nForum logs users out who spent too long editing a comment.

    While I notice every now and then that some threads don’t take me to their latest messages, I had not idea what is causing this. Maybe if we can isolate a minimal test thread showcasing the issue, then we could tell the technical team about it.

    I may try to look into this later, currently it’s mighty busy here…

    • CommentRowNumber78.
    • CommentAuthorGuest
    • CommentTimeJan 8th 2023

    Progress in theoretical quantum computer science might be good but how useful would it be in industry if it turns out that actual quantum computers are limited by decoherence effects and interactions with the environment, or limited by the exponentially large cost to construct a quantum computer?

    • CommentRowNumber79.
    • CommentAuthorUrs
    • CommentTimeApr 12th 2023

    added pointer to:

    • David Jaz Myers, How do you identify one thing with another? – an intro to Homotopy Type Theory, talk in Prof. Sadok Kallel’s seminar at American University of Sharjah (10 Apr 2023) [slides:pdf]

    diff, v145, current

    • CommentRowNumber80.
    • CommentAuthorUrs
    • CommentTimeMay 17th 2023

    added more of the original/precursor articles (here)

    diff, v147, current

    • CommentRowNumber81.
    • CommentAuthorUrs
    • CommentTimeSep 5th 2023
    • (edited Sep 5th 2023)

    This summer at CQTS, David Myers and Mitchell Riley have run an introductory course on HoTT via cubical Agda. While their lecture notes (all commented Agda code) are being finalized for publication they are already available in some form at: github.com/CQTS/summer23-homework/tree/master/homework.

    • CommentRowNumber82.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2023
    • (edited Nov 6th 2023)

    below Hofman & Streicher 1998 I added pointer to:

    • Ethan Lewis, Max Bohnet, The groupoid model of type theory, seminar notes (2017) [pdf]

    diff, v148, current

    • CommentRowNumber83.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2023

    and similarly to:

    diff, v148, current

    • CommentRowNumber84.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2023

    added pointer to:

    diff, v148, current