This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
The UniMath library consists of Coq source files (file ending *.v) in the subdirectory UniMath/UniMath
.
Once you have installed UniMath, you can start browsing and editing the source files. There are several programs to interactively edit and step through the files, among which are
Here, we focus on Emacs/ProofGeneral.
When first opening a file in UniMath/UniMath
, you will be asked to apply a list of local variables, similar to the screenshot below. To accept permanently and not be asked again, type “!”. These variables are needed to achieve the automatic setup described below.
When opening a source file in the directory UniMath/UniMath
in Emacs, the following happens automatically.
Items 2 and 3 are achieved through the Emacs configuration file .dirlocals.el
located in
the subdirectory UniMath/UniMath
.
For this reason, we recommend you save your UniMath files in this subdirectory as well.
Andrej Bauer has a screencast on using Emacs/ProofGeneral
for writing and stepping through a Coq file.
(More screencasts are listed on his website.)
For following his instructions using his example, we recommend you save the Coq file in the subdirectory UniMath/UniMath
to profit from the automatic setup mentioned above.
Note that for Bauer’s specific example to work in UniMath, you need to insert the line
Require Import Coq.Init.Prelude.
at the beginning of the file, since the setup above does not load this library by default when reading a file.
UniMath uses both ASCII and Unicode notation. Below we give an overview of the most important symbols.
To see how to input a specific Unicode character, type
Cu Cx =
(meaning: hold CTRL, then press u and x; release CTRL, press =) while hovering over that character.
Below is a partial list of Unicode symbols and identifiers used in UniMath.
Item  UniMath symbol  Unicode input  UniMath ASCII alternative 

Type and term constructors  
Product type  ∏ (x : A), B 
\prod 
forall x : A, B 
Function type  A → B 
\to 
A > B 
Lambda abstraction  λ x, e 
\lambda 
fun x => e 
Sigma type  ∑ (x : A), B 
\sum 
total2 (fun x => B) 
Cartesian product type  X × Y 
\times 
dirprod X Y 
Pair term  a,,b 
a,,b 

Coproduct type  X ⨿ Y 
\union , then press down key 
coprod X Y 
Identity type  a = b 
a = b 

Univalent logic in hProp 

Conjunction  A ∧ B 
\and 
hconj A B 
Disjunction  A ∨ B 
\or 
hdisj A B 
Implication  A ⇒ B 
\=> 
himpl A B 
Negation  ¬ X 
\neg 
hneg X 
Universal quantification  ∀ x , P x 
\forall 
forall_hProp A 
Existential quantification  ∃ x, P x 
\ex 
hexists P 
Propositional truncation  ∥ A ∥ 
\\\ 
ishinh A 
Category theory  
Object type of C 
ob C or C (ob is a coercion) 

Morphisms  C⟦a,b⟧ 
\[[ and \]] 
a > b 
Functor F on objects 
F a (coercion) 

Functor F on morphisms 
#F f 