Skip to content

Opportunities.md

Latest commit

 

History

History
85 lines (67 loc) · 4.75 KB

Opportunities.md

File metadata and controls

85 lines (67 loc) · 4.75 KB

Projects in UniMath

This page collects possible projects in UniMath that

  • are well-specified
  • can be done in a reasonable amount of time
  • would be suitable for inclusion in UniMath/UniMath (or, possibly, in a satellite repository)
  • possibly satisfy other criteria? (To be discussed.)

Construction of the free category generated by a graph

  • Could use an impredicative generation of the morphisms, or an inductive type (in the latter case, it would need to go into a satellite repository)
  • Would be useful for connecting different definitions of (co)limit

Proof that (co)limits commute with (co)limits

  • Should, in the first instance, use (co)limits indexed by a category, not (co)limits indexed by a graph
  • Special cases would also be useful (for instance, the case of colimits of cochains), but it is unclear if this is any easier than the general result

Moggi semantics

Moggi semantics are a well-established way to interpret programming languages with side effects using category.

The goal of this project would be:

  • Define the mono requirement (Definition 1.2 in [1])
  • Define strong monads (Definition 3.2 in [1])
  • Give examples of strong monads (Example 3.5 in [1])
  • Define models of λc (Definition 3.9 in [1])
  • Provide a shallow embedding of the rules of λc in arbitrary models (Tables 8-11 in [1])

Literature: [1]: Notions of computation and monads

Relevant notions in UniMath:

Markov Categories

Markov categories [1] give a synthetic way to study probability theory, and in particular, they can be used to give semantics for probabilistic programming languages [2]. For example, the notion of a deterministic morphism can be define internal to arbitrary Markov categories.

The goal of this project would be: ⁃ Define the notion of Markov category (Definition 2.1 in [1], Definition 6.3 in [2]).

  • Define affine monads (Definition 3.4 in [2])
  • Define commutative monads (Definition 3.3 in [2]). Note: there are alternative definitions as well (Proposition 2.6 in [3])
  • Show that the Kleisli category of an affine monad is a Markov category (Proposition 6.4 in [2]).
  • Define deterministic morphisms in Markov categories (Definition 6.5 in [2])
  • Define the representability condition for commutative and affine monads (Definition 6.8 in [2])
  • Give instances of such monads (Proposition 6.10 in [2])
  • Prove Proposition 6.9 in [2]

Literature: [1]: https://arxiv.org/pdf/1908.07021.pdf [2]: https://dario-stein.de/thesis.pdf [3]: https://ncatlab.org/nlab/show/monoidal+monad [4]: https://arxiv.org/pdf/2010.07416.pdf

Relevant notions in UniMath:

Quantum theory

Recently, category theory has found applications in quantum theory/computation. Using the language of monoidal categories and dagger categories, one can describe concepts and prove theorems from quantum mechanics in an abstract way

The goal of this project would be:

  • Define the category Rel of relations (Definition 0.5 in [1])
  • Define the monoid of scalars in monoidal categories (Definition 2.1 in [1]), and prove multiplication of scalars in commutative (Lemma 2.3 in [1])
  • Define dagger categories (Definition 2.32 in [1], Definitions 9.7.1 and 9.7.4 in [2])
  • Define various notions of morphisms in dagger categories (Definition 2.34 in [1])
  • Define monoidal dagger categories (Definition 2.37 in [1])
  • Define superposition rules (Definition 2.12 in [1])
  • Define dagger biproducts (Definition 2.39 in [1])
  • Define complete sets of effects (Definition 2.50 in [1])
  • Prove that Rel is a symmetric monoidal dagger category (Definition 2.33 in [1]) with a superposition rule and dagger biproducts
  • Prove the Born rule (Proposition 2.55 in [1])

Literature: [1]: Categories for Quantum Theory: an introduction [2]: https://homotopytypetheory.org/book/ [3]: https://ncatlab.org/nlab/show/dagger+category

Relevant notions in UniMath: