Require Import Category.Core Category.Univalent Category.Morphisms.
Require Import Structure.Core.
Require Import Types.Sigma Trunc Equivalences.
Require Import Basics.Iff Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope path_scope.
Local Open Scope category_scope.
Local Open Scope morphism_scope.
Local Open Scope structure_scope.

Section sip.
  Variable X : PreCategory.
  Variable P : NotionOfStructure X.
  Context `{IsCategory X}.
  Context `{@IsStandardNotionOfStructure X P}.

  Let StrX := @precategory_of_structures X P.

  Definition sip_isotoid_helper (xa yb : StrX)
             (f : xa <~=~> yb)
  : xa.1 <~=~> yb.1.
  Proof.
    ∃ (PreCategoryOfStructures.f (f : morphism _ _ _)).
    ∃ (PreCategoryOfStructures.f f^-1).
    - exact (ap (@PreCategoryOfStructures.f _ _ _ _) (@left_inverse _ _ _ _ f)).
    - exact (ap (@PreCategoryOfStructures.f _ _ _ _) (@right_inverse _ _ _ _ f)).
  Defined.

  Lemma sip_isotoid_helper_refl (xa : StrX)
  : @sip_isotoid_helper xa xa (reflexivity _) = reflexivity _.
  Proof.
    unfold sip_isotoid_helper, reflexivity, isomorphic_refl.
    apply ap.
    apply path_ishprop.
  Defined.

  Lemma sip_helper x y (p : x = y) (a : P x) (b : P y)
  : transport P p a = b
    ↔ is_structure_homomorphism P _ _ (idtoiso X p) a b ×
        is_structure_homomorphism P _ _ (idtoiso X p)^-1 b a.
  Proof.
    split.
    - intros; path_induction; split; apply reflexivity.
    - intros [H0 H1]; path_induction; simpl in ×.
      apply antisymmetry_structure; assumption.
  Defined.

  Definition sip_isotoid (xa yb : StrX)
             (f : xa <~=~> yb)
  : xa = yb.
  Proof.
    refine (path_sigma_uncurried
              _ _ _
              (isotoid
                 X
                 xa.1
                 yb.1
                 (sip_isotoid_helper f);
               _)).
    apply sip_helper; simpl.
    split;
      lazymatch goal with
        | [ |- context[idtoiso ?X ((isotoid ?X ?x ?y) ?m)] ]
          ⇒ pose proof (eisretr (@idtoiso X x y) m) as H';
             pattern (idtoiso X ((isotoid X x y) m))
      end;
      refine (transport _ H'^ _); clear H'; simpl;
      apply PreCategoryOfStructures.h.
  Defined.

  Lemma sip_isotoid_refl xa
  : @sip_isotoid xa xa (reflexivity _) = reflexivity _.
  Proof.
    refine (_ @ eta_path_sigma_uncurried _).
    refine (ap (path_sigma_uncurried _ _ _) _).
    apply equiv_path_sigma_hprop.
    simpl.
    refine (_ @ eisretr (isotoid X xa.1 xa.1) 1%path).
    apply ap.
    apply sip_isotoid_helper_refl.
  Defined.

  Lemma path_f_idtoiso_precategory_of_structures xa yb (p : xa = yb)
  : PreCategoryOfStructures.f (idtoiso (precategory_of_structures P) p : morphism _ _ _)
    = idtoiso X p..1.
  Proof.
    induction p; reflexivity.
  Defined.

  Lemma structure_identity_principle_helper
        (xa yb : StrX)
        (x : xa <~=~> yb)
  : PreCategoryOfStructures.f
      (idtoiso (precategory_of_structures P) (sip_isotoid x) : morphism _ _ _)
    = PreCategoryOfStructures.f (x : morphism _ _ _).
  Proof.
    refine (path_f_idtoiso_precategory_of_structures _ @ _).
    refine ((ap _ (ap _ _))
              @ (ap (@morphism_isomorphic _ _ _)
                    (eisretr (@idtoiso X xa.1 yb.1) (sip_isotoid_helper _)))).
    exact (pr1_path_sigma_uncurried _).
  Defined.

  #[export] Instance structure_identity_principle
  : IsCategory (precategory_of_structures P).
  Proof.
    intros xa yb.
    refine (isequiv_adjointify
              _ (@sip_isotoid xa yb)
              _ _);
      intro; simpl in ×.
    - abstract (
          apply path_isomorphic; simpl;
          apply PreCategoryOfStructures.path_morphism;
          apply structure_identity_principle_helper
        ).
    - abstract (induction x; apply sip_isotoid_refl).
  Defined.
End sip.