Step
*
1
of Lemma
csm-transport-fun
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(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. ((λtransport(Gamma.(A)[0(𝕀)];q)))s ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
9. (λtransport(H.((A)s+)[0(𝕀)];q)) ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
⊢ ((λtransport(Gamma.(A)[0(𝕀)];q)))s = (λtransport(H.((A)s+)[0(𝕀)];q)) ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
BY
{ ((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)
) }
1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(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. ((λtransport(Gamma.(A)[0(𝕀)];q)))s ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
9. (λtransport(H.((A)s+)[0(𝕀)];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 ⊢ _}
⊢ ((λtransport(Gamma.(A)[0(𝕀)];q)))s = (λtransport(H.((A)s+)[0(𝕀)];q)) ∈ {H ⊢ _:(((A)[0(𝕀)] ⟶ (A)[1(𝕀)]))s}
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma.\mBbbI{} \mvdash{} \_\}
3. cA : Gamma.\mBbbI{} \mvdash{} CompOp(A)
4. H : CubicalSet\{j\}
5. s : H j{}\mrightarrow{} Gamma
6. s+ \mmember{} H.\mBbbI{} ij{}\mrightarrow{} Gamma.\mBbbI{}
7. \{H \mvdash{} \_:(((A)[0(\mBbbI{})] {}\mrightarrow{} (A)[1(\mBbbI{})]))s\} = \{H \mvdash{} \_:(((A)s+)[0(\mBbbI{})] {}\mrightarrow{} ((A)s+)[1(\mBbbI{})])\}
8. ((\mlambda{}transport(Gamma.(A)[0(\mBbbI{})];q)))s \mmember{} \{H \mvdash{} \_:(((A)[0(\mBbbI{})] {}\mrightarrow{} (A)[1(\mBbbI{})]))s\}
9. (\mlambda{}transport(H.((A)s+)[0(\mBbbI{})];q)) \mmember{} \{H \mvdash{} \_:(((A)[0(\mBbbI{})] {}\mrightarrow{} (A)[1(\mBbbI{})]))s\}
\mvdash{} ((\mlambda{}transport(Gamma.(A)[0(\mBbbI{})];q)))s = (\mlambda{}transport(H.((A)s+)[0(\mBbbI{})];q))
By
Latex:
((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)
)
Home
Index