search

nmvdw / Three-HITs

All higher inductive types can be obtained from three simple HITs.
17 stars 2 forks source link

Colimit via sigma and coequalizers #11

Closed nmvdw closed 7 years ago

nmvdw commented 7 years ago

Conjecture: Given are F : N -> Type and f : Π n : N, F n -> F(n+1). Define C = Σ n : N, F n. Note we have a map i : Π n : N, F n -> C sending x : F n to (n, x). Define g_1 : Σ n : N, F n -> F n to be Σ n : N, (i (n+1)) o f n and g_2 : Σ n : N, F n -> F n to be Σ n : N, i n. Then hocolim F f is isomorphic to the coequalizer of g_1 and g_2.

nmvdw commented 7 years ago

Showed that there are maps between them which are inverses.