Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
* [HoTT] 1-Types are groupoids
@ 2019-02-20 11:08 kristian.alfsvag
  2019-02-20 11:48 ` Michael Shulman
  0 siblings, 1 reply; 3+ messages in thread
From: kristian.alfsvag @ 2019-02-20 11:08 UTC (permalink / raw)
  To: Homotopy Type Theory

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

Hi

I was wondering whether there exists a proof in literature that the type of 
1-truncated types is equivalent to the type of groupoids (defined as 
categories with only isomorphisms, for example).

I.e. a truncated version of the "types as infinity categories" viewpoint.

Thanks in advance,
Kristian Alfsvåg

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

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

* Re: [HoTT] 1-Types are groupoids
  2019-02-20 11:08 [HoTT] 1-Types are groupoids kristian.alfsvag
@ 2019-02-20 11:48 ` Michael Shulman
  2019-02-20 12:05   ` Niels van der Weide
  0 siblings, 1 reply; 3+ messages in thread
From: Michael Shulman @ 2019-02-20 11:48 UTC (permalink / raw)
  To: Kristian Alfsvåg; +Cc: Homotopy Type Theory

I assume you mean a proof inside of type theory?  This is Exercise 9.6
in the book; I don't know offhand of anywhere that the proof is
written out.  You do need to assume the groupoids are
saturated/univalent ("groupoids" in the terminology of the book rather
than "pregroupoids").

On Wed, Feb 20, 2019 at 3:08 AM <kristian.alfsvag@uib.no> wrote:
>
> Hi
>
> I was wondering whether there exists a proof in literature that the type of 1-truncated types is equivalent to the type of groupoids (defined as categories with only isomorphisms, for example).
>
> I.e. a truncated version of the "types as infinity categories" viewpoint.
>
> Thanks in advance,
> Kristian Alfsvåg
>
> --
> 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] 3+ messages in thread

* Re: [HoTT] 1-Types are groupoids
  2019-02-20 11:48 ` Michael Shulman
@ 2019-02-20 12:05   ` Niels van der Weide
  0 siblings, 0 replies; 3+ messages in thread
From: Niels van der Weide @ 2019-02-20 12:05 UTC (permalink / raw)
  To: Homotopy Type Theory

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

Together with Dan Frumin I formally defined the biequivalence between 1-types and univalent groupoids. See
https://github.com/nmvdw/groupoids

-- 
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] 3+ messages in thread

end of thread, back to index

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-02-20 11:08 [HoTT] 1-Types are groupoids kristian.alfsvag
2019-02-20 11:48 ` Michael Shulman
2019-02-20 12:05   ` Niels van der Weide

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox