Finish section on category of sets

doc/feedback.txt

@@ -0,0 +1,72 @@
+Andrea Vezzosi <vezzosi@chalmers.se>	Tue, Apr 24, 2018 at 2:02 PM
+To: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
+Cc: Thierry Coquand <coquand@chalmers.se>
+On Tue, Apr 24, 2018 at 12:57 PM, Frederik Hanghøj Iversen
+<fhi.1990@gmail.com> wrote:
+> I've written the first few sections about my implementation. I was wondering
+> if you could have a quick look at it. You don't need to read it
+> word-for-word but I would like some indication from you if this is the sort
+> of thing you would like to see in the final report.
+
+Yes! I would say this very much fits the bill of what the main part of
+the report should be, then you could have a discussion section where
+you might put some analysis of the pros and cons of cubical, design
+choices you made, and your experience overall.
+
+I wonder if there should be some short introduction to Cubical Type
+Theory before this chapter, so you can introduce the Path type by
+itself and show some simple proof with it. e.g. how to get function
+extensionality.
+
+You mention a few "combinators" like propPi and lemPropF, you might
+want to call them just lemmas, so it's clearer that these can be
+proven in --cubical.
+
+>
+> I refer you specifically to "Chapter 2 - Implementation" on p. 6.
+>
+> In this chapter I plan to additionally include some text about the proof we
+> did that products are mere propositions and the proof about the two
+> equivalent notions of a monad.
+
+I've read the chapter up until 2.3 and skimmed the rest for now, but I
+accumulated some editing suggestions I copy here.
+Remember to look for things like these when you proof-read the rest :)
+
+
+You should be careful to properly introduce things before you use
+them, like IsPreCategory (I'd prefer if it took the raw category as
+argument btw) and its fields isIdentity, isAssociative, .. come up a
+bit out of the blue from the end of page 8.
+Maybe the easiest is to show the definition of IsPreCategory.
+
+Maybe give a type for propIsIdentity and mention the other prop* are similar.
+
+Also the notation "isIdentity_a" to apply projections is a bit unusual
+so it needs to be introduced as well.
+To be fair it would be simpler to stick to function application
+(though I see that it would introduce more parentheses),
+
+"The situation is a bit more complicated when we have a dependent
+type" could be more clear by being more specific:
+"The situation is a bit more complicated when the type of a field
+depends on a previous field"
+
+Here too it might be more concrete if you also give the code for IsCategory.
+
+In Path ( λ i → Univalent_{p i} ) isPreCategory_a isPreCategory_b
+I suggest parentheses around (p i), but also you should be consistent
+on whether you want to call the proof "p" or "p_{isPreCategory}",
+finally i'm guessing the two fields should be "isUnivalent" rather
+than "isPreCategory".
+
+You can cite the book on the specific definition of isEquiv,
+"contractible fibers" in section 4.4, the grad lemma is also from
+somewhere but I don't remember off-hand.
+
+You have not defined what you mean by _\~=_ and isomorphism.
+
+
+Cheers,
+Andrea
+[Quoted text hidden]

doc/implementation.tex

@@ -189,7 +189,7 @@ $$
 and one heterogeneous:
 %
 $$
-Path\ (\lambda i \to Univalent_{p\ i})\ \isPreCategory_a\ \isPreCategory_b
+\Path\ (\lambda\; i \mto Univalent_{p\ i})\ \isPreCategory_a\ \isPreCategory_b
 $$
 %
 Which depends on the choice of $p_{\isPreCategory}$. The first of these we can
@@ -203,7 +203,7 @@ path between some two elements in $A$; $p : a_0 \equiv a_1$ then we can built a
 heterogeneous path between any two $b$'s at the endpoints:
 %
 $$
-Path\ (\lambda i \to B\ (p\ i))\ b0\ b1
+\Path\ (\lambda\; i \mto B\ (p\ i))\ b0\ b1
 $$
 %
 where $b_0 \tp B a_0$ and $b_1 \tp B\ a_1$. This is quite a mouthful, but the
@@ -216,7 +216,7 @@ applying using congruence of paths: $\congruence\ \mathit{isIdentity}\
 p_{\isPreCategory}$
 
 When we have a proper category we can make precise the notion of ``identifying
-isomorphic types'' (TODO cite awodey here). That is, we can construct the
+isomorphic types'' \TODO{cite awodey here}. That is, we can construct the
 function:
 %
 $$
@@ -227,11 +227,11 @@ One application of this, and a perhaps somewhat surprising result, is that
 terminal objects are propositional. Intuitively; they do not have any
 interesting structure. The proof of this follows from the usual observation that
 any two terminal objects are isomorphic. The proof is omitted here, but the
-curious reader can check the implementation for the details. (TODO: The proof is
+curious reader can check the implementation for the details. \TODO{The proof is
-a bit fun, should I include it?)
+a bit fun, should I include it?}
 
 \section{Equivalences}
-\label{equiv}
+\label{sec:equiv}
 The usual notion of a function $f : A \to B$ having an inverses is:
 %
 $$
@@ -253,7 +253,7 @@ what an equivalence $\isEquiv : (A \to B) \to \MCU$ must supply:
 %
 Having such an interface gives us both 1) a way to think rather abstractly about
 how to work with equivalences and 2) to use ad-hoc definitions of equivalences.
-The specific instantiation of $\isEquiv$ as defined in \cite{cubical} is:
+The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is:
 %
 $$
 isEquiv\ f \defeq \prod_{b : B} \isContr\ (\fiber\ f\ b)
@@ -269,7 +269,7 @@ once we have shown that this definition actually works as an equivalence.
 
 The first function from the list of requirements we will call
 $\mathit{fromIsomorphism}$, this is known as $\mathit{gradLemma}$ in
-\cite{cubical} the second one we will refer to as $\mathit{toIsmorphism}$. It's
+\cite{cubical-agda} the second one we will refer to as $\mathit{toIsmorphism}$. It's
 implementation can be found in the sources. Likewise the proof that this
 equivalence is propositional can be found in my implementation.
 
@@ -353,7 +353,7 @@ $$
 \isoToId \tp A \approxeq B \to A \equiv B
 $$
 %
-The next few theorems are variations on theorem 9.1.9 from \cite{HoTT-book}. Let
+The next few theorems are variations on theorem 9.1.9 from \cite{hott-2013}. Let
 an isomorphism $A \approxeq B$ in some category $\bC$ be given. Name the
 isomorphism $\iota \tp A \to B$ and its inverse $\widetilde{\iota} \tp B \to A$.
 Since $\bC$ is a category (and therefore univalent) the isomorphism induces a
@@ -425,7 +425,7 @@ univalence in a very simple category where the structure of the category is
 rather simple.
 
 Let $\bC$ be some category, we then define the opposite category
-$\bC^{\matit{Op}}$. It has the same objects, but the type of arrows are flipped,
+$\bC^{\mathit{Op}}$. It has the same objects, but the type of arrows are flipped,
 that is to say an arrow from $A$ to $B$ in the opposite category corresponds to
 an arrow from $B$ to $A$ in the underlying category. The identity arrow is the
 same as the one in the underlying category (they have the same type). Function
@@ -442,7 +442,7 @@ Since $\rrr$ is reverse function composition this is just the symmetric version
 of associativity.
 %
 $$
-\matit{identity} \rrr f \equiv f \x f \rrr identity \equiv f
+\mathit{identity} \rrr f \equiv f \x f \rrr identity \equiv f
 $$
 %
 This is just the swapped version of identity.
@@ -452,7 +452,7 @@ arguments. Or in other words since $\Hom_{A\ B}$ is a set for all $A\ B \tp
 \Object$ then so is $\Hom_{B\ A}$.
 
 Now, to show that this category is univalent is not as straight-forward. Lucliy
-section \ref{equiv} gave us some tools to work with equivalences. We saw that we
+section \ref{sec:equiv} gave us some tools to work with equivalences. We saw that we
 can prove this category univalent by giving an inverse to
 $\idToIso_{\mathit{Op}} \tp (A \equiv B) \to (A \approxeq_{\mathit{Op}} B)$.
 From the original category we have that $\idToIso \tp (A \equiv B) \to (A \cong
@@ -500,7 +500,7 @@ This finished the proof that the opposite category is in fact a category. Now,
 to prove that that opposite-of is an involution we must show:
 %
 $$
-\prod_{\bC \tp \mathit{Category}} \left(\bC^{\matit{Op}}\right)^{\matit{Op}} \equiv \bC
+\prod_{\bC \tp \mathit{Category}} \left(\bC^{\mathit{Op}}\right)^{\mathit{Op}} \equiv \bC
 $$
 %
 As we've seen the laws in $\left(\bC^{\mathit{Op}}\right)^{\mathit{Op}}$ get
@@ -543,20 +543,23 @@ $$
 %
 Which, as we saw in section \ref{univalence}, is sufficient to show that the
 category is univalent. The way that I have shown this is with a three-step
-process. For objects $(A, s_A)\; (B, s_B) \tp \Set$ I show that.
+process. For objects $(A, s_A)\; (B, s_B) \tp \Set$ I show the following chain
+of equivalences:
 %
 \begin{align*}
- ((A, s_A) \equiv (B, s_B)) & \simeq (A \equiv B) \\
+((A, s_A) \equiv (B, s_B))
- (A \equiv B) & \simeq (\fst A \simeq \fst B) \\
+ & \simeq (A \equiv B) && \ref{eq:equivPropSig} \\
- (A \simeq B) & \simeq ((A, s_A) \approxeq (B, s_B))
+ & \simeq (A \simeq B) && \text{Univalence} \\
+ & \simeq ((A, s_A) \approxeq (B, s_B)) && \text{\ref{eq:equivSig} and \ref{eq:equivIso}}
 \end{align*}
 
 And since $\simeq$ is an equivalence relation we can chain these equivalences
 together. Step one will be proven with the following lemma:
 %
-$$
+\begin{align}
+  \label{eq:equivPropSig}
 \left(\prod_{a \tp A} \isProp (P\ a)\right) \to \prod_{x\;y \tp \sum_{a \tp A} P\ a} (x \equiv y) \simeq (\fst\ x \equiv \fst\ y)
-$$
+\end{align}
 %
 The lemma states that for pairs whose second component are mere propositions
 equiality is equivalent to equality of the first components. In this case the
@@ -564,21 +567,105 @@ type-family $P$ is $\isSet$ which itself is a proposition for any type $A \tp
 \Type$. Step two is univalence. Step three will be proven with the following
 lemma:
 %
-$$
+\begin{align}
+  \label{eq:equivSig}
 \prod_{a \tp A} \left( P\ a \simeq Q\ a \right) \to \sum_{a \tp A} P\ a \simeq \sum_{a \tp A} Q\ a
-$$
+\end{align}
 %
 Which says that if two type-families are equivalent at all points, then pairs
 with identitical first components and these families as second components will
 also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq
 \mathit{Isomorphism}$. So we must finally prove:
 %
-$$
+\begin{align}
+  \label{eq:equivIso}
 \prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \mathit{Isomorphism}\ f \right)
-$$
+\end{align}
 
+First, lets proove \ref{eq:equivPropSig}: Let $propP \tp \prod_{a \tp A} \isProp (P\ a)$ and $x\;y \tp \sum_{a \tp A} P\ a$ be given. Because
+of $\mathit{fromIsomorphism}$ it suffices to give an isomorphism between
+$x \equiv y$ and $\fst\ x \equiv \fst\ y$:
+%
+\begin{align*}
+  f & \defeq \congruence\ \fst \tp x \equiv y \to \fst\ x \equiv \fst\ y \\
+  g & \defeq \mathit{lemSig}\ \mathit{propP}\ x\ y \tp \fst\ x \equiv \fst\ y \to x \equiv y
+\end{align*}
+%
+\TODO{Is it confusing that I use point-free style here?}
+Here $\mathit{lemSig}$ is a lemma that says that if the second component of a
+pair is a proposition, it suffices to give a path between it's first components
+to construct an equality of the two pairs:
+%
+\begin{align*}
+\mathit{lemSig} \tp \left( \prod_{x \tp A} \isProp\ (B\ x) \right) \to
+\prod_{u\; v \tp \sum_{a \tp A} B\ a}
+  \left( \fst\ u \equiv \fst\ v \right) \to u \equiv v
+\end{align*}
+%
+The proof that these are indeed inverses has been omitted. \TODO{Do I really
+  want to ommit it?}\QED
 
-\subsection{Categories}
+Now to prove \ref{eq:equivSig}: Let $e \tp \prod_{a \tp A} \left( P\ a \simeq
+Q\ a \right)$ be given. To prove the equivalence, it suffices to give an
+isomorphism between $\sum_{a \tp A} P\ a$ and $\sum_{a \tp A} Q\ a$, but since
+they have identical first components it suffices to give an isomorphism between
+$P\ a$ and $Q\ a$ for all $a \tp A$. This is exactly what we can get from
+the equivalence $e$.\QED
+
+Lastly we prove \ref{eq:equivIso}. Let $f \tp A \to B$ be given. For the maps we
+choose:
+%
+\begin{align*}
+\mathit{toIso}
+  & \tp \isEquiv\ f             \to \mathit{Isomorphism}\ f \\
+\mathit{fromIso}
+  & \tp \mathit{Isomorphism}\ f \to \isEquiv\ f
+\end{align*}
+%
+As mentioned in section \ref{sec:equiv}. These maps are not in general inverses
+of each other. In stead, we will use the fact that $A$ and $B$ are sets. The first thing we must prove is:
+%
+\begin{align*}
+  \mathit{fromIso} \comp \mathit{toIso} \equiv \identity_{\isEquiv\ f}
+\end{align*}
+%
+For this we can use the fact that being-an-equivalence is a mere proposition.
+For the other direction:
+%
+\begin{align*}
+  \mathit{toIso} \comp \mathit{fromIso} \equiv \identity_{\mathit{Isomorphism}\ f}
+\end{align*}
+%
+We will show that $\mathit{Isomorphism}\ f$ is also a mere proposition. To this
+end, let $X\;Y \tp \mathit{Isomorphism}\ f$ be given. Name the maps $x\;y \tp B
+\to A$ respectively. Now, the proof that $X$ and $Y$ are the same is a pair of
+paths: $p \tp x \equiv y$ and $\Path\ (\lambda\; i \mto
+\mathit{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where $\mathcal{X}$
+and $\mathcal{Y}$ denotes the witnesses that $x$ (respectively $y$) is an
+inverse to $f$. $p$ is inhabited by:
+%
+\begin{align*}
+  x
+  & \equiv x \comp \identity \\
+  & \equiv x \comp (f \comp y)
+  && \text{$y$ is an inverse to $f$} \\
+  & \equiv (x \comp f) \comp y \\
+  & \equiv \identity \comp y
+  && \text{$x$ is an inverse to $f$} \\
+  & \equiv y
+\end{align*}
+%
+For the other (dependent) path we can prove that being-an-inverse-of is a
+proposition and then use $\lemPropF$. So we prove the generalization:
+%
+\begin{align*}
+\prod_{g : B \to A} \isProp\ (\mathit{AreInverses}\ f\ g)
+\end{align*}
+%
+But $\mathit{AreInverses}\ f\ g$ is a pair of equations on arrows, so we use
+$\propSig$ and the fact that both $A$ and $B$ are sets to close this proof.
+
+\subsection{Category of categories}
 Note that this category does in fact not exist. In stead I provide the
 definition of the ``raw'' category as well as some of the laws.
 
@@ -589,8 +676,40 @@ These lemmas can be used to provide the actual exponential object in a context
 where we have a witness to this being a category. This is useful if this library
 is later extended to talk about higher categories.
 
-
 \section{Product}
+In the following I'll demonstrate a technique for using categories to prove
+properties. The goal in this section is to show that products are propositions:
+%
+$$
+\prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\mathit{Product}\ \bC\ A\ B)
+$$
+%
+Where $\mathit{Product}\ \bC\ A\ B$ denotes the type of products of objects $A$
+and $B$ in the category $\bC$. I do this by constructing a category whose
+terminal objects are equivalent to products in $\bC$, and since terminal objects
+are propositional in a proper category and equivalences preservehomotopy level,
+then we know that products also are propositions. But before we get to that,
+let's recall the definition of products.
+
+Given a category $\bC$ and two objects $A$ and $B$ in $bC$ we define the product
+of $A$ and $B$ to be an object $A \x B$ in $\bC$ and two arrows $\pi_1 \tp A \x
+B \to A$ and $\pi_2 \tp A \x B \to B$ called the projections of the product. The projections must satisfy the following property:
+
+For all $X \tp Object$, $f \tp \Arrow\ X\ A$ and $g \tp \Arrow\ X\ B$ we have
+that there exists a unique arrow $\pi \tp \Arrow\ X\ (A \x B)$ satisfying
+%
+\begin{align}
+\label{eq:umpProduct}
+%% \prod_{X \tp Object} \prod_{f \tp \Arrow\ X\ A} \prod_{g \tp \Arrow\ X\ B}\\
+%% \uexists_{f \x g \tp \Arrow\ X\ (A \x B)}
+\pi_1 \lll \pi \equiv f \x \pi_2 \lll \pi \equiv g
+%% ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ])
+%%           → ∃![ f×g ] (ℂ [ fst ∘ f×g ] ≡ f P.× ℂ [ snd ∘ f×g ] ≡ g)
+\end{align*}
+$
+$\pi$ is called the product (arrow) of $f$ and $g$.
+
+
 \section{Monads}
 
 %% \subsubsection{Functors}

doc/introduction.tex

@@ -73,12 +73,13 @@ the (left) identity law of the underlying category to proove $\idFun \comp g
 %
 \subsection{Equality of isomorphic types}
 %
-Let $\top$ denote the unit type -- a type with a single constructor. In the
+Let $\top$ denote the unit type -- a type with a single constructor. In
-propositions-as-types interpretation of type theory $\top$ is the proposition
+the propositions-as-types interpretation of type theory $\top$ is the
-that is always true. The type $A \x \top$ and $A$ has an element for each $a :
+proposition that is always true. The type $A \x \top$ and $A$ has an element for
-A$. So in a sense they are the same. The second element of the pair does not add
+each $a : A$. So in a sense they are the same. The second element of the pair
-any ``interesting information''. It can be useful to identify such types. In
+does not add any ``interesting information''. It can be useful to identify such
-fact, it is quite commonplace in mathematics. Say we look at a set $\{x \mid
+types. In fact, it is quite commonplace in mathematics. Say we look at a set
+$\{x \mid
 \phi\ x \land \psi\ x\}$ and somehow conclude that $\psi\ x \equiv \top$ for all
 $x$. A mathematician would immediately conclude $\{x \mid \phi\ x \land
 \psi\ x\} \equiv \{x \mid \phi\ x\}$ without thinking twice. Unfortunately such
@@ -92,8 +93,9 @@ types. The principle of univalence says that:
 %
 $$\mathit{univalence} \tp (A \simeq B) \simeq (A \equiv B)$$
 %
-In particular this allows us to construct an equality from an equivalence $\mathit{ua} \tp
+In particular this allows us to construct an equality from an equivalence
-(A \simeq B) \to (A \equiv B)$ and vice-versa.
+($\mathit{ua} \tp (A \simeq B) \to (A \equiv B)$) and vice-versa.
+
 \section{Formalizing Category Theory}
 %
 The above examples serve to illustrate the limitation of Agda. One case where
@@ -115,20 +117,21 @@ Inspiration:
 \end{verbatim}
 The idea of formalizing Category Theory in proof assistants is not new. There
 are a multitude of these available online. Just as first reference see this
-question on Math Overflow: \cite{mo-formalizations}. Notably these two implementations of category theory in Agda:
+question on Math Overflow: \cite{mo-formalizations}. Notably these
+implementations of category theory in Agda:
 \begin{itemize}
 \item
-\url{https://github.com/copumpkin/categories} - setoid interpretation
+\url{https://github.com/copumpkin/categories} -- setoid interpretation
 \item
-\url{https://github.com/pcapriotti/agda-categories} - homotopic setting with postulates
+\url{https://github.com/pcapriotti/agda-categories} -- homotopic setting with postulates
 \item
-\url{https://github.com/pcapriotti/agda-categories} - homotopic setting in coq
+\url{https://github.com/pcapriotti/agda-categories} -- homotopic setting in coq
 \item
-\url{https://github.com/mortberg/cubicaltt} - homotopic setting in \texttt{cubicaltt}
+\url{https://github.com/mortberg/cubicaltt} -- homotopic setting in \texttt{cubicaltt}
 \end{itemize}
-The contribution of this
+
-thesis is to explore how working in a cubical setting will make it possible to
+The contribution of this thesis is to explore how working in a cubical setting
-prove more things and to reuse proofs.
+will make it possible to prove more things and to reuse proofs.
 
 There are alternative approaches to working in a cubical setting where one can
 still have univalence and functional extensionality. One option is to postulate

doc/macros.tex

@@ -59,3 +59,9 @@
 \newcommand\rrr{\ggg}
 \newcommand\fst{\mathit{fst}}
 \newcommand\snd{\mathit{snd}}
+\newcommand\Path{\mathit{Path}}
+\newcommand\Category{\mathit{Category}}
+\newcommand\TODO[1]{TODO: \emph{#1}}
+\newcommand*{\QED}{\hfill\ensuremath{\square}}%
+\newcommand\uexists{\exists!}
+\newcommand\Arrow{\mathit{Arrow}}

doc/main.tex

@@ -26,8 +26,8 @@
 \bibliographystyle{plainnat}
 \nocite{cubical-demo}
 \nocite{coquand-2013}
-%% \bibliography{refs}
+\bibliography{refs}
-%% \begin{appendices}
+\begin{appendices}
 %% \input{planning.tex}
 %% \input{halftime.tex}
 \end{appendices}

src/Cat/Equivalence.agda

@@ -10,7 +10,7 @@ open import Cubical.GradLemma hiding (isoToPath)
 open import Cat.Prelude using
   ( lemPropF ; setPi ; lemSig ; propSet
   ; Preorder ; equalityIsEquivalence ; propSig ; id-coe
-  ; Setoid )
+  ; Setoid ; _$_ ; propPi )
 
 import Cubical.Univalence as U
 
@@ -133,7 +133,7 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where
     -- | The other inverse law does not hold in general, it does hold, however,
     -- | if `A` and `B` are sets.
     module _ (sA : isSet A) (sB : isSet B) where
-      module _ {f : A → B} (iso : Isomorphism f) where
+      module _ {f : A → B} where
         module _ (iso-x iso-y : Isomorphism f) where
           open Σ iso-x renaming (fst to x ; snd to inv-x)
           open Σ iso-y renaming (fst to y ; snd to inv-y)
@@ -146,22 +146,18 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where
             y ∎
 
           propInv : ∀ g → isProp (AreInverses f g)
-          propInv g t u i = a i , b i
+          propInv g t u = λ i → a i , b i
             where
             a : (fst t) ≡ (fst u)
-            a i = h
+            a i = funExt hh
               where
               hh : ∀ a → (g ∘ f) a ≡ a
               hh a = sA ((g ∘ f) a) a (λ i → (fst t) i a) (λ i → (fst u) i a) i
-              h : g ∘ f ≡ idFun A
-              h i a = hh a i
             b : (snd t) ≡ (snd u)
-            b i = h
+            b i = funExt hh
               where
               hh : ∀ b → (f ∘ g) b ≡ b
               hh b = sB _ _ (λ i → snd t i b) (λ i → snd u i b) i
-              h : f ∘ g ≡ idFun B
-              h i b = hh b i
 
           inx≡iny : (λ i → AreInverses f (fx≡fy i)) [ inv-x ≡ inv-y ]
           inx≡iny = lemPropF propInv fx≡fy
@@ -169,6 +165,7 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where
           propIso : iso-x ≡ iso-y
           propIso i = fx≡fy i , inx≡iny i
 
+        module _ (iso : Isomorphism f) where
           inverse-to-from-iso : (toIso {f} ∘ fromIso {f}) iso ≡ iso
           inverse-to-from-iso = begin
             (toIso ∘ fromIso) iso ≡⟨⟩
@@ -419,7 +416,7 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
   equivPropSig pA p q = fromIsomorphism _ _ iso
     where
     f : ∀ {p q} → p ≡ q → fst p ≡ fst q
-    f e i = fst (e i)
+    f = cong fst
     g : ∀ {p q} → fst p ≡ fst q → p ≡ q
     g {p} {q} = lemSig pA p q
     ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e
@@ -507,31 +504,26 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
     → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q
   equivSig {Q = Q} eA = res
     where
+    P≅Q : ∀ {a} → P a ≅ Q a
+    P≅Q {a} = toIsomorphism _ _ (eA a)
     f : Σ A P → Σ A Q
-    f (a , pA) = a , fst (eA a) pA
+    f (a , pA) = a , fst P≅Q pA
     g : Σ A Q → Σ A P
-    g (a , qA) = a , g' qA
+    g (a , qA) = a , fst (snd P≅Q) qA
-      where
-      k : Isomorphism _
-      k = toIso _ _ (snd (eA a))
-      open Σ k renaming (fst to g')
     ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
-    ve-re x i = fst x , eq i
+    ve-re (a , pA) i = a , eq i
       where
-      eq : snd ((g ∘ f) x) ≡ snd x
+      eq : snd ((g ∘ f) (a , pA)) ≡ pA
       eq = begin
-        snd ((g ∘ f) x) ≡⟨⟩
+        snd ((g ∘ f) (a , pA)) ≡⟨⟩
         snd (g (f (a , pA))) ≡⟨⟩
         g' (fst (eA a) pA) ≡⟨ lem ⟩
         pA ∎
         where
-        open Σ x renaming (fst to a ; snd to pA)
+        open Σ (snd P≅Q) renaming (fst to g' ; snd to inv)
-        k : Isomorphism _
-        k = toIso _ _ (snd (eA a))
-        open Σ k renaming (fst to g' ; snd to inv)
         -- anti-funExt
         lem : (g' ∘ (fst (eA a))) pA ≡ pA
-        lem i = fst inv i pA
+        lem = cong (_$ pA) (fst (snd (snd P≅Q)))
     re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
     re-ve x i = fst x , eq i
       where

src/Cat/Prelude.agda

@@ -62,10 +62,8 @@ module _ (ℓ : Level) where
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
 module _ {ℓa ℓb} {A : Set ℓa} {P : A → Set ℓb} (f g : ∃! P) where
-  open Σ (snd f) renaming (snd to u)
-
   ∃-unique : fst f ≡ fst g
-  ∃-unique = u (fst (snd g))
+  ∃-unique = (snd (snd f)) (fst (snd g))
 
 module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
   (fst≡ : (λ _ → A)            [ fst a ≡ fst b ])