[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy
theory & advantage of UF/Coq
Vladimir Voevodsky
vladimir at ias.edu
Thu Jan 9 00:41:16 CET 2014
On Jan 8, 2014, at 6:39 PM, Matthieu Sozeau <matthieu.sozeau at gmail.com> wrote:
> Well, take the transitive closure of p <_le le_succ n m p.
> — Matthieu
What is "p <_le le_succ n m p." ?
V.
More information about the Agda
mailing list