text:
-- Instances of semantic kits
module Semantics.Substitution.Instances where

open import Syntax.Types
open import Syntax.Context renaming (_,_ to _,,_)
open import Syntax.Terms
open import Syntax.Substitution.Kits
open import Syntax.Substitution.Instances

open import Semantics.Types
open import Semantics.Context
open import Semantics.Terms
open import Semantics.Substitution.Kits
open import Semantics.Substitution.Traversal

open import CategoryTheory.Categories using (ext)
open import CategoryTheory.NatTrans
open import CategoryTheory.Functor
open import CategoryTheory.Monad
open import CategoryTheory.Comonad
open import CategoryTheory.Instances.Reactive renaming (top to ⊤)
open import TemporalOps.Diamond
open import TemporalOps.Box
open import TemporalOps.Common.Rewriting

open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality as ≅ using (_≅_)

open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

open ≡-Reasoning
private module F-□ = Functor F-□
open Comonad W-□

-- Denotation of variable kits
⟦𝒱ar⟧ : ⟦Kit⟧ 𝒱ar
⟦𝒱ar⟧ = record
    { ⟦_⟧ = ⟦_⟧-var
    ; ⟦𝓋⟧ = λ A Δ → refl
    ; ⟦𝓉⟧ = ⟦𝓉⟧-var
    ; ⟦𝓌⟧ = λ B T → refl
    ; ⟦𝒶⟧ = ⟦𝒶⟧-var
    }
    where
    open Kit 𝒱ar
    ⟦_⟧-var : ∀{A Γ} → Var Γ A → ⟦ Γ ⟧ₓ ⇴ ⟦ A ⟧ⱼ
    ⟦ top ⟧-var n (_ , ⟦A⟧) = ⟦A⟧
    ⟦ pop v ⟧-var n (⟦Γ⟧ , _) = ⟦ v ⟧-var n ⟦Γ⟧

    ⟦𝓉⟧-var : ∀{A Γ} → (x : Var Γ A)
          -> ⟦ 𝓉 x ⟧ₘ ≈ ⟦ x ⟧-var
    ⟦𝓉⟧-var {A now} top = refl
    ⟦𝓉⟧-var {A always} top = refl
    ⟦𝓉⟧-var {A now} (pop x) = ⟦𝓉⟧-var x
    ⟦𝓉⟧-var {A always} (pop x) = ⟦𝓉⟧-var x

    ⟦𝒶⟧-var : ∀{A Δ} → (x : Var Δ (A always))
           -> F-□.fmap ⟦ 𝒶 x ⟧-var ∘ ⟦ Δ ˢ⟧□ ≈ δ.at ⟦ A ⟧ₜ ∘ ⟦ x ⟧-var
    ⟦𝒶⟧-var top = refl
    ⟦𝒶⟧-var (pop {B = B now} x) = ⟦𝒶⟧-var x
    ⟦𝒶⟧-var (pop {B = B always} x) = ⟦𝒶⟧-var x

-- Denotation of term kits
⟦𝒯erm⟧ : ⟦Kit⟧ 𝒯erm
⟦𝒯erm⟧ = record
    { ⟦_⟧ = ⟦_⟧ₘ
    ; ⟦𝓋⟧ = λ A Δ → refl
    ; ⟦𝓉⟧ = λ T → refl
    ; ⟦𝓌⟧ = ⟦𝓌⟧-term
    ; ⟦𝒶⟧ = ⟦𝒶⟧-term
    }
    where
    open Kit 𝒯erm
    open ⟦Kit⟧ ⟦𝒱ar⟧
    open K
    open ⟦K⟧ ⟦𝒱ar⟧

    ⟦𝓌⟧-term : ∀ B {Δ A} → (M : Term Δ A)
           -> ⟦ 𝓌 {B} M ⟧ₘ ≈ ⟦ M ⟧ₘ ∘ π₁
    ⟦𝓌⟧-term B {Δ} M {n} {⟦Δ⟧ , ⟦B⟧}
        rewrite traverse-sound ⟦𝒱ar⟧ (_⁺_ {B} (idₛ 𝒱ar) 𝒱ar) M {n} {⟦Δ⟧ , ⟦B⟧}
              | ⟦⁺⟧ B {Δ} (idₛ 𝒱ar) {n} {⟦Δ⟧ , ⟦B⟧}
              | ⟦idₛ⟧ {Δ} {n} {⟦Δ⟧} = refl

    ⟦𝒶⟧-term : ∀{A Δ} (M : Δ ⊢ A always)
           -> F-□.fmap ⟦ 𝒶 M ⟧ₘ ∘ ⟦ Δ ˢ⟧□ ≈ δ.at ⟦ A ⟧ₜ ∘ ⟦ M ⟧ₘ
    ⟦𝒶⟧-term {A} {∙} (var ())
    ⟦𝒶⟧-term {A} {∙} (stable M) = refl
    ⟦𝒶⟧-term {A} {Δ ,, B now} (var (pop x)) = ⟦𝒶⟧-term (var x)
    ⟦𝒶⟧-term {A} {Δ ,, B now} (stable M) = ⟦𝒶⟧-term {A} {Δ} (stable M)
    ⟦𝒶⟧-term {.B} {Δ ,, B always} (var top) = refl
    ⟦𝒶⟧-term {A} {Δ ,, B always} (var (pop x)) {n} {⟦Δ⟧ , □⟦B⟧} = ext lemma
        where
        lemma : ∀ l -> ⟦ traverse 𝒱ar (_⁺_ {B always} (idₛ 𝒱ar) 𝒱ar) (𝒶 (var x)) ⟧ₘ l (⟦ Δ ˢ⟧□ n ⟦Δ⟧ l , □⟦B⟧)
                     ≡ ⟦ var x ⟧ₘ n ⟦Δ⟧
        lemma l rewrite traverse-sound ⟦𝒱ar⟧ (_⁺_ {B always} (idₛ 𝒱ar) 𝒱ar) (𝒶 (var x)) {l} {⟦ Δ ˢ⟧□ n ⟦Δ⟧ l , □⟦B⟧}
                      | ⟦⁺⟧ (B always) {Δ ˢ} (idₛ 𝒱ar) {l} {⟦ Δ ˢ⟧□ n ⟦Δ⟧ l , □⟦B⟧}
                      | ⟦idₛ⟧ {Δ ˢ} {l} {⟦ Δ ˢ⟧□ n ⟦Δ⟧ l}
                      | □-≡ n l (⟦𝒶⟧-term (var x) {n} {⟦Δ⟧}) l = refl
    ⟦𝒶⟧-term {A} {Δ ,, B always} (stable M) {n} {⟦Δ⟧ , □⟦B⟧} = ext λ x → ext (lemma2 x)
        where
        lemma1 : ∀ Δ (n l m : ℕ) (⟦Δ⟧ : ⟦ Δ ⟧ₓ n)
                 -> (F-□.fmap ⟦ Δ ˢ ˢ⟧□ ∘ ⟦ Δ ˢ⟧□) n ⟦Δ⟧ l m
                  ≡ (F-□.fmap ⟦ Δ ˢ ˢ⟧ ∘ ⟦ Δ ˢ⟧□) n ⟦Δ⟧ m
        lemma1 Δ n l m ⟦Δ⟧ rewrite □-≡ l m (□-≡ n l (⟦ˢ⟧□-twice Δ {n} {⟦Δ⟧}) l) m
                = □-≡ n m (⟦ˢ⟧-comm Δ) m

        lemma2 : ∀ l j
              -> (F-□.fmap ⟦ 𝒶 {Δ ,, B always} (stable M) ⟧ₘ ∘ ⟦ Δ ,, B always ˢ⟧□) n (⟦Δ⟧ , □⟦B⟧) l j
               ≡ (δ.at ⟦ A ⟧ₜ ∘ ⟦ stable {Δ ,, B always} M ⟧ₘ) n (⟦Δ⟧ , □⟦B⟧) l j
        lemma2 l j =
            begin
                ⟦ subst (λ x → x ,, B always ⊢ A now) (ˢ-idemp′ Δ) M ⟧ₘ j (⟦ Δ ˢ ˢ⟧□ l (⟦ Δ ˢ⟧□ n ⟦Δ⟧ l) j  , □⟦B⟧)
            ≡⟨ cong (λ x → ⟦ subst (λ x → x ,, B always ⊢ A now) (ˢ-idemp′ Δ) M ⟧ₘ j (x , □⟦B⟧)) (lemma1 Δ n l j ⟦Δ⟧) ⟩
                ⟦ subst (λ x → x ,, B always ⊢ A now) (ˢ-idemp′ Δ) M ⟧ₘ j (⟦ Δ ˢ ˢ⟧ j (⟦ Δ ˢ⟧□ n ⟦Δ⟧ j) , □⟦B⟧)
            ≡⟨ cong (λ x → ⟦ subst (λ x → x ,, B always ⊢ A now) (ˢ-idemp′ Δ) M ⟧ₘ j (x , □⟦B⟧)) (⟦ˢ⟧-rew Δ n j ⟦Δ⟧) ⟩
                ⟦ subst (λ x → x ,, B always ⊢ A now) (ˢ-idemp′ Δ) M ⟧ₘ j (rew (⟦ˢ⟧-idemp Δ j) (⟦ Δ ˢ⟧□ n ⟦Δ⟧ j) , □⟦B⟧)
            ≅⟨ full-eq j M-eq (≅.sym (rew-to-≅ (⟦ˢ⟧-idemp Δ j))) □⟦B⟧ ⟩
                ⟦ M ⟧ₘ j (⟦ Δ ˢ⟧□ n ⟦Δ⟧ j , □⟦B⟧)
            ∎

         where
            ˢ-idemp′ : ∀ Γ -> Γ ˢ ≡ Γ ˢ ˢ
            ˢ-idemp′ Γ = sym (ˢ-idemp Γ)

            ⟦ˢ⟧-idemp : ∀ Δ n -> ⟦ Δ ˢ ⟧ₓ n ≡ ⟦ Δ ˢ ˢ ⟧ₓ n
            ⟦ˢ⟧-idemp Δ n = cong (λ x → ⟦ x ⟧ₓ n) (ˢ-idemp′ Δ)

            rew-lemma : ∀ Δ A n l ⟦Δ⟧ □⟦A⟧
                 -> (rew (cong (λ x → ⟦ x ⟧ₓ l) (ˢ-idemp′ Δ)) (⟦ Δ ˢ⟧□ n ⟦Δ⟧ l) , □⟦A⟧)
                  ≡ rew (cong (λ x → ⟦ x ⟧ₓ l) (ˢ-idemp′ (Δ ,, A always))) (⟦ Δ ˢ⟧□ n ⟦Δ⟧ l , □⟦A⟧)
            rew-lemma Δ A n l ⟦Δ⟧ □⟦A⟧ rewrite ˢ-idemp Δ = refl

            ⟦ˢ⟧-rew : ∀ Δ n l ⟦Δ⟧ -> ⟦ Δ ˢ ˢ⟧ l (⟦ Δ ˢ⟧□ n ⟦Δ⟧ l)
                                  ≡ rew (⟦ˢ⟧-idemp Δ l) (⟦ Δ ˢ⟧□ n ⟦Δ⟧ l)
            ⟦ˢ⟧-rew ∙ n l ⟦Δ⟧ = refl
            ⟦ˢ⟧-rew (Δ ,, A now) n l (⟦Δ⟧ , ⟦A⟧) = ⟦ˢ⟧-rew Δ n l ⟦Δ⟧
            ⟦ˢ⟧-rew (Δ ,, A always) n l (⟦Δ⟧ , □⟦A⟧)
                    rewrite ⟦ˢ⟧-rew Δ n l ⟦Δ⟧
                          | rew-lemma Δ A n l ⟦Δ⟧ □⟦A⟧ = refl

            M-eq : subst (λ x → x ,, B always ⊢ A now) (ˢ-idemp′ Δ) M  ≅ M
            M-eq = ≅.≡-subst-removable (λ x → x ,, B always ⊢ A now) (ˢ-idemp′ Δ) M

            full-eq : ∀ j {M₁ : Δ ˢ ˢ ,, B always ⊢ A now}
                          {M₂ : Δ ˢ ,, B always ⊢ A now}
                          {⟦Δ⟧₁ : ⟦ Δ ˢ ˢ ⟧ₓ j} {⟦Δ⟧₂ : ⟦ Δ ˢ ⟧ₓ j}
                          (p-M : M₁ ≅ M₂) (p-⟦Δ⟧ : ⟦Δ⟧₁ ≅ ⟦Δ⟧₂) □⟦B⟧
                   -> ⟦ M₁ ⟧ₘ j (⟦Δ⟧₁ , □⟦B⟧) ≅ ⟦ M₂ ⟧ₘ j (⟦Δ⟧₂ , □⟦B⟧)
            full-eq j p-M p-⟦Δ⟧ □⟦B⟧ rewrite ˢ-idemp Δ
                    = ≅.cong₂ ((λ x y → ⟦ x ⟧ₘ j (y , □⟦B⟧))) p-M p-⟦Δ⟧

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A larger example for sublists (propositional case):
-- Simply-typed lambda terms with globally unique variables
-- (both bound and free ones).
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables (Base : Set) where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; subst; module ≡-Reasoning)
open ≡-Reasoning

open import Data.List.Base using (List; []; _∷_; [_])
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (Null; [])
open import Data.List.Relation.Binary.Sublist.Propositional using
  ( _⊆_; []; _∷_; _∷ʳ_
  ; ⊆-refl; ⊆-trans; minimum
  ; from∈; to∈; lookup
  ; ⊆-pushoutˡ; RawPushout
  ; Disjoint; DisjointUnion
  ; separateˡ; Separation
  )
open import Data.List.Relation.Binary.Sublist.Propositional.Properties using
  ( ∷ˡ⁻
  ; ⊆-trans-assoc
  ; from∈∘to∈; from∈∘lookup; lookup-⊆-trans
  ; ⊆-pushoutˡ-is-wpo
  ; Disjoint→DisjointUnion; DisjointUnion→Disjoint
  ; Disjoint-sym; DisjointUnion-inj₁; DisjointUnion-inj₂; DisjointUnion-[]ʳ
  ; weakenDisjoint; weakenDisjointUnion; shrinkDisjointˡ
  ; disjoint⇒disjoint-to-union; DisjointUnion-fromAny∘toAny-∷ˡ⁻
  ; equalize-separators
  )

open import Data.Product using (_,_; proj₁; proj₂)

-- Simple types over a set Base of base types.

data Ty : Set where
  base : (o : Base) → Ty
  _⇒_ : (a b : Ty) → Ty

-- Typing contexts are lists of types.

Cxt = List Ty

variable
  a b : Ty
  Γ Δ : Cxt
  x y : a ∈ Γ

-- The familiar intrinsically well-typed formulation of STLC
-- where a de Bruijn index x is a pointer into the context.

module DeBruijn where

  data Tm (Δ : Cxt) : (a : Ty) → Set where
    var : (x : a ∈ Δ) → Tm Δ a
    abs : (t : Tm (a ∷ Δ) b) → Tm Δ (a ⇒ b)
    app : (t : Tm Δ (a ⇒ b)) (u : Tm Δ a) → Tm Δ b

-- We formalize now intrinsically well-typed STLC with
-- named variables that are globally unique, i.e.,
-- each variable can be bound at most once.

-- List of bound variables of a term.

BVars = List Ty

variable
  B    : BVars
  noBV : Null B

-- There is a single global context Γ of all variables used in the terms.
-- Each list of bound variables B is a sublist of Γ.

variable
  β βₜ βᵤ yβ β\y : B ⊆ Γ

-- Named terms are parameterized by a sublist β : B ⊆ Γ of bound variables.
-- Variables outside B can occur as free variables in a term.
--
--   * Variables x do not contain any bound variables (Null B).
--
--   * The bound variables of an application (t u) is the disjoint union
--     of the bound variables βₜ of t and βᵤ of u.
--
--   * The bound variables β of an abstraction λyt is the disjoint union
--     of the single variable y and the bound variables β\y of t.

module UniquelyNamed where

  data Tm (β : B ⊆ Γ) : (a : Ty) → Set where

    var : (noBV : Null B)
          (x : a ∈ Γ)
        → Tm β a

    abs : (y : a ∈ Γ)
          (y# : DisjointUnion (from∈ y) β\y β)
          (t : Tm β\y b)
        → Tm β (a ⇒ b)

    app : (t : Tm βₜ (a ⇒ b))
          (u : Tm βᵤ a)
          (t#u : DisjointUnion βₜ βᵤ β)
        → Tm β b

  pattern var! x = var [] x

  -- Bound variables β : B ⊆ Γ can be considered in a larger context Γ′
  -- obtained by γ : Γ ⊆ Γ′.  The embedding β′ : B ⊆ Γ′ is simply the
  -- composition of β and γ, and terms can be coerced recursively:

  weakenBV : ∀ {Γ B Γ′} {β : B ⊆ Γ} (γ : Γ ⊆ Γ′)  →
          Tm β a → Tm (⊆-trans β γ) a

  weakenBV γ (var noBV x)  = var noBV (lookup γ x)
  weakenBV γ (app t u t#u) = app (weakenBV γ t) (weakenBV γ u) (weakenDisjointUnion γ t#u)
  weakenBV γ (abs y y# t)  = abs y′ y′# (weakenBV γ t)
    where
    y′  = lookup γ y
    -- Typing:  y′# : DisjointUnion (from∈ y′) (⊆-trans β\y γ) (⊆-trans β γ)
    y′# = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#)

-- We bring de Bruijn terms into scope as Exp.

open DeBruijn renaming (Tm to Exp)
open UniquelyNamed

variable
  t u  : Tm β a
  f e  : Exp Δ a

-- Relating de Bruijn terms and uniquely named terms.
--
-- The judgement δ ⊢ e ~ β ▷ t relates a de Bruijn term e with potentially free variables δ : Δ ⊆ Γ
-- to a named term t with exact bound variables β : B ⊆ Γ.  The intention is to relate exactly
-- the terms with the same meaning.
--
-- The judgement will imply the disjointness of Δ and B.

variable
  δ yδ : Δ ⊆ Γ

data _⊢_~_▷_ {Γ Δ : Cxt} (δ : Δ ⊆ Γ) : ∀{a} (e : Exp Δ a) {B} (β : B ⊆ Γ) (t : Tm β a) → Set where

  -- Free de Bruijn index x : a ∈ Δ is related to free variable y : a ∈ Γ
  -- if δ : Δ ⊆ Γ maps x to y.

  var : ∀{y} (δx≡y : lookup δ x ≡ y) (δ#β : Disjoint δ β)
      → δ ⊢ var x ~ β ▷ var! y

  -- Unnamed lambda δ ⊢ λ.e is related to named lambda y,β ▷ λy.t
  -- if body y,δ ⊢ e is related to body β ▷ t.

  abs : (y#δ : DisjointUnion (from∈ y) δ yδ)
      → (y#β : DisjointUnion (from∈ y) β yβ)
      → yδ ⊢ e ~ β ▷ t
      → δ ⊢ abs e ~ yβ ▷ abs y y#β t

  -- Application δ ⊢ f e is related to application βₜ,βᵤ ▷ t u
  -- if function δ ⊢ f is related to βₜ ▷ t
  -- and argument δ ⊢ e is related to βᵤ ▷ u.

  app : δ ⊢ f ~ βₜ ▷ t
      → δ ⊢ e ~ βᵤ ▷ u
      → (t#u : DisjointUnion βₜ βᵤ β)
      → δ ⊢ app f e ~ β ▷ app t u t#u

-- A dependent substitution lemma for ~.
-- Trivial, but needed because term equality t : Tm β a ≡ t′ : Tm β′ a is heterogeneous,
-- or, more precisely, indexed by a sublist equality β ≡ β′.

subst~ : ∀ {a Δ Γ B} {δ δ′ : Δ ⊆ Γ} {β β′ : B ⊆ Γ}
         {e : Exp Δ a} {t : Tm β a} {t′ : Tm β′ a}
         (δ≡δ′ : δ ≡ δ′)
         (β≡β′ : β ≡ β′)
         (t≡t′ : subst (λ □ → Tm □ a) β≡β′ t ≡ t′) →
         δ ⊢ e ~ β ▷ t →
         δ′ ⊢ e ~ β′ ▷ t′
subst~ refl refl refl d = d

-- The judgement δ ⊢ e ~ β ▷ t relative to Γ
-- can be transported to a bigger context γ : Γ ⊆ Γ′.

weaken~ : ∀{a Δ B Γ Γ′} {δ : Δ ⊆ Γ} {β : B ⊆ Γ} {e : Exp Δ a} {t : Tm β a}  (γ : Γ ⊆ Γ′)
  (let δ′ = ⊆-trans δ γ)
  (let β′ = ⊆-trans β γ)
  (let t′ = weakenBV γ t) →
  δ ⊢ e ~ β ▷ t →
  δ′ ⊢ e ~ β′ ▷ t′
weaken~ γ (var refl δ#β)  = var (lookup-⊆-trans γ _) (weakenDisjoint γ δ#β)
weaken~ γ (abs y#δ y#β d) = abs y′#δ′ y′#β′ (weaken~ γ d)
  where
  y′#δ′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#δ)
  y′#β′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#β)
weaken~ γ (app dₜ dᵤ t#u) = app (weaken~ γ dₜ) (weaken~ γ dᵤ) (weakenDisjointUnion γ t#u)

-- Lemma:  If δ ⊢ e ~ β ▷ t, then
-- the (potentially) free variables δ of the de Bruijn term e
-- are disjoint from the bound variables β of the named term t.

disjoint-fv-bv : δ ⊢ e ~ β ▷ t → Disjoint δ β
disjoint-fv-bv (var _ δ#β) = δ#β

disjoint-fv-bv {β = yβ} (abs y⊎δ y⊎β d) = δ#yβ
  where
  δ#y     = Disjoint-sym (DisjointUnion→Disjoint y⊎δ)
  yδ#β    = disjoint-fv-bv d
  δ⊆yδ,eq = DisjointUnion-inj₂ y⊎δ
  δ⊆yδ    = proj₁ δ⊆yδ,eq
  eq      = proj₂ δ⊆yδ,eq
  δ#β     = subst (λ □ → Disjoint □ _) eq (shrinkDisjointˡ δ⊆yδ yδ#β)
  δ#yβ    = disjoint⇒disjoint-to-union δ#y δ#β y⊎β

disjoint-fv-bv (app dₜ dᵤ βₜ⊎βᵤ) = disjoint⇒disjoint-to-union δ#βₜ δ#βᵤ βₜ⊎βᵤ
  where
  δ#βₜ = disjoint-fv-bv dₜ
  δ#βᵤ = disjoint-fv-bv dᵤ

-- Translating de Bruijn terms to uniquely named terms.
--
-- Given a de Bruijn term Δ ⊢ e : a, we seek to produce a named term β ▷ t : a
-- that is related to the de Bruijn term.  On the way, we have to compute the
-- global context Γ that hosts all free and bound variables of t.

-- Record (NamedOf e) collects all the outputs of the translation of e.

record NamedOf (e : Exp Δ a) : Set where
  constructor mkNamedOf
  field
    {glob} : Cxt                    -- Γ
    emb    : Δ ⊆ glob               -- δ : Δ ⊆ Γ
    {bv}   : BVars                  -- B
    bound  : bv ⊆ glob              -- β : B ⊆ Γ
    {tm}   : Tm bound a             -- t : Tm β a
    relate : emb ⊢ e ~ bound ▷ tm   -- δ ⊢ e ~ β ▷ t

-- The translation.

dB→Named : (e : Exp Δ a) → NamedOf e

-- For the translation of a variable x : a ∈ Δ, we can pick Γ := Δ and B := [].
-- Δ and B are obviously disjoint subsets of Γ.

dB→Named (var x) = record
    { emb    = ⊆-refl     -- Γ := Δ
    ; bound  = minimum _  -- no bound variables
    ; relate = var refl (DisjointUnion→Disjoint DisjointUnion-[]ʳ)
    }

-- For the translation of an abstraction
--
--   abs (t : Exp (a ∷ Δ) b) : Exp Δ (a ⇒ b)
--
-- we recursively have Γ, B and β : B ⊆ Γ with z,δ : (a ∷ Δ) ⊆ Γ
-- and know that B # a∷Δ.
--
-- We keep Γ and produce embedding δ : Δ ⊆ Γ and bound variables z ⊎ β.

dB→Named {Δ = Δ} {a = a ⇒ b} (abs e) with dB→Named e
... | record{ glob = Γ; emb = zδ; bound = β; relate = d } =
  record
    { glob   = Γ
    ; emb    = δ̇
    ; bound  = proj₁ (proj₂ z⊎β)
    ; relate = abs [a]⊆Γ⊎δ (proj₂ (proj₂ z⊎β)) d
    }
  where
  -- Typings:
  -- zδ   : a ∷ Δ ⊆ Γ
  -- β    : bv ⊆ Γ
  zδ#β    = disjoint-fv-bv d
  z       : a ∈ Γ
  z       = to∈ zδ
  [a]⊆Γ   = from∈ z
  δ̇       = ∷ˡ⁻ zδ
  [a]⊆Γ⊎δ = DisjointUnion-fromAny∘toAny-∷ˡ⁻ zδ
  [a]⊆aΔ  : [ a ] ⊆ (a ∷ Δ)
  [a]⊆aΔ  = refl ∷ minimum _
  eq      : ⊆-trans [a]⊆aΔ zδ ≡ [a]⊆Γ
  eq      = sym (from∈∘to∈ _)
  z#β     : Disjoint [a]⊆Γ β
  z#β     = subst (λ □ → Disjoint □ β) eq (shrinkDisjointˡ [a]⊆aΔ zδ#β)
  z⊎β     = Disjoint→DisjointUnion z#β

-- For the translation of an application (f e) we have by induction hypothesis
-- two independent extensions δ₁ : Δ ⊆ Γ₁ and δ₂ : Δ ⊆ Γ₂
-- and two bound variable lists β₁ : B₁ ⊆ Γ₁ and β₂ : B₂ ⊆ Γ₂.
-- We need to find a common global context Γ such that
--
--   (a) δ : Δ ⊆ Γ and
--   (b) the bound variables embed disjointly as β₁″ : B₁ ⊆ Γ and β₂″ : B₂ ⊆ Γ.
--
-- (a) δ is (eventually) found via a weak pushout of δ₁ and δ₂, giving
-- ϕ₁ : Γ₁ ⊆ Γ₁₂  and  ϕ₂ : Γ₂ ⊆ Γ₁₂.
--
-- (b) The bound variable embeddings
--
--   β₁′ = β₁ϕ₁ : B₁ ⊆ Γ₁₂ and
--   β₂′ = β₂ϕ₂ : B₂ ⊆ Γ₁₂ and
--
-- may be overlapping, but we can separate them by enlarging the global context
-- to Γ with two embeddings
--
--   γ₁ : Γ₁₂ ⊆ Γ
--   γ₂ : Γ₁₂ ⊆ Γ
--
-- such that
--
--   β₁″ = β₁′γ₁ : B₁ ⊆ Γ
--   β₂″ = β₂′γ₂ : B₂ ⊆ Γ
--
-- are disjoint.  Since Δ is disjoint to both B₁ and B₂ we have equality of
--
--   δ₁ϕ₁γ₁ : Δ ⊆ Γ
--   δ₂ϕ₂γ₂ : Δ ⊆ Γ
--
-- Thus, we can return either of them as δ.

dB→Named (app f e) with dB→Named f | dB→Named e
... | mkNamedOf {Γ₁} δ₁ β₁ {t} d₁ | mkNamedOf {Γ₂} δ₂ β₂ {u} d₂ =
  mkNamedOf δ̇ β̇ (app d₁″ d₂″ β₁″⊎β₂″)
  where
  -- Disjointness of δᵢ and βᵢ from induction hypotheses.
  δ₁#β₁   = disjoint-fv-bv d₁
  δ₂#β₂   = disjoint-fv-bv d₂

  -- join δ₁ and δ₂ via weak pushout
  po      = ⊆-pushoutˡ δ₁ δ₂
  Γ₁₂     = RawPushout.upperBound po
  ϕ₁      = RawPushout.leg₁ po
  ϕ₂      = RawPushout.leg₂ po
  δ₁′     = ⊆-trans δ₁ ϕ₁
  δ₂′     = ⊆-trans δ₂ ϕ₂
  β₁′     = ⊆-trans β₁ ϕ₁
  β₂′     = ⊆-trans β₂ ϕ₂
  δ₁′#β₁′ : Disjoint δ₁′ β₁′
  δ₁′#β₁′ = weakenDisjoint ϕ₁ δ₁#β₁
  δ₂′#β₂′ : Disjoint δ₂′ β₂′
  δ₂′#β₂′ = weakenDisjoint ϕ₂ δ₂#β₂
  δ₁′≡δ₂′ : δ₁′ ≡ δ₂′
  δ₁′≡δ₂′ = ⊆-pushoutˡ-is-wpo δ₁ δ₂
  δ₂′#β₁′ : Disjoint δ₂′ β₁′
  δ₂′#β₁′ = subst (λ □ → Disjoint □ β₁′) δ₁′≡δ₂′ δ₁′#β₁′

  -- separate β₁ and β₂
  sep     : Separation β₁′ β₂′
  sep     = separateˡ β₁′ β₂′
  γ₁      = Separation.separator₁ sep
  γ₂      = Separation.separator₂ sep
  β₁″     = Separation.separated₁ sep
  β₂″     = Separation.separated₂ sep

  -- produce their disjoint union
  uni     = Disjoint→DisjointUnion (Separation.disjoint sep)
  β̇       = proj₁ (proj₂ uni)
  β₁″⊎β₂″ : DisjointUnion β₁″ β₂″ β̇
  β₁″⊎β₂″ = proj₂ (proj₂ uni)
  ι₁      = DisjointUnion-inj₁ β₁″⊎β₂″
  ι₂      = DisjointUnion-inj₂ β₁″⊎β₂″

  -- after separation, the FVs are still disjoint from the BVs.
  δ₁″     = ⊆-trans δ₂′ γ₁
  δ₂″     = ⊆-trans δ₂′ γ₂
  δ₁″≡δ₂″ : δ₁″ ≡ δ₂″
  δ₁″≡δ₂″ = equalize-separators δ₂′#β₁′ δ₂′#β₂′
  δ₁″#β₁″ : Disjoint δ₁″ β₁″
  δ₁″#β₁″ = weakenDisjoint γ₁ δ₂′#β₁′
  δ₂″#β₂″ : Disjoint δ₂″ β₂″
  δ₂″#β₂″ = weakenDisjoint γ₂ δ₂′#β₂′
  δ̇       = δ₂″
  δ₂″#β₁″ : Disjoint δ₂″ β₁″
  δ₂″#β₁″ = subst (λ □ → Disjoint □ β₁″) δ₁″≡δ₂″ δ₁″#β₁″
  δ̇#β̇     : Disjoint δ̇ β̇
  δ̇#β̇     = disjoint⇒disjoint-to-union δ₂″#β₁″ δ₂″#β₂″ β₁″⊎β₂″

  -- Combined weakening from Γᵢ to Γ
  γ₁′     = ⊆-trans ϕ₁ γ₁
  γ₂′     = ⊆-trans ϕ₂ γ₂

  -- Weakening and converting the first derivation.
  d₁′     : ⊆-trans δ₁ γ₁′ ⊢ f ~ ⊆-trans β₁ γ₁′ ▷ weakenBV γ₁′ t
  d₁′     = weaken~ γ₁′ d₁
  δ₁≤δ̇    : ⊆-trans δ₁ γ₁′ ≡ ⊆-trans δ₂′ γ₂
  δ₁≤δ̇    = begin
            ⊆-trans δ₁ γ₁′ ≡⟨ ⊆-trans-assoc ⟩
            ⊆-trans δ₁′ γ₁ ≡⟨ cong (λ □ → ⊆-trans □ γ₁) δ₁′≡δ₂′ ⟩
            ⊆-trans δ₂′ γ₁ ≡⟨⟩
            δ₁″            ≡⟨ δ₁″≡δ₂″ ⟩
            δ₂″            ≡⟨⟩
            δ̇              ∎
  β₁≤β₁″  : ⊆-trans β₁ γ₁′ ≡ β₁″
  β₁≤β₁″  = ⊆-trans-assoc
  d₁″     : δ̇ ⊢ f ~ β₁″ ▷ subst (λ □ → Tm □ _) β₁≤β₁″ (weakenBV γ₁′ t)
  d₁″     =  subst~ δ₁≤δ̇ β₁≤β₁″ refl d₁′

  -- Weakening and converting the second derivation.
  d₂′     : ⊆-trans δ₂ γ₂′ ⊢ e ~ ⊆-trans β₂ γ₂′ ▷ weakenBV γ₂′ u
  d₂′     = weaken~ γ₂′ d₂
  β₂≤β₂″  : ⊆-trans β₂ γ₂′ ≡ β₂″
  β₂≤β₂″  = ⊆-trans-assoc
  δ₂≤δ̇    : ⊆-trans δ₂ γ₂′ ≡ δ̇
  δ₂≤δ̇    = ⊆-trans-assoc
  d₂″     : δ̇ ⊢ e ~ β₂″ ▷ subst (λ □ → Tm □ _) β₂≤β₂″ (weakenBV γ₂′ u)
  d₂″     = subst~ δ₂≤δ̇ β₂≤β₂″ refl d₂′

ext: agda


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

module Properties.TypeNormalization where

open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
open import Luau.Subtyping using (Tree; Language; ¬Language; function; scalar; unknown; left; right; function-ok₁; function-ok₂; function-err; function-tgt; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; function-scalar; _,_)
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize)
open import Luau.Subtyping using (_<:_; _≮:_; witness; never)
open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect;  ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never)

-- Normal forms for types
data FunType : Type → Set
data Normal : Type → Set

data FunType where
  _⇒_ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ T)
  _∩_ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ G)

data Normal where
  _⇒_ : ∀ {S T} → Normal S → Normal T → Normal (S ⇒ T)
  _∩_ : ∀ {F G} → FunType F → FunType G → Normal (F ∩ G)
  _∪_ : ∀ {S T} → Normal S → Scalar T → Normal (S ∪ T)
  never : Normal never
  unknown : Normal unknown

data OptScalar : Type → Set where
  never : OptScalar never
  number : OptScalar number
  boolean : OptScalar boolean
  string : OptScalar string
  nil : OptScalar nil

-- Top function type
fun-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
fun-top (S ⇒ T) = <:-function <:-never <:-unknown
fun-top (F ∩ G) = <:-trans <:-∩-left (fun-top F)

-- function types are inhabited
fun-function : ∀ {F} → FunType F → Language F function
fun-function (S ⇒ T) = function
fun-function (F ∩ G) = (fun-function F , fun-function G)

fun-≮:-never : ∀ {F} → FunType F → (F ≮: never)
fun-≮:-never F = witness function (fun-function F) never

-- function types aren't scalars
fun-¬scalar : ∀ {F S t} → (s : Scalar S) → FunType F → Language F t → ¬Language S t
fun-¬scalar s (S ⇒ T) function = scalar-function s
fun-¬scalar s (S ⇒ T) (function-ok₁ p) = scalar-function-ok s
fun-¬scalar s (S ⇒ T) (function-ok₂ p) = scalar-function-ok s
fun-¬scalar s (S ⇒ T) (function-err p) = scalar-function-err s
fun-¬scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt s
fun-¬scalar s (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂

¬scalar-fun : ∀ {F S} → FunType F → (s : Scalar S) → ¬Language F (scalar s)
¬scalar-fun (S ⇒ T) s = function-scalar s
¬scalar-fun (F ∩ G) s = left (¬scalar-fun F s)

scalar-≮:-fun : ∀ {F S} → FunType F → Scalar S → S ≮: F
scalar-≮:-fun F s = witness (scalar s) (scalar s) (¬scalar-fun F s)

unknown-≮:-fun : ∀ {F} → FunType F → unknown ≮: F
unknown-≮:-fun F = witness (scalar nil) unknown (¬scalar-fun F nil)

-- Normalization produces normal types
normal : ∀ T → Normal (normalize T)
normalᶠ : ∀ {F} → FunType F → Normal F
normal-∪ⁿ : ∀ {S T} → Normal S → Normal T → Normal (S ∪ⁿ T)
normal-∩ⁿ : ∀ {S T} → Normal S → Normal T → Normal (S ∩ⁿ T)
normal-∪ⁿˢ : ∀ {S T} → Normal S → OptScalar T → Normal (S ∪ⁿˢ T)
normal-∩ⁿˢ : ∀ {S T} → Normal S → Scalar T → OptScalar (S ∩ⁿˢ T)
normal-∪ᶠ : ∀ {F G} → FunType F → FunType G → FunType (F ∪ᶠ G)

normal nil = never ∪ nil
normal (S ⇒ T) = (normal S) ⇒ (normal T)
normal never = never
normal unknown = unknown
normal boolean = never ∪ boolean
normal number = never ∪ number
normal string = never ∪ string
normal (S ∪ T) = normal-∪ⁿ (normal S) (normal T)
normal (S ∩ T) = normal-∩ⁿ (normal S) (normal T)

normalᶠ (S ⇒ T) = S ⇒ T
normalᶠ (F ∩ G) = F ∩ G

normal-∪ⁿ S (T₁ ∪ T₂) = (normal-∪ⁿ S T₁) ∪ T₂
normal-∪ⁿ S never = S
normal-∪ⁿ S unknown = unknown
normal-∪ⁿ never (T ⇒ U) = T ⇒ U
normal-∪ⁿ never (G₁ ∩ G₂) = G₁ ∩ G₂
normal-∪ⁿ unknown (T ⇒ U) = unknown
normal-∪ⁿ unknown (G₁ ∩ G₂) = unknown
normal-∪ⁿ (R ⇒ S) (T ⇒ U) = normalᶠ (normal-∪ᶠ (R ⇒ S) (T ⇒ U))
normal-∪ⁿ (R ⇒ S) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂))
normal-∪ⁿ (F₁ ∩ F₂) (T ⇒ U) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (T ⇒ U))
normal-∪ⁿ (F₁ ∩ F₂) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂))
normal-∪ⁿ (S₁ ∪ S₂) (T₁ ⇒ T₂) = normal-∪ⁿ S₁ (T₁ ⇒ T₂) ∪ S₂
normal-∪ⁿ (S₁ ∪ S₂) (G₁ ∩ G₂) = normal-∪ⁿ S₁ (G₁ ∩ G₂) ∪ S₂

normal-∩ⁿ S never = never
normal-∩ⁿ S unknown = S
normal-∩ⁿ S (T ∪ U) = normal-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U )
normal-∩ⁿ never (T ⇒ U) = never
normal-∩ⁿ unknown (T ⇒ U) = T ⇒ U
normal-∩ⁿ (R ⇒ S) (T ⇒ U) = (R ⇒ S) ∩ (T ⇒ U)
normal-∩ⁿ (R ∩ S) (T ⇒ U) = (R ∩ S) ∩ (T ⇒ U)
normal-∩ⁿ (R ∪ S) (T ⇒ U) = normal-∩ⁿ R (T ⇒ U)
normal-∩ⁿ never (T ∩ U) = never
normal-∩ⁿ unknown (T ∩ U) = T ∩ U
normal-∩ⁿ (R ⇒ S) (T ∩ U) = (R ⇒ S) ∩ (T ∩ U)
normal-∩ⁿ (R ∩ S) (T ∩ U) = (R ∩ S) ∩ (T ∩ U)
normal-∩ⁿ (R ∪ S) (T ∩ U) = normal-∩ⁿ R (T ∩ U)

normal-∪ⁿˢ S never = S
normal-∪ⁿˢ never number = never ∪ number
normal-∪ⁿˢ unknown number = unknown
normal-∪ⁿˢ (R ⇒ S) number = (R ⇒ S) ∪ number
normal-∪ⁿˢ (R ∩ S) number = (R ∩ S) ∪ number
normal-∪ⁿˢ (R ∪ number) number = R ∪ number
normal-∪ⁿˢ (R ∪ boolean) number = normal-∪ⁿˢ R number ∪ boolean
normal-∪ⁿˢ (R ∪ string) number = normal-∪ⁿˢ R number ∪ string
normal-∪ⁿˢ (R ∪ nil) number = normal-∪ⁿˢ R number ∪ nil
normal-∪ⁿˢ never boolean = never ∪ boolean
normal-∪ⁿˢ unknown boolean = unknown
normal-∪ⁿˢ (R ⇒ S) boolean = (R ⇒ S) ∪ boolean
normal-∪ⁿˢ (R ∩ S) boolean = (R ∩ S) ∪ boolean
normal-∪ⁿˢ (R ∪ number) boolean = normal-∪ⁿˢ R boolean ∪ number
normal-∪ⁿˢ (R ∪ boolean) boolean = R ∪ boolean
normal-∪ⁿˢ (R ∪ string) boolean = normal-∪ⁿˢ R boolean ∪ string
normal-∪ⁿˢ (R ∪ nil) boolean = normal-∪ⁿˢ R boolean ∪ nil
normal-∪ⁿˢ never string = never ∪ string
normal-∪ⁿˢ unknown string = unknown
normal-∪ⁿˢ (R ⇒ S) string = (R ⇒ S) ∪ string
normal-∪ⁿˢ (R ∩ S) string = (R ∩ S) ∪ string
normal-∪ⁿˢ (R ∪ number) string = normal-∪ⁿˢ R string ∪ number
normal-∪ⁿˢ (R ∪ boolean) string = normal-∪ⁿˢ R string ∪ boolean
normal-∪ⁿˢ (R ∪ string) string = R ∪ string
normal-∪ⁿˢ (R ∪ nil) string = normal-∪ⁿˢ R string ∪ nil
normal-∪ⁿˢ never nil = never ∪ nil
normal-∪ⁿˢ unknown nil = unknown
normal-∪ⁿˢ (R ⇒ S) nil = (R ⇒ S) ∪ nil
normal-∪ⁿˢ (R ∩ S) nil = (R ∩ S) ∪ nil
normal-∪ⁿˢ (R ∪ number) nil = normal-∪ⁿˢ R nil ∪ number
normal-∪ⁿˢ (R ∪ boolean) nil = normal-∪ⁿˢ R nil ∪ boolean
normal-∪ⁿˢ (R ∪ string) nil = normal-∪ⁿˢ R nil ∪ string
normal-∪ⁿˢ (R ∪ nil) nil = R ∪ nil

normal-∩ⁿˢ never number = never
normal-∩ⁿˢ never boolean = never
normal-∩ⁿˢ never string = never
normal-∩ⁿˢ never nil = never
normal-∩ⁿˢ unknown number = number
normal-∩ⁿˢ unknown boolean = boolean
normal-∩ⁿˢ unknown string = string
normal-∩ⁿˢ unknown nil = nil
normal-∩ⁿˢ (R ⇒ S) number = never
normal-∩ⁿˢ (R ⇒ S) boolean = never
normal-∩ⁿˢ (R ⇒ S) string = never
normal-∩ⁿˢ (R ⇒ S) nil = never
normal-∩ⁿˢ (R ∩ S) number = never
normal-∩ⁿˢ (R ∩ S) boolean = never
normal-∩ⁿˢ (R ∩ S) string = never
normal-∩ⁿˢ (R ∩ S) nil = never
normal-∩ⁿˢ (R ∪ number) number = number
normal-∩ⁿˢ (R ∪ boolean) number = normal-∩ⁿˢ R number
normal-∩ⁿˢ (R ∪ string) number = normal-∩ⁿˢ R number
normal-∩ⁿˢ (R ∪ nil) number = normal-∩ⁿˢ R number
normal-∩ⁿˢ (R ∪ number) boolean = normal-∩ⁿˢ R boolean
normal-∩ⁿˢ (R ∪ boolean) boolean = boolean
normal-∩ⁿˢ (R ∪ string) boolean = normal-∩ⁿˢ R boolean
normal-∩ⁿˢ (R ∪ nil) boolean = normal-∩ⁿˢ R boolean
normal-∩ⁿˢ (R ∪ number) string = normal-∩ⁿˢ R string
normal-∩ⁿˢ (R ∪ boolean) string = normal-∩ⁿˢ R string
normal-∩ⁿˢ (R ∪ string) string = string
normal-∩ⁿˢ (R ∪ nil) string = normal-∩ⁿˢ R string
normal-∩ⁿˢ (R ∪ number) nil = normal-∩ⁿˢ R nil
normal-∩ⁿˢ (R ∪ boolean) nil = normal-∩ⁿˢ R nil
normal-∩ⁿˢ (R ∪ string) nil = normal-∩ⁿˢ R nil
normal-∩ⁿˢ (R ∪ nil) nil = nil

normal-∪ᶠ (R ⇒ S) (T ⇒ U) = (normal-∩ⁿ R T) ⇒ (normal-∪ⁿ S U)
normal-∪ᶠ (R ⇒ S) (G ∩ H) = normal-∪ᶠ (R ⇒ S) G ∩ normal-∪ᶠ (R ⇒ S) H
normal-∪ᶠ (E ∩ F) G = normal-∪ᶠ E G ∩ normal-∪ᶠ F G

scalar-∩-fun-<:-never : ∀ {F S} → FunType F → Scalar S → (F ∩ S) <: never
scalar-∩-fun-<:-never (T ⇒ U) S = scalar-∩-function-<:-never S
scalar-∩-fun-<:-never (F ∩ G) S = <:-trans (<:-intersect <:-∩-left <:-refl) (scalar-∩-fun-<:-never F S)

flipper : ∀ {S T U} → ((S ∪ T) ∪ U) <: ((S ∪ U) ∪ T)
flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪-assocl)

∩-<:-∩ⁿ :  ∀ {S T} → Normal S → Normal T → (S ∩ T) <: (S ∩ⁿ T)
∩ⁿ-<:-∩ :  ∀ {S T} → Normal S → Normal T → (S ∩ⁿ T) <: (S ∩ T)
∩-<:-∩ⁿˢ :  ∀ {S T} → Normal S → Scalar T → (S ∩ T) <: (S ∩ⁿˢ T)
∩ⁿˢ-<:-∩ :  ∀ {S T} → Normal S → Scalar T → (S ∩ⁿˢ T) <: (S ∩ T)
∪ᶠ-<:-∪ : ∀ {F G} → FunType F → FunType G → (F ∪ᶠ G) <: (F ∪ G)
∪ⁿ-<:-∪ : ∀ {S T} → Normal S → Normal T → (S ∪ⁿ T) <: (S ∪ T)
∪-<:-∪ⁿ : ∀ {S T} → Normal S → Normal T → (S ∪ T) <: (S ∪ⁿ T)
∪ⁿˢ-<:-∪ : ∀ {S T} → Normal S → OptScalar T → (S ∪ⁿˢ T) <: (S ∪ T)
∪-<:-∪ⁿˢ : ∀ {S T} → Normal S → OptScalar T → (S ∪ T) <: (S ∪ⁿˢ T)

∩-<:-∩ⁿ S never = <:-∩-right
∩-<:-∩ⁿ S unknown = <:-∩-left
∩-<:-∩ⁿ S (T ∪ U) = <:-trans <:-∩-distl-∪ (<:-trans (<:-union (∩-<:-∩ⁿ S T) (∩-<:-∩ⁿˢ S U)) (∪-<:-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) )
∩-<:-∩ⁿ never (T ⇒ U) = <:-∩-left
∩-<:-∩ⁿ unknown (T ⇒ U) = <:-∩-right
∩-<:-∩ⁿ (R ⇒ S) (T ⇒ U) = <:-refl
∩-<:-∩ⁿ (R ∩ S) (T ⇒ U) = <:-refl
∩-<:-∩ⁿ (R ∪ S) (T ⇒ U) = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R (T ⇒ U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T ⇒ U) S))) (<:-∪-lub <:-refl <:-never))
∩-<:-∩ⁿ never (T ∩ U) = <:-∩-left
∩-<:-∩ⁿ unknown (T ∩ U) = <:-∩-right
∩-<:-∩ⁿ (R ⇒ S) (T ∩ U) = <:-refl
∩-<:-∩ⁿ (R ∩ S) (T ∩ U) = <:-refl
∩-<:-∩ⁿ (R ∪ S) (T ∩ U) = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R (T ∩ U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T ∩ U) S))) (<:-∪-lub <:-refl <:-never))

∩ⁿ-<:-∩ S never = <:-never
∩ⁿ-<:-∩ S unknown = <:-∩-glb <:-refl <:-unknown
∩ⁿ-<:-∩ S (T ∪ U) = <:-trans (∪ⁿˢ-<:-∪ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) (<:-trans (<:-union (∩ⁿ-<:-∩ S T) (∩ⁿˢ-<:-∩ S U)) ∩-distl-∪-<:)
∩ⁿ-<:-∩ never (T ⇒ U) = <:-never
∩ⁿ-<:-∩ unknown (T ⇒ U) = <:-∩-glb <:-unknown <:-refl
∩ⁿ-<:-∩ (R ⇒ S) (T ⇒ U) = <:-refl
∩ⁿ-<:-∩ (R ∩ S) (T ⇒ U) = <:-refl
∩ⁿ-<:-∩ (R ∪ S) (T ⇒ U) = <:-trans (∩ⁿ-<:-∩ R (T ⇒ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right)
∩ⁿ-<:-∩ never (T ∩ U) = <:-never
∩ⁿ-<:-∩ unknown (T ∩ U) = <:-∩-glb <:-unknown <:-refl
∩ⁿ-<:-∩ (R ⇒ S) (T ∩ U) = <:-refl
∩ⁿ-<:-∩ (R ∩ S) (T ∩ U) = <:-refl
∩ⁿ-<:-∩ (R ∪ S) (T ∩ U) = <:-trans (∩ⁿ-<:-∩ R (T ∩ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right)

∩-<:-∩ⁿˢ never number = <:-∩-left
∩-<:-∩ⁿˢ never boolean = <:-∩-left
∩-<:-∩ⁿˢ never string = <:-∩-left
∩-<:-∩ⁿˢ never nil = <:-∩-left
∩-<:-∩ⁿˢ unknown T = <:-∩-right
∩-<:-∩ⁿˢ (R ⇒ S) T = scalar-∩-fun-<:-never (R ⇒ S) T
∩-<:-∩ⁿˢ (F ∩ G) T = scalar-∩-fun-<:-never (F ∩ G) T
∩-<:-∩ⁿˢ (R ∪ number) number = <:-∩-right
∩-<:-∩ⁿˢ (R ∪ boolean) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never boolean number (λ ())))
∩-<:-∩ⁿˢ (R ∪ string) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never string number (λ ())))
∩-<:-∩ⁿˢ (R ∪ nil) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never nil number (λ ())))
∩-<:-∩ⁿˢ (R ∪ number) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never number boolean (λ ())))
∩-<:-∩ⁿˢ (R ∪ boolean) boolean = <:-∩-right
∩-<:-∩ⁿˢ (R ∪ string) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never string boolean (λ ())))
∩-<:-∩ⁿˢ (R ∪ nil) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never nil boolean (λ ())))
∩-<:-∩ⁿˢ (R ∪ number) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never number string (λ ())))
∩-<:-∩ⁿˢ (R ∪ boolean) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never boolean string (λ ())))
∩-<:-∩ⁿˢ (R ∪ string) string = <:-∩-right
∩-<:-∩ⁿˢ (R ∪ nil) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never nil string (λ ())))
∩-<:-∩ⁿˢ (R ∪ number) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never number nil (λ ())))
∩-<:-∩ⁿˢ (R ∪ boolean) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never boolean nil (λ ())))
∩-<:-∩ⁿˢ (R ∪ string) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never string nil (λ ())))
∩-<:-∩ⁿˢ (R ∪ nil) nil = <:-∩-right

∩ⁿˢ-<:-∩ never T = <:-never
∩ⁿˢ-<:-∩ unknown T = <:-∩-glb <:-unknown <:-refl
∩ⁿˢ-<:-∩ (R ⇒ S) T = <:-never
∩ⁿˢ-<:-∩ (F ∩ G) T = <:-never
∩ⁿˢ-<:-∩ (R ∪ number) number = <:-∩-glb <:-∪-right <:-refl
∩ⁿˢ-<:-∩ (R ∪ boolean) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ string) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ nil) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ number) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ boolean) boolean = <:-∩-glb <:-∪-right <:-refl
∩ⁿˢ-<:-∩ (R ∪ string) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ nil) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ number) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ boolean) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ string) string = <:-∩-glb <:-∪-right <:-refl
∩ⁿˢ-<:-∩ (R ∪ nil) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ number) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ boolean) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ string) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ nil) nil = <:-∩-glb <:-∪-right <:-refl

∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U) = <:-trans (<:-function (∩-<:-∩ⁿ R T) (∪ⁿ-<:-∪ S U)) <:-function-∪-∩
∪ᶠ-<:-∪ (R ⇒ S) (G ∩ H) = <:-trans (<:-intersect (∪ᶠ-<:-∪ (R ⇒ S) G) (∪ᶠ-<:-∪ (R ⇒ S) H)) ∪-distl-∩-<:
∪ᶠ-<:-∪ (E ∩ F) G = <:-trans (<:-intersect (∪ᶠ-<:-∪ E G) (∪ᶠ-<:-∪ F G)) ∪-distr-∩-<:

∪-<:-∪ᶠ : ∀ {F G} → FunType F → FunType G → (F ∪ G) <: (F ∪ᶠ G)
∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∪ (<:-function (∩ⁿ-<:-∩ R T) (∪-<:-∪ⁿ S U))
∪-<:-∪ᶠ (R ⇒ S) (G ∩ H) = <:-trans <:-∪-distl-∩ (<:-intersect (∪-<:-∪ᶠ (R ⇒ S) G) (∪-<:-∪ᶠ (R ⇒ S) H))
∪-<:-∪ᶠ (E ∩ F) G = <:-trans <:-∪-distr-∩ (<:-intersect (∪-<:-∪ᶠ E G) (∪-<:-∪ᶠ F G))

∪ⁿˢ-<:-∪ S never = <:-∪-left
∪ⁿˢ-<:-∪ never number = <:-refl
∪ⁿˢ-<:-∪ never boolean = <:-refl
∪ⁿˢ-<:-∪ never string = <:-refl
∪ⁿˢ-<:-∪ never nil = <:-refl
∪ⁿˢ-<:-∪ unknown number = <:-∪-left
∪ⁿˢ-<:-∪ unknown boolean = <:-∪-left
∪ⁿˢ-<:-∪ unknown string = <:-∪-left
∪ⁿˢ-<:-∪ unknown nil = <:-∪-left
∪ⁿˢ-<:-∪ (R ⇒ S) number = <:-refl
∪ⁿˢ-<:-∪ (R ⇒ S) boolean = <:-refl
∪ⁿˢ-<:-∪ (R ⇒ S) string = <:-refl
∪ⁿˢ-<:-∪ (R ⇒ S) nil = <:-refl
∪ⁿˢ-<:-∪ (R ∩ S) number = <:-refl
∪ⁿˢ-<:-∪ (R ∩ S) boolean = <:-refl
∪ⁿˢ-<:-∪ (R ∩ S) string = <:-refl
∪ⁿˢ-<:-∪ (R ∩ S) nil = <:-refl
∪ⁿˢ-<:-∪ (R ∪ number) number = <:-union <:-∪-left <:-refl
∪ⁿˢ-<:-∪ (R ∪ boolean) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ string) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ nil) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ number) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ boolean) boolean = <:-union <:-∪-left <:-refl
∪ⁿˢ-<:-∪ (R ∪ string) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ nil) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ number) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ boolean) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ string) string = <:-union <:-∪-left <:-refl
∪ⁿˢ-<:-∪ (R ∪ nil) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ number) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ boolean) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ string) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ nil) nil = <:-union <:-∪-left <:-refl

∪-<:-∪ⁿˢ T never = <:-∪-lub <:-refl <:-never
∪-<:-∪ⁿˢ never number = <:-refl
∪-<:-∪ⁿˢ never boolean = <:-refl
∪-<:-∪ⁿˢ never string = <:-refl
∪-<:-∪ⁿˢ never nil = <:-refl
∪-<:-∪ⁿˢ unknown number = <:-unknown
∪-<:-∪ⁿˢ unknown boolean = <:-unknown
∪-<:-∪ⁿˢ unknown string = <:-unknown
∪-<:-∪ⁿˢ unknown nil = <:-unknown
∪-<:-∪ⁿˢ (R ⇒ S) number = <:-refl
∪-<:-∪ⁿˢ (R ⇒ S) boolean = <:-refl
∪-<:-∪ⁿˢ (R ⇒ S) string = <:-refl
∪-<:-∪ⁿˢ (R ⇒ S) nil = <:-refl
∪-<:-∪ⁿˢ (R ∩ S) number = <:-refl
∪-<:-∪ⁿˢ (R ∩ S) boolean = <:-refl
∪-<:-∪ⁿˢ (R ∩ S) string = <:-refl
∪-<:-∪ⁿˢ (R ∩ S) nil = <:-refl
∪-<:-∪ⁿˢ (R ∪ number) number = <:-∪-lub <:-refl <:-∪-right
∪-<:-∪ⁿˢ (R ∪ boolean) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
∪-<:-∪ⁿˢ (R ∪ string) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
∪-<:-∪ⁿˢ (R ∪ nil) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
∪-<:-∪ⁿˢ (R ∪ number) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
∪-<:-∪ⁿˢ (R ∪ boolean) boolean = <:-∪-lub <:-refl <:-∪-right
∪-<:-∪ⁿˢ (R ∪ string) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
∪-<:-∪ⁿˢ (R ∪ nil) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
∪-<:-∪ⁿˢ (R ∪ number) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
∪-<:-∪ⁿˢ (R ∪ boolean) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
∪-<:-∪ⁿˢ (R ∪ string) string = <:-∪-lub <:-refl <:-∪-right
∪-<:-∪ⁿˢ (R ∪ nil) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
∪-<:-∪ⁿˢ (R ∪ number) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
∪-<:-∪ⁿˢ (R ∪ boolean) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
∪-<:-∪ⁿˢ (R ∪ string) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
∪-<:-∪ⁿˢ (R ∪ nil) nil = <:-∪-lub <:-refl <:-∪-right

∪ⁿ-<:-∪ S never = <:-∪-left
∪ⁿ-<:-∪ S unknown = <:-∪-right
∪ⁿ-<:-∪ never (T ⇒ U) = <:-∪-right
∪ⁿ-<:-∪ unknown (T ⇒ U) = <:-∪-left
∪ⁿ-<:-∪ (R ⇒ S) (T ⇒ U) = ∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U)
∪ⁿ-<:-∪ (R ∩ S) (T ⇒ U) = ∪ᶠ-<:-∪ (R ∩ S) (T ⇒ U)
∪ⁿ-<:-∪ (R ∪ S) (T ⇒ U) = <:-trans (<:-union (∪ⁿ-<:-∪ R (T ⇒ U)) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left))
∪ⁿ-<:-∪ never (T ∩ U) = <:-∪-right
∪ⁿ-<:-∪ unknown (T ∩ U) = <:-∪-left
∪ⁿ-<:-∪ (R ⇒ S) (T ∩ U) = ∪ᶠ-<:-∪ (R ⇒ S) (T ∩ U)
∪ⁿ-<:-∪ (R ∩ S) (T ∩ U) = ∪ᶠ-<:-∪ (R ∩ S) (T ∩ U)
∪ⁿ-<:-∪ (R ∪ S) (T ∩ U) = <:-trans (<:-union (∪ⁿ-<:-∪ R (T ∩ U)) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left))
∪ⁿ-<:-∪ S (T ∪ U) = <:-∪-lub (<:-trans (∪ⁿ-<:-∪ S T) (<:-union <:-refl <:-∪-left)) (<:-trans <:-∪-right <:-∪-right)

∪-<:-∪ⁿ S never = <:-∪-lub <:-refl <:-never
∪-<:-∪ⁿ S unknown = <:-unknown
∪-<:-∪ⁿ never (T ⇒ U) = <:-∪-lub <:-never <:-refl
∪-<:-∪ⁿ unknown (T ⇒ U) = <:-unknown
∪-<:-∪ⁿ (R ⇒ S) (T ⇒ U) = ∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U)
∪-<:-∪ⁿ (R ∩ S) (T ⇒ U) = ∪-<:-∪ᶠ (R ∩ S) (T ⇒ U)
∪-<:-∪ⁿ (R ∪ S) (T ⇒ U) = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R (T ⇒ U)) <:-refl)))
∪-<:-∪ⁿ never (T ∩ U) = <:-∪-lub <:-never <:-refl
∪-<:-∪ⁿ unknown (T ∩ U) = <:-unknown
∪-<:-∪ⁿ (R ⇒ S) (T ∩ U) = ∪-<:-∪ᶠ (R ⇒ S) (T ∩ U)
∪-<:-∪ⁿ (R ∩ S) (T ∩ U) = ∪-<:-∪ᶠ (R ∩ S) (T ∩ U)
∪-<:-∪ⁿ (R ∪ S) (T ∩ U) = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R (T ∩ U)) <:-refl)))
∪-<:-∪ⁿ never (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ never T) <:-refl)
∪-<:-∪ⁿ unknown (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ unknown T) <:-refl)
∪-<:-∪ⁿ (R ⇒ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ⇒ S) T) <:-refl)
∪-<:-∪ⁿ (R ∩ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ∩ S) T) <:-refl)
∪-<:-∪ⁿ (R ∪ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ∪ S) T) <:-refl)

normalize-<: : ∀ T → normalize T <: T
<:-normalize : ∀ T → T <: normalize T

<:-normalize nil = <:-∪-right
<:-normalize (S ⇒ T) = <:-function (normalize-<: S) (<:-normalize T)
<:-normalize never = <:-refl
<:-normalize unknown = <:-refl
<:-normalize boolean = <:-∪-right
<:-normalize number = <:-∪-right
<:-normalize string = <:-∪-right
<:-normalize (S ∪ T) = <:-trans (<:-union (<:-normalize S) (<:-normalize T)) (∪-<:-∪ⁿ (normal S) (normal T))
<:-normalize (S ∩ T) = <:-trans (<:-intersect (<:-normalize S) (<:-normalize T)) (∩-<:-∩ⁿ (normal S) (normal T))

normalize-<: nil = <:-∪-lub <:-never <:-refl
normalize-<: (S ⇒ T) = <:-function (<:-normalize S) (normalize-<: T)
normalize-<: never = <:-refl
normalize-<: unknown = <:-refl
normalize-<: boolean = <:-∪-lub <:-never <:-refl
normalize-<: number = <:-∪-lub <:-never <:-refl
normalize-<: string = <:-∪-lub <:-never <:-refl
normalize-<: (S ∪ T) = <:-trans (∪ⁿ-<:-∪ (normal S) (normal T)) (<:-union (normalize-<: S) (normalize-<: T))
normalize-<: (S ∩ T) = <:-trans (∩ⁿ-<:-∩ (normal S) (normal T)) (<:-intersect (normalize-<: S) (normalize-<: T))

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


text:
-- Soundness proofs of structural lemmas and substitution
module Semantics.Substitution.Soundness where

open import Syntax.Types
open import Syntax.Context renaming (_,_ to _,,_)
open import Syntax.Terms
open import Syntax.Substitution.Kits
open import Syntax.Substitution.Instances
open import Syntax.Substitution.Lemmas

open import Semantics.Types
open import Semantics.Context
open import Semantics.Terms
open import Semantics.Substitution.Kits
open import Semantics.Substitution.Traversal
open import Semantics.Substitution.Instances
open import Semantics.Bind

open import CategoryTheory.Categories using (Category ; ext)
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad
open import CategoryTheory.Comonad
open import CategoryTheory.Linear
open import CategoryTheory.Instances.Reactive renaming (top to ⊤)
open import TemporalOps.Diamond
open import TemporalOps.Box
open import TemporalOps.OtherOps
open import TemporalOps.StrongMonad
open import TemporalOps.Linear

open import Data.Sum
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality as ≡
    using (_≡_ ; refl ; sym ; trans ; cong ; cong₂ ; subst)

open ≡.≡-Reasoning
open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

open ⟦K⟧ ⟦𝒯erm⟧

-- | Interpretation of various types of substitution as context morphisms

-- Denotation of term substitutions
⟦_⟧ₛ : ∀{Γ Δ} -> Subst Term Γ Δ -> ⟦ Δ ⟧ₓ ⇴ ⟦ Γ ⟧ₓ
⟦ σ ⟧ₛ = ⟦subst⟧ σ

-- Denotation of OPEs
⟦_⟧⊆ : ∀{Γ Δ} -> Γ ⊆ Δ -> ⟦ Δ ⟧ₓ ⇴ ⟦ Γ ⟧ₓ
⟦ s ⟧⊆ = ⟦ s ⊆ₛ 𝒯erm ⟧ₛ

-- Denotation of context exchange
⟦exch⟧ : ∀ Γ Γ′ Γ″ {A B} -> ⟦ Γ ⌊ B ⌋ Γ′ ⌊ A ⌋ Γ″ ⟧ₓ ⇴ ⟦ Γ ⌊ A ⌋ Γ′ ⌊ B ⌋ Γ″ ⟧ₓ
⟦exch⟧ Γ Γ′ Γ″ = ⟦ exₛ 𝒯ermₛ Γ Γ′ Γ″ ⟧ₛ

-- Denotation of context contraction
⟦contr⟧ : ∀ Γ Γ′ Γ″ {A} -> ⟦ Γ ⌊ A ⌋ Γ′ ⌊⌋ Γ″ ⟧ₓ ⇴ ⟦ Γ ⌊ A ⌋ Γ′ ⌊ A ⌋ Γ″ ⟧ₓ
⟦contr⟧ Γ Γ′ Γ″ = ⟦ contr-lₛ 𝒯ermₛ Γ Γ′ Γ″ ⟧ₛ

-- Denotation of middle context substitution
⟦_⌊⌋ₛ_⊢ₛ_⟧ : ∀ Γ Γ′ {A} -> Γ ⌊⌋ Γ′ ⊢ A -> ⟦ Γ ⌊⌋ Γ′ ⟧ₓ ⇴ ⟦ Γ ⌊ A ⌋ Γ′ ⟧ₓ
⟦ Γ ⌊⌋ₛ Γ′ ⊢ₛ M ⟧ = ⟦ sub-midₛ 𝒯ermₛ Γ Γ′ M ⟧ₛ

-- Denotational soundness of top substitution
⟦sub-topₛ⟧ : ∀ {Γ A} -> (M : Γ ⊢ A)
        -> ⟦ sub-topₛ 𝒯ermₛ M ⟧ₛ ≈ ⟨ id , ⟦ M ⟧ₘ ⟩
⟦sub-topₛ⟧ {Γ} M {n} {⟦Γ⟧} rewrite ⟦idₛ⟧ {Γ} {n} {⟦Γ⟧} = refl

-- | Soundness theorems
-- | Concrete soundness theorems for structural lemmas and substitution
-- | are instances of the general traversal soundness proof

-- Substituting traversal is sound
substitute-sound : ∀{Γ Δ A} (σ : Subst Term Γ Δ) (M : Γ ⊢ A)
                -> ⟦ substitute σ M ⟧ₘ ≈ ⟦ M ⟧ₘ ∘ ⟦ σ ⟧ₛ
substitute-sound σ M = traverse-sound ⟦𝒯erm⟧ σ M

substitute′-sound : ∀{Γ Δ A} (σ : Subst Term Γ Δ) (M : Γ ⊨ A)
                -> ⟦ substitute′ σ M ⟧ᵐ ≈ ⟦ M ⟧ᵐ ∘ ⟦ σ ⟧ₛ
substitute′-sound σ M = traverse′-sound ⟦𝒯erm⟧ σ M

-- Weakening lemma is sound
weakening-sound : ∀{Γ Δ A} (s : Γ ⊆ Δ) (M : Γ ⊢ A)
               -> ⟦ weakening s M ⟧ₘ ≈ ⟦ M ⟧ₘ ∘ ⟦ s ⟧⊆
weakening-sound s = substitute-sound (s ⊆ₛ 𝒯erm)

-- Exchange lemma is sound
exchange-sound : ∀{Γ Γ′ Γ″ A B C} (M : Γ ⌊ A ⌋ Γ′ ⌊ B ⌋ Γ″ ⊢ C)
              -> ⟦ exchange Γ Γ′ Γ″ M ⟧ₘ ≈ ⟦ M ⟧ₘ ∘ (⟦exch⟧ Γ Γ′ Γ″)
exchange-sound {Γ} {Γ′} {Γ″} = substitute-sound (exₛ 𝒯ermₛ Γ Γ′ Γ″)

-- Contraction lemma is sound
contraction-sound : ∀{Γ Γ′ Γ″ A B} (M : Γ ⌊ A ⌋ Γ′ ⌊ A ⌋ Γ″ ⊢ B)
                 -> ⟦ contraction Γ Γ′ Γ″ M ⟧ₘ ≈ ⟦ M ⟧ₘ ∘ (⟦contr⟧ Γ Γ′ Γ″)
contraction-sound {Γ} {Γ′} {Γ″} = substitute-sound (contr-lₛ 𝒯ermₛ Γ Γ′ Γ″)

-- Substitution lemma is sound
substitution-sound : ∀{Γ Γ′ A B} (M : Γ ⌊⌋ Γ′ ⊢ A) (N : Γ ⌊ A ⌋ Γ′ ⊢ B)
                 -> ⟦ substitution Γ Γ′ M N ⟧ₘ ≈ ⟦ N ⟧ₘ ∘ ⟦ Γ ⌊⌋ₛ Γ′ ⊢ₛ M ⟧
substitution-sound {Γ} {Γ′} M = substitute-sound (sub-midₛ 𝒯ermₛ Γ Γ′ M)

-- Substitution lemma is sound
substitution′-sound : ∀{Γ Γ′ A B} (M : Γ ⌊⌋ Γ′ ⊢ A) (N : Γ ⌊ A ⌋ Γ′ ⊨ B)
                 -> ⟦ substitution′ Γ Γ′ M N ⟧ᵐ ≈ ⟦ N ⟧ᵐ ∘ ⟦ Γ ⌊⌋ₛ Γ′ ⊢ₛ M ⟧
substitution′-sound {Γ} {Γ′} M N = traverse′-sound ⟦𝒯erm⟧ (sub-midₛ 𝒯ermₛ Γ Γ′ M) N

-- Top substitution is sound (full categorical proof)
subst-sound : ∀{Γ A B} (M : Γ ⊢ A) (N : Γ ,, A ⊢ B)
           -> ⟦ [ M /] N ⟧ₘ ≈ ⟦ N ⟧ₘ ∘ ⟨ id , ⟦ M ⟧ₘ ⟩
subst-sound M N {n} {a} rewrite sym (⟦sub-topₛ⟧ M {n} {a}) =
    substitute-sound (sub-topₛ 𝒯ermₛ M) N

-- Top substitution is sound (full categorical proof)
subst′-sound : ∀{Γ A B} (M : Γ ⊢ A) (N : Γ ,, A ⊨ B)
           -> ⟦ [ M /′] N ⟧ᵐ ≈ ⟦ N ⟧ᵐ ∘ ⟨ id , ⟦ M ⟧ₘ ⟩
subst′-sound M N {n} {a} rewrite sym (⟦sub-topₛ⟧ M {n} {a}) =
    traverse′-sound ⟦𝒯erm⟧ (sub-topₛ 𝒯ermₛ M) N

open K 𝒯erm
open Monad M-◇
open Comonad W-□
open Functor F-□ renaming (fmap to □-f)
open Functor F-◇ renaming (fmap to ◇-f)
private module F-◇ = Functor F-◇

-- Lemma used in the soundness proof of computational substitution
subst″-sound-lemma : ∀ Γ {A B} (n k l : ℕ)
                    -> (D : Γ ˢ ,, A now ⊨ B now)
                    -> (⟦Γ⟧ : ⟦ Γ ⟧ₓ n) (⟦A⟧ : ⟦ A ⟧ₜ l)
                  -> ⟦ substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ l (⟦ Γ ˢ ˢ⟧□ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k) l , ⟦A⟧)
                   ≡ ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧)
subst″-sound-lemma Γ {A} n k l D ⟦Γ⟧ ⟦A⟧
    rewrite substitute′-sound ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D {l} {⟦ Γ ˢ ˢ⟧□ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k) l , ⟦A⟧}
          | ⟦↑⟧ (A now) (Γ ˢˢₛ 𝒯erm) {l} {⟦ Γ ˢ ˢ⟧□ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k) l , ⟦A⟧}
          | □-≡ k l (□-≡ n k (⟦ˢ⟧□-twice Γ {n} {⟦Γ⟧}) k) l
          | □-≡ k l (⟦ˢˢ⟧ Γ {n} {⟦Γ⟧}) l = refl

subst″-sound : ∀{Γ A B} (C : Γ ⊨ A now) (D : Γ ˢ ,, A now ⊨ B now)
            -> ⟦ ⟨ C /⟩ D ⟧ᵐ ≈ bindEvent Γ ⟦ C ⟧ᵐ ⟦ D ⟧ᵐ
subst″-sound {Γ}{A}{B} (pure M) D {n} {⟦Γ⟧}
    rewrite traverse′-sound ⟦𝒯erm⟧ (sub-topˢₛ 𝒯ermₛ M) D {n} {⟦Γ⟧}
          | ⟦subst⟧-Γˢ⊆Γ Γ {n} {⟦Γ⟧} | ⟦ˢ⟧-factor Γ {n} {⟦Γ⟧} = refl
subst″-sound {Γ}{A}{B} (letSig_InC_ {A = G} S C) D {n} {⟦Γ⟧}
    rewrite subst″-sound C (substitute′ (idₛ 𝒯erm ⁺ 𝒯erm ↑ 𝒯erm) D) {n} {⟦Γ⟧ , ⟦ S ⟧ₘ n ⟦Γ⟧}
    =
    begin
        bindEvent (Γ ,, G always) ⟦ C ⟧ᵐ ⌞ ⟦ substitute′ ((_⁺_ {G always} (idₛ 𝒯erm) 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ ⌟ n (⟦Γ⟧ , ⟦ S ⟧ₘ n ⟦Γ⟧)
    ≡⟨ bind-to->>= (Γ ,, G always) ⟦ C ⟧ᵐ ⟦ substitute′ ((_⁺_ {G always} (idₛ 𝒯erm) 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ n (⟦Γ⟧ , ⟦ S ⟧ₘ n ⟦Γ⟧) ⟩
            ⟦ C ⟧ᵐ n (⟦Γ⟧ , ⟦ S ⟧ₘ n ⟦Γ⟧)
            >>= (λ l ⟦A⟧ → ⟦ substitute′ (idₛ 𝒯erm ⁺ 𝒯erm ↑ 𝒯erm) D ⟧ᵐ l ((⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦ S ⟧ₘ n ⟦Γ⟧) , ⟦A⟧))
    ≡⟨ cong (λ x → (⟦ C ⟧ᵐ n (⟦Γ⟧ , ⟦ S ⟧ₘ n ⟦Γ⟧) >>= x))
        (ext λ l → ext λ ⟦A⟧ →
            begin
                ⟦ substitute′ (idₛ 𝒯erm ⁺ 𝒯erm ↑ 𝒯erm) D ⟧ᵐ l ((⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦ S ⟧ₘ n ⟦Γ⟧) , ⟦A⟧)
            ≡⟨ substitute′-sound (_↑_ {A now} (_⁺_ {G always} (idₛ 𝒯erm) 𝒯erm) 𝒯erm) D {l} {((⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦ S ⟧ₘ n ⟦Γ⟧) , ⟦A⟧)} ⟩
                ⟦ D ⟧ᵐ l (⟦ (_↑_ {A now} {Γ = Γ ˢ} (_⁺_ {G always} (idₛ 𝒯erm) 𝒯erm) 𝒯erm) ⟧ₛ l ((⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦ S ⟧ₘ n ⟦Γ⟧) , ⟦A⟧))
            ≡⟨ cong (⟦ D ⟧ᵐ l) (⟦↑⟧ (A now) {Γ ˢ ,, G always} (_⁺_ {G always} (idₛ 𝒯erm) 𝒯erm) {l} {(⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦ S ⟧ₘ n ⟦Γ⟧) , ⟦A⟧}) ⟩
                ⟦ D ⟧ᵐ l (⟦ _⁺_ {G always} {Γ = Γ ˢ} (idₛ 𝒯erm) 𝒯erm ⟧ₛ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦ S ⟧ₘ n ⟦Γ⟧) , ⟦A⟧)
            ≡⟨ cong (λ x → ⟦ D ⟧ᵐ l (x , ⟦A⟧)) (⟦⁺⟧ (G always) {Γ ˢ} (idₛ 𝒯erm) {l} {⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦ S ⟧ₘ n ⟦Γ⟧}) ⟩
                ⟦ D ⟧ᵐ l (⟦ idₛ {Γ ˢ} 𝒯erm ⟧ₛ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l) , ⟦A⟧)
            ≡⟨ cong (λ x → ⟦ D ⟧ᵐ l (x , ⟦A⟧)) (⟦idₛ⟧ {Γ ˢ} {l} {⟦ Γ ˢ⟧□ n ⟦Γ⟧ l}) ⟩
                ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧)
            ∎
        )
     ⟩
        ⟦ letSig S InC C ⟧ᵐ n ⟦Γ⟧
        >>= (λ l ⟦A⟧ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
    ≡⟨ sym (bind-to->>= Γ ⟦ letSig S InC C ⟧ᵐ ⟦ D ⟧ᵐ n ⟦Γ⟧) ⟩
        bindEvent Γ ⟦ letSig S InC C ⟧ᵐ ⟦ D ⟧ᵐ n ⟦Γ⟧
    ∎

subst″-sound {Γ}{A}{B} (letEvt_In_ {A = G} E C) D {n} {⟦Γ⟧} =
    begin
        ⟦ ⟨ letEvt E In C /⟩ D ⟧ᵐ n ⟦Γ⟧
    ≡⟨ bind-to->>= Γ ⟦ E ⟧ₘ ⟦ ⟨ C /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ n ⟦Γ⟧ ⟩
        ⟦ E ⟧ₘ n ⟦Γ⟧
            >>= (λ k ⟦A⟧ → ⟦ ⟨ C /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧))
    ≡⟨ cong (λ x → ⟦ E ⟧ₘ n ⟦Γ⟧ >>= x)
        (ext λ k → ext λ ⟦A⟧ → (begin
            ⟦ ⟨ C /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧)
        ≡⟨ subst″-sound C (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) {k} {⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧} ⟩
            bindEvent (Γ ˢ ,, G now) ⟦ C ⟧ᵐ
                ⟦ substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧)
        ≡⟨ bind-to->>= (Γ ˢ ,, G now) ⟦ C ⟧ᵐ ⟦ substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧) ⟩
            ⟦ C ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧)
            >>= (λ l ⟦A⟧₁ → ⟦ substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ l (⟦ Γ ˢ ˢ⟧□ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k) l , ⟦A⟧₁))
        ≡⟨ cong (λ x → ⟦ C ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧) >>= x)
                (ext λ l → ext λ ⟦A⟧₁ → subst″-sound-lemma Γ n k l D ⟦Γ⟧ ⟦A⟧₁) ⟩
            ⟦ C ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧)
            >>= (λ l ⟦A⟧₁ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧₁))
        ∎)) ⟩
        ⟦ E ⟧ₘ n ⟦Γ⟧
            >>= (λ k ⟦A⟧ → ⟦ C ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧)
                >>=  λ l ⟦A⟧ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
    ≡⟨ sym (>>=-assoc (⟦ E ⟧ₘ n ⟦Γ⟧) _ _) ⟩
        (⟦ E ⟧ₘ n ⟦Γ⟧
            >>= λ k ⟦A⟧ → ⟦ C ⟧ᵐ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧ k , ⟦A⟧))
        >>= (λ l ⟦A⟧ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
    ≡⟨ cong (λ x -> x >>= _) (sym (bind-to->>= Γ ⟦ E ⟧ₘ ⟦ C ⟧ᵐ n ⟦Γ⟧)) ⟩
        (⟦ letEvt E In C ⟧ᵐ n ⟦Γ⟧
            >>= (λ l ⟦A⟧ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧)))
    ≡⟨ sym (bind-to->>= Γ ⟦ letEvt E In C ⟧ᵐ ⟦ D ⟧ᵐ n ⟦Γ⟧) ⟩
        bindEvent Γ ⟦ letEvt E In C ⟧ᵐ ⟦ D ⟧ᵐ n ⟦Γ⟧
    ∎

subst″-sound {Γ}{A}{B} (select_↦_||_↦_||both↦_ {A = G}{H} E₁ C₁ E₂ C₂ C₃) D {n} {⟦Γ⟧} =
    begin
        ⟦ ⟨ select E₁ ↦ C₁ || E₂ ↦ C₂ ||both↦ C₃ /⟩ D ⟧ᵐ n ⟦Γ⟧
    ≡⟨⟩
        ⟦ select E₁ ↦ ⟨ C₁ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D)
              || E₂ ↦ ⟨ C₂ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D)
              ||both↦ ⟨ C₃ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ n ⟦Γ⟧
    ≡⟨⟩
        bindEvent Γ (⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫) (handle
            ⟦ ⟨ C₁ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ
            ⟦ ⟨ C₂ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ
            ⟦ ⟨ C₃ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ) n ⟦Γ⟧
    ≡⟨ bind-to->>= Γ (⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫) (handle
                ⟦ ⟨ C₁ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ
                ⟦ ⟨ C₂ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ
                ⟦ ⟨ C₃ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ) n ⟦Γ⟧ ⟩
        ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫ n ⟦Γ⟧
        >>= (λ l ⟦A⟧ → handle
                ⟦ ⟨ C₁ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ
                ⟦ ⟨ C₂ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ
                ⟦ ⟨ C₃ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
    ≡⟨ cong (λ x → ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫ n ⟦Γ⟧ >>= x) (ext λ m → ext λ c → lemma m c) ⟩
        ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫ n ⟦Γ⟧
            >>= (λ m c → handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ m (⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , c)
                >>= λ l ⟦A⟧ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
    ≡⟨ sym (>>=-assoc (⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫ n ⟦Γ⟧) _ _) ⟩
        (⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫ n ⟦Γ⟧
            >>= λ m c -> handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ m (⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , c))
        >>= (λ l ⟦A⟧ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
    ≡⟨ cong (λ x -> x >>= _) (sym (bind-to->>= Γ (⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫)
                (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ) n ⟦Γ⟧)) ⟩
        bindEvent Γ (⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫)
            (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ) n ⟦Γ⟧
        >>= (λ l ⟦A⟧ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
    ≡⟨ sym (bind-to->>= Γ (bindEvent Γ (⟪_,_⟫ ⟦ E₁ ⟧ₘ ⟦ E₂ ⟧ₘ) (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ))
                    ⟦ D ⟧ᵐ n ⟦Γ⟧) ⟩
        bindEvent Γ (bindEvent Γ ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫ (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ)) ⟦ D ⟧ᵐ n ⟦Γ⟧
    ∎
    where
    lemma : ∀ m c
           -> handle
               ⟦ ⟨ C₁ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ
               ⟦ ⟨ C₂ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ
               ⟦ ⟨ C₃ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) ⟧ᵐ m (⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , c)
            ≡ (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ m (⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , c)
                >>= λ l ⟦A⟧ → ⟦ D ⟧ᵐ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
    lemma m (inj₁ (inj₁ (⟦A⟧ , ⟦◇B⟧)))
        rewrite subst″-sound C₁ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) {m} {(⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , ⟦A⟧) , ⟦◇B⟧}
              | bind-to->>= (Γ ˢ ,, G now ,, Event H now) ⟦ C₁ ⟧ᵐ ⟦ substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ m ((⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , ⟦A⟧) , ⟦◇B⟧)
              | (ext λ l → ext λ ⟦C⟧ → subst″-sound-lemma Γ n m l D ⟦Γ⟧ ⟦C⟧)
        = refl
    lemma m (inj₁ (inj₂ (⟦◇A⟧ , ⟦B⟧)))
        rewrite subst″-sound C₂ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) {m} {(⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , ⟦◇A⟧) , ⟦B⟧}
              | bind-to->>= (Γ ˢ ,, Event G now ,, H now) ⟦ C₂ ⟧ᵐ ⟦ substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ m ((⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , ⟦◇A⟧) , ⟦B⟧)
              | (ext λ l → ext λ ⟦C⟧ → subst″-sound-lemma Γ n m l D ⟦Γ⟧ ⟦C⟧)
        = refl
    lemma m (inj₂ (⟦A⟧ , ⟦B⟧))
        rewrite subst″-sound C₃ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D) {m} {(⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , ⟦A⟧) , ⟦B⟧}
              | bind-to->>= (Γ ˢ ,, G now ,, H now) ⟦ C₃ ⟧ᵐ ⟦ substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D ⟧ᵐ m ((⟦ Γ ˢ⟧□ n ⟦Γ⟧ m , ⟦A⟧) , ⟦B⟧)
              | (ext λ l → ext λ ⟦C⟧ → subst″-sound-lemma Γ n m l D ⟦Γ⟧ ⟦C⟧)
        = refl


text:
module Category.Monad.Maybe.Typeclass where

open import Category.Monad
open import Data.Maybe

record MaybeMonad (M : Set → Set) : Set₁ where
  field
    no  : ∀ {A} → M A
    yes : ∀ {A} → A → M A

open MaybeMonad
maybe-monad-ops : MaybeMonad Maybe
no  maybe-monad-ops = nothing
yes maybe-monad-ops = just


text:
module Lib.Nat where

open import Lib.Bool
open import Lib.Logic
open import Lib.Id

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

infixr 50 _*_
infixr 40 _+_

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

lem-plus-zero : (n : Nat) -> n + 0 ≡ n
lem-plus-zero  zero   = refl
lem-plus-zero (suc n) = cong suc (lem-plus-zero n)

lem-plus-suc : (n m : Nat) -> n + suc m ≡ suc (n + m)
lem-plus-suc  zero   m = refl
lem-plus-suc (suc n) m = cong suc (lem-plus-suc n m)

lem-plus-commute : (n m : Nat) -> n + m ≡ m + n
lem-plus-commute n  zero   = lem-plus-zero _
lem-plus-commute n (suc m) with n + suc m | lem-plus-suc n m
... | .(suc (n + m)) | refl = cong suc (lem-plus-commute n m)

_*_ : Nat -> Nat -> Nat
zero  * m = zero
suc n * m = m + n * m

{-# BUILTIN NATPLUS  _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}

_==_ : Nat -> Nat -> Bool
zero  == zero  = true
zero  == suc _ = false
suc _ == zero  = false
suc n == suc m = n == m

{-# BUILTIN NATEQUALS _==_ #-}

NonZero : Nat -> Set
NonZero zero    = False
NonZero (suc _) = True

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --without-K --safe #-}
module Util.Relation.Binary.LogicalEquivalence where

open import Relation.Binary using (IsEquivalence ; Setoid)

open import Util.Prelude

private
  variable
    α β γ : Level
    A B C : Set α

infix 4 _↔_

record _↔_ (A : Set α) (B : Set β) : Set (α ⊔ℓ β) where
  field
    forth : A → B
    back : B → A

open _↔_ public

↔-refl : A ↔ A
↔-refl .forth = id
↔-refl .back = id

↔-reflexive : A ≡ B → A ↔ B
↔-reflexive refl = ↔-refl

↔-sym : A ↔ B → B ↔ A
↔-sym A↔B .forth = A↔B .back
↔-sym A↔B .back = A↔B .forth

↔-trans : A ↔ B → B ↔ C → A ↔ C
↔-trans A↔B B↔C .forth = B↔C .forth ∘ A↔B .forth
↔-trans A↔B B↔C .back = A↔B .back ∘ B↔C .back

↔-isEquivalence : IsEquivalence (_↔_ {α})
↔-isEquivalence = record
  { refl = ↔-refl
  ; sym = ↔-sym
  ; trans = ↔-trans
  }

↔-setoid : ∀ α → Setoid (lsuc α) α
↔-setoid α .Setoid.Carrier = Set α
↔-setoid α .Setoid._≈_ = _↔_
↔-setoid α .Setoid.isEquivalence = ↔-isEquivalence

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Categories.Families where

open import Library
open import Categories

open Cat

Fam : Set → Cat
Fam I = record {
  Obj  = I → Set;
  Hom  = λ A B → ∀ {i} → A i → B i;
  iden = id;
  comp = λ f g → f ∘ g;
  idl  = refl;
  idr  = refl;
  ass  = refl}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
-- Functors on Set

module Control.Functor where

open import Function using (id; flip) renaming (_∘′_ to _∘_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- Operations of a functor.

module T-FunctorOps (F : Set → Set) where

  -- Type of the map function.
  T-map = ∀ {A B} → (A → B) → F A → F B
  T-for = ∀ {A B} → F A → (A → B) → F B

record FunctorOps (F : Set → Set) : Set₁ where
  open T-FunctorOps F

  -- The map function.
  field
    map  : T-map

  -- Alternative notations.
  for : T-for
  for = flip map

  infixr 5 _<$>_ _<&>_
  _<$>_ = map
  _<&>_ = for

-- Laws of a functor.

module T-FunctorLaws {F : Set → Set} (ops : FunctorOps F) where
  open FunctorOps ops public

  -- First functor law: identity.     ∀ (m : F A) → id <$> m ≡ m
  T-map-id = ∀ {A : Set} →

      map {A = A} id ≡ id

  -- Second functor law: composition. ∀ (m : F A) → (g ∘ f) <$> m ≡ g <$> (f <$> m)
  T-map-∘  = ∀ {A B C} {f : A → B} {g : B → C} →

      map (g ∘ f) ≡ map g ∘ map f

record FunctorLaws {F : Set → Set} (ops : FunctorOps F) : Set₁ where
  open T-FunctorLaws ops

  field
    map-id : T-map-id
    map-∘  : T-map-∘

-- Functoriality.

record IsFunctor (F : Set → Set) : Set₁ where

  field
    ops  : FunctorOps  F
    laws : FunctorLaws ops

  open FunctorOps  ops  public
  open FunctorLaws laws public

record Functor : Set₁ where
  constructor functor
  field
    F  : Set → Set
    F! : IsFunctor F

  open IsFunctor F! public

-- Id is a functor.

idIsFunctor : IsFunctor (λ A → A)
idIsFunctor = record
  { ops  = record { map = λ f → f }
  ; laws = record { map-id = refl ; map-∘ = refl }
  }

Id : Functor
Id = record { F = λ A → A ; F! = idIsFunctor }

-- Functors compose.

-- open FunctorOps  {{...}}
-- open FunctorLaws {{...}}

compIsFunctor : ∀ {F G} → IsFunctor F → IsFunctor G → IsFunctor (λ A → F (G A))
compIsFunctor f g = record
  { ops  = record { map    = λ h → F.map (G.map h) }
  ; laws = record { map-id = trans (cong F.map G.map-id) F.map-id
                  ; map-∘  = map-comp
                  }
  }
  where
    module F = IsFunctor f
    module G = IsFunctor g

    map-comp : ∀ {A B C} {h : A → B} {i : B → C} →
      F.map (G.map (i ∘ h)) ≡ F.map (G.map i) ∘ F.map (G.map h)
    map-comp {h = h}{i = i} = begin
        F.map (G.map (i ∘ h))
      ≡⟨ cong F.map G.map-∘ ⟩
        F.map (G.map i ∘ G.map h)
      ≡⟨ F.map-∘ ⟩
        F.map (G.map i) ∘ F.map (G.map h)
      ∎

Comp : Functor → Functor → Functor
Comp (functor F F!) (functor G G!) = functor (λ A → F (G A)) (compIsFunctor F! G!)

-- The constant functor.

constIsFunctor : ∀ A → IsFunctor (λ _ → A)
constIsFunctor A = record
  { ops  = record { map = λ f x → x }
  ; laws = record { map-id = refl ; map-∘ = refl }
  }

Const : (A : Set) → Functor
Const A = functor (λ _ → A) (constIsFunctor A)

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
module Homotopy where

infixr 20 _◎_

open import Data.Product

------------------------------------------------------------------------------
-- Level 0
-- Start with this set and its elements

data B : Set where
  ZERO  : B
  ONE   : B
  PLUS  : B → B → B
  TIMES : B → B → B

------------------------------------------------------------------------------
-- Level 1
-- Now we introduce Id_B. Given b1 : B, b2 : B, we have the types
-- Id_B(b1,b2) of equivalences

data Id_B : B × B → Set where
  unite₊  : { b : B } → Id_B (PLUS ZERO b , b)
  uniti₊  : { b : B } → Id_B (b , PLUS ZERO b)
  swap₊   : { b₁ b₂ : B } → Id_B (PLUS b₁ b₂ , PLUS b₂ b₁)
  assocl₊ : { b₁ b₂ b₃ : B } → Id_B (PLUS b₁ (PLUS b₂ b₃) , PLUS (PLUS b₁ b₂) b₃)
  assocr₊ : { b₁ b₂ b₃ : B } → Id_B (PLUS (PLUS b₁ b₂) b₃ , PLUS b₁ (PLUS b₂ b₃))
  unite⋆  : { b : B } → Id_B (TIMES ONE b , b)
  uniti⋆  : { b : B } → Id_B (b , TIMES ONE b)
  swap⋆   : { b₁ b₂ : B } → Id_B (TIMES b₁ b₂ , TIMES b₂ b₁)
  assocl⋆ : { b₁ b₂ b₃ : B } →
            Id_B (TIMES b₁ (TIMES b₂ b₃) , TIMES (TIMES b₁ b₂) b₃)
  assocr⋆ : { b₁ b₂ b₃ : B } →
            Id_B (TIMES (TIMES b₁ b₂) b₃ , TIMES b₁ (TIMES b₂ b₃))
  dist    : { b₁ b₂ b₃ : B } →
            Id_B (TIMES (PLUS b₁ b₂) b₃ , PLUS (TIMES b₁ b₃) (TIMES b₂ b₃))
  factor  : { b₁ b₂ b₃ : B } →
            Id_B (PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) , TIMES (PLUS b₁ b₂) b₃)
  id⟷   : { b : B } → Id_B (b , b)
  sym    : { b₁ b₂ : B } → Id_B (b₁ , b₂) → Id_B (b₂ , b₁)
  _◎_    : { b₁ b₂ b₃ : B } → Id_B (b₁ , b₂) → Id_B (b₂ , b₃) → Id_B (b₁ , b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           Id_B (b₁ , b₃) → Id_B (b₂ , b₄) → Id_B (PLUS b₁ b₂ , PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           Id_B (b₁ , b₃) → Id_B (b₂ , b₄) → Id_B (TIMES b₁ b₂ , TIMES b₃ b₄)

-- values

data BVAL : B → Set where
  UNIT : BVAL ONE
  LEFT : {b₁ b₂ : B} → BVAL b₁ → BVAL (PLUS b₁ b₂)
  RIGHT : {b₁ b₂ : B} → BVAL b₂ → BVAL (PLUS b₁ b₂)
  PAIR : {b₁ b₂ : B} → BVAL b₁ → BVAL b₂ → BVAL (TIMES b₁ b₂)

mutual

  eval : {b₁ b₂ : B} → Id_B (b₁ , b₂) → BVAL b₁ → BVAL b₂
  eval unite₊ (LEFT ())
  eval unite₊ (RIGHT v) = v
  eval uniti₊ v = RIGHT v
  eval swap₊ (LEFT v) = RIGHT v
  eval swap₊ (RIGHT v) = LEFT v
  eval assocl₊ (LEFT v) = LEFT (LEFT v)
  eval assocl₊ (RIGHT (LEFT v)) = LEFT (RIGHT v)
  eval assocl₊ (RIGHT (RIGHT v)) = RIGHT v
  eval assocr₊ (LEFT (LEFT v)) = LEFT v
  eval assocr₊ (LEFT (RIGHT v)) = RIGHT (LEFT v)
  eval assocr₊ (RIGHT v) = RIGHT (RIGHT v)
  eval unite⋆ (PAIR UNIT v) = v
  eval uniti⋆ v = PAIR UNIT v
  eval swap⋆ (PAIR v1 v2) = PAIR v2 v1
  eval assocl⋆ (PAIR v1 (PAIR v2 v3)) = PAIR (PAIR v1 v2) v3
  eval assocr⋆ (PAIR (PAIR v1 v2) v3) = PAIR v1 (PAIR v2 v3)
  eval dist (PAIR (LEFT v1) v3) = LEFT (PAIR v1 v3)
  eval dist (PAIR (RIGHT v2) v3) = RIGHT (PAIR v2 v3)
  eval factor (LEFT (PAIR v1 v3)) = PAIR (LEFT v1) v3
  eval factor (RIGHT (PAIR v2 v3)) = PAIR (RIGHT v2) v3
  eval id⟷ v = v
  eval (sym c) v = evalB c v
  eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
  eval (c₁ ⊕ c₂) (LEFT v) = LEFT (eval c₁ v)
  eval (c₁ ⊕ c₂) (RIGHT v) = RIGHT (eval c₂ v)
  eval (c₁ ⊗ c₂) (PAIR v₁ v₂) = PAIR (eval c₁ v₁) (eval c₂ v₂)

  evalB : {b₁ b₂ : B} → Id_B (b₁ , b₂) → BVAL b₂ → BVAL b₁
  evalB unite₊ v = RIGHT v
  evalB uniti₊ (LEFT ())
  evalB uniti₊ (RIGHT v) = v
  evalB swap₊ (LEFT v) = RIGHT v
  evalB swap₊ (RIGHT v) = LEFT v
  evalB assocl₊ (LEFT (LEFT v)) = LEFT v
  evalB assocl₊ (LEFT (RIGHT v)) = RIGHT (LEFT v)
  evalB assocl₊ (RIGHT v) = RIGHT (RIGHT v)
  evalB assocr₊ (LEFT v) = LEFT (LEFT v)
  evalB assocr₊ (RIGHT (LEFT v)) = LEFT (RIGHT v)
  evalB assocr₊ (RIGHT (RIGHT v)) = RIGHT v
  evalB unite⋆ v = PAIR UNIT v
  evalB uniti⋆ (PAIR UNIT v) = v
  evalB swap⋆ (PAIR v1 v2) = PAIR v2 v1
  evalB assocl⋆ (PAIR (PAIR v1 v2) v3) = PAIR v1 (PAIR v2 v3)
  evalB assocr⋆ (PAIR v1 (PAIR v2 v3)) = PAIR (PAIR v1 v2) v3
  evalB dist (LEFT (PAIR v1 v3)) = PAIR (LEFT v1) v3
  evalB dist (RIGHT (PAIR v2 v3)) = PAIR (RIGHT v2) v3
  evalB factor (PAIR (LEFT v1) v3) = LEFT (PAIR v1 v3)
  evalB factor (PAIR (RIGHT v2) v3) = RIGHT (PAIR v2 v3)
  evalB id⟷ v = v
  evalB (sym c) v = eval c v
  evalB (c₁ ◎ c₂) v = evalB c₁ (evalB c₂ v)
  evalB (c₁ ⊕ c₂) (LEFT v) = LEFT (evalB c₁ v)
  evalB (c₁ ⊕ c₂) (RIGHT v) = RIGHT (evalB c₂ v)
  evalB (c₁ ⊗ c₂) (PAIR v₁ v₂) = PAIR (evalB c₁ v₁) (evalB c₂ v₂)

------------------------------------------------------------------------------
-- Level 2

-- Now we introduce Id_{Id_B}. Given c1 : Id_B(b1,b2) and c2 :
-- Id_B(b1,b2), we have the type of equivalences that show that c1 and
-- c2 are isomorphic.
--
-- We want:
--
-- data Id_Id_B : {b₁ b₂ : B} → Id_B (b₁ , b₂) × Id_B (b₁ , b₂) → Set where
--  ...
-- but before we do that we need to embed the combinators as values that can
-- be manipulated using combinators

-- define the category Int C whose objects are pairs (B,B) and which has an
-- inverse recip sending (B1,B2) to (B2,B1) and then the compact closed
-- eta/epsilon where eta : I -> (A+,A-) * (recip (A+,A-))

-- the embedding send B to (B,I)

-- INT B has as objects pairs of B objects

{--
data Id_BB : (B × B) × (B × B) → Set where
  intarr : { b₁ b₂ b₃ b₄ : B } → Id_BB ((b₁ , b₂) , (b₃ , b₄))

embedArr : { b₁ b₂ b₃ b₄ : B } →
           Id_BB ((b₁ , b₂) , (b₃ , b₄)) → Id_B ((b₁ , b₄) , (b₂ , b₃))
embedArr x = ?

  Iuniti₊  : { b : B } → Id_BB (b , PLUS ZERO b)
  Iswap₊   : { b₁ b₂ : B } → Id_BB (PLUS b₁ b₂ , PLUS b₂ b₁)
  Iassocl₊ : { b₁ b₂ b₃ : B } → Id_BB (PLUS b₁ (PLUS b₂ b₃) , PLUS (PLUS b₁ b₂) b₃)
  Iassocr₊ : { b₁ b₂ b₃ : B } → Id_BB (PLUS (PLUS b₁ b₂) b₃ , PLUS b₁ (PLUS b₂ b₃))
  Iunite⋆  : { b : B } → Id_BB (TIMES ONE b , b)
  Iuniti⋆  : { b : B } → Id_BB (b , TIMES ONE b)
  Iswap⋆   : { b₁ b₂ : B } → Id_BB (TIMES b₁ b₂ , TIMES b₂ b₁)
  Iassocl⋆ : { b₁ b₂ b₃ : B } →
            Id_BB (TIMES b₁ (TIMES b₂ b₃) , TIMES (TIMES b₁ b₂) b₃)
  Iassocr⋆ : { b₁ b₂ b₃ : B } →
            Id_BB (TIMES (TIMES b₁ b₂) b₃ , TIMES b₁ (TIMES b₂ b₃))
  Idist    : { b₁ b₂ b₃ : B } →
            Id_BB (TIMES (PLUS b₁ b₂) b₃ , PLUS (TIMES b₁ b₃) (TIMES b₂ b₃))
  Ifactor  : { b₁ b₂ b₃ : B } →
            Id_BB (PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) , TIMES (PLUS b₁ b₂) b₃)
  Iid⟷   : { b : B } → Id_BB (b , b)
  Isym    : { b₁ b₂ : B } → Id_BB (b₁ , b₂) → Id_BB (b₂ , b₁)
  _I◎_    : { b₁ b₂ b₃ : B } → Id_BB (b₁ , b₂) → Id_BB (b₂ , b₃) → Id_BB (b₁ , b₃)
  _I⊕_    : { b₁ b₂ b₃ b₄ : B } →
           Id_BB (b₁ , b₃) → Id_BB (b₂ , b₄) → Id_BB (PLUS b₁ b₂ , PLUS b₃ b₄)
  _I⊗_    : { b₁ b₂ b₃ b₄ : B } →
           Id_BB (b₁ , b₃) → Id_BB (b₂ , b₄) → Id_BB (TIMES b₁ b₂ , TIMES b₃ b₄)

data BRVAL : BR → Set where
  UNITR : BRVAL ONER
  LEFTR : {b₁ b₂ : BR} → BRVAL b₁ → BRVAL (PLUSR b₁ b₂)
  RIGHTR : {b₁ b₂ : BR} → BRVAL b₂ → BRVAL (PLUSR b₁ b₂)
  PAIRR : {b₁ b₂ : BR} → BRVAL b₁ → BRVAL b₂ → BRVAL (TIMESR b₁ b₂)
  RECIPR : {b : BR} → BRVAL b → BRVAL (RECIP b)

embedT : B → BR
embedT ZERO = ZEROR
embedT ONE = ONER
embedT (PLUS b₁ b₂) = PLUSR (embedT b₁) (embedT b₂)
embedT (TIMES b₁ b₂) = TIMESR (embedT b₁) (embedT b₂)

embedV : {b : B} → BVAL b → BRVAL (embedT b)
embedV UNIT = UNITR
embedV (LEFT v) = LEFTR (embedV v)
embedV (RIGHT v) = RIGHTR (embedV v)
embedV (PAIR v₁ v₂) = PAIRR (embedV v₁) (embedV v₂)

embedC : {b₁ b₂ : B} →
         Id_B (b₁ , b₂) → BRVAL (TIMESR (RECIP (embedT b₁)) (embedT b₂))
embedC unite₊ = ?
embedC uniti₊ = ?
embedC swap₊ = ?
embedC assocl₊ = ?
embedC assocr₊ = ?
embedC unite⋆ = ?
embedC uniti⋆ = ?
embedC swap⋆ = ?
embedC assocl⋆ = ?
embedC assocr⋆ = ?
embedC dist = ?
embedC factor = ?
embedC id⟷ = ?
embedC (sym c) = ?
embedC (c₁ ◎ c₂) = ?
embedC (c₁ ⊕ c₂) = ?
embedC (c₁ ⊗ c₂) = ?
--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Groups.Definition
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Fields.Fields
open import Rings.Orders.Total.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Orders.LeastUpperBounds.Definition
open import Fields.Orders.Total.Definition
open import Sets.EquivalenceRelations

module Numbers.ClassicalReals.RealField.Lemmas {a b c : _} {A : Set a} {S : Setoid {_} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (F : Field R) {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} (pOrderedRing : PartiallyOrderedRing R pOrder) {orderNontrivialX orderNontrivialY : A} (orderNontrivial : orderNontrivialX < orderNontrivialY) where

open Ring R
open Group additiveGroup
open Setoid S
open Equivalence eq
open SetoidPartialOrder pOrder
open import Rings.Orders.Partial.Lemmas pOrderedRing
open PartiallyOrderedRing pOrderedRing

IsInterval : {d : _} {pred : A → Set d} (subset : subset S pred) → Set (a ⊔ c ⊔ d)
IsInterval {pred = pred} subset = (x y : A) → (x<y : x < y) → pred x → pred y → (c : A) → (x < c) → (c < y) → pred c

-- Example: (a, b) is an interval
openBallPred : A → A → A → Set c
openBallPred a b x = (a < x) && (x < b)
openBallSubset : (a b : A) → subset S (openBallPred a b)
openBallSubset a b {x} {y} x=y (a<x ,, x<y) = <WellDefined reflexive x=y a<x ,, <WellDefined x=y reflexive x<y
openBallInterval : (a b : A) → IsInterval (openBallSubset a b)
openBallInterval a b x y x<y (a<x ,, x<b) (a<y ,, y<b) c x<c c<y = <Transitive a<x x<c ,, <Transitive c<y y<b

nonemptyBoundedIntervalHasLubImpliesAllLub : ({d : _} {pred : A → Set d} {subset : subset S pred} (interval : IsInterval subset) → (nonempty : Sg A pred) → (boundedAbove : Sg A (UpperBound pOrder subset)) → Sg A (LeastUpperBound pOrder subset)) → {d : _} → {pred : A → Set d} → (sub : subset S pred) → (nonempty : Sg A pred) → (boundedAbove : Sg A (UpperBound pOrder sub)) → Sg A (LeastUpperBound pOrder sub)
nonemptyBoundedIntervalHasLubImpliesAllLub axiom {d} {pred} sub (member , predMember) (bound , isBound) = lub , lubIsLub
  where
    intervalPredicate : A → Set (a ⊔ b ⊔ c ⊔ d)
    intervalPredicate a = Sg A (λ k → ((a < k) || (a ∼ k)) && pred k)
    intervalIsSubset : subset S intervalPredicate
    intervalIsSubset {x} {y} x=y (bigger , (inl x<bigger ,, biggerWorks)) = (bigger , (inl (<WellDefined x=y reflexive x<bigger) ,, biggerWorks))
    intervalIsSubset {x} {y} x=y (bigger , (inr x=bigger ,, biggerWorks)) = (bigger , (inr (transitive (symmetric x=y) x=bigger) ,, biggerWorks))
    intervalIsInterval : IsInterval intervalIsSubset
    intervalIsInterval x y x<y (dominateX , (x<dominateX ,, predDominateX)) (dominateY , (inl y<dominateY ,, predDominateY)) c x<c c<y = dominateY , (inl (<Transitive c<y y<dominateY) ,, predDominateY)
    intervalIsInterval x y x<y (dominateX , (x<dominateX ,, predDominateX)) (dominateY , (inr y=dominateY ,, predDominateY)) c x<c c<y = dominateY , (inl (<WellDefined reflexive y=dominateY c<y) ,, predDominateY)
    intervalNonempty : Sg A intervalPredicate
    intervalNonempty = ((member + orderNontrivialX) + inverse orderNontrivialY) , (member , (inl (<WellDefined (transitive groupIsAbelian +Associative) identLeft (orderRespectsAddition (moveInequality' orderNontrivial) member)) ,, predMember))
    intervalBounded : Sg A (UpperBound pOrder intervalIsSubset)
    intervalBounded = bound , ans
      where
        ans : (y : A) → intervalPredicate y → (y < bound) || (y ∼ bound)
        ans y (boundY , (y<boundY ,, predY)) with isBound boundY predY
        ans y (boundY , (inl y<boundY ,, predY)) | inl boundY<Bound = inl (<Transitive y<boundY boundY<Bound)
        ans y (boundY , (inr y=boundY ,, predY)) | inl boundY<Bound = inl (<WellDefined (symmetric y=boundY) reflexive boundY<Bound)
        ans y (boundY , (inl y<boundY ,, predY)) | inr boundY=Bound = inl (<WellDefined reflexive boundY=Bound y<boundY)
        ans y (boundY , (inr y=boundY ,, predY)) | inr boundY=Bound = inr (transitive y=boundY boundY=Bound)
    intervalLub : Sg A (LeastUpperBound pOrder intervalIsSubset)
    intervalLub = axiom intervalIsInterval intervalNonempty intervalBounded
    lub : A
    lub with intervalLub
    ... | b , _ = b
    lubProof : LeastUpperBound pOrder intervalIsSubset lub
    lubProof with intervalLub
    ... | b , pr = pr
    ubImpliesUbSub : {x : A} → UpperBound pOrder sub x → UpperBound pOrder intervalIsSubset x
    ubImpliesUbSub {x} ub y (bound , (y<bound ,, predBound)) with ub bound predBound
    ubImpliesUbSub {x} ub y (bound , (inl y<bound ,, predBound)) | inl bound<x = inl (<Transitive y<bound bound<x)
    ubImpliesUbSub {x} ub y (bound , (inr y=bound ,, predBound)) | inl bound<x = inl (<WellDefined (symmetric y=bound) reflexive bound<x)
    ubImpliesUbSub {x} ub y (bound , (inl y<bound ,, predBound)) | inr bound=x = inl (<WellDefined reflexive bound=x y<bound)
    ubImpliesUbSub {x} ub y (bound , (inr y=bound ,, predBound)) | inr bound=x = inr (transitive y=bound bound=x)
    ubSubImpliesUb : {x : A} → UpperBound pOrder intervalIsSubset x → UpperBound pOrder sub x
    ubSubImpliesUb {x} ub y predY with ub y (y , (inr reflexive ,, predY))
    ubSubImpliesUb {x} ub y predY | inl t<x = inl t<x
    ubSubImpliesUb {x} ub y predY | inr t=x = inr t=x
    lubIsLub : LeastUpperBound pOrder sub lub
    LeastUpperBound.upperBound lubIsLub = ubSubImpliesUb (LeastUpperBound.upperBound lubProof)
    LeastUpperBound.leastUpperBound lubIsLub y yIsUpperBound = LeastUpperBound.leastUpperBound lubProof y (ubImpliesUbSub yIsUpperBound)


text:
module UniDB.Morph.StarPrime where

open import UniDB.Spec
open import UniDB.Morph.Depth

mutual
  data Star* (Ξ : MOR) : MOR where
    refl : {γ : Dom} → Star* Ξ γ γ
    incl : {γ₁ γ₂ : Dom} (ξs : Star+ Ξ γ₁ γ₂) → Star* Ξ γ₁ γ₂

  data Star+ (Ξ : MOR) : MOR where
    step : {γ₁ γ₂ γ₃ : Dom} (ξs : Star* Ξ γ₁ γ₂) (ξ : Ξ γ₂ γ₃) → Star+ Ξ γ₁ γ₃

module _ {Ξ : MOR} where
  mutual
    step` : {Ξ : MOR} {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζs : Star* Ξ γ₂ γ₃) → Star+ Ξ γ₁ γ₃
    step` ξ refl     = step refl ξ
    step` ξ (incl ζ) = step+ ξ ζ

    step+ : {Ξ : MOR} {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζs : Star+ Ξ γ₂ γ₃) → Star+ Ξ γ₁ γ₃
    step+ ξ (step ζs ζ) = step (incl (step` ξ ζs)) ζ

  mutual
    comp** : {γ₁ γ₂ γ₃ : Dom} (ξs : Star* Ξ γ₁ γ₂) (ζs : Star* Ξ γ₂ γ₃) → Star* Ξ γ₁ γ₃
    comp** ξs refl      = ξs
    comp** ξs (incl ζs) = incl (comp*+ ξs ζs)

    comp*+ : {γ₁ γ₂ γ₃ : Dom} (ξs : Star* Ξ γ₁ γ₂) (ζs : Star+ Ξ γ₂ γ₃) → Star+ Ξ γ₁ γ₃
    comp*+ ξs (step ζs ζ) = step (comp** ξs ζs) ζ

  mutual
    comp+* : {γ₁ γ₂ γ₃ : Dom} (ξs : Star+ Ξ γ₁ γ₂) (ζs : Star* Ξ γ₂ γ₃) → Star+ Ξ γ₁ γ₃
    comp+* ξs refl      = ξs
    comp+* ξs (incl ζs) = comp++ ξs ζs

    comp++ : {γ₁ γ₂ γ₃ : Dom} (ξs : Star+ Ξ γ₁ γ₂) (ζs : Star+ Ξ γ₂ γ₃) → Star+ Ξ γ₁ γ₃
    comp++ ξs (step ζs ζ) = step (incl (comp+* ξs ζs)) ζ

module _ {Ξ : MOR} {{upΞ : Up Ξ}} where

  mutual
    instance
      iUpStar* : Up (Star* Ξ)
      _↑₁ {{iUpStar*}} refl      = refl
      _↑₁ {{iUpStar*}} (incl ξs) = incl (ξs ↑₁)
      _↑_ {{iUpStar*}} ξ 0 = ξ
      _↑_ {{iUpStar*}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
      ↑-zero {{iUpStar*}} ξ = refl
      ↑-suc {{iUpStar*}} ξ δ⁺ = refl

      iUpStar+ : Up (Star+ Ξ)
      _↑₁ {{iUpStar+}} (step ξs ξ) = step (ξs ↑₁) (ξ ↑₁)
      _↑_ {{iUpStar+}} ξ 0 = ξ
      _↑_ {{iUpStar+}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
      ↑-zero {{iUpStar+}} ξ = refl
      ↑-suc {{iUpStar+}} ξ δ⁺ = refl

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
-- Andreas, 2015-12-28, issue reported by effectfully
-- {-# OPTIONS -v tc.data.fits:15 -v tc.conv.sort:30 -v tc.conv.nat:30 #-}

open import Common.Level

postulate
  fun : Level → Level

data Test : Set (fun lzero) where
  c : Test → Test

-- The primitive lzero in argument of neutral is what matters here.
-- Agda reported:
--   The type of the constructor does not fit in the sort of the
--   datatype, since Set (fun lzero) is not less or equal than
--   Set (fun lzero)
-- Upon inspection of non-prettyTCM Terms, one side had turned
-- `lzero` into `Level (Max [])`, whereas it remained `Def lzero []`
-- on the other side.

-- Should work now.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- 2014-04-06 Andreas, issue reported by flickyfrans
-- {-# OPTIONS --show-implicit -v tc.section.apply:60 #-}

open import Common.Level renaming (lsuc to suc)

record RawMonad {α β : Level} (M : {γ : Level} → Set γ → Set γ) : Set (suc (α ⊔ β)) where
  infixl 1 _>>=_
  field
    return' : {A : Set α} → A → M A
    _>>=_   : {A : Set α} {B : Set β} → M A → (A → M B) → M B

module MonoMonad {α} = RawMonad {α} {α}
module MM = MonoMonad {{...}}

-- return : {α : Level} {M : {γ : Level} → Set γ → Set γ} {{m : RawMonad {α} {α} M }} {A : Set α} → A → M A

return : _
return = MM.return'

-- WAS: Panic: deBruijn index out of scope: 2 in context [M,α]
-- when checking that the expression MM.return' has type _15

-- CAUSE: Ill-formed section telescope produced by checkSectionApplication.

-- NOW: Works.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties of reflexive closures
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Closure.Reflexive.Properties where

open import Data.Product as Prod
open import Data.Sum.Base as Sum
open import Function.Equivalence using (_⇔_; equivalence)
open import Function using (id)
open import Level
open import Relation.Binary
open import Relation.Binary.Construct.Closure.Reflexive
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Unary using (Pred)

private
  variable
    a b ℓ p q : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Relational properties

module _ {P : Rel A p} {Q : Rel B q} where

  =[]⇒ : ∀ {f : A → B} → P =[ f ]⇒ Q → Refl P =[ f ]⇒ Refl Q
  =[]⇒ x [ x∼y ] = [ x x∼y ]
  =[]⇒ x refl    = refl

module _ {_~_ : Rel A ℓ} where

  sym : Symmetric _~_ → Symmetric (Refl _~_)
  sym ~-sym [ x∼y ] = [ ~-sym x∼y ]
  sym ~-sym refl    = refl

  trans : Transitive _~_ → Transitive (Refl _~_)
  trans ~-trans [ x∼y ] [ x∼y₁ ] = [ ~-trans x∼y x∼y₁ ]
  trans ~-trans [ x∼y ] refl     = [ x∼y ]
  trans ~-trans refl    [ x∼y ]  = [ x∼y ]
  trans ~-trans refl    refl     = refl

  antisym : ∀ {ℓ'} (_≈_ : Rel A ℓ') → Reflexive _≈_ →
            Asymmetric _~_ → Antisymmetric _≈_ (Refl _~_)
  antisym _≈_ ref asym [ x∼y ] [ y∼x ] = contradiction x∼y (asym y∼x)
  antisym _≈_ ref asym [ x∼y ] refl    = ref
  antisym _≈_ ref asym refl    _       = ref

  total : Trichotomous _≡_ _~_ → Total (Refl _~_)
  total compare x y with compare x y
  ... | tri< a _    _ = inj₁ [ a ]
  ... | tri≈ _ refl _ = inj₁ refl
  ... | tri> _ _    c = inj₂ [ c ]

  fromSum : ∀ {a b} → a ≡ b ⊎ a ~ b → Refl _~_ a b
  fromSum (inj₁ refl) = refl
  fromSum (inj₂ y) = [ y ]

  toSum : ∀ {a b} → Refl _~_ a b → a ≡ b ⊎ a ~ b
  toSum [ x∼y ] = inj₂ x∼y
  toSum refl = inj₁ refl

  ⊎⇔Refl : ∀ {a b} → (a ≡ b ⊎ a ~ b) ⇔ Refl _~_ a b
  ⊎⇔Refl = equivalence fromSum toSum

  dec : Decidable {A = A} _≡_ → Decidable _~_ → Decidable (Refl _~_)
  dec ≡-dec ~-dec a b = Dec.map ⊎⇔Refl (≡-dec a b ⊎-dec ~-dec a b)

  decidable : Trichotomous _≡_ _~_ → Decidable (Refl _~_)
  decidable ~-tri a b with ~-tri a b
  ... | tri< a~b  _  _ = yes [ a~b ]
  ... | tri≈ _  refl _ = yes refl
  ... | tri> ¬a ¬b   _ = no λ { refl → ¬b refl ; [ p ] → ¬a p }

  respˡ : ∀ {P : REL A B p} → P Respectsˡ _~_ → P Respectsˡ (Refl _~_)
  respˡ p-respˡ-~ [ x∼y ] = p-respˡ-~ x∼y
  respˡ _         refl    = id

  respʳ : ∀ {P : REL B A p} → P Respectsʳ _~_ → P Respectsʳ (Refl _~_)
  respʳ = respˡ

module _ {_~_ : Rel A ℓ} {P : Pred A p} where

  resp : P Respects _~_ → P Respects (Refl _~_)
  resp p-resp-~ [ x∼y ] = p-resp-~ x∼y
  resp _        refl    = id

module _ {_~_ : Rel A ℓ} {P : Rel A p} where

  resp₂ : P Respects₂ _~_ → P Respects₂ (Refl _~_)
  resp₂ = Prod.map respˡ respʳ

------------------------------------------------------------------------
-- Structures

module _ {_~_ : Rel A ℓ} where

  isPreorder : Transitive _~_ → IsPreorder _≡_ (Refl _~_)
  isPreorder ~-trans = record
    { isEquivalence = PropEq.isEquivalence
    ; reflexive     = λ { refl → refl }
    ; trans         = trans ~-trans
    }

  isPartialOrder : IsStrictPartialOrder _≡_ _~_ → IsPartialOrder _≡_ (Refl _~_)
  isPartialOrder O = record
    { isPreorder = isPreorder O.trans
    ; antisym    = antisym _≡_ refl O.asym
    } where module O = IsStrictPartialOrder O

  isDecPartialOrder : IsDecStrictPartialOrder _≡_ _~_ → IsDecPartialOrder _≡_ (Refl _~_)
  isDecPartialOrder O = record
    { isPartialOrder = isPartialOrder O.isStrictPartialOrder
    ; _≟_            = O._≟_
    ; _≤?_           = dec O._≟_ O._<?_
    } where module O = IsDecStrictPartialOrder O

  isTotalOrder : IsStrictTotalOrder _≡_ _~_ → IsTotalOrder _≡_ (Refl _~_)
  isTotalOrder O = record
    { isPartialOrder = isPartialOrder isStrictPartialOrder
    ; total          = total compare
    } where open IsStrictTotalOrder O

  isDecTotalOrder : IsStrictTotalOrder _≡_ _~_ → IsDecTotalOrder _≡_ (Refl _~_)
  isDecTotalOrder O = record
    { isTotalOrder = isTotalOrder O
    ; _≟_          = _≟_
    ; _≤?_         = dec _≟_ _<?_
    } where open IsStrictTotalOrder O


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

open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Sets.EquivalenceRelations

module Setoids.Setoids where

record Setoid {a} {b} (A : Set a) : Set (a ⊔ lsuc b) where
  infix 1 _∼_
  field
    _∼_ : A → A → Set b
    eq : Equivalence _∼_

  open Equivalence eq

  ~refl : {r : A} → (r ∼ r)
  ~refl {r} = reflexive {r}

record Quotient {a} {b} {c} {A : Set a} {image : Set b} (S : Setoid {a} {c} A) : Set (a ⊔ b ⊔ c) where
  open Setoid S
  field
    map : A → image
    mapWellDefined : {x y : A} → x ∼ y → map x ≡ map y
    mapSurjective : Surjection map
    mapInjective : {x y : A} → map x ≡ map y → x ∼ y

record SetoidToSet {a b c : _} {A : Set a} (S : Setoid {a} {c} A) (quotient : Set b) : Set (a ⊔ b ⊔ c) where
  open Setoid S
  field
    project : A → quotient
    wellDefined : (x y : A) → (x ∼ y) → project x ≡ project y
    surj : Surjection project
    inj : (x y : A) → project x ≡ project y → x ∼ y

open Setoid

reflSetoid : {a : _} (A : Set a) → Setoid A
_∼_ (reflSetoid A) a b = a ≡ b
Equivalence.reflexive (eq (reflSetoid A)) = refl
Equivalence.symmetric (eq (reflSetoid A)) {b} {.b} refl = refl
Equivalence.transitive (eq (reflSetoid A)) {b} {.b} {.b} refl refl = refl

record SetoidInjection {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
  open Setoid S renaming (_∼_ to _∼A_)
  open Setoid T renaming (_∼_ to _∼B_)
  field
    wellDefined : {x y : A} → x ∼A y → (f x) ∼B (f y)
    injective : {x y : A} → (f x) ∼B (f y) → x ∼A y

reflSetoidWellDefined : {a b c : _} {A : Set a} (S : Setoid {a} {b} A) (C : Set c) (f : C → A) → {x y : C} → x ≡ y → Setoid._∼_ S (f x) (f y)
reflSetoidWellDefined S C f refl = Equivalence.reflexive (Setoid.eq S)

record SetoidSurjection {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
  open Setoid S renaming (_∼_ to _∼A_)
  open Setoid T renaming (_∼_ to _∼B_)
  field
    wellDefined : {x y : A} → x ∼A y → (f x) ∼B (f y)
    surjective : {x : B} → Sg A (λ a → f a ∼B x)

record SetoidBijection {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
  field
    inj : SetoidInjection S T f
    surj : SetoidSurjection S T f
  wellDefined : {x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)
  wellDefined = SetoidInjection.wellDefined inj

record SetoidsBiject {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) : Set (a ⊔ b ⊔ c ⊔ d) where
  field
    bij : A → B
    bijIsBijective : SetoidBijection S T bij

setoidInjComp : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {g : A → B} {h : B → C} → (gB : SetoidInjection S T g) (hB : SetoidInjection T U h) → SetoidInjection S U (h ∘ g)
SetoidInjection.wellDefined (setoidInjComp gI hI) x~y = SetoidInjection.wellDefined hI (SetoidInjection.wellDefined gI x~y)
SetoidInjection.injective (setoidInjComp gI hI) hgx~hgy = SetoidInjection.injective gI (SetoidInjection.injective hI hgx~hgy)

setoidSurjComp : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {g : A → B} {h : B → C} → (gB : SetoidSurjection S T g) (hB : SetoidSurjection T U h) → SetoidSurjection S U (h ∘ g)
SetoidSurjection.wellDefined (setoidSurjComp gI hI) x~y = SetoidSurjection.wellDefined hI (SetoidSurjection.wellDefined gI x~y)
SetoidSurjection.surjective (setoidSurjComp gI hI) {x} with SetoidSurjection.surjective hI {x}
SetoidSurjection.surjective (setoidSurjComp gI hI) {x} | a , prA with SetoidSurjection.surjective gI {a}
SetoidSurjection.surjective (setoidSurjComp {U = U} gI hI) {x} | a , prA | b , prB = b , Equivalence.transitive (Setoid.eq U) (SetoidSurjection.wellDefined hI prB) prA
  where
    open Setoid U

setoidBijComp : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {g : A → B} {h : B → C} → (gB : SetoidBijection S T g) (hB : SetoidBijection T U h) → SetoidBijection S U (h ∘ g)
SetoidBijection.inj (setoidBijComp gB hB) = setoidInjComp (SetoidBijection.inj gB) (SetoidBijection.inj hB)
SetoidBijection.surj (setoidBijComp gB hB) = setoidSurjComp (SetoidBijection.surj gB) (SetoidBijection.surj hB)

setoidIdIsBijective : {a b : _} {A : Set a} {S : Setoid {a} {b} A} → SetoidBijection S S (λ i → i)
SetoidInjection.wellDefined (SetoidBijection.inj (setoidIdIsBijective {A = A})) = id
SetoidInjection.injective (SetoidBijection.inj (setoidIdIsBijective {A = A})) = id
SetoidSurjection.wellDefined (SetoidBijection.surj (setoidIdIsBijective {A = A})) = id
SetoidSurjection.surjective (SetoidBijection.surj (setoidIdIsBijective {S = S})) {x} = x , Equivalence.reflexive (Setoid.eq S)

record SetoidInvertible {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
  field
    fWellDefined : {x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)
    inverse : B → A
    inverseWellDefined : {x y : B} → Setoid._∼_ T x y → Setoid._∼_ S (inverse x) (inverse y)
    isLeft : (b : B) → Setoid._∼_ T (f (inverse b)) b
    isRight : (a : A) → Setoid._∼_ S (inverse (f a)) a

setoidBijectiveImpliesInvertible : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {f : A → B} (bij : SetoidBijection S T f) → SetoidInvertible S T f
SetoidInvertible.fWellDefined (setoidBijectiveImpliesInvertible bij) x~y = SetoidInjection.wellDefined (SetoidBijection.inj bij) x~y
SetoidInvertible.inverse (setoidBijectiveImpliesInvertible bij) x with SetoidSurjection.surjective (SetoidBijection.surj bij) {x}
SetoidInvertible.inverse (setoidBijectiveImpliesInvertible bij) x | a , b = a
SetoidInvertible.inverseWellDefined (setoidBijectiveImpliesInvertible bij) {x} {y} x~y with SetoidSurjection.surjective (SetoidBijection.surj bij) {x}
SetoidInvertible.inverseWellDefined (setoidBijectiveImpliesInvertible {T = T} bij) {x} {y} x~y | a , prA with SetoidSurjection.surjective (SetoidBijection.surj bij) {y}
... | b , prB = SetoidInjection.injective (SetoidBijection.inj bij) (Equivalence.transitive (Setoid.eq T) prA (Equivalence.transitive (Setoid.eq T) x~y (Equivalence.symmetric (Setoid.eq T) prB)))
  where
    open Setoid T
SetoidInvertible.isLeft (setoidBijectiveImpliesInvertible bij) b with SetoidSurjection.surjective (SetoidBijection.surj bij) {b}
... | a , prA = prA
SetoidInvertible.isRight (setoidBijectiveImpliesInvertible {f = f} bij) b with SetoidSurjection.surjective (SetoidBijection.surj bij) {f b}
... | fb , prFb = SetoidInjection.injective (SetoidBijection.inj bij) prFb

setoidInvertibleImpliesBijective : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {f : A → B} (inv : SetoidInvertible S T f) → SetoidBijection S T f
SetoidInjection.wellDefined (SetoidBijection.inj (setoidInvertibleImpliesBijective inv)) x~y = SetoidInvertible.fWellDefined inv x~y
SetoidInjection.injective (SetoidBijection.inj (setoidInvertibleImpliesBijective {S = S} {f = f} inv)) {x} {y} pr = Equivalence.transitive (Setoid.eq S) (Equivalence.symmetric (Setoid.eq S) (SetoidInvertible.isRight inv x)) (Equivalence.transitive (Setoid.eq S) (SetoidInvertible.inverseWellDefined inv pr) (SetoidInvertible.isRight inv y))
  where
    open Setoid S
SetoidSurjection.wellDefined (SetoidBijection.surj (setoidInvertibleImpliesBijective inv)) x~y = SetoidInvertible.fWellDefined inv x~y
SetoidSurjection.surjective (SetoidBijection.surj (setoidInvertibleImpliesBijective inv)) {x} = SetoidInvertible.inverse inv x , SetoidInvertible.isLeft inv x

inverseInvertible : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {f : A → B} (inv1 : SetoidInvertible S T f) → SetoidInvertible T S (SetoidInvertible.inverse inv1)
SetoidInvertible.fWellDefined (inverseInvertible record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) x=y = inverseWellDefined x=y
SetoidInvertible.inverse (inverseInvertible {f = f} record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) = f
SetoidInvertible.inverseWellDefined (inverseInvertible record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) = fWellDefined
SetoidInvertible.isLeft (inverseInvertible record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) = isRight
SetoidInvertible.isRight (inverseInvertible record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) = isLeft


text:
-- Andreas, 2012-06-30, case reported by Noam Zeilbereger
module Issue670 where

infix 4 _≡_

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

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

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN SUC     suc  #-}
{-# BUILTIN ZERO    zero #-}

record T : Set where
    field
      x : Nat
      .eq : x ≡ x

foo : T
foo = record { x = 0 ; eq = refl }

bar : T
bar = record { x = 0 ; eq = {!refl!} }
-- give should succeed

max_stars_repo_name: np/agda-git-experiment


text:
module ConsoleLib where

open import NativeIO public
open import SizedIO.Console public  hiding (main) renaming (translateIOConsole to run)
open import Size
open import SizedIO.Base
open import Data.List

WriteString : (s : String) → IOConsole ∞ Unit
WriteString s = Exec (putStrLn s)

GetLine : IOConsole ∞ String
GetLine = Exec getLine

ConsoleProg : Set
ConsoleProg = NativeIO Unit

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- Andreas, 2014-08-30, reported by asr
-- All of the following corecursive functions from Data.Stream
-- should pass the termination checker.

{-# OPTIONS --cubical-compatible --guardedness #-}
-- {-# OPTIONS -v term:20 #-}

open import Common.Coinduction
open import Common.Prelude renaming (Nat to ℕ) hiding (_∷_; map)

infixr 5 _∷_

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

map : ∀ {A B} → (A → B) → Stream A → Stream B
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

zipWith : ∀ {A B C} →
          (A → B → C) → Stream A → Stream B → Stream C
zipWith _∙_ (x ∷ xs) (y ∷ ys) = (x ∙ y) ∷ ♯ zipWith _∙_ (♭ xs) (♭ ys)

drop : ∀ {A} → ℕ → Stream A → Stream A
drop zero    xs       = xs
drop (suc n) (x ∷ xs) = drop n (♭ xs)

repeat : ∀ {A} → A → Stream A
repeat x = x ∷ ♯ repeat x

iterate : ∀ {A} → (A → A) → A → Stream A
iterate f x = x ∷ ♯ iterate f (f x)

-- Interleaves the two streams.

infixr 5 _⋎_

_⋎_ : ∀ {A} → Stream A → Stream A → Stream A
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)

mutual

  -- Takes every other element from the stream, starting with the
  -- first one.

  evens : ∀ {A} → Stream A → Stream A
  evens (x ∷ xs) = x ∷ ♯ odds (♭ xs)

  -- Takes every other element from the stream, starting with the
  -- second one.

  odds : ∀ {A} → Stream A → Stream A
  odds (x ∷ xs) = evens (♭ xs)