text:
------------------------------------------------------------------------
-- The univalence axiom
------------------------------------------------------------------------

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

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

open import Equality

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

open import Bijection eq as Bijection using (_↔_)
open import Bool eq
open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq
  using (_≃_; ⟨_,_⟩; Is-equivalence) renaming (_∘_ to _⊚_)
import Equivalence.Contractible-preimages eq as CP
import Equivalence.Half-adjoint eq as HA
open import Function-universe eq as F hiding (id; _∘_)
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 using (_⇔_)
import Nat eq as Nat
open import Prelude hiding (swap)
open import Surjection eq using (_↠_)

------------------------------------------------------------------------
-- The univalence axiom

-- If two sets are equal, then they are equivalent.

≡⇒≃ : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B
≡⇒≃ = ≡⇒↝ equivalence

-- The univalence axiom states that ≡⇒≃ is an equivalence.

record Univalence′ {ℓ} (A B : Type ℓ) : Type (lsuc ℓ) where
  no-eta-equality
  pattern
  field
    univalence : Is-equivalence (≡⇒≃ {A = A} {B = B})

Univalence : ∀ ℓ → Type (lsuc ℓ)
Univalence ℓ = {A B : Type ℓ} → Univalence′ A B

-- An immediate consequence is that equalities are equivalent to
-- equivalences.

≡≃≃ : ∀ {ℓ} {A B : Type ℓ} → Univalence′ A B → (A ≡ B) ≃ (A ≃ B)
≡≃≃ univ = ⟨ ≡⇒≃ , Univalence′.univalence univ ⟩

-- In the case of sets equalities are equivalent to bijections (if we
-- add the assumption of extensionality).

≡≃↔ : ∀ {ℓ} {A B : Type ℓ} →
      Univalence′ A B →
      Extensionality ℓ ℓ →
      Is-set A →
      (A ≡ B) ≃ (A ↔ B)
≡≃↔ {A = A} {B} univ ext A-set =
  (A ≡ B)  ↝⟨ ≡≃≃ univ ⟩
  (A ≃ B)  ↔⟨ inverse $ Eq.↔↔≃ ext A-set ⟩□
  (A ↔ B)  □

-- Some abbreviations.

≡⇒→ : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A → B
≡⇒→ = _≃_.to ∘ ≡⇒≃

≡⇒← : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → B → A
≡⇒← = _≃_.from ∘ ≡⇒≃

≃⇒≡ : ∀ {ℓ} {A B : Type ℓ} → Univalence′ A B → A ≃ B → A ≡ B
≃⇒≡ univ = _≃_.from (≡≃≃ univ)

-- Univalence′ can be expressed without the record type.

Univalence′≃Is-equivalence-≡⇒≃ :
  ∀ {ℓ} {A B : Type ℓ} →
  Univalence′ A B ≃ Is-equivalence (≡⇒≃ {A = A} {B = B})
Univalence′≃Is-equivalence-≡⇒≃ =
  Eq.↔→≃
    Univalence′.univalence
    (λ eq → record { univalence = eq })
    refl
    (λ { (record { univalence = _ }) → refl _ })

------------------------------------------------------------------------
-- Propositional extensionality

-- Propositional extensionality.
--
-- Basically as defined by Chapman, Uustalu and Veltri in "Quotienting
-- the Delay Monad by Weak Bisimilarity".

Propositional-extensionality : (ℓ : Level) → Type (lsuc ℓ)
Propositional-extensionality ℓ =
  {A B : Type ℓ} → Is-proposition A → Is-proposition B → A ⇔ B → A ≡ B

-- Propositional extensionality is equivalent to univalence restricted
-- to propositions (assuming extensionality).
--
-- I took the statement of this result from Chapman, Uustalu and
-- Veltri's "Quotienting the Delay Monad by Weak Bisimilarity", and
-- Nicolai Kraus helped me with the proof.

Propositional-extensionality-is-univalence-for-propositions :
  ∀ {ℓ} →
  Extensionality (lsuc ℓ) (lsuc ℓ) →

  Propositional-extensionality ℓ
    ≃
  ({A B : Type ℓ} →
   Is-proposition A → Is-proposition B → Univalence′ A B)

Propositional-extensionality-is-univalence-for-propositions {ℓ} ext =
  Propositional-extensionality ℓ                          ↝⟨ lemma ⟩

  ({A B : Type ℓ} →
   Is-proposition A → Is-proposition B →
   Is-equivalence (≡⇒≃ {A = A} {B = B}))                  ↝⟨ (implicit-∀-cong ext $
                                                              implicit-∀-cong ext $
                                                              ∀-cong ext′ λ _ →
                                                              ∀-cong ext′ λ _ →
                                                              inverse Univalence′≃Is-equivalence-≡⇒≃) ⟩□
  ({A B : Type ℓ} →
   Is-proposition A → Is-proposition B → Univalence′ A B) □
  where
  ext′ : Extensionality ℓ (lsuc ℓ)
  ext′ = lower-extensionality _ lzero ext

  ext″ : Extensionality ℓ ℓ
  ext″ = lower-extensionality _ _ ext

  ⇔≃≡ :
    Propositional-extensionality ℓ →
    {A B : Type ℓ} →
    Is-proposition A → Is-proposition B →
    (A ⇔ B) ≃ (A ≡ B)
  ⇔≃≡ prop-ext {A} {B} A-prop B-prop =
    A ⇔ B                        ↝⟨ proj₂ (Eq.propositional-identity≃≡
                                             (λ (A B : Proposition ℓ) → proj₁ A ⇔ proj₁ B)
                                             (λ { (A , A-prop) (B , B-prop) →
                                                  ⇔-closure ext″ 1 A-prop B-prop })
                                             (λ _ → F.id)
                                             (λ { (A , A-prop) (B , B-prop) A⇔B →
                                                  Σ-≡,≡→≡ (prop-ext A-prop B-prop A⇔B)
                                                          (H-level-propositional ext″ 1 _ _) }))
                                          ext ⟩
    (A , A-prop) ≡ (B , B-prop)  ↔⟨ inverse $ ignore-propositional-component
                                                (H-level-propositional ext″ 1) ⟩□
    A ≡ B                        □

  ≡-closure :
    Propositional-extensionality ℓ →
    {A B : Type ℓ} →
    Is-proposition A → Is-proposition B → Is-proposition (A ≡ B)
  ≡-closure prop-ext A-prop B-prop =
    H-level.respects-surjection
      (_≃_.surjection (⇔≃≡ prop-ext A-prop B-prop))
      1
      (⇔-closure ext″ 1 A-prop B-prop)

  lemma =
    Eq.⇔→≃
      ([inhabited⇒+]⇒+ 0 λ prop-ext →
       implicit-Π-closure ext 1 λ _ →
       implicit-Π-closure ext 1 λ _ →
       Π-closure ext′ 1 λ A-prop →
       Π-closure ext′ 1 λ B-prop →
       Π-closure ext′ 1 λ _ →
       ≡-closure (prop-ext {_}) A-prop B-prop)
      (implicit-Π-closure ext 1 λ _ →
       implicit-Π-closure ext 1 λ _ →
       Π-closure ext′ 1 λ _ →
       Π-closure ext′ 1 λ _ →
       Eq.propositional ext _)
      (λ prop-ext A-prop B-prop →
         _⇔_.from HA.Is-equivalence⇔Is-equivalence-CP $ λ A≃B →
         ( prop-ext A-prop B-prop (_≃_.logical-equivalence A≃B)
         , Eq.left-closure ext″ 0 A-prop _ _
         ) , λ _ → Σ-≡,≡→≡
               (≡-closure prop-ext A-prop B-prop _ _)
               (mono₁ 1 (Eq.left-closure ext″ 0 A-prop) _ _))
      (λ univ {A B} A-prop B-prop →
         A ⇔ B  ↔⟨ Eq.⇔↔≃ ext″ A-prop B-prop ⟩
         A ≃ B  ↔⟨ inverse ⟨ _ , univ A-prop B-prop ⟩ ⟩□
         A ≡ B  □)

------------------------------------------------------------------------
-- An alternative formulation of univalence

-- First some supporting lemmas.

-- A variant of a part of Theorem 5.8.2 from the HoTT book.

flip-subst-is-equivalence↔∃-is-contractible :
  ∀ {a pℓ} {A : Type a} {P : A → Type pℓ} {x : A} {p : P x} →
  (∀ y → Is-equivalence (flip (subst {y = y} P) p))
    ↝[ a ⊔ pℓ ∣ a ⊔ pℓ ]
  Contractible (∃ P)
flip-subst-is-equivalence↔∃-is-contractible
  {pℓ = pℓ} {P = P} {x = x} {p = p} =
  generalise-ext?-prop
    lemma
    (λ ext → Π-closure (lower-extensionality pℓ lzero ext) 1 λ _ →
             Eq.propositional ext _)
    Contractible-propositional
  where
  lemma :
    (∀ y → Is-equivalence (flip (subst {y = y} P) p))
      ⇔
    Contractible (∃ P)
  lemma = record
    { to = λ eq →                         $⟨ other-singleton-contractible x ⟩
        Contractible (Other-singleton x)  ↝⟨ id ⟩
        Contractible (∃ (x ≡_))           ↝⟨ H-level.respects-surjection (∃-cong λ y → _≃_.surjection ⟨ _ , eq y ⟩) 0 ⟩□
        Contractible (∃ P)                □
    ; from = λ { ((y , q) , u) z →
        _≃_.is-equivalence (Eq.↔⇒≃ (record
          { surjection = record
            { logical-equivalence = record
              { from = λ r →
                  x  ≡⟨ cong proj₁ $ sym $ u (x , p) ⟩
                  y  ≡⟨ cong proj₁ $ u (z , r) ⟩∎
                  z  ∎
              }
            ; right-inverse-of = λ r →
                subst P (trans (cong proj₁ (sym (u (x , p))))
                               (cong proj₁ (u (z , r)))) p         ≡⟨ sym $ subst-subst _ _ _ _ ⟩

                subst P (cong proj₁ (u (z , r)))
                  (subst P (cong proj₁ (sym (u (x , p)))) p)       ≡⟨ cong (subst P _) $ cong (λ p → subst P p _) $ sym $ proj₁-Σ-≡,≡←≡ _ ⟩

                subst P (cong proj₁ (u (z , r)))
                  (subst P (proj₁ (Σ-≡,≡←≡ (sym (u (x , p))))) p)  ≡⟨ cong (subst P _) $ proj₂ $ Σ-≡,≡←≡ (sym (u (x , p))) ⟩

                subst P (cong proj₁ (u (z , r))) q                 ≡⟨ cong (λ p → subst P p _) $ sym $ proj₁-Σ-≡,≡←≡ _ ⟩

                subst P (proj₁ (Σ-≡,≡←≡ (u (z , r)))) q            ≡⟨ proj₂ $ Σ-≡,≡←≡ (u (z , r)) ⟩∎

                r                                                  ∎
            }
          ; left-inverse-of = elim¹
              (λ {z} x≡z → trans (cong proj₁ (sym (u (x , p))))
                                 (cong proj₁ (u (z , subst P x≡z p))) ≡
                           x≡z)
              (trans (cong proj₁ (sym (u (x , p))))
                     (cong proj₁ (u (x , subst P (refl x) p)))  ≡⟨ cong₂ trans (cong-sym _ _)
                                                                               (cong (λ p → cong proj₁ (u (x , p))) $ subst-refl _ _) ⟩
               trans (sym (cong proj₁ (u (x , p))))
                     (cong proj₁ (u (x , p)))                   ≡⟨ trans-symˡ _ ⟩∎

               refl x                                           ∎)
          })) }
    }

-- If f is an equivalence, then f ∘ sym is also an equivalence.

∘-sym-preserves-equivalences :
  ∀ {a b} {A : Type a} {B : Type b} {x y : A} {f : x ≡ y → B} →
  Is-equivalence f ↝[ a ⊔ b ∣ a ⊔ b ] Is-equivalence (f ∘ sym)
∘-sym-preserves-equivalences {A = A} {B} =
  Is-equivalence≃Is-equivalence-∘ʳ
    (_≃_.is-equivalence $ Eq.↔⇒≃ ≡-comm)

-- An alternative formulation of univalence, due to Martin Escardo
-- (see the following post to the Homotopy Type Theory group from
-- 2018-04-05:
-- https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ).

Other-univalence : ∀ ℓ → Type (lsuc ℓ)
Other-univalence ℓ =
  {B : Type ℓ} → Contractible (∃ λ (A : Type ℓ) → A ≃ B)

-- Univalence and Other-univalence are pointwise isomorphic (assuming
-- extensionality).

Univalence↔Other-univalence :
  ∀ {ℓ} →
  Univalence ℓ ↝[ lsuc ℓ ∣ lsuc ℓ ] Other-univalence ℓ
Univalence↔Other-univalence {ℓ = ℓ} ext =
  Univalence ℓ                                                          ↝⟨ implicit-∀-cong ext $ implicit-∀-cong ext $
                                                                           from-equivalence Univalence′≃Is-equivalence-≡⇒≃ ⟩
  ({A B : Type ℓ} → Is-equivalence (≡⇒≃ {A = A} {B = B}))               ↔⟨ Bijection.implicit-Π↔Π ⟩
  ((A {B} : Type ℓ) → Is-equivalence (≡⇒≃ {A = A} {B = B}))             ↝⟨ (∀-cong ext λ _ → from-bijection Bijection.implicit-Π↔Π) ⟩
  ((A B : Type ℓ) → Is-equivalence (≡⇒≃ {A = A} {B = B}))               ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → ∘-sym-preserves-equivalences ext) ⟩
  ((A B : Type ℓ) → Is-equivalence (≡⇒≃ {A = A} {B = B} ∘ sym))         ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ B →
                                                                            Is-equivalence-cong ext (λ B≡A →
      ≡⇒≃ (sym B≡A)                                                           ≡⟨ ≡⇒↝-in-terms-of-subst-sym _ _ ⟩
      subst (_≃ B) (sym (sym B≡A)) Eq.id                                      ≡⟨ cong (flip (subst _) _) $ sym-sym _ ⟩∎
      subst (_≃ B) B≡A Eq.id                                                  ∎)) ⟩

  ((A B : Type ℓ) → Is-equivalence (flip (subst {y = A} (_≃ B)) F.id))  ↔⟨ Π-comm ⟩
  ((B A : Type ℓ) → Is-equivalence (flip (subst {y = A} (_≃ B)) F.id))  ↝⟨ (∀-cong ext λ _ → flip-subst-is-equivalence↔∃-is-contractible ext) ⟩
  ((B : Type ℓ) → Contractible (∃ λ (A : Type ℓ) → A ≃ B))              ↔⟨ inverse Bijection.implicit-Π↔Π ⟩□
  ({B : Type ℓ} → Contractible (∃ λ (A : Type ℓ) → A ≃ B))              □

------------------------------------------------------------------------
-- Some simple lemmas

abstract

  -- "Evaluation rule" for ≡⇒≃.

  ≡⇒≃-refl : ∀ {a} {A : Type a} →
             ≡⇒≃ (refl A) ≡ Eq.id
  ≡⇒≃-refl = ≡⇒↝-refl

  -- "Evaluation rule" for ≡⇒→.

  ≡⇒→-refl : ∀ {a} {A : Type a} →
             ≡⇒→ (refl A) ≡ id
  ≡⇒→-refl = cong _≃_.to ≡⇒≃-refl

  -- "Evaluation rule" for ≡⇒←.

  ≡⇒←-refl : ∀ {a} {A : Type a} →
             ≡⇒← (refl A) ≡ id
  ≡⇒←-refl = cong _≃_.from ≡⇒≃-refl

  -- "Evaluation rule" (?) for ≃⇒≡.

  ≃⇒≡-id : ∀ {a} {A : Type a}
           (univ : Univalence′ A A) →
           ≃⇒≡ univ Eq.id ≡ refl A
  ≃⇒≡-id univ =
    ≃⇒≡ univ Eq.id           ≡⟨ sym $ cong (≃⇒≡ univ) ≡⇒≃-refl ⟩
    ≃⇒≡ univ (≡⇒≃ (refl _))  ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
    refl _                   ∎

  -- A simplification lemma for ≃⇒≡.

  ≡⇒→-≃⇒≡ : ∀ k {ℓ} {A B : Type ℓ} {eq : A ≃ B}
            (univ : Univalence′ A B) →
            to-implication (≡⇒↝ k (≃⇒≡ univ eq)) ≡ _≃_.to eq
  ≡⇒→-≃⇒≡ k {eq = eq} univ =
    to-implication (≡⇒↝ k (≃⇒≡ univ eq))  ≡⟨ to-implication-≡⇒↝ k _ ⟩
    ≡⇒↝ implication (≃⇒≡ univ eq)         ≡⟨ sym $ to-implication-≡⇒↝ equivalence _ ⟩
    ≡⇒→ (≃⇒≡ univ eq)                     ≡⟨ cong _≃_.to (_≃_.right-inverse-of (≡≃≃ univ) _) ⟩∎
    _≃_.to eq                             ∎

------------------------------------------------------------------------
-- Another alternative formulation of univalence

-- Univalence′ A B is pointwise equivalent to CP.Univalence′ A B
-- (assuming extensionality).

Univalence′≃Univalence′-CP :
  ∀ {ℓ} {A B : Type ℓ} →
  Extensionality (lsuc ℓ) (lsuc ℓ) →
  Univalence′ A B ≃ CP.Univalence′ A B
Univalence′≃Univalence′-CP {ℓ = ℓ} {A = A} {B = B} ext =
  Univalence′ A B                         ↝⟨ Univalence′≃Is-equivalence-≡⇒≃ ⟩

  Is-equivalence ≡⇒≃                      ↝⟨ Is-equivalence-cong ext $
                                             elim
                                               (λ A≡B → ≡⇒≃ A≡B ≡ _≃_.from ≃≃≃ (CP.≡⇒≃ A≡B))
                                               (λ C →
      ≡⇒≃ (refl _)                                ≡⟨ ≡⇒≃-refl ⟩
      Eq.id                                       ≡⟨ Eq.lift-equality ext′ (refl _) ⟩
      _≃_.from ≃≃≃ CP.id                          ≡⟨ cong (_≃_.from ≃≃≃) $ sym CP.≡⇒≃-refl ⟩∎
      _≃_.from ≃≃≃ (CP.≡⇒≃ (refl _))              ∎) ⟩

  Is-equivalence (_≃_.from ≃≃≃ ∘ CP.≡⇒≃)  ↝⟨ Eq.⇔→≃
                                               (Eq.propositional ext _)
                                               (Eq.propositional ext _)
                                               (Eq.Two-out-of-three.g-g∘f (Eq.two-out-of-three _ _)
                                                  (_≃_.is-equivalence (inverse ≃≃≃)))
                                               (flip (Eq.Two-out-of-three.f-g (Eq.two-out-of-three _ _))
                                                  (_≃_.is-equivalence (inverse ≃≃≃))) ⟩

  Is-equivalence CP.≡⇒≃                   ↝⟨ Is-equivalence≃Is-equivalence-CP ext ⟩□

  CP.Is-equivalence CP.≡⇒≃                □
  where
  ext′ : Extensionality ℓ ℓ
  ext′ = lower-extensionality _ _ ext

  ≃≃≃ : {A B : Type ℓ} → (A ≃ B) ≃ (A CP.≃ B)
  ≃≃≃ = ≃≃≃-CP ext′

-- Univalence ℓ is pointwise equivalent to CP.Univalence ℓ (assuming
-- extensionality).

Univalence≃Univalence-CP :
  ∀ {ℓ} →
  Extensionality (lsuc ℓ) (lsuc ℓ) →
  Univalence ℓ ≃ CP.Univalence ℓ
Univalence≃Univalence-CP {ℓ = ℓ} ext =
  implicit-∀-cong ext $ implicit-∀-cong ext $
  Univalence′≃Univalence′-CP ext

------------------------------------------------------------------------
-- A consequence: Type is not a set

-- The univalence axiom implies that Type is not a set. (This was
-- pointed out to me by Thierry Coquand.)

module _ (univ : Univalence′ Bool Bool) where

  -- First note that the univalence axiom implies that there is an
  -- inhabitant of Bool ≡ Bool that is not equal to refl.

  swap-as-an-equality : Bool ≡ Bool
  swap-as-an-equality = ≃⇒≡ univ (Eq.↔⇒≃ swap)

  abstract

    swap≢refl : swap-as-an-equality ≢ refl Bool
    swap≢refl =
      swap-as-an-equality ≡ refl _            ↝⟨ cong ≡⇒→ ⟩
      ≡⇒→ swap-as-an-equality ≡ ≡⇒→ (refl _)  ↝⟨ subst (uncurry _≡_) (cong₂ _,_ (≡⇒→-≃⇒≡ equivalence univ) ≡⇒→-refl) ⟩
      not ≡ id                                ↝⟨ cong (_$ false) ⟩
      true ≡ false                            ↝⟨ Bool.true≢false ⟩□
      ⊥                                       □

    -- This implies that Type is not a set.

    ¬-Type-set : ¬ Is-set Type
    ¬-Type-set =
      Is-set Type                      ↝⟨ (λ h → h _ _) ⟩
      swap-as-an-equality ≡ refl Bool  ↝⟨ swap≢refl ⟩□
      ⊥                                □

abstract

  -- The result can be generalised to arbitrary universe levels.

  ¬-Type-set-↑ : ∀ {ℓ} →
                 Univalence′ (↑ ℓ Bool) (↑ ℓ Bool) →
                 ¬ Is-set (Type ℓ)
  ¬-Type-set-↑ {ℓ} univ =
    Is-set (Type ℓ)                          ↝⟨ (λ h → h _ _) ⟩
    swap-as-an-equality-↑ ≡ refl (↑ ℓ Bool)  ↝⟨ swap-↑≢refl ⟩□
    ⊥                                        □
    where
    swap-as-an-equality-↑ : ↑ ℓ Bool ≡ ↑ ℓ Bool
    swap-as-an-equality-↑ =
      ≃⇒≡ univ $
      Eq.↔⇒≃ $
      (Bijection.inverse Bijection.↑↔
         Bijection.∘
       swap
         Bijection.∘
       Bijection.↑↔)

    swap-↑≢refl : swap-as-an-equality-↑ ≢ refl (↑ ℓ Bool)
    swap-↑≢refl =
      swap-as-an-equality-↑ ≡ refl _            ↝⟨ cong ≡⇒→ ⟩
      ≡⇒→ swap-as-an-equality-↑ ≡ ≡⇒→ (refl _)  ↝⟨ subst (uncurry _≡_) (cong₂ _,_ (≡⇒→-≃⇒≡ equivalence univ) ≡⇒→-refl) ⟩
      lift ∘ not ∘ lower ≡ id                   ↝⟨ cong (lower ∘ (_$ lift false)) ⟩
      true ≡ false                              ↝⟨ Bool.true≢false ⟩□
      ⊥                                         □

------------------------------------------------------------------------
-- A consequence: some equality types have infinitely many inhabitants

abstract

  -- Some equality types have infinitely many inhabitants (assuming
  -- univalence).

  equality-can-have-infinitely-many-inhabitants :
    Univalence′ ℕ ℕ →
    ∃ λ (A : Type) → ∃ λ (B : Type) →
    ∃ λ (p : ℕ → A ≡ B) → Injective p
  equality-can-have-infinitely-many-inhabitants univ =
    (ℕ , ℕ , cast ∘ p , cast-preserves-injections p p-injective)
    where
    cast : ℕ ≃ ℕ → ℕ ≡ ℕ
    cast = ≃⇒≡ univ

    cast-preserves-injections :
      {A : Type} (f : A → ℕ ≃ ℕ) →
      Injective f → Injective (cast ∘ f)
    cast-preserves-injections f inj {x = x} {y = y} cast-f-x≡cast-f-y =
      inj (f x               ≡⟨ sym $ _≃_.right-inverse-of (≡≃≃ univ) (f x) ⟩
           ≡⇒≃ (cast (f x))  ≡⟨ cong ≡⇒≃ cast-f-x≡cast-f-y ⟩
           ≡⇒≃ (cast (f y))  ≡⟨ _≃_.right-inverse-of (≡≃≃ univ) (f y) ⟩∎
           f y               ∎)

    swap_and-0 : ℕ → ℕ → ℕ
    swap i and-0 zero    = i
    swap i and-0 (suc n) with i Nat.≟ suc n
    ... | yes i≡1+n = zero
    ... | no  i≢1+n = suc n

    swap∘swap : ∀ i n → swap i and-0 (swap i and-0 n) ≡ n
    swap∘swap zero    zero    = refl zero
    swap∘swap (suc i) zero    with i Nat.≟ i
    ... | yes _   = refl 0
    ... | no  i≢i = ⊥-elim $ i≢i (refl i)
    swap∘swap i       (suc n) with i Nat.≟ suc n
    ... | yes i≡1+n = i≡1+n
    ... | no  i≢1+n with i Nat.≟ suc n
    ...   | yes i≡1+n = ⊥-elim $ i≢1+n i≡1+n
    ...   | no  _     = refl (suc n)

    p : ℕ → ℕ ≃ ℕ
    p i = Eq.↔⇒≃ record
      { surjection = record
        { logical-equivalence = record { to   = swap i and-0
                                       ; from = swap i and-0
                                       }
        ; right-inverse-of    = swap∘swap i
        }
      ; left-inverse-of = swap∘swap i
      }

    p-injective : Injective p
    p-injective {x = i₁} {y = i₂} p-i₁≡p-i₂ =
      i₁               ≡⟨ refl i₁ ⟩
      swap i₁ and-0 0  ≡⟨ cong (λ f → f 0) swap-i₁≡swap-i₂ ⟩
      swap i₂ and-0 0  ≡⟨ refl i₂ ⟩∎
      i₂               ∎
      where
      swap-i₁≡swap-i₂ : swap i₁ and-0 ≡ swap i₂ and-0
      swap-i₁≡swap-i₂ = cong _≃_.to p-i₁≡p-i₂

------------------------------------------------------------------------
-- A consequence: extensionality for functions

-- The transport theorem.

transport-theorem :
  ∀ {p₁ p₂} (P : Type p₁ → Type p₂) →
  (resp : ∀ {A B} → A ≃ B → P A → P B) →
  (∀ {A} (p : P A) → resp Eq.id p ≡ p) →
  ∀ {A B} (univ : Univalence′ A B) →
  (A≃B : A ≃ B) (p : P A) →
  resp A≃B p ≡ subst P (≃⇒≡ univ A≃B) p
transport-theorem P resp resp-id univ A≃B p =
  resp A≃B p              ≡⟨ sym $ cong (λ q → resp q p) (right-inverse-of A≃B) ⟩
  resp (to (from A≃B)) p  ≡⟨ elim (λ {A B} A≡B → ∀ p →
                                     resp (≡⇒≃ A≡B) p ≡ subst P A≡B p)
                                  (λ A p →
                                     resp (≡⇒≃ (refl A)) p  ≡⟨ trans (cong (λ q → resp q p) ≡⇒↝-refl) (resp-id p) ⟩
                                     p                      ≡⟨ sym $ subst-refl P p ⟩∎
                                     subst P (refl A) p     ∎) _ _ ⟩∎
  subst P (from A≃B) p    ∎
  where open _≃_ (≡≃≃ univ)

abstract

  -- If the univalence axiom holds, then any "resp" function that
  -- preserves identity is an equivalence family.

  resp-is-equivalence :
    ∀ {p₁ p₂} (P : Type p₁ → Type p₂) →
    (resp : ∀ {A B} → A ≃ B → P A → P B) →
    (∀ {A} (p : P A) → resp Eq.id p ≡ p) →
    ∀ {A B} (univ : Univalence′ A B) →
    (A≃B : A ≃ B) → Is-equivalence (resp A≃B)
  resp-is-equivalence P resp resp-id univ A≃B =
    Eq.respects-extensional-equality
      (λ p → sym $ transport-theorem P resp resp-id univ A≃B p)
      (Eq.subst-is-equivalence P (≃⇒≡ univ A≃B))

  -- If f is an equivalence, then (non-dependent) precomposition with
  -- f is also an equivalence (assuming univalence).

  precomposition-is-equivalence :
    ∀ {ℓ c} {A B : Type ℓ} {C : Type c} →
    Univalence′ B A → (A≃B : A ≃ B) →
    Is-equivalence (λ (g : B → C) → g ∘ _≃_.to A≃B)
  precomposition-is-equivalence {ℓ} {c} {C = C} univ A≃B =
    resp-is-equivalence P resp refl univ (Eq.inverse A≃B)
    where
    P : Type ℓ → Type (ℓ ⊔ c)
    P X = X → C

    resp : ∀ {A B} → A ≃ B → P A → P B
    resp A≃B p = p ∘ _≃_.from A≃B

-- If h is an equivalence, then one can cancel (non-dependent)
-- precompositions with h (assuming univalence).

precompositions-cancel :
  ∀ {ℓ c} {A B : Type ℓ} {C : Type c} →
  Univalence′ B A → (A≃B : A ≃ B) {f g : B → C} →
  let open _≃_ A≃B in
  f ∘ to ≡ g ∘ to → f ≡ g
precompositions-cancel univ A≃B {f} {g} f∘to≡g∘to =
  f            ≡⟨ sym $ left-inverse-of f ⟩
  from (to f)  ≡⟨ cong from f∘to≡g∘to ⟩
  from (to g)  ≡⟨ left-inverse-of g ⟩∎
  g            ∎
  where open _≃_ (⟨ _ , precomposition-is-equivalence univ A≃B ⟩)

-- Pairs of equal elements.

_²/≡ : ∀ {ℓ} → Type ℓ → Type ℓ
A ²/≡ = ∃ λ (x : A) → ∃ λ (y : A) → x ≡ y

-- The set of such pairs is isomorphic to the underlying type.

-²/≡↔- : ∀ {a} {A : Type a} → (A ²/≡) ↔ A
-²/≡↔- {A = A} =
  (∃ λ (x : A) → ∃ λ (y : A) → x ≡ y)  ↝⟨ ∃-cong (λ _ → _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _)) ⟩
  A × ⊤                                ↝⟨ ×-right-identity ⟩□
  A                                    □

abstract

  -- The univalence axiom implies non-dependent functional
  -- extensionality.

  extensionality :
    ∀ {a b} {A : Type a} {B : Type b} →
    Univalence′ (B ²/≡) B →
    {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
  extensionality {A = A} {B} univ {f} {g} f≡g =
    f          ≡⟨ refl f ⟩
    f′ ∘ pair  ≡⟨ cong (λ (h : B ²/≡ → B) → h ∘ pair) f′≡g′ ⟩
    g′ ∘ pair  ≡⟨ refl g ⟩∎
    g          ∎
    where
    f′ : B ²/≡ → B
    f′ = proj₁

    g′ : B ²/≡ → B
    g′ = proj₁ ∘ proj₂

    f′≡g′ : f′ ≡ g′
    f′≡g′ = precompositions-cancel
              univ
              (Eq.↔⇒≃ $ Bijection.inverse -²/≡↔-)
              (refl id)

    pair : A → B ²/≡
    pair x = (f x , g x , f≡g x)

  -- The univalence axiom implies that contractibility is closed under
  -- Π A.

  Π-closure-contractible :
    ∀ {b} → Univalence′ (Type b ²/≡) (Type b) →
    ∀ {a} {A : Type a} {B : A → Type b} →
    (∀ x → Univalence′ (↑ b ⊤) (B x)) →
    (∀ x → Contractible (B x)) → Contractible ((x : A) → B x)
  Π-closure-contractible {b} univ₁ {A = A} {B} univ₂ contr =
    subst Contractible A→⊤≡[x:A]→Bx →⊤-contractible
    where
    const-⊤≡B : const (↑ b ⊤) ≡ B
    const-⊤≡B = extensionality univ₁ λ x →
      _≃_.from (≡≃≃ (univ₂ x)) $ Eq.↔⇒≃ $
        Bijection.contractible-isomorphic
          (↑-closure 0 ⊤-contractible) (contr x)

    A→⊤≡[x:A]→Bx : (A → ↑ b ⊤) ≡ ((x : A) → B x)
    A→⊤≡[x:A]→Bx = cong (λ X → (x : A) → X x) const-⊤≡B

    →⊤-contractible : Contractible (A → ↑ b ⊤)
    →⊤-contractible = (_ , λ _ → refl _)

  -- Thus we also get extensionality for dependent functions.

  dependent-extensionality′ :
    ∀ {b} → Univalence′ (Type b ²/≡) (Type b) →
    ∀ {a} {A : Type a} →
    (∀ {B : A → Type b} x → Univalence′ (↑ b ⊤) (B x)) →
    {B : A → Type b} → Extensionality′ A B
  dependent-extensionality′ univ₁ univ₂ =
    _⇔_.to Π-closure-contractible⇔extensionality
      (Π-closure-contractible univ₁ univ₂)

  dependent-extensionality :
    ∀ {b} →
    Univalence (lsuc b) →
    Univalence b →
    ∀ {a} → Extensionality a b
  apply-ext (dependent-extensionality univ₁ univ₂) =
    dependent-extensionality′ univ₁ (λ _ → univ₂)

------------------------------------------------------------------------
-- Pow and Fam

-- Slightly different variants of Pow and Fam are described in
-- "Specifying interactions with dependent types" by Peter Hancock and
-- Anton Setzer (in APPSEM Workshop on Subtyping & Dependent Types in
-- Programming, DTP'00). The fact that Pow and Fam are logically
-- equivalent is proved in "Programming Interfaces and Basic Topology"
-- by Peter Hancock and Pierre Hyvernat (Annals of Pure and Applied
-- Logic, 2006). The results may be older than this.

-- Pow.

Pow : ∀ ℓ {a} → Type a → Type (lsuc (a ⊔ ℓ))
Pow ℓ {a} A = A → Type (a ⊔ ℓ)

-- Fam.

Fam : ∀ ℓ {a} → Type a → Type (lsuc (a ⊔ ℓ))
Fam ℓ {a} A = ∃ λ (I : Type (a ⊔ ℓ)) → I → A

-- Pow and Fam are pointwise logically equivalent.

Pow⇔Fam : ∀ ℓ {a} {A : Type a} →
          Pow ℓ A ⇔ Fam ℓ A
Pow⇔Fam _ = record
  { to   = λ P → ∃ P , proj₁
  ; from = λ { (I , f) a → ∃ λ i → f i ≡ a }
  }

-- Pow and Fam are pointwise isomorphic (assuming extensionality and
-- univalence).

Pow↔Fam : ∀ ℓ {a} {A : Type a} →
          Extensionality a (lsuc (a ⊔ ℓ)) →
          Univalence (a ⊔ ℓ) →
          Pow ℓ A ↔ Fam ℓ A
Pow↔Fam ℓ {A = A} ext univ = record
  { surjection = record
    { logical-equivalence = Pow⇔Fam ℓ
    ; right-inverse-of    = λ { (I , f) →
        let lemma₁ =
              (∃ λ a → ∃ λ i → f i ≡ a)  ↔⟨ ∃-comm ⟩
              (∃ λ i → ∃ λ a → f i ≡ a)  ↔⟨ ∃-cong (λ _ → _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _)) ⟩
              I × ⊤                      ↔⟨ ×-right-identity ⟩□
              I                          □

            lemma₂ =
              subst (λ I → I → A) (≃⇒≡ univ lemma₁) proj₁  ≡⟨ sym $ transport-theorem (λ I → I → A) (λ eq → _∘ _≃_.from eq) refl univ _ _ ⟩
              proj₁ ∘ _≃_.from lemma₁                      ≡⟨ refl _ ⟩∎
              f                                            ∎
        in
        (∃ λ a → ∃ λ i → f i ≡ a) , proj₁  ≡⟨ Σ-≡,≡→≡ (≃⇒≡ univ lemma₁) lemma₂ ⟩∎
        I                         , f      ∎ }
    }
  ; left-inverse-of = λ P →
      let lemma = λ a →
            (∃ λ (i : ∃ P) → proj₁ i ≡ a)  ↔⟨ inverse Σ-assoc ⟩
            (∃ λ a′ → P a′ × a′ ≡ a)       ↔⟨ inverse $ ∃-intro _ _ ⟩□
            P a                            □
      in
      (λ a → ∃ λ (i : ∃ P) → proj₁ i ≡ a)  ≡⟨ apply-ext ext (λ a → ≃⇒≡ univ (lemma a)) ⟩∎
      P                                    ∎
  }

-- An isomorphism that follows from Pow↔Fam.
--
-- This isomorphism was suggested to me by Paolo Capriotti.

→↔Σ≃Σ :
  ∀ ℓ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b ⊔ ℓ) (lsuc (a ⊔ b ⊔ ℓ)) →
  Univalence (a ⊔ b ⊔ ℓ) →
  (A → B) ↔ ∃ λ (P : B → Type (a ⊔ b ⊔ ℓ)) → A ≃ Σ B P
→↔Σ≃Σ ℓ {a} {b} {A} {B} ext univ =
  (A → B)                                                    ↝⟨ →-cong₁ (lower-extensionality lzero _ ext) (inverse Bijection.↑↔) ⟩
  (↑ (b ⊔ ℓ) A → B)                                          ↝⟨ inverse ×-left-identity ⟩
  ⊤ × (↑ _ A → B)                                            ↝⟨ inverse $ _⇔_.to contractible⇔↔⊤ (singleton-contractible _) ×-cong F.id ⟩
  (∃ λ (A′ : Type ℓ′) → A′ ≡ ↑ _ A) × (↑ _ A → B)            ↝⟨ inverse Σ-assoc ⟩
  (∃ λ (A′ : Type ℓ′) → A′ ≡ ↑ _ A × (↑ _ A → B))            ↝⟨ (∃-cong λ _ → ∃-cong λ eq → →-cong₁ (lower-extensionality lzero _ ext) (≡⇒≃ (sym eq))) ⟩
  (∃ λ (A′ : Type ℓ′) → A′ ≡ ↑ _ A × (A′ → B))               ↝⟨ (∃-cong λ _ → ×-comm) ⟩
  (∃ λ (A′ : Type ℓ′) → (A′ → B) × A′ ≡ ↑ _ A)               ↝⟨ Σ-assoc ⟩
  (∃ λ (p : ∃ λ (A′ : Type ℓ′) → A′ → B) → proj₁ p ≡ ↑ _ A)  ↝⟨ inverse $ Σ-cong (Pow↔Fam (a ⊔ ℓ) (lower-extensionality ℓ′ lzero ext) univ) (λ _ → F.id) ⟩
  (∃ λ (P : B → Type ℓ′) → ∃ P ≡ ↑ _ A)                      ↔⟨ (∃-cong λ _ → ≡≃≃ univ) ⟩
  (∃ λ (P : B → Type ℓ′) → ∃ P ≃ ↑ _ A)                      ↝⟨ (∃-cong λ _ → Groupoid.⁻¹-bijection (Eq.groupoid (lower-extensionality ℓ′ _ ext))) ⟩
  (∃ λ (P : B → Type ℓ′) → ↑ _ A ≃ ∃ P)                      ↔⟨ (∃-cong λ _ →
                                                                 Eq.≃-preserves (lower-extensionality lzero _ ext) (Eq.↔⇒≃ Bijection.↑↔) F.id) ⟩□
  (∃ λ (P : B → Type ℓ′) → A ≃ ∃ P)                          □
  where
  ℓ′ = a ⊔ b ⊔ ℓ

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

abstract

  -- The univalence axiom is propositional (assuming extensionality).

  Univalence′-propositional :
    ∀ {ℓ} → Extensionality (lsuc ℓ) (lsuc ℓ) →
    {A B : Type ℓ} → Is-proposition (Univalence′ A B)
  Univalence′-propositional ext {A = A} {B = B} =          $⟨ Eq.propositional ext ≡⇒≃ ⟩
    Is-proposition (Is-equivalence (≡⇒≃ {A = A} {B = B}))  ↝⟨ H-level-cong _ 1 (inverse Univalence′≃Is-equivalence-≡⇒≃) ⦂ (_ → _) ⟩□
    Is-proposition (Univalence′ A B)                       □

  Univalence-propositional :
    ∀ {ℓ} → Extensionality (lsuc ℓ) (lsuc ℓ) →
    Is-proposition (Univalence ℓ)
  Univalence-propositional ext =
    implicit-Π-closure ext 1 λ _ →
    implicit-Π-closure ext 1 λ _ →
    Univalence′-propositional ext

  -- ≡⇒≃ commutes with sym/Eq.inverse (assuming extensionality).

  ≡⇒≃-sym :
    ∀ {ℓ} → Extensionality ℓ ℓ →
    {A B : Type ℓ} (A≡B : A ≡ B) →
    ≡⇒≃ (sym A≡B) ≡ Eq.inverse (≡⇒≃ A≡B)
  ≡⇒≃-sym ext = elim¹

    (λ eq → ≡⇒≃ (sym eq) ≡ Eq.inverse (≡⇒≃ eq))

    (≡⇒≃ (sym (refl _))         ≡⟨ cong ≡⇒≃ sym-refl ⟩
     ≡⇒≃ (refl _)               ≡⟨ ≡⇒≃-refl ⟩
     Eq.id                      ≡⟨ sym $ Groupoid.identity (Eq.groupoid ext) ⟩
     Eq.inverse Eq.id           ≡⟨ cong Eq.inverse $ sym ≡⇒≃-refl ⟩∎
     Eq.inverse (≡⇒≃ (refl _))  ∎)

  -- ≃⇒≡ univ commutes with Eq.inverse/sym (assuming extensionality).

  ≃⇒≡-inverse :
    ∀ {ℓ} (univ : Univalence ℓ) → Extensionality ℓ ℓ →
    {A B : Type ℓ} (A≃B : A ≃ B) →
    ≃⇒≡ univ (Eq.inverse A≃B) ≡ sym (≃⇒≡ univ A≃B)
  ≃⇒≡-inverse univ ext A≃B =
    ≃⇒≡ univ (Eq.inverse A≃B)                   ≡⟨ sym $ cong (λ p → ≃⇒≡ univ (Eq.inverse p)) (_≃_.right-inverse-of (≡≃≃ univ) _) ⟩
    ≃⇒≡ univ (Eq.inverse (≡⇒≃ (≃⇒≡ univ A≃B)))  ≡⟨ cong (≃⇒≡ univ) $ sym $ ≡⇒≃-sym ext _ ⟩
    ≃⇒≡ univ (≡⇒≃ (sym (≃⇒≡ univ A≃B)))         ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
    sym (≃⇒≡ univ A≃B)                          ∎

  -- ≡⇒≃ commutes with trans/_⊚_ (assuming extensionality).

  ≡⇒≃-trans :
    ∀ {ℓ} → Extensionality ℓ ℓ →
    {A B C : Type ℓ} (A≡B : A ≡ B) (B≡C : B ≡ C) →
    ≡⇒≃ (trans A≡B B≡C) ≡ ≡⇒≃ B≡C ⊚ ≡⇒≃ A≡B
  ≡⇒≃-trans ext A≡B = elim¹

    (λ eq → ≡⇒≃ (trans A≡B eq) ≡ ≡⇒≃ eq ⊚ ≡⇒≃ A≡B)

    (≡⇒≃ (trans A≡B (refl _))  ≡⟨ cong ≡⇒≃ $ trans-reflʳ _ ⟩
     ≡⇒≃ A≡B                   ≡⟨ sym $ Groupoid.left-identity (Eq.groupoid ext) _ ⟩
     Eq.id ⊚ ≡⇒≃ A≡B           ≡⟨ sym $ cong (λ eq → eq ⊚ ≡⇒≃ A≡B) ≡⇒≃-refl ⟩∎
     ≡⇒≃ (refl _) ⊚ ≡⇒≃ A≡B    ∎)

  -- ≃⇒≡ univ commutes with _⊚_/flip trans (assuming extensionality).

  ≃⇒≡-∘ :
    ∀ {ℓ} (univ : Univalence ℓ) → Extensionality ℓ ℓ →
    {A B C : Type ℓ} (A≃B : A ≃ B) (B≃C : B ≃ C) →
    ≃⇒≡ univ (B≃C ⊚ A≃B) ≡ trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)
  ≃⇒≡-∘ univ ext A≃B B≃C =
    ≃⇒≡ univ (B≃C ⊚ A≃B)                                  ≡⟨ sym $ cong₂ (λ p q → ≃⇒≡ univ (p ⊚ q)) (_≃_.right-inverse-of (≡≃≃ univ) _)
                                                                                (_≃_.right-inverse-of (≡≃≃ univ) _) ⟩
    ≃⇒≡ univ (≡⇒≃ (≃⇒≡ univ B≃C) ⊚ ≡⇒≃ (≃⇒≡ univ A≃B))    ≡⟨ cong (≃⇒≡ univ) $ sym $ ≡⇒≃-trans ext _ _ ⟩
    ≃⇒≡ univ (≡⇒≃ (trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)))  ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
    trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)                   ∎

  -- A variant of the transport theorem.

  transport-theorem′ :
    ∀ {a p r} {A : Type a}
    (P : A → Type p) (R : A → A → Type r)
    (≡↠R : ∀ {x y} → (x ≡ y) ↠ R x y)
    (resp : ∀ {x y} → R x y → P x → P y) →
    (∀ x p → resp (_↠_.to ≡↠R (refl x)) p ≡ p) →
    ∀ {x y} (r : R x y) (p : P x) →
    resp r p ≡ subst P (_↠_.from ≡↠R r) p
  transport-theorem′ P R ≡↠R resp hyp r p =
    resp r p              ≡⟨ sym $ cong (λ r → resp r p) (right-inverse-of r) ⟩
    resp (to (from r)) p  ≡⟨ elim (λ {x y} x≡y → ∀ p →
                                     resp (_↠_.to ≡↠R x≡y) p ≡ subst P x≡y p)
                                  (λ x p →
                                     resp (_↠_.to ≡↠R (refl x)) p  ≡⟨ hyp x p ⟩
                                     p                             ≡⟨ sym $ subst-refl P p ⟩∎
                                     subst P (refl x) p            ∎) _ _ ⟩∎
    subst P (from r) p    ∎
    where open _↠_ ≡↠R

  -- Simplification (?) lemma for transport-theorem′.

  transport-theorem′-refl :
    ∀ {a p r} {A : Type a}
    (P : A → Type p) (R : A → A → Type r)
    (≡≃R : ∀ {x y} → (x ≡ y) ≃ R x y)
    (resp : ∀ {x y} → R x y → P x → P y) →
    (resp-refl : ∀ x p → resp (_≃_.to ≡≃R (refl x)) p ≡ p) →
    ∀ {x} (p : P x) →
    transport-theorem′ P R (_≃_.surjection ≡≃R) resp resp-refl
                       (_≃_.to ≡≃R (refl x)) p ≡
    trans (trans (resp-refl x p) (sym $ subst-refl P p))
          (sym $ cong (λ eq → subst P eq p)
                      (_≃_.left-inverse-of ≡≃R (refl x)))
  transport-theorem′-refl P R ≡≃R resp resp-refl {x} p =

    let body = λ x p → trans (resp-refl x p) (sym $ subst-refl P p)

        lemma =
          trans (sym $ cong (λ r → resp (to r) p) $ refl (refl x))
                (elim (λ {x y} x≡y →
                         ∀ p → resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
                      (λ x p → trans (resp-refl x p)
                                     (sym $ subst-refl P p))
                      (refl x) p)                                        ≡⟨ cong₂ (λ q r → trans q (r p))
                                                                                (sym $ cong-sym (λ r → resp (to r) p) _)
                                                                                (elim-refl (λ {x y} x≡y → ∀ p →
                                                                                resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p) _) ⟩
          trans (cong (λ r → resp (to r) p) $ sym $ refl (refl x))
                (body x p)                                               ≡⟨ cong (λ q → trans (cong (λ r → resp (to r) p) q) (body x p))
                                                                                sym-refl ⟩
          trans (cong (λ r → resp (to r) p) $ refl (refl x)) (body x p)  ≡⟨ cong (λ q → trans q (body x p)) $
                                                                                cong-refl (λ r → resp (to r) p) ⟩
          trans (refl (resp (to (refl x)) p)) (body x p)                 ≡⟨ trans-reflˡ _ ⟩

          body x p                                                       ≡⟨ sym $ trans-reflʳ _ ⟩

          trans (body x p) (refl (subst P (refl x) p))                   ≡⟨ cong (trans (body x p)) $ sym $
                                                                                cong-refl (λ eq → subst P eq p) ⟩
          trans (body x p)
                (cong (λ eq → subst P eq p) (refl (refl x)))             ≡⟨ cong (trans (body x p) ∘ cong (λ eq → subst P eq p)) $
                                                                                sym sym-refl ⟩
          trans (body x p)
                (cong (λ eq → subst P eq p) (sym (refl (refl x))))       ≡⟨ cong (trans (body x p)) $ cong-sym (λ eq → subst P eq p) _ ⟩∎

          trans (body x p)
                (sym $ cong (λ eq → subst P eq p) (refl (refl x)))       ∎
    in

    trans (sym $ cong (λ r → resp r p) $ right-inverse-of (to (refl x)))
          (elim (λ {x y} x≡y →
                   ∀ p → resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
                body (from (to (refl x))) p)                              ≡⟨ cong (λ eq → trans (sym $ cong (λ r → resp r p) eq)
                                                                                (elim (λ {x y} x≡y → ∀ p →
                                                                                resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
                                                                                body (from (to (refl x))) p)) $
                                                                                sym $ left-right-lemma (refl x) ⟩
    trans (sym $ cong (λ r → resp r p) $ cong to $
             left-inverse-of (refl x))
          (elim (λ {x y} x≡y →
                   ∀ p → resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
                body (from (to (refl x))) p)                              ≡⟨ cong (λ eq → trans (sym eq)
                                                                                (elim (λ {x y} x≡y → ∀ p →
                                                                                resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
                                                                                body (from (to (refl x))) p)) $
                                                                                cong-∘ (λ r → resp r p) to _ ⟩
    trans (sym $ cong (λ r → resp (to r) p) $ left-inverse-of (refl x))
          (elim (λ {x y} x≡y →
                   ∀ p → resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
                body (from (to (refl x))) p)                              ≡⟨ elim₁ (λ {q} eq → trans (sym $ cong (λ r → resp (to r) p) eq)
                                                                                (elim (λ {x y} x≡y → ∀ p →
                                                                                resp (_≃_.to ≡≃R x≡y) p ≡
                                                                                subst P x≡y p)
                                                                                body q p) ≡
                                                                                trans (body x p)
                                                                                (sym $ cong (λ eq → subst P eq p) eq))
                                                                                lemma
                                                                                (left-inverse-of (refl x)) ⟩∎

    trans (body x p)
          (sym $ cong (λ eq → subst P eq p) (left-inverse-of (refl x)))   ∎

    where open _≃_ ≡≃R

  -- Simplification (?) lemma for transport-theorem.

  transport-theorem-≡⇒≃-refl :
    ∀ {p₁ p₂} (P : Type p₁ → Type p₂)
    (resp : ∀ {A B} → A ≃ B → P A → P B)
    (resp-id : ∀ {A} (p : P A) → resp Eq.id p ≡ p)
    (univ : Univalence p₁) {A} (p : P A) →
    transport-theorem P resp resp-id univ (≡⇒≃ (refl A)) p ≡
    trans (trans (trans (cong (λ eq → resp eq p) ≡⇒≃-refl)
                    (resp-id p))
             (sym $ subst-refl P p))
      (sym $ cong (λ eq → subst P eq p)
                  (_≃_.left-inverse-of (≡≃≃ univ) (refl A)))
  transport-theorem-≡⇒≃-refl P resp resp-id univ {A} p =
    transport-theorem′-refl P _≃_ (≡≃≃ univ) resp
      (λ _ p → trans (cong (λ eq → resp eq p) ≡⇒≃-refl) (resp-id p)) p

  -- A variant of resp-is-equivalence.

  resp-is-equivalence′ :
    ∀ {a p r} {A : Type a}
    (P : A → Type p) (R : A → A → Type r)
    (≡↠R : ∀ {x y} → (x ≡ y) ↠ R x y)
    (resp : ∀ {x y} → R x y → P x → P y) →
    (∀ x p → resp (_↠_.to ≡↠R (refl x)) p ≡ p) →
    ∀ {x y} (r : R x y) → Is-equivalence (resp r)
  resp-is-equivalence′ P R ≡↠R resp hyp r =
    Eq.respects-extensional-equality
      (λ p → sym $ transport-theorem′ P R ≡↠R resp hyp r p)
      (Eq.subst-is-equivalence P (_↠_.from ≡↠R r))

  -- A lemma relating ≃⇒≡, →-cong and cong₂.

  ≃⇒≡-→-cong :
    ∀ {ℓ} {A₁ A₂ B₁ B₂ : Type ℓ}
    (ext : Extensionality ℓ ℓ) →
    (univ : Univalence ℓ)
    (A₁≃A₂ : A₁ ≃ A₂) (B₁≃B₂ : B₁ ≃ B₂) →
    ≃⇒≡ univ (→-cong ext A₁≃A₂ B₁≃B₂) ≡
      cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂) (≃⇒≡ univ B₁≃B₂)
  ≃⇒≡-→-cong {A₂ = A₂} {B₁} ext univ A₁≃A₂ B₁≃B₂ =
    ≃⇒≡ univ (→-cong ext A₁≃A₂ B₁≃B₂)                        ≡⟨ cong (≃⇒≡ univ) (Eq.lift-equality ext lemma) ⟩

    ≃⇒≡ univ (≡⇒≃ (cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂)
                                         (≃⇒≡ univ B₁≃B₂)))  ≡⟨ left-inverse-of (≡≃≃ univ) _ ⟩∎

    cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂) (≃⇒≡ univ B₁≃B₂)  ∎
    where
    open _≃_

    lemma :
      (λ f → to B₁≃B₂ ∘ f ∘ from A₁≃A₂) ≡
      to (≡⇒≃ (cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂)
                                     (≃⇒≡ univ B₁≃B₂)))
    lemma =
      (λ f → to B₁≃B₂ ∘ f ∘ from A₁≃A₂)                  ≡⟨ apply-ext ext (λ _ → transport-theorem (λ B → A₂ → B) (λ A≃B g → _≃_.to A≃B ∘ g)
                                                                                refl univ B₁≃B₂ _) ⟩
      subst (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂) ∘
      (λ f → f ∘ from A₁≃A₂)                             ≡⟨ cong (_∘_ (subst (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂))) (apply-ext ext λ f →
                                                              transport-theorem (λ A → A → B₁) (λ A≃B g → g ∘ _≃_.from A≃B) refl univ A₁≃A₂ f) ⟩
      subst (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂) ∘
      subst (λ A → A → B₁) (≃⇒≡ univ A₁≃A₂)              ≡⟨ cong₂ (λ g h f → g (h f))
                                                              (apply-ext ext $ subst-in-terms-of-≡⇒↝ equivalence _ (λ B → A₂ → B))
                                                              (apply-ext ext $ subst-in-terms-of-≡⇒↝ equivalence _ (λ A → A → B₁)) ⟩
      to (≡⇒≃ (cong (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂))) ∘
      to (≡⇒≃ (cong (λ A → A → B₁) (≃⇒≡ univ A₁≃A₂)))    ≡⟨⟩

      to (≡⇒≃ (cong (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂)) ⊚
          ≡⇒≃ (cong (λ A → A → B₁) (≃⇒≡ univ A₁≃A₂)))    ≡⟨ cong to $ sym $ ≡⇒≃-trans ext _ _ ⟩∎

      to (≡⇒≃ (cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂)
                                     (≃⇒≡ univ B₁≃B₂)))  ∎

  -- One can sometimes push cong through ≃⇒≡ (assuming
  -- extensionality).

  cong-≃⇒≡ :
    ∀ {ℓ p} {A B : Type ℓ} {A≃B : A ≃ B} →
    Extensionality p p →
    (univ₁ : Univalence ℓ)
    (univ₂ : Univalence p)
    (P : Type ℓ → Type p)
    (P-cong : ∀ {A B} → A ≃ B → P A ≃ P B) →
    (∀ {A} (p : P A) → _≃_.to (P-cong Eq.id) p ≡ p) →
    cong P (≃⇒≡ univ₁ A≃B) ≡ ≃⇒≡ univ₂ (P-cong A≃B)
  cong-≃⇒≡ {A≃B = A≃B} ext univ₁ univ₂ P P-cong P-cong-id =
    cong P (≃⇒≡ univ₁ A≃B)                    ≡⟨ sym $ _≃_.left-inverse-of (≡≃≃ univ₂) _ ⟩
    ≃⇒≡ univ₂ (≡⇒≃ (cong P (≃⇒≡ univ₁ A≃B)))  ≡⟨ cong (≃⇒≡ univ₂) $ Eq.lift-equality ext lemma ⟩∎
    ≃⇒≡ univ₂ (P-cong A≃B)                    ∎
    where
    lemma : ≡⇒→ (cong P (≃⇒≡ univ₁ A≃B)) ≡ _≃_.to (P-cong A≃B)
    lemma = apply-ext ext λ x →
      ≡⇒→ (cong P (≃⇒≡ univ₁ A≃B)) x  ≡⟨ sym $ subst-in-terms-of-≡⇒↝ equivalence _ P x ⟩
      subst P (≃⇒≡ univ₁ A≃B) x       ≡⟨ sym $ transport-theorem P (_≃_.to ∘ P-cong) P-cong-id univ₁ A≃B x ⟩∎
      _≃_.to (P-cong A≃B) x           ∎

  -- Any "resp" function that preserves identity also preserves
  -- compositions (assuming univalence and extensionality).

  resp-preserves-compositions :
    ∀ {p₁ p₂} (P : Type p₁ → Type p₂) →
    (resp : ∀ {A B} → A ≃ B → P A → P B) →
    (∀ {A} (p : P A) → resp Eq.id p ≡ p) →
    Univalence p₁ → Extensionality p₁ p₁ →
    ∀ {A B C} (A≃B : A ≃ B) (B≃C : B ≃ C) p →
    resp (B≃C ⊚ A≃B) p ≡ (resp B≃C ∘ resp A≃B) p
  resp-preserves-compositions P resp resp-id univ ext A≃B B≃C p =
    resp (B≃C ⊚ A≃B) p                                 ≡⟨ transport-theorem P resp resp-id univ _ _ ⟩
    subst P (≃⇒≡ univ (B≃C ⊚ A≃B)) p                   ≡⟨ cong (λ eq → subst P eq p) $ ≃⇒≡-∘ univ ext A≃B B≃C ⟩
    subst P (trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)) p    ≡⟨ sym $ subst-subst P _ _ _ ⟩
    subst P (≃⇒≡ univ B≃C) (subst P (≃⇒≡ univ A≃B) p)  ≡⟨ sym $ transport-theorem P resp resp-id univ _ _ ⟩
    resp B≃C (subst P (≃⇒≡ univ A≃B) p)                ≡⟨ sym $ cong (resp _) $ transport-theorem P resp resp-id univ _ _ ⟩∎
    resp B≃C (resp A≃B p)                              ∎

  -- Any "resp" function that preserves identity also preserves
  -- inverses (assuming univalence and extensionality).

  resp-preserves-inverses :
    ∀ {p₁ p₂} (P : Type p₁ → Type p₂) →
    (resp : ∀ {A B} → A ≃ B → P A → P B) →
    (∀ {A} (p : P A) → resp Eq.id p ≡ p) →
    Univalence p₁ → Extensionality p₁ p₁ →
    ∀ {A B} (A≃B : A ≃ B) p q →
    resp A≃B p ≡ q → resp (inverse A≃B) q ≡ p
  resp-preserves-inverses P resp resp-id univ ext A≃B p q eq =
    let lemma =
          q                                     ≡⟨ sym eq ⟩
          resp A≃B p                            ≡⟨ transport-theorem P resp resp-id univ _ _ ⟩
          subst P (≃⇒≡ univ A≃B) p              ≡⟨ cong (λ eq → subst P eq p) $ sym $ sym-sym _ ⟩∎
          subst P (sym (sym (≃⇒≡ univ A≃B))) p  ∎
    in

    resp (inverse A≃B) q                                                 ≡⟨ transport-theorem P resp resp-id univ _ _ ⟩
    subst P (≃⇒≡ univ (inverse A≃B)) q                                   ≡⟨ cong (λ eq → subst P eq q) $ ≃⇒≡-inverse univ ext A≃B ⟩
    subst P (sym (≃⇒≡ univ A≃B)) q                                       ≡⟨ cong (subst P (sym (≃⇒≡ univ A≃B))) lemma ⟩
    subst P (sym (≃⇒≡ univ A≃B)) (subst P (sym (sym (≃⇒≡ univ A≃B))) p)  ≡⟨ subst-subst-sym P _ _ ⟩∎
    p                                                                    ∎

-- Equality preserves equivalences (assuming extensionality and
-- univalence).

≡-preserves-≃ :
  ∀ {ℓ₁ ℓ₂}
    {A₁ : Type ℓ₁} {A₂ : Type ℓ₂} {B₁ : Type ℓ₁} {B₂ : Type ℓ₂} →
  Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂) →
  Univalence′ A₁ B₁ →
  Univalence′ A₂ B₂ →
  A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ ≡ B₁) ≃ (A₂ ≡ B₂)
≡-preserves-≃ {ℓ₁} {ℓ₂} {A₁} {A₂} {B₁} {B₂}
              ext univ₁ univ₂ A₁≃A₂ B₁≃B₂ = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  })
  where
  to = λ A₁≡B₁ → ≃⇒≡ univ₂ (
    A₂  ↝⟨ inverse A₁≃A₂ ⟩
    A₁  ↝⟨ ≡⇒≃ A₁≡B₁ ⟩
    B₁  ↝⟨ B₁≃B₂ ⟩□
    B₂  □)

  from = λ A₂≡B₂ → ≃⇒≡ univ₁ (
    A₁  ↝⟨ A₁≃A₂ ⟩
    A₂  ↝⟨ ≡⇒≃ A₂≡B₂ ⟩
    B₂  ↝⟨ inverse B₁≃B₂ ⟩□
    B₁  □)

  abstract

    to∘from : ∀ eq → to (from eq) ≡ eq
    to∘from A₂≡B₂ =
      let ext₂ = lower-extensionality ℓ₁ ℓ₁ ext in

      _≃_.to (Eq.≃-≡ (≡≃≃ univ₂)) (Eq.lift-equality ext₂ (

        ≡⇒→ (≃⇒≡ univ₂ ((B₁≃B₂ ⊚ ≡⇒≃ (≃⇒≡ univ₁ ((inverse B₁≃B₂ ⊚
                             ≡⇒≃ A₂≡B₂) ⊚ A₁≃A₂))) ⊚ inverse A₁≃A₂))  ≡⟨ cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ₂) _ ⟩

        (_≃_.to B₁≃B₂ ∘
         ≡⇒→ (≃⇒≡ univ₁ ((inverse B₁≃B₂ ⊚ ≡⇒≃ A₂≡B₂) ⊚ A₁≃A₂)) ∘
         _≃_.from A₁≃A₂)                                              ≡⟨ cong (λ eq → _≃_.to B₁≃B₂ ∘ _≃_.to eq ∘ _≃_.from A₁≃A₂) $
                                                                           _≃_.right-inverse-of (≡≃≃ univ₁) _ ⟩
        ((_≃_.to B₁≃B₂ ∘ _≃_.from B₁≃B₂) ∘ ≡⇒→ A₂≡B₂ ∘
         (_≃_.to A₁≃A₂ ∘ _≃_.from A₁≃A₂))                             ≡⟨ cong₂ (λ f g → f ∘ ≡⇒→ A₂≡B₂ ∘ g)
                                                                               (apply-ext ext₂ $ _≃_.right-inverse-of B₁≃B₂)
                                                                               (apply-ext ext₂ $ _≃_.right-inverse-of A₁≃A₂) ⟩∎
        ≡⇒→ A₂≡B₂                                                     ∎))

    from∘to : ∀ eq → from (to eq) ≡ eq
    from∘to A₁≡B₁ =
      let ext₁ = lower-extensionality ℓ₂ ℓ₂ ext in

      _≃_.to (Eq.≃-≡ (≡≃≃ univ₁)) (Eq.lift-equality ext₁ (

        ≡⇒→ (≃⇒≡ univ₁ ((inverse B₁≃B₂ ⊚ ≡⇒≃ (≃⇒≡ univ₂ ((B₁≃B₂ ⊚
                             ≡⇒≃ A₁≡B₁) ⊚ inverse A₁≃A₂))) ⊚ A₁≃A₂))  ≡⟨ cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ₁) _ ⟩

        (_≃_.from B₁≃B₂ ∘
         ≡⇒→ (≃⇒≡ univ₂ ((B₁≃B₂ ⊚ ≡⇒≃ A₁≡B₁) ⊚ inverse A₁≃A₂)) ∘
         _≃_.to A₁≃A₂)                                                ≡⟨ cong (λ eq → _≃_.from B₁≃B₂ ∘ _≃_.to eq ∘ _≃_.to A₁≃A₂) $
                                                                           _≃_.right-inverse-of (≡≃≃ univ₂) _ ⟩
        ((_≃_.from B₁≃B₂ ∘ _≃_.to B₁≃B₂) ∘ ≡⇒→ A₁≡B₁ ∘
         (_≃_.from A₁≃A₂ ∘ _≃_.to A₁≃A₂))                             ≡⟨ cong₂ (λ f g → f ∘ ≡⇒→ A₁≡B₁ ∘ g)
                                                                               (apply-ext ext₁ $ _≃_.left-inverse-of B₁≃B₂)
                                                                               (apply-ext ext₁ $ _≃_.left-inverse-of A₁≃A₂) ⟩∎
        ≡⇒→ A₁≡B₁                                                     ∎))

-- Singletons expressed using equivalences instead of equalities,
-- where the types are required to live in the same universe, are
-- contractible (assuming univalence).

singleton-with-≃-contractible :
  ∀ {b} {B : Type b} →
  Univalence b →
  Contractible (∃ λ (A : Type b) → A ≃ B)
singleton-with-≃-contractible univ =
  H-level.respects-surjection
    (∃-cong λ _ → _≃_.surjection (≡≃≃ univ))
    0
    (singleton-contractible _)

other-singleton-with-≃-contractible :
  ∀ {a} {A : Type a} →
  Univalence a →
  Contractible (∃ λ (B : Type a) → A ≃ B)
other-singleton-with-≃-contractible univ =
  H-level.respects-surjection
    (∃-cong λ _ → _≃_.surjection (≡≃≃ univ))
    0
    (other-singleton-contractible _)

-- Singletons expressed using equivalences instead of equalities are
-- isomorphic to the unit type (assuming extensionality and
-- univalence).

singleton-with-≃-↔-⊤ :
  ∀ {a b} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Univalence (a ⊔ b) →
  (∃ λ (A : Type (a ⊔ b)) → A ≃ B) ↔ ⊤
singleton-with-≃-↔-⊤ {a} {B = B} ext univ =
  (∃ λ A → A ≃ B)      ↝⟨ inverse (∃-cong λ _ → Eq.≃-preserves-bijections ext F.id Bijection.↑↔) ⟩
  (∃ λ A → A ≃ ↑ a B)  ↔⟨ inverse (∃-cong λ _ → ≡≃≃ univ) ⟩
  (∃ λ A → A ≡ ↑ a B)  ↝⟨ _⇔_.to contractible⇔↔⊤ (singleton-contractible _) ⟩□
  ⊤                    □

other-singleton-with-≃-↔-⊤ :
  ∀ {a b} {A : Type a} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Univalence (a ⊔ b) →
  (∃ λ (B : Type (a ⊔ b)) → A ≃ B) ↔ ⊤
other-singleton-with-≃-↔-⊤ {b = b} {A} ext univ =
  (∃ λ B → A ≃ B)  ↝⟨ (∃-cong λ _ → Eq.inverse-isomorphism ext) ⟩
  (∃ λ B → B ≃ A)  ↝⟨ singleton-with-≃-↔-⊤ {a = b} ext univ ⟩□
  ⊤                □

-- Variants of the two lemmas above.

singleton-with-Π-≃-≃-⊤ :
  ∀ {a q} {A : Type a} {Q : A → Type q} →
  Extensionality a (lsuc q) →
  Univalence q →
  (∃ λ (P : A → Type q) → ∀ x → P x ≃ Q x) ≃ ⊤
singleton-with-Π-≃-≃-⊤ {a = a} {q = q} {A = A} {Q = Q} ext univ =
  (∃ λ (P : A → Type q) → ∀ x → P x ≃ Q x)  ↝⟨ (inverse $ ∃-cong λ _ → ∀-cong ext λ _ → ≡≃≃ univ) ⟩
  (∃ λ (P : A → Type q) → ∀ x → P x ≡ Q x)  ↝⟨ (∃-cong λ _ → Eq.extensionality-isomorphism ext) ⟩
  (∃ λ (P : A → Type q) → P ≡ Q)            ↔⟨ _⇔_.to contractible⇔↔⊤ (singleton-contractible _) ⟩□
  ⊤                                         □

other-singleton-with-Π-≃-≃-⊤ :
  ∀ {a p} {A : Type a} {P : A → Type p} →
  Extensionality a (lsuc p) →
  Univalence p →
  (∃ λ (Q : A → Type p) → ∀ x → P x ≃ Q x) ≃ ⊤
other-singleton-with-Π-≃-≃-⊤ {a = a} {p = p} {A = A} {P = P} ext univ =
  (∃ λ (Q : A → Type p) → ∀ x → P x ≃ Q x)  ↝⟨ (inverse $ ∃-cong λ _ → ∀-cong ext λ _ → ≡≃≃ univ) ⟩
  (∃ λ (Q : A → Type p) → ∀ x → P x ≡ Q x)  ↝⟨ (∃-cong λ _ → Eq.extensionality-isomorphism ext) ⟩
  (∃ λ (Q : A → Type p) → P ≡ Q)            ↔⟨ _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _) ⟩□
  ⊤                                         □

-- ∃ Contractible is isomorphic to the unit type (assuming
-- extensionality and univalence).

∃Contractible↔⊤ :
  ∀ {a} →
  Extensionality a a →
  Univalence a →
  (∃ λ (A : Type a) → Contractible A) ↔ ⊤
∃Contractible↔⊤ ext univ =
  (∃ λ A → Contractible A)  ↝⟨ (∃-cong λ _ → contractible↔≃⊤ ext) ⟩
  (∃ λ A → A ≃ ⊤)           ↝⟨ singleton-with-≃-↔-⊤ ext univ ⟩
  ⊤                         □

-- If two types have a certain h-level, then the type of equalities
-- between these types also has the given h-level (assuming
-- extensionality and univalence).

H-level-H-level-≡ :
  ∀ {a} {A₁ A₂ : Type a} →
  Extensionality a a →
  Univalence′ A₁ A₂ →
  ∀ n → H-level n A₁ → H-level n A₂ → H-level n (A₁ ≡ A₂)
H-level-H-level-≡ {A₁ = A₁} {A₂} ext univ n = curry (
  H-level n A₁ × H-level n A₂  ↝⟨ uncurry (Eq.h-level-closure ext n) ⟩
  H-level n (A₁ ≃ A₂)          ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) n ⟩
  H-level n (A₁ ≡ A₂)          □)

-- If a type has a certain positive h-level, then the types of
-- equalities between this type and other types also has the given
-- h-level (assuming extensionality and univalence).

H-level-H-level-≡ˡ :
  ∀ {a} {A₁ A₂ : Type a} →
  Extensionality a a →
  Univalence′ A₁ A₂ →
  ∀ n → H-level (1 + n) A₁ → H-level (1 + n) (A₁ ≡ A₂)
H-level-H-level-≡ˡ {A₁ = A₁} {A₂} ext univ n =
  H-level (1 + n) A₁         ↝⟨ Eq.left-closure ext n ⟩
  H-level (1 + n) (A₁ ≃ A₂)  ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) (1 + n) ⟩
  H-level (1 + n) (A₁ ≡ A₂)  □

H-level-H-level-≡ʳ :
  ∀ {a} {A₁ A₂ : Type a} →
  Extensionality a a →
  Univalence′ A₁ A₂ →
  ∀ n → H-level (1 + n) A₂ → H-level (1 + n) (A₁ ≡ A₂)
H-level-H-level-≡ʳ {A₁ = A₁} {A₂} ext univ n =
  H-level (1 + n) A₂         ↝⟨ Eq.right-closure ext n ⟩
  H-level (1 + n) (A₁ ≃ A₂)  ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) (1 + n) ⟩
  H-level (1 + n) (A₁ ≡ A₂)  □

-- ∃ λ A → H-level n A has h-level 1 + n (assuming extensionality and
-- univalence).

∃-H-level-H-level-1+ :
  ∀ {a} →
  Extensionality a a →
  Univalence a →
  ∀ n → H-level (1 + n) (∃ λ (A : Type a) → H-level n A)
∃-H-level-H-level-1+ ext univ n = ≡↔+ _ _ λ { (A₁ , h₁) (A₂ , h₂) →
                                     $⟨ h₁ , h₂ ⟩
  H-level n A₁ × H-level n A₂        ↝⟨ uncurry (H-level-H-level-≡ ext univ n) ⟩
  H-level n (A₁ ≡ A₂)                ↝⟨ H-level.respects-surjection
                                          (_↔_.surjection $ ignore-propositional-component
                                                              (H-level-propositional ext _)) n ⟩□
  H-level n ((A₁ , h₁) ≡ (A₂ , h₂))  □ }

-- ∃ λ A → Is-proposition A is a set (assuming extensionality and
-- propositional extensionality).

Is-set-∃-Is-proposition :
  ∀ {a} →
  Extensionality (lsuc a) (lsuc a) →
  Propositional-extensionality a →
  Is-set (∃ λ (A : Type a) → Is-proposition A)
Is-set-∃-Is-proposition {a} ext prop-ext
                        {x = A₁ , A₁-prop} {y = A₂ , A₂-prop} =
                                                    $⟨ _≃_.to (Propositional-extensionality-is-univalence-for-propositions ext)
                                                            prop-ext A₁-prop A₂-prop ⟩
  Univalence′ A₁ A₂                                 ↝⟨ (λ univ → H-level-H-level-≡ ext′ univ 1 A₁-prop A₂-prop) ⟩
  Is-proposition (A₁ ≡ A₂)                          ↝⟨ H-level.respects-surjection
                                                         (_↔_.surjection $ ignore-propositional-component
                                                                             (H-level-propositional ext′ 1)) 1 ⟩□
  Is-proposition ((A₁ , A₁-prop) ≡ (A₂ , A₂-prop))  □
  where
  ext′ = lower-extensionality _ _ ext

-- ∃ λ A → H-level n A does not in general have h-level n.
--
-- (Kraus and Sattler show that, for all n,
-- ∃ λ (A : Set (# n)) → H-level (2 + n) A does not have h-level
-- 2 + n, assuming univalence. See "Higher Homotopies in a Hierarchy
-- of Univalent Universes".)

¬-∃-H-level-H-level :
  ∀ {a} →
  ∃ λ n → ¬ H-level n (∃ λ (A : Type a) → H-level n A)
¬-∃-H-level-H-level =
  1 ,
  ( Is-proposition (∃ λ A → Is-proposition A)               ↔⟨⟩
    ((p q : ∃ λ A → Is-proposition A) → p ≡ q)              ↝⟨ (λ f p q → cong proj₁ (f p q)) ⟩
    ((p q : ∃ λ A → Is-proposition A) → proj₁ p ≡ proj₁ q)  ↝⟨ (_$ (⊥ , ⊥-propositional)) ∘
                                                               (_$ (↑ _ ⊤ , ↑-closure 1 (mono₁ 0 ⊤-contractible))) ⟩
    ↑ _ ⊤ ≡ ⊥                                               ↝⟨ flip (subst id) _ ⟩
    ⊥                                                       ↝⟨ ⊥-elim ⟩□
    ⊥₀                                                      □)

-- A certain type of uninhabited types is isomorphic to the unit type
-- (assuming extensionality and univalence).

∃¬↔⊤ :
  ∀ {a} →
  Extensionality a a →
  Univalence a →
  (∃ λ (A : Type a) → ¬ A) ↔ ⊤
∃¬↔⊤ ext univ =
  (∃ λ A → ¬ A)     ↔⟨ inverse (∃-cong λ _ → ≃⊥≃¬ ext) ⟩
  (∃ λ A → A ≃ ⊥₀)  ↔⟨ singleton-with-≃-↔-⊤ ext univ ⟩
  ⊤                 □

-- The following three proofs are taken from or variants of proofs in
-- "Higher Homotopies in a Hierarchy of Univalent Universes" by Kraus
-- and Sattler (Section 3).

-- There is a function which, despite having the same type, is not
-- equal to a certain instance of reflexivity (assuming extensionality
-- and univalence).

∃≢refl :
  Extensionality (# 1) (# 1) →
  Univalence (# 0) →
  ∃ λ (A : Type₁) → ∃ λ (f : (x : A) → x ≡ x) → f ≢ refl
∃≢refl ext univ =
    (∃ λ (A : Type) → A ≡ A)
  , _↔_.from iso f
  , (_↔_.from iso f ≡ refl                                      ↝⟨ cong (_↔_.to iso) ⟩

     _↔_.to iso (_↔_.from iso f) ≡ _↔_.to iso refl              ↝⟨ (λ eq → f                            ≡⟨ sym (_↔_.right-inverse-of iso f) ⟩
                                                                           _↔_.to iso (_↔_.from iso f)  ≡⟨ eq ⟩∎
                                                                           _↔_.to iso refl              ∎) ⟩
     f ≡ _↔_.to iso refl                                        ↝⟨ cong (λ f → proj₁ (f Bool (swap-as-an-equality univ))) ⟩

     swap-as-an-equality univ ≡ proj₁ (_↔_.to iso refl Bool _)  ↝⟨ (λ eq → swap-as-an-equality univ        ≡⟨ eq ⟩
                                                                           proj₁ (_↔_.to iso refl Bool _)  ≡⟨ cong proj₁ Σ-≡,≡←≡-refl ⟩∎
                                                                           refl Bool                       ∎) ⟩

     swap-as-an-equality univ ≡ refl Bool                       ↝⟨ swap≢refl univ ⟩□

     ⊥                                                          □)
  where
  f = λ A p → p , refl (trans p p)

  iso =
    ((p : ∃ λ A → A ≡ A) → p ≡ p)                      ↝⟨ currying ⟩

    (∀ A (p : A ≡ A) → (A , p) ≡ (A , p))              ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                             inverse $ Bijection.Σ-≡,≡↔≡ {a = # 1}) ⟩
    ((A : Type) (p : A ≡ A) →
       ∃ λ (q : A ≡ A) → subst (λ A → A ≡ A) q p ≡ p)  ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                             ∃-cong λ _ → ≡⇒↝ _ [subst≡]≡[trans≡trans]) ⟩□
    ((A : Type) (p : A ≡ A) →
       ∃ λ (q : A ≡ A) → trans p q ≡ trans q p)        □

-- The type (a : A) → a ≡ a is not necessarily a proposition (assuming
-- extensionality and univalence).

¬-type-of-refl-propositional :
  Extensionality (# 1) (# 1) →
  Univalence (# 0) →
  ∃ λ (A : Type₁) → ¬ Is-proposition ((a : A) → a ≡ a)
¬-type-of-refl-propositional ext univ =
  let A , f , f≢refl = ∃≢refl ext univ in
  A ,
  (Is-proposition (∀ x → x ≡ x)  ↝⟨ (λ irr → irr _ _) ⟩
   f ≡ refl                      ↝⟨ f≢refl ⟩□
   ⊥                             □)

-- Type₁ does not have h-level 3 (assuming extensionality and
-- univalence).

¬-Type₁-groupoid :
  Extensionality (# 1) (# 1) →
  Univalence (# 1) →
  Univalence (# 0) →
  ¬ H-level 3 Type₁
¬-Type₁-groupoid ext univ₁ univ₀ =
  let L = _ in

  H-level 3 Type₁                       ↝⟨ (λ h → h) ⟩
  Is-set (L ≡ L)                        ↝⟨ H-level.respects-surjection (_≃_.surjection $ ≡≃≃ univ₁) 2 ⟩
  Is-set (L ≃ L)                        ↝⟨ (λ h → h) ⟩
  Is-proposition (F.id ≡ F.id)          ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ Eq.≃-as-Σ) 1 ⟩
  Is-proposition ((id , _) ≡ (id , _))  ↝⟨ H-level.respects-surjection
                                             (_↔_.surjection $ inverse $ ignore-propositional-component (Eq.propositional ext id)) 1 ⟩
  Is-proposition (id ≡ id)              ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ Eq.extensionality-isomorphism ext) 1 ⟩
  Is-proposition ((l : L) → l ≡ l)      ↝⟨ proj₂ $ ¬-type-of-refl-propositional ext univ₀ ⟩□
  ⊥                                     □

-- For propositional types there is a split surjection from equality
-- to logical equivalence (assuming univalence).

≡↠⇔ : ∀ {ℓ} {A B : Type ℓ} →
      Univalence′ A B →
      Is-proposition A → Is-proposition B →
      (A ≡ B) ↠ (A ⇔ B)
≡↠⇔ {A = A} {B} univ A-prop B-prop =
  A ≡ B  ↔⟨ ≡≃≃ univ ⟩
  A ≃ B  ↝⟨ Eq.≃↠⇔ A-prop B-prop ⟩□
  A ⇔ B  □

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

⇔↔≡ : ∀ {ℓ} {A B : Type ℓ} →
      Extensionality ℓ ℓ →
      Univalence′ A B →
      Is-proposition A → Is-proposition B →
      (A ⇔ B) ↔ (A ≡ B)
⇔↔≡ {A = A} {B} ext univ A-prop B-prop =
  A ⇔ B  ↝⟨ Eq.⇔↔≃ ext A-prop B-prop ⟩
  A ≃ B  ↔⟨ inverse $ ≡≃≃ univ ⟩□
  A ≡ B  □

-- A variant of the previous statement.

⇔↔≡′ : ∀ {ℓ} {A B : Proposition ℓ} →
       Extensionality ℓ ℓ →
       Univalence′ (proj₁ A) (proj₁ B) →
       (proj₁ A ⇔ proj₁ B) ↔ (A ≡ B)
⇔↔≡′ {A = A} {B} ext univ =
  proj₁ A ⇔ proj₁ B  ↝⟨ ⇔↔≡ ext univ (proj₂ A) (proj₂ B) ⟩
  proj₁ A ≡ proj₁ B  ↝⟨ ignore-propositional-component (H-level-propositional ext 1) ⟩□
  A ≡ B              □

-- A variant of the previous statement.

⇔↔≡″ : ∀ {ℓ} {A B : Proposition ℓ} →
       Extensionality (lsuc ℓ) (lsuc ℓ) →
       Propositional-extensionality ℓ →
       (proj₁ A ⇔ proj₁ B) ↔ (A ≡ B)
⇔↔≡″ {ℓ} {A} {B} ext =
  Propositional-extensionality ℓ   ↝⟨ (λ prop-ext → _≃_.to (Propositional-extensionality-is-univalence-for-propositions ext)
                                                           prop-ext (proj₂ A) (proj₂ B)) ⟩
  Univalence′ (proj₁ A) (proj₁ B)  ↝⟨ ⇔↔≡′ (lower-extensionality _ _ ext) ⟩□
  (proj₁ A ⇔ proj₁ B) ↔ (A ≡ B)    □

------------------------------------------------------------------------
-- Variants of J for equivalences

-- Two variants of the J rule for equivalences, along with
-- "computation" rules.
--
-- The types of the eliminators are similar to the statement of
-- Corollary 5.8.5 from the HoTT book (where the motive takes two type
-- arguments). The type and code of ≃-elim₁ are based on code from the
-- cubical library written by Matthew Yacavone, which was possibly
-- based on code written by Anders Mörtberg.

≃-elim₁ :
  ∀ {ℓ p} {A B : Type ℓ} →
  Univalence ℓ →
  (P : {A : Type ℓ} → A ≃ B → Type p) →
  P (Eq.id {A = B}) →
  (A≃B : A ≃ B) → P A≃B
≃-elim₁ univ P p A≃B =
  subst
    (λ (_ , A≃B) → P A≃B)
    (mono₁ 0 (singleton-with-≃-contractible univ) _ _)
    p

≃-elim₁-id :
  ∀ {ℓ p} {B : Type ℓ}
  (univ : Univalence ℓ)
  (P : {A : Type ℓ} → A ≃ B → Type p)
  (p : P (Eq.id {A = B})) →
  ≃-elim₁ univ P p Eq.id ≡ p
≃-elim₁-id univ P p =
  subst
    (λ (_ , A≃B) → P A≃B)
    (mono₁ 0 (singleton-with-≃-contractible univ) _ _)
    p                                                   ≡⟨ cong (λ eq → subst (λ (_ , A≃B) → P A≃B) eq _) $
                                                           mono₁ 1 (mono₁ 0 (singleton-with-≃-contractible univ)) _ _ ⟩

  subst (λ (_ , A≃B) → P A≃B) (refl _) p                ≡⟨ subst-refl _ _ ⟩∎

  p                                                     ∎

≃-elim¹ :
  ∀ {ℓ p} {A B : Type ℓ} →
  Univalence ℓ →
  (P : {B : Type ℓ} → A ≃ B → Type p) →
  P (Eq.id {A = A}) →
  (A≃B : A ≃ B) → P A≃B
≃-elim¹ univ P p A≃B =
  subst
    (λ (_ , A≃B) → P A≃B)
    (mono₁ 0 (other-singleton-with-≃-contractible univ) _ _)
    p

≃-elim¹-id :
  ∀ {ℓ p} {A : Type ℓ}
  (univ : Univalence ℓ)
  (P : {B : Type ℓ} → A ≃ B → Type p)
  (p : P (Eq.id {A = A})) →
  ≃-elim¹ univ P p Eq.id ≡ p
≃-elim¹-id univ P p =
  subst
    (λ (_ , A≃B) → P A≃B)
    (mono₁ 0 (other-singleton-with-≃-contractible univ) _ _)
    p                                                         ≡⟨ cong (λ eq → subst (λ (_ , A≃B) → P A≃B) eq _) $
                                                                 mono₁ 1 (mono₁ 0 (other-singleton-with-≃-contractible univ)) _ _ ⟩

  subst (λ (_ , A≃B) → P A≃B) (refl _) p                      ≡⟨ subst-refl _ _ ⟩∎

  p                                                           ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module lib.groups.Groups where

open import lib.groups.CommutingSquare public
open import lib.groups.FreeAbelianGroup public
open import lib.groups.FreeGroup public
open import lib.groups.GroupProduct public
open import lib.groups.Homomorphism public
open import lib.groups.HomotopyGroup public
open import lib.groups.Int public
open import lib.groups.Isomorphism public
open import lib.groups.Lift public
open import lib.groups.LoopSpace public
open import lib.groups.QuotientGroup public
open import lib.groups.PullbackGroup public
open import lib.groups.Subgroup public
open import lib.groups.SubgroupProp public
open import lib.groups.TruncationGroup public
open import lib.groups.Unit public

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
A : Set₁
A = Set

{-# POLARITY A #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Float where

open import Agda.Builtin.Bool
open import Agda.Builtin.Int
open import Agda.Builtin.Maybe
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
open import Agda.Builtin.Word

postulate Float : Set
{-# BUILTIN FLOAT Float #-}

primitive
  -- Relations
  primFloatInequality        : Float → Float → Bool
  primFloatEquality          : Float → Float → Bool
  primFloatLess              : Float → Float → Bool
  primFloatIsInfinite        : Float → Bool
  primFloatIsNaN             : Float → Bool
  primFloatIsNegativeZero    : Float → Bool
  primFloatIsSafeInteger     : Float → Bool
  -- Conversions
  primFloatToWord64          : Float → Word64
  primNatToFloat             : Nat → Float
  primIntToFloat             : Int → Float
  primFloatRound             : Float → Maybe Int
  primFloatFloor             : Float → Maybe Int
  primFloatCeiling           : Float → Maybe Int
  primFloatToRatio           : Float → (Σ Int λ _ → Int)
  primRatioToFloat           : Int → Int → Float
  primFloatDecode            : Float → Maybe (Σ Int λ _ → Int)
  primFloatEncode            : Int → Int → Maybe Float
  primShowFloat              : Float → String
  -- Operations
  primFloatPlus              : Float → Float → Float
  primFloatMinus             : Float → Float → Float
  primFloatTimes             : Float → Float → Float
  primFloatDiv               : Float → Float → Float
  primFloatPow               : Float → Float → Float
  primFloatNegate            : Float → Float
  primFloatSqrt              : Float → Float
  primFloatExp               : Float → Float
  primFloatLog               : Float → Float
  primFloatSin               : Float → Float
  primFloatCos               : Float → Float
  primFloatTan               : Float → Float
  primFloatASin              : Float → Float
  primFloatACos              : Float → Float
  primFloatATan              : Float → Float
  primFloatATan2             : Float → Float → Float
  primFloatSinh              : Float → Float
  primFloatCosh              : Float → Float
  primFloatTanh              : Float → Float
  primFloatASinh             : Float → Float
  primFloatACosh             : Float → Float
  primFloatATanh             : Float → Float

{-# COMPILE JS
    primFloatRound = function(x) {
        x = agdaRTS._primFloatRound(x);
        if (x === null) {
            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
        }
        else {
            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
        }
    };
#-}
{-# COMPILE JS
    primFloatFloor = function(x) {
        x = agdaRTS._primFloatFloor(x);
        if (x === null) {
            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
        }
        else {
            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
        }
    };
#-}
{-# COMPILE JS
    primFloatCeiling = function(x) {
        x = agdaRTS._primFloatCeiling(x);
        if (x === null) {
            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
        }
        else {
            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
        }
    };
#-}
{-# COMPILE JS
    primFloatToRatio = function(x) {
        x = agdaRTS._primFloatToRatio(x);
        return z_jAgda_Agda_Builtin_Sigma["_,_"](x.numerator)(x.denominator);
    };
#-}
{-# COMPILE JS
    primFloatDecode = function(x) {
        x = agdaRTS._primFloatDecode(x);
        if (x === null) {
            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
        }
        else {
            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](
                z_jAgda_Agda_Builtin_Sigma["_,_"](x.mantissa)(x.exponent));
        }
    };
#-}
{-# COMPILE JS
    primFloatEncode = function(x) {
        return function (y) {
            x = agdaRTS.uprimFloatEncode(x, y);
            if (x === null) {
                return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
            }
            else {
                return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
            }
        }
    };
#-}

primFloatNumericalEquality = primFloatEquality
{-# WARNING_ON_USAGE primFloatNumericalEquality
"Warning: primFloatNumericalEquality was deprecated in Agda v2.6.2.
Please use primFloatEquality instead."
#-}

primFloatNumericalLess = primFloatLess
{-# WARNING_ON_USAGE primFloatNumericalLess
"Warning: primFloatNumericalLess was deprecated in Agda v2.6.2.
Please use primFloatLess instead."
#-}

primRound = primFloatRound
{-# WARNING_ON_USAGE primRound
"Warning: primRound was deprecated in Agda v2.6.2.
Please use primFloatRound instead."
#-}

primFloor = primFloatFloor
{-# WARNING_ON_USAGE primFloor
"Warning: primFloor was deprecated in Agda v2.6.2.
Please use primFloatFloor instead."
#-}

primCeiling = primFloatCeiling
{-# WARNING_ON_USAGE primCeiling
"Warning: primCeiling was deprecated in Agda v2.6.2.
Please use primFloatCeiling instead."
#-}

primExp = primFloatExp
{-# WARNING_ON_USAGE primExp
"Warning: primExp was deprecated in Agda v2.6.2.
Please use primFloatExp instead."
#-}

primLog = primFloatLog
{-# WARNING_ON_USAGE primLog
"Warning: primLog was deprecated in Agda v2.6.2.
Please use primFloatLog instead."
#-}

primSin = primFloatSin
{-# WARNING_ON_USAGE primSin
"Warning: primSin was deprecated in Agda v2.6.2.
Please use primFloatSin instead."
#-}

primCos = primFloatCos
{-# WARNING_ON_USAGE primCos
"Warning: primCos was deprecated in Agda v2.6.2.
Please use primFloatCos instead."
#-}

primTan = primFloatTan
{-# WARNING_ON_USAGE primTan
"Warning: primTan was deprecated in Agda v2.6.2.
Please use primFloatTan instead."
#-}

primASin = primFloatASin
{-# WARNING_ON_USAGE primASin
"Warning: primASin was deprecated in Agda v2.6.2.
Please use primFloatASin instead."
#-}

primACos = primFloatACos
{-# WARNING_ON_USAGE primACos
"Warning: primACos was deprecated in Agda v2.6.2.
Please use primFloatACos instead."
#-}

primATan = primFloatATan
{-# WARNING_ON_USAGE primATan
"Warning: primATan was deprecated in Agda v2.6.2.
Please use primFloatATan instead."
#-}

primATan2 = primFloatATan2
{-# WARNING_ON_USAGE primATan2
"Warning: primATan2 was deprecated in Agda v2.6.2.
Please use primFloatATan2 instead."
#-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Issue4 where

postulate
  D    : Set
  _≡_  : D → D → Set
  refl : ∀ {a} → a ≡ a
  P    : D → Set

-- We test the translation of a definition where we need to erase proof terms.
foo : ∀ {a} → P a → ∀ {b} → P b → a ≡ a
foo {a} Pa {b} Pb = bar
  where
  c : D
  c = a
  {-# ATP definition c #-}

  postulate bar : c ≡ a
  {-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module WarningOnUsage where

id : {A : Set} → A → A
id x = x

-- Deprecated names

λx→x = id

{-# WARNING_ON_USAGE λx→x "DEPRECATED: Use `id` instead of `λx→x`" #-}

open import Agda.Builtin.Equality

_ : {A : Set} {x : A} → λx→x x ≡ x
_ = refl

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Morphisms between algebraic structures
------------------------------------------------------------------------

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

module Algebra.Morphism where

import Algebra.Morphism.Definitions as MorphismDefinitions
open import Relation.Binary
open import Algebra
import Algebra.Properties.Group as GroupP
open import Function
open import Level
import Relation.Binary.Reasoning.Setoid as EqR

private
  variable
    a b ℓ₁ ℓ₂ : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
--

module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) where
  open MorphismDefinitions A B _≈_ public

open import Algebra.Morphism.Structures public

------------------------------------------------------------------------
-- Bundle homomorphisms

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : Semigroup c₁ ℓ₁)
         (To   : Semigroup c₂ ℓ₂) where

  private
    module F = Semigroup From
    module T = Semigroup To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsSemigroupMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
      ∙-homo  : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_

  IsSemigroupMorphism-syntax = IsSemigroupMorphism
  syntax IsSemigroupMorphism-syntax From To F = F Is From -Semigroup⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : Monoid c₁ ℓ₁)
         (To   : Monoid c₂ ℓ₂) where

  private
    module F = Monoid From
    module T = Monoid To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsMonoidMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      sm-homo : IsSemigroupMorphism F.semigroup T.semigroup ⟦_⟧
      ε-homo  : Homomorphic₀ ⟦_⟧ F.ε T.ε

    open IsSemigroupMorphism sm-homo public

  IsMonoidMorphism-syntax = IsMonoidMorphism
  syntax IsMonoidMorphism-syntax From To F = F Is From -Monoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : CommutativeMonoid c₁ ℓ₁)
         (To   : CommutativeMonoid c₂ ℓ₂) where

  private
    module F = CommutativeMonoid From
    module T = CommutativeMonoid To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

    open IsMonoidMorphism mn-homo public

  IsCommutativeMonoidMorphism-syntax = IsCommutativeMonoidMorphism
  syntax IsCommutativeMonoidMorphism-syntax From To F = F Is From -CommutativeMonoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : IdempotentCommutativeMonoid c₁ ℓ₁)
         (To   : IdempotentCommutativeMonoid c₂ ℓ₂) where

  private
    module F = IdempotentCommutativeMonoid From
    module T = IdempotentCommutativeMonoid To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsIdempotentCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

    open IsMonoidMorphism mn-homo public

    isCommutativeMonoidMorphism :
      IsCommutativeMonoidMorphism F.commutativeMonoid T.commutativeMonoid ⟦_⟧
    isCommutativeMonoidMorphism = record { mn-homo = mn-homo }

  IsIdempotentCommutativeMonoidMorphism-syntax = IsIdempotentCommutativeMonoidMorphism
  syntax IsIdempotentCommutativeMonoidMorphism-syntax From To F = F Is From -IdempotentCommutativeMonoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : Group c₁ ℓ₁)
         (To   : Group c₂ ℓ₂) where

  private
    module F = Group From
    module T = Group To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsGroupMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

    open IsMonoidMorphism mn-homo public

    ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
    ⁻¹-homo x = let open EqR T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin
      ⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩
      ⟦ x F.⁻¹ F.∙ x ⟧     ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩
      ⟦ F.ε ⟧              ≈⟨ ε-homo ⟩
      T.ε ∎

  IsGroupMorphism-syntax = IsGroupMorphism
  syntax IsGroupMorphism-syntax From To F = F Is From -Group⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : AbelianGroup c₁ ℓ₁)
         (To   : AbelianGroup c₂ ℓ₂) where

  private
    module F = AbelianGroup From
    module T = AbelianGroup To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsAbelianGroupMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      gp-homo : IsGroupMorphism F.group T.group ⟦_⟧

    open IsGroupMorphism gp-homo public

  IsAbelianGroupMorphism-syntax = IsAbelianGroupMorphism
  syntax IsAbelianGroupMorphism-syntax From To F = F Is From -AbelianGroup⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : Ring c₁ ℓ₁)
         (To   : Ring c₂ ℓ₂) where

  private
    module F = Ring From
    module T = Ring To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsRingMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      +-abgp-homo : ⟦_⟧ Is F.+-abelianGroup -AbelianGroup⟶ T.+-abelianGroup
      *-mn-homo   : ⟦_⟧ Is F.*-monoid -Monoid⟶ T.*-monoid

  IsRingMorphism-syntax = IsRingMorphism
  syntax IsRingMorphism-syntax From To F = F Is From -Ring⟶ To


text:
module Issue1760b where

-- Skipping an old-style mutual block: Somewhere within a `mutual`
-- block before a record definition.
mutual
  data D : Set where
    lam : (D → D) → D

  {-# NO_POSITIVITY_CHECK #-}
  record U : Set where
    field ap : U → U

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Mutual2 where

data Bool
  : Set
  where

  false
    : Bool

  true
    : Bool

data ℕ
  : Set
  where

  zero
    : ℕ

  suc
    : ℕ
    → ℕ

is-even
  : ℕ
  → Bool

is-odd
  : ℕ
  → Bool

is-even zero
  = true
is-even (suc n)
  = is-odd n

is-odd zero
  = false
is-odd (suc n)
  = is-even n

is-even'
  : ℕ
  → Bool
is-even'
  = is-even

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


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

open import Level

-- Kan Complexes
--
-- These are technically "Algebraic" Kan Complexes, as they come with a choice of fillers
-- However, this notion is far easier than the more geometric flavor,
-- as we can sidestep questions about choice.

module Categories.Category.Construction.KanComplex (o ℓ : Level) where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin; inject₁)

open import Categories.Category using (Category)

open import Categories.Category.Instance.SimplicialSet using (SimplicialSet)
open import Categories.Category.Instance.SimplicialSet.Properties o ℓ using (ΔSet; Δ[_]; Λ[_,_]; Λ-inj)

open Category (SimplicialSet o ℓ)

-- A Kan complex is a simplicial set where every k-horn has a filler.
record IsKanComplex (X : ΔSet) : Set (o ⊔ ℓ) where
  field
    filler      : ∀ {n} {k} → Λ[ n , k ] ⇒ X → Δ[ n ] ⇒ X
    filler-cong : ∀ {n} {k} → {f g : Λ[ n , k ] ⇒ X} → f ≈ g → filler {n} f ≈ filler g
    is-filler   : ∀ {n} {k} → (f : Λ[ n , k ] ⇒ X) → filler f ∘ Λ-inj k ≈ f

-- 'inner k' will embed 'k : Fin n' into the "inner" portion of 'Fin (n + 2)'
-- Visually, it looks a little something like:
--
--   * * *
--   | | |
--   v v v
-- * * * * *
--
-- Note that this is set up in such a way that we can normalize
-- as far as possible without pattern matching on 'i' in proofs.
inner : ∀ {n} → Fin n → Fin (ℕ.suc (ℕ.suc n))
inner i = Fin.suc (inject₁ i)

-- A Weak Kan complex is similar to a Kan Complex, but where only "inner horns" have fillers.
--
-- The indexing here is tricky, but it lets us avoid extra proof conditions that the horn is an inner horn.
-- The basic idea is that if we want an n-dimensional inner horn, then we only want to allow the faces {1,2,3...n-1}
-- to be missing. We could do this by requiring proofs that the missing face is greater than 0 and less than n, but
-- this makes working with the definition _extremely_ difficult.
--
-- To avoid this, we only allow an missing face index that ranges from 0 to n-2, and then embed that index
-- into the full range of face indexes via 'inner'. This does require us to shift our indexes around a bit.
-- To make this indexing more obvious, we use the suggestively named variable 'n-2'.
record IsWeakKanComplex (X : ΔSet) : Set (o ⊔ ℓ) where
  field
    filler      : ∀ {n-2} {k : Fin n-2} → Λ[ ℕ.suc (ℕ.suc n-2) , inner k ] ⇒ X → Δ[ ℕ.suc (ℕ.suc n-2) ] ⇒ X
    filler-cong : ∀ {n-2} {k : Fin n-2} → {f g : Λ[ ℕ.suc (ℕ.suc n-2) , inner k ] ⇒ X} → f ≈ g → filler f ≈ filler g
    is-filler   : ∀ {n-2} {k : Fin n-2} → (f : Λ[ ℕ.suc (ℕ.suc n-2) , inner k ] ⇒ X) → filler f ∘ Λ-inj (inner k) ≈ f

KanComplex⇒WeakKanComplex : ∀ {X} → IsKanComplex X → IsWeakKanComplex X
KanComplex⇒WeakKanComplex complex = record { IsKanComplex complex }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
import      Lvl
open import Structure.Setoid
open import Type

module Automaton.Deterministic.Finite where

open import Automaton.Deterministic
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.List renaming (∅ to ε ; _⊰_ to _·_)
open import Data.List.Setoid
open import Data.List.Functions using (postpend ; _++_)
open import Data.List.Proofs
open import Functional
open import Logic.Propositional
open import Logic
open import Sets.ExtensionalPredicateSet using (PredSet ; intro ; _∈_ ; _∋_ ; ⊶ ; [∋]-binaryRelator)
import      Structure.Function.Names as Names
open import Structure.Operator
open import Structure.Relator.Properties
open import Type.Size.Finite

private variable ℓₚ ℓₛ ℓₑ₁ ℓₐ ℓₑ₂ : Lvl.Level

module _
  {ℓₚ}
  (State : Type{ℓₛ}) ⦃ equiv-state : Equiv{ℓₑ₁}(State) ⦄
  (Alphabet : Type{ℓₐ}) ⦃ equiv-alphabet : Equiv{ℓₑ₂}(Alphabet) ⦄
  where

  record DFA : Type{ℓₛ Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓₑ₂ Lvl.⊔ ℓₐ Lvl.⊔ Lvl.𝐒(ℓₚ)} where
    field
      ⦃ State-finite ⦄ : Finite(State)
      ⦃ Alphabet-finite ⦄ : Finite(Alphabet)
      automata : Deterministic{ℓₚ = ℓₚ}(State)(Alphabet)
    open Deterministic(automata) hiding (transitionedAutomaton ; wordTransitionedAutomaton) public

    transitionedAutomaton : Alphabet → DFA
    transitionedAutomaton c = record{automata = Deterministic.transitionedAutomaton(automata) c}

    wordTransitionedAutomaton : Word → DFA
    wordTransitionedAutomaton w = record{automata = Deterministic.wordTransitionedAutomaton(automata) w}

    postulate isFinal : State → Bool
    postulate isFinal-correctness : ∀{s} → IsTrue(isFinal s) ↔ (s ∈ Final)

    isWordAccepted : Word → Bool
    isWordAccepted(w) = isFinal(wordTransition(start)(w))

  pattern dfa {fin-Q} {fin-Σ} δ {δ-op} q₀ F = record{State-finite = fin-Q ; Alphabet-finite = fin-Σ ; automata = deterministic δ ⦃ δ-op ⦄ q₀ F}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Andreas, 2017-05-13, issue reported by nad

module Issue2579 where

open import Common.Bool

open import Issue2579.Import
import Issue2579.Instance Bool true as I
-- without the "as I" the instance is not in scope
-- (and you get a parse error)

theWrapped : {{w : Wrap Bool}} → Bool
theWrapped {{w}} = Wrap.wrapped w

test : Bool
test = theWrapped


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue248 where

open import Common.Level

data ⊥ : Set where

-- This type checks:

Foo : ⊥ → (l : Level) → Set
Foo x l with x
Foo x l | ()

-- This didn't (but now it does):

Bar : ⊥ → (l : Level) → Set l → Set
Bar x l A with x
Bar x l A | ()

-- Bug.agda:25,1-15
-- ⊥ !=< Level of type Set
-- when checking that the expression w has type Level


text:
module Structure.Operator.Vector.LinearMaps where

open import Functional
open import Function.Proofs
open import Logic.Predicate
import      Lvl
open import Structure.Function
open import Structure.Function.Multi
open import Structure.Operator.Properties
open import Structure.Operator.Vector.LinearMap
open import Structure.Operator.Vector.Proofs
open import Structure.Operator.Vector
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓᵥ ℓᵥₗ ℓᵥᵣ ℓᵥ₁ ℓᵥ₂ ℓᵥ₃ ℓₛ ℓᵥₑ ℓᵥₑₗ ℓᵥₑᵣ ℓᵥₑ₁ ℓᵥₑ₂ ℓᵥₑ₃ ℓₛₑ : Lvl.Level
private variable V Vₗ Vᵣ V₁ V₂ V₃ S : Type{ℓ}
private variable _+ᵥ_ _+ᵥₗ_ _+ᵥᵣ_ _+ᵥ₁_ _+ᵥ₂_ _+ᵥ₃_ : V → V → V
private variable _⋅ₛᵥ_ _⋅ₛᵥₗ_ _⋅ₛᵥᵣ_ _⋅ₛᵥ₁_ _⋅ₛᵥ₂_ _⋅ₛᵥ₃_ : S → V → V
private variable _+ₛ_ _⋅ₛ_ : S → S → S
private variable f g : Vₗ → Vᵣ

open VectorSpace ⦃ … ⦄

module _
  ⦃ equiv-Vₗ : Equiv{ℓᵥₑₗ}(Vₗ) ⦄
  ⦃ equiv-Vᵣ : Equiv{ℓᵥₑᵣ}(Vᵣ) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpaceₗ : VectorSpace{V = Vₗ}{S = S}(_+ᵥₗ_)(_⋅ₛᵥₗ_)(_+ₛ_)(_⋅ₛ_))
  (vectorSpaceᵣ : VectorSpace{V = Vᵣ}{S = S}(_+ᵥᵣ_)(_⋅ₛᵥᵣ_)(_+ₛ_)(_⋅ₛ_))
  where

  instance _ = vectorSpaceₗ
  instance _ = vectorSpaceᵣ

  zero : LinearMap(vectorSpaceₗ)(vectorSpaceᵣ)(const 𝟎ᵥ)
  Preserving.proof (LinearMap.preserves-[+ᵥ] zero) {x} {y} =
    const 𝟎ᵥ (x +ᵥₗ y)            🝖[ _≡_ ]-[]
    𝟎ᵥ                            🝖[ _≡_ ]-[ identityₗ(_+ᵥᵣ_)(𝟎ᵥ) ]-sym
    𝟎ᵥ +ᵥᵣ 𝟎ᵥ                     🝖[ _≡_ ]-[]
    (const 𝟎ᵥ x) +ᵥᵣ (const 𝟎ᵥ y) 🝖-end
  Preserving.proof (LinearMap.preserves-[⋅ₛᵥ] zero {s}) {x} =
    const 𝟎ᵥ (s ⋅ₛᵥₗ x) 🝖[ _≡_ ]-[]
    𝟎ᵥ                  🝖[ _≡_ ]-[ [⋅ₛᵥ]-absorberᵣ ]-sym
    s ⋅ₛᵥᵣ 𝟎ᵥ           🝖[ _≡_ ]-[]
    s ⋅ₛᵥᵣ (const 𝟎ᵥ x) 🝖-end

module _
  ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpace : VectorSpace{V = V}{S = S}(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_))
  where

  instance _ = vectorSpace

  identity : LinearOperator(vectorSpace)(id)
  Preserving.proof (LinearMap.preserves-[+ᵥ]  identity) = reflexivity(_≡_)
  Preserving.proof (LinearMap.preserves-[⋅ₛᵥ] identity) = reflexivity(_≡_)

module _
  ⦃ equiv-V₁ : Equiv{ℓᵥₑ₁}(V₁) ⦄
  ⦃ equiv-V₂ : Equiv{ℓᵥₑ₂}(V₂) ⦄
  ⦃ equiv-V₂ : Equiv{ℓᵥₑ₃}(V₃) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpace₁ : VectorSpace{V = V₁}{S = S}(_+ᵥ₁_)(_⋅ₛᵥ₁_)(_+ₛ_)(_⋅ₛ_))
  (vectorSpace₂ : VectorSpace{V = V₂}{S = S}(_+ᵥ₂_)(_⋅ₛᵥ₂_)(_+ₛ_)(_⋅ₛ_))
  (vectorSpace₃ : VectorSpace{V = V₃}{S = S}(_+ᵥ₃_)(_⋅ₛᵥ₃_)(_+ₛ_)(_⋅ₛ_))
  where

  instance _ = vectorSpace₁
  instance _ = vectorSpace₂
  instance _ = vectorSpace₃

  compose : LinearMap(vectorSpace₂)(vectorSpace₃)(f) → LinearMap(vectorSpace₁)(vectorSpace₂)(g) → LinearMap(vectorSpace₁)(vectorSpace₃)(f ∘ g)
  LinearMap.function (compose {f} {g} F G) = [∘]-function {f = f}{g = g}
  Preserving.proof (LinearMap.preserves-[+ᵥ] (compose {f} {g} F G)) {x}{y} =
    (f ∘ g)(x +ᵥ₁ y)          🝖[ _≡_ ]-[]
    f(g(x +ᵥ₁ y))             🝖[ _≡_ ]-[ congruence₁(f) (preserving₂(g) (_+ᵥ₁_)(_+ᵥ₂_)) ]
    f(g(x) +ᵥ₂ g(y))          🝖[ _≡_ ]-[ preserving₂(f) (_+ᵥ₂_)(_+ᵥ₃_) ]
    f(g(x)) +ᵥ₃ f(g(y))       🝖[ _≡_ ]-[]
    (f ∘ g)(x) +ᵥ₃ (f ∘ g)(y) 🝖-end
  Preserving.proof (LinearMap.preserves-[⋅ₛᵥ] (compose {f} {g} F G) {s}) {v} =
    (f ∘ g) (s ⋅ₛᵥ₁ v) 🝖[ _≡_ ]-[]
    f(g(s ⋅ₛᵥ₁ v))     🝖[ _≡_ ]-[ congruence₁(f) (preserving₁(g) (s ⋅ₛᵥ₁_)(s ⋅ₛᵥ₂_)) ]
    f(s ⋅ₛᵥ₂ g(v))     🝖[ _≡_ ]-[ preserving₁(f) (s ⋅ₛᵥ₂_)(s ⋅ₛᵥ₃_) ]
    s ⋅ₛᵥ₃ f(g(v))     🝖[ _≡_ ]-[]
    s ⋅ₛᵥ₃ (f ∘ g)(v)  🝖-end

module _ ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄ {_+ₛ_ _⋅ₛ_ : S → S → S} where
  private variable A B C : VectorSpaceVObject {ℓᵥ}{_}{ℓᵥₑ}{ℓₛₑ} ⦃ equiv-S ⦄ (_+ₛ_)(_⋅ₛ_)
  open VectorSpaceVObject hiding (𝟎ᵥ)

  𝟎ˡⁱⁿᵉᵃʳᵐᵃᵖ : A →ˡⁱⁿᵉᵃʳᵐᵃᵖ B
  𝟎ˡⁱⁿᵉᵃʳᵐᵃᵖ {A = A}{B = B} = [∃]-intro (const 𝟎ᵥ) ⦃ zero (vectorSpace A) (vectorSpace B) ⦄

  idˡⁱⁿᵉᵃʳᵐᵃᵖ : A →ˡⁱⁿᵉᵃʳᵐᵃᵖ A
  idˡⁱⁿᵉᵃʳᵐᵃᵖ {A = A} = [∃]-intro id ⦃ identity(vectorSpace A) ⦄

  _∘ˡⁱⁿᵉᵃʳᵐᵃᵖ_ : let _ = A in (B →ˡⁱⁿᵉᵃʳᵐᵃᵖ C) → (A →ˡⁱⁿᵉᵃʳᵐᵃᵖ B) → (A →ˡⁱⁿᵉᵃʳᵐᵃᵖ C)
  _∘ˡⁱⁿᵉᵃʳᵐᵃᵖ_ {A = A}{B = B}{C = C} ([∃]-intro f ⦃ linmap-f ⦄) ([∃]-intro g ⦃ linmap-g ⦄) = [∃]-intro (f ∘ g) ⦃ compose (vectorSpace A) (vectorSpace B) (vectorSpace C) linmap-f linmap-g ⦄


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Modules.Definition
open import Vectors
open import Sets.EquivalenceRelations
open import Sets.FinSet.Definition
open import Modules.Span
open import Groups.Definition

module Modules.VectorModule {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open import Rings.Definition
open import Rings.Lemmas R
open import Groups.Vector (Ring.additiveGroup R)
open Ring R
open Group additiveGroup
open Setoid S
open Equivalence eq

ringModule : {n : ℕ} → Module R (abelianVectorGroup {n = n} abelianUnderlyingGroup) λ a v → vecMap (_* a) v
Module.dotWellDefined (ringModule) {r} {s} {[]} {[]} r=s t=u = record {}
Module.dotWellDefined (ringModule) {r} {s} {t ,- ts} {u ,- us} r=s (t=u ,, ts=us) = Ring.*WellDefined R t=u r=s ,, Module.dotWellDefined (ringModule) {r} {s} {ts} {us} r=s ts=us
Module.dotDistributesLeft (ringModule) {a} {[]} {[]} = record {}
Module.dotDistributesLeft (ringModule) {a} {y ,- ys} {z ,- zs} = Ring.*DistributesOver+' R ,, Module.dotDistributesLeft (ringModule) {a} {ys} {zs}
Module.dotDistributesRight (ringModule) {a} {b} {[]} = record {}
Module.dotDistributesRight (ringModule) {a} {b} {z ,- zs} = Ring.*DistributesOver+ R ,, Module.dotDistributesRight (ringModule) {a} {b} {zs}
Module.dotAssociative (ringModule) {r} {s} {[]} = record {}
Module.dotAssociative (ringModule) {r} {s} {x ,- xs} = transitive (Ring.*WellDefined R reflexive (Ring.*Commutative R)) (Ring.*Associative R) ,, Module.dotAssociative (ringModule) {r} {s} {xs}
Module.dotIdentity (ringModule) {[]} = record {}
Module.dotIdentity (ringModule) {x ,- xs} = transitive (Ring.*Commutative R) (Ring.identIsIdent R) ,, Module.dotIdentity ringModule {xs}

vecModuleBasis : {n : ℕ} → FinSet n → Vec A n
vecModuleBasis {succ n} fzero = (Ring.1R R) ,- vecPure (Ring.0R R)
vecModuleBasis {succ n} (fsucc i) = (Ring.0R R) ,- vecModuleBasis i

vecTimesZero : {n : ℕ} (a : A) → vecEquiv {n} (vecMap (_* a) (vecPure 0G)) (vecPure 0G)
vecTimesZero {zero} a = record {}
vecTimesZero {succ n} a = transitive *Commutative timesZero ,, vecTimesZero a

--private
--  lemma2 : {n : ℕ} → (f : _ → _) → (j : _) → vecEquiv (dot ringModule (vecMap (λ i → 0G ,- f i)) j) ?
--  lemma2 = ?

allEntries : (n : ℕ) → Vec (FinSet n) n
allEntries zero = []
allEntries (succ n) = fzero ,- vecMap fsucc (allEntries n)

extractZero : {n m : ℕ} → (y : Vec A m) (xs : Vec (FinSet n) m) (f : FinSet n → Vec A n) → vecEquiv (dot ringModule (vecMap (λ i → 0G ,- f i) xs) y) (0G ,- dot ringModule (vecMap f xs) y)
extractZero {zero} {zero} [] [] f = Equivalence.reflexive (Setoid.eq (vectorSetoid _))
extractZero {zero} {succ m} (y ,- ys) (() ,- xs) f
extractZero {succ n} {zero} [] [] f = reflexive ,, (reflexive ,, Equivalence.reflexive (Setoid.eq (vectorSetoid _)))
extractZero {succ n} {succ m} (y ,- ys) (x ,- xs) f = Equivalence.transitive (Setoid.eq (vectorSetoid _)) (Group.+WellDefined vectorGroup (transitive *Commutative timesZero ,, Equivalence.reflexive (Setoid.eq (vectorSetoid _))) (extractZero ys xs f)) (identLeft ,, Equivalence.reflexive (Setoid.eq (vectorSetoid _)))

identityMatrixProduct : {n : ℕ} → (b : Vec A n) → vecEquiv (dot ringModule (vecMap vecModuleBasis (allEntries n)) b) b
identityMatrixProduct [] = record {}
identityMatrixProduct {succ n} (x ,- b) rewrite vecMapCompose fsucc vecModuleBasis (allEntries n) = Equivalence.transitive (Setoid.eq (vectorSetoid _)) (Group.+WellDefined vectorGroup (identIsIdent ,, vecTimesZero x) (extractZero b (allEntries n) vecModuleBasis)) (identRight ,, Equivalence.transitive (Setoid.eq (vectorSetoid _)) (Group.identLeft vectorGroup) (identityMatrixProduct b))

rearrangeBasis : {n : ℕ} → (coeffs : Vec A n) → (r : Vec (FinSet (succ n)) n) → (eq : vecEquiv (dot ringModule (vecMap vecModuleBasis r) coeffs) (vecPure 0G)) → (uniq : {a : ℕ} {b : ℕ} (a<n : a <N n) (b<n : b <N n) → vecIndex r a a<n ≡ vecIndex r b b<n → a ≡ b) → {!!}
rearrangeBasis coeffs r eq uniq = {!!}

vecModuleBasisSpans : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) {n : ℕ} → Spans (ringModule {n}) (vecModuleBasis {n})
vecModuleBasisSpans R {n} m = n , ((allEntries n ,, m) , identityMatrixProduct m)

vecModuleBasisIndependent : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) {n : ℕ} → Independent (ringModule {n}) (vecModuleBasis {n})
vecModuleBasisIndependent R {zero} [] _ [] x = record {}
vecModuleBasisIndependent R {succ n} r _ [] x = record {}
vecModuleBasisIndependent R {succ n} r uniq coeffs x = {!!}