---

Step * 1 of Lemma composition-function-subset

.....subterm..... T:t
1:n
1. Y : CubicalSet{j}
2. X : CubicalSet{j}
3. sub_cubical_set{j:l}(Y; X)
4. B : {X ⊢ _}
5. x : composition-function{j:l,i:l}(X;B)
⊢ x ∈ composition-function{j:l,i:l}(Y;B)
BY
{ (All (Unfold `composition-function`)
   THEN RepeatFor 5 ((FunExt THENA Auto))
   THEN RepeatFor 4 ((MemCD THEN Try (Trivial)))
   THEN Try ((MemCD THEN Trivial))) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  Y  :  CubicalSet\{j\}
2.  X  :  CubicalSet\{j\}
3.  sub\_cubical\_set\{j:l\}(Y;  X)
4.  B  :  \{X  \mvdash{}  \_\}
5.  x  :  composition-function\{j:l,i:l\}(X;B)
\mvdash{}  x  \mmember{}  composition-function\{j:l,i:l\}(Y;B)


By

---

Latex:
(All  (Unfold  `composition-function`)
  THEN  RepeatFor  5  ((FunExt  THENA  Auto))
  THEN  RepeatFor  4  ((MemCD  THEN  Try  (Trivial)))
  THEN  Try  ((MemCD  THEN  Trivial)))

---

Home Index