Events

Microsoft Research - Inria Joint Centre
Campus de l’Ecole polytechnique, Palaiseau
Bld Alan Turing, Salle MilnerSome Thoughts on Galois Connections, Poset-Enriched Categorical Logic, and Type Theory
McMaster Univ. & MSR-Inria Joint CentreIn this talk I will present three bits of mathematics that have recently piqued my interest:- The first item is Galois connections. I will give some examples of how Galois connections can be used to give very concise specifications of some mathematical functions.- The second item is poset-enriched categories. I will give a quick overview of what enriched categories are and give some motivation as to why I think that poset-enriched categories are more fundamental than ordinary categories.- The third item is categorical logic. I will give an example of how adjuctions, which are generalizations of Galois connections, can be used to give very concise specifications of the basic connectives of type theory.Lastly I will tie the themes together by describing what poset-enriched categorical logic might be, and how its corresponding type theory might differ from ordinary type theory.