[HoTT] Re: [Agda] Higher inductive-recursive definitions?

[Jason Gross]

Is there any way to make sense of "eqU commutes with J" as a higher
constructor?  It seems like postulating that "(x : U) -> (y : U) -> (p : El
x == El y) -> (P : Set -> Set) -> J (P o El) (eqU p) == J P p might buy you
what you want, if its sensical to postulate.  Another alternative (again,
if it could be made sense of) might be to postulate IsEquiv (ap El).

-Jason
On May 23, 2014 9:59 PM, "Jason Gross" <jasongross9 at gmail.com> wrote:

> If you had very/insanely dependent functions, you might be able try
> something like
>
> ElimU : (X : U -> Set)
>        -> (n : X nat)
>        -> (p : (a : U) -> X a -> (b : El a -> U) -> ((x : El a) -> X (b
> x)) -> X (pi a b))
>        -> (H : (a : U) -> (b : U) -> (eq : El a == El b) -> transport X
> (eqU eq) (ElimU X n p H a) == ElimU X n p H b)
>        -> (a : U) -> X a
> ElimU X n p H nat = n
> ElimU X n p H (pi a b) = p a (ElimU X n p H a) b (λ x -> ElimU X n p H (b
> x))
>
> I'm not sure if this would pass the termination checker of any type theory
> with such functions, though...  (I'm also not sure what could be done in
> standard dependent type theories.)
>
> -Jason
>
>
> On Fri, May 23, 2014 at 6:23 PM, Altenkirch Thorsten <
> psztxa at exmail.nottingham.ac.uk> wrote:
>
>> Thank you for pointing this out Guillaume. I always fall for this one :-)
>>
>> We often want to say that a function on paths is an omega functor..
>>
>> Thorsten
>>
>> From: Guillaume Brunerie <guillaume.brunerie at gmail.com>
>> Date: Friday, 23 May 2014 16:27
>> To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>
>> Cc: agda list <agda at lists.chalmers.se>, "
>> HomotopyTypeTheory at googlegroups.com" <homotopytypetheory at googlegroups.com
>> >
>> Subject: [HoTT] Re: [Agda] Higher inductive-recursive definitions?
>>
>> Hi Thorsten,
>>
>> I don't know about the elimination rule, but I just wanted to point out
>> that you won't get a univalent universe in this way because eqU refl and
>> refl won't be identified, and similarly for concat (eqU p) (eqU q) and eqU
>> (concat p q).
>> And the obvious way to fix requires something like defining
>> semi-simplicial types internally...
>>
>> Guillaume
>> Le 23 mai 2014 15:23, "Altenkirch Thorsten" <
>> psztxa at exmail.nottingham.ac.uk> a écrit :
>>
>>> I would like to combine higher inductive definitions (I.e. have path
>>> constructors) with induction-recursion. One application would be to define
>>> a closed universe which is univalent. However, I cannot see any reasonable
>>> way to define an eliminator.
>>>
>>> Ok, I start with a simple universe(using Agda) - an inductive recursive
>>> definition
>>>
>>> data U : Set
>>> El : U -> Set
>>>
>>> data U where
>>>   nat : U
>>>   pi : (a : U)(b : El a -> U) -> U
>>>
>>> El nat = Nat
>>> El (pi a b) = (x : El a) -> El (b x)
>>>
>>> Now I can define an eliminator for the universe which allows me to
>>> define dependent functions by recursion over type codes:
>>>
>>> ElimU : (X : U -> Set)
>>>        -> (X nat)
>>>        -> ((a : U) -> X a -> (b : El a -> U) -> ((x : El a) -> X (b x))
>>> -> X (pi a b))
>>>        -> (a : U) -> X a
>>> ElimU X n p nat = n
>>> ElimU X n p (pi a b) = p a (ElimU X n p a) b (? x -> ElimU X n p (b x))
>>>
>>> However, I also would like to add a path constructor, which identifies
>>> codes if the have the same semantics:
>>>
>>> postulate
>>>   eqU : forall {a b} -> El a == El b -> a == b
>>>
>>> But I don't see a good way to modify the Eliminator. It seems that this
>>> corresponds to a condition on the eliminator as a whole.
>>>
>>> An alternative is to quotient the universe afterwards. However, the
>>> problem is that in this case I cannot lift the pi constructor to the
>>> quotiented universe – the usual problem when quotienting infinitary
>>> constructors. This can usually be overcome by defining the path
>>> constructors mutually..
>>>
>>> Any ideas? Maybe the whole thing doesn't make sense semantically?
>>>
>>> Thorsten
>>>
>>> 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.
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>> --
>> 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 at googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>> 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.
>>
>>  --
>> 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 at googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140524/c297e1ca/attachment-0001.html