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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped as U
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Reduction

open import Tools.Product
import Tools.PropositionalEquality as PE

import Data.Fin as Fin
import Data.Nat as Nat

-- The different cases of the logical relation are spread out through out
-- this file. This is due to them having different dependencies.

-- We will refer to expressions that satisfies the logical relation as reducible.

-- Reducibility of Neutrals:

-- Neutral type
record _⊩ne_^[_,_] (Γ : Con Term) (A : Term) (r : Relevance) (l : Level) : Set where
  constructor ne
  field
    K   : Term
    D   : Γ ⊢ A :⇒*: K ^ [ r , ι l ]
    neK : Neutral K
    K≡K : Γ ⊢ K ~ K ∷ (Univ r l) ^ [ ! , next l ]

-- Neutral type equality
record _⊩ne_≡_^[_,_]/_ (Γ : Con Term) (A B : Term) (r : Relevance) (l : Level) ([A] : Γ ⊩ne A ^[ r , l ]) : Set where
  constructor ne₌
  open _⊩ne_^[_,_] [A]
  field
    M   : Term
    D′  : Γ ⊢ B :⇒*: M ^ [ r , ι l ]
    neM : Neutral M
    K≡M : Γ ⊢ K ~ M ∷ (Univ r l) ^ [ ! , next l ]

-- Neutral term in WHNF
record _⊩neNf_∷_^_ (Γ : Con Term) (k A : Term) (r : TypeInfo) : Set where
  inductive
  constructor neNfₜ
  field
    neK  : Neutral k
    ⊢k   : Γ ⊢ k ∷ A ^ r
    k≡k  : Γ ⊢ k ~ k ∷ A ^ r

-- Neutral relevant term
record _⊩ne_∷_^_/_ (Γ : Con Term) (t A : Term) (l : Level) ([A] : Γ ⊩ne A ^[ ! , l ]) : Set where
  inductive
  constructor neₜ
  open _⊩ne_^[_,_] [A]
  field
    k   : Term
    d   : Γ ⊢ t :⇒*: k ∷ K ^ ι l
    nf  : Γ ⊩neNf k ∷ K ^ [ ! , ι l ]

-- Neutral irrelevant term
record _⊩neIrr_∷_^_/_ (Γ : Con Term) (t A : Term) (l : Level) ([A] : Γ ⊩ne A ^[ % , l ]) : Set where
  inductive
  constructor neₜ
  open _⊩ne_^[_,_] [A]
  field
    d : Γ ⊢ t ∷ A ^ [ % , ι l ]

-- Neutral term equality in WHNF
record _⊩neNf_≡_∷_^_ (Γ : Con Term) (k m A : Term) (r : TypeInfo) : Set where
  inductive
  constructor neNfₜ₌
  field
    neK  : Neutral k
    neM  : Neutral m
    k≡m  : Γ ⊢ k ~ m ∷ A ^ r

-- Neutral relevant term equality
record _⊩ne_≡_∷_^_/_ (Γ : Con Term) (t u A : Term) (l : Level) ([A] : Γ ⊩ne A ^[ ! , l ]) : Set where
  constructor neₜ₌
  open _⊩ne_^[_,_] [A]
  field
    k m : Term
    d   : Γ ⊢ t :⇒*: k ∷ K ^ ι l
    d′  : Γ ⊢ u :⇒*: m ∷ K ^ ι l
    nf  : Γ ⊩neNf k ≡ m ∷ K ^ [ ! , ι l ]

-- Neutral irrelevant term equality
record _⊩neIrr_≡_∷_^_/_ (Γ : Con Term) (t u A : Term) (l : Level) ([A] : Γ ⊩ne A ^[ % , l ]) : Set where
  constructor neₜ₌
  open _⊩ne_^[_,_] [A]
  field
    d   : Γ ⊢ t ∷ A ^ [ % , ι l ]
    d′  : Γ ⊢ u ∷ A ^ [ % , ι l ]

-- Reducibility of natural numbers:

-- Natural number type
_⊩ℕ_ : (Γ : Con Term) (A : Term) → Set
Γ ⊩ℕ A = Γ ⊢ A :⇒*: ℕ ^ [ ! , ι ⁰ ]

-- Natural number type equality
_⊩ℕ_≡_ : (Γ : Con Term) (A B : Term) → Set
Γ ⊩ℕ A ≡ B = Γ ⊢ B ⇒* ℕ ^ [ ! , ι ⁰ ]

mutual
  -- Natural number term
  data _⊩ℕ_∷ℕ (Γ : Con Term) (t : Term) : Set where
    ℕₜ : (n : Term) (d : Γ ⊢ t :⇒*: n ∷ ℕ ^ ι ⁰) (n≡n : Γ ⊢ n ≅ n ∷ ℕ ^ [ ! , ι ⁰ ])
         (prop : Natural-prop Γ n)
       → Γ ⊩ℕ t ∷ℕ

  -- WHNF property of natural number terms
  data Natural-prop (Γ : Con Term) : (n : Term) → Set where
    sucᵣ  : ∀ {n} → Γ ⊩ℕ n ∷ℕ → Natural-prop Γ (suc n)
    zeroᵣ : Natural-prop Γ zero
    ne    : ∀ {n} → Γ ⊩neNf n ∷ ℕ ^ [ ! , ι ⁰ ] → Natural-prop Γ n

mutual
  -- Natural number term equality
  data _⊩ℕ_≡_∷ℕ (Γ : Con Term) (t u : Term) : Set where
    ℕₜ₌ : (k k′ : Term) (d : Γ ⊢ t :⇒*: k  ∷ ℕ ^ ι ⁰) (d′ : Γ ⊢ u :⇒*: k′ ∷ ℕ ^ ι ⁰)
          (k≡k′ : Γ ⊢ k ≅ k′ ∷ ℕ ^ [ ! , ι ⁰ ])
          (prop : [Natural]-prop Γ k k′) → Γ ⊩ℕ t ≡ u ∷ℕ

  -- WHNF property of Natural number term equality
  data [Natural]-prop (Γ : Con Term) : (n n′ : Term) → Set where
    sucᵣ  : ∀ {n n′} → Γ ⊩ℕ n ≡ n′ ∷ℕ → [Natural]-prop Γ (suc n) (suc n′)
    zeroᵣ : [Natural]-prop Γ zero zero
    ne    : ∀ {n n′} → Γ ⊩neNf n ≡ n′ ∷ ℕ ^ [ ! , ι ⁰ ] → [Natural]-prop Γ n n′

-- Natural extraction from term WHNF property
natural : ∀ {Γ n} → Natural-prop Γ n → Natural n
natural (sucᵣ x) = sucₙ
natural zeroᵣ = zeroₙ
natural (ne (neNfₜ neK ⊢k k≡k)) = ne neK

-- Natural extraction from term equality WHNF property
split : ∀ {Γ a b} → [Natural]-prop Γ a b → Natural a × Natural b
split (sucᵣ x) = sucₙ , sucₙ
split zeroᵣ = zeroₙ , zeroₙ
split (ne (neNfₜ₌ neK neM k≡m)) = ne neK , ne neM

-- Reducibility of Empty

-- Empty type
_⊩Empty_^_ : (Γ : Con Term) (A : Term) (l : Level) → Set
Γ ⊩Empty A ^ l = Γ ⊢ A :⇒*: Empty l ^ [ % , ι l ]

-- Empty type equality
_⊩Empty_≡_^_ : (Γ : Con Term) (A B : Term) (l : Level) → Set
Γ ⊩Empty A ≡ B ^ l = Γ ⊢ B ⇒* Empty l ^ [ % , ι l ]

data Empty-prop (Γ : Con Term) (n : Term) (l : Level) : Set where
  ne    : Γ ⊢ n ∷ Empty l ^ [ % , ι l ] → Empty-prop Γ n l

-- -- Empty term

data _⊩Empty_∷Empty^_ (Γ : Con Term) (t : Term) (l : Level) : Set where
  Emptyₜ : (prop : Empty-prop Γ t l) → Γ ⊩Empty t ∷Empty^ l

data [Empty]-prop (Γ : Con Term) : (n n′ : Term)  (l : Level) → Set where
  ne    : ∀ {n n′ l} → Γ ⊢ n ∷ Empty l ^ [ % , ι l ] → Γ ⊢ n′ ∷ Empty l ^ [ % , ι l ]  → [Empty]-prop Γ n n′ l

-- Empty term equality
data _⊩Empty_≡_∷Empty^_ (Γ : Con Term) (t u : Term) (l : Level) : Set where
  Emptyₜ₌ : (prop : [Empty]-prop Γ t u l) → Γ ⊩Empty t ≡ u ∷Empty^ l

-- Logical relation

record LogRelKit : Set₁ where
  constructor Kit
  field
    _⊩U_^_ : (Γ : Con Term) → Term → TypeLevel → Set
    _⊩Π_^[_,_] : (Γ : Con Term) → Term → Relevance → Level → Set
    _⊩∃_^_ : (Γ : Con Term) → Term → Level → Set

    _⊩_^_ : (Γ : Con Term) → Term → TypeInfo → Set
    _⊩_≡_^_/_ : (Γ : Con Term) (A B : Term) (r : TypeInfo) → Γ ⊩ A ^ r → Set
    _⊩_∷_^_/_ : (Γ : Con Term) (t A : Term) (r : TypeInfo) → Γ ⊩ A ^ r → Set
    _⊩_≡_∷_^_/_ : (Γ : Con Term) (t u A : Term) (r : TypeInfo) → Γ ⊩ A ^ r → Set

module LogRel (l : TypeLevel) (rec : ∀ {l′} → l′ <∞ l → LogRelKit) where

  -- Reducibility of Universe:

  -- Universe type
  record _⊩¹U_^_ (Γ : Con Term) (A : Term) (ll : TypeLevel) : Set where
    constructor Uᵣ
    field
      r : Relevance
      l′ : Level
      l< : ι l′ <∞ l
      eq : next l′ PE.≡ ll
      d : Γ ⊢ A :⇒*: Univ r l′ ^ [ ! , next l′ ]

  -- Universe type equality
  _⊩¹U_≡_^_/_ : (Γ : Con Term) (A B : Term) (ll : TypeLevel) ([A] : Γ ⊩¹U A ^ ll) → Set
  Γ ⊩¹U A ≡ B ^ ll / [A] = Γ ⊢ B ⇒* Univ (_⊩¹U_^_.r [A]) (_⊩¹U_^_.l′ [A]) ^ [ ! , ll ]

  -- Universe term
  record _⊩¹U_∷_^_/_  (Γ : Con Term) (t : Term) (A : Term) (ll : TypeLevel) ([A] : Γ ⊩¹U A ^ ll) : Set where
    constructor Uₜ
    open _⊩¹U_^_ [A]
    open LogRelKit (rec l<)
    field
      K    : Term
      d     : Γ ⊢ t :⇒*: K ∷ Univ r l′ ^ next l′
      typeK : Type K
      K≡K   : Γ ⊢ K ≅ K ∷ Univ r l′ ^ [ ! , next l′ ]
      [t]   : ∀ {ρ Δ} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ) → Δ ⊩ U.wk ρ t ^ [ r , ι l′ ]

  -- Universe term equality
  record _⊩¹U_≡_∷_^_/_ (Γ : Con Term) (t u : Term) (X : Term) (ll : TypeLevel) ([X] : Γ ⊩¹U X ^ ll) : Set where
    constructor Uₜ₌
    open _⊩¹U_^_ [X]
    open LogRelKit (rec l<)
    field
      [t]   : Γ ⊩¹U t ∷ X ^ ll / [X]
      [u]   : Γ ⊩¹U u ∷ X ^ ll / [X]
      A≡B   : Γ ⊢ _⊩¹U_∷_^_/_.K [t] ≅ _⊩¹U_∷_^_/_.K [u] ∷ Univ r l′ ^ [ ! , next l′ ]
      [t≡u] : ∀ {ρ Δ} → ([ρ] : ρ ∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ) → Δ ⊩ U.wk ρ t ≡ U.wk ρ u ^ [ r , ι l′ ] / _⊩¹U_∷_^_/_.[t] [t] [ρ] ⊢Δ

  mutual

    -- Reducibility of Π:

    -- Π-type
    record _⊩¹Π_^[_,_] (Γ : Con Term) (A : Term) (r : Relevance) (lΠ : Level)  : Set where
      inductive
      eta-equality
      constructor Πᵣ
      field
        rF : Relevance
        lF : Level
        lG : Level
        lF≤ : lF ≤ lΠ
        lG≤ : lG ≤ lΠ
        F : Term
        G : Term
        D : Γ ⊢ A :⇒*: Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ r , ι lΠ ]
        ⊢F : Γ ⊢ F ^ [ rF , ι lF ]
        ⊢G : Γ ∙ F ^ [ rF , ι lF ] ⊢ G ^ [ r , ι lG ]
        A≡A : Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ≅ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ r , ι lΠ ]
        [F] : ∀ {ρ Δ} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ) → Δ ⊩¹ U.wk ρ F ^ [ rF , ι lF ]
        [G] : ∀ {ρ Δ a}
            → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
            → Δ ⊩¹ a ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ
            → Δ ⊩¹ U.wk (lift ρ) G [ a ] ^ [ r , ι lG ]
        G-ext : ∀ {ρ Δ a b}
              → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
              → ([a] : Δ ⊩¹ a ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
              → ([b] : Δ ⊩¹ b ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
              → Δ ⊩¹ a ≡ b ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ
              → Δ ⊩¹ U.wk (lift ρ) G [ a ] ≡ U.wk (lift ρ) G [ b ] ^ [ r , ι lG ] / [G] [ρ] ⊢Δ [a]

    -- Π-type equality
    record _⊩¹Π_≡_^[_,_]/_ (Γ : Con Term) (A B : Term) (r : Relevance) (lΠ : Level) ([A] : Γ ⊩¹Π A ^[ r , lΠ ]) : Set where
      inductive
      eta-equality
      constructor Π₌
      open _⊩¹Π_^[_,_] [A]
      field
        F′     : Term
        G′     : Term
        D′     : Γ ⊢ B ⇒* Π F′ ^ rF ° lF ▹ G′ ° lG ° lΠ ^ [ r , ι lΠ ]
        A≡B    : Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ≅ Π F′ ^ rF ° lF ▹ G′ ° lG ° lΠ ^ [ r , ι lΠ ]
        [F≡F′] : ∀ {ρ Δ}
               → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
               → Δ ⊩¹ U.wk ρ F ≡ U.wk ρ F′ ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ
        [G≡G′] : ∀ {ρ Δ a}
               → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
               → ([a] : Δ ⊩¹ a ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
               → Δ ⊩¹ U.wk (lift ρ) G [ a ] ≡ U.wk (lift ρ) G′ [ a ] ^ [ r , ι lG ] / [G] [ρ] ⊢Δ [a]

    -- relevant Term of Π-type
    _⊩¹Π_∷_^_/_ : (Γ : Con Term) (t A : Term) (lΠ : Level) ([A] : Γ ⊩¹Π A ^[ ! , lΠ ]) → Set
    Γ ⊩¹Π t ∷ A ^ lΠ / Πᵣ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext =
      ∃ λ f → Γ ⊢ t :⇒*: f ∷ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ ι lΠ
            × Function f
            × Γ ⊢ f ≅ f ∷ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ ! , ι lΠ ]
            × (∀ {ρ Δ a b}
              → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                ([a] : Δ ⊩¹ a ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
                ([b] : Δ ⊩¹ b ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
                ([a≡b] : Δ ⊩¹ a ≡ b ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
              → Δ ⊩¹ U.wk ρ f ∘ a ^ lΠ ≡ U.wk ρ f ∘ b ^ lΠ ∷ U.wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [G] [ρ] ⊢Δ [a])
            × (∀ {ρ Δ a} → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
              → ([a] : Δ ⊩¹ a ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
              → Δ ⊩¹ U.wk ρ f ∘ a ^ lΠ ∷ U.wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [G] [ρ] ⊢Δ [a])
    -- Issue: Agda complains about record use not being strictly positive.
    --        Therefore we have to use ×

    -- Irrelevant term of Π-type
    _⊩¹Πirr_∷_^_/_ : (Γ : Con Term) (t A : Term) (l′ : Level) ([A] : Γ ⊩¹Π A ^[ % , l′ ]) → Set
    Γ ⊩¹Πirr t ∷ A ^ l′ / Πᵣ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext =
      Γ ⊢ t ∷ Π F ^ rF ° lF ▹ G ° lG ° l′ ^ [ % , ι l′ ]

    -- Term equality of Π-type
    _⊩¹Π_≡_∷_^_/_ : (Γ : Con Term) (t u A : Term) (l′ : Level) ([A] : Γ ⊩¹Π A ^[ ! , l′ ]) → Set
    Γ ⊩¹Π t ≡ u ∷ A ^ l′ / Πᵣ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext =
      let [A] = Πᵣ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext
      in  ∃₂ λ f g →
          ( Γ ⊢ t :⇒*: f ∷ Π F ^ rF ° lF ▹ G ° lG ° l′ ^ ι l′ )
      ×   ( Γ ⊢ u :⇒*: g ∷ Π F ^ rF ° lF ▹ G ° lG ° l′ ^ ι l′ )
      ×   Function f
      ×   Function g
      ×   Γ ⊢ f ≅ g ∷ Π F ^ rF ° lF ▹ G ° lG ° l′ ^ [ ! , ι l′ ]
      ×   Γ ⊩¹Π t ∷ A ^ l′ / [A]
      ×   Γ ⊩¹Π u ∷ A ^ l′ / [A]
      ×   (∀ {ρ Δ a} → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          → ([a] : Δ ⊩¹ a ∷ U.wk ρ F ^ [ rF , ι lF ] / [F] [ρ] ⊢Δ)
          → Δ ⊩¹ U.wk ρ f ∘ a ^ l′ ≡ U.wk ρ g ∘ a ^ l′ ∷ U.wk (lift ρ) G [ a ] ^ [ ! , ι lG ] / [G] [ρ] ⊢Δ [a])
    -- Issue: Same as above.

    -- Irrelevant term equality of Π-type
    _⊩¹Πirr_≡_∷_^_/_ : (Γ : Con Term) (t u A : Term) (l′ : Level) ([A] : Γ ⊩¹Π A ^[ % , l′ ] ) → Set
    Γ ⊩¹Πirr t ≡ u ∷ A ^ l′ / Πᵣ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext =
          (Γ ⊢ t ∷ Π F ^ rF ° lF ▹ G ° lG ° l′ ^ [ % , ι l′ ])
          ×
          (Γ ⊢ u ∷ Π F ^ rF ° lF ▹ G ° lG ° l′ ^ [ % , ι l′ ])

    -- Existential types
    record _⊩¹∃_^_ (Γ : Con Term) (A : Term) (l′ : Level) : Set where
      inductive
      eta-equality
      constructor ∃ᵣ
      field
        F : Term
        G : Term
        D : Γ ⊢ A :⇒*: ∃ F ▹ G ^ [ % , ι l′ ]
        ⊢F : Γ ⊢ F ^ [ % , ι l′ ]
        ⊢G : Γ ∙ F ^ [ % , ι l′ ] ⊢ G ^ [ % , ι l′ ]
        A≡A : Γ ⊢ (∃ F ▹ G) ≅ (∃ F ▹ G) ^ [ % , ι l′ ]
        [F] : ∀ {ρ Δ} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ) → Δ ⊩¹ U.wk ρ F ^ [ % , ι l′ ]
        [G] : ∀ {ρ Δ a}
            → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
            → Δ ⊩¹ a ∷ U.wk ρ F ^ [ % , ι l′ ] / [F] [ρ] ⊢Δ
            → Δ ⊩¹ U.wk (lift ρ) G [ a ] ^ [ % , ι l′ ]
        G-ext : ∀ {ρ Δ a b}
              → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
              → ([a] : Δ ⊩¹ a ∷ U.wk ρ F ^ [ % , ι l′ ] / [F] [ρ] ⊢Δ)
              → ([b] : Δ ⊩¹ b ∷ U.wk ρ F ^ [ % , ι l′ ] / [F] [ρ] ⊢Δ)
              → Δ ⊩¹ a ≡ b ∷ U.wk ρ F ^ [ % , ι l′ ] / [F] [ρ] ⊢Δ
              → Δ ⊩¹ U.wk (lift ρ) G [ a ] ≡ U.wk (lift ρ) G [ b ] ^ [ % , ι l′ ] / [G] [ρ] ⊢Δ [a]

    -- ∃-type equality
    record _⊩¹∃_≡_^_/_ (Γ : Con Term) (A B : Term) (l′ : Level) ([A] : Γ ⊩¹∃ A ^ l′) : Set where
      inductive
      eta-equality
      constructor ∃₌
      open _⊩¹∃_^_ [A]
      field
        F′     : Term
        G′     : Term
        D′     : Γ ⊢ B ⇒* ∃ F′ ▹ G′ ^ [ % , ι l′ ]
        A≡B    : Γ ⊢ ∃ F ▹ G ≅ ∃ F′ ▹ G′ ^ [ % , ι l′ ]
        [F≡F′] : ∀ {ρ Δ}
               → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
               → Δ ⊩¹ U.wk ρ F ≡ U.wk ρ F′ ^ [ % , ι l′ ] / [F] [ρ] ⊢Δ
        [G≡G′] : ∀ {ρ Δ a}
               → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
               → ([a] : Δ ⊩¹ a ∷ U.wk ρ F ^ [ % , ι l′ ] / [F] [ρ] ⊢Δ)
               → Δ ⊩¹ U.wk (lift ρ) G [ a ] ≡ U.wk (lift ρ) G′ [ a ] ^ [ % , ι l′ ] / [G] [ρ] ⊢Δ [a]

    -- Terms of ∃-types (always irrelevant)
    _⊩¹∃_∷_^_/_ : (Γ : Con Term) (t A : Term) (l′ : Level) ([A] : Γ ⊩¹∃ A ^ l′) → Set
    Γ ⊩¹∃ t ∷ A ^ l′ / ∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext =
      Γ ⊢ t ∷ ∃ F ▹ G ^ [ % , ι l′ ]

    -- Term equality for ∃-types
    _⊩¹∃_≡_∷_^_/_ : (Γ : Con Term) (t u A : Term) (l′ : Level) ([A] : Γ ⊩¹∃ A ^ l′) → Set
    Γ ⊩¹∃ t ≡ u ∷ A ^ l′ / ∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext =
          (Γ ⊢ t ∷ ∃ F ▹ G ^ [ % , ι l′ ])
          ×
          (Γ ⊢ u ∷ ∃ F ▹ G ^ [ % , ι l′ ])

    -- Logical relation definition

    data _⊩¹_^_ (Γ : Con Term) : Term → TypeInfo → Set where
      Uᵣ  : ∀ {A ll} → (UA : Γ ⊩¹U A ^ ll) → Γ ⊩¹ A ^ [ ! , ll ]
      ℕᵣ  : ∀ {A} → Γ ⊩ℕ A → Γ ⊩¹ A ^ [ ! , ι ⁰ ]
      Emptyᵣ : ∀ {A l} → Γ ⊩Empty A ^ l → Γ ⊩¹ A ^ [ % , ι l ]
      ne  : ∀ {A r l} → Γ ⊩ne A ^[ r , l ] → Γ ⊩¹ A ^ [ r , ι l ]
      Πᵣ  : ∀ {A r l} → Γ ⊩¹Π A ^[ r , l ] → Γ ⊩¹ A ^ [ r , ι l ]
      ∃ᵣ  : ∀ {A l} → Γ ⊩¹∃ A ^ l → Γ ⊩¹ A ^ [ % , ι l ]
      emb : ∀ {A r l′} (l< : l′ <∞ l) (let open LogRelKit (rec l<))
            ([A] : Γ ⊩ A ^ r) → Γ ⊩¹ A ^ r

    _⊩¹_≡_^_/_ : (Γ : Con Term) (A B : Term) (r : TypeInfo) → Γ ⊩¹ A ^ r  → Set
    Γ ⊩¹ A ≡ B ^ [ .! , l ] / Uᵣ UA = Γ ⊩¹U A ≡ B ^ l / UA
    Γ ⊩¹ A ≡ B ^ [ .! , .ι ⁰ ] / ℕᵣ D = Γ ⊩ℕ A ≡ B
    Γ ⊩¹ A ≡ B ^ [ .% , .ι l ] / Emptyᵣ D = Γ ⊩Empty A ≡ B ^ l
    Γ ⊩¹ A ≡ B ^ [ r , ι l ] / ne neA = Γ ⊩ne A ≡ B ^[ r , l ]/ neA
    Γ ⊩¹ A ≡ B ^ [ r , ι l ] / Πᵣ ΠA =  Γ ⊩¹Π A ≡ B ^[ r , l ]/ ΠA
    Γ ⊩¹ A ≡ B ^ [ .% , ι l ] / ∃ᵣ ∃A = Γ ⊩¹∃ A ≡ B ^ l / ∃A
    Γ ⊩¹ A ≡ B ^ r / emb l< [A] = Γ ⊩ A ≡ B ^ r / [A]
      where open LogRelKit (rec l<)

    _⊩¹_∷_^_/_ : (Γ : Con Term) (t A : Term) (r : TypeInfo) → Γ ⊩¹ A ^ r  → Set
    Γ ⊩¹ t ∷ A ^ [ .! , ll ] / Uᵣ UA = Γ ⊩¹U t ∷ A ^ ll / UA
    Γ ⊩¹ t ∷ A ^ .([ ! , ι ⁰ ]) / ℕᵣ x = Γ ⊩ℕ t ∷ℕ
    Γ ⊩¹ t ∷ A ^ [ .% , ι ll ] / Emptyᵣ x =  Γ ⊩Empty t ∷Empty^ ll
    Γ ⊩¹ t ∷ A ^ .([ ! , ι l ]) / ne {r = !} {l} neA = Γ ⊩ne t ∷ A ^ l / neA
    Γ ⊩¹ t ∷ A ^ .([ % , ι l ]) / ne {r = %} {l} neA = Γ ⊩neIrr t ∷ A ^ l / neA
    Γ ⊩¹ t ∷ A ^ [ ! , ι l ] / Πᵣ ΠA  = Γ ⊩¹Π t ∷ A ^ l / ΠA
    Γ ⊩¹ t ∷ A ^ [ % , ι l ] / Πᵣ ΠA  = Γ ⊩¹Πirr t ∷ A ^ l / ΠA
    Γ ⊩¹ t ∷ A ^ .([ % , ι l ]) / ∃ᵣ {l = l} ∃A = Γ ⊩¹∃ t ∷ A ^ l / ∃A
    Γ ⊩¹ t ∷ A ^ r / emb l< [A] =  Γ ⊩ t ∷ A ^ r / [A]
      where open LogRelKit (rec l<)

    _⊩¹_≡_∷_^_/_ : (Γ : Con Term) (t u A : Term) (r : TypeInfo) → Γ ⊩¹ A ^ r → Set
    Γ ⊩¹ t ≡ u ∷ A ^ [ .! , ll ] / Uᵣ UA = Γ ⊩¹U t ≡ u ∷ A ^ ll / UA
    Γ ⊩¹ t ≡ u ∷ A ^ .([ ! , ι ⁰ ]) / ℕᵣ D = Γ ⊩ℕ t ≡ u ∷ℕ
    Γ ⊩¹ t ≡ u ∷ A ^ [ .% , ι ll ] / Emptyᵣ D = Γ ⊩Empty t ≡ u ∷Empty^ ll
    Γ ⊩¹ t ≡ u ∷ A ^ .([ ! , ι l ]) / ne {r = !} {l} neA = Γ ⊩ne t ≡ u ∷ A ^  l / neA
    Γ ⊩¹ t ≡ u ∷ A ^ .([ % , ι l ]) / ne {r = %} {l} neA = Γ ⊩neIrr t ≡ u ∷ A ^ l / neA
    Γ ⊩¹ t ≡ u ∷ A ^ [ ! , ι l ] / Πᵣ ΠA = Γ ⊩¹Π t ≡ u ∷ A ^ l  / ΠA
    Γ ⊩¹ t ≡ u ∷ A ^ [ % , ι l ] / Πᵣ ΠA = Γ ⊩¹Πirr t ≡ u ∷ A ^ l / ΠA
    Γ ⊩¹ t ≡ u ∷ A ^ .([ % , ι l ]) / ∃ᵣ {l = l} ∃A = Γ ⊩¹∃ t ≡ u ∷ A ^ l / ∃A
    Γ ⊩¹ t ≡ u ∷ A ^ r / emb l< [A] = Γ ⊩ t ≡ u ∷ A ^ r / [A]
      where open LogRelKit (rec l<)

    kit : LogRelKit
    kit = Kit _⊩¹U_^_ _⊩¹Π_^[_,_] _⊩¹∃_^_
              _⊩¹_^_ _⊩¹_≡_^_/_ _⊩¹_∷_^_/_ _⊩¹_≡_∷_^_/_

open LogRel public using (Uᵣ; ℕᵣ; Emptyᵣ; ne; Πᵣ ; ∃ᵣ ; emb; Uₜ; Uₜ₌; Π₌; ∃₌)

-- Patterns for the non-records of Π
pattern Πₜ a b c d e f = a , b , c , d , e , f
pattern Πₜ₌ a b c d e f g h i j = a , b , c , d , e , f , g , h , i , j

pattern Uᵣ′ A ll r l a e d = Uᵣ {A = A} {ll = ll} (Uᵣ r l a e d)
pattern ne′ b c d e = ne (ne b c d e)
pattern Πᵣ′  a a' a'' lf lg b c d e f g h i j = Πᵣ (Πᵣ a a' a'' lf lg b c d e f g h i j)
pattern ∃ᵣ′  a b c d e f g h i = ∃ᵣ (∃ᵣ a b c d e f g h i)

-- we need to split the LogRelKit into the level part and the general part to convince Agda termination checker

logRelRec : ∀ l {l′} → l′ <∞ l → LogRelKit
logRelRec (ι ⁰) = λ ()
logRelRec (ι ¹) X = LogRel.kit (ι ⁰) λ ()
logRelRec ∞ X = LogRel.kit (ι ¹) (λ X → LogRel.kit (ι ⁰) λ ())

kit : ∀ (i : TypeLevel) → LogRelKit
kit l =  LogRel.kit l (logRelRec l)

_⊩′⟨_⟩U_^_ : (Γ : Con Term) (l : TypeLevel) → Term → TypeLevel → Set
Γ ⊩′⟨ l ⟩U A ^ ll = Γ ⊩U A ^ ll where open LogRelKit (kit l)

_⊩′⟨_⟩Π_^[_,_] : (Γ : Con Term) (l : TypeLevel) → Term → Relevance → Level → Set
Γ ⊩′⟨ l ⟩Π A ^[ r , lΠ ] = Γ ⊩Π A ^[ r , lΠ ]  where open LogRelKit (kit l)

_⊩′⟨_⟩∃_^_ : (Γ : Con Term) (l : TypeLevel) → Term → Level → Set
Γ ⊩′⟨ l ⟩∃ A ^ l' = Γ ⊩∃ A ^ l' where open LogRelKit (kit l)

_⊩⟨_⟩_^_ : (Γ : Con Term) (l : TypeLevel) → Term → TypeInfo → Set
Γ ⊩⟨ l ⟩ A ^ r = Γ ⊩ A ^ r where open LogRelKit (kit l)

_⊩⟨_⟩_≡_^_/_ : (Γ : Con Term) (l : TypeLevel) (A B : Term) (r : TypeInfo) → Γ ⊩⟨ l ⟩ A ^ r → Set
Γ ⊩⟨ l ⟩ A ≡ B ^ r / [A] = Γ ⊩ A ≡ B ^ r / [A] where open LogRelKit (kit l)

_⊩⟨_⟩_∷_^_/_ : (Γ : Con Term) (l : TypeLevel) (t A : Term) (r : TypeInfo) → Γ ⊩⟨ l ⟩ A ^ r → Set
Γ ⊩⟨ l ⟩ t ∷ A ^ r / [A] = Γ ⊩ t ∷ A ^ r / [A] where open LogRelKit (kit l)

_⊩⟨_⟩_≡_∷_^_/_ : (Γ : Con Term) (l : TypeLevel) (t u A : Term) (r : TypeInfo) → Γ ⊩⟨ l ⟩ A ^ r → Set
Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ r / [A] = Γ ⊩ t ≡ u ∷ A ^ r / [A] where open LogRelKit (kit l)

-- Well-typed irrelevant terms are always reducible
logRelIrr : ∀ {l t Γ l' A} ([A] : Γ ⊩⟨ l ⟩ A ^ [ % , l' ]) (⊢t : Γ ⊢ t ∷ A ^ [ % , l' ]) → Γ ⊩⟨ l ⟩ t ∷ A ^ [ % , l' ] / [A]
logRelIrr (Emptyᵣ [[ ⊢A , ⊢B , D ]]) ⊢t = Emptyₜ (ne (conv ⊢t (reduction D (id ⊢B) Emptyₙ Emptyₙ (refl ⊢B))))
logRelIrr (ne x) ⊢t = neₜ ⊢t
logRelIrr (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ⊢t = conv ⊢t (reduction (red D) (id (_⊢_:⇒*:_^_.⊢B D)) Πₙ Πₙ (refl (_⊢_:⇒*:_^_.⊢B D)))
logRelIrr (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ⊢t = conv ⊢t (reduction (red D) (id (_⊢_:⇒*:_^_.⊢B D)) ∃ₙ ∃ₙ (refl (_⊢_:⇒*:_^_.⊢B D)))
logRelIrr {ι ¹} (emb X [A]) ⊢t = logRelIrr [A] ⊢t
logRelIrr {∞} (emb X [A]) ⊢t = logRelIrr [A] ⊢t

-- Well-typed irrelevant terms are reducibly equal as soon as they have the same type
logRelIrrEq : ∀ {l t u Γ l' A} ([A] : Γ ⊩⟨ l ⟩ A ^ [ % , l' ]) (⊢t : Γ ⊢ t ∷ A ^ [ % , l' ]) (⊢u : Γ ⊢ u ∷ A ^ [ % , l' ]) → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ % , l' ] / [A]
logRelIrrEq (Emptyᵣ [[ ⊢A , ⊢B , D ]]) ⊢t ⊢u = Emptyₜ₌ (ne ((conv ⊢t (reduction D (id ⊢B) Emptyₙ Emptyₙ (refl ⊢B))))
                                                         (conv ⊢u (reduction D (id ⊢B) Emptyₙ Emptyₙ (refl ⊢B))))
logRelIrrEq (ne x) ⊢t ⊢u = neₜ₌ ⊢t ⊢u
logRelIrrEq (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ⊢t ⊢u = (conv ⊢t (reduction (red D) (id (_⊢_:⇒*:_^_.⊢B D)) Πₙ Πₙ (refl (_⊢_:⇒*:_^_.⊢B D))) ) , (conv ⊢u (reduction (red D) (id (_⊢_:⇒*:_^_.⊢B D)) Πₙ Πₙ (refl (_⊢_:⇒*:_^_.⊢B D))) )
logRelIrrEq (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ⊢t ⊢u = (conv ⊢t (reduction (red D) (id (_⊢_:⇒*:_^_.⊢B D)) ∃ₙ ∃ₙ (refl (_⊢_:⇒*:_^_.⊢B D))) ) , (conv ⊢u (reduction (red D) (id (_⊢_:⇒*:_^_.⊢B D)) ∃ₙ ∃ₙ (refl (_⊢_:⇒*:_^_.⊢B D))) )
logRelIrrEq {ι ¹} (emb X [A]) ⊢t = logRelIrrEq [A] ⊢t
logRelIrrEq {∞} (emb X [A]) ⊢t = logRelIrrEq [A] ⊢t

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module DualCoinductive where

open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Data.Fin hiding (_+_)
open import Function
open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open import Agda.Builtin.Equality.Rewrite
open import Direction

-- variables

variable
  n m : ℕ

-- session types coinductively

module COI where
  mutual
    data Type : Set where
      TUnit TInt : Type
      TPair : Type → Type → Type
      TChan : SType → Type

    data STypeF (S : Set) : Set where
      transmit : (d : Dir) (t : Type) (s : S) → STypeF S
      choice : (d : Dir) (m : ℕ) (alt : Fin m → S) → STypeF S
      end : STypeF S

    record SType : Set where
      coinductive
      constructor delay
      field force : STypeF SType

  open SType

  variable
    t t₁ t₂ t₃ t₁' t₂' t₃' : Type
    s s₁ s₂ s₃ : SType
    s' s₁' s₂' s₃' : STypeF SType

  -- type equivalence
  data EquivT (R : SType → SType → Set) : Type → Type → Set where
    eq-unit : EquivT R TUnit TUnit
    eq-int  : EquivT R TInt TInt
    eq-pair : EquivT R t₁ t₁' → EquivT R t₂ t₂' → EquivT R (TPair t₁ t₂) (TPair t₁' t₂')
    eq-chan : R s₁ s₂ → EquivT R (TChan s₁) (TChan s₂)

  -- session type equivalence
  data EquivF (R : SType → SType → Set) : STypeF SType → STypeF SType → Set where
    eq-transmit : (d : Dir) → EquivT R t₁ t₂ → R s₁ s₂ → EquivF R (transmit d t₁ s₁) (transmit d t₂ s₂)
    eq-choice : ∀ {alt alt'} → (d : Dir) → ((i : Fin m) → R (alt i) (alt' i)) → EquivF R (choice d m alt) (choice d m alt')
    eq-end : EquivF R end end

  record Equiv (s₁ : SType) (s₂ : SType) : Set where
    coinductive
    field force : EquivF Equiv (force s₁) (force s₂)

  open Equiv

  _≈_ = Equiv
  _≈'_ = EquivF Equiv
  _≈ᵗ_ = EquivT Equiv

  -- reflexivity
  ≈ᵗ-refl : t ≈ᵗ t
  ≈-refl : s ≈ s
  ≈'-refl : s' ≈' s'

  force (≈-refl {s}) = ≈'-refl

  ≈'-refl {transmit d t s} = eq-transmit d ≈ᵗ-refl ≈-refl
  ≈'-refl {choice d m alt} = eq-choice d λ i → ≈-refl
  ≈'-refl {end} = eq-end

  ≈ᵗ-refl {TUnit} = eq-unit
  ≈ᵗ-refl {TInt} = eq-int
  ≈ᵗ-refl {TPair t t₁} = eq-pair ≈ᵗ-refl ≈ᵗ-refl
  ≈ᵗ-refl {TChan x} = eq-chan ≈-refl

  -- symmetry
  ≈-symm : s₁ ≈ s₂ → s₂ ≈ s₁
  ≈'-symm : s₁' ≈' s₂' → s₂' ≈' s₁'
  ≈ᵗ-symm : t₁ ≈ᵗ t₂ → t₂ ≈ᵗ t₁

  force (≈-symm s₁≈s₂) = ≈'-symm (force s₁≈s₂)

  ≈'-symm (eq-transmit d x x₁) = eq-transmit d (≈ᵗ-symm x) (≈-symm x₁)
  ≈'-symm (eq-choice d x) = eq-choice d (λ i → ≈-symm (x i))
  ≈'-symm eq-end = eq-end

  ≈ᵗ-symm eq-unit = eq-unit
  ≈ᵗ-symm eq-int = eq-int
  ≈ᵗ-symm (eq-pair t₁≈t₂ t₁≈t₃) = eq-pair (≈ᵗ-symm t₁≈t₂) (≈ᵗ-symm t₁≈t₃)
  ≈ᵗ-symm (eq-chan x) = eq-chan (≈-symm x)

  -- transitivity
  ≈-trans : s₁ ≈ s₂ → s₂ ≈ s₃ → s₁ ≈ s₃
  ≈'-trans : s₁' ≈' s₂' → s₂' ≈' s₃' → s₁' ≈' s₃'
  ≈ᵗ-trans : t₁ ≈ᵗ t₂ → t₂ ≈ᵗ t₃ → t₁ ≈ᵗ t₃

  force (≈-trans s₁≈s₂ s₂≈s₃) = ≈'-trans (force s₁≈s₂) (force s₂≈s₃)

  ≈'-trans (eq-transmit d tt₁ ss₁) (eq-transmit .d tt₂ ss₂) = eq-transmit d (≈ᵗ-trans tt₁ tt₂) (≈-trans ss₁ ss₂)
  ≈'-trans (eq-choice d x) (eq-choice .d x₁) = eq-choice d (λ i → ≈-trans (x i) (x₁ i))
  ≈'-trans eq-end eq-end = eq-end

  ≈ᵗ-trans eq-unit eq-unit = eq-unit
  ≈ᵗ-trans eq-int eq-int = eq-int
  ≈ᵗ-trans (eq-pair t₁≈ᵗt₂ t₁≈ᵗt₃) (eq-pair t₂≈ᵗt₃ t₂≈ᵗt₄) = eq-pair (≈ᵗ-trans t₁≈ᵗt₂ t₂≈ᵗt₃) (≈ᵗ-trans t₁≈ᵗt₃ t₂≈ᵗt₄)
  ≈ᵗ-trans (eq-chan ss₁) (eq-chan ss₂) = eq-chan (≈-trans ss₁ ss₂)

  ----------------------------------------------------------------------
  -- relational duality
  data DualD : Dir → Dir → Set where
    dual-sr : DualD SND RCV
    dual-rs : DualD RCV SND

  -- session type duality
  data DualF (R : SType → SType → Set) : STypeF SType → STypeF SType → Set where
    dual-transmit : DualD d₁ d₂ → t₁ ≈ᵗ t₂ → R s₁ s₂ → DualF R (transmit d₁ t₁ s₁) (transmit d₂ t₂ s₂)
    dual-choice : ∀ {alt alt'} → DualD d₁ d₂ → ((i : Fin m) → R (alt i) (alt' i)) → DualF R (choice d₁ m alt) (choice d₂ m alt')
    dual-end : DualF R end end

  record Dual (s₁ : SType) (s₂ : SType) : Set where
    coinductive
    field force : DualF Dual (force s₁) (force s₂)

  -- open Dual

  _⊥_ = Dual
  _⊥'_ = DualF Dual
  -- _≈ᵗ_ = EquivT Equiv

  -- symmetric

  DualD-symm : DualD d₁ d₂ → DualD d₂ d₁
  DualD-symm dual-sr = dual-rs
  DualD-symm dual-rs = dual-sr

  ⊥-symm : s₁ ⊥ s₂ → s₂ ⊥ s₁
  ⊥'-symm : s₁' ⊥' s₂' → s₂' ⊥' s₁'

  Dual.force (⊥-symm s₁⊥s₂) = ⊥'-symm (Dual.force s₁⊥s₂)

  ⊥'-symm (dual-transmit x x₁ x₂) = dual-transmit (DualD-symm x) (≈ᵗ-symm x₁) (⊥-symm x₂)
  ⊥'-symm (dual-choice x x₁) = dual-choice (DualD-symm x) (⊥-symm ∘ x₁)
  ⊥'-symm dual-end = dual-end

  -- involutory
  DualD-inv : DualD d₁ d₂ → DualD d₂ d₃ → d₁ ≡ d₃
  DualD-inv dual-sr dual-rs = refl
  DualD-inv dual-rs dual-sr = refl

  ⊥-inv : s₁ ⊥ s₂ → s₂ ⊥ s₃ → s₁ ≈ s₃
  ⊥'-inv : s₁' ⊥' s₂' → s₂' ⊥' s₃' → s₁' ≈' s₃'

  force (⊥-inv s₁⊥s₂ s₂⊥s₃) = ⊥'-inv (Dual.force s₁⊥s₂) (Dual.force s₂⊥s₃)

  ⊥'-inv (dual-transmit dd₁ tt₁ ss₁) (dual-transmit dd₂ tt₂ ss₂) rewrite DualD-inv dd₁ dd₂ = eq-transmit _ (≈ᵗ-trans tt₁ tt₂) (⊥-inv ss₁ ss₂)
  ⊥'-inv (dual-choice dd₁ ss₁) (dual-choice dd₂ ss₂) rewrite DualD-inv dd₁ dd₂ = eq-choice _ (λ i → ⊥-inv (ss₁ i) (ss₂ i))
  ⊥'-inv dual-end dual-end = eq-end

  ----------------------------------------------------------------------
  -- duality
  dual : SType → SType
  dualF : STypeF SType → STypeF SType

  force (dual s) = dualF (force s)

  dualF (transmit d t s) = transmit (dual-dir d) t (dual s)
  dualF (choice d m alt) = choice (dual-dir d) m (dual ∘ alt)
  dualF end = end

  -- properties

  dual-involution : ∀ s → s ≈ dual (dual s)
  dual-involutionF : ∀ s' → s' ≈' dualF (dualF s')

  force (dual-involution s) = dual-involutionF (force s)

  dual-involutionF (transmit d t s)
    rewrite dual-dir-inv d = eq-transmit d ≈ᵗ-refl (dual-involution s)
  dual-involutionF (choice d m alt)
    rewrite dual-dir-inv d = eq-choice d (dual-involution ∘ alt)
  dual-involutionF end = eq-end

  -----------------------------------------------------------------------
  -- relational duality vs functional duality

  -- soundness

  dual-soundD : DualD d (dual-dir d)
  dual-soundD {SND} = dual-sr
  dual-soundD {RCV} = dual-rs

  dual-soundS : s ⊥ dual s
  dual-soundF : s' ⊥' dualF s'

  Dual.force dual-soundS = dual-soundF

  dual-soundF {transmit d t s} = dual-transmit dual-soundD ≈ᵗ-refl dual-soundS
  dual-soundF {choice d m alt} = dual-choice dual-soundD (λ i → dual-soundS)
  dual-soundF {end} = dual-end

  -- completeness

  dual-completeD : DualD d₁ d₂ → d₁ ≡ dual-dir d₂
  dual-completeD dual-sr = refl
  dual-completeD dual-rs = refl

  dual-completeS : s₁ ⊥ s₂ → s₁ ≈ dual s₂
  dual-completeF : s₁' ⊥' s₂' → s₁' ≈' dualF s₂'

  force (dual-completeS s₁⊥s₂) = dual-completeF (Dual.force s₁⊥s₂)

  dual-completeF (dual-transmit dd tt ss) rewrite dual-completeD dd = eq-transmit _ tt (dual-completeS ss)
  dual-completeF (dual-choice dd x₁) rewrite dual-completeD dd = eq-choice _ (λ i → dual-completeS (x₁ i))
  dual-completeF dual-end = eq-end

ext: agda

max_stars_repo_name: kcaliban/dual-session

max_issues_repo_name: kcaliban/dual-session

max_forks_repo_name: kcaliban/dual-session


text:
------------------------------------------------------------------------
-- A simplified parser type
------------------------------------------------------------------------

module StructurallyRecursiveDescentParsing.Simplified where

open import Category.Monad
open import Codata.Musical.Notation
open import Data.Bool
open import Data.List using (List; _∷_; []; _++_)
import Data.List.Categorical as ListMonad
import Data.List.Properties as ListProp
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.List.NonEmpty
  using (List⁺; _∷_; [_]; _⁺++_; head; tail)
import Data.List.NonEmpty.Categorical as List⁺
open import Data.List.NonEmpty.Properties
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open RawMonad {f = zero} ListMonad.monad
  using () renaming (_>>=_ to _>>=′_)
open RawMonad {f = zero} List⁺.monad
  using () renaming (_>>=_ to _>>=⁺_)
private
  open module BagS {A : Set} = Setoid ([ bag ]-Equality A)
    using () renaming (_≈_ to _Bag-≈_)

open import TotalParserCombinators.Parser as P
  hiding (Parser; module Parser)

------------------------------------------------------------------------
-- Parsers

infixl 10 _!>>=_ _?>>=_
infixl  5 _∣_

-- A type for parsers which are not left recursive.
--
-- The boolean index is true iff the parser is nullable (accepts the
-- empty string).

data Parser (Tok : Set) : Bool → Set → Set1 where
  return : ∀ {R} (x : R) → Parser Tok true R
  fail   : ∀ {R} → Parser Tok false R
  token  : Parser Tok false Tok
  _∣_    : ∀ {e₁ e₂ R}
           (p₁ : Parser Tok  e₁       R)
           (p₂ : Parser Tok       e₂  R) →
                 Parser Tok (e₁ ∨ e₂) R
  _?>>=_ : ∀ {e₂ R₁ R₂}
           (p₁ :      Parser Tok true R₁)
           (p₂ : R₁ → Parser Tok e₂   R₂) →
                      Parser Tok e₂   R₂
  _!>>=_ : ∀ {R₁ R₂} {e₂ : R₁ → Bool}
           (p₁ :               Parser Tok false  R₁)
           (p₂ : (x : R₁) → ∞ (Parser Tok (e₂ x) R₂)) →
                               Parser Tok false  R₂

-- Note that Parser has only one coinductive recursive component.
-- Making any other recursive component coinductive would allow left
-- recursive grammars to be formed, but it is safe to use coinduction
-- in _>>=_ when we know that a token has been consumed, because for
-- every successive use of coinduction we are at least one step closer
-- to the end of the input.

------------------------------------------------------------------------
-- "Initial bags"

-- The initial bag of a parser is calculated in such a way that it is
-- obvious, given the nullability of the parser, whether or not the
-- bag is empty.

mutual

  initial⁺ : ∀ {Tok e R} → Parser Tok e R → e ≡ true → List⁺ R
  initial⁺ (return x)                  refl = [ x ]
  initial⁺ fail                        ()
  initial⁺ token                       ()
  initial⁺ (_∣_ {true}          p₁ p₂) refl = initial⁺ p₁ refl ⁺++ initial p₂
  initial⁺ (_∣_ {false} {true}  p₁ p₂) refl = initial⁺ p₂ refl
  initial⁺ (_∣_ {false} {false} p₁ p₂) ()
  initial⁺ (p₁ ?>>= p₂)                refl = initial⁺ p₁     refl >>=⁺ λ x →
                                              initial⁺ (p₂ x) refl
  initial⁺ (p₁ !>>= p₂)                ()

  initial : ∀ {e Tok R} → Parser Tok e R → List R
  initial {false} p = []
  initial {true}  p = head is ∷ tail is
    where is = initial⁺ p refl

-- Some boring lemmas.

private

  ∣-lemma : ∀ {e₁ e₂ Tok R}
            (p₁ : Parser Tok e₁ R) (p₂ : Parser Tok e₂ R) →
            initial p₁ ++ initial p₂ ≡ initial (p₁ ∣ p₂)
  ∣-lemma {false} {false} p₁ p₂ = refl
  ∣-lemma {false} {true}  p₁ p₂ = refl
  ∣-lemma {true}          p₁ p₂ = refl

  ?>>=-lemma : ∀ {e₂ Tok R₁ R₂}
               (p₁ : Parser Tok true R₁) (p₂ : R₁ → Parser Tok e₂ R₂) →
               initial (p₂ (head (initial⁺ p₁ refl))) ++
                 (tail (initial⁺ p₁ refl) >>=′ λ x → initial (p₂ x)) ≡
               initial (p₁ ?>>= p₂)
  ?>>=-lemma {false} p₁ p₂ = ListMonad.MonadProperties.right-zero
                               (tail (initial⁺ p₁ refl))
  ?>>=-lemma {true}  p₁ p₂ = toList->>= f xs
    where f  = λ x → initial⁺ (p₂ x) refl
          xs = initial⁺ p₁ refl

------------------------------------------------------------------------
-- Semantics

-- The semantics of simplified parsers is defined by translation.

⟦_⟧ : ∀ {Tok e R} (p : Parser Tok e R) → P.Parser Tok R (initial p)
⟦ return x   ⟧ = return x
⟦ fail       ⟧ = fail
⟦ token      ⟧ = token
⟦ p₁ ∣ p₂    ⟧ = cast lem (⟦ p₁ ⟧ ∣ ⟦ p₂ ⟧)
                 where
                 lem : _ Bag-≈ _
                 lem = BagS.reflexive (∣-lemma p₁ p₂)
⟦ p₁ !>>= p₂ ⟧ =           ⟦ p₁ ⟧ >>= λ x → ♯ ⟦ ♭ (p₂ x) ⟧
⟦ p₁ ?>>= p₂ ⟧ = cast lem (⟦ p₁ ⟧ >>= λ x →   ⟦    p₂ x  ⟧)
                 where
                 lem : _ Bag-≈ _
                 lem = BagS.reflexive (?>>=-lemma p₁ p₂)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definitions for Functions
------------------------------------------------------------------------

-- The contents of this file should usually be accessed from `Function`.

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

module Function.Core where

------------------------------------------------------------------------
-- Types

Fun₁ : ∀ {a} → Set a → Set a
Fun₁ A = A → A

Fun₂ : ∀ {a} → Set a → Set a
Fun₂ A = A → A → A


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Pointed.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed.Base
open import Cubical.Data.Prod

Π∙ : ∀ {ℓ ℓ'} (A : Type ℓ) (B∙ : A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Π∙ A B∙ = (∀ a → typ (B∙ a)) , (λ a → pt (B∙ a))

Σ∙ : ∀ {ℓ ℓ'} (A∙ : Pointed ℓ) (B∙ : typ A∙ → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Σ∙ A∙ B∙ = (Σ[ a ∈ typ A∙ ] typ (B∙ a)) , (pt A∙ , pt (B∙ (pt A∙)))

_×∙_ : ∀ {ℓ ℓ'} (A∙ : Pointed ℓ) (B∙ : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
A∙ ×∙ B∙ = ((typ A∙) × (typ B∙)) , (pt A∙ , pt B∙)

max_stars_repo_name: oisdk/cubical

max_issues_repo_name: oisdk/cubical

max_forks_repo_name: oisdk/cubical


text:
module FStream.Containers where

------------------------------------------------------------------------
-- Containers & their extension
------------------------------------------------------------------------

open import Data.Fin
open import Data.Maybe
open import Data.Unit

open import Library

ListC : Container ℓ₀
Shape    ListC   = ℕ
Position ListC n = Fin n

StateC : ∀ {ℓ} → Set ℓ → Container ℓ
Shape (StateC S) = S → S
Position (StateC S) _ = S

StreamC : Container ℓ₀
Shape StreamC = ⊤
Position StreamC = const ℕ

ReaderC : Set → Container ℓ₀
Shape (ReaderC R) = ⊤
Position (ReaderC R) _ = R

runReader : {R A : Set} → ⟦ ReaderC R ⟧ A → R → A
runReader (proj₁ , proj₂) r = proj₂ r

ask : ∀ {R} → ⟦ ReaderC R ⟧ R
proj₁ ask = tt
proj₂ ask x = x

returnReader : ∀ {ℓ} {A : Set ℓ} {R : Set} → A → ⟦ ReaderC R ⟧ A
returnReader a = tt , (λ _ → a)

ExceptC : Set → Container ℓ₀
Shape (ExceptC E) = Maybe E
Position (ExceptC E₁) (just x) = ⊥
Position (ExceptC E₁) nothing = ⊤

-- TODO Use stdlib
IdC : Container ℓ₀
Shape IdC = ⊤
Position IdC tt = ⊤

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
module MJ.Types where

open import Prelude hiding (_≟_)
open import Data.Fin.Properties as FinP using ()
open import Data.Vec
open import Data.List

open import Relation.Binary.Core
open import Relation.Nullary
open import Relation.Binary

data Cid (c : ℕ) : Set where
  cls : Fin c → Cid c
  Object : Cid c

_cid≟_ : ∀ {c} → Decidable (_≡_ {A = Cid c})
cls x cid≟ cls y with x FinP.≟ y
cls x cid≟ cls .x | yes refl = yes refl
cls x cid≟ cls y | no ¬p = no (λ{ refl → ¬p refl})
cls x cid≟ Object = no (λ ())
Object cid≟ cls x = no (λ ())
Object cid≟ Object = yes refl

data Ty (c : ℕ) : Set where
  void : Ty c
  int  : Ty c
  ref  : Cid c → Ty c

data Ty⁺ (c : ℕ) : Set where
  vty : Ty c → Ty⁺ c
  obj : Cid c → Ty⁺ c

World : ℕ → Set
World c = List (Ty⁺ c)

Sig : ℕ → Set
Sig c = List (Ty c) × Ty c

_≟_ : ∀ {c} → Decidable (_≡_ {A = Ty c})
void ≟ void = yes refl
void ≟ int = no (λ ())
void ≟ ref x = no (λ ())
int ≟ void = no (λ ())
int ≟ int = yes refl
int ≟ ref x = no (λ ())
ref x ≟ void = no (λ ())
ref x ≟ int = no (λ ())
ref x ≟ ref y with x cid≟ y
ref x ≟ ref y | yes p = yes (cong ref p)
ref x ≟ ref y | no ¬p = no λ{ refl → ¬p refl }


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

module Math.NumberTheory.Summation.Generic where

-- agda-stdlib
open import Algebra
open import Data.Nat

module MonoidSummation {c e} (M : Monoid c e) where
  open Monoid M renaming (Carrier to A)

  -- Σ< n f = Σₖ₌₀ⁿ⁻¹[f k]
  Σ< : ℕ → (ℕ → A) → A
  Σ< 0       f = ε
  Σ< (suc n) f = Σ< n f ∙ f n

  -- Σ≤ n f = Σₖ₌₀ⁿ[f k]
  Σ≤ : ℕ → (ℕ → A) → A
  Σ≤ n f = Σ< (suc n) f

  -- Σ<range m n f = Σₖ₌ₘⁿ⁻¹[f k]
  Σ<range : ℕ → ℕ → (ℕ → A) → A
  Σ<range m n f = Σ< (n ∸ m) (λ o → f (m + o))

  -- Σ≤range m n f = Σₖ₌ₘⁿ[f k]
  Σ≤range : ℕ → ℕ → (ℕ → A) → A
  Σ≤range m n f = Σ<range m (suc n) f

  -- syntax
  syntax Σ< n (λ k → e) = Σ[ k < n ] e
  syntax Σ≤ n (λ k → e) = Σ[ k ≤ n ] e
  syntax Σ<range m n (λ k → e) = Σ[ m ≤ k < n ] e
  syntax Σ≤range m n (λ k → e) = Σ[ m ≤ k ≤ n ] e


text:
module Type.Dependent where

import      Lvl
open import Type

private
  module Module where
    -- Dependent product type (pi-type).
    -- Also called: Dependent function type.
    -- The right-hand side's type is a function type that uses the left-hand side's type as its "domain".
    -- And then the type of the resulting function of the two types depends on the argument.
    record Π {ℓ₁ ℓ₂} (A : Type{ℓ₁}) (B : A → Type{ℓ₂}) : Type{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field
        apply : (a : A) → B(a)

    -- Dependent sum type (sigma-type).
    -- Also called: Dependent pair type.
    -- The right-hand side's type is a function type that uses the left-hand side's type as its "domain".
    -- And then the type of the resulting pair depends on the left-hand side.
    record Σ {ℓ₁ ℓ₂} (A : Type{ℓ₁}) (B : A → Type{ℓ₂}) : Type{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field
        left  : A
        right : B(left)

ℰ : ∀{ℓ₁ ℓ₂}{A : Type{ℓ₁}} → (A → Type{ℓ₂}) → Type{ℓ₁ Lvl.⊔ ℓ₂}
ℰ {A = A} B = Module.Σ A B
module ℰ where
  pattern intro {left} right = Module.intro left right

open Module public
{-# BUILTIN SIGMA Σ #-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Categories.Category.Core

module Categories.Object.Product.Limit {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Nat.Base using (ℕ)
open import Data.Fin.Base using (Fin)
open import Data.Fin.Patterns

open import Categories.Category.Lift
open import Categories.Category.Finite.Fin
open import Categories.Category.Finite.Fin.Construction.Discrete
open import Categories.Object.Product C
open import Categories.Diagram.Limit
open import Categories.Functor.Core

import Categories.Category.Construction.Cones as Co
import Categories.Morphism.Reasoning as MR

private
  module C = Category C
  open C
  open MR C
  open HomReasoning

module _ {o′ ℓ′ e′} {F : Functor (liftC o′ ℓ′ e′ (Discrete 2)) C} where
  private
    module F = Functor F
    open F

  limit⇒product : Limit F → Product (F₀ (lift 0F)) (F₀ (lift 1F))
  limit⇒product L = record
    { A×B      = apex
    ; π₁       = proj (lift 0F)
    ; π₂       = proj (lift 1F)
    ; ⟨_,_⟩    = λ f g → rep record
      { apex = record
        { ψ       = λ { (lift 0F) → f
                      ; (lift 1F) → g }
        ; commute = λ { {lift 0F} {lift 0F} (lift 0F) → elimˡ identity
                      ; {lift 1F} {lift 1F} (lift 0F) → elimˡ identity }
        }
      }
    ; project₁ = commute
    ; project₂ = commute
    ; unique   = λ {_} {h} eq eq′ → terminal.!-unique record
      { arr     = h
      ; commute = λ { {lift 0F} → eq
                    ; {lift 1F} → eq′ }
      }
    }
    where open Limit L

module _ o′ ℓ′ e′ A B where
  open Equiv

  product⇒limit-F : Functor (liftC o′ ℓ′ e′ (Discrete 2)) C
  product⇒limit-F = record
    { F₀           = λ { (lift 0F) → A
                       ; (lift 1F) → B }
    ; F₁           = λ { {lift 0F} {lift 0F} _ → C.id
                       ; {lift 1F} {lift 1F} _ → C.id }
    ; identity     = λ { {lift 0F} → refl
                       ; {lift 1F} → refl }
    ; homomorphism = λ { {lift 0F} {lift 0F} {lift 0F} → sym identity²
                       ; {lift 1F} {lift 1F} {lift 1F} → sym identity² }
    ; F-resp-≈     = λ { {lift 0F} {lift 0F} _ → refl
                       ; {lift 1F} {lift 1F} _ → refl }
    }

module _ o′ ℓ′ e′ {A B} (p : Product A B) where
  open Product p
  private
    F = product⇒limit-F o′ ℓ′ e′ A B
    open Functor F

  product⇒limit : Limit F
  product⇒limit = record
    { terminal = record
      { ⊤        = record
        { N    = A×B
        ; apex = record
          { ψ       = λ { (lift 0F) → π₁
                        ; (lift 1F) → π₂ }
          ; commute = λ { {lift 0F} {lift 0F} (lift 0F) → identityˡ
                        ; {lift 1F} {lift 1F} (lift 0F) → identityˡ }
          }
        }
      ; !        = λ {K} →
        let open Co.Cone F K
        in record
        { arr     = ⟨ ψ (lift 0F) , ψ (lift 1F) ⟩
        ; commute = λ { {lift 0F} → project₁
                      ; {lift 1F} → project₂ }
        }
      ; !-unique = λ {K} f →
        let module K = Co.Cone F K
            module f = Co.Cone⇒ F f
        in begin
          ⟨ K.ψ (lift 0F) , K.ψ (lift 1F) ⟩ ≈˘⟨ ⟨⟩-cong₂ f.commute f.commute ⟩
          ⟨ π₁ ∘ f.arr , π₂ ∘ f.arr ⟩       ≈⟨ g-η ⟩
          f.arr                             ∎
      }
    }

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
module Scratch.FinDecEq1 where

open import Data.Bool.Base hiding (_≤_)
open import Data.Product
open import Data.Sum
open import Level renaming (suc to lsuc; _⊔_ to _⊔ℓ_; zero to lzero)

open import Relation.Nullary
open import Relation.Nullary.Decidable

open import Relation.Unary using (Decidable)
open import Relation.Binary hiding (Decidable)

open import Function.Base
-- open import Function.Bijection hiding (_∘_)
-- open import Function.Equality hiding (≡-setoid; _∘_)

open import Data.Nat.Base hiding (_≤_)
open import Data.Fin renaming (zero to fzero; suc to fsuc)
open import Data.Fin.Properties hiding (to-from)
-- see http://firsov.ee/finset/finset.pdf

open import Data.List.Base renaming (tabulate to tab;
                                     lookup to nth;
                                     filter to lfilter;
                                     allFin to allF)
open import Data.List.Properties
open import Data.List.Relation.Unary.Any
-- open import Data.List.Membership.Propositional renaming (_∈_ to _∈ℓ_)
-- open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.Any as Any -- hiding (tail)
open import Data.List.Relation.Unary.Any.Properties hiding (tabulate⁺)
open import Data.List.Relation.Unary.All as All hiding (tabulate)
open import Data.List.Relation.Unary.AllPairs as AllPairs
open import Data.List.Relation.Unary.AllPairs.Properties renaming (map⁺ to ap-map⁺)

-- :-( can't use Vector because it doesn't have a filter
-- open import Data.Vec.Functional as Coll
-- open import Data.Vec.Functional.Relation.Unary.Any
--   renaming (here to here'; there to there')

open import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning

open import Scratch.Data.List.Relation.Helpers
open import Scratch.Subset

-- record StronglyFiniteSetoid (n : ℕ) : Set (lsuc (c ⊔ℓ ℓ)) where
--   field
--     S : Setoid c ℓ
--     χ : Bijection (≡-setoid n) S
--
--   open Setoid S
--   open Bijection χ
--   open Π to renaming (_⟨$⟩_ to to')
--   open Π from renaming (_⟨$⟩_ to from')
--
--   ι : Fin n → Carrier
--   ι x = to' x
--
--   ρ : Carrier → Fin n
--   ρ y = from' y

  -- TODO: pullback of ω where ω ≤ _≈_ (see orbital relation)
  -- /Users/amantini/dev/agda/agda-stdlib/README/Data/Interleaving.agda
  -- if ω is decidable then the pullback is a FinDecEq

open import Data.Vec hiding (length)
                     renaming (lookup to vlookup)
open import Data.Vec.Properties
-- open import Data.Vec.Relation.Unary.Any
open import Data.Fin.Subset
open import Data.Fin.Subset.Properties

lmap = Data.List.Base.map
syntax lmap (λ x → B) L = ⟦ B ∣ x ∈ℓ L ⟧

fsuc∈ : ∀ {n} → { p : Subset n} → {x : Fin n} → {s : Side} → (x ∈ p) → (fsuc x) ∈ (s Data.Vec.∷ p)
fsuc∈ here = there here
fsuc∈ (there x∈p) = there (fsuc∈ x∈p)

fst₊ : ∀ {n} → (s : Subset n) → Nonempty s → Σ (Fin n) (λ x → ( x ∈ s × (∀ {y} → (y ∈ s) → x ≤ y )))
fst₊ {suc n} (inside ∷ rest) ne = ( fzero , here , λ _ → z≤n )
fst₊ {suc n} (outside ∷ rest) ne with (∃-toSum ne)
... | inj₂ b = let w = drop-there (proj₂ b)
                   z = (proj₁ b , w)
                   ( a , bb , c ) = (fst₊ rest z)
               in (fsuc a , fsuc∈ bb , λ { (there y∈s) → s≤s (c y∈s) } )

fst₋ : ∀ {n} → (s : Subset n) → Nonempty s → Fin n
fst₋ s ne = proj₁ (fst₊ s ne)

fst₋unique : ∀ {n} → ∀ (s t : Subset n) → (ns : Nonempty s) → (nt : Nonempty t) →
             s ≡ t → (fst₋ s ns) ≡ (fst₋ t nt)

fst₋unique s t ns nt s≡t = let fs , fs∈s , fs≤ = (fst₊ s ns)
                               ft , ft∈t , ft≤ = (fst₊ t nt)
                               ft∈s : ft ∈ s
                               ft∈s = subst _ (sym s≡t) ft∈t
                               fs∈t : fs ∈ t
                               fs∈t = subst _ s≡t fs∈s
                           in ≤-antisym (fs≤ ft∈s) (ft≤ fs∈t)

open import Data.Unit hiding (_≟_; ⊤)
-- TODO: see src/Data/List/Membership/Setoid.agda
--       see src/Relation/Nullary/Decidable.agda

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl  =  tt

record FinDecEq {a} (n : ℕ) : Set (lsuc a) where
  field
    _ω_ : Rel (Fin n) a
    isDecEq : IsDecEquivalence _ω_

  std : DecSetoid _ _
  std = record { Carrier = (Fin n) ;
                _≈_ = _ω_ ;
                isDecEquivalence = isDecEq }

  open DecSetoid std
    renaming (_≟_ to _ω?_ ;
              refl to r ;
              sym to s ;
              trans to t ;
              Carrier to F;
              setoid to std')
    public

  import Data.List.Membership.Propositional
  module MP = Data.List.Membership.Propositional {A = F}
  open MP renaming (_∈_ to _∈ℓ_)
  -- open import Data.List.Membership.Propositional renaming (_∈_ to _∈ℓ_)
  open import Data.List.Membership.Propositional.Properties

  [_]ω : (Fin n) → Subset n
  [ o ]ω = tabulate (does ∘ (_ω? o))
  -- TODO: use src/Data/List/Membership/Setoid.agda
  --       and src/Data/Fin/Subset/Properties.agda

  ω⇒∈ : ∀ {x y} → x ω y → x ∈ [ y ]ω
  ω⇒∈ {x} {y} xωy = let lkp = begin vlookup [ y ]ω x ≡⟨ lookup∘tabulate _ x ⟩
                               does (x ω? y) ≡⟨ dec-true (x ω? y) xωy ⟩
                               true ∎
               in lookup⇒[]= x [ y ]ω lkp

  -- in particular classes are not empty
  o∈[o]ω : ∀ { o : Fin n } → o ∈ [ o ]ω
  o∈[o]ω = ω⇒∈ r

  -- and actually equal

  -- conversely
  ∈⇒ω : ∀ {x y} → x ∈ [ y ]ω → x ω y
  ∈⇒ω {x} {y} x∈[y] = let w = begin true ≡˘⟨ []=⇒lookup x∈[y] ⟩
                              vlookup [ y ]ω x ≡⟨ lookup∘tabulate _ x ⟩
                              does (x ω? y) ≡˘⟨ isYes≗does _ ⟩
                              isYes (x ω? y) ∎
                          r : True (x ω? y)
                          r = ≡→T (sym w)
                        in toWitness r

  ω⇒⊆ : ∀ {x y} → x ω y → [ x ]ω ⊆ [ y ]ω
  ω⇒⊆ {x} {y} xωy {s} s∈[x] = ω⇒∈ (t (∈⇒ω s∈[x]) xωy )

  ω⇒≡ : ∀ {x y} → x ω y → [ x ]ω ≡ [ y ]ω
  ω⇒≡ {x} {y} xωy = ⊆-antisym (ω⇒⊆ xωy) (ω⇒⊆ (s xωy))

  -- canonical choice - TODO
  c : F → F
  c f = fst₋ {n} [ f ]ω ( f , o∈[o]ω )

  --
  cx∈[x] : ∀ (x : Fin n) → (c x) ∈ [ x ]ω
  cx∈[x] x = proj₁ (proj₂ (fst₊ [ x ]ω ( x , o∈[o]ω )))

  xωcx : ∀ (x : F) → x ω (c x)
  xωcx x = s (∈⇒ω (cx∈[x] x))
  --
  c⇒ω : ∀ {x y} → c x ≡ c y → x ω y
  c⇒ω {x} {y} cx≡cy = let P = λ q → q ∈ [ y ]ω
                          w : (c x) ∈ [ y ]ω
                          w = subst P (sym cx≡cy) (cx∈[x] y)
                      in t (xωcx x) (∈⇒ω w)
  --
  ω⇒c : ∀ {x y} → x ω y → c x ≡ c y
  ω⇒c {x} {y} xωy = fst₋unique _ _ _ _ (ω⇒≡ xωy)

  c-idempt : (x : F) → c (c x) ≡ c x
  c-idempt x = ω⇒c {c x} {x} (s (xωcx x))

  ω-disj : ∀ {x y} → ¬ (x ω y) → Empty ([ x ]ω ∩ [ y ]ω)
  ω-disj {x} {y} ¬xωy f∈∩ = let f , [x]∩[y] = f∈∩
                                l , r = x∈p∩q⁻ _ _ [x]∩[y]
                                fωx : f ω x
                                fωx = ∈⇒ω l
                                fωy = ∈⇒ω r
                            in ¬xωy (t (s fωx) fωy)

  ω-Disj : ∀ {x y} → ¬ (x ω y) → Disj [ x ]ω [ y ]ω
  ω-Disj ¬xωy = Empty-unique (ω-disj ¬xωy)

  -- canonical representative
  cr : (i : F) → Set
  cr i = i ≡ (c i)

  -- c' : (i : F) → cr i × i ω (c i)
  -- _≟_
  cr? : Decidable cr
  cr? = λ i → i ≟ (c i)

  cr-disj : ∀ {x y} → (cr x) → (cr y) → x ≢ y → ¬ (x ω y)
  cr-disj {x} {y} crx cry x≢y xωy = let x≡y = begin x ≡⟨ crx ⟩
                                                c x ≡⟨ ω⇒c xωy ⟩
                                                c y ≡˘⟨ cry ⟩
                                                y ∎
                                    in x≢y x≡y

  Tr : List F
  Tr = (lfilter cr? (allF n))

  -- ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v

  -- C : List (Subset n)
  -- C = ⟦ [ x ]ω ∣ x ∈ℓ Tr ⟧

  --  ap x≢y allF
  --  ap ¬ x ω y Tr
  --  ap Disj (map [_] Tr)

  ap1 : AllPairs _≢_ (allF n)
  ap1 = tabulate⁺ id
  ap2 : AllPairs (λ x y → ¬ x ω y) Tr
  ap2 = filter⁺⁺ cr? cr-disj ap1

  ap3 : AllPairs Disj ⟦ [ x ]ω ∣ x ∈ℓ Tr ⟧
  ap3 = ap-map⁺ (AllPairs.map ω-Disj ap2)

  C-cover' : ∀ (x : F) → (∃ λ k → cr k × x ω k)
  C-cover' x = (c x) , sym (c-idempt x) , xωcx x

  C-cover : ∀ (x : F) → Any (x ∈_) ⟦ [ x ]ω ∣ x ∈ℓ Tr ⟧
  C-cover x = let (k , crk , xωk) = C-cover' x
                  k∈ℓallF : k ∈ℓ allF n
                  k∈ℓallF = ∈-allFin {n} k
                  k∈ℓTr : k ∈ℓ Tr
                  k∈ℓTr = ∈-filter⁺ cr? k∈ℓallF crk
                  a : Any (x ω_) Tr
                  a = lose k∈ℓTr xωk
                  b : Any ((x ∈_) ∘ [_]ω) Tr
                  b = Any.map ω⇒∈ a
              -- map⁺ : Any (P ∘ f) xs → Any P (List.map f xs)
              in map⁺ b

  --
  []ω-cover : ⊤ ≡ ⋃ ⟦ [ x ]ω ∣ x ∈ℓ Tr ⟧
  []ω-cover = cover-⊤ ⟦ [ x ]ω ∣ x ∈ℓ Tr ⟧ C-cover

  -- Cardinality : n ≡ Data.List.Base.sum ⟦ ∣ [ x ]ω ∣ ∣ x ∈ℓ Tr ⟧
  -- Cardinality =
  --   let c = ∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ ⟦ [ x ]ω ∣ x ∈ℓ Tr ⟧ ap3
  --       in begin
  --           n ≡˘⟨ ∣⊤∣≡n n ⟩
  --           ∣ ⊤ {n} ∣ ≡⟨ cong ∣_∣ []ω-cover ⟩
  --           ∣ ⋃ ⟦ [ x ]ω ∣ x ∈ℓ Tr ⟧ ∣ ≡⟨ c ⟩
  --           -- cong List.sum (map-compose λ t → ∣ [ t ]ω ∣ ) refl
  --           Data.List.Base.sum (lmap ∣_∣ ⟦ [ x ]ω ∣ x ∈ℓ Tr ⟧) ≡˘⟨ ? ⟩
  --           Data.List.Base.sum ⟦ ∣ [ x ]ω ∣ ∣ x ∈ℓ Tr ⟧ ∎

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


text:
module Web.Semantic.DL.Signature where

infixr 4 _,_

-- a Signature is constructed from Concept Names and Role/Relation Names
data Signature : Set₁ where
  _,_ : (CN RN : Set) → Signature

-- concept name (maps to Sets)
CN : Signature → Set
CN (CN , RN) = CN

-- Role Names (or relation names)
RN : Signature → Set
RN (CN , RN) = RN

max_stars_repo_name: bblfish/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Every respectful binary relation induces a preorder. No claim is
-- made that this preorder is unique.
------------------------------------------------------------------------

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

open import Relation.Binary
open Setoid using (Carrier)

module Relation.Binary.Construct.FromRel
  {s₁ s₂} (S : Setoid s₁ s₂)                    -- The underlying equality
  {a r} {A : Set a} (_R_ : REL A (Carrier S) r) -- The relation
  where

open import Data.Product
open import Function
open import Level using (_⊔_)

open module Eq = Setoid S using (_≈_) renaming (Carrier to B)

------------------------------------------------------------------------
-- Definition

Resp : Rel B (a ⊔ r)
Resp x y = ∀ {a} → a R x → a R y

------------------------------------------------------------------------
-- Properties

reflexive : (∀ {a} → (a R_) Respects _≈_) → _≈_ ⇒ Resp
reflexive resp x≈y = resp x≈y

trans : Transitive Resp
trans x∼y y∼z = y∼z ∘ x∼y

isPreorder : (∀ {a} → (a R_) Respects _≈_) → IsPreorder _≈_ Resp
isPreorder resp = record
  { isEquivalence = Eq.isEquivalence
  ; reflexive     = reflexive resp
  ; trans         = trans
  }

preorder : (∀ {a} → (a R_) Respects _≈_) → Preorder _ _ _
preorder resp = record
  { isPreorder = isPreorder resp
  }


text:
module regular-star where

open import Level renaming ( suc to Suc ; zero to Zero )
open import Data.List
open import Data.Nat hiding ( _≟_ )
open import Data.Fin hiding ( _+_ )
open import Data.Empty
open import Data.Unit
open import Data.Product
-- open import Data.Maybe
open import  Relation.Nullary
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import logic
open import nat
open import automaton
open import regular-language

open import nfa
open import sbconst2
open import finiteSet
open import finiteSetUtil
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import regular-concat

open Automaton
open FiniteSet

open RegularLanguage

Star-NFA :  {Σ : Set} → (A : RegularLanguage Σ ) → NAutomaton (states A ) Σ
Star-NFA {Σ} A  = record { Nδ = δnfa ; Nend = nend }
   module Star-NFA where
       δnfa : states A → Σ → states A → Bool
       δnfa q i q₁ with aend (automaton A) q
       ... | true = equal? (afin A) ( astart A) q₁
       ... | false = equal? (afin A) (δ (automaton A) q i) q₁
       nend : states A → Bool
       nend q = aend (automaton A) q

Star-NFA-start :  {Σ : Set} → (A : RegularLanguage Σ ) → states A  → Bool
Star-NFA-start A q = equal? (afin A) (astart A) q \/  aend (automaton A) q

SNFA-exist : {Σ : Set} → (A : RegularLanguage Σ ) → (states A → Bool) → Bool
SNFA-exist A qs = exists (afin A) qs

M-Star : {Σ : Set} → (A : RegularLanguage Σ ) → RegularLanguage Σ
M-Star {Σ} A  = record {
       states = states A  → Bool
     ; astart = Star-NFA-start A
     ; afin = fin→  (afin A)
     ; automaton = subset-construction (SNFA-exist A ) (Star-NFA A )
   }

open Split

open _∧_

open NAutomaton
open import Data.List.Properties

closed-in-star :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Star (contain A) ) x ( M-Star A  )
closed-in-star {Σ} A B x = ≡-Bool-func closed-in-star→ closed-in-star← where
    NFA = (Star-NFA A )

    closed-in-star→ : Star (contain A)  x ≡ true → contain (M-Star A ) x ≡ true
    closed-in-star→ star = {!!}

    open Found

    closed-in-star← : contain (M-Star A ) x ≡ true → Star (contain A)  x ≡ true
    closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA {!!} x C
    ... | CC = {!!}

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
-- Andreas, Ulf, 2022-05-06, AIM XXXV
-- Make sure you cannot trick Agda into admitting data types in IUniv.
-- The previous check let this exploit through.
-- Note: I : IUniv : SSet₁

open import Agda.Primitive.Cubical

mutual
  Univ = _
  data False : Univ where

  I' : Univ
  I' = I

-- Should fail.

-- Error:
-- The universe _6 of False
-- is unresolved, thus does not permit data or record declarations
-- when checking the definition of False


text:
module Run where

open import Data.Bool
open import Data.Maybe
open import Data.Nat
open import Data.List
open import Data.List.All

open import Typing
open import Syntax
open import Global
open import Channel
open import Values
open import Session
open import Schedule

open import Examples
open import Aexamples

gas : ℕ → Gas
gas zero = Empty
gas (suc n) = More (gas n)

-- the magic number shows the last state before termination

-- runs to completion: the magic number is 7
runex1 : Outcome
runex1 = start (gas 8) ex1

-- runs to completion, but gets slow at 9
runex2 : Outcome
runex2 = start (gas 14) ex2

-- need more steps, but gets *very* slow
runex3 : Outcome
runex3 = start (gas 6) ex3

-- runs to completion
runex4 : Outcome
runex4 = start (gas 11) ex4

-- just lambda calculus
-- runs to completion: the magic number is 2
runex5 : Outcome
runex5 = start (gas 3) ex5

-- just lambda calculus
-- magic number is 6
runex6 : Outcome
runex6 = start (gas 7) ex6

-- now asynchronous examples
runaex1 : Outcome
runaex1 = start (gas 40) aex1

runasyncex1 : Outcome
runasyncex1 = start (gas 40) asyncex1

runasyncex2 : Outcome
runasyncex2 = start (gas 80) asyncex2

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
import      Lvl
open import Type

module Type.Cardinality.Proofs {ℓₗ : Lvl.Level} where

open import Functional
import      Logic.Predicate
import      Logic.Predicate.Theorems
import      Relator.Equals
import      Relator.Equals.Proofs
import      Type.Cardinality
import      Type.Functions
import      Type.Functions.Proofs
import      Type.Functions.Inverse
import      Type.Functions.Inverse.Proofs

module _ {ℓₒ₁}{ℓₒ₂} {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} where
  open Logic.Predicate               {ℓₗ}
  open Logic.Predicate.Theorems      {ℓₗ}
  open Type.Cardinality              {ℓₗ}
  open Type.Functions                {ℓₗ}
  open Type.Functions.Inverse        {ℓₗ}
  open Type.Functions.Inverse.Proofs {ℓₗ}
  open Type.Functions.Proofs         {ℓₗ}

  instance
    [≍]-to-[≼] : ⦃ _ : X ≍ Y ⦄ → (X ≼ Y)
    [≍]-to-[≼] ⦃ proof ⦄ = [∃]-map (proof ↦ bijective-to-injective ⦃ proof ⦄) proof

  instance
    [≍]-to-[≽] : ⦃ _ : X ≍ Y ⦄ → (X ≼ Y)
    [≍]-to-[≽] ⦃ proof ⦄ = [∃]-map (proof ↦ bijective-to-injective ⦃ proof ⦄) proof

  [≍]-symmetry : (X ≍ Y) → (Y ≍ X)
  [≍]-symmetry ([∃]-intro f ⦃ proof ⦄) = [∃]-intro (inv f ⦃ proof ⦄) ⦃ inv-bijective {ℓₒ₁}{ℓₒ₂} {_}{_} {f} ⦃ proof ⦄ ⦄

  -- TODO: Is it possible to prove these?
  -- [≍]-antisymmetry : (X ≼ Y) → (X ≽ Y) → (X ≍ Y)
  -- [≍]-antisymmetry = [∃]-map ()

  -- [≼][≽]-swap : (X ≼ Y) → (Y ≽ X)
  -- [≽][≼]-swap : (X ≽ Y) → (Y ≼ X)

module _ {ℓₒ} {X : Type{ℓₒ}} where
  open Logic.Predicate          {ℓₗ Lvl.⊔ ℓₒ}
  open Logic.Predicate.Theorems {ℓₗ Lvl.⊔ ℓₒ}
  open Type.Cardinality         {ℓₗ Lvl.⊔ ℓₒ}
  open Type.Functions.Proofs     {ℓₗ Lvl.⊔ ℓₒ}

  instance
    [≍]-reflexivity : (X ≍ X)
    [≍]-reflexivity = [∃]-intro (id) ⦃ id-is-bijective ⦄

  instance
    [≼]-reflexivity : (X ≼ X)
    [≼]-reflexivity = [∃]-intro(id) ⦃ bijective-to-injective ⦃ id-is-bijective ⦄ ⦄

  instance
    [≽]-reflexivity : (X ≽ X)
    [≽]-reflexivity = [∃]-intro(id) ⦃ bijective-to-surjective ⦃ id-is-bijective ⦄ ⦄

module _ {ℓₒ} {X : Type{ℓₒ}} {Y : Type{ℓₒ}} where
  open Type.Cardinality {ℓₗ Lvl.⊔ ℓₒ}
  open Relator.Equals   {ℓₗ Lvl.⊔ ℓₒ}{Lvl.𝐒(ℓₒ)}

  [≡]-to-[≍] : (X ≡ Y) → (X ≍ Y)
  [≡]-to-[≍] [≡]-intro = [≍]-reflexivity


text:
-- Andreas, 2016-06-03, bug found by Ulf
-- {-# OPTIONS -v tc.cover:20 #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field fst : A
        snd : B fst
open Σ

record ⊤ : Set where
data ⊥ : Set where

T : Bool → Set
T true = ⊤
T false = ⊥

p : Σ Bool T
fst p = false
p = true , _

loop : ⊥
loop = snd p

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Data.List.Relation.Permutation where

import      Data
open import Data.Boolean
open import Data.List
open import Data.List.Functions renaming (module LongOper to List)
open import Data.List.Relation
open import Functional using (id ; _∘_ ; const)
open import Logic.Propositional
open import Logic
import      Lvl
open import Numeral.Finite
open import Syntax.Function
open import Type

private variable ℓ : Lvl.Level
private variable T A B : Type{ℓ}
private variable l l₁ l₂ l₃ l₄ : List(T)
private variable x y z : T
private variable f : A → B
private variable P : T → Bool

-- The relation for two lists that are permutations of each other.
-- This means that they contain the same elements and the same number of them but possibly in a different order.
-- Or in other words, the first list is a reordered list of the second.
data _permutes_ {ℓ} : List{ℓ}(T) → List{ℓ}(T) → Stmt{Lvl.𝐒(ℓ)} where
  empty   : ∅ permutes (∅ {T = T})
  prepend : (l₁ permutes l₂) → ((x ⊰ l₁) permutes (x ⊰ l₂))
  swap    : (x ⊰ y ⊰ l) permutes (y ⊰ x ⊰ l)
  trans   : (l₁ permutes l₂) → (l₂ permutes l₃) → (l₁ permutes l₃)

trans-swap : (l₁ permutes l₂) → ((x ⊰ y ⊰ l₁) permutes (y ⊰ x ⊰ l₂))
trans-swap p = trans swap (prepend (prepend p))

-- TODO
-- _partition-of_ : List(List(T)) → List(T) → Stmt
-- p partition-of l = (foldᵣ (x ↦ ¬ Empty(x) ∧_) Data.Unit p) ∧ (concat(p) permutes l)

-- The permutation as a function between the permutated elements' indices.
-- Example:
--   p : [a,b,c,d,e,f] permutes [a,f,e,d,b,c]
--   map(permutation-mapping(p)) [0,1,2,3,4,5] = [0,4,5,3,2,1]
permutation-mapping : (l₁ permutes l₂) → (𝕟(length(l₁)) → 𝕟(length(l₂)))
permutation-mapping empty                = id
permutation-mapping (prepend p) 𝟎        = 𝟎
permutation-mapping (prepend p) (𝐒 n)    = 𝐒(permutation-mapping p n)
permutation-mapping swap        𝟎        = 𝐒(𝟎)
permutation-mapping swap        (𝐒 𝟎)    = 𝟎
permutation-mapping swap        (𝐒(𝐒 n)) = 𝐒 (𝐒 n)
permutation-mapping (trans p q)          = permutation-mapping q ∘ permutation-mapping p

-- TODO: It should be possible to make (_permutes_) the morphism of a category with some correct notion of equivalence (maybe trans swap swap ≡ refl for example?). Then permutation-mapping would be an instance of Functor(length) for the ((_→_) on₂ 𝕟) category?

module Proofs where
  open import Data.List.Proofs
  open import Data.List.Equiv.Id
  open import Lang.Inspect
  open import Logic.Predicate
  open import Numeral.Natural
  open import Numeral.Finite.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import Structure.Function.Domain
  open import Structure.Function.Domain.Proofs
  import      Structure.Function.Names as Names
  open import Structure.Function.Proofs
  open import Structure.Function
  import      Structure.Operator.Names as Names
  open import Structure.Operator.Properties
  open import Structure.Operator
  import      Structure.Relator.Names as Names
  open import Structure.Relator.Equivalence
  open import Structure.Relator.Properties
  open import Structure.Setoid using (Equiv)
  open import Syntax.Function
  open import Syntax.Transitivity

  instance
    permutes-reflexivity : Reflexivity(_permutes_ {T = T})
    permutes-reflexivity = intro proof where
      proof : Names.Reflexivity(_permutes_)
      proof {∅}     = empty
      proof {_ ⊰ _} = prepend proof

  instance
    permutes-symmetry : Symmetry(_permutes_ {T = T})
    permutes-symmetry = intro proof where
      proof : Names.Symmetry(_permutes_)
      proof empty       = empty
      proof (prepend p) = prepend (proof p)
      proof swap        = swap
      proof (trans p q) = trans (proof q) (proof p)

  instance
    permutes-transitivity : Transitivity(_permutes_ {T = T})
    permutes-transitivity = intro trans

  instance
    permutes-equivalence : Equivalence(_permutes_ {T = T})
    permutes-equivalence = intro

  permutes-equiv : Equiv(List(T))
  Equiv._≡_         permutes-equiv = _permutes_
  Equiv.equivalence permutes-equiv = permutes-equivalence

  -- If permutation relation had empty, prepend and trans-swap
  module _ where
    swap-from-trans-swap : (x ⊰ y ⊰ l) permutes (y ⊰ x ⊰ l)
    swap-from-trans-swap = trans-swap(reflexivity(_permutes_))

  PermutationMappingCorrectness : (l₁ l₂ : List(T)) → (𝕟(length(l₁)) → 𝕟(length(l₂))) → Stmt
  PermutationMappingCorrectness l₁ l₂ mapping = ∀{i} → (index l₁(i) ≡ index l₂(mapping i))

  permutation-mapping-correctness : (p : (l₁ permutes l₂)) → PermutationMappingCorrectness l₁ l₂ (permutation-mapping p)
  permutation-mapping-correctness empty                 = reflexivity(_≡_)
  permutation-mapping-correctness (prepend p) {𝟎}       = reflexivity(_≡_)
  permutation-mapping-correctness (prepend p) {𝐒 i}     = permutation-mapping-correctness p {i}
  permutation-mapping-correctness swap        {𝟎}       = reflexivity(_≡_)
  permutation-mapping-correctness swap        {𝐒 𝟎}     = reflexivity(_≡_)
  permutation-mapping-correctness swap        {𝐒 (𝐒 i)} = reflexivity(_≡_)
  permutation-mapping-correctness (trans p q)           = permutation-mapping-correctness p 🝖 permutation-mapping-correctness q

  instance
    permutation-mapping-injective : ∀{p : (l₁ permutes l₂)} → Injective(permutation-mapping p)
    permutation-mapping-injective {p = p} = intro(proof p) where
      proof : (p : (l₁ permutes l₂)) → Names.Injective(permutation-mapping p)
      proof (prepend p) {𝟎}   {𝟎}   eq = [≡]-intro
      proof (prepend p) {𝐒 x} {𝐒 y} eq = congruence₁(𝐒) (proof p (injective(𝐒) ⦃ [𝐒]-injective ⦄ eq))
      proof swap {𝟎}       {𝟎}       eq = [≡]-intro
      proof swap {𝟎}       {𝐒 (𝐒 y)} ()
      proof swap {𝐒 (𝐒 x)} {𝟎}       ()
      proof swap {𝐒 𝟎}     {𝐒 𝟎}     eq = [≡]-intro
      proof swap {𝐒 (𝐒 x)} {𝐒 (𝐒 y)} eq = eq
      proof (trans p q) = proof p ∘ proof q

  instance
    permutation-mapping-surjective : ∀{p : (l₁ permutes l₂)} → Surjective(permutation-mapping p)
    permutation-mapping-surjective {p = p} = intro(proof p) where
      proof : (p : (l₁ permutes l₂)) → Names.Surjective(permutation-mapping p)
      ∃.witness (proof p {y}) = permutation-mapping(symmetry(_permutes_) p) y
      ∃.proof (proof (prepend p) {𝟎})   = [≡]-intro
      ∃.proof (proof (prepend p) {𝐒 y}) = congruence₁(𝐒) (∃.proof (proof p {y}))
      ∃.proof (proof swap {𝟎})       = [≡]-intro
      ∃.proof (proof swap {𝐒 𝟎})     = [≡]-intro
      ∃.proof (proof swap {𝐒 (𝐒 y)}) = [≡]-intro
      ∃.proof (proof (trans p q) {y}) =
        permutation-mapping (trans p q) (∃.witness (proof (trans p q))) 🝖[ _≡_ ]-[]
        (permutation-mapping (trans p q) ∘ permutation-mapping(symmetry(_permutes_) p) ∘ permutation-mapping (symmetry(_permutes_) q)) y 🝖[ _≡_ ]-[]
        (permutation-mapping q ∘ permutation-mapping p ∘ permutation-mapping(symmetry(_permutes_) p) ∘ permutation-mapping (symmetry(_permutes_) q)) y 🝖[ _≡_ ]-[ congruence₁(permutation-mapping q) (∃.proof (proof p {_})) ]
        (permutation-mapping q ∘ permutation-mapping (symmetry(_permutes_) q)) y 🝖[ _≡_ ]-[ ∃.proof (proof q {y}) ]
        y 🝖[ _≡_ ]-end

  permutation-mapping-bijective : ∀{p : (l₁ permutes l₂)} → Bijective(permutation-mapping p)
  permutation-mapping-bijective {p = p} = injective-surjective-to-bijective(permutation-mapping p) ⦃ permutation-mapping-injective {p = p} ⦄ ⦃ permutation-mapping-surjective {p = p} ⦄

  {-
  permutation-from-mapping : (p : 𝕟(length(l₁)) → 𝕟(length(l₂))) ⦃ bij : Bijective(p) ⦄ (correctness : PermutationMappingCorrectness l₁ l₂ p) → (l₁ permutes l₂)
  permutation-from-mapping {l₁ = ∅} {l₂ = ∅} p _ = empty
  permutation-from-mapping {l₁ = ∅} {l₂ = x₂ ⊰ l₂} p _ = {!!}
  permutation-from-mapping {l₁ = x₁ ⊰ l₁} {l₂ = ∅} p _ = {!!}
  permutation-from-mapping {l₁ = x₁ ⊰ l₁} {l₂ = x₂ ⊰ l₂} p correctness with p(𝟎) | correctness{𝟎}
  ... | 𝟎   | [≡]-intro = prepend (permutation-from-mapping (forgetFirstCutoffOfBij p) ⦃ forgetFirstCutoffOfBij-bijective ⦄ {!!}) where
    bijective-equinumerous : ∀{a b}{f : 𝕟(a) → 𝕟(b)} → Bijective(f) → (a ≡ b)
    forgetFirstCutoff : ∀{a} → (𝕟(𝐒(a)) → 𝕟(𝐒(a))) → (𝕟(a) → 𝕟(a))
    forgetFirstCutoff {𝐒(a)} f(x) with f(𝐒(x))
    ... | 𝟎    = 𝟎
    ... | 𝐒(y) = y

    forgetFirstCutoffOfBij : ∀{a b} → (f : 𝕟(𝐒(a)) → 𝕟(𝐒(b))) ⦃ bij : Bijective(f) ⦄ → (𝕟(a) → 𝕟(b))
    forgetFirstCutoffOfBij {𝐒 a} f ⦃ bij ⦄ with [≡]-intro ← bijective-equinumerous bij = forgetFirstCutoff f
    forgetFirstCutoffOfBij-bijective : ∀{a b}{f : 𝕟(𝐒(a)) → 𝕟(𝐒(b))} ⦃ bij : Bijective(f) ⦄ → Bijective(forgetFirstCutoffOfBij f)

    -- proof : ∀{l₁ l₂ : List(T)}{p : 𝕟(length(l₁)) → 𝕟(length(l₂))} → PermutationMappingCorrectness l₁ l₂ (forgetFirstCutoffOfBij p)
    proof : PermutationMappingCorrectness l₁ l₂ (forgetFirstCutoffOfBij p)
    proof {i} =
      index l₁ i                            🝖[ _≡_ ]-[ {!correctness!} ]
      index l₂ (forgetFirstCutoffOfBij p i) 🝖-end
  ... | 𝐒 w | _ = {!!}
  -}

  permutes-prepend-function : Function ⦃ permutes-equiv ⦄ ⦃ permutes-equiv ⦄ (List.prepend x)
  permutes-prepend-function = intro prepend

  permutes-postpend-function : Function ⦃ permutes-equiv ⦄ ⦃ permutes-equiv ⦄ (postpend x)
  permutes-postpend-function = intro proof where
    proof : (l₁ permutes l₂) → (postpend x l₁) permutes (postpend x l₂)
    proof empty       = prepend empty
    proof (prepend x) = prepend (proof x)
    proof swap        = swap
    proof (trans x y) = trans (proof x) (proof y)

  postpend-prepend-permutes : (postpend x l) permutes (List.prepend x l)
  postpend-prepend-permutes {l = ∅} = prepend empty
  postpend-prepend-permutes {l = x ⊰ l} = trans (prepend postpend-prepend-permutes) swap

  permutes-reverse : (reverse l) permutes l
  permutes-reverse {l = ∅} = empty
  permutes-reverse {l = x ⊰ l} = trans (Function.congruence ⦃ _ ⦄ ⦃ _ ⦄ permutes-postpend-function(permutes-reverse {l = l})) postpend-prepend-permutes

  permutes-length-function : Function ⦃ permutes-equiv {T = T} ⦄ (length)
  permutes-length-function = intro proof where
    proof : (l₁ permutes l₂) → (length l₁ ≡ length l₂)
    proof empty       = [≡]-intro
    proof (prepend p) = congruence₁(𝐒) (proof p)
    proof swap        = [≡]-intro
    proof (trans p q) = transitivity(_≡_) (proof p) (proof q)

  permutes-countᵣ-function : Function ⦃ permutes-equiv ⦄ (count P)
  permutes-countᵣ-function = intro proof where
    proof : (l₁ permutes l₂) → (count P l₁ ≡ count P l₂)
    proof empty = [≡]-intro
    proof {l₁ = x₁ ⊰ l₁} {P = P} (prepend {x = x} p) with P(x)
    ... | 𝑇 = [≡]-with 𝐒(proof {l₁ = l₁} {P = P} p)
    ... | 𝐹 = proof {l₁ = l₁} {P = P} p
    proof {P = P} (swap {x = x} {y = y}) with P(x) | P(y)
    ... | 𝑇 | 𝑇 = [≡]-intro
    ... | 𝑇 | 𝐹 = [≡]-intro
    ... | 𝐹 | 𝑇 = [≡]-intro
    ... | 𝐹 | 𝐹 = [≡]-intro
    proof (trans p q) = proof p 🝖 proof q

  permutes-satisfiesAny-functionᵣ : Function ⦃ permutes-equiv ⦄ (satisfiesAny f)
  permutes-satisfiesAny-functionᵣ = intro proof where
    proof : (l₁ permutes l₂) → (satisfiesAny f l₁ ≡ satisfiesAny f l₂)
    proof empty = [≡]-intro
    proof {f = f} (prepend{x = x} p) with f(x)
    ... | 𝑇 = [≡]-intro
    ... | 𝐹 = proof p
    proof {l₁ = x ⊰ y ⊰ l₁}{y ⊰ x ⊰ l₂}{f = f} (swap{x = x}{y = y}) with f(x) | f(y) | inspect f(x) | inspect f(y)
    ... | 𝑇 | 𝑇 | intro _ | intro _ = [≡]-intro
    ... | 𝑇 | 𝐹 | intro _ | intro _ with 𝑇 ← f(x) = [≡]-intro
    ... | 𝐹 | 𝑇 | intro _ | intro _ with 𝑇 ← f(y) = [≡]-intro
    ... | 𝐹 | 𝐹 | intro _ | intro _ with 𝐹 ← f(x) | 𝐹 ← f(y)= reflexivity(_≡_)
    proof (trans p q) = proof p 🝖 proof q

  {- TODO
  permutes-countₗ : (∀{P} → count P l₁ ≡ count P l₂) → (l₁ permutes l₂)
  permutes-countₗ {l₁ = ∅} {l₂ = ∅} p = empty
  permutes-countₗ {l₁ = ∅} {l₂ = x ⊰ l₂} p with () ← p{const 𝑇}
  permutes-countₗ {l₁ = x ⊰ l₁} {l₂ = ∅} p with () ← p{const 𝑇}
  permutes-countₗ {l₁ = x ⊰ l₁} {l₂ = x₁ ⊰ l₂} p = {!!} -- TODO: The rest of the cases from _permutes_. Maybe decidable equality on the items are required?
  -}

  permutes-[++]-function : BinaryOperator ⦃ permutes-equiv ⦄ ⦃ permutes-equiv ⦄ ⦃ permutes-equiv ⦄ (_++_ {T = T})
  permutes-[++]-function = binaryOperator-from-function ⦃ _ ⦄ ⦃ _ ⦄ ⦃ _ ⦄ ⦃ \{l} → intro(R{l = l}) ⦄ ⦃ intro L ⦄ where
    L : Names.Congruence₁ ⦃ permutes-equiv ⦄ ⦃ permutes-equiv ⦄ (_++ l)
    L {l = l} empty = reflexivity(_permutes_)
    L {l = l} (prepend l12) = prepend (L {l = l} l12)
    L {l = l} swap = swap
    L {l = l} (trans l13 l32) = transitivity(_permutes_) (L {l = l} l13) (L {l = l} l32)

    R : Names.Congruence₁ ⦃ permutes-equiv ⦄ ⦃ permutes-equiv ⦄ (l ++_)
    R {l = ∅}     l12 = l12
    R {l = x ⊰ l} l12 = prepend (R {l = l} l12)

  permutes-[++]-commutativity : Commutativity ⦃ permutes-equiv {T = T} ⦄ (_++_)
  permutes-[++]-commutativity = intro(\{l₁}{l₂} → proof{l₁}{l₂}) where
    proof : Names.Commutativity ⦃ permutes-equiv ⦄ (_++_)
    proof {∅}      {l₂} rewrite identityᵣ(_++_)(∅) {l₂} = reflexivity(_permutes_)
    proof {x ⊰ l₁} {l₂} =
      (x ⊰ l₁) ++ l₂        🝖[ _permutes_ ]-[]
      x ⊰ (l₁ ++ l₂)        🝖[ _permutes_ ]-[ prepend (proof {l₁} {l₂}) ]
      x ⊰ (l₂ ++ l₁)        🝖[ _permutes_ ]-[]
      (x ⊰ l₂) ++ l₁        🝖[ _permutes_ ]-[ BinaryOperator.congruence ⦃ _ ⦄ ⦃ _ ⦄ ⦃ _ ⦄ permutes-[++]-function (postpend-prepend-permutes {l = l₂}) (reflexivity(_permutes_)) ]-sym
      (postpend x l₂) ++ l₁ 🝖[ _permutes_ ]-[ sub₂(_≡_)(_permutes_) ([++]-middle-prepend-postpend {l₁ = l₂}{l₂ = l₁}) ]
      l₂ ++ (x ⊰ l₁)        🝖[ _permutes_ ]-end

  permutes-empty-not-empty : ¬(∅ permutes (x ⊰ l))
  permutes-empty-not-empty (trans {l₂ = ∅}     p q) = permutes-empty-not-empty q
  permutes-empty-not-empty (trans {l₂ = _ ⊰ _} p q) = permutes-empty-not-empty p

  permutes-map : ∀{f : A → B} → Function ⦃ permutes-equiv ⦄ ⦃ permutes-equiv ⦄ (map f)
  permutes-map {f = f} = intro proof where
    proof : Names.Congruence₁ ⦃ permutes-equiv ⦄ ⦃ permutes-equiv ⦄ (map f)
    proof empty       = empty
    proof (prepend p) = prepend (proof p)
    proof swap        = swap
    proof (trans p q) = trans(proof p) (proof q)

  permutes-on-empty : (l permutes ∅) → (l ≡ ∅)
  permutes-on-empty empty = [≡]-intro
  permutes-on-empty (trans p q)
    rewrite permutes-on-empty q
    rewrite permutes-on-empty p
    = [≡]-intro

  permutes-on-singleton : (l permutes (singleton x)) → (l ≡ singleton x)
  permutes-on-singleton (prepend empty) = [≡]-intro
  permutes-on-singleton (prepend (trans p q))
    rewrite permutes-on-empty q
    rewrite permutes-on-empty p
    = [≡]-intro
  permutes-on-singleton (trans p q)
    rewrite permutes-on-singleton q
    rewrite permutes-on-singleton p
    = [≡]-intro

  permutes-insertIn : ∀{n} → ((insertIn x l n) permutes (x ⊰ l))
  permutes-insertIn {n = 𝟎}               = reflexivity(_permutes_)
  permutes-insertIn {l = x ⊰ l} {n = 𝐒 n} = trans (prepend (permutes-insertIn {n = n})) swap

module InsertionPermutation where
  data _insertion-permutes_ {ℓ} : List{ℓ}(T) → List{ℓ}(T) → Stmt{Lvl.𝐒(ℓ)} where
    empty : ∅ insertion-permutes (∅ {T = T})
    ins : (n : 𝕟₌(length l₁)) → (l₁ insertion-permutes l₂) → ((insertIn x l₁ n) insertion-permutes (x ⊰ l₂))

  open import Data.List.Proofs.Length
  open import Relator.Equals.Proofs
  open import Structure.Relator

  insertion-permutation-mapping : (l₁ insertion-permutes l₂) → (𝕟(length(l₁)) → 𝕟(length(l₂)))
  insertion-permutation-mapping empty              ()
  insertion-permutation-mapping (ins 𝟎 p)          𝟎              = 𝟎
  insertion-permutation-mapping (ins 𝟎 p)          (𝐒 i)          = 𝐒(insertion-permutation-mapping p i)
  insertion-permutation-mapping (ins {l₁ = x ⊰ l₁} (𝐒 n) p) 𝟎     = 𝟎
  insertion-permutation-mapping (ins {l₁ = x ⊰ l₁} (𝐒 n) p) (𝐒 i) = 𝐒(insertion-permutation-mapping p (substitute₁(𝕟) (length-insertIn {l = l₁} {n = n}) i))

  open import Data using ()
  open import Numeral.Natural
  open import Relator.Equals
  open import Syntax.Number

  insertion-permutes-prepend : (l₁ insertion-permutes l₂) → ((x ⊰ l₁) insertion-permutes (x ⊰ l₂))
  insertion-permutes-prepend p = ins 𝟎 p

  insertion-permutes-refl : l insertion-permutes l
  insertion-permutes-refl {l = ∅} = empty
  insertion-permutes-refl {l = x ⊰ l} = insertion-permutes-prepend insertion-permutes-refl

  insertion-permutes-swap : (x ⊰ y ⊰ l) insertion-permutes (y ⊰ x ⊰ l)
  insertion-permutes-swap = ins 1 (insertion-permutes-prepend insertion-permutes-refl)

  insertion-permutes-to-permutes : (l₁ insertion-permutes l₂) → (l₁ permutes l₂)
  insertion-permutes-to-permutes empty     = empty
  insertion-permutes-to-permutes (ins n p) = trans Proofs.permutes-insertIn (prepend (insertion-permutes-to-permutes p))

  insertion-permutes-flipped-ins : ∀{n} → (l₁ insertion-permutes l₂) → ((x ⊰  l₁) insertion-permutes (insertIn x l₂ n))
  insertion-permutes-flipped-ins {n = 𝟎}   empty      = insertion-permutes-refl
  insertion-permutes-flipped-ins {n = 𝟎}   (ins k p)  = insertion-permutes-prepend (ins k p)
  insertion-permutes-flipped-ins {n = 𝐒 n} (ins k p) = ins (𝐒 k) (insertion-permutes-flipped-ins {n = n} p)

  insertion-permutes-sym : (l₁ insertion-permutes l₂) → (l₂ insertion-permutes l₁)
  insertion-permutes-sym empty = empty
  insertion-permutes-sym (ins n p) = insertion-permutes-flipped-ins(insertion-permutes-sym p)

  {-
  insertion-permutes-trans : (l₁ insertion-permutes l₂) → (l₃ insertion-permutes l₂) → (l₁ insertion-permutes l₃)
  ins2 : ∀{n₁ n₂} → (l₁ insertion-permutes l₂) → ((insertIn x l₁ n₁) insertion-permutes (insertIn x l₂ n₂))

  ins2 {l₁ = l₁} {l₂} {n₁ = n₁} {𝟎} p = ins n₁ p
  ins2 {l₁ = .(insertIn x _ n)} {x ⊰ l₂} {n₁ = 𝟎} {𝐒 n₂} (ins n p) = insertion-permutes-trans (insertion-permutes-prepend (ins n p)) (ins(𝐒 n₂) insertion-permutes-refl)
  ins2 {l₁ = .(insertIn x _ n)} {x ⊰ l₂} {n₁ = 𝐒 n₁} {𝐒 n₂} (ins n p) = {!!}

  insertion-permutes-trans empty     empty     = empty
  insertion-permutes-trans (ins m p) (ins n q) = {!!}
  -- ins2(insertion-permutes-trans p q)
  -}

  {-
  insertion-permutation-mapping-correctness : (p : (l₁ insertion-permutes l₂)) → Proofs.PermutationMappingCorrectness l₁ l₂ (insertion-permutation-mapping p)
  insertion-permutation-mapping-correctness (ins {l₁ = ∅} 𝟎 p) {𝟎} = [≡]-intro
  insertion-permutation-mapping-correctness (ins {l₁ = x ⊰ l₁} 𝟎 p) {𝟎} = [≡]-intro
  insertion-permutation-mapping-correctness (ins {l₁ = x ⊰ l₁} 𝟎 p) {𝐒 i} = insertion-permutation-mapping-correctness p
  insertion-permutation-mapping-correctness (ins {l₁ = x ⊰ l₁} (𝐒 n) p) {𝟎} = {!!}
  insertion-permutation-mapping-correctness (ins {l₁ = x ⊰ l₁} (𝐒 n) p) {𝐒 i} = {!!}
  -}

  -- test : (p : (l₁ insertion-permutes l₂)) → (∀{i} → (index l₁(insertion-permutation-mapping p i) ≡ index l₂(i)))
  -- test p = ?

  {-
  open import Data.Boolean.Stmt
  open import Numeral.Finite.Oper.Comparisons
  test : ∀{l : List(T)}{n₁ : 𝕟(𝐒(length l))}{n₂ : 𝕟(𝐒(length (insertIn y l n₁)))} → IsTrue(n₁ >? n₂) → (insertIn y (insertIn x l n₁) n₂ ≡ insertIn x (insertIn y l n₁) n₂)
  test p = {!!}
  -}

  {-
  ins2 : ∀{n₁ n₂} → (l₁ insertion-permutes l₂) → ((insertIn x l₁ n₁) insertion-permutes (insertIn x l₂ n₂))
  ins2 {n₁ = 𝟎} {𝟎} empty = insertion-permutes-refl
  ins2 {n₁ = n₁} {𝟎} (ins n p) = ins n₁ (ins n p)
  ins2 {x = x} {n₁ = n₁} {𝐒 n₂} (ins {x = y} n p) = {!(ins2 {x = x}{n₁ = n}{n₂ = n₂} p)!}

  insertion-permutes-trans : (l₁ insertion-permutes l₂) → (l₃ insertion-permutes l₂) → (l₁ insertion-permutes l₃)
  insertion-permutes-trans empty empty = empty
  insertion-permutes-trans (ins m p) (ins n q) = {!!}
  -}

  {-
  test : ∀{n} → (l₁ insertion-permutes (y ⊰ insertIn x l₂ n)) → (l₁ insertion-permutes (x ⊰ insertIn y l₂ n))
  test {l₂ = l₂} (ins {l₁ = l₁} n p) = {!!}

  ins2 : ∀{n₁ n₂} → (l₁ insertion-permutes l₂) → ((insertIn x l₁ n₁) insertion-permutes (insertIn x l₂ n₂))
  ins2 {n₁ = n₁} {𝟎} p = ins n₁ p
  ins2 {n₁ = n₁} {𝐒 n₂} (ins {x = x} n p) = test(ins n₁ (ins2{x = x}{n}{n₂} p))

  -- insertIn x₁ (insertIn x l₁ n) n₁
  -- x ⊰ insertIn x₁ l₂ n₂

  tr : (l₁ insertion-permutes l₂) → (l₃ insertion-permutes l₂) → (l₁ insertion-permutes l₃)
  tr {l₂ = ∅}       empty      empty      = empty
  tr {l₂ = x₂ ⊰ l₂} (ins n₁ p) (ins n₂ q) = ins2(tr p q)

  sym : (l₁ insertion-permutes l₂) → (l₂ insertion-permutes l₁)
  sym = tr insertion-permutes-refl
  -}


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

open import lib.Basics
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Paths
import lib.types.Generic1HIT as Generic1HIT
open import lib.types.Pushout

module lib.types.PushoutFlattening {i} {j} {k} {d : Span {i} {j} {k}} where

open Span d renaming (f to g; g to h)

module PushoutRecType {l} (left* : A → Type l) (right* : B → Type l)
  (glue* : (c : C) → left* (g c) ≃ right* (h c)) where

  open PushoutRec left* right* (ua ∘ glue*) public

  abstract
    coe-glue-β : (c : C) (a : left* (g c))
      → coe (ap f (glue c)) a == –> (glue* c) a
    coe-glue-β c a =
      coe (ap f (glue c)) a  =⟨ glue-β c |in-ctx (λ u → coe u a) ⟩
      coe (ua (glue* c)) a   =⟨ coe-β (glue* c) a ⟩
      –> (glue* c) a ∎

    coe!-glue-β : (c : C) (b : right* (h c))
      → coe! (ap f (glue c)) b == <– (glue* c) b
    coe!-glue-β c b =
      coe! (ap f (glue c)) b  =⟨ glue-β c |in-ctx (λ u → coe! u b) ⟩
      coe! (ua (glue* c)) b   =⟨ coe!-β (glue* c) b ⟩
      <– (glue* c) b ∎

    ↓-glue-out : (c : C) {a : left* (g c)} {b : right* (h c)}
      → a == b [ f ↓ glue c ]
      → –> (glue* c) a == b
    ↓-glue-out c {a} {b} p =
      –> (glue* c) a          =⟨ ! (coe-glue-β c a) ⟩
      coe (ap f (glue c)) a   =⟨ to-transp p ⟩
      b ∎

    ↓-glue-in : (c : C) {a : left* (g c)} {b : right* (h c)}
      → –> (glue* c) a == b
      → a == b [ f ↓ glue c ]
    ↓-glue-in c {a} {b} p = from-transp f (glue c) (coe-glue-β c a ∙ p)

  private
    module _ where
      fA : Type _
      fA = Σ A left*

      fB : Type _
      fB = Σ B right*

      fC : Type _
      fC = Σ C (left* ∘ g)

      fg : fC → fA
      fg (c , c') = (g c , c')

      fh : fC → fB
      fh (c , c') = (h c , –> (glue* c) c')

    f-d : Span
    f-d = span fA fB fC fg fh

  flattening : Σ (Pushout d) f == Pushout f-d
  flattening = Σ= p p' ∙ q ∙ r ∙ s  where

    module G = PushoutGeneric {d = d}

    P-cc : Coprod A B → Type _
    P-cc (inl a) = left* a
    P-cc (inr b) = right* b

    module P = G.RecType P-cc glue*

    import lib.types.Flattening as Flattening
    module FlatteningPushout = Flattening
      (Coprod A B) C (inl ∘ g) (inr ∘ h) P-cc glue*
    open FlatteningPushout public hiding (flattening-equiv; module P)

    p-equiv : Pushout d ≃ G.T
    p-equiv = G.generic-pushout

    p : Pushout d == G.T
    p = ua p-equiv

    p' : f == P.f [ (λ X → (X → Type _)) ↓ p ]
    p' = ↓-app→cst-in (λ {t} {t'} q →
           Pushout-elim {P = λ t → f t == P.f (–> p-equiv t)}
             (λ a → idp) (λ b → idp)
             (λ c → ↓-='-in
               (ap (P.f ∘ (–> p-equiv)) (glue c)    =⟨ ap-∘ P.f (–> p-equiv) (glue c) ⟩
                ap P.f (ap (–> p-equiv) (glue c))   =⟨ G.To.glue-β c |in-ctx ap P.f ⟩
                ap P.f (pp c)                       =⟨ P.pp-β c ⟩
                ua (glue* c)                        =⟨ ! (glue-β c) ⟩
                ap f (glue c) ∎))
         t ∙ ap P.f (↓-idf-ua-out _ q))

    --

    module fG' = Generic1HIT At Bt ft gt

    q : Σ G.T P.f == fG'.T
    q = ua FlatteningPushout.flattening-equiv

    --

    {-
    This part is basically [Generic1HIT=] applied to the flattening lemma
    for coproducts. Maybe it would make sense to refactor it that way.
    -}

    module fG = PushoutGeneric {d = f-d}

    r : fG'.T == fG.T
    r = ua (equiv to from to-from from-to)  where

      to-cc : At → fG.T
      to-cc (inl a , a') = fG.cc (inl (a , a'))
      to-cc (inr b , b') = fG.cc (inr (b , b'))

      module To = fG'.Rec to-cc fG.pp

      to : fG'.T → fG.T
      to = To.f

      from-cc : Coprod fA fB → fG'.T
      from-cc (inl (a , a')) = fG'.cc (inl a , a')
      from-cc (inr (b , b')) = fG'.cc (inr b , b')

      module From = fG.Rec from-cc fG'.pp

      from : fG.T → fG'.T
      from = From.f

      abstract
        to-from : (x : fG.T) → to (from x) == x
        to-from = fG.elim to-from-cc to-from-pp  where
          to-from-cc : (x : Coprod fA fB)
            → to (from (fG.cc x)) == fG.cc x
          to-from-cc (inl _) = idp
          to-from-cc (inr _) = idp

          to-from-pp : (c : fC)
            → idp == idp [ (λ x → to (from x) == x) ↓ fG.pp c ]
          to-from-pp c = ↓-∘=idf-in to from
            (ap to (ap from (fG.pp c))   =⟨ From.pp-β c |in-ctx ap to ⟩
             ap to (fG'.pp c)            =⟨ To.pp-β c ⟩
             fG.pp c ∎)

        from-to : (x : fG'.T) → from (to x) == x
        from-to = fG'.elim from-to-cc from-to-pp  where
          from-to-cc : (a : At) → from (to (fG'.cc a)) == fG'.cc a
          from-to-cc (inl _ , _) = idp
          from-to-cc (inr _ , _) = idp

          from-to-pp : (b : Bt)
            → idp == idp [ (λ x → from (to x) == x) ↓ fG'.pp b ]
          from-to-pp b = ↓-∘=idf-in from to
            (ap from (ap to (fG'.pp b))   =⟨ To.pp-β b |in-ctx ap from ⟩
             ap from (fG.pp b)            =⟨ From.pp-β b ⟩
             fG'.pp b ∎)

    --

    s : fG.T == Pushout f-d
    s = ! (ua fG.generic-pushout)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
postulate
  A : Set
  I : (@erased _ : A) → Set
  R : A → Set
  f : ∀ (@erased x : A) (r : R x) → I x
 -- can now be used here ^


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.NatMinusOne.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat
open import Cubical.Data.NatMinusOne.Base

-1+Path : ℕ ≡ ℕ₋₁
-1+Path = isoToPath (iso -1+_ 1+_ (λ _ → refl) (λ _ → refl))

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: data _ : Set where

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2016-09-28, Level meta below neutral level
-- Agda previously simplified X <= a to X = a.
-- This loses the solution X = lzero.

-- {-# OPTIONS -v tc.constr.add:40 #-}

open import Common.Level

module _ (a : Level) where

module WorksWithSwappedDeclarations where

  mutual
    X : Level
    X = _

    data E : Set₁ where
      c : Set X → E  -- constraint lsuc X <= 1 solves X = lzero

    data D : Set (lsuc a) where
      c : Set X → D  -- fine since lzero <= a

module WorksWithGivenSolution where

  mutual
    X : Level
    X = lzero

    data D : Set (lsuc a) where
      c : Set X → D

    data E : Set₁ where
      c : Set X → E

module Test where

  mutual
    X : Level
    X = _

    data D : Set (lsuc a) where
      c : Set X → D  -- solved X (prematurely) since X <= a implies X = a ?? (Wrong!)

    data E : Set₁ where
      c : Set X → E  -- constraint X <= 0 became contradictory constraint a <= 0

-- ERROR WAS:
-- The type of the constructor does not fit in the sort of the
-- datatype, since Set (lsuc a) is not less or equal than Set₁
-- when checking the constructor c in the declaration of E

-- should succeed


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.TBox.Interp using ( Δ ; _⊨_≈_ ) renaming
  ( Interp to Interp′ ; emp to emp′ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.Util using ( False ; id )

module Web.Semantic.DL.ABox.Interp where

infixr 4 _,_
infixr 5 _*_

data Interp (Σ : Signature) (X : Set) : Set₁ where
  _,_ : ∀ I → (X → Δ {Σ} I) → (Interp Σ X)

⌊_⌋ : ∀ {Σ X} → Interp Σ X → Interp′ Σ
⌊ I , i ⌋ = I

ind : ∀ {Σ X} → (I : Interp Σ X) → X → Δ ⌊ I ⌋
ind (I , i) = i

ind² : ∀ {Σ X} → (I : Interp Σ X) → (X × X) → (Δ ⌊ I ⌋ × Δ ⌊ I ⌋)
ind² I (x , y) = (ind I x , ind I y)

_*_ : ∀ {Σ X Y} → (Y → X) → Interp Σ X → Interp Σ Y
f * I = (⌊ I ⌋ , λ x → ind I (f x))

emp : ∀ {Σ} → Interp Σ False
emp = (emp′ , id)

data Surjective {Σ X} (I : Interp Σ X) : Set where
  surj : (∀ x → ∃ λ y → ⌊ I ⌋ ⊨ x ≈ ind I y) → (I ∈ Surjective)

ind⁻¹ : ∀ {Σ X} {I : Interp Σ X} → (I ∈ Surjective) → (Δ ⌊ I ⌋ → X)
ind⁻¹ (surj i) x = proj₁ (i x)

surj✓ : ∀ {Σ X} {I : Interp Σ X} (I∈Surj : I ∈ Surjective) → ∀ x → (⌊ I ⌋ ⊨ x ≈ ind I (ind⁻¹ I∈Surj x))
surj✓ (surj i) x = proj₂ (i x)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
module cwf where

open import Nat
open import Base
open import univ
open import help

-- Category with Families

infix 40 _─→_
infixl 50 _,_ _,,_
infixl 70 _∘_ _∙_
infixl 60 _/_ _//_

Con : Set
Con = S

_─→_ : Con -> Con -> Set
Γ ─→ Δ = El (pi Γ (K Δ))

p─→ : {Γ Δ : Con}(σ : Γ ─→ Δ){x y : El Γ} -> x == y -> σ # x == σ # y
p─→ σ {x}{y} x=y =
  chain> σ # x
     === refS << σ # y by pFun σ x=y
     === σ # y         by ref<< (σ # y)
  where open module C13 = Chain _==_ (ref {_}) (trans {_})

id : {Γ : Con} -> Γ ─→ Γ
id = el < (\x -> x) , (\{x}{y} -> prf x y) >
  where
    prf : (x y : El _)(x=y : x == y) -> x == refS << y
    prf x y x=y =
      chain> x
         === refS << x by sym (ref<< x)
         === refS << y by p<< refS x=y
      where open module C0 = Chain _==_ (ref {_}) (trans {_})

_∘_ : {Γ Δ Θ : Con} -> (Δ ─→ Θ) -> (Γ ─→ Δ) -> Γ ─→ Θ
σ ∘ δ = el < (\x -> σ # (δ # x))
           , (\{x}{y} -> prf x y)
           >
  where
    prf : (x y : El _)(x=y : x == y) -> σ # (δ # x) == _ << σ # (δ # y)
    prf x y x=y =
      chain> σ # (δ # x)
         === σ # (δ # y)      by p─→ σ (p─→ δ x=y)
         === _ << σ # (δ # y) by sym (castref _ _)
      where open module C1 = Chain _==_ (ref {_}) (trans {_})

Type : Con -> Set
Type Γ = Fam Γ

data _=Ty_ {Γ : Con}(A B : Type Γ) : Set where
  eqTy : A =Fam B -> A =Ty B

symTy : {Γ : Con}{A B : Type Γ} -> A =Ty B -> B =Ty A
symTy {Γ}{A}{B} (eqTy A=B) = eqTy (symFam {Γ}{A}{B} A=B)

_/_ : {Γ Δ : Con} -> Type Γ -> (Δ ─→ Γ) -> Type Δ
_/_ {Γ}{Δ} A (el < σ , pσ >) = fam B pB
  where
    B : El Δ -> S
    B x = A ! σ x

    σ' : Δ ─→ Γ
    σ' = el < σ , (\{x}{y} -> pσ) >

    pB : Map _==_ _=S_ B
    pB {x}{y} x=y = pFam A (p─→ σ' x=y)

lem-/id : {Γ : Con}{A : Type Γ} -> A / id =Ty A
lem-/id {Γ}{A} = eqTy \x -> refS

data Elem (Γ : Con)(A : Type Γ) : Set where
  elem : El (pi Γ A) -> Elem Γ A

_=El'_ : {Γ : Con}{A : Type Γ} -> Elem Γ A -> Elem Γ A -> Set
elem u =El' elem v = u == v

data _=El_ {Γ : Con}{A : Type Γ}(u v : Elem Γ A) : Set where
  eqEl : u =El' v -> u =El v

castElem : {Γ : Con}{A B : Type Γ} -> B =Ty A -> Elem Γ A -> Elem Γ B
castElem {Γ}{A}{B} (eqTy B=A) (elem u) = elem (ΓB=ΓA << u)
  where
    ΓB=ΓA : pi Γ B =S pi Γ A
    ΓB=ΓA = eqS < refS , Bx=Acx >
      where
        Bx=Acx : (x : El Γ) -> B ! x =S A ! (refS << x)
        Bx=Acx x =
          chain> B ! x
             === A ! x            by B=A x
             === A ! (refS << x)  by pFam A (sym (ref<< x))
          where open module C2-5 = Chain _=S_ refS transS

_//_ : {Γ Δ : Con}{A : Type Γ} -> Elem Γ A -> (σ : Δ ─→ Γ) -> Elem Δ (A / σ)
_//_ {Γ}{Δ}{A} (elem t) (el < σ , pσ >) =
    elem (el < tσ , (\{x}{y} -> prf x y) >)
  where
    tσ : (x : El Δ) -> El (A ! σ x)
    tσ x = t # σ x

    σ' : Δ ─→ Γ
    σ' = el < σ , (\{x}{y} -> pσ) >

    prf : (x y : El Δ)(x=y : x == y) -> t # σ x == _ << t # σ y
    prf x y x=y =
      chain> t # σ x
         === _ << t # σ y by pFun t (p─→ σ' x=y)
         === _ << t # σ y by pfi _ _ _
      where open module C3 = Chain _==_ (ref {_}) (trans {_})

_,_ : (Γ : Con)(A : Type Γ) -> Con
Γ , A = sigma Γ A

wk : {Γ : Con}{A : Type Γ} -> Γ , A ─→ Γ
wk {Γ}{A} = el < f , (\{x}{y} -> pf x y) >
  where
    f : El (Γ , A) -> El Γ
    f (el < x , _ >) = x

    pf : (x y : El (Γ , A))(x=y : x == y) -> f x == _ << f y
    pf (el < x , _ >) (el < y , _ >) (eq < x=y , _ >) =
      chain> x
         === y      by x=y
         === _ << y by sym (castref _ _)
      where open module C4 = Chain _==_ (ref {_}) (trans {_})

vz : {Γ : Con}{A : Type Γ} -> Elem (Γ , A) (A / wk)
vz {Γ}{A} = elem (el < f , (\{x}{y} -> pf x y) >)
  where
    f : (x : El (Γ , A)) -> El ((A / wk) ! x)
    f (el < _ , z >) = z

    pf : (x y : El (Γ , A))(x=y : x == y) -> f x == _ << f y
    pf (el < _ , x >)(el < _ , y >)(eq < _ , x=y >) =
      chain> x
         === _ << y by x=y
         === _ << y by pfi _ _ _
      where open module C5 = Chain _==_ (ref {_}) (trans {_})

_,,_ : {Γ Δ : Con}{A : Type Γ}(σ : Δ ─→ Γ)(u : Elem Δ (A / σ)) -> Δ ─→ Γ , A
_,,_ {Γ}{Δ}{A} (el < σ , pσ >) (elem (el < u , pu >)) = build δ pδ
  where
    -- We need to generalise to be able to infer the proof of Γ, A =S Γ, A
    Ok : (f : El Δ -> El (Γ , A)) -> Set
    Ok f = (x y : El Δ)(p : Γ , A =S Γ , A)(x=y : x == y) -> f x == p << f y

    build : (f : El Δ -> El (Γ , A)) -> Ok f -> Δ ─→ Γ , A
    build f p = el < f , (\{x}{y} -> p x y _) >

    δ : El Δ -> El (Γ , A)
    δ x = el {Γ , A} < σ x , u x >

    pδ : Ok δ
    pδ x y (eqS < Γ=Γ , A=A >) x=y =
      eq < σx=cσy , ux=ccuy >
      where
        σx=cσy = trans (pσ x=y) (pfi _ _ _)
        ux=ccuy =
          chain> u x
             === _ << u y      by pu x=y
             === _ << _ << u y by sym (casttrans _ _ _ _)
          where open module C6 = Chain _==_ (ref {_}) (trans {_})

{- TODO: Prove

  wk ∘ (σ ,, u) = σ
  vz / (σ ,, u) = u

  (σ ,, u) ∘ δ  = (σ ∘ δ ,, u)
  wk ,, vz      = id

-}

[_] : {Γ : Con}{A : Type Γ} -> Elem Γ A -> Γ ─→ Γ , A
[_] {Γ}{A} u = id ,, castElem lem-/id u

Π : {Γ : Con}(A : Type Γ)(B : Type (Γ , A)) -> Type Γ
Π {Γ} A B = fam F pF
  where
    F : El Γ -> S
    F x = pi (A ! x) (curryFam B x)

    pF : Map _==_ _=S_ F
    pF {y}{z} y=z = eqS
        < pFam A (sym y=z)
        , (\x -> pFam B (eq < y=z
                            , trans (sym (castref _ _)) (trans<< _ _ _)
                            >
                        )
          )
        >

{- TODO: Prove

  (Π A B) / σ = Π (A / σ) (B / (σ / wk ,, vz))

-}

ƛ : {Γ : Con}{A : Type Γ}{B : Type (Γ , A)} -> Elem (Γ , A) B -> Elem Γ (Π A B)
ƛ {Γ}{A}{B} (elem u) = elem (mkFun f pf)
  where
    f : (x : El Γ) -> El (Π A B ! x)
    f x = el < g , (\{x}{y} -> pg) >
      where
        g : (y : El (A ! x)) -> El (B ! el < x , y >)
        g y = u # el < x , y >

        pg : {y z : El (A ! x)}(y=z : y == z) -> g y == _ << g z
        pg {y}{z} y=z =
          chain> u # el < x , y >
             === _ << u # el < x , z > by pFun u (eqSnd y=z)
             === _ << u # el < x , z > by pfi _ _ _
          where open module C7 = Chain _==_ (ref {_}) (trans {_})

    pf : IsFun {F = Π A B} f
    pf {y}{z} (eqS < Ay=Az , B'=B' >) y=z = eq prf
      where
        prf : (x : El (A ! y)) -> _ == _
        prf x =
          chain> u # el < y , x >
             === _ << u # el < z , _ << x >
              by pFun u (eq < y=z , sym (castref2 _ _ _) >)
             === _ << u # el < z , _ << x > by pfi _ _ _
          where open module C8 = Chain _==_ (ref {_}) (trans {_})

_∙_ : {Γ : Con}{A : Type Γ}{B : Type (Γ , A)}
      (w : Elem Γ (Π A B))(u : Elem Γ A) -> Elem Γ (B / [ u ])
_∙_ {Γ}{A}{B} (elem w) (elem u) = elem (el < f , (\{x}{y} -> pf) >)
  where
    f : (x : El Γ) -> El ((B / [ elem u ]) ! x)
    f x = p u << y
      where
        y : El (B ! el < x , u # x >)
        y = (w # x) # (u # x)

        p : (u : El (pi Γ A)) -> (B / [ elem u ]) ! x =S B ! el < x , u # x >
        p (el < u , pu >) = pFam B (
          chain> el < x , _ << u (refS << x) >
             === el < x , _ << _ << u x > by eqSnd (p<< _ (pu (ref<< _)))
             === el < x , u x >           by eqSnd (castref2 _ _ _)
          )
          where open module C9 = Chain _==_ (ref {_}) (trans {_})

    pf : {x y : El Γ}(x=y : x == y) -> f x == _ << f y
    pf {x}{y} x=y =
      chain> q1 << (w # x) # (u # x)
         === q1 << (q3 << w # y) ## (u # x)
          by p<< q1 (p# (pFun w x=y))
         === q1 << q4 << (w # y) # (q5 << u # x)
          by p<< q1 (distr<<# (w # y) q3)
         === q7 << (w # y) # (q5 << u # x)
          by sym (trans<< q1 q4 _)
         === q7 << q8 << (w # y) # (q5 << q9 << u # y)
          by p<< q7 (pFun (w # y) (p<< q5 (pFun u x=y)))
         === qA << (w # y) # (q5 << q9 << u # y)
          by sym (trans<< q7 q8 _)
         === qA << qB << (w # y) # (u # y)
          by p<< qA (pFun (w # y) (castref2 q5 q9 _))
         === q2 << q6 << (w # y) # (u # y)
          by pfi2 qA q2 qB q6 _
      where
        open module C10 = Chain _==_ (ref {_}) (trans {_})
        q1 = _
        q2 = _
        q3 = _
        q4 = _
        q5 = _
        q6 = _
        q7 = _
        q8 = _
        q9 = _
        qA = _
        qB = _
        infixl 150 _##_
        _##_ = _#_ {F = curryFam B x}

{- TODO: Prove

  (ƛ v) ∙ u = v // [ u ]    (β)
  w = ƛ ((w // wk) ∙ vz)    (η)

  ƛ v // σ = ƛ (v // (σ ∘ wk ,, vz))
  w ∙ u // σ = (w // σ) ∙ (u // σ)

-}


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyFun where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat hiding (_·_) renaming (_+_ to _+n_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.GradedRing.DirectSumFun

private variable
  ℓ : Level

module _
  (ACommRing@(A , Astr) : CommRing ℓ)
  where

  open CommRingStr Astr
  open RingTheory (CommRing→Ring ACommRing)

  UnivariatePolyFun-CommRing : CommRing ℓ
  UnivariatePolyFun-CommRing = ⊕FunGradedRing-CommRing
                   _+n_ (makeIsMonoid isSetℕ +-assoc +-zero λ _ → refl) (λ _ _ → refl)
                   (λ _ → A)
                   (λ _ → snd (Ring→AbGroup (CommRing→Ring ACommRing)))
                   1r _·_ 0LeftAnnihilates 0RightAnnihilates
                   (λ a b c → ΣPathP ((+-assoc _ _ _) , (·Assoc _ _ _)))
                   (λ a → ΣPathP ((+-zero _) , (·IdR _)))
                   (λ a → ΣPathP (refl , (·IdL _)))
                   ·DistR+
                   ·DistL+
                   λ x y → ΣPathP ((+-comm _ _) , (·Comm _ _))

nUnivariatePolyFun : (A' : CommRing ℓ) → (n : ℕ) → CommRing ℓ
nUnivariatePolyFun A' zero = A'
nUnivariatePolyFun A' (suc n) = UnivariatePolyFun-CommRing (nUnivariatePolyFun A' n)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All

module LibraBFT.Impl.Execution.ExecutorTypes.StateComputeResult where

extensionProof : StateComputeResult → AccumulatorExtensionProof
extensionProof self = AccumulatorExtensionProof∙new (self ^∙ scrObmNumLeaves)