Comment: Rules of MLTT without type formers
The rules from Figure 1 in Bezem, Coquand, Huber
"A model of type theory in cubical sets".
But here the intepretation uses an arbitrary base category C..
(First those without type formers: 20 lemmas)
Γ ⊢
------------- this is pscm-id_wf
1: Γ ⟶ Γ
σ: Δ ⟶ Γ δ: Θ -> Δ
------------------------ this is pscm-comp_wf
σ δ : Θ ⟶ Γ
Γ ⊢ A σ : Δ ⟶ Γ
---------------------- this is pscm-ap-type_wf
Δ ⊢ A σ
Γ ⊢ t: A σ: Δ ⟶ Γ
----------------------- this is pscm-ap-term_wf
Δ ⊢ t σ: A σ
------------- this is trivial-psc_wf
() ⊢
Γ ⊢ Γ ⊢ A
----------------- this is psc-adjoin_wf
Γ.A ⊢
Γ ⊢ A
------------------ this is psc-fst_wf
p: Γ.A ⟶ Γ
Γ ⊢ A
----------------- this is psc-snd_wf
Γ.A ⊢ q: Ap
σ:Δ ⟶ Γ Γ ⊢ A Δ ⊢ u:A s
------------------------------ this is pscm-adjoin_wf
(σ,u) ⊢ Δ ⟶ Γ.A
1 σ = σ 1 = σ this is pscm-id-comp
(σ δ) ν = σ (δ ν) this is pscm-comp-assoc
[u] = (1,u) this is pscm-id-adjoin
A 1 = A this is pscm-ap-id-type
(A σ) δ = A (σ δ) this is pscm-ap-comp-type
u 1 = 1 this is pscm-ap-id-term
(u σ) δ = u (σ δ) this is pscm-ap-comp-term
(σ, u) δ = (σ δ, u δ) this is pscm-adjoin-ap
p (σ, u) = σ this is psc-fst-pscm-adjoin
q (σ, u) = u this is psc-snd-pscm-adjoin
(p,q) = 1 this is pscm-adjoin-fst-snd
⋅
Comment: 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".
(Interpreted using an arbitrary base category C: 19 lemmas)
Γ.A ⊢ B
------------- this is presheaf-pi_wf
Γ ⊢ Π A B
Γ.A ⊢ B Γ.A ⊢ b:B
------------------------ this is presheaf-lambda_wf
Γ ⊢ λb : Π A B
Γ.A ⊢ B
------------- this is presheaf-sigma_wf
Γ ⊢ Σ A B
Γ.A ⊢ B Γ ⊢ u:A Γ ⊢ v:B[u]
------------------------------ this is presheaf-pair_wf
Γ ⊢ (u,v): Σ A B
Γ ⊢ w: Σ A B
---------------- this is presheaf-fst_wf
Γ ⊢ w.1: A
Γ ⊢ w: Σ A B
----------------- this is presheaf-snd_wf
Γ ⊢ w.2: B[w.1]
Γ ⊢ w:Π A B Γ ⊢ u:A
------------------------ this is presheaf-app_wf
Γ ⊢ app(w,u): B[u]
(Π A B)σ = Π (Aσ) (B(σp,q)) this is pscm-presheaf-pi
(λb)σ = λ(b(σp,q)) this is pscm-ap-presheaf-lambda
app(w,u)δ = app(wδ, uδ) this is pscm-ap-presheaf-app
app(λb, u) = b[u] this is presheaf-beta
w = λ(app(wp,q)) this is presheaf-eta
(Σ A B)σ = (Aσ) (B(σp,q)) this is pscm-presheaf-sigma
(w.1)σ = (wσ).1 this is pscm-ap-presheaf-fst
(w.2)σ = (wσ).2 this is pscm-ap-presheaf-snd
(u,v)σ = (uσ, vσ) this is pscm-presheaf-pair
(u,v).1 = u this is presheaf-fst-pair
(u,v).2 = v this is presheaf-snd-pair
(w.1,w.2) = w this is presheaf-pair-eta
⋅
Definition: ps_context
__⊢ == Functor(op-cat(C);TypeCat')
Lemma: ps_context_wf
∀[C:SmallCategory]. (ps_context{j:l}(C) ∈ 𝕌{[i | j'']})
Definition: small_ps_context
small_ps_context{i:l}(C) == Functor(op-cat(C);TypeCat)
Lemma: small_ps_context_wf
∀[C:SmallCategory]. (small_ps_context{j:l}(C) ∈ 𝕌{[i | j']})
Lemma: small_ps_context_subtype
∀[C:SmallCategory]. (small_ps_context{j:l}(C) ⊆r ps_context{j:l}(C))
Lemma: ps_context_cumulativity
∀[C:SmallCategory]. (ps_context{j:l}(C) ⊆r ps_context{j':l}(C))
Lemma: ps_context_cumulativity2
∀[C:SmallCategory]. (ps_context{j:l}(C) ⊆r ps_context{[i | j]:l}(C))
Lemma: ps_contexts_equal
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].
X = Y ∈ ps_context{j:l}(C)
supposing X = Y ∈ (F:cat-ob(C) ⟶ 𝕌{j'} × (x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ (cat-arrow(C) y x) ⟶ (F x) ⟶ (F y)))
Definition: ext-eq-psc
X ≡ Y == ext-equal-presheaves(C;X;Y)
Lemma: ext-eq-psc_wf
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)]. (X ≡ Y ∈ ℙ{[i | j']})
Definition: I_set
A(I) == A I
Lemma: I_set_wf
∀[C:SmallCategory]. ∀[A:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. (A(I) ∈ 𝕌{j'})
Lemma: I_set_pair_redex_lemma
∀I,G,F:Top. (<F, G>(I) ~ F I)
Definition: psc-restriction
f(s) == (snd(X)) I J f s
Lemma: psc-restriction_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[I,J:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[s:X(I)]. (f(s) ∈ X(J))
Lemma: psc_restriction_pair_lemma
∀s,f,J,I,G,F:Top. (f(s) ~ G I J f s)
Lemma: ps_context-ext
∀[C:SmallCategory]
{FM:F:cat-ob(C) ⟶ 𝕌{j'} × (I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ (cat-arrow(C) J I) ⟶ (F I) ⟶ (F J))|
let F,M = FM
in (∀I:cat-ob(C). ∀s:FM(I). (cat-id(C) I(s) = s ∈ FM(I)))
∧ (∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀s:FM(I).
(cat-comp(C) K J I g f(s) = g(f(s)) ∈ FM(K)))} ≡ ps_context{j:l}(C)
Definition: psc-predicate
psc-predicate(C; X; I,rho.P[I; rho]) == stable-element-predicate(C;X;I,rho.P[I; rho])
Lemma: psc-predicate_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[P:I:cat-ob(C) ⟶ X(I) ⟶ ℙ{[i | j']}].
(psc-predicate(C; X; I,rho.P[I;rho]) ∈ ℙ{[i | j']})
Definition: sub-presheaf-set
X | I,rho.P[I; rho] == X|I,rho.P[I; rho]
Lemma: sub-presheaf-set_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[P:I:cat-ob(C) ⟶ X(I) ⟶ ℙ{j'}].
X | I,rho.P[I;rho] ∈ ps_context{j:l}(C) supposing psc-predicate(C; X; I,rho.P[I;rho])
Lemma: sub-presheaf-set_functionality
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[P,Q:I:cat-ob(C) ⟶ X(I) ⟶ ℙ].
X | I,rho.P[I;rho] ≡ X | I,rho.Q[I;rho]
supposing (∀I:cat-ob(C). ∀rho:X(I). (P[I;rho] ⇐⇒ Q[I;rho])) ∧ psc-predicate(C; X; I,rho.P[I;rho])
Lemma: sub-presheaf-set-true
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. X | I,rho.True ≡ X
Lemma: sub-presheaf-set-and
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[P,Q:I:cat-ob(C) ⟶ X(I) ⟶ ℙ].
X | I,rho.P[I;rho] | I,rho.Q[I;rho] ≡ X | I,rho.P[I;rho] ∧ Q[I;rho]
supposing psc-predicate(C; X; I,rho.P[I;rho]) ∧ psc-predicate(C; X; I,rho.Q[I;rho])
Definition: sets
sets(C; X) == el(X)
Lemma: sets_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (sets(C; X) ∈ small-category{[i | j']:l})
Lemma: sets-ob
∀[C:SmallCategory]. ∀[X:Top]. (cat-ob(sets(C; X)) ~ I:cat-ob(C) × X(I))
Lemma: sets-id
∀[C:SmallCategory]. ∀[X:Top]. (cat-id(sets(C; X)) ~ λA.(cat-id(C) (fst(A))))
Lemma: sets-arrow
∀[C:SmallCategory]. ∀[X:Top].
(cat-arrow(sets(C; X)) ~ λAa,Bb. let A,a = Aa in let B,b = Bb in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} )
Lemma: sets-comp
∀[C:SmallCategory]. ∀[X:Top]. (cat-comp(sets(C; X)) ~ λAa,Bb,Dd,f,g. (cat-comp(C) (fst(Aa)) (fst(Bb)) (fst(Dd)) f g))
Definition: Yoneda
Yoneda(I) == <λJ.(cat-arrow(C) J I), λJ,K,f,g. (cat-comp(C) K J I f g)>
Lemma: Yoneda-is-rep-pre-sheaf
∀[C,I:Top]. (Yoneda(I) ~ rep-pre-sheaf(C;I))
Lemma: Yoneda_wf
∀[C:SmallCategory]. ∀[I:cat-ob(C)]. (Yoneda(I) ∈ __⊢)
Lemma: Yoneda-restriction
∀[C,I,f,s,A,B:Top]. (f(s) ~ cat-comp(C) B A I f s)
Definition: representable-psc
representable-psc(C) == {G:ps_context{1:l}(C)| ∃I:cat-ob(C). (G = Yoneda(I) ∈ ps_context{1:l}(C))}
Lemma: representable-psc_wf
∀[C:small-category{1:l}]. (representable-psc(C) ∈ 𝕌{3})
Definition: trivial-psc
() == <λJ.Unit, λJ,K,f,x. ⋅>
Lemma: trivial-psc_wf
∀[C:SmallCategory]. (() ∈ ps_context{j:l}(C))
Definition: discrete-set
discrete-set(A) == <λJ.A, λJ,K,f,x. x>
Lemma: discrete-set_wf
∀[C:SmallCategory]. ∀[A:𝕌{j}]. (discrete-set(A) ∈ ps_context{j:l}(C))
Definition: presheaf-false
False == discrete-set(Void)
Lemma: presheaf-false_wf
∀[C:SmallCategory]. (False ∈ ps_context{j:l}(C))
Definition: psc_map
A ⟶ B == nat-trans(op-cat(C);TypeCat';A;B)
Lemma: psc_map_wf
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)]. (psc_map{j:l}(C; A; B) ∈ 𝕌{[i | j'']})
Lemma: psc_map_cumulativity
∀[C:SmallCategory]. ∀[G,H:ps_context{j:l}(C)]. (psc_map{j:l}(C; H; G) ⊆r psc_map{j':l}(C; H; G))
Definition: ps-context-map
<rho> == λA,f. (Gamma I A f rho)
Lemma: ps-context-map_wf
∀C:SmallCategory. ∀I:cat-ob(C). ∀Gamma:ps_context{j:l}(C). ∀rho:Gamma(I). (<rho> ∈ psc_map{j:l}(C; Yoneda(I); Gamma))
Lemma: pscm-equal
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)]. ∀[f:psc_map{j:l}(C; A; B)]. ∀[g:I:cat-ob(C) ⟶ A(I) ⟶ B(I)].
f = g ∈ psc_map{j:l}(C; A; B) supposing f = g ∈ (I:cat-ob(C) ⟶ A(I) ⟶ B(I))
Lemma: pscm-equal2
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)]. ∀[f,g:psc_map{j:l}(C; A; B)].
f = g ∈ psc_map{j:l}(C; A; B) supposing ∀K:cat-ob(C). ∀x:A(K). ((f K x) = (g K x) ∈ B(K))
Lemma: psc-map-subtype
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)]. (psc_map{j:l}(C; A; B) ⊆r (I:cat-ob(C) ⟶ A(I) ⟶ B(I)))
Definition: pscm-ap
(s)x == s I x
Lemma: pscm-ap_wf
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)]. ∀[s:psc_map{j:l}(C; X; Y)]. ∀[I:cat-ob(C)]. ∀[x:X(I)]. ((s)x ∈ Y(I))
Lemma: pscm-ap-context-map
∀[I,J,a,rho,G:Top]. ((<rho>)a ~ a(rho))
Definition: pscm-comp
G o F == λx.((G x) o (F x))
Lemma: pscm-comp-sq
∀[C:SmallCategory]. ∀[A,B,E,F,G:Top]. (G o F ~ F o G)
Lemma: pscm-comp_wf
∀[C:SmallCategory]. ∀[A,B,E:ps_context{j:l}(C)]. ∀[F:psc_map{j:l}(C; A; B)]. ∀[G:psc_map{j:l}(C; B; E)].
(G o F ∈ psc_map{j:l}(C; A; E))
Lemma: pscm-comp-assoc
∀[C:SmallCategory]. ∀[A,B,E,D:ps_context{j:l}(C)]. ∀[F:psc_map{j:l}(C; A; B)]. ∀[G:psc_map{j:l}(C; B; E)].
∀[H:psc_map{j:l}(C; E; D)].
(H o G o F = H o G o F ∈ psc_map{j:l}(C; A; D))
Definition: pscm-id
1(X) == λA,x. x
Lemma: pscm-id-sq
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (1(X) ~ identity-trans(op-cat(C);type-cat{j':l};X))
Lemma: pscm-id_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (1(X) ∈ psc_map{j:l}(C; X; X))
Lemma: pscm-id-comp
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)]. ∀[sigma:psc_map{j:l}(C; A; B)].
((sigma o 1(A) = sigma ∈ psc_map{j:l}(C; A; B)) ∧ (1(B) o sigma = sigma ∈ psc_map{j:l}(C; A; B)))
Lemma: pscm-id-comp-sq
∀[A,B,C,D,x,y,X,Y,Z:Top]. (1(D) o x o y ~ x o y)
Lemma: pscm-ap-pscm-comp
∀Gamma,Delta,Z,s1,s2,I,alpha:Top. ((s2 o s1)alpha ~ (s2)(s1)alpha)
Lemma: ps-context-map-1
∀[C:SmallCategory]. ∀[I:cat-ob(C)]. (<cat-id(C) I> = 1(Yoneda(I)) ∈ Yoneda(I) ⟶ Yoneda(I))
Lemma: ps-ps-context-map-comp
∀[C:SmallCategory]. ∀[I,J,K:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[g:cat-arrow(C) K J].
(<cat-comp(C) K J I g f> = <f> o <g> ∈ Yoneda(K) ⟶ Yoneda(I))
Lemma: psc-restriction-id
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. ∀[s:X(I)]. (cat-id(C) I(s) = s ∈ X(I))
Lemma: psc-restriction-when-id
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. ∀[s:X(I)]. ∀[f:cat-arrow(C) I I].
f(s) = s ∈ X(I) supposing f = (cat-id(C) I) ∈ (cat-arrow(C) I I)
Lemma: psc-restriction-comp
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:X(I).
(g(f(a)) = cat-comp(C) K J I g f(a) ∈ X(K))
Lemma: psc-restriction-comp2
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀I,J1,J2,K:cat-ob(C). ∀f:cat-arrow(C) J1 I. ∀g:cat-arrow(C) K J1. ∀a:X(I).
g(f(a)) = cat-comp(C) K J1 I g f(a) ∈ X(K) supposing J1 = J2 ∈ cat-ob(C)
Lemma: psc-map-is
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)].
(psc_map{j:l}(C; A; B) ~ {trans:I:cat-ob(C) ⟶ A(I) ⟶ B(I)|
∀I,J:cat-ob(C). ∀g:cat-arrow(C) J I.
((λs.g(trans I s)) = (λs.(trans J g(s))) ∈ (A(I) ⟶ B(J)))} )
Lemma: pscm-ap-restriction
∀C:SmallCategory. ∀X,Y:ps_context{j:l}(C). ∀s:psc_map{j:l}(C; X; Y). ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).
(f((s)a) = (s)f(a) ∈ Y(J))
Definition: sub_ps_context
Y ⊆ X == 1(Y) ∈ Y ⟶ X
Lemma: sub_ps_context_wf
∀[C:SmallCategory]. ∀[Y,X:ps_context{j:l}(C)]. (sub_ps_context{j:l}(C; Y; X) ∈ 𝕌{[i | j'']})
Lemma: sub_ps_context_transitivity
∀[C:SmallCategory]. ∀[X,Y,Z:ps_context{j:l}(C)].
sub_ps_context{j:l}(C; Z; X) supposing sub_ps_context{j:l}(C; Z; Y) ∧ sub_ps_context{j:l}(C; Y; X)
Lemma: sub_ps_context_weakening
∀[C:SmallCategory]. ∀[X,Z:ps_context{j:l}(C)]. sub_ps_context{j:l}(C; Z; X) supposing Z = X ∈ ps_context{j:l}(C)
Lemma: sub_ps_context_self
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. sub_ps_context{j:l}(C; X; X)
Lemma: implies-sub_ps_context
∀[C:SmallCategory]. ∀[Y,X:ps_context{j:l}(C)].
(sub_ps_context{j:l}(C; Y; X)) supposing
((∀A,B:cat-ob(C). ∀g:cat-arrow(C) B A. ∀rho:Y(A). (g(rho) = g(rho) ∈ X(B))) and
(∀I:cat-ob(C). (Y(I) ⊆r X(I))))
Lemma: subset-I_set
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)]. ∀I:cat-ob(C). (Y(I) ⊆r X(I)) supposing sub_ps_context{j:l}(C; Y; X)
Lemma: ps-subset-restriction
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].
∀[I,J:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[a:Y(I)]. (f(a) = f(a) ∈ X(J)) supposing sub_ps_context{j:l}(C; Y; X)
Lemma: psc_map_subtype
∀[C:SmallCategory]. ∀[X,Y,Z:ps_context{j:l}(C)].
psc_map{j:l}(C; Z; X) ⊆r psc_map{j:l}(C; Z; Y) supposing sub_ps_context{j:l}(C; X; Y)
Lemma: psc_map_subtype2
∀[C:SmallCategory]. ∀[X,Y,Z:ps_context{j:l}(C)].
psc_map{j:l}(C; X; Z) ⊆r psc_map{j:l}(C; Y; Z) supposing sub_ps_context{j:l}(C; Y; X)
Lemma: psc_map_subtype3
∀[C:SmallCategory]. ∀[X,Y,Z,U:ps_context{j:l}(C)].
(psc_map{j:l}(C; X; Z) ⊆r psc_map{j:l}(C; Y; U)) supposing
(sub_ps_context{j:l}(C; Y; X) and
sub_ps_context{j:l}(C; Z; U))
Lemma: psc_map_cumulativity2
∀[C:SmallCategory]. ∀[X,Y,Z,U:ps_context{j:l}(C)].
(psc_map{j:l}(C; X; Z) ⊆r psc_map{j:l}(C; Y; U)) supposing
(sub_ps_context{j:l}(C; Y; X) and
sub_ps_context{j:l}(C; Z; U))
Definition: presheaf_type
presheaf_type{i:l}(C; X) == presheaf{i':l}(sets(C; X))
Lemma: presheaf_type_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (presheaf_type{i:l}(C; X) ∈ 𝕌{[i'' | j']})
Definition: presheaf-type
{X ⊢ _} ==
{AF:A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
⟶ J:cat-ob(C)
⟶ f:(cat-arrow(C) J I)
⟶ a:X(I)
⟶ (A I a)
⟶ (A J f(a)))|
let A,F = AF
in (∀I:cat-ob(C). ∀a:X(I). ∀u:A I a. ((F I I (cat-id(C) I) a u) = u ∈ (A I a)))
∧ (∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:X(I). ∀u:A I a.
((F I K (cat-comp(C) K J I g f) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K cat-comp(C) K J I g f(a))))}
Lemma: presheaf-type_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (X ⊢ ∈ 𝕌{[j' | i']})
Lemma: presheaf-type-equal
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
⟶ J:cat-ob(C)
⟶ f:(cat-arrow(C) J I)
⟶ a:X(I)
⟶ (A I a)
⟶ (A J f(a)))].
A = B ∈ {X ⊢ _}
supposing A
= B
∈ (A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
⟶ J:cat-ob(C)
⟶ f:(cat-arrow(C) J I)
⟶ a:X(I)
⟶ (A I a)
⟶ (A J f(a))))
Lemma: presheaf-type-equal2
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}].
A = B ∈ {X ⊢ _}
supposing A
= B
∈ (A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
⟶ J:cat-ob(C)
⟶ f:(cat-arrow(C) J I)
⟶ a:X(I)
⟶ (A I a)
⟶ (A J f(a))))
Definition: presheaf-type-iso
presheaf-type-iso(X) == λF.<λI,rho. (F <I, rho>), λI,J,f,a. (F <I, a> <J, f(a)> f)>
Lemma: presheaf-type-iso_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (presheaf-type-iso(X) ∈ presheaf_type{i:l}(C; X) ⟶ {X ⊢' _})
Definition: presheaf-type-rev-iso
presheaf-type-rev-iso(X) ==
λF.Presheaf(Set(p) =(fst(F)) (fst(p)) (snd(p));
Morphism(p,q,f,a) = (snd(F)) (fst(p)) (fst(q)) f (snd(p)) a)
Lemma: presheaf-type-rev-iso_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (presheaf-type-rev-iso(X) ∈ {X ⊢ _} ⟶ presheaf_type{i:l}(C; X))
Lemma: presheaf-type-iso-inverse
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].
((presheaf-type-rev-iso(X) o presheaf-type-iso(X)) = (λx.x) ∈ (presheaf_type{i:l}(C; X) ⟶ presheaf_type{i:l}(C; X)))
Lemma: presheaf-type-iso-inverse2
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].
((presheaf-type-iso(X) o presheaf-type-rev-iso(X)) = (λx.x) ∈ ({X ⊢ _} ⟶ {X ⊢ _}))
Lemma: presheaf-type-cumulativity
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ({X ⊢ _} ⊆r {X ⊢' _})
Lemma: presheaf-type-cumulativity2
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ({X ⊢ _} ⊆r presheaf-type{[j | i]:l}(C; X))
Definition: presheaf-type-at
A(a) == (fst(A)) I a
Lemma: presheaf-type-at_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[I:cat-ob(C)]. ∀[a:X(I)]. (A(a) ∈ Type)
Lemma: presheaf_type_at_pair_lemma
∀a,I,B,A:Top. (<A, B>(a) ~ A I a)
Definition: presheaf-type-ap-morph
(u a f) == (snd(A)) I J f a u
Lemma: presheaf-type-ap-morph_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[I,J:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[a:X(I)].
∀[u:A(a)].
((u a f) ∈ A(f(a)))
Lemma: presheaf_type_ap_morph_pair_lemma
∀u,a,f,J,I,G,F:Top. ((u a f) ~ G I J f a u)
Lemma: presheaf-type-ap-morph-comp
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[I,J,K:cat-ob(C)]. ∀[f:cat-arrow(C) J I].
∀[g:cat-arrow(C) K J]. ∀[a:X(I)]. ∀[u:A(a)].
(((u a f) f(a) g) = (u a cat-comp(C) K J I g f) ∈ A(cat-comp(C) K J I g f(a)))
Lemma: presheaf-type-ap-morph-comp-eq
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[I,J,K:cat-ob(C)]. ∀[f:cat-arrow(C) J I].
∀[g:cat-arrow(C) K J]. ∀[a:X(I)]. ∀[b:X(J)]. ∀[u:A(a)].
((u a f) b g) = (u a cat-comp(C) K J I g f) ∈ A(cat-comp(C) K J I g f(a)) supposing b = f(a) ∈ X(J)
Lemma: presheaf-type-ap-morph-id
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[I:cat-ob(C)]. ∀[f:cat-arrow(C) I I]. ∀[a:X(I)]. ∀[u:A(a)].
(u a f) = u ∈ A(a) supposing f = (cat-id(C) I) ∈ (cat-arrow(C) I I)
Lemma: presheaf-type-equal3
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}].
(A = B ∈ {X ⊢ _}) supposing
((∀I:cat-ob(C)
∀[rho:X(I)]. ∀[J:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[u:A(rho)]. ((u rho f) = (u rho f) ∈ A(f(rho)))) and
(∀I:cat-ob(C). ∀[rho:X(I)]. (A(rho) = B(rho) ∈ Type)))
Definition: pscm-ap-type
(AF)s == let A,F = AF in <λI,a. (A I (s)a), λI,J,f,a,u. (F I J f (s)a u)>
Lemma: pscm-ap-type_wf
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[s:psc_map{j:l}(C; Delta; Gamma)].
((A)s ∈ Delta ⊢ )
Definition: pscm-type-ap
pscm-type-ap(A;s) == (A)s
Lemma: pscm-type-ap_wf
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[s:psc_map{j:l}(C; Delta; Gamma)]. ∀[A:{Gamma ⊢ _}].
(pscm-type-ap(A;s) ∈ Delta ⊢ )
Lemma: ps-context-map-ap-type
∀[C:SmallCategory]. ∀[I:cat-ob(C)]. ∀[Gamma:ps_context{j:l}(C)]. ∀[rho:Gamma(I)]. ∀[A:{Gamma ⊢ _}].
((A)<rho> ∈ Yoneda(I) ⊢ )
Lemma: pscm-ap-type-at
∀[B,s,x,K:Top]. ((B)s(x) ~ B((s)x))
Lemma: pscm-ap-id-type
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ((A)1(Gamma) = A ∈ {Gamma ⊢ _})
Lemma: pscm-ap-type-is-id
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[s:psc_map{j:l}(C; Gamma; Gamma)].
(A)s = A ∈ {Gamma ⊢ _} supposing s = 1(Gamma) ∈ psc_map{j:l}(C; Gamma; Gamma)
Lemma: pscm-comp-type
∀[Gamma,Delta,Z,s1,s2,A:Top]. ((A)s2 o s1 ~ ((A)s2)s1)
Lemma: pscm-type-comp
∀[Gamma,A,Delta,Z,s1,s2:Top]. (((A)s2)s1 ~ (A)s2 o s1)
Lemma: pscm-ap-comp-type
∀[C:SmallCategory]. ∀[Gamma,Delta,Z:ps_context{j:l}(C)]. ∀[s1:psc_map{j:l}(C; Z; Delta)]. ∀[s2:psc_map{j:l}(C;
Delta;
Gamma)].
∀[A:{Gamma ⊢ _}].
((A)s2 o s1 = ((A)s2)s1 ∈ {Z ⊢ _})
Lemma: pscm-ap-comp-type-sq
∀[Gamma,Delta,Z,s1,s2,A:Top]. ((A)s2 o s1 ~ ((A)s2)s1)
Lemma: pscm-ap-comp-type-sq2
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[s1,s2:Top]. (((A)s2)s1 ~ (A)s2 o s1)
Lemma: pscm-presheaf-type-ap-morph
∀[A,I,J,f,a,u,s:Top]. ((u a f) ~ (u (s)a f))
Definition: presheaf-term
{X ⊢ _:A} ==
{u:I:cat-ob(C) ⟶ a:X(I) ⟶ A(a)|
∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I). ((u I a a f) = (u J f(a)) ∈ A(f(a)))}
Lemma: presheaf-term_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ({X ⊢ _:A} ∈ 𝕌{[i | j']})
Lemma: presheaf-term_wf2
∀[C:SmallCategory]. ∀[X:ps_context{[i | j]:l}(C)]. ∀[A:{X ⊢ _}]. ({X ⊢ _:A} ∈ 𝕌{[i' | j']})
Definition: presheaf-term-at
u(a) == u I a
Lemma: presheaf-term-at_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[I:cat-ob(C)]. ∀[a:X(I)]. (u(a) ∈ A(a))
Lemma: presheaf-term-at-morph
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[I:cat-ob(C)]. ∀[a:X(I)]. ∀[J:cat-ob(C)].
∀[f:cat-arrow(C) J I].
((u(a) a f) = u(f(a)) ∈ A(f(a)))
Lemma: presheaf-term-equal
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:cat-ob(C) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:cat-ob(C) ⟶ a:X(I) ⟶ A(a))
Lemma: presheaf-term-equal2
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u,z:{X ⊢ _:A}].
u = z ∈ {X ⊢ _:A} supposing ∀I:cat-ob(C). ∀a:X(I). ((u I a) = (z I a) ∈ A(a))
Definition: ps-canonical-section
ps-canonical-section(Gamma;A;I;rho;a) == λK,f. (a rho f)
Lemma: ps-canonical-section_wf
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[I:cat-ob(C)]. ∀[rho:Gamma(I)]. ∀[a:A(rho)].
(ps-canonical-section(Gamma;A;I;rho;a) ∈ {Yoneda(I) ⊢ _:(A)<rho>})
Lemma: ps-canonical-section-at
∀[Gamma,A,I,rho,a,J,x:Top]. (ps-canonical-section(Gamma;A;I;rho;a)(x) ~ (a rho x))
Definition: pscm-ap-term
(t)s == λI,a. (t I (s)a)
Lemma: pscm-ap-term_wf
∀[C:SmallCategory]. ∀[Delta,Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[s:psc_map{j:l}(C; Delta; Gamma)].
∀[t:{Gamma ⊢ _:A}].
((t)s ∈ {Delta ⊢ _:(A)s})
Lemma: pscm-ap-term-at
∀[J,s,rho,t:Top]. ((t)s(rho) ~ t((s)rho))
Lemma: pscm-ap-id-term
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:A}].
((t)1(Gamma) = t ∈ {Gamma ⊢ _:A})
Lemma: pscm-comp-term
∀[Gamma,Delta,Z,s1,s2,t:Top]. ((t)s2 o s1 ~ ((t)s2)s1)
Lemma: pscm-ap-comp-term-sq
∀[Gamma,Delta,Z,s1,s2,t:Top]. ((t)s2 o s1 ~ ((t)s2)s1)
Lemma: pscm-ap-comp-term-sq2
∀[s1,s2,t:Top]. (((t)s2)s1 ~ (t)s2 o s1)
Lemma: pscm-ap-comp-term
∀[C:SmallCategory]. ∀[Gamma,Delta,Z:ps_context{j:l}(C)]. ∀[s1:psc_map{j:l}(C; Z; Delta)]. ∀[s2:psc_map{j:l}(C;
Delta;
Gamma)].
∀[A:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:A}].
((t)s2 o s1 = ((t)s2)s1 ∈ {Z ⊢ _:(A)s2 o s1})
Lemma: ps-context-map-comp2
∀[C:SmallCategory]. ∀[G:ps_context{j:l}(C)]. ∀[I,J:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[a:G(I)].
(<a> o <f> = <f(a)> ∈ psc_map{[i | j]:l}(C; Yoneda(J); G))
Lemma: pscm-comp-context-map
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[sigma:psc_map{j:l}(C; Delta; Gamma)]. ∀[I:cat-ob(C)].
∀[rho:Delta(I)].
(sigma o <rho> = <(sigma)rho> ∈ psc_map{[i | j]:l}(C; Yoneda(I); Gamma))
Definition: psc-adjoin
X.A == <λI.(alpha:X(I) × A(alpha)), λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>>
Lemma: psc-adjoin-wf
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢' _}]. (Gamma.A ∈ ps_context{[i | j]:l}(C))
Lemma: psc-adjoin_wf
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. (Gamma.A ∈ ps_context{[i | j]:l}(C))
Lemma: psc-adjoin-I_set
∀[Gamma,A,I:Top]. (Gamma.A(I) ~ alpha:Gamma(I) × A(alpha))
Definition: psc-adjoin-set
(v;u) == <v, u>
Lemma: psc-adjoin-set_wf
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀A:{X ⊢ _}. ∀J:cat-ob(C). ∀v:X(J). ∀u:A(v). ((v;u) ∈ X.A(J))
Lemma: psc-adjoin-set-restriction
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[J,K,g,v,u:Top]. (g((v;u)) ~ (g(v);(u v g)))
Definition: psc-fst
p == λI,p. (fst(p))
Lemma: psc-fst_wf
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. (p ∈ psc_map{[i | j]:l}(C; Gamma.A; Gamma))
Definition: psc-snd
q == λI,p. (snd(p))
Lemma: psc-snd_wf
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. (q ∈ {Gamma.A ⊢ _:(A)p})
Lemma: cc_fst_adjoin_set_lemma
∀y,x,J:Top. ((p)(x;y) ~ x)
Lemma: cc_snd_adjoin_set_lemma
∀y,x,J:Top. ((q)(x;y) ~ y)
Lemma: csm_comp_fst_adjoin_set_lemma
∀y,x,K,s,X,B,A:Top. ((s o p)(x;y) ~ (s)x)
Lemma: csm_comp_snd_adjoin-set_lemma
∀y,x,K,s,X,B,A:Top. ((s o q)(x;y) ~ (s)y)
Definition: psc-fstfst
pp == λI,rho. (fst(fst(rho)))
Lemma: psc-fstfst_wf
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[B:{Gamma.A ⊢ _}].
(pp ∈ psc_map{[i | j]:l}(C; Gamma.A.B; Gamma))
Definition: typed-psc-fst
tp{i:l} == p
Lemma: typed-psc-fst_wf
∀[C:SmallCategory]. ∀[G:ps_context{j:l}(C)]. ∀[A:{G ⊢ _}]. (tp{i:l} ∈ psc_map{[i | j]:l}(C; G.A; G))
Definition: typed-psc-snd
tq == q
Lemma: typed-psc-snd_wf
∀C:SmallCategory. ∀G:ps_context{j:l}(C). ∀A:{G ⊢ _}. (tq ∈ {G.A ⊢ _:(A)tp{i:l}})
Definition: psc-m2
q2 == (q)p
Lemma: psc-m2_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. (q2 ∈ {X.A.B ⊢ _:((A)p)p})
Definition: psc-m3
q3 == (q2)p
Lemma: psc-m3_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[E:{X.A.B ⊢ _}].
(q3 ∈ {X.A.B.E ⊢ _:(((A)p)p)p})
Definition: psc-m4
q4 == (q3)p
Lemma: psc-m4_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[E:{X.A.B ⊢ _}]. ∀[D:{X.A.B.E ⊢ _}].
(q4 ∈ {X.A.B.E.D ⊢ _:((((A)p)p)p)p})
Lemma: pscm-ap-term-p
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A,T:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:A}]. ((t)p ∈ {Gamma.T ⊢ _:(A)p})
Lemma: pscm-type-at
∀s,A,I,alpha:Top. ((A)s(alpha) ~ A((s)alpha))
Definition: pscm-adjoin
(s;u) == λI,a. <(s)a, u I a>
Lemma: pscm-adjoin-wf
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢' _}]. ∀[sigma:psc_map{j:l}(C; Delta; Gamma)].
∀[u:{Delta ⊢ _:(A)sigma}].
((sigma;u) ∈ psc_map{[i | j]:l}(C; Delta; Gamma.A))
Lemma: pscm-adjoin_wf
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:psc_map{j:l}(C; Delta; Gamma)].
∀[u:{Delta ⊢ _:(A)sigma}].
((sigma;u) ∈ psc_map{[i | j]:l}(C; Delta; Gamma.A))
Lemma: pscm-adjoin-comp
∀[Gamma,Delta,X,A,sigma,u,g:Top]. ((sigma;u) o g ~ (sigma o g;(u)g))
Lemma: pscm-adjoin-ap
∀[sigma,u,I,del:Top]. (((sigma;u))del ~ ((sigma)del;(u)del))
Definition: pscm-id-adjoin
[u] == (1(X);u)
Lemma: pscm-id-adjoin-wf
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢' _}]. ∀[u:{Gamma ⊢ _:A}].
([u] ∈ psc_map{[i | j]:l}(C; Gamma; Gamma.A))
Lemma: pscm-id-adjoin_wf
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[u:{Gamma ⊢ _:A}].
([u] ∈ psc_map{[i | j]:l}(C; Gamma; Gamma.A))
Lemma: pscm-id-adjoin-ap
∀X,u,I,a:Top. (([u])a ~ (a;u I a))
Lemma: psc-fst-pscm-adjoin-sq
∀[Gamma,Delta,X,sigma,u:Top]. (p o (sigma;u) ~ sigma o 1(Delta))
Lemma: psc-fst-pscm-adjoin
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:psc_map{j:l}(C; Delta; Gamma)].
∀[u:{Delta ⊢ _:(A)sigma}].
(p o (sigma;u) = sigma ∈ psc_map{j:l}(C; Delta; Gamma))
Lemma: ps-cc_snd_csm_id_adjoin_lemma
∀u,G:Top. ((q)[u] ~ (u)1(G))
Lemma: ps-typed_cc_snd_id_adjoin_lemma
∀A,G,u,X:Top. ((tq)[u] ~ (u)1(X))
Lemma: ps-csm_id_adjoin_fst_type_lemma
∀A,t,X:Top. (((A)p)[t] ~ (A)1(X))
Lemma: ps-csm_id_adjoin_fst_term_lemma
∀a,t,X:Top. (((a)p)[t] ~ (a)1(X))
Lemma: ps-csm_id_ap_term_lemma
∀t,X,s:Top. (((t)1(X))s ~ (t)s)
Lemma: psc-snd-pscm-adjoin-sq
∀[G,sigma,u:Top]. ((q)(sigma;u) ~ (u)1(G))
Lemma: psc-snd-pscm-adjoin
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:psc_map{j:l}(C; Delta; Gamma)].
∀[u:{Delta ⊢ _:(A)sigma}].
((q)(sigma;u) = u ∈ {Delta ⊢ _:(A)sigma})
Lemma: pscm-adjoin-fst-snd
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}].
((p;q) = 1(Gamma.A) ∈ psc_map{[i | j]:l}(C; Gamma.A; Gamma.A))
Lemma: pscm-ap-type-fst-adjoin
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[B:{X ⊢ _}]. ∀[s,u:Top]. (((B)p)(s;u) ~ (B)s)
Lemma: pscm-ap-type-fst-id-adjoin
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[B:{X ⊢ _}]. ∀[u:Top]. (((B)p)[u] = B ∈ {X ⊢ _})
Lemma: pscm-id-adjoin-ap-type
∀C:SmallCategory. ∀Gamma,Delta:ps_context{j:l}(C). ∀A:{Gamma ⊢ _}. ∀B:{Gamma.A ⊢ _}.
∀sigma:psc_map{j:l}(C; Delta; Gamma). ∀u:{Delta ⊢ _:(A)sigma}.
(((B)(sigma o p;q))[u] = (B)(sigma;u) ∈ {Delta ⊢ _})
Lemma: ps-csm_ap_term_fst_adjoin_lemma
∀zz,yy,xx:Top. (((zz)p)(xx;yy) ~ (zz)xx)
Lemma: pscm-ap-term-snd-adjoin
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[xx:Top]. ((q)(xx;u) = u ∈ {X ⊢ _:A})
Lemma: pscm-adjoin-id-adjoin
∀[B,xx,s,X,Y,Z:Top]. (((B)(s o p;q))[xx] ~ (B)(s;xx))
Definition: pscm+
tau+ == (tau o p;q)
Lemma: pscm+_wf
∀[C:SmallCategory]. ∀[H,K:ps_context{j:l}(C)]. ∀[A:{H ⊢ _}]. ∀[tau:psc_map{j:l}(C; K; H)].
(tau+ ∈ psc_map{[i | j]:l}(C; K.(A)tau; H.A))
Lemma: p-pscm+-type
∀[H,K,A,B,tau:Top]. (((A)p)tau+ ~ ((A)tau)p)
Lemma: pcsm+-p-type
∀[C,H,K,A,B,tau:Top]. (((A)p)(tau+ o p;q) ~ ((A)tau+)p)
Lemma: p-pscm+-term
∀[H,K,A,t,tau:Top]. (((t)p)tau+ ~ ((t)tau)p)
Lemma: pcsm+-p-term
∀[C,H,K,t,B,tau:Top]. (((t)p)(tau+ o p;q) ~ ((t)tau+)p)
Lemma: q-pscm+
∀[H,K,A,tau:Top]. ((q)tau+ ~ q)
Lemma: pscm-adjoin-p-q
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ((B)(p;q) = B ∈ {X.A ⊢ _})
Definition: pscm-swap
pscm-swap(G;A;B) == (p+;(q)p)
Lemma: pscm-swap_wf
∀[C:SmallCategory]. ∀[G:ps_context{j:l}(C)]. ∀[A,B:{G ⊢ _}].
(pscm-swap(G;A;B) ∈ psc_map{[i | j]:l}(C; G.A.(B)p; G.B.(A)p))
Definition: presheaf-pi-family
presheaf-pi-family(C; X; A; B; I; a) ==
{w:J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f(a)) ⟶ B((f(a);u))|
∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A(f(a)).
((w J f u (f(a);u) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ B(g((f(a);u))))}
Lemma: presheaf-pi-family_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[I:cat-ob(C)]. ∀[a:X(I)].
(presheaf-pi-family(C; X; A; B; I; a) ∈ Type)
Lemma: presheaf-pi-family-comp
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀s:psc_map{j:l}(C; Delta; X). ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I.
∀a:Delta(I). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀w:presheaf-pi-family(C; X; A; B; I; (s)a).
(λK,g. (w K (cat-comp(C) K J I g f)) ∈ presheaf-pi-family(C; X; A; B; J; (s)f(a)))
Lemma: pscm-presheaf-pi-family
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X). ∀I:cat-ob(C).
∀a:Delta(I).
(presheaf-pi-family(C; X; A; B; I; (s)a) = presheaf-pi-family(C; Delta; (A)s; (B)(s o p;q); I; a) ∈ Type)
Definition: presheaf-fun-family
presheaf-fun-family(C; X; A; B; I; a) ==
{w:J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f(a)) ⟶ B(f(a))|
∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A(f(a)).
((w J f u f(a) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ B(g(f(a))))}
Lemma: presheaf-fun-family_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[I:cat-ob(C)]. ∀[a:X(I)].
(presheaf-fun-family(C; X; A; B; I; a) ∈ Type)
Lemma: presheaf-fun-family-comp
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀s:psc_map{j:l}(C; Delta; X). ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I.
∀a:Delta(I). ∀A,B:{X ⊢ _}. ∀w:presheaf-fun-family(C; X; A; B; I; (s)a).
(λK,g. (w K (cat-comp(C) K J I g f)) ∈ presheaf-fun-family(C; X; A; B; J; (s)f(a)))
Lemma: pscm-presheaf-fun-family
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A,B:{X ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X). ∀I:cat-ob(C). ∀a:Delta(I).
(presheaf-fun-family(C; X; A; B; I; (s)a) = presheaf-fun-family(C; Delta; (A)s; (B)s; I; a) ∈ Type)
Definition: presheaf-pi
ΠA B == <λI,a. presheaf-pi-family(C; X; A; B; I; a), λI,J,f,a,w,K,g. (w K (cat-comp(C) K J I g f))>
Lemma: presheaf-pi_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. (ΠA B ∈ X ⊢ )
Lemma: pscm-presheaf-pi
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X).
((ΠA B)s = Delta ⊢ Π(A)s (B)(s o p;q) ∈ {Delta ⊢ _})
Lemma: presheaf-pi-p
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀T,A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ((ΠA B)p = X.T ⊢ Π(A)p (B)(p o p;q) ∈ {X.T ⊢ _})
Definition: pscm-dependent
(s)dep == (s o tp{i:l};tq)
Lemma: pscm-dependent_wf
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A:{X ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X).
((s)dep ∈ psc_map{j:l}(C; Delta.(A)s; X.A))
Lemma: ps-csm_dep_p_rewrite_lemma
∀T,s,A,Delta,X:Top. (((T)p)(s)dep ~ ((T)s)p)
Lemma: ps-csm_dep_typed_p_lemma
∀T,s,A,Delta,X:Top. (((T)tp{i:l})(s)dep ~ ((T)s)tp{i:l})
Lemma: pscm-dep_term_p_lemma
∀t,s,A,Delta,X:Top. (((t)tp{i:l})(s)dep ~ ((t)s)tp{i:l})
Lemma: ps-csm_dep_term_q_lemma
∀s,A,Delta,X:Top. ((tq)(s)dep ~ tq)
Definition: presheaf-fun
(A ⟶ B) == <λI,a. presheaf-fun-family(C; X; A; B; I; a), λI,J,f,a,w,K,g. (w K (cat-comp(C) K J I g f))>
Lemma: presheaf-fun_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ((A ⟶ B) ∈ X ⊢ )
Lemma: pscm-presheaf-fun
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A,B:{X ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X).
(((A ⟶ B))s = (Delta ⊢ (A)s ⟶ (B)s) ∈ {Delta ⊢ _})
Lemma: presheaf-fun-equal
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[f,g:{X ⊢ _:(A ⟶ B)}].
f = g ∈ {X ⊢ _:(A ⟶ B)}
supposing ∀[I:cat-ob(C)]. ∀[a:X(I)]. ∀[J:cat-ob(C)]. ∀[h:cat-arrow(C) J I]. ∀[u:A(h(a))].
((f(a) J h u) = (g(a) J h u) ∈ B(h(a)))
Lemma: presheaf-fun-equal2
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[f:{X ⊢ _:(A ⟶ B)}]. ∀[g:I:cat-ob(C)
⟶ a:X(I)
⟶ J:cat-ob(C)
⟶ h:(cat-arrow(C) J I)
⟶ u:A(h(a))
⟶ B(h(a))].
f = g ∈ {X ⊢ _:(A ⟶ B)}
supposing ∀[I:cat-ob(C)]. ∀[a:X(I)]. ∀[J:cat-ob(C)]. ∀[h:cat-arrow(C) J I]. ∀[u:A(h(a))].
((f(a) J h u) = (g(a) J h u) ∈ B(h(a)))
Lemma: presheaf-fun-p
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀A,B,T:{X ⊢ _}. (((A ⟶ B))p = (X.T ⊢ (A)p ⟶ (B)p) ∈ {X.T ⊢ _})
Lemma: member-presheaf-fun-p
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B,T:{X ⊢ _}]. ∀[x:{X ⊢ _:(A ⟶ B)}]. ((x)p ∈ {X.T ⊢ _:((A)p ⟶ (B)p)})
Lemma: psc-snd_wf-presheaf-fun
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀A,B:{X ⊢ _}. (q ∈ {X.(A ⟶ B) ⊢ _:((A)p ⟶ (B)p)})
Lemma: presheaf-fun-as-presheaf-pi
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ((X ⊢ A ⟶ B) = X ⊢ ΠA (B)p ∈ {X ⊢ _})
Definition: presheaf-lambda
(λb) == λI,a,J,f,u. (b J (f(a);u))
Lemma: presheaf-lambda_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}]. ((λb) ∈ {X ⊢ _:ΠA B})
Lemma: pscm-presheaf-lambda
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}]. ∀[H:ps_context{j:l}(C)].
∀[s:psc_map{j:l}(C; H; X)].
(((λb))s = (λ(b)s+) ∈ {H ⊢ _:(ΠA B)s})
Definition: presheaf-lam
presheaf-lam(X;b) == (λb)
Lemma: presheaf-lam_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[b:{X.A ⊢ _:(B)p}].
(presheaf-lam(X;b) ∈ {X ⊢ _:(A ⟶ B)})
Lemma: pscm-presheaf-lam
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[b:{X.A ⊢ _:(B)p}]. ∀[H:ps_context{j:l}(C)].
∀[s:psc_map{j:l}(C; H; X)].
((presheaf-lam(X;b))s = presheaf-lam(H;(b)s+) ∈ {H ⊢ _:((A ⟶ B))s})
Definition: presheaf-id-fun
presheaf-id-fun(X) == presheaf-lam(X;q)
Lemma: presheaf-id-fun_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. (presheaf-id-fun(X) ∈ {X ⊢ _:(A ⟶ A)})
Lemma: pscm-presheaf-id-fun
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[H:ps_context{j:l}(C)]. ∀[s:psc_map{j:l}(C; H; X)].
((presheaf-id-fun(X))s = presheaf-id-fun(H) ∈ {H ⊢ _:((A)s ⟶ (A)s)})
Definition: presheaf-app
app(w; u) == λI,a. (w I a I (cat-id(C) I) (u I a))
Lemma: presheaf-app_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}]. ∀[u:{X ⊢ _:A}].
(app(w; u) ∈ {X ⊢ _:(B)[u]})
Lemma: presheaf-app_wf-pscm
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}]. ∀[H:ps_context{j:l}(C)].
∀[tau:psc_map{j:l}(C; H; X)]. ∀[u:{H ⊢ _:(A)tau}].
(app((w)tau; u) ∈ {H ⊢ _:((B)tau+)[u]})
Definition: presheaf-apply
presheaf-apply(w;u) == app(w; u)
Lemma: presheaf-apply_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}]. ∀[u:{X ⊢ _:A}].
(presheaf-apply(w;u) ∈ {X ⊢ _:(B)[u]})
Lemma: presheaf-app_wf_fun
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[w:{X ⊢ _:(A ⟶ B)}]. ∀[u:{X ⊢ _:A}].
(app(w; u) ∈ {X ⊢ _:B})
Definition: presheaf-fun-comp
(f o g) == presheaf-lam(G;app((f)p; app((g)p; q)))
Lemma: presheaf-fun-comp_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B,E:{X ⊢ _}]. ∀[g:{X ⊢ _:(A ⟶ B)}]. ∀[f:{X ⊢ _:(B ⟶ E)}].
((f o g) ∈ {X ⊢ _:(A ⟶ E)})
Definition: presheaf-sigma
Σ A B == <λI,a. (u:A(a) × B((a;u))), λI,J,f,a,p. <(fst(p) a f), (snd(p) (a;fst(p)) f)>>
Lemma: presheaf-sigma_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. (Σ A B ∈ X ⊢ )
Lemma: presheaf-sigma-at
∀[X,A,B,I,a:Top]. (Σ A B(a) ~ u:A(a) × B((a;u)))
Lemma: pscm-presheaf-sigma
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X).
((Σ A B)s = Σ (A)s (B)(s o p;q) ∈ {Delta ⊢ _})
Lemma: presheaf-sigma-p
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀T,A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ((Σ A B)p = Σ (A)p (B)(p o p;q) ∈ {X.T ⊢ _})
Lemma: presheaf-sigma-p-p
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀T,A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀E:{X.T ⊢ _}.
(((Σ A B)p)p = Σ ((A)p)p (B)(p o p o p;q) ∈ {X.T.E ⊢ _})
Lemma: pscm-presheaf-sigma-typed
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X).
((Σ A B)s = Σ (A)s (B)(s)dep ∈ {Delta ⊢ _})
Definition: presheaf-fst
p.1 == λI,a. (fst((p I a)))
Lemma: presheaf-fst_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}]. (p.1 ∈ {X ⊢ _:A})
Lemma: pscm-presheaf-fst
∀[p,s:Top]. ((p.1)s ~ (p)s.1)
Lemma: pscm-ap-presheaf-fst
∀[C:SmallCategory]. ∀[X,Delta:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}].
∀[s:psc_map{j:l}(C; Delta; X)].
((p.1)s = (p)s.1 ∈ {Delta ⊢ _:(A)s})
Definition: presheaf-snd
p.2 == λI,a. (snd((p I a)))
Lemma: presheaf-snd_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}]. (p.2 ∈ {X ⊢ _:(B)[p.1]})
Lemma: presheaf-snd-at
∀[a,I,p:Top]. (p.2(a) ~ snd(p(a)))
Lemma: presheaf-fst-at
∀[a,I,p:Top]. (p.1(a) ~ fst(p(a)))
Lemma: pscm-presheaf-snd
∀[p,s:Top]. ((p.2)s ~ (p)s.2)
Lemma: pscm-ap-presheaf-snd
∀[C:SmallCategory]. ∀[X,Delta:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}].
∀[s:psc_map{j:l}(C; Delta; X)].
((p.2)s = (p)s.2 ∈ {Delta ⊢ _:((B)[p.1])s})
Definition: presheaf-pair
presheaf-pair(u;v) == λI,a. <u I a, v I a>
Lemma: presheaf-pair_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:{X ⊢ _:(B)[u]}].
(presheaf-pair(u;v) ∈ {X ⊢ _:Σ A B})
Lemma: pscm-presheaf-pair
∀[u,v,s:Top]. ((presheaf-pair(u;v))s ~ presheaf-pair((u)s;(v)s))
Definition: sigma-elim-pscm
SigmaElim == λI,x. let a,u,v = x in ((a;u);v)
Lemma: sigma-elim-pscm_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].
(SigmaElim ∈ psc_map{[i | j]:l}(C; X.Σ A B; X.A.B))
Definition: sigma-unelim-pscm
SigmaUnElim == λI,x. let au,v = x in let a,u = au in (a;(u;v))
Lemma: sigma-unelim-pscm_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].
(SigmaUnElim ∈ psc_map{[i | j]:l}(C; X.A.B; X.Σ A B))
Lemma: ps-sigma-elim-unelim
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].
(SigmaUnElim o SigmaElim = 1(X.Σ A B) ∈ psc_map{[i | j]:l}(C; X.Σ A B; X.Σ A B))
Lemma: ps-sigma-unelim-elim
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].
(SigmaElim o SigmaUnElim = 1(X.A.B) ∈ psc_map{[i | j]:l}(C; X.A.B; X.A.B))
Lemma: ps-sigma-unelim-elim-type
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[T:{X.Σ A B ⊢ _}].
(((T)SigmaUnElim)SigmaElim = T ∈ {X.Σ A B ⊢ _})
Lemma: ps-sigma-unelim-elim-term
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[T:{X.Σ A B ⊢ _}]. ∀[t:{X.Σ A B ⊢ _:T}].
(((t)SigmaUnElim)SigmaElim = t ∈ {X.Σ A B ⊢ _:T})
Lemma: ps-sigma-unelim-p
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].
(p o SigmaUnElim = p o p ∈ psc_map{[i | j]:l}(C; X.A.B; X))
Lemma: ps-sigma-unelim-p-type
∀[T:Top]. (((T)p)SigmaUnElim ~ ((T)p)p)
Lemma: ps-sigma-unelim-p-term
∀[t:Top]. (((t)p)SigmaUnElim ~ ((t)p)p)
Lemma: ps-sigma-elim-rule
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[T:{X.Σ A B ⊢ _}].
∀[t:{X.A.B ⊢ _:(T)SigmaUnElim}].
((t)SigmaElim ∈ {X.Σ A B ⊢ _:T})
Lemma: ps-sigma-elim-equality-rule
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[T:{X.Σ A B ⊢ _}].
∀[t1,t2:{X.A.B ⊢ _:(T)SigmaUnElim}].
(t1)SigmaElim = (t2)SigmaElim ∈ {X.Σ A B ⊢ _:T} supposing t1 = t2 ∈ {X.A.B ⊢ _:(T)SigmaUnElim}
Lemma: ps-sigma-elim-equality-rule2
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[T:{X.Σ A B ⊢ _}].
∀[t1:{X.A.B ⊢ _:(T)SigmaUnElim}]. ∀[t2:{X.Σ A B ⊢ _:T}].
(t1)SigmaElim = t2 ∈ {X.Σ A B ⊢ _:T} supposing t1 = (t2)SigmaUnElim ∈ {X.A.B ⊢ _:(T)SigmaUnElim}
Lemma: pscm-ap-presheaf-pair
∀[C:SmallCategory]. ∀[X,Delta:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:{X ⊢ _:(B)[u]}].
∀[s:psc_map{j:l}(C; Delta; X)].
((presheaf-pair(u;v))s = presheaf-pair((u)s;(v)s) ∈ {Delta ⊢ _:(Σ A B)s})
Lemma: pscm-presheaf-app
∀[C,w,u,s:Top]. ((app(w; u))s ~ app((w)s; (u)s))
Lemma: pscm-ap-presheaf-app
∀[C:SmallCategory]. ∀[X,Delta:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}]. ∀[u:{X ⊢ _:A}].
∀[s:psc_map{j:l}(C; Delta; X)].
((app(w; u))s = app((w)s; (u)s) ∈ {Delta ⊢ _:((B)[u])s})
Lemma: pscm-ap-presheaf-app-fun
∀[C:SmallCategory]. ∀[X,Delta:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[w:{X ⊢ _:(A ⟶ B)}]. ∀[u:{X ⊢ _:A}].
∀[s:psc_map{j:l}(C; Delta; X)].
((app(w; u))s = app((w)s; (u)s) ∈ {Delta ⊢ _:(B)s})
Lemma: pscm-ap-presheaf-lambda
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}]. ∀[H:ps_context{j:l}(C)].
∀[s:psc_map{j:l}(C; H; X)].
(((λb))s = (λ(b)s+) ∈ {H ⊢ _:(ΠA B)s})
Lemma: presheaf-snd-pair
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:{X ⊢ _:(B)[u]}].
(presheaf-pair(u;v).2 = v ∈ {X ⊢ _:(B)[u]})
Lemma: presheaf-fst-pair
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:Top].
(presheaf-pair(u;v).1 = u ∈ {X ⊢ _:A})
Lemma: presheaf-pair-eta
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:Σ A B}].
(presheaf-pair(w.1;w.2) = w ∈ {X ⊢ _:Σ A B})
Lemma: presheaf-sigma-equal
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w,y:{X ⊢ _:Σ A B}].
(w = y ∈ {X ⊢ _:Σ A B}) supposing ((w.2 = y.2 ∈ {X ⊢ _:(B)[w.1]}) and (w.1 = y.1 ∈ {X ⊢ _:A}))
Lemma: presheaf-eta
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}].
((λapp((w)p; q)) = w ∈ {X ⊢ _:ΠA B})
Lemma: presheaf-fun-eta
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[w:{X ⊢ _:(A ⟶ B)}].
(presheaf-lam(X;app((w)p; q)) = w ∈ {X ⊢ _:(A ⟶ B)})
Lemma: presheaf-beta
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}]. ∀[u:{X ⊢ _:A}].
(app((λb); u) = (b)[u] ∈ {X ⊢ _:(B)[u]})
Lemma: presheaf-app-id-fun
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. (app(presheaf-id-fun(X); u) = u ∈ {X ⊢ _:A})
Definition: presheaf-sigma-fun
presheaf-sigma-fun(G;A;B;f) == presheaf-lam(G;presheaf-pair(q.1;app(app(((λf))p; q.1); q.2)))
Lemma: presheaf-sigma-fun_wf
∀[C:SmallCategory]. ∀[G:ps_context{j:l}(C)]. ∀[A:{G ⊢ _}]. ∀[B,B':{G.A ⊢ _}]. ∀[f:{G.A ⊢ _:(B ⟶ B')}].
(presheaf-sigma-fun(G;A;B;f) ∈ {G ⊢ _:(Σ A B ⟶ Σ A B')})
Definition: discrete-presheaf-type
discr(T) == <λI,alpha. T, λI,J,f,alpha,x. x>
Lemma: discrete-presheaf-type_wf
∀[C:SmallCategory]. ∀[T:Type]. ∀[X:ps_context{j:l}(C)]. (discr(T) ∈ X ⊢ )
Lemma: pscm-discrete-presheaf-type
∀[T,s:Top]. ((discr(T))s ~ discr(T))
Definition: discrete-presheaf-term
discr(t) == λI,alpha. t
Lemma: discrete-presheaf-term_wf
∀[C:SmallCategory]. ∀[T:Type]. ∀[t:T]. ∀[X:ps_context{j:l}(C)]. (discr(t) ∈ {X ⊢ _:discr(T)})
Lemma: discrete-presheaf-term-at-morph
∀[C:SmallCategory]. ∀[T:Type]. ∀[X:ps_context{j:l}(C)]. ∀[t:{X ⊢ _:discr(T)}].
∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I). (t(a) = t(f(a)) ∈ T)
Definition: discrete-unary
discrete-unary(t;x.f[x]) == λI,a. f[t(a)]
Lemma: discrete-unary_wf
∀[C:SmallCategory]. ∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[X:ps_context{j:l}(C)]. ∀[t:{X ⊢ _:discr(A)}].
(discrete-unary(t;x.f[x]) ∈ {X ⊢ _:discr(B)})
Lemma: pscm-discrete-presheaf-term
∀[t,s:Top]. ((discr(t))s ~ discr(t))
Lemma: discrete-presheaf-term-is-map
∀[C:SmallCategory]. ∀[T:Type]. ∀[X:ps_context{j:l}(C)]. {X ⊢ _:discr(T)} ≡ psc_map{[i | j]:l}(C; X; discrete-set(T))
Lemma: ps-discrete-map-is-constant
∀[C:SmallCategory]. ∀[T:𝕌{j}]. ∀[I:cat-ob(C)]. ∀[s:psc_map{[i | j]:l}(C; Yoneda(I); discrete-set(T))].
(s = (λJ,g. (s I (cat-id(C) I))) ∈ psc_map{[i | j]:l}(C; Yoneda(I); discrete-set(T)))
Lemma: discrete-presheaf-term-is-constant
Not every term of a discrete presheaf type is constant, but when the
context is the Yoneda(I) -- Yoneda(I) -- then it is.⋅
∀[C:SmallCategory]. ∀[T:Type]. ∀[I:cat-ob(C)]. ∀[t:{Yoneda(I) ⊢ _:discr(T)}].
(t = discr(t(cat-id(C) I)) ∈ {Yoneda(I) ⊢ _:discr(T)})
Definition: presheaf-unit
1 == discr(Unit)
Lemma: presheaf-unit_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (1 ∈ X ⊢ )
Lemma: pscm-presheaf-unit
∀[s:Top]. ((1)s ~ 1)
Definition: presheaf-it
* == discr(⋅)
Lemma: presheaf-it_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (* ∈ {X ⊢ _:1})
Lemma: presheaf-it-unique
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[t:{X ⊢ _:1}]. (t = * ∈ {X ⊢ _:1})
Definition: constant-presheaf-type
(X) == <λI,alpha. X(I), λI,J,f,alpha,w. f(w)>
Lemma: constant-presheaf-type_wf
∀[C:SmallCategory]. ∀[X:small_ps_context{i:l}(C)]. ∀[Gamma:ps_context{j:l}(C)]. ((X) ∈ Gamma ⊢ )
Lemma: pscm-constant-presheaf-type
∀[X,s:Top]. (((X))s ~ (X))
Lemma: constant-presheaf-type-at
∀[X,I,a:Top]. ((X)(a) ~ X(I))
Lemma: unit-set-presheaf-type
∀[C:SmallCategory]. ∀[I:cat-ob(C)].
({Yoneda(I) ⊢ _} ~ {AF:A:L:cat-ob(C) ⟶ (cat-arrow(C) L I) ⟶ Type × (L:cat-ob(C)
⟶ J:cat-ob(C)
⟶ f:(cat-arrow(C) J L)
⟶ a:(cat-arrow(C) L I)
⟶ (A L a)
⟶ (A J (cat-comp(C) J L I f a)))|
let A,F = AF
in (∀K:cat-ob(C). ∀a:cat-arrow(C) K I. ∀u:A K a. ((F K K (cat-id(C) K) a u) = u ∈ (A K a)))
∧ (∀L,J,K:cat-ob(C). ∀f:cat-arrow(C) J L. ∀g:cat-arrow(C) K J. ∀a:cat-arrow(C) L I. ∀u:A L a.
((F L K (cat-comp(C) K J L g f) a u)
= (F J K g (cat-comp(C) J L I f a) (F L J f a u))
∈ (A K (cat-comp(C) K L I (cat-comp(C) K J L g f) a))))} )
Lemma: presheaf-term-at-comp
∀C:SmallCategory. ∀Gamma:ps_context{j:l}(C). ∀T:{Gamma ⊢ _}. ∀t:{Gamma ⊢ _:T}. ∀I:cat-ob(C). ∀rho:Gamma(I).
∀J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀K:cat-ob(C). ∀g:cat-arrow(C) K J.
(t(cat-comp(C) K J I g f(rho)) = t(g(f(rho))) ∈ T(g(f(rho))))
Lemma: subset-presheaf-type
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)]. {X ⊢ _} ⊆r {Y ⊢ _} supposing sub_ps_context{j:l}(C; Y; X)
Lemma: subset-presheaf-term
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].
∀[A:{X ⊢ _}]. ({X ⊢ _:A} ⊆r {Y ⊢ _:A}) supposing sub_ps_context{j:l}(C; Y; X)
Lemma: subset-presheaf-term2
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].
∀[A,B:{X ⊢ _}]. {X ⊢ _:A} ⊆r {Y ⊢ _:B} supposing A = B ∈ {X ⊢ _} supposing sub_ps_context{j:l}(C; Y; X)
Lemma: pscm-subset-codomain
∀[C:SmallCategory]. ∀[X,Y,Z:ps_context{j:l}(C)].
psc_map{j:l}(C; X; Y) ⊆r psc_map{j:l}(C; X; Z) supposing sub_ps_context{j:l}(C; Y; Z)
Lemma: pscm-subset-domain
∀[C:SmallCategory]. ∀[X,Y,Z:ps_context{j:l}(C)].
psc_map{j:l}(C; Y; X) ⊆r psc_map{j:l}(C; Z; X) supposing sub_ps_context{j:l}(C; Z; Y)
Lemma: pscm-subset-subtype
∀[C:SmallCategory]. ∀[A,B,Y,Z:ps_context{j:l}(C)].
(psc_map{j:l}(C; Y; A) ⊆r psc_map{j:l}(C; Z; B)) supposing
(sub_ps_context{j:l}(C; A; B) and
sub_ps_context{j:l}(C; Z; Y))
Lemma: sub_ps_context_functionality
∀[C:SmallCategory]. ∀[Y,X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}].
sub_ps_context{[i | j]:l}(C; Y.A; X.A) supposing sub_ps_context{j:l}(C; Y; X)
Lemma: presheaf-pi-intro
∀C:SmallCategory. ∀G:ps_context{j:l}(C). ∀A:{G ⊢ _}. ∀B:{G.A ⊢ _}. ({G.A ⊢ _:B} ⇒ {G ⊢ _:ΠA B})
Lemma: presheaf-sigma-intro
∀C:SmallCategory. ∀G:ps_context{j:l}(C). ∀A:{G ⊢ _}. ∀B:{G.A ⊢ _}. ((∃a:{G ⊢ _:A}. {G ⊢ _:(B)[a]}) ⇒ {G ⊢ _:Σ A B})
Lemma: presheaf-pi-implies-sigma
∀C:SmallCategory. ∀G:ps_context{j:l}(C). ∀A:{G ⊢ _}. ∀B:{G.A ⊢ _}. ({G ⊢ _:A} ⇒ {G ⊢ _:ΠA B} ⇒ {G ⊢ _:Σ A B})
Lemma: ps-csm_typedp_id_adjoin_lemma
∀E,s,F,G,u,H:Top. ((((E)s)tp{i:l})[u] ~ (E)s)
Lemma: presheaf-fun-family-discrete
∀[C:SmallCategory]. ∀[A,B:Type]. ∀[X:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. ∀[a:X(I)].
(presheaf-fun-family(C; X; discr(A); discr(B); I; a)
= {w:J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A ⟶ B|
∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A.
((w J f u) = (w K (cat-comp(C) K J I g f) u) ∈ B)}
∈ Type)
Definition: psdcff-inj
psdcff-inj(I;w) == w I (cat-id(C) I)
Lemma: psdcff-inj_wf
∀[C:SmallCategory]. ∀[A,B:Type]. ∀[X:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. ∀[a:X(I)]. ∀[w:presheaf-fun-family(C;
X;
discr(A);
discr(B);
I;
a)].
(psdcff-inj(I;w) ∈ A ⟶ B)
Lemma: psdcff-inj-injection
∀[C:SmallCategory]. ∀[A,B:Type]. ∀[X:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. ∀[a:X(I)].
Inj(presheaf-fun-family(C; X; discr(A); discr(B); I; a);A ⟶ B;λw.psdcff-inj(I;w))
Lemma: psdcff-inj-bijection
∀[C:SmallCategory]. ∀[A,B:Type]. ∀[X:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. ∀[a:X(I)].
Bij(presheaf-fun-family(C; X; discr(A); discr(B); I; a);A ⟶ B;λw.psdcff-inj(I;w))
Home
Index