text:
{-# OPTIONS --without-K #-}

-- This should really be called FinSet. From nlab:

-- FinSet is the category of finite sets and all functions between
-- them: the full subcategory of Set on finite sets. It is easy (and
-- thus common) to make FinSet skeletal; there is one object for each
-- natural number n (including n=0), and a morphism from m to n is an
-- m-tuple (f0,…,fm−1) of numbers satisfying 0≤fi<n. This amounts to
-- identifying n with the set {0,…,n−1}. (Sometimes {1,…,n} is used
-- instead.) This is exactly what we do below

-- Definition of the Operations on permutations, based on the Vector representation
-- There are 2 sets of definitions here:
-- 1. pure Vector, in which the contents are arbitrary sets
-- 2. specialized to Fin contents.

-- Some notes:
--   - There are operations (such as sequential composition) which 'lift' more
--     awkwardly.
--   - To avoid a proliferation of bad names, we use sub-modules

-- Cauchy representation Vec (Fin m) n without checks that m=n or
-- checks of uniqueness and completeness has a commutative semiring
-- structure (modulo a postulate about sym). This is the main building
-- block of ConcretePermutation

module FinVec where

open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Vec renaming (map to mapV; _++_ to _++V_; concat to concatV)
open import Data.Fin using (Fin; inject+; raise; zero; suc)
open import Function using (_∘_; id; _$_)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) renaming (map to map⊎)
open import Data.Product using (_×_; _,′_; proj₁; proj₂)

open import Equiv
open import TypeEquiv using (swap₊; swap⋆)
import TypeEquiv as TE
open import FinEquiv using (module Plus; module Times; module PlusTimes)
open import Proofs using (
  -- VectorLemmas
     _!!_; concat-map; map-map-map; lookup-map; map-∘
     )
import Level
open import Algebra
open import Algebra.Structures
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality using (subst; sym; trans; cong₂)
open import Groupoid

------------------------------------------------------------------------------
-- Pure vector operations
-- Does not involve Fin at all.
-- Note: not exported!

private

  module V where
    _⊎v_ : ∀ {m n} {A B : Set} → Vec A m → Vec B n → Vec (A ⊎ B) (m + n)
    α ⊎v β = tabulate (inj₁ ∘ _!!_ α) ++V tabulate (inj₂ ∘ _!!_ β)

    swap+ : {m n : ℕ} {A B : Set} → Vec (A ⊎ B) (m + n) → Vec (B ⊎ A) (m + n)
    swap+ v = tabulate (swap₊ ∘ _!!_ v)

    _×v_ : ∀ {m n} {A B : Set} → Vec A m → Vec B n → Vec (A × B) (m * n)
    α ×v β = α >>= (λ b → mapV (_,′_ b) β)

    0v : {A : Set} → Vec A 0
    0v = []

------------------------------------------------------------------------------
-- Elementary permutations, Fin version
-- Cauchy Representation Vec (Fin m) n without checks of uniqueness
-- and completeness

-- We need to define (at least) 0, 1, +, *, ∘, swap+, swap*

module F where

  open import Data.Nat.Properties.Simple using (+-right-identity)
  open import Data.Vec.Properties
    using (lookup-allFin; tabulate∘lookup; lookup∘tabulate; tabulate-∘; lookup-++-inject+)
  open import Relation.Binary.PropositionalEquality
    using (_≡_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)
  open ≡-Reasoning

  open import Equiv using (_∼_)
  open import Proofs using (congD!;
    -- FinNatLemmas
       inject+0≡uniti+;
    -- FiniteFunctions
       finext;
    -- VectorLemmas
       lookupassoc; map-++-commute; tabulate-split; left!!; right!!;
       lookup-++-raise; unSplit; tab++[]≡tab∘̂unite+
       )

  open V

  -- convenient abbreviations
  FinVec : ℕ → ℕ → Set
  FinVec m n = Vec (Fin m) n

  private
    fwd : {m n : ℕ} → (Fin m ⊎ Fin n) → Fin (m + n)
    fwd = proj₁ Plus.fwd-iso

    bwd : {m n : ℕ} → Fin (m + n) → (Fin m ⊎ Fin n)
    bwd = Equiv.qinv.g (proj₂ Plus.fwd-iso)

    bwd∘fwd~id : {m n : ℕ} → bwd {m} {n} ∘ fwd ∼ id
    bwd∘fwd~id = Equiv.qinv.β (proj₂ Plus.fwd-iso)

  -- make all the definitions abstract.  Note that the type isn't,
  -- otherwise we could not do anything at all with it!

  abstract
    -- principal component of the identity permutation
    1C : {n : ℕ} → FinVec n n
    1C {n} = allFin n

    -- corresponds to ⊥ ≃ (⊥ × A) and other impossibilities
    -- but don't use it, as it is abstract and will confuse external proofs!
    0C : FinVec 0 0
    0C = 1C {0}

    -- Sequential composition
    _∘̂_ : {n₀ n₁ n₂ : ℕ} → Vec (Fin n₁) n₀ → Vec (Fin n₂) n₁ → Vec (Fin n₂) n₀
    π₁ ∘̂ π₂ = tabulate (_!!_ π₂ ∘ _!!_ π₁)

    -- swap the first m elements with the last n elements
    -- [ v₀ , v₁   , v₂   , ... , vm-1 ,     vm , vm₊₁ , ... , vm+n-1 ]
    -- ==>
    -- [ vm , vm₊₁ , ... , vm+n-1 ,     v₀ , v₁   , v₂   , ... , vm-1 ]

    swap+cauchy : (m n : ℕ) → FinVec (n + m) (m + n)
    swap+cauchy m n = tabulate (Plus.swapper m n)

    -- Parallel additive composition
    -- conceptually, what we want is
    _⊎c'_ : ∀ {m₁ n₁ m₂ n₂} → FinVec m₁ m₂ → FinVec n₁ n₂ → FinVec (m₁ + n₁) (m₂ + n₂)
    _⊎c'_ α β = mapV fwd (α ⊎v β)
    -- but the above is tedious to work with.  Instead, inline a bit to get
    _⊎c_ : ∀ {m₁ n₁ m₂ n₂} → FinVec m₁ m₂ → FinVec n₁ n₂ → FinVec (m₁ + n₁) (m₂ + n₂)
    _⊎c_ {m₁} α β = tabulate (fwd ∘ inj₁ ∘ _!!_ α) ++V
                     tabulate (fwd {m₁} ∘ inj₂ ∘ _!!_ β)
    -- see ⊎c≡⊎c' lemma below

    _⊎fv_ : ∀ {m₁ n₁ m₂ n₂} → FinVec m₁ m₂ → FinVec n₁ n₂ → FinVec (m₁ + n₁) (m₂ + n₂)
    _⊎fv_ {m₁} α β = tabulate (λ j → fwd (map⊎ (_!!_ α) (_!!_ β) (bwd j)))

    ⊎-equiv : ∀ {m₁ n₁ m₂ n₂} → (α : FinVec m₁ m₂) → (β : FinVec n₁ n₂) → α ⊎c β ≡ α ⊎fv β
    ⊎-equiv {m₁} {n₁} {m₂} {n₂} α β =
      let mm s = map⊎ (_!!_ α) (_!!_ β) s in
      let g = fwd ∘ mm ∘ bwd in
      begin (
      tabulate (λ j → fwd (inj₁ (α !! j))) ++V tabulate (λ j → fwd {m₁} (inj₂ (β !! j)))
        ≡⟨ refl ⟩ -- map⊎ evaluates on inj₁/inj₂
      tabulate (fwd ∘ mm ∘ inj₁) ++V tabulate (fwd ∘ mm ∘ inj₂)
        ≡⟨ cong₂ _++V_ (finext (λ i → cong (fwd ∘ mm) (sym (bwd∘fwd~id (inj₁ i)))))
                       (finext (λ i → cong (fwd ∘ mm) (sym (bwd∘fwd~id (inj₂ i))))) ⟩
      tabulate {m₂} (g ∘ fwd ∘ inj₁) ++V tabulate {n₂} (g ∘ fwd {m₂} ∘ inj₂)
        ≡⟨ sym (tabulate-split {m₂} {n₂} {f = g}) ⟩
      tabulate g ∎)
      where
        open ≡-Reasoning

    -- Tensor multiplicative composition
    -- Transpositions in α correspond to swapping entire rows
    -- Transpositions in β correspond to swapping entire columns
    _×c_ : ∀ {m₁ n₁ m₂ n₂} → FinVec m₁ m₂ → FinVec n₁ n₂ → FinVec (m₁ * n₁) (m₂ * n₂)
    α ×c β = mapV Times.fwd (α ×v β)

    -- swap⋆
    --
    -- This is essentially the classical problem of in-place matrix transpose:
    -- "http://en.wikipedia.org/wiki/In-place_matrix_transposition"
    -- Given m and n, the desired permutation in Cauchy representation is:
    -- P(i) = m*n-1 if i=m*n-1
    --      = m*i mod m*n-1 otherwise

    -- transposeIndex : {m n : ℕ} → Fin m × Fin n → Fin (n * m)
    -- transposeIndex = Times.fwd ∘ swap
      -- inject≤ (fromℕ (toℕ d * m + toℕ b)) (i*n+k≤m*n d b)

    swap⋆cauchy : (m n : ℕ) → FinVec (n * m) (m * n)
    swap⋆cauchy m n = tabulate (Times.swapper m n)
      -- mapV transposeIndex (V.tcomp 1C 1C)

    -------------------------------------------------------------------------------------------
    -- Things which are the foundations of other permutations, but coming
    -- from properties, rather than being operators

    unite+ : {m : ℕ} → FinVec m (0 + m)
    unite+ {m} = tabulate (proj₁ (Plus.unite+ {m}))

    uniti+ : {m : ℕ} → FinVec (0 + m) m
    uniti+ {m} = tabulate (proj₁ (Plus.uniti+ {m}))

    unite+r : {m : ℕ} → FinVec m (m + 0)
    unite+r {m} = tabulate (proj₁ (Plus.unite+r {m}))

    uniti+r : {m : ℕ} → FinVec (m + 0) m
    uniti+r {m} = tabulate (proj₁ (Plus.uniti+r {m}))

    assocl+ : {m n o : ℕ} → FinVec  ((m + n) + o) (m + (n + o))
    assocl+ {m} {n} {o} = tabulate (proj₁ (Plus.assocl+ {m} {n} {o}))

    assocr+ : {m n o : ℕ} → FinVec  (m + (n + o)) (m + n + o)
    assocr+ {m} {n} {o} = tabulate (proj₁ (Plus.assocr+ {m} {n} {o}))

    unite* : {m : ℕ} → FinVec m (1 * m)
    unite* {m} = tabulate (proj₁ (Times.unite* {m}))

    uniti* : {m : ℕ} → FinVec (1 * m) m
    uniti* {m} = tabulate (proj₁ (Times.uniti* {m}))

    unite*r : {m : ℕ} → FinVec m (m * 1)
    unite*r {m} = tabulate (proj₁ (Times.unite*r {m}))

    uniti*r : {m : ℕ} → FinVec (m * 1) m
    uniti*r {m} = tabulate (proj₁ (Times.uniti*r {m}))

    assocl* : {m n o : ℕ} → FinVec  ((m * n) * o) (m * (n * o))
    assocl* {m} {n} {o} = tabulate (proj₁ (Times.assocl* {m} {n} {o}))

    assocr* : {m n o : ℕ} → FinVec  (m * (n * o)) (m * n * o)
    assocr* {m} {n} {o} = tabulate (proj₁ (Times.assocr* {m} {n} {o}))

    dist*+ : ∀ {m n o} → FinVec (m * o + n * o) ((m + n) * o)
    dist*+ {m} {n} {o} = tabulate (proj₁ (PlusTimes.dist {m} {n} {o}))

    factor*+ : ∀ {m n o} → FinVec ((m + n) * o) (m * o + n * o)
    factor*+ {m} {n} {o} = tabulate (proj₁ (PlusTimes.factor {m} {n} {o}))

    distl*+ : ∀ {m n o} → FinVec (m * n + m * o) (m * (n + o))
    distl*+ {m} {n} {o} = tabulate (proj₁ (PlusTimes.distl {m} {n} {o}))

    factorl*+ : ∀ {m n o} → FinVec (m * (n + o)) (m * n + m * o)
    factorl*+ {m} {n} {o} = tabulate (proj₁ (PlusTimes.factorl {m} {n} {o}))

    right-zero*l : ∀ {m} → FinVec 0 (m * 0)
    right-zero*l {m} = tabulate (proj₁ (Times.distzr {m}))

    right-zero*r : ∀ {m} → FinVec (m * 0) 0
    right-zero*r {m} = tabulate (proj₁ (Times.factorzr {m}))

    -------------------------------------------------------------------------------------------
    -- Below here, we start with properties

    -- Useful stuff
    infix 4 _∼p_

    _∼p_ : {n m : ℕ} (p₁ p₂ : Vec (Fin m) n) → Set
    _∼p_ {n} p₁ p₂ = (i : Fin n) → p₁ !! i ≡ p₂ !! i

    ∼p⇒≡ : {n : ℕ} {p₁ p₂ : Vec (Fin n) n} → (p₁ ∼p p₂) → p₁ ≡ p₂
    ∼p⇒≡ {n} {p₁} {p₂} eqv =
      begin (
        p₁                            ≡⟨ sym (tabulate∘lookup p₁) ⟩
        tabulate (_!!_ p₁)            ≡⟨ finext eqv ⟩
        tabulate (_!!_ p₂)            ≡⟨ tabulate∘lookup p₂ ⟩
        p₂ ∎)
      where open ≡-Reasoning

    -- note the flip!
    ∘̂⇒∘ : {m n o : ℕ} → (f : Fin m → Fin n) → (g : Fin n → Fin o) →
              tabulate f ∘̂ tabulate g ∼p tabulate (g ∘ f)
    ∘̂⇒∘ f g i =
      begin (
        (tabulate f ∘̂ tabulate g) !! i
          ≡⟨ lookup∘tabulate _ i ⟩
        (tabulate g) !! (tabulate f !! i)
          ≡⟨ lookup∘tabulate _ (tabulate f !! i) ⟩
        g (tabulate f !! i)
          ≡⟨ cong g (lookup∘tabulate f i) ⟩
        g (f i)
          ≡⟨ sym (lookup∘tabulate (g ∘ f) i) ⟩
        tabulate (g ∘ f) !! i ∎)
      where open ≡-Reasoning

    -- this is just tabulate∘lookup, but it hides the details; should this be
    -- called 'join' or 'flatten' ?
    cauchyext : {m n : ℕ} (π : FinVec m n) → tabulate (_!!_ π) ≡ π
    cauchyext π = tabulate∘lookup π

    -- we could go through ~p, but this works better in practice
    ~⇒≡ : {m n : ℕ} {f : Fin m → Fin n} {g : Fin n → Fin m} →
               (f ∘ g ∼ id) → (tabulate g ∘̂ tabulate f ≡ 1C)
    ~⇒≡ {f = f} {g} β = ∼p⇒≡ (λ i → trans (∘̂⇒∘ g f i) (cong (λ x → x !! i) (finext β)))

    -- make a permutation from something lower level, directly
    --  ~⇒≡ {m} {n = m} {o = m} (p∘!p≡id {p = Plus.unite+ {m}})

    -- properties of sequential composition
    ∘̂-assoc : {m₁ m₂ m₃ m₄ : ℕ} →
             (a : Vec (Fin m₂) m₁) (b : Vec (Fin m₃) m₂) (c : Vec (Fin m₄) m₃) →
             a ∘̂ (b ∘̂ c) ≡ (a ∘̂ b) ∘̂ c
    ∘̂-assoc a b c = finext (lookupassoc a b c)

    ∘̂-rid : {m n : ℕ} → (π : Vec (Fin m) n) → π ∘̂ 1C ≡ π
    ∘̂-rid π = trans (finext (λ i → lookup-allFin (π !! i))) (cauchyext π)

    ∘̂-lid : {m n : ℕ} → (π : Vec (Fin m) n) → 1C ∘̂ π ≡ π
    ∘̂-lid π = trans (finext (λ i → cong (_!!_ π) (lookup-allFin i))) (cauchyext π)

    !!⇒∘̂ : {n₁ n₂ n₃ : ℕ} →
            (π₁ : Vec (Fin n₁) n₂) → (π₂ : Vec (Fin n₂) n₃) → (i : Fin n₃) →
            π₁ !! (π₂ !! i) ≡ (π₂ ∘̂ π₁) !! i
    !!⇒∘̂ π₁ π₂ i =
      begin (
        π₁ !! (π₂ !! i)
              ≡⟨ sym (lookup∘tabulate (λ j → (π₁ !! (π₂ !! j))) i) ⟩
        tabulate (λ i → π₁ !! (π₂ !! i)) !! i
              ≡⟨ refl ⟩
        (π₂ ∘̂ π₁) !! i ∎)
      where open ≡-Reasoning

    -- properties of sequential composition
    0C∘̂0C≡0C : 1C {0} ∘̂ 1C {0} ≡ 1C {0}
    0C∘̂0C≡0C = refl

    -- properties of parallel composition
    -- trivial ones first
    1C₀⊎x≡x : ∀ {m n} {x : FinVec m n} → 1C {0} ⊎c x ≡ x
    1C₀⊎x≡x {x = x} = cauchyext x

    unite+∘[0⊎x]≡x∘unite+ : ∀ {m n} {x : FinVec m n} → unite+ ∘̂ (1C {0} ⊎c x) ≡ x ∘̂ unite+
    unite+∘[0⊎x]≡x∘unite+ {m} {n} {x} = finext pf
      where
        pf : (i : Fin n) → (0C ⊎c x) !! (unite+ !! i) ≡ unite+ !! (x !! i)
        pf i =
          begin (
            tabulate (λ y → x !! y) !! (tabulate id !! i)
              ≡⟨ cong (λ j → tabulate (λ y → x !! y) !! j) (lookup∘tabulate id i) ⟩
            tabulate (λ y → x !! y) !! i
              ≡⟨ lookup∘tabulate (_!!_ x) i ⟩
            x !! i
              ≡⟨ sym (lookup∘tabulate id (x !! i)) ⟩
            tabulate id !! (x !! i) ∎)

    uniti+∘x≡[0⊎x]∘uniti+ : ∀ {m n} {x : FinVec m n} →
      uniti+ ∘̂ x ≡ (1C {0} ⊎c x) ∘̂ uniti+
    uniti+∘x≡[0⊎x]∘uniti+ {m} {n} {x} = finext pf
      where
        pf : (i : Fin n) → x !! (uniti+ !! i) ≡ uniti+ !! ((0C ⊎c x) !! i)
        pf i = begin (
          x !! (tabulate id !! i)
            ≡⟨ cong (_!!_ x) (lookup∘tabulate id i) ⟩
          x !! i
            ≡⟨ sym (lookup∘tabulate (λ y → x !! y) i) ⟩
          tabulate (λ y → x !! y) !! i
            ≡⟨ sym (lookup∘tabulate id _) ⟩
          tabulate id !! (tabulate (λ y → x !! y) !! i) ∎)

{-
    x⊎1C₀≡x : ∀ {m n} {x : FinVec m n} → x ⊎c (1C {0}) ≡ ?
    x⊎1C₀≡x {m} {n} {x = x} =
      let e = proj₁ (Plus.unite+) in
      let i = proj₁ (Plus.uniti+) in
      let eq = sym (+-right-identity m) in
      begin (
        tabulate (λ j → inject+ 0 (x !! j)) ++V []
          ≡⟨ cong (λ x → x ++V []) (finext (λ j → inject+0≡uniti+ (x !! j) eq)) ⟩
        tabulate (λ j → i (x !! j)) ++V []
          ≡⟨ tab++[]≡tab∘̂unite+ (λ j → i (x !! j)) (+-right-identity n) ⟩
        tabulate (λ j → i (x !! e j))
          ≡⟨ finext (λ j → sym (lookup∘tabulate (λ k → i (x !! k)) (e j))) ⟩
        tabulate (λ j → tabulate (λ k → i (x !! k)) !! (e j))
          ≡⟨ finext (λ j → cong₂ _!!_
                           (finext (λ k → sym (lookup∘tabulate i (x !! k))))
                           (sym (lookup∘tabulate e j))) ⟩
        tabulate (λ j →
           (tabulate (λ k → tabulate i !! (x !! k))) !! ((tabulate e) !! j))
         ∎)
      where open ≡-Reasoning -}

    1C⊎1C≡1C : ∀ {m n} → 1C {m} ⊎c 1C {n} ≡ 1C
    1C⊎1C≡1C {m} {n} =
      begin (
         tabulate {m} (inject+ n ∘ _!!_ 1C) ++V tabulate {n} (raise m ∘ _!!_ 1C)
           ≡⟨ cong₂ (_++V_ {m = m}) (finext (λ i → cong (inject+ n) (lookup-allFin i)))
                                      (finext (λ i → cong (raise m) (lookup-allFin i))) ⟩
         tabulate {m} (inject+ n) ++V tabulate {n} (raise m)
           ≡⟨ unSplit {m} id ⟩
         tabulate {m + n} id ∎)
      where open ≡-Reasoning

    1C!!i≡i : ∀ {m} {i : Fin m} → 1C {m} !! i ≡ i
    1C!!i≡i = lookup∘tabulate id _

    unite+∘̂uniti+~id : ∀ {m} → (unite+ {m}) ∘̂ uniti+ ≡ 1C {m}
    unite+∘̂uniti+~id {m} = ~⇒≡ {m} {n = m} (p∘!p≡id {p = Plus.unite+ {m}})

    uniti+∘̂unite+~id : ∀ {m} → (uniti+ {m}) ∘̂ unite+ ≡ 1C {m}
    uniti+∘̂unite+~id {m} = ~⇒≡ {m} {n = m} (p∘!p≡id {p = Plus.uniti+})

    unite+r∘̂uniti+r~id : ∀ {m} → (unite+r {m}) ∘̂ uniti+r ≡ 1C {m + 0}
    unite+r∘̂uniti+r~id {m} = ~⇒≡ {m} (p∘!p≡id {p = Plus.unite+r {m}})

    uniti+r∘̂unite+r~id : ∀ {m} → (uniti+r {m}) ∘̂ unite+r ≡ 1C {m}
    uniti+r∘̂unite+r~id {m} = ~⇒≡ (p∘!p≡id {p = Plus.uniti+r})

    assocl+∘̂assocr+~id : ∀ {m n o} → assocl+ {m} {n} {o} ∘̂ assocr+ {m} ≡ 1C
    assocl+∘̂assocr+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = Plus.assocl+ {m}})

    assocr+∘̂assocl+~id : ∀ {m n o} → assocr+ {m} {n} {o} ∘̂ assocl+ {m} ≡ 1C
    assocr+∘̂assocl+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = Plus.assocr+ {m}})

    swap+-inv : ∀ {m n} → swap+cauchy m n ∘̂ swap+cauchy n m ≡ 1C
    swap+-inv {m} {n} = ~⇒≡ (Plus.swap-inv m n)

    idˡ⊕ : ∀ {m n} {x : FinVec m n} → uniti+ ∘̂ (1C {0} ⊎c x) ≡ x ∘̂ uniti+
    idˡ⊕ {m} {n} {x} = finext pf
      where
        open ≡-Reasoning
        pf : (i : Fin n) → (1C {0} ⊎c x) !! (uniti+ !! i) ≡ (uniti+ !! (x !! i))
        pf i =  begin (
          tabulate (λ y → x !! y) !! (tabulate id !! i)
            ≡⟨ cong (_!!_ (tabulate λ y → x !! y)) (lookup∘tabulate id i) ⟩
          (tabulate (λ y → x !! y)) !! i
            ≡⟨ lookup∘tabulate (λ y → x !! y) i ⟩
          x !! i
            ≡⟨ sym (lookup∘tabulate id (x !! i)) ⟩
          tabulate id !! (x !! i) ∎)

    [,]-commute : {A B C D E : Set} → {f : A → C} → {g : B → C} → {h : C → D} →
      ∀ x → h ([ f , g ]′ x) ≡ [ (h ∘ f) , (h ∘ g) ]′ x
    [,]-commute (inj₁ x) = refl
    [,]-commute (inj₂ y) = refl

{-
    assocl-commute : ∀ {m₁ m₂ m₃ n₁ n₂ n₃} {a : FinVec m₁ n₁} {b : FinVec m₂ n₂}
      {c : FinVec m₃ n₃} → assocl+ {n₁} ∘̂ ((a ⊎c b) ⊎c c) ≡ (a ⊎c (b ⊎c c)) ∘̂ assocl+ {m₁}
    assocl-commute {m₁} {m₂} {m₃} {n₁} {n₂} {n₃} {a} {b} {c} = begin (
      assocl+ {n₁} ∘̂ ((a ⊎c b) ⊎c c)
        ≡⟨ cong (λ x → assocl+ {n₁} ∘̂ x) (trans (⊎-equiv (a ⊎c b) c) (cong (λ x → x ⊎fv c) (⊎-equiv a b))) ⟩
      assocl+ {n₁} ∘̂ ((a ⊎fv b) ⊎fv c)
        ≡⟨ refl ⟩
      tabulate (λ i → ((a ⊎fv b) ⊎fv c) !! (assocl+ {n₁} !! i))
        ≡⟨ finext pf₁ ⟩
      tabulate (λ i → assocl+ {m₁} !! ((a ⊎fv (b ⊎fv c)) !! i) )
        ≡⟨ refl ⟩
      (a ⊎fv (b ⊎fv c)) ∘̂ assocl+ {m₁}
        ≡⟨ cong (λ x → x ∘̂ assocl+ {m₁}) (sym (trans (cong (λ x → a ⊎c x) (⊎-equiv b c)) (⊎-equiv a (b ⊎fv c)))) ⟩
      (a ⊎c (b ⊎c c)) ∘̂ assocl+ {m₁} ∎)
      where
        pf₁ : ∀ i →  ((a ⊎fv b) ⊎fv c) !! (assocl+ {n₁} !! i) ≡ assocl+ {m₁} !! ((a ⊎fv (b ⊎fv c)) !! i)
        pf₁ i =
          let assoc1 k = proj₁ (Plus.assocl+ {n₁}) k in
          let assoc2 k = proj₁ (Plus.assocl+ {m₁} {m₂}) k in
          let abc!! = (_!!_ ((a ⊎fv b) ⊎fv c)) in
          let a!! = (_!!_ a) in let b!! = (_!!_ b) in let c!! = (_!!_ c) in
          let ab!! = (_!!_ (a ⊎fv b)) in
          let bc!! = (_!!_ (b ⊎fv c)) in
          let iso4 = ((sym≃ (Plus.fwd-iso {n₁})) ● ((path⊎ id≃ (sym≃ Plus.fwd-iso)) ● (TE.assocl₊equiv ● (path⊎ Plus.fwd-iso id≃)))) in
          let iso3 = (sym≃ (Plus.fwd-iso {n₁})) ● ((path⊎ id≃ (sym≃ Plus.fwd-iso)) ● (TE.assocl₊equiv)) in
          let iso4b = (path⊎ id≃ (sym≃ Plus.fwd-iso) ● ((TE.assocl₊equiv ● path⊎ Plus.fwd-iso id≃) ● Plus.fwd-iso)) in
          begin (
          ((a ⊎fv b) ⊎fv c) !! (assocl+ {n₁} !! i)
            ≡⟨ cong abc!! (lookup∘tabulate _ i) ⟩
          abc!! (assoc1 i)
            ≡⟨ lookup∘tabulate _ (assoc1 i) ⟩
          fwd (map⊎ ab!! c!! (bwd (assoc1 i)))
            ≡⟨ cong (fwd ∘ map⊎ ab!! c!!) (bwd∘fwd~id (iso4 ⋆ i)) ⟩
          fwd (map⊎ ab!! c!! (iso4 ⋆ i))
            ≡⟨ cong fwd (merge-[,] {h = fwd} {i = id} (iso3 ⋆ i)) ⟩
          fwd (map⊎ (ab!! ∘ fwd) c!! (iso3 ⋆ i))
            ≡⟨ {!!} ⟩
          iso4b ⋆ (map⊎ a!! bc!! (bwd i))
            ≡⟨ sym (cong (λ x → iso4b ⋆ x) (bwd∘fwd~id (map⊎ a!! bc!! (bwd i)))) ⟩
          assoc2 (fwd (map⊎ a!! bc!! (bwd i)))
            ≡⟨ sym (cong assoc2 (lookup∘tabulate _ i)) ⟩
          assoc2 ((a ⊎fv (b ⊎fv c)) !! i)
            ≡⟨ sym (lookup∘tabulate assoc2 _) ⟩
          assocl+ {m₁} !! ((a ⊎fv (b ⊎fv c)) !! i) ∎)
-}
    -- properties of multiplicative composition
    unite*∘̂uniti*~id : ∀ {m} → (unite* {m}) ∘̂ uniti* ≡ 1C {1 * m}
    unite*∘̂uniti*~id {m} = ~⇒≡ {m} {n = 1 * m} (p∘!p≡id {p = Times.unite* {m}})

    uniti*∘̂unite*~id : ∀ {m} → (uniti* {m}) ∘̂ unite* ≡ 1C {m}
    uniti*∘̂unite*~id {m} = ~⇒≡ {1 * m} {n = m} (p∘!p≡id {p = Times.uniti* {m}})

    unite*r∘̂uniti*r~id : ∀ {m} → (unite*r {m}) ∘̂ uniti*r ≡ 1C {m * 1}
    unite*r∘̂uniti*r~id {m} = ~⇒≡ {m} {n = m * 1} (p∘!p≡id {p = Times.unite*r {m}})

    uniti*r∘̂unite*r~id : ∀ {m} → (uniti*r {m}) ∘̂ unite*r ≡ 1C {m}
    uniti*r∘̂unite*r~id {m} = ~⇒≡ {m * 1} {n = m} (p∘!p≡id {p = Times.uniti*r {m}})

    assocl*∘̂assocr*~id : ∀ {m n o} → assocl* {m} {n} {o} ∘̂ assocr* {m} ≡ 1C
    assocl*∘̂assocr*~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = Times.assocl* {m}})

    assocr*∘̂assocl*~id : ∀ {m n o} → assocr* {m} {n} {o} ∘̂ assocl* {m} ≡ 1C
    assocr*∘̂assocl*~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = Times.assocr* {m}})

    dist*+∘̂factor*+~id : ∀ {m n o} → dist*+ {m} {n} {o} ∘̂ factor*+ {m} ≡ 1C
    dist*+∘̂factor*+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = PlusTimes.dist {m}})

    factor*+∘̂dist*+~id : ∀ {m n o} → factor*+ {m} {n} {o} ∘̂ dist*+ {m} ≡ 1C
    factor*+∘̂dist*+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = PlusTimes.factor {m}})

    distl*+∘̂factorl*+~id : ∀ {m n o} → distl*+ {m} {n} {o} ∘̂ factorl*+ {m} ≡ 1C
    distl*+∘̂factorl*+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = PlusTimes.distl {m}})

    factorl*+∘̂distl*+~id : ∀ {m n o} → factorl*+ {m} {n} {o} ∘̂ distl*+ {m} ≡ 1C
    factorl*+∘̂distl*+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = PlusTimes.factorl {m}})

    right-zero*l∘̂right-zero*r~id : ∀ {m} → right-zero*l {m} ∘̂ right-zero*r {m} ≡ 1C {m * 0}
    right-zero*l∘̂right-zero*r~id {m} = ~⇒≡ {f = proj₁ (Times.factorzr {m})} (p∘!p≡id {p = Times.distzr {m}})

    right-zero*r∘̂right-zero*l~id : ∀ {m} → right-zero*r {m} ∘̂ right-zero*l {m} ≡ 1C
    right-zero*r∘̂right-zero*l~id {m} = ~⇒≡ { f = proj₁ (Times.factorz {m})} (p∘!p≡id {p = Times.distz {m}})

    private
      left⊎⊎!! :  ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → (p₁ : FinVec m₁ n₁) → (p₂ : FinVec m₂ n₂)
        → (p₃ : FinVec m₃ m₁) → (p₄ : FinVec m₄ m₂) → (i : Fin n₁) →
        (p₃ ⊎c p₄) !! ( (p₁ ⊎c p₂) !! inject+ n₂ i ) ≡ inject+ m₄ ( (p₁ ∘̂ p₃) !! i)
      left⊎⊎!! {m₁} {m₂} {_} {m₄} {_} {n₂} p₁ p₂ p₃ p₄ i =
        let pp = p₃ ⊎c p₄ in
        let qq = p₁ ⊎c p₂ in
        begin (
            pp !! (qq !! inject+ n₂ i)
              ≡⟨ cong
                   (_!!_ pp)
                   (lookup-++-inject+
                     (tabulate (inject+ m₂ ∘ _!!_ p₁))
                     (tabulate (raise m₁ ∘ _!!_ p₂))
                     i) ⟩
           pp !! (tabulate (inject+ m₂ ∘ _!!_ p₁ ) !! i)
              ≡⟨ cong (_!!_ pp) (lookup∘tabulate _ i) ⟩
           pp !! (inject+ m₂ (p₁ !! i))
              ≡⟨ left!! (p₁ !! i) (inject+ m₄ ∘ (_!!_ p₃)) ⟩
            inject+ m₄ (p₃ !! (p₁ !! i))
              ≡⟨ cong (inject+ m₄) (sym (lookup∘tabulate _ i)) ⟩
            inject+ m₄ ((p₁ ∘̂ p₃) !! i) ∎ )

      right⊎⊎!! :  ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → (p₁ : FinVec m₁ n₁) → (p₂ : FinVec m₂ n₂)
        → (p₃ : FinVec m₃ m₁) → (p₄ : FinVec m₄ m₂) → (i : Fin n₂) →
        (p₃ ⊎c p₄) !! ( (p₁ ⊎c p₂) !! raise n₁ i ) ≡ raise m₃ ( (p₂ ∘̂ p₄) !! i)
      right⊎⊎!! {m₁} {m₂} {m₃} {_} {n₁} {_} p₁ p₂ p₃ p₄ i =
        let pp = p₃ ⊎c p₄ in
        let qq = p₁ ⊎c p₂ in
        begin (
          pp !! (qq !! raise n₁ i)
            ≡⟨ cong
                 (_!!_ pp)
                 (lookup-++-raise
                   (tabulate (inject+ m₂ ∘ _!!_ p₁))
                   (tabulate (raise m₁ ∘ _!!_ p₂))
                   i) ⟩
          pp !! (tabulate (raise m₁ ∘ _!!_ p₂) !! i)
            ≡⟨ cong (_!!_ pp) (lookup∘tabulate _ i) ⟩
          pp !! raise m₁ (p₂ !! i)
            ≡⟨ right!! {m₁} (p₂ !! i) (raise m₃ ∘ (_!!_ p₄)) ⟩
          raise m₃ (p₄ !! (p₂ !! i))
            ≡⟨ cong (raise m₃) (sym (lookup∘tabulate _ i)) ⟩
          raise m₃ ((p₂ ∘̂ p₄) !! i) ∎ )

    ⊎c-distrib : ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → {p₁ : FinVec m₁ n₁} → {p₂ : FinVec m₂ n₂}
      → {p₃ : FinVec m₃ m₁} → {p₄ : FinVec m₄ m₂} →
        (p₁ ⊎c p₂) ∘̂ (p₃ ⊎c p₄) ≡ (p₁ ∘̂ p₃) ⊎c (p₂ ∘̂ p₄)
    ⊎c-distrib {m₁} {m₂} {m₃} {m₄} {n₁} {n₂} {p₁} {p₂} {p₃} {p₄} =
      let p₃₄ = p₃ ⊎c p₄ in let p₁₂ = p₁ ⊎c p₂ in
      let lhs = λ i → p₃₄ !! (p₁₂ !! i) in
      begin (
        tabulate lhs
          ≡⟨ tabulate-split {n₁} {n₂} ⟩
        tabulate {n₁} (lhs ∘ inject+ n₂) ++V tabulate {n₂} (lhs ∘ raise n₁)
          ≡⟨ cong₂ _++V_ (finext (left⊎⊎!! p₁ _ _ _)) (finext (right⊎⊎!! p₁ _ _ _)) ⟩
        tabulate {n₁} (λ i → inject+ m₄ ((p₁ ∘̂ p₃) !! i)) ++V
        tabulate {n₂} (λ i → raise m₃ ((p₂ ∘̂ p₄) !! i))
          ≡⟨ refl ⟩
        (p₁ ∘̂ p₃) ⊎c (p₂ ∘̂ p₄) ∎)

    ------------------------------------------------------------------------------
    -- properties of ×c

    private
      concat!! : {A : Set} {m n : ℕ} → (a : Fin m) → (b : Fin n) → (xss : Vec (Vec A n) m) →
        concatV xss !! (Times.fwd (a ,′ b)) ≡ (xss !! a) !! b
      concat!! zero b (xs ∷ xss) = lookup-++-inject+ xs (concatV xss) b
      concat!! (suc a) b (xs ∷ xss) =
        trans (lookup-++-raise xs (concatV xss) (Times.fwd (a ,′ b))) (concat!! a b xss)

      ×c-equiv : {m₁ m₂ n₁ n₂ : ℕ} (p₁ : FinVec m₁ n₁) (p₂ : FinVec m₂ n₂) →
        (p₁ ×c p₂) ≡ concatV (mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂)) p₁)
      ×c-equiv p₁ p₂ =
        let zss = mapV  (λ b → mapV (λ x → b ,′ x) p₂) p₁ in
        begin (
          (p₁ ×c p₂)
            ≡⟨ refl ⟩
          mapV Times.fwd (concatV zss)
            ≡⟨ sym (concat-map zss Times.fwd) ⟩
          concatV (mapV (mapV Times.fwd) zss)
            ≡⟨ cong concatV (map-map-map Times.fwd (λ b → mapV (λ x → b ,′ x) p₂) p₁) ⟩
           concatV (mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂)) p₁) ∎)

      lookup-2d : {A : Set} (m n : ℕ) → (k : Fin (m * n)) → {f : Fin m × Fin n → A} →
         concatV (tabulate {m} (λ i → tabulate {n} (λ j → f (i ,′ j)))) !! k ≡ f (Times.bwd k)
      lookup-2d m n k {f} =
        let lhs =  concatV (tabulate {m} (λ i → tabulate {n} (λ j → f (i ,′ j)))) in
        let a = proj₁ (Times.bwd {m} {n} k) in
        let b = proj₂ (Times.bwd {m} {n} k) in
        begin (
          lhs !! k
            ≡⟨ cong (_!!_ lhs) (sym (Times.fwd∘bwd~id {m} k)) ⟩
          lhs !! (Times.fwd (a ,′ b))
            ≡⟨ concat!! a b _ ⟩
          (tabulate {m} (λ i → tabulate {n} (λ j → f (i ,′ j))) !! a) !! b
            ≡⟨ cong (λ x → x !! b) (lookup∘tabulate _ a) ⟩
          tabulate {n} (λ j → f (a ,′ j)) !! b
            ≡⟨ lookup∘tabulate _ b ⟩
          f (a ,′ b)
            ≡⟨ refl ⟩
          f (Times.bwd k) ∎)

      ×c!! : {m₁ m₂ n₁ n₂ : ℕ} (p₁ : FinVec m₁ n₁) (p₂ : FinVec m₂ n₂) (k : Fin (n₁ * n₂)) →
        (p₁ ×c p₂) !! k ≡ Times.fwd (p₁ !! proj₁ (Times.bwd k) ,′ p₂ !! proj₂ (Times.bwd {n₁} k))
      ×c!! {n₁ = n₁} p₁ p₂ k =
        let a = proj₁ (Times.bwd {n₁} k) in
        let b = proj₂ (Times.bwd {n₁} k) in
        begin (
          (p₁ ×c p₂) !! k
            ≡⟨ cong₂ _!!_ (×c-equiv p₁ p₂) (sym (Times.fwd∘bwd~id {n₁} k)) ⟩
          concatV (mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂)) p₁) !! Times.fwd (a ,′ b)
            ≡⟨ concat!! a b _ ⟩
          ((mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂)) p₁) !! a) !! b
            ≡⟨ cong (λ x → x !! b) (lookup-map a _ p₁) ⟩
          mapV Times.fwd (mapV (λ x → p₁ !! a ,′ x) p₂) !! b
            ≡⟨ cong (λ x → x !! b) (sym (map-∘ Times.fwd _ p₂)) ⟩
          mapV (Times.fwd ∘ (λ x → p₁ !! a ,′ x)) p₂ !! b
            ≡⟨ lookup-map b _ p₂ ⟩
          Times.fwd (p₁ !! a ,′ p₂ !! b) ∎)

    ×c-distrib : ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → {p₁ : FinVec m₁ n₁} → {p₂ : FinVec m₂ n₂}
      → {p₃ : FinVec m₃ m₁} → {p₄ : FinVec m₄ m₂} →
        (p₁ ×c p₂) ∘̂ (p₃ ×c p₄) ≡ (p₁ ∘̂ p₃) ×c (p₂ ∘̂ p₄)
    ×c-distrib {m₁} {m₂} {m₃} {m₄} {n₁} {n₂} {p₁} {p₂} {p₃} {p₄} =
      let p₃₄ = p₃ ×c p₄ in let p₁₂ = p₁ ×c p₂ in
      let p₂₄ = p₂ ∘̂ p₄ in let p₁₃ = p₁ ∘̂ p₃ in
      let lhs = λ i → p₃₄ !! (p₁₂ !! i) in
      let zss = mapV  (λ b → mapV (λ x → b ,′ x) (p₂ ∘̂ p₄)) (p₁ ∘̂ p₃) in
      begin (
         tabulate {n₁ * n₂} (λ i → p₃₄ !! (p₁₂ !! i))
           ≡⟨ finext (λ j → cong (_!!_ p₃₄) (×c!! p₁ p₂ j)) ⟩
         tabulate {n₁ * n₂}
           (λ i → p₃₄ !! Times.fwd (p₁ !! proj₁ (Times.bwd i) ,′ p₂ !! proj₂ (Times.bwd i)))
           ≡⟨ finext (λ j → ×c!! p₃ p₄ _) ⟩
         tabulate (λ i →
           let k = Times.fwd (p₁ !! proj₁ (Times.bwd i) ,′ p₂ !! proj₂ (Times.bwd i)) in
           Times.fwd (p₃ !! proj₁ (Times.bwd k) ,′ p₄ !! proj₂ (Times.bwd k)))
           ≡⟨ finext (λ i → cong₂ (λ x y → Times.fwd (p₃ !! proj₁ x ,′ p₄ !! proj₂ y))
                     (Times.bwd∘fwd~id {m₁} {m₂} (p₁ !! proj₁ (Times.bwd i) ,′ _))
                     (Times.bwd∘fwd~id (_ ,′ p₂ !! proj₂ (Times.bwd i)))) ⟩
         tabulate (λ i → Times.fwd (p₃ !! (p₁ !! proj₁ (Times.bwd i)) ,′
                                    (p₄ !! (p₂ !! proj₂ (Times.bwd i)))))
           ≡⟨ finext (λ k → sym (lookup-2d n₁ n₂ k)) ⟩
         tabulate (λ k →
           concatV (tabulate {n₁} (λ z →
                    tabulate {n₂} (λ w →
                    Times.fwd ((p₃ !! (p₁ !! z)) ,′ (p₄ !! (p₂ !! w))))))
           !! k)

           ≡⟨ tabulate∘lookup _ ⟩
         concatV (tabulate {n₁} (λ z →
                  tabulate {n₂} (λ w →
                  Times.fwd ((p₃ !! (p₁ !! z)) ,′ (p₄ !! (p₂ !! w))))))
           ≡⟨ cong
               concatV
               (finext (λ i →
                 tabulate-∘ Times.fwd (λ w → ((p₃ !! (p₁ !! i)) ,′ (p₄ !! (p₂ !! w)))) )) ⟩
         concatV (tabulate (λ z →
                  mapV Times.fwd (tabulate (λ w → (p₃ !! (p₁ !! z)) ,′ (p₄ !! (p₂ !! w))))))
           ≡⟨ cong
               concatV
               (finext (λ i →
                 cong
                   (mapV Times.fwd)
                   (tabulate-∘ (λ x → (p₃ !! (p₁ !! i)) ,′ x) (_!!_ p₄ ∘ _!!_ p₂)))) ⟩
         concatV (tabulate (λ z → mapV Times.fwd (mapV (λ x → (p₃ !! (p₁ !! z)) ,′ x) p₂₄)))
           ≡⟨ cong concatV (tabulate-∘ _ (_!!_ p₃ ∘ _!!_ p₁)) ⟩
         concatV (mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂₄)) p₁₃)
           ≡⟨ sym (×c-equiv p₁₃ p₂₄) ⟩
         (p₁ ∘̂ p₃) ×c (p₂ ∘̂ p₄) ∎)

    -- there might be a simpler proofs of this using tablate∘lookup right
    -- at the start.

    1C×1C≡1C : ∀ {m n} → (1C {m} ×c 1C {n}) ≡ 1C {m * n}
    1C×1C≡1C {m} {n} =
      begin (
        1C {m} ×c 1C
          ≡⟨ ×c-equiv 1C 1C ⟩
        concatV (mapV (λ y → mapV Times.fwd (mapV (_,′_ y) (1C {n}))) (1C {m}))
          ≡⟨ cong (concatV {n = m}) (sym (tabulate-∘ _ id)) ⟩
        concatV {n = m} (tabulate (λ y → mapV Times.fwd (mapV (_,′_ y) (1C {n}))))
          ≡⟨ cong (concatV {n = m}) (finext (λ y → sym (map-∘ Times.fwd (λ x → y ,′ x) 1C))) ⟩
        concatV (tabulate {n = m} (λ y → mapV (Times.fwd ∘ (_,′_ y)) (1C {n})))
          ≡⟨ cong
              (concatV {m = n} {m})
              (finext (λ y → sym (tabulate-∘ (Times.fwd ∘ (_,′_ y)) id))) ⟩
        concatV (tabulate {n = m} (λ a → tabulate {n = n} (λ b → Times.fwd (a ,′ b))))
          ≡⟨ sym (tabulate∘lookup _) ⟩
        tabulate (λ k →
        concatV (tabulate {n = m} (λ a → tabulate {n = n} (λ b → Times.fwd (a ,′ b)))) !! k)
          ≡⟨ finext (λ k → lookup-2d m n k) ⟩
        tabulate (λ k → Times.fwd {m} {n} (Times.bwd k))
          ≡⟨ finext (Times.fwd∘bwd~id {m} {n}) ⟩
        1C {m * n} ∎ )

    swap*-inv : ∀ {m n} → swap⋆cauchy m n ∘̂ swap⋆cauchy n m ≡ 1C
    swap*-inv {m} {n} = ~⇒≡ (Times.swap-inv m n)

    ------------------------
    -- A few "reveal" functions, to let us peek into the representation
    reveal1C : ∀ {m} → allFin m ≡ 1C
    reveal1C = refl

    reveal0C : [] ≡ 1C {0}
    reveal0C = refl

    reveal⊎c :  ∀ {m₁ n₁ m₂ n₂} → {α : FinVec m₁ m₂} → {β : FinVec n₁ n₂} →
      α ⊎c β ≡
        tabulate (fwd ∘ inj₁ ∘ _!!_ α) ++V
        tabulate (fwd {m₁} ∘ inj₂ ∘ _!!_ β)
    reveal⊎c = refl

------------------------------------------------------------------------------
-- Commutative semiring structure

open F

_cauchy≃_ : (m n : ℕ) → Set
m cauchy≃ n = FinVec m n

id-iso : {m : ℕ} → FinVec m m
id-iso = 1C

private
  postulate sym-iso : {m n : ℕ} → FinVec m n → FinVec n m

trans-iso : {m n o : ℕ} → FinVec m n → FinVec n o → FinVec m o
trans-iso c₁ c₂ = c₂ ∘̂ c₁

cauchy≃IsEquiv : IsEquivalence {Level.zero} {Level.zero} {ℕ} _cauchy≃_
cauchy≃IsEquiv = record {
  refl = id-iso ;
  sym = sym-iso ;
  trans = trans-iso
  }

cauchyPlusIsSG : IsSemigroup {Level.zero} {Level.zero} {ℕ} _cauchy≃_ _+_
cauchyPlusIsSG = record {
  isEquivalence = cauchy≃IsEquiv ;
  assoc = λ m n o → assocl+ {m} {n} {o} ;
  ∙-cong = _⊎c_
  }

cauchyTimesIsSG : IsSemigroup {Level.zero} {Level.zero} {ℕ} _cauchy≃_ _*_
cauchyTimesIsSG = record {
  isEquivalence = cauchy≃IsEquiv ;
  assoc = λ m n o → assocl* {m} {n} {o} ;
  ∙-cong = _×c_
  }

cauchyPlusIsCM : IsCommutativeMonoid _cauchy≃_ _+_ 0
cauchyPlusIsCM = record {
  isSemigroup = cauchyPlusIsSG ;
  identityˡ = λ m → 1C ;
  comm = λ m n → swap+cauchy n m
  }

cauchyTimesIsCM : IsCommutativeMonoid _cauchy≃_ _*_ 1
cauchyTimesIsCM = record {
  isSemigroup = cauchyTimesIsSG ;
  identityˡ = λ m → uniti* {m} ;
  comm = λ m n → swap⋆cauchy n m
  }

cauchyIsCSR : IsCommutativeSemiring _cauchy≃_ _+_ _*_ 0 1
cauchyIsCSR = record {
  +-isCommutativeMonoid = cauchyPlusIsCM ;
  *-isCommutativeMonoid = cauchyTimesIsCM ;
  distribʳ = λ o m n → factor*+ {m} {n} {o} ;
  zeroˡ = λ m → 0C
  }

cauchyCSR : CommutativeSemiring Level.zero Level.zero
cauchyCSR = record {
  Carrier = ℕ ;
  _≈_ = _cauchy≃_ ;
  _+_ = _+_ ;
  _*_ = _*_ ;
  0# = 0 ;
  1# = 1 ;
  isCommutativeSemiring = cauchyIsCSR
  }

------------------------------------------------------------------------------
-- Groupoid structure

private
  postulate linv : {m n : ℕ} (c : FinVec m n) → (sym-iso c) ∘̂ c ≡ 1C
  postulate rinv : {m n : ℕ} (c : FinVec m n) → c ∘̂ (sym-iso c) ≡ 1C

G : 1Groupoid
G = record {
  set = ℕ ;
  _↝_ = _cauchy≃_ ;
  _≈_ = _≡_ ;
  id  = id-iso ;
  _∘_ = λ c₁ c₂ → trans-iso c₂ c₁ ;
  _⁻¹ = sym-iso ;
  lneutr = ∘̂-lid ;
  rneutr = ∘̂-rid ;
  assoc  = λ c₁ c₂ c₃ → sym (∘̂-assoc c₁ c₂ c₃) ;
  equiv = record {
            refl  = refl ;
            sym   = sym ;
            trans = trans
          } ;
  linv = linv ;
  rinv = rinv ;
  ∘-resp-≈ = cong₂ _∘̂_
  }

{--
-- Move to its own spot later
merge-[,] : {A B C D E : Set} → {h : A → C} → {i : B → D} → {f : C → E}
  → {g : D → E} → (x : A ⊎ B) →
    [ f , g ]′ ( map⊎ h i x ) ≡ [ (f ∘ h) , (g ∘ i) ]′ x
merge-[,] (inj₁ x) = refl
merge-[,] (inj₂ y) = refl
--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- Equivalences
------------------------------------------------------------------------

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

-- Partly based on Voevodsky's work on so-called univalent
-- foundations.

open import Equality

module Equivalence
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq as Bijection using (_↔_)
open Derived-definitions-and-properties eq
open import Equality.Decidable-UIP eq using (propositional-identity⇒set)
import Equivalence.Half-adjoint eq as HA
open import Groupoid eq
open import H-level eq as H-level
open import H-level.Closure eq
open import Injection eq using (_↣_; Injective)
open import Logical-equivalence as L-eq using (_⇔_)
open import Nat eq
open import Preimage eq as Preimage using (_⁻¹_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)
open import Surjection eq as Surjection using (_↠_)

------------------------------------------------------------------------
-- Is-equivalence

open HA public using
  (Is-equivalence;
   propositional;
   sometimes-contractible;
   respects-extensional-equality;
   function-between-contractible-types-is-equivalence;
   drop-Σ-map-id;
   inverse-drop-Σ-map-id;
   ext⁻¹-is-equivalence)

------------------------------------------------------------------------
-- _≃_

private
 module Dummy where

  -- Equivalences.

  infix 4 _≃_

  record _≃_ {a b} (A : Type a) (B : Type b) : Type (a ⊔ b) where
    constructor ⟨_,_⟩
    field
      to             : A → B
      is-equivalence : Is-equivalence to

open Dummy public using (_≃_; ⟨_,_⟩) hiding (module _≃_)

-- Some definitions with erased type arguments.

module _≃₀_ {a b} {@0 A : Type a} {@0 B : Type b} (A≃B : A ≃ B) where

  -- The forward direction of the equivalence.

  to : A → B
  to = Dummy._≃_.to A≃B

  -- The function to is an equivalence.

  is-equivalence : Is-equivalence to
  is-equivalence = Dummy._≃_.is-equivalence A≃B

  -- Equivalent types are isomorphic.

  from : B → A
  from = HA.inverse is-equivalence

  right-inverse-of : ∀ x → to (from x) ≡ x
  right-inverse-of = HA.right-inverse-of is-equivalence

  left-inverse-of : ∀ x → from (to x) ≡ x
  left-inverse-of = HA.left-inverse-of is-equivalence

  bijection : A ↔ B
  bijection = record
    { surjection = record
      { logical-equivalence = record
        { to   = to
        ; from = from
        }
      ; right-inverse-of = right-inverse-of
      }
    ; left-inverse-of = left-inverse-of
    }

module _≃_ {a b} {A : Type a} {B : Type b} (A≃B : A ≃ B) where

  open _≃₀_ A≃B public

  open _↔_ bijection public
    hiding (from; to; right-inverse-of; left-inverse-of)

  -- All preimages of an element under the equivalence are equal.

  irrelevance : ∀ y (p : to ⁻¹ y) → (from y , right-inverse-of y) ≡ p
  irrelevance = HA.irrelevance is-equivalence

  -- The two proofs left-inverse-of and right-inverse-of are
  -- related.

  left-right-lemma :
    ∀ x → cong to (left-inverse-of x) ≡ right-inverse-of (to x)
  left-right-lemma = proj₂ (proj₂ (proj₂ is-equivalence))

  right-left-lemma :
    ∀ x → cong from (right-inverse-of x) ≡ left-inverse-of (from x)
  right-left-lemma =
    proj₂ (proj₂ (proj₂ (HA.inverse-equivalence is-equivalence)))

-- Equivalences are isomorphic to pairs.

≃-as-Σ : ∀ {a b} {A : Type a} {B : Type b} →
         A ≃ B ↔ ∃ λ (f : A → B) → Is-equivalence f
≃-as-Σ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { ⟨ f , is ⟩ → f , is }
      ; from = uncurry ⟨_,_⟩
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Bijections are equivalences.
--
-- Note that the right inverse proof is preserved unchanged.

↔⇒≃ : ∀ {a b} {A : Type a} {B : Type b} → A ↔ B → A ≃ B
↔⇒≃ A↔B = record
  { to             = _↔_.to A↔B
  ; is-equivalence = HA.↔→Is-equivalenceʳ A↔B
  }

_ :
  ∀ {a b} {A : Type a} {B : Type b} {A↔B : A ↔ B} →
  _≃_.right-inverse-of (↔⇒≃ A↔B) ≡ _↔_.right-inverse-of A↔B
_ = refl _

-- A variant of the previous result.
--
-- Note that the right inverse proof is preserved unchanged.

↔→≃ :
  ∀ {a b} {A : Type a} {B : Type b} →
  (f : A → B) (g : B → A) →
  (∀ x → f (g x) ≡ x) →
  (∀ x → g (f x) ≡ x) →
  A ≃ B
↔→≃ f g f∘g g∘f = ↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = f
      ; from = g
      }
    ; right-inverse-of = f∘g
    }
  ; left-inverse-of = g∘f
  })

_ :
  ∀ {a b} {A : Type a} {B : Type b} {f : A → B} {g : B → A}
    {f-g : ∀ x → f (g x) ≡ x} {g-f : ∀ x → g (f x) ≡ x} →
  _≃_.right-inverse-of (↔→≃ f g f-g g-f) ≡ f-g
_ = refl _

-- There is a logical equivalence between A ↔ B and A ≃ B.

↔⇔≃ :
  ∀ {a b} {A : Type a} {B : Type b} →
  (A ↔ B) ⇔ (A ≃ B)
↔⇔≃ = record
  { to   = ↔⇒≃
  ; from = _≃_.bijection
  }

-- The function subst is an equivalence family.

subst-as-equivalence :
  ∀ {a p} {A : Type a} (P : A → Type p) {x y : A} (x≡y : x ≡ y) →
  P x ≃ P y
subst-as-equivalence P {y = y} x≡y = ↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = subst P x≡y
      ; from = subst P (sym x≡y)
      }
    ; right-inverse-of = subst-subst-sym P x≡y
    }
  ; left-inverse-of = λ p →
      subst P (sym x≡y) (subst P x≡y p)              ≡⟨ cong (λ eq → subst P (sym x≡y) (subst P eq _)) $ sym $ sym-sym _ ⟩
      subst P (sym x≡y) (subst P (sym (sym x≡y)) p)  ≡⟨ subst-subst-sym P _ _ ⟩∎
      p                                              ∎
  })

abstract

  subst-is-equivalence :
    ∀ {a p} {A : Type a} (P : A → Type p) {x y : A} (x≡y : x ≡ y) →
    Is-equivalence (subst P x≡y)
  subst-is-equivalence P x≡y =
    _≃_.is-equivalence (subst-as-equivalence P x≡y)

------------------------------------------------------------------------
-- Equivalence

-- Equivalences are equivalence relations.

id : ∀ {a} {A : Type a} → A ≃ A
id = ⟨ P.id , HA.id-equivalence ⟩

inverse : ∀ {a b} {A : Type a} {B : Type b} → A ≃ B → B ≃ A
inverse A≃B =
  ⟨ HA.inverse             (_≃_.is-equivalence A≃B)
  , HA.inverse-equivalence (_≃_.is-equivalence A≃B)
  ⟩

infixr 9 _∘_

_∘_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
      B ≃ C → A ≃ B → A ≃ C
f ∘ g =
  ⟨ _≃_.to f ⊚ _≃_.to g
  , HA.composition-equivalence
      (_≃_.is-equivalence f)
      (_≃_.is-equivalence g)
  ⟩

-- Equational reasoning combinators.

infix  -1 finally-≃
infixr -2 step-≃

-- For an explanation of why step-≃ is defined in this way, see
-- Equality.step-≡.

step-≃ : ∀ {a b c} (A : Type a) {B : Type b} {C : Type c} →
         B ≃ C → A ≃ B → A ≃ C
step-≃ _ = _∘_

syntax step-≃ A B≃C A≃B = A ≃⟨ A≃B ⟩ B≃C

finally-≃ : ∀ {a b} (A : Type a) (B : Type b) → A ≃ B → A ≃ B
finally-≃ _ _ A≃B = A≃B

syntax finally-≃ A B A≃B = A ≃⟨ A≃B ⟩□ B □

-- Some simplification lemmas.

right-inverse-of-id :
  ∀ {a} {A : Type a} {x : A} →
  _≃_.right-inverse-of id x ≡ refl x
right-inverse-of-id {x = x} = refl (refl x)

left-inverse-of-id :
  ∀ {a} {A : Type a} {x : A} →
  _≃_.left-inverse-of id x ≡ refl x
left-inverse-of-id {x = x} = refl (refl x)

right-inverse-of∘inverse :
  ∀ {a b} {A : Type a} {B : Type b} →
  ∀ (A≃B : A ≃ B) {x} →
  _≃_.right-inverse-of (inverse A≃B) x ≡
  _≃_.left-inverse-of A≃B x
right-inverse-of∘inverse _ = refl _

left-inverse-of∘inverse :
  ∀ {a b} {A : Type a} {B : Type b} →
  ∀ (A≃B : A ≃ B) {x} →
  _≃_.left-inverse-of (inverse A≃B) x ≡
  _≃_.right-inverse-of A≃B x
left-inverse-of∘inverse _ = refl _

------------------------------------------------------------------------
-- One can replace either of the functions with an extensionally equal
-- function

with-other-function :
  ∀ {a b} {A : Type a} {B : Type b}
  (A≃B : A ≃ B) (f : A → B) →
  (∀ x → _≃_.to A≃B x ≡ f x) →
  A ≃ B
with-other-function ⟨ g , is-equivalence ⟩ f g≡f =
  ⟨ f , respects-extensional-equality g≡f is-equivalence ⟩

with-other-inverse :
  ∀ {a b} {A : Type a} {B : Type b}
  (A≃B : A ≃ B) (f : B → A) →
  (∀ x → _≃_.from A≃B x ≡ f x) →
  A ≃ B
with-other-inverse A≃B f from≡f =
  inverse $ with-other-function (inverse A≃B) f from≡f

private

  -- The two functions above compute in the right way.

  to∘with-other-function :
    ∀ {a b} {A : Type a} {B : Type b}
    (A≃B : A ≃ B) (f : A → B)
    (to≡f : ∀ x → _≃_.to A≃B x ≡ f x) →
    _≃_.to (with-other-function A≃B f to≡f) ≡ f
  to∘with-other-function _ _ _ = refl _

  from∘with-other-function :
    ∀ {a b} {A : Type a} {B : Type b}
    (A≃B : A ≃ B) (f : A → B)
    (to≡f : ∀ x → _≃_.to A≃B x ≡ f x) →
    _≃_.from (with-other-function A≃B f to≡f) ≡ _≃_.from A≃B
  from∘with-other-function _ _ _ = refl _

  to∘with-other-inverse :
    ∀ {a b} {A : Type a} {B : Type b}
    (A≃B : A ≃ B) (g : B → A)
    (from≡g : ∀ x → _≃_.from A≃B x ≡ g x) →
    _≃_.to (with-other-inverse A≃B g from≡g) ≡ _≃_.to A≃B
  to∘with-other-inverse _ _ _ = refl _

  from∘with-other-inverse :
    ∀ {a b} {A : Type a} {B : Type b}
    (A≃B : A ≃ B) (g : B → A)
    (from≡g : ∀ x → _≃_.from A≃B x ≡ g x) →
    _≃_.from (with-other-inverse A≃B g from≡g) ≡ g
  from∘with-other-inverse _ _ _ = refl _

------------------------------------------------------------------------
-- The two-out-of-three property

-- If two out of three of f, g and g ∘ f are equivalences, then the
-- third one is also an equivalence.

record Two-out-of-three
         {a b c} {A : Type a} {B : Type b} {C : Type c}
         (f : A → B) (g : B → C) : Type (a ⊔ b ⊔ c) where
  field
    f-g   : Is-equivalence f → Is-equivalence g → Is-equivalence (g ⊚ f)
    g-g∘f : Is-equivalence g → Is-equivalence (g ⊚ f) → Is-equivalence f
    g∘f-f : Is-equivalence (g ⊚ f) → Is-equivalence f → Is-equivalence g

two-out-of-three :
  ∀ {a b c} {A : Type a} {B : Type b} {C : Type c}
  (f : A → B) (g : B → C) → Two-out-of-three f g
two-out-of-three f g = record
  { f-g   = λ f-eq g-eq →
              _≃_.is-equivalence (⟨ g , g-eq ⟩ ∘ ⟨ f , f-eq ⟩)
  ; g-g∘f = λ g-eq g∘f-eq →
              respects-extensional-equality
                (λ x → let g⁻¹ = _≃_.from ⟨ g , g-eq ⟩ in
                   g⁻¹ (g (f x))  ≡⟨ _≃_.left-inverse-of ⟨ g , g-eq ⟩ (f x) ⟩∎
                   f x            ∎)
                (_≃_.is-equivalence
                   (inverse ⟨ g , g-eq ⟩ ∘ ⟨ _ , g∘f-eq ⟩))
  ; g∘f-f = λ g∘f-eq f-eq →
              respects-extensional-equality
                (λ x → let f⁻¹ = _≃_.from ⟨ f , f-eq ⟩ in
                   g (f (f⁻¹ x))  ≡⟨ cong g (_≃_.right-inverse-of ⟨ f , f-eq ⟩ x) ⟩∎
                   g x            ∎)
                (_≃_.is-equivalence
                   (⟨ _ , g∘f-eq ⟩ ∘ inverse ⟨ f , f-eq ⟩))
  }

------------------------------------------------------------------------
-- Extensionality

-- f ≡ g and ∀ x → f x ≡ g x are isomorphic (assuming extensionality).

extensionality-isomorphism :
  ∀ {a b} →
  Extensionality a b →
  {A : Type a} {B : A → Type b} {f g : (x : A) → B x} →
  (∀ x → f x ≡ g x) ≃ (f ≡ g)
extensionality-isomorphism ext =
  inverse ⟨ _ , ext⁻¹-is-equivalence (apply-ext ext) ⟩

-- Note that the isomorphism gives us a really well-behaved notion of
-- extensionality.

good-ext : ∀ {a b} → Extensionality a b → Extensionality a b
apply-ext (good-ext ext) = _≃_.to (extensionality-isomorphism ext)

abstract

  good-ext-is-equivalence :
    ∀ {a b} (ext : Extensionality a b) →
    {A : Type a} {B : A → Type b} {f g : (x : A) → B x} →
    Is-equivalence {A = ∀ x → f x ≡ g x} (apply-ext (good-ext ext))
  good-ext-is-equivalence ext =
    _≃_.is-equivalence (extensionality-isomorphism ext)

  good-ext-refl :
    ∀ {a b} (ext : Extensionality a b)
    {A : Type a} {B : A → Type b} (f : (x : A) → B x) →
    apply-ext (good-ext ext) (λ x → refl (f x)) ≡ refl f
  good-ext-refl ext f =
    _≃_.to (extensionality-isomorphism ext) (λ x → refl (f x))  ≡⟨ cong (_≃_.to (extensionality-isomorphism ext)) $ sym $
                                                                        apply-ext ext (λ _ → ext⁻¹-refl f) ⟩
    _≃_.to (extensionality-isomorphism ext) (ext⁻¹ (refl f))    ≡⟨ _≃_.right-inverse-of (extensionality-isomorphism ext) _ ⟩∎
    refl f                                                      ∎

  good-ext-const :
    ∀ {a b} (ext : Extensionality a b)
    {A : Type a} {B : Type b} {x y : B}
    (x≡y : x ≡ y) →
    apply-ext (good-ext ext) (const {B = A} x≡y) ≡
    cong const x≡y
  good-ext-const ext x≡y =
    apply-ext (good-ext ext) (const x≡y)                        ≡⟨ cong (apply-ext (good-ext ext) ⊚ const) $ cong-id _ ⟩
    apply-ext (good-ext ext) (const (cong P.id x≡y))            ≡⟨⟩
    apply-ext (good-ext ext) (λ z → cong ((_$ z) ⊚ const) x≡y)  ≡⟨ cong (apply-ext (good-ext ext)) $
                                                                   apply-ext (good-ext ext) (λ _ → sym $ cong-∘ _ _ _) ⟩
    apply-ext (good-ext ext) (ext⁻¹ (cong const x≡y))           ≡⟨ _≃_.right-inverse-of (extensionality-isomorphism ext) _ ⟩∎
    cong const x≡y                                              ∎

  cong-good-ext :
    ∀ {a b} (ext : Extensionality a b)
    {A : Type a} {B : A → Type b} {f g : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) {x} →
    cong (_$ x) (apply-ext (good-ext ext) f≡g) ≡ f≡g x
  cong-good-ext ext f≡g {x} =
    cong (_$ x) (apply-ext (good-ext ext) f≡g)  ≡⟨⟩
    ext⁻¹ (apply-ext (good-ext ext) f≡g) x      ≡⟨ cong (_$ x) $ _≃_.left-inverse-of (extensionality-isomorphism ext) f≡g ⟩∎
    f≡g x                                       ∎

  good-ext-cong :
    ∀ {a b c} (ext : Extensionality b c)
    {A : Type a} {B : Type b} {C : B → Type c}
    {f : A → (x : B) → C x} {x y : A} {x≡y : x ≡ y} →
    apply-ext (good-ext ext) (λ z → cong (flip f z) x≡y) ≡
    cong f x≡y
  good-ext-cong ext {f = f} {x≡y = x≡y} =
    apply-ext (good-ext ext) (λ z → cong (flip f z) x≡y)       ≡⟨ (cong (apply-ext (good-ext ext)) $ apply-ext ext λ _ → sym $ cong-∘ _ _ _) ⟩
    apply-ext (good-ext ext) (λ z → cong (_$ z) (cong f x≡y))  ≡⟨⟩
    apply-ext (good-ext ext) (ext⁻¹ (cong f x≡y))              ≡⟨ _≃_.right-inverse-of (extensionality-isomorphism ext) _ ⟩∎
    cong f x≡y                                                 ∎

  subst-good-ext :
    ∀ {a b p} (ext : Extensionality a b)
    {A : Type a} {B : A → Type b} {f g : (x : A) → B x} {x}
    (P : B x → Type p) {p}
    (f≡g : ∀ x → f x ≡ g x) →
    subst (λ f → P (f x)) (apply-ext (good-ext ext) f≡g) p ≡
    subst P (f≡g x) p
  subst-good-ext ext {f = f} {g} {x} P {p} f≡g =
    subst (λ f → P (f x)) (apply-ext (good-ext ext) f≡g) p  ≡⟨ subst-∘ P (_$ x) _ ⟩
    subst P (cong (_$ x) (apply-ext (good-ext ext) f≡g)) p  ≡⟨ cong (λ eq → subst P eq p) (cong-good-ext ext f≡g) ⟩∎
    subst P (f≡g x) p                                       ∎

  elim-good-ext :
    ∀ {a b p}
    (ext : Extensionality a b)
    {A : Type a} {B : A → Type b} {x : A}
    (P : B x → B x → Type p)
    (p : (y : B x) → P y y)
    {f g : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) →
    elim (λ {f g} _ → P (f x) (g x)) (p ⊚ (_$ x))
         (apply-ext (good-ext ext) f≡g) ≡
    elim (λ {x y} _ → P x y) p (f≡g x)
  elim-good-ext ext {x = x} P p f≡g =
    elim (λ {f g} _ → P (f x) (g x)) (p ⊚ (_$ x)) (apply-ext (good-ext ext) f≡g)  ≡⟨ sym $ elim-cong _ _ _ ⟩
    elim (λ {x y} _ → P x y) p (cong (_$ x) (apply-ext (good-ext ext) f≡g))       ≡⟨ cong (elim (λ {x y} _ → P x y) p) (cong-good-ext ext f≡g) ⟩
    elim (λ {x y} _ → P x y) p (f≡g x)                                            ∎

  -- I based the statements of the following three lemmas on code in
  -- the Lean Homotopy Type Theory Library with Jakob von Raumer and
  -- Floris van Doorn listed as authors. The file was claimed to have
  -- been ported from the Coq HoTT library. (The third lemma has later
  -- been generalised.)

  good-ext-sym :
    ∀ {a b} (ext : Extensionality a b)
    {A : Type a} {B : A → Type b} {f g : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) →
    apply-ext (good-ext ext) (sym ⊚ f≡g) ≡
    sym (apply-ext (good-ext ext) f≡g)
  good-ext-sym ext f≡g =
    apply-ext (good-ext ext) (sym ⊚ f≡g)                 ≡⟨ cong (apply-ext (good-ext ext) ⊚ (sym ⊚_)) $ sym $
                                                              _≃_.left-inverse-of (extensionality-isomorphism ext) _ ⟩
    apply-ext (good-ext ext)
      (sym ⊚ ext⁻¹ (apply-ext (good-ext ext) f≡g))       ≡⟨⟩

    apply-ext (good-ext ext) (λ x →
      sym $ cong (_$ x) (apply-ext (good-ext ext) f≡g))  ≡⟨ cong (apply-ext (good-ext ext)) $
                                                              apply-ext ext (λ _ → sym $ cong-sym _ _) ⟩
    apply-ext (good-ext ext) (λ x →
      cong (_$ x) (sym $ apply-ext (good-ext ext) f≡g))  ≡⟨⟩

    apply-ext (good-ext ext)
      (ext⁻¹ (sym $ apply-ext (good-ext ext) f≡g))       ≡⟨ _≃_.right-inverse-of (extensionality-isomorphism ext) _ ⟩∎

    sym (apply-ext (good-ext ext) f≡g)                   ∎

  good-ext-trans :
    ∀ {a b} (ext : Extensionality a b)
    {A : Type a} {B : A → Type b} {f g h : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) (g≡h : ∀ x → g x ≡ h x) →
    apply-ext (good-ext ext) (λ x → trans (f≡g x) (g≡h x)) ≡
    trans (apply-ext (good-ext ext) f≡g) (apply-ext (good-ext ext) g≡h)
  good-ext-trans ext f≡g g≡h =
    apply-ext (good-ext ext) (λ x → trans (f≡g x) (g≡h x))  ≡⟨ sym $ cong₂ (λ f g → apply-ext (good-ext ext) (λ x → trans (f x) (g x)))
                                                                           (_≃_.left-inverse-of (extensionality-isomorphism ext) _)
                                                                           (_≃_.left-inverse-of (extensionality-isomorphism ext) _) ⟩
    apply-ext (good-ext ext) (λ x →
      trans (ext⁻¹ (apply-ext (good-ext ext) f≡g) x)
            (ext⁻¹ (apply-ext (good-ext ext) g≡h) x))       ≡⟨⟩

    apply-ext (good-ext ext) (λ x →
      trans (cong (_$ x) (apply-ext (good-ext ext) f≡g))
            (cong (_$ x) (apply-ext (good-ext ext) g≡h)))   ≡⟨ cong (apply-ext (good-ext ext)) $ apply-ext ext (λ _ → sym $
                                                                 cong-trans _ _ _) ⟩
    apply-ext (good-ext ext) (λ x →
      cong (_$ x) (trans (apply-ext (good-ext ext) f≡g)
                         (apply-ext (good-ext ext) g≡h)))   ≡⟨⟩

    apply-ext (good-ext ext)
      (ext⁻¹ (trans (apply-ext (good-ext ext) f≡g)
                    (apply-ext (good-ext ext) g≡h)))        ≡⟨ _≃_.right-inverse-of (extensionality-isomorphism ext) _ ⟩∎

    trans (apply-ext (good-ext ext) f≡g)
          (apply-ext (good-ext ext) g≡h)                    ∎

  cong-post-∘-good-ext :
    ∀ {a b c} {A : Type a} {B : A → Type b} {C : A → Type c}
      {f g : (x : A) → B x} {h : ∀ {x} → B x → C x}
    (ext₁ : Extensionality a b)
    (ext₂ : Extensionality a c)
    (f≡g : ∀ x → f x ≡ g x) →
    cong (h ⊚_) (apply-ext (good-ext ext₁) f≡g) ≡
    apply-ext (good-ext ext₂) (cong h ⊚ f≡g)
  cong-post-∘-good-ext {f = f} {g} {h} ext₁ ext₂ f≡g =
    cong (h ⊚_) (apply-ext (good-ext ext₁) f≡g)                   ≡⟨ sym $ _≃_.right-inverse-of (extensionality-isomorphism ext₂) _ ⟩

    apply-ext (good-ext ext₂)
      (ext⁻¹ (cong (h ⊚_) (apply-ext (good-ext ext₁) f≡g)))       ≡⟨⟩

    apply-ext (good-ext ext₂) (λ x →
      cong (_$ x) (cong (h ⊚_) (apply-ext (good-ext ext₁) f≡g)))  ≡⟨ cong (apply-ext (good-ext ext₂)) $ apply-ext ext₂ (λ _ →
                                                                       cong-∘ _ _ _) ⟩
    apply-ext (good-ext ext₂) (λ x →
      cong (λ f → h (f x)) (apply-ext (good-ext ext₁) f≡g))       ≡⟨ cong (apply-ext (good-ext ext₂)) $ apply-ext ext₂ (λ _ → sym $
                                                                       cong-∘ _ _ _) ⟩
    apply-ext (good-ext ext₂) (λ x →
      cong h (cong (_$ x) (apply-ext (good-ext ext₁) f≡g)))       ≡⟨⟩

    apply-ext (good-ext ext₂)
      (cong h ⊚ ext⁻¹ (apply-ext (good-ext ext₁) f≡g))            ≡⟨ cong (apply-ext (good-ext ext₂) ⊚ (cong h ⊚_)) $
                                                                       _≃_.left-inverse-of (extensionality-isomorphism ext₁) _ ⟩∎
    apply-ext (good-ext ext₂) (cong h ⊚ f≡g)                      ∎

  cong-pre-∘-good-ext :
    ∀ {a b c} {A : Type a} {B : Type b} {C : B → Type c}
      {f g : (x : B) → C x} {h : A → B}
    (ext₁ : Extensionality a c)
    (ext₂ : Extensionality b c)
    (f≡g : ∀ x → f x ≡ g x) →
    cong (_⊚ h) (apply-ext (good-ext ext₂) f≡g) ≡ apply-ext (good-ext ext₁) (f≡g ⊚ h)
  cong-pre-∘-good-ext {f = f} {g} {h} ext₁ ext₂ f≡g =
    cong (_⊚ h) (apply-ext (good-ext ext₂) f≡g)                   ≡⟨ sym $ _≃_.right-inverse-of (extensionality-isomorphism ext₁) _ ⟩

    apply-ext (good-ext ext₁)
      (ext⁻¹ (cong (_⊚ h) (apply-ext (good-ext ext₂) f≡g)))       ≡⟨⟩

    apply-ext (good-ext ext₁) (λ x →
      cong (_$ x) (cong (_⊚ h) (apply-ext (good-ext ext₂) f≡g)))  ≡⟨ cong (apply-ext (good-ext ext₁)) $ apply-ext ext₁ (λ _ →
                                                                       cong-∘ _ _ _) ⟩
    apply-ext (good-ext ext₁) (λ x →
      cong (_$ h x) (apply-ext (good-ext ext₂) f≡g))              ≡⟨ cong (apply-ext (good-ext ext₁)) $ apply-ext ext₁ (λ _ →
                                                                       cong-good-ext ext₂ _) ⟩
    apply-ext (good-ext ext₁) (λ x → f≡g (h x))                   ≡⟨⟩

    apply-ext (good-ext ext₁) (f≡g ⊚ h)                           ∎

  cong-∘-good-ext :
    ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} {f g : B → C}
    (ext₁ : Extensionality b c)
    (ext₂ : Extensionality (a ⊔ b) (a ⊔ c))
    (ext₃ : Extensionality a c)
    (f≡g : ∀ x → f x ≡ g x) →
    cong {B = (A → B) → (A → C)}
         (λ f → f ⊚_) (apply-ext (good-ext ext₁) f≡g) ≡
    apply-ext (good-ext ext₂) λ h → apply-ext (good-ext ext₃) λ x →
    f≡g (h x)
  cong-∘-good-ext ext₁ ext₂ ext₃ f≡g =
    cong (λ f → f ⊚_) (apply-ext (good-ext ext₁) f≡g)                  ≡⟨ sym $ _≃_.right-inverse-of (extensionality-isomorphism ext₂) _ ⟩

    (apply-ext (good-ext ext₂) λ h →
     cong (_$ h) (cong (λ f → f ⊚_) (apply-ext (good-ext ext₁) f≡g)))  ≡⟨ (cong (apply-ext (good-ext ext₂)) $ apply-ext ext₂ λ _ →
                                                                           cong-∘ _ _ _) ⟩

    (apply-ext (good-ext ext₂) λ h →
     cong (_⊚ h) (apply-ext (good-ext ext₁) f≡g))                      ≡⟨ (cong (apply-ext (good-ext ext₂)) $ apply-ext ext₂ λ _ → cong-pre-∘-good-ext ext₃ ext₁ _) ⟩∎

    (apply-ext (good-ext ext₂) λ h → apply-ext (good-ext ext₃) λ x →
     f≡g (h x))                                                        ∎

------------------------------------------------------------------------
-- Groupoid

abstract

  -- Two proofs of equivalence are equal if the function components
  -- are equal (assuming extensionality).
  --
  -- See also Function-universe.≃-to-≡↔≡.

  lift-equality :
    ∀ {a b} → Extensionality (a ⊔ b) (a ⊔ b) →
    {A : Type a} {B : Type b} {p q : A ≃ B} →
    _≃_.to p ≡ _≃_.to q → p ≡ q
  lift-equality {a} {b} ext {p = ⟨ f , f-eq ⟩} {q = ⟨ g , g-eq ⟩} f≡g =
    elim (λ {f g} f≡g → ∀ f-eq g-eq → ⟨ f , f-eq ⟩ ≡ ⟨ g , g-eq ⟩)
         (λ f f-eq g-eq →
            cong (⟨_,_⟩ f) (propositional ext f f-eq g-eq))
         f≡g f-eq g-eq

  -- A computation rule for lift-equality.

  lift-equality-refl :
    ∀ {a b} {A : Type a} {B : Type b}
      {p : A ≃ B} {q : Is-equivalence (_≃_.to p)}
    (ext : Extensionality (a ⊔ b) (a ⊔ b)) →
    lift-equality ext (refl (_≃_.to p)) ≡
    cong ⟨ _≃_.to p ,_⟩
      (propositional ext (_≃_.to p) (_≃_.is-equivalence p) q)
  lift-equality-refl ext =
    cong (λ f → f _ _) $
    elim-refl
      (λ {f g} f≡g → ∀ f-eq g-eq → ⟨ f , f-eq ⟩ ≡ ⟨ g , g-eq ⟩)
      _

  -- Two proofs of equivalence are equal if the /inverses/ of the
  -- function components are equal (assuming extensionality).
  --
  -- See also Function-universe.≃-from-≡↔≡.

  lift-equality-inverse :
    ∀ {a b} → Extensionality (a ⊔ b) (a ⊔ b) →
    {A : Type a} {B : Type b} {p q : A ≃ B} →
    _≃_.from p ≡ _≃_.from q → p ≡ q
  lift-equality-inverse ext {p = p} {q = q} f≡g =
    p                    ≡⟨ lift-equality ext (refl _) ⟩
    inverse (inverse p)  ≡⟨ cong inverse $
                            lift-equality ext {p = inverse p} {q = inverse q} f≡g ⟩
    inverse (inverse q)  ≡⟨ lift-equality ext (refl _) ⟩∎
    q                    ∎

  -- An equality rearrangement lemma.

  cong-to-from-lift-equality :
    ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} {eq₁ eq₂ : A ≃ B}
      {f : (A → B) → (B → A) → C}
      {eq : _≃_.to eq₁ ≡ _≃_.to eq₂} →
    (ext₁ : Extensionality (a ⊔ b) (a ⊔ b))
    (ext₂ : Extensionality b a) →
    cong (λ eq → f (_≃_.to eq) (_≃_.from eq))
      (lift-equality ext₁ {p = eq₁} {q = eq₂} eq) ≡
    cong₂ f
      eq
      (apply-ext (good-ext ext₂) λ b →

       _≃_.from eq₁ b                              ≡⟨ cong (_≃_.from eq₁) $ sym $ _≃_.right-inverse-of eq₂ b ⟩
       _≃_.from eq₁ (_≃_.to eq₂ (_≃_.from eq₂ b))  ≡⟨ cong (_≃_.from eq₁) $ cong (_$ _≃_.from eq₂ b) $ sym eq ⟩
       _≃_.from eq₁ (_≃_.to eq₁ (_≃_.from eq₂ b))  ≡⟨ _≃_.left-inverse-of eq₁ (_≃_.from eq₂ b) ⟩∎
       _≃_.from eq₂ b                              ∎)
  cong-to-from-lift-equality {eq₂ = eq₂} {f = f} {eq = eq} ext₁ ext₂ =
    elim₁
      (λ {g} eq →
         (is-eq : Is-equivalence g) →
         let eq₁ = ⟨ g , is-eq ⟩ in
         cong (λ eq → f (_≃_.to eq) (_≃_.from eq))
           (lift-equality ext₁ {p = eq₁} {q = eq₂} eq) ≡
         cong₂ f
           eq
           (apply-ext (good-ext ext₂) λ b →
            trans (cong (_≃_.from eq₁) $ sym $
                   _≃_.right-inverse-of eq₂ b) $
            trans (cong (_≃_.from eq₁) $
                   cong (_$ _≃_.from eq₂ b) $ sym eq) $
            _≃_.left-inverse-of eq₁ (_≃_.from eq₂ b)))
      (λ is-eq →
         let eq₁ = ⟨ _≃_.to eq₂ , is-eq ⟩ in

         cong (λ eq → f (_≃_.to eq) (_≃_.from eq))
           (lift-equality ext₁ (refl _))                                   ≡⟨ cong (cong _) $ lift-equality-refl ext₁ ⟩

         cong (λ eq → f (_≃_.to eq) (_≃_.from eq))
           (cong ⟨ _≃_.to eq₂ ,_⟩
              (propositional ext₁ (_≃_.to eq₂) _ _))                       ≡⟨ cong-∘ _ _ _ ⟩

         cong (λ is-eq → f (_≃_.to eq₂) (_≃_.from ⟨ _ , is-eq ⟩))
           (propositional ext₁ (_≃_.to eq₂) _ _)                           ≡⟨ sym $ cong-∘ _ _ _ ⟩

         cong (f (_≃_.to eq₂))
           (cong (λ is-eq → _≃_.from ⟨ _ , is-eq ⟩)
              (propositional ext₁ (_≃_.to eq₂) _ _))                       ≡⟨ cong (cong _) $
                                                                              elim₁
                                                                                (λ {is-eq} eq →
                                                                                let eq₁ = ⟨ _≃_.to eq₂ , is-eq ⟩ in
                                                                                cong (λ is-eq → _≃_.from ⟨ _ , is-eq ⟩) eq ≡
                                                                                apply-ext (good-ext ext₂) λ b →
                                                                                trans (cong (_≃_.from eq₁) $ sym $
                                                                                _≃_.right-inverse-of eq₂ b) $
                                                                                _≃_.left-inverse-of eq₁ (_≃_.from eq₂ b))
                                                                                (
             cong (λ is-eq → _≃_.from ⟨ _ , is-eq ⟩) (refl _)                    ≡⟨ cong-refl _ ⟩

             refl _                                                              ≡⟨ sym (good-ext-refl ext₂ _) ⟩

             (apply-ext (good-ext ext₂) λ _ → refl _)                            ≡⟨ (cong (apply-ext (good-ext ext₂)) $ apply-ext ext₂ λ _ → sym $
                                                                                trans-symˡ _) ⟩
             (apply-ext (good-ext ext₂) λ b →
              trans (sym $ cong (_≃_.from eq₂) $
                     _≃_.right-inverse-of eq₂ b) $
              cong (_≃_.from eq₂) $ _≃_.right-inverse-of eq₂ b)                  ≡⟨ (cong (apply-ext (good-ext ext₂)) $ apply-ext ext₂ λ _ →
                                                                                cong₂ trans
                                                                                (sym $ cong-sym _ _)
                                                                                (_≃_.right-left-lemma eq₂ _)) ⟩∎
             (apply-ext (good-ext ext₂) λ b →
              trans (cong (_≃_.from eq₂) $ sym $
                     _≃_.right-inverse-of eq₂ b) $
              _≃_.left-inverse-of eq₂ (_≃_.from eq₂ b))                          ∎)
                                                                                (propositional ext₁ (_≃_.to eq₂) _ _) ⟩
         cong (f (_≃_.to eq₂))
           (apply-ext (good-ext ext₂) λ b →
            trans (cong (_≃_.from eq₁) $ sym $
                   _≃_.right-inverse-of eq₂ b) $
            _≃_.left-inverse-of eq₁ (_≃_.from eq₂ b))                      ≡⟨ (cong (cong _) $
                                                                               cong (apply-ext (good-ext ext₂)) $ apply-ext ext₂ λ _ →
                                                                               cong (trans _) $ sym $
                                                                               trans (cong (flip trans _) $
                                                                                trans (cong (cong _) $
                                                                                trans (cong (cong _) sym-refl) $
                                                                                cong-refl _) $
                                                                                cong-refl _) $
                                                                               trans-reflˡ _) ⟩
         cong (f (_≃_.to eq₂))
           (apply-ext (good-ext ext₂) λ b →
            trans (cong (_≃_.from eq₁) $ sym $
                   _≃_.right-inverse-of eq₂ b) $
            trans (cong (_≃_.from eq₁) $ cong (_$ _≃_.from eq₂ b) $ sym $
                   refl (_≃_.to eq₂)) $
            _≃_.left-inverse-of eq₁ (_≃_.from eq₂ b))                      ≡⟨ sym $ cong₂-reflˡ _ ⟩∎

         cong₂ f
           (refl _)
           (apply-ext (good-ext ext₂) λ b →
            trans (cong (_≃_.from eq₁) $ sym $
                   _≃_.right-inverse-of eq₂ b) $
            trans (cong (_≃_.from eq₁) $ cong (_$ _≃_.from eq₂ b) $ sym $
                   refl (_≃_.to eq₂)) $
            _≃_.left-inverse-of eq₁ (_≃_.from eq₂ b))                      ∎)
      eq
      _

-- _≃_ comes with a groupoid structure (assuming extensionality).

groupoid : ∀ {ℓ} → Extensionality ℓ ℓ → Groupoid (lsuc ℓ) ℓ
groupoid {ℓ} ext = record
  { Object         = Type ℓ
  ; _∼_            = _≃_
  ; id             = id
  ; _∘_            = _∘_
  ; _⁻¹            = inverse
  ; left-identity  = left-identity
  ; right-identity = right-identity
  ; assoc          = assoc
  ; left-inverse   = left-inverse
  ; right-inverse  = right-inverse
  }
  where
  abstract
    left-identity : {X Y : Type ℓ} (p : X ≃ Y) → id ∘ p ≡ p
    left-identity _ = lift-equality ext (refl _)

    right-identity : {X Y : Type ℓ} (p : X ≃ Y) → p ∘ id ≡ p
    right-identity _ = lift-equality ext (refl _)

    assoc : {W X Y Z : Type ℓ} (p : Y ≃ Z) (q : X ≃ Y) (r : W ≃ X) →
            p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r
    assoc _ _ _ = lift-equality ext (refl _)

    left-inverse : {X Y : Type ℓ} (p : X ≃ Y) → inverse p ∘ p ≡ id
    left-inverse p =
      lift-equality ext (apply-ext ext $ _≃_.left-inverse-of p)

    right-inverse : {X Y : Type ℓ} (p : X ≃ Y) → p ∘ inverse p ≡ id
    right-inverse p =
      lift-equality ext (apply-ext ext $ _≃_.right-inverse-of p)

-- Inverse is involutive (assuming extensionality).
--
-- This property is more general than
-- Groupoid.involutive (groupoid …), because A and B do not have to
-- have the same size.

inverse-involutive :
  ∀ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  (p : A ≃ B) →
  inverse (inverse p) ≡ p
inverse-involutive ext p = lift-equality ext (refl _)

-- Inverse is a logical equivalence.

inverse-logical-equivalence :
  ∀ {a b} {A : Type a} {B : Type b} →
  A ≃ B ⇔ B ≃ A
inverse-logical-equivalence = record
  { to   = inverse
  ; from = inverse
  }

-- Inverse is an isomorphism (assuming extensionality).
--
-- This property is more general than
-- Groupoid.⁻¹-bijection (groupoid …), because A and B do not have to
-- have the same size.

inverse-isomorphism :
  ∀ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  A ≃ B ↔ B ≃ A
inverse-isomorphism ext = record
  { surjection = record
    { logical-equivalence = inverse-logical-equivalence
    ; right-inverse-of    = inverse-involutive ext
    }
  ; left-inverse-of = inverse-involutive ext
  }

------------------------------------------------------------------------
-- A surjection from A ↔ B to A ≃ B, and related results

private
 abstract

  -- ↔⇒≃ is a left inverse of _≃_.bijection (assuming extensionality).

  ↔⇒≃-left-inverse :
    ∀ {a b} {A : Type a} {B : Type b} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    (A≃B : A ≃ B) →
    ↔⇒≃ (_≃_.bijection A≃B) ≡ A≃B
  ↔⇒≃-left-inverse ext _ = lift-equality ext (refl _)

  -- When sets are used ↔⇒≃ is a right inverse of _≃_.bijection
  -- (assuming extensionality).

  ↔⇒≃-right-inverse :
    ∀ {a b} {A : Type a} {B : Type b} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    Is-set A → (A↔B : A ↔ B) →
    _≃_.bijection (↔⇒≃ A↔B) ≡ A↔B
  ↔⇒≃-right-inverse {a} {b} {B = B} ext A-set A↔B =
    cong₂ (λ l r → record
             { surjection = record
               { logical-equivalence = _↔_.logical-equivalence A↔B
               ; right-inverse-of    = r
               }
             ; left-inverse-of = l
             })
          (apply-ext (lower-extensionality b b ext) λ _ → A-set _ _)
          (apply-ext (lower-extensionality a a ext) λ _ → B-set _ _)
    where
    B-set : Is-set B
    B-set = respects-surjection (_↔_.surjection A↔B) 2 A-set

-- There is a surjection from A ↔ B to A ≃ B (assuming
-- extensionality).

↔↠≃ :
  ∀ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  (A ↔ B) ↠ (A ≃ B)
↔↠≃ ext = record
  { logical-equivalence = ↔⇔≃
  ; right-inverse-of    = ↔⇒≃-left-inverse ext
  }

-- When A is a set A ↔ B and A ≃ B are isomorphic (assuming
-- extensionality).

↔↔≃ :
  ∀ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-set A → (A ↔ B) ↔ (A ≃ B)
↔↔≃ ext A-set = record
  { surjection      = ↔↠≃ ext
  ; left-inverse-of = ↔⇒≃-right-inverse ext A-set
  }

-- When B is a set A ↔ B and A ≃ B are isomorphic (assuming
-- extensionality).

↔↔≃′ :
  ∀ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-set B → (A ↔ B) ↔ (A ≃ B)
↔↔≃′ ext B-set = record
  { surjection      = ↔↠≃ ext
  ; left-inverse-of = λ A↔B →
      ↔⇒≃-right-inverse
        ext
        (H-level.respects-surjection
           (_↔_.surjection $ Bijection.inverse A↔B) 2 B-set)
        A↔B
  }

-- For propositional types there is a split surjection from
-- equivalence to logical equivalence.

≃↠⇔ : ∀ {a b} {A : Type a} {B : Type b} →
      Is-proposition A → Is-proposition B → (A ≃ B) ↠ (A ⇔ B)
≃↠⇔ {A = A} {B} A-prop B-prop = record
  { logical-equivalence = record
    { to   = _≃_.logical-equivalence
    ; from = ⇔→≃
    }
  ; right-inverse-of = refl
  }
  where
  ⇔→≃ : A ⇔ B → A ≃ B
  ⇔→≃ A⇔B = ↔⇒≃ record
    { surjection = record
      { logical-equivalence = A⇔B
      ; right-inverse-of    = to∘from
      }
    ; left-inverse-of = from∘to
    }
    where
    open _⇔_ A⇔B

    abstract

      to∘from : ∀ x → to (from x) ≡ x
      to∘from _ = B-prop _ _

      from∘to : ∀ x → from (to x) ≡ x
      from∘to _ = A-prop _ _

-- A corollary.

⇔→≃ :
  ∀ {a b} {A : Type a} {B : Type b} →
  Is-proposition A → Is-proposition B →
  (A → B) → (B → A) →
  A ≃ B
⇔→≃ A-prop B-prop to from =
  _↠_.from (≃↠⇔ A-prop B-prop)
    (record { to = to; from = from })

-- For propositional types logical equivalence is isomorphic to
-- equivalence (assuming extensionality).

⇔↔≃ : ∀ {a b} → Extensionality (a ⊔ b) (a ⊔ b) →
      {A : Type a} {B : Type b} →
      Is-proposition A → Is-proposition B → (A ⇔ B) ↔ (A ≃ B)
⇔↔≃ ext {A} {B} A-prop B-prop = record
  { surjection = record
    { logical-equivalence = L-eq.inverse $ _↠_.logical-equivalence $
                              ≃↠⇔ A-prop B-prop
    ; right-inverse-of    = λ _ → lift-equality ext (refl _)
    }
  ; left-inverse-of = refl
  }

-- If there is a propositional, reflexive relation on A, and related
-- elements are equal, then A is a set, and (assuming extensionality)
-- the relation is equivalent to equality.
--
-- (This is more or less Theorem 7.2.2 from "Homotopy Type Theory:
-- Univalent Foundations of Mathematics" (first edition).)

propositional-identity≃≡ :
  ∀ {a b} {A : Type a}
  (B : A → A → Type b) →
  (∀ x y → Is-proposition (B x y)) →
  (∀ x → B x x) →
  (∀ x y → B x y → x ≡ y) →
  Is-set A ×
  (Extensionality (a ⊔ b) (a ⊔ b) → ∀ {x y} → B x y ≃ (x ≡ y))
propositional-identity≃≡ B B-prop B-refl f =
    A-set
  , λ ext →
      _↔_.to (⇔↔≃ ext (B-prop _ _) A-set)
        (record
           { to   = f _ _
           ; from = λ x≡y → subst (B _) x≡y (B-refl _)
           })
  where
  A-set = propositional-identity⇒set B B-prop B-refl f

------------------------------------------------------------------------
-- Closure, preservation

abstract

  -- All h-levels are closed under the equivalence operator (assuming
  -- extensionality).

  h-level-closure :
    ∀ {a b} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    ∀ {A : Type a} {B : Type b} n →
    H-level n A → H-level n B → H-level n (A ≃ B)
  h-level-closure {a} {b} ext {A = A} {B} n hA hB =
    H-level.respects-surjection
      (_↔_.surjection $ Bijection.inverse ≃-as-Σ) n lemma₂
    where
    lemma₁ : ∀ n {to : A → B} →
             H-level n A → H-level n B →
             H-level n (Is-equivalence to)
    lemma₁ zero    cA cB = sometimes-contractible ext cA (mono₁ 0 cB)
    lemma₁ (suc n) _  _  = mono (m≤m+n 1 n) (propositional ext _)

    lemma₂ : H-level n (∃ λ (to : A → B) → Is-equivalence to)
    lemma₂ = Σ-closure n
              (Π-closure (lower-extensionality b a ext) n (λ _ → hB))
              (λ _ → lemma₁ n hA hB)

  -- For positive h-levels it is enough if one of the sides has the
  -- given h-level.

  left-closure :
    ∀ {a b} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    ∀ {A : Type a} {B : Type b} n →
    H-level (1 + n) A → H-level (1 + n) (A ≃ B)
  left-closure ext {A = A} {B} n hA =
    H-level.[inhabited⇒+]⇒+ n λ (A≃B : A ≃ B) →
      h-level-closure ext (1 + n) hA $
        H-level.respects-surjection (_≃_.surjection A≃B) (1 + n) hA

  right-closure :
    ∀ {a b} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    ∀ {A : Type a} {B : Type b} n →
    H-level (1 + n) B → H-level (1 + n) (A ≃ B)
  right-closure ext {A = A} {B} n hB =
    H-level.[inhabited⇒+]⇒+ n λ (A≃B : A ≃ B) →
      left-closure ext n $
        H-level.respects-surjection
          (_≃_.surjection (inverse A≃B)) (1 + n) hB

  -- This is not enough for level 0.

  ¬-left-closure :
    ∀ {a b} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    ∃ λ (A : Type a) → ∃ λ (B : Type b) →
      Contractible A × Is-proposition B × ¬ Contractible (A ≃ B)
  ¬-left-closure ext =
    ↑ _ ⊤ ,
    ⊥ ,
    ↑-closure 0 ⊤-contractible ,
    ⊥-propositional ,
    λ c → ⊥-elim (_≃_.to (proj₁ c) _)

  ¬-right-closure :
    ∀ {a b} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    ∃ λ (A : Type a) → ∃ λ (B : Type b) →
      Is-proposition A × Contractible B × ¬ Contractible (A ≃ B)
  ¬-right-closure ext =
    ⊥ ,
    ↑ _ ⊤ ,
    ⊥-propositional ,
    ↑-closure 0 ⊤-contractible ,
    λ c → ⊥-elim (_≃_.from (proj₁ c) _)

  -- ⊥ ≃ ⊥ is contractible (assuming extensionality).

  ⊥≃⊥-contractible :
    ∀ {ℓ₁ ℓ₂} →
    Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂) →
    Contractible (⊥ {ℓ = ℓ₁} ≃ ⊥ {ℓ = ℓ₂})
  ⊥≃⊥-contractible {ℓ₁} {ℓ₂} ext =
    ↔⇒≃ ⊥↔⊥ , λ ⊥↔⊥′ →
      lift-equality ext $
        apply-ext (lower-extensionality ℓ₂ ℓ₁ ext) λ x → ⊥-elim x
    where
    ⊥↔⊥ : ⊥ {ℓ = ℓ₁} ↔ ⊥ {ℓ = ℓ₂}
    ⊥↔⊥ = record
      { surjection = record
        { logical-equivalence = record
          { to   = ⊥-elim
          ; from = ⊥-elim
          }
        ; right-inverse-of = λ x → ⊥-elim x
        }
      ; left-inverse-of = λ x → ⊥-elim x
      }

-- Equalities are closed, in a strong sense, under applications of
-- equivalences.

≃-≡ : ∀ {a b} {A : Type a} {B : Type b} (A≃B : A ≃ B) {x y : A} →
      let open _≃_ A≃B in
      (to x ≡ to y) ≃ (x ≡ y)
≃-≡ A≃B {x} {y} = ↔⇒≃ record
  { surjection      = surjection′
  ; left-inverse-of = left-inverse-of′
  }
  where
  open _≃_ A≃B

  surjection′ : (to x ≡ to y) ↠ (x ≡ y)
  surjection′ =
    Surjection.↠-≡ $
    _↔_.surjection $
    Bijection.inverse $
    _≃_.bijection A≃B

  abstract
    left-inverse-of′ :
      ∀ p → _↠_.from surjection′ (_↠_.to surjection′ p) ≡ p
    left-inverse-of′ = λ to-x≡to-y →
      cong to (
        trans (sym (left-inverse-of x)) $
        trans (cong from to-x≡to-y) $
        left-inverse-of y)                         ≡⟨ cong-trans to _ _ ⟩
      trans (cong to (sym (left-inverse-of x))) (
        cong to (trans (cong from to-x≡to-y) (
                 left-inverse-of y)))              ≡⟨ cong₂ trans (cong-sym to _) (cong-trans to _ _) ⟩
      trans (sym (cong to (left-inverse-of x))) (
        trans (cong to (cong from to-x≡to-y)) (
        cong to (left-inverse-of y)))              ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym eq₁) $
                                                                         trans (cong to (cong from to-x≡to-y)) $
                                                                         eq₂)
                                                           (left-right-lemma x)
                                                           (left-right-lemma y) ⟩
      trans (sym (right-inverse-of (to x))) (
        trans (cong to (cong from to-x≡to-y)) (
        right-inverse-of (to y)))                  ≡⟨ _↠_.right-inverse-of (Surjection.↠-≡ $ _≃_.surjection A≃B) to-x≡to-y ⟩∎
      to-x≡to-y                                    ∎

-- A "computation rule" for ≃-≡.

to-≃-≡-refl :
  ∀ {a b} {A : Type a} {B : Type b} (A≃B : A ≃ B) {x : A} →
  _≃_.to (≃-≡ A≃B) (refl (_≃_.to A≃B x)) ≡ refl x
to-≃-≡-refl A≃B =
  Surjection.to-↠-≡-refl
    (_↔_.surjection $ Bijection.inverse $ _≃_.bijection A≃B)

-- ∃ preserves equivalences.

∃-cong :
  ∀ {a b₁ b₂} {A : Type a} {B₁ : A → Type b₁} {B₂ : A → Type b₂} →
  (∀ x → B₁ x ≃ B₂ x) → ∃ B₁ ≃ ∃ B₂
∃-cong B₁≃B₂ = ↔⇒≃ (record
  { surjection      = Surjection.∃-cong (_≃_.surjection ⊚ B₁≃B₂)
  ; left-inverse-of = uncurry λ x y →
      cong (_,_ x) (_≃_.left-inverse-of (B₁≃B₂ x) y)
  })

abstract
  private

    -- We can push subst through certain function applications.

    push-subst :
      ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂}
        (B₁ : A₁ → Type b₁) {B₂ : A₂ → Type b₂}
        {f : A₂ → A₁} {x₁ x₂ : A₂} {y : B₁ (f x₁)}
      (g : ∀ x → B₁ (f x) → B₂ x) (eq : x₁ ≡ x₂) →
      subst B₂ eq (g x₁ y) ≡ g x₂ (subst B₁ (cong f eq) y)
    push-subst B₁ {B₂} {f} g eq = elim
      (λ {x₁ x₂} eq → ∀ y → subst B₂ eq (g x₁ y) ≡
                            g x₂ (subst B₁ (cong f eq) y))
      (λ x y → subst B₂ (refl x) (g x y)           ≡⟨ subst-refl B₂ _ ⟩
               g x y                               ≡⟨ sym $ cong (g x) $ subst-refl B₁ _ ⟩
               g x (subst B₁ (refl (f x)) y)       ≡⟨ cong (λ eq → g x (subst B₁ eq y)) (sym $ cong-refl f) ⟩∎
               g x (subst B₁ (cong f (refl x)) y)  ∎)
      eq _

    push-subst′ :
      ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂}
      (A₁≃A₂ : A₁ ≃ A₂) (B₁ : A₁ → Type b₁) (B₂ : A₂ → Type b₂) →
      let open _≃_ A₁≃A₂ in {x₁ x₂ : A₁} {y : B₁ (from (to x₁))}
      (g : ∀ x → B₁ (from (to x)) → B₂ (to x)) (eq : to x₁ ≡ to x₂) →
      subst B₂ eq (g x₁ y) ≡ g x₂ (subst B₁ (cong from eq) y)
    push-subst′ A₁≃A₂ B₁ B₂ {x₁} {x₂} {y} g eq =
      subst B₂ eq (g x₁ y)                    ≡⟨ cong (subst B₂ eq) $ sym $ g′-lemma _ _ ⟩
      subst B₂ eq (g′ (to x₁) y)              ≡⟨ push-subst B₁ g′ eq ⟩
      g′ (to x₂) (subst B₁ (cong from eq) y)  ≡⟨ g′-lemma _ _ ⟩∎
      g x₂ (subst B₁ (cong from eq) y)        ∎
      where
      open _≃_ A₁≃A₂

      g′ : ∀ x′ → B₁ (from x′) → B₂ x′
      g′ x′ y = subst B₂ (right-inverse-of x′) $
                g (from x′) $
                subst B₁ (sym $ cong from $ right-inverse-of x′) y

      g′-lemma : ∀ x y → g′ (to x) y ≡ g x y
      g′-lemma x y =
        let lemma = λ y →
              let gy = g (from (to x)) $
                         subst B₁
                           (sym $ cong from $ cong to (refl _)) y in
              subst B₂ (cong to (refl _)) gy             ≡⟨ cong (λ p → subst B₂ p gy) $ cong-refl to ⟩
              subst B₂ (refl _) gy                       ≡⟨ subst-refl B₂ gy ⟩
              gy                                         ≡⟨ cong (λ p → g (from (to x)) $ subst B₁ (sym $ cong from p) y) $ cong-refl to ⟩
              g (from (to x))
                (subst B₁ (sym $ cong from (refl _)) y)  ≡⟨ cong (λ p → g (from (to x)) $ subst B₁ (sym p) y) $ cong-refl from ⟩
              g (from (to x))
                (subst B₁ (sym (refl _)) y)              ≡⟨ cong (λ p → g (from (to x)) $ subst B₁ p y) sym-refl ⟩
              g (from (to x)) (subst B₁ (refl _) y)      ≡⟨ cong (g (from (to x))) $ subst-refl B₁ y ⟩∎
              g (from (to x)) y                          ∎
        in
        subst B₂ (right-inverse-of (to x))
          (g (from (to x)) $
           subst B₁ (sym $ cong from $
                       right-inverse-of (to x)) y)  ≡⟨ cong (λ p → subst B₂ p (g (from (to x)) $ subst B₁ (sym $ cong from p) y)) $
                                                         sym $ left-right-lemma x ⟩
        subst B₂ (cong to $ left-inverse-of x)
          (g (from (to x)) $
           subst B₁ (sym $ cong from $ cong to $
                       left-inverse-of x) y)        ≡⟨ elim¹
                                                         (λ {x′} eq →
                                                            (y : B₁ (from (to x′))) →
                                                            subst B₂ (cong to eq)
                                                              (g (from (to x)) $ subst B₁ (sym $ cong from $ cong to eq) y) ≡
                                                            g x′ y)
                                                         lemma
                                                         (left-inverse-of x) y ⟩∎
        g x y                                       ∎

-- If the first component is instantiated to the identity, then the
-- following lemmas state that ∃ preserves injections and bijections.

∃-preserves-injections :
  ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂}
    {B₁ : A₁ → Type b₁} {B₂ : A₂ → Type b₂}
  (A₁≃A₂ : A₁ ≃ A₂) → (∀ x → B₁ x ↣ B₂ (_≃_.to A₁≃A₂ x)) →
  Σ A₁ B₁ ↣ Σ A₂ B₂
∃-preserves-injections {A₁ = A₁} {A₂} {B₁} {B₂} A₁≃A₂ B₁↣B₂ = record
  { to        = to′
  ; injective = injective′
  }
  where
  open _↣_

  to′ : Σ A₁ B₁ → Σ A₂ B₂
  to′ = Σ-map (_≃_.to A₁≃A₂) (_↣_.to (B₁↣B₂ _))

  abstract
    injective′ : Injective to′
    injective′ {x = (x₁ , x₂)} {y = (y₁ , y₂)} =
      _↔_.to Bijection.Σ-≡,≡↔≡ ⊚
      Σ-map (_≃_.injective A₁≃A₂) (λ {eq₁} eq₂ →
        let lemma =
              to (B₁↣B₂ y₁) (subst B₁ (_≃_.injective A₁≃A₂ eq₁) x₂)      ≡⟨ refl _ ⟩
              to (B₁↣B₂ y₁)
                (subst B₁ (trans (sym (_≃_.left-inverse-of A₁≃A₂ x₁)) $
                           trans (cong (_≃_.from A₁≃A₂) eq₁)
                                 (_≃_.left-inverse-of A₁≃A₂ y₁))
                          x₂)                                            ≡⟨ cong (to (B₁↣B₂ y₁)) $ sym $ subst-subst B₁ _ _ _ ⟩
              to (B₁↣B₂ y₁)
                 (subst B₁ (trans (cong (_≃_.from A₁≃A₂) eq₁)
                                  (_≃_.left-inverse-of A₁≃A₂ y₁)) $
                  subst B₁ (sym (_≃_.left-inverse-of A₁≃A₂ x₁))
                           x₂)                                           ≡⟨ cong (to (B₁↣B₂ y₁)) $ sym $ subst-subst B₁ _ _ _ ⟩
              to (B₁↣B₂ y₁)
                 (subst B₁ (_≃_.left-inverse-of A₁≃A₂ y₁) $
                  subst B₁ (cong (_≃_.from A₁≃A₂) eq₁) $
                  subst B₁ (sym (_≃_.left-inverse-of A₁≃A₂ x₁)) x₂)      ≡⟨ sym $ push-subst′ A₁≃A₂ B₁ B₂
                                                                              (λ x y → to (B₁↣B₂ x)
                                                                                (subst B₁ (_≃_.left-inverse-of A₁≃A₂ x) y))
                                                                              eq₁ ⟩
              subst B₂ eq₁
                (to (B₁↣B₂ x₁) $
                 subst B₁ (_≃_.left-inverse-of A₁≃A₂ x₁) $
                 subst B₁ (sym (_≃_.left-inverse-of A₁≃A₂ x₁)) x₂)       ≡⟨ cong (subst B₂ eq₁ ⊚ to (B₁↣B₂ x₁)) $ subst-subst B₁ _ _ _ ⟩
              subst B₂ eq₁
                (to (B₁↣B₂ x₁) $
                 subst B₁ (trans (sym (_≃_.left-inverse-of A₁≃A₂ x₁))
                                 (_≃_.left-inverse-of A₁≃A₂ x₁))
                          x₂)                                            ≡⟨ cong (λ p → subst B₂ eq₁ (to (B₁↣B₂ x₁) (subst B₁ p x₂))) $
                                                                                trans-symˡ _ ⟩
              subst B₂ eq₁ (to (B₁↣B₂ x₁) $ subst B₁ (refl _) x₂)        ≡⟨ cong (subst B₂ eq₁ ⊚ to (B₁↣B₂ x₁)) $
                                                                                subst-refl B₁ x₂ ⟩
              subst B₂ eq₁ (to (B₁↣B₂ x₁) x₂)                            ≡⟨ eq₂ ⟩∎
              to (B₁↣B₂ y₁) y₂                                           ∎
        in
        subst B₁ (_≃_.injective A₁≃A₂ eq₁) x₂  ≡⟨ _↣_.injective (B₁↣B₂ y₁) lemma ⟩∎
        y₂                                     ∎) ⊚
      Σ-≡,≡←≡

∃-preserves-bijections :
  ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂}
    {B₁ : A₁ → Type b₁} {B₂ : A₂ → Type b₂}
  (A₁≃A₂ : A₁ ≃ A₂) → (∀ x → B₁ x ↔ B₂ (_≃_.to A₁≃A₂ x)) →
  Σ A₁ B₁ ↔ Σ A₂ B₂
∃-preserves-bijections {A₁ = A₁} {A₂} {B₁} {B₂} A₁≃A₂ B₁↔B₂ = record
  { surjection      = surjection′
  ; left-inverse-of = left-inverse-of′
  }
  where
  open _↔_

  surjection′ : Σ A₁ B₁ ↠ Σ A₂ B₂
  surjection′ =
    Surjection.Σ-cong (_≃_.surjection A₁≃A₂) (surjection ⊚ B₁↔B₂)

  abstract
    left-inverse-of′ :
      ∀ p → _↠_.from surjection′ (_↠_.to surjection′ p) ≡ p
    left-inverse-of′ = λ p → Σ-≡,≡→≡
      (_≃_.left-inverse-of A₁≃A₂ (proj₁ p))
      (subst B₁ (_≃_.left-inverse-of A₁≃A₂ (proj₁ p))
         (from (B₁↔B₂ _)
            (subst B₂ (sym (_≃_.right-inverse-of A₁≃A₂
                              (_≃_.to A₁≃A₂ (proj₁ p))))
               (to (B₁↔B₂ _) (proj₂ p))))                        ≡⟨ push-subst B₂ (λ x → from (B₁↔B₂ x))
                                                                      (_≃_.left-inverse-of A₁≃A₂ (proj₁ p)) ⟩
       from (B₁↔B₂ _)
         (subst B₂ (cong (_≃_.to A₁≃A₂)
                         (_≃_.left-inverse-of A₁≃A₂ (proj₁ p)))
            (subst B₂ (sym (_≃_.right-inverse-of A₁≃A₂
                              (_≃_.to A₁≃A₂ (proj₁ p))))
               (to (B₁↔B₂ _) (proj₂ p))))                        ≡⟨ cong (λ eq → from (B₁↔B₂ _)
                                                                                (subst B₂ eq
                                                                                (subst B₂ (sym (_≃_.right-inverse-of A₁≃A₂ _))
                                                                                (to (B₁↔B₂ _) (proj₂ p))))) $
                                                                         _≃_.left-right-lemma A₁≃A₂ _ ⟩
       from (B₁↔B₂ _)
         (subst B₂ (_≃_.right-inverse-of A₁≃A₂
                      (_≃_.to A₁≃A₂ (proj₁ p)))
            (subst B₂ (sym (_≃_.right-inverse-of A₁≃A₂
                              (_≃_.to A₁≃A₂ (proj₁ p))))
               (to (B₁↔B₂ _) (proj₂ p))))                        ≡⟨ cong (from (B₁↔B₂ _)) $ subst-subst-sym B₂ _ _ ⟩
       from (B₁↔B₂ _) (to (B₁↔B₂ _) (proj₂ p))                   ≡⟨ left-inverse-of (B₁↔B₂ _) _ ⟩∎
       proj₂ p                                                   ∎)

-- Σ preserves equivalence.

Σ-preserves : ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂}
                {B₁ : A₁ → Type b₁} {B₂ : A₂ → Type b₂}
              (A₁≃A₂ : A₁ ≃ A₂) → (∀ x → B₁ x ≃ B₂ (_≃_.to A₁≃A₂ x)) →
              Σ A₁ B₁ ≃ Σ A₂ B₂
Σ-preserves A₁≃A₂ B₁≃B₂ = ↔⇒≃ $
  ∃-preserves-bijections A₁≃A₂ (_≃_.bijection ⊚ B₁≃B₂)

-- A part of the implementation of ≃-preserves (see below) that does
-- not depend on extensionality.

≃-preserves-⇔ :
  ∀ {a₁ a₂ b₁ b₂}
    {A₁ : Type a₁} {A₂ : Type a₂} {B₁ : Type b₁} {B₂ : Type b₂} →
  A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ ≃ B₁) ⇔ (A₂ ≃ B₂)
≃-preserves-⇔ A₁≃A₂ B₁≃B₂ = record
  { to   = λ A₁≃B₁ → B₁≃B₂ ∘ A₁≃B₁ ∘ inverse A₁≃A₂
  ; from = λ A₂≃B₂ → inverse B₁≃B₂ ∘ A₂≃B₂ ∘ A₁≃A₂
  }

-- Equivalence preserves equivalences (assuming extensionality).

≃-preserves :
  ∀ {a₁ a₂ b₁ b₂} →
  Extensionality (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂) (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂) →
  {A₁ : Type a₁} {A₂ : Type a₂} {B₁ : Type b₁} {B₂ : Type b₂} →
  A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ ≃ B₁) ≃ (A₂ ≃ B₂)
≃-preserves {a₁} {a₂} {b₁} {b₂} ext {A₁} {A₂} {B₁} {B₂} A₁≃A₂ B₁≃B₂ =
  ↔⇒≃ (record
    { surjection = record
      { logical-equivalence = ≃-preserves-⇔ A₁≃A₂ B₁≃B₂
      ; right-inverse-of    = to∘from
      }
    ; left-inverse-of = from∘to
    })
  where
  open _≃_

  ext₁ = lower-extensionality (a₁ ⊔ b₁) (a₁ ⊔ b₁) ext
  ext₂ = lower-extensionality (a₂ ⊔ b₂) (a₂ ⊔ b₂) ext

  abstract
    to∘from :
      (A₂≃B₂ : A₂ ≃ B₂) →
      B₁≃B₂ ∘ (inverse B₁≃B₂ ∘ A₂≃B₂ ∘ A₁≃A₂) ∘ inverse A₁≃A₂ ≡ A₂≃B₂
    to∘from A₂≃B₂ =
      lift-equality ext₁ $
      apply-ext (lower-extensionality b₂ a₂ ext₁) λ x →
        to B₁≃B₂ (from B₁≃B₂ (to A₂≃B₂ (to A₁≃A₂ (from A₁≃A₂ x))))  ≡⟨ right-inverse-of B₁≃B₂ _ ⟩
        to A₂≃B₂ (to A₁≃A₂ (from A₁≃A₂ x))                          ≡⟨ cong (to A₂≃B₂) $ right-inverse-of A₁≃A₂ _ ⟩∎
        to A₂≃B₂ x                                                  ∎

    from∘to :
      (A₁≃B₁ : A₁ ≃ B₁) →
      inverse B₁≃B₂ ∘ (B₁≃B₂ ∘ A₁≃B₁ ∘ inverse A₁≃A₂) ∘ A₁≃A₂ ≡ A₁≃B₁
    from∘to A₁≃B₁ =
      lift-equality ext₂ $
      apply-ext (lower-extensionality b₁ a₁ ext₂) λ x →
        from B₁≃B₂ (to B₁≃B₂ (to A₁≃B₁ (from A₁≃A₂ (to A₁≃A₂ x))))  ≡⟨ left-inverse-of B₁≃B₂ _ ⟩
        to A₁≃B₁ (from A₁≃A₂ (to A₁≃A₂ x))                          ≡⟨ cong (to A₁≃B₁) $ left-inverse-of A₁≃A₂ _ ⟩∎
        to A₁≃B₁ x                                                  ∎

-- Equivalence preserves bijections (assuming extensionality).

≃-preserves-bijections :
  ∀ {a₁ a₂ b₁ b₂} →
  Extensionality (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂) (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂) →
  {A₁ : Type a₁} {A₂ : Type a₂} {B₁ : Type b₁} {B₂ : Type b₂} →
  A₁ ↔ A₂ → B₁ ↔ B₂ → (A₁ ≃ B₁) ↔ (A₂ ≃ B₂)
≃-preserves-bijections ext A₁↔A₂ B₁↔B₂ =
  _≃_.bijection $ ≃-preserves ext (↔⇒≃ A₁↔A₂) (↔⇒≃ B₁↔B₂)

------------------------------------------------------------------------
-- More lemmas

abstract

  -- As a consequence of extensionality-isomorphism and ≃-≡ we get a
  -- strengthening of W-≡,≡↠≡.

  W-≡,≡≃≡ : ∀ {a b} {A : Type a} {B : A → Type b} →
            Extensionality b (a ⊔ b) →
            ∀ {x y} {f : B x → W A B} {g : B y → W A B} →
            (∃ λ (p : x ≡ y) → ∀ i → f i ≡ g (subst B p i)) ≃
            (sup x f ≡ sup y g)
  W-≡,≡≃≡ {a} {A = A} {B} ext {x} {y} {f} {g} =
    (∃ λ p → ∀ i → f i ≡ g (subst B p i))        ≃⟨ Σ-preserves id lemma ⟩
    (∃ λ p → subst (λ x → B x → W A B) p f ≡ g)  ≃⟨ ↔⇒≃ Bijection.Σ-≡,≡↔≡ ⟩
    ((x , f) ≡ (y , g))                          ≃⟨ ≃-≡ (↔⇒≃ W-unfolding) ⟩□
    (sup x f ≡ sup y g)                          □
    where
    lemma : (p : x ≡ y) →
            (∀ i → f i ≡ g (subst B p i)) ≃
            (subst (λ x → B x → W A B) p f ≡ g)
    lemma p = elim
      (λ {x y} p → (f : B x → W A B) (g : B y → W A B) →
                   (∀ i → f i ≡ g (subst B p i)) ≃
                   (subst (λ x → B x → W A B) p f ≡ g))
      (λ x f g →
         (∀ i → f i ≡ g (subst B (refl x) i))        ≃⟨ subst (λ h → (∀ i → f i ≡ g (h i)) ≃ (∀ i → f i ≡ g i))
                                                              (sym (apply-ext (lower-extensionality lzero a ext) (subst-refl B)))
                                                              id ⟩
         (∀ i → f i ≡ g i)                           ≃⟨ extensionality-isomorphism ext ⟩
         (f ≡ g)                                     ≃⟨ subst (λ h → (f ≡ g) ≃ (h ≡ g))
                                                              (sym $ subst-refl (λ x' → B x' → W A B) f)
                                                              id ⟩□
         (subst (λ x → B x → W A B) (refl x) f ≡ g)  □)
      p f g

  -- Some rearrangement lemmas.

  to-subst :
    ∀ {a p q} {A : Type a} {P : A → Type p} {Q : A → Type q}
      {x y : A} {eq : x ≡ y} {f : P x ≃ Q x} →
    _≃_.to (subst (λ x → P x ≃ Q x) eq f) ≡
    subst (λ x → P x → Q x) eq (_≃_.to f)
  to-subst {P = P} {Q = Q} {eq = eq} {f = f} = elim¹
    (λ eq →
       _≃_.to (subst (λ x → P x ≃ Q x) eq f) ≡
       subst (λ x → P x → Q x) eq (_≃_.to f))
    (_≃_.to (subst (λ x → P x ≃ Q x) (refl _) f)  ≡⟨ cong _≃_.to $ subst-refl (λ _ → _ ≃ _) _ ⟩
     _≃_.to f                                     ≡⟨ sym $ subst-refl _ _ ⟩∎
     subst (λ x → P x → Q x) (refl _) (_≃_.to f)  ∎)
    eq

  from-subst :
    ∀ {a p q} {A : Type a} {P : A → Type p} {Q : A → Type q}
      {x y : A} {eq : x ≡ y} {f : P x ≃ Q x} →
    _≃_.from (subst (λ x → P x ≃ Q x) eq f) ≡
    subst (λ x → Q x → P x) eq (_≃_.from f)
  from-subst {P = P} {Q = Q} {eq = eq} {f = f} = elim¹
    (λ eq →
       _≃_.from (subst (λ x → P x ≃ Q x) eq f) ≡
       subst (λ x → Q x → P x) eq (_≃_.from f))
    (_≃_.from (subst (λ x → P x ≃ Q x) (refl _) f)  ≡⟨ cong _≃_.from $ subst-refl (λ _ → _ ≃ _) _ ⟩
     _≃_.from f                                     ≡⟨ sym $ subst-refl _ _ ⟩∎
     subst (λ x → Q x → P x) (refl _) (_≃_.from f)  ∎)
    eq

-- If P is pointwise equivalent to x ≡_, then every function of type
-- {y : A} → x ≡ y → P y is an equivalence (pointwise).
--
-- Andrea Vezzosi showed me a similar result, that he thought that
-- Thierry Coquand had informed him about.

≡≃→≡→→Is-equivalence :
  ∀ {a p} {A : Type a} {x : A}
  (P : A → Type p) →
  ({y : A} → (x ≡ y) ≃ P y) →
  (f : {y : A} → x ≡ y → P y) →
  {y : A} → Is-equivalence (f {y = y})
≡≃→≡→→Is-equivalence {x = x} P ≡≃P f {y = y} =
  drop-Σ-map-id f equiv₂ y
  where
  equiv₁ : (∃ λ y → x ≡ y) ≃ ∃ P
  equiv₁ = ∃-cong λ _ → ≡≃P

  contr : Contractible (∃ P)
  contr =
    H-level.respects-surjection
      (_≃_.surjection equiv₁)
      0
      (other-singleton-contractible _)

  equiv₂ : Is-equivalence (Σ-map P.id f)
  equiv₂ =
    _≃_.is-equivalence $
    with-other-function
      equiv₁
      _
      (λ _ → mono₁ 0 contr _ _)

ext: agda

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Data.Char.Instance where

open import Agda.Builtin.Char
open import Class.Equality
open import Class.Show
open import Data.Char renaming (_≟_ to _≟C_)
open import Data.List
open import Data.String

instance
  Char-Eq : Eq Char
  Char-Eq = record { _≟_ = _≟C_ }

  Char-EqB : EqB Char
  Char-EqB = record { _≣_ = primCharEquality }

  Char-Show : Show Char
  Char-Show = record { show = λ c -> fromList [ c ] }

  CharList-Show : Show (List Char)
  CharList-Show = record { show = fromList }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-# OPTIONS --without-K --rewriting #-}

module lib.types.Types where

open import lib.Basics
open import lib.types.BigWedge public
open import lib.types.Bool public
open import lib.types.Choice public
open import lib.types.Circle public
open import lib.types.Cofiber public
open import lib.types.CommutingSquare public
open import lib.types.Coproduct public
open import lib.types.Cospan public
open import lib.types.Cover public
open import lib.types.EilenbergMacLane1 public
open import lib.types.Empty public
open import lib.types.Fin public
open import lib.types.NatColim public
open import lib.types.Group public
open import lib.types.GroupSet public
open import lib.types.Groupoid public
open import lib.types.HList public
open import lib.types.Int public
open import lib.types.IteratedSuspension public
open import lib.types.Join public
open import lib.types.Lift public
open import lib.types.List public
open import lib.types.LoopSpace public
open import lib.types.Modality public
open import lib.types.Nat public
open import lib.types.PathSeq public
open import lib.types.PathSet public
open import lib.types.Paths public
open import lib.types.Pi public
open import lib.types.Pointed public
open import lib.types.Pullback public
open import lib.types.Pushout public
open import lib.types.PushoutFlattening public
open import lib.types.PushoutFlip public
open import lib.types.PushoutFmap public
open import lib.types.SetQuotient public
open import lib.types.Sigma public
open import lib.types.Smash public
open import lib.types.Span public
open import lib.types.Subtype public
open import lib.types.Suspension public
open import lib.types.TLevel public
open import lib.types.Torus public
open import lib.types.Truncation public
open import lib.types.Unit public
open import lib.types.Wedge public
open import lib.types.Word public

-- This should probably not be exported
-- module Generic1HIT {i j} (A : Type i) (B : Type j) (f g : B → A) where
--   open import lib.types.Generic1HIT A B f g public

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

module Algebra.Linear.Core where

open import Relation.Binary
open import Relation.Nullary using (¬_)
open import Level using (_⊔_)
open import Data.Fin using (Fin; suc; zero)

VectorAddition : ∀ {c} -> Set c -> Set c
VectorAddition V = V -> V -> V

ScalarMultiplication : ∀ {c k} -> Set k -> Set c -> Set (k ⊔ c)
ScalarMultiplication K V = K -> V -> V

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
{-# OPTIONS --cubical --safe #-}

open import Prelude
open import Relation.Binary

module Relation.Binary.Construct.LowerBound {e} {E : Type e} {r} (totalOrder : TotalOrder E r) where

open TotalOrder totalOrder renaming (refl to ≤-refl)
import Data.Unit.UniversePolymorphic as Poly
import Data.Empty.UniversePolymorphic as Poly

data ⌊∙⌋ : Type e where
  ⌊⊥⌋ : ⌊∙⌋
  ⌊_⌋ : E → ⌊∙⌋

_≤⌊_⌋ : ⌊∙⌋ → E → Type r
⌊⊥⌋   ≤⌊ y ⌋ = Poly.⊤
⌊ x ⌋ ≤⌊ y ⌋ = x ≤ y

_⌊≤⌋_ : ⌊∙⌋ → ⌊∙⌋ → Type r
x     ⌊≤⌋ ⌊ y ⌋ = x ≤⌊ y ⌋
⌊⊥⌋   ⌊≤⌋ ⌊⊥⌋   = Poly.⊤
⌊ x ⌋ ⌊≤⌋ ⌊⊥⌋   = Poly.⊥

lb-ord : TotalOrder ⌊∙⌋ r
PartialOrder._≤_ (TotalOrder.partialOrder lb-ord) = _⌊≤⌋_
PartialOrder.refl (partialOrder lb-ord) {⌊⊥⌋} = Poly.tt
PartialOrder.refl (partialOrder lb-ord) {⌊ x ⌋} = ≤-refl
PartialOrder.antisym (TotalOrder.partialOrder lb-ord) {⌊⊥⌋} {⌊⊥⌋} x≤y y≤x _ = ⌊⊥⌋
PartialOrder.antisym (TotalOrder.partialOrder lb-ord) {⌊ x ⌋} {⌊ x₁ ⌋} x≤y y≤x i = ⌊ antisym x≤y y≤x i ⌋
PartialOrder.trans (TotalOrder.partialOrder lb-ord) {⌊⊥⌋} {⌊⊥⌋} {⌊⊥⌋} x≤y y≤z = Poly.tt
PartialOrder.trans (TotalOrder.partialOrder lb-ord) {⌊⊥⌋} {⌊⊥⌋} {⌊ x ⌋} x≤y y≤z = Poly.tt
PartialOrder.trans (TotalOrder.partialOrder lb-ord) {⌊⊥⌋} {⌊ x ⌋} {⌊ x₁ ⌋} x≤y y≤z = Poly.tt
PartialOrder.trans (TotalOrder.partialOrder lb-ord) {⌊ x ⌋} {⌊ x₁ ⌋} {⌊ x₂ ⌋} x≤y y≤z = trans x≤y y≤z
TotalOrder._≤?_ lb-ord ⌊⊥⌋ ⌊⊥⌋ = inl Poly.tt
TotalOrder._≤?_ lb-ord ⌊ x ⌋ ⌊⊥⌋ = inr Poly.tt
TotalOrder._≤?_ lb-ord ⌊⊥⌋ ⌊ x₁ ⌋ = inl Poly.tt
TotalOrder._≤?_ lb-ord ⌊ x ⌋ ⌊ y ⌋ = x ≤? y

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper