---

Step * of Lemma A-face-compatible-image

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

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. K : Cname List
5. f : name-morph(I;K)
6. alpha : X(I)
7. x : nameset(I)
8. i : ℕ2
9. f2 : A((x:=i)(alpha))
10. y : nameset(I)
11. i1 : ℕ2
12. f4 : A((y:=i1)(alpha))
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha)))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
⊢ ((f2 (x:=i)(alpha) f) (f x:=i)(f(alpha)) (f y:=i1))
= ((f4 (y:=i1)(alpha) f) (f y:=i1)(f(alpha)) (f x:=i))
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))

---

Latex:

---

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


By

---

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

---

Home Index