text:
module Numeral.Finite.Sequence where

import      Lvl
open import Data.Either as Either using (_‖_)
open import Data.Either.Equiv as Either
open import Data.Either.Equiv.Id
open import Data.Either.Proofs as Either
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Equiv as Tuple
open import Data.Tuple.Equiv.Id
open import Data.Tuple.Proofs as Tuple
open import Functional
open import Function.Equals
open import Function.Proofs
open import Logic
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.Finite
open import Numeral.Finite.Bound
-- open import Numeral.Finite.Equiv
import      Numeral.Finite.Oper as 𝕟
open import Numeral.Natural
import      Numeral.Natural.Oper as ℕ
open import Numeral.Natural.Oper.Proofs.Order
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv using () renaming ([≡]-equiv to Id-equiv ; [≡]-function to Id-function)
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
import      Structure.Function.Names as Names
open import Structure.Operator
open import Structure.Relator
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type
open import Type.Size

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ ℓₑ₅ ℓₑ₆ : Lvl.Level
private variable A : Type{ℓ₁}
private variable B : Type{ℓ₂}
private variable a b : ℕ

module Interleaving where
  join : (𝕟(a) ‖ 𝕟(b)) → 𝕟(a ℕ.+ b)
  join {𝟎}  {𝐒 b} (Either.Right n)     = n
  join {𝐒 a}{𝟎}   (Either.Left  n)     = n
  join {𝐒 a}{𝐒 b} (Either.Left  𝟎)     = 𝟎
  join {𝐒 a}{𝐒 b} (Either.Right 𝟎)     = 𝐒(𝟎)
  join {𝐒 a}{𝐒 b} (Either.Left  (𝐒 n)) = 𝐒(𝐒(join {a}{b} (Either.Left n)))
  join {𝐒 a}{𝐒 b} (Either.Right (𝐒 n)) = 𝐒(𝐒(join {a}{b} (Either.Right n)))

  split : 𝕟(a ℕ.+ b) → (𝕟(a) ‖ 𝕟(b))
  split {𝟎}   {𝐒 b} n         = Either.Right n
  split {𝐒 a} {𝟎}   n         = Either.Left  n
  split {𝐒 a} {𝐒 b} 𝟎         = Either.Left  𝟎
  split {𝐒 a} {𝐒 b} (𝐒(𝟎))    = Either.Right 𝟎
  split {𝐒 a} {𝐒 b} (𝐒(𝐒(n))) = Either.map 𝐒 𝐒 (split {a} {b} n)

  instance
    join-split-inverses : Inverseᵣ(join{a}{b})(split{a}{b})
    join-split-inverses {a}{b} = intro(proof{a}{b}) where
      proof : ∀{a b} → Names.Inverses(join{a}{b})(split{a}{b})
      proof {𝟎}  {𝐒 b}{𝟎}      = [≡]-intro
      proof {𝟎}  {𝐒 b}{𝐒 n}    = [≡]-intro
      proof {𝐒 a}{𝟎}  {𝟎}      = [≡]-intro
      proof {𝐒 a}{𝟎}  {𝐒 n}    = [≡]-intro
      proof {𝐒 a}{𝐒 b}{𝟎}      = [≡]-intro
      proof {𝐒 a}{𝐒 b}{𝐒 𝟎}    = [≡]-intro
      proof {𝐒 a}{𝐒 b}{𝐒(𝐒 n)} with split{a}{b} n | proof {a}{b}{n}
      ... | Either.Left  m | p = congruence₁(𝐒) (congruence₁(𝐒) p)
      ... | Either.Right m | p = congruence₁(𝐒) (congruence₁(𝐒) p)

  instance
    split-join-inverses : Inverseₗ(join{a}{b})(split{a}{b})
    split-join-inverses {a}{b} = intro(proof{a}{b}) where
      proof : ∀{a b} → Names.Inverses(split{a}{b})(join{a}{b})
      proof {𝟎}      {𝟎}      {Either.Left  ()}
      proof {𝟎}      {𝟎}      {Either.Right ()}
      proof {𝟎}      {𝐒 b}    {Either.Right n}     = [≡]-intro
      proof {𝐒 a}    {𝟎}      {Either.Left  n}     = [≡]-intro
      proof {𝐒 a}    {𝐒 b}    {Either.Left  𝟎}     = [≡]-intro
      proof {𝐒 a}    {𝐒 b}    {Either.Right 𝟎}     = [≡]-intro
      proof {𝐒(𝐒 a)} {𝐒 𝟎}    {Either.Left  (𝐒 n)} = [≡]-intro
      proof {𝐒 𝟎}    {𝐒(𝐒 b)} {Either.Right (𝐒 n)} = [≡]-intro
      proof {𝐒(𝐒 a)} {𝐒(𝐒 b)} {Either.Left  (𝐒 n)} with join{𝐒 a}{𝐒 b} (Either.Left n) | proof {𝐒 a}{𝐒 b}{Either.Left n}
      ... | 𝟎      | p = congruence₁(Either.map 𝐒 𝐒) p
      ... | 𝐒(𝐒 m) | p = congruence₁(Either.map 𝐒 𝐒) p
      proof {𝐒(𝐒 a)} {𝐒(𝐒 b)} {Either.Right (𝐒 n)} with join{𝐒 a}{𝐒 b} (Either.Right n) | proof {𝐒 a}{𝐒 b}{Either.Right n}
      ... | 𝐒(𝟎)   | p = congruence₁(Either.map 𝐒 𝐒) p
      ... | 𝐒(𝐒 m) | p = congruence₁(Either.map 𝐒 𝐒) p

  instance
    split-join-inverse : Inverse(split{a}{b})(join{a}{b})
    split-join-inverse = [∧]-intro join-split-inverses split-join-inverses

  instance
    split-bijective : Bijective(split{a}{b})
    split-bijective = invertible-to-bijective ⦃ inver = [∃]-intro join ⦃ [∧]-intro Id-function split-join-inverse ⦄ ⦄

-- Interleaves two sequences into one, alternating between the elements and then putting the leftovers at the end.
interleave : (𝕟(a) → A) → (𝕟(b) → B) → (𝕟(a ℕ.+ b) → (A ‖ B))
interleave af bf = Either.map af bf ∘ Interleaving.split

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-AB : Equiv{ℓₑ}(A ‖ B) ⦄ ⦃ ext-AB : Either.Extensionality ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (equiv-AB) ⦄
  {af : 𝕟(a) → A} ⦃ bij-af : Bijective ⦃ Id-equiv ⦄ ⦃ equiv-A ⦄ (af) ⦄
  {bf : 𝕟(b) → B} ⦃ bij-bf : Bijective ⦃ Id-equiv ⦄ ⦃ equiv-B ⦄ (bf) ⦄
  where

  instance
    interleave-bijective : Bijective(interleave af bf)
    interleave-bijective = [∘]-bijective ⦃ bij-f = Either.map-bijective ⦄ ⦃ bij-g = Interleaving.split-bijective ⦄

module Concatenation where
  join : (𝕟(a) ‖ 𝕟(b)) → 𝕟(a ℕ.+ b)
  join {a} {b} (Either.Left  n) = bound-[≤] [≤]-of-[+]ₗ n
  join {a} {b} (Either.Right n) = a 𝕟.Unclosed.+ₙₗ n

  split : 𝕟(a ℕ.+ b) → (𝕟(a) ‖ 𝕟(b))
  split {𝟎}  {𝐒 b} n     = Either.Right n
  split {𝐒 a}{𝟎}   n     = Either.Left n
  split {𝐒 a}{𝐒 b} 𝟎     = Either.Left 𝟎
  split {𝐒 a}{𝐒 b} (𝐒 n) = Either.mapLeft 𝐒 (split {a}{𝐒 b} n)

  open import Numeral.Finite.Category
  open import Structure.Category.Functor
  instance
    join-split-inverses : Inverseᵣ(join{a}{b})(split{a}{b})
    join-split-inverses {a}{b} = intro(proof{a}{b}) where
      proof : ∀{a b} → Names.Inverses(join{a}{b})(split{a}{b})
      proof {𝟎}   {𝐒 b} {n} = [≡]-intro
      proof {𝐒 a} {𝟎}   {n} = _⊜_.proof (Functor.id-preserving bound-functor)
      proof {𝐒 a} {𝐒 b} {𝟎} = [≡]-intro
      proof {𝐒 a} {𝐒 b} {𝐒 n} with split {a}{𝐒 b} n | proof {a} {𝐒 b} {n}
      ... | Either.Left  _ | [≡]-intro = [≡]-intro
      ... | Either.Right _ | [≡]-intro = [≡]-intro

  instance
    split-join-inverses : Inverseₗ(join{a}{b})(split{a}{b})
    split-join-inverses {a}{b} = intro(proof{a}{b}) where
      proof : ∀{a b} → Names.Inverses(split{a}{b})(join{a}{b})
      proof {𝟎}   {𝐒 b} {Either.Right n}     = [≡]-intro
      proof {𝐒 a} {𝟎}   {Either.Left  n}     = congruence₁(Either.Left) (_⊜_.proof (Functor.id-preserving bound-functor))
      proof {𝐒 a} {𝐒 b} {Either.Left  𝟎}     = [≡]-intro
      proof {𝐒 a} {𝐒 b} {Either.Left  (𝐒 n)} = congruence₁(Either.mapLeft 𝐒) (proof{a}{𝐒 b} {Either.Left  n})
      proof {𝐒 a} {𝐒 b} {Either.Right n}     = congruence₁(Either.mapLeft 𝐒) (proof{a}{𝐒 b} {Either.Right n})

  instance
    split-join-inverse : Inverse(split{a}{b})(join{a}{b})
    split-join-inverse = [∧]-intro join-split-inverses split-join-inverses

  instance
    split-bijective : Bijective(split{a}{b})
    split-bijective = invertible-to-bijective ⦃ inver = [∃]-intro join ⦃ [∧]-intro Id-function split-join-inverse ⦄ ⦄

-- Concatenates two sequences into one, putting the elements of the first sequence first followed by the elements of the second sequence.
concat : (𝕟(a) → A) → (𝕟(b) → B) → (𝕟(a ℕ.+ b) → (A ‖ B))
concat af bf = Either.map af bf ∘ Concatenation.split

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-AB : Equiv{ℓₑ}(A ‖ B) ⦄ ⦃ ext-AB : Either.Extensionality ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (equiv-AB) ⦄
  {af : 𝕟(a) → A} ⦃ bij-af : Bijective ⦃ Id-equiv ⦄ ⦃ equiv-A ⦄ (af) ⦄
  {bf : 𝕟(b) → B} ⦃ bij-bf : Bijective ⦃ Id-equiv ⦄ ⦃ equiv-B ⦄ (bf) ⦄
  where

  instance
    concat-bijective : Bijective(concat af bf)
    concat-bijective = [∘]-bijective ⦃ bij-f = Either.map-bijective ⦄ ⦃ bij-g = Concatenation.split-bijective ⦄

module LinearSpaceFilling where
  join : (𝕟(a) ⨯ 𝕟(b)) → 𝕟(a ℕ.⋅ b)
  join = Tuple.uncurry(𝕟.Exact._⋅_)

  -- split : 𝕟(a ℕ.⋅ b) → (𝕟(a) ⨯ 𝕟(b))
  -- split {a}{b} n = ({!n mod a!} , {!n / a!})

module BaseNumerals where -- TODO: Maybe try to use Numeral.FixedPositional
  -- When interpreting the function as a numeral in a certain base, the parameters mean the following:
  -- • `a` is the base.
  -- • `b` is the length of the numerals (the maximum number of digits).
  -- • The argument of the specified function is the position of the numeral.
  -- • The value of the specified function is the digit on the argument's position.
  {-join : (𝕟(a) ← 𝕟(b)) → 𝕟(a ℕ.^ b)
  join {a}{𝟎}   f = 𝟎
  join {a}{𝐒 b} f = {!f(𝟎) 𝕟.Exact.+ ((join {a}{b} (f ∘ 𝐒)) 𝕟.Unclosed.⋅ₙᵣ a)!}-}
  -- f(𝟎) 𝕟.Exact.⋅ join {a}{b} (f ∘ 𝐒)
  -- 4321
  -- 1⋅10⁰ + 2⋅10¹ + 3⋅10² + 4⋅10³
  -- 1 + 10⋅(2 + 10⋅(3 + 10⋅(4 + 10⋅0)))

  -- TODO: Something is incorrect here. This is the type of the induction step:
  -- a + 𝐒(a⋅(a ^ b))
  -- 𝐒(a + a⋅(a ^ b))
  -- 𝐒(a + (a ^ 𝐒(b)))
  -- 𝐒(a) + (a ^ 𝐒(b))

  {-
  open import Data.Boolean
  join : (𝕟(a) → Bool) → 𝕟(2 ℕ.^ a)
  join {𝟎}   f = 𝟎
  join {𝐒 a} f = {!(if f(𝟎) then 𝕟.𝐒(𝕟.𝟎) else 𝕟.𝟎) 𝕟.Exact.+ join {a} (f ∘ 𝕟.𝐒)!}
  -}

{- TODO: Old stuff below. Could be useful to have some properties of the interleave and concat functions
-- Interleaves two sequences into one, alternating between the elements and then putting the leftovers at the end.
interleave : (𝕟(a) → A) → (𝕟(b) → B) → (𝕟(a ℕ.+ b) → (A ‖ B))
interleave {a = 𝟎}   {b = 𝐒 b} af bf n        = Either.Right(bf(n))
interleave {a = 𝐒 a} {b = 𝟎}   af bf n        = Either.Left(af(n))
interleave {a = 𝐒 a} {b = 𝐒 b} af bf 𝟎        = Either.Left(af(𝟎))
interleave {a = 𝐒 a} {b = 𝐒 b} af bf (𝐒 𝟎)    = Either.Right(bf(𝟎))
interleave {a = 𝐒 a} {b = 𝐒 b} af bf (𝐒(𝐒 n)) = interleave {a = a}{b = b} (af ∘ 𝐒) (bf ∘ 𝐒) n

-- Concatenates two sequences into one, putting the elements of the first sequence first followed by the elements of the second sequence.
concat : (𝕟(a) → A) → (𝕟(b) → B) → (𝕟(a ℕ.+ b) → (A ‖ B))
concat {a = 𝟎}   {b = 𝐒 b} af bf n     = Either.Right(bf(n))
concat {a = 𝐒 a} {b = b}   af bf 𝟎     = Either.Left(af(𝟎))
concat {a = 𝐒 a} {b = b}   af bf (𝐒 n) = concat {a = a} {b = b} (af ∘ 𝐒) bf n

concat-is-left : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n : 𝕟(a)} → (concat af bf (bound-[≤] [≤]-of-[+]ₗ n) ≡ Either.Left(af(n)))
concat-is-left {a = 𝐒 a} {b} {af}{bf} {n = 𝟎}   = [≡]-intro
concat-is-left {a = 𝐒 a} {𝟎} {af}{bf} {n = 𝐒 n} = ([≡]-with(concat af bf) (p{n = n})) 🝖 concat-is-left {a = a} {b = 𝟎} {af = af ∘ 𝐒}{bf = bf} {n = n} where
  p : ∀{A}{n : 𝕟(A)} → (bound-[≤] ([≤]-of-[+]ₗ {𝐒 A}{𝟎}) (𝐒(n)) ≡ 𝐒(bound-[≤] [≤]-of-[+]ₗ n))
  p {.(𝐒 _)} {𝟎}   = [≡]-intro
  p {.(𝐒 _)} {𝐒 n} = [≡]-intro
concat-is-left {a = 𝐒 a} {𝐒 b} {af}{bf} {n = 𝐒 n} = concat-is-left {a = a} {b = 𝐒 b} {af = af ∘ 𝐒}{bf = bf} {n = n}

concat-is-left-on-0 : ∀{a}{af : 𝕟(a) → A}{bf : 𝕟(𝟎) → B}{n : 𝕟(a)} → (concat af bf n ≡ Either.Left(af(n)))
concat-is-left-on-0 {a = 𝐒 a} {n = 𝟎} = [≡]-intro
concat-is-left-on-0 {a = 𝐒 a} {n = 𝐒 n} = concat-is-left-on-0 {a = a} {n = n}

-- concat-is-right : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(𝐒 b) → B}{n : 𝕟(b)} → (concat af bf (maximum{n = a} 𝕟.+ n) ≡ Either.Right(bf(bound-𝐒 n)))

concat-left-pattern : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n : 𝕟(a ℕ.+ b)}{aa} → (concat af bf n ≡ Either.Left(aa)) → ∃(k ↦ (af(k) ≡ aa))
concat-left-pattern {a = 𝟎} {𝟎} {af} {bf} {}
concat-left-pattern {a = 𝐒 a} {b} {af} {bf} {𝟎} {aa} p = [∃]-intro 𝟎 ⦃ injective(Either.Left) p ⦄
concat-left-pattern {a = 𝐒 a} {𝟎} {af} {bf} {𝐒 n} {aa} p rewrite concat-is-left-on-0 {af = af}{bf = bf}{n = 𝐒 n} = [∃]-intro (𝐒(n)) ⦃ injective(Either.Left) p ⦄
concat-left-pattern {a = 𝐒 a} {𝐒 b} {af} {bf} {𝐒 n} {aa} p with concat-left-pattern {a = a}{𝐒 b}{af ∘ 𝐒}{bf}{n}
... | q with q p
... | [∃]-intro witness ⦃ proof ⦄ = [∃]-intro (𝐒 witness) ⦃ proof ⦄

concat-right-pattern : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n : 𝕟(a ℕ.+ b)}{bb} → (concat af bf n ≡ Either.Right(bb)) → ∃(k ↦ (bf(k) ≡ bb))
concat-right-pattern {a = 𝟎} {𝟎}     {af} {bf} {}
concat-right-pattern {a = 𝟎} {𝐒 b}   {af} {bf} {𝟎} {bb} p = [∃]-intro 𝟎 ⦃ injective(Either.Right) p ⦄
concat-right-pattern {a = 𝟎} {𝐒 b}   {af} {bf} {𝐒 n} {bb} p = [∃]-intro (𝐒(n)) ⦃ injective(Either.Right) p ⦄
concat-right-pattern {a = 𝐒 a} {𝟎}   {af} {bf} {𝐒 n} {bb} p = concat-right-pattern {a = a}{𝟎} {af ∘ 𝐒}{bf} {n} {bb} p
concat-right-pattern {a = 𝐒 a} {𝐒 b} {af} {bf} {𝐒 n} {bb} p = concat-right-pattern {a = a}{𝐒 b}{af ∘ 𝐒}{bf}{n} p

concat-left-or-right : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n : 𝕟(a ℕ.+ b)} → ∃(aa ↦ concat af bf n ≡ Either.Left(af(aa))) ∨ ∃(bb ↦ concat af bf n ≡ Either.Right(bf(bb)))
concat-left-or-right {a = a} {b} {af} {bf} {n} with concat af bf n | inspect (concat af bf) n
... | [∨]-introₗ aa | intro q with [∃]-intro r ⦃ rp ⦄ ← concat-left-pattern{a = a}{b}{af}{bf}{n}{aa} q = [∨]-introₗ ([∃]-intro r ⦃ [≡]-with(Either.Left) (symmetry(_≡_) rp) ⦄)
... | [∨]-introᵣ bb | intro q with [∃]-intro r ⦃ rp ⦄ ← concat-right-pattern{a = a}{b}{af}{bf}{n}{bb} q = [∨]-introᵣ ([∃]-intro r ⦃ [≡]-with(Either.Right) (symmetry(_≡_) rp) ⦄)

instance
  concat-injective : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → ⦃ Injective(af) ⦄ → ⦃ Injective(bf) ⦄ → Injective(concat af bf)
  Injective.proof (concat-injective {a = 𝟎} {𝐒 b} {af} {bf}) {x} {y} p = injective(bf) (injective(Either.Right) p)
  Injective.proof (concat-injective {a = 𝐒 a} {b} {af} {bf}) {𝟎} {𝟎} p = [≡]-intro
  Injective.proof (concat-injective {a = 𝐒 a} {𝟎} {af} {bf}) {𝟎} {𝐒 y} p rewrite concat-is-left-on-0 {af = af}{bf = bf}{n = 𝐒 y} with () ← injective(af) (injective(Either.Left) p)
  Injective.proof (concat-injective {a = 𝐒 a} {𝟎} {af} {bf}) {𝐒 x} {𝟎} p rewrite concat-is-left-on-0 {af = af}{bf = bf}{n = 𝐒 x} with () ← injective(af) (injective(Either.Left) p)
  Injective.proof (concat-injective {a = 𝐒 a} {𝐒 b} {af} {bf}) {𝟎} {𝐒 y} p with concat-left-or-right{af = af ∘ 𝐒}{bf = bf}{n = y}
  ... | [∨]-introₗ ([∃]-intro _ ⦃ proof ⦄) with () ← injective(af) (injective(Either.Left) (p 🝖 proof))
  ... | [∨]-introᵣ ([∃]-intro _ ⦃ proof ⦄) with () ← p 🝖 proof
  Injective.proof (concat-injective {a = 𝐒 a} {𝐒 b} {af} {bf}) {𝐒 x} {𝟎} p with concat-left-or-right{af = af ∘ 𝐒}{bf = bf}{n = x}
  ... | [∨]-introₗ ([∃]-intro _ ⦃ proof ⦄) with () ← injective(af) (injective(Either.Left) (symmetry(_≡_) p 🝖 proof))
  ... | [∨]-introᵣ ([∃]-intro _ ⦃ proof ⦄) with () ← symmetry(_≡_) p 🝖 proof
  {-# CATCHALL #-}
  Injective.proof (concat-injective {a = 𝐒 a} {b} {af} {bf}) {𝐒 x} {𝐒 y} p = congruence₁(𝐒) (Injective.proof (concat-injective {a = a} {b} {af ∘ 𝐒} {bf} ⦃ [∘]-injective {f = af}{g = 𝐒} ⦄) {x} {y} p)

concat-when-left : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n} → ∃(aa ↦ concat af bf n ≡ Either.Left(aa)) ↔ (𝕟-to-ℕ(n) < a)
concat-when-left {a = a} {b} {af} {bf} {n} = [↔]-intro l r where
  l : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n} → ∃(aa ↦ concat af bf n ≡ Either.Left(aa)) ← (𝕟-to-ℕ(n) < a)
  l {a = .(𝐒 _)} {b} {af} {bf} {𝟎}   [≤]-with-[𝐒] = [∃]-intro (af(𝟎)) ⦃ reflexivity(_≡_) ⦄
  l {a = .(𝐒 _)} {b} {af} {bf} {𝐒 n} ([≤]-with-[𝐒] {y = a} ⦃ p ⦄) = l {a = a}{b}{af ∘ 𝐒}{bf}{n} p

  r : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n} → ∃(aa ↦ concat af bf n ≡ Either.Left(aa)) → (𝕟-to-ℕ(n) < a)
  r {a = 𝟎}   {b} {af} {bf} {𝟎}   ([∃]-intro aa ⦃ ⦄)
  r {a = 𝐒 a} {b} {af} {bf} {𝟎}   ([∃]-intro aa ⦃ p ⦄) = [<]-minimum
  r {a = 𝐒 a} {b} {af} {bf} {𝐒 n} ([∃]-intro aa ⦃ p ⦄) = [≤]-with-[𝐒] ⦃ r {a = a}{b}{af ∘ 𝐒}{bf}{n} ([∃]-intro aa ⦃ p ⦄) ⦄

concat-when-right : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n} → ∃(bb ↦ concat af bf n ≡ Either.Right(bb)) ↔ (a ≤ 𝕟-to-ℕ(n))
concat-when-right {a = a} {b} {af} {bf} {n} = [↔]-intro l r where
  l : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n} → ∃(bb ↦ concat af bf n ≡ Either.Right(bb)) ← (a ≤ 𝕟-to-ℕ(n))
  l {a = 𝟎}   {𝐒 b} {af} {bf} {n} [≤]-minimum  = [∃]-intro (bf(n)) ⦃ reflexivity(_≡_) ⦄
  l {a = 𝐒 a} {b} {af} {bf} {𝐒 n} ([≤]-with-[𝐒] ⦃ p ⦄) = l {a = a}{b}{af ∘ 𝐒}{bf}{n} p

  r : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n} → ∃(bb ↦ concat af bf n ≡ Either.Right(bb)) → (a ≤ 𝕟-to-ℕ(n))
  r {a = 𝟎}   {b} {af} {bf} {_}   ([∃]-intro bb ⦃ p ⦄) = [≤]-minimum
  r {a = 𝐒 a} {b} {af} {bf} {𝟎}   ([∃]-intro bb ⦃ ⦄)
  r {a = 𝐒 a} {b} {af} {bf} {𝐒 n} ([∃]-intro bb ⦃ p ⦄) = [≤]-with-[𝐒] ⦃ r {a = a}{b}{af ∘ 𝐒}{bf}{n} ([∃]-intro bb ⦃ p ⦄) ⦄

𝕟-shrink : ∀{A B} → (b : 𝕟(B)) → (𝕟-to-ℕ(b) < A) → 𝕟(A)
𝕟-shrink {𝐒 A}{𝐒 B} 𝟎     [≤]-with-[𝐒] = 𝟎
𝕟-shrink {𝐒 A}{𝐒 B} (𝐒 b) ([≤]-with-[𝐒] ⦃ p ⦄) = 𝐒(𝕟-shrink {A}{B} b p)

𝕟-subtract : ∀{A B} → (b : 𝕟(B)) → (A < 𝕟-to-ℕ(b)) → 𝕟(𝐒(A))
𝕟-subtract {𝟎}  {𝐒 B} (𝐒 b) [≤]-with-[𝐒] = 𝟎
𝕟-subtract {𝐒 A}{𝐒 B} (𝐒 b) ([≤]-with-[𝐒] ⦃ p ⦄) = 𝐒(𝕟-subtract {A}{B} b p)

concat-when-lesser : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{n} → (na : 𝕟-to-ℕ(n) < a) → (concat af bf n ≡ Either.Left(af(𝕟-shrink n na)))
concat-when-lesser {a = 𝐒 a} {b} {af} {bf} {𝟎}   [≤]-with-[𝐒]         = [≡]-intro
concat-when-lesser {a = 𝐒 a} {b} {af} {bf} {𝐒 n} ([≤]-with-[𝐒] ⦃ p ⦄) = concat-when-lesser {a = a} {b} {af ∘ 𝐒} {bf} {n} p

{-
open import Numeral.Natural.Relation.Order.Proofs
concat-when-greater : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(𝐒(b)) → B}{n} → (bn : 𝐒(b) < 𝕟-to-ℕ(n)) → (concat af bf n ≡ Either.Right(bf(𝕟-subtract n ([≤]-predecessor bn))))
concat-when-greater {a = 𝟎} {𝐒 b} {af} {bf} {𝐒 n} [≤]-with-[𝐒] = {!!}
concat-when-greater {a = 𝐒 a} {𝟎} {af} {bf} {𝐒 n} ([≤]-with-[𝐒] {y = y} ⦃ p ⦄) with n | 𝕟-to-ℕ n
... | 𝟎 | 𝟎 = {!concat-when-greater {a = a} {?} {af ∘ 𝐒} {bf} {𝟎}!}
... | 𝟎 | 𝐒 bb = {!!}
... | 𝐒 aa | 𝟎 = {!!}
... | 𝐒 aa | 𝐒 bb = {!!}
concat-when-greater {a = 𝐒 a} {𝐒 b} {af} {bf} {𝐒 n} ([≤]-with-[𝐒] {y = _} ⦃ p ⦄) = {!concat-when-greater {a = a} {𝐒 b} {af ∘ 𝐒} {bf} {n}!}

open import Numeral.Natural.Relation.Order.Proofs
bound-[≤]-of-refl : ∀{n}{x} → (bound-[≤] (reflexivity(_≤_) {n}) x ≡ x)
bound-[≤]-of-refl {𝐒 n} {𝟎}   = [≡]-intro
bound-[≤]-of-refl {𝐒 n} {𝐒 x} = [≡]-with(𝐒) (bound-[≤]-of-refl {n}{x})

concat-surjective-left : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B}{x} → ⦃ Surjective(af) ⦄ → ∃(n ↦ concat af bf n ≡ Either.Left(x))
concat-surjective-left {a = 𝟎} {b} {af} {bf} {x} with () ← [∃]-witness(surjective(af) {x})
concat-surjective-left {a = 𝐒 a} {b} {af} {bf} {x} with [∃]-intro x ⦃ q ⦄ ← [↔]-to-[←] (concat-when-left {a = 𝐒 a}{b}{af}{bf}{{!!}}) {!!} = {!!}
{-∃.witness (concat-surjective-left {a = a} {b} {af} {bf} {x}) = bound-[≤] ([≤]-of-[+]ₗ {y = b}) ([∃]-witness(surjective(af) {x}))
∃.proof   (concat-surjective-left {a = 𝟎}   {_}   {af} {bf} {x}) with () ← [∃]-witness(surjective(af) {x})
∃.proof   (concat-surjective-left {a = 𝐒 a} {𝟎}   {af} {bf} {x}) rewrite bound-[≤]-of-refl {𝐒 a}{[∃]-witness(surjective(af) {x})} with surjective(af) {x}
... | [∃]-intro 𝟎     ⦃ p ⦄ = congruence₁(Either.Left) p
... | [∃]-intro (𝐒 c) ⦃ p ⦄ with [∃]-intro x ⦃ q ⦄ ← [↔]-to-[←] (concat-when-left {a = 𝐒 a}{𝟎}{af}{bf}{𝐒 c}) {!!} = {!!}
∃.proof   (concat-surjective-left {a = 𝐒 a} {𝐒 b} {af} {bf} {x}) = {!!}-}
-}

interleave-join-equality : ∀{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → (interleave af bf ∘ Interleaving.join ⊜ Either.map af bf)
interleave-join-equality {a = a}{b = b} = intro(p{a = a}{b = b}) where
  p : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → (interleave af bf ∘ Interleaving.join Names.⊜ Either.map af bf)
  p {a = 𝟎}  {b = 𝐒 b} {af}{bf} {Either.Right n}     = [≡]-intro
  p {a = 𝐒 a}{b = 𝟎}   {af}{bf} {Either.Left  n}     = [≡]-intro
  p {a = 𝐒 a}{b = 𝐒 b} {af}{bf} {Either.Left  𝟎}     = [≡]-intro
  p {a = 𝐒 a}{b = 𝐒 b} {af}{bf} {Either.Right 𝟎}     = [≡]-intro
  p {a = 𝐒 a}{b = 𝐒 b} {af}{bf} {Either.Left  (𝐒 n)} = p {a = a}{b = b} {af ∘ 𝐒}{bf ∘ 𝐒} {Either.Left  n}
  p {a = 𝐒 a}{b = 𝐒 b} {af}{bf} {Either.Right (𝐒 n)} = p {a = a}{b = b} {af ∘ 𝐒}{bf ∘ 𝐒} {Either.Right n}

interleave-split-equality : ∀{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → (interleave af bf ⊜ Either.map af bf ∘ Interleaving.split)
interleave-split-equality {a = a}{b = b}{af = af}{bf = bf} =
  interleave af bf                                                🝖[ _⊜_ ]-[]
  interleave af bf ∘ id                                           🝖[ _⊜_ ]-[ congruence₂ᵣ(_∘_)(interleave af bf) (intro(inverseᵣ(Interleaving.join{a}{b})(Interleaving.split{a}{b}))) ]-sym
  interleave af bf ∘ Interleaving.join{a}{b} ∘ Interleaving.split 🝖[ _⊜_ ]-[ congruence₂ₗ(_∘_)(Interleaving.split) (interleave-join-equality{a = a}{b = b}{af = af}{bf = bf}) ]
  Either.map af bf ∘ Interleaving.split                          🝖-end

instance
  interleave-injective : ∀{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → ⦃ Injective(af) ⦄ → ⦃ Injective(bf) ⦄ → Injective(interleave af bf)
  interleave-injective {a = a}{b = b}{af = af}{bf = bf} = substitute₁ₗ(Injective) (interleave-split-equality {af = af}{bf = bf}) ([∘]-injective {f = Either.map af bf}{g = Interleaving.split} ⦃ inj-g = inverse-to-injective ⦃ inver = [∧]-intro Interleaving.join-split-inverse Interleaving.split-join-inverse ⦄ ⦄)

instance
  interleave-surjective : ∀{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → ⦃ Surjective(af) ⦄ → ⦃ Surjective(bf) ⦄ → Surjective(interleave af bf)
  interleave-surjective {a = a}{b = b}{af = af}{bf = bf} = substitute₁ₗ(Surjective) (interleave-split-equality {af = af}{bf = bf}) ([∘]-surjective {f = Either.map af bf}{g = Interleaving.split} ⦃ surj-g = inverse-to-surjective ⦃ inver = [∧]-intro Interleaving.join-split-inverse Interleaving.split-join-inverse ⦄ ⦄)

instance
  interleave-bijective : ∀{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → ⦃ Bijective(af) ⦄ → ⦃ Bijective(bf) ⦄ → Bijective(interleave af bf)
  interleave-bijective {a = a}{b = b}{af = af}{bf = bf} = substitute₁ₗ(Bijective) (interleave-split-equality {af = af}{bf = bf}) ([∘]-bijective {f = Either.map af bf}{g = Interleaving.split} ⦃ bij-g = inverse-to-bijective ⦃ inver = [∧]-intro Interleaving.join-split-inverse Interleaving.split-join-inverse ⦄ ⦄)

concat-split-equality : ∀{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → (concat af bf ⊜ Either.map af bf ∘ Concatenation.split)
concat-split-equality {a = a}{b = b} = intro(p{a = a}{b = b}) where
  p : ∀{a b}{af : 𝕟(a) → A}{bf : 𝕟(b) → B} → (concat af bf Names.⊜ Either.map af bf ∘ Concatenation.split)
  p {a = 𝟎}     {b = 𝐒 b} {af = af}{bf = bf} {n}   = [≡]-intro
  p {a = 𝐒 a}   {b = 𝟎}   {af = af}{bf = bf} {𝟎}   = [≡]-intro
  p {a = 𝐒(𝐒 a)}{b = 𝟎}   {af = af}{bf = bf} {𝐒 n} = p{a = 𝐒 a}{b = 𝟎}{af = af ∘ 𝐒}{bf = bf}{n}
  p {a = 𝐒 a}   {b = 𝐒 b} {af = af}{bf = bf} {𝟎}   = [≡]-intro
  p {a = 𝐒 a}   {b = 𝐒 b} {af = af}{bf = bf} {𝐒 n} with Concatenation.split {a}{𝐒 b} n | p {a = a} {b = 𝐒 b} {af = af ∘ 𝐒} {bf = bf} {n}
  ... | Either.Left  _ | prev = prev
  ... | Either.Right _ | prev = prev

-- TODO: It is possible to copy-paste the proofs of inj/surj/bijectivity with a few modifications from Interleaving and apply it to Concatenation

-}

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:
open import Agda.Primitive
open import Data.Nat using (ℕ)

data ∑ {n₁ : Level} {n₂ : Level} (A : Set n₁) (P : A → Set n₂) : Set (n₁ ⊔ n₂) where
  sum : (a : A) → (pa : P a) → ∑ A P

data List {n : Level} (t : Set n) : Set n where
  _::_ : t → List t → List t
  []   : List t

data Unit {n : Level} : Set n where
  ##   : Unit

heterohomo : List (∑ Set λ x → x)
heterohomo = (sum ℕ 0) :: ((sum (List Unit) (## :: [])) :: ((sum Unit ##) :: []))

ext: agda

max_stars_repo_name: Mikotochan/csders

max_issues_repo_name: Mikotochan/csders

max_forks_repo_name: Mikotochan/csders


text:
module AbsurdLam where

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

data Fin : Nat -> Set where
  fzero : forall {n} -> Fin (suc n)
  fsuc  : forall {n} -> Fin n -> Fin (suc n)

data False : Set where

elimFalse : (A : Set) -> False -> A
elimFalse A = \()

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

magic : forall {n} -> suc n == zero -> False
magic = \()

hidden : Nat -> {x : Fin zero} -> False
hidden = \n {}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module UnequalRelevance where

postulate
  A : Set
  f : .A -> A
  g : (A -> A) -> A -> A

-- this should fail because
-- cannot use irrelevant function where relevant is needed
h : A -> A
h = g f  -- error: function types are not equal because one is relevant and the other not

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

module Properties.TypeSaturation where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Either using (Either; Left; Right)
open import Luau.Subtyping using (Tree; Language; ¬Language; _<:_; _≮:_; witness; scalar; function; function-err; function-ok; function-ok₁; function-ok₂; scalar-function; _,_; never)
open import Luau.Type using (Type; _⇒_; _∩_; _∪_; never; unknown)
open import Luau.TypeNormalization using (_∩ⁿ_; _∪ⁿ_)
open import Luau.TypeSaturation using (_⋓_; _⋒_; _∩ᵘ_; _∩ⁱ_; ∪-saturate; ∩-saturate; saturate)
open import Properties.Subtyping using (dec-language; language-comp; <:-impl-⊇; <:-refl; <:-trans; <:-trans-≮:; <:-impl-¬≮: ; <:-never; <:-unknown; <:-function; <:-union; <:-∪-symm; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∪-assocl; <:-∪-assocr; <:-intersect; <:-∩-symm; <:-∩-left; <:-∩-right; <:-∩-glb; ≮:-function-left; ≮:-function-right; <:-function-∩-∪; <:-function-∩-∩; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
open import Properties.TypeNormalization using (Normal; FunType; _⇒_; _∩_; _∪_; never; unknown; normal-∪ⁿ; normal-∩ⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.Functions using (_∘_)

-- Saturation preserves normalization
normal-⋒ : ∀ {F G} → FunType F → FunType G → FunType (F ⋒ G)
normal-⋒ (R ⇒ S) (T ⇒ U) = (normal-∩ⁿ R T) ⇒ (normal-∩ⁿ S U)
normal-⋒ (R ⇒ S) (G ∩ H) = normal-⋒ (R ⇒ S) G ∩ normal-⋒ (R ⇒ S) H
normal-⋒ (E ∩ F) G = normal-⋒ E G ∩ normal-⋒ F G

normal-⋓ : ∀ {F G} → FunType F → FunType G → FunType (F ⋓ G)
normal-⋓ (R ⇒ S) (T ⇒ U) = (normal-∪ⁿ R T) ⇒ (normal-∪ⁿ S U)
normal-⋓ (R ⇒ S) (G ∩ H) = normal-⋓ (R ⇒ S) G ∩ normal-⋓ (R ⇒ S) H
normal-⋓ (E ∩ F) G = normal-⋓ E G ∩ normal-⋓ F G

normal-∩-saturate : ∀ {F} → FunType F → FunType (∩-saturate F)
normal-∩-saturate (S ⇒ T) = S ⇒ T
normal-∩-saturate (F ∩ G) = (normal-∩-saturate F ∩ normal-∩-saturate G) ∩ normal-⋒ (normal-∩-saturate F) (normal-∩-saturate G)

normal-∪-saturate : ∀ {F} → FunType F → FunType (∪-saturate F)
normal-∪-saturate (S ⇒ T) = S ⇒ T
normal-∪-saturate (F ∩ G) = (normal-∪-saturate F ∩ normal-∪-saturate G) ∩ normal-⋓ (normal-∪-saturate F) (normal-∪-saturate G)

normal-saturate : ∀ {F} → FunType F → FunType (saturate F)
normal-saturate F = normal-∪-saturate (normal-∩-saturate F)

-- Saturation resects subtyping
∪-saturate-<: : ∀ {F} → FunType F → ∪-saturate F <: F
∪-saturate-<: (S ⇒ T) = <:-refl
∪-saturate-<: (F ∩ G) = <:-trans <:-∩-left (<:-intersect (∪-saturate-<: F) (∪-saturate-<: G))

∩-saturate-<: : ∀ {F} → FunType F → ∩-saturate F <: F
∩-saturate-<: (S ⇒ T) = <:-refl
∩-saturate-<: (F ∩ G) = <:-trans <:-∩-left (<:-intersect (∩-saturate-<: F) (∩-saturate-<: G))

saturate-<: : ∀ {F} → FunType F → saturate F <: F
saturate-<: F = <:-trans (∪-saturate-<: (normal-∩-saturate F)) (∩-saturate-<: F)

∩-<:-⋓ : ∀ {F G} → FunType F → FunType G → (F ∩ G) <: (F ⋓ G)
∩-<:-⋓ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∩-∪ (<:-function (∪ⁿ-<:-∪ R T) (∪-<:-∪ⁿ S U))
∩-<:-⋓ (R ⇒ S) (G ∩ H) = <:-trans (<:-∩-glb (<:-intersect <:-refl <:-∩-left) (<:-intersect <:-refl <:-∩-right)) (<:-intersect (∩-<:-⋓ (R ⇒ S) G) (∩-<:-⋓ (R ⇒ S) H))
∩-<:-⋓ (E ∩ F) G = <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-intersect <:-∩-right <:-refl)) (<:-intersect (∩-<:-⋓ E G) (∩-<:-⋓ F G))

∩-<:-⋒ : ∀ {F G} → FunType F → FunType G → (F ∩ G) <: (F ⋒ G)
∩-<:-⋒ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∩-∩ (<:-function (∩ⁿ-<:-∩ R T) (∩-<:-∩ⁿ S U))
∩-<:-⋒ (R ⇒ S) (G ∩ H) = <:-trans (<:-∩-glb (<:-intersect <:-refl <:-∩-left) (<:-intersect <:-refl <:-∩-right)) (<:-intersect (∩-<:-⋒ (R ⇒ S) G) (∩-<:-⋒ (R ⇒ S) H))
∩-<:-⋒ (E ∩ F) G = <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-intersect <:-∩-right <:-refl)) (<:-intersect (∩-<:-⋒ E G) (∩-<:-⋒ F G))

<:-∪-saturate : ∀ {F} → FunType F → F <: ∪-saturate F
<:-∪-saturate (S ⇒ T) = <:-refl
<:-∪-saturate (F ∩ G) = <:-∩-glb (<:-intersect (<:-∪-saturate F) (<:-∪-saturate G)) (<:-trans (<:-intersect (<:-∪-saturate F) (<:-∪-saturate G)) (∩-<:-⋓ (normal-∪-saturate F) (normal-∪-saturate G)))

<:-∩-saturate : ∀ {F} → FunType F → F <: ∩-saturate F
<:-∩-saturate (S ⇒ T) = <:-refl
<:-∩-saturate (F ∩ G) = <:-∩-glb (<:-intersect (<:-∩-saturate F) (<:-∩-saturate G)) (<:-trans (<:-intersect (<:-∩-saturate F) (<:-∩-saturate G)) (∩-<:-⋒ (normal-∩-saturate F) (normal-∩-saturate G)))

<:-saturate : ∀ {F} → FunType F → F <: saturate F
<:-saturate F = <:-trans (<:-∩-saturate F) (<:-∪-saturate (normal-∩-saturate F))

-- Overloads F is the set of overloads of F
data Overloads : Type → Type → Set where

   here : ∀ {S T} → Overloads (S ⇒ T) (S ⇒ T)
   left : ∀ {S T F G} → Overloads F (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T)
   right : ∀ {S T F G} → Overloads G (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T)

normal-overload-src : ∀ {F S T} → FunType F → Overloads F (S ⇒ T) → Normal S
normal-overload-src (S ⇒ T) here = S
normal-overload-src (F ∩ G) (left o) = normal-overload-src F o
normal-overload-src (F ∩ G) (right o) = normal-overload-src G o

normal-overload-tgt : ∀ {F S T} → FunType F → Overloads F (S ⇒ T) → Normal T
normal-overload-tgt (S ⇒ T) here = T
normal-overload-tgt (F ∩ G) (left o) = normal-overload-tgt F o
normal-overload-tgt (F ∩ G) (right o) = normal-overload-tgt G o

-- An inductive presentation of the overloads of F ⋓ G
data ∪-Lift (P Q : Type → Set) : Type → Set where

  union : ∀ {R S T U} →

    P (R ⇒ S) →
    Q (T ⇒ U) →
    --------------------
    ∪-Lift P Q ((R ∪ T) ⇒ (S ∪ U))

-- An inductive presentation of the overloads of F ⋒ G
data ∩-Lift (P Q : Type → Set) : Type → Set where

  intersect : ∀ {R S T U} →

    P (R ⇒ S) →
    Q (T ⇒ U) →
    --------------------
    ∩-Lift P Q ((R ∩ T) ⇒ (S ∩ U))

-- An inductive presentation of the overloads of ∪-saturate F
data ∪-Saturate (P : Type → Set) : Type → Set where

  base : ∀ {S T} →

    P (S ⇒ T) →
    --------------------
    ∪-Saturate P (S ⇒ T)

  union : ∀ {R S T U} →

    ∪-Saturate P (R ⇒ S) →
    ∪-Saturate P (T ⇒ U) →
    --------------------
    ∪-Saturate P ((R ∪ T) ⇒ (S ∪ U))

-- An inductive presentation of the overloads of ∩-saturate F
data ∩-Saturate (P : Type → Set) : Type → Set where

  base : ∀ {S T} →

    P (S ⇒ T) →
    --------------------
    ∩-Saturate P (S ⇒ T)

  intersect : ∀ {R S T U} →

    ∩-Saturate P (R ⇒ S) →
    ∩-Saturate P (T ⇒ U) →
    --------------------
    ∩-Saturate P ((R ∩ T) ⇒ (S ∩ U))

-- The <:-up-closure of a set of function types
data <:-Close (P : Type → Set) : Type → Set where

  defn : ∀ {R S T U} →

    P (S ⇒ T) →
    R <: S →
    T <: U →
    ------------------
    <:-Close P (R ⇒ U)

-- F ⊆ᵒ G whenever every overload of F is an overload of G
_⊆ᵒ_ : Type → Type → Set
F ⊆ᵒ G = ∀ {S T} → Overloads F (S ⇒ T) → Overloads G (S ⇒ T)

-- F <:ᵒ G when every overload of G is a supertype of an overload of F
_<:ᵒ_ : Type → Type → Set
_<:ᵒ_ F G = ∀ {S T} → Overloads G (S ⇒ T) → <:-Close (Overloads F) (S ⇒ T)

-- P ⊂: Q when any type in P is a subtype of some type in Q
_⊂:_ : (Type → Set) → (Type → Set) → Set
P ⊂: Q = ∀ {S T} → P (S ⇒ T) → <:-Close Q (S ⇒ T)

-- <:-Close is a monad
just : ∀ {P S T} → P (S ⇒ T) → <:-Close P (S ⇒ T)
just p = defn p <:-refl <:-refl

infixl 5 _>>=_ _>>=ˡ_ _>>=ʳ_
_>>=_ : ∀ {P Q S T} → <:-Close P (S ⇒ T) → (P ⊂: Q) → <:-Close Q (S ⇒ T)
(defn p p₁ p₂) >>= P⊂Q with P⊂Q p
(defn p p₁ p₂) >>= P⊂Q | defn q q₁ q₂ = defn q (<:-trans p₁ q₁) (<:-trans q₂ p₂)

_>>=ˡ_ : ∀ {P R S T} → <:-Close P (S ⇒ T) → (R <: S) → <:-Close P (R ⇒ T)
(defn p p₁ p₂) >>=ˡ q = defn p (<:-trans q p₁) p₂

_>>=ʳ_ : ∀ {P S T U} → <:-Close P (S ⇒ T) → (T <: U) → <:-Close P (S ⇒ U)
(defn p p₁ p₂) >>=ʳ q = defn p p₁ (<:-trans p₂ q)

-- Properties of ⊂:
⊂:-refl : ∀ {P} → P ⊂: P
⊂:-refl p = just p

_[∪]_ : ∀ {P Q R S T U} → <:-Close P (R ⇒ S) → <:-Close Q (T ⇒ U) → <:-Close (∪-Lift P Q) ((R ∪ T) ⇒ (S ∪ U))
(defn p p₁ p₂) [∪] (defn q q₁ q₂) = defn (union p q) (<:-union p₁ q₁) (<:-union p₂ q₂)

_[∩]_ : ∀ {P Q R S T U} → <:-Close P (R ⇒ S) → <:-Close Q (T ⇒ U) → <:-Close (∩-Lift P Q) ((R ∩ T) ⇒ (S ∩ U))
(defn p p₁ p₂) [∩] (defn q q₁ q₂) = defn (intersect p q) (<:-intersect p₁ q₁) (<:-intersect p₂ q₂)

⊂:-∩-saturate-inj : ∀ {P} → P ⊂: ∩-Saturate P
⊂:-∩-saturate-inj p = defn (base p) <:-refl <:-refl

⊂:-∪-saturate-inj : ∀ {P} → P ⊂: ∪-Saturate P
⊂:-∪-saturate-inj p = just (base p)

⊂:-∩-lift-saturate : ∀ {P} → ∩-Lift (∩-Saturate P) (∩-Saturate P) ⊂: ∩-Saturate P
⊂:-∩-lift-saturate (intersect p q) = just (intersect p q)

⊂:-∪-lift-saturate : ∀ {P} → ∪-Lift (∪-Saturate P) (∪-Saturate P) ⊂: ∪-Saturate P
⊂:-∪-lift-saturate (union p q) = just (union p q)

⊂:-∩-lift : ∀ {P Q R S} → (P ⊂: Q) → (R ⊂: S) → (∩-Lift P R ⊂: ∩-Lift Q S)
⊂:-∩-lift P⊂Q R⊂S (intersect n o) = P⊂Q n [∩] R⊂S o

⊂:-∪-lift : ∀ {P Q R S} → (P ⊂: Q) → (R ⊂: S) → (∪-Lift P R ⊂: ∪-Lift Q S)
⊂:-∪-lift P⊂Q R⊂S (union n o) = P⊂Q n [∪] R⊂S o

⊂:-∩-saturate : ∀ {P Q} → (P ⊂: Q) → (∩-Saturate P ⊂: ∩-Saturate Q)
⊂:-∩-saturate P⊂Q (base p) = P⊂Q p >>= ⊂:-∩-saturate-inj
⊂:-∩-saturate P⊂Q (intersect p q) = (⊂:-∩-saturate P⊂Q p [∩] ⊂:-∩-saturate P⊂Q q) >>= ⊂:-∩-lift-saturate

⊂:-∪-saturate : ∀ {P Q} → (P ⊂: Q) → (∪-Saturate P ⊂: ∪-Saturate Q)
⊂:-∪-saturate P⊂Q (base p) = P⊂Q p >>= ⊂:-∪-saturate-inj
⊂:-∪-saturate P⊂Q (union p q) = (⊂:-∪-saturate P⊂Q p [∪] ⊂:-∪-saturate P⊂Q q) >>= ⊂:-∪-lift-saturate

⊂:-∩-saturate-indn : ∀ {P Q} → (P ⊂: Q) → (∩-Lift Q Q ⊂: Q) → (∩-Saturate P ⊂: Q)
⊂:-∩-saturate-indn P⊂Q QQ⊂Q (base p) = P⊂Q p
⊂:-∩-saturate-indn P⊂Q QQ⊂Q (intersect p q) = (⊂:-∩-saturate-indn P⊂Q QQ⊂Q p [∩] ⊂:-∩-saturate-indn P⊂Q QQ⊂Q q) >>= QQ⊂Q

⊂:-∪-saturate-indn : ∀ {P Q} → (P ⊂: Q) → (∪-Lift Q Q ⊂: Q) → (∪-Saturate P ⊂: Q)
⊂:-∪-saturate-indn P⊂Q QQ⊂Q (base p) = P⊂Q p
⊂:-∪-saturate-indn P⊂Q QQ⊂Q (union p q) = (⊂:-∪-saturate-indn P⊂Q QQ⊂Q p [∪] ⊂:-∪-saturate-indn P⊂Q QQ⊂Q q) >>= QQ⊂Q

∪-saturate-resp-∩-saturation : ∀ {P} → (∩-Lift P P ⊂: P) → (∩-Lift (∪-Saturate P) (∪-Saturate P) ⊂: ∪-Saturate P)
∪-saturate-resp-∩-saturation ∩P⊂P (intersect (base p) (base q)) = ∩P⊂P (intersect p q) >>= ⊂:-∪-saturate-inj
∪-saturate-resp-∩-saturation ∩P⊂P (intersect p (union q q₁)) = (∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q) [∪] ∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q₁)) >>= ⊂:-∪-lift-saturate >>=ˡ <:-∩-distl-∪ >>=ʳ ∩-distl-∪-<:
∪-saturate-resp-∩-saturation ∩P⊂P (intersect (union p p₁) q) = (∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q) [∪] ∪-saturate-resp-∩-saturation ∩P⊂P (intersect p₁ q)) >>= ⊂:-∪-lift-saturate >>=ˡ <:-∩-distr-∪ >>=ʳ ∩-distr-∪-<:

ov-language : ∀ {F t} → FunType F → (∀ {S T} → Overloads F (S ⇒ T) → Language (S ⇒ T) t) → Language F t
ov-language (S ⇒ T) p = p here
ov-language (F ∩ G) p = (ov-language F (p ∘ left) , ov-language G (p ∘ right))

ov-<: : ∀ {F R S T U} → FunType F → Overloads F (R ⇒ S) → ((R ⇒ S) <: (T ⇒ U)) → F <: (T ⇒ U)
ov-<: F here p = p
ov-<: (F ∩ G) (left o) p = <:-trans <:-∩-left (ov-<: F o p)
ov-<: (F ∩ G) (right o) p = <:-trans <:-∩-right (ov-<: G o p)

<:ᵒ-impl-<: : ∀ {F G} → FunType F → FunType G → (F <:ᵒ G) → (F <: G)
<:ᵒ-impl-<: F (T ⇒ U) F<G with F<G here
<:ᵒ-impl-<: F (T ⇒ U) F<G | defn o o₁ o₂ = ov-<: F o (<:-function o₁ o₂)
<:ᵒ-impl-<: F (G ∩ H) F<G = <:-∩-glb (<:ᵒ-impl-<: F G (F<G ∘ left)) (<:ᵒ-impl-<: F H (F<G ∘ right))

⊂:-overloads-left : ∀ {F G} → Overloads F ⊂: Overloads (F ∩ G)
⊂:-overloads-left p = just (left p)

⊂:-overloads-right : ∀ {F G} → Overloads G ⊂: Overloads (F ∩ G)
⊂:-overloads-right p = just (right p)

⊂:-overloads-⋒ : ∀ {F G} → FunType F → FunType G → ∩-Lift (Overloads F) (Overloads G) ⊂: Overloads (F ⋒ G)
⊂:-overloads-⋒ (R ⇒ S) (T ⇒ U) (intersect here here) = defn here (∩-<:-∩ⁿ R T) (∩ⁿ-<:-∩ S U)
⊂:-overloads-⋒ (R ⇒ S) (G ∩ H) (intersect here (left o)) = ⊂:-overloads-⋒ (R ⇒ S) G (intersect here o) >>= ⊂:-overloads-left
⊂:-overloads-⋒ (R ⇒ S) (G ∩ H) (intersect here (right o)) = ⊂:-overloads-⋒ (R ⇒ S) H (intersect here o) >>= ⊂:-overloads-right
⊂:-overloads-⋒ (E ∩ F) G (intersect (left n) o) = ⊂:-overloads-⋒ E G (intersect n o) >>= ⊂:-overloads-left
⊂:-overloads-⋒ (E ∩ F) G (intersect (right n) o) = ⊂:-overloads-⋒ F G (intersect n o) >>= ⊂:-overloads-right

⊂:-⋒-overloads : ∀ {F G} → FunType F → FunType G → Overloads (F ⋒ G) ⊂: ∩-Lift (Overloads F) (Overloads G)
⊂:-⋒-overloads (R ⇒ S) (T ⇒ U) here = defn (intersect here here) (∩ⁿ-<:-∩ R T) (∩-<:-∩ⁿ S U)
⊂:-⋒-overloads (R ⇒ S) (G ∩ H) (left o) = ⊂:-⋒-overloads (R ⇒ S) G o >>= ⊂:-∩-lift ⊂:-refl ⊂:-overloads-left
⊂:-⋒-overloads (R ⇒ S) (G ∩ H) (right o) = ⊂:-⋒-overloads (R ⇒ S) H o >>= ⊂:-∩-lift ⊂:-refl ⊂:-overloads-right
⊂:-⋒-overloads (E ∩ F) G (left o) = ⊂:-⋒-overloads E G o >>= ⊂:-∩-lift ⊂:-overloads-left ⊂:-refl
⊂:-⋒-overloads (E ∩ F) G (right o) = ⊂:-⋒-overloads F G o >>= ⊂:-∩-lift ⊂:-overloads-right ⊂:-refl

⊂:-overloads-⋓ : ∀ {F G} → FunType F → FunType G → ∪-Lift (Overloads F) (Overloads G) ⊂: Overloads (F ⋓ G)
⊂:-overloads-⋓ (R ⇒ S) (T ⇒ U) (union here here) = defn here (∪-<:-∪ⁿ R T) (∪ⁿ-<:-∪ S U)
⊂:-overloads-⋓ (R ⇒ S) (G ∩ H) (union here (left o)) = ⊂:-overloads-⋓ (R ⇒ S) G (union here o) >>= ⊂:-overloads-left
⊂:-overloads-⋓ (R ⇒ S) (G ∩ H) (union here (right o)) = ⊂:-overloads-⋓ (R ⇒ S) H (union here o) >>= ⊂:-overloads-right
⊂:-overloads-⋓ (E ∩ F) G (union (left n) o) = ⊂:-overloads-⋓ E G (union n o) >>= ⊂:-overloads-left
⊂:-overloads-⋓ (E ∩ F) G (union (right n) o) = ⊂:-overloads-⋓ F G (union n o) >>= ⊂:-overloads-right

⊂:-⋓-overloads : ∀ {F G} → FunType F → FunType G → Overloads (F ⋓ G) ⊂: ∪-Lift (Overloads F) (Overloads G)
⊂:-⋓-overloads (R ⇒ S) (T ⇒ U) here = defn (union here here) (∪ⁿ-<:-∪ R T) (∪-<:-∪ⁿ S U)
⊂:-⋓-overloads (R ⇒ S) (G ∩ H) (left o) = ⊂:-⋓-overloads (R ⇒ S) G o >>= ⊂:-∪-lift ⊂:-refl ⊂:-overloads-left
⊂:-⋓-overloads (R ⇒ S) (G ∩ H) (right o) = ⊂:-⋓-overloads (R ⇒ S) H o >>= ⊂:-∪-lift ⊂:-refl ⊂:-overloads-right
⊂:-⋓-overloads (E ∩ F) G (left o) = ⊂:-⋓-overloads E G o >>= ⊂:-∪-lift ⊂:-overloads-left ⊂:-refl
⊂:-⋓-overloads (E ∩ F) G (right o) = ⊂:-⋓-overloads F G o >>= ⊂:-∪-lift ⊂:-overloads-right ⊂:-refl

∪-saturate-overloads : ∀ {F} → FunType F → Overloads (∪-saturate F) ⊂: ∪-Saturate (Overloads F)
∪-saturate-overloads (S ⇒ T) here = just (base here)
∪-saturate-overloads (F ∩ G) (left (left o)) = ∪-saturate-overloads F o >>= ⊂:-∪-saturate ⊂:-overloads-left
∪-saturate-overloads (F ∩ G) (left (right o)) = ∪-saturate-overloads G o >>= ⊂:-∪-saturate ⊂:-overloads-right
∪-saturate-overloads (F ∩ G) (right o) =
  ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) o >>=
  ⊂:-∪-lift (∪-saturate-overloads F) (∪-saturate-overloads G) >>=
  ⊂:-∪-lift (⊂:-∪-saturate ⊂:-overloads-left) (⊂:-∪-saturate ⊂:-overloads-right) >>=
  ⊂:-∪-lift-saturate

overloads-∪-saturate : ∀ {F} → FunType F → ∪-Saturate (Overloads F) ⊂: Overloads (∪-saturate F)
overloads-∪-saturate F = ⊂:-∪-saturate-indn (inj F) (step F) where

  inj : ∀ {F} → FunType F → Overloads F ⊂: Overloads (∪-saturate F)
  inj (S ⇒ T) here = just here
  inj (F ∩ G) (left p) = inj F p >>= ⊂:-overloads-left >>= ⊂:-overloads-left
  inj (F ∩ G) (right p) = inj G p >>= ⊂:-overloads-right >>= ⊂:-overloads-left

  step : ∀ {F} → FunType F → ∪-Lift (Overloads (∪-saturate F)) (Overloads (∪-saturate F)) ⊂: Overloads (∪-saturate F)
  step (S ⇒ T) (union here here) = defn here (<:-∪-lub <:-refl <:-refl) <:-∪-left
  step (F ∩ G) (union (left (left p)) (left (left q))) = step F (union p q) >>= ⊂:-overloads-left >>= ⊂:-overloads-left
  step (F ∩ G) (union (left (left p)) (left (right q))) = ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) (union p q) >>= ⊂:-overloads-right
  step (F ∩ G) (union (left (right p)) (left (left q))) = ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) (union q p) >>= ⊂:-overloads-right >>=ˡ <:-∪-symm >>=ʳ <:-∪-symm
  step (F ∩ G) (union (left (right p)) (left (right q))) = step G (union p q) >>= ⊂:-overloads-right >>= ⊂:-overloads-left
  step (F ∩ G) (union p (right q)) with ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) q
  step (F ∩ G) (union (left (left p)) (right q)) | defn (union q₁ q₂) q₃ q₄ =
    (step F (union p q₁) [∪] just q₂) >>=
    ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-union <:-refl q₃) <:-∪-assocl >>=ʳ
    <:-trans <:-∪-assocr (<:-union <:-refl q₄)
  step (F ∩ G) (union (left (right p)) (right q)) | defn (union q₁ q₂) q₃ q₄ =
    (just q₁ [∪] step G (union p q₂)) >>=
    ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-union <:-refl q₃) (<:-∪-lub (<:-trans <:-∪-left <:-∪-right) (<:-∪-lub <:-∪-left (<:-trans <:-∪-right <:-∪-right))) >>=ʳ
    <:-trans (<:-∪-lub (<:-trans <:-∪-left <:-∪-right) (<:-∪-lub <:-∪-left (<:-trans <:-∪-right <:-∪-right))) (<:-union <:-refl q₄)
  step (F ∩ G) (union (right p) (right q)) | defn (union q₁ q₂) q₃ q₄ with ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) p
  step (F ∩ G) (union (right p) (right q)) | defn (union q₁ q₂) q₃ q₄ | defn (union p₁ p₂) p₃ p₄ =
    (step F (union p₁ q₁) [∪] step G (union p₂ q₂)) >>=
    ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-union p₃ q₃) (<:-∪-lub (<:-union <:-∪-left <:-∪-left) (<:-union <:-∪-right <:-∪-right)) >>=ʳ
    <:-trans (<:-∪-lub (<:-union <:-∪-left <:-∪-left) (<:-union <:-∪-right <:-∪-right)) (<:-union p₄ q₄)
  step (F ∩ G) (union (right p) q) with ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) p
  step (F ∩ G) (union (right p) (left (left q))) | defn (union p₁ p₂) p₃ p₄ =
    (step F (union p₁ q) [∪] just p₂) >>=
    ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-union p₃ <:-refl) (<:-∪-lub (<:-union <:-∪-left <:-refl) (<:-trans <:-∪-right <:-∪-left)) >>=ʳ
    <:-trans (<:-∪-lub (<:-union <:-∪-left <:-refl) (<:-trans <:-∪-right <:-∪-left)) (<:-union p₄ <:-refl)
  step (F ∩ G) (union (right p) (left (right q))) | defn (union p₁ p₂) p₃ p₄ =
    (just p₁ [∪] step G (union p₂ q)) >>=
    ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-union p₃ <:-refl) <:-∪-assocr >>=ʳ
    <:-trans <:-∪-assocl (<:-union p₄ <:-refl)
  step (F ∩ G) (union (right p) (right q)) | defn (union p₁ p₂) p₃ p₄ with ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) q
  step (F ∩ G) (union (right p) (right q)) | defn (union p₁ p₂) p₃ p₄ | defn (union q₁ q₂) q₃ q₄ =
    (step F (union p₁ q₁) [∪] step G (union p₂ q₂)) >>=
    ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-union p₃ q₃) (<:-∪-lub (<:-union <:-∪-left <:-∪-left) (<:-union <:-∪-right <:-∪-right)) >>=ʳ
    <:-trans (<:-∪-lub (<:-union <:-∪-left <:-∪-left) (<:-union <:-∪-right <:-∪-right)) (<:-union p₄ q₄)

∪-saturated : ∀ {F} → FunType F → ∪-Lift (Overloads (∪-saturate F)) (Overloads (∪-saturate F)) ⊂: Overloads (∪-saturate F)
∪-saturated F o =
  ⊂:-∪-lift (∪-saturate-overloads F) (∪-saturate-overloads F) o >>=
  ⊂:-∪-lift-saturate >>=
  overloads-∪-saturate F

∩-saturate-overloads : ∀ {F} → FunType F → Overloads (∩-saturate F) ⊂: ∩-Saturate (Overloads F)
∩-saturate-overloads (S ⇒ T) here = just (base here)
∩-saturate-overloads (F ∩ G) (left (left o)) = ∩-saturate-overloads F o >>= ⊂:-∩-saturate ⊂:-overloads-left
∩-saturate-overloads (F ∩ G) (left (right o)) = ∩-saturate-overloads G o >>= ⊂:-∩-saturate ⊂:-overloads-right
∩-saturate-overloads (F ∩ G) (right o) =
  ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) o >>=
  ⊂:-∩-lift (∩-saturate-overloads F) (∩-saturate-overloads G) >>=
  ⊂:-∩-lift (⊂:-∩-saturate ⊂:-overloads-left) (⊂:-∩-saturate ⊂:-overloads-right) >>=
  ⊂:-∩-lift-saturate

overloads-∩-saturate : ∀ {F} → FunType F → ∩-Saturate (Overloads F) ⊂: Overloads (∩-saturate F)
overloads-∩-saturate F = ⊂:-∩-saturate-indn (inj F) (step F) where

  inj :  ∀ {F} → FunType F → Overloads F ⊂: Overloads (∩-saturate F)
  inj (S ⇒ T) here = just here
  inj (F ∩ G) (left p) = inj F p >>= ⊂:-overloads-left >>= ⊂:-overloads-left
  inj (F ∩ G) (right p) = inj G p >>= ⊂:-overloads-right >>= ⊂:-overloads-left

  step : ∀ {F} → FunType F → ∩-Lift (Overloads (∩-saturate F)) (Overloads (∩-saturate F)) ⊂: Overloads (∩-saturate F)
  step (S ⇒ T) (intersect here here) = defn here <:-∩-left (<:-∩-glb <:-refl <:-refl)
  step (F ∩ G) (intersect (left (left p)) (left (left q))) = step F (intersect p q) >>= ⊂:-overloads-left >>= ⊂:-overloads-left
  step (F ∩ G) (intersect (left (left p)) (left (right q))) = ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) (intersect p q) >>= ⊂:-overloads-right
  step (F ∩ G) (intersect (left (right p)) (left (left q))) = ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) (intersect q p) >>= ⊂:-overloads-right >>=ˡ <:-∩-symm >>=ʳ <:-∩-symm
  step (F ∩ G) (intersect (left (right p)) (left (right q))) = step G (intersect p q) >>= ⊂:-overloads-right >>= ⊂:-overloads-left
  step (F ∩ G) (intersect (right p) q) with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) p
  step (F ∩ G) (intersect (right p) (left (left q))) | defn (intersect p₁ p₂) p₃ p₄ =
    (step F (intersect p₁ q) [∩] just p₂) >>=
    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-intersect p₃ <:-refl) (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-trans <:-∩-left <:-∩-right)) >>=ʳ
    <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-trans <:-∩-left <:-∩-right)) (<:-intersect p₄ <:-refl)
  step (F ∩ G) (intersect (right p) (left (right q))) | defn (intersect p₁ p₂) p₃ p₄ =
    (just p₁ [∩] step G (intersect p₂ q)) >>=
    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-intersect p₃ <:-refl) <:-∩-assocr >>=ʳ
    <:-trans <:-∩-assocl (<:-intersect p₄ <:-refl)
  step (F ∩ G) (intersect (right p) (right q)) | defn (intersect p₁ p₂) p₃ p₄ with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) q
  step (F ∩ G) (intersect (right p) (right q)) | defn (intersect p₁ p₂) p₃ p₄ | defn (intersect q₁ q₂) q₃ q₄ =
    (step F (intersect p₁ q₁) [∩] step G (intersect p₂ q₂)) >>=
    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-intersect p₃ q₃) (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) >>=ʳ
    <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) (<:-intersect p₄ q₄)
  step (F ∩ G) (intersect p (right q)) with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) q
  step (F ∩ G) (intersect (left (left p)) (right q)) | defn (intersect q₁ q₂) q₃ q₄ =
    (step F (intersect p q₁) [∩] just q₂) >>=
    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-intersect <:-refl q₃) <:-∩-assocl >>=ʳ
    <:-trans <:-∩-assocr (<:-intersect <:-refl q₄)
  step (F ∩ G) (intersect (left (right p)) (right q)) | defn (intersect q₁ q₂) q₃ q₄ =
    (just q₁ [∩] step G (intersect p q₂) ) >>=
    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-intersect <:-refl q₃) (<:-∩-glb (<:-trans <:-∩-right <:-∩-left) (<:-∩-glb <:-∩-left (<:-trans <:-∩-right <:-∩-right))) >>=ʳ
    <:-∩-glb (<:-trans <:-∩-right <:-∩-left) (<:-trans (<:-∩-glb <:-∩-left (<:-trans <:-∩-right <:-∩-right)) q₄)
  step (F ∩ G) (intersect (right p) (right q)) | defn (intersect q₁ q₂) q₃ q₄ with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) p
  step (F ∩ G) (intersect (right p) (right q)) | defn (intersect q₁ q₂) q₃ q₄ | defn (intersect p₁ p₂) p₃ p₄ =
    (step F (intersect p₁ q₁) [∩] step G (intersect p₂ q₂)) >>=
    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
    ⊂:-overloads-right >>=ˡ
    <:-trans (<:-intersect p₃ q₃) (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) >>=ʳ
    <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) (<:-intersect p₄ q₄)

saturate-overloads : ∀ {F} → FunType F → Overloads (saturate F) ⊂: ∪-Saturate (∩-Saturate (Overloads F))
saturate-overloads F o = ∪-saturate-overloads (normal-∩-saturate F) o >>= (⊂:-∪-saturate (∩-saturate-overloads F))

overloads-saturate : ∀ {F} → FunType F → ∪-Saturate (∩-Saturate (Overloads F)) ⊂: Overloads (saturate F)
overloads-saturate F o = ⊂:-∪-saturate (overloads-∩-saturate F) o >>= overloads-∪-saturate (normal-∩-saturate F)

-- Saturated F whenever
-- * if F has overloads (R ⇒ S) and (T ⇒ U) then F has an overload which is a subtype of ((R ∩ T) ⇒ (S ∩ U))
-- * ditto union
data Saturated (F : Type) : Set where

  defn :

    (∀ {R S T U} → Overloads F (R ⇒ S) → Overloads F (T ⇒ U) → <:-Close (Overloads F) ((R ∩ T) ⇒ (S ∩ U))) →
    (∀ {R S T U} → Overloads F (R ⇒ S) → Overloads F (T ⇒ U) → <:-Close (Overloads F) ((R ∪ T) ⇒ (S ∪ U))) →
    -----------
    Saturated F

-- saturated F is saturated!
saturated : ∀ {F} → FunType F → Saturated (saturate F)
saturated F = defn
  (λ n o → (saturate-overloads F n [∩] saturate-overloads F o) >>= ∪-saturate-resp-∩-saturation ⊂:-∩-lift-saturate >>= overloads-saturate F)
  (λ n o → ∪-saturated (normal-∩-saturate F) (union n o))

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


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

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

module Reflection.Pattern where

open import Data.List.Base hiding (_++_)
open import Data.List.Properties
open import Data.Product
open import Data.String as String using (String; braces; parens; _++_; _<+>_)
import Reflection.Literal as Literal
import Reflection.Name as Name
open import Relation.Nullary
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Reflection.Argument
open import Reflection.Argument.Visibility using (Visibility); open Visibility
open import Reflection.Argument.Relevance using (Relevance); open Relevance
open import Reflection.Argument.Information using (ArgInfo); open ArgInfo

------------------------------------------------------------------------
-- Re-exporting the builtin type and constructors

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

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

con-injective₁ : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′
con-injective₁ refl = refl

con-injective₂ : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → args ≡ args′
con-injective₂ refl = refl

con-injective : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′ × args ≡ args′
con-injective = < con-injective₁ , con-injective₂ >

var-injective : ∀ {x y} → var x ≡ var y → x ≡ y
var-injective refl = refl

lit-injective : ∀ {x y} → Pattern.lit x ≡ lit y → x ≡ y
lit-injective refl = refl

proj-injective : ∀ {x y} → proj x ≡ proj y → x ≡ y
proj-injective refl = refl

_≟s_ : Decidable (_≡_ {A = Args Pattern})
_≟_  : Decidable (_≡_ {A = Pattern})

con c ps ≟ con c′ ps′ = Dec.map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×-dec ps ≟s ps′)
var s    ≟ var s′     = Dec.map′ (cong var) var-injective (s String.≟ s′)
lit l    ≟ lit l′     = Dec.map′ (cong lit) lit-injective (l Literal.≟ l′)
proj a   ≟ proj a′    = Dec.map′ (cong proj) proj-injective (a Name.≟ a′)

con x x₁ ≟ dot = no (λ ())
con x x₁ ≟ var x₂ = no (λ ())
con x x₁ ≟ lit x₂ = no (λ ())
con x x₁ ≟ proj x₂ = no (λ ())
con x x₁ ≟ absurd = no (λ ())
dot ≟ con x x₁ = no (λ ())
dot ≟ dot = yes refl
dot ≟ var x = no (λ ())
dot ≟ lit x = no (λ ())
dot ≟ proj x = no (λ ())
dot ≟ absurd = no (λ ())
var s ≟ con x x₁ = no (λ ())
var s ≟ dot = no (λ ())
var s ≟ lit x = no (λ ())
var s ≟ proj x = no (λ ())
var s ≟ absurd = no (λ ())
lit x ≟ con x₁ x₂ = no (λ ())
lit x ≟ dot = no (λ ())
lit x ≟ var _ = no (λ ())
lit x ≟ proj x₁ = no (λ ())
lit x ≟ absurd = no (λ ())
proj x ≟ con x₁ x₂ = no (λ ())
proj x ≟ dot = no (λ ())
proj x ≟ var _ = no (λ ())
proj x ≟ lit x₁ = no (λ ())
proj x ≟ absurd = no (λ ())
absurd ≟ con x x₁ = no (λ ())
absurd ≟ dot = no (λ ())
absurd ≟ var _ = no (λ ())
absurd ≟ lit x = no (λ ())
absurd ≟ proj x = no (λ ())
absurd ≟ absurd = yes refl

[]             ≟s []             = yes refl
(arg i p ∷ xs) ≟s (arg j q ∷ ys) = ∷-dec (unArg-dec (p ≟ q)) (xs ≟s ys)

[]      ≟s (_ ∷ _) = no λ()
(_ ∷ _) ≟s []      = no λ()


text:
module sum-thms where

open import eq
open import sum
open import list
open import product
open import empty
open import negation

inj₁-inj : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{x : A}{x'} → inj₁{ℓ}{ℓ'}{A}{B} x ≡ inj₁ x' → x ≡ x'
inj₁-inj refl = refl

⊎-assoc-iso₁ : ∀{ℓ}{U V W : Set ℓ}{x : U ⊎ V ⊎ W} → ⊎-assoc-inv (⊎-assoc x) ≡ x
⊎-assoc-iso₁ {x = inj₁ x} = refl
⊎-assoc-iso₁ {x = inj₂ (inj₁ x)} = refl
⊎-assoc-iso₁ {x = inj₂ (inj₂ y)} = refl

⊎-assoc-iso₂ : ∀{ℓ}{U V W : Set ℓ}{x : (U ⊎ V) ⊎ W} → ⊎-assoc (⊎-assoc-inv x) ≡ x
⊎-assoc-iso₂ {x = inj₁ (inj₁ x)} = refl
⊎-assoc-iso₂ {x = inj₁ (inj₂ y)} = refl
⊎-assoc-iso₂ {x = inj₂ y} = refl

⊎-left-ident-iso₁ : ∀{ℓ}{X : Set ℓ}{x} → ⊎-left-ident-inv {_}{X} (⊎-left-ident x) ≡ x
⊎-left-ident-iso₁ {x = inj₁ x} = ⊥-elim x
⊎-left-ident-iso₁ {x = inj₂ y} = refl

⊎-left-ident-iso₂ : ∀{ℓ}{X : Set ℓ}{x} → ⊎-left-ident {_}{X} (⊎-left-ident-inv x) ≡ x
⊎-left-ident-iso₂ = refl

⊎-right-ident-iso₁ : ∀{ℓ}{X : Set ℓ}{x} → ⊎-right-ident-inv {_}{X} (⊎-right-ident x) ≡ x
⊎-right-ident-iso₁ {x = inj₁ x} = refl
⊎-right-ident-iso₁ {x = inj₂ y} = ⊥-elim y

⊎-right-ident-iso₂ : ∀{ℓ}{X : Set ℓ}{x} → ⊎-right-ident {_}{X} (⊎-right-ident-inv x) ≡ x
⊎-right-ident-iso₂ = refl

¬⊎→× : ∀{ℓ}{A B : Set ℓ} → ¬ (_⊎_ {ℓ} A B) → ¬ A × ¬ B
¬⊎→× {ℓ}{A}{B} p = (λ x → p (inj₁ x)) , λ x → p (inj₂ x)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module Imports.Unsolved where

X : Set
X = ?


text:
open import Agda.Primitive

postulate
  F : (a : Level) → Set a → Set a
  P : (a : Level) (A : Set a) → F a A → Set a
  p : (a : Level) (A : Set a) (x : F a A) → P a A x
  Q : (a : Level) (A : Set a) → A → Set a

variable
  a : Level
  A : Set a

postulate
  q : (x : F _ A) → Q a _ (p a A x)

q' : {a : Level} {A : Set a} (x : F a A) → Q a (P a A x) (p a A x)
q' {a} {A} = q {a} {A}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Unary.All directly.
------------------------------------------------------------------------

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

module Data.Vec.All where

open import Data.Vec.Relation.Unary.All public


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

open import Categories.Category
open import Categories.Functor
open import Categories.Adjoint

-- Right Adjoint Preserves Limits.
module Categories.Adjoint.RAPL {o o′ ℓ ℓ′ e e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  {L : Functor C D} {R : Functor D C} (L⊣R : L ⊣ R) where

open import Categories.Functor.Properties

import Categories.Morphism.Reasoning as MR
import Categories.Diagram.Limit as Lim
import Categories.Category.Construction.Cones as Con

private
  module C = Category C
  module D = Category D
  module L = Functor L
  module R = Functor R

open Adjoint L⊣R

module _ {o″ ℓ″ e″} {J : Category o″ ℓ″ e″} (F : Functor J D) where
  private
    module F = Functor F
    module LF = Lim F
    module CF = Con F

    RF = R ∘F F

    module LRF = Lim RF
    module CRF = Con RF

  rapl : LF.Limit → LRF.Limit
  rapl lim = record
    { terminal = record
      { ⊤        = ⊤
      ; !        = !
      ; !-unique = !-unique
      }
    }
    where module lim = LF.Limit lim
          open lim

          ⊤ : CRF.Cone
          ⊤ = record
            { N    = R.F₀ apex
            ; apex = record
              { ψ       = λ X → R.F₁ (proj X)
              ; commute = λ f → [ R ]-resp-∘ (limit-commute f)
              }
            }

          K′ : CRF.Cone → CF.Cone
          K′ K = record
            { N    = L.F₀ K.N
            ; apex = record
              { ψ       = λ X → counit.η (F.F₀ X) D.∘ L.F₁ (K.ψ X)
              ; commute = λ {X Y} f → begin
                F.F₁ f D.∘ counit.η (F.F₀ X) D.∘ L.F₁ (K.ψ X)
                  ≈˘⟨ pushˡ (counit.commute (F.F₁ f)) ⟩
                (counit.η (F.F₀ Y) D.∘ L.F₁ (R.F₁ (F.F₁ f))) D.∘ L.F₁ (K.ψ X)
                  ≈⟨ pullʳ ([ L ]-resp-∘ (K.commute f)) ⟩
                counit.η (F.F₀ Y) D.∘ L.F₁ (K.ψ Y)
                  ∎
              }
            }
            where module K = CRF.Cone K
                  open D.HomReasoning
                  open MR D

          module K′ K = CF.Cone (K′ K)

          ! : ∀ {K : CRF.Cone} → CRF.Cones [ K , ⊤ ]
          ! {K} = record
            { arr     = R.F₁ (rep (K′ K)) C.∘ unit.η K.N
            ; commute = commute′
            }
            where module K = CRF.Cone K
                  commute′ : ∀ {X} → R.F₁ (proj X) C.∘ R.F₁ (rep (K′ K)) C.∘ unit.η K.N C.≈ K.ψ X
                  commute′ {X} = begin
                    R.F₁ (proj X) C.∘ R.F₁ (rep (K′ K)) C.∘ unit.η K.N
                      ≈⟨ pullˡ ([ R ]-resp-∘ commute) ⟩
                    R.F₁ (K′.ψ K X) C.∘ unit.η K.N
                      ≈⟨ LRadjunct≈id ⟩
                    K.ψ X
                      ∎
                    where open C.HomReasoning
                          open MR C

          module ! {K} = CRF.Cone⇒ (! {K})

          !-unique : ∀ {K : CRF.Cone} (f : CRF.Cones [ K , ⊤ ]) → CRF.Cones [ ! ≈ f ]
          !-unique {K} f =
            let open C.HomReasoning
                open MR C
             in begin
               R.F₁ (rep (K′ K)) C.∘ unit.η K.N ≈⟨ R.F-resp-≈ (terminal.!-unique f′) ⟩∘⟨refl ⟩
               Ladjunct (Radjunct f.arr)        ≈⟨ LRadjunct≈id ⟩
               f.arr                            ∎
            where module K = CRF.Cone K
                  module f = CRF.Cone⇒ f

                  f′ : CF.Cones [ K′ K , limit ]
                  f′ = record
                    { arr     = Radjunct f.arr
                    ; commute = λ {X} → begin
                      proj X D.∘ Radjunct f.arr                                   ≈˘⟨ pushˡ (counit.commute (proj X)) ⟩
                      (counit.η (F.F₀ X) D.∘ L.F₁ (R.F₁ (proj X))) D.∘ L.F₁ f.arr ≈˘⟨ pushʳ L.homomorphism ⟩
                      Radjunct (R.F₁ (proj X) C.∘ f.arr)                          ≈⟨ Radjunct-resp-≈ f.commute ⟩
                      Radjunct (K.ψ X)                                            ∎
                    }
                    where open D.HomReasoning
                          open MR D

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Convertibility where

open import Syntax public

-- β-η-equivalence.

infix 4 _≡ᵝᵑ_
data _≡ᵝᵑ_ : ∀ {A Γ} → Γ ⊢ A → Γ ⊢ A → Set where
  refl≡ᵝᵑ  : ∀ {A Γ} {d : Γ ⊢ A} → d ≡ᵝᵑ d

  trans≡ᵝᵑ : ∀ {A Γ} {d d′ d″ : Γ ⊢ A} → d ≡ᵝᵑ d′ → d′ ≡ᵝᵑ d″ → d ≡ᵝᵑ d″

  sym≡ᵝᵑ   : ∀ {A Γ} {d d′ : Γ ⊢ A} → d ≡ᵝᵑ d′ → d′ ≡ᵝᵑ d

  -- Congruences.

  cong≡ᵝᵑlam  : ∀ {A B Γ} {d d′ : Γ , A ⊢ B} →
                d ≡ᵝᵑ d′ → lam d ≡ᵝᵑ lam d′

  cong≡ᵝᵑapp  : ∀ {A B Γ} {d d′ : Γ ⊢ A ⇒ B} {e e′ : Γ ⊢ A} →
                d ≡ᵝᵑ d′ → e ≡ᵝᵑ e′ → app d e ≡ᵝᵑ app d′ e′

  cong≡ᵝᵑpair : ∀ {A B Γ} {d d′ : Γ ⊢ A} {e e′ : Γ ⊢ B} →
                d ≡ᵝᵑ d′ → e ≡ᵝᵑ e′ → pair d e ≡ᵝᵑ pair d′ e′

  cong≡ᵝᵑfst  : ∀ {A B Γ} {d d′ : Γ ⊢ A ⩕ B} →
                d ≡ᵝᵑ d′ → fst d ≡ᵝᵑ fst d′

  cong≡ᵝᵑsnd  : ∀ {A B Γ} {d d′ : Γ ⊢ A ⩕ B} →
                d ≡ᵝᵑ d′ → snd d ≡ᵝᵑ snd d′

  -- Reductions, or β-conversions.

  reduce⇒ : ∀ {A B Γ} → (d : Γ , A ⊢ B) (e : Γ ⊢ A) →
             app (lam d) e ≡ᵝᵑ [ top ≔ e ] d

  reduce⩕₁ : ∀ {A B Γ} → (d : Γ ⊢ A) (e : Γ ⊢ B) →
             fst (pair d e) ≡ᵝᵑ d

  reduce⩕₂ : ∀ {A B Γ} → (d : Γ ⊢ A) (e : Γ ⊢ B) →
             snd (pair d e) ≡ᵝᵑ e

  -- Expansions, or η-conversions.

  expand⇒ : ∀ {A B Γ} → (d : Γ ⊢ A ⇒ B) →
             d ≡ᵝᵑ lam (app (mono⊢ weak⊆ d) v₀)

  expand⩕  : ∀ {A B Γ} → (d : Γ ⊢ A ⩕ B) →
             d ≡ᵝᵑ pair (fst d) (snd d)

  expand⫪ : ∀ {Γ} → (d : Γ ⊢ ⫪) →
             d ≡ᵝᵑ unit

≡→≡ᵝᵑ : ∀ {A Γ} {d d′ : Γ ⊢ A} → d ≡ d′ → d ≡ᵝᵑ d′
≡→≡ᵝᵑ refl = refl≡ᵝᵑ

-- Syntax for equational reasoning with β-η-equivalence.

module ≡ᵝᵑ-Reasoning where
  infix 1 begin≡ᵝᵑ_
  begin≡ᵝᵑ_ : ∀ {A Γ} {d d′ : Γ ⊢ A} → d ≡ᵝᵑ d′ → d ≡ᵝᵑ d′
  begin≡ᵝᵑ_ p = p

  infixr 2 _≡→≡ᵝᵑ⟨⟩_
  _≡→≡ᵝᵑ⟨⟩_ : ∀ {A Γ} (d {d′} : Γ ⊢ A) → d ≡ d′ → d ≡ᵝᵑ d′
  d ≡→≡ᵝᵑ⟨⟩ p = ≡→≡ᵝᵑ p

  infixr 2 _≡ᵝᵑ⟨⟩_
  _≡ᵝᵑ⟨⟩_ : ∀ {A Γ} (d {d′} : Γ ⊢ A) → d ≡ᵝᵑ d′ → d ≡ᵝᵑ d′
  d ≡ᵝᵑ⟨⟩ p = p

  infixr 2 _≡ᵝᵑ⟨_⟩_
  _≡ᵝᵑ⟨_⟩_ : ∀ {A Γ} (d {d′ d″} : Γ ⊢ A) → d ≡ᵝᵑ d′ → d′ ≡ᵝᵑ d″ → d ≡ᵝᵑ d″
  d ≡ᵝᵑ⟨ p ⟩ q = trans≡ᵝᵑ p q

  infix 3 _∎≡ᵝᵑ
  _∎≡ᵝᵑ : ∀ {A Γ} (d : Γ ⊢ A) → d ≡ᵝᵑ d
  _∎≡ᵝᵑ _ = refl≡ᵝᵑ

open ≡ᵝᵑ-Reasoning public

max_stars_repo_name: mietek/nbe-correctness

max_issues_repo_name: mietek/nbe-correctness

max_forks_repo_name: mietek/nbe-correctness


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to propositional list membership, that rely on
-- the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.List.Membership.Propositional.Properties.WithK where

open import Data.List.Base
open import Data.List.Relation.Unary.Unique.Propositional
open import Data.List.Membership.Propositional
import Data.List.Membership.Setoid.Properties as Membershipₛ
open import Relation.Unary using (Irrelevant)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Binary.PropositionalEquality.WithK

------------------------------------------------------------------------
-- Irrelevance

unique⇒irrelevant : ∀ {a} {A : Set a} {xs : List A} →
                    Unique xs → Irrelevant (_∈ xs)
unique⇒irrelevant = Membershipₛ.unique⇒irrelevant (P.setoid _) ≡-irrelevant


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

module Bool where
  open import Basics
  open import lib.Basics
  open import lib.types.Bool public

  _≤b_ : Bool → Bool → PropT₀
  true ≤b true = True
  true ≤b false  = False
  false ≤b true = True
  false ≤b false = True

  ≤b-refl : (b : Bool) → (b ≤b b) holds
  ≤b-refl true = unit
  ≤b-refl false = unit

  ≤b-trans : {a b c : Bool} → (a ≤b b) holds → (b ≤b c) holds → (a ≤b c) holds
  ≤b-trans {a} {b} {c} = ≤b-trans' a b c
    where
      ≤b-trans' : (a b c : Bool) → (a ≤b b) holds → (b ≤b c) holds → (a ≤b c) holds
      ≤b-trans' true true true = λ _ _ → unit
      ≤b-trans' true true false = λ _ z → z
      ≤b-trans' true false true = λ _ _ → unit
      ≤b-trans' true false false = λ z _ → z
      ≤b-trans' false true true = λ _ _ → unit
      ≤b-trans' false true false = λ _ _ → unit
      ≤b-trans' false false true = λ _ _ → unit
      ≤b-trans' false false false = λ _ _ → unit

  Bool-to-PropT₀ : Bool → PropT₀
  Bool-to-PropT₀ true = True
  Bool-to-PropT₀ false = False

  Dec-Prop-to-Bool : {i : ULevel} (P : PropT i) → Dec (P holds) → Bool
  Dec-Prop-to-Bool _ (inl _) = true
  Dec-Prop-to-Bool _ (inr _) = false

  Dec-Prop-to-Bool-true-id : {i : ULevel} (P : PropT i) (d : Dec (P holds))
                             → P holds → (Dec-Prop-to-Bool P d) == true
  Dec-Prop-to-Bool-true-id P (inl _) p  = refl
  Dec-Prop-to-Bool-true-id P (inr d) p = quodlibet (d p)

  Dec-Prop-to-Bool-false-id : {i : ULevel} (P : PropT i) (d : Dec (P holds))
                              → ¬ (P holds) → (Dec-Prop-to-Bool P d) == false
  Dec-Prop-to-Bool-false-id P (inl x) np = quodlibet (np x)
  Dec-Prop-to-Bool-false-id P (inr _) np = refl

  _holds-b : Bool → Type₀
  b holds-b = (Bool-to-PropT₀ b) holds

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


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

module sets.int.properties where

open import equality
open import function.core
import sets.nat as N
open N using (ℕ; suc)
open import sets.int.definition
open import sets.int.utils
import sets.int.core as Z

private
  module _ where
    open N

    add-right-unit : ∀ n n' → (n + 0) [-] (n' + 0) ≡ n [-] n'
    add-right-unit n n' = ap₂ _[-]_ (+-right-unit n) (+-right-unit n')

    add-left-inverse : ∀ n n' → (n' + n) [-] (n + n') ≡ 0 [-] 0
    add-left-inverse n n' = sym
      $ eq-ℤ 0 0 (n' + n)
      · ap₂ _[-]_ (+-right-unit (n' + n))
                  (+-right-unit (n' + n) · +-commutativity n' n)

module _ where
  open Z

  +-left-unit : ∀ n → zero + n ≡ n
  +-left-unit = elim-prop-ℤ (λ n → hℤ (zero + n) n)
                            (λ n n' → refl)

  +-right-unit : ∀ n → n + zero ≡ n
  +-right-unit = elim-prop-ℤ (λ n → hℤ (n + zero) n)
                             add-right-unit

  +-left-inverse : ∀ n → negate n + n ≡ zero
  +-left-inverse = elim-prop-ℤ (λ n → hℤ (negate n + n) zero)
                               add-left-inverse

  +-right-inverse : ∀ n → n + negate n ≡ zero
  +-right-inverse = elim-prop-ℤ (λ n → hℤ (n + negate n) zero)
                                (λ n n' → add-left-inverse n' n)

  inc-dec : ∀ n → inc (dec n) ≡ n
  inc-dec = elim-prop-ℤ (λ n → hℤ (inc (dec n)) n)
                        (λ n n' → sym (eq-ℤ n n' 1))

  dec-inc : ∀ n → dec (inc n) ≡ n
  dec-inc = elim-prop-ℤ (λ n → hℤ (dec (inc n)) n)
                        (λ n n' → sym (eq-ℤ n n' 1))

  +-associativity : ∀ n m p → n + m + p ≡ n + (m + p)
  +-associativity = elim₃-prop-ℤ
    (λ n m p → hℤ (n + m + p) (n + (m + p)))
    (λ n n' m m' p p' → ap₂ _[-]_ (N.+-associativity n m p)
                                  (N.+-associativity n' m' p'))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --safe #-}
module Issue2487.B where

import Issue2487.A


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

open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import Fields.Fields
open import Fields.Orders.Total.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Sets.EquivalenceRelations
open import LogicalFormulae
open import Groups.Definition

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

module Fields.Orders.Total.Lemmas {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {F : Field R} {p : _} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} {oR : PartiallyOrderedRing R pOrder} (oF : TotallyOrderedField F oR) where

open Ring R
open Group additiveGroup
open Setoid S
open Equivalence eq
open Field F
open TotallyOrderedField oF
open TotallyOrderedRing oRing
open PartiallyOrderedRing oR
open SetoidTotalOrder total
open SetoidPartialOrder pOrder
open import Rings.InitialRing R
open import Rings.Orders.Total.Lemmas oRing
open import Rings.Orders.Partial.Lemmas oR
open import Rings.Lemmas R
open import Groups.Lemmas additiveGroup

charNotN : (n : ℕ) → fromN (succ n) ∼ 0R → False
charNotN n pr = irreflexive (<WellDefined reflexive pr t)
  where
    t : 0R < fromN (succ n)
    t = fromNPreservesOrder (0<1 (Field.nontrivial F)) (succIsPositive n)

charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False
charNot2 pr = charNotN 1 (transitive (transitive +Associative identRight) pr)


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Package where

open import Light.Level using (Setω)

record Meta : Setω where
      field Dependencies : Setω
      field Library : Dependencies → Setω

record Package (meta : Meta) : Setω where
      instance constructor package
      open Meta meta
      field ⦃ dependencies ⦄ : Dependencies
      field ⦃ library ⦄ : Library dependencies
open Package ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

open import HoTT
open import homotopy.SuspSectionDecomp
open import homotopy.CofiberComp
open import homotopy.SmashIsCofiber

module homotopy.SuspProduct where

module SuspProduct {i} {j} (X : Ptd i) (Y : Ptd j) where

  private
    i₁ : X ⊙→ X ⊙× Y
    i₁ = ((λ x → (x , pt Y)) , idp)

    i₂ : Y ⊙→ X ⊙× Y
    i₂ = ((λ y → (pt X , y)) , idp)

    j₂ : de⊙ (⊙Cofiber i₁) → de⊙ Y
    j₂ = CofiberRec.f (pt Y) snd (λ x → idp)

  ⊙eq : ⊙Susp (X ⊙× Y) ⊙≃ ⊙Susp X ⊙∨ (⊙Susp Y ⊙∨ ⊙Susp (X ⊙∧ Y))
  ⊙eq =
    ⊙∨-emap (⊙ide (⊙Susp X))
      (⊙∨-emap (⊙ide (⊙Susp Y))
        (⊙Susp-emap (Smash-⊙equiv-Cof X Y ⊙⁻¹ ⊙∘e CofiberComp.⊙eq i₁ i₂)))
    ⊙∘e ⊙∨-emap (⊙ide (⊙Susp X))
          (≃-to-⊙≃ (SuspSectionDecomp.eq (⊙cfcod' i₁ ⊙∘ i₂) j₂ (λ y → idp))
                   (! $ ap winl $ merid (pt Y)))
    ⊙∘e ≃-to-⊙≃ (SuspSectionDecomp.eq i₁ fst (λ x → idp))
                (! $ ap winl $ merid (pt X))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Structure.Operator.Monoid.Invertible.Proofs where

import      Data.Tuple as Tuple
import      Lvl
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Operator
open import Structure.Operator.Monoid
open import Structure.Operator.Monoid.Invertible
open import Structure.Operator.Properties hiding (InverseOperatorₗ ; InverseOperatorᵣ)
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₗ ℓₑ : Lvl.Level
private variable T : Type{ℓ}
private variable _▫_ : T → T → T
private variable _⨞_ : T → T → Type{ℓₗ}

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ monoid : Monoid{T = T}(_▫_) ⦄ ⦃ invRel : InverseRelationᵣ(_▫_){ℓₗ}(_⨞_) ⦄ where
  open Monoid(monoid) using (id)

  instance
    inverseRelationᵣ-reflexivity : Reflexivity(_⨞_)
    Reflexivity.proof inverseRelationᵣ-reflexivity = [↔]-to-[←] (InverseRelationᵣ.proof invRel) ([∃]-intro id ⦃ identityᵣ(_▫_)(id) ⦄)

  instance
    inverseRelationᵣ-transitivity : Transitivity(_⨞_)
    Transitivity.proof inverseRelationᵣ-transitivity xy yz
      with [∃]-intro a ⦃ pa ⦄ ← [↔]-to-[→] (InverseRelationᵣ.proof invRel) xy
      with [∃]-intro b ⦃ pb ⦄ ← [↔]-to-[→] (InverseRelationᵣ.proof invRel) yz
      = [↔]-to-[←] (InverseRelationᵣ.proof invRel) ([∃]-intro (a ▫ b) ⦃ symmetry(_≡_) (associativity(_▫_)) 🝖 congruence₂ₗ(_▫_)(b) pa 🝖 pb ⦄)

  inverseRelationᵣ-with-opᵣ : ∀{a x y} → (x ⨞ y) → ((a ▫ x) ⨞ (a ▫ y))
  inverseRelationᵣ-with-opᵣ {a}{x}{y} xy
    with [∃]-intro z ⦃ xzy ⦄ ← [↔]-to-[→] (InverseRelationᵣ.proof invRel) xy
    = [↔]-to-[←] (InverseRelationᵣ.proof invRel) ([∃]-intro z ⦃ associativity(_▫_) 🝖 congruence₂ᵣ(_▫_)(a) xzy ⦄)

  inverseRelationᵣ-without-opᵣ : ⦃ cancₗ : Cancellationₗ(_▫_) ⦄ → ∀{a x y} → ((a ▫ x) ⨞ (a ▫ y)) → (x ⨞ y)
  inverseRelationᵣ-without-opᵣ {a}{x}{y} xy
    with [∃]-intro z ⦃ xzy ⦄ ← [↔]-to-[→] (InverseRelationᵣ.proof invRel) xy
    = [↔]-to-[←] (InverseRelationᵣ.proof invRel) ([∃]-intro z ⦃ cancellationₗ(_▫_) (symmetry(_≡_) (associativity(_▫_)) 🝖 xzy) ⦄)

  inverseRelationᵣ-of-idₗ : ∀{x} → (id ⨞ x)
  inverseRelationᵣ-of-idₗ {x} = [↔]-to-[←] (InverseRelationᵣ.proof invRel) ([∃]-intro x ⦃ identityₗ(_▫_)(id) ⦄)

  module _ {_⋄_ : (x : T) → (y : T) → . ⦃ inv : (y ⨞ x) ⦄ → T} ⦃ invOper : InverseOperatorᵣ(_▫_)(_⋄_) ⦄ where
    {-op-cancellationᵣ : ∀{a x y} → (a ⨞ x) → (a ⨞ y) → (a ▫ x ≡ a ▫ y) → (x ≡ y)
    op-cancellationᵣ {a}{x}{y} ax ay axay
      with [∃]-intro r ⦃ pr ⦄ ← [↔]-to-[→] (InverseRelationᵣ.proof invRel) ax
      with [∃]-intro s ⦃ ps ⦄ ← [↔]-to-[→] (InverseRelationᵣ.proof invRel) ay
      =
        x 🝖[ _≡_ ]-[ {!!} ]
        y 🝖-end-}

    inverseRelationᵣ-to-invertibleᵣ : ∀{x} → ⦃ x ⨞ id ⦄ → InvertibleElementᵣ(_▫_) ⦃ Monoid.identity-existenceᵣ(monoid) ⦄ (x)
    inverseRelationᵣ-to-invertibleᵣ {x} ⦃ xid ⦄ = [∃]-intro (id ⋄ x) ⦃ intro p ⦄ where
      p =
        (x ▫ (id ⋄ x))                                                    🝖[ _≡_ ]-[ congruence₂ᵣ(_▫_)(x) (InverseOperatorᵣ.proof invOper {id}{x}) ]
        (x ▫ [∃]-witness([↔]-to-[→] (InverseRelationᵣ.proof invRel) xid)) 🝖[ _≡_ ]-[ [∃]-proof([↔]-to-[→] (InverseRelationᵣ.proof invRel) xid) ]
        id                                                                🝖-end

    {- TODO: Should this not be possible without cancellation?
    inverseOperator-self : ∀{x} → let instance _ = reflexivity(_⨞_) in (x ⋄ x ≡ id)
    inverseOperator-self {x} = let instance _ = reflexivity(_⨞_) {x} in
      (x ⋄ x)                                                                        🝖[ _≡_ ]-[ InverseOperatorᵣ.proof invOper {x}{x} ]
      [∃]-witness([↔]-to-[→] (InverseRelationᵣ.proof invRel) (reflexivity(_⨞_) {x})) 🝖[ _≡_ ]-[]
      ∃.witness(Tuple.right(InverseRelationᵣ.proof invRel) (reflexivity(_⨞_)))       🝖[ _≡_ ]-[ {!!} ]
      id                                                                             🝖-end
    -}


text:
module PiQ.SAT where
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Data.Nat
open import Data.Nat.Properties
open import Data.List as L
open import Data.Maybe
open import Relation.Binary.PropositionalEquality
open import PiQ.Syntax
open import PiQ.Eval
open import PiQ.Examples

-- Given reversible F : 𝔹^n ↔ 𝔹^n, generate a circuit to find x̅ such that F(x̅) = (𝔽,…)
-- via running (LOOP F)(𝔽,𝔽̅).
-- (id↔ ⊗ F)((LOOP F)(𝔽,𝔽̅)) = (𝔽,𝔽,…)
LOOP : ∀ {n} → 𝔹^ n ↔ 𝔹^ n → 𝔹 ×ᵤ 𝔹^ n ↔ 𝔹 ×ᵤ 𝔹^ n
LOOP {0} F = id↔
LOOP {1} F = id↔ ⊗ F
LOOP {suc (suc n)} F = trace₊ ((dist ⊕ id↔) ⨾ [A+B]+C=[A+C]+B ⨾ (factor ⊕ id↔) ⨾
                               ((RESET ⨾ (id↔ ⊗ F) ⨾ COPY ⨾ (id↔ ⊗ ! F)) ⊕ id↔) ⨾
                               (dist ⊕ id↔) ⨾ [A+B]+C=[A+C]+B ⨾ (factor ⊕ (id↔ ⊗ INCR)))

MERGE : (n m : ℕ) → 𝔹^ n ×ᵤ 𝔹^ m ↔ 𝔹^ (n + m)
MERGE 0 m = unite⋆l
MERGE 1 0 = unite⋆r
MERGE 1 (suc m) = id↔
MERGE (suc (suc n)) m = assocr⋆ ⨾ (id↔ ⊗ MERGE (suc n) m)

SPLIT : (n m : ℕ) → 𝔹^ (n + m) ↔ 𝔹^ n ×ᵤ 𝔹^ m
SPLIT n m = ! MERGE n m

~_ : ∀ {n} → 𝔹^ (1 + n) ↔ 𝔹^ (1 + n) → 𝔹^ (1 + n) ↔ 𝔹^ (1 + n)
~_ {zero} F = F
~_ {suc n} F = F ⨾ NOT ⊗ id↔

-- Given a function G : 𝔹^n → 𝔹 there exists a reversible Gʳ : 𝔹^(1+n) ↔ 𝔹^(1+n) such that Gʳ(𝔽,xⁿ) = (F(xⁿ),…)
-- SAT(Gʳ) = tt iff ∃ xⁿ . G(xⁿ) = 𝕋
SAT : ∀ {n} → 𝔹^ (1 + n) ↔ 𝔹^ (1 + n) → 𝟙 ↔ 𝟙
SAT {n} Gʳ = trace⋆ (𝔽^ (3 + n)) (id↔ ⊗ ((id↔ ⊗ (LOOP (~ Gʳ) ⨾ (id↔ ⊗ SPLIT 1 n))) ⨾
                                         (id↔ ⊗ (assocl⋆ ⨾ (COPY ⊗ id↔) ⨾ assocr⋆)) ⨾
                                         assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                                         (id↔ ⊗ ((id↔ ⊗ MERGE 1 n) ⨾ LOOP⁻¹ (~ Gʳ)))))
    where
    LOOP⁻¹ : ∀ {n} → 𝔹^ n ↔ 𝔹^ n → 𝔹 ×ᵤ 𝔹^ n ↔ 𝔹 ×ᵤ 𝔹^ n
    LOOP⁻¹ F = ! (LOOP F)

module SAT_test where
  -- Examples
  -- AND(𝔽,a,b) = AND(a∧b,a,b)
  AND : 𝔹^ 3 ↔ 𝔹^ 3
  AND = FST2LAST ⨾ (dist ⨾ (id↔ ⊕ (id↔ ⊗ (dist ⨾ (id↔ ⊕ (id↔ ⊗ swap₊)) ⨾ factor))) ⨾ factor) ⨾ FST2LAST⁻¹

  NAND : 𝔹^ 3 ↔ 𝔹^ 3
  NAND = AND ⨾ (NOT ⊗ id↔)

  -- OR(𝔽,a,b) = OR(a∨b,a,b)
  OR : 𝔹^ 3 ↔ 𝔹^ 3
  OR = FST2LAST ⨾ (dist ⨾ ((id↔ ⊗ (dist ⨾ (id↔ ⊕ (id↔ ⊗ swap₊)) ⨾ factor)) ⊕ (id↔ ⊗ (id↔ ⊗ swap₊))) ⨾ factor) ⨾ FST2LAST⁻¹

  NOR : 𝔹^ 3 ↔ 𝔹^ 3
  NOR = OR ⨾ (NOT ⊗ id↔)

  -- XOR(a,b) = XOR(a xor b,b)
  XOR : 𝔹^ 2 ↔ 𝔹^ 2
  XOR = distl ⨾ (id↔ ⊕ (swap₊ ⊗ id↔)) ⨾ factorl

  tests : List ⟦ 𝔹^ 3 ⟧
  tests = (𝔽 , 𝔽 , 𝔽) ∷ (𝔽 , 𝔽 , 𝕋) ∷ (𝔽 , 𝕋 , 𝔽) ∷ (𝔽 , 𝕋 , 𝕋) ∷ (𝕋 , 𝔽 , 𝔽) ∷ (𝕋 , 𝔽 , 𝕋) ∷ (𝕋 , 𝕋 , 𝔽) ∷ (𝕋 , 𝕋 , 𝕋) ∷ []

  -- Ex₁(𝔽,a,b) = ((a∧b) xor (a∧b),_,_)
  -- ¬∃a,b . Ex₁(𝔽,a,b) = (𝕋,…)
  Ex₁ : 𝔹^ 3 ↔ 𝔹^ 3
  Ex₁ = trace⋆ (𝔽^ 1) (swap⋆ ⨾
                       (id↔ ⊗ AND) ⨾
                       assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                       (id↔ ⊗ AND) ⨾
                       assocl⋆ ⨾ (XOR ⊗ id↔) ⨾ assocr⋆ ⨾
                       (id↔ ⊗ ! AND) ⨾
                       assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                       swap⋆ )
  tests₁ = L.map (eval' Ex₁) tests

  -- Ex₂(𝔽,a,b) = ((a∧b) xor (a∨b),_,_)
  -- ∃a,b . Ex₂(𝔽,a,b) = (𝕋,…)
  Ex₂ : 𝔹^ 3 ↔ 𝔹^ 3
  Ex₂ = trace⋆ (𝔽^ 1) (swap⋆ ⨾
                       (id↔ ⊗ AND) ⨾
                       assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                       (id↔ ⊗ OR) ⨾
                       assocl⋆ ⨾ (XOR ⊗ id↔) ⨾ assocr⋆ ⨾
                       (id↔ ⊗ ! OR) ⨾
                       assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                       swap⋆ )
  tests₂ = L.map (eval' Ex₂) tests

  -- Ex₃(𝔽,a,b) = (((a∧b) ∧ (a xor b)),_,_)
  -- ¬∃a,b . Ex₃(𝔽,a,b) = (𝕋,…)
  Ex₃ : 𝔹^ 3 ↔ 𝔹^ 3
  Ex₃ = trace⋆ (𝔽^ 1) (swap⋆ ⨾
                       assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                       id↔ ⊗ F ⨾
                       (id↔ ⊗ assocl⋆) ⨾ assocl⋆ ⨾
                       (AND ⊗ id↔) ⨾
                       assocr⋆ ⨾ (id↔ ⊗ assocr⋆) ⨾
                       id↔ ⊗ ! F ⨾
                       assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                       swap⋆)
     where
     F : 𝔹^ 3 ↔ 𝔹^ 3
     F = AND ⨾ (id↔ ⊗ XOR)
  tests₃ = L.map (eval' Ex₃) tests

  -- Ex₄(𝔽,a,b) = (((a∨b) ∧ (a xor b)),_,_)
  -- ∃a,b . Ex₄(𝔽,a,b) = (𝕋,…)
  Ex₄ : 𝔹^ 3 ↔ 𝔹^ 3
  Ex₄ = trace⋆ (𝔽^ 1) (swap⋆ ⨾
                       assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                       id↔ ⊗ F ⨾
                       (id↔ ⊗ assocl⋆) ⨾ assocl⋆ ⨾
                       (AND ⊗ id↔) ⨾
                       assocr⋆ ⨾ (id↔ ⊗ assocr⋆) ⨾
                       id↔ ⊗ ! F ⨾
                       assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾
                       swap⋆)
     where
     F : 𝔹^ 3 ↔ 𝔹^ 3
     F = OR ⨾ (id↔ ⊗ XOR)
  tests₄ = L.map (eval' Ex₄) tests

  SAT-tests : List (𝟙 ↔ 𝟙)
  SAT-tests = (SAT AND) ∷ (SAT OR) ∷ (SAT XOR) ∷ (SAT Ex₁) ∷ (SAT Ex₂) ∷ (SAT Ex₃) ∷ (SAT Ex₄) ∷ []

  results : List (Maybe (Σ[ t ∈ 𝕌 ] ⟦ t ⟧) × ℕ)
  results = L.map (λ c → eval' c tt) SAT-tests
  -- (just (𝟙 , tt) , 3923) ∷
  -- (just (𝟙 , tt) , 2035) ∷
  -- (just (𝟙 , tt) , 1347) ∷
  -- (nothing , 10386) ∷
  -- (just (𝟙 , tt) , 4307) ∷
  -- (nothing , 11442) ∷
  -- (just (𝟙 , tt) , 4827) ∷ []


text:
-- Andreas, 2019-03-25, issue #3640, reported by gallais

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

-- {-# OPTIONS -v tc.polarity:40 #-}

module _ where

open import Agda.Builtin.Size

module M (_ : Set) where
  data U : Size → Set where
    node : ∀ {i} → U (↑ i)

module L (A B : Set) where
  open M A

-- WAS: crash because of number of parameters in size-index checki
-- of L.U was wrongly calculated.

-- Should succeed.


text:
open import FRP.JS.Delay using ( Delay )

module FRP.JS.Time.Core where

record Time : Set where
  constructor epoch
  field toDelay : Delay

{-# COMPILED_JS Time function(x,v) { return v.epoch(x); } #-}
{-# COMPILED_JS epoch function(d) { return d; } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module Shallow where

open import Level using (_⊔_) renaming (suc to lsuc)
open import Function
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.Nat hiding (_⊔_)
open import Data.Fin
open import Relation.Binary.PropositionalEquality as PE hiding ([_]; subst)

Π : ∀ {a b} (A : Set a) (B : A → Set b) → Set (a ⊔ b)
Π A B = (a : A) → B a

Fam : ∀ {a} → Set a → Set (lsuc a)
Fam {a} I = I → Set a

data Σ' {A B : Set} (f : A → B) (P : Fam A) : B → Set where
  ins : (a : A) → P a → Σ' f P (f a)

Π' : {I J : Set} (u : I → J) (P : Fam I) → Fam J
Π' {I} u P j = Π (∃ λ i → u i ≡ j) (λ { (i , _) → P i})

_* : {I J : Set} → (I → J) → Fam J → Fam I
(u *) A i = A (u i)

Fin⁺ : ℕ → Set
Fin⁺ = Fin ∘ suc

Vec⁺ : ∀ {a} → Set a → ℕ → Set a
Vec⁺ A n = Fin⁺ n → A

[_] : ∀ {a} {A : Set a} → A → Vec⁺ A 0
[ x ] _ = x

_∷_ : ∀ {a} {A : Set a} {n : ℕ} → A → Vec⁺ A n → Vec⁺ A (suc n)
(x ∷ v) zero    = x
(x ∷ v) (suc k) = v k

module Simple where
  module _ where
    mutual
      data U : Set where
        zero : U
        one : U
        sigma : (A : U) → (Elem A → U) → U
        pi : (A : U) → (Elem A → U) → U

      Elem : U → Set
      Elem zero        = ⊥
      Elem one         = ⊤
      Elem (sigma A B) = Σ (Elem A) (λ x → Elem (B x))
      Elem (pi A B)    = Π (Elem A) (λ x → Elem (B x))

module Recursive where
  module _ where
    ∐ : {n : ℕ} {I : Set} → (Fin⁺ n → Fam I) → Fam I
    ∐ {zero}  f   = f zero
    ∐ {suc n} f i = f zero i ⊎ ∐ (λ k → f (suc k)) i

    ∏ : {n : ℕ} {I : Set} → (Fin⁺ n → Fam I) → Fam I
    ∏ {zero}  f   = f zero
    ∏ {suc n} f i = f zero i × ∏ (λ k → f (suc k)) i

    data FP : Set where
      μ : FP
      ν : FP

    mutual
      data U : Set where
        fp : {n : ℕ} (A : U) (o : Vec⁺ U n) →
             FP → Functor [ A ] o → Subst o A → U

      -- | Substitutions
      Subst : {n : ℕ} → Vec⁺ U n → U → Set
      Subst {n} o A = (k : Fin⁺ n) → Elem (o k) → Elem A

      data Functor : {m n : ℕ} → Vec⁺ U m → Vec⁺ U n → Set where
        K : {m : ℕ} (v : Vec⁺ U m) (A : U)     → Functor v [ A ]
        π : {m : ℕ} (v : Vec⁺ U m) (i : Fin⁺ m) → Functor v [ v i ]
        fpF : {m n : ℕ} {v : Vec⁺ U m} {o : Vec⁺ U n} {A : U} →
              FP → Functor (A ∷ v) o → Subst o A → Functor v [ A ]

      Elem : U → Set
      Elem (fp A o μ F u) = {!!} -- LFP F u {!!}
        where
          G : Fam (Elem A) → Fam (Elem A)
          G = IndFun F u

      Elem (fp A o ν F u) = {!!}

      IdxFam : {m : ℕ} → Vec⁺ U m → Set₁
      IdxFam {m} v = (k : Fin⁺ m) → Fam (Elem (v k))

      ⟦_⟧ : {m n : ℕ} {i : Vec⁺ U m} {o : Vec⁺ U n} →
            Functor i o → (IdxFam i → IdxFam o)
      ⟦ K v A ⟧ x k        i = Elem A
      ⟦ π v k ⟧ x zero     i = x k i
      ⟦ π v k ⟧ x (suc ()) i
      ⟦ fpF μ F u ⟧ x = {!!}
      ⟦ fpF ν F u ⟧ x = {!!}

      IndFun : {n : ℕ} {A : U} {o : Vec⁺ U n} →
               (F : Functor [ A ] o) →
               -- (F : Fam (Elem A) → IdxFam o) →
               (u : Subst o A) →
               (Fam (Elem A) → Fam (Elem A))
      IndFun {n} {A} F u X = ∐ f
        where
          f : Fin⁺ n → Fam (Elem A)
          f k = Σ' (u k) (⟦ F ⟧ (λ _ → X) k)

      CoindFun : {n : ℕ} {A : U} {o : Vec⁺ U n} →
                 (F : Functor [ A ] o) →
                 -- (F : Fam (Elem A) → IdxFam o) →
                 (u : Subst o A) →
                 (Fam (Elem A) → Fam (Elem A))
      CoindFun {n} {A} F u X = ∏ f
        where
          f : Fin⁺ n → Fam (Elem A)
          f k = Π' (u k) (⟦ F ⟧ (λ _ → X) k)

      data LFP {n : ℕ} {A : U} {o : Vec⁺ U n}
               (F : Functor [ A ] o) (u : Subst o A) : Elem A → Set where
--        α : (a : Elem A) → IndFun F u (LFP F u) a → LFP F u a

{-
      data U : Set where
        fp : {n : ℕ} (C : Cat) (o : Vec Cat n) →
             FP → Functor [ C ] o → Subst o C → U

      -- | Index of a fibre
      Cat : Set
      Cat = Σ U Elem

      Mor : Cat → Set
      Mor C = ? -- (A , x) = -- Σ U (λ B → {!Elem B → x!})

      -- | Substitutions
      Subst : {n : ℕ} → Vec Cat n → Cat → Set
      Subst {n} o C = Vec {!!} n

      data Functor : {m n : ℕ} → Vec Cat m → Vec Cat n → Set where
        K : {m : ℕ} (v : Vec Cat m) → {A : U} → (x : Elem A) → Functor v [ , x ]
        π : {m : ℕ} (v : Vec Cat m) → (i : Fin m) → Functor v [ lookup i v ]
        fpF : {m n : ℕ} {v : Vec Cat m} {o : Vec Cat n} {C : Cat} →
              FP → Functor (C ∷ v) o → Subst o C → Functor v [ C ]

      Elem : U → Set
      Elem x = {!!}
-}

module DepPoly where
  module _ where
    record DPoly (J I : Set) : Set₁ where
      constructor dpoly
      field
        -- J <- Shapes -> Pos -> I
        Pos : Set
        Shapes : Set
        s : Shapes → J
        f : Shapes → Pos
        t : Pos → I
    open DPoly

    ⟦_⟧ : {J I : Set} → DPoly J I → Fam J → Fam I
    ⟦ dpoly A B s f t ⟧ X = Σ' t (Π' f ((s *) X))

    data W {I : Set} (P : DPoly I I) : I → Set where
      α : (i : I) → ⟦ P ⟧ (W P) i → W P i

    record M {I : Set} (P : DPoly I I) (i : I) : Set where
      coinductive
      field
        ξ : ⟦ P ⟧ (M P) i

    data FP : Set where
      μ : FP
      ν : FP

    mutual
      data U : Set where
        fp : {n : ℕ} (A : U) (o : Vec⁺ U n) →
             FP → Functor [ A ] o → Subst o A → U

      -- | Substitutions
      Subst : {n : ℕ} → Vec⁺ U n → U → Set
      Subst {n} o A = (k : Fin⁺ n) → Elem (o k) → Elem A

      data Functor : {m n : ℕ} → Vec⁺ U m → Vec⁺ U n → Set where
        K : {m : ℕ} (v : Vec⁺ U m) {I A : U} → (Elem A → Elem I) → Functor v [ I ]
        π : {m : ℕ} (v : Vec⁺ U m) (i : Fin⁺ m) → Functor v [ v i ]
        fpF : {m n : ℕ} {v : Vec⁺ U m} {o : Vec⁺ U n} {A : U} →
              FP → Functor (A ∷ v) o → Subst o A → Functor v [ A ]

      Elem : U → Set
      Elem (fp A o μ F u) = Σ (Elem A) (W (Poly F u))
      Elem (fp A o ν F u) = {!!}

      Poly : {n : ℕ} {I : U} {o : Vec⁺ U n} (F : Functor [ I ] o) →
             (u : Subst o I) → DPoly (Elem I) (Elem I)
      Poly         (K ._ {J} {A} B) u =
        dpoly (Elem A) ⊥ (λ ()) (λ ()) (u zero ∘ B)
      Poly {I = I} (π ._ i)         u =
        dpoly (Elem I) (Elem I) id id id
      Poly         (fpF μ F v) u =
        {!!}
      Poly         (fpF ν F v) u =
        {!!}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- Σ type (also used as existential) and
-- cartesian product (also used as conjunction).

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

module Tools.Product where

open import Agda.Primitive

infixr 4 _,_
infixr 2 _×_

-- Dependent pair type (aka dependent sum, Σ type).

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

open Σ public

record Σω₀ {ℓ} (A : Set ℓ) (B : A → Setω) : Setω where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σω₀ public

record Σω₂ {ℓ} (A : Setω) (B : A → Set ℓ) : Setω where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σω₂ public

record Σω₃ (A : Setω) (B : A → Setω) : Setω where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σω₃ public

record Σω₄ (A : Setω₁) (B : A → Setω) : Setω₁ where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σω₄ public

-- Existential quantification.

∃ : {ℓ ℓ′ : Level} → {A : Set ℓ} → (A → Set ℓ′) → Set (ℓ ⊔ ℓ′)
∃ = Σ _

∃₂ : {ℓ ℓ′ ℓ″ : Level} → {A : Set ℓ} {B : A → Set ℓ′}
     (C : (x : A) → B x → Set ℓ″) → Set (ℓ ⊔ ℓ′ ⊔ ℓ″)
∃₂ C = ∃ λ a → ∃ λ b → C a b

∃ω₃ : {A : Setω} → (A → Setω) → Setω
∃ω₃ = Σω₃ _

∃ω₃² : {A : Setω} {B : A → Setω}
     (C : (x : A) → B x → Setω) → Setω
∃ω₃² C = ∃ω₃ λ a → ∃ω₃ λ b → C a b

∃ω₄ : {A : Setω₁} → (A → Setω) → Setω₁
∃ω₄ = Σω₄ _

-- Cartesian product.

_×_ : {ℓ ℓ′ : Level} → (A : Set ℓ) → (B : Set ℓ′) → Set (ℓ ⊔ ℓ′)
A × B = Σ A (λ x → B)

_×ω₂_ : {ℓ : Level} → (A : Setω) → (B : Set ℓ) → Setω
A ×ω₂ B = Σω₂ A (λ x → B)

_×ω₃_ : (A : Setω) → (B : Setω) → Setω
A ×ω₃ B = Σω₃ A (λ x → B)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
-- Andreas, 2012-11-22 issue #729, abstract aliases
-- Andreas, 2016-07-19 issue #2102, better fix of #418 helps!

module Issue729 where

abstract
  B = Set
  B₁ = B
  B₂ = Set

abstract
  foo : Set₁
  foo = x
    where x = B

mutual
  abstract
    D = C
    C = B

abstract
  mutual
    F = E
    E = D

-- other stuff

private
  A = Set

Y = let X = Set in Set


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

open import Categories.Category

module Categories.Category.Site {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Product using (Σ; _,_; ∃₂)

open Category C

private
  variable
    X Y Z : Obj

record Coverage {i} j {I : Obj → Set i}
                (covering₀ : ∀ {X} → I X → Obj)
                (covering₁ : ∀ {X} (i : I X) → covering₀ i ⇒ X) : Set (i ⊔ suc j ⊔ o ⊔ ℓ ⊔ e) where
  field
    J          : ∀ (g : Y ⇒ Z) → Set j
    universal₀ : ∀ {g : Y ⇒ Z} → J g → Obj
    universal₁ : ∀ {g : Y ⇒ Z} (j : J g) → universal₀ j ⇒ Y
    commute    : ∀ {g : Y ⇒ Z} (j : J g) → ∃₂ (λ i k → g ∘ universal₁ j ≈ covering₁ i ∘ k)

record Site i j : Set (suc i ⊔ suc j ⊔ o ⊔ ℓ ⊔ e) where
  field
    I         : Obj → Set i
    covering₀ : ∀ {X} → I X → Obj
    covering₁ : ∀ {X} (i : I X) → covering₀ i ⇒ X
    coverage  : Coverage j covering₀ covering₁

  module coverage = Coverage coverage
  open coverage public

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:
module JVM.Model.Properties where

open import Data.List
open import Data.List.Properties
open import Data.List.Relation.Binary.Permutation.Propositional
open import Data.List.Relation.Binary.Permutation.Propositional.Properties

open import Data.Product hiding (map)

open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Construct.Bag.Properties
open import Function

module _ {p t} {T : Set t} {P : Pred _ p} where

  open import JVM.Model (List T)
  open import Data.List.Relation.Unary.All

  -- If you know the split and what is bubbling up from the left and right parts,
  -- then you know what bubbles up from the composite.
  source : ∀ {Φ₁ : Intf} → Φ₁ ∙ Φ₂ ≣ Φ → All P (up Φ₁) → All P (up Φ₂) → All P (up Φ)
  source (ex {u₁} {u₂} (sub x₁ x₂) (sub x₃ x₄) x₅ x₆) pu₁ pu₂ = joinAll (λ ()) x₅ pu₁' pu₂'
    where
      pu₂' = proj₁ (splitAll (λ where dup p → p , p) x₂ pu₂)
      pu₁' = proj₁ (splitAll (λ where dup p → p , p) x₄ pu₁)

  -- If you know the split and what is bubbling up from the left and flowing down the composite,
  -- then you know what flows down the right part.
  sinkᵣ : ∀ {Φ₁ : Intf} → Φ₁ ∙ Φ₂ ≣ Φ → All P (up Φ₁) → All P (down Φ) → All P (down Φ₂)
  sinkᵣ (ex (sub x₁ x₂) (sub x₃ x₄) x₅ x₆) pu₁ pu₂ = joinAll (λ ()) x₃ pd₁' pe₁
    where
      pd₁' = proj₁ (splitAll (λ where dup p → p , p) x₆ pu₂)
      pe₁  = proj₂ (splitAll (λ where dup p → p , p) x₄ pu₁)

  -- The same, but different.
  sinkₗ : ∀ {Φ₁ Φ₂ Φ : Intf} → Φ₁ ∙ Φ₂ ≣ Φ → All P (up Φ₂) → All P (down Φ) → All P (down Φ₁)
  sinkₗ σ ups downs = sinkᵣ (∙-comm σ) ups downs

-- {- Mapping along any injection yields a model morphism -}
-- module _ {a b} {A : Set a} {B : Set b} (𝑚 : A ↣ B) where

--   open Injection 𝑚

--   private
--     ⟦_⟧ = λ a → f a
--     j   = map ⟦_⟧

--   open import JVM.Model A as L
--   open import JVM.Model B as R
--   import Relation.Ternary.Construct.Duplicate.Properties as D
--   import Relation.Ternary.Construct.Empty.Properties as E
--   module OMM = MonoidMorphism (bagMap (D.f-morphism 𝑚))
--   module DMM = MonoidMorphism (bagMap (E.⊥-morphism ⟦_⟧))
--   import Relation.Ternary.Construct.Bag.Overlapping as O
--   import Relation.Ternary.Construct.Bag.Disjoint as D

--   private

--     sub-lemma⁺ : ∀ {xs ys u d} → xs L.- ys ≣ (u L.⇅ d) → j xs R.- j ys ≣ (j u R.⇅ j d)
--     sub-lemma⁺ (sub x x₁) = R.sub (DMM.j-∙ x) (OMM.j-∙ x₁)

--     sub-lemma⁻ : ∀ {xs ys u d} → j xs R.- j ys ≣ (u R.⇅ d) →
--                ∃₂ λ u' d' → xs L.- ys ≣ (u' L.⇅ d') × u ≡ j u' × d ≡ j d'
--     sub-lemma⁻ (sub x y)
--       with _ , x' , refl , refl ← D.map-inv _ ⟦_⟧ x
--          | _ , y' , refl , eq   ← O.map-inv _ ⟦_⟧ y
--          with refl ← map-injective 𝑚 eq
--          = -, -, (L.sub x' y' , refl , refl)

--   ⟦⟧-morphism : SemigroupMorphism L.intf-isSemigroup R.intf-isSemigroup
--   SemigroupMorphism.j ⟦⟧-morphism (e ⇅ d)       = (j e) R.⇅ (j d)
--   SemigroupMorphism.jcong ⟦⟧-morphism (ρ₁ , ρ₂) = map⁺ ⟦_⟧ ρ₁ , map⁺ ⟦_⟧ ρ₂
--   SemigroupMorphism.j-∙ ⟦⟧-morphism (ex x x₁ σ₁ σ₂)  =
--     R.ex (sub-lemma⁺ x) (sub-lemma⁺ x₁) (DMM.j-∙ σ₁) (OMM.j-∙ σ₂)
--   SemigroupMorphism.j-∙⁻ ⟦⟧-morphism (ex x x₁ σ₁ σ₂) with sub-lemma⁻ x
--   ... | _ , _ , y  , refl , refl with sub-lemma⁻ x₁
--   ... | _ , _ , y₁ , refl , refl with _ , τ₁ , refl ← DMM.j-∙⁻ σ₁ | _ , τ₂ , refl ← OMM.j-∙⁻ σ₂
--      = -, L.ex y y₁ τ₁ τ₂ , refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Functors
------------------------------------------------------------------------

-- Note that currently the functor laws are not included here.

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

module Category.Functor where

open import Function
open import Level

open import Relation.Binary.PropositionalEquality

record RawFunctor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
  infixl 4 _<$>_ _<$_
  infixl 1 _<&>_

  field
    _<$>_ : ∀ {A B} → (A → B) → F A → F B

  _<$_ : ∀ {A B} → A → F B → F A
  x <$ y = const x <$> y

  _<&>_ : ∀ {A B} → F A → (A → B) → F B
  _<&>_ = flip _<$>_

-- A functor morphism from F₁ to F₂ is an operation op such that
-- op (F₁ f x) ≡ F₂ f (op x)

record Morphism {ℓ} {F₁ F₂ : Set ℓ → Set ℓ}
                (fun₁ : RawFunctor F₁)
                (fun₂ : RawFunctor F₂) : Set (suc ℓ) where
  open RawFunctor
  field
    op     : ∀{X} → F₁ X → F₂ X
    op-<$> : ∀{X Y} (f : X → Y) (x : F₁ X) →
             op (fun₁ ._<$>_ f x) ≡ fun₂ ._<$>_ f (op x)


text:
module Naturals where

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

infixl 60 _+_
infixl 80 _*_

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

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

{-# BUILTIN NATURAL  Nat  #-}
{-# BUILTIN ZERO     zero #-}
{-# BUILTIN SUC      suc  #-}
{-# BUILTIN NATPLUS  _+_  #-}
{-# BUILTIN NATTIMES _*_  #-}

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- Two fun examples of generic programming using univalence

{-# OPTIONS --cubical --safe #-}
module Cubical.Experiments.Generic where

open import Agda.Builtin.String
open import Agda.Builtin.List

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

open import Cubical.Data.Nat
open import Cubical.Data.Int
open import Cubical.Data.Prod

----------------------------------------------------------------------------
--
-- Dan Licata's example from slide 47 of:
-- http://dlicata.web.wesleyan.edu/pubs/l13jobtalk/l13jobtalk.pdf

There : Type₀ → Type₀
There X = List (ℕ × String × (X × ℕ))

Database : Type₀
Database = There (ℕ × ℕ)

us : Database
us = (4  , "John"  , (30 ,  5) , 1956)
   ∷ (8  , "Hugo"  , (29 , 12) , 1978)
   ∷ (15 , "James" , (1  ,  7) , 1968)
   ∷ (16 , "Sayid" , (2  , 10) , 1967)
   ∷ (23 , "Jack"  , (3  , 12) , 1969)
   ∷ (42 , "Sun"   , (20 ,  3) , 1980)
   ∷ []

convert : Database → Database
convert d = transport (λ i → There (swapEq ℕ ℕ i)) d

-- Swap the dates of the American database to get the European format
eu : Database
eu = convert us

-- A sanity check
_ : us ≡ convert eu
_ = refl

----------------------------------------------------------------------------
--
-- Example inspired by:
--
-- Scrap Your Boilerplate: A Practical Design Pattern for Generic Programming
-- Ralf Lämmel & Simon Peyton Jones, TLDI'03

Address : Type₀
Address = String

Name : Type₀
Name = String

data Person : Type₀ where
  P : Name → Address → Person

data Salary (A : Type₀) : Type₀ where
  S : A → Salary A

data Employee (A : Type₀) : Type₀ where
  E : Person → Salary A → Employee A

Manager : Type₀ → Type₀
Manager A = Employee A

-- First test of "mutual"
mutual
  data Dept (A : Type₀) : Type₀ where
    D : Name → Manager A → List (SubUnit A) → Dept A

  data SubUnit (A : Type₀) : Type₀ where
    PU : Employee A → SubUnit A
    DU : Dept A → SubUnit A

data Company (A : Type₀) : Type₀ where
  C : List (Dept A) → Company A

-- A small example

anders : Employee Int
anders = E (P "Anders" "Pittsburgh") (S (pos 2500))

andrea : Employee Int
andrea = E (P "Andrea" "Copenhagen") (S (pos 2000))

andreas : Employee Int
andreas = E (P "Andreas" "Gothenburg") (S (pos 3000))

-- For now we have a small company
genCom : Company Int
genCom =
  C ( D "Research" andreas (PU anders ∷ PU andrea ∷ [])
    ∷ [])

-- Increase the salary for everyone by 1
incSalary : Company Int → Company Int
incSalary c = transport (λ i → Company (sucPathInt i)) c

genCom1 : Company Int
genCom1 = incSalary genCom

-- Increase the salary more
incSalaryℕ : ℕ → Company Int → Company Int
incSalaryℕ n c = transport (λ i → Company (addEq n i)) c

genCom2 : Company Int
genCom2 = incSalaryℕ 2 genCom

genCom10 : Company Int
genCom10 = incSalaryℕ 10 genCom

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical