Require Import Category.Core Functor.Core NaturalTransformation.Core.
Require Import Functor.Paths NaturalTransformation.Paths.
Require Import HoTT.Tactics Basics.PathGroupoids Types.Forall Types.Prod.

Ltac exp_laws_misc_t' :=
  idtac;
  match goal with
    | _ ⇒ reflexivity
    | _ ⇒ progress intros
    | _ ⇒ progress simpl in ×
    | _ ⇒ apply (@path_forall _); intro
    | _ ⇒ rewrite !identity_of
    | _ ⇒ progress autorewrite with morphism
  end.

Ltac exp_laws_simplify_types' :=
  idtac;
  match goal with
    | [ H : (_ + _) |- _ ] ⇒ destruct H
    | [ H : Unit |- _ ] ⇒ destruct H
    | [ H : Empty |- _ ] ⇒ destruct H
    | [ H : (_ × _) |- _ ] ⇒ destruct H
    | [ |- _ = _ :> Functor _ _ ] ⇒ progress path_functor
    | [ |- _ = _ :> NaturalTransformation _ _ ] ⇒ progress path_natural_transformation
    | [ |- _ = _ :> prod _ _ ] ⇒ apply path_prod
  end.

Ltac exp_laws_handle_contr' :=
  idtac;
  match goal with
    | [ H : Contr ?T, x : ?T |- _ ] ⇒ progress destruct (contr x)
    | [ H : ∀ a, Contr (?T a), x : ?T _ |- _ ] ⇒ progress destruct (contr x)
    | [ H : ∀ a b, Contr (?T a b), x : ?T _ _ |- _ ] ⇒ progress destruct (contr x)
    | [ |- context[contr (center ?x)] ]
      ⇒ progress let H := fresh in
                  assert (H : idpath = contr (center x)) by exact (center _);
                    destruct H
  end.

Ltac exp_laws_handle_transport' :=
  idtac;
  match goal with
    | _ ⇒ progress rewrite ?transport_forall_constant, ?path_forall_2_beta, ?transport_const, ?transport_path_prod
    | [ |- context [path_functor_uncurried ?F ?G (?x; ?y)] ] (* https://coq.inria.fr/bugs/show_bug.cgi?id=3768 *)
      ⇒ rewrite (@path_functor_uncurried_fst _ _ _ F G x y)
    | [ |- context[transport (fun y : Functor ?C ?D ⇒ ?f (y _0 ?x)%object)] ]
      ⇒ rewrite (fun a b ⇒ @transport_compose _ _ a b (fun y' ⇒ f (y' x)) (@object_of C D))
    | [ |- context[transport (fun y : Functor ?C ?D ⇒ ?f (y _0 ?x)%object ?z)] ]
      ⇒ rewrite (fun a b ⇒ @transport_compose _ _ a b (fun y' ⇒ f (y' x) z) (@object_of C D))
    | [ |- context[transport (fun y : Functor ?C ?D ⇒ ?f (y _0 ?x)%object ?z)] ]
      ⇒ rewrite (fun a b ⇒ @transport_compose _ _ a b (fun y' ⇒ f (y' x) z) (@object_of C D))
    | [ |- context[transport (fun y : Functor ?C ?D ⇒ ?f (?g (y _0 ?x)%object))] ]
      ⇒ rewrite (fun a b ⇒ @transport_compose _ _ a b (fun y' ⇒ f (g (y' x))) (@object_of C D))
    | [ |- context[transport (fun y : Functor ?C ?D ⇒ ?f (?g (y _0 ?x)%object) ?z)] ]
      ⇒ rewrite (fun a b ⇒ @transport_compose _ _ a b (fun y' ⇒ f (g (y' x)) z) (@object_of C D))
    | _ ⇒ progress transport_path_forall_hammer
    | [ |- context[components_of (transport ?P ?p ?z)] ]
      ⇒ simpl rewrite (@ap_transport _ P _ _ _ p (fun _ ⇒ components_of) z)
    | [ |- context[object_of (transport ?P ?p ?z)] ]
      ⇒ simpl rewrite (@ap_transport _ P _ _ _ p (fun _ ⇒ object_of) z)
    | [ |- context[morphism_of (transport ?P ?p ?z)] ]
      ⇒ simpl rewrite (@ap_transport _ P _ _ _ p (fun _ ⇒ morphism_of) z)
    | [ |- context[fst (transport ?P ?p ?z)] ]
      ⇒ simpl rewrite (@ap_transport _ P _ _ _ p (fun _ ⇒ fst) z)
    | [ |- context[snd (transport ?P ?p ?z)] ]
      ⇒ simpl rewrite (@ap_transport _ P _ _ _ p (fun _ ⇒ snd) z)
    | [ |- context[pr1 (transport ?P ?p ?z)] ]
      ⇒ simpl rewrite (@ap_transport _ P _ _ _ p (fun _ ⇒ pr1) z)
  end.

Ltac exp_laws_t' :=
  first [ exp_laws_misc_t'
        | exp_laws_simplify_types'
        | exp_laws_handle_contr'
        | exp_laws_handle_transport' ].

Ltac exp_laws_t := repeat exp_laws_t'.