Library UniMath.Topology.CategoryTop
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.Core.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.
Show 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).
- intro X. exact (isTopologicalSet (pr1hSet X)).
- cbn. intros X Y T U f.
apply (@continuous (pr1hSet X,,T) (pr1hSet Y,,U) f).
Definition top_disp_cat_data : disp_cat_data HSET.
Show proof.
exists 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.
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.
Definition top_disp_cat_axioms : disp_cat_axioms SET top_disp_cat_data.
Show proof.
repeat split; cbn; intros; try (apply proofirrelevance, isaprop_continuous).
apply isasetaprop. apply isaprop_continuous.
apply isasetaprop. apply isaprop_continuous.
Definition disp_top : disp_cat SET := _ ,, top_disp_cat_axioms.