Require Import Category.Core Functor.Core.
Require Import Functor.Paths.
Require Import Functor.Identity Functor.Composition.Core.
Require Import ExponentialLaws.Law4.Functors.
Require Import ExponentialLaws.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope functor_scope.

Section Law4.
  Context `{Funext}.
  Variables C1 C2 D : PreCategory.

  Lemma helper1 c
  : functor C1 C2 D (inverse C1 C2 D c) = c.
  Proof.
    path_functor.
    abstract (
        exp_laws_t;
        rewrite <- composition_of;
        exp_laws_t
      ).
  Defined.

  Lemma helper2_helper c x
  : inverse C1 C2 D (functor C1 C2 D c) x = c x.
  Proof.
    path_functor.
    abstract exp_laws_t.
  Defined.

  Lemma helper2 c
  : inverse C1 C2 D (functor C1 C2 D c) = c.
  Proof.
    path_functor.
    ∃ (path_forall _ _ (helper2_helper c)).
    abstract (unfold helper2_helper; exp_laws_t).
  Defined.

  Lemma law
  : functor C1 C2 D o inverse C1 C2 D = 1
    ∧ inverse C1 C2 D o functor C1 C2 D = 1.
  Proof.
    split;
    path_functor;
    [ (∃ (path_forall _ _ helper1))
    | (∃ (path_forall _ _ helper2)) ];
    unfold helper1, helper2, helper2_helper;
    exp_laws_t.
  Qed.
End Law4.