------------------------------------------------------------------------
-- 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 (# 1) (# 1)
    univ  : Univalence (# 0)
    univ₁ : Univalence (# 1)

  abstract

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

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

-- An algebraic structure universe.

mutual

  -- Codes for structures.

  infixl 5 _▻_

  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 0 ⊤-contractible)
                                                    (↑-closure 1 (mono₁ 0 ⊤-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 (# 0))
  (univ₁ : Univalence (# 1))
  (univ₂ : Univalence (# 2)) 

  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-from∘≡⇒≃ ext₁
                                                                            (isomorphic-to-itself″ ass rfl)  z  z  x) _ ⟩∎
      from (≡⇒≃ $ cong  z  z  x) $ isomorphic-to-itself″ ass rfl)
           sx≡x                                                        

      where
      open _≃_
      open Assumptions ass

    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 6 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 0 ⊤-contractible)
                               (mono₁ 0 (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) 2)
  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 (# 1) (# 1) 
             {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 (# 1) (# 1) 
     {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.