Sou um homem simples que realmente não entende todos os detalhes do Cubical Agda. Tentei ler seus documentos e HoTT, e parei de acompanhar o que estava acontecendo bem rápido.
O que espero especificamente é um exemplo de como escrever uma operação simples para um tipo indutivo mais alto, de preferência sem bibliotecas fora de Cubical.Core.Everything.
Para um exemplo específico, vamos considerar os inteiros como um quociente sobre pares de naturais:
data N : Set where
0N : N
suc : N -> N
_+N_ : N -> N -> N
0N +N n = n
suc m +N n = suc (m +N n)
data Z : Set where
zpair : N -> N -> N
zeq : (a b c d : N) -> (a +N d) === (b +N c) -> zpair a b === zpair c d
_+Z_ : Z -> Z -> Z
zpair a b + zpair c d = zpair (a +N c) (b +N d)
zeq a b c d ad=bc i + zeq e f g h eh=fg j = ???
Eu posso e tenho trabalhado meu caminho através de eg zpair + zeqe vice-versa, onde há um i : Ie eu posso simplesmente construir um caminho apropriado e aplicá-lo a i. Eu não entendo o que fazer quando eu tenho i j : Ie estou combinando os pontos nos caminhos juntos, e em particular não parece que eu posso simplesmente juntá-los, nem vejo uma composição óbvia ou um valor em Iaplicá-lo.
Uma resposta satisfatória preencheria o ???, assumindo quaisquer lemas convenientes necessários _+N_e usando a API de raciocínio equacional conforme necessário.
Procurei definições de números inteiros no Agda que os definem como um quociente, mas não consigo encontrar onde esse tipo de operação é definido.