1005 wants to remove the swan identity type because Agda.Builtin.Equality now has the same computational behavior. This pull request extends the Cubical.Data.Equality module, which contains some basic results for this equality type. The main changes are the following.
A proof of univalence which is behaves like "Book HoTT", that is, pr₁ (idToEquiv p) x = transport id p x holds, where transport is defined in terms of pattern matching. Thus, the function which is an equivalence is the same one as in the book (see Lemma 2.10.1 and Axiom 2.10.3).
The interface for S¹ is extended with the eliminator and its corresponding β and η rules.
A more general result (similar to the one here) is proven, which simplifies lifting HITs to the inductively defined equality type.
1005 wants to remove the swan identity type because
Agda.Builtin.Equalitynow has the same computational behavior. This pull request extends theCubical.Data.Equalitymodule, which contains some basic results for this equality type. The main changes are the following.pr₁ (idToEquiv p) x = transport id p xholds, wheretransportis defined in terms of pattern matching. Thus, the function which is an equivalence is the same one as in the book (see Lemma 2.10.1 and Axiom 2.10.3).S¹is extended with the eliminator and its corresponding β and η rules.