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