Category Theory Problems Size Extensionality Notation e.g. "the" product Automation Category Theory in HOL Mathematical Engineering No set of all sets Augment logic with proper classes... Or, polymorphic category of sets Higher-Order Logic "Unique-up-to" Readability Ramana Kumar
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)
Loading presentation...
Present Remotely
Send the link below via email or IM
Present to your audience
- 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
Category Theory in Higher-Order Logic
The issues that arise when formalizing the category of sets in HOL. 8 minute presentation for the MPhil in ACS.
by
Tweet
