Library UniMath.CategoryTheory.Hyperdoctrines.TriposToTopos

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.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERBinProducts.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PEREqualizers.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERTerminal.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERSubobjectClassifier.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialPER.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialEval.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialLam.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialEqs.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERExponentials.

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.