---

Step * 1 of Lemma A-face-compatible-image


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)))
BY
{ TACTIC:((Assert ⌜¬(x = y ∈ Cname)⌝⋅ THENA (ParallelLast THEN HypSubst' (-1) 0 THEN Auto))
          THEN DVar `x'
          THEN DVar `y'
          THEN (Assert y ∈ nameset(I-[x]) BY
                      (DVar `y' THEN MemTypeCD THEN Try (RepeatFor 2 ((RW ListC 0 THENA Auto))) THEN Auto))
          THEN (Assert x ∈ nameset(I-[y]) BY
                      (DVar `x' THEN MemTypeCD THEN Try (RepeatFor 2 ((RW ListC 0 THENA Auto))) THEN Auto))
          THEN (Assert ⌜f ∈ name-morph(I-[x];K-[f x])⌝⋅ THENA (BLemma `name-morph_subtype_remove1` ⋅ THEN Auto))
          THEN (Assert ⌜f ∈ name-morph(I-[y];K-[f y])⌝⋅ THENA (BLemma `name-morph_subtype_remove1` ⋅ 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 : Cname
8. (x ∈ I)
9. i : ℕ2
10. f2 : A((x:=i)(alpha))
11. y : Cname
12. (y ∈ I)
13. i1 : ℕ2
14. f4 : A((y:=i1)(alpha))
15. ↑isname(f x)
16. ↑isname(f y)
17. (¬(x = y ∈ Cname)) ⇒ ((f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha)))
18. f y ∈ nameset(K)
19. f x ∈ nameset(K)
20. ¬((f x) = (f y) ∈ Cname)
21. ¬(x = y ∈ Cname)
22. y ∈ nameset(I-[x])
23. x ∈ nameset(I-[y])
24. f ∈ name-morph(I-[x];K-[f x])
25. f ∈ name-morph(I-[y];K-[f y])
⊢ ((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:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  I  :  Cname  List
4.  K  :  Cname  List
5.  f  :  name-morph(I;K)
6.  alpha  :  X(I)
7.  x  :  nameset(I)
8.  i  :  \mBbbN{}2
9.  f2  :  A((x:=i)(alpha))
10.  y  :  nameset(I)
11.  i1  :  \mBbbN{}2
12.  f4  :  A((y:=i1)(alpha))
13.  \muparrow{}isname(f  x)
14.  \muparrow{}isname(f  y)
15.  (\mneg{}(x  =  y))  {}\mRightarrow{}  ((f2  (x:=i)(alpha)  (y:=i1))  =  (f4  (y:=i1)(alpha)  (x:=i)))
16.  f  y  \mmember{}  nameset(K)
17.  f  x  \mmember{}  nameset(K)
18.  \mneg{}((f  x)  =  (f  y))
\mvdash{}  ((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))


By

---

Latex:
TACTIC:((Assert  \mkleeneopen{}\mneg{}(x  =  y)\mkleeneclose{}\mcdot{}  THENA  (ParallelLast  THEN  HypSubst'  (-1)  0  THEN  Auto))
                THEN  DVar  `x'
                THEN  DVar  `y'
                THEN  (Assert  y  \mmember{}  nameset(I-[x])  BY
                                        (DVar  `y'
                                          THEN  MemTypeCD
                                          THEN  Try  (RepeatFor  2  ((RW  ListC  0  THENA  Auto)))
                                          THEN  Auto))
                THEN  (Assert  x  \mmember{}  nameset(I-[y])  BY
                                        (DVar  `x'
                                          THEN  MemTypeCD
                                          THEN  Try  (RepeatFor  2  ((RW  ListC  0  THENA  Auto)))
                                          THEN  Auto))
                THEN  (Assert  \mkleeneopen{}f  \mmember{}  name-morph(I-[x];K-[f  x])\mkleeneclose{}\mcdot{}
                            THENA  (BLemma  `name-morph\_subtype\_remove1`  \mcdot{}  THEN  Auto)
                            )
                THEN  (Assert  \mkleeneopen{}f  \mmember{}  name-morph(I-[y];K-[f  y])\mkleeneclose{}\mcdot{}
                            THENA  (BLemma  `name-morph\_subtype\_remove1`  \mcdot{}  THEN  Auto)
                            ))

---

Home Index