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 induction on $n$. The problem I am running into is that I do not know how to use induction on $\mathbb{N}$ in the middle of the definition of a HIT. For example, I have the code

data _-glob (n : ℕ) : Type where

and I want to case on $n$ so that I may specify what $n:\equiv 0$ is and what $n:\equiv suc (n)$ is, given what $n$ is. But, I cannot simply write

data _-glob (n : ℕ) : Type where
 H : ?

and then case on $n$. Does anyone know how to use induction in the middle of such a definition?

EDIT: Here is my (quite literal) "black board" inductive definition of _-glob. Its pretty messy and I'm sure there are more elgant ways to define it but this is what I'm trying to turn into agda code:

0-glob where

 G0 : 0-glob

1-glob where

 in : 0-glob -> 1-glob

 G0_2 : 1-glob

 G1 : in(G0) = G0_2

(n+2)-glob where

 in : (n+1)-glob -> (n+2)-glob

 G(n+1)_2 : in(in(Gn)) = in(Gn_2)

 G(n+2) : in(G(n+1)) = G(n+1)_2

Now, I'm pretty sure this give me what I want. 1-glob is equivalent to the interval. 2-glob contains a copy of 1-glob, via the constructor "in". But, 2-glob contains and additional path parallel to the preexisting one. And it contains a two path between these 1 paths. But, to actually define this as a HIT (in one go), i would need to case on n to specify the constructors.

  • $\begingroup$ oh, thats a typo. I think it should read in(in(Gn)) = in(Gn_2). I intended Gn to be the filler of the n-glob. Then, to create the n+1 glob, copy the n-glob with in and add a path Gn_2 which is parallel to in(Gn). Then, add G(n+1) : in (Gn) = Gn_2. So, in(Gn) and Gn_2 should be parallel n globs living in the type of the n+1 glob, with filler G(n+1). To create the (n+2)-glob, copy again with in. So we should have ```in(Gn+1) : in(in(Gn))=in(Gn_2). Add in a parallel path G(n+1)_2 and a filler G(n+2). $\endgroup$ Commented Jun 3, 2022 at 6:29
  • $\begingroup$ @Trebor This was more complicated than I hoped. I'm probably going to end up asking my advisor about this. Thank you for the help, though! $\endgroup$ Commented Jun 3, 2022 at 6:32
  • $\begingroup$ G(n+2) : in(G(n+1)) = G(n+1)_2 doesn't seem well-typed to me: the left-hand side is a point, the right-hand side is a path. $\endgroup$
    – Cactus
    Commented Jul 23, 2022 at 4:31
  • $\begingroup$ @Cactus the rhs is a path type. A point is just a term in a type. $\endgroup$ Commented Jul 23, 2022 at 15:34
  • 1
    $\begingroup$ @Cactus ah, I think this is the confusion. $G(n+1)$ is not meant to be a term of type $(n+1)-glob$. Rather, I intend it to be a path as follows $G(n+1) : in(Gn) = Gn_2$. In this case, I use the shorthand of in(G(n+1)) for the higher dimensional action of paths of in on G(n+1). Anyways, learned a way to formalize this that avoids all this mess. Thank you though! $\endgroup$ Commented Jul 25, 2022 at 4:16

1 Answer 1



data _-glob : ℕ -> Type where

Now you can just do something like H : blabla -> zero -glob. Warning: This is called an indexed inductive family, and cubical Agda still has some unimplemented functionalities about this feature yet. You might want to look at the standard library (not the cubical library) on the Fin type to see an example.

Another way to do it is as a recursive type. You first define zero-glob separately. Then you define suc-glob (n-glob : Type) : Type. Now take

_-glob : (n : ℕ) -> Type
zero -glob = zero-glob
(suc n) -glob = suc-glob (n -glob)
  • $\begingroup$ I'm not sure I understand you first method. How would this allow me to case on n? $\endgroup$ Commented Jun 3, 2022 at 3:38
  • $\begingroup$ @IsAdisplayName just write ordinary constructors, but now you can choose to let the resulting type be zero -glob or (suc ?) -glob now. $\endgroup$
    – Trebor
    Commented Jun 3, 2022 at 3:43
  • $\begingroup$ Hm, I don't really understand how that works. I guess I'll track down the type FIn in the standard library $\endgroup$ Commented Jun 3, 2022 at 4:02
  • $\begingroup$ @IsAdisplayName Can you write what you would suppose you _-glob to be? I can show you how to do it with that concrete example. $\endgroup$
    – Trebor
    Commented Jun 3, 2022 at 4:06
  • $\begingroup$ okay, I'll edit the post with that. I'm only going to be able to give _-glob informally, i.e., basically what I have on my blackboard. Thank you for the help! $\endgroup$ Commented Jun 3, 2022 at 4:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.