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