圏:junked
from 圏
category.sigsig Category fixed-in CLASS %
Data
%0-morph
Obj
%1-morph
Hom : Obj × Obj -> Set
%2-morph
"identity element" @ id
: i => Δ * hom
: I -> Set
"composition morphism" @ comp
: Ob^ × Δ × Ob^ ; hom ⊗ hom
=> Ob^ × ! × Ob^ ; hom
: Ob × Ob × Ob -> V
Axioms
%3-eq "associative"
comp ⊗ hom^; comp
=(hom×hom×hom)α; hom^ ⊗ comp; comp
: Ob^ × Δ × Δ × Ob^; (hom⊗hom)⊗hom
=> Ob^ × ! × ! × Ob^ ; hom
: Ob × Ob × Ob × Ob -> V
%3-eq "left unital"
考察中
真理値実例Ω
\left\lang\mathrm{ Heyting\ alg. }\colon |Ω|; ∧, ∨, ⊥, ⊤, ⊃ \right\rang
X上の述語
\operatorname{Pred}(X) = [X,|Ω|]
\operatorname{Pred}\colon \mathbf{Set}^\mathrm{op} → \mathbf{HeytingAlg}
反変冪集合函手との類似
\mathrm{Pow}^\circ\colon \mathbf{Set}^{\mathrm{op}}→\mathbf{Set}
Δ_{a}\colon [a^\mathrm{op}×a ,b] → \operatorname{Pred}(b)