HITs with inductive higher constructors

[Thorsten Altenkirch]

Hi,

We are working on a generic theory for higher Inductive Types (HITs). HiTs have not only first order constructors

c0 : . . . -> T

but also higher constructors like

c1 . . .  -> t =_T u

c2 . . . -> v =_(t’ =_T u’) w

etc. We want to use an approach related to containers to make sure that all the references to T are “strictly positive” and that they type has a reasonable semantics. It seems that we can also cover the case where . . . again contains equations of the same level as the codomain. That is we could write

b : T 

c : b =_T b

d : b =_T b -> b =_T  b

Nice, but what is the use of this? Does anybody know a HIT which uses inductive higher constructors like this and which makes any (intuitive) sense? 

Cheers,

Thorsten & Gabe

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.

[Michael Shulman]

I take it you don't just mean the sort of constructor that arises
naturally in, say, the 0-truncation:

tr : A -> ||A||₀
uip : (a b : ||A||₀) -> (p q : a = b) -> (p = q)

because here the codomain p=q of 'uip' is at a higher "level" than the
type a=b in the domain?

[Michael Shulman]

Is that really the suspension of the natural numbers? What does
something like "midS (mid0 . (midS mid0)^-1 . mid0)" correspond to in
the usual presentation of Susp Nat?

On Thu, Mar 19, 2015 at 12:01 PM, Fran Mota <fmo...@gmail.com> wrote:
> The suspension of the natural numbers (written as a single inductive type)
> is such a HIT:
>
> SuspNat ::=
> | north : SuspNat
> | south : SuspNat
> | mid0 : (north = south)
> | midS : (north = south) -> (north = south)
>
> And in general you could suspend any usual inductive type like this
> explicitly, although it might be better to find a more natural example of
> "path to path" constructors.

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

[Michael Shulman]

Maybe one factor is that the hub-and-spoke translation does not
respect judgmentality of computation rules?

On Thu, Mar 19, 2015 at 12:08 PM, Dan Licata <d...@cs.cmu.edu> wrote:
>
> Hi Thorsten and Gabe,
>
> I am wondering why the relative "level" of the arguments/results of the constructor should even be a factor in what kinds of definitions can be allowed (if I understand you correctly here).
>
> With the hub-and-spoke technique, can't you smuggle in an argument with an arbitrary level no matter what level restrictions you make?
>
> I.e. suppose you only allow only point arguments, then you can have
>
> c0 : (S^n -> T) -> any globe in T
>
> which is equivalent to
>
> c0 : n-loop in T -> any globe in T
>
> -Dan

[Alexander Altman]

One such HIT is the following type, which I've mentioned before on the "HoTT Café" (formerly "HoTT Amateurs") list:

PNest : Type
base : PNest
nest : base = base -> base = base

[Thorsten Altenkirch]

Hi Dan,

the question wasn’t so much “should it be allowed” but rather “what is it
good for”?

>I am wondering why the relative "level" of the arguments/results of the
>constructor should even be a factor in what kinds of definitions can be
>allowed (if I understand you correctly here).
>
>With the hub-and-spoke technique, can't you smuggle in an argument with
>an arbitrary level no matter what level restrictions you make?
>
>I.e. suppose you only allow only point arguments, then you can have
>
>c0 : (S^n -> T) -> any globe in T
>
>which is equivalent to
>
>c0 : n-loop in T -> any globe in T

However, this is a good point: Indeed we could even have

c0 : (X -> T) -> any globe in T


where X is a parameter. Then the domain of c0 can depend on arbitrary high
levels depending on the argument since we could instantiate X with any S^n.

However, I think we can make precise what the level of the domain is.
Clearly a constructor with a domain C -> T where C is n-truncated can
depend on globes of level n. Hence, in your example (S^n -> T) has the
same level as n-loops namely n, while the level of X -> T is unbounded.

Hence our question is: what are natural examples of HITs whose domain is
of the same (or higher level) as the codomain?

It seems that so far all examples are of the type Mike mentions where the
argument of a constructor is of a lower level as the result.

We had also thought of examples like the one Fran mentions but as Mike
points out it isn’t clear what

SuspNat ::=

| north : SuspNat

| south : SuspNat

| mid0 : (north = south)

| midS : (north = south) -> (north = south)

actually defines.


Thorsten

[Dan Licata]

Hi Thorsten and Gabe,

I am wondering why the relative "level" of the arguments/results of the constructor should even be a factor in what kinds of definitions can be allowed (if I understand you correctly here).

With the hub-and-spoke technique, can't you smuggle in an argument with an arbitrary level no matter what level restrictions you make?

I.e. suppose you only allow only point arguments, then you can have

c0 : (S^n -> T) -> any globe in T

which is equivalent to

c0 : n-loop in T -> any globe in T

-Dan



On Mar 19, 2015, at 2:53 PM, Michael Shulman <shu...@sandiego.edu> wrote:

[Fran Mota]

The suspension of the natural numbers (written as a single inductive type) is such a HIT:

SuspNat ::=

  | north : SuspNat

  | south : SuspNat

  | mid0  : (north = south)

  | midS  : (north = south) -> (north = south)

And in general you could suspend any usual inductive type like this explicitly, although it might be better to find a more natural example of "path to path" constructors.

[Dan Licata]

I'm glad the list was renamed! Much more welcoming.

-Dan

[Fran Mota]

Oops, that's a good point, I don't know what SuspNat defines either.

A better example for taking arguments of higher level is in order to emulate essentially algebraic theories using higher inductive types.

For example, if X is an hset of points, and E : X -> X -> Type specifies some edges, the free category on (X,E) is a higher inductive type:

FreeCategory X E ::=

  | id  : X -> FreeCategory X E

  | hom : (x1 x2 : X) -> E x1 x2 -> FreeCategory X E

  | dom : FreeCategory X E -> FreeCategory X E

  | cod : FreeCategory X E -> FreeCategory X E

  | compose : (m1 m2 : FreeCategory X E) -> (cod m1 = dom m2) -> FreeCategory X E 

  | dom_id : (x : X) -> dom (id x) = id x

  | cod_id : (x : X) -> cod (id x) = id x

  | dom_hom : (x1 x2 : X) -> (e : E x1 x2) -> dom (hom x1 x2 e) = id x1

  | cod_hom : (x1 x2 : X) -> (e : E x1 x2) -> cod (hom x1 x2 e) = id x2

  | dom_compose : (m1 m2 : FreeCategory X E) -> (p : cod m1 = dom m2) -> dom (compose m1 m2 p) = dom m1

  | cod_compose : (m1 m2 : FreeCategory X E) -> (p : cod m1 = dom m2) -> cod (compose m1 m2 p) = cod m2

  | unit_dom : (x : X) -> (m : FreeCategory X E) -> (p : cod (id x) = dom m) -> compose (id x) m p = m

  | unit_cod : (x : X) -> (m : FreeCategory X E) -> (p : cod m = dom (id x)) -> compose m (id x) p = m

  | associativity : (m1 m2 m3 : FreeCategory X E)
                   -> (p1 : cod m1 = dom m2)

                   -> (p2 : cod m2 = dom m3)

                   -> (p3 : cod (compose m1 m2 p1) = dom m3)

                   -> (p4 : cod m1 = dom (compose m2 m3 p2))

                   -> compose (compose m1 m2 p1) m3 p3 = compose m1 (compose m2 m3 p2) p4

  | truncate : (m1 m2 : FreeCategory X E) -> (p1 p2 : m1 = m2) -> p1 = p2

(or free pre-category). This is the free category, where the points of FreeCategory X E are just the morphisms in the free category. In this type, compose, dom_compose, cod_compose, unit_dom, unit_cod, associaitivity all require arguments of higher level. Especially compose, which requires a path argument to construct a point.

(Hopefully I didn't make too many mistakes in the definition above...)

[Michael Shulman]

I guess by "the free category on (X,E)" you mean "the set of arrows in
the free category on (X,E)". But in this case, at least, I think it
should be much easier to remember that categories are naturally a
dependently-typed theory and just build the hom-sets of that free
category as higher-inductive type families X -> X -> Type.

[Fran Mota]

That is more precisely what I mean, although the object-less representation of categories is well-known. In this case the dependent family approach is usually more sensible. But I don't know if that's generally true (or even possible) for all essentially algebraic theories.

[Peter LeFanu Lumsdaine]

On Sat, Mar 21, 2015 at 5:05 AM, Fran Mota <fmo...@gmail.com> wrote:

That is more precisely what I mean, although the object-less representation of categories is well-known. In this case the dependent family approach is usually more sensible. But I don't know if that's generally true (or even possible) for all essentially algebraic theories.

I seem to remember that this is always possible, though I’m afraid the source for that belief escapes me for the moment.

But regardless of that, this seems like a very nice class of examples.  Essentially algebraic are certainly something that arises “in nature”, even if particular cases are often better seen as dependent algebraic theories.

–p.

[Paolo Capriotti]

On Sat, Mar 21, 2015 at 3:04 AM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> On Sat, Mar 21, 2015 at 5:05 AM, Fran Mota <fmo...@gmail.com> wrote:
>>
>> That is more precisely what I mean, although the object-less
>> representation of categories is well-known. In this case the dependent
>> family approach is usually more sensible. But I don't know if that's
>> generally true (or even possible) for all essentially algebraic theories.
>
> I seem to remember that this is always possible, though I’m afraid the
> source for that belief escapes me for the moment.

I would have guessed differently, since essentially algebraic theories
are given by categories with finite limits, whereas dependent type
theories are given by things like categories with families, where only
display maps have pullbacks. So, if you have to take the pullback of
something that is not a fibration to express the domain of an
operation, I don't see how you can represent this in a dependent type
theory. For example, can you represent the following with dependent
types?

f : A -> A
g : A x A -> A, where g(x,y) is defined iff f x = f y.

Paolo

[Peter LeFanu Lumsdaine]

On Sat, Mar 21, 2015 at 9:10 PM, Paolo Capriotti <pa...@capriotti.io> wrote:

On Sat, Mar 21, 2015 at 3:04 AM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> On Sat, Mar 21, 2015 at 5:05 AM, Fran Mota <fmo...@gmail.com> wrote:
>>
>> That is more precisely what I mean, although the object-less
>> representation of categories is well-known. In this case the dependent
>> family approach is usually more sensible. But I don't know if that's
>> generally true (or even possible) for all essentially algebraic theories.
>
> I seem to remember that this is always possible, though I’m afraid the
> source for that belief escapes me for the moment.

I would have guessed differently, since essentially algebraic theories
are given by categories with finite limits, whereas dependent type
theories are given by things like categories with families, where only
display maps have pullbacks. So, if you have to take the pullback of
something that is not a fibration to express the domain of an
operation, I don't see how you can represent this in a dependent type
theory.

The point is that if we start from an EAT, we can choose to make as many things as we want fibrations.  In particular (your example below reminds me how to do the general case) we can always simply add a new relation over a type, and force it to be the equality of that type:

For example, can you represent the following with dependent

types?

f : A -> A
g : A x A -> A, where g(x,y) is defined iff f x = f y.

|– A type

x,y:A |— E(x,y) type

x:A |— r(x) : E(x,y)

x,y:A, e:E(x,y) |— x=y : A

x,y:A, e1,e2:E(x,y) |— e1=e2 : E(x,y)

x:A |— f(x) : A

x:A, e:E(f(x),x) |— g(x,e) : A

Just to nail things down: this is equivalent in that for each finite limit category C, the category of models of your original EAT in C will be equivalent to the category of models of this GAT in C (with all maps of C considered fibrations); and naturally in C, of course.

Writing this example out, I now remember where the construction is from — Cartmell sketches it in his original paper introducing GAT’s.  I don’t know anywhere that it’s stated and proved carefully; does anyone else?

–p.

[Paolo Capriotti]

On Sat, Mar 21, 2015 at 12:37 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> On Sat, Mar 21, 2015 at 9:10 PM, Paolo Capriotti <pa...@capriotti.io> wrote:
>
>> For example, can you represent the following with dependent
>>
>> types?
>>
>> f : A -> A
>> g : A x A -> A, where g(x,y) is defined iff f x = f y.
>
>
> |– A type
>
> x,y:A |— E(x,y) type
>
> x:A |— r(x) : E(x,y)
>
> x,y:A, e:E(x,y) |— x=y : A
>
> x,y:A, e1,e2:E(x,y) |— e1=e2 : E(x,y)
>
> x:A |— f(x) : A
>
> x:A, e:E(f(x),x) |— g(x,e) : A
>

Oh, I see, very nice.

Paolo

[Thorsten Altenkirch]

Thank you, Fran.

Clearly, free essentially algebraic theories provide a good source of examples. However, I would usually prefer to cast this as an inductive family, as in the example of the free category.

Also it seems to me that we are only defining a sets. Or is there an example for a higher EAT? 

A;so is there an example where we would prefere EATs to Generalzed algebraic theories, i.e. using dependent types?

Cheers,

Thorsten