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

[Peter LeFanu Lumsdaine]

Actually, if I am not mistaken, this is not a problem after all — because
one has to also add a corresponding extra clause for eqU in the recursive
definition of El, which one adds as

ap El (eqU p) == p

and from this, one can prove that El is an equivalence on paths.  (Thorsten
and I have been discussing this in a little more detail off-list; I think
he will be posting a longer follow-up email later.)

–p.




On Fri, May 23, 2014 at 5:27 PM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140524/4fa66721/attachment.html