# 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.
Local Open Scope bicategory_scope.

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

Definition two_type_bicat_data
: prebicat_data.
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)).
Defined.

Definition two_type_bicat_laws
: prebicat_laws two_type_bicat_data.
Proof.
repeat (use tpair) ; try reflexivity.
- intros ; cbn in ×.
apply pathscomp0rid.
- intros ; cbn in ×.
apply path_assoc.
- intros ; cbn in ×.
symmetry.
apply maponpathscomp0.
- intros ; cbn in ×.
rewrite maponpathscomp0.
reflexivity.
- intros x y p₁ p₂ q ; cbn in ×.
induction q ; cbn.
reflexivity.
- 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.
reflexivity.
- intros v w x y z p₁ p₂ p₃ p₄ ; cbn in ×.
induction p₁, p₂, p₃, p₄ ; cbn.
reflexivity.
Qed.

Definition fundamental_bigroupoid
: bicat.
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₂).
Defined.

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

Each 1-cell is an adjoint equivalence
Definition fundamental_bigroupoid_1cell_equivalence
{x y : fundamental_bigroupoid}
(p : fundamental_bigroupoidx,y)
: left_equivalence p.
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.
Defined.

{x y : fundamental_bigroupoid}
(p : fundamental_bigroupoidx,y)

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

Definition fundamental_bigroupoid_is_univalent_2_0
: is_univalent_2_0 fundamental_bigroupoid.
Proof.
intros x y.
use isweq_iso.
- intros p.
apply p.
- intros p ; cbn in ×.
induction p ; cbn.
reflexivity.
- intros p ; cbn in ×.
+ apply fundamental_bigroupoid_is_univalent_2_1.
+ cbn in ×.
induction (pr1 p) ; cbn.
reflexivity.
Defined.

Definition fundamental_bigroupoid_is_univalent_2
: is_univalent_2 fundamental_bigroupoid.
Proof.
split.
- exact fundamental_bigroupoid_is_univalent_2_0.
- exact fundamental_bigroupoid_is_univalent_2_1.
Defined.

End TwoTypeBiGroupoid.