From 129eef115035373ec57f9cadbc6b99ac60b28447 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 24 Apr 2018 14:11:22 +0200 Subject: [PATCH] Finish section on category of sets --- doc/feedback.txt | 72 +++++++++++++++++ doc/implementation.tex | 169 +++++++++++++++++++++++++++++++++------ doc/introduction.tex | 35 ++++---- doc/macros.tex | 6 ++ doc/main.tex | 4 +- src/Cat/Equivalence.agda | 50 +++++------- src/Cat/Prelude.agda | 4 +- 7 files changed, 265 insertions(+), 75 deletions(-) create mode 100644 doc/feedback.txt diff --git a/doc/feedback.txt b/doc/feedback.txt new file mode 100644 index 0000000..e45ae95 --- /dev/null +++ b/doc/feedback.txt @@ -0,0 +1,72 @@ +Andrea Vezzosi Tue, Apr 24, 2018 at 2:02 PM +To: Frederik Hanghøj Iversen +Cc: Thierry Coquand +On Tue, Apr 24, 2018 at 12:57 PM, Frederik Hanghøj Iversen + 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] diff --git a/doc/implementation.tex b/doc/implementation.tex index 6ff388b..02ca940 100644 --- a/doc/implementation.tex +++ b/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 -a bit fun, should I include it?) +curious reader can check the implementation for the details. \TODO{The proof is +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 \equiv B) & \simeq (\fst A \simeq \fst B) \\ - (A \simeq B) & \simeq ((A, s_A) \approxeq (B, s_B)) +((A, s_A) \equiv (B, s_B)) + & \simeq (A \equiv B) && \ref{eq:equivPropSig} \\ + & \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} diff --git a/doc/introduction.tex b/doc/introduction.tex index 3153e83..08fde09 100644 --- a/doc/introduction.tex +++ b/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 -propositions-as-types interpretation of type theory $\top$ is the proposition -that is always true. The type $A \x \top$ and $A$ has an element for each $a : -A$. So in a sense they are the same. The second element of the pair does not add -any ``interesting information''. It can be useful to identify such types. In -fact, it is quite commonplace in mathematics. Say we look at a set $\{x \mid +Let $\top$ denote the unit type -- a type with a single constructor. In +the propositions-as-types interpretation of type theory $\top$ is the +proposition that is always true. The type $A \x \top$ and $A$ has an element for +each $a : A$. So in a sense they are the same. The second element of the pair +does not add any ``interesting information''. It can be useful to identify such +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 -(A \simeq B) \to (A \equiv B)$ and vice-versa. +In particular this allows us to construct an equality from an equivalence +($\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 -prove more things and to reuse proofs. + +The contribution of this thesis is to explore how working in a cubical setting +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 diff --git a/doc/macros.tex b/doc/macros.tex index 33f09d2..6a2a0ee 100644 --- a/doc/macros.tex +++ b/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}} diff --git a/doc/main.tex b/doc/main.tex index cf00dc9..bae31dd 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -26,8 +26,8 @@ \bibliographystyle{plainnat} \nocite{cubical-demo} \nocite{coquand-2013} -%% \bibliography{refs} -%% \begin{appendices} +\bibliography{refs} +\begin{appendices} %% \input{planning.tex} %% \input{halftime.tex} \end{appendices} diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index 6c96f1b..cc8870c 100644 --- a/src/Cat/Equivalence.agda +++ b/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,11 +165,12 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where propIso : iso-x ≡ iso-y propIso i = fx≡fy i , inx≡iny i - inverse-to-from-iso : (toIso {f} ∘ fromIso {f}) iso ≡ iso - inverse-to-from-iso = begin - (toIso ∘ fromIso) iso ≡⟨⟩ - toIso (fromIso iso) ≡⟨ propIso _ _ ⟩ - iso ∎ + module _ (iso : Isomorphism f) where + inverse-to-from-iso : (toIso {f} ∘ fromIso {f}) iso ≡ iso + inverse-to-from-iso = begin + (toIso ∘ fromIso) iso ≡⟨⟩ + toIso (fromIso iso) ≡⟨ propIso _ _ ⟩ + iso ∎ fromIsomorphism : A ≅ B → A ~ B fromIsomorphism (f , iso) = f , 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 - where - k : Isomorphism _ - k = toIso _ _ (snd (eA a)) - open Σ k renaming (fst to g') + g (a , qA) = a , fst (snd P≅Q) qA 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) - k : Isomorphism _ - k = toIso _ _ (snd (eA a)) - open Σ k renaming (fst to g' ; snd to inv) + open Σ (snd P≅Q) 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 diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index 0c0bec0..71e5cbd 100644 --- a/src/Cat/Prelude.agda +++ b/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 ])