text:
open import FRP.JS.Level using ( Level ; _⊔_ ) renaming ( zero to o ; suc to ↑ )
open import FRP.JS.Time using ( Time ; _≤_ ; _<_ )
open import FRP.JS.Bool using ( Bool ; true ; false ; not ; _≟_ )
open import FRP.JS.True using ( True ; tt )

module FRP.JS.Model where

-- This model is essentially System F-omega with a kind time
-- together with a type for the partial order on time,
-- and expressions for reflexivity and transitivity.
-- We prove parametricity, and then show that parametricity implies causality.

-- Note that this is a "deep" notion of causality, not the "shallow"
-- causality usually used in FRP. The pragmatic upshot of this is that
-- there is only one time model: nested signals are in the same time
-- model, not a simulated time model. This fits with the JS implementation,
-- which uses wall clock time for all signals.

-- Propositional equality

data _≡_ {α} {A : Set α} (a : A) : A → Set α where
  refl : a ≡ a

sym : ∀ {α} {A : Set α} {a b : A} → (a ≡ b) → (b ≡ a)
sym refl = refl

trans : ∀ {α} {A : Set α} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c)
trans refl refl = refl

cong : ∀ {α β} {A : Set α} {B : Set β} (f : A → B) {a₁ a₂ : A} →
  (a₁ ≡ a₂) → (f a₁ ≡ f a₂)
cong f refl = refl

apply : ∀ {α β} {A : Set α} {B : Set β} {F G : A → B} → (F ≡ G) →
  ∀ {a b} → (a ≡ b) → (F a ≡ G b)
apply refl refl = refl

cast : ∀ {α} {A B : Set α} → (A ≡ B) → A → B
cast refl a = a

cast² : ∀ {α} {A B : Set α} {ℜ ℑ : A → B → Set α} → (ℜ ≡ ℑ) → ∀ {a b} → ℜ a b → ℑ a b
cast² refl aℜb = aℜb

irrel : ∀ b → (b₁ b₂ : True b) → (b₁ ≡ b₂)
irrel true  tt tt = refl
irrel false () ()

-- Postulates (including dependent extensionality)

data _≤?_ (t u : Time) : Set where
  leq : True (t ≤ u) → (t ≤? u)
  geq : True (u ≤ t) → (t ≤? u)

postulate
  ≤-refl : ∀ t → True (t ≤ t)
  ≤-trans : ∀ t u v → True (t ≤ u) → True (u ≤ v) → True (t ≤ v)
  ≤-asym : ∀ t u → True (t ≤ u) → True (u ≤ t) → (t ≡ u)
  ≤-total : ∀ t u → (t ≤? u)
  dext : ∀ {α β} {A : Set α} {B : A → Set β} {F G : ∀ a → B a} → (∀ a → F a ≡ G a) → (F ≡ G)

ext : ∀ {α β} {A : Set α} {B : Set β} {F G : A → B} →
  (∀ a → F a ≡ G a) → (F ≡ G)
ext = dext

iext : ∀ {α β} {A : Set α} {B : A → Set β} {F G : ∀ {a} → B a} →
  (∀ a → F {a} ≡ G {a}) → ((λ {a} → F {a}) ≡ (λ {a} → G {a}))
iext F≈G = cong (λ X {a} → X a) (dext F≈G)

-- Finite products

record ⊤ {α} : Set α where
  constructor tt

open ⊤ public

record Σ {α β} (A : Set α) (B : A → Set β) : Set (α ⊔ β) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

_×_ : ∀ {α β} → Set α → Set β → Set (α ⊔ β)
A × B = Σ A (λ a → B)

_×²_ : ∀ {α β} {A C : Set α} {B D : Set β} →
  (A → C → Set α) → (B → D → Set β) → ((A × B) → (C × D) → Set (α ⊔ β))
(ℜ ×² ℑ) (a , b) (c , d) = (ℜ a c × ℑ b d)

_→²_ : ∀ {α β} {A C : Set α} {B D : Set β} →
  (A → C → Set α) → (B → D → Set β) → ((A → B) → (C → D) → Set (α ⊔ β))
(ℜ →² ℑ) f g = ∀ {a b} → ℜ a b → ℑ (f a) (g b)

-- Case on booleans

data Case (c : Bool) : Set where
  _,_ : ∀ b → True (b ≟ c) → Case c

switch : ∀ b → Case b
switch true  = (true , tt)
switch false = (false , tt)

-- Reactive sets

RSet : ∀ α → Set (↑ α)
RSet α = Time → Set α

-- Equalitional reasoning

infix  4 _IsRelatedTo_
infix  2 _∎
infixr 2 _≡⟨_⟩_
infix  1 begin_

data _IsRelatedTo_ {α} {A : Set α} (a b : A) : Set α where
  relTo : (a≡b : a ≡ b) → a IsRelatedTo b

begin_ : ∀ {α} {A : Set α} {a b : A} → a IsRelatedTo b → a ≡ b
begin relTo a≡b = a≡b

_≡⟨_⟩_ : ∀ {α} {A : Set α} a {b c : A} → a ≡ b → b IsRelatedTo c → a IsRelatedTo c
_ ≡⟨ a≡b ⟩ relTo b≡c = relTo (trans a≡b b≡c)

_∎ : ∀ {α} {A : Set α} (a : A) → a IsRelatedTo a
_∎ _ = relTo refl

-- Kinds

data Kind : Set where
  time : Kind
  set : Level → Kind
  _⇒_ : Kind → Kind → Kind

level : Kind → Level
level time    = o
level (set α) = ↑ α
level (K ⇒ L) = level K ⊔ level L

K⟦_⟧ : ∀ K → Set (level K)
K⟦ time ⟧  = Time
K⟦ set α ⟧ = Set α
K⟦ K ⇒ L ⟧ = K⟦ K ⟧ → K⟦ L ⟧

_∋_↔_ : ∀ K → K⟦ K ⟧ → K⟦ K ⟧ → Set (level K)
time    ∋ t ↔ u = (t ≡ u)
set α   ∋ A ↔ B = A → B → Set α
(K ⇒ L) ∋ F ↔ G = ∀ {A B} → (K ∋ A ↔ B) → (L ∋ F A ↔ G B)

-- ≡ can be used as a structural equivalence on relations.

struct : ∀ K {A B C D} → (A ≡ B) → (K ∋ B ↔ D) → (C ≡ D) → (K ∋ A ↔ C)
struct K refl ℜ refl = ℜ

struct-ext : ∀ K L {A B} {F G H I : K⟦ K ⇒ L ⟧}
  (F≈G : ∀ A → F A ≡ G A) (ℜ : (K ⇒ L) ∋ G ↔ I) (H≈I : ∀ B → H B ≡ I B) (ℑ : K ∋ A ↔ B) →
    struct L (F≈G A) (ℜ ℑ) (H≈I B) ≡ struct (K ⇒ L) (ext F≈G) ℜ (ext H≈I) ℑ
struct-ext K L {A} {B} F≈G ℜ H≈I ℑ
 with ext F≈G | ext H≈I | F≈G A | H≈I B
... | refl    | refl    | refl  | refl = refl

struct-apply : ∀ K L {F G H I A B C D} →
  (F≡G : F ≡ G) (ℜ : (K ⇒ L) ∋ G ↔ I) (H≡I : H ≡ I) →
  (A≡B : A ≡ B) (ℑ : K ∋ B ↔ D) (C≡D : C ≡ D) →
    struct (K ⇒ L) F≡G ℜ H≡I (struct K A≡B ℑ C≡D)
      ≡ struct L (apply F≡G A≡B) (ℜ ℑ) (apply H≡I C≡D)
struct-apply K L refl ℜ refl refl ℑ refl = refl

struct-cast : ∀ {α A B C D} (ℜ : set α ∋ B ↔ D) (A≡B : A ≡ B) (C≡D : C ≡ D) {a c} →
  struct (set α) A≡B ℜ C≡D a c → ℜ (cast A≡B a) (cast C≡D c)
struct-cast ℜ refl refl aℜc = aℜc

struct-sym : ∀ K {A B C D ℑ ℜ} → (A≡B : A ≡ B) → (C≡D : C ≡ D) →
  (ℑ ≡ struct K A≡B ℜ C≡D) →
    (ℜ ≡ struct K (sym A≡B) ℑ (sym C≡D))
struct-sym K refl refl refl = refl

struct-trans : ∀ K {A B C D E F}
  (A≡B : A ≡ B) (B≡C : B ≡ C) (ℜ : K ∋ C ↔ F) (E≡F : E ≡ F) (D≡E : D ≡ E) →
    struct K A≡B (struct K B≡C ℜ E≡F) D≡E ≡
      struct K (trans A≡B B≡C) ℜ (trans D≡E E≡F)
struct-trans K refl refl ℜ refl refl = refl

-- Type contexts

infixr 4 _∷_

data Kinds : Set where
  [] : Kinds
  _∷_ : Kind → Kinds → Kinds

levels : Kinds → Level
levels []      = o
levels (K ∷ Σ) = level K ⊔ levels Σ

Σ⟦_⟧ : ∀ Σ → Set (levels Σ)
Σ⟦ [] ⟧    = ⊤
Σ⟦ K ∷ Σ ⟧ = K⟦ K ⟧ × Σ⟦ Σ ⟧

_∋_↔*_ : ∀ Σ → Σ⟦ Σ ⟧ → Σ⟦ Σ ⟧ → Set (levels Σ)
[]      ∋ tt       ↔* tt       = ⊤
(K ∷ Σ) ∋ (A , As) ↔* (B , Bs) = (K ∋ A ↔ B) × (Σ ∋ As ↔* Bs)

-- Inclusion order on type contexts.
-- Credited by Randy Pollack to Geuvers and Nederhof, JAR 1991.
-- http://thread.gmane.org/gmane.comp.lang.agda/3259/focus=3267

data _⊑_ : Kinds → Kinds → Set where
  id : ∀ {Σ} → Σ ⊑ Σ
  keep : ∀ K {Σ Υ} → (Σ ⊑ Υ) → ((K ∷ Σ) ⊑ (K ∷ Υ))
  skip : ∀ K {Σ Υ} → (Σ ⊑ Υ) → (Σ ⊑ (K ∷ Υ))

⊑⟦_⟧ : ∀ {Σ Υ} → (Σ ⊑ Υ) → Σ⟦ Υ ⟧ → Σ⟦ Σ ⟧
⊑⟦ id ⟧         As       = As
⊑⟦ keep K Σ⊑Υ ⟧ (A , As) = (A , ⊑⟦ Σ⊑Υ ⟧ As)
⊑⟦ skip K Σ⊑Υ ⟧ (A , As) = ⊑⟦ Σ⊑Υ ⟧ As

⊑⟦_⟧² : ∀ {Σ Υ} → (Σ⊑Υ : Σ ⊑ Υ) → ∀ {As Bs} → (Υ ∋ As ↔* Bs) → (Σ ∋ ⊑⟦ Σ⊑Υ ⟧ As ↔* ⊑⟦ Σ⊑Υ ⟧ Bs)
⊑⟦ id ⟧²         ℜs       = ℜs
⊑⟦ keep K Σ⊑Υ ⟧² (ℜ , ℜs) = (ℜ , ⊑⟦ Σ⊑Υ ⟧² ℜs)
⊑⟦ skip K Σ⊑Υ ⟧² (ℜ , ℜs) = ⊑⟦ Σ⊑Υ ⟧² ℜs

-- Concatenation of type contexts

_++_ : Kinds → Kinds → Kinds
[]      ++ Υ = Υ
(K ∷ Σ) ++ Υ = K ∷ (Σ ++ Υ)

_∋_++_∋_ : ∀ Σ → Σ⟦ Σ ⟧ → ∀ Υ → Σ⟦ Υ ⟧ → Σ⟦ Σ ++ Υ ⟧
[]      ∋ tt       ++ Υ ∋ Bs = Bs
(K ∷ Σ) ∋ (A , As) ++ Υ ∋ Bs = (A , (Σ ∋ As ++ Υ ∋ Bs))

_∋_++²_∋_ : ∀ Σ {As Bs} → (Σ ∋ As ↔* Bs) → ∀ Υ {Cs Ds} → (Υ ∋ Cs ↔* Ds) →
  ((Σ ++ Υ) ∋ (Σ ∋ As ++ Υ ∋ Cs) ↔* (Σ ∋ Bs ++ Υ ∋ Ds))
[]      ∋ tt       ++² Υ ∋ ℑs = ℑs
(K ∷ Σ) ∋ (ℜ , ℜs) ++² Υ ∋ ℑs = (ℜ , (Σ ∋ ℜs ++² Υ ∋ ℑs))

-- Type variables

data TVar (K : Kind) : Kinds → Set where
  zero : ∀ {Σ} → TVar K (K ∷ Σ)
  suc : ∀ {L Σ} → TVar K Σ → TVar K (L ∷ Σ)

τ⟦_⟧ : ∀ {Σ K} (τ : TVar K Σ) → Σ⟦ Σ ⟧ → K⟦ K ⟧
τ⟦ zero ⟧  (A , As)  = A
τ⟦ suc τ ⟧ (A , As)  = τ⟦ τ ⟧ As

τ⟦_⟧² : ∀ {Σ K} (τ : TVar K Σ) {As Bs} → (Σ ∋ As ↔* Bs) → (K ∋ τ⟦ τ ⟧ As ↔ τ⟦ τ ⟧ Bs)
τ⟦ zero ⟧²  (ℜ , ℜs)  = ℜ
τ⟦ suc τ ⟧² (ℜ , ℜs)  = τ⟦ τ ⟧² ℜs

-- Type constants

data TConst : Kind → Set where
  prod fun : ∀ {α β} → TConst (set α ⇒ (set β ⇒ set (α ⊔ β)))
  leq : TConst (time ⇒ (time ⇒ set o))
  univ : ∀ K {α} → TConst ((K ⇒ set α) ⇒ set (level K ⊔ α))

C⟦_⟧ : ∀ {K} → (TConst K) → K⟦ K ⟧
C⟦ prod ⟧   = λ A B → (A × B)
C⟦ fun ⟧    = λ A B → (A → B)
C⟦ leq ⟧    = λ t u → True (t ≤ u)
C⟦ univ K ⟧ = λ F → ∀ A → F A

C⟦_⟧² : ∀ {K} (C : TConst K) → (K ∋ C⟦ C ⟧ ↔ C⟦ C ⟧)
C⟦ prod ⟧²   = λ ℜ ℑ → (ℜ ×² ℑ)
C⟦ fun ⟧²    = λ ℜ ℑ → (ℜ →² ℑ)
C⟦ leq ⟧²    = λ _ _ _ _ → ⊤
C⟦ univ K ⟧² = λ ℜ f g → ∀ {a b} ℑ → ℜ ℑ (f a) (g b)

-- Types

data Typ (Σ : Kinds) : Kind → Set where
  const : ∀ {K} → TConst K → Typ Σ K
  abs : ∀ K {L} → Typ (K ∷ Σ) L → Typ Σ (K ⇒ L)
  app : ∀ {K L} → Typ Σ (K ⇒ L) → Typ Σ K → Typ Σ L
  var : ∀ {K} → TVar K Σ → Typ Σ K

tlevel : ∀ {Σ α} → Typ Σ (set α) → Level
tlevel {Σ} {α} T = α

T⟦_⟧ : ∀ {Σ K} (T : Typ Σ K) → Σ⟦ Σ ⟧ → K⟦ K ⟧
T⟦ const C ⟧ As  = C⟦ C ⟧
T⟦ abs K T ⟧ As  = λ A → T⟦ T ⟧ (A , As)
T⟦ app T U ⟧ As  = T⟦ T ⟧ As (T⟦ U ⟧ As)
T⟦ var τ ⟧ As    = τ⟦ τ ⟧ As

T⟦_⟧² : ∀ {Σ K} (T : Typ Σ K) {As Bs} → (Σ ∋ As ↔* Bs) → (K ∋ T⟦ T ⟧ As ↔ T⟦ T ⟧ Bs)
T⟦ const C ⟧² ℜs  = C⟦ C ⟧²
T⟦ abs K T ⟧² ℜs  = λ ℜ → T⟦ T ⟧² (ℜ , ℜs)
T⟦ app T U ⟧² ℜs  = T⟦ T ⟧² ℜs (T⟦ U ⟧² ℜs)
T⟦ var τ ⟧² ℜs    = τ⟦ τ ⟧² ℜs

-- Type shorthands

app₂ :  ∀ {Σ K L M} → Typ Σ (K ⇒ (L ⇒ M)) → Typ Σ K → Typ Σ L → Typ Σ M
app₂ T U V = app (app T U) V

capp :  ∀ {Σ K L} → TConst (K ⇒ L) → Typ Σ K → Typ Σ L
capp C = app (const C)

capp₂ :  ∀ {Σ K L M} → TConst (K ⇒ (L ⇒ M)) → Typ Σ K → Typ Σ L → Typ Σ M
capp₂ C = app₂ (const C)

_⊗_ : ∀ {Σ α β} → Typ Σ (set α) → Typ Σ (set β) → Typ Σ (set (α ⊔ β))
_⊗_ = capp₂ prod

_⊸_ : ∀ {Σ α β} → Typ Σ (set α) → Typ Σ (set β) → Typ Σ (set (α ⊔ β))
_⊸_ = capp₂ fun

_≼_ : ∀ {Σ} → Typ Σ time → Typ Σ time → Typ Σ (set o)
_≼_ = capp₂ leq

Π : ∀ {Σ α} K → Typ (K ∷ Σ) (set α) → Typ Σ (set (level K ⊔ α))
Π K T = capp (univ K) (abs K T)

tvar₀ : ∀ {Σ K} → Typ (K ∷ Σ) K
tvar₀ = var zero

tvar₁ : ∀ {Σ K L} → Typ (L ∷ K ∷ Σ) K
tvar₁ = var (suc zero)

tvar₂ : ∀ {Σ K L M} → Typ (M ∷ L ∷ K ∷ Σ) K
tvar₂ = var (suc (suc zero))

tvar₃ : ∀ {Σ K L M N} → Typ (N ∷ M ∷ L ∷ K ∷ Σ) K
tvar₃ = var (suc (suc (suc zero)))

rset : Level → Kind
rset α = time ⇒ set α

rset₀ : Kind
rset₀ = rset o

prodʳ : ∀ {Σ α β} → Typ Σ (rset α ⇒ (rset β ⇒ rset (α ⊔ β)))
prodʳ {Σ} {α} {β} = abs (rset α) (abs (rset β) (abs time (app tvar₂ tvar₀ ⊗ app tvar₁ tvar₀)))

_⊗ʳ_ : ∀ {Σ α β} → Typ Σ (rset α) → Typ Σ (rset β) → Typ Σ (rset (α ⊔ β))
_⊗ʳ_ = app₂ prodʳ

funʳ : ∀ {Σ α β} → Typ Σ (rset α ⇒ (rset β ⇒ rset (α ⊔ β)))
funʳ {Σ} {α} {β} = abs (rset α) (abs (rset β) (abs time (app tvar₂ tvar₀ ⊸ app tvar₁ tvar₀)))

_⊸ʳ_ : ∀ {Σ α β} → Typ Σ (rset α) → Typ Σ (rset β) → Typ Σ (rset (α ⊔ β))
_⊸ʳ_ = app₂ funʳ

always : ∀ {Σ α} → Typ Σ (set α ⇒ rset α)
always {Σ} {α} = abs (set α) (abs time tvar₁)

interval : ∀ {Σ α} → Typ Σ (rset α ⇒ (time ⇒ (time ⇒ set α)))
interval {Σ} {α} = abs (rset α) (abs time (abs time (Π time
  ((tvar₂ ≼ tvar₀) ⊸ ((tvar₀ ≼ tvar₁) ⊸ app tvar₃ tvar₀)))))

_[_,_] : ∀ {Σ α} → Typ Σ (rset α) → Typ Σ time → Typ Σ time → Typ Σ (set α)
T [ t , u ] = app (app (app interval T) t) u

constreq : ∀ {Σ α β} → Typ Σ (rset α ⇒ (rset β ⇒ rset (α ⊔ β)))
constreq {Σ} {α} {β} = abs (rset α) (abs (rset β) (abs time (Π time
  ((tvar₁ ≼ tvar₀) ⊸ ((tvar₃ [ tvar₁ , tvar₀ ]) ⊸ app tvar₂ tvar₀)))))

_⊵_ : ∀ {Σ α β} → Typ Σ (rset α) → Typ Σ (rset β) → Typ Σ (rset (α ⊔ β))
T ⊵ U = app₂ constreq T U

-- Contexts

data Typs (Σ : Kinds) : Set where
  [] : Typs Σ
  _∷_ : ∀ {α} → (Typ Σ (set α)) → Typs Σ → Typs Σ

tlevels : ∀ {Σ} → Typs Σ → Level
tlevels []       = o
tlevels (T ∷ Γ) = tlevel T ⊔ tlevels Γ

Γ⟦_⟧ : ∀ {Σ} (Γ : Typs Σ) → Σ⟦ Σ ⟧ → Set (tlevels Γ)
Γ⟦ [] ⟧    As = ⊤
Γ⟦ T ∷ Γ ⟧ As = T⟦ T ⟧ As × Γ⟦ Γ ⟧ As

Γ⟦_⟧² : ∀ {Σ} (Γ : Typs Σ) {As Bs} (ℜs : Σ ∋ As ↔* Bs) → (Γ⟦ Γ ⟧ As → Γ⟦ Γ ⟧ Bs → Set (tlevels Γ))
Γ⟦ [] ⟧²    ℜs tt       tt       = ⊤
Γ⟦ T ∷ Γ ⟧² ℜs (a , as) (b , bs) = T⟦ T ⟧² ℜs a b × Γ⟦ Γ ⟧² ℜs as bs

-- Weakening of type variables

τweaken : ∀ {Σ Υ K} → (Σ ⊑ Υ) → TVar K Σ → TVar K Υ
τweaken id           x       = x
τweaken (keep K Σ⊑Υ) zero    = zero
τweaken (keep K Σ⊑Υ) (suc x) = suc (τweaken Σ⊑Υ x)
τweaken (skip K Σ⊑Υ) x       = suc (τweaken Σ⊑Υ x)

τweaken⟦_⟧ : ∀ {Σ Υ K} (τ : TVar K Σ) (Σ⊑Υ : Σ ⊑ Υ) (As : Σ⟦ Υ ⟧) →
  τ⟦ τ ⟧ (⊑⟦ Σ⊑Υ ⟧ As) ≡ τ⟦ τweaken Σ⊑Υ τ ⟧ As
τweaken⟦ τ ⟧     id           As       = refl
τweaken⟦ zero ⟧  (keep K Σ⊑Υ) (A , As) = refl
τweaken⟦ suc τ ⟧ (keep K Σ⊑Υ) (A , As) = τweaken⟦ τ ⟧ Σ⊑Υ As
τweaken⟦ τ ⟧     (skip K Σ⊑Υ) (A , As) = τweaken⟦ τ ⟧ Σ⊑Υ As

τweaken⟦_⟧² : ∀ {Σ Υ K} (τ : TVar K Σ) (Σ⊑Υ : Σ ⊑ Υ) {As Bs} (ℜs : Υ ∋ As ↔* Bs) →
  τ⟦ τ ⟧² (⊑⟦ Σ⊑Υ ⟧² ℜs) ≡
    struct K (τweaken⟦ τ ⟧ Σ⊑Υ As) (τ⟦ τweaken Σ⊑Υ τ ⟧² ℜs) (τweaken⟦ τ ⟧ Σ⊑Υ Bs)
τweaken⟦ τ ⟧²     id           ℜs       = refl
τweaken⟦ zero ⟧²  (keep K Σ⊑Υ) (ℜ , ℜs) = refl
τweaken⟦ suc τ ⟧² (keep K Σ⊑Υ) (ℜ , ℜs) = τweaken⟦ τ ⟧² Σ⊑Υ ℜs
τweaken⟦ τ ⟧²     (skip K Σ⊑Υ) (ℜ , ℜs) = τweaken⟦ τ ⟧² Σ⊑Υ ℜs

-- Weakening of types

weaken : ∀ {Σ Υ K} → (Σ ⊑ Υ) → Typ Σ K → Typ Υ K
weaken Σ⊑Υ (const C)  = const C
weaken Σ⊑Υ (abs K T)  = abs K (weaken (keep K Σ⊑Υ) T)
weaken Σ⊑Υ (app T U)  = app (weaken Σ⊑Υ T) (weaken Σ⊑Υ U)
weaken Σ⊑Υ (var τ)    = var (τweaken Σ⊑Υ τ)

weaken⟦_⟧ : ∀ {Σ Υ K} (T : Typ Σ K) (Σ⊑Υ : Σ ⊑ Υ) (As : Σ⟦ Υ ⟧) →
  T⟦ T ⟧ (⊑⟦ Σ⊑Υ ⟧ As) ≡ T⟦ weaken Σ⊑Υ T ⟧ As
weaken⟦ const C ⟧ Σ⊑Υ As = refl
weaken⟦ abs K T ⟧ Σ⊑Υ As = ext (λ A → weaken⟦ T ⟧ (keep K Σ⊑Υ) (A , As))
weaken⟦ app T U ⟧ Σ⊑Υ As = apply (weaken⟦ T ⟧ Σ⊑Υ As) (weaken⟦ U ⟧ Σ⊑Υ As)
weaken⟦ var τ ⟧   Σ⊑Υ As = τweaken⟦ τ ⟧ Σ⊑Υ As

weaken⟦_⟧² : ∀ {Σ Υ K} (T : Typ Σ K) (Σ⊑Υ : Σ ⊑ Υ) {As Bs} (ℜs : Υ ∋ As ↔* Bs) →
  T⟦ T ⟧² (⊑⟦ Σ⊑Υ ⟧² ℜs) ≡ struct K (weaken⟦ T ⟧ Σ⊑Υ As) (T⟦ weaken Σ⊑Υ T ⟧² ℜs) (weaken⟦ T ⟧ Σ⊑Υ Bs)
weaken⟦ const C ⟧² Σ⊑Υ ℜs = refl
weaken⟦ abs K {L} T ⟧² Σ⊑Υ {As} {Bs} ℜs =
  iext (λ A → iext (λ B → ext (λ ℜ → begin
    T⟦ abs K T ⟧² (⊑⟦ Σ⊑Υ ⟧² ℜs) ℜ
  ≡⟨ weaken⟦ T ⟧² (keep K Σ⊑Υ) (ℜ , ℜs) ⟩
    struct L
      (weaken⟦ T ⟧ (keep K Σ⊑Υ) (A , As))
      (T⟦ weaken (keep K Σ⊑Υ) T ⟧² (ℜ , ℜs))
      (weaken⟦ T ⟧ (keep K Σ⊑Υ) (B , Bs))
  ≡⟨ struct-ext K L
       (λ A → weaken⟦ T ⟧ (keep K Σ⊑Υ) (A , As))
       (λ ℜ → T⟦ weaken (keep K Σ⊑Υ) T ⟧² (ℜ , ℜs))
       (λ B → weaken⟦ T ⟧ (keep K Σ⊑Υ) (B , Bs)) ℜ ⟩
    struct (K ⇒ L)
      (weaken⟦ abs K T ⟧ Σ⊑Υ As)
      (T⟦ weaken Σ⊑Υ (abs K T) ⟧² ℜs)
      (weaken⟦ abs K T ⟧ Σ⊑Υ Bs) ℜ
  ∎)))
weaken⟦ app {K} {L} T U ⟧² Σ⊑Υ {As} {Bs} ℜs =
  begin
    T⟦ app T U ⟧² (⊑⟦ Σ⊑Υ ⟧² ℜs)
  ≡⟨ cong (T⟦ T ⟧² (⊑⟦ Σ⊑Υ ⟧² ℜs)) (weaken⟦ U ⟧² Σ⊑Υ ℜs) ⟩
    T⟦ T ⟧² (⊑⟦ Σ⊑Υ ⟧² ℜs)
      (struct K (weaken⟦ U ⟧ Σ⊑Υ As) (T⟦ weaken Σ⊑Υ U ⟧² ℜs) (weaken⟦ U ⟧ Σ⊑Υ Bs))
  ≡⟨ cong (λ X → X (struct K (weaken⟦ U ⟧ Σ⊑Υ As) (T⟦ weaken Σ⊑Υ U ⟧² ℜs) (weaken⟦ U ⟧ Σ⊑Υ Bs)))
       (weaken⟦ T ⟧² Σ⊑Υ ℜs) ⟩
    (struct (K ⇒ L) (weaken⟦ T ⟧ Σ⊑Υ As) (T⟦ weaken Σ⊑Υ T ⟧² ℜs) (weaken⟦ T ⟧ Σ⊑Υ Bs))
      (struct K (weaken⟦ U ⟧ Σ⊑Υ As) (T⟦ weaken Σ⊑Υ U ⟧² ℜs) (weaken⟦ U ⟧ Σ⊑Υ Bs))
  ≡⟨ struct-apply K L
       (weaken⟦ T ⟧ Σ⊑Υ As) (T⟦ weaken Σ⊑Υ T ⟧² ℜs) (weaken⟦ T ⟧ Σ⊑Υ Bs)
       (weaken⟦ U ⟧ Σ⊑Υ As) (T⟦ weaken Σ⊑Υ U ⟧² ℜs) (weaken⟦ U ⟧ Σ⊑Υ Bs) ⟩
    struct L
      (weaken⟦ app T U ⟧ Σ⊑Υ As)
      (T⟦ weaken Σ⊑Υ (app T U) ⟧² ℜs)
      (weaken⟦ app T U ⟧ Σ⊑Υ Bs)
  ∎
weaken⟦ var τ ⟧² Σ⊑Υ ℜs = τweaken⟦ τ ⟧² Σ⊑Υ ℜs

-- Weakening on type contexts

weakens : ∀ {Σ Υ} → (Σ ⊑ Υ) → Typs Σ → Typs Υ
weakens Σ⊑Υ []      = []
weakens Σ⊑Υ (T ∷ Γ) = weaken Σ⊑Υ T ∷ weakens Σ⊑Υ Γ

weakens⟦_⟧ : ∀ {Σ Υ} (Γ : Typs Σ) (Σ⊑Υ : Σ ⊑ Υ) (As : Σ⟦ Υ ⟧) →
  Γ⟦ Γ ⟧ (⊑⟦ Σ⊑Υ ⟧ As) → Γ⟦ weakens Σ⊑Υ Γ ⟧ As
weakens⟦ [] ⟧    Σ⊑Υ As tt       = tt
weakens⟦ T ∷ Γ ⟧ Σ⊑Υ As (B , Bs) = (cast (weaken⟦ T ⟧ Σ⊑Υ As) B , weakens⟦ Γ ⟧ Σ⊑Υ As Bs)

weakens⟦_⟧² : ∀ {Σ Υ} (Γ : Typs Σ) (Σ⊑Υ : Σ ⊑ Υ) {As Bs} (ℜs : Υ ∋ As ↔* Bs) {as bs} →
  Γ⟦ Γ ⟧² (⊑⟦ Σ⊑Υ ⟧² ℜs) as bs →
  Γ⟦ weakens Σ⊑Υ Γ ⟧² ℜs (weakens⟦ Γ ⟧ Σ⊑Υ As as) (weakens⟦ Γ ⟧ Σ⊑Υ Bs bs)
weakens⟦ [] ⟧²    Σ⊑Υ ℜs tt
  = tt
weakens⟦ T ∷ Γ ⟧² Σ⊑Υ ℜs (aℜb , asℜbs)
  = ( struct-cast (T⟦ weaken Σ⊑Υ T ⟧² ℜs)
        (weaken⟦ T ⟧ Σ⊑Υ _) (weaken⟦ T ⟧ Σ⊑Υ _) (cast² (weaken⟦ T ⟧² Σ⊑Υ ℜs) aℜb)
    , weakens⟦ Γ ⟧² Σ⊑Υ ℜs asℜbs)

-- Susbtitution on type variables under a context

τsubstn+ : ∀ Σ {Υ K L} → TVar K (Σ ++ (L ∷ Υ)) → Typ Υ L → Typ (Σ ++ Υ) K
τsubstn+ []      zero    U = U
τsubstn+ []      (suc τ) U = var τ
τsubstn+ (K ∷ Σ) zero    U = var zero
τsubstn+ (K ∷ Σ) (suc τ) U = weaken (skip K id) (τsubstn+ Σ τ U)

τsubstn+_⟦_⟧⟦_⟧ : ∀ Σ {Υ K L} (τ : TVar K (Σ ++ (L ∷ Υ))) (U : Typ Υ L)
  (As : Σ⟦ Σ ⟧) (Bs : Σ⟦ Υ ⟧) →
    τ⟦ τ ⟧ (Σ ∋ As ++ (L ∷ Υ) ∋ (T⟦ U ⟧ Bs , Bs)) ≡
      T⟦ τsubstn+ Σ τ U ⟧ (Σ ∋ As ++ Υ ∋ Bs)
τsubstn+ []      ⟦ zero  ⟧⟦ U ⟧ tt       Bs = refl
τsubstn+ []      ⟦ suc τ ⟧⟦ U ⟧ tt       Bs = refl
τsubstn+ (K ∷ Σ) ⟦ zero  ⟧⟦ U ⟧ (A , As) Bs = refl
τsubstn+ (K ∷ Σ) ⟦ suc τ ⟧⟦ U ⟧ (A , As) Bs = trans
  (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ As Bs)
  (weaken⟦ τsubstn+ Σ τ U ⟧ (skip K id) (A , (Σ ∋ As ++ _ ∋ Bs)))

τsubstn+_⟦_⟧⟦_⟧² : ∀ Σ {Υ L K} (τ : TVar K (Σ ++ (L ∷ Υ))) (U : Typ Υ L) {As Bs Cs Ds}
  (ℜs : Σ ∋ As ↔* Bs) → (ℑs : Υ ∋ Cs ↔* Ds) →
    τ⟦ τ ⟧² (Σ ∋ ℜs ++² (L ∷ Υ) ∋ (T⟦ U ⟧² ℑs , ℑs)) ≡
      struct K
        (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ As Cs)
        (T⟦ τsubstn+ Σ τ U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs) )
        (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ Bs Ds)
τsubstn+ []      ⟦ zero  ⟧⟦ U ⟧² tt       ℑs = refl
τsubstn+ []      ⟦ suc τ ⟧⟦ U ⟧² tt       ℑs = refl
τsubstn+ (J ∷ Σ) ⟦ zero  ⟧⟦ U ⟧² (ℜ , ℜs) ℑs = refl
τsubstn+_⟦_⟧⟦_⟧² (J ∷ Σ) {Υ} {L} {K} (suc τ) U {A , As} {B , Bs} {Cs} {Ds} (ℜ , ℜs) ℑs =
  begin
    τ⟦ τ ⟧² (Σ ∋ ℜs ++² (L ∷ Υ) ∋ (T⟦ U ⟧² ℑs , ℑs))
  ≡⟨ τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧² ℜs ℑs ⟩
    struct K
      (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ As Cs)
      (T⟦ τsubstn+ Σ τ U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
      (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ Bs Ds)
  ≡⟨ cong (λ X → struct K (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ As Cs) X (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ Bs Ds))
       (weaken⟦ τsubstn+ Σ τ U ⟧² (skip J id) (ℜ , (Σ ∋ ℜs ++² Υ ∋ ℑs))) ⟩
    struct K
      (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ As Cs)
      (struct K
        (weaken⟦ τsubstn+ Σ τ U ⟧ (skip J id) (A , (Σ ∋ As ++ Υ ∋ Cs)))
        (T⟦ weaken (skip J id) (τsubstn+ Σ τ U) ⟧² (ℜ , (Σ ∋ ℜs ++² Υ ∋ ℑs)))
        (weaken⟦ τsubstn+ Σ τ U ⟧ (skip J id) (B , (Σ ∋ Bs ++ Υ ∋ Ds))))
      (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ Bs Ds)
  ≡⟨ struct-trans K
       (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ As Cs)
       (weaken⟦ τsubstn+ Σ τ U ⟧ (skip J id) (A , (Σ ∋ As ++ Υ ∋ Cs)))
       (T⟦ weaken (skip J id) (τsubstn+ Σ τ U) ⟧² (ℜ , (Σ ∋ ℜs ++² Υ ∋ ℑs)))
       (weaken⟦ τsubstn+ Σ τ U ⟧ (skip J id) (B , (Σ ∋ Bs ++ Υ ∋ Ds)))
       (τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ Bs Ds) ⟩
    struct K
      (τsubstn+ (J ∷ Σ) ⟦ suc τ ⟧⟦ U ⟧ (A , As) Cs)
      (T⟦ τsubstn+ (J ∷ Σ) (suc τ) U ⟧² (ℜ , (Σ ∋ ℜs ++² Υ ∋ ℑs)) )
      (τsubstn+ (J ∷ Σ) ⟦ suc τ ⟧⟦ U ⟧ (B , Bs) Ds)
  ∎

-- Substitution on types under a context

substn+ : ∀ Σ {Υ K L} → Typ (Σ ++ (L ∷ Υ)) K → Typ Υ L → Typ (Σ ++ Υ) K
substn+ Σ (const C) U = const C
substn+ Σ (abs K T) U = abs K (substn+ (K ∷ Σ) T U)
substn+ Σ (app S T) U = app (substn+ Σ S U) (substn+ Σ T U)
substn+ Σ (var τ)   U = τsubstn+ Σ τ U

substn+_⟦_⟧⟦_⟧ : ∀ Σ {Υ K L} (T : Typ (Σ ++ (L ∷ Υ)) K) (U : Typ Υ L)
  (As : Σ⟦ Σ ⟧) (Bs : Σ⟦ Υ ⟧) →
    T⟦ T ⟧ (Σ ∋ As ++ (L ∷ Υ) ∋ (T⟦ U ⟧ Bs , Bs)) ≡
      T⟦ substn+ Σ T U ⟧ (Σ ∋ As ++ Υ ∋ Bs)
substn+ Σ ⟦ const C ⟧⟦ U ⟧ As Bs = refl
substn+ Σ ⟦ abs K T ⟧⟦ U ⟧ As Bs = ext (λ A → substn+ K ∷ Σ ⟦ T ⟧⟦ U ⟧ (A , As) Bs)
substn+ Σ ⟦ app S T ⟧⟦ U ⟧ As Bs = apply (substn+ Σ ⟦ S ⟧⟦ U ⟧ As Bs) (substn+ Σ ⟦ T ⟧⟦ U ⟧ As Bs)
substn+ Σ ⟦ var τ   ⟧⟦ U ⟧ As Bs = τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧ As Bs

substn+_⟦_⟧⟦_⟧² : ∀ Σ {Υ L K} (T : Typ (Σ ++ (L ∷ Υ)) K) (U : Typ Υ L) {As Bs Cs Ds}
  (ℜs : Σ ∋ As ↔* Bs) → (ℑs : Υ ∋ Cs ↔* Ds) →
    T⟦ T ⟧² (Σ ∋ ℜs ++² (L ∷ Υ) ∋ (T⟦ U ⟧² ℑs , ℑs)) ≡
      struct K
        (substn+ Σ ⟦ T ⟧⟦ U ⟧ As Cs)
        (T⟦ substn+ Σ T U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs) )
        (substn+ Σ ⟦ T ⟧⟦ U ⟧ Bs Ds)
substn+ Σ ⟦ const C ⟧⟦ U ⟧² ℜs ℑs = refl
substn+_⟦_⟧⟦_⟧² Σ {Υ} {L} (abs J {K} T) U {As} {Bs} {Cs} {Ds} ℜs ℑs =
  iext (λ A → iext (λ B → ext (λ ℜ → begin
    T⟦ abs J T ⟧² (Σ ∋ ℜs ++² (L ∷ Υ) ∋ (T⟦ U ⟧² ℑs , ℑs)) ℜ
  ≡⟨ substn+ (J ∷ Σ) ⟦ T ⟧⟦ U ⟧² (ℜ , ℜs) ℑs ⟩
    struct K
      (substn+ J ∷ Σ ⟦ T ⟧⟦ U ⟧ (A , As) Cs)
      (T⟦ substn+ (J ∷ Σ) T U ⟧² ((J ∷ Σ) ∋ (ℜ , ℜs) ++² Υ ∋ ℑs))
      (substn+ J ∷ Σ ⟦ T ⟧⟦ U ⟧ (B , Bs) Ds)
  ≡⟨ struct-ext J K
       (λ A → substn+ J ∷ Σ ⟦ T ⟧⟦ U ⟧ (A , As) Cs)
       (λ ℜ → T⟦ substn+ (J ∷ Σ) T U ⟧² ((J ∷ Σ) ∋ ℜ , ℜs ++² Υ ∋ ℑs))
       (λ B → substn+ J ∷ Σ ⟦ T ⟧⟦ U ⟧ (B , Bs) Ds) ℜ ⟩
    struct (J ⇒ K)
      (substn+ Σ ⟦ abs J T ⟧⟦ U ⟧ As Cs)
      (T⟦ substn+ Σ (abs J T) U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
      (substn+ Σ ⟦ abs J T ⟧⟦ U ⟧ Bs Ds) ℜ
  ∎)))
substn+_⟦_⟧⟦_⟧² Σ {Υ} {L} (app {J} {K} S T) U {As} {Bs} {Cs} {Ds} ℜs ℑs =
  begin
    T⟦ app S T ⟧² (Σ ∋ ℜs ++² L ∷ Υ ∋ (T⟦ U ⟧² ℑs , ℑs))
  ≡⟨ cong (T⟦ S ⟧² (Σ ∋ ℜs ++² L ∷ Υ ∋ (T⟦ U ⟧² ℑs , ℑs))) (substn+ Σ ⟦ T ⟧⟦ U ⟧² ℜs ℑs) ⟩
    T⟦ S ⟧² (Σ ∋ ℜs ++² L ∷ Υ ∋ (T⟦ U ⟧² ℑs , ℑs))
      (struct J
         (substn+ Σ ⟦ T ⟧⟦ U ⟧ As Cs)
         (T⟦ substn+ Σ T U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
         (substn+ Σ ⟦ T ⟧⟦ U ⟧ Bs Ds))
  ≡⟨ cong (λ X → X (struct J
       (substn+ Σ ⟦ T ⟧⟦ U ⟧ As Cs)
       (T⟦ substn+ Σ T U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
       (substn+ Σ ⟦ T ⟧⟦ U ⟧ Bs Ds)))
       (substn+ Σ ⟦ S ⟧⟦ U ⟧² ℜs ℑs) ⟩
    struct (J ⇒ K)
      (substn+ Σ ⟦ S ⟧⟦ U ⟧ As Cs)
      (T⟦ substn+ Σ S U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
      (substn+ Σ ⟦ S ⟧⟦ U ⟧ Bs Ds)
      (struct J
         (substn+ Σ ⟦ T ⟧⟦ U ⟧ As Cs)
         (T⟦ substn+ Σ T U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
         (substn+ Σ ⟦ T ⟧⟦ U ⟧ Bs Ds))
  ≡⟨ struct-apply J K
       (substn+ Σ ⟦ S ⟧⟦ U ⟧ As Cs)
       (T⟦ substn+ Σ S U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
       (substn+ Σ ⟦ S ⟧⟦ U ⟧ Bs Ds)
       (substn+ Σ ⟦ T ⟧⟦ U ⟧ As Cs)
       (T⟦ substn+ Σ T U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
       (substn+ Σ ⟦ T ⟧⟦ U ⟧ Bs Ds) ⟩
    struct K
      (substn+ Σ ⟦ app S T ⟧⟦ U ⟧ As Cs)
      (T⟦ substn+ Σ (app S T) U ⟧² (Σ ∋ ℜs ++² Υ ∋ ℑs))
      (substn+ Σ ⟦ app S T ⟧⟦ U ⟧ Bs Ds)
  ∎
substn+ Σ ⟦ var τ ⟧⟦ U ⟧² ℜs ℑs = τsubstn+ Σ ⟦ τ ⟧⟦ U ⟧² ℜs ℑs

-- Substitution on types

substn : ∀ {Σ K L} → Typ (L ∷ Σ) K → Typ Σ L → Typ Σ K
substn = substn+ []

substn⟦_⟧⟦_⟧ : ∀ {Σ K L} (T : Typ (L ∷ Σ) K) (U : Typ Σ L) (As : Σ⟦ Σ ⟧)→
  T⟦ T ⟧ (T⟦ U ⟧ As , As) ≡ T⟦ substn T U ⟧ As
substn⟦ T ⟧⟦ U ⟧ = substn+ [] ⟦ T ⟧⟦ U ⟧ tt

substn⟦_⟧⟦_⟧² : ∀ {Σ K L} (T : Typ (L ∷ Σ) K) (U : Typ Σ L) {As Bs} (ℜs : Σ ∋ As ↔* Bs) →
  T⟦ T ⟧² (T⟦ U ⟧² ℜs , ℜs) ≡
    struct K (substn⟦ T ⟧⟦ U ⟧ As) (T⟦ substn T U ⟧² ℜs) (substn⟦ T ⟧⟦ U ⟧ Bs)
substn⟦ T ⟧⟦ U ⟧² = substn+ [] ⟦ T ⟧⟦ U ⟧² tt

-- Eta-beta equivalence on types

data _∋_≣_ {Σ} : ∀ K → Typ Σ K → Typ Σ K → Set where
  abs : ∀ K {L T U} → (L ∋ T ≣ U) → ((K ⇒ L) ∋ abs K T ≣ abs K U)
  app : ∀ {K L F G T U} → ((K ⇒ L) ∋ F ≣ G) → (K ∋ T ≣ U) → (L ∋ app F T ≣ app G U)
  beta : ∀ {K L} T U → (L ∋ app (abs K T) U ≣ substn T U)
  eta : ∀ {K L} T → ((K ⇒ L) ∋ T ≣ abs K (app (weaken (skip K id) T) tvar₀))
  ≣-refl : ∀ {K T} → (K ∋ T ≣ T)
  ≣-sym : ∀ {K T U} → (K ∋ T ≣ U) → (K ∋ U ≣ T)
  ≣-trans : ∀ {K T U V} → (K ∋ T ≣ U) → (K ∋ U ≣ V) → (K ∋ T ≣ V)

≣⟦_⟧ : ∀ {Σ K} {T U : Typ Σ K} → (K ∋ T ≣ U) → ∀ As → T⟦ T ⟧ As ≡ T⟦ U ⟧ As
≣⟦ abs K T≣U ⟧       As = ext (λ A → ≣⟦ T≣U ⟧ (A , As))
≣⟦ app F≣G T≣U ⟧     As = apply (≣⟦ F≣G ⟧ As) (≣⟦ T≣U ⟧ As)
≣⟦ beta T U ⟧        As = substn⟦ T ⟧⟦ U ⟧ As
≣⟦ eta {K} T ⟧       As = ext (λ A → apply (weaken⟦ T ⟧ (skip K id) (A , As)) refl)
≣⟦ ≣-refl ⟧          As = refl
≣⟦ ≣-sym T≣U ⟧       As = sym (≣⟦ T≣U ⟧ As)
≣⟦ ≣-trans T≣U U≣V ⟧ As = trans (≣⟦ T≣U ⟧ As) (≣⟦ U≣V ⟧ As)

≣⟦_⟧² : ∀ {Σ K} {T U : Typ Σ K} (T≣U : K ∋ T ≣ U) {As Bs} (ℜs : Σ ∋ As ↔* Bs) →
  T⟦ T ⟧² ℜs ≡ struct K (≣⟦ T≣U ⟧ As) (T⟦ U ⟧² ℜs) (≣⟦ T≣U ⟧ Bs)
≣⟦ abs K {L} {T} {U} T≣U ⟧² {As} {Bs} ℜs =
  iext (λ A → iext (λ B → ext (λ ℜ → begin
    T⟦ T ⟧² (ℜ , ℜs)
  ≡⟨ ≣⟦ T≣U ⟧² (ℜ , ℜs) ⟩
    struct L (≣⟦ T≣U ⟧ (A , As)) (T⟦ U ⟧² (ℜ , ℜs)) (≣⟦ T≣U ⟧ (B , Bs))
  ≡⟨ struct-ext K L (λ A → ≣⟦ T≣U ⟧ (A , As)) (λ ℜ' → T⟦ U ⟧² (ℜ' , ℜs)) (λ B → ≣⟦ T≣U ⟧ (B , Bs)) ℜ ⟩
    struct (K ⇒ L) (≣⟦ abs K T≣U ⟧ As) (T⟦ abs K U ⟧² ℜs) (≣⟦ abs K T≣U ⟧ Bs) ℜ
  ∎)))
≣⟦ app {K} {L} {F} {G} {T} {U} F≣G T≣U ⟧² {As} {Bs} ℜs =
  begin
    T⟦ app F T ⟧² ℜs
  ≡⟨ cong (T⟦ F ⟧² ℜs) (≣⟦ T≣U ⟧² ℜs) ⟩
    T⟦ F ⟧² ℜs (struct K (≣⟦ T≣U ⟧ As) (T⟦ U ⟧² ℜs) (≣⟦ T≣U ⟧ Bs))
  ≡⟨ cong (λ X → X (struct K (≣⟦ T≣U ⟧ As) (T⟦ U ⟧² ℜs) (≣⟦ T≣U ⟧ Bs)))
       (≣⟦ F≣G ⟧² ℜs) ⟩
    struct (K ⇒ L) (≣⟦ F≣G ⟧ As) (T⟦ G ⟧² ℜs) (≣⟦ F≣G ⟧ Bs)
      (struct K (≣⟦ T≣U ⟧ As) (T⟦ U ⟧² ℜs) (≣⟦ T≣U ⟧ Bs))
  ≡⟨ struct-apply K L
       (≣⟦ F≣G ⟧ As) (T⟦ G ⟧² ℜs) (≣⟦ F≣G ⟧ Bs)
       (≣⟦ T≣U ⟧ As) (T⟦ U ⟧² ℜs) (≣⟦ T≣U ⟧ Bs) ⟩
    struct L (≣⟦ app F≣G T≣U ⟧ As) (T⟦ app G U ⟧² ℜs) (≣⟦ app F≣G T≣U ⟧ Bs)
  ∎
≣⟦ beta T U ⟧² ℜs = substn⟦ T ⟧⟦ U ⟧² ℜs
≣⟦ eta {K} {L} T ⟧² {As} {Bs} ℜs = iext (λ A → iext (λ B → ext (λ ℜ →
  begin
    T⟦ T ⟧² ℜs ℜ
  ≡⟨ cong (λ X → X ℜ) (weaken⟦ T ⟧² (skip K id) (ℜ , ℜs)) ⟩
    struct (K ⇒ L)
      (weaken⟦ T ⟧ (skip K id) (A , As))
      (T⟦ weaken (skip K id) T ⟧² (ℜ , ℜs))
      (weaken⟦ T ⟧ (skip K id) (B , Bs)) ℜ
  ≡⟨ struct-apply K L
       (weaken⟦ T ⟧ (skip K id) (A , As))
       (T⟦ weaken (skip K id) T ⟧² (ℜ , ℜs))
       (weaken⟦ T ⟧ (skip K id) (B , Bs)) refl ℜ refl ⟩
    struct L
      (apply (weaken⟦ T ⟧ (skip K id) (A , As)) refl)
      (T⟦ weaken (skip K id) T ⟧² (ℜ , ℜs) ℜ)
      (apply (weaken⟦ T ⟧ (skip K id) (B , Bs)) refl)
  ≡⟨ struct-ext K L
       (λ A → apply (weaken⟦ T ⟧ (skip K id) (A , As)) refl)
       (λ ℜ → T⟦ weaken (skip K id) T ⟧² (ℜ , ℜs) ℜ)
       (λ B → apply (weaken⟦ T ⟧ (skip K id) (B , Bs)) refl) ℜ ⟩
    struct (K ⇒ L)
      (≣⟦ eta T ⟧ As)
      (T⟦ abs K (app (weaken (skip K id) T) (var zero)) ⟧² ℜs)
      (≣⟦ eta T ⟧ Bs) ℜ
  ∎)))
≣⟦ ≣-refl ⟧² ℜs = refl
≣⟦ ≣-sym {K} {T} {U} T≣U ⟧² {As} {Bs} ℜs =
  struct-sym K (≣⟦ T≣U ⟧ As) (≣⟦ T≣U ⟧ Bs) (≣⟦ T≣U ⟧² ℜs)
≣⟦ ≣-trans {K} {T} {U} {V} T≣U U≣V ⟧² {As} {Bs} ℜs =
  begin
    T⟦ T ⟧² ℜs
  ≡⟨ ≣⟦ T≣U ⟧² ℜs ⟩
    struct K (≣⟦ T≣U ⟧ As) (T⟦ U ⟧² ℜs) (≣⟦ T≣U ⟧ Bs)
  ≡⟨ cong (λ X → struct K (≣⟦ T≣U ⟧ As) X (≣⟦ T≣U ⟧ Bs)) (≣⟦ U≣V ⟧² ℜs) ⟩
    struct K (≣⟦ T≣U ⟧ As) (struct K (≣⟦ U≣V ⟧ As) (T⟦ V ⟧² ℜs) (≣⟦ U≣V ⟧ Bs)) (≣⟦ T≣U ⟧ Bs)
  ≡⟨ struct-trans K (≣⟦ T≣U ⟧ As) (≣⟦ U≣V ⟧ As) (T⟦ V ⟧² ℜs) (≣⟦ U≣V ⟧ Bs) (≣⟦ T≣U ⟧ Bs) ⟩
    struct K (≣⟦ ≣-trans T≣U U≣V ⟧ As) (T⟦ V ⟧² ℜs) (≣⟦ ≣-trans T≣U U≣V ⟧ Bs)
  ∎

-- Variables

data Var {Σ : Kinds} {α} (T : Typ Σ (set α)) : Typs Σ → Set where
  zero : ∀ {Γ} → Var T (T ∷ Γ)
  suc : ∀ {β Γ} {U : Typ Σ (set β)} → Var T Γ → Var T (U ∷ Γ)

x⟦_⟧ : ∀ {Σ} {Γ : Typs Σ} {α} {T : Typ Σ (set α)} →
  Var T Γ → (As : Σ⟦ Σ ⟧) → (as : Γ⟦ Γ ⟧ As) → (T⟦ T ⟧ As)
x⟦ zero ⟧  As (a , as) = a
x⟦ suc x ⟧ As (a , as) = x⟦ x ⟧ As as

x⟦_⟧² : ∀ {Σ} {Γ : Typs Σ} {α} {T : Typ Σ (set α)} (x : Var T Γ) →
  ∀ {As Bs} (ℜs : Σ ∋ As ↔* Bs) {as bs} →
    (Γ⟦ Γ ⟧² ℜs as bs) → (T⟦ T ⟧² ℜs (x⟦ x ⟧ As as) (x⟦ x ⟧ Bs bs))
x⟦ zero ⟧²  ℜs (aℜb , asℜbs) = aℜb
x⟦ suc x ⟧² ℜs (aℜb , asℜbs) = x⟦ x ⟧² ℜs asℜbs

-- Constants

data Const {Σ : Kinds} : ∀ {α} → Typ Σ (set α) → Set where
  pair : ∀ {α β} → Const (Π (set α) (Π (set β) (tvar₁ ⊸ (tvar₀ ⊸ (tvar₁ ⊗ tvar₀)))))
  fst : ∀ {α β} → Const (Π (set α) (Π (set β) ((tvar₁ ⊗ tvar₀) ⊸ tvar₁)))
  snd : ∀ {α β} → Const (Π (set α) (Π (set β) ((tvar₁ ⊗ tvar₀) ⊸ tvar₀)))
  ≼-refl : Const (Π time (tvar₀ ≼ tvar₀))
  ≼-trans : Const (Π time (Π time (Π time ((tvar₂ ≼ tvar₁) ⊸ ((tvar₁ ≼ tvar₀) ⊸ (tvar₂ ≼ tvar₀))))))
  ≼-antisym : ∀ {α} → Const (Π (rset α) (Π time (Π time ((tvar₁ ≼ tvar₀) ⊸ ((tvar₀ ≼ tvar₁) ⊸ (app tvar₂ tvar₁ ⊸ app tvar₂ tvar₀))))))
  ≼-case : ∀ {α} → Const (Π (set α) (Π time (Π time (((tvar₁ ≼ tvar₀) ⊸ tvar₂) ⊸ (((tvar₀ ≼ tvar₁) ⊸ tvar₂) ⊸ tvar₂)))))

≤-antisym : ∀ {α} (A : RSet α) t u → True (t ≤ u) → True (u ≤ t) → A t → A u
≤-antisym A t u t≤u u≤t a with ≤-asym t u t≤u u≤t
≤-antisym A t .t _   _  a | refl = a

≤-case′ : ∀ {α} {A : Set α} {t u} → (t ≤? u) → (True (t ≤ u) → A) → (True (u ≤ t) → A) → A
≤-case′ (leq t≤u) f g = f t≤u
≤-case′ (geq u≤t) f g = g u≤t

≤-case : ∀ {α} (A : Set α) t u → (True (t ≤ u) → A) → (True (u ≤ t) → A) → A
≤-case A t u = ≤-case′ (≤-total t u)

c⟦_⟧ : ∀ {Σ} {α} {T : Typ Σ (set α)} →
  Const T → (As : Σ⟦ Σ ⟧) → (T⟦ T ⟧ As)
c⟦ pair ⟧      As = λ A B a b → (a , b)
c⟦ fst ⟧       As = λ A B → proj₁
c⟦ snd ⟧       As = λ A B → proj₂
c⟦ ≼-refl ⟧    As = ≤-refl
c⟦ ≼-trans ⟧   As = ≤-trans
c⟦ ≼-antisym ⟧ As = ≤-antisym
c⟦ ≼-case ⟧    As = ≤-case

c⟦_⟧² : ∀ {Σ} {α} {T : Typ Σ (set α)} (c : Const T) →
  ∀ {As Bs} (ℜs : Σ ∋ As ↔* Bs) →
    (T⟦ T ⟧² ℜs (c⟦ c ⟧ As) (c⟦ c ⟧ Bs))
c⟦ pair ⟧²          ℜs = λ ℜ ℑ aℜb cℑd → (aℜb , cℑd)
c⟦ fst ⟧²           ℜs = λ ℜ ℑ → proj₁
c⟦ snd ⟧²           ℜs = λ ℜ ℑ → proj₂
c⟦ ≼-refl ⟧²        ℜs = _
c⟦ ≼-trans ⟧²       ℜs = _
c⟦ ≼-antisym {α} ⟧² ℜs = lemma where
  lemma : ∀ {α} {A B : RSet α} (ℜ : rset α ∋ A ↔ B) →
    {t u : Time} → (t≡u : t ≡ u) → {v w : Time} → (v≡w : v ≡ w) →
    {t≤v : True (t ≤ v)} {u≤w : True (u ≤ w)} → ⊤ →
    {v≤t : True (v ≤ t)} {w≤u : True (w ≤ u)} → ⊤ →
    {a : A t} {b : B u} → ℜ t≡u a b →
    ℜ v≡w (≤-antisym A t v t≤v v≤t a) (≤-antisym B u w u≤w w≤u b)
  lemma ℜ {t} refl {v} refl {t≤v} {u≤w} tt {v≤t} {w≤u} tt aℜb
    with irrel (t ≤ v) t≤v u≤w | irrel (v ≤ t) v≤t w≤u
  lemma ℜ {t} refl {v} refl {t≤v} tt {v≤t} tt aℜb
    | refl | refl with ≤-asym t v t≤v v≤t
  lemma ℜ refl refl tt tt aℜb
    | refl | refl | refl = aℜb
c⟦ ≼-case {α} ⟧²    ℜs = lemma where
  lemma : ∀ {α} {A B : Set α} (ℜ : set α ∋ A ↔ B) →
    ∀ {t u : Time} → (t≡u : t ≡ u) → ∀ {v w : Time} → (v≡w : v ≡ w) →
    ∀ {f g} → (∀ {t≤v} {u≤w} → ⊤ → ℜ (f t≤v) (g u≤w)) →
    ∀ {h i} → (∀ {v≤t} {w≤u} → ⊤ → ℜ (h v≤t) (i w≤u)) →
    ℜ (≤-case A t v f h) (≤-case B u w g i)
  lemma ℜ {t} refl {v} refl {f} {g} fℜg {h} {i} hℜi = lemma′ (≤-total t v) where
    lemma′ : ∀ t≤?v → ℜ (≤-case′ t≤?v f h) (≤-case′ t≤?v g i)
    lemma′ (leq t≤v) = fℜg {t≤v} {t≤v} tt
    lemma′ (geq v≤t) = hℜi {v≤t} {v≤t} tt

-- Expressions

data Exp {Σ : Kinds} (Γ : Typs Σ) : ∀ {α} → Typ Σ (set α) → Set where
  const : ∀ {α} {T : Typ Σ (set α)} → Const T → Exp Γ T
  abs : ∀ {α β} (T : Typ Σ (set α)) {U : Typ Σ (set β)} (M : Exp (T ∷ Γ) U) → Exp Γ (T ⊸ U)
  app : ∀ {α β} {T : Typ Σ (set α)} {U : Typ Σ (set β)} (M : Exp Γ (T ⊸ U)) (N : Exp Γ T) → Exp Γ U
  var : ∀ {α} {T : Typ Σ (set α)} → Var T Γ → Exp Γ T
  tabs : ∀ K {α} {T : Typ (K ∷ Σ) (set α)} (M : Exp (weakens (skip K id) Γ) T) → Exp Γ (Π K T)
  tapp : ∀ {K α} {T : Typ (K ∷ Σ) (set α)} → Exp Γ (Π K T) → ∀ U → Exp Γ (substn T U)
  eq : ∀ {α T U} → (set α ∋ T ≣ U) → (Exp Γ T) → (Exp Γ U)

ctxt : ∀ {Σ Γ α T} → Exp {Σ} Γ {α} T → Typs Σ
ctxt {Σ} {Γ} M = Γ

M⟦_⟧ : ∀ {Σ} {Γ : Typs Σ} {α} {T : Typ Σ (set α)} →
  Exp Γ T → (As : Σ⟦ Σ ⟧) → (as : Γ⟦ Γ ⟧ As) → (T⟦ T ⟧ As)
M⟦ const c ⟧  As as = c⟦ c ⟧ As
M⟦ abs T M ⟧  As as = λ a → M⟦ M ⟧ As (a , as)
M⟦ app M N ⟧  As as = M⟦ M ⟧ As as (M⟦ N ⟧ As as)
M⟦ var x ⟧    As as = x⟦ x ⟧ As as
M⟦ tabs K M ⟧ As as = λ A →
  M⟦ M ⟧ (A , As) (weakens⟦ ctxt (tabs K M) ⟧ (skip K id) (A , As) as)
M⟦ tapp {T = T} M U ⟧ As as =
  cast (substn⟦ T ⟧⟦ U ⟧ As) (M⟦ M ⟧ As as (T⟦ U ⟧ As))
M⟦ eq T≣U M ⟧ As as = cast (≣⟦ T≣U ⟧ As) (M⟦ M ⟧ As as)

M⟦_⟧² : ∀ {Σ} {Γ : Typs Σ} {α} {T : Typ Σ (set α)} (M : Exp Γ T) →
  ∀ {As Bs} (ℜs : Σ ∋ As ↔* Bs) {as bs} →
    (Γ⟦ Γ ⟧² ℜs as bs) → (T⟦ T ⟧² ℜs (M⟦ M ⟧ As as) (M⟦ M ⟧ Bs bs))
M⟦ const c ⟧²  ℜs asℜbs = c⟦ c ⟧² ℜs
M⟦ abs T M ⟧²  ℜs asℜbs = λ aℜb → M⟦ M ⟧² ℜs (aℜb , asℜbs)
M⟦ app M N ⟧²  ℜs asℜbs = M⟦ M ⟧² ℜs asℜbs (M⟦ N ⟧² ℜs asℜbs)
M⟦ var x  ⟧²   ℜs asℜbs = x⟦ x ⟧² ℜs asℜbs
M⟦ tabs K M ⟧² ℜs asℜbs = λ ℜ →
  M⟦ M ⟧² (ℜ , ℜs) (weakens⟦ ctxt (tabs K M) ⟧² (skip K id) (ℜ , ℜs) asℜbs)
M⟦ tapp {T = T} M U ⟧² ℜs asℜbs =
  struct-cast (T⟦ substn T U ⟧² ℜs) (substn⟦ T ⟧⟦ U ⟧ _) (substn⟦ T ⟧⟦ U ⟧ _)
    (cast² (substn⟦ T ⟧⟦ U ⟧² ℜs) (M⟦ M ⟧² ℜs asℜbs (T⟦ U ⟧² ℜs)))
M⟦ eq {α} {T} {U} T≣U M ⟧² {As} {Bs} ℜs asℜbs =
  struct-cast (T⟦ U ⟧² ℜs) (≣⟦ T≣U ⟧ As) (≣⟦ T≣U ⟧ Bs) (cast² (≣⟦ T≣U ⟧² ℜs) (M⟦ M ⟧² ℜs asℜbs))

-- Types with a chosen free world variable

_∷ʳ_ : Kinds → Kind → Kinds
[]      ∷ʳ K = K ∷ []
(T ∷ Σ) ∷ʳ K = T ∷ (Σ ∷ʳ K)

TVar+ : Kind → Kinds → Set
TVar+ K Σ = TVar K (Σ ∷ʳ rset₀)

Typ+ : Kinds → Kind → Set
Typ+ Σ = Typ (Σ ∷ʳ rset₀)

wvar : ∀ Σ → TVar+ rset₀ Σ
wvar []      = zero
wvar (K ∷ Σ) = suc (wvar Σ)

world : ∀ {Σ} → Typ+ Σ rset₀
world {Σ} = var (wvar Σ)

World : Time → Set
World t = ⊤

taut : ∀ {Σ α} → Typ+ Σ (rset α ⇒ set α)
taut {Σ} {α} = abs (rset α) (Π time
  (app (world {time ∷ rset α ∷ Σ}) tvar₀ ⊸ app tvar₁ tvar₀))

-- Surface types

data STyp : Kind → Set where
  ⟨_⟩ : ∀ {α} → STyp (set α) → STyp (rset α)
  [_] : ∀ {α} → STyp (rset α) → STyp (set α)
  _⊠_ _↦_ : ∀ {α β} → STyp (set α) → STyp (set β) → STyp (set (α ⊔ β))
  _∧_ _⇒_ : ∀ {α β} → STyp (rset α) → STyp (rset β) → STyp (rset (α ⊔ β))
  □ : ∀ {α} → STyp (rset α) → STyp (rset α)

⟪_⟫ : ∀ {K} → STyp K → Typ+ [] K
⟪ ⟨ T ⟩ ⟫ = app always ⟪ T ⟫
⟪ [ T ] ⟫ = app (taut {[]}) ⟪ T ⟫
⟪ T ⊠ U ⟫ = ⟪ T ⟫ ⊗ ⟪ U ⟫
⟪ T ↦ U ⟫ = ⟪ T ⟫ ⊸ ⟪ U ⟫
⟪ T ∧ U ⟫ = ⟪ T ⟫ ⊗ʳ ⟪ U ⟫
⟪ T ⇒ U ⟫ = ⟪ T ⟫ ⊸ʳ ⟪ U ⟫
⟪ □ T ⟫   = tvar₀ ⊵ ⟪ T ⟫

T⟪_⟫ : ∀ {K} → STyp K → K⟦ K ⟧
T⟪ T ⟫ = T⟦ ⟪ T ⟫ ⟧ (World , tt)

-- Signals of T are iso to □ T

Signal : ∀ {α} → RSet α → RSet α
Signal A s = ∀ t → True (s ≤ t) → A t

sig : ∀ {α} (T : STyp (rset α)) s →
  T⟪ □ T ⟫ s → Signal T⟪ T ⟫ s
sig T s σ t s≤t = σ t s≤t _

sig⁻¹ : ∀ {α} (T : STyp (rset α)) s →
  Signal T⟪ T ⟫ s → T⟪ □ T ⟫ s
sig⁻¹ T s σ t s≤t _ = σ t s≤t

sig-iso : ∀ {α} (T : STyp (rset α)) s σ →
  (sig T s (sig⁻¹ T s σ) ≡ σ)
sig-iso T s σ = refl

sig-iso⁻¹ : ∀ {α} (T : STyp (rset α)) s σ →
  (sig⁻¹ T s (sig T s σ) ≡ σ)
sig-iso⁻¹ T s σ = refl

-- Signal functions from T to U are iso to □ T ⇒ □ U

SF : ∀ {α β} → RSet α → RSet β → RSet (α ⊔ β)
SF A B s = Signal A s → Signal B s

sf : ∀ {α β} (T : STyp (rset α)) (U : STyp (rset β)) s →
  T⟪ □ T ⇒ □ U ⟫ s → SF T⟪ T ⟫ T⟪ U ⟫ s
sf T U s f σ = sig U s (f (sig⁻¹ T s σ))

sf⁻¹ : ∀ {α β} (T : STyp (rset α)) (U : STyp (rset β)) s →
   SF T⟪ T ⟫ T⟪ U ⟫ s → T⟪ □ T ⇒ □ U ⟫ s
sf⁻¹ T U s f σ = sig⁻¹ U s (f (sig T s σ))

sf-iso : ∀ {α β} (T : STyp (rset α)) (U : STyp (rset β)) s f →
  (sf T U s (sf⁻¹ T U s f) ≡ f)
sf-iso T U s f = refl

sf-iso⁻¹ : ∀ {α β} (T : STyp (rset α)) (U : STyp (rset β)) s f →
  (sf⁻¹ T U s (sf T U s f) ≡ f)
sf-iso⁻¹ T U s f = refl

-- Causality

mutual

  _at_⊨_≈[_]_ : ∀ {α} (T : STyp (rset α)) s → T⟪ T ⟫ s → Time → T⟪ T ⟫ s → Set α
  ⟨ T ⟩   at s ⊨ a       ≈[ u ] b       = T ⊨ a ≈[ u ] b
  (T ∧ U) at s ⊨ (a , b) ≈[ u ] (c , d) = (T at s ⊨ a ≈[ u ] c) × (U at s ⊨ b ≈[ u ] d)
  (T ⇒ U) at s ⊨ f       ≈[ u ] g       = ∀ a b → (T at s ⊨ a ≈[ u ] b) → (U at s ⊨ f a ≈[ u ] g b)
  □ T     at s ⊨ σ       ≈[ u ] τ       = (∀ t s≤t → True (t ≤ u) → (T at t ⊨ σ t s≤t _ ≈[ u ] τ t s≤t _))

  _⊨_≈[_]_ : ∀ {α} → (T : STyp (set α)) → T⟪ T ⟫ → Time → T⟪ T ⟫ → Set α
  [ T ]   ⊨ σ       ≈[ u ] τ       = ∀ s → True (s ≤ u) → (T at s ⊨ σ s _ ≈[ u ] τ s _)
  (T ⊠ U) ⊨ (a , b) ≈[ u ] (c , d) = (T ⊨ a ≈[ u ] c) × (U ⊨ b ≈[ u ] d)
  (T ↦ U) ⊨ f       ≈[ u ] g       = ∀ a b → (T ⊨ a ≈[ u ] b) → (U ⊨ f a ≈[ u ] g b)

Causal : ∀ {α β} (T : STyp (set α)) (U : STyp (set β)) → T⟪ T ↦ U ⟫ → Set (α ⊔ β)
Causal T U f = ∀ u σ τ →
  (T ⊨ σ ≈[ u ] τ) → (U ⊨ f σ ≈[ u ] f τ)

-- Parametricity implies causality

ℜ[_] : Time → (rset o ∋ World ↔ World)
ℜ[ u ] {t} s≡t tt tt = True (t ≤ u)

mutual

  ℜ-impl-≈_at : ∀ {α} (T : STyp (rset α)) s u → True (s ≤ u) → ∀ a b →
    (T⟦ ⟪ T ⟫ ⟧² (ℜ[ u ] , tt) refl a b) → (T at s ⊨ a ≈[ u ] b)
  ℜ-impl-≈ ⟨ T ⟩   at s u s≤u a b aℜb
    = ℜ-impl-≈ T u a b aℜb
  ℜ-impl-≈ (T ∧ U) at s u s≤u (a , b) (c , d) (aℜc , bℜd)
    = (ℜ-impl-≈ T at s u s≤u a c aℜc , ℜ-impl-≈ U at s u s≤u b d bℜd)
  ℜ-impl-≈ (T ⇒ U) at s u s≤u f g fℜg
    = λ a b a≈b → ℜ-impl-≈ U at s u s≤u (f a) (g b) (fℜg (≈-impl-ℜ T at s u s≤u a b a≈b))
  ℜ-impl-≈_at (□ T) s u s≤u σ τ σℜτ = λ t s≤t t≤u →
    ℜ-impl-≈ T at t u t≤u (σ t s≤t _) (τ t s≤t _)
      (σℜτ refl tt (λ {r} _ _ {r≤t} _ → ≤-trans r t u r≤t t≤u))

  ≈-impl-ℜ_at : ∀ {α} (T : STyp (rset α)) s u → True (s ≤ u) → ∀ a b →
     (T at s ⊨ a ≈[ u ] b) → (T⟦ ⟪ T ⟫ ⟧² (ℜ[ u ] , tt) refl a b)
  ≈-impl-ℜ ⟨ T ⟩   at s u s≤u a b a≈b
    = ≈-impl-ℜ T u a b a≈b
  ≈-impl-ℜ (T ∧ U) at s u s≤u (a , b) (c , d) (a≈c , b≈d)
    = (≈-impl-ℜ T at s u s≤u a c a≈c , ≈-impl-ℜ U at s u s≤u b d b≈d)
  ≈-impl-ℜ (T ⇒ U) at s u s≤u f g f≈g
    = λ {a} {b} aℜb → ≈-impl-ℜ U at s u s≤u (f a) (g b) (f≈g a b (ℜ-impl-≈ T at s u s≤u a b aℜb))
  ≈-impl-ℜ (□ T)   at s u s≤u σ τ σ≈τ = lemma where
    lemma : T⟦ ⟪ □ T ⟫ ⟧² (ℜ[ u ] , tt) {s} refl σ τ
    lemma {t} refl {s≤t} {s≤t′} tt kℜk′ with irrel (s ≤ t) s≤t s≤t′
    lemma {t} refl {s≤t}        tt kℜk′ | refl
      = ≈-impl-ℜ T at t u t≤u (σ t s≤t _) (τ t s≤t _) (σ≈τ t s≤t t≤u) where
        t≤u = kℜk′ {t} refl {s≤t} {s≤t} tt {≤-refl t} {≤-refl t} tt

  ℜ-impl-≈ : ∀ {α} (T : STyp (set α)) (u : Time) (a b : T⟪ T ⟫) →
    (T⟦ ⟪ T ⟫ ⟧² (ℜ[ u ] , tt) a b) → (T ⊨ a ≈[ u ] b)
  ℜ-impl-≈ (T ⊠ U) u (a , b) (c , d) (aℜc , bℜd)
    = (ℜ-impl-≈ T u a c aℜc , ℜ-impl-≈ U u b d bℜd)
  ℜ-impl-≈ (T ↦ U) u f g fℜg
    = λ a b a≈b → ℜ-impl-≈ U u (f a) (g b) (fℜg (≈-impl-ℜ T u a b a≈b))
  ℜ-impl-≈ [ T ] u σ τ σℜτ
    = λ s s≤u → ℜ-impl-≈ T at s u s≤u (σ s _) (τ s _) (σℜτ refl s≤u)

  ≈-impl-ℜ : ∀ {α} (T : STyp (set α)) (u : Time) (a b : T⟪ T ⟫) →
    (T ⊨ a ≈[ u ] b) → (T⟦ ⟪ T ⟫ ⟧² (ℜ[ u ] , tt) a b)
  ≈-impl-ℜ (T ⊠ U) u (a , b) (c , d) (a≈c , b≈d)
    = (≈-impl-ℜ T u a c a≈c , ≈-impl-ℜ U u b d b≈d)
  ≈-impl-ℜ (T ↦ U) u f g f≈g
    = λ {a} {b} aℜb → ≈-impl-ℜ U u (f a) (g b) (f≈g a b (ℜ-impl-≈ T u a b aℜb))
  ≈-impl-ℜ [ T ] u σ τ σ≈τ = lemma where
    lemma : T⟦ ⟪ [ T ] ⟫ ⟧² (ℜ[ u ] , tt) σ τ
    lemma {s} refl s≤u = ≈-impl-ℜ T at s u s≤u (σ s _) (τ s _) (σ≈τ s s≤u)

-- Every F-omega function is causal

causality : ∀ {α β} (T : STyp (set α)) (U : STyp (set β)) (M : Exp [] ⟪ T ↦ U ⟫) →
  Causal T U (M⟦ M ⟧ (World , tt) tt)
causality T U M u
  = ℜ-impl-≈ (T ↦ U) u
      (M⟦ M ⟧ (World , tt) tt)
      (M⟦ M ⟧ (World , tt) tt)
      (M⟦ M ⟧² (ℜ[ u ] , _) tt)

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module x00-playpen where

-- prove properties of inductive naturals and operations on them via induction

import      Relation.Binary.PropositionalEquality as Eq
open        Eq             using (_≡_; refl; cong; sym)
open        Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat       using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

*-assoc : ∀ (m n p : ℕ)
        → (m *  n) * p
        ≡  m * (n  * p)
*-assoc m n p = {!!}

+-xx : ∀ (n  : ℕ)
       → (n ^ 3) ∸ ((n * n) * n)
       ≡ zero
+-xx zero = refl
+-xx (suc n) = {!!}
{-
  begin
              (n * (n ^ 2))   ∸ ((n * n) * n)
  ≡⟨⟩
         (n * (n * (n ^ 1)))  ∸ ((n * n) * n)
  ≡⟨⟩
    (n * (n * (n * (n ^ 0)))) ∸ ((n * n) * n)
  ≡⟨⟩
    (n * (n * (n *  1     ))) ∸ ((n * n) * n)
  ≡⟨⟩
    (n * (n *  n          ))  ∸ ((n * n) * n)
  ≡⟨ cong ( ((n * (n *  n))) ∸_) (*-assoc n n n) ⟩
    (n * (n *  n          ))  ∸ ( n * (n * n))
  ∎
-}

ext: agda

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


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

module Cubical.Data.Queue where

open import Cubical.Data.Queue.Base public
open import Cubical.Data.Queue.Finite 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 Numeral.CoordinateVector where

import      Lvl
open import Data.Boolean
open import Functional
open import Lang.Instance
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Finite.Oper
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Natural
import      Numeral.Natural.Oper as ℕ
open import Numeral.Natural.Function
open import Numeral.Natural.Function.Proofs
open import Type

private variable ℓ : Lvl.Level
private variable T A B C : Type{ℓ}
private variable d d₁ d₂ : ℕ

-- Accessor of data in 1-dimensional finite space (Implies bounded).
-- Like a homogenous tuple or a fixed-size list.
-- The type is defined as the type of the vector projection function (A cell in the vector).
Vector : ℕ → Type{ℓ} → Type
Vector(d)(T) = 𝕟(d) → T

-- Type of elements in the vector
Element : Vector(d)(T) → Type
Element{T = T} = const T

-- The maximum number of dimensions of a space that the vector can describe points in
dim : Vector(d)(T) → ℕ
dim{d = d} = const d

-- The projection function (which also is the function itself).
proj : Vector(d)(T) → 𝕟(d) → T
proj = id

-- TODO: Move this to a separate "Relations" file
open import Logic
open import Relator.Equals.Proofs.Equivalence
open import Structure.Function.Domain
open import Structure.Setoid
private variable ℓₑ : Lvl.Level
-- The vector's elements are all distinct (the vector contains no duplicate elements).
Distinct : ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → Vector(d)(T) → Stmt
Distinct = Injective ⦃ [≡]-equiv ⦄

-- The first element of a non-empty vector
head : Vector(𝐒(d))(T) → T
head(v) = v(𝟎)

-- The list without the first element of a non-empty vector
tail : Vector(𝐒(d))(T) → Vector(d)(T)
(tail{𝐒(_)}(v)) (i) = v(𝐒(i))

-- The list without the first element if there were any
tail₀ : Vector(d)(T) → Vector(Numeral.Natural.𝐏(d))(T)
tail₀{𝟎}    = id
tail₀{𝐒(_)} = tail

-- The last element of a non-empty vector
last : Vector(𝐒(d))(T) → T
last(v) = v(maximum)

-- The list without the last element if there were any
withoutLast : Vector(𝐒(d))(T) → Vector(d)(T)
(withoutLast v)(i) = v(bound-𝐒(i))

-- Applies a function on every value of the vector
map : (A → B) → Vector(d)(A) → Vector(d)(B)
(map f(v))(i) = f(v(i))

-- Applies a binary operation on every pair of values, each from 2 vectors elementwise
-- Example:
--   map₂(_+_) [1,2,3] [10,20,30] = [1+10 , 2+20 , 3+30] = [11,22,33]
map₂ : (A → B → C) → Vector(d)(A) → Vector(d)(B) → Vector(d)(C)
(map₂(_▫_) (v₁)(v₂))(i) = v₁(i) ▫ v₂(i)

map₂-min : (A → B → C) → ∀{d₁ d₂} → Vector(d₁)(A) → Vector(d₂)(B) → Vector(min d₁ d₂)(C)
(map₂-min(_▫_) (v₁)(v₂))(i) = v₁(bound-[≤] infer i) ▫ v₂(bound-[≤] infer i)

-- Example:
--   foldₗ (_▫_) (0) [1,2,3,4]
--   = (((0 ▫ 1) ▫ 2) ▫ 3) ▫ 4
foldₗ : (B → A → B) → B → Vector(d)(A) → B
foldₗ {d = 𝟎}    (_▫_) (init) (v) = init
foldₗ {d = 𝐒(d)} (_▫_) (init) (v) = foldₗ {d = d} (_▫_) (init ▫ (head v)) (tail v)

-- Example:
--   reduceₗ (_▫_) [1,2,3,4]
--   = ((1 ▫ 2) ▫ 3) ▫ 4
reduceₗ : (A → A → A) → Vector(𝐒(d))(A) → A
reduceₗ(_▫_) v = foldₗ(_▫_) (head v) (tail v)

-- Example:
--   reduceOrₗ (_▫_) 0 [1,2,3,4]
--   = ((1 ▫ 2) ▫ 3) ▫ 4
reduceOrₗ : (A → A → A) → A → Vector(d)(A) → A
reduceOrₗ {d = 𝟎}    _     empty _ = empty
reduceOrₗ {d = 𝐒(d)} (_▫_) empty v = foldₗ(_▫_) (head v) (tail v)

-- Example:
--   foldᵣ (_▫_) (0) [1,2,3,4]
--   = 1 ▫ (2 ▫ (3 ▫ (4 ▫ 0)))
foldᵣ : (A → B → B) → B → Vector(d)(A) → B
foldᵣ {d = 𝟎}    (_▫_) (init) (v) = init
foldᵣ {d = 𝐒(d)} (_▫_) (init) (v) = (head v) ▫ (foldᵣ {d = d} (_▫_) (init) (tail v))

-- Example:
--   foldᵣ-init (_▫_) (0) [1,2,3,4]
--   = 0 ▫ (1 ▫ (2 ▫ (3 ▫ 4)))
foldᵣ-init : (A → A → A) → A → Vector(d)(A) → A
foldᵣ-init {d = 𝟎}    (_▫_) (init) (v) = init
foldᵣ-init {d = 𝐒(d)} (_▫_) (init) (v) = init ▫ (foldᵣ-init {d = d} (_▫_) (head v) (tail v))

-- Example:
--   reduceᵣ (_▫_) [1,2,3,4]
--   = 1 ▫ (2 ▫ (3 ▫ 4))
reduceᵣ : (T → T → T) → Vector(𝐒(d))(T) → T
reduceᵣ {d = 𝟎}    (_▫_) (v) = head v
reduceᵣ {d = 𝐒(d)} (_▫_) (v) = (head v) ▫ (reduceᵣ (_▫_) (tail v))

-- Example:
--   reduceOrᵣ (_▫_) (0) [1,2,3,4]
--   = 1 ▫ (2 ▫ (3 ▫ 4))
reduceOrᵣ : (T → T → T) → T → Vector(d)(T) → T
reduceOrᵣ {d = 𝟎}    _     empty v = empty
reduceOrᵣ {d = 𝐒(d)} (_▫_) empty v = reduceᵣ(_▫_) v

-- A vector filled with multiple copies of a single element.
fill : T → Vector(d)(T)
fill(elem) = const(elem)

-- An empty vector.
empty : Vector(0)(T)
empty()

-- A vector with a single element.
singleton : T → Vector(1)(T)
singleton x 𝟎 = x

-- A vector with two elements.
pair : T → T → Vector(2)(T)
pair x _ (𝟎)   = x
pair _ y (𝐒 𝟎) = y

-- A vector with an additional element at the start.
prepend : T → Vector(d)(T) → Vector(𝐒(d))(T)
(prepend(x)(_)) (𝟎)    = x
(prepend(_)(v)) (𝐒(n)) = v(n)

-- A vector with an additional element inserted at an already existing position.
-- Examples:
--   insert 0 x [a,b,c] = [x,a,b,c]
--   insert 1 x [a,b,c] = [a,x,b,c]
--   insert 2 x [a,b,c] = [a,b,x,c]
--   insert 3 x [a,b,c] is a type error because 3 is not an existing position.
insert : 𝕟(d) → T → Vector(d)(T) → Vector(𝐒(d))(T)
insert 𝟎               = prepend
insert (𝐒 _) _ v 𝟎     = v(𝟎)
insert (𝐒 i) x v (𝐒 n) = insert i x (tail v) n

-- A vector with an additional element inserted at a position.
-- Note: The difference compared to insert is that this includes the postpending operation.
-- Examples:
--   insert₊ 0 x [a,b] = [x,a,b]
--     insert₊ 0 x [a,b] 0 ≟ [x,a,b] 0 = x
--     insert₊ 0 x [a,b] 1 ≟ [x,a,b] 1 = a
--     insert₊ 0 x [a,b] 2 ≟ [x,a,b] 2 = b
--   insert₊ 1 x [a,b] = [a,x,b]
--     insert₊ 1 x [a,b] 0 = a
--     insert₊ 1 x [a,b] 1 = insert₊ 0 x [b] 0 = x
--     insert₊ 1 x [a,b] 2 = insert₊ 0 x [b] 1 = [x,b] 1 = b
--   insertv 2 x [a,b] = [a,b,x]
--     insert₊ 2 x [a,b] 0 = a
--     insert₊ 2 x [a,b] 1 = insert₊ 1 x [b] 0 = b
--     insert₊ 2 x [a,b] 2 = insert₊ 1 x [b] 1 = insert₊ 0 x [] 0 = [x] 0 = x
insert₊ : 𝕟₌(d) → T → Vector(d)(T) → Vector(𝐒(d))(T)
insert₊{_}   𝟎               = prepend
insert₊{𝐒 _} (𝐒 _) _ v 𝟎     = v(𝟎)
insert₊{𝐒 _} (𝐒 i) x v (𝐒 n) = insert₊ i x (tail v) n

-- A vector concatenated with another vector
_++_ : Vector(d₁)(T) → Vector(d₂)(T) → Vector(d₁ ℕ.+ d₂)(T)
_++_ {d₁ = 𝟎}     {d₂ = d₂} v₁ v₂        = v₂
_++_ {d₁ = 𝐒(d₁)} {d₂ = d₂} v₁ v₂ (𝟎)    = v₁(𝟎)
_++_ {d₁ = 𝐒(d₁)} {d₂ = d₂} v₁ v₂ (𝐒(i)) = _++_ {d₁ = d₁} {d₂ = d₂} (v₁ ∘ 𝐒) v₂ i

count : (T → Bool) → Vector(d)(T) → ℕ
count {d = 𝟎}    (f)(v) = 𝟎
count {d = 𝐒(n)} (f)(v) = (if f(head v) then 𝐒 else id) (count{d = n} (f)(tail v))

reverse : Vector(d)(T) → Vector(d)(T)
(reverse(v)) (n) = v(Wrapping.[−] n)

indexProject : 𝕟(d) → T → T → Vector(d)(T)
indexProject n true false i = if(n ≡? i) then true else false

-- A vector without the element at the specified index
-- TODO: Implement Numeral.Finite.Bound.bound-𝐏
-- without : ∀{T}{d} → 𝕟(𝐒(d)) → Vector(𝐒(d))(T) → Vector(d)(T)
-- Vector.proj (without {_}{𝐒(_)} (𝟎)   (v)) (i) = Vector.proj(v)(𝐒(i))
-- Vector.proj (without {_}{𝐒(_)} (𝐒(n))(v)) (i) = if(i ≤? n) then Vector.proj(v)(𝐒(i)) else Vector.proj(v)(bound-𝐏(i))

-- postpend : ∀{T}{d} → T → Vector(d)(T) → Vector(𝐒(d))(T)
-- Vector.proj(postpend{_}{d} (x)(_)) (n) = if (n ≡? d) then x else Vector.proj(v)(n)

-- concat : ∀{T}{d₁ d₂} → Vector(d₁)(T) → Vector(d₂)(T) → Vector(d₁ + d₂)(T)
-- Vector.proj(concat(v₁)(v₂)) (n) with (n < d₁ ≡ 𝑇)
-- ... () = Vector.proj(v₁) (n)
-- ... () = Vector.proj(v₂) (n)

-- TODO: take / truncate
-- TODO: Equality by function equality

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 #-}
module Issue4365 where

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

postulate
  A : Set
  a : A

_ : primTransp (\ i → A) i0 a ≡ a
_ = \ _ → a

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Cats where

-- The (large) category of (small) categories.
-- Even though Agda can figure out the levels, it is worth making them explicit,
-- to see the large level jumps involved.

open import Level
open import Categories.Category using (Category)
open import Categories.Functor using (Functor; id; _∘F_)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e
    F G H I : Functor C D

Cats : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔  e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Cats o ℓ e = record
  { Obj       = Category o ℓ e
  ; _⇒_       = Functor
  ; _≈_       = NaturalIsomorphism
  ; id        = id
  ; _∘_       = _∘F_
  ; assoc     = λ {_ _ _ _ F G H} → associator F G H
  ; sym-assoc = λ {_ _ _ _ F G H} → sym (associator F G H)
  ; identityˡ = unitorˡ
  ; identityʳ = unitorʳ
  ; identity² = unitor²
  ; equiv     = isEquivalence
  ; ∘-resp-≈  = _ⓘₕ_
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Cubical.HITs.InfNat where

open import Cubical.HITs.InfNat.Base public
open import Cubical.HITs.InfNat.Properties public


text:
module LFRef.Readme where

open import LFRef.Syntax
open import LFRef.Welltyped
open import LFRef.Eval
open import LFRef.Properties.Soundness
open import LFRef.Properties.Confluence


text:
open import Prelude
open import dynamics-core

module lemmas-consistency where
  -- type consistency is symmetric
  ~sym : {t1 t2 : htyp} → t1 ~ t2 → t2 ~ t1
  ~sym TCRefl = TCRefl
  ~sym TCHole1 = TCHole2
  ~sym TCHole2 = TCHole1
  ~sym (TCArr p1 p2) = TCArr (~sym p1) (~sym p2)
  ~sym (TCSum p1 p2) = TCSum (~sym p1) (~sym p2)
  ~sym (TCProd p1 p2) = TCProd (~sym p1) (~sym p2)

  -- type consistency isn't transitive
  not-trans : ((t1 t2 t3 : htyp) → t1 ~ t2 → t2 ~ t3 → t1 ~ t3) → ⊥
  not-trans t with t (num ==> num) ⦇-⦈ num TCHole1 TCHole2
  ... | ()

  --  every pair of types is either consistent or not consistent
  ~dec : (t1 t2 : htyp) → ((t1 ~ t2) + (t1 ~̸ t2))
    -- this takes care of all hole cases, so we don't consider them below
  ~dec _ ⦇-⦈ = Inl TCHole1
  ~dec ⦇-⦈ _ = Inl TCHole2
  ~dec num num = Inl TCRefl
  ~dec num (t2 ==> t3) = Inr (λ ())
  ~dec num (t2 ⊕ t3) = Inr (λ ())
  ~dec (t1 ==> t3) num = Inr (λ ())
  ~dec (t1 ==> t3) (t2 ==> t4)
    with ~dec t1 t2 | ~dec t3 t4
  ... | Inl x | Inl x₁ = Inl (TCArr x x₁)
  ... | Inl x | Inr x₁ = Inr λ{ TCRefl → x₁ TCRefl ; (TCArr x₂ x₃) → x₁ x₃}
  ... | Inr x | w = Inr λ{ TCRefl → x TCRefl ; (TCArr x₁ x₂) → x x₁}
  ~dec (t1 ==> t3) (t2 ⊕ t4) = Inr (λ ())
  ~dec (t1 ⊕ t3) num = Inr (λ ())
  ~dec (t1 ⊕ t3) (t2 ==> t4) = Inr (λ ())
  ~dec (t1 ⊕ t3) (t2 ⊕ t4)
    with ~dec t1 t2 | ~dec t3 t4
  ... | Inl x | Inl x₁ = Inl (TCSum x x₁)
  ... | Inl x | Inr x₁ = Inr λ{ TCRefl → x₁ TCRefl ; (TCSum x₂ x₃) → x₁ x₃}
  ... | Inr x | w = Inr λ{ TCRefl → x TCRefl ; (TCSum x₁ x₂) → x x₁}
  ~dec num (t2 ⊠ t4) = Inr (λ ())
  ~dec (t1 ==> t3) (t2 ⊠ t4) = Inr (λ ())
  ~dec (t1 ⊕ t3) (t2 ⊠ t4) = Inr (λ ())
  ~dec (t1 ⊠ t3) num = Inr (λ ())
  ~dec (t1 ⊠ t3) (t2 ==> t4) = Inr (λ ())
  ~dec (t1 ⊠ t3) (t2 ⊕ t4) = Inr (λ ())
  ~dec (t1 ⊠ t3) (t2 ⊠ t4)
    with ~dec t1 t2 | ~dec t3 t4
  ... | Inl x | Inl x₁ = Inl (TCProd x x₁)
  ... | Inl x | Inr x₁ = Inr λ{ TCRefl → x₁ TCRefl ; (TCProd x₂ x₃) → x₁ x₃}
  ... | Inr x | w = Inr λ{ TCRefl → x TCRefl ; (TCProd x₁ x₂) → x x₁}

  -- if arrows are consistent, their components are consistent
  ~arr : ∀{τ1 τ2 τ3 τ4} →
         (τ1 ==> τ2) ~ (τ3 ==> τ4) →
         (τ1 ~ τ3) × (τ2 ~ τ4)
  ~arr TCRefl = TCRefl , TCRefl
  ~arr (TCArr con con₁) = con , con₁

  -- if sums are consistent, their components are consistent
  ~sum : ∀{τ1 τ2 τ3 τ4} →
         (τ1 ⊕ τ2) ~ (τ3 ⊕ τ4) →
         (τ1 ~ τ3) × (τ2 ~ τ4)
  ~sum TCRefl = TCRefl , TCRefl
  ~sum (TCSum con con₁) = con , con₁

   -- if products are consistent, their components are consistent
  ~prod : ∀{τ1 τ2 τ3 τ4} →
          (τ1 ⊠ τ2) ~ (τ3 ⊠ τ4) →
          (τ1 ~ τ3) × (τ2 ~ τ4)
  ~prod TCRefl = TCRefl , TCRefl
  ~prod (TCProd con con₁) = con , con₁

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Operator.Equals {ℓ ℓₑ} where

open import Data.Boolean
open import Logic
open import Structure.Setoid
open import Type.Properties.Decidable
open import Type

DecidableEquiv : (T : Type{ℓ}) ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → Stmt
DecidableEquiv(T) = Decidable(2)(_≡_)

_==_ : ∀{T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ _ : DecidableEquiv(T) ⦄ → (T → T → Bool)
_==_ = decide(2)(_≡_)


text:
module Issue175 where

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

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

postulate
  Char   : Set
  String : Set

{-# BUILTIN CHAR   Char   #-}
{-# BUILTIN STRING String #-}

primitive primStringToList : String → List Char

lemma : primStringToList "0" ≡ ('0' ∷ [])
lemma = refl

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text: import Issue2447.Operator-error

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --rewriting --prop --confluence-check #-}

open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Data.Vec.Base
open import Data.Bool
open import Data.Sum

-- sigma type in Prop used to handle telescopes.

record Tel {a b} (A : Prop a) (B : A → Prop b) : Prop (a ⊔ b) where
  constructor _,_
  field
    fstC : A
    sndC : B fstC

open Tel public

infixr 4 _,_

record ΣCov {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fstCov : A
    sndCov : B fstCov

open ΣCov public

record prod {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fstprod : A
    sndprod : B

open prod public

variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

-- a bit of boilerplate to deal with Prop

data ⊥ : Prop where

record ⊤P : Prop ℓ where
  constructor ttP

record Box (A : Prop ℓ) : Set ℓ where
  constructor box
  field
    unbox : A

open Box public

_×_ : ∀ (A : Prop ℓ) (B : Prop ℓ₁) → Prop (ℓ ⊔ ℓ₁)
A × B = Tel A (λ _ → B)

-- we need this for cumulativity

record i (A : Prop ℓ) : Prop (ℓ ⊔ ℓ₁) where
  constructor inj
  field
    uninj : A

open i public

record iS (A : Set ℓ) : Set (ℓ ⊔ ℓ₁) where
  constructor inj
  field
    uninj : A

open iS public

{-
 Axiomatisation of Id, Id-refl, transport (for proposition), cast

 Note that Id-refl, transport are axioms in Prop,
 so we don't need to give them a computation content.

 Also transport-refl is useless for transport on Prop
-}

postulate Id : (A : Set ℓ) → A → A → Prop ℓ

postulate cast : (A B : Set ℓ) (e : Id (Set ℓ) A B) → A → B

postulate Id-refl : {A : Set ℓ} (x : A) → Id A x x

postulate cast-refl : {A : Set ℓ} (e : Id _ A A) (a : A) → Id A (cast A A e a) a

postulate transport : {A : Set ℓ} (P : A → Prop ℓ₁) (x : A) (t : P x) (y : A) (e : Id A x y) → P y

-- cast-refl' : {A : Set ℓ} (e : Id (Set ℓ) A A) (a : A) → Id A (cast A A e a) a
-- cast-refl' {A = A} e a = transport (λ z → Id A z a) {!!} (Id-refl a) {!!} {!!}

-- direct derived functions

ap : {A : Set ℓ} {B : Set ℓ₁} {x y : A} (f : A → B) (e : Id A x y) →
     Id B (f x) (f y)
ap {ℓ} {ℓ₁} {A} {B} {x} {y} f e = transport (λ z → Id B (f x) (f z)) x (Id-refl _) y e

transport-Id : {A : Set ℓ} (P : A → Set ℓ₁) (x : A) (t : P x) (y : A) (e : Id A x y) → P y
transport-Id P x t y e = cast (P x) (P y) (ap P e) t

transport-refl : {A : Set ℓ} (P : A → Set ℓ₁) (x : A) (t : P x) (e : Id A x x) → Id _ (transport-Id P x t x e) t
transport-refl P x t e = cast-refl (ap P e) t

inverse  : (A : Set ℓ) {x y : A} (p : Id {ℓ} A x y) → Id A y x
inverse A {x} {y} p = transport (λ z → Id A z x) x (Id-refl x) y p

concatId : (A : Set ℓ) {x y z : A} (p : Id {ℓ} A x y)
           (q : Id {ℓ} A y z) → Id A x z
concatId A {x} {y} {z} p q = transport (λ t → Id A x t) y p z q

-- we now state rewrite rules for the identity type

postulate Id-Pi : (A : Set ℓ) (B : A → Set ℓ₁) (f g : (a : A) → B a) →
                  Id ((a : A) → B a) f g ≡ ((a : A) → Id (B a) (f a) (g a))

{-# REWRITE Id-Pi #-}

-- rewrite rules on Id-refl are not needed because it is in Prop

refl-Pi : (A : Set ℓ) (B : A → Set ℓ₁) (f : (a : A) → B a) →
          box (Id-refl f) ≡ box (λ a → Id-refl (f a))
refl-Pi A B f = refl

-- sanity check for funext

funext : (A : Set ℓ) (B : A → Set ℓ₁) (f g : (a : A) → B a) →
         ((a : A) → Id (B a) (f a) (g a)) → Id ((a : A) → B a) f g
funext A B f g e = e

postulate Id-Sigma : (A : Set ℓ) (B : A → Set ℓ₁) (a a' : A)
                     (b : B a) (b' : B a') →
                     Id (Σ A B) (a , b) (a' , b') ≡
                     Tel (Id A a a')
                         (λ e → Id (B a') (transport-Id B a b a' e) b')

{-# REWRITE Id-Sigma #-}

postulate Id-SigmaCov : (A : Set ℓ) (B : A → Set ℓ₁) (a a' : A)
                     (b : B a) (b' : B a') →
                     Id (ΣCov A B) (a , b) (a' , b') ≡
                     Tel (Id A a a')
                         (λ e → Id (B a) b (transport-Id B a' b' a (inverse A e)))

{-# REWRITE Id-SigmaCov #-}

postulate Id-prod : (A : Set ℓ) (B : Set ℓ₁) (a a' : A)
                     (b b' : B) →
                     Id (prod A B) (a , b) (a' , b') ≡
                     (Id A a a') × (Id B b b')

{-# REWRITE Id-prod #-}

postulate Id-Box : (A : Prop ℓ) (p q : A) → Id (Box A) (box p) (box q) ≡ ⊤P

{-# REWRITE Id-Box #-}

postulate Id-Unit : (p q : ⊤) → Id ⊤ p q ≡ ⊤P

{-# REWRITE Id-Unit #-}

postulate Id-list-nil-nil : (A : Set ℓ) →
                            Id (List A) [] [] ≡ ⊤P

-- postulate Id-list-nil-cons : (A : Set ℓ) (a' : A) (l' : List A) →
--                              Id (List A) [] (a' ∷ l') ≡ i ⊥

-- postulate Id-list-cons-nil : (A : Set ℓ) (a : A) (l : List A) →
--                              Id (List A) (a ∷ l) [] ≡ i ⊥

postulate Id-list-cons-cons : (A : Set ℓ) (a a' : A) (l l' : List A) →
                             Id (List A) (a ∷ l) (a' ∷ l') ≡
                             Id A a a' × Id (List A) l l'

{-# REWRITE Id-list-nil-nil #-}
{-# REWRITE Id-list-cons-cons #-}

postulate Id-nat-zero-zero : Id Nat 0 0 ≡ ⊤P

-- postulate Id-nat-zero-suc : (n : Nat) →
--                             Id Nat 0 (suc n) ≡ i ⊥

-- postulate Id-nat-suc-zero : (n : Nat) →
--                             Id Nat (suc n) zero ≡ i ⊥

postulate Id-nat-suc-suc : (n n' : Nat) →
                           Id Nat (suc n) (suc n') ≡
                           Id Nat n n'

{-# REWRITE Id-nat-zero-zero #-}
{-# REWRITE Id-nat-suc-suc #-}

postulate Id-bool-true-true : Id Bool true true ≡ ⊤P
postulate Id-bool-false-false : Id Bool false false ≡ ⊤P

{-# REWRITE Id-bool-true-true #-}
{-# REWRITE Id-bool-false-false #-}

postulate Id-sum-inj₁-inj₁ : (A : Set ℓ) (B : Set ℓ₁) (a a' : A) →
                           Id (A ⊎ B) (inj₁ a) (inj₁ a') ≡
                           i {ℓ = ℓ} {ℓ₁ = ℓ₁} (Id A a a')

postulate Id-sum-inj₂-inj₂ : (A : Set ℓ) (B : Set ℓ₁) (b b' : B) →
                           Id (A ⊎ B) (inj₂ b) (inj₂ b') ≡
                           i {ℓ = ℓ₁} {ℓ₁ = ℓ} (Id B b b')

{-# REWRITE Id-sum-inj₁-inj₁ #-}
{-# REWRITE Id-sum-inj₂-inj₂ #-}

-- rewrite rules for the identity type on the universe

telescope-Sigma : Set (lsuc (ℓ ⊔ ℓ₁))
telescope-Sigma {ℓ} {ℓ₁} = ΣCov (Set ℓ) (λ A → A → Set ℓ₁)

postulate Id-Type-Sigma : (A A' : Set ℓ) (B : A → Set ℓ₁) (B' : A' → Set ℓ₁) →
                          Id (Set (ℓ ⊔ ℓ₁)) (Σ A B) (Σ A' B') ≡
                          Id telescope-Sigma (A , B) (A' , B')

{-# REWRITE Id-Type-Sigma #-}

telescope-Forall : Set (lsuc (ℓ ⊔ ℓ₁))
telescope-Forall {ℓ} {ℓ₁} = Σ (Set ℓ) (λ A → A → Set ℓ₁)

postulate Id-Type-Pi : (A A' : Set ℓ) (B : A → Set ℓ₁) (B' : A' → Set ℓ₁) →
                       Id (Set (ℓ ⊔ ℓ₁)) ((a : A) → B a) ((a' : A') → B' a') ≡
                       Id telescope-Forall (A , B) (A' , B')

{-# REWRITE Id-Type-Pi #-}

telescope-Sum : Set (lsuc (ℓ ⊔ ℓ₁))
telescope-Sum {ℓ} {ℓ₁} = Σ (Set ℓ) (λ _ → Set ℓ₁)

postulate Id-Type-Sum : (A A' : Set ℓ) (B B' : Set ℓ₁)  →
                          Id (Set (ℓ ⊔ ℓ₁)) (A ⊎ B) (A' ⊎ B') ≡
                          Id telescope-Sum (A , B) (A' , B')

{-# REWRITE Id-Type-Sum #-}

postulate Id-Type-prod : (A A' : Set ℓ) (B B' : Set ℓ₁)  →
                          Id (Set (ℓ ⊔ ℓ₁)) (prod A B) (prod A' B') ≡
                          Id telescope-Sum (A , B) (A' , B')

{-# REWRITE Id-Type-prod #-}

telescope-List : Set (lsuc ℓ)
telescope-List {ℓ} = Set ℓ

postulate Id-Type-List : (A A' : Set ℓ) →
                       Id (Set ℓ) (List A) (List A') ≡
                       Id telescope-List A A'

{-# REWRITE Id-Type-List #-}

postulate Id-Type-Unit : Id Set ⊤ ⊤ ≡ ⊤P

{-# REWRITE Id-Type-Unit #-}

postulate Id-Type-Nat : Id Set Nat Nat ≡ Id Set ⊤ ⊤

{-# REWRITE Id-Type-Nat #-}

postulate Id-Type-Bool : Id Set Bool Bool ≡ Id Set ⊤ ⊤

{-# REWRITE Id-Type-Bool #-}

telescope-Box : Set (lsuc ℓ)
telescope-Box {ℓ} = Prop ℓ

postulate Id-Type-Box : (P P' : Prop ℓ) → Id (Set ℓ) (Box P) (Box P') ≡ Id telescope-Box P P'

{-# REWRITE Id-Type-Box #-}

-- rewrite rules for the identity type on Prop : Prop ext modulo cumul

postulate Id-prop : (P Q : Prop ℓ) → Id (Prop ℓ) P Q ≡ i (P → Q) × (Q → P)

{-# REWRITE Id-prop #-}

postulate Id-set : Id (Set (lsuc ℓ₁)) (Set ℓ₁) (Set ℓ₁) ≡ ⊤P

{-# REWRITE Id-set #-}

-- non-diagonal cases

{- There are n^2 cases, that's a pain, this is not exhaustive for the moment -}

postulate Id-set-nat : Id _ (Set ℓ) (iS Nat) ≡ i ⊥
postulate Id-nat-set : Id (Set (lsuc ℓ)) (iS Nat) (Set ℓ) ≡ i ⊥
postulate Id-set-bool : Id _ (Set ℓ) (iS Bool) ≡ i ⊥
postulate Id-bool-set : Id (Set (lsuc ℓ)) (iS Bool) (Set ℓ) ≡ i ⊥
postulate Id-bool-nat : Id _ Bool Nat ≡ i ⊥
postulate Id-nat-bool : Id _ Nat Bool ≡ i ⊥
postulate Id-set-pi : (A : Set ℓ₁) (B : A → Set ℓ₂) → Id (Set (lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂)) (iS {lsuc ℓ} {lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂} (Set ℓ))
                                                                                (iS {ℓ₁ ⊔ ℓ₂} {lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂} ((a : A) → B a)) ≡ i ⊥
postulate Id-pi-set : (A : Set ℓ₁) (B : A → Set ℓ₂) → Id (Set (lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂)) (iS {ℓ₁ ⊔ ℓ₂} {lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂} ((a : A) → B a))
                                                                                (iS {lsuc ℓ} {lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂} (Set ℓ)) ≡ i ⊥
postulate Id-set-sigma : (A : Set ℓ₁) (B : A → Set ℓ₂) → Id (Set (lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂)) (iS {lsuc ℓ} {lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂} (Set ℓ))
                                                                                (iS {ℓ₁ ⊔ ℓ₂} {lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂} (Σ A B)) ≡ i ⊥
postulate Id-sigma-set : (A : Set ℓ₁) (B : A → Set ℓ₂) → Id (Set (lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂)) (iS {ℓ₁ ⊔ ℓ₂} {lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂} (Σ A B))
                                                                                (iS {lsuc ℓ} {lsuc ℓ ⊔ ℓ₁ ⊔ ℓ₂} (Set ℓ)) ≡ i ⊥

{-# REWRITE Id-set-nat Id-nat-set Id-set-bool Id-bool-set Id-bool-nat Id-nat-bool Id-set-pi Id-pi-set Id-set-sigma Id-sigma-set #-}

--- Contractibility of singletons and J can be defined

contr-sing : (A : Set ℓ) {x y : A} (p : Id {ℓ} A x y) →
    Id (Σ A (λ y → Box (Id A x y))) (x , box (Id-refl x)) (y , box p)
contr-sing A {x} {y} p = p , ttP

J : (A : Set ℓ) (x : A) (P : (y : A) → Id A x y → Prop ℓ₁)
    (t : P x (Id-refl x)) (y : A) (e : Id A x y) → P y e
J A x P t y e = transport (λ z → P (fst z) (unbox (snd z))) (x , box (Id-refl x)) t (y , box e) (contr-sing A e)

-- tranporting back and forth is the identity

-- cast-inv : (A B : Set ℓ) (e : Id _ A B) (a : A) →
--                      Id A (cast B A (inverse (Set ℓ) {x = A} {y = B} e) (cast A B e a)) a
-- cast-inv {ℓ} A B e a = let e-refl = cast-refl (Id-refl A) a in
--                        let e-refl-cast = cast-refl (Id-refl A) (cast A A (Id-refl A) a) in
--                        J (Set ℓ) A (λ B e → Id A (cast B A (inverse (Set ℓ) {x = A} {y = B} e) (cast A B e a)) a)
--                          (concatId A e-refl-cast e-refl) B e

postulate cast-set : (A : Set ℓ) (e : _) → cast (Set ℓ) (Set ℓ) e A ≡ A

{-# REWRITE cast-set #-}

postulate cast-prop : (A : Prop ℓ) (e : _) → cast (Prop ℓ) (Prop ℓ) e A ≡ A

{-# REWRITE cast-prop #-}

postulate cast-type-family : (A A' : Set ℓ) (f : (a : A) → Set ℓ₁) (e : _) →
                    cast ((a : A) → Set ℓ₁) ((a' : A') → Set ℓ₁) e f ≡
                    λ (a' : A') → let a = cast A' A (inverse (Set ℓ) {x = A} {y = A'} (fstC e)) a' in f a

{-# REWRITE cast-type-family #-}

postulate cast-Pi : (A A' : Set ℓ) (B : A → Set ℓ₁) (B' : A' → Set ℓ₁) (f : (a : A) → B a) (e : Id _ ((a : A) → B a) ((a' : A') → B' a')) →
                    cast ((a : A) → B a) ((a' : A') → B' a') e f ≡
                    λ (a' : A') → let a = cast A' A (inverse (Set ℓ) {x = A} {y = A'} (fstC e)) a' in
                                  cast _ _ (sndC e a') (f a)

{-# REWRITE cast-Pi #-}

postulate cast-Sigma : (A A' : Set ℓ) (B : A → Set ℓ₁) (B' : A' → Set ℓ₁) (x : A) (y : B x) (e : _) →
                    let eA = fstC e in
                    let x' = cast A A' eA x in
                    let eB = sndC e x in
                    cast (Σ A B) (Σ A' B') e (x , y) ≡
                    (cast A A' eA x , cast (B x) (B' x') eB y)

{-# REWRITE cast-Sigma #-}

postulate cast-prod : (A A' : Set ℓ) (B B' : Set ℓ₁) (x : A) (y : B) (e : _) →
                    let eA = fstC e in
                    let eB = sndC e in
                    cast (prod A B) (prod A' B') e (x , y) ≡
                    (cast A A' eA x , cast B B' eB y)

{-# REWRITE cast-prod #-}

postulate cast-Sum-inj₁ : (A A' : Set ℓ) (B B' : Set ℓ₁) (a : A) (e : _) →
                    let eA = fstC e in
                    let eB = sndC e in
                    cast (A ⊎ B) (A' ⊎ B') e (inj₁ a) ≡
                    inj₁ (cast A A' eA a)

postulate cast-Sum-inj₂ : (A A' : Set ℓ) (B B' : Set ℓ₁) (b : B) (e : _) →
                    let eA = fstC e in
                    let eB = sndC e in
                    cast (A ⊎ B) (A' ⊎ B') e (inj₂ b) ≡
                    inj₂ (cast B B' eB b)

{-# REWRITE cast-Sum-inj₁ #-}
{-# REWRITE cast-Sum-inj₂ #-}

postulate cast-List-nil : (A A' : Set ℓ) (e : _) →
                          cast (List A) (List A') e [] ≡ []

postulate cast-List-cons : (A A' : Set ℓ) (e : _) (a : A) (l : List A) →
                           cast (List A) (List A') e (a ∷ l) ≡
                           cast A A' e a ∷ cast _ _ e l

{-# REWRITE cast-List-nil #-}

{-# REWRITE cast-List-cons #-}

postulate cast-Nat : (e : _) (n : Nat) → cast Nat Nat e n ≡ n

{-# REWRITE cast-Nat #-}

postulate cast-Bool : (e : _) (b : Bool) → cast Bool Bool e b ≡ b

{-# REWRITE cast-Bool #-}

postulate cast-Unit : (e : _) (t : ⊤) → cast ⊤ ⊤ e t ≡ t

{-# REWRITE cast-Unit #-}

postulate cast-Box : (A A' : Prop ℓ) (a : A) (f : _) (g : _) →
                    cast (Box A) (Box A') (f , g) (box a) ≡ box (uninj f a)

{-# REWRITE cast-Box #-}

-- sanity check on closed terms

foo : transport-Id (λ (T : Σ Set (λ A → Σ A (λ _ → A → Set))) → ((snd (snd T)) (fst (snd T))))
                          (Nat , (0 , λ _ → Nat))
                          3
                          (Nat , (0 , λ _ → Nat))
                          (Id-refl {A = Σ Set (λ A → Σ A (λ _ → A → Set))} (Nat , (0 , λ _ → Nat)))
      ≡ 3
foo = refl

test-J-refl-on-closed-term : (X : Set ℓ) (x : X) →
       transport-Id (λ z → Σ ⊤ (λ z → ⊤)) x (tt , tt) x (Id-refl x) ≡ (tt , tt)
test-J-refl-on-closed-term X x = refl

-- Quotient types

{-
  Note that r s and t are not used in the definitions, they are just here
  to make sure the theory stays consistent, because postulating the quotient,
  we can derive them. In particular, with R = λ - - → ⊥, we would get
  a direct inconsistency using Id-refl
-}

record quotient-data ℓ : Set (lsuc ℓ) where
  constructor q-data
  field
    carrier : Set ℓ
    rel : carrier → carrier → Prop ℓ
    rel-refl : (x : carrier) → rel x x
    rel-sym : (x y : carrier) → rel x y → rel y x
    rel-trans : (x y z : carrier) → rel x y → rel y z → rel x z

open quotient-data public

postulate Quotient : (Q : quotient-data ℓ) →
                     Set ℓ

postulate pi : {Q : quotient-data ℓ} →
               carrier Q → Quotient Q

telescope-Quotient : Set (lsuc ℓ)
telescope-Quotient {ℓ} = Σ (Set ℓ) (λ A → A → A → Prop ℓ)

postulate Id-Quotient : (Q : quotient-data ℓ)
                        (a a' : carrier Q) →
                        Id (Quotient Q)
                           (pi a) (pi a') ≡ rel Q a a'

{-# REWRITE Id-Quotient #-}

postulate Quotient-elim : (Q : quotient-data ℓ)
               (P : Quotient Q → Set ℓ₁)
               (p : (x : carrier Q) → P (pi x))
               (e : (x y : carrier Q) → (r : rel Q x y) →
                    Id _ (transport-Id P (pi x) (p x) (pi y) r) (p y))
               (w : Quotient Q) → P w

postulate Quotient-elim-red : (Q : quotient-data ℓ)
                (P : Quotient Q → Set ℓ₁)
                (p : (x : carrier Q) → P (pi x))
                (e : (x y : carrier Q) → (r : rel Q x y) →
                     Id _ (transport-Id P (pi x) (p x) (pi y) r) (p y))
                (a : carrier Q) →
                Quotient-elim Q P p e (pi a)
                ≡ p a

{-# REWRITE Quotient-elim-red #-}

postulate Quotient-elim-prop : (Q : quotient-data ℓ)
               (P : Quotient Q → Prop ℓ₁)
               (p : (x : carrier Q) → P (pi x))
               (w : Quotient Q) → P w

postulate Id-Type-Quotient : (Q Q' : quotient-data ℓ) →
                Id (Set ℓ) (Quotient Q) (Quotient Q')
                ≡
                Id telescope-Quotient (carrier Q , rel Q) (carrier Q' , rel Q')

{-# REWRITE Id-Type-Quotient #-}

postulate cast-Quotient : (Q Q' : quotient-data ℓ)
                (a : carrier Q) (e : _) →
                cast (Quotient Q) (Quotient Q') e (pi a) ≡
                pi (cast (carrier Q) (carrier Q') (fstC e) a)

{-# REWRITE cast-Quotient #-}

-- double induction principle

Quotient-elim2-aux : (Q : quotient-data ℓ)
                 (P : Quotient Q → Quotient Q → Set ℓ₁)
                 (p : (x y : carrier Q) → P (pi x) (pi y))
                 (e : (x x' y y' : carrier Q) → (Q-rel1 : rel Q x x') → (Q-rel2 : rel Q y y') →
                            Id _ (transport-Id (P (pi x')) (pi y) (transport-Id (λ x → P x (pi y)) (pi x) (p x y) (pi x') Q-rel1) (pi y') Q-rel2) (p x' y')) (x : carrier Q) (w : Quotient Q) → P w (pi x)
Quotient-elim2-aux Q P p e x = Quotient-elim Q (λ w → P w (pi x)) (λ y → p y x) (λ y y' r → let e-cst = e y y' x x r (rel-refl Q x) in transport (λ e → Id (P (pi y') (pi x))
        (e
         (cast (P (pi y) (pi x)) (P (pi y') (pi x)) (ap (λ y → P y (pi x)) r) (p y x)))
        (p y' x)) (cast (P (pi y') (pi x)) (P (pi y') (pi x)) (ap (P (pi y')) (rel-refl Q x)))
           e-cst (λ w → w) λ a → cast-refl {A = P (pi y') (pi x)} (Id-refl (P (pi y') (pi x))) a )

Quotient-elim2 : (Q : quotient-data ℓ)
                 (P : Quotient Q → Quotient Q → Set ℓ₁)
                 (p : (x y : carrier Q) → P (pi x) (pi y))
                 (e : (x x' y y' : carrier Q) → (Q-rel1 : rel Q x x') → (Q-rel2 : rel Q y y') →
                         Id _ (transport-Id (P (pi x')) (pi y) (transport-Id (λ x → P x (pi y)) (pi x) (p x y) (pi x') Q-rel1) (pi y') Q-rel2) (p x' y'))
                 (w w' : Quotient Q) → P w w'
Quotient-elim2 Q P p e w =
  Quotient-elim Q (P w) (λ x → Quotient-elim2-aux Q P p e x w)
                (λ x x' r → Quotient-elim-prop Q (λ w → Id (P w (pi x'))
                (transport-Id (P w) (pi x) (Quotient-elim2-aux Q P p e x w) (pi x') r)
                (Quotient-elim2-aux Q P p e x' w)) (λ y → let e-cst = e y y x x' (rel-refl Q y) r in
                                    transport (λ e → Id (P (pi y) (pi x'))
        (cast (P (pi y) (pi x)) (P (pi y) (pi x')) (ap (P (pi y)) r) (e (p y x)))
        (p y x')) (cast (P (pi y) (pi x)) (P (pi y) (pi x)) (ap (P (pi y)) (rel-refl Q x)))
           e-cst (λ w → w)  λ a → cast-refl {A = P (pi y) (pi x)} (Id-refl (P (pi y) (pi x))) a  ) w)

{-
-- Sanity Check: transport-refl on quotient type

transport-refl-Quotient : (X : Set ℓ)
                  (carrier Q : X -> Set ℓ₁)
                  (R : (x : X) → carrier Q x → carrier Q x → Prop ℓ₁)
                  (r : (z : X) (x : carrier Q z) → R z x x)
                  (s : (z : X) (x y : carrier Q z) → R z x y → R z y x)
                  (t : (zz : X) (x y z : carrier Q zz) → R zz x y → R zz y z → R zz x z)
                  (x : X) (q : Quotient (carrier Q x) (R x) (r x) (s x) (t x))
                  (e : Id X x x) →
                  Id _
                    (transport-Id (λ x → Quotient (carrier Q x) (R x) (r x) (s x) (t x))
                               x q x e)
                    q
transport-refl-Quotient X carrier Q R r s t x q e =
  Quotient-elim-prop (carrier Q x) (R x) (r x) (s x) (t x)
                     ((λ a → Id _ (transport-Id (λ (x : X) → Quotient (carrier Q x) (R x) (r x) (s x) (t x)) x a x e) a))
                     (λ a →  transport (λ a' → R x a' a) a (r x a) (cast (carrier Q x) (carrier Q x) _ a) (inverse (carrier Q x) (transport-refl carrier Q x a e)))
                     q

-}

-- Now for Path

telescope-Path : Set (lsuc ℓ)
telescope-Path {ℓ} = Σ (Set ℓ) (λ A → prod A A)

postulate Id-Path : (A : Set ℓ) (x : A) (y : A) (e e' : _)→
                    Id (x ≡ y) e e' ≡ ⊤P

{-# REWRITE Id-Path #-}

postulate Id-Type-Path : (A A' : Set ℓ) (x y : A) (x' y' : A') →
                       Id (Set ℓ) (x ≡ y) (x' ≡ y') ≡
                       Id telescope-Path
                         (A  , (x , y))
                         (A' , (x' , y' ))

{-# REWRITE Id-Type-Path #-}

-- not enough to get canonicity

-- postulate cast-Path : (A A' : Set ℓ) (x : A) (x' : A') (e : _) →
                    -- cast (x ≡ x) (x' ≡ x') e refl ≡ refl

-- {-# REWRITE cast-Path #-}

transport-Path : {A : Set ℓ} (x : A) (P :  (y : A) → Set ℓ₁)  (t : P x) (y : A) (e : x ≡ y) → P y
transport-Path P x t y refl = t

transport-Path-refl : {A : Set ℓ} (P : A → Prop ℓ₁) (x : A) (t : P x) (y : A) (e : x ≡ y) → P y
transport-Path-refl P x t .x refl = t

path-to-Id : {A : Set ℓ} {x y : A} → x ≡ y → Id A x y
path-to-Id {ℓ} {A} {x} {y} = transport-Path-refl (Id A x) x (Id-refl x) y

-- we treat cast X (a ≡ b) e x as a new constructor of equality

postulate IdPath : {A : Set ℓ} {x y : A} → Id A x y → x ≡ y

postulate transport-Path-cast-refl : {A B : Set ℓ} (a : A) (b b' : B) (e : Id (Set ℓ) (a ≡ a) (b ≡ b')) →
                             cast (a ≡ a) (b ≡ b') e refl ≡
                             IdPath ( let X = fstC (sndC e) in let Y = sndC (sndC e) in concatId B (inverse B X) Y)

{-# REWRITE transport-Path-cast-refl #-}

postulate transport-Path-IdPath : {A : Set ℓ} (x : A) (P : (y : A) → Set ℓ₁) (t : P x) (y : A) (e : Id A x y) →
                        transport-Path x P t y (IdPath e) ≡ transport-Id P x t y e

{-# REWRITE transport-Path-IdPath #-}

postulate transport-Path-cast-IdPath : {A B : Set ℓ} (a a' : A) (b b' : B) (ea : Id A a a') (e : Id (Set ℓ) (a ≡ a') (b ≡ b')) →
                             cast (a ≡ a') (b ≡ b') e (IdPath ea) ≡
                             IdPath (concatId B (inverse B (fstC (sndC e)))
                                          (concatId B  (ap (cast A B (fstC e)) ea) (sndC (sndC e))))

{-# REWRITE transport-Path-cast-IdPath #-}

transport-refl-Path : {A : Set ℓ} (P : A → Set ℓ₁) (x : A) (t : P x) → transport-Path x P t x refl ≡ t
transport-refl-Path P x t = refl

funext-Path : (A : Set ℓ) (B : A → Set ℓ₁) (f g : (a : A) → B a) →
          ((a : A) → f a ≡ g a) → f ≡ g
funext-Path A B f g e = IdPath (λ a → path-to-Id (e a))

etaBool : (a : Bool) → a ≡ (if a then true else false)
etaBool true = refl
etaBool false = refl

eq_fun : (λ (b : Bool) → b) ≡ (λ (b : Bool) → if b then true else false)
eq_fun = funext-Path Bool (λ - → Bool) _ _ λ a → etaBool a

-- standard boolean using equality

std-bool : Bool
std-bool = transport-Path (λ (b : Bool) → b) (λ f → Bool) true (λ (b : Bool) → if b then true else false) eq_fun

sanity-check : std-bool ≡ true
sanity-check = refl

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
------------------------------------------------------------------------
-- A parser for PBM images; illustrates "essential" use of bind
------------------------------------------------------------------------

-- Note that I am using the simple "Plain PBM" format, and I try to
-- adhere to the following statement from the pbm man page:
--
--   "Programs that read this format should be as lenient as possible,
--   accepting anything that looks remotely like a bitmap."

-- I got the idea to write this particular parser from "The Power of
-- Pi" by Oury and Swierstra.

module StructurallyRecursiveDescentParsing.PBM where

import Data.Vec as Vec
import Data.List as List
open import Codata.Musical.Notation
open import Data.Bool
open import Data.Char using (_==_)
import Data.Char.Properties as Char
import Data.String as String
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality

open import StructurallyRecursiveDescentParsing.Grammar
open import StructurallyRecursiveDescentParsing.Lib
open import StructurallyRecursiveDescentParsing.DepthFirst
open Token Char.decSetoid

open import TotalParserCombinators.Examples.PBM using (module PBM)
open PBM

mutual

  comment : Parser EmptyNT _ _ _
  comment = tt <$ tok '#'
               <⊛ sat' (not ∘ _==_ '\n') ⋆
               <⊛ tok '\n'

  colour = white <$ tok '0'
         ∣ black <$ tok '1'

  pbm =
     w∣c ⋆ ⊛>
     theString (String.toVec "P1") ⊛>
     w∣c ⋆ ⊛>
     number !>>= λ cols → ♯ -- _>>=_ works just as well.
    (w∣c + ⊛>
     number >>=  λ rows →   -- _!>>=_ works just as well.
     w∣c ⊛>
     (toPBM <$> exactly rows (exactly cols (w∣c ⋆ ⊛> colour))) <⊛
     any ⋆)
    where w∣c = whitespace ∣ comment

module Example where

  open Vec

  image = toPBM ((white ∷ black ∷ white ∷ []) ∷
                 (black ∷ white ∷ black ∷ []) ∷
                 (white ∷ black ∷ white ∷ []) ∷ [])

  ex : parseComplete (⟦ pbm ⟧ emptyGrammar)
                     (String.toList (show image)) ≡
       List.[_] image
  ex = refl

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Setoids.Setoids
open import Rings.Definition
open import Rings.IntegralDomains.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.PrincipalIdealDomains.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open import Rings.Ideals.Principal.Definition R
open import Rings.Ideals.Definition R

PrincipalIdealDomain : {c : _} → Set (a ⊔ b ⊔ lsuc c)
PrincipalIdealDomain {c} = {pred : A → Set c} → (ideal : Ideal pred) → PrincipalIdeal ideal


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Lists.Definition
open import Lists.Concat

module Lists.Reversal.Reversal where

rev : {a : _} → {A : Set a} → List A → List A
rev [] = []
rev (x :: l) = (rev l) ++ [ x ]

revIsHom : {a : _} → {A : Set a} → (l1 : List A) → (l2 : List A) → (rev (l1 ++ l2) ≡ (rev l2) ++ (rev l1))
revIsHom l1 [] = applyEquality rev (appendEmptyList l1)
revIsHom [] (x :: l2) with (rev l2 ++ [ x ])
... | r = equalityCommutative (appendEmptyList r)
revIsHom (w :: l1) (x :: l2) = transitivity t (equalityCommutative s)
  where
    s : ((rev l2 ++ [ x ]) ++ (rev l1 ++ [ w ])) ≡ (((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ])
    s = equalityCommutative (concatAssoc (rev l2 ++ (x :: [])) (rev l1) ([ w ]))
    t' : rev (l1 ++ (x :: l2)) ≡ rev (x :: l2) ++ rev l1
    t' = revIsHom l1 (x :: l2)
    t : (rev (l1 ++ (x :: l2)) ++ [ w ]) ≡ ((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ]
    t = applyEquality (λ r → r ++ [ w ]) {rev (l1 ++ (x :: l2))} {((rev l2) ++ [ x ]) ++ rev l1} (transitivity t' (applyEquality (λ r → r ++ rev l1) {rev l2 ++ (x :: [])} {rev l2 ++ (x :: [])} refl))

revRevIsId : {a : _} → {A : Set a} → (l : List A) → (rev (rev l) ≡ l)
revRevIsId [] = refl
revRevIsId (x :: l) = t
  where
    s : rev (rev l ++ [ x ] ) ≡ [ x ] ++ rev (rev l)
    s = revIsHom (rev l) [ x ]
    t : rev (rev l ++ [ x ] ) ≡ [ x ] ++ l
    t = identityOfIndiscernablesRight _≡_ s (applyEquality (λ n → [ x ] ++ n) (revRevIsId l))


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

module Experiment.Omniscience where

open import Level using () renaming (zero to lzero)
open import Data.Nat using (ℕ; zero; suc; _≤_; _+_)
open import Data.Nat.Properties using (≤-refl; +-identityʳ)
open import Data.Product using (Σ; _,_; proj₁; proj₂; ∃; _×_)
open import Data.Bool using (Bool; true; false; _∧_; not)
open import Data.Bool.Properties using (∧-assoc; ∧-idem)
open import Function.Base using (_$_)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; subst; sym; _≢_; cong; module ≡-Reasoning)

infix 5 _≤ᵇ_

_≤ᵇ_ : Bool → Bool → Bool
false ≤ᵇ false = true
true  ≤ᵇ false = false
false ≤ᵇ true  = true
true  ≤ᵇ true  = true

x≤ᵇtrue≡true : ∀ x → x ≤ᵇ true ≡ true
x≤ᵇtrue≡true false = refl
x≤ᵇtrue≡true true  = refl

Decrease : (ℕ → Bool) → Set
Decrease α = ∀ i → α (suc i) ≤ᵇ α i ≡ true

ℕ∞ : Set
ℕ∞ = Σ (ℕ → Bool) Decrease

-- less n i ≡ true <=> n > i
less : ℕ → ℕ → Bool
less zero    zero    = false
less zero    (suc n) = false
less (suc m) zero    = true
less (suc m) (suc n) = less m n

less-decrease : ∀ n → Decrease (less n)
less-decrease zero     zero   = refl
less-decrease zero    (suc i) = refl
less-decrease (suc n) zero    = x≤ᵇtrue≡true (less n 0)
less-decrease (suc n) (suc i) = less-decrease n i

toℕ∞ : ℕ → ℕ∞
toℕ∞ n = less n , less-decrease n

_≈C_ : Rel (ℕ → Bool) lzero
α ≈C β = ∀ i → α i ≡ β i

_≈_ : Rel ℕ∞ lzero
x ≈ y = proj₁ x ≈C proj₁ y

_#C_ : Rel (ℕ → Bool) lzero
α #C β = ∃ λ i → α i ≢ β i

_#_ : Rel ℕ∞ lzero
x # y = proj₁ x #C proj₁ y

-- retract
𝓇 : (ℕ → Bool) → (ℕ → Bool)
𝓇 α zero    = α 0
𝓇 α (suc n) = α (suc n) ∧ 𝓇 α n

𝓇-decrease : ∀ α → Decrease (𝓇 α)
𝓇-decrease α i = lemma (α (suc i)) (𝓇 α i)
  where
  lemma : ∀ x y → x ∧ y ≤ᵇ y ≡ true
  lemma false false = refl
  lemma false true  = refl
  lemma true  false = refl
  lemma true  true  = refl

𝓇-idem : ∀ α → 𝓇 (𝓇 α) ≈C 𝓇 α
𝓇-idem α zero    = refl
𝓇-idem α (suc i) = begin
  (α (suc i) ∧ 𝓇 α i) ∧ 𝓇 (𝓇 α) i
    ≡⟨ cong (λ v → (α (suc i) ∧ 𝓇 α i) ∧ v) $ 𝓇-idem α i ⟩
  (α (suc i) ∧ 𝓇 α i) ∧ 𝓇 α i
    ≡⟨ ∧-assoc (α (suc i)) (𝓇 α i) (𝓇 α i) ⟩
  α (suc i) ∧ (𝓇 α i ∧ 𝓇 α i)
    ≡⟨ cong (λ v → α (suc i) ∧ v) $ ∧-idem (𝓇 α i) ⟩
  α (suc i) ∧ 𝓇 α i ∎
  where open ≡-Reasoning

⟦_⟧ : ℕ∞ → (ℕ → Bool)
⟦_⟧ = proj₁

private
  contraposition-Bool : ∀ {x y z} → (x ≡ z → y ≡ z) → y ≡ not z → x ≡ not z
  contraposition-Bool {false} {false} {true} f e = refl
  contraposition-Bool {false} {true} {false} f e = (λ ()) $ f refl
  contraposition-Bool {true}  {false} {true} f e = (λ ()) $ f refl
  contraposition-Bool {true}  {true} {false} f e = refl

  ≤ᵇ-to-fun : ∀ {x y} → x ≤ᵇ y ≡ true → x ≡ true → y ≡ true
  ≤ᵇ-to-fun {true} {true} _ _ = refl

lemma-3-2-lemma : ∀ (x : ℕ∞) m n → ⟦ x ⟧ n ≡ false → ⟦ x ⟧ (m + n) ≡ false
lemma-3-2-lemma x@(α , d) zero    n αn≡false = αn≡false
lemma-3-2-lemma x@(α , d) (suc m) n αn≡false =
  contraposition-Bool (≤ᵇ-to-fun (d (m + n))) (lemma-3-2-lemma x m n αn≡false)

lemma-3-2 : ∀ (x : ℕ∞) n → ⟦ x ⟧ n ≡ false → ∃ λ k → k ≤ n × x ≈ toℕ∞ k
lemma-3-2 x@(α , d) zero    αn≡false = 0 , (≤-refl , f)
  where
  f : ∀ i → α i ≡ less 0 i
  f zero    = αn≡false
  f (suc i) = subst (λ v → α (suc v) ≡ false) (+-identityʳ i) $
                lemma-3-2-lemma x (suc i) 0 αn≡false
lemma-3-2 (α , d) (suc n) αn≡false = {!   !}

-- α i ≡ less 0 i


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Monoid.Construct.Unit where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Monoid
open import Cubical.Data.Prod using (_,_)

open import Cubical.Data.Unit

import Cubical.Algebra.Semigroup.Construct.Unit as ⊤Semigroup
open ⊤Semigroup public hiding (⊤-isSemigroup; ⊤-Semigroup)

◯-identityˡ : LeftIdentity tt _◯_
◯-identityˡ _ = refl

◯-identityʳ : RightIdentity tt _◯_
◯-identityʳ _ = refl

◯-identity : Identity tt _◯_
◯-identity = ◯-identityˡ , ◯-identityʳ

⊤-isMonoid : IsMonoid ⊤ _◯_ tt
⊤-isMonoid = record
  { isSemigroup = ⊤Semigroup.⊤-isSemigroup
  ; identity    = ◯-identity
  }

⊤-Monoid : Monoid ℓ-zero
⊤-Monoid = record { isMonoid = ⊤-isMonoid }


text:
module Data.List.All.Properties.Extra {a}{A : Set a} where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Fin
open import Data.List as List hiding (reverse)
open import Data.List.Relation.Unary.Any hiding (tail)
open import Data.List.Membership.Propositional
open import Data.List.Properties.Extra
open import Data.List.At
open import Data.List.Relation.Unary.All as All hiding (_[_]=_)
open import Data.List.Relation.Unary.All.Properties
open import Data.Product
open import Function

map-map : ∀ {p q r}{P : A → Set p}{Q : A → Set q}{R : A → Set r}{l : List A}(ps : All P l)
          {f : ∀ {x : A} → P x → Q x}{g : ∀ {x : A} → Q x → R x} →
          All.map g (All.map f ps) ≡ All.map (g ∘ f) ps
map-map [] = refl
map-map (px ∷ ps) = cong₂ _∷_ refl (map-map ps)

drop-all : ∀ {p}{P : A → Set p}{l : List A} n → All P l → All P (drop n l)
drop-all zero px = px
drop-all (suc n) [] = []
drop-all (suc n) (px ∷ pxs) = drop-all n pxs

split-++ : ∀ {p}{P : A → Set p}(l m : List A) → All P (l ++ m) → All P l × All P m
split-++ [] m pxs = [] , pxs
split-++ (x ∷ l) m (px ∷ pxs) with split-++ l m pxs
... | lp , rp = px ∷ lp , rp

_++-all_ : ∀ {l m p}{P : A → Set p} → All P l → All P m → All P (l ++ m)
[] ++-all pm = pm
(px ∷ pl) ++-all pm = px ∷ (pl ++-all pm)

∈-all : ∀ {p}{P : A → Set p}{l : List A}{x} → x ∈ l → All P l → P x
∈-all (here refl) (px ∷ q) = px
∈-all (there p) (px ∷ q) = ∈-all p q

-- proof matters; update a particular witness of a property
_All[_]≔_ : ∀ {p}{P : A → Set p} {xs : List A} {i x} →
            All P xs → xs [ i ]= x → P x → All P xs
_All[_]≔_ [] ()
_All[_]≔_ {xs = .(_ ∷ _)} {zero} (px ∷ xs) refl px' = px' ∷ xs
_All[_]≔_ {xs = .(_ ∷ _)} {suc i} (px ∷ xs) q px' = px ∷ (xs All[ q ]≔ px')

-- strong update
-- _All[_]≔!_ : ∀ {p}{P : A → Set p} {xs : List A} {x} →
--             All P xs → (i : Fin (length xs)) → P x → All P (xs [ i ]≔ x)
-- [] All[ () ]≔! y
-- (px ∷ xs) All[ zero ]≔! y = y ∷ xs
-- (px ∷ xs) All[ suc i ]≔! y = px ∷ xs All[ i ]≔! y

_all-∷ʳ_ : ∀ {p}{l : List A} {x} {P : A → Set p} → All P l → P x → All P (l ∷ʳ x)
_all-∷ʳ_ [] q = q ∷ []
_all-∷ʳ_ (px ∷ p) q = px ∷ (p all-∷ʳ q)

-- All≔'∘map : ∀ {p q}{P : A → Set p}{Q : A → Set q}{xs : List A} {x}(pxs : All P xs)(e : x ∈ xs)(px : P x)(f : ∀ {x} → P x → Q x) →
--             (All.map f pxs) All[ e ]≔' (f px) ≡ All.map f (pxs All[ e ]≔' px)
-- All≔'∘map [] ()
-- All≔'∘map (px ∷ pxs) (here refl) qx f = refl
-- All≔'∘map (px ∷ pxs) (there e) qx f = cong₂ _∷_ refl (All≔'∘map pxs e qx f)

all-∷ʳ∘map : ∀ {p q}{P : A → Set p}{Q : A → Set q}{xs : List A} {x}(pxs : All P xs)(px : P x)(f : ∀ {x} → P x → Q x) →
             (All.map f pxs) all-∷ʳ (f px) ≡ All.map f (pxs all-∷ʳ px)
all-∷ʳ∘map [] px f = refl
all-∷ʳ∘map (px₁ ∷ pxs) px f = cong₂ _∷_ refl (all-∷ʳ∘map pxs px f)

lookup∘map : ∀ {p q}{P : A → Set p}{Q : A → Set q}{xs : List A} {x}(pxs : All P xs)(e : x ∈ xs)(f : ∀ {x} → P x → Q x) →
             All.lookup (All.map f pxs) e ≡ f (All.lookup pxs e)
lookup∘map [] ()
lookup∘map (px ∷ pxs) (here refl) f = refl
lookup∘map (px ∷ pxs) (there e) f = lookup∘map pxs e f

erase : ∀ {p b}{P : A → Set p}{l : List A}{B : Set b} → (∀ {x} → P x → B) → All P l → List B
erase f [] = []
erase f (px ∷ xs₁) = f px ∷ erase f xs₁

-- pop₁ : ∀ {x : A}{p xs}{P : A → Set p} → All P (x ∷ xs) → P x × All P xs
-- pop₁ st = head st , tail st

-- open import Data.List.Properties
-- popₙ : ∀ (as : List A){p xs}{P : A → Set p} → All P (as ++ xs) → All P (List.reverse as) × All P xs
-- popₙ [] st = [] , st
-- popₙ (x ∷ xs) (px ∷ pxs) rewrite unfold-reverse x xs =
--   let pys , pzs = popₙ xs pxs in (pys all-∷ʳ px) , pzs

-- open import Relation.Binary.Core
-- open import Data.List.Relation.Pointwise hiding (Rel)
-- module _ {a ℓ}{A : Set a}(_∼_ : Rel A ℓ) where

--   pw-map : ∀ {l m p}{P : A → Set p} → (∀ {a b} → a ∼ b → P a → P b) → Pointwise _∼_ l m → All P l → All P m
--   pw-map f [] [] = []
--   pw-map f (x∼y ∷ r) (px ∷ xs) = f x∼y px ∷ pw-map f r xs


text:
module Examples.OpSem where

open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
open import Luau.Syntax using (Block; var; nil; local_←_; _∙_; done; return; block_is_end)
open import Luau.Heap using (∅)

ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
ex1 = subst


text:
------------------------------------------------------------------------------
-- Testing Agda internal term: @Con@
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- The following hint uses the internal Agda term @Con@.

module AgdaInternalTerms.ConTerm where

-- We add 3 to the fixities of the standard library.
infixl 9 _+_
infix  7 _≡_

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

data ℕ : Set where
  zero :     ℕ
  succ : ℕ → ℕ

data _≡_ (n : ℕ) : ℕ → Set where
  refl : n ≡ n

_+_ : ℕ → ℕ → ℕ
zero   + n = n
succ m + n = succ (m + n)

+-0x : ∀ n → zero + n ≡ n
+-0x n = refl
{-# ATP hint +-0x #-}

postulate foo : ∀ n → zero + n ≡ n
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
open import Prelude
open import Data.Maybe using (Maybe; just; nothing)

open import RW.Language.RTerm
open import RW.Language.RTermUtils using (hole2Abs)
open import RW.Language.Instantiation using (RSubst)
open import RW.Utils.Error
open import RW.Strategy

module RW.Strategy.PropEq where

  pattern pat-≡  = (rdef (quote _≡_))

  private
    open UData

    ≡-when : RTermName → RTermName → Bool
    ≡-when pat-≡ pat-≡ = true
    ≡-when _     _     = false

    fixTrs : Trs → RTerm ⊥ → RTerm ⊥
    fixTrs Symmetry term = rapp (rdef (quote sym)) (term ∷ [])

    ≡-how : Name → UData → Err StratErr (RTerm ⊥)
    ≡-how act (u-data g□ σ trs)
      = i2 (rapp (rdef (quote cong))
                 ( hole2Abs g□
                 ∷ foldr fixTrs (makeApp act σ) trs
                 ∷ [])
           )

  ≡-strat : TStrat
  ≡-strat = record
    { when = ≡-when
    ; how  = ≡-how
    }

  open import RW.RW (≡-strat ∷ [])

  by*-≡ : by*-tactic
  by*-≡ = by* (quote trans)

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
module Id where

id : {A : Set} -> A -> A
id x = {!!}

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


text:
------------------------------------------------------------------------------
-- Proving mirror (mirror t) = t using mutual data types
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.Program.Mirror.MirrorMutualSL where

infixr 5 _∷_ _++_

open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

------------------------------------------------------------------------------
-- The mutual data types

data Tree   (A : Set) : Set
data Forest (A : Set) : Set

data Tree A where
  tree : A → Forest A → Tree A

data Forest A where
  []  : Forest A
  _∷_ : Tree A → Forest A → Forest A

------------------------------------------------------------------------------
-- Auxiliary functions

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

map : {A B : Set} → (Tree A → Tree B) → Forest A → Forest B
map f []       = []
map f (a ∷ ts) = f a ∷ map f ts

reverse : {A : Set} → Forest A → Forest A
reverse []       = []
reverse (a ∷ ts) = reverse ts ++ a ∷ []

postulate
  map-++     : {A B : Set}(f : Tree A → Tree B)(xs ys : Forest A) →
               map f (xs ++ ys) ≡ map f xs ++ map f ys
  reverse-++ : {A : Set}(xs ys : Forest A) →
               reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

------------------------------------------------------------------------------
-- The mirror function.

{-# TERMINATING #-}
mirror : {A : Set} → Tree A → Tree A
mirror (tree a ts) = tree a (reverse (map mirror ts))

------------------------------------------------------------------------------
-- The proof of the property.
mirror-involutive : {A : Set} → (t : Tree A) → mirror (mirror t) ≡ t
helper            : {A : Set} → (ts : Forest A) →
                  reverse (map mirror (reverse (map mirror ts))) ≡ ts

mirror-involutive (tree a []) = refl
mirror-involutive (tree a (t ∷ ts)) =
  begin
    tree a (reverse (map mirror (reverse (map mirror ts) ++ mirror t ∷ [])))
      ≡⟨ cong (tree a) (helper (t ∷ ts)) ⟩
    tree a (t ∷ ts)
  ∎

helper [] = refl
helper (t ∷ ts) =
  begin
    reverse (map mirror (reverse (map mirror ts) ++ mirror t ∷ []))
     ≡⟨ cong reverse
             (map-++ mirror (reverse (map mirror ts)) (mirror t ∷ []))
     ⟩
    reverse (map mirror (reverse (map mirror ts)) ++
            (map mirror (mirror t ∷ [])))
      ≡⟨ subst (λ x → (reverse (map mirror (reverse (map mirror ts)) ++
                                    (map mirror (mirror t ∷ [])))) ≡ x)
               (reverse-++ (map mirror (reverse (map mirror ts)))
                           (map mirror (mirror t ∷ [])))
               refl
      ⟩
    reverse (map mirror (mirror t ∷ [])) ++
    reverse (map mirror (reverse (map mirror ts)))
      ≡⟨ refl ⟩
    mirror (mirror t) ∷ reverse (map mirror (reverse (map mirror ts)))
      ≡⟨ cong (flip _∷_ (reverse (map mirror (reverse (map mirror ts)))))
              (mirror-involutive t)
      ⟩
    t ∷ reverse (map mirror (reverse (map mirror ts)))
      ≡⟨ cong (_∷_ t) (helper ts) ⟩
    t ∷ ts
  ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Data.Tree.Instance where

open import Class.Functor
open import Class.Monad
open import Class.Monoid
open import Class.Show
open import Class.Traversable
open import Data.List
open import Data.List.Instance
open import Data.String using (String)
open import Data.String.Instance
open import Data.Tree.Base

instance
  {-# TERMINATING #-}
  Tree-Functor : Functor Tree
  Tree-Functor = record { _<$>_ = helper }
    where
      helper : ∀ {A B} -> (A -> B) -> Tree A -> Tree B
      helper f (Node x x₁) = Node (f x) (map (helper f) x₁)

  {-# TERMINATING #-}
  Tree-Show : ∀ {A} {{_ : Show A}} -> Show (Tree A)
  Tree-Show = record { show = helper show }
    where
      helper : ∀ {A} -> (A -> String) -> Tree A -> String
      helper f (Node x x₁) = "Node (" + f x + ") " + show (map (helper f) x₁)

  {-# TERMINATING #-}
  Tree-Traversable : Traversable Tree
  Tree-Traversable = record { sequence = helper }
    where
      helper : {M : Set → Set} {{_ : Monad M}} {A : Set} → Tree (M A) → M (Tree A)
      helper (Node x y) = do
        x' <- x
        y' <- sequence (map helper y)
        return (Node x' y')

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
-- Getting projection like functions right was a little tricky.
-- Here are the cases that didn't work and weren't caught by
-- existing test cases.
module ProjectionLikeFunctions where

record Wrap (A : Set) : Set where
  constructor [_]
  field unwrap : A

postulate
  Nat   : Set
  n     : Nat
  Thm   : Nat → Set
  prf   : ∀ n → Thm n

module M x (p : Thm x) (w : Wrap Nat) where
  module W = Wrap w

module M′ = M n (prf n) ([ n ])

test₁ : Thm M′.W.unwrap
test₁ = prf n

eq! : ∀ x (S : Thm x) → Wrap Nat → Nat
eq! s S [n] = W.unwrap
  module Local where
    module W = Wrap [n]

test₂ : Thm (eq! n (prf n) [ n ])
test₂ = prf n


text:
module IsPropositionalFormula where

open import OscarPrelude
open import Formula
open import Term
open import PredicateName
open import HasNeitherNor

data IsPropositionalFormula : Formula → Set
 where
  atomic : (𝑃 : PredicateName) → (τs : Terms) → IsPropositionalFormula $ 𝑃[ 𝑃 ♭ τs ]
  logical : {φ₁ : Formula} → IsPropositionalFormula φ₁ → {φ₂ : Formula} → IsPropositionalFormula φ₂ → IsPropositionalFormula (φ₁ ⊗ φ₂)

instance EqIsPropositionalFormula : ∀ {φ} → Eq (IsPropositionalFormula φ)
Eq._==_ EqIsPropositionalFormula (atomic _ _) (atomic _ _ ) = yes refl
Eq._==_ EqIsPropositionalFormula (logical φ₁₁ φ₁₂) (logical φ₂₁ φ₂₂) with φ₁₁ ≟ φ₂₁ | φ₁₂ ≟ φ₂₂
Eq._==_ EqIsPropositionalFormula (logical φ₁₁ φ₁₂) (logical φ₂₁ φ₂₂) | yes refl | yes refl = yes refl
Eq._==_ EqIsPropositionalFormula (logical φ₁₁ φ₁₂) (logical φ₂₁ φ₂₂) | yes refl | no φ₁₂≢φ₂₂ = no λ {refl → φ₁₂≢φ₂₂ refl}
Eq._==_ EqIsPropositionalFormula (logical φ₁₁ φ₁₂) (logical φ₂₁ φ₂₂) | no φ₁₁≢φ₂₁ | _ = no λ {refl → φ₁₁≢φ₂₁ refl}

{-
-- need to use coinduction to prove this
foo : ¬ ∃ λ φ → ∃ λ (p₁ : IsPropositionalFormula φ) → ∃ λ (p₂ : IsPropositionalFormula φ) → p₁ ≢ p₂
foo (atomic x x₁ , atomic .x .x₁ , atomic .x .x₁ , snd₁) = snd₁ refl
foo (logical fst₁ fst₂ , logical fst₃ fst₄ , logical fst₅ fst₆ , snd₁) with fst₃ ≟ fst₅ | fst₄ ≟ fst₆
foo (logical fst₁ fst₂ , logical fst₃ fst₄ , logical .fst₃ .fst₄ , snd₁) | yes refl | (yes refl) = snd₁ refl
foo (logical fst₁ fst₂ , logical fst₃ fst₄ , logical .fst₃ fst₆ , snd₁) | yes refl | (no x₁) = foo (fst₂ , fst₄ , fst₆ , λ xs → x₁ xs)
foo (logical fst₁ fst₂ , logical fst₃ fst₄ , logical fst₅ fst₆ , snd₁) | no x | (yes x₁) = {!!}
foo (logical fst₁ fst₂ , logical fst₃ fst₄ , logical fst₅ fst₆ , snd₁) | no x | (no x₁) = {!!}
foo (quantified x fst₁ , () , fst₃ , snd₁)
-}


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

macro

  m-0 : Term → TC ⊤
  m-0 goal =
    bindTC (inferType goal) λ where
      (pi (arg (arg-info _ (modality _ quantity-0)) _) _) →
        bindTC (quoteTC (λ (_ : Set) → Set))
               (unify goal)
      type → typeError (termErr type ∷ [])

  m-ω : Term → TC ⊤
  m-ω goal =
    bindTC (inferType goal) λ where
      (pi (arg (arg-info _ (modality _ quantity-ω)) _) _) →
        bindTC (quoteTC (λ (_ : Set) → Set))
               (unify goal)
      type → typeError (termErr type ∷ [])

_ : @0 Set → Set₁
_ = m-0

_ : @ω Set → Set₁
_ = m-ω

postulate
  f : @0 Set₁ → Set₁

macro

  m₁ : Set₁ → Term → TC ⊤
  m₁ A goal =
    bindTC (quoteTC A) λ A →
    unify goal
      (def (quote f)
         (arg (arg-info visible (modality relevant quantity-0)) A ∷
          []))

_ : Set₁ → Set₁
_ = λ A → m₁ A

macro

  m₂ : Set₁ → Term → TC ⊤
  m₂ A goal =
    bindTC (quoteTC A) λ A →
    unify goal
      (def (quote f)
                                -- The modality is ignored.
         (arg (arg-info visible (modality irrelevant quantity-ω)) A ∷
          []))

_ : Set₁ → Set₁
_ = λ A → m₂ A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda