Univalence from scratch

[Martín Hötzel Escardó]

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.

[Jason Gross]

> Perhaps somebody should add a Coq "version from scratch" of this.

If you just want a straightforward transcription of the Agda code, I've made one here: https://gist.github.com/JasonGross/c6745e6d3ffbab3ee7034988c1b5b904

Feel free to adapt it as you desire, and use it with or without crediting me.
The only "design decisions" of note are:

1. Making sigma types a record with primitive projections and eta is needed to get Coq's "compute" to use projections in the normal form, rather than "match"

2. I used "Opaque J" so that running reduction wouldn't print "match" statements on the Id type.

3. I added a definition "isUnivalentAt" defined so that "isUnivalent := (X Y : U) -> isUnivalentAt X Y", because I wanted to only pass universes in the definition of isUnivalent, in a way that induced minimal clutter

4. I added some notations in "Module Short." to suppress printing of types, to match your normal form with types elided.

-Jason

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Matt Oliveri]

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.

[Andrej Bauer]

Martin-Löf's paper "25 years of constructive type theory" might be an
appropriate reference. It's an updated version of earlier work, and
somewhere near the beginning he says explicitly that terms are always
constructed with their types.

With kind regards,

Andrej

[Andrej Bauer]

> Martin-Löf's paper "25 years of constructive type theory"

Sorry, that should have been: Martin-Löf's contribution in the book

[N. Raghavendra]

At 2018-03-07T13:10:53-08:00, Martín Hötzel Escardó wrote:

> 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.

I have kept my attempt at a Coq version at

http://www.retrotexts.net/just-univalence/toc.html

However, I don't know how to define the univalence of a universe in Coq,
that is, I don't know what to write for foo and bar in

Definition univalence (U : foo) : bar := baz.

Remarks are welcome.

Raghu.

--
N. Raghavendra <ra...@hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Jason Gross]

Raghu, perhaps you want

  Set Universe Polymorphism.

  Definition univalence@{U U'} : Type@{U'} := forall X Y : Type@{U}, ...

or alternatively

  Universe U.

  Definition univalence := forall X Y : Type@{U}, ...
?

[Martin Escardo]

On 08/03/18 01:37, Jason Gross wrote:
> > Perhaps somebody should add a Coq "version from scratch" of this.
>
> If you just want a straightforward transcription of the Agda code, I've
> made one here:
> https://gist.github.com/JasonGross/c6745e6d3ffbab3ee7034988c1b5b904

Thanks, Jason. I am sending you a private message with further discussion.

Best,
Martin

> <mailto:HomotopyTypeThe...@googlegroups.com>.

[Martin Escardo]

Thanks Matt and Andrej.

Best,
Martin

[N. Raghavendra]

At 2018-03-09T07:02:08Z, Jason Gross wrote:

> Raghu, perhaps you want
>   Set Universe Polymorphism.
>   Definition univalence@{U U'} : Type@{U'} := forall X Y : Type@{U},
> ...
> or alternatively
>   Universe U.
>   Definition univalence := forall X Y : Type@{U}, ...
> ?

Thanks, I'll try that. At present, I am working with a specified
polymorphic universe 𝕌, and am using

Definition univalences : 𝕌 := ∏ (X Y : 𝕌) , ....

[Jeff Olson]

I posted a version written in Idris here (https://github.com/jdolson/univalence-from-scratch) if anyone is curious. -Jeff