text:
module Metaprog2016 where

open import Data.List using (List) renaming ([] to ⌀)
open import Data.Maybe using (Maybe)
open import Data.Product using (_×_)
open import Data.Unit using () renaming (⊤ to 𝟙)

-- TOWARDS INTENSIONAL ANALYSIS OF SYNTAX
--
-- Miëtek Bak
-- mietek@bak.io
--
-- http://github.com/mietek/metaprog2016
--
-- International Summer School on Metaprogramming
-- Robinson College, Cambridge, 8th to 12th August 2016

-- Consider a basic fragment of intuitionistic modal logic S4 (IS4).

data Type : Set where
  _▻_ : Type → Type → Type
  _∧_ : Type → Type → Type
  ⊤  : Type
  □_  : Type → Type

postulate
  _⊢_ : List Type → Type → Set

-- IS4 provides the logical foundations for MetaML.

-- Sheard (2001) reminds us that MetaML only allows syntax to be constructed
-- and executed at runtime.  Observation and decomposition is not supported.
--
-- “Accomplishments and research challenges in meta-programming”
-- http://dx.doi.org/10.1007/3-540-44806-3_2

postulate
  •     : Type
  yes   : ∀ {Γ}   → Γ ⊢ •
  no    : ∀ {Γ}   → Γ ⊢ •
  isApp : ∀ {Γ A} → Γ ⊢ ((□ A) ▻ •)

-- Has anyone built a typed system supporting intensional analysis of syntax?

-- I don’t know, but Gabbay and Nanevski (2012) come close.  They give a
-- Tarski-style semantics for IS4, reading “□ A” as “closed syntax of type A”.
--
-- “Denotation of contextual modal type theory: Syntax and meta-programming”
-- http://dx.doi.org/10.1016/j.jal.2012.07.002

module GabbayNanevski2012 where
  ⊨_ : Type → Set
  ⊨ (A ▻ B) = ⊨ A → ⊨ B
  ⊨ (A ∧ B) = (⊨ A) × (⊨ B)
  ⊨ ⊤      = 𝟙
  ⊨ (□ A)   = (⌀ ⊢ A) × (⊨ A)

-- Can we construct a proof of completeness with respect to this semantics
-- and obtain normalisation by evaluation (NbE) for IS4?

-- Yes, we can!  As long as we also take from Coquand and Dybjer (1997).
--
-- “Intuitionistic model constructions and normalization proofs”
-- http://dx.doi.org/10.1017/S0960129596002150

module CoquandDybjer1997GabbayNanevski2012 where
  ⊨_ : Type → Set
  ⊨ (A ▻ B) = (⌀ ⊢ (A ▻ B)) × (⊨ A → ⊨ B)
  ⊨ (A ∧ B) = (⊨ A) × (⊨ B)
  ⊨ ⊤      = 𝟙
  ⊨ (□ A)   = (⌀ ⊢ A) × (⊨ A)

-- Could we perhaps read “□ A” as “open syntax of type A”?

-- I don’t know, but I’ve had an idea about that...

postulate
  _⊆_ : List Type → List Type → Set

module ??? where
  _⊨_ : List Type → Type → Set
  Δ ⊨ (A ▻ B) = ∀ {Δ′} → Δ ⊆ Δ′ → Δ′ ⊨ A → Δ′ ⊨ B
  Δ ⊨ (A ∧ B) = (Δ ⊨ A) × (Δ ⊨ B)
  Δ ⊨ ⊤      = 𝟙
  Δ ⊨ (□ A)   = ∀ {Δ′} → Δ ⊆ Δ′ → (Δ′ ⊢ A) × (Δ′ ⊨ A)

-- Does this look suspiciously like a Kripke-style possible worlds semantics?

-- Yes, it does!  We can find one of these in Alechina et al. (2001).
--
-- “Categorical and Kripke semantics for constructive S4 modal logic”
-- http://dx.doi.org/10.1007/3-540-44802-0_21

postulate
  World : Set
  _≤_   : World → World → Set
  _R_   : World → World → Set

module AlechinaMendlerDePaivaRitter2001 where
  _⊩_ : World → Type → Set
  w ⊩ (A ▻ B) = ∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B
  w ⊩ (A ∧ B) = (w ⊩ A) × (w ⊩ B)
  w ⊩ ⊤      = 𝟙
  w ⊩ (□ A)   = ∀ {w′} → w ≤ w′ → ∀ {v′} → w′ R v′ → v′ ⊩ A

-- Has anyone constructed a proof of completeness with respect to a
-- Kripke-style semantics for IS4?

-- I haven’t found one, and I’ve tried five.

--           v′      w″  →   v″              w″
--           ◌───R───●   →   ◌───────R───────●
--           │           →   │
--           ≤  ξ′,ζ′    →   │
--   v       │           →   │
--   ◌───R───●           →   ≤
--   │       w′          →   │
--   ≤  ξ,ζ              →   │
--   │                   →   │
--   ●                   →   ●
--   w                   →   w

-- How do we go from being able to talk about open syntax to being able
-- to intensionally analyse syntax at runtime?

-- I don’t know, but I’ve noticed a funny coincidence...
--
-- Work in progress:
-- http://github.com/mietek/hilbert-gentzen

-- FIN


text:
module _ where

record Structure : Set1 where
  infixl 20 _×_
  infix   8 _⟶_
  infixl 20 _,_
  infixr 40 _∘_

  infix 5 _~_

  field
    Type : Set
    _×_  : Type → Type → Type

    _⟶_ : Type → Type → Set
    _∘_ : ∀ {X Y Z} → Y ⟶ Z → X ⟶ Y → X ⟶ Z
    _,_ : ∀ {X A B} → X ⟶ A → X ⟶ B → X ⟶ A × B
    π₁  : ∀ {A B} → A × B ⟶ A
    π₂  : ∀ {A B} → A × B ⟶ B
    Op3 : ∀ {X} → X × X × X ⟶ X

    _~_ : ∀ {X Y} → X ⟶ Y → X ⟶ Y → Set

record Map {{C : Structure}} {{D : Structure}} : Set1 where
  open Structure {{...}}
  field
    Ty⟦_⟧ : Structure.Type C → Structure.Type D
    Tm⟦_⟧ : ∀ {X A} → X ⟶ A → Ty⟦ X ⟧ ⟶ Ty⟦ A ⟧

    ×-inv : ∀ {X A} → Ty⟦ X ⟧ × Ty⟦ A ⟧ ⟶ Ty⟦ X × A ⟧

    ⟦Op3⟧ : ∀ {X} → Tm⟦ Op3 {X = X} ⟧ ∘ ×-inv ∘ (×-inv ∘ (π₁ ∘ π₁ , π₂ ∘ π₁) , π₂) ~ Op3

ext: agda

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2016-01-19, issue raised by Twey
-- {-# OPTIONS -v 10 #-}

{-# OPTIONS --allow-unsolved-metas #-}

Rel : Set → Set₁
Rel A = A → A → Set

record Category : Set₁ where
  field
    Obj : Set
    _⇒_ : Rel Obj -- unfolding the definition of Rel removes the error

record Product (C : Category) (A B : Category.Obj C) : Set where
  field
    A×B : Category.Obj C

postulate
  anything : ∀{a}{A : Set a} → A

trivial : ∀ {C} → Category.Obj C → Set
trivial _ = anything

map-obj : ∀ {P : _} → trivial (Product.A×B P) -- Note: hole _ cannot be filled
map-obj = anything

{- Error thrown during printing open metas:
piApply
  t    = Rel _24   Def Issue1783.Rel [Apply []r(MetaV (MetaId 24) [])]}
  args = @0        [[]r{Var 0 []}]
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:382
-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-

This file introduces the "powerset" of a type in the style of
Escardó's lecture notes:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#propositionalextensionality

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Powerset where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence using (hPropExt)

open import Cubical.Data.Sigma

private
  variable
    ℓ : Level
    X : Type ℓ

ℙ : Type ℓ → Type (ℓ-suc ℓ)
ℙ X = X → hProp _

infix 5 _∈_

_∈_ : {X : Type ℓ} → X → ℙ X → Type ℓ
x ∈ A = ⟨ A x ⟩

_⊆_ : {X : Type ℓ} → ℙ X → ℙ X → Type ℓ
A ⊆ B = ∀ x → x ∈ A → x ∈ B

∈-isProp : (A : ℙ X) (x : X) → isProp (x ∈ A)
∈-isProp A = snd ∘ A

⊆-isProp : (A B : ℙ X) → isProp (A ⊆ B)
⊆-isProp A B = isPropΠ2 (λ x _ → ∈-isProp B x)

⊆-refl : (A : ℙ X) → A ⊆ A
⊆-refl A x = idfun (x ∈ A)

⊆-refl-consequence : (A B : ℙ X) → A ≡ B → (A ⊆ B) × (B ⊆ A)
⊆-refl-consequence A B p = subst (A ⊆_) p (⊆-refl A)
                          , subst (B ⊆_) (sym p) (⊆-refl B)

⊆-extensionality : (A B : ℙ X) → (A ⊆ B) × (B ⊆ A) → A ≡ B
⊆-extensionality A B (φ , ψ) =
  funExt (λ x → TypeOfHLevel≡ 1 (hPropExt (A x .snd) (B x .snd) (φ x) (ψ x)))

powersets-are-sets : isSet (ℙ X)
powersets-are-sets = isSetΠ (λ _ → isSetHProp)

⊆-extensionalityEquiv : (A B : ℙ X) → (A ⊆ B) × (B ⊆ A) ≃ (A ≡ B)
⊆-extensionalityEquiv A B = isoToEquiv (iso (⊆-extensionality A B)
                                            (⊆-refl-consequence A B)
                                            (λ _ → powersets-are-sets A B _ _)
                                            (λ _ → isPropΣ (⊆-isProp A B) (λ _ → ⊆-isProp B A) _ _))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Issue2792.Safe where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Algebra (Σ : Signature) where

open import Level using (Level; _⊔_; suc)
open import Data.Vec using (Vec)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise)
open import Relation.Binary using (Setoid; Rel; IsEquivalence)

private
  variable
    a ℓ : Level

module _ (S : Setoid a ℓ) where

  open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_)

  open Setoid S renaming (Carrier to A)

  Interpretation : Set a
  Interpretation = ∀ {arity} → (f : ops Σ arity) → Vec A arity → A

  Congruence : Interpretation → Set (a ⊔ ℓ)
  Congruence ⟦_⟧ = ∀ {arity}
                   → (f : ops Σ arity)
                   → ∀ {xs ys} → Pointwise _≈_ xs ys → ⟦ f ⟧ xs ≈ ⟦ f ⟧ ys

  record IsAlgebra : Set (a ⊔ ℓ) where
    field
      ⟦_⟧     : Interpretation
      ⟦⟧-cong : Congruence ⟦_⟧

record Algebra : Set (suc a ⊔ suc ℓ) where
  constructor algebra
  field
    ∥_∥/≈           : Setoid a ℓ
    ∥_∥/≈-isAlgebra : IsAlgebra ∥_∥/≈

  ∥_∥ : Set a
  ∥_∥ = Setoid.Carrier ∥_∥/≈

  infix 10 _⟦_⟧_

  _⟦_⟧_ : Interpretation (∥_∥/≈)
  _⟦_⟧_ = IsAlgebra.⟦_⟧ ∥_∥/≈-isAlgebra

  _⟦_⟧-cong : Congruence (∥_∥/≈) (_⟦_⟧_)
  _⟦_⟧-cong = IsAlgebra.⟦⟧-cong ∥_∥/≈-isAlgebra

  ≈[_] : Rel ∥_∥ ℓ
  ≈[_] = Setoid._≈_ ∥_∥/≈

  ≈[_]-isEquivalence : IsEquivalence ≈[_]
  ≈[_]-isEquivalence = Setoid.isEquivalence ∥_∥/≈

open Algebra public

infix 5 ≈-syntax

≈-syntax : (A : Algebra {a} {ℓ}) → ∥ A ∥ → ∥ A ∥ → Set ℓ
≈-syntax A x y = Setoid._≈_ ∥ A ∥/≈ x y

syntax ≈-syntax A x y = x =[ A ] y

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-
  This type ℕ₋₂ was originally used as the index to n-truncation in order to
   be consistent with the notation in the HoTT book. However, ℕ was already
   being used as an analogous index in Foundations.HLevels, and it became
   clear that having two different indexing schemes for truncation levels was
   very inconvenient. In the end, having slightly nicer notation was not worth
   the hassle of having to use this type everywhere where truncation levels
   were needed. So for this library, use the type `HLevel = ℕ` instead.

  See the discussions below for more context:
   - https://github.com/agda/cubical/issues/266
   - https://github.com/agda/cubical/pull/238
-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Experiments.NatMinusTwo where

open import Cubical.Experiments.NatMinusTwo.Base public

open import Cubical.Experiments.NatMinusTwo.Properties public

open import Cubical.Experiments.NatMinusTwo.ToNatMinusOne using (1+_; ℕ₋₁→ℕ₋₂; -1+Path) public


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- Mainly *properties* of isomorphisms, and a lot of other things too

-- TODO: split things up more semantically?

module Categories.Morphism.Isomorphism {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level using (_⊔_)
open import Function using (flip)

open import Data.Product using (_,_)
open import Relation.Binary using (Rel; _Preserves_⟶_; IsEquivalence)
open import Relation.Binary.Construct.Closure.Transitive
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

import Categories.Category.Construction.Core as Core
open import Categories.Category.Groupoid using (IsGroupoid)
import Categories.Category.Groupoid.Properties as GroupoidProps
import Categories.Morphism as Morphism
import Categories.Morphism.Properties as MorphismProps
import Categories.Morphism.IsoEquiv as IsoEquiv
import Categories.Category.Construction.Path as Path

open Core 𝒞 using (Core; Core-isGroupoid; CoreGroupoid)
open Morphism 𝒞
open MorphismProps 𝒞
open IsoEquiv 𝒞 using (_≃_; ⌞_⌟)
open Path 𝒞

import Categories.Morphism.Reasoning as MR

open Category 𝒞

private
  module MCore where
    open IsGroupoid    Core-isGroupoid public
    open GroupoidProps CoreGroupoid public
    open MorphismProps Core public
    open Morphism      Core public
    open Path          Core public

  variable
    A B C D E F : Obj

open MCore using () renaming (_∘_ to _∘ᵢ_) public

CommutativeIso = IsGroupoid.CommutativeSquare Core-isGroupoid

--------------------
-- Also stuff about transitive closure

∘ᵢ-tc : A [ _≅_ ]⁺ B → A ≅ B
∘ᵢ-tc = MCore.∘-tc

infix 4 _≃⁺_
_≃⁺_ : Rel (A [ _≅_ ]⁺ B) _
_≃⁺_ = MCore._≈⁺_

TransitiveClosure : Category _ _ _
TransitiveClosure = MCore.Path

--------------------
-- some infrastructure setup in order to say something about morphisms and isomorphisms
module _ where
  private
    data IsoPlus : A [ _⇒_ ]⁺ B → Set (o ⊔ ℓ ⊔ e) where
      [_]     : {f : A ⇒ B} {g : B ⇒ A} → Iso f g → IsoPlus [ f ]
      _∼⁺⟨_⟩_ : ∀ A {f⁺ : A [ _⇒_ ]⁺ B} {g⁺ : B [ _⇒_ ]⁺ C} → IsoPlus f⁺ → IsoPlus g⁺ → IsoPlus (_ ∼⁺⟨ f⁺ ⟩ g⁺)

  open _≅_

  ≅⁺⇒⇒⁺ : A [ _≅_ ]⁺ B → A [ _⇒_ ]⁺ B
  ≅⁺⇒⇒⁺ [ f ]            = [ from f ]
  ≅⁺⇒⇒⁺ (_ ∼⁺⟨ f⁺ ⟩ f⁺′) = _ ∼⁺⟨ ≅⁺⇒⇒⁺ f⁺ ⟩ ≅⁺⇒⇒⁺ f⁺′

  reverse : A [ _≅_ ]⁺ B → B [ _≅_ ]⁺ A
  reverse [ f ]            = [ ≅.sym f ]
  reverse (_ ∼⁺⟨ f⁺ ⟩ f⁺′) = _ ∼⁺⟨ reverse f⁺′ ⟩ reverse f⁺

  reverse⇒≅-sym : (f⁺ : A [ _≅_ ]⁺ B) → ∘ᵢ-tc (reverse f⁺) ≡ ≅.sym (∘ᵢ-tc f⁺)
  reverse⇒≅-sym [ f ]            = ≡.refl
  reverse⇒≅-sym (_ ∼⁺⟨ f⁺ ⟩ f⁺′)  = ≡.cong₂ (Morphism.≅.trans 𝒞) (reverse⇒≅-sym f⁺′) (reverse⇒≅-sym f⁺)

  TransitiveClosure-groupoid : IsGroupoid TransitiveClosure
  TransitiveClosure-groupoid = record
    { _⁻¹ = reverse
    ; iso = λ {_ _ f⁺} → record { isoˡ = isoˡ′ f⁺ ; isoʳ = isoʳ′ f⁺ }
    }
    where
      open MCore.HomReasoning

      isoˡ′ : (f⁺ : A [ _≅_ ]⁺ B) → ∘ᵢ-tc (reverse f⁺) ∘ᵢ ∘ᵢ-tc f⁺ ≃ ≅.refl
      isoˡ′ f⁺ = begin
          ∘ᵢ-tc (reverse f⁺) ∘ᵢ ∘ᵢ-tc f⁺
        ≡⟨ ≡.cong (_∘ᵢ ∘ᵢ-tc f⁺) (reverse⇒≅-sym f⁺) ⟩
          ≅.sym (∘ᵢ-tc f⁺) ∘ᵢ ∘ᵢ-tc f⁺
        ≈⟨ MCore.iso.isoˡ ⟩
          ≅.refl
        ∎

      isoʳ′ : (f⁺ : A [ _≅_ ]⁺ B) → ∘ᵢ-tc f⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺) ≃ ≅.refl
      isoʳ′ f⁺ = begin
          ∘ᵢ-tc f⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺)
        ≡⟨ ≡.cong (∘ᵢ-tc f⁺ ∘ᵢ_) (reverse⇒≅-sym f⁺) ⟩
          ∘ᵢ-tc f⁺ ∘ᵢ ≅.sym (∘ᵢ-tc f⁺)
        ≈⟨ MCore.iso.isoʳ ⟩
          ≅.refl
        ∎

  from-∘ᵢ-tc : (f⁺ : A [ _≅_ ]⁺ B) → from (∘ᵢ-tc f⁺) ≡ ∘-tc (≅⁺⇒⇒⁺ f⁺)
  from-∘ᵢ-tc [ f ]            = ≡.refl
  from-∘ᵢ-tc (_ ∼⁺⟨ f⁺ ⟩ f⁺′) = ≡.cong₂ _∘_ (from-∘ᵢ-tc f⁺′) (from-∘ᵢ-tc f⁺)

  ≅*⇒⇒*-cong : ≅⁺⇒⇒⁺ {A} {B} Preserves _≃⁺_ ⟶ _≈⁺_
  ≅*⇒⇒*-cong {_} {_} {f⁺} {g⁺} f⁺≃⁺g⁺ = begin
    ∘-tc (≅⁺⇒⇒⁺ f⁺)  ≡˘⟨ from-∘ᵢ-tc f⁺ ⟩
    from (∘ᵢ-tc f⁺)  ≈⟨ _≃_.from-≈ f⁺≃⁺g⁺ ⟩
    from (∘ᵢ-tc g⁺)  ≡⟨ from-∘ᵢ-tc g⁺ ⟩
    ∘-tc (≅⁺⇒⇒⁺ g⁺)  ∎
    where open HomReasoning

  ≅-shift : ∀ {f⁺ : A [ _≅_ ]⁺ B} {g⁺ : B [ _≅_ ]⁺ C} {h⁺ : A [ _≅_ ]⁺ C} →
              (_ ∼⁺⟨ f⁺ ⟩  g⁺) ≃⁺ h⁺ → g⁺ ≃⁺ (_ ∼⁺⟨ reverse f⁺ ⟩ h⁺)
  ≅-shift {f⁺ = f⁺} {g⁺ = g⁺} {h⁺ = h⁺} eq = begin
    ∘ᵢ-tc g⁺                                      ≈⟨ introʳ (I.isoʳ f⁺) ⟩
    ∘ᵢ-tc g⁺ ∘ᵢ (∘ᵢ-tc f⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺))  ≈⟨ pullˡ eq ⟩
    ∘ᵢ-tc h⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺)                ∎
    where
      open MCore.HomReasoning
      open MR Core
      module I {A B} (f⁺ : A [ _≅_ ]⁺ B) = Morphism.Iso (IsGroupoid.iso TransitiveClosure-groupoid {f = f⁺})

  lift : ∀ {f⁺ : A [ _⇒_ ]⁺ B} → IsoPlus f⁺ → A [ _≅_ ]⁺ B
  lift [ iso ]            = [ record
    { from = _
    ; to   = _
    ; iso  = iso
    } ]
  lift (_ ∼⁺⟨ iso ⟩ iso′) = _ ∼⁺⟨ lift iso ⟩ lift iso′

  reduce-lift : ∀ {f⁺ : A [ _⇒_ ]⁺ B} (f′ : IsoPlus f⁺) → from (∘ᵢ-tc (lift f′)) ≡ ∘-tc f⁺
  reduce-lift [ f ]           = ≡.refl
  reduce-lift (_ ∼⁺⟨ f′ ⟩ f″) = ≡.cong₂ _∘_ (reduce-lift f″) (reduce-lift f′)

  lift-cong : ∀ {f⁺ g⁺ : A [ _⇒_ ]⁺ B} (f′ : IsoPlus f⁺) (g′ : IsoPlus g⁺) →
              f⁺ ≈⁺ g⁺ → lift f′ ≃⁺ lift g′
  lift-cong {_} {_} {f⁺} {g⁺} f′ g′ eq = ⌞ from-≈′ ⌟
    where
      open HomReasoning

      from-≈′ : from (∘ᵢ-tc (lift f′)) ≈ from (∘ᵢ-tc (lift g′))
      from-≈′ = begin
        from (∘ᵢ-tc (lift f′))  ≡⟨ reduce-lift f′ ⟩
        ∘-tc f⁺                 ≈⟨ eq ⟩
        ∘-tc g⁺                 ≡˘⟨ reduce-lift g′ ⟩
        from (∘ᵢ-tc (lift g′))  ∎

  lift-triangle : {f : A ⇒ B} {g : C ⇒ A} {h : C ⇒ B} {k : B ⇒ C} {i : B ⇒ A} {j : A ⇒ C} →
    f ∘ g ≈ h → (f′ : Iso f i) → (g′ : Iso g j) → (h′ : Iso h k) →
    lift (_ ∼⁺⟨ [ g′ ] ⟩ [ f′ ]) ≃⁺ lift [ h′ ]
  lift-triangle eq f′ g′ h′ = lift-cong (_ ∼⁺⟨ [ g′ ] ⟩ [ f′ ]) [ h′ ] eq

  lift-square : {f : A ⇒ B} {g : C ⇒ A} {h : D ⇒ B} {i : C ⇒ D} {j : D ⇒ C} {a : B ⇒ A} {b : A ⇒ C} {c : B ⇒ D} →
    f ∘ g ≈ h ∘ i → (f′ : Iso f a) → (g′ : Iso g b) → (h′ : Iso h c) → (i′ : Iso i j) →
    lift (_ ∼⁺⟨ [ g′ ] ⟩ [ f′ ]) ≃⁺ lift (_ ∼⁺⟨ [ i′ ] ⟩ [ h′ ])
  lift-square eq f′ g′ h′ i′ = lift-cong (_ ∼⁺⟨ [ g′ ] ⟩ [ f′ ]) (_ ∼⁺⟨ [ i′ ] ⟩ [ h′ ]) eq

  lift-pentagon : {f : A ⇒ B} {g : C ⇒ A} {h : D ⇒ C} {i : E ⇒ B} {j : D ⇒ E} {l : E ⇒ D}
                  {a : B ⇒ A} {b : A ⇒ C} {c : C ⇒ D} {d : B ⇒ E} →
    f ∘ g ∘ h ≈ i ∘ j →
    (f′ : Iso f a) → (g′ : Iso g b) → (h′ : Iso h c) → (i′ : Iso i d) → (j′ : Iso j l) →
    lift (_ ∼⁺⟨ _ ∼⁺⟨ [ h′ ] ⟩ [ g′ ] ⟩ [ f′ ]) ≃⁺ lift (_ ∼⁺⟨ [ j′ ] ⟩ [ i′ ])
  lift-pentagon eq f′ g′ h′ i′ j′ = lift-cong (_ ∼⁺⟨ _ ∼⁺⟨ [ h′ ] ⟩ [ g′ ] ⟩ [ f′ ]) (_ ∼⁺⟨ [ j′ ] ⟩ [ i′ ]) eq

module _ where
  open _≅_

  -- projecting isomorphism commutations to morphism commutations

  project-triangle : {g : A ≅ B} {f : C ≅ A} {h : C ≅ B} → g ∘ᵢ f ≃ h → from g ∘ from f ≈ from h
  project-triangle = _≃_.from-≈

  project-square : {g : A ≅ B} {f : C ≅ A} {i : D ≅ B} {h : C ≅ D} → g ∘ᵢ f ≃ i ∘ᵢ h → from g ∘ from f ≈ from i ∘ from h
  project-square = _≃_.from-≈

  -- direct lifting from morphism commutations to isomorphism commutations

  lift-triangle′ : {f : A ≅ B} {g : C ≅ A} {h : C ≅ B} → from f ∘ from g ≈ from h → f ∘ᵢ g ≃ h
  lift-triangle′ = ⌞_⌟

  lift-square′ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ B} {i : C ≅ D} → from f ∘ from g ≈ from h ∘ from i → f ∘ᵢ g ≃ h ∘ᵢ i
  lift-square′ = ⌞_⌟

  lift-pentagon′ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ C} {i : E ≅ B} {j : D ≅ E} →
                   from f ∘ from g ∘ from h ≈ from i ∘ from j → f ∘ᵢ g ∘ᵢ h ≃ i ∘ᵢ j
  lift-pentagon′ = ⌞_⌟

  open MR Core
  open MCore using (_⁻¹)
  open MCore.HomReasoning
  open MR.GroupoidR _ Core-isGroupoid

  squares×≃⇒≃ : {f f′ : A ≅ B} {g : A ≅ C} {h : B ≅ D} {i i′ : C ≅ D} →
                CommutativeIso f g h i → CommutativeIso f′ g h i′ → i ≃ i′ → f ≃ f′
  squares×≃⇒≃ sq₁ sq₂ eq = MCore.isos×≈⇒≈ eq helper₁ (MCore.≅.sym helper₂) sq₁ sq₂
    where
      helper₁ = record { iso = MCore.iso }
      helper₂ = record { iso = MCore.iso }

  -- imagine a triangle prism, if all the sides and the top face commute, the bottom face commute.
  triangle-prism : {i′ : A ≅ B} {f′ : C ≅ A} {h′ : C ≅ B} {i : D ≅ E} {j : D ≅ A}
    {k : E ≅ B} {f : F ≅ D} {g : F ≅ C} {h : F ≅ E} →
    i′ ∘ᵢ f′ ≃ h′ →
    CommutativeIso i j k i′ → CommutativeIso f g j f′ → CommutativeIso h g k h′ →
    i ∘ᵢ f ≃ h
  triangle-prism {i′ = i′} {f′} {_} {i} {_} {k} {f} {g} {_} eq sq₁ sq₂ sq₃ =
    squares×≃⇒≃ glued sq₃ eq
    where
      glued : CommutativeIso (i ∘ᵢ f) g k (i′ ∘ᵢ f′)
      glued = sym (glue (sym sq₁) (sym sq₂))

  elim-triangleˡ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ C} {i : D ≅ B} {j : D ≅ A} →
                   f ∘ᵢ g ∘ᵢ h ≃ i → f ∘ᵢ j ≃ i → g ∘ᵢ h ≃ j
  elim-triangleˡ perim tri = MCore.mono _ _ (perim ○ ⟺ tri)

  elim-triangleˡ′ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ C} {i : D ≅ B} {j : C ≅ B} →
                    f ∘ᵢ g ∘ᵢ h ≃ i → j ∘ᵢ h ≃ i → f ∘ᵢ g ≃ j
  elim-triangleˡ′ {f = f} {g} {h} {i} {j} perim tri = MCore.epi _ _ ( begin
    (f ∘ᵢ g) ∘ᵢ h ≈⟨ MCore.assoc ⟩
    f ∘ᵢ g ∘ᵢ h   ≈⟨ perim ⟩
    i             ≈˘⟨ tri ⟩
    j ∘ᵢ h        ∎ )

  cut-squareʳ : {g : A ≅ B} {f : A ≅ C} {h : B ≅ D} {i : C ≅ D} {j : B ≅ C} →
                CommutativeIso g f h i → i ∘ᵢ j ≃ h → j ∘ᵢ g ≃ f
  cut-squareʳ {g = g} {f = f} {h = h} {i = i} {j = j} sq tri = begin
    j ∘ᵢ g            ≈⟨ switch-fromtoˡ′ {f = i} {h = j} {k = h} tri ⟩∘⟨ refl ⟩
    (i ⁻¹ ∘ᵢ h) ∘ᵢ g  ≈⟨ MCore.assoc ⟩
    i ⁻¹ ∘ᵢ h ∘ᵢ g    ≈˘⟨ switch-fromtoˡ′ {f = i} {h = f} {k = h ∘ᵢ g} (sym sq) ⟩
    f                 ∎

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Generic.Test.Data.Lift where

open import Generic.Main as Main hiding (Lift; lift; lower)

Lift : ∀ {α} β -> Set α -> Set (α ⊔ β)
Lift = readData Main.Lift

pattern lift x = !#₀ (relv x , lrefl)

lower : ∀ {α} {A : Set α} β -> Lift β A -> A
lower β (lift x) = x

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
------------------------------------------------------------------------
-- Extra lemmas about substitutions
------------------------------------------------------------------------

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

module Data.Fin.Substitution.ExtraLemmas where

open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Vec using (Vec; _∷_; lookup; map)
open import Data.Vec.Properties using (map-cong; map-∘; lookup-map)
open import Data.Vec.Relation.Unary.All hiding (lookup; map)
open import Function using (_∘_; _$_; flip)
open import Level using (_⊔_) renaming (zero to lzero; suc to lsuc)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; ε; _◅_; _▻_)
open import Relation.Binary.PropositionalEquality as PropEq hiding (subst)
open PropEq.≡-Reasoning
open import Relation.Unary using (Pred)

-- Simple extension of substitutions.
--
-- FIXME: this should go into Data.Fin.Substitution.
record Extension {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
  infixr 5 _/∷_

  field weaken : ∀ {n} → T n → T (suc n)  -- Weakens Ts.

  -- Iterated weakening of types.
  weaken⋆ : ∀ m {n} → T n → T (m + n)
  weaken⋆ zero    t = t
  weaken⋆ (suc m) t = weaken (weaken⋆ m t)

  -- Extension.
  _/∷_ : ∀ {m n} → T (suc n) → Sub T m n → Sub T (suc m) (suc n)
  t /∷ ρ = t ∷ map weaken ρ

-- Helper module
module SimpleExt {ℓ} {T : Pred ℕ ℓ} (simple : Simple T) where
  open Simple simple public

  extension : Extension T
  extension = record { weaken = weaken }
  open Extension extension public hiding (weaken)

-- An generalized version of Data.Fin.Lemmas.Lemmas₀
--
-- FIXME: this should go into Data.Fin.Substitution.Lemmas.
module ExtLemmas₀ {ℓ} {T : Pred ℕ ℓ} (lemmas₀ : Lemmas₀ T) where
  open Data.Fin using (lift; raise)

  open Lemmas₀   lemmas₀ public hiding (lookup-map-weaken-↑⋆)
  open SimpleExt simple

  -- A generalized variant of Lemmas₀.lookup-map-weaken-↑⋆.
  lookup-map-weaken-↑⋆ : ∀ {m n} k x {ρ : Sub T m n} {t} →
                         lookup (map weaken ρ ↑⋆ k) x ≡
                         lookup ((t /∷ ρ) ↑⋆ k) (lift k suc x)
  lookup-map-weaken-↑⋆ zero    x               = refl
  lookup-map-weaken-↑⋆ (suc k) zero            = refl
  lookup-map-weaken-↑⋆ (suc k) (suc x) {ρ} {t} = begin
      lookup (map weaken (map weaken ρ ↑⋆ k)) x
    ≡⟨ lookup-map x weaken (map weaken ρ ↑⋆ k) ⟩
      weaken (lookup (map weaken ρ ↑⋆ k) x)
    ≡⟨ cong weaken (lookup-map-weaken-↑⋆ k x) ⟩
      weaken (lookup ((t /∷ ρ) ↑⋆ k) (lift k suc x))
    ≡⟨ sym (lookup-map (lift k suc x) weaken ((t /∷ ρ) ↑⋆ k)) ⟩
      lookup (map weaken ((t /∷ ρ) ↑⋆ k)) (lift k suc x)
    ∎

-- A version of Data.Fin.Lemmas.Lemmas₁ with additional lemmas.
--
-- FIXME: this should go into Data.Fin.Substitution.Lemmas.
module ExtLemmas₁ {ℓ} {T : Pred ℕ ℓ} (lemmas₁ : Lemmas₁ T) where
  open Data.Fin using (raise; fromℕ; lift)

  open Lemmas₁ lemmas₁
  open Simple simple

  lookup-wk⋆ : ∀ {n} (x : Fin n) k → lookup (wk⋆ k) x ≡ var (raise k x)
  lookup-wk⋆ x zero    = lookup-id x
  lookup-wk⋆ x (suc k) = lookup-map-weaken x {_} {wk⋆ k} (lookup-wk⋆ x k)

  lookup-raise-↑⋆ : ∀ k {m n} x {y} {σ : Sub T m n} →
                    lookup  σ                x  ≡ var          y →
                    lookup (σ ↑⋆ k) (raise k x) ≡ var (raise k y)
  lookup-raise-↑⋆ zero    x         hyp = hyp
  lookup-raise-↑⋆ (suc k) x {y} {σ} hyp =
    lookup-map-weaken (raise k x) {_} {σ ↑⋆ k} (lookup-raise-↑⋆ k x hyp)

-- A generalized version of Data.Fin.Lemmas.Lemmas₄
--
-- FIXME: this should go into Data.Fin.Substitution.Lemmas.
module ExtLemmas₄ {ℓ} {T : Pred ℕ ℓ} (lemmas₄ : Lemmas₄ T) where
  open Data.Fin using (lift; raise)

  open Lemmas₄    lemmas₄ public hiding (⊙-wk; wk-commutes)
  open Lemmas₃    lemmas₃        using (lookup-wk-↑⋆-⊙; /✶-↑✶′)
  open SimpleExt  simple         using (_/∷_; weaken⋆)
  open ExtLemmas₀ lemmas₀        using (lookup-map-weaken-↑⋆)

  ⊙-wk-↑⋆ : ∀ {m n} {ρ : Sub T m n} {t} k →
            ρ ↑⋆ k ⊙ wk ↑⋆ k ≡ wk ↑⋆ k ⊙ (t /∷ ρ) ↑⋆ k
  ⊙-wk-↑⋆ {ρ = ρ} {t} k = sym (begin
    wk ↑⋆ k ⊙ (t /∷ ρ) ↑⋆ k   ≡⟨ lemma ⟩
    map weaken ρ ↑⋆ k         ≡⟨ cong (λ ρ′ → ρ′ ↑⋆ k) map-weaken ⟩
    (ρ ⊙ wk) ↑⋆ k             ≡⟨ ↑⋆-distrib k ⟩
    ρ ↑⋆ k ⊙ wk ↑⋆ k          ∎)
    where
    lemma = extensionality λ x → begin
        lookup (wk ↑⋆ k ⊙ (t /∷ ρ) ↑⋆ k) x
      ≡⟨ lookup-wk-↑⋆-⊙ k ⟩
        lookup ((t /∷ ρ) ↑⋆ k) (lift k suc x)
      ≡⟨ sym (lookup-map-weaken-↑⋆ k x) ⟩
        lookup (map weaken ρ ↑⋆ k) x
      ∎

  ⊙-wk : ∀ {m n} {ρ : Sub T m n} {t} → ρ ⊙ wk ≡ wk ⊙ (t /∷ ρ)
  ⊙-wk = ⊙-wk-↑⋆ zero

  wk-⊙-∷ : ∀ {n m} t {ρ : Sub T m n} → wk ⊙ (t ∷ ρ) ≡ ρ
  wk-⊙-∷ t {ρ} = extensionality λ x → begin
    lookup (wk ⊙ (t ∷ ρ)) x  ≡⟨ lookup-wk-↑⋆-⊙ zero {x} ⟩
    lookup (t ∷ ρ) (suc x)   ≡⟨⟩
    lookup ρ       x         ∎

  wk-↑⋆-commutes : ∀ {m n} {ρ : Sub T m n} {t′} k t →
                   t / ρ ↑⋆ k / wk ↑⋆ k ≡ t / wk ↑⋆ k / (t′ /∷ ρ) ↑⋆ k
  wk-↑⋆-commutes {ρ = ρ} {t} k =
    /✶-↑✶′ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ (t /∷ ρ)) ⊙-wk-↑⋆ k

  wk-commutes : ∀ {m n} {ρ : Sub T m n} {t′} t →
                t / ρ / wk ≡ t / wk / (t′ /∷ ρ)
  wk-commutes = wk-↑⋆-commutes zero

  raise-/-↑⋆ : ∀ {m n} k x {ρ : Sub T m n} →
               var (raise k x) / ρ ↑⋆ k ≡ var x / ρ / wk⋆ k
  raise-/-↑⋆ zero    x {ρ} = sym (id-vanishes (var x / ρ))
  raise-/-↑⋆ (suc k) x {ρ} = begin
    var (suc (raise k x)) / ρ ↑⋆ suc k   ≡⟨ suc-/-↑ (raise k x) ⟩
    var (raise k x) / ρ ↑⋆ k / wk        ≡⟨ cong (_/ wk) (raise-/-↑⋆ k x) ⟩
    var x / ρ / wk⋆ k / wk               ≡⟨ sym (/-⊙ (var x / ρ)) ⟩
    var x / ρ / wk⋆ k ⊙ wk           ≡⟨ cong (var x / ρ /_) (sym map-weaken) ⟩
    var x / ρ / wk⋆ (suc k)          ∎

  /-wk⋆ : ∀ {n} k {t : T n} → t / wk⋆ k ≡ weaken⋆ k t
  /-wk⋆ zero    {t} = id-vanishes t
  /-wk⋆ (suc k) {t} = begin
    t / map weaken (wk⋆ k)   ≡⟨ cong (t /_) map-weaken ⟩
    t / wk⋆ k ⊙ wk           ≡⟨ /-⊙ t ⟩
    t / wk⋆ k / wk           ≡⟨ /-wk ⟩
    weaken (t / wk⋆ k)       ≡⟨ cong weaken (/-wk⋆ k) ⟩
    weaken (weaken⋆ k t)     ∎

  -- Weakening commutes with substitution.

  weaken-/ : ∀ {m n} {ρ : Sub T m n} {t′} t →
             weaken (t / ρ) ≡ weaken t / (t′ /∷ ρ)
  weaken-/ {ρ = ρ} {t′} t = begin
    weaken (t / ρ)         ≡⟨ sym /-wk ⟩
    t / ρ / wk             ≡⟨ wk-commutes t ⟩
    t / wk / (t′ /∷ ρ)     ≡⟨ cong₂ _/_ /-wk refl ⟩
    weaken t / (t′ /∷ ρ)   ∎

  weaken-/-∷ : ∀ {n m} {t′} {ρ : Sub T m n} t → weaken t / (t′ ∷ ρ) ≡ t / ρ
  weaken-/-∷ {_} {_} {t′} {ρ} t = begin
    weaken t / (t′ ∷ ρ)   ≡⟨ cong (_/ (t′ ∷ ρ)) (sym /-wk) ⟩
    t / wk / (t′ ∷ ρ)     ≡⟨ sym (/-⊙ t) ⟩
    t / (wk ⊙ (t′ ∷ ρ))   ≡⟨ cong (t /_) (wk-⊙-∷ t′) ⟩
    t / ρ                 ∎

-- A generalize version of Data.Fin.Lemmas.AppLemmas
--
-- FIXME: this should go into Data.Fin.Substitution.Lemmas.
module ExtAppLemmas {ℓ₁ ℓ₂} {T₁ : Pred ℕ ℓ₁} {T₂ : Pred ℕ ℓ₂}
                    (appLemmas : AppLemmas T₁ T₂) where

  open AppLemmas appLemmas public hiding (wk-commutes)
  open SimpleExt simple           using (_/∷_)
  private module L₄ = ExtLemmas₄ lemmas₄
  open L₄ public using (wk-⊙-∷)

  wk-↑⋆-commutes : ∀ {m n} {ρ : Sub T₂ m n} {t′} k t →
                   t / ρ ↑⋆ k / wk ↑⋆ k ≡ t / wk ↑⋆ k / (t′ /∷ ρ) ↑⋆ k
  wk-↑⋆-commutes {ρ = ρ} {t} k =
    ⨀→/✶ (ε ▻ ρ ↑⋆ k ▻ wk ↑⋆ k) (ε ▻ wk ↑⋆ k ▻ (t /∷ ρ) ↑⋆ k) (L₄.⊙-wk-↑⋆ k)

  wk-commutes : ∀ {m n} {ρ : Sub T₂ m n} {t′} t →
                t / ρ / wk ≡ t / wk / (t′ /∷ ρ)
  wk-commutes = wk-↑⋆-commutes zero

-- Lemmas relating T₃ substitutions in T₁ and T₂.
record LiftAppLemmas {ℓ₁ ℓ₂ ℓ₃}
                     (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) (T₃ : Pred ℕ ℓ₃)
                     : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  field
    lift          : ∀ {n} → T₃ n → T₂ n
    application₁₃ : Application T₁ T₃
    application₂₃ : Application T₂ T₃
    lemmas₂       : Lemmas₄     T₂
    lemmas₃       : Lemmas₄     T₃

  private
    module L₂ = ExtLemmas₄  lemmas₂
    module L₃ = ExtLemmas₄  lemmas₃
    module A₁ = Application application₁₃
    module A₂ = Application application₂₃

  field
    -- Lifting commutes with application of T₃ substitutions.
    lift-/ : ∀ {m n} t {σ : Sub T₃ m n} → lift (t L₃./ σ) ≡ lift t A₂./ σ

    -- Lifting preserves variables.
    lift-var : ∀ {n} (x : Fin n) → lift (L₃.var x) ≡ L₂.var x

    -- Sequences of T₃ substitutions are equivalent when applied to
    -- T₁s if they are equivalent when applied to T₂ variables.
    /✶-↑✶ :
      ∀ {m n} (σs₁ σs₂ : Subs T₃ m n) →
      (∀ k x → L₂.var x A₂./✶ σs₁ L₃.↑✶ k ≡ L₂.var x A₂./✶ σs₂ L₃.↑✶ k) →
       ∀ k t → t        A₁./✶ σs₁ L₃.↑✶ k ≡ t        A₁./✶ σs₂ L₃.↑✶ k

  lift-lookup-⊙ : ∀ {m n k} x {σ₁ : Sub T₃ m n} {σ₂ : Sub T₃ n k} →
                  lift (lookup (σ₁ L₃.⊙ σ₂) x) ≡ lift (lookup σ₁ x) A₂./ σ₂
  lift-lookup-⊙ x {σ₁} {σ₂} = begin
    lift (lookup (σ₁ L₃.⊙ σ₂) x)   ≡⟨ cong lift (L₃.lookup-⊙ x {σ₁}) ⟩
    lift (lookup σ₁ x L₃./ σ₂)     ≡⟨ lift-/ (lookup σ₁ x) ⟩
    lift (lookup σ₁ x) A₂./ σ₂     ∎

  lift-lookup-⨀ : ∀ {m n} x (σs : Subs T₃ m n) →
                  lift (lookup (L₃.⨀ σs) x) ≡ L₂.var x A₂./✶ σs
  lift-lookup-⨀ x ε = begin
    lift (lookup L₃.id x)    ≡⟨ cong lift (L₃.lookup-id x) ⟩
    lift (L₃.var x)          ≡⟨ lift-var x ⟩
    L₂.var x                 ∎
  lift-lookup-⨀ x (σ ◅ ε) = begin
    lift (lookup σ x)        ≡⟨ cong lift (sym L₃.var-/) ⟩
    lift (L₃.var x L₃./ σ)   ≡⟨ lift-/ _ ⟩
    lift (L₃.var x) A₂./ σ   ≡⟨ cong₂ A₂._/_ (lift-var x) refl ⟩
    L₂.var x A₂./ σ          ∎
  lift-lookup-⨀ x (σ ◅ (σ′ ◅ σs′)) = begin
      lift (lookup (L₃.⨀ σs L₃.⊙ σ) x)
    ≡⟨ lift-lookup-⊙ x {L₃.⨀ σs} ⟩
      lift (lookup (L₃.⨀ σs) x) A₂./ σ
    ≡⟨ cong₂ A₂._/_ (lift-lookup-⨀ x (σ′ ◅ σs′)) refl ⟩
      L₂.var x A₂./✶ σs A₂./ σ
    ∎
    where σs = σ′ ◅ σs′

  -- Sequences of T₃ substitutions are equivalent when applied to
  -- T₁s if they are equivalent when applied as composites.
  /✶-↑✶′ : ∀ {m n} (σs₁ σs₂ : Subs T₃ m n) →
           (∀ k → L₃.⨀ (σs₁ L₃.↑✶ k) ≡ L₃.⨀ (σs₂ L₃.↑✶ k)) →
            ∀ k t → t A₁./✶ σs₁ L₃.↑✶ k ≡ t A₁./✶ σs₂ L₃.↑✶ k
  /✶-↑✶′ σs₁ σs₂ hyp = /✶-↑✶ σs₁ σs₂ (λ k x → begin
      L₂.var x A₂./✶ σs₁ L₃.↑✶ k
    ≡⟨ sym (lift-lookup-⨀ x (σs₁ L₃.↑✶ k)) ⟩
      lift (lookup (L₃.⨀ (σs₁ L₃.↑✶ k)) x)
    ≡⟨ cong (λ σ → lift (lookup σ x)) (hyp k) ⟩
      lift (lookup (L₃.⨀ (σs₂ L₃.↑✶ k)) x)
    ≡⟨ lift-lookup-⨀ x (σs₂ L₃.↑✶ k) ⟩
      L₂.var x A₂./✶ σs₂ L₃.↑✶ k
    ∎)

  -- Derived lemmas about applications of T₃ substitutions to T₁s.
  appLemmas : AppLemmas T₁ T₃
  appLemmas = record
    { application = application₁₃
    ; lemmas₄     = lemmas₃
    ; id-vanishes = /✶-↑✶′ (ε ▻ L₃.id) ε L₃.id-↑⋆ 0
    ; /-⊙         = /✶-↑✶′ (ε ▻ _ L₃.⊙ _) (ε ▻ _ ▻ _) L₃.↑⋆-distrib 0
    }
  open ExtAppLemmas appLemmas public
    hiding (application; lemmas₂; lemmas₃; var; weaken; subst; simple)

-- Lemmas relating T₂ and T₃ substitutions in T₁.

record LiftSubLemmas {ℓ₁ ℓ₂ ℓ₃}
                     (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) (T₃ : Pred ℕ ℓ₃)
                     : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  field
    application₁₂ : Application   T₁ T₂
    liftAppLemmas : LiftAppLemmas T₁ T₂ T₃

  open LiftAppLemmas liftAppLemmas hiding (/✶-↑✶; /-wk)
  private
    module L₃  = ExtLemmas₄  lemmas₃
    module L₂  = ExtLemmas₄  lemmas₂
    module A₁₂ = Application application₁₂
    module A₁₃ = Application (AppLemmas.application appLemmas)
    module A₂₃ = Application application₂₃

  field
    -- Weakening commutes with lifting.
    weaken-lift : ∀ {n} (t : T₃ n) → L₂.weaken (lift t) ≡ lift (L₃.weaken t)

    -- Applying a composition of T₂ substitutions to T₁s
    -- corresponds to two consecutive applications.
    /-⊙₂ : ∀ {m n k} {σ₁ : Sub T₂ m n} {σ₂ : Sub T₂ n k} t →
           t A₁₂./ σ₁ L₂.⊙ σ₂ ≡ t A₁₂./ σ₁ A₁₂./ σ₂

    -- Sequences of T₃ substitutions are equivalent to T₂
    -- substitutions when applied to T₁s if they are equivalent when
    -- applied to variables.
    /✶-↑✶₁ :
      ∀ {m n} (σs₁ : Subs T₃ m n) (σs₂ : Subs T₂ m n) →
      (∀ k x → L₂.var x A₂₃./✶ σs₁ ↑✶ k ≡ L₂.var x L₂./✶  σs₂ L₂.↑✶ k) →
       ∀ k t → t        A₁₃./✶ σs₁ ↑✶ k ≡ t        A₁₂./✶ σs₂ L₂.↑✶ k

    -- Sequences of T₃ substitutions are equivalent to T₂
    -- substitutions when applied to T₂s if they are equivalent when
    -- applied to variables.
    /✶-↑✶₂ :
      ∀ {m n} (σs₁ : Subs T₃ m n) (σs₂ : Subs T₂ m n) →
      (∀ k x → L₂.var x A₂₃./✶ σs₁ ↑✶ k ≡ L₂.var x L₂./✶ σs₂ L₂.↑✶ k) →
       ∀ k t → t        A₂₃./✶ σs₁ ↑✶ k ≡ t        L₂./✶ σs₂ L₂.↑✶ k

  -- Lifting of T₃ substitutions to T₂ substitutions.
  liftSub : ∀ {m n} → Sub T₃ m n → Sub T₂ m n
  liftSub σ = map lift σ

  -- The two types of lifting commute.
  liftSub-↑⋆ : ∀ {m n} (σ : Sub T₃ m n) k →
               liftSub σ L₂.↑⋆ k ≡ liftSub (σ ↑⋆ k)
  liftSub-↑⋆ σ zero    = refl
  liftSub-↑⋆ σ (suc k) = cong₂ _∷_ (sym (lift-var _)) (begin
    map L₂.weaken (liftSub σ L₂.↑⋆ k)   ≡⟨ cong (map _) (liftSub-↑⋆ σ k) ⟩
    map L₂.weaken (map lift (σ ↑⋆ k))   ≡⟨ sym (map-∘ _ _ _) ⟩
    map (L₂.weaken ∘ lift) (σ ↑⋆ k)     ≡⟨ map-cong weaken-lift _ ⟩
    map (lift ∘ L₃.weaken)  (σ ↑⋆ k)    ≡⟨ map-∘ _ _ _ ⟩
    map lift (map L₃.weaken (σ ↑⋆ k))   ∎)

  -- The identity substitutions are equivalent up to lifting.
  liftSub-id : ∀ {n} → liftSub (L₃.id {n}) ≡ L₂.id {n}
  liftSub-id {zero}  = refl
  liftSub-id {suc n} = begin
    liftSub (L₃.id L₃.↑)  ≡⟨ sym (liftSub-↑⋆ L₃.id 1) ⟩
    liftSub L₃.id L₂.↑    ≡⟨ cong L₂._↑ liftSub-id ⟩
    L₂.id ∎

  -- Weakening is equivalent up to lifting.
  liftSub-wk⋆ : ∀ k {n} → liftSub (L₃.wk⋆ k {n}) ≡ L₂.wk⋆ k {n}
  liftSub-wk⋆ zero    = liftSub-id
  liftSub-wk⋆ (suc k) = begin
    liftSub (map L₃.weaken (L₃.wk⋆ k))   ≡⟨ sym (map-∘ _ _ _) ⟩
    map (lift ∘ L₃.weaken) (L₃.wk⋆ k)    ≡⟨ sym (map-cong weaken-lift _) ⟩
    map (L₂.weaken ∘ lift) (L₃.wk⋆ k)    ≡⟨ map-∘ _ _ _ ⟩
    map L₂.weaken (liftSub (L₃.wk⋆ k))   ≡⟨ cong (map _) (liftSub-wk⋆ k) ⟩
    map L₂.weaken (L₂.wk⋆ k)             ∎

  -- Weakening is equivalent up to lifting.
  liftSub-wk : ∀ {n} → liftSub (L₃.wk {n}) ≡ L₂.wk {n}
  liftSub-wk = liftSub-wk⋆ 1

  -- Single variable substitution is equivalent up to lifting.
  liftSub-sub : ∀ {n} (t : T₃ n) → liftSub (L₃.sub t) ≡ L₂.sub (lift t)
  liftSub-sub t = cong₂ _∷_ refl liftSub-id

  -- Lifting commutes with application to variables.
  var-/-liftSub-↑⋆ : ∀ {m n} (σ : Sub T₃ m n) k x →
                     L₂.var x A₂₃./ σ ↑⋆ k ≡ L₂.var x L₂./ liftSub σ L₂.↑⋆ k
  var-/-liftSub-↑⋆ σ k x = begin
      L₂.var x A₂₃./ σ ↑⋆ k
    ≡⟨ cong₂ A₂₃._/_ (sym (lift-var x)) refl ⟩
      lift (L₃.var x) A₂₃./ σ ↑⋆ k
    ≡⟨ sym (lift-/ _) ⟩
      lift (L₃.var x L₃./ σ ↑⋆ k)
    ≡⟨ cong lift L₃.var-/ ⟩
      lift (lookup (σ ↑⋆ k) x)
    ≡⟨ sym (lookup-map x lift (σ ↑⋆ k)) ⟩
      lookup (liftSub (σ ↑⋆ k)) x
    ≡⟨ sym L₂.var-/ ⟩
      L₂.var x L₂./ liftSub (σ ↑⋆ k)
    ≡⟨ cong (L₂._/_ (L₂.var x)) (sym (liftSub-↑⋆ σ k)) ⟩
      L₂.var x L₂./ liftSub σ L₂.↑⋆ k
    ∎

  -- Lifting commutes with application.

  /-liftSub-↑⋆ : ∀ {m n} k t {σ : Sub T₃ m n} →
                 t A₁₃./ σ ↑⋆ k ≡ t A₁₂./ liftSub σ L₂.↑⋆ k
  /-liftSub-↑⋆ k t {σ} =
    /✶-↑✶₁ (ε ▻ σ) (ε ▻ liftSub σ) (var-/-liftSub-↑⋆ σ) k t

  /-liftSub : ∀ {m n} t {σ : Sub T₃ m n} → t A₁₃./ σ ≡ t A₁₂./ liftSub σ
  /-liftSub = /-liftSub-↑⋆ zero

  -- Weakening is equivalent up to choice of application.

  /-wk-↑⋆ : ∀ {n} k {t : T₁ (k + n)} →
            t A₁₃./ L₃.wk ↑⋆ k ≡ t A₁₂./ L₂.wk L₂.↑⋆ k
  /-wk-↑⋆ k {t = t} = begin
      t A₁₃./ L₃.wk ↑⋆ k
    ≡⟨ /-liftSub-↑⋆ k t ⟩
      t A₁₂./ (liftSub L₃.wk) L₂.↑⋆ k
    ≡⟨ cong (λ σ → t A₁₂./ σ L₂.↑⋆ k) liftSub-wk ⟩
      t A₁₂./ L₂.wk L₂.↑⋆ k
    ∎

  /-wk : ∀ {n} {t : T₁ n} → t A₁₃./ L₃.wk ≡ t A₁₂./ L₂.wk
  /-wk = /-wk-↑⋆ zero

  -- Single-variable substitution is equivalent up to choice of
  -- application.

  /-sub-↑⋆ : ∀ {n} k t (s : T₃ n) →
             t A₁₃./ L₃.sub s ↑⋆ k ≡ t A₁₂./ L₂.sub (lift s) L₂.↑⋆ k
  /-sub-↑⋆ k t s = begin
      t A₁₃./ L₃.sub s ↑⋆ k
    ≡⟨ /-liftSub-↑⋆ k t ⟩
      t A₁₂./ liftSub (L₃.sub s) L₂.↑⋆ k
    ≡⟨ cong (λ σ → t A₁₂./ σ L₂.↑⋆ k) (liftSub-sub s) ⟩
      t A₁₂./ L₂.sub (lift s) L₂.↑⋆ k
    ∎

  /-sub : ∀ {n} t (s : T₃ n) →
          t A₁₃./ L₃.sub s ≡ t A₁₂./ L₂.sub (lift s)
  /-sub = /-sub-↑⋆ zero

  -- Lifting commutes with application.
  /-sub-↑ : ∀ {m n} t s (σ : Sub T₃ m n) →
            t A₁₂./ L₂.sub s A₁₃./ σ ≡ (t A₁₃./ σ ↑) A₁₂./ L₂.sub (s A₂₃./ σ)
  /-sub-↑ t s σ = begin
      t A₁₂./ L₂.sub s A₁₃./ σ
    ≡⟨ /-liftSub _ ⟩
      t A₁₂./ L₂.sub s A₁₂./ liftSub σ
    ≡⟨ sym (/-⊙₂ t) ⟩
      t A₁₂./ (L₂.sub s L₂.⊙ liftSub σ)
    ≡⟨ cong₂ A₁₂._/_ refl (L₂.sub-⊙ s) ⟩
      t A₁₂./ (liftSub σ L₂.↑ L₂.⊙ L₂.sub (s L₂./ liftSub σ))
    ≡⟨ /-⊙₂ t ⟩
      t A₁₂./ liftSub σ L₂.↑ A₁₂./ L₂.sub (s L₂./ liftSub σ)
    ≡⟨ cong₂ (A₁₂._/_ ∘ A₁₂._/_ t) (liftSub-↑⋆ _ 1)
             (cong L₂.sub (sym (/-liftSub₂ s))) ⟩
      t A₁₂./ liftSub (σ ↑) A₁₂./ L₂.sub (s A₂₃./ σ)
    ≡⟨ cong₂ A₁₂._/_ (sym (/-liftSub t)) refl ⟩
      t A₁₃./ σ ↑ A₁₂./ L₂.sub (s A₂₃./ σ)
    ∎
    where
      /-liftSub₂ : ∀ {m n} s {σ : Sub T₃ m n} →
                   s A₂₃./ σ ≡ s L₂./ liftSub σ
      /-liftSub₂ s {σ} = /✶-↑✶₂ (ε ▻ σ) (ε ▻ liftSub σ)
                                (var-/-liftSub-↑⋆ σ) zero s

-- Lemmas relating weakening of T₁ to T₂ substitutions in T₁.

record WeakenLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂)
                    : Set (ℓ₁ ⊔ ℓ₂) where
  field
    weaken : ∀ {n} → T₁ n → T₁ (suc n)    -- Weakening of T₁s.

    -- Lemmas about application of T₂ substitutions in T₁

    appLemmas : AppLemmas T₁ T₂

  open ExtAppLemmas appLemmas hiding (/-wk; weaken; _⊙_)
  open Lemmas₄ lemmas₄ using (_⊙_) renaming (weaken to weaken′)

  -- A lemma relating weakening to the wk substitution

  field /-wk : ∀ {n} {t : T₁ n} → t / wk ≡ weaken t

  extension : Extension T₁
  extension = record { weaken = weaken }
  open Extension extension public using (weaken⋆)

  -- A generalized version of wk-sub-vanishes for T₁s.

  weaken-sub : ∀ {n t′} → (t : T₁ n) → weaken t / sub t′ ≡ t
  weaken-sub t = begin
    weaken t / sub _   ≡⟨ cong₂ _/_ (sym /-wk) refl ⟩
    t / wk / sub _     ≡⟨ wk-sub-vanishes t ⟩
    t                  ∎

  -- A variants of /-wk⋆ for T₁s.

  /-wk⋆ : ∀ {n} k {t : T₁ n} → t / wk⋆ k ≡ weaken⋆ k t
  /-wk⋆ zero    {t} = id-vanishes t
  /-wk⋆ (suc k) {t} = begin
    t / map weaken′ (wk⋆ k)   ≡⟨ /-weaken t ⟩
    t / wk⋆ k / wk            ≡⟨ /-wk ⟩
    weaken (t / wk⋆ k)        ≡⟨ cong weaken (/-wk⋆ k) ⟩
    weaken (weaken⋆ k t)      ∎

  open SimpleExt simple public using (_/∷_)

  -- Weakening commutes with substitution.

  weaken-/ : ∀ {m n} {σ : Sub T₂ m n} {t′} t →
             weaken (t / σ) ≡ weaken t / (t′ /∷ σ)
  weaken-/ {σ = σ} {t′} t = begin
    weaken (t / σ)         ≡⟨ sym /-wk ⟩
    t / σ / wk             ≡⟨ wk-commutes t ⟩
    t / wk / (t′ /∷ σ)     ≡⟨ cong₂ _/_ /-wk refl ⟩
    weaken t / (t′ /∷ σ)   ∎

  weaken-/-∷ : ∀ {n m} {t′} {σ : Sub T₂ m n} (t : T₁ m) →
               weaken t / (t′ ∷ σ) ≡ t / σ
  weaken-/-∷ {_} {_} {t′} {σ} t = begin
    weaken t / (t′ ∷ σ)   ≡⟨ cong (_/ (t′ ∷ σ)) (sym /-wk) ⟩
    t / wk / (t′ ∷ σ)     ≡⟨ sym (/-⊙ t) ⟩
    t / wk ⊙ (t′ ∷ σ)     ≡⟨ cong (t /_) (wk-⊙-∷ t′) ⟩
    t / σ                 ∎

-- T₂-substitutions in term-like T₁
--
-- FIXME: this should go into Data.Fin.Substitution.

record TermLikeSubst {ℓ} (T₁ : Pred ℕ ℓ) (T₂ : ℕ → Set)
                     : Set (lsuc (ℓ ⊔ lzero)) where
  field
    app       : ∀ {T₃} → Lift T₃ T₂ → ∀ {m n} → T₁ m → Sub T₃ m n → T₁ n
    termSubst : TermSubst T₂

  open TermSubst termSubst public
    hiding (app; var; weaken; _/Var_; _/_; _/✶_)

  termApplication : Application T₁ T₂
  termApplication = record { _/_ = app termLift }

  varApplication : Application T₁ Fin
  varApplication = record { _/_ = app varLift }

  open Application termApplication public using (_/_; _/✶_)
  open Application varApplication  public using () renaming (_/_ to _/Var_)

  -- Weakening of T₁s.

  weaken : ∀ {n} → T₁ n → T₁ (suc n)
  weaken t = t /Var VarSubst.wk

-- Lemmas for a term-like T₁ derived from term lemmas for T₂

record TermLikeLemmas {ℓ} (T₁ : Pred ℕ ℓ) (T₂ : ℕ → Set)
                      : Set (lsuc (ℓ ⊔ lzero)) where
  field
    app        : ∀ {T₃} → Lift T₃ T₂ → ∀ {m n} → T₁ m → Sub T₃ m n → T₁ n
    termLemmas : TermLemmas T₂

  termLikeSubst : TermLikeSubst T₁ T₂
  termLikeSubst = record
    { app       = app
    ; termSubst = TermLemmas.termSubst termLemmas
    }

  open TermLikeSubst termLikeSubst using (termSubst; termLift; varLift; weaken)
  open TermSubst     termSubst     using (var; _⊙_; module Lifted)

  field /✶-↑✶₁ : ∀ {T₃} {lift : Lift T₃ T₂} →
                 let open Application (record { _/_ = app lift })
                       using ()     renaming (_/✶_ to _/✶₁_)
                     open Lifted lift
                       using (_↑✶_) renaming (_/✶_ to _/✶₂_)
                 in
                 ∀ {m n} (σs₁ : Subs T₃ m n) (σs₂ : Subs T₃ m n) →
                 (∀ k x → var x /✶₂ σs₁ ↑✶ k ≡ var x /✶₂ σs₂ ↑✶ k) →
                  ∀ k t → t     /✶₁ σs₁ ↑✶ k ≡ t     /✶₁ σs₂ ↑✶ k

  termApplication : Application T₁ T₂
  termApplication = record { _/_ = app termLift }

  varApplication : Application T₁ Fin
  varApplication = record { _/_ = app varLift }

  field /✶-↑✶₂ : let open Application varApplication
                       using () renaming (_/✶_ to _/✶₁₃_)
                     open Application termApplication
                       using () renaming (_/✶_ to _/✶₁₂_)
                     open Lifted varLift
                       using () renaming (_↑✶_ to _↑✶₃_; _/✶_ to _/✶₂₃_)
                     open TermSubst termSubst
                       using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂₂_)
                 in
                 ∀ {m n} (σs₁ : Subs Fin m n) (σs₂ : Subs T₂ m n) →
                 (∀ k x → var x /✶₂₃ σs₁ ↑✶₃ k ≡ var x /✶₂₂ σs₂ ↑✶₂ k) →
                  ∀ k t → t     /✶₁₃ σs₁ ↑✶₃ k ≡ t     /✶₁₂ σs₂ ↑✶₂ k

  -- An instantiation of the above lemmas for T₂ substitutions in T₁s.
  termLiftAppLemmas : LiftAppLemmas T₁ T₂ T₂
  termLiftAppLemmas = record
    { lift          = Lift.lift termLift
    ; application₁₃ = termApplication
    ; application₂₃ = TermLemmas.application termLemmas
    ; lemmas₂       = TermLemmas.lemmas₄ termLemmas
    ; lemmas₃       = TermLemmas.lemmas₄ termLemmas
    ; lift-/        = λ _ → refl
    ; lift-var      = λ _ → refl
    ; /✶-↑✶         = /✶-↑✶₁
    }

  open LiftAppLemmas termLiftAppLemmas public hiding (/-wk; _⊙_)

  -- An instantiation of the above lemmas for variable substitutions
  -- (renamings) in T₁s.
  varLiftSubLemmas : LiftSubLemmas T₁ T₂ Fin
  varLiftSubLemmas = record
    { application₁₂ = termApplication
    ; liftAppLemmas = record
      { lift          = Lift.lift varLift
      ; application₁₃ = varApplication
      ; application₂₃ = Lifted.application varLift
      ; lemmas₂       = TermLemmas.lemmas₄ termLemmas
      ; lemmas₃       = VarLemmas.lemmas₄
      ; lift-/        = λ _ → sym (TermLemmas.app-var termLemmas)
      ; lift-var      = λ _ → refl
      ; /✶-↑✶         = /✶-↑✶₁
      }
    ; weaken-lift = λ _ → TermLemmas.weaken-var termLemmas
    ; /-⊙₂        = AppLemmas./-⊙ appLemmas
    ; /✶-↑✶₁      = /✶-↑✶₂
    ; /✶-↑✶₂      = TermLemmas./✶-↑✶ termLemmas
    }

  open Application   varApplication   public using () renaming (_/_ to _/Var_)
  open LiftSubLemmas varLiftSubLemmas public hiding (/✶-↑✶₁; /✶-↑✶₂; _⊙_; /-wk)
    renaming (liftAppLemmas to varLiftAppLemmas)

  -- Lemmas relating weakening of T₁s to T₂-substitutions in T₁s.

  weakenLemmas : WeakenLemmas T₁ T₂
  weakenLemmas = record
    { weaken    = weaken
    ; appLemmas = appLemmas
    ; /-wk      = sym /-wk
    }
    where open LiftSubLemmas varLiftSubLemmas using (/-wk)

  open WeakenLemmas weakenLemmas public hiding (appLemmas)

  -- Another variant of /-wk⋆ relating VarSubst.wk to weakening of T₁s.

  /Var-wk⋆ : ∀ {n} k {t : T₁ n} →
             t /Var VarSubst.wk⋆ k ≡ weaken⋆ k t
  /Var-wk⋆ k {t} = begin
    t /Var VarSubst.wk⋆ k          ≡⟨ /-liftSub t ⟩
    t / liftSub (VarSubst.wk⋆ k)   ≡⟨ cong (t /_) (liftSub-wk⋆ k) ⟩
    t / wk⋆ k                      ≡⟨ /-wk⋆ k ⟩
    weaken⋆ k t                    ∎

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


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

module Relation.Binary.Equivalence.PropHIT where

open import Prelude
open import Relation.Nullary.Stable
open import HITs.PropositionalTruncation
open import HITs.PropositionalTruncation.Sugar
open import Relation.Binary

infix 4 _≐_
_≐_ : A → A → Type _
x ≐ y = ∥ x ≡ y ∥

import Relation.Binary.Equivalence.Reasoning

module _ {A : Type a} where
  prop-equiv : Equivalence A _
  prop-equiv .Equivalence._≋_ = _≐_
  prop-equiv .Equivalence.sym = sym ∥$∥_
  prop-equiv .Equivalence.refl = ∣ refl ∣
  prop-equiv .Equivalence.trans x≐y y≐z = ⦇ x≐y ; y≐z ⦈

  module Reasoning = Relation.Binary.Equivalence.Reasoning prop-equiv

-- data ∙⊥ : Prop where

-- private
--   variable
--     x y z : A

-- rerel : ∙⊥ → ⊥
-- rerel ()

-- ∙refute : x ≐ y → (x ≡ y → ⊥) → ∙⊥
-- ∙refute ∣ x≡y ∣ x≢y with x≢y x≡y
-- ∙refute ∣ x≡y ∣ x≢y | ()

-- refute : x ≐ y → ¬ (¬ (x ≡ y))
-- refute x≐y x≢y = rerel (∙refute x≐y x≢y)

-- unsquash : Stable (x ≡ y) → x ≐ y → x ≡ y
-- unsquash st x≐y = st (refute x≐y)

-- ∙refl : x ≐ x
-- ∙refl = ∣ refl ∣

-- ∙trans : x ≐ y → y ≐ z → x ≐ z
-- ∙trans ∣ xy ∣ (∣_∣ yz) = ∣_∣ (xy ; yz)

-- ∙sym : x ≐ y → y ≐ x
-- ∙sym (∣_∣ p) = ∣_∣ (sym p)

-- ∙cong : (f : A → B) → x ≐ y → f x ≐ f y
-- ∙cong f ∣ x≡y ∣ = ∣ cong f x≡y ∣

-- module Reasoning where
--   infixr 2 ≐˘⟨⟩-syntax ≐⟨∙⟩-syntax

--   ≐˘⟨⟩-syntax : ∀ (x : A) {y z} → y ≐ z → y ≐ x → x ≐ z
--   ≐˘⟨⟩-syntax _ y≡z y≡x = ∙trans (∙sym y≡x) y≡z

--   syntax ≐˘⟨⟩-syntax x y≡z y≡x = x ≐˘⟨ y≡x ⟩ y≡z

--   ≐⟨∙⟩-syntax : ∀ (x : A) {y z} → y ≐ z → x ≐ y → x ≐ z
--   ≐⟨∙⟩-syntax _ y≡z x≡y = ∙trans x≡y y≡z

--   syntax ≐⟨∙⟩-syntax x y≡z x≡y = x ≐⟨ x≡y ⟩ y≡z

--   _≐⟨⟩_ : ∀ (x : A) {y} → x ≐ y → x ≐ y
--   _ ≐⟨⟩ x≡y = x≡y

--   infix 2.5 _∎
--   _∎ : ∀ {A : Type a} (x : A) → x ≐ x
--   _∎ x = ∙refl

--   infixr 2 ≡˘⟨⟩-syntax ≡⟨∙⟩-syntax

--   ≡˘⟨⟩-syntax : ∀ (x : A) {y z} → y ≐ z → y ≡ x → x ≐ z
--   ≡˘⟨⟩-syntax _ y≡z y≡x = ∙trans (∣_∣ (sym y≡x)) y≡z

--   syntax ≡˘⟨⟩-syntax x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

--   ≡⟨∙⟩-syntax : ∀ (x : A) {y z} → y ≐ z → x ≡ y → x ≐ z
--   ≡⟨∙⟩-syntax _ y≡z x≡y = ∙trans ∣ x≡y ∣ y≡z

--   syntax ≡⟨∙⟩-syntax x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Extensions.ListFirst where

open import Prelude hiding (_⊔_)

open import Data.Product
open import Data.List
open import Data.List.Any
open Membership-≡ hiding (find)
open import Level

-- proof that an element is the first in a vector to satisfy the predicate B
data First {a b} {A : Set a} (B : A → Set b) : (x : A) → List A → Set (a ⊔ b) where

  here  : ∀ {x : A} → (p : B x) → (v : List A) → First B x (x ∷ v)
  there : ∀ {x} {v : List A} (x' : A) → ¬ (B x') → First B x v → First B x (x' ∷ v)

-- get the witness of B x from the element ∈ First
first⟶witness : ∀ {A : Set} {B : A → Set} {x l} → First B x l → B x
first⟶witness (here p v) = p
first⟶witness (there x ¬px f) = first⟶witness f

first⟶∈ : ∀ {A : Set} {B : A → Set} {x l} → First B x l → (x ∈ l × B x)
first⟶∈ (here {x = x} p v) = here refl , p
first⟶∈ (there x' ¬px f) with (first⟶∈ f)
first⟶∈ (there x' ¬px f) | x∈l , p = there x∈l , p

-- more likable syntax for the above structure
first_∈_⇔_ : {A : Set} → A → List A → (B : A → Set) → Set
first_∈_⇔_ x v p = First p x v

-- a decision procedure to find the first element in a vector that satisfies a predicate
find : ∀ {A : Set} (P : A → Set) → ((a : A) → Dec (P a)) → (v : List A) →
       Dec (∃ λ e → first e ∈ v ⇔ P)
find P dec [] = no (λ{ (e , ()) })
find P dec (x ∷ v) with dec x
find P dec (x ∷ v) | yes px = yes (x , here px v)
find P dec (x ∷ v) | no ¬px with find P dec v
find P dec (x ∷ v) | no ¬px | yes firstv = yes (, there x ¬px (proj₂ firstv))
find P dec (x ∷ v) | no ¬px | no ¬firstv = no $ helper ¬px ¬firstv
  where
    helper : ¬ (P x) → ¬ (∃ λ e → First P e v) → ¬ (∃ λ e → First P e (x ∷ v))
    helper ¬px ¬firstv (.x , here p .v) = ¬px p
    helper ¬px ¬firstv (u  , there ._ _ firstv) = ¬firstv (u , firstv)

module FirstLemmas where

  first-unique : ∀ {A : Set} {P : A → Set} {x y v} → First P x v → First P y v → x ≡ y
  first-unique (here x v) (here y .v) = refl
  first-unique (here {x = x} px v) (there .x ¬px r) = ⊥-elim (¬px px)
  first-unique (there x ¬px l) (here {x = .x} px v) = ⊥-elim (¬px px)
  first-unique (there x' _ l) (there .x' _ r) = first-unique l r


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some theory for Semigroup
------------------------------------------------------------------------

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

open import Algebra using (Semigroup)

module Algebra.Properties.Semigroup {a ℓ} (S : Semigroup a ℓ) where

open Semigroup S

x∙yz≈xy∙z : ∀ x y z → x ∙ (y ∙ z) ≈ (x ∙ y) ∙ z
x∙yz≈xy∙z x y z =  sym (assoc x y z)


text:
------------------------------------------------------------------------
-- Infinite grammars
------------------------------------------------------------------------

-- The grammar language introduced below is not more expressive than
-- the one in Grammar.Infinite.Basic. There are two reasons for
-- introducing this new language:
--
-- ⑴ The function final-whitespace? below analyses the structure of a
--   grammar, and can in some cases automatically prove a certain
--   theorem. It is quite hard to analyse grammars that contain
--   unrestricted corecursion and/or the higher-order bind combinator,
--   so the new language contains extra constructors intended to make
--   the analysis easier (in some cases).
--
-- ⑵ The extra constructors can also make it easier to convince Agda's
--   termination checker that certain infinite grammars are
--   productive.

{-# OPTIONS --guardedness #-}

module Grammar.Infinite where

open import Algebra
open import Category.Monad
open import Codata.Musical.Colist
  using (Colist; []; _∷_; _∈_; here; there)
open import Codata.Musical.Notation
open import Data.Bool
open import Data.Char
open import Data.Empty
open import Data.List as List using (List; []; _∷_; [_]; _++_; concat)
open import Data.List.Categorical
  renaming (module MonadProperties to List-monad)
open import Data.List.NonEmpty as List⁺
  using (List⁺; _∷_; _∷⁺_; head; tail)
open import Data.List.Properties
open import Data.Maybe hiding (_>>=_)
open import Data.Maybe.Categorical as MaybeC
open import Data.Nat
open import Data.Product as Prod
open import Data.String as String using (String)
open import Data.Unit
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (_↔_; module Inverse)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Relation.Nullary
open import Tactic.MonoidSolver

private
  module LM {A : Set} = Monoid (++-monoid A)
  open module MM {f} = RawMonadPlus (MaybeC.monadPlus {f = f})
    using () renaming (_<$>_ to _<$>M_; _⊛_ to _⊛M_)

import Grammar.Infinite.Basic as Basic; open Basic._∈_·_
open import Utilities

------------------------------------------------------------------------
-- A grammar language that is less minimal than the one in
-- Grammar.Infinite.Basic

mutual

  infix  30 _⋆
  infixl 20 _<$>_ _<$_ _⊛_ _<⊛_ _⊛>_
  infixl 15 _>>=_
  infixl 10 _∣_

  data Grammar : Set → Set₁ where

    -- The empty string.

    return : ∀ {A} → A → Grammar A

    -- A single, arbitrary token.

    token  : Grammar Char

    -- Monadic sequencing.

    _>>=_  : ∀ {c₁ c₂ A B} →
             ∞Grammar c₁ A → (A → ∞Grammar c₂ B) → Grammar B

    -- Symmetric choice.

    _∣_    : ∀ {c₁ c₂ A} → ∞Grammar c₁ A → ∞Grammar c₂ A → Grammar A

    -- Failure.

    fail   : ∀ {A} → Grammar A

    -- A specific token.

    tok    : Char → Grammar Char

    -- Map.

    _<$>_  : ∀ {c A B} → (A → B) → ∞Grammar c A → Grammar B
    _<$_   : ∀ {c A B} → A → ∞Grammar c B → Grammar A

    -- Applicative sequencing.

    _⊛_    : ∀ {c₁ c₂ A B} →
             ∞Grammar c₁ (A → B) → ∞Grammar c₂ A → Grammar B
    _<⊛_   : ∀ {c₁ c₂ A B} → ∞Grammar c₁ A → ∞Grammar c₂ B → Grammar A
    _⊛>_   : ∀ {c₁ c₂ A B} → ∞Grammar c₁ A → ∞Grammar c₂ B → Grammar B

    -- Kleene star.

    _⋆     : ∀ {c A} → ∞Grammar c A → Grammar (List A)

  -- Coinductive if the argument is true.
  --
  -- Conditional coinduction is used to avoid having to write the
  -- delay operator (♯_) all the time.

  ∞Grammar : Bool → Set → Set₁
  ∞Grammar true  A = ∞ (Grammar A)
  ∞Grammar false A =    Grammar A

-- Families of grammars for specific values.

Grammar-for : Set → Set₁
Grammar-for A = (x : A) → Grammar (∃ λ x′ → x′ ≡ x)

-- Forcing of a conditionally coinductive grammar.

♭? : ∀ {c A} → ∞Grammar c A → Grammar A
♭? {true}  = ♭
♭? {false} = id

-- A grammar combinator: Kleene plus.

infix 30 _+

_+ : ∀ {c A} → ∞Grammar c A → Grammar (List⁺ A)
g + = _∷_ <$> g ⊛ g ⋆

-- The semantics of "extended" grammars is given by translation to
-- simple grammars.

⟦_⟧ : ∀ {A} → Grammar A → Basic.Grammar A
⟦ return x  ⟧ = Basic.return x
⟦ token     ⟧ = Basic.token
⟦ g₁ >>= g₂ ⟧ = ♯ ⟦ ♭? g₁ ⟧ Basic.>>= λ x → ♯ ⟦ ♭? (g₂ x) ⟧
⟦ g₁ ∣ g₂   ⟧ = ♯ ⟦ ♭? g₁ ⟧ Basic.∣ ♯ ⟦ ♭? g₂ ⟧
⟦ fail      ⟧ = Basic.fail
⟦ tok t     ⟧ = Basic.tok t
⟦ f <$> g   ⟧ = ♯ ⟦ ♭? g  ⟧ Basic.>>= λ x → ♯ Basic.return (f x)
⟦ x <$ g    ⟧ = ♯ ⟦ ♭? g  ⟧ Basic.>>= λ _ → ♯ Basic.return x
⟦ g₁ ⊛ g₂   ⟧ = ♯ ⟦ ♭? g₁ ⟧ Basic.>>= λ f → ♯ ⟦ f <$> g₂ ⟧
⟦ g₁ <⊛ g₂  ⟧ = ♯ ⟦ ♭? g₁ ⟧ Basic.>>= λ x → ♯ ⟦ x <$  g₂ ⟧
⟦ g₁ ⊛> g₂  ⟧ = ♯ ⟦ ♭? g₁ ⟧ Basic.>>= λ _ → ♯ ⟦    ♭? g₂ ⟧
⟦ g ⋆       ⟧ = ♯ Basic.return [] Basic.∣ ♯ ⟦ List⁺.toList <$> g + ⟧

------------------------------------------------------------------------
-- More grammar combinators

mutual

  -- Combinators that transform families of grammars for certain
  -- elements to families of grammars for certain lists.

  list : ∀ {A} → Grammar-for A → Grammar-for (List A)
  list elem []       = return ([] , refl)
  list elem (x ∷ xs) =
    Prod.map List⁺.toList
             (λ eq → P.cong₂ _∷_ (P.cong head eq) (P.cong tail eq)) <$>
      list⁺ elem (x ∷ xs)

  list⁺ : ∀ {A} → Grammar-for A → Grammar-for (List⁺ A)
  list⁺ elem (x ∷ xs) =
    Prod.zip _∷_ (P.cong₂ _∷_) <$> elem x ⊛ list elem xs

-- Elements preceded by something.

infixl 18 _prec-by_

_prec-by_ : ∀ {A B} → Grammar A → Grammar B → Grammar (List A)
g prec-by prec = (prec ⊛> g) ⋆

-- Elements separated by something.

infixl 18 _sep-by_

_sep-by_ : ∀ {A B} → Grammar A → Grammar B → Grammar (List⁺ A)
g sep-by sep = _∷_ <$> g ⊛ (g prec-by sep)

-- The empty string if the argument is true, otherwise failure.

if-true : (b : Bool) → Grammar (T b)
if-true true  = return tt
if-true false = fail

-- A token satisfying a given predicate.

sat : (p : Char → Bool) → Grammar (∃ λ t → T (p t))
sat p = token >>= λ t → _,_ t <$> if-true (p t)

-- A given token satisfying a given predicate.

tok-sat : (p : Char → Bool) → Grammar-for (∃ (T ∘ p))
tok-sat p (t , pt) = ((t , pt) , refl) <$ tok t

-- Whitespace.

whitespace : Grammar Char
whitespace = tok ' ' ∣ tok '\n'

-- The given string.

string : List Char → Grammar (List Char)
string []      = return []
string (t ∷ s) = _∷_ <$> tok t ⊛ string s

-- A variant of string that takes a String rather than a list of
-- characters.

string′ : String → Grammar (List Char)
string′ = string ∘ String.toList

-- The given string, possibly followed by some whitespace.

symbol : List Char → Grammar (List Char)
symbol s = string s <⊛ whitespace ⋆

symbol′ : String → Grammar (List Char)
symbol′ = symbol ∘ String.toList

------------------------------------------------------------------------
-- Alternative definition of the semantics

-- Pattern matching on values of type x Basic.∈ ⟦ g₁ ⊛ g₂ ⟧ · s (say)
-- is somewhat inconvenient: the patterns have the form
-- (>>=-sem _ (>>=-sem _ return-sem)). The following, direct
-- definition of the semantics may be easier to use.

infix 4 _∈_·_

data _∈_·_ : ∀ {A} → A → Grammar A → List Char → Set₁ where
  return-sem : ∀ {A} {x : A} → x ∈ return x · []
  token-sem  : ∀ {t} → t ∈ token · [ t ]
  >>=-sem    : ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A}
                 {g₂ : A → ∞Grammar c₂ B} {x y s₁ s₂} →
               x ∈ ♭? g₁ · s₁ → y ∈ ♭? (g₂ x) · s₂ →
               y ∈ g₁ >>= g₂ · s₁ ++ s₂
  left-sem   : ∀ {c₁ c₂ A} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A}
                 {x s} →
               x ∈ ♭? g₁ · s → x ∈ g₁ ∣ g₂ · s
  right-sem  : ∀ {c₁ c₂ A} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A}
                 {x s} →
               x ∈ ♭? g₂ · s → x ∈ g₁ ∣ g₂ · s
  tok-sem    : ∀ {t} → t ∈ tok t · [ t ]
  <$>-sem    : ∀ {c A B} {f : A → B} {g : ∞Grammar c A} {x s} →
               x ∈ ♭? g · s → f x ∈ f <$> g · s
  <$-sem     : ∀ {c A B} {x : A} {g : ∞Grammar c B} {y s} →
               y ∈ ♭? g · s → x ∈ x <$ g · s
  ⊛-sem      : ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ (A → B)}
                 {g₂ : ∞Grammar c₂ A} {f x s₁ s₂} →
               f ∈ ♭? g₁ · s₁ → x ∈ ♭? g₂ · s₂ →
               f x ∈ g₁ ⊛ g₂ · s₁ ++ s₂
  <⊛-sem     : ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B}
                 {x y s₁ s₂} →
               x ∈ ♭? g₁ · s₁ → y ∈ ♭? g₂ · s₂ →
               x ∈ g₁ <⊛ g₂ · s₁ ++ s₂
  ⊛>-sem     : ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B}
                 {x y s₁ s₂} →
               x ∈ ♭? g₁ · s₁ → y ∈ ♭? g₂ · s₂ →
               y ∈ g₁ ⊛> g₂ · s₁ ++ s₂
  ⋆-[]-sem   : ∀ {c A} {g : ∞Grammar c A} →
               [] ∈ g ⋆ · []
  ⋆-+-sem    : ∀ {c A} {g : ∞Grammar c A} {x xs s} →
               (x ∷ xs) ∈ g + · s → x ∷ xs ∈ g ⋆ · s

-- A weak form of "local unambiguity", unambiguity for a given string.
-- (Note that the parse trees are not required to be equal.)

Locally-unambiguous : ∀ {A} → Grammar A → List Char → Set₁
Locally-unambiguous g s = ∀ {x y} → x ∈ g · s → y ∈ g · s → x ≡ y

-- A weak form of unambiguity.

Unambiguous : ∀ {A} → Grammar A → Set₁
Unambiguous g = ∀ {s} → Locally-unambiguous g s

-- Parsers.

Parser : ∀ {A} → Grammar A → Set₁
Parser g = ∀ s → Dec (∃ λ x → x ∈ g · s)

-- Cast lemma.

cast : ∀ {A} {g : Grammar A} {x s₁ s₂} →
       s₁ ≡ s₂ → x ∈ g · s₁ → x ∈ g · s₂
cast refl = id

-- The alternative semantics is isomorphic to the one above.

isomorphic : ∀ {A x s} {g : Grammar A} →
             x ∈ g · s ↔ x Basic.∈ ⟦ g ⟧ · s
isomorphic {g = g} = record
  { to         = P.→-to-⟶ sound
  ; from       = P.→-to-⟶ (complete g)
  ; inverse-of = record
    { left-inverse-of  = complete∘sound
    ; right-inverse-of = sound∘complete g
    }
  }
  where

  -- Some short lemmas.

  lemma₁ : ∀ s → s ++ [] ≡ s
  lemma₁ = proj₂ LM.identity

  lemma₂ : ∀ s₁ s₂ → s₁ ++ s₂ ++ [] ≡ s₁ ++ s₂
  lemma₂ s₁ s₂ = P.cong (_++_ s₁) (lemma₁ s₂)

  lemma₃ : ∀ s₁ s₂ → s₁ ++ s₂ ≡ ((s₁ ++ []) ++ s₂ ++ []) ++ []
  lemma₃ s₁ s₂ = begin
    s₁ ++ s₂                        ≡⟨ P.cong₂ _++_ (P.sym $ lemma₁ s₁) (P.sym $ lemma₁ s₂) ⟩
    (s₁ ++ []) ++ s₂ ++ []          ≡⟨ P.sym $ lemma₁ _ ⟩
    ((s₁ ++ []) ++ s₂ ++ []) ++ []  ∎
    where open P.≡-Reasoning

  tok-lemma : ∀ {t t′ s} → t ≡ t′ × s ≡ [ t ] → t′ ∈ tok t · s
  tok-lemma (refl , refl) = tok-sem

  -- Soundness.

  sound : ∀ {A x s} {g : Grammar A} → x ∈ g · s → x Basic.∈ ⟦ g ⟧ · s
  sound return-sem               = return-sem
  sound token-sem                = token-sem
  sound (>>=-sem x∈ y∈)          = >>=-sem (sound x∈) (sound y∈)
  sound (left-sem x∈)            = left-sem (sound x∈)
  sound (right-sem x∈)           = right-sem (sound x∈)
  sound tok-sem                  = Inverse.from Basic.tok-sem
                                     ⟨$⟩ (refl , refl)
  sound (<$>-sem x∈)             = Basic.cast (lemma₁ _)
                                     (>>=-sem (sound x∈) return-sem)
  sound (<$-sem x∈)              = Basic.cast (lemma₁ _)
                                     (>>=-sem (sound x∈) return-sem)
  sound (⊛-sem {s₁ = s₁} f∈ x∈)  = Basic.cast (lemma₂ s₁ _)
                                     (>>=-sem (sound f∈)
                                        (>>=-sem (sound x∈) return-sem))
  sound (<⊛-sem {s₁ = s₁} x∈ y∈) = Basic.cast (lemma₂ s₁ _)
                                     (>>=-sem (sound x∈)
                                        (>>=-sem (sound y∈) return-sem))
  sound (⊛>-sem {s₁ = s₁} x∈ y∈) = >>=-sem (sound x∈) (sound y∈)
  sound ⋆-[]-sem                 = left-sem return-sem
  sound (⋆-+-sem xs∈)            = Basic.cast (lemma₁ _)
                                     (right-sem
                                        (>>=-sem (sound xs∈)
                                                 return-sem))

  -- Completeness.

  complete : ∀ {A x s} (g : Grammar A) → x Basic.∈ ⟦ g ⟧ · s → x ∈ g · s
  complete (return x)  return-sem      = return-sem
  complete token       token-sem       = token-sem
  complete (g₁ >>= g₂) (>>=-sem x∈ y∈) = >>=-sem (complete _ x∈)
                                                 (complete _ y∈)
  complete (g₁ ∣ g₂)   (left-sem x∈)   = left-sem  (complete _ x∈)
  complete (g₁ ∣ g₂)   (right-sem x∈)  = right-sem (complete _ x∈)

  complete fail    ∈fail = ⊥-elim (Basic.fail-sem⁻¹ ∈fail)
  complete (tok t) t∈    = tok-lemma (Inverse.to Basic.tok-sem ⟨$⟩ t∈)

  complete (f <$> g) (>>=-sem x∈ return-sem) =
    cast (P.sym $ lemma₁ _)
         (<$>-sem (complete _ x∈))
  complete (x <$ g) (>>=-sem x∈ return-sem) =
    cast (P.sym $ lemma₁ _)
         (<$-sem (complete _ x∈))
  complete (g₁ ⊛ g₂) (>>=-sem {s₁ = s₁} f∈ (>>=-sem x∈ return-sem)) =
    cast (P.sym $ lemma₂ s₁ _)
         (⊛-sem (complete _ f∈) (complete _ x∈))
  complete (g₁ <⊛ g₂) (>>=-sem {s₁ = s₁} x∈ (>>=-sem y∈ return-sem)) =
    cast (P.sym $ lemma₂ s₁ _)
         (<⊛-sem (complete _ x∈) (complete _ y∈))
  complete (g₁ ⊛> g₂) (>>=-sem x∈ y∈) =
    ⊛>-sem (complete _ x∈) (complete _ y∈)

  complete (g ⋆) (left-sem return-sem) = ⋆-[]-sem
  complete (g ⋆) (right-sem (>>=-sem
                    (>>=-sem (>>=-sem {s₁ = s₁} x∈  return-sem)
                             (>>=-sem           xs∈ return-sem))
                    return-sem)) =
    cast (lemma₃ s₁ _)
         (⋆-+-sem (⊛-sem (<$>-sem (complete _ x∈)) (complete _ xs∈)))

  -- More short lemmas.

  sound-cast :
    ∀ {A x s₁ s₂}
    (g : Grammar A) (eq : s₁ ≡ s₂) (x∈ : x ∈ g · s₁) →
    sound (cast eq x∈) ≡ Basic.cast eq (sound x∈)
  sound-cast _ refl _ = refl

  complete-cast :
    ∀ {A x s₁ s₂}
    (g : Grammar A) (eq : s₁ ≡ s₂) (x∈ : x Basic.∈ ⟦ g ⟧ · s₁) →
    complete g (Basic.cast eq x∈) ≡ cast eq (complete g x∈)
  complete-cast _ refl _ = refl

  cast-cast :
    ∀ {A} {x : A} {s₁ s₂ g} (eq : s₁ ≡ s₂) {x∈ : x Basic.∈ g · s₁} →
    Basic.cast (P.sym eq) (Basic.cast eq x∈) ≡ x∈
  cast-cast refl = refl

  cast-cast′ :
    ∀ {A} {x : A} {s₁ s₂ g}
    (eq₁ : s₂ ≡ s₁) (eq₂ : s₁ ≡ s₂) {x∈ : x Basic.∈ g · s₁} →
    Basic.cast eq₁ (Basic.cast eq₂ x∈) ≡ x∈
  cast-cast′ refl refl = refl

  -- The functions sound and complete are inverses.

  complete∘sound : ∀ {A x s} {g : Grammar A} (x∈ : x ∈ g · s) →
                   complete g (sound x∈) ≡ x∈
  complete∘sound return-sem      = refl
  complete∘sound token-sem       = refl
  complete∘sound (>>=-sem x∈ y∈) = P.cong₂ >>=-sem (complete∘sound x∈)
                                                   (complete∘sound y∈)
  complete∘sound (left-sem x∈)   = P.cong left-sem (complete∘sound x∈)
  complete∘sound (right-sem x∈)  = P.cong right-sem (complete∘sound x∈)

  complete∘sound (tok-sem {t = t})
    rewrite Inverse.right-inverse-of (Basic.tok-sem {t = t})
                                     (refl , refl)
    = refl

  complete∘sound (<$>-sem {s = s} x∈) with sound x∈ | complete∘sound x∈
  complete∘sound (<$>-sem {f = f} {g = g} {s = s}
                          .(complete _ x∈′)) | x∈′ | refl
    rewrite complete-cast (f <$> g) (lemma₁ s) (>>=-sem x∈′ return-sem)
          | lemma₁ s
    = refl

  complete∘sound (<$-sem {x = x} {g = g} {s = s} x∈) with sound x∈ | complete∘sound x∈
  complete∘sound (<$-sem {x = x} {g = g} {s = s}
                         .(complete _ x∈′)) | x∈′ | refl
    rewrite complete-cast (x <$ g) (lemma₁ s) (>>=-sem x∈′ return-sem)
          | lemma₁ s
    = refl

  complete∘sound (⊛-sem f∈ x∈) with sound f∈ | complete∘sound f∈
                                  | sound x∈ | complete∘sound x∈
  complete∘sound (⊛-sem {g₁ = g₁} {g₂ = g₂} {s₁ = s₁} {s₂ = s₂}
                        .(complete _ f∈′) .(complete _ x∈′))
    | f∈′ | refl | x∈′ | refl
    rewrite complete-cast (g₁ ⊛ g₂) (lemma₂ s₁ s₂)
                          (>>=-sem f∈′ (>>=-sem x∈′ return-sem))
          | lemma₁ s₂
    = refl

  complete∘sound (<⊛-sem x∈ y∈) with sound x∈ | complete∘sound x∈
                                   | sound y∈ | complete∘sound y∈
  complete∘sound (<⊛-sem {g₁ = g₁} {g₂ = g₂} {s₁ = s₁} {s₂ = s₂}
                         .(complete _ x∈′) .(complete _ y∈′))
    | x∈′ | refl | y∈′ | refl
    rewrite complete-cast (g₁ <⊛ g₂) (lemma₂ s₁ s₂)
                          (>>=-sem x∈′ (>>=-sem y∈′ return-sem))
          | lemma₁ s₂
    = refl

  complete∘sound (⊛>-sem x∈ y∈) with sound x∈ | complete∘sound x∈
                                   | sound y∈ | complete∘sound y∈
  complete∘sound (⊛>-sem .(complete _ x∈′) .(complete _ y∈′))
    | x∈′ | refl | y∈′ | refl
    = refl

  complete∘sound ⋆-[]-sem      = refl
  complete∘sound (⋆-+-sem xs∈) with sound xs∈ | complete∘sound xs∈
  complete∘sound (⋆-+-sem {g = g}
                    .(complete _ (>>=-sem (>>=-sem x∈   return-sem)
                                          (>>=-sem xs∈′ return-sem))))
    | >>=-sem (>>=-sem {s₁ = s₁} x∈   return-sem)
              (>>=-sem {s₁ = s₂} xs∈′ return-sem)
    | refl
    rewrite complete-cast (g ⋆) (lemma₁ ((s₁ ++ []) ++ s₂ ++ []))
                          (right-sem
                            (>>=-sem (>>=-sem (>>=-sem x∈   return-sem)
                                              (>>=-sem xs∈′ return-sem))
                                     return-sem))
          | lemma₁ s₁ | lemma₁ s₂ | lemma₁ (s₁ ++ s₂)
    = refl

  sound∘complete : ∀ {A x s}
                   (g : Grammar A) (x∈ : x Basic.∈ ⟦ g ⟧ · s) →
                   sound (complete g x∈) ≡ x∈
  sound∘complete (return x)  return-sem      = refl
  sound∘complete token       token-sem       = refl
  sound∘complete (g₁ >>= g₂) (>>=-sem x∈ y∈) = P.cong₂ >>=-sem (sound∘complete (♭? g₁) x∈)
                                                               (sound∘complete (♭? (g₂ _)) y∈)
  sound∘complete (g₁ ∣ g₂)   (left-sem x∈)   = P.cong left-sem  (sound∘complete (♭? g₁) x∈)
  sound∘complete (g₁ ∣ g₂)   (right-sem x∈)  = P.cong right-sem (sound∘complete (♭? g₂) x∈)

  sound∘complete fail    ∈fail = ⊥-elim (Basic.fail-sem⁻¹ ∈fail)
  sound∘complete (tok t) t∈    =
    helper _ (Inverse.left-inverse-of Basic.tok-sem t∈)
    where
    helper : ∀ {t t′ s} {t∈ : t′ Basic.∈ Basic.tok t · s}
             (eqs : t ≡ t′ × s ≡ [ t ]) →
             Inverse.from Basic.tok-sem ⟨$⟩ eqs ≡ t∈ →
             sound (tok-lemma eqs) ≡ t∈
    helper (refl , refl) ≡t∈ = ≡t∈

  sound∘complete (f <$> g) (>>=-sem x∈ return-sem)
    with complete (♭? g) x∈ | sound∘complete (♭? g) x∈
  sound∘complete (f <$> g) (>>=-sem {s₁ = s₁} .(sound x∈′) return-sem)
    | x∈′ | refl
    rewrite sound-cast (f <$> g) (P.sym $ lemma₁ s₁) (<$>-sem x∈′)
    = cast-cast (lemma₁ s₁)

  sound∘complete (x <$ g) (>>=-sem x∈ return-sem)
    with complete (♭? g) x∈ | sound∘complete (♭? g) x∈
  sound∘complete (x <$ g) (>>=-sem {s₁ = s₁} .(sound x∈′) return-sem)
    | x∈′ | refl
    rewrite sound-cast (x <$ g) (P.sym $ lemma₁ s₁) (<$-sem x∈′)
    = cast-cast (lemma₁ s₁)

  sound∘complete (g₁ ⊛ g₂) (>>=-sem f∈ (>>=-sem x∈ return-sem))
    with complete (♭? g₁) f∈ | sound∘complete (♭? g₁) f∈
       | complete (♭? g₂) x∈ | sound∘complete (♭? g₂) x∈
  sound∘complete (g₁ ⊛ g₂)
    (>>=-sem {s₁ = s₁} .(sound f∈′)
             (>>=-sem {s₁ = s₂} .(sound x∈′) return-sem))
    | f∈′ | refl | x∈′ | refl
    rewrite sound-cast (g₁ ⊛ g₂) (P.sym $ lemma₂ s₁ s₂) (⊛-sem f∈′ x∈′)
    = cast-cast (lemma₂ s₁ s₂)

  sound∘complete (g₁ <⊛ g₂) (>>=-sem x∈ (>>=-sem y∈ return-sem))
    with complete (♭? g₁) x∈ | sound∘complete (♭? g₁) x∈
       | complete (♭? g₂) y∈ | sound∘complete (♭? g₂) y∈
  sound∘complete (g₁ <⊛ g₂)
    (>>=-sem {s₁ = s₁} .(sound x∈′)
             (>>=-sem {s₁ = s₂} .(sound y∈′) return-sem))
    | x∈′ | refl | y∈′ | refl
    rewrite sound-cast (g₁ <⊛ g₂) (P.sym $ lemma₂ s₁ s₂) (<⊛-sem x∈′ y∈′)
    = cast-cast (lemma₂ s₁ s₂)

  sound∘complete (g₁ ⊛> g₂) (>>=-sem x∈ y∈)
    with complete (♭? g₁) x∈ | sound∘complete (♭? g₁) x∈
       | complete (♭? g₂) y∈ | sound∘complete (♭? g₂) y∈
  sound∘complete (g₁ ⊛> g₂) (>>=-sem .(sound x∈′) .(sound y∈′))
    | x∈′ | refl | y∈′ | refl
    = refl

  sound∘complete (g ⋆) (left-sem return-sem) = refl
  sound∘complete (g ⋆)
    (right-sem
       (>>=-sem (>>=-sem (>>=-sem x∈  return-sem)
                         (>>=-sem xs∈ return-sem))
                return-sem))
    with complete (♭? g) x∈ | sound∘complete (♭? g) x∈
       | complete (g ⋆) xs∈ | sound∘complete (g ⋆) xs∈
  sound∘complete (g ⋆)
    (right-sem
       (>>=-sem (>>=-sem (>>=-sem {s₁ = s₁} .(sound x∈′)  return-sem)
                         (>>=-sem {s₁ = s₂} .(sound xs∈′) return-sem))
                return-sem))
    | x∈′ | refl | xs∈′ | refl
    rewrite sound-cast (g ⋆) (lemma₃ s₁ s₂)
                       (⋆-+-sem (⊛-sem (<$>-sem x∈′) xs∈′))
    = lemma g (lemma₃ s₁ s₂) (lemma₁ (s₁ ++ s₂))
              (lemma₂ s₁ s₂) (lemma₁ s₁)
              (>>=-sem (sound x∈′)  return-sem)
              (>>=-sem (sound xs∈′) return-sem)
    where
    lemma :
      ∀ {c A} {f : List A → List⁺ A} {xs s₁ s₁++s₂ s₁++[] s₂++[]}
      (g   : ∞Grammar c A)
      (eq₁ : s₁++s₂ ≡ (s₁++[] ++ s₂++[]) ++ [])
      (eq₂ : (s₁++s₂) ++ [] ≡ s₁++s₂)
      (eq₃ : s₁ ++ s₂++[] ≡ s₁++s₂)
      (eq₄ : s₁++[] ≡ s₁)
      (f∈  : f  Basic.∈ ⟦ _∷_ <$> g ⟧ · s₁++[])
      (xs∈ : xs Basic.∈ ⟦ f <$> g ⋆ ⟧ · s₂++[]) →
      _≡_ {A = List⁺.toList xs Basic.∈ ⟦ g ⋆ ⟧ · _}
          (Basic.cast eq₁
             (Basic.cast eq₂
                (right-sem
                   (>>=-sem
                      (Basic.cast eq₃ (>>=-sem (Basic.cast eq₄ f∈) xs∈))
                      return-sem))))
          (right-sem (>>=-sem (>>=-sem f∈ xs∈) return-sem))
    lemma _ eq₁ eq₂ refl refl _ _ = cast-cast′ eq₁ eq₂

------------------------------------------------------------------------
-- Semantics combinators

+-sem : ∀ {c A} {g : ∞Grammar c A} {x xs s₁ s₂} →
        x ∈ ♭? g · s₁ → xs ∈ g ⋆ · s₂ → (x ∷ xs) ∈ g + · s₁ ++ s₂
+-sem x∈ xs∈ = ⊛-sem (<$>-sem x∈) xs∈

⋆-∷-sem : ∀ {c A} {g : ∞Grammar c A} {x xs s₁ s₂} →
          x ∈ ♭? g · s₁ → xs ∈ g ⋆ · s₂ → x ∷ xs ∈ g ⋆ · s₁ ++ s₂
⋆-∷-sem x∈ xs∈ = ⋆-+-sem (+-sem x∈ xs∈)

⋆-⋆-sem : ∀ {c A} {g : ∞Grammar c A} {xs₁ xs₂ s₁ s₂} →
          xs₁ ∈ g ⋆ · s₁ → xs₂ ∈ g ⋆ · s₂ → xs₁ ++ xs₂ ∈ g ⋆ · s₁ ++ s₂
⋆-⋆-sem ⋆-[]-sem xs₂∈ = xs₂∈
⋆-⋆-sem (⋆-+-sem (⊛-sem (<$>-sem {s = s₁} x∈) xs₁∈)) xs₂∈ =
  cast (P.sym $ LM.assoc s₁ _ _)
       (⋆-∷-sem x∈ (⋆-⋆-sem xs₁∈ xs₂∈))

+-∷-sem : ∀ {c A} {g : ∞Grammar c A} {x xs s₁ s₂} →
          x ∈ ♭? g · s₁ → xs ∈ g + · s₂ → x ∷⁺ xs ∈ g + · s₁ ++ s₂
+-∷-sem x∈ xs∈ = +-sem x∈ (⋆-+-sem xs∈)

mutual

  list-sem : ∀ {A} {g : Grammar-for A} {s : A → List Char} →
             (∀ x → (x , refl) ∈ g x · s x) →
             ∀ xs → (xs , refl) ∈ list g xs · concat (List.map s xs)
  list-sem elem []       = return-sem
  list-sem elem (x ∷ xs) = <$>-sem (list⁺-sem elem (x ∷ xs))

  list⁺-sem :
    ∀ {A} {g : Grammar-for A} {s : A → List Char} →
    (∀ x → (x , refl) ∈ g x · s x) →
    ∀ xs → (xs , refl) ∈ list⁺ g xs ·
           concat (List.map s (List⁺.toList xs))
  list⁺-sem elem (x ∷ xs) = ⊛-sem (<$>-sem (elem x)) (list-sem elem xs)

sep-by-sem-singleton :
  ∀ {A B} {g : Grammar A} {sep : Grammar B} {x s} →
  x ∈ g · s → x ∷ [] ∈ g sep-by sep · s
sep-by-sem-singleton x∈ =
  cast (proj₂ LM.identity _)
             (⊛-sem (<$>-sem x∈) ⋆-[]-sem)

sep-by-sem-∷ :
  ∀ {A B} {g : Grammar A} {sep : Grammar B} {x y xs s₁ s₂ s₃} →
  x ∈ g · s₁ → y ∈ sep · s₂ → xs ∈ g sep-by sep · s₃ →
  x ∷⁺ xs ∈ g sep-by sep · s₁ ++ s₂ ++ s₃
sep-by-sem-∷ {s₂ = s₂} x∈ y∈ (⊛-sem (<$>-sem x′∈) xs∈) =
  ⊛-sem (<$>-sem x∈)
        (cast (LM.assoc s₂ _ _)
              (⋆-∷-sem (⊛>-sem y∈ x′∈) xs∈))

if-true-sem : ∀ {b} (t : T b) → t ∈ if-true b · []
if-true-sem {b = true}  _  = return-sem
if-true-sem {b = false} ()

sat-sem : ∀ {p : Char → Bool} {t} (pt : T (p t)) →
          (t , pt) ∈ sat p · [ t ]
sat-sem pt = >>=-sem token-sem (<$>-sem (if-true-sem pt))

tok-sat-sem : ∀ {p : Char → Bool} {t} (pt : T (p t)) →
              ((t , pt) , refl) ∈ tok-sat p (t , pt) · [ t ]
tok-sat-sem _ = <$-sem tok-sem

list-sem-lemma : ∀ {A} {x : A} {g s} →
                 x ∈ g · concat (List.map [_] s) → x ∈ g · s
list-sem-lemma = cast (List-monad.right-identity _)

single-space-sem : (' ' ∷ []) ∈ whitespace + · String.toList " "
single-space-sem = +-sem (left-sem tok-sem) ⋆-[]-sem

string-sem′ : ∀ {s s′ s″} → s ∈ string s′ · s″ ↔ (s ≡ s′ × s′ ≡ s″)
string-sem′ = record
  { to         = P.→-to-⟶ (to _)
  ; from       = P.→-to-⟶ (from _)
  ; inverse-of = record
    { left-inverse-of  = from∘to _
    ; right-inverse-of = to∘from _
    }
  }
  where
  to : ∀ {s} s′ {s″} → s ∈ string s′ · s″ → s ≡ s′ × s′ ≡ s″
  to []       return-sem                   = (refl , refl)
  to (c ∷ s′) (⊛-sem (<$>-sem tok-sem) s∈) =
    Prod.map (P.cong (_∷_ c)) (P.cong (_∷_ c)) $ to s′ s∈

  from : ∀ {s} s′ {s″} → s ≡ s′ × s′ ≡ s″ → s ∈ string s′ · s″
  from []       (refl , refl) = return-sem
  from (c ∷ s′) (refl , refl) =
    ⊛-sem (<$>-sem tok-sem) (from s′ (refl , refl))

  from∘to : ∀ {s} s′ {s″} (s∈ : s ∈ string s′ · s″) →
            from s′ (to s′ s∈) ≡ s∈
  from∘to []       return-sem                   = refl
  from∘to (c ∷ s′) (⊛-sem (<$>-sem tok-sem) s∈)
    with to s′ s∈ | from∘to s′ s∈
  from∘to (c ∷ s′) (⊛-sem (<$>-sem tok-sem) .(from s′ (refl , refl)))
    | (refl , refl) | refl = refl

  to∘from : ∀ {s} s′ {s″} (eqs : s ≡ s′ × s′ ≡ s″) →
            to s′ (from s′ eqs) ≡ eqs
  to∘from []       (refl , refl) = refl
  to∘from (c ∷ s′) (refl , refl)
    rewrite to∘from s′ (refl , refl)
    = refl

string-sem : ∀ {s} → s ∈ string s · s
string-sem = Inverse.from string-sem′ ⟨$⟩ (refl , refl)

------------------------------------------------------------------------
-- Expressiveness

-- Every language that can be recursively enumerated can be
-- represented by a (unit-valued) grammar.
--
-- Note that, given a Turing machine that halts and accepts for
-- certain strings, and runs forever for other strings, one can define
-- a potentially infinite list of type Colist (Maybe (List Char)) that
-- contains exactly the strings accepted by the Turing machine
-- (assuming that there is some way to construct a stream containing
-- all strings of type List Char).

expressive : (enumeration : Colist (Maybe (List Char))) →
             ∃ λ (g : Grammar ⊤) →
               ∀ {s} → tt ∈ g · s ↔ just s ∈ enumeration
expressive ss = (g ss , g-sem ss)
  where
  maybe-string : Maybe (List Char) → Grammar ⊤
  maybe-string nothing  = fail
  maybe-string (just s) = tt <$ string s

  g : Colist (Maybe (List Char)) → Grammar ⊤
  g []       = fail
  g (s ∷ ss) = maybe-string s ∣ ♯ g (♭ ss)

  maybe-string-sem : ∀ {m s} → tt ∈ maybe-string m · s ↔ just s ≡ m
  maybe-string-sem {nothing} = record
    { to         = P.→-to-⟶ (λ ())
    ; from       = P.→-to-⟶ (λ ())
    ; inverse-of = record
      { left-inverse-of  = λ ()
      ; right-inverse-of = λ ()
      }
    }
  maybe-string-sem {just s} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = to∘from
      }
    }
    where
    to : ∀ {s′} →
         tt ∈ tt <$ string s · s′ → Maybe.just s′ ≡ just s
    to (<$-sem s∈) =
      P.sym $ P.cong just $ proj₂ (Inverse.to string-sem′ ⟨$⟩ s∈)

    from : ∀ {s′} →
           Maybe.just s′ ≡ just s → tt ∈ tt <$ string s · s′
    from refl = <$-sem (Inverse.from string-sem′ ⟨$⟩ (refl , refl))

    from∘to : ∀ {s′} (tt∈ : tt ∈ tt <$ string s · s′) →
              from (to tt∈) ≡ tt∈
    from∘to (<$-sem s∈)
      with Inverse.to string-sem′ ⟨$⟩ s∈
         | Inverse.left-inverse-of string-sem′ s∈
    from∘to (<$-sem .(Inverse.from string-sem′ ⟨$⟩ (refl , refl)))
      | (refl , refl) | refl = refl

    to∘from : ∀ {s′} (eq : Maybe.just s′ ≡ just s) →
              to (from eq) ≡ eq
    to∘from refl
      rewrite Inverse.right-inverse-of
                (string-sem′ {s = s}) (refl , refl)
      = refl

  g-sem : ∀ ss {s} → tt ∈ g ss · s ↔ just s ∈ ss
  g-sem ss = record
    { to         = P.→-to-⟶ (to   ss)
    ; from       = P.→-to-⟶ (from ss)
    ; inverse-of = record
      { left-inverse-of  = from∘to ss
      ; right-inverse-of = to∘from ss
      }
    }
    where
    to : ∀ ss {s} → tt ∈ g ss · s → just s ∈ ss
    to []       ()
    to (s ∷ ss) (left-sem  tt∈) = here (Inverse.to maybe-string-sem ⟨$⟩ tt∈)
    to (s ∷ ss) (right-sem tt∈) = there (to (♭ ss) tt∈)

    from : ∀ ss {s} → just s ∈ ss → tt ∈ g ss · s
    from []       ()
    from (s ∷ ss) (here eq) = left-sem (Inverse.from maybe-string-sem ⟨$⟩ eq)
    from (s ∷ ss) (there p) = right-sem (from (♭ ss) p)

    from∘to : ∀ ss {s} (tt∈ : tt ∈ g ss · s) → from ss (to ss tt∈) ≡ tt∈
    from∘to []       ()
    from∘to (s ∷ ss) (right-sem tt∈) = P.cong right-sem (from∘to (♭ ss) tt∈)
    from∘to (s ∷ ss) (left-sem  tt∈) =
      P.cong left-sem (Inverse.left-inverse-of maybe-string-sem tt∈)

    to∘from : ∀ ss {s} (eq : just s ∈ ss) → to ss (from ss eq) ≡ eq
    to∘from []       ()
    to∘from (s ∷ ss) (there p) = P.cong there (to∘from (♭ ss) p)
    to∘from (s ∷ ss) (here eq) =
      P.cong here (Inverse.right-inverse-of maybe-string-sem eq)

------------------------------------------------------------------------
-- Detecting the whitespace combinator

-- A predicate for the whitespace combinator.

data Is-whitespace : ∀ {A} → Grammar A → Set₁ where
  is-whitespace : Is-whitespace whitespace

-- Detects the whitespace combinator.

is-whitespace? : ∀ {A} (g : Grammar A) → Maybe (Is-whitespace g)
is-whitespace? (_∣_ {c₁ = false} {c₂ = false} (tok ' ') g) =
  helper _ refl
  where
  helper : ∀ {A} (g : Grammar A) (eq : A ≡ Char) →
           Maybe (Is-whitespace (tok ' ' ∣ P.subst Grammar eq g))
  helper (tok '\n') refl = just is-whitespace
  helper _          _    = nothing

is-whitespace? _ = nothing

------------------------------------------------------------------------
-- Trailing whitespace

-- A predicate for grammars that can "swallow" extra trailing
-- whitespace.

Trailing-whitespace : ∀ {A} → Grammar A → Set₁
Trailing-whitespace g =
  ∀ {x s} → x ∈ g <⊛ whitespace ⋆ · s → x ∈ g · s

-- A similar but weaker property.

Trailing-whitespace′ : ∀ {A} → Grammar A → Set₁
Trailing-whitespace′ g =
  ∀ {x s s₁ s₂} →
  x ∈ g · s₁ → s ∈ whitespace ⋆ · s₂ → ∃ λ y → y ∈ g · s₁ ++ s₂

-- A heuristic (and rather incomplete) procedure that either proves
-- that a production can swallow trailing whitespace (in the weaker
-- sense), or returns "don't know" as the answer.
--
-- The natural number n is used to ensure termination.

trailing-whitespace′ : ∀ (n : ℕ) {A} (g : Grammar A) →
                       Maybe (Trailing-whitespace′ g)
trailing-whitespace′ = trailing?
  where
  <$>-lemma : ∀ {c A B} {f : A → B} {g : ∞Grammar c A} →
              Trailing-whitespace′ (♭? g) →
              Trailing-whitespace′ (f <$> g)
  <$>-lemma t (<$>-sem x∈) w = -, <$>-sem (proj₂ $ t x∈ w)

  <$-lemma : ∀ {c A B} {x : A} {g : ∞Grammar c B} →
             Trailing-whitespace′ (♭? g) →
             Trailing-whitespace′ (x <$ g)
  <$-lemma t (<$-sem x∈) w = -, <$-sem (proj₂ $ t x∈ w)

  ⊛-lemma : ∀ {c₁ c₂ A B}
              {g₁ : ∞Grammar c₁ (A → B)} {g₂ : ∞Grammar c₂ A} →
            Trailing-whitespace′ (♭? g₂) →
            Trailing-whitespace′ (g₁ ⊛ g₂)
  ⊛-lemma t₂ (⊛-sem {s₁ = s₁} f∈ x∈) w =
    -, cast (P.sym $ LM.assoc s₁ _ _)
            (⊛-sem f∈ (proj₂ $ t₂ x∈ w))

  <⊛-lemma : ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
             Trailing-whitespace′ (♭? g₂) →
             Trailing-whitespace′ (g₁ <⊛ g₂)
  <⊛-lemma t₂ (<⊛-sem {s₁ = s₁} x∈ y∈) w =
    -, cast (P.sym $ LM.assoc s₁ _ _)
            (<⊛-sem x∈ (proj₂ $ t₂ y∈ w))

  ⊛>-lemma : ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
             Trailing-whitespace′ (♭? g₂) →
             Trailing-whitespace′ (g₁ ⊛> g₂)
  ⊛>-lemma t₂ (⊛>-sem {s₁ = s₁} x∈ y∈) w =
    -, cast (P.sym $ LM.assoc s₁ _ _)
            (⊛>-sem x∈ (proj₂ $ t₂ y∈ w))

  ∣-lemma : ∀ {c₁ c₂ A} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A} →
            Trailing-whitespace′ (♭? g₁) →
            Trailing-whitespace′ (♭? g₂) →
            Trailing-whitespace′ (g₁ ∣ g₂)
  ∣-lemma t₁ t₂ (left-sem  x∈) w = -, left-sem  (proj₂ $ t₁ x∈ w)
  ∣-lemma t₁ t₂ (right-sem x∈) w = -, right-sem (proj₂ $ t₂ x∈ w)

  whitespace⋆-lemma :
    ∀ {A} {g : Grammar A} →
    Is-whitespace g →
    Trailing-whitespace′ (g ⋆)
  whitespace⋆-lemma is-whitespace xs∈ w = -, ⋆-⋆-sem xs∈ w

  trailing? : ℕ → ∀ {A} (g : Grammar A) → Maybe (Trailing-whitespace′ g)
  trailing? (suc n) fail               = just (λ ())
  trailing? (suc n) (f <$> g)          = <$>-lemma <$>M trailing? n (♭? g)
  trailing? (suc n) (x <$ g)           = <$-lemma  <$>M trailing? n (♭? g)
  trailing? (suc n) (g₁ ⊛ g₂)          = ⊛-lemma   <$>M trailing? n (♭? g₂)
  trailing? (suc n) (g₁ <⊛ g₂)         = <⊛-lemma  <$>M trailing? n (♭? g₂)
  trailing? (suc n) (g₁ ⊛> g₂)         = ⊛>-lemma  <$>M trailing? n (♭? g₂)
  trailing? (suc n) (g₁ ∣ g₂)          = ∣-lemma   <$>M trailing? n (♭? g₁)
                                                     ⊛M trailing? n (♭? g₂)
  trailing? (suc n) (_⋆ {c = false} g) = whitespace⋆-lemma <$>M
                                           is-whitespace? g
  trailing? _       _                  = nothing

-- A heuristic (and rather incomplete) procedure that either proves
-- that a production can swallow trailing whitespace, or returns
-- "don't know" as the answer.
--
-- The natural number n is used to ensure termination.

trailing-whitespace : ∀ (n : ℕ) {A} (g : Grammar A) →
                      Maybe (Trailing-whitespace g)
trailing-whitespace n g = convert <$>M trailing? n g
  where
  -- An alternative formulation of Trailing-whitespace.

  Trailing-whitespace″ : ∀ {A} → Grammar A → Set₁
  Trailing-whitespace″ g =
    ∀ {x s s₁ s₂} →
    x ∈ g · s₁ → s ∈ whitespace ⋆ · s₂ → x ∈ g · s₁ ++ s₂

  convert : ∀ {A} {g : Grammar A} →
            Trailing-whitespace″ g → Trailing-whitespace g
  convert t (<⊛-sem x∈ w) = t x∈ w

  ++-lemma : ∀ s₁ {s₂} → (s₁ ++ s₂) ++ [] ≡ (s₁ ++ []) ++ s₂
  ++-lemma _ = solve (++-monoid Char)

  <$>-lemma : ∀ {c A B} {f : A → B} {g : ∞Grammar c A} →
              Trailing-whitespace″ (♭? g) →
              Trailing-whitespace″ (f <$> g)
  <$>-lemma t (<$>-sem x∈) w = <$>-sem (t x∈ w)

  <$-lemma : ∀ {c A B} {x : A} {g : ∞Grammar c B} →
             Trailing-whitespace′ (♭? g) →
             Trailing-whitespace″ (x <$ g)
  <$-lemma t (<$-sem x∈) w = <$-sem (proj₂ $ t x∈ w)

  ⊛-return-lemma :
    ∀ {c A B} {g : ∞Grammar c (A → B)} {x} →
    Trailing-whitespace″ (♭? g) →
    Trailing-whitespace″ (g ⊛ return x)
  ⊛-return-lemma t (⊛-sem {s₁ = s₁} f∈ return-sem) w =
    cast (++-lemma s₁)
         (⊛-sem (t f∈ w) return-sem)

  +-lemma :
    ∀ {c A} {g : ∞Grammar c A} →
    Trailing-whitespace″ (♭? g) →
    Trailing-whitespace″ (g +)
  +-lemma t (⊛-sem {s₁ = s₁} (<$>-sem x∈) ⋆-[]-sem) w =
    cast (++-lemma s₁)
         (+-sem (t x∈ w) ⋆-[]-sem)
  +-lemma t (⊛-sem {s₁ = s₁} (<$>-sem x∈) (⋆-+-sem xs∈)) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (+-∷-sem x∈ (+-lemma t xs∈ w))

  ⊛-⋆-lemma :
    ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ (List A → B)} {g₂ : ∞Grammar c₂ A} →
    Trailing-whitespace″ (♭? g₁) →
    Trailing-whitespace″ (♭? g₂) →
    Trailing-whitespace″ (g₁ ⊛ g₂ ⋆)
  ⊛-⋆-lemma t₁ t₂ (⊛-sem {s₁ = s₁} f∈ ⋆-[]-sem) w =
    cast (++-lemma s₁)
         (⊛-sem (t₁ f∈ w) ⋆-[]-sem)
  ⊛-⋆-lemma t₁ t₂ (⊛-sem {s₁ = s₁} f∈ (⋆-+-sem xs∈)) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (⊛-sem f∈ (⋆-+-sem (+-lemma t₂ xs∈ w)))

  ⊛-∣-lemma : ∀ {c₁ c₂₁ c₂₂ A B} {g₁ : ∞Grammar c₁ (A → B)}
                {g₂₁ : ∞Grammar c₂₁ A} {g₂₂ : ∞Grammar c₂₂ A} →
              Trailing-whitespace″ (g₁ ⊛ g₂₁) →
              Trailing-whitespace″ (g₁ ⊛ g₂₂) →
              Trailing-whitespace″ (g₁ ⊛ (g₂₁ ∣ g₂₂))
  ⊛-∣-lemma t₁₂ t₁₃ {s₂ = s₃}
            (⊛-sem {f = f} {x = x} {s₁ = s₁} {s₂ = s₂}
                   f∈ (left-sem x∈)) w
    with f x | (s₁ ++ s₂) ++ s₃ | t₁₂ (⊛-sem f∈ x∈) w
  ... | ._ | ._ | ⊛-sem f∈′ x∈′ = ⊛-sem f∈′ (left-sem x∈′)
  ⊛-∣-lemma t₁₂ t₁₃ {s₂ = s₃}
            (⊛-sem {f = f} {x = x} {s₁ = s₁} {s₂ = s₂}
                   f∈ (right-sem x∈)) w
    with f x | (s₁ ++ s₂) ++ s₃ | t₁₃ (⊛-sem f∈ x∈) w
  ... | ._ | ._ | ⊛-sem f∈′ x∈′ = ⊛-sem f∈′ (right-sem x∈′)

  ⊛-lemma : ∀ {c₁ c₂ A B}
              {g₁ : ∞Grammar c₁ (A → B)} {g₂ : ∞Grammar c₂ A} →
            Trailing-whitespace″ (♭? g₂) →
            Trailing-whitespace″ (g₁ ⊛ g₂)
  ⊛-lemma t₂ (⊛-sem {s₁ = s₁} f∈ x∈) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (⊛-sem f∈ (t₂ x∈ w))

  <⊛-return-lemma :
    ∀ {c A B} {g : ∞Grammar c A} {x : B} →
    Trailing-whitespace″ (♭? g) →
    Trailing-whitespace″ (g <⊛ return x)
  <⊛-return-lemma t (<⊛-sem {s₁ = s₁} f∈ return-sem) w =
    cast (++-lemma s₁)
         (<⊛-sem (t f∈ w) return-sem)

  <⊛-lemma : ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
             Trailing-whitespace′ (♭? g₂) →
             Trailing-whitespace″ (g₁ <⊛ g₂)
  <⊛-lemma t₂ (<⊛-sem {s₁ = s₁} x∈ y∈) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (<⊛-sem x∈ (proj₂ $ t₂ y∈ w))

  ⊛>-lemma : ∀ {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
             Trailing-whitespace″ (♭? g₂) →
             Trailing-whitespace″ (g₁ ⊛> g₂)
  ⊛>-lemma t₂ (⊛>-sem {s₁ = s₁} x∈ y∈) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (⊛>-sem x∈ (t₂ y∈ w))

  ∣-lemma : ∀ {c₁ c₂ A} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A} →
            Trailing-whitespace″ (♭? g₁) →
            Trailing-whitespace″ (♭? g₂) →
            Trailing-whitespace″ (g₁ ∣ g₂)
  ∣-lemma t₁ t₂ (left-sem  x∈) w = left-sem  (t₁ x∈ w)
  ∣-lemma t₁ t₂ (right-sem x∈) w = right-sem (t₂ x∈ w)

  trailing? : ℕ → ∀ {A} (g : Grammar A) → Maybe (Trailing-whitespace″ g)

  trailing? (suc n) fail = just (λ ())

  trailing? (suc n) (f <$> g) = <$>-lemma <$>M trailing? n (♭? g)
  trailing? (suc n) (x <$ g)  = <$-lemma  <$>M trailing-whitespace′ (suc n) (♭? g)

  trailing? (suc n) (_⊛_ {c₂ = false} g  (return x))  = ⊛-return-lemma <$>M trailing? n (♭? g)
  trailing? (suc n) (_⊛_ {c₂ = false} g₁ (g₂ ⋆))      = ⊛-⋆-lemma      <$>M trailing? n (♭? g₁)
                                                                         ⊛M trailing? n (♭? g₂)
  trailing? (suc n) (_⊛_ {c₂ = false} g₁ (g₂₁ ∣ g₂₂)) = ⊛-∣-lemma      <$>M trailing? n (g₁ ⊛ g₂₁)
                                                                         ⊛M trailing? n (g₁ ⊛ g₂₂)
  trailing? (suc n) (_⊛_              g₁ g₂)          = ⊛-lemma        <$>M trailing? n (♭? g₂)

  trailing? (suc n) (_<⊛_ {c₂ = false} g  (return x)) = <⊛-return-lemma <$>M trailing? n (♭? g)
  trailing? (suc n) (_<⊛_              g₁ g₂)         = <⊛-lemma <$>M
                                                          trailing-whitespace′ (suc n) (♭? g₂)

  trailing? (suc n) (g₁ ⊛> g₂) = ⊛>-lemma <$>M trailing? n (♭? g₂)

  trailing? (suc n) (g₁ ∣ g₂) = ∣-lemma <$>M trailing? n (♭? g₁)
                                          ⊛M trailing? n (♭? g₂)

  trailing? _ _ = nothing

private

  -- Some unit tests.

  test₁ : T (is-just (trailing-whitespace′ 1 (whitespace ⋆)))
  test₁ = _

  test₂ : T (is-just (trailing-whitespace′ 2 (whitespace +)))
  test₂ = _

  test₃ : T (is-just (trailing-whitespace 1 (tt <$ whitespace ⋆)))
  test₃ = _

  test₄ : T (is-just (trailing-whitespace 2 (tt <$ whitespace +)))
  test₄ = _

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
{- Copyright © 2015 Benjamin Barenblat

Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
this file except in compliance with the License.  You may obtain a copy of the
License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed
under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
CONDITIONS OF ANY KIND, either express or implied.  See the License for the
specific language governing permissions and limitations under the License. -}

module B.Prelude.Eq where

import Data.Bool as Bool
open Bool using (Bool)
import Data.Char as Char
open Char using (Char)
import Data.Nat as ℕ
open ℕ using (ℕ)
open import Function using (_$_)
import Level
open Level using (_⊔_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary using (DecSetoid)

record Eq {c} {ℓ} (t : Set c) : Set (Level.suc $ c ⊔ ℓ) where
  field
    decSetoid : DecSetoid c ℓ

  _≟_ = DecSetoid._≟_ decSetoid

  _==_ : DecSetoid.Carrier decSetoid
       → DecSetoid.Carrier decSetoid
       → Bool
  x == y = ⌊ x ≟ y ⌋

open Eq ⦃...⦄ public

instance
  Eq-Bool : Eq Bool
  Eq-Bool = record { decSetoid = Bool.decSetoid }

  Eq-Char : Eq Char
  Eq-Char = record { decSetoid = Char.decSetoid }

  -- TODO: Float

  Eq-ℕ : Eq ℕ
  Eq-ℕ =
    let module DecTotalOrder = Relation.Binary.DecTotalOrder in
    record { decSetoid = DecTotalOrder.Eq.decSetoid ℕ.decTotalOrder }

max_stars_repo_name: bbarenblat/B

max_issues_repo_name: bbarenblat/B

max_forks_repo_name: bbarenblat/B


text:
module FRP.JS.Bool where

open import FRP.JS.Primitive public using ( Bool ; true ; false )

not : Bool → Bool
not true  = false
not false = true

{-# COMPILED_JS not function(x) { return !x; } #-}

_≟_ : Bool → Bool → Bool
true  ≟ b = b
false ≟ b = not b

{-# COMPILED_JS _≟_ function(x) { return function(y) { return x === y; }; } #-}

if_then_else_ : ∀ {α} {A : Set α} → Bool → A → A → A
if true  then t else f = t
if false then t else f = f

{-# COMPILED_JS if_then_else_ function(a) { return function(A) { return function(x) {
  if (x) { return function(t) { return function(f) { return t; }; }; }
  else { return function(t) { return function(f) { return f; }; }; }
}; }; } #-}

_∧_ : Bool → Bool → Bool
true  ∧ b = b
false ∧ b = false

{-# COMPILED_JS _∧_ function(x) { return function(y) { return x && y; }; } #-}

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

{-# COMPILED_JS _∨_ function(x) { return function(y) { return x || y; }; } #-}

_xor_ : Bool → Bool → Bool
true  xor b = not b
false xor b = b

_≠_ = _xor_

{-# COMPILED_JS _xor_ function(x) { return function(y) { return x !== y; }; } #-}
{-# COMPILED_JS _≠_ function(x) { return function(y) { return x !== y; }; } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js