Thanks for the references. So am I allowed to say a type is simply connected if any two paths are equal, or is that a meta statement which has no meaning within type theory.

On Thursday, 10 January 2019 21:12:13 UTC, Michael Shulman wrote:

Yes, you have to truncate the equality.  See section 7.5 of the HoTT
Book, and also Exercise 7.6.

On Thu, Jan 10, 2019 at 12:36 PM Brian Sanderson
<brianjs...@gmail.com> wrote:
>
> The type of a simply connected space would seem to make it just a set as any two paths with the same endpoints would be homotopic. I see that there would not be a continuous function from the space of pairs of paths to homotopies between them. What would the type of a simply connected space look like? Can I say in type theory any two equalities are equal without having a function?
>
> --
> 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.