text:
------------------------------------------------------------------------
-- Squashing
------------------------------------------------------------------------

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

import Equality.Path as P

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

open P.Derived-definitions-and-properties eq

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

open import Bijection equality-with-J using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Double-negation equality-with-J as DN using (¬¬_)
open import Embedding equality-with-J using (Embedding; Is-embedding)
open import Equality.Decision-procedures equality-with-J
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Erased equality-with-J using (_≃ᴱ_)
open import For-iterated-equality equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as Trunc using (∥_∥)
open import Injection equality-with-J using (_↣_)
open import Monad equality-with-J
open import Surjection equality-with-J using (_↠_; Split-surjective)

private
  variable
    a b ℓ p : Level
    A B     : Type a
    P       : A → Type p
    k x y   : A
    n       : ℕ

------------------------------------------------------------------------
-- The squash type

-- Any two elements of type Squash′ A are definitionally equal.

data Squash′ (A : Type a) : Prop a where
  squash′ : A → Squash′ A

-- However, Squash′ A does not have type Type a. The following wrapper
-- makes it possible to use squashed types in, say, lists.

record Squash (A : Type a) : Type a where
  constructor squash
  field
    squashed : Squash′ A

pattern [_] x = squash (squash′ x)

private

  -- A unit test.

  test : [ 4 ] ∷ [ 5 ] ∷ [] ≡ [ 3 ] ∷ [ 9 ] ∷ []
  test = refl _

-- Squashed types are propositions.

Squash-propositional : Is-proposition (Squash A)
Squash-propositional = λ _ _ → refl _

------------------------------------------------------------------------
-- Squash is a monad

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : Squash A → (A → Squash B) → Squash B
_>>=′_ {A = A} {B = B} (squash x) f = squash (lemma x)
  where
  lemma : Squash′ A → Squash′ B
  lemma (squash′ x) = Squash.squashed (f x)

instance

  -- Squash is a monad.

  raw-monad : Raw-monad {c = ℓ} Squash
  Raw-monad.return raw-monad = [_]
  Raw-monad._>>=_  raw-monad = _>>=′_

  monad : Monad {c = ℓ} Squash
  Monad.raw-monad      monad = raw-monad
  Monad.left-identity  monad = λ _ _ → refl _
  Monad.right-identity monad = λ _ → refl _
  Monad.associativity  monad = λ _ _ _ → refl _

------------------------------------------------------------------------
-- Squash preserves all kinds of functions

private

  -- Squash preserves functions.

  Squash-cong-→ : (A → B) → Squash A → Squash B
  Squash-cong-→ A→B x = x >>=′ return ∘ A→B

-- If A and B are logically equivalent, then Squash A and Squash B are
-- equivalent.

Squash-cong-⇔ : A ⇔ B → Squash A ≃ Squash B
Squash-cong-⇔ A⇔B = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = Squash-cong-→ (_⇔_.to   A⇔B)
      ; from = Squash-cong-→ (_⇔_.from A⇔B)
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = λ _ → refl _
  })

-- If there is a split surjection from A to B, then Squash A and
-- Squash B are equivalent.

Squash-cong-↠ : A ↠ B → Squash A ≃ Squash B
Squash-cong-↠ = Squash-cong-⇔ ∘ _↠_.logical-equivalence

private

  -- Some lemmas used in Squash-cong.

  Squash-cong-↔ : A ↔ B → Squash A ↔ Squash B
  Squash-cong-↔ =
    from-isomorphism ∘ Squash-cong-⇔ ∘ _↔_.logical-equivalence

  Squash-cong-≃ : A ≃ B → Squash A ≃ Squash B
  Squash-cong-≃ = Squash-cong-⇔ ∘ _≃_.logical-equivalence

  Squash-cong-≃ᴱ : A ≃ᴱ B → Squash A ≃ᴱ Squash B
  Squash-cong-≃ᴱ =
    from-isomorphism ∘ Squash-cong-⇔ ∘ _≃ᴱ_.logical-equivalence

  Squash-cong-↣ : A ↣ B → Squash A ↣ Squash B
  Squash-cong-↣ A↣B = record
    { to        = Squash-cong-→ (_↣_.to A↣B)
    ; injective = λ _ → refl _
    }

  Squash-cong-Embedding :
    Embedding A B → Embedding (Squash A) (Squash B)
  Squash-cong-Embedding A↣B = record
    { to           = Squash-cong-→ (Embedding.to A↣B)
    ; is-embedding = λ x y →
        _≃_.is-equivalence $
        _↠_.from (Eq.≃↠⇔ (⇒≡ 1 Squash-propositional)
                         (⇒≡ 1 Squash-propositional))
          (record { from = λ _ → refl _ })
    }

Squash-cong : A ↝[ k ] B → Squash A ↝[ k ] Squash B
Squash-cong {k = implication}         = Squash-cong-→
Squash-cong {k = logical-equivalence} = from-isomorphism ∘ Squash-cong-⇔
Squash-cong {k = injection}           = Squash-cong-↣
Squash-cong {k = embedding}           = Squash-cong-Embedding
Squash-cong {k = surjection}          = from-isomorphism ∘ Squash-cong-↠
Squash-cong {k = bijection}           = Squash-cong-↔
Squash-cong {k = equivalence}         = Squash-cong-≃
Squash-cong {k = equivalenceᴱ}        = Squash-cong-≃ᴱ

------------------------------------------------------------------------
-- Some isomorphisms

-- Squash ⊤ is isomorphic to ⊤.

Squash-⊤↔⊤ : Squash ⊤ ↔ ⊤
Squash-⊤↔⊤ = record
  { surjection = record
    { logical-equivalence = record
      { from = λ _ → [ _ ]
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = λ _ → refl _
  }

-- Squash ⊥ is isomorphic to ⊥.

Squash-⊥↔⊥ : Squash (⊥ {ℓ = ℓ}) ↔ ⊥ {ℓ = ℓ}
Squash-⊥↔⊥ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ x → ⊥-in-prop→⊥ (Squash-⊥→⊥-in-prop x)
      ; from = λ ()
      }
    ; right-inverse-of = λ ()
    }
  ; left-inverse-of = λ _ → refl _
  }
  where

  -- An empty type in Prop.

  data ⊥-in-prop : Prop where

  -- Squash ⊥ implies ⊥-in-prop.

  Squash-⊥→⊥-in-prop : Squash (⊥ {ℓ = ℓ}) → ⊥-in-prop
  Squash-⊥→⊥-in-prop [ () ]

  -- ⊥-in-prop implies ⊥.

  ⊥-in-prop→⊥ : ⊥-in-prop → ⊥ {ℓ = ℓ}
  ⊥-in-prop→⊥ ()

-- Squash commutes with _×_.
--
-- This lemma was suggested by Jesper Cockx.

Squash-×↔× : Squash (A × B) ↔ Squash A × Squash B
Squash-×↔× = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ p → Squash-cong proj₁ p , Squash-cong proj₂ p
      ; from = λ (x , y) → x >>=′ λ x → y >>=′ λ y → return (x , y)
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Squash commutes with ↑ ℓ.

Squash-↑↔↑ : Squash (↑ ℓ A) ↔ ↑ ℓ (Squash A)
Squash-↑↔↑ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { x .lower → Squash-cong lower x }
      ; from = λ (lift x) → Squash-cong lift x
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = λ _ → refl _
  }

------------------------------------------------------------------------
-- Some properties

-- ∥ A ∥ implies Squash A.

∥∥→Squash : ∥ A ∥ → Squash A
∥∥→Squash = Trunc.rec Squash-propositional [_]

-- Squash A implies ¬ ¬ A.

Squash→¬¬ : Squash A → ¬ ¬ A
Squash→¬¬ {A = A} = curry (
  Squash A × ¬ A  ↝⟨ uncurry (flip Squash-cong) ⟩
  Squash ⊥        ↔⟨ Squash-⊥↔⊥ ⟩□
  ⊥               □)

-- It is not in general the case that [ x ] ≡ [ y ] implies
-- Squash (x ≡ y).

¬-[]≡[]→Squash-≡ :
  ¬ ({A : Type a} {x y : A} → [ x ] ≡ [ y ] → Squash (x ≡ y))
¬-[]≡[]→Squash-≡ {a = a} =
  ({A : Type a} {x y : A} → [ x ] ≡ [ y ] → Squash (x ≡ y))  ↝⟨ _$ refl _ ⟩
  Squash (lift true ≡ lift false)                            ↝⟨ Squash-cong (cong lower) ⟩
  Squash (true ≡ false)                                      ↝⟨ Squash-cong Bool.true≢false ⟩
  Squash ⊥                                                   ↔⟨ Squash-⊥↔⊥ ⟩□
  ⊥                                                          □

-- [_] is split surjective for decided types.

Split-surjective-[] : Dec A → Split-surjective {A = A} [_]
Split-surjective-[] (yes x) _ = x , refl _
Split-surjective-[] (no ¬x) x =
  ⊥-elim (_↔_.to Squash-⊥↔⊥ (Squash-cong ¬x x))

------------------------------------------------------------------------
-- Stability

-- A type A is stable if Squash A implies A.

Stable : Type a → Type a
Stable A = Squash A → A

-- A type A is very stable if Squash A is equivalent to A.

Very-stable : Type a → Type a
Very-stable A = Squash A ≃ A

-- Variants of the definitions above for equality.

Stable-≡ : Type a → Type a
Stable-≡ = For-iterated-equality 1 Stable

Very-stable-≡ : Type a → Type a
Very-stable-≡ = For-iterated-equality 1 Very-stable

------------------------------------------------------------------------
-- Some lemmas related to stability

-- Very stable types are stable.

Very-stable→Stable :
  ∀ n →
  For-iterated-equality n Very-stable A →
  For-iterated-equality n Stable A
Very-stable→Stable n =
  For-iterated-equality-cong₁ _ n _≃_.to

-- Very-stable is propositional (assuming extensionality).

Very-stable-propositional :
  {A : Type a} →
  Extensionality a a →
  Is-proposition (Very-stable A)
Very-stable-propositional ext =
  Eq.left-closure ext 0 Squash-propositional

private

  -- The previous result can be generalised.

  For-iterated-equality-Very-stable-propositional :
    {A : Type a} →
    Extensionality a a →
    ∀ n → Is-proposition (For-iterated-equality n Very-stable A)
  For-iterated-equality-Very-stable-propositional ext n =
    H-level-For-iterated-equality ext 1 n
      (Very-stable-propositional ext)

-- A type is very stable if and only if [_] is an equivalence for that
-- type.

Very-stable↔Is-equivalence-[] :
  {A : Type a} →
  Very-stable A ↝[ a ∣ a ] Is-equivalence {A = A} [_]
Very-stable↔Is-equivalence-[] =
  generalise-ext?-prop
    (record { from = inverse ∘ Eq.⟨ _ ,_⟩
            ; to   = λ s →
                _≃_.is-equivalence $
                Eq.with-other-function
                  (inverse s)
                  [_]
                  (λ _ → refl _)
            })
    Very-stable-propositional
    (λ ext → Eq.propositional ext _)

-- A type is very stable if and only if it is a stable proposition.

Very-stable↔Stable×Is-proposition :
  {A : Type a} →
  Very-stable A ↝[ a ∣ a ] Stable A × Is-proposition A
Very-stable↔Stable×Is-proposition =
  generalise-ext?-prop
    (record { to   = λ s → _≃_.to s
                         , H-level-cong _ 1 s Squash-propositional
            ; from = λ (s , prop) →
                _↠_.from (Eq.≃↠⇔ Squash-propositional prop)
                  (record { to = s; from = [_] })
            })
    Very-stable-propositional
    (λ ext →
       [inhabited⇒+]⇒+ 0 λ (_ , prop) →
       ×-closure 1
         (Π-closure ext 1 (λ _ → prop))
         (H-level-propositional ext 1))

-- If A has h-level 1 + n and is stable "n levels up", then A is very
-- stable "n levels up".

Stable→H-level-suc→Very-stable :
  ∀ n →
  For-iterated-equality n Stable A → H-level (suc n) A →
  For-iterated-equality n Very-stable A
Stable→H-level-suc→Very-stable {A = A} n = curry (
  For-iterated-equality n Stable A × H-level (suc n) A            ↝⟨ (∃-cong λ _ → lemma) ⟩

  For-iterated-equality n Stable A ×
  For-iterated-equality n Is-proposition A                        ↝⟨ For-iterated-equality-commutes-× n _ ⟩

  For-iterated-equality n (λ A → Stable A × Is-proposition A) A   ↝⟨ For-iterated-equality-cong₁ _ n $
                                                                     uncurry (curry $ _⇔_.from (Very-stable↔Stable×Is-proposition _)) ⟩
  For-iterated-equality n Very-stable A                           □)
  where
  lemma =
    H-level (suc n) A                         ↝⟨ _⇔_.to H-level⇔H-level′ ⟩
    H-level′ (suc n) A                        ↝⟨ inverse-ext? (For-iterated-equality-For-iterated-equality n 1) _ ⟩
    For-iterated-equality n (H-level′ 1) A    ↝⟨ For-iterated-equality-cong₁ _ n $
                                                 _⇔_.from (H-level⇔H-level′ {n = 1}) ⟩□
    For-iterated-equality n Is-proposition A  □

-- Types with h-level n are very stable "n levels up".

H-level→Very-stable :
  ∀ n → H-level n A → For-iterated-equality n Very-stable A
H-level→Very-stable {A = A} n =
  H-level n A                            ↝⟨ _⇔_.to H-level⇔H-level′ ⟩
  H-level′ n A                           ↝⟨ For-iterated-equality-cong₁ _ n Contractible→Very-stable ⟩□
  For-iterated-equality n Very-stable A  □
  where
  Contractible→Very-stable :
    ∀ {A} → Contractible A → Very-stable A
  Contractible→Very-stable c =
    _⇔_.from (Very-stable↔Stable×Is-proposition _)
      ( (λ _ → proj₁ c)
      , mono₁ 0 c
      )

-- If A is very stable, then [_] {A = A} is an embedding.

Very-stable→Is-embedding-[] :
  Very-stable A → Is-embedding {A = A} [_]
Very-stable→Is-embedding-[] s x y =
  _≃_.is-equivalence (
    x ≡ y          ↝⟨ inverse $ Eq.≃-≡ $ Eq.⟨ _ , Very-stable↔Is-equivalence-[] _ s ⟩ ⟩□
    [ x ] ≡ [ y ]  □)

-- If A is very stable, then [_] {A = A} is split surjective.

Very-stable→Split-surjective-[] :
  Very-stable A → Split-surjective {A = A} [_]
Very-stable→Split-surjective-[] {A = A} =
  Very-stable A         ↝⟨ Very-stable↔Is-equivalence-[] _ ⟩
  Is-equivalence [_]    ↝⟨ (λ hyp → _↠_.split-surjective $ _≃_.surjection $ Eq.⟨ _ , hyp ⟩) ⟩
  Split-surjective [_]  □

-- Types that are stable for double negation are stable for Squash.

¬¬-Stable→Stable : (¬ ¬ A → A) → Stable A
¬¬-Stable→Stable ¬¬-Stable x = ¬¬-Stable (Squash→¬¬ x)

-- Types for which it is known whether or not they are inhabited are
-- stable.

Dec→Stable : Dec A → Stable A
Dec→Stable (yes x) _ = x
Dec→Stable (no ¬x) x with () ← Squash→¬¬ x ¬x

-- Every type is stable in the double negation monad.

¬¬-Stable : ¬¬ Stable A
¬¬-Stable = DN.map′ Dec→Stable DN.excluded-middle

-- Bool is not very stable. (But it is stable, see Dec→Stable above.)

¬-Very-stable-Bool : ¬ Very-stable Bool
¬-Very-stable-Bool =
  Very-stable Bool     ↝⟨ proj₂ ∘ Very-stable↔Stable×Is-proposition _ ⟩
  Is-proposition Bool  ↝⟨ ¬-Bool-propositional ⟩□
  ⊥                    □

-- If equality is decidable for A, then equality is very stable for A.

Decidable-equality→Very-stable-≡ :
  Decidable-equality A → Very-stable-≡ A
Decidable-equality→Very-stable-≡ dec _ _ =
  _⇔_.from (Very-stable↔Stable×Is-proposition _)
    ( Dec→Stable (dec _ _)
    , decidable⇒set dec
    )

----------------------------------------------------------------------
-- Preservation lemmas

-- Stable preserves some kinds of functions (those that are
-- "symmetric"), possibly assuming extensionality.

Stable-cong :
  {A : Type a} {B : Type b} →
  Extensionality? ⌊ k ⌋-sym (a ⊔ b) (a ⊔ b) →
  A ↝[ ⌊ k ⌋-sym ] B → Stable A ↝[ ⌊ k ⌋-sym ] Stable B
Stable-cong {k = k} {A = A} {B = B} ext A↝B =
  Stable A        ↔⟨⟩
  (Squash A → A)  ↝⟨ →-cong ext (Squash-cong A↝B) A↝B ⟩
  (Squash B → B)  ↔⟨⟩
  Stable B        □

-- A kind of map function for Stable.

Stable-map : A ⇔ B → Stable A → Stable B
Stable-map = _⇔_.to ∘ Stable-cong _

-- A kind of map function for Very-stable.

Very-stable-map :
  A ↠ B → Very-stable A → Very-stable B
Very-stable-map {A = A} {B = B} A↠B s =
  _↠_.from (Eq.≃↠⇔ Squash-propositional B-prop)
    (record { from = [_]
            ; to   = Squash B  ↝⟨ Squash-cong (_↠_.from A↠B) ⟩
                     Squash A  ↔⟨ s ⟩
                     A         ↝⟨ _↠_.to A↠B ⟩□
                     B         □
            })
  where
  A-prop : Is-proposition A
  A-prop = proj₂ $ Very-stable↔Stable×Is-proposition _ s

  B-prop : Is-proposition B
  B-prop = H-level.respects-surjection A↠B 1 A-prop

-- Very-stable preserves equivalences (assuming extensionality).

Very-stable-cong :
  {A : Type a} {B : Type b} →
  Extensionality? k (a ⊔ b) (a ⊔ b) →
  A ≃ B → Very-stable A ↝[ k ] Very-stable B
Very-stable-cong {A = A} {B = B} ext A≃B =
  Very-stable A  ↔⟨⟩
  Squash A ≃ A   ↝⟨ generalise-ext?
                      (Eq.≃-preserves-⇔ (Squash-cong A≃B) A≃B)
                      (λ ext →
                         let eq = Eq.≃-preserves ext (Squash-cong-≃ A≃B) A≃B in
                         _≃_.right-inverse-of eq , _≃_.left-inverse-of eq)
                      ext ⟩
  Squash B ≃ B   ↔⟨⟩
  Very-stable B  □

------------------------------------------------------------------------
-- Closure properties

-- Squash A is very stable.

Very-stable-Squash : Very-stable (Squash A)
Very-stable-Squash =
  _⇔_.from (Very-stable↔Stable×Is-proposition _)
    ( _>>= id
    , Squash-propositional
    )

-- ⊤ is very stable.

Very-stable-⊤ : Very-stable ⊤
Very-stable-⊤ = Eq.↔⇒≃ Squash-⊤↔⊤

-- ⊥ is very stable.

Very-stable-⊥ : Very-stable (⊥ {ℓ = ℓ})
Very-stable-⊥ = Eq.↔⇒≃ Squash-⊥↔⊥

-- Stable is closed under Π A.

Stable-Π :
  (∀ x → Stable (P x)) →
  Stable ((x : A) → P x)
Stable-Π {P = P} s =
  Squash (∀ x → P x)    ↝⟨ (λ s x → Squash-cong (_$ x) s) ⟩
  (∀ x → Squash (P x))  ↝⟨ ∀-cong _ s ⟩□
  (∀ x → P x)           □

-- Very-stable is closed under Π A (assuming extensionality).

Very-stable-Π :
  {A : Type a} {P : A → Type p} →
  Extensionality a p →
  (∀ x → Very-stable (P x)) →
  Very-stable ((x : A) → P x)
Very-stable-Π {P = P} ext s =
  _⇔_.from (Very-stable↔Stable×Is-proposition _)
    ( Stable-Π (Very-stable→Stable 0 ∘ s)
    , (Π-closure ext 1 λ x →
       H-level-cong _ 1 (s x) Squash-propositional)
    )

-- Stable is closed under _×_.

Stable-× : Stable A → Stable B → Stable (A × B)
Stable-× {A = A} {B = B} s₁ s₂ =
  Squash (A × B)       ↔⟨ Squash-×↔× ⟩
  Squash A × Squash B  ↝⟨ s₁ ×-cong s₂ ⟩□
  A × B                □

-- Very-stable is closed under _×_.

Very-stable-× : Very-stable A → Very-stable B → Very-stable (A × B)
Very-stable-× s₁ s₂ =
  _⇔_.from (Very-stable↔Stable×Is-proposition _)
    ( Stable-× (Very-stable→Stable 0 s₁) (Very-stable→Stable 0 s₂)
    , ×-closure 1 (H-level-cong _ 1 s₁ Squash-propositional)
                  (H-level-cong _ 1 s₂ Squash-propositional)
    )

-- Stable is closed under ↑ ℓ.

Stable-↑ : Stable A → Stable (↑ ℓ A)
Stable-↑ {A = A} s =
  Squash (↑ _ A)  ↔⟨ Squash-↑↔↑ ⟩
  ↑ _ (Squash A)  ↝⟨ ↑-cong s ⟩□
  ↑ _ A           □

-- Very-stable is closed under ↑ ℓ.

Very-stable-↑ : Very-stable A → Very-stable (↑ ℓ A)
Very-stable-↑ {A = A} s =
  Squash (↑ _ A)  ↔⟨ Squash-↑↔↑ ⟩
  ↑ _ (Squash A)  ↝⟨ ↑-cong s ⟩□
  ↑ _ A           □

-- If A is very stable, then equality is very stable for A.

Very-stable→Very-stable-≡ :
  ∀ n →
  For-iterated-equality n       Very-stable A →
  For-iterated-equality (suc n) Very-stable A
Very-stable→Very-stable-≡ {A = A} n =
  For-iterated-equality n Very-stable A        ↝⟨ For-iterated-equality-cong₁ _ n lemma ⟩
  For-iterated-equality n Very-stable-≡ A      ↝⟨ For-iterated-equality-For-iterated-equality n 1 _ ⟩□
  For-iterated-equality (suc n) Very-stable A  □
  where
  lemma : ∀ {A} → Very-stable A → Very-stable-≡ A
  lemma {A = A} s x y =
    _⇔_.from (Very-stable↔Stable×Is-proposition _)
      ( (Squash (x ≡ y)        ↝⟨ const prop ⟩
         Is-proposition A      ↝⟨ +⇒≡ ⟩
         Contractible (x ≡ y)  ↝⟨ proj₁ ⟩□
         x ≡ y                 □)
      , ⇒≡ 1 prop
      )
    where
    prop : Is-proposition A
    prop = proj₂ $ _⇔_.to (Very-stable↔Stable×Is-proposition _) s

private

  -- Some examples showing how Very-stable→Very-stable-≡ can be
  -- used.

  -- Equalities between erased values are very stable.

  Very-stable-≡₀ : Very-stable-≡ (Squash A)
  Very-stable-≡₀ = Very-stable→Very-stable-≡ 0 Very-stable-Squash

  -- Equalities between equalities between erased values are very
  -- stable.

  Very-stable-≡₁ : For-iterated-equality 2 Very-stable (Squash A)
  Very-stable-≡₁ = Very-stable→Very-stable-≡ 1 Very-stable-≡₀

  -- And so on…

private

  -- A lemma.

  For-iterated-equality-Is-proposition↔H-level′-suc :
    {A : Type a} →
    ∀ n →
    For-iterated-equality n Is-proposition A ↝[ a ∣ a ]
    H-level′ (suc n) A
  For-iterated-equality-Is-proposition↔H-level′-suc {A = A} n ext =
    For-iterated-equality n Is-proposition A  ↝⟨ For-iterated-equality-cong₁ ext n (H-level↔H-level′ {n = 1} ext) ⟩
    For-iterated-equality n (H-level′ 1) A    ↝⟨ For-iterated-equality-For-iterated-equality n 1 ext ⟩□
    H-level′ (suc n) A                        □

-- If A is "stable 1 + n levels up", then H-level′ (suc n) A is
-- stable.

Stable-H-level′ :
  ∀ n →
  For-iterated-equality (suc n) Stable A →
  Stable (H-level′ (suc n) A)
Stable-H-level′ {A = A} n =
  For-iterated-equality (suc n) Stable A               ↝⟨ inverse-ext? (For-iterated-equality-For-iterated-equality n 1) _ ⟩
  For-iterated-equality n Stable-≡ A                   ↝⟨ For-iterated-equality-cong₁ _ n lemma ⟩
  For-iterated-equality n (Stable ∘ Is-proposition) A  ↝⟨ For-iterated-equality-commutes-← _ Stable n Stable-Π ⟩
  Stable (For-iterated-equality n Is-proposition A)    ↝⟨ Stable-map (For-iterated-equality-Is-proposition↔H-level′-suc n _) ⟩□
  Stable (H-level′ (suc n) A)                          □
  where
  lemma : ∀ {A} → Stable-≡ A → Stable (Is-proposition A)
  lemma s =
    Stable-Π λ _ →
    Stable-Π λ _ →
    s _ _

-- If A is "stable 1 + n levels up", then H-level (suc n) A is
-- stable.

Stable-H-level :
  ∀ n →
  For-iterated-equality (suc n) Stable A →
  Stable (H-level (suc n) A)
Stable-H-level {A = A} n =
  For-iterated-equality (suc n) Stable A  ↝⟨ Stable-H-level′ n ⟩
  Stable (H-level′ (suc n) A)             ↝⟨ Stable-map (record { to = inverse-ext? H-level↔H-level′ _; from = H-level↔H-level′ _ }) ⟩□
  Stable (H-level (suc n) A)              □

-- If A is "very stable 1 + n levels up", then H-level′ (suc n) A is
-- very stable (assuming extensionality).

Very-stable-H-level′ :
  {A : Type a} →
  Extensionality a a →
  ∀ n →
  For-iterated-equality (suc n) Very-stable A →
  Very-stable (H-level′ (suc n) A)
Very-stable-H-level′ {A = A} ext n =
  For-iterated-equality (suc n) Very-stable A               ↝⟨ inverse-ext? (For-iterated-equality-For-iterated-equality n 1) _ ⟩
  For-iterated-equality n Very-stable-≡ A                   ↝⟨ For-iterated-equality-cong₁ _ n lemma ⟩
  For-iterated-equality n (Very-stable ∘ Is-proposition) A  ↝⟨ For-iterated-equality-commutes-← _ Very-stable n (Very-stable-Π ext) ⟩
  Very-stable (For-iterated-equality n Is-proposition A)    ↝⟨ Very-stable-map (For-iterated-equality-Is-proposition↔H-level′-suc n ext) ⟩□
  Very-stable (H-level′ (suc n) A)                          □
  where
  lemma : ∀ {A} → Very-stable-≡ A → Very-stable (Is-proposition A)
  lemma s =
    Very-stable-Π ext λ _ →
    Very-stable-Π ext λ _ →
    s _ _

-- If A is "very stable 1 + n levels up", then H-level (suc n) A is
-- very stable (assuming extensionality).

Very-stable-H-level :
  {A : Type a} →
  Extensionality a a →
  ∀ n →
  For-iterated-equality (suc n) Very-stable A →
  Very-stable (H-level (suc n) A)
Very-stable-H-level {A = A} ext n =
  For-iterated-equality (suc n) Very-stable A  ↝⟨ Very-stable-H-level′ ext n ⟩
  Very-stable (H-level′ (suc n) A)             ↝⟨ Very-stable-cong _ (inverse $ H-level↔H-level′ ext) ⟩□
  Very-stable (H-level (suc n) A)              □

-- If equality is stable for A and B, then it is stable for A ⊎ B.

Stable-≡-⊎ :
  ∀ n →
  For-iterated-equality (suc n) Stable A →
  For-iterated-equality (suc n) Stable B →
  For-iterated-equality (suc n) Stable (A ⊎ B)
Stable-≡-⊎ n sA sB =
  For-iterated-equality-⊎-suc
    n
    (Stable-map ∘ from-isomorphism)
    (Very-stable→Stable 0 Very-stable-⊥)
    (For-iterated-equality-↑ _ (suc n) (Stable-map ∘ from-isomorphism) sA)
    (For-iterated-equality-↑ _ (suc n) (Stable-map ∘ from-isomorphism) sB)

-- If equality is very stable for A and B, then it is very stable
-- for A ⊎ B.

Very-stable-≡-⊎ :
  ∀ n →
  For-iterated-equality (suc n) Very-stable A →
  For-iterated-equality (suc n) Very-stable B →
  For-iterated-equality (suc n) Very-stable (A ⊎ B)
Very-stable-≡-⊎ n sA sB =
  For-iterated-equality-⊎-suc
    n
    lemma
    Very-stable-⊥
    (For-iterated-equality-↑ _ (suc n) lemma sA)
    (For-iterated-equality-↑ _ (suc n) lemma sB)
  where
  lemma : A ↔ B → Very-stable A → Very-stable B
  lemma = Very-stable-cong _ ∘ from-isomorphism

-- If equality is stable for A, then it is stable for List A.

Stable-≡-List :
  ∀ n →
  For-iterated-equality (suc n) Stable A →
  For-iterated-equality (suc n) Stable (List A)
Stable-≡-List n =
  For-iterated-equality-List-suc
    n
    (Stable-map ∘ from-isomorphism)
    (Very-stable→Stable 0 $ Very-stable-↑ Very-stable-⊤)
    (Very-stable→Stable 0 Very-stable-⊥)
    Stable-×

-- If equality is very stable for A, then it is very stable for
-- List A.

Very-stable-≡-List :
  ∀ n →
  For-iterated-equality (suc n) Very-stable A →
  For-iterated-equality (suc n) Very-stable (List A)
Very-stable-≡-List n =
  For-iterated-equality-List-suc
    n
    (Very-stable-cong _ ∘ from-isomorphism)
    (Very-stable-↑ Very-stable-⊤)
    Very-stable-⊥
    Very-stable-×

----------------------------------------------------------------------
-- Simple corollaries or variants of results above

-- A generalisation of Stable-Π.

Stable-Πⁿ :
  {A : Type a} {P : A → Type p} →
  Extensionality a p →
  ∀ n →
  (∀ x → For-iterated-equality n Stable (P x)) →
  For-iterated-equality n Stable ((x : A) → P x)
Stable-Πⁿ ext n =
  For-iterated-equality-Π
    ext
    n
    (Stable-map ∘ from-isomorphism)
    Stable-Π

-- A generalisation of Very-stable-Π.

Very-stable-Πⁿ :
  {A : Type a} {P : A → Type p} →
  Extensionality a p →
  ∀ n →
  (∀ x → For-iterated-equality n Very-stable (P x)) →
  For-iterated-equality n Very-stable ((x : A) → P x)
Very-stable-Πⁿ ext n =
  For-iterated-equality-Π
    ext
    n
    (Very-stable-cong _ ∘ from-isomorphism)
    (Very-stable-Π ext)

-- A generalisation of Stable-×.

Stable-×ⁿ :
  ∀ n →
  For-iterated-equality n Stable A →
  For-iterated-equality n Stable B →
  For-iterated-equality n Stable (A × B)
Stable-×ⁿ n =
  For-iterated-equality-×
    n
    (Stable-map ∘ from-isomorphism)
    Stable-×

-- A generalisation of Very-stable-×.

Very-stable-×ⁿ :
  ∀ n →
  For-iterated-equality n Very-stable A →
  For-iterated-equality n Very-stable B →
  For-iterated-equality n Very-stable (A × B)
Very-stable-×ⁿ n =
  For-iterated-equality-×
    n
    (Very-stable-cong _ ∘ from-isomorphism)
    Very-stable-×

-- A generalisation of Stable-↑.

Stable-↑ⁿ :
  ∀ n →
  For-iterated-equality n Stable A →
  For-iterated-equality n Stable (↑ ℓ A)
Stable-↑ⁿ n =
  For-iterated-equality-↑ _ n (Stable-map ∘ from-isomorphism)

-- A generalisation of Very-stable-↑.

Very-stable-↑ⁿ :
  ∀ n →
  For-iterated-equality n Very-stable A →
  For-iterated-equality n Very-stable (↑ ℓ A)
Very-stable-↑ⁿ n =
  For-iterated-equality-↑
    _
    n
    (Very-stable-cong _ ∘ from-isomorphism)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module RenamingAndSubstitution where

open import Library
open import Syntax
open ≡-Reasoning

infixr 4 _,_

------------------------------------------------------------------------
-- Renaming
------------------------------------------------------------------------

-- Renamings from Γ to Δ are snoc-lists of variables living in Δ,
-- one for each entry in Γ.

data Ren (Δ : Cxt) : (Γ : Cxt) → Set where
  ε   : Ren Δ ε
  _,_ : ∀ {Γ a} (ρ : Ren Δ Γ) (x : Var Δ a) → Ren Δ (Γ , a)

-- A renaming in  Ren Δ Γ  is a code for a
-- renaming function in  Var Γ ∙→ Var Δ.

lookr : ∀{Γ Δ} → Ren Δ Γ → ∀ {σ} → Var Γ σ → Var Δ σ
lookr (xs , x) zero    = x
lookr (xs , x) (suc i) = lookr xs i

-- Weaking a renaming by increasing all variables by 1.
-- This lets them live in the extended context Γ , σ.

wkr : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ , σ) Δ
wkr ε        = ε
wkr (xs , x) = wkr xs , suc x

-- Lifting a renaming to go under a binder.

liftr : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ , σ) (Δ , σ)
liftr xs = wkr xs , zero

-- The category of renamings (operations only).
------------------------------------------------------------------------

-- The identity renaming.

renId : ∀{Γ} → Ren Γ Γ
renId {ε}     = ε
renId {Γ , _} = liftr (renId {Γ})

-- Forward composition of renamings.

renComp : ∀{Φ Γ Δ} → Ren Δ Γ → Ren Γ Φ → Ren Δ Φ
renComp xs ε        = ε
renComp xs (ys , y) = renComp xs ys , lookr xs y

-- Various combinations of renamings.
------------------------------------------------------------------------

-- Weakening a renaming acts behaves like
-- post-composing the renaming function with successor.

lookrwkr : ∀{Γ Δ σ τ}(xs : Ren Δ Γ)(i : Var Γ σ) →
           lookr (wkr {σ = τ} xs) i ≡ suc (lookr xs i)
lookrwkr (xs , _) zero    = refl
lookrwkr (xs , _) (suc i) = lookrwkr xs i

-- A weakning cancels a renaming extension.

lemrr : ∀{Φ Γ Δ σ}(xs : Ren Φ Γ)(x : Var Φ σ)(ys : Ren Γ Δ) →
       renComp (xs , x) (wkr ys) ≡ renComp xs ys
lemrr xs x ε        = refl
lemrr xs x (ys , y) = cong (_, lookr xs y) (lemrr xs x ys)

-- Associativity of renaming composition in case the first
-- renaming is a weakening.

wkrcomp : ∀{Φ Γ Δ σ}(xs : Ren Φ Γ)(ys : Ren Γ Δ) →
  renComp (wkr {σ = σ} xs) ys ≡ wkr {σ = σ} (renComp xs ys)
wkrcomp xs ε        = refl
wkrcomp xs (ys , y) = cong₂ _,_ (wkrcomp xs ys) (lookrwkr xs y)

-- Composition of liftings is a lifting.

liftrcomp : ∀{Φ Γ Δ σ}(xs : Ren Φ Γ)(ys : Ren Γ Δ) →
  renComp (liftr {σ = σ} xs) (liftr {σ = σ} ys) ≡ liftr {σ = σ} (renComp xs ys)
liftrcomp xs ys = begin
  renComp (wkr xs , zero) (wkr ys) , zero  ≡⟨ cong (_, zero) (lemrr (wkr xs) zero ys) ⟩
  renComp (wkr xs) ys              , zero  ≡⟨ cong (_, zero) (wkrcomp xs ys) ⟩
  wkr (renComp xs ys)              , zero  ∎

-- lookr is a morphism from the category  Ren
-- to the category of the corresponding renaming functions on variables.
------------------------------------------------------------------------

-- The identity renaming corresponds to the identity function.

lookrid : ∀{Γ σ}(x : Var Γ σ) → lookr renId x ≡ x
lookrid zero    = refl
lookrid (suc x) = begin
  lookr (wkr renId) x  ≡⟨ lookrwkr renId x ⟩
  suc (lookr renId x)  ≡⟨ cong suc (lookrid x) ⟩
  suc x                ∎

-- A composition of renamings corresponds to the composition
-- of the corresponding renaming functions.

lookrcomp : ∀{Φ Γ Δ}(f : Ren Δ Γ)(g : Ren Γ Φ){σ}(i : Var Φ σ) →
            lookr (renComp f g) i ≡ (lookr f ∘ lookr g) i
lookrcomp f (g , v) zero = refl
lookrcomp f (g , v) (suc i) = lookrcomp f g i

-- Laws for the category of renamings.
------------------------------------------------------------------------

-- Left identity of forward composition

lidr : ∀{Φ Γ}(xs : Ren Φ Γ) → renComp renId xs ≡ xs
lidr ε        = refl
lidr (xs , x) = cong₂ _,_ (lidr xs) (lookrid x)

-- Right identity of forward composition

ridr : ∀{Φ Γ}(xs : Ren Φ Γ) → renComp xs renId ≡ xs
ridr {Γ = ε}     ε  = refl
ridr {Γ = Γ , σ} (xs , x) = begin
  renComp (xs , x) (wkr renId) , x  ≡⟨ cong (_, x) (lemrr xs x renId) ⟩
  renComp xs renId             , x  ≡⟨ cong (_, x) (ridr xs) ⟩
  xs                           , x  ∎

-- Renaming of terms.
------------------------------------------------------------------------

-- Renaming in a term.

ren : ∀{Γ Δ} → Ren Δ Γ → ∀ {σ} → Tm Γ σ → Tm Δ σ
ren xs (var x)   = var (lookr xs x)
ren xs (abs t)   = abs (ren (liftr xs) t)
ren xs (app t u) = app (ren xs t) (ren xs u)

-- ren is a morphism from Ren
-- to the corresponding category of renaming functions on terms.

renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≡ t
renid (var x)   = cong var (lookrid x)
renid (abs t)   = cong abs (renid t)
renid (app t u) = cong₂ app (renid t) (renid u)

rencomp : ∀ {Φ Γ Δ}(f : Ren Δ Γ)(g : Ren Γ Φ){σ}(t : Tm Φ σ) →
            ren (renComp f g) t ≡ (ren f ∘ ren g) t
rencomp f g (var x)   = cong var (lookrcomp f g x)
rencomp f g (abs t)   = begin
  abs (ren (liftr (renComp f g))         t)   ≡⟨ cong (λ xs → abs $ ren xs t) (sym $ liftrcomp f g) ⟩
  abs (ren (renComp (liftr f) (liftr g)) t)   ≡⟨ cong abs (rencomp (liftr f) (liftr g) t) ⟩
  abs (ren (liftr f) (ren (liftr g) t))       ∎
rencomp f g (app t u) = cong₂ app (rencomp f g t) (rencomp f g u)

-- Weakening a term.

weak : ∀{Γ b} a → Tm Γ b → Tm (Γ , a) b
weak a = ren (wkr renId)

-- Renaming of normal forms.
------------------------------------------------------------------------

mutual
  rennf : ∀{Γ Δ} → Ren Γ Δ → ∀{a} → Nf Δ a → Nf Γ a
  rennf α (ne t)   = ne (rennen α t)
  rennf α (abs t)  = abs (rennf (liftr α) t)

  rennen : ∀{Γ Δ} → Ren Γ Δ → ∀{a} → Ne Δ a → Ne Γ a
  rennen α (var x) = var (lookr α x)
  rennen α (app n x) = app (rennen α n) (rennf α x)

------------------------------------------------------------------------
-- Substitution
------------------------------------------------------------------------

data Sub (Δ : Cxt) : (Γ : Cxt) → Set where
  ε   : Sub Δ ε
  _,_ : ∀ {Γ a} (ρ : Sub Δ Γ) (v : Tm Δ a) → Sub Δ (Γ , a)

ren2sub : ∀{Γ Δ} → Ren Γ Δ → Sub Γ Δ
ren2sub ε        = ε
ren2sub (xs , x) = ren2sub xs , var x

looks : ∀{Γ Δ} → Sub Δ Γ → ∀ {σ} → Var Γ σ → Tm Δ σ
looks (xs , x) zero    = x
looks (xs , x) (suc i) = looks xs i

wks : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ , σ) Δ
wks ε        = ε
wks (xs , x) = wks xs , ren (wkr renId) x

lifts : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ , σ) (Δ , σ)
lifts xs = wks xs , var zero

sub : ∀{Γ Δ} → Sub Δ Γ → ∀{σ} → Tm Γ σ → Tm Δ σ
sub xs (var x)   = looks xs x
sub xs (abs t)   = abs (sub (lifts xs) t)
sub xs (app t u) = app (sub xs t) (sub xs u)

subId : ∀{Γ} → Sub Γ Γ
subId {ε}     = ε
subId {Γ , _} = lifts (subId {Γ})

subComp : ∀{Φ Γ Δ} → Sub Δ Γ → Sub Γ Φ → Sub Δ Φ
subComp xs ε        = ε
subComp xs (ys , y) = subComp xs ys , sub xs y

-- Substitute the last variable

sub0 : ∀{Γ a b} → Tm (Γ , a) b → Tm Γ a → Tm Γ b
sub0 t u = sub (subId , u) t

-- Substitution laws

lookswks : ∀{Γ Δ σ τ}(i : Var Γ σ)(xs : Sub Δ Γ) →
           looks (wks {σ = τ} xs) i ≡ ren (wkr {σ = τ} renId) (looks xs i)
lookswks zero    (xs , _) = refl
lookswks (suc i) (xs , _) = lookswks i xs

lemsr : ∀{Φ Γ Δ σ}(xs : Sub Φ Γ)(x : Tm Φ σ)(ys : Ren Γ Δ) →
        subComp (xs , x) (ren2sub (wkr ys)) ≡ subComp xs (ren2sub ys)
lemsr xs x ε        = refl
lemsr xs x (ys , y) = cong (λ zs → zs , looks xs y) (lemsr xs x ys)

lookslookr : ∀{Φ Γ Δ}(f : Sub Δ Γ)(g : Ren Γ Φ){σ}(x : Var Φ σ) →
            looks (subComp f (ren2sub g)) x ≡ looks f (lookr g x)
lookslookr f (g , _) zero    = refl
lookslookr f (g , _) (suc x) = lookslookr f g x

wksrcomp : ∀{Φ Γ Δ σ}(xs : Sub Φ Γ)(ys : Ren Γ Δ) →
  subComp (wks {σ = σ} xs) (ren2sub ys) ≡ wks {σ = σ} (subComp xs (ren2sub ys))
wksrcomp xs ε        = refl
wksrcomp xs (ys , y) = cong₂ Sub._,_ (wksrcomp xs ys) (lookswks y xs)

liftsrcomp : ∀{Φ Γ Δ σ}(xs : Sub Φ Γ)(ys : Ren Γ Δ) →
             subComp (lifts {σ = σ} xs) (ren2sub (liftr ys)) ≡ lifts {σ = σ} (subComp xs (ren2sub ys))
liftsrcomp xs ys = begin
  subComp (wks xs , var zero) (ren2sub (wkr ys)) , var zero ≡⟨ cong (_, var zero) (lemsr (wks xs) (var zero) ys) ⟩
  subComp (wks xs) (ren2sub ys)                  , var zero ≡⟨ cong (_, var zero) (wksrcomp xs ys) ⟩
  wks (subComp xs (ren2sub ys))                  , var zero ∎

subren : ∀{Φ Γ Δ}(f : Sub Δ Γ)(g : Ren Γ Φ){σ}(t : Tm Φ σ) →
         (sub f ∘ ren g) t ≡ sub (subComp f (ren2sub g)) t
subren f g (var x)   = sym $ lookslookr f g x
subren f g (abs t)   = begin
  abs (sub (lifts f) (ren (liftr g) t))               ≡⟨ cong abs $ subren (lifts f) (liftr g) t ⟩
  abs (sub (subComp (lifts f) (ren2sub (liftr g))) t) ≡⟨ cong (λ f → abs (sub f t)) $ liftsrcomp f g ⟩
  abs (sub (lifts (subComp f (ren2sub g))) t)         ∎
subren f g (app t u) = cong₂ app (subren f g t) (subren f g u)

looksid : ∀{Γ σ}(x : Var Γ σ) → looks subId x ≡ var x
looksid zero    = refl
looksid (suc x) = begin
  looks (wks subId) x             ≡⟨ lookswks x subId ⟩
  ren (wkr renId) (looks subId x) ≡⟨ cong (ren (wkr renId)) (looksid x) ⟩
  ren (wkr renId) (var x)         ≡⟨⟩
  var (lookr (wkr renId) x)       ≡⟨ cong var $ lookrwkr renId x ⟩
  var (suc (lookr renId x))       ≡⟨ cong (λ x → var (suc x)) (lookrid x) ⟩ -- using ∘ makes it go yellow
  var (suc x)                     ∎

subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≡ t
subid (var x)   = looksid x
subid (abs t)   = cong abs (subid t)
subid (app t u) = cong₂ app (subid t) (subid u)

sidl : ∀{Φ Γ}(xs : Sub Φ Γ) → subComp subId xs ≡ xs
sidl ε        = refl
sidl (xs , t) = cong₂ _,_ (sidl xs) (subid t)

sidr2 : ∀{Φ Γ}(xs : Sub Φ Γ) → subComp xs (ren2sub renId) ≡ xs
sidr2 {Γ = ε} ε            = refl
sidr2 {Γ = Γ , a} (xs , x) = begin
  subComp (xs , x) (ren2sub (wkr renId)) , x ≡⟨ cong (_, x) (lemsr xs x renId) ⟩
  subComp xs (ren2sub renId)             , x ≡⟨ cong (_, x) (sidr2 xs) ⟩
  xs                                     , x ∎

liftSubRen : ∀{Γ Δ a b} (f : Sub Δ Γ) (t : Tm Γ b)
  → sub (lifts f) (weak a t) ≡ sub (wks f) t
liftSubRen {a = a} f t = begin
  sub (lifts f) (weak a t)  ≡⟨ subren (lifts f) (wkr renId) t ⟩
  sub (subComp (lifts f) (ren2sub (wkr renId))) t ≡⟨ cong (λ f' → sub f' t) (lemsr (wks f) (var zero) renId) ⟩
  sub (subComp (wks f) (ren2sub renId)) t ≡⟨ cong (λ f' → sub f' t) (sidr2 (wks f)) ⟩
  sub (wks f) t ∎

lemss : ∀{Φ Γ Δ σ}(xs : Sub Φ Γ)(x : Tm Φ σ)(ys : Sub Γ Δ) →
        subComp (xs , x) (wks ys) ≡ subComp xs ys
lemss xs x ε        = refl
lemss xs x (ys , y) = begin
  subComp (xs , x) (wks ys) , sub (xs , x) (ren (wkr renId) y)               ≡⟨ cong₂ _,_ (lemss xs x ys) (subren (xs , x) (wkr renId) y) ⟩
  subComp xs       ys       , sub (subComp (xs , x) (ren2sub (wkr renId))) y ≡⟨ cong (λ g → subComp xs ys , sub g y) (lemsr xs x renId) ⟩
  subComp xs       ys       , sub (subComp xs       (ren2sub renId))       y ≡⟨ cong (λ g → subComp xs ys , sub g y) (sidr2 xs) ⟩
  subComp xs       ys       , sub xs                                       y ∎

ren2sublook : ∀{Γ Δ σ}(f : Ren Δ Γ)(i : Var Γ σ) →
              var (lookr f i) ≡ looks (ren2sub f) i
ren2sublook (f , _) zero    = refl
ren2sublook (f , _) (suc i) = ren2sublook f i

ren2subwk : ∀{Γ Δ σ}(g : Ren Δ Γ) →
            ren2sub (wkr {σ = σ} g) ≡ wks {σ = σ} (ren2sub g)
ren2subwk ε       = refl
ren2subwk (g , x) = begin
  (ren2sub (wkr g) , var (suc x))               ≡⟨ cong₂ (λ xs x → xs , var (suc x)) (ren2subwk g) (sym $ lookrid x) ⟩
  (wks (ren2sub g) , var (suc (lookr renId x))) ≡⟨ cong (λ x → wks (ren2sub g) , var x) (sym $ lookrwkr renId x) ⟩
  (wks (ren2sub g) , var (lookr (wkr renId) x)) ∎

ren2sublift : ∀{Γ Δ σ}(g : Ren Δ Γ) →
            ren2sub (liftr {σ = σ} g) ≡ lifts {σ = σ} (ren2sub g)
ren2sublift g = cong (_, var zero) (ren2subwk g)

ren2subren : ∀{Γ Δ σ}(f : Ren Δ Γ)(t : Tm Γ σ) → ren f t ≡ sub (ren2sub f) t
ren2subren f (var x)   = ren2sublook f x
ren2subren f (abs t)   = begin
  abs (ren (liftr f) t)               ≡⟨ cong abs (ren2subren (liftr f) t) ⟩
  abs (sub (ren2sub (liftr f)) t)     ≡⟨ cong (λ f → abs (sub f t)) (ren2sublift f) ⟩
  abs (sub (lifts (ren2sub f)) t) ∎
ren2subren f (app t u) = cong₂ app (ren2subren f t) (ren2subren f u)

wkrscomp : ∀{Φ Γ Δ σ}(xs : Ren Φ Γ)(ys : Sub Γ Δ) →
  subComp (ren2sub (wkr {σ = σ} xs)) ys ≡ wks {σ = σ} (subComp (ren2sub xs) ys)
wkrscomp xs ε        = refl
wkrscomp xs (ys , y) = begin
  subComp (ren2sub (wkr xs)) ys , sub (ren2sub (wkr xs)) y                 ≡⟨ cong₂ _,_ (wkrscomp xs ys) (sym $ ren2subren (wkr xs) y) ⟩
  wks (subComp (ren2sub xs) ys) , ren (wkr xs) y                           ≡⟨ cong (λ f → wks (subComp (ren2sub xs) ys) , ren (wkr f) y) (sym $ lidr xs) ⟩
  wks (subComp (ren2sub xs) ys) , ren (wkr (renComp renId xs))  y          ≡⟨ cong (λ f → wks (subComp (ren2sub xs) ys) , ren f y) (sym $ wkrcomp renId xs) ⟩
  wks (subComp (ren2sub xs) ys) , ren (renComp (wkr renId)  xs) y          ≡⟨ cong (wks (subComp (ren2sub xs) ys) ,_) (rencomp (wkr renId) xs y) ⟩
  wks (subComp (ren2sub xs) ys) , ren (wkr renId) (ren xs y)               ≡⟨ cong (λ t → wks (subComp (ren2sub xs) ys) , ren (wkr renId) t) (ren2subren xs y)  ⟩
  wks (subComp (ren2sub xs) ys) , ren (wkr renId) (sub (ren2sub xs) y)     ∎

liftrscomp : ∀{Φ Γ Δ σ}(xs : Ren Φ Γ)(ys : Sub Γ Δ) →
  subComp (ren2sub (liftr {σ = σ} xs)) (lifts ys) ≡ lifts {σ = σ} (subComp (ren2sub xs) ys)
liftrscomp xs ys = begin
  (subComp (ren2sub (wkr xs) , var zero) (wks ys) , var zero) ≡⟨ cong (_, var zero) (lemss (ren2sub (wkr xs)) (var zero) ys) ⟩
  (subComp (ren2sub (wkr xs)) ys                  , var zero) ≡⟨ cong (_, var zero) (wkrscomp xs ys) ⟩
  (wks (subComp (ren2sub xs) ys)                  , var zero) ∎

renlooks : ∀{Φ Γ Δ}(f : Ren Δ Γ)(g : Sub Γ Φ){σ}(x : Var Φ σ) →
         (ren f ∘ looks g) x ≡ looks (subComp (ren2sub f) g) x
renlooks f (_ , v) zero    = ren2subren f v
renlooks f (g , _) (suc x) = renlooks f g x

rensub : ∀{Φ Γ Δ}(f : Ren Δ Γ)(g : Sub Γ Φ){σ}(t : Tm Φ σ) →
         (ren f ∘ sub g) t ≡ sub (subComp (ren2sub f) g) t
rensub f g (var x) = renlooks f g x
rensub f g (abs t) = begin
  abs (ren (liftr f) (sub (lifts g) t))               ≡⟨ cong abs $ rensub (liftr f) (lifts g) t ⟩
  abs (sub (subComp (ren2sub (liftr f)) (lifts g)) t) ≡⟨ cong (λ f → abs (sub f t)) (liftrscomp f g) ⟩
  abs (sub (lifts (subComp (ren2sub f) g)) t)         ∎
rensub f g (app t u) = cong₂ app (rensub f g t) (rensub f g u)

lookscomp : ∀{Φ Γ Δ}(f : Sub Δ Γ)(g : Sub Γ Φ){σ}(x : Var Φ σ) →
            looks (subComp f g) x ≡ sub f (looks g x)
lookscomp f (g , _) zero    = refl
lookscomp f (g , _) (suc x) = lookscomp f g x

ren2subid : ∀{Γ} → subId {Γ} ≡ ren2sub renId
ren2subid {ε}     = refl
ren2subid {Γ , a} = begin
  (wks subId           , var zero) ≡⟨ cong (λ f → wks f , var zero) (ren2subid {Γ}) ⟩
  (wks (ren2sub renId) , var zero) ≡⟨ cong (_, var zero) (sym $ ren2subwk renId) ⟩
  (ren2sub (wkr renId) , var zero) ∎

wksscomp : ∀{Φ Γ Δ σ}(xs : Sub Φ Γ)(ys : Sub Γ Δ) →
  subComp (wks {σ = σ} xs) ys ≡ wks {σ = σ} (subComp xs ys)
wksscomp xs ε        = refl
wksscomp xs (ys , y) = begin
  subComp (wks xs) ys , sub (wks xs)                           y ≡⟨ cong (λ f → subComp (wks xs) ys , sub (wks f) y) (sym $ sidl xs) ⟩
  subComp (wks xs) ys , sub (wks (subComp subId xs))           y ≡⟨ cong₂ _,_ (wksscomp xs ys) (cong (λ f → sub (wks (subComp f xs)) y) ren2subid) ⟩
  wks (subComp xs ys) , sub (wks (subComp (ren2sub renId) xs)) y ≡⟨ cong (λ f → wks (subComp xs ys) , sub f y) (sym $ wkrscomp renId xs) ⟩
  wks (subComp xs ys) , sub (subComp (ren2sub (wkr renId)) xs) y ≡⟨ cong (wks (subComp xs ys) ,_) (sym $ rensub (wkr renId) xs y) ⟩
  wks (subComp xs ys) , ren (wkr renId) (sub xs y)               ∎

sidr : ∀{Φ Γ}(xs : Sub Φ Γ) → subComp xs subId ≡ xs
sidr xs = begin
  subComp xs subId           ≡⟨ cong (subComp xs) ren2subid ⟩
  subComp xs (ren2sub renId) ≡⟨ sidr2 xs ⟩
  xs                         ∎

liftscomp : ∀{Φ Γ Δ σ}(xs : Sub Φ Γ)(ys : Sub Γ Δ) →
  subComp (lifts {σ = σ} xs) (lifts ys) ≡ lifts {σ = σ} (subComp xs ys)
liftscomp xs ys = begin
  subComp (wks xs , var zero) (wks ys) , var zero ≡⟨ cong (_, var zero) (lemss (wks xs) (var zero) ys) ⟩
  subComp (wks xs) ys                  , var zero ≡⟨ cong (_, var zero) (wksscomp xs ys) ⟩
  wks (subComp xs ys)                  , var zero ∎

subcomp : ∀{Φ Γ Δ}(f : Sub Δ Γ)(g : Sub Γ Φ){σ}(t : Tm Φ σ) →
          sub (subComp f g) t ≡ (sub f ∘ sub g) t
subcomp f g (var x)   = lookscomp f g x
subcomp f g (abs t)   = begin
  abs (sub (lifts (subComp f g)) t)         ≡⟨ cong (λ f → abs (sub f t)) (sym $ liftscomp f g) ⟩
  abs (sub (subComp (lifts f) (lifts g)) t) ≡⟨ cong abs (subcomp (lifts f) (lifts g) t) ⟩
  abs (sub (lifts f) (sub (lifts g) t))     ∎
subcomp f g (app t u) = cong₂ app (subcomp f g t) (subcomp f g u)

--

mutual
  renembNe : ∀{Γ Δ a}(u : Ne Γ a)(σ : Ren Δ Γ) →
             ren σ (embNe u) ≡ embNe (rennen σ u)
  renembNe (var x)   σ = refl
  renembNe (app u n) σ = cong₂ app (renembNe u σ) (renembNf n σ)

  renembNf : ∀{Γ Δ a}(n : Nf Γ a)(σ : Ren Δ Γ) →
             ren σ (embNf n) ≡ embNf (rennf σ n)
  renembNf (abs n) σ = cong abs (renembNf n (liftr σ))
  renembNf (ne n)  σ = renembNe n σ
-- -}

ext: agda

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
module Issue127 where

data C : Set where
  c : C
  d : C

F : C → Set → Set
F c = λ A → A
F d = λ A → A

data D : C → Set where
  d : (x : C) → F x (D x) → D x

--                                               .-< no longer
-- The following non-well-founded definition is / seemingly accepted by
-- Agda:

∞ : (x : C) → D x
∞ x = d x (d x (∞ x))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module test.StringLiteral where

open import Type
open import Declarative
open import Builtin
open import Builtin.Constant.Type
open import Builtin.Constant.Term Ctx⋆ Kind * # _⊢⋆_ con size⋆

-- zerepoch/zerepoch-core/test/data/stringLiteral.plc

postulate str1 : ByteString
{-# FOREIGN GHC import qualified Data.ByteString.Char8 as BS #-}
{-# COMPILE GHC str1 = BS.pack "4321758fabce1aa4780193f" #-}

open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.TrustMe

lemma1 : length str1 ≡ 23
lemma1 = primTrustMe

open import Data.Nat

lemma1' : BoundedB 100 str1
lemma1' rewrite lemma1 = gen _ _ _

stringLit : ∀{Γ} → Γ ⊢ con bytestring (size⋆ 100)
stringLit = con (bytestring 100  str1 lemma1')

max_stars_repo_name: Quantum-One-DLT/zerepoch

max_issues_repo_name: Quantum-One-DLT/zerepoch

max_forks_repo_name: Quantum-One-DLT/zerepoch


text:
------------------------------------------------------------------------
-- Simplification of parsers
------------------------------------------------------------------------

module TotalParserCombinators.Simplification where

open import Algebra
open import Codata.Musical.Notation
open import Data.List using (List; [])
import Data.List.Relation.Binary.BagAndSetEquality as BSEq
open import Data.Maybe using (Maybe); open Data.Maybe.Maybe
open import Data.Nat
open import Data.Product
open import Data.Vec.Recursive hiding ([])
open import Function
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; [_])
open import Relation.Binary.HeterogeneousEquality
  using (refl) renaming (_≅_ to _≅H_)

private
  module BSMonoid {k} {A : Set} =
    CommutativeMonoid (BSEq.commutativeMonoid k A)

open import TotalParserCombinators.Congruence
  hiding (return; fail; token) renaming (_∣_ to _∣′_)
import TotalParserCombinators.Congruence.Sound as C
import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- Simplification of a single "layer"

-- The result type used for single-layer simplification.

record Simplify₁ {Tok R xs} (p : Parser Tok R xs) : Set₁ where
  constructor result
  field
    {bag}   : List R
    parser  : Parser Tok R bag
    correct : p ≅P parser

-- The function simplify₁ simplifies the first "layer" of a parser,
-- down to the first occurrences of ♯_. The following simplifications
-- are applied in a bottom-up manner (in relevant cases also for
-- delayed arguments):
--
-- f <$> fail                  → fail
-- f <$> return x              → return (f x)
-- fail         ∣ p            → p
-- p            ∣ fail         → p
-- token >>= p₁ ∣ token >>= p₂ → token >>= λ t →
--                                 ♯ (♭? (p₁ t) ∣ ♭? (p₂ t))
-- fail     ⊛ p                → fail
-- p        ⊛ fail             → fail
-- return f ⊛ return x         → return (f x)
-- fail     >>= p              → fail
-- return x >>= p              → p x
-- nonempty fail               → fail
-- nonempty (return x)         → fail
-- cast eq p                   → p
--
-- Some ♯_'s may be removed, but care is taken to ensure that
-- non-simplified parsers in the result are delayed.

mutual

  simplify₁ : ∀ {Tok R xs} (p : Parser Tok R xs) → Simplify₁ p

  -- • return:

  simplify₁ (return x) = result _ (return x ∎)

  -- • fail:

  simplify₁ fail       = result _ (fail ∎)

  -- • token:

  simplify₁ token      = result _ (token ∎)

  -- • _<$>_:

  simplify₁ (f <$> p) with simplify₁ p
  ... | result fail       p≅∅  = result _ (
                                 f <$> p     ≅⟨ (λ _ → refl) <$> p≅∅ ⟩
                                 f <$> fail  ≅⟨ <$>.zero ⟩
                                 fail        ∎)
  ... | result (return x) p≅ε  = result _ (
                                 f <$> p         ≅⟨ (λ x → refl {x = f x}) <$> p≅ε ⟩
                                 f <$> return x  ≅⟨ <$>.homomorphism f ⟩
                                 return (f x)    ∎)
  ... | result p′         p≅p′ = result _ (
                                 f <$> p   ≅⟨ (λ _ → refl) <$> p≅p′ ⟩
                                 f <$> p′  ∎)

  -- • _∣_:

  simplify₁ (p₁ ∣ p₂) with simplify₁ p₁ | simplify₁ p₂
  ... | result fail          p₁≅∅
      | result p₂′           p₂≅p₂′ = result _ (
                                      p₁   ∣ p₂   ≅⟨ p₁≅∅ ∣′ p₂≅p₂′ ⟩
                                      fail ∣ p₂′  ≅⟨ AdditiveMonoid.left-identity p₂′ ⟩
                                      p₂′         ∎)
  ... | result p₁′           p₁≅p₁′
      | result fail          p₂≅∅   = result _ (
                                      p₁  ∣ p₂    ≅⟨ p₁≅p₁′ ∣′ p₂≅∅ ⟩
                                      p₁′ ∣ fail  ≅⟨ AdditiveMonoid.right-identity p₁′ ⟩
                                      p₁′         ∎)
  ... | result (p₁₁ >>= p₁₂) p₁≅…
      | result (p₂₁ >>= p₂₂) p₂≅…   = let h = helper p₁₁ refl p₁₂ p₂₁ refl p₂₂ in
                                      result _ (
                                      p₁          ∣ p₂           ≅⟨ p₁≅… ∣′ p₂≅… ⟩
                                      p₁₁ >>= p₁₂ ∣ p₂₁ >>= p₂₂  ≅⟨ Simplify₁.correct h ⟩
                                      Simplify₁.parser h         ∎)
    where
    helper : ∀ {Tok R₁ R₂ R xs₁ xs₁′ xs₂ xs₂′ f₁ f₂}
             (p₁₁ : ∞⟨ f₁ ⟩Parser Tok R₁ xs₁′)
             (eq₁ : xs₁′ ≡ flatten xs₁)
             (p₁₂ : (x : R₁) → ∞⟨ xs₁ ⟩Parser Tok R (apply f₁ x))
             (p₂₁ : ∞⟨ f₂ ⟩Parser Tok R₂ xs₂′)
             (eq₂ : xs₂′ ≡ flatten xs₂)
             (p₂₂ : (x : R₂) → ∞⟨ xs₂ ⟩Parser Tok R (apply f₂ x)) →
             Simplify₁ (P.subst (∞⟨ f₁ ⟩Parser Tok R₁) eq₁ p₁₁ >>= p₁₂ ∣
                        P.subst (∞⟨ f₂ ⟩Parser Tok R₂) eq₂ p₂₁ >>= p₂₂)
    helper p₁₁ eq₁ p₁₂ p₂₁ eq₂ p₂₂
      with ♭? p₁₁ | P.inspect ♭? p₁₁ | ♭? p₂₁ | P.inspect ♭? p₂₁
    helper {Tok} {f₁ = f₁} {f₂} p₁₁ eq₁ p₁₂ p₂₁ eq₂ p₂₂
      | token | [ eq₁′ ] | token | [ eq₂′ ] = result _ (
      cast₁ p₁₁ >>= p₁₂ ∣ cast₂ p₂₁ >>= p₂₂          ≅⟨ [ forced? p₁₁ - ○ - forced?′ p₁₂ - ○ ] Subst.correct∞ eq₁ p₁₁ >>=
                                                                                (λ t → ♭? (p₁₂ t) ∎) ∣′
                                                        [ forced? p₂₁ - ○ - forced?′ p₂₂ - ○ ] Subst.correct∞ eq₂ p₂₁ >>=
                                                                                (λ t → ♭? (p₂₂ t) ∎) ⟩
      ♭? p₁₁ >>= (♭? ∘ p₁₂) ∣ ♭? p₂₁ >>= (♭? ∘ p₂₂)  ≅⟨ [ ○ - ○ - ○ - ○ ]
                                                          P.subst (λ p → p ≅P token) (P.sym eq₁′) (token ∎) >>= (λ t → ♭? (p₁₂ t) ∎) ∣′
                                                        [ ○ - ○ - ○ - ○ ]
                                                          P.subst (λ p → p ≅P token) (P.sym eq₂′) (token ∎) >>= (λ t → ♭? (p₂₂ t) ∎) ⟩
      token >>= (♭? ∘ p₁₂) ∣ token >>= (♭? ∘ p₂₂)    ≅⟨ sym $ Monad.left-distributive token (♭? ∘ p₁₂) (♭? ∘ p₂₂) ⟩
      token >>= (λ t → ♭? (p₁₂ t) ∣ ♭? (p₂₂ t))      ≅⟨ [ ○ - ○ - ○ - ◌ ] token ∎ >>= (λ t → ♭? (p₁₂ t) ∣ ♭? (p₂₂ t) ∎) ⟩
      token >>= (λ t → ♯ (♭? (p₁₂ t) ∣ ♭? (p₂₂ t)))  ∎)
      where
      cast₁ = P.subst (∞⟨ f₁ ⟩Parser Tok Tok) eq₁
      cast₂ = P.subst (∞⟨ f₂ ⟩Parser Tok Tok) eq₂
    helper _ _ _ _ _ _ | _ | _ | _ | _ = result _ (_ ∎)

  simplify₁ (p₁ ∣ p₂) | result p₁′ p₁≅p₁′ | result p₂′ p₂≅p₂′ =
    result _ (
    p₁  ∣ p₂   ≅⟨ p₁≅p₁′ ∣′ p₂≅p₂′ ⟩
    p₁′ ∣ p₂′  ∎)

  -- • _⊛_:

  simplify₁ (p₁ ⊛ p₂) =
    helper _ _ p₁ p₂ (simplify₁∞ p₁) (simplify₁∞ p₂) refl refl
    where
    -- token ⊛ token is never type correct, but Agda's case-splitting
    -- machinery cannot see this, so instead of a with clause the
    -- following ugly machinery is used.

    cast₁ : ∀ {Tok R R₁ R₁′ xs xs′} {ys : Maybe (List R)} →
            (R≡  : R₁ ≡ R₁′) → xs ≅H xs′ →
            ∞⟨ ys ⟩Parser Tok R₁′ (flatten xs′) →
            ∞⟨ ys ⟩Parser Tok R₁  (flatten xs)
    cast₁ refl refl p = p

    helper : ∀ {Tok R₁ R₁′ R₂} fs xs {xs′}
               (p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs))
               (p₂ : ∞⟨ fs ⟩Parser Tok  R₁′      (flatten xs′)) →
             Simplify₁ (♭? p₁) → Simplify₁ (♭? p₂) →
             (R≡ : R₁ ≡ R₁′) (xs≅ : xs ≅H xs′) →
             Simplify₁ (p₁ ⊛ cast₁ R≡ xs≅ p₂)
    helper fs xs p₁ p₂ (result fail p₁≅∅) _ refl refl = result _ (
      p₁   ⊛ p₂     ≅⟨ [ xs - ○ - fs - ○ ] p₁≅∅ ⊛ (♭? p₂ ∎) ⟩
      fail ⊛ ♭? p₂  ≅⟨ ApplicativeFunctor.left-zero (♭? p₂) ⟩
      fail          ∎)
    helper fs xs p₁ p₂ _ (result fail p₂≅∅) refl refl = result _ (
      p₁    ⊛ p₂    ≅⟨ [ xs - ○ - fs - ○ ] ♭? p₁ ∎ ⊛ p₂≅∅ ⟩
      ♭? p₁ ⊛ fail  ≅⟨ ApplicativeFunctor.right-zero (♭? p₁) ⟩
      fail          ∎)
    helper fs xs p₁ p₂ (result (return f) p₁≅ε) (result (return x) p₂≅ε)
           refl refl = result _ (
      p₁       ⊛ p₂        ≅⟨ [ xs - ○ - fs - ○ ] p₁≅ε ⊛ p₂≅ε ⟩
      return f ⊛ return x  ≅⟨ ApplicativeFunctor.homomorphism f x ⟩
      return (f x)         ∎)
    helper fs xs p₁ p₂ p₁′ p₂′ R≡ xs≅ =
      helper′ fs xs p₁ p₂ p₁′ p₂′ R≡ xs≅
      where
      helper′ :
        ∀ {Tok R₁ R₁′ R₂} fs xs {xs′}
          (p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs))
          (p₂ : ∞⟨ fs ⟩Parser Tok  R₁′      (flatten xs′)) →
        Simplify₁ (♭? p₁) → Simplify₁ (♭? p₂) →
        (R≡ : R₁ ≡ R₁′) (xs≅ : xs ≅H xs′) →
        Simplify₁ (p₁ ⊛ cast₁ R≡ xs≅ p₂)
      helper′ nothing nothing p₁ p₂ _ _ refl refl = result _ (
        p₁ ⊛ p₂  ∎)
      helper′ (just fs) nothing p₁ p₂ _ (result p₂′ p₂≅p₂′) refl refl
        with BSEq.empty-unique $ I.cong $ C.sound $ sym p₂≅p₂′
      helper′ (just fs) nothing p₁ p₂ _ (result p₂′ p₂≅p₂′) refl refl
        | refl = result _ (
                 p₁ ⊛ p₂   ≅⟨ [ ◌ - ◌ - ○ - ○ ] ♭ p₁ ∎ ⊛ p₂≅p₂′ ⟩
                 p₁ ⊛ p₂′  ∎)
      helper′ nothing (just xs) p₁ p₂ (result p₁′ p₁≅p₁′) _ refl refl
        with BSEq.empty-unique $ I.cong $ C.sound $ sym p₁≅p₁′
      helper′ nothing (just xs) p₁ p₂ (result p₁′ p₁≅p₁′) _ refl refl
        | refl = result _ (
                 p₁  ⊛ p₂  ≅⟨ [ ○ - ○ - ◌ - ◌ ] p₁≅p₁′ ⊛ (♭ p₂ ∎) ⟩
                 p₁′ ⊛ p₂  ∎)
      helper′ (just fs) (just xs)
              p₁ p₂ (result p₁′ p₁≅p₁′) (result p₂′ p₂≅p₂′) refl refl =
        result _ (
        p₁  ⊛ p₂   ≅⟨ [ ○ - ○ - ○ - ○ ] p₁≅p₁′ ⊛ p₂≅p₂′ ⟩
        p₁′ ⊛ p₂′  ∎)

  -- • _>>=_:

  simplify₁ (_>>=_ {xs = xs} {f = f} p₁ p₂) with simplify₁∞ p₁
  ... | result fail       p₁≅∅ = result _ (
                                 p₁   >>= p₂         ≅⟨ [ f - ○ - xs - ○ ] p₁≅∅ >>= (λ x → ♭? (p₂ x) ∎) ⟩
                                 fail >>= (♭? ∘ p₂)  ≅⟨ Monad.left-zero (♭? ∘ p₂) ⟩
                                 fail                ∎)
  ... | result (return x) p₁≅ε with simplify₁∞ (p₂ x)
  ...   | result p₂x′ p₂x≅p₂x′ = result _ (
                                 p₁       >>= p₂         ≅⟨ [ f - ○ - xs - ○ ] p₁≅ε >>= (λ x → ♭? (p₂ x) ∎) ⟩
                                 return x >>= (♭? ∘ p₂)  ≅⟨ Monad.left-identity x (♭? ∘ p₂) ⟩
                                 ♭? (p₂ x)               ≅⟨ p₂x≅p₂x′ ⟩
                                 p₂x′                    ∎)
  simplify₁ (p₁ >>= p₂) | result p₁′ p₁≅p₁′
    with forced? p₁ | forced?′ p₂
  ... | nothing | just xs = result _ (
                            p₁ >>= p₂                           ≅⟨ [ ◌ - ◌ - ○ - ○ ] ♭ p₁ ∎ >>= (λ x → simplify₁-[]-correct (p₂ x)) ⟩
                            p₁ >>= (λ x → simplify₁-[] (p₂ x))  ∎)
  ... | just f  | just xs = result _ (
                            p₁  >>= p₂                          ≅⟨ [ ○ - ○ - ○ - ○ ] p₁≅p₁′ >>=
                                                                                (λ x → Simplify₁.correct (simplify₁ (p₂ x))) ⟩
                            p₁′ >>= (λ x → Simplify₁.parser $
                                             simplify₁ (p₂ x))  ∎)
  ... | nothing | nothing = result _ (
                            p₁ >>= p₂ ∎)
  ... | just f  | nothing = result _ (
                            p₁          >>= p₂        ≅⟨ [ ○ - ○ - ◌ - ○ ] p₁≅p₁′ >>= (λ x → ♭ (p₂ x) ∎) ⟩
                            p₁′         >>= (♭ ∘ p₂)  ≅⟨ [ ○ - ○ - ○ - ◌ ] sym (Subst.correct lemma) >>= (λ x → ♭ (p₂ x) ∎) ⟩
                            cast-[] p₁′ >>= p₂        ∎)
    where
    lemma   = BSEq.empty-unique $ I.cong $ C.sound $ sym p₁≅p₁′
    cast-[] = P.subst (Parser _ _) lemma

  -- • nonempty:

  simplify₁ (nonempty p) with simplify₁ p
  ... | result fail       p≅∅  = result _ (
                                 nonempty p     ≅⟨ nonempty p≅∅ ⟩
                                 nonempty fail  ≅⟨ Nonempty.zero ⟩
                                 fail           ∎)
  ... | result (return x) p≅ε  = result _ (
                                 nonempty p           ≅⟨ nonempty p≅ε ⟩
                                 nonempty (return x)  ≅⟨ Nonempty.nonempty-return ⟩
                                 fail                 ∎)
  ... | result p′         p≅p′ = result _ (
                                 nonempty p   ≅⟨ nonempty p≅p′ ⟩
                                 nonempty p′  ∎)

  -- • cast:

  simplify₁ (cast xs₁≈xs₂ p) with simplify₁ p
  ... | result p′ p≅p′ = result _ (
                         cast xs₁≈xs₂ p  ≅⟨ Cast.correct ⟩
                         p               ≅⟨ p≅p′ ⟩
                         p′              ∎)

  private

    -- Note that if an argument parser is delayed, then simplification
    -- is not applied recursively (because this could lead to
    -- non-termination).

    simplify₁∞ : ∀ {Tok R R′ xs} {m : Maybe R′}
                 (p : ∞⟨ m ⟩Parser Tok R xs) → Simplify₁ (♭? p)
    simplify₁∞ {m = nothing} p = result _ (♭ p ∎)
    simplify₁∞ {m = just _}  p = simplify₁ p

    simplify₁-[] : ∀ {Tok R} → Parser Tok R [] → Parser Tok R []
    simplify₁-[] p = P.subst (Parser _ _) ([]-lemma p) $
                       Simplify₁.parser $ simplify₁ p

    simplify₁-[]-correct : ∀ {Tok R} (p : Parser Tok R []) →
                           p ≅P simplify₁-[] p
    simplify₁-[]-correct p =
      p                               ≅⟨ Simplify₁.correct (simplify₁ p) ⟩
      Simplify₁.parser (simplify₁ p)  ≅⟨ sym $ Subst.correct ([]-lemma p) ⟩
      simplify₁-[] p                  ∎

    []-lemma : ∀ {Tok R} (p : Parser Tok R []) →
               Simplify₁.bag (simplify₁ p) ≡ []
    []-lemma p = BSEq.empty-unique $ I.cong $ C.sound $
                   sym $ Simplify₁.correct $ simplify₁ p

------------------------------------------------------------------------
-- Deep simplification

-- The function simplify simplifies the first layer, then it traverses
-- the result and simplifies the following layers, and so on. The
-- extra traversals have been implemented to satisfy Agda's
-- termination checker; they could perhaps be avoided.
--
-- Note that simplifications in an upper layer do not get to take
-- advantage of simplifications performed in lower layers. Consider
-- ♯ p ⊛ token, for instance. If p can be simplified to fail, then one
-- might believe that ♯ p ⊛ token is simplified to fail as well.
-- However, this is only the case if p actually /computes/ to fail.
--
-- If simplification of the upper layer were dependent on complete
-- simplification of lower layers, then simplification could fail to
-- terminate. This does not mean that one cannot propagate /any/
-- information from lower layers to upper layers, though: one could
-- for instance perform partial simplification of lower layers, up to
-- a certain depth, before an upper layer is simplified.

mutual

  simplify : ∀ {Tok R xs} (p : Parser Tok R xs) →
             Parser Tok R (Simplify₁.bag $ simplify₁ p)
  simplify p = simplify↓ (Simplify₁.parser (simplify₁ p))

  private

    simplify↓ : ∀ {Tok R xs} → Parser Tok R xs → Parser Tok R xs
    simplify↓ (return x)       = return x
    simplify↓ fail             = fail
    simplify↓ token            = token
    simplify↓ (p₁ ∣ p₂)        = simplify↓ p₁ ∣ simplify↓ p₂
    simplify↓ (f <$> p)        = f <$> simplify↓ p
    simplify↓ (nonempty p)     = nonempty (simplify↓ p)
    simplify↓ (cast xs₁≈xs₂ p) = cast xs₁≈xs₂ (simplify↓ p)
    simplify↓ (p₁ ⊛ p₂)        with forced? p₁ | forced? p₂
    ... | just xs | just fs =   simplify↓      p₁  ⊛   simplify↓      p₂
    ... | just xs | nothing =   simplify↓      p₁  ⊛ ♯ simplify    (♭ p₂)
    ... | nothing | just fs = ♯ simplify    (♭ p₁) ⊛   simplify↓      p₂
    ... | nothing | nothing = ♯ simplify-[] (♭ p₁) ⊛ ♯ simplify-[] (♭ p₂)
    simplify↓ (p₁ >>= p₂)      with forced? p₁ | forced?′ p₂
    ... | just f  | just xs =   simplify↓      p₁  >>= λ x →   simplify↓      (p₂ x)
    ... | just f  | nothing =   simplify↓      p₁  >>= λ x → ♯ simplify    (♭ (p₂ x))
    ... | nothing | just xs = ♯ simplify    (♭ p₁) >>= λ x →   simplify↓      (p₂ x)
    ... | nothing | nothing = ♯ simplify-[] (♭ p₁) >>= λ x → ♯ simplify-[] (♭ (p₂ x))

    simplify-[] : ∀ {Tok R} → Parser Tok R [] → Parser Tok R []
    simplify-[] p = simplify↓ (simplify₁-[] p)

-- The simplifier is correct.

mutual

  correct : ∀ {Tok R xs} (p : Parser Tok R xs) → simplify p ≅P p
  correct p =
    simplify↓ (Simplify₁.parser $ simplify₁ p)  ≅⟨ correct↓ (Simplify₁.parser $ simplify₁ p) ⟩
    Simplify₁.parser (simplify₁ p)              ≅⟨ sym $ Simplify₁.correct $ simplify₁ p ⟩
    p                                           ∎

  private

    correct↓ : ∀ {Tok R xs} (p : Parser Tok R xs) → simplify↓ p ≅P p
    correct↓ (return x)       = return x ∎
    correct↓ fail             = fail ∎
    correct↓ token            = token ∎
    correct↓ (p₁ ∣ p₂)        = correct↓ p₁ ∣′ correct↓ p₂
    correct↓ (f <$> p)        = (λ _ → refl) <$> correct↓ p
    correct↓ (nonempty p)     = nonempty (correct↓ p)
    correct↓ (cast xs₁≈xs₂ p) = cast (correct↓ p)
    correct↓ (p₁ ⊛ p₂)        with forced? p₁ | forced? p₂
    ... | just xs | just fs = [ just (○ , ○) - just (○ , ○) ]   correct↓      p₁  ⊛   correct↓      p₂
    ... | just xs | nothing = [ just (○ , ○) - nothing      ]   correct↓      p₁  ⊛ ♯ correct    (♭ p₂)
    ... | nothing | just fs = [ nothing      - just (○ , ○) ] ♯ correct    (♭ p₁) ⊛   correct↓      p₂
    ... | nothing | nothing = [ nothing      - nothing      ] ♯ correct-[] (♭ p₁) ⊛ ♯ correct-[] (♭ p₂)
    correct↓ (p₁ >>= p₂)      with forced? p₁ | forced?′ p₂
    ... | just f  | just xs = [ just (○ , ○) - just (○ , ○) ]   correct↓      p₁  >>= λ x →   correct↓      (p₂ x)
    ... | just f  | nothing = [ just (○ , ○) - nothing      ]   correct↓      p₁  >>= λ x → ♯ correct    (♭ (p₂ x))
    ... | nothing | just xs = [ nothing      - just (○ , ○) ] ♯ correct    (♭ p₁) >>= λ x →   correct↓      (p₂ x)
    ... | nothing | nothing = [ nothing      - nothing      ] ♯ correct-[] (♭ p₁) >>= λ x → ♯ correct-[] (♭ (p₂ x))

    correct-[] : ∀ {Tok R} (p : Parser Tok R []) → simplify-[] p ≅P p
    correct-[] p =
      simplify-[] p   ≅⟨ correct↓ (simplify₁-[] p) ⟩
      simplify₁-[] p  ≅⟨ sym $ simplify₁-[]-correct p ⟩
      p               ∎

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
import MJ.Classtable.Core as Core

module MJ.Classtable.Membership {c}(Ct : Core.Classtable c) where

open Core c
open Classtable Ct

open import Prelude
open import Data.Star
open import Data.Product hiding (Σ)
open import Data.List
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.First.Membership
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Relation.Nullary.Decidable
open import Data.Maybe
open import Data.String as Str
open import Function.Equality using (Π)
open import Function.Inverse using (Inverse)

open import MJ.Types as Types

{-
We can observe that a class declares a member in a particular namespace using a
predicate Declares.
-}
Declares : Cid c → (ns : NS) → String → typing ns → Set
Declares cid ns m ty = let cl = Σ cid in (m , ty) ∈ (Class.decls cl ns)

{-
We define a notion of *declarative membership* of C as the product
of a witness that C inherits from P and a declaration in P.
-}
IsMember : Cid c → (ns : NS) → String → typing ns → Set
IsMember cid ns m ty = let C = Σ cid in ∃ λ P → Σ ⊢ cid <: P × Declares P ns m ty

{-
We can prove that Object has no members.
-}
∉Object : ∀ {ns m a} → ¬ IsMember Object ns m a
∉Object (.Object , ε , mem) rewrite Σ-Object = ¬x∈[] mem
∉Object (._ , () ◅ _ , _)

{-
And we can show that Declares and IsMember are decidable relations
-}
find-declaration : ∀ cid ns n ty → Dec (Declares cid ns n ty)
find-declaration cid ns m ty = find (Str._≟_ ×-≟ _typing-≟_) (m , ty) (Class.decls (Σ cid) ns)

find-member : ∀ cid ns n ty → Dec (IsMember cid ns n ty)
find-member cid ns n ty = helper cid ns n ty (rooted cid)
  where
    helper : ∀ cid ns n ty → Σ ⊢ cid <: Object → Dec (IsMember cid ns n ty)
    helper cid ns n ty ε = no (⊥-elim ∘ ∉Object)
    helper cid ns n ty (super ◅ p) with find-declaration cid ns n ty
    ... | yes q = yes (cid , ε , q)
    ... | no ¬q with helper _ ns n ty p
    ... | yes (pid , s , d) = yes (pid , super ◅ s , d)
    ... | no ¬r = no impossible
      where
        impossible : ¬ (IsMember cid ns n ty)
        impossible (_ , ε , d) = ¬q d
        impossible (pid , Core.super ◅ s , d) = ¬r (pid , s , d)

{-
Using said decision procedures we can formalize a notion of accessible members.
-}
AccMember : Cid c → (ns : NS) → String → typing ns → Set
AccMember cid ns n ty = True (find-member cid ns n ty)

{-
All accessible members are also declarative members, but not vice versa,
because overrides make their super inaccessible.
-}
sound : ∀ {cid ns n ty} → AccMember cid ns n ty → IsMember cid ns n ty
sound p = toWitness p

{-
Declarative members are inherited:
-}
inherit' : ∀ {C P ns m a} → Σ ⊢ C <: P → IsMember P ns m a → IsMember C ns m a
inherit' S (_ , S' , def) = -, S ◅◅ S' , def

{-
Accessible members are inherited (but may point to different definitions thanks to overrides):
-}
inherit : ∀ {m ns ty pid} cid → Σ ⊢ cid <: pid → AccMember pid ns m ty → AccMember cid ns m ty
inherit {m}{ns}{ty} cid s mb with find-member cid ns m ty
... | yes mb' = tt
... | no ¬mb = ⊥-elim (¬mb (inherit' s (sound mb)))


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

module rings-with-properties where

import rings
open rings public

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

{- Commutative rings -}

is-commutative-Ring :
  { l : Level} → Ring l → UU l
is-commutative-Ring R =
  (x y : type-Ring R) → Id (mul-Ring R x y) (mul-Ring R y x)

is-prop-is-commutative-Ring :
  { l : Level} (R : Ring l) → is-prop (is-commutative-Ring R)
is-prop-is-commutative-Ring R =
  is-prop-Π
    ( λ x →
      is-prop-Π
      ( λ y →
        is-set-type-Ring R (mul-Ring R x y) (mul-Ring R y x)))

Comm-Ring :
  ( l : Level) → UU (lsuc l)
Comm-Ring l = Σ (Ring l) is-commutative-Ring

ring-Comm-Ring :
  { l : Level} → Comm-Ring l → Ring l
ring-Comm-Ring = pr1

is-commutative-Comm-Ring :
  { l : Level} (R : Comm-Ring l) → is-commutative-Ring (ring-Comm-Ring R)
is-commutative-Comm-Ring = pr2

hom-Comm-Ring :
  { l1 l2 : Level} → Comm-Ring l1 → Comm-Ring l2 → UU (l1 ⊔ l2)
hom-Comm-Ring R1 R2 = hom-Ring (ring-Comm-Ring R1) (ring-Comm-Ring R2)

iso-Comm-Ring :
  { l1 l2 : Level} → Comm-Ring l1 → Comm-Ring l2 → UU (l1 ⊔ l2)
iso-Comm-Ring R1 R2 = iso-Ring (ring-Comm-Ring R1) (ring-Comm-Ring R2)

is-contr-total-iso-Comm-Ring :
  { l1 : Level} (R1 : Comm-Ring l1) →
  is-contr (Σ (Comm-Ring l1) (iso-Comm-Ring R1))
is-contr-total-iso-Comm-Ring R1 =
  is-contr-total-Eq-substructure
    ( is-contr-total-iso-Ring (ring-Comm-Ring R1))
    ( is-prop-is-commutative-Ring)
    ( ring-Comm-Ring R1)
    ( id-iso-Ring (ring-Comm-Ring R1))
    ( is-commutative-Comm-Ring R1)

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

{- Division rings -}

zero-neq-one-Ring :
  { l : Level} → Ring l → UU l
zero-neq-one-Ring R = ¬ (Id (zero-Ring R) (unit-Ring R))

has-left-inverse-Ring :
  { l : Level} (R : Ring l) → type-Ring R → UU l
has-left-inverse-Ring R x =
  Σ (type-Ring R) (λ y → Id (mul-Ring R y x) (unit-Ring R))

has-right-inverse-Ring :
  {l : Level} (R : Ring l) → type-Ring R → UU l
has-right-inverse-Ring R x =
  Σ (type-Ring R) (λ y → Id (mul-Ring R x y) (unit-Ring R))

has-two-sided-inverse-Ring :
  {l : Level} (R : Ring l) → type-Ring R → UU l
has-two-sided-inverse-Ring R x =
  ( has-left-inverse-Ring R x) × (has-right-inverse-Ring R x)

is-invertible-Ring :
  {l : Level} (R : Ring l) → type-Ring R → UU l
is-invertible-Ring R x =
  Σ ( type-Ring R)
    ( λ y →
      Id (mul-Ring R y x) (unit-Ring R) ×
      Id (mul-Ring R x y) (unit-Ring R))

is-division-Ring :
  { l : Level} → Ring l → UU l
is-division-Ring R =
  (zero-neq-one-Ring R) ×
  ((x : type-Ring R) → ¬ (Id (zero-Ring R) x) → is-invertible-Ring R x)

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

{- Fields -}

is-field-Comm-Ring :
  { l : Level} → Comm-Ring l → UU l
is-field-Comm-Ring R = is-division-Ring (ring-Comm-Ring R)

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


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

-- Should be rejected:
data Eq (A : Set) : (x y : A) → Set where
  refl : (x y : A) → Eq A x y

{-# BUILTIN EQUALITY Eq #-}

-- Expected error:
-- Wrong type of constructor of BUILTIN EQUALITY
-- when checking the pragma BUILTIN EQUALITY Eq

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Reasoning about _⇔_
--
-- NOTE: we don’t use Relation.Binary.IsEquivalence here, since we’re reasoning
-- about a heterogeneous equivalence relation (i.e., the types of the operands
-- of _⇔_, which are themselves types, can be of different levels). In the proof
-- of Chapter₁₅.problem₁, the fact that _⇔_ is heterogeneous is actually used,
-- so we cannot use a homogeneous version of _⇔_.
------------------------------------------------------------------------

module Function.Equivalence.Reasoning where

open import Function using (_⇔_)
open import Function.Construct.Composition using (_∘-⇔_) public
open import Function.Construct.Identity using (id-⇔) public
open import Function.Construct.Symmetry using (sym-⇔) public
open import Level using (Level)

private
  variable
    a b c : Level

infix  1 begin_
infixr 2 _⇔⟨⟩_ step-⇔ step-⇔˘
infix  3 _∎

begin_ : {A : Set a} {B : Set b} → A ⇔ B → A ⇔ B
begin A⇔B = A⇔B

_∎ : (A : Set a) → A ⇔ A
_∎ = id-⇔

_⇔⟨⟩_ : (A : Set a) {B : Set b} → A ⇔ B → A ⇔ B
A ⇔⟨⟩ A⇔B = A⇔B

step-⇔ : (A : Set a) {B : Set b} {C : Set c} → A ⇔ B → B ⇔ C → A ⇔ C
step-⇔ A = _∘-⇔_

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

step-⇔˘ : (A : Set a) {B : Set b} {C : Set c} → B ⇔ A → B ⇔ C → A ⇔ C
step-⇔˘ A B⇔A B⇔C = A ⇔⟨ sym-⇔ B⇔A ⟩ B⇔C

syntax step-⇔˘ A B⇔A B⇔C = A ⇔˘⟨ B⇔A ⟩ B⇔C

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic