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.Arithmetic.NNO.
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 Import UniMath.CategoryTheory.Hyperdoctrines.HyperdoctrineNat.
Require Import UniMath.CategoryTheory.Hyperdoctrines.Completion.Construction.
Require Import UniMath.CategoryTheory.Hyperdoctrines.Completion.Naturals.
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.
Require Export UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERNaturals.

Definition weak_tripos_to_topos
           (H : weak_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.

Definition weak_tripos_to_topos_NNO
           (H : weak_tripos)
           (N : first_order_hyperdoctrine_nats H)
  : NNO (Topos_Terminal (weak_tripos_to_topos H))
  := category_of_partial_setoids_NNO N.

Definition tripos_to_topos
           (H : tripos)
  : Topos
  := weak_tripos_to_topos (tripos_to_weak_tripos H).

Definition tripos_to_topos_NNO
           (H : tripos)
           (N : first_order_hyperdoctrine_nats H)
  : NNO (Topos_Terminal (tripos_to_topos H))
  := weak_tripos_to_topos_NNO
       (tripos_to_weak_tripos H)
       (tripos_to_weak_tripos_nats H N).

Definition preorder_tripos_to_topos
           (H : preorder_tripos)
  : Topos
  := weak_tripos_to_topos (tripos_completion H).

Definition preorder_tripos_to_topos_NNO
           (H : preorder_tripos)
           (N : first_order_preorder_hyperdoctrine_nats H)
  : NNO (Topos_Terminal (preorder_tripos_to_topos H))
  := weak_tripos_to_topos_NNO
       (tripos_completion H)
       (first_order_preorder_hyperdoctrine_completion_nats N).