Step
*
1
1
1
2
1
1
1
of Lemma
cubical-refl_wf
1. X : CubicalSet
2. A1 : I:(Cname List) ⟶ X(I) ⟶ Type
3. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
4. (∀I:Cname List. ∀a:X(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a))))
5. a : I:(Cname List) ⟶ a:X(I) ⟶ (A1 I a)
6. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a@0:X(I). ((A2 I J f a@0 (a I a@0)) = (a J f(a@0)) ∈ (A1 J f(a@0)))
7. I : Cname List
8. J : Cname List
9. f : name-morph(I;J)
10. alpha : X(I)
11. v : {x:Cname| ¬(x ∈ I)}
12. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)}
13. v1 : {x:Cname| ¬(x ∈ J)}
14. fresh-cname(J) = v1 ∈ {x:Cname| ¬(x ∈ J)}
15. (((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])
∈ <A1, A2>(iota(v1)(f(alpha)))
16. ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
= (a I alpha alpha (iota(v) o f[v:=v1]))
∈ <A1, A2>((iota(v) o f[v:=v1])(alpha))
17. X ⊢ <A1, A2>
⊢ (A2 J [v1 / J] iota(v1) f(alpha) (a J f(alpha)))
= (A2 I [v1 / J] (iota(v) o f[v:=v1]) alpha (a I alpha))
∈ <A1, A2>(iota(v1)(f(alpha)))
BY
{ TACTIC:(RWO "6" 0 THENA Auto) }
1
1. X : CubicalSet
2. A1 : I:(Cname List) ⟶ X(I) ⟶ Type
3. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
4. (∀I:Cname List. ∀a:X(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a))))
5. a : I:(Cname List) ⟶ a:X(I) ⟶ (A1 I a)
6. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a@0:X(I). ((A2 I J f a@0 (a I a@0)) = (a J f(a@0)) ∈ (A1 J f(a@0)))
7. I : Cname List
8. J : Cname List
9. f : name-morph(I;J)
10. alpha : X(I)
11. v : {x:Cname| ¬(x ∈ I)}
12. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)}
13. v1 : {x:Cname| ¬(x ∈ J)}
14. fresh-cname(J) = v1 ∈ {x:Cname| ¬(x ∈ J)}
15. (((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])
∈ <A1, A2>(iota(v1)(f(alpha)))
16. ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
= (a I alpha alpha (iota(v) o f[v:=v1]))
∈ <A1, A2>((iota(v) o f[v:=v1])(alpha))
17. X ⊢ <A1, A2>
⊢ (a [v1 / J] iota(v1)(f(alpha))) = (a [v1 / J] (iota(v) o f[v:=v1])(alpha)) ∈ <A1, A2>(iota(v1)(f(alpha)))
Latex:
Latex:
1. X : CubicalSet
2. A1 : I:(Cname List) {}\mrightarrow{} X(I) {}\mrightarrow{} Type
3. A2 : I:(Cname List) {}\mrightarrow{} J:(Cname List) {}\mrightarrow{} f:name-morph(I;J) {}\mrightarrow{} a:X(I) {}\mrightarrow{} (A1 I a) {}\mrightarrow{} (A1 J f(a))
4. (\mforall{}I:Cname List. \mforall{}a:X(I). \mforall{}u:A1 I a. ((A2 I I 1 a u) = u))
\mwedge{} (\mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K). \mforall{}a:X(I). \mforall{}u:A1 I a.
((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u))))
5. a : I:(Cname List) {}\mrightarrow{} a:X(I) {}\mrightarrow{} (A1 I a)
6. \mforall{}I,J:Cname List. \mforall{}f:name-morph(I;J). \mforall{}a@0:X(I). ((A2 I J f a@0 (a I a@0)) = (a J f(a@0)))
7. I : Cname List
8. J : Cname List
9. f : name-morph(I;J)
10. alpha : X(I)
11. v : \{x:Cname| \mneg{}(x \mmember{} I)\}
12. fresh-cname(I) = v
13. v1 : \{x:Cname| \mneg{}(x \mmember{} J)\}
14. fresh-cname(J) = v1
15. (((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])
16. ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1]) = (a I alpha alpha (iota(v) o f[v:=v1]))
17. X \mvdash{} <A1, A2>
\mvdash{} (A2 J [v1 / J] iota(v1) f(alpha) (a J f(alpha)))
= (A2 I [v1 / J] (iota(v) o f[v:=v1]) alpha (a I alpha))
By
Latex:
TACTIC:(RWO "6" 0 THENA Auto)
Home
Index