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.
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.
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 .
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.