圏:junked

from 圏

junked.icon

signature.icon

code:category.sig

sig 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

より一般の真理値としてはHeyting代数くらいを想定しておけばいいのかな

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)