Let be a discrete fibration and let be monic in . If satisfy , lift uniquely to with codomain . The composites are lifts of the same arrow with codomain , so uniqueness gives equality. Since is monic, , hence . Thus is monic.
Use the convention that has objects . Its forgetful functor sends to . Given , the unique arrow above with codomain has domain . Hence the forgetful functor is a discrete fibration.

Articles by others on the same topic (0)

There are currently no matching articles.