Fundamental theorem of identity types

[felixwellen]

A basic characterization of the identity type. This can be used to compute identity types.

[mortberg]

Nice! I seem to recall that Egbert used this theorem to derive Omega(S1) = Z. Would such a proof be substantially different in any way or is it just a refactoring?

[felixwellen]

I guess there will be no substantial difference. The theorem is also not so far from encode-decode, but I haven't thought about the exact relation (to which version...) for some time. For me, the fundamental theorem is just easier to remember/think about because it looks more like a universal property.

[mortberg]

I guess there will be no substantial difference. The theorem is also not so far from encode-decode, but I haven't thought about the exact relation (to which version...) for some time. For me, the fundamental theorem is just easier to remember/think about because it looks more like a universal property.

Right, I guess what I'm really asking is exactly how it relates to encode-decode.

[felixwellen]

Ok, let's say we fix x:A then code(y) should certainly be Eq(x,y). The map
encode : (y:A) -> x=y -> code(y)
should be given by
encode(relf) := reflEq x : code(x)=Eq(x,x)
(assuming with have this ingredient of the fundamental theorem).
And decode : (y : A) -> code(y) -> x = y we can define by projecting from the contractibilty proof for Sigma(y:A) Eq(x,y) (the second ingredient of the theorem).
Now, if you unpack the contractability of Sigma(y:A) Eq(x,y), that means

• there is a center, but that's just given by relfEq x
• any other thing in the sigma-type is equal to that, which can be rewritten as:
  transport in Eq(x,_) (along some p:x==y) (some q : Eq(x,y)) == (x,reflEq x)
  So p is decode y q and then (without thinking through all details) this looks like Lemma 8.9.1 in the HoTT-Book.

[mortberg]

Hmm, can't one prove that this is an equivalence directly? I feel like it might be easier, but I might be wrong in which case this proof is fine...

[felixwellen]

I made a direct proof. It avoids isoToEquiv, but it doesn't look better. But that might be due to me avoiding cubical primitives...

[ecavallo]

Note there is also a isContr→Equiv in Foundations.Equiv.

[felixwellen]

Yes, but I thought that might be a bit awkward to use to show, that some particular function is an equivalence.

[felixwellen]

But I guess my proof would look nicer, if I use that.

[felixwellen]

Ok, it does look better.

[mortberg]

Yeah, that looks good!

[mortberg]

Ok, let's say we fix x:A then code(y) should certainly be Eq(x,y). The map encode : (y:A) -> x=y -> code(y) should be given by encode(relf) := reflEq x : code(x)=Eq(x,x) (assuming with have this ingredient of the fundamental theorem). And decode : (y : A) -> code(y) -> x = y we can define by projecting from the contractibilty proof for Sigma(y:A) Eq(x,y) (the second ingredient of the theorem). Now, if you unpack the contractability of Sigma(y:A) Eq(x,y), that means

* there is a center, but that's just given by `relfEq x`

* any other thing in the sigma-type is equal to that, which can be rewritten as:
  `transport in Eq(x,_) (along some p:x==y) (some q : Eq(x,y)) == (x,reflEq x)`
  So `p` is `decode y q` and then (without thinking through all details) this looks like Lemma 8.9.1 in the HoTT-Book.

Thanks! This was helpful :-)

I would be happy to merge this once the question about this one proof has been answered