Re: Univalence from scratch

[Matt Oliveri <atm...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2187 bytes --]

The paper of Martin-Löf that you cite is about extensional type theory, not 
intensional type theory. In particular, in that paper, it's not the case 
that "Types are constructed together with their elements, and not by 
collecting some previously existing elements." as you write. You should 
probably cite something else. (Otherwise, looks good to me!)

I think the system you want was introduced in "An Intuitionistic Theory of 
Types: Predicative Part" (1975) 
(http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-Predicative-Part-1975.pdf). 
But it doesn't have a nice concise description of the formal system.

On Wednesday, March 7, 2018 at 4:10:54 PM UTC-5, Martín Hötzel Escardó 
wrote:
>
> I have often seen competent mathematicians and logicians, outside our 
> circle, making technically erroneous comments about the univalence axiom, 
> in conversations, in talks, and even in public material, in journals or the 
> web. 
>
> For some time I was a bit upset about this. But maybe this is our fault, 
> by often trying to explain univalence only imprecisely, mixing the 
> explanation of the models with the explanation of the underlying theory 
> (MLTT, identity types, universe), with none of the two explained 
> sufficiently precisely. 
>
> There are long, precise explanations such as the HoTT book, for example, 
> or, the formalizations in Coq, Agda and Lean.
>
> But perhaps we don't have publicly available material with a 
> self-contained, brief and complete formulation of univalence, so that 
> interested mathematicians and logicians can try to contemplate the axiom in 
> a fully defined form.
>
> Here is an attempt to rectify this:
>
>   https://arxiv.org/abs/1803.02294
>
> This also has an ancillary Agda file with univalence defined from scratch 
> (without the use of any library at all). Perhaps somebody should add a Coq 
> "version from scratch" of this. 
>
> There is also a web version of this (
> http://www.cs.bham.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html) to try 
> to make this as accessible as possible, with the text and the Agda code 
> together.
>
> M.
>
>

[-- Attachment #1.2: Type: text/html, Size: 3518 bytes --]