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
Chronological Thread
- From: Conor McBride <conor AT strictlypositive.org>
- To: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq
- Date: Thu, 9 Jan 2014 11:26:33 +0000
On 9 Jan 2014, at 10:51, Matthieu Sozeau
<matthieu.sozeau AT gmail.com>
wrote:
> On 9 janv. 2014, at 11:42, Altenkirch Thorsten
> <psztxa AT exmail.nottingham.ac.uk>
> wrote:
>
>>>
>>>
>>>
>>> About K: Coq has managed to describe a pattern-match which does not
>>> allow it (by making less unification information available in the
>>> branches), and I don't think it's that relevant to the problem at hand,
>>> which is mostly concerned about when a term is a subterm of another.
>>
>> I don't agree!
>>
>> If the only proof of equality is refl then it is clear that subst should
>> preserve the structural ordering. So K and the wrong (because untyped)
>> subterm ordering are related.
>
> +1: All these counterexamples implicitly assume UIP on equalities of types,
> don’t they?
In the sense that a previously valid assumption has been quietly broken, yes.
> I’ve been wondering, in OTT adding Empty -> Box = Box would be outright
> inconsistent right? IIRC it would even actually reduce to _|_ as type
> equality is defined.
OTT separates sets from props. Indeed, the set equation
(Zero -> One) <-> One is considered
outright false, and in the Agda model, even computes to the proposition False.
However, equality of proof sets is more generous, amounting to propositional
extensionality:
Prf (False => True) <-> Prf True
is given by the proposition
((False => True) => True) /\ (True => False => True)
whose proof set is inhabited.
The intuition is that OTT type equality means a rather conservative notion of
compatibility of run-time representation, so that transportation by equality
can definitely be erased. Proof sets have no run-time representation, so we
can
relax equality to mutual implication.
All the best
Conor
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, (continued)
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Vladimir Voevodsky, 01/07/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Jean Goubault-Larrecq, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Frédéric Blanqui, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/08/2014
- Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Matthieu Sozeau, 01/08/2014
- Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Frédéric Blanqui, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Altenkirch Thorsten, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Matthieu Sozeau, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Conor McBride, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Bruno Barras, 01/09/2014
- RE: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Nikhil Swamy, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Andreas Abel, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Jorge Luis Sacchini, 01/10/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Frédéric Blanqui, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Jean Goubault-Larrecq, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Vladimir Voevodsky, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Bruno Barras, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Andrej Bauer, 01/08/2014
Archive powered by MHonArc 2.6.18.