Library UniMath.CategoryTheory.ModelCategories.MorphismClass
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.ModelCategories.Retract.
Declare Scope morcls.
Delimit Scope morcls with morcls.
Local Open Scope morcls.
Local Open Scope cat.
Definition morphism_class (C : category) : UU :=
∏ (X Y : C), hsubtype (X --> Y).
Lemma isasetmorphism_class {C : category} : isaset (morphism_class C).
Show proof.
Definition morphism_class_set (C : category) : hSet :=
make_hSet (morphism_class C) (isasetmorphism_class (C := C)).
Definition morphism_class_containedIn {C : category} : hrel (morphism_class_set C) :=
λ S T, ∀ (X Y : C) (f : X --> Y), ((S _ _) f ⇒ (T _ _) f)%logic.
Notation "S ⊆ T" := (morphism_class_containedIn S T) (at level 70) : morcls.
Lemma morphism_class_ext {C : category} {I J : morphism_class C}
(h : ∏ x y (f : x --> y), ((I _ _) f <-> (J _ _) f)) : I = J.
Show proof.
Lemma morphism_class_subset_antisymm {C : category} {I J : morphism_class C} (h : I ⊆ J) (h' : J ⊆ I) : I = J.
Show proof.
Definition morphism_class_intersection {C : category} (S T : morphism_class C) : morphism_class C:=
λ X Y f, (S _ _ f) ∧ (T _ _ f).
Notation "S ∩ T" := (morphism_class_intersection S T) : morcls.
Definition morphism_class_univ (C : category) : (morphism_class C) :=
λ X Y f, htrue.
Definition morphism_class_isos (C : category) : (morphism_class C) :=
λ X Y f, make_hProp (is_iso f) (isaprop_is_iso _ _ _).
Lemma iso_in_morphism_class_isos {C : category} {a b : C} (f : iso a b) : (morphism_class_isos C _ _ f).
Show proof.
Definition morphism_class_opp {C : category} (S : morphism_class C) : (morphism_class (op_cat C)) :=
λ X Y f, (S _ _) (opp_mor f).
Definition morphism_class_rm_opp {C : category} (S : morphism_class (op_cat C)) : (morphism_class C) :=
λ X Y f, (S _ _) (rm_opp_mor f).
Lemma morphism_class_opp_opp {C : category} (S : morphism_class C) :
morphism_class_opp (morphism_class_opp S) = S.
Show proof.
Definition morphism_class_opp_equal {C : category} {S T : morphism_class C} (e : morphism_class_opp S = morphism_class_opp T) :
S = T.
Show proof.
Definition morphism_class_retract_closure {C : category} (S : morphism_class C) :=
λ x y (f : x --> y), ∃ x y (f' : x --> y), (S _ _ f') × (retract f' f).
Notation "S ^cl" := (morphism_class_retract_closure S) (at level 70) : morcls.
Lemma in_morcls_retc_if_in_morcls {C : category} (S : morphism_class C)
{a b} (f : a --> b) :
(S _ _ f) -> (S^cl _ _ f).
Show proof.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.ModelCategories.Retract.
Declare Scope morcls.
Delimit Scope morcls with morcls.
Local Open Scope morcls.
Local Open Scope cat.
Definition morphism_class (C : category) : UU :=
∏ (X Y : C), hsubtype (X --> Y).
Lemma isasetmorphism_class {C : category} : isaset (morphism_class C).
Show proof.
change (isaset) with (isofhlevel 2).
apply impred; intro x.
apply impred; intro t.
exact (isasethsubtype _).
apply impred; intro x.
apply impred; intro t.
exact (isasethsubtype _).
Definition morphism_class_set (C : category) : hSet :=
make_hSet (morphism_class C) (isasetmorphism_class (C := C)).
Definition morphism_class_containedIn {C : category} : hrel (morphism_class_set C) :=
λ S T, ∀ (X Y : C) (f : X --> Y), ((S _ _) f ⇒ (T _ _) f)%logic.
Notation "S ⊆ T" := (morphism_class_containedIn S T) (at level 70) : morcls.
Lemma morphism_class_ext {C : category} {I J : morphism_class C}
(h : ∏ x y (f : x --> y), ((I _ _) f <-> (J _ _) f)) : I = J.
Show proof.
do 3 (apply funextsec; intro).
destruct ((h x x0 x1)) as [impl conv].
exact (hPropUnivalence _ _ impl conv).
destruct ((h x x0 x1)) as [impl conv].
exact (hPropUnivalence _ _ impl conv).
Lemma morphism_class_subset_antisymm {C : category} {I J : morphism_class C} (h : I ⊆ J) (h' : J ⊆ I) : I = J.
Show proof.
Definition morphism_class_intersection {C : category} (S T : morphism_class C) : morphism_class C:=
λ X Y f, (S _ _ f) ∧ (T _ _ f).
Notation "S ∩ T" := (morphism_class_intersection S T) : morcls.
Definition morphism_class_univ (C : category) : (morphism_class C) :=
λ X Y f, htrue.
Definition morphism_class_isos (C : category) : (morphism_class C) :=
λ X Y f, make_hProp (is_iso f) (isaprop_is_iso _ _ _).
Lemma iso_in_morphism_class_isos {C : category} {a b : C} (f : iso a b) : (morphism_class_isos C _ _ f).
Show proof.
Definition morphism_class_opp {C : category} (S : morphism_class C) : (morphism_class (op_cat C)) :=
λ X Y f, (S _ _) (opp_mor f).
Definition morphism_class_rm_opp {C : category} (S : morphism_class (op_cat C)) : (morphism_class C) :=
λ X Y f, (S _ _) (rm_opp_mor f).
Lemma morphism_class_opp_opp {C : category} (S : morphism_class C) :
morphism_class_opp (morphism_class_opp S) = S.
Show proof.
trivial.
Definition morphism_class_opp_equal {C : category} {S T : morphism_class C} (e : morphism_class_opp S = morphism_class_opp T) :
S = T.
Show proof.
Definition morphism_class_retract_closure {C : category} (S : morphism_class C) :=
λ x y (f : x --> y), ∃ x y (f' : x --> y), (S _ _ f') × (retract f' f).
Notation "S ^cl" := (morphism_class_retract_closure S) (at level 70) : morcls.
Lemma in_morcls_retc_if_in_morcls {C : category} (S : morphism_class C)
{a b} (f : a --> b) :
(S _ _ f) -> (S^cl _ _ f).
Show proof.