* computing K @ 2017-04-25 9:46 Michael Shulman 2017-04-25 13:17 ` [HoTT] " Thomas Streicher ` (2 more replies) 0 siblings, 3 replies; 7+ messages in thread From: Michael Shulman @ 2017-04-25 9:46 UTC (permalink / raw) To: HomotopyT...@googlegroups.com 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] computing K 2017-04-25 9:46 computing K Michael Shulman @ 2017-04-25 13:17 ` Thomas Streicher 2017-04-25 14:10 ` Favonia 2017-04-25 22:05 ` Martin Escardo [not found] ` <f9cd4d85-a186-f228-cdc2-75ea4e434e0e@cs.bham.ac.uk> 2 siblings, 1 reply; 7+ messages in thread From: Thomas Streicher @ 2017-04-25 13:17 UTC (permalink / raw) To: Michael Shulman; +Cc: HomotopyT...@googlegroups.com 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 > ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] computing K 2017-04-25 13:17 ` [HoTT] " Thomas Streicher @ 2017-04-25 14:10 ` Favonia 0 siblings, 0 replies; 7+ messages in thread From: Favonia @ 2017-04-25 14:10 UTC (permalink / raw) To: Thomas Streicher, Michael Shulman Cc: HomotopyT...@googlegroups.com, Jesper Cockx [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] computing K 2017-04-25 9:46 computing K Michael Shulman 2017-04-25 13:17 ` [HoTT] " Thomas Streicher @ 2017-04-25 22:05 ` Martin Escardo [not found] ` <f9cd4d85-a186-f228-cdc2-75ea4e434e0e@cs.bham.ac.uk> 2 siblings, 0 replies; 7+ messages in thread From: Martin Escardo @ 2017-04-25 22:05 UTC (permalink / raw) To: HomotopyT...@googlegroups.com 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 > ^ permalink raw reply [flat|nested] 7+ messages in thread
[parent not found: <f9cd4d85-a186-f228-cdc2-75ea4e434e0e@cs.bham.ac.uk>]
* Re: [HoTT] computing K [not found] ` <f9cd4d85-a186-f228-cdc2-75ea4e434e0e@cs.bham.ac.uk> @ 2017-04-25 23:08 ` Michael Shulman 2017-04-26 20:40 ` Floris van Doorn 0 siblings, 1 reply; 7+ messages in thread From: Michael Shulman @ 2017-04-25 23:08 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT...@googlegroups.com 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] computing K 2017-04-25 23:08 ` Michael Shulman @ 2017-04-26 20:40 ` Floris van Doorn 2017-04-26 21:33 ` Floris van Doorn 0 siblings, 1 reply; 7+ messages in thread From: Floris van Doorn @ 2017-04-26 20:40 UTC (permalink / raw) To: Michael Shulman; +Cc: Martin Escardo, HomotopyT...@googlegroups.com [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] computing K 2017-04-26 20:40 ` Floris van Doorn @ 2017-04-26 21:33 ` Floris van Doorn 0 siblings, 0 replies; 7+ messages in thread From: Floris van Doorn @ 2017-04-26 21:33 UTC (permalink / raw) To: HomotopyT...@googlegroups.com [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
end of thread, other threads:[~2017-04-28 4:55 UTC | newest] Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-04-25 9:46 computing K Michael Shulman 2017-04-25 13:17 ` [HoTT] " Thomas Streicher 2017-04-25 14:10 ` Favonia 2017-04-25 22:05 ` Martin Escardo [not found] ` <f9cd4d85-a186-f228-cdc2-75ea4e434e0e@cs.bham.ac.uk> 2017-04-25 23:08 ` Michael Shulman 2017-04-26 20:40 ` Floris van Doorn 2017-04-26 21:33 ` Floris van Doorn
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).