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

open import HoTT
open import lib.cubical.elims.SuspSmash

module homotopy.SuspProduct where

module SuspProduct {i} {j} (X : Ptd i) (Y : Ptd j) where

  private

    {- into -}

    into-glue : fst (X ⊙× Y) → winl (north _) == winr (winr (north _))
    into-glue (x , y) =
      ap winl (σloop X x) ∙ wglue
      ∙ ap (winr ∘ winl) (σloop (⊙Smash X Y) (cfcod _ (x , y)))
      ∙ ap winr wglue ∙ ap (winr ∘ winr) (σloop Y y)

    into-glue-x : (x : fst X) →
      into-glue (x , snd Y) == ap winl (σloop X x) ∙ wglue ∙ ap winr wglue
    into-glue-x x =
      ap (λ p → ap winl (σloop X x) ∙ wglue ∙ p
                 ∙ ap winr wglue ∙ ap (winr ∘ winr) (σloop Y (snd Y)))
         (ap (ap (winr ∘ winl) ∘ σloop (⊙Smash X Y)) (! (cfglue _ (winl x)))
          ∙ ap (ap (winr ∘ winl)) σloop-pt)
      ∙
      ap (λ q → ap winl (σloop X x) ∙ wglue ∙ ap winr wglue
                ∙ ap (winr ∘ winr) q)
         σloop-pt
      ∙
      ap (λ q → ap winl (σloop X x) ∙ wglue ∙ q) (∙-unit-r _)

    into-glue-y : (y : fst Y) →
      into-glue (snd X , y)
      == wglue ∙ ap winr wglue ∙ ap (winr ∘ winr) (σloop Y y)
    into-glue-y y =
      ap (λ p → ap winl (σloop X (snd X)) ∙ wglue ∙ p
                 ∙ ap winr wglue ∙ ap (winr ∘ winr) (σloop Y y))
         (ap (ap (winr ∘ winl) ∘ σloop (⊙Smash X Y)) (! (cfglue _ (winr y)))
          ∙ ap (ap (winr ∘ winl)) σloop-pt)
      ∙
      ap (λ q → ap winl q ∙ wglue ∙ ap winr wglue
                ∙ ap (winr ∘ winr) (σloop Y y))
         σloop-pt

    into-glue-0 : into-glue (snd X , snd Y) == wglue ∙ ap winr wglue
    into-glue-0 = into-glue-x (snd X)
                  ∙ ap (λ p → ap winl p ∙ wglue ∙ ap winr wglue) σloop-pt

    module Into = SuspensionRec (fst (X ⊙× Y))
      {C = fst (⊙Susp X ⊙∨ (⊙Susp (X ⊙∧ Y) ⊙∨ ⊙Susp Y))}
      (winl (north _))
      (winr (winr (north _)))
      into-glue

    into = Into.f

    {- out -}

    out-× : fst X × fst Y → north _ == north _
    out-× (x , y) = merid _ (snd X , snd Y) ∙ ! (merid _ (x , snd Y))
                    ∙ merid _ (x , y) ∙ ! (merid _ (snd X , y))

    expand₁ : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : z == y)
      → idp == p ∙ ! q ∙ q ∙ ! p
    expand₁ idp idp = idp

    expand₂ : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : x == z)
      → idp == p ∙ ! p ∙ q ∙ ! q
    expand₂ idp idp = idp

    shift : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
      {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
      {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
      → Square p₀₋ p₋₀ p₋₁ p₁₋
      → Square p₀₋ idp p₋₁ (p₋₀ ∙ p₁₋)
    shift ids = ids

    fill : Σ (idp == idp) (λ p →
      Square (expand₁ (merid _ (snd X , snd Y)) (merid _ (snd X , snd Y))) p
             (ap (λ w → out-× (∨-in-× X Y w)) wglue)
             (expand₂ (merid _ (snd X , snd Y)) (merid _ (snd X , snd Y))))
    fill = fill-square-top _ _ _

    module OutSmash = SuspensionRec (Smash X Y)
      (north (fst (X ⊙× Y)))
      (north _)
      (CofiberRec.f _
        idp
        out-×
        (Wedge-elim
          (λ x → expand₁ (merid _ (snd X , snd Y)) (merid _ (x , snd Y)))
          (λ y → fst fill
                 ∙ expand₂ (merid _ (snd X , snd Y)) (merid _ (snd X , y)))
          (↓-cst=app-from-square $ shift (snd fill))))

    module OutWinr = WedgeRec {X = ⊙Susp (X ⊙∧ Y)} {Y = ⊙Susp Y}
      {C = fst (⊙Susp (X ⊙× Y))}
      OutSmash.f
      (susp-fmap (λ y → (snd X , y)))
      idp

    module Out = WedgeRec {X = ⊙Susp X}
      {Y = ⊙Susp (X ⊙∧ Y) ⊙∨ ⊙Susp Y}
      {C = fst (⊙Susp (X ⊙× Y))}
      (susp-fmap (λ x → (x , snd Y)))
      OutWinr.f
      idp

    out = Out.f

    {- into-out -}

    into-out-x : ∀ σx → into (out (winl σx)) == winl σx
    into-out-x = Suspension-elim _
      idp
      (! (ap winl (! (merid _ (snd X))) ∙ wglue ∙ ap winr wglue))
      (λ x → ↓-='-from-square $
        (ap-∘ into (out ∘ winl) (merid _ x)
         ∙ ap (ap into) (SuspFmap.glue-β (λ x → (x , snd Y)) x)
         ∙ Into.glue-β (x , snd Y) ∙ into-glue-x x
         ∙ ap (λ p → p ∙ wglue ∙ ap winr wglue)
              (ap-∙ winl (merid _ x) (! (merid _ (snd X))))
         ∙ ∙-assoc (ap winl (merid _ x)) (ap winl (! (merid _ (snd X))))
                   (wglue ∙ ap winr wglue))
        ∙v⊡ (vid-square {p = ap winl (merid _ x)} ⊡h
             tr-square (ap winl (! (merid _ (snd X))) ∙ wglue ∙ ap winr wglue))
        ⊡v∙ ∙-unit-r _)

    into-out-y : ∀ σy → into (out (winr (winr σy))) == winr (winr σy)
    into-out-y = Suspension-elim _
      (wglue ∙ ap winr wglue)
      (ap (winr ∘ winr) (merid _ (snd Y)))
      (λ y → ↓-='-from-square $
        (ap-∘ into (out ∘ winr ∘ winr) (merid _ y)
         ∙ ap (ap into) (SuspFmap.glue-β (λ y → (snd X , y)) y)
         ∙ Into.glue-β (snd X , y) ∙ into-glue-y y
         ∙ ap (λ p → wglue ∙ ap winr wglue ∙ p)
              (ap-∙ (winr ∘ winr) (merid _ y) (! (merid _ (snd Y)))
               ∙ ap (λ q → ap (winr ∘ winr) (merid _ y) ∙ q)
                    (ap-! (winr ∘ winr) (merid _ (snd Y)))))
        ∙v⊡ lemma wglue (ap winr wglue) (ap (winr ∘ winr) (merid _ y))
                  (ap (winr ∘ winr) (merid _ (snd Y))))
      where
      lemma : ∀ {i} {A : Type i} {a₁ a₂ a₃ a₄ : A}
        (p : a₁ == a₂) (q : a₂ == a₃) (r : a₃ == a₄) (s : a₃ == a₄)
        → Square (p ∙ q) (p ∙ q ∙ r ∙ ! s) r s
      lemma idp idp idp s = disc-to-square (! (!-inv-l s))

    into-out-s : ∀ σs → into (out (winr (winl σs))) == winr (winl σs)
    into-out-s = susp-smash-path-elim _ _
      wglue
      (wglue ∙ ap (winr ∘ winl) (merid _ (cfbase _)))
      (λ {(x , y) →
        (ap-∘ into (out ∘ winr ∘ winl) (merid _ (cfcod _ (x , y)))
         ∙ ap (ap into) (OutSmash.glue-β (cfcod _ (x , y)))
         ∙ lemma₁ into
             (Into.glue-β (snd X , snd Y) ∙ into-glue-0)
             (Into.glue-β (x , snd Y) ∙ into-glue-x x)
             (Into.glue-β (x , y))
             (Into.glue-β (snd X , y) ∙ into-glue-y y))
        ∙v⊡ lemma₂ wglue (ap winr wglue) (ap winl (σloop X x))
                    (ap (winr ∘ winl) (σloop (⊙Smash X Y) (cfcod _ (x , y))))
                    (ap (winr ∘ winr) (σloop Y y))
                    (ap (winr ∘ winl) (merid _ (cfcod _ (x , y))))
                    (ap (winr ∘ winl) (merid _ (cfbase _)))
                    (ap-∙ (winr ∘ winl) (merid _ (cfcod _ (x , y)))
                                        (! (merid _ (cfbase _)))
                     ∙ ap (λ p → ap (winr ∘ winl) (merid _ (cfcod _ (x , y)))
                                 ∙ p)
                          (ap-! (winr ∘ winl) (merid _ (cfbase _))))})
      where
      {- Let's not do these by hand -}
      lemma₁ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
        {a₀ a₁ a₂ a₃ a₄ : A}
        {p : a₀ == a₁} {q : a₂ == a₁} {r : a₂ == a₃} {s : a₄ == a₃}
        {p' : f a₀ == f a₁} {q' : f a₂ == f a₁}
        {r' : f a₂ == f a₃} {s' : f a₄ == f a₃}
        (α : ap f p == p') (β : ap f q == q')
        (γ : ap f r == r') (δ : ap f s == s')
        → ap f (p ∙ ! q ∙ r ∙ ! s) == p' ∙ ! q' ∙ r' ∙ ! s'
      lemma₁ f {p = idp} {q = idp} {r = idp} {s = idp} idp idp idp idp = idp

      lemma₂ : ∀ {i} {A : Type i} {a₀ a₁ a₂ a₃ a₄ a₅ : A}
        (p : a₀ == a₁) (q : a₁ == a₂) (r : a₃ == a₀) (s : a₁ == a₁)
        (t : a₂ == a₄) (u : a₁ == a₅) (v : a₁ == a₅)
        → s == u ∙ ! v
        → Square p ((p ∙ q) ∙ ! (r ∙ p ∙ q) ∙ (r ∙ p ∙ s ∙ q ∙ t)
                    ∙ ! (p ∙ q ∙ t))
                 u (p ∙ v)
      lemma₂ idp idp idp ._ idp idp v idp = disc-to-square $
        ! (ap (λ w → w ∙ v) (∙-unit-r _ ∙ ∙-unit-r (! v)) ∙ !-inv-l v)

    into-out-winr : ∀ r → into (out (winr r)) == winr r
    into-out-winr = Wedge-elim
      into-out-s
      into-out-y
      (↓-='-from-square $
        (ap-∘ into (out ∘ winr) wglue
         ∙ ap (ap into) OutWinr.glue-β)
        ∙v⊡ disc-to-square idp)

    into-out : ∀ w → into (out w) == w
    into-out = Wedge-elim
      into-out-x
      into-out-winr
      (↓-∘=idf-from-square into out $
        ap (ap into) Out.glue-β ∙v⊡ connection)

    out-into-merid : (s : fst (X ⊙× Y))
      → idp == merid _ (snd X , snd Y) [ (λ σ → out (into σ) == σ) ↓ merid _ s ]
    out-into-merid (x , y) = ↓-∘=idf-from-square out into $
      (ap (ap out) (Into.glue-β (x , y))
        ∙ lemma₁ out
            (∘-ap out winl (σloop X x)
             ∙ ap-∙ (out ∘ winl) (merid _ x) (! (merid _ (snd X)))
             ∙ SuspFmap.glue-β (λ x → (x , snd Y)) x
               ∙2 (ap-! (out ∘ winl) (merid _ (snd X))
                   ∙ ap ! (SuspFmap.glue-β (λ x → (x , snd Y)) (snd X))))
            Out.glue-β
            (∘-ap out (winr ∘ winl) (σloop _ (cfcod _ (x , y)))
             ∙ ap-∙ OutSmash.f (merid _ (cfcod _ (x , y)))
                               (! (merid _ (cfbase _)))
             ∙ OutSmash.glue-β (cfcod _ (x , y))
               ∙2 (ap-! OutSmash.f (merid _ (cfbase _))
                   ∙ ap ! (OutSmash.glue-β (cfbase _))))
            (∘-ap out winr wglue ∙ OutWinr.glue-β)
            (∘-ap out (winr ∘ winr) (σloop Y y)
             ∙ ap-∙ (out ∘ winr ∘ winr) (merid _ y) (! (merid _ (snd Y)))
             ∙ SuspFmap.glue-β (λ y → (snd X , y)) y
               ∙2 (ap-! (out ∘ winr ∘ winr) (merid _ (snd Y))
                   ∙ ap ! (SuspFmap.glue-β (λ y → (snd X , y)) (snd Y)))))
      ∙v⊡ lemma₂ (merid _ (x , snd Y)) (merid _ (snd X , snd Y))
                  (merid _ (x , y)) (merid _ (snd X , y))
                  (merid _ (snd X , snd Y))
      where
      lemma₁ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
        {a₀ a₁ a₂ a₃ a₄ a₅ : A}
        {p : a₀ == a₁} {q : a₁ == a₂} {r : a₂ == a₃}
        {s : a₃ == a₄} {t : a₄ == a₅}
        {p' : f a₀ == f a₁} {q' : f a₁ == f a₂} {r' : f a₂ == f a₃}
        {s' : f a₃ == f a₄} {t' : f a₄ == f a₅}
        (α : ap f p == p') (β : ap f q == q') (γ : ap f r == r')
        (δ : ap f s == s') (ε : ap f t == t')
        → ap f (p ∙ q ∙ r ∙ s ∙ t) == p' ∙ q' ∙ r' ∙ s' ∙ t'
      lemma₁ f {p = idp} {q = idp} {r = idp} {s = idp} {t = idp}
        idp idp idp idp idp = idp

      lemma₂ : ∀ {i} {A : Type i} {a₀ a₁ a₂ a₃ a₄ a₅ : A}
        (p : a₀ == a₁) (q : a₂ == a₁) (r : a₀ == a₃)
        (s : a₄ == a₃) (t : a₅ == a₃)
        → Square idp ((p ∙ ! q) ∙ ((q ∙ ! p ∙ r ∙ ! s) ∙ idp) ∙ (s ∙ ! t)) r t
      lemma₂ idp idp idp idp idp = ids

    out-into : ∀ σ → out (into σ) == σ
    out-into = Suspension-elim _
      idp
      (merid _ (snd X , snd Y))
      out-into-merid

  abstract
    eq : fst (⊙Susp (X ⊙× Y)) ≃ fst (⊙Susp X ⊙∨ (⊙Susp (X ⊙∧ Y) ⊙∨ ⊙Susp Y))
    eq = equiv into out into-out out-into

    ⊙path : ⊙Susp (X ⊙× Y) == ⊙Susp X ⊙∨ (⊙Susp (X ⊙∧ Y) ⊙∨ ⊙Susp Y)
    ⊙path = ⊙ua eq idp

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
-- Adapted from an example reported by John Leon

-- It seems that the change reported in the issue was caused by the
-- commit 344296cf06cedd13736e50bb53e63217d9f19ecf.

-- Using `C-c C-,` in the first goal, master and 2.4.2.5 have different
-- behaviours. In master, the type of `a` is not normalised

-- Goal: n ≡ n + zero
-- ————————————————————————————————————————————————————————————
-- a : flip _≡_ (n + zero) n
-- n : ℕ

-- but in 2.4.2.5, the type of `a` is full normalised

-- Goal: n ≡ n + zero
-- ————————————————————————————————————————————————————————————
-- a : n ≡ n + 0
-- n : ℕ

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

cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

REL : Set → Set → Set₁
REL A B = A → B → Set

flip : {A B : Set} {C : A → B → Set₁} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y

infixr 4 _⇒_
_⇒_ : {A B : Set} → REL A B → REL A B → Set
P ⇒ Q = ∀ {i j} → P i j → Q i j

Sym : {A B : Set} → REL A B → REL B A → Set
Sym P Q = P ⇒ flip Q

Symmetric : {A : Set} → REL A A → Set
Symmetric _∼_ = Sym _∼_ _∼_

sym : {A : Set} → Symmetric (_≡_ {A = A})
sym refl = refl

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
zero  + m = m
suc n + m = suc (n + m)

n+0=n : (n : ℕ) → n + zero ≡ n
n+0=n zero    = refl
n+0=n (suc n) = cong suc (n+0=n (n))

m+Sn : (m n : ℕ) → m + suc n ≡ suc (m + n)
m+Sn zero    n = refl
m+Sn (suc m) n = cong suc (m+Sn m n)

+comm : (m n : ℕ) → m + n ≡ n + m
+comm zero    n =
  let a = sym (n+0=n n)
  in {!!}
+comm (suc m) n =
  let a = cong suc (+comm m n)
      b = sym (m+Sn n m)
  in {!!}

ext: agda


text:
{-

    Interactive Programming with Dependent Types

                      Ulf Norell

                  ICFP 2013, Boston

 -}

module ICFP where

open import ICFPPrelude

data Type : Set where
  nat : Type
  _⇒_ : (a b : Type) → Type

infixr 7 _⇒_

data Raw : Set where
  var : (n : Nat) → Raw
  app : (e₁ e₂ : Raw) → Raw
  lam : (a : Type) (e : Raw) → Raw

data Cxt : Set where
  [] : Cxt
  _,_ : (Γ : Cxt) (a : Type) → Cxt

data Var : Cxt → Type → Set where
  zero : ∀ {Γ a} → Var (Γ , a) a
  suc  : ∀ {Γ a b} → Var Γ a → Var (Γ , b) a

data Term : Cxt → Type → Set where
  var : ∀ {Γ a} → Var Γ a → Term Γ a
  app : ∀ {Γ a b} (u : Term Γ (a ⇒ b)) (v : Term Γ a) →
        Term Γ b
  lam : ∀ {Γ} a {b} (u : Term (Γ , a) b) → Term Γ (a ⇒ b)

eraseVar : ∀ {Γ a} → Var Γ a → Nat
eraseVar zero = zero
eraseVar (suc x) = suc (eraseVar x)

erase : ∀ {Γ a} → Term Γ a → Raw
erase (var x) = var (eraseVar x)
erase (app v v₁) = app (erase v) (erase v₁)
erase (lam a v) = lam a (erase v)

data _≠_ : Type → Type → Set where
  nat≠fun : ∀ {a b} → nat ≠ a ⇒ b
  fun≠nat : ∀ {a b} → a ⇒ b ≠ nat
  src≠    : ∀ {a a′ b c} → a ≠ a′ → a ⇒ b ≠ a′ ⇒ c
  tgt≠    : ∀ {a b c c′} → c ≠ c′ → a ⇒ c ≠ b ⇒ c′

sound : ∀ a → a ≠ a → ⊥
sound nat ()
sound (a ⇒ b) (src≠ x) = sound a x
sound (a ⇒ b) (tgt≠ x) = sound b x

infix 4 _≠_ _≟_

data _≟_ : Type → Type → Set where
  equal : ∀ {a} → a ≟ a
  not-equal : ∀ {a b} → a ≠ b → a ≟ b

compareFun : ∀ {a b c d} → a ≟ b → c ≟ d → a ⇒ c ≟ b ⇒ d
compareFun equal equal = equal
compareFun equal (not-equal x) = not-equal (tgt≠ x)
compareFun (not-equal x) q = not-equal (src≠ x)

compare : ∀ a b → a ≟ b
compare nat nat = equal
compare nat (a ⇒ b) = not-equal nat≠fun
compare (a ⇒ b) nat = not-equal fun≠nat
compare (a ⇒ b) (a₁ ⇒ b₁) = compareFun (compare a a₁) (compare b b₁)

data OutOfScope : Cxt → Nat → Set where
  oops : ∀ {n} → OutOfScope [] n
  suc  : ∀ {Γ a n} → OutOfScope Γ n → OutOfScope (Γ , a) (suc n)

data WellScoped? : Cxt → Nat → Set where
  yes : ∀ {Γ} a (x : Var Γ a) → WellScoped? Γ (eraseVar x)
  no  : ∀ {Γ n} → OutOfScope Γ n → WellScoped? Γ n

data TypeError : Cxt → Raw → Set where
  arg-mismatch : ∀ {a a′ Γ b} {u : Term Γ (a ⇒ b)} {u₁ : Term Γ a′} →
                 a ≠ a′ → TypeError Γ (app (erase u) (erase u₁))
  not-fun : ∀ {Γ} {u : Term Γ nat} {a₁} {u₁ : Term Γ a₁} →
            TypeError Γ (app (erase u) (erase u₁))
  bad-arg : ∀ {Γ e₂ e₁} → TypeError Γ e₂ → TypeError Γ (app e₁ e₂)
  bad-fun : ∀ {Γ e₁ e₂} → TypeError Γ e₁ → TypeError Γ (app e₁ e₂)
  out-of-scope : ∀ {Γ n} → OutOfScope Γ n → TypeError Γ (var n)
  lam : ∀ {Γ e} a → TypeError (Γ , a) e → TypeError Γ (lam a e)

data WellTyped? : Cxt → Raw → Set where
  yes : ∀ {Γ} a (u : Term Γ a) → WellTyped? Γ (erase u)
  no  : ∀ {Γ e} (err : TypeError Γ e) → WellTyped? Γ e

checkApp : ∀ {Γ e₁ e₂} → WellTyped? Γ e₁ → WellTyped? Γ e₂ →
             WellTyped? Γ (app e₁ e₂)
checkApp (yes nat u) (yes a₁ u₁) = no not-fun
checkApp (yes (a ⇒ b) u) (yes a′ u₁) with compare a a′
checkApp (yes (a ⇒ b) u) (yes .a u₁) | equal         = yes b (app u u₁)
checkApp (yes (a ⇒ b) u) (yes a′ u₁) | not-equal err = no (arg-mismatch err)
checkApp (yes a u) (no err) = no (bad-arg err)
checkApp (no err) (yes a u) = no (bad-fun err)
checkApp (no err) (no err₁) = no (bad-arg err₁)

lookupSuc : ∀ {Γ a n} →
            WellScoped? Γ n → WellScoped? (Γ , a) (suc n)
lookupSuc (yes a₁ x) = yes a₁ (suc x)
lookupSuc (no x) = no (suc x)

lookupVar : ∀ Γ n → WellScoped? Γ n
lookupVar [] n = no oops
lookupVar (Γ , a) zero = yes a zero
lookupVar (Γ , a) (suc n) = lookupSuc (lookupVar Γ n)

checkVar : ∀ {Γ n} → WellScoped? Γ n → WellTyped? Γ (var n)
checkVar (yes a x) = yes a (var x)
checkVar (no x) = no (out-of-scope x)

checkLam : ∀ {Γ e} a → WellTyped? (Γ , a) e → WellTyped? Γ (lam a e)
checkLam a (yes a₁ u) = yes (a ⇒ a₁) (lam a u)
checkLam a (no err) = no (lam a err)

check : ∀ Γ e → WellTyped? Γ e
check Γ (var n) = checkVar (lookupVar Γ n)
check Γ (app e₁ e₂) = checkApp (check Γ e₁) (check Γ e₂)
check Γ (lam a e) = checkLam a (check (Γ , a) e)

max_stars_repo_name: enlambdment/disco

max_issues_repo_name: enlambdment/disco

max_forks_repo_name: enlambdment/disco


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Simply-typed changes with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Change.Type where

open import Nehemiah.Syntax.Type

import Parametric.Change.Type Base as ChangeType

ΔBase : ChangeType.Structure
ΔBase base-int = base base-int
ΔBase base-bag = base base-bag

open ChangeType.Structure ΔBase public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Class.Functor where

open import Category.Functor using () renaming (RawFunctor to Functor) public

open Functor {{...}} public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
-- Andreas, 2019-06-18, LAIM 2019, issue #3855:
-- Successful tests for the erasure (@0) modality.

module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Coinduction

open import Common.IO

module WhereInErasedDeclaration where

  @0 n : Nat
  n = 4711

  @0 m : Nat
  m = n'
    where
    n' = n

module ErasedDeclarationInWhere where

  F : (G : @0 Set → Set) (@0 A : Set) → Set
  F G A = G B
    where
    @0 B : Set
    B = A

module FlatErasure where

  @0 resurrect-λ : (A : Set) (@0 x : A) → A
  resurrect-λ A = λ x → x

  @0 resurrect-λ-where : (A : Set) (@0 x : A) → A
  resurrect-λ-where A = λ where x → x

  @0 resurrect-app : (A : Set) (@0 x : A) → A
  resurrect-app A x = x

module ErasedEquality where

  -- Should maybe not work --without-K
  -- should definitely not work in --cubical

  cast : ∀{A B : Set} → @0 A ≡ B → A → B
  cast refl x = x

  J : ∀{A : Set} {a : A} (P : (x : A) → a ≡ x → Set) {b : A}
      (@0 eq : a ≡ b) → P a refl → P b eq
  J P refl p = p

module ParametersAreErased where

  test : (@0 A : Set) → A ≡ A
  test A = refl {x = _}           -- TODO: A instead of _

module Records where

  record R (A : Set) : Set where
    field
      el : A
    Par : Set
    Par = A    -- record module parameters are NOT erased, so, this should be accepted

  proj : (A : Set) → R A → A  -- TODO: @0 A instead of A
  proj A r = R.el {A = _} r

  MyPar : (A : Set) → R A → Set
  MyPar A = R.Par {A = A}

  record RB (b : Bool) : Set where
    bPar : Bool
    bPar = b

  myBPar : (b : Bool) → RB b → Bool
  myBPar b r = RB.bPar {b = b} r

module CoinductionWithErasure (A : Set) where

  data Stream : Set where
    cons : (x : A) (xs : ∞ Stream) → Stream

  @0 repeat : (@0 a : A) → Stream
  repeat a = cons a (♯ (repeat a))

main = putStrLn "Hello, world!"

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module PiQ.Interp where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Data.Nat hiding (_≟_)
open import Data.List as L hiding (_∷_)
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import PiQ.Syntax
open import PiQ.Opsem
open import PiQ.Eval

{-# TERMINATING #-}
mutual
  interp : {A B : 𝕌} → (A ↔ B) → Val A B → Maybe (Val B A)
  -- Forward
  interp unite₊l (inj₂ y ⃗)        = just (y ⃗)
  interp uniti₊l (v ⃗)             = just (inj₂ v ⃗)
  interp swap₊   (inj₁ x ⃗)        = just (inj₂ x ⃗)
  interp swap₊   (inj₂ y ⃗)        = just (inj₁ y ⃗)
  interp assocl₊ (inj₁ x ⃗)        = just (inj₁ (inj₁ x) ⃗)
  interp assocl₊ (inj₂ (inj₁ y) ⃗) = just (inj₁ (inj₂ y) ⃗)
  interp assocl₊ (inj₂ (inj₂ z) ⃗) = just (inj₂ z ⃗)
  interp assocr₊ (inj₁ (inj₁ x) ⃗) = just (inj₁ x ⃗)
  interp assocr₊ (inj₁ (inj₂ y) ⃗) = just (inj₂ (inj₁ y) ⃗)
  interp assocr₊ (inj₂ z ⃗)        = just (inj₂ (inj₂ z) ⃗)
  interp unite⋆l ((tt , v) ⃗)      = just (v ⃗)
  interp uniti⋆l (v ⃗)             = just ((tt , v) ⃗)
  interp swap⋆   ((x , y) ⃗)       = just ((y , x) ⃗)
  interp assocl⋆ ((x , (y , z)) ⃗) = just (((x , y) , z) ⃗)
  interp assocr⋆ (((x , y) , z) ⃗) = just ((x , y , z) ⃗)
  interp dist    ((inj₁ x , z) ⃗)  = just (inj₁ (x , z) ⃗)
  interp dist    ((inj₂ y , z) ⃗)  = just (inj₂ (y , z) ⃗)
  interp factor  (inj₁ (x , z) ⃗)  = just ((inj₁ x , z) ⃗)
  interp factor  (inj₂ (y , z) ⃗)  = just ((inj₂ y , z) ⃗)
  interp id↔     (v ⃗)             = just (v ⃗)
  interp (c₁ ⨾ c₂) (v ⃗) = interp c₁ (v ⃗) >>=
                           λ {(v' ⃖) → just (v' ⃖) ;
                              (v' ⃗) → c₁ ⨾[ v' ⃗]⨾ c₂}
  interp (c₁ ⊕ c₂) (inj₁ x ⃗) = interp c₁ (x ⃗) >>=
                                λ {(x' ⃗) → just (inj₁ x' ⃗) ;
                                  (x' ⃖) → just (inj₁ x' ⃖)}
  interp (c₁ ⊕ c₂) (inj₂ y ⃗) = interp c₂ (y ⃗) >>=
                                λ {(y' ⃗) → just (inj₂ y' ⃗) ;
                                  (y' ⃖) → just (inj₂ y' ⃖)}
  interp (c₁ ⊗ c₂) ((x , y) ⃗) = interp c₁ (x ⃗) >>=
                                 λ {(x' ⃖) → just ((x' , y) ⃖) ;
                                   (x' ⃗) → interp c₂ (y ⃗) >>=
                                            λ {(y' ⃗) → just ((x' , y') ⃗) ;
                                               (y' ⃖) → just ((x , y') ⃖)}}
  interp ε₊      (inj₁ v ⃗)     = just (inj₂ (- v) ⃖)
  interp ε₊      (inj₂ (- v) ⃗) = just (inj₁ v ⃖)
  interp (ηₓ v)  (tt ⃗)         = just ((v , ↻) ⃗)
  interp (εₓ v)  ((v' , ↻) ⃗) with v ≟ v'
  ... | yes _ = just (tt ⃗)
  ... | no  _ = nothing
  -- Backward
  interp unite₊l (v ⃖)             = just (inj₂ v ⃖)
  interp uniti₊l (inj₂ v ⃖)        = just (v ⃖)
  interp swap₊   (inj₁ x ⃖)        = just (inj₂ x ⃖)
  interp swap₊   (inj₂ y ⃖)        = just (inj₁ y ⃖)
  interp assocl₊ (inj₁ (inj₁ x) ⃖) = just (inj₁ x ⃖)
  interp assocl₊ (inj₁ (inj₂ y) ⃖) = just (inj₂ (inj₁ y) ⃖)
  interp assocl₊ (inj₂ z ⃖)        = just (inj₂ (inj₂ z) ⃖)
  interp assocr₊ (inj₁ x ⃖)        = just (inj₁ (inj₁ x) ⃖)
  interp assocr₊ (inj₂ (inj₁ y) ⃖) = just (inj₁ (inj₂ y) ⃖)
  interp assocr₊ (inj₂ (inj₂ z) ⃖) = just (inj₂ z ⃖)
  interp unite⋆l (v ⃖)             = just ((tt , v) ⃖)
  interp uniti⋆l ((tt , v) ⃖)      = just (v ⃖)
  interp swap⋆   ((x , y) ⃖)       = just ((y , x) ⃖)
  interp assocl⋆ (((x , y) , z) ⃖) = just ((x , (y , z)) ⃖)
  interp assocr⋆ ((x , (y , z)) ⃖) = just (((x , y) , z) ⃖)
  interp dist    (inj₁ (x , z) ⃖)  = just ((inj₁ x , z) ⃖)
  interp dist    (inj₂ (y , z) ⃖)  = just ((inj₂ y , z) ⃖)
  interp factor  ((inj₁ x , z) ⃖)  = just (inj₁ (x , z) ⃖)
  interp factor  ((inj₂ y , z) ⃖)  = just (inj₂ (y , z) ⃖)
  interp id↔ (v ⃖) = just (v ⃖)
  interp (c₁ ⨾ c₂) (v ⃖) = interp c₂ (v ⃖) >>=
                           λ {(v' ⃗) → just (v' ⃗) ;
                              (v' ⃖) → c₁ ⨾[ v' ⃖]⨾ c₂}
  interp (c₁ ⊕ c₂) (inj₁ x ⃖) = interp c₁ (x ⃖) >>=
                                λ {(x' ⃖) → just (inj₁ x' ⃖) ;
                                  (x' ⃗) → just (inj₁ x' ⃗)}
  interp (c₁ ⊕ c₂) (inj₂ y ⃖) = interp c₂ (y ⃖) >>=
                                λ {(y' ⃖) → just (inj₂ y' ⃖) ;
                                  (y' ⃗) → just (inj₂ y' ⃗)}
  interp (c₁ ⊗ c₂) ((x , y) ⃖) = interp c₂ (y ⃖) >>=
                                 λ {(y' ⃗) → just ((x , y') ⃗) ;
                                    (y' ⃖) → interp c₁ (x ⃖) >>=
                                            λ {(x' ⃖) → just ((x' , y') ⃖) ;
                                               (x' ⃗) → just ((x' , y) ⃗)}}
  interp η₊     (inj₁ v ⃖)     = just (inj₂ (- v) ⃗)
  interp η₊     (inj₂ (- v) ⃖) = just (inj₁ v ⃗)
  interp (εₓ v) (tt ⃖)         = just ((v , ↻) ⃖)
  interp (ηₓ v) ((v' , ↻) ⃖) with v ≟ v'
  ... | yes _ = just (tt ⃖)
  ... | no  _ = nothing

  _⨾[_⃗]⨾_ : ∀ {A B C} → (A ↔ B) → ⟦ B ⟧ → (B ↔ C) → Maybe (Val C A)
  c₁ ⨾[ b ⃗]⨾ c₂ = interp c₂ (b ⃗) >>=
                   λ {(c ⃗)  → just (c ⃗) ;
                      (b' ⃖) → c₁ ⨾[ b' ⃖]⨾ c₂}

  _⨾[_⃖]⨾_ : ∀ {A B C} → (A ↔ B) → ⟦ B ⟧ → (B ↔ C) → Maybe (Val C A)
  c₁ ⨾[ b ⃖]⨾ c₂ = interp c₁ (b ⃖) >>=
                   λ {(a  ⃖) → just (a ⃖) ;
                      (b' ⃗) → c₁ ⨾[ b' ⃗]⨾ c₂}


text:
import cedille-options

module interactive-cmds (options : cedille-options.options) where

open import functions
open import cedille-types
open import conversion
open import constants
open import ctxt
open import general-util
open import spans options {Id}
open import subst
open import syntax-util
open import type-util
open import to-string options
open import toplevel-state options {IO}
open import untyped-spans options {Id}
open import parser
open import resugar
open import rewriting
open import rename
open import classify options {Id} (λ _ → return triv)
import spans options {IO} as io-spans
open import datatype-util
open import free-vars
open import json

private

  elab-typed-err : ∀ {ed} → ctxt → ⟦ ed ⟧' → ⟦ ed ⟧ × 𝔹
  elab-typed-err {TERM} Γ t =
    map-snd spans-have-error $ map-fst fst $ id-out $ check-term Γ t nothing empty-spans
  elab-typed-err {TYPE} Γ T =
    map-snd spans-have-error $ map-fst fst $ id-out $ check-type Γ T nothing empty-spans
  elab-typed-err {KIND} Γ k =
    map-snd spans-have-error $ id-out $ check-kind Γ k empty-spans

  elab-typed : ∀ {ed} → ctxt → ⟦ ed ⟧' → ⟦ ed ⟧
  elab-typed Γ = fst ∘ elab-typed-err Γ

  elab-untyped : ∀ {ed} → ctxt → ⟦ ed ⟧' → ⟦ ed ⟧
  elab-untyped {TERM} Γ t = fst $ id-out $ untyped-term Γ t empty-spans
  elab-untyped {TYPE} Γ T = fst $ id-out $ untyped-type Γ T empty-spans
  elab-untyped {KIND} Γ k = fst $ id-out $ untyped-kind Γ k empty-spans

  elab-untyped-no-params : ∀ {ed} → ctxt → ⟦ ed ⟧' → ⟦ ed ⟧
  elab-untyped-no-params Γ =
    elab-untyped (record Γ {qual = trie-map (map-snd λ _ → []) (ctxt.qual Γ)})

  {- Parsing -}

  ll-ind : ∀ {X : exprd → Set} → X TERM → X TYPE → X KIND → (ll : exprd) → X ll
  ll-ind t T k TERM = t
  ll-ind t T k TYPE = T
  ll-ind t T k KIND = k

  ll-ind' : ∀ {X : Σ exprd ⟦_⟧ → Set} → (s : Σ exprd ⟦_⟧) → ((t : term) → X (TERM , t)) → ((T : type) → X (TYPE , T)) → ((k : kind) → X (KIND , k)) → X s
  ll-ind' (TERM , t) tf Tf kf = tf t
  ll-ind' (TYPE , T) tf Tf kf = Tf T
  ll-ind' (KIND , k) tf Tf kf = kf k

  ll-disambiguate : ctxt → ex-tm → maybe ex-tp
  ll-disambiguate Γ (ExVar pi x) = ctxt-lookup-type-var Γ x >>= λ _ → just (ExTpVar pi x)
  ll-disambiguate Γ (ExApp t NotErased t') = ll-disambiguate Γ t >>= λ T →
    just (ExTpAppt T t')
  ll-disambiguate Γ (ExAppTp t T') = ll-disambiguate Γ t >>= λ T → just (ExTpApp T T')
  ll-disambiguate Γ (ExLam pi ff pi' x (just atk) t) =
    ll-disambiguate (ctxt-tk-decl pi' x (case atk of λ {(ExTkt _) → Tkt (TpHole pi'); (ExTkk _) → Tkk KdStar}) Γ) t >>= λ T →
    just (ExTpLam pi pi' x atk T)
  ll-disambiguate Γ (ExParens pi t pi') = ll-disambiguate Γ t
  ll-disambiguate Γ (ExLet pi _ d t) =
    ll-disambiguate (Γ' d) t >>= λ T → just (ExTpLet pi d T)
    where
    Γ' : ex-def → ctxt
    Γ' (ExDefTerm pi' x T? t) = ctxt-term-def pi' localScope opacity-open x (just (Hole pi')) (TpHole pi') Γ
    Γ' (ExDefType pi' x k T) = ctxt-type-def pi' localScope opacity-open x (just (TpHole pi')) KdStar Γ
  ll-disambiguate Γ t = nothing

  parse-string : (ll : exprd) → string → maybe ⟦ ll ⟧'
  parse-string ll s = case ll-ind {λ ll → string → Either string ⟦ ll ⟧'}
    parseTerm parseType parseKind ll s of λ {(Left e) → nothing; (Right e) → just e}

  ttk = "term, type, or kind"

  parse-err-msg : (failed-to-parse : string) → (as-a : string) → string
  parse-err-msg failed-to-parse "" =
    "Failed to parse \\\\\"" ^ failed-to-parse ^ "\\\\\""
  parse-err-msg failed-to-parse as-a =
    "Failed to parse \\\\\"" ^ failed-to-parse ^ "\\\\\" as a " ^ as-a

  infixr 7 _>>nothing_ _-_!_>>parse_ _!_>>error_
  _>>nothing_ : ∀{ℓ}{A : Set ℓ} → maybe A → maybe A → maybe A
  (nothing >>nothing m₂) = m₂
  (m₁ >>nothing m₂) = m₁

  _-_!_>>parse_ : ∀{A B : Set} → (string → maybe A) → string →
                  (error-msg : string) → (A → string ⊎ B) → string ⊎ B
  (f - s ! e >>parse f') = maybe-else (inj₁ (parse-err-msg s e)) f' (f s)

  _!_>>error_ : ∀{E A B : Set} → maybe A → E → (A → E ⊎ B) → E ⊎ B
  (just a ! e >>error f) = f a
  (nothing ! e >>error f) = inj₁ e

  parse-try : ∀ {X : Set} → ctxt → string → maybe
                (((ll : exprd) → ⟦ ll ⟧' → X) → X)
  parse-try Γ s =
    maybe-map (λ t f → maybe-else (f TERM t) (f TYPE) (ll-disambiguate Γ t))
      (parse-string TERM s) >>nothing
    maybe-map (λ T f → f TYPE T) (parse-string TYPE s) >>nothing
    maybe-map (λ k f → f KIND k) (parse-string KIND s)

  string-to-𝔹 : string → maybe 𝔹
  string-to-𝔹 "tt" = just tt
  string-to-𝔹 "ff" = just ff
  string-to-𝔹 _ = nothing

  parse-ll : string → maybe exprd
  parse-ll "term" = just TERM
  parse-ll "type" = just TYPE
  parse-ll "kind" = just KIND
  parse-ll _ = nothing

  {- Local Context -}

  record lci : Set where
    constructor mk-lci
    field ll : string; x : var; t : string; T : string; fn : string; pi : posinfo

  data 𝕃ₛ {ℓ} (A : Set ℓ) : Set ℓ where
    [_]ₛ : A → 𝕃ₛ A
    _::ₛ_ : A → 𝕃ₛ A → 𝕃ₛ A

  headₛ : ∀ {ℓ} {A : Set ℓ} → 𝕃ₛ A → A
  headₛ [ a ]ₛ = a
  headₛ (a ::ₛ as) = a

  𝕃ₛ-to-𝕃 : ∀ {ℓ} {A : Set ℓ} → 𝕃ₛ A → 𝕃 A
  𝕃ₛ-to-𝕃 [ a ]ₛ = [ a ]
  𝕃ₛ-to-𝕃 (a ::ₛ as) = a :: 𝕃ₛ-to-𝕃 as

  merge-lcis-ctxt-tvs : ctxt → 𝕃 string → ctxt × 𝕃 tagged-val
  merge-lcis-ctxt-tvs c =
    foldl merge-lcis-ctxt' (c , [])
      ∘ (sort-lcis ∘ strings-to-lcis)
    where
    strings-to-lcis : 𝕃 string → 𝕃 lci
    strings-to-lcis ss = strings-to-lcis-h ss [] where
      strings-to-lcis-h : 𝕃 string → 𝕃 lci → 𝕃 lci
      strings-to-lcis-h (ll :: x :: t :: T :: fn :: pi :: tl) items =
        strings-to-lcis-h tl (mk-lci ll x t T fn pi :: items)
      strings-to-lcis-h _ items = items

    -- TODO: Local context information does not pass Δ information!
    -- When users are using BR-explorer to rewrite with the rec function,
    -- if they call it upon "μ' [SUBTERM] {...}", it won't work unless they say
    -- "μ'<rec/mu> [SUBTERM] {...}".
    decl-lci : posinfo → var → ctxt → ctxt
    decl-lci pi x Γ =
      record Γ { qual = trie-insert (ctxt.qual Γ) x (pi % x , []) }

    exprd-type-of : exprd → exprd
    exprd-type-of TERM = TYPE
    exprd-type-of _ = KIND

    merge-lci-ctxt : lci → ctxt × 𝕃 tagged-val → ctxt × 𝕃 tagged-val
    merge-lci-ctxt (mk-lci ll v t T fn pi) (Γ , tvs) =
      maybe-else (Γ , tvs) (map-snd (λ tv → tvs ++ [ tv ]))
        (parse-ll ll >>= λ ll →
         parse-string (exprd-type-of ll) T >>=
         h ll (parse-string ll t))
      where
      h : (ll : exprd) → maybe ⟦ ll ⟧' → ⟦ exprd-type-of ll ⟧' → maybe (ctxt × tagged-val)
      h TERM (just t) T =
        let t = elab-untyped Γ t
            T = elab-typed Γ T in
        return2 (ctxt-term-def pi localScope opacity-open v (just t) T Γ)
                (binder-data Γ pi v (Tkt T) ff (just t) "0" "0")
      h TYPE (just T) k =
        let T = elab-untyped Γ T
            k = elab-typed Γ k in
        return2 (ctxt-type-def pi localScope opacity-open v (just T) k Γ)
                (binder-data Γ pi v (Tkk k) ff (just T) "0" "0")
      h TERM nothing T =
        let T = elab-typed Γ T in
        return2 (ctxt-term-decl pi v T Γ)
                (binder-data Γ pi v (Tkt T) ff nothing "0" "0")
      h TYPE nothing k =
        let k = elab-typed Γ k in
        return2 (ctxt-type-decl pi v k Γ)
                (binder-data Γ pi v (Tkk k) ff nothing "0" "0")
      h _ _ _ = nothing

    merge-lcis-ctxt' : 𝕃ₛ lci → ctxt × 𝕃 tagged-val → ctxt × 𝕃 tagged-val
    merge-lcis-ctxt' ls (Γ , tvs) =
      let ls' = 𝕃ₛ-to-𝕃 ls in
      foldr merge-lci-ctxt (foldr (λ l → decl-lci (lci.pi l) (lci.x l)) Γ ls' , tvs) ls'

    sort-eq : ∀ {ℓ} {A : Set ℓ} → (A → A → compare-t) → 𝕃 A → 𝕃 (𝕃ₛ A)
    sort-eq {_} {A} c = foldr insert [] where
      insert : A → 𝕃 (𝕃ₛ A) → 𝕃 (𝕃ₛ A)
      insert n [] = [ [ n ]ₛ ]
      insert n (a :: as) with c (headₛ a) n
      ...| compare-eq = n ::ₛ a :: as
      ...| compare-gt = [ n ]ₛ :: a :: as
      ...| compare-lt = a :: insert n as

    sort-lcis : 𝕃 lci → 𝕃 (𝕃ₛ lci)
    sort-lcis = sort-eq λ l₁ l₂ →
      compare (posinfo-to-ℕ $ lci.pi l₁) (posinfo-to-ℕ $ lci.pi l₂)
    {-
    sort-lcis = list-merge-sort.merge-sort lci λ l l' →
                posinfo-to-ℕ (lci.pi l) > posinfo-to-ℕ (lci.pi l')
      where import list-merge-sort
    -}

  merge-lcis-ctxt : ctxt → 𝕃 string → ctxt
  merge-lcis-ctxt Γ ls = fst $ merge-lcis-ctxt-tvs Γ ls

  get-local-ctxt-tvs : ctxt → (pos : ℕ) → (local-ctxt : 𝕃 string) → ctxt × 𝕃 tagged-val
  get-local-ctxt-tvs Γ pi =
    merge-lcis-ctxt-tvs (foldr (flip ctxt-clear-symbol ∘ fst) Γ
      (flip filter (trie-mappings (ctxt.i Γ)) λ {(x , ci , fn' , pi') →
        ctxt.fn Γ =string fn' && posinfo-to-ℕ pi' > pi}))

  get-local-ctxt : ctxt → (pos : ℕ) → (local-ctxt : 𝕃 string) → ctxt
  get-local-ctxt Γ pi ls = fst (get-local-ctxt-tvs Γ pi ls)

  {- Helpers -}

  step-reduce : ∀ {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
  step-reduce Γ t =
    let t' = erase t in maybe-else t' id (step-reduceh Γ t') where
    step-reduceh : ∀ {ed : exprd} → ctxt → ⟦ ed ⟧ → maybe ⟦ ed ⟧
    step-reduceh{TERM} Γ (Var x) = ctxt-lookup-term-var-def Γ x
    step-reduceh{TYPE} Γ (TpVar x) = ctxt-lookup-type-var-def Γ x
    step-reduceh{TERM} Γ (App (Lam ff x nothing t) t') = just (subst Γ t' x t)
    step-reduceh{TYPE} Γ (TpApp (TpLam x (Tkk _) T) (Ttp T')) = just (subst Γ T' x T)
    step-reduceh{TYPE} Γ (TpApp (TpLam x (Tkt _) T) (Ttm t)) = just (subst Γ t x T)
    step-reduceh{TERM} Γ (App t t') = step-reduceh Γ t >>= λ t → just (App t t')
    step-reduceh{TYPE} Γ (TpApp T tT) = step-reduceh Γ T >>= λ T → just (TpApp T tT)
    step-reduceh{TERM} Γ (Lam ff x nothing t) = step-reduceh (ctxt-var-decl x Γ) t >>= λ t → just (Lam ff x nothing t)
    step-reduceh{TYPE} Γ (TpLam x atk T) = step-reduceh (ctxt-var-decl x Γ) T >>= λ T → just (TpLam x atk T)
    step-reduceh{TERM} Γ (LetTm ff x T t' t) = just (subst Γ t' x t)
    step-reduceh{TERM} Γ t @ (Mu μ s Tₘ f~ ms) with
      decompose-var-headed s >>=c λ sₕ sₐs → env-lookup Γ sₕ
    ...| just (ctr-def _ _ _ _ _ , _) = just (hnf Γ unfold-head-no-defs t)
    ...| _ = step-reduceh Γ s >>= λ s → just (Mu μ s Tₘ f~ ms)
    step-reduceh Γ t = nothing

  parse-norm : erased? → string → maybe (∀ {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧)
  parse-norm me "all" = just λ Γ → hnf Γ (record unfold-all {unfold-erase = me})
  parse-norm me "head" = just λ Γ → hnf Γ (record unfold-head-elab {unfold-erase = me})
  parse-norm me "once" = just λ Γ → step-reduce Γ ∘ erase
  parse-norm _ _ = nothing

  parse-norm-err = "normalization method (all, head, once)"

  {- Command Executors -}

  normalize-cmd : ctxt → (str ll pi norm : string) → 𝕃 string → string ⊎ tagged-val
  normalize-cmd Γ str ll pi norm ls =
    parse-ll - ll ! "language-level" >>parse λ ll' →
    string-to-ℕ - pi ! "natural number" >>parse λ sp →
    parse-norm tt - norm ! parse-norm-err >>parse λ norm →
    parse-string ll' - str ! ll >>parse λ t →
      let Γ' = get-local-ctxt Γ sp ls in
    inj₂ (to-string-tag "" Γ' (norm Γ' (elab-untyped Γ' t)))

  normalize-prompt : ctxt → (str norm : string) → 𝕃 string → string ⊎ tagged-val
  normalize-prompt Γ str norm ls =
    parse-norm tt - norm ! parse-norm-err >>parse λ norm →
    let Γ' = merge-lcis-ctxt Γ ls in
    parse-try Γ' - str ! ttk >>parse λ f → f λ ll t →
    inj₂ (to-string-tag "" Γ' (norm Γ' (elab-untyped Γ' t)))

  erase-cmd : ctxt → (str ll pi : string) → 𝕃 string → string ⊎ tagged-val
  erase-cmd Γ str ll pi ls =
    parse-ll - ll ! "language-level" >>parse λ ll' →
    string-to-ℕ - pi ! "natural number" >>parse λ sp →
    parse-string ll' - str ! ll >>parse λ t →
    let Γ' = get-local-ctxt Γ sp ls in
    inj₂ (to-string-tag "" Γ' (erase (elab-untyped Γ' t)))

  erase-prompt : ctxt → (str : string) → 𝕃 string → string ⊎ tagged-val
  erase-prompt Γ str ls =
    let Γ' = merge-lcis-ctxt Γ ls in
    parse-try Γ' - str ! ttk >>parse λ f → f λ ll t →
    inj₂ (to-string-tag "" Γ' (erase (elab-untyped Γ' t)))

--  private
--    cmds-to-escaped-string : cmds → strM
--    cmds-to-escaped-string (c :: cs) = cmd-to-string c $ strAdd "\\n\\n" >>str cmds-to-escaped-string cs
--    cmds-to-escaped-string [] = strEmpty

--  data-cmd : ctxt → (encoding name ps is cs : string) → string ⊎ tagged-val
--  data-cmd Γ encodingₛ x psₛ isₛ csₛ =
--    string-to-𝔹 - encodingₛ ! "boolean" >>parse λ encoding →
--    parse-string KIND - psₛ ! "kind" >>parse λ psₖ →
--    parse-string KIND - isₛ ! "kind" >>parse λ isₖ →
--    parse-string KIND - csₛ ! "kind" >>parse λ csₖ →
--    let ps = map (λ {(Index x atk) → Decl posinfo-gen posinfo-gen Erased x atk posinfo-gen}) $ kind-to-indices Γ psₖ
--        cs = map (λ {(Index x (Tkt T)) → Ctr posinfo-gen x T; (Index x (Tkk k)) → Ctr posinfo-gen x $ mtpvar "ErrorExpectedTypeNotKind"}) $ kind-to-indices empty-ctxt csₖ
--        is = kind-to-indices (add-ctrs-to-ctxt cs $ add-params-to-ctxt ps Γ) isₖ
--        picked-encoding = if encoding then mendler-encoding else mendler-simple-encoding
--        defs = datatype-encoding.mk-defs picked-encoding Γ $ Data x ps is cs in
--    inj₂ $ strRunTag "" Γ $ cmds-to-escaped-string $ fst defs

--  pretty-cmd : filepath → filepath → IO string
--  pretty-cmd src-fn dest-fn =
--    readFiniteFile src-fn >>= λ src →
--    case parseStart src of λ where
--      (Left (Left p)) → return ("Lexical error at position " ^ p)
--      (Left (Right p)) → return ("Parse error at position " ^ p)
--      (Right file) → writeFile dest-fn "" >> writeRopeToFile dest-fn (to-string.strRun empty-ctxt (to-string.file-to-string file)) >> return "Finished"
--    where import to-string (record options {pretty-print = tt}) as to-string

  {- Commands -}

  tv-to-json : string ⊎ tagged-val → json
  tv-to-json (inj₁ s) = json-object [ "error" , json-string s ] -- [[ "{\"error\":\"" ]] ⊹⊹ [[ s ]] ⊹⊹ [[ "\"}" ]]
  tv-to-json (inj₂ (_ , v , ts)) = tagged-vals-to-json [ "value" , v , ts ]

  interactive-cmd-h : ctxt → 𝕃 string → string ⊎ tagged-val
  interactive-cmd-h Γ ("normalize" :: input :: ll :: sp :: norm :: lc) =
    normalize-cmd Γ input ll sp norm lc
  interactive-cmd-h Γ ("erase" :: input :: ll :: sp :: lc) =
    erase-cmd Γ input ll sp lc
  interactive-cmd-h Γ ("normalizePrompt" :: input :: norm :: lc) =
    normalize-prompt Γ input norm lc
  interactive-cmd-h Γ ("erasePrompt" :: input :: lc) =
    erase-prompt Γ input lc
--  interactive-cmd-h Γ ("data" :: encoding :: x :: ps :: is :: cs :: []) =
--    data-cmd Γ encoding x ps is cs
  interactive-cmd-h Γ cs =
    inj₁ ("Unknown interactive cmd: " ^ 𝕃-to-string (λ s → s) ", " cs)

  record br-history : Set where
    inductive
    constructor mk-br-history
    field
      Γ : ctxt
      t : term
      Tₗₗ : exprd
      T : ⟦ Tₗₗ ⟧
      Tᵤ : string
      f : term → 𝕃 (ctr × term) → term
      Γₗ : 𝕃 tagged-val
      undo : 𝕃 br-history
      redo : 𝕃 br-history

  data br-history2 : Set where
    br-node : br-history → 𝕃 (ctr × br-history2) → br-history2

  br-get-h : br-history2 → br-history
  br-get-h (br-node h hs) = h

  br-lookup : 𝕃 ℕ → br-history2 → maybe br-history
  br-lookup xs h = maybe-map br-get-h $
    foldl (λ x h? → h? >>= λ {(br-node h hs) → maybe-map snd $ head2 (nthTail x hs)}) (just h) xs

  {-# TERMINATING #-}
  br-cmd2 : ctxt → string → string → string → 𝕃 string → IO ⊤
  br-cmd2 Γ Tₛ tₛ sp ls =
    (string-to-ℕ - sp ! "natural number" >>parse inj₂) >>parseIO λ sp →
    elim-pair (get-local-ctxt-tvs Γ sp ls) λ Γ Γₗ →
    (parse-try Γ - Tₛ ! ttk >>parse inj₂) >>parseIO λ Tf → Tf λ Tₗₗ T →
    (parse-string TERM - tₛ ! "term" >>parse inj₂) >>parseIO λ t →
    let T = elab-untyped Γ T
        Tₑ = erase T
        t = elab-typed Γ t in -- TODO: Probably should switch back to ex-tm so if this doesn't currently check it won't elaborate to a hole!
    putJson (tv-to-json $ inj₂ $ ts-tag Γ Tₑ) >>
    await (br-node (mk-br-history Γ t Tₗₗ T (rope-to-string $ ts2.to-string Γ Tₑ) const Γₗ [] []) [])
    where

    import to-string (record options {erase-types = ff}) as ts2
    import to-string (record options {erase-types = ff; pretty-print = tt}) as pretty2s

    ts-tag : ∀ {ed} → ctxt → ⟦ ed ⟧ → tagged-val
    ts-tag = ts2.to-string-tag ""

    infixr 6 _>>parseIO_
    _>>parseIO_ : ∀ {A : Set} → string ⊎ A → (A → IO ⊤) → IO ⊤
    inj₁ e >>parseIO f = putJson $ tv-to-json $ inj₁ e
    inj₂ a >>parseIO f = f a

    replace-substring : string → string → ℕ → ℕ → string × string
    replace-substring sₒ sᵣ fm to with string-to-𝕃char sₒ | string-to-𝕃char sᵣ
    ...| csₒ | csᵣ =
      𝕃char-to-string (take fm csₒ ++ csᵣ ++ drop to csₒ) ,
      𝕃char-to-string (take (to ∸ fm) $ drop fm csₒ)

    replace : string → string → ℕ → ℕ → string
    replace sₒ sᵣ fm to = fst $ replace-substring sₒ sᵣ fm to

    substring : string → ℕ → ℕ → string
    substring s fm to = snd $ replace-substring s "" fm to

    escape-rope : rope → rope
    escape-rope [[ s ]] = [[ escape-string s ]]
    escape-rope (r₁ ⊹⊹ r₂) = escape-rope r₁ ⊹⊹ escape-rope r₂

    parse-path : string → maybe (𝕃 ℕ)
    parse-path "" = just []
    parse-path s with string-split s ' ' | foldr (λ n ns →  ns >>= λ ns → string-to-ℕ n >>= λ n → just (n :: ns)) (just [])
    ...| "" :: ss | f = f ss
    ...| path | f = f path

    write-history : 𝕃 ℕ → br-history → br-history2 → br-history2
    write-history [] h (br-node _ hs) = br-node h hs
    write-history (n :: ns) h (br-node hₒ hs) = br-node hₒ $ writeh n hs where
      writeh : ℕ → 𝕃 (ctr × br-history2) → 𝕃 (ctr × br-history2)
      writeh _ [] = []
      writeh zero ((c , h') :: hs) = (c , write-history ns h h') :: hs
      writeh (suc n) (h' :: hs) = h' :: writeh n hs

    write-children : 𝕃 ℕ → 𝕃 (ctr × br-history) → br-history2 → br-history2
    write-children [] hs (br-node h _) = br-node h (map (uncurry λ c h → c , br-node h []) hs)
    write-children (n :: ns) hs (br-node h hsₒ) = br-node h $ writeh n hsₒ where
      writeh : ℕ → 𝕃 (ctr × br-history2) → 𝕃 (ctr × br-history2)
      writeh _ [] = []
      writeh zero ((c , h') :: hs') = (c , write-children ns hs h') :: hs'
      writeh (suc n) (h' :: hs) = h' :: writeh n hs

    outline : br-history2 → term
--    outline (br-node (mk-br-history Γ t TYPE T Tₛ f Γₗ undo redo) []) =
--      elim-pair (id-out $ check-term Γ t (just T) empty-spans) λ t~ ss → f t~ []
--    outline (br-node (mk-br-history Γ t Tₗₗ T Tₛ f Γₗ undo redo) []) = f (elab-untyped-no-params Γ t) []
--    outline (br-node (mk-br-history Γ t Tₗₗ T Tₛ f Γₗ undo redo) hs) =
--      f (elab-typed Γ t) (map (uncurry λ c h → c , outline h) hs)
    outline (br-node (mk-br-history Γ t Tₗₗ T Tₛ f Γₗ undo redo) hs) =
      f t (map-snd outline <$> hs)

    make-case : ctxt → params → term → case-args × term
    make-case = h [] where
      h : params → ctxt → params → term → case-args × term
      h acc Γ (Param me x atk :: ps) (Lam me' x' oc' t') =
        h (Param me x' atk :: acc) (ctxt-var-decl x' Γ) (substh-params Γ (renamectxt-single x x') empty-trie ps) t'
      h acc Γ ps (Hole pi) = params-to-case-args (reverse acc ++ ps) , Hole pi
      h acc Γ ps t = params-to-case-args (reverse acc ++ ps) , params-to-apps ps t

    await : br-history2 → IO ⊤
    awaith : br-history2 → 𝕃 string → IO ⊤
    await his =
      getLine >>= λ input →
      let input = undo-escape-string input
          as = string-split input delimiter in
      awaith his as

    awaith his as =
      let put = putJson ∘ tv-to-json
          err = (_>> await his) ∘' put ∘' inj₁ in
      case as of λ where -- TODO: for these commands, do not add TYPES/KINDS of local decls to context, as they are probably just bound by foralls/pis/lambdas, not _really_ in scope!
        ("br" :: path :: as) →
          maybe-else' (parse-path path) (err ("Could not parse " ^ path ^ " as a list of space-delimited natural numbers")) λ path →
          let await-with = await ∘ flip (write-history path) his in
          maybe-else' (br-lookup path his) (err "Beta-reduction pointer does not exist") λ where
            this @ (mk-br-history Γ t Tₗₗ T Tᵤ f Γₗ undo redo) → case as of λ where

              ("undo" :: []) → case undo of λ where
                [] → err "No undo history"
                (u :: us) →
                  put (inj₂ $ "" , [[ "Undo" ]] , []) >>
                  await-with (record u {undo = us; redo = this :: redo})
                  --u (await Γ t Tₗₗ T Tᵤ f undo redo :: redo)

              ("redo" :: []) → case redo of λ where
                [] → err "No redo history"
                (r :: rs) →
                  put (inj₂ $ "" , [[ "Redo" ]] , []) >>
                  await-with (record r {undo = this :: undo; redo = rs})
                  --r

              ("get" :: []) →
                put (inj₂ $ "" , [[ Tᵤ ]] , []) >>
                await his

              ("parse" :: []) →
                (_>> await his) $
                maybe-else' (parse-string Tₗₗ Tᵤ)
                  (putJson $ spans-to-json $ global-error "Parse error" nothing)
                  λ T → putJson $ spans-to-json $ snd $ id-out $ ll-ind {λ ll → ctxt → ⟦ ll ⟧' → spanM ⟦ ll ⟧}
                          untyped-term untyped-type untyped-kind Tₗₗ (record Γ { fn = "missing" }) T empty-spans

              ("context" :: []) →
                putJson (json-object [ "value" , json-array [ tagged-vals-to-json Γₗ ] ]) >> await his

              ("check" :: t?) →
                let await-set = maybe-else (await his) λ t → await-with $ record this
                                  {t = t; undo = this :: undo; redo = []} in
                (λ e → either-else' e
                  (uncurry λ t? e → put (inj₁ e) >> await-set t?)
                  (uncurry λ t? m → put (inj₂ $ "value" , [[ m ]] , []) >> await-set t?)) $
                ll-ind' {λ T → (maybe term × string) ⊎ (maybe term × string)} (Tₗₗ , T)
                  (λ _ → inj₁ $ nothing , "Expression must be a type, not a term!")
                  (λ T →
                    (case t? of λ where
                      [] → inj₂ nothing
                      (t :: []) → maybe-else' (parse-string TERM t)
                        (inj₁ $ nothing , parse-err-msg t "term")
                        (inj₂ ∘ just)
                      _ → inj₁ $ nothing ,
                        "To many arguments given to beta-reduction command 'check'")
                  >>= λ t? →
                    elim-pair (maybe-else' t? (elim-pair (id-out (check-term (qualified-ctxt Γ) (resugar t) (just T) empty-spans)) λ t~ ss → nothing , spans-have-error ss)
                                 λ t → elim-pair (id-out (check-term Γ t (just T) empty-spans))
                                         λ t~ ss → just t~ , spans-have-error ss) λ t~? e? →
                    let fail = inj₁ (just (maybe-else' t~? t id) , "Type error")
                        try-β = elim-pair (id-out (check-term Γ (ExBeta pi-gen nothing nothing) (just T) empty-spans)) λ β~ ss → if spans-have-error ss then inj₁ (nothing , "Type error") else inj₂ (just β~ , "Equal by beta") in
                    if e?
                      then if isJust t? then fail else try-β
                      else inj₂ (t~? , "Type inhabited"))
                  (λ _ → inj₁ $ nothing , "Expression must be a type, not a kind!")

              ("rewrite" :: fm :: to :: eq :: ρ+? :: lc) →
                let Γ' = merge-lcis-ctxt Γ lc in
                either-else'
                  (parse-string TERM - eq ! "term" >>parse λ eqₒ →
                   string-to-𝔹 - ρ+? ! "boolean" >>parse λ ρ+? →
                   string-to-ℕ - fm ! "natural number" >>parse λ fm →
                   string-to-ℕ - to ! "natural number" >>parse λ to →
                   parse-try Γ' - substring Tᵤ fm to ! ttk >>parse λ Tf → Tf λ ll Tₗ →
                   elim-pair (id-out (check-term Γ' eqₒ nothing empty-spans)) $ uncurry λ eq Tₑ ss →
                   is-eq-tp? Tₑ ! "Synthesized a non-equational type from the proof"
                     >>error uncurry λ t₁ t₂ →
                   err⊎-guard (spans-have-error ss) "Proof does not type check" >>
                   let Tₑ = TpEq t₁ t₂
                       x = fresh-var Γ' "x"
                       Tₗ = elab-untyped-no-params Γ' Tₗ in
                   elim-pair (map-snd snd $ rewrite-exprd Tₗ Γ' ρ+? nothing (just eq) t₁ x 0) λ Tᵣ n →
                   err⊎-guard (iszero n) "No rewrites could be performed" >>
                   parse-string Tₗₗ - replace Tᵤ
                     (rope-to-string $ [[ "(" ]] ⊹⊹ ts2.to-string Γ' Tᵣ ⊹⊹ [[ ")" ]]) fm to
                     ! ll-ind "term" "type" "kind" Tₗₗ >>parse λ Tᵤ →
                   let Tᵤ = elab-untyped-no-params (ctxt-var-decl x Γ) Tᵤ in
                   ll-ind' {λ {(ll , T) → ⟦ ll ⟧ → string ⊎ ⟦ ll ⟧ × (term → term)}}
                     (Tₗₗ , Tᵤ)
                     (λ t T → inj₂ $ rewrite-mk-phi x eq T (subst Γ t₂ x t) , id)
                     (λ Tᵤ _ → inj₂ $ post-rewrite (ctxt-var-decl x Γ) x eq t₂ Tᵤ ,
                                      Rho eq x Tᵤ)
                     (λ k _ → inj₂ $ subst Γ t₂ x k , id)
                     T) err $ uncurry λ T' fₜ →
                  put (inj₂ $ ts-tag Γ $ erase T') >>
                  await-with (record this {T = T'; Tᵤ = rope-to-string $ ts2.to-string Γ $ erase T'; f = f ∘ fₜ; undo = this :: undo; redo = []})

              ("normalize" :: fm :: to :: norm :: lc) →
                either-else'
                  (let Γ' = merge-lcis-ctxt Γ lc in
                   string-to-ℕ - fm ! "natural number" >>parse λ fm →
                   string-to-ℕ - to ! "natural number" >>parse λ to →
                   let tₛ = substring Tᵤ fm to in
                   parse-try Γ' - tₛ ! ttk >>parse λ t → t λ ll t →
                   parse-norm ff - norm ! parse-norm-err >>parse λ norm →
                   let s = norm Γ' $ elab-untyped-no-params Γ' t
                       rs = rope-to-string $ [[ "(" ]] ⊹⊹ ts2.to-string Γ' s ⊹⊹ [[ ")" ]]
                       Tᵤ' = replace Tᵤ rs fm to in
                   parse-string Tₗₗ - Tᵤ' ! ll-ind "term" "type" "kind" Tₗₗ >>parse λ Tᵤ' →
                   let Tᵤ' = elab-untyped-no-params Γ' Tᵤ' in
                   inj₂ Tᵤ')
                  err λ Tᵤ' →
                  put (inj₂ $ ts-tag Γ Tᵤ') >>
                  await-with (record this {T = Tᵤ' {-Checks?-}; Tᵤ = rope-to-string $ ts2.to-string Γ $ erase Tᵤ'; undo = this :: undo; redo = []})

              ("conv" :: ll :: fm :: to :: t' :: ls) →
                let Γ' = merge-lcis-ctxt Γ ls in
                either-else'
                  (parse-ll - ll ! "language level" >>parse λ ll →
                   string-to-ℕ - fm ! "natural number" >>parse λ fm →
                   string-to-ℕ - to ! "natural number" >>parse λ to →
                   let t = substring Tᵤ fm to in
                   parse-string ll - t  ! ll-ind "term" "type" "kind" ll >>parse λ t  →
                   parse-string ll - t' ! ll-ind "term" "type" "kind" ll >>parse λ t' →
                   let t = elab-untyped-no-params Γ' t; t' = elab-untyped-no-params Γ' t' in
                   err⊎-guard (~ ll-ind {λ ll → ctxt → ⟦ ll ⟧ → ⟦ ll ⟧ → 𝔹}
                     conv-term conv-type conv-kind ll Γ' t t') "Inconvertible" >>
                   let rs = [[ "(" ]] ⊹⊹ ts2.to-string Γ' (erase t') ⊹⊹ [[ ")" ]]
                       Tᵤ = replace Tᵤ (rope-to-string rs) fm to in
                   parse-string Tₗₗ - Tᵤ ! ll-ind "term" "type" "kind" Tₗₗ >>parse λ Tᵤ →
                   inj₂ (elab-untyped-no-params Γ Tᵤ)) err λ Tᵤ' →
                  put (inj₂ $ ts-tag Γ $ erase Tᵤ') >>
                  await-with (record this {Tᵤ = rope-to-string $ ts2.to-string Γ $ erase Tᵤ'; undo = this :: undo; redo = []})

              ("bind" :: xᵤ :: []) →
                let Γₚᵢ = ℕ-to-string (length Γₗ) in
                either-else'
                  (ll-ind' {λ {(ll , _) → string ⊎ ctxt × erased? × tpkd × ⟦ ll ⟧ × (term → term)}} (Tₗₗ , T)
                    (λ t' →
                      let R = string ⊎ ctxt × erased? × tpkd × term × (term → term) in
                      (case_of_ {B = (erased? → var → maybe tpkd → term → R) → R}
                        (t' , hnf Γ unfold-head t') $ uncurry λ where
                          (Lam me x oc body) _ f → f me x oc body
                          _ (Lam me x oc body) f → f me x oc body
                          _ _ _ → inj₁ "Not a term abstraction") λ me x oc body →
                      inj₂ $ ctxt-var-decl-loc Γₚᵢ xᵤ Γ ,
                             me ,
                             maybe-else' oc (Tkt $ TpHole pi-gen) id ,
                             rename-var (ctxt-var-decl-loc Γₚᵢ xᵤ Γ) x xᵤ body ,
                             Lam me xᵤ oc)
                    (λ T → Γ ⊢ T =β= λ where
                      (TpAbs me x dom cod) →
                        let Γ' = ctxt-tk-decl Γₚᵢ xᵤ dom Γ in
                        inj₂ $ Γ' ,
                               me ,
                               dom ,
                               rename-var Γ' x (Γₚᵢ % xᵤ) cod ,
                               Lam me xᵤ (just dom)
                      _ → inj₁ "Not a type abstraction")
                    (λ k → inj₁ "Expression must be a term or a type"))
                  err λ where
                    (Γ' , me , dom , cod , fₜ) →
                      let tv = binder-data Γ' Γₚᵢ xᵤ dom me nothing "0" "0" in
--                      putJson (json-object [ "value" , json-array (json-array (json-rope (fst (snd tv)) :: json-rope (to-string Γ' $ erase cod) :: []) :: []) ]) >>
                      putJson (json-object [ "value" , json-array [ json-rope (to-string Γ' $ erase cod) ] ]) >>
                      await-with (record this
                        {Γ = Γ' ;
                         T = cod;
                         Tᵤ = rope-to-string $ ts2.to-string Γ' $ erase cod;
                         f = f ∘ fₜ;
                         Γₗ = Γₗ ++ [ tv ];
                         undo = this :: undo;
                         redo = []})

              ("case" :: scrutinee :: rec :: motive?) → -- TODO: Motive?
                let Γₚᵢ = ℕ-to-string (length Γₗ) in
                either-else'
                  (parse-string TERM - scrutinee ! "term" >>parse λ scrutinee →
                   elim-pair (id-out (check-term Γ scrutinee nothing empty-spans)) $ uncurry λ tₛ Tₛ ss →
                   if (spans-have-error ss) then inj₁ "Error synthesizing a type from the input term"
                   else
                   let Tₛ = hnf Γ unfold-no-defs Tₛ in
                   case decompose-ctr-type Γ Tₛ of λ where
                     (TpVar Xₛ , [] , as) →
                       ll-ind' {λ T → string ⊎ (term × term × 𝕃 (ctr × type) × type × ctxt × 𝕃 tagged-val × datatype-info)} (Tₗₗ , T)
                         (λ t → inj₁ "Expression must be a type to case split")
                         (λ T → maybe-else' (data-lookup Γ Xₛ as)
                           (inj₁ "The synthesized type of the input term is not a datatype")
                           λ d → let mk-data-info X _ asₚ asᵢ ps kᵢ k cs csₚₛ _ _ = d
                                     is' = kind-to-indices (add-params-to-ctxt ps Γ) kᵢ
                                     is = drop-last 1 is'
                                     Tₘ = refine-motive Γ is' (asᵢ ++ [ Ttm tₛ ]) T
                                     sM' = ctxt-mu-decls Γ tₛ is Tₘ d Γₚᵢ "0" "0" rec
                                     σ = λ y → inst-ctrs Γ ps asₚ (map-snd (rename-var {TYPE} Γ X y) <$> cs)
                                     sM = if rec =string ""
                                             then (σ X , const spanMok , Γ , [] , empty-renamectxt , (λ Γ t T → t) , (λ Γ T k → T))
                                             else (σ (Γₚᵢ % mu-Type/ rec) , sM')
                                     mu = sigma-build-evidence Xₛ d in
                             case sM of λ where
                               (σ-cs , _ , Γ' , ts , ρ , tf , Tf) →
                                 if spans-have-error (snd $ id-out $
                                      check-type (qualified-ctxt Γ) (resugar Tₘ) (just kᵢ) empty-spans)
                                   then inj₁ "Computed an ill-typed motive"
                                   else inj₂ (
                                     tₛ ,
                                     mu ,
                                     map (λ {(Ctr x T) →
                                       let T' = hnf Γ' unfold-head-elab T in
                                       Ctr x T ,
                                       (case decompose-ctr-type Γ' T' of λ {(Tₕ , ps' , as) →
                                         params-to-alls ps' $ hnf Γ' unfold-head-no-defs (TpApp
                                           (recompose-tpapps (drop (length ps) as) Tₘ)
                                           (Ttm (recompose-apps (params-to-args ps') $
                                             recompose-apps asₚ (Var x))))})})
                                       σ-cs ,
                                     Tₘ ,
                                     Γ' ,
                                     ts ,
                                     d))
                         (λ k → inj₁ "Expression must be a type to case split")
                     (Tₕ , [] , as) → inj₁ "Synthesized a non-datatype from the input term"
                     (Tₕ , ps , as) →
                       inj₁ "Case splitting is currently restricted to datatypes")
                err $ λ where
                 (scrutinee , mu , cs , Tₘ , Γ , ts , d) →
                   let json = json-object [ "value" , json-array
                                   [ json-object (map
                                    (λ {(Ctr x _ , T) → unqual-all (ctxt.qual Γ) x ,
                                      json-rope (to-string Γ (erase T))})
                                    cs) ] ] in -- ) ] ] in
                   putJson json >>
                   let shallow = iszero (string-length rec)
                       mk-cs = map λ where
                         (Ctr x T , t) →
                           let T' = hnf Γ unfold-head-elab T in
                           case decompose-ctr-type Γ T' of λ where
                             (Tₕ , ps , as) →
                               elim-pair (make-case Γ ps t) λ cas t → Case x cas t []
                       f'' = λ t cs → (if shallow then Mu rec else Sigma (just mu)) t (just Tₘ) d (mk-cs cs)
                       f' = λ t cs → f (f'' t cs) cs
                       mk-hs = map $ map-snd λ T'' →
                                 mk-br-history Γ t TYPE T''
                                   (rope-to-string $ to-string Γ $ erase T'')
                                   (λ t cs → t) (Γₗ ++ ts) [] [] in
                   await (write-children path (mk-hs cs) $
                            write-history path (record this
                              {f = f';
                               Γ = Γ;
                               t = scrutinee;
                               Γₗ = Γₗ ++ ts;-- TODO: Should we really do this?
                               undo = this :: undo;
                               redo = []})
                              his)

              ("print" :: tab :: []) →
                either-else' (string-to-ℕ - tab ! "natural number" >>parse inj₂) err λ tab →
                putRopeLn (escape-rope (json-to-rope (tv-to-json (inj₂ $ pretty2s.strRunTag "" Γ $ pretty2s.strNest (suc {-left paren-} tab) (pretty2s.to-stringh $ outline his))))) >> await his

              ("quit" :: []) → put $ inj₂ $ strRunTag "" Γ $ strAdd "Quitting beta-reduction mode..."

              _ → err $ foldl (λ a s → s ^ char-to-string delimiter ^ a)
                      "Unknown beta-reduction command: " as
        _ → err "A beta-reduction buffer is still open"

interactive-cmd : 𝕃 string → toplevel-state → IO ⊤
interactive-cmd ("br2" :: T :: t :: sp :: lc) ts = br-cmd2 (toplevel-state.Γ ts) T t sp lc
--interactive-cmd ("pretty" :: src :: dest :: []) ts = pretty-cmd src dest >>= putStrLn
interactive-cmd ls ts = putRopeLn (json-to-rope (tv-to-json (interactive-cmd-h (toplevel-state.Γ ts) ls)))

interactive-not-br-cmd-msg = tv-to-json $ inj₁ "Beta-reduction mode has been terminated"


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Permutation.Propositional directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Permutation.Inductive where

{-# WARNING_ON_IMPORT
"Data.List.Relation.Binary.Permutation.Inductive was deprecated in v1.1.
Use Data.List.Relation.Binary.Permutation.Propositional instead."
#-}

open import Data.List.Relation.Binary.Permutation.Propositional public


text:
open import Agda.Primitive
open import Agda.Builtin.Equality  renaming (_≡_ to _==_) --(( If I want to rename the built-in equality ))

module AlgebraFormalization where

  -- Here is an attempt to translate (part of) the Coq formalization. I did not translate the definition of the free algebra, the proof, and the part concerning the groups yet. I hope I did not do too weird things with the levels.

  -- ** Formalization of single-sorted algebraic theories **

  -- Function extensionality
  postulate
    funext : ∀ {X : Set} {Y : X → Set} {f g : ∀ (x : X) → (Y x)} → (∀ (x : X) → ((f x) == (g x))) → (f == g)
  -- Operation Signature
  record OpSignature {l : Level} : Set (lsuc l) where
    field
      operation : Set l
      arity : operation → Set l
  -- I used the things with the levels of the hierachy of types because Agda was unhappy with what I was doing (and I did not want to define it only with Set₀ and Set₁ beacause I wanted to avoid weird things if we then want to define an OpSignature with an operation OpSignature)

-- Here is a attempt (partial for the moment) to add context and terms, based on the same principles as in the file "ManySortedAlgebra.agda"
  -- Contexts
  record Context {l : Level} (Σ : OpSignature {l}) : Set (lsuc l) where
    field
      var : Set l

  open Context

  -- Terms on an operation signature
  data Term {l : Level} {Σ : OpSignature {l}} (Γ : Context Σ) : Set l  where
    tm-var : ∀ (x : var Γ) → Term Γ
    tm-op : ∀ (f : OpSignature.operation Σ) → (OpSignature.arity Σ f → Term Γ) → Term Γ

  substitution : ∀ {l : Level} {Σ : OpSignature {l}} (Γ Δ : Context Σ) → Set l
  substitution Γ Δ = ∀ (x : var Γ) → Term Δ

  -- the action of a substitution on a term
  _·_ : ∀ {l : Level} {Σ : OpSignature {l}} {Γ Δ : Context Σ} → substitution Γ Δ  → Term Γ → Term Δ
  σ · (tm-var x) = σ x
  σ · (tm-op f x) = tm-op f (λ i → σ · x i)

  infixr 6 _·_

  -- composition of substitutions
  _○_ : ∀ {l : Level} {Σ : OpSignature {l}} {Γ Δ Θ : Context Σ} → substitution Δ Θ → substitution Γ Δ → substitution Γ Θ
  (σ ○ τ) x = σ · τ x

  infixl 7 _○_

-- End of the attempt

  -- Operation Algebra
  record OpAlgebra {l : Level} (S : OpSignature {l}) : Set (lsuc l) where
    field
      carrier : Set l
      op : ∀ (o : OpSignature.operation S) (f : OpSignature.arity S o → carrier) → carrier

  -- Homomorphisms
  record Hom {l : Level} {S : OpSignature {l}} (A : OpAlgebra {l} S) (B : OpAlgebra {l} S) : Set (lsuc l) where
    field
      map : (OpAlgebra.carrier A) → (OpAlgebra.carrier B)
      op-commute : ∀ (o : OpSignature.operation S) (args : OpSignature.arity S o → OpAlgebra.carrier A) → (map (OpAlgebra.op A o args) == OpAlgebra.op B o (λ x → map (args x) ))

  -- For the moment I skip the translation of the part concerning the free algebra

-- Attempt to formalize the Equational theories diffenrently, based on what is done in the file "ManySortedAglebra.agda"

  -- Equational Theory (equations are seen as "in a context" and not with arities anymore)
  record EquationalTheory {l : Level} (Σ : OpSignature {l}) : Set (lsuc l) where
    field
      eq : Set l
      eq-ctx : ∀ (ε : eq) → Context {l} Σ
      eq-lhs : ∀ (ε : eq) → Term (eq-ctx ε)
      eq-rhs : ∀ (ε : eq) → Term (eq-ctx ε)

  open EquationalTheory

  -- Equality of terms
  infix 4 _≡_

  data _≡_ {l : Level} {Σ : OpSignature {l}} {T : EquationalTheory {l} Σ } : {Γ : Context Σ} → Term Γ → Term Γ → Set (lsuc l) where
    -- general rules
    eq-refl : ∀ {Γ} {t : Term Γ } → t ≡ t
    eq-symm : ∀ {Γ} {s t : Term {l} {Σ} Γ } → _≡_ {T = T} s t → t ≡ s
    eq-tran : ∀ {Γ} {s t u : Term Γ } → _≡_ {T = T} s t → _≡_ {T = T} t u → s ≡ u
    -- congruence rule
    eq-congr : ∀ {Γ} {f : OpSignature.operation Σ} (x y : ∀ (i : OpSignature.arity Σ f) → Term Γ) → (∀ i → _≡_ {_} {_} {T} (x i) (y i)) → ((tm-op f x) ≡ (tm-op f y))
    -- equational axiom
    eq-axiom : ∀ (ε : eq T) {Δ : Context {l} Σ} (σ : substitution (eq-ctx T ε) Δ) →
               ((σ · eq-lhs T ε) ≡ (σ · eq-rhs T ε))

  -- composition is functorial
  subst-○ : ∀ {l : Level} {Σ : OpSignature {l}} {T : EquationalTheory Σ} {Γ Δ Θ : Context Σ}
              (σ : substitution Δ Θ) (τ : substitution Γ Δ) →
              ∀ (t : Term Γ ) → _≡_ {T = T} (σ · τ · t)  (σ ○ τ · t)
  subst-○ σ τ (tm-var x) = eq-refl
  subst-○ σ τ (tm-op f x) = eq-congr (λ i → σ · τ · x i) (λ i → σ ○ τ · x i) λ i → subst-○ σ τ (x i)

  -- substitution preserves equality
  eq-subst : ∀ {l : Level} {Σ : OpSignature {l}} {T : EquationalTheory Σ} {Γ Δ : Context Σ} (σ : substitution Γ Δ)
               {s t : Term Γ}  → _≡_ {T = T} s t → _≡_ {T = T} (σ · s) (σ · t)
  eq-subst σ eq-refl = eq-refl
  eq-subst σ (eq-symm ξ) = eq-symm (eq-subst σ ξ)
  eq-subst σ (eq-tran ζ ξ) = eq-tran (eq-subst σ ζ) (eq-subst σ ξ)
  eq-subst σ (eq-congr x y ξ) = eq-congr (λ i → σ · x i) (λ i → σ · y i) λ i → eq-subst σ (ξ i)
  eq-subst {T = T} σ (eq-axiom ε τ) =
    eq-tran (subst-○ σ τ (eq-lhs T ε))
            (eq-tran (eq-axiom ε (σ ○ τ)) (eq-symm (subst-○ σ τ (eq-rhs T ε))))

-- End of the attempt

  -- Equation Signature
  record EqSignature {l : Level} (S : OpSignature {l}) : Set (lsuc l) where
    field
      eq : Set l
      eq-arity : eq → Set l
      -- the two sides of the equation
      lhs : ∀ {A : OpAlgebra {l} S} {e : eq} → ((eq-arity e) → (OpAlgebra.carrier A)) → (OpAlgebra.carrier A)
      rhs : ∀ {A : OpAlgebra {l} S} {e : eq} → ((eq-arity e) → (OpAlgebra.carrier A)) → (OpAlgebra.carrier A)
      -- naturality / commutation
      lhs-natural : ∀ (A B : OpAlgebra {l} S) (f : Hom A B) (e : eq) (args : eq-arity e → OpAlgebra.carrier A) → ( (Hom.map f) (lhs {A} {e} args) == lhs {B} {e} (λ i → (Hom.map f) (args i)))
      rhs-natural : ∀ (A B : OpAlgebra {l} S) (f : Hom A B) (e : eq) (args : eq-arity e → OpAlgebra.carrier A) → ( (Hom.map f) (rhs {A} {e} args) == rhs {B} {e} (λ i → (Hom.map f) (args i)))

  --  Algebra
  record Algebra {l : Level} (S : OpSignature {l}) (E : EqSignature {l} S) : Set (lsuc l) where
    field
      alg : OpAlgebra S
      equations : ∀ (e : EqSignature.eq E) (args : EqSignature.eq-arity E e → OpAlgebra.carrier  alg) → (EqSignature.rhs E {alg} {e} args == EqSignature.lhs E {alg} {e} args)

   -- For the moment, I think that we did not talk about terms in contexts, did we ? Should we generalize the things we did in Lambda.agda (using De Bruijn indices for the variables) ? -> I tried things

  -- ** Other things **

  -- Useful arities
  data nullary : Set where
  data unary : Set where
    only : unary
  data binary : Set where
    fst : binary
    snd : binary

  -- Definition of groups
  data GroupOperation : Set where
    one : GroupOperation
    mul : GroupOperation
    inv : GroupOperation

  GroupArity : (o : GroupOperation) → Set
  GroupArity one = nullary
  GroupArity mul = binary
  GroupArity inv = unary

  GroupOp : OpSignature
  GroupOp = record { operation = GroupOperation ;  arity = GroupArity}

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module 100-natural where

open import 010-false-true
open import 020-equivalence

record Natural
  {N : Set}
  (zero : N)
  (suc : N -> N)
  (_==_ : N -> N -> Set)
  : Set1 where

  -- axioms
  field
    equiv : Equivalence _==_
    sucn!=zero : ∀ {r} -> suc r == zero -> False
    sucinjective : ∀ {r s} -> suc r == suc s -> r == s
    cong : ∀ {r s} -> r == s -> suc r == suc s
    induction : (p : N -> Set) -> p zero -> (∀ n -> p n -> p (suc n)) -> (∀ n -> p n)

  open Equivalence equiv public

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


text:
module Formalization.LambdaCalculus.Semantics.Reduction where

import      Lvl
open import Data
open import Formalization.LambdaCalculus
open import Formalization.LambdaCalculus.SyntaxTransformation
open import Numeral.Natural
open import Numeral.Finite
open import Relator.ReflexiveTransitiveClosure
open import Syntax.Number
open import Type

private variable d d₁ d₂ : ℕ
private variable f g x y : Term(d)

-- β-reduction (beta) with its compatible closure over `Apply`.
-- Reduces a term of form `f(x)` to `f[0 ≔ x]`.
data _β⇴_ : Term(d₁) → Term(d₂) → Type{1} where
  β : {f : Term(𝐒(d))}{x : Term(d)} → (Apply(Abstract(f))(x) β⇴ substituteVar0(x)(f))
  cong-applyₗ : (f β⇴ g) → (Apply f(x) β⇴ Apply g(x)) -- TODO: cong-applyₗ and cong-applyᵣ can be applied in any order, but many evaluation strategies have a fixed order. How should this be represented?
  cong-applyᵣ : (x β⇴ y) → (Apply f(x) β⇴ Apply f(y))
  cong-abstract : (x β⇴ y) → (Abstract x β⇴ Abstract y) -- TODO: Sometimes this is not included, specifically for the call by value evaluation strategy? But it seems to be required for the encoding of ℕ?

-- η-reduction (eta). (TODO: May require more introductions like β have)
-- Reduces a term of form `x ↦ f(x)` to `f`.
data _η⇴_ : Term(d₁) → Term(d₂) → Type{1} where
  η : (Abstract(Apply(f)(Var(maximum))) η⇴ f)

-- Reduction of expressions (TODO: May require more introductions like β have)
data _⇴_ : Term(d₁) → Term(d₂) → Type{1} where
  β : (Apply(Abstract(f))(x) ⇴ substituteVar0(x)(f))
  η : (Abstract(Apply(f)(Var(maximum))) ⇴ f)

_β⇴*_ : Term(d) → Term(d) → Type
_β⇴*_ = ReflexiveTransitiveClosure(_β⇴_)

_β⥈_ : Term(d) → Term(d) → Type
_β⥈_ = SymmetricClosure(_β⇴_)

_β⥈*_ : Term(d) → Term(d) → Type
_β⥈*_ = ReflexiveTransitiveClosure(_β⥈_)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Cubical.Data.Queue.1List public
open import Cubical.Data.Queue.Truncated2List public
open import Cubical.Data.Queue.Untruncated2List public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module dynamic where

open import LSsyntax
open import static
open import Relation.Nullary
open import Data.Nat using (ℕ ; _+_)
open import Data.Fin using (Fin; toℕ)
open import Data.Vec using (Vec ; lookup; _∷_; [])
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Bool using (Bool; true ; false)

data _⊓ˡ_ : (ℓ₁ ℓ₂ : Label) → Set where
    ℓ⊓✭ : ∀ ℓ → ℓ ⊓ˡ ✭
    ✭⊓ℓ : ∀ ℓ → ✭ ⊓ˡ ℓ
    idℓ : ∀ ℓ → ℓ ⊓ˡ ℓ

_⊓ᵣ_ : ∀ (ℓ₁ ℓ₂ : Label) → Dec (ℓ₁ ⊓ˡ ℓ₂)
⊤ ⊓ᵣ ⊤ = yes (idℓ ⊤)
⊤ ⊓ᵣ ⊥ = no (λ ())
⊤ ⊓ᵣ ✭ = yes (ℓ⊓✭ ⊤)
⊥ ⊓ᵣ ⊤ = no (λ ())
⊥ ⊓ᵣ ⊥ = yes (idℓ ⊥)
⊥ ⊓ᵣ ✭ = yes (ℓ⊓✭ ⊥)
✭ ⊓ᵣ ⊤ = yes (✭⊓ℓ ⊤)
✭ ⊓ᵣ ⊥ = yes (✭⊓ℓ ⊥)
✭ ⊓ᵣ ✭ = yes (ℓ⊓✭ ✭)

-- note that this is not actually correct. The meet of ⊤ and bottom for example should be undefined,
-- but that isn't easy to model directly in Agda. However, if we only call this after induction over
-- the proof of _⊓ᵣ_ it (should) be impossible to call one of the incorrect cases.
recMeet : ∀ (ℓ₁ ℓ₂ : Label) → Label
recMeet ⊤ ⊤ = ⊤
recMeet ⊤ ✭ = ⊤
recMeet ⊥ ⊥ = ⊥
recMeet ⊥ ✭ = ⊥
recMeet ✭ ⊤ = ⊤
recMeet ✭ ⊥ = ⊥
recMeet ✭ ✭ = ✭
recMeet _ _ = ✭     -- fake case

_⊓_ : ∀ (t₁ t₂ : GType) → GType
bool x ⊓ bool x₁ with x ⊓ᵣ x₁
bool x ⊓ bool x₁ | yes p = bool (recMeet x x₁)
bool x ⊓ bool x₁ | no ¬p = err
bool x ⊓ _ = err
(t₁ ⇒ x) t₂ ⊓ (t₃ ⇒ x₁) t₄ with x ⊓ᵣ x₁
(t₁ ⇒ x) t₂ ⊓ (t₃ ⇒ x₁) t₄ | yes p with (t₁ ⊓ t₃) | (t₂ ⊓ t₄)
(t₁ ⇒ x₂) t₂ ⊓ (t₃ ⇒ x₃) t₄ | yes p | (bool x) | (bool x₁) = ((bool x) ⇒ (recMeet x₂ x₃)) (bool x)
-- this is probably not correct, but it keeps things simple.
(t₁ ⇒ x₂) t₂ ⊓ (t₃ ⇒ x₃) t₄ | yes p | (bool x) | ((d ⇒ x₁) d₁) = err
(t₁ ⇒ x₂) t₂ ⊓ (t₃ ⇒ x₃) t₄ | yes p | ((c ⇒ x) c₁) | (bool x₁) = err
(t₁ ⇒ x₂) t₂ ⊓ (t₃ ⇒ x₃) t₄ | yes p | ((c ⇒ x) c₁) | ((d ⇒ x₁) d₁) = err
(t₁ ⇒ x₁) t₂ ⊓ (t₃ ⇒ x₂) t₄ | yes p | (bool x) | err = err
(t₁ ⇒ x₁) t₂ ⊓ (t₃ ⇒ x₂) t₄ | yes p | ((c ⇒ x) c₁) | err = err
(t₁ ⇒ x₁) t₂ ⊓ (t₃ ⇒ x₂) t₄ | yes p | err | (bool x) = err
(t₁ ⇒ x₁) t₂ ⊓ (t₃ ⇒ x₂) t₄ | yes p | err | ((d ⇒ x) d₁) = err
(t₁ ⇒ x) t₂ ⊓ (t₃ ⇒ x₁) t₄ | yes p | err | err = err
(t₁ ⇒ x) t₂ ⊓ (t₃ ⇒ x₁) t₄ | no ¬p = err
_ ⊓ _ = err

I≼ : ∀ (ℓ₁ ℓ₂ : Label) → (Label × Label)
I≼ ⊤ ✭   = ⊤ , ⊤
I≼ ✭ ⊤   = ✭ , ⊤
I≼ ✭ ⊥   = ⊥ , ⊥
I≼ ⊥ ✭   = ⊥ , ✭
I≼ ℓ₁ ℓ₂ = ℓ₁ , ℓ₂

Δ≼ : ∀ (triple : Label × Label × Label) → (Label × Label)
Δ≼ (ℓ₁ , ⊤ , ⊤) = ℓ₁ , ⊤
Δ≼ (ℓ₁ , ⊤ , ✭) = ℓ₁ , ⊤
Δ≼ (⊥ , ⊥ , ℓ₃) = ⊥ , ℓ₃
Δ≼ (⊥ , ✭ , ℓ₃) = ⊥ , ℓ₃
Δ≼ (ℓ₁ , ✭ , ℓ₃) = ℓ₁ , ℓ₃
Δ≼ (ℓ₁ , ℓ₂ , ℓ₃) = ℓ₁ , ℓ₃

Δ< : ∀ (triple : GType × GType × GType) → (GType × GType)
Δ< (bool ℓ₁ , bool ℓ₂ , bool ℓ₃) =
    let new = Δ≼ (ℓ₁ , ℓ₂ , ℓ₃) in
    bool (proj₁ new) , bool (proj₂ new)
Δ< ((t₁ ⇒ ℓ₁) t′₁ , (t₂ ⇒ ℓ₂) t′₂ , (t₃ ⇒ ℓ₃) t′₃) =
    let new = Δ≼ (ℓ₁ , ℓ₂ , ℓ₃) in
    ((t₁ ⇒ (proj₁ new)) t′₁) , ((t₃ ⇒ (proj₂ new)) t′₃)
Δ< (_ , _ , _) = err , err

interior : ∀ (t : GType) → (GType × GType)
interior (bool ℓ) =  (bool ℓ) , (bool ℓ)
interior ((t ⇒ ℓ) t₁) =
    let (ℓ₁ , ℓ₂) = I≼ (getLabel t) ℓ in
    ((setLabel t ℓ₁) ⇒ ℓ₂) t₁ , ((setLabel t ℓ₁) ⇒ ℓ₂) t₁
interior err = err , err

_∘<_ : ∀ (t₁ t₂ : (GType × GType)) → (GType × GType)
(s₁ , s₂₁) ∘< (s₂₂ , s₃) = Δ< (s₁ , (s₂₁ ⊓ s₂₂) , s₃)

dynamicCheck : ∀ {n} (Γ : Ctx n) (t : Term) → Check Γ t
-- variables
dynamicCheck {n} Γ (var v) with fromℕ n v
dynamicCheck {n} Γ (var .(toℕ m)) | yes m = yes (lookup m Γ) (Sx m refl)
dynamicCheck {n} Γ (var .(n + m)) | no m = no

-- literals
dynamicCheck Γ (litBool x ℓ) = yes (bool ℓ) (Sb x ℓ)

-- lambda abstraction
dynamicCheck Γ (lam x t x₁) with dynamicCheck (x ∷ Γ) t
dynamicCheck Γ (lam x .(erase t) ℓ) | yes τ t = yes ((x ⇒ ℓ) τ) (Sλ x ℓ t)
dynamicCheck Γ (lam x t x₁) | no = no

-- logical and
dynamicCheck Γ (t ∧ t₁) with dynamicCheck Γ t | dynamicCheck Γ t₁
dynamicCheck Γ (.(erase t) ∧ .(erase t₁)) | yes τ t | (yes τ₁ t₁) with (interior τ) ∘< (interior τ₁)
dynamicCheck Γ (.(erase t) ∧ .(erase t₁)) | yes τ t | (yes τ₁ t₁) | (bool x , bool x₁) = yes (bool (getLabel τ ~⋎~ getLabel τ₁)) (t S∧ t₁)
dynamicCheck Γ (.(erase t) ∧ .(erase t₁)) | yes τ t | (yes τ₁ t₁) | (_ , _) = no
dynamicCheck Γ (t ∧ t₁) | _ | _ = no

-- logical or
dynamicCheck Γ (t ∨ t₁) with dynamicCheck Γ t | dynamicCheck Γ t₁
dynamicCheck Γ (.(erase t) ∨ .(erase t₁)) | yes τ t | (yes τ₁ t₁) with (interior τ) ∘< (interior τ₁)
dynamicCheck Γ (.(erase t) ∨ .(erase t₁)) | yes τ t | (yes τ₁ t₁) | (bool x , bool x₁) = yes (bool (getLabel τ ~⋎~ getLabel τ₁)) (t S∨ t₁)
dynamicCheck Γ (.(erase t) ∨ .(erase t₁)) | yes τ t | (yes τ₁ t₁) | (_ , _) = no
dynamicCheck Γ (t ∨ t₁) | _ | _ = no

-- application
-- this needs to be doublechecked!
dynamicCheck Γ (t ∙ t₁) with dynamicCheck Γ t | dynamicCheck Γ t₁
dynamicCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ₁) τ₁) t | yes τ₂ t₁ with (interior ((τ ⇒ ℓ₁) τ₁)) ∘< (interior τ₂)
dynamicCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ₁) τ₁) t | (yes τ₂ t₁) | (bool x , bool x₁) = yes (bool (getLabel τ₁ ~⋎~ ℓ₁)) (S∙ t t₁ (yes τ₂ τ))
dynamicCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ₁) τ₁) t | (yes τ₂ t₁) | (bool x , (proj₄ ⇒ x₁) proj₅) = no
dynamicCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ₁) τ₁) t | (yes τ₂ t₁) | ((proj₃ ⇒ x) proj₄ , bool x₁) = no
dynamicCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ₁) τ₁) t | (yes τ₂ t₁) | ((proj₃ ⇒ x) proj₄ , (proj₅ ⇒ x₁) proj₆) = no
dynamicCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ₁) τ₁) t | (yes τ₂ t₁) | (_ , _) = no
dynamicCheck Γ (.(erase t) ∙ .(erase t₁)) | yes _ t | (yes _ t₁) = no
dynamicCheck Γ (.(erase t) ∙ t₁) | yes τ t | no = no
dynamicCheck Γ (t₁ ∙ .(erase t)) | no | yes τ t = no
dynamicCheck Γ (t ∙ t₁) | no | no = no

-- if then else
dynamicCheck Γ (if b then t₁ else t₂) with dynamicCheck Γ b
dynamicCheck Γ (if .(erase b) then t₁ else t₂) | yes τ b with dynamicCheck Γ t₁ | dynamicCheck Γ t₂
dynamicCheck Γ (if .(erase b) then .(erase t₁) else .(erase t₂)) | yes τ b | (yes τ₁ t₁) | (yes τ₂ t₂) with (interior τ₁) ∘< (interior τ₂)
dynamicCheck Γ (if .(erase b) then .(erase t₁) else .(erase t₂)) | yes τ b | (yes τ₁ t₁) | (yes τ₂ t₂) | (bool ℓ , bool ℓ₁) = yes (bool (getLabel (τ₁ :∨: τ₂) ~⋎~ getLabel τ)) (Sif b t₁ t₂)
dynamicCheck Γ (if .(erase b) then .(erase t₁) else .(erase t₂)) | yes τ b | (yes τ₁ t₁) | (yes τ₂ t₂) | (_ , _) = no
dynamicCheck Γ (if .(erase b) then t₁ else t₂) | yes τ b | _ | _ = no
dynamicCheck Γ (if b then t₁ else t₂) | no = no

-- error
dynamicCheck Γ error = no

max_stars_repo_path: Agda/Gradual Security/dynamic.agda

max_stars_repo_name: kellino/TypeSystems

max_issues_repo_path: Agda/Gradual Security/dynamic.agda

max_issues_repo_name: kellino/TypeSystems

max_forks_repo_path: Agda/Gradual Security/dynamic.agda

max_forks_repo_name: kellino/TypeSystems


text:
module Numeral.Natural.Sequence where

import      Lvl
open import Data
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
import      Data.Tuple.Raise as Tuple
open import Functional
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.FlooredDivision
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable n : ℕ
private variable A : Type{ℓ}
private variable B : Type{ℓ}

-- Alternates between the two sides, starting with the left.
-- A countable bijection for the Either type.
-- Examples:
--   alternate₂(0) = Left(0)
--   alternate₂(2) = Left(1)
--   alternate₂(4) = Left(2)
--   alternate₂(6) = Left(3)

--   alternate₂(1) = Right(0)
--   alternate₂(3) = Right(1)
--   alternate₂(5) = Right(2)
--   alternate₂(7) = Right(3)
alternate₂ : ℕ → (ℕ ‖ ℕ)
alternate₂(0)       = Either.Left 0
alternate₂(1)       = Either.Right 0
alternate₂(𝐒(𝐒(n))) = Either.map 𝐒 𝐒 (alternate₂ n)

-- The inverse of `alternate₂`.
unalternate₂ : (ℕ ‖ ℕ) → ℕ
unalternate₂(Either.Left  n) = n ⋅ 2
unalternate₂(Either.Right n) = 𝐒(n ⋅ 2)

-- Maps two natural numbers to a single one without overlaps by following the inverse diagonals downwards.
-- A countable bijection for the tuple pairing type.
-- Alternative forms:
--   pairIndexing a b = a + (∑(𝕟(a + b)) (i ↦ 𝕟-to-ℕ(i)))
--   pairIndexing a b = a + ((a + b) * (a + b + 1) / 2)
-- Example:
--   Horizontal axis is `a` starting from 0.
--   Vertical axis is `b` starting from 0.
--   Cells are `pairIndexing a b`.
--    0, 1, 3, 6,10,15
--    2, 4, 7,11,16,..
--    5, 8,12,17,   ..
--    9,13,18,      ..
--   14,19,         ..
--   20,.. .. .. .. ..
-- Termination:
--   Decreases `a` until 0 while at the same time increases `b` (So `b` is at most `a`).
--   Then the arguments is swapped, but using the predecessor of `b`.
--   This means that `b` will eventually reach 0.
{-# TERMINATING #-}
pairIndexing : ℕ → ℕ → ℕ
pairIndexing 𝟎     𝟎     = 𝟎
pairIndexing (𝐒 a) 𝟎     = 𝐒(pairIndexing 𝟎 a)
{-# CATCHALL #-}
pairIndexing a     (𝐒 b) = 𝐒(pairIndexing (𝐒 a) b)

-- A sequence which fills a discrete two dimensional grid (a space bounded in two directions and infinite in the other two).
-- It is the inverse of an uncurried `pairIndexing`.
-- Example:
--   •-→-• ↗→• ↗→•
--     ↙ ↗ ↙ ↗ ↙
--   •→↗ • ↗ •   •
--     ↙ ↗ ↙
--   •→↗ •   •   •
diagonalFilling : ℕ → (ℕ ⨯ ℕ)
diagonalFilling 𝟎      = (𝟎 , 𝟎)
diagonalFilling (𝐒(n)) with diagonalFilling n
... | (𝟎    , b) = (𝐒(b) , 0)
... | (𝐒(a) , b) = (a , 𝐒(b))

tupleIndexing : (ℕ Tuple.^ n) → ℕ
tupleIndexing {𝟎}       <>      = 𝟎
tupleIndexing {𝐒(𝟎)}    x       = x
tupleIndexing {𝐒(𝐒(n))} (x , y) = pairIndexing x (tupleIndexing {𝐒(n)} y)

spaceFilling : ℕ → (ℕ Tuple.^ n)
spaceFilling {𝟎}          _ = <>
spaceFilling {𝐒(𝟎)}       i = i
spaceFilling {𝐒(𝐒(n))}    i = Tuple.mapRight (spaceFilling {𝐒(n)}) (diagonalFilling i)

-- Interleaves two sequences into one, alternating between the elements from each sequence.
interleave : (ℕ → A) → (ℕ → B) → (ℕ → (A ‖ B))
interleave af bf = Either.map af bf ∘ alternate₂

pair : (ℕ → A) → (ℕ → B) → (ℕ → (A ⨯ B))
pair af bf = Tuple.map af bf ∘ diagonalFilling


text:
module Utils.Exception where

{-# IMPORT Utils.Exception #-}

open import Utils.HaskellTypes

data Either (A : Set) (B : Set) : Set where
  Left : A → Either A B
  Right : B → Either A B
{-# COMPILED_DATA Either Either Left Right #-}

right : ∀{X A : Set} → A → Either X A
right x = Right x

error : ∀{X A : Set} → X → Either X A
error e = Left e

_>>=E_ : ∀{X A B : Set} → Either X A → (A → Either X B) → Either X B
_>>=E_ (Left x) f = Left x
_>>=E_ (Right x) f = f x

commExpTriple : {X A B C : Set} → Triple (Either X A) B C → Either X (Triple A B C)
commExpTriple (triple (Left e) b c) = error e
commExpTriple (triple (Right a) b c) = right (triple a b c)

commExpList : {X A : Set} → List (Either X A) → Either X (List A)
commExpList [] = right []
commExpList (Left e :: xs) = Left e
commExpList (Right y :: xs) = (commExpList xs) >>=E (λ ys → right (y :: ys))

data Exception : Set where
  IllformedLetPattern : Exception
  IllformedPromote : Exception
  VarNotInCtx : Exception
  Nonlinearity : Exception
  NonlocallyClosed : Exception
  NonEmptyCtx : Exception
  TypeErrorLetNotTop : Exception
  TypeErrorLetNotTensor : Exception
  TypeErrorPromoteNotBang : Exception
  TypeErrorTypesNotEqual : Exception
  TypeErrorAppNotImp : Exception
  NonLinearCtx : Exception
  TypeErrorDuplicatedFreeVar : Exception
{-# COMPILED_DATA Exception Utils.Exception.Exception Utils.Exception.IllformedLetPattern
                                                      Utils.Exception.IllformedPromote
                                                      Utils.Exception.VarNotInCtx
                                                      Utils.Exception.Nonlinearity
                                                      Utils.Exception.NonlocallyClosed
                                                      Utils.Exception.NonEmptyCtx
                                                      Utils.Exception.TypeErrorLetNotTop
                                                      Utils.Exception.TypeErrorLetNotTensor
                                                      Utils.Exception.TypeErrorPromoteNotBang
                                                      Utils.Exception.TypeErrorTypesNotEqual
                                                      Utils.Exception.TypeErrorAppNotImp
                                                      Utils.Exception.NonLinearCtx
                                                      Utils.Exception.TypeErrorDuplicatedFreeVar #-}

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


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

module Cubical.Categories.Category.Base where

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv

private
  variable
    ℓ ℓ' : Level

-- Precategories

record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  -- no-eta-equality ; NOTE: need eta equality for `opop`
  field
    ob : Type ℓ
    Hom[_,_] : ob → ob → Type ℓ'
    id : ∀ x → Hom[ x , x ]
    _⋆_ : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
    -- TODO: change these to implicit argument
    ⋆IdL : ∀ {x y : ob} (f : Hom[ x , y ]) → (id x) ⋆ f ≡ f
    ⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ (id y) ≡ f
    ⋆Assoc : ∀ {u v w x} (f : Hom[ u , v ]) (g : Hom[ v , w ]) (h : Hom[ w , x ]) → (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)

  -- composition: alternative to diagramatic order
  _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
  g ∘ f = f ⋆ g

open Precategory

-- Helpful syntax/notation

_[_,_] : (C : Precategory ℓ ℓ') → (x y : C .ob) → Type ℓ'
_[_,_] = Hom[_,_]

-- needed to define this in order to be able to make the subsequence syntax declaration
seq' : ∀ (C : Precategory ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
seq' = _⋆_

infixl 15 seq'
syntax seq' C f g = f ⋆⟨ C ⟩ g

-- composition
comp' : ∀ (C : Precategory ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ]
comp' = _∘_

infixr 16 comp'
syntax comp' C g f = g ∘⟨ C ⟩ f

-- Categories

record isCategory (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    isSetHom : ∀ {x y} → isSet (C [ x , y ])

-- Isomorphisms and paths in precategories

record CatIso {C : Precategory ℓ ℓ'} (x y : C .Precategory.ob) : Type ℓ' where
  constructor catiso
  field
    mor : C [ x , y ]
    inv : C [ y , x ]
    sec : inv ⋆⟨ C ⟩ mor ≡ C .id y
    ret : mor ⋆⟨ C ⟩ inv ≡ C .id x

pathToIso : {C : Precategory ℓ ℓ'} (x y : C .ob) (p : x ≡ y) → CatIso {C = C} x y
pathToIso {C = C} x y p = J (λ z _ → CatIso x z) (catiso (C .id x) idx (C .⋆IdL idx) (C .⋆IdL idx)) p
  where
    idx = C .id x

-- Univalent Categories

record isUnivalent (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    univ : (x y : C .ob) → isEquiv (pathToIso {C = C} x y)

  -- package up the univalence equivalence
  univEquiv : ∀ (x y : C .ob) → (x ≡ y) ≃ (CatIso x y)
  univEquiv x y = (pathToIso {C = C} x y) , (univ x y)

open isUnivalent public

-- Opposite Categories

_^op : Precategory ℓ ℓ' → Precategory ℓ ℓ'
(C ^op) .ob = C .ob
(C ^op) .Hom[_,_] x y = C .Hom[_,_] y x
(C ^op) .id = C .id
(C ^op) ._⋆_ f g = C ._⋆_ g f
(C ^op) .⋆IdL = C .⋆IdR
(C ^op) .⋆IdR = C .⋆IdL
(C ^op) .⋆Assoc f g h = sym (C .⋆Assoc _ _ _)

open isCategory public


text:
-- Partly based on code due to Andrea Vezzosi.

open import Common.Prelude

data D : Set where
  run-time        : Bool → D
  @0 compile-time : Bool → D

f : D → @0 D → Bool
f (run-time x)     _                = x
f (compile-time x) (run-time y)     = x
f (compile-time x) (compile-time y) = y

main : IO Unit
main =
  putStrLn (if f (run-time true) (compile-time false)
            then "ok" else "bad")

max_stars_repo_name: guilhermehas/agda

max_issues_repo_name: guilhermehas/agda

max_forks_repo_name: guilhermehas/agda


text:
module Structure.Type.Identity where

import      Lvl
open import Lang.Instance
open import Logic.Propositional
open import Logic
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type
open import Type.Properties.MereProposition
open import Type.Size

module _ {ℓ ℓₑ ℓₚ} {T : Type{ℓ}} (_≡_ : T → T → Stmt{ℓₑ}) where
  -- When a binary relation is the smallest reflexive relation (in the sense of cardinality of the relation set).
  -- This is one of many characterizations of equality.
  MinimalReflexiveRelation : Stmt
  MinimalReflexiveRelation = ∀{_▫_ : T → T → Stmt{ℓₚ}} → ⦃ refl : Reflexivity(_▫_) ⦄ → ((_≡_) ⊆₂ (_▫_))

  -- When a binary relation is able to substitute every unary relation and is satisfied when every unary relation .
  -- This is one of many characterizations of equality.
  GlobalSubstitution : Stmt
  GlobalSubstitution = ∀{x y : T} → ((x ≡ y) ↔ (∀{P : T → Type{ℓₚ}} → P(x) → P(y)))

module _ {ℓ ℓₑ ℓₘₑ} (T : Type{ℓ}) ⦃ equiv-T : Equiv{ℓₑ}(T) ⦄ ⦃ equiv-eq : ∀{x y : T} → Equiv{ℓₘₑ}(x ≡ y) ⦄ where
  -- A proof of identity is unique (there is only one inhabitant of the identity type).
  -- This is interpreted as saying that all proofs of an identity are equal to each other.
  -- Also called: Uniqueness of identity proofs (UIP).
  -- There is an axiom called "axiom UIP" which is a construction of the following type:
  -- • ∀{T} → UniqueIdentityProofs(T)
  UniqueIdentityProofs : Stmt
  UniqueIdentityProofs = ∀{x y : T} → MereProposition(x ≡ y)

module Names where
  module _ {ℓ ℓₑ ℓₚ} {T : Type{ℓ}} (Id : T → T → Stmt{ℓₑ}) ⦃ refl : Reflexivity(Id) ⦄ where
    -- Elimination rule for identity types.
    -- Also called J.
    -- Explanation:
    --   P{x}{y} (eq-proof) is an arbitrary predicate with possible mentions of an identity proof.
       --   A value of type (∀{x : T} → P(reflexivity(_≡_) {x})) means:
    --     reflexivity(_≡_) satisfies P for every pair of equal objects.
    --   The conclusion of the type (∀{x y : T} → (eq : (x ≡ y)) → P{x}{y}(eq)) means:
    --     Every identity proof satisfies P for every pair there is.
    --   In other words, to prove a proposition that depends on an identity proof, one only need to prove it for reflexivity.
    -- When this is joined by reflexivity, they become another characterization of equality.
    -- More information:
    -- • https://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/
    -- • https://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda
    IdentityEliminator : Stmt
    IdentityEliminator = (P : ∀{x y : T} → (Id x y) → Stmt{ℓₚ}) → (∀{x : T} → P(reflexivity(Id) {x})) → (∀{x y : T} → (eq : (Id x y)) → P(eq))

    -- Usage of the trivial equality reflexivity proof can be substituted by any proof of the same type.
    -- There is an axiom called "axiom K" which is a construction of the following type:
    -- • ∀{T} → IntroProofSubstitution(T)
    IntroProofSubstitution : Stmt
    IntroProofSubstitution = ∀{x : T}{P : (Id x x) → Type{ℓₚ}} → P(reflexivity(Id)) → (∀{eq : (Id x x)} → P(eq))

module _ {ℓ ℓₑ ℓₚ} {T : Type{ℓ}} (Id : T → T → Stmt{ℓₑ}) ⦃ refl : Reflexivity(Id) ⦄ where
  record IdentityEliminator : Stmt{ℓ Lvl.⊔ ℓₑ Lvl.⊔ Lvl.𝐒(ℓₚ)} where
    constructor intro
    field elim : Names.IdentityEliminator{ℓₚ = ℓₚ}(Id)
  idElim = inst-fn IdentityEliminator.elim

module _
  {ℓ ℓₘ ℓₑ ℓₘₑ}
  {T : Type{ℓ}}
  (Id : T → T → Type{ℓₑ}) ⦃ refl-T :  Reflexivity(Id) ⦄  ⦃ identElim-T : IdentityEliminator(Id) ⦄
  (_≡_ : ∀{T : Type{ℓₘ}} → T → T → Type{ℓₘₑ})
  where

  open Reflexivity (refl-T) using () renaming (proof to refl)

  -- Reflexivity is an identity element for the identity elimination operation.
  record IdentityEliminationOfIntro : Stmt{ℓ Lvl.⊔ Lvl.𝐒 ℓₘ Lvl.⊔ ℓₑ Lvl.⊔ ℓₘₑ} where
    constructor intro
    field proof : (P : ∀{x y : T} → (Id x y) → Stmt{ℓₘ}) → (p : ∀{x} → P{x}{x}(refl)) → (∀{x : T} → (idElim(Id)(P) p refl ≡ p{x}))
  idElimOfIntro = inst-fn IdentityEliminationOfIntro.proof

module _ {ℓₑ : Lvl.Level → Lvl.Level} (Id : ∀{ℓ}{T : Type{ℓ}} → T → T → Stmt{ℓₑ(ℓ)}) where
  record IdentityType : Stmtω where
    constructor intro
    field
      ⦃ identity-intro ⦄ : ∀{ℓₒ}{T : Type{ℓₒ}} → Reflexivity(Id{T = T})
      ⦃ identity-elim ⦄  : ∀{ℓₒ ℓₚ}{T : Type{ℓₒ}} → IdentityEliminator{ℓₚ = ℓₚ}(Id{T = T})
      ⦃ refl-elim-inverses ⦄ : ∀{ℓ ℓₘ}{T : Type{ℓ}} → IdentityEliminationOfIntro{ℓₘ = ℓₘ}(Id{T = T})(Id)


text:
module PLRTree.Complete.Correctness.Base {A : Set} where

open import BTree.Complete.Base {A}
open import BTree.Complete.Alternative.Correctness {A} renaming (lemma-complete'-complete to lemma-complete''-complete)
open import Function using (_∘_)
open import PLRTree {A}
open import PLRTree.Complete {A} renaming (Complete to Complete' ; _⋗_ to _⋗'_ ; _⋘_ to _⋘'_ ; _⋙_ to _⋙'_)
open import PLRTree.Complete.Correctness.Alternative {A} renaming (lemma-complete'-complete to lemma-complete'-complete'')
open import PLRTree.Equality.Correctness {A}

lemma-complete'-complete : {t : PLRTree} → Complete' t → Complete (forget t)
lemma-complete'-complete = lemma-complete''-complete ∘ lemma-complete'-complete''

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Example where

open import Logic.Identity
open import Base
open import Category
open import Product
open import Terminal
open import Unique
import Iso

infixr 30 _─→_
infixr 90 _∘_

data Name : Set where
  Zero : Name
  One  : Name
  Half : Name

data Obj : Set1 where
  obj : Name -> Obj

mutual
  _─→'_ : Name -> Name -> Set
  x ─→' y = obj x ─→ obj y

  data _─→_ : Obj -> Obj -> Set where
    Idle  : {A : Name} -> A    ─→' A
    All   :		  Zero ─→' One
    Start :		  Zero ─→' Half
    Turn  :		  Half ─→' Half
    Back  :		  One  ─→' Half
    End   :		  Half ─→' One

id : {A : Obj} -> A ─→ A
id {obj x} = Idle

_∘_ : {A B C : Obj} -> B ─→ C -> A ─→ B -> A ─→ C
f    ∘ Idle  = f
Idle ∘ All   = All
Idle ∘ Start = Start
Turn ∘ Start = Start
End  ∘ Start = All
Idle ∘ Turn  = Turn
Turn ∘ Turn  = Turn
End  ∘ Turn  = End
Idle ∘ Back  = Back
Turn ∘ Back  = Back
End  ∘ Back  = Idle
Idle ∘ End   = End

idL : {A B : Obj}{f : A ─→ B} -> id ∘ f ≡ f
idL {f = Idle  } = refl
idL {f = All   } = refl
idL {f = Start } = refl
idL {f = Turn  } = refl
idL {f = Back  } = refl
idL {f = End   } = refl

idR : {A B : Obj}{f : A ─→ B} -> f ∘ id ≡ f
idR {obj _} = refl

assoc : {A B C D : Obj}{f : C ─→ D}{g : B ─→ C}{h : A ─→ B} ->
	(f ∘ g) ∘ h ≡ f ∘ (g ∘ h)
assoc {f = _   }{g = _   }{h = Idle } = refl
assoc {f = _   }{g = Idle}{h = All  } = refl
assoc {f = _   }{g = Idle}{h = Start} = refl
assoc {f = Idle}{g = Turn}{h = Start} = refl
assoc {f = Turn}{g = Turn}{h = Start} = refl
assoc {f = End }{g = Turn}{h = Start} = refl
assoc {f = Idle}{g = End }{h = Start} = refl
assoc {f = _   }{g = Idle}{h = Turn } = refl
assoc {f = Idle}{g = Turn}{h = Turn } = refl
assoc {f = Turn}{g = Turn}{h = Turn } = refl
assoc {f = End }{g = Turn}{h = Turn } = refl
assoc {f = Idle}{g = End }{h = Turn } = refl
assoc {f = _   }{g = Idle}{h = Back } = refl
assoc {f = Idle}{g = Turn}{h = Back } = refl
assoc {f = Turn}{g = Turn}{h = Back } = refl
assoc {f = End }{g = Turn}{h = Back } = refl
assoc {f = Idle}{g = End }{h = Back } = refl
assoc {f = _   }{g = Idle}{h = End  } = refl

ℂ : Cat
ℂ = cat Obj _─→_ id _∘_
	(\{_}{_} -> Equiv)
	(\{_}{_}{_} -> cong2 _∘_)
	idL idR assoc

open module T = Term ℂ
open module I = Init ℂ
open module S = Sum ℂ

term : Terminal (obj One)
term (obj Zero) = ?

init : Initial (obj Zero)
init = ?

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --experimental-irrelevance #-}
module ShapeIrrelevantParameterNoBecauseOfRecursion where

data ⊥ : Set where
record ⊤ : Set where

data Bool : Set where
  true false : Bool

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

data D ..(b : Bool) : Set where
  c : True b → D b  -- should fail

fromD : {b : Bool} → D b → True b
fromD (c p) = p

cast : .(a b : Bool) → D a → D b
cast _ _ x = x

bot : ⊥
bot = fromD (cast true false (c _))

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda