How does substitution on partial elements/systems (in terms of cubical) work?

Question

Let h = hcomp (λ j → λ { (i = i1) → x }) u, using Cubical Agda syntax. The equivalent cubicaltt syntax is hcomp A u [ (i = 1) -> x ].

Consider $h [i ↦ l ∨ k]$, is it hcomp (λ j → λ { (l = i1) → x; (k = i1) → x }) u? In other words, does substitution on partial elements create more clauses? Do they share the same clause body?

Answer 1

In other words, does substitution on partial elements create more clauses? Do they share the same clause body?

Yes, you may check both in Cubical Agda:

{-# OPTIONS --cubical #-}

open import Agda.Primitive.Cubical public
  renaming ( primIMin       to _∧_
           ; primIMax       to _∨_
           ; primINeg       to -_)
open import Agda.Primitive public

f : (i : I) → Partial i Set₁
f i = λ { (i = i1) → Set }

g : (i j k : I) → Partial ((i ∧ - j) ∨ k) Set₁
g i j k = f ((i ∧ - j) ∨ k)

h : (i j k : I) → Partial ((i ∧ - j) ∨ k) Set₁
h i j k = λ { (i = i1) (j = i0) → Set; (k = i1) → Set  }

data Eq {A : Setω} : A → A → Setω where
  refl : {a : A} → Eq a a

test : (i j k : I) → Eq (g i j k) (h i j k)
test i j k = refl

Also note that substitutions may produce clauses like $(0 = 1)$, which may be discarded, and like $(1 = 1)$, which allow to discard all other clauses.