Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.HorizontalComposition.

Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory.
Require Import UniMath.Bicategories.WkCatEnrichment.Notations.

Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.

Local Open Scope cat.

Local Notation "C 'c×' D" := (precategory_binproduct C D)
 (at level 75, right associativity).

Section Build_Bicategory.

Variable C : bicat.

Definition bicate_ob_hom : prebicategory_ob_hom.
Show proof.

Definition bicate_id_comp : prebicategory_id_comp.
Show proof.


Definition bicate_lassociator_fun {a b c d : bicate_id_comp}
           (x : C ⟦ a, b ⟧ × C ⟦ b, c ⟧ × C ⟦ c, d ⟧)
  : pr1 x · (pr12 x · pr22 x) ==> pr1 x · pr12 x · pr22 x
  := lassociator (pr1 x) (pr12 x) (pr22 x).

Lemma bicate_lassociator_fun_natural {a b c d : bicate_id_comp}
  : is_nat_trans
      (functor_composite
         (pair_functor (functor_identity _) (compose_functor b c d))
         hcomp_functor)
      (functor_composite
         (precategory_binproduct_assoc
            (hom a b)
            (hom b c)
            (hom c d))
         (functor_composite
            (pair_functor (compose_functor a b c) (functor_identity _))
            hcomp_functor)) bicate_lassociator_fun.
Show proof.

Definition bicate_lassociator (a b c d : bicate_id_comp) : associator_trans_type a b c d.
Show proof.

Lemma bicate_transfs :
  (∏ a b c d : bicate_id_comp, associator_trans_type a b c d) ×
  (∏ a b : bicate_id_comp, left_unitor_trans_type a b) ×
  (∏ a b : bicate_id_comp, right_unitor_trans_type a b).
Show proof.

Definition bicate_data : prebicategory_data.
Show proof.

Lemma prebicat_associator_and_unitors_are_iso
  : associator_and_unitors_are_iso bicate_data.
Show proof.

Lemma triangle_identity {a b c : C} (f : C ⟦ a, b ⟧) (g : C ⟦ b, c ⟧)
  : id2 f ⋆ lunitor g =
    lassociator f (identity b) g • (runitor f ⋆ id2 g).
Show proof.

Lemma pentagon_identity {a b c d e : C}
      (k : C ⟦ a, b ⟧)
      (h : C ⟦ b, c ⟧)
      (g : C ⟦ c, d ⟧)
      (f : C ⟦ d, e ⟧)
  : lassociator k h (g · f) • lassociator (k · h) g f =
    ((id2 k ⋆ lassociator h g f) • lassociator k (h · g) f) •
    (lassociator k h g ⋆ id2 f).
Show proof.

Lemma prebicat_prebicategory_coherence
  : prebicategory_coherence bicate_data.
Show proof.

Hypothesis sc : isaset_cells C.

Lemma is_prebicategory_bicate : is_prebicategory bicate_data.
Show proof.

Definition prebicategory_of_prebicat : prebicategory.
Show proof.

End Build_Bicategory.