computing K

computing K

[Michael Shulman]

Here is a little observation that may be of interest (thanks to
Favonia for bringing this question to my attention).

The Axiom K that is provable using unrestricted Agda-style
pattern-matching has an extra property: it computes to refl on refl.
That is, if we define

K: (A : Type) (x : A) (p : x == x) -> p == refl
K A x refl = refl

then the equation "K A x refl = refl" holds definitionally.  As was
pointed out on the Agda mailing list a while ago, this might be
considered a problem if one wants to extend Agda's --without-K to
allow unrestricted pattern-matching when the types are automatically
provable to be hsets, since a general hset apparently need not admit a
K satisfying this *definitional* behavior.

However (this is the perhaps-new observation), in good
model-categorical semantics, such a "computing K" *can* be constructed
for any hset.  Suppose we are in a model category whose cofibrations
are exactly the monomorphisms, like simplicial sets or any Cisinski
model category.  If A is an hset, then the map A -> Delta^*(PA) (which
type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence.
But it is also a split monomorphism, hence a cofibration; and thus an
acyclic cofibration.  Therefore, we can define functions by induction
on loops in A that have definitionally computing behavior on refl,
which is exactly what unrestricted pattern-matching allows.

Mike

Re: [HoTT] computing K

[Thomas Streicher]

In lccc's (actually finite limits cats) there is no problem to have K.
But K allows one to prove UIP which is in contradiction with UA. So we
can't have K in all model cat's modelling intensioal TT.

Thomas

> Here is a little observation that may be of interest (thanks to
> Favonia for bringing this question to my attention).
> 
> The Axiom K that is provable using unrestricted Agda-style
> pattern-matching has an extra property: it computes to refl on refl.
> That is, if we define
> 
> K: (A : Type) (x : A) (p : x == x) -> p == refl
> K A x refl = refl
> 
> then the equation "K A x refl = refl" holds definitionally.  As was
> pointed out on the Agda mailing list a while ago, this might be
> considered a problem if one wants to extend Agda's --without-K to
> allow unrestricted pattern-matching when the types are automatically
> provable to be hsets, since a general hset apparently need not admit a
> K satisfying this *definitional* behavior.
> 
> However (this is the perhaps-new observation), in good
> model-categorical semantics, such a "computing K" *can* be constructed
> for any hset.  Suppose we are in a model category whose cofibrations
> are exactly the monomorphisms, like simplicial sets or any Cisinski
> model category.  If A is an hset, then the map A -> Delta^*(PA) (which
> type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence.
> But it is also a split monomorphism, hence a cofibration; and thus an
> acyclic cofibration.  Therefore, we can define functions by induction
> on loops in A that have definitionally computing behavior on refl,
> which is exactly what unrestricted pattern-matching allows.
> 
> Mike
> 

Re: [HoTT] computing K

[Favonia]

[-- Attachment #1: Type: text/plain, Size: 2591 bytes --]

I believe Mike is talking about a restricted version of K which only
applies to types satisfying UIP, not all types. The question is whether a
"weak" K which might not compute can be "strictified" to another K which
does, at least in good models. By the way, my question about the restricted
K was due to Jesper's attempt to have Agda automatically detect types that
admit K (now temporarily disabled). -Favonia

On Tue, Apr 25, 2017 at 9:17 AM Thomas Streicher <
stre...@mathematik.tu-darmstadt.de> wrote:

> In lccc's (actually finite limits cats) there is no problem to have K.
> But K allows one to prove UIP which is in contradiction with UA. So we
> can't have K in all model cat's modelling intensioal TT.
>
> Thomas
>
> > Here is a little observation that may be of interest (thanks to
> > Favonia for bringing this question to my attention).
> >
> > The Axiom K that is provable using unrestricted Agda-style
> > pattern-matching has an extra property: it computes to refl on refl.
> > That is, if we define
> >
> > K: (A : Type) (x : A) (p : x == x) -> p == refl
> > K A x refl = refl
> >
> > then the equation "K A x refl = refl" holds definitionally.  As was
> > pointed out on the Agda mailing list a while ago, this might be
> > considered a problem if one wants to extend Agda's --without-K to
> > allow unrestricted pattern-matching when the types are automatically
> > provable to be hsets, since a general hset apparently need not admit a
> > K satisfying this *definitional* behavior.
> >
> > However (this is the perhaps-new observation), in good
> > model-categorical semantics, such a "computing K" *can* be constructed
> > for any hset.  Suppose we are in a model category whose cofibrations
> > are exactly the monomorphisms, like simplicial sets or any Cisinski
> > model category.  If A is an hset, then the map A -> Delta^*(PA) (which
> > type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence.
> > But it is also a split monomorphism, hence a cofibration; and thus an
> > acyclic cofibration.  Therefore, we can define functions by induction
> > on loops in A that have definitionally computing behavior on refl,
> > which is exactly what unrestricted pattern-matching allows.
> >
> > Mike
> >
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #2: Type: text/html, Size: 3299 bytes --]

Re: [HoTT] computing K

[Martin Escardo]

Interesting. So, then, here are some questions:

(1) Suppose, for given type A, a hypothetical

K: (x : A) (p : x == x) -> p == refl

is given, internally in a univalent type theory.

Is it possible to cook-up a K' of the same type, internally in univalent 
type theory,  with the definitional behaviour you require?

We are looking for an endofunction of the type ((x : A) (p : x == x) -> 
p == refl) that performs some sort of definitional improvement.

We know of an instance of such a phenomenon: if a factor f':||X||->A of 
some f:X->A through |-|:X->||X|| is given, then we can find another 
*definitional* factor f':||X||->A.

This is here in agda 
http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html#15508 
and also in a paper by Nicolai, Thorsten, Thierry and myself.

(2) Failing that, can we, given the same hypothetical K, cook-up a type 
A' equivalent to A (maybe A'= Sigma(x:A) (x=x)) with K' as above?

(That is, maybe A itself won't provably have (1), but still will have an 
equivalent manifestation which does.)

Or is this wishful thinking?

Martin

On 25/04/17 10:46, Michael Shulman wrote:
> Here is a little observation that may be of interest (thanks to
> Favonia for bringing this question to my attention).
>
> The Axiom K that is provable using unrestricted Agda-style
> pattern-matching has an extra property: it computes to refl on refl.
> That is, if we define
>
> K: (A : Type) (x : A) (p : x == x) -> p == refl
> K A x refl = refl
>
> then the equation "K A x refl = refl" holds definitionally.  As was
> pointed out on the Agda mailing list a while ago, this might be
> considered a problem if one wants to extend Agda's --without-K to
> allow unrestricted pattern-matching when the types are automatically
> provable to be hsets, since a general hset apparently need not admit a
> K satisfying this *definitional* behavior.
>
> However (this is the perhaps-new observation), in good
> model-categorical semantics, such a "computing K" *can* be constructed
> for any hset.  Suppose we are in a model category whose cofibrations
> are exactly the monomorphisms, like simplicial sets or any Cisinski
> model category.  If A is an hset, then the map A -> Delta^*(PA) (which
> type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence.
> But it is also a split monomorphism, hence a cofibration; and thus an
> acyclic cofibration.  Therefore, we can define functions by induction
> on loops in A that have definitionally computing behavior on refl,
> which is exactly what unrestricted pattern-matching allows.
>
> Mike
>

Re: [HoTT] computing K

[Michael Shulman]

Favonia, Dan Licata, and I spent a bit of time trying to answer (1)
but didn't get anywhere.  I haven't thought much about (2), but I
think we were unable to think of any nontrivial types for which we
could construct a computing K inside MLTT.

On Tue, Apr 25, 2017 at 3:04 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Interesting. So, then, here are some questions:
>
> (1) Suppose, for given type A, a hypothetical
>
> K: (x : A) (p : x == x) -> p == refl
>
> is given, internally in a univalent type theory.
>
> Is it possible to cook-up a K' of the same type, internally in univalent
> type theory,  with the definitional behaviour you require?
>
> We are looking for an endofunction of the type ((x : A) (p : x == x) -> p ==
> refl) that performs some sort of definitional improvement.
>
> We know of an instance of such a phenomenon: if a factor f':||X||->A of some
> f:X->A through |-|:X->||X|| is given, then we can find another
> *definitional* factor f':||X||->A.
>
> This is here in agda
> http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html#15508
> and also in a paper by Nicolai, Thorsten, Thierry and myself.
>
> (2) Failing that, can we, given the same hypothetical K, cook-up a type A'
> equivalent to A (maybe A'= Sigma(x:A) (x=x)) with K' as above?
>
> (That is, maybe A itself won't provably have (1), but still will have an
> equivalent manifestation which does.)
>
> Or is this wishful thinking?
>
> Martin
>
>
> On 25/04/17 10:46, Michael Shulman wrote:
>>
>> Here is a little observation that may be of interest (thanks to
>> Favonia for bringing this question to my attention).
>>
>> The Axiom K that is provable using unrestricted Agda-style
>> pattern-matching has an extra property: it computes to refl on refl.
>> That is, if we define
>>
>> K: (A : Type) (x : A) (p : x == x) -> p == refl
>> K A x refl = refl
>>
>> then the equation "K A x refl = refl" holds definitionally.  As was
>> pointed out on the Agda mailing list a while ago, this might be
>> considered a problem if one wants to extend Agda's --without-K to
>> allow unrestricted pattern-matching when the types are automatically
>> provable to be hsets, since a general hset apparently need not admit a
>> K satisfying this *definitional* behavior.
>>
>> However (this is the perhaps-new observation), in good
>> model-categorical semantics, such a "computing K" *can* be constructed
>> for any hset.  Suppose we are in a model category whose cofibrations
>> are exactly the monomorphisms, like simplicial sets or any Cisinski
>> model category.  If A is an hset, then the map A -> Delta^*(PA) (which
>> type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence.
>> But it is also a split monomorphism, hence a cofibration; and thus an
>> acyclic cofibration.  Therefore, we can define functions by induction
>> on loops in A that have definitionally computing behavior on refl,
>> which is exactly what unrestricted pattern-matching allows.
>>
>> Mike
>>
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe

Re: [HoTT] computing K

[Floris van Doorn]

[-- Attachment #1: Type: text/plain, Size: 4784 bytes --]

I think (1) is indeed wishful thinking.

I can disprove it assuming the following metatheoretical property. I think
this property holds for book-HoTT, but I'm not sure.

If X is a HIT and p : A -> X is a path constructor of X, and if p a ≡ p a'
for terms a a' : A then a ≡ a'. (Here ≡ is judgmental equality.)

I believe that similar properties are true for MLTT if p is a constructor
of an inductive type.

Now let I be the interval with points 0, 1 : I and consider the following
HIT:
HIT X :=
| * : X
| p : I -> * = *
| q : p(0) = refl
Note that X is the reduced suspension of the interval, which is
contractible, hence in particular a set. But assuming the above
metatheoretical property, X cannot have an axiom K with the definitional
properties Mike described. That would mean that p(0) ≡ p(1) and hence 0 ≡
1. But it is impossible that the two points of the interval are
judgmentally equal (because you can make a function which sends them to
equal, but not judgmentally equal terms, for example (Σ(X : Type), X =
empty) and (Σ(X : Type), X = unit)).

Best,
Floris

On 25 April 2017 at 19:08, Michael Shulman <shu...@sandiego.edu> wrote:

> Favonia, Dan Licata, and I spent a bit of time trying to answer (1)
> but didn't get anywhere.  I haven't thought much about (2), but I
> think we were unable to think of any nontrivial types for which we
> could construct a computing K inside MLTT.
>
> On Tue, Apr 25, 2017 at 3:04 PM, Martin Escardo <m.es...@cs.bham.ac.uk>
> wrote:
> > Interesting. So, then, here are some questions:
> >
> > (1) Suppose, for given type A, a hypothetical
> >
> > K: (x : A) (p : x == x) -> p == refl
> >
> > is given, internally in a univalent type theory.
> >
> > Is it possible to cook-up a K' of the same type, internally in univalent
> > type theory,  with the definitional behaviour you require?
> >
> > We are looking for an endofunction of the type ((x : A) (p : x == x) ->
> p ==
> > refl) that performs some sort of definitional improvement.
> >
> > We know of an instance of such a phenomenon: if a factor f':||X||->A of
> some
> > f:X->A through |-|:X->||X|| is given, then we can find another
> > *definitional* factor f':||X||->A.
> >
> > This is here in agda
> > http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/
> hsetfunext.html#15508
> > and also in a paper by Nicolai, Thorsten, Thierry and myself.
> >
> > (2) Failing that, can we, given the same hypothetical K, cook-up a type
> A'
> > equivalent to A (maybe A'= Sigma(x:A) (x=x)) with K' as above?
> >
> > (That is, maybe A itself won't provably have (1), but still will have an
> > equivalent manifestation which does.)
> >
> > Or is this wishful thinking?
> >
> > Martin
> >
> >
> > On 25/04/17 10:46, Michael Shulman wrote:
> >>
> >> Here is a little observation that may be of interest (thanks to
> >> Favonia for bringing this question to my attention).
> >>
> >> The Axiom K that is provable using unrestricted Agda-style
> >> pattern-matching has an extra property: it computes to refl on refl.
> >> That is, if we define
> >>
> >> K: (A : Type) (x : A) (p : x == x) -> p == refl
> >> K A x refl = refl
> >>
> >> then the equation "K A x refl = refl" holds definitionally.  As was
> >> pointed out on the Agda mailing list a while ago, this might be
> >> considered a problem if one wants to extend Agda's --without-K to
> >> allow unrestricted pattern-matching when the types are automatically
> >> provable to be hsets, since a general hset apparently need not admit a
> >> K satisfying this *definitional* behavior.
> >>
> >> However (this is the perhaps-new observation), in good
> >> model-categorical semantics, such a "computing K" *can* be constructed
> >> for any hset.  Suppose we are in a model category whose cofibrations
> >> are exactly the monomorphisms, like simplicial sets or any Cisinski
> >> model category.  If A is an hset, then the map A -> Delta^*(PA) (which
> >> type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence.
> >> But it is also a split monomorphism, hence a cofibration; and thus an
> >> acyclic cofibration.  Therefore, we can define functions by induction
> >> on loops in A that have definitionally computing behavior on refl,
> >> which is exactly what unrestricted pattern-matching allows.
> >>
> >> Mike
> >>
> >
> > --
> > Martin Escardo
> > http://www.cs.bham.ac.uk/~mhe
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #2: Type: text/html, Size: 6267 bytes --]

Re: [HoTT] computing K

[Floris van Doorn]

[-- Attachment #1: Type: text/plain, Size: 5113 bytes --]

Disregard previous email. I misread Mike's proposed computing K (I thought
it was refl on all loops).

On 26 April 2017 at 16:40, Floris van Doorn <fpvd...@gmail.com> wrote:

> I think (1) is indeed wishful thinking.
>
> I can disprove it assuming the following metatheoretical property. I think
> this property holds for book-HoTT, but I'm not sure.
>
> If X is a HIT and p : A -> X is a path constructor of X, and if p a ≡ p a'
> for terms a a' : A then a ≡ a'. (Here ≡ is judgmental equality.)
>
> I believe that similar properties are true for MLTT if p is a constructor
> of an inductive type.
>
> Now let I be the interval with points 0, 1 : I and consider the following
> HIT:
> HIT X :=
> | * : X
> | p : I -> * = *
> | q : p(0) = refl
> Note that X is the reduced suspension of the interval, which is
> contractible, hence in particular a set. But assuming the above
> metatheoretical property, X cannot have an axiom K with the definitional
> properties Mike described. That would mean that p(0) ≡ p(1) and hence 0 ≡
> 1. But it is impossible that the two points of the interval are
> judgmentally equal (because you can make a function which sends them to
> equal, but not judgmentally equal terms, for example (Σ(X : Type), X =
> empty) and (Σ(X : Type), X = unit)).
>
> Best,
> Floris
>
> On 25 April 2017 at 19:08, Michael Shulman <shu...@sandiego.edu> wrote:
>
>> Favonia, Dan Licata, and I spent a bit of time trying to answer (1)
>> but didn't get anywhere.  I haven't thought much about (2), but I
>> think we were unable to think of any nontrivial types for which we
>> could construct a computing K inside MLTT.
>>
>> On Tue, Apr 25, 2017 at 3:04 PM, Martin Escardo <m.es...@cs.bham.ac.uk>
>> wrote:
>> > Interesting. So, then, here are some questions:
>> >
>> > (1) Suppose, for given type A, a hypothetical
>> >
>> > K: (x : A) (p : x == x) -> p == refl
>> >
>> > is given, internally in a univalent type theory.
>> >
>> > Is it possible to cook-up a K' of the same type, internally in univalent
>> > type theory,  with the definitional behaviour you require?
>> >
>> > We are looking for an endofunction of the type ((x : A) (p : x == x) ->
>> p ==
>> > refl) that performs some sort of definitional improvement.
>> >
>> > We know of an instance of such a phenomenon: if a factor f':||X||->A of
>> some
>> > f:X->A through |-|:X->||X|| is given, then we can find another
>> > *definitional* factor f':||X||->A.
>> >
>> > This is here in agda
>> > http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/
>> hsetfunext.html#15508
>> > and also in a paper by Nicolai, Thorsten, Thierry and myself.
>> >
>> > (2) Failing that, can we, given the same hypothetical K, cook-up a type
>> A'
>> > equivalent to A (maybe A'= Sigma(x:A) (x=x)) with K' as above?
>> >
>> > (That is, maybe A itself won't provably have (1), but still will have an
>> > equivalent manifestation which does.)
>> >
>> > Or is this wishful thinking?
>> >
>> > Martin
>> >
>> >
>> > On 25/04/17 10:46, Michael Shulman wrote:
>> >>
>> >> Here is a little observation that may be of interest (thanks to
>> >> Favonia for bringing this question to my attention).
>> >>
>> >> The Axiom K that is provable using unrestricted Agda-style
>> >> pattern-matching has an extra property: it computes to refl on refl.
>> >> That is, if we define
>> >>
>> >> K: (A : Type) (x : A) (p : x == x) -> p == refl
>> >> K A x refl = refl
>> >>
>> >> then the equation "K A x refl = refl" holds definitionally.  As was
>> >> pointed out on the Agda mailing list a while ago, this might be
>> >> considered a problem if one wants to extend Agda's --without-K to
>> >> allow unrestricted pattern-matching when the types are automatically
>> >> provable to be hsets, since a general hset apparently need not admit a
>> >> K satisfying this *definitional* behavior.
>> >>
>> >> However (this is the perhaps-new observation), in good
>> >> model-categorical semantics, such a "computing K" *can* be constructed
>> >> for any hset.  Suppose we are in a model category whose cofibrations
>> >> are exactly the monomorphisms, like simplicial sets or any Cisinski
>> >> model category.  If A is an hset, then the map A -> Delta^*(PA) (which
>> >> type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence.
>> >> But it is also a split monomorphism, hence a cofibration; and thus an
>> >> acyclic cofibration.  Therefore, we can define functions by induction
>> >> on loops in A that have definitionally computing behavior on refl,
>> >> which is exactly what unrestricted pattern-matching allows.
>> >>
>> >> Mike
>> >>
>> >
>> > --
>> > Martin Escardo
>> > http://www.cs.bham.ac.uk/~mhe
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>
>

[-- Attachment #2: Type: text/html, Size: 6891 bytes --]