Require Import HoTT.Basics HoTT.Types.
Require Import Category.Core Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Prod Functor.Prod Functor.Composition.Core Functor.Identity Functor.Composition.Laws.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.
Local Open Scope functor_scope.

Local Notation prod_type := Basics.Overture.prod.
Local Notation fst_type := Basics.Overture.fst.
Local Notation snd_type := Basics.Overture.snd.
Local Notation pair_type := Basics.Overture.pair.

Module Swap.
  Definition functor (C D : PreCategory)
  : Functor (C × D) (D × C)
    := Build_Functor (C × D) (D × C)
                     (fun cd ⇒ (snd_type cd, fst_type cd)%core)
                     (fun _ _ m ⇒ (snd_type m, fst_type m)%core)
                     (fun _ _ _ _ _ ⇒ idpath)
                     (fun _ ⇒ idpath).

  Definition law (C D : PreCategory)
  : functor C D o functor D C = 1
    := idpath.
End Swap.

Module Associativity.
  Section associativity.
    Variables A B C : PreCategory.

    Definition functor : Functor (A × (B × C)) ((A × B) × C)
      := (fst × (fst o snd)) × (snd o snd).
    Definition inverse : Functor ((A × B) × C) (A × (B × C))
      := (fst o fst) × ((snd o fst) × snd).

    Definition law
    : functor o inverse = 1
      ∧ inverse o functor = 1
      := (idpath, idpath)%core.
  End associativity.
End Associativity.

Module Law0.
  Section law0.
    Context `{Funext}.
    Context `{IsInitialCategory zero}.
    Local Notation "0" := zero : category_scope.

    Variable C : PreCategory.

    #[export] Instance is_initial_category__product
    : IsInitialCategory (C × 0)
      := fun P c ⇒ initial_category_ind P (snd c).

    #[export] Instance is_initial_category__product'
    : IsInitialCategory (0 × C)
      := fun P c ⇒ initial_category_ind P (fst c).

    Definition functor : Functor (C × 0) 0 := Functors.from_initial _.
    Definition functor' : Functor (0 × C) 0 := Functors.from_initial _.
    Definition inverse : Functor 0 (C × 0) := Functors.from_initial _.
    Definition inverse' : Functor 0 (0 × C) := Functors.from_initial _.

    Definition law
    : functor o inverse = 1
      ∧ inverse o functor = 1
      := center _.

    Definition law'
    : functor' o inverse' = 1
      ∧ inverse' o functor' = 1
      := center _.
  End law0.
End Law0.

Module Law1.
  Section law1.
    Context `{Funext}.
    Context `{IsTerminalCategory one}.
    Local Notation "1" := one : category_scope.
    Variable C : PreCategory.

    Definition functor : Functor (C × 1) C
      := fst.

    Definition functor' : Functor (1 × C) C
      := snd.

    Definition inverse : Functor C (C × 1)
      := 1 × Functors.to_terminal _.

    Definition inverse' : Functor C (1 × C)
      := Functors.to_terminal _ × 1.

    Local Ltac t_prod :=
      split;
      try first [ exact (compose_fst_prod _ _)
                | exact (compose_snd_prod _ _) ];
      [];
      apply Functor.Prod.Universal.path_prod;
      rewrite <- !Functor.Composition.Laws.associativity by assumption;
      (rewrite ?compose_fst_prod, ?compose_snd_prod,
       ?Functor.Composition.Laws.left_identity,
       ?Functor.Composition.Laws.right_identity
        by assumption);
      try (reflexivity || exact (center _)).

    Lemma law1
    : functor o inverse = 1
      ∧ inverse o functor = 1.
    Proof.
      unfold functor, inverse.
      t_prod.
    Qed.

    Lemma law1'
    : functor' o inverse' = 1
      ∧ inverse' o functor' = 1.
    Proof.
      unfold functor', inverse'.
      t_prod.
    Qed.
  End law1.
End Law1.