text:
module Logic.DiagonalMethod where

open import Functional
open import Logic.Predicate
open import Logic.Propositional
import      Lvl
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Domain
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Function
open import Type.Size
open import Type

private variable ℓ : Lvl.Level
private variable T A B : Type{ℓ}

-- Also called: Diagonal method, Cantor's diagonal argument.
function-type-surjectivity-fixpoint : (A ≽ (A → B)) → ∀{f : B → B} → ∃(Fixpoint f)
function-type-surjectivity-fixpoint ([∃]-intro s) {f}
  with [∃]-intro i ⦃ p ⦄ ← surjective(s) {f ∘ (s $₂_)}
  = [∃]-intro(s i i) ⦃ intro(symmetry(_≡_) (congruence₂ₗ(_$_)(i) p)) ⦄

module _ where
  open import Data.Boolean
  open import Data.Boolean.Proofs

  decidable-power-set-no-surjection : ¬(T ≽ (T → Bool))
  decidable-power-set-no-surjection = (p ↦ [!]-no-fixpoints(Fixpoint.proof([∃]-proof(p{not})))) ∘ function-type-surjectivity-fixpoint

module _ where
  open import Data.Boolean
  open import Data.Boolean.Proofs
  open import Function.Inverseᵣ
  open import Structure.Function.Domain.Proofs
  open import Structure.Function
  open import Syntax.Transitivity

  function-type-no-surjection : (B ≽ Bool) → ¬(A ≽ (A → B))
  function-type-no-surjection ([∃]-intro r-bool) surj
    with [∃]-intro i ⦃ fix ⦄ ← function-type-surjectivity-fixpoint surj {invᵣ r-bool ⦃ surjective-to-invertibleᵣ ⦄ ∘ not ∘ r-bool}
    = [!]-no-fixpoints(symmetry(_≡_) (Inverseᵣ.proof surjective-to-inverseᵣ) 🝖 congruence₁(r-bool) (Fixpoint.proof fix))

module _ where
  open import Numeral.Natural
  open import Numeral.Natural.Oper.Proofs

  ℕ-function-non-surjectivity : ¬(ℕ ≽ (ℕ → ℕ))
  ℕ-function-non-surjectivity = (p ↦ 𝐒-not-self(Fixpoint.proof([∃]-proof(p{𝐒})))) ∘ function-type-surjectivity-fixpoint

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors
------------------------------------------------------------------------

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

module Data.Vec where

open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.List.Base as List using (List)
open import Data.Product as Prod using (∃; ∃₂; _×_; _,_)
open import Data.These as These using (These; this; that; these)
open import Function
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (yes; no)
open import Relation.Unary using (Pred; Decidable)

------------------------------------------------------------------------
-- Types

infixr 5 _∷_

data Vec {a} (A : Set a) : ℕ → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

infix 4 _[_]=_

data _[_]=_ {a} {A : Set a} :
            {n : ℕ} → Vec A n → Fin n → A → Set a where
  here  : ∀ {n}     {x}   {xs : Vec A n} → x ∷ xs [ zero ]= x
  there : ∀ {n} {i} {x y} {xs : Vec A n}
          (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x

------------------------------------------------------------------------
-- Basic operations

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

  head : ∀ {n} → Vec A (1 + n) → A
  head (x ∷ xs) = x

  tail : ∀ {n} → Vec A (1 + n) → Vec A n
  tail (x ∷ xs) = xs

  lookup : ∀ {n} → Vec A n → Fin n → A
  lookup (x ∷ xs) zero    = x
  lookup (x ∷ xs) (suc i) = lookup xs i

  insert : ∀ {n} → Vec A n → Fin (suc n) → A → Vec A (suc n)
  insert xs       zero     v = v ∷ xs
  insert []       (suc ()) v
  insert (x ∷ xs) (suc i)  v = x ∷ insert xs i v

  remove : ∀ {n} → Vec A (suc n) → Fin (suc n) → Vec A n
  remove (_ ∷ xs)     zero     = xs
  remove (x ∷ [])     (suc ())
  remove (x ∷ y ∷ xs) (suc i)  = x ∷ remove (y ∷ xs) i

  updateAt : ∀ {n} → Fin n → (A → A) → Vec A n → Vec A n
  updateAt zero    f (x ∷ xs) = f x ∷ xs
  updateAt (suc i) f (x ∷ xs) = x   ∷ updateAt i f xs

  -- xs [ i ]%= f  modifies the i-th element of xs according to f

  infixl 6 _[_]%=_

  _[_]%=_ : ∀ {n} → Vec A n → Fin n → (A → A) → Vec A n
  xs [ i ]%= f = updateAt i f xs

  -- xs [ i ]≔ y  overwrites the i-th element of xs with y

  infixl 6 _[_]≔_

  _[_]≔_ : ∀ {n} → Vec A n → Fin n → A → Vec A n
  xs [ i ]≔ y = xs [ i ]%= const y

------------------------------------------------------------------------
-- Operations for transforming vectors

map : ∀ {a b n} {A : Set a} {B : Set b} →
      (A → B) → Vec A n → Vec B n
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

-- Concatenation.

infixr 5 _++_

_++_ : ∀ {a m n} {A : Set a} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

concat : ∀ {a m n} {A : Set a} →
         Vec (Vec A m) n → Vec A (n * m)
concat []         = []
concat (xs ∷ xss) = xs ++ concat xss

-- Align and Zip.

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  alignWith : ∀ {m n} → (These A B → C) → Vec A m → Vec B n → Vec C (m ⊔ n)
  alignWith f []         bs       = map (f ∘′ that) bs
  alignWith f as@(_ ∷ _) []       = map (f ∘′ this) as
  alignWith f (a ∷ as)   (b ∷ bs) = f (these a b) ∷ alignWith f as bs

  zipWith : ∀ {n} → (A → B → C) → Vec A n → Vec B n → Vec C n
  zipWith f []       []       = []
  zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

  unzipWith : ∀ {n} → (A → B × C) → Vec A n → Vec B n × Vec C n
  unzipWith f []       = [] , []
  unzipWith f (a ∷ as) = Prod.zip _∷_ _∷_ (f a) (unzipWith f as)

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

  align : ∀ {m n} → Vec A m → Vec B n → Vec (These A B) (m ⊔ n)
  align = alignWith id

  zip : ∀ {n} → Vec A n → Vec B n → Vec (A × B) n
  zip = zipWith _,_

  unzip : ∀ {n} → Vec (A × B) n → Vec A n × Vec B n
  unzip = unzipWith id

-- Interleaving.

infixr 5 _⋎_

_⋎_ : ∀ {a m n} {A : Set a} →
      Vec A m → Vec A n → Vec A (m +⋎ n)
[]       ⋎ ys = ys
(x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs)

-- Pointwise application

infixl 4 _⊛_

_⊛_ : ∀ {a b n} {A : Set a} {B : Set b} →
      Vec (A → B) n → Vec A n → Vec B n
[]       ⊛ _        = []
(f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs)

-- Multiplication

infixl 1 _>>=_

_>>=_ : ∀ {a b m n} {A : Set a} {B : Set b} →
        Vec A m → (A → Vec B n) → Vec B (m * n)
xs >>= f = concat (map f xs)

infixl 4 _⊛*_

_⊛*_ : ∀ {a b m n} {A : Set a} {B : Set b} →
       Vec (A → B) m → Vec A n → Vec B (m * n)
fs ⊛* xs = fs >>= λ f → map f xs

allPairs : ∀ {a b m n} {A : Set a} {B : Set b} →
           Vec A m → Vec B n → Vec (A × B) (m * n)
allPairs xs ys = map _,_ xs ⊛* ys

------------------------------------------------------------------------
-- Operations for reducing vectors

foldr : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → A → B n → B (suc n)) →
        B zero →
        Vec A m → B m
foldr b _⊕_ n []       = n
foldr b _⊕_ n (x ∷ xs) = x ⊕ foldr b _⊕_ n xs

foldr₁ : ∀ {a} {A : Set a} {m} →
         (A → A → A) → Vec A (suc m) → A
foldr₁ _⊕_ (x ∷ [])     = x
foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys)

foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → B n → A → B (suc n)) →
        B zero →
        Vec A m → B m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs

foldl₁ : ∀ {a} {A : Set a} {m} →
         (A → A → A) → Vec A (suc m) → A
foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs

-- Special folds

sum : ∀ {n} → Vec ℕ n → ℕ
sum = foldr _ _+_ 0

count : ∀ {a p} {A : Set a} {P : Pred A p} → Decidable P →
        ∀ {n} → Vec A n → ℕ
count P? []       = zero
count P? (x ∷ xs) with P? x
... | yes _ = suc (count P? xs)
... | no  _ = count P? xs

------------------------------------------------------------------------
-- Operations for building vectors

[_] : ∀ {a} {A : Set a} → A → Vec A 1
[ x ] = x ∷ []

replicate : ∀ {a n} {A : Set a} → A → Vec A n
replicate {n = zero}  x = []
replicate {n = suc n} x = x ∷ replicate x

tabulate : ∀ {n a} {A : Set a} → (Fin n → A) → Vec A n
tabulate {zero}  f = []
tabulate {suc n} f = f zero ∷ tabulate (f ∘ suc)

allFin : ∀ n → Vec (Fin n) n
allFin _ = tabulate id

------------------------------------------------------------------------
-- Operations for dividing vectors

splitAt : ∀ {a} {A : Set a} m {n} (xs : Vec A (m + n)) →
          ∃₂ λ (ys : Vec A m) (zs : Vec A n) → xs ≡ ys ++ zs
splitAt zero    xs                = ([] , xs , refl)
splitAt (suc m) (x ∷ xs)          with splitAt m xs
splitAt (suc m) (x ∷ .(ys ++ zs)) | (ys , zs , refl) =
  ((x ∷ ys) , zs , refl)

take : ∀ {a} {A : Set a} m {n} → Vec A (m + n) → Vec A m
take m xs          with splitAt m xs
take m .(ys ++ zs) | (ys , zs , refl) = ys

drop : ∀ {a} {A : Set a} m {n} → Vec A (m + n) → Vec A n
drop m xs          with splitAt m xs
drop m .(ys ++ zs) | (ys , zs , refl) = zs

group : ∀ {a} {A : Set a} n k (xs : Vec A (n * k)) →
        ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss
group zero    k []                  = ([] , refl)
group (suc n) k xs                  with splitAt k xs
group (suc n) k .(ys ++ zs)         | (ys , zs , refl) with group n k zs
group (suc n) k .(ys ++ concat zss) | (ys , ._ , refl) | (zss , refl) =
  ((ys ∷ zss) , refl)

split : ∀ {a n} {A : Set a} → Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋
split []           = ([]     , [])
split (x ∷ [])     = (x ∷ [] , [])
split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs)

------------------------------------------------------------------------
-- Operations for converting between lists

toList : ∀ {a n} {A : Set a} → Vec A n → List A
toList []       = List.[]
toList (x ∷ xs) = List._∷_ x (toList xs)

fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)
fromList List.[]         = []
fromList (List._∷_ x xs) = x ∷ fromList xs

------------------------------------------------------------------------
-- Operations for reversing vectors

reverse : ∀ {a n} {A : Set a} → Vec A n → Vec A n
reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []

infixl 5 _∷ʳ_

_∷ʳ_ : ∀ {a n} {A : Set a} → Vec A n → A → Vec A (1 + n)
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)

initLast : ∀ {a n} {A : Set a} (xs : Vec A (1 + n)) →
           ∃₂ λ (ys : Vec A n) (y : A) → xs ≡ ys ∷ʳ y
initLast {n = zero}  (x ∷ [])         = ([] , x , refl)
initLast {n = suc n} (x ∷ xs)         with initLast xs
initLast {n = suc n} (x ∷ .(ys ∷ʳ y)) | (ys , y , refl) =
  ((x ∷ ys) , y , refl)

init : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
init xs         with initLast xs
init .(ys ∷ʳ y) | (ys , y , refl) = ys

last : ∀ {a n} {A : Set a} → Vec A (1 + n) → A
last xs         with initLast xs
last .(ys ∷ʳ y) | (ys , y , refl) = y

ext: agda


text:
open import Prelude hiding (abs)
open import Container.List
open import Container.Traversable
open import Tactic.Reflection hiding (substArgs) renaming (unify to unifyTC)
open import Tactic.Reflection.Equality
open import Tactic.Deriving

module Tactic.Deriving.Eq where

_∋_ : ∀ {a} (A : Set a) → A → A
A ∋ x = x

private
  -- Pattern synonyms --
  infix 5 _`≡_
  pattern _`≡_ x y = def₂ (quote _≡_) x y
  pattern `subst x y z = def₃ (quote transport) x y z
  pattern `refl = con (quote refl) []

  pattern `Eq a = def (quote Eq) (vArg a ∷ [])

  pattern vLam s t = lam visible (abs s t)

  -- Helper functions --

  nLam : ∀ {A} → List (Arg A) → Term → Term
  nLam [] t = t
  nLam (arg (arg-info v _) s ∷ tel) t = lam v (abs "x" (nLam tel t))

  nPi : ∀ {A} → List (Arg A) → Term → Term
  nPi [] t = t
  nPi (arg i _ ∷ tel) t = pi (arg i unknown) (abs "x" (nPi tel t))

  newArgs : ∀ {A} → List (Arg A) → List (Arg Term)
  newArgs {A} tel = newArgsFrom (length tel) tel
    where
      newArgsFrom : Nat → List (Arg A) → List (Arg Term)
      newArgsFrom (suc n) (arg i _ ∷ tel) = arg i (var n []) ∷ newArgsFrom n tel
      newArgsFrom _ _ = []

  hideTel : ∀ {A} → List (Arg A) → List (Arg A)
  hideTel [] = []
  hideTel (arg (arg-info _ r) t ∷ tel) = arg (arg-info hidden r) t ∷ hideTel tel

  weakenTelFrom : (from n : Nat) → Telescope → Telescope
  weakenTelFrom from n [] = []
  weakenTelFrom from n (t ∷ tel) = weakenFrom from n t ∷ weakenTelFrom (suc from) n tel

  weakenTel : (n : Nat) → Telescope → Telescope
  weakenTel 0 = id
  weakenTel n = weakenTelFrom 0 n

  #pars : (d : Name) → TC Nat
  #pars = getParameters

  argsTel : (c : Name) → TC Telescope
  argsTel c = caseM telView <$> getType c of λ
    { (tel , def d ixs) → flip drop tel <$> #pars d
    ; (tel , _        ) → pure tel
    }

  #args : (c : Name) → TC Nat
  #args c = length <$> argsTel c

  params : (c : Name) → TC (List (Arg Type))
  params c = telView <$> getType c >>= λ
    { (tel , def d ixs) → flip take tel <$> #pars d
    ; _                 → pure []
    }

  -- Parallel substitution --

  Substitution : Set
  Substitution = List (Nat × Term)

  underLambda : Substitution → Substitution
  underLambda = map (λ { (i , t) → suc i , weaken 1 t })

  {-# TERMINATING #-}
  subst : Substitution → Term → Term
  apply : Term → List (Arg Term) → Term
  substArgs : Substitution → List (Arg Term) → List (Arg Term)

  subst sub (var x args) = case (lookup sub x) of λ
    { (just s) → apply s (substArgs sub args)
    ; nothing  → var x (substArgs sub args)
    }
  subst sub (con c args) = con c (substArgs sub args)
  subst sub (def f args) = def f (substArgs sub args)
  subst sub (lam v t)    = lam v (fmap (subst (underLambda sub)) t)
  subst sub (lit l)      = lit l
  subst sub _            = unknown -- TODO

  apply f [] = f
  apply (var x args) xs = var x (args ++ xs)
  apply (con c args) xs = con c (args ++ xs)
  apply (def f args) xs = def f (args ++ xs)
  apply (lam _ (abs _ t)) (arg _ x ∷ xs) = case (strengthen 1 (subst ((0 , weaken 1 x) ∷ []) t)) of λ
    { (just f) → apply f xs
    ; nothing  → unknown
    }
  apply _ _ = unknown -- TODO

  substArgs sub = map (fmap (subst sub))

  -- Unification of datatype indices --

  data Unify : Set where
    positive : List (Nat × Term) → Unify
    negative : Unify

  failure : ∀ {a} {A : Set a} → String → TC A
  failure s = typeErrorS ("Unification error when deriving Eq: " & s)

  _&U_ : Unify → Unify → Unify
  (positive xs) &U (positive ys) = positive (xs ++ ys)
  (positive _)  &U negative      = negative
  negative      &U (positive _)  = negative
  negative      &U negative      = negative

  {-# TERMINATING #-}
  unify : Term → Term → TC Unify
  unifyArgs : List (Arg Term) → List (Arg Term) → TC Unify

  unify s            t            with s == t
  unify s            t            | yes _ = pure (positive [])
  unify (var x [])   (var y [])   | no  _ =
    if (x <? y) -- In var-var case, instantiate the one that is bound the closest to us.
    then pure (positive ((x , var y []) ∷ []))
    else pure (positive ((y , var x []) ∷ []))
  unify (var x [])   t            | no  _ =
    if (elem x (freeVars t))
    then failure "cyclic occurrence" -- We don't currently know if the occurrence is rigid or not
    else pure (positive ((x , t) ∷ []))
  unify t            (var x [])   | no  _ =
    if (elem x (freeVars t))
    then failure "cyclic occurrence"
    else pure (positive ((x , t) ∷ []))
  unify (con c₁ xs₁) (con c₂ xs₂) | no  _ =
    if (isYes (c₁ == c₂))
    then unifyArgs xs₁ xs₂
    else pure negative
  unify _ _                       | no  _ = failure "not a constructor or a variable"

  unifyArgs [] [] = pure (positive [])
  unifyArgs [] (_ ∷ _) = failure "panic: different number of arguments"
  unifyArgs (_ ∷ _) [] = failure "panic: different number of arguments"
  unifyArgs (arg v₁ x ∷ xs) (arg v₂ y ∷ ys) =
    if isYes (_==_ {{EqArgInfo}} v₁ v₂)
    then (unify x y >>= λ
      { (positive sub) → (positive sub &U_) <$> unifyArgs (substArgs sub xs) (substArgs sub ys)
      ; negative       → pure negative
      })
    else failure "panic: hiding mismatch"

  unifyIndices : (c₁ c₂ : Name) → TC Unify
  unifyIndices c₁ c₂ = do
    let panic = failure "panic: constructor type doesn't end in a def"
    tel₁ , def d₁ xs₁ ← telView <$> getType c₁ where _ → panic
    tel₂ , def d₂ xs₂ ← telView <$> getType c₂ where _ → panic
    n₁ ← #pars d₁
    n₂ ← #pars d₂
    let ixs₁ = drop n₁ xs₁
        ixs₂ = drop n₂ xs₂
    unifyArgs (weaken                        (length tel₂ - n₂) ixs₁)
            -- weaken all variables of first constructor by number of arguments of second constructor
              (weakenFrom (length tel₂ - n₂) (length tel₁ - n₁) ixs₂)
            -- weaken parameters of second constructor by number of arguments of first constructor

  -- Analysing constructor types --

  forcedArgs : (c : Name) → TC (List Nat)
  forcedArgs c = caseM (unifyIndices c c) of λ
    { (positive xs) → pure (map fst xs)
    ; _             → pure []
    }

  data Forced : Set where forced free : Forced

  instance
    DeBruijnForced : DeBruijn Forced
    strengthenFrom {{DeBruijnForced}} _ _ = just
    weakenFrom     {{DeBruijnForced}} _ _ = id

    DeBruijnProd : {A B : Set} {{_ : DeBruijn A}} {{_ : DeBruijn B}} → DeBruijn (A × B)
    strengthenFrom {{DeBruijnProd}} m n (x , y) = ⦇ strengthenFrom m n x , strengthenFrom m n y ⦈
    weakenFrom     {{DeBruijnProd}} m n (x , y) = weakenFrom m n x , weakenFrom m n y

  RemainingArgs : Nat → Set
  RemainingArgs = Vec (Arg (Forced × Term × Term))

  leftArgs : ∀ {n} → RemainingArgs n → List (Arg Term)
  leftArgs = map (fmap (fst ∘ snd)) ∘ vecToList

  rightArgs : ∀ {n} → RemainingArgs n → List (Arg Term)
  rightArgs = map (fmap (snd ∘ snd)) ∘ vecToList

  classifyArgs : (c : Name) → TC (Σ Nat RemainingArgs)
  classifyArgs c = do
      #argsc  ← #args c
      forcedc ← forcedArgs c
      let #freec = #argsc - length forcedc
      _,_ _ ∘ classify #freec forcedc (#argsc - 1) (#freec - 1) <$> argsTel c
  -- The final argument should be (weakenTel (#argsc + #freec) (argsTel c)),
  -- but we don't really care about the types of the arguments anyway.
    where
      classify : Nat → List Nat → (m n : Nat) (tel : List (Arg Type)) → RemainingArgs (length tel)
      classify _ _ m n [] = []
      classify #freec forcedc m n (arg i ty ∷ tel) =
        if (elem m forcedc)
        then arg i (forced , var (#freec + m) [] , var (#freec + m) []) ∷
             classify #freec forcedc (m - 1) n       tel
        else arg i (free   , var (#freec + m) [] , var n            []) ∷
             classify #freec forcedc (m - 1) (n - 1) tel

  rightArgsFree : ∀ {n} → RemainingArgs n → List (Arg Term)
  rightArgsFree [] = []
  rightArgsFree (arg _ (forced , _ , _) ∷ xs) = rightArgsFree xs
  rightArgsFree (arg i (free   , _ , x) ∷ xs) = arg i x ∷ rightArgsFree xs

  countFree : ∀ {n} → RemainingArgs n → Nat
  countFree xs = length (rightArgsFree xs)

  refreshArgs : ∀ {n} → RemainingArgs n → RemainingArgs n
  refreshArgs xs = refresh (nfree - 1) xs
    where
      nfree = countFree xs

      refresh : ∀ {n} → Nat → RemainingArgs n → RemainingArgs n
      refresh n [] = []
      refresh n (arg i (forced , x , y) ∷ xs) = arg i (forced , x , y) ∷ refresh n xs
      refresh n (arg i (free   , x , y) ∷ xs) = arg i (free , x , var n []) ∷ refresh (n - 1) xs

  -- Matching constructor case --

  caseDec : ∀ {a b} {A : Set a} {B : Set b} → Dec A → (A → B) → (¬ A → B) → B
  caseDec (yes x) y n = y x
  caseDec (no x)  y n = n x

  checkEqArgs : ∀ {n} (c : Name) (xs : List (Arg Term)) (ys : RemainingArgs n) → Term
  checkEqArgs c xs (arg i (forced , y , z) ∷ args) =
    checkEqArgs c (xs ++ [ arg i y ]) args
  checkEqArgs {suc remainingArgs} c xs (arg i (free , y , z) ∷ args) =
    def₃ (quote caseDec)
      (def₂ (quote _==_) y z)
      (vLam "x≡y" checkEqArgsYes)
      (vLam "x≢y" checkEqArgsNo)
    where
      remainingFree = countFree args

      wk : {A : Set} {{_ : DeBruijn A}} → Nat → A → A
      wk k = weaken (k + remainingFree)

      checkEqArgsYes : Term
      checkEqArgsYes =
        def (quote transport) (
          (vArg (vLam "x" (nPi (rightArgsFree args) (def₁ (quote Dec)
            (wk 2
               (con c (xs ++ arg i y ∷ (leftArgs args)))
             `≡
             con c (wk 2 xs ++
                    arg i (var remainingFree []) ∷
                    rightArgs (refreshArgs (wk 2 args)))))))) ∷
          (vArg (var 0 [])) ∷
          (vArg (nLam (rightArgsFree args)
            (checkEqArgs c
              (wk 1 (xs ++ [ arg i y ]))
              (refreshArgs (wk 1 args))))) ∷
          weaken 1 (rightArgsFree args))

      checkEqArgsNo : Term
      checkEqArgsNo =
        con₁ (quote no) (vLam "eq" (var 1 (vArg (def₃ (quote _∋_)
          (nPi (hideTel (arg i z ∷ rightArgsFree args))
            (weaken (3 + remainingFree) (con c (xs ++ arg i y ∷ leftArgs args))
              `≡ con c (wk 3 xs ++
                        arg i (var remainingFree []) ∷
                        rightArgs (refreshArgs (wk 3 args)))
            `→
             wk 4 y `≡ var (1 + remainingFree) []))
          (pat-lam (clause
            (replicate (1 + remainingFree) (hArg dot) ++ vArg `refl ∷ [])
            `refl ∷ []) [])
          (var 0 [])) ∷ [])))

  checkEqArgs _ _ _ = con₁ (quote yes) (con₀ (quote refl))

  matchingClause : (c : Name) → TC Clause
  matchingClause c = do
      _ , args ← classifyArgs c
      paramPats ← map (fmap λ _ → var "A") ∘ hideTel <$> params c
      params    ← makeParams args
      pure (clause (paramPats ++
                  vArg (con c (makeLeftPattern args)) ∷
                  vArg (con c (makeRightPattern args)) ∷ [])
                 (checkEqArgs c params args))
    where
      args = classifyArgs c

      makeParamsPats : TC (List (Arg Pattern))
      makeParamsPats = map (fmap λ _ → var "A") ∘ hideTel <$> params c

      makeParams : ∀ {n} → RemainingArgs n → TC (List (Arg Term))
      makeParams args = do
        ps ← params c
        pure (weaken (length (vecToList args) + countFree args) (newArgs ps))

      makeLeftPattern : ∀ {n} → RemainingArgs n → List (Arg Pattern)
      makeLeftPattern [] = []
      makeLeftPattern (arg i _ ∷ xs) = arg i (var "x") ∷ makeLeftPattern xs

      makeRightPattern : ∀ {n} → RemainingArgs n → List (Arg Pattern)
      makeRightPattern [] = []
      makeRightPattern (arg i (forced , _ , _) ∷ xs) = arg i dot ∷ makeRightPattern xs
      makeRightPattern (arg i (free   , _ , _) ∷ xs) = arg i (var "y") ∷ makeRightPattern xs

  -- Mismatching constructor case --

  mismatchingClause : (c₁ c₂ : Name) (fs : List Nat) → TC Clause
  mismatchingClause c₁ c₂ fs = do
      args₁ ← argsTel c₁
      args₂ ← argsTel c₂
      let #args₁ = length args₁
          #args₂ = length args₂
      pure (clause (vArg (con c₁ (makePattern (#args₁ + #args₂ - 1) args₁)) ∷
                     vArg (con c₂ (makePattern (#args₂ - 1) args₂)) ∷ [])
                    (con (quote no) ([ vArg (pat-lam ([ absurd-clause ([ vArg absurd ]) ]) []) ])))
    where
      makePattern : (k : Nat) (args : List (Arg Type)) → List (Arg Pattern)
      makePattern k [] = []
      makePattern k (arg i _ ∷ args) = (if (elem k fs) then (arg i dot) else arg i (var "x"))
                                         ∷ makePattern (k - 1) args

  -- Clauses --

  makeClause : (c₁ c₂ : Name) → TC (List Clause)
  makeClause c₁ c₂ = case (c₁ == c₂) of λ
    { (yes _) → _∷ [] <$> matchingClause c₁
    ; (no  _) → caseM (unifyIndices c₁ c₂) of λ
      { (positive fs) → _∷ [] <$> mismatchingClause c₁ c₂ (map fst fs)
      ; _             → pure []
      }
    }

  constructorPairs : (d : Name) → TC (List (Name × Name))
  constructorPairs d = caseM getDefinition d of λ
    { (data-type _ cs) → pure $ concat (map (λ c₁ → map (_,_ c₁) cs) cs)
    ; _ → pure []
    }

  eqDefinition : (d : Name) → TC (List Clause)
  eqDefinition d = concat <$> (mapM (uncurry makeClause) =<< constructorPairs d)

  makeArgs : Nat → List (Arg Nat) → List (Arg Term)
  makeArgs n xs = reverse $ map (fmap (λ i → var (n - i - 1) [])) xs

  computeInstanceType : Nat → List (Arg Nat) → Type → Maybe Term
  computeInstanceType n xs (agda-sort _) =
    just (`Eq (var n (makeArgs n xs)))
  computeInstanceType n xs (pi a (abs s b)) =
    pi (hArg (unArg a)) ∘ abs s <$> computeInstanceType (suc n) ((n <$ a) ∷ xs) b
  computeInstanceType _ _ _ = nothing

  computeType : Name → Nat → List (Arg Nat) → Telescope → Telescope → Term
  computeType d n xs is [] =
    telPi (reverse is) $
    def d (makeArgs (n + k) xs) `→ def d (makeArgs (n + k + 1) xs) `→
    def₁ (quote Dec) (var 1 [] `≡ var 0 [])
    where k = length is
  computeType d n xs is (a ∷ tel) =
    unArg a `→ʰ
    (case computeInstanceType 0 [] (weaken 1 $ unArg a) of
     λ { (just i) → computeType d (1 + n) ((n <$ a) ∷ xs) (iArg (weaken (length is) i) ∷ weaken 1 is) tel
       ; nothing →  computeType d (1 + n) ((n <$ a) ∷ xs) (weaken 1 is) tel })

eqType : Name → TC Type
eqType d = computeType d 0 [] [] ∘ fst ∘ telView <$> getType d

macro
  deriveEqType : Name → Tactic
  deriveEqType d hole = unifyTC hole =<< (computeType d 0 [] [] ∘ fst ∘ telView <$> getType d)

deriveEqDef : Name → Name → TC ⊤
deriveEqDef i d = defineFun i =<< eqDefinition d

declareEqInstance : Name → Name → TC ⊤
declareEqInstance iname d =
  declareDef (iArg iname) =<< instanceType d (quote Eq)

defineEqInstance : Name → Name → TC ⊤
defineEqInstance iname d = do
  fname ← freshName ("_==[" & show d & "]_")
  declareDef (vArg fname) =<< eqType d
  dictCon ← recordConstructor (quote Eq)
  defineFun iname (clause [] (con₁ dictCon (def₀ fname)) ∷ [])
  defineFun fname =<< eqDefinition d
  return _

deriveEq : Name → Name → TC ⊤
deriveEq iname d =
  declareEqInstance iname d >>
  defineEqInstance  iname d

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import Optics.All
open import Util.Encode
open import Util.KVMap             as KVMap
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String using (String)

-- This module defines types for an out-of-date implementation, based
-- on a previous version of LibraBFT.  It will be updated to model a
-- more recent version in future.
--
-- One important trick here is that the RoundManager type separayes
-- types that /define/ the EpochConfig and types that /use/ the
-- /EpochConfig/. The advantage of doing this separation can be seen
-- in Util.Util.liftEC, where we define a lifting of a function that
-- does not change the bits that define the EpochConfig into the whole
-- state.  This enables a more elegant approach for reasoning about
-- functions that do not change parts of the state responsible for
-- defining the epoch config.  However, the separation is not perfect,
-- so sometimes fields may be modified in EpochIndep even though there
-- is no epoch change.

module LibraBFT.ImplShared.Consensus.Types where
  open import LibraBFT.ImplShared.NetworkMsg                     public
  open import LibraBFT.ImplShared.Base.Types                     public
  open import LibraBFT.ImplShared.Consensus.Types.EpochIndep     public
  open import LibraBFT.ImplShared.Util.Crypto                    public

  record ExponentialTimeInterval : Set where
    constructor mkExponentialTimeInterval
    field
      _etiBaseMs       : U64
      _etiExponentBase : F64
      _etiMaxExponent  : Usize
  unquoteDecl etiBaseMs   etiExponentBase   etiMaxExponent  = mkLens (quote ExponentialTimeInterval)
             (etiBaseMs ∷ etiExponentBase ∷ etiMaxExponent ∷ [])

  RoundStateTimeInterval = ExponentialTimeInterval

  record RoundState : Set where
    constructor mkRoundState
    field
      _rsTimeInterval          : RoundStateTimeInterval
      _rsHighestCommittedRound : Round
      _rsCurrentRound          : Round
      _rsCurrentRoundDeadline  : Instant
      _rsPendingVotes          : PendingVotes
      _rsVoteSent              : Maybe Vote
  open RoundState public
  unquoteDecl rsTimeInterval           rsHighestCommittedRound   rsCurrentRound
              rsCurrentRoundDeadline   rsPendingVotes            rsVoteSent = mkLens (quote RoundState)
             (rsTimeInterval         ∷ rsHighestCommittedRound ∷ rsCurrentRound ∷
              rsCurrentRoundDeadline ∷ rsPendingVotes          ∷ rsVoteSent ∷ [])

  record ObmNeedFetch : Set where
    constructor ObmNeedFetch∙new

  -- The parts of the state of a peer that are used to
  -- define the EpochConfig are the SafetyRules and ValidatorVerifier:
  record RoundManager : Set where
    constructor RoundManager∙new
    field
      _rmObmNeedFetch     : ObmNeedFetch
      -------------------------
      _rmEpochState       : EpochState
      _rmBlockStore       : BlockStore
      _rmRoundState       : RoundState
      _rmProposerElection : ProposerElection
      _rmProposalGenerator : ProposalGenerator
      _rmSafetyRules      : SafetyRules
      _rmSyncOnly         : Bool
  open RoundManager public
  unquoteDecl rmObmNeedFetch
              rmEpochState   rmBlockStore   rmRoundState   rmProposerElection
              rmProposalGenerator   rmSafetyRules   rmSyncOnly = mkLens (quote RoundManager)
             (rmObmNeedFetch ∷
              rmEpochState ∷ rmBlockStore ∷ rmRoundState ∷ rmProposerElection ∷
              rmProposalGenerator ∷ rmSafetyRules ∷ rmSyncOnly ∷ [])

  -- IMPL-DIFF: this is RoundManager field/lens in Haskell; and it is implemented completely different
  rmObmAllAuthors : Lens RoundManager (List Author)
  rmObmAllAuthors = mkLens'
    (λ rm → List-map proj₁ (kvm-toList (rm ^∙ rmEpochState ∙ esVerifier ∙ vvAddressToValidatorInfo)))
    (λ rm _ → rm) -- TODO-1 cannot be written

  -- IMPL-DIFF : In places that do "set"
  -- e.g., RoundState.processCertificates
  -- the Haskell code is :               rsVoteSent     .= Nothing
  -- the Agda    code is : lRoundState ∙ rsVoteSent     ∙= nothing
  --
  -- The Haskell code leverages the "RW" constraints (e.g., RWRoundState)
  -- to enable not specifying where something is contained (i.e., in the round manager).
  -- The Agda code does not model that, therefore it needs `lRoundState`.

  lRoundManager : Lens RoundManager RoundManager
  lRoundManager = lens (λ _ _ f rm → f rm)

  lBlockStore : Lens RoundManager BlockStore
  lBlockStore = rmBlockStore

  lBlockTree : Lens RoundManager BlockTree
  lBlockTree = lBlockStore ∙ bsInner

  lPendingVotes : Lens RoundManager PendingVotes
  lPendingVotes = rmRoundState ∙ rsPendingVotes

  lRoundState : Lens RoundManager RoundState
  lRoundState = rmRoundState

  lProposerElection : Lens RoundManager ProposerElection
  lProposerElection = rmProposerElection

  lProposalGenerator : Lens RoundManager ProposalGenerator
  lProposalGenerator = rmProposalGenerator

  lSafetyRules : Lens RoundManager SafetyRules
  lSafetyRules = rmSafetyRules

  lPersistentSafetyStorage : Lens RoundManager PersistentSafetyStorage
  lPersistentSafetyStorage = lSafetyRules ∙ srPersistentStorage

  lObmNeedFetch : Lens RoundManager ObmNeedFetch
  lObmNeedFetch = rmObmNeedFetch

  -- getter only in Haskell
  pgAuthor : Lens RoundManager (Maybe Author)
  pgAuthor = mkLens' g s
    where
    g : RoundManager → Maybe Author
    g rm = maybeS (rm ^∙ rmSafetyRules ∙ srValidatorSigner) nothing (just ∘ (_^∙ vsAuthor))
    s : RoundManager → Maybe Author → RoundManager
    s rm _ma = rm -- TODO-1 cannot be written

  -- getter only in Haskell
  srValidatorVerifier : Lens RoundManager ValidatorVerifier
  srValidatorVerifier = rmEpochState ∙ esVerifier

  -- getter only in Haskell
  -- IMPL-DIFF : this returns Author OR does an errorExit
  rmObmMe : Lens RoundManager (Maybe Author)
  rmObmMe = mkLens' g s
    where
    g : RoundManager → Maybe Author
    g rm = case rm ^∙ rmSafetyRules ∙ srValidatorSigner of λ where
             (just vs) → just (vs ^∙ vsAuthor)
             nothing   → nothing
    s : RoundManager → Maybe Author → RoundManager
    s s _ = s

  -- getter only in Haskell
  rmEpoch : Lens RoundManager Epoch
  rmEpoch = rmEpochState ∙ esEpoch

  -- not defined in Haskell, only used for proofs
  rmValidatorVerifer : Lens RoundManager ValidatorVerifier
  rmValidatorVerifer = rmEpochState ∙ esVerifier

  -- getter only in Haskell
  rmRound : Lens RoundManager Round
  rmRound = rmRoundState ∙ rsCurrentRound

  -- not defined in Haskell
  rmLastVotedRound : Lens RoundManager Round
  rmLastVotedRound = rmSafetyRules ∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVotedRound

  -- BEGIN : lens mimicking Haskell/LBFT RW* setters.
  -- IN THE MODEL OF THE HASKELL CODE, THESE SHOULD ONLY BE USED FOR SETTING.
  -- THEY CAN BE USED AS GETTERS IN PROPERTIES/PROOFS.
  rsVoteSent-rm : Lens RoundManager (Maybe Vote)
  rsVoteSent-rm = lRoundState ∙ rsVoteSent

  pssSafetyData-rm : Lens RoundManager SafetyData
  pssSafetyData-rm = lPersistentSafetyStorage ∙ pssSafetyData
  -- END : lens mimicking Haskell/LBFT RW* setters.

  record BootstrapInfo : Set where
    constructor mkBootstrapInfo
    field
      _bsiNumFaults : ℕ
      _bsiLIWS      : LedgerInfoWithSignatures
      _bsiVSS       : List ValidatorSigner
      _bsiVV        : ValidatorVerifier
      _bsiPE        : ProposerElection

  open BootstrapInfo public
  unquoteDecl bsiNumFaults   bsiLIWS   bsiVSS   bsiVV   bsiPE = mkLens (quote BootstrapInfo)
             (bsiNumFaults ∷ bsiLIWS ∷ bsiVSS ∷ bsiVV ∷ bsiPE ∷ [])

  postulate -- valid assumption
    -- We postulate the existence of BootstrapInfo known to all
    -- TODO: construct one or write a function that generates one from some parameters.
    fakeBootstrapInfo : BootstrapInfo

  data ∈BootstrapInfo-impl (bi : BootstrapInfo) : Signature → Set where
   inBootstrapQC : ∀ {sig} → sig ∈ (KVMap.elems (bi ^∙ bsiLIWS ∙ liwsSignatures))
                 → ∈BootstrapInfo-impl bi sig

  postulate -- TODO-1 : prove
    ∈BootstrapInfo?-impl : (bi : BootstrapInfo) (sig : Signature)
                         → Dec (∈BootstrapInfo-impl bi sig)

  postulate -- TODO-1: prove after defining bootstrapInfo
    bootstrapVotesRound≡0
      : ∀ {pk v}
      → (wvs : WithVerSig pk v)
      → ∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature wvs)
      → v ^∙ vRound ≡ 0
    bootstrapVotesConsistent
      : (v1 v2 : Vote)
      → ∈BootstrapInfo-impl fakeBootstrapInfo (_vSignature v1)
      → ∈BootstrapInfo-impl fakeBootstrapInfo (_vSignature v2)
      → v1 ^∙ vProposedId ≡ v2 ^∙ vProposedId

  -- To enable modeling of logging info that has not been added yet,
  -- InfoLog and an inhabitant is postulated.
  postulate -- Valid assumption: InfoLog type
    InfoLog  : Set
    fakeInfo : InfoLog

  -- The Haskell implementation has many more constructors.
  -- Constructors are being added incrementally as needed for the verification effort.
  data ErrLog : Set where
    -- full name of following field : Consensus_BlockNotFound
    ErrCBlockNotFound   : HashValue   → ErrLog
    -- full name of following field : ExecutionCorrectnessClient_BlockNotFound
    ErrECCBlockNotFound : HashValue   → ErrLog
    ErrInfo             : InfoLog     → ErrLog -- to exit early, but not an error
    ErrVerify           : VerifyError → ErrLog

  -- To enable modeling of logging errors that have not been added yet,
  -- an inhabitant of ErrLog is postulated.
  postulate -- Valid assumption: ErrLog type
    fakeErr : ErrLog

  record TxTypeDependentStuffForNetwork : Set where
    constructor TxTypeDependentStuffForNetwork∙new
    field
      _ttdsnProposalGenerator : ProposalGenerator
      _ttdsnStateComputer     : StateComputer
  open TxTypeDependentStuffForNetwork public
  unquoteDecl ttdsnProposalGenerator   ttdsnStateComputer = mkLens (quote TxTypeDependentStuffForNetwork)
             (ttdsnProposalGenerator ∷ ttdsnStateComputer ∷ [])


text:
------------------------------------------------------------------------
-- An implementation of "A Unifying Approach to Recursive and
-- Co-recursive Definitions" by Pietro Di Gianantonio and Marino
-- Miculan
------------------------------------------------------------------------

-- See the paper for more explanations.

module Contractive where

open import Relation.Unary
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as EqR
open import Induction.WellFounded
open import Function
open import Level hiding (lift)

-- Well-founded orders.

record IsWellFoundedOrder {A} (_<_ : Rel A zero) : Set where
  field
    trans         : Transitive _<_
    isWellFounded : WellFounded _<_

-- Ordered families of equivalences.

record OFE : Set1 where
  field
    Carrier            : Set
    Domain             : Set
    _<_                : Rel Carrier zero
    isWellFoundedOrder : IsWellFoundedOrder _<_
    Eq                 : Carrier → Rel Domain zero
    isEquivalence      : ∀ a → IsEquivalence (Eq a)

  open IsWellFoundedOrder isWellFoundedOrder public
  open All isWellFounded public

  setoid : Carrier → Setoid _ _
  setoid a = record { Carrier       = Domain
                    ; _≈_           = Eq a
                    ; isEquivalence = isEquivalence a
                    }

  module EqReasoning {a : Carrier} where
    open EqR    (setoid a) public
    open Setoid (setoid a) public using (refl; sym)

  -- The set of predecessors of a.

  ↓ : Carrier → Carrier → Set
  ↓ a = λ a' → a' < a

  -- The intersection of all the equivalences.

  _≅_ : Rel Domain zero
  x ≅ y = ∀ a → Eq a x y

  Family : (Carrier → Set) → Set
  Family I = ∀ x → x ∈ I → Domain

  lift : ∀ {I} → (Carrier → Domain) → Family I
  lift P = λ x _ → P x

  IsCoherent : ∀ {I} → Family I → Set
  IsCoherent {I} fam = ∀ {a' a}
    (a'∈I : a' ∈ I) (a∈I : a ∈ I) → a' < a →
    Eq a' (fam a' a'∈I) (fam a a∈I)

  IsLimit : ∀ {I} → Family I → Domain → Set
  IsLimit {I} fam y = ∀ {a'}
    (a'∈I : a' ∈ I) → Eq a' (fam a' a'∈I) y

  IsContractive : (Domain → Domain) → Set
  IsContractive F = ∀ {x y a} →
    (∀ {a'} → a' < a → Eq a' x y) → Eq a (F x) (F y)

-- Complete ordered families of equivalences.

record COFE : Set1 where
  field
    ofe : OFE

  open OFE ofe

  field
    limU     : (Carrier → Domain) → Domain
    isLimitU : ∀ {fam} →
               IsCoherent {U} (lift fam) →
               IsLimit {U} (lift fam) (limU fam)

    lim↓     : ∀ a → Family (↓ a) → Domain
    isLimit↓ : ∀ a {fam : Family (↓ a)} →
               IsCoherent fam → IsLimit fam (lim↓ a fam)

  open OFE ofe public

-- Contractive functions over complete ordered families have
-- fixpoints.

record ContractiveFun (cofe : COFE) : Set where
  open COFE cofe
  field
    F             : Domain → Domain
    isContractive : IsContractive F

  open EqReasoning

  -- The fixpoint is the limit of the following family.

  fam : Carrier → Domain
  fam = wfRec _ (const Domain) (λ a rec → F (lim↓ a rec))

  fixpoint : Domain
  fixpoint = limU fam

  -- I am not sure if this lemma can be proved without assuming some
  -- kind of proof irrelevance and/or extensionality. It is not
  -- central to the ideas developed here, though, so I leave it as a
  -- postulate.

  postulate unfold : ∀ a → fam a ≅ F (lim↓ a (lift fam))

  -- The family is coherent in several ways.

  fam-isCoherent-↓ : ∀ a → IsCoherent {↓ a} (lift fam)
  fam-isCoherent-↓ = wfRec _ P step
    where
    P : Carrier → Set
    P a = IsCoherent {↓ a} (lift fam)

    step : ∀ a → WfRec _<_ P a → P a
    step a rec {c} {b} c<a b<a c<b = begin
      fam c                  ≈⟨ unfold c c ⟩
      F (lim↓ c (lift fam))  ≈⟨ isContractive (λ {d} d<c → begin
         lim↓ c (lift fam)      ≈⟨ sym $ isLimit↓ c (rec c c<a) d<c ⟩
         lift {↓ a} fam d
              (trans d<c c<a)   ≈⟨ isLimit↓ b (rec b b<a) (trans d<c c<b) ⟩
         lim↓ b (lift fam)      ∎) ⟩
      F (lim↓ b (lift fam))  ≈⟨ sym $ unfold b c ⟩
      fam b                  ∎

  fam-isCoherent-U : IsCoherent {U} (lift fam)
  fam-isCoherent-U {a'} {a} _ _ = wfRec _ P step a a'
    where
    P : Carrier → Set
    P a = ∀ a' → a' < a → Eq a' (fam a') (fam a)

    step : ∀ a → WfRec _<_ P a → P a
    step a rec a' a'<a = begin
      fam a'                  ≈⟨ unfold a' a' ⟩
      F (lim↓ a' (lift fam))  ≈⟨ isContractive (λ {b} b<a' → begin
         lim↓ a' (lift fam)      ≈⟨ sym $ isLimit↓ a' (fam-isCoherent-↓ a') b<a' ⟩
         fam b                   ≈⟨ isLimit↓ a (fam-isCoherent-↓ a) (trans b<a' a'<a) ⟩
         lim↓ a  (lift fam)      ∎) ⟩
      F (lim↓ a  (lift fam))  ≈⟨ sym $ unfold a a' ⟩
      fam a                   ∎

  -- The fixpoint is a fixpoint.

  isFixpoint : fixpoint ≅ F fixpoint
  isFixpoint a = begin
    fixpoint               ≈⟨ sym $ isLimitU fam-isCoherent-U _ ⟩
    fam a                  ≈⟨ unfold a a ⟩
    F (lim↓ a (lift fam))  ≈⟨ isContractive (λ {a'} a'<a → begin
       lim↓ a (lift fam)      ≈⟨ sym $ isLimit↓ a (fam-isCoherent-↓ a) a'<a ⟩
       fam a'                 ≈⟨ isLimitU fam-isCoherent-U _ ⟩
       limU fam               ∎) ⟩
    F (limU fam)           ≈⟨ refl ⟩
    F fixpoint             ∎

  -- And it is unique.

  unique : ∀ x → x ≅ F x → x ≅ fixpoint
  unique x isFix = wfRec _ P step
    where
    P = λ a → Eq a x fixpoint

    step : ∀ a → WfRec _<_ P a → P a
    step a rec = begin
      x           ≈⟨ isFix a ⟩
      F x         ≈⟨ isContractive (λ {a'} a'<a → rec a' a'<a) ⟩
      F fixpoint  ≈⟨ sym $ isFixpoint a ⟩
      fixpoint    ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- Problem 2: Multiplication for matrices (from the matrix algebra DSL).

module P2 where

-- 2a: Type the variables in the text.
-- (This answer uses Agda syntax, but that is not required.)

postulate Nat : Set
postulate V : Nat -> Set -> Set
postulate Fin : Nat -> Set

Op : Set -> Set
Op a = a -> a -> a

postulate sum : {n : Nat} {a : Set} -> Op a -> V n a -> a
postulate zipWith : {n : Nat} {a : Set} -> Op a -> V n a -> V n a -> V n a

data M (m n : Nat) (a : Set) : Set where
  matrix : (Fin m -> Fin n -> a) -> M m n a

record Dummy (a : Set) : Set where
  field
    m : Nat
    n : Nat
    A : M m n a
    p : Nat
    B : M n p a
    i : Fin m
    j : Fin p

-- 2b: Type |mul| and |proj|

postulate
  proj : {m n : Nat} {a : Set} -> Fin m -> Fin n -> M m n a -> a

mul  : {m n p : Nat} {a : Set} -> Op a -> Op a ->
       M m n a -> M n p a -> M m p a

-- 2c: Implement |mul|.

postulate
  row : {m n : Nat} {a : Set} -> Fin m -> M m n a -> V n a
  col : {m n : Nat} {a : Set} -> Fin n -> M m n a -> V m a

mul addE mulE A B = matrix (\i j ->
                      sum addE (zipWith mulE (row i A) (col j B)))

max_stars_repo_name: nicolabotta/DSLsofMath

max_issues_repo_name: nicolabotta/DSLsofMath

max_forks_repo_name: nicolabotta/DSLsofMath


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

module C where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import Singleton

infixr 70 _×ᵤ_
infixr 60 _+ᵤₗ_
infixr 60 _+ᵤᵣ_
infixr 50 _⊚_

------------------------------------------------------------------------------
-- Pi

data 𝕌 : Set
⟦_⟧ : 𝕌 → Σ[ A ∈ Set ] A
data _⟷_ : 𝕌 → 𝕌 → Set

data 𝕌 where
  𝟙       : 𝕌
  _+ᵤₗ_    : 𝕌 → 𝕌 → 𝕌
  _+ᵤᵣ_    : 𝕌 → 𝕌 → 𝕌
  _×ᵤ_    : 𝕌 → 𝕌 → 𝕌
  Singᵤ : 𝕌 → 𝕌
  Recipᵤ : 𝕌 → 𝕌

⟦ 𝟙 ⟧ = ⊤ , tt
⟦ T₁ ×ᵤ T₂ ⟧ = zip _×_ _,_ ⟦ T₁ ⟧ ⟦ T₂ ⟧
⟦ T₁ +ᵤₗ T₂ ⟧ = zip _⊎_ (λ x _ → inj₁ x) ⟦ T₁ ⟧ ⟦ T₂ ⟧
⟦ T₁ +ᵤᵣ T₂ ⟧ = zip _⊎_ (λ _ y → inj₂ y) ⟦ T₁ ⟧ ⟦ T₂ ⟧
⟦ Singᵤ T ⟧ = < uncurry Singleton , (λ y → proj₂ y , refl) > ⟦ T ⟧
⟦ Recipᵤ T ⟧ = < uncurry Recip , (λ _ _ → tt) > ⟦ T ⟧

data _⟷_ where
  swap₊₁   : {t₁ t₂ : 𝕌} → t₁ +ᵤₗ t₂ ⟷ t₂ +ᵤᵣ t₁
  swap₊₂   : {t₁ t₂ : 𝕌} → t₁ +ᵤᵣ t₂ ⟷ t₂ +ᵤₗ t₁
  assocl₊₁ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤₗ (t₂ +ᵤₗ t₃) ⟷ (t₁ +ᵤₗ t₂) +ᵤₗ t₃
  assocl₊₂ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤₗ (t₂ +ᵤᵣ t₃) ⟷ (t₁ +ᵤₗ t₂) +ᵤₗ t₃
  assocl₊₃ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤᵣ (t₂ +ᵤₗ t₃) ⟷ (t₁ +ᵤᵣ t₂) +ᵤₗ t₃
  assocl₊₄ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤᵣ (t₂ +ᵤᵣ t₃) ⟷ (t₁ +ᵤₗ t₂) +ᵤᵣ t₃
  assocl₊₅ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤᵣ (t₂ +ᵤᵣ t₃) ⟷ (t₁ +ᵤᵣ t₂) +ᵤᵣ t₃
  assocr₊₁ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤₗ t₂) +ᵤₗ t₃ ⟷ t₁ +ᵤₗ (t₂ +ᵤᵣ t₃)
  assocr₊₂ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤₗ t₂) +ᵤₗ t₃ ⟷ t₁ +ᵤₗ (t₂ +ᵤₗ t₃)
  assocr₊₃ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤᵣ t₂) +ᵤₗ t₃ ⟷ t₁ +ᵤᵣ (t₂ +ᵤₗ t₃)
  assocr₊₄ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤₗ t₂) +ᵤᵣ t₃ ⟷ t₁ +ᵤᵣ (t₂ +ᵤᵣ t₃)
  assocr₊₅ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤᵣ t₂) +ᵤᵣ t₃ ⟷ t₁ +ᵤᵣ (t₂ +ᵤᵣ t₃)
  unite⋆l : {t : 𝕌} → 𝟙 ×ᵤ t ⟷ t
  uniti⋆l : {t : 𝕌} → t ⟷ 𝟙 ×ᵤ t
  unite⋆r : {t : 𝕌} → t ×ᵤ 𝟙 ⟷ t
  uniti⋆r : {t : 𝕌} → t ⟷ t ×ᵤ 𝟙
  swap⋆   : {t₁ t₂ : 𝕌} → t₁ ×ᵤ t₂ ⟷ t₂ ×ᵤ t₁
  assocl⋆ : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) ×ᵤ t₃
  assocr⋆ : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₂) ×ᵤ t₃ ⟷ t₁ ×ᵤ (t₂ ×ᵤ t₃)
  dist₁    : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤₗ t₂) ×ᵤ t₃ ⟷ (t₁ ×ᵤ t₃) +ᵤₗ (t₂ ×ᵤ t₃)
  dist₂    : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤᵣ t₂) ×ᵤ t₃ ⟷ (t₁ ×ᵤ t₃) +ᵤᵣ (t₂ ×ᵤ t₃)
  factor₁  : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₃) +ᵤₗ (t₂ ×ᵤ t₃) ⟷ (t₁ +ᵤₗ t₂) ×ᵤ t₃
  factor₂  : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₃) +ᵤᵣ (t₂ ×ᵤ t₃) ⟷ (t₁ +ᵤᵣ t₂) ×ᵤ t₃
  distl₁   : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ +ᵤₗ t₃) ⟷ (t₁ ×ᵤ t₂) +ᵤₗ (t₁ ×ᵤ t₃)
  distl₂   : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ +ᵤᵣ t₃) ⟷ (t₁ ×ᵤ t₂) +ᵤᵣ (t₁ ×ᵤ t₃)
  factorl₁ : {t₁ t₂ t₃ : 𝕌 } → (t₁ ×ᵤ t₂) +ᵤₗ (t₁ ×ᵤ t₃) ⟷ t₁ ×ᵤ (t₂ +ᵤₗ t₃)
  factorl₂ : {t₁ t₂ t₃ : 𝕌 } → (t₁ ×ᵤ t₂) +ᵤᵣ (t₁ ×ᵤ t₃) ⟷ t₁ ×ᵤ (t₂ +ᵤᵣ t₃)
  id⟷     : {t : 𝕌} → t ⟷ t
  _⊚_     : {t₁ t₂ t₃ : 𝕌} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕₁_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ +ᵤₗ t₂ ⟷ t₃ +ᵤₗ t₄)
  _⊕₂_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ +ᵤᵣ t₂ ⟷ t₃ +ᵤᵣ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ ×ᵤ t₂ ⟷ t₃ ×ᵤ t₄)
  -- monad
  return : (T : 𝕌) → T ⟷ Singᵤ T
  join : (T : 𝕌) → Singᵤ (Singᵤ T) ⟷ Singᵤ T
  unjoin : (T : 𝕌) → Singᵤ T ⟷ Singᵤ (Singᵤ T)
  tensorl : (T₁ T₂ : 𝕌) → (Singᵤ T₁ ×ᵤ T₂) ⟷ Singᵤ (T₁ ×ᵤ T₂)
  tensorr : (T₁ T₂ : 𝕌) → (T₁ ×ᵤ Singᵤ T₂) ⟷ Singᵤ (T₁ ×ᵤ T₂)
  tensor : (T₁ T₂ : 𝕌) → (Singᵤ T₁ ×ᵤ Singᵤ T₂) ⟷ Singᵤ (T₁ ×ᵤ T₂)
  untensor : (T₁ T₂ : 𝕌) → Singᵤ (T₁ ×ᵤ T₂) ⟷ (Singᵤ T₁ ×ᵤ Singᵤ T₂)
  plusl : (T₁ T₂ : 𝕌) → (Singᵤ T₁ +ᵤₗ T₂) ⟷ Singᵤ (T₁ +ᵤₗ T₂)
  plusr : (T₁ T₂ : 𝕌) → (T₁ +ᵤᵣ Singᵤ T₂) ⟷ Singᵤ (T₁ +ᵤᵣ T₂)
  -- comonad
  extract : (T : 𝕌) → Singᵤ T ⟷ T
  cojoin : (T : 𝕌) → Singᵤ T ⟷ Singᵤ (Singᵤ T)
  counjoin : (T : 𝕌) → Singᵤ (Singᵤ T) ⟷ Singᵤ T
  cotensorl : (T₁ T₂ : 𝕌) → Singᵤ (T₁ ×ᵤ T₂) ⟷ (Singᵤ T₁ ×ᵤ T₂)
  cotensorr : (T₁ T₂ : 𝕌) → Singᵤ (T₁ ×ᵤ T₂) ⟷ (T₁ ×ᵤ Singᵤ T₂)
  coplusl : (T₁ T₂ : 𝕌) → Singᵤ (T₁ +ᵤₗ T₂) ⟷ (Singᵤ T₁ +ᵤₗ T₂)
  coplusr : (T₁ T₂ : 𝕌) → Singᵤ (T₁ +ᵤᵣ T₂) ⟷ (T₁ +ᵤᵣ Singᵤ T₂)
  -- both?
  Singᵤ : (T₁ T₂ : 𝕌) → (T₁ ⟷ T₂) → (Singᵤ T₁ ⟷ Singᵤ T₂)
  -- eta/epsilon
  η : (T : 𝕌) → 𝟙 ⟷ (Singᵤ T ×ᵤ Recipᵤ T)
  ε : (T : 𝕌) → (Singᵤ T ×ᵤ Recipᵤ T) ⟷ 𝟙

!_ : {t₁ t₂ : 𝕌} → t₁ ⟷ t₂ → t₂ ⟷ t₁
! swap₊₁ = swap₊₂
! swap₊₂ = swap₊₁
! assocl₊₁ = assocr₊₂
! assocl₊₂ = assocr₊₁
! assocl₊₃ = assocr₊₃
! assocl₊₄ = assocr₊₄
! assocl₊₅ = assocr₊₅
! assocr₊₁ = assocl₊₂
! assocr₊₂ = assocl₊₁
! assocr₊₃ = assocl₊₃
! assocr₊₄ = assocl₊₄
! assocr₊₅ = assocl₊₅
! unite⋆l = uniti⋆l
! uniti⋆l = unite⋆l
! unite⋆r = uniti⋆r
! uniti⋆r = unite⋆r
! swap⋆ = swap⋆
! assocl⋆ = assocr⋆
! assocr⋆ = assocl⋆
! dist₁ = factor₁
! dist₂ = factor₂
! factor₁ = dist₁
! factor₂ = dist₂
! distl₁ = factorl₁
! distl₂ = factorl₂
! factorl₁ = distl₁
! factorl₂ = distl₂
! id⟷ = id⟷
! (c ⊚ c₁) = (! c₁) ⊚ (! c)
! (c ⊕₁ c₁) = (! c) ⊕₁ (! c₁)
! (c ⊕₂ c₁) = (! c) ⊕₂ (! c₁)
! (c ⊗ c₁) = (! c) ⊗ (! c₁)
! return T = extract T
! join T = return (Singᵤ T)
! unjoin T = join T
! tensorl T₁ T₂ = cotensorl T₁ T₂
! tensorr T₁ T₂ = cotensorr T₁ T₂
! tensor T₁ T₂ = untensor T₁ T₂
! untensor T₁ T₂ = tensor T₁ T₂
! plusl T₁ T₂ = coplusl T₁ T₂
! plusr T₁ T₂ = coplusr T₁ T₂
! extract T = return T
! cojoin T = join T
! counjoin T = return (Singᵤ T)
! cotensorl T₁ T₂ = tensorl T₁ T₂
! cotensorr T₁ T₂ = tensorr T₁ T₂
! coplusl T₁ T₂ = plusl T₁ T₂
! coplusr T₁ T₂ = plusr T₁ T₂
! Singᵤ T₁ T₂ c = Singᵤ T₂ T₁ (! c)
! η T = ε T
! ε T = η T

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Level
open import Function using () renaming (_∘_ to _∙_)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)

open import Categories.Category

private
  map⁎ : ∀ {a b p q} {A : Set a} {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → (v : Σ A P) → Σ (B (proj₁ v)) (Q (proj₂ v))
  map⁎ f g (x , y) = (f x , g y)

  map⁎′ : ∀ {a b p q} {A : Set a} {B : A → Set b} {P : Set p} {Q : P → Set q} → (f : (x : A) → B x) → ((x : P) → Q x) → (v : A × P) → B (proj₁ v) × Q (proj₂ v)
  map⁎′ f g (x , y) = (f x , g y)

  zipWith : ∀ {a b c p q r s} {A : Set a} {B : Set b} {C : Set c} {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → (_*_ : (x : C) → (y : R x) → S x y) → (x : Σ A P) → (y : Σ B Q) → S (proj₁ x ∙ proj₁ y) (proj₂ x ∘ proj₂ y)
  zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q)
  syntax zipWith f g h = f -< h >- g

Product : ∀ {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
Product C D = record
  { Obj = C.Obj × D.Obj
  ; _⇒_ = C._⇒_ -< _×_ >- D._⇒_
  ; _≡_ = C._≡_ -< _×_ >- D._≡_
  ; _∘_ = zip C._∘_ D._∘_
  ; id = C.id , D.id
  ; assoc = C.assoc , D.assoc
  ; identityˡ = C.identityˡ , D.identityˡ
  ; identityʳ = C.identityʳ , D.identityʳ
  ; equiv = record
    { refl = C.Equiv.refl , D.Equiv.refl
    ; sym = map C.Equiv.sym D.Equiv.sym
    ; trans = zip C.Equiv.trans D.Equiv.trans
    }
  ; ∘-resp-≡ = zip C.∘-resp-≡ D.∘-resp-≡
  }
  where
  module C = Category C
  module D = Category D

open import Categories.Functor using (Functor; module Functor)

infixr 2 _※_
_※_ : ∀ {o ℓ e o′₁ ℓ′₁ e′₁ o′₂ ℓ′₂ e′₂} {C : Category o ℓ e} {D₁ : Category o′₁ ℓ′₁ e′₁} {D₂ : Category o′₂ ℓ′₂ e′₂} → (F : Functor C D₁) → (G : Functor C D₂) → Functor C (Product D₁ D₂)
F ※ G = record
        { F₀ = < F.F₀ , G.F₀ >
        ; F₁ = < F.F₁ , G.F₁ >
        ; identity = F.identity , G.identity
        ; homomorphism = F.homomorphism , G.homomorphism
        ; F-resp-≡ = < F.F-resp-≡ , G.F-resp-≡ >
        }
        where
        module F = Functor F
        module G = Functor G

infixr 2 _⁂_
_⁂_ : ∀ {o₁ ℓ₁ e₁ o′₁ ℓ′₁ e′₁ o₂ ℓ₂ e₂ o′₂ ℓ′₂ e′₂} {C₁ : Category o₁ ℓ₁ e₁} {D₁ : Category o′₁ ℓ′₁ e′₁} → {C₂ : Category o₂ ℓ₂ e₂} {D₂ : Category o′₂ ℓ′₂ e′₂} → (F₁ : Functor C₁ D₁) → (F₂ : Functor C₂ D₂) → Functor (Product C₁ C₂) (Product D₁ D₂)
F ⁂ G = record
        { F₀ = map F.F₀ G.F₀
        ; F₁ = map F.F₁ G.F₁
        ; identity = F.identity , G.identity
        ; homomorphism = F.homomorphism , G.homomorphism
        ; F-resp-≡ = map F.F-resp-≡ G.F-resp-≡
        }
        where
        module F = Functor F
        module G = Functor G

open import Categories.NaturalTransformation using (NaturalTransformation; module NaturalTransformation)

infixr 2 _⁂ⁿ_
_⁂ⁿ_ : ∀ {o₁ ℓ₁ e₁ o′₁ ℓ′₁ e′₁ o₂ ℓ₂ e₂ o′₂ ℓ′₂ e′₂} {C₁ : Category o₁ ℓ₁ e₁} {D₁ : Category o′₁ ℓ′₁ e′₁} → {C₂ : Category o₂ ℓ₂ e₂} {D₂ : Category o′₂ ℓ′₂ e′₂} → {F₁ G₁ : Functor C₁ D₁} {F₂ G₂ : Functor C₂ D₂} → (α : NaturalTransformation F₁ G₁) → (β : NaturalTransformation F₂ G₂) → NaturalTransformation (F₁ ⁂ F₂) (G₁ ⁂ G₂)
α ⁂ⁿ β = record { η = map⁎′ α.η β.η; commute = map⁎′ α.commute β.commute }
         where
         module α = NaturalTransformation α
         module β = NaturalTransformation β

infixr 2 _※ⁿ_
_※ⁿ_ : ∀ {o ℓ e o′₁ ℓ′₁ e′₁} {C : Category o ℓ e} {D₁ : Category o′₁ ℓ′₁ e′₁} {F₁ G₁ : Functor C D₁} (α : NaturalTransformation F₁ G₁) → ∀ {o′₂ ℓ′₂ e′₂} {D₂ : Category o′₂ ℓ′₂ e′₂} {F₂ G₂ : Functor C D₂} (β : NaturalTransformation F₂ G₂) → NaturalTransformation (F₁ ※ F₂) (G₁ ※ G₂)
α ※ⁿ β = record { η = < α.η , β.η >; commute = < α.commute , β.commute > }
         where
         module α = NaturalTransformation α
         module β = NaturalTransformation β

assocˡ : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃} → (C₁ : Category o₁ ℓ₁ e₁) (C₂ : Category o₂ ℓ₂ e₂) (C₃ : Category o₃ ℓ₃ e₃) → Functor (Product (Product C₁ C₂) C₃) (Product C₁ (Product C₂ C₃))
assocˡ C₁ C₂ C₃ = record
  { F₀ = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
  ; F₁ = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
  ; identity = C₁.Equiv.refl , C₂.Equiv.refl , C₃.Equiv.refl
  ; homomorphism = C₁.Equiv.refl , C₂.Equiv.refl , C₃.Equiv.refl
  ; F-resp-≡ = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
  }
  where
  module C₁ = Category C₁
  module C₂ = Category C₂
  module C₃ = Category C₃

assocʳ : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃} → (C₁ : Category o₁ ℓ₁ e₁) (C₂ : Category o₂ ℓ₂ e₂) (C₃ : Category o₃ ℓ₃ e₃) → Functor (Product C₁ (Product C₂ C₃)) (Product (Product C₁ C₂) C₃)
assocʳ C₁ C₂ C₃ = record
  { F₀ = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
  ; F₁ = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
  ; identity = (C₁.Equiv.refl , C₂.Equiv.refl) , C₃.Equiv.refl
  ; homomorphism = (C₁.Equiv.refl , C₂.Equiv.refl) , C₃.Equiv.refl
  ; F-resp-≡ = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
  }
  where
  module C₁ = Category C₁
  module C₂ = Category C₂
  module C₃ = Category C₃

πˡ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Functor (Product C D) C
πˡ {C = C} = record { F₀ = proj₁; F₁ = proj₁; identity = refl
                    ; homomorphism = refl; F-resp-≡ = proj₁ }
  where open Category.Equiv C using (refl)

πʳ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Functor (Product C D) D
πʳ {D = D} = record { F₀ = proj₂; F₁ = proj₂; identity = refl
                    ; homomorphism = refl; F-resp-≡ = proj₂ }
  where open Category.Equiv D using (refl)

Swap : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Functor (Product D C) (Product C D)
Swap {C = C} {D = D} = (record
  { F₀ = swap
  ; F₁ = swap
  ; identity = C.Equiv.refl , D.Equiv.refl
  ; homomorphism = C.Equiv.refl , D.Equiv.refl
  ; F-resp-≡ = swap
  })
  where
  module C = Category C
  module D = Category D

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Nat
open import Prelude
open import List
open import core
open import judgemental-erase
open import sensibility
open import moveerase

module checks where
  -- these three judmgements lift the action semantics judgements to relate
  -- an expression and a list of pair-wise composable actions to the
  -- expression that's produced by tracing through the action semantics for
  -- each element in that list.
  --
  -- we do this just by appealing to the original judgement with
  -- constraints on the terms to enforce composability.
  --
  -- in all three cases, we assert that the empty list of actions
  -- constitutes a reflexivity step, so when you run out of actions to
  -- preform you have to be where you wanted to be.
  --
  -- note that the only difference between the types for each judgement and
  -- the original action semantics is that the action is now a list of
  -- actions.
  data runtype : (t : τ̂) (Lα : List action) (t' : τ̂) → Set where
     DoRefl : {t : τ̂} → runtype t [] t
     DoType : {t : τ̂} {α : action} {t' t'' : τ̂}
              {L : List action} →
               t + α +> t' →
               runtype t' L t'' →
               runtype t (α :: L) t''

  data runsynth :
    (Γ : ·ctx) (e : ê) (t1 : τ̇) (Lα : List action) (e' : ê) (t2 : τ̇) → Set where
     DoRefl  : {Γ : ·ctx} {e : ê} {t : τ̇} → runsynth Γ e t [] e t
     DoSynth : {Γ : ·ctx} {e : ê} {t : τ̇} {α : action} {e' e'' : ê} {t' t'' : τ̇}
               {L : List action} →
               Γ ⊢ e => t ~ α ~> e' => t' →
               runsynth Γ e' t' L e'' t'' →
               runsynth Γ e t (α :: L) e'' t''

  data runana : (Γ : ·ctx) (e : ê) (Lα : List action) (e' : ê) (t : τ̇) → Set where
     DoRefl : {Γ : ·ctx} {e : ê} {t : τ̇} → runana Γ e [] e t
     DoAna : {Γ : ·ctx} {e : ê} {α : action} {e' e'' : ê} {t : τ̇}
              {L : List action} →
              Γ ⊢ e ~ α ~> e' ⇐ t →
              runana Γ e' L e'' t →
              runana Γ e (α :: L) e'' t

  -- all three run judgements lift to the list monoid as expected. these
  -- theorems are simple because the structure of lists is simple, but they
  -- amount a reasoning principle about the composition of action sequences
  -- by letting you split lists in (nearly) arbitrary places and argue
  -- about the consequences of the splits before composing them together.
  runtype++ : ∀{t t' t'' L1 L2 }
                → runtype t  L1 t'
                → runtype t' L2 t''
                → runtype t (L1 ++ L2) t''
  runtype++ DoRefl d2 = d2
  runtype++ (DoType x d1) d2 = DoType x (runtype++ d1 d2)

  runsynth++ : ∀{Γ e t L1 e' t' L2 e'' t''}
                → runsynth Γ e t L1 e' t'
                → runsynth Γ e' t' L2 e'' t''
                → runsynth Γ e t (L1 ++ L2) e'' t''
  runsynth++ DoRefl d2 = d2
  runsynth++ (DoSynth x d1) d2 = DoSynth x (runsynth++ d1 d2)

  runana++ : ∀{Γ e t L1 e' L2 e''}
                → runana Γ e  L1 e' t
                → runana Γ e' L2 e'' t
                → runana Γ e (L1 ++ L2) e'' t
  runana++ DoRefl d2 = d2
  runana++ (DoAna x d1) d2 = DoAna x (runana++ d1 d2)

  -- the following collection of lemmas asserts that the various runs
  -- interoperate nicely. in many cases, these amount to observing
  -- something like congruence: if a subterm is related to something by one
  -- of the judgements, it can be replaced by the thing to which it is
  -- related in a larger context without disrupting that larger
  -- context.
  --
  -- taken together, this is a little messier than a proper congruence,
  -- because the action semantics demand well-typedness at each step, and
  -- therefore there are enough premises to each lemma to supply to the
  -- action semantics rules.
  --
  -- therefore, these amount to a checksum on the zipper actions under the
  -- lifing of the action semantics to the list monoid.
  --
  -- they only check the zipper actions they happen to be include, however,
  -- which is driven by the particular lists we use in the proofs of
  -- contructability and reachability, which may or may not be all of
  -- them. additionally, the lemmas given here are what is needed for these
  -- proofs, not anything that's more general.

    -- type zippers
  ziplem-tmarr1 : ∀ {t1 t1' t2 L } →
            runtype t1' L t1 →
            runtype (t1' ==>₁ t2) L (t1 ==>₁ t2)
  ziplem-tmarr1 DoRefl = DoRefl
  ziplem-tmarr1 (DoType x L') = DoType (TMArrZip1 x) (ziplem-tmarr1 L')

  ziplem-tmarr2 : ∀ {t1 t2 t2' L } →
            runtype t2' L t2 →
            runtype (t1 ==>₂ t2') L (t1 ==>₂ t2)
  ziplem-tmarr2 DoRefl = DoRefl
  ziplem-tmarr2 (DoType x L') = DoType (TMArrZip2 x) (ziplem-tmarr2 L')

    -- expression zippers
  ziplem-asc1 : ∀{Γ t L e e'} →
        runana Γ e L e' t →
        runsynth Γ (e ·:₁ t) t L (e' ·:₁ t) t
  ziplem-asc1 DoRefl = DoRefl
  ziplem-asc1 (DoAna a r) = DoSynth (SAZipAsc1 a) (ziplem-asc1 r)

  ziplem-asc2 : ∀{Γ t L t' t◆ t'◆} →
               erase-t t t◆ →
               erase-t t' t'◆ →
               runtype t L t' →
               runsynth Γ (⦇-⦈ ·:₂ t) t◆ L (⦇-⦈ ·:₂ t') t'◆
  ziplem-asc2 {Γ} er er' rt with erase-t◆ er | erase-t◆ er'
  ... | refl | refl = ziplem-asc2' {Γ = Γ} rt
   where
     ziplem-asc2' : ∀{t L t' Γ } →
               runtype t L t' →
               runsynth Γ (⦇-⦈ ·:₂ t) (t ◆t) L (⦇-⦈ ·:₂ t') (t' ◆t)
     ziplem-asc2' DoRefl = DoRefl
     ziplem-asc2' (DoType x rt) = DoSynth
                      (SAZipAsc2 x (◆erase-t _ _ refl) (◆erase-t _ _ refl)
                                (ASubsume SEHole TCHole1)) (ziplem-asc2' rt)

  ziplem-lam : ∀ {Γ x e t t1 t2 L e'} →
                   x # Γ →
                   t ▸arr (t1 ==> t2) →
                   runana (Γ ,, (x , t1)) e L e' t2 →
                   runana Γ (·λ x e) L (·λ x e') t
  ziplem-lam a m DoRefl = DoRefl
  ziplem-lam a m (DoAna x₁ d) =  DoAna (AAZipLam a m x₁) (ziplem-lam a m d)

  ziplem-plus1 : ∀{ Γ e L e' f} →
                       runana Γ e L e' num →
                       runsynth Γ (e ·+₁ f) num L (e' ·+₁ f) num
  ziplem-plus1 DoRefl = DoRefl
  ziplem-plus1 (DoAna x d) = DoSynth (SAZipPlus1 x) (ziplem-plus1 d)

  ziplem-plus2 : ∀{ Γ e L e' f} →
                       runana Γ e L e' num →
                       runsynth Γ (f ·+₂ e) num L (f ·+₂ e') num
  ziplem-plus2 DoRefl = DoRefl
  ziplem-plus2 (DoAna x d) = DoSynth (SAZipPlus2 x) (ziplem-plus2 d)

  ziplem-ap2 : ∀{ Γ e L e' t t' f tf} →
                       Γ ⊢ f => t' →
                       t' ▸arr (t ==> tf) →
                       runana Γ e L e' t →
                       runsynth Γ (f ∘₂ e) tf L (f ∘₂ e') tf
  ziplem-ap2 wt m DoRefl = DoRefl
  ziplem-ap2 wt m (DoAna x d) = DoSynth (SAZipApAna m wt x) (ziplem-ap2 wt m d)

  ziplem-nehole-a : ∀{Γ e e' L t t'} →
                (Γ ⊢ e ◆e => t) →
                runsynth Γ e t L e' t' →
                runsynth Γ ⦇⌜ e ⌟⦈ ⦇-⦈ L ⦇⌜ e' ⌟⦈ ⦇-⦈
  ziplem-nehole-a wt DoRefl = DoRefl
  ziplem-nehole-a wt (DoSynth {e = e} x d) =
    DoSynth (SAZipHole (rel◆ e) wt x) (ziplem-nehole-a (actsense-synth (rel◆ e) (rel◆ _) x wt) d)

  ziplem-nehole-b : ∀{Γ e e' L t t' t''} →
                (Γ ⊢ e ◆e => t) →
                (t'' ~ t') →
                runsynth Γ e t L e' t' →
                runana Γ ⦇⌜ e ⌟⦈ L ⦇⌜ e' ⌟⦈ t''
  ziplem-nehole-b wt c DoRefl = DoRefl
  ziplem-nehole-b wt c (DoSynth x rs) =
                     DoAna (AASubsume (erase-in-hole (rel◆ _)) (SNEHole wt) (SAZipHole (rel◆ _) wt x) TCHole1)
                           (ziplem-nehole-b (actsense-synth (rel◆ _) (rel◆ _) x wt) c rs)

  -- because the point of the reachability theorems is to show that we
  -- didn't forget to define any of the action semantic cases, it's
  -- important that theorems include the fact that the witness only uses
  -- move -- otherwise, you could cheat by just prepending [ del ] to the
  -- list produced by constructability. constructability does also use
  -- some, but not all, of the possible movements, so this would no longer
  -- demonstrate the property we really want. to that end, we define a
  -- predicate on lists that they contain only (move _) and that the
  -- various things above that produce the lists we use have this property.

  -- predicate
  data movements : List action → Set where
    AM:: : {L : List action} {δ : direction}
              → movements L
              → movements ((move δ) :: L)
    AM[] : movements []

  -- movements breaks over the list monoid, as expected
  movements++ : {l1 l2 : List action} →
              movements l1 → movements l2 → movements (l1 ++ l2)
  movements++ (AM:: m1) m2 = AM:: (movements++ m1 m2)
  movements++ AM[] m2 = m2

  -- these are zipper lemmas that are specific to list of movement
  -- actions. they are not true for general actions, but because
  -- reachability is restricted to movements, we get some milage out of
  -- them anyway.
  endpoints : ∀{ Γ e t L e' t'} →
                  Γ ⊢ (e ◆e) => t →
                  runsynth Γ e t L e' t' →
                  movements L →
                  t == t'
  endpoints _ DoRefl AM[] = refl
  endpoints wt (DoSynth x rs) (AM:: mv)
    with endpoints (actsense-synth (rel◆ _) (rel◆ _) x wt) rs mv
  ... | refl = π2 (moveerase-synth (rel◆ _) wt x)

  ziplem-moves-asc2 : ∀{ Γ l t t' e t◆ } →
                      movements l →
                      erase-t t t◆ →
                      Γ ⊢ e <= t◆ →
                      runtype t l t' →
                      runsynth Γ (e ·:₂ t) t◆ l (e ·:₂ t') t◆
  ziplem-moves-asc2 _ _ _ DoRefl = DoRefl
  ziplem-moves-asc2 (AM:: m) er wt (DoType x rt) with moveeraset' er x
  ... | er' =  DoSynth (SAZipAsc2 x er' er wt) (ziplem-moves-asc2 m er' wt rt)

  synthana-moves : ∀{t t' l e e' Γ} →
                   Γ ⊢ e ◆e => t' →
                   movements l →
                   t ~ t' →
                   runsynth Γ e t' l e' t' →
                   runana Γ e l e' t
  synthana-moves _ _ _ DoRefl = DoRefl
  synthana-moves wt (AM:: m) c (DoSynth x rs) with π2 (moveerase-synth (rel◆ _) wt x)
  ... | refl = DoAna (AASubsume (rel◆ _) wt x c)
                     (synthana-moves (actsense-synth (rel◆ _) (rel◆ _) x wt) m c rs)

  ziplem-moves-ap1 : ∀{Γ l e1 e1' e2 t t' tx} →
                   Γ ⊢ e1 ◆e => t →
                   t ▸arr (tx ==> t') →
                   Γ ⊢ e2 <= tx →
                   movements l →
                   runsynth Γ e1 t l e1' t →
                   runsynth Γ (e1 ∘₁ e2) t' l (e1' ∘₁ e2) t'
  ziplem-moves-ap1 _ _ _ _ DoRefl = DoRefl
  ziplem-moves-ap1 wt1 mch wt2 (AM:: m) (DoSynth x rs) with π2 (moveerase-synth (rel◆ _) wt1 x)
  ... | refl = DoSynth (SAZipApArr mch (rel◆ _) wt1 x wt2)
                        (ziplem-moves-ap1 (actsense-synth (rel◆ _) (rel◆ _) x wt1)
                                                     mch wt2 m rs)


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

open import Agda.Primitive renaming (Set to _X_X_)

test : _X_X₁_
test = _X_X_

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

open import Agda.Primitive using (Level; lsuc)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product using (proj₁; proj₂; Σ-syntax; _,_)
open import Function.Base using (_∘_)

variable
  ℓ ℓ′ : Level
  A C : Set ℓ
  B : A → Set ℓ

{- Sizes
  Defining sizes as a generalized form of Brouwer ordinals,
  with an order (see https://arxiv.org/abs/2104.02549)
-}

infix 30 ↑_
infix 30 ⊔_

data Size {ℓ} : Set (lsuc ℓ) where
  ↑_ : Size {ℓ} → Size
  ⊔_ : {A : Set ℓ} → (A → Size {ℓ}) → Size

data _≤_ {ℓ} : Size {ℓ} → Size {ℓ} → Set (lsuc ℓ) where
  ↑s≤↑s : ∀ {r s} → r ≤ s → ↑ r ≤ ↑ s
  s≤⊔f  : ∀ {s} f (a : A) → s ≤ f a → s ≤ ⊔ f
  ⊔f≤s  : ∀ {s} f → (∀ (a : A) → f a ≤ s) → ⊔ f ≤ s

-- A possible definition of the smallest size
◯ : Size
◯ = ⊔ ⊥-elim

◯≤s : ∀ {s} → ◯ ≤ s
◯≤s = ⊔f≤s ⊥-elim λ ()

-- Reflexivity of ≤
s≤s : ∀ {s : Size {ℓ}} → s ≤ s
s≤s {s = ↑ s} = ↑s≤↑s s≤s
s≤s {s = ⊔ f} = ⊔f≤s f (λ a → s≤⊔f f a s≤s)

-- Transitivity of ≤
s≤s≤s : ∀ {r s t : Size {ℓ}} → r ≤ s → s ≤ t → r ≤ t
s≤s≤s (↑s≤↑s r≤s) (↑s≤↑s s≤t) = ↑s≤↑s (s≤s≤s r≤s s≤t)
s≤s≤s r≤s (s≤⊔f f a s≤fa) = s≤⊔f f a (s≤s≤s r≤s s≤fa)
s≤s≤s (⊔f≤s f fa≤s) s≤t = ⊔f≤s f (λ a → s≤s≤s (fa≤s a) s≤t)
s≤s≤s (s≤⊔f f a s≤fa) (⊔f≤s f fa≤t) = s≤s≤s s≤fa (fa≤t a)

-- Successor behaves as expected wrt ≤
s≤↑s : ∀ {s : Size {ℓ}} → s ≤ ↑ s
s≤↑s {s = ↑ s} = ↑s≤↑s s≤↑s
s≤↑s {s = ⊔ f} = ⊔f≤s f (λ a → s≤s≤s s≤↑s (↑s≤↑s (s≤⊔f f a s≤s)))

-- Strict order
_<_ : Size {ℓ} → Size {ℓ} → Set (lsuc ℓ)
r < s = ↑ r ≤ s

{- Well-founded induction for Sizes via an
  accessibility predicate based on strict order
-}

record Acc (s : Size {ℓ}) : Set (lsuc ℓ) where
  inductive
  pattern
  constructor acc
  field acc< : (∀ r → r < s → Acc r)
open Acc

-- The accessibility predicate is a mere proposition
accIsProp : ∀ {s : Size {ℓ}} → (acc1 acc2 : Acc s) → acc1 ≡ acc2
accIsProp (acc p) (acc q) =
  cong acc (funext p q (λ r → funext (p r) (q r) (λ r<s → accIsProp (p r r<s) (q r r<s))))
  where postulate funext : ∀ (p q : ∀ x → B x) → (∀ x → p x ≡ q x) → p ≡ q

-- A size smaller or equal to an accessible size is still accessible
acc≤ : ∀ {r s : Size {ℓ}} → r ≤ s → Acc s → Acc r
acc≤ r≤s (acc p) = acc (λ t t<r → p t (s≤s≤s t<r r≤s))

-- All sizes are accessible
wf : ∀ (s : Size {ℓ}) → Acc s
wf (↑ s) = acc (λ { _ (↑s≤↑s r≤s) → acc≤ r≤s (wf s) })
wf (⊔ f) = acc (λ { r (s≤⊔f f a r<fa) → (wf (f a)).acc< r r<fa })

-- Well-founded induction:
-- If P holds on every smaller size, then P holds on this size
-- Recursion occurs structurally on the accessbility of sizes
wfInd : ∀ (P : Size {ℓ} → Set ℓ′) → (∀ s → (∀ r → r < s → P r) → P s) → ∀ s → P s
wfInd P f s = wfAcc s (wf s)
  where
  wfAcc : ∀ s → Acc s → P s
  wfAcc s (acc p) = f s (λ r r<s → wfAcc r (p r r<s))

{- W types
  W∞ is the full or "infinite" form, where there are no sizes;
  W is the bounded-sized form, parameterized by some Size,
  where constructors take a proof of smaller-sizedness
-}

data W∞ (A : Set ℓ) (B : A → Set ℓ) : Set ℓ where
  sup∞ : ∀ a → (B a → W∞ A B) → W∞ A B

data W (A : Set ℓ) (B : A → Set ℓ) (s : Size {ℓ}) : Set (lsuc ℓ) where
  sup : ∀ r → r < s → (a : A) → (B a → W A B r) → W A B s

-- Eliminator for the W type based on wellfoundedness of sizes
elimW : (P : ∀ s → W A B s → Set ℓ′) →
  (p : ∀ s → (∀ r → r < s → (w : W A B r) → P r w) → (w : W A B s) → P s w) →
  ∀ s → (w : W A B s) → P s w
elimW P = wfInd (λ s → (w : W _ _ s) → P s w)

-- A full W∞ to a size-paired bounded-sized W form
findW : W∞ {ℓ} A B → Σ[ s ∈ Size ] W A B s
findW (sup∞ a f) =
  let s = ⊔ (proj₁ ∘ findW ∘ f)
  in ↑ s , sup s s≤s a ⊔f
  where
  ⊔f : _
  ⊔f b with proj₂ (findW (f b))
  ... | sup r r<s a g = sup r (s≤s≤s r<s (s≤⊔f (proj₁ ∘ findW ∘ f) b s≤s)) a g

-- The axiom of choice specialized to sized W types, "choosing" a size
ac : ∀ a → (B a → Σ[ s ∈ Size ] W A B s) → Σ[ s ∈ Size ] (B a → W A B s)
ac a f = ⊔ (proj₁ ∘ f) , f′
  where
  f′ : _
  f′ b with proj₂ (f b)
  ... | sup r r<s a f = sup r (s≤s≤s r<s (s≤⊔f _ b s≤s)) a f

-- Constructing a bounded-sized W out of the necessary pieces
mkW : ∀ a → (B a → Σ[ s ∈ Size ] W A B s) → Σ[ s ∈ Size ] W A B s
mkW a f =
  let sf = ac a f
  in sup (proj₁ sf) ? a (proj₂ f)

max_stars_repo_name: ionathanch/msc-thesis

max_issues_repo_name: ionathanch/msc-thesis

max_forks_repo_name: ionathanch/msc-thesis


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

module Cubical.Homotopy.Loopspace where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.GroupoidLaws

{- loop space of a pointed type -}
Ω : {ℓ : Level} → Pointed ℓ → Pointed ℓ
Ω (_ , a) = ((a ≡ a) , refl)

{- n-fold loop space of a pointed type -}
Ω^_ : ∀ {ℓ} → ℕ → Pointed ℓ → Pointed ℓ
(Ω^ 0) p = p
(Ω^ (suc n)) p = Ω ((Ω^ n) p)

{- loop space map -}
Ω→ : ∀ {ℓA ℓB} {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → (Ω A →∙ Ω B)
Ω→ (f , f∙) = (λ p → (sym f∙ ∙ cong f p) ∙ f∙) , cong (λ q → q ∙ f∙) (sym (rUnit (sym f∙))) ∙ lCancel f∙


text:
module Sets.ImageSet.Oper where

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

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

module _ where
  open import Data.Boolean
  open import Data.Boolean.Stmt
  open import Data.Either as Either using (_‖_)
  open import Function.Domains

  ∅ : ImageSet{ℓᵢ}(T)
  ∅ = intro empty

  𝐔 : ImageSet{Lvl.of(T)}(T)
  𝐔 = intro id

  singleton : T → ImageSet{ℓᵢ}(T)
  singleton(x) = intro{Index = Unit} \{<> → x}

  pair : T → T → ImageSet{ℓᵢ}(T)
  pair x y = intro{Index = Lvl.Up(Bool)} \{(Lvl.up 𝐹) → x ; (Lvl.up 𝑇) → y}

  _∪_ : ImageSet{ℓᵢ₁}(T) → ImageSet{ℓᵢ₂}(T) → ImageSet{ℓᵢ₁ Lvl.⊔ ℓᵢ₂}(T)
  A ∪ B = intro{Index = Index(A) ‖ Index(B)} (Either.map1 (elem(A)) (elem(B)))

  ⋃ : ImageSet{ℓᵢ}(ImageSet{ℓᵢ}(T)) → ImageSet{ℓᵢ}(T)
  ⋃ A = intro{Index = Σ(Index(A)) (Index ∘ elem(A))} \{(intro ia i) → elem(elem(A)(ia))(i)}

  indexFilter : (A : ImageSet{ℓᵢ}(T)) → (Index(A) → Stmt{ℓ}) → ImageSet{ℓᵢ Lvl.⊔ ℓ}(T)
  indexFilter A P = intro {Index = Σ(Index(A)) P} (elem(A) ∘ Σ.left)

  filter : (T → Stmt{ℓ}) → ImageSet{ℓᵢ}(T) → ImageSet{ℓᵢ Lvl.⊔ ℓ}(T)
  filter P(A) = indexFilter A (P ∘ elem(A))

  indexFilterBool : (A : ImageSet{ℓᵢ}(T)) → (Index(A) → Bool) → ImageSet{ℓᵢ}(T)
  indexFilterBool A f = indexFilter A (IsTrue ∘ f)

  filterBool : (T → Bool) → ImageSet{ℓᵢ}(T) → ImageSet{ℓᵢ}(T)
  filterBool f(A) = indexFilterBool A (f ∘ elem(A))

  map : (X → Y) → (ImageSet{ℓᵢ}(X) → ImageSet{ℓᵢ}(Y))
  map f(A) = intro{Index = Index(A)} (f ∘ elem(A))

  unapply : (X → Y) → ⦃ _ : Equiv{ℓₑ}(Y)⦄ → (Y → ImageSet{Lvl.of(X) Lvl.⊔ ℓₑ}(X))
  unapply f(y) = intro{Index = ∃(x ↦ f(x) ≡ₛ y)} [∃]-witness

  -- unmap : (X → Y) → ⦃ _ : Equiv{ℓₑ}(Y)⦄ → (ImageSet{{!Lvl.of(T) Lvl.⊔ ℓₑ!}}(Y) → ImageSet{Lvl.of(T) Lvl.⊔ ℓₑ}(X))
  -- unmap f(B) = intro{Index = ∃(x ↦ f(x) ∈ B)} [∃]-witness

  ℘ : ImageSet{ℓᵢ}(T) → ImageSet{Lvl.𝐒(ℓᵢ)}(ImageSet{ℓᵢ}(T))
  ℘(A) = intro{Index = Index(A) → Stmt} (indexFilter A)

  _∩_ : ⦃ _ : Equiv{ℓᵢ}(T) ⦄ → ImageSet{ℓᵢ}(T) → ImageSet{ℓᵢ}(T) → ImageSet{ℓᵢ}(T)
  A ∩ B = indexFilter(A) (iA ↦ elem(A) iA ∈ B)

  ⋂ : ⦃ _ : Equiv{ℓᵢ}(T) ⦄ → ImageSet{Lvl.of(T)}(ImageSet{Lvl.of(T)}(T)) → ImageSet{ℓᵢ Lvl.⊔ Lvl.of(T)}(T)
  -- ⋂ As = intro{Index = Σ((iAs : Index(As)) → Index(elem(As) iAs)) (f ↦ (∀{iAs₁ iAs₂} → (elem(elem(As) iAs₁)(f iAs₁) ≡ₛ elem(elem(As) iAs₂)(f iAs₂))))} {!!} (TODO: I think this definition only works with excluded middle because one must determine if an A from AS is empty or not and if it is not, then one can apply its index to the function in the Σ)
  ⋂ As = indexFilter(⋃ As) (iUAs ↦ ∃{Obj = (iAs : Index(As)) → Index(elem(As) iAs)}(f ↦ ∀{iAs} → (elem(⋃ As) iUAs ≡ₛ elem(elem(As) iAs) (f iAs))))
  -- ⋂ As = indexFilter(⋃ As) (iUAs ↦ ∀{iAs} → (elem(⋃ As) iUAs ∈ elem(As) iAs))

  {-
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  open import Data.Boolean
  open import Data.Either as Either using (_‖_)
  open import Data.Tuple as Tuple using (_⨯_ ; _,_)
  import      Structure.Container.SetLike as Sets
  open import Structure.Function.Domain
  open import Structure.Operator.Properties
  open import Structure.Relator
  open import Structure.Relator.Properties
  open import Syntax.Transitivity

  private variable A B C : ImageSet{ℓₑ}(T)
  private variable x y a b : T

  [∈]-of-elem : ∀{ia : Index(A)} → (elem(A)(ia) ∈ A)
  ∃.witness ([∈]-of-elem {ia = ia}) = ia
  ∃.proof    [∈]-of-elem = reflexivity(_≡ₛ_)

  instance
    ∅-membership : Sets.EmptySet(_∈_ {T = T}{ℓ})
    Sets.EmptySet.∅          ∅-membership = ∅
    Sets.EmptySet.membership ∅-membership ()

  instance
    𝐔-membership : Sets.UniversalSet(_∈_ {T = T})
    Sets.UniversalSet.𝐔          𝐔-membership = 𝐔
    Sets.UniversalSet.membership 𝐔-membership {x = x} = [∃]-intro x ⦃ reflexivity(_≡ₛ_) ⦄

  instance
    singleton-membership : Sets.SingletonSet(_∈_ {T = T}{ℓ})
    Sets.SingletonSet.singleton singleton-membership = singleton
    Sets.SingletonSet.membership singleton-membership = proof where
      proof : (x ∈ singleton{ℓᵢ = ℓᵢ}(a)) ↔ (x ≡ₛ a)
      Tuple.left  proof xin = [∃]-intro <> ⦃ xin ⦄
      Tuple.right proof ([∃]-intro i ⦃ eq ⦄ ) = eq

  instance
    pair-membership : Sets.PairSet(_∈_ {T = T}{ℓ})
    Sets.PairSet.pair pair-membership = pair
    Sets.PairSet.membership pair-membership = proof where
      proof : (x ∈ pair a b) ↔ (x ≡ₛ a)∨(x ≡ₛ b)
      Tuple.left  proof ([∨]-introₗ p) = [∃]-intro (Lvl.up 𝐹) ⦃ p ⦄
      Tuple.left  proof ([∨]-introᵣ p) = [∃]-intro (Lvl.up 𝑇) ⦃ p ⦄
      Tuple.right proof ([∃]-intro (Lvl.up 𝐹) ⦃ eq ⦄) = [∨]-introₗ eq
      Tuple.right proof ([∃]-intro (Lvl.up 𝑇) ⦃ eq ⦄) = [∨]-introᵣ eq

  instance
    [∪]-membership : Sets.UnionOperator(_∈_ {T = T})
    Sets.UnionOperator._∪_        [∪]-membership = _∪_
    Sets.UnionOperator.membership [∪]-membership = proof where
      proof : (x ∈ (A ∪ B)) ↔ (x ∈ A)∨(x ∈ B)
      Tuple.left  proof ([∨]-introₗ ([∃]-intro  ia)) = [∃]-intro (Either.Left  ia)
      Tuple.left  proof ([∨]-introᵣ ([∃]-intro  ib)) = [∃]-intro (Either.Right ib)
      Tuple.right proof ([∃]-intro  ([∨]-introₗ ia)) = [∨]-introₗ ([∃]-intro ia)
      Tuple.right proof ([∃]-intro  ([∨]-introᵣ ib)) = [∨]-introᵣ ([∃]-intro ib)

  instance
    [∩]-membership : Sets.IntersectionOperator(_∈_ {T = T})
    Sets.IntersectionOperator._∩_        [∩]-membership = _∩_
    Sets.IntersectionOperator.membership [∩]-membership = proof where
      proof : (x ∈ (A ∩ B)) ↔ (x ∈ A)∧(x ∈ B)
      _⨯_.left proof ([↔]-intro ([∃]-intro iA ⦃ pA ⦄) ([∃]-intro iB ⦃ pB ⦄)) = [∃]-intro (intro iA ([∃]-intro iB ⦃ symmetry(_≡ₛ_) pA 🝖 pB ⦄))
      _⨯_.right proof ([∃]-intro (intro iA ([∃]-intro iB ⦃ pAB ⦄)) ⦃ pxAB ⦄) = [∧]-intro ([∃]-intro iA) ([∃]-intro iB ⦃ pxAB 🝖 pAB ⦄)

  instance
    map-membership : Sets.MapFunction(_∈_ {T = T})(_∈_ {T = T})
    Sets.MapFunction.map        map-membership f = map f
    Sets.MapFunction.membership map-membership {f = f} ⦃ function ⦄ = proof where
      proof : (y ∈ map f(A)) ↔ ∃(x ↦ (x ∈ A) ∧ (f(x) ≡ₛ y))
      ∃.witness (Tuple.left  (proof)                         ([∃]-intro x ⦃ [∧]-intro xA fxy ⦄)) = [∃]-witness xA
      ∃.proof   (Tuple.left  (proof {y = y} {A = A}) ([∃]-intro x ⦃ [∧]-intro xA fxy ⦄)) =
        y                                🝖[ _≡ₛ_ ]-[ fxy ]-sym
        f(x)                             🝖[ _≡ₛ_ ]-[ congruence₁(f) ⦃ function ⦄ ([∃]-proof xA) ]
        f(elem(A) ([∃]-witness xA))      🝖[ _≡ₛ_ ]-[]
        elem (map f(A)) ([∃]-witness xA) 🝖[ _≡ₛ_ ]-end
      ∃.witness (Tuple.right (proof {A = A}) ([∃]-intro iA))       = elem(A) iA
      ∃.proof   (Tuple.right proof           ([∃]-intro iA ⦃ p ⦄)) = [∧]-intro ([∈]-of-elem {ia = iA}) (symmetry(_≡ₛ_) p)

  indexFilter-membership : ∀{P : Index(A) → Stmt{ℓ}} → (x ∈ indexFilter A P) ↔ ∃(i ↦ (x ≡ₛ elem(A) i) ∧ P(i))
  _⨯_.left indexFilter-membership ([∃]-intro iA ⦃ [∧]-intro xe p ⦄) = [∃]-intro (intro iA p) ⦃ xe ⦄
  _⨯_.right indexFilter-membership ([∃]-intro (intro iA p) ⦃ xe ⦄) = [∃]-intro iA ⦃ [∧]-intro xe p ⦄

  indexFilter-subset : ∀{P : Index(A) → Stmt{ℓₑ}} → (indexFilter{ℓₑ} A P ⊆ A)
  indexFilter-subset = [∃]-map-proof [∧]-elimₗ ∘ [↔]-to-[→] indexFilter-membership

  indexFilter-elem-membershipₗ : ∀{P : Index(A) → Stmt{ℓ}}{i : Index(A)} → (elem(A)(i) ∈ indexFilter A P) ← P(i)
  indexFilter-elem-membershipₗ {i = i} pi = [∃]-intro (intro i pi) ⦃ reflexivity _ ⦄

  indexFilter-elem-membershipᵣ : ⦃ _ : Equiv{ℓₑ}(Index(A)) ⦄ ⦃ _ : Injective(elem A) ⦄ → ∀{P : Index(A) → Stmt{ℓ}} ⦃ _ : UnaryRelator(P) ⦄{i : Index(A)} → (elem(A)(i) ∈ indexFilter A P) → P(i)
  indexFilter-elem-membershipᵣ {A = A}{P = P} {i = i} ([∃]-intro (intro iA PiA) ⦃ p ⦄) = substitute₁ₗ(P) (injective(elem A) p) PiA

  instance
    filter-membership : Sets.FilterFunction(_∈_ {T = T})
    Sets.FilterFunction.filter     filter-membership f       = filter{ℓ = ℓₑ} f
    Sets.FilterFunction.membership filter-membership {P = P} = proof where
      proof : (x ∈ filter P(A)) ↔ ((x ∈ A) ∧ P(x))
      Tuple.left proof ([∧]-intro ([∃]-intro i ⦃ p ⦄) pb) = [∃]-intro (intro i (substitute₁(P) p pb)) ⦃ p ⦄
      Tuple.left  (Tuple.right proof ([∃]-intro (intro iA PiA)))        = [∃]-intro iA
      Tuple.right (Tuple.right proof ([∃]-intro (intro iA PiA) ⦃ pp ⦄)) = substitute₁ₗ(P) pp PiA

  filter-subset : ∀{P : T → Stmt{ℓₑ}} → (filter P(A) ⊆ A)
  filter-subset ([∃]-intro (intro i p) ⦃ xf ⦄) = [∃]-intro i ⦃ xf ⦄

  instance
    postulate [∩]-commutativity : Commutativity(_∩_ {T = T})

  -- TODO: These should come from Structure.Container.SetLike, which in turn should come from Structure.Operator.Lattice, which in turn should come from Structure.Relator.Ordering.Lattice
  postulate [∩]-subset-of-right : (A ⊆ B) → (A ∩ B ≡ₛ B)
  postulate [∩]-subset-of-left : (B ⊆ A) → (A ∩ B ≡ₛ A)
  postulate [∩]-subsetₗ : (A ∩ B) ⊆ A
  [∩]-subsetᵣ : (A ∩ B) ⊆ B
  [∩]-subsetᵣ {A} {B} {x} xAB = indexFilter-subset ([↔]-to-[→] (commutativity(_∩_) ⦃ [∩]-commutativity ⦄ {A} {B} {x}) xAB)

  instance
    ℘-membership : Sets.PowerFunction(_∈_)(_∈_)
    Sets.PowerFunction.℘ ℘-membership = ℘
    Sets.PowerFunction.membership ℘-membership = [↔]-intro l r where
      l : (B ∈ ℘(A)) ← (B ⊆ A)
      ∃.witness (l {B} {A} BA) iA = elem(A) iA ∈ B
      _⨯_.left (∃.proof (l {B}{A} BA) {x}) a = apply a $
        A ∩ B 🝖[ _⊆_ ]-[ [∩]-subsetᵣ ]
        B     🝖[ _⊆_ ]-end
      _⨯_.right (∃.proof (l {B}{A} BA) {x}) b = apply b $
        B     🝖[ _⊆_ ]-[ BA ]
        A     🝖[ _⊆_ ]-[ sub₂(_≡_)(_⊇_) ([∩]-subset-of-left BA) ]
        A ∩ B 🝖[ _⊆_ ]-end

      r : (B ∈ ℘(A)) → (B ⊆ A)
      r ([∃]-intro _ ⦃ BA ⦄) xB with [↔]-to-[→] BA xB
      ... | [∃]-intro (intro iA _) ⦃ xe ⦄ = [∃]-intro iA ⦃ xe ⦄
-}


text:
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.String using (String)
open import Agda.Builtin.Unit using (⊤)

data D : Set where
  c₁ c₂ : D

f : D → Set → String
f c₁ = λ _ → "OK"
f c₂ = λ _ → "OK"

-- The following pragma should refer to the generated Haskell name
-- for f.

{-# FOREIGN GHC {-# NOINLINE d_f_8 #-} #-}

x : String
x = f c₁ ⊤

postulate
  putStrLn : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStrLn = Data.Text.IO.putStrLn #-}

main : IO ⊤
main = putStrLn x

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

module Issue424 where

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

f : Set → Set
f A = A
f A = A

fails : (A : Set) → f A ≡ A
fails A = refl

-- The case tree compiler used to treat f as a definition with an
-- absurd pattern.

max_forks_repo_name: Agda-zh/agda


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

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Function.Base using (_∋_; _$_)

open import MorePropAlgebra.Bundles
import Cubical.Structures.CommRing as Std

module MorePropAlgebra.Properties.CommRing {ℓ} (assumptions : CommRing {ℓ}) where
open CommRing assumptions renaming (Carrier to R)

import MorePropAlgebra.Properties.Ring
module Ring'Properties = MorePropAlgebra.Properties.Ring   (record { CommRing assumptions })
module Ring'           =                            Ring   (record { CommRing assumptions })
(      Ring')          =                            Ring ∋ (record { CommRing assumptions })

stdIsCommRing : Std.IsCommRing 0r 1r _+_ _·_ (-_)
stdIsCommRing .Std.IsCommRing.isRing = Ring'Properties.stdIsRing
stdIsCommRing .Std.IsCommRing.·-comm = ·-comm

stdCommRing : Std.CommRing {ℓ}
stdCommRing = record { CommRing assumptions ; isCommRing = stdIsCommRing }
--
-- module RingTheory' = Std.Theory stdRing

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Trie, basic type and operations
------------------------------------------------------------------------

-- See README.Data.Trie.NonDependent for an example of using a trie to
-- build a lexer.

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

open import Relation.Binary using (Rel; StrictTotalOrder)

module Data.Trie {k e r} (S : StrictTotalOrder k e r) where

open import Level
open import Size
open import Data.List.Base using (List; []; _∷_; _++_)
import Data.List.NonEmpty as List⁺
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe′)
open import Data.Product as Prod using (∃)
open import Data.These.Base as These using (These)
open import Function
open import Relation.Unary using (IUniversal; _⇒_)

open StrictTotalOrder S
  using (module Eq)
  renaming (Carrier to Key)

open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid
open import Data.AVL.Value ≋-setoid using (Value)

------------------------------------------------------------------------
-- Definition

-- Trie is defined in terms of Trie⁺, the type of non-empty trie. This
-- guarantees that the trie is minimal: each path in the tree leads to
-- either a value or a number of non-empty sub-tries.

open import Data.Trie.NonEmpty S as Trie⁺ public
  using (Trie⁺; Tries⁺; Word; eat)

Trie : ∀ {v} (V : Value v) → Size → Set (v ⊔ k ⊔ e ⊔ r)
Trie V i = Maybe (Trie⁺ V i)

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

-- Functions acting on Trie are wrappers for functions acting on Tries.
-- Sometimes the empty case is handled in a special way (e.g. insertWith
-- calls singleton when faced with an empty Trie).

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

  private Val = Value.family V

------------------------------------------------------------------------
-- Lookup

  lookup : ∀ ks → Trie V ∞ → Maybe (These (Val ks) (Tries⁺ (eat V ks) ∞))
  lookup ks t = t Maybe.>>= Trie⁺.lookup ks

  lookupValue : ∀ ks → Trie V ∞ → Maybe (Val ks)
  lookupValue ks t = t Maybe.>>= Trie⁺.lookupValue ks

  lookupTries⁺ : ∀ ks → Trie V ∞ → Maybe (Tries⁺ (eat V ks) ∞)
  lookupTries⁺ ks t = t Maybe.>>= Trie⁺.lookupTries⁺ ks

  lookupTrie : ∀ k → Trie V ∞ → Trie (eat V (k ∷ [])) ∞
  lookupTrie k t = t Maybe.>>= Trie⁺.lookupTrie⁺ k

------------------------------------------------------------------------
-- Construction

  empty : Trie V ∞
  empty = nothing

  singleton : ∀ ks → Val ks → Trie V ∞
  singleton ks v = just (Trie⁺.singleton ks v)

  insertWith : ∀ ks → (Maybe (Val ks) → Val ks) → Trie V ∞ → Trie V ∞
  insertWith ks f (just t) = just (Trie⁺.insertWith ks f t)
  insertWith ks f nothing  = singleton ks (f nothing)

  insert : ∀ ks → Val ks → Trie V ∞ → Trie V ∞
  insert ks = insertWith ks ∘′ const

  fromList : List (∃ Val) → Trie V ∞
  fromList = Maybe.map Trie⁺.fromList⁺ ∘′ List⁺.fromList

  toList : Trie V ∞ → List (∃ Val)
  toList (just t) = List⁺.toList (Trie⁺.toList⁺ t)
  toList nothing  = []

------------------------------------------------------------------------
-- Modification

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

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

  map : ∀ {i} → ∀[ Val ⇒ Wal ] → Trie V i → Trie W i
  map = Maybe.map ∘′ Trie⁺.map V W

-- Deletion

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

  -- Use a function to decide how to modify the sub-Trie⁺ whose root is
  -- at the end of path ks.
  deleteWith : ∀ {i} (ks : Word) →
     (∀ {i} → Trie⁺ (eat V ks) i → Maybe (Trie⁺ (eat V ks) i)) →
     Trie V i → Trie V i
  deleteWith ks f t = t Maybe.>>= Trie⁺.deleteWith ks f

  -- Remove the whole node
  deleteTrie⁺ : ∀ {i} (ks : Word) → Trie V i → Trie V i
  deleteTrie⁺ ks t = t Maybe.>>= Trie⁺.deleteTrie⁺ ks

  -- Remove the value and keep the sub-Tries (if any)
  deleteValue : ∀ {i} (ks : Word) → Trie V i → Trie V i
  deleteValue ks t = t Maybe.>>= Trie⁺.deleteValue ks

  -- Remove the sub-Tries and keep the value (if any)
  deleteTries⁺ : ∀ {i} (ks : Word) → Trie V i → Trie V i
  deleteTries⁺ ks t = t Maybe.>>= Trie⁺.deleteTries⁺ ks


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Logical relation for erasure (Def. 3.8 and Lemma 3.9)
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Denotation.Value as Value
import Parametric.Denotation.Evaluation as Evaluation
import Parametric.Change.Validity as Validity
import Parametric.Change.Specification as Specification
import Parametric.Change.Type as ChangeType
import Parametric.Change.Value as ChangeValue
import Parametric.Change.Derive as Derive

module Parametric.Change.Implementation
    {Base : Type.Structure}
    (Const : Term.Structure Base)
    (⟦_⟧Base : Value.Structure Base)
    (⟦_⟧Const : Evaluation.Structure Const ⟦_⟧Base)
    (ΔBase : ChangeType.Structure Base)
    {{validity-structure : Validity.Structure ⟦_⟧Base}}
    (⟦apply-base⟧ : ChangeValue.ApplyStructure Const ⟦_⟧Base ΔBase)
    (⟦diff-base⟧ : ChangeValue.DiffStructure Const ⟦_⟧Base ΔBase)
    (⟦nil-base⟧ : ChangeValue.NilStructure Const ⟦_⟧Base ΔBase)
    (derive-const : Derive.Structure Const ΔBase)
  where

open Type.Structure Base
open Term.Structure Base Const
open Value.Structure Base ⟦_⟧Base
open Evaluation.Structure Const ⟦_⟧Base ⟦_⟧Const
open Validity.Structure ⟦_⟧Base {{validity-structure}}
open ChangeType.Structure Base ΔBase
open ChangeValue.Structure Const ⟦_⟧Base ΔBase ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧
open Derive.Structure Const ΔBase derive-const

open import Base.Denotation.Notation

open import Relation.Binary.PropositionalEquality
open import Postulate.Extensionality

record Structure : Set₁ where

  ----------------
  -- Parameters --
  ----------------

  field
    -- Extension point 1: Logical relation on base types.
    --
    -- In the paper, we assume that the logical relation is equality on base types
    -- (see Def. 3.8a). Here, we only require that plugins define what the logical
    -- relation is on base types, and provide proofs for the two extension points
    -- below.
    implements-base : ∀ ι {v : ⟦ ι ⟧Base} → Δ₍ ι ₎ v → ⟦ ΔBase ι ⟧Type → Set

    -- Extension point 2: Differences on base types are logically related.
    u⊟v≈u⊝v-base : ∀ ι {u v : ⟦ ι ⟧Base} →
      implements-base ι (u ⊟₍ ι ₎ v) (⟦diff-base⟧ ι u v)

    nil-v≈⟦nil⟧-v-base : ∀ ι {v : ⟦ ι ⟧Base} →
      implements-base ι (nil₍ ι ₎ v) (⟦nil-base⟧ ι v)
    -- Extension point 3: Lemma 3.1 for base types.
    carry-over-base : ∀ {ι}
      {v : ⟦ ι ⟧Base}
      (Δv : Δ₍ ι ₎ v)
      {Δv′ : ⟦ ΔBase ι ⟧Type} (Δv≈Δv′ : implements-base ι Δv Δv′) →
        v ⊞₍ base ι ₎ Δv ≡ v ⟦⊕₍ base ι ₎⟧ Δv′

  ------------------------
  -- Logical relation ≈ --
  ------------------------

  infix 4 implements
  syntax implements τ u v = u ≈₍ τ ₎ v
  implements : ∀ τ {v} → Δ₍ τ ₎ v → ⟦ ΔType τ ⟧ → Set

  implements (base ι) Δf Δf′ = implements-base ι Δf Δf′
  implements (σ ⇒ τ) {f} Δf Δf′ =
    (w : ⟦ σ ⟧) (Δw : Δ₍ σ ₎ w)
    (Δw′ : ⟦ ΔType σ ⟧) (Δw≈Δw′ : implements σ {w} Δw Δw′) →
    implements τ {f w} (call-change {σ} {τ} Δf w Δw) (Δf′ w Δw′)

  infix 4 _≈_
  _≈_ : ∀ {τ v} → Δ₍ τ ₎ v → ⟦ ΔType τ ⟧ → Set
  _≈_ {τ} {v} = implements τ {v}

  data implements-env : ∀ Γ → {ρ : ⟦ Γ ⟧} (dρ : Δ₍ Γ ₎ ρ) → ⟦ mapContext ΔType Γ ⟧ → Set where
    ∅ : implements-env ∅ {∅} ∅ ∅
    _•_ : ∀ {τ Γ v ρ dv dρ v′ ρ′} →
      (dv≈v′ : implements τ {v} dv v′) →
      (dρ≈ρ′ : implements-env Γ {ρ} dρ ρ′) →
      implements-env (τ • Γ) {v • ρ} (dv • dρ) (v′ • ρ′)

  ----------------
  -- carry-over --
  ----------------

  -- This is lemma 3.10.
  carry-over : ∀ {τ}
    {v : ⟦ τ ⟧}
    (Δv : Δ₍ τ ₎ v)
    {Δv′ : ⟦ ΔType τ ⟧} (Δv≈Δv′ : Δv ≈₍ τ ₎ Δv′) →
      after₍ τ ₎ Δv ≡ before₍ τ ₎ Δv ⟦⊕₍ τ ₎⟧ Δv′

  u⊟v≈u⊝v : ∀ {τ : Type} {u v : ⟦ τ ⟧} →
    u ⊟₍ τ ₎ v ≈₍ τ ₎ u ⟦⊝₍ τ ₎⟧ v

  u⊟v≈u⊝v {base ι} {u} {v} = u⊟v≈u⊝v-base ι {u} {v}
  u⊟v≈u⊝v {σ ⇒ τ} {g} {f} w Δw Δw′ Δw≈Δw′ =
    subst
      (λ □ → (g □ ⊟₍ τ ₎ f (before₍ σ ₎ Δw)) ≈₍ τ ₎ g (before₍ σ ₎ Δw ⟦⊕₍ σ ₎⟧ Δw′) ⟦⊝₍ τ ₎⟧ f (before₍ σ ₎ Δw))
      (sym (carry-over {σ} Δw Δw≈Δw′))
      (u⊟v≈u⊝v {τ} {g (before₍ σ ₎ Δw ⟦⊕₍ σ ₎⟧ Δw′)} {f (before₍ σ ₎ Δw)})

  nil-v≈⟦nil⟧-v : ∀ {τ : Type} {v : ⟦ τ ⟧} →
    nil₍ τ ₎ v ≈₍ τ ₎ (⟦nil₍ τ ₎⟧ v)
  nil-v≈⟦nil⟧-v {base ι} = nil-v≈⟦nil⟧-v-base ι
  nil-v≈⟦nil⟧-v {σ ⇒ τ} {f} = u⊟v≈u⊝v {σ ⇒ τ} {f} {f}

  carry-over {base ι} Δv Δv≈Δv′ = carry-over-base Δv Δv≈Δv′
  carry-over {σ ⇒ τ} {f} Δf {Δf′} Δf≈Δf′ =
    ext (λ v →
      carry-over {τ} {f v} (call-change {σ} {τ} Δf v (nil₍ σ ₎ v))
        {Δf′ v (⟦nil₍ σ ₎⟧ v)}
        (Δf≈Δf′ v (nil₍ σ ₎ v) (⟦nil₍ σ ₎⟧ v) (nil-v≈⟦nil⟧-v {σ} {v})))

  -- A property relating `alternate` and the subcontext relation Γ≼ΔΓ
  ⟦Γ≼ΔΓ⟧ : ∀ {Γ} (ρ : ⟦ Γ ⟧) (dρ : ⟦ mapContext ΔType Γ ⟧) →
    ρ ≡ ⟦ Γ≼ΔΓ ⟧≼ (alternate ρ dρ)
  ⟦Γ≼ΔΓ⟧ ∅ ∅ = refl
  ⟦Γ≼ΔΓ⟧ (v • ρ) (dv • dρ) = cong₂ _•_ refl (⟦Γ≼ΔΓ⟧ ρ dρ)

  -- A specialization of the soundness of weakening
  ⟦fit⟧ : ∀ {τ Γ} (t : Term Γ τ) (ρ : ⟦ Γ ⟧) (dρ : ⟦ mapContext ΔType Γ ⟧) →
    ⟦ t ⟧ ρ ≡ ⟦ fit t ⟧ (alternate ρ dρ)
  ⟦fit⟧ t ρ dρ =
    trans (cong ⟦ t ⟧ (⟦Γ≼ΔΓ⟧ ρ dρ)) (sym (weaken-sound t _))

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

data I : Set where
  it : I

data D : I → Set where
  d : D it

data Box : Set where
  [_] : Nat → Box

mutual
  data Code : Set where
    d   : I → Code
    box : Code
    sg  : (a : Code) → (El a → Code) → Code

  El : Code → Set
  El (d i)    = D i
  El box      = Box
  El (sg a f) = Σ (El a) λ x → El (f x)

foo : (i : I) → Code
foo i = sg (d i) aux
  where
    aux : D i → Code
    aux d = sg box λ { [ a ] → box }

crash : ∀ i → El (foo i) → Nat
crash i (d , p) = p


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

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

module _ (Form : Set) where  -- FAILS
-- postulate Form : Set -- WORKS

data Cxt : Set where
  ε : Cxt
  _∙_ : (Γ : Cxt) (A : Form) → Cxt

data _≤_ : (Γ Δ : Cxt) → Set where
  id≤ : ∀{Γ} → Γ ≤ Γ
  weak : ∀{A Γ Δ} (τ : Γ ≤ Δ) → (Γ ∙ A) ≤ Δ
  lift : ∀{A Γ Δ} (τ : Γ ≤ Δ) → (Γ ∙ A) ≤ (Δ ∙ A)

postulate lift-id≤ : ∀{Γ A} → lift id≤ ≡ id≤ {Γ ∙ A}
{-# REWRITE lift-id≤ #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Nat

record R : Set where
  field
    x : Nat

open R {{...}}

f₁ : R

-- This is fine.
x ⦃ f₁ ⦄ = 0

-- WAS: THIS WORKS BUT MAKES NO SENSE!!!
_ : Nat
_ = f₁ {{ .x }}

-- Should raise an error.

-- Illegal hiding in postfix projection  ⦃ .x ⦄
-- when scope checking f₁ ⦃ .x ⦄