---

Step * of Lemma face-compatible-image

∀X:CubicalSet. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀fc1,fc2:I-face(X;I).
  ((↑isname(f (fst(fc1))))
  ⇒ (↑isname(f (fst(fc2))))
  ⇒ face-compatible(X;I;fc1;fc2)
  ⇒ face-compatible(X;K;face-image(X;I;K;f;fc1);face-image(X;I;K;f;fc2)))
BY
{ (Intros
   THEN RepeatFor 2 (D -5)
   THEN RepeatFor 2 (D -4)
   THEN RepUR ``face-compatible`` -1
   THEN RepUR ``face-compatible face-image`` 0
   THEN All Reduce
   THEN RenameVar `y' (-6)
   THEN ∀h:hyp. (FLemma `assert-isname` [h] THENA Auto) 
   THEN (D 0 THENA Auto)
   THEN (Decide x = y ∈ Cname THENA Auto)) }

1
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : nameset(I)
6. f2 : ℕ2
7. f3 : X(I-[x])
8. y : nameset(I)
9. f5 : ℕ2
10. f6 : X(I-[y])
11. ↑isname(f x)
12. ↑isname(f y)
13. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
14. f y ∈ nameset(K)
15. f x ∈ nameset(K)
16. ¬((f x) = (f y) ∈ Cname)
17. x = y ∈ Cname
⊢ (f y:=f5)(f(f3)) = (f x:=f2)(f(f6)) ∈ X(K-[f x; f y])

2
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : nameset(I)
6. f2 : ℕ2
7. f3 : X(I-[x])
8. y : nameset(I)
9. f5 : ℕ2
10. f6 : X(I-[y])
11. ↑isname(f x)
12. ↑isname(f y)
13. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
14. f y ∈ nameset(K)
15. f x ∈ nameset(K)
16. ¬((f x) = (f y) ∈ Cname)
17. ¬(x = y ∈ Cname)
⊢ (f y:=f5)(f(f3)) = (f x:=f2)(f(f6)) ∈ X(K-[f x; f y])

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}fc1,fc2:I-face(X;I).
    ((\muparrow{}isname(f  (fst(fc1))))
    {}\mRightarrow{}  (\muparrow{}isname(f  (fst(fc2))))
    {}\mRightarrow{}  face-compatible(X;I;fc1;fc2)
    {}\mRightarrow{}  face-compatible(X;K;face-image(X;I;K;f;fc1);face-image(X;I;K;f;fc2)))


By

---

Latex:
(Intros
  THEN  RepeatFor  2  (D  -5)
  THEN  RepeatFor  2  (D  -4)
  THEN  RepUR  ``face-compatible``  -1
  THEN  RepUR  ``face-compatible  face-image``  0
  THEN  All  Reduce
  THEN  RenameVar  `y'  (-6)
  THEN  \mforall{}h:hyp.  (FLemma  `assert-isname`  [h]  THENA  Auto) 
  THEN  (D  0  THENA  Auto)
  THEN  (Decide  x  =  y  THENA  Auto))

---

Home Index