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.
A abordagem usual para isso é adicionar um construtor de truncamento de conjunto , como
Isso garante que você possa preencher qualquer quadrado em
Z, por exemplo, usandoisSet→SquareP. (Observe queisSet Zse desdobra em algo que tem o formato correto para ser usado como o tipo de um construtor superior.)Você pode ver essa abordagem em ação na biblioteca cúbica aqui : observe que
ℤé definido como o quociente deℕ × ℕpor alguma relaçãorel, onde quocientes são definidos como um tipo indutivo superior com umsquash/construtor que força o quociente a ser um conjunto.Para outra abordagem que não requer truncamento, veja o 1lab : aqui restringimos o construtor de caminho para relacionar pares da forma (x, y) e (x + 1, y + 1). Você pode se convencer de que isso não introduz nenhum loop não trivial, de modo que o HIT resultante é um conjunto (comece desenhando ℕ × ℕ como uma grade, então desenhe uma linha entre cada par de pontos que está relacionado por um caminho; você vê como isso difere da abordagem anterior?).
Uma vez que isso esteja em vigor, é comum abstrair os detalhes da implementação definindo um princípio de recursão para os inteiros, que muitas vezes pode ter uma forma mais simples se assumirmos que o tipo de destino é de nível h inferior (neste caso, um conjunto).