Require Import Category.Core Functor.Core Functor.Identity Functor.Paths ExponentialLaws.Law1.Functors Functor.Composition.Core.
Require Import InitialTerminalCategory.Core.
Require Import Basics.Trunc ExponentialLaws.Tactics.
Require Import Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope functor_scope.

Section law1.
  Context `{Funext}.
  Context `{IsInitialCategory zero}.
  Context `{IsTerminalCategory one}.
  Local Notation "0" := zero : category_scope.
  Local Notation "1" := one : category_scope.

  Variable C : PreCategory.

  Definition helper (c : Functor 1 C)
  : Functors.from_terminal C (c (center _)) = c.
  Proof.
    path_functor.
    ∃ (path_forall _ _ (fun x ⇒ ap (object_of c) (contr _))).
    abstract (
        exp_laws_t;
        simpl;
        rewrite <- identity_of;
        f_ap;
        symmetry;
        apply contr
      ).
  Defined.

  Lemma law
  : @functor _ one _ C o inverse C = 1
    ∧ inverse C o @functor _ one _ C = 1.
  Proof.
    split;
    path_functor.
    ∃ (path_forall _ _ helper).
    unfold helper.
    exp_laws_t.
  Qed.
End law1.