text:
module MJ.Examples.Exceptions where

open import Prelude
open import Data.Star
import Data.Vec.All as Vec∀
open import Data.List
open import Data.List.Any
open import Data.List.Membership.Propositional
open import Data.List.All hiding (lookup)
open import Data.Product hiding (Σ)
open import Relation.Binary.PropositionalEquality

open import MJ.Examples.Integer

open import MJ.Types
open import MJ.Classtable
open import MJ.Classtable.Code Σ
open import MJ.Syntax Σ
open import MJ.Syntax.Program Σ
open import MJ.Semantics Σ Lib
open import MJ.Semantics.Values Σ

-- Integer class body

caught : Prog int
caught = Lib , let
    x = (here refl)
    y = (there (here refl))
    v = (there (there (here refl)))
  in body
    (
      loc int
      ◅ loc (ref INT)
      ◅ loc (ref INT)
      ◅ asgn v (num 0)
      ◅ asgn x (new INT (num 9 ∷ []))
      ◅ asgn y (new INT (num 18 ∷ []))
      ◅ (try (block (
          -- perform a side effect on the heap: writing 18 to x's int field
          run (call (var x) "set" {_}{void} (var y ∷ []))
          -- raise the exception
          ◅ raise
          ◅ ε
        )) catch (block (
          -- read the 18 from x's field
          asgn v (call (var x) "get" [])
          ◅ ε
        )))
      ◅ ε
    )
    (var v)

uncaught : Prog int
uncaught = Lib , let
    x = (here refl)
    y = (there (here refl))
    v = (there (there (here refl)))
  in body
    (
      loc int
      ◅ loc (ref INT)
      ◅ loc (ref INT)
      ◅ asgn v (num 0)
      ◅ asgn x (new INT (num 9 ∷ []))
      ◅ asgn y (new INT (num 18 ∷ []))
      ◅ asgn v (call (var x) "get" [])
      ◅ raise
      ◅ ε
    )
    (var v)

test : caught ⇓⟨ 100 ⟩ (λ v → v ≡ num 18)
test = refl

test₂ : uncaught ⇓⟨ 100 ⟩! (λ μ e → e ≡ other)
test₂ = refl


text:
module STLC.Type.Relation where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)

open import STLC.Term
open import STLC.Type

open import STLC.Type.Context using (Ctxt)

open import Data.Vec using (_∷_; lookup)

open import Relation.Nullary using (¬_)

open import Relation.Binary.PropositionalEquality as Eq
  using (refl; _≡_; sym; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

infix 4 _⊢_⦂_

data _⊢_⦂_ { m n } (Γ : Ctxt m n) : Term m -> Type n -> Set where

  ⊢# : ∀ { x : Fin m }
    -- ---------------
    -> Γ ⊢ # x ⦂ lookup Γ x

  ⊢ƛ : ∀  { t τ₁ τ₂ }
    -> τ₁ ∷ Γ ⊢ t ⦂ τ₂
    -- -----------------
    -> Γ ⊢ ƛ t ⦂ τ₁ ⇒ τ₂

  ⊢_·_ : ∀ { t₁ t₂ τ₁ τ₂ }
    -> Γ ⊢ t₁ ⦂ τ₁ ⇒ τ₂
    -> Γ ⊢ t₂ ⦂ τ₁
    -- ------------------
    -> Γ ⊢ t₁ · t₂ ⦂ τ₂

_⊬_⦂_ : ∀ { m n } -> Ctxt m n -> Term m -> Type n -> Set
Γ ⊬ t ⦂ τ = ¬ (Γ ⊢ t ⦂ τ)

module Lemmas₀ where

  ⊢-subst : ∀ { m n } { Γ₁ Γ₂ : Ctxt m n } { t₁ t₂ : Term m } { τ₁ τ₂ : Type n }
    -> Γ₁ ≡ Γ₂ -> t₁ ≡ t₂ -> τ₁ ≡ τ₂ -> Γ₁ ⊢ t₁ ⦂ τ₁ -> Γ₂ ⊢ t₂ ⦂ τ₂
  ⊢-subst refl refl refl hyp = hyp

  ⊢-Γ-subst : ∀ { m n } { Γ₁ Γ₂ : Ctxt m n } { t : Term m } { τ : Type n }
    -> Γ₁ ≡ Γ₂ -> Γ₁ ⊢ t ⦂ τ -> Γ₂ ⊢ t ⦂ τ
  ⊢-Γ-subst ≡-Γ hyp = ⊢-subst ≡-Γ refl refl hyp

  ⊢-τ-subst : ∀ { m n } { Γ : Ctxt m n } { t : Term m } { τ₁ τ₂ : Type n }
    -> τ₁ ≡ τ₂ -> Γ ⊢ t ⦂ τ₁ -> Γ ⊢ t ⦂ τ₂
  ⊢-τ-subst ≡-τ hyp = ⊢-subst refl refl ≡-τ hyp

-- TODO: Substitutions on typing derivations
-- TODO: Equivalent for Value e.g. value ⦂ τ relation w/ some lemmas :)

ext: agda

max_stars_repo_name: johnyob/agda-types

max_issues_repo_name: johnyob/agda-types

max_forks_repo_name: johnyob/agda-types


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data Ix : Set where
  ix : .(i : Nat) (n : Nat) → Ix

data D : Ix → Set where
  mkD : ∀ n → D (ix n n)

data ΣD : Set where
  _,_ : ∀ i → D i → ΣD

foo : ΣD → Nat
foo (i , mkD n) = n

d :  ΣD
d = ix 0 6 , mkD 6

-- Check that we pick the right (the non-irrelevant) `n` when binding
-- the forced argument.
check : foo d ≡ 6
check = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Reverse view
------------------------------------------------------------------------

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

module Data.List.Reverse where

open import Data.List.Base as L hiding (reverse)
open import Data.List.Properties
open import Function
open import Relation.Binary.PropositionalEquality

-- If you want to traverse a list from the end, then you can use the
-- reverse view of it.

infixl 5 _∶_∶ʳ_

data Reverse {a} {A : Set a} : List A → Set a where
  []     : Reverse []
  _∶_∶ʳ_ : ∀ xs (rs : Reverse xs) (x : A) → Reverse (xs ∷ʳ x)

module _ {a} {A : Set a} where

  reverse : (xs : List A) → Reverse (L.reverse xs)
  reverse []       = []
  reverse (x ∷ xs) = cast $ _ ∶ reverse xs ∶ʳ x where
    cast = subst Reverse (sym $ unfold-reverse x xs)

  reverseView : (xs : List A) → Reverse xs
  reverseView xs = cast $ reverse (L.reverse xs) where
    cast = subst Reverse (reverse-involutive xs)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decidable propositional membership over vectors
------------------------------------------------------------------------

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

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; decSetoid)

module Data.Vec.Membership.DecPropositional
  {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) where

------------------------------------------------------------------------
-- Re-export contents of propositional membership

open import Data.Vec.Membership.Propositional {A = A} public
open import Data.Vec.Membership.DecSetoid (decSetoid _≟_) public
  using (_∈?_)


text:
------------------------------------------------------------------------
-- Encodings and properties of higher-order extrema and intervals in
-- Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Typing.Encodings where

open import Data.Fin using (zero)
open import Data.Fin.Substitution using (Sub; Lift; TermSubst)
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (suc)
open import Data.Product using (_,_; proj₁; proj₂; _×_)
open import Relation.Binary.PropositionalEquality hiding ([_])

open import FOmegaInt.Syntax
open import FOmegaInt.Typing
open import FOmegaInt.Typing.Validity

open Syntax
open TermCtx
open Substitution hiding (subst; _/_; _Kind/_)
open Typing
open TypedSubstitution
open TypedNarrowing

----------------------------------------------------------------------
-- Injection of shapes into kinds.

-- For every shape `k' there is a kind `⌈ k ⌉' that erases/simplifies
-- back to `k', i.e. `⌈_⌉' is a right inverse of kind erasure `⌊_⌋'.
--
-- NOTE. The definition of the injection `⌈_⌉' is rather intuitive,
-- but it is neither the only right inverse of `⌊_⌋', nor even the
-- "most canonical" one.  Below we define two alternatives `⌈_⌉↓' and
-- `⌈_⌉↑' which, in addition to being right-inverse to `⌊_⌋', have
-- some appealing order-theoretic properties.

⌈_⌉ : ∀ {n} → SKind → Kind Term n
⌈ ★     ⌉ = *
⌈ j ⇒ k ⌉ = Π ⌈ j ⌉ ⌈ k ⌉

⌊⌋∘⌈⌉-id : ∀ {n} k → ⌊ ⌈_⌉ {n} k ⌋ ≡ k
⌊⌋∘⌈⌉-id ★       = refl
⌊⌋∘⌈⌉-id (j ⇒ k) = cong₂ _⇒_ (⌊⌋∘⌈⌉-id j) (⌊⌋∘⌈⌉-id k)

-- The kind `⌈ k ⌉' is well-formed (in any well-formed context).

⌈⌉-kd : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢ ⌈ k ⌉ kd
⌈⌉-kd ★       Γ-ctx = *-kd Γ-ctx
⌈⌉-kd (j ⇒ k) Γ-ctx =
  let ⌈j⌉-kd = ⌈⌉-kd j Γ-ctx
  in kd-Π ⌈j⌉-kd (⌈⌉-kd k (wf-kd ⌈j⌉-kd ∷ Γ-ctx))

----------------------------------------------------------------------
-- Encodings and properties of extremal kinds.

-- The empty interval (note the use of absurd bounds).

∅ : ∀ {n} → Kind Term n
∅ = ⊤ ⋯ ⊥

-- Well-formedness of the empty interval kind.

∅-kd : ∀ {n} {Γ : Ctx n} → Γ ctx → Γ ⊢ ∅ kd
∅-kd Γ-ctx = kd-⋯ (∈-⊤-f Γ-ctx) (∈-⊥-f Γ-ctx)

-- Right-inverses of kind simplification: for every shape `k' there
-- are two canonical kinds `⌈ k ⌉↓' and `⌈ k ⌉↑', such that
--
--  1. `⌈_⌉↓' and `⌈_⌉↑' are right-inverses for `⌊_⌋', i.e. `⌈ k ⌉↓'
--     and `⌈ k ⌉↑' both simplify to `k',
--
--  2. `⌈ k ⌉↓' and `⌈ k ⌉↑' are limits, i.e. they are the least
--     resp. greatest kinds for which 1 holds.
--
-- NOTE. Rather than thinking of `⌈_⌉↓' and `⌈_⌉↑' as right-inverses
-- of kind simplifications, one may instead think of `⌊_⌋' as defining
-- a "kind space" `S(k, Γ) = { j | ⌊ j ⌋ ≡ k, Γ ⊢ j kd }' ordered by
-- subkinding, and interpret `⌈ k ⌉↓' and `⌈ k ⌉↑' as the extrema of
-- the space `S(k, Γ)' associated with `k'.

mutual

  ⌈_⌉↓ : ∀ {n} → SKind → Kind Term n
  ⌈ ★     ⌉↓ = ∅
  ⌈ j ⇒ k ⌉↓ = Π ⌈ j ⌉↑ ⌈ k ⌉↓

  ⌈_⌉↑ : ∀ {n} → SKind → Kind Term n
  ⌈ ★     ⌉↑ = *
  ⌈ j ⇒ k ⌉↑ = Π ⌈ j ⌉↓ ⌈ k ⌉↑

mutual

  -- Proof of point 1 above: `⌈_⌉↓' and `⌈_⌉↑' are right-inverses of
  -- `⌊_⌋'.

  ⌊⌋∘⌈⌉↓-id : ∀ {n} k → ⌊ ⌈_⌉↓ {n} k ⌋ ≡ k
  ⌊⌋∘⌈⌉↓-id ★       = refl
  ⌊⌋∘⌈⌉↓-id (j ⇒ k) = cong₂ _⇒_ (⌊⌋∘⌈⌉↑-id j) (⌊⌋∘⌈⌉↓-id k)

  ⌊⌋∘⌈⌉↑-id : ∀ {n} k → ⌊ ⌈_⌉↑ {n} k ⌋ ≡ k
  ⌊⌋∘⌈⌉↑-id ★       = refl
  ⌊⌋∘⌈⌉↑-id (j ⇒ k) = cong₂ _⇒_ (⌊⌋∘⌈⌉↓-id j) (⌊⌋∘⌈⌉↑-id k)

mutual

  -- `⌈ k ⌉↓' and `⌈ k ⌉↑' are well-formed (in any well-formed
  -- context).

  ⌈⌉↓-kd : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢ ⌈ k ⌉↓ kd
  ⌈⌉↓-kd ★       Γ-ctx = ∅-kd Γ-ctx
  ⌈⌉↓-kd (j ⇒ k) Γ-ctx =
    let ⌈j⌉↑-kd = ⌈⌉↑-kd j Γ-ctx
    in kd-Π ⌈j⌉↑-kd (⌈⌉↓-kd k (wf-kd ⌈j⌉↑-kd ∷ Γ-ctx))

  ⌈⌉↑-kd : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢ ⌈ k ⌉↑ kd
  ⌈⌉↑-kd ★       Γ-ctx = *-kd Γ-ctx
  ⌈⌉↑-kd (j ⇒ k) Γ-ctx =
    let ⌈j⌉↓-kd = ⌈⌉↓-kd j Γ-ctx
    in kd-Π ⌈j⌉↓-kd (⌈⌉↑-kd k (wf-kd ⌈j⌉↓-kd ∷ Γ-ctx))

mutual

  -- Proof of point 2 above: `⌈ k ⌉↓' and `⌈ k ⌉↑' are the least
  -- resp. greatest (well-formed) kinds that have shape `k'.

  ⌈⌉↑-maximum : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ k <∷ ⌈ ⌊ k ⌋ ⌉↑
  ⌈⌉↑-maximum (kd-⋯ a∈* b∈*)       = <∷-⋯ (<:-⊥ a∈*) (<:-⊤ b∈*)
  ⌈⌉↑-maximum (kd-Π {j} j-kd k-kd) =
    let ⌈⌊j⌋⌉↓<∷j = ⌈⌉↓-minimum j-kd
    in <∷-Π ⌈⌊j⌋⌉↓<∷j (⌈⌉↑-maximum (⇓-kd ⌈⌊j⌋⌉↓<∷j k-kd))
            (kd-Π j-kd k-kd)

  ⌈⌉↓-minimum : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ ⌈ ⌊ k ⌋ ⌉↓ <∷ k
  ⌈⌉↓-minimum (kd-⋯ a∈* b∈*)   = <∷-⋯ (<:-⊤ a∈*) (<:-⊥ b∈*)
  ⌈⌉↓-minimum (kd-Π {j} {k} j-kd k-kd) =
    <∷-Π (⌈⌉↑-maximum j-kd) (⌈⌉↓-minimum k-kd) (⌈⌉↓-kd ⌊ Π j k ⌋ (kd-ctx j-kd))

-- Some corollaries.

-- Minima are subkinds of maxima.

⌈⌉↓<∷⌈⌉↑ : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢ ⌈ k ⌉↓ <∷ ⌈ k ⌉↑
⌈⌉↓<∷⌈⌉↑ k Γ-ctx =
  subst (_ ⊢ ⌈ k ⌉↓ <∷_) (cong ⌈_⌉↑ (⌊⌋∘⌈⌉↓-id k))
        (⌈⌉↑-maximum (⌈⌉↓-kd k Γ-ctx))

-- Minima are subkinds of the "intuitively" injected shapes.

⌈⌉↓<∷⌈⌉ : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢ ⌈ k ⌉↓ <∷ ⌈ k ⌉
⌈⌉↓<∷⌈⌉ k Γ-ctx =
  subst (_ ⊢_<∷ ⌈ k ⌉) (cong ⌈_⌉↓ (⌊⌋∘⌈⌉-id k))
        (⌈⌉↓-minimum (⌈⌉-kd k Γ-ctx))

-- Maxima are superkinds of the "intuitively" injected shapes.

⌈⌉<∷⌈⌉↑ : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢ ⌈ k ⌉ <∷ ⌈ k ⌉↑
⌈⌉<∷⌈⌉↑ k Γ-ctx =
  subst (_ ⊢ ⌈ k ⌉ <∷_) (cong ⌈_⌉↑ (⌊⌋∘⌈⌉-id k))
        (⌈⌉↑-maximum (⌈⌉-kd k Γ-ctx))

-- Every well-kinded type inhabits the maximum kind associated with
-- its shape.

∈-⇑-⌈⌉↑ : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ ⊢Tp a ∈ ⌈ ⌊ k ⌋ ⌉↑
∈-⇑-⌈⌉↑ a∈k = ∈-⇑ a∈k (⌈⌉↑-maximum (Tp∈-valid a∈k))

----------------------------------------------------------------------
-- Encodings and properties of higher-order extrema

-- Higher-order extremal types, indexed by shapes.
--
-- NOTE. We will define a variant of the higher-order extrema indexed
-- by possibly dependent kinds below.

⊥⟨_⟩ : ∀ {n} → SKind → Term n
⊥⟨ ★ ⟩     = ⊥
⊥⟨ j ⇒ k ⟩ = Λ ⌈ j ⌉ ⊥⟨ k ⟩

⊤⟨_⟩ : ∀ {n} → SKind → Term n
⊤⟨ ★ ⟩     = ⊤
⊤⟨ j ⇒ k ⟩ = Λ ⌈ j ⌉ ⊤⟨ k ⟩

-- ⊥⟨ k ⟩ and ⊤⟨ k ⟩ inhabit ⌈ k ⌉.

∈-⊥⟨⟩ : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢Tp ⊥⟨ k ⟩ ∈ ⌈ k ⌉
∈-⊥⟨⟩ ★       Γ-ctx = ∈-⊥-f Γ-ctx
∈-⊥⟨⟩ (j ⇒ k) Γ-ctx =
  let ⌈j⌉-kd = ⌈⌉-kd j Γ-ctx
      ⌈j⌉∷Γ  = wf-kd ⌈j⌉-kd ∷ Γ-ctx
  in ∈-Π-i ⌈j⌉-kd (∈-⊥⟨⟩ k ⌈j⌉∷Γ)

∈-⊤⟨⟩ : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢Tp ⊤⟨ k ⟩ ∈ ⌈ k ⌉
∈-⊤⟨⟩ ★       Γ-ctx = ∈-⊤-f Γ-ctx
∈-⊤⟨⟩ (j ⇒ k) Γ-ctx =
  let ⌈j⌉-kd = ⌈⌉-kd j Γ-ctx
      ⌈j⌉∷Γ  = wf-kd ⌈j⌉-kd ∷ Γ-ctx
  in ∈-Π-i ⌈j⌉-kd (∈-⊤⟨⟩ k ⌈j⌉∷Γ)

-- ⊥⟨ k ⟩ and ⊤⟨ k ⟩ are extremal types in ⌈ k ⌉.

⊥⟨⟩-minimum : ∀ {n} {Γ : Ctx n} {a k} →
              Γ ⊢Tp a ∈ ⌈ k ⌉ → Γ ⊢ ⊥⟨ k ⟩ <: a ∈ ⌈ k ⌉
⊥⟨⟩-minimum {k = ★    } a∈*     = <:-⊥ a∈*
⊥⟨⟩-minimum {k = j ⇒ k} a∈⌈j⇒k⌉ =
  <:-trans (<:-λ (⊥⟨⟩-minimum a·z∈⌈k⌉) (∈-⊥⟨⟩ (j ⇒ k) Γ-ctx) Λa·z∈⌈j⇒k⌉)
           (<:-η₁ a∈⌈j⇒k⌉)
  where
    Γ-ctx  = Tp∈-ctx a∈⌈j⇒k⌉
    Λa·z∈⌈j⇒k⌉ = Tp∈-η a∈⌈j⇒k⌉
    a·z∈⌈k⌉    = proj₂ (Tp∈-Λ-inv Λa·z∈⌈j⇒k⌉)

⊤⟨⟩-maximum : ∀ {n} {Γ : Ctx n} {a k} →
              Γ ⊢Tp a ∈ ⌈ k ⌉ → Γ ⊢ a <: ⊤⟨ k ⟩ ∈ ⌈ k ⌉
⊤⟨⟩-maximum {k = ★    } a∈*     = <:-⊤ a∈*
⊤⟨⟩-maximum {k = j ⇒ k} a∈⌈j⇒k⌉ =
  <:-trans (<:-η₂ a∈⌈j⇒k⌉)
           (<:-λ (⊤⟨⟩-maximum a·z∈⌈k⌉) Λa·z∈⌈j⇒k⌉ (∈-⊤⟨⟩ (j ⇒ k) Γ-ctx))
  where
    Γ-ctx  = Tp∈-ctx a∈⌈j⇒k⌉
    Λa·z∈⌈j⇒k⌉ = Tp∈-η a∈⌈j⇒k⌉
    a·z∈⌈k⌉    = proj₂ (Tp∈-Λ-inv Λa·z∈⌈j⇒k⌉)

-- An alternate pair of higher-order extremal types inhabiting the
-- family of kinds ⌈ k ⌉↑, rather than ⌈ k ⌉.

⊥↑⟨_⟩ : ∀ {n} → SKind → Term n
⊥↑⟨ ★ ⟩     = ⊥
⊥↑⟨ j ⇒ k ⟩ = Λ ⌈ j ⌉↑ ⊥↑⟨ k ⟩

⊤↑⟨_⟩ : ∀ {n} → SKind → Term n
⊤↑⟨ ★ ⟩     = ⊤
⊤↑⟨ j ⇒ k ⟩ = Λ ⌈ j ⌉↑ ⊤↑⟨ k ⟩

-- ⊥↑⟨ k ⟩ and ⊤↑⟨ k ⟩ inhabit ⌈ k ⌉↑.

∈-⊥↑⟨⟩ : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢Tp ⊥↑⟨ k ⟩ ∈ ⌈ k ⌉↑
∈-⊥↑⟨⟩ ★       Γ-ctx = ∈-⊥-f Γ-ctx
∈-⊥↑⟨⟩ (j ⇒ k) Γ-ctx =
  let ⌈j⌉↑-kd = ⌈⌉↑-kd j Γ-ctx
      ⌈j⌉↑∷Γ  = wf-kd ⌈j⌉↑-kd ∷ Γ-ctx
      ⌈k⌉↑-kd = ⌈⌉↑-kd k ⌈j⌉↑∷Γ
  in ∈-⇑ (∈-Π-i ⌈j⌉↑-kd (∈-⊥↑⟨⟩ k ⌈j⌉↑∷Γ))
         (<∷-Π (⌈⌉↓<∷⌈⌉↑ j Γ-ctx)
               (<∷-refl (⌈⌉↑-kd k ((wf-kd (⌈⌉↓-kd j Γ-ctx)) ∷ Γ-ctx)))
               (kd-Π ⌈j⌉↑-kd ⌈k⌉↑-kd))

∈-⊤↑⟨⟩ : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢Tp ⊤↑⟨ k ⟩ ∈ ⌈ k ⌉↑
∈-⊤↑⟨⟩ ★       Γ-ctx = ∈-⊤-f Γ-ctx
∈-⊤↑⟨⟩ (j ⇒ k) Γ-ctx =
  let ⌈j⌉↑-kd = ⌈⌉↑-kd j Γ-ctx
      ⌈j⌉↑∷Γ  = wf-kd ⌈j⌉↑-kd ∷ Γ-ctx
      ⌈k⌉↑-kd = ⌈⌉↑-kd k ⌈j⌉↑∷Γ
  in ∈-⇑ (∈-Π-i ⌈j⌉↑-kd (∈-⊤↑⟨⟩ k ⌈j⌉↑∷Γ))
         (<∷-Π (⌈⌉↓<∷⌈⌉↑ j Γ-ctx)
               (<∷-refl (⌈⌉↑-kd k ((wf-kd (⌈⌉↓-kd j Γ-ctx)) ∷ Γ-ctx)))
               (kd-Π ⌈j⌉↑-kd ⌈k⌉↑-kd))

-- ⊥↑⟨ k ⟩ and ⊤↑⟨ k ⟩ are extremal types in ⌈ k ⌉↑.

⊥↑⟨⟩-minimum : ∀ {n} {Γ : Ctx n} {a k} →
               Γ ⊢Tp a ∈ k → Γ ⊢ ⊥↑⟨ ⌊ k ⌋ ⟩ <: a ∈ ⌈ ⌊ k ⌋ ⌉↑
⊥↑⟨⟩-minimum {k = b ⋯ c} a∈b⋯c = <:-⊥ a∈b⋯c
⊥↑⟨⟩-minimum {k = Π j k} a∈Πjk with Tp∈-valid a∈Πjk
... | kd-Π j-kd k-kd =
  <:-trans (<:-λ (⊥↑⟨⟩-minimum a·z∈k′) (∈-⊥↑⟨⟩ ⌊ Π j k ⌋ Γ-ctx)
                 (∈-⇑ Λa·z∈Πjk Πjk<∷⌈Πjk⌉↑))
           (<:-⇑ (<:-η₁ a∈Πjk) Πjk<∷⌈Πjk⌉↑)
  where
    Πjk<∷⌈Πjk⌉↑ = ⌈⌉↑-maximum (kd-Π j-kd k-kd)
    Γ-ctx       = Tp∈-ctx a∈Πjk
    ⌈⌊j⌋⌉↓<∷j   = ⌈⌉↓-minimum j-kd
    Λa·z∈Πjk    = Tp∈-η a∈Πjk
    a·z∈k       = proj₂ (Tp∈-Λ-inv Λa·z∈Πjk)
    a·z∈k′      = ⇓-Tp∈ ⌈⌊j⌋⌉↓<∷j a·z∈k

⊤↑⟨⟩-maximum : ∀ {n} {Γ : Ctx n} {a k} →
               Γ ⊢Tp a ∈ k → Γ ⊢ a <: ⊤↑⟨ ⌊ k ⌋ ⟩ ∈ ⌈ ⌊ k ⌋ ⌉↑
⊤↑⟨⟩-maximum {k = b ⋯ c} a∈b⋯c = <:-⊤ a∈b⋯c
⊤↑⟨⟩-maximum {k = Π j k} a∈Πjk with Tp∈-valid a∈Πjk
... | kd-Π j-kd k-kd =
  <:-trans (<:-⇑ (<:-η₂ a∈Πjk) Πjk<∷⌈Πjk⌉↑)
           (<:-λ (⊤↑⟨⟩-maximum a·z∈k′) (∈-⇑ Λa·z∈Πjk Πjk<∷⌈Πjk⌉↑)
                 (∈-⊤↑⟨⟩ ⌊ Π j k ⌋ Γ-ctx))
  where
    Πjk<∷⌈Πjk⌉↑ = ⌈⌉↑-maximum (kd-Π j-kd k-kd)
    Γ-ctx       = Tp∈-ctx a∈Πjk
    ⌈⌊j⌋⌉↓<∷j   = ⌈⌉↓-minimum j-kd
    Λa·z∈Πjk    = Tp∈-η a∈Πjk
    a·z∈k       = proj₂ (Tp∈-Λ-inv Λa·z∈Πjk)
    a·z∈k′      = ⇓-Tp∈ ⌈⌊j⌋⌉↓<∷j a·z∈k

-- Yet another variant of higher-order extremal types, this time
-- indexed by possibly dependent kinds.

⊥′⟨_⟩ : ∀ {n} → Kind Term n → Term n
⊥′⟨ a ⋯ b ⟩ = ⊥
⊥′⟨ Π j k ⟩ = Λ j ⊥′⟨ k ⟩

⊤′⟨_⟩ : ∀ {n} → Kind Term n → Term n
⊤′⟨ a ⋯ b ⟩ = ⊤
⊤′⟨ Π j k ⟩ = Λ j ⊤′⟨ k ⟩

-- A higher-order variant of *.

*⟨_⟩ : ∀ {n} → Kind Term n → Kind Term n
*⟨ a ⋯ b ⟩ = *
*⟨ Π j k ⟩ = Π j *⟨ k ⟩

-- Substitution commutes with ⊥′⟨_⟩, ⊤′⟨_⟩ and *⟨_⟩.

module EncSubstLemmas {T} (l : Lift T Term) where
  open SubstApp l
  open Lift l hiding (var)

  ⊥′⟨⟩-/ : ∀ {n m} {σ : Sub T m n} k → ⊥′⟨ k ⟩ / σ ≡ ⊥′⟨ k Kind/ σ ⟩
  ⊥′⟨⟩-/ (a ⋯ b) = refl
  ⊥′⟨⟩-/ (Π j k) = cong (Λ _) (⊥′⟨⟩-/ k)

  ⊤′⟨⟩-/ : ∀ {n m} {σ : Sub T m n} k → ⊤′⟨ k ⟩ / σ ≡ ⊤′⟨ k Kind/ σ ⟩
  ⊤′⟨⟩-/ (a ⋯ b) = refl
  ⊤′⟨⟩-/ (Π j k) = cong (Λ _) (⊤′⟨⟩-/ k)

  *⟨⟩-/ : ∀ {n m} {σ : Sub T m n} k → *⟨ k ⟩ Kind/ σ ≡ *⟨ k Kind/ σ ⟩
  *⟨⟩-/ (a ⋯ b) = refl
  *⟨⟩-/ (Π j k) = cong (Π _) (*⟨⟩-/ k)

open EncSubstLemmas (TermSubst.termLift termSubst) public
open EncSubstLemmas (TermSubst.varLift  termSubst) public
  renaming (⊥′⟨⟩-/ to ⊥′⟨⟩-/Var; ⊤′⟨⟩-/ to ⊤′⟨⟩-/Var; *⟨⟩-/ to *⟨⟩-/Var)

-- Well-formedness of higher-order star kinds.

kd-*⟨⟩ : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ *⟨ k ⟩ kd
kd-*⟨⟩ (kd-⋯ a∈* b∈*)   = *-kd (Tp∈-ctx a∈*)
kd-*⟨⟩ (kd-Π j-kd k-kd) = kd-Π j-kd (kd-*⟨⟩ k-kd)

-- ⊥′⟨ k ⟩ and ⊤′⟨ k ⟩ inhabit *⟨ k ⟩.

∈-⊥′⟨⟩ : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢Tp ⊥′⟨ k ⟩ ∈ *⟨ k ⟩
∈-⊥′⟨⟩ (kd-⋯ a∈* b∈*)   = ∈-⊥-f (Tp∈-ctx a∈*)
∈-⊥′⟨⟩ (kd-Π j-kd k-kd) = ∈-Π-i j-kd (∈-⊥′⟨⟩ k-kd)

∈-⊤′⟨⟩ : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢Tp ⊤′⟨ k ⟩ ∈ *⟨ k ⟩
∈-⊤′⟨⟩ (kd-⋯ a∈* b∈*)   = ∈-⊤-f (Tp∈-ctx a∈*)
∈-⊤′⟨⟩ (kd-Π j-kd k-kd) = ∈-Π-i j-kd (∈-⊤′⟨⟩ k-kd)

-- A helper: any well-formed kind k is a subkind of *⟨ k ⟩.

*⟨⟩-maximum : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ k <∷ *⟨ k ⟩
*⟨⟩-maximum (kd-⋯ a∈* b∈*)   = <∷-⋯ (<:-⊥ a∈*) (<:-⊤ b∈*)
*⟨⟩-maximum (kd-Π j-kd k-kd) =
  <∷-Π (<∷-refl j-kd) (*⟨⟩-maximum k-kd) (kd-Π j-kd k-kd)

-- ⊥′⟨ k ⟩ and ⊤′⟨ k ⟩ are extremal types in *⟨ k ⟩.

⊥′⟨⟩-minimum : ∀ {n} {Γ : Ctx n} {a k} →
               Γ ⊢Tp a ∈ k → Γ ⊢ ⊥′⟨ k ⟩ <: a ∈ *⟨ k ⟩
⊥′⟨⟩-minimum {k = b ⋯ c} a∈b⋯c = <:-⊥ a∈b⋯c
⊥′⟨⟩-minimum {k = Π j k} a∈Πjk =
  <:-trans (<:-λ (⊥′⟨⟩-minimum a·z∈k) (∈-⊥′⟨⟩ Πjk-kd)
                 (∈-⇑ Λa·z∈Πjk Πjk-kd<∷*⟨Πjk⟩))
           (<:-η₁ (∈-⇑ a∈Πjk Πjk-kd<∷*⟨Πjk⟩))
  where
    Λa·z∈Πjk       = Tp∈-η a∈Πjk
    a·z∈k          = proj₂ (Tp∈-Λ-inv Λa·z∈Πjk)
    Πjk-kd         = Tp∈-valid a∈Πjk
    Πjk-kd<∷*⟨Πjk⟩ = *⟨⟩-maximum Πjk-kd

⊤′⟨⟩-maximum : ∀ {n} {Γ : Ctx n} {a k} →
               Γ ⊢Tp a ∈ k → Γ ⊢ a <: ⊤′⟨ k ⟩ ∈ *⟨ k ⟩
⊤′⟨⟩-maximum {k = b ⋯ c} a∈b⋯c = <:-⊤ a∈b⋯c
⊤′⟨⟩-maximum {k = Π j k} a∈Πjk =
  <:-trans (<:-η₂ (∈-⇑ a∈Πjk Πjk-kd<∷*⟨Πjk⟩))
           (<:-λ (⊤′⟨⟩-maximum a·z∈k) (∈-⇑ Λa·z∈Πjk Πjk-kd<∷*⟨Πjk⟩)
                 (∈-⊤′⟨⟩ Πjk-kd))
  where
    Λa·z∈Πjk       = Tp∈-η a∈Πjk
    a·z∈k          = proj₂ (Tp∈-Λ-inv Λa·z∈Πjk)
    Πjk-kd         = Tp∈-valid a∈Πjk
    Πjk-kd<∷*⟨Πjk⟩ = *⟨⟩-maximum Πjk-kd

-- Applications of higher-order extrema result in lower-order extrema.

≃-⊥′⟨⟩-· : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢ Π j k kd → Γ ⊢Tp a ∈ j →
           Γ ⊢ ⊥′⟨ Π j k ⟩ · a ≃ ⊥′⟨ k Kind[ a ] ⟩ ∈ *⟨ k Kind[ a ] ⟩
≃-⊥′⟨⟩-· (kd-Π {j} {k} j-kd k-kd) a∈j =
  subst₂ (_ ⊢ ⊥′⟨ Π j k ⟩ · _ ≃_∈_) (⊥′⟨⟩-/ _) (*⟨⟩-/ _)
         (≃-β′ ⊥⟨k⟩ a∈j ⊥⟨Πjk⟩)
  where
    ⊥⟨Πjk⟩ = ∈-⊥′⟨⟩ (kd-Π j-kd k-kd)
    ⊥⟨k⟩   = ∈-⊥′⟨⟩ k-kd

≃-⊤′⟨⟩-· : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢ Π j k kd → Γ ⊢Tp a ∈ j →
           Γ ⊢ ⊤′⟨ Π j k ⟩ · a ≃ ⊤′⟨ k Kind[ a ] ⟩ ∈ *⟨ k Kind[ a ] ⟩
≃-⊤′⟨⟩-· (kd-Π {j} {k} j-kd k-kd) a∈j =
  subst₂ (_ ⊢ ⊤′⟨ Π j k ⟩ · _ ≃_∈_) (⊤′⟨⟩-/ _) (*⟨⟩-/ _)
         (≃-β′ ⊤⟨k⟩ a∈j ⊤⟨Πjk⟩)
  where
    ⊤⟨Πjk⟩ = ∈-⊤′⟨⟩ (kd-Π j-kd k-kd)
    ⊤⟨k⟩   = ∈-⊤′⟨⟩ k-kd

----------------------------------------------------------------------
-- Encodings and properties of higher-order intervals

infix 6 _⋯⟨_⟩_

-- Higher-order interval kinds.

_⋯⟨_⟩_ : ∀ {n} → Term n → Kind Term n → Term n → Kind Term n
a ⋯⟨ c ⋯ d ⟩ b = a ⋯ b
a ⋯⟨ Π j k ⟩ b = Π j (weaken a · var zero ⋯⟨ k ⟩ weaken b · var zero)

-- Higher order interval kinds have the same shape as their
-- kind-indices.

⌊⌋-⋯⟨⟩ : ∀ {n} {a b : Term n} k → ⌊ a ⋯⟨ k ⟩ b ⌋ ≡ ⌊ k ⌋
⌊⌋-⋯⟨⟩ (a ⋯ b) = refl
⌊⌋-⋯⟨⟩ (Π j k) = cong (⌊ j ⌋ ⇒_) (⌊⌋-⋯⟨⟩ k)

-- "Idempotence" of higher order interval kinds.

⋯⟨⟩-idempotent : ∀ {n} {a b : Term n} k → a ⋯⟨ a ⋯⟨ k ⟩ b ⟩ b ≡ a ⋯⟨ k ⟩ b
⋯⟨⟩-idempotent (a ⋯ b) = refl
⋯⟨⟩-idempotent (Π j k) = cong (Π j) (⋯⟨⟩-idempotent k)

-- Well-formedness of higher-order interval kinds.

kd-⋯⟨⟩ : ∀ {n} {Γ : Ctx n} {a b k} →
         Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ k → Γ ⊢ a ⋯⟨ k ⟩ b kd
kd-⋯⟨⟩ a∈k   b∈k   with Tp∈-valid a∈k
kd-⋯⟨⟩ a∈c⋯d b∈c⋯d | kd-⋯ _ _       = kd-⋯ (Tp∈-⋯-* a∈c⋯d) (Tp∈-⋯-* b∈c⋯d)
kd-⋯⟨⟩ a∈Πjk b∈Πjk | kd-Π j-kd k-kd =
  kd-Π j-kd (kd-⋯⟨⟩ a·z∈k b·z∈k)
  where
    a·z∈k = proj₂ (Tp∈-Λ-inv (Tp∈-η a∈Πjk))
    b·z∈k = proj₂ (Tp∈-Λ-inv (Tp∈-η b∈Πjk))

-- NOTE.  We would like to show that the inverse of the above also
-- holds, i.e. that given a well-formed higher-order interval kind `a
-- ⋯⟨ k ⟩ b', we have `a ∈ k' and `b ∈ k'.  Unfortunately this is not
-- true because the definition of `a ⋯⟨ k ⟩ b' is a bit too forgetful
-- when the kind-index `k' is itself an interval `k = c ⋯ d', that is,
-- when `a' and `b' are proper types.  E.g. the kind `⊥ ⋯⟨ ∅ ⟩ ⊤' is
-- well-formed, but clearly `⊥ , ⊤ ∉ ø'.
--
-- However, as the following lemma illustrates, we can invert some
-- judgments about higher-order intervals with "sensible" kind
-- indices, such as those resulting from shapes via ⌈_⌉.  Still, a
-- proper inversion lemma would require more work, in particular one
-- has to contract the kinding derivations of the η-expanded bounds
-- `a' and `b' back into their non-expanded form.

-- Higher-order interval kinds indexed by `⌈ k ⌉' for some `k' are
-- subkinds of `⌈ k ⌉'.

⋯⟨⌈⌉⟩-<∷-⌈⌉ : ∀ {n} {Γ : Ctx n} {a b k} →
              Γ ⊢ a ⋯⟨ ⌈ k ⌉ ⟩ b kd → Γ ⊢ a ⋯⟨ ⌈ k ⌉ ⟩ b <∷ ⌈ k ⌉
⋯⟨⌈⌉⟩-<∷-⌈⌉ {k = ★    } (kd-⋯ a∈* b∈*) = <∷-⋯ (<:-⊥ a∈*) (<:-⊤ b∈*)
⋯⟨⌈⌉⟩-<∷-⌈⌉ {k = j ⇒ k} (kd-Π ⌈j⌉-kd a·z⋯⟨⌈k⌉⟩b·z-kd) =
  <∷-Π (<∷-refl ⌈j⌉-kd) (⋯⟨⌈⌉⟩-<∷-⌈⌉ a·z⋯⟨⌈k⌉⟩b·z-kd)
       (kd-Π ⌈j⌉-kd a·z⋯⟨⌈k⌉⟩b·z-kd)

-- Two corollaries.

-- Types inhabiting a type interval indexed by a shape `k' also
-- inhabit `⌈ k ⌉`.

Tp∈-⋯⟨⌈⌉⟩-inv : ∀ {n} {Γ : Ctx n} {a b c k} →
                Γ ⊢Tp a ∈ b ⋯⟨ ⌈ k ⌉ ⟩ c → Γ ⊢Tp a ∈ ⌈ k ⌉
Tp∈-⋯⟨⌈⌉⟩-inv a∈b⋯⟨⌈k⌉⟩c =
  ∈-⇑ a∈b⋯⟨⌈k⌉⟩c (⋯⟨⌈⌉⟩-<∷-⌈⌉ (Tp∈-valid a∈b⋯⟨⌈k⌉⟩c))

-- Types related in a type interval indexed by a shape `k' are also
-- related in `⌈ k ⌉`.

<:-⋯⟨⌈⌉⟩-inv : ∀ {n} {Γ : Ctx n} {a b c d k} →
               Γ ⊢ a <: b ∈ c ⋯⟨ ⌈ k ⌉ ⟩ d → Γ ⊢ a <: b ∈ ⌈ k ⌉
<:-⋯⟨⌈⌉⟩-inv a<:b∈c⋯⟨⌈k⌉⟩d =
  <:-⇑ a<:b∈c⋯⟨⌈k⌉⟩d (⋯⟨⌈⌉⟩-<∷-⌈⌉ (<:-valid-kd a<:b∈c⋯⟨⌈k⌉⟩d))

-- Subkinding of higher-order interval kinds.

<∷-⋯⟨⟩ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂ k} →
         Γ ⊢ a₂ <: a₁ ∈ k → Γ ⊢ b₁ <: b₂ ∈ k → Γ ⊢ a₁ ⋯⟨ k ⟩ b₁ <∷ a₂ ⋯⟨ k ⟩ b₂
<∷-⋯⟨⟩ a₂<:a₁∈k   b₁<:b₂∈k   with <:-valid-kd a₂<:a₁∈k
<∷-⋯⟨⟩ a₂<:a₁∈c⋯d b₁<:b₂∈c⋯d | kd-⋯ _ _ =
  <∷-⋯ (<:-⋯-* a₂<:a₁∈c⋯d) (<:-⋯-* b₁<:b₂∈c⋯d)
<∷-⋯⟨⟩ a₂<:a₁∈Πjk b₁<:b₂∈Πjk | kd-Π j-kd k-kd =
  let a₂∈Πjk , a₁∈Πjk = <:-valid a₂<:a₁∈Πjk
      b₁∈Πjk , b₂∈Πjk = <:-valid b₁<:b₂∈Πjk
      Γ-ctx   = kd-ctx j-kd
      j-wf    = wf-kd j-kd
      j∷Γ-ctx = j-wf ∷ Γ-ctx
      z∈k     = ∈-var zero j∷Γ-ctx refl
      z≃z∈k   = ≃-refl z∈k
      a₂<:a₁∈Πjk′ = <:-weaken j-wf a₂<:a₁∈Πjk
      b₁<:b₂∈Πjk′ = <:-weaken j-wf b₁<:b₂∈Πjk
      k[z]≡k      = Kind-wk↑-sub-zero-vanishes _
      a₂·z<:a₁·z∈k[z] = <:-· a₂<:a₁∈Πjk′ z≃z∈k
      b₁·z<:b₂·z∈k[z] = <:-· b₁<:b₂∈Πjk′ z≃z∈k
      a₂·z<:a₁·z∈k = subst (_ ⊢ _ <: _ ∈_) k[z]≡k a₂·z<:a₁·z∈k[z]
      b₁·z<:b₂·z∈k = subst (_ ⊢ _ <: _ ∈_) k[z]≡k b₁·z<:b₂·z∈k[z]
  in <∷-Π (<∷-refl j-kd)
          (<∷-⋯⟨⟩ a₂·z<:a₁·z∈k b₁·z<:b₂·z∈k)
          (kd-⋯⟨⟩ a₁∈Πjk b₁∈Πjk)

-- A corollary: equality of higher-order interval kinds.

≅-⋯⟨⟩ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂ k} →
        Γ ⊢ a₁ ≃ a₂ ∈ k → Γ ⊢ b₁ ≃ b₂ ∈ k → Γ ⊢ a₁ ⋯⟨ k ⟩ b₁ ≅ a₂ ⋯⟨ k ⟩ b₂
≅-⋯⟨⟩ (<:-antisym a₁<:a₂∈k a₂<:a₁∈k) (<:-antisym b₁<:b₂∈k b₂<:b₁∈k) =
  <∷-antisym (<∷-⋯⟨⟩ a₂<:a₁∈k b₁<:b₂∈k) (<∷-⋯⟨⟩ a₁<:a₂∈k b₂<:b₁∈k)

-- A variant of kind-driven η-expansion that only expands the head.

η-exp : ∀ {n} → Kind Term n → Term n → Term n
η-exp (_ ⋯ _) a = a
η-exp (Π j k) a = Λ j (η-exp k (weaken a · var zero))

-- Soundness of η-expansion.

≃-η-exp : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ ⊢ a ≃ η-exp k a ∈ k
≃-η-exp {_} {_} {_} {b ⋯ c} a∈b⋯c = ≃-refl a∈b⋯c
≃-η-exp {_} {_} {a} {Π j k} a∈Πjk with Tp∈-valid a∈Πjk
... | kd-Π j-kd k-kd = begin
  a                                     ≃⟨ ≃-sym (≃-η a∈Πjk) ⟩
  Λ j (weaken a · var zero)             ≃⟨ ≃-λ′ (≅-refl j-kd) (≃-η-exp a·z∈k) ⟩
  Λ j (η-exp k (weaken a · var zero))   ∎
  where
    open ≃-Reasoning
    a·z∈k = proj₂ (Tp∈-Λ-inv (Tp∈-η a∈Πjk))

-- A singleton introduction rule for higher-order interval kinds.

∈-s⟨⟩-i : ∀ {n} {Γ : Ctx n} {a k} →
          Γ ⊢Tp a ∈ k → Γ ⊢Tp η-exp k a ∈ a ⋯⟨ k ⟩ a
∈-s⟨⟩-i a∈k   with Tp∈-valid a∈k
∈-s⟨⟩-i a∈b⋯c | kd-⋯ _ _       = ∈-s-i a∈b⋯c
∈-s⟨⟩-i a∈Πjk | kd-Π j-kd k-kd =
  ∈-Π-i j-kd (∈-s⟨⟩-i a·z∈k)
  where
    a·z∈k = proj₂ (Tp∈-Λ-inv (Tp∈-η a∈Πjk))

-- A corollary: we can kind (the η-expansion of) a type with explicit
-- lower and uper bounds in the interval defined by these bounds.

Tp∈-<:-⋯ : ∀ {n} {Γ : Ctx n} {a b c k} →
           Γ ⊢ b <: a ∈ k → Γ ⊢ a <: c ∈ k → Γ ⊢Tp η-exp k a ∈ b ⋯⟨ k ⟩ c
Tp∈-<:-⋯ b<:a∈k a<:c∈k =
  ∈-⇑ (∈-s⟨⟩-i (proj₁ (<:-valid a<:c∈k))) (<∷-⋯⟨⟩ b<:a∈k a<:c∈k)

-- Bound projection rules for higher-order intervals.
--
-- NOTE.  These lemmas are a bit weaker than one might like.  In
-- particular, the additional premises `Γ ⊢ a , b , c ∈ k' might seem
-- redundant.  But recall that we cannot, in general, invert
-- well-formed higher-order intervals, i.e. `Γ ⊢ b ⋯⟨ k ⟩ c kd' does
-- *not* imply `Γ ⊢ b ∈ k' and `Γ ⊢ c ∈ k'.  Similarly, `Γ ⊢ a ∈ b ⋯⟨
-- k ⟩ c' does *not* imply `Γ ⊢ a ∈ k'.  To see this, consider again
-- the kind `⊥ ⋯⟨ ∅ ⟩ ⊤', which is well-formed and inhabited by both
-- `⊥' and `⊤', yet clearly `⊥ , ⊤ ∉ ø'.

<:-⋯⟨⟩-⟨|⟩ : ∀ {n} {Γ : Ctx n} {a b c k} →
             Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ k → Γ ⊢Tp c ∈ k →
             Γ ⊢Tp a ∈ b ⋯⟨ k ⟩ c → Γ ⊢ b <: a ∈ k × Γ ⊢ a <: c ∈ k
<:-⋯⟨⟩-⟨|⟩ {k = _ ⋯ _} a∈d⋯e b∈d⋯e c∈d⋯e a∈b⋯c          =
  <:-⇑ (<:-⋯-i (<:-⟨| a∈b⋯c)) (<∷-⋯ (<:-⟨| b∈d⋯e) (<:-|⟩ a∈d⋯e)) ,
  <:-⇑ (<:-⋯-i (<:-|⟩ a∈b⋯c)) (<∷-⋯ (<:-⟨| a∈d⋯e) (<:-|⟩ c∈d⋯e))
<:-⋯⟨⟩-⟨|⟩ {k = Π _ _} a∈Πjk b∈Πjk c∈Πjk a∈Πjb·z⋯⟨k⟩c·z =
  let Λa·z∈Πjk  = Tp∈-η a∈Πjk
      Λb·z∈Πjk  = Tp∈-η b∈Πjk
      Λc·z∈Πjk  = Tp∈-η c∈Πjk
      _ , a·z∈k = Tp∈-Λ-inv Λa·z∈Πjk
      _ , b·z∈k = Tp∈-Λ-inv Λb·z∈Πjk
      _ , c·z∈k = Tp∈-Λ-inv Λc·z∈Πjk
      Λa·z∈Πjb·z⋯⟨k⟩c·z  = Tp∈-η a∈Πjb·z⋯⟨k⟩c·z
      _ , a·z∈b·z⋯⟨k⟩c·z = Tp∈-Λ-inv Λa·z∈Πjb·z⋯⟨k⟩c·z
      b·z<:a·z∈k , a·z<:c·z∈k = <:-⋯⟨⟩-⟨|⟩ a·z∈k b·z∈k c·z∈k a·z∈b·z⋯⟨k⟩c·z
      Λjb·z<:Λja·z∈Πjk = <:-λ b·z<:a·z∈k Λb·z∈Πjk Λa·z∈Πjk
      Λja·z<:Λjc·z∈Πjk = <:-λ a·z<:c·z∈k Λa·z∈Πjk Λc·z∈Πjk
      Λja·z<:a∈kΠjk    = <:-η₁ a∈Πjk
      a<:Λja·z∈kΠjk    = <:-η₂ a∈Πjk
      Λjc·z<:c∈kΠjk    = <:-η₁ c∈Πjk
      b<:Λjb·z∈kΠjk    = <:-η₂ b∈Πjk
  in <:-trans (<:-trans b<:Λjb·z∈kΠjk Λjb·z<:Λja·z∈Πjk) Λja·z<:a∈kΠjk ,
     <:-trans (<:-trans a<:Λja·z∈kΠjk Λja·z<:Λjc·z∈Πjk) Λjc·z<:c∈kΠjk

<:-⋯⟨⟩-⟨| : ∀ {n} {Γ : Ctx n} {a b c k} →
            Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ k → Γ ⊢Tp c ∈ k →
            Γ ⊢Tp a ∈ b ⋯⟨ k ⟩ c → Γ ⊢ b <: a ∈ k
<:-⋯⟨⟩-⟨| a∈k b∈k c∈k a∈b⋯⟨k⟩c = proj₁ (<:-⋯⟨⟩-⟨|⟩ a∈k b∈k c∈k a∈b⋯⟨k⟩c)

<:-⋯⟨⟩-|⟩ : ∀ {n} {Γ : Ctx n} {a b c k} →
            Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ k → Γ ⊢Tp c ∈ k →
            Γ ⊢Tp a ∈ b ⋯⟨ k ⟩ c → Γ ⊢ a <: c ∈ k
<:-⋯⟨⟩-|⟩ a∈k b∈k c∈k a∈b⋯⟨k⟩c = proj₂ (<:-⋯⟨⟩-⟨|⟩ a∈k b∈k c∈k a∈b⋯⟨k⟩c)

-- An interval introduction rule for subtypes inhabiting higher-order
-- interval kinds.

<:-⋯⟨⟩-i : ∀ {n} {Γ : Ctx n} {a b k} →
           Γ ⊢ a <: b ∈ k → Γ ⊢ η-exp k a <: η-exp k b ∈ a ⋯⟨ k ⟩ b
<:-⋯⟨⟩-i a<:b∈k   with <:-valid-kd a<:b∈k
<:-⋯⟨⟩-i a<:b∈c⋯d | kd-⋯ _ _    = <:-⋯-i a<:b∈c⋯d
<:-⋯⟨⟩-i a<:b∈Πjk | kd-Π j-kd _ =
  let j-wf          = wf-kd j-kd
      Γ-ctx         = <:-ctx a<:b∈Πjk
      j∷Γ-ctx       = j-wf ∷ Γ-ctx
      a∈Πjk , b∈Πjk = <:-valid a<:b∈Πjk
      a<:b∈Πjk′     = <:-weaken j-wf a<:b∈Πjk
      a·z<:b·z∈k[z] = <:-· a<:b∈Πjk′ (≃-refl (∈-var zero j∷Γ-ctx refl))
      a·z<:b·z∈k    = subst (_ ⊢ _ <: _ ∈_) (Kind-wk↑-sub-zero-vanishes _)
                            a·z<:b·z∈k[z]
      a·z<:b·z∈a·z⋯⟨k⟩b·z = <:-⋯⟨⟩-i a·z<:b·z∈k
  in <:-λ a·z<:b·z∈a·z⋯⟨k⟩b·z
          (∈-⇑ (∈-s⟨⟩-i a∈Πjk) (<∷-⋯⟨⟩ (<:-refl a∈Πjk) a<:b∈Πjk))
          (∈-⇑ (∈-s⟨⟩-i b∈Πjk) (<∷-⋯⟨⟩ a<:b∈Πjk (<:-refl b∈Πjk)))

-- Any interval indexed by *⟨ k ⟩ can be re-indexed by k

*⟨⟩-⋯⟨⟩ : ∀ {n} {a b : Term n} k → a ⋯⟨ *⟨ k ⟩ ⟩ b ≡ a ⋯⟨ k ⟩ b
*⟨⟩-⋯⟨⟩ (a ⋯ b) = refl
*⟨⟩-⋯⟨⟩ (Π j k) = cong (Π j) (*⟨⟩-⋯⟨⟩ k)

-- *⟨ k ⟩ is equal to the HO interval bounded by ⊥′⟨ k ⟩ and ⊤′⟨ k ⟩.

*⟨⟩-⊥⟨⟩⋯⟨⟩⊤⟨⟩ : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd →
                Γ ⊢ *⟨ k ⟩ ≅ ⊥′⟨ k ⟩ ⋯⟨ k ⟩ ⊤′⟨ k ⟩
*⟨⟩-⊥⟨⟩⋯⟨⟩⊤⟨⟩         (kd-⋯ a∈* b∈*)           = ≅-refl (*-kd (Tp∈-ctx a∈*))
*⟨⟩-⊥⟨⟩⋯⟨⟩⊤⟨⟩ {_} {Γ} (kd-Π {j} {k} j-kd k-kd) =
  ≅-Π (≅-refl j-kd)
      (≅-trans (*⟨⟩-⊥⟨⟩⋯⟨⟩⊤⟨⟩ k-kd)
               (subst₂ (_ ⊢_≅_) (*⟨⟩-⋯⟨⟩ k) (*⟨⟩-⋯⟨⟩ k)
                       (≅-⋯⟨⟩ ⊥⟨k⟩≃Λ⊥⟨k⟩·z ⊤⟨k⟩≃Λ⊤⟨k⟩·z)))
  where
    module KL = TermLikeLemmas termLikeLemmasKind

    Γ-ctx   = kd-ctx j-kd
    z∈j     = ∈-var zero (wf-kd j-kd ∷ Γ-ctx) refl
    Πjk-kd′ = kd-weaken (wf-kd j-kd) (kd-Π j-kd k-kd)
    eq₁     = cong (λ k → (Λ (weakenKind j) k) · var zero) (sym (⊥′⟨⟩-/Var k))
    eq₂     = cong (λ k → (Λ (weakenKind j) k) · var zero) (sym (⊤′⟨⟩-/Var k))
    k′[z]   = (k Kind/Var _) Kind[ var zero ]
    ⊥⟨k⟩≃Λ⊥⟨k⟩·z = subst₂ (_ ⊢_≃ weaken (Λ j ⊥′⟨ k ⟩) · var zero ∈_)
                          (cong ⊥′⟨_⟩ (Kind-wk↑-sub-zero-vanishes k))
                          (cong *⟨_⟩ (Kind-wk↑-sub-zero-vanishes k))
                          (subst (kd j ∷ Γ ⊢ ⊥′⟨ k′[z] ⟩ ≃_∈ *⟨ k′[z] ⟩) eq₁
                                 (≃-sym (≃-⊥′⟨⟩-· Πjk-kd′ z∈j)))
    ⊤⟨k⟩≃Λ⊤⟨k⟩·z = subst₂ (_ ⊢_≃ weaken (Λ j ⊤′⟨ k ⟩) · var zero ∈_)
                          (cong ⊤′⟨_⟩ (Kind-wk↑-sub-zero-vanishes k))
                          (cong *⟨_⟩ (Kind-wk↑-sub-zero-vanishes k))
                          (subst (kd j ∷ Γ ⊢ ⊤′⟨ k′[z] ⟩ ≃_∈ *⟨ k′[z] ⟩) eq₂
                                 (≃-sym (≃-⊤′⟨⟩-· Πjk-kd′ z∈j)))

----------------------------------------------------------------------
-- Encodings and admissible kinding rules of bounded quantifiers and
-- operators

-- Bounded operator kind.

Π′ : ∀ {n} → Term n → Term n → Kind Term n → Kind Term (suc n) → Kind Term n
Π′ a b j k = Π (a ⋯⟨ j ⟩ b) k

-- Bounded universal quantifiers.

∀′ : ∀ {n} → Term n → Term n → Kind Term n → Term (suc n) → Term n
∀′ a b k c = Π (a ⋯⟨ k ⟩ b) c

-- Bounded type abstraction.

Λ′ : ∀ {n} → Term n → Term n → Kind Term n → Term (suc n) → Term n
Λ′ a b k c = Λ (a ⋯⟨ k ⟩ b) c

-- A formation rule for bounded operator kinds.

∈-Π′-f : ∀ {n} {Γ : Ctx n} {a b j k} →
         Γ ⊢Tp a ∈ j → Γ ⊢Tp b ∈ j → kd (a ⋯⟨ j ⟩ b) ∷ Γ ⊢ k kd →
         Γ ⊢ Π′ a b j k kd
∈-Π′-f a∈j b∈j k-kd = kd-Π (kd-⋯⟨⟩ a∈j b∈j) k-kd

-- An introduction rule for bounded universal quantifiers.

∈-Π′-i : ∀ {n} {Γ : Ctx n} {a b j c k} →
         Γ ⊢Tp a ∈ j → Γ ⊢Tp b ∈ j → kd (a ⋯⟨ j ⟩ b) ∷ Γ ⊢Tp c ∈ k →
         Γ ⊢Tp Λ′ a b j c ∈ Π′ a b j k
∈-Π′-i a∈j b∈j c∈k = ∈-Π-i (kd-⋯⟨⟩ a∈j b∈j) c∈k

-- An elimination rule for bounded universal quantifiers.

∈-Π′-e : ∀ {n} {Γ : Ctx n} {a b c j k d} →
         Γ ⊢Tp a ∈ Π′ b c j k → Γ ⊢ b <: d ∈ j → Γ ⊢ d <: c ∈ j →
         Γ ⊢Tp a · η-exp j d ∈ k Kind[ η-exp j d ]
∈-Π′-e a∈Πbcjk b<:d∈j d<:c∈j =
  let d∈j , _ = <:-valid d<:c∈j
  in ∈-Π-e a∈Πbcjk (Tp∈-<:-⋯ b<:d∈j d<:c∈j)

-- A formation rule for bounded universal quantifiers.

∈-∀′-f : ∀ {n} {Γ : Ctx n} {a b k c} →
         Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ k → kd (a ⋯⟨ k ⟩ b) ∷ Γ ⊢Tp c ∈ * →
         Γ ⊢Tp ∀′ a b k c ∈ *
∈-∀′-f a∈k b∈k c∈* = ∈-∀-f (kd-⋯⟨⟩ a∈k b∈k) c∈*

-- An introduction rule for bounded universal quantifiers.

∈-∀′-i : ∀ {n} {Γ : Ctx n} {a b k c d} →
         Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ k → kd (a ⋯⟨ k ⟩ b) ∷ Γ ⊢Tm c ∈ d →
         Γ ⊢Tm Λ′ a b k c ∈ ∀′ a b k d
∈-∀′-i a∈k b∈k c∈d = ∈-∀-i (kd-⋯⟨⟩ a∈k b∈k) c∈d

-- An elimination rule for bounded universal quantifiers.

∈-∀′-e : ∀ {n} {Γ : Ctx n} {a b c k d e} →
         Γ ⊢Tm a ∈ ∀′ b c k d → Γ ⊢ b <: e ∈ k → Γ ⊢ e <: c ∈ k →
         Γ ⊢Tm a ⊡ η-exp k e ∈ d [ η-exp k e ]
∈-∀′-e a∈∀bckd b<:e∈k e<:c∈k =
  let e∈k , _ = <:-valid e<:c∈k
  in ∈-∀-e a∈∀bckd (Tp∈-<:-⋯ b<:e∈k e<:c∈k)

------------------------------------------------------------------------
-- Stone and Harper's singleton (sub)kinding rules.
--
-- See p. 3 (216) of C. A. Stone and R. Harper, Deciding Type
-- Equivalence in a Language with Singleton Kinds, proc. POPL'00, ACM,
-- 2000.

-- An encoding of Stone and Harper's singleton kinds.

S : ∀ {n} → Term n → Kind Term n
S a = a ⋯ a

-- Singleton kind formation.

kd-s : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢Tp a ∈ * → Γ ⊢ S a kd
kd-s a∈* = kd-⋯ a∈* a∈*

-- Singleton introduction for kinding is exactly the `∈-s-i' kinding rule.

-- Singleton introduction for equality.
--
-- NOTE. This is just a weaker version of `≃-s-i'.

≃-s-i′ : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ≃ b ∈ * → Γ ⊢ a ≃ b ∈ S a
≃-s-i′ a≃b∈* = ≃-s-i a≃b∈*

-- Singleton elimination.
≃-s-e : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢Tp a ∈ S b → Γ ⊢ a ≃ b ∈ *
≃-s-e a∈b⋯b = <:-antisym (<:-|⟩ a∈b⋯b) (<:-⟨| a∈b⋯b)

-- Subkinding of singletons.

<∷-s-* : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢Tp a ∈ * → Γ ⊢ S a <∷ *
<∷-s-* a∈* = <∷-⋯ (<:-⊥ a∈*) (<:-⊤ a∈*)

<∷-s-s : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ≃ b ∈ * → Γ ⊢ S a <∷ S b
<∷-s-s (<:-antisym a<:b∈* b<:a∈*) = <∷-⋯ b<:a∈* a<:b∈*

-- Equality of singleton kinds.
--
-- NOTE. This is just a weaker version of `≅-⋯'.

≅-s : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ≃ b ∈ * → Γ ⊢ S a ≅ S b
≅-s a≃b∈* = ≅-⋯ a≃b∈* a≃b∈*

------------------------------------------------------------------------
-- Cardelli and Longo's power (sub)kinding rules.
--
-- See p. 8 (424) of L. Cardelli, G. Longo, A Semantic Basis for
-- Quest, JFP 1(4), Cambridge University Press, 1991.

-- An encoding of Cardelli and Longo's power kinds.

P : ∀ {n} → Term n → Kind Term n
P a = ⊥ ⋯ a

-- Power kind formation.

kd-p : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢Tp a ∈ * → Γ ⊢ P a kd
kd-p a∈* = kd-⋯ (∈-⊥-f (Tp∈-ctx a∈*)) a∈*

-- Power kind introduction.

∈-p-i : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢Tp a ∈ * → Γ ⊢Tp a ∈ P a
∈-p-i a∈* = ∈-⇑ (∈-s-i a∈*) (<∷-⋯ (<:-⊥ a∈*) (<:-refl a∈*))

-- Subkinding of power kinds.

<∷-p : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a <: b ∈ * → Γ ⊢ P a <∷ P b
<∷-p a<:b∈* = <∷-⋯ (<:-⊥ (∈-⊥-f (<:-ctx a<:b∈*))) a<:b∈*

-- Power kinding is equivalent to subtyping of proper types.

∈P⇒<: : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢Tp a ∈ P b → Γ ⊢ a <: b ∈ *
∈P⇒<: a∈Pb = <:-|⟩ a∈Pb

<:⇒∈P : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a <: b ∈ * → Γ ⊢Tp a ∈ P b
<:⇒∈P a<:b∈* = ∈-⇑ (∈-p-i (proj₁ (<:-valid a<:b∈*))) (<∷-p a<:b∈*)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
module Ex6Edit where -- git would rather indicate that nothing has happened 0/15

{- This is the file where you should work. -}

open import CS410-Prelude
open import CS410-Nat
open import Ex6AgdaSetup

  -- the setup gives you a nondependent pair type _**_
  -- because that's what the compiler can exchange with Haskell code

{- The key editor data structure is the cursor. A Cursor M X represents
   being somewhere in the middle of a sequence of X values, holding an M. -}

record Cursor (M X : Set) : Set where
  constructor _<[_]>_
  field
    beforeMe  : Bwd X
    atMe      : M
    afterMe   : List X
infix 2 _<[_]>_

{- An editor buffer is a nested cursor: we're in the middle of a bunch of
   *lines*, holding a cursor for the current line, which puts us in the
   middle of a bunch of characters, holding the element of One. -}
Buffer : Set
Buffer = Cursor (Cursor One Char) (List Char)

{- This operator, called "chips", shuffles the elements from a backward list
   on to the start of a forward list, keeping them in the same order. -}
_<>>_ : {X : Set} -> Bwd X -> List X -> List X
[]         <>> xs  = xs
(xz <: x)  <>> xs  = xz <>> (x :: xs)

{- The "fish" operator goes the other way. -}
_<><_ : {X : Set} -> Bwd X -> List X -> Bwd X
xz <>< []         = xz
xz <>< (x :: xs)  = (xz <: x) <>< xs

{- You can turn a buffer into a list of lines, preserving its text. -}
bufText : Buffer -> List (List Char)
bufText
  (sz <[
   cz <[ <> ]> cs
   ]> ss)
  = sz <>> ((cz <>> cs) :: ss)

{- Here's an example of a proof of a fact about fish and chips. -}
firstFishFact : {X : Set} -> (xz : Bwd X)(xs : List X) ->
  (xz <>< xs) <>> []  ==  xz <>> xs
firstFishFact xz []          = refl
firstFishFact xz (x :: xs)   = firstFishFact (xz <: x) xs

{- You will need more such facts. -}

{- EXERCISE 6.1 -}
{- When we start the editor with the command
      ./Edit foo.txt
   the contents of foo.txt will be turned into a list of lines.
   Your (not so tricky) mission is to turn the file contents into a buffer which
   contains the same text.
   (1 mark)
-}
initBuf : List (List Char) -> Buffer
initBuf ss =
  [] <[
  [] <[ <> ]> []
  ]> []
{- As you can see, the current version will run, but it always gives the empty
   buffer, which is not what we want unless the input is empty. -}

{- Next comes the heart of the editor. You get a keystroke and the current buffer,
   and you have to say what is the new buffer. You also have to say what is the
   extent of the change.

   The tricky part is this: you have to be honest enough about your change
   report, so that we don't underestimate the amount of updating the screen needs.
-}

Honest : Buffer -> Change ** Buffer -> Set
Honest b (allQuiet    , b')                            = b == b'
Honest b (cursorMove  , b')                            = bufText b == bufText b'
Honest (sz <[ _ ]> ss) (lineEdit , (sz' <[ _ ]> ss'))  = (sz == sz') ** (ss == ss')
Honest _ (bigChange   , _)                             = One

record UpdateFrom (b : Buffer) : Set where   -- b is the starting buffer
  constructor _///_
  field
    update  : Change ** Buffer   -- change and new buffer
    honest  : Honest b update
open UpdateFrom
infix 2 _///_

{- EXERCISE 6.2 -}
{- Implement the appropriate behaviour for as many keystrokes as you can.
   I have done a couple for you, but I don't promise to have done them
   correctly. -}
keystroke : Key -> (b : Buffer) -> UpdateFrom b
keystroke (char c)
  (sz <[
   cz <[ <> ]> cs
   ]> ss)
  = lineEdit ,
  (sz <[
   cz <[ <> ]> c :: cs
   ]> ss)
  /// refl , refl          -- see? same above and below
keystroke (arrow normal right)
  (sz <: s <[
   [] <[ <> ]> cs
   ]> ss)
  = cursorMove ,
  (sz <[ ([] <>< s) <[ <> ]> [] ]> cs :: ss)
  /// within (\ x -> sz <>> (x :: cs :: ss)) turn s into ([] <>< s) <>> []
        because sym (firstFishFact [] s)
keystroke k b = allQuiet , b /// refl
{- Please expect to need to invent extra functions, e.g., to measure where you
   are, so that up and down arrow work properly. -}
{- Remember also that you can always overestimate the change by saying bigChange,
   which needs only a trivial proof. But you may find that the display will flicker
   badly if you do. -}
{- (char c)                 1 mark
   enter                    2 marks
   backspace delete         2 marks for the pair
   left right               2 marks for the pair (with cursorMove change)
   up down                  2 marks for the pair (with cursorMove change)
   -}

{- EXERCISE 6.3 -}
{- You will need to improve substantially on my implementation of the next component,
   whose purpose is to update the window. Mine displays only one line! -}
render :
  Nat ** Nat ->        -- height and width of window -- CORRECTION! width and height
  Nat ** Nat ->        -- first visible row, first visible column
  Change ** Buffer ->  -- what just happened
  List Action **       -- how to update screen
    (Nat ** Nat)       -- new first visible row, first visible column
render _ tl (allQuiet , _) = ([] , tl)
render _ tl (_ , (_ <[ cz <[ <> ]> cs ]> _))
  = (goRowCol 0 0 :: sendText (cz <>> cs) :: []) , tl
{- The editor window gives you a resizable rectangular viewport onto the editor buffer.
   You get told
     the current size of the viewport
     which row and col of the buffer are at the top left of the viewport
       (so you can handle documents which are taller or wider than the window)
     the most recent change report and buffer

   You need to figure out whether you need to move the viewport
       (by finding out if the cursor is still within the viewport)
     and if so, where to.

   You need to figure out what to redisplay. If the change report says
     lineEdit and the viewport has not moved, you need only repaint the
     current line. If the viewport has moved or the change report says
     bigChange, you need to repaint the whole buffer.

   You will need to be able to grab a rectangular region of text from the
     buffer, but you do know how big and where from.

   Remember to put the cursor in the right place, relative to where in
     the buffer the viewport is supposed to be. The goRowCol action takes
     *viewport* coordinates, not *buffer* coordinates! You will need to
     invent subtraction!
-}
{- Your code does not need to worry about resizing the window. My code does
   that. On detecting a size change, my code just calls your code with a
   bigChange report and the same buffer, so if you are doing a proper repaint,
   the right thing will happen. -}
{- 2 marks for ensuring that a buffer smaller than the viewport displays
       correctly, with the cursor in the right place, if nobody changes
       the viewport size
   2 marks for ensuring that the cursor remains within the viewport even if
       the viewport needs to move
   1 mark for ensuring that lineEdit changes need only affect one line of
       the display (provided the cursor stays in the viewport)
-}

{- Your code then hooks into mine to produce a top level executable! -}
main : IO One
main = mainLoop initBuf (\ k b -> update (keystroke k b)) render

{- To build the editor, just do
     make Ex6Edit
   in a shell window.
   To run the editor, once compiled, do
     make edit
   in the shell window, which should become the editor window.
   To quit the editor, do
     ctrl-C
   like an old-fashioned soul.
-}

{- There is no one right way to do this exercise, and there is some scope for
   extension. It's important that you get in touch if you need help, either in
   achieving the basic deliverable, or in finding ways to explore beyond it.
-}


text:
{-

Defines different notions of morphisms and properties of morphisms of
groups:

- GroupHom (homomorphisms)
- GroupEquiv (equivs which are homomorphisms)
- GroupIso (isos which are homomorphisms)
- Image
- Kernel
- Surjective
- Injective
- Mono
- BijectionIso (surjective + injective)

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Morphisms where

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

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.DirProd
open import Cubical.Data.Sigma

open import Cubical.Reflection.RecordEquiv

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

record IsGroupHom {A : Type ℓ} {B : Type ℓ'}
  (M : GroupStr A) (f : A → B) (N : GroupStr B)
  : Type (ℓ-max ℓ ℓ')
  where

  -- Shorter qualified names
  private
    module M = GroupStr M
    module N = GroupStr N

  field
    pres· : (x y : A) → f (x M.· y) ≡ f x N.· f y
    pres1 : f M.1g ≡ N.1g
    presinv : (x : A) → f (M.inv x) ≡ N.inv (f x)

unquoteDecl IsGroupHomIsoΣ = declareRecordIsoΣ IsGroupHomIsoΣ (quote IsGroupHom)

GroupHom : (G : Group ℓ) (H : Group ℓ') → Type (ℓ-max ℓ ℓ')
GroupHom G H = Σ[ f ∈ (G .fst → H .fst) ] IsGroupHom (G .snd) f (H .snd)

GroupIso : (G : Group ℓ) (H : Group ℓ') → Type (ℓ-max ℓ ℓ')
GroupIso G H = Σ[ e ∈ Iso (G .fst) (H .fst) ] IsGroupHom (G .snd) (e .Iso.fun) (H .snd)

IsGroupEquiv : {A : Type ℓ} {B : Type ℓ'}
  (M : GroupStr A) (e : A ≃ B) (N : GroupStr B) → Type (ℓ-max ℓ ℓ')
IsGroupEquiv M e N = IsGroupHom M (e .fst) N

GroupEquiv : (G : Group ℓ) (H : Group ℓ') → Type (ℓ-max ℓ ℓ')
GroupEquiv G H = Σ[ e ∈ (G .fst ≃ H .fst) ] IsGroupEquiv (G .snd) e (H .snd)

groupEquivFun : {G : Group ℓ} {H : Group ℓ'} → GroupEquiv G H → G .fst → H .fst
groupEquivFun e = e .fst .fst

-- Image, kernel, surjective, injective, and bijections

open IsGroupHom
open GroupStr

private
  variable
    G H : Group ℓ

isInIm : GroupHom G H → ⟨ H ⟩ → Type _
isInIm {G = G} ϕ h = ∃[ g ∈ ⟨ G ⟩ ] ϕ .fst g ≡ h

isInKer : GroupHom G H → ⟨ G ⟩ → Type _
isInKer {H = H} ϕ g = ϕ .fst g ≡ 1g (snd H)

Ker : GroupHom G H → Type _
Ker {G = G} ϕ = Σ[ x ∈ ⟨ G ⟩ ] isInKer ϕ x

Im : GroupHom G H → Type _
Im {H = H} ϕ = Σ[ x ∈ ⟨ H ⟩ ] isInIm ϕ x

isSurjective : GroupHom G H → Type _
isSurjective {H = H} ϕ = (x : ⟨ H ⟩) → isInIm ϕ x

isInjective : GroupHom G H → Type _
isInjective {G = G} ϕ = (x : ⟨ G ⟩) → isInKer ϕ x → x ≡ 1g (snd G)

isMono : GroupHom G H → Type _
isMono {G = G} f = {x y : ⟨ G ⟩} → f .fst x ≡ f .fst y → x ≡ y

-- Group bijections
record BijectionIso (G : Group ℓ) (H : Group ℓ') : Type (ℓ-max ℓ ℓ') where

  constructor bijIso

  field
    fun : GroupHom G H
    inj : isInjective fun
    surj : isSurjective fun

max_stars_repo_name: FernandoLarrain/cubical


text:
-- Showing that destroy-guardedness in Issue1209-4 indeed does
-- destroy guardedness

{-# OPTIONS --safe --guardedness --no-sized-types #-}

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A

open Stream

destroy-guardedness : ∀ {A} → Stream A → Stream A
destroy-guardedness xs .head = xs .head
destroy-guardedness xs .tail = xs .tail

repeat : ∀ {A} → A → Stream A
repeat x .head = x
repeat x .tail = destroy-guardedness (repeat x)


text:
open import Nat
open import Prelude
open import contexts
open import core

open import canonical-value-forms

module canonical-boxed-forms where
  canonical-boxed-forms-b : ∀{Δ d} →
                            Δ , ∅ ⊢ d :: b →
                            d boxedval →
                            d == c
  canonical-boxed-forms-b (TAVar _) (BVVal ())
  canonical-boxed-forms-b wt (BVVal v) = canonical-value-forms-b wt v

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for boxed values at arrow type
  data cbf-arr : (Δ : hctx) (d : ihexp) (τ1 τ2 : htyp) → Set where
    CBFLam : ∀{Δ d τ1 τ2} →
      (Σ[ x ∈ Nat ] Σ[ d' ∈ ihexp ]
         (d == (·λ x [ τ1 ] d') × Δ , ■ (x , τ1) ⊢ d' :: τ2))
      → cbf-arr Δ d τ1 τ2
    CBFCastArr : ∀{Δ d τ1 τ2} →
      (Σ[ d' ∈ ihexp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
         (d == (d' ⟨ τ1' ==> τ2' ⇒ τ1 ==> τ2 ⟩) ×
         (τ1' ==> τ2' ≠ τ1 ==> τ2) ×
         (Δ , ∅ ⊢ d' :: τ1' ==> τ2')))
      → cbf-arr Δ d τ1 τ2

  canonical-boxed-forms-arr : ∀{Δ d τ1 τ2 } →
                            Δ , ∅ ⊢ d :: (τ1 ==> τ2)  →
                            d boxedval →
                            cbf-arr Δ d τ1 τ2
  canonical-boxed-forms-arr (TAVar x₁) (BVVal ())
  canonical-boxed-forms-arr (TALam f wt) (BVVal v) = CBFLam (canonical-value-forms-arr (TALam f wt) v)
  canonical-boxed-forms-arr (TAAp wt wt₁) (BVVal ())
  canonical-boxed-forms-arr (TAEHole x x₁) (BVVal ())
  canonical-boxed-forms-arr (TANEHole x wt x₁) (BVVal ())
  canonical-boxed-forms-arr (TACast wt x) (BVVal ())
  canonical-boxed-forms-arr (TACast wt x) (BVArrCast x₁ bv) = CBFCastArr (_ , _ , _ , refl , x₁ , wt)
  canonical-boxed-forms-arr (TAFailedCast x x₁ x₂ x₃) (BVVal ())

  canonical-boxed-forms-hole : ∀{Δ d} →
                               Δ , ∅ ⊢ d :: ⦇-⦈ →
                               d boxedval →
                               Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
                                 ((d == d' ⟨ τ' ⇒ ⦇-⦈ ⟩) ×
                                  (τ' ground) ×
                                  (Δ , ∅ ⊢ d' :: τ'))
  canonical-boxed-forms-hole (TAVar x₁) (BVVal ())
  canonical-boxed-forms-hole (TAAp wt wt₁) (BVVal ())
  canonical-boxed-forms-hole (TAEHole x x₁) (BVVal ())
  canonical-boxed-forms-hole (TANEHole x wt x₁) (BVVal ())
  canonical-boxed-forms-hole (TACast wt x) (BVVal ())
  canonical-boxed-forms-hole (TACast wt x) (BVHoleCast x₁ bv) = _ , _ , refl , x₁ , wt
  canonical-boxed-forms-hole (TAFailedCast x x₁ x₂ x₃) (BVVal ())

  canonical-boxed-forms-coverage : ∀{Δ d τ} →
                                   Δ , ∅ ⊢ d :: τ →
                                   d boxedval →
                                   τ ≠ b →
                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
                                   τ ≠ ⦇-⦈ →
                                   ⊥
  canonical-boxed-forms-coverage TAConst (BVVal x) nb na nh = nb refl
  canonical-boxed-forms-coverage (TAVar x₁) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TALam _ wt) (BVVal x₁) nb na nh = na _ _ refl
  canonical-boxed-forms-coverage (TAAp wt wt₁) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TAEHole x x₁) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TANEHole x wt x₁) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TACast wt x) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TACast wt x) (BVArrCast x₁ bv) nb na nh = na _ _ refl
  canonical-boxed-forms-coverage (TACast wt x) (BVHoleCast x₁ bv) nb na nh = nh refl
  canonical-boxed-forms-coverage (TAFailedCast x x₁ x₂ x₃) (BVVal ())

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
{-# OPTIONS  --no-termination-check #-}

module Data.Bin.BinDivNt where

  open import Data.Bin
  open import Data.Bin.Properties
  open import Data.Product
  open import Relation.Binary
  open StrictTotalOrder <-strictTotalOrder

  open import Relation.Nullary
  open import Data.Bin.Utils
  open import Data.Bin.Minus

  _divMod-nt_ : Bin → Bin → (Bin × Bin)
  a divMod-nt b with a <? b
  ... | yes _ = (fromℕ 0 , a)
  ... | no _ with a divMod-nt (b *2)
  ... | (d , m) with m <? b
  ... | yes _ = (d *2 , m)
  ... | no _ = (fromℕ 1 + (d *2) , m - b)

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
data Unit : Set where
  unit : Unit

test : Unit
test = {!!}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


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

open import lib.Basics
open import lib.types.Group
open import lib.groups.Homomorphism
open import lib.types.TwoSemiCategory
open import lib.two-semi-categories.Functor

module lib.two-semi-categories.GroupToCategory where

group-to-cat : ∀ {i} → Group i → TwoSemiCategory lzero i
group-to-cat G =
  record
  { El = ⊤
  ; Arr = λ _ _ → G.El
  ; Arr-level = λ _ _ → raise-level 0 G.El-level
  ; two-semi-cat-struct =
    record
    { comp = G.comp
    ; assoc = G.assoc
    ; pentagon-identity = λ _ _ _ _ → =ₛ-in (prop-path (has-level-apply G.El-level _ _) _ _)
    }
  }
  where
    module G = Group G

homomorphism-to-functor : ∀ {i j} {G : Group i} {H : Group j}
  → G →ᴳ H
  → TwoSemiFunctor (group-to-cat G) (group-to-cat H)
homomorphism-to-functor {G = G} {H = H} φ =
  record
  { F₀ = idf ⊤
  ; F₁ = φ.f
  ; pres-comp = φ.pres-comp
  ; pres-comp-coh = λ _ _ _ → =ₛ-in $ prop-path (has-level-apply H.El-level _ _) _ _
  }
  where
    module G = Group G
    module H = Group H
    module φ = GroupHom φ

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import AbstractInterfaces public

module OrdersAndEqualities {{_ : IsProc}} {{_ : IsTime}} {{_ : IsMsg}} {{_ : IsEvent}} where

-- _≡ₑ_ is a decidable equality on events within one process.

data _≡ₑ_ : ∀ {P T T′} → Event P T → Event P T′ → Set where
  refl≡ₑ : ∀ {P T} {a b : Event P T} →
           a ≡ₑ b

_≢ₑ_ : ∀ {P T T′} → Event P T → Event P T′ → Set
a ≢ₑ b = ¬ (a ≡ₑ b)

≡→≡ₑ : ∀ {P T T′} {a : Event P T} {b : Event P T′} →
        T ≡ T′ → a ≡ₑ b
≡→≡ₑ refl = refl≡ₑ

≢→≢ₑ : ∀ {P T T′} {a : Event P T} {b : Event P T′} →
        T ≢ T′ → a ≢ₑ b
≢→≢ₑ T≢T′ refl≡ₑ = refl ↯ T≢T′

_≡ₑ?_ : ∀ {T T′ P} → (a : Event P T) (b : Event P T′) → Dec (a ≡ₑ b)
_≡ₑ?_ {T} {T′} a b with T ≡ₜ? T′
a ≡ₑ? b | yes T≡T′ = yes (≡→≡ₑ T≡T′)
a ≡ₑ? b | no  T≢T′ = no (≢→≢ₑ T≢T′)

-- _≅ₑ_ is a decidable equality on events across all processes.

data _≅ₑ_ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} → Event Pᵢ Tᵢ → Event Pⱼ Tⱼ → Set where
  refl≅ₑ : ∀ {P T} {a : Event P T} {b : Event P T} →
           a ≅ₑ b

_≇ₑ_ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} → Event Pᵢ Tᵢ → Event Pⱼ Tⱼ → Set
a ≇ₑ b = ¬ (a ≅ₑ b)

≡ₑ→≅ₑ : ∀ {P T T′} {a : Event P T} {b : Event P T′} →
         a ≡ₑ b → a ≅ₑ b
≡ₑ→≅ₑ refl≡ₑ = refl≅ₑ

≢ₑ→≇ₑ : ∀ {P T T′} {a : Event P T} {b : Event P T′} →
         a ≢ₑ b → a ≇ₑ b
≢ₑ→≇ₑ a≢b refl≅ₑ = refl≡ₑ ↯ a≢b

≢ₚ→≇ₑ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} →
         Pᵢ ≢ Pⱼ → a ≇ₑ b
≢ₚ→≇ₑ P≢P′ refl≅ₑ = refl ↯ P≢P′

≢ₜ→≇ₑ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} →
         Tᵢ ≢ Tⱼ → a ≇ₑ b
≢ₜ→≇ₑ T≢T′ refl≅ₑ = refl ↯ T≢T′

_≅ₑ?_ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} → (a : Event Pᵢ Tᵢ) (b : Event Pⱼ Tⱼ) → Dec (a ≅ₑ b)
_≅ₑ?_ {Pᵢ} {Pⱼ} a b with Pᵢ ≡ₚ? Pⱼ
a ≅ₑ? b | yes refl  with a ≡ₑ? b
a ≅ₑ? b | yes refl  | yes a≡b = yes (≡ₑ→≅ₑ a≡b)
a ≅ₑ? b | yes refl  | no  a≢b = no (≢ₑ→≇ₑ a≢b)
a ≅ₑ? b | no  Pᵢ≢Pⱼ = no (≢ₚ→≇ₑ Pᵢ≢Pⱼ)

-- _<ₑ_ is a decidable strict total order on events within one process.

_<ₑ_ : ∀ {T T′ P} → Event P T → Event P T′ → Set
_<ₑ_ {T} {T′} a b = T <ₜ T′

_≮ₑ_ : ∀ {P T T′} → Event P T → Event P T′ → Set
a ≮ₑ b = ¬ (a <ₑ b)

trans<ₑ : ∀ {P T T′ T″} {a : Event P T} {b : Event P T′} {c : Event P T″} →
          a <ₑ b → b <ₑ c → a <ₑ c
trans<ₑ = trans<ₜ

tri<ₑ : ∀ {T T′ P} → (a : Event P T) (b : Event P T′) →
        Tri (a <ₑ b) (a ≡ₑ b) (b <ₑ a)
tri<ₑ {T} {T′} a b with tri<ₜ T T′
tri<ₑ a b | τ₍ T<T′ T≢T′ T′≮T = τ₍ T<T′ (≢→≢ₑ T≢T′) T′≮T
tri<ₑ a b | τ₌ T≮T′ T≡T′ T′≮T = τ₌ T≮T′ (≡→≡ₑ T≡T′) T′≮T
tri<ₑ a b | τ₎ T≮T′ T≢T′ T′<T = τ₎ T≮T′ (≢→≢ₑ T≢T′) T′<T

irrefl<ₑ : ∀ {P T} {a : Event P T} → a ≮ₑ a
irrefl<ₑ {a = a} with tri<ₑ a a
irrefl<ₑ | τ₍ a<a a≢a a≮a = a≮a
irrefl<ₑ | τ₌ a≮a a≡a _   = a≮a
irrefl<ₑ | τ₎ a≮a a≢a a<a = a≮a

_<ₑ?_ : ∀ {P T T′} → (a : Event P T) (b : Event P T′) → Dec (a <ₑ b)
a <ₑ? b with tri<ₑ a b
a <ₑ? b | τ₍ a<b a≢b b≮a = yes a<b
a <ₑ? b | τ₌ a≮b a≡b b≮a = no a≮b
a <ₑ? b | τ₎ a≮b a≢b b<a = no a≮b

-- _⊳_ is a strict partial order on events across all processes.

data _⊳_ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} → Event Pᵢ Tᵢ → Event Pⱼ Tⱼ → Set where
  lift⊳  : ∀ {P T T′} {a : Event P T} {b : Event P T′} →
           a <ₑ b → a ⊳ b

  pass⊳  : ∀ {Cᵢ Cⱼ Pᵢ Pⱼ Tₘ Tⱼ} {{_ : Tₘ ≡ sucₜ Cᵢ}} {{_ : Tⱼ ≡ sucₜ (Tₘ ⊔ₜ Cⱼ)}} →
           {m : Msg Pᵢ Pⱼ Tₘ} {a : Event Pᵢ Tₘ} {b : Event Pⱼ Tⱼ} →
           isSendₑ {Cᵢ} m a → isRecvₑ {Cⱼ} m b → a ⊳ b

  trans⊳ : ∀ {Pᵢ Pⱼ Pₖ Tᵢ Tⱼ Tₖ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} {c : Event Pₖ Tₖ} →
           a ⊳ b → b ⊳ c → a ⊳ c

_⋫_ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} → Event Pᵢ Tᵢ → Event Pⱼ Tⱼ → Set
a ⋫ b = ¬ (a ⊳ b)

clock⊳ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} →
         a ⊳ b → Tᵢ <ₜ Tⱼ
clock⊳ (lift⊳ Tᵢ<Tⱼ)                           = Tᵢ<Tⱼ
clock⊳ (pass⊳ {Cᵢ} {Cⱼ} {{refl}} {{refl}} _ _) = n<s[n⊔m]ₜ (sucₜ Cᵢ) Cⱼ
clock⊳ (trans⊳ a⊳b b⊳c)                        = trans<ₜ (clock⊳ a⊳b) (clock⊳ b⊳c)

irrefl⊳ : ∀ {P T} {a : Event P T} → a ⋫ a
irrefl⊳ (lift⊳ {a = a} a<a) = a<a ↯ irrefl<ₑ {a = a}
irrefl⊳ (pass⊳ x y)         = (x , y) ↯ absurdₑ
irrefl⊳ (trans⊳ {Tᵢ = Tᵢ} {Tⱼ} a⊳b b⊳a) with tri<ₜ Tᵢ Tⱼ
irrefl⊳ (trans⊳ a⊳b b⊳a) | τ₍ Tᵢ<Tⱼ Tᵢ≢Tⱼ Tⱼ≮Tᵢ = clock⊳ b⊳a ↯ Tⱼ≮Tᵢ
irrefl⊳ (trans⊳ a⊳b b⊳a) | τ₌ Tᵢ≮Tⱼ Tᵢ≡Tⱼ Tⱼ≮Tᵢ = clock⊳ a⊳b ↯ Tᵢ≮Tⱼ
irrefl⊳ (trans⊳ a⊳b b⊳a) | τ₎ Tᵢ≮Tⱼ Tᵢ≢Tⱼ Tⱼ<Tᵢ = clock⊳ a⊳b ↯ Tᵢ≮Tⱼ

asym⊳ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} → a ⊳ b → b ⋫ a
asym⊳ a⊳b b⊳a = irrefl⊳ (trans⊳ a⊳b b⊳a)

-- _⇒_ is a decidable strict total order on events across all processes.

data _⇒_ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} → Event Pᵢ Tᵢ → Event Pⱼ Tⱼ → Set where
  diff⇒ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} →
           Tᵢ <ₜ Tⱼ → a ⇒ b

  same⇒ : ∀ {Pᵢ Pⱼ T} {a : Event Pᵢ T} {b : Event Pⱼ T} →
           Pᵢ <ₚ Pⱼ → a ⇒ b

_⇏_ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} → Event Pᵢ Tᵢ → Event Pⱼ Tⱼ → Set
a ⇏ b = ¬ (a ⇒ b)

lift⇒ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} →
         a ⊳ b → a ⇒ b
lift⇒ = diff⇒ ∘ clock⊳

trans⇒ : ∀ {Pᵢ Pⱼ Pₖ Tᵢ Tⱼ Tₖ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} {c : Event Pₖ Tₖ} →
          a ⇒ b → b ⇒ c → a ⇒ c
trans⇒ (diff⇒ Tᵢ<Tⱼ) (diff⇒ Tⱼ<Tₖ) = diff⇒ (trans<ₜ Tᵢ<Tⱼ Tⱼ<Tₖ)
trans⇒ (diff⇒ Tᵢ<Tⱼ) (same⇒ Pⱼ<Pₖ) = diff⇒ Tᵢ<Tⱼ
trans⇒ (same⇒ Pᵢ<Pⱼ) (diff⇒ Tⱼ<Tₖ) = diff⇒ Tⱼ<Tₖ
trans⇒ (same⇒ Pᵢ<Pⱼ) (same⇒ Pⱼ<Pₖ) = same⇒ (trans<ₚ Pᵢ<Pⱼ Pⱼ<Pₖ)

≮→⇏ : ∀ {Pᵢ Pⱼ T} {a : Event Pᵢ T} {b : Event Pⱼ T} →
        Pᵢ ≮ₚ Pⱼ → a ⇏ b
≮→⇏ Pᵢ≮Pⱼ (diff⇒ T<T)   = T<T ↯ irrefl<ₜ
≮→⇏ Pᵢ≮Pⱼ (same⇒ Pᵢ<Pⱼ) = Pᵢ<Pⱼ ↯ Pᵢ≮Pⱼ

≮×≮→⇏ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} →
          Tᵢ ≮ₜ Tⱼ → Pᵢ ≮ₚ Pⱼ → a ⇏ b
≮×≮→⇏ Tᵢ≮Tⱼ Pᵢ≮Pⱼ (diff⇒ Tᵢ<Tⱼ) = Tᵢ<Tⱼ ↯ Tᵢ≮Tⱼ
≮×≮→⇏ Tᵢ≮Tⱼ Pᵢ≮Pⱼ (same⇒ Pᵢ<Pⱼ) = Pᵢ<Pⱼ ↯ Pᵢ≮Pⱼ

≮×≢→⇏ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} {a : Event Pᵢ Tᵢ} {b : Event Pⱼ Tⱼ} →
          Tᵢ ≮ₜ Tⱼ → Tᵢ ≢ Tⱼ → a ⇏ b
≮×≢→⇏ Tᵢ≮Tⱼ Tᵢ≢Tⱼ (diff⇒ Tᵢ<Tⱼ) = Tᵢ<Tⱼ ↯ Tᵢ≮Tⱼ
≮×≢→⇏ Tᵢ≮Tⱼ Tᵢ≢Tⱼ (same⇒ Pᵢ<Pⱼ) = refl ↯ Tᵢ≢Tⱼ

tri⇒₌ : ∀ {Pᵢ Pⱼ T} → (a : Event Pᵢ T) (b : Event Pⱼ T) →
         Tri (a ⇒ b) (a ≅ₑ b) (b ⇒ a)
tri⇒₌ {Pᵢ} {Pⱼ} a b with tri<ₚ Pᵢ Pⱼ
tri⇒₌ a b | τ₍ Pᵢ<Pⱼ Pᵢ≢Pⱼ Pⱼ≮Pᵢ = τ₍ (same⇒ Pᵢ<Pⱼ) (≢ₚ→≇ₑ Pᵢ≢Pⱼ) (≮→⇏ Pⱼ≮Pᵢ)
tri⇒₌ a b | τ₌ Pᵢ≮Pⱼ refl  Pⱼ≮Pᵢ = τ₌ (≮→⇏ Pᵢ≮Pⱼ) refl≅ₑ  (≮→⇏ Pⱼ≮Pᵢ)
tri⇒₌ a b | τ₎ Pᵢ≮Pⱼ Pᵢ≢Pⱼ Pⱼ<Pᵢ = τ₎ (≮→⇏ Pᵢ≮Pⱼ) (≢ₚ→≇ₑ Pᵢ≢Pⱼ) (same⇒ Pⱼ<Pᵢ)

tri⇒ : ∀ {Tᵢ Tⱼ Pᵢ Pⱼ} → (a : Event Pᵢ Tᵢ) (b : Event Pⱼ Tⱼ) →
        Tri (a ⇒ b) (a ≅ₑ b) (b ⇒ a)
tri⇒ {Tᵢ} {Tⱼ} a b with tri<ₜ Tᵢ Tⱼ
tri⇒ a b | τ₍ Tᵢ<Tⱼ Tᵢ≢Tⱼ Tⱼ≮Tᵢ = τ₍ (diff⇒ Tᵢ<Tⱼ) (≢ₜ→≇ₑ Tᵢ≢Tⱼ) (≮×≢→⇏ Tⱼ≮Tᵢ (sym≢ Tᵢ≢Tⱼ))
tri⇒ a b | τ₌ Tᵢ≮Tⱼ refl  Tⱼ≮Tᵢ = tri⇒₌ a b
tri⇒ a b | τ₎ Tᵢ≮Tⱼ Tᵢ≢Tⱼ Tⱼ<Tᵢ = τ₎ (≮×≢→⇏ Tᵢ≮Tⱼ Tᵢ≢Tⱼ) (≢ₜ→≇ₑ Tᵢ≢Tⱼ) (diff⇒ Tⱼ<Tᵢ)

irrefl⇒ : ∀ {P T} {a : Event P T} → a ⇏ a
irrefl⇒ {a = a} with tri⇒ a a
irrefl⇒ | τ₍ a⇒a a≢a a⇏a = a⇏a
irrefl⇒ | τ₌ a⇏a a≢a _    = a⇏a
irrefl⇒ | τ₎ a⇏a a≢a a⇒a = a⇏a

_⇒?_ : ∀ {Pᵢ Pⱼ Tᵢ Tⱼ} → (a : Event Pᵢ Tᵢ) (b : Event Pⱼ Tⱼ) → Dec (a ⇒ b)
a ⇒? b with tri⇒ a b
a ⇒? b | τ₍ a⇒b a≇b b⇏a = yes a⇒b
a ⇒? b | τ₌ a⇏b a≅b b⇏a = no a⇏b
a ⇒? b | τ₎ a⇏b a≇b b⇒a = no a⇏b

max_stars_repo_name: mietek/lamport-timestamps

max_issues_repo_name: mietek/lamport-timestamps

max_forks_repo_name: mietek/lamport-timestamps