<p>In HoTT with univalence, it is indeed provable that <code>list1 A</code> is equal to <code>list2 A</code> for all <code>A</code>. Given a proof <code>p : list1 A = list2 A</code>, transport (or <code>subst</code>) gives you <code>P (list1 A) -&gt; P (list2 A)</code> for any <code>P</code>. In cubical type theories, such transporting may also compute as expected. To my knowledge, cubical type theory (<a href="https://hal.inria.fr/hal-01378906/document" rel="nofollow noreferrer">CCHM</a> or <a href="https://arxiv.org/pdf/1712.01800.pdf" rel="nofollow noreferrer">cartesian</a>) is the only setting where this currently works. <a href="https://github.com/mortberg/cubicaltt" rel="nofollow noreferrer"><code>cubicaltt</code></a> is the most usable (but still not really practical) implementation.</p>
Is there a type theory in which the equivalence of identically shaped inductive datatypes is representable?
<p>Say I have two inductively defined datatypes:</p>

<pre><code>Inductive list1 (A : Type) : Type :=
 | nil1 : list1 A
 | cons1 : A -&gt; list1 A -&gt; list1 A.
</code></pre>

<p>and</p>

<pre><code>Inductive list2 (A : Type) : Type :=
 | nil2 : list2 A
 | cons2 : A -&gt; list2 A -&gt; list2 A.
</code></pre>

<p>For any <code>P (list1 a)</code> I should be able to construct a <code>P (list2 a)</code>, by applying the exact same method I used to construct <code>P (list1 a)</code> except replacing <code>nil1</code> with <code>nil2</code>, <code>list1</code> with <code>list2</code> and <code>cons1</code> with <code>cons2</code>. Similarly, any function that takes <code>list1 a</code> as a parameter could be extended to take a <code>list2 a</code>.</p>

<p>Is there a type system that allows me to speak of two datatypes having the same shape in this manner (having identically shaped constructors), and prove <code>P (list1 a) -&gt; P (list2 a)</code>? For instance, is this something that univalence, HOTT, or a cubical/observational type system allows? It might also allow defining functions like <code>reverse: list_like a -&gt; list_like a</code> that accept both <code>list1</code>s and <code>list2</code>s as parameters.</p>