TypeTheory

The mathematical study of type theories, in univalent foundations

This project is maintained by UniMath

Library TypeTheory.Auxiliary.UnicodeNotations

TypeTheory.Auxiliary.UnicodeNotations
Part of the TypeTheory library (Ahrens, Lumsdaine, Voevodsky, 2015–present).

Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.opp_precat.
Require Export UniMath.Foundations.Propositions.
Require Export UniMath.CategoryTheory.Categories.
Require Export UniMath.CategoryTheory.functor_categories.
Require Export UniMath.CategoryTheory.opp_precat.

Open Scope cat.
Open Scope cat_deprecated.