Lemma starcomp {S: UU} {X Y Z: sUU S} (f: Y s→ Z) (g: X s→ Y) (l: list S) (x: X⋆ l) : (f s∘ g)⋆⋆ _ x = f⋆⋆ _ (g⋆⋆ _ x). Proof. unfold starfun. apply pathsinv0. apply h1map_compose. Defined.
Require Import UniMath.Foundations.All.