Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added a Properties-section to pullback
I made some minor improvements to the Properties section of pullback, making it match the similar section in pushout insofar as it can. (It’s a bit tiring to have to look at both these pages to get all the basic properties, so I fixed that, but for properties that hold both for pullbacks and dually for pushouts I’m happy to have all the proofs at pullback - that’s how it works now.)
Several pages on inductive types/W-types link to this page and use the term “pullback functor” with notation $f^*$, yet if you Ctrl-F on this page, you can’t find this term. This edit at least shortly mentions it and links to base change.
Stipulation: redirect pullback functor to base change
WorldSEnder
Thank you very much, Mr. or Mrs. Anonymous!
added pointer to:
1 to 13 of 13