Library UniMath.CategoryTheory.categories.commrigs
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.RigsAndRings.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.
Section def_commrig_precategory.
Definition commrig_fun_space (A B : commrig) : hSet := make_hSet (rigfun A B) (isasetrigfun A B).
Definition commrig_precategory_ob_mor : precategory_ob_mor :=
tpair (λ ob : UU, ob -> ob -> UU) commrig (λ A B : commrig, commrig_fun_space A B).
Definition commrig_precategory_data : precategory_data :=
make_precategory_data
commrig_precategory_ob_mor (λ (X : commrig), (rigisotorigfun (idrigiso X)))
(fun (X Y Z : commrig) (f : rigfun X Y) (g : rigfun Y Z) => rigfuncomp f g).
Local Lemma commrig_id_left (X Y : commrig) (f : rigfun X Y) :
rigfuncomp (rigisotorigfun (idrigiso X)) f = f.
Show proof.
Opaque commrig_id_left.
Local Lemma commrig_id_commright (X Y : commrig) (f : rigfun X Y) :
rigfuncomp f (rigisotorigfun (idrigiso Y)) = f.
Show proof.
Opaque commrig_id_commright.
Local Lemma commrig_assoc (X Y Z W : commrig) (f : rigfun X Y) (g : rigfun Y Z) (h : rigfun Z W) :
rigfuncomp f (rigfuncomp g h) = rigfuncomp (rigfuncomp f g) h.
Show proof.
Opaque commrig_assoc.
Lemma is_precategory_commrig_precategory_data : is_precategory commrig_precategory_data.
Show proof.
Definition commrig_precategory : precategory :=
make_precategory commrig_precategory_data is_precategory_commrig_precategory_data.
Lemma has_homsets_commrig_precategory : has_homsets commrig_precategory.
Show proof.
End def_commrig_precategory.
Definition commrig_fun_space (A B : commrig) : hSet := make_hSet (rigfun A B) (isasetrigfun A B).
Definition commrig_precategory_ob_mor : precategory_ob_mor :=
tpair (λ ob : UU, ob -> ob -> UU) commrig (λ A B : commrig, commrig_fun_space A B).
Definition commrig_precategory_data : precategory_data :=
make_precategory_data
commrig_precategory_ob_mor (λ (X : commrig), (rigisotorigfun (idrigiso X)))
(fun (X Y Z : commrig) (f : rigfun X Y) (g : rigfun Y Z) => rigfuncomp f g).
Local Lemma commrig_id_left (X Y : commrig) (f : rigfun X Y) :
rigfuncomp (rigisotorigfun (idrigiso X)) f = f.
Show proof.
Opaque commrig_id_left.
Local Lemma commrig_id_commright (X Y : commrig) (f : rigfun X Y) :
rigfuncomp f (rigisotorigfun (idrigiso Y)) = f.
Show proof.
Opaque commrig_id_commright.
Local Lemma commrig_assoc (X Y Z W : commrig) (f : rigfun X Y) (g : rigfun Y Z) (h : rigfun Z W) :
rigfuncomp f (rigfuncomp g h) = rigfuncomp (rigfuncomp f g) h.
Show proof.
Opaque commrig_assoc.
Lemma is_precategory_commrig_precategory_data : is_precategory commrig_precategory_data.
Show proof.
use make_is_precategory_one_assoc.
- intros a b f. use commrig_id_left.
- intros a b f. use commrig_id_commright.
- intros a b c d f g h. use commrig_assoc.
- intros a b f. use commrig_id_left.
- intros a b f. use commrig_id_commright.
- intros a b c d f g h. use commrig_assoc.
Definition commrig_precategory : precategory :=
make_precategory commrig_precategory_data is_precategory_commrig_precategory_data.
Lemma has_homsets_commrig_precategory : has_homsets commrig_precategory.
Show proof.
End def_commrig_precategory.
Section def_commrig_category.
Definition commrig_category : category := make_category _ has_homsets_commrig_precategory.
Definition commrig_category : category := make_category _ has_homsets_commrig_precategory.
Lemma commrig_iso_is_equiv (A B : ob commrig_category) (f : z_iso A B) : isweq (pr1 (pr1 f)).
Show proof.
use isweq_iso.
- exact (pr1rigfun _ _ (inv_from_z_iso f)).
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
intros x0. use isapropisrigfun.
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
intros x0. use isapropisrigfun.
Opaque commrig_iso_is_equiv.- exact (pr1rigfun _ _ (inv_from_z_iso f)).
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
intros x0. use isapropisrigfun.
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
intros x0. use isapropisrigfun.
Lemma commrig_iso_equiv (X Y : ob commrig_category) :
z_iso X Y -> rigiso (X : commrig) (Y : commrig).
Show proof.
intro f.
use make_rigiso.
- exact (make_weq (pr1 (pr1 f)) (commrig_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
use make_rigiso.
- exact (make_weq (pr1 (pr1 f)) (commrig_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
Lemma commrig_equiv_is_z_iso (X Y : ob commrig_category)
(f : rigiso (X : commrig) (Y : commrig)) :
@is_z_isomorphism commrig_precategory X Y (rigfunconstr (pr2 f)).
Show proof.
exists (rigfunconstr (pr2 (invrigiso f))).
use make_is_inverse_in_precat.
- use rigfun_paths. use funextfun. intros x. use homotinvweqweq.
- use rigfun_paths. use funextfun. intros y. use homotweqinvweq.
Opaque commrig_equiv_is_z_iso.use make_is_inverse_in_precat.
- use rigfun_paths. use funextfun. intros x. use homotinvweqweq.
- use rigfun_paths. use funextfun. intros y. use homotweqinvweq.
Lemma commrig_equiv_iso (X Y : ob commrig_category) :
rigiso (X : commrig) (Y : commrig) -> z_iso X Y.
Show proof.
Lemma commrig_iso_equiv_is_equiv (X Y : commrig_category) : isweq (commrig_iso_equiv X Y).
Show proof.
use isweq_iso.
- exact (commrig_equiv_iso X Y).
- intros x. use z_iso_eq. use rigfun_paths. apply idpath.
- intros y. use rigiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ apply idpath.
Opaque commrig_iso_equiv_is_equiv.- exact (commrig_equiv_iso X Y).
- intros x. use z_iso_eq. use rigfun_paths. apply idpath.
- intros y. use rigiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ apply idpath.
Definition commrig_iso_equiv_weq (X Y : ob commrig_category) :
weq (z_iso X Y) (rigiso (X : commrig) (Y : commrig)).
Show proof.
Lemma commrig_equiv_iso_is_equiv (X Y : ob commrig_category) : isweq (commrig_equiv_iso X Y).
Show proof.
use isweq_iso.
- exact (commrig_iso_equiv X Y).
- intros y. use rigiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ apply idpath.
- intros x. use z_iso_eq. use rigfun_paths. apply idpath.
Opaque commrig_equiv_iso_is_equiv.- exact (commrig_iso_equiv X Y).
- intros y. use rigiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ apply idpath.
- intros x. use z_iso_eq. use rigfun_paths. apply idpath.
Definition commrig_equiv_weq_iso (X Y : ob commrig_category) :
(rigiso (X : commrig) (Y : commrig)) ≃ (z_iso X Y).
Show proof.
Definition commrig_category_isweq (X Y : ob commrig_category) :
isweq (λ p : X = Y, idtoiso p).
Show proof.
use (@isweqhomot
(X = Y) (z_iso X Y)
(pr1weq (weqcomp (commrig_univalence X Y) (commrig_equiv_weq_iso X Y)))
_ _ (weqproperty (weqcomp (commrig_univalence X Y) (commrig_equiv_weq_iso X Y)))).
intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use total2_paths_f.
- apply idpath.
- use proofirrelevance. use isaprop_is_z_isomorphism.
Opaque commrig_category_isweq.(X = Y) (z_iso X Y)
(pr1weq (weqcomp (commrig_univalence X Y) (commrig_equiv_weq_iso X Y)))
_ _ (weqproperty (weqcomp (commrig_univalence X Y) (commrig_equiv_weq_iso X Y)))).
intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use total2_paths_f.
- apply idpath.
- use proofirrelevance. use isaprop_is_z_isomorphism.
Definition commrig_category_is_univalent : is_univalent commrig_category.
Show proof.
Definition commrig_univalent_category : univalent_category :=
make_univalent_category commrig_category commrig_category_is_univalent.
End def_commrig_category.