---

Step * 1 1 1 2 1 of Lemma cubical-refl_wf

.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. alpha : X(I)
8. v : {x:Cname| ¬(x ∈ I)} 
9. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
10. v1 : {x:Cname| ¬(x ∈ J)} 
11. fresh-cname(J) = v1 ∈ {x:Cname| ¬(x ∈ J)} 
12. (((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1]) iota(v1)(f(alpha)) rename-one-name(v1;v1))
= ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
∈ A(iota(v1)(f(alpha)))
⊢ (a J f(alpha) f(alpha) iota(v1)) = ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1]) ∈ A(iota(v1)(f(alpha)))
BY
{ TACTIC:((InstLemma `cubical-type-ap-morph-comp` 
           [⌜X⌝;⌜A⌝;⌜I⌝;⌜[v / I]⌝;⌜[v1 / J]⌝;⌜iota(v)⌝;⌜f[v:=v1]⌝;⌜alpha⌝;⌜a I alpha⌝]⋅
           THENA Auto
           )
          THEN Symmetry
          THEN NthHypEq (-1)
          THEN EqCD
          THEN Auto) }

1
.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. alpha : X(I)
8. v : {x:Cname| ¬(x ∈ I)} 
9. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
10. v1 : {x:Cname| ¬(x ∈ J)} 
11. fresh-cname(J) = v1 ∈ {x:Cname| ¬(x ∈ J)} 
12. (((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1]) iota(v1)(f(alpha)) rename-one-name(v1;v1))
= ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
∈ A(iota(v1)(f(alpha)))
13. ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
= (a I alpha alpha (iota(v) o f[v:=v1]))
∈ A((iota(v) o f[v:=v1])(alpha))
⊢ (a J f(alpha) f(alpha) iota(v1)) = (a I alpha alpha (iota(v) o f[v:=v1])) ∈ A(iota(v1)(f(alpha)))

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  I  :  Cname  List
5.  J  :  Cname  List
6.  f  :  name-morph(I;J)
7.  alpha  :  X(I)
8.  v  :  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 
9.  fresh-cname(I)  =  v
10.  v1  :  \{x:Cname|  \mneg{}(x  \mmember{}  J)\} 
11.  fresh-cname(J)  =  v1
12.  (((a  I  alpha  alpha  iota(v))  iota(v)(alpha)  f[v:=v1])  iota(v1)(f(alpha))  rename-one-name(v1;v1))
=  ((a  I  alpha  alpha  iota(v))  iota(v)(alpha)  f[v:=v1])
\mvdash{}  (a  J  f(alpha)  f(alpha)  iota(v1))  =  ((a  I  alpha  alpha  iota(v))  iota(v)(alpha)  f[v:=v1])


By

---

Latex:
TACTIC:((InstLemma  `cubical-type-ap-morph-comp` 
                  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}[v  /  I]\mkleeneclose{};\mkleeneopen{}[v1  /  J]\mkleeneclose{};\mkleeneopen{}iota(v)\mkleeneclose{};\mkleeneopen{}f[v:=v1]\mkleeneclose{};\mkleeneopen{}alpha\mkleeneclose{};\mkleeneopen{}a  I  alpha\mkleeneclose{}]\mcdot{}
                  THENA  Auto
                  )
                THEN  Symmetry
                THEN  NthHypEq  (-1)
                THEN  EqCD
                THEN  Auto)

---

Home Index