Nuprl Lemma : Rules of MLTT type formers
The rules about type formers Π and ⌈Σ⌉ from Figure 1 in Bezem, Coquand, Huber
"A model of type theory in cubical sets".
Γ.A ⊢ B
------------- this is { cubical-pi_wf }
Γ ⊢ Π A B
Γ.A ⊢ B Γ.A ⊢ b:B
------------------------ this is { cubical-lambda_wf }
Γ ⊢ λb : Π A B
Γ.A ⊢ B
------------- this is { cubical-sigma_wf }
Γ ⊢ Σ A B
Γ.A ⊢ B Γ ⊢ u:A Γ ⊢ v:B[u]
------------------------------ this is { cubical-pair_wf }
Γ ⊢ (u,v): Σ A B
Γ ⊢ w: Σ A B
---------------- this is { cubical-fst_wf }
Γ ⊢ w.1: A
Γ ⊢ w: Σ A B
----------------- this is { cubical-snd_wf }
Γ ⊢ w.2: B[w.1]
Γ ⊢ w:Π A B Γ ⊢ u:A
------------------------ this is { cubical-app_wf }
Γ ⊢ app(w,u): B[u]
(Π A B)σ = Π (Aσ) (B(σp,q)) this is { csm-cubical-pi }
(λb)σ = λ(b(σp,q)) this is { csm-ap-cubical-lambda }
app(w,u)δ = app(wδ, uδ) this is { csm-ap-cubical-app }
app(λb, u) = b[u] this is { cubical-beta }
w = λ(app(wp,q)) this is { cubical-eta }
(Σ A B)σ = (Aσ) (B(σp,q)) this is { csm-cubical-sigma }
(w.1)σ = (wσ).1 this is { csm-ap-cubical-fst }
(w.2)σ = (wσ).2 this is { csm-ap-cubical-snd }
(u,v)σ = (uσ, vσ) this is { csm-ap-cubical-pair }
(u,v).1 = u this is { cubical-fst-pair }
(u,v).2 = v this is { cubical-snd-pair }
(w.1,w.2) = w this is { cubical-pair-eta }
⋅
Latex:
The rules about type formers \mPi{} and \mkleeneopen{}\mSigma{}\mkleeneclose{} from Figure 1 in Bezem, Coquand, Huber
"A model of type theory in cubical sets".
\00CC.A \mvdash{} B
------------- this is \{ cubical-pi\_wf \}
\00CC \mvdash{} \mPi{} A B
\00CC.A \mvdash{} B \00CC.A \mvdash{} b:B
------------------------ this is \{ cubical-lambda\_wf \}
\00CC \mvdash{} \mlambda{}b : \mPi{} A B
\00CC.A \mvdash{} B
------------- this is \{ cubical-sigma\_wf \}
\00CC \mvdash{} \mSigma{} A B
\00CC.A \mvdash{} B \00CC \mvdash{} u:A \00CC \mvdash{} v:B[u]
------------------------------ this is \{ cubical-pair\_wf \}
\00CC \mvdash{} (u,v): \mSigma{} A B
\00CC \mvdash{} w: \mSigma{} A B
---------------- this is \{ cubical-fst\_wf \}
\00CC \mvdash{} w.1: A
\00CC \mvdash{} w: \mSigma{} A B
----------------- this is \{ cubical-snd\_wf \}
\00CC \mvdash{} w.2: B[w.1]
\00CC \mvdash{} w:\mPi{} A B \00CC \mvdash{} u:A
------------------------ this is \{ cubical-app\_wf \}
\00CC \mvdash{} app(w,u): B[u]
(\mPi{} A B)\00CF = \mPi{} (A\00CF) (B(\00CFp,q)) this is \{ csm-cubical-pi \}
(\mlambda{}b)\00CF = \mlambda{}(b(\00CFp,q)) this is \{ csm-ap-cubical-lambda \}
app(w,u)\mdelta{} = app(w\mdelta{}, u\mdelta{}) this is \{ csm-ap-cubical-app \}
app(\mlambda{}b, u) = b[u] this is \{ cubical-beta \}
w = \mlambda{}(app(wp,q)) this is \{ cubical-eta \}
(\mSigma{} A B)\00CF = (A\00CF) (B(\00CFp,q)) this is \{ csm-cubical-sigma \}
(w.1)\00CF = (w\00CF).1 this is \{ csm-ap-cubical-fst \}
(w.2)\00CF = (w\00CF).2 this is \{ csm-ap-cubical-snd \}
(u,v)\00CF = (u\00CF, v\00CF) this is \{ csm-ap-cubical-pair \}
(u,v).1 = u this is \{ cubical-fst-pair \}
(u,v).2 = v this is \{ cubical-snd-pair \}
(w.1,w.2) = w this is \{ cubical-pair-eta \}
\mcdot{}
Date html generated:
2015_07_17-PM-06_22_07
Last ObjectModification:
2015_03_16-PM-07_12_50
Home
Index