Library UniMath.CategoryTheory.categories.grs
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Groups.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Core.Functors.
Section def_gr_precategory.
Definition gr_fun_space (A B : gr) : hSet := make_hSet (monoidfun A B) (isasetmonoidfun A B).
Definition gr_precategory_ob_mor : precategory_ob_mor :=
tpair (λ ob : UU, ob -> ob -> UU) gr (λ A B : gr, gr_fun_space A B).
Definition gr_precategory_data : precategory_data :=
make_precategory_data
gr_precategory_ob_mor (λ (X : gr), ((idmonoidiso X) : monoidfun X X))
(fun (X Y Z : gr) (f : monoidfun X Y) (g : monoidfun Y Z) => monoidfuncomp f g).
Local Lemma gr_id_left (X Y : gr) (f : monoidfun X Y) : monoidfuncomp (idmonoidiso X) f = f.
Show proof.
Opaque gr_id_left.
Local Lemma gr_id_right (X Y : gr) (f : monoidfun X Y) : monoidfuncomp f (idmonoidiso Y) = f.
Show proof.
Opaque gr_id_right.
Local Lemma gr_assoc (X Y Z W : gr) (f : monoidfun X Y) (g : monoidfun Y Z) (h : monoidfun Z W) :
monoidfuncomp f (monoidfuncomp g h) = monoidfuncomp (monoidfuncomp f g) h.
Show proof.
Opaque gr_assoc.
Lemma is_precategory_gr_precategory_data : is_precategory gr_precategory_data.
Show proof.
Definition gr_precategory : precategory :=
make_precategory gr_precategory_data is_precategory_gr_precategory_data.
Lemma has_homsets_gr_precategory : has_homsets gr_precategory.
Show proof.
End def_gr_precategory.
Definition gr_fun_space (A B : gr) : hSet := make_hSet (monoidfun A B) (isasetmonoidfun A B).
Definition gr_precategory_ob_mor : precategory_ob_mor :=
tpair (λ ob : UU, ob -> ob -> UU) gr (λ A B : gr, gr_fun_space A B).
Definition gr_precategory_data : precategory_data :=
make_precategory_data
gr_precategory_ob_mor (λ (X : gr), ((idmonoidiso X) : monoidfun X X))
(fun (X Y Z : gr) (f : monoidfun X Y) (g : monoidfun Y Z) => monoidfuncomp f g).
Local Lemma gr_id_left (X Y : gr) (f : monoidfun X Y) : monoidfuncomp (idmonoidiso X) f = f.
Show proof.
Opaque gr_id_left.
Local Lemma gr_id_right (X Y : gr) (f : monoidfun X Y) : monoidfuncomp f (idmonoidiso Y) = f.
Show proof.
Opaque gr_id_right.
Local Lemma gr_assoc (X Y Z W : gr) (f : monoidfun X Y) (g : monoidfun Y Z) (h : monoidfun Z W) :
monoidfuncomp f (monoidfuncomp g h) = monoidfuncomp (monoidfuncomp f g) h.
Show proof.
Opaque gr_assoc.
Lemma is_precategory_gr_precategory_data : is_precategory gr_precategory_data.
Show proof.
use make_is_precategory_one_assoc.
- intros a b f. use gr_id_left.
- intros a b f. use gr_id_right.
- intros a b c d f g h. use gr_assoc.
- intros a b f. use gr_id_left.
- intros a b f. use gr_id_right.
- intros a b c d f g h. use gr_assoc.
Definition gr_precategory : precategory :=
make_precategory gr_precategory_data is_precategory_gr_precategory_data.
Lemma has_homsets_gr_precategory : has_homsets gr_precategory.
Show proof.
End def_gr_precategory.
Section def_gr_category.
Definition gr_category : category := make_category _ has_homsets_gr_precategory.
Definition gr_category : category := make_category _ has_homsets_gr_precategory.
Lemma gr_iso_is_equiv (A B : ob gr_category) (f : z_iso A B) : isweq (pr1 (pr1 f)).
Show proof.
use isweq_iso.
- exact (pr1monoidfun _ _ (inv_from_z_iso f)).
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
intros x0. use isapropismonoidfun.
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
intros x0. use isapropismonoidfun.
Opaque gr_iso_is_equiv.- exact (pr1monoidfun _ _ (inv_from_z_iso f)).
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
intros x0. use isapropismonoidfun.
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
intros x0. use isapropismonoidfun.
Lemma gr_iso_equiv (X Y : ob gr_category) : z_iso X Y -> monoidiso (X : gr) (Y : gr).
Show proof.
intro f.
use make_monoidiso.
- exact (make_weq (pr1 (pr1 f)) (gr_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
use make_monoidiso.
- exact (make_weq (pr1 (pr1 f)) (gr_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
Lemma gr_equiv_is_iso (X Y : ob gr_category) (f : monoidiso (X : gr) (Y : gr)) :
@is_z_isomorphism gr_precategory X Y (monoidfunconstr (pr2 f)).
Show proof.
exists (monoidfunconstr (pr2 (invmonoidiso f))).
use make_is_inverse_in_precat.
- use monoidfun_paths. use funextfun. intros x. use homotinvweqweq.
- use monoidfun_paths. use funextfun. intros y. use homotweqinvweq.
Opaque gr_equiv_is_iso.use make_is_inverse_in_precat.
- use monoidfun_paths. use funextfun. intros x. use homotinvweqweq.
- use monoidfun_paths. use funextfun. intros y. use homotweqinvweq.
Lemma gr_equiv_iso (X Y : ob gr_category) : monoidiso (X : gr) (Y : gr) -> z_iso X Y.
Show proof.
Lemma gr_iso_equiv_is_equiv (X Y : gr_category) : isweq (gr_iso_equiv X Y).
Show proof.
use isweq_iso.
- exact (gr_equiv_iso X Y).
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
Opaque gr_iso_equiv_is_equiv.- exact (gr_equiv_iso X Y).
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
Definition gr_iso_equiv_weq (X Y : ob gr_category) :
weq (z_iso X Y) (monoidiso (X : gr) (Y : gr)).
Show proof.
Lemma gr_equiv_iso_is_equiv (X Y : ob gr_category) : isweq (gr_equiv_iso X Y).
Show proof.
use isweq_iso.
- exact (gr_iso_equiv X Y).
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
- intros x. apply z_iso_eq. use monoidfun_paths. use idpath.
Opaque gr_equiv_iso_is_equiv.- exact (gr_iso_equiv X Y).
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
- intros x. apply z_iso_eq. use monoidfun_paths. use idpath.
Definition gr_equiv_weq_iso (X Y : ob gr_category) :
(monoidiso (X : gr) (Y : gr)) ≃ (z_iso X Y).
Show proof.
Definition gr_precategory_isweq (X Y : ob gr_category) : isweq (λ p : X = Y, idtoiso p).
Show proof.
use (@isweqhomot
(X = Y) (z_iso X Y)
(pr1weq (weqcomp (gr_univalence X Y) (gr_equiv_weq_iso X Y)))
_ _ (weqproperty (weqcomp (gr_univalence X Y) (gr_equiv_weq_iso X Y)))).
intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use total2_paths_f.
- use idpath.
- use proofirrelevance. use isaprop_is_z_isomorphism.
Opaque gr_precategory_isweq.(X = Y) (z_iso X Y)
(pr1weq (weqcomp (gr_univalence X Y) (gr_equiv_weq_iso X Y)))
_ _ (weqproperty (weqcomp (gr_univalence X Y) (gr_equiv_weq_iso X Y)))).
intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use total2_paths_f.
- use idpath.
- use proofirrelevance. use isaprop_is_z_isomorphism.
Definition gr_category_is_univalent : is_univalent gr_category.
Show proof.
Definition gr_univalent_category : univalent_category
:= make_univalent_category gr_category gr_category_is_univalent.
End def_gr_category.