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

[Jason Gross]

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/20140523/ca3795ee/attachment.html