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

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?

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.