coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
Cc: Andrej Bauer <andrej.bauer AT andrej.com>, Coq Club <coq-club AT inria.fr>, "agda AT lists.chalmers.se" <agda AT lists.chalmers.se>, Cody Roux <cody.roux AT andrew.cmu.edu>, "homotopytypetheory AT googlegroups.com" <homotopytypetheory AT googlegroups.com>
Subject: Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq
Date: Wed, 8 Jan 2014 18:41:16 -0500

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.

Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, (continued)