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.

# Category Archives: Math

# Representable functors in Haskell

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 , where each is divisible by some number , is irreducible in when does not divide .

If A is not irreducible then there are some and such as .

But that means that , which means that XOR (since does not divide ).

Let’s assume that . Now let’s take a map (I believe this method is called homomorphism-reduction).

, but , where .

That is possible only when is constant and . Which means that is irreducible.

Note: here denotes where is a homomorphism .

# Union of countable sets is countable.

Let’s say we have a possibly infinite countable collection of countable sets , prove that is countable too. We are going to do this using Axiom of Choice.

Since every set is countable, there is a set of injections from to , let’s call it . Using the axiom of choice we can create a set of maps from to . Now, we are going to create an injection from to . If is an element of then it’s also an element of some set . Therefore we can construct where . And since we know that is countable, we can map to . QED.