text:
{-# OPTIONS --rewriting #-}

module Properties.Subtyping where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
open import Properties.Equality using (_≢_)
open import Properties.Functions using (_∘_)
open import Properties.Product using (_×_; _,_)

-- Language membership is decidable
dec-language : ∀ T t → Either (¬Language T t) (Language T t)
dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ()))
dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ()))
dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ()))
dec-language nil (scalar nil) = Right (scalar nil)
dec-language nil function = Left (scalar-function nil)
dec-language nil (function-ok t) = Left (scalar-function-ok nil)
dec-language nil (function-err t) = Left (scalar-function-err nil)
dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ()))
dec-language boolean (scalar boolean) = Right (scalar boolean)
dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ()))
dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ()))
dec-language boolean function = Left (scalar-function boolean)
dec-language boolean (function-ok t) = Left (scalar-function-ok boolean)
dec-language boolean (function-err t) = Left (scalar-function-err boolean)
dec-language number (scalar number) = Right (scalar number)
dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ()))
dec-language number (scalar string) = Left (scalar-scalar string number (λ ()))
dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ()))
dec-language number function = Left (scalar-function number)
dec-language number (function-ok t) = Left (scalar-function-ok number)
dec-language number (function-err t) = Left (scalar-function-err number)
dec-language string (scalar number) = Left (scalar-scalar number string (λ ()))
dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ()))
dec-language string (scalar string) = Right (scalar string)
dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ()))
dec-language string function = Left (scalar-function string)
dec-language string (function-ok t) = Left (scalar-function-ok string)
dec-language string (function-err t) = Left (scalar-function-err string)
dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s)
dec-language (T₁ ⇒ T₂) function = Right function
dec-language (T₁ ⇒ T₂) (function-ok t) = mapLR function-ok function-ok (dec-language T₂ t)
dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t))
dec-language never t = Left never
dec-language unknown t = Right unknown
dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)

-- ¬Language T is the complement of Language T
language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q
language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q
language-comp t (left p) (q₁ , q₂) = language-comp t p q₁
language-comp t (right p) (q₁ , q₂) = language-comp t p q₂
language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl
language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function
language-comp (scalar s) never (scalar ())
language-comp function (scalar-function ()) function
language-comp (function-ok t) (scalar-function-ok ()) (function-ok q)
language-comp (function-ok t) (function-ok p) (function-ok q) = language-comp t p q
language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p

-- ≮: is the complement of <:
¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U)
¬≮:-impl-<: {T} {U} p t q with dec-language U t
¬≮:-impl-<: {T} {U} p t q | Left r = CONTRADICTION (p (witness t q r))
¬≮:-impl-<: {T} {U} p t q | Right r = r

<:-impl-¬≮: : ∀ {T U} → (T <: U) → ¬(T ≮: U)
<:-impl-¬≮: p (witness t q r) = language-comp t r (p t q)

<:-impl-⊇ : ∀ {T U} → (T <: U) → ∀ t → ¬Language U t → ¬Language T t
<:-impl-⊇ {T} p t q with dec-language T t
<:-impl-⊇ {_} p t q | Left r = r
<:-impl-⊇ {_} p t q | Right r = CONTRADICTION (language-comp t q (p t r))

-- reflexivity
≮:-refl : ∀ {T} → ¬(T ≮: T)
≮:-refl (witness t p q) = language-comp t q p

<:-refl : ∀ {T} → (T <: T)
<:-refl = ¬≮:-impl-<: ≮:-refl

-- transititivity
≮:-trans-≡ : ∀ {S T U} → (S ≮: T) → (T ≡ U) → (S ≮: U)
≮:-trans-≡ p refl = p

≡-trans-≮: : ∀ {S T U} → (S ≡ T) → (T ≮: U) → (S ≮: U)
≡-trans-≮: refl p = p

≮:-trans : ∀ {S T U} → (S ≮: U) → Either (S ≮: T) (T ≮: U)
≮:-trans {T = T} (witness t p q) = mapLR (witness t p) (λ z → witness t z q) (dec-language T t)

<:-trans : ∀ {S T U} → (S <: T) → (T <: U) → (S <: U)
<:-trans p q t r = q t (p t r)

<:-trans-≮: : ∀ {S T U} → (S <: T) → (S ≮: U) → (T ≮: U)
<:-trans-≮: p (witness t q r) = witness t (p t q) r

≮:-trans-<: : ∀ {S T U} → (S ≮: U) → (T <: U) → (S ≮: T)
≮:-trans-<: (witness t p q) r = witness t p (<:-impl-⊇ r t q)

-- Properties of union

<:-union : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∪ S) <: (T ∪ U))
<:-union p q t (left r) = left (p t r)
<:-union p q t (right r) = right (q t r)

<:-∪-left : ∀ {S T} → S <: (S ∪ T)
<:-∪-left t p = left p

<:-∪-right : ∀ {S T} → T <: (S ∪ T)
<:-∪-right t p = right p

<:-∪-lub : ∀ {S T U} → (S <: U) → (T <: U) → ((S ∪ T) <: U)
<:-∪-lub p q t (left r) = p t r
<:-∪-lub p q t (right r) = q t r

<:-∪-symm : ∀ {T U} → (T ∪ U) <: (U ∪ T)
<:-∪-symm t (left p) = right p
<:-∪-symm t (right p) = left p

<:-∪-assocl : ∀ {S T U} → (S ∪ (T ∪ U)) <: ((S ∪ T) ∪ U)
<:-∪-assocl t (left p) = left (left p)
<:-∪-assocl t (right (left p)) = left (right p)
<:-∪-assocl t (right (right p)) = right p

<:-∪-assocr : ∀ {S T U} → ((S ∪ T) ∪ U) <: (S ∪ (T ∪ U))
<:-∪-assocr t (left (left p)) = left p
<:-∪-assocr t (left (right p)) = right (left p)
<:-∪-assocr t (right p) = right (right p)

≮:-∪-left : ∀ {S T U} → (S ≮: U) → ((S ∪ T) ≮: U)
≮:-∪-left (witness t p q) = witness t (left p) q

≮:-∪-right : ∀ {S T U} → (T ≮: U) → ((S ∪ T) ≮: U)
≮:-∪-right (witness t p q) = witness t (right p) q

-- Properties of intersection

<:-intersect : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∩ S) <: (T ∩ U))
<:-intersect p q t (r₁ , r₂) = (p t r₁ , q t r₂)

<:-∩-left : ∀ {S T} → (S ∩ T) <: S
<:-∩-left t (p , _) = p

<:-∩-right : ∀ {S T} → (S ∩ T) <: T
<:-∩-right t (_ , p) = p

<:-∩-glb : ∀ {S T U} → (S <: T) → (S <: U) → (S <: (T ∩ U))
<:-∩-glb p q t r = (p t r , q t r)

<:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T)
<:-∩-symm t (p₁ , p₂) = (p₂ , p₁)

≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U))
≮:-∩-left (witness t p q) = witness t p (left q)

≮:-∩-right : ∀ {S T U} → (S ≮: U) → (S ≮: (T ∩ U))
≮:-∩-right (witness t p q) = witness t p (right q)

-- Distribution properties
<:-∩-distl-∪ : ∀ {S T U} → (S ∩ (T ∪ U)) <: ((S ∩ T) ∪ (S ∩ U))
<:-∩-distl-∪ t (p₁ , left p₂) = left (p₁ , p₂)
<:-∩-distl-∪ t (p₁ , right p₂) = right (p₁ , p₂)

∩-distl-∪-<: : ∀ {S T U} → ((S ∩ T) ∪ (S ∩ U)) <: (S ∩ (T ∪ U))
∩-distl-∪-<: t (left (p₁ , p₂)) = (p₁ , left p₂)
∩-distl-∪-<: t (right (p₁ , p₂)) = (p₁ , right p₂)

<:-∩-distr-∪ : ∀ {S T U} → ((S ∪ T) ∩ U) <:  ((S ∩ U) ∪ (T ∩ U))
<:-∩-distr-∪ t (left p₁ , p₂) = left (p₁ , p₂)
<:-∩-distr-∪ t (right p₁ , p₂) = right (p₁ , p₂)

∩-distr-∪-<: : ∀ {S T U} → ((S ∩ U) ∪ (T ∩ U)) <: ((S ∪ T) ∩ U)
∩-distr-∪-<: t (left (p₁ , p₂)) = (left p₁ , p₂)
∩-distr-∪-<: t (right (p₁ , p₂)) = (right p₁ , p₂)

<:-∪-distl-∩ : ∀ {S T U} → (S ∪ (T ∩ U)) <: ((S ∪ T) ∩ (S ∪ U))
<:-∪-distl-∩ t (left p) = (left p , left p)
<:-∪-distl-∩ t (right (p₁ , p₂)) = (right p₁ , right p₂)

∪-distl-∩-<: : ∀ {S T U} → ((S ∪ T) ∩ (S ∪ U)) <: (S ∪ (T ∩ U))
∪-distl-∩-<: t (left p₁ , p₂) = left p₁
∪-distl-∩-<: t (right p₁ , left p₂) = left p₂
∪-distl-∩-<: t (right p₁ , right p₂) = right (p₁ , p₂)

<:-∪-distr-∩ : ∀ {S T U} → ((S ∩ T) ∪ U) <: ((S ∪ U) ∩ (T ∪ U))
<:-∪-distr-∩ t (left (p₁ , p₂)) = left p₁ , left p₂
<:-∪-distr-∩ t (right p) = (right p , right p)

∪-distr-∩-<: : ∀ {S T U} → ((S ∪ U) ∩ (T ∪ U)) <: ((S ∩ T) ∪ U)
∪-distr-∩-<: t (left p₁ , left p₂) = left (p₁ , p₂)
∪-distr-∩-<: t (left p₁ , right p₂) = right p₂
∪-distr-∩-<: t (right p₁ , p₂) = right p₁

-- Properties of functions
<:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U)
<:-function p q function function = function
<:-function p q (function-ok t) (function-ok r) = function-ok (q t r)
<:-function p q (function-err s) (function-err r) = function-err (<:-impl-⊇ p s r)

<:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U))
<:-function-∩-∪ function (function , function) = function
<:-function-∩-∪ (function-ok t) (function-ok p₁ , function-ok p₂) = function-ok (right p₂)
<:-function-∩-∪ (function-err _) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)

<:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U))
<:-function-∩ function (function , function) = function
<:-function-∩ (function-ok t) (function-ok p₁ , function-ok p₂) = function-ok (p₁ , p₂)
<:-function-∩ (function-err s) (function-err p₁ , function-err p₂) = function-err p₂

<:-function-∪ : ∀ {R S T U} → ((R ⇒ S) ∪ (T ⇒ U)) <: ((R ∩ T) ⇒ (S ∪ U))
<:-function-∪ function (left function) = function
<:-function-∪ (function-ok t) (left (function-ok p)) = function-ok (left p)
<:-function-∪ (function-err s) (left (function-err p)) = function-err (left p)
<:-function-∪ (scalar s) (left (scalar ()))
<:-function-∪ function (right function) = function
<:-function-∪ (function-ok t) (right (function-ok p)) = function-ok (right p)
<:-function-∪ (function-err s) (right (function-err x)) = function-err (right x)
<:-function-∪ (scalar s) (right (scalar ()))

<:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U))
<:-function-∪-∩ function function = left function
<:-function-∪-∩ (function-ok t) (function-ok (left p)) = left (function-ok p)
<:-function-∪-∩ (function-ok t) (function-ok (right p)) = right (function-ok p)
<:-function-∪-∩ (function-err s) (function-err (left p)) = left (function-err p)
<:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p)

≮:-function-left : ∀ {R S T U} → (R ≮: S) → (S ⇒ T) ≮: (R ⇒ U)
≮:-function-left (witness t p q) = witness (function-err t) (function-err q) (function-err p)

≮:-function-right : ∀ {R S T U} → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U)
≮:-function-right (witness t p q) = witness (function-ok t) (function-ok p) (function-ok q)

-- Properties of scalars
skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t))
skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))

scalar-<: : ∀ {S T} → (s : Scalar S) → Language T (scalar s) → (S <: T)
scalar-<: number p (scalar number) (scalar number) = p
scalar-<: boolean p (scalar boolean) (scalar boolean) = p
scalar-<: string p (scalar string) (scalar string) = p
scalar-<: nil p (scalar nil) (scalar nil) = p

scalar-∩-function-<:-never : ∀ {S T U} → (Scalar S) → ((T ⇒ U) ∩ S) <: never
scalar-∩-function-<:-never number .(scalar number) (() , scalar number)
scalar-∩-function-<:-never boolean .(scalar boolean) (() , scalar boolean)
scalar-∩-function-<:-never string .(scalar string) (() , scalar string)
scalar-∩-function-<:-never nil .(scalar nil) (() , scalar nil)

function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U)
function-≮:-scalar s = witness function function (scalar-function s)

scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T))
scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s)

unknown-≮:-scalar : ∀ {U} → (Scalar U) → (unknown ≮: U)
unknown-≮:-scalar s = witness (function-ok (scalar s)) unknown (scalar-function-ok s)

scalar-≮:-never : ∀ {U} → (Scalar U) → (U ≮: never)
scalar-≮:-never s = witness (scalar s) (scalar s) never

scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U)
scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p)

scalar-≢-∩-<:-never : ∀ {T U V} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ∩ U) <: V
scalar-≢-∩-<:-never s t p u (scalar s₁ , scalar s₂) = CONTRADICTION (p refl)

skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s))
skalar-scalar number = left (scalar number)
skalar-scalar boolean = right (right (right (scalar boolean)))
skalar-scalar string = right (left (scalar string))
skalar-scalar nil = right (right (left (scalar nil)))

-- Properties of unknown and never
unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U)
unknown-≮: (witness t p q) = witness t unknown q

never-≮: : ∀ {T U} → (T ≮: U) → (T ≮: never)
never-≮: (witness t p q) = witness t p never

unknown-≮:-never : (unknown ≮: never)
unknown-≮:-never = witness (scalar nil) unknown never

function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never)
function-≮:-never = witness function function never

<:-never : ∀ {T} → (never <: T)
<:-never t (scalar ())

≮:-never-left : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: T) → (S ∩ U) ≮: never
≮:-never-left p (witness t q₁ q₂) with p t q₁
≮:-never-left p (witness t q₁ q₂) | left r = CONTRADICTION (language-comp t q₂ r)
≮:-never-left p (witness t q₁ q₂) | right r = witness t (q₁ , r) never

≮:-never-right : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: U) → (S ∩ T) ≮: never
≮:-never-right p (witness t q₁ q₂) with p t q₁
≮:-never-right p (witness t q₁ q₂) | left r = witness t (q₁ , r) never
≮:-never-right p (witness t q₁ q₂) | right r = CONTRADICTION (language-comp t q₂ r)

<:-unknown : ∀ {T} → (T <: unknown)
<:-unknown t p = unknown

<:-everything : unknown <: ((never ⇒ unknown) ∪ skalar)
<:-everything (scalar s) p = right (skalar-scalar s)
<:-everything function p = left function
<:-everything (function-ok t) p = left (function-ok unknown)
<:-everything (function-err s) p = left (function-err never)

-- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf)
-- defines a "set-theoretic" model (sec 2.5)
-- Unfortunately we don't quite have this property, due to uninhabited types,
-- for example (never -> T) is equivalent to (never -> U)
-- when types are interpreted as sets of syntactic values.

_⊆_ : ∀ {A : Set} → (A → Set) → (A → Set) → Set
(P ⊆ Q) = ∀ a → (P a) → (Q a)

_⊗_ : ∀ {A B : Set} → (A → Set) → (B → Set) → ((A × B) → Set)
(P ⊗ Q) (a , b) = (P a) × (Q b)

Comp : ∀ {A : Set} → (A → Set) → (A → Set)
Comp P a = ¬(P a)

Lift : ∀ {A : Set} → (A → Set) → (Maybe A → Set)
Lift P nothing = ⊥
Lift P (just a) = P a

set-theoretic-if : ∀ {S₁ T₁ S₂ T₂} →

  -- This is the "if" part of being a set-theoretic model
  -- though it uses the definition from Frisch's thesis
  -- rather than from the Gentle Introduction. The difference
  -- being the presence of Lift, (written D_Ω in Defn 4.2 of
  -- https://www.cduce.org/papers/frisch_phd.pdf).
  (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)) →
  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂))))

set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , just u) Qtu (S₂t , ¬T₂u) = q (t , just u) Qtu (S₁t , ¬T₁u) where

  S₁t : Language S₁ t
  S₁t with dec-language S₁ t
  S₁t | Left ¬S₁t with p (function-err t) (function-err ¬S₁t)
  S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
  S₁t | Right r = r

  ¬T₁u : ¬(Language T₁ u)
  ¬T₁u T₁u with p (function-ok u) (function-ok T₁u)
  ¬T₁u T₁u | function-ok T₂u = ¬T₂u T₂u

set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _) = q (t , nothing) Qt- (S₁t , λ ()) where

  S₁t : Language S₁ t
  S₁t with dec-language S₁ t
  S₁t | Left ¬S₁t with p (function-err t) (function-err ¬S₁t)
  S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
  S₁t | Right r = r

not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →

  -- We don't quite have that this is a set-theoretic model
  -- it's only true when Language T₁ and ¬Language T₂ t₂ are inhabited
  -- in particular it's not true when T₁ is never, or T₂ is unknown.
  ∀ s₂ t₂ → Language S₂ s₂ → ¬Language T₂ t₂ →

  -- This is the "only if" part of being a set-theoretic model
  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂)))) →
  (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂))

not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = r where

  Q : (Tree × Maybe Tree) → Set
  Q (t , just u) = Either (¬Language S₁ t) (Language T₁ u)
  Q (t , nothing) = ¬Language S₁ t

  q : Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁)))
  q (t , just u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t
  q (t , just u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u
  q (t , nothing) ¬S₁t (S₁t , _) = language-comp t ¬S₁t S₁t

  r : Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)
  r function function = function
  r (function-err s) (function-err ¬S₁s) with dec-language S₂ s
  r (function-err s) (function-err ¬S₁s) | Left ¬S₂s = function-err ¬S₂s
  r (function-err s) (function-err ¬S₁s) | Right S₂s = CONTRADICTION (p Q q (s , nothing) ¬S₁s (S₂s , λ ()))
  r (function-ok t) (function-ok T₁t) with dec-language T₂ t
  r (function-ok t) (function-ok T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , just t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t))
  r (function-ok t) (function-ok T₁t) | Right T₂t = function-ok T₂t

-- A counterexample when the argument type is empty.

set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Lift(Language number))) → Q ⊆ Comp((Language never) ⊗ Comp(Lift(Language string))))
set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p)

set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string)
set-theoretic-counterexample-two = witness
  (function-ok (scalar number)) (function-ok (scalar number))
  (function-ok (scalar-scalar number string (λ ())))

-- At some point we may deal with overloaded function resolution, which should fix this problem...
-- The reason why this is connected to overloaded functions is that currently we have that the type of
-- f(x) is (tgt T) where f:T. Really we should have the type depend on the type of x, that is use (tgt T U),
-- where U is the type of x. In particular (tgt (S => T) (U & V)) should be the same as (tgt ((S&U) => T) V)
-- and tgt(never => T) should be unknown. For example
--
-- tgt((number => string) & (string => bool))(number)
-- is tgt(number => string)(number) & tgt(string => bool)(number)
-- is tgt(number => string)(number) & tgt(string => bool)(number&unknown)
-- is tgt(number => string)(number) & tgt(string&number => bool)(unknown)
-- is tgt(number => string)(number) & tgt(never => bool)(unknown)
-- is string & unknown
-- is string
--
-- there's some discussion of this in the Gentle Introduction paper.

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: TheGreatSageEqualToHeaven/luau

max_forks_repo_name: TheGreatSageEqualToHeaven/luau


text:
module Issue100 where

-- hiding (Nat) goes on the 'open' not on the 'import'.
open import Nat hiding (Nat)

one : Nat.Nat
one = suc zero

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2014-01-08, following Maxime Denes 2014-01-06

-- This file demonstrates then incompatibility of the untyped
-- structural termination ordering with HoTT.

open import Common.Equality

data Empty : Set where

data Box : Set where
  wrap : (Empty → Box) → Box

-- Box is inhabited:

gift : Empty → Box
gift ()

box : Box
box = wrap gift

-- wrap has an inverse:

unwrap : Box → (Empty → Box)
unwrap (wrap f) = f

-- Thus, Box is isomorphic to (Empty → Box).
-- However, they cannot be propositionally equal,
-- as this leads to an inconsistency as follows:

postulate iso : (Empty → Box) ≡ Box

module Rewrite where

  loop : Box → Empty
  loop (wrap x) rewrite iso = loop x

-- rewrite is not to blame, we can do it with with:

module With where

  loop : Box → Empty
  loop (wrap x) with (Empty → Box) | iso
  ... | ._ | refl = loop x

-- with is not to be blamed either, we can desugar it:

module Aux where
 mutual
  loop : Box → Empty
  loop (wrap x) = loop' (Empty → Box) iso x

  loop' : ∀ A → A ≡ Box → A → Empty
  loop' .Box refl x = loop x

open Aux

bug : Empty
bug = loop box

-- Moral of the story: the termination checker should reject `loop'.

-- If the termination checker should be fixed in that way,
-- move this test case to test/fail.


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

module _ where

module M where
  data D : Set where

record R₁ : Set where
  field
    x : let module M′ = M in M′.D

variable
  A : Set

record R₂ (A : Set) : Set where

_ : (r : R₂ A) → let open R₂ r in Set₁
_ = λ _ → Set


text:
------------------------------------------------------------------------
-- Properties relating All to various list functions
------------------------------------------------------------------------

module Data.List.All.Properties where

open import Data.Bool
open import Data.Bool.Properties
open import Data.Function
open import Data.List as List
import Data.List.Any as Any
open Any.Membership-≡
open import Data.List.All as All using (All; []; _∷_)
open import Data.Product
open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)

-- Functions can be shifted between the predicate and the list.

All-map : ∀ {A B} {P : Pred B} {f : A → B} {xs} →
          All (P ∘₀ f) xs → All P (List.map f xs)
All-map []       = []
All-map (p ∷ ps) = p ∷ All-map ps

map-All : ∀ {A B} {P : Pred B} {f : A → B} {xs} →
          All P (List.map f xs) → All (P ∘₀ f) xs
map-All {xs = []}    []       = []
map-All {xs = _ ∷ _} (p ∷ ps) = p ∷ map-All ps

-- A variant of All.map.

gmap : ∀ {A B} {P : A → Set} {Q : B → Set} {f : A → B} →
       P ⋐ Q ∘₀ f → All P ⋐ All Q ∘₀ List.map f
gmap g = All-map ∘ All.map g

-- All and all are related via T.

All-all : ∀ {A} (p : A → Bool) {xs} →
          All (T ∘₀ p) xs → T (all p xs)
All-all p []         = _
All-all p (px ∷ pxs) = proj₂ T-∧ (px , All-all p pxs)

all-All : ∀ {A} (p : A → Bool) xs →
          T (all p xs) → All (T ∘₀ p) xs
all-All p []       _     = []
all-All p (x ∷ xs) px∷xs with proj₁ (T-∧ {p x}) px∷xs
all-All p (x ∷ xs) px∷xs | (px , pxs) = px ∷ all-All p xs pxs

-- All is anti-monotone.

anti-mono : ∀ {A} {P : Pred A} {xs ys} → xs ⊆ ys → All P ys → All P xs
anti-mono xs⊆ys pys = All.tabulate (All.lookup pys ∘ xs⊆ys)

-- all is anti-monotone.

all-anti-mono : ∀ {A} (p : A → Bool) {xs ys} →
                xs ⊆ ys → T (all p ys) → T (all p xs)
all-anti-mono p xs⊆ys = All-all p ∘ anti-mono xs⊆ys ∘ all-All p _

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module _ where

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

module Vars (A : Set) where
  variable
    x : A

data It {A : Set} : A → Set where
  it : ∀ x → It x

module Fixed where
  open Vars Nat
  ret : It x
  ret {x = x} = it x

module Param (A : Set) where
  open Vars A
  ret : It x
  ret {x = x} = it x

open Vars Nat

check : Param.ret Nat ≡ Fixed.ret {x = x}
check = refl

-- Check that you can let open as long as you don't use the variables
foo : (A : Set) (let open Vars A) (x : A) → x ≡ x
foo A x = refl


text:
------------------------------------------------------------------------
-- Embeddings with erased "proofs"
------------------------------------------------------------------------

-- Partially following the HoTT book.

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

open import Equality

module Embedding.Erased
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude hiding (id; _∘_)

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Embedding eq as Emb using (Is-embedding; Embedding)
open import Equivalence eq as Eq using (_≃_)
open import Equivalence.Erased eq as EEq
  using (_≃ᴱ_; Is-equivalenceᴱ)
open import Equivalence.Erased.Contractible-preimages eq as ECP
  using (_⁻¹ᴱ_)
open import Erased.Level-1 eq using (Erased; []-cong-axiomatisation)
open import Function-universe eq hiding (id; _∘_; equivalence)
open import H-level.Closure eq
open import Preimage eq using (_⁻¹_)

private
  variable
    a b ℓ t : Level
    A B C   : Type a
    f k x y : A

------------------------------------------------------------------------
-- Embeddings

-- The property of being an embedding with erased "proofs".

Is-embeddingᴱ : {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Is-embeddingᴱ f = ∀ x y → Is-equivalenceᴱ (cong {x = x} {y = y} f)

-- Is-embeddingᴱ is propositional in erased contexts (assuming
-- extensionality).

@0 Is-embeddingᴱ-propositional :
  {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-proposition (Is-embeddingᴱ f)
Is-embeddingᴱ-propositional {b = b} ext =
  Π-closure (lower-extensionality b lzero ext) 1 λ _ →
  Π-closure (lower-extensionality b lzero ext) 1 λ _ →
  EEq.Is-equivalenceᴱ-propositional ext _

-- Embeddings with erased proofs.

record Embeddingᴱ (From : Type f) (To : Type t) : Type (f ⊔ t) where
  field
    to           : From → To
    is-embedding : Is-embeddingᴱ to

  equivalence : (x ≡ y) ≃ᴱ (to x ≡ to y)
  equivalence = EEq.⟨ _ , is-embedding _ _ ⟩

------------------------------------------------------------------------
-- Some conversion functions

-- The type family above could have been defined using Σ.

Embeddingᴱ-as-Σ : Embeddingᴱ A B ↔ ∃ λ (f : A → B) → Is-embeddingᴱ f
Embeddingᴱ-as-Σ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ emb → Embeddingᴱ.to emb , Embeddingᴱ.is-embedding emb
      ; from = λ { (f , is) → record { to = f; is-embedding = is } }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Conversions between Is-embedding and Is-embeddingᴱ.

Is-embedding→Is-embeddingᴱ : Is-embedding f → Is-embeddingᴱ f
Is-embedding→Is-embeddingᴱ {f = f} =
  (∀ x y → Eq.Is-equivalence (cong {x = x} {y = y} f))  ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → EEq.Is-equivalence→Is-equivalenceᴱ) ⟩□
  (∀ x y → Is-equivalenceᴱ (cong {x = x} {y = y} f))    □

@0 Is-embedding≃Is-embeddingᴱ :
  {A : Type a} {B : Type b} {f : A → B} →
  Is-embedding f ↝[ a ∣ a ⊔ b ] Is-embeddingᴱ f
Is-embedding≃Is-embeddingᴱ {f = f} {k = k} ext =
  (∀ x y → Eq.Is-equivalence (cong {x = x} {y = y} f))  ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → from-equivalence
                                                            EEq.Is-equivalence≃Is-equivalenceᴱ) ⟩□
  (∀ x y → Is-equivalenceᴱ (cong {x = x} {y = y} f))    □

@0 Is-embeddingᴱ→Is-embedding : Is-embeddingᴱ f → Is-embedding f
Is-embeddingᴱ→Is-embedding = inverse-ext? Is-embedding≃Is-embeddingᴱ _

-- Conversions between Embedding and Embeddingᴱ.

Embedding→Embeddingᴱ : Embedding A B → Embeddingᴱ A B
Embedding→Embeddingᴱ {A = A} {B = B} =
  Embedding A B                        ↔⟨ Emb.Embedding-as-Σ ⟩
  (∃ λ (f : A → B) → Is-embedding f)   ↝⟨ (∃-cong λ _ → Is-embedding→Is-embeddingᴱ) ⟩
  (∃ λ (f : A → B) → Is-embeddingᴱ f)  ↔⟨ inverse Embeddingᴱ-as-Σ ⟩□
  Embeddingᴱ A B                       □

@0 Embedding≃Embeddingᴱ :
  {A : Type a} {B : Type b} →
  Embedding A B ↝[ a ∣ a ⊔ b ] Embeddingᴱ A B
Embedding≃Embeddingᴱ {A = A} {B = B} ext =
  Embedding A B                        ↔⟨ Emb.Embedding-as-Σ ⟩
  (∃ λ (f : A → B) → Is-embedding f)   ↝⟨ (∃-cong λ _ → Is-embedding≃Is-embeddingᴱ ext) ⟩
  (∃ λ (f : A → B) → Is-embeddingᴱ f)  ↔⟨ inverse Embeddingᴱ-as-Σ ⟩□
  Embeddingᴱ A B                       □

@0 Embeddingᴱ→Embedding : Embeddingᴱ A B → Embedding A B
Embeddingᴱ→Embedding = inverse-ext? Embedding≃Embeddingᴱ _

-- Data corresponding to the erased proofs of an embedding with
-- erased proofs.

Erased-proofs :
  {A : Type a} {B : Type b} →
  (to : A → B) →
  (∀ {x y} → to x ≡ to y → x ≡ y) →
  Type (a ⊔ b)
Erased-proofs to from =
  ∀ {x y} → EEq.Erased-proofs (cong {x = x} {y = y} to) from

-- Extracts "erased proofs" from a regular embedding.

[proofs] :
  (A↝B : Embedding A B) →
  Erased-proofs
    (Embedding.to A↝B)
    (_≃_.from (Embedding.equivalence A↝B))
[proofs] A↝B = EEq.[proofs] (Embedding.equivalence A↝B)

-- Converts two functions and some erased proofs to an embedding with
-- erased proofs.
--
-- Note that Agda can in many cases infer "to" and "from" from the
-- first explicit argument, see (for instance) _∘_ below.

[Embedding]→Embeddingᴱ :
  {to : A → B} {from : ∀ {x y} → to x ≡ to y → x ≡ y} →
  @0 Erased-proofs to from →
  Embeddingᴱ A B
[Embedding]→Embeddingᴱ {to = to} {from = from} ep = record
  { to           = to
  ; is-embedding = λ _ _ → _≃ᴱ_.is-equivalence (EEq.[≃]→≃ᴱ ep)
  }

------------------------------------------------------------------------
-- Preorder

-- Embeddingᴱ is a preorder.

id : Embeddingᴱ A A
id = Embedding→Embeddingᴱ Emb.id

infixr 9 _∘_

_∘_ : Embeddingᴱ B C → Embeddingᴱ A B → Embeddingᴱ A C
f ∘ g =
  [Embedding]→Embeddingᴱ
    ([proofs] (Embeddingᴱ→Embedding f Emb.∘ Embeddingᴱ→Embedding g))

------------------------------------------------------------------------
-- "Preimages"

-- If f is an embedding (with erased proofs), then f ⁻¹ᴱ y is
-- propositional (in an erased context).
--
-- This result is based on the proof of Theorem 4.6.3 in the HoTT book
-- (first edition).

@0 embedding→⁻¹ᴱ-propositional :
  Is-embeddingᴱ f →
  ∀ y → Is-proposition (f ⁻¹ᴱ y)
embedding→⁻¹ᴱ-propositional {f = f} =
  Is-embeddingᴱ f                   ↝⟨ Is-embeddingᴱ→Is-embedding ⟩
  Is-embedding f                    ↝⟨ Emb.embedding→⁻¹-propositional ⟩
  (∀ y → Is-proposition (f ⁻¹ y))   ↝⟨ (∀-cong _ λ _ → H-level-cong _ 1 ECP.⁻¹≃⁻¹ᴱ) ⟩□
  (∀ y → Is-proposition (f ⁻¹ᴱ y))  □

------------------------------------------------------------------------
-- Results that depend on an axiomatisation of []-cong (for a single
-- universe level)

module []-cong₁ (ax : []-cong-axiomatisation ℓ) where

  ----------------------------------------------------------------------
  -- More conversion functions

  -- Equivalences (with erased proofs) from Erased A to B are
  -- embeddings (with erased proofs).

  Is-equivalenceᴱ→Is-embeddingᴱ-Erased :
    {A : Type ℓ} {f : Erased A → B} →
    Is-equivalenceᴱ f → Is-embeddingᴱ f
  Is-equivalenceᴱ→Is-embeddingᴱ-Erased eq _ _ =
    _≃ᴱ_.is-equivalence $ inverse $
      EEq.[]-cong₁.to≡to≃ᴱ≡-Erased ax EEq.⟨ _ , eq ⟩

  -- Equivalences with erased proofs between Erased A and B can be
  -- converted to embeddings with erased proofs.

  Erased≃→Embedding :
    {A : Type ℓ} →
    Erased A ≃ᴱ B → Embeddingᴱ (Erased A) B
  Erased≃→Embedding EEq.⟨ f , is-equiv ⟩ = record
    { to           = f
    ; is-embedding = Is-equivalenceᴱ→Is-embeddingᴱ-Erased is-equiv
    }

------------------------------------------------------------------------
-- Results that depend on an axiomatisation of []-cong (for all
-- universe levels)

module []-cong (ax : ∀ {ℓ} → []-cong-axiomatisation ℓ) where

  private
    open module BC₁ {ℓ} =
      []-cong₁ (ax {ℓ = ℓ})
      public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Closure of a unary relation with respect to a preorder
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Unary.Closure.Preorder {a r e} (P : Preorder a e r) where

open Preorder P
open import Relation.Unary using (Pred)

-- Specialising the results proven generically in `Base`.
import Relation.Unary.Closure.Base _∼_ as Base
open Base public using (□; map; Closed)

module _ {t} {T : Pred Carrier t} where

  reindex : ∀ {x y} → x ∼ y → □ T x → □ T y
  reindex = Base.reindex trans

  extract : ∀ {x} → □ T x → T x
  extract = Base.extract refl

  duplicate : ∀ {x} → □ T x → □ (□ T) x
  duplicate = Base.duplicate trans

□-closed : ∀ {t} {T : Pred Carrier t} → Closed (□ T)
□-closed = Base.□-closed trans


text:
-- Module shadowing using generated modules for records and datatypes
module Issue260d where

data D : Set where
module D where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module PLRTree.Complete.Properties {A : Set} where

open import Data.Empty
open import Data.Sum renaming (_⊎_ to _∨_)
open import PLRTree {A}
open import PLRTree.Complete {A}
open import PLRTree.Equality {A}
open import PLRTree.Equality.Properties {A}

lemma-⋗-≃ : {t t' t'' : PLRTree} → t ⋗ t' → t' ≃ t'' → t ⋗ t''
lemma-⋗-≃ (⋗lf x) ≃lf = ⋗lf x
lemma-⋗-≃ (⋗nd x x' l≃r l'≃r' l⋗l') (≃nd .x' x'' _ l''≃r'' l'≃l'') = ⋗nd x x'' l≃r l''≃r'' (lemma-⋗-≃ l⋗l' l'≃l'')

lemma-≃-⋗ : {t t' t'' : PLRTree} → t ≃ t' → t ⋗ t'' → t' ⋗ t''
lemma-≃-⋗ ≃lf t⋗t'' = t⋗t''
lemma-≃-⋗ (≃nd x x' ≃lf ≃lf ≃lf) (⋗lf .x) = ⋗lf x'
lemma-≃-⋗ (≃nd x _ ≃lf (≃nd _ _ _ _ _) ()) (⋗lf .x)
lemma-≃-⋗ (≃nd x x' l≃r l'≃r' l≃l') (⋗nd .x x'' _ l''≃r'' l⋗l'') = ⋗nd x' x'' l'≃r' l''≃r'' (lemma-≃-⋗ l≃l' l⋗l'')

lemma-⋗* : {t t' t'' : PLRTree} → t ⋗ t' → t ⋗ t'' → t' ≃ t''
lemma-⋗* (⋗lf x) (⋗lf .x) = ≃lf
lemma-⋗* (⋗lf x) (⋗nd .x _ _ _ ())
lemma-⋗* (⋗nd x  _ _ _ ()) (⋗lf .x)
lemma-⋗* (⋗nd x x' l≃r l'≃r' l⋗l') (⋗nd .x x'' _ l''≃r'' l'⋗l'') = ≃nd x' x'' l'≃r' l''≃r'' (lemma-⋗* l⋗l' l'⋗l'')

lemma-*⋗ : {t t' t'' : PLRTree} → t ⋗ t' → t'' ⋗ t' → t ≃ t''
lemma-*⋗ (⋗lf x) (⋗lf y) = ≃nd x y ≃lf ≃lf ≃lf
lemma-*⋗ (⋗nd x x' l≃r l'≃r' l⋗l') (⋗nd x'' .x' l''≃r'' _ l''⋗l') = ≃nd x x'' l≃r l''≃r'' (lemma-*⋗ l⋗l' l''⋗l')

lemma-⋗refl-⊥ : {t : PLRTree} → t ⋗ t → ⊥
lemma-⋗refl-⊥ (⋗nd x .x _ _ t⋗t)
    with lemma-⋗refl-⊥ t⋗t
... | ()

lemma-⋙-⋗ : {t t' t'' : PLRTree} → t ⋙ t' → t ⋗ t'' → t' ⋘ t'' ∨ t' ≃ t''
lemma-⋙-⋗ (⋙p (⋗lf x)) (⋗lf .x) = inj₂ ≃lf
lemma-⋙-⋗ (⋙p (⋗nd x _ _ _ ())) (⋗lf .x)
lemma-⋙-⋗ (⋙p (⋗lf x)) (⋗nd .x _ _ _ ())
lemma-⋙-⋗ (⋙p (⋗nd x x' l≃r l'≃r' l⋗l')) (⋗nd .x x'' _ l''≃r'' l⋗l'') = inj₂ (≃nd x' x'' l'≃r' l''≃r'' (lemma-⋗* l⋗l' l⋗l''))
lemma-⋙-⋗ (⋙l x _ _ _ ()) (⋗lf .x)
lemma-⋙-⋗ (⋙l x x' l≃r l'⋘r' l⋗r') (⋗nd .x x'' _ l''≃r'' l⋗l'') = inj₁ (l⋘ x' x'' l'⋘r' l''≃r'' (lemma-⋗* l⋗r' l⋗l''))
lemma-⋙-⋗ (⋙r x x' ≃lf (⋙p ()) ≃lf) (⋗lf .x)
lemma-⋙-⋗ (⋙r x x' ≃lf (⋙l _ _ _ _ _) ()) (⋗lf .x)
lemma-⋙-⋗ (⋙r x x' ≃lf (⋙r _ _ _ _ _) ()) (⋗lf .x)
lemma-⋙-⋗ (⋙r x x' l≃r l'⋙r' l≃l') (⋗nd .x x'' _ l''≃r'' l⋗l'') = inj₁ (r⋘ x' x'' l'⋙r' l''≃r'' (lemma-≃-⋗ l≃l' l⋗l''))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Gentzen-style formalisation of syntax with context pairs, after Pfenning-Davies.
-- Normal forms, neutrals, and spines.

module BasicIS4.Syntax.DyadicGentzenSpinalNormalForm where

open import BasicIS4.Syntax.DyadicGentzen public

-- Commuting propositions for neutrals.

data Tyⁿᵉ : Ty → Set where
  α_ : (P : Atom) → Tyⁿᵉ (α P)
  □_ : (A : Ty) → Tyⁿᵉ (□ A)

-- Derivations.

mutual
  -- Normal forms, or introductions.
  infix 3 _⊢ⁿᶠ_
  data _⊢ⁿᶠ_ : Cx² Ty Ty → Ty → Set where
    neⁿᶠ   : ∀ {A Γ Δ}   → Γ ⁏ Δ ⊢ⁿᵉ A → {{_ : Tyⁿᵉ A}} → Γ ⁏ Δ ⊢ⁿᶠ A
    lamⁿᶠ  : ∀ {A B Γ Δ} → Γ , A ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ▻ B
    boxⁿᶠ  : ∀ {A Γ Δ}   → ∅ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ □ A
    pairⁿᶠ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ∧ B
    unitⁿᶠ : ∀ {Γ Δ}     → Γ ⁏ Δ ⊢ⁿᶠ ⊤

  -- Neutrals, or eliminations.
  infix 3 _⊢ⁿᵉ_
  data _⊢ⁿᵉ_ : Cx² Ty Ty → Ty → Set where
    spⁿᵉ  : ∀ {A B C Γ Δ} → A ∈ Γ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ⁿᵉ C
    mspⁿᵉ : ∀ {A B C Γ Δ} → A ∈ Δ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ⁿᵉ C

  -- Spines.
  infix 3 _⊢ˢᵖ_⦙_
  data _⊢ˢᵖ_⦙_ : Cx² Ty Ty → Ty → Ty → Set where
    nilˢᵖ : ∀ {C Γ Δ} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ C
    appˢᵖ : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ A ▻ B ⦙ C
    fstˢᵖ : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ ⊢ˢᵖ A ∧ B ⦙ C
    sndˢᵖ : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢᵖ A ∧ B ⦙ C

  -- Spine tips.
  infix 3 _⊢ᵗᵖ_⦙_
  data _⊢ᵗᵖ_⦙_ : Cx² Ty Ty → Ty → Ty → Set where
    nilᵗᵖ   : ∀ {C Γ Δ} → Γ ⁏ Δ ⊢ᵗᵖ C ⦙ C
    unboxᵗᵖ : ∀ {A C Γ Δ} → Γ ⁏ Δ , A ⊢ⁿᶠ C → Γ ⁏ Δ ⊢ᵗᵖ □ A ⦙ C

-- Translation to simple terms.

mutual
  nf→tm : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ A
  nf→tm (neⁿᶠ t)     = ne→tm t
  nf→tm (lamⁿᶠ t)    = lam (nf→tm t)
  nf→tm (boxⁿᶠ t)    = box (nf→tm t)
  nf→tm (pairⁿᶠ t u) = pair (nf→tm t) (nf→tm u)
  nf→tm unitⁿᶠ       = unit

  ne→tm : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ A
  ne→tm (spⁿᵉ i xs y)  = tp→tm (var i) xs y
  ne→tm (mspⁿᵉ i xs y) = tp→tm (mvar i) xs y

  sp→tm : ∀ {A C Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ ⊢ C
  sp→tm t nilˢᵖ        = t
  sp→tm t (appˢᵖ xs u) = sp→tm (app t (nf→tm u)) xs
  sp→tm t (fstˢᵖ xs)   = sp→tm (fst t) xs
  sp→tm t (sndˢᵖ xs)   = sp→tm (snd t) xs

  tp→tm : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ C
  tp→tm t xs nilᵗᵖ       = sp→tm t xs
  tp→tm t xs (unboxᵗᵖ u) = unbox (sp→tm t xs) (nf→tm u)

-- Monotonicity with respect to context inclusion.

mutual
  mono⊢ⁿᶠ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ⁿᶠ A → Γ′ ⁏ Δ ⊢ⁿᶠ A
  mono⊢ⁿᶠ η (neⁿᶠ t)     = neⁿᶠ (mono⊢ⁿᵉ η t)
  mono⊢ⁿᶠ η (lamⁿᶠ t)    = lamⁿᶠ (mono⊢ⁿᶠ (keep η) t)
  mono⊢ⁿᶠ η (boxⁿᶠ t)    = boxⁿᶠ t
  mono⊢ⁿᶠ η (pairⁿᶠ t u) = pairⁿᶠ (mono⊢ⁿᶠ η t) (mono⊢ⁿᶠ η u)
  mono⊢ⁿᶠ η unitⁿᶠ       = unitⁿᶠ

  mono⊢ⁿᵉ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ⁿᵉ A → Γ′ ⁏ Δ ⊢ⁿᵉ A
  mono⊢ⁿᵉ η (spⁿᵉ i xs y)  = spⁿᵉ (mono∈ η i) (mono⊢ˢᵖ η xs) (mono⊢ᵗᵖ η y)
  mono⊢ⁿᵉ η (mspⁿᵉ i xs y) = mspⁿᵉ i (mono⊢ˢᵖ η xs) (mono⊢ᵗᵖ η y)

  mono⊢ˢᵖ : ∀ {A C Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ′ ⁏ Δ ⊢ˢᵖ A ⦙ C
  mono⊢ˢᵖ η nilˢᵖ        = nilˢᵖ
  mono⊢ˢᵖ η (appˢᵖ xs u) = appˢᵖ (mono⊢ˢᵖ η xs) (mono⊢ⁿᶠ η u)
  mono⊢ˢᵖ η (fstˢᵖ xs)   = fstˢᵖ (mono⊢ˢᵖ η xs)
  mono⊢ˢᵖ η (sndˢᵖ xs)   = sndˢᵖ (mono⊢ˢᵖ η xs)

  mono⊢ᵗᵖ : ∀ {A C Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ᵗᵖ A ⦙ C → Γ′ ⁏ Δ ⊢ᵗᵖ A ⦙ C
  mono⊢ᵗᵖ η nilᵗᵖ       = nilᵗᵖ
  mono⊢ᵗᵖ η (unboxᵗᵖ u) = unboxᵗᵖ (mono⊢ⁿᶠ η u)

-- Monotonicity with respect to modal context inclusion.

mutual
  mmono⊢ⁿᶠ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ′ ⊢ⁿᶠ A
  mmono⊢ⁿᶠ θ (neⁿᶠ t)     = neⁿᶠ (mmono⊢ⁿᵉ θ t)
  mmono⊢ⁿᶠ θ (lamⁿᶠ t)    = lamⁿᶠ (mmono⊢ⁿᶠ θ t)
  mmono⊢ⁿᶠ θ (boxⁿᶠ t)    = boxⁿᶠ (mmono⊢ⁿᶠ θ t)
  mmono⊢ⁿᶠ θ (pairⁿᶠ t u) = pairⁿᶠ (mmono⊢ⁿᶠ θ t) (mmono⊢ⁿᶠ θ u)
  mmono⊢ⁿᶠ θ unitⁿᶠ       = unitⁿᶠ

  mmono⊢ⁿᵉ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ′ ⊢ⁿᵉ A
  mmono⊢ⁿᵉ θ (spⁿᵉ i xs y)  = spⁿᵉ i (mmono⊢ˢᵖ θ xs) (mmono⊢ᵗᵖ θ y)
  mmono⊢ⁿᵉ θ (mspⁿᵉ i xs y) = mspⁿᵉ (mono∈ θ i) (mmono⊢ˢᵖ θ xs) (mmono⊢ᵗᵖ θ y)

  mmono⊢ˢᵖ : ∀ {A C Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ′ ⊢ˢᵖ A ⦙ C
  mmono⊢ˢᵖ θ nilˢᵖ        = nilˢᵖ
  mmono⊢ˢᵖ θ (appˢᵖ xs u) = appˢᵖ (mmono⊢ˢᵖ θ xs) (mmono⊢ⁿᶠ θ u)
  mmono⊢ˢᵖ θ (fstˢᵖ xs)   = fstˢᵖ (mmono⊢ˢᵖ θ xs)
  mmono⊢ˢᵖ θ (sndˢᵖ xs)   = sndˢᵖ (mmono⊢ˢᵖ θ xs)

  mmono⊢ᵗᵖ : ∀ {A C Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ᵗᵖ A ⦙ C → Γ ⁏ Δ′ ⊢ᵗᵖ A ⦙ C
  mmono⊢ᵗᵖ θ nilᵗᵖ       = nilᵗᵖ
  mmono⊢ᵗᵖ θ (unboxᵗᵖ u) = unboxᵗᵖ (mmono⊢ⁿᶠ (keep θ) u)

-- Monotonicity using context pairs.

mono²⊢ⁿᶠ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ⁿᶠ A → Π′ ⊢ⁿᶠ A
mono²⊢ⁿᶠ (η , θ) = mono⊢ⁿᶠ η ∘ mmono⊢ⁿᶠ θ

mono²⊢ⁿᵉ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ⁿᵉ A → Π′ ⊢ⁿᵉ A
mono²⊢ⁿᵉ (η , θ) = mono⊢ⁿᵉ η ∘ mmono⊢ⁿᵉ θ

mono²⊢ˢᵖ : ∀ {A C Π Π′} → Π ⊆² Π′ → Π ⊢ˢᵖ A ⦙ C → Π′ ⊢ˢᵖ A ⦙ C
mono²⊢ˢᵖ (η , θ) = mono⊢ˢᵖ η ∘ mmono⊢ˢᵖ θ

mono²⊢ᵗᵖ : ∀ {A C Π Π′} → Π ⊆² Π′ → Π ⊢ᵗᵖ A ⦙ C → Π′ ⊢ᵗᵖ A ⦙ C
mono²⊢ᵗᵖ (η , θ) = mono⊢ᵗᵖ η ∘ mmono⊢ᵗᵖ θ

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Common.Context  where

import Level
open import Data.Nat as Nat
open import Data.List as List
import Level
open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open import Relation.Binary -- using (Setoid; Rel; IsEquivalence)
open ≡-Reasoning
open import Function as Fun hiding (_∘′_)
open import Data.Sum as Sum hiding ([_,_])
open import Categories.Category using (Category)

open import Common.SumProperties

-------------------------
---- Type contexts

Ctx : Set → Set
Ctx Ty = List Ty

-- | De Bruijn variable indexing
data Var {Ty : Set} : (Γ : Ctx Ty) (a : Ty) → Set where
  zero : ∀{Γ a}                          → Var (a ∷ Γ) a
  succ : ∀{Γ b} (a : Ty) → (x : Var Γ a) → Var (b ∷ Γ) a

data _≅V_ {Ty} : ∀ {Γ Γ' : Ctx Ty} {a a' : Ty} → Var Γ a → Var Γ' a' → Set where
  zero : ∀ {Γ Γ'} {a a'}
         → zero {Γ = Γ} {a} ≅V zero {Γ = Γ'} {a'}

  succ  : ∀ {Γ Γ'} {a a'}
          → ∀ {x : Var Γ a} {x' : Var Γ' a'} {b b' : Ty}
          → x ≅V x'
          → succ {b = b} a x ≅V succ {b = b'} a' x'

Vrefl : ∀ {Ty} {Γ} {a : Ty} {x : Var Γ a} → x ≅V x
Vrefl {x = zero}  = zero
Vrefl {x = succ _ t} = succ Vrefl

Vsym : ∀ {Ty} {Γ Γ'} {a a' : Ty} {x : Var Γ a} {x' : Var Γ' a'}
       → x ≅V x' → x' ≅V x
Vsym zero      = zero
Vsym {Ty} (succ [x]) = succ (Vsym [x])

Vtrans : ∀ {Ty} {Γ Γ' Γ''} {a a' a'' : Ty}
           {x : Var Γ a} {x' : Var Γ' a'} {x'' : Var Γ'' a''}
         → x ≅V x' → x' ≅V x'' → x ≅V x''
Vtrans zero     zero      = zero
Vtrans (succ eq) (succ eq') = succ (Vtrans eq eq')

-- Note: makes the equality homogeneous in Γ and a
≅V-setoid : ∀ {Ty} {Γ} {a : Ty} → Setoid _ _
≅V-setoid {Ty} {Γ} {a} = record
  { Carrier = Var Γ a
  ; _≈_ = _≅V_
  ; isEquivalence = record
    { refl = Vrefl ; sym = Vsym ; trans = Vtrans }
  }

arr : ∀ {Ty} → (Γ Δ : Ctx Ty) → Set
arr {Ty} Γ Δ = ∀ (a : Ty) → Var Γ a → Var Δ a

_►_ = arr
-- _▹_ = arr

infix 4 _≡C_

record _≡C_ {Ty} {Γ Δ : Ctx Ty} (ρ : arr Γ Δ) (γ : arr Γ Δ) : Set where
  field
    ≡C-proof : ∀ {a} {x} → ρ a x ≡ γ a x
open _≡C_

_≈_ = _≡C_

Crefl : ∀ {Ty} {Γ Δ : Ctx Ty} → Reflexive (_≡C_ {Γ = Γ} {Δ})
Crefl = record { ≡C-proof = PE.refl }
Csym : ∀ {Ty} {Γ Δ : Ctx Ty} → Symmetric (_≡C_ {Γ = Γ} {Δ})
Csym p = record { ≡C-proof = PE.sym (≡C-proof p) }
Ctrans : ∀ {Ty} {Γ Δ : Ctx Ty} → Transitive (_≡C_ {Γ = Γ} {Δ})
Ctrans p₁ p₂ = record { ≡C-proof = PE.trans (≡C-proof p₁) (≡C-proof p₂) }

≡C-equiv : ∀ {Ty} {Γ Δ : Ctx Ty} → IsEquivalence (_≡C_ {Γ = Γ} {Δ})
≡C-equiv =
  record
  { refl = Crefl
  ; sym = Csym
  ; trans = Ctrans
  }

≡C-setoid : ∀ {Ty} {Γ Δ : Ctx Ty} → Setoid _ _
≡C-setoid {_} {Γ} {Δ} = record
  { Carrier = arr Γ Δ
  ; _≈_ = _≡C_
  ; isEquivalence = ≡C-equiv
  }

_∘′_ : ∀ {Ty} {Γ Δ Ξ : Ctx Ty} (ρ : Δ ► Ξ) (γ : Γ ► Δ) → Γ ► Ξ
_∘′_ ρ γ = λ a x → ρ a (γ a x)

_●_ = _∘′_

ctx-id : ∀ {Ty} {Γ : Ctx Ty} →  arr Γ Γ
ctx-id = λ _ x → x

comp-resp-≡C : ∀ {Ty} {Γ Δ Ξ : Ctx Ty} {ρ ρ' : arr Δ Ξ} {γ γ' : arr Γ Δ} →
               ρ ≡C ρ' → γ ≡C γ' → ρ ∘′ γ ≡C ρ' ∘′ γ'
comp-resp-≡C {_} {Γ} {Δ} {Ξ} {ρ} {ρ'} {γ} {γ'} ρ≡ρ' γ≡γ'
  = record { ≡C-proof = p }
  where
    p : ∀ {a} {x} → (ρ ∘′ γ) a x ≡ (ρ' ∘′ γ') a x
    p {a} {x} =
      begin
        (ρ ∘′ γ) a x
      ≡⟨ refl ⟩
        ρ a (γ a x)
      ≡⟨ cong (λ u → ρ a u) (≡C-proof γ≡γ') ⟩
        ρ a (γ' a x)
      ≡⟨ ≡C-proof ρ≡ρ' ⟩
        ρ' a (γ' a x)
      ≡⟨ refl ⟩
        (ρ' ∘′ γ') a x
      ∎

-- | Contexts form a category
ctx-cat : Set → Category Level.zero Level.zero Level.zero
ctx-cat Ty = record
   { Obj = Ctx Ty
   ; _⇒_ = arr
   ; _≡_ = _≡C_
   ; _∘_ = _∘′_
   ; id = ctx-id
   ; assoc = record { ≡C-proof = refl }
   ; identityˡ = record { ≡C-proof = refl }
   ; identityʳ = record { ≡C-proof = refl }
   ; equiv = ≡C-equiv
   ; ∘-resp-≡ = comp-resp-≡C
   }

-------------------------
---- Coproduct structure on contexts

{-
_⊕_ : Ctx → Ctx → Ctx
Γ₁ ⊕ Γ₂ = Γ₁ ++ Γ₂

in₁ : {Γ₁ Γ₂ : Ctx} → Γ₁ ▹ (Γ₁ ⊕ Γ₂)
in₁ _ zero     = zero
in₁ a (succ .a x) = succ a (in₁ a x)

in₂ : {{Γ₁ Γ₂ : Ctx}} → Γ₂ ▹ (Γ₁ ⊕ Γ₂)
in₂ {{[]}}     _ x = x
in₂ {{b ∷ Γ₁}} a x = succ a (in₂ a x)

split : {Γ₁ Γ₂ : Ctx} {a : Ty} → Var (Γ₁ ⊕ Γ₂) a → Var Γ₁ a ⊎ Var Γ₂ a
split {[]}      {Γ₂}     x        = inj₂ x
split {a ∷ Γ₁'} {Γ₂}     zero     = inj₁ zero
split {b ∷ Γ₁'} {Γ₂} {a} (succ .a y) = (Sum.map (succ a) (ctx-id a)) (split {Γ₁'} y)

[_,_] : {Γ₁ Γ₂ Δ : Ctx} (f : Γ₁ ▹ Δ) (g : Γ₂ ▹ Δ)
      → ((Γ₁ ⊕ Γ₂) ▹ Δ)
[_,_] {Γ} {Γ₂} f g a x = ([ f a , g a ]′) (split x)

_-⊕-_ : {Γ Γ₂ Γ' Γ₂' : Ctx} (f : Γ ▹ Γ') (g : Γ₂ ▹ Γ₂')
      → ((Γ ⊕ Γ₂) ▹ (Γ' ⊕ Γ₂'))
_-⊕-_ {Γ} {Γ₂} {Γ'} {Γ₂'} f g = [ in₁ ● f , in₂ {{Γ'}} {{Γ₂'}} ● g ]

succ-distr-lemma : {Γ : Ctx} {a b : Ty} (Γ₂ : Ctx) (x : Var Γ a) →
                   (in₁ {b ∷ Γ} ● succ {Γ}) a x
                   ≡ (succ {Γ ⊕ Γ₂} ● in₁ {Γ} {Γ₂}) a x
succ-distr-lemma Γ₂ x = refl

split-lemma₁ : {a : Ty} (Γ₁ Γ₂ : Ctx) (x : Var Γ₁ a) →
               split {Γ₁} {Γ₂} (in₁ {Γ₁} a x) ≡ inj₁ x
split-lemma₁ (tt ∷ Γ₁) Γ₂ zero       = refl
split-lemma₁ (tt ∷ Γ₁) Γ₂ (succ a x) =
  begin
    split {tt ∷ Γ₁} (in₁ {tt ∷ Γ₁} a (succ a x))
  ≡⟨ refl ⟩
    (Sum.map (succ a) id) (split (in₁ a x))
  ≡⟨ cong (Sum.map (succ a) id) (split-lemma₁ Γ₁ Γ₂ x) ⟩
    (Sum.map (succ a) id) (inj₁ x)
  ≡⟨ refl ⟩
    inj₁ (succ a x)
  ∎

split-lemma₂ : {a : Ty} (Γ₁ Γ₂ : Ctx) (x : Var Γ₂ a) →
               split {Γ₁} {Γ₂} (in₂ a x) ≡ inj₂ x
split-lemma₂ [] Γ₂ x = refl
split-lemma₂ {a} (tt ∷ Γ₁) Γ₂ x =
  begin
    split {tt ∷ Γ₁} {Γ₂} (in₂ {{tt ∷ Γ₁}} a x)
  ≡⟨ refl ⟩
    Sum.map (succ a) id (split (in₂ {{Γ₁}} a x))
  ≡⟨ cong (λ u → Sum.map (succ a) id u) (split-lemma₂ Γ₁ Γ₂ x) ⟩
    Sum.map (succ a) id (inj₂ x)
  ≡⟨ refl ⟩
    inj₂ x
  ∎

split-lemma : (Γ₁ Γ₂ : Ctx) (a : Ty) (x : Var (Γ₁ ⊕ Γ₂) a) →
             [ in₁ {Γ₁} {Γ₂} a , in₂ a ]′ (split x) ≡ x
split-lemma []       Γ₂ _  x           = refl
split-lemma (a ∷ Γ₁) Γ₂ .a zero        = refl
split-lemma (b ∷ Γ₁) Γ₂ a  (succ .a x) =
  begin
    [ in₁ {b ∷ Γ₁} a , in₂ {{b ∷ Γ₁}} a ]′ (split (succ a x))
  ≡⟨ refl ⟩
    [ in₁ {b ∷ Γ₁} a , (succ {Γ₁ ⊕ Γ₂} ● in₂ {{Γ₁}} ) a ]′
      (Sum.map (succ {Γ₁} a) id (split x))
  ≡⟨ copair-sum-map-merge {f₁ = Var.succ {Γ₁} {b} a} (split x) ⟩
    [ (in₁ {b ∷ Γ₁} ● succ {Γ₁}) a , (succ {Γ₁ ⊕ Γ₂} ● in₂) a ]′ (split x)
  ≡⟨ copair-cong {f = (in₁ {b ∷ Γ₁} ● succ {Γ₁}) a}
                 (succ-distr-lemma Γ₂)
                 (split x) ⟩
    [ (succ {Γ₁ ⊕ Γ₂} ● in₁ {Γ₁}) a , (succ {Γ₁ ⊕ Γ₂} ● in₂) a ]′ (split x)
  ≡⟨ copair-distr {f = in₁ {Γ₁} {Γ₂} a} {h = succ {Γ₁ ⊕ Γ₂} a} (split x)⟩
    (Var.succ {Γ₁ ⊕ Γ₂} {b} a ∘ [ in₁ {Γ₁} a , in₂ a ]′) (split x)
  ≡⟨ cong (succ {Γ₁ ⊕ Γ₂} {b} a) (split-lemma Γ₁ Γ₂ a x) ⟩
     succ {Γ₁ ⊕ Γ₂} a x
  ∎

⊕-is-coprod-arg : ∀{Γ₁ Γ₂ : Ctx} (a : Ty) (x : Var (Γ₁ ⊕ Γ₂) a) →
                  [ in₁ {Γ₁} {Γ₂} , in₂ ] a x ≡ ctx-id a x
⊕-is-coprod-arg {Γ₁} {Γ₂} = split-lemma Γ₁ Γ₂

⊕-is-coprod : ∀{Γ₁ Γ₂ : Ctx} → [ in₁ {Γ₁} {Γ₂} , in₂ ] ≡C ctx-id
⊕-is-coprod {Γ₁} = {!!}
{-
  η-≡ {f₁ = [ in₁ {Γ₁} , in₂ ]}
      {f₂ = ctx-id}
      (λ (a : Ty) →
        η-≡ {f₁ = [ in₁ {Γ₁}, in₂ ] a}
            {f₂ = ctx-id a}
            (⊕-is-coprod-arg {Γ₁} a)
       )
-}

●-distr-copair₁ˡ : ∀{Γ₁ Γ₂ Δ : Ctx}
                   (h : (Γ₁ ⊕ Γ₂) ▹ Δ) (a : Ty) (x : Var (Γ₁ ⊕ Γ₂) a) →
                   [ h ● in₁ {Γ₁} {Γ₂} , h ● in₂ {{Γ₁}} {{Γ₂}} ] a x
                   ≡ (h ● [ in₁ {Γ₁} {Γ₂} , in₂ ]) a x
●-distr-copair₁ˡ {Γ₁} {Γ₂} {Δ} h a x =
  begin
    [ h ● in₁ {Γ₁} , h ● in₂ ] a x
  ≡⟨ refl ⟩
    ([ (h ● in₁ {Γ₁}) a , (h ● in₂) a ]′) (split x)
  ≡⟨ copair-distr {f = in₁ {Γ₁} a} {g = in₂ a} {h = h a} (split x) ⟩
    (h ● [ in₁ {Γ₁} , in₂ ]) a x
  ∎

●-distr-copairˡ : ∀{Γ₁ Γ₂ Δ : Ctx} (h : (Γ₁ ⊕ Γ₂) ▹ Δ) →
                 [ h ● in₁ {Γ₁} {Γ₂} , h ● in₂ {{Γ₁}} {{Γ₂}} ]
                 ≡ h ● [ in₁ {Γ₁} {Γ₂} , in₂ ]
●-distr-copairˡ {Γ₁} h = {!!}
  -- η-≡ (λ a → η-≡ (●-distr-copair₁ˡ {Γ₁} h a))

⊕-is-coprod₁ : ∀{Γ₁ Γ₂ Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ} {h : (Γ₁ ⊕ Γ₂) ▹ Δ} →
               h ● in₁ ≡C f → h ● in₂ ≡C g → [ f , g ] ≡C h
⊕-is-coprod₁ {Γ₁} {Γ₂} {Δ} {f} {g} {h} h●in₁≡f h●in₂≡g
  = record { ≡C-proof = p }
  where
    p : ∀ {a} {x} → [ f , g ] a x ≡ h a x
    p {a} {x} =
      begin
        [ f , g ] a x
      ≡⟨ refl ⟩
        ([ f a , g a ]′) (split x)
      ≡⟨ cong (λ u → [ u , g a ]′ (split x)) {!!} ⟩
        ([ (h ● in₁ {Γ₁}) a , g a ]′) (split x)
      ≡⟨ {!!} ⟩
        h a x
      ∎
{-
        [ h ● in₁ {Γ₁} , g ]
      ≡⟨ cong (λ u → [ h ● in₁ {Γ₁} , u ]) (sym h●in₂≡g) ⟩
        [ h ● in₁ {Γ₁} , h ● in₂ ]
      ≡⟨ ●-distr-copairˡ {Γ₁} h ⟩
        h ● [ in₁ {Γ₁}, in₂ ]
      ≡⟨ cong (λ u → h ● u) (⊕-is-coprod {Γ₁}) ⟩
        h ● ctx-id
      ≡⟨ refl ⟩
        h
  -}

commute-in₁-arg : ∀ {Γ₁ Γ₂ Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ}
                    (a : Ty) (x : Var Γ₁ a) →
                  ([ f , g ] ● in₁) a x ≡ f a x
commute-in₁-arg _ zero = refl
commute-in₁-arg {b ∷ Γ₁} {Γ₂} {Δ} {f} {g} a (succ .a x) =
  begin
    ([ f , g ] ● in₁ {b ∷ Γ₁}) a (succ {Γ₁} a x)
  ≡⟨ refl ⟩
    [ f , g ] a (succ {Γ₁ ⊕ Γ₂} a (in₁ {Γ₁} a x))
  ≡⟨ refl ⟩
    ([ f a , g a ]′) (split (succ {Γ₁ ⊕ Γ₂} a (in₁ {Γ₁} a x)))
  ≡⟨ refl ⟩
    [ f a , g a ]′ ((Sum.map (succ a) id) (split {Γ₁} {Γ₂} (in₁ {Γ₁} a x)))
  ≡⟨ refl ⟩
    (([ f a , g a ]′ ∘ (Sum.map (succ a) id)) (split {Γ₁} {Γ₂} (in₁ {Γ₁} a x)))
  ≡⟨ copair-sum-map-merge {f₁ = succ a} (split {Γ₁} {Γ₂} (in₁ {Γ₁} a x)) ⟩
    ([ (f ● succ) a , g a ]′ (split {Γ₁} {Γ₂} (in₁ {Γ₁} a x)))
  ≡⟨ cong ([ (f ● succ) a , g a ]′) (split-lemma₁ Γ₁ Γ₂ x) ⟩
    f a (succ a x)
  ∎

commute-in₁ : (Γ₁ : Ctx) → (Γ₂ : Ctx) → {Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ}
              → ([ f , g ] ● in₁) ≡C f
commute-in₁ Γ₁ Γ₂ {Δ} {f} {g} =
  record { ≡C-proof = λ {a} {x} → commute-in₁-arg {f = f} {g} a x }

commute-in₂-arg : ∀ {Γ₁ Γ₂ Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ}
                    (a : Ty) (x : Var Γ₂ a) →
                  ([ f , g ] ● in₂) a x ≡ g a x
commute-in₂-arg {[]} _ _ = refl
commute-in₂-arg {tt ∷ Γ₁} {Γ₂} {Δ} {f} {g} a x =
  begin
    ([ f , g ] ● in₂ {{tt ∷ Γ₁}} ) a x
  ≡⟨ refl ⟩
    [ f , g ] a ((succ ● in₂) a x)
  ≡⟨ refl ⟩
    [ f a , g a ]′ (split {tt ∷ Γ₁} (succ a (in₂ a x)))
  ≡⟨ cong (λ u → [ f a , g a ]′ u) {x = split {tt ∷ Γ₁} (succ a (in₂ a x))} refl ⟩
    [ f a , g a ]′ ((Sum.map (succ a) id) (split {Γ₁} (in₂ a x)))
  ≡⟨ cong (λ u → [ f a , g a ]′ (Sum.map (succ a) id u)) (split-lemma₂ Γ₁ Γ₂ x) ⟩
    [ f a , g a ]′ ((Sum.map (succ a) id) (inj₂ x))
  ≡⟨ copair-sum-map-merge {f₁ = succ {Γ₁} a} {f₂ = id} {g₁ = f a} {g₂ = g a} (inj₂ x) ⟩
    [ (f ● succ) a , (g ● ctx-id) a ]′ (inj₂ x)
  ≡⟨ copair-elimʳ {f = (f ● succ) a} {g = (g ● ctx-id) a} x ⟩
    g a x
  ∎

commute-in₂ : (Γ₁ : Ctx) → (Γ₂ : Ctx) → {Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ}
              → ([ f , g ] ● in₂) ≡C g
commute-in₂ Γ₁ Γ₂ {Δ} {f} {g} =
  record { ≡C-proof = λ {a} {x} → commute-in₂-arg {f = f} {g} a x }

open import Categories.Object.Coproduct ctx-cat

ctx-coproduct : ∀{Γ₁ Γ₂ : Ctx} → Coproduct Γ₁ Γ₂
ctx-coproduct {Γ₁} {Γ₂} = record
                  { A+B = Γ₁ ⊕ Γ₂
                  ; i₁ = in₁
                  ; i₂ = in₂
                  ; [_,_] = [_,_]
                  ; commute₁ = commute-in₁ Γ₁ Γ₂
                  ; commute₂ = commute-in₂ Γ₁ Γ₂
                  ; universal = ⊕-is-coprod₁
                  }

open import Categories.Object.BinaryCoproducts ctx-cat

ctx-bin-coproducts : BinaryCoproducts
ctx-bin-coproducts = record { coproduct = ctx-coproduct }

open BinaryCoproducts ctx-bin-coproducts

-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- Andreas, 2017-01-24, issue #2429
-- ..-annotation in lambdas should be taken seriously

-- A ≤ ..A ≤ .A
-- (.A → B) ≤ (..A → B) ≤ A → B

should-fail : ∀{A B : Set} → (.A → B) → (.A → B)
should-fail f = λ ..a → f a

-- Expected error:
-- Found a non-strict lambda where a irrelevant lambda was expected
-- when checking that the expression λ ..a → f a has type ..A → .B

-- Note: Since A and B are not in scope, they are printed as .A and .B
-- This makes this error message super confusing.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{- Name: Bowornmet (Ben) Hudson

--Preorders in Agda!--

-}

open import Preliminaries

module Preorder where

  {- definition: a Preorder on a set A is a binary relation
     that is reflexive and transitive.
  -}
  record Preorder-str (A : Set) : Set1 where
    constructor preorder
    field
      ≤ : A → A → Set
      refl : ∀ x → ≤ x x
      trans : ∀ x y z → ≤ x y → ≤ y z → ≤ x z

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

  -- Task 1: Show that the Natural numbers with ≤ form a preorder

  -- the ≤ relation on Natural numbers
  ≤nat : Nat → Nat → Set
  ≤nat Z Z = Unit
  ≤nat Z (S y) = Unit
  ≤nat (S x) Z = Void
  ≤nat (S x) (S y) = ≤nat x y

  -- proof that Nat is reflexive under ≤
  nat-refl : ∀ (x : Nat) → ≤nat x x
  nat-refl Z = <>
  nat-refl (S x) = nat-refl x

  -- proof that Nat is transitive under ≤
  nat-trans : ∀ (x y z : Nat) → ≤nat x y → ≤nat y z → ≤nat x z
  nat-trans Z Z Z p q = <>
  nat-trans Z Z (S z) p q = <>
  nat-trans Z (S y) Z p q = abort q
  nat-trans Z (S y) (S z) p q = <>
  nat-trans (S x) Z Z () q
  nat-trans (S x) Z (S z) () q
  nat-trans (S x) (S y) Z p ()
  nat-trans (S x) (S y) (S z) p q = nat-trans x y z p q

  -- proof that Nat and ≤ (the ≤ relation defined on the natural numbers) form a preorder
  nat-ispreorder : Preorder-str Nat
  nat-ispreorder = record { ≤ = ≤nat; refl = nat-refl; trans = nat-trans }

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

  -- Task 2: Show that the product of two preorders is a preorder

  {- defining the relation: when is one cartesian product 'less than' another?
     if A and B are preorders and we have cartesian products (a1,b1) and (a2,b2)
     such that a1,a2 ∈ A and b1,b2 ∈ B,
     then (a1,b1)≤(a2,b2) iff a1≤a2 and b1≤b2
  -}
  ≤axb : ∀ {A B : Set} → Preorder-str A → Preorder-str B → (A × B) → (A × B) → Set
  ≤axb PA PB (a1 , b1) (a2 , b2) = Preorder-str.≤ PA a1 a2 × Preorder-str.≤ PB b1 b2

  {-  a cartesian product (a,b) is 'less than' itself
     if each component of the product is reflexive, i.e.
     just show that a is reflexive and b is reflexive
  -}
  axb-refl : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x : (A × B)) →  ≤axb PA PB x x
  axb-refl PA PB (a , b) = Preorder-str.refl PA a , Preorder-str.refl PB b

  -- same idea for transitivity...
  axb-trans : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x y z : (A × B)) → ≤axb PA PB x y → ≤axb PA PB y z → ≤axb PA PB x z
  axb-trans PA PB (a1 , b1) (a2 , b2) (a3 , b3) (a1<a2 , b1<b2) (a2<a3 , b2<b3) =
                          Preorder-str.trans PA a1 a2 a3 a1<a2 a2<a3 , Preorder-str.trans PB b1 b2 b3 b1<b2 b2<b3

  -- proof that AxB is a preorder
  AxB-ispreorder : ∀ (A B : Set) → Preorder-str A → Preorder-str B → Preorder-str (A × B)
  AxB-ispreorder A B pre-a pre-b = record { ≤ = ≤axb pre-a pre-b; refl = axb-refl pre-a pre-b; trans = axb-trans pre-a pre-b }

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

  -- Task 3: Show that the sum of two preorders is a preorder

  ≤a+b : ∀ {A B : Set} → Preorder-str A → Preorder-str B → (Either A B) → (Either A B) → Set
  ≤a+b (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inl a1) (Inl a2) = (a1 ≤a a2)
  ≤a+b (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inl a1) (Inr b2) = Void
  ≤a+b (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inr b1) (Inl a2) = Void
  ≤a+b (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inr b1) (Inr b2) = (b1 ≤b b2)

  a+b-refl : ∀ {A B : Set} → (a : Preorder-str A) → (b : Preorder-str B) → (x : (Either A B)) → ≤a+b a b x x
  a+b-refl (preorder _≤a_ refla transa) pre-b (Inl a) = refla a
  a+b-refl pre-a (preorder _≤b_ reflb transb) (Inr b) = reflb b

  a+b-trans : ∀ {A B : Set} → (a : Preorder-str A) → (b : Preorder-str B) → (x y z : (Either A B)) → ≤a+b a b x y → ≤a+b a b y z → ≤a+b a b x z
  a+b-trans (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inl a1) (Inl a2) (Inl a3) a1<a2 a2<a3 = transa a1 a2 a3 a1<a2 a2<a3
  a+b-trans (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inl a1) (Inl a2) (Inr b3) p ()
  a+b-trans (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inl a1) (Inr b2) (Inl a3) () q
  a+b-trans (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inl a1) (Inr b2) (Inr b3) () q
  a+b-trans (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inr b1) (Inl a2) (Inl a3) () q
  a+b-trans (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inr b1) (Inl a2) (Inr b3) () q
  a+b-trans (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inr b1) (Inr b2) (Inl a3) p ()
  a+b-trans (preorder _≤a_ refla transa) (preorder _≤b_ reflb transb) (Inr b1) (Inr b2) (Inr b3) b1<b2 b2<b3 = transb b1 b2 b3 b1<b2 b2<b3

  -- proof that A+B is a preorder
  A+B-ispreorder : ∀ (A B : Set) → Preorder-str A → Preorder-str B → Preorder-str (Either A B)
  A+B-ispreorder A B pre-a pre-b = record { ≤ = ≤a+b pre-a pre-b; refl = a+b-refl pre-a pre-b; trans = a+b-trans pre-a pre-b }

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

  -- Task 4: Show that given a Preorder A and Preorder B, Preorder (Monotone A B)

  -- the type of monotone functions from A to B
  -- i.e. functions which give you bigger outputs when you give them bigger inputs
  record Monotone (A : Set) (B : Set) (PA : Preorder-str A) (PB : Preorder-str B) : Set where
    constructor monotone
    field
      f : A → B
      is-monotone : ∀ (x y : A) → Preorder-str.≤ PA x y → Preorder-str.≤ PB (f x) (f y)

  -- the order on monotone functions is just the
  -- pointwise order on the underlying functions
  ≤mono : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (Monotone A B PA PB) → (Monotone A B PA PB) → Set
  ≤mono {A} PA PB f g = (x : A) → Preorder-str.≤ PB (Monotone.f f x) (Monotone.f g x)

  mono-refl : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x : (Monotone A B PA PB)) → ≤mono PA PB x x
  mono-refl PA PB f = λ x → Preorder-str.refl PB (Monotone.f f x)

  mono-trans : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x y z : (Monotone A B PA PB)) → ≤mono PA PB x y → ≤mono PA PB y z → ≤mono PA PB x z
  mono-trans PA PB f g h p q = λ x → Preorder-str.trans PB (Monotone.f f x) (Monotone.f g x) (Monotone.f h x) (p x) (q x)

  monotone-ispreorder : ∀ (A B : Set) → (PA : Preorder-str A) → (PB : Preorder-str B) → Preorder-str (Monotone A B PA PB)
  monotone-ispreorder A B PA PB = preorder (≤mono PA PB) (mono-refl PA PB) (mono-trans PA PB)

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

-- New stuff: Interpreting types as preorders

  -- repackaging preorder as a type together with a Preorder structure on that type
  PREORDER = Σ (λ (A : Set) → Preorder-str A)

  MONOTONE : (PΓ PA : PREORDER) → Set
  MONOTONE (Γ , PΓ) (A , PA) = Monotone Γ A PΓ PA

  -- some operations
  _×p_ : PREORDER → PREORDER → PREORDER
  (A , PA) ×p (B , PB) = A × B , AxB-ispreorder A B PA PB

  _+p_ : PREORDER → PREORDER → PREORDER
  (A , PA) +p (B , PB) = Either A B , A+B-ispreorder A B PA PB

  _->p_ : PREORDER → PREORDER → PREORDER
  (A , PA) ->p (B , PB) = Monotone A B PA PB , monotone-ispreorder A B PA PB

  -- Unit is a preorder
  unit-p : PREORDER
  unit-p = Unit , preorder (λ x y → Unit) (λ x → <>) (λ x y z _ _ → <>)

  -- identity preserves monotonicity
  id : ∀ {Γ} → MONOTONE Γ Γ
  id = λ {Γ} → monotone (λ x → x) (λ x y x₁ → x₁)

  -- composition preserves monotonicity
  comp : ∀ {PA PB PC} → MONOTONE PA PB → MONOTONE PB PC → MONOTONE PA PC
  comp (monotone f f-ismono) (monotone g g-ismono) =
          monotone (λ x → g (f x)) (λ x y x₁ → g-ismono (f x) (f y) (f-ismono x y x₁))

  -- proofs that types like pairs etc. with preorders are monotone
  pair' : ∀ {PΓ PA PB} → MONOTONE PΓ PA → MONOTONE PΓ PB → MONOTONE PΓ (PA ×p PB)
  pair' (monotone f f-ismono) (monotone g g-ismono) =
          monotone (λ x → f x , g x) (λ x y z → f-ismono x y z , g-ismono x y z)

  fst' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ×p PB) → MONOTONE PΓ PA
  fst' (monotone f f-ismono) =
          monotone (λ x → fst (f x)) (λ x y z → fst (f-ismono x y z))

  snd' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ×p PB) → MONOTONE PΓ PB
  snd' (monotone f f-ismono) =
          monotone (λ x → snd (f x)) (λ x y z → snd (f-ismono x y z))

  lam' : ∀ {PΓ PA PB} → MONOTONE (PΓ ×p PA) PB → MONOTONE PΓ (PA ->p PB)
  lam' {Γ , preorder ≤Γ reflΓ transΓ} {a , preorder ≤a refla transa} {b , preorder ≤b reflb transb} (monotone f f-ismono) =
          monotone (λ x → monotone (λ p → f (x , p)) (λ a b c → f-ismono (x , a) (x , b) (reflΓ x , c))) (λ x y z w → f-ismono (x , w) (y , w) (z , refla w))

  app' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ->p PB) → MONOTONE PΓ PA → MONOTONE PΓ PB
  app' {Γ , preorder ≤Γ reflΓ transΓ} {a , preorder ≤a refla transa} {b , preorder ≤b reflb transb} (monotone f f-ismono) (monotone g g-ismono) =
          monotone (λ x → Monotone.f (f x) (g x)) (λ x y z → transb (Monotone.f (f x) (g x)) (Monotone.f (f y) (g x)) (Monotone.f (f y) (g y))
          (f-ismono x y z (g x)) (Monotone.is-monotone (f y) (g x) (g y) (g-ismono x y z)))

  inl' : ∀ {PΓ PA PB} → MONOTONE PΓ PA → MONOTONE PΓ (PA +p PB)
  inl' (monotone f f-ismono) =
          monotone (λ x → Inl (f x)) (λ x y z → f-ismono x y z)

  inr' : ∀ {PΓ PA PB} → MONOTONE PΓ PB → MONOTONE PΓ (PA +p PB)
  inr' (monotone f f-ismono) =
          monotone (λ x → Inr (f x)) (λ x y z → f-ismono x y z)

  case : ∀ {A B C : Set} → (A → C) → (B → C) → (Either A B → C)
  case a b (Inl x) = a x
  case a b (Inr x) = b x

  el : PREORDER → Set
  el = fst

  PREORDER≤ : (PA : PREORDER) → el PA → el PA → Set
  PREORDER≤ PA = Preorder-str.≤ (snd PA)

  -- oh my god
  lemma : ∀ {PA PB PC} {c1 c2 : el (PA +p PB)} {f1 f2 : el (PA ->p PC)} {g1 g2 : el (PB ->p PC)}
        → (PREORDER≤ (PA +p PB) c1 c2)
        → (PREORDER≤ (PA ->p PC) f1 f2)
        → (PREORDER≤ (PB ->p PC) g1 g2)
        → (PREORDER≤ PC (case (Monotone.f f1) (Monotone.f g1) c1) (case (Monotone.f f2) (Monotone.f g2) c2))
  lemma {A , preorder ≤a refla transa} {B , preorder ≤b reflb transb} {C , preorder ≤c reflc transc}
        {Inl a1} {Inl a2}
        {monotone f1 f1-ismono} {monotone f2 f2-ismono}
        a b c = transc (f1 a1) (f1 a2) (f2 a2) (f1-ismono a1 a2 a) (b a2)
  lemma {PA} {PB} {PC} {Inl a1} {Inr b1} () b c
  lemma {PA} {PB} {PC} {Inr b1} {Inl a1} () b c
  lemma {A , preorder ≤a refla transa} {B , preorder ≤b reflb transb} {C , preorder ≤c reflc transc}
        {Inr b1} {Inr b2}
        {monotone f1 f1-ismono} {monotone f2 f2-ismono} {monotone g1 g1-ismono} {monotone g2 g2-ismono}
        a b c = transc (g1 b1) (g1 b2) (g2 b2) (g1-ismono b1 b2 a) (c b2)

  lemma2 : ∀ {PΓ PA PC} → MONOTONE (PΓ ×p PA) PC → el PΓ → MONOTONE PA PC
  lemma2 {Γ , preorder ≤Γ reflΓ transΓ} (monotone f f-ismono) q = monotone (λ a → f (q , a)) (λ x y z → f-ismono (q , x) (q , y) (reflΓ q , z))

  case' : ∀ {PΓ PA PB PC} → MONOTONE (PΓ ×p PA) PC -> MONOTONE (PΓ ×p PB) PC -> MONOTONE PΓ (PA +p PB) -> MONOTONE PΓ PC
  case' {Γ , preorder ≤Γ reflΓ transΓ} {a , preorder ≤a refla transa} {b , preorder ≤b reflb transb} {c , preorder ≤c reflc transc}
        (monotone f f-ismono) (monotone g g-ismono) (monotone h h-ismono) =
          monotone (λ x → case (λ a → f (x , a)) (λ b → g (x , b)) (h x))
            (λ x y z → lemma {a , preorder ≤a refla transa} {b , preorder ≤b reflb transb} {c , preorder ≤c reflc transc} {h x} {h y}
            {lemma2 {Γ , preorder ≤Γ reflΓ transΓ}
               {a , preorder ≤a refla transa} {c , preorder ≤c reflc transc}
               (monotone f f-ismono) x}
            {lemma2 {Γ , preorder ≤Γ reflΓ transΓ}
               {a , preorder ≤a refla transa} {c , preorder ≤c reflc transc}
               (monotone f f-ismono) y}
            {lemma2 {Γ , preorder ≤Γ reflΓ transΓ}
               {b , preorder ≤b reflb transb} {c , preorder ≤c reflc transc}
               (monotone g g-ismono) x}
            {lemma2 {Γ , preorder ≤Γ reflΓ transΓ}
               {b , preorder ≤b reflb transb} {c , preorder ≤c reflc transc}
               (monotone g g-ismono) y}
                         (h-ismono x y z) (λ a₁ → f-ismono (x , a₁) (y , a₁) (z , refla a₁)) (λ b₁ → g-ismono (x , b₁) (y , b₁) (z , reflb b₁)))

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Colimit.Examples where

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.SumFin

open import Cubical.Data.Graph
open import Cubical.HITs.Colimit.Base

open import Cubical.HITs.Pushout

-- Pushouts are colimits over the graph ⇐⇒

module _ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} where

  PushoutDiag : (A → B) → (A → C) → Diag (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) ⇐⇒
  (PushoutDiag f g) $ fzero             = Lift {j = ℓ-max ℓ  ℓ'' } B
  (PushoutDiag f g) $ fsuc fzero        = Lift {j = ℓ-max ℓ' ℓ'' } A
  (PushoutDiag f g) $ fsuc (fsuc fzero) = Lift {j = ℓ-max ℓ  ℓ'  } C
  _<$>_ (PushoutDiag f g) {fsuc fzero} {fzero}             tt (lift a) = lift (f a)
  _<$>_ (PushoutDiag f g) {fsuc fzero} {fsuc (fsuc fzero)} tt (lift a) = lift (g a)

module _ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {f : A → B} {g : A → C} where

  PushoutCocone : Cocone _ (PushoutDiag f g) (Pushout f g)
  leg PushoutCocone fzero               (lift b) = inl b
  leg PushoutCocone (fsuc fzero)        (lift a) = inr (g a)
  leg PushoutCocone (fsuc (fsuc fzero)) (lift c) = inr c
  com PushoutCocone {fsuc fzero} {fzero}             tt i (lift a) = push a i
  com PushoutCocone {fsuc fzero} {fsuc (fsuc fzero)} tt i (lift a) = inr (g a)

  private
    module _ ℓq (Y : Type ℓq) where

      fwd : (Pushout f g → Y) → Cocone ℓq (PushoutDiag f g) Y
      fwd = postcomp PushoutCocone

      module _ (C : Cocone ℓq (PushoutDiag f g) Y) where
        coml : ∀ a → leg C fzero               (lift (f a)) ≡ leg C (fsuc fzero) (lift a)
        comr : ∀ a → leg C (fsuc (fsuc fzero)) (lift (g a)) ≡ leg C (fsuc fzero) (lift a)
        coml a i = com C {j = fsuc fzero} {k = fzero}             tt i (lift a)
        comr a i = com C {j = fsuc fzero} {k = fsuc (fsuc fzero)} tt i (lift a)

      bwd : Cocone ℓq (PushoutDiag f g) Y → (Pushout f g → Y)
      bwd C (inl b)    = leg C fzero (lift b)
      bwd C (inr c)    = leg C (fsuc (fsuc fzero)) (lift c)
      bwd C (push a i) = (coml C a ∙ sym (comr C a)) i

      bwd-fwd : ∀ F → bwd (fwd F) ≡ F
      bwd-fwd F i (inl b) = F (inl b)
      bwd-fwd F i (inr c) = F (inr c)
      bwd-fwd F i (push a j) = compPath-filler (coml (fwd F) a) (sym (comr (fwd F) a)) (~ i) j

      fwd-bwd : ∀ C → fwd (bwd C) ≡ C
      leg (fwd-bwd C i) fzero               (lift b) = leg C fzero (lift b)
      leg (fwd-bwd C i) (fsuc fzero)        (lift a) = comr C a i
      leg (fwd-bwd C i) (fsuc (fsuc fzero)) (lift c) = leg C (fsuc (fsuc fzero)) (lift c)
      com (fwd-bwd C i) {fsuc fzero} {fzero}             tt j (lift a) -- coml (fwd-bwd C i) = ...
        = compPath-filler (coml C a) (sym (comr C a)) (~ i) j
      com (fwd-bwd C i) {fsuc fzero} {fsuc (fsuc fzero)} tt j (lift a) -- comr (fwd-bwd C i) = ...
        = comr C a (i ∧ j)

      eqv : isEquiv {A = (Pushout f g → Y)} {B = Cocone ℓq (PushoutDiag f g) Y} (postcomp PushoutCocone)
      eqv = isoToIsEquiv (iso fwd bwd fwd-bwd bwd-fwd)

  isColimPushout : isColimit (PushoutDiag f g) (Pushout f g)
  cone isColimPushout = PushoutCocone
  univ isColimPushout = eqv

  colim≃Pushout : colim (PushoutDiag f g) ≃ Pushout f g
  colim≃Pushout = uniqColimit colimIsColimit isColimPushout

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Luau.OpSem where

open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
open import FFI.Data.Maybe using (just)
open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; number)
open import Luau.Value using (addr; val; number)

evalBinOp : Float → BinaryOperator → Float → Float
evalBinOp x + y = primFloatPlus x y
evalBinOp x - y = primFloatMinus x y
evalBinOp x * y = primFloatTimes x y
evalBinOp x / y = primFloatDiv x y

data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set

data _⊢_⟶ᴱ_⊣_  where

  nil : ∀ {H} →

    -------------------
    H ⊢ nil ⟶ᴱ nil ⊣ H

  function : ∀ {H H′ a F B} →

    H′ ≡ H ⊕ a ↦ (function F is B end) →
    -------------------------------------------
    H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′

  app₁ : ∀ {H H′ M M′ N} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    -----------------------------
    H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′

  app₂ : ∀ {H H′ V N N′} →

    H ⊢ N ⟶ᴱ N′ ⊣ H′ →
    -----------------------------
    H ⊢ (val V $ N) ⟶ᴱ (val V $ N′) ⊣ H′

  beta : ∀ {H a F B V} →

    H [ a ] ≡ just(function F is B end) →
    -----------------------------------------------------------------------------
    H ⊢ (addr a $ val V) ⟶ᴱ (block (fun F) is (B [ V / name(arg F) ]ᴮ) end) ⊣ H

  block : ∀ {H H′ B B′ b} →

    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
    ----------------------------------------------------
    H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′

  return : ∀ {H V B b} →

    --------------------------------------------------------
    H ⊢ (block b is return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H

  done : ∀ {H b} →

    ---------------------------------
    H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H

  binOpEval :
    ∀ {H x op y} →
    --------------------------------------------------------------------------
    H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (number (evalBinOp x op y)) ⊣ H

  binOp₁ :
    ∀ {H H′ x x′ op y} →
    H ⊢ x ⟶ᴱ x′ ⊣ H′ →
    ---------------------------------------------
    H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′

  binOp₂ :
    ∀ {H H′ x op y y′} →
    H ⊢ y ⟶ᴱ y′ ⊣ H′ →
    ---------------------------------------------
    H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′

data _⊢_⟶ᴮ_⊣_  where

  local : ∀ {H H′ x M M′ B} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    -------------------------------------------------
    H ⊢ (local x ← M ∙ B) ⟶ᴮ (local x ← M′ ∙ B) ⊣ H′

  subst : ∀ {H x v B} →

    ------------------------------------------------------
    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H

  function : ∀ {H H′ a F B C} →

    H′ ≡ H ⊕ a ↦ (function F is C end) →
    --------------------------------------------------------------
    H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / fun F ]ᴮ) ⊣ H′

  return : ∀ {H H′ M M′ B} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    --------------------------------------------
    H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′

data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set where

  refl : ∀ {H B} →

    ----------------
    H ⊢ B ⟶* B ⊣ H

  step : ∀ {H H′ H″ B B′ B″} →
    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
    H′ ⊢ B′ ⟶* B″ ⊣ H″ →
    ------------------
    H ⊢ B ⟶* B″ ⊣ H″


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Arguments used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Argument where

open import Data.List.Base as List using (List; []; _∷_)
open import Data.Product using (_×_; _,_; uncurry; <_,_>)
open import Data.Nat using (ℕ)
open import Reflection.Argument.Visibility
open import Reflection.Argument.Relevance
open import Reflection.Argument.Information as Information
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Level

private
  variable
    a b : Level
    A B : Set a

------------------------------------------------------------------------
-- Re-exporting the builtins publicly

open import Agda.Builtin.Reflection public using (Arg)
open Arg public

-- Pattern synonyms

pattern vArg ty = arg (arg-info visible relevant)   ty
pattern hArg ty = arg (arg-info hidden relevant)    ty
pattern iArg ty = arg (arg-info instance′ relevant) ty

------------------------------------------------------------------------
-- Lists of arguments

Args : {a : Level} (A : Set a) → Set a
Args A = List (Arg A)

infixr 5 _⟨∷⟩_ _⟅∷⟆_
pattern _⟨∷⟩_ x xs = vArg x ∷ xs
pattern _⟅∷⟆_ x xs = hArg x ∷ xs

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

map : (A → B) → Arg A → Arg B
map f (arg i x) = arg i (f x)

map-Args : (A → B) → Args A → Args B
map-Args f xs = List.map (map f) xs

------------------------------------------------------------------------
-- Decidable equality

arg-injective₁ : ∀ {i i′} {a a′ : A} → arg i a ≡ arg i′ a′ → i ≡ i′
arg-injective₁ refl = refl

arg-injective₂ : ∀ {i i′} {a a′ : A} → arg i a ≡ arg i′ a′ → a ≡ a′
arg-injective₂ refl = refl

arg-injective : ∀ {i i′} {a a′ : A} → arg i a ≡ arg i′ a′ → i ≡ i′ × a ≡ a′
arg-injective = < arg-injective₁ , arg-injective₂ >

-- We often need decidability of equality for Arg A when implementing it
-- for A. Unfortunately ≡-dec makes the termination checker unhappy.
-- Instead, we can match on both Arg A and use unArg-dec for an obviously
-- decreasing recursive call.

unArg : Arg A → A
unArg (arg i a) = a

unArg-dec : {x y : Arg A} → Dec (unArg x ≡ unArg y) → Dec (x ≡ y)
unArg-dec {x = arg i a} {arg i′ a′} a≟a′ =
  Dec.map′ (uncurry (cong₂ arg)) arg-injective ((i Information.≟ i′) ×-dec a≟a′)

≡-dec : DecidableEquality A → DecidableEquality (Arg A)
≡-dec _≟_ x y = unArg-dec (unArg x ≟ unArg y)


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Concrete.Records
open import LibraBFT.Impl.Consensus.Network
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.NetworkMsg
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.Network.Properties where

open Invariants

module processProposalSpec (proposal : ProposalMsg) (myEpoch : Epoch) (vv : ValidatorVerifier) where
  postulate -- TODO-2: Refine contract
    -- We also need to know that the the proposal message was successfully
    -- checked by `ProposalMsg.verify`
    contract
      : case (processProposal proposal myEpoch vv) of λ where
          (Left _) → Unit
          (Right _) → proposal ^∙ pmProposal ∙ bEpoch ≡ myEpoch
                      × BlockId-correct (proposal ^∙ pmProposal)


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

module Cubical.Data.Fin where

open import Cubical.Data.Fin.Base public
open import Cubical.Data.Fin.Properties public

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed containers aka interaction structures aka polynomial
-- functors. The notation and presentation here is closest to that of
-- Hancock and Hyvernat in "Programming interfaces and basic topology"
-- (2006/9).
------------------------------------------------------------------------

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

module Data.Container.Indexed where

open import Level
open import Codata.Musical.M.Indexed
open import Data.Product as Prod hiding (map)
open import Data.W.Indexed
open import Function renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (_↔_; module Inverse)
open import Relation.Unary using (Pred; _⊆_)
import Relation.Binary as B
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl)

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

-- The type and its semantics ("extension").

open import Data.Container.Indexed.Core public
open Container public

-- Abbreviation for the commonly used level one version of indexed
-- containers.

_▷_ : Set → Set → Set₁
I ▷ O = Container I O zero zero

-- The least and greatest fixpoint.

μ ν : ∀ {o c r} {O : Set o} → Container O O c r → Pred O _
μ = W
ν = M

-- An equivalence relation is defined in Data.Container.Indexed.WithK.

------------------------------------------------------------------------
-- Functoriality

-- Indexed containers are functors.

map : ∀ {i o c r ℓ₁ ℓ₂} {I : Set i} {O : Set o}
      (C : Container I O c r) {X : Pred I ℓ₁} {Y : Pred I ℓ₂} →
      X ⊆ Y → ⟦ C ⟧ X ⊆ ⟦ C ⟧ Y
map _ f = Prod.map ⟨id⟩ (λ g → f ⟨∘⟩ g)

-- Some properties are proved in Data.Container.Indexed.WithK.

------------------------------------------------------------------------
-- Container morphisms

module _ {i₁ i₂ o₁ o₂}
         {I₁ : Set i₁} {I₂ : Set i₂} {O₁ : Set o₁} {O₂ : Set o₂} where

  -- General container morphism.

  record ContainerMorphism {c₁ c₂ r₁ r₂ ℓ₁ ℓ₂}
         (C₁ : Container I₁ O₁ c₁ r₁) (C₂ : Container I₂ O₂ c₂ r₂)
         (f : I₁ → I₂) (g : O₁ → O₂)
         (_∼_ : B.Rel I₂ ℓ₁) (_≈_ : B.REL (Set r₂) (Set r₁) ℓ₂)
         (_·_ : ∀ {A B} → A ≈ B → A → B) :
         Set (i₁ ⊔ i₂ ⊔ o₁ ⊔ o₂ ⊔ c₁ ⊔ c₂ ⊔ r₁ ⊔ r₂ ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      command   : Command C₁ ⊆ Command C₂ ⟨∘⟩ g
      response  : ∀ {o} {c₁ : Command C₁ o} →
                  Response C₂ (command c₁) ≈ Response C₁ c₁
      coherent  : ∀ {o} {c₁ : Command C₁ o} {r₂ : Response C₂ (command c₁)} →
                  f (next C₁ c₁ (response · r₂)) ∼ next C₂ (command c₁) r₂

  open ContainerMorphism public

  -- Plain container morphism.

  _⇒[_/_]_ : ∀ {c₁ c₂ r₁ r₂} →
             Container I₁ O₁ c₁ r₁ → (I₁ → I₂) → (O₁ → O₂) →
             Container I₂ O₂ c₂ r₂ → Set _
  C₁ ⇒[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ (λ R₂ R₁ → R₂ → R₁) _$_

  -- Linear container morphism.

  _⊸[_/_]_ : ∀ {c₁ c₂ r₁ r₂} →
             Container I₁ O₁ c₁ r₁ → (I₁ → I₂) → (O₁ → O₂) →
             Container I₂ O₂ c₂ r₂ → Set _
  C₁ ⊸[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ _↔_
                                       (λ r₂↔r₁ r₂ → Inverse.to r₂↔r₁ ⟨$⟩ r₂)

  -- Cartesian container morphism.

  _⇒C[_/_]_ : ∀ {c₁ c₂ r} →
              Container I₁ O₁ c₁ r → (I₁ → I₂) → (O₁ → O₂) →
              Container I₂ O₂ c₂ r → Set _
  C₁ ⇒C[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ (λ R₂ R₁ → R₂ ≡ R₁)
                                        (λ r₂≡r₁ r₂ → P.subst ⟨id⟩ r₂≡r₁ r₂)

-- Degenerate cases where no reindexing is performed.

module _ {i o c r} {I : Set i} {O : Set o} where

  _⇒_ : B.Rel (Container I O c r) _
  C₁ ⇒ C₂ = C₁ ⇒[ ⟨id⟩ / ⟨id⟩ ] C₂

  _⊸_ : B.Rel (Container I O c r) _
  C₁ ⊸ C₂ = C₁ ⊸[ ⟨id⟩ / ⟨id⟩ ] C₂

  _⇒C_ : B.Rel (Container I O c r) _
  C₁ ⇒C C₂ = C₁ ⇒C[ ⟨id⟩ / ⟨id⟩ ] C₂

------------------------------------------------------------------------
-- Plain morphisms

-- Interpretation of _⇒_.

⟪_⟫ : ∀ {i o c r ℓ} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r} →
      C₁ ⇒ C₂ → (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
⟪ m ⟫ X (c , k) = command m c , λ r₂ →
  P.subst X (coherent m) (k (response m r₂))

module PlainMorphism {i o c r} {I : Set i} {O : Set o} where

  -- Identity.

  id : (C : Container I O c r) → C ⇒ C
  id _ = record
    { command  = ⟨id⟩
    ; response = ⟨id⟩
    ; coherent = refl
    }

  -- Composition.

  infixr 9 _∘_

  _∘_ : {C₁ C₂ C₃ : Container I O c r} →
        C₂ ⇒ C₃ → C₁ ⇒ C₂ → C₁ ⇒ C₃
  f ∘ g = record
    { command  = command  f ⟨∘⟩ command g
    ; response = response g ⟨∘⟩ response f
    ; coherent = coherent g ⟨ P.trans ⟩ coherent f
    }

  -- Identity commutes with ⟪_⟫.

  id-correct : ∀ {ℓ} {C : Container I O c r} → ∀ {X : Pred I ℓ} {o} →
               ⟪ id C ⟫ X {o} ≗ ⟨id⟩
  id-correct _ = refl

  -- More properties are proved in Data.Container.Indexed.WithK.

------------------------------------------------------------------------
-- Linear container morphisms

module LinearMorphism
  {i o c r} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r}
  (m : C₁ ⊸ C₂)
  where

  morphism : C₁ ⇒ C₂
  morphism = record
    { command  = command m
    ; response = _⟨$⟩_ (Inverse.to (response m))
    ; coherent = coherent m
    }

  ⟪_⟫⊸ : ∀ {ℓ} (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
  ⟪_⟫⊸ = ⟪ morphism ⟫

open LinearMorphism public using (⟪_⟫⊸)

------------------------------------------------------------------------
-- Cartesian morphisms

module CartesianMorphism
  {i o c r} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r}
  (m : C₁ ⇒C C₂)
  where

  morphism : C₁ ⇒ C₂
  morphism = record
    { command  = command m
    ; response = P.subst ⟨id⟩ (response m)
    ; coherent = coherent m
    }

  ⟪_⟫C : ∀ {ℓ} (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
  ⟪_⟫C = ⟪ morphism ⟫

open CartesianMorphism public using (⟪_⟫C)

------------------------------------------------------------------------
-- All and any

-- □ and ◇ are defined in the core module.

module _ {i o c r ℓ₁ ℓ₂} {I : Set i} {O : Set o} (C : Container I O c r)
         {X : Pred I ℓ₁} {P Q : Pred (Σ I X) ℓ₂} where

  -- All.

  □-map : P ⊆ Q → □ C P ⊆ □ C Q
  □-map P⊆Q = _⟨∘⟩_ P⊆Q

  -- Any.

  ◇-map : P ⊆ Q → ◇ C P ⊆ ◇ C Q
  ◇-map P⊆Q = Prod.map ⟨id⟩ P⊆Q

-- Membership is defined in Data.Container.Indexed.WithK.


text:
module Monads.ExceptT where

open import Class.Monad
open import Class.Monad.Except
open import Class.Monad.State
open import Class.MonadTrans
open import Data.Sum
open import Function
open import Level

private
  variable
    a : Level

ExceptT : (M : Set a -> Set a) -> Set a -> Set a -> Set a
ExceptT M E A = M (E ⊎ A)

ExceptT-MonadTrans : {E : Set a} -> MonadTrans (λ (M : Set a -> Set a) -> ExceptT M E)
ExceptT-MonadTrans = record { embed = λ x -> x >>= (return ∘ inj₂) }

module _ {M : Set a -> Set a} {{_ : Monad M}} {E : Set a} where

  ExceptT-Monad : Monad (ExceptT M E)
  ExceptT-Monad = record { _>>=_ = helper ; return = λ x → (return $ inj₂ x) }
    where
      helper : ∀ {A B} -> ExceptT M E A -> (A -> ExceptT M E B) -> ExceptT M E B
      helper x f = x >>= λ { (inj₁ y) -> return $ inj₁ y ; (inj₂ y) -> f y }

  private
    throwError' : ∀ {A : Set a} -> E -> ExceptT M E A
    throwError' = return ∘ inj₁

    catchError' : ∀ {A} -> ExceptT M E A -> (E -> ExceptT M E A) -> ExceptT M E A
    catchError' x f = x >>= λ { (inj₁ x) → f x ; (inj₂ y) → return {{ExceptT-Monad}} y }

  ExceptT-MonadExcept : MonadExcept (ExceptT M E) {{ExceptT-Monad}} E
  ExceptT-MonadExcept = record { throwError = throwError' ; catchError = catchError' }

  ExceptT-MonadState : ∀ {S} {{_ : MonadState M S}} -> MonadState (ExceptT M E) {{ExceptT-Monad}} S
  ExceptT-MonadState = record
    { get = embed {{ExceptT-MonadTrans}} get
    ; put = embed {{ExceptT-MonadTrans}} ∘ put }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
-- Andreas, 2020-06-17, issue #4135
-- Constructor disambiguation on should only instantiate metas
-- in a unique way.

-- {-# OPTIONS -v tc.lhs:10 #-}
-- {-# OPTIONS -v tc.lhs.split:40 #-}
-- {-# OPTIONS -v tc.lhs.disamb:40 #-}

data Bool : Set where
  true false : Bool

module Foo (b : Bool) where

  data D : Set where
    c : D

open module True  = Foo true
open module False = Foo false

test : Foo.D ? → Set
test c = ?

-- C-c C-=

-- EXPECTED ERROR:
-- Ambiguous constructor c.
-- ...
-- when checking that the pattern c has type Foo.D ?0


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------

-- This file contains some core definitions which are re-exported by
-- Relation.Binary.Indexed.Heterogeneous.

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

module Relation.Binary.Indexed.Heterogeneous.Core where

open import Level
import Relation.Binary.Core as B
import Relation.Binary.PropositionalEquality.Core as P

------------------------------------------------------------------------
-- Indexed binary relations

-- Heterogeneous types

IREL : ∀ {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} →
      (I₁ → Set a₁) → (I₂ → Set a₂) → (ℓ : Level) → Set _
IREL A₁ A₂ ℓ = ∀ {i₁ i₂} → A₁ i₁ → A₂ i₂ → Set ℓ

-- Homogeneous types

IRel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
IRel A ℓ = IREL A A ℓ

------------------------------------------------------------------------
-- Simple properties of indexed binary relations

Reflexive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → IRel A ℓ → Set _
Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})

Symmetric : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → IRel A ℓ → Set _
Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_

Transitive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → IRel A ℓ → Set _
Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})

-- Generalised implication.

infixr 4 _=[_]⇒_

_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} →
          B.Rel A ℓ₁ → ((x : A) → B x) → IRel B ℓ₂ → Set _
P =[ f ]⇒ Q = ∀ {i j} → P i j → Q (f i) (f j)


text:
module System.File where

open import System.FilePath
open import Prelude.IO
open import Prelude.String
open import Prelude.Unit
open import Prelude.Function
open import Prelude.Bytes

{-# FOREIGN GHC import qualified Data.Text as Text #-}
{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}
{-# FOREIGN GHC import qualified Data.ByteString as B #-}

private
  module Internal where
    StrFilePath : Set
    StrFilePath = String

    postulate
      readTextFile  : StrFilePath → IO String
      writeTextFile : StrFilePath → String → IO Unit

      readBinaryFile  : StrFilePath → IO Bytes
      writeBinaryFile : StrFilePath → Bytes → IO Unit

    {-# COMPILE GHC readTextFile    = Text.readFile  . Text.unpack #-}
    {-# COMPILE GHC writeTextFile   = Text.writeFile . Text.unpack #-}
    {-# COMPILE GHC readBinaryFile  = B.readFile     . Text.unpack #-}
    {-# COMPILE GHC writeBinaryFile = B.writeFile    . Text.unpack #-}

    {-# COMPILE UHC readTextFile  = UHC.Agda.Builtins.primReadFile  #-}
    {-# COMPILE UHC writeTextFile = UHC.Agda.Builtins.primWriteFile #-}

readTextFile : ∀ {k} → Path k → IO String
readTextFile = Internal.readTextFile ∘ toString

writeTextFile : ∀ {k} → Path k → String → IO Unit
writeTextFile = Internal.writeTextFile ∘ toString

readBinaryFile : ∀ {k} → Path k → IO Bytes
readBinaryFile = Internal.readBinaryFile ∘ toString

writeBinaryFile : ∀ {k} → Path k → Bytes → IO Unit
writeBinaryFile = Internal.writeBinaryFile ∘ toString

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


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

module Examples.Gcd.Refine where

open import Calf.CostMonoid
import Calf.CostMonoids as CM

open import Calf CM.ℕ-CostMonoid
open import Calf.Types.Nat
open import Calf.Types.Bounded CM.ℕ-CostMonoid

open import Examples.Gcd.Euclid
open import Examples.Gcd.Clocked as Clocked

open import Data.Nat.DivMod
open import Data.Nat
open import Relation.Binary.PropositionalEquality as P
open import Function
open import Data.Nat.Properties
open import Data.Product
open import Data.Bool using (Bool; false; true)
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary

fib : ℕ → ℕ
fib 0 = 0
fib 1 = 1
fib (suc (suc n)) = fib (suc n) + fib n

fib⁻¹/helper : ℕ → ℕ → ℕ
fib⁻¹/helper F zero = 0
fib⁻¹/helper F (suc i) with fib (suc i) ≤? F
... | (true because (ofʸ py)) = suc i
... | (false because (ofⁿ pn)) = fib⁻¹/helper F i

fib⁻¹ : ℕ → ℕ
fib⁻¹ F = fib⁻¹/helper F (1 + F)

fib⁻¹-unfold : ∀ F i → ¬ (fib (suc i) ≤ F) →
               fib⁻¹/helper F (suc i) ≡ fib⁻¹/helper F i
fib⁻¹-unfold F i h with fib (suc i) ≤? F
... | (true because (ofʸ py)) = case (h py) of λ {()}
... | (false because (ofⁿ pn)) = refl

fib-base : ∀ n → 1 ≤ fib (1 + n)
fib-base zero = s≤s z≤n
fib-base (suc n') =
  let g = fib-base n' in
  ≤-trans g (m≤m+n _ _)

fib-inc : ∀ n → n < fib (2 + n)
fib-inc zero = s≤s z≤n
fib-inc (suc n') =
  let g = fib-inc n' in
  let g1 = +-mono-≤ g (fib-base n') in
  subst (λ k → k ≤ fib (2 + suc n')) (P.cong suc (P.trans (+-suc n' 0) (P.cong suc (+-identityʳ _)))) g1

fib-fib⁻¹/helper : ∀ F i → fib (suc i) > F → Σ (fib (fib⁻¹/helper F i) ≤ F) λ _ → F < fib (1 + fib⁻¹/helper F i)
fib-fib⁻¹/helper F zero h = z≤n , h
fib-fib⁻¹/helper F (suc i') h with fib (suc i') ≤? F
... | (true because (ofʸ py)) = py , h
... | (false because (ofⁿ pn)) = fib-fib⁻¹/helper F i' (≰⇒> pn)

fib-fib⁻¹ : ∀ F → Σ (fib (fib⁻¹ F) ≤ F) λ _ → F < fib (1 + fib⁻¹ F)
fib-fib⁻¹ F = fib-fib⁻¹/helper F (1 + F) (fib-inc F)

fib-mono-< : fib Preserves _<_ ⟶ _≤_
fib-mono-< {zero} {zero} h = case h of λ {()}
fib-mono-< {zero} {suc y} h = ≤-trans z≤n (fib-base y)
fib-mono-< {1} {1} (s≤s h) = case h of λ {()}
fib-mono-< {1} {suc (suc y)} h = fib-base (suc y)
fib-mono-< {suc (suc x)} {suc (suc y)} (s≤s (s≤s h)) =
  let g = fib-mono-< h in
  let g1 = fib-mono-< (s≤s h) in
  +-mono-≤ g1 g

-- test : ℕ
-- test = gcd/depth (7 , 4 , s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))

gcd/fib : ∀ (n : ℕ) (i@(x , y , h) : m>n) →
          gcd/depth i ≥ 1 + n  →
          Σ (x ≥ fib (2 + n)) λ _ → (y ≥ fib (1 + n))
gcd/fib zero (x , y , h) h1 with 1 ≤? y | 1 ≤? x
... | (true because (ofʸ py)) | (true because (ofʸ px)) = px , py
... | (true because _) | (false because (ofⁿ px)) =
  let g = ≰⇒> px in
  let g1 = n<1⇒n≡0 g in
  let g2 = P.subst (λ x → y < x) g1 h in
  case g2 of λ { () }
... | (false because (ofⁿ py)) | _ rewrite (n<1⇒n≡0 (≰⇒> py)) =
  case h1 of λ { () }
gcd/fib (suc n) (x , y , h) h1 with y
... | zero = let g = n≤0⇒n≡0 h1 in case g of λ {()}
... | suc y' rewrite gcd/depth-unfold-suc {x} {y'} {h} =
  let g : suc (gcd/depth (suc y' , x % suc y' , m%n<n x y')) ≥ 1 + (suc n)
      g = h1 in
  let g1 = +-cancelˡ-≤ 1 g in
  let (r1 , r2) = gcd/fib n (suc y' , x % suc y' , m%n<n x y') g1 in
  let r1' : fib n + fib (suc n) ≤ suc y'
      r1' = P.subst (λ n → n ≤ suc y') (+-comm (fib (suc n)) (fib n)) r1 in
  (let e1 = m≡m%n+[m/n]*n x y' in
  let e2 = m/n*n≤m x (suc y') in
  let e3 : 1 ≤ x / suc y'
      e3 = m≥n⇒m/n>0 (≤-trans (n≤1+n (suc y'))  h) in
  let e4 : 1 * (suc y') ≤ x / suc y' * suc y'
      e4 = *-monoˡ-≤ (suc y') e3 in
  let e5 = P.subst (λ n → n ≤ x / suc y' * suc y') (*-identityˡ (suc y')) e4 in
  P.subst (λ n → x ≥ n) (P.sym (+-assoc (fib (1 + n)) (fib n) (fib (1 + n)))) (
  P.subst (λ x → x ≥ _) (P.sym e1)
    (+-mono-≤ {x = fib (1 + n)} {y = x % (suc y')}
    r2 (≤-trans r1' e5))
  )), r1

gcd/depth/bound : ∀ (n : ℕ) (i@(x , y , h) : m>n) →
                x < fib (2 + n) → y < (fib (1 + n)) →
                gcd/depth i < 1 + n
gcd/depth/bound n i h1 h2 = ≰⇒> (contraposition (gcd/fib n i) (λ { (g1 , g2) → (<⇒≱ h1) g1}))

gcd/depth/closed : m>n → ℕ
gcd/depth/closed i@(x , y , h) = 1 + fib⁻¹ x

gcd/depth≤gcd/depth/closed : ∀ (i@(x , y , h) : m>n) → gcd/depth i ≤ gcd/depth/closed i
gcd/depth≤gcd/depth/closed i@(x , y , h) =
  let g : x < fib (1 + fib⁻¹ x)
      g = fib-fib⁻¹ x .proj₂ in
  let g1 : fib (1 + fib⁻¹ x) ≤ fib (2 + fib⁻¹ x)
      g1 = fib-mono-< {1 + fib⁻¹ x} {2 + fib⁻¹ x} (+-monoˡ-< (fib⁻¹ x) (s≤s (s≤s z≤n))) in
  (<⇒≤ (gcd/depth/bound _ i (<-transˡ g g1) (<-trans h g)))

gcd≤gcd/depth/closed : ∀ i → IsBounded nat (gcd i) (gcd/depth/closed i)
gcd≤gcd/depth/closed i = bound/relax (λ _ → gcd/depth≤gcd/depth/closed i) (gcd≤gcd/depth i)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
-- Andreas, 2016-05-03 issue #1950
-- testcases from issue #679

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v reify.display:100 #-}
-- {-# OPTIONS -v tc.display.top:100 #-}

postulate anything : ∀{A : Set} → A
postulate Anything : ∀{A : Set1} → A

record ⊤ : Set where

data ty : Set where
  ♭ : ty
  _`→_ : ty → ty → ty

⟦_⟧ : ty → Set
⟦ ♭ ⟧ = ⊤
⟦ A `→ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

eq : ∀ (σ : ty) (a b : ⟦ σ ⟧) → Set
eq ♭ a b = Anything
eq (A `→ B) f g = ∀ {a : ⟦ A ⟧} → eq B (f a) (g a)

eq-sym : ∀ σ {a b} (h : eq σ a b) → eq σ b a
eq-sym ♭ h = anything
eq-sym (A `→ B) h with B
... | B' = {!B'!}

-- splitting on B' should yield
-- eq-sym (A `→ B) h | ♭ = {!!}
-- eq-sym (A `→ B) h | B' `→ B'' = {!!}

data Unit : Set where
  unit : Unit

T : Unit → Set
T unit = {u : Unit} → Unit

fails : (u : Unit) → T u
fails unit with unit
... | q = {!q!}

-- Splitting on q should yield
-- fails unit | unit = {!!}