Definition tripos_to_topos (H : tripos) : Topos. Proof. use make_Topos. - exact (category_of_partial_setoids H). - use make_Topos_Structure. + use Pullbacks_from_Equalizers_BinProducts. * exact (binproducts_partial_setoid H). * exact (equalizers_partial_setoid H). + exact (terminal_partial_setoid H). + exact (subobject_classifier_partial_setoid H). + use PowerObject_from_exponentials. exact (exponentials_independent _ _ (exponentials_partial_setoid H)). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.PowerObject. Require Import UniMath.CategoryTheory.ElementaryTopos. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos. Require Import UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate.