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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.ShapeView {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Reflexivity

open import Tools.Product
open import Tools.Empty using (⊥; ⊥-elim)
import Tools.PropositionalEquality as PE

-- Type for maybe embeddings of reducible types
data MaybeEmb (l : TypeLevel) (⊩⟨_⟩ : TypeLevel → Set) : Set where
  noemb : ⊩⟨ l ⟩ → MaybeEmb l ⊩⟨_⟩
  emb   : ∀ {l′} → l′ < l → MaybeEmb l′ ⊩⟨_⟩ → MaybeEmb l ⊩⟨_⟩

-- Specific reducible types with possible embedding

_⊩⟨_⟩U : (Γ : Con Term) (l : TypeLevel) → Set
Γ ⊩⟨ l ⟩U = MaybeEmb l (λ l′ → Γ ⊩′⟨ l′ ⟩U)

_⊩⟨_⟩ℕ_ : (Γ : Con Term) (l : TypeLevel) (A : Term) → Set
Γ ⊩⟨ l ⟩ℕ A = MaybeEmb l (λ l′ → Γ ⊩ℕ A)

_⊩⟨_⟩Empty_ : (Γ : Con Term) (l : TypeLevel) (A : Term) → Set
Γ ⊩⟨ l ⟩Empty A = MaybeEmb l (λ l′ → Γ ⊩Empty A)

_⊩⟨_⟩Unit_ : (Γ : Con Term) (l : TypeLevel) (A : Term) → Set
Γ ⊩⟨ l ⟩Unit A = MaybeEmb l (λ l′ → Γ ⊩Unit A)

_⊩⟨_⟩ne_ : (Γ : Con Term) (l : TypeLevel) (A : Term) → Set
Γ ⊩⟨ l ⟩ne A = MaybeEmb l (λ l′ → Γ ⊩ne A)

_⊩⟨_⟩B⟨_⟩_ : (Γ : Con Term) (l : TypeLevel) (W : BindingType) (A : Term) → Set
Γ ⊩⟨ l ⟩B⟨ W ⟩ A = MaybeEmb l (λ l′ → Γ ⊩′⟨ l′ ⟩B⟨ W ⟩ A)

-- Construct a general reducible type from a specific

U-intr : ∀ {Γ l} → Γ ⊩⟨ l ⟩U → Γ ⊩⟨ l ⟩ U
U-intr (noemb x) = Uᵣ x
U-intr (emb 0<1 x) = emb 0<1 (U-intr x)

ℕ-intr : ∀ {A Γ l} → Γ ⊩⟨ l ⟩ℕ A → Γ ⊩⟨ l ⟩ A
ℕ-intr (noemb x) = ℕᵣ x
ℕ-intr (emb 0<1 x) = emb 0<1 (ℕ-intr x)

Empty-intr : ∀ {A Γ l} → Γ ⊩⟨ l ⟩Empty A → Γ ⊩⟨ l ⟩ A
Empty-intr (noemb x) = Emptyᵣ x
Empty-intr (emb 0<1 x) = emb 0<1 (Empty-intr x)

Unit-intr : ∀ {A Γ l} → Γ ⊩⟨ l ⟩Unit A → Γ ⊩⟨ l ⟩ A
Unit-intr (noemb x) = Unitᵣ x
Unit-intr (emb 0<1 x) = emb 0<1 (Unit-intr x)

ne-intr : ∀ {A Γ l} → Γ ⊩⟨ l ⟩ne A → Γ ⊩⟨ l ⟩ A
ne-intr (noemb x) = ne x
ne-intr (emb 0<1 x) = emb 0<1 (ne-intr x)

B-intr : ∀ {A Γ l} W → Γ ⊩⟨ l ⟩B⟨ W ⟩ A → Γ ⊩⟨ l ⟩ A
B-intr W (noemb x) = Bᵣ W x
B-intr W (emb 0<1 x) = emb 0<1 (B-intr W x)

-- Construct a specific reducible type from a general with some criterion

U-elim : ∀ {Γ l} → Γ ⊩⟨ l ⟩ U → Γ ⊩⟨ l ⟩U
U-elim (Uᵣ′ l′ l< ⊢Γ) = noemb (Uᵣ l′ l< ⊢Γ)
U-elim (ℕᵣ D) with whnfRed* (red D) Uₙ
... | ()
U-elim (Emptyᵣ D) with whnfRed* (red D) Uₙ
... | ()
U-elim (Unitᵣ D) with whnfRed* (red D) Uₙ
... | ()
U-elim (ne′ K D neK K≡K) =
  ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
U-elim (Bᵣ′ W F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (U≢B W (whnfRed* (red D) Uₙ))
U-elim (emb 0<1 x) with U-elim x
U-elim (emb 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
U-elim (emb 0<1 x) | emb () x₁

ℕ-elim′ : ∀ {A Γ l} → Γ ⊢ A ⇒* ℕ → Γ ⊩⟨ l ⟩ A → Γ ⊩⟨ l ⟩ℕ A
ℕ-elim′ D (Uᵣ′ l′ l< ⊢Γ) with whrDet* (id (Uⱼ ⊢Γ) , Uₙ) (D , ℕₙ)
... | ()
ℕ-elim′ D (ℕᵣ D′) = noemb D′
ℕ-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elim (ℕ≢ne neK (whrDet* (D , ℕₙ) (red D′ , ne neK)))
ℕ-elim′ D (Bᵣ′ W F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (ℕ≢B W (whrDet* (D , ℕₙ) (red D′ , ⟦ W ⟧ₙ)))
ℕ-elim′ D (Emptyᵣ D′) with whrDet* (D , ℕₙ) (red D′ , Emptyₙ)
... | ()
ℕ-elim′ D (Unitᵣ D′) with whrDet* (D , ℕₙ) (red D′ , Unitₙ)
... | ()
ℕ-elim′ D (emb 0<1 x) with ℕ-elim′ D x
ℕ-elim′ D (emb 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
ℕ-elim′ D (emb 0<1 x) | emb () x₂

ℕ-elim : ∀ {Γ l} → Γ ⊩⟨ l ⟩ ℕ → Γ ⊩⟨ l ⟩ℕ ℕ
ℕ-elim [ℕ] = ℕ-elim′ (id (escape [ℕ])) [ℕ]

Empty-elim′ : ∀ {A Γ l} → Γ ⊢ A ⇒* Empty → Γ ⊩⟨ l ⟩ A → Γ ⊩⟨ l ⟩Empty A
Empty-elim′ D (Uᵣ′ l′ l< ⊢Γ) with whrDet* (id (Uⱼ ⊢Γ) , Uₙ) (D , Emptyₙ)
... | ()
Empty-elim′ D (Emptyᵣ D′) = noemb D′
Empty-elim′ D (Unitᵣ D′) with whrDet* (D , Emptyₙ) (red D′ , Unitₙ)
... | ()
Empty-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elim (Empty≢ne neK (whrDet* (D , Emptyₙ) (red D′ , ne neK)))
Empty-elim′ D (Bᵣ′ W F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (Empty≢B W (whrDet* (D , Emptyₙ) (red D′ , ⟦ W ⟧ₙ)))
Empty-elim′ D (ℕᵣ D′) with whrDet* (D , Emptyₙ) (red D′ , ℕₙ)
... | ()
Empty-elim′ D (emb 0<1 x) with Empty-elim′ D x
Empty-elim′ D (emb 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
Empty-elim′ D (emb 0<1 x) | emb () x₂

Empty-elim : ∀ {Γ l} → Γ ⊩⟨ l ⟩ Empty → Γ ⊩⟨ l ⟩Empty Empty
Empty-elim [Empty] = Empty-elim′ (id (escape [Empty])) [Empty]

Unit-elim′ : ∀ {A Γ l} → Γ ⊢ A ⇒* Unit → Γ ⊩⟨ l ⟩ A → Γ ⊩⟨ l ⟩Unit A
Unit-elim′ D (Uᵣ′ l′ l< ⊢Γ) with whrDet* (id (Uⱼ ⊢Γ) , Uₙ) (D , Unitₙ)
... | ()
Unit-elim′ D (Unitᵣ D′) = noemb D′
Unit-elim′ D (Emptyᵣ D′) with whrDet* (D , Unitₙ) (red D′ , Emptyₙ)
... | ()
Unit-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elim (Unit≢ne neK (whrDet* (D , Unitₙ) (red D′ , ne neK)))
Unit-elim′ D (Bᵣ′ W F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (Unit≢B W (whrDet* (D , Unitₙ) (red D′ , ⟦ W ⟧ₙ)))
Unit-elim′ D (ℕᵣ D′) with whrDet* (D , Unitₙ) (red D′ , ℕₙ)
... | ()
Unit-elim′ D (emb 0<1 x) with Unit-elim′ D x
Unit-elim′ D (emb 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
Unit-elim′ D (emb 0<1 x) | emb () x₂

Unit-elim : ∀ {Γ l} → Γ ⊩⟨ l ⟩ Unit → Γ ⊩⟨ l ⟩Unit Unit
Unit-elim [Unit] = Unit-elim′ (id (escape [Unit])) [Unit]

ne-elim′ : ∀ {A Γ l K} → Γ ⊢ A ⇒* K → Neutral K → Γ ⊩⟨ l ⟩ A → Γ ⊩⟨ l ⟩ne A
ne-elim′ D neK (Uᵣ′ l′ l< ⊢Γ) =
  ⊥-elim (U≢ne neK (whrDet* (id (Uⱼ ⊢Γ) , Uₙ) (D , ne neK)))
ne-elim′ D neK (ℕᵣ D′) = ⊥-elim (ℕ≢ne neK (whrDet* (red D′ , ℕₙ) (D , ne neK)))
ne-elim′ D neK (Emptyᵣ D′) = ⊥-elim (Empty≢ne neK (whrDet* (red D′ , Emptyₙ) (D , ne neK)))
ne-elim′ D neK (Unitᵣ D′) = ⊥-elim (Unit≢ne neK (whrDet* (red D′ , Unitₙ) (D , ne neK)))
ne-elim′ D neK (ne′ K D′ neK′ K≡K) = noemb (ne K D′ neK′ K≡K)
ne-elim′ D neK (Bᵣ′ W F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (B≢ne W neK (whrDet* (red D′ , ⟦ W ⟧ₙ) (D , ne neK)))
ne-elim′ D neK (emb 0<1 x) with ne-elim′ D neK x
ne-elim′ D neK (emb 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
ne-elim′ D neK (emb 0<1 x) | emb () x₂

ne-elim : ∀ {Γ l K} → Neutral K  → Γ ⊩⟨ l ⟩ K → Γ ⊩⟨ l ⟩ne K
ne-elim neK [K] = ne-elim′ (id (escape [K])) neK [K]

B-elim′ : ∀ {A Γ F G l} W → Γ ⊢ A ⇒* ⟦ W ⟧ F ▹ G → Γ ⊩⟨ l ⟩ A → Γ ⊩⟨ l ⟩B⟨ W ⟩ A
B-elim′ W D (Uᵣ′ l′ l< ⊢Γ) =
  ⊥-elim (U≢B W (whrDet* (id (Uⱼ ⊢Γ) , Uₙ) (D , ⟦ W ⟧ₙ)))
B-elim′ W D (ℕᵣ D′) =
  ⊥-elim (ℕ≢B W (whrDet* (red D′ , ℕₙ) (D , ⟦ W ⟧ₙ)))
B-elim′ W D (Emptyᵣ D′) =
  ⊥-elim (Empty≢B W (whrDet* (red D′ , Emptyₙ) (D , ⟦ W ⟧ₙ)))
B-elim′ W D (Unitᵣ D′) =
  ⊥-elim (Unit≢B W (whrDet* (red D′ , Unitₙ) (D , ⟦ W ⟧ₙ)))
B-elim′ W D (ne′ K D′ neK K≡K) =
  ⊥-elim (B≢ne W neK (whrDet* (D , ⟦ W ⟧ₙ) (red D′ , ne neK)))
B-elim′ BΠ D (Bᵣ′ BΣ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) with whrDet* (D , Πₙ) (red D′ , Σₙ)
... | ()
B-elim′ BΣ D (Bᵣ′ BΠ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) with whrDet* (D , Σₙ) (red D′ , Πₙ)
... | ()
B-elim′ BΠ D (Bᵣ′ BΠ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  noemb (Bᵣ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext)
B-elim′ BΣ D (Bᵣ′ BΣ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  noemb (Bᵣ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext)
B-elim′ W D (emb 0<1 x) with B-elim′ W D x
B-elim′ W D (emb 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
B-elim′ W D (emb 0<1 x) | emb () x₂

B-elim : ∀ {Γ F G l} W → Γ ⊩⟨ l ⟩ ⟦ W ⟧ F ▹ G → Γ ⊩⟨ l ⟩B⟨ W ⟩ ⟦ W ⟧ F ▹ G
B-elim W [Π] = B-elim′ W (id (escape [Π])) [Π]

Π-elim : ∀ {Γ F G l} → Γ ⊩⟨ l ⟩ Π F ▹ G → Γ ⊩⟨ l ⟩B⟨ BΠ ⟩ Π F ▹ G
Π-elim [Π] = B-elim′ BΠ (id (escape [Π])) [Π]

Σ-elim : ∀ {Γ F G l} → Γ ⊩⟨ l ⟩ Σ F ▹ G → Γ ⊩⟨ l ⟩B⟨ BΣ ⟩ Σ F ▹ G
Σ-elim [Σ] = B-elim′ BΣ (id (escape [Σ])) [Σ]

-- Extract a type and a level from a maybe embedding
extractMaybeEmb : ∀ {l ⊩⟨_⟩} → MaybeEmb l ⊩⟨_⟩ → ∃ λ l′ → ⊩⟨ l′ ⟩
extractMaybeEmb (noemb x) = _ , x
extractMaybeEmb (emb 0<1 x) = extractMaybeEmb x

-- A view for constructor equality of types where embeddings are ignored
data ShapeView Γ : ∀ l l′ A B (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ B) → Set where
  Uᵥ : ∀ {l l′} UA UB → ShapeView Γ l l′ U U (Uᵣ UA) (Uᵣ UB)
  ℕᵥ : ∀ {A B l l′} ℕA ℕB → ShapeView Γ l l′ A B (ℕᵣ ℕA) (ℕᵣ ℕB)
  Emptyᵥ : ∀ {A B l l′} EmptyA EmptyB → ShapeView Γ l l′ A B (Emptyᵣ EmptyA) (Emptyᵣ EmptyB)
  Unitᵥ : ∀ {A B l l′} UnitA UnitB → ShapeView Γ l l′ A B (Unitᵣ UnitA) (Unitᵣ UnitB)
  ne  : ∀ {A B l l′} neA neB
      → ShapeView Γ l l′ A B (ne neA) (ne neB)
  Bᵥ : ∀ {A B l l′} W BA BB
    → ShapeView Γ l l′ A B (Bᵣ W BA) (Bᵣ W BB)
  emb⁰¹ : ∀ {A B l p q}
        → ShapeView Γ ⁰ l A B p q
        → ShapeView Γ ¹ l A B (emb 0<1 p) q
  emb¹⁰ : ∀ {A B l p q}
        → ShapeView Γ l ⁰ A B p q
        → ShapeView Γ l ¹ A B p (emb 0<1 q)

-- Construct an shape view from an equality (aptly named)
goodCases : ∀ {l l′ Γ A B} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
          → Γ ⊩⟨ l ⟩ A ≡ B / [A] → ShapeView Γ l l′ A B [A] [B]
-- Diagonal cases
goodCases (Uᵣ UA) (Uᵣ UB) A≡B = Uᵥ UA UB
goodCases (ℕᵣ ℕA) (ℕᵣ ℕB) A≡B = ℕᵥ ℕA ℕB
goodCases (Emptyᵣ EmptyA) (Emptyᵣ EmptyB) A≡B = Emptyᵥ EmptyA EmptyB
goodCases (Unitᵣ UnitA) (Unitᵣ UnitB) A≡B = Unitᵥ UnitA UnitB
goodCases (ne neA) (ne neB) A≡B = ne neA neB
goodCases (Bᵣ BΠ ΠA) (Bᵣ BΠ ΠB) A≡B = Bᵥ BΠ ΠA ΠB
goodCases (Bᵣ BΣ ΣA) (Bᵣ BΣ ΣB) A≡B = Bᵥ BΣ ΣA ΣB
--goodCases (Σᵣ ΣA) (Σᵣ ΣB) A≡B = Σᵥ ΣA ΣB

goodCases {l} [A] (emb 0<1 x) A≡B =
  emb¹⁰ (goodCases {l} {⁰} [A] x A≡B)
goodCases {l′ = l} (emb 0<1 x) [B] A≡B =
  emb⁰¹ (goodCases {⁰} {l} x [B] A≡B)

-- Refutable cases
-- U ≡ _
goodCases (Uᵣ′ _ _ ⊢Γ) (ℕᵣ D) PE.refl with whnfRed* (red D) Uₙ
... | ()
goodCases (Uᵣ′ _ _ ⊢Γ) (Emptyᵣ D) PE.refl with whnfRed* (red D) Uₙ
... | ()
goodCases (Uᵣ′ _ _ ⊢Γ) (Unitᵣ D) PE.refl with whnfRed* (red D) Uₙ
... | ()
goodCases (Uᵣ′ _ _ ⊢Γ) (ne′ K D neK K≡K) PE.refl =
  ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
goodCases (Uᵣ′ _ _ ⊢Γ) (Bᵣ′ W F G D ⊢F ⊢G A≡A [F] [G] G-ext) PE.refl =
  ⊥-elim (U≢B W (whnfRed* (red D) Uₙ))

-- ℕ ≡ _
goodCases (ℕᵣ D) (Uᵣ ⊢Γ) A≡B with whnfRed* A≡B Uₙ
... | ()
goodCases (ℕᵣ _) (Emptyᵣ D') D with whrDet* (D , ℕₙ) (red D' , Emptyₙ)
... | ()
goodCases (ℕᵣ x) (Unitᵣ D') D with whrDet* (D , ℕₙ) (red D' , Unitₙ)
... | ()
goodCases (ℕᵣ D) (ne′ K D₁ neK K≡K) A≡B =
  ⊥-elim (ℕ≢ne neK (whrDet* (A≡B , ℕₙ) (red D₁ , ne neK)))
goodCases (ℕᵣ D) (Bᵣ′ W F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) A≡B =
  ⊥-elim (ℕ≢B W (whrDet* (A≡B , ℕₙ) (red D₁ , ⟦ W ⟧ₙ)))

-- Empty ≢ _
goodCases (Emptyᵣ D) (Uᵣ ⊢Γ) A≡B with whnfRed* A≡B Uₙ
... | ()
goodCases (Emptyᵣ _) (Unitᵣ D') D with whrDet* (red D' , Unitₙ) (D , Emptyₙ)
... | ()
goodCases (Emptyᵣ _) (ℕᵣ D') D with whrDet* (red D' , ℕₙ) (D , Emptyₙ)
... | ()
goodCases (Emptyᵣ D) (ne′ K D₁ neK K≡K) A≡B =
  ⊥-elim (Empty≢ne neK (whrDet* (A≡B , Emptyₙ) (red D₁ , ne neK)))
goodCases (Emptyᵣ D) (Bᵣ′ W F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) A≡B =
  ⊥-elim (Empty≢B W (whrDet* (A≡B , Emptyₙ) (red D₁ , ⟦ W ⟧ₙ)))

-- Unit ≡ _
goodCases (Unitᵣ _) (Uᵣ x₁) A≡B with whnfRed* A≡B Uₙ
... | ()
goodCases (Unitᵣ _) (Emptyᵣ D') D with whrDet* (red D' , Emptyₙ) (D , Unitₙ)
... | ()
goodCases (Unitᵣ _) (ℕᵣ D') D with whrDet* (red D' , ℕₙ) (D , Unitₙ)
... | ()
goodCases (Unitᵣ D) (ne′ K D₁ neK K≡K) A≡B =
  ⊥-elim (Unit≢ne neK (whrDet* (A≡B , Unitₙ) (red D₁ , ne neK)))
goodCases (Unitᵣ D) (Bᵣ′ W F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) A≡B =
  ⊥-elim (Unit≢B W (whrDet* (A≡B , Unitₙ) (red D₁ , ⟦ W ⟧ₙ)))

-- ne ≡ _
goodCases (ne′ K D neK K≡K) (Uᵣ ⊢Γ) (ne₌ M D′ neM K≡M) =
  ⊥-elim (U≢ne neM (whnfRed* (red D′) Uₙ))
goodCases (ne′ K D neK K≡K) (ℕᵣ D₁) (ne₌ M D′ neM K≡M) =
  ⊥-elim (ℕ≢ne neM (whrDet* (red D₁ , ℕₙ) (red D′ , ne neM)))
goodCases (ne′ K D neK K≡K) (Emptyᵣ D₁) (ne₌ M D′ neM K≡M) =
  ⊥-elim (Empty≢ne neM (whrDet* (red D₁ , Emptyₙ) (red D′ , ne neM)))
goodCases (ne′ K D neK K≡K) (Unitᵣ D₁) (ne₌ M D′ neM K≡M) =
  ⊥-elim (Unit≢ne neM (whrDet* (red D₁ , Unitₙ) (red D′ , ne neM)))
goodCases (ne′ K D neK K≡K) (Bᵣ′ W F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) (ne₌ M D′ neM K≡M) =
  ⊥-elim (B≢ne W neM (whrDet* (red D₁ , ⟦ W ⟧ₙ) (red D′ , ne neM)))

-- Π ≡ _
goodCases (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Uᵣ ⊢Γ)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) with whnfRed* D′ Uₙ
... | ()
goodCases (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ℕᵣ D₁)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) with whrDet* (red D₁ , ℕₙ) (D′ , Πₙ)
... | ()
goodCases (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Emptyᵣ D₁)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) with whrDet* (red D₁ , Emptyₙ) (D′ , Πₙ)
... | ()
goodCases (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Unitᵣ D₁)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) with whrDet* (red D₁ , Unitₙ) (D′ , Πₙ)
... | ()
goodCases (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Bᵣ′ BΣ F′ G′ D′ ⊢F′ ⊢G′ A≡A′ [F]′ [G]′ G-ext′)
  (B₌ F′₁ G′₁ D′₁ A≡B [F≡F′] [G≡G′]) with whrDet* (red D′ , Σₙ) (D′₁ , Πₙ)
... | ()
goodCases (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ne′ K D₁ neK K≡K)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (B≢ne BΠ neK (whrDet* (D′ , Πₙ) (red D₁ , ne neK)))

-- Σ ≡ _
goodCases (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Uᵣ ⊢Γ)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) with whnfRed* D′ Uₙ
... | ()
goodCases (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ℕᵣ D₁)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) with whrDet* (red D₁ , ℕₙ) (D′ , Σₙ)
... | ()
goodCases (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Emptyᵣ D₁)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) with whrDet* (red D₁ , Emptyₙ) (D′ , Σₙ)
... | ()
goodCases (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Unitᵣ D₁)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) with whrDet* (red D₁ , Unitₙ) (D′ , Σₙ)
... | ()
goodCases (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Bᵣ′ BΠ F′ G′ D′ ⊢F′ ⊢G′ A≡A′ [F]′ [G]′ G-ext′)
  (B₌ F′₁ G′₁ D′₁ A≡B [F≡F′] [G≡G′]) with whrDet* (red D′ , Πₙ) (D′₁ , Σₙ)
... | ()
goodCases (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ne′ K D₁ neK K≡K)
          (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (B≢ne BΣ neK (whrDet* (D′ , Σₙ) (red D₁ , ne neK)))

-- Construct an shape view between two derivations of the same type
goodCasesRefl : ∀ {l l′ Γ A} ([A] : Γ ⊩⟨ l ⟩ A) ([A′] : Γ ⊩⟨ l′ ⟩ A)
              → ShapeView Γ l l′ A A [A] [A′]
goodCasesRefl [A] [A′] = goodCases [A] [A′] (reflEq [A])

-- A view for constructor equality between three types
data ShapeView₃ Γ : ∀ l l′ l″ A B C
                 (p : Γ ⊩⟨ l   ⟩ A)
                 (q : Γ ⊩⟨ l′  ⟩ B)
                 (r : Γ ⊩⟨ l″ ⟩ C) → Set where
  Uᵥ : ∀ {l l′ l″} UA UB UC → ShapeView₃ Γ l l′ l″ U U U (Uᵣ UA) (Uᵣ UB) (Uᵣ UC)
  ℕᵥ : ∀ {A B C l l′ l″} ℕA ℕB ℕC
    → ShapeView₃ Γ l l′ l″ A B C (ℕᵣ ℕA) (ℕᵣ ℕB) (ℕᵣ ℕC)
  Emptyᵥ : ∀ {A B C l l′ l″} EmptyA EmptyB EmptyC
    → ShapeView₃ Γ l l′ l″ A B C (Emptyᵣ EmptyA) (Emptyᵣ EmptyB) (Emptyᵣ EmptyC)
  Unitᵥ : ∀ {A B C l l′ l″} UnitA UnitB UnitC
    → ShapeView₃ Γ l l′ l″ A B C (Unitᵣ UnitA) (Unitᵣ UnitB) (Unitᵣ UnitC)
  ne  : ∀ {A B C l l′ l″} neA neB neC
      → ShapeView₃ Γ l l′ l″ A B C (ne neA) (ne neB) (ne neC)
  Bᵥ : ∀ {A B C l l′ l″} W BA BB BC
    → ShapeView₃ Γ l l′ l″ A B C (Bᵣ W BA) (Bᵣ W BB) (Bᵣ W BC)
  emb⁰¹¹ : ∀ {A B C l l′ p q r}
         → ShapeView₃ Γ ⁰ l l′ A B C p q r
         → ShapeView₃ Γ ¹ l l′ A B C (emb 0<1 p) q r
  emb¹⁰¹ : ∀ {A B C l l′ p q r}
         → ShapeView₃ Γ l ⁰ l′ A B C p q r
         → ShapeView₃ Γ l ¹ l′ A B C p (emb 0<1 q) r
  emb¹¹⁰ : ∀ {A B C l l′ p q r}
         → ShapeView₃ Γ l l′ ⁰ A B C p q r
         → ShapeView₃ Γ l l′ ¹ A B C p q (emb 0<1 r)

-- Combines two two-way views into a three-way view
combine : ∀ {Γ l l′ l″ l‴ A B C [A] [B] [B]′ [C]}
        → ShapeView Γ l l′ A B [A] [B]
        → ShapeView Γ l″ l‴ B C [B]′ [C]
        → ShapeView₃ Γ l l′ l‴ A B C [A] [B] [C]
-- Diagonal cases
combine (Uᵥ UA₁ UB₁) (Uᵥ UA UB) = Uᵥ UA₁ UB₁ UB
combine (ℕᵥ ℕA₁ ℕB₁) (ℕᵥ ℕA ℕB) = ℕᵥ ℕA₁ ℕB₁ ℕB
combine (Emptyᵥ EmptyA₁ EmptyB₁) (Emptyᵥ EmptyA EmptyB) = Emptyᵥ EmptyA₁ EmptyB₁ EmptyB
combine (Unitᵥ UnitA₁ UnitB₁) (Unitᵥ UnitA UnitB) = Unitᵥ UnitA₁ UnitB₁ UnitB
combine (ne neA₁ neB₁) (ne neA neB) = ne neA₁ neB₁ neB
combine (Bᵥ BΠ ΠA₁ ΠB₁) (Bᵥ BΠ ΠA ΠB) = Bᵥ BΠ ΠA₁ ΠB₁ ΠB
combine (Bᵥ BΣ ΣA₁ ΣB₁) (Bᵥ BΣ ΣA ΣB) = Bᵥ BΣ ΣA₁ ΣB₁ ΣB
combine (emb⁰¹ [AB]) [BC] = emb⁰¹¹ (combine [AB] [BC])
combine (emb¹⁰ [AB]) [BC] = emb¹⁰¹ (combine [AB] [BC])
combine [AB] (emb⁰¹ [BC]) = combine [AB] [BC]
combine [AB] (emb¹⁰ [BC]) = emb¹¹⁰ (combine [AB] [BC])

-- Refutable cases
-- U ≡ _
combine (Uᵥ UA UB) (ℕᵥ ℕA ℕB) with whnfRed* (red ℕA) Uₙ
... | ()
combine (Uᵥ UA UB) (Emptyᵥ EmptyA EmptyB) with whnfRed* (red EmptyA) Uₙ
... | ()
combine (Uᵥ UA UB) (Unitᵥ UnA UnB) with whnfRed* (red UnA) Uₙ
... | ()
combine (Uᵥ UA UB) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
combine (Uᵥ UA UB) (Bᵥ W (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) BB) =
  ⊥-elim (U≢B W (whnfRed* (red D) Uₙ))

-- ℕ ≡ _
combine (ℕᵥ ℕA ℕB) (Uᵥ UA UB) with whnfRed* (red ℕB) Uₙ
... | ()
combine (ℕᵥ ℕA ℕB) (Emptyᵥ EmptyA EmptyB) with whrDet* (red ℕB , ℕₙ) (red EmptyA , Emptyₙ)
... | ()
combine (ℕᵥ ℕA ℕB) (Unitᵥ UnA UnB) with whrDet* (red ℕB , ℕₙ) (red UnA , Unitₙ)
... | ()
combine (ℕᵥ ℕA ℕB) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (ℕ≢ne neK (whrDet* (red ℕB , ℕₙ) (red D , ne neK)))
combine (ℕᵥ ℕA ℕB) (Bᵥ W (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) BB) =
  ⊥-elim (ℕ≢B W (whrDet* (red ℕB , ℕₙ) (red D , ⟦ W ⟧ₙ)))

-- Empty ≡ _
combine (Emptyᵥ EmptyA EmptyB) (Uᵥ UA UB) with whnfRed* (red EmptyB) Uₙ
... | ()
combine (Emptyᵥ EmptyA EmptyB) (ℕᵥ ℕA ℕB) with whrDet* (red EmptyB , Emptyₙ) (red ℕA , ℕₙ)
... | ()
combine (Emptyᵥ EmptyA EmptyB) (Unitᵥ UnA UnB) with whrDet* (red EmptyB , Emptyₙ) (red UnA , Unitₙ)
... | ()
combine (Emptyᵥ EmptyA EmptyB) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (Empty≢ne neK (whrDet* (red EmptyB , Emptyₙ) (red D , ne neK)))
combine (Emptyᵥ EmptyA EmptyB) (Bᵥ W (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) BB) =
  ⊥-elim (Empty≢B W (whrDet* (red EmptyB , Emptyₙ) (red D , ⟦ W ⟧ₙ)))

-- Unit ≡ _
combine (Unitᵥ UnitA UnitB) (Uᵥ UA UB) with whnfRed* (red UnitB) Uₙ
... | ()
combine (Unitᵥ UnitA UnitB) (ℕᵥ ℕA ℕB) with whrDet* (red UnitB , Unitₙ) (red ℕA , ℕₙ)
... | ()
combine (Unitᵥ UnitA UnitB) (Emptyᵥ EmptyA EmptyB) with whrDet* (red UnitB , Unitₙ) (red EmptyA , Emptyₙ)
... | ()
combine (Unitᵥ UnitA UnitB) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (Unit≢ne neK (whrDet* (red UnitB , Unitₙ) (red D , ne neK)))
combine (Unitᵥ UnitA UnitB) (Bᵥ W (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) BB) =
  ⊥-elim (Unit≢B W (whrDet* (red UnitB , Unitₙ) (red D , ⟦ W ⟧ₙ)))

-- ne ≡ _
combine (ne neA (ne K D neK K≡K)) (Uᵥ UA UB) =
  ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
combine (ne neA (ne K D neK K≡K)) (ℕᵥ ℕA ℕB) =
  ⊥-elim (ℕ≢ne neK (whrDet* (red ℕA , ℕₙ) (red D , ne neK)))
combine (ne neA (ne K D neK K≡K)) (Emptyᵥ EmptyA EmptyB) =
  ⊥-elim (Empty≢ne neK (whrDet* (red EmptyA , Emptyₙ) (red D , ne neK)))
combine (ne neA (ne K D neK K≡K)) (Unitᵥ UnA UnB) =
  ⊥-elim (Unit≢ne neK (whrDet* (red UnA , Unitₙ) (red D , ne neK)))
combine (ne neA (ne K D neK K≡K)) (Bᵥ W (Bᵣ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) BB) =
  ⊥-elim (B≢ne W neK (whrDet* (red D₁ , ⟦ W ⟧ₙ) (red D , ne neK)))

-- Π/Σ ≡ _
combine (Bᵥ W BA (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Uᵥ UA UB) =
  ⊥-elim (U≢B W (whnfRed* (red D) Uₙ))
combine (Bᵥ W BA (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (ℕᵥ ℕA ℕB) =
  ⊥-elim (ℕ≢B W (whrDet* (red ℕA , ℕₙ) (red D , ⟦ W ⟧ₙ)))
combine (Bᵥ W BA (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Emptyᵥ EmptyA EmptyB) =
  ⊥-elim (Empty≢B W (whrDet* (red EmptyA , Emptyₙ) (red D , ⟦ W ⟧ₙ)))
combine (Bᵥ W BA (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Unitᵥ UnitA UnitB) =
  ⊥-elim (Unit≢B W (whrDet* (red UnitA , Unitₙ) (red D , ⟦ W ⟧ₙ)))
combine (Bᵥ W BA (Bᵣ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext)) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (B≢ne W neK (whrDet* (red D₁ , ⟦ W ⟧ₙ) (red D , ne neK)))
combine (Bᵥ BΠ ΠA (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Bᵥ BΣ (Bᵣ F′ G′ D′ ⊢F′ ⊢G′ A≡A′ [F]′ [G]′ G-ext′) ΣA)
  with whrDet* (red D , Πₙ) (red D′ , Σₙ)
... | ()
combine (Bᵥ BΣ ΣA (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Bᵥ BΠ (Bᵣ F′ G′ D′ ⊢F′ ⊢G′ A≡A′ [F]′ [G]′ G-ext′) ΠA)
  with whrDet* (red D , Σₙ) (red D′ , Πₙ)
... | ()


text:
open import Prelude hiding (id; Bool; _∷_; [])

module Examples.PartialResolution where

data TC : Set where
  tc-int : TC
  tc-bool : TC

_tc≟_ : (a b : TC) → Dec (a ≡ b)
tc-int tc≟ tc-int = yes refl
tc-int tc≟ tc-bool = no (λ ())
tc-bool tc≟ tc-int = no (λ ())
tc-bool tc≟ tc-bool = yes refl

open import Implicits.Syntax
open import Implicits.WellTyped
open import Implicits.Substitutions
open import Implicits.Syntax.Type.Unification
open import Implicits.Resolution.Infinite.Algorithm
open import Data.Maybe
open import Data.List
open import Category.Monad.Partiality

Bool : ∀ {n} → Type n
Bool = simpl (tc tc-bool)

Int : ∀ {n} → Type n
Int = simpl (tc tc-int)

module Ex₁ where

  Δ : ICtx zero
  Δ = Bool ∷ Int ∷ []

  -- resolves directly using a value from the implicit context
  r = run_for_steps (resolve Δ Int) 10

  p : isNow r ≡ true
  p = refl

module Ex₂ where

  Δ : ICtx zero
  Δ = Bool ∷ (Bool ⇒ Int) ∷ []

  -- resolves using implicit application
  r = run_for_steps (resolve Δ Int) 10

  p : r resolved? ≡ true
  p = refl

module Ex₃ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' (Bool ⇒ (simpl (tvar zero)))) ∷ []

  -- resolves using polymorphic appliation + implicit application
  r = run_for_steps (resolve Δ Int) 10

  p : r resolved? ≡ true
  p = refl

module Ex₄ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' ((simpl (tvar zero)) ⇒ Int)) ∷ []

  r = run_for_steps (resolve Δ Int) 10

  -- Maybe surprisingly this fails.
  -- But we should note that unification on the codomain of the rule does not fix the domain to a
  -- concrete type, such that it's instantiation is left ambiguous.
  -- Like Oliveira we reject those rules, because they lead to ambiguous terms.
  p : r failed? ≡ true
  p = refl

module Ex₅ where

  -- The following context would not resolved Int in Oliveira's deterministic calculus.
  -- Demonstratint that partial resolution is more powerful for terminating contexts.
  Δ : ICtx zero
  Δ = (Bool ⇒ Int) ∷ Int ∷ []

  r = run_for_steps (resolve Δ Int) 10

  p : r resolved? ≡ true
  p = refl

module Ex₆ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' (Bool ⇒ (simpl (tvar zero)))) ∷ []

  -- resolves rule types
  r = run_for_steps (resolve Δ (Bool ⇒ Int)) 10

  p : r resolved? ≡ true
  p = refl

module Ex₇ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' (Bool ⇒ (simpl (tvar zero)))) ∷ []

  q : Type zero
  q = (∀' (Bool ⇒ (simpl (tvar zero))))

  -- Resolves polymorphic types.
  -- Note that it doesn't resolve to the rule in the context directly.
  -- Instead, it will apply r-tabs and r-iabs, to obtain resolve Δ' ⊢ᵣ (∀' (tvar zero))
  r = run_for_steps (resolve Δ q) 10

  p : r resolved? ≡ true
  p = refl

module Ex₈ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' ((simpl (tvar zero)) ⇒ (simpl (tvar zero)))) ∷ []

  -- infinite derivation exists: not decidable
  r = run_for_steps (resolve Δ Int) 10

  p : r resolved? ≡ false
  p = refl

  ¬p : r failed? ≡ false
  ¬p = refl

module Ex₉ where

  Δ : ICtx zero
  Δ = (∀' ((Int ⇒ simpl (tvar zero)) ⇒ ((simpl (tvar zero)) ⇒ Int))) ∷ (Int ⇒ Bool) ∷ []

  r = run_for_steps (resolve Δ (Bool ⇒ Int)) 10

  p : r resolved? ≡ false
  p = refl

  ¬p : r failed? ≡ true
  ¬p = refl

  -- Below p' demonstrates however that a derivation exists!
  -- The algorithm doesn't find it because we left the ⊢unamb predicate from oliveira implicit.
  -- at some point the algorithm has to match ((simpl (mvar zero) ⇒ Int)) with Int.
  -- However, when we match the codomain Int with the goal Int (note the open mvar):
  test : mgu {m = suc zero} {ν = zero} (to-meta Int) (tc tc-int) ≡ nothing
  test = refl
  -- Because mgu requires that all meta variables are instantiated by unification
  -- and in this example (mvar zero) does not occur and thus can't be unified.

  open import Implicits.Resolution.Infinite.Resolution
  open import Coinduction

  p' : Δ ⊢ᵣ (Bool ⇒ Int)
  p' = r-iabs
    (r-simp
      (there (here refl))
      (i-tabs
        (simpl (tc tc-bool))
        (i-iabs
          (♯ (r-iabs (r-simp (there (here refl)) (i-simp (tc tc-bool)))))
          (i-iabs (♯ (r-simp (here refl) (i-simp (tc tc-bool)))) (i-simp (tc tc-int)))
        )
      )
    )

ext: agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on characters
------------------------------------------------------------------------

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

module Data.Char.Properties where

open import Data.Bool using (Bool)
open import Data.Char.Base

import Data.Nat.Properties as ℕₚ

open import Function
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (map′;  ⌊_⌋)
open import Relation.Binary using (Decidable; Setoid; DecSetoid; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality.Core
import Relation.Binary.Construct.On as On
import Relation.Binary.PropositionalEquality as PropEq

------------------------------------------------------------------------
-- Primitive properties

open import Agda.Builtin.Char.Properties
  renaming ( primCharToNatInjective to toNat-injective)
  public

------------------------------------------------------------------------
-- Decidable equality

infix 4 _≟_
_≟_ : Decidable {A = Char} _≡_
x ≟ y = map′ (toNat-injective x y) (cong toNat)
      $ toNat x ℕₚ.≟ toNat y

------------------------------------------------------------------------
-- Boolean equality test.
--
-- Why is the definition _==_ = primCharEquality not used? One reason
-- is that the present definition can sometimes improve type
-- inference, at least with the version of Agda that is current at the
-- time of writing: see unit-test below.

infix 4 _==_
_==_ : Char → Char → Bool
c₁ == c₂ = ⌊ c₁ ≟ c₂ ⌋

private

  -- The following unit test does not type-check (at the time of
  -- writing) if _==_ is replaced by primCharEquality.

  data P : (Char → Bool) → Set where
    p : (c : Char) → P (c ==_)

  unit-test : P ('x' ==_)
  unit-test = p _

------------------------------------------------------------------------
-- Structures

setoid : Setoid _ _
setoid = PropEq.setoid Char

decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = On.strictTotalOrder ℕₚ.<-strictTotalOrder toNat


text:
-- This module is copied from Agda's standard library. It has been
-- renamed (original name is Size) to avoid name clash in case you
-- have the standard library installed.

------------------------------------------------------------------------
-- The Agda standard library
--
-- Sizes for Agda's sized types
------------------------------------------------------------------------

module Sized where

postulate
  Size : Set
  ↑_   : Size → Size
  ∞    : Size

{-# BUILTIN SIZE    Size #-}
{-# BUILTIN SIZESUC ↑_   #-}
{-# BUILTIN SIZEINF ∞    #-}

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.Sn.Properties where

open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Path
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.HITs.S1 renaming (_·_ to _*_)
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Sigma
open import Cubical.HITs.Sn.Base
open import Cubical.HITs.Susp renaming (toSusp to σ)
open import Cubical.HITs.Truncation
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Join renaming (joinS¹S¹→S³ to joinS¹S¹→S3)
open import Cubical.Data.Bool

private
  variable
    ℓ : Level

open Iso

IsoSucSphereSusp : (n : ℕ) → Iso (S₊ (suc n)) (Susp (S₊ n))
IsoSucSphereSusp zero = S¹IsoSuspBool
IsoSucSphereSusp (suc n) = idIso

IsoSucSphereSusp∙ : (n : ℕ)
  → Iso.inv (IsoSucSphereSusp n) north ≡ ptSn (suc n)
IsoSucSphereSusp∙ zero = refl
IsoSucSphereSusp∙ (suc n) = refl

-- Elimination principles for spheres
sphereElim : (n : ℕ) {A : (S₊ (suc n)) → Type ℓ} → ((x : S₊ (suc n)) → isOfHLevel (suc n) (A x))
          → A (ptSn (suc n))
          → (x : S₊ (suc n)) → A x
sphereElim zero hlev pt = toPropElim hlev pt
sphereElim (suc n) hlev pt north = pt
sphereElim (suc n) {A = A} hlev pt south = subst A (merid (ptSn (suc n))) pt
sphereElim (suc n) {A = A} hlev pt (merid a i) =
  sphereElim n {A = λ a → PathP (λ i → A (merid a i)) pt (subst A (merid (ptSn (suc n))) pt)}
               (λ a → isOfHLevelPathP' (suc n) (hlev south) _ _)
               (λ i → transp (λ j → A (merid (ptSn (suc n)) (i ∧ j))) (~ i) pt)
               a i

sphereElim2 : ∀ {ℓ} (n : ℕ) {A : (S₊ (suc n)) → (S₊ (suc n)) → Type ℓ}
          → ((x y : S₊ (suc n)) → isOfHLevel (suc n) (A x y))
          → A (ptSn (suc n)) (ptSn (suc n))
          → (x y : S₊ (suc n)) → A x y
sphereElim2 n hlev pt = sphereElim n (λ _ → isOfHLevelΠ (suc n) λ _ → hlev _ _)
                                     (sphereElim n (hlev _ ) pt)

private
  compPath-lem : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : z ≡ y)
              → PathP (λ i → (p ∙ sym q) i ≡ y) p q
  compPath-lem {y = y} p q i j =
    hcomp (λ k → λ { (i = i0) → p j
                    ; (i = i1) → q (~ k ∨ j)
                    ; (j = i1) → y })
          (p (j ∨ i))

sphereToPropElim : (n : ℕ) {A : (S₊ (suc n)) → Type ℓ} → ((x : S₊ (suc n)) → isProp (A x))
          → A (ptSn (suc n))
          → (x : S₊ (suc n)) → A x
sphereToPropElim zero = toPropElim
sphereToPropElim (suc n) hlev pt north = pt
sphereToPropElim (suc n) {A = A} hlev pt south = subst A (merid (ptSn (suc n))) pt
sphereToPropElim (suc n) {A = A} hlev pt (merid a i) =
  isProp→PathP {B = λ i → A (merid a i)} (λ _ → hlev _) pt (subst A (merid (ptSn (suc n))) pt) i

-- Elimination rule for fibrations (x : Sⁿ) → (y : Sᵐ) → A x y of h-Level (n + m).
-- The following principle is just the special case of the "Wedge Connectivity Lemma"
-- for spheres (See Cubical.Homotopy.WedgeConnectivity or chapter 8.6 in the HoTT book).
-- We prove it directly here for three reasons:
-- (i) it should perform better
-- (ii) we get a slightly stronger statement for spheres: one of the homotopies will, by design, be refl
-- (iii) the fact that the two homotopies only differ by (composition with) the homotopy leftFunction(base) ≡ rightFunction(base)
-- is close to trivial

wedgeconFun : (n m : ℕ) {A : (S₊ (suc n)) → (S₊ (suc m)) → Type ℓ}
          → ((x : S₊ (suc n)) (y : S₊ (suc m)) → isOfHLevel ((suc n) + (suc m)) (A x y))
          → (f : (x : _) → A (ptSn (suc n)) x)
          → (g : (x : _) → A x (ptSn (suc m)))
          → (g (ptSn (suc n)) ≡ f (ptSn (suc m)))
          → (x : S₊ (suc n)) (y : S₊ (suc m)) → A x y
wedgeconLeft : (n m : ℕ) {A : (S₊ (suc n)) → (S₊ (suc m)) → Type ℓ}
             → (hLev : ((x : S₊ (suc n)) (y : S₊ (suc m)) → isOfHLevel ((suc n) + (suc m)) (A x y)))
             → (f : (x : _) → A (ptSn (suc n)) x)
             → (g : (x : _) → A x (ptSn (suc m)))
             → (hom : g (ptSn (suc n)) ≡ f (ptSn (suc m)))
             → (x : _) → wedgeconFun n m hLev f g hom (ptSn (suc n)) x ≡ f x
wedgeconRight : (n m : ℕ) {A : (S₊ (suc n)) → (S₊ (suc m)) → Type ℓ}
             → (hLev : ((x : S₊ (suc n)) (y : S₊ (suc m)) → isOfHLevel ((suc n) + (suc m)) (A x y)))
             → (f : (x : _) → A (ptSn (suc n)) x)
             → (g : (x : _) → A x (ptSn (suc m)))
             → (hom : g (ptSn (suc n)) ≡ f (ptSn (suc m)))
             → (x : _) → wedgeconFun n m hLev f g hom x (ptSn (suc m)) ≡ g x
wedgeconFun zero zero {A = A} hlev f g hom = F
  where
  helper : SquareP (λ i j → A (loop i) (loop j)) (cong f loop) (cong f loop)
                        (λ i → hcomp (λ k → λ { (i = i0) → hom k
                                                ; (i = i1) → hom k })
                                      (g (loop i)))
                         λ i → hcomp (λ k → λ { (i = i0) → hom k
                                                ; (i = i1) → hom k })
                                       (g (loop i))
  helper = toPathP (isOfHLevelPathP' 1 (hlev _ _) _ _ _ _)

  F : (x y : S¹) → A x y
  F base y = f y
  F (loop i) base = hcomp (λ k → λ { (i = i0) → hom k
                                    ; (i = i1) → hom k })
                          (g (loop i))
  F (loop i) (loop j) = helper i j

wedgeconFun zero (suc m) {A = A} hlev f g hom = F₀
  module _ where
  transpLemma₀ : (x : S₊ (suc m)) → transport (λ i₁ → A base (merid x i₁)) (g base) ≡ f south
  transpLemma₀ x = cong (transport (λ i₁ → A base (merid x i₁)))
                                  hom
              ∙ (λ i → transp (λ j → A base (merid x (i ∨ j))) i
                               (f (merid x i)))

  pathOverMerid₀ : (x : S₊ (suc m)) → PathP (λ i₁ → A base (merid x i₁))
                                            (g base)
                                            (transport (λ i₁ → A base (merid (ptSn (suc m)) i₁))
                                                       (g base))
  pathOverMerid₀ x i = hcomp (λ k → λ { (i = i0) → g base
                                      ; (i = i1) → (transpLemma₀ x ∙ sym (transpLemma₀ (ptSn (suc m)))) k})
                            (transp (λ i₁ → A base (merid x (i₁ ∧ i))) (~ i)
                                    (g base))

  pathOverMeridId₀ : pathOverMerid₀ (ptSn (suc m)) ≡ λ i → transp (λ i₁ → A base (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                                                                 (g base)
  pathOverMeridId₀  =
       (λ j i → hcomp (λ k → λ {(i = i0) → g base
                               ; (i = i1) → rCancel (transpLemma₀ (ptSn (suc m))) j k})
                      (transp (λ i₁ → A base (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                              (g base)))
     ∙ λ j i → hfill (λ k → λ { (i = i0) → g base
                                ; (i = i1) → transport (λ i₁ → A base (merid (ptSn (suc m)) i₁))
                                                        (g base)})
                      (inS (transp (λ i₁ → A base (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                                   (g base))) (~ j)

  indStep₀ : (x : _) (a : _) → PathP (λ i → A x (merid a i))
                                             (g x)
                                             (subst (λ y → A x y) (merid (ptSn (suc m)))
                                                    (g x))
  indStep₀ = wedgeconFun zero m (λ _ _ → isOfHLevelPathP' (2 + m) (hlev _ _) _ _)
                              pathOverMerid₀
                              (λ a i → transp (λ i₁ → A a (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                                               (g a))
                              (sym pathOverMeridId₀)

  F₀ : (x : S¹) (y : Susp (S₊ (suc m))) → A x y
  F₀ x north = g x
  F₀ x south = subst (λ y → A x y) (merid (ptSn (suc m))) (g x)
  F₀ x (merid a i) = indStep₀ x a i
wedgeconFun (suc n) m {A = A} hlev f g hom = F₁
  module _ where
  transpLemma₁ : (x : S₊ (suc n)) → transport (λ i₁ → A (merid x i₁) (ptSn (suc m))) (f (ptSn (suc m))) ≡ g south
  transpLemma₁ x = cong (transport (λ i₁ → A (merid x i₁) (ptSn (suc m))))
                       (sym hom)
                ∙ (λ i → transp (λ j → A (merid x (i ∨ j)) (ptSn (suc m))) i
                                 (g (merid x i)))

  pathOverMerid₁ : (x : S₊ (suc n)) → PathP (λ i₁ → A (merid x i₁) (ptSn (suc m)))
                                            (f (ptSn (suc m)))
                                            (transport (λ i₁ → A (merid (ptSn (suc n)) i₁) (ptSn (suc m)))
                                                       (f (ptSn (suc m))))
  pathOverMerid₁ x i = hcomp (λ k → λ { (i = i0) → f (ptSn (suc m))
                                      ; (i = i1) → (transpLemma₁ x ∙ sym (transpLemma₁ (ptSn (suc n)))) k })
                            (transp (λ i₁ → A (merid x (i₁ ∧ i)) (ptSn (suc m))) (~ i)
                                    (f (ptSn (suc m))))

  pathOverMeridId₁ : pathOverMerid₁ (ptSn (suc n)) ≡ λ i → transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) (ptSn (suc m))) (~ i)
                                                                 (f (ptSn (suc m)))
  pathOverMeridId₁ =
        (λ j i → hcomp (λ k → λ { (i = i0) → f (ptSn (suc m))
                                  ; (i = i1) → rCancel (transpLemma₁ (ptSn (suc n))) j k })
                        (transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) (ptSn (suc m))) (~ i)
                                (f (ptSn (suc m)))))
       ∙ λ j i → hfill (λ k → λ { (i = i0) → f (ptSn (suc m))
                                  ; (i = i1) → transport (λ i₁ → A (merid (ptSn (suc n)) i₁) (ptSn (suc m)))
                                                          (f (ptSn (suc m))) })
                        (inS (transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) (ptSn (suc m))) (~ i)
                                     (f (ptSn (suc m))))) (~ j)

  indStep₁ : (a : _) (y : _) → PathP (λ i → A (merid a i) y)
                                             (f y)
                                             (subst (λ x → A x y) (merid (ptSn (suc n)))
                                                    (f y))
  indStep₁ = wedgeconFun n m (λ _ _ → isOfHLevelPathP' (suc (n + suc m)) (hlev _ _) _ _)
                           (λ a i → transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) a) (~ i)
                                            (f a))
                           pathOverMerid₁
                           pathOverMeridId₁

  F₁ : (x : Susp (S₊ (suc n))) (y : S₊ (suc m))  → A x y
  F₁ north y = f y
  F₁ south y = subst (λ x → A x y) (merid (ptSn (suc n))) (f y)
  F₁ (merid a i) y = indStep₁ a y i
wedgeconRight zero zero {A = A} hlev f g hom = right
  where
  right : (x : S¹) → _
  right base = sym hom
  right (loop i) j = hcomp (λ k → λ { (i = i0) → hom (~ j ∧ k)
                                     ; (i = i1) → hom (~ j ∧ k)
                                     ; (j = i1) → g (loop i) })
                           (g (loop i))
wedgeconRight zero (suc m) {A = A} hlev f g hom x = refl
wedgeconRight (suc n) m {A = A} hlev f g hom = right
  where
  lem : (x : _) → indStep₁ n m hlev f g hom x (ptSn (suc m)) ≡ _
  lem = wedgeconRight n m (λ _ _ → isOfHLevelPathP' (suc (n + suc m)) (hlev _ _) _ _)
                           (λ a i → transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) a) (~ i)
                                            (f a))
                           (pathOverMerid₁ n m hlev f g hom)
                           (pathOverMeridId₁ n m hlev f g hom)

  right : (x : Susp (S₊ (suc n))) → _ ≡ g x
  right north = sym hom
  right south = cong (subst (λ x → A x (ptSn (suc m)))
                            (merid (ptSn (suc n))))
                            (sym hom)
              ∙ λ i → transp (λ j → A (merid (ptSn (suc n)) (i ∨ j)) (ptSn (suc m))) i
                              (g (merid (ptSn (suc n)) i))
  right (merid a i) j =
    hcomp (λ k → λ { (i = i0) → hom (~ j)
                    ; (i = i1) → transpLemma₁ n m hlev f g hom (ptSn (suc n)) j
                    ; (j = i0) → lem a (~ k) i
                    ; (j = i1) → g (merid a i)})
          (hcomp (λ k →  λ { (i = i0) → hom (~ j)
                            ; (i = i1) → compPath-lem (transpLemma₁ n m hlev f g hom a) (transpLemma₁ n m hlev f g hom (ptSn (suc n))) k j
                            ; (j = i1) → g (merid a i)})
                 (hcomp (λ k → λ { (i = i0) → hom (~ j)
                                  ; (j = i0) → transp (λ i₂ → A (merid a (i₂ ∧ i)) (ptSn (suc m))) (~ i)
                                                       (f (ptSn (suc m)))
                                  ; (j = i1) → transp (λ j → A (merid a (i ∧ (j ∨ k))) (ptSn (suc m))) (k ∨ ~ i)
                                                       (g (merid a (i ∧ k))) })
                        (transp (λ i₂ → A (merid a (i₂ ∧ i)) (ptSn (suc m))) (~ i)
                                (hom (~ j)))))
wedgeconLeft zero zero {A = A} hlev f g hom x = refl
wedgeconLeft zero (suc m) {A = A} hlev f g hom = help
  where
  left₁ : (x : _) → indStep₀ m hlev f g hom base x ≡ _
  left₁ = wedgeconLeft zero m (λ _ _ → isOfHLevelPathP' (2 + m) (hlev _ _) _ _)
                              (pathOverMerid₀ m hlev f g hom)
                              (λ a i → transp (λ i₁ → A a (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                                               (g a))
                              (sym (pathOverMeridId₀ m hlev f g hom))

  help : (x : S₊ (suc (suc m))) → _
  help north = hom
  help south = cong (subst (A base) (merid (ptSn (suc m)))) hom
             ∙ λ i → transp (λ j → A base (merid (ptSn (suc m)) (i ∨ j))) i
                             (f (merid (ptSn (suc m)) i))
  help (merid a i) j =
    hcomp (λ k → λ { (i = i0) → hom j
                    ; (i = i1) → transpLemma₀ m hlev f g hom (ptSn (suc m)) j
                    ; (j = i0) → left₁ a (~ k) i
                    ; (j = i1) → f (merid a i)})
          (hcomp (λ k →  λ { (i = i0) → hom j
                            ; (i = i1) → compPath-lem (transpLemma₀ m hlev f g hom a)
                                                       (transpLemma₀ m hlev f g hom (ptSn (suc m))) k j
                            ; (j = i1) → f (merid a i)})
                 (hcomp (λ k → λ { (i = i0) → hom j
                                  ; (j = i0) → transp (λ i₂ → A base (merid a (i₂ ∧ i))) (~ i)
                                                       (g base)
                                  ; (j = i1) → transp (λ j → A base (merid a (i ∧ (j ∨ k)))) (k ∨ ~ i)
                                                       (f (merid a (i ∧ k)))})
                        (transp (λ i₂ → A base (merid a (i₂ ∧ i))) (~ i)
                                (hom j))))
wedgeconLeft (suc n) m {A = A} hlev f g hom _ = refl

---------- Connectedness -----------

sphereConnected : (n : HLevel) → isConnected (suc n) (S₊ n)
sphereConnected n = ∣ ptSn n ∣ , elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
                                     (λ a → sym (spoke ∣_∣ (ptSn n)) ∙ spoke ∣_∣ a)

-- The fact that path spaces of Sn are connected can be proved directly for Sⁿ.
-- (Unfortunately, this does not work for higher paths)
pathIdTruncSⁿ : (n : ℕ) (x y : S₊ (suc n))
             → Path (hLevelTrunc (2 + n) (S₊ (suc n))) ∣ x ∣ ∣ y ∣
             → hLevelTrunc (suc n) (x ≡ y)
pathIdTruncSⁿ n = sphereElim n (λ _ → isOfHLevelΠ (suc n) λ _ → isOfHLevelΠ (suc n)  λ _ → isOfHLevelTrunc (suc n))
                     (sphereElim n (λ _ → isOfHLevelΠ (suc n)  λ _ → isOfHLevelTrunc (suc n))
                       λ _ → ∣ refl ∣)

pathIdTruncSⁿ⁻ : (n : ℕ) (x y : S₊ (suc n))
             → hLevelTrunc (suc n) (x ≡ y)
             → Path (hLevelTrunc (2 + n) (S₊ (suc n))) ∣ x ∣ ∣ y ∣
pathIdTruncSⁿ⁻ n x y = rec (isOfHLevelTrunc (2 + n) _ _)
                           (J (λ y _ → Path (hLevelTrunc (2 + n) (S₊ (suc n))) ∣ x ∣ ∣ y ∣) refl)

pathIdTruncSⁿretract : (n : ℕ) (x y : S₊ (suc n)) → (p : hLevelTrunc (suc n) (x ≡ y)) → pathIdTruncSⁿ n x y (pathIdTruncSⁿ⁻ n x y p) ≡ p
pathIdTruncSⁿretract n =
  sphereElim n (λ _ → isOfHLevelΠ (suc n) λ _ → isOfHLevelΠ (suc n) λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
    λ y → elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
      (J (λ y p → pathIdTruncSⁿ n (ptSn (suc n)) y (pathIdTruncSⁿ⁻ n (ptSn (suc n)) y ∣ p ∣) ≡ ∣ p ∣)
         (cong (pathIdTruncSⁿ n (ptSn (suc n)) (ptSn (suc n))) (transportRefl refl) ∙ pm-help n))
  where
  pm-help : (n : ℕ) → pathIdTruncSⁿ n (ptSn (suc n)) (ptSn (suc n)) refl  ≡ ∣ refl ∣
  pm-help zero = refl
  pm-help (suc n) = refl

isConnectedPathSⁿ : (n : ℕ) (x y : S₊ (suc n)) → isConnected (suc n) (x ≡ y)
isConnectedPathSⁿ n x y =
  isContrRetract
   (pathIdTruncSⁿ⁻ n x y)
   (pathIdTruncSⁿ n x y)
   (pathIdTruncSⁿretract n x y)
     ((isContr→isProp (sphereConnected (suc n)) ∣ x ∣ ∣ y ∣)
      , isProp→isSet (isContr→isProp (sphereConnected (suc n))) _ _ _)

-- Some lemmas on the H space structure on S¹
rUnitS¹ : (x : S¹) → x * base ≡ x
rUnitS¹ base = refl
rUnitS¹ (loop i₁) = refl

commS¹ : (a x : S¹) → a * x ≡ x * a
commS¹ = wedgeconFun _ _ (λ _ _ → isGroupoidS¹ _ _)
         (sym ∘ rUnitS¹)
         rUnitS¹
         refl

assocS¹ : (x y z : S¹) → x * (y * z) ≡ (x * y) * z
assocS¹ = wedgeconFun _ _ (λ _ _ → isSetΠ λ _ → isGroupoidS¹ _ _)
          (λ _ _ → refl)
          (λ x z i → (rUnitS¹ x (~ i)) * z)
          refl

invLooperDistr : (x y : S¹) → invLooper (x * y) ≡ invLooper x * invLooper y
invLooperDistr =
  wedgeconFun 0 0 (λ _ _ → isGroupoidS¹ _ _) (λ _ → refl)
    (λ x → cong invLooper (rUnitS¹ x) ∙ sym (rUnitS¹ (invLooper x)))
    (sym (rUnit refl))

SuspS¹-hom : (a x : S¹)
  → Path (Path (hLevelTrunc 4 (S₊ 2)) _ _)
          (cong ∣_∣ₕ (σ (S₊∙ 1) (a * x)))
          (cong ∣_∣ₕ (σ (S₊∙ 1) a)
        ∙ (cong ∣_∣ₕ (σ (S₊∙ 1) x)))
SuspS¹-hom = wedgeconFun _ _ (λ _ _ → isOfHLevelTrunc 4 _ _ _ _)
           (λ x → lUnit _
                 ∙ cong (_∙ cong ∣_∣ₕ (σ (S₊∙ 1) x))
                        (cong (cong ∣_∣ₕ) (sym (rCancel (merid base)))))
           (λ x → (λ i → cong ∣_∣ₕ (σ (S₊∙ 1) (rUnitS¹ x i)))
               ∙∙ rUnit _
               ∙∙ cong (cong ∣_∣ₕ (σ (S₊∙ 1) x) ∙_)
                       (cong (cong ∣_∣ₕ) (sym (rCancel (merid base)))))
           (sym (l (cong ∣_∣ₕ (σ (S₊∙ 1) base))
                (cong (cong ∣_∣ₕ) (sym (rCancel (merid base))))))
  where
  l : ∀ {ℓ} {A : Type ℓ} {x : A} (p : x ≡ x) (P : refl ≡ p)
    → lUnit p ∙ cong (_∙ p) P ≡ rUnit p ∙ cong (p ∙_) P
  l p = J (λ p P → lUnit p ∙ cong (_∙ p) P ≡ rUnit p ∙ cong (p ∙_) P) refl

rCancelS¹ : (x : S¹) → ptSn 1 ≡ x * (invLooper x)
rCancelS¹ base = refl
rCancelS¹ (loop i) j =
  hcomp (λ r → λ {(i = i0) → base ; (i = i1) → base ; (j = i0) → base})
        base

SuspS¹-inv : (x : S¹) → Path (Path (hLevelTrunc 4 (S₊ 2)) _ _)
                         (cong ∣_∣ₕ (σ (S₊∙ 1) (invLooper x)))
                         (cong ∣_∣ₕ (sym (σ (S₊∙ 1) x)))
SuspS¹-inv x = (lUnit _
       ∙∙ cong (_∙ cong ∣_∣ₕ (σ (S₊∙ 1) (invLooper x)))
               (sym (lCancel (cong ∣_∣ₕ (σ (S₊∙ 1) x))))
                  ∙∙ sym (assoc _ _ _))
       ∙∙ cong (sym (cong ∣_∣ₕ (σ (S₊∙ 1) x)) ∙_) lem
       ∙∙ (assoc _ _ _
       ∙∙ cong (_∙ (cong ∣_∣ₕ (sym (σ (S₊∙ 1) x))))
               (lCancel (cong ∣_∣ₕ (σ (S₊∙ 1) x)))
       ∙∙ sym (lUnit _))
  where
  lem : cong ∣_∣ₕ (σ (S₊∙ 1) x)
      ∙ cong ∣_∣ₕ (σ (S₊∙ 1) (invLooper x))
     ≡ cong ∣_∣ₕ (σ (S₊∙ 1) x)
     ∙ cong ∣_∣ₕ (sym (σ (S₊∙ 1) x))
  lem = sym (SuspS¹-hom x (invLooper x))
     ∙ ((λ i → cong ∣_∣ₕ (σ (S₊∙ 1) (rCancelS¹ x (~ i))))
     ∙ cong (cong ∣_∣ₕ) (rCancel (merid base))) ∙ sym (rCancel _)

-------------------- join Sⁿ Sᵐ ≃ Sⁿ⁺¹⁺ᵐ -------------------------
{-
This section contains a proof that join Sⁿ Sᵐ ≃ Sⁿ⁺ᵐ⁺¹. This is easy using
various properties proved in HITs.Join. However, we would like the map
join Sⁿ Sᵐ → Sⁿ⁺ᵐ⁺¹
to be nice, in particular when n = m = 1. Therefore, we put in some extra work into
the equivalence.
-}

{- We begin with join S¹ S¹ ≃ S³. The iso is induced by: -}
S¹×S¹→S² : S¹ → S¹ → S₊ 2
S¹×S¹→S² base y = north
S¹×S¹→S² (loop i) base = north
S¹×S¹→S² (loop i) (loop j) =
  (sym (rCancel (merid base))
  ∙∙ (λ i → merid (loop i) ∙ sym (merid base))
  ∙∙ rCancel (merid base)) i j

joinS¹S¹→S³ : join S¹ S¹ → S₊ 3
joinS¹S¹→S³ (inl x) = north
joinS¹S¹→S³ (inr x) = south
joinS¹S¹→S³ (push a b i) = merid (S¹×S¹→S² a b) i

{- Proving that this is an equivalence directly is painful,
  so we simply prove that it is equal to the old definition of
  the equivalence join S¹ S¹ ≃ S³ ≃ S₊ 3
  To this end, we start by rephrasing the map -}
private
  3cell : (r i j k : I) → S₊ 3
  3cell r i j k =
    hfill (λ r → λ {(i = i0) → merid (merid base j) (k ∧ ~ r)
                   ; (i = i1) → merid (merid base j) (k ∧ ~ r)
                   ; (j = i0) → merid north (k ∧ ~ r)
                   ; (j = i1) → merid south (k ∧ ~ r)
                   ; (k = i0) → north
                   ; (k = i1) → merid (merid base j) (~ r)})
          (inS (merid (merid (loop i) j) k))
          r

joinS¹S¹→S³' : join S¹ S¹ → S₊ 3
joinS¹S¹→S³' (inl x) = north
joinS¹S¹→S³' (inr x) = north
joinS¹S¹→S³' (push base b i) = north
joinS¹S¹→S³' (push (loop i₁) base i) = north
joinS¹S¹→S³' (push (loop i₁) (loop i₂) i) = 3cell i1 i₁ i₂ i

{- These two maps are equal -}
joinS¹S¹→S³'≡joinS¹S¹→S³' : (x : _) → joinS¹S¹→S³ x ≡ joinS¹S¹→S³' x
joinS¹S¹→S³'≡joinS¹S¹→S³' (inl base) = refl
joinS¹S¹→S³'≡joinS¹S¹→S³' (inl (loop i)) = refl
joinS¹S¹→S³'≡joinS¹S¹→S³' (inr base) = sym (merid north)
joinS¹S¹→S³'≡joinS¹S¹→S³' (inr (loop i)) = sym (merid north)
joinS¹S¹→S³'≡joinS¹S¹→S³' (push base base i) k = merid north (~ k ∧ i)
joinS¹S¹→S³'≡joinS¹S¹→S³' (push base (loop i₁) i) k  = merid north (~ k ∧ i)
joinS¹S¹→S³'≡joinS¹S¹→S³' (push (loop i₁) base i) k =  (merid north) (~ k ∧ i)
joinS¹S¹→S³'≡joinS¹S¹→S³' (push (loop i) (loop j) k) l =
  hcomp (λ r → λ { (i = i0) → merid (sym (rCancel (merid base)) (~ r) j)
                                      (~ l ∧ k)
                  ; (i = i1) → merid (sym (rCancel (merid base)) (~ r) j)
                                      (~ l ∧ k)
                  ; (j = i0) → merid north (~ l ∧ k)
                  ; (j = i1) → merid north (~ l ∧ k)
                  ; (k = i0) → north
                  ; (k = i1) → merid (sym (rCancel (merid base)) (~ r) j) (~ l)
                  ; (l = i0) → merid (doubleCompPath-filler
                                      (sym (rCancel (merid base)))
                                      (cong (σ (S₊∙ 1)) loop)
                                      (rCancel (merid base)) r i j) k
                  ; (l = i1) → 3cell i1 i j k})
    (hcomp (λ r → λ {(i = i0) → merid (cp-fill base r j) (k ∧ ~ l)
                   ; (i = i1) → merid (cp-fill base r j) (k ∧ ~ l)
                   ; (j = i0) → merid north (~ l ∧ k)
                   ; (j = i1) → merid (merid base (~ r)) (~ l ∧ k)
                   ; (k = i0) → north
                   ; (k = i1) → merid (cp-fill base r j) (~ l)
                   ; (l = i0) → merid (cp-fill (loop i) r j) k
                   ; (l = i1) → 3cell i1 i j k})
       (hcomp (λ r → λ {(i = i0) → merid (merid base j) (k ∧ (~ r ∨ ~ l))
                   ; (i = i1) → merid (merid base j) (k ∧ (~ r ∨ ~ l))
                   ; (j = i0) → merid north (k ∧ (~ l ∨ ~ r))
                   ; (j = i1) → merid south (k ∧ (~ l ∨ ~ r))
                   ; (k = i0) → north
                   ; (k = i1) → merid (merid base j) (~ r ∨ ~ l)
                   ; (l = i0) → merid (merid (loop i) j) k
                   ; (l = i1) → 3cell r i j k})
              (merid (merid (loop i) j) k)))
  where
  cp-fill : (a : S¹) → _
  cp-fill a = compPath-filler (merid a) (sym (merid base))

{- joinS¹S¹→S³' is equal to the original
  equivalence (modulo a flipping of interval variables) -}
joinS¹S¹→S³'Id : (x : join S¹ S¹)
  → joinS¹S¹→S³' x ≡ (Iso.fun IsoS³S3 ∘ flip₀₂S³ ∘ joinS¹S¹→S3) x
joinS¹S¹→S³'Id (inl x) = refl
joinS¹S¹→S³'Id (inr x) = refl
joinS¹S¹→S³'Id (push base base i) = refl
joinS¹S¹→S³'Id (push base (loop i₁) i) = refl
joinS¹S¹→S³'Id (push (loop i₁) base i) = refl
joinS¹S¹→S³'Id (push (loop i) (loop j) k) l =
  hcomp (λ r → λ {(i = i0) → merid (merid base (j ∧ ~ l)) (~ r ∧ k)
                 ; (i = i1) → merid (merid base (j ∧ ~ l)) (~ r ∧ k)
                 ; (j = i0) → merid north (k ∧ ~ r)
                 ; (j = i1) → merid (merid base (~ l)) (~ r ∧ k)
                 ; (k = i0) → north
                 ; (k = i1) → merid (merid base (j ∧ ~ l)) (~ r)
                 ; (l = i0) → 3cell r i j k
                 ; (l = i1) → Iso.fun (IsoType→IsoSusp S²IsoSuspS¹)
                                       (meridian-contraction-2 k j i r)})
        (merid (S²Cube i j l) k)
  where
  S²Cube : Cube {A = S₊ 2} (λ j l → merid base (j ∧ ~ l))
                             (λ j l → merid base (j ∧ ~ l))
                             (λ i l → north)
                             (λ i l → merid base (~ l))
                             (λ i j → merid (loop i) j)
                             λ i j → fun S²IsoSuspS¹ (surf j i)
  S²Cube i j l =
    hcomp (λ r → λ {(i = i0) → merid base (j ∧ (~ l ∨ ~ r))
                 ; (i = i1) → merid base (j ∧ (~ l ∨ ~ r))
                 ; (j = i0) → north
                 ; (j = i1) → merid base (~ l ∨ ~ r)
                 ; (l = i0) → merid (loop i) j
                 ; (l = i1) → meridian-contraction j i r})
           (merid (loop i) j)

{-So, finally our map joinS¹S¹→S³ is an iso. We state its inverse explicitly. -}
Iso-joinS¹S¹-S³ : Iso (join S¹ S¹) (S₊ 3)
fun Iso-joinS¹S¹-S³ = joinS¹S¹→S³
inv Iso-joinS¹S¹-S³ = S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3
rightInv Iso-joinS¹S¹-S³ x =
     joinS¹S¹→S³'≡joinS¹S¹→S³'
       ((S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3) x)
  ∙∙ joinS¹S¹→S³'Id ((S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3) x)
  ∙∙ Iso.leftInv (compIso (invIso IsoS³S3)
                  (compIso flip₀₂S³Iso (S³IsojoinS¹S¹))) x
leftInv Iso-joinS¹S¹-S³ x =
     cong (S³→joinS¹S¹ ∘ flip₀₂S³ ∘ inv IsoS³S3)
          (joinS¹S¹→S³'≡joinS¹S¹→S³' x ∙ joinS¹S¹→S³'Id x)
   ∙ Iso.rightInv (compIso (invIso IsoS³S3) (compIso flip₀₂S³Iso (S³IsojoinS¹S¹))) x

{- We now get the full iso Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹ -}
IsoSphereJoin : (n m : ℕ)
  → Iso (join (S₊ n) (S₊ m)) (S₊ (suc (n + m)))
IsoSphereJoin zero zero = compIso (invIso Susp-iso-joinBool) (invIso S¹IsoSuspBool)
IsoSphereJoin zero (suc m) = compIso join-comm (invIso Susp-iso-joinBool)
IsoSphereJoin (suc zero) zero = (invIso Susp-iso-joinBool)
IsoSphereJoin (suc zero) (suc zero) = Iso-joinS¹S¹-S³
IsoSphereJoin (suc zero) (suc (suc m)) =
  compIso join-comm
    (compIso (compIso (Iso-joinSusp-suspJoin {A = S₊∙ (suc m)} {B = S₊∙ (suc zero)})
      (congSuspIso join-comm))
      (congSuspIso (IsoSphereJoin (suc zero) (suc m))))
IsoSphereJoin (suc (suc n)) m =
  compIso (Iso-joinSusp-suspJoin {A = S₊∙ (suc n)} {B = S₊∙ m}) (congSuspIso (IsoSphereJoin (suc n) m))

{- Pointedness holds by refl.
  This is due to the explicit definition of Iso-joinSusp-suspJoin  -}
IsoSphereJoinPres∙ : (n m : ℕ)
  → Iso.fun (IsoSphereJoin n m) (inl (ptSn n)) ≡ ptSn (suc (n + m))
IsoSphereJoinPres∙ zero zero = refl
IsoSphereJoinPres∙ zero (suc m) = refl
IsoSphereJoinPres∙ (suc zero) zero = refl
IsoSphereJoinPres∙ (suc zero) (suc zero) = refl
IsoSphereJoinPres∙ (suc zero) (suc (suc m)) = refl
IsoSphereJoinPres∙ (suc (suc n)) m = refl

IsoSphereJoin⁻Pres∙ : (n m : ℕ)
  → Iso.inv (IsoSphereJoin n m) (ptSn (suc (n + m))) ≡ inl (ptSn n)
IsoSphereJoin⁻Pres∙ n m =
     cong (Iso.inv (IsoSphereJoin n m)) (sym (IsoSphereJoinPres∙ n m))
   ∙ Iso.leftInv (IsoSphereJoin n m) (inl (ptSn n))

-- Inversion on spheres
invSphere : {n : ℕ} → S₊ n → S₊ n
invSphere {n = zero} = not
invSphere {n = (suc zero)} = invLooper
invSphere {n = (suc (suc n))} = invSusp

invSphere² : (n : ℕ) (x : S₊ n) → invSphere (invSphere x) ≡ x
invSphere² zero = notnot
invSphere² (suc zero) base = refl
invSphere² (suc zero) (loop i) = refl
invSphere² (suc (suc n)) = invSusp²

-- Interaction between σ and invSphere
σ-invSphere : (n : ℕ) (x : S₊ (suc n))
                 → σ (S₊∙ (suc n)) (invSphere x)
                 ≡ sym (σ (S₊∙ (suc n)) x)
σ-invSphere zero base =
  rCancel (merid base) ∙∙ refl ∙∙ cong sym (sym (rCancel (merid base)))
σ-invSphere zero (loop i) j =
  hcomp (λ k → λ { (j = i0) → doubleCompPath-filler
                                 (sym (rCancel (merid base)))
                                 (λ i → (σ (S₊∙ 1) (loop (~ i))))
                                 (rCancel (merid base)) (~ k) i
                  ; (j = i1) → doubleCompPath-filler
                                  (sym (cong sym (rCancel (merid base))))
                                  (λ i → sym (σ (S₊∙ 1) (loop i)))
                                  (cong sym (rCancel (merid base))) (~ k) i})
        (sym≡cong-sym  (sym (rCancel (merid base))
                    ∙∙ (λ i → (σ (S₊∙ 1) (loop i)))
                    ∙∙ (rCancel (merid base))) j i)
σ-invSphere (suc n) x = toSusp-invSusp (S₊∙ (suc n)) x

-- Some facts about the map S¹×S¹→S²
-- Todo: generalise to Sⁿ×Sᵐ→Sⁿ⁺ᵐ
S¹×S¹→S²rUnit : (a : S¹) → S¹×S¹→S² a base ≡ north
S¹×S¹→S²rUnit base = refl
S¹×S¹→S²rUnit (loop i) = refl

S¹×S¹→S²x+x : (x : S¹) → S¹×S¹→S² x x ≡ north
S¹×S¹→S²x+x base = refl
S¹×S¹→S²x+x (loop i) k = lem k i
  where
  lem : cong₂ S¹×S¹→S² loop loop ≡ refl
  lem = cong₂Funct S¹×S¹→S² loop loop
    ∙ (λ i → rUnit (cong (λ x → S¹×S¹→S²rUnit x i) loop) (~ i))

S¹×S¹→S²-antiComm : (a b : S¹) → S¹×S¹→S² a b ≡ S¹×S¹→S² b (invLooper a)
S¹×S¹→S²-antiComm base base = refl
S¹×S¹→S²-antiComm base (loop i) = refl
S¹×S¹→S²-antiComm (loop i) base = refl
S¹×S¹→S²-antiComm (loop i) (loop j) k =
  sym≡flipSquare (λ j i → S¹×S¹→S² (loop i) (loop j)) (~ k) i j

private
  S¹×S¹→S²-Distr-filler : (i : I)
    → cong₂ (λ b c → S¹×S¹→S² ((loop i) * b) c) loop loop
    ≡ cong (S¹×S¹→S² (loop i)) loop
  S¹×S¹→S²-Distr-filler i =
    cong₂Funct (λ b c → S¹×S¹→S² ((loop i) * b) c) loop loop
     ∙∙ (λ j → cong (λ x → S¹×S¹→S²rUnit (rotLoop x i) j) loop ∙
                cong (λ c → S¹×S¹→S² (loop i) c) loop)
     ∙∙ sym (lUnit _)

S¹×S¹→S²-Distr : (a b : S¹) → S¹×S¹→S² (a * b) b ≡ S¹×S¹→S² a b
S¹×S¹→S²-Distr a base j = S¹×S¹→S² (rUnitS¹ a j) base
S¹×S¹→S²-Distr base (loop i) k = S¹×S¹→S²-Distr-filler i0 k i
S¹×S¹→S²-Distr (loop i₁) (loop i) k = S¹×S¹→S²-Distr-filler i₁ k i

invSusp∘S¹×S¹→S² : (a b : S¹)
  → S¹×S¹→S² a (invLooper b) ≡ invSusp (S¹×S¹→S² a b)
invSusp∘S¹×S¹→S² base b = merid base
invSusp∘S¹×S¹→S² (loop i) base = merid base
invSusp∘S¹×S¹→S² (loop i) (loop j) k =
  hcomp (λ r → λ {(i = i0) → i-Boundary₂ r j k
                 ; (i = i1) → i-Boundary₂ r j k
                 ; (j = i0) → m-b k
                 ; (j = i1) → m-b k
                 ; (k = i0) → doubleCompPath-filler
                                rCancel-mb⁻¹ (cong σ₁ loop) rCancel-mb r i (~ j)
                 ; (k = i1)
                    → invSusp (doubleCompPath-filler
                                 rCancel-mb⁻¹ (cong σ₁ loop) rCancel-mb r i j)})
   (hcomp (λ r → λ {(i = i0) → i-Boundary r (~ j) k
                   ; (i = i1) → i-Boundary r (~ j) k
                   ; (j = i0) → merid base (~ r ∨ k)
                   ; (j = i1) → merid base (r ∧ k)
                   ; (k = i0) → cp-filler (loop i) r (~ j)
                   ; (k = i1) → invSusp (cp-filler (loop i) r j)})
           (merid (loop i) (~ j)))
  where
  σ₁ = σ (S₊∙ 1)
  m-b = merid base
  rCancel-mb = rCancel m-b
  rCancel-mb⁻¹ = sym (rCancel m-b)

  cp-filler : (a : S¹) (i j : I) → S₊ 2
  cp-filler a i j = compPath-filler (merid a) (sym (merid base)) i j

  i-Boundary : I → I → I → S₊ 2
  i-Boundary r j k =
    hfill (λ r → λ{(j = i0) → m-b (k ∧ r)
                  ; (j = i1) → m-b (~ r ∨ k)
                  ; (k = i0) → cp-filler base r j
                  ; (k = i1) → invSusp (cp-filler base r (~ j))})
          (inS (m-b j))
          r

  i-Boundary₂ : I → I → I → S₊ 2
  i-Boundary₂ r j k =
    hcomp (λ i → λ {(r = i0) → i-Boundary i (~ j) k
                 ; (r = i1) → m-b k
                 ; (j = i0) → m-b (k ∨ (~ i ∧ ~ r))
                 ; (j = i1) → m-b (k ∧ (i ∨ r))
                 ; (k = i0) → rCancel-filler m-b i r (~ j)
                 ; (k = i1) → invSusp (rCancel-filler m-b i r j) })
     (hcomp (λ i → λ {(r = i0) → m-b (~ j ∨ (~ i ∧ k))
                 ; (r = i1) → m-b (k ∨ (~ i ∧ ~ j))
                 ; (j = i0) → m-b (k ∨ (~ r ∨ ~ i))
                 ; (j = i1) → m-b (k ∧ (~ i ∨ r))
                 ; (k = i0) → m-b (~ j ∧ (~ r ∨ ~ i))
                 ; (k = i1) → m-b ((~ j ∨ ~ i) ∨ r) })
            (m-b (~ j ∨ k)))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module Numeral.Finite.Oper where

open import Data
open import Data.Boolean.Stmt
open import Data.Option
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
open import Numeral.Finite as 𝕟 using (𝕟 ; 𝕟₌ ; 𝕟-to-ℕ)
open import Numeral.Finite.Bound
open import Numeral.Natural hiding (𝟎 ; 𝐒 ; 𝐏)
open import Numeral.Natural.Function
open import Numeral.Natural.Function.Proofs
import      Numeral.Natural.Oper as ℕ
import      Numeral.Natural.Oper.Comparisons as ℕ
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Syntax.Number

module Exact where
  -- Predecessor bounded at the minimum (0) for both the value and the maximum.
  -- Example: (𝐏₀(5): 𝕟(8)) = (4: 𝕟(7))
  𝐏₀ : ∀{n} → 𝕟(ℕ.𝐒(ℕ.𝐒(n))) → 𝕟(ℕ.𝐒(n))
  𝐏₀(𝕟.𝟎)    = 𝕟.𝟎
  𝐏₀(𝕟.𝐒(n)) = n

  -- Addition for both the value and the maximum.
  -- Example: (5: 𝕟(8)) + (4: 𝕟(6)) = ((5+4): 𝕟(8+6)) = (9: 𝕟(14))
  _+_ : ∀{b₁ b₂} → 𝕟(b₁) → 𝕟(b₂) → 𝕟(b₁ ℕ.+ b₂)
  _+_ {ℕ.𝐒(b₁)}{ℕ.𝐒(b₂)} 𝕟.𝟎      𝕟.𝟎      = 𝕟.𝟎
  _+_ {ℕ.𝐒(b₁)}{ℕ.𝐒(b₂)} 𝕟.𝟎      (𝕟.𝐒(b)) = 𝕟.𝐒(𝕟.𝟎{b₁} + b)
  _+_ {ℕ.𝐒(b₁)}{ℕ.𝐒(b₂)} (𝕟.𝐒(a)) b        = 𝕟.𝐒(a + b)

  -- Distance between two numbers.
  -- Examples:
  --   (3: 𝕟(8)) 𝄩 (5: 𝕟(6)) = ((3𝄩5): 𝕟(max 8 6)) = (2: 𝕟(8))
  --   (5: 𝕟(8)) 𝄩 (3: 𝕟(6)) = ((5𝄩3): 𝕟(max 8 6)) = (2: 𝕟(8))
  --   (7: 𝕟(8)) 𝄩 (0: 𝕟(6)) = ((7𝄩0): 𝕟(max 8 6)) = (7: 𝕟(8))
  _𝄩_ : ∀{b₁ b₂} → 𝕟(b₁) → 𝕟(b₂) → 𝕟(max b₁ b₂)
  _𝄩_ {ℕ.𝐒 b₁}       {ℕ.𝐒 b₂}       𝕟.𝟎     𝕟.𝟎     = 𝕟.𝟎
  _𝄩_ {ℕ.𝐒 ℕ.𝟎}      {ℕ.𝐒 b₂}       𝕟.𝟎     (𝕟.𝐒 b) = 𝕟.𝐒 b
  _𝄩_ {ℕ.𝐒 (ℕ.𝐒 b₁)} {ℕ.𝐒 b₂}       𝕟.𝟎     (𝕟.𝐒 b) = 𝕟.𝐒(𝕟.𝟎 𝄩 b)
  _𝄩_ {ℕ.𝐒 b₁}       {ℕ.𝐒 b₂}       (𝕟.𝐒 a) (𝕟.𝐒 b) = bound-𝐒(a 𝄩 b)
  _𝄩_ {ℕ.𝐒 b₁}       {ℕ.𝐒 ℕ.𝟎}      (𝕟.𝐒 a) 𝕟.𝟎     = 𝕟.𝐒 a
  _𝄩_ {ℕ.𝐒 b₁}       {ℕ.𝐒 (ℕ.𝐒 b₂)} (𝕟.𝐒 a) 𝕟.𝟎     = 𝕟.𝐒(a 𝄩 𝕟.𝟎)

  _⋅_ : ∀{b₁ b₂} → 𝕟(b₁) → 𝕟(b₂) → 𝕟(b₁ ℕ.⋅ b₂)
  _⋅_ {ℕ.𝐒 b₁} {ℕ.𝐒 b₂} a 𝕟.𝟎     = 𝕟.𝟎
  _⋅_ {ℕ.𝐒 b₁} {ℕ.𝐒 b₂} a (𝕟.𝐒 b) = a + (a ⋅ b)

module Bounded where
  -- Predecessor bounded at the minimum (0) for the value only.
  -- Example: (𝐏₀(5): 𝕟(8)) = (4: 𝕟(8))
  𝐏₀ : ∀{n} → 𝕟(n) → 𝕟(n)
  𝐏₀ {ℕ.𝐒(b)} (𝕟.𝟎)         = 𝕟.𝟎
  𝐏₀ {ℕ.𝐒(b)} (𝕟.𝐒(𝕟.𝟎))    = 𝕟.𝟎
  𝐏₀ {ℕ.𝐒(b)} (𝕟.𝐒(𝕟.𝐒(n))) = 𝕟.𝐒(𝐏₀ {b} (𝕟.𝐒(n)))

module Total where
  𝐒 : ∀{b} → (n : 𝕟(b)) → ⦃ _ : IsTrue(ℕ.𝐒(𝕟-to-ℕ (n)) ℕ.<? b) ⦄ → 𝕟(b)
  𝐒 {ℕ.𝐒(ℕ.𝐒(b))} (𝕟.𝟎)    = 𝕟.𝐒(𝕟.𝟎)
  𝐒 {ℕ.𝐒(ℕ.𝐒(b))} (𝕟.𝐒(n)) = 𝕟.𝐒(𝐒(n))

module Optional where
  minimum : ∀{n} → Option(𝕟(n))
  minimum{ℕ.𝟎}    = None
  minimum{ℕ.𝐒(_)} = Some 𝕟.minimum

  maximum : ∀{n} → Option(𝕟(n))
  maximum{ℕ.𝟎}    = None
  maximum{ℕ.𝐒(n)} = Some 𝕟.maximum

  _+₀ₗ_ : ∀{b₁ b₂} → Option(𝕟(b₁)) → 𝕟(b₂) → 𝕟(b₁ ℕ.+ b₂)
  _+₀ₗ_      None     𝕟.𝟎      = 𝕟.𝟎
  _+₀ₗ_ {b₁} None     (𝕟.𝐒(b)) = 𝕟.𝐒(_+₀ₗ_ {b₁} None b)
  _+₀ₗ_      (Some a) b        = a Exact.+ b

  _+₀ᵣ_ : ∀{b₁ b₂} → 𝕟(b₁) → Option(𝕟(b₂)) → 𝕟(b₁ ℕ.+ b₂)
  _+₀ᵣ_ 𝕟.𝟎      None     = 𝕟.𝟎
  _+₀ᵣ_ (𝕟.𝐒(a)) None     = 𝕟.𝐒(_+₀ᵣ_ a None)
  {-# CATCHALL #-}
  _+₀ᵣ_ a        (Some b) = a Exact.+ b

module Unclosed where
  _+ₙₗ_ : ∀{b₂} → (b₁ : ℕ) → 𝕟(b₂) → 𝕟(b₁ ℕ.+ b₂)
  ℕ.𝟎    +ₙₗ b = b
  ℕ.𝐒(a) +ₙₗ b = 𝕟.𝐒(a +ₙₗ b)

  _+ₙᵣ_ : ∀{b₁} → 𝕟(b₁) → (b₂ : ℕ) → 𝕟(b₁ ℕ.+ b₂)
  a +ₙᵣ ℕ.𝟎    = a
  a +ₙᵣ ℕ.𝐒(b) = 𝕟.𝐒(a +ₙᵣ b)

  -- Example: shrink-subtract(5) (7 : 𝕟(6 + 5)) = (2 : 𝕟(6))
  shrink-subtractₗ : ∀{b₁} → (b₂ : ℕ) → 𝕟(ℕ.𝐒(b₁) ℕ.+ b₂) → 𝕟(ℕ.𝐒(b₁))
  shrink-subtractₗ          _        𝕟.𝟎     = 𝕟.𝟎
  shrink-subtractₗ          ℕ.𝟎      (𝕟.𝐒 a) = 𝕟.𝐒 a
  shrink-subtractₗ {ℕ.𝟎}    (ℕ.𝐒 b₂) (𝕟.𝐒 a) = 𝕟.𝟎
  shrink-subtractₗ {ℕ.𝐒 b₁} (ℕ.𝐒 b₂) (𝕟.𝐒 a) = shrink-subtractₗ {ℕ.𝐒 b₁} (b₂) (a)

  shrink-subtractᵣ : (b₁ : ℕ) → ∀{b₂} → 𝕟(b₁ ℕ.+ ℕ.𝐒(b₂)) → 𝕟(ℕ.𝐒(b₂))
  shrink-subtractᵣ _                 𝕟.𝟎     = 𝕟.𝟎
  shrink-subtractᵣ ℕ.𝟎               (𝕟.𝐒 a) = 𝕟.𝐒 a
  shrink-subtractᵣ (ℕ.𝐒 b₁) {ℕ.𝟎}    (𝕟.𝐒 a) = 𝕟.𝟎
  shrink-subtractᵣ (ℕ.𝐒 b₁) {ℕ.𝐒 b₂} (𝕟.𝐒 a) = shrink-subtractᵣ (b₁) {ℕ.𝐒 b₂} (a)

  {-_⋅ₙₗ_ : ∀{b₂} → (b₁ : ℕ) → 𝕟(b₂) → 𝕟(ℕ.𝐒(b₁ ℕ.⋅ b₂))
  _⋅ₙₗ_ {ℕ.𝐒 _} ℕ.𝟎     _ = 𝕟.𝟎
  _⋅ₙₗ_ {ℕ.𝐒 _} (ℕ.𝐒 a) b = {!b Exact.+ (a ⋅ₙₗ b)!}
  -}

  _⋅ₙᵣ_ : ∀{b₁} → 𝕟(b₁) → (b₂ : ℕ) → 𝕟(ℕ.𝐒(b₁ ℕ.⋅ b₂)) -- TODO: Bounds is too great
  _⋅ₙᵣ_ {ℕ.𝐒 _} a ℕ.𝟎     = 𝕟.𝟎
  _⋅ₙᵣ_ {ℕ.𝐒 _} a (ℕ.𝐒 b) = a Exact.+ (a ⋅ₙᵣ b)

module Wrapping where
  -- Wrapping subtraction.
  -- Essentially: _[−]_ {b₁}{b₂} a b = (a −ℤ b) mod b₁
  _[−]_ : ∀{b₁ b₂} → 𝕟(b₁) → 𝕟(b₂) → 𝕟(b₁)
  _[−]_ {_}      {ℕ.𝐒 _}  a       𝕟.𝟎     = a
  _[−]_ {ℕ.𝐒 b₁} {ℕ.𝐒 _}  𝕟.𝟎     (𝕟.𝐒 b) = 𝕟.maximum {b₁} [−] b
  _[−]_ {ℕ.𝐒 b₁} {ℕ.𝐒 b₂} (𝕟.𝐒 a) (𝕟.𝐒 b) = _[−]_ {ℕ.𝐒 b₁}{b₂} (bound-𝐒 a) b

  -- Wrapping negation (Flipping around the symmetric point).
  -- Essentially: [−]_ {b} n = (−ℤ n) mod b
  [−]_ : ∀{b} → 𝕟(b) → 𝕟(b)
  [−]_ {ℕ.𝐒 b} n = 𝕟.maximum {b} [−] n

{- TODO: Cannot solve first. Unsure why
[𝐒]-not-0 : ∀{b : ℕ}{n : 𝕟(ℕ.𝐒(b))} → (𝐒{b}(n) ≢ 𝟎{ℕ.𝐒(b)})
[𝐒]-not-0 ()

𝐏keep : ∀{b} → (n : 𝕟(𝐒(b))) → ⦃ _ : n ≢ 𝟎 ⦄ → 𝕟(𝐒(b))
𝐏keep {ℕ.𝟎}    (𝟎)       ⦃ proof ⦄ with proof([≡]-intro)
... | ()
𝐏keep {ℕ.𝐒(b)} (𝟎)       ⦃ _ ⦄     = 𝟎
𝐏keep {ℕ.𝐒(b)} (𝐒(𝟎))    ⦃ _ ⦄     = 𝟎
𝐏keep {ℕ.𝐒(b)} (𝐒(𝐒(n))) ⦃ proof ⦄ = 𝐒(𝐏keep {b} (𝐒(n)) ⦃ [𝐒]-not-0 ⦄)
-}

-- _ : ∀{b} → (n : 𝕟(b)) → (𝕟-to-ℕ (n) < b)

-- _+small_ : ∀{b₁ b₂} → (x : 𝕟(𝐒(b₁))) → (y : 𝕟(𝐒(b₂))) → 𝕟(ℕ.𝐒(𝕟-to-ℕ (x) ℕ.+ 𝕟-to-ℕ (y)))
-- _+small_      𝟎       𝟎      = 𝟎
-- _+small_ {b₁} (𝐒(a))  𝟎      = 𝐒(a +small 𝟎)
-- _+small_      a       (𝐒(b)) = 𝐒(a +small b)

-- _−small_ : ∀{b} → (x : 𝕟(𝐒(b))) → (y : 𝕟(ℕ.𝐒(𝕟-to-ℕ (x)))) → 𝕟(ℕ.𝐒(𝕟-to-ℕ (x) ℕ.−₀ 𝕟-to-ℕ (y)))
-- 𝟎    −small 𝟎    = 𝟎
-- 𝐒(a) −small 𝟎    = 𝐒(a −small 𝟎)
-- 𝐒(a) −small 𝐒(b) = a −small b

{- TODO: Will not work like this
-- Modulo subtraction.
-- Essentially: a [−] b mod n = (a −ℤ b) mod n
_[−]_mod_ : ℕ → ℕ → (n : ℕ) → 𝕟₌(n)
_    [−] _    mod 𝟎    = 𝟎
𝟎    [−] 𝟎    mod 𝐒(n) = 𝟎
𝐒(a) [−] 𝟎    mod 𝐒(n) = a [−] n mod 𝐒(n)
𝟎    [−] 𝐒(b) mod 𝐒(n) = n [−] b mod 𝐒(n)
𝐒(a) [−] 𝐒(b) mod 𝐒(n) = a [−] b mod 𝐒(n)

open import Data
test1 : [−]_ {4} 1 ≡ 3
test1 = [≡]-intro
-}

-- _−_ : ∀{b} → (x : 𝕟(𝐒(b))) → (y : 𝕟(ℕ.𝐒(𝕟-to-ℕ (x)))) → 𝕟(𝐒(b))
-- 𝟎    − 𝟎    = 𝟎
-- 𝐒(a) − 𝟎    = 𝐒(a)
-- 𝐒(a) − 𝐒(b) = bound-𝐒(a − b)

-- TODO: Wrapping and bounded operations

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:
------------------------------------------------------------------------
-- The circle with an erased higher constructor
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- Partly following the HoTT book.

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the circle uses path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Circle.Erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Circle eq as C using (𝕊¹)
open import Equality.Groupoid equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PE
open import Erased.Cubical eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import Group equality-with-J as G using (_≃ᴳ_)
open import H-level equality-with-J
open import H-level.Truncation.Propositional.Erased eq as T using (∥_∥ᴱ)
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹)
open import H-level.Truncation.Propositional.One-step.Erased eq as OE
  using (∥_∥¹ᴱ)
open import Integer equality-with-J using (ℤ; +_; ℤ-group)
open import Nat equality-with-J
open import Pointed-type equality-with-J as PT using (_≃ᴮ_)
open import Pointed-type.Homotopy-group eq

private
  variable
    a p : Level
    A   : Type p
    P   : A → Type p
    b ℓ : A

------------------------------------------------------------------------
-- The type and some eliminators

-- The circle.

data 𝕊¹ᴱ : Type where
  base     : 𝕊¹ᴱ
  @0 loopᴾ : base P.≡ base

@0 loop : base ≡ base
loop = _↔_.from ≡↔≡ loopᴾ

-- A dependent eliminator, expressed using paths.

elimᴾ :
  (P : 𝕊¹ᴱ → Type p)
  (b : P base) →
  @0 P.[ (λ i → P (loopᴾ i)) ] b ≡ b →
  (x : 𝕊¹ᴱ) → P x
elimᴾ P b ℓ base      = b
elimᴾ P b ℓ (loopᴾ i) = ℓ i

-- A non-dependent eliminator, expressed using paths.

recᴾ : (b : A) → @0 b P.≡ b → 𝕊¹ᴱ → A
recᴾ = elimᴾ _

-- A dependent eliminator.

elim :
  (P : 𝕊¹ᴱ → Type p)
  (b : P base) →
  @0 subst P loop b ≡ b →
  (x : 𝕊¹ᴱ) → P x
elim P b ℓ = elimᴾ P b (subst≡→[]≡ ℓ)

-- A "computation" rule.

@0 elim-loop :
  dcong (elim P b ℓ) loop ≡ ℓ
elim-loop = dcong-subst≡→[]≡ (refl _)

-- Every dependent function of type (x : 𝕊¹ᴱ) → P x can be expressed
-- using elim.

η-elim :
  {f : (x : 𝕊¹ᴱ) → P x} →
  f ≡ elim P (f base) (dcong f loop)
η-elim {P = P} {f = f} =
  ⟨ext⟩ $ elim _ (refl _)
    (subst (λ x → f x ≡ elim P (f base) (dcong f loop) x) loop (refl _)  ≡⟨ subst-in-terms-of-trans-and-dcong ⟩

     trans (sym (dcong f loop))
       (trans (cong (subst P loop) (refl _))
          (dcong (elim P (f base) (dcong f loop)) loop))                 ≡⟨ cong (trans (sym (dcong f loop))) $
                                                                            trans (cong (flip trans _) $ cong-refl _) $
                                                                            trans-reflˡ _ ⟩
     trans (sym (dcong f loop))
       (dcong (elim P (f base) (dcong f loop)) loop)                     ≡⟨ cong (trans (sym (dcong f loop))) elim-loop ⟩

     trans (sym (dcong f loop)) (dcong f loop)                           ≡⟨ trans-symˡ _ ⟩∎

     refl _                                                              ∎)

-- A non-dependent eliminator.

rec : (b : A) → @0 b ≡ b → 𝕊¹ᴱ → A
rec b ℓ = recᴾ b (_↔_.to ≡↔≡ ℓ)

-- A "computation" rule.

@0 rec-loop : cong (rec b ℓ) loop ≡ ℓ
rec-loop = cong-≡↔≡ (refl _)

-- Every function from 𝕊¹ᴱ to A can be expressed using rec.

η-rec : {f : 𝕊¹ᴱ → A} → f ≡ rec (f base) (cong f loop)
η-rec {f = f} =
  ⟨ext⟩ $ elim _ (refl _)
    (subst (λ x → f x ≡ rec (f base) (cong f loop) x) loop (refl _)      ≡⟨ subst-in-terms-of-trans-and-cong ⟩

     trans (sym (cong f loop))
       (trans (refl _) (cong (rec (f base) (cong f loop)) loop))         ≡⟨ cong (trans (sym (cong f loop))) $ trans-reflˡ _ ⟩

     trans (sym (cong f loop)) (cong (rec (f base) (cong f loop)) loop)  ≡⟨ cong (trans (sym (cong f loop))) rec-loop ⟩

     trans (sym (cong f loop)) (cong f loop)                             ≡⟨ trans-symˡ _ ⟩∎

     refl _                                                              ∎)

------------------------------------------------------------------------
-- Conversion functions

-- In erased contexts 𝕊¹ is equivalent to 𝕊¹ᴱ.

@0 𝕊¹≃𝕊¹ᴱ : 𝕊¹ ≃ 𝕊¹ᴱ
𝕊¹≃𝕊¹ᴱ = Eq.↔→≃
  𝕊¹→𝕊¹ᴱ
  𝕊¹ᴱ→𝕊¹
  (elim _ (refl _)
     (subst (λ x → 𝕊¹→𝕊¹ᴱ (𝕊¹ᴱ→𝕊¹ x) ≡ x) loop (refl _)  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym (cong (𝕊¹→𝕊¹ᴱ ∘ 𝕊¹ᴱ→𝕊¹) loop))
        (trans (refl _) (cong id loop))                  ≡⟨ cong (trans _) $
                                                            trans (trans-reflˡ _) $
                                                            sym $ cong-id _ ⟩

      trans (sym (cong (𝕊¹→𝕊¹ᴱ ∘ 𝕊¹ᴱ→𝕊¹) loop)) loop     ≡⟨ cong (flip trans _) $ cong sym $
                                                            trans (sym $ cong-∘ _ _ _) $
                                                            trans (cong (cong 𝕊¹→𝕊¹ᴱ)
                                                                   rec-loop) $
                                                            C.rec-loop ⟩

      trans (sym loop) loop                              ≡⟨ trans-symˡ _ ⟩∎

      refl _                                             ∎))
  (C.elim _ (refl _)
     (subst (λ x → 𝕊¹ᴱ→𝕊¹ (𝕊¹→𝕊¹ᴱ x) ≡ x) C.loop (refl _)  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym (cong (𝕊¹ᴱ→𝕊¹ ∘ 𝕊¹→𝕊¹ᴱ) C.loop))
        (trans (refl _) (cong id C.loop))                  ≡⟨ cong (trans _) $
                                                              trans (trans-reflˡ _) $
                                                              sym $ cong-id _ ⟩

      trans (sym (cong (𝕊¹ᴱ→𝕊¹ ∘ 𝕊¹→𝕊¹ᴱ) C.loop)) C.loop   ≡⟨ cong (flip trans _) $ cong sym $
                                                              trans (sym $ cong-∘ _ _ _) $
                                                              trans (cong (cong 𝕊¹ᴱ→𝕊¹)
                                                                     C.rec-loop) $
                                                              rec-loop ⟩

      trans (sym C.loop) C.loop                            ≡⟨ trans-symˡ _ ⟩∎

      refl _                                               ∎))
  where
  𝕊¹→𝕊¹ᴱ = C.rec base loop
  𝕊¹ᴱ→𝕊¹ = rec C.base C.loop

-- In erased contexts there is a based equivalence between 𝕊¹ , C.base
-- and 𝕊¹ᴱ , base.

@0 𝕊¹≃ᴮ𝕊¹ᴱ : (𝕊¹ , C.base) ≃ᴮ (𝕊¹ᴱ , base)
𝕊¹≃ᴮ𝕊¹ᴱ = 𝕊¹≃𝕊¹ᴱ , refl _

-- The one-step truncation of the unit type is equivalent to 𝕊¹ᴱ.
--
-- Paolo Capriotti informed me about the corresponding result without
-- erasure.

∥⊤∥¹ᴱ≃𝕊¹ᴱ : ∥ ⊤ ∥¹ᴱ ≃ 𝕊¹ᴱ
∥⊤∥¹ᴱ≃𝕊¹ᴱ = _↔_.from ≃↔≃ $ PE.↔→≃
  (OE.recᴾ λ where
     .OE.∣∣ʳ _            → base
     .OE.∣∣-constantʳ _ _ → loopᴾ)
  (recᴾ OE.∣ _ ∣ (OE.∣∣-constantᴾ _ _))
  (elimᴾ _ P.refl (λ _ → P.refl))
  (OE.elimᴾ λ where
     .OE.∣∣ʳ _              → P.refl
     .OE.∣∣-constantʳ _ _ _ → P.refl)

------------------------------------------------------------------------
-- The loop space of 𝕊¹ᴱ

-- The function trans is commutative for the loop space of 𝕊¹ᴱ.

trans-commutative : (p q : base ≡ base) → trans p q ≡ trans q p
trans-commutative =
  flip $ Transitivity-commutative.commutative base _∙_ ∙-base base-∙
  where
  _∙_ : 𝕊¹ᴱ → 𝕊¹ᴱ → 𝕊¹ᴱ
  x ∙ y = rec x (elim (λ x → x ≡ x) loop lemma x) y
    where
    @0 lemma : subst (λ x → x ≡ x) loop loop ≡ loop
    lemma = ≡⇒↝ _ (sym [subst≡]≡[trans≡trans]) (refl _)

  base-∙ : ∀ x → x ∙ base ≡ x
  base-∙ _ = refl _

  ∙-base : ∀ y → base ∙ y ≡ y
  ∙-base =
    elim _ (refl _)
      (subst (λ x → rec base loop x ≡ x) loop (refl _)         ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (rec base loop) loop))
         (trans (refl _) (cong id loop))                       ≡⟨ cong (trans _) $ trans-reflˡ _ ⟩

       trans (sym (cong (rec base loop) loop)) (cong id loop)  ≡⟨ cong₂ (trans ∘ sym)
                                                                    rec-loop
                                                                    (sym $ cong-id _) ⟩

       trans (sym loop) loop                                   ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                  ∎)

-- The loop space is equivalent to x ≡ x, for any x : 𝕊¹ᴱ.

base≡base≃≡ : {x : 𝕊¹ᴱ} → (base ≡ base) ≃ (x ≡ x)
base≡base≃≡ = elim
  (λ x → (base ≡ base) ≃ (x ≡ x))
  Eq.id
  (Eq.lift-equality ext $ ⟨ext⟩ λ eq →
   _≃_.to (subst (λ x → (base ≡ base) ≃ (x ≡ x)) loop Eq.id) eq        ≡⟨ cong (_$ eq) Eq.to-subst ⟩
   subst (λ x → base ≡ base → x ≡ x) loop id eq                        ≡⟨ subst-→ ⟩
   subst (λ x → x ≡ x) loop (subst (λ _ → base ≡ base) (sym loop) eq)  ≡⟨ cong (subst (λ x → x ≡ x) loop) $ subst-const _ ⟩
   subst (λ x → x ≡ x) loop eq                                         ≡⟨ ≡⇒↝ _ (sym [subst≡]≡[trans≡trans]) (

       trans eq loop                                                        ≡⟨ trans-commutative _ _ ⟩∎
       trans loop eq                                                        ∎) ⟩∎

   eq                                                                  ∎)
  _

-- In erased contexts the loop space of 𝕊¹ᴱ is equivalent to the type
-- of integers.

@0 base≡base≃ℤ : (base ≡ base) ≃ ℤ
base≡base≃ℤ =
  base ≡ base      ↝⟨ Eq.≃-≡ 𝕊¹≃𝕊¹ᴱ ⟩
  C.base ≡ C.base  ↝⟨ C.base≡base≃ℤ univ ⟩□
  ℤ                □

-- In erased contexts the fundamental group of 𝕊¹ᴱ is equivalent to
-- the group of integers.

@0 Fundamental-group≃ℤ : Fundamental-group (𝕊¹ᴱ , base) ≃ᴳ ℤ-group
Fundamental-group≃ℤ =
  G.↝ᴳ-trans (G.≃ᴳ-sym $ ≃ᴮ→≃ᴳ _ _ 0 𝕊¹≃ᴮ𝕊¹ᴱ)
    (C.Fundamental-group≃ℤ univ)

-- 𝕊¹ᴱ is a groupoid (in erased contexts).

@0 𝕊¹ᴱ-groupoid : H-level 3 𝕊¹ᴱ
𝕊¹ᴱ-groupoid =   $⟨ (λ {_ _ _ _} → C.𝕊¹-groupoid univ) ⟩
  H-level 3 𝕊¹   ↝⟨ H-level-cong _ 3 𝕊¹≃𝕊¹ᴱ ⦂ (_ → _) ⟩□
  H-level 3 𝕊¹ᴱ  □

-- The type of endofunctions on 𝕊¹ᴱ is equivalent to
-- ∃ λ (x : 𝕊¹ᴱ) → Erased (x ≡ x).

𝕊¹ᴱ→𝕊¹ᴱ≃Σ𝕊¹ᴱ-Erased≡ : (𝕊¹ᴱ → 𝕊¹ᴱ) ≃ ∃ λ (x : 𝕊¹ᴱ) → Erased (x ≡ x)
𝕊¹ᴱ→𝕊¹ᴱ≃Σ𝕊¹ᴱ-Erased≡ = Eq.↔→≃ to from to-from from-to
  where
  to : (𝕊¹ᴱ → 𝕊¹ᴱ) → ∃ λ (x : 𝕊¹ᴱ) → Erased (x ≡ x)
  to f = f base , [ cong f loop ]

  from : (∃ λ (x : 𝕊¹ᴱ) → Erased (x ≡ x)) → (𝕊¹ᴱ → 𝕊¹ᴱ)
  from (x , [ eq ]) = rec x eq

  to-from : ∀ p → to (from p) ≡ p
  to-from (x , [ eq ]) = cong (x ,_)
    ([ cong (rec x eq) loop ]  ≡⟨ []-cong [ rec-loop ] ⟩∎
     [ eq ]                    ∎)

  from-to : ∀ f → from (to f) ≡ f
  from-to f =
    rec (f base) (cong f loop)  ≡⟨ sym η-rec ⟩∎
    f                           ∎

-- The type of endofunctions on 𝕊¹ᴱ is equivalent to 𝕊¹ᴱ × Erased ℤ.

𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ : (𝕊¹ᴱ → 𝕊¹ᴱ) ≃ (𝕊¹ᴱ × Erased ℤ)
𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ =
  (𝕊¹ᴱ → 𝕊¹ᴱ)                       ↝⟨ 𝕊¹ᴱ→𝕊¹ᴱ≃Σ𝕊¹ᴱ-Erased≡ ⟩
  (∃ λ (x : 𝕊¹ᴱ) → Erased (x ≡ x))  ↝⟨ (∃-cong λ _ → Erased-cong (inverse base≡base≃≡)) ⟩
  𝕊¹ᴱ × Erased (base ≡ base)        ↝⟨ (∃-cong λ _ → Erased-cong base≡base≃ℤ) ⟩□
  𝕊¹ᴱ × Erased ℤ                    □

-- The forward direction of 𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ maps the identity
-- function to base , [ + 1 ].

𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ-id :
  _≃_.to 𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ id ≡ (base , [ + 1 ])
𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ-id = _≃_.from-to 𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ
  (rec base (cong (_≃_.to 𝕊¹≃𝕊¹ᴱ) (trans (refl C.base) C.loop))  ≡⟨ cong (λ ([ ℓ ]) → rec base ℓ) $ []-cong [ lemma ] ⟩
   rec base (cong id loop)                                       ≡⟨ sym η-rec ⟩∎
   id                                                            ∎)
  where
  @0 lemma : _
  lemma =
    cong (_≃_.to 𝕊¹≃𝕊¹ᴱ) (trans (refl C.base) C.loop)  ≡⟨ cong (cong (_≃_.to 𝕊¹≃𝕊¹ᴱ)) $ trans-reflˡ _ ⟩
    cong (_≃_.to 𝕊¹≃𝕊¹ᴱ) C.loop                        ≡⟨ C.rec-loop ⟩
    loop                                               ≡⟨ cong-id _ ⟩∎
    cong id loop                                       ∎

-- The forward direction of 𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ maps the constant
-- function returning base to base , [ + 0 ].

𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ-const :
  _≃_.to 𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ (const base) ≡ (base , [ + 0 ])
𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ-const = _≃_.from-to 𝕊¹ᴱ→𝕊¹ᴱ≃𝕊¹ᴱ×Erased-ℤ
  (rec base (cong (_≃_.to 𝕊¹≃𝕊¹ᴱ) (refl C.base))  ≡⟨ cong (λ ([ ℓ ]) → rec base ℓ) $ []-cong [ lemma ] ⟩
   rec base (cong (const base) loop)              ≡⟨ sym η-rec ⟩∎
   const base                                     ∎)
  where
  @0 lemma : _
  lemma =
    cong (_≃_.to 𝕊¹≃𝕊¹ᴱ) (refl C.base)  ≡⟨ cong-refl _ ⟩
    refl _                              ≡⟨ sym $ cong-const _ ⟩∎
    cong (const base) loop              ∎

------------------------------------------------------------------------
-- Some negative results

-- The equality loop is not equal to refl base.

loop≢refl : loop ≢ refl base
loop≢refl =
  Stable-¬
    [ loop ≡ refl base                                                  ↔⟨ inverse $ Eq.≃-≡ $ inverse $ Eq.≃-≡ $ inverse 𝕊¹≃𝕊¹ᴱ ⟩
      cong (_≃_.from 𝕊¹≃𝕊¹ᴱ) loop ≡ cong (_≃_.from 𝕊¹≃𝕊¹ᴱ) (refl base)  ↝⟨ trans (sym rec-loop) ∘ flip trans (cong-refl _) ⟩
      C.loop ≡ refl C.base                                              ↝⟨ C.loop≢refl ⟩□
      ⊥                                                                 □
    ]

-- 𝕊¹ᴱ is not a set.

¬-𝕊¹ᴱ-set : ¬ Is-set 𝕊¹ᴱ
¬-𝕊¹ᴱ-set =
  Stable-¬
    [ Is-set 𝕊¹ᴱ  ↝⟨ H-level-cong _ 2 $ inverse 𝕊¹≃𝕊¹ᴱ ⟩
      Is-set 𝕊¹   ↝⟨ C.¬-𝕊¹-set ⟩□
      ⊥           □
    ]

-- It is not necessarily the case that the one-step truncation of a
-- proposition is a proposition.

¬-Is-proposition-∥∥¹ᴱ :
  ¬ ({A : Type a} → Is-proposition A → Is-proposition ∥ A ∥¹ᴱ)
¬-Is-proposition-∥∥¹ᴱ {a = a} =
  Stable-¬
    [ ({A : Type a} → Is-proposition A → Is-proposition ∥ A ∥¹ᴱ)  ↝⟨ (implicit-∀-cong _ $ ∀-cong _ λ _ → H-level-cong _ 1 O.∥∥¹ᴱ≃∥∥¹) ⟩
      ({A : Type a} → Is-proposition A → Is-proposition ∥ A ∥¹)   ↝⟨ C.¬-Is-proposition-∥∥¹ ⟩□
      ⊥                                                           □
    ]

-- A function with the type of refl (for 𝕊¹ᴱ) that is not equal to
-- refl. The function is available in erased contexts.

@0 not-refl : (x : 𝕊¹ᴱ) → x ≡ x
not-refl x =                             $⟨ C.not-refl (_≃_.from 𝕊¹≃𝕊¹ᴱ x) ⟩
  _≃_.from 𝕊¹≃𝕊¹ᴱ x ≡ _≃_.from 𝕊¹≃𝕊¹ᴱ x  ↝⟨ Eq.≃-≡ $ inverse 𝕊¹≃𝕊¹ᴱ ⟩□
  x ≡ x                                  □

-- The function not-refl is not equal to refl.

not-refl≢refl : not-refl ≢ refl
not-refl≢refl =
  Stable-¬
    [ not-refl ≡ refl                                                    ↔⟨⟩

      _≃_.to (Eq.≃-≡ $ inverse 𝕊¹≃𝕊¹ᴱ) ∘ C.not-refl ∘ _≃_.from 𝕊¹≃𝕊¹ᴱ ≡
      refl                                                               ↝⟨ flip trans (⟨ext⟩ lemma) ⟩

      _≃_.to (Eq.≃-≡ $ inverse 𝕊¹≃𝕊¹ᴱ) ∘ C.not-refl ∘ _≃_.from 𝕊¹≃𝕊¹ᴱ ≡
      _≃_.to (Eq.≃-≡ $ inverse 𝕊¹≃𝕊¹ᴱ) ∘ refl ∘ _≃_.from 𝕊¹≃𝕊¹ᴱ          ↔⟨ (Eq.≃-≡ $ inverse $
                                                                             Π-cong ext (inverse 𝕊¹≃𝕊¹ᴱ) λ _ →
                                                                             inverse $ Eq.≃-≡ $ inverse 𝕊¹≃𝕊¹ᴱ) ⟩

      C.not-refl ≡ refl                                                  ↝⟨ C.not-refl≢refl ⟩□

      ⊥                                                                  □
    ]
  where
  @0 lemma : _
  lemma x = sym $ _≃_.from-to (Eq.≃-≡ $ Eq.inverse 𝕊¹≃𝕊¹ᴱ)
    (_≃_.from (Eq.≃-≡ $ Eq.inverse 𝕊¹≃𝕊¹ᴱ) (refl x)  ≡⟨⟩
     cong (_≃_.from 𝕊¹≃𝕊¹ᴱ) (refl x)                 ≡⟨ cong-refl _ ⟩∎
     refl (_≃_.from 𝕊¹≃𝕊¹ᴱ x)                        ∎)

-- For every universe level there is a type A such that
-- (x : A) → x ≡ x is not a proposition.

¬-type-of-refl-propositional :
  ∃ λ (A : Type a) → ¬ Is-proposition ((x : A) → x ≡ x)
¬-type-of-refl-propositional {a = a} =
    ↑ _ 𝕊¹ᴱ
  , Stable-¬
      [ Is-proposition ((x : ↑ _ 𝕊¹ᴱ) → x ≡ x)  ↝⟨ (H-level-cong _ 1 $
                                                    Π-cong ext (↑-cong $ inverse 𝕊¹≃𝕊¹ᴱ) λ _ →
                                                    inverse $ Eq.≃-≡ $ ↑-cong $ inverse 𝕊¹≃𝕊¹ᴱ) ⟩
        Is-proposition ((x : ↑ _ 𝕊¹) → x ≡ x)   ↝⟨ proj₂ C.¬-type-of-refl-propositional ⟩□
        ⊥                                       □
      ]

-- Every value of type 𝕊¹ᴱ is merely equal to the base point (using
-- ∥_∥ᴱ to express "merely").
--
-- A variant of this lemma was mentioned by Mike Shulman in a blog
-- post (http://homotopytypetheory.org/2013/07/24/cohomology/).

all-points-on-the-circle-are-merely-equal :
  (x : 𝕊¹ᴱ) → ∥ x ≡ base ∥ᴱ
all-points-on-the-circle-are-merely-equal =
  elim _
       T.∣ refl base ∣
       (T.truncation-is-proposition _ _)

-- Every value of type 𝕊¹ᴱ is not not equal to the base point.

all-points-on-the-circle-are-¬¬-equal :
  (x : 𝕊¹ᴱ) → ¬ ¬ x ≡ base
all-points-on-the-circle-are-¬¬-equal x =
  Stable-¬
    [ x ≢ base                    ↔⟨ →-cong ext (inverse $ Eq.≃-≡ $ inverse 𝕊¹≃𝕊¹ᴱ) Eq.id ⟩
      _≃_.from 𝕊¹≃𝕊¹ᴱ x ≢ C.base  ↝⟨ C.all-points-on-the-circle-are-¬¬-equal _ ⟩□
      ⊥                           □
    ]

-- It is not the case that every value of type 𝕊¹ᴱ is equal to the
-- base point.

¬-all-points-on-the-circle-are-equal :
  ¬ ((x : 𝕊¹ᴱ) → x ≡ base)
¬-all-points-on-the-circle-are-equal =
  Stable-¬
    [ ((x : 𝕊¹ᴱ) → x ≡ base)   ↔⟨ (Π-cong ext (inverse 𝕊¹≃𝕊¹ᴱ) λ _ →
                                   inverse $ Eq.≃-≡ $ Eq.inverse 𝕊¹≃𝕊¹ᴱ) ⟩
      ((x : 𝕊¹) → x ≡ C.base)  ↝⟨ C.¬-all-points-on-the-circle-are-equal ⟩□
      ⊥                        □
    ]

-- Double-negation shift for Type-valued predicates over 𝕊¹ᴱ does not
-- hold in general.

¬-double-negation-shift :
  ¬ ({P : 𝕊¹ᴱ → Type} → ((x : 𝕊¹ᴱ) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹ᴱ) → P x))
¬-double-negation-shift =
  Stable-¬
    [ ({P : 𝕊¹ᴱ → Type} → ((x : 𝕊¹ᴱ) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹ᴱ) → P x))  ↔⟨ (implicit-Π-cong ext
                                                                                (→-cong₁ {k₂ = equivalence} ext $ inverse 𝕊¹≃𝕊¹ᴱ) λ _ →
                                                                              →-cong ext (inverse $ Π-cong ext 𝕊¹≃𝕊¹ᴱ λ _ → Eq.id) $
                                                                              ¬-cong ext $ ¬-cong ext $ inverse $ Π-cong ext 𝕊¹≃𝕊¹ᴱ λ _ → Eq.id) ⟩
      ({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x))     ↝⟨ C.¬-double-negation-shift ⟩□
      ⊥                                                                   □
    ]

-- H-level.Closure.proj₁-closure cannot be generalised by replacing
-- the assumption ∀ a → B a with ∀ a → ∥ B a ∥ᴱ.
--
-- A variant of this observation is due to Andrea Vezzosi.

¬-generalised-proj₁-closure :
  ¬ ({A : Type} {B : A → Type} →
     (∀ a → ∥ B a ∥ᴱ) →
     ∀ n → H-level n (Σ A B) → H-level n A)
¬-generalised-proj₁-closure generalised-proj₁-closure =
                                  $⟨ singleton-contractible _ ⟩
  Contractible (Σ 𝕊¹ᴱ (_≡ base))  ↝⟨ generalised-proj₁-closure
                                       all-points-on-the-circle-are-merely-equal
                                       0 ⟩
  Contractible 𝕊¹ᴱ                ↝⟨ ¬-𝕊¹ᴱ-set ∘ mono (zero≤ 2) ⟩□
  ⊥                               □

-- There is no based equivalence between 𝕊¹ᴱ and the product of 𝕊¹ᴱ
-- with itself.

𝕊¹ᴱ≄ᴮ𝕊¹ᴱ×𝕊¹ᴱ : ¬ (𝕊¹ᴱ , base) ≃ᴮ ((𝕊¹ᴱ , base) PT.× (𝕊¹ᴱ , base))
𝕊¹ᴱ≄ᴮ𝕊¹ᴱ×𝕊¹ᴱ =
  Stable-¬
    [ (𝕊¹ᴱ , base) ≃ᴮ ((𝕊¹ᴱ , base) PT.× (𝕊¹ᴱ , base))     ↝⟨ PT.↝ᴮ-trans 𝕊¹≃ᴮ𝕊¹ᴱ ∘
                                                              flip PT.↝ᴮ-trans (PT.≃ᴮ-sym (𝕊¹≃ᴮ𝕊¹ᴱ PT.×-cong-≃ᴮ 𝕊¹≃ᴮ𝕊¹ᴱ)) ⟩
      (𝕊¹ , C.base) ≃ᴮ ((𝕊¹ , C.base) PT.× (𝕊¹ , C.base))  ↝⟨ C.𝕊¹≄ᴮ𝕊¹×𝕊¹ ⟩□
      ⊥                                                    □
    ]

-- 𝕊¹ᴱ is not equivalent to 𝕊¹ᴱ × 𝕊¹ᴱ.

𝕊¹ᴱ≄𝕊¹ᴱ×𝕊¹ᴱ : ¬ 𝕊¹ᴱ ≃ (𝕊¹ᴱ × 𝕊¹ᴱ)
𝕊¹ᴱ≄𝕊¹ᴱ×𝕊¹ᴱ =
  Stable-¬
    [ 𝕊¹ᴱ ≃ (𝕊¹ᴱ × 𝕊¹ᴱ)  ↔⟨ Eq.≃-preserves ext (inverse 𝕊¹≃𝕊¹ᴱ) (inverse $ 𝕊¹≃𝕊¹ᴱ ×-cong 𝕊¹≃𝕊¹ᴱ) ⟩
      𝕊¹ ≃ (𝕊¹ × 𝕊¹)     ↝⟨ C.𝕊¹≄𝕊¹×𝕊¹ ⟩□
      ⊥                  □
    ]

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module _ (_ : Set) where

open import Imports.Issue5198 Set

data D : Set where
  r : D

F : D → Set₂
F r = R

f : {d : D} → F d → F d
f x = x

_ : R
_ = f record {A = Set}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-01-12, issue #2386

postulate
  A : Set

data _≡_ (x : A) : A → Set where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

-- Monomorphic equality is not accepted.

-- If needed, this could change in the future.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Data.These where

open import Light.Level using (Setω ; Level)
open import Light.Variable.Levels
open import Light.Variable.Sets

record Dependencies : Setω where

record Library (dependencies : Dependencies) : Setω where
      field
            ℓf : Level → Level → Level
            These : Set aℓ → Set bℓ → Set (ℓf aℓ bℓ)
            this : 𝕒 → These 𝕒 𝕓
            that : 𝕓 → These 𝕒 𝕓
            these : 𝕒 → 𝕓 → These 𝕒 𝕓
open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.meta:25 #-}
module NoBlockOnLevel where

open import Common.Level
open import Common.Product

BSetoid : ∀ c → Set (lsuc c)
BSetoid c = Set c

infixr 0 _⟶_

postulate
  _⟶_ : ∀ {f t} → BSetoid f → BSetoid t → Set (f ⊔ t)
  →-to-⟶ : ∀ {a b} {A : Set a} {B : BSetoid b} →
           (A → B) → A ⟶ B

postulate
  a b p : Level
  A : Set a
  B : Set b
  P : A → B → Set p

-- This will leave unsolved metas if we give up on an unsolved level constraint
-- when checking argument spines. Since we can't match on levels it's safe to keep
-- checking later constraints even if they depend on the unsolved levels.
f : (∃ λ x → ∃ λ y → P x y) ⟶ (∃ λ y → ∃ λ x → P x y)
f = →-to-⟶ λ p → proj₁ (proj₂ p) , proj₁ p , proj₂ (proj₂ p)


text:
-- {-# OPTIONS -v term:20 -v tc.term:20  #-}
-- {-# OPTIONS -v tc.def.alias:100 -v tc.term.expr.coind:100 #-}
module Issue807 where

open import Common.Coinduction

data Stream : Set where
  cons : ∞ Stream → Stream

mutual

  -- s : Stream
  s = cons s′

  -- s′ : ∞ _
  s′ = ♯ s

-- Under 2.3.0.1: The code is accepted.
-- Under 2.3.2:   The termination checker complains.

-- Bug was that aliases did not lead to construction of ♯-auxiliary function.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --erased-cubical --save-metas #-}

module Erased-cubical-Pattern-matching-Erased where

open import Agda.Builtin.String
open import Erased-cubical-Pattern-matching-Cubical

-- If c₁ and c₂ are treated as erased, then f might be compiled to
-- something akin to ⊥-elim. However, the main module uses
-- --cubical, not --erased-cubical, so f should not be compiled in
-- that way.

f : D → String
f c₁ = "Success\n"
f c₂ = "Failure\n"

max_stars_repo_name: sseefried/agda


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

module Type.Cubical.InductiveInterval where

open import Functional
import      Lvl
open import Type
import      Type.Cubical             as Cubical
import      Type.Cubical.Path        as Cubical
import      Type.Cubical.Path.Proofs as Cubical

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable A B P : Type{ℓ}

data Interval : Type{Lvl.𝟎} where
  𝟎 : Interval
  𝟏 : Interval
  segment : Cubical.Path 𝟎 𝟏

elim : (P : Interval → Type{ℓ}) → (p0 : P(𝟎)) → (p1 : P(𝟏)) → (Cubical.PathP(\i → P(segment i)) p0 p1) → ((i : Interval) → P(i))
elim(P) p0 _  _  𝟎           = p0
elim(P) _  p1 _  𝟏           = p1
elim(P) _  _  ps (segment i) = ps(i)

flip : Interval → Interval
flip 𝟎 = 𝟏
flip 𝟏 = 𝟎
flip (segment i) = segment(Cubical.Interval.flip i)

min : Interval → Interval → Interval
min 𝟎 𝟎 = 𝟎
min 𝟎 𝟏 = 𝟎
min 𝟏 𝟎 = 𝟎
min 𝟏 𝟏 = 𝟏
min 𝟎           (segment i) = 𝟎
min 𝟏           (segment i) = segment i
min (segment i) 𝟎           = 𝟎
min (segment i) 𝟏           = segment i
min (segment i) (segment j) = segment(Cubical.Interval.min i j)

max : Interval → Interval → Interval
max = flip ∘₂ (min on₂ flip)

open import Structure.Relator.Properties
open import Type.Cubical.Path.Equality
open import Type.Properties.Singleton

instance
  Interval-unit : IsUnit(Interval)
  IsUnit.unit Interval-unit = 𝟏
  IsUnit.uniqueness Interval-unit {𝟎} = segment
  IsUnit.uniqueness Interval-unit {𝟏} = reflexivity(Cubical.Path)
  IsUnit.uniqueness Interval-unit {segment i} j = segment(Cubical.Interval.max i j)

transp : (P : Interval → Type{ℓ}) → P(𝟎) → P(𝟏)
transp(P) = sub₂(Cubical.Path)(_→ᶠ_) (Cubical.map P(segment))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to negation
------------------------------------------------------------------------

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

module Relation.Nullary.Negation where

open import Category.Monad
open import Data.Bool.Base using (Bool; false; true; if_then_else_)
open import Data.Empty
open import Data.Product as Prod
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Function
open import Level
open import Relation.Nullary
open import Relation.Unary

contradiction : ∀ {p w} {P : Set p} {Whatever : Set w} →
                P → ¬ P → Whatever
contradiction p ¬p = ⊥-elim (¬p p)

contraposition : ∀ {p q} {P : Set p} {Q : Set q} →
                 (P → Q) → ¬ Q → ¬ P
contraposition f ¬q p = contradiction (f p) ¬q

-- Note also the following use of flip:

private
  note : ∀ {p q} {P : Set p} {Q : Set q} →
         (P → ¬ Q) → Q → ¬ P
  note = flip

-- If we can decide P, then we can decide its negation.

¬? : ∀ {p} {P : Set p} → Dec P → Dec (¬ P)
¬? (yes p) = no (λ ¬p → ¬p p)
¬? (no ¬p) = yes ¬p

------------------------------------------------------------------------
-- Quantifier juggling

∃⟶¬∀¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
        ∃ P → ¬ (∀ x → ¬ P x)
∃⟶¬∀¬ = flip uncurry

∀⟶¬∃¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
        (∀ x → P x) → ¬ ∃ λ x → ¬ P x
∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)

¬∃⟶∀¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
        ¬ ∃ (λ x → P x) → ∀ x → ¬ P x
¬∃⟶∀¬ = curry

∀¬⟶¬∃ : ∀ {a p} {A : Set a} {P : A → Set p} →
        (∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
∀¬⟶¬∃ = uncurry

∃¬⟶¬∀ : ∀ {a p} {A : Set a} {P : A → Set p} →
        ∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
∃¬⟶¬∀ = flip ∀⟶¬∃¬

------------------------------------------------------------------------
-- Double-negation

¬¬-map : ∀ {p q} {P : Set p} {Q : Set q} →
         (P → Q) → ¬ ¬ P → ¬ ¬ Q
¬¬-map f = contraposition (contraposition f)

-- Stability under double-negation.

Stable : ∀ {ℓ} → Set ℓ → Set ℓ
Stable P = ¬ ¬ P → P

-- Everything is stable in the double-negation monad.

stable : ∀ {p} {P : Set p} → ¬ ¬ Stable P
stable ¬[¬¬p→p] = ¬[¬¬p→p] (λ ¬¬p → ⊥-elim (¬¬p (¬[¬¬p→p] ∘ const)))

-- Negated predicates are stable.

negated-stable : ∀ {p} {P : Set p} → Stable (¬ P)
negated-stable ¬¬¬P P = ¬¬¬P (λ ¬P → ¬P P)

-- Decidable predicates are stable.

decidable-stable : ∀ {p} {P : Set p} → Dec P → Stable P
decidable-stable (yes p) ¬¬p = p
decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)

¬-drop-Dec : ∀ {p} {P : Set p} → Dec (¬ ¬ P) → Dec (¬ P)
¬-drop-Dec (yes ¬¬p) = no ¬¬p
¬-drop-Dec (no ¬¬¬p) = yes (negated-stable ¬¬¬p)

-- Double-negation is a monad (if we assume that all elements of ¬ ¬ P
-- are equal).

¬¬-Monad : ∀ {p} → RawMonad (λ (P : Set p) → ¬ ¬ P)
¬¬-Monad = record
  { return = contradiction
  ; _>>=_  = λ x f → negated-stable (¬¬-map f x)
  }

¬¬-push : ∀ {p q} {P : Set p} {Q : P → Set q} →
          ¬ ¬ ((x : P) → Q x) → (x : P) → ¬ ¬ Q x
¬¬-push ¬¬P⟶Q P ¬Q = ¬¬P⟶Q (λ P⟶Q → ¬Q (P⟶Q P))

-- A double-negation-translated variant of excluded middle (or: every
-- nullary relation is decidable in the double-negation monad).

excluded-middle : ∀ {p} {P : Set p} → ¬ ¬ Dec P
excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))

-- If Whatever is instantiated with ¬ ¬ something, then this function
-- is call with current continuation in the double-negation monad, or,
-- if you will, a double-negation translation of Peirce's law.
--
-- In order to prove ¬ ¬ P one can assume ¬ P and prove ⊥. However,
-- sometimes it is nice to avoid leaving the double-negation monad; in
-- that case this function can be used (with Whatever instantiated to
-- ⊥).

call/cc : ∀ {w p} {Whatever : Set w} {P : Set p} →
          ((P → Whatever) → ¬ ¬ P) → ¬ ¬ P
call/cc hyp ¬p = hyp (λ p → ⊥-elim (¬p p)) ¬p

-- The "independence of premise" rule, in the double-negation monad.
-- It is assumed that the index set (Q) is inhabited.

independence-of-premise
  : ∀ {p q r} {P : Set p} {Q : Set q} {R : Q → Set r} →
    Q → (P → Σ Q R) → ¬ ¬ (Σ[ x ∈ Q ] (P → R x))
independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
  where
  helper : Dec P → _
  helper (yes p) = Prod.map id const (f p)
  helper (no ¬p) = (q , ⊥-elim ∘′ ¬p)

-- The independence of premise rule for binary sums.

independence-of-premise-⊎
  : ∀ {p q r} {P : Set p} {Q : Set q} {R : Set r} →
    (P → Q ⊎ R) → ¬ ¬ ((P → Q) ⊎ (P → R))
independence-of-premise-⊎ {P = P} f = ¬¬-map helper excluded-middle
  where
  helper : Dec P → _
  helper (yes p) = Sum.map const const (f p)
  helper (no ¬p) = inj₁ (⊥-elim ∘′ ¬p)

private

  -- Note that independence-of-premise-⊎ is a consequence of
  -- independence-of-premise (for simplicity it is assumed that Q and
  -- R have the same type here):

  corollary : ∀ {p ℓ} {P : Set p} {Q R : Set ℓ} →
              (P → Q ⊎ R) → ¬ ¬ ((P → Q) ⊎ (P → R))
  corollary {P = P} {Q} {R} f =
    ¬¬-map helper (independence-of-premise
                     true ([ _,_ true , _,_ false ] ∘′ f))
    where
    helper : ∃ (λ b → P → if b then Q else R) → (P → Q) ⊎ (P → R)
    helper (true  , f) = inj₁ f
    helper (false , f) = inj₂ f

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

Excluded-Middle : (ℓ : Level) → Set (suc ℓ)
Excluded-Middle p = {P : Set p} → Dec P
{-# WARNING_ON_USAGE Excluded-Middle
"Warning: Excluded-Middle was deprecated in v1.0.
Please use ExcludedMiddle from `Axiom.ExcludedMiddle` instead."
#-}

Double-Negation-Elimination : (ℓ : Level) → Set (suc ℓ)
Double-Negation-Elimination p = {P : Set p} → Stable P
{-# WARNING_ON_USAGE Double-Negation-Elimination
"Warning: Double-Negation-Elimination was deprecated in v1.0.
Please use DoubleNegationElimination from `Axiom.DoubleNegationElimination` instead."
#-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Strings
------------------------------------------------------------------------

module Data.String where

open import Data.List as List using (_∷_; []; List)
open import Data.Vec as Vec using (Vec)
open import Data.Colist as Colist using (Colist)
open import Data.Char as Char using (Char)
open import Data.Bool using (Bool; true; false)
open import Function
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary
open import Relation.Binary.List.StrictLex as StrictLex
import Relation.Binary.On as On
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe

import Data.String.Core as Core
open Core public using (String)
open Core

-- Possibly infinite strings.

Costring : Set
Costring = Colist Char

------------------------------------------------------------------------
-- Operations

infixr 5 _++_

_++_ : String → String → String
_++_ = primStringAppend

toList : String → List Char
toList = primStringToList

fromList : List Char → String
fromList = primStringFromList

toList∘fromList : ∀ s → toList (fromList s) ≡ s
toList∘fromList s = trustMe

fromList∘toList : ∀ s → fromList (toList s) ≡ s
fromList∘toList s = trustMe

toVec : (s : String) → Vec Char (List.length (toList s))
toVec s = Vec.fromList (toList s)

toCostring : String → Costring
toCostring = Colist.fromList ∘ toList

unlines : List String → String
unlines []       = ""
unlines (x ∷ xs) = x ++ "\n" ++ unlines xs

show : String → String
show = primShowString

-- Informative equality test.

_≟_ : Decidable {A = String} _≡_
s₁ ≟ s₂ with primStringEquality s₁ s₂
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _

-- Boolean equality test.
--
-- Why is the definition _==_ = primStringEquality not used? One
-- reason is that the present definition can sometimes improve type
-- inference, at least with the version of Agda that is current at the
-- time of writing: see unit-test below.

infix 4 _==_

_==_ : String → String → Bool
s₁ == s₂ = ⌊ s₁ ≟ s₂ ⌋

private

  -- The following unit test does not type-check (at the time of
  -- writing) if _==_ is replaced by primStringEquality.

  data P : (String → Bool) → Set where
    p : (c : String) → P (_==_ c)

  unit-test : P (_==_ "")
  unit-test = p _

setoid : Setoid _ _
setoid = PropEq.setoid String

decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_

-- Lexicographic ordering of strings.

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder =
  On.strictTotalOrder
    (StrictLex.<-strictTotalOrder Char.strictTotalOrder)
    toList