------------------------------------------------------------------------
-- The structure identity principle can be used to establish that
-- isomorphism coincides with equality (assuming univalence)
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Equality

module
  Univalence-axiom.Isomorphism-is-equality.Structure-identity-principle
    {reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

open import Bijection eq using (_↔_)
open import Category eq
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq hiding (_∘_; inverse)
open import Function-universe eq renaming (_∘_ to _⊚_)
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence using (_⇔_)
open import Prelude as P
open import Structure-identity-principle eq
open import Univalence-axiom eq
open import Univalence-axiom.Isomorphism-is-equality.Simple eq
  using (Assumptions; module Assumptions;
         Universe; module Universe;
         module Class)

-- The structure identity principle can be used to prove a slightly
-- restricted variant of isomorphism-is-equality (which is defined in
-- Univalence-axiom.Isomorphism-is-equality.Simple.Class).

isomorphism-is-equality′ :
  (Univ : Universe)  let open Universe Univ in
  Assumptions 
   c X Y 
  (∀ {B}  Is-set B  Is-set (El (proj₁ c) B))   -- Extra assumption.
  Is-set (proj₁ X)  Is-set (proj₁ Y)            -- Extra assumptions.
  Class.Isomorphic Univ c X Y  (X  Y)
isomorphism-is-equality′ Univ ass
  (a , P) (C , x , p) (D , y , q) El-set C-set D-set = isomorphic

  module Isomorphism-is-equality′ where

  open Assumptions ass
  open Universe Univ
  open Class Univ using (Isomorphic; Carrier)

  -- The category of sets and functions.

  Fun : Category (# 2) (# 1)
  Fun = category-Set (# 1) ext  _ _  univ₁)

  module Fun = Category Fun

  -- The category of sets and bijections.

  Bij : Category (# 2) (# 1)
  Bij = category-Set-≅ (# 1) ext  _ _  univ₁)

  module Bij = Category Bij

  -- If two sets are isomorphic, then the underlying types are
  -- equivalent.

  ≅⇒≃ : (C D : Fun.Obj)  C Fun.≅ D  Type C  Type D
  ≅⇒≃ C D = _≃_.from (≃≃≅-Set (# 1) ext C D)

  -- The "standard notion of structure" that the structure identity
  -- principle is instantiated with.

  S : Standard-notion-of-structure (# 1) (# 1) Bij.precategory
  S = record
    { P               = El a  Type
    ; H               = λ {C D} x y C≅D 
                          Is-isomorphism a (≅⇒≃ C D C≅D) x y
    ; H-prop          = λ {C D}  H-prop′ C D
    ; H-id            = λ {C}  H-id′ C
    ; H-∘             = λ {B C D}  H-∘′ B C D
    ; H-antisymmetric = λ {C}  H-antisymmetric′ C
    }
    where

    module Separate-abstract-block where

      abstract

        H-prop′ :
          (C D : SET (# 1))
          {x : El a (Type C)} {y : El a (Type D)}
          (f : Bij.Hom C D) 
          Is-proposition (Is-isomorphism a (≅⇒≃ C D f) x y)
        H-prop′ _ D _ = El-set (proj₂ D) _ _

        H-id′ :
          (C : SET (# 1)) {x : El a (Type C)} 
          Is-isomorphism a (≅⇒≃ C C (Bij.id {X = C})) x x
        H-id′ C {x} =
          resp a (≅⇒≃ C C (Bij.id {X = C})) x  ≡⟨ cong  eq  resp a eq x) $ Eq.lift-equality ext (refl _) 
          resp a Eq.id x                       ≡⟨ resp-id ass a x ⟩∎
          x                                    

        H-∘′ :
          (B C D : SET (# 1))
          {x : El a (Type B)} {y : El a (Type C)} {z : El a (Type D)}
          {B≅C : Bij.Hom B C} {C≅D : Bij.Hom C D} 
          Is-isomorphism a (≅⇒≃ B C B≅C) x y 
          Is-isomorphism a (≅⇒≃ C D C≅D) y z 
          Is-isomorphism a
            (≅⇒≃ B D (Bij._∙_ {X = B} {Y = C} {Z = D} C≅D B≅C)) x z
        H-∘′ B C D {x} {y} {z} {B≅C} {C≅D} x≅y y≅z =
          resp a (≅⇒≃ B D (C≅D Bij.∙ B≅C)) x             ≡⟨ cong  eq  resp a eq x) $ Eq.lift-equality ext (refl _) 
          resp a (≅⇒≃ C D C≅D  ≅⇒≃ B C B≅C) x           ≡⟨ resp-preserves-compositions (El a) (resp a) (resp-id ass a)
                                                                                        univ₁ ext (≅⇒≃ B C B≅C) (≅⇒≃ C D C≅D) x 
          resp a (≅⇒≃ C D C≅D) (resp a (≅⇒≃ B C B≅C) x)  ≡⟨ cong (resp a (≅⇒≃ C D C≅D)) x≅y 
          resp a (≅⇒≃ C D C≅D) y                         ≡⟨ y≅z ⟩∎
          z                                              

        H-antisymmetric′ :
          (C : SET (# 1))
          (x y : El a (Type C)) 
          Is-isomorphism a (≅⇒≃ C C (Bij.id {X = C})) x y 
          Is-isomorphism a (≅⇒≃ C C (Bij.id {X = C})) y x 
          x  y
        H-antisymmetric′ C x y x≡y _ =
          x                                    ≡⟨ sym $ resp-id ass a x 
          resp a Eq.id x                       ≡⟨ cong  eq  resp a eq x) $ Eq.lift-equality ext (refl _) 
          resp a (≅⇒≃ C C (Bij.id {X = C})) x  ≡⟨ x≡y ⟩∎
          y                                    

    open Separate-abstract-block

  open module S = Standard-notion-of-structure S
    using (H; Str; module Str)

  abstract

    -- Every Str morphism is an isomorphism.

    Str-homs-are-isos :
       {C D x y} (f :  (H {X = C} {Y = D} x y)) 
      Str.Is-isomorphism {X = C , x} {Y = D , y} f
    Str-homs-are-isos {C} {D} {x} {y} (C≅D , x≅y) =

      (D≅C ,
       (resp a (≅⇒≃ D C D≅C) y            ≡⟨ cong  eq  resp a eq y) $ Eq.lift-equality ext (refl _) 
        resp a (inverse $ ≅⇒≃ C D C≅D) y  ≡⟨ resp-preserves-inverses (El a) (resp a) (resp-id ass a) univ₁ ext (≅⇒≃ C D C≅D) _ _ x≅y ⟩∎
        x                                 )) ,

      S.lift-equality {X = D , y} {Y = D , y} (
        C≅D Fun.∙≅ D≅C   ≡⟨ _≃_.from (Fun.≡≃≡¹ {X = D} {Y = D}) (Fun._¹⁻¹ {X = C} {Y = D} C≅D) ⟩∎
        Fun.id≅ {X = D}  ) ,

      S.lift-equality {X = C , x} {Y = C , x} (
        D≅C Fun.∙≅ C≅D   ≡⟨ _≃_.from (Fun.≡≃≡¹ {X = C} {Y = C}) (Fun._⁻¹¹ {X = C} {Y = D} C≅D) ⟩∎
        Fun.id≅ {X = C}  )

      where

      D≅C : D Fun.≅ C
      D≅C = Fun._⁻¹≅ {X = C} {Y = D} C≅D

    -- The isomorphism that should be constructed.

    isomorphic : Isomorphic (a , P) (C , x , p) (D , y , q) 
                 ((C , x , p)  (D , y , q))
    isomorphic =
      Σ (C  D)  eq  Is-isomorphism a eq x y)     ↝⟨ (let ≃≃≅-CD = ≃≃≅-Set (# 1) ext (C , C-set) (D , D-set) in
                                                         Σ-cong ≃≃≅-CD  eq 
                                                           let eq′ = _≃_.from ≃≃≅-CD (_≃_.to ≃≃≅-CD eq) in
                                                           Is-isomorphism a eq  x y  ↝⟨ ≡⇒↝ _ $ cong  eq  Is-isomorphism a eq x y) $ sym $
                                                                                          _≃_.left-inverse-of ≃≃≅-CD eq 
                                                           Is-isomorphism a eq′ x y  )) 
       (H {X = C , C-set} {Y = D , D-set} x y)      ↝⟨ inverse ×-right-identity 
       (H {X = C , C-set} {Y = D , D-set} x y) ×   ↝⟨ ∃-cong  X≅Y  inverse $ _⇔_.to contractible⇔↔⊤ $
                                                                        propositional⇒inhabited⇒contractible
                                                                          (Str.Is-isomorphism-propositional X≅Y)
                                                                          (Str-homs-are-isos X≅Y)) 
      (((C , C-set) , x) Str.≅ ((D , D-set) , y))    ↔⟨ inverse  _ , structure-identity-principle ext Bij S
                                                                        {X = (C , C-set) , x} {Y = (D , D-set) , y}  
      (((C , C-set) , x)  ((D , D-set) , y))        ↔⟨ ≃-≡ $ ↔⇒≃ (Σ-assoc  ∃-cong  _  ×-comm)  inverse Σ-assoc) 
      (((C , x) , C-set)  ((D , y) , D-set))        ↝⟨ inverse $ ignore-propositional-component (H-level-propositional ext 2) 
      ((C , x)  (D , y))                            ↝⟨ ignore-propositional-component (proj₂ (P D y) ass) 
      (((C , x) , p)  ((D , y) , q))                ↔⟨ ≃-≡ $ ↔⇒≃ Σ-assoc ⟩□
      ((C , x , p)  (D , y , q))                    

    -- A simplification lemma.

    proj₁-from-isomorphic :
       X≡Y 
      proj₁ (_↔_.from isomorphic X≡Y) 
      elim  {X Y} _  proj₁ X  proj₁ Y)  _  Eq.id) X≡Y
    proj₁-from-isomorphic X≡Y = Eq.lift-equality ext (

      _≃_.to (proj₁ (_↔_.from isomorphic X≡Y))                         ≡⟨⟩

      cast C-set D-set X≡Y                                             ≡⟨ lemma ⟩∎

      _≃_.to (elim  {X Y} _  proj₁ X  proj₁ Y)  _  Eq.id) X≡Y)  )

      where

      cast :  {X Y} 
             Is-set (Carrier (a , P) X)  Is-set (Carrier (a , P) Y) 
             X  Y  Carrier (a , P) X  Carrier (a , P) Y
      cast {C , x , p} {D , y , q} C-set D-set X≡Y =
        proj₁ $ proj₁ $ proj₁ $
        Str.≡→≅ {X = (C , C-set) , x} {Y = (D , D-set) , y} $
        cong  { ((C , x) , C-set)  (C , C-set) , x }) $
        Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡
                   (cong  { (C , (x , p))  (C , x) , p }) X≡Y)))
                (proj₁ (H-level-propositional ext 2 _ _))

      lemma :
        cast C-set D-set X≡Y 
        _≃_.to (elim  {X Y} _  proj₁ X  proj₁ Y)  _  Eq.id) X≡Y)
      lemma = elim¹
         X≡Y   D-set  cast C-set D-set X≡Y 
                           _≃_.to (elim  {X Y} _  proj₁ X  proj₁ Y)
                                         _  Eq.id) X≡Y))
         C-set′ 

           cast C-set C-set′ (refl (C , x , p))                      ≡⟨ cong  eq 
                                                                                proj₁ $ proj₁ $ proj₁ $
                                                                                Str.≡→≅ {X = (C , C-set) , x} {Y = (C , C-set′) , x} $
                                                                                cong  { ((C , x) , C-set)  (C , C-set) , x }) $
                                                                                Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ {B = proj₁  uncurry P} eq))
                                                                                        (proj₁ (H-level-propositional ext 2 _ _)))
                                                                             (cong-refl  { (C , (x , p))  (C , x) , p })) 
           (proj₁ $ proj₁ $ proj₁ $
            Str.≡→≅ {X = (C , C-set) , x} {Y = (C , C-set′) , x} $
            cong  { ((C , x) , C-set)  (C , C-set) , x }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (H-level-propositional ext 2 _ _)))       ≡⟨ cong proj₁ (S.proj₁-≡→≅-¹ _) 

           (proj₁ $
            Fun.≡→≅ $
            cong proj₁ $
            cong  { ((C , x) , C-set)  (C , C-set) , x }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (H-level-propositional ext 2 _ _)))       ≡⟨ cong (proj₁  Fun.≡→≅) $
                                                                          cong-∘ proj₁  { ((C , x) , C-set)  (C , C-set) , x }) _ 
           (proj₁ $
            Fun.≡→≅ $
            cong  { ((C , _) , C-set)  C , C-set }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (H-level-propositional ext 2 _ _)))       ≡⟨ Fun.≡→≅-¹ _ 

           (elim  {X Y} _  Fun.Hom X Y)  _  P.id) $
            cong  { ((C , _) , C-set)  C , C-set }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (H-level-propositional ext 2 _ _)))       ≡⟨ elim¹  eq  elim  {X Y} _  Fun.Hom X Y)  _  P.id) eq 
                                                                                      ≡⇒↝ implication (cong proj₁ eq))
                        (elim  {X Y} _  Fun.Hom X Y)  _  P.id)
                              (refl (C , C-set))                          ≡⟨ elim-refl  {X Y} _  Fun.Hom X Y) _ 
                         P.id                                             ≡⟨ sym $ elim-refl  {A B} _  A  B) _ 
                         ≡⇒↝ implication (refl C)                         ≡⟨ cong (≡⇒↝ implication) (sym $ cong-refl proj₁) ⟩∎
                         ≡⇒↝ implication (cong proj₁ (refl (C , C-set)))  ) _ 

           (≡⇒↝ implication $
            cong proj₁ $
            cong  { ((C , _) , C-set)  C , C-set }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (H-level-propositional ext 2 _ _)))       ≡⟨ cong (≡⇒↝ implication)
                                                                             (cong-∘ proj₁  { ((C , _) , C-set)  C , C-set }) _) 
           (≡⇒↝ implication $
            cong  { ((C , _) , _)  C }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (H-level-propositional ext 2 _ _)))       ≡⟨ cong  eq 
                                                                                ≡⇒↝ implication $
                                                                                cong  { ((C , _) , _)  C }) $
                                                                                Σ-≡,≡→≡ (proj₁ {B = λ q  subst (proj₁  uncurry P) q p  p} eq)
                                                                                        (proj₁ (H-level-propositional ext 2 _ C-set′)))
                                                                             (Σ-≡,≡←≡-refl {B = λ { (C , x)  proj₁ (P C x)}}) 
           (≡⇒↝ implication $
            cong  { ((C , _) , _)  C }) $
            Σ-≡,≡→≡ (refl (C , x))
                    (proj₁ (H-level-propositional ext 2 _ _)))       ≡⟨ cong (≡⇒↝ implication  cong  { ((C , _) , _)  C }))
                                                                             (Σ-≡,≡→≡-reflˡ (proj₁ (H-level-propositional ext 2 _ _))) 
           (≡⇒↝ implication $
            cong  { ((C , _) , _)  C }) $
            cong (_,_ (C , x))
                 (trans (sym $ subst-refl (Is-set  proj₁) C-set)
                        (proj₁ (H-level-propositional ext 2 _ _))))  ≡⟨ cong (≡⇒↝ implication)
                                                                             (cong-∘  { ((C , _) , _)  C }) (_,_ (C , x)) _) 
           (≡⇒↝ implication $
            cong (const C)
                 (trans (sym $ subst-refl (Is-set  proj₁) C-set)
                        (proj₁ (H-level-propositional ext 2 _ _))))  ≡⟨ cong (≡⇒↝ implication) (cong-const _) 

           ≡⇒↝ implication (refl C)                                  ≡⟨ ≡⇒↝-refl 

           P.id                                                      ≡⟨ sym $ cong _≃_.to $ elim-refl  {X Y} _  proj₁ X  proj₁ Y) _ ⟩∎

           _≃_.to (elim  {X Y} _  proj₁ X  proj₁ Y)
                         _  Eq.id)
                        (refl (C , x , p)))                          )

        X≡Y D-set

abstract

  -- The from component of isomorphism-is-equality′ is equal
  -- to a simple function.

  from-isomorphism-is-equality′ :
     Univ ass c X Y  let open Universe Univ; open Class Univ in
    (El-set :  {B}  Is-set B  Is-set (El (proj₁ c) B)) 
     I-set J-set 
    _↔_.from (isomorphism-is-equality′
                Univ ass c X Y El-set I-set J-set) 
    elim  {X Y} _  Isomorphic c X Y)
          { (_ , x , _)  Eq.id , resp-id ass (proj₁ c) x })
  from-isomorphism-is-equality′ Univ ass c X Y El-set I-set J-set =
    apply-ext ext λ eq 
      Σ-≡,≡→≡ (lemma eq) (_⇔_.to set⇔UIP (El-set J-set) _ _)
    where
    open Assumptions ass
    open Universe Univ
    open Class Univ

    lemma :
       eq 
      proj₁ (_↔_.from (isomorphism-is-equality′
                         Univ ass c X Y El-set I-set J-set) eq) 
      proj₁ (elim  {X Y} _  Isomorphic c X Y)
                   { (_ , x , _)  Eq.id , resp-id ass (proj₁ c) x })
                  eq)
    lemma eq =
      proj₁ (_↔_.from (isomorphism-is-equality′
                         Univ ass c X Y El-set I-set J-set) eq)          ≡⟨ Isomorphism-is-equality′.proj₁-from-isomorphic
                                                                              Univ ass _ _ _ _ _ _ _ _ El-set I-set J-set eq 
      elim  {X Y} _  proj₁ X  proj₁ Y)  _  Eq.id) eq              ≡⟨ sym $ elim-∘  {X Y} _  Isomorphic c X Y) _ proj₁ _ ⟩∎
      proj₁ (elim  {X Y} _  Isomorphic c X Y)
                   { (_ , x , _)  Eq.id , resp-id ass (proj₁ c) x })
                  eq)