Realizability in OCAs and AKSs

In the context of the $\mathcal{OCA}$ associated to an ${\mathcal{AKS}}$ we introduce a closure operator and two associated maps that replace the closure and the maps defined in \cite{kn:ocar}. We were motivated by the search of a full adjunction to the original implication map. We show that all the constructions from $\mathcal{OCA}$s to triposes developped in \cite{kn:ocar} can be also implemented in the new situation.

No reviews yet.

No comments yet.