Email about higher inductive types.

gistfile1.txt

---------- Forwarded message ----------
From: Michael Shulman 
Date: Sunday, October 13, 2013
Subject: Generalizing Higher Inductive Types
To: Jason Gross <[email protected]>
Cc: Peter LeFanu Lumsdaine <[email protected]>


This looks kind of like a proposal for generalizing inductive types
that Peter discussed with me last year; I'm surprised if he didn't
mention it to you.  Remember my earlier comment in that thread said
that for a polynomial functor G to be the output of a constructor you
need G(1)=1.  If G(1) is not 1, then what you need is the extra data
of an element of G(1).  The point is that while a polynomial functor
with G(1)=1 has a left adjoint, that's only part of the story: the
reason that's true is that *every* polynomial functor is a parametric
right adjoint, i.e. the induced functor G : C -> C/G1 has a left
adjoint.  Thus, if you have an element of G1 specified along with your
constructor, then you can apply the left adjoint as before.  This
seems to be similar to what you're trying to do, but it has the
advantage of being semantically justified, hence consistent.  (-:

The answer to your first question is yes via the hub-and-spoke
construction, section 6.7 of the book.  I think my comment above
answers your second question.  And the answer to your third question
is no, there's no problem.  You should think of the elements of
0-truncation of type as equivalence/isomorphism classes of types.  In
section 10.2 of the book, the 0-truncation of hSet is called the "type
of cardinal numbers".

Mike

On Sat, Oct 12, 2013 at 8:31 PM, Jason Gross <[email protected]> wrote:
> Hi,
> I've been thinking a bit about the proposal that I mentioned to you, Peter,
> for generalizing higher inductive types so that equality isn't special
> (which I described partially at
> http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/comment-page-1/#comment-29867).
> I've been trying to compose an email to the homotopy type theory mailing
> list with a more fleshed out version, but have been getting caught up in how
> to phrase the fully general statement without getting lost in notation.
> But, in the meantime, I wanted to ask a question about an interesting case
> that I stumbled upon:
>
> In my proposal (or the slight generalization of the one that I described,
> where you generalize over not just constructors but any term of the
> inductive type you're constructing), you can do hProp-truncation as
>
> Inductive hProp_trunc (A : Type) :=
> | inhabited : A -> hProp_trunc A
> | trunc_hProp_trunc : forall x y : hProp_trunc A, x = y
> exhibiting
> | trunc_hProp_trunc := fun x y => idpath : x = _.
>
>
> However, you can't do 0-truncation, which you'd want to do as
>
> Inductive hSet_trunc (A : Type) :=
> | class_of : A -> hSet_trunc
> | trunc_class_of : forall (x y : hSet_trunc A) (p q : x = y), p = q
> exhibiting
> | trunc_class_of := fun x y p q => ??? : p = q.
>
> because you don't get to generalize things of type [@paths (hSet_trunc A) _
> _], only things of type [hSet_trunc A].  So it seems that you might not be
> able to get 0-truncation, unless there's a way to do it with just HITs
> involving equalities of constructors.  The reason this seems right to me is
> that, for example, having a version of [paths] with two constructors causes
> (I think) a contradiction:
>
> Inductive paths2 A (x : A) : A -> Type :=
> | idpath1 : paths2 x x
> | idpath2 : paths2 x x.
>
> Inductive hSet_bad (A : Type) :=
> | class_of : A -> hSet_bad
> | trunc_class_of : forall (x y : hSet_bad A) (p q : paths2 x y), p = q.
>
> (* You should be able to prove that [idpath1 <>  idpath2], and then derive a
> contradiction from [trunc_class_of]. *)
>
> So I am especially curious about the following things:
>
> Is it ok if the HITs can only add paths between constructors (or things of
> the inductive type we're defining), and no higher path constructors?
> Why is it ok to have an n-truncation HIT?  (What's special about equality
> that lets you do this with equality, but not the [paths2] type that I
> defined, while both can work for hProp-truncation?)
> What does the 0-truncation of [Type] look like, and are there any problems
> with univalence and the 0-truncation of [Type]?  (I don't have a good
> intuition here, so I'm wondering if you can run into trouble with knowing
> that two types are isomorphic, but not being able to know which isomorphism
> is used.  I suspect the answer is no, but I'm not completely sure.)
>
>
> -Jason