nLab bicartesian closed preordered object

Redirected from "Heyting prealgebra object".
Contents

Context

Relations

Category theory

Limits and colimits

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

Contents

Idea

The notion of a bicartesian closed preordered object or Heyting prealgebra object is the generalization of that of bicartesian closed preordered set or Heyting prealgebra as one passes from the ambient category of sets into more general ambient categories with suitable properties.

Definition

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

(X,R,s,t,ρ,τ p,,τ,λ l,λ r,,,β,κ l,κ r)(X, R, 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 July 17, 2022 at 06:36:01. See the history of this page for a list of all contributions to it.