# Frobenius property of weak factorisation systems and Pi-types

I’ve put together a note on the Frobenius property for weak factorisaion systems and it’s relation to models of type theory. Awodey and Warren described a way of obtaining a model of type theory with identity types from a model category structure/weak factorisation system. However, in absence of axioms for other type formers (specifically, Π-types), one is required to put an additional restriction on the weak factorisation system, in order to model identity elimination in an arbitrary context/with arbitrary parameters; specifically, it is required that cofibrations are stable under pullbacks along fibrations. In presence of Π-types, however, this is not necessary, as I tried to explain in the note.

I have finally managed to upload a (dry version) of a note about representable functors in Haskell. You can find it here: http://covariant.me/notes/rep-functors.html

Representable functors are functors that are isomorphic to $Hom(A, -)$ or $Hom(-, A)$ for some object $A$. In the note I give examples of some simple representable functors and prove that Maybe is not representable.

# Proving the Eisenstein’s criteria

Polynomial $A = x^n + a_{n-1}x^{n-1} + .. + a_1 x + a_0$, where each $a_i$ is divisible by some number $p$, is irreducible in $\mathbb Q$ when $p^2$ does not divide $a_0$.
If A is not irreducible then there are some $F$ and $G$ such as $A = FG$.
But that means that $a_0 = f_0 g_0$, which means that $(p | f_0)$ XOR $(p | g_0)$ (since $p^2$ does not divide $a_0$).
Let’s assume that $p | f_0$. Now let’s take a map $Z[x] \rightarrow (Z/pZ)[x]$ (I believe this method is called homomorphism-reduction).
$[A] = x^n$, but $[G] = \cdots + [g_0]$, where $[g_0] \neq 0$.
That is possible only when $[G]$ is constant and $[F] = [A]/[G]$. Which means that $A$ is irreducible.

Note: here $[a]$ denotes $f(a)$ where $f$ is a homomorphism $Z[x] \rightarrow (Z/pZ)[x]$.

# Union of countable sets is countable.

Let’s say we have a possibly infinite countable collection of countable sets $A_1, A_2, \cdots, A_n, \cdots$, prove that $\bigcup A_i$ is countable too. We are going to do this using Axiom of Choice.

Since every set $A_i$ is countable, there is a set of injections from $N$ to $A_i$, let’s call it $M_i$. Using the axiom of choice we can create a set of maps $\{g_1, g_2, \cdots\}$ from $N$ to $A_i$. Now, we are going to create an injection from $(N, N)$ to $\bigcup A_i$. If $x_k$ is an element of $\bigcup A_i$ then it’s also an element of some set $A_m$. Therefore we can construct $f(z, m) = x_k$ where $x_k = g_m(z)$. And since we know that $(N, N)$ is countable, we can map $N$ to $\bigcup A_i$. QED.