[Agda] Higher inductive-recursive definitions?

[Guillaume Brunerie]

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