Require Import UniMath.Foundations.Preamble.
Require Import UniMath.MoreFoundations.Tactics.
Require Export UniMath.Topology.Filters.
Require Import UniMath.Algebra.DivisionRig.
Require Import UniMath.Algebra.ConstructiveStructures.

Require Import UniMath.Topology.Topology.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.

Definition top_disp_cat_ob_mor : disp_cat_ob_mor HSET.
Proof.
  use tpair.
  - intro X. exact (isTopologicalSet (pr1hSet X)).
  - cbn. intros X Y T U f.
    apply (@continuous (pr1hSet X,,T) (pr1hSet Y,,U) f).
Defined.

Definition top_disp_cat_data : disp_cat_data HSET.
Proof.
  ∃ top_disp_cat_ob_mor.
  use tpair.
  - intros X XX. cbn. unfold continuous. intros.
    unfold continuous_at. cbn. unfold is_lim. cbn.
    unfold filterlim. cbn. unfold filter_le. cbn.
    intros. assumption.
  - intros X Y Z f g XX YY ZZ Hf Hg.
    use (@continuous_funcomp (pr1hSet X,,XX) (pr1hSet Y,,YY) (pr1hSet Z,,ZZ) f g);
      assumption.
Defined.

Definition top_disp_cat_axioms : disp_cat_axioms SET top_disp_cat_data.
Proof.
  repeat split; cbn; intros; try (apply proofirrelevance, isaprop_continuous).
  apply isasetaprop. apply isaprop_continuous.
Defined.

Definition disp_top : disp_cat SET := _ ,, top_disp_cat_axioms.