The Freyd cover is the special case .
One of the first applications of the Freyd cover was to deduce facts about the initial topos? (initial with respect to logical morphisms — also called the free topos). They were originally proved by syntactic means; the conceptual proofs of the lemma and theorem below are due to Freyd.
For any category with a terminal object , the terminal object of the Freyd cover is connected and projective, i.e., the representable preserves any colimits that exist.
To check that preserves limits, it suffices to check that the composite
preserves limits, because the contravariant power set functor is monadic. But it is easily checked that this composite is the contravariant representable given by .
The terminal object in the initial topos is connected and projective, i.e., preserves finite colimits.
We divide the argument into three segments:
The hom-functor preserves finite limits, so by general properties of Artin gluing, the Freyd cover is also a topos. Observe that is equivalent to the slice where is the object . Since pulling back to a slice is a logical functor, we have a logical functor
Since is initial, is a retraction for the unique logical functor .
We have maps (the isomorphism comes from , which is clear since is logical), and since is logical and retracts . Their composite must be the identity on , because there is only one such endomorphism, using the Yoneda lemma and terminality of .
Finally, since is a retract of a functor that preserves finite colimits (by the lemma, and the fact that the logical functor preserves finite colimits), it must also preserve finite colimits.
This is important because it implies that the internal logic of the free topos (which is exactly “intuitionistic higher-order logic”) satisfies the following properties:
The existence property: if “there exists an such that ” is provable in the empty context, then there exists a global element such that is provable in the empty context. (Again, this is clearly a constructivity property.)
The negation property: False is not provable in the empty context.
See (Johnstone, lemma C3.6.4).
You can find more on Artin gluing in this important (and nice) paper:
See also section C3.6 of
Some of the above material is taken from
The argument given above for properties of the free topos is an amplification of