Step
*
of Lemma
csm-transprt-fun
No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 +⊢ Compositon(A)]. ∀[H:j⊢]. ∀[s:H j⟶ Gamma].
((transprt-fun(Gamma;A;cA))s = transprt-fun(H;(A)s+;(cA)s+) ∈ {H ⊢ _:(((A)s+)[0(𝕀)] ⟶ ((A)s+)[1(𝕀)])})
BY
{ (Intros
THEN (InstLemma `csm+_wf` [⌜Gamma⌝;⌜H⌝;⌜𝕀⌝;⌜s⌝]⋅ THENA Auto)
THEN (RWO "csm-interval-type" (-1) THENA Auto)
THEN (Assert {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s} = {H ⊢ _:(((A)s+)[0(𝕀)] ⟶ ((A)s+)[1(𝕀)])} ∈ 𝕌{[i' | j']} BY
(EqCDA THEN (RWO "csm-cubical-fun" 0 THENA Auto) THEN EqCDA THEN CsmTypeSq THEN Auto))
THEN (Assert ⌜(transprt-fun(Gamma;A;cA))s = transprt-fun(H;(A)s+;(cA)s+) ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}⌝⋅
THENM (InferEqualType THEN Auto)
)
THEN (Assert (transprt-fun(Gamma;A;cA))s ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s} BY
Auto)
THEN (Assert transprt-fun(H;(A)s+;(cA)s+) ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s} BY
(InferEqualType THEN Auto))
THEN All (Unfold `transprt-fun`)
THEN (InstLemma `cubical-fun-as-cubical-pi` [⌜H⌝;⌜((A)s+)[0(𝕀)]⌝;⌜((A)s+)[1(𝕀)]⌝]⋅ THENA Auto)
THEN (InstLemma `cubical-fun-as-cubical-pi` [⌜Gamma⌝;⌜(A)[0(𝕀)]⌝;⌜(A)[1(𝕀)]⌝]⋅ THENA Auto)
THEN (InstLemma `csm-cubical-lambda` [⌜Gamma⌝;⌜(A)[0(𝕀)]⌝;⌜((A)[1(𝕀)])p⌝]⋅ THENA Auto)
THEN InstHyp [⌜transprt(Gamma.(A)[0(𝕀)];(cA)p+;q)⌝;⌜H⌝;⌜s⌝] (-1)⋅
THEN Try (Trivial)) }
1
.....wf.....
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 +⊢ Compositon(A)
4. H : CubicalSet{j}
5. s : H j⟶ Gamma
6. s+ ∈ H.𝕀 ij⟶ Gamma.𝕀
7. {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s} = {H ⊢ _:(((A)s+)[0(𝕀)] ⟶ ((A)s+)[1(𝕀)])} ∈ 𝕌{[i' | j']}
8. ((λtransprt(Gamma.(A)[0(𝕀)];(cA)p+;q)))s ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
9. (λtransprt(H.((A)s+)[0(𝕀)];((cA)s+)p+;q)) ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
10. (H ⊢ ((A)s+)[0(𝕀)] ⟶ ((A)s+)[1(𝕀)]) = H ⊢ Π((A)s+)[0(𝕀)] (((A)s+)[1(𝕀)])p ∈ {H ⊢ _}
11. (Gamma ⊢ (A)[0(𝕀)] ⟶ (A)[1(𝕀)]) = Gamma ⊢ Π(A)[0(𝕀)] ((A)[1(𝕀)])p ∈ {Gamma ⊢ _}
12. ∀[b:{Gamma.(A)[0(𝕀)] ⊢ _:((A)[1(𝕀)])p}]. ∀[H:j⊢]. ∀[s:H j⟶ Gamma].
(((λb))s = (λ(b)s+) ∈ {H ⊢ _:(Π(A)[0(𝕀)] ((A)[1(𝕀)])p)s})
⊢ transprt(Gamma.(A)[0(𝕀)];(cA)p+;q) ∈ {Gamma.(A)[0(𝕀)] ⊢ _:((A)[1(𝕀)])p}
2
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 +⊢ Compositon(A)
4. H : CubicalSet{j}
5. s : H j⟶ Gamma
6. s+ ∈ H.𝕀 ij⟶ Gamma.𝕀
7. {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s} = {H ⊢ _:(((A)s+)[0(𝕀)] ⟶ ((A)s+)[1(𝕀)])} ∈ 𝕌{[i' | j']}
8. ((λtransprt(Gamma.(A)[0(𝕀)];(cA)p+;q)))s ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
9. (λtransprt(H.((A)s+)[0(𝕀)];((cA)s+)p+;q)) ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
10. (H ⊢ ((A)s+)[0(𝕀)] ⟶ ((A)s+)[1(𝕀)]) = H ⊢ Π((A)s+)[0(𝕀)] (((A)s+)[1(𝕀)])p ∈ {H ⊢ _}
11. (Gamma ⊢ (A)[0(𝕀)] ⟶ (A)[1(𝕀)]) = Gamma ⊢ Π(A)[0(𝕀)] ((A)[1(𝕀)])p ∈ {Gamma ⊢ _}
12. ∀[b:{Gamma.(A)[0(𝕀)] ⊢ _:((A)[1(𝕀)])p}]. ∀[H:j⊢]. ∀[s:H j⟶ Gamma].
(((λb))s = (λ(b)s+) ∈ {H ⊢ _:(Π(A)[0(𝕀)] ((A)[1(𝕀)])p)s})
13. ((λtransprt(Gamma.(A)[0(𝕀)];(cA)p+;q)))s
= (λ(transprt(Gamma.(A)[0(𝕀)];(cA)p+;q))s+)
∈ {H ⊢ _:(Π(A)[0(𝕀)] ((A)[1(𝕀)])p)s}
⊢ ((λtransprt(Gamma.(A)[0(𝕀)];(cA)p+;q)))s
= (λtransprt(H.((A)s+)[0(𝕀)];((cA)s+)p+;q))
∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
Latex:
Latex:
No Annotations
\mforall{}[Gamma:j\mvdash{}]. \mforall{}[A:\{Gamma.\mBbbI{} \mvdash{} \_\}]. \mforall{}[cA:Gamma.\mBbbI{} +\mvdash{} Compositon(A)]. \mforall{}[H:j\mvdash{}]. \mforall{}[s:H j{}\mrightarrow{} Gamma].
((transprt-fun(Gamma;A;cA))s = transprt-fun(H;(A)s+;(cA)s+))
By
Latex:
(Intros
THEN (InstLemma `csm+\_wf` [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (RWO "csm-interval-type" (-1) THENA Auto)
THEN (Assert \{H \mvdash{} \_:(((A)[0(\mBbbI{})] {}\mrightarrow{} (A)[1(\mBbbI{})]))s\} = \{H \mvdash{} \_:(((A)s+)[0(\mBbbI{})] {}\mrightarrow{} ((A)s+)[1(\mBbbI{})])\} BY
(EqCDA THEN (RWO "csm-cubical-fun" 0 THENA Auto) THEN EqCDA THEN CsmTypeSq THEN Auto))
THEN (Assert \mkleeneopen{}(transprt-fun(Gamma;A;cA))s = transprt-fun(H;(A)s+;(cA)s+)\mkleeneclose{}\mcdot{}
THENM (InferEqualType THEN Auto)
)
THEN (Assert (transprt-fun(Gamma;A;cA))s \mmember{} \{H \mvdash{} \_:(((A)[0(\mBbbI{})] {}\mrightarrow{} (A)[1(\mBbbI{})]))s\} BY
Auto)
THEN (Assert transprt-fun(H;(A)s+;(cA)s+) \mmember{} \{H \mvdash{} \_:(((A)[0(\mBbbI{})] {}\mrightarrow{} (A)[1(\mBbbI{})]))s\} BY
(InferEqualType THEN Auto))
THEN All (Unfold `transprt-fun`)
THEN (InstLemma `cubical-fun-as-cubical-pi` [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}((A)s+)[0(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}((A)s+)[1(\mBbbI{})]\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `cubical-fun-as-cubical-pi` [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}(A)[0(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}(A)[1(\mBbbI{})]\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `csm-cubical-lambda` [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}(A)[0(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}((A)[1(\mBbbI{})])p\mkleeneclose{}]\mcdot{} THENA Auto)
THEN InstHyp [\mkleeneopen{}transprt(Gamma.(A)[0(\mBbbI{})];(cA)p+;q)\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}] (-1)\mcdot{}
THEN Try (Trivial))
Home
Index