Library UniMath.Bicategories.Core.Examples.TwoType

The fundamental groupoid of a 2-type.
Authors: Dan Frumin, Niels van der Weide
Ported from: https://github.com/nmvdw/groupoids
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Local Open Scope cat.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Core.EquivToAdjequiv.
Require Import UniMath.Bicategories.Core.AdjointUnique.
Local Open Scope bicategory_scope.

Section TwoTypeBiGroupoid.
  Variable (X : Type)
           (HX : isofhlevel 4 X).

  Definition two_type_bicat_data
    : prebicat_data.
  Show proof.
    use build_prebicat_data.
    - exact X.
    - exact (λ x y, x = y).
    - exact (λ _ _ p q, p = q).
    - exact (fun _ => idpath _).
    - exact (λ _ _ _ p q, p @ q).
    - exact (λ _ _ p, idpath p).
    - exact (λ _ _ _ _ _ q₁ q₂, q₁ @ q₂).
    - exact (λ _ _ _ p _ _ r, maponpaths (λ s, p @ s) r).
    - exact (λ _ _ _ _ _ q r, maponpaths (λ s, s @ q) r).
    - exact (λ _ _ p, idpath p).
    - exact (λ _ _ p, idpath p).
    - exact (λ _ _ p, pathscomp0rid p).
    - exact (λ _ _ p, !(pathscomp0rid p)).
    - exact (λ _ _ _ _ p q r, path_assoc p q r).
    - exact (λ _ _ _ _ p q r, !(path_assoc p q r)).

  Lemma two_type_bicat_laws
    : prebicat_laws two_type_bicat_data.
  Show proof.
    repeat (use tpair) ; try (intros; apply idpath).
    - intros ; cbn in *.
      apply pathscomp0rid.
    - intros ; cbn in *.
      apply path_assoc.
    - intros ; cbn in *.
      symmetry.
      apply maponpathscomp0.
    - intros ; cbn in *.
      rewrite maponpathscomp0.
      apply idpath.
    - intros x y p₁ p₂ q ; cbn in *.
      induction q ; cbn.
      apply idpath.
    - intros x y p₁ p₂ q ; cbn in *.
      induction q ; cbn.
      exact (!(pathscomp0rid _)).
    - intros w x y z p₁ p₂ p₃ p₄ q ; cbn in *.
      induction q ; cbn.
      exact (!(pathscomp0rid _)).
    - intros w x y z p₁ p₂ p₃ p₄ q ; cbn in *.
      induction q ; cbn.
      exact (!(pathscomp0rid _)).
    - intros w x y z p₁ p₂ p₃ p₄ q ; cbn in *.
      induction q ; cbn.
      exact ((pathscomp0rid _)).
    - intros w x y z p₁ p₂ p₃ p₄ q ; cbn in *.
      induction q ; cbn.
      exact ((pathscomp0rid _)).
    - intros x y p ; cbn in *.
      apply pathsinv0r.
    - intros x y p ; cbn in *.
      apply pathsinv0l.
    - intros w x y z p₁ p₂ p₃ ; cbn in *.
      apply pathsinv0r.
    - intros w x y z p₁ p₂ p₃ ; cbn in *.
      apply pathsinv0l.
    - intros x y z p q ; cbn in *.
      induction p ; cbn.
      apply idpath.
    - intros v w x y z p₁ p₂ p₃ p₄ ; cbn in *.
      induction p₁, p₂, p₃, p₄ ; cbn.
      apply idpath.

  Definition fundamental_bigroupoid
    : bicat.
  Show proof.
    use build_bicategory.
    - exact two_type_bicat_data.
    - exact two_type_bicat_laws.
    - intros x y p₁ p₂ ; cbn in *.
      exact (HX x y p₁ p₂).

Each 2-cell is an iso
  Definition fundamental_groupoid_2cell_iso
             {x y : fundamental_bigroupoid}
             {p₁ p₂ : fundamental_bigroupoid⟦x,y⟧}
             (s : p₁ ==> p₂)
    : is_invertible_2cell s.
  Show proof.
    refine (!s ,, _).
    split ; cbn.
    - apply pathsinv0r.
    - apply pathsinv0l.

Each 1-cell is an adjoint equivalence
  Definition fundamental_bigroupoid_1cell_equivalence
             {x y : fundamental_bigroupoid}
             (p : fundamental_bigroupoid⟦x,y⟧)
    : left_equivalence p.
  Show proof.
    use tpair.
    - refine (!p ,, _).
      split ; cbn.
      + exact (! (pathsinv0r p)).
      + exact (pathsinv0l p).
    - split ; cbn.
      + apply fundamental_groupoid_2cell_iso.
      + apply fundamental_groupoid_2cell_iso.

  Definition fundamental_bigroupoid_1cell_adj_equiv
             {x y : fundamental_bigroupoid}
             (p : fundamental_bigroupoid⟦x,y⟧)
    : left_adjoint_equivalence p
    := equiv_to_isadjequiv p (fundamental_bigroupoid_1cell_equivalence p).

It is univalent
  Definition fundamental_bigroupoid_is_univalent_2_1
    : is_univalent_2_1 fundamental_bigroupoid.
  Show proof.
    intros x y p₁ p₂.
    use isweq_iso ; cbn in *.
    - intros q.
      apply q.
    - intros q.
      induction q ; cbn.
      apply idpath.
    - intros q.
      induction q as [q Hq].
      induction q ; cbn.
      use subtypePath ; cbn.
      + intro. apply (isaprop_is_invertible_2cell (C:=fundamental_bigroupoid)).
      + apply idpath.

  Definition fundamental_bigroupoid_is_univalent_2_0
    : is_univalent_2_0 fundamental_bigroupoid.
  Show proof.
    intros x y.
    use isweq_iso.
    - intros p.
      apply p.
    - intros p ; cbn in *.
      induction p ; cbn.
      apply idpath.
    - intros p ; cbn in *.
      apply path_internal_adjoint_equivalence.
      + apply fundamental_bigroupoid_is_univalent_2_1.
      + cbn in *.
        induction (pr1 p) ; cbn.
        apply idpath.

  Definition fundamental_bigroupoid_is_univalent_2
    : is_univalent_2 fundamental_bigroupoid.
  Show proof.
    split.
    - exact fundamental_bigroupoid_is_univalent_2_0.
    - exact fundamental_bigroupoid_is_univalent_2_1.

End TwoTypeBiGroupoid.