Index

A

axiom

C

constructor

context

E

element

extensionality

H

higher-inductive type

HIT hproposition

N

n-type

O

object

P

point pointed type

principle of excluded middle proof proposition

S

space

T

term	truncated type type

W

weak excluded middle