Added definition of propositional truncation as a sequential colimit and added the reference where the definition came from

Anonymouse

]]>added definition of bracket type using a type of all propositions.

]]>added pointer to:

- Nicolai Kraus,
*The General Universal Property of the Propositional Truncation*, in*TYPES 2014*Leibniz International Proceedings in Informatics (LIPIcs)**39**(2015) [arXiv:1411.2682, doi:10.4230/LIPIcs.TYPES.2014.111]

Have only scanned the first few pages, but: Is this not secretly rediscovering the notion of *anafunctor*?

added pointer to

- Univalent Foundations Project, §3.7
*Homotopy Type Theory – Univalent Foundations of Mathematics*(2013) [web, pdf]

and doi-link to:

- Steve Awodey, Andrej Bauer,
*Propositions as $[$Types$]$*, Journal of Logic and Computation,**14**(2004) 447-471 [doi:10.1093/logcom/14.4.447, pdf]

added section relating propositional truncations to localizations.

Anonymous

]]>fixed HTML entities to UTF-8 characters in Agda snippet

anqurvanillapy

]]>I added the recursion principle for $supp(A)$. I also added to the notations for the bracket type. We’re up to 6 now.

]]>Voevodsky defined it, as Guillaume said, “using impredicative quantification and resizing rules” (and also univalence). I believe his definition simply mimics the classical proof that a (1-)topos is a regular category — univalence plus a resizing rule is just the way that you get a subobject classifier in HoTT.

The definition as an HIT is what is due to Peter Lumsdaine.

]]>I have added to *bracket type* a brief section *Definition in homotopy type theory* with the definition of $supp(A)$.

Also added four references on this. I see in Mike’s lectures the construction is attributed to Lumsdaine. However in the recent post by Brunerie, it seems to be attributed to Voevodsky. I don’t know. The entry currently does not cite Lumsdaine yet, but probably it should.

]]>I am somewhat surprised that the idea of “bracket types” is not already in the original articles on propositions as types. I had thought that taking bracket types is implicitly understood all along.

]]>had the chance to add a bit more to bracket type: now there is an *Idea*-section a *Semantics*-section.

I have also added links to bracket type to relevant entries, in particular to types and logic - table.

Experts please check. I am pretty sure I know what I am talking about here, but I may not be using language in the standard way.

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

]]>