Metamath Proof Explorer
Table of Contents - 8.1.8. Full & faithful functors
- cful
- cfth
- df-full
- df-fth
- fullfunc
- fthfunc
- relfull
- relfth
- isfull
- isfull2
- fullfo
- fulli
- isfth
- isfth2
- isffth2
- fthf1
- fthi
- ffthf1o
- fullpropd
- fthpropd
- fulloppc
- fthoppc
- ffthoppc
- fthsect
- fthinv
- fthmon
- fthepi
- ffthiso
- fthres2b
- fthres2c
- fthres2
- idffth
- cofull
- cofth
- coffth
- rescfth
- ressffth
- fullres2c
- ffthres2c