text:
{-# OPTIONS --without-K --safe #-}
module Source.Term where

open import Source.Size as S using
  ( Size ; _<_ ; Δ ; Δ′ ; Δ″ ; Ω ; Ω′ ; Ω″ ; n ; m ; o ; b ; v0 ; v1 ; ⋆ )
open import Source.Size.Substitution.Theory
open import Source.Size.Substitution.Canonical as SC using () renaming
  ( Sub⊢ to Subₛ⊢ )
open import Source.Size.Substitution.Universe as SU using
  ( ⟨_⟩ ) renaming
  ( Sub⊢ᵤ to Subₛ⊢ᵤ )
open import Source.Type as T using
  ( Type ; Ctx ; T ; U ; V ; Γ ; Γ′ ; Γ″ ; Ψ ; Ψ′ ; Ψ″ ; SubTheory-Type
  ; SubTheory-Ctx )
open import Util.Prelude hiding (id ; _∘_)

open Ctx
open S.Ctx
open S.Size
open S.Var
open Type

infix  0 _,_⊢_∶_ _,_⊢ₓ_∶_ Sub⊢
infix  3 _⊇_
infixl 5 sub-syntax-Termₛ sub-syntax-Subₛ sub-syntax-Term sub-syntax-⊇
infixr 6 Λ_,_ Λₛ_,_
infixl 7 _·_ _·ₛ_

Var : Set
Var = ℕ

variable x y : Var

data Term Δ : Set where
  var : (x : Var) → Term Δ
  Λ_,_ : (T : Type Δ) (t : Term Δ) → Term Δ
  _·_ : (t u : Term Δ) → Term Δ
  Λₛ_,_ : (n : Size Δ) (t : Term (Δ ∙ n)) → Term Δ
  _·ₛ_ : (t : Term Δ) (m : Size Δ) → Term Δ
  zero : (n : Size Δ) → Term Δ
  suc : (n m : Size Δ) (i : Term Δ) → Term Δ
  cons : (i : Term Δ) (n : Size Δ) (is : Term Δ) → Term Δ
  head : (n : Size Δ) (is : Term Δ) → Term Δ
  tail : (n : Size Δ) (is : Term Δ) (m : Size Δ) → Term Δ
  caseNat : (T : Type Δ) (n : Size Δ) (i : Term Δ) (z : Term Δ) (s : Term Δ)
    → Term Δ
  fix : (T : Type (Δ ∙ ⋆)) (t : Term Δ) (n : Size Δ) → Term Δ

variable t u v w i is z s t′ u′ v′ w′ i′ is′ z′ s′ : Term Δ

data _,_⊢ₓ_∶_ : ∀ Δ (Γ : Ctx Δ) (x : Var) (T : Type Δ) → Set where
  zero
    : Δ , Γ ∙ T ⊢ₓ zero ∶ T
  suc
    : (⊢x : Δ , Γ ⊢ₓ x ∶ T)
    → Δ , Γ ∙ U ⊢ₓ suc x ∶ T

data _,_⊢_∶_ : ∀ Δ (Γ : Ctx Δ) (t : Term Δ) (T : Type Δ) → Set where
  var
    : (⊢x : Δ , Γ ⊢ₓ x ∶ T)
    → Δ , Γ ⊢ var x ∶ T
  abs
    : (⊢t : Δ , Γ ∙ T ⊢ t ∶ U)
    → Δ , Γ ⊢ Λ T , t ∶ T ⇒ U
  app
    : (⊢t : Δ , Γ ⊢ t ∶ T ⇒ U)
    → (⊢u : Δ , Γ ⊢ u ∶ T)
    → Δ , Γ ⊢ t · u ∶ U
  absₛ
    : (⊢t : Δ ∙ n , Ψ ⊢ t ∶ T)
    → Ψ ≡ Γ [ SC.Wk ]
    → Δ , Γ ⊢ Λₛ n , t ∶ Π n , T
  appₛ
    : (m<n : m < n)
    → (⊢t : Δ , Γ ⊢ t ∶ (Π n , T))
    → U ≡ T [ SC.Sing m ]
    → Δ , Γ ⊢ t ·ₛ m ∶ U
  zero
    : (n<⋆ : n < ⋆)
    → Δ , Γ ⊢ zero n ∶ Nat n
  suc
    : (n<⋆ : n < ⋆)
    → (m<n : m < n)
    → (⊢i : Δ , Γ ⊢ i ∶ Nat m)
    → Δ , Γ ⊢ suc n m i ∶ Nat n
  cons
    : (n<⋆ : n < ⋆)
    → (⊢i : Δ , Γ ⊢ i ∶ Nat ∞)
    → (⊢is : Δ , Γ ⊢ is ∶ Π n , Stream v0)
    → Δ , Γ ⊢ cons i n is ∶ Stream n
  head
    : (n<⋆ : n < ⋆)
    → (⊢is : Δ , Γ ⊢ is ∶ Stream n)
    → Δ , Γ ⊢ head n is ∶ Nat ∞
  tail
    : (n<⋆ : n < ⋆)
    → (m<n : m < n)
    → (⊢is : Δ , Γ ⊢ is ∶ Stream n)
    → Δ , Γ ⊢ tail n is m ∶ Stream m
  caseNat
    : (n<⋆ : n < ⋆)
    → (⊢i : Δ , Γ ⊢ i ∶ Nat n)
    → (⊢z : Δ , Γ ⊢ z ∶ T)
    → (⊢s : Δ , Γ ⊢ s ∶ Π n , Nat v0 ⇒ U)
    → U ≡ T [ SC.Wk ]
    → Δ , Γ ⊢ caseNat T n i z s ∶ T
  fix
    : (n<⋆ : n < ⋆)
    → (⊢t : Δ , Γ ⊢ t ∶ Π ⋆ , (Π v0 , U) ⇒ T)
    → U ≡ T [ SC.Skip ]
    → V ≡ T [ SC.Sing n ]
    → Δ , Γ ⊢ fix T t n ∶ V

subₛ : SC.Sub Δ Ω → Term Ω → Term Δ
subₛ σ (var x) = var x
subₛ σ (Λ T , t) = Λ T [ σ ] , subₛ σ t
subₛ σ (t · u) = subₛ σ t · subₛ σ u
subₛ σ (Λₛ n , t) = Λₛ n [ σ ] , subₛ (SC.Lift σ) t
subₛ σ (t ·ₛ m) = subₛ σ t ·ₛ (m [ σ ])
subₛ σ (zero n) = zero (n [ σ ])
subₛ σ (suc n m i) = suc (n [ σ ]) (m [ σ ]) (subₛ σ i)
subₛ σ (cons i n is) = cons (subₛ σ i) (n [ σ ]) (subₛ σ is)
subₛ σ (head n is) = head (n [ σ ]) (subₛ σ is)
subₛ σ (tail n is m) = tail (n [ σ ]) (subₛ σ is) (m [ σ ])
subₛ σ (caseNat T n i z s)
  = caseNat (T [ σ ]) (n [ σ ]) (subₛ σ i) (subₛ σ z) (subₛ σ s)
subₛ σ (fix T t n) = fix (T [ SC.Lift σ ]) (subₛ σ t) (n [ σ ])

sub-syntax-Termₛ = subₛ

syntax sub-syntax-Termₛ σ t = t [ σ ]ₛ

abstract
  subₛ-resp-⊢ₓ : ∀ {σ}
    → σ ∶ Δ ⇒ Ω
    → Ω , Γ ⊢ₓ x ∶ T
    → Δ , Γ [ σ ] ⊢ₓ x ∶ T [ σ ]
  subₛ-resp-⊢ₓ ⊢σ zero = zero
  subₛ-resp-⊢ₓ ⊢σ (suc ⊢x) = suc (subₛ-resp-⊢ₓ ⊢σ ⊢x)

  subₛ-resp-⊢ : ∀ {σ}
    → σ ∶ Δ ⇒ Ω
    → Ω , Γ ⊢ t ∶ T
    → Δ , Γ [ σ ] ⊢ subₛ σ t ∶ T [ σ ]
  subₛ-resp-⊢ ⊢σ (var ⊢x) = var (subₛ-resp-⊢ₓ ⊢σ ⊢x)
  subₛ-resp-⊢ ⊢σ (abs ⊢t) = abs (subₛ-resp-⊢ ⊢σ ⊢t)
  subₛ-resp-⊢ ⊢σ (app ⊢t ⊢u) = app (subₛ-resp-⊢ ⊢σ ⊢t) (subₛ-resp-⊢ ⊢σ ⊢u)
  subₛ-resp-⊢ {Δ} {Γ = Γ} {σ = σ} ⊢σ (absₛ {Ψ = Ψ} ⊢t p)
    = absₛ (subₛ-resp-⊢ (SC.Lift⊢ ⊢σ refl) ⊢t) eq
    where
      eq : Ψ [ SC.Lift σ ] ≡ Γ [ σ ] [ SC.Wk ]
      eq = trans (cong (λ Ψ → Ψ [ SC.Lift σ ]) p)
        ([>>]″ (SC.Lift σ) SC.Wk SC.Wk σ Γ SC.Lift>>Wk)
  subₛ-resp-⊢ {σ = σ} ⊢σ (appₛ {m = m} {T = T} {U = U} m<n ⊢t p)
    = appₛ (SC.sub-resp-< ⊢σ m<n) (subₛ-resp-⊢ ⊢σ ⊢t) eq
    where
      eq : U [ σ ] ≡ T [ SC.Lift σ ] [ SC.Sing (m [ σ ]) ]
      eq = trans (cong (λ U → U [ σ ]) p)
        ([>>]″ _ _ _ _ _ (sym (SC.Sing>>Lift m)))
  subₛ-resp-⊢ ⊢σ (zero n<⋆)
    = zero (SC.sub-resp-< ⊢σ n<⋆)
  subₛ-resp-⊢ ⊢σ (suc n<⋆ m<n ⊢i)
    = suc (SC.sub-resp-< ⊢σ n<⋆) (SC.sub-resp-< ⊢σ m<n) (subₛ-resp-⊢ ⊢σ ⊢i)
  subₛ-resp-⊢ ⊢σ (cons n<⋆ ⊢i ⊢is)
    = cons (SC.sub-resp-< ⊢σ n<⋆) (subₛ-resp-⊢ ⊢σ ⊢i) (subₛ-resp-⊢ ⊢σ ⊢is)
  subₛ-resp-⊢ ⊢σ (head n<⋆ ⊢is)
    = head (SC.sub-resp-< ⊢σ n<⋆) (subₛ-resp-⊢ ⊢σ ⊢is)
  subₛ-resp-⊢ ⊢σ (tail n<⋆ m<n ⊢is)
    = tail (SC.sub-resp-< ⊢σ n<⋆) (SC.sub-resp-< ⊢σ m<n) (subₛ-resp-⊢ ⊢σ ⊢is)
  subₛ-resp-⊢ {σ = σ} ⊢σ (caseNat {T = T} {U = U} n<⋆ ⊢i ⊢z ⊢s p)
    = caseNat (SC.sub-resp-< ⊢σ n<⋆) (subₛ-resp-⊢ ⊢σ ⊢i) (subₛ-resp-⊢ ⊢σ ⊢z)
        (subₛ-resp-⊢ ⊢σ ⊢s) eq
    where
      eq : U [ SC.Lift σ ] ≡ T [ σ ] [ SC.Wk ]
      eq = trans (cong (λ U → U [ SC.Lift σ ]) p)
        ([>>]″ _ _ _ _ _ SC.Lift>>Wk)
  subₛ-resp-⊢ {σ = σ} ⊢σ (fix {n = n} {U = U} {T = T} {V = V} n<⋆ ⊢t p q)
    = fix (SC.sub-resp-< ⊢σ n<⋆) (subₛ-resp-⊢ ⊢σ ⊢t) eq₀ eq₁
    where
      eq₀ : U [ SC.Lift (SC.Lift σ) ] ≡ T [ SC.Lift σ ] [ SC.Skip ]
      eq₀ = trans (cong (λ U → U [ SC.Lift (SC.Lift σ) ]) p)
        ([>>]″ _ _ _ _ _ SC.LiftLift>>Skip)

      eq₁ : V [ σ ] ≡ T [ SC.Lift σ ] [ SC.Sing (n [ σ ]) ]
      eq₁ = trans (cong (λ V → V [ σ ]) q)
        ([>>]″ _ _ _ _ _ (sym (SC.Sing>>Lift n)))

  subₛ-Id : (t : Term Δ) → subₛ SC.Id t ≡ t
  subₛ-Id (var x) = refl
  subₛ-Id (Λ T , t) = cong₂ Λ_,_ ([Id] T) (subₛ-Id t)
  subₛ-Id (t · u) = cong₂ _·_ (subₛ-Id t) (subₛ-Id u)
  subₛ-Id (Λₛ n , t)
    rewrite [Id] n | subₛ-Id t
    = refl
  subₛ-Id (t ·ₛ m) = cong₂ _·ₛ_ (subₛ-Id t) ([Id] m)
  subₛ-Id (zero n) = cong zero ([Id] n)
  subₛ-Id (suc n m i)
    rewrite [Id] n | [Id] m | subₛ-Id i
    = refl
  subₛ-Id (cons i n is)
    rewrite subₛ-Id i | [Id] n | subₛ-Id is
    = refl
  subₛ-Id (head n is) = cong₂ head ([Id] n) (subₛ-Id is)
  subₛ-Id (tail n is m)
    rewrite [Id] n | subₛ-Id is | [Id] m
    = refl
  subₛ-Id (caseNat T n i z s)
    rewrite [Id] T | [Id] n | subₛ-Id i | subₛ-Id z | subₛ-Id s
    = refl
  subₛ-Id (fix T t n)
    rewrite [Id] T | subₛ-Id t | [Id] n
    = refl

  subₛ->> : ∀ (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″) t
    → subₛ (σ SC.>> τ) t ≡ subₛ σ (subₛ τ t)
  subₛ->> σ τ (var x) = refl
  subₛ->> σ τ (Λ T , t) = cong₂ Λ_,_ ([>>] σ τ T) (subₛ->> σ τ t)
  subₛ->> σ τ (t · u) = cong₂ _·_ (subₛ->> σ τ t) (subₛ->> σ τ u)
  subₛ->> σ τ (Λₛ n , t)
    rewrite [>>] σ τ n
    = cong (λ t → Λₛ SC.sub σ (SC.sub τ n) , t)
        (trans (cong (λ σ → subₛ σ t) (sym (SC.Lift>>Lift {n = n [ τ ]})))
          (subₛ->> (SC.Lift σ) (SC.Lift τ) t))
  subₛ->> σ τ (t ·ₛ m)
    = cong₂ _·ₛ_ (subₛ->> σ τ t) ([>>] σ τ m)
  subₛ->> σ τ (zero n) = cong zero ([>>] σ τ n)
  subₛ->> σ τ (suc n m i)
    rewrite [>>] σ τ n | [>>] σ τ m | subₛ->> σ τ i
    = refl
  subₛ->> σ τ (cons i n is)
    rewrite subₛ->> σ τ i | [>>] σ τ n | subₛ->> σ τ is
    = refl
  subₛ->> σ τ (head n is)
    rewrite [>>] σ τ n | subₛ->> σ τ is
    = refl
  subₛ->> σ τ (tail n is m)
    rewrite [>>] σ τ n | subₛ->> σ τ is | [>>] σ τ m
    = refl
  subₛ->> σ τ (caseNat T n i z s)
    rewrite [>>] σ τ T | [>>] σ τ n | subₛ->> σ τ i | subₛ->> σ τ z
      | subₛ->> σ τ s
    = refl
  subₛ->> σ τ (fix T t n)
    rewrite subₛ->> σ τ t | [>>] σ τ n
    = cong (λ T → fix T (subₛ σ (subₛ τ t)) (n [ τ ] [ σ ]))
        ([>>]′ _ _ _ _ (sym SC.Lift>>Lift))

subₛᵤ : SU.Sub Δ Ω → Term Ω → Term Δ
subₛᵤ σ = subₛ ⟨ σ ⟩

abstract
  subₛᵤ-resp-⊢ : ∀ {σ}
    → σ ∶ Δ ⇒ᵤ Ω
    → Ω , Γ ⊢ t ∶ T
    → Δ , Γ [ σ ]ᵤ ⊢ subₛᵤ σ t ∶ T [ σ ]ᵤ
  subₛᵤ-resp-⊢ ⊢σ ⊢t = subₛ-resp-⊢ (SU.⟨⟩-resp-⊢ ⊢σ) ⊢t

  subₛᵤ-Id : (t : Term Δ) → subₛᵤ SU.Id t ≡ t
  subₛᵤ-Id t = subₛ-Id t

  subₛᵤ->> : ∀ (σ : SU.Sub Δ Δ′) (τ : SU.Sub Δ′ Δ″) t
    → subₛᵤ (σ SU.>> τ) t ≡ subₛᵤ σ (subₛᵤ τ t)
  subₛᵤ->> σ τ t = subₛ->> ⟨ σ ⟩ ⟨ τ ⟩ t

data _⊇_ {Δ} : (Γ Ψ : Ctx Δ) → Set where
  [] : [] ⊇ []
  keep : (α : Γ ⊇ Ψ) (T : Type Δ) → Γ ∙ T ⊇ Ψ ∙ T
  weak : (α : Γ ⊇ Ψ) (T : Type Δ) → Γ ∙ T ⊇ Ψ

variable α β γ : Γ ⊇ Ψ

sub⊇ : (σ : SC.Sub Δ Ω) → Γ ⊇ Ψ → Γ [ σ ] ⊇ Ψ [ σ ]
sub⊇ σ [] = []
sub⊇ σ (keep α T) = keep (sub⊇ σ α) (T [ σ ])
sub⊇ σ (weak α T) = weak (sub⊇ σ α) (T [ σ ])

sub-syntax-⊇ = sub⊇

syntax sub-syntax-⊇ σ α = α [ σ ]α

renV : Γ ⊇ Ψ → Var → Var
renV [] x = x -- impossible if x is well-scoped
renV (keep α T) zero = zero
renV (keep α T) (suc x) = suc (renV α x)
renV (weak α T) x = suc (renV α x)

ren : {Γ Ψ : Ctx Δ} → Γ ⊇ Ψ → Term Δ → Term Δ
ren α (var x) = var (renV α x)
ren α (Λ T , t) = Λ T , ren (keep α T) t
ren α (t · u) = ren α t · ren α u
ren α (Λₛ n , t) = Λₛ n , ren (α [ SC.Wk ]α) t
ren α (t ·ₛ m) = ren α t ·ₛ m
ren α (zero n) = zero n
ren α (suc n m i) = suc n m (ren α i)
ren α (cons i n is) = cons (ren α i) n (ren α is)
ren α (head n is) = head n (ren α is)
ren α (tail n is m) = tail n (ren α is) m
ren α (caseNat T n i z s) = caseNat T n (ren α i) (ren α z) (ren α s)
ren α (fix T t n) = fix T (ren α t) n

abstract
  renV-resp-⊢ₓ
    : (α : Γ ⊇ Ψ)
    → Δ , Ψ ⊢ₓ x ∶ T
    → Δ , Γ ⊢ₓ renV α x ∶ T
  renV-resp-⊢ₓ (keep α T) zero = zero
  renV-resp-⊢ₓ (keep α T) (suc ⊢x) = suc (renV-resp-⊢ₓ α ⊢x)
  renV-resp-⊢ₓ (weak α T) ⊢x = suc (renV-resp-⊢ₓ α ⊢x)

  ren-resp-⊢
    : (α : Γ ⊇ Ψ)
    → Δ , Ψ ⊢ t ∶ T
    → Δ , Γ ⊢ ren α t ∶ T
  ren-resp-⊢ α (var ⊢x) = var (renV-resp-⊢ₓ α ⊢x)
  ren-resp-⊢ α (abs ⊢t)
    = abs (ren-resp-⊢ (keep α _) ⊢t)
  ren-resp-⊢ α (app ⊢t ⊢u) = app (ren-resp-⊢ α ⊢t) (ren-resp-⊢ α ⊢u)
  ren-resp-⊢ α (absₛ ⊢t refl)
    = absₛ (ren-resp-⊢ (α [ SC.Wk ]α) ⊢t) refl
  ren-resp-⊢ α (appₛ m<n ⊢t p) = appₛ m<n (ren-resp-⊢ α ⊢t) p
  ren-resp-⊢ α (zero n<⋆) = zero n<⋆
  ren-resp-⊢ α (suc n<⋆ m<n ⊢i) = suc n<⋆ m<n (ren-resp-⊢ α ⊢i)
  ren-resp-⊢ α (cons n<⋆ ⊢i ⊢is)
    = cons n<⋆ (ren-resp-⊢ α ⊢i) (ren-resp-⊢ α ⊢is)
  ren-resp-⊢ α (head n<⋆ ⊢is) = head n<⋆ (ren-resp-⊢ α ⊢is)
  ren-resp-⊢ α (tail n<⋆ m<n ⊢is) = tail n<⋆ m<n (ren-resp-⊢ α ⊢is)
  ren-resp-⊢ α (caseNat n<⋆ ⊢i ⊢z ⊢s p)
    = caseNat n<⋆ (ren-resp-⊢ α ⊢i) (ren-resp-⊢ α ⊢z) (ren-resp-⊢ α ⊢s) p
  ren-resp-⊢ α (fix n<⋆ ⊢t p q) = fix n<⋆ (ren-resp-⊢ α ⊢t) p q

Id⊇ : (Γ : Ctx Δ) → Γ ⊇ Γ
Id⊇ [] = []
Id⊇ (Γ ∙ T) = keep (Id⊇ Γ) T

Wk⊇ : ∀ (Γ : Ctx Δ) T → Γ ∙ T ⊇ Γ
Wk⊇ Γ T = weak (Id⊇ Γ) _

data Sub {Δ} (Γ : Ctx Δ) : (Ψ : Ctx Δ) → Set where
  [] : Sub Γ []
  Snoc : (ν : Sub Γ Ψ) (t : Term Δ) → Sub Γ (Ψ ∙ T)

variable ν φ : Sub Γ Ψ

data Sub⊢ {Δ} (Γ : Ctx Δ) : ∀ Ψ → Sub Γ Ψ → Set where
  [] : Sub⊢ Γ [] []
  Snoc : (⊢ν : Sub⊢ Γ Ψ ν) (⊢t : Δ , Γ ⊢ t ∶ T) → Sub⊢ Γ (Ψ ∙ T) (Snoc ν t)

syntax Sub⊢ Γ Ψ ν = ν ∶ Γ ⇛ Ψ

Weaken : Sub Γ Ψ → Sub (Γ ∙ T) Ψ
Weaken [] = []
Weaken {Γ = Γ} {T = T} (Snoc ν t) = Snoc (Weaken ν) (ren (Wk⊇ Γ T) t)

abstract
  Weaken⊢ : ν ∶ Γ ⇛ Ψ → Weaken ν ∶ Γ ∙ T ⇛ Ψ
  Weaken⊢ [] = []
  Weaken⊢ (Snoc ⊢ν ⊢t)
    = Snoc (Weaken⊢ ⊢ν) (ren-resp-⊢ (Wk⊇ _ _) ⊢t)

Lift : Sub Γ Ψ → ∀ T → Sub (Γ ∙ T) (Ψ ∙ T)
Lift σ T = Snoc (Weaken σ) (var zero)

abstract
  Lift⊢ : ν ∶ Γ ⇛ Ψ → Lift ν T ∶ Γ ∙ T ⇛ Ψ ∙ T
  Lift⊢ ⊢ν = Snoc (Weaken⊢ ⊢ν) (var zero)

Id : Sub Γ Γ
Id {Γ = []} = []
Id {Γ = Γ ∙ T} = Lift Id T

abstract
  Id⊢ : Id ∶ Γ ⇛ Γ
  Id⊢ {Γ = []} = []
  Id⊢ {Γ = Γ ∙ T} = Snoc (Weaken⊢ Id⊢) (var zero)

Wk : Sub (Γ ∙ T) Γ
Wk = Weaken Id

abstract
  Wk⊢ : Wk ∶ Γ ∙ T ⇛ Γ
  Wk⊢ = Weaken⊢ Id⊢

Fill : ∀ (Γ : Ctx Δ) T → Term Δ → Sub Γ (Γ ∙ T)
Fill Γ T t = Snoc Id t

abstract
  Fill⊢ : Δ , Γ ⊢ t ∶ T → Fill Γ T t ∶ Γ ⇛ Γ ∙ T
  Fill⊢ ⊢t = Snoc Id⊢ ⊢t

subν : (σ : SC.Sub Δ Ω) → Sub Γ Ψ → Sub (Γ [ σ ]) (Ψ [ σ ])
subν σ [] = []
subν σ (Snoc ν t) = Snoc (subν σ ν) (t [ σ ]ₛ)

abstract
  subν-resp-⊢ : ∀ {σ} → σ ∶ Δ ⇒ Ω → ν ∶ Γ ⇛ Ψ → subν σ ν ∶ Γ [ σ ] ⇛ Ψ [ σ ]
  subν-resp-⊢ ⊢σ [] = []
  subν-resp-⊢ ⊢σ (Snoc ⊢ν ⊢t) = Snoc (subν-resp-⊢ ⊢σ ⊢ν) (subₛ-resp-⊢ ⊢σ ⊢t)

sub-syntax-Subₛ = subν

syntax sub-syntax-Subₛ σ ν = ν [ σ ]ν

subV : Sub {Δ} Γ Ψ → Var → Term Δ
subV [] x = var x -- impossible if x is well-scoped
subV (Snoc ν t) zero = t
subV (Snoc ν t) (suc x) = subV ν x

sub : Sub {Δ} Γ Ψ → Term Δ → Term Δ
sub ν (var x) = subV ν x
sub ν (Λ T , t) = Λ T , sub (Lift ν T) t
sub ν (t · u) = sub ν t · sub ν u
sub ν (Λₛ n , t) = Λₛ n , sub (ν [ SC.Wk ]ν) t
sub ν (t ·ₛ m) = sub ν t ·ₛ m
sub ν (zero n) = zero n
sub ν (suc n m i) = suc n m (sub ν i)
sub ν (cons i n is) = cons (sub ν i) n (sub ν is)
sub ν (head n is) = head n (sub ν is)
sub ν (tail n is m) = tail n (sub ν is) m
sub ν (caseNat T n i z s) = caseNat T n (sub ν i) (sub ν z) (sub ν s)
sub ν (fix T t n) = fix T (sub ν t) n

sub-syntax-Term = sub

syntax sub-syntax-Term ν t = t [ ν ]t

abstract
  subV-resp-⊢
    : ν ∶ Γ ⇛ Ψ
    → Δ , Ψ ⊢ₓ x ∶ T
    → Δ , Γ ⊢ subV ν x ∶ T
  subV-resp-⊢ (Snoc ⊢ν ⊢t) zero = ⊢t
  subV-resp-⊢ (Snoc ⊢ν ⊢t) (suc ⊢x) = subV-resp-⊢ ⊢ν ⊢x

  sub-resp-⊢
    : ν ∶ Γ ⇛ Ψ
    → Δ , Ψ ⊢ t ∶ T
    → Δ , Γ ⊢ sub ν t ∶ T
  sub-resp-⊢ ⊢ν (var ⊢x)
    = subV-resp-⊢ ⊢ν ⊢x
  sub-resp-⊢ ⊢ν (abs ⊢t)
    = abs (sub-resp-⊢ (Lift⊢ ⊢ν) ⊢t)
  sub-resp-⊢ ⊢ν (app ⊢t ⊢u)
    = app (sub-resp-⊢ ⊢ν ⊢t) (sub-resp-⊢ ⊢ν ⊢u)
  sub-resp-⊢ ⊢ν (absₛ ⊢t refl)
    = absₛ (sub-resp-⊢ (subν-resp-⊢ SC.Wk⊢ ⊢ν) ⊢t) refl
  sub-resp-⊢ ⊢ν (appₛ m<n ⊢t p)
    = appₛ m<n (sub-resp-⊢ ⊢ν ⊢t) p
  sub-resp-⊢ ⊢ν (zero n<⋆)
    = zero n<⋆
  sub-resp-⊢ ⊢ν (suc n<⋆ m<n ⊢i)
    = suc n<⋆ m<n (sub-resp-⊢ ⊢ν ⊢i)
  sub-resp-⊢ ⊢ν (cons n<⋆ ⊢i ⊢is)
    = cons n<⋆ (sub-resp-⊢ ⊢ν ⊢i) (sub-resp-⊢ ⊢ν ⊢is)
  sub-resp-⊢ ⊢ν (head n<⋆ ⊢is)
    = head n<⋆ (sub-resp-⊢ ⊢ν ⊢is)
  sub-resp-⊢ ⊢ν (tail n<⋆ m<n ⊢is)
    = tail n<⋆ m<n (sub-resp-⊢ ⊢ν ⊢is)
  sub-resp-⊢ ⊢ν (caseNat n<⋆ ⊢i ⊢z ⊢s p)
    = caseNat n<⋆ (sub-resp-⊢ ⊢ν ⊢i) (sub-resp-⊢ ⊢ν ⊢z) (sub-resp-⊢ ⊢ν ⊢s) p
  sub-resp-⊢ ⊢ν (fix n<⋆ ⊢t p q)
    = fix n<⋆ (sub-resp-⊢ ⊢ν ⊢t) p q

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Structure.Operator.Group.Proofs where

open import Functional hiding (id)
open import Function.Iteration.Order
import      Lvl
open import Lang.Instance
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Function.Domain
open import Structure.Operator.Group
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator.Proofs
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

{-
module _ {ℓ₁ ℓ₂} {X : Type{ℓ₁}} ⦃ _ : Equiv(X) ⦄ {_▫X_ : X → X → X} ⦃ structureₗ : Group(_▫X_) ⦄ {Y : Type{ℓ₂}} ⦃ _ : Equiv(Y) ⦄ {_▫Y_ : Y → Y → Y} ⦃ structureᵣ : Group(_▫Y_) ⦄ (f : X → Y) where
  monomorphic-cyclic : ⦃ (_▫X_) ↣ (_▫Y_) ⦄ → Cyclic(_▫X_) → Cyclic(_▫Y_)
  monomorphic-cyclic ⦃ [∃]-intro θ ⦃ θ-proof ⦄ ⦄ ([∃]-intro index ⦃ intro a ⦄) = {!!}
-}

{-
module _ {T : Type{ℓ₂}} {_▫_ : T → T → T} ⦃ group : Group(_▫_) ⦄ where
  open Group  {T} ⦃ [≡]-equiv ⦄ {_▫_} (group)
  open Monoid {T} ⦃ [≡]-equiv ⦄ {_▫_} (monoid)

  commutationₗ : ∀{x y} → (x ▫ y ≡ y ▫ x) ← ((x ▫ y) ▫ inv (x) ≡ y)
  commutationₗ {x}{y} (comm) =
    symmetry(
      (congruence₁(_▫ x)
        (symmetry comm)
      )
      🝖 (associativity)
      🝖 (congruence₁((x ▫ y) ▫_)) (inverseₗ)
      🝖 (identityᵣ)
    )
  -- (x▫y)▫inv(x) = y //comm
  -- y = (x▫y)▫inv(x) //[≡]-symmetry
  -- y▫x
  -- = ((x▫y)▫inv(x))▫x //congruence₁(expr ↦ expr ▫ x) (..)
  -- = (x▫y)▫(inv(x)▫x) //Group.associativity
  -- = (x▫y)▫id //congruence₁(_) Group.inverseₗ
  -- = x▫y //Group.identityᵣ
  -- x▫y = y▫x //[≡]-symmetry

  commutationᵣ : ∀{x y} → (x ▫ y ≡ y ▫ x) → ((x ▫ y) ▫ inv(x) ≡ y)
  commutationᵣ {x}{y} (comm) =
    (congruence₁(_▫ inv(x)) comm)
    🝖 (associativity)
    🝖 (congruence₁(y ▫_) (inverseᵣ))
    🝖 (identityᵣ)
  -- x▫y = y▫x //comm
  -- (x▫y)▫inv(x)
  -- = (y▫x)▫inv(x) //congruence₁(expr ↦ expr ▫ inv(x)) (..)
  -- = y▫(x▫inv(x)) //Group.associativity
  -- = y▫id //congruence₁(expr ↦ y ▫ expr) Group.inverseᵣ
  -- = y //Group.identityᵣ

module _ {T : Type} {_▫_ : T → T → T} ⦃ commGroup : CommutativeGroup(_▫_) ⦄ where
  open CommutativeGroup {T} ⦃ [≡]-equiv ⦄ {_▫_} (commGroup)
  open Group            {T} ⦃ [≡]-equiv ⦄ {_▫_} (group)
  open Monoid           {T} ⦃ [≡]-equiv ⦄ {_▫_} (monoid)

  commutation : ∀{x y} → ((x ▫ y) ▫ inv(x) ≡ y)
  commutation = commutationᵣ(commutativity)

module _ {T : Type} {_▫_ : T → T → T} ⦃ associativity : Associativity(_▫_) ⦄ where

-}

ext: agda

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:
open import Agda.Builtin.Nat

data Vec (a : Set) : {n : Nat} → Set where
  Nil : Vec a {0}
  Cons : {n : Nat} → a → Vec a {n} → Vec a {suc n}
{-# COMPILE AGDA2HS Vec #-}

mapV : {a b : Set} {n : Nat} (f : a → b) → Vec a {n} → Vec b {n}
mapV f Nil = Nil
mapV f (Cons x xs) = Cons (f x) (mapV f xs)
{-# COMPILE AGDA2HS mapV #-}

tailV : {a : Set} {n : Nat} → Vec a {suc n} → Vec a {n}
tailV (Cons x xs) = xs
{-# COMPILE AGDA2HS tailV #-}

-- Using erasure instead of implicit arguments
data Vec' (a : Set) : (@0 n : Nat) → Set where
  Nil' : Vec' a 0
  Cons' : {@0 n : Nat} → a → Vec' a n → Vec' a (suc n)
{-# COMPILE AGDA2HS Vec' #-}

mapV' : {a b : Set} {@0 n : Nat} (f : a → b) → Vec' a n → Vec' b n
mapV' f Nil' = Nil'
mapV' f (Cons' x xs) = Cons' (f x) (mapV' f xs)
{-# COMPILE AGDA2HS mapV' #-}

tailV' : {a : Set} {@0 n : Nat} → Vec' a (suc n) → Vec' a n
tailV' (Cons' x xs) = xs
{-# COMPILE AGDA2HS tailV' #-}


text:
{-

The goal of this file is to prove the iso π₄S³≅ℤ/β
where β is a natural number (aka "the Brunerie number",
defined below).

-}
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Group.Pi4S3.BrunerieNumber where

open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.Group.Pi3S2
open import Cubical.Homotopy.Group.PinSn
open import Cubical.Homotopy.BlakersMassey
open import Cubical.Homotopy.Whitehead
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Group.LES
open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2
open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Int
  renaming (ℤ to Z ; _·_ to _·Z_ ; _+_ to _+Z_)

open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.Pushout
open import Cubical.HITs.PropositionalTruncation
  renaming (rec to pRec ; elim to pElim ; map to pMap)
open import Cubical.HITs.SetTruncation
  renaming (rec to sRec ; rec2 to sRec2
          ; elim to sElim ; elim2 to sElim2 ; elim3 to sElim3
          ; map to sMap)
open import Cubical.HITs.Truncation renaming
  (rec to trRec ; elim to trElim ; elim2 to trElim2 ; map to trMap)

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Exact
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Instances.IntMod
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Unit
open import Cubical.Algebra.Group.GroupPath

open Iso
open Exact4

-- The Brunerie number (see Corollary 3.4.5 in Brunerie's PhD thesis)
Brunerie : ℕ
Brunerie =
  abs (HopfInvariant-π' 0  [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π')

-- First we need to define the following maps.
W : S₊ 3 → (S₊∙ 2 ⋁ S₊∙ 2)
W = joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1} ∘ Iso.inv (IsoSphereJoin 1 1)

fold∘W : S₊ 3 → S₊ 2
fold∘W = fold⋁ ∘ W

{-
We will now instantiate Blakers Massey to get a square:

         fold∘W
 S³ --------------> S²
 |\              ↗ |
 |  \         ↗    |
 |    \    ↗       |
 |      X           |  inr
 |    /             |
 |   /              |
 |  /               |
 v /                v
 1 -----------> coFib fold∘W
         inl

where X is the pullback of inl and inr and the map S³ → X is
surjective on π₃. This will give us a sequence
π₃ S³ --ᶠ→ π₃ S² → π₃ (coFib fold∘W) → π₂ X ≅ 0, where f is
the function induced by fold∘W. From this, we can deduce that
π₃ (coFib fold∘W) ≅ ℤ/ f(1) where f(1) is interpreted as an
integer via the isos π₃ S³ ≅ π₃ S² ≅ ℤ

(Recall that π₃(coFib fold∘W) ≅ π₄S³)

For clarity:
X, above will have two names (via a trivial iso) below:

TotalPushoutPath× (the version the falls out of BM)
P = fiber inr (Same name as in Brunerie's prop 4.3.4.)
-}

-- Before instantiating, we need to show that
-- any map S³ → S² is 0-connected
isConnectedS3→S2 : (f : S₊ 3 → S₊ 2) → isConnectedFun 2 f
isConnectedS3→S2 f p =
  trRec (isProp→isOfHLevelSuc 1 isPropIsContr)
    (J (λ p _ → isConnected 2 (fiber f p))
      (∣ north , refl ∣
     , (trElim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _)
         (uncurry
           (sphereElim 2
             (λ _ → isOfHLevelΠ 3
               λ _ → isOfHLevelPath 3
                 (isOfHLevelSuc 2 (isOfHLevelTrunc 2)) _ _)
           λ p → trRec (isOfHLevelTrunc 2 _ _)
             (λ r → cong ∣_∣ₕ (ΣPathP (refl , r)))
            (fun (PathIdTruncIso 1)
              (isContr→isProp
                (isConnectedPath 2 (sphereConnected 2)
                  (f north) (f north)) ∣ refl ∣ ∣ p ∣)))))))
    (fun (PathIdTruncIso 2)
      (isContr→isProp (sphereConnected 2) ∣ f north ∣ ∣ p ∣))

-- We get our square
module BM-inst =
  BlakersMassey□
   (λ _ → tt) fold∘W 3 1
   (λ _ → subst (isConnected 4)
            (isoToPath (invIso fiberUnitIso))
            (sphereConnected 3))
   (isConnectedS3→S2 fold∘W)

open BM-inst

-- The central types
coFib-fold∘W : Type
coFib-fold∘W = Pushout (λ _ → tt) fold∘W

coFib-fold∘W∙ : Pointed₀
coFib-fold∘W∙ = coFib-fold∘W , inl tt

TotalPushoutPath×∙ : Pointed ℓ-zero
fst TotalPushoutPath×∙ = Σ (Unit × S₊ 2) PushoutPath×
snd TotalPushoutPath×∙ = (tt , north) , push north

S³→TotalPushoutPath× : S₊ 3 → Σ (Unit × S₊ 2) PushoutPath×
S³→TotalPushoutPath× = toPullback

private
  inr' : S₊ 2 → coFib-fold∘W
  inr' = inr

  inr∙ : S₊∙ 2 →∙ coFib-fold∘W∙
  fst inr∙ = inr'
  snd inr∙ = sym (push north)

  fiberinr'Iso' : Iso (fiber inr' (inl tt))
                      (Σ (Unit × S₊ 2) PushoutPath×)
  fiberinr'Iso' =
    compIso (Σ-cong-iso-snd (λ x → symIso))
            (Σ-cong-iso-fst (invIso lUnit×Iso))

  fiberinr'Iso : Iso (fiber inr' (inl tt))
                     (Σ (Unit × S₊ 2) PushoutPath×)
  fun fiberinr'Iso (x , p) = (tt , x) , (sym p)
  inv fiberinr'Iso ((tt , x) , p) = x , (sym p)
  rightInv fiberinr'Iso _ = refl
  leftInv fiberinr'Iso _ = refl

  P : Pointed₀
  P = (fiber inr' (inl tt) , north , (sym (push north)))

π'P→π'TotalPath× : (n : ℕ)
  → GroupEquiv (π'Gr n TotalPushoutPath×∙) (π'Gr n P)
fst (fst (π'P→π'TotalPath× n)) =
  π'eqFun n ((invEquiv (isoToEquiv fiberinr'Iso)) , refl)
snd (fst (π'P→π'TotalPath× n)) = π'eqFunIsEquiv n _
snd (π'P→π'TotalPath× n) = π'eqFunIsHom n _

-- Time to invoke the long exact sequence of homotopy groups on
-- inr : S² → coFib-fold∘W
module LESinst = πLES {A = S₊∙ 2} {B = coFib-fold∘W∙} inr∙

-- We instantiate the sequence
-- π₃ P → π₃ S² → π₃ coFib-fold∘W∙ → π₂ P
P→S²→Pushout :
  Exact4 (πGr 2 P) (πGr 2 (S₊∙ 2)) (πGr 2 coFib-fold∘W∙) (πGr 1 P)
        (LESinst.fib→A 2)
        (LESinst.A→B 2)
        (LESinst.B→fib 1)
Exact4.ImG→H⊂KerH→L P→S²→Pushout = LESinst.Im-fib→A⊂Ker-A→B 2
Exact4.KerH→L⊂ImG→H P→S²→Pushout = LESinst.Ker-A→B⊂Im-fib→A 2
Exact4.ImH→L⊂KerL→R P→S²→Pushout = LESinst.Im-A→B⊂Ker-B→fib 1
Exact4.KerL→R⊂ImH→L P→S²→Pushout = LESinst.Ker-B→fib⊂Im-A→B 1

-- The goal now is to rewrite it as
-- π₃ S³ → π₃ S² → π₃ coFib-fold∘W∙ → Unit using the
-- "functions from spheres"-definition of πₙ.
-- Here, the first map is the one induced by fold∘W. We do this by:
-- (1) showing that π₂ P is trivial
-- (2) extending the sequence by appending surjections
-- π₃ S³ → π₃ TotalPushoutPath×∙ → π₃ P on the left.
-- (3) proving that this new composition is indeed the appropriate map

-- Step 1: π₂ P is trivial
π₂P≅0 : GroupEquiv (πGr 1 P) UnitGroup₀
π₂P≅0 = compGroupEquiv (πIso (isoToEquiv fiberinr'Iso , refl) 1)
         (GroupIso→GroupEquiv
           (contrGroupIsoUnit
             (isOfHLevelRetractFromIso 0 (invIso iso₂) isContrπ₂S³)))
  where
  iso₁ : Iso (hLevelTrunc 4 (S₊ 3))
             (hLevelTrunc 4 (Σ (Unit × S₊ 2) PushoutPath×))
  iso₁ = connectedTruncIso 4 S³→TotalPushoutPath× isConnected-toPullback

  iso₂ : Iso (π 2 (hLevelTrunc∙ 4 (S₊∙ 3)))
              (π 2 TotalPushoutPath×∙)
  iso₂ =
    (compIso (setTruncIso
      (equivToIso (_ ,
        (isEquivΩ^→ 2 (fun iso₁ , refl) (isoToIsEquiv iso₁)))))
     (invIso (πTruncIso 2)))

  isContrπ₂S³ : isContr (π 2 (hLevelTrunc∙ 4 (S₊∙ 3)))
  isContrπ₂S³ =
    subst (λ x → isContr (π 2 x))
      (λ i → ((sym (isContr→≡Unit (sphereConnected 3))) i)
            , transp (λ j → isContr→≡Unit
              (sphereConnected 3) (~ i ∧ j)) i ∣ north ∣)
      (∣ refl ∣₂ , sElim (λ _ → isSetPathImplicit)
                  λ p → cong ∣_∣₂
                          (isProp→isSet
                           (isOfHLevelPath 1 isPropUnit _ _) _ _ _ p))

-- Step 2. We transform our original sequence to one for the
-- the "maps from spheres" definition of πₙ and where π₂ P is
-- replaced by the trivial group:
-- π₃ P → π₃ S² → π₃ coFib-fold∘W∙ → 0
P→S²→Pushout→P' :
  Exact4 (π'Gr 2 P) (π'Gr 2 (S₊∙ 2)) (π'Gr 2 coFib-fold∘W∙) UnitGroup₀
         (π'∘∙Hom 2 (fst , refl))
         (π'∘∙Hom 2 inr∙)
         (→UnitHom _)
P→S²→Pushout→P' =
  transportExact4
  (sym (GroupPath _ _ .fst ((GroupIso→GroupEquiv (π'Gr≅πGr 2 P)))))
  (sym (GroupPath _ _ .fst ((GroupIso→GroupEquiv (π'Gr≅πGr 2 (S₊∙ 2))))))
  (sym (GroupPath _ _ .fst ((GroupIso→GroupEquiv (π'Gr≅πGr 2 coFib-fold∘W∙)))))
  (sym (GroupPath _ _ .fst π₂P≅0))
  _ _ _ _ _
  P→S²→Pushout
  (ΣPathPProp (λ _ → isPropIsGroupHom _ _)
    λ i → fst (π∘∙fib→A-PathP 2 inr∙ i))
  (ΣPathPProp (λ _ → isPropIsGroupHom _ _)
    λ i → fst (π∘∙A→B-PathP 2 inr∙ i))

-- The two surjections in question
π₃S³→π₃P : GroupHom (π'Gr 2 (S₊∙ 3)) (π'Gr 2 TotalPushoutPath×∙)
π₃S³→π₃P = π'∘∙Hom 2 (S³→TotalPushoutPath× , refl)

TotalPushoutPath×∙→P : TotalPushoutPath×∙ →∙ P -- Surjective, and in particular on π₃
fst TotalPushoutPath×∙→P x = (snd (fst x)) , (sym (snd x))
snd TotalPushoutPath×∙→P = refl

-- This surjectivity is where Blakers-Massey is used
-- In particular, it uses isConnected-toPullback
isSurjective-π₃S³→π₃TotalPushoutPath× : isSurjective π₃S³→π₃P
isSurjective-π₃S³→π₃TotalPushoutPath× =
  transport (λ i → isSurjective (transportLem i))
              isSurjective-π₃S³→π₃TotalPushoutPath×'
  where
  π₃S³→π₃TotalPushoutPath× : GroupHom (πGr 2 (S₊∙ 3)) (πGr 2 TotalPushoutPath×∙)
  π₃S³→π₃TotalPushoutPath× = πHom 2 (S³→TotalPushoutPath× , refl)

  isSurjective-π₃S³→π₃TotalPushoutPath×' : isSurjective π₃S³→π₃TotalPushoutPath×
  isSurjective-π₃S³→π₃TotalPushoutPath×' =
    sElim (λ _ → isProp→isSet squash₁)
      λ p → trRec squash₁
        (λ s → ∣ ∣ fst s ∣₂ , (cong ∣_∣₂ (snd s)) ∣₁)
        (((isConnectedΩ^→ 3 3 (S³→TotalPushoutPath× , refl)
          isConnected-toPullback) p) .fst)

  transportLem : PathP (λ i → GroupHomπ≅π'PathP (S₊∙ 3) TotalPushoutPath×∙ 2 i)
                       π₃S³→π₃TotalPushoutPath× π₃S³→π₃P
  transportLem =
    toPathP (Σ≡Prop (λ _ → isPropIsGroupHom _ _)
       (π'∘∙Hom'≡π'∘∙fun {A = S₊∙ 3} {B = TotalPushoutPath×∙}
         2 (S³→TotalPushoutPath× , refl)))

-- We get a sequence on the right form π₃S³ → π₃S² → π₃ Pushout → Unit
S³→S²→Pushout→Unit'' :
  Exact4 (π'Gr 2 (S₊∙ 3)) (π'Gr 2 (S₊∙ 2)) (π'Gr 2 coFib-fold∘W∙) UnitGroup₀
        (compGroupHom π₃S³→π₃P
          (compGroupHom
            (π'∘∙Hom 2 TotalPushoutPath×∙→P) (π'∘∙Hom 2 (fst , refl))))
        (π'∘∙Hom 2 inr∙)
        (→UnitHom (π'Gr 2 coFib-fold∘W∙))
S³→S²→Pushout→Unit'' =
  extendExact4Surjective _ _ _ _ _ _ _ _ _
    isSurjective-π₃S³→π₃TotalPushoutPath×
    (extendExact4Surjective _ _ _ _ _ _ _ _ _
      ((sElim (λ _ → isProp→isSet squash₁)
      (λ f → ∣ ∣ (λ x → (tt , fst f x .fst) , sym (fst f x .snd))
      , ΣPathP ((ΣPathP (refl , cong fst (snd f)))
                       , λ j i → snd f j  .snd (~ i)) ∣₂
              , cong ∣_∣₂ (ΣPathP (refl , sym (rUnit _))) ∣₁)))
      P→S²→Pushout→P')

-- Step 3: We need to show that the map π₃S³ → π₃S² in the above sequence
-- indeed comes from fold∘W
tripleComp≡ :
    (compGroupHom π₃S³→π₃P
     (compGroupHom
      (π'∘∙Hom 2 TotalPushoutPath×∙→P) (π'∘∙Hom 2 (fst , refl))))
  ≡ π'∘∙Hom 2 (fold∘W , refl)
tripleComp≡ =
  Σ≡Prop (λ _ → isPropIsGroupHom _ _)
    (funExt (sElim (λ _ → isSetPathImplicit)
     λ f → cong ∣_∣₂ (ΣPathP (refl , (cong (_∙ refl)
     (λ j → cong fst (rUnit (cong (fst TotalPushoutPath×∙→P)
               (rUnit (cong S³→TotalPushoutPath× (snd f)) (~ j))) (~ j))))))))

-- We finally get the correct sequence
S³→S²→Pushout→Unit :
  Exact4 (π'Gr 2 (S₊∙ 3)) (π'Gr 2 (S₊∙ 2)) (π'Gr 2 coFib-fold∘W∙) UnitGroup₀
        (π'∘∙Hom 2 (fold∘W , refl))
        (π'∘∙Hom 2 inr∙)
        (→UnitHom (π'Gr 2 coFib-fold∘W∙))
S³→S²→Pushout→Unit =
  subst
   (λ F → Exact4 (π'Gr 2 (S₊∙ 3)) (π'Gr 2 (S₊∙ 2)) (π'Gr 2 coFib-fold∘W∙) UnitGroup₀
            F (π'∘∙Hom 2 inr∙)
            (→UnitHom (π'Gr 2 coFib-fold∘W∙)))
            tripleComp≡
   S³→S²→Pushout→Unit''

-- We need to throw around some pushouts
module _ where
  Pushout-coFibW-fold⋁≃coFib-fold∘W :
    Pushout {B = (Pushout W (λ _ → tt))} inl fold⋁ ≃ fst coFib-fold∘W∙
  Pushout-coFibW-fold⋁≃coFib-fold∘W = compEquiv
          (compEquiv pushoutSwitchEquiv
            (isoToEquiv (PushoutDistr.PushoutDistrIso fold⋁ W λ _ → tt)))
          pushoutSwitchEquiv

  coFibW≅coFibW' : Pushout W (λ _ → tt) ≃ cofibW S¹ S¹ base base
  coFibW≅coFibW' = pushoutEquiv W (λ _ → tt) joinTo⋁ (λ _ → tt)
           (isoToEquiv (invIso (IsoSphereJoin 1 1)))
           (idEquiv _)
           (idEquiv _)
           refl
           refl

  Pushout-coFibW-fold⋁≃Pushout⋁↪fold⋁ :
      Pushout {B = (Pushout W (λ _ → tt))} inl fold⋁
    ≃ fst (Pushout⋁↪fold⋁∙ (S₊∙ 2))
  Pushout-coFibW-fold⋁≃Pushout⋁↪fold⋁ = pushoutEquiv inl _ ⋁↪ fold⋁
          (idEquiv _)
          (compEquiv coFibW≅coFibW'
            (isoToEquiv (invIso (Iso-Susp×Susp-cofibJoinTo⋁ S¹ S¹ base base))))
          (idEquiv _)
          (Susp×Susp→cofibW≡ S¹ S¹ base base)
          refl

  Pushout-coFibW-fold⋁≃Pushout⋁↪fold⋁∙ :
       (Pushout {B = (Pushout W (λ _ → tt))} inl fold⋁ , inr north)
    ≃∙ (Pushout⋁↪fold⋁∙ (S₊∙ 2))
  fst Pushout-coFibW-fold⋁≃Pushout⋁↪fold⋁∙ =
    Pushout-coFibW-fold⋁≃Pushout⋁↪fold⋁
  snd Pushout-coFibW-fold⋁≃Pushout⋁↪fold⋁∙ =
    sym (push (inl north))

π₄S³≅π₃coFib-fold∘W∙ : GroupEquiv (π'Gr 3 (S₊∙ 3)) (π'Gr 2 coFib-fold∘W∙)
π₄S³≅π₃coFib-fold∘W∙ =
  compGroupEquiv
    (GroupIso→GroupEquiv
      (compGroupIso
        (π'Gr≅πGr 3 (S₊∙ 3))
        (compGroupIso
          π₄S³≅π₃PushS²
          (invGroupIso (π'Gr≅πGr 2 (Pushout⋁↪fold⋁∙ (S₊∙ 2)))))))
    (compGroupEquiv
      (invGroupEquiv (π'Iso 2 Pushout-coFibW-fold⋁≃Pushout⋁↪fold⋁∙))
      (π'Iso 2 (Pushout-coFibW-fold⋁≃coFib-fold∘W , sym (push north))))

-- We get the iso
-- For type checking reasons, let's first prove it for the abstract
-- definition of ℤ/_

-- To get everything on the same form as in Brunerie's thesis, we
-- first need the following:
fold∘W≡Whitehead :
        fst (π'∘∙Hom 2 (fold∘W , refl)) ∣ idfun∙ (S₊∙ 3) ∣₂
      ≡ ∣ [ idfun∙ (S₊∙ 2) ∣ idfun∙ (S₊∙ 2) ]₂ ∣₂
fold∘W≡Whitehead =
  pRec (squash₂ _ _)
    (cong ∣_∣₂)
    (indΠ₃S₂ _ _
      (funExt (λ x → funExt⁻ (sym (cong fst (id∨→∙id {A = S₊∙ 2}))) (W x))))
  where
  indΠ₃S₂ : ∀ {ℓ} {A : Pointed ℓ}
    → (f g : A →∙ S₊∙ 2)
      → fst f ≡ fst g → ∥ f ≡ g ∥₁
  indΠ₃S₂ {A = A} f g p =
    trRec squash₁
     (λ r → ∣ ΣPathP (p , r) ∣₁)
      (isConnectedPathP 1 {A = (λ i → p i (snd A) ≡ north)}
        (isConnectedPathSⁿ 1 (fst g (pt A)) north) (snd f) (snd g) .fst )

BrunerieIsoAbstract : GroupEquiv (π'Gr 3 (S₊∙ 3)) (abstractℤGroup/ Brunerie)
BrunerieIsoAbstract =
  compGroupEquiv π₄S³≅π₃coFib-fold∘W∙
    (invGroupEquiv
      (GroupEquiv-abstractℤ/abs-gen
        (π'Gr 2 (S₊∙ 3)) (π'Gr 2 (S₊∙ 2)) (π'Gr 2 coFib-fold∘W∙)
          (GroupIso→GroupEquiv (invGroupIso (πₙ'Sⁿ≅ℤ 2)))
          (invGroupEquiv hopfInvariantEquiv)
          (π'∘∙Hom 2 (fold∘W , refl))
          _
          S³→S²→Pushout→Unit Brunerie main))
  where
  mainPath :
    fst (π'∘∙Hom 2 (fold∘W , refl))
         (Iso.inv (fst (πₙ'Sⁿ≅ℤ 2)) 1)
     ≡ [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π'
  mainPath =
      cong (fst (π'∘∙Hom 2 (fold∘W , refl)))
           (cong (Iso.inv (fst (πₙ'Sⁿ≅ℤ 2))) (sym (πₙ'Sⁿ≅ℤ-idfun∙ 2))
           ∙ (Iso.leftInv (fst (πₙ'Sⁿ≅ℤ 2)) ∣ idfun∙ (S₊∙ 3) ∣₂))
    ∙ fold∘W≡Whitehead
    ∙ cong ∣_∣₂ (sym ([]≡[]₂ (idfun∙ (S₊∙ 2)) (idfun∙ (S₊∙ 2))))

  main : _ ≡ Brunerie
  main i = abs (HopfInvariant-π' 0 (mainPath i))

-- And, finally, we get the actual iso
-- (as in Corollary 3.4.5 in Brunerie's thesis)
BrunerieIso : GroupEquiv (π'Gr 3 (S₊∙ 3)) (ℤGroup/ Brunerie)
BrunerieIso =
  compGroupEquiv BrunerieIsoAbstract (abstractℤ/≅ℤ Brunerie)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module UniDB.Morph.WeakenPrime where

open import UniDB.Spec
open import UniDB.Morph.ShiftsPrime
open import Function

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

data Weaken` : MOR where
  baseW : {γ : Dom} → Weaken` γ γ
  stepW : {γ₁ γ₂ : Dom} → Weaken` γ₁ γ₂  → Weaken` γ₁ (suc γ₂)

lkWeakenIx` : {γ₁ γ₂ : Dom} → Weaken` γ₁ γ₂ → Ix γ₁ → Ix γ₂
lkWeakenIx` baseW     i = i
lkWeakenIx` (stepW ξ) i = suc (lkWeakenIx` ξ i)

instance
  iLkWeaken` : {T : STX} {{vrT : Vr T}} → Lk T Weaken`
  lk {{iLkWeaken`}} ξ i = vr (lkWeakenIx` ξ i)

  iWkmWeaken` : Wkm Weaken`
  Wkm.wkm iWkmWeaken` zero    = baseW
  Wkm.wkm iWkmWeaken` (suc δ) = stepW (wkm {Weaken`} δ)

  iIdmWeaken` : Idm Weaken`
  idm {{iIdmWeaken`}} γ = baseW

  iWkWeaken` : {γ₁ : Dom} → Wk (Weaken` γ₁)
  wk₁ {{iWkWeaken`}} ξ = stepW ξ
  wk {{iWkWeaken`}} zero x = x
  wk {{iWkWeaken`}} (suc δ) x = wk₁ (wk δ x)
  wk-zero {{iWkWeaken`}} x = refl
  wk-suc {{iWkWeaken`}} δ x = refl

lkWeakenIx`-wkm : {γ : Dom} (δ : Dom) (i : Ix γ) →
  lkWeakenIx` (wkm {Weaken`} δ) i ≡ wk δ i
lkWeakenIx`-wkm zero    i = refl
lkWeakenIx`-wkm (suc δ) i = cong suc (lkWeakenIx`-wkm δ i)

instance
  iLkWkmWeaken` : {T : STX} {{vrT : Vr T}} → LkWkm T Weaken`
  lk-wkm {{iLkWkmWeaken` {T}}} δ i = cong (vr {T}) (lkWeakenIx`-wkm δ i)

  iCompWeaken` : Comp Weaken`
  _⊙_ {{iCompWeaken`}} ξ baseW      = ξ
  _⊙_ {{iCompWeaken`}} ξ (stepW ξ₂) = stepW (ξ ⊙ ξ₂)

wk-comp` : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Weaken` γ₁ γ₂) (ξ₂ : Weaken` γ₂ γ₃)
  (δ : Dom) → wk δ (ξ₁ ⊙ ξ₂) ≡ ξ₁ ⊙ wk δ ξ₂
wk-comp` ξ₁ ξ₂ zero    = refl
wk-comp` ξ₁ ξ₂ (suc δ) = cong stepW (wk-comp` ξ₁ ξ₂ δ)

lkIx-wk-weaken` : {γ₁ γ₂ : Dom} (δ : Dom) (ξ : Weaken` γ₁ γ₂) (i : Ix γ₁) →
  lk {Ix} {Weaken`} (wk δ ξ) i ≡ wk δ (lk {Ix} {Weaken`} ξ i)
lkIx-wk-weaken` zero    ξ i = refl
lkIx-wk-weaken` (suc δ) ξ i = cong suc (lkIx-wk-weaken` δ ξ i)

module _ (T : STX) {{vrT : Vr T}}  {{wkT : Wk T}} {{wkVrT : WkVr T}} where

  lk-wk₁-weaken` :
    {γ₁ γ₂ : Dom} (ξ : Weaken` γ₁ γ₂) (i : Ix γ₁) →
    lk {T} {Weaken`} (wk₁ ξ) i ≡ wk₁ (lk {T} {Weaken`} ξ i)
  lk-wk₁-weaken` ξ i = sym (wk₁-vr {T} (lk {Ix} {Weaken`} ξ i) )

  lk-wk-weaken` :
    {γ₁ γ₂ : Dom} (δ : Dom) (ξ : Weaken` γ₁ γ₂) (i : Ix γ₁) →
    lk {T} {Weaken`} (wk δ ξ) i ≡ wk δ (lk {T} {Weaken`} ξ i)
  lk-wk-weaken` δ ξ i = trans
    (cong (vr {T}) (lkIx-wk-weaken` δ ξ i))
    (sym (wk-vr {T} δ (lk {Ix} {Weaken`} ξ i)))

lkWeakenIx`-comp :
  {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Weaken` γ₁ γ₂) (ξ₂ : Weaken` γ₂ γ₃)
  (i : Ix γ₁) →
  lkWeakenIx` ((iCompWeaken` Comp.⊙ ξ₁) ξ₂) i ≡
  lkWeakenIx` ξ₂ (lkWeakenIx` ξ₁ i)
lkWeakenIx`-comp ξ₁ baseW      i = refl
lkWeakenIx`-comp ξ₁ (stepW ξ₂) i = cong suc (lkWeakenIx`-comp ξ₁ ξ₂ i)

instance
  iLkRenWeaken` : {T : STX} {{vrT : Vr T}} → LkRen T Weaken`
  lk-ren {{iLkRenWeaken`}} ξ i = refl

  iLkRenCompWeaken` : {T : STX} {{vrT : Vr T}} → LkRenComp T Weaken`
  lk-ren-comp {{iLkRenCompWeaken` {T}}} ξ₁ ξ₂ i =
    cong (vr {T}) (lkWeakenIx`-comp ξ₁ ξ₂ i)

  iCompIdmWeaken` : CompIdm Weaken`
  ⊙-idm {{iCompIdmWeaken`}} ξ = refl
  idm-⊙ {{iCompIdmWeaken`}} baseW = refl
  idm-⊙ {{iCompIdmWeaken`}} (stepW ξ) = cong stepW (idm-⊙ {Weaken`} ξ)

  iCompAssocWeaken` : CompAssoc Weaken`
  ⊙-assoc {{iCompAssocWeaken`}} ξ₁ ξ₂ baseW      = refl
  ⊙-assoc {{iCompAssocWeaken`}} ξ₁ ξ₂ (stepW ξ₃) =
    cong stepW (⊙-assoc {Weaken`} ξ₁ ξ₂ ξ₃)

⊙-wkm-weaken` : {γ₁ γ₂ : Dom} (ξ : Weaken` γ₁ γ₂) (δ : Dom) →
  ξ ⊙ wkm {Weaken`} δ ≡ wk δ ξ
⊙-wkm-weaken` ξ zero = refl
⊙-wkm-weaken` ξ (suc δ) = cong stepW (⊙-wkm-weaken` ξ δ)

extensionality-weaken` : {γ₁ γ₂ : Dom} (ξ₁ ξ₂ : Weaken` γ₁ γ₂)
  (hyp : (i : Ix γ₁) → lk {Ix} ξ₁ i ≡ lk {Ix} ξ₂ i) →
  ξ₁ ≡ ξ₂
extensionality-weaken` baseW baseW           hyp = refl
extensionality-weaken` baseW (stepW ξ₂)      hyp = case hyp zero of λ ()
extensionality-weaken` (stepW ξ₁) baseW      hyp = case hyp zero of λ ()
extensionality-weaken` (stepW ξ₁) (stepW ξ₂) hyp =
  cong stepW (extensionality-weaken` ξ₁ ξ₂ (suc-inj ∘ hyp))

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

-- A cartesian functor preserves products (of cartesian categories)
module Categories.Functor.Cartesian where

open import Data.Product using (Σ; _,_)
open import Level

open import Categories.Category.Cartesian
open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Product
open import Categories.Functor using (Functor; _∘F_)
open import Categories.NaturalTransformation using (NaturalTransformation)

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

record CartesianF {A : Category o ℓ e} {B : Category o′ ℓ′ e′} (CA : Cartesian A) (CB : Cartesian B)
  (F : Functor A B) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module CA = Cartesian CA
    module CB = Cartesian CB
  field
    -- F is product preserving
    ε : B [ CB.⊤ , Functor.F₀ F CA.⊤ ]
    ⊗-homo : NaturalTransformation (CB.⊗ ∘F (F ⁂ F)) (F ∘F CA.⊗)


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

module Categories.Adjoint.Instance.0-Truncation where

-- The adjunction between 0-truncation and the inclusion functor from
-- Setoids to Categories/Groupoids.

open import Level using (Lift)
open import Data.Unit using (⊤)
import Function
open import Relation.Binary using (Setoid)
open import Function.Equality using (Π) renaming (id to idΠ)

open import Categories.Adjoint using (_⊣_)
open import Categories.Category.Construction.0-Groupoid using (0-Groupoid)
open import Categories.Category.Groupoid using (Groupoid)
open import Categories.Category.Instance.Groupoids using (Groupoids)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Instance.0-Truncation using (Trunc)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (refl)

-- The inclusion functor from Setoids to Groupoids

Inclusion : ∀ {c ℓ} e → Functor (Setoids c ℓ) (Groupoids c ℓ e)
Inclusion {c} {ℓ} e = record
  { F₀           = 0-Groupoid e
  ; F₁           = λ f → record { F₀ = f ⟨$⟩_ ; F₁ = cong f }
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = λ {S T f g} f≗g →
    let module S = Setoid S
        module T = Setoid T
    in record
    { F⇒G = record { η = λ _ → f≗g S.refl         }
    ; F⇐G = record { η = λ _ → T.sym (f≗g S.refl) }
    }
  }
  where open Π

-- Trunc is left-adjoint to the inclusion functor from Setoids to Groupoids

TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e
TruncAdj {o} {ℓ} {e} = record
  { unit   = unit
  ; counit = counit
  ; zig    = Function.id
  ; zag    = refl
  }
  where
    open Π
    open Groupoid using (category)

    unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
    unit = record
      { η           = λ _ → record { F₀ = Function.id ; F₁ = Function.id }
      ; commute     = λ _ → refl
      ; sym-commute = λ _ → refl
      }

    counit : NaturalTransformation (Trunc ∘F Inclusion e) idF
    counit = ntHelper record { η = λ S → idΠ ; commute = λ f → cong f }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module AbstractInterfaces where

open import Prelude public

-- Process identifiers.

record IsProc : Set₁ where
  field
    Proc    : Set
    _≡ₚ?_   : Decidable (_≡_ {A = Proc})
    _<ₚ_    : Proc → Proc → Set
    trans<ₚ : Transitive _<ₚ_
    tri<ₚ   : Trichotomous _≡_ _<ₚ_

  _≮ₚ_ : Proc → Proc → Set
  P ≮ₚ P′ = ¬ (P <ₚ P′)

open IsProc {{…}} public

-- Process clocks, message timestamps, and event timestamps.

record IsTime : Set₁ where
  field
    Time      : Set
    _≡ₜ?_     : Decidable (_≡_ {A = Time})
    _<ₜ_      : Time → Time → Set
    trans<ₜ   : Transitive _<ₜ_
    tri<ₜ     : Trichotomous _≡_ _<ₜ_
    irrefl<ₜ  : Irreflexive _<ₜ_
    sucₜ      : Time → Time
    _⊔ₜ_      : Time → Time → Time
    n<s[n⊔m]ₜ : ∀ T T′ → T <ₜ sucₜ (T ⊔ₜ T′)

  _≮ₜ_ : Time → Time → Set
  T ≮ₜ T′ = ¬ (T <ₜ T′)

open IsTime {{…}} public

-- Messages.

record IsMsg {{_ : IsProc}} {{_ : IsTime}} : Set₁ where
  field
    Msg : (Pᵢ Pⱼ : Proc) (Tₘ : Time) → Set

open IsMsg {{…}} public

-- Events within one process.

record IsEvent {{_ : IsProc}} {{_ : IsTime}} {{_ : IsMsg}} : Set₁ where
  field
    Event   : Proc → Time → Set

    isSendₑ : ∀ {Cᵢ Pᵢ Pⱼ Tₘ} {{_ : Tₘ ≡ sucₜ Cᵢ}} →
              Msg Pᵢ Pⱼ Tₘ → Event Pᵢ Tₘ → Set

    isRecvₑ : ∀ {Cⱼ Pᵢ Pⱼ Tₘ Tⱼ} {{_ : Tⱼ ≡ sucₜ (Tₘ ⊔ₜ Cⱼ)}} →
              Msg Pᵢ Pⱼ Tₘ → Event Pⱼ Tⱼ → Set

    absurdₑ : ∀ {Cᵢ Cⱼ P T} {m : Msg P P T} {a : Event P T} →
              {{_ : T ≡ sucₜ Cᵢ}} {{_ : T ≡ sucₜ (T ⊔ₜ Cⱼ)}} →
              ¬ (isSendₑ {Cᵢ} m a × isRecvₑ {Cⱼ} m a)

open IsEvent {{…}} public

max_stars_repo_name: mietek/lamport-timestamps

max_issues_repo_name: mietek/lamport-timestamps

max_forks_repo_name: mietek/lamport-timestamps


text:
-- Andreas, 2016-12-30, issue #1886, reported by nad
--
-- Omitted hidden parameters are not in scope.

postulate
  A : Set
  P : A → Set

data D {a} (X : P a) : Set₁

data D X where
  c : P a → D _

-- Expected error:
--
-- Not in scope: a

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Ch2-1 where

open import Level

infixl 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

J : {a b : Level} (A : Set a) (C : (x y : A) → x ≡ y → Set b)
    → ((x : A) → C x x refl)
    → (x y : A) (P : x ≡ y)
    → C x y P
J A C b x .x refl = b x

-- K : (A : Set) (x : A) (C : x ≡ x → Set)
--   → C refl
--   → (loop : x ≡ x)
--   → C loop
-- K A x C b p = {! p  !}

-- Lemma 2.1.1 (inversion of paths)
infix 6 ¬_
¬_ : {a : Level} {A : Set a} {x y : A} → x ≡ y → y ≡ x
¬_ {a} {A} {x} {y} p = J A D d x y p

  where
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = y ≡ x

    d : (x : A) → D x x refl
    d x = refl

-- Lemma 2.1.2 (concatenation of paths)
infixl 5 _∙_
_∙_ : {a : Level} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {a} {A} {x} {y} {z} p q = J {a} {a} A D d x y p z q

  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = (z : A) (q : y ≡ z) → x ≡ z

    -- base case
    d : (x : A) → D x x refl
    d x z q = J A E e x z q
      where
        -- the predicate
        E : (x z : A) (q : x ≡ z) → Set a
        E x z q = x ≡ z

        -- base case
        e : (x : A) → E x x refl
        e x = refl

-- Lemma 2.1.4.i (identity of path concatenation)
∙-identityʳ : {a : Level} {A : Set a} {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
∙-identityʳ {a} {A} {x} {y} p = J A D d x y p

  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = p ≡ p ∙ refl

    -- base case
    d : (x : A) → D x x refl
    d x = refl

∙-identityˡ : {a : Level} {A : Set a} {x y : A} (p : x ≡ y) → p ≡ refl ∙ p
∙-identityˡ {a} {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = p ≡ refl ∙ p

    -- base case
    d : (x : A) → D x x refl
    d x = refl

-- Lemma 2.1.4.ii (identity of path inversion)
¬-identityʳ : {a : Level} {A : Set a} {x y : A} (p : x ≡ y) → ¬ p ∙ p ≡ refl
¬-identityʳ {a} {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = ¬ p ∙ p ≡ refl

    -- base case
    d : (x : A) → D x x refl
    d x = refl

¬-identityˡ : {a : Level} {A : Set a} {x y : A} (p : x ≡ y) → p ∙ ¬ p ≡ refl
¬-identityˡ {a} {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = p ∙ ¬ p ≡ refl

    -- base case
    d : (x : A) → D x x refl
    d x = refl

-- Lemma 2.1.4.iii (involution of path inversion)
involution : {A : Set} {x y : A} (p : x ≡ y) → ¬ ¬ p ≡ p
involution {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set
    D x y p = ¬ ¬ p ≡ p

    -- base case
    d : (x : A) → D x x refl
    d x = refl

-- Lemma 2.1.4.iv (associativity of path concatenation)
∙-assoc : {a : Level} {A : Set a} {w x y z : A}
  → (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
  → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
∙-assoc {a} {A} {w} {x} {y} {z} p q r = J A D d w x p y q z r
  where
    -- the predicate
    D : (w x : A) (p : w ≡ x) → Set a
    D w x p = (y : A) (q : x ≡ y)
            → (z : A) (r : y ≡ z)
            → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r

    -- base case
    d : (x : A) → D x x refl
    d x y q z r = J A E e x y q z r
      where
        -- the predicate
        E : (x y : A) (q : x ≡ y) → Set a
        E x y q = (z : A) (r : y ≡ z)
                → refl ∙ (q ∙ r) ≡ refl ∙ q ∙ r

        -- base case
        e : (x : A) → E x x refl
        e x z r = J A F f x z r
          where
            -- the predicate
            F : (y z : A) (r : y ≡ z) → Set a
            F y z r = refl ∙ (refl ∙ r) ≡ refl ∙ refl ∙ r

            -- base case
            f : (x : A) → F x x refl
            f x = refl

open import Relation.Binary

isEquivalence : ∀ {a} {A : Set a} → IsEquivalence (_≡_ {a} {A})
isEquivalence = record
  { refl = refl
  ; sym = ¬_
  ; trans = _∙_
  }

setoid : ∀ {a} → Set a → Setoid _ _
setoid {a} A = record
  { Carrier       = A
  ; _≈_           = _≡_
  ; isEquivalence = isEquivalence {a} {A}
  }
-- module EckmannHilton where
--
--     -- begin
--     --   p ∙ refl
--     -- ≈⟨ ¬ ∙-identityʳ p ⟩
--     --   p
--     -- ≈⟨ α ⟩
--     --   q
--     -- ≈⟨ ∙-identityʳ q ⟩
--     --   q ∙ refl
--     -- ∎
--     -- where
--     --   open import Relation.Binary.Reasoning.Setoid (setoid (a ≡ x))
--
--   -- whisker right
--   infixl 6 _∙r_
--   _∙r_ : {A : Set} {a b c : A} {p q : a ≡ b}
--     → (α : p ≡ q) (r : b ≡ c)
--     → p ∙ r ≡ q ∙ r
--   _∙r_ {A} {a} {b} {c} {p} {q} α r = J A D d b c r a p q α
--     where
--       -- the predicate
--       D : (b c : A) (r : b ≡ c) → Set
--       D b c r = (a : A) (p q : a ≡ b) (α : p ≡ q)
--         → p ∙ r ≡ q ∙ r
--
--       -- base case
--       d : (x : A) → D x x refl
--       d x a p q α = J A E e a x p q
--         where
--           -- the predicate
--           E : (a x : A) (p : a ≡ x) → Set
--           E a x p = (q : a ≡ x) → p ∙ refl ≡ q ∙ refl
--
--           -- base case
--           e : (x : A) → E x x refl
--           e x q = {!   !}
--             where
--               -- the predicate
--               F : (a x : A) (q : a ≡ x) → Set
--               F a x q = {!   !}
--                 -- refl ∙ refl ≡ q ∙ refl
--                 -- refl ∙ refl ≡ q ∙ refl
--
--               -- base case
--               f : (x : A) → F x x refl
--               f x = {!   !}
--         --
--         -- ¬ ∙-identityʳ p ∙ α ∙ ∙-identityʳ q
--   --
--   --
--   -- -- whisker left
--   -- infixl 6 _∙l_
--   -- _∙l_ : {A : Set} {a b c : A} {r s : b ≡ c}
--   --   → (q : a ≡ b) (β : r ≡ s)
--   --   → q ∙ r ≡ q ∙ s
--   -- _∙l_ {A} {a} {b} {c} {r} {s} q β = J A D d a b q c r s β
--   --   where
--   --     -- the predicate
--   --     D : (a b : A) (q : a ≡ b) → Set
--   --     D a b q = (c : A) (r s : b ≡ c) (β : r ≡ s)
--   --       → q ∙ r ≡ q ∙ s
--   --
--   --     -- base case
--   --     d : (x : A) → D x x refl
--   --     d x c r s β = ¬ ∙-identityˡ r ∙ β ∙ ∙-identityˡ s
--   --
--   -- -- horizontal composition
--   -- _⋆_ : {A : Set} {a b c : A} {p q : a ≡ b} {r s : b ≡ c}
--   --   → (α : p ≡ q) (β : r ≡ s)
--   --   → p ∙ r ≡ q ∙ s
--   -- _⋆_ {A} {a} {b} {c} {p} {q} {r} {s} α β = (α ∙r r) ∙ (q ∙l β)
--   --
--   --   where
--   --     whisker-right-lemma : ∀ {A : Set} {a b : A}
--   --       → {p q : a ≡ b} {α : p ≡ q}
--   --       → α ∙r refl ≡ ¬ ∙-identityʳ p ∙ α ∙ ∙-identityʳ q
--   --     whisker-right-lemma {A} {a} {b} {p} {q} {α} = refl
--   --
--   --     whisker-left-lemma : ∀ {A : Set} {b c : A}
--   --       → {r s : b ≡ c} {β : r ≡ s}
--   --       → refl ∙l β ≡ ¬ ∙-identityˡ r ∙ β ∙ ∙-identityˡ s
--   --     whisker-left-lemma {A} {b} {c} {r} {s} {α} = refl
--   --
--   -- cong : {A B : Set} {x y : A}
--   --   → (f : A → B) (p : x ≡ y)
--   --   → f x ≡ f y
--   -- cong {A} {B} {x} {y} f p = J A D d x y p f
--   --   where
--   --     -- the predicate
--   --     D : (x y : A) (p : x ≡ y) → Set
--   --     D x y p = (f : A → B) → f x ≡ f y
--   --
--   --     -- base case
--   --     d : (x : A) → D x x refl
--   --     d x f = refl
--   --
--   -- cong2 : {A B C : Set} {x y : A} {a b : B}
--   --   → (f : A → B → C) (p : x ≡ y) (q : a ≡ b)
--   --   → f x a ≡ f y b
--   -- cong2 {A} {B} {C} {x} {y} {a} {b} f p q = J A D d x y p a b q f
--   --   -- J A D d x y p f
--   --   where
--   --     -- the predicate
--   --     D : (x y : A) (p : x ≡ y) → Set
--   --     D x y p = (a b : B) (q : a ≡ b) (f : A → B → C) → f x a ≡ f y b
--   --
--   --     -- base case
--   --     d : (x : A) → D x x refl
--   --     d x a b q f = cong (f x) q
--   --
--   --
--   -- -- theorem : {A : Set} {a b c : A}
--   -- --   → {p q : a ≡ b} {r s : b ≡ c}
--   -- --   → (α : p ≡ q) (β : r ≡ s)
--   -- --   → α ⋆ β ≡ cong2 _∙_ α β
--   -- -- theorem {A} {a} {b} {c} {p} {q} {r} {s} α β = J A D d a b p q c r s α β
--   -- --
--   -- --   where
--   -- --     -- the predicate
--   -- --     D : (a b : A) (p : a ≡ b) → Set
--   -- --     D a b p = (q : a ≡ b) (c : A) (r s : b ≡ c) (α : p ≡ q) (β : r ≡ s)
--   -- --       → α ⋆ β ≡ cong2 _∙_ α β
--   -- --
--   -- --     -- base case ʳˡ
--   -- --     d : (x : A) → D x x refl
--   -- --     d x q c r s α β = J A E e x c r s q α β
--   -- --
--   -- --       where
--   -- --         -- the predicate
--   -- --         E : (b c : A) (r : b ≡ c) → Set
--   -- --         E b c r = (s : b ≡ c) (q : b ≡ b) (α : refl ≡ q) (β : r ≡ s)
--   -- --           → α ⋆ β ≡ cong2 _∙_ α β
--   -- --
--   -- --         -- base case
--   -- --         e : (x : A) → E x x refl
--   -- --         e x s q α β = {!   !}

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


text:
------------------------------------------------------------------------
-- The "interval"
------------------------------------------------------------------------

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

-- Partly based on the HoTT book.

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

import Equality.Path as P

module Interval
  {c⁺} (eq : ∀ {a p} → P.Equality-with-paths a p c⁺) where

private
  open module D = P.Derived-definitions-and-properties eq hiding (elim)

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
import Equality.Path.Isomorphisms eq as I
open import Equivalence equality-with-J hiding (_∘_)
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J using (ext⁻¹)

private
  variable
    a p   : Level
    A B C : Type a

------------------------------------------------------------------------
-- The interval

-- The interval, defined as a higher inductive type.

data Interval : Type where
  [0] [1] : Interval
  0≡1ᴾ    : [0] P.≡ [1]

-- [0] is equal to [1].

0≡1 : [0] ≡ [1]
0≡1 = _↔_.from ≡↔≡ 0≡1ᴾ

-- An eliminator, expressed using paths.

elimᴾ :
  (P : Interval → Type p)
  (p₀ : P [0])
  (p₁ : P [1]) →
  P.[ (λ i → P (0≡1ᴾ i)) ] p₀ ≡ p₁ →
  (x : Interval) → P x
elimᴾ P p₀ p₁ p₀≡p₁ = λ where
  [0]      → p₀
  [1]      → p₁
  (0≡1ᴾ i) → p₀≡p₁ i

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

recᴾ : (p₀ p₁ : A) → p₀ P.≡ p₁ → Interval → A
recᴾ = elimᴾ _

-- An eliminator.

module Elim
  (P : Interval → Type p)
  (p₀ : P [0])
  (p₁ : P [1])
  (p₀≡p₁ : subst P 0≡1 p₀ ≡ p₁)
  where

  -- The eliminator.

  elim : (x : Interval) → P x
  elim = elimᴾ P p₀ p₁ (I.subst≡→[]≡ p₀≡p₁)

  -- A "computation" rule for elim.

  elim-0≡1 : dcong elim 0≡1 ≡ p₀≡p₁
  elim-0≡1 = I.dcong-subst≡→[]≡ (refl _)

open Elim public

-- A non-dependent eliminator.

module Rec
  (p₀ p₁ : A)
  (p₀≡p₁ : p₀ ≡ p₁)
  where

  -- The eliminator.

  rec : Interval → A
  rec = recᴾ p₀ p₁ (_↔_.to ≡↔≡ p₀≡p₁)

  -- A computation rule for rec.

  rec-0≡1 : cong rec 0≡1 ≡ p₀≡p₁
  rec-0≡1 = I.cong-≡↔≡ (refl _)

open Rec public

------------------------------------------------------------------------
-- Contractibility

-- The interval is contractible.

interval-contractible : Contractible Interval
interval-contractible = [1] , sym ∘ f
  where
  f : (x : Interval) → x ≡ [1]
  f = elim (_≡ [1]) 0≡1 (refl _)
        (subst (_≡ [1]) 0≡1 0≡1              ≡⟨ cong (λ p → subst (_≡ [1]) p 0≡1)
                                                     (sym $ sym-sym 0≡1) ⟩
         subst (_≡ [1]) (sym (sym 0≡1)) 0≡1  ≡⟨ subst-trans (sym 0≡1) ⟩
         trans (sym 0≡1) 0≡1                 ≡⟨ trans-symˡ 0≡1 ⟩∎
         refl _                              ∎)

-- A simplification lemma for rec p p.

rec-const :
  ∀ {p} {P : Type p} (p : P) (p≡p : p ≡ p) i →
  rec p p p≡p i ≡ p
rec-const p p≡p i =
  rec p p p≡p i    ≡⟨ cong (rec p p p≡p) (mono₁ 0 interval-contractible i [0]) ⟩∎
  rec p p p≡p [0]  ∎

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

-- The definition of bad-ext has been placed in a separate abstract
-- block to ensure that the definitions in the other abstract block
-- below do not accidentally depend on the implementation of bad-ext.

private
 module Separate-abstract-block where

  abstract

    -- The interval can be used to prove that equality of functions is
    -- extensional.
    --
    -- The proof bad-ext is perhaps not less "good" than ext (I don't
    -- know), it is called this simply because it is not defined using
    -- good-ext.

    private

      -- ext-helper {f = f} {g = g} f≡g reduces to λ x → f x when the
      -- input is [0], and to λ x → g x when the input is [1].

      ext-helper :
        ∀ {a b} {A : Type a} {B : A → Type b} {f g : (x : A) → B x} →
        (∀ x → f x ≡ g x) → Interval → (x : A) → B x
      ext-helper {f = f} {g} f≡g i =
        λ x → rec (f x) (g x) (f≡g x) i

    bad-ext : ∀ {a b} → Extensionality a b
    apply-ext bad-ext {f = f} {g = g} f≡g =
      f                   ≡⟨⟩
      ext-helper f≡g [0]  ≡⟨ cong (ext-helper f≡g) 0≡1 ⟩∎
      ext-helper f≡g [1]  ∎

open Separate-abstract-block public

ext : ∀ {a b} → Extensionality a b
ext = good-ext bad-ext

⟨ext⟩ : ∀ {a b} {A : Type a} {B : A → Type b} → Extensionality′ A B
⟨ext⟩ = apply-ext ext

abstract

  -- The function ⟨ext⟩ is an equivalence.

  ext-is-equivalence :
    ∀ {a b} {A : Type a} {B : A → Type b} {f g : (x : A) → B x} →
    Is-equivalence {A = ∀ x → f x ≡ g x} ⟨ext⟩
  ext-is-equivalence = good-ext-is-equivalence bad-ext

  -- Equality rearrangement lemmas for ⟨ext⟩.

  ext-refl :
    ∀ {a b} {A : Type a} {B : A → Type b} (f : (x : A) → B x) →
    ⟨ext⟩ (λ x → refl (f x)) ≡ refl f
  ext-refl = good-ext-refl bad-ext

  ext-const :
    ∀ {a b} {A : Type a} {B : Type b} {x y : B}
    (x≡y : x ≡ y) →
    ⟨ext⟩ (const {B = A} x≡y) ≡ cong const x≡y
  ext-const = good-ext-const bad-ext

  cong-ext :
    ∀ {a b} {A : Type a} {B : A → Type b} {f g : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) {x} →
    cong (_$ x) (⟨ext⟩ f≡g) ≡ f≡g x
  cong-ext = cong-good-ext bad-ext

  ext-cong :
    ∀ {a b c} {A : Type a} {B : Type b} {C : B → Type c}
    {f : A → (x : B) → C x} {x y : A} {x≡y : x ≡ y} →
    ⟨ext⟩ (λ z → cong (flip f z) x≡y) ≡ cong f x≡y
  ext-cong = good-ext-cong bad-ext

  subst-ext :
    ∀ {a b p} {A : Type a} {B : A → Type b} {f g : (x : A) → B x} {x}
    (P : B x → Type p) {p} (f≡g : ∀ x → f x ≡ g x) →
    subst (λ f → P (f x)) (⟨ext⟩ f≡g) p ≡ subst P (f≡g x) p
  subst-ext = subst-good-ext bad-ext

  elim-ext :
    ∀ {a b p} {A : Type a} {B : A → Type b} {x : A}
    (P : B x → B x → Type p)
    (p : (y : B x) → P y y)
    {f g : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) →
    D.elim (λ {f g} _ → P (f x) (g x)) (p ∘ (_$ x)) (⟨ext⟩ f≡g) ≡
    D.elim (λ {x y} _ → P x y) p (f≡g x)
  elim-ext = elim-good-ext bad-ext

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

  ext-sym :
    ∀ {a b} {A : Type a} {B : A → Type b} {f g : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) →
    ⟨ext⟩ (sym ∘ f≡g) ≡ sym (⟨ext⟩ f≡g)
  ext-sym = good-ext-sym bad-ext

  ext-trans :
    ∀ {a b} {A : Type a} {B : A → Type b} {f g h : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) (g≡h : ∀ x → g x ≡ h x) →
    ⟨ext⟩ (λ x → trans (f≡g x) (g≡h x)) ≡ trans (⟨ext⟩ f≡g) (⟨ext⟩ g≡h)
  ext-trans = good-ext-trans bad-ext

  cong-post-∘-ext :
    ∀ {a b c} {A : Type a} {B : A → Type b} {C : A → Type c}
      {f g : (x : A) → B x} {h : ∀ {x} → B x → C x}
    (f≡g : ∀ x → f x ≡ g x) →
    cong (h ∘_) (⟨ext⟩ f≡g) ≡ ⟨ext⟩ (cong h ∘ f≡g)
  cong-post-∘-ext {h = h} = cong-post-∘-good-ext {h = h} bad-ext bad-ext

  cong-pre-∘-ext :
    ∀ {a b c} {A : Type a} {B : Type b} {C : B → Type c}
      {f g : (x : B) → C x} {h : A → B}
    (f≡g : ∀ x → f x ≡ g x) →
    cong (_∘ h) (⟨ext⟩ f≡g) ≡ ⟨ext⟩ (f≡g ∘ h)
  cong-pre-∘-ext = cong-pre-∘-good-ext bad-ext bad-ext

  cong-∘-ext :
    {f g : B → C}
    (f≡g : ∀ x → f x ≡ g x) →
    cong {B = (A → B) → (A → C)}
         (λ f → f ∘_) (⟨ext⟩ f≡g) ≡
    ⟨ext⟩ λ h → ⟨ext⟩ λ x → f≡g (h x)
  cong-∘-ext = cong-∘-good-ext bad-ext bad-ext bad-ext

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2017-01-26.
-- The --no-eta-equality option

{-# OPTIONS --no-eta-equality #-}
{-# OPTIONS --allow-unsolved-metas #-}

-- is only valid for the record types defined in this file.

open import HaveEtaForImportedRecords.EtaRecord

-- Eta holds for the imported record.

test-imported : ∀{x y : ⊤} → x ≡ y
test-imported = refl

-- Eta does not hold for a record defined here

record Unit : Set where

test : Unit
test = _   -- Should be yellow!

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Correctness of differentiation (Lemma 3.10 and Theorem 3.11).
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Denotation.Value as Value
import Parametric.Denotation.Evaluation as Evaluation
import Parametric.Change.Validity as Validity
import Parametric.Change.Specification as Specification
import Parametric.Change.Type as ChangeType
import Parametric.Change.Term as ChangeTerm
import Parametric.Change.Value as ChangeValue
import Parametric.Change.Evaluation as ChangeEvaluation
import Parametric.Change.Derive as Derive
import Parametric.Change.Implementation as Implementation

module Parametric.Change.Correctness
    {Base : Type.Structure}
    (Const : Term.Structure Base)
    (⟦_⟧Base : Value.Structure Base)
    (⟦_⟧Const : Evaluation.Structure Const ⟦_⟧Base)
    (ΔBase : ChangeType.Structure Base)
    (apply-base : ChangeTerm.ApplyStructure Const ΔBase)
    (diff-base : ChangeTerm.DiffStructure Const ΔBase)
    (nil-base : ChangeTerm.NilStructure Const ΔBase)
    (⟦apply-base⟧ : ChangeValue.ApplyStructure Const ⟦_⟧Base ΔBase)
    (⟦diff-base⟧ : ChangeValue.DiffStructure Const ⟦_⟧Base ΔBase)
    (⟦nil-base⟧ : ChangeValue.NilStructure Const ⟦_⟧Base ΔBase)
    (meaning-⊕-base : ChangeEvaluation.ApplyStructure
      ⟦_⟧Base ⟦_⟧Const ΔBase apply-base diff-base nil-base ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧)
    (meaning-⊝-base : ChangeEvaluation.DiffStructure
      ⟦_⟧Base ⟦_⟧Const ΔBase apply-base diff-base nil-base ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧)
    (meaning-onil-base : ChangeEvaluation.NilStructure
      ⟦_⟧Base ⟦_⟧Const ΔBase apply-base diff-base nil-base ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧)
    {{validity-structure : Validity.Structure ⟦_⟧Base}}
    (derive-const : Derive.Structure Const ΔBase)
    (implementation-structure : Implementation.Structure
      Const ⟦_⟧Base ⟦_⟧Const ΔBase
      ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧ derive-const)
  where

open Type.Structure Base
open Term.Structure Base Const
open Value.Structure Base ⟦_⟧Base
open Evaluation.Structure Const ⟦_⟧Base ⟦_⟧Const
open Validity.Structure ⟦_⟧Base {{validity-structure}}
open Specification.Structure Const ⟦_⟧Base ⟦_⟧Const
open ChangeType.Structure Base ΔBase
open ChangeTerm.Structure Const ΔBase apply-base diff-base nil-base
open ChangeValue.Structure Const ⟦_⟧Base ΔBase ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧
open ChangeEvaluation.Structure
  ⟦_⟧Base ⟦_⟧Const ΔBase
  apply-base diff-base nil-base
  ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧
  meaning-⊕-base meaning-⊝-base meaning-onil-base
open Derive.Structure Const ΔBase derive-const
open Implementation.Structure implementation-structure
-- The denotational properties of the `derive` transformation.
-- In particular, the main theorem about it producing the correct
-- incremental behavior.

open import Base.Denotation.Notation
open import Relation.Binary.PropositionalEquality
open import Postulate.Extensionality

-- Extension point: A proof that change evaluation for a
-- primitive is related to the value of incrementalizing
-- this primitive.
Structure : Set
Structure = ∀ {τ} (c : Const τ) →
  nil₍ τ ₎ ⟦ c ⟧Const ≈₍ τ ₎ ⟦ derive-const c ⟧Term ∅

module Structure (derive-const-correct : Structure) where
  deriveVar-correct : ∀ {τ Γ} (x : Var Γ τ)
    (ρ : ⟦ Γ ⟧) (dρ : Δ₍ Γ ₎ ρ) (ρ′ : ⟦ mapContext ΔType Γ ⟧) (dρ≈ρ′ : implements-env Γ dρ ρ′) →
    ⟦ x ⟧ΔVar ρ dρ ≈₍ τ ₎ ⟦ deriveVar x ⟧ (alternate ρ ρ′)
  deriveVar-correct this (v • ρ) (dv • dρ) (dv′ • dρ′) (dv≈dv′ • dρ≈dρ′) = dv≈dv′
  deriveVar-correct (that x) (v • ρ) (dv • dρ) (dv′ • dρ′) (dv≈dv′ • dρ≈dρ′) = deriveVar-correct x ρ dρ dρ′ dρ≈dρ′

  derive-const-env-irrelevant : ∀ {Γ τ} (c : Const τ) → (ρ : ⟦ ΔContext Γ ⟧) → ⟦ weaken ∅≼Γ (derive-const c) ⟧Term ρ ≡
      ⟦ derive-const c ⟧Term ∅
  derive-const-env-irrelevant {Γ} c ρ =
    trans
      (weaken-sound {Γ₁≼Γ₂ = (∅≼Γ {ΔContext Γ})} (derive-const c) ρ)
      (cong ⟦ derive-const c ⟧Term (⟦∅≼Γ⟧-∅ ρ))
  -- We provide: A variant of Lemma 3.10 for arbitrary contexts.
  derive-correct : ∀ {τ Γ} (t : Term Γ τ)
    (ρ : ⟦ Γ ⟧) (dρ : Δ₍ Γ ₎ ρ) (ρ′ : ⟦ mapContext ΔType Γ ⟧) (dρ≈ρ′ : implements-env Γ dρ ρ′) →
    ⟦ t ⟧Δ ρ dρ ≈₍ τ ₎ ⟦ derive t ⟧ (alternate ρ ρ′)

  derive-correct {τ} {Γ} (const c) ρ dρ ρ′ dρ≈ρ′ =
    subst (implements τ (nil₍ τ ₎ ⟦ c ⟧Const))
      (sym (derive-const-env-irrelevant c (alternate ρ ρ′)))
      (derive-const-correct c)
  derive-correct (var x) ρ dρ ρ′ dρ≈ρ′ =
    deriveVar-correct x ρ dρ ρ′ dρ≈ρ′
  derive-correct (app {σ} {τ} s t) ρ dρ ρ′ dρ≈ρ′
   = subst (λ ⟦t⟧ → ⟦ app s t ⟧Δ ρ dρ ≈₍ τ ₎ (⟦ derive s ⟧Term (alternate ρ ρ′)) ⟦t⟧ (⟦ derive t ⟧Term (alternate ρ ρ′))) (⟦fit⟧ t ρ ρ′)
       (derive-correct {σ ⇒ τ} s ρ dρ ρ′ dρ≈ρ′
          (⟦ t ⟧ ρ) (⟦ t ⟧Δ ρ dρ) (⟦ derive t ⟧ (alternate ρ ρ′)) (derive-correct {σ} t ρ dρ ρ′ dρ≈ρ′))

  derive-correct (abs {σ} {τ} t) ρ dρ ρ′ dρ≈ρ′ =
    λ w dw w′ dw≈w′ →
      derive-correct t (w • ρ) (dw • dρ) (w′ • ρ′) (dw≈w′ • dρ≈ρ′)

  derive-correct-closed : ∀ {τ} (t : Term ∅ τ) →
    ⟦ t ⟧Δ ∅ ∅ ≈₍ τ ₎ ⟦ derive t ⟧ ∅

  derive-correct-closed t = derive-correct t ∅ ∅ ∅ ∅

  -- And we proof Theorem 3.11, finally.
  main-theorem : ∀ {σ τ}
    {f : Term ∅ (σ ⇒ τ)} {s : Term ∅ σ} {ds : Term ∅ (ΔType σ)} →
    {dv : Δ₍ σ ₎ (⟦ s ⟧ ∅)} {erasure : dv ≈₍ σ ₎ (⟦ ds ⟧ ∅)} →

    ⟦ app f (s ⊕₍ σ ₎ ds) ⟧ ≡ ⟦ app f s ⊕₍ τ ₎ app (app (derive f) s) ds ⟧

  main-theorem {σ} {τ} {f} {s} {ds} {dv} {erasure} =
    let
      g  = ⟦ f ⟧ ∅
      Δg = ⟦ f ⟧Δ ∅ ∅
      Δg′ = ⟦ derive f ⟧ ∅
      v  = ⟦ s ⟧ ∅
      dv′ = ⟦ ds ⟧ ∅
      u  = ⟦ s ⊕₍ σ ₎ ds ⟧ ∅
      -- Δoutput-term = app (app (derive f) x) (y ⊝ x)
    in
      ext {A = ⟦ ∅ ⟧Context} (λ { ∅ →
      begin
        g u
      ≡⟨ cong g (sym (meaning-⊕ {t = s} {Δt = ds})) ⟩
        g (v ⟦⊕₍ σ ₎⟧ dv′)
      ≡⟨ cong g (sym (carry-over {σ} dv erasure)) ⟩
        g (v ⊞₍ σ ₎ dv)
      ≡⟨ corollary-closed {σ} {τ} f v dv ⟩
        g v ⊞₍ τ ₎ call-change {σ} {τ} Δg v dv
      ≡⟨ carry-over {τ} (call-change {σ} {τ} Δg v dv)
           (derive-correct-closed f v dv dv′ erasure) ⟩
        g v ⟦⊕₍ τ ₎⟧ Δg′ v dv′
      ≡⟨ meaning-⊕ {t = app f s} {Δt = app (app (derive f) s) ds} ⟩
        ⟦ app f s ⊕₍ τ ₎ app (app (derive f) s) ds ⟧ ∅
      ∎}) where open ≡-Reasoning

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Data.Nat.Properties.Extra where

open import Data.Nat
open import Data.Product
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Function
open import Level using ()
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Nullary.Negation
open import Relation.Nullary
-- open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality hiding (isPreorder)
open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

------------------------------------------------------------------------
-- Misc
------------------------------------------------------------------------

isDecTotalOrder : IsDecTotalOrder {A = ℕ} _≡_ _≤_
isDecTotalOrder = DecTotalOrder.isDecTotalOrder decTotalOrder

isTotalOrder : IsTotalOrder {A = ℕ} _≡_ _≤_
isTotalOrder = IsDecTotalOrder.isTotalOrder isDecTotalOrder

isPartialOrder : IsPartialOrder {A = ℕ} _≡_ _≤_
isPartialOrder = IsTotalOrder.isPartialOrder isTotalOrder

isPreorder : IsPreorder {A = ℕ} _≡_ _≤_
isPreorder = IsPartialOrder.isPreorder isPartialOrder

open import Algebra.Structures
import Algebra.FunctionProperties as P; open P (_≡_ {A = ℕ})

isSemiringWithoutOne : IsSemiringWithoutOne _≡_ _⊔_ _⊓_ zero
isSemiringWithoutOne = IsCommutativeSemiringWithoutOne.isSemiringWithoutOne ⊔-⊓-0-isCommutativeSemiringWithoutOne

+-isCommutativeMonoid : IsCommutativeMonoid _≡_ _⊔_ zero
+-isCommutativeMonoid = IsSemiringWithoutOne.+-isCommutativeMonoid  isSemiringWithoutOne

cmp : Trichotomous _≡_ _<_
cmp = StrictTotalOrder.compare strictTotalOrder

⊓-comm : Commutative _⊓_
⊓-comm = IsCommutativeSemiringWithoutOne.*-comm ⊔-⊓-0-isCommutativeSemiringWithoutOne

⊔-comm : Commutative _⊔_
⊔-comm = IsCommutativeMonoid.comm +-isCommutativeMonoid

------------------------------------------------------------------------
-- Equational
------------------------------------------------------------------------

-- ℕ
cancel-suc : ∀ {x y} → suc x ≡ suc y → x ≡ y
cancel-suc {x} {.x} refl = refl
-- cancel-suc : ∀ {x y} → suc x ≡ suc y → x ≡ y
-- cancel-suc {x} {.x} refl = refl

-- _+_
[a+b]+c≡[a+c]+b : ∀ a b c → a + b + c ≡ a + c + b
[a+b]+c≡[a+c]+b a b c =
    begin
        a + b + c
    ≡⟨ +-assoc a b c ⟩
        a + (b + c)
    ≡⟨ cong (λ x → a + x) (+-comm b c) ⟩
        a + (c + b)
    ≡⟨ sym (+-assoc a c b) ⟩
        a + c + b
    ∎

a+[b+c]≡b+[a+c] : ∀ a b c → a + (b + c) ≡ b + (a + c)
a+[b+c]≡b+[a+c] a b c =
    begin
        a + (b + c)
    ≡⟨ sym (+-assoc a b c) ⟩
        a + b + c
    ≡⟨ cong (λ x → x + c) (+-comm a b) ⟩
        b + a + c
    ≡⟨ +-assoc b a c ⟩
        b + (a + c)
    ∎

cancel-+-right : ∀ k {i j} → i + k ≡ j + k → i ≡ j
cancel-+-right zero {i} {j} p  =
    begin
        i
    ≡⟨ sym (+-right-identity i) ⟩
        i + zero
    ≡⟨ p ⟩
        j + zero
    ≡⟨ +-right-identity j ⟩
        j
    ∎
cancel-+-right (suc k) {i} {j} p = cancel-+-right k lemma
    where   lemma : i + k ≡ j + k
            lemma = cancel-suc $
                begin
                    suc (i + k)
                ≡⟨ sym (+-suc i k) ⟩
                    i + suc k
                ≡⟨ p ⟩
                    j + suc k
                ≡⟨ +-suc j k ⟩
                    suc (j + k)
                ∎

-- _*_
*-right-identity : ∀ n → n * 1 ≡ n
*-right-identity zero    = refl
*-right-identity (suc n) = cong suc (*-right-identity n)

*-left-identity : ∀ n → 1 * n ≡ n
*-left-identity zero    = refl
*-left-identity (suc n) = cong suc (*-left-identity n)

distrib-left-*-+ : ∀ m n o → m * (n + o) ≡ m * n + m * o
distrib-left-*-+ m n o =
    begin
        m * (n + o)
    ≡⟨ *-comm m (n + o) ⟩
        (n + o) * m
    ≡⟨ distribʳ-*-+ m n o ⟩
        n * m + o * m
    ≡⟨ cong₂ _+_ (*-comm n m) (*-comm o m) ⟩
        m * n + m * o
    ∎

-- _∸_
m∸n+n≡m : ∀ {m n} → n ≤ m → m ∸ n + n ≡ m
m∸n+n≡m {m} {n} n≤m =
    begin
        m ∸ n + n
    ≡⟨ +-comm (m ∸ n) n ⟩
        n + (m ∸ n)
    ≡⟨ m+n∸m≡n n≤m ⟩
        m
    ∎

m∸[o∸n]+o≡m+n : ∀ m n o
    → n ≤ o
    → o ∸ n ≤ m
    → m ∸ ( o ∸ n ) + o ≡ m + n
m∸[o∸n]+o≡m+n m n o n≤o o∸n≤m =
    begin
        m ∸ (o ∸ n) + o
    ≡⟨ +-comm (m ∸ (o ∸ n)) o ⟩
        o + (m ∸ (o ∸ n))
    ≡⟨ cong (λ x → x + (m ∸ (o ∸ n))) (sym (m+n∸m≡n {n} {o} n≤o)) ⟩
        (n + (o ∸ n)) + (m ∸ (o ∸ n))
    ≡⟨ +-assoc n (o ∸ n) (m ∸ (o ∸ n)) ⟩
        n + ((o ∸ n) + (m ∸ (o ∸ n)))
    ≡⟨ cong (λ w → n + w) (m+n∸m≡n {o ∸ n} o∸n≤m) ⟩
        n + m
    ≡⟨ +-comm n m ⟩
        m + n
    ∎

------------------------------------------------------------------------
-- Relational
------------------------------------------------------------------------

-- _≤_
≤-trans : Transitive _≤_
≤-trans = IsPreorder.trans isPreorder

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ {zero} p = z≤n
<⇒≤ {suc i} (s≤s p) = s≤s (<⇒≤ p)

>⇒≰ : _>_ ⇒ _≰_
>⇒≰ {zero}  ()      q
>⇒≰ {suc m} (s≤s p) (s≤s q) = >⇒≰ p q

≤⇒≯ : _≤_ ⇒ _≯_
≤⇒≯ {zero} p ()
≤⇒≯ {suc m} (s≤s p) (s≤s q) = ≤⇒≯ p q

<⇒≱ : _<_ ⇒ _≱_
<⇒≱ {zero} () z≤n
<⇒≱ {suc i} (s≤s p) (s≤s q) = <⇒≱ p q

>⇒≢ : _>_ ⇒ _≢_
>⇒≢ {zero} () refl
>⇒≢ {suc m} (s≤s m>n) refl = >⇒≢ m>n refl

≥⇒≮ : _≥_ ⇒ _≮_
≥⇒≮ z≤n     ()
≥⇒≮ (s≤s m) (s≤s p) = ≥⇒≮ m p

<⇒≢ : _<_ ⇒ _≢_
<⇒≢ {zero} () refl
<⇒≢ {suc m} (s≤s m<n) refl = <⇒≢ m<n refl

≤∧≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
≤∧≢⇒< {zero}  {zero}  p       q = contradiction refl q
≤∧≢⇒< {zero}  {suc n} p       q = s≤s z≤n
≤∧≢⇒< {suc m} {zero}  ()      q
≤∧≢⇒< {suc m} {suc n} (s≤s p) q = s≤s (≤∧≢⇒< p (q ∘ cong suc))

≥∧≢⇒> : ∀ {m n} → m ≥ n → m ≢ n → m > n
≥∧≢⇒> {zero}  {zero}  p       q = contradiction refl q
≥∧≢⇒> {zero}  {suc n} ()      q
≥∧≢⇒> {suc m} {zero}  p       q = s≤s z≤n
≥∧≢⇒> {suc m} {suc n} (s≤s p) q = s≤s (≥∧≢⇒> p (q ∘ cong suc))

≤0⇒≡0 : ∀ n → n ≤ 0 → n ≡ 0
≤0⇒≡0 zero    n≤0 = refl
≤0⇒≡0 (suc n) ()

-- ≤-suc : ∀ {m n} → m ≤ n → suc m ≤ suc n
-- ≤-suc z≤n = s≤s z≤n
-- ≤-suc (s≤s rel) = s≤s (s≤s rel)

-- i*j>0⇒i>0∧j>0 : ∀ i j → i * j > 0 → (i > 0 × j > 0)
-- i*j>0⇒i>0∧j>0 zero j ()
-- i*j>0⇒i>0∧j>0 (suc i) zero p = contradiction (proj₂ (i*j>0⇒i>0∧j>0 i 0 p)) (λ ())
-- i*j>0⇒i>0∧j>0 (suc i) (suc j) p = s≤s z≤n , s≤s z≤n

-- _+_
-- m≡n+o⇒m≥o : ∀ {m} {o} n → m ≡ n + o → m ≥ o
-- m≡n+o⇒m≥o {.(n + o)} {o} n refl = n≤m+n o n

n+-mono : ∀ n → (λ x → n + x) Preserves _≤_ ⟶ _≤_
n+-mono n = _+-mono_ {n} {n} ≤-refl

n+-mono-inverse : ∀ n → ∀ {a b} → n + a ≤ n + b → a ≤ b
n+-mono-inverse zero    a≤b       = a≤b
n+-mono-inverse (suc n) (s≤s a≤b) = n+-mono-inverse n a≤b

+n-mono : ∀ n → (λ x → x + n) Preserves _≤_ ⟶ _≤_
+n-mono n {a} {b} a≤b = _+-mono_ {a} {b} {n} {n} a≤b ≤-refl

+n-mono-inverse : ∀ n → ∀ {a b} → a + n ≤ b + n → a ≤ b
+n-mono-inverse zero    {a} {b} p =
    start
        a
    ≈⟨ sym (+-right-identity a) ⟩
        a + 0
    ≤⟨ p ⟩
        b + 0
    ≈⟨ +-right-identity b ⟩
        b
    □
+n-mono-inverse (suc n) {a} {b} p = +n-mono-inverse n p'
    where   p' : a + n ≤ b + n
            p' = ≤-pred $ start
                    suc (a + n)
                ≈⟨ sym (+-suc a n) ⟩
                    a + suc n
                ≤⟨ p ⟩
                    b + suc n
                ≈⟨ +-suc b n ⟩
                    suc (b + n)
                □

+-mono-contra : ∀ {a b c d} → a ≥ b → a + c < b + d → c < d
+-mono-contra {zero} {zero} p q = q
+-mono-contra {zero} {suc b} () q
+-mono-contra {suc a} {zero} {c} {d} p q =
    start
        suc c
    ≤⟨ n≤m+n (suc a) (suc c) ⟩
        suc a + suc c
    ≈⟨ +-suc (suc a) c ⟩
        suc (suc a) + c
    ≤⟨ q ⟩
        d
    □
+-mono-contra {suc a} {suc b} (s≤s p) (s≤s q) = +-mono-contra p q

-- _∸_
∸n-mono : ∀ n → (λ x → x ∸ n) Preserves _≤_ ⟶ _≤_
∸n-mono n {a} {b} a≤b = ∸-mono {a} {b} {n} {n} a≤b ≤-refl

∸n-mono-inverse :  ∀ n → ∀ {a b} → a > n → a ∸ n ≤ b ∸ n → a ≤ b
∸n-mono-inverse zero                    p q = q
∸n-mono-inverse (suc n) {zero}  {zero}  p q = q
∸n-mono-inverse (suc n) {zero}  {suc b} p q = z≤n
∸n-mono-inverse (suc n) {suc a} {zero}  p q = contradiction (≤-pred p) (≤⇒≯ q')
    where
        q' : a ≤ n
        q' = ∸n-mono-inverse n (≤-pred p) $
            start
                a ∸ n
            ≤⟨ q ⟩
                zero
            ≈⟨ sym (n∸n≡0 n) ⟩
                n ∸ n
            □
∸n-mono-inverse (suc n) {suc a} {suc b} p q = s≤s (∸n-mono-inverse n (≤-pred p) q)

n∸-mono : ∀ n → (λ x → n ∸ x) Preserves _≥_ ⟶ _≤_
n∸-mono n {a} {b} a≥b = ∸-mono {n} {n} {a} {b} ≤-refl a≥b

m≥n+o⇒m∸o≥n : ∀ m n o → m ≥ n + o → m ∸ o ≥ n
m≥n+o⇒m∸o≥n m n o p =
    start
        n
    ≈⟨ sym (m+n∸n≡m n o) ⟩
        n + o ∸ o
    ≤⟨ ∸-mono {n + o} {m} {o} p ≤-refl ⟩
        m ∸ o
    □

cancel-∸-right : ∀ {m n} o → m ≥ o → n ≥ o → m ∸ o ≡ n ∸ o → m ≡ n
cancel-∸-right                 zero    p  q  eq = eq
cancel-∸-right {zero}          (suc o) () q  eq
cancel-∸-right {suc m} {zero}  (suc o) p  () eq
cancel-∸-right {suc m} {suc n} (suc o) p  q  eq = cong suc (cancel-∸-right o (≤-pred p) (≤-pred q) eq)

-- _*_
n*-mono : ∀ n → (λ x → n * x) Preserves _≤_ ⟶ _≤_
n*-mono n = _*-mono_ {n} {n} ≤-refl

n*-mono-strict-inverse : ∀ n {a} {b} → n * a < n * b → a < b
n*-mono-strict-inverse zero ()
n*-mono-strict-inverse (suc n) {a} {b} p with suc a ≤? b
n*-mono-strict-inverse (suc n) {a} {b} p | yes q = q
n*-mono-strict-inverse (suc n) {a} {b} p | no ¬q = contradiction p ¬p
    where
        ¬q' : b ≤ a
        ¬q' = ≤-pred (≰⇒> ¬q)
        ¬p : suc (suc n * a) ≰ suc n * b
        ¬p = >⇒≰ (s≤s (n*-mono (suc n) ¬q'))

*n-mono : ∀ n → (λ x → x * n) Preserves _≤_ ⟶ _≤_
*n-mono n {a} {b} a≤b = _*-mono_ {a} {b} {n} {n} a≤b ≤-refl

*-comm-mono : ∀ {a b c d} → a * b ≤ c * d → b * a ≤ d * c
*-comm-mono {a} {b} {c} {d} p =
    start
        b * a
    ≈⟨ *-comm b a ⟩
        a * b
    ≤⟨ p ⟩
        c * d
    ≈⟨ *-comm c d ⟩
        d * c
    □

*-comm-mono-strict : ∀ {a b c d} → a * b < c * d → b * a < d * c
*-comm-mono-strict {a} {b} {c} {d} p =
    start
        suc (b * a)
    ≈⟨ cong suc (*-comm b a) ⟩
        suc (a * b)
    ≤⟨ p ⟩
        c * d
    ≈⟨ *-comm c d ⟩
        d * c
    □

*n-mono-inverse : ∀ n {a} {b} → a * (suc n) ≤ b * (suc n) → a ≤ b
*n-mono-inverse n {zero}          p       = z≤n
*n-mono-inverse n {suc a} {zero}  ()
*n-mono-inverse n {suc a} {suc b} (s≤s p) = s≤s (*n-mono-inverse n (n+-mono-inverse n p))

*n-mono-strict-inverse : ∀ n {a} {b} → a * n < b * n → a < b
*n-mono-strict-inverse n {a} {b} p = n*-mono-strict-inverse n (*-comm-mono-strict {a} {n} {b} {n} p)

m≤m*1+n : ∀ m n → m ≤ m * suc n
m≤m*1+n m zero = reflexive (sym (*-right-identity m))
m≤m*1+n m (suc n) =
    start
        m
    ≤⟨ m≤m+n m (m * suc n) ⟩
        m + m * suc n
    ≈⟨ sym (+-*-suc m (suc n)) ⟩
        m * suc (suc n)
    □

-- _⊔_
m≤n⊔m : ∀ m n → m ≤ n ⊔ m
m≤n⊔m zero    n       = z≤n
m≤n⊔m (suc m) zero    = s≤s (m≤n⊔m m zero)
m≤n⊔m (suc m) (suc n) = s≤s (m≤n⊔m m n)

m⊓n≤n : ∀ m n → m ⊓ n ≤ n
m⊓n≤n zero n          = z≤n
m⊓n≤n (suc m) zero    = z≤n
m⊓n≤n (suc m) (suc n) = s≤s (m⊓n≤n m n)

⊔-upper-bound : ∀ m n o → m + n ≥ o → o ⊔ n ≤ m + n
⊔-upper-bound zero zero zero p = p
⊔-upper-bound zero zero (suc o) ()
⊔-upper-bound zero (suc n) zero p = s≤s (⊔-upper-bound zero n zero z≤n)
⊔-upper-bound zero (suc n) (suc o) p = s≤s (⊔-upper-bound zero n o (≤-pred p))
⊔-upper-bound (suc m) zero zero p = p
⊔-upper-bound (suc m) zero (suc o) p = p
⊔-upper-bound (suc m) (suc n) zero p =
    start
        suc n
    ≤⟨ s≤s (≤-step ≤-refl) ⟩
        suc (suc n)
    ≤⟨ s≤s (n≤m+n m (suc n)) ⟩
        suc (m + suc n)
    □
⊔-upper-bound (suc m) (suc n) (suc o) p =
    start
        suc (o ⊔ n)
    ≤⟨ s≤s (⊔-upper-bound (suc m) n o $
        start
            o
        ≤⟨ ≤-pred p ⟩
            m + suc n
        ≈⟨ +-suc m n ⟩
            suc (m + n)
        □
    ) ⟩
        suc (suc (m + n))
    ≈⟨ cong suc (sym (+-suc m n)) ⟩
        suc (m + suc n)
    □

m⊔n≤m+n : ∀ m n → m ⊔ n ≤ m + n
m⊔n≤m+n zero n = ≤-refl
m⊔n≤m+n (suc m) zero = s≤s (m≤m+n m zero)
m⊔n≤m+n (suc m) (suc n) = s≤s $
    start
        m ⊔ n
    ≤⟨ m⊔n≤m+n m n ⟩
        m + n
    ≤⟨ n+-mono m (n≤m+n 1 n) ⟩
        m + suc n
    □

-- double : ∀ m → m + m ≡ m * 2
-- double m =
--     begin
--         m + m
--     ≡⟨ cong (λ w → m + w) (sym (+-right-identity m)) ⟩
--         m + (m + zero)
--     ≡⟨ *-comm (suc (suc zero)) m ⟩
--         m * suc (suc zero)
--     ∎

-- cancel-∸-right-inverse : ∀ m n o → n ≥ o → m + o ≡ n → m ≡ n ∸ o
-- cancel-∸-right-inverse m n zero p eq =
--     begin
--         m
--     ≡⟨ sym (+-right-identity m) ⟩
--         m + 0
--     ≡⟨ eq ⟩
--         n
--     ∎
-- cancel-∸-right-inverse m zero (suc o) () eq
-- cancel-∸-right-inverse m (suc n) (suc o) p eq =
--     begin
--         m
--     ≡⟨ cancel-∸-right-inverse m n o (≤-pred p) $ cancel-+-left 1 $
--         begin
--             suc m + o
--         ≡⟨ sym (+-suc m o) ⟩
--             m + suc o
--         ≡⟨ eq ⟩
--             suc n
--         ∎
--      ⟩
--         n ∸ o
--     ∎

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
open import Data.List using () renaming
  ( List to ♭List ; [] to []♭ ; _∷_ to _∷♭_ ; _++_ to _++♭_
  ; length to length♭ ; map to ♭map )
open import Data.Maybe using ( Maybe ; just ; nothing )
open import Data.Nat using ( zero ; suc ) renaming ( _+_ to _+♭_ )
open import Function using () renaming ( _∘′_ to _∘_ )
open import Relation.Binary.PropositionalEquality using
  ( _≡_ ; refl ; sym ; subst ; cong ; cong₂ )

open import AssocFree.Util using ( ≡-relevant ) renaming ( lookup to lookup♭ )

open import AssocFree.DNat using ( ℕ ; ♯0 ; _+_ ; iso-resp-+ ) renaming
  ( ♭ to ♭ⁿ ; ♯ to ♯ⁿ ; iso to isoⁿ ; iso⁻¹ to isoⁿ⁻¹ )

module AssocFree.DList where

open Relation.Binary.PropositionalEquality.≡-Reasoning using ( begin_ ; _≡⟨_⟩_ ; _∎ )

infixr 4 _++_
infixl 3 _≪_
infixr 2 _≫_

cat : ∀ {A : Set} → ♭List A → ♭List A → ♭List A
cat = _++♭_

cat-assoc : ∀ {A} (as bs : ♭List A) → (cat (cat as bs) ≡ ((cat as) ∘ (cat bs)))
cat-assoc []♭       bs = refl
cat-assoc (a ∷♭ as) bs = cong (_∘_ (_∷♭_ a)) (cat-assoc as bs)

cat-unit : ∀ {A} (as : ♭List A) → cat as []♭ ≡ as
cat-unit []♭       = refl
cat-unit (a ∷♭ as) = cong (_∷♭_ a) (cat-unit as)

-- List A is isomorphic to ♭List A, but has associativity of concatenation
-- up to beta reduction, not just up to propositional equality.
-- We keep track of the length explicitly to ensure that length is a monoid
-- homomorphism up to beta-reduction, not just up to ≡.

record List (A : Set) : Set where
  constructor list
  field
    length : ℕ
    fun : ♭List A → ♭List A
    .length✓ : length ≡ ♯ⁿ (length♭ (fun []♭))
    .fun✓ : fun ≡ cat (fun []♭)

open List public

-- Convert any ♭List into a List and back

♯ : ∀ {A} → ♭List A → List A
♯ as = list
  (♯ⁿ (length♭ as))
  (cat as)
  (cong (♯ⁿ ∘ length♭) (sym (cat-unit as)))
  (cong cat (sym (cat-unit as)))

♭ : ∀ {A} → List A → ♭List A
♭ (list n f n✓ f✓) = f []♭

-- Map

map : ∀ {A B} → (A → B) → List A → List B
map f as = ♯ (♭map f (♭ as))

-- Empty list

[] : ∀ {A} → List A
[] = ♯ []♭

-- Singleton

[_] : ∀ {A} → A → List A
[ a ] = ♯ (a ∷♭ []♭)

-- Concatenation

length♭-resp-++ : ∀ {A : Set} (as bs : ♭List A) → length♭ (as ++♭ bs) ≡ (length♭ as +♭ length♭ bs)
length♭-resp-++ []♭       bs = refl
length♭-resp-++ (a ∷♭ as) bs = cong (_+♭_ 1) (length♭-resp-++ as bs)

_++_ : ∀ {A} → List A → List A → List A
list m f m✓ f✓ ++ list n g n✓ g✓ = list (m + n) (f ∘ g) m+n✓ f∘g✓ where
  .m+n✓ : (m + n) ≡ ♯ⁿ (length♭ (f (g []♭)))
  m+n✓ = begin
      m + n
    ≡⟨ cong₂ _+_ m✓ n✓ ⟩
      ♯ⁿ (length♭ (f []♭)) + ♯ⁿ (length♭ (g []♭))
    ≡⟨ sym (isoⁿ (♯ⁿ (length♭ (f []♭)) + ♯ⁿ (length♭ (g []♭)))) ⟩
      ♯ⁿ (♭ⁿ (♯ⁿ (length♭ (f []♭)) + ♯ⁿ (length♭ (g []♭))))
    ≡⟨ cong ♯ⁿ (iso-resp-+ (♯ⁿ (length♭ (f []♭))) (♯ⁿ (length♭ (g []♭)))) ⟩
      ♯ⁿ (♭ⁿ (♯ⁿ (length♭ (f []♭))) +♭ ♭ⁿ (♯ⁿ (length♭ (g []♭))))
    ≡⟨ cong ♯ⁿ (cong₂ _+♭_ (isoⁿ⁻¹ (length♭ (f []♭))) (isoⁿ⁻¹ (length♭ (g []♭)))) ⟩
      ♯ⁿ (length♭ (f []♭) +♭ length♭ (g []♭))
    ≡⟨ cong ♯ⁿ (sym (length♭-resp-++ (f []♭) (g []♭))) ⟩
      ♯ⁿ (length♭ (f []♭ ++♭ g []♭))
    ≡⟨ cong (λ X → ♯ⁿ (length♭ (X (g []♭)))) (sym f✓) ⟩
      ♯ⁿ (length♭ (f (g []♭)))
    ∎
  .f∘g✓ : (f ∘ g) ≡ cat (f (g []♭))
  f∘g✓ = begin
      f ∘ g
    ≡⟨ cong₂ _∘_ f✓ g✓ ⟩
      cat (f []♭) ∘ cat (g []♭)
    ≡⟨ sym (cat-assoc (f []♭) (g []♭)) ⟩
      cat (f []♭ ++♭ g []♭)
    ≡⟨ cong (λ X → cat (X (g []♭))) (sym f✓) ⟩
      cat (f (g []♭))
    ∎

-- Cons

_∷_ : ∀ {A} → A → List A → List A
a ∷ as = [ a ] ++ as

-- Ismorphism between List and ♭List which respects ++ and length

inject : ∀ {A} (as bs : List A) → (length as ≡ length bs) → (fun as ≡ fun bs) → (as ≡ bs)
inject (list m f m✓ f✓) (list .m .f n✓ g✓) refl refl = refl

iso : ∀ {A} (as : List A) → ♯ (♭ as) ≡ as
iso as = inject (♯ (♭ as)) as (sym (≡-relevant (length✓ as))) (sym (≡-relevant (fun✓ as)))

iso⁻¹ : ∀ {A} (as : ♭List A) → ♭ (♯ as) ≡ as
iso⁻¹ = cat-unit

iso-resp-++ : ∀ {A} (as bs : List A) → ♭ (as ++ bs) ≡ (♭ as ++♭ ♭ bs)
iso-resp-++ (list m f m✓ f✓) (list n g n✓ g✓) = cong (λ X → X (g []♭)) (≡-relevant f✓)

iso-resp-length : ∀ {A} (as : List A) → ♭ⁿ (length as) ≡ length♭ (♭ as)
iso-resp-length as =
  begin
    ♭ⁿ (length as)
  ≡⟨ cong (♭ⁿ ∘ length) (sym (iso as)) ⟩
    ♭ⁿ (♯ⁿ (length♭ (♭ as)))
  ≡⟨ isoⁿ⁻¹ (length♭ (♭ as)) ⟩
    length♭ (♭ as)
  ∎

-- Associtivity and units on the nose

++-assoc : ∀ {A} (as bs cs : List A) → ((as ++ bs) ++ cs) ≡ (as ++ (bs ++ cs))
++-assoc as bs cs = refl

++-unit₁ : ∀ {A} (as : List A) → (([] ++ as) ≡ as)
++-unit₁ as = refl

++-unit₂ : ∀ {A} (as : List A) → ((as ++ []) ≡ as)
++-unit₂ as = refl

-- Length is a monoid homomorphism on the nose

length-resp-++ : ∀ {A} (as bs : List A) → (length (as ++ bs) ≡ (length as + length bs))
length-resp-++ as bs = refl

length-resp-[] : ∀ {A} → (length {A} [] ≡ ♯0)
length-resp-[] = refl

-- Lookup

lookup : ∀ {A} → List A → ℕ → Maybe A
lookup as n = lookup♭ (♭ as) (♭ⁿ n)

lookup♭₁ : ∀ {A : Set} {a : A} as bs n →
  (lookup♭ as n ≡ just a) → (lookup♭ (as ++♭ bs) n ≡ just a)
lookup♭₁ []♭       bs n       ()
lookup♭₁ (a ∷♭ as) bs zero    refl    = refl
lookup♭₁ (a ∷♭ as) bs (suc n) as[n]≡a = lookup♭₁ as bs n as[n]≡a

lookup♭₂ : ∀ {A : Set} {a : A} as bs n →
  (lookup♭ bs n ≡ just a) → (lookup♭ (as ++♭ bs) (length♭ as +♭ n) ≡ just a)
lookup♭₂ []♭       bs n bs[n]≡a = bs[n]≡a
lookup♭₂ (a ∷♭ as) bs n bs[n]≡a = lookup♭₂ as bs n bs[n]≡a

lookup₁ : ∀ {A} {a : A} as bs n →
  (lookup as n ≡ just a) → (lookup (as ++ bs) n ≡ just a)
lookup₁ {A} {a} as bs n as[n]≡a =
  begin
    lookup♭ (♭ (as ++ bs)) (♭ⁿ n)
  ≡⟨ cong (λ X → lookup♭ X (♭ⁿ n)) (iso-resp-++ as bs) ⟩
    lookup♭ (♭ as ++♭ ♭ bs) (♭ⁿ n)
  ≡⟨ lookup♭₁ (♭ as) (♭ bs) (♭ⁿ n) as[n]≡a ⟩
    just a
  ∎

lookup₂ : ∀ {A} {a : A} as bs n →
  (lookup bs n ≡ just a) → (lookup (as ++ bs) (length as + n) ≡ just a)
lookup₂ {A} {a} as bs n bs[n]≡a =
  begin
    lookup♭ (♭ (as ++ bs)) (♭ⁿ (length as + n))
  ≡⟨ cong₂ lookup♭ (iso-resp-++ as bs) (iso-resp-+ (length as) n) ⟩
    lookup♭ (♭ as ++♭ ♭ bs) (♭ⁿ (length as) +♭ ♭ⁿ n)
  ≡⟨ cong (λ X → lookup♭ (♭ as ++♭ ♭ bs) (X +♭ ♭ⁿ n)) (iso-resp-length as) ⟩
    lookup♭ (♭ as ++♭ ♭ bs) (length♭ (♭ as) +♭ ♭ⁿ n)
  ≡⟨ lookup♭₂ (♭ as) (♭ bs) (♭ⁿ n) bs[n]≡a ⟩
    just a
  ∎

-- Membership

record _∈_ {A} (a : A) (as : List A) : Set where
  constructor _,_
  field
    index : ℕ
    .index✓ : lookup as index ≡ just a

open _∈_ public

-- Extending membership on the left and right

_≪_ : ∀ {A} {a : A} {as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
_≪_ {A} {a} {as} (n , n✓) bs = (n , lookup₁ as bs n n✓)

_≫_ : ∀ {A} {a : A} as {bs} → (a ∈ bs) → (a ∈ (as ++ bs))
_≫_ as {bs} (n , n✓) = ((length as + n) , lookup₂ as bs n n✓)

-- Membership extensions have units

≪-unit : ∀ {A} {a : A} as (a∈as : a ∈ as) →
  (a∈as ≪ []) ≡ a∈as
≪-unit as a∈as = refl

≫-unit : ∀ {A} {a : A} as (a∈as : a ∈ as) →
  ([] ≫ a∈as) ≡ a∈as
≫-unit as a∈as = refl

-- Membership extension is associative on the nose

≪-assoc : ∀ {A} {a : A} as bs cs (a∈as : a ∈ as) →
  (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
≪-assoc as bs cs a∈as = refl

≫-≪-assoc : ∀ {A} {a : A} as bs cs (a∈bs : a ∈ bs) →
  ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
≫-≪-assoc as bs cs a∈bs = refl

≫-assoc : ∀ {A} {a : A} as bs cs (a∈cs : a ∈ cs) →
  (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
≫-assoc as bs cs a∈cs = refl

-- Index is a monoid homomorphism on the nose

≪-index : ∀ {A} {a : A} as bs (a∈as : a ∈ as) →
  index (a∈as ≪ bs) ≡ index a∈as
≪-index as bs a∈as = refl

≫-index : ∀ {A} {a : A} as bs (a∈bs : a ∈ bs) →
  index (as ≫ a∈bs) ≡ (length as + index a∈bs)
≫-index as bs a∈bs = refl

-- Index is injective

index-inj : ∀ {A} (a : A) {as} (a∈as₁ a∈as₂ : a ∈ as) →
  (index a∈as₁ ≡ index a∈as₂) → (a∈as₁ ≡ a∈as₂)
index-inj a (m , m✓) (.m , n✓) refl = refl

-- Membership of empty list

absurd : ∀ {β} {A} {B : Set β} {a : A} → (a ∈ []) → B
absurd (n , ())

-- Membership of singleton

lookup-uniq : ∀ {A} {a : A} {m} {b} n → (♯ⁿ n ≡ m) →
  (lookup (b ∷ []) m ≡ just a) → (b ≡ a)
lookup-uniq zero    refl refl = refl
lookup-uniq (suc n) refl ()

uniq : ∀ {A} {a b : A} → (a ∈ [ b ]) → (b ≡ a)
uniq (n , n✓) = lookup-uniq (♭ⁿ n) (isoⁿ n) (≡-relevant n✓)

singleton : ∀ {A} (a : A) → (a ∈ [ a ])
singleton a = (♯0 , refl)

-- Case on membership

data Case {A} a (as bs : List A) : Set where
  inj₁ : (a∈as : a ∈ as) → Case a as bs
  inj₂ : (a∈bs : a ∈ bs) → Case a as bs

-- Case function

_⋙_ : ∀ {A a} as {bs cs} → Case {A} a bs cs → Case a (as ++ bs) cs
as ⋙ inj₁ a∈bs = inj₁ (as ≫ a∈bs)
as ⋙ inj₂ a∈cs = inj₂ a∈cs

lookup♭-case : ∀ {A} {a : A} cs ds n →
  .(lookup♭ (cs ++♭ ds ++♭ []♭) (n +♭ 0) ≡ just a) → (Case a (♯ cs) (♯ ds))
lookup♭-case []♭       ds n       n✓ = inj₂ (♯ⁿ n , n✓)
lookup♭-case (c ∷♭ cs) ds zero    n✓ = inj₁ (♯0 , n✓)
lookup♭-case (c ∷♭ cs) ds (suc n) n✓ = [ c ] ⋙ lookup♭-case cs ds n n✓

lookup-case : ∀ {A a as bs m} cs ds n →
  .(lookup (as ++ bs) m ≡ just a) → (♯ cs ≡ as) → (♯ ds ≡ bs) → (♯ⁿ n ≡ m) →
    Case {A} a as bs
lookup-case cs ds n n✓ refl refl refl = lookup♭-case cs ds n n✓

case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
case {A} {a} as bs (n , n✓) =
  lookup-case {A} {a} {as} {bs} {n} (♭ as) (♭ bs) (♭ⁿ n) n✓ (iso as) (iso bs) (isoⁿ n)

-- Beta for case with ≪

lookup♭-case-≪ : ∀ {A} {a : A} cs ds n .n✓₁ .n✓₂ →
  lookup♭-case {A} {a} cs ds n n✓₂ ≡ inj₁ (♯ⁿ n , n✓₁)
lookup♭-case-≪ []♭       ds n       ()  n✓₂
lookup♭-case-≪ (c ∷♭ cs) ds zero    n✓₁ n✓₂ = refl
lookup♭-case-≪ (c ∷♭ cs) ds (suc n) n✓₁ n✓₂ = cong (_⋙_ [ c ]) (lookup♭-case-≪ cs ds n n✓₁ n✓₂)

lookup-case-≪ : ∀ {A} {a : A} {as bs m} cs ds n .m✓₁ .m✓₂ cs≡as ds≡bs n≡m →
  lookup-case {A} {a} {as} {bs} {m} cs ds n m✓₂ cs≡as ds≡bs n≡m
    ≡ inj₁ (m , m✓₁)
lookup-case-≪ cs ds n m✓₁ m✓₂ refl refl refl = lookup♭-case-≪ cs ds n m✓₁ m✓₂

case-≪ : ∀ {A a as} (a∈as : a ∈ as) bs → (case {A} {a} as bs (a∈as ≪ bs) ≡ inj₁ a∈as)
case-≪ {A} {a} {as} (n , n✓) bs =
  lookup-case-≪ {A} {a} {as} {bs} {n} (♭ as) (♭ bs) (♭ⁿ n) n✓
    (lookup₁ as bs n n✓) (iso as) (iso bs) (isoⁿ n)

-- Beta for case with ≫

lookup♭-case-≫ : ∀ {A} {a : A} cs ds n₁ n₂ .n✓₁ .n✓₂ → (n₂ ≡ n₁) →
  lookup♭-case {A} {a} cs ds (length♭ cs +♭ n₂) n✓₂ ≡ inj₂ (♯ⁿ n₁ , n✓₁)
lookup♭-case-≫ []♭       ds n .n n✓₁ n✓₂ refl = refl
lookup♭-case-≫ (c ∷♭ cs) ds n .n n✓₁ n✓₂ refl = cong (_⋙_ [ c ]) (lookup♭-case-≫ cs ds n n n✓₁ n✓₂ refl)

lookup-case-≫ : ∀ {A} {a : A} {as bs m l+m} cs ds n .m✓₁ .m✓₂ cs≡as ds≡bs l+n≡l+m → (♯ⁿ n ≡ m) →
    lookup-case {A} {a} {as} {bs} {l+m} cs ds (♭ⁿ (length as + m)) m✓₂ cs≡as ds≡bs l+n≡l+m
      ≡ inj₂ (m , m✓₁)
lookup-case-≫ cs ds n m✓₁ m✓₂ refl refl refl refl =
  lookup♭-case-≫ cs ds n (n +♭ 0) m✓₁ m✓₂ (isoⁿ⁻¹ n)

case-≫ : ∀ {A a} as {bs} (a∈bs : a ∈ bs) → (case {A} {a} as bs (as ≫ a∈bs) ≡ inj₂ a∈bs)
case-≫ {A} {a} as {bs} (n , n✓) =
  lookup-case-≫ {A} {a} {as} {bs} {n} {length as + n} (♭ as) (♭ bs) (♭ⁿ n) n✓
    (lookup₂ as bs n n✓) (iso as) (iso bs) (isoⁿ (length as + n)) (isoⁿ n)

-- A variant of case which remembers its argument

data Case+ {A} {a} (as bs : List A) : (a ∈ (as ++ bs)) → Set where
  inj₁ : (a∈as : a ∈ as) → Case+ as bs (a∈as ≪ bs)
  inj₂ : (a∈bs : a ∈ bs) → Case+ as bs (as ≫ a∈bs)

_⋙+_ : ∀ {A a} as {bs cs} {a∈bs++cs} →
  Case+ {A} {a} bs cs a∈bs++cs → Case+ (as ++ bs) cs (as ≫ a∈bs++cs)
as ⋙+ inj₁ a∈bs = inj₁ (as ≫ a∈bs)
as ⋙+ inj₂ a∈cs = inj₂ a∈cs

lookup♭-case+ : ∀ {A a} cs ds n .n✓ → (Case+ {A} {a} (♯ cs) (♯ ds) (♯ⁿ n , n✓))
lookup♭-case+ []♭       ds n       n✓ = inj₂ (♯ⁿ n , n✓)
lookup♭-case+ (c ∷♭ cs) ds zero    n✓ = inj₁ (♯0 , n✓)
lookup♭-case+ (c ∷♭ cs) ds (suc n) n✓ = [ c ] ⋙+ lookup♭-case+ cs ds n n✓

lookup-case+ : ∀ {A a as bs m} cs ds n .m✓ → (♯ cs ≡ as) → (♯ ds ≡ bs) → (♯ⁿ n ≡ m) →
  Case+ {A} {a} as bs (m , m✓)
lookup-case+ cs ds n n✓ refl refl refl = lookup♭-case+ cs ds n n✓

case+ : ∀ {A a} as bs a∈as++bs → Case+ {A} {a} as bs a∈as++bs
case+ {A} {a} as bs (n , n✓) =
  lookup-case+ {A} {a} {as} {bs} {n} (♭ as) (♭ bs) (♭ⁿ n) n✓ (iso as) (iso bs) (isoⁿ n)

-- Inverse of case

case⁻¹ : ∀ {A a as bs} → Case {A} a as bs → (a ∈ (as ++ bs))
case⁻¹ {A} {a} {as} {bs} (inj₁ a∈as) = (a∈as ≪ bs)
case⁻¹ {A} {a} {as} {bs} (inj₂ a∈bs) = (as ≫ a∈bs)

case-iso : ∀ {A a} as bs (a∈as++bs : a ∈ (as ++ bs)) →
  case⁻¹ (case {A} {a} as bs a∈as++bs) ≡ a∈as++bs
case-iso as bs a∈as++bs     with case+ as bs a∈as++bs
case-iso as bs .(a∈as ≪ bs) | inj₁ a∈as = cong case⁻¹ (case-≪ a∈as bs)
case-iso as bs .(as ≫ a∈bs) | inj₂ a∈bs = cong case⁻¹ (case-≫ as a∈bs)

case-iso⁻¹ : ∀ {A a} as bs (a∈as++bs : Case a as bs) →
  case {A} {a} as bs (case⁻¹ a∈as++bs) ≡ a∈as++bs
case-iso⁻¹ as bs (inj₁ a∈as) = case-≪ a∈as bs
case-iso⁻¹ as bs (inj₂ a∈bs) = case-≫ as a∈bs

-- ⋙ distributes through case

case-⋙ : ∀ {A} {a : A} as bs cs (a∈bs++cs : a ∈ (bs ++ cs)) →
  (as ⋙ case bs cs a∈bs++cs) ≡ (case (as ++ bs) cs (as ≫ a∈bs++cs))
case-⋙ as bs cs a∈bs++cs with case+ bs cs a∈bs++cs
case-⋙ as bs cs .(a∈bs ≪ cs) | inj₁ a∈bs =
  begin
    as ⋙ case bs cs (a∈bs ≪ cs)
  ≡⟨ cong (_⋙_ as) (case-≪ a∈bs cs) ⟩
    inj₁ (as ≫ a∈bs)
  ≡⟨ sym (case-≪ (as ≫ a∈bs) cs) ⟩
    case (as ++ bs) cs (as ≫ a∈bs ≪ cs)
  ∎
case-⋙ as bs cs .(bs ≫ a∈cs) | inj₂ a∈cs =
  begin
    as ⋙ case bs cs (bs ≫ a∈cs)
  ≡⟨ cong (_⋙_ as) (case-≫ bs a∈cs) ⟩
    inj₂ a∈cs
  ≡⟨ sym (case-≫ (as ++ bs) a∈cs) ⟩
    case (as ++ bs) cs (as ≫ bs ≫ a∈cs)
  ∎

-- Three-way case, used for proving associativity properties

data Case₃ {A} (a : A) as bs cs : Set where
  inj₁ : (a ∈ as) → Case₃ a as bs cs
  inj₂ : (a ∈ bs) → Case₃ a as bs cs
  inj₃ : (a ∈ cs) → Case₃ a as bs cs

case₂₃ : ∀ {A} {a : A} as bs cs → (Case a bs cs) → (Case₃ a as bs cs)
case₂₃ as bs cs (inj₁ a∈bs) = inj₂ a∈bs
case₂₃ as bs cs (inj₂ a∈cs) = inj₃ a∈cs

case₁₃ : ∀ {A} {a : A} as bs cs → (Case a as (bs ++ cs)) → (Case₃ a as bs cs)
case₁₃ as bs cs (inj₁ a∈as)     = inj₁ a∈as
case₁₃ as bs cs (inj₂ a∈bs++cs) = case₂₃ as bs cs (case bs cs a∈bs++cs)

case₃ : ∀ {A} {a : A} as bs cs → (a ∈ (as ++ bs ++ cs)) → (Case₃ a as bs cs)
case₃ as bs cs a∈as++bs++cs = case₁₃ as bs cs (case as (bs ++ cs) a∈as++bs++cs)

-- Associating case₃ to the left gives case

caseˡ : ∀ {A} {a : A} {as bs cs} → Case₃ a as bs cs → Case a (as ++ bs) cs
caseˡ {bs = bs} (inj₁ a∈as) = inj₁ (a∈as ≪ bs)
caseˡ {as = as} (inj₂ a∈bs) = inj₁ (as ≫ a∈bs)
caseˡ           (inj₃ a∈cs) = inj₂ a∈cs

caseˡ₂₃ : ∀ {A a} as bs cs {a∈bs++cs} → Case+ {A} {a} bs cs a∈bs++cs →
  caseˡ (case₂₃ as bs cs (case bs cs a∈bs++cs)) ≡ case (as ++ bs) cs (as ≫ a∈bs++cs)
caseˡ₂₃ as bs cs (inj₁ a∈bs) =
  begin
    caseˡ (case₂₃ as bs cs (case bs cs (a∈bs ≪ cs)))
  ≡⟨ cong (caseˡ ∘ case₂₃ as bs cs) (case-≪ a∈bs cs) ⟩
    inj₁ (as ≫ a∈bs)
  ≡⟨ sym (case-≪ (as ≫ a∈bs) cs) ⟩
    case (as ++ bs) cs (as ≫ a∈bs ≪ cs)
  ∎
caseˡ₂₃ as bs cs (inj₂ a∈cs) =
  begin
    caseˡ (case₂₃ as bs cs (case bs cs (bs ≫ a∈cs)))
  ≡⟨ cong (caseˡ ∘ case₂₃ as bs cs) (case-≫ bs a∈cs) ⟩
    inj₂ a∈cs
  ≡⟨ sym (case-≫ (as ++ bs) a∈cs) ⟩
    case (as ++ bs) cs (as ≫ bs ≫ a∈cs)
  ∎

caseˡ₁₃ : ∀ {A a} as bs cs {a∈as++bs++cs} → Case+ {A} {a} as (bs ++ cs) a∈as++bs++cs →
  caseˡ (case₁₃ as bs cs (case as (bs ++ cs) a∈as++bs++cs)) ≡ case (as ++ bs) cs a∈as++bs++cs
caseˡ₁₃ as bs cs (inj₁ a∈as) =
  begin
    caseˡ (case₁₃ as bs cs (case as (bs ++ cs) (a∈as ≪ bs ≪ cs)))
  ≡⟨ cong (caseˡ ∘ case₁₃ as bs cs) (case-≪ a∈as (bs ++ cs)) ⟩
    inj₁ (a∈as ≪ bs)
  ≡⟨ sym (case-≪ (a∈as ≪ bs) cs) ⟩
    case (as ++ bs) cs (a∈as ≪ bs ≪ cs)
  ∎
caseˡ₁₃ as bs cs (inj₂ a∈bs++cs) =
  begin
    caseˡ (case₁₃ as bs cs (case as (bs ++ cs) (as ≫ a∈bs++cs)))
  ≡⟨ cong (caseˡ ∘ case₁₃ as bs cs) (case-≫ as a∈bs++cs) ⟩
    caseˡ (case₂₃ as bs cs (case bs cs a∈bs++cs))
  ≡⟨ caseˡ₂₃ as bs cs (case+ bs cs a∈bs++cs) ⟩
    case (as ++ bs) cs (as ≫ a∈bs++cs)
  ∎

caseˡ₃ : ∀ {A} {a : A} as bs cs (a∈as++bs++cs : a ∈ (as ++ bs ++ cs)) →
  caseˡ (case₃ as bs cs a∈as++bs++cs) ≡ case (as ++ bs) cs a∈as++bs++cs
caseˡ₃ as bs cs a∈as++bs++cs = caseˡ₁₃ as bs cs (case+ as (bs ++ cs) a∈as++bs++cs)

-- Associating case₃ to the right gives case

caseʳ : ∀ {A} {a : A} {as bs cs} → Case₃ a as bs cs → Case a as (bs ++ cs)
caseʳ           (inj₁ a∈as) = inj₁ a∈as
caseʳ {cs = cs} (inj₂ a∈bs) = inj₂ (a∈bs ≪ cs)
caseʳ {bs = bs} (inj₃ a∈cs) = inj₂ (bs ≫ a∈cs)

caseʳ₂₃ : ∀ {A a} as bs cs {a∈bs++cs} → Case+ {A} {a} bs cs a∈bs++cs →
  caseʳ (case₂₃ as bs cs (case bs cs a∈bs++cs)) ≡ inj₂ a∈bs++cs
caseʳ₂₃ as bs cs (inj₁ a∈bs) = cong (caseʳ ∘ case₂₃ as bs cs) (case-≪ a∈bs cs)
caseʳ₂₃ as bs cs (inj₂ a∈cs) = cong (caseʳ ∘ case₂₃ as bs cs) (case-≫ bs a∈cs)

caseʳ₁₃ : ∀ {A a} as bs cs {a∈as++bs++cs} → Case+ {A} {a} as (bs ++ cs) a∈as++bs++cs →
  caseʳ (case₁₃ as bs cs (case as (bs ++ cs) a∈as++bs++cs)) ≡ case as (bs ++ cs) a∈as++bs++cs
caseʳ₁₃ as bs cs (inj₁ a∈as) =
  begin
    caseʳ (case₁₃ as bs cs (case as (bs ++ cs) (a∈as ≪ bs ≪ cs)))
  ≡⟨ cong (caseʳ ∘ case₁₃ as bs cs) (case-≪ a∈as (bs ++ cs)) ⟩
    inj₁ a∈as
  ≡⟨ sym (case-≪ a∈as (bs ++ cs)) ⟩
    case as (bs ++ cs) (a∈as ≪ bs ≪ cs)
  ∎
caseʳ₁₃ as bs cs (inj₂ a∈bs++cs) =
  begin
    caseʳ (case₁₃ as bs cs (case as (bs ++ cs) (as ≫ a∈bs++cs)))
  ≡⟨ cong (caseʳ ∘ case₁₃ as bs cs) (case-≫ as a∈bs++cs) ⟩
    caseʳ (case₂₃ as bs cs (case bs cs a∈bs++cs))
  ≡⟨ caseʳ₂₃ as bs cs (case+ bs cs a∈bs++cs) ⟩
    inj₂ a∈bs++cs
  ≡⟨ sym (case-≫ as a∈bs++cs) ⟩
    case as (bs ++ cs) (as ≫ a∈bs++cs)
  ∎

caseʳ₃ : ∀ {A} {a : A} as bs cs (a∈as++bs++cs : a ∈ (as ++ bs ++ cs)) →
  caseʳ (case₃ as bs cs a∈as++bs++cs) ≡ case as (bs ++ cs) a∈as++bs++cs
caseʳ₃ as bs cs a∈as++bs++cs = caseʳ₁₃ as bs cs (case+ as (bs ++ cs) a∈as++bs++cs)

max_stars_repo_name: agda/agda-assoc-free

max_issues_repo_name: agda/agda-assoc-free

max_forks_repo_name: agda/agda-assoc-free


text:
-- Andreas, 2012-02-14. No short-circuit conversion test for sizes!
{-# OPTIONS --sized-types --show-implicit #-}
-- {-# OPTIONS -v tc.size.solve:20 -v tc.conv.size:20 -v tc.term.con:50 -v tc.term.args:50 #-}

module Issue298b where

open import Common.Size

data BTree : {size : Size} → Set where
  leaf : {i : Size} → BTree {↑ i}
  node : {i : Size} → BTree {i} → BTree {i} → BTree {↑ i}

works : ∀ {i} → BTree {i} → BTree
works (node (node t1 t2) t3) = node (works t1) (node t2 t3)
works t = t

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda