<div dir="ltr"><div>Hi,</div><div><br></div><div>when constructing the different unary, binary, ternary... types that represent the natural numbers it seems that both the constructors and the increment operator follow a pattern.</div><div><br></div><div><a href="https://gist.github.com/pnlph/3f6aca8dea4ba570abcb461b37ae14cb">https://gist.github.com/pnlph/3f6aca8dea4ba570abcb461b37ae14cb</a></div><div><br></div><div>Is it possible or makes sense defining this pattern in Agda as a type of natural numbers representations, say Nr, indexed on the natural numbers themselves so that Nr 1 = N, Nr 2 = Bin, Nr 3 = Ter, ..., Nr 10 = Dec,...?<br></div><div><br></div><div>best, herminie</div></div>