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?