nmvdw Three-HITs issues - Githubissues

nmvdw / Three-HITs

All higher inductive types can be obtained from three simple HITs.

17 stars 2 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Types of paths in computation rule for paths

#12 andrejbauer opened 7 years ago
2
Colimit via sigma and coequalizers

#11 nmvdw closed 7 years ago
1
Some typos in the first part

#10 co-dan closed 7 years ago
0
Where do we rely on the boudned nesting of constructors

#9 andrejbauer opened 7 years ago
4
Why separate the recursive and non-recursive constructors?

#8 andrejbauer opened 7 years ago
1
Explaining the construction

#7 andrejbauer opened 7 years ago
14
Getting rid of parameters

#6 andrejbauer opened 7 years ago
3
I am confused

#5 andrejbauer opened 7 years ago
4
Lemma 13

#4 nmvdw closed 7 years ago
1
Abstract

#3 nmvdw closed 7 years ago
0
Definition of a constructor term over a given `c`

#2 andrejbauer closed 7 years ago
1
Colimits in HoTT

#1 andrejbauer closed 7 years ago
2