Loading presentation...

Present Remotely

Send the link below via email or IM


Present to your audience

Start 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.


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.

Ramana Kumar

on 18 May 2011

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Category Theory in Higher-Order Logic

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)
Full transcript