HoTT Cafe

Contact owners and managers

1–30 of 287

A place where non-experts can discuss homotopy type theory and related topics. Experts are welcome to join in of course!

0 selected

fernan...@gmail.com

9/20/21

Interesting topics for a master thesis?

Hello everyone, I've been interested in homotopy type theory for a while, but I haven't read

unread,

Interesting topics for a master thesis?

Hello everyone, I've been interested in homotopy type theory for a while, but I haven't read

9/20/21

Yusha3 L, … Hendrik Boom3

6/14/21

Type theory beginners' study group

On Sun, Jun 13, 2021 at 11:04:30AM -0700, Yusha3 L wrote: Looks interesting. I got into type theory

unread,

Type theory beginners' study group

On Sun, Jun 13, 2021 at 11:04:30AM -0700, Yusha3 L wrote: Looks interesting. I got into type theory

6/14/21

12/16/20

A new problem equivalent to the RH - submission/peer-review

Hello, This paper needs peer-reviewing. I know for sure that the results are correct because I've

unread,

A new problem equivalent to the RH - submission/peer-review

Hello, This paper needs peer-reviewing. I know for sure that the results are correct because I've

12/16/20

3/3/20

Which texts on set theory and on (mathematical) logic are great companions to learning HoTT?

Hello. My university provides both a graduate level set theory course and a graduate level

unread,

Which texts on set theory and on (mathematical) logic are great companions to learning HoTT?

Hello. My university provides both a graduate level set theory course and a graduate level

3/3/20

Jizhan Huang (黃基展), Louis Garde2

2/5/20

Prerequisites to HoTT for those on at most advanced undergraduate level?

You will find some suggestions in previous messages of the group: See https://groups.google.com/d/msg

unread,

Prerequisites to HoTT for those on at most advanced undergraduate level?

You will find some suggestions in previous messages of the group: See https://groups.google.com/d/msg

2/5/20

Oscar Cunningham, … Matt Oliveri4

10/1/19

Directed HoTT based on profunctors?

I was also thinking that it might be nice for directed morphisms in a universe to be like profunctors

unread,

Directed HoTT based on profunctors?

I was also thinking that it might be nice for directed morphisms in a universe to be like profunctors

10/1/19

Henry Story, … Scott Morrison3

9/9/19

Arend proof assistant?

There's topic on Arend on the Lean discussion forum: https://leanprover.zulipchat.com/#narrow/

unread,

Arend proof assistant?

There's topic on Arend on the Lean discussion forum: https://leanprover.zulipchat.com/#narrow/

9/9/19

7/27/19

Formalizing Primes in UniMath

based on this: https://perimeterinstitute.ca/personal/tfritz/2014/primestype.pdf On Saturday, July 13

unread,

Formalizing Primes in UniMath

based on this: https://perimeterinstitute.ca/personal/tfritz/2014/primestype.pdf On Saturday, July 13

7/27/19

Yiming Xu, … Scott Morrison8

3/31/19

Hi, everyone. I have checked that Scott's instruction works! The instruction is now on : https://

unread,

Hi, everyone. I have checked that Scott's instruction works! The instruction is now on : https://

3/31/19

Yiming Xu, Michael Shulman2

3/19/19

Is there anything special about types such that it makes the Whitehead Theorem true for any type?

Whitehead's theorem in HoTT is *not* provable about all types unless we assert it as an axiom.

unread,

Is there anything special about types such that it makes the Whitehead Theorem true for any type?

Whitehead's theorem in HoTT is *not* provable about all types unless we assert it as an axiom.

3/19/19

Yiming Xu, Michael Shulman2

3/18/19

Confusion about Definition 8.6.5, page 286

The reason it disappears from the other side of the equation is that the target of the function types

unread,

Confusion about Definition 8.6.5, page 286

The reason it disappears from the other side of the equation is that the target of the function types

3/18/19

u594...@gmail.com, … Anders Mortberg7

3/15/19

Prove if A and B are sets, then A = B is also a set

Thank you a lot! I think I get it.

unread,

Prove if A and B are sets, then A = B is also a set

Thank you a lot! I think I get it.

3/15/19

Brandon Harrington, … Michael Shulman15

2/21/19

Structural Rules and Inductive Types

I am not sure that the terminology is uniform across all authors, in fact I am pretty sure it's

unread,

Structural Rules and Inductive Types

I am not sure that the terminology is uniform across all authors, in fact I am pretty sure it's

2/21/19

Sunrise Confusion, … Ben Sherman7

2/18/19

Relaxation of BHK interpretation that doesn't require empty type?

Thank you for your answers and explanations so far. I wanted to post this a lot earlier, but life got

unread,

Relaxation of BHK interpretation that doesn't require empty type?

Thank you for your answers and explanations so far. I wanted to post this a lot earlier, but life got

2/18/19

Matt Oliveri, … Michael Shulman6

12/16/18

(1-topos) theory in set theory vs HoTT

If by U_n you mean the universe of n-types (rather than just the n-th universe in a hierarchy that

unread,

(1-topos) theory in set theory vs HoTT

If by U_n you mean the universe of n-types (rather than just the n-th universe in a hierarchy that

12/16/18

Ali Caglayan, … Matt Oliveri7

9/19/18

Formal HoTT contexts

1) The context is propagated from the root (of the derivation) to the leaves without checking it as

unread,

Formal HoTT contexts

1) The context is propagated from the root (of the derivation) to the leaves without checking it as

9/19/18

Ali Caglayan, Michael Shulman3

9/7/18

Adjoint functor theorem in HoTT

A first note is that in type theory there is not really a notion of "proper class" and thus

unread,

Adjoint functor theorem in HoTT

A first note is that in type theory there is not really a notion of "proper class" and thus

9/7/18

Sunrise Confusion, Michael Shulman2

9/4/18

"First presentation" of type theory: replace lambda-abstraction by defining equation?

On Mon, Sep 3, 2018 at 12:17 PM Sunrise Confusion <hobbye...@gmail.com> wrote: > Is

unread,

"First presentation" of type theory: replace lambda-abstraction by defining equation?

On Mon, Sep 3, 2018 at 12:17 PM Sunrise Confusion <hobbye...@gmail.com> wrote: > Is

9/4/18

Ali Caglayan, … Michael Shulman12

8/11/18

Topos theory in HoTT

Right, this is exactly what I said would be really nice to have, but doesn't yet exist. On Sat,

unread,

Topos theory in HoTT

Right, this is exactly what I said would be really nice to have, but doesn't yet exist. On Sat,

8/11/18

Ali Caglayan, … Andrej Bauer3

8/7/18

Proposed change to HoTT wiki

There's such a thing as sections. With kind regards, Andrej

unread,

Proposed change to HoTT wiki

There's such a thing as sections. With kind regards, Andrej

8/7/18

Ali Caglayan, … Michael Shulman5

8/3/18

Smash products in HoTT

My memory is that the adjunction is a little subtle, right? You've shown that there is a smash/

unread,

Smash products in HoTT

My memory is that the adjunction is a little subtle, right? You've shown that there is a smash/

8/3/18

Henry Story, … Jacques Carette3

7/30/18

negative and fractional types?

Right. And you'll notice that the James-Sabry paper was never published. That's because the

unread,

negative and fractional types?

Right. And you'll notice that the James-Sabry paper was never published. That's because the

7/30/18

Tim Campion, … Michael Shulman4

6/26/18

Grappling with semisimplicial types

Thanks, Mike! It's good to know that I wasn't going crazy regarding the associahedra, and

unread,

Grappling with semisimplicial types

Thanks, Mike! It's good to know that I wasn't going crazy regarding the associahedra, and

6/26/18

Ali Caglayan, … Michael Shulman4

6/13/18

Eilenberg-Maclane spaces in HoTT

I don't think using ooGroup is a good idea for this; ooGroups are essentially defined by having a

unread,

Eilenberg-Maclane spaces in HoTT

I don't think using ooGroup is a good idea for this; ooGroups are essentially defined by having a

6/13/18

sami a, Ben Lee2

5/24/18

Fwd: Us congress hearing of maan alsaan Money laundry قضية الكونغجرس لغسيل الأموال للمليادير معن الصانع

Apologies for the spam, this user is now being moderated.

unread,

Fwd: Us congress hearing of maan alsaan Money laundry قضية الكونغجرس لغسيل الأموال للمليادير معن الصانع

Apologies for the spam, this user is now being moderated.

5/24/18

5/9/18

Functor composition

I am trying to understand the coherence condition on associativity of the composition of functors. I

unread,

Functor composition

I am trying to understand the coherence condition on associativity of the composition of functors. I

5/9/18

3/31/18

"Categories for the Working Philosopher"

"Categories for the Working Philosopher" is a recent book edited by Elaine Landry with a

unread,

"Categories for the Working Philosopher"

"Categories for the Working Philosopher" is a recent book edited by Elaine Landry with a

3/31/18

louis...@free.fr, … Tom Jack5

3/30/18

Induction as a special case of recursion ?

> We can use it to prove by recursion that: > forall n:N, p1(REC(n)) = n In this step, you use

unread,

Induction as a special case of recursion ?

> We can use it to prove by recursion that: > forall n:N, p1(REC(n)) = n In this step, you use

3/30/18

Andrew Dabrowski, … Michael Shulman46

11/3/17

HoTT applied to something other than topology

On Wed, Nov 1, 2017 at 7:19 PM, Andrew Dabrowski <unhan...@gmail.com> wrote: > Isn't

unread,

HoTT applied to something other than topology

On Wed, Nov 1, 2017 at 7:19 PM, Andrew Dabrowski <unhan...@gmail.com> wrote: > Isn't

11/3/17

Henry Story, … Julian Michael7

10/30/17

isomorphism in the real world

For sure, coinduction is interesting and seems like it could be useful if we want to describe real-

unread,

isomorphism in the real world

For sure, coinduction is interesting and seems like it could be useful if we want to describe real-

10/30/17

Search

Clear search

Close search

Google apps

Main menu