Questions tagged [higher-inductive-types]

Higher inductive types (HITs) are a generalization of inductive types to higher dimensions. HITs are generated inductively by elements of itself and its iterated identity types. (from nLab)

Filter by
Sorted by
Tagged with
3 votes
1 answer

Using induction to define Indexed family of HITs in agda

I am looking to define a family of HITs parametrized by $\mathbb{N}$. I want $(-)$-glob : $\mathbb{N} \to Type$, so that $n$-glob is the n-dimensional glob. I know how to construct the n-$glob$ by ...
IsAdisplayName's user avatar
9 votes
1 answer

Case splitting with quotient types in Cubical Agda

I'm getting started with Cubcal Agda and I'm quite confused. I've got a HIT A defined, with a path constructor eq returning <...
Joey Eremondi's user avatar
6 votes
2 answers

Can I use if_then_else on indexed paths in HITs?

I want to define a function out of an indexed higher inductive type, and am running into some problems. Here is a somewhat contrived minimal example of what I'm doing: ...
Åsmund Kløvstad's user avatar