Send the link below via email or IMCopy
Present to your audienceStart remote presentation
- Invited audience members will follow you as you navigate and present
- People invited to a presentation do not need a Prezi account
- This link expires 10 minutes after you close the presentation
- A maximum of 30 users can follow your presentation
- Learn more about this feature in our knowledge base article
Do you really want to delete this prezi?
Neither you, nor the coeditors you shared it with will be able to recover it again.
Make your likes visible on Facebook?
You can change this under Settings & Account at any time.
Category Theory in Higher-Order Logic
Transcript of Category Theory in Higher-Order Logic
Supervisor: Sam Staton Motivation What is the composite of
f : X→Y and g : W→Z
(where Y ≠ W)? HOL only has total functions Dependent types... F,G : C→D, Fx = Gx for all x in C, but Fa ≠ Ga.
F = G? Or, fix a target to send things outside the domain Understand Category Theory better Test the foundations Case study for a future system
where maths can be formalized without fixing implementation details Or, pick a limit arbitrarily
and prove invariance under isomorphism plus principles of definition : bool : α → β : (α, β) category Or both? interacts better with HOL but not closed under products etc. (or talk about classes informally)