nLab
bicartesian closed preordered object

Contents

Context

Relations

Category theory

Limits and colimits

(0,1)(0,1)-Category theory

Contents

Definition

In a finitely complete category CC, a bicartesian closed preordered object or Heyting prealgebra object is a bicartesian preordered object

(X,s,t,ρ,τ p,,τ,λ l,λ r,,,β,κ l,κ r)(X, s, t, \rho, \tau_p \wedge, \top, \tau, \lambda_l, \lambda_r, \vee, \bot, \beta, \kappa_l, \kappa_r)

with a morphism ()():X×XX(-)\Rightarrow(-):X \times X \to X and functions

ϵ l:((*X)×(*X))(*R)\epsilon_l:((* \to X) \times (* \to X)) \to (* \to R)
ϵ r:((*X)×(*X))(*R)\epsilon_r:((* \to X) \times (* \to X)) \to (* \to R)

such that for all global elements a:*Xa:* \to X and b:*Xb:* \to X,

  • sϵ l(a,b)=(ab)as \circ \epsilon_l(a, b) = (a \Rightarrow b) \wedge a
  • tϵ l(a,b)=bt \circ \epsilon_l(a, b) = b
  • sϵ r(a,b)=as \circ \epsilon_r(a, b) = a
  • tϵ r(a,b)=b(ab)t \circ \epsilon_r(a, b) = b \Rightarrow (a \wedge b)

See also

Last revised on May 14, 2022 at 10:39:38. See the history of this page for a list of all contributions to it.