# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeJan 27th 2011

Created complete small category, and moved the proof of Freyd’s theorem to there from adjoint functor theorem.

• CommentRowNumber2.
• CommentAuthorTobyBartels
• CommentTimeJan 27th 2011

I added to the latter that the adjoint functor theorem for posets still holds constructively, despite the classical reasoning that precedes it. (After all, the classical stuff was only going the other way, but it still confused me for a minute as to whether you had actually proved the theorem constructively.)

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeJan 28th 2011

Thanks.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeSep 10th 2011

I just realized that the proof of Freyd’s theorem, in addition to being non-constructive, at least appears to be evil. We need the collection of all morphisms in the category to be a set (or a class, or something with an equality relation), which appears to require that the collection of all objects in the category be also a set, i.e. that the category be strict.

It looks even eviller if you beta-reduce the application of Cantor’s theorem by diagonalization. Then you get something like this: assuming $r,s \colon x\to y$, define a morphism $g\colon x \to \prod_{f\in Mor(D)} y$ whose $f^{th}$ component is $r$ if $f$ is a morphism $x \to \prod_{f\in Mor(D)} y$ whose $f^{th}$ component is $s$, and $s$ otherwise. Then the $g^{th}$ component of $g$ is $r$ if it’s $s$ and $s$ if it’s $r$, hence $r=s$. But now in the definition of $g$ there is an explicit equality test on the domain and codomain of each $f\in Mor(D)$.

Is this evil irredeemable?

(Personal story: last night I read the corresponding beta-reduced proof of the generalized version for factorization structures, and spent a while feeling ill about its evilness. Eventually I realized it was a beta-reduced version of a generalization of Freyd’s theorem, which simultaneously made me feel more comfortable with the proof for factorization structures, and less comfortable with Freyd’s proof.)

• CommentRowNumber5.
• CommentAuthorSam Staton
• CommentTimeDec 7th 2018

Added two references and a slightly longer discussion of models of impredicative type theory.