Following discussion in some other threads, I thought one should make it explicit and so I created an entry

Currently this contains some (hopefully) evident remarks of what “dependent linear type theory” reasonably should be at least, namely a hyperdoctrine with values in linear type theories.

The entry keeps saying “should”. I’d ask readers to please either point to previous proposals for what “linear dependent type theory” is/should be, or criticise or else further expand/refine what hopefully are the obvious definitions.

This is hopefully uncontroversial and should be regarded an obvious triviality. But it seems it might be one of those hidden trivialities which deserve to be highlighted a bit more. I am getting the impression that there is a big story hiding here.

Thanks for whatever input you might have.

]]>I came to think that the term *geometric type theory* for the type theory internal toi sheaf toposes should exists. Thanks to Bas Spitter for pointing out that Steve Vickers had already had the same idea (now linked to at the above entry).

Also created *geometric homotopy type theory* in this vein, with some evident comments.

I finally created an entry *internal category in homotopy type theory*.

There is old discussion of this topic which I had once written at *category object in an (infinity,1)-category* in the sub-section *HoTT formulation*, but it’s probably good to give this a stand-alone entry, for ease of linking (such as from *equivalence of categories* now).

stub for homotopy type theory

]]>added to the references-section of the stub *type-theoretic model category* pointers to André Joyal’s slides on “typoses” (he is currently speaking about that again at CRM in Barcelona).

(maybe that entry should be renamed to “categorical semantics for homotopy type theory” or the like, but I won’t further play with it for the time being).

I am also pointing to Mike’s article and to his course notes. I will maybe ask André later, but I am a bit confused about (was already in Halifax) how he presents his typoses, without mentioning of at least very similar categorical semantics that has been discussed before. Maybe I am missing some sociological subtleties here.

]]>added to *Cachy real number* a pointer to

- Egbert Rijke, Bas Spitters,
*Cauchy reals in the univalent foundations*(talk notes, May 2013) (pdf)

Created *opetopic type theory* with a bit of explanation based on what I understood based on what Eric Finster explained and demonstrated to me today.

This is the most remarkable thing.

I have added pointers to his talk slides and to his online opetopic type system, but I am afraid unguided exposition to either does not reveal at all the utmost profoundness of what Eric made me see when he explained and demonstrated OTT to me on his notebook. I hope he finds time and a way to communicate this insight.

]]>started bracket type, just for completeness, but don’t really have time for it

]]>added pointer to

- Steve Awodey, Nicola Gambino, Kristina Sojakova,
*Homotopy-initial algebras in type theory*(arXiv:1504.05531)

to *initial algebra over an endofunctor*, *higher inductive type* and *W-type*

I have split off the section on *points-to-pieces transform* from *cohesive topos* and expanded slightly, pointing also to *comparison map between algebraic and topological K-theory*

created *Homotopy Type System* with an Idea-section

an entry for *mere proposition* had been missing. Created a minimum, just so as to satisfy links.

I apologize in advance if this isn’t the right venue for this question, but if someone could point me to the right venue, I’d appreciate it.

However, on the off chance this *is* the right venue, I’m trying to learn the basics of HoTT and I’m troubled by something I must not understand about the analogy between $A\to B$ in homotopy and $A\Rightarrow B$ in logic:

Suppose I know that propositions $A$ and $B$ are true, that is I have $a:A$ and $b: B$. I can construct (introduce?) $f:A\to B$ by $\lambda x.b$. Should I therefore conclude that $A\Rightarrow B$? It seems like I’ve just claimed “any two true propositions imply one another.”

Where am I going astray?

]]>Prompted by discussion in the thread on “internal sets” (badly named so) I have added to *h-set* a comment in *Properties - Relation to internal set*.

I see that on the open problems in Homotopy Type Theory page, the question “Can we verify computational algebraic topology using HoTT?” is listed, with a link to Kenzo. I did some digging, and a presentation by Heras et al. seems to suggest that the Basic Perturbation Lemma has been proved in Coq (without univalence, HITs or quotient types to get around using setoids, etc.) Given that the Basic Perturbation Lemma is somewhat central to Kenzo’s operation, what would we expect/hope to gain from formalizing it again in book HoTT?

Looking beyond the BPL, what other formalization efforts would help fulfill the stated goal?

]]>In the process of expaning on [[n-truncated object in an (infinity,1)-topos]] I added some remarks along these lines to the beginning of [[homotopy n-type]], thereby rewriting the first few sentences.

]]>Given any object $V$ in an elementary $\infty$-topos, then its automorphism group $\mathbf{Aut}(V)$ may be characterized as the pointed connected object which is the 1-image of the name of $V$ in the type universe.

Now if $V$ itself has group structure, hence if there is pointed connected $\ast \to \mathbf{B}V$, what is the elementary way to speak of its group $\mathbf{Aut}_{Grp}(V)$ of group automorphisms, hence of automorphisms of $\mathbf{B}V$ that preserve the basepoint?

And I’d need a canonical forgetful map

$\mathbf{Aut}_{Grp}(V) \longrightarrow \mathbf{Aut}(V) \,.$ ]]>added to [[group cohomology]]

in the section structured group cohomology some remarks about how to correctly define Lie group cohomology and topological group cohomology etc. and how not to

in the section Lie group cohiomology a derivation of how from the right oo-categorical definition one finds after some unwinding the correct definition as given in the article by Brylinski cited there.

it's late here and I am now in a bit of a hurry to call it quits, so the proof I give there may need a bit polishing. I'll take care of that later...

]]>I gave “adjoint cylinder” its own entry.

This is the term that Lawvere in *Cohesive Toposes and Cantor’s “lauter Einsen”* (see the entry for links) proposes for adjoint triples that induce idempotet (co-)monads, and which he proposes to be a formalization of Hegel’s “unity of opposites”.

In the entry I expand slightly on this. I hope the terminology does not come across as overblown. If it does, please give it a thought. I believe it is fun to see how this indeed formalizes quite well several of the examples from the informal literature.

I am not sure if “adjoint cylinder” is such a great term. I like “adjoint modality” better. Made that a redirect.

]]>Tomorrow (today, really) there takes place a little workshop in Paris

*Sur la notion d’identification en physique et en mathématiques*.

After talks by Mathieu Anel and Eric Finster on homotopy and homotopy type theory, David Corfield and myself will speak about cohesive homotopy theory and physics.

I will be using slides (pdf) based on the slides that I used at the QFT meeting in Trento a few weeks back.

]]>I wrote a little piece at *general covariance* on how to formalize the notion in homotopy type theory. Just for completeness, I also ended up writing a little blurb at the beginning about the genera idea of general covariance.

I have added pointer to Mike’s discussion of spectral sequences here at “homotopy spectral sequence” and in related entries.

But now looking at this I am unsure what the claim is: has this been formalized in HoTT?

(Clearly a question for Mike! :-)

]]>A thought: the way that homotopy invariants and coinvariants are built abstracly as described at *infinity-action* is just the internal version of the construction of $\infty$-colimits and $\infty$-limits in terms of the object classifier of $\infty Grpd$ here.

Namely the story at infinity-action is that given any type $V$ then the 1-image of its name in the universe is $\mathbf{B}\mathbf{Aut}(V) \to Type$. This we may think of as being a diagram of shape $\mathbf{B}\mathbf{Aut}(V)$ internal in the $\infty$-topos. And then the statement is that the homotopy coinvariants of this $\mathbf{Aut}(V)$-action, hence the $\infty$-colimit of this internal diagram, is the pullback of the universal object bundle over the object classifier $Type$ along this map, and the homotopy invariants, hence the $\infty$-limit of the internal diagram, is the sections (i.e. dependent product) of the resulting colimit.

Done in $\infty Grpd$ this is just a special case of the discussion here.

So I am wondering: the above has an evident generalization to a construction that seems to give internal $\infty$-(co-)limits over any internal $\infty$-groupoidal diagram. And then boosting the type universe to its canonical Rezk-complete category object, one may easily mimic internally also what is done for $\infty$-category-indexed (co-)limits here.

Has this way of approaching internal $\infty$-(co-)limits already been considered anywhere?

(Sorry, this is sort of obvious, now that I think about it. Probably it’s an old hat. What’s a reference?)

]]>Discussion with Mike reminded me that we were lacking an entry *reflective subuniverse*.

I started a template and cross-linked, but now I am out of battery and time before filling in any content. Will do that tomorrow.

]]>