text:
{-# OPTIONS --without-K #-}
module common-utilities where
open import common

lift-≟-1 : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} → (f : A → B) → {x : A} → {y : A} → Maybe (x ≡ y) → Maybe (f x ≡ f y)
lift-≟-1 f (just refl) = just refl
lift-≟-1 f nothing = nothing

lift-≟-1-refl : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} f {x} p → p ≡ just refl → lift-≟-1 {ℓ} {ℓ′} {A} {B} f {x} {x} p ≡ just refl
lift-≟-1-refl f ._ refl = refl

lift-≟-2-helper : ∀ {A : Set} {B : A → Set} {C : Set} {f : (x : A) → B x → C} {x : A} {y y' : B x} → Maybe (y ≡ y') → Maybe (f x y ≡ f x y')
lift-≟-2-helper (just refl) = just refl
lift-≟-2-helper nothing = nothing

lift-≟-2 : ∀ {A} {B : A → Set} {C} → (f : (x : A) → B x → C) → {x x' : A} → {y : B x} → {y' : B x'} → Maybe (x ≡ x') → ((p : x ≡ x') → Maybe (transport B p y ≡ y')) → Maybe (f x y ≡ f x' y')
lift-≟-2 {A} {B} {C} f {x} {.x} {y} {y'} (just refl) p = lift-≟-2-helper {A} {B} {C} {f} {x} {y} {y'} (p refl)
lift-≟-2 f nothing _ = nothing

lift-≟-2-helper-refl : ∀ {A B C f x y p} → p ≡ just refl → lift-≟-2-helper {A} {B} {C} {f} {x} {y} {y} p ≡ just refl
lift-≟-2-helper-refl refl = refl

lift-≟-2-refl : ∀ {A B C} f {x} {y} p q → p ≡ just refl → q refl ≡ just refl → lift-≟-2 {A} {B} {C} f {x} {x} {y} {y} p q ≡ just refl
lift-≟-2-refl {A} {B} {C} f {x} {y} ._ q refl q' = lift-≟-2-helper-refl {A} {B} {C} {f} {x} {y} {q refl} q'

lift-≟-3-helper : ∀ {A : Set} {B : A → Set} {C D} → {f : (x : A) → (y : B x) → C x y → D} → {x : A} → {y y' : B x} → {z : C x y} → {z' : C x y'} → Maybe (y ≡ y') → ((q : y ≡ y') → Maybe (transport2 C refl q z ≡ z')) → Maybe (f x y z ≡ f x y' z')
lift-≟-3-helper {A} {B} {C} {D} {f} {x} {y} {.y} {z} {z'} (just refl) q = lift-≟-2-helper {B x} {C x} {D} {f x} {y} {z} {z'} (q refl)
lift-≟-3-helper nothing q = nothing

lift-≟-3 : ∀ {A B C D} → (f : (x : A) → (y : B x) → C x y → D) → {x x' : A} → {y : B x} → {y' : B x'} → {z : C x y} → {z' : C x' y'} → Maybe (x ≡ x') → ((p : x ≡ x') → Maybe (transport B p y ≡ y')) → ((p : x ≡ x') → (q : transport B p y ≡ y') → Maybe (transport2 C p q z ≡ z')) → Maybe (f x y z ≡ f x' y' z')
lift-≟-3 {A} {B} {C} {D} f {x} {.x} {y} {y'} {z} {z'} (just refl) q r = lift-≟-3-helper {A} {B} {C} {D} {f} {x} {y} {y'} {z} {z'} (q refl) (r refl)
lift-≟-3 f nothing q r = nothing

lift-≟-3-helper-refl : ∀ {A B C D f x y z p q} → p ≡ just refl → q refl ≡ just refl → lift-≟-3-helper {A} {B} {C} {D} {f} {x} {y} {y} {z} {z} p q ≡ just refl
lift-≟-3-helper-refl {A} {B} {C} {D} {f} {x} {y} {z} {._} {q} refl q' = lift-≟-2-helper-refl {B x} {C x} {D} {f x} {y} {z} {q refl} q'

lift-≟-3-refl : ∀ {A B C D} f {x y z} p q r → p ≡ just refl → q refl ≡ just refl → r refl refl ≡ just refl → lift-≟-3 {A} {B} {C} {D} f {x} {x} {y} {y} {z} {z} p q r ≡ just refl
lift-≟-3-refl {A} {B} {C} {D} f {x} {y} {z} ._ q r refl q' r' = lift-≟-3-helper-refl {A} {B} {C} {D} {f} {x} {y} {z} {q refl} {r refl} q' r'

lift-≟-4-helper : ∀ {A : Set} {B : A → Set} {C : (x : A) → B x → Set} {D : (x : A) → (y : B x) → C x y → Set} {E} → {f : (x : A) → (y : B x) → (z : C x y) → (w : D x y z) → E} → {x : A} → {y y' : B x} → {z : C x y} → {z' : C x y'} → {w : D x y z} → {w' : D x y' z'} → Maybe (y ≡ y') → ((q : y ≡ y') → Maybe (transport2 C refl q z ≡ z')) → ((q : y ≡ y') → (r : transport2 C refl q z ≡ z') → Maybe (transport3 D refl q r w ≡ w')) → Maybe (f x y z w ≡ f x y' z' w')
lift-≟-4-helper {A} {B} {C} {D} {E} {f} {x} {y} {.y} {z} {z'} {w} {w'} (just refl) q r = lift-≟-3-helper {B x} {C x} {D x} {E} {f x} {y} {z} {z'} {w} {w'}
                                                                                (q refl) (r refl)
lift-≟-4-helper nothing q r = nothing

lift-≟-4 : ∀ {A B C D E} → (f : (x : A) → (y : B x) → (z : C x y) → (w : D x y z) → E) → {x x' : A} → {y : B x} → {y' : B x'} → {z : C x y} → {z' : C x' y'} → {w : D x y z} → {w' : D x' y' z'}
  → Maybe (x ≡ x')
  → ((p : x ≡ x') → Maybe (transport B p y ≡ y'))
  → ((p : x ≡ x') → (q : transport B p y ≡ y') → Maybe (transport2 C p q z ≡ z'))
  → ((p : x ≡ x') → (q : transport B p y ≡ y') → (r : transport2 C p q z ≡ z') → Maybe (transport3 D p q r w ≡ w'))
  → Maybe (f x y z w ≡ f x' y' z' w')
lift-≟-4 {A} {B} {C} {D} {E} f {x} {.x} {y} {y'} {z} {z'} {w} {w'} (just refl) q r s = lift-≟-4-helper {A} {B} {C} {D} {E} {f} {x} {y} {y'} {z} {z'} {w} {w'} (q refl) (r refl) (s refl)
lift-≟-4 f nothing q r s = nothing

lift-≟-5-helper : ∀ {A : Set} {B : A → Set} {C : (x : A) → B x → Set} {D : (x : A) → (y : B x) → C x y → Set} {E F} → {f : (x : A) → (y : B x) → (z : C x y) → (w : D x y z) → (v : E x y z w) → F} → {x : A} → {y y' : B x} → {z : C x y} → {z' : C x y'} → {w : D x y z} → {w' : D x y' z'} → {v : E x y z w} → {v' : E x y' z' w'} → Maybe (y ≡ y') → ((q : y ≡ y') → Maybe (transport2 C refl q z ≡ z')) → ((q : y ≡ y') → (r : transport2 C refl q z ≡ z') → Maybe (transport3 D refl q r w ≡ w')) → ((q : y ≡ y') → (r : transport2 C refl q z ≡ z') → (s : transport3 D refl q r w ≡ w') → Maybe (transport4 E refl q r s v ≡ v')) → Maybe (f x y z w v ≡ f x y' z' w' v')
lift-≟-5-helper {A} {B} {C} {D} {E} {F} {f} {x} {y} {.y} {z} {z'} {w} {w'} {v} {v'} (just refl) q r s
  = lift-≟-4-helper {B x} {C x} {D x} {E x} {F} {f x} {y} {z} {z'} {w}
      {w'} {v} {v'} (q refl) (r refl) (s refl)
lift-≟-5-helper nothing q r s = nothing

lift-≟-5 : ∀ {A B C D E F} → (f : (x : A) → (y : B x) → (z : C x y) → (w : D x y z) → (v : E x y z w) → F) → {x x' : A} → {y : B x} → {y' : B x'} → {z : C x y} → {z' : C x' y'} → {w : D x y z} → {w' : D x' y' z'} → {v : E x y z w} → {v' : E x' y' z' w'} → Maybe (x ≡ x') → ((p : x ≡ x') → Maybe (transport B p y ≡ y')) → ((p : x ≡ x') → (q : transport B p y ≡ y') → Maybe (transport2 C p q z ≡ z')) → ((p : x ≡ x') → (q : transport B p y ≡ y') → (r : transport2 C p q z ≡ z') → Maybe (transport3 D p q r w ≡ w')) → ((p : x ≡ x') → (q : transport B p y ≡ y') → (r : transport2 C p q z ≡ z') → (s : transport3 D p q r w ≡ w') → Maybe (transport4 E p q r s v ≡ v')) → Maybe (f x y z w v ≡ f x' y' z' w' v')
lift-≟-5 {A} {B} {C} {D} {E} {F} f {x} {.x} {y} {y'} {z} {z'} {w} {w'} {v} {v'} (just refl) q r s t = lift-≟-5-helper {A} {B} {C} {D} {E} {F} {f} {x} {y} {y'} {z} {z'} {w} {w'} {v} {v'} (q refl) (r refl) (s refl) (t refl)
lift-≟-5 f nothing q r s t = nothing

lift-≟-4-helper-refl : ∀ {A B C D E f x y z w p q r} → p ≡ just refl → q refl ≡ just refl → r refl refl ≡ just refl → lift-≟-4-helper {A} {B} {C} {D} {E} {f} {x} {y} {y} {z} {z} {w} {w} p q r ≡ just refl
lift-≟-4-helper-refl {A} {B} {C} {D} {E} {f} {x} {y} {z} {w} {._} {q} {r} refl q' r' = lift-≟-3-helper-refl {B x} {C x} {D x} {E} {f x} {y} {z} {w}
                                                                                {q refl} {r refl} q' r'

lift-≟-4-refl : ∀ {A B C D E} f {x y z w} p q r s → p ≡ just refl → q refl ≡ just refl → r refl refl ≡ just refl → s refl refl refl ≡ just refl → lift-≟-4 {A} {B} {C} {D} {E} f {x} {x} {y} {y} {z} {z} {w} {w} p q r s ≡ just refl
lift-≟-4-refl {A} {B} {C} {D} {E} f {x} {y} {z} {w} ._ q r s refl q' r' s' = lift-≟-4-helper-refl {A} {B} {C} {D} {E} {f} {x} {y} {z} {w} {q refl} {r refl} {s refl} q' r' s'

lift-≟-5-helper-refl : ∀ {A B C D E F f x y z w v p q r s} → p ≡ just refl → q refl ≡ just refl → r refl refl ≡ just refl → s refl refl refl ≡ just refl → lift-≟-5-helper {A} {B} {C} {D} {E} {F} {f} {x} {y} {y} {z} {z} {w} {w} {v} {v} p q r s ≡ just refl
lift-≟-5-helper-refl {A} {B} {C} {D} {E} {F} {f} {x} {y} {z} {w} {v} {._} {q} {r} {s} refl q' r' s'
  = lift-≟-4-helper-refl {B x} {C x} {D x} {E x} {F} {f x} {y} {z} {w}
      {v} {q refl} {r refl} {s refl} q' r' s'

lift-≟-5-refl : ∀ {A B C D E F} f {x y z w v} p q r s t → p ≡ just refl → q refl ≡ just refl → r refl refl ≡ just refl → s refl refl refl ≡ just refl → t refl refl refl refl ≡ just refl → lift-≟-5 {A} {B} {C} {D} {E} {F} f {x} {x} {y} {y} {z} {z} {w} {w} {v} {v} p q r s t ≡ just refl
lift-≟-5-refl {A} {B} {C} {D} {E} {F} f {x} {y} {z} {w} {v} ._ q r s t refl q' r' s' t' = lift-≟-5-helper-refl {A} {B} {C} {D} {E} {F} {f} {x} {y} {z} {w} {v} {q refl} {r refl} {s refl} {t refl} q' r' s' t'

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Types and functions which are used to keep track of height
-- invariants in AVL Trees
------------------------------------------------------------------------

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

module Data.AVL.Height where

open import Data.Nat.Base
open import Data.Fin using (Fin; zero; suc)

ℕ₂ = Fin 2
pattern 0# = zero
pattern 1# = suc zero
pattern ## = suc (suc ())

-- Addition.

infixl 6 _⊕_

_⊕_ : ℕ₂ → ℕ → ℕ
0# ⊕ n = n
1# ⊕ n = 1 + n
## ⊕ n

-- pred[ i ⊕ n ] = pred (i ⊕ n).

pred[_⊕_] : ℕ₂ → ℕ → ℕ
pred[ i ⊕ zero  ] = 0
pred[ i ⊕ suc n ] = i ⊕ n

infix 4 _∼_⊔_

-- If i ∼ j ⊔ m, then the difference between i and j is at most 1,
-- and the maximum of i and j is m. _∼_⊔_ is used to record the
-- balance factor of the AVL trees, and also to ensure that the
-- absolute value of the balance factor is never more than 1.

data _∼_⊔_ : ℕ → ℕ → ℕ → Set where
  ∼+ : ∀ {n} →     n ∼ 1 + n ⊔ 1 + n
  ∼0 : ∀ {n} →     n ∼ n     ⊔ n
  ∼- : ∀ {n} → 1 + n ∼ n     ⊔ 1 + n

-- Some lemmas.

max∼ : ∀ {i j m} → i ∼ j ⊔ m → m ∼ i ⊔ m
max∼ ∼+ = ∼-
max∼ ∼0 = ∼0
max∼ ∼- = ∼0

∼max : ∀ {i j m} → i ∼ j ⊔ m → j ∼ m ⊔ m
∼max ∼+ = ∼0
∼max ∼0 = ∼0
∼max ∼- = ∼+

ext: agda


text:
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; cong)

open import Syntax
import Renaming
import Substitution

module Instantiation where

  module _ {𝕊 : Signature} where

    open Expression 𝕊
    open Substitution
    open Renaming
    open Equality

    -- the set of instantiations

    infix 5 _→ⁱ_∥_

    _→ⁱ_∥_ : MShape → MShape → VShape → Set
    𝕄 →ⁱ 𝕂 ∥ γ = ∀ {clᴹ γᴹ} (M : [ clᴹ , γᴹ ]∈ 𝕄) → Arg clᴹ 𝕂 γ γᴹ

    -- equality of instantiations

    infix 4 _≈ⁱ_

    _≈ⁱ_ : ∀ {𝕂 𝕄} {γ} (I J : 𝕂 →ⁱ 𝕄 ∥ γ) → Set
    I ≈ⁱ J = ∀ {clᴹ γᴹ} (M : [ clᴹ , γᴹ ]∈ _) → I M ≈ J M

    -- equality of instaniations is an equivalence relation

    ≈ⁱ-refl : ∀ {𝕂 𝕄} {γ} {I : 𝕂 →ⁱ 𝕄 ∥ γ} → I ≈ⁱ I
    ≈ⁱ-refl M = ≈-refl

    ≈ⁱ-sym : ∀ {𝕂 𝕄} {γ} {I J : 𝕂 →ⁱ 𝕄 ∥ γ} → I ≈ⁱ J → J ≈ⁱ I
    ≈ⁱ-sym ξ M = ≈-sym (ξ M)

    ≈ⁱ-trans : ∀ {𝕂 𝕄} {γ} {I J K : 𝕂 →ⁱ 𝕄 ∥ γ} → I ≈ⁱ J → J ≈ⁱ K → I ≈ⁱ K
    ≈ⁱ-trans ζ ξ M = ≈-trans (ζ M) (ξ M)

    -- identity instantiation

    𝟙ⁱ : ∀ {𝕄 γ} → 𝕄 →ⁱ 𝕄 ∥ γ
    𝟙ⁱ M = expr-meta-generic M

    -- instantiation extension

    ⇑ⁱ : ∀ {𝕂 𝕄 γ δ} → 𝕂 →ⁱ 𝕄 ∥ γ → 𝕂 →ⁱ 𝕄 ∥ γ ⊕ δ
    ⇑ⁱ I M = [ ⇑ʳ var-left ]ʳ (I M)

    -- extension respects equality

    ⇑ⁱ-resp-≈ⁱ : ∀ {𝕂 𝕄} {γ δ} → {I J : 𝕂 →ⁱ 𝕄 ∥ γ} → I ≈ⁱ J → ⇑ⁱ {δ = δ} I ≈ⁱ ⇑ⁱ J
    ⇑ⁱ-resp-≈ⁱ ξ M = []ʳ-resp-≈ (⇑ʳ var-left) (ξ M)

    -- the action of an instantiation on an expression

    infix 6 [_]ⁱ_

    [_]ⁱ_ : ∀ {cl 𝕂 𝕄} {γ} → (𝕂 →ⁱ 𝕄 ∥ γ) → Expr cl 𝕂 γ → Expr cl 𝕄 γ
    [ I ]ⁱ (expr-var x) = expr-var x
    [ I ]ⁱ (expr-symb S es) = expr-symb S (λ i → [ ⇑ⁱ I ]ⁱ es i)
    [ I ]ⁱ (expr-meta M ts) = [ [ 𝟙ˢ , (λ i → [ I ]ⁱ ts i) ]ˢ ]ˢ I M
    [ I ]ⁱ expr-eqty = expr-eqty
    [ I ]ⁱ expr-eqtm = expr-eqtm

    -- instantiations respects equality

    []ⁱ-resp-≈ : ∀ {cl} {𝕂 𝕄} {γ} (I : 𝕂 →ⁱ 𝕄 ∥ γ) {t u : Expr cl 𝕂 γ} → t ≈ u → [ I ]ⁱ t ≈ [ I ]ⁱ u
    []ⁱ-resp-≈ I (≈-≡ ξ) = ≈-≡ (cong [ I ]ⁱ_ ξ)
    []ⁱ-resp-≈ I (≈-symb ξ) = ≈-symb (λ i → []ⁱ-resp-≈ (⇑ⁱ I) (ξ i))
    []ⁱ-resp-≈ I (≈-meta ξ) = []ˢ-resp-≈ˢ ([,]ˢ-resp-≈ˢ ≈ˢ-refl (λ i → []ⁱ-resp-≈ I (ξ i))) (I _)

    []ⁱ-resp-≈ⁱ : ∀ {cl} {𝕂 𝕄} {γ} {I J : 𝕂 →ⁱ 𝕄 ∥ γ} (t : Expr cl 𝕂 γ) → I ≈ⁱ J → [ I ]ⁱ t ≈ [ J ]ⁱ t
    []ⁱ-resp-≈ⁱ (expr-var x) ξ = ≈-refl
    []ⁱ-resp-≈ⁱ (expr-symb S es) ξ = ≈-symb (λ i → []ⁱ-resp-≈ⁱ (es i) (⇑ⁱ-resp-≈ⁱ ξ))
    []ⁱ-resp-≈ⁱ (expr-meta M ts) ξ = []ˢ-resp-≈ˢ-≈ ([,]ˢ-resp-≈ˢ ≈ˢ-refl (λ i → []ⁱ-resp-≈ⁱ (ts i) ξ)) (ξ M)
    []ⁱ-resp-≈ⁱ expr-eqty ξ = ≈-eqty
    []ⁱ-resp-≈ⁱ expr-eqtm ξ = ≈-eqtm

    []ⁱ-resp-≈ⁱ-≈ : ∀ {cl} {𝕂 𝕄} {γ} {I J : 𝕂 →ⁱ 𝕄 ∥ γ} {t u : Expr cl 𝕂 γ} →
                    I ≈ⁱ J → t ≈ u → [ I ]ⁱ t ≈ [ J ]ⁱ u
    []ⁱ-resp-≈ⁱ-≈ {J = J} {t = t} ζ ξ = ≈-trans ([]ⁱ-resp-≈ⁱ t ζ) ([]ⁱ-resp-≈ J ξ)

    -- composition of instantiations

    infixl 7 _∘ⁱ_

    _∘ⁱ_ : ∀ {𝕂 𝕃 𝕄} {γ} → 𝕃 →ⁱ 𝕄 ∥ γ → 𝕂 →ⁱ 𝕃 ∥ γ → 𝕂 →ⁱ 𝕄 ∥ γ
    (J ∘ⁱ I) M = [ ⇑ⁱ J ]ⁱ I M

    -- composition of a renaming and instantiation

    infixr 7 _ʳ∘ⁱ_

    _ʳ∘ⁱ_ : ∀ {𝕂 𝕄} {γ δ} → (ρ : γ →ʳ δ) → (I : 𝕂 →ⁱ 𝕄 ∥ γ) → 𝕂 →ⁱ 𝕄 ∥ δ
    (ρ ʳ∘ⁱ I) M =  [ ⇑ʳ ρ ]ʳ I M

    ⇑ⁱ-resp-ʳ∘ⁱ : ∀ {𝕂 𝕄} {γ δ η} {ρ : γ →ʳ δ} → {I : 𝕂 →ⁱ 𝕄 ∥ γ} →
                  ⇑ⁱ {δ = η} (ρ ʳ∘ⁱ I) ≈ⁱ ⇑ʳ ρ ʳ∘ⁱ ⇑ⁱ I
    ⇑ⁱ-resp-ʳ∘ⁱ {I = I} M =
      ≈-trans
        (≈-trans
          (≈-sym ([∘ʳ] (I M)))
          ([]ʳ-resp-≡ʳ (I M) (λ {(var-left x) → refl ; (var-right y) → refl})))
        ([∘ʳ] (I M))

    [ʳ∘ⁱ] : ∀ {cl 𝕂 𝕄} {γ δ} {ρ : γ →ʳ δ} {I : 𝕂 →ⁱ 𝕄 ∥ γ} (t : Expr cl 𝕂 γ) →
             [ ρ ]ʳ ([ I ]ⁱ t) ≈ [ ρ ʳ∘ⁱ I ]ⁱ [ ρ ]ʳ t
    [ʳ∘ⁱ] (expr-var x) = ≈-refl
    [ʳ∘ⁱ] {ρ = ρ} {I = I} (expr-symb S es) =
      ≈-symb (λ i → ≈-trans
                     ([ʳ∘ⁱ] (es i))
                     ([]ⁱ-resp-≈ⁱ
                        ([ ⇑ʳ ρ ]ʳ es i)
                        (≈ⁱ-sym (⇑ⁱ-resp-ʳ∘ⁱ {I = I}))))
    [ʳ∘ⁱ] {ρ = ρ} {I = I} (expr-meta M ts) =
      ≈-trans
        (≈-sym ([ʳ∘ˢ] (I M)))
        (≈-trans
          ([]ˢ-resp-≈ˢ (λ { (var-left x) → ≈-refl ; (var-right y) →  [ʳ∘ⁱ] (ts y)}) (I M))
          ([ˢ∘ʳ] (I M)))
    [ʳ∘ⁱ] expr-eqty = ≈-eqty
    [ʳ∘ⁱ] expr-eqtm = ≈-eqtm

    -- composition of an instantiation and substitution

    infixr 7 _ⁱ∘ˢ_

    _ⁱ∘ˢ_ : ∀ {𝕂 𝕄} {γ δ} (I : 𝕂 →ⁱ 𝕄 ∥ δ) (σ : 𝕂 ∥ γ →ˢ δ) → (𝕄 ∥ γ →ˢ δ)
    (I ⁱ∘ˢ σ) x = [ I ]ⁱ σ x

    -- extension respects identity

    ⇑ⁱ-resp-𝟙ⁱ : ∀ {𝕄 γ δ} → ⇑ⁱ {δ = δ} 𝟙ⁱ ≈ⁱ 𝟙ⁱ {𝕄 = 𝕄} {γ = γ ⊕ δ}
    ⇑ⁱ-resp-𝟙ⁱ {clᴹ = obj _} M = ≈-refl
    ⇑ⁱ-resp-𝟙ⁱ {clᴹ = EqTy} M = ≈-eqty
    ⇑ⁱ-resp-𝟙ⁱ {clᴹ = EqTm} M = ≈-eqtm

    -- extension respects composition

    ⇑ⁱ-resp-∘ⁱ : ∀ {𝕂 𝕃 𝕄 γ δ} {I : 𝕂 →ⁱ 𝕃 ∥ γ} {J : 𝕃 →ⁱ 𝕄 ∥ γ} → ⇑ⁱ {δ = δ} (J ∘ⁱ I) ≈ⁱ ⇑ⁱ J ∘ⁱ ⇑ⁱ I
    ⇑ⁱ-resp-∘ⁱ {I = I} {J = J} M =
      ≈-trans
        ([ʳ∘ⁱ] (I M))
        ([]ⁱ-resp-≈ⁱ ([ ⇑ʳ var-left ]ʳ I M)
          λ N → ≈-trans (≈-sym ([∘ʳ] (J N)))
                  (≈-trans ([]ʳ-resp-≡ʳ (J N)  λ {(var-left x) → refl ; (var-right y) → refl}) ([∘ʳ] (J N))))

    ⇑ⁱ-resp-ⁱ∘ˢ : ∀ {𝕂 𝕄} {γ δ η} {I : 𝕂 →ⁱ 𝕄 ∥ δ} {σ : 𝕂 ∥ γ →ˢ δ} →
                  ⇑ˢ {η = η} (I ⁱ∘ˢ σ ) ≈ˢ ⇑ⁱ I ⁱ∘ˢ ⇑ˢ σ
    ⇑ⁱ-resp-ⁱ∘ˢ {σ = σ}(var-left x) = ≈-trans ([ʳ∘ⁱ] (σ x)) ([]ⁱ-resp-≈ⁱ ([ var-left ]ʳ σ x) (λ _ → ≈-refl))
    ⇑ⁱ-resp-ⁱ∘ˢ (var-right y) = ≈-refl

    -- the action of an instantiation on a generic metavariable application

    []ⁱ-meta-generic : ∀ {𝕂 𝕄} {γ} {I : 𝕂 →ⁱ 𝕄 ∥ γ} {clᴹ γᴹ} {M : [ clᴹ , γᴹ ]∈ 𝕂} → [ ⇑ⁱ I ]ⁱ (expr-meta-generic {γ = γ} M) ≈ I M
    []ⁱ-meta-generic {I = I} {clᴹ = obj _} {M = M} =
      ≈-trans (≈-sym ([ˢ∘ʳ] (I M))) ([]ˢ-id (λ { (var-left _) → ≈-refl ; (var-right _) → ≈-refl}))
    []ⁱ-meta-generic {clᴹ = EqTy} = ≈-eqty
    []ⁱ-meta-generic {clᴹ = EqTm} = ≈-eqtm

    -- action of the identity

    [𝟙ⁱ] : ∀ {cl 𝕄 γ} (t : Expr cl 𝕄 γ) → [ 𝟙ⁱ ]ⁱ t ≈ t
    [𝟙ⁱ] (expr-var x) = ≈-refl
    [𝟙ⁱ] (expr-symb S es) = ≈-symb (λ i → ≈-trans ([]ⁱ-resp-≈ⁱ (es i) ⇑ⁱ-resp-𝟙ⁱ) ([𝟙ⁱ] (es i)))
    [𝟙ⁱ] (expr-meta M ts) = ≈-meta (λ i → [𝟙ⁱ] (ts i))
    [𝟙ⁱ] (expr-eqty) = ≈-eqty
    [𝟙ⁱ] (expr-eqtm) = ≈-eqtm

    -- interaction of instantiation, substitution and renaming

    []ⁱ-[]ˢ : ∀ {cl 𝕂 𝕄 γ δ} {I : 𝕂 →ⁱ 𝕄 ∥ δ} {σ : 𝕂 ∥ γ →ˢ δ} {ρ : δ →ʳ γ} (t : Expr cl 𝕂 γ) →
          σ ˢ∘ʳ ρ ≈ˢ 𝟙ˢ → ([ I ]ⁱ ([ σ ]ˢ t)) ≈ ([ I ⁱ∘ˢ σ ]ˢ [ ρ ʳ∘ⁱ I ]ⁱ t)
    []ⁱ-[]ˢ (expr-var x) ξ = ≈-refl
    []ⁱ-[]ˢ {I = I} {σ = σ} {ρ = ρ} (expr-symb S es) ξ =
      ≈-symb (λ i →
        ≈-trans
          ([]ⁱ-[]ˢ {ρ = ⇑ʳ ρ} (es i)
            λ where
              (var-left x) → []ʳ-resp-≈ var-left (ξ x)
              (var-right x) → ≈-refl)
          (≈-sym ([]ˢ-resp-≈ˢ-≈ (⇑ⁱ-resp-ⁱ∘ˢ) (([]ⁱ-resp-≈ⁱ (es i) (⇑ⁱ-resp-ʳ∘ⁱ {I = I}))))))
    []ⁱ-[]ˢ {I = I} {σ = σ} (expr-meta M ts) ξ =
      ≈-trans
        (≈-trans
          ([]ˢ-resp-≈ˢ (λ where
                          (var-left x) → ≈-sym ([]ⁱ-resp-≈ I (ξ x))
                          (var-right x) → []ⁱ-[]ˢ (ts x) ξ)
                       (I M))
          ([∘ˢ] (I M)))
        (≈-sym ([]ˢ-resp-≈ (I ⁱ∘ˢ σ) (≈-sym ([ˢ∘ʳ] (I M))) ))
    []ⁱ-[]ˢ expr-eqty _ = ≈-eqty
    []ⁱ-[]ˢ expr-eqtm _ = ≈-eqtm

    _ˢ∘ⁱ_ : ∀ {𝕂 𝕄 γ δ} → 𝕊 % 𝕄 ∥ γ →ˢ δ → 𝕂 →ⁱ 𝕄 ∥ γ → 𝕂 →ⁱ 𝕄 ∥ δ
    (σ ˢ∘ⁱ I) M =  [ ⇑ˢ σ ]ˢ I M

    ⇑ⁱ-resp-ˢ∘ⁱ : ∀ {𝕂 𝕄 γ δ η} {σ : 𝕊 % 𝕄 ∥ γ →ˢ δ} {I : 𝕂 →ⁱ 𝕄 ∥ γ} →
                  ⇑ⁱ {δ = η} (σ ˢ∘ⁱ I) ≈ⁱ ⇑ˢ σ ˢ∘ⁱ ⇑ⁱ I
    ⇑ⁱ-resp-ˢ∘ⁱ {I = I} M =
      ≈-trans
        (≈-sym ([ʳ∘ˢ] (I M)))
        (≈-trans
           ([]ˢ-resp-≈ˢ (≈ˢ-sym ⇑ˢ-resp-ʳ∘ˢ) (I M))
           (≈-trans
              ([]ˢ-resp-≈ˢ
                 (λ { (var-left x) → ≈-refl ; (var-right y) → ≈-refl})
                 (I M))
              ([ˢ∘ʳ] (I M))))

    []ˢ-[]ⁱ : ∀ {cl 𝕂 𝕄 γ δ η} {I : 𝕂 →ⁱ 𝕄 ∥ γ} {σ : 𝕊 % 𝕄 ∥ γ →ˢ δ} {ρ : η →ʳ δ} {τ : η →ʳ γ} (t : Expr cl 𝕂 η) →
              (∀ x → σ (τ x) ≈ expr-var (ρ x)) → [ σ ]ˢ ([ I ]ⁱ ([ τ ]ʳ t)) ≈ [ σ ˢ∘ⁱ I ]ⁱ ([ ρ ]ʳ t)
    []ˢ-[]ⁱ (expr-var x) ξ = ξ x
    []ˢ-[]ⁱ {I = I} {σ = σ} {ρ = ρ} (expr-symb S es) ξ =
      ≈-symb
        (λ i →
           ≈-trans
             ([]ˢ-[]ⁱ {I = ⇑ⁱ I} {σ = ⇑ˢ σ} {ρ = ⇑ʳ ρ} (es i)
                (λ { (var-left x) → []ʳ-resp-≈ var-left (ξ x)
                   ; (var-right x) → ≈-refl}))
             ([]ⁱ-resp-≈ⁱ ([ ⇑ʳ ρ ]ʳ es i) (≈ⁱ-sym (⇑ⁱ-resp-ˢ∘ⁱ {σ = σ} {I = I}))))
    []ˢ-[]ⁱ {I = I} {σ = σ} (expr-meta M ts) ξ =
      ≈-trans
        (≈-sym ([∘ˢ] (I M)))
        (≈-trans
           ([]ˢ-resp-≈ˢ
              (λ { (var-left x) → ≈-trans (≈-sym ([𝟙ˢ] (σ x))) ([ˢ∘ʳ] (σ x))
                 ; (var-right j) → []ˢ-[]ⁱ (ts j) ξ}) (I M))
           ([∘ˢ] (I M)))
    []ˢ-[]ⁱ expr-eqty ξ = ≈-eqty
    []ˢ-[]ⁱ expr-eqtm ξ = ≈-eqtm

    -- action of composition

    [∘ⁱ] : ∀ {cl 𝕂 𝕃 𝕄 γ} {I : 𝕂 →ⁱ 𝕃 ∥ γ} {J : 𝕃 →ⁱ 𝕄 ∥ γ} (t : Expr cl 𝕂 γ) → [ J ∘ⁱ I ]ⁱ t ≈ [ J ]ⁱ [ I ]ⁱ t
    [∘ⁱ] (expr-var _) = ≈-refl
    [∘ⁱ] {I = I} {J = J} (expr-symb S es) =
      ≈-symb (λ i → ≈-trans ([]ⁱ-resp-≈ⁱ (es i) (⇑ⁱ-resp-∘ⁱ {I = I})) ([∘ⁱ] (es i)))
    [∘ⁱ] {I = I} {J = J} (expr-meta M ts) =
      ≈-sym (≈-trans
               ([]ⁱ-[]ˢ {I = J} {ρ = var-left} (I M) λ _ → ≈-refl)
               ([]ˢ-resp-≈ˢ
                 (λ { (var-left x) → ≈-refl ; (var-right x) → ≈-sym ([∘ⁱ] (ts x))})
                 ([ ⇑ⁱ J ]ⁱ (I M))))
    [∘ⁱ] expr-eqty = ≈-eqty
    [∘ⁱ] expr-eqtm = ≈-eqtm

  -- Notation for working with multiple signatures

  infix 5 _%_→ⁱ_∥_
  _%_→ⁱ_∥_ : ∀ (𝕊 : Signature) → MShape → MShape → VShape → Set
  _%_→ⁱ_∥_ 𝕊 = _→ⁱ_∥_ {𝕊 = 𝕊}


text:
-- Construction of the four functions SST, SK, SK⃗, and αₖ from
-- "Extending Homotopy Type Theory with Strict Equality" by Thorsten
-- Altenkirch, Paolo Capriotti, Nicolai Kraus (2016)
-- (https://arxiv.org/abs/1604.03799).

{-# OPTIONS --cubical-compatible --two-level --rewriting #-}

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

variable
  ℓ ℓ′ ℓ₁ ℓ₂ ℓ₃ : Level
  A B C : Set ℓ
  x y z : A

infix 4 _≡ₛ_ _≡ₛₛ_
data _≡ₛ_ {A : Set ℓ} (x : A) : A → SSet ℓ where
  instance
    refl : x ≡ₛ x

data _≡ₛₛ_ {A : SSet ℓ} (x : A) : A → SSet ℓ where
  instance
    refl : x ≡ₛₛ x

UIPₛ : {A : Set ℓ} {x y : A} {e₁ e₂ : x ≡ₛ y} → e₁ ≡ₛₛ e₂
UIPₛ {e₁ = refl} {e₂ = refl} = refl

{-# BUILTIN REWRITE _≡ₛₛ_ #-}

sym : x ≡ₛ y → y ≡ₛ x
sym refl = refl

trans : x ≡ₛ y → y ≡ₛ z → x ≡ₛ z
trans refl refl = refl

infixr 10 _≡⟨_⟩ₛ_
_≡⟨_⟩ₛ_ : {A : Set ℓ} (x : A) {y z : A} → x ≡ₛ y → y ≡ₛ z → x ≡ₛ z
x ≡⟨ refl ⟩ₛ refl = refl

infix 15 _∎ₛ
_∎ₛ : {A : Set ℓ} (x : A) → x ≡ₛ x
x ∎ₛ = refl

transport : {A : Set ℓ} (P : A → Set ℓ′) {x y : A} → x ≡ₛ y → P x → P y
transport P refl p = p

transport-merge : {A : Set ℓ} {P : A → Set ℓ′} {x y z : A}
                  {e₁ : x ≡ₛ y} {e₂ : y ≡ₛ z} {p : P x}
                → transport P e₂ (transport P e₁ p) ≡ₛ transport P (trans e₁ e₂) p
transport-merge {e₁ = refl} {e₂ = refl} = refl

transport-pi : {A : Set ℓ₁} {B : Set ℓ₂} {C : A → B → Set ℓ₃}
             → {x₁ x₂ : A} {e : x₁ ≡ₛ x₂} {f : (y : B) → C x₁ y} {y : B}
             → transport (λ x → (y : B) → C x y) e f y ≡ₛ transport (λ x → C x y) e (f y)
transport-pi {e = refl} = refl

cong : (f : A → B) {x₁ x₂ : A} → x₁ ≡ₛ x₂ → f x₁ ≡ₛ f x₂
cong f refl = refl

cong₂ : {A : Set ℓ} {B : A → Set ℓ′} (f : (x : A) → B x → C)
      → {x₁ x₂ : A} {y₁ : B x₁} {y₂ : B x₂}
      → (p : x₁ ≡ₛ x₂) (q : transport B p y₁ ≡ₛ y₂)
      → f x₁ y₁ ≡ₛ f x₂ y₂
cong₂ f refl refl = refl

transport-cong : {f : A → B} {P : B → Set ℓ} {x₁ x₂ : A} {e : x₁ ≡ₛ x₂} {p : P (f x₁)}
               → transport (λ x → P (f x)) e p ≡ₛ transport P (cong f e) p
transport-cong {e = refl} = refl

cong-transport : {A : Set ℓ} {P : A → Set ℓ′} {x y : A} {e₁ e₂ : x ≡ₛ y} {p : P x}
               → e₁ ≡ₛₛ e₂ → transport P e₁ p ≡ₛ transport P e₂ p
cong-transport refl = refl

postulate
  funextₛ : {A : Set ℓ} {B : A → Set ℓ′} {f g : (x : A) → B x}
          → (∀ x → f x ≡ₛ g x) → f ≡ₛ g

data sNat : SSet lzero where
  zero : sNat
  suc  : sNat → sNat

variable
  k l m n : sNat

postulate
  Nat→sNat : Nat → sNat
  zero→szero : Nat→sNat zero ≡ₛₛ zero
  suc→ssuc : ∀ n → Nat→sNat (suc n) ≡ₛₛ suc (Nat→sNat n)

{-# REWRITE zero→szero #-}
{-# REWRITE suc→ssuc #-}

data ⊥ {ℓ} : Set ℓ where

record ⊤ {ℓ} : Set ℓ where
  constructor ∗

data _⊎_ (A B : Set ℓ) : Set ℓ where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

{-# NO_UNIVERSE_CHECK #-}
data Fin : sNat → Set where
  fzero : Fin (suc n)
  fsuc  : Fin n → Fin (suc n)

{-# NO_UNIVERSE_CHECK #-}
data _<ⁿ_ : Fin n → Fin n → Set where
  z<s : fzero <ⁿ fsuc x
  s<s : x <ⁿ y → fsuc x <ⁿ fsuc y

isIncr : (Fin k → Fin l) → Set
isIncr f = ∀ {x} {y} → x <ⁿ y → f x <ⁿ f y

Δ₊ : (i j : sNat) → Set
Δ₊ i j = Σ (Fin i → Fin j) isIncr

_∘_ : Δ₊ l m → Δ₊ k l → Δ₊ k m
(f , f-incr) ∘ (g , g-incr) = (λ x → f (g x)) , λ p → f-incr (g-incr p)

∘-assoc : ∀ {k l m n} {f : Δ₊ k l} {g : Δ₊ l m} {h : Δ₊ m n}
        → (h ∘ g) ∘ f ≡ₛ h ∘ (g ∘ f)
∘-assoc = refl

SST : sNat → Set₁
SK : (k : sNat) → SST k → sNat → Set
SK⃗ : (k : sNat) (X : SST k) {m n : sNat} (f : Δ₊ m n) → SK k X n → SK k X m
α : (k : sNat) {l m n : sNat} (X : SST k) (f : Δ₊ l m) (g : Δ₊ m n)
  → (x : SK k X n) → SK⃗ k X (g ∘ f) x ≡ₛ SK⃗ k X f (SK⃗ k X g x)

SST zero = ⊤
SST (suc k) = Σ (SST k) λ X → (SK k X (suc k) → Set)

SK zero X n = ⊤
SK (suc k) (X , Y) n = Σ (SK k X n) λ x → (f : Δ₊ (suc k) n) → Y (SK⃗ k X f x)

SK⃗ zero X f = λ x → x
SK⃗ (suc k) (X , Y) f (x , h) = SK⃗ k X f x , λ g →
  let h[f∘g] : Y (SK⃗ k X (f ∘ g) x)
      h[f∘g] = h (f ∘ g)
      αₖ : SK⃗ k X (f ∘ g) x ≡ₛ SK⃗ k X g (SK⃗ k X f x)
      αₖ = α k X g f x
  in transport Y αₖ h[f∘g]

α zero X f g x    = refl
α (suc k) {l} {m} {n} (X , Y) f g (x , y) =
  cong₂ _,_ (α k X f g x) (funextₛ λ h →

    transport (λ z → (f′ : Δ₊ (suc k) l) → Y (SK⃗ k X f′ z)) (α k X f g x)
      (λ g′ → transport Y (α k X g′ (g ∘ f) x) (y ((g ∘ f) ∘ g′))) h

      ≡⟨ transport-pi {B = Δ₊ (suc k) l} {C = λ z f′ → Y (SK⃗ k X f′ z)} {e = α k X f g x} ⟩ₛ

    transport (λ z → Y (SK⃗ k X h z)) (α k X f g x)
      (transport Y (α k X h (g ∘ f) x) (y ((g ∘ f) ∘ h)))

      ≡⟨ transport-cong {f = SK⃗ k X h} {P = Y} {e = α k X f g x} ⟩ₛ

    transport Y (cong (SK⃗ k X h) (α k X f g x))
      (transport Y (α k X h (g ∘ f) x) (y ((g ∘ f) ∘ h)))

      ≡⟨ transport-merge {P = Y} {e₂ = cong (SK⃗ k X h) (α k X f g x)} {p = y ((g ∘ f) ∘ h)} ⟩ₛ

    transport Y (trans (α k X h (g ∘ f) x) (cong (SK⃗ k X h) (α k X f g x))) (y ((g ∘ f) ∘ h))

      ≡⟨ cong-transport {P = Y}
           {e₁ = trans (α k X h (g ∘ f) x) (cong (SK⃗ k X h) (α k X f g x))}
           {e₂ = trans (α k X (f ∘ h) g x) (α k X h f (SK⃗ k X g x))}
           {p = y (g ∘ (f ∘ h))} UIPₛ ⟩ₛ

    transport Y (trans (α k X (f ∘ h) g x) (α k X h f (SK⃗ k X g x))) (y (g ∘ (f ∘ h)))

      ≡⟨ sym (transport-merge {e₁ = α k X (f ∘ h) g x} {e₂ = α k X h f (SK⃗ k X g x)} {p = y (g ∘ (f ∘ h))}) ⟩ₛ

    transport Y (α k X h f (SK⃗ k X g x)) (transport Y (α k X (f ∘ h) g x) (y (g ∘ (f ∘ h))))
      ∎ₛ

  )


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst)

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.VRenaming
import SecondOrder.MRenaming
import SecondOrder.Term
import SecondOrder.Substitution
import SecondOrder.RelativeMonadMorphism

module SecondOrder.Instantiation
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ
  open SecondOrder.VRenaming Σ
  open SecondOrder.MRenaming Σ
  open SecondOrder.Substitution Σ
  open import SecondOrder.RelativeMonadMorphism

  -- metavariable instantiation

  _⇒ⁱ_⊕_ : MContext → MContext → VContext → Set ℓ
  Θ ⇒ⁱ Ξ ⊕ Γ = ∀ {Γᴹ Aᴹ} (M : [ Γᴹ , Aᴹ ]∈ Θ) → Term Ξ (Γ ,, Γᴹ) Aᴹ

  -- syntactic equality of instantiations

  infix 5 _≈ⁱ_

  _≈ⁱ_ : ∀ {Θ Ψ Γ} (I J : Θ ⇒ⁱ Ψ ⊕ Γ) → Set ℓ
  _≈ⁱ_ {Θ} I J = ∀ {Γᴹ Aᴹ} (M : [ Γᴹ , Aᴹ ]∈ Θ) → I M ≈ J M

  -- equality of instantiations is an equivalence relation

  ≈ⁱ-refl : ∀ {Θ Ψ Γ} {I : Θ ⇒ⁱ Ψ ⊕ Γ} → I ≈ⁱ I
  ≈ⁱ-refl M = ≈-refl

  ≈ⁱ-sym : ∀ {Θ Ψ Γ} {I J : Θ ⇒ⁱ Ψ ⊕ Γ} → I ≈ⁱ J → J ≈ⁱ I
  ≈ⁱ-sym ξ M = ≈-sym (ξ M)

  ≈ⁱ-trans : ∀ {Θ Ψ Γ} {I J K : Θ ⇒ⁱ Ψ ⊕ Γ} → I ≈ⁱ J → J ≈ⁱ K → I ≈ⁱ K
  ≈ⁱ-trans ζ ξ M = ≈-trans (ζ M) (ξ M)

  -- extension of an instantiation

  ⇑ⁱ : ∀ {Θ Ψ Γ Δ} → Θ ⇒ⁱ Ψ ⊕ Γ → Θ ⇒ⁱ Ψ ⊕ (Γ ,, Δ)
  ⇑ⁱ I M =  [ ⇑ᵛ var-inl ]ᵛ I M

  -- extension of instantiations preserve equality of instantiations

  ⇑ⁱ-resp-≈ⁱ : ∀ {Θ Ψ Γ Δ} (I J : Θ ⇒ⁱ Ψ ⊕ Γ) → (I ≈ⁱ J) → (⇑ⁱ {Δ = Δ} I ≈ⁱ ⇑ⁱ J)
  ⇑ⁱ-resp-≈ⁱ I J ξ M = []ᵛ-resp-≈ (ξ M)

  -- action of a metavariable instantiation on terms

  infixr 6 [_]ⁱ_

  [_]ⁱ_ : ∀ {Θ ψ Γ} → ψ ⇒ⁱ Θ ⊕ Γ → ∀ {A} → Term ψ Γ A → Term Θ Γ A
  [ I ]ⁱ (tm-var x) = tm-var x
  [ I ]ⁱ (tm-meta M ts) = [ [ idˢ , (λ i → [ I ]ⁱ ts i) ]ˢ ]ˢ (I M)
  [ I ]ⁱ (tm-oper f es) = tm-oper f λ i → [ ⇑ⁱ I ]ⁱ es i

  -- instantiation preserves equality of terms

  []ⁱ-resp-≈ : ∀ {Θ Ξ Γ} (I : Ξ ⇒ⁱ Θ ⊕ Γ) → ∀ {A} {t u : Term Ξ Γ A} →
               t ≈ u → [ I ]ⁱ t ≈ [ I ]ⁱ u
  []ⁱ-resp-≈ I (≈-≡ refl) = ≈-refl
  []ⁱ-resp-≈ I (≈-meta {M = M} ξ) = []ˢ-resp-≈ˢ (I M) ([,]ˢ-resp-≈ˢ (λ x → ≈-refl) λ i → []ⁱ-resp-≈ I (ξ i))
  []ⁱ-resp-≈ I (≈-oper ξ) = ≈-oper λ i → []ⁱ-resp-≈ (⇑ⁱ I) (ξ i)

  -- action preserves equality of instantiation

  []ⁱ-resp-≈ⁱ : ∀ {Θ Ξ Γ} {I J : Ξ ⇒ⁱ Θ ⊕ Γ} → ∀ {A} (t : Term Ξ Γ A) →
               I ≈ⁱ J → [ I ]ⁱ t ≈ [ J ]ⁱ t
  []ⁱ-resp-≈ⁱ (tm-var x) ξ = ≈-refl
  []ⁱ-resp-≈ⁱ (tm-meta M ts) ξ =
    []ˢ-resp-≈ˢ-≈ ([,]ˢ-resp-≈ˢ (λ x → ≈-refl) λ i → []ⁱ-resp-≈ⁱ (ts i) ξ) (ξ M)
  []ⁱ-resp-≈ⁱ {I = I} {J = J} (tm-oper f es) ξ = ≈-oper λ i → []ⁱ-resp-≈ⁱ (es i) (⇑ⁱ-resp-≈ⁱ I J ξ)

  -- generically applied metavariable

  tm-meta-generic : ∀ {Θ} {Γ} {Γᴹ Aᴹ} (M : [ Γᴹ , Aᴹ ]∈ Θ) → Term Θ (Γ ,, Γᴹ) Aᴹ
  tm-meta-generic M = tm-meta M λ i → tm-var (var-inr i)

  -- the action of an instantiation on a generically applied metavariable

  []ⁱ-generic : ∀ {Θ Ξ} {Γ} {I : Θ ⇒ⁱ Ξ ⊕ Γ} {Γᴹ Aᴹ} {M : [ Γᴹ , Aᴹ ]∈ Θ} →
                [ ⇑ⁱ {Δ = Γᴹ} I ]ⁱ tm-meta-generic M ≈ I M
  []ⁱ-generic {Θ = Θ} {Ξ = Ξ} {Γ = Γ} {I = I} {Γᴹ = Γᴹ} {M = M} =
    ≈-trans
      (≈-sym ([ˢ∘ᵛ] (I M)))
      (≈ˢ-idˢ-[]ˢ (λ { (var-inl _) → ≈-refl ; (var-inr _) → ≈-refl}))

  -- Interactions involving instantiations

  -- the identity metavariable instantiation

  idⁱ : ∀ {Θ Γ} → Θ ⇒ⁱ Θ ⊕ Γ
  idⁱ M = tm-meta-generic M

  -- composition of metavariable instantiations

  infixl 6 _∘ⁱ_

  _∘ⁱ_ : ∀ {Θ Ξ Ω Γ} → Ξ ⇒ⁱ Ω ⊕ Γ → Θ ⇒ⁱ Ξ ⊕ Γ → (Θ ⇒ⁱ Ω ⊕ Γ)
  (I ∘ⁱ J) M =  [ ⇑ⁱ I ]ⁱ J M

  -- composition of a renaming and an instantiation

  _ᵛ∘ⁱ_ : ∀ {Θ ψ Γ Δ} → Γ ⇒ᵛ Δ → Θ ⇒ⁱ ψ ⊕ Γ → Θ ⇒ⁱ ψ ⊕ Δ
  (ρ ᵛ∘ⁱ I) M = [ ⇑ᵛ ρ ]ᵛ I M

  -- composition of a substitution and an instantiation

  _ˢ∘ⁱ_ : ∀ {Θ ψ Γ Δ} → ψ ⊕ Γ ⇒ˢ Δ → Θ ⇒ⁱ ψ ⊕ Γ → Θ ⇒ⁱ ψ ⊕ Δ
  (σ ˢ∘ⁱ I) M = [ ⇑ˢ σ ]ˢ I M

  -- composition of an instantiation and a substitution

  _ⁱ∘ˢ_ : ∀ {Θ ψ Γ Δ} → Θ ⇒ⁱ ψ ⊕ Δ → Θ ⊕ Γ ⇒ˢ Δ →  ψ ⊕ Γ ⇒ˢ Δ
  (I ⁱ∘ˢ σ) x = [ I ]ⁱ σ x

  -- composition of a renaming and an instantiation preerve equality of instantiations

  [ᵛ∘ⁱ]-resp-≈ⁱ : ∀ {Θ ψ Γ Δ} (ρ : Γ ⇒ᵛ Δ) (I J : Θ ⇒ⁱ ψ ⊕ Γ) → (I ≈ⁱ J) → (ρ ᵛ∘ⁱ I) ≈ⁱ (ρ ᵛ∘ⁱ J)
  [ᵛ∘ⁱ]-resp-≈ⁱ σ I J ξ M = []ᵛ-resp-≈ (ξ M)

  -- composition of a renaming and an instantiation preserve equality of instantiations

  [ˢ∘ⁱ]-resp-≈ⁱ : ∀ {Θ ψ Γ Δ} (σ : ψ ⊕ Γ ⇒ˢ Δ) (I J : Θ ⇒ⁱ ψ ⊕ Γ) → (I ≈ⁱ J) → (σ ˢ∘ⁱ I) ≈ⁱ (σ ˢ∘ⁱ J)
  [ˢ∘ⁱ]-resp-≈ⁱ σ I J ξ M = []ˢ-resp-≈ (⇑ˢ σ) (ξ M)

  -- Actions correspondig to the interactions

  -- the action of the identity

  [idⁱ] : ∀ {Θ Γ A Δ} {t : Term Θ (Γ ,, Δ) A}  → [ idⁱ ]ⁱ t ≈ t
  [idⁱ] {t = tm-var x} = ≈-refl
  [idⁱ] {t = tm-meta M ts} = ≈-meta (λ i → [idⁱ])
  [idⁱ] {t = tm-oper f es} = ≈-oper (λ i → [idⁱ])

  -- extension commutes with composition of renaming and substitution

  ⇑ⁱ-resp-ᵛ∘ⁱ : ∀ {Θ ψ} {Γ Δ Ξ} {I : Θ ⇒ⁱ ψ ⊕ Γ} {ρ : Γ ⇒ᵛ Δ}
               → ⇑ⁱ {Δ = Ξ} (ρ ᵛ∘ⁱ I) ≈ⁱ ⇑ᵛ ρ ᵛ∘ⁱ ⇑ⁱ I
  ⇑ⁱ-resp-ᵛ∘ⁱ {ρ = ρ} M = ≈-trans (≈-sym [∘ᵛ]) (≈-trans ([]ᵛ-resp-≡ᵛ λ {(var-inl _) → refl ; (var-inr x) → refl}) [∘ᵛ])

  -- the action of the composition of an instantiation and a renaming

  [ᵛ∘ⁱ] : ∀ {Θ Ψ Γ Δ A} {ρ : Γ ⇒ᵛ Δ} {I : Θ ⇒ⁱ Ψ ⊕ Γ} (t : Term Θ Γ A) →
           [ ρ ]ᵛ [ I ]ⁱ t ≈ [ ρ ᵛ∘ⁱ I ]ⁱ [ ρ ]ᵛ t
  [ᵛ∘ⁱ] (tm-var x) = ≈-refl
  [ᵛ∘ⁱ] {I = I} (tm-meta M ts) =
    ≈-trans
     (≈-sym ([ᵛ∘ˢ] (I M)))
     (≈-trans
       ([]ˢ-resp-≈ˢ (I M) (λ { (var-inl _) → ≈-refl ; (var-inr j) → [ᵛ∘ⁱ] (ts j)}))
       ([ˢ∘ᵛ] (I M)))
  [ᵛ∘ⁱ] {ρ = ρ} {I = I} (tm-oper f es) =
    ≈-oper λ i → ≈-trans ([ᵛ∘ⁱ] (es i)) ([]ⁱ-resp-≈ⁱ ([ ⇑ᵛ ρ ]ᵛ es i) (≈ⁱ-sym (⇑ⁱ-resp-ᵛ∘ⁱ {I = I})))

  -- extension commutes with composition

  ⇑ⁱ-resp-∘ⁱ : ∀ {Θ Ξ Ω} {Γ Δ} {I : Θ ⇒ⁱ Ξ ⊕ Γ} {J : Ξ ⇒ⁱ Ω ⊕ Γ} →
               ⇑ⁱ {Δ = Δ} (J ∘ⁱ I) ≈ⁱ ⇑ⁱ J ∘ⁱ ⇑ⁱ I
  ⇑ⁱ-resp-∘ⁱ {I = I} {J = J} M =
    ≈-trans
     ([ᵛ∘ⁱ] (I M))
     ([]ⁱ-resp-≈ⁱ
        ([ ⇑ᵛ var-inl ]ᵛ I M)
        (λ N → ≈-trans
                 (≈-sym [∘ᵛ])
                 (≈-trans
                   ([]ᵛ-resp-≡ᵛ (λ { (var-inl x) → refl ; (var-inr x) → refl }))
                   [∘ᵛ])))

  ⇑ˢ-resp-ⁱ∘ˢ : ∀ {Θ ψ Γ Δ Ξ} → {I : Θ ⇒ⁱ ψ ⊕ Δ} → {σ : Θ ⊕ Γ ⇒ˢ Δ} → ⇑ˢ {Ξ = Ξ} (I ⁱ∘ˢ σ) ≈ˢ ⇑ⁱ I ⁱ∘ˢ ⇑ˢ σ
  ⇑ˢ-resp-ⁱ∘ˢ {σ = σ} (var-inl x) = [ᵛ∘ⁱ] (σ x)
  ⇑ˢ-resp-ⁱ∘ˢ (var-inr x) = ≈-refl

  -- interaction lemma
  []ⁱ-[]ˢ : ∀ {Θ Ψ Γ Δ A} {I : Θ ⇒ⁱ Ψ ⊕ Δ} {σ : Θ ⊕ Γ ⇒ˢ Δ} {ρ : Δ ⇒ᵛ Γ} (t : Term Θ Γ A) →
        σ ˢ∘ᵛ ρ ≈ˢ idˢ → ([ I ]ⁱ ([ σ ]ˢ t)) ≈ ([ I ⁱ∘ˢ σ ]ˢ [ ρ ᵛ∘ⁱ I ]ⁱ t)
  []ⁱ-[]ˢ (tm-var x) ξ = ≈-refl
  []ⁱ-[]ˢ {I = I} {σ = σ} {ρ = ρ} (tm-meta M ts) ξ =
   ≈-trans
     ([]ˢ-resp-≈ˢ (I M)
        (λ { (var-inl i) → []ⁱ-resp-≈ I (≈-sym (ξ i)) ; (var-inr j) → []ⁱ-[]ˢ (ts j) ξ}))
     (≈-trans
       ([ˢ∘ᵛ] (I M))
       ([∘ˢ] ((ρ ᵛ∘ⁱ I) M)))
  []ⁱ-[]ˢ {I = I} {σ = σ} {ρ = ρ} (tm-oper f es) ξ =
    ≈-oper λ i →
      ≈-trans
       ([]ⁱ-[]ˢ {σ = ⇑ˢ σ} {ρ = ⇑ᵛ ρ} (es i)
         (≈ˢ-trans
           (≈ˢ-sym (⇑ˢ-resp-ˢ∘ᵛ  {ρ = ρ} {σ = σ}))
           (≈ˢ-trans (⇑ˢ-resp-≈ˢ ξ) ⇑ˢ-resp-idˢ)))
       ([]ˢ-resp-≈ˢ-≈
          {σ = ⇑ⁱ I ⁱ∘ˢ ⇑ˢ σ }
          {τ = ⇑ˢ (I ⁱ∘ˢ σ)}
          {t = ([ ⇑ᵛ ρ ᵛ∘ⁱ ⇑ⁱ I ]ⁱ es i)}
          {u = ([ ⇑ⁱ (ρ ᵛ∘ⁱ I) ]ⁱ es i)}
          (≈ˢ-sym ⇑ˢ-resp-ⁱ∘ˢ)
          ([]ⁱ-resp-≈ⁱ (es i) (≈ⁱ-sym (⇑ⁱ-resp-ᵛ∘ⁱ {I = I}))))

  -- the action of a composition

  [∘ⁱ] : ∀ {Θ Ξ Ω Γ} → {I : Θ ⇒ⁱ Ξ ⊕ Γ} → {J : Ξ ⇒ⁱ Ω ⊕ Γ} →
           ∀ {A} → ∀ (t : Term Θ Γ A) → [ J ∘ⁱ I ]ⁱ t ≈ [ J ]ⁱ [ I ]ⁱ t
  [∘ⁱ] (tm-var x) = ≈-refl
  [∘ⁱ] {Θ = Θ} {Ξ = Ξ} {Γ = Γ} {I = I} {J = J} (tm-meta {Γᴹ = Γᴹ} M ts) =
    ≈-trans
      ([]ˢ-resp-≈ˢ
        ([ ⇑ⁱ J ]ⁱ (I M))
        ([,]ˢ-resp-≈ˢ (λ x → ≈-refl) (λ i → [∘ⁱ] {I = I} {J = J} (ts i))))
      (≈-trans
        ([]ˢ-resp-≈ˢ {τ = λ i → [ J ]ⁱ var-or-ts i} ([ ⇑ⁱ J ]ⁱ (I M))
        λ {(var-inl x) → ≈-refl ; (var-inr y) → ≈-refl})
        (≈-trans
           (≈-sym ([]ⁱ-[]ˢ {I = J} {σ = var-or-ts} {ρ = var-inl} (I M) λ x → ≈-refl))
            ([]ⁱ-resp-≈ J
                       ([]ˢ-resp-≈ˢ (I M) λ { (var-inl x) → ≈-refl ; (var-inr x) → ≈-refl}))))
                 where
                 var-or-ts : ∀ {A} → A ∈ (Γ ,, Γᴹ) → Term Ξ Γ A
                 var-or-ts (var-inl x) = tm-var x
                 var-or-ts (var-inr y) = [ I ]ⁱ ts y

  [∘ⁱ] {I = I} {J = J} (tm-oper f es) =
            ≈-oper (λ i → ≈-trans ([]ⁱ-resp-≈ⁱ (es i) (⇑ⁱ-resp-∘ⁱ {I = I})) ([∘ⁱ] (es i)))

max_stars_repo_name: andrejbauer/formal

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
-- Example by Sandro Stucki on the Agda mailing list.

-- If higher-dimensional unification fails and --without-K is not
-- enabled, we should still apply injectivity.

open import Agda.Builtin.Nat

postulate Fin : Nat → Set

data Indexed : Nat → Nat → Set where
  con : ∀ m {n} (i : Fin n) → Indexed (m + n) (m + suc n)

data RelIndexed : ∀ {m n} → Indexed m n → Indexed m n → Set where
  relIdx : ∀ {m n} (i : Fin n) (j : Fin n) → RelIndexed (con m i) (con m j)

test1 : ∀ {m n} {a b : Indexed m n} → RelIndexed a b → Indexed m n
test1 (relIdx {m} i _) = con m i

test2 : ∀ {m n} {a : Indexed m n} → RelIndexed a a → Indexed m n
test2 (relIdx {m} i _) = con m i

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of Maybe
------------------------------------------------------------------------

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

module Data.Maybe.Categorical where

open import Data.Maybe.Base
open import Category.Functor
open import Category.Applicative
open import Category.Monad
import Function.Identity.Categorical as Id
open import Function

------------------------------------------------------------------------
-- Maybe applicative functor

functor : ∀ {f} → RawFunctor {f} Maybe
functor = record
  { _<$>_ = map
  }

applicative : ∀ {f} → RawApplicative {f} Maybe
applicative = record
  { pure = just
  ; _⊛_  = maybe map (const nothing)
  }

applicativeZero : ∀ {f} → RawApplicativeZero {f} Maybe
applicativeZero = record
  { applicative = applicative
  ; ∅           = nothing
  }

alternative : ∀ {f} → RawAlternative {f} Maybe
alternative = record
  { applicativeZero = applicativeZero
  ; _∣_             = _<∣>_
  }

------------------------------------------------------------------------
-- Maybe monad transformer

monadT : ∀ {f} → RawMonadT {f} (_∘′ Maybe)
monadT M = record
  { return = M.return ∘ just
  ; _>>=_  = λ m f → m M.>>= maybe f (M.return nothing)
  }
  where module M = RawMonad M

------------------------------------------------------------------------
-- Maybe monad

monad : ∀ {f} → RawMonad {f} Maybe
monad = monadT Id.monad

monadZero : ∀ {f} → RawMonadZero {f} Maybe
monadZero = record
  { monad           = monad
  ; applicativeZero = applicativeZero
  }

monadPlus : ∀ {f} → RawMonadPlus {f} Maybe
monadPlus {f} = record
  { monad       = monad
  ; alternative = alternative
  }

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {f F} (App : RawApplicative {f} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → Maybe (F A) → F (Maybe A)
  sequenceA nothing  = pure nothing
  sequenceA (just x) = just <$> x

  mapA : ∀ {a} {A : Set a} {B} → (A → F B) → Maybe A → F (Maybe B)
  mapA f = sequenceA ∘ map f

  forA : ∀ {a} {A : Set a} {B} → Maybe A → (A → F B) → F (Maybe B)
  forA = flip mapA

module _ {m M} (Mon : RawMonad {m} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM = sequenceA App
  mapM = mapA App
  forM = forA App


text:
module _ where

record ⊤ : Set where
  constructor tt

f : {{u : ⊤}} → ⊤
f = _

foo : (x : ⊤) → ⊤
foo x = f

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
postulate
  A : Set
  P : A → Set

record ΣAP : Set where
  no-eta-equality
  field
    fst : A
    snd : P fst
open ΣAP

test : (x : ΣAP) → P (fst x)
test x = snd {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.Unit where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv

open import Cubical.Data.Unit

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.DirProd
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.GroupPath

open GroupStr
open IsGroupHom

private
  variable
    ℓ : Level

UnitGroup₀ : Group₀
fst UnitGroup₀ = Unit
1g (snd UnitGroup₀) = tt
_·_ (snd UnitGroup₀) = λ _ _ → tt
inv (snd UnitGroup₀) = λ _ → tt
isGroup (snd UnitGroup₀) =
  makeIsGroup isSetUnit (λ _ _ _ → refl) (λ _ → refl) (λ _ → refl)
                        (λ _ → refl) (λ _ → refl)

UnitGroup : Group ℓ
fst UnitGroup = Unit*
1g (snd UnitGroup) = tt*
_·_ (snd UnitGroup) = λ _ _ → tt*
inv (snd UnitGroup) = λ _ → tt*
isGroup (snd UnitGroup) =
  makeIsGroup (isOfHLevelUnit* 2)
              (λ _ _ _ → refl) (λ _ → refl) (λ _ → refl)
              (λ _ → refl) (λ _ → refl)

open Iso

-- The trivial group is a unit.
lUnitGroupIso : {G : Group ℓ} → GroupIso (DirProd UnitGroup₀ G) G
fun (fst lUnitGroupIso) = snd
inv (fst lUnitGroupIso) g = tt , g
rightInv (fst lUnitGroupIso) _ = refl
leftInv (fst lUnitGroupIso) _ = refl
snd lUnitGroupIso = makeIsGroupHom λ _ _ → refl

rUnitGroupIso : {G : Group ℓ} → GroupIso (DirProd G UnitGroup₀) G
fun (fst rUnitGroupIso) = fst
inv (fst rUnitGroupIso) g = g , tt
rightInv (fst rUnitGroupIso) _ = refl
leftInv (fst rUnitGroupIso) _ = refl
snd rUnitGroupIso = makeIsGroupHom λ _ _ → refl

lUnitGroupEquiv : {G : Group ℓ} → GroupEquiv (DirProd UnitGroup₀ G) G
lUnitGroupEquiv = GroupIso→GroupEquiv lUnitGroupIso

rUnitGroupEquiv : ∀ {ℓ} {G : Group ℓ} → GroupEquiv (DirProd G UnitGroup₀) G
rUnitGroupEquiv = GroupIso→GroupEquiv rUnitGroupIso

contrGroupIsoUnit : {G : Group ℓ} → isContr ⟨ G ⟩ → GroupIso G UnitGroup₀
fun (fst (contrGroupIsoUnit contr)) _ = tt
inv (fst (contrGroupIsoUnit contr)) _ = fst contr
rightInv (fst (contrGroupIsoUnit contr)) _ = refl
leftInv (fst (contrGroupIsoUnit contr)) x = snd contr x
snd (contrGroupIsoUnit contr) = makeIsGroupHom λ _ _ → refl

contrGroupEquivUnit : {G : Group ℓ} → isContr ⟨ G ⟩ → GroupEquiv G UnitGroup₀
contrGroupEquivUnit contr = GroupIso→GroupEquiv (contrGroupIsoUnit contr)

isContr→≡UnitGroup : {G : Group ℓ-zero} → isContr (fst G) → UnitGroup₀ ≡ G
isContr→≡UnitGroup c =
  fst (GroupPath _ _)
    (invGroupEquiv ((isContr→≃Unit c)
                  , (makeIsGroupHom (λ _ _ → refl))))

GroupIsoUnitGroup→isContr : {G : Group ℓ-zero}
                           → GroupIso UnitGroup₀ G → isContr (fst G)
GroupIsoUnitGroup→isContr is =
  isOfHLevelRetractFromIso 0 (invIso (fst is)) isContrUnit

→UnitHom : ∀ {ℓ} (G : Group ℓ) → GroupHom G UnitGroup₀
fst (→UnitHom G) _ = tt
snd (→UnitHom G) = makeIsGroupHom λ _ _ → refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Reported by matteo.acerbi, AIMXX, 2014-10-21

-- The following is accepted.

{-# OPTIONS --guardedness #-}
{-# OPTIONS --cubical-compatible  #-}

-- {-# OPTIONS -v term:30 #-}

record X : Set where
  coinductive
  constructor ↑_
  field       ↓_ : X
open X

record Y (x1 x2 : X) : Set where
  coinductive
  field       ]_[ : Y (↑ x1) (↑ x2)
open Y

trivial-Y : ∀ {x1 x2} → Y x1 x2
] trivial-Y [ = trivial-Y

-- Should termination check.


text:
module _ where

open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

record Id (A : Set) : Set where
  field id : A → A

open Id {{...}}

postulate
  T    : {A : Set} → A → Set
  cong : ∀ {A B : Set} (f : A → B) {x} → T x → T (f x)

  X : Set
  lem  : (x : X) → T x

instance
  IdX : Id X
  IdX .id n = n

macro
  follows-from : Term → Term → TC ⊤
  follows-from prf hole = do
    typeError (termErr prf ∷ [])

loops : (x : X) → T x
loops x =
  follows-from (cong id (lem x))


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

module Base where

open import Agda.Primitive public using (lzero)
  renaming (Level to ULevel; lsuc to lsucc; _⊔_ to lmax)

Type : (i : ULevel) → Set (lsucc i)
Type i = Set i

Type₀ = Type lzero
Type0 = Type lzero

Type₁ = Type (lsucc lzero)
Type1 = Type (lsucc lzero)

{- Naturals -}

data ℕ : Type₀ where
  O : ℕ
  S : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}

Nat = ℕ

infix 3 _==_

data _==_ {i} {A : Type i} (a : A) : A → Type i where
  idp : a == a

Path = _==_

{-# BUILTIN EQUALITY _==_ #-}
{-# BUILTIN REFL  idp #-}

{- Free path induction, or as close as I could get, written in Section 1.12.1 as

ind=A : ∏ ∏(x:A)C(x,x,reflx) → ∏ ∏ C(x,y,p) (C:∏(x,y:A)(x=Ay)→U) (x,y:A) (p:x=Ay)
ind=A (C, c, x, x, reflx) :≡ c(x)
-}
ind== : ∀ {i j} {A : Type i} (D : (x y : A) → x == y → Type j) (d : (x : A) → D x x idp)
  {x y : A} (p : x == y) → D x y p
ind== D d {x} idp = d x -- slight concern: what rules govern the implicit {x} and {y}
                        -- converging on the single {x} parameter here?  I don't know Agda
                        -- well enough to answer this yet.  Depending upon what
                        -- they are, this rule may be a duplicate of one of the based
                        -- path induction rules below.

{- Based path induction, or the J rule in HoTT-Agda lib -}
ind=' : ∀ {i j} {A : Type i} {a : A} (D : (x : A) (p : a == x) → Type j) (d : D a idp)
  {x : A} (p : a == x) → D x p
ind=' D d idp = d

{- Right-based path induction, or J' in the HoTT-Agda lib -}
ind'= : ∀ {i j} {A : Type i} {a : A} (D : (x : A) (p : x == a) → Type j) (d : D a idp)
  {x : A} (p : x == a) → D x p
ind'= D d idp = d

ind==2 : ∀ {i j} {A : Type i} (D : {x y : A} → x == y → Type j) (d : {x : A} → D {x} {x} idp)
  {x y : A} (p : x == y) → D p
ind==2 D d idp = d -- slight concern: what rules govern the implicit {x} and {y}

-- {- Alternative based path induction as a specialized free path induction -}
-- ind='2 : ∀ {i j} {A : Type i} {a : A} (D : {x : A} (p : a == x) → Type j) (d : D idp)
--   {x : A} (p : a == x) → D p
-- ind='2 D d = ind==2 {!!} {!!}

-- Christine Paulin-Mohring’s version of the J rule is based path induction ind='
J : ∀ {i j} {A : Type i} {a : A} (D : {x : A} → a == x → Type j) → D idp →
  {x : A} (p : a == x) → D p
J D d idp = d

{- Unit type

The unit type is defined as record so that we also get the η-rule definitionally.
-}

record Unit : Type₀ where
  constructor unit

{- Dependent paths

The notion of dependent path is a very important notion.
If you have a dependent type [B] over [A], a path [p : x == y] in [A] and two
points [u : B x] and [v : B y], there is a type [u == v [ B ↓ p ]] of paths from
[u] to [v] lying over the path [p].
By definition, if [p] is a constant path, then [u == v [ B ↓ p ]] is just an
ordinary path in the fiber.
-}

PathOver : ∀ {i j} {A : Type i} (B : A → Type j)
  {x y : A} (p : x == y) (u : B x) (v : B y) → Type j
PathOver B idp u v = (u == v)

syntax PathOver B p u v =
  u == v [ B ↓ p ]

{- Ap, coe and transport

Given two fibrations over a type [A], a fiberwise map between the two fibrations
can be applied to any dependent path in the first fibration ([ap↓]).
As a special case, when [A] is [Unit], we find the familiar [ap] ([ap] is
defined in terms of [ap↓] because it shouldn’t change anything for the user
and this is helpful in some rare cases)
-}

ap : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {x y : A}
  → (x == y → f x == f y)
ap f idp = idp

ap↓ : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  (g : {a : A} → B a → C a) {x y : A} {p : x == y}
  {u : B x} {v : B y}
  → (u == v [ B ↓ p ] → g u == g v [ C ↓ p ])
ap↓ g {p = idp} p = ap g p

{-
[apd↓] is defined in lib.PathOver. Unlike [ap↓] and [ap], [apd] is not
definitionally a special case of [apd↓]
-}

apd : ∀ {i j} {A : Type i} {B : A → Type j} (f : (a : A) → B a) {x y : A}
  → (p : x == y) → f x == f y [ B ↓ p ]
apd f idp = idp

{-
An equality between types gives two maps back and forth
-}

coe : ∀ {i} {A B : Type i} (p : A == B) → A → B
coe idp x = x

coe! : ∀ {i} {A B : Type i} (p : A == B) → B → A
coe! idp x = x

{-
The operations of transport forward and backward are defined in terms of [ap]
and [coe], because this is more convenient in practice.
-}

transport : ∀ {i j} {A : Type i} (B : A → Type j) {x y : A} (p : x == y)
  → (B x → B y)
transport B p = coe (ap B p)

transport! : ∀ {i j} {A : Type i} (B : A → Type j) {x y : A} (p : x == y)
  → (B y → B x)
transport! B p = coe! (ap B p)

{- Equational reasoning

Equational reasoning is a way to write readable chains of equalities.
The idea is that you can write the following:

  t : a == e
  t = a =⟨ p ⟩
      b =⟨ q ⟩
      c =⟨ r ⟩
      d =⟨ s ⟩
      e ∎

where [p] is a path from [a] to [b], [q] is a path from [b] to [c], and so on.

You often have to apply some equality in some context, for instance [p] could be
[ap ctx thm] where [thm] is the interesting theorem used to prove that [a] is
equal to [b], and [ctx] is the context.
In such cases, you can use instead [thm |in-ctx ctx]. The advantage is that
[ctx] is usually boring whereas the first word of [thm] is the most interesting
part.

_=⟨_⟩ is not definitionally the same thing as concatenation of paths _∙_ because
we haven’t defined concatenation of paths yet, and also you probably shouldn’t
reason on paths constructed with equational reasoning.
If you do want to reason on paths constructed with equational reasoning, check
out lib.types.PathSeq instead.
-}

infix  2 _∎
infixr 2 _=⟨_⟩_

_=⟨_⟩_ : ∀ {i} {A : Type i} (x : A) {y z : A} → x == y → y == z → x == z
_ =⟨ idp ⟩ idp = idp

_∎ : ∀ {i} {A : Type i} (x : A) → x == x
_ ∎ = idp

syntax ap f p = p |in-ctx f

{- Truncation levels

The type of truncation levels is isomorphic to the type of natural numbers but
"starts at -2".
-}

data TLevel : Type₀ where
  ⟨-2⟩ : TLevel
  succT : (n : TLevel) → TLevel

ℕ₋₂ = TLevel

⟨-1⟩ : TLevel
⟨-1⟩ = succT ⟨-2⟩

⟨0⟩ : TLevel
⟨0⟩ = succT ⟨-1⟩

{- Coproducts and case analysis -}

data Coprod {i j} (A : Type i) (B : Type j) : Type (lmax i j) where
  inl : A → Coprod A B
  inr : B → Coprod A B

{- Σ-types

Σ-types are defined as a record so that we have definitional η.
-}

infix 1 _,_

record Σ {i j} (A : Type i) (B : A → Type j) : Type (lmax i j) where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ public

pair= : ∀ {i j} {A : Type i} {B : A → Type j}
  {a a' : A} (p : a == a') {b : B a} {b' : B a'}
  (q : b == b' [ B ↓ p ])
  → (a , b) == (a' , b')
pair= idp q = ap (_,_ _) q

pair×= : ∀ {i j} {A : Type i} {B : Type j}
  {a a' : A} (p : a == a') {b b' : B} (q : b == b')
  → (a , b) == (a' , b')
pair×= idp q = pair= idp q

{- Empty type

We define the eliminator of the empty type using an absurd pattern. Given that
absurd patterns are not consistent with HIT, we will not use empty patterns
anymore after that.
-}

data Empty : Type₀ where

Empty-elim : ∀ {i} {A : Empty → Type i} → ((x : Empty) → A x)
Empty-elim ()

{- Negation and disequality -}

¬ : ∀ {i} (A : Type i) → Type i
¬ A = A → Empty

_≠_ : ∀ {i} {A : Type i} → (A → A → Type i)
x ≠ y = ¬ (x == y)

-- Cartesian product
_×_ : ∀ {i j} (A : Type i) (B : Type j) → Type _
A × B = Σ A (λ _ → B)

⊥ = Empty

{- Π-types

Shorter notation for Π-types.
-}

Π : ∀ {i j} (A : Type i) (P : A → Type j) → Type _
Π A P = (x : A) → P x

{- Bool type -}

data Bool : Type₀ where
  true : Bool
  false : Bool

{- Equivalences -}

module _ {i} {j} {A : Type i} {B : Type j} where

  record is-equiv (f : A → B) : Type (lmax i j)
    where
    field
      g : B → A
      f-g : (b : B) → f (g b) == b
      g-f : (a : A) → g (f a) == a
      adj : (a : A) → ap f (g-f a) == f-g (f a)

{- Definition of contractible types and truncation levels -}

module _ {i} where
  is-contr : Type i → Type i
  is-contr A = Σ A (λ a → ((x : A) → a == x))

  has-level : ℕ₋₂ → (Type i → Type i)
  has-level ⟨-2⟩ A = is-contr A
  has-level (succT n) A = (x y : A) → has-level n (x == y)

  is-prop = has-level ⟨-1⟩
  is-set  = has-level ⟨0⟩

max_stars_repo_name: aerskine/hott-ex

max_issues_repo_name: aerskine/hott-ex

max_forks_repo_name: aerskine/hott-ex


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Relation.Binary.Raw

module Cubical.Relation.Binary.Reasoning.StrictPartialOrder
  {a ℓ} {A : Type a} (S : StrictPartialOrder A ℓ) where

open StrictPartialOrder S
import Cubical.Relation.Binary.Raw.Construct.StrictToNonStrict _<_ as NonStrict

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Cubical.Relation.Binary.Reasoning.Base.Double
  (NonStrict.isPreorder transitive)
  transitive
  NonStrict.<⇒≤
  (NonStrict.<-≤-trans transitive)
  public


text:
{-# OPTIONS --allow-exec #-}

module ExecAgda where

open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Reflection.External

macro
  test : Term → TC ⊤
  test hole = execTC "agda" ("-v0" ∷ "-i" ∷ "test/Succeed" ∷ "test/Succeed/exec-tc/empty.agda" ∷ []) ""
          >>= λ{(exitCode , (stdOut , stdErr)) → unify hole (lit (string stdOut))}

_ : test ≡ ""
_ = refl


text:
module Issue623.B where

S : Set
S = S


text:
module Options-in-right-order where

data Unit : Set where
  unit : Unit

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}

postulate
  return : {A : Set} → A → IO A

{-# COMPILED return (\_ -> return) #-}

main = return unit

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Numeral.Natural.Combinatorics.Proofs where

open import Functional
import      Lvl
open import Logic
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Combinatorics
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Multiplication
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Relator.Equals.Proofs.Equiv
open import Structure.Setoid hiding (_≡_ ; _≢_)
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity
open import Type

factorial-non-zero : ∀{n} → ((n !) ≢ 𝟎)
factorial-non-zero {𝟎}   ()
factorial-non-zero {𝐒 n} p with [⋅]-product-is-0 {a = 𝐒 n}{b = n !} p
... | [∨]-introᵣ n!0 = factorial-non-zero {n} n!0

instance
  factorial-positive : ∀{n} → Positive(n !)
  factorial-positive {n} = non-zero-positive(factorial-non-zero {n})

-- Also called: Pascals's identity
𝑐𝐶-step : ∀{n k} → (𝑐𝐶 (𝐒(n)) (𝐒(k)) ≡ 𝑐𝐶 n k + 𝑐𝐶 n (𝐒(k)))
𝑐𝐶-step = [≡]-intro

𝑐𝐶-empty-subsets : ∀{n} → (𝑐𝐶 n 𝟎 ≡ 𝐒(𝟎))
𝑐𝐶-empty-subsets {𝟎}   = [≡]-intro
𝑐𝐶-empty-subsets {𝐒 n} = [≡]-intro

𝑐𝐶-singleton-subsets : ∀{n} → (𝑐𝐶 n (𝐒 𝟎) ≡ n)
𝑐𝐶-singleton-subsets {𝟎}   = [≡]-intro
𝑐𝐶-singleton-subsets {𝐒 n} = congruence₁(𝐒) (𝑐𝐶-singleton-subsets {n})
{-# REWRITE 𝑐𝐶-singleton-subsets #-}

𝑐𝐶-larger-subsets : ∀{n k} → (n < k) → (𝑐𝐶 n k ≡ 𝟎)
𝑐𝐶-larger-subsets {𝟎}         (succ _) = [≡]-intro
𝑐𝐶-larger-subsets {𝐒 n} {𝐒 k} (succ p)
  rewrite 𝑐𝐶-larger-subsets {n} {k} p
  rewrite 𝑐𝐶-larger-subsets {n} {𝐒 k} ([≤]-successor p)
  = [≡]-intro

𝑐𝐶-full-subsets : ∀{n} → (𝑐𝐶 n n ≡ 𝐒(𝟎))
𝑐𝐶-full-subsets {𝟎}   = [≡]-intro
𝑐𝐶-full-subsets {𝐒 n}
  rewrite 𝑐𝐶-full-subsets {n}
  rewrite 𝑐𝐶-larger-subsets {n}{𝐒 n} (reflexivity(_≤_))
  = [≡]-intro

𝑐𝐶-excluding-single-subsets : ∀{n} → (𝑐𝐶 (𝐒 n) n ≡ 𝐒(n))
𝑐𝐶-excluding-single-subsets {𝟎}   = [≡]-intro
𝑐𝐶-excluding-single-subsets {𝐒 n}
  rewrite 𝑐𝐶-excluding-single-subsets {n}
  rewrite 𝑐𝐶-full-subsets {n}
  rewrite 𝑐𝐶-larger-subsets {n}{𝐒 n} (reflexivity(_≤_))
  = [≡]-intro

{-
𝑐𝐶-test2 : ∀{k₁ k₂} → (𝑐𝐶 (𝐒(k₁ + k₂)) k₁ + 𝑐𝐶 (k₁ + k₂) (𝐒 k₁) ≡ 𝑐𝐶 (𝐒(k₁ + k₂)) k₂ + 𝑐𝐶 (k₁ + k₂) (𝐒 k₂))
𝑐𝐶-test2 {𝟎} {𝟎} = [≡]-intro
𝑐𝐶-test2 {𝟎} {𝐒 k₂}
  rewrite 𝑐𝐶-full-subsets {k₂}
  rewrite 𝑐𝐶-larger-subsets {k₂} (reflexivity(_≤_))
  rewrite 𝑐𝐶-larger-subsets {k₂} ([≤]-successor(reflexivity(_≤_)))
  rewrite 𝑐𝐶-excluding-single-subsets {k₂}
  = [≡]-intro
𝑐𝐶-test2 {𝐒 k₁} {𝟎}
  rewrite 𝑐𝐶-full-subsets {k₁}
  rewrite 𝑐𝐶-larger-subsets {k₁} (reflexivity(_≤_))
  rewrite 𝑐𝐶-larger-subsets {k₁} ([≤]-successor(reflexivity(_≤_)))
  rewrite 𝑐𝐶-excluding-single-subsets {k₁}
  = [≡]-intro
𝑐𝐶-test2 {𝐒 k₁} {𝐒 k₂}
  -- rewrite test2 {k₁ + k₂} {k₁} {k₂} [≡]-intro
  -- rewrite test2 {𝐒(k₁ + k₂)} {𝐒 k₁} {k₂} [≡]-intro
  -- rewrite test2 {𝐒(k₁ + k₂)} {k₁} {𝐒 k₂} [≡]-intro
  = {!!}

𝑐𝐶-symmetric : ∀{n k₁ k₂} → (k₁ + k₂ ≡ n) → (𝑐𝐶 n k₁ ≡ 𝑐𝐶 n k₂)
𝑐𝐶-symmetric {𝟎} {𝟎} {𝟎} x = [≡]-intro
𝑐𝐶-symmetric {𝐒 n} {𝟎} {𝐒 .n} [≡]-intro
  rewrite 𝑐𝐶-full-subsets {n}
  rewrite 𝑐𝐶-larger-subsets {n} (reflexivity(_≤_))
  = [≡]-intro
𝑐𝐶-symmetric {𝐒 n} {𝐒 .n} {𝟎} [≡]-intro
  rewrite 𝑐𝐶-full-subsets {n}
  rewrite 𝑐𝐶-larger-subsets {n} (reflexivity(_≤_))
  = [≡]-intro
𝑐𝐶-symmetric {𝐒 .(𝐒(k₁ + k₂))} {𝐒 k₁} {𝐒 k₂} [≡]-intro
  =
    𝑐𝐶 (𝐒(𝐒(k₁ + k₂))) (𝐒 k₁)                                    🝖[ _≡_ ]-[]
    𝑐𝐶 (𝐒(k₁ + k₂)) k₁ + 𝑐𝐶 (𝐒(k₁ + k₂)) (𝐒 k₁)                  🝖[ _≡_ ]-[]
    𝑐𝐶 (𝐒(k₁ + k₂)) k₁ + (𝑐𝐶 (k₁ + k₂) k₁ + 𝑐𝐶 (k₁ + k₂) (𝐒 k₁)) 🝖[ _≡_ ]-[ One.commuteₗ-assocᵣ {_▫_ = _+_}{a = 𝑐𝐶 (𝐒(k₁ + k₂)) k₁}{b = 𝑐𝐶 (k₁ + k₂) k₁}{c = 𝑐𝐶 (k₁ + k₂) (𝐒 k₁)} ]
    𝑐𝐶 (k₁ + k₂) k₁ + (𝑐𝐶 (𝐒(k₁ + k₂)) k₁ + 𝑐𝐶 (k₁ + k₂) (𝐒 k₁)) 🝖[ _≡_ ]-[ congruence₂(_+_) (𝑐𝐶-symmetric {k₁ + k₂} {k₁} {k₂} [≡]-intro) (𝑐𝐶-test2 {k₁}{k₂}) ]
    𝑐𝐶 (k₁ + k₂) k₂ + (𝑐𝐶 (𝐒(k₁ + k₂)) k₂ + 𝑐𝐶 (k₁ + k₂) (𝐒 k₂)) 🝖[ _≡_ ]-[ One.commuteₗ-assocᵣ {_▫_ = _+_}{a = 𝑐𝐶 (𝐒(k₁ + k₂)) k₂}{b = 𝑐𝐶 (k₁ + k₂) k₂}{c = 𝑐𝐶 (k₁ + k₂) (𝐒 k₂)} ]-sym
    𝑐𝐶 (𝐒(k₁ + k₂)) k₂ + (𝑐𝐶 (k₁ + k₂) k₂ + 𝑐𝐶 (k₁ + k₂) (𝐒 k₂)) 🝖[ _≡_ ]-[]
    𝑐𝐶 (𝐒(k₁ + k₂)) k₂ + 𝑐𝐶 (𝐒(k₁ + k₂)) (𝐒 k₂)                  🝖[ _≡_ ]-[]
    𝑐𝐶 (𝐒(𝐒(k₁ + k₂))) (𝐒 k₂)                                    🝖-end
-}

-- ∀{n k} → 𝑐𝐶 n k ≡ 𝑐𝐶 n (n−k)
-- ∀{n k} → 𝑐𝐶 (𝐒 n) (𝐒 k) ≡ 𝑐𝐶 n k ⋅ (𝐒 n) / (𝐒 k)
-- ∀{n} → (∑(𝟎 ‥ n) (𝑐𝐶 n) ≡ 2 ^ n)
-- ∀{n k} → (𝑐𝐶 (𝐒 n) (𝐒 k) ≡ ∑(0 ‥ n) (i ↦ 𝑐𝐶 i k) = ∑(k ‥ n) (i ↦ 𝑐𝐶 i k))

𝑐𝑃-empty : ∀{n} → (𝑐𝑃 n 𝟎 ≡ 𝐒(𝟎))
𝑐𝑃-empty {𝟎}   = [≡]-intro
𝑐𝑃-empty {𝐒 n} = [≡]-intro

𝑐𝑃-singleton : ∀{n} → (𝑐𝑃 n (𝐒 𝟎) ≡ n)
𝑐𝑃-singleton {𝟎}   = [≡]-intro
𝑐𝑃-singleton {𝐒 n} = [≡]-intro
{-# REWRITE 𝑐𝑃-singleton #-}

𝑐𝑃-step-diff : ∀{n k} → (𝑐𝑃 n k ⋅ n ≡ 𝑐𝑃 n k ⋅ k + 𝑐𝑃 n (𝐒 k)) -- TODO: Prove this for 𝑐𝐶 by using 𝑐𝐶-permutations-is-𝑐𝑃
𝑐𝑃-step-diff {𝟎} {𝟎} = [≡]-intro
𝑐𝑃-step-diff {𝟎} {𝐒 k} = [≡]-intro
𝑐𝑃-step-diff {𝐒 n} {𝟎} = [≡]-intro
𝑐𝑃-step-diff {𝐒 n} {𝐒 k} =
  𝑐𝑃 (𝐒 n) (𝐒 k) ⋅ (𝐒 n)                                      🝖[ _≡_ ]-[]
  (𝑐𝑃 n k ⋅ (𝐒 n)) ⋅ (𝐒 n)                                    🝖[ _≡_ ]-[]
  (𝑐𝑃 n k + 𝑐𝑃 n k ⋅ n) ⋅ (𝐒 n)                               🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_+_) {x = 𝑐𝑃 n k}{y = 𝑐𝑃 n k ⋅ n}{z = 𝐒 n} ]
  (𝑐𝑃 n k ⋅ (𝐒 n)) + ((𝑐𝑃 n k ⋅ n) ⋅ (𝐒 n))                   🝖[ _≡_ ]-[ congruence₂(_+_) (reflexivity(_≡_) {x = 𝑐𝑃 (𝐒 n) (𝐒 k)}) proof1 ]
  𝑐𝑃 (𝐒 n) (𝐒 k) + ((𝑐𝑃 (𝐒 n) (𝐒 k) ⋅ k) + 𝑐𝑃 (𝐒 n) (𝐒(𝐒 k))) 🝖[ _≡_ ]-[ associativity(_+_) {x = 𝑐𝑃 (𝐒 n) (𝐒 k)}{y = 𝑐𝑃 (𝐒 n) (𝐒 k) ⋅ k}{z = 𝑐𝑃 (𝐒 n) (𝐒(𝐒 k))} ]-sym
  (𝑐𝑃 (𝐒 n) (𝐒 k) + (𝑐𝑃 (𝐒 n) (𝐒 k) ⋅ k)) + 𝑐𝑃 (𝐒 n) (𝐒(𝐒 k)) 🝖[ _≡_ ]-[]
  (𝑐𝑃 (𝐒 n) (𝐒 k) ⋅ 𝐒 k) + 𝑐𝑃 (𝐒 n) (𝐒(𝐒 k))                  🝖-end
  where
    proof2 =
      (𝑐𝑃 n k ⋅ k) ⋅ (𝐒 n) 🝖[ _≡_ ]-[ One.commuteᵣ-assocₗ {_▫_ = _⋅_}{a = 𝑐𝑃 n k}{b = k}{c = 𝐒 n} ]
      (𝑐𝑃 n k ⋅ (𝐒 n)) ⋅ k 🝖[ _≡_ ]-[]
      𝑐𝑃 (𝐒 n) (𝐒 k) ⋅ k   🝖-end

    proof1 =
      (𝑐𝑃 n k ⋅ n) ⋅ (𝐒 n)                          🝖[ _≡_ ]-[ congruence₂ₗ(_⋅_)(𝐒 n) (𝑐𝑃-step-diff {n}{k}) ]
      (𝑐𝑃 n k ⋅ k + 𝑐𝑃 n (𝐒 k)) ⋅ (𝐒 n)             🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_+_) {x = 𝑐𝑃 n k ⋅ k}{y = 𝑐𝑃 n (𝐒 k)}{z = 𝐒 n} ]
      ((𝑐𝑃 n k ⋅ k) ⋅ (𝐒 n)) + (𝑐𝑃 n (𝐒 k) ⋅ (𝐒 n)) 🝖[ _≡_ ]-[ congruence₂(_+_) proof2 (reflexivity(_≡_)) ]
      (𝑐𝑃 (𝐒 n) (𝐒 k) ⋅ k) + 𝑐𝑃 (𝐒 n) (𝐒(𝐒 k))      🝖-end

𝑐𝑃-step-alt : ∀{n k} → (𝑐𝑃 (𝐒 n) (𝐒 k) ≡ (𝑐𝑃 n k ⋅ 𝐒 k) + 𝑐𝑃 n (𝐒 k))
𝑐𝑃-step-alt {n}{k} rewrite 𝑐𝑃-step-diff {n}{k} = symmetry(_≡_) (associativity(_+_) {x = 𝑐𝑃 n k}{y = 𝑐𝑃 n k ⋅ k}{z = 𝑐𝑃 n (𝐒 k)})

𝑐𝐶-permutations-is-𝑐𝑃 : ∀{n k} → (𝑐𝐶 n k ⋅ (k !) ≡ 𝑐𝑃 n k)
𝑐𝐶-permutations-is-𝑐𝑃 {𝟎} {𝟎}     = [≡]-intro
𝑐𝐶-permutations-is-𝑐𝑃 {𝟎} {𝐒 k}   = [≡]-intro
𝑐𝐶-permutations-is-𝑐𝑃 {𝐒 n} {𝟎}   = [≡]-intro
𝑐𝐶-permutations-is-𝑐𝑃 {𝐒 n} {𝐒 k} =
  (𝑐𝐶 n k + 𝑐𝐶 n (𝐒 k)) ⋅ (𝐒 k ⋅ (k !))                   🝖-[ distributivityᵣ(_⋅_)(_+_) {x = 𝑐𝐶 n k}{y = 𝑐𝐶 n (𝐒 k)}{z = 𝐒 k ⋅ (k !)} ]
  (𝑐𝐶 n k ⋅ (𝐒 k ⋅ (k !))) + (𝑐𝐶 n (𝐒 k) ⋅ (𝐒 k ⋅ (k !))) 🝖-[ congruence₂(_+_) l r ]
  (𝑐𝑃 n k ⋅ 𝐒 k) + 𝑐𝑃 n (𝐒 k)                             🝖-[ 𝑐𝑃-step-alt {n}{k} ]-sym
  𝑐𝑃 n k ⋅ 𝐒 n                                            🝖-end
  where
    l =
      𝑐𝐶 n k ⋅ (𝐒 k ⋅ (k !)) 🝖-[ congruence₂ᵣ(_⋅_)(𝑐𝐶 n k) (commutativity(_⋅_) {𝐒 k}{k !}) ]
      𝑐𝐶 n k ⋅ ((k !) ⋅ 𝐒 k) 🝖-[ associativity(_⋅_) {x = 𝑐𝐶 n k}{y = k !}{z = 𝐒 k} ]-sym
      (𝑐𝐶 n k ⋅ (k !)) ⋅ 𝐒 k 🝖-[ congruence₂ₗ(_⋅_)(𝐒 k) (𝑐𝐶-permutations-is-𝑐𝑃 {n} {k}) ]
      𝑐𝑃 n k ⋅ 𝐒 k           🝖-end

    r =
      𝑐𝐶 n (𝐒 k) ⋅ (𝐒 k ⋅ (k !)) 🝖[ _≡_ ]-[]
      𝑐𝐶 n (𝐒 k) ⋅ ((𝐒 k)!)      🝖[ _≡_ ]-[ 𝑐𝐶-permutations-is-𝑐𝑃 {n} {𝐒 k} ]
      𝑐𝑃 n (𝐒 k)                 🝖-end

𝑐𝑃-full : ∀{n} → (𝑐𝑃 n n ≡ n !)
𝑐𝑃-full {n} =
  𝑐𝑃 n n         🝖[ _≡_ ]-[ 𝑐𝐶-permutations-is-𝑐𝑃 {n}{n} ]-sym
  𝑐𝐶 n n ⋅ (n !) 🝖[ _≡_ ]-[ congruence₂ₗ(_⋅_)(n !) (𝑐𝐶-full-subsets {n}) ]
  𝐒(𝟎) ⋅ (n !)   🝖[ _≡_ ]-[]
  n !            🝖-end

𝑐𝐶-step-diff : ∀{n k} → (𝑐𝐶 n k ⋅ n ≡ (𝑐𝐶 n k ⋅ k) + (𝑐𝐶 n (𝐒 k) ⋅ (𝐒 k)))
𝑐𝐶-step-diff {n}{k} = [⋅]-cancellationᵣ {x = k !} ⦃ factorial-positive {k} ⦄ $
  (𝑐𝐶 n k ⋅ n) ⋅ (k !)                                  🝖[ _≡_ ]-[ One.commuteᵣ-assocₗ {_▫_ = _⋅_}{a = 𝑐𝐶 n k}{b = n}{c = k !} ]
  (𝑐𝐶 n k ⋅ (k !)) ⋅ n                                  🝖[ _≡_ ]-[ congruence₁(_⋅ n) (𝑐𝐶-permutations-is-𝑐𝑃 {n}{k}) ]
  𝑐𝑃 n k ⋅ n                                            🝖[ _≡_ ]-[ 𝑐𝑃-step-diff {n}{k} ]
  𝑐𝑃 n k ⋅ k + 𝑐𝑃 n (𝐒 k)                               🝖[ _≡_ ]-[ congruence₂(_+_) (congruence₁(_⋅ k) (symmetry(_≡_) (𝑐𝐶-permutations-is-𝑐𝑃 {n}{k}))) (symmetry(_≡_) (𝑐𝐶-permutations-is-𝑐𝑃 {n}{𝐒 k})) ]
  (𝑐𝐶 n k ⋅ (k !)) ⋅ k + (𝑐𝐶 n (𝐒 k) ⋅ ((𝐒 k) !))       🝖[ _≡_ ]-[]
  (𝑐𝐶 n k ⋅ (k !)) ⋅ k + (𝑐𝐶 n (𝐒 k) ⋅ ((𝐒 k) ⋅ (k !))) 🝖[ _≡_ ]-[ congruence₂(_+_) (One.commuteᵣ-assocₗ {_▫_ = _⋅_}{a = 𝑐𝐶 n k}{b = k !}{c = k}) (symmetry(_≡_) (associativity(_⋅_) {x = 𝑐𝐶 n (𝐒 k)}{y = 𝐒 k}{z = k !})) ]
  (𝑐𝐶 n k ⋅ k) ⋅ (k !) + ((𝑐𝐶 n (𝐒 k) ⋅ (𝐒 k)) ⋅ (k !)) 🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_+_) {x = 𝑐𝐶 n k ⋅ k}{y = 𝑐𝐶 n (𝐒 k) ⋅ (𝐒 k)}{z = k !} ]-sym
  ((𝑐𝐶 n k ⋅ k) + (𝑐𝐶 n (𝐒 k) ⋅ (𝐒 k))) ⋅ (k !)         🝖-end

{-
-- Note: This is a variant of the usual definition of 𝑐𝐶 (The usual one: 𝑐𝐶 n k = (n !) / ((k !) ⋅ (n − k)!)).
factorial-of-[+] : ∀{k₁ k₂} → ((k₁ + k₂)! ≡ (k₁ !) ⋅ (k₂ !) ⋅ 𝑐𝐶 (k₁ + k₂) k₁)
factorial-of-[+] {𝟎} {k₂} = [≡]-intro
factorial-of-[+] {𝐒 k₁} {k₂} =
  ((𝐒(k₁) + k₂) !)                                 🝖[ _≡_ ]-[]
  (𝐒(k₁ + k₂) !)                                   🝖[ _≡_ ]-[]
  𝐒(k₁ + k₂) ⋅ ((k₁ + k₂) !)                       🝖[ _≡_ ]-[ congruence₂ᵣ(_⋅_)(𝐒(k₁ + k₂)) (factorial-of-[+] {k₁} {k₂}) ]
  𝐒(k₁ + k₂) ⋅ ((k₁ !) ⋅ (k₂ !) ⋅ 𝑐𝐶 (k₁ + k₂) k₁) 🝖[ _≡_ ]-[]
  (𝐒(k₁) + k₂) ⋅ ((k₁ !) ⋅ (k₂ !) ⋅ 𝑐𝐶 (k₁ + k₂) k₁) 🝖[ _≡_ ]-[ {!!} ]
  ((𝐒(k₁) + k₂) ⋅ (k₁ !)) ⋅ ((k₂ !) ⋅ 𝑐𝐶 (k₁ + k₂) k₁) 🝖[ _≡_ ]-[ {!!} ]
  ((𝐒(k₁) ⋅ (k₁ !)) + (k₂ ⋅ (k₁ !))) ⋅ ((k₂ !) ⋅ 𝑐𝐶 (k₁ + k₂) k₁) 🝖[ _≡_ ]-[ {!!} ]
  ((𝐒(k₁) !) + (k₂ ⋅ (k₁ !))) ⋅ ((k₂ !) ⋅ 𝑐𝐶 (k₁ + k₂) k₁) 🝖[ _≡_ ]-[ {!!} ]
  (𝐒(k₁) !) ⋅ (k₂ !) ⋅ 𝑐𝐶(𝐒(k₁) + k₂) (𝐒(k₁))      🝖-end

𝐒 k₁ ⋅ (k₁ !) ⋅ (k₂ !) ⋅ (𝑐𝐶 (k₁ + k₂) k₁ + 𝑐𝐶 (k₁ + k₂) (𝐒 k₁))
-}
{-factorial-of-[+] {𝟎} {𝟎} = [≡]-intro
factorial-of-[+] {𝟎} {𝐒 k₂} = [≡]-intro
factorial-of-[+] {𝐒 k₁} {𝟎}
  rewrite 𝑐𝐶-full-subsets {k₁}
  rewrite 𝑐𝐶-larger-subsets {k₁} {𝐒 k₁} (reflexivity(_≤_))
  = [≡]-intro
factorial-of-[+] {𝐒 k₁} {𝐒 k₂} = {!!}
𝐒(𝐒(k₁ + k₂)) ⋅ (𝐒(k₁ + k₂) ⋅ ((k₁ + k₂)!))
𝐒(𝐒(k₁ + k₂)) ⋅ (𝐒(k₁ + k₂) ⋅ ((k₁ !) ⋅ (k₂ !) ⋅ 𝑐𝐶 (k₁ + k₂) k₁))
𝐒(k₁) ⋅ (k₁ !) ⋅ (𝐒 k₂ ⋅ (k₂ !)) ⋅ (𝑐𝐶 (𝐒(k₁ + k₂)) k₁ + (𝑐𝐶 (k₁ + k₂) k₁ + 𝑐𝐶 (k₁ + k₂) (𝐒 k₁)))
-}

{-
-- Note: This is a variant of the usual definition of 𝑐𝑃 (The usual one: 𝑐𝑃 n k = (n !) / ((n − k)!)).
factorial-of-[+]-𝑐𝑃 : ∀{k₁ k₂} → ((k₁ + k₂)! ≡ 𝑐𝑃 (k₁ + k₂) k₂ ⋅ (k₁ !))
factorial-of-[+]-𝑐𝑃 {𝟎} {𝟎} = [≡]-intro
factorial-of-[+]-𝑐𝑃 {𝟎} {𝐒 k₂}
  rewrite 𝑐𝑃-full {k₂}
  =
    𝐒 k₂ ⋅ (k₂ !)        🝖[ _≡_ ]-[ commutativity(_⋅_) {𝐒 k₂}{k₂ !} ]
    (k₂ !) ⋅ 𝐒 k₂        🝖[ _≡_ ]-[]
    (k₂ !) + (k₂ !) ⋅ k₂ 🝖-end
factorial-of-[+]-𝑐𝑃 {𝐒 k₁} {𝟎} = [≡]-intro
factorial-of-[+]-𝑐𝑃 {𝐒 k₁} {𝐒 k₂} = {!!}
𝐒(𝐒(k₁ + k₂)) ⋅ (𝐒(k₁ + k₂) ⋅ ((k₁ + k₂)!))
𝐒(𝐒(k₁ + k₂)) ⋅ (𝐒(k₁ + k₂) ⋅ (𝑐𝑃 (k₁ + k₂) k₂ ⋅ (k₁ !)))
(𝑐𝑃 (𝐒(k₁ + k₂)) k₂ + (𝑐𝑃 (𝐒(k₁ + k₂)) k₂ + 𝑐𝑃 (𝐒(k₁ + k₂)) k₂ ⋅ (k₁ + k₂))) ⋅ (𝐒 k₁ ⋅ (k₁ !))
-}

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:
------------------------------------------------------------------------
-- Parallel substitutions (defined as functions)
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Function.Basics
  {i u e} {Uni : IndexedUniverse i u e} where

import Axiom.Extensionality.Propositional as E
import deBruijn.Context; open deBruijn.Context Uni
open import Function using (id; _∘_; _$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning

-- Substitutions, represented as functions from variables to terms.

Sub : ∀ {t} (T : Term-like t) {Γ Δ : Ctxt} → Γ ⇨̂ Δ → Set _
Sub T = [ Var ⟶ T ]

private
 module Dummy {t} {T : Term-like t} where

  open Term-like T

  -- Interpretation of substitutions: context morphisms.

  ⟦_⟧⇨ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Γ ⇨̂ Δ
  ⟦_⟧⇨ {ρ̂ = ρ̂} _ = ρ̂

  -- Application of substitutions to types.

  infixl 8 _/I_ _/_

  _/I_ : ∀ {Γ Δ i} {ρ̂ : Γ ⇨̂ Δ} → IType Γ i → Sub T ρ̂ → IType Δ i
  σ /I ρ = σ /̂I ⟦ ρ ⟧⇨

  _/_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Type Γ → Sub T ρ̂ → Type Δ
  σ / ρ = σ /̂ ⟦ ρ ⟧⇨

  -- Application of substitutions to values.

  infixl 8 _/Val_

  _/Val_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
           Value Γ σ → Sub T ρ̂ → Value Δ (σ /̂ ρ̂)
  v /Val ρ = v /̂Val ⟦ ρ ⟧⇨

  -- Application of substitutions to context extensions.

  infixl 8 _/⁺_ _/₊_

  _/⁺_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Ctxt⁺ Γ → Sub T ρ̂ → Ctxt⁺ Δ
  Γ⁺ /⁺ ρ = Γ⁺ /̂⁺ ⟦ ρ ⟧⇨

  _/₊_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Ctxt₊ Γ → Sub T ρ̂ → Ctxt₊ Δ
  Γ₊ /₊ ρ = Γ₊ /̂₊ ⟦ ρ ⟧⇨

  -- Application of substitutions to variables.

  infixl 8 _/∋_ _/∋-lemma_

  _/∋_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ∋ σ → (ρ : Sub T ρ̂) → Δ ⊢ σ / ρ
  x /∋ ρ = ρ · x

  _/∋-lemma_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρ : Sub T ρ̂) →
               x /̂∋ ⟦ ρ ⟧⇨ ≅-Value ⟦ x /∋ ρ ⟧
  x /∋-lemma ρ = corresponds ρ x

  app∋ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → [ Var ⟶ T ] ρ̂
  app∋ ρ = record
    { function    = λ _ x → x /∋       ρ
    ; corresponds = λ _ x → x /∋-lemma ρ
    }

  -- Empty substitution.

  ε⇨ : ∀ {Δ} → Sub T ε̂[ Δ ]
  ε⇨ = record { function = λ _ (); corresponds = λ _ () }

  ε⇨[_] : ∀ Δ → Sub T ε̂[ Δ ]
  ε⇨[ _ ] = ε⇨

  -- Extends a substitution with another term.

  private

    -- This function is not local to _▻⇨[_]_ because a proof below
    -- fails to type check if the function depends on the proof
    -- component of the substitution.

    fun : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
          (∀ {τ} → Γ ∋ τ → Δ ⊢ τ /̂ ρ̂) →
          (t : Δ ⊢ σ /̂ ρ̂) →
          ∀ {τ} → Γ ▻ σ ∋ τ → Δ ⊢ τ /̂ (ρ̂ ▻̂ ⟦ t ⟧)
    fun f t zero    = t
    fun f t (suc x) = f x

  infixl 5 _▻⇨_ _▻⇨[_]_

  _▻⇨[_]_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
            (ρ : Sub T ρ̂) σ (t : Δ ⊢ σ / ρ) → Sub T (ρ̂ ▻̂[ σ ] ⟦ t ⟧)
  _▻⇨[_]_ {Γ} {Δ} {ρ̂} ρ σ t =
    record { function = λ _ → fun (_·_ ρ) t; corresponds = λ _ → corr }
    where
    abstract
      corr : ∀ {τ} (x : Γ ▻ σ ∋ τ) →
             x /̂∋ (ρ̂ ▻̂ ⟦ t ⟧) ≅-Value ⟦ fun (_·_ ρ) t x ⟧
      corr zero    = P.refl
      corr (suc x) = x /∋-lemma ρ

  _▻⇨_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ}
         (ρ : Sub T ρ̂) (t : Δ ⊢ σ / ρ) → Sub T (ρ̂ ▻̂[ σ ] ⟦ t ⟧)
  ρ ▻⇨ t = ρ ▻⇨[ _ ] t

  -- The tail of a nonempty substitution.

  tail : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} → Sub T ρ̂ → Sub T (t̂ail ρ̂)
  tail ρ = ρ [∘] weaken∋

  -- The head of a nonempty substitution.

  head : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) → Δ ⊢ σ / tail ρ
  head ρ = zero /∋ ρ

  head-lemma : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) →
               ĥead ⟦ ρ ⟧⇨ ≅-Value ⟦ head ρ ⟧
  head-lemma ρ = zero /∋-lemma ρ

  -- Equality of substitutions.

  infix 4 _≅-⇨_

  _≅-⇨_ : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} (ρ₁ : Sub T ρ̂₁)
            {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} (ρ₂ : Sub T ρ̂₂) → Set _
  _≅-⇨_ = _≅-⟶_

  -- Certain uses of substitutivity can be removed.

  drop-subst-Sub :
    ∀ {a} {A : Set a} {x₁ x₂ : A} {Γ Δ}
    (f : A → Γ ⇨̂ Δ) {ρ} (eq : x₁ ≡ x₂) →
    P.subst (λ x → Sub T (f x)) eq ρ ≅-⇨ ρ
  drop-subst-Sub f P.refl = [ P.refl ]

  -- Some congruence lemmas.

  ε⇨-cong : ∀ {Δ₁ Δ₂} → Δ₁ ≅-Ctxt Δ₂ → ε⇨[ Δ₁ ] ≅-⇨ ε⇨[ Δ₂ ]
  ε⇨-cong P.refl = [ P.refl ]

  ▻⇨-cong :
    ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {t₁ : Δ₁ ⊢ σ₁ / ρ₁}
      {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {t₂ : Δ₂ ⊢ σ₂ / ρ₂} →
    σ₁ ≅-Type σ₂ → ρ₁ ≅-⇨ ρ₂ → t₁ ≅-⊢ t₂ →
    ρ₁ ▻⇨[ σ₁ ] t₁ ≅-⇨ ρ₂ ▻⇨[ σ₂ ] t₂
  ▻⇨-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] P.refl =
    [ P.refl ]

  ⟦⟧⇨-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
               {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
             ρ₁ ≅-⇨ ρ₂ → ⟦ ρ₁ ⟧⇨ ≅-⇨̂ ⟦ ρ₂ ⟧⇨
  ⟦⟧⇨-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} [ P.refl ] = P.refl

  /I-cong :
    ∀ {i}
      {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {σ₁ : IType Γ₁ i} {ρ₁ : Sub T ρ̂₁}
      {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {σ₂ : IType Γ₂ i} {ρ₂ : Sub T ρ̂₂} →
    σ₁ ≅-IType σ₂ → ρ₁ ≅-⇨ ρ₂ → σ₁ /I ρ₁ ≅-IType σ₂ /I ρ₂
  /I-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  /-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
             {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
           σ₁ ≅-Type σ₂ → ρ₁ ≅-⇨ ρ₂ → σ₁ / ρ₁ ≅-Type σ₂ / ρ₂
  /-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  /⁺-cong : ∀ {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
            Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ≅-⇨ ρ₂ → Γ⁺₁ /⁺ ρ₁ ≅-Ctxt⁺ Γ⁺₂ /⁺ ρ₂
  /⁺-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  /₊-cong : ∀ {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
            Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ≅-⇨ ρ₂ → Γ₊₁ /₊ ρ₁ ≅-Ctxt₊ Γ₊₂ /₊ ρ₂
  /₊-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  /∋-cong : ∀ {Γ₁ Δ₁ σ₁} {x₁ : Γ₁ ∋ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
            x₁ ≅-∋ x₂ → ρ₁ ≅-⇨ ρ₂ → x₁ /∋ ρ₁ ≅-⊢ x₂ /∋ ρ₂
  /∋-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  tail-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ▻ σ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ▻ σ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
              ρ₁ ≅-⇨ ρ₂ → tail ρ₁ ≅-⇨ tail ρ₂
  tail-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} [ P.refl ] = [ P.refl ]

  head-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ▻ σ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ▻ σ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
              ρ₁ ≅-⇨ ρ₂ → head ρ₁ ≅-⊢ head ρ₂
  head-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} [ P.refl ] = P.refl

  abstract

    -- Some eta-laws, based on the assumption of extensionality.

    -- Eta in empty contexts.

    ηε : E.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t) →
         ∀ {Δ} {ρ̂ : ε ⇨̂ Δ} (ρ : Sub T ρ̂) → ρ ≅-⇨ ε⇨[ Δ ]
    ηε ext ρ = extensional-equality₁ ext P.refl (λ ())

    -- Eta in non-empty contexts.

    η▻ : E.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t) →
         ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) →
         ρ ≅-⇨ tail ρ ▻⇨[ σ ] head ρ
    η▻ ext {Γ} {σ = σ} {ρ̂} ρ = extensional-equality₂ ext lemma₁ lemma₂
      where
      open Term-like Var using () renaming (_≅-⊢_ to _≅-∋′_)

      lemma₁ : ρ̂ ≅-⇨̂ t̂ail ρ̂ ▻̂[ σ ] ⟦ head ρ ⟧
      lemma₁ = begin
        [ ρ̂                   ]  ≡⟨ P.refl ⟩
        [ t̂ail ρ̂ ▻̂ ĥead ρ̂     ]  ≡⟨ ▻̂-cong P.refl P.refl (head-lemma ρ) ⟩
        [ t̂ail ρ̂ ▻̂ ⟦ head ρ ⟧ ]  ∎

      lemma₂′ : ∀ {τ} (x : Γ ▻ σ ∋ τ) →
                x /∋ ρ ≅-⊢ x /∋ (tail ρ ▻⇨[ σ ] head ρ)
      lemma₂′ zero    = P.refl
      lemma₂′ (suc x) = P.refl

      lemma₂ : ∀ {τ₁} {x₁ : Γ ▻ σ ∋ τ₁}
                 {τ₂} {x₂ : Γ ▻ σ ∋ τ₂} →
               x₁ ≅-∋′ x₂ → x₁ /∋ ρ ≅-⊢ x₂ /∋ (tail ρ ▻⇨[ σ ] head ρ)
      lemma₂ {x₁ = x} P.refl = lemma₂′ x

    -- Two substitutions are equal if their indices are equal and
    -- their projections are pairwise equal (assuming extensionality).

    extensionality :
      E.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t) →
      ∀ {Γ Δ₁} {ρ̂₁ : Γ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
          {Δ₂} {ρ̂₂ : Γ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
      Δ₁ ≅-Ctxt Δ₂ → (∀ {σ} (x : Γ ∋ σ) → x /∋ ρ₁ ≅-⊢ x /∋ ρ₂) →
      ρ₁ ≅-⇨ ρ₂
    extensionality ext {ε} {ρ₁ = ρ₁} {ρ₂ = ρ₂} P.refl hyp =
      ρ₁  ≅-⟶⟨ ηε ext ρ₁ ⟩
      ε⇨  ≅-⟶⟨ sym-⟶ $ ηε ext ρ₂ ⟩
      ρ₂  ∎-⟶
    extensionality ext {Γ ▻ σ} {ρ₁ = ρ₁} {ρ₂ = ρ₂} P.refl hyp =
      ρ₁                  ≅-⟶⟨ η▻ ext ρ₁ ⟩
      tail ρ₁ ▻⇨ head ρ₁  ≅-⟶⟨ ▻⇨-cong P.refl
                                       (extensionality ext P.refl (hyp ∘ suc))
                                       (hyp zero) ⟩
      tail ρ₂ ▻⇨ head ρ₂  ≅-⟶⟨ sym-⟶ $ η▻ ext ρ₂ ⟩
      ρ₂                  ∎-⟶

open Dummy public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
{- Type system of the language. -}
module Syntax.Types where

-- Abstract syntax of types for the language.
data Type : Set where
    -- Unit type
    Unit   : Type
    -- Product type
    _&_    : Type -> Type -> Type
    -- Sum type
    _+_    : Type -> Type -> Type
    -- Function type
    _=>_   : Type -> Type -> Type
    -- Event type
    Event  : Type -> Type
    -- Signal type
    Signal : Type -> Type
infixr 65 _=>_
infixl 68 _+_
infixl 70 _&_

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
-- Andreas, 2019-10-21, issue #4142, reported and test case by Jason Hu

-- When the record-expression-to-copattern-translation is revisited
-- after positivity checking, the defCopatternLHS flag needs to be
-- updated as well!

-- {-# OPTIONS -v tc.cc.record:20 #-}
-- {-# OPTIONS -v tc.conv:30 #-}

open import Agda.Builtin.Equality

record WrapSet : Set1 where
  constructor wrap
  -- eta-equality -- WAS: needed for test
  field
    Wrapped : Set

  eta : WrapSet
  eta .Wrapped = Wrapped

  pack : WrapSet
  pack = record { Wrapped = Wrapped }

-- The positivity check makes WrapSet an eta-record after the fact.
-- Thus, the record-expression-to-copattern-translation is run again for pack.

open WrapSet

-- Make sure eta was inferred correctly for WrapSet

hasEta : (w : WrapSet) → w ≡ record{ Wrapped = Wrapped w }
hasEta w = refl

-- When we have a definition by copattern matching it works.

works : (w : WrapSet) → w ≡ eta w
works w = refl

-- Should also work for pack.

test : (w : WrapSet) → w ≡ pack w
test w = refl


text:
module Setoid where

open import Logic.Base

record Setoid : Set1 where
  field
    A     : Set
    _==_  : A -> A -> Prop
    refl  : {x : A} -> x == x
    sym   : {x y : A} -> x == y -> y == x
    trans : {x y z : A} -> x == y -> y == z -> x == z

module Set-Ar where

  !_! : (S : Setoid) -> Set
  ! S ! = Setoid.A S

  record SetoidArrow (S₁ S₂ : Setoid) : Set where
    field
      map  : ! S₁ ! -> ! S₂ !
      stab : {x y : Setoid.A S₁} -> Setoid._==_ S₁ x y -> Setoid._==_ S₂ (map x) (map y)

  _∘_ : {S₁ S₂ S₃ : Setoid} -> SetoidArrow S₂ S₃ -> SetoidArrow S₁ S₂ -> SetoidArrow S₁ S₃
  _∘_ {S₁} F₁ F₂ = record
    { map  = \x -> SetoidArrow.map F₁ (SetoidArrow.map F₂ x)
    ; stab = \{x y : ! S₁ !}(p : Setoid._==_ S₁ x y) -> SetoidArrow.stab F₁ (SetoidArrow.stab F₂ p)
    }

  id : {S : Setoid} -> SetoidArrow S S
  id = record
    { map  = \x -> x
    ; stab = \p -> p
    }

  _==→_ : {S₁ S₂ : Setoid} -> SetoidArrow S₁ S₂ -> SetoidArrow S₁ S₂ -> Set
  _==→_ {_} {S₂} F₁ F₂ = (forall x -> Setoid._==_ S₂ (SetoidArrow.map F₁ x) (SetoidArrow.map F₂ x)) -> True

module Set-Fam where

  open Set-Ar

  record SetoidFam (S : Setoid) : Set1 where
    field
      index     : ! S ! -> Setoid
      reindex   : {x x' : ! S !} -> Setoid._==_ S x x' -> SetoidArrow (index x) (index x')
      id-coh    : {x : ! S !} -> (reindex (Setoid.refl S)) ==→ id {index x}
      sym-coh-l : {x y : ! S !}(p : Setoid._==_ S x y) -> ((reindex (Setoid.sym S p)) ∘ (reindex p)) ==→ id
      sym-coh-r : {x y : ! S !}(p : Setoid._==_ S x y) -> ((reindex p) ∘ (reindex (Setoid.sym S p))) ==→ id
      trans-coh : {x y z : ! S !}(p : Setoid._==_ S x y)(p' : Setoid._==_ S y z) ->
                  (reindex (Setoid.trans S p p')) ==→ ((reindex p') ∘ (reindex p))

module Set-Fam-Ar where

  open Set-Ar
  open Set-Fam

  record SetoidFamArrow {S₁ S₂ : Setoid}(F₁ : SetoidFam S₁)(F₂ : SetoidFam S₂) : Set where
    field
      indexingmap : SetoidArrow S₁ S₂
      indexmap    : (x : ! S₁ !) -> SetoidArrow (SetoidFam.index F₁ x)
                    (SetoidFam.index F₂ (SetoidArrow.map indexingmap x))
      reindexmap  : (x x' : ! S₁ !)(p : Setoid._==_ S₁ x' x) ->
                    ((indexmap x) ∘ (SetoidFam.reindex F₁ p)) ==→
                    ((SetoidFam.reindex F₂ (SetoidArrow.stab indexingmap p)) ∘ (indexmap x'))

max_stars_repo_name: asr/agda-kanso


text:
-- Term matching.
module Tactic.Reflection.Match where

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.Equality

open import Control.Monad.Zero
open import Control.Monad.State
open import Container.Traversable

private
  M : Nat → Set → Set
  M n = StateT (Vec (Maybe Term) n) Maybe

  fN : ∀ {n} (i : Nat) → IsTrue (lessNat i n) → Fin n
  fN i lt = fromNat i {{lt}}

  patVar : ∀ {n} → Nat → Nat → Maybe (Fin n)
  patVar {n} zero i with lessNat i n | fN {n} i
  ... | true  | toFin = just (toFin true)
  ... | false | _     = nothing
  patVar (suc k) zero    = nothing
  patVar (suc k) (suc i) = patVar k i

  upd : ∀ {a} {A : Set a} {n} → Fin n → A → Vec A n → Vec A n
  upd  zero   x (_ ∷ xs) = x ∷ xs
  upd (suc i) x (y ∷ xs) = y ∷ upd i x xs

  matchVar : ∀ {n} → Fin n → Term → M n ⊤
  matchVar i v =
    caseM flip indexVec i <$> get of λ
    { (just u) → guard (u == v) (pure _)
    ; nothing  → _ <$ modify (upd i (just v)) }

  MatchFun : Set → Set
  MatchFun A = ∀ {n} → Nat → A → A → M n ⊤

  matchTerm matchTerm′ : MatchFun Term
  matchArgs : MatchFun (List (Arg Term))
  matchArg : MatchFun (Arg Term)
  matchAbs : MatchFun (Abs Term)

  matchTerm k (var i []) v with patVar k i
  ... | just x  = matchVar x v
  ... | nothing = matchTerm′ k (var i []) v
  matchTerm k p v = matchTerm′ k p v

  matchTerm′ {n} k (var i args) (var j args₁) =
    guard! (j <? k && isYes (i == j) || j ≥? k && isYes (j + n == i))
           (matchArgs k args args₁)
  matchTerm′ k (con c args) (con c₁ args₁) = guard (c == c₁) (matchArgs k args args₁)
  matchTerm′ k (def f args) (def g args₁) = guard (f == g) (matchArgs k args args₁)
  matchTerm′ k (lam h p) (lam h₁ v) = guard (h == h₁) (matchAbs k p v)
  matchTerm′ k (pat-lam cs args) v = empty -- todo
  matchTerm′ k (pi a b) (pi a₁ b₁) = matchArg k a a₁ >> matchAbs k b b₁
  matchTerm′ k (lit l) (lit l₁) = guard (l == l₁) (pure _)
  matchTerm′ k (agda-sort _) _ = pure _ -- ignore sorts
  matchTerm′ k (meta _ _) _ = pure _
  matchTerm′ k unknown _ = pure _
  matchTerm′ k p v = empty

  matchArgs k (x ∷ xs) (y ∷ ys) = matchArg k x y >> matchArgs k xs ys
  matchArgs k [] [] = pure _
  matchArgs k _ _   = empty

  matchAbs k (abs _ x) (abs _ y) = matchTerm (suc k) x y
  matchArg k (arg i x) (arg j y) = guard (i == j) (matchTerm k x y)

-- match |Δ| p v = just σ
--  where Γ, Δ ⊢ p
--        Γ    ⊢ v
--        Γ    ⊢ σ : Δ
--        p σ ≡ v
match : (n : Nat) → Term → Term → Maybe (Vec Term n)
match n pat v = do
  env ← snd <$> runStateT (matchTerm 0 pat v) (pure nothing ofType Vec (Maybe Term) n)
  traverse id env

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module _ where

open import Common.Bool

private
  unused = true
  used = true

private
 module Private where
  not-in-scope = true

in-scope = used

-- History:
--
-- * Ulf, 2015-20-12 c823aa9a0e84816d3e36ea86e04e9f9caa536c4a
--   [ deadcode ] local private things are not in scope at top-level
--                but imported things should be
--   The previous restriction of the top level scope (7f47d51c) was a
--   bit draconian and removed not only local private definitions but
--   all imported things from the scope. This is fixed by this commit.
--
-- * Andreas, 2021-05-18, used as testcase for issue #4647

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Issue857 where

-- From the Agda mailing list, 2013-05-24, question raised by Martin Escardo.
-- 2013-05-24 reported by Martin Escardo, test case by Andrea Vezzosi

{- The crucial point is that λ() is not equal to λ(), so e.g. the
ones appearing in the body of main-closed-ground' don't match the ones
in its own type.

To be concrete we can use a simplified version of what happens in
main-closed-ground': -}

data ⊥ : Set where

postulate
    X : Set
    P : (⊥ → X) → Set
    lemma : (f : ⊥ → X) → P f

-- Given the context above we attempt to feed agda code using λ():

main : P λ()
main = lemma λ()

{- Before we can check the type of main we have to translate λ()
away into toplevel definitions, because internally only those are
allowed pattern-matching. But each use of λ() is translated
separately, so we get:

absurd1 : ⊥ → X
absurd1 ()

absurd2 : ⊥ → X
absurd2 ()

main : P absurd1
main = lemma absurd2

Now we can proceed typechecking and find that (lemma absurd2 : P
absurd2), i.e. applications of lemma only care about the type of its
argument, but for main to typecheck we need the type of the body (P
absurd2) to equal the declared type (P absurd1), and so we'd need
absurd2 = absurd1 which unfortunately we can't deduce because those
are different definitions.  -}

-- 2013-05-24 example by Martin Escardo

open import Common.Equality

absurd-equality : _≡_ {A = ⊥ → ⊥} (λ()) λ()
absurd-equality = refl

-- λ() is not translated as λ() → () (identity with variable name ())
-- thus, these examples should type check now.


text:
------------------------------------------------------------------------
-- The stream container
------------------------------------------------------------------------

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

open import Equality

module Container.Stream
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude hiding (id; List; []; _∷_)

open import Bijection eq using (_↔_; module _↔_)
open import Container eq
open import Container.List eq as L hiding (_∷_; _++_; Any-∷; Any-++)
open import Function-universe eq hiding (_∘_)

------------------------------------------------------------------------
-- Streams

Stream : Container lzero
Stream = ⊤ ▷ const ℕ

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

-- Cons.

infixr 5 _∷_

_∷_ : {A : Type} → A → ⟦ Stream ⟧ A → ⟦ Stream ⟧ A
x ∷ (tt , lkup) = tt , λ { zero → x; (suc n) → lkup n }

-- The head of a stream.

head : {A : Type} → ⟦ Stream ⟧ A → A
head (tt , lkup) = lkup 0

-- The tail of a stream.

tail : {A : Type} → ⟦ Stream ⟧ A → ⟦ Stream ⟧ A
tail (tt , lkup) = (tt , lkup ∘ suc)

-- Appending a stream to a list.

infixr 5 _++_

_++_ : {A : Type} → ⟦ List ⟧ A → ⟦ Stream ⟧ A → ⟦ Stream ⟧ A
xs ++ ys = fold ys (λ z _ zs → z ∷ zs) xs

-- Taking the first n elements from a stream.

take : {A : Type} → ℕ → ⟦ Stream ⟧ A → ⟦ List ⟧ A
take zero    xs = []
take (suc n) xs = L._∷_ (head xs) (take n (tail xs))

-- Dropping the first n elements from a stream.

drop : {A : Type} → ℕ → ⟦ Stream ⟧ A → ⟦ Stream ⟧ A
drop zero    xs = xs
drop (suc n) xs = drop n (tail xs)

------------------------------------------------------------------------
-- Any lemmas

-- Any lemma for head/tail.

Any-head-tail : ∀ {A : Type} (P : A → Type) {xs} →
                Any P xs ↔ P (head xs) ⊎ Any P (tail xs)
Any-head-tail P = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (zero  , p) → inj₁ p
                 ; (suc n , p) → inj₂ (n , p)
                 }
      ; from = λ { (inj₁ p)       → (zero , p)
                 ; (inj₂ (n , p)) → (suc n , p)
                 }
      }
    ; right-inverse-of = λ { (inj₁ p)       → refl _
                           ; (inj₂ (n , p)) → refl _
                           }
    }
  ; left-inverse-of = λ { (zero  , p) → refl _
                        ; (suc n , p) → refl _
                        }
  }

-- Any lemma for cons.

Any-∷ : ∀ {A : Type} (P : A → Type) {x xs} →
        Any P (x ∷ xs) ↔ P x ⊎ Any P xs
Any-∷ P = Any-head-tail P

-- Any lemma for append.
--
-- (TODO: Generalise. The definitions of _++_ and Any-++ in this
-- module are almost identical to those in Container.List.)

Any-++ : ∀ {A : Type} (P : A → Type) (xs : ⟦ List ⟧ A) ys →
         Any P (xs ++ ys) ↔ Any P xs ⊎ Any P ys
Any-++ P xs ys = fold-lemma
  (λ xs xs++ys → Any P xs++ys ↔ Any P xs ⊎ Any P ys)

  (λ us vs us≈vs us++ys hyp →
    Any P us++ys         ↔⟨ hyp ⟩
    Any P us ⊎ Any P ys  ↔⟨ _⇔_.to (∼⇔∼″ us vs) us≈vs P ⊎-cong id ⟩
    Any P vs ⊎ Any P ys  □)

  (Any P ys             ↔⟨ inverse ⊎-left-identity ⟩
   ⊥ ⊎ Any P ys         ↔⟨ inverse (Any-[] P) ⊎-cong id ⟩
   Any P [] ⊎ Any P ys  □)

  (λ x xs xs++ys ih →
     Any P (x ∷ xs++ys)             ↔⟨ Any-∷ P ⟩
     P x ⊎ Any P xs++ys             ↔⟨ id ⊎-cong ih ⟩
     P x ⊎ Any P xs ⊎ Any P ys      ↔⟨ ⊎-assoc ⟩
     (P x ⊎ Any P xs) ⊎ Any P ys    ↔⟨ inverse $ L.Any-∷ P ⊎-cong id ⟩
     Any P (L._∷_ x xs) ⊎ Any P ys  □)

  xs

-- Any lemma for take/drop.

Any-take-drop : ∀ {A : Type} (P : A → Type) n {xs} →
                Any P xs ↔ Any P (take n xs) ⊎ Any P (drop n xs)
Any-take-drop P zero {xs} =
  Any P xs             ↔⟨ inverse ⊎-left-identity ⟩
  ⊥        ⊎ Any P xs  ↔⟨ inverse (Any-[] P) ⊎-cong id ⟩
  Any P [] ⊎ Any P xs  □
Any-take-drop P (suc n) {xs} =
  Any P xs                                                 ↔⟨ Any-head-tail P ⟩
  P (head xs) ⊎ Any P (tail xs)                            ↔⟨ id ⊎-cong Any-take-drop P n ⟩
  P (head xs) ⊎
    (Any P (take n (tail xs)) ⊎ Any P (drop n (tail xs)))  ↔⟨ ⊎-assoc ⟩
  (P (head xs) ⊎ Any P (take n (tail xs))) ⊎
    Any P (drop n (tail xs))                               ↔⟨ inverse $ L.Any-∷ P ⊎-cong id ⟩
  Any P (L._∷_ (head xs) (take n (tail xs))) ⊎
    Any P (drop n (tail xs))                               □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
----------------------------------------------------------------------------------
-- Types for parse trees
----------------------------------------------------------------------------------

module huffman-types where

open import lib
open import parse-tree

posinfo = string
character = string
character-bar-3 = string
character-bar-4 = string
character-bar-5 = string
character-bar-6 = string
character-bar-7 = string
character-range-1 = string
character-range-2 = string
word = string

mutual

  data bvlit : Set where
    BvlitCons : digit → bvlit → bvlit
    BvlitStart : digit → bvlit

  data cmd : Set where
    Decode : codes → bvlit → cmd
    Encode : words → cmd

  data code : Set where
    Code : word → bvlit → code

  data codes : Set where
    CodesNext : code → codes → codes
    CodesStart : code → codes

  data digit : Set where
    One : digit
    Zero : digit

  data start : Set where
    File : cmd → start

  data words : Set where
    WordsNext : word → words → words
    WordsStart : word → words

-- embedded types:

data ParseTreeT : Set where
  parsed-bvlit : bvlit → ParseTreeT
  parsed-cmd : cmd → ParseTreeT
  parsed-code : code → ParseTreeT
  parsed-codes : codes → ParseTreeT
  parsed-digit : digit → ParseTreeT
  parsed-start : start → ParseTreeT
  parsed-words : words → ParseTreeT
  parsed-posinfo : posinfo → ParseTreeT
  parsed-character : character → ParseTreeT
  parsed-character-bar-3 : character-bar-3 → ParseTreeT
  parsed-character-bar-4 : character-bar-4 → ParseTreeT
  parsed-character-bar-5 : character-bar-5 → ParseTreeT
  parsed-character-bar-6 : character-bar-6 → ParseTreeT
  parsed-character-bar-7 : character-bar-7 → ParseTreeT
  parsed-character-range-1 : character-range-1 → ParseTreeT
  parsed-character-range-2 : character-range-2 → ParseTreeT
  parsed-word : word → ParseTreeT
  parsed-aws : ParseTreeT
  parsed-aws-bar-8 : ParseTreeT
  parsed-aws-bar-9 : ParseTreeT
  parsed-ows : ParseTreeT
  parsed-ows-star-11 : ParseTreeT
  parsed-ws : ParseTreeT
  parsed-ws-plus-10 : ParseTreeT

------------------------------------------
-- Parse tree printing functions
------------------------------------------

posinfoToString : posinfo → string
posinfoToString x = "(posinfo " ^ x ^ ")"
characterToString : character → string
characterToString x = "(character " ^ x ^ ")"
character-bar-3ToString : character-bar-3 → string
character-bar-3ToString x = "(character-bar-3 " ^ x ^ ")"
character-bar-4ToString : character-bar-4 → string
character-bar-4ToString x = "(character-bar-4 " ^ x ^ ")"
character-bar-5ToString : character-bar-5 → string
character-bar-5ToString x = "(character-bar-5 " ^ x ^ ")"
character-bar-6ToString : character-bar-6 → string
character-bar-6ToString x = "(character-bar-6 " ^ x ^ ")"
character-bar-7ToString : character-bar-7 → string
character-bar-7ToString x = "(character-bar-7 " ^ x ^ ")"
character-range-1ToString : character-range-1 → string
character-range-1ToString x = "(character-range-1 " ^ x ^ ")"
character-range-2ToString : character-range-2 → string
character-range-2ToString x = "(character-range-2 " ^ x ^ ")"
wordToString : word → string
wordToString x = "(word " ^ x ^ ")"

mutual
  bvlitToString : bvlit → string
  bvlitToString (BvlitCons x0 x1) = "(BvlitCons" ^ " " ^ (digitToString x0) ^ " " ^ (bvlitToString x1) ^ ")"
  bvlitToString (BvlitStart x0) = "(BvlitStart" ^ " " ^ (digitToString x0) ^ ")"

  cmdToString : cmd → string
  cmdToString (Decode x0 x1) = "(Decode" ^ " " ^ (codesToString x0) ^ " " ^ (bvlitToString x1) ^ ")"
  cmdToString (Encode x0) = "(Encode" ^ " " ^ (wordsToString x0) ^ ")"

  codeToString : code → string
  codeToString (Code x0 x1) = "(Code" ^ " " ^ (wordToString x0) ^ " " ^ (bvlitToString x1) ^ ")"

  codesToString : codes → string
  codesToString (CodesNext x0 x1) = "(CodesNext" ^ " " ^ (codeToString x0) ^ " " ^ (codesToString x1) ^ ")"
  codesToString (CodesStart x0) = "(CodesStart" ^ " " ^ (codeToString x0) ^ ")"

  digitToString : digit → string
  digitToString (One) = "One" ^ ""
  digitToString (Zero) = "Zero" ^ ""

  startToString : start → string
  startToString (File x0) = "(File" ^ " " ^ (cmdToString x0) ^ ")"

  wordsToString : words → string
  wordsToString (WordsNext x0 x1) = "(WordsNext" ^ " " ^ (wordToString x0) ^ " " ^ (wordsToString x1) ^ ")"
  wordsToString (WordsStart x0) = "(WordsStart" ^ " " ^ (wordToString x0) ^ ")"

ParseTreeToString : ParseTreeT → string
ParseTreeToString (parsed-bvlit t) = bvlitToString t
ParseTreeToString (parsed-cmd t) = cmdToString t
ParseTreeToString (parsed-code t) = codeToString t
ParseTreeToString (parsed-codes t) = codesToString t
ParseTreeToString (parsed-digit t) = digitToString t
ParseTreeToString (parsed-start t) = startToString t
ParseTreeToString (parsed-words t) = wordsToString t
ParseTreeToString (parsed-posinfo t) = posinfoToString t
ParseTreeToString (parsed-character t) = characterToString t
ParseTreeToString (parsed-character-bar-3 t) = character-bar-3ToString t
ParseTreeToString (parsed-character-bar-4 t) = character-bar-4ToString t
ParseTreeToString (parsed-character-bar-5 t) = character-bar-5ToString t
ParseTreeToString (parsed-character-bar-6 t) = character-bar-6ToString t
ParseTreeToString (parsed-character-bar-7 t) = character-bar-7ToString t
ParseTreeToString (parsed-character-range-1 t) = character-range-1ToString t
ParseTreeToString (parsed-character-range-2 t) = character-range-2ToString t
ParseTreeToString (parsed-word t) = wordToString t
ParseTreeToString parsed-aws = "[aws]"
ParseTreeToString parsed-aws-bar-8 = "[aws-bar-8]"
ParseTreeToString parsed-aws-bar-9 = "[aws-bar-9]"
ParseTreeToString parsed-ows = "[ows]"
ParseTreeToString parsed-ows-star-11 = "[ows-star-11]"
ParseTreeToString parsed-ws = "[ws]"
ParseTreeToString parsed-ws-plus-10 = "[ws-plus-10]"

------------------------------------------
-- Reorganizing rules
------------------------------------------

mutual

  {-# NO_TERMINATION_CHECK #-}
  norm-words : (x : words) → words
  norm-words x = x

  {-# NO_TERMINATION_CHECK #-}
  norm-start : (x : start) → start
  norm-start x = x

  {-# NO_TERMINATION_CHECK #-}
  norm-posinfo : (x : posinfo) → posinfo
  norm-posinfo x = x

  {-# NO_TERMINATION_CHECK #-}
  norm-digit : (x : digit) → digit
  norm-digit x = x

  {-# NO_TERMINATION_CHECK #-}
  norm-codes : (x : codes) → codes
  norm-codes x = x

  {-# NO_TERMINATION_CHECK #-}
  norm-code : (x : code) → code
  norm-code x = x

  {-# NO_TERMINATION_CHECK #-}
  norm-cmd : (x : cmd) → cmd
  norm-cmd x = x

  {-# NO_TERMINATION_CHECK #-}
  norm-bvlit : (x : bvlit) → bvlit
  norm-bvlit x = x

isParseTree : ParseTreeT → 𝕃 char → string → Set
isParseTree p l s = ⊤ {- this will be ignored since we are using simply typed runs -}

ptr : ParseTreeRec
ptr = record { ParseTreeT = ParseTreeT ; isParseTree = isParseTree ; ParseTreeToString = ParseTreeToString }

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-

  Functions building UARels and DUARels on propositions / propositional families

-}
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Displayed.Prop where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Displayed.Base

private
  variable
    ℓA ℓ≅A ℓB ℓ≅B ℓP : Level

𝒮-prop : (P : hProp ℓP) → UARel (P .fst) ℓ-zero
𝒮-prop P .UARel._≅_ _ _ = Unit
𝒮-prop P .UARel.ua _ _ =
  invEquiv (isContr→≃Unit (isOfHLevelPath' 0 (P .snd) _ _))

𝒮ᴰ-prop : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) (P : A → hProp ℓP)
  → DUARel 𝒮-A (λ a → P a .fst) ℓ-zero
𝒮ᴰ-prop 𝒮-A P .DUARel._≅ᴰ⟨_⟩_ _ _ _ = Unit
𝒮ᴰ-prop 𝒮-A P .DUARel.uaᴰ _ _ _ =
  invEquiv (isContr→≃Unit (isOfHLevelPathP' 0 (P _ .snd) _ _))

𝒮-subtype : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) {P : A → Type ℓP}
  → (∀ a → isProp (P a))
  → UARel (Σ A P) ℓ≅A
𝒮-subtype 𝒮-A propP .UARel._≅_ (a , _) (a' , _) = 𝒮-A .UARel._≅_ a a'
𝒮-subtype 𝒮-A propP .UARel.ua (a , _) (a' , _) =
  compEquiv (𝒮-A .UARel.ua a a') (Σ≡PropEquiv propP)

𝒮ᴰ-subtype : {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {P : (a : A) → B a → Type ℓP}
  → (∀ a b → isProp (P a b))
  → DUARel 𝒮-A (λ a → Σ[ b ∈ B a ] (P a b)) ℓ≅B
𝒮ᴰ-subtype 𝒮ᴰ-B propP .DUARel._≅ᴰ⟨_⟩_ (b , _) p (b' , _) = 𝒮ᴰ-B .DUARel._≅ᴰ⟨_⟩_ b p b'
𝒮ᴰ-subtype 𝒮ᴰ-B propP .DUARel.uaᴰ (b , _) p (b' , _) =
  compEquiv
    (𝒮ᴰ-B .DUARel.uaᴰ b p b')
    (compEquiv
      (invEquiv (Σ-contractSnd λ _ → isOfHLevelPathP' 0 (propP _ b') _ _))
      ΣPath≃PathΣ)

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
open import Relation.Binary using (Setoid)

module Data.Vec.Any.Membership {a ℓ} (S : Setoid a ℓ) where
  open import Level using (_⊔_)
  open Setoid S renaming (Carrier to A; refl to ≈-refl; trans to ≈-trans )
  open import Relation.Nullary
  open import Relation.Binary
  open import Data.Fin
  open import Data.Nat as ℕ hiding (_⊔_)
  open import Data.Product as Prod hiding (map)
  open import Data.Vec as Vec hiding (map)
  open import Data.Vec.Equality
  open import Data.Vec.Any as Any
  open import Function using (_∘_; id; flip)
  open Equality S renaming (_≈_ to _≋_; trans to ≋-trans)

  infix 4 _∈′_ _∉′_
  _∈′_ : ∀ {n} → A → Vec A n → Set (a ⊔ ℓ)
  x ∈′ xs = Any (x ≈_) xs

  _∉′_ : ∀ {n} → A → Vec A n → Set (a ⊔ ℓ)
  x ∉′ xs = ¬ (x ∈′ xs)

  infix 4 _⊆_ _⊈_

  _⊆_  : ∀ {n m} → Vec A n → Vec A m → Set _
  xs ⊆ ys = ∀ {x} → x ∈′ xs → x ∈′ ys
  _⊈_  : ∀ {n m} → Vec A n → Vec A m → Set _
  xs ⊈ ys = ¬ (xs ⊆ ys)

  -- A variant of Vec.map.

  map-with-∈′ : ∀ {n b} {B : Set b}
             (xs : Vec A n) → (∀ {x} → x ∈′ xs → B) → Vec B n
  map-with-∈′ []       f = []
  map-with-∈′ (x ∷ xs) f = f (here ≈-refl)  ∷ map-with-∈′ xs (f ∘ there)

  -- Finds an element satisfying the predicate.

  find′ : ∀ {p n} {P : A → Set p} {xs : Vec A n} →
         Any P xs → ∃ λ x → x ∈′ xs × P x
  find′ (here px) = , here ≈-refl  , px
  find′ (there pxs) = Prod.map id (Prod.map there id) (find′ pxs)

  lose′ : ∀ {p n} {P : A → Set p} {x}{xs : Vec A n} →
         P Respects _≈_ → x ∈′ xs → P x → Any P xs
  lose′ resp x∈′xs  px = map (flip resp px) x∈′xs

max_stars_repo_name: tizmd/agda-vector-any

max_issues_repo_name: tizmd/agda-vector-any

max_forks_repo_name: tizmd/agda-vector-any


text:
module CTL.Modalities.AU where

open import CTL.Modalities.AN
open import FStream.Core
open import Library

data _AU'_ {ℓ₁ ℓ₂} {C : Container ℓ₁}
     (props₁ props₂ : FStream' C (Set ℓ₂)) : Set (ℓ₁ ⊔ ℓ₂) where
  finallyA : head props₁ → props₁ AU' props₂
  _untilA_ : head props₂ → AN'ₛ props₁ AU' AN'ₛ props₂ → props₁ AU' props₂

-- TODO Implement with Applicative
AU : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} → FStream C (Set ℓ₂)
   → FStream C (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
AU s₁ s₂ = {!   !}

mutual
  AUₛ' : ∀ {i : Size} {ℓ₁ ℓ₂} {C : Container ℓ₁} → FStream' C (Set ℓ₂)
       → FStream' C (Set ℓ₂) → FStream' {i} C (Set (ℓ₁ ⊔ ℓ₂))
  AUₛ' = {!   !}

  AUₛ : ∀ {i : Size} {ℓ₁ ℓ₂} {C : Container ℓ₁} → FStream C (Set ℓ₂)
      → FStream C (Set ℓ₂) → FStream {i} C (Set (ℓ₁ ⊔ ℓ₂))
  AUₛ = {!   !}

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
{-# OPTIONS --cubical-compatible #-}
module Common.List where

open import Agda.Builtin.List public
open import Common.Nat

infixr 5 _++_

_++_ : ∀ {a} {A : Set a} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map _ []       = []
map f (x ∷ xs) = f x ∷ map f xs

length : ∀ {a} {A : Set a} → List A → Nat
length []       = 0
length (x ∷ xs) = 1 + length xs


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

-- This is unfortunate, but Arch doesn't have the cubical stuff
-- in the stdlib package it comes with (and cabal on Arch is
-- significantly worse).
open import Agda.Builtin.Cubical.Id
open import Agda.Builtin.Cubical.Path

-- Other builtins
open import Agda.Builtin.List
open import Agda.Builtin.Bool

open import Axiom.Extensionality.Propositional

-- I understand it better calling stuff "UU" from Egbert's notes.
open import 00-preamble
-- Same for + types -- too lazy to find the builtin
open import 04-inductive-types

-- https://dl.acm.org/doi/pdf/10.1145/3341691 page 11
-- set quotient (truncate the quotient)
-- ≡ is from Agda.Builtin.Id
data Quot {i : Level} (A : UU i) (R : A → A → UU i): UU i where
  cls : A → Quot A R
  eq : (a b : A) → (r : R a b) → (cls a) ≡ (cls b)
  trunc : (x y : Quot A R) → (p q : x ≡ y) → p ≡ q

-- First definition of a group: List(A + A) / R. Some oddity:
-- 1) f : A → A → Bool is an equality predicate (Eq in Haskell), but I'm not sure how to
--    insist that (f a₁ a₂ = true) ≅ (a₁ = a₂) or just say "if the identity type is
--    inhabited." Also encode-decode seems to use information from the type, so defining
--    f should be a reasonable requirement (it's just code, but using true for 𝟙 and false
--    for 𝟘).
-- 2) I promise it terminates. Otherwise it insists that the first recursive call is
--    uncertain but the list is clearly one element shorter.
-- 3) I think the warning isn't all that important (but I'm a programmer, don't trust me).
--    My understanding is that the warning means "the definitional equalities Agda has can
--    be surprising" but I don't see how it's bad yet.
{-# TERMINATING #-}
cancelList : {i : Level} {A : UU i} (eq : A → A → Bool) (l : List (coprod A A)) → List (coprod A A)
cancelList e [] = []
cancelList e ((inl a₁) ∷ (inr a₂) ∷ xs) with e a₁ a₂
...                                      | true = cancelList e xs
...                                      | false = (inl a₁) ∷ (cancelList e ((inr a₂) ∷ xs))
cancelList e ((inr a₁) ∷ (inl a₂) ∷ xs) with e a₁ a₂
...                                      | true = cancelList e xs
...                                      | false = (inr a₁) ∷ (cancelList e ((inl a₂) ∷ xs))
cancelList e (x ∷ xs) = x ∷ (cancelList e xs)

-- Proof that cancel list is idempotent (done on sets bc why the #$%^ does the built-in
-- funext need a #$%^ing level as an explicit param?)
-- Note that oddity 1 from above is relevant -- I'm just going to be lazy and prove for all
-- equality-like things.
cancelList-idempotent : {A : UU (lsuc lzero)} (e : A → A → Bool)
                        → ((λ x → cancelList e (cancelList e x)) ≡ (cancelList e))
cancelList-idempotent e =

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
-- Andreas, 2012-09-13 respect irrelevance at meta-var creation
-- {-# OPTIONS -v tc.conv.irr:20 #-}
module Issue168-irrelevant where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

module Id .(A : Set) where
  id : Nat → Nat
  id zero     = zero
  id (suc xs) = suc (id xs)
open Id Nat

postulate
  P : Nat → Set
  lemma : ∀ n → P (id n)

foo : P zero
foo = lemma _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda