Library UniMath.CategoryTheory.categories.commrings
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_commring_precategory.
Definition commring_fun_space (A B : commring) : hSet := make_hSet (ringfun A B) (isasetrigfun A B).
Definition commring_precategory_ob_mor : precategory_ob_mor :=
tpair (λ ob : UU, ob -> ob -> UU) commring (λ A B : commring, commring_fun_space A B).
Definition commring_precategory_data : precategory_data :=
make_precategory_data
commring_precategory_ob_mor (λ (X : commring), (rigisotorigfun (idrigiso X)))
(fun (X Y Z : commring) (f : ringfun X Y) (g : ringfun Y Z) => rigfuncomp f g).
Local Lemma commring_id_left (X Y : commring) (f : ringfun X Y) :
rigfuncomp (rigisotorigfun (idrigiso X)) f = f.
Show proof.
Opaque commring_id_left.
Local Lemma commring_id_right (X Y : commring) (f : ringfun X Y) :
rigfuncomp f (rigisotorigfun (idrigiso Y)) = f.
Show proof.
Opaque commring_id_right.
Local Lemma commring_assoc (X Y Z W : commring) (f : ringfun X Y) (g : ringfun Y Z)
(h : ringfun Z W) : rigfuncomp f (rigfuncomp g h) = rigfuncomp (rigfuncomp f g) h.
Show proof.
Opaque commring_assoc.
Lemma is_precategory_commring_precategory_data : is_precategory commring_precategory_data.
Show proof.
Definition commring_precategory : precategory :=
make_precategory commring_precategory_data is_precategory_commring_precategory_data.
Lemma has_homsets_commring_precategory : has_homsets commring_precategory.
Show proof.
End def_commring_precategory.
Definition commring_fun_space (A B : commring) : hSet := make_hSet (ringfun A B) (isasetrigfun A B).
Definition commring_precategory_ob_mor : precategory_ob_mor :=
tpair (λ ob : UU, ob -> ob -> UU) commring (λ A B : commring, commring_fun_space A B).
Definition commring_precategory_data : precategory_data :=
make_precategory_data
commring_precategory_ob_mor (λ (X : commring), (rigisotorigfun (idrigiso X)))
(fun (X Y Z : commring) (f : ringfun X Y) (g : ringfun Y Z) => rigfuncomp f g).
Local Lemma commring_id_left (X Y : commring) (f : ringfun X Y) :
rigfuncomp (rigisotorigfun (idrigiso X)) f = f.
Show proof.
Opaque commring_id_left.
Local Lemma commring_id_right (X Y : commring) (f : ringfun X Y) :
rigfuncomp f (rigisotorigfun (idrigiso Y)) = f.
Show proof.
Opaque commring_id_right.
Local Lemma commring_assoc (X Y Z W : commring) (f : ringfun X Y) (g : ringfun Y Z)
(h : ringfun Z W) : rigfuncomp f (rigfuncomp g h) = rigfuncomp (rigfuncomp f g) h.
Show proof.
Opaque commring_assoc.
Lemma is_precategory_commring_precategory_data : is_precategory commring_precategory_data.
Show proof.
use make_is_precategory_one_assoc.
- intros a b f. use commring_id_left.
- intros a b f. use commring_id_right.
- intros a b c d f g h. use commring_assoc.
- intros a b f. use commring_id_left.
- intros a b f. use commring_id_right.
- intros a b c d f g h. use commring_assoc.
Definition commring_precategory : precategory :=
make_precategory commring_precategory_data is_precategory_commring_precategory_data.
Lemma has_homsets_commring_precategory : has_homsets commring_precategory.
Show proof.
End def_commring_precategory.
Section def_commring_category.
Definition commring_category : category := make_category _ has_homsets_commring_precategory.
Definition commring_category : category := make_category _ has_homsets_commring_precategory.
Lemma commring_iso_is_equiv (A B : ob commring_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 commring_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 commring_iso_equiv (X Y : ob commring_category) :
z_iso X Y -> ringiso (X : commring) (Y : commring).
Show proof.
intro f.
use make_ringiso.
- exact (make_weq (pr1 (pr1 f)) (commring_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
use make_ringiso.
- exact (make_weq (pr1 (pr1 f)) (commring_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
Lemma commring_equiv_is_z_iso (X Y : ob commring_category)
(f : ringiso (X : commring) (Y : commring)) :
@is_z_isomorphism commring_category X Y (ringfunconstr (pr2 f)).
Show proof.
exists (ringfunconstr (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 commring_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 commring_equiv_iso (X Y : ob commring_category) :
ringiso (X : commring) (Y : commring) -> z_iso X Y.
Show proof.
Lemma commring_iso_equiv_is_equiv (X Y : commring_category) : isweq (commring_iso_equiv X Y).
Show proof.
use isweq_iso.
- exact (commring_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 commring_iso_equiv_is_equiv.- exact (commring_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 commring_iso_equiv_weq (X Y : ob commring_category) :
weq (z_iso X Y) (ringiso (X : commring) (Y : commring)).
Show proof.
Lemma commring_equiv_iso_is_equiv (X Y : ob commring_category) : isweq (commring_equiv_iso X Y).
Show proof.
use isweq_iso.
- exact (commring_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 commring_equiv_iso_is_equiv.- exact (commring_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 commring_equiv_weq_iso (X Y : ob commring_category) :
(ringiso (X : commring) (Y : commring)) ≃ (z_iso X Y).
Show proof.
Definition commring_category_isweq (X Y : ob commring_category) :
isweq (λ p : X = Y, idtoiso p).
Show proof.
use (@isweqhomot
(X = Y) (z_iso X Y)
(pr1weq (weqcomp (commring_univalence X Y) (commring_equiv_weq_iso X Y)))
_ _ (weqproperty (weqcomp (commring_univalence X Y) (commring_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 commring_category_isweq.(X = Y) (z_iso X Y)
(pr1weq (weqcomp (commring_univalence X Y) (commring_equiv_weq_iso X Y)))
_ _ (weqproperty (weqcomp (commring_univalence X Y) (commring_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 commring_category_is_univalent : is_univalent commring_category.
Show proof.
Definition commring_univalent_category : univalent_category :=
make_univalent_category commring_category commring_category_is_univalent.
End def_commring_category.