Long way to the HoTT book

[Danil Kolesnyk]

Hi!

I've recently known about the HoTT book.

And I want to understand the subject, but I'm not a mathematician.

I learned Analysis about 5 years ago, but forgot almost knowledge. 

Could you suggest books( theory and exercises) list to start from Set Theory and to prepare myself for the HoTT book.

WBR Danil

[Colin Adams]

I'm not a mathematician either - I would suggest just reading the book itself (repeating chapters 1 and 2 a lot). 

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

[Henry Story]

On Monday, 13 July 2015 12:34:05 UTC+1, Colin Adams wrote:

I'm not a mathematician either - I would suggest just reading the book itself (repeating chapters 1 and 2 a lot). 

Yes, chapter 1 is very readable. I found and 2 gets a bit harder but one gets through it. 

I worked like this: I read as much as I could in one go so that I could understand where this whole project was going. I found that after 5 pages like that I usually got stuck, because I had failed to understand some concept properly. Then I had to back-track and re-read carefully, doing a few exercises when needed.  After chapter 1 it gets harder going because of extra knowledge from topology that is required, but chapter 2 is well explained and quite intuitive.

 In any case it is good to have another text so that if you get stuck in one you can refer back to the other one to get you unstuck - it helps to have two eyes to see the third dimension. 

I recently found the articles here which would have helped me when I was getting going:

   http://www.bristol.ac.uk/arts/research/projects/homotopy-type-theory/

There is a primer there, and a number of other philosophical texts that help give one overview of the subject. What is nice is that it starts there with HoTT-  that is HoTTwithout the topological stuff, and explains there some of the tricky concepts of equality very nicely. The primer also ties in nicely with the more logical formalism.

Finally I think it helps to see a real person explain a project with chalk and passion. Robert Harper's course is really helpful there.

    http://www.cs.cmu.edu/~rwh/courses/hott/

What you get to see there is:

  • Why he is passionate about it - which may get you to understand things and why you should care - what he finds problematic with HoTT, what bothers him, etc... Ie how this field is alive.

  • how the reasoning  and notation works:

    + how to pronounce the symbols, what their meaning is, how they are meant to be used. New notations written on a piece of paper can be quite puzzling because one is constantly wondering if one has missed something. By seeing someone use it you get to understand what is automatic, presupposed, unimportant, and what you need to pay attention to

    + he makes mistakes on the board, and the students help him fix his mistakes, so you see how the notation is meant to work. You get to see the objective nature of the notation how it works as a communication tool

 • larger contextual issue: eg notational clashes between areas of mathematics that may be misleading you

 • interestingly the whole course starts off with Brouwers notion of mathematics as a language of communication

etc.. A lot of things that just don't go through well in books, but that are really important to understand.

 

My guess is that after that one should try learning how to program in this, probably by playing with coq, but I have not gotten there yet...

[Siddhartha Gadgil]

I taught a course last semester at undergraduate level that I hoped was pre-HoTT, and had a course blog on this at:

     http://siddhartha-gadgil.github.io/LogicTypesSpaces/

I don't know if this is much use, especially standalone. Reading the posts from the archive  from the beginning may be  some use.

regards,

Siddhartha

[Henry Story]

Is the language you are using in your examples coq ? ( Sorry I am new to this and it is not evident to me )

[Siddhartha Gadgil]

I used Agda. The course was over a couple of months ago - offline at the Indian Institute of Science. But I may try to make it online (my experience is trying to do both at once does not work well).

best,

Siddhartha

[Henry Story]

I discovered Steve Awodey's talk "Univalence as a new Principle of Logic" 

   

  http://www.mathtube.org/lecture/video/univalence-new-principle-logic

which should perhaps be the first video to watch. 

Mind you around minute 46 he does not quite explain why substitution of equivalents does not work automatically everywhere, though it is really simple to explain when discussiong belief contexts.  That is statements made in belief contexts, or involving propositional attitudes, such as the following are invalid. 

Laura Lane loves Superman

Superman = Clark Kent

---------

Laura Lane loves Clark Kent

I think that's what he is getting at. Constructive logic helps here I think because the contexts act as belief contexts.

[Andrej Bauer]

On Tue, Jul 14, 2015 at 4:11 PM, Henry Story <henry...@gmail.com> wrote:
> Mind you around minute 46 he does not quite explain why substitution of
> equivalents does not work automatically everywhere, though it is really
> simple to explain when discussiong belief contexts.

In set theory:

The sets {∅} and {{∅}} are equivalent because they are both contractible.
It is the case that ∅ ∈ {∅}, however ∅ ∉ {{∅}} and so it is not the
case that we may substitute one for the other.

With kind regards,

Andrej

[Andrej Bauer]

> The sets {∅} and {{∅}} are equivalent because they are both contractible.
> It is the case that ∅ ∈ {∅}, however ∅ ∉ {{∅}} and so it is not the
> case that we may substitute one for the other.

Let me be a bit more explicit, and also use more logical notation, as
I think it will get the point accross a bit better.

Consider the sets

a := {∅}
b := {{∅}}

and the logical formula

φ(x) := ∀ y ∈ x . ¬ ∃ z ∈ y . z = z

The formula φ(x) says that every element of x is an empty set. Now we have:

1) a and b are equivalent because they are both contractible
2) φ(a) is true
3) φ(b) is false

The principle that equivalent objects may be used interchangably is
therefore violated in set theory.

With kind regards,

Andrej

[Henry Story]

Thanks for this intriguing example. This raises the following question. In a recent talk Prof. Vladimir wrote: 

As a part of Univalent Foundations we now have a formalization of set theory in the form of the theory of types of h-level 2 in MLTT.

How does that work out then in the new set theory? Is there an overview of this yet?

Also though your example shows a more stunning example for mathematicians of a problem of substitution is the example I gave of intentional contexts also an example where that would make sense?

 

 

With kind regards,

Andrej

[Andrej Bauer]

On Tue, Jul 14, 2015 at 10:28 PM, Henry Story <henry...@gmail.com> wrote:
> How does that work out then in the new set theory? Is there an overview of
> this yet?

When sets are viewed as h-level 2 in MLTT then interchangeability of
equivalent sets is validated by the univalence axiom. The set theory
which arises this way is really a kind of type theory, as opposed to
it being a first-order theory, like ZFC. You may wish to read the nlab
page on "structural set theory"
(http://ncatlab.org/nlab/show/structural+set+theory) to see what's
going on.

With kind regards,

Andrej

[Mark Farrell]

Hi Danil,

I believe that I may also be in a somewhat similar situation as you. I am trying to gain momentum in understanding and working in homotopy type theory, so that eI ideally could start to e.g. contribute to the research programme. Mind you, I have limited background knowledge and skills that would enable me to do so. I think I am slowly getting there, but still have more ground to cover.

Reflecting on my experiences so far, I think I would (personally) approach homotopy type theory in this order:

1) Begin with Frank Pfenning's 2012 lectures on proof theory foundations.

Lecture 1 - https://www.youtube.com/watch?v=YRu7Xi-mNK8
Lecture 2 - https://www.youtube.com/watch?v=JzIAEv8fN88
Lecture 3 - https://www.youtube.com/watch?v=nw0JAF79gYI
Lecture 4- https://www.youtube.com/watch?v=_XtflAEN6aA

2) Watch Ed Moorhouse's 2015 lectures on category theory foundations (as an algebraic approach to proof theory).

Playlist - https://www.youtube.com/playlist?list=PLiHLLF-foEew8Xa8TJfEqF4reiDDWYbV1

3) Watch Robert Harper's lectures on type theory foundations, which I think Pfenning and Moorhouse's lectures better prepared me to understand.

Playlist - https://www.youtube.com/watch?v=U8pBjQ84E9g&list=PLiHLLF-foEewJDTQhXW2Iogu_lQmxkDDe

4) Learn how to write a proof checker for intensional type theory.

Stephanie Weirich's project (w/ links to videos) on how to write a proof checker - https://github.com/sweirich/pi-forall
MiniTT tutorial - http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf
MiniAgda project - http://www2.tcs.ifi.lmu.de/~abel/miniagda/

5) Listen to Dan Licata on homotopy type theory.

Podcast episode - http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on-homotopy-type-theory/

6) Watch the IAS lecture on homotopy theory in type theory.

Link - https://www.youtube.com/watch?v=ziN2XcK5-PQ

7) Watch the IAS lecture on calculating the fundamental group of the circle in homotopy type theory.

Link - https://video.ias.edu/members/licata2012Nov26

8) Watch the IAS lecture on Eilenberg-MacLane spaces in homotopy type theory.

Link - http://video.ias.edu/univalent/1213/0313-DanielLicata

9) Watch the Oxford lecture on cubical type theory.

Link - https://www.youtube.com/watch?v=lt8JgGRw7gg&list=UU7qaZ5pg0l0cDKb1y4yhHRQ

10) Check out the cubical type theory project on GitHub.

Link - https://github.com/mortberg/cubicaltt

11) Approach the HoTT book and other research on HoTT.

This is likely not the only way to acquire some background knowledge to approach the subject of homotopy type theory, but (somewhat in retrospect) it is what I would do, at least coming from my particular background.

Hope that helps you, and others who might be reading in a similar situation.

-Mark

[Danil Kolesnyk]

Hi Mark!

It's very pleasure.

Thank you for your detailed answer.

WBR

Daniil

Цей електронний лист відправлено з вільного від вірусів комп'ютера, захищеного програмою Avast. www.avast.com

--
You received this message because you are subscribed to a topic in the Google Groups "HoTT Cafe" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/hott-cafe/VHzQWyYbXt0/unsubscribe.
To unsubscribe from this group and all its topics, send an email to hott-cafe+...@googlegroups.com.