Library UniMath.CategoryTheory.category_binops

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.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 BINOPS_precategory.

  Definition binops_fun_space (A B : setwithbinop) : hSet :=
    make_hSet _ (isasetbinopfun A B).

  Definition binops_precategory_ob_mor : precategory_ob_mor :=
    tpair (λ ob : UU, ob -> ob -> UU) setwithbinop
          (λ A B : setwithbinop, binops_fun_space A B).

  Definition idbinopfun (A : setwithbinop) : binopfun A A.
  Show proof.
    use make_binopfun. intros a. exact a.
    intros a a'.
    apply idpath.

  Definition idbinopfun_remove_left (A B : setwithbinop) (f : binopfun A B) :
    binopfuncomp (idbinopfun A) f = f.
  Show proof.
    unfold binopfuncomp. unfold idbinopfun.
    use total2_paths_f. cbn. apply idpath.
    apply proofirrelevance. apply isapropisbinopfun.

  Definition idbinopfun_remove_right (A B : setwithbinop) (f : binopfun A B) :
    binopfuncomp f (idbinopfun B) = f.
  Show proof.
    unfold binopfuncomp. unfold idbinopfun.
    use total2_paths_f. cbn. apply idpath.
    apply proofirrelevance. apply isapropisbinopfun.

  Definition binopfuncomp_assoc (A B C D : setwithbinop) (f : binopfun A B)
             (g : binopfun B C) (h : binopfun C D) :
    binopfuncomp (binopfuncomp f g) h = binopfuncomp f (binopfuncomp g h).
  Show proof.
    unfold binopfuncomp. apply maponpaths.
    apply isapropisbinopfun.

  Definition binop_precategory_data : precategory_data :=
    make_precategory_data binops_precategory_ob_mor
                          (λ (A : setwithbinop), idbinopfun A )
                          (fun (A B C : setwithbinop) (f : binopfun A B)
                             (g : binopfun B C) => binopfuncomp f g).

  Lemma is_precategory_binop_precategory_data :
    is_precategory binop_precategory_data.
  Show proof.
    repeat split; cbn.

    intros a b f. apply idbinopfun_remove_left.
    intros a b f. apply idbinopfun_remove_right.

    intros a b c d f g h. apply pathsinv0.
    apply (binopfuncomp_assoc a b c d f g h).

    intros a b c d f g h.
    apply (binopfuncomp_assoc a b c d f g h).

  Definition binop_precategory : precategory :=
    tpair _ _ is_precategory_binop_precategory_data.

  Lemma has_homsets_BINOP : has_homsets binop_precategory.
  Show proof.
intros a b; apply isasetbinopfun.

End BINOPS_precategory.

Section BINOP_category.

  Definition binop_category : category := make_category _ has_homsets_BINOP.
  Notation BINOP := binop_category.

Equivalence between isomorphisms and binopisos


  Lemma binop_iso_is_equiv (A B : ob BINOP)
        (f : z_iso A B) : isweq (pr1 (pr1 f)).
  Show proof.
    apply (isweq_iso _ (pr1binopfun _ _ (inv_from_z_iso f))).
    - intro x.
      set (T:=z_iso_inv_after_z_iso f).
      apply subtypeInjectivity in T.
      set (T':=toforallpaths _ _ _ T). apply T'.
      intro x0.
      apply isapropisbinopfun.
    - intros y.

      set (T:=z_iso_after_z_iso_inv f).
      apply subtypeInjectivity in T.
      set (T':=toforallpaths _ _ _ T). apply T'.
      intros x0.
      apply isapropisbinopfun.

  Lemma binop_iso_equiv (A B : ob BINOP) : z_iso A B -> binopiso A B.
  Show proof.
    intro f.
    use make_binopiso.
    set (X := binop_iso_is_equiv A B f).
    apply (make_weq (pr1 (pr1 f)) X).
    apply (pr2 (pr1 f)).

  Lemma binop_equiv_is_z_iso (A B : setwithbinop)
        (f : binopiso A B) :
    @is_z_isomorphism BINOP A B (make_binopfun (pr1 (pr1 f)) (pr2 f)).
  Show proof.
    exists (make_binopfun (pr1 (pr1 (invbinopiso f)))
                                                  (pr2 (invbinopiso f))).
    split; cbn.
    - unfold compose, identity. cbn. unfold binopfuncomp, idbinopfun.
      cbn. use total2_paths_f. cbn. apply funextfun. intros x.
      apply homotinvweqweq. cbn. apply impred_isaprop. intros t.
      apply impred_isaprop. intros t0. apply (pr2 (pr1 A)).

    - use total2_paths_f. cbn. apply funextfun. intros x.
      apply homotweqinvweq. cbn. apply impred_isaprop. intros yt.
      apply impred_isaprop. intros t0. apply (pr2 (pr1 B)).

  Lemma binop_equiv_iso (A B : BINOP) : binopiso A B -> z_iso A B.
  Show proof.
    intro f.
    cbn in *.
    set (T := binop_equiv_is_z_iso A B f).
    exact (_,,T).

  Lemma binop_iso_equiv_is_equiv (A B : BINOP) : isweq (binop_iso_equiv A B).
  Show proof.
    apply (isweq_iso _ (binop_equiv_iso A B)).
    - intro; apply z_iso_eq. apply maponpaths.
      unfold binop_equiv_iso, binop_iso_equiv. cbn.
      use total2_paths_f.
      + cbn. unfold make_binopfun.
        apply subtypePath.
        * intros y. apply isapropisbinopfun.
        * apply maponpaths. apply subtypePath.
          -- unfold isPredicate.
             intros x0. apply isapropisbinopfun.
          -- apply idpath.
      + apply proofirrelevance.
        apply (isaprop_is_z_isomorphism(C:=BINOP)).
    - intros y. unfold binop_iso_equiv, binop_equiv_iso. cbn.
      use total2_paths_f.
      + cbn. unfold make_binopfun.
        apply subtypePath.
        * intros x. apply isapropisweq.
        * apply idpath.
      + apply proofirrelevance.
        apply isapropisbinopfun.

  Definition binop_iso_equiv_weq (A B : BINOP) : (z_iso A B) ≃ (binopiso A B).
  Show proof.
    exists (binop_iso_equiv A B).
    apply binop_iso_equiv_is_equiv.

  Lemma binop_equiv_iso_is_equiv (A B : BINOP) : isweq (binop_equiv_iso A B).
  Show proof.
    apply (isweq_iso _ (binop_iso_equiv A B)).
    intros x. apply subtypePath.
    intros y. apply isapropisbinopfun.

    unfold binop_equiv_iso, binop_iso_equiv. cbn.
    use total2_paths_f. cbn. apply idpath.
    apply isapropisweq.

    intros y. unfold binop_equiv_iso, binop_iso_equiv. cbn.
    use total2_paths_f. cbn. unfold make_binopfun. cbn.
    apply subtypePath. intros x. apply isapropisbinopfun.
    apply idpath. apply proofirrelevance.
    apply (isaprop_is_z_isomorphism(C:=BINOP)).

  Definition binop_equiv_weq_iso (A B : BINOP) :
    (binopiso A B) ≃ (z_iso A B).
  Show proof.
    exists (binop_equiv_iso A B).
    apply binop_equiv_iso_is_equiv.

  Definition binop_precategory_isweq (a b : BINOP) :
    isweq (λ p : a = b, idtoiso p).
  Show proof.
    use (@isweqhomot
           (a = b) (z_iso a b)
           (pr1weq (weqcomp (setwithbinop_univalence a b) (binop_equiv_weq_iso a b)))
           _ _ (weqproperty (weqcomp (setwithbinop_univalence a b) (binop_equiv_weq_iso a b)))).
    intros e. induction e.
    use (pathscomp0 weqcomp_to_funcomp_app).
    use total2_paths_f.
    - use idpath.
    - use proofirrelevance. use isaprop_is_z_isomorphism.
  Opaque binop_precategory_isweq.

  Definition binop_precategory_is_univalent : is_univalent binop_category.
  Show proof.
    intros a b. exact (binop_precategory_isweq a b).

End BINOP_category.