Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] On the Use of Computational Paths in Path Spaces of Homotopy Type Theory
@ 2018-10-14 17:15 Ali Caglayan
  2018-10-14 19:05 ` Corlin Fardal
  2018-10-30  2:02 ` [HoTT] Quantum Groups José Manuel Rodriguez Caballero
  0 siblings, 2 replies; 4+ messages in thread
From: Ali Caglayan @ 2018-10-14 17:15 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I have seen these papers on the arXiv for a while now:

https://arxiv.org/abs/1804.01413

https://arxiv.org/abs/1803.01709

Can anybody explain what they are about?

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 4+ messages in thread

* [HoTT] On the Use of Computational Paths in Path Spaces of Homotopy Type Theory
  2018-10-14 17:15 [HoTT] On the Use of Computational Paths in Path Spaces of Homotopy Type Theory Ali Caglayan
@ 2018-10-14 19:05 ` Corlin Fardal
  2018-10-30  2:02 ` [HoTT] Quantum Groups José Manuel Rodriguez Caballero
  1 sibling, 0 replies; 4+ messages in thread
From: Corlin Fardal @ 2018-10-14 19:05 UTC (permalink / raw)
  To: Homotopy Type Theory

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

From vaugely skimming through it, it looks like they define a more explicit version of judgmental equality, from which they found an extensional type theory, and proceed to calculate the fundamental group of different spaces in that theory.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 4+ messages in thread

* [HoTT] Quantum Groups
  2018-10-14 17:15 [HoTT] On the Use of Computational Paths in Path Spaces of Homotopy Type Theory Ali Caglayan
  2018-10-14 19:05 ` Corlin Fardal
@ 2018-10-30  2:02 ` José Manuel Rodriguez Caballero
  2018-10-30  3:21   ` Michael Shulman
  1 sibling, 1 reply; 4+ messages in thread
From: José Manuel Rodriguez Caballero @ 2018-10-30  2:02 UTC (permalink / raw)
  To: HomotopyTypeTheory

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

Hello,
  Roughly speaking, a quantum group is an algebraic structure which is
obtained by means of a deformation of a group. There rigorous definition is
here: https://ncatlab.org/nlab/show/quantum+group

Official reference to quantum groups: Kassel, Christian (1995), Quantum
groups, Graduate Texts in Mathematics, 155, Berlin, New York:
Springer-Verlag, doi:10.1007/978-1-4612-0783-2, ISBN 978-0-387-94370-1, MR
1321145

Deformations... homotopy type... Well, given a "well-behaved" family of
quantum groups, which are deformations of the same group, is it "natural"
to define this family as a homotopy type? Is HoTT, in some way, a natural
setting to work with quantum groups because types and homotopy types are
identified?

Kind Regards,
José 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 4+ messages in thread

* Re: [HoTT] Quantum Groups
  2018-10-30  2:02 ` [HoTT] Quantum Groups José Manuel Rodriguez Caballero
@ 2018-10-30  3:21   ` Michael Shulman
  0 siblings, 0 replies; 4+ messages in thread
From: Michael Shulman @ 2018-10-30  3:21 UTC (permalink / raw)
  To: josephcmac; +Cc: HomotopyTypeTheory

I doubt it.  My understanding of quantum groups is that they are
supposed to be groups with "noncommutative underlying spaces", and the
homotopy types of HoTT are all "commutative" in this sense.
On Mon, Oct 29, 2018 at 7:02 PM José Manuel Rodriguez Caballero
<josephcmac@gmail.com> wrote:
>
> Hello,
>   Roughly speaking, a quantum group is an algebraic structure which is obtained by means of a deformation of a group. There rigorous definition is here: https://ncatlab.org/nlab/show/quantum+group
>
> Official reference to quantum groups: Kassel, Christian (1995), Quantum groups, Graduate Texts in Mathematics, 155, Berlin, New York: Springer-Verlag, doi:10.1007/978-1-4612-0783-2, ISBN 978-0-387-94370-1, MR 1321145
>
> Deformations... homotopy type... Well, given a "well-behaved" family of quantum groups, which are deformations of the same group, is it "natural" to define this family as a homotopy type? Is HoTT, in some way, a natural setting to work with quantum groups because types and homotopy types are identified?
>
> Kind Regards,
> José 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 4+ messages in thread

end of thread, other threads:[~2018-10-30  3:21 UTC | newest]

Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-10-14 17:15 [HoTT] On the Use of Computational Paths in Path Spaces of Homotopy Type Theory Ali Caglayan
2018-10-14 19:05 ` Corlin Fardal
2018-10-30  2:02 ` [HoTT] Quantum Groups José Manuel Rodriguez Caballero
2018-10-30  3:21   ` Michael Shulman

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).