`star f` can be identified with taking pullbacks

b-mehta / topos

Topos theory in lean

55 stars 2 forks source link

`star f` can be identified with taking pullbacks #24

Closed b-mehta closed 4 years ago

b-mehta commented 4 years ago

Where f : over B

See top of p44 of my notes or end of proof of Thm I.9.4 in MM

b-mehta commented 4 years ago

I suspect the hard part of this is figuring out how to express the statement... But also we might run into issues about transferring over isomorphisms