Univalence from scratch

Univalence from scratch

[Martín Hötzel Escardó]

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

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: 1582 bytes --]

Re: [HoTT] Univalence from scratch

[Jason Gross]

[-- Attachment #1: Type: text/plain, Size: 2792 bytes --]

> 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

On Wed, Mar 7, 2018 at 4:10 PM Martín Hötzel Escardó <
escardo...@gmail.com> 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.
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 3791 bytes --]

Re: Univalence from scratch

[Matt Oliveri]

[-- 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 --]

Re: [HoTT] Re: Univalence from scratch

[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

Re: [HoTT] Re: Univalence from scratch

[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
"25 years of constructive type theory"

Re: [HoTT] Univalence from scratch

[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


> 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
> 
> On Wed, Mar 7, 2018 at 4:10 PM Martín Hötzel Escardó 
> <escardo...@gmail.com <mailto:escardo...@gmail.com>> 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.
> 
>     -- 
>     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
>     <mailto:HomotopyTypeThe...@googlegroups.com>.
>     For more options, visit https://groups.google.com/d/optout.
> 

Re: [HoTT] Re: Univalence from scratch

[Martin Escardo]

On 08/03/18 09:25, Andrej Bauer wrote:
> 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
> 

Thanks Matt and Andrej.

Best,
Martin

Re: [HoTT] Univalence from scratch

[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/

Re: [HoTT] Univalence from scratch

[Jason Gross]

[-- Attachment #1: Type: text/plain, Size: 1347 bytes --]

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}, ...
?

On Fri, Mar 9, 2018 at 12:00 AM N. Raghavendra <ra...@hri.res.in> wrote:

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

[-- Attachment #2: Type: text/html, Size: 2215 bytes --]

Re: [HoTT] Univalence from scratch

[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 : 𝕌) , ....

Raghu.

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

Re: Univalence from scratch

[Jeff Olson]

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

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

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