Pointed groupoids as the pullback of pointed categories

This file shows that PGrpd.forgetToGrpd is the pullback along Grpd.forgetToCat of PCat.forgetToCat.

Main statements

• CategoryTheory.PGrpd.isPullback_forgetToGrpd_forgetToCat - the functor PGrpd.forgetToGrpd is the pullback along Grpd.forgetToCat of PCat.forgetToCat.

• TODO Probably the latter half of this file can be shortened significantly by providing a direct proof of pullback using the IsMegaPullback definitions

theorem CategoryTheory.PGrpd.forgetToPCat_forgetToCat : forgetToPCat.comp PCat.forgetToCat = forgetToGrpd.comp Grpd.forgetToCat

def CategoryTheory.PGrpd.isPullback : forgetToPCat.IsPullback forgetToGrpd PCat.forgetToCat Grpd.forgetToCat

The following square is a (meta-theoretic) pullback

PGrpd ------ toPCat ------> PCat | | | | PGrpd.forgetToGrpd PCat.forgetToCat | | v v Grpd------forgetToCat------->Cat

Equations

• CategoryTheory.PGrpd.isPullback = CategoryTheory.Grothendieck.isPullback (CategoryTheory.Grpd.forgetToCat.comp (CategoryTheory.Functor.id CategoryTheory.Cat))

theorem CategoryTheory.PGrpd.isPullback' : IsPullback (Cat.homOf forgetToPCat) (Cat.homOf forgetToGrpd) (Cat.homOf PCat.forgetToCat) (Cat.homOf Grpd.forgetToCat)

The following square is a pullback in Cat

 PGrpd ------ toPCat ------> PCat
   |                           |
   |                           |

PGrpd.forgetToGrpd PCat.forgetToCat | | v v Grpd------forgetToCat------->Cat