------------------------------------------------------------------------
-- A large(r) class of algebraic structures satisfies the property
-- that isomorphic instances of a structure are equal (assuming
-- univalence)
------------------------------------------------------------------------

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

-- Note that this module uses ordinary propositional equality, with a
-- computing J rule.

-- This module has been developed in collaboration with Thierry
-- Coquand.

module Univalence-axiom.Isomorphism-is-equality.More where

open import Equality.Propositional
  hiding (refl) renaming (equality-with-J to eq)
open import Equality
open Derived-definitions-and-properties eq using (refl)

open import Bijection eq hiding (id; _∘_; inverse; _↔⟨_⟩_; finally-↔)
open import Equivalence eq as Eq hiding (id; _∘_; inverse)
open import Function-universe eq hiding (id; _∘_)
open import H-level eq as H-level hiding (Proposition; Type)
open import H-level.Closure eq
open import Preimage eq
open import Prelude
open import Univalence-axiom eq

------------------------------------------------------------------------
-- A record packing up certain assumptions

-- Use of these or similar assumptions is usually not documented in
-- comments below (with remarks like "assuming univalence").

record Assumptions : Set₂ where
  field
    ext₁  : Extensionality (# ) (# )
    univ  : Univalence (# )
    univ₁ : Univalence (# )

  abstract

    ext : Extensionality (# ) (# )
    ext = lower-extensionality (# ) (# ) ext₁

------------------------------------------------------------------------
-- A class of algebraic structures

-- An algebraic structure universe.

mutual

  -- Codes for structures.

  infixl  _▻_

  data Code : Set₂ where
    ε   : Code
    _▻_ : (c : Code) → Extension c → Code

  -- Structures can contain arbitrary "extensions".

  record Extension (c : Code) : Set₂ where
    field

      -- An instance-indexed type.

      Ext : ⟦ c ⟧ → Set₁

      -- A predicate specifying when two elements are isomorphic with
      -- respect to an isomorphism.

      Iso : (ass : Assumptions) →
            {I J : ⟦ c ⟧} → Isomorphic ass c I J →
            Ext I → Ext J → Set₁

    -- An alternative definition of Iso.

    Iso′ : (ass : Assumptions) →
           ∀ {I J} → Isomorphic ass c I J →
           Ext I → Ext J → Set₁
    Iso′ ass I≅J x y =
      subst Ext (_≃_.to (isomorphism≃equality ass c) I≅J) x ≡ y

    field

      -- Iso and Iso′ are equivalent.

      Iso≃Iso′ :
        (ass : Assumptions) →
        ∀ {I J} (I≅J : Isomorphic ass c I J) {x y} →
        Iso ass I≅J x y ≃ Iso′ ass I≅J x y

  -- Interpretation of the codes. The elements of ⟦ c ⟧ are instances
  -- of the structure encoded by c.

  ⟦_⟧ : Code → Set₁
  ⟦ ε     ⟧ = ↑ _ ⊤
  ⟦ c ▻ e ⟧ = Σ ⟦ c ⟧ (Extension.Ext e)

  -- Isomorphisms.

  Isomorphic : Assumptions → (c : Code) → ⟦ c ⟧ → ⟦ c ⟧ → Set₁
  Isomorphic _   ε       _       _       = ↑ _ ⊤
  Isomorphic ass (c ▻ e) (I , x) (J , y) =
    Σ (Isomorphic ass c I J) λ I≅J → Extension.Iso e ass I≅J x y

  -- Isomorphism is equivalent to equality.

  isomorphism≃equality : (ass : Assumptions) →
                         (c : Code) {I J : ⟦ c ⟧} →
                         Isomorphic ass c I J ≃ (I ≡ J)

  isomorphism≃equality _ ε =

      ↑ _ ⊤              ↔⟨ contractible-isomorphic (↑-closure  ⊤-contractible)
                                                    (↑-closure  (mono₁  ⊤-contractible) _ _) ⟩□
      lift tt ≡ lift tt  □

  isomorphism≃equality ass (c ▻ e) {I , x} {J , y} =

    (Σ (Isomorphic ass c I J) λ I≅J → Iso e ass I≅J x y)  ↝⟨ Σ-cong (isomorphism≃equality ass c)
                                                                    (λ I≅J → Iso≃Iso′ e ass I≅J) ⟩
    (Σ (I ≡ J) λ I≡J → subst (Ext e) I≡J x ≡ y)           ↔⟨ Σ-≡,≡↔≡ ⟩□

    ((I , x) ≡ (J , y))                                   □

    where open Extension

-- Isomorphism is equal to equality (assuming /only/ univalence).

isomorphism≡equality :
  (univ  : Univalence (# ))
  (univ₁ : Univalence (# ))
  (univ₂ : Univalence (# )) →

  let ass = record
        { ext₁  = dependent-extensionality univ₂ (λ _ → univ₁)
        ; univ  = univ
        ; univ₁ = univ₁
        } in

  (c : Code) {I J : ⟦ c ⟧} →
  Isomorphic ass c I J ≡ (I ≡ J)
isomorphism≡equality univ univ₁ univ₂ c =
  ≃⇒≡ univ₁ $ isomorphism≃equality _ c

------------------------------------------------------------------------
-- Reflexivity

-- The isomorphism relation is reflexive.

reflexivity : (ass : Assumptions) → ∀ c I → Isomorphic ass c I I
reflexivity ass c I =
  _≃_.from (isomorphism≃equality ass c) (refl I)

-- Reflexivity relates an element to itself.

reflexivityE :
  (ass : Assumptions) →
  ∀ c e I x →
  Extension.Iso e ass (reflexivity ass c I) x x
reflexivityE ass c e I x =
  _≃_.from (Iso≃Iso′ ass (reflexivity ass c I)) (
    subst Ext (to (from (refl I))) x  ≡⟨ subst (λ eq → subst Ext eq x ≡ x)
                                               (sym $ right-inverse-of (refl I))
                                               (refl x) ⟩∎
    x                                 ∎)
  where
  open Extension e
  open _≃_ (isomorphism≃equality ass c)

-- Unfolding lemma (definitional) for reflexivity.

reflexivity-▻ :
  ∀ {ass c e I x} →
  reflexivity ass (c ▻ e) (I , x) ≡
  (reflexivity ass c I , reflexivityE ass c e I x)
reflexivity-▻ = refl _

------------------------------------------------------------------------
-- Recipe for defining extensions

-- Another kind of extension.

record Extension-with-resp (c : Code) : Set₂ where
  field

    -- An instance-indexed type.

    Ext : ⟦ c ⟧ → Set₁

    -- A predicate specifying when two elements are isomorphic with
    -- respect to an isomorphism.

    Iso : (ass : Assumptions) →
          {I J : ⟦ c ⟧} → Isomorphic ass c I J →
          Ext I → Ext J → Set₁

    -- Ext, seen as a predicate, respects isomorphisms.

    resp : (ass : Assumptions) →
           ∀ {I J} → Isomorphic ass c I J →
           Ext I → Ext J

    -- The resp function respects reflexivity.

    resp-refl : (ass : Assumptions) →
                ∀ {I} (x : Ext I) →
                resp ass (reflexivity ass c I) x ≡ x

  -- An alternative definition of Iso.

  Iso″ : (ass : Assumptions) →
         {I J : ⟦ c ⟧} → Isomorphic ass c I J →
         Ext I → Ext J → Set₁
  Iso″ ass I≅J x y = resp ass I≅J x ≡ y

  field

    -- Iso and Iso″ are equivalent.

    Iso≃Iso″ :
      (ass : Assumptions) →
      ∀ {I J} (I≅J : Isomorphic ass c I J) {x y} →
      Iso ass I≅J x y ≃ Iso″ ass I≅J x y

  -- Another alternative definition of Iso.

  Iso′ : (ass : Assumptions) →
         ∀ {I J} → Isomorphic ass c I J →
         Ext I → Ext J → Set₁
  Iso′ ass I≅J x y =
    subst Ext (_≃_.to (isomorphism≃equality ass c) I≅J) x ≡ y

  abstract

    -- Every element is isomorphic to itself, transported along the
    -- "outer" isomorphism.

    isomorphic-to-itself″ :
      (ass : Assumptions) →
      ∀ {I J} (I≅J : Isomorphic ass c I J) {x} →
      Iso″ ass I≅J x
           (subst Ext (_≃_.to (isomorphism≃equality ass c) I≅J) x)
    isomorphic-to-itself″ ass I≅J {x} = transport-theorem′
      Ext
      (Isomorphic ass c)
      (_≃_.surjection $ inverse $ isomorphism≃equality ass c)
      (resp ass)
      (λ _ → resp-refl ass)
      I≅J
      x

  -- Iso and Iso′ are equivalent.

  Iso≃Iso′ :
    (ass : Assumptions) →
    ∀ {I J} (I≅J : Isomorphic ass c I J) {x y} →
    Iso ass I≅J x y ≃ Iso′ ass I≅J x y
  Iso≃Iso′ ass I≅J {x} {y} = record
    { to             = to
    ; is-equivalence = λ y →
        (from y , right-inverse-of y) , irrelevance y
    }
    where
    -- This is the core of the definition. I could have defined
    -- Iso≃Iso′ ... = I≃I′. The rest is only included in order to
    -- control how much Agda unfolds the code.
    I≃I′ =
      Iso  ass I≅J x y  ↝⟨ Iso≃Iso″ ass I≅J ⟩
      Iso″ ass I≅J x y  ↝⟨ ≡⇒≃ $ cong (λ z → z ≡ y) $ isomorphic-to-itself″ ass I≅J ⟩□
      Iso′ ass I≅J x y  □

    to   = _≃_.to   I≃I′
    from = _≃_.from I≃I′

    abstract
      right-inverse-of : ∀ x → to (from x) ≡ x
      right-inverse-of = _≃_.right-inverse-of I≃I′

      irrelevance : ∀ y (p : to ⁻¹ y) → (from y , right-inverse-of y) ≡ p
      irrelevance = _≃_.irrelevance I≃I′

  -- An extension constructed from the fields above.

  extension : Extension c
  extension = record { Ext = Ext; Iso = Iso; Iso≃Iso′ = Iso≃Iso′ }

  -- Every element is isomorphic to itself, transported (in another
  -- way) along the "outer" isomorphism.

  isomorphic-to-itself :
    (ass : Assumptions) →
    ∀ {I J} (I≅J : Isomorphic ass c I J) x →
    Iso ass I≅J x (resp ass I≅J x)
  isomorphic-to-itself ass I≅J x =
    _≃_.from (Iso≃Iso″ ass I≅J) (refl (resp ass I≅J x))

  abstract

    -- Simplification lemmas.

    resp-refl-lemma :
      (ass : Assumptions) →
      ∀ I x →
      resp-refl ass x ≡
      _≃_.from (≡⇒≃ $ cong (λ z → z ≡ x) $
                      isomorphic-to-itself″ ass (reflexivity ass c I))
               (subst (λ eq → subst Ext eq x ≡ x)
                      (sym $ _≃_.right-inverse-of
                               (isomorphism≃equality ass c)
                               (refl I))
                      (refl x))
    resp-refl-lemma ass I x =
      let rfl    = reflexivity ass c I
          iso≃eq = λ {I J} → isomorphism≃equality ass c {I = I} {J = J}
          rio    = right-inverse-of iso≃eq (refl I)
          lio    = left-inverse-of (inverse iso≃eq) (refl I)
          sx≡x   = subst (λ eq → subst Ext eq x ≡ x) (sym rio) (refl x)

          sx≡x-lemma =
            cong (λ eq → subst Ext eq x) rio                      ≡⟨ sym $ trans-reflʳ _ ⟩

            trans (cong (λ eq → subst Ext eq x) rio)
                  (refl x)                                        ≡⟨ sym $ subst-trans (cong (λ eq → subst Ext eq x) rio) ⟩

            subst (λ z → z ≡ x)
                  (sym $ cong (λ eq → subst Ext eq x) rio)
                  (refl x)                                        ≡⟨ cong (λ eq → subst (λ z → z ≡ x) eq (refl x)) $ sym $
                                                                          cong-sym (λ eq → subst Ext eq x) rio ⟩
            subst (λ z → z ≡ x)
                  (cong (λ eq → subst Ext eq x) $ sym rio)
                  (refl x)                                        ≡⟨ sym $ subst-∘ (λ z → z ≡ x) (λ eq → subst Ext eq x) (sym rio) ⟩∎

            subst (λ eq → subst Ext eq x ≡ x) (sym rio) (refl x)  ∎

          lemma₁ =
            trans (sym lio) rio  ≡⟨ cong (λ eq → trans (sym eq) rio) $ left-inverse-of∘inverse iso≃eq ⟩

            trans (sym rio) rio  ≡⟨ trans-symˡ rio ⟩∎

            refl (refl I)        ∎

          lemma₂ =
            elim-refl (λ {I J} _ → Ext I → Ext J) (λ _ e → e)  ≡⟨⟩

            cong (subst Ext) (refl (refl I))                   ≡⟨ cong (cong (subst Ext)) $ sym lemma₁ ⟩∎

            cong (subst Ext) (trans (sym lio) rio)             ∎

          lemma₃ =
            cong (λ r → r x)
                 (elim-refl (λ {I J} _ → Ext I → Ext J) (λ _ e → e))   ≡⟨ cong (cong (λ r → r x)) lemma₂ ⟩

            cong (λ r → r x) (cong (subst Ext) (trans (sym lio) rio))  ≡⟨ cong-∘ (λ r → r x) (subst Ext) (trans (sym lio) rio) ⟩

            cong (λ eq → subst Ext eq x) (trans (sym lio) rio)         ≡⟨ cong-trans (λ eq → subst Ext eq x) (sym lio) rio ⟩

            trans (cong (λ eq → subst Ext eq x) (sym lio))
                  (cong (λ eq → subst Ext eq x) rio)                   ≡⟨ cong (λ eq → trans eq (cong (λ eq → subst Ext eq x) rio)) $
                                                                               cong-sym (λ eq → subst Ext eq x) lio ⟩∎
            trans (sym (cong (λ eq → subst Ext eq x) lio))
                  (cong (λ eq → subst Ext eq x) rio)                   ∎
      in

      resp-refl ass x                                                  ≡⟨ sym $ trans-reflʳ _ ⟩

      trans (resp-refl ass x) (refl x)                                 ≡⟨ cong (trans (resp-refl ass x)) $ trans-symˡ (subst-refl Ext x) ⟩

      trans (resp-refl ass x)
            (trans (sym $ subst-refl Ext x) (subst-refl Ext x))        ≡⟨ sym $ trans-assoc _ (sym $ subst-refl Ext x) (subst-refl Ext x) ⟩

      trans (trans (resp-refl ass x) (sym $ subst-refl Ext x))
            (subst-refl Ext x)                                         ≡⟨ cong (trans (trans (resp-refl ass x) (sym $ subst-refl Ext x)))
                                                                               lemma₃ ⟩
      trans (trans (resp-refl ass x) (sym $ subst-refl Ext x))
            (trans (sym (cong (λ eq → subst Ext eq x) lio))
                   (cong (λ eq → subst Ext eq x) rio))                 ≡⟨ sym $ trans-assoc _ _ (cong (λ eq → subst Ext eq x) rio) ⟩

      trans (trans (trans (resp-refl ass x) (sym $ subst-refl Ext x))
                   (sym (cong (λ eq → subst Ext eq x) lio)))
            (cong (λ eq → subst Ext eq x) rio)                         ≡⟨ cong₂ trans
                                                                            (sym $ transport-theorem′-refl Ext (Isomorphic ass c) (inverse iso≃eq)
                                                                                                           (resp ass) (λ _ → resp-refl ass) x)
                                                                            sx≡x-lemma ⟩
      trans (isomorphic-to-itself″ ass rfl) sx≡x                       ≡⟨ sym $ subst-trans (isomorphic-to-itself″ ass rfl) ⟩

      subst (λ z → z ≡ x) (sym $ isomorphic-to-itself″ ass rfl) sx≡x   ≡⟨ subst-in-terms-of-inverse∘≡⇒↝ equivalence
                                                                            (isomorphic-to-itself″ ass rfl) (λ z → z ≡ x) _ ⟩∎
      from (≡⇒≃ $ cong (λ z → z ≡ x) $ isomorphic-to-itself″ ass rfl)
           sx≡x                                                        ∎

      where open _≃_

    isomorphic-to-itself-reflexivity :
      (ass : Assumptions) →
      ∀ I x →
      isomorphic-to-itself ass (reflexivity ass c I) x ≡
      subst (Iso ass (reflexivity ass c I) x)
            (sym $ resp-refl ass x)
            (reflexivityE ass c extension I x)
    isomorphic-to-itself-reflexivity ass I x =
      let rfl = reflexivity ass c I
          r-r = resp-refl ass x in

      from (Iso≃Iso″ ass rfl) (refl (resp ass rfl x))                  ≡⟨ elim¹ (λ {y} resp-x≡y → from (Iso≃Iso″ ass rfl) (refl (resp ass rfl x)) ≡
                                                                                                  subst (Iso ass rfl x) (sym resp-x≡y)
                                                                                                        (from (Iso≃Iso″ ass rfl) resp-x≡y))
                                                                                (refl _) r-r ⟩
      subst (Iso ass rfl x) (sym r-r) (from (Iso≃Iso″ ass rfl) r-r)    ≡⟨ cong (subst (Iso ass rfl x) (sym r-r) ∘ from (Iso≃Iso″ ass rfl))
                                                                               (resp-refl-lemma ass I x) ⟩∎
      subst (Iso ass rfl x) (sym r-r)
        (from (Iso≃Iso″ ass rfl)
           (from
              (≡⇒≃ $ cong (λ z → z ≡ x)
                          (isomorphic-to-itself″ ass rfl))
              (subst (λ eq → subst Ext eq x ≡ x)
                 (sym $ right-inverse-of (isomorphism≃equality ass c)
                                         (refl I)) (refl x))))         ∎

      where open _≃_

------------------------------------------------------------------------
-- Type extractors

record Extractor (c : Code) : Set₂ where
  field

    -- Extracts a type from an instance.

    Type : ⟦ c ⟧ → Set₁

    -- Extracts an equivalence relating types extracted from
    -- isomorphic instances.
    --
    -- Perhaps one could have a variant of Type-cong that is not based
    -- on any "Assumptions", and produces logical equivalences (_⇔_)
    -- instead of equivalences (_≃_). Then one could (hopefully)
    -- define isomorphism without using any assumptions.

    Type-cong : (ass : Assumptions) →
                ∀ {I J} → Isomorphic ass c I J → Type I ≃ Type J

    -- Reflexivity is mapped to the identity equivalence.

    Type-cong-reflexivity :
      (ass : Assumptions) →
      ∀ I → Type-cong ass (reflexivity ass c I) ≡ Eq.id

-- Constant type extractor.

[_] : ∀ {c} → Set₁ → Extractor c
[_] {c} A = record
  { Type                  = λ _ → A
  ; Type-cong             = λ _ _ → Eq.id
  ; Type-cong-reflexivity = λ _ _ → refl _
  }

-- Successor type extractor.

infix  1+_

1+_ : ∀ {c e} → Extractor c → Extractor (c ▻ e)
1+_ {c} {e} extractor = record
  { Type                  = Type ∘ proj₁
  ; Type-cong             = λ ass → Type-cong ass ∘ proj₁
  ; Type-cong-reflexivity = λ { ass (I , x) →
      Type-cong ass (reflexivity ass c I)  ≡⟨ Type-cong-reflexivity ass I ⟩∎
      Eq.id                                ∎ }
  }
  where
  open Extractor extractor

------------------------------------------------------------------------
-- An extension: types

-- Extends a structure with a type.

A-type : ∀ {c} → Extension c
A-type {c} = record
  { Ext      = λ _ → Set
  ; Iso      = λ _ _ A B → ↑ _ (A ≃ B)
  ; Iso≃Iso′ = λ ass I≅J {A B} →
                 let I≡J = _≃_.to (isomorphism≃equality ass c) I≅J in

                 ↑ _ (A ≃ B)                    ↔⟨ ↑↔ ⟩
                 (A ≃ B)                        ↝⟨ inverse $ ≡≃≃ (Assumptions.univ ass) ⟩
                 (A ≡ B)                        ↝⟨ ≡⇒≃ $ cong (λ C → C ≡ B) $ sym (subst-const I≡J) ⟩
                 (subst (λ _ → Set) I≡J A ≡ B)  □
  }

-- A corresponding type extractor.

[0] : ∀ {c} → Extractor (c ▻ A-type)
[0] {c} = record
  { Type                  = λ { (_ , A) → ↑ _ A }
  ; Type-cong             = λ { _ (_ , lift A≃B) → ↑-cong A≃B }
  ; Type-cong-reflexivity = λ { ass (I , A) → elim₁
      (λ {p} q →
         ↑-cong (≡⇒≃
           (from (≡⇒≃ (cong (λ C → C ≡ A) (sym (subst-const p))))
                 (subst (λ eq → subst Ext eq A ≡ A)
                        (sym q) (refl A)))) ≡
         Eq.id)
      (lift-equality (Assumptions.ext₁ ass) (refl _))
      (right-inverse-of (isomorphism≃equality ass c) (refl I)) }
  }
  where
  open Extension A-type
  open _≃_

------------------------------------------------------------------------
-- An extension: propositions

-- Extends a structure with a proposition.

Proposition : ∀ {c} →

              -- The proposition.
              (P : ⟦ c ⟧ → Set₁) →

              -- The proposition must be propositional (given some
              -- assumptions).
              (Assumptions → ∀ I → Is-proposition (P I)) →

              Extension c
Proposition {c} P prop = record
  { Ext      = P
  ; Iso      = λ _ _ _ _ → ↑ _ ⊤
  ; Iso≃Iso′ = λ ass I≅J {_ p} →
                 ↑ _ ⊤    ↔⟨ contractible-isomorphic
                               (↑-closure  ⊤-contractible)
                               (mono₁  (propositional⇒inhabited⇒contractible (prop ass _) p) _ _) ⟩□
                 (_ ≡ _)  □
  }

-- The proposition stating that a given type is a set.

Is-a-set : ∀ {c} → Extractor c → Extension c
Is-a-set extractor =
  Proposition (Is-set ∘ Type)
              (λ ass _ → H-level-propositional (Assumptions.ext₁ ass) )
  where open Extractor extractor

------------------------------------------------------------------------
-- An extension: n-ary functions

-- N-ary functions.

_^_⟶_ : Set₁ → ℕ → Set₁ → Set₁
A ^ zero  ⟶ B = B
A ^ suc n ⟶ B = A → A ^ n ⟶ B

-- N-ary function morphisms.

Is-_-ary-morphism :
  ∀ (n : ℕ) {A B} → (A ^ n ⟶ A) → (B ^ n ⟶ B) → (A → B) → Set₁
Is- zero  -ary-morphism x y m = m x ≡ y
Is- suc n -ary-morphism f g m =
  ∀ x → Is- n -ary-morphism (f x) (g (m x)) m

-- An n-ary function extension.

N-ary : ∀ {c} →

        -- Extracts the underlying type.
        Extractor c →

        -- The function's arity.
        ℕ →

        Extension c
N-ary {c} extractor n = Extension-with-resp.extension record
  { Ext       = λ I → Type I ^ n ⟶ Type I
  ; Iso       = λ ass I≅J f g →
                    Is- n -ary-morphism f g (_≃_.to (Type-cong ass I≅J))
  ; resp      = λ ass I≅J → cast n (Type-cong ass I≅J)
  ; resp-refl = λ ass f →
                    cast n (Type-cong ass (reflexivity ass c _)) f  ≡⟨ cong (λ eq → cast n eq f) $ Type-cong-reflexivity ass _ ⟩
                    cast n Eq.id f                                  ≡⟨ cast-id (Assumptions.ext₁ ass) n f ⟩∎
                    f                                               ∎
  ; Iso≃Iso″  = λ ass I≅J {f g} →
      Iso≃Iso″ (Assumptions.ext₁ ass) (Type-cong ass I≅J) n f g
  }
  where
  open Extractor extractor

  -- Changes the type of an n-ary function.

  cast : ∀ n {A B} → A ≃ B → A ^ n ⟶ A → B ^ n ⟶ B
  cast zero    A≃B = _≃_.to A≃B
  cast (suc n) A≃B = λ f x → cast n A≃B (f (_≃_.from A≃B x))

  -- Cast simplification lemma.

  cast-id : Extensionality (# ) (# ) →
            ∀ {A} n (f : A ^ n ⟶ A) → cast n Eq.id f ≡ f
  cast-id ext zero    x = refl x
  cast-id ext (suc n) f = ext λ x → cast-id ext n (f x)

  -- Two definitions of isomorphism are equivalent.

  Iso≃Iso″ :
    Extensionality (# ) (# ) →
    ∀ {A B} (A≃B : A ≃ B)
    (n : ℕ) (f : A ^ n ⟶ A) (g : B ^ n ⟶ B) →
    Is- n -ary-morphism f g (_≃_.to A≃B) ≃ (cast n A≃B f ≡ g)

  Iso≃Iso″ ext A≃B zero x y =

    (_≃_.to A≃B x ≡ y)  □

  Iso≃Iso″ ext A≃B (suc n) f g =

    (∀ x → Is- n -ary-morphism (f x) (g (_≃_.to A≃B x)) (_≃_.to A≃B))  ↝⟨ Eq.∀-preserves ext (λ x →
                                                                            Iso≃Iso″ ext A≃B n (f x) (g (_≃_.to A≃B x))) ⟩
    (∀ x → cast n A≃B (f x) ≡ g (_≃_.to A≃B x))                        ↝⟨ Eq.extensionality-isomorphism ext ⟩

    (cast n A≃B ∘ f ≡ g ∘ _≃_.to A≃B)                                  ↝⟨ inverse $ ∘from≡↔≡∘to ext A≃B ⟩□

    (cast n A≃B ∘ f ∘ _≃_.from A≃B ≡ g)                                □

------------------------------------------------------------------------
-- An extension: simply typed functions

-- This section contains a generalisation of the development for n-ary
-- functions above.

-- Simple types.

data Simple-type (c : Code) : Set₂ where
  base : Extractor c → Simple-type c
  _⟶_  : Simple-type c → Simple-type c → Simple-type c

-- Interpretation of a simple type.

⟦_⟧⟶ : ∀ {c} → Simple-type c → ⟦ c ⟧ → Set₁
⟦ base A ⟧⟶ I = Extractor.Type A I
⟦ σ ⟶ τ  ⟧⟶ I = ⟦ σ ⟧⟶ I → ⟦ τ ⟧⟶ I

-- A simply typed function extension.

Simple : ∀ {c} → Simple-type c → Extension c
Simple {c} σ = Extension-with-resp.extension record
  { Ext       = ⟦ σ ⟧⟶
  ; Iso       = λ ass → Iso ass σ
  ; resp      = λ ass I≅J → _≃_.to (cast ass σ I≅J)
  ; resp-refl = λ ass f → cong (λ eq → _≃_.to eq f) $ cast-refl ass σ
  ; Iso≃Iso″  = λ ass → Iso≃Iso″ ass σ
  }
  where
  open Extractor

  -- Isomorphisms between simply typed values.

  Iso : (ass : Assumptions) →
        (σ : Simple-type c) →
        ∀ {I J} → Isomorphic ass c I J → ⟦ σ ⟧⟶ I → ⟦ σ ⟧⟶ J → Set₁
  Iso ass (base A) I≅J x y = _≃_.to (Type-cong A ass I≅J) x ≡ y
  Iso ass (σ ⟶ τ)  I≅J f g =
    ∀ x y → Iso ass σ I≅J x y → Iso ass τ I≅J (f x) (g y)

  -- Cast.

  cast : (ass : Assumptions) →
         (σ : Simple-type c) →
         ∀ {I J} → Isomorphic ass c I J → ⟦ σ ⟧⟶ I ≃ ⟦ σ ⟧⟶ J
  cast ass (base A) I≅J = Type-cong A ass I≅J
  cast ass (σ ⟶ τ)  I≅J = →-cong ext₁ (cast ass σ I≅J) (cast ass τ I≅J)
    where open Assumptions ass

  -- Cast simplification lemma.

  cast-refl : (ass : Assumptions) →
              ∀ σ {I} → cast ass σ (reflexivity ass c I) ≡ Eq.id
  cast-refl ass (base A) {I} =
    Type-cong A ass (reflexivity ass c I)  ≡⟨ Type-cong-reflexivity A ass I ⟩∎
    Eq.id                                  ∎

  cast-refl ass (σ ⟶ τ) {I} =
    cast ass (σ ⟶ τ) (reflexivity ass c I)  ≡⟨ lift-equality ext₁ $ cong _≃_.to $
                                                 cong₂ (→-cong ext₁) (cast-refl ass σ) (cast-refl ass τ) ⟩∎
    Eq.id                                   ∎
    where open Assumptions ass

  -- Two definitions of isomorphism are equivalent.

  Iso≃Iso″ :
    (ass : Assumptions) →
    (σ : Simple-type c) →
    ∀ {I J} (I≅J : Isomorphic ass c I J) {f g} →
    Iso ass σ I≅J f g ≃ (_≃_.to (cast ass σ I≅J) f ≡ g)
  Iso≃Iso″ ass (base A) I≅J {x} {y} =

    (_≃_.to (Type-cong A ass I≅J) x ≡ y)  □

  Iso≃Iso″ ass (σ ⟶ τ) I≅J {f} {g} =

    (∀ x y → Iso ass σ I≅J x y → Iso ass τ I≅J (f x) (g y))        ↝⟨ ∀-preserves ext₁ (λ _ → ∀-preserves ext₁ λ _ →
                                                                        →-cong ext₁ (Iso≃Iso″ ass σ I≅J) (Iso≃Iso″ ass τ I≅J)) ⟩
    (∀ x y → to (cast ass σ I≅J) x ≡ y →
             to (cast ass τ I≅J) (f x) ≡ g y)                      ↝⟨ inverse $ ∀-preserves ext₁ (λ x → ↔⇒≃ $
                                                                        ∀-intro ext₁ (λ y _ → to (cast ass τ I≅J) (f x) ≡ g y)) ⟩
    (∀ x → to (cast ass τ I≅J) (f x) ≡ g (to (cast ass σ I≅J) x))  ↝⟨ extensionality-isomorphism ext₁ ⟩

    (to (cast ass τ I≅J) ∘ f ≡ g ∘ to (cast ass σ I≅J))            ↝⟨ inverse $ ∘from≡↔≡∘to ext₁ (cast ass σ I≅J) ⟩□

    (to (cast ass τ I≅J) ∘ f ∘ from (cast ass σ I≅J) ≡ g)          □

    where
    open _≃_
    open Assumptions ass

------------------------------------------------------------------------
-- An unfinished extension: dependent types

-- The extension currently supports polymorphic types.

module Dependent where

  open Extractor

  ----------------------------------------------------------------------
  -- The extension

  -- Dependent types.

  data Ty (c : Code) : Set₂

  -- Extension: Dependently-typed functions.

  ext-with-resp : ∀ {c} → Ty c → Extension-with-resp c

  private
    open module E {c} (σ : Ty c) =
      Extension-with-resp (ext-with-resp σ)
      hiding (Iso; Iso≃Iso″; extension)
    open E public using () renaming (extension to Dep)

  data Ty c where
    set  : Ty c
    base : Extractor c → Ty c
    Π    : (σ : Ty c) → Ty (c ▻ Dep σ) → Ty c

  -- Interpretation of a dependent type.

  ⟦_⟧Π : ∀ {c} → Ty c → ⟦ c ⟧ → Set₁

  -- Isomorphisms between dependently typed functions.

  Iso :
    (ass : Assumptions) →
    ∀ {c} (σ : Ty c) →
    ∀ {I J} → Isomorphic ass c I J → ⟦ σ ⟧Π I → ⟦ σ ⟧Π J → Set₁

  -- A cast function.

  cast : (ass : Assumptions) →
         ∀ {c} (σ : Ty c) {I J} →
         Isomorphic ass c I J → ⟦ σ ⟧Π I ≃ ⟦ σ ⟧Π J

  -- Reflexivity is mapped to identity.

  cast-refl : (ass : Assumptions) →
              ∀ {c} (σ : Ty c) {I} →
              cast ass σ (reflexivity ass c I) ≡ Eq.id

  -- Two definitions of isomorphism are equivalent.

  Iso≃Iso″ : (ass : Assumptions) →
             ∀ {c} (σ : Ty c) {I J} (I≅J : Isomorphic ass c I J) {f g} →
             Iso ass σ I≅J f g ≃ (_≃_.to (cast ass σ I≅J) f ≡ g)

  -- Extension: Dependently-typed functions.

  ext-with-resp {c} σ = record
    { Ext       = ⟦ σ ⟧Π
    ; Iso       = λ ass → Iso ass σ
    ; resp      = λ ass I≅J → _≃_.to (cast ass σ I≅J)
    ; resp-refl = λ ass f → cong (λ eq → _≃_.to eq f) $ cast-refl ass σ
    ; Iso≃Iso″  = λ ass → Iso≃Iso″ ass σ
    }

  -- Interpretation of a dependent type.

  ⟦ set    ⟧Π _ = Set
  ⟦ base A ⟧Π I = Type A I
  ⟦ Π σ τ  ⟧Π I = (x : ⟦ σ ⟧Π I) → ⟦ τ ⟧Π (I , x)

  -- Isomorphisms between dependently typed functions.

  Iso _   set      _   A B = ↑ _ (A ≃ B)
  Iso ass (base A) I≅J x y = x ≡ _≃_.from (Type-cong A ass I≅J) y
  Iso ass (Π σ τ)  I≅J f g = ∀ x y →
    (x≅y : Iso ass σ I≅J x y) → Iso ass τ (I≅J , x≅y) (f x) (g y)

  -- A cast function.

  cast ass set      I≅J = Eq.id
  cast ass (base A) I≅J = Type-cong A ass I≅J
  cast ass (Π σ τ)  I≅J = Π-preserves ext₁
    (cast ass σ I≅J)
    (λ x → cast ass τ (I≅J , isomorphic-to-itself σ ass I≅J x))
    where open Assumptions ass

  abstract

    -- Reflexivity is mapped to identity.

    cast-refl ass     set          = refl Eq.id
    cast-refl ass {c} (base A) {I} =

      Type-cong A ass (reflexivity ass c I)  ≡⟨ Type-cong-reflexivity A ass I ⟩∎

      Eq.id                                  ∎

    cast-refl ass {c} (Π σ τ) {I} =
      let rfl   = reflexivity ass c I
          rflE  = reflexivityE ass c (Dep σ) I in

      lift-equality-inverse ext₁ $ ext₁ λ f → ext₁ λ x →

        from (cast ass τ (rfl , isomorphic-to-itself σ ass rfl x))
             (f (resp σ ass rfl x))                                 ≡⟨ cong (λ iso → from (cast ass τ (rfl , iso)) (f (resp σ ass rfl x))) $
                                                                            isomorphic-to-itself-reflexivity σ ass I x ⟩
        from (cast ass τ (rfl , subst (Iso ass σ rfl x)
                                      (sym $ resp-refl σ ass x)
                                      (rflE x)))
             (f (resp σ ass rfl x))                                 ≡⟨ elim¹ (λ {y} x≡y →
                                                                                from (cast ass τ (rfl , subst (Iso ass σ rfl x)
                                                                                                              x≡y (rflE x)))
                                                                                     (f y) ≡
                                                                                f x)
                                                                             (cong (λ h → _≃_.from h (f x)) $ cast-refl ass τ)
                                                                             (sym $ resp-refl σ ass x) ⟩∎
        f x                                                         ∎

      where
      open _≃_
      open Assumptions ass

  -- Two definitions of isomorphism are equivalent.

  Iso≃Iso‴ :
    (ass : Assumptions) →
    ∀ {c} (σ : Ty c) {I J} (I≅J : Isomorphic ass c I J) {f g} →
    Iso ass σ I≅J f g ≃ (f ≡ _≃_.from (cast ass σ I≅J) g)

  Iso≃Iso‴ ass set I≅J {A} {B} =

    ↑ _ (A ≃ B)  ↔⟨ ↑↔ ⟩

    (A ≃ B)      ↝⟨ inverse $ ≡≃≃ (Assumptions.univ ass) ⟩□

    (A ≡ B)      □

  Iso≃Iso‴ ass (base A) I≅J {x} {y} =

    (x ≡ _≃_.from (Type-cong A ass I≅J) y)  □

  Iso≃Iso‴ ass (Π σ τ) I≅J {f} {g} =
    let iso-to-itself = isomorphic-to-itself σ ass I≅J in

    (∀ x y (x≅y : Iso ass σ I≅J x y) →
           Iso ass τ (I≅J , x≅y) (f x) (g y))                        ↝⟨ ∀-preserves ext₁ (λ x → ∀-preserves ext₁ λ y →
                                                                          Π-preserves ext₁ (Iso≃Iso″ ass σ I≅J) (λ x≅y →
           Iso ass τ (I≅J , x≅y) (f x) (g y)                                ↝⟨ Iso≃Iso″ ass τ (I≅J , x≅y) ⟩
           (resp τ ass (I≅J , x≅y) (f x) ≡ g y)                             ↝⟨ ≡⇒≃ $ cong (λ x≅y → resp τ ass (I≅J , x≅y) (f x) ≡ g y) $
                                                                                 sym $ left-inverse-of (Iso≃Iso″ ass σ I≅J) _ ⟩□
           (resp τ ass (I≅J , from (Iso≃Iso″ ass σ I≅J)
                                   (to (Iso≃Iso″ ass σ I≅J) x≅y))
               (f x) ≡ g y)                                                 □)) ⟩

    (∀ x y (x≡y : to (cast ass σ I≅J) x ≡ y) →
           resp τ ass (I≅J , from (Iso≃Iso″ ass σ I≅J) x≡y) (f x) ≡
           g y)                                                      ↝⟨ ∀-preserves ext₁ (λ x → inverse $ ↔⇒≃ $
                                                                          ∀-intro ext₁ (λ y x≡y → _ ≡ _)) ⟩
    (∀ x → resp τ ass (I≅J , iso-to-itself x) (f x) ≡
           g (resp σ ass I≅J x))                                     ↔⟨ extensionality-isomorphism ext₁ ⟩

    (resp τ ass (I≅J , iso-to-itself _) ∘ f ≡ g ∘ resp σ ass I≅J)    ↝⟨ to∘≡↔≡from∘ ext₁ (cast ass τ (I≅J , iso-to-itself _)) ⟩

    (f ≡ from (cast ass τ (I≅J , iso-to-itself _)) ∘
         g ∘ resp σ ass I≅J)                                         □

    where
    open _≃_
    open Assumptions ass

  abstract

    -- Two definitions of isomorphism are equivalent.

    Iso≃Iso″ ass σ I≅J {f} {g} =
      Iso ass σ I≅J f g                  ↝⟨ Iso≃Iso‴ ass σ I≅J ⟩

      (f ≡ _≃_.from (cast ass σ I≅J) g)  ↝⟨ inverse $ from≡↔≡to (inverse $ cast ass σ I≅J) ⟩□

      (_≃_.to (cast ass σ I≅J) f ≡ g)    □

  ----------------------------------------------------------------------
  -- An instantiation of the type extractor mechanism that gives us
  -- support for polymorphic types

  abstract

    reflexivityE-set :
      (ass : Assumptions) →
      ∀ {c} {I : ⟦ c ⟧} {A} →
      reflexivityE ass c (Dep set) I A ≡ lift Eq.id
    reflexivityE-set ass {c} {I} {A} =

      reflexivityE ass c (Dep set) I A                                 ≡⟨⟩

      lift (≡⇒≃ (to (from≡↔≡to (inverse Eq.id))
              (from (≡⇒≃ $ cong (λ B → B ≡ A) $
                       isomorphic-to-itself″ set ass
                         (reflexivity ass c I))
                    (subst (λ eq → subst (λ _ → Set) eq A ≡ A)
                           (sym $ right-inverse-of
                                    (isomorphism≃equality ass c)
                                    (refl I))
                           (refl A)))))                                ≡⟨ cong (λ eq → lift (≡⇒≃ (to (from≡↔≡to (inverse Eq.id)) eq))) $ sym $
                                                                            resp-refl-lemma set ass I A ⟩
      lift (≡⇒≃ (to (from≡↔≡to (inverse Eq.id))
                    (resp-refl set ass {I = I} A)))                    ≡⟨⟩

      lift (≡⇒≃ (to (from≡↔≡to (inverse Eq.id)) (refl A)))             ≡⟨⟩

      lift (≡⇒≃ (≡⇒→ (cong (λ B → B ≡ A)
                           (right-inverse-of (inverse Eq.id) A))
                     (cong id (refl A))))                              ≡⟨⟩

      lift (≡⇒≃ (≡⇒→ (cong (λ B → B ≡ A) (left-inverse-of Eq.id A))
                     (cong id (refl A))))                              ≡⟨ cong (λ eq → lift (≡⇒≃ (≡⇒→ (cong (λ B → B ≡ A) eq) (refl A))))
                                                                          left-inverse-of-id  ⟩
      lift (≡⇒≃ (≡⇒→ (cong (λ B → B ≡ A) (refl A)) (refl A)))          ≡⟨⟩

      lift (≡⇒≃ (≡⇒→ (refl (A ≡ A)) (refl A)))                         ≡⟨⟩

      lift (≡⇒≃ (refl A))                                              ≡⟨ refl _ ⟩∎

      lift Eq.id                                                       ∎

      where open _≃_

  ⟨0⟩ : ∀ {c} → Extractor (c ▻ Dep set)
  ⟨0⟩ {c} = record
    { Type                  = λ { (_ , A) → ↑ _ A }
    ; Type-cong             = λ { _ (_ , lift A≃B) → ↑-cong A≃B }
    ; Type-cong-reflexivity = λ { ass (I , A) →
        let open Assumptions ass; open _≃_ in

        lift-equality ext₁ (ext₁ λ { (lift x) → cong lift (

          to (lower (reflexivityE ass c (Dep set) I A)) x  ≡⟨ cong (λ eq → to (lower eq) x) $ reflexivityE-set ass ⟩∎

          x                                                ∎ )})}
    }

------------------------------------------------------------------------
-- Examples

-- For examples, see
-- Univalence-axiom.Isomorphism-is-equality.More.Examples.