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

module FinNatLemmas where

open import Data.Empty using (⊥-elim)
open import Data.Product using (_×_; _,_)

open import Data.Nat
  using (ℕ; zero; suc; _+_; _*_; _<_; _≤_; _∸_; z≤n; s≤s; module ≤-Reasoning)
open import Data.Nat.Properties
  using (m+n∸n≡m; m≤m+n; +-∸-assoc; cancel-+-left)
open import Data.Nat.Properties.Simple
  using (+-comm; +-assoc; *-comm; distribʳ-*-+; +-right-identity)

open import Data.Fin
  using (Fin; zero; suc; toℕ; raise; fromℕ≤; reduce≥; inject+)
open import Data.Fin.Properties
  using (bounded; toℕ-injective; toℕ-raise; toℕ-fromℕ≤; inject+-lemma)

open import Relation.Binary using (module StrictTotalOrder)
open import Relation.Binary.Core using (_≢_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; subst; refl; sym; cong; cong₂; trans; module ≡-Reasoning)

------------------------------------------------------------------------------
-- Fin and Nat lemmas

toℕ-fin : (m n : ℕ) → (eq : m ≡ n) (fin : Fin m) →
  toℕ (subst Fin eq fin) ≡ toℕ fin
toℕ-fin m .m refl fin = refl

∸≡ : (m n : ℕ) (i j : Fin (m + n)) (i≥ : m ≤ toℕ i) (j≥ : m ≤ toℕ j) →
  toℕ i ∸ m ≡ toℕ j ∸ m → i ≡ j
∸≡ m n i j i≥ j≥ p = toℕ-injective pr
  where pr = begin (toℕ i
                    ≡⟨ sym (m+n∸n≡m (toℕ i) m) ⟩
                    (toℕ i + m) ∸ m
                    ≡⟨ cong (λ x → x ∸ m) (+-comm (toℕ i) m) ⟩
                    (m + toℕ i) ∸ m
                    ≡⟨ +-∸-assoc m i≥ ⟩
                    m + (toℕ i ∸ m)
                    ≡⟨ cong (λ x → m + x) p ⟩
                    m + (toℕ j ∸ m)
                    ≡⟨ sym (+-∸-assoc m j≥) ⟩
                    (m + toℕ j) ∸ m
                    ≡⟨ cong (λ x → x ∸ m) (+-comm m (toℕ j)) ⟩
                    (toℕ j + m) ∸ m
                    ≡⟨ m+n∸n≡m (toℕ j) m ⟩
                    toℕ j ∎)
             where open ≡-Reasoning

cancel-right∸ : (m n k : ℕ) (k≤m : k ≤ m) (k≤n : k ≤ n) →
  (m ∸ k ≡ n ∸ k) → m ≡ n
cancel-right∸ m n k k≤m k≤n mk≡nk =
  begin (m
         ≡⟨ sym (m+n∸n≡m m k) ⟩
         (m + k) ∸ k
         ≡⟨ cong (λ x → x ∸ k) (+-comm m k) ⟩
         (k + m) ∸ k
         ≡⟨ +-∸-assoc k k≤m ⟩
         k + (m ∸ k)
         ≡⟨ cong (λ x → k + x) mk≡nk ⟩
         k + (n ∸ k)
         ≡⟨ sym (+-∸-assoc k k≤n) ⟩
         (k + n) ∸ k
         ≡⟨ cong (λ x → x ∸ k) (+-comm k n) ⟩
         (n + k) ∸ k
         ≡⟨ m+n∸n≡m n k ⟩
         n ∎)
  where open ≡-Reasoning

raise< : (m n : ℕ) (i : Fin (m + n)) (i< : toℕ i < m) →
         toℕ (subst Fin (+-comm n m) (raise n (fromℕ≤ i<))) ≡ n + toℕ i
raise< m n i i< =
  begin (toℕ (subst Fin (+-comm n m) (raise n (fromℕ≤ i<)))
         ≡⟨ toℕ-fin (n + m) (m + n) (+-comm n m) (raise n (fromℕ≤ i<)) ⟩
         toℕ (raise n (fromℕ≤ i<))
         ≡⟨ toℕ-raise n (fromℕ≤ i<) ⟩
         n + toℕ (fromℕ≤ i<)
         ≡⟨ cong (λ x → n + x) (toℕ-fromℕ≤ i<) ⟩
         n + toℕ i ∎)
  where open ≡-Reasoning

toℕ-reduce≥ : (m n : ℕ) (i : Fin (m + n)) (i≥ : m ≤ toℕ i) →
               toℕ (reduce≥ i i≥) ≡ toℕ i ∸ m
toℕ-reduce≥ 0 n i _ = refl
toℕ-reduce≥ (suc m) n zero ()
toℕ-reduce≥ (suc m) n (suc i) (s≤s i≥) = toℕ-reduce≥ m n i i≥

inject≥ : (m n : ℕ) (i : Fin (m + n)) (i≥ : m ≤ toℕ i) →
        toℕ (subst Fin (+-comm n m) (inject+ m (reduce≥ i i≥))) ≡ toℕ i ∸ m
inject≥ m n i i≥ =
  begin (toℕ (subst Fin (+-comm n m) (inject+ m (reduce≥ i i≥)))
         ≡⟨ toℕ-fin (n + m) (m + n) (+-comm n m) (inject+ m (reduce≥ i i≥)) ⟩
         toℕ (inject+ m (reduce≥ i i≥))
         ≡⟨ sym (inject+-lemma m (reduce≥ i i≥)) ⟩
         toℕ (reduce≥ i i≥)
         ≡⟨ toℕ-reduce≥ m n i i≥ ⟩
         toℕ i ∸ m ∎)
  where open ≡-Reasoning

fromℕ≤-inj : (m n : ℕ) (i j : Fin n) (i< : toℕ i < m) (j< : toℕ j < m) →
  fromℕ≤ i< ≡ fromℕ≤ j< → i ≡ j
fromℕ≤-inj m n i j i< j< fi≡fj =
  toℕ-injective
    (trans (sym (toℕ-fromℕ≤ i<)) (trans (cong toℕ fi≡fj) (toℕ-fromℕ≤ j<)))

reduce≥-inj : (m n : ℕ) (i j : Fin (m + n)) (i≥ : m ≤ toℕ i) (j≥ : m ≤ toℕ j) →
  reduce≥ i i≥ ≡ reduce≥ j j≥ → i ≡ j
reduce≥-inj m n i j i≥ j≥ ri≡rj =
  toℕ-injective
    (cancel-right∸ (toℕ i) (toℕ j) m i≥ j≥
      (trans (sym (toℕ-reduce≥ m n i i≥))
      (trans (cong toℕ ri≡rj) (toℕ-reduce≥ m n j j≥))))

inj₁-toℕ≡ : {m n : ℕ} (i : Fin (m + n)) (i< : toℕ i < m) →
            toℕ i ≡ toℕ (inject+ n (fromℕ≤ i<))
inj₁-toℕ≡ {0} _ ()
inj₁-toℕ≡ {suc m} zero (s≤s z≤n) = refl
inj₁-toℕ≡ {suc (suc m)} (suc i) (s≤s (s≤s i<)) = cong suc (inj₁-toℕ≡ i (s≤s i<))

inj₁-≡ : {m n : ℕ} (i : Fin (m + n)) (i< : toℕ i < m) → i ≡ inject+ n (fromℕ≤ i<)
inj₁-≡ i i< = toℕ-injective (inj₁-toℕ≡ i i<)

inj₂-toℕ≡ :  {m n : ℕ} (i : Fin (m + n)) (i≥ : m ≤ toℕ i ) →
             toℕ i ≡ toℕ (raise m (reduce≥ i i≥))
inj₂-toℕ≡ {Data.Nat.zero} i i≥ = refl
inj₂-toℕ≡ {suc m} zero ()
inj₂-toℕ≡ {suc m} (suc i) (s≤s i≥) = cong suc (inj₂-toℕ≡ i i≥)

inj₂-≡ :  {m n : ℕ} (i : Fin (m + n)) (i≥ : m ≤ toℕ i ) → i ≡ raise m (reduce≥ i i≥)
inj₂-≡ i i≥ = toℕ-injective (inj₂-toℕ≡ i i≥)

inject+-injective : {m n : ℕ} (i j : Fin m) → (inject+ n i ≡ inject+ n j) → i ≡ j
inject+-injective {m} {n} i j p = toℕ-injective pf
  where
    open ≡-Reasoning
    pf : toℕ i ≡ toℕ j
    pf = begin (
      toℕ i
          ≡⟨ inject+-lemma n i ⟩
      toℕ (inject+ n i)
          ≡⟨ cong toℕ p ⟩
      toℕ (inject+ n j)
          ≡⟨ sym (inject+-lemma n j) ⟩
      toℕ j ∎)

raise-injective : {m n : ℕ} (i j : Fin n) → (raise m i ≡ raise m j) → i ≡ j
raise-injective {m} {n} i j p = toℕ-injective (cancel-+-left m pf)
  where
    open ≡-Reasoning
    pf : m + toℕ i ≡ m + toℕ j
    pf = begin (
      m + toℕ i
        ≡⟨ sym (toℕ-raise m i)  ⟩
      toℕ (raise m i)
        ≡⟨ cong toℕ p ⟩
      toℕ (raise m j)
        ≡⟨ toℕ-raise m j ⟩
      m + toℕ j ∎)

toℕ-invariance : ∀ {n n'} → (i : Fin n) → (eq : n ≡ n') → toℕ (subst Fin eq i) ≡ toℕ i
toℕ-invariance i refl = refl

-- see FinEquiv for the naming

inject+0≡uniti+ : ∀ {m} → (n : Fin m) → (eq : m ≡ m + 0) → inject+ 0 n ≡ subst Fin eq n
inject+0≡uniti+ {m} n eq = toℕ-injective pf
  where
    open ≡-Reasoning
    pf : toℕ (inject+ 0 n) ≡ toℕ (subst Fin eq n)
    pf = begin (
      toℕ (inject+ 0 n)
        ≡⟨ sym (inject+-lemma 0 n) ⟩
      toℕ n
        ≡⟨ sym (toℕ-invariance n eq) ⟩
      toℕ (subst Fin eq n) ∎)

-- Following code taken from
-- https://github.com/copumpkin/derpa/blob/master/REPA/Index.agda#L210

-- the next few bits are lemmas to prove uniqueness of euclidean division

-- first : for nonzero divisors, a nonzero quotient would require a larger
-- dividend than is consistent with a zero quotient, regardless of
-- remainders.

large : ∀ {d} {r : Fin (suc d)} x (r′ : Fin (suc d)) →
        toℕ r ≢ suc x * suc d + toℕ r′
large {d} {r} x r′ pf = irrefl pf (
    start
      suc (toℕ r)
    ≤⟨ bounded r ⟩
      suc d
    ≤⟨ m≤m+n (suc d) (x * suc d) ⟩
      suc d + x * suc d -- same as (suc x * suc d)
    ≤⟨ m≤m+n (suc x * suc d) (toℕ r′) ⟩
      suc x * suc d + toℕ r′ -- clearer in two steps; we'd need assoc anyway
    □)
  where
  open ≤-Reasoning
    renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≡⟨_⟩'_)
  open Relation.Binary.StrictTotalOrder Data.Nat.Properties.strictTotalOrder

-- a raw statement of the uniqueness, in the arrangement of terms that's
-- easiest to work with computationally

addMul-lemma′ : ∀ x x′ d (r r′ : Fin (suc d)) →
  x * suc d + toℕ r ≡ x′ * suc d + toℕ r′ → r ≡ r′ × x ≡ x′
addMul-lemma′ zero zero d r r′ hyp = (toℕ-injective hyp) , refl
addMul-lemma′ zero (suc x′) d r r′ hyp = ⊥-elim (large x′ r′ hyp)
addMul-lemma′ (suc x) zero d r r′ hyp = ⊥-elim (large x r (sym hyp))
addMul-lemma′ (suc x) (suc x′) d r r′ hyp
                      rewrite +-assoc (suc d) (x * suc d) (toℕ r)
                            | +-assoc (suc d) (x′ * suc d) (toℕ r′)
                      with addMul-lemma′ x x′ d r r′ (cancel-+-left (suc d) hyp)
... | pf₁ , pf₂ = pf₁ , cong suc pf₂

-- and now rearranged to the order that Data.Nat.DivMod uses

addMul-lemma : ∀ x x′ d (r r′ : Fin (suc d)) →
  toℕ r + x * suc d ≡ toℕ r′ + x′ * suc d → r ≡ r′ × x ≡ x′
addMul-lemma x x′ d r r′ hyp rewrite +-comm (toℕ r) (x * suc d)
                                   | +-comm (toℕ r′) (x′ * suc d)
  = addMul-lemma′ x x′ d r r′ hyp

-- purely about Nat, but still not in Data.Nat.Properties.Simple

distribˡ-*-+ : ∀ m n o → m * (n + o)  ≡ m * n + m * o
distribˡ-*-+ m n o =
  trans (*-comm m (n + o)) (
  trans (distribʳ-*-+ m n o) (
        (cong₂ _+_ (*-comm n m) (*-comm o m))))

*-right-identity : ∀ n → n * 1 ≡ n
*-right-identity n = trans (*-comm n 1) (+-right-identity n)

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

ext: agda

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

test : (A : Set) (let X = _) (x : X) (p : A ≡ Bool) → Bool
test .Bool true  refl = false
test .Bool false refl = true

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2014-09-23
-- Syntax declaration for overloaded constructor.

module _ where

module A where

  syntax c x = ⟦ x ⟧

  data D2 (A : Set) : Set where
    c : A → D2 A

  data D1 : Set where
    c : D1

open A

test : D2 D1
test = ⟦ c ⟧

-- Should work.


text:
module Issue1419 where

module A where
  module M where

module B where
  module M where

open A
open B

module N (let open M) where

  module LotsOfStuff where


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A simple example of a program using the foreign function interface
------------------------------------------------------------------------

module README.Foreign.Haskell where

-- In order to be considered safe by Agda, the standard library cannot
-- add COMPILE pragmas binding the inductive types it defines to concrete
-- Haskell types.

-- To work around this limitation, we have defined FFI-friendly versions
-- of these types together with a zero-cost coercion `coerce`.

open import Level using (Level)
open import Agda.Builtin.Int
open import Agda.Builtin.Nat
open import Data.Bool.Base using (Bool; if_then_else_)
open import Data.Char as Char
open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Product
open import Function
open import Relation.Nullary.Decidable

import Foreign.Haskell as FFI
open import Foreign.Haskell.Coerce

private
  variable
    a : Level
    A : Set a

-- Here we use the FFI version of Maybe and Pair.

postulate
  primUncons    : List A → FFI.Maybe (FFI.Pair A (List A))
  primCatMaybes : List (FFI.Maybe A) → List A
  primTestChar  : Char → Bool
  primIntEq     : Int → Int → Bool

{-# COMPILE GHC primUncons = \ _ _ xs -> case xs of
  { []       -> Nothing
  ; (x : xs) -> Just (x, xs)
  }
#-}

{-# FOREIGN GHC import Data.Maybe #-}
{-# COMPILE GHC primCatMaybes = \ _ _ -> catMaybes #-}

{-# COMPILE GHC primTestChar = ('-' /=) #-}

{-# COMPILE GHC primIntEq = (==) #-}

-- We however want to use the notion of Maybe and Pair internal to
-- the standard library. For this we use `coerce` to take use back
-- to the types we are used to.

-- The typeclass mechanism uses the coercion rules for Maybe and Pair,
-- as well as the knowledge that natural numbers are represented as
-- integers.
-- We additionally benefit from the congruence rules for List, Char,
-- Bool, and a reflexivity principle for variable A.

uncons : List A → Maybe (A × List A)
uncons = coerce primUncons

catMaybes : List (Maybe A) → List A
catMaybes = coerce primCatMaybes

testChar : Char → Bool
testChar = coerce primTestChar
  -- note that coerce is useless here but the proof could come from
  -- either `coerce-fun coerce-refl coerce-refl` or `coerce-refl` alone
  -- We (and Agda) do not care which proof we got.

eqNat : Nat → Nat → Bool
eqNat = coerce primIntEq
  -- We can coerce `Nat` to `Int` but not `Int` to `Nat`. This fundamentally
  -- relies on the fact that `Coercible` understands that functions are
  -- contravariant.

open import IO
open import Codata.Musical.Notation
open import Data.String.Base
open import Relation.Nullary.Negation

-- example program using uncons, catMaybes, and testChar

main = run $
  ♯ readFiniteFile "README/Foreign/Haskell.agda" {- read this file -} >>= λ f →
  ♯ let chars   = toList f in
    let cleanup = catMaybes ∘ List.map (λ c → if testChar c then just c else nothing) in
    let cleaned = dropWhile ('\n' ≟_) $ cleanup chars in
  case uncons cleaned of λ where
    nothing         → putStrLn "I cannot believe this file is filed with dashes only!"
    (just (c , cs)) → putStrLn $ unlines
                    $ ("First (non dash) character: " ++ Char.show c)
                    ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≟_)) cs))
                    ∷ []

-- You can compile and run this test by writing:
-- agda -c Haskell.agda
-- ../../Haskell

-- You should see the following text (without the indentation on the left):
--   First (non dash) character: ' '
--   Rest (dash free) of the line: The Agda standard library


text:
{-# OPTIONS --sized-types #-}

module Sized.Data.List where

import      Lvl
open import Lang.Size
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T A A₁ A₂ B B₁ B₂ Result : Type{ℓ}
private variable s s₁ s₂ : Size

data List(s : Size){ℓ} (T : Type{ℓ}) : Type{ℓ} where
  ∅   : List(s)(T) -- An empty list
  _⊰_ : ∀{sₛ : <ˢⁱᶻᵉ s} → T → List(sₛ)(T) → List(s)(T) -- Cons
infixr 1000 _⊰_

tail : List(s)(T) → List(s)(T)
tail ∅       = ∅
tail (_ ⊰ l) = l

{-
-- TODO: Size problems. See notes in Lang.Size.
_++_ : List(s)(T) → List(s)(T) → List(s)(T)
_++_         ∅                   b = b
_++_ {s = s} (_⊰_ {sₛ = sₛ} x a) b = _⊰_ {s = s}{sₛ = sₛ} x (_++_ {s = sₛ} a b)
infixl 1000 _++_
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import HoTT

{- The cofiber space of [winl : X → X ∨ Y] is equivalent to [Y],
 - and the cofiber space of [winr : Y → X ∨ Y] is equivalent to [X]. -}

module homotopy.WedgeCofiber {i} (X Y : Ptd i) where

  module CofWinl where

    module Into = CofiberRec {f = winl} (pt Y) (projr X Y) (λ _ → idp)

    into = Into.f

    out : de⊙ Y → Cofiber (winl {X = X} {Y = Y})
    out = cfcod ∘ winr

    abstract
      out-into : (κ : Cofiber (winl {X = X} {Y = Y})) → out (into κ) == κ
      out-into = Cofiber-elim
        (! (cfglue (pt X) ∙ ap cfcod wglue))
        (Wedge-elim
          (λ x → ! (cfglue (pt X) ∙ ap cfcod wglue) ∙ cfglue x)
          (λ y → idp)
          (↓-='-from-square $
            (lemma (cfglue (pt X)) (ap cfcod wglue)
             ∙h⊡ (ap-∘ out (projr X Y) wglue ∙ ap (ap out) (Projr.glue-β X Y))
                  ∙v⊡ bl-square (ap cfcod wglue))))
        (λ x → ↓-∘=idf-from-square out into $
          ! (∙-unit-r _) ∙h⊡
            ap (ap out) (Into.glue-β x) ∙v⊡
             hid-square {p = (! (cfglue' winl (pt X) ∙ ap cfcod wglue))}
             ⊡v connection {q = cfglue x})
        where
        lemma : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z)
          → ! (p ∙ q) ∙ p == ! q
        lemma idp idp = idp

    eq : Cofiber winl ≃ de⊙ Y
    eq = equiv into out (λ _ → idp) out-into

    ⊙eq : ⊙Cofiber ⊙winl ⊙≃ Y
    ⊙eq = ≃-to-⊙≃ eq idp

  cfcod-winl-projr-comm-sqr : CommSquare (cfcod' winl) (projr X Y) (idf _) CofWinl.into
  cfcod-winl-projr-comm-sqr = comm-sqr λ _ → idp

  module CofWinr where

    module Into = CofiberRec {f = winr} (pt X) (projl X Y) (λ _ → idp)

    into = Into.f

    out : de⊙ X → Cofiber (winr {X = X} {Y = Y})
    out = cfcod ∘ winl

    abstract
      out-into : ∀ κ → out (into κ) == κ
      out-into = Cofiber-elim
        (ap cfcod wglue ∙ ! (cfglue (pt Y)))
        (Wedge-elim
          (λ x → idp)
          (λ y → (ap cfcod wglue ∙ ! (cfglue (pt Y))) ∙ cfglue y)
          (↓-='-from-square $
            (ap-∘ out (projl X Y) wglue ∙ ap (ap out) (Projl.glue-β X Y)) ∙v⊡
               connection
             ⊡h∙ ! (lemma (ap (cfcod' winr) wglue) (cfglue (pt Y)))))
        (λ y → ↓-∘=idf-from-square out into $
          ! (∙-unit-r _) ∙h⊡
            ap (ap out) (Into.glue-β y) ∙v⊡
              hid-square {p = (ap (cfcod' winr) wglue ∙ ! (cfglue (pt Y)))}
              ⊡v connection {q = cfglue y})
        where
        lemma : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : z == y)
          → (p ∙ ! q) ∙ q == p
        lemma idp idp = idp

    eq : Cofiber winr ≃ de⊙ X
    eq = equiv into out (λ _ → idp) out-into

    ⊙eq : ⊙Cofiber ⊙winr ⊙≃ X
    ⊙eq = ≃-to-⊙≃ eq idp

  cfcod-winr-projl-comm-sqr : CommSquare (cfcod' winr) (projl X Y) (idf _) CofWinr.into
  cfcod-winr-projl-comm-sqr = comm-sqr λ _ → idp

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Issue1278.A (X : Set1) where

  data D : Set where
    d : D

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Combinators for logical reasoning
{-# OPTIONS --without-K --safe --exact-split #-}

module Constructive.Combinators where

-- agda-stdlib
open import Data.Empty
open import Data.Sum as Sum
open import Data.Product as Prod
open import Function.Base
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
import Relation.Unary as U
open import Relation.Binary.PropositionalEquality

-- agda-misc
open import Constructive.Common

---------------------------------------------------------------------------
-- Combinators
---------------------------------------------------------------------------

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
  →-distrib-⊎-× : ((A ⊎ B) → C) → (A → C) × (B → C)
  →-distrib-⊎-× f = f ∘ inj₁ , f ∘ inj₂

  →-undistrib-⊎-× : (A → C) × (B → C) → (A ⊎ B) → C
  →-undistrib-⊎-× (f , g) (inj₁ x) = f x
  →-undistrib-⊎-× (f , g) (inj₂ y) = g y

  →-undistrib-⊎-×-flip : (A ⊎ B) → (A → C) × (B → C) → C
  →-undistrib-⊎-×-flip = flip →-undistrib-⊎-×

  →-undistrib-×-⊎ : (A → C) ⊎ (B → C) → (A × B) → C
  →-undistrib-×-⊎ (inj₁ f) (x , y) = f x
  →-undistrib-×-⊎ (inj₂ g) (x , y) = g y

  →-undistrib-×-⊎-flip : (A × B) → (A → C) ⊎ (B → C) → C
  →-undistrib-×-⊎-flip = flip →-undistrib-×-⊎

-- contradiction
contradiction : ∀ {a w} {A : Set a} {WhatEver : Set w} → A → ¬ A → WhatEver
contradiction x ¬x = ⊥-elim (¬x x)

-- sum and product
module _ {a b} {A : Set a} {B : Set b} where
  A⊎B→¬A→B : A ⊎ B → ¬ A → B
  A⊎B→¬A→B (inj₁ x) ¬A = contradiction x ¬A
  A⊎B→¬A→B (inj₂ y) ¬A = y

  A⊎B→¬B→A : A ⊎ B → ¬ B → A
  A⊎B→¬B→A (inj₁ x) ¬B = x
  A⊎B→¬B→A (inj₂ y) ¬B = contradiction y ¬B

  ¬A⊎B→A→B : ¬ A ⊎ B → A → B
  ¬A⊎B→A→B (inj₁ ¬A) x = contradiction x ¬A
  ¬A⊎B→A→B (inj₂ y)  _ = y

  [A→B]→¬[A×¬B] : (A → B) → ¬ (A × ¬ B)
  [A→B]→¬[A×¬B] f (x , y) = y (f x)

  A×B→¬[A→¬B] : A × B → ¬ (A → ¬ B)
  A×B→¬[A→¬B] (x , y) f = f x y

  -- De Morgan's laws
  ¬[A⊎B]→¬A×¬B : ¬ (A ⊎ B) → ¬ A × ¬ B
  ¬[A⊎B]→¬A×¬B = →-distrib-⊎-×

  ¬A×¬B→¬[A⊎B] : ¬ A × ¬ B → ¬ (A ⊎ B)
  ¬A×¬B→¬[A⊎B] = →-undistrib-⊎-×

  A⊎B→¬[¬A×¬B] : A ⊎ B → ¬ (¬ A × ¬ B)
  A⊎B→¬[¬A×¬B] = →-undistrib-⊎-×-flip

  ¬A⊎¬B→¬[A×B] : ¬ A ⊎ ¬ B → ¬ (A × B)
  ¬A⊎¬B→¬[A×B] = →-undistrib-×-⊎

  A×B→¬[¬A⊎¬B] : A × B → ¬ (¬ A ⊎ ¬ B)
  A×B→¬[¬A⊎¬B] = →-undistrib-×-⊎-flip

  -- Double negated DEM₃
  ¬[A×B]→¬¬[¬A⊎¬B] : ¬ (A × B) → ¬ ¬ (¬ A ⊎ ¬ B)
  ¬[A×B]→¬¬[¬A⊎¬B] ¬[A×B] ¬[¬A⊎¬B] =
    ¬[¬A⊎¬B] (inj₁ λ x → contradiction (inj₂ (λ y → ¬[A×B] (x , y))) ¬[¬A⊎¬B])

  dec⊎⇒¬[A×B]→¬A⊎¬B : Dec⊎ A → Dec⊎ B → ¬ (A × B) → ¬ A ⊎ ¬ B
  dec⊎⇒¬[A×B]→¬A⊎¬B (inj₁ x)  (inj₁ y)  ¬[A×B] = contradiction (x , y) ¬[A×B]
  dec⊎⇒¬[A×B]→¬A⊎¬B (inj₁ x)  (inj₂ ¬y) ¬[A×B] = inj₂ ¬y
  dec⊎⇒¬[A×B]→¬A⊎¬B (inj₂ ¬x) _         ¬[A×B] = inj₁ ¬x

  join : (A → A → B) → A → B
  join f x = f x x

-- properties of negation
module _ {a} {A : Set a} where
  [A→¬A]→¬A : (A → ¬ A) → ¬ A
  [A→¬A]→¬A = join

  [¬A→A]→¬¬A : (¬ A → A) → ¬ ¬ A
  [¬A→A]→¬¬A ¬A→A ¬A = ¬A (¬A→A ¬A)

  -- Law of noncontradiction (LNC)
  ¬[A×¬A] : ¬ (A × ¬ A)
  ¬[A×¬A] = uncurry (flip _$_)

module _ {a b} {A : Set a} {B : Set b} where
  ¬[A→B]→¬B : ¬ (A → B) → ¬ B
  ¬[A→B]→¬B ¬[A→B] y = ¬[A→B] (const y)

  ¬[A→B]→¬[A→¬¬B] : ¬ (A → B) → ¬ (A → ¬ ¬ B)
  ¬[A→B]→¬[A→¬¬B] ¬[A→B] A→¬¬B = ¬[A→B] λ x → ⊥-elim $ A→¬¬B x (¬[A→B]→¬B ¬[A→B])

  ¬[A→B]→B→A : ¬ (A → B) → B → A
  ¬[A→B]→B→A ¬[A→B] y = contradiction (λ _ → y) ¬[A→B]

  [[A→B]→A]→¬A→A : ((A → B) → A) → ¬ A → A
  [[A→B]→A]→¬A→A [A→B]→A ¬A = [A→B]→A (⊥-elim ∘′ ¬A)

  [[A→B]→A]→¬¬A : ((A → B) → A) → ¬ ¬ A
  [[A→B]→A]→¬¬A [A→B]→A ¬A = ¬A ([[A→B]→A]→¬A→A [A→B]→A ¬A)

  [[[A→B]→A]→A]→¬B→¬¬A→A : (((A → B) → A) → A) → ¬ B → ¬ ¬ A → A
  [[[A→B]→A]→A]→¬B→¬¬A→A [[A→B]→A]→A ¬B ¬¬A =
    [[A→B]→A]→A λ A→B → contradiction (flip _∘′_ A→B ¬B) ¬¬A

module _ {a b} {A : Set a} {B : Set b} where
  contraposition : (A → B) → ¬ B → ¬ A
  contraposition = flip _∘′_

  -- variant of contraposition
  [A→¬¬B]→¬B→¬A : (A → ¬ ¬ B) → ¬ B → ¬ A
  [A→¬¬B]→¬B→¬A f ¬B x = (f x) ¬B

  [¬A→¬B]→¬¬[B→A] : (¬ A → ¬ B) → ¬ ¬ (B → A)
  [¬A→¬B]→¬¬[B→A] ¬A→¬B ¬[B→A] = ¬[B→A] λ y → ⊥-elim $ ¬A→¬B (¬[A→B]→¬B ¬[B→A]) y

  [A→¬B]→¬¬A→¬B : (A → ¬ B) → ¬ ¬ A → ¬ B
  [A→¬B]→¬¬A→¬B A→¬B ¬¬A y = ¬¬A λ x → A→¬B x y

module _ {a} {A : Set a} where
  -- introduction for double negation
  DN-intro : A → ¬ ¬ A
  DN-intro = flip _$_

  -- triple negation to negation
  TN-to-N : ¬ ¬ ¬ A → ¬ A
  TN-to-N = contraposition DN-intro

  -- Double negation of excluded middle
  DN-Dec⊎ : ¬ ¬ Dec⊎ A
  DN-Dec⊎ = λ f → (f ∘ inj₂) (f ∘ inj₁)

-- eliminator for ⊥
⊥-stable : ¬ ¬ ⊥ → ⊥
⊥-stable f = f id

-- Double negation is monad
module _ {a} {A : Set a} where
  DN-join : ¬ ¬ ¬ ¬ A → ¬ ¬ A
  DN-join = TN-to-N

module _ {a b} {A : Set a} {B : Set b} where
  DN-map : (A → B) → ¬ ¬ A → ¬ ¬ B
  DN-map = contraposition ∘′ contraposition

module _ {a b} {A : Set a} {B : Set b} where
  DN-bind : (A → ¬ ¬ B) → ¬ ¬ A → ¬ ¬ B
  DN-bind f = DN-join ∘′ DN-map f

  DN-bind⁻¹ : (¬ ¬ A → ¬ ¬ B) → A → ¬ ¬ B
  DN-bind⁻¹ f = f ∘′ DN-intro

module _ {a b} {A : Set a} {B : Set b} where
  DN-ap : ¬ ¬ (A → B) → ¬ ¬ A → ¬ ¬ B
  DN-ap ff fx = DN-bind (λ f → DN-map f fx) ff

  DN-ap⁻¹ : (¬ ¬ A → ¬ ¬ B) → ¬ ¬ (A → B)
  DN-ap⁻¹ f ¬[A→B] = ¬[A→B]→¬[A→¬¬B] ¬[A→B] (DN-bind⁻¹ f)

-- distributive properties
  DN-distrib-× : ¬ ¬ (A × B) → ¬ ¬ A × ¬ ¬ B
  DN-distrib-× ¬¬A×B = DN-map proj₁ ¬¬A×B , DN-map proj₂ ¬¬A×B

  DN-undistrib-× : ¬ ¬ A × ¬ ¬ B → ¬ ¬ (A × B)
  DN-undistrib-× = [A→¬¬B]→¬B→¬A ¬[A×B]→¬¬[¬A⊎¬B] ∘′ ¬A×¬B→¬[A⊎B]

  DN-undistrib-⊎ : ¬ ¬ A ⊎ ¬ ¬ B → ¬ ¬ (A ⊎ B)
  DN-undistrib-⊎ = Sum.[ DN-map inj₁ , DN-map inj₂ ]

  stable-undistrib-× : Stable A × Stable B → Stable (A × B)
  stable-undistrib-× (A-stable , B-stable) ¬¬[A×B] =
    Prod.map A-stable B-stable $ DN-distrib-× ¬¬[A×B]

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
  ip-⊎-DN : (A → (B ⊎ C)) → ¬ ¬ ((A → B) ⊎ (A → C))
  ip-⊎-DN f =
    DN-map Sum.[ (Sum.map const const ∘ f) , (λ ¬A → inj₁ λ x → ⊥-elim (¬A x)) ]
          DN-Dec⊎

DN-ip : ∀ {p q r} {P : Set p} {Q : Set q} {R : Q → Set r} →
        Q → (P → Σ Q R) → ¬ ¬ (Σ Q λ x → (P → R x))
DN-ip q f =
  DN-map Sum.[ (λ x → Prod.map₂ const (f x)) ,
               (λ ¬P → q , λ P → ⊥-elim $ ¬P P) ] DN-Dec⊎

-- Properties of Dec⊎
module _ {a} {A : Set a} where
  dec⊎⇒dec : Dec⊎ A → Dec A
  dec⊎⇒dec (inj₁ x) = yes x
  dec⊎⇒dec (inj₂ y) = no y

  dec⇒dec⊎ : Dec A → Dec⊎ A
  dec⇒dec⊎ (yes p) = inj₁ p
  dec⇒dec⊎ (no ¬p) = inj₂ ¬p

  ¬-dec⊎ : Dec⊎ A → Dec⊎ (¬ A)
  ¬-dec⊎ (inj₁ x) = inj₂ (DN-intro x)
  ¬-dec⊎ (inj₂ y) = inj₁ y

module _ {a b} {A : Set a} {B : Set b} where
  dec⊎-map : (A → B) → (B → A) → Dec⊎ A → Dec⊎ B
  dec⊎-map f g dec⊎ = Sum.map f (contraposition g) dec⊎

  dec⊎-⊎ : Dec⊎ A → Dec⊎ B → Dec⊎ (A ⊎ B)
  dec⊎-⊎ (inj₁ x)  _         = inj₁ (inj₁ x)
  dec⊎-⊎ (inj₂ ¬x) (inj₁ y)  = inj₁ (inj₂ y)
  dec⊎-⊎ (inj₂ ¬x) (inj₂ ¬y) = inj₂ (¬A×¬B→¬[A⊎B] (¬x , ¬y))

  dec⊎-× : Dec⊎ A → Dec⊎ B → Dec⊎ (A × B)
  dec⊎-× (inj₁ x)  (inj₁ y)  = inj₁ (x , y)
  dec⊎-× (inj₁ x)  (inj₂ ¬y) = inj₂ (¬y ∘ proj₂)
  dec⊎-× (inj₂ ¬x) _         = inj₂ (¬x ∘ proj₁)

-- Properties of Stable
module _ {a} {A : Set a} where
  dec⇒stable : Dec A → Stable A
  dec⇒stable (yes p) ¬¬A = p
  dec⇒stable (no ¬p) ¬¬A = ⊥-elim (¬¬A ¬p)

  ¬-stable : Stable (¬ A)
  ¬-stable = TN-to-N

  dec⊎⇒stable : Dec⊎ A → Stable A
  dec⊎⇒stable dec⊎ = dec⇒stable (dec⊎⇒dec dec⊎)

module _ {a p} {A : Set a} {P : A → Set p} where
  DecU⇒stable : DecU P → ∀ x → Stable (P x)
  DecU⇒stable P? x = dec⊎⇒stable (P? x)

  -- Properties of DecU
  ¬-DecU : DecU P → DecU (λ x → ¬ (P x))
  ¬-DecU P? x = ¬-dec⊎ (P? x)

  DecU⇒decidable : DecU P → U.Decidable P
  DecU⇒decidable P? x = dec⊎⇒dec (P? x)

  decidable⇒DecU : U.Decidable P → DecU P
  decidable⇒DecU P? x = dec⇒dec⊎ (P? x)

DecU-map : ∀ {a b p} {A : Set a} {B : Set b} {P : A → Set p} →
  (f : B → A) → DecU P → DecU (λ x → P (f x))
DecU-map f P? x = dec⊎-map id id (P? (f x))

module _ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} where
  DecU-⊎ : DecU P → DecU Q → DecU (λ x → P x ⊎ Q x)
  DecU-⊎ P? Q? x = dec⊎-⊎ (P? x) (Q? x)

  DecU-× : DecU P → DecU Q → DecU (λ x → P x × Q x)
  DecU-× P? Q? x = dec⊎-× (P? x) (Q? x)

-- Quantifier
module _ {a p} {A : Set a} {P : A → Set p} where
  ∃P→¬∀¬P : ∃ P → ¬ (∀ x → ¬ (P x))
  ∃P→¬∀¬P = flip uncurry

  ∀P→¬∃¬P : (∀ x → P x) → ¬ ∃ λ x → ¬ (P x)
  ∀P→¬∃¬P f (x , ¬Px) = ¬Px (f x)

  ¬∃P→∀¬P : ¬ ∃ P → ∀ x → ¬ (P x)
  ¬∃P→∀¬P = curry

  ∀¬P→¬∃P : (∀ x → ¬ (P x)) → ¬ ∃ P
  ∀¬P→¬∃P = uncurry

  ∃¬P→¬∀P : ∃ (λ x → ¬ (P x)) → ¬ (∀ x → P x)
  ∃¬P→¬∀P (x , ¬Px) ∀P = ¬Px (∀P x)

  ¬∀¬P→¬¬∃P : ¬ (∀ x → ¬ P x) → ¬ ¬ ∃ P
  ¬∀¬P→¬¬∃P ¬∀¬P = contraposition ¬∃P→∀¬P ¬∀¬P

  ¬¬∃P→¬∀¬P : ¬ ¬ ∃ P → ¬ (∀ x → ¬ P x)
  ¬¬∃P→¬∀¬P ¬¬∃P = contraposition ∀¬P→¬∃P ¬¬∃P

  ¬¬∀P→¬∃¬P : ¬ ¬ (∀ x → P x) → ¬ ∃ λ x → ¬ (P x)
  ¬¬∀P→¬∃¬P ¬¬∀P = contraposition ∃¬P→¬∀P ¬¬∀P

  ¬¬∃P<=>¬∀¬P : ¬ ¬ ∃ P <=> ¬ (∀ x → ¬ P x)
  ¬¬∃P<=>¬∀¬P = mk<=> ¬¬∃P→¬∀¬P ¬∀¬P→¬¬∃P

  -- remove?
  ∀¬¬P→¬∃¬P : (∀ x → ¬ ¬ P x) → ¬ ∃ λ x → ¬ (P x)
  ∀¬¬P→¬∃¬P = uncurry

  -- converse of DNS
  ¬¬∀P→∀¬¬P : ¬ ¬ (∀ x → P x) → ∀ x → ¬ ¬ P x
  ¬¬∀P→∀¬¬P f x = DN-map (λ ∀P → ∀P x) f

  ∃¬¬P→¬¬∃P  : (∃ λ x → ¬ ¬ P x) → ¬ ¬ ∃ λ x → P x
  ∃¬¬P→¬¬∃P (x , ¬¬Px) = DN-map (λ Px → x , Px) ¬¬Px

  ¬¬∃¬P→¬∀P : ¬ ¬ ∃ (λ x → ¬ (P x)) → ¬ (∀ x → P x)
  ¬¬∃¬P→¬∀P = contraposition ∀P→¬∃¬P

  ¬∃¬P→∀¬¬P : ¬ ∃ (λ x → ¬ P x) → ∀ x → ¬ ¬ P x
  ¬∃¬P→∀¬¬P = curry

  ∀P→∀¬¬P : (∀ x → P x) → ∀ x → ¬ ¬ P x
  ∀P→∀¬¬P ∀P x = DN-intro (∀P x)

  ∃P→∃¬¬P : ∃ P → ∃ λ x → ¬ ¬ P x
  ∃P→∃¬¬P (x , Px) = x , DN-intro Px

module _ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} where
  [∀¬P→∀¬Q]→¬¬[∃Q→∃P] : ((∀ x → ¬ P x) → (∀ x → ¬ Q x)) → ¬ ¬ (∃ Q → ∃ P)
  [∀¬P→∀¬Q]→¬¬[∃Q→∃P] ∀¬P→∀¬Q =
    DN-ap⁻¹ (¬∀¬P→¬¬∃P ∘ contraposition ∀¬P→∀¬Q ∘ ¬¬∃P→¬∀¬P)

-- Quantifier rearrangement for stable predicate
module _ {a p} {A : Set a} {P : A → Set p} (P-stable : ∀ x → Stable (P x)) where
  P-stable⇒∃¬¬P→∃P : ∃ (λ x → ¬ ¬ P x) → ∃ P
  P-stable⇒∃¬¬P→∃P (x , ¬¬Px) = x , P-stable x ¬¬Px

  P-stable⇒∀¬¬P→∀P : (∀ x → ¬ ¬ P x) → ∀ x → P x
  P-stable⇒∀¬¬P→∀P ∀¬¬P x = P-stable x (∀¬¬P x)

  P-stable⇒¬¬∀P→∀P : ¬ ¬ (∀ x → P x) → ∀ x → P x
  P-stable⇒¬¬∀P→∀P = P-stable⇒∀¬¬P→∀P ∘′ ¬¬∀P→∀¬¬P

  P-stable⇒¬∃¬P→∀P : ¬ ∃ (λ x → ¬ P x) → ∀ x → P x
  P-stable⇒¬∃¬P→∀P ¬∃¬P = P-stable⇒∀¬¬P→∀P (¬∃¬P→∀¬¬P ¬∃¬P)

  P-stable⇒¬∀P→¬¬∃¬P : ¬ (∀ x → P x) → ¬ ¬ ∃ (λ x → ¬ (P x))
  P-stable⇒¬∀P→¬¬∃¬P ¬∀P = contraposition P-stable⇒¬∃¬P→∀P ¬∀P

module _ {a p} {A : Set a} {P : A → Set p} (P? : DecU P) where
  P?⇒∃¬¬P→∃P : ∃ (λ x → ¬ ¬ P x) → ∃ P
  P?⇒∃¬¬P→∃P = P-stable⇒∃¬¬P→∃P (DecU⇒stable P?)

  P?⇒∀¬¬P→∀P : (∀ x → ¬ ¬ P x) → ∀ x → P x
  P?⇒∀¬¬P→∀P = P-stable⇒∀¬¬P→∀P (DecU⇒stable P?)

  P?⇒¬¬∀P→∀P : ¬ ¬ (∀ x → P x) → ∀ x → P x
  P?⇒¬¬∀P→∀P = P-stable⇒¬¬∀P→∀P (DecU⇒stable P?)

  P?⇒¬∃¬P→∀P : ¬ ∃ (λ x → ¬ P x) → ∀ x → P x
  P?⇒¬∃¬P→∀P = P-stable⇒¬∃¬P→∀P (DecU⇒stable P?)

  P?⇒¬∀P→¬¬∃¬P : ¬ (∀ x → P x) → ¬ ¬ ∃ (λ x → ¬ P x)
  P?⇒¬∀P→¬¬∃¬P = P-stable⇒¬∀P→¬¬∃¬P (DecU⇒stable P?)

  -- call/cc
  P?⇒[¬∀P→∀P]→∀P : (¬ (∀ x → P x) → ∀ x → P x) → ∀ x → P x
  P?⇒[¬∀P→∀P]→∀P ¬∀P→∀P = P?⇒¬¬∀P→∀P λ ¬∀P → ¬∀P (¬∀P→∀P ¬∀P)

  P?⇒[∃¬P→∀P]→∀P : (∃ (λ x → ¬ P x) → ∀ x → P x) → ∀ x → P x
  P?⇒[∃¬P→∀P]→∀P ∃¬P→∀P =
    P?⇒¬¬∀P→∀P λ ¬∀P → P?⇒¬∀P→¬¬∃¬P ¬∀P λ ∃¬P → ¬∀P (∃¬P→∀P ∃¬P)

  -- [∀¬P→¬∀Q]→¬∃¬Q→¬¬∃P

module _ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} where
  P?⇒[∃¬P→∃¬Q]→∀Q→∀P : DecU P → (∃ (λ x → ¬ P x) → ∃ (λ x → ¬ Q x)) →
                       (∀ x → Q x) → ∀ x → P x
  P?⇒[∃¬P→∃¬Q]→∀Q→∀P P? ∃¬P→∃¬Q =
    P?⇒¬∃¬P→∀P P? ∘ contraposition ∃¬P→∃¬Q ∘ ∀P→¬∃¬P

  P?⇒[∃Q→∀P]→¬∀¬Q→∀P : DecU P → (∃ Q → ∀ x → P x) → ¬ (∀ x → ¬ Q x) → ∀ x → P x
  P?⇒[∃Q→∀P]→¬∀¬Q→∀P P? ∃Q→∀P ¬∀¬Q = P?⇒¬¬∀P→∀P P? (DN-map ∃Q→∀P (¬∀¬P→¬¬∃P ¬∀¬Q))

  ¬[¬∀P⊎¬∀Q]→∀P×∀Q : DecU P → DecU Q → ¬ (¬ (∀ x → P x) ⊎ ¬ (∀ x → Q x)) →
                     (∀ x → P x) × (∀ x → Q x)
  ¬[¬∀P⊎¬∀Q]→∀P×∀Q P? Q? ¬[¬∀P⊎¬∀Q] =
    Prod.map (P?⇒¬¬∀P→∀P P?) (P?⇒¬¬∀P→∀P Q?) (¬[A⊎B]→¬A×¬B ¬[¬∀P⊎¬∀Q])

module _ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} where
  ∃-undistrib-⊎ : ∃ P ⊎ ∃ Q → ∃ (λ x → P x ⊎ Q x)
  ∃-undistrib-⊎ (inj₁ (x , Px)) = x , inj₁ Px
  ∃-undistrib-⊎ (inj₂ (x , Qx)) = x , inj₂ Qx

  ∃-distrib-⊎ : ∃ (λ x → P x ⊎ Q x) → ∃ P ⊎ ∃ Q
  ∃-distrib-⊎ (x , inj₁ Px) = inj₁ (x , Px)
  ∃-distrib-⊎ (x , inj₂ Qx) = inj₂ (x , Qx)

  ∃-distrib-× : ∃ (λ x → P x × Q x) → ∃ P × ∃ Q
  ∃-distrib-× (x , Px , Qx) = (x , Px) , (x , Qx)

  ∀-undistrib-× : (∀ x → P x) × (∀ x → Q x) → ∀ x → P x × Q x
  ∀-undistrib-× (∀P , ∀Q) x = ∀P x , ∀Q x

  ∀-distrib-× : (∀ x → P x × Q x) → (∀ x → P x) × (∀ x → Q x)
  ∀-distrib-× ∀x→Px×Qx = proj₁ ∘ ∀x→Px×Qx , proj₂ ∘ ∀x→Px×Qx

  ∀-undistrib-⊎ : (∀ x → P x) ⊎ (∀ x → Q x) → ∀ x → P x ⊎ Q x
  ∀-undistrib-⊎ (inj₁ ∀P) x = inj₁ (∀P x)
  ∀-undistrib-⊎ (inj₂ ∀Q) x = inj₂ (∀Q x)

  ¬[¬∃P×¬∃Q]→¬¬∃x→Px⊎Qx : ¬ (¬ ∃ P × ¬ ∃ Q) → ¬ ¬ ∃ λ x → P x ⊎ Q x
  ¬[¬∃P×¬∃Q]→¬¬∃x→Px⊎Qx = DN-map ∃-undistrib-⊎ ∘′ contraposition ¬[A⊎B]→¬A×¬B

  [¬¬∃x→Px⊎Qx]→¬[¬∃P×¬∃Q] : (¬ ¬ ∃ λ x → P x ⊎ Q x) → ¬ (¬ ∃ P × ¬ ∃ Q)
  [¬¬∃x→Px⊎Qx]→¬[¬∃P×¬∃Q] = contraposition ¬A×¬B→¬[A⊎B] ∘′ DN-map ∃-distrib-⊎

  ¬∀¬P×¬∀¬Q→¬¬[∃P×∃Q] : ¬ (∀ x → ¬ P x) × ¬ (∀ x → ¬ Q x) → ¬ ¬ (∃ P × ∃ Q)
  ¬∀¬P×¬∀¬Q→¬¬[∃P×∃Q] = DN-undistrib-× ∘′ Prod.map ¬∀¬P→¬¬∃P ¬∀¬P→¬¬∃P

  ¬¬[∃P×∃Q]→¬∀¬P×¬∀¬Q : ¬ ¬ (∃ P × ∃ Q) → ¬ (∀ x → ¬ P x) × ¬ (∀ x → ¬ Q x)
  ¬¬[∃P×∃Q]→¬∀¬P×¬∀¬Q = Prod.map ¬¬∃P→¬∀¬P ¬¬∃P→¬∀¬P ∘′ DN-distrib-×

  [∀x→Px→Qx]→∀P→∀Q : (∀ x → P x → Q x) → (∀ x → P x) → ∀ x → Q x
  [∀x→Px→Qx]→∀P→∀Q f g x = f x (g x)


text:
module Sessions.Semantics.Commands where

open import Prelude
open import Data.Fin

open import Sessions.Syntax.Types
open import Sessions.Syntax.Values

mutual
  data Cmd : Pred RCtx 0ℓ where
    fork    :             ∀[ Comp unit ⇒ Cmd ]
    mkchan  : ∀ α       → ε[ Cmd ]
    send    : ∀ {a α}   → ∀[ (Endptr (a ! α) ✴ Val a) ⇒ Cmd ]
    receive : ∀ {a α}   → ∀[ Endptr (a ¿ α) ⇒ Cmd ]
    close   :             ∀[ Endptr end ⇒ Cmd ]

  δ : ∀ {Δ} → Cmd Δ → Pred RCtx 0ℓ
  δ (fork {α} _)        = Emp
  δ (mkchan α)          = Endptr α ✴ Endptr (α ⁻¹)
  δ (send {α = α} _)    = Endptr α
  δ (receive {a} {α} _) = Val a ✴ Endptr α
  δ (close _)           = Emp

  open import Relation.Ternary.Separation.Monad.Free Cmd δ renaming (Cont to Cont')
  open import Relation.Ternary.Separation.Monad.Error

  Comp : Type → Pred RCtx _
  Comp a = ErrorT Free (Val a)


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

module Relation.Nullary.Decidable.Properties where

open import Relation.Nullary.Decidable
open import Level
open import Relation.Nullary.Stable
open import Data.Empty
open import HLevels
open import Data.Empty.Properties using (isProp¬)
open import Data.Unit
open import Data.Empty

Dec→Stable : ∀ {ℓ} (A : Type ℓ) → Dec A → Stable A
Dec→Stable A (yes x) = λ _ → x
Dec→Stable A (no x) = λ f → ⊥-elim (f x)

isPropDec : (Aprop : isProp A) → isProp (Dec A)
isPropDec Aprop (yes a) (yes a') i = yes (Aprop a a' i)
isPropDec Aprop (yes a) (no ¬a) = ⊥-elim (¬a a)
isPropDec Aprop (no ¬a) (yes a) = ⊥-elim (¬a a)
isPropDec {A = A} Aprop (no ¬a) (no ¬a') i = no (isProp¬ A ¬a ¬a' i)

True : Dec A → Type
True (yes _) = ⊤
True (no  _) = ⊥

toWitness : {x : Dec A} → True x → A
toWitness {x = yes p} _ = p

open import Path
open import Data.Bool.Base

from-reflects : ∀ b → (d : Dec A) → Reflects A b → does d ≡ b
from-reflects false (no  y) r = refl
from-reflects false (yes y) r = ⊥-elim (r y)
from-reflects true  (no  y) r = ⊥-elim (y r)
from-reflects true  (yes y) r = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Semantics of syntactic traversal and substitution
module Semantics.Substitution.Traversal 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 CategoryTheory.Categories using (Category ; ext)
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans
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.OtherOps
open import TemporalOps.Linear
open import TemporalOps.StrongMonad

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

open ≡.≡-Reasoning
private module F-□ = Functor F-□
private module F-◇ = Functor F-◇
open Comonad W-□
open Monad M-◇
open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

module _ {𝒮} {k : Kit 𝒮} (⟦k⟧ : ⟦Kit⟧ k) where
    open ⟦Kit⟧ ⟦k⟧
    open Kit k
    open ⟦K⟧ ⟦k⟧
    open K k

    -- Soundness of syntactic traversal:
    -- Denotation of a term M traversed with substitution σ is
    -- the same as the denotation of σ followed by the denotation of M
    traverse-sound : ∀{Γ Δ A} (σ : Subst 𝒮 Γ Δ) (M : Γ ⊢ A)
                  -> ⟦ traverse σ M ⟧ₘ ≈ ⟦ M ⟧ₘ ∘ ⟦subst⟧ σ
    traverse′-sound : ∀{Γ Δ A} (σ : Subst 𝒮 Γ Δ) (C : Γ ⊨ A)
                  -> ⟦ traverse′ σ C ⟧ᵐ ≈ ⟦ C ⟧ᵐ ∘ ⟦subst⟧ σ

    traverse-sound ● (var ())
    traverse-sound (σ ▸ T) (var top) = ⟦𝓉⟧ T
    traverse-sound (σ ▸ T) (var (pop x)) = traverse-sound σ (var x)
    traverse-sound σ (lam {Γ} {A} M) {n} {⟦Δ⟧} = ext lemma
        where
        lemma : ∀(⟦A⟧ : ⟦ A ⟧ₜ n) →
                Λ ⟦ traverse (σ ↑ k) M ⟧ₘ n ⟦Δ⟧ ⟦A⟧ ≡ (Λ ⟦ M ⟧ₘ ∘ ⟦subst⟧ σ) n ⟦Δ⟧ ⟦A⟧
        lemma ⟦A⟧ rewrite traverse-sound (σ ↑ k) M {n} {⟦Δ⟧ , ⟦A⟧}
                        | ⟦↑⟧ (A now) σ {n} {⟦Δ⟧ , ⟦A⟧} = refl
    traverse-sound σ (M $ N) {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧}
                                             | traverse-sound σ N {n} {⟦Δ⟧} = refl
    traverse-sound σ unit = refl
    traverse-sound σ [ M ,, N ] {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧}
                                                | traverse-sound σ N {n} {⟦Δ⟧} = refl
    traverse-sound σ (fst M) {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧} = refl
    traverse-sound σ (snd M) {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧} = refl
    traverse-sound σ (inl M) {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧} = refl
    traverse-sound σ (inr M) {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧} = refl
    traverse-sound σ (case M inl↦ N₁ ||inr↦ N₂) {n} {⟦Δ⟧}
        rewrite traverse-sound σ M {n} {⟦Δ⟧} with ⟦ M ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)
    traverse-sound σ (case_inl↦_||inr↦_ {A = A} M N₁ N₂) {n} {⟦Δ⟧} | inj₁ ⟦A⟧
        rewrite traverse-sound (σ ↑ k) N₁ {n} {⟦Δ⟧ , ⟦A⟧}
              | ⟦↑⟧ (A now) σ {n} {⟦Δ⟧ , ⟦A⟧} = refl
    traverse-sound σ (case_inl↦_||inr↦_ {B = B} M N₁ N₂) {n} {⟦Δ⟧} | inj₂ ⟦B⟧
        rewrite traverse-sound (σ ↑ k) N₂ {n} {⟦Δ⟧ , ⟦B⟧}
              | ⟦↑⟧ (B now) σ {n} {⟦Δ⟧ , ⟦B⟧} = refl
    traverse-sound σ (sample M) {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧} = refl
    traverse-sound {Γ} {Δ} {A} σ (stable M) {n} {⟦Δ⟧} = ext lemma
        where
        lemma : ∀ l -> ⟦ traverse {Γ} σ (stable M) ⟧ₘ n ⟦Δ⟧ l
                     ≡ (⟦ stable {Γ} M ⟧ₘ ∘ ⟦subst⟧ σ) n ⟦Δ⟧ l
        lemma l rewrite traverse-sound (σ ↓ˢ k) M {l} {⟦ Δ ˢ⟧□ n ⟦Δ⟧ l}
                      | □-≡ n l (⟦↓ˢ⟧ σ {n} {⟦Δ⟧}) l = refl
    traverse-sound σ (sig M) {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧} = refl
    traverse-sound σ (letSig_In_ {A = A} M N) {n} {⟦Δ⟧}
        rewrite traverse-sound σ M {n} {⟦Δ⟧}
              | traverse-sound (σ ↑ k) N {n} {⟦Δ⟧ , ⟦ M ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)}
              | ⟦↑⟧ (A always) σ {n} {⟦Δ⟧ , (⟦ M ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧))} = refl
    traverse-sound σ (event E) = traverse′-sound σ E

    traverse′-sound σ (pure M) {n} {⟦Δ⟧} rewrite traverse-sound σ M {n} {⟦Δ⟧} = refl
    traverse′-sound σ (letSig_InC_ {A = A} S C) {n} {⟦Δ⟧}
                rewrite traverse-sound σ S {n} {⟦Δ⟧}
                      | traverse′-sound (σ ↑ k) C {n} {⟦Δ⟧ , ⟦ S ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)}
                      | ⟦↑⟧ (A always) σ {n} {⟦Δ⟧ , (⟦ S ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧))} = refl

    traverse′-sound {Γ} {Δ} σ (letEvt_In_ {A = A} {B} E C) {n} {⟦Δ⟧}
        rewrite traverse-sound σ E {n} {⟦Δ⟧}
              | (ext λ m → ext λ b → traverse′-sound (σ ↓ˢ k ↑ k) C {m} {b}) =
        begin
            μ.at ⟦ B ⟧ₜ n
                (F-◇.fmap (⟦ C ⟧ᵐ ∘ ⟦subst⟧ (_↑_ {A = A now} (σ ↓ˢ k) k) ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id) n
                         (st ⟦ Δ ˢ ⟧ₓ ⟦ A ⟧ₜ n (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧))))
        ≡⟨ cong (μ.at ⟦ B ⟧ₜ n) (F-◇.fmap-∘ {g = ⟦ C ⟧ᵐ} {⟦subst⟧ (_↑_ {A = A now} (σ ↓ˢ k) k) ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id}
                                         {n} {st ⟦ Δ ˢ ⟧ₓ ⟦ A ⟧ₜ n (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧))}) ⟩
            μ.at ⟦ B ⟧ₜ n (F-◇.fmap (⟦ C ⟧ᵐ) n
                (F-◇.fmap (⟦subst⟧ (_↑_ {A = A now} (σ ↓ˢ k) k) ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id) n
                     (st ⟦ Δ ˢ ⟧ₓ ⟦ A ⟧ₜ n (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)))))
        ≡⟨ cong (λ x → μ.at ⟦ B ⟧ₜ n (F-◇.fmap ⟦ C ⟧ᵐ n x)) (
            begin
                F-◇.fmap (⌞ ⟦subst⟧ (_↑_ {A = A now} (σ ↓ˢ k) k) ⌟ ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id) n
                     (st ⟦ Δ ˢ ⟧ₓ ⟦ A ⟧ₜ n (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)))
            ≡⟨ cong! (ext λ m -> ext λ b → ⟦↑⟧ (A now) (σ ↓ˢ k) {m} {b}) ⟩
                F-◇.fmap (⟦subst⟧ (σ ↓ˢ k) * id ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id) n
                     (st ⟦ Δ ˢ ⟧ₓ ⟦ A ⟧ₜ n (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)))
            ≡⟨ F-◇.fmap-∘ ⟩
                F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (F-◇.fmap (F-□.fmap (⟦subst⟧ (σ ↓ˢ k)) * id) n
                    (st ⟦ Δ ˢ ⟧ₓ ⟦ A ⟧ₜ n ( ⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧))))
            ≡⟨ cong (F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n)
                    (st-nat₁ (⟦subst⟧ (σ ↓ˢ k))) ⟩
                F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (st ⟦ Γ ˢ ⟧ₓ ⟦ A ⟧ₜ n ( ⌞ F-□.fmap (⟦subst⟧ (σ ↓ˢ k)) n (⟦ Δ ˢ⟧□ n ⟦Δ⟧) ⌟
                                   , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)))
            ≡⟨ cong! (⟦↓ˢ⟧ σ) ⟩
                F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                    (st ⟦ Γ ˢ ⟧ₓ ⟦ A ⟧ₜ n ( ⟦ Γ ˢ⟧□ n (⟦subst⟧ σ n ⟦Δ⟧)
                                       , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)))
            ∎
        ) ⟩
            μ.at ⟦ B ⟧ₜ n (F-◇.fmap ⟦ C ⟧ᵐ n
                (F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (st ⟦ Γ ˢ ⟧ₓ ⟦ A ⟧ₜ n ( ⟦ Γ ˢ⟧□ n (⟦subst⟧ σ n ⟦Δ⟧)
                                   , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧)))))
        ≡⟨ cong (μ.at ⟦ B ⟧ₜ n) (sym (F-◇.fmap-∘ {g = ⟦ C ⟧ᵐ}{ε.at ⟦ Γ ˢ ⟧ₓ * id}{n}
                            {st ⟦ Γ ˢ ⟧ₓ ⟦ A ⟧ₜ n ( ⟦ Γ ˢ⟧□ n (⟦subst⟧ σ n ⟦Δ⟧)
                                               , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧))})) ⟩
            μ.at ⟦ B ⟧ₜ n (F-◇.fmap (⟦ C ⟧ᵐ ∘ ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (st ⟦ Γ ˢ ⟧ₓ ⟦ A ⟧ₜ n ( ⟦ Γ ˢ⟧□ n (⟦subst⟧ σ n ⟦Δ⟧)
                                   , ⟦ E ⟧ₘ n (⟦subst⟧ σ n ⟦Δ⟧))))
        ≡⟨⟩
            ⟦ letEvt E In C ⟧ᵐ n (⟦subst⟧ σ n ⟦Δ⟧)
        ∎

    traverse′-sound {_} {Δ} σ (select_↦_||_↦_||both↦_ {Γ} {A} {B} {C} E₁ C₁ E₂ C₂ C₃) {n} {⟦Δ⟧}
        rewrite traverse-sound σ E₁ {n} {⟦Δ⟧}
              | traverse-sound σ E₂ {n} {⟦Δ⟧} =
        begin
            μ.at ⟦ C ⟧ₜ n
                (F-◇.fmap (⌞ handle ⟦ traverse′ (σ ↓ˢ k ↑ k ↑ k) C₁ ⟧ᵐ
                                    ⟦ traverse′ (σ ↓ˢ k ↑ k ↑ k) C₂ ⟧ᵐ
                                    ⟦ traverse′ (σ ↓ˢ k ↑ k ↑ k) C₃ ⟧ᵐ ⌟ ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id) n
                (st ⟦ Δ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟪ ⟦ E₁ ⟧ₘ ∘ ⟦subst⟧ σ , ⟦ E₂ ⟧ₘ ∘ ⟦subst⟧ σ ⟫ n ⟦Δ⟧)))
        ≡⟨ cong! (ext λ m → ext λ b → ind-hyp m b) ⟩
            μ.at ⟦ C ⟧ₜ n
                (F-◇.fmap (⌞ handle
                       (⟦ C₁ ⟧ᵐ ∘ (⟦subst⟧ (_↑_ {Event B now} (_↑_ {A now} (σ ↓ˢ k) k) k)))
                       (⟦ C₂ ⟧ᵐ ∘ (⟦subst⟧ (_↑_ {B now} (_↑_ {Event A now} (σ ↓ˢ k) k) k)))
                       (⟦ C₃ ⟧ᵐ ∘ (⟦subst⟧ (_↑_ {B now} (_↑_ {A now}       (σ ↓ˢ k) k) k))) ⌟
                       ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id) n
                (st ⟦ Δ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟪ ⟦ E₁ ⟧ₘ ∘ ⟦subst⟧ σ , ⟦ E₂ ⟧ₘ ∘ ⟦subst⟧ σ ⟫ n ⟦Δ⟧)))
        ≡⟨ cong! (ext λ m → ext λ b →
            ⟦subst⟧-handle {Δ}{Γ}{A}{B}{C} σ {⟦ C₁ ⟧ᵐ}{⟦ C₂ ⟧ᵐ}{⟦ C₃ ⟧ᵐ}{n = m} {b}) ⟩
            μ.at ⟦ C ⟧ₜ n
                (F-◇.fmap (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ ∘ ⟦subst⟧ (σ ↓ˢ k) * id ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id) n
                (st ⟦ Δ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟪ ⟦ E₁ ⟧ₘ ∘ ⟦subst⟧ σ , ⟦ E₂ ⟧ₘ ∘ ⟦subst⟧ σ ⟫ n ⟦Δ⟧)))
        ≡⟨ cong (μ.at ⟦ C ⟧ₜ n) (F-◇.fmap-∘ {g = handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ}
                      {f = ⟦subst⟧ (σ ↓ˢ k) * id ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id} {n}
                      {st ⟦ Δ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                      (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟪ ⟦ E₁ ⟧ₘ ∘ ⟦subst⟧ σ , ⟦ E₂ ⟧ₘ ∘ ⟦subst⟧ σ ⟫ n ⟦Δ⟧)})
         ⟩
            μ.at ⟦ C ⟧ₜ n (F-◇.fmap (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ) n
              ⌞ (F-◇.fmap (⟦subst⟧ (σ ↓ˢ k) * id ∘ ε.at ⟦ Δ ˢ ⟧ₓ * id) n
                (st ⟦ Δ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟪ ⟦ E₁ ⟧ₘ ∘ ⟦subst⟧ σ , ⟦ E₂ ⟧ₘ ∘ ⟦subst⟧ σ ⟫ n ⟦Δ⟧))) ⌟)
        ≡⟨ cong (λ x → μ.at ⟦ C ⟧ₜ n (F-◇.fmap (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ) n x)) (
            begin
                F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id ∘ F-□.fmap (⟦subst⟧ (σ ↓ˢ k)) * id) n
                (st ⟦ Δ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟪ ⟦ E₁ ⟧ₘ ∘ ⟦subst⟧ σ , ⟦ E₂ ⟧ₘ ∘ ⟦subst⟧ σ ⟫ n ⟦Δ⟧))
            ≡⟨ F-◇.fmap-∘ ⟩
                F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (F-◇.fmap (F-□.fmap (⟦subst⟧ (σ ↓ˢ k)) * id) n
                (st ⟦ Δ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Δ ˢ⟧□ n ⟦Δ⟧ , ⟪ ⟦ E₁ ⟧ₘ ∘ ⟦subst⟧ σ , ⟦ E₂ ⟧ₘ ∘ ⟦subst⟧ σ ⟫ n ⟦Δ⟧)))
            ≡⟨ cong (F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n)
                    (st-nat₁ (⟦subst⟧ (σ ↓ˢ k))) ⟩
                F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (st ⟦ Γ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⌞ F-□.fmap (⟦subst⟧ (σ ↓ˢ k)) n (⟦ Δ ˢ⟧□ n ⟦Δ⟧) ⌟ , ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫  n (⟦subst⟧ σ n ⟦Δ⟧)))
            ≡⟨ cong! (⟦↓ˢ⟧ σ) ⟩
                F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (st ⟦ Γ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Γ ˢ⟧□  n (⟦subst⟧ σ n ⟦Δ⟧) , ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫  n (⟦subst⟧ σ n ⟦Δ⟧)))
            ∎
        ) ⟩
            μ.at ⟦ C ⟧ₜ n (F-◇.fmap (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ) n
                (F-◇.fmap (ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (st ⟦ Γ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Γ ˢ⟧□  n (⟦subst⟧ σ n ⟦Δ⟧) , ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫  n (⟦subst⟧ σ n ⟦Δ⟧)))))
        ≡⟨ cong (μ.at ⟦ C ⟧ₜ n) (sym (F-◇.fmap-∘ {g = handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ}
            {ε.at ⟦ Γ ˢ ⟧ₓ * id}{n} {st ⟦ Γ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Γ ˢ⟧□  n (⟦subst⟧ σ n ⟦Δ⟧) , ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫  n (⟦subst⟧ σ n ⟦Δ⟧))})) ⟩
            μ.at ⟦ C ⟧ₜ n (F-◇.fmap (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ ∘ ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (st ⟦ Γ ˢ ⟧ₓ (⟦ A ⟧ₜ ⊛ ⟦ B ⟧ₜ) n
                (⟦ Γ ˢ⟧□  n (⟦subst⟧ σ n ⟦Δ⟧) , ⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫  n (⟦subst⟧ σ n ⟦Δ⟧))))
        ≡⟨⟩
            ⟦ select E₁ ↦ C₁ || E₂ ↦ C₂ ||both↦ C₃ ⟧ᵐ n (⟦subst⟧ σ n ⟦Δ⟧)
        ∎
        where
        ind-hyp : ∀ l c
            -> handle
                    ⟦ traverse′ (σ ↓ˢ k ↑ k ↑ k) C₁ ⟧ᵐ
                    ⟦ traverse′ (σ ↓ˢ k ↑ k ↑ k) C₂ ⟧ᵐ
                    ⟦ traverse′ (σ ↓ˢ k ↑ k ↑ k) C₃ ⟧ᵐ l c
             ≡ handle
                    (⟦ C₁ ⟧ᵐ ∘ (⟦subst⟧ (_↑_ {Event B now} (_↑_ {A now} (σ ↓ˢ k) k) k)))
                    (⟦ C₂ ⟧ᵐ ∘ (⟦subst⟧ (_↑_ {B now} (_↑_ {Event A now} (σ ↓ˢ k) k) k)))
                    (⟦ C₃ ⟧ᵐ ∘ (⟦subst⟧ (_↑_ {B now} (_↑_ {A now}       (σ ↓ˢ k) k) k))) l c
        ind-hyp l c rewrite ext (λ n -> (ext λ ⟦Δ⟧ -> (traverse′-sound (σ ↓ˢ k ↑ k ↑ k) C₁ {n} {⟦Δ⟧})))
                          | ext (λ n -> (ext λ ⟦Δ⟧ -> (traverse′-sound (σ ↓ˢ k ↑ k ↑ k) C₂ {n} {⟦Δ⟧})))
                          | ext (λ n -> (ext λ ⟦Δ⟧ -> (traverse′-sound (σ ↓ˢ k ↑ k ↑ k) C₃ {n} {⟦Δ⟧}))) = refl

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
--
-- Endomorphisms on a Set
------------------------------------------------------------------------

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

module Function.Endomorphism.Propositional {a} (A : Set a) where

open import Algebra using (Magma; Semigroup; Monoid)
open import Algebra.FunctionProperties.Core using (Op₂)
open import Algebra.Morphism; open Definitions
open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)

open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
open import Data.Product using (_,_)

open import Function
open import Function.Equality using (_⟨$⟩_)
open import Relation.Binary using (_Preserves_⟶_)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

import Function.Endomorphism.Setoid (P.setoid A) as Setoid

Endo : Set a
Endo = A → A

------------------------------------------------------------------------
-- Conversion back and forth with the Setoid-based notion of Endomorphism

fromSetoidEndo : Setoid.Endo → Endo
fromSetoidEndo = _⟨$⟩_

toSetoidEndo : Endo → Setoid.Endo
toSetoidEndo f = record
  { _⟨$⟩_ = f
  ; cong  = P.cong f
  }

------------------------------------------------------------------------
-- N-th composition

_^_ : Endo → ℕ → Endo
f ^ zero  = id
f ^ suc n = f ∘′ (f ^ n)

^-homo : ∀ f → Homomorphic₂ ℕ Endo _≡_ (f ^_) _+_ _∘′_
^-homo f zero    n = refl
^-homo f (suc m) n = P.cong (f ∘′_) (^-homo f m n)

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

∘-isMagma : IsMagma _≡_ (Op₂ Endo ∋ _∘′_)
∘-isMagma = record
  { isEquivalence = P.isEquivalence
  ; ∙-cong        = P.cong₂ _∘′_
  }

∘-magma : Magma _ _
∘-magma = record { isMagma = ∘-isMagma }

∘-isSemigroup : IsSemigroup _≡_ (Op₂ Endo ∋ _∘′_)
∘-isSemigroup = record
  { isMagma = ∘-isMagma
  ; assoc   = λ _ _ _ → refl
  }

∘-semigroup : Semigroup _ _
∘-semigroup = record { isSemigroup = ∘-isSemigroup }

∘-id-isMonoid : IsMonoid _≡_ _∘′_ id
∘-id-isMonoid = record
  { isSemigroup = ∘-isSemigroup
  ; identity    = (λ _ → refl) , (λ _ → refl)
  }

∘-id-monoid : Monoid _ _
∘-id-monoid = record { isMonoid = ∘-id-isMonoid }

------------------------------------------------------------------------
-- Homomorphism

^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_)
^-isSemigroupMorphism f = record
  { ⟦⟧-cong = P.cong (f ^_)
  ; ∙-homo  = ^-homo f
  }

^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_)
^-isMonoidMorphism f = record
  { sm-homo = ^-isSemigroupMorphism f
  ; ε-homo  = refl
  }


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

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

open import Size

open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.List using ([]; _∷_; _∷ʳ_; _++_)

open import Codata.Thunk

open import Relation.Nullary
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Unary using (_∈_; _⊆_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)

open import Function.Base using (case_of_)

open import Common

module Subtyping {ℙ : Set} (message : Message ℙ)
  where

open Message message

open import Trace message
open import SessionType message
open import Transitions message
open import Session message
open import Compliance message
open import HasTrace message

data Sub : SessionType -> SessionType -> Size -> Set where
  nil<:any : ∀{T i} -> Sub nil T i
  end<:def : ∀{T S i} (e : End T) (def : Defined S) -> Sub T S i
  inp<:inp : ∀{f g i}                 (inc : dom f ⊆ dom g) (F : (x : ℙ) -> Thunk (Sub (f x .force) (g x .force)) i) -> Sub (inp f) (inp g) i
  out<:out : ∀{f g i} (W : Witness g) (inc : dom g ⊆ dom f) (F : ∀{x} (!x : x ∈ dom g) -> Thunk (Sub (f x .force) (g x .force)) i) -> Sub (out f) (out g) i

_<:_ : SessionType -> SessionType -> Set
_<:_ T S = Sub T S ∞

sub-defined : ∀{T S} -> T <: S -> Defined T -> Defined S
sub-defined (end<:def _ def) _ = def
sub-defined (inp<:inp _ _) _   = inp
sub-defined (out<:out _ _ _) _ = out

sub-sound : ∀{T S R} -> Compliance (R # T) -> T <: S -> ∞Compliance (R # S)
force (sub-sound (win#def w def) sub) = win#def w (sub-defined sub def)
force (sub-sound (out#inp (_ , !x) F) (end<:def (inp U) def)) with U _ (proj₂ (compliance->defined (F !x .force)))
... | ()
force (sub-sound (out#inp (_ , !x) F) (inp<:inp _ G)) =
  out#inp (_ , !x) λ !x -> sub-sound (F !x .force) (G _ .force)
force (sub-sound (inp#out (_ , !x) F) (end<:def (out U) def)) = ⊥-elim (U _ !x)
force (sub-sound (inp#out (_ , !x) F) (out<:out {f} {g} (_ , !y) inc G)) =
  inp#out (_ , !y) λ !x -> sub-sound (F (inc !x) .force) (G !x .force)

SubtypingQ : SessionType -> SessionType -> Set
SubtypingQ T S = ∀{R} -> Compliance (R # T) -> Compliance (R # S)

if-eq : ℙ -> SessionType -> SessionType -> Continuation
force (if-eq x T S y) with x ?= y
... | yes _ = T
... | no _  = S

input* : SessionType
input* = inp λ _ -> λ where .force -> win

input : ℙ -> SessionType -> SessionType -> SessionType
input x T S = inp (if-eq x T S)

input*-but : ℙ -> SessionType
input*-but x = input x nil win

output : ℙ -> SessionType -> SessionType -> SessionType
output x T S = out (if-eq x T S)

input-if-eq-comp :
  ∀{f x T} ->
  Compliance (T # f x .force) ->
  ∀{y} (!y : y ∈ dom f) ->
  ∞Compliance (if-eq x T win y .force # f y .force)
force (input-if-eq-comp {_} {x} comp {y} !y) with x ?= y
... | yes refl = comp
... | no neq = win#def Win-win !y

output-if-eq-comp :
  ∀{f : Continuation}{x}{T} ->
  Compliance (T # f x .force) ->
  ∀{y} (!y : y ∈ dom (if-eq x T nil)) ->
  ∞Compliance (if-eq x T nil y .force # f y .force)
force (output-if-eq-comp {_} {x} comp {y} !y) with x ?= y
... | yes refl = comp
force (output-if-eq-comp {_} {x} comp {y} ()) | no neq

input*-comp : ∀{f} (W : Witness f) -> Compliance (input* # out f)
input*-comp W = inp#out W λ !x -> λ where .force -> win#def Win-win !x

input*-but-comp :
  ∀{f x}
  (W : Witness f)
  (N : ¬ x ∈ dom f) ->
  Compliance (input*-but x # out f)
input*-but-comp {f} {x} W N = inp#out W aux
  where
    aux : ∀{y : ℙ} -> (fy : y ∈ dom f) -> ∞Compliance (if-eq x nil win y .force # f y .force)
    force (aux {y} fy) with x ?= y
    ... | yes refl = ⊥-elim (N fy)
    ... | no neq = win#def Win-win fy

∈-output-if-eq : ∀{R} (x : ℙ) -> Defined R -> x ∈ dom (if-eq x R nil)
∈-output-if-eq x def with x ?= x
... | yes refl = def
... | no neq = ⊥-elim (neq refl)

input-comp : ∀{g x R} -> Compliance (R # g x .force) -> Compliance (input x R win # out g)
input-comp {g} {x} comp = inp#out (x , proj₂ (compliance->defined comp)) (input-if-eq-comp {g} comp)

output-comp : ∀{f x R} -> Compliance (R # f x .force) -> Compliance (output x R nil # inp f)
output-comp {f} {x} comp = out#inp (_ , ∈-output-if-eq x (proj₁ (compliance->defined comp))) (output-if-eq-comp {f} comp)

sub-inp-inp :
  ∀{f g}
  (spec : SubtypingQ (inp f) (inp g))
  (x : ℙ) ->
  SubtypingQ (f x .force) (g x .force)
sub-inp-inp spec x comp with spec (output-comp comp)
... | win#def (out U) def = ⊥-elim (U _ (∈-output-if-eq x (proj₁ (compliance->defined comp))))
... | out#inp (y , fy) F with F fy .force
... | comp' with x ?= y
... | yes refl = comp'
sub-inp-inp spec x comp | out#inp (y , fy) F | win#def () def | no neq

sub-out-out :
  ∀{f g}
  (spec : SubtypingQ (out f) (out g)) ->
  ∀{x} -> x ∈ dom g ->
  SubtypingQ (f x .force) (g x .force)
sub-out-out spec {x} gx comp with spec (input-comp comp)
... | inp#out W F with F gx .force
... | comp' with x ?= x
... | yes refl = comp'
... | no neq = ⊥-elim (neq refl)

sub-out->def :
  ∀{f g}
  (spec : SubtypingQ (out f) (out g))
  (Wf : Witness f) ->
  ∀{x} (gx : x ∈ dom g) ->
  x ∈ dom f
sub-out->def {f} spec Wf {x} gx with x ∈? f
... | yes fx = fx
... | no nfx with spec (input*-but-comp Wf nfx)
... | inp#out W F with F gx .force
... | res with x ?= x
sub-out->def {f} spec Wf {x} gx | no nfx | inp#out W F | win#def () def | yes refl
... | no neq = ⊥-elim (neq refl)

sub-inp->def : ∀{f g} (spec : SubtypingQ (inp f) (inp g)) -> ∀{x} (fx : x ∈ dom f) -> x ∈ dom g
sub-inp->def {f} spec {x} fx with spec {output x win nil} (output-comp (win#def Win-win fx))
... | win#def (out U) def = ⊥-elim (U _ (∈-output-if-eq x out))
... | out#inp W F with F (∈-output-if-eq x out) .force
... | comp = proj₂ (compliance->defined comp)

sub-complete : ∀{T S i} -> SubtypingQ T S -> Thunk (Sub T S) i
force (sub-complete {nil} {_} spec) = nil<:any
force (sub-complete {inp f} {nil} spec) with spec {win} (win#def Win-win inp)
... | win#def _ ()
force (sub-complete {inp _} {inp _} spec) = inp<:inp (sub-inp->def spec) λ x -> sub-complete (sub-inp-inp spec x)
force (sub-complete {inp f} {out _} spec) with Empty? f
... | inj₁ U = end<:def (inp U) out
... | inj₂ (x , ?x) with spec {output x win nil} (output-comp (win#def Win-win ?x))
... | win#def (out U) def = ⊥-elim (U x (∈-output-if-eq x out))
force (sub-complete {out f} {nil} spec) with spec {win} (win#def Win-win out)
... | win#def _ ()
force (sub-complete {out f} {inp _} spec) with Empty? f
... | inj₁ U = end<:def (out U) inp
... | inj₂ W with spec {input*} (input*-comp W)
... | win#def () _
force (sub-complete {out f} {out g} spec) with Empty? f
... | inj₁ Uf = end<:def (out Uf) out
... | inj₂ Wf with Empty? g
... | inj₂ Wg = out<:out Wg (sub-out->def spec Wf) λ !x -> sub-complete (sub-out-out spec !x)
... | inj₁ Ug with spec {input*} (input*-comp Wf)
... | inp#out (_ , !x) F = ⊥-elim (Ug _ !x)

SubtypingQ->SubtypingS : ∀{T S} -> SubtypingQ T S -> SubtypingS T S
SubtypingQ->SubtypingS spec comp = compliance-sound (spec (compliance-complete comp .force))

SubtypingS->SubtypingQ : ∀{T S} -> SubtypingS T S -> SubtypingQ T S
SubtypingS->SubtypingQ spec comp = compliance-complete (spec (compliance-sound comp)) .force

sub-excluded :
  ∀{T S φ}
  (sub : T <: S)
  (tφ  : T HasTrace φ)
  (nsφ : ¬ S HasTrace φ) ->
  ∃[ ψ ] ∃[ x ]
  (ψ ⊑ φ × T HasTrace ψ × S HasTrace ψ × T HasTrace (ψ ∷ʳ O x) × ¬ S HasTrace (ψ ∷ʳ O x))
sub-excluded nil<:any tφ nsφ = ⊥-elim (nil-has-no-trace tφ)
sub-excluded (end<:def e def) tφ nsφ with end-has-empty-trace e tφ
... | eq rewrite eq = ⊥-elim (nsφ (_ , def , refl))
sub-excluded (inp<:inp inc F) (_ , tdef , refl) nsφ =
  ⊥-elim (nsφ (_ , inp , refl))
sub-excluded (inp<:inp {f} {g} inc F) (_ , tdef , step inp tr) nsφ =
  let ψ , x , pre , tψ , sψ , tψx , nψx = sub-excluded (F _ .force) (_ , tdef , tr) (contraposition inp-has-trace nsφ) in
  _ , _ , some pre , inp-has-trace tψ , inp-has-trace sψ , inp-has-trace tψx , inp-has-no-trace nψx
sub-excluded (out<:out W inc F) (_ , tdef , refl) nsφ =
  ⊥-elim (nsφ (_ , out , refl))
sub-excluded (out<:out {f} {g} W inc F) (_ , tdef , step (out {_} {x} fx) tr) nsφ with x ∈? g
... | yes gx =
  let ψ , x , pre , tψ , sψ , tψx , nψx = sub-excluded (F gx .force) (_ , tdef , tr) (contraposition out-has-trace nsφ) in
  _ , _ , some pre , out-has-trace tψ , out-has-trace sψ , out-has-trace tψx , out-has-no-trace nψx
... | no ngx =
  [] , _ , none , (_ , out , refl) , (_ , out , refl) , (_ , fx , step (out fx) refl) , λ { (_ , _ , step (out gx) _) → ⊥-elim (ngx gx) }

sub-after : ∀{T S φ} (tφ : T HasTrace φ) (sφ : S HasTrace φ) -> T <: S -> after tφ <: after sφ
sub-after (_ , _ , refl) (_ , _ , refl) sub = sub
sub-after tφ@(_ , _ , step inp _) (_ , _ , step inp _) (end<:def e _) with end-has-empty-trace e tφ
... | ()
sub-after (_ , tdef , step inp tr) (_ , sdef , step inp sr) (inp<:inp _ F) =
  sub-after (_ , tdef , tr) (_ , sdef , sr) (F _ .force)
sub-after tφ@(_ , _ , step (out _) _) (_ , _ , step (out _) _) (end<:def e _) with end-has-empty-trace e tφ
... | ()
sub-after (_ , tdef , step (out _) tr) (_ , sdef , step (out gx) sr) (out<:out _ _ F) =
  sub-after (_ , tdef , tr) (_ , sdef , sr) (F gx .force)

sub-simulation :
  ∀{R R' T S S' φ}
  (comp : Compliance (R # T))
  (sub  : T <: S)
  (rr   : Transitions R (co-trace φ) R')
  (sr   : Transitions S φ S') ->
  ∃[ T' ] (Transitions T φ T' × T' <: S')
sub-simulation comp sub refl refl = _ , refl , sub
sub-simulation (win#def (out U) def) sub (step (out hx) rr) (step inp sr) = ⊥-elim (U _ hx)
sub-simulation (out#inp W F) (end<:def (inp U) def) (step (out hx) rr) (step inp sr) with F hx .force
... | comp = ⊥-elim (U _ (proj₂ (compliance->defined comp)))
sub-simulation (out#inp W F) (inp<:inp inc G) (step (out hx) rr) (step inp sr) =
  let _ , tr , sub = sub-simulation (F hx .force) (G _ . force) rr sr in
  _ , step inp tr , sub
sub-simulation (inp#out {h} {f} (_ , fx) F) (end<:def (out U) def) (step inp rr) (step (out gx) sr) with F fx .force
... | comp = ⊥-elim (U _ (proj₂ (compliance->defined comp)))
sub-simulation (inp#out W F) (out<:out W₁ inc G) (step inp rr) (step (out fx) sr) =
  let _ , tr , sub = sub-simulation (F (inc fx) .force) (G fx .force) rr sr in
  _ , step (out (inc fx)) tr , sub

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
open import Agda.Primitive using (_⊔_; lsuc)

open import Categories.Category
open import Categories.Functor
import Categories.Category.Cartesian as Cartesian
open import Categories.Monad.Relative

import SecondOrder.RelativeKleisli
open import SecondOrder.RelativeMonadMorphism

-- The category of relative monads and relative monad morphisms

module SecondOrder.RelMon
  {o l e o' l' e'}
  {𝒞 : Category o l e}
  {𝒟 : Category o' l' e'}
  {J : Functor 𝒞 𝒟}
  where

RelMon : Category (o ⊔ o' ⊔ l' ⊔ e') (lsuc o ⊔ lsuc l' ⊔ lsuc e') (o ⊔ e')
RelMon =
  let open Category 𝒟 renaming (id to id_D; identityˡ to identˡ; identityʳ to identʳ; assoc to ass) in
  let open RMonadMorph in
  let open Monad in
  let open HomReasoning in
  record
    { Obj = Monad J
    ; _⇒_ = λ M N → RMonadMorph M N
    ; _≈_ = λ {M} {N} φ ψ → ∀ X → morph φ {X} ≈ morph ψ {X}
    ; id = λ {M} →
           record
           { morph = λ {X} → id_D {F₀ M X}
           ; law-unit = λ {X} → identˡ
           ; law-extend = λ {X} {Y} {f} →
                        begin
                          (id_D ∘ extend M f) ≈⟨ identˡ ⟩
                          extend M f ≈⟨ extend-≈ M {k = f} {h = id_D ∘ f} (⟺ identˡ) ⟩
                          extend M (id_D ∘ f) ≈⟨ ⟺ identʳ ⟩
                          (extend M (id_D ∘ f) ∘ id_D)
                        ∎
           }
    ; _∘_ = λ {M} {N} {L} φ ψ →
          record
          { morph = λ {X} → (morph φ {X}) ∘ (morph ψ {X})
          ; law-unit = λ {X} →
                     begin
                       ((morph φ ∘ morph ψ) ∘ unit M) ≈⟨ ass ⟩
                       (morph φ ∘ (morph ψ ∘ unit M)) ≈⟨ refl⟩∘⟨ law-unit ψ ⟩
                       (morph φ ∘ unit N) ≈⟨ law-unit φ ⟩
                       unit L
                     ∎
          ; law-extend = λ {X} {Y} {f} →
                       begin
                         (morph φ ∘ morph ψ) ∘ extend M f ≈⟨ ass ⟩
                         morph φ ∘ (morph ψ ∘ extend M f) ≈⟨ refl⟩∘⟨ law-extend ψ ⟩
                         morph φ ∘ (extend N (morph ψ ∘ f) ∘ morph ψ) ≈⟨ ⟺ (ass) ⟩
                         (morph φ ∘ extend N (morph ψ ∘ f)) ∘ morph ψ ≈⟨ (law-extend φ  ⟩∘⟨refl) ⟩
                         ((extend L (morph φ ∘ morph ψ ∘ f)) ∘ morph φ) ∘ morph ψ ≈⟨ ass ⟩
                         (extend L (morph φ ∘ morph ψ ∘ f)) ∘ morph φ ∘ morph ψ
                                 ≈⟨ ( extend-≈ L (⟺ (ass)) ⟩∘⟨refl) ⟩
                         extend L ((morph φ ∘ morph ψ) ∘ f) ∘ morph φ ∘ morph ψ
                       ∎
          }
    ; assoc = λ X  → ass
    ; sym-assoc = λ X → ⟺ (ass)
    ; identityˡ = λ X → identˡ
    ; identityʳ = λ X → identʳ
    ; identity² = λ X → identˡ
    ; equiv = record
              { refl = λ X → Equiv.refl
              ; sym = λ φ≈ψ X → ⟺ (φ≈ψ X)
              ; trans = λ φ≈ψ ψ≈θ X → φ≈ψ X ○ ψ≈θ X
              }
    ; ∘-resp-≈ = λ φ≈ψ θ≈ω X → φ≈ψ X ⟩∘⟨ θ≈ω X
    }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module Sets.ImageSet where

open import Data
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
open import Structure.Function
open import Structure.Setoid renaming (_≡_ to _≡ₛ_)
open import Type
open import Type.Dependent

private variable ℓ ℓₑ ℓᵢ ℓᵢ₁ ℓᵢ₂ ℓᵢ₃ ℓᵢₑ ℓ₁ ℓ₂ ℓ₃ : Lvl.Level
private variable T X Y Z : Type{ℓ}

record ImageSet {ℓᵢ ℓ} (T : Type{ℓ}) : Type{Lvl.𝐒(ℓᵢ) Lvl.⊔ ℓ} where
  constructor intro
  field
    {Index} : Type{ℓᵢ}
    elem : Index → T
open ImageSet using (Index ; elem) public

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  _∈_ : T → ImageSet{ℓᵢ}(T) → Stmt
  a ∈ A = ∃(i ↦ a ≡ₛ elem A(i))

  open import Data.Proofs
  open import Function.Proofs
  open import Logic.Propositional.Theorems
  open import Structure.Relator
  open import Structure.Relator.Properties
  open import Syntax.Transitivity

  {-
  instance
    ImageSet-equiv : Equiv(ImageSet{ℓᵢ}(T))
    ImageSet-equiv = intro(_≡_) ⦃ [≡]-equivalence ⦄
  -}

  instance
    [∈]-unaryOperatorₗ : ∀{A : ImageSet{ℓᵢ}(T)} → UnaryRelator(_∈ A)
    UnaryRelator.substitution [∈]-unaryOperatorₗ xy ([∃]-intro i ⦃ p ⦄) = [∃]-intro i ⦃ symmetry(_≡ₛ_) xy 🝖 p ⦄


text:
module Issue878 where

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a

data ⊤ : Set where
  tt : ⊤

record args : Set₁ where
  field
    P : ⊤ → Set
    g : (b : ⊤) → P b

module _ (r : args) where
  open args r

  postulate
    ext : ∀ b → P b

module _ {r : args} where
  open args r

  postulate
    β-r : ∀ b → ext r b == g b

a : args
a = record {P = λ x → (⊤ → ⊤); g = λ x → λ c → tt}

err : ext a tt tt == tt
err = β-r tt
-- WAS: __IMPOSSIBLE__ in Conversion.hs


text:
------------------------------------------------------------------------
-- ω-continuous functions
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Partiality-monad.Inductive.Omega-continuous where

open import Equality.Propositional
open import Prelude

open import Bijection equality-with-J using (_↔_)

import Partiality-algebra.Omega-continuous as O
open import Partiality-monad.Inductive

-- Definition of ω-continuous functions.

[_⊥→_⊥] : ∀ {a b} → Type a → Type b → Type (a ⊔ b)
[ A ⊥→ B ⊥] = O.[ partiality-algebra A ⟶ partiality-algebra B ]

module [_⊥→_⊥] {a b} {A : Type a} {B : Type b} (f : [ A ⊥→ B ⊥]) =
  O.[_⟶_] f

open [_⊥→_⊥]

-- Identity.

idω : ∀ {a} {A : Type a} → [ A ⊥→ A ⊥]
idω = O.idω

-- Composition.

infixr 40 _∘ω_

_∘ω_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
       [ B ⊥→ C ⊥] → [ A ⊥→ B ⊥] → [ A ⊥→ C ⊥]
_∘ω_ = O._∘ω_

-- Equality characterisation lemma for ω-continuous functions.

equality-characterisation-continuous :
  ∀ {a b} {A : Type a} {B : Type b} {f g : [ A ⊥→ B ⊥]} →
  (∀ x → function f x ≡ function g x) ↔ f ≡ g
equality-characterisation-continuous =
  O.equality-characterisation-continuous

-- Composition is associative.

∘ω-assoc :
  ∀ {a b c d} {A : Type a} {B : Type b} {C : Type c} {D : Type d}
  (f : [ C ⊥→ D ⊥]) (g : [ B ⊥→ C ⊥]) (h : [ A ⊥→ B ⊥]) →
  f ∘ω (g ∘ω h) ≡ (f ∘ω g) ∘ω h
∘ω-assoc = O.∘ω-assoc

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the Data.(Nat/Fin).Induction
-- modules directly.
------------------------------------------------------------------------

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

module Induction.Nat where

open import Data.Nat.Induction public
open import Data.Fin.Induction public

{-# WARNING_ON_IMPORT
"Induction.Nat was deprecated in v1.1.
Use Data.Nat.Induction and Data.Fin.Induction instead."
#-}


text:
module SystemF.Syntax.Context where

open import Prelude
open import SystemF.Syntax.Type
open import Data.Vec

Ctx : ℕ → ℕ → Set
Ctx ν n = Vec (Type ν) n


text:
module #9 where

{-
  Define the type family Fin : N → U mentioned at the end of §1.3, and the dependent
  function fmax : ∏(n:N) Fin(n + 1) mentioned in §1.4.
-}

open import Data.Nat

data Fin : ℕ → Set where
  FZ : {n : ℕ} → Fin (suc n)
  FS : {n : ℕ} → Fin n → Fin (suc n)

fmax : (n : ℕ) → Fin (n + 1)
fmax zero = FZ
fmax (suc n) = FS (fmax n)

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
------------------------------------------------------------------------
-- An expression can be derived from at most one string
------------------------------------------------------------------------

open import Mixfix.Expr

module Mixfix.Cyclic.Uniqueness
         (i : PrecedenceGraphInterface)
         (g : PrecedenceGraphInterface.PrecedenceGraph i)
         where

open import Codata.Musical.Notation using (♭)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using (List; []; _∷_)
open import Data.List.Relation.Unary.Any using (here)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Product using (_,_; -,_; proj₂)
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open PrecedenceCorrect i g
open import TotalParserCombinators.Semantics hiding (_≅_)
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Cyclic.Lib as Lib
open Lib.Semantics
import Mixfix.Cyclic.Grammar
private module Grammar = Mixfix.Cyclic.Grammar i g

module Unique where

 data _≋_ {A : Set} {x₁ : A} {s₁ p₁} (∈ : x₁ ∈⟦ p₁ ⟧· s₁) :
          ∀ {x₂ : A} {s₂ p₂} → x₂ ∈⟦ p₂ ⟧· s₂ → Set where
   refl : ∈ ≋ ∈

 mutual

  precs : ∀ ps {s₁ s₂} {e₁ e₂ : Expr ps}
          (∈₁ : e₁ ∈⟦ Grammar.precs ps ⟧· s₁)
          (∈₂ : e₂ ∈⟦ Grammar.precs ps ⟧· s₂) →
          e₁ ≡ e₂ → ∈₁ ≋ ∈₂
  precs [] () () _
  precs (p ∷ ps) (∣ʳ (<$>_ {x = ( _ ∙  _)}  ∈₁))
                 (∣ʳ (<$>_ {x = (._ ∙ ._)}  ∈₂)) refl with precs ps ∈₁ ∈₂ refl
  precs (p ∷ ps) (∣ʳ (<$>_ {x = ( _ ∙  _)}  ∈₁))
                 (∣ʳ (<$>_ {x = (._ ∙ ._)} .∈₁)) refl | refl = refl
  precs (p ∷ ps) (∣ˡ (<$> ∈₁)) (∣ʳ (<$>_ {x = _ ∙ _} ∈₂)) ()
  precs (p ∷ ps) (∣ʳ (<$>_ {x = _ ∙ _} ∈₁)) (∣ˡ (<$> ∈₂)) ()
  precs (p ∷ ps) (∣ˡ (<$>_ {x = e₁} ∈₁)) (∣ˡ (<$>_ {x = e₂} ∈₂)) eq =
    helper (lemma₁ eq) (lemma₂ eq) ∈₁ ∈₂
    where
    lemma₁ : ∀ {assoc₁ assoc₂}
               {e₁ : ExprIn p assoc₁} {e₂ : ExprIn p assoc₂} →
             (Expr._∙_ (here {xs = ps} refl) e₁) ≡ (here refl ∙ e₂) →
             assoc₁ ≡ assoc₂
    lemma₁ refl = refl

    lemma₂ : ∀ {assoc₁ assoc₂}
               {e₁ : ExprIn p assoc₁} {e₂ : ExprIn p assoc₂} →
             (Expr._∙_ (here {xs = ps} refl) e₁) ≡ (here refl ∙ e₂) →
             e₁ ≅ e₂
    lemma₂ refl = refl

    helper : ∀ {assoc₁ assoc₂ s₁ s₂}
             {e₁ : ExprIn p assoc₁} {e₂ : ExprIn p assoc₂} →
             assoc₁ ≡ assoc₂ → e₁ ≅ e₂ →
             (∈₁ : (-, e₁) ∈⟦ Grammar.prec p ⟧· s₁) →
             (∈₂ : (-, e₂) ∈⟦ Grammar.prec p ⟧· s₂) →
             ∣ˡ {p₁ = (λ e → here refl ∙ proj₂ e) <$> Grammar.prec p}
                {p₂ = weakenE <$> Grammar.precs ps} (<$> ∈₁) ≋
             ∣ˡ {p₁ = (λ e → here refl ∙ proj₂ e) <$> Grammar.prec p}
                {p₂ = weakenE <$> Grammar.precs ps} (<$> ∈₂)
    helper refl refl ∈₁ ∈₂ with prec ∈₁ ∈₂
    helper refl refl ∈ .∈  | refl = refl

  prec : ∀ {p assoc s₁ s₂} {e : ExprIn p assoc}
         (∈₁ : (-, e) ∈⟦ Grammar.prec p ⟧· s₁)
         (∈₂ : (-, e) ∈⟦ Grammar.prec p ⟧· s₂) →
         ∈₁ ≋ ∈₂
  prec {p} ∈₁′ ∈₂′ = prec′ ∈₁′ ∈₂′ refl
    where
    module P = Grammar.Prec p

    preRight⁺ : ∀ {s₁ s₂} {e₁ e₂ : ExprIn p right}
                (∈₁ : e₁ ∈⟦ P.preRight⁺ ⟧· s₁)
                (∈₂ : e₂ ∈⟦ P.preRight⁺ ⟧· s₂) →
                e₁ ≡ e₂ → ∈₁ ≋ ∈₂
    preRight⁺ (∣ˡ (<$>  ∈₁)       ⊛∞ ∣ˡ (<$>  ∈₂))
              (∣ˡ (<$> ∈₁′)       ⊛∞ ∣ˡ (<$> ∈₂′)) refl with inner _   ∈₁ ∈₁′ refl | preRight⁺ ∈₂ ∈₂′ refl
    preRight⁺ (∣ˡ (<$>  ∈₁)       ⊛∞ ∣ˡ (<$>  ∈₂))
              (∣ˡ (<$> .∈₁)       ⊛∞ ∣ˡ (<$> .∈₂)) refl | refl | refl = refl
    preRight⁺ (∣ˡ (<$>  ∈₁)       ⊛∞ ∣ʳ (<$>  ∈₂))
              (∣ˡ (<$> ∈₁′)       ⊛∞ ∣ʳ (<$> ∈₂′)) refl with inner _ ∈₁ ∈₁′ refl | precs _ ∈₂ ∈₂′ refl
    preRight⁺ (∣ˡ (<$>  ∈₁)       ⊛∞ ∣ʳ (<$>  ∈₂))
              (∣ˡ (<$> .∈₁)       ⊛∞ ∣ʳ (<$> .∈₂)) refl | refl | refl = refl
    preRight⁺ (∣ʳ (<$>  ∈₁ ⊛  ∈₃) ⊛∞ ∣ˡ (<$>  ∈₂))
              (∣ʳ (<$> ∈₁′ ⊛ ∈₃′) ⊛∞ ∣ˡ (<$> ∈₂′)) refl with precs _   ∈₁ ∈₁′ refl | preRight⁺ ∈₂ ∈₂′ refl | inner _   ∈₃ ∈₃′ refl
    preRight⁺ (∣ʳ (<$>  ∈₁ ⊛  ∈₃) ⊛∞ ∣ˡ (<$>  ∈₂))
              (∣ʳ (<$> .∈₁ ⊛ .∈₃) ⊛∞ ∣ˡ (<$> .∈₂)) refl | refl | refl | refl = refl
    preRight⁺ (∣ʳ (<$>  ∈₁ ⊛  ∈₃) ⊛∞ ∣ʳ (<$>  ∈₂))
              (∣ʳ (<$> ∈₁′ ⊛ ∈₃′) ⊛∞ ∣ʳ (<$> ∈₂′)) refl with precs _ ∈₁ ∈₁′ refl | precs _ ∈₂ ∈₂′ refl | inner _ ∈₃ ∈₃′ refl
    preRight⁺ (∣ʳ (<$>  ∈₁ ⊛  ∈₃) ⊛∞ ∣ʳ (<$>  ∈₂))
              (∣ʳ (<$> .∈₁ ⊛ .∈₃) ⊛∞ ∣ʳ (<$> .∈₂)) refl | refl | refl | refl = refl

    preRight⁺ (∣ˡ (<$> _)     ⊛∞ _)
              (∣ʳ (<$> _ ⊛ _) ⊛∞ _)          ()
    preRight⁺ (∣ʳ (<$> _ ⊛ _) ⊛∞ _)
              (∣ˡ (<$> _)     ⊛∞ _)          ()
    preRight⁺ (∣ˡ (<$> _)     ⊛∞ ∣ˡ (<$> _))
              (∣ˡ (<$> _)     ⊛∞ ∣ʳ (<$> _)) ()
    preRight⁺ (∣ˡ (<$> _)     ⊛∞ ∣ʳ (<$> _))
              (∣ˡ (<$> _)     ⊛∞ ∣ˡ (<$> _)) ()
    preRight⁺ (∣ʳ (<$> _ ⊛ _) ⊛∞ ∣ˡ (<$> _))
              (∣ʳ (<$> _ ⊛ _) ⊛∞ ∣ʳ (<$> _)) ()
    preRight⁺ (∣ʳ (<$> _ ⊛ _) ⊛∞ ∣ʳ (<$> _))
              (∣ʳ (<$> _ ⊛ _) ⊛∞ ∣ˡ (<$> _)) ()

    postLeft⁺ : ∀ {s₁ s₂} {e₁ e₂ : ExprIn p left}
                (∈₁ : e₁ ∈⟦ P.postLeft⁺ ⟧· s₁)
                (∈₂ : e₂ ∈⟦ P.postLeft⁺ ⟧· s₂) →
                e₁ ≡ e₂ → ∈₁ ≋ ∈₂
    postLeft⁺ (<$> (∣ˡ (<$>  ∈₁)) ⊛∞ ∣ˡ (<$>  ∈₂))
              (<$> (∣ˡ (<$> ∈₁′)) ⊛∞ ∣ˡ (<$> ∈₂′))       refl with postLeft⁺ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl
    postLeft⁺ (<$> (∣ˡ (<$>  ∈₁)) ⊛∞ ∣ˡ (<$>  ∈₂))
              (<$> (∣ˡ (<$> .∈₁)) ⊛∞ ∣ˡ (<$> .∈₂))       refl | refl | refl = refl
    postLeft⁺ (<$> (∣ʳ (<$>  ∈₁)) ⊛∞ ∣ˡ (<$>  ∈₂))
              (<$> (∣ʳ (<$> ∈₁′)) ⊛∞ ∣ˡ (<$> ∈₂′))       refl with precs _ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl
    postLeft⁺ (<$> (∣ʳ (<$>  ∈₁)) ⊛∞ ∣ˡ (<$>  ∈₂))
              (<$> (∣ʳ (<$> .∈₁)) ⊛∞ ∣ˡ (<$> .∈₂))       refl | refl | refl = refl
    postLeft⁺ (<$> (∣ˡ (<$>  ∈₁)) ⊛∞ ∣ʳ (<$>  ∈₂ ⊛  ∈₃))
              (<$> (∣ˡ (<$> ∈₁′)) ⊛∞ ∣ʳ (<$> ∈₂′ ⊛ ∈₃′)) refl with postLeft⁺ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl | precs _ ∈₃ ∈₃′ refl
    postLeft⁺ (<$> (∣ˡ (<$>  ∈₁)) ⊛∞ ∣ʳ (<$>  ∈₂ ⊛  ∈₃))
              (<$> (∣ˡ (<$> .∈₁)) ⊛∞ ∣ʳ (<$> .∈₂ ⊛ .∈₃)) refl | refl | refl | refl = refl
    postLeft⁺ (<$> (∣ʳ (<$>  ∈₁)) ⊛∞ ∣ʳ (<$>  ∈₂ ⊛  ∈₃))
              (<$> (∣ʳ (<$> ∈₁′)) ⊛∞ ∣ʳ (<$> ∈₂′ ⊛ ∈₃′)) refl with precs _ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl | precs _ ∈₃ ∈₃′ refl
    postLeft⁺ (<$> (∣ʳ (<$>  ∈₁)) ⊛∞ ∣ʳ (<$>  ∈₂ ⊛  ∈₃))
              (<$> (∣ʳ (<$> .∈₁)) ⊛∞ ∣ʳ (<$> .∈₂ ⊛ .∈₃)) refl | refl | refl | refl = refl

    postLeft⁺ (<$> _            ⊛∞ ∣ˡ (<$> _))
              (<$> _            ⊛∞ ∣ʳ (<$> _ ⊛ _)) ()
    postLeft⁺ (<$> _            ⊛∞ ∣ʳ (<$> _ ⊛ _))
              (<$> _            ⊛∞ ∣ˡ (<$> _))     ()
    postLeft⁺ (<$> (∣ˡ (<$> _)) ⊛∞ ∣ˡ (<$> _))
              (<$> (∣ʳ (<$> _)) ⊛∞ ∣ˡ (<$> _))     ()
    postLeft⁺ (<$> (∣ʳ (<$> _)) ⊛∞ ∣ˡ (<$> _))
              (<$> (∣ˡ (<$> _)) ⊛∞ ∣ˡ (<$> _))     ()
    postLeft⁺ (<$> (∣ˡ (<$> _)) ⊛∞ ∣ʳ (<$> _ ⊛ _))
              (<$> (∣ʳ (<$> _)) ⊛∞ ∣ʳ (<$> _ ⊛ _)) ()
    postLeft⁺ (<$> (∣ʳ (<$> _)) ⊛∞ ∣ʳ (<$> _ ⊛ _))
              (<$> (∣ˡ (<$> _)) ⊛∞ ∣ʳ (<$> _ ⊛ _)) ()

    prec′ : ∀ {assoc s₁ s₂} {e₁ e₂ : ExprIn p assoc} →
            (∈₁ : (-, e₁) ∈⟦ Grammar.prec p ⟧· s₁)
            (∈₂ : (-, e₂) ∈⟦ Grammar.prec p ⟧· s₂) →
            e₁ ≡ e₂ → ∈₁ ≋ ∈₂
    prec′ (∥ˡ (<$> ∈₁)) (∥ˡ (<$>  ∈₂)) refl with inner _ ∈₁ ∈₂ refl
    prec′ (∥ˡ (<$> ∈₁)) (∥ˡ (<$> .∈₁)) refl | refl = refl

    prec′ (∥ʳ (∥ˡ (<$> ∈₁  ⊛ ∈₂  ⊛∞ ∈₃ )))
          (∥ʳ (∥ˡ (<$> ∈₁′ ⊛ ∈₂′ ⊛∞ ∈₃′))) refl
      with precs _ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl | precs _ ∈₃ ∈₃′ refl
    prec′ (∥ʳ (∥ˡ (<$>  ∈₁ ⊛  ∈₂ ⊛∞  ∈₃)))
          (∥ʳ (∥ˡ (<$> .∈₁ ⊛ .∈₂ ⊛∞ .∈₃))) refl | refl | refl | refl = refl

    prec′ (∥ʳ (∥ʳ (∥ˡ ∈₁))) (∥ʳ (∥ʳ (∥ˡ  ∈₂))) refl with preRight⁺ ∈₁ ∈₂ refl
    prec′ (∥ʳ (∥ʳ (∥ˡ ∈₁))) (∥ʳ (∥ʳ (∥ˡ .∈₁))) refl | refl = refl

    prec′ (∥ʳ (∥ʳ (∥ʳ (∥ˡ ∈₁)))) (∥ʳ (∥ʳ (∥ʳ (∥ˡ  ∈₂)))) refl with postLeft⁺ ∈₁ ∈₂ refl
    prec′ (∥ʳ (∥ʳ (∥ʳ (∥ˡ ∈₁)))) (∥ʳ (∥ʳ (∥ʳ (∥ˡ .∈₁)))) refl | refl = refl

    prec′ (∥ˡ (<$> _)) (∥ʳ (∥ˡ (<$> _ ⊛ _ ⊛∞ _))) ()
    prec′ (∥ʳ (∥ˡ (<$> _ ⊛ _ ⊛∞ _))) (∥ˡ (<$> _)) ()
    prec′ (∥ʳ (∥ʳ (∥ʳ (∥ʳ ())))) _ _
    prec′ _ (∥ʳ (∥ʳ (∥ʳ (∥ʳ ())))) _

  inner : ∀ {fix s₁ s₂} ops {e₁ e₂ : Inner {fix} ops}
          (∈₁ : e₁ ∈⟦ Grammar.inner ops ⟧· s₁)
          (∈₂ : e₂ ∈⟦ Grammar.inner ops ⟧· s₂) →
          e₁ ≡ e₂ → ∈₁ ≋ ∈₂
  inner [] () () _
  inner ((_ , op) ∷ ops) (∣ˡ (<$>  ∈₁))
                         (∣ˡ (<$>  ∈₂)) refl with inner′ _ _ ∈₁ ∈₂
  inner ((_ , op) ∷ ops) (∣ˡ (<$>  ∈₁))
                         (∣ˡ (<$> .∈₁)) refl | refl = refl
  inner ((_ , op) ∷ ops) (∣ʳ (<$>_ {x = ( _ ∙  _)}  ∈₁))
                         (∣ʳ (<$>_ {x = (._ ∙ ._)}  ∈₂)) refl with inner ops ∈₁ ∈₂ refl
  inner ((_ , op) ∷ ops) (∣ʳ (<$>_ {x = ( _ ∙  _)}  ∈₁))
                         (∣ʳ (<$>_ {x = (._ ∙ ._)} .∈₁)) refl | refl = refl
  inner ((_ , op) ∷ ops) (∣ˡ (<$> ∈₁)) (∣ʳ (<$>_ {x = (_ ∙ _)} ∈₂)) ()
  inner ((_ , op) ∷ ops) (∣ʳ (<$>_ {x = (_ ∙ _)} ∈₁)) (∣ˡ (<$> ∈₂)) ()

  inner′ : ∀ {arity s₁ s₂}
           (ns : Vec NamePart (1 + arity))
           (args : Vec (Expr anyPrecedence) arity)
           (∈₁ : args ∈⟦ Grammar.expr between ns ⟧· s₁)
           (∈₂ : args ∈⟦ Grammar.expr between ns ⟧· s₂) →
           ∈₁ ≋ ∈₂
  inner′ (n ∷ [])      []           between-[] between-[] = refl
  inner′ (n ∷ n′ ∷ ns) (arg ∷ args)
         (between-∷ ∈₁ ∈⋯₁) (between-∷ ∈₂ ∈⋯₂)
    with precs _ ∈₁ ∈₂ refl | inner′ (n′ ∷ ns) args ∈⋯₁ ∈⋯₂
  inner′ (n ∷ n′ ∷ ns) (arg ∷ args)
         (between-∷ ∈₁ ∈⋯₁) (between-∷ .∈₁ .∈⋯₁) | refl | refl = refl

-- There is at most one string representing a given expression.

unique : ∀ {e s₁ s₂} →
         e ∈ Grammar.expression · s₁ →
         e ∈ Grammar.expression · s₂ →
         s₁ ≡ s₂
unique ∈₁ ∈₂ with ∈₁′ | ∈₂′ | Unique.precs _ ∈₁′ ∈₂′ refl
  where
  ∈₁′ = Lib.Semantics.complete (♭ Grammar.expr) ∈₁
  ∈₂′ = Lib.Semantics.complete (♭ Grammar.expr) ∈₂
... | ∈ | .∈ | Unique.refl = refl

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Example where

open import Prelude
import Typed

data Data : Set where
  nat  : Data
  bool : Data

Datatype : Data -> List (List Data)
Datatype nat  = ε ◄ ε ◄ (ε ◄ nat)
Datatype bool = ε ◄ ε ◄ ε

data Effect : Set where

data _⊆_ : Effect -> Effect -> Set where
  refl⊆  : forall {M} -> M ⊆ M

Monad : Effect -> Set -> Set
Monad e A = A

return : forall {M A} -> A -> Monad M A
return x = x

map    : forall {M A B} -> (A -> B) -> Monad M A -> Monad M B
map f m = f m

join   : forall {M A} -> Monad M (Monad M A) -> Monad M A
join m = m

morph  : forall {M N} -> M ⊆ N -> (A : Set) -> Monad M A -> Monad N A
morph _ A x = x

open module TT =
       Typed Data Datatype
             Effect _⊆_
             Monad
             (\{M A} -> return {M}{A})
             (\{M A B} -> map {M}{A}{B})
             (\{M A} -> join {M}{A})
             morph

zero : forall {M Γ} -> InV M Γ (TyCon nat)
zero = con (tl hd) ⟨⟩

suc : forall {M Γ} -> InV M Γ (TyCon nat) -> InV M Γ (TyCon nat)
suc n = con hd (⟨⟩ ◃ n)

true : forall {M Γ} -> InV M Γ (TyCon bool)
true = con hd ⟨⟩

false : forall {M Γ} -> InV M Γ (TyCon bool)
false = con (tl hd) ⟨⟩


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

open import Categories.Category.Core

module Categories.Category.Construction.KaroubiEnvelope.Properties {o ℓ e} (𝒞 : Category o ℓ e) where

open import Data.Product using (_,_)

open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties

open import Categories.Category.Construction.KaroubiEnvelope

open import Categories.Morphism.Idempotent
import Categories.Morphism.Idempotent.Bundles as BundledIdem

open Category 𝒞
open Equiv

--------------------------------------------------------------------------------
-- Some facts about embedding 𝒞 into it's Karoubi Envelope

KaroubiEmbedding : Functor 𝒞 (KaroubiEnvelope 𝒞)
KaroubiEmbedding = record
  { F₀ = λ X → record
    { obj = X
    ; isIdempotent = record
      { idem = id
      ; idempotent = identity²
      }
    }
  ; F₁ = λ f → record
    { hom = f
    ; absorbˡ = identityˡ
    ; absorbʳ = identityʳ
    }
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = λ eq → eq
  }

private
  module KaroubiEmbedding = Functor KaroubiEmbedding

karoubi-embedding-full : Full KaroubiEmbedding
karoubi-embedding-full = record
  { from = record
    { _⟨$⟩_ = λ f → BundledIdem.Idempotent⇒.hom f
    ; cong = λ eq → eq
    }
  ; right-inverse-of = λ _ → refl
  }

karoubi-embedding-faithful : Faithful KaroubiEmbedding
karoubi-embedding-faithful f g eq = eq

karoubi-embedding-fully-faithful : FullyFaithful KaroubiEmbedding
karoubi-embedding-fully-faithful = karoubi-embedding-full , karoubi-embedding-faithful

--------------------------------------------------------------------------------
-- Some facts about splitting idempotents

-- All idempotents in the Karoubi Envelope are split
idempotent-split : ∀ {A} → Idempotent (KaroubiEnvelope 𝒞) A → SplitIdempotent (KaroubiEnvelope 𝒞) A
idempotent-split {A} I = record
  { idem = idem
  ; isSplitIdempotent = record
    { obj = record
      { isIdempotent = record
        { idem = idem.hom
        ; idempotent = idempotent
        }
      }
    ; retract = record
      { hom = idem.hom
      ; absorbˡ = idempotent
      ; absorbʳ = idem.absorbʳ
      }
    ; section = record
      { hom = idem.hom
      ; absorbˡ = idem.absorbˡ
      ; absorbʳ = idempotent
      }
    ; retracts = idempotent
    ; splits = idempotent
    }
  }
  where
    module A = BundledIdem.Idempotent A
    open Idempotent I
    module idem = BundledIdem.Idempotent⇒ idem

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Functor.Hom where

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

open import Categories.Support.Equivalence
open import Categories.Support.SetoidFunctions renaming (id to id′)
open import Categories.Category
open import Categories.Bifunctor using (Bifunctor; Functor; module Functor)
open import Categories.Agda

module Hom {o ℓ e} (C : Category o ℓ e) where
  open Category C

  Hom[-,-] : Bifunctor (Category.op C) C (ISetoids ℓ e)
  Hom[-,-] = record
    { F₀ = F₀′
    ; F₁ = λ f → record
      { _⟨$⟩_ = λ x → proj₂ f ∘ x ∘ proj₁ f
      ; cong = cong′ f
      }
    ; identity = identity′
    ; homomorphism = homomorphism′
    ; F-resp-≡ = F-resp-≡′
    }
    where

    F₀′ : Obj × Obj → Setoid ℓ e
    F₀′ x = record
      { Carrier = uncurry _⇒_ x
      ; _≈_ = _≡_
      ; isEquivalence = equiv
      }

    _⇆_ : ∀ A B → Set ℓ
    A ⇆ B = (proj₁ B ⇒ proj₁ A) × (proj₂ A ⇒ proj₂ B)

    .cong′ : ∀ {A B} → (f : A ⇆ B) → {x y : uncurry _⇒_ A} → x ≡ y
           → proj₂ f ∘ x ∘ proj₁ f ≡ proj₂ f ∘ y ∘ proj₁ f
    cong′ f x≡y = ∘-resp-≡ʳ (∘-resp-≡ˡ x≡y)

    .identity′ : {A : Obj × Obj} {x y : uncurry _⇒_ A} → x ≡ y → id ∘ x ∘ id ≡ y
    identity′ {A} {x} {y} x≡y =
      begin
        id ∘ x ∘ id
      ↓⟨ identityˡ ⟩
        x ∘ id
      ↓⟨ identityʳ ⟩
        x
      ↓⟨ x≡y ⟩
        y
      ∎
      where
      open HomReasoning

    .homomorphism′ : {X Y Z : Obj × Obj}
                   → {f : X ⇆ Y}
                   → {g : Y ⇆ Z}
                   → {x y : uncurry _⇒_ X} → (x ≡ y)
                   → (proj₂ g ∘ proj₂ f) ∘ (x ∘ (proj₁ f ∘ proj₁ g)) ≡ proj₂ g ∘ ((proj₂ f ∘ (y ∘ proj₁ f)) ∘ proj₁ g)
    homomorphism′ {f = f} {g} {x} {y} x≡y =
      begin
        (proj₂ g ∘ proj₂ f) ∘ (x ∘ (proj₁ f ∘ proj₁ g))
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ x≡y) ⟩
        (proj₂ g ∘ proj₂ f) ∘ (y ∘ (proj₁ f ∘ proj₁ g))
      ↓⟨ assoc ⟩
        proj₂ g ∘ (proj₂ f ∘ (y ∘ (proj₁ f ∘ proj₁ g)))
      ↑⟨ ∘-resp-≡ʳ assoc ⟩
        proj₂ g ∘ ((proj₂ f ∘ y) ∘ (proj₁ f ∘ proj₁ g))
      ↑⟨ ∘-resp-≡ʳ assoc ⟩
        proj₂ g ∘ (((proj₂ f ∘ y) ∘ proj₁ f) ∘ proj₁ g)
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ assoc) ⟩
        proj₂ g ∘ ((proj₂ f ∘ (y ∘ proj₁ f)) ∘ proj₁ g)
      ∎
      where
      open HomReasoning

    .F-resp-≡′ : {A B : Obj × Obj} {f g : A ⇆ B}
               → proj₁ f ≡ proj₁ g × proj₂ f ≡ proj₂ g
               → {x y : uncurry _⇒_ A} → (x ≡ y)
               → proj₂ f ∘ x ∘ proj₁ f ≡ proj₂ g ∘ y ∘ proj₁ g
    F-resp-≡′ (f₁≡g₁ , f₂≡g₂) x≡y = ∘-resp-≡ f₂≡g₂ (∘-resp-≡ x≡y f₁≡g₁)

  Hom[_,-] : Obj → Functor C (ISetoids ℓ e)
  Hom[_,-] B = record
    { F₀ = λ x → Hom[-,-].F₀ (B , x)
    ; F₁ = λ f → Hom[-,-].F₁ (id , f)
    ; identity = Hom[-,-].identity
    ; homomorphism = homomorphism′
    ; F-resp-≡ = λ F≡G x≡y → ∘-resp-≡ F≡G (∘-resp-≡ˡ x≡y)
    }
    where
    module Hom[-,-] = Functor Hom[-,-]

    -- I can't see an easy way to reuse the proof for the bifunctor :(
    -- luckily, it's an easy proof!
    .homomorphism′ : {X Y Z : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} {x y : B ⇒ X}
                   → (x ≡ y)   → (g ∘ f) ∘ (x ∘ id) ≡ g ∘ ((f ∘ (y ∘ id)) ∘ id)
    homomorphism′ {f = f} {g} {x} {y} x≡y =
      begin
        (g ∘ f) ∘ (x ∘ id)
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ x≡y) ⟩
        (g ∘ f) ∘ (y ∘ id)
      ↓⟨ assoc ⟩
        g ∘ (f ∘ (y ∘ id))
      ↑⟨ ∘-resp-≡ʳ identityʳ ⟩
        g ∘ ((f ∘ (y ∘ id)) ∘ id)
      ∎
      where
      open HomReasoning

  Hom[-,_] : Obj → Functor (Category.op C) (ISetoids ℓ e)
  Hom[-,_] B = record
    { F₀ = λ x → Hom[-,-].F₀ (x , B)
    ; F₁ = λ f → Hom[-,-].F₁ (f , id)
    ; identity = Hom[-,-].identity
    ; homomorphism = homomorphism′
    ; F-resp-≡ = λ F≡G x≡y → ∘-resp-≡ʳ (∘-resp-≡ x≡y F≡G)
    }
    where
    module Hom[-,-] = Functor Hom[-,-]

    .homomorphism′ : {X Y Z : Obj} {f : Y ⇒ X} {g : Z ⇒ Y} {x y : X ⇒ B} →
                    (x ≡ y) → id ∘ (x ∘ (f ∘ g)) ≡ id ∘ ((id ∘ (y ∘ f)) ∘ g)
    homomorphism′ {f = f} {g} {x} {y} x≡y =
      begin
        id ∘ (x ∘ (f ∘ g))
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ x≡y) ⟩
        id ∘ (y ∘ (f ∘ g))
      ↑⟨ ∘-resp-≡ʳ assoc ⟩
        id ∘ ((y ∘ f) ∘ g)
      ↑⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ identityˡ) ⟩
        id ∘ ((id ∘ (y ∘ f)) ∘ g)
      ∎
      where
      open HomReasoning

-- More explicit versions

Hom[_][-,-] : ∀ {o ℓ e} → (C : Category o ℓ e) → Bifunctor (Category.op C) C (ISetoids ℓ e)
Hom[ C ][-,-] = Hom[-,-]
  where open Hom C

Hom[_][_,-] : ∀ {o ℓ e} → (C : Category o ℓ e) → Category.Obj C → Functor C (ISetoids ℓ e)
Hom[ C ][ B ,-] = Hom[ B ,-]
  where open Hom C

Hom[_][-,_] : ∀ {o ℓ e} → (C : Category o ℓ e) → Category.Obj C → Functor (Category.op C) (ISetoids ℓ e)
Hom[ C ][-, B ] = Hom[-, B ]
  where open Hom C

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Path where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

-- Less polymorphic version of `cong`, to avoid some unresolved metas
cong′ : ∀ {B : Type ℓ'} (f : A → B) {x y : A} (p : x ≡ y)
      → Path B (f x) (f y)
cong′ f = cong f

toPathP-isEquiv : ∀ (A : I → Set ℓ){x y} → isEquiv (toPathP {A = A} {x} {y})
toPathP-isEquiv A {x} {y} = isoToIsEquiv (iso toPathP fromPathP to-from from-to)
 where
   to-from : ∀ (p : PathP A x y) → toPathP (fromPathP p) ≡ p
   to-from p h i = outS (hcomp-unique (λ { j (i = i0) → x ; j (i = i1) → fromPathP p j })
                                  (inS (transp (λ j → A (i ∧ j)) (~ i) x))
                                  \ h → inS (sq1 h i))
                        h
      where
        sq1 : (\ h → A [ x ≡ transp (\ j → A (h ∨ j)) h (p h) ]) [ (\ i → transp (λ j → A (i ∧ j)) (~ i) x) ≡ p ]
        sq1 = \ h i → comp (\ z → (hcomp (\ w →
                                                    \ { (z = i1) → A (i ∧ (w ∨ h))
                                                      ; (z = i0) → A (i ∧ h)
                                                      ; (i = i0) → A i0
                                                      ; (i = i1) → A (h ∨ (w ∧ z))
                                                      ; (h = i0) → A (i ∧ (w ∧ z))
                                                      ; (h = i1) → A i})
                                                   ((A (i ∧ h)))))
                                          (\ z → \ { (i = i0) → x
                                                   ; (i = i1) → transp (\ j → A (h ∨ (z ∧ j))) (h ∨ ~ z) (p h)
                                                   ; (h = i0) → transp (λ j → A ((i ∧ z) ∧ j)) (~ (i ∧ z)) x
                                                   ; (h = i1) → p i })
                                (p (i ∧ h))
   from-to : ∀ (q : transp A i0 x ≡ y) → fromPathP (toPathP {A = A} q) ≡ q
   from-to q = (\ h i → outS (transp-hcomp i {A' = A i1} (\ j → inS (A (i ∨ j)))
                                           ((λ { j (i = i0) → x ; j (i = i1) → q j }))
                                           (inS ((transp (λ j → A (i ∧ j)) (~ i) x))))
                             h)
             ∙ (\ h i → outS (hcomp-unique {A = A i1} ((λ { j (i = i0) → transp A i0 x ; j (i = i1) → q j }))
                                      (inS ((transp (λ j → A (i ∨ j)) i (transp (λ j → A (i ∧ j)) (~ i) x))))
                                      \ h → inS (sq2 h i))
                             h)
             ∙ sym (lUnit q)
     where
       sq2 : (\ h → transp A i0 x ≡ q h) [ (\ i → transp (\ j → A (i ∨ j)) i (transp (\ j → A (i ∧ j)) (~ i) x)) ≡ refl ∙ q ]
       sq2 = \ h i → comp (\ z → hcomp (\ w → \ { (i = i1) → A i1
                                              ; (i = i0) → A (h ∨ (w ∧ z))
                                              ; (h = i0) → A (i ∨ (w ∧ z))
                                              ; (h = i1) → A i1
                                              ; (z = i0) → A (i ∨ h)
                                              ; (z = i1) → A ((i ∨ h) ∨ w) })
                                             (A (i ∨ h)))
                 (\ z → \ { (i = i0) → transp (λ j → A ((z ∨ h) ∧ j)) (~ z ∧ ~ h) x
                          ; (i = i1) → q (z ∧ h)
                          ; (h = i1) → compPath-filler refl q z i
                          ; (h = i0) → transp (\ j → A (i ∨ (z ∧ j))) (i ∨ ~ z) (transp (\ j → A (i ∧ j)) (~ i) x)
                          })
                          (transp (\ j → A ((i ∨ h) ∧ j)) (~ (i ∨ h)) x)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module DivMod where

open import IO
open import Data.Nat
open import Data.Nat.DivMod
open import Codata.Musical.Notation
open import Data.String.Base
open import Data.Fin.Base using (toℕ)
open import Level using (0ℓ)

g : ℕ
g = 7 div 5

k : ℕ
k = toℕ (7 mod 5)

showNat : ℕ → String
showNat zero = "Z"
showNat (suc x) = "S (" ++ showNat x ++ ")"

main = run {0ℓ} (putStrLn (showNat g) >> putStrLn (showNat k))

max_stars_repo_name: guilhermehas/agda

max_issues_repo_name: guilhermehas/agda

max_forks_repo_name: guilhermehas/agda


text:
-- Andreas, 2016-07-29
--
--   agda --library-file=GARBAGE Issue2122.agda
--
-- should complain about non-existent library file.

-- This file is intentionally left empty.


text:
module Sets.IterativeSet.Oper where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using ()
open import Functional
open import Logic
open import Numeral.Natural
open import Relator.Equals using () renaming (_≡_ to Id ; [≡]-intro to intro)
open import Sets.IterativeSet
open import Syntax.Function
open import Type.Dependent

module _ where
  private variable {ℓ ℓ₁ ℓ₂} : Lvl.Level
  open Iset

  -- The empty set, consisting of no elements.
  -- Index is the empty type, which means that there are no objects pointing to elements in the set.
  ∅ : Iset{ℓ}
  ∅ = set{Index = Empty} empty

  -- The singleton set, consisting of one element.
  -- Index is the unit type, which means that there are a single object pointing to a single element in the set.
  singleton : Iset{ℓ} → Iset{ℓ}
  singleton = set{Index = Unit} ∘ const

  -- The pair set, consisting of two elements.
  -- Index is the boolean type, which means that there are two objects pointing to two elements in the set.
  pair : Iset{ℓ} → Iset{ℓ} → Iset{ℓ}
  pair A B = set{Index = Lvl.Up(Bool)} ((if_then B else A) ∘ Lvl.Up.obj)

  -- The union operator.
  -- Index(A ∪ B) is the either type of two indices, which means that both objects from the A and the B index point to elements in the set.
  _∪_ : Iset{ℓ} → Iset{ℓ} → Iset{ℓ}
  A ∪ B = set{Index = Index(A) ‖ Index(B)} (Either.map1 (elem(A)) (elem(B)))

  _,_ : Iset{ℓ} → Iset{ℓ} → Iset{ℓ}
  A , B = pair (singleton A) (pair A B)

  _⨯_ : Iset{ℓ} → Iset{ℓ} → Iset{ℓ}
  A ⨯ B = set{Index = Index(A) Tuple.⨯ Index(B)} \{(ia Tuple., ib) → (elem(A)(ia) , elem(B)(ib))}

  -- The big union operator.
  -- Index(⋃ A) is the dependent sum type of an Index(A) and the index of the element this index points to.
  ⋃ : Iset{ℓ} → Iset{ℓ}
  ⋃ A = set{Index = Σ(Index(A)) (ia ↦ Index(elem(A)(ia)))} (\{(intro ia i) → elem(elem(A)(ia))(i)})

  indexFilter : (A : Iset{ℓ}) → (Index(A) → Stmt{ℓ}) → Iset{ℓ}
  indexFilter A P = set{Index = Σ(Index(A)) P} (elem(A) ∘ Σ.left)

  filter : (A : Iset{ℓ}) → (Iset{ℓ} → Stmt{ℓ}) → Iset{ℓ}
  filter{ℓ} A P = indexFilter A (P ∘ elem(A))

  indexFilterBool : (A : Iset{ℓ}) → (Index(A) → Bool) → Iset{ℓ}
  indexFilterBool A f = indexFilter A (Lvl.Up ∘ IsTrue ∘ f)

  filterBool : (A : Iset{ℓ}) → (Iset{ℓ} → Bool) → Iset{ℓ}
  filterBool A f = indexFilterBool A (f ∘ elem(A))

  mapSet : (Iset{ℓ} → Iset{ℓ}) → (Iset{ℓ} → Iset{ℓ})
  mapSet f(A) = set{Index = Index(A)} (f ∘ elem(A))

  -- The power set operator.
  -- Index(℘(A)) is a function type. An instance of such a function represents a subset, and essentially maps every element in A to a boolean which is interpreted as "in the subset of not".
  -- Note: This only works properly in a classical setting. Trying to use indexFilter instead result in universe level problems.
  ℘ : Iset{ℓ} → Iset{ℓ}
  ℘(A) = set{Index = Index(A) → Bool} (indexFilterBool A)

  -- The set of ordinal numbers of the first order.
  ω : Iset{ℓ}
  ω = set{Index = Lvl.Up ℕ} (N ∘ Lvl.Up.obj) where
    N : ℕ → Iset{ℓ}
    N(𝟎)    = ∅
    N(𝐒(n)) = N(n) ∪ singleton(N(n))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty AVL trees
------------------------------------------------------------------------

-- AVL trees are balanced binary search trees.

-- The search tree invariant is specified using the technique
-- described by Conor McBride in his talk "Pivotal pragmatism".

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

open import Relation.Binary using (StrictTotalOrder)

module Data.AVL.NonEmpty
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where

open import Data.Bool.Base using (Bool)
open import Data.Empty
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; _++⁺_)
open import Data.Maybe.Base hiding (map)
open import Data.Nat.Base hiding (_<_; _⊔_; compare)
open import Data.Product hiding (map)
open import Data.Unit
open import Function
open import Level using (_⊔_; Lift; lift)
open import Relation.Unary

open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
open import Data.AVL.Value Eq.setoid
import Data.AVL.Indexed strictTotalOrder as Indexed
open Indexed using (K&_ ; ⊥⁺ ; ⊤⁺; ⊥⁺<⊤⁺; ⊥⁺<[_]<⊤⁺; ⊥⁺<[_]; [_]<⊤⁺; node; toList)

------------------------------------------------------------------------
-- Types and functions with hidden indices

-- NB: the height is non-zero thus guaranteeing that the AVL tree contains
-- at least one value.

data Tree⁺ {v} (V : Value v) : Set (a ⊔ v ⊔ ℓ₂) where
  tree : ∀ {h} → Indexed.Tree V ⊥⁺ ⊤⁺ (suc h) → Tree⁺ V

module _ {v} {V : Value v} where

  private
    Val = Value.family V

  singleton : (k : Key) → Val k → Tree⁺ V
  singleton k v = tree (Indexed.singleton k v ⊥⁺<[ k ]<⊤⁺)

  insert : (k : Key) → Val k → Tree⁺ V → Tree⁺ V
  insert k v (tree t) with Indexed.insert k v t ⊥⁺<[ k ]<⊤⁺
  ... | Indexed.0# , t′ = tree t′
  ... | Indexed.1# , t′ = tree t′

  insertWith : (k : Key) → (Maybe (Val k) → Val k) → Tree⁺ V → Tree⁺ V
  insertWith k f (tree t) with Indexed.insertWith k f t ⊥⁺<[ k ]<⊤⁺
  ... | Indexed.0# , t′ = tree t′
  ... | Indexed.1# , t′ = tree t′

  delete : Key → Tree⁺ V → Maybe (Tree⁺ V)
  delete k (tree {h}     t) with Indexed.delete k t ⊥⁺<[ k ]<⊤⁺
  delete k (tree {h}     t) | Indexed.1# , t′ = just (tree t′)
  delete k (tree {0}     t) | Indexed.0# , t′ = nothing
  delete k (tree {suc h} t) | Indexed.0# , t′ = just (tree t′)

  lookup : (k : Key) → Tree⁺ V → Maybe (Val k)
  lookup k (tree t) = Indexed.lookup k t ⊥⁺<[ k ]<⊤⁺

module _ {v w} {V : Value v} {W : Value w} where

  private
    Val = Value.family V
    Wal = Value.family W

  map : ∀[ Val ⇒ Wal ] → Tree⁺ V → Tree⁺ W
  map f (tree t) = tree $ Indexed.map f t

module _ {v} {V : Value v} where

  -- The input does not need to be ordered.

  fromList⁺ : List⁺ (K& V) → Tree⁺ V
  fromList⁺ = List⁺.foldr (uncurry insert) (uncurry singleton)

  -- The output is ordered

  toList⁺ : Tree⁺ V → List⁺ (K& V)
  toList⁺ (tree (node k&v l r bal)) = toList l ++⁺ k&v ∷ toList r


text:
module examplesPaperJFP.CounterCell where

open import Data.Product
open import Data.Nat.Base
open import Data.Nat.Show
open import Data.String.Base using (String; _++_)

open import Size

-- open import NativeIO

-- open import SizedIO.Base
-- open import SizedIO.Object
-- open import SizedIO.IOObject
-- open import SizedIO.ConsoleObject
-- open import SizedIO.Console hiding (main)

open import examplesPaperJFP.NativeIOSafe

open import examplesPaperJFP.ConsoleInterface
open import examplesPaperJFP.Console hiding (main)
open import examplesPaperJFP.Object using (Interface; Method; Result; CellMethod; get; put; CellResult; cellJ)
open import examplesPaperJFP.Sized hiding (program; main)

data CounterMethod A : Set where
  super  :  (m : CellMethod A) → CounterMethod A
  stats  :  CounterMethod A

pattern getᶜ    = super get
pattern putᶜ x  = super (put x)

statsCellI : (A : Set) → Interface
Method  (statsCellI A)            =  CounterMethod A
Result  (statsCellI A) (super m)  =  Result (cellJ A) m
Result  (statsCellI A) stats      =  Unit

CounterC : (i : Size) → Set
CounterC = IOObject ConsoleInterface (statsCellI String)

counterCell : ∀{i} (c : CellC i) (ngets nputs : ℕ) → CounterC i

method (counterCell c ngets nputs) getᶜ =
  method c get                                >>= λ { (s , c′) →
  return (s , counterCell c′ (1 + ngets) nputs)  }

method (counterCell c ngets nputs) (putᶜ x) =
  method c (put x)                            >>= λ { (_ , c′) →
  return (unit , counterCell c′ ngets (1 + nputs))  }

method (counterCell c ngets nputs) stats =
  exec (putStrLn ("Counted "
    ++ show ngets ++ " calls to get and "
    ++ show nputs ++ " calls to put."))       λ _ →
  return (unit , counterCell c ngets nputs)

program : String → IO ConsoleInterface ∞ Unit
program arg =
  let c₀ = counterCell (simpleCell "Start") 0 0 in
  method c₀ getᶜ               >>= λ{ (s   , c₁) →
  exec (putStrLn s)              λ _ →
  method c₁ (putᶜ arg)         >>= λ{ (_        , c₂) →
  method c₂ getᶜ               >>= λ{ (s′  , c₃) →
  exec (putStrLn s′)             λ _ →
  method c₃ (putᶜ "Over!")     >>= λ{ (_ , c₄) →
  method c₄ stats              >>= λ{ (_ , c₅) →
  return unit                  }}}}}

main : NativeIO Unit
main = translateIO translateIOConsoleLocal (program "Hello")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda