Skip to Content.
Sympa Menu

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

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


Archive powered by MHonArc 2.6.18.

Top of Page