Can we use the internal logic of a category to do diagram chases "as in $\mathbf{Ab}$" ?

Question

Disclaimer: I'm not yet really comfortable with internal logics, though I know the basics, so the best answer would not be the most technical one.

Suppose you want to prove a diagram lemma (say the snake lemma for instance) in an arbitrary abelian category. As many authors show, one can do this in a purely "categorical way", obviously elements-free. I believe there's a proof in McLane for instance.

You can also use Mitchell's embedding theorem: as the diagram is a small one, the abelian category generated by it is small as well (it can be built in $\omega$ steps), and one can then fully, faithfully, exactly embed it in a category of $R$-modules for some module $R$ , and use the lemma in question in this category (to get the connecting morphism for instance, in the snake lemma), and then go back up to your category, and the properties of the embedding imply what you want.

Of course in categories of $R$-modules, you're allowed to reason like "let $x$ be such that $f(x)=0$. Then $x\in Ker(f)= Im(g)$ so there is $y$ such that blabla", which makes the proofs (usually) somewhat easier.

My question is whether one can use the internal logic of the category to reason exactly as in the $R$-module case, as long as we don't go beyond the logic that we have at hand. For instance, regular logic has an existential quantifier, and so perhaps $f(x)=0\vdash_x \exists y, g(y) = x$ is valid in an abelian category where we have an exact sequence $A\to B \to C$ (that's one part I'm unsure about) and perhaps we could reason as usual (though with a "restricted" logic) to prove some results about arbitrary abelian categories. Is it the case ? Is there a way to use the internal logic to build the connecting morphism in the snake lemma for instance ?

For another example: can we prove, using internal logic, that in the five-lemma, the middle morphism is "injective" ($f(x)=f(y)\vdash_{x,y} x=y$) and "surjective" ($\vdash_{y} \exists x, f(x)=y$) and somehow that would imply that it's both mono and epi, and thus (in an abelian category) iso ? (I'm not typing the sequents, though of course I should)

So to sum up,

Is there a way in which reasoning with the internal logic of an abelian category can help us prove things (such as diagram lemmas) in those, much like we do in the "ordinary ones" (i.e. $R-\mathbf{Mod}, \mathbf{Ab}$) ?

Answer 1

This MathOverflow question and answer and the referenced slides and the comments both by Ingo Blechschmidt seem directly aimed at your question. See also the nLab page on diagram chasing whose section on diagram chasing in abelian categories addresses the approach you are considering. What you are suggesting is the fourth approach. For your purposes, you may want to look at the other approaches mentioned as well, such as the two element in an abelian category approaches.

As far as I can tell from the above, the "obvious" approach works. Basically, an abelian category is a regular category, so you can definitely interpret regular logic. You can then assert the existence of an abelian group structure for every sort/type, i.e. $\cfrac{\Gamma\vdash t_1:B\qquad \Gamma\vdash t_2:B}{\Gamma\vdash t_1+t_2 : B}$ and so forth. The mentioned "axiom of unique choice", true in any lex category, states that morphisms are equivalent to total functional relations in the internal logic. With the caveat of requiring constructive logic, you can use ordinary element-wise reasoning in this language and the results will be true in any abelian category.

Starting with a regular logic and then asserting every sort has an abelian group structure, should essentially give you the internal language of a regular additive category. However, an abelian category is precisely an exact additive category. Regular categories and exact categories are intimately related. A regular category says all congruences of the form $\Gamma,x:A,y:A\vdash f(x)=f(y)$ for any morphism $f$ have quotients, i.e. coequalizers of the two components of $\{\langle x,y\rangle\in A\times A\mid f(x)=f(y)\}\rightarrowtail A\times A$. This is exactly the image of $f$. An exact category states that every congruence is of the above form for some $f$. (In particular, for the quotient map $q:A\to A/{\sim}$.)

I'm just making this up and patching things together, so take this all with a large grain of salt, but combining the presentation of a regular type theory with effective quotients in Maria Maietti's Modular correspondence between dependent type theories and categories including pretopoi and topoi should give a characterization of exactness. Then adding the additive group structure should give a type theory compatible with abelian categories. I adapt Maietti's presentation notationally. I'll use $\Gamma\vdash T\ \mathsf{prop}$ to mean $\Gamma\vdash T\ \mathsf{type}$ and $\Gamma,x:T,y:T\vdash x=y:T$, i.e. that $T$ is a mono type. Terms of mono types correspond to subobjects. As another shorthand, I'll write $\Gamma\vdash T$ when $T$ is a monotype to mean $\Gamma\vdash c:T$ where $c$ is any term of type $T$ in scope (which are necessarily all equal). I'm omitting the usual structural rules and the rules for equality.

Terminal object: $$\cfrac{}{\Gamma\vdash\top\ \mathsf{type}}\top F\qquad\cfrac{}{\Gamma\vdash\star:\top}\top I \qquad\cfrac{\Gamma\vdash t:\top}{\Gamma\vdash t = \star:\top}\top\beta$$

Dependent sum (and thus finite products): $$\cfrac{\Gamma,x:B\vdash C(x)\ \mathsf{type}}{\Gamma\vdash\Sigma x:B.C(x)\ \mathsf{type}}\Sigma F\qquad\cfrac{\Gamma\vdash b:B\qquad\Gamma\vdash c:C(b)\qquad\Sigma x:B.C(x)\ \mathsf{type}}{\Gamma\vdash\langle b,c\rangle:\Sigma x:B.C(x)}\Sigma I$$

$$\cfrac{\Gamma,z:\Sigma x:B.C(x)\vdash M(z)\ \mathsf{type}\qquad \Gamma\vdash d:\Sigma x:B.C(x)\qquad\Gamma,x:B,y:C(x)\vdash m(x,y):M(\langle x,y\rangle)}{\Gamma\vdash\mathsf{elim}_\Sigma(d,x,y.m(x,y)):M(d)}\Sigma E$$

$$\cfrac{\Gamma,z:\Sigma x:B.C(x)\vdash M(z)\ \mathsf{type}\qquad \Gamma\vdash b:B\qquad \Gamma\vdash c:C(b)\qquad\Gamma,x:B,y:C(x)\vdash m(x,y):M(\langle x,y\rangle)}{\Gamma\vdash\mathsf{elim}_\Sigma(\langle b,c\rangle, x,y.m(x,y))=m(b,c):M(\langle b,c\rangle)}\Sigma\beta$$

Extensional equality type (and thus pullbacks given the dependent sum): $$\cfrac{\Gamma\vdash C\ \mathsf{type}\qquad\Gamma\vdash c:C\qquad\Gamma\vdash d:C}{\Gamma\vdash\mathsf{Eq}(C,c,d)\ \mathsf{type}}\mathsf{Eq}F\qquad\cfrac{\Gamma\vdash c:C}{\Gamma\vdash\mathsf{refl}_C(c):\mathsf{Eq}(C,c,c)}\mathsf{Eq}I$$

$$\cfrac{\Gamma\vdash p:\mathsf{Eq}(C,c,d)}{\Gamma\vdash c=d:C}\mathsf{Eq}E\qquad\cfrac{\Gamma\vdash p:\mathsf{Eq}(C,c,d)}{\Gamma\vdash p=\mathsf{refl}_C(c):\mathsf{Eq}(C,c,d)}\mathsf{Eq}\beta$$

Existential type (which can actually be defined as $(\Sigma x:B.C(x))/\top$): $$\cfrac{\Gamma,x:B\vdash C(x)\ \mathsf{prop}}{\Gamma\vdash\exists x:B.C(x)\ \mathsf{type}}\exists F\qquad\cfrac{\Gamma\vdash b:B\qquad\Gamma\vdash c:C(b)\qquad\Gamma\vdash\exists x:B.C(x)\ \mathsf{type}}{\Gamma\vdash(b,c):\exists x:B.C(x)}\exists I$$

$$\cfrac{\Gamma\vdash\exists x:B.C(x)\ \mathsf{type}\qquad\Gamma\vdash b:B\qquad\Gamma\vdash c:C(b)\qquad\Gamma\vdash d:B\qquad\Gamma\vdash t:C(d)}{\Gamma\vdash(b,c)=(d,t):\exists x:B.C(x)}\exists{=}$$

$$\cfrac{\Gamma,z:\exists x:B.C(x)\vdash M(z)\ \mathsf{prop}\qquad\Gamma\vdash d:\exists x:B.C(x)\qquad\Gamma,x:B,y:C(x)\vdash m(x,y):M((x,y))}{\Gamma\vdash\mathsf{elim}_\exists(d,x,y.m(x,y)):M(d)}\exists E$$

Effective extensional quotient types: $$\cfrac{\Gamma,x:A,y:A\vdash R(x,y)\ \mathsf{prop}\qquad\Gamma,x:A\vdash R(x,x)\qquad\Gamma,x:A,y:A,p:R(x,y)\vdash R(y,x)\qquad\Gamma,x:A,y:A,z:A,p:R(x,y),q:R(y,z)\vdash R(x,z)}{\Gamma\vdash A/R\ \mathsf{type}}QF$$

$$\cfrac{\Gamma\vdash a:A\qquad\Gamma\vdash A/R\ \mathsf{type}}{\Gamma\vdash[a]:A/R}QI\qquad\cfrac{\Gamma\vdash a:A\qquad\Gamma\vdash b:A\qquad\Gamma\vdash A/R\ \mathsf{type}}{\Gamma\vdash [a]=[b]:A/R}Q{=}$$

$$\cfrac{\Gamma,z:A/R\vdash L(z)\ \mathsf{type}\qquad\Gamma\vdash p:A/R\qquad\Gamma,x:A\vdash l(x):L([x])\qquad\Gamma,x:A,y:A,d:R(x,y)\vdash l(x)=l(y):L([x])}{\Gamma\vdash\mathsf{elim}_Q(p, x.l(x)):L(p)}QE$$

$$\cfrac{\Gamma,z:A/R\vdash L(z)\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma,x:A\vdash l(x):L([x])\qquad\Gamma,x:A,y:A,d:R(x,y)\vdash l(x)=l(y):L([x])}{\Gamma\vdash\mathsf{elim}_Q([a], x.l(x))=l(a):L([a])}Q\beta$$

$$\cfrac{\Gamma\vdash a:A\qquad\Gamma\vdash b:A\qquad\Gamma\vdash [a]=[b]:A/R}{\Gamma\vdash\mathsf{eff}(a,b):R(a,b)}\mathsf{Eff}$$

Additive structure: $$\cfrac{\vdash A\ \mathsf{type}}{\Gamma\vdash 0_A:A}0I\qquad\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma\vdash b:A}{\Gamma\vdash a+b:A}{+}I\qquad\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A}{\Gamma\vdash -a:A}{-}I$$

$$\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma\vdash b:A}{\Gamma\vdash a+b=b+a:A}{+}\sigma\qquad\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A}{\Gamma\vdash 0+a=a:A}{+}\lambda$$

$$\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma\vdash b:A\qquad\Gamma\vdash c:A}{\Gamma\vdash (a+b)+c=a+(b+c):A}{+}\alpha\qquad\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A}{\Gamma\vdash a+(-a)=0_A:A}{+}i$$

$$\cfrac{\vdash A\ \mathsf{type}\qquad\vdash B\ \mathsf{type}\qquad x:A\vdash t:B}{\Gamma\vdash t[0_A/x]=0_B:B}0c$$

$$\cfrac{\vdash A \ \mathsf{type}\qquad\vdash B\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma\vdash b:A\qquad x:A\vdash t:B}{\Gamma\vdash t[a+b/x]=t[a/x]+t[b/x]:B}{+}c$$

It is not the case that $\top$ and $A\times B(=\Sigma x:A.B)$ correspond to a void/empty/false/$\bot$ type and coproduct type respectively, because initial objects and coproducts in abelian categories are not stable, i.e. preserved by pullback functors. What we can show is that they do behave like void types and coproduct types if we only consider closed types, i.e. the types that correspond to objects of the abelian category rather than objects in a fiber category. All the additive structure is restricted to terms of closed types.

Let $\vdash A\ \mathsf{type}$, $\vdash B\ \mathsf{type}$, and $\vdash C\ \mathsf{type}$, i.e $A$, $B$, and $C$ are closed types, from this point on. Let's show that $\top$ is initial. Clearly, $x:\top\vdash 0_A:A$ shows that there exists an arrow from $\top$ to any (closed) $A$. To show uniqueness, consider a term $x:\top\vdash t(x):A$. Since $x=\star:\top$ via $\top\beta$, this term is the same as $x:\top\vdash t(\star):A$ and so we have $t(x)=t(\star)=t[t'/x]$ for any $t':\top$. In particular, for $t'=0_\top$ we get $t(x)=t[0_\top/x]=0_A$ via $0c$. (Really, we could replace the rule $0c$ with the rule $\frac{\vdash t:A}{\Gamma\vdash t=0_A:A}$ which is to say the only constant term is zero which makes sense as the only constant abelian group homomorphism is the zero morphism.) Next, write $A\oplus B$ for $A\times B$. Define $\mathsf{inl}(a)$ as $\langle a,0_B\rangle$ and $\mathsf{inr}(b)$ as $\langle 0_A,b\rangle$. Define $\mathsf{elim}_\oplus(t,x.f(x),y.g(y))$ as $\mathsf{elim}_\Sigma(t, x,y.f(x)+g(y))$ where $\Gamma\vdash t:A\oplus B$, $\Gamma,x:A\vdash f(x):C$, and $\Gamma,y:B\vdash g(y):C$. It's easy to show that this satisfies the universal property of the coproduct.

The kernel of $\Gamma,x:A\vdash f(x):B$ is $\Sigma x:A.\mathsf{Eq}(B,f(x),0_B)$. The image is $A/R$ where $R(x,y)$ is defined as $\mathsf{Eq}(B,f(x),f(y))$. The cokernel is $B/R$ where $R(x,y)$ is defined as $\exists a:A.\mathsf{Eq}(B,f(a),x-y)$. The coimage is $A/R$ where $R(x,y)$ is defined as $\exists a:A.\mathsf{Eq}(B,f(a),0_B)\times\mathsf{Eq}(A,a,x-y)$. Showing that the image is isomorphic to the kernel of the cokernel using this language is a good exercise. Similarly for the coimage and the cokernel of the kernel. From here it is fairly obvious that the coimage is isomorphic to the image. Either direction is just $\mathsf{elim}_Q(z,x.[x])$ whose well-formedness in both directions just requires $(\exists a:A.f(a)=0\land a = x-y)\iff (f(x)=f(y))$ which clearly holds.

Answer 2

While Andreas raises a very interesting question in the comments, to which I don't know the answer, except to agree that disjunction doesn't work normally in abelian categories since they're not coherent, the restriction to regular logic presents no problems.

For example, given $f:B\to C$, the proposition $f(x)=0$ is simply interpreted as the subobject of $B$ given by all $x$ such that $f(x)=0$. Similarly, $g(y)=x$ is the appropriate subobject of $A\oplus B$, while $\exists y:g(y)=x$ is its image in $B$, which is precisely the image of $g$. Exactness is the assumption that these subobjects are contained in each other, which is how we interpret entailment of propositions.

We can actually prove that this kind of thing will always work using Mitchell's embedding theorem. The embedding is exact and fully faithful, so it preserves and reflects statements of regular logic, and the categorical interpretation of logical statements in a module category is, of course, just the classical interpretation. So any regular statement you can prove in a module category will be true in the internal logic in any abelian category.

Answer 3

Since the OP asked for it I will give a sort description of a method for proving the existence of the connecting morphism in the snake lemma, this method will use generalized elements to transport almost verbatim the tradional proof for categories of modules.

In this proof I will follow the diagrams in this pdf (I preferred to use a single pdf instead of putting lots of images, I apologize for the inconvenience). $\DeclareMathOperator{\Ker}{Ker} \DeclareMathOperator{\Coker}{Coker} \DeclareMathOperator{\coker}{coker}$

So assume we have a situation as depicted in diagram (1) in the pdf.

We want to build a morphism from $\Ker \gamma$ into $\Coker \alpha$. The guiding idea to provide such morphism is that a morphism is the same as a natural transformation between the associated presheaves (by Yoneda): so to provide a morphism between two objects $X$ and $Y$ one could provide a family of bijections $\hom[U,X] \to \hom[U,Y]$ natural in $U$.

Using this guiding principle we try to find a function that associates to every generalized element of $\Ker \gamma$, i.e. a morphism $x \colon U \to \Ker \gamma$, a generalized element of $\Coker \alpha$ with the same domain, i.e. a morphism $\delta x \colon U \to \Coker \alpha$.

This function is basically an arrow-version of the mapping provided in the module-proof: in the case of modules the connecting map $\delta$

• picks an $x \in \Ker \gamma$,
• pulls it back through the epimorphism $g$,
• sends in down through $\beta$,
• pulls back again along $f'$
• (finally) pushs it down via $\coker \alpha$.

We will do something similar.

• We start by picking a generalized element $x \colon U \to \Ker \gamma$

• We pull back $(\ker \gamma) \circ x$ along $g$, thus obtaining the generalized element $\bar x \colon P \to B$ and an epimorphism $\pi \colon P \to U$ (by a theorem, in abelian categories pullbacks preserve epimorphisms). The square $(\bar x,\bar g,g,\ker \gamma \circ x)$ is a pullback square (as depicted in the diagram (3)).

• Then we can push down ${\bar x}$ along $\beta$ getting $\beta \circ \bar x$.

By diagram chasing one can easily see that $g' \circ \beta \circ \bar x$ is equal to the null map, hence $\beta \circ \bar x$ factors through the kernel of $g'$, which by the exactness of the lower row is $f'$.

• In this way we get a unique (generalized) element $\bar{\bar x} \colon P \to A'$, as shown in diagram (4), which is the unique morphism that can be obtained by pulling back $\beta \circ \bar x$ along $f$, i.e. the unique morphism such that $f \circ \bar{\bar x}=\beta \circ \bar x$.

• By composition with $\coker \alpha$ we get a generalized element $\coker \alpha \circ \bar{\bar x} \colon P \to \Coker \alpha$.

The problem is that $\coker\alpha \circ \bar{\bar x}$ has domain $P$ while we need a generalized element with domain $U$.

To solve this problem we just need to show that $\coker \alpha \circ \bar {\bar x}$ factors through the epimorphism $\bar g$.

We do this by showing that $\coker \alpha \circ \bar{\bar x} \circ \ker \bar g$ is a null morphism, this implies that $\coker \alpha \circ \bar{\bar x}$ factors through the coker of $\ker \bar g$, which is $\bar g$ by abstract-nonsense.

In diagram (5) we consider have a unique $\bar x$ which makes commute the square (this comes from abstract nonsense) so we have the equality $$f \circ \bar x' = \bar x \circ \ker \bar g\ .$$

From this last equality, by diagram chasing, it follows that $$\bar{\bar x} \circ \ker \bar g = \alpha \circ \bar x'$$ hence that $$\coker \alpha \circ \bar{\bar x} \circ \ker \bar g = 0$$ as we wanted.

From this it follows, as said before, that $\coker \alpha \circ \bar{\bar x}$ factors through $\bar g$, i.e. that there is a generalized element (which is uniquely determined by universal properties) $\delta x \colon U \to \Coker \alpha$ such that $$\coker \alpha \circ \bar{\bar x}=\delta x \circ \bar g\ .$$

Summarizing we basically have build a function $\delta \colon \hom[U,\Ker \gamma] \to \hom[U,\Coker \alpha]$ (which maps generalized elements by the same pulling-pushing game that is used in the module-version with some adjustments).

From this one could proceed by showing the naturality of the functions in $U$, but since we are interested just in the morphism $\delta \colon \ker \gamma \to \Coker \alpha$ (again using yoneda under the hood) we can simply observe that by letting $U=\Ker \gamma$ and $x=\text{id}_{\Ker \gamma}$ the morphism $\delta \text{id} \colon Ker \gamma \to \Coker \alpha$ gives exactly the required morphism.

Some comments: I want to strees that the complications found in order to obtain the morphism $\delta x$ from $\coker \alpha \circ \bar{\bar x}$ are the arrow-version of the well-definition problem that one encounters while defining the connection-morphism $\delta$ in the module case.

I hope this example can give an hint of the power of the use of generalized elements in .... generalizing proofs from the classical set-based cases.

Answer 4

There are many good answers here, but none do actually show a diagram chase in an abelian category performed in 'the' internal language. I like to fill the gap by chasing both the five lemma (or a part of it) and the snake lemma. I do the latter because we have to construct a new morphism in its proof, and it is nice to see how categorical logic deals with that problem.

Abelian categories are precisely additive categories for which the subobject fibration can interpret regular logic and has effective quotients. This means we can interpret a type theory in the subobject fibration of any abelian category which I will now try to describe in broad stroaks.

Fix a small abelian category $\mathbb A$. If it isn't small, then we switch to a larger universe in which it is. Part of the type theory is the usual type theory to describe morphism in a category with finite products. For example we use $\mathtt{x : A, y : B \vdash x : A}$ to denote the first projection map $A\oplus B\to A$. We denote the terminal object by $\mathbf 0$ instead of the usual $\mathbf 1$, because it is actually a zero object, and we give it the elimination rules of both a terminal and an initial object. We can also equip the type constructor $A\oplus B$ with elimination and introduction rules for both coproducts and products. Finally we add for each type term forming rules such as \begin{align}\cfrac{\mathtt{\Gamma\vdash M : A}\qquad \mathtt{\Gamma \vdash N : A}}{\mathtt{\Gamma \vdash M + N : A}}\end{align}

and we make the equalities (of the theory of abelian groups) hold judgmentally. We can also let the usual equations between the coproduct and product term constructors of $\mathtt{A \oplus B}$ hold judgementally, but we won't need all of this. Important is that it should be clear how to interpret sequents $\mathtt{\Gamma \vdash M : A}$ in the base category $\mathbb A$. I will manipulate predicates in the style of fibred categorical logic (a very good reference are the chapters 3 and 4 of Bart Jacobs' book Categorical Logic and Type Theory). That means we are manipulating sequents of the form $\mathtt{\Gamma |\Theta \vdash \varphi}$ where $\mathtt{\Gamma}$ is a type context, $\mathtt{\Theta}$ is a list of predicates lying over the $\mathtt{\Gamma}$ (they literally do in the syntactic regular fibration created from the formal language), and also $\mathtt{\varphi}$ is a predicate with free variables coming from the variables declared in the context. The interpretation of such a sequent in the subobject fibration of the abelian category $\mathbb A$ will be that the subobject denoted by $\mathtt{\Theta}$ factors through the subobject denoted by $\mathtt{\varphi}$. We can use the connectives $\mathtt{\wedge}$, $\mathtt{\top}$ and $\mathtt{=}$ of regular logic and all the rules of logic are sound with respect to the interpretation in the subobject fibration of $\mathbb A$. Important:

• The interpretation of a context is an object in $\mathbb A$. For example the interpretation of the context $\mathtt{a:A,b:B,x:C\oplus B}$ is the object $A \oplus B \oplus (C \oplus B)$.

• The interpretation of a sequent of the form $\mathtt{\Gamma \vdash M : B}$ is a morphism in the abelian category $\mathbb A$. For example if $f,g: A \to B$ are two morphisms in the abelian category, then the interpretation of the sequent $\mathtt{a:A\vdash fa + ga : B}$ is the morphism $f+g$ in the abelian category.

• The interpretation of a string of the form $\mathtt{\Gamma | \Theta}$, where $\mathtt{\Gamma}$ is a context and $\mathtt{\Theta}$ is a list of predicates with free variables coming from $\mathtt{\Gamma}$, is a subobject of the interpretation of $\mathtt{\Gamma}$.

• The interpretation of a sequent of the form $\mathtt{\Gamma|\Theta\vdash \varphi}$ is a morphism from the interpretation of $\mathtt{\Gamma|\Theta}$ to the interpretation of $\mathtt{\Gamma|\varphi}$ in the fibre over the interpretation of the type context. Since the fibres of the subobject fibration are partial orders, there can be at most one morphism between any two predicates, and thus $\mathtt{\Gamma|\Theta\vdash \varphi}$ is more an assertion about the two subobjects than an actual morphism. We say that such a sequence is true, if it can be interpreted (i.e. if there is an actual morphism in the subobject fibration between the two subobjects).

Now let us chase a diagram. We will prove one of the four lemmas. Assume that in the diagram $\require{AMScd}$ \begin{CD} A @>{f}>> B @>{g}>> C @>{h}>> D\\ @V{\alpha}VV @V{\beta}VV @V{\gamma}VV @V{\delta}VV\\ A' @>{f'}>> B' @>{g'}>> C' @>{h'}>> D' \end{CD} the rows are exact, $\alpha$ and $\gamma$ are epimorphisms and $\delta$ is a monomorphism. Then $\beta$ is an epimorphism. Before we can even start chasing in the internal language we need to be able to express the hypothesis and the conclusion of the lemma in the new language. Here are some facts.

Fact 1. A sequence $A \xrightarrow{f} B\xrightarrow{g}C$ is exact at $B$ if and only if the interpretation of the sequents $\mathtt{b : B | g\, b = 0 \vdash \exists a : A, f \,a = b}$ and $\mathtt{b : B | \exists a : A, f \,a = b \vdash g\, b = 0}$ is true. The second sequent is interderivable with $\mathtt{a : A| \top \vdash g (f a) = 0}$.

Proof. The first claim follows from the fact that the interpretation of $\mathtt{b : B|\exists a : A,fa = b}$ is the image of the morphism $f$, and the interpretation of $\mathtt{b : B|gb = 0}$ is the kernel of $g$. Next let us show how we can derive $\mathtt{a : A|\top \vdash g(fa) = 0}$ from $\mathtt{b:B|\exists a:A,fa = b \vdash gb = 0}$. The Lawvere double rule of the existence quantifier (see Jacob page 230) tells us that we get $\mathtt{b:B,a:A|fa = b \vdash gb = 0}$ from our assumption. Now clearly if the sequent is true for arbitrary terms of type $\mathtt{B}$, then we should be allowed to insert a specific term, namely $\mathtt{a:A\vdash fa:B}$ of type $\mathtt{B}$. This is indeed the case and follows from the structure and substitution rules of logic. We are allowed to conclude that $\mathtt{a:A|fa= fa \vdash gfa= 0}$, and since the left predicate is true by reflexivity of the internal equality, we get that $\mathtt{a:A|\top\vdash gfa = 0}$. The other direction is an exercise. $\square$

Facts 2 and 3. A map $f: A \to B$ is epi if and only if it is a regular epimorphism, and this is the case if and only if the sequent $\mathtt{b : B| \top\vdash \exists a : A, f\, a = b}$ is true. The map is monic if and only if the sequent $\mathtt{a : A, a ': A | f\, a = f\,a' \vdash a = a'}$ is true. In the setting in which we are the sequent is provably equivalent to the sequent $\mathtt{a : A | f\, a = 0 \vdash a = 0}$.

Proof. I skip the proof, sorry. $\square$

Here is the chase of the four lemma. We know that $\alpha$ and $\gamma$ are epi and that $\delta$ is monic. And we know that the rows are exact. This gives us a lot of sequent as assumptions which we will use throughout the proof. We like to derive that $\mathtt{b ' : B'| \top \vdash \exists b : B, \beta \,b = b'}$.

How does a formal proof look like? A formal proof is a list of sequents, such that the last sequent in the list is the statement we like to prove, and every list entry is either an axiom, and assuption or follows from previous entries by a deduction rule (or a rule which is derived from the deduction rules of the logic). We will allow ourselves to be a bit sloppy and skip over some steps which use the structure and substitution rules of logic. Here is my proof. There are probably some mistakes in it, because being formal is hard. It is more for the flair and the vibes.

1.  b':B' ⊢ g'b':C'                                        -- function rule for g'
2.  c':C' |  ⊢ ∃c:C, γc = c'                               -- assumption: γ is epi
3.  b':B', c':C'|  ⊢ ∃c:C, γc = c'                         -- weakening of 2.
4.  b':B' |  ⊢ ∃c:C, γc = g'b'                             -- substitution rule with 1. and 3.
5.  c:C | hc = 0 ⊢ ∃b:B, gb = c                            -- assumption: ker h ⊂ im g
6.  b':B', c:C |  ⊢ h'g'b' = 0                             -- assumption: h'∘ g' = 0
7.  b':B', c:C | γc = g'b' ⊢ h'γc = 0                      -- weakening of 6.
8.  b':B', c:C |  ⊢ δhc = h'γc                             -- assumption : the diagram commutes         
9.  b':B', c:C | γc = g'b' ⊢ δhc = 0                       -- combining 7. and 8. and rules of =
10. b':B', c:C | γc = g'b' ⊢ hc = 0                        -- use that δ is monic by assumption 
11. b':B', c:C | hc = 0 ⊢ ∃b:B, gb = c                     -- recall line 5. 
12. b':B', c:C | γc = g'b' ⊢ ∃b:B, gb = c                  -- CUT on 10. and 11.
13. b':B', c:C, b:B | γc = g'b', gb = c ⊢ γgb = g'b'       -- self-evident
14. b':B', c:C, b:B | b:B                                  -- also self-evident
15. b':B', c:C, b:B | γc = g'b', gb = c ⊢ ∃x:B, γgx = g'b' -- ∃ Intro with 14. and 13.   
16. b':B', c:C | γc = g'b' ⊢ ∃x:B, γgx = g'b'              -- ∃ Elim with 15. and 12.
17. b':B' |  ⊢ ∃b:B, γgb = g'b'                            -- ∃ Elim with 16. and 4.
 
 -- Let's take a small break. We have started with some b':B' 
 -- we managed to show that there is a c which maps to g'b' (line 4)
 -- and we managed to lift that c to some b:B, such that γgb = g'b' (line 17). 
 -- Now we are a bit more sloppy

18. b':B', b:B | γgb = g'b' ⊢ g'(b' - βb) = 0       -- because g'(βb - b') = g'βb - g'b' =  γgb - g'b' = 0
19. b':B', b:B | γgb = g'b' ⊢ ∃a':A', fa' = b' - βb -- because the lower sequence is exact
20. b':B', b:B | γgb = g'b' ⊢ ∃a:A, f'αa = b' - βb  -- because the map α is epi
21. b':B', b:B, a:A | γgb = g'b', fαa = b' - βb ⊢ β(b + fa) = b' -- a simple computation
22. b':B', b:B, a:A | γgb = g'b', fαa = b' - βb ⊢ ∃x:B,βx = b' --∃ Introduction 
23. b':B', b:B | γgb = g'b' ⊢ ∃x:B, βx = b'         -- ∃ Elim with line 20
24. b':B' |  ⊢ ∃x:B, βx = b'                        -- ∃ Elim with line 17. 

I know I promised a proof of the snake lemma in my first paragraph, but I am now tired. I will write the missing part tomorrow. But for now here are the main points:

• Subobject fibration satisfy a principle of unique description. If you have some formula $\mathtt{a:A,b:B|\varphi(a,b)}$ and you manage to prove that it is the relation of a function (in the internal logic), that is $\mathtt{ |\top\vdash \forall a:A \exists!b:B, \varphi(a,b)}$ then there is one and only one morphism $f: A\to B$ in the base category for which $\mathtt{a:A|\top \vdash \varphi(a,fa)}$ will be true. This is how you can define the connecting morphism when you do the proof of the snake lemma. If you only can use regular logic, then you have to replace $\mathtt{a:A,b:B|\varphi(a,b)}$ by equivalent conditions in regular logic, of course. You can even enhance the language of first order logic by a 'definite description' $\iota$ operator. It allows to introduce terms like $\mathtt{a:A\vdash \iota b:B, \varphi(a,b) : B}$. The idea is that the term describes, given $a$, the unique $b$ for which $varphi(a,b)$ holds. The interpretation of the sequent is then of course the unique map $f$ we have just mentioned. Adding $\iota$-description operators to your language allows you to prove the properties of the snake lemma connecting morphism without leaving the internal language and introducing a new function symbol.

• Regular logic can be conservatively extended to first order intuitionistic logic (and even higher order intuitionistic logic). This follows from the Barr-embedding theorem. See the answer from Zehn Lin to a question I asked a while ago. This means you can show rigorously that every small abelian category is an exact full subcategory of the category of internal abelian groups in a sheaf topos (and a topos is a category in which all of higher order intuitionistic logic may be interpreted). This simplifies life by a lot! In particular in our example above it means we could have used the full strength of first order logic to derive the sequent $\mathtt{b':B'|\top\vdash \exists b:B, \beta b= b'}$.