Nuprl Lemma : cubical-set-eqs-istype
∀[XF:X:L:(Cname List) ⟶ Type × (I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J))]
istype(let X,F = XF
in (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((F I K (f o g)) = ((F J K g) o (F I J f)) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((F I I 1) = (λx.x) ∈ ((X I) ⟶ (X I)))))
Proof
Definitions occuring in Statement :
name-comp: (f o g),
id-morph: 1,
name-morph: name-morph(I;J),
coordinate_name: Cname,
list: T List,
compose: f o g,
istype: istype(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
and: P ∧ Q,
all: ∀x:A. B[x],
member: t ∈ T
Lemmas referenced :
name-morph_wf,
name-comp_wf,
compose_wf,
id-morph_wf,
list_wf,
coordinate_name_wf,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
productElimination,
thin,
sqequalRule,
productIsType,
functionIsType,
because_Cache,
universeIsType,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
hypothesis,
equalityIstype,
applyEquality,
baseClosed,
sqequalBase,
equalitySymmetry,
instantiate,
universeEquality
Latex:
\mforall{}[XF:X:L:(Cname List) {}\mrightarrow{} Type \mtimes{} (I:(Cname List)
{}\mrightarrow{} J:(Cname List)
{}\mrightarrow{} name-morph(I;J)
{}\mrightarrow{} (X I)
{}\mrightarrow{} (X J))]
istype(let X,F = XF
in (\mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K).
((F I K (f o g)) = ((F J K g) o (F I J f))))
\mwedge{} (\mforall{}I:Cname List. ((F I I 1) = (\mlambda{}x.x))))
Date html generated:
2019_11_05-PM-00_25_19
Last ObjectModification:
2018_12_10-AM-09_36_07
Theory : cubical!sets
Home
Index