New notion of equivalence: Bijective relations

[anshwad10]

IMO, cubically this is a very natural notion of equivalence, because from any path p : A ≡ B we get a bijective relation PathP λ i → P i as a primitive notion of cubical. The inverse of a bijective relation is also very easy to define and it is definitionally involutive;
I also prove that this is equivalent to the usual notion of equivalence

[anshwad10]

Now that I gave an explicit construction of EquivIsoBijectiveRel and pathIsoBijectiveRel I think I could actually use these to get better definitions of invEquiv and pathToEquiv

[anshwad10]

So I tried it and it's not that much better. For pathToEquiv I think going through isoToEquiv is then the simplest solution which computes decently. For invEquiv I didn't notice that much of a difference (in terms of complexity of normal forms) between the one going through Iso and the one going through BijectiveRel, so I don't think it's worth bothering with that

[anshwad10]

@ecavallo this is ready to merge, please review

[maxsnew]

Do we really need all of this duplication of singlP?

[anshwad10]

I needed contrSinglP' to define isBijectivePathP; I could instead define contrSinglP' by transporting the proof of contrSinglP but I don't think there is a way to do that which computes as nicely?

[maxsnew]

It can't be defined as singlP (\i -> A (~ i))?

[anshwad10]

PathP (\i -> A (~ i)) a x is not definitionally identical to PathP A x a. Although they are definitionally isomorphic, if I used isContrRetract to transport contrSinglP along that isomorphism it wouldn't reduce as nicely (because isContrRetract can't rely on retraction being definitional, so it must adjust by the path even though it is reflexivity). I guess another solution could be to have a version of isOfHLevelRespectEquiv for strict iso's, but thay would need either reflection or the 2LTT strict equality (maybe I should add it in another PR? that might actually also actually simplify the proof of isFunctionalCompRel and isCofunctionalCompRel)

[maxsnew]

Why would it need reflection? In cubical-categorical-logic when we need to abstract over a definitional equality we use the inductive Data.Equality type and then only use the construction when it is Eq.refl.

[anshwad10]

oh yeah I didn't think of that! for some reason I had assumed that we would need the 2LTT strict equality, but I forgot that the inductive equality works just as well.
... Does this mean that Cubical.Reflection.StrictEquiv does not actually need reflection either?

[maxsnew]

The reflection there is still helpful, it's just to allow for an abbreviation of writing an equivalence that is strict without manually invoking strictContrFibers.