[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