K and UIP · theory: type theory · Zulip Chat Archive

K is a rule, whereas UIP is a theorem. If you're talking about the formal theory or implementation or something, you tend to talk about the K rule, whereas if you're talking about the emergent mathematics or a temporary assumption, you tend to talk about UIP.

Mike Shulman (Jun 26 2021 at 18:33):

Well, both of then can be asserted internally as axioms too. But it's true that K can be given a computational interpretation and UIP can't.

Xuanrui Qi (Jun 27 2021 at 15:46):

The computational interpretation of K is just dependent pattern matching, right?

Mike Shulman (Jun 27 2021 at 21:07):

Leopold Schlicht (Jun 28 2021 at 17:23):

Thanks. How can it be the case that K computes while UIP doesn't if they are both equivalent? In what sense are they equivalent?

Mike Shulman (Jun 28 2021 at 17:42):

They're equivalent in the sense that when stated as axioms, either one can be proven from the other. But one can state a computation rule for the K axiom that is well-behaved (normalizing), whereas this doesn't seem possible for UIP.

Jon Sterling (Jun 28 2021 at 17:44):

Am I confused, or is this a distinction without a difference? Once I've got a computation rule for the K axiom, then I can define a computation rule for the UIP axiom (have the postulated axiom compute to the now-definable element P : UIP, defined by dependent pattern matching or whatever). This is a definitional extension of the calculus with K, so normalization is preserved.

Conor McBride (Jun 28 2021 at 17:44):

Hang on a minute. This will take me a few minutes to do properly. It took me a few years, back in the nineties.

Mike Shulman (Jun 28 2021 at 17:50):

@Jonathan Sterling Can you give a normalizing type theory in which K is defined in terms of UIP rather than vice versa?

Conor McBride (Jun 28 2021 at 17:51):

data I (X : Set)(x : X) : X -> Set where
  refl : I X x x

J : (X : Set)(x y : X)(q : I X x y) ->
    (P : (y : X)(q : I X x y) -> Set) ->
    P x refl ->
    P y q
J X x .x refl P p = p

K : (X : Set)(x : X)(q : I X x x) ->
    (P : (q : I X x x) -> Set) ->
    P refl ->
    P q
K X x refl P p = p

UIP : (X : Set)(x y : X)(q r : I X x y) -> I (I X x y) q r
UIP X x .x refl refl = refl

Here is the identity type, together with J, K and UIP all defined by dependent pattern matching.

Jon Sterling (Jun 28 2021 at 17:51):

I feel the question is really not so well-defined, but perhaps I am misunderstanding it. I think that "rather than" is doing a lot of work in this sentence ;-)

Conor McBride (Jun 28 2021 at 17:52):

J is exactly the standard induction principle you get for I by the usual scheme. (By yanking x to the left of : I get Christin Paulin's version, rather than Per's but they're equivalent.)

Mike Shulman (Jun 28 2021 at 17:53):

@Jonathan Sterling I mean, if I first add K and UIP as non-computing axioms, and then I add a reduction rule reducing K to its definition in terms of UIP, can I add further computation rules to make the theory normalizing?

Conor McBride (Jun 28 2021 at 17:54):

The main result of my thesis is that anything you can define by dependent pattern matching, you can just as well obtain from induction principles plus K (with its reduction rule as given).

Jon Sterling (Jun 28 2021 at 17:55):

Jon Sterling (Jun 28 2021 at 17:57):

I think a valid solution to your question is to just add the additional computation rules that reduce both K and UIP! Obviously there is something to be worked out here in terms of coherence, but I hope you see why I think there isn't really any difference here.

Mike Shulman (Jun 28 2021 at 18:06):

If you reduce K to UIP and also UIP to K, isn't there a circularity problem? Or are you saying to give UIP only the reduction rule that it would have if defined in terms of K without actually defining it that way? (I'm not sure offhand what that rule is.) It seems a little weird to give K two different reduction rules.

Jon Sterling (Jun 28 2021 at 18:10):

Well, we can give a term as many reduction rules as we want... We may run into problems with confluence, but (1) often you can just keep adding rules until it converges, and (2) even lack of confluence does not prevent a computational interpretation that is sound and complete for judgmental equality.

Jon Sterling (Jun 28 2021 at 18:11):

My point here is not to make too precise of technical claims (because I don't have time to check them), but to say that questions like "is there a computational interpretation of Axiom X when there is a computational interpretation of Axiom Y, which is equivalent to X" are very subtle and I have found that the best way to deal with such questions is to explain them away (in a way that respects the principle of equivalence) rather than try to answer them.

Mike Shulman (Jun 28 2021 at 18:11):

Well, maybe there's no formal way to distinguish them, but informally it still feels to me like your "computation rule" for UIP is fundamentally parasitic on K, so that K is the one that "really" has a computational interpretation.

Conor McBride (Jun 28 2021 at 18:12):

UIP' : (X : Set)(x y : X)(q r : I X x y) -> I (I X x y) q r
UIP' X x y q r =
  J X x y q (\ y q -> (r : I X x y) -> I (I X x y) q r)
    (\ r -> K X x r (\ r -> I (I X x x) refl r)
      (refl {- : I (I X x x) refl refl -})
     {- : (r : I X x x) -> I (I X x x) refl r -})
  r

We can check that UIP's pattern matching equation holds definitionally by observing that refl suffices to prove it.

UIP'q : (X : Set)(x : X) ->
  I (I (I X x x) refl refl) (UIP' X x x refl refl) refl
UIP'q X x = refl

K' : (X : Set)(x : X)(q : I X x x) ->
     (P : (q : I X x x) -> Set) ->
     P refl ->
     P q
K' X x q P p = J (I X x x) refl q (UIP X x x refl q) (\ y _ -> P y) p

and moreover, if UIP's pattern matching behaviour holds intensionally, then so does K's:

K'q : (X : Set)(x : X)(q : I X x x) ->
    (P : (q : I X x x) -> Set) ->
    (p : P refl) ->
  I (P refl) (K' X x refl P p) p
K'q X x q P p = refl

The point is that K is a really strong statement about circular paths (corresponding to pattern matching's intuition about covering the constructors), while J is a statement about path-to-somewhere pairs.

Mike Shulman (Jun 28 2021 at 18:17):

@Conor McBride Ah, now I think I see what you're saying: since UIP can also be defined by dependent pattern-matching, it gets a reduction rule from that which is equally computational, and its equivalence to K preserves those computation rules. So I was wrong -- they're both equally instances of dependent pattern matching (in "with-K" style) and hence equally computational. Right?

Conor McBride (Jun 28 2021 at 18:17):

Conor McBride (Jun 28 2021 at 18:21):

Moreover, they're complete. Either gives you enough to do anything you can do with dependent pattern matching.

Leopold Schlicht (Jun 28 2021 at 18:25):

Is there a sense in which the axiom K without its computation rule (that is, UIP) is equivalent to "K + its computation rule"? One cannot say that both yield the same typing judgments, because equality judgments can entail typing judgments, right? (For instance, if

t\equiv t'

and

t\colon A

then

t'\colon A

Conor McBride (Jun 28 2021 at 18:37):

K without its computation rule allows you (especially if you happen to be Matthieu Sozeau) to implement dependent pattern matching in a way that all the pattern matching equations are provable, even though they do not hold judgmentally. However, to recover by proof everything which once held judgmentally requires some additional function extensionality. Nicolas Oury did the spadework on that result.

Observational Type Theory takes this further: you have not only provable UIP but judgmental proof irrelevance for propositions (it's aggressively anti-univalent, as it stands, but rather fun). In OTT, given an axiom K that eliminates over Set but does not compute, you could derive UIP from that K, and then K' as above from UIP...and K' jolly well would compute!

Category Theory
Zulip Server
Archive

Stream: theory: type theory

Topic: K and UIP

Leopold Schlicht (Jun 26 2021 at 13:50):

Mike Shulman (Jun 26 2021 at 15:37):

James Wood (Jun 26 2021 at 15:54):