Nuprl Lemma : Rules of MLTT without type formers
The rules from Figure 1 in Bezem, Coquand, Huber
"A model of type theory in cubical sets".
(First those without type formers)
Γ ⊢
------------- this is { csm-id_wf }
1: σ ─→ Γ
σ: Δ ─→ Γ δ: Θ -> Δ
------------------------ this is { csm-comp_wf }
σ δ : Θ ─→ Γ
Γ ⊢ A σ : Δ ─→ Γ
---------------------- this is { csm-ap-type_wf }
Δ ⊢ A σ
Γ ⊢ t: A σ: Δ ─→ Γ
----------------------- this is { csm-ap-term_wf }
Δ ⊢ t σ: A σ
------------- this is { trivial-cube-set_wf }
() ⊢
Γ ⊢ Γ ⊢ A
----------------- this is { cube-context-adjoin_wf }
Γ.A ⊢
Γ ⊢ A
------------------ this is { cc-fst_wf }
p: Γ.A ─→ Γ
Γ ⊢ A
----------------- this is { cc-snd_wf }
Γ.A ⊢ q: Ap
σ:Δ ─→ Γ Γ ⊢ A Δ ⊢ u:A s
------------------------------ this is { csm-adjoin_wf }
(σ,u) ⊢ Δ ─→ Γ.A
1 σ = σ 1 = σ this is { csm-id-comp }
(σ δ) ν = σ (δ ν) this is { csm-comp-assoc }
[u] = (1,u) this is csm-id-adjoin: [u]
A 1 = A this is { csm-ap-id-type }
(A σ) δ = A (σ δ) this is { csm-ap-comp-type }
u 1 = 1 this is { csm-ap-id-term }
(u σ) δ = u (σ δ) this is { csm-ap-comp-term }
(σ, u) δ = (σ δ, u δ) this is { csm-adjoin-ap }
p (σ, u) = σ this is { cc-fst-csm-adjoin }
q (σ, u) = u this is { cc-snd-csm-adjoin }
(p,q) = 1 this is { csm-adjoin-fst-snd }
⋅
Latex:
The rules from Figure 1 in Bezem, Coquand, Huber
"A model of type theory in cubical sets".
(First those without type formers)
\00CC \mvdash{}
------------- this is \{ csm-id\_wf \}
1: \00CF {}\mrightarrow{} \00CC
\00CF: \mDelta{} {}\mrightarrow{} \00CC \mdelta{}: \00CD -> \mDelta{}
------------------------ this is \{ csm-comp\_wf \}
\00CF \mdelta{} : \00CD {}\mrightarrow{} \00CC
\00CC \mvdash{} A \00CF : \mDelta{} {}\mrightarrow{} \00CC
---------------------- this is \{ csm-ap-type\_wf \}
\mDelta{} \mvdash{} A \00CF
\00CC \mvdash{} t: A \00CF: \mDelta{} {}\mrightarrow{} \00CC
----------------------- this is \{ csm-ap-term\_wf \}
\mDelta{} \mvdash{} t \00CF: A \00CF
------------- this is \{ trivial-cube-set\_wf \}
() \mvdash{}
\00CC \mvdash{} \00CC \mvdash{} A
----------------- this is \{ cube-context-adjoin\_wf \}
\00CC.A \mvdash{}
\00CC \mvdash{} A
------------------ this is \{ cc-fst\_wf \}
p: \00CC.A {}\mrightarrow{} \00CC
\00CC \mvdash{} A
----------------- this is \{ cc-snd\_wf \}
\00CC.A \mvdash{} q: Ap
\00CF:\mDelta{} {}\mrightarrow{} \00CC \00CC \mvdash{} A \mDelta{} \mvdash{} u:A s
------------------------------ this is \{ csm-adjoin\_wf \}
(\00CF,u) \mvdash{} \mDelta{} {}\mrightarrow{} \00CC.A
1 \00CF = \00CF 1 = \00CF this is \{ csm-id-comp \}
(\00CF \mdelta{}) \00CE = \00CF (\mdelta{} \00CE) this is \{ csm-comp-assoc \}
[u] = (1,u) this is csm-id-adjoin: [u]
A 1 = A this is \{ csm-ap-id-type \}
(A \00CF) \mdelta{} = A (\00CF \mdelta{}) this is \{ csm-ap-comp-type \}
u 1 = 1 this is \{ csm-ap-id-term \}
(u \00CF) \mdelta{} = u (\00CF \mdelta{}) this is \{ csm-ap-comp-term \}
(\00CF, u) \mdelta{} = (\00CF \mdelta{}, u \mdelta{}) this is \{ csm-adjoin-ap \}
p (\00CF, u) = \00CF this is \{ cc-fst-csm-adjoin \}
q (\00CF, u) = u this is \{ cc-snd-csm-adjoin \}
(p,q) = 1 this is \{ csm-adjoin-fst-snd \}
\mcdot{}
Date html generated:
2015_07_17-PM-06_22_07
Last ObjectModification:
2015_03_14-AM-06_48_24
Home
Index