Я пытаюсь выучить Cubical Agda. Я до сих пор не совсем понимаю, как перенос может изменить форму программы. Например, если я правильно понимаю, если у нас есть доказательство того, что Nat == Bits и мы используем transp на zero : Nat, мы получим bit0 : Bits. Это не похоже на subst для типа идентификатора, который изменяет два идентичных значения в типе, но сохраняет сам типизированный термин нетронутым. Я понимаю, что в некотором смысле доказательства равенства Cubical Agda несут информацию о том, как go от одного конца до другого, но я не уверен, как это работает точно. Чтобы лучше понять, что именно делает transp, я думаю, было бы полезно несколько конкретных примеров. Какие простые, конкретные примеры использования transp и его до / после обычных форм?