text:
module Generic.Lib.Reflection.Core where

open import Agda.Builtin.Reflection using (withNormalisation; Relevance; Visibility; clause) public
open import Reflection
  renaming (visible to expl; hidden to impl; instance′ to inst;
    relevant to rel; irrelevant to irr; pi to absPi; lam to absLam; def to appDef)
  hiding (Arg-info; var; con; meta; visibility; relevance; _≟_; return; _>>=_; _>>_) public
open import Reflection.Argument.Information using (ArgInfo; visibility; relevance) public
import Reflection.Name
open Term    using () renaming (var to appVar; con to appCon; meta to appMeta) public
open Pattern using () renaming (var to patVar; con to patCon) public
open Literal using () renaming (meta to litMeta) public
open Sort public

open import Generic.Lib.Intro
open import Generic.Lib.Equality.Propositional
open import Generic.Lib.Decidable
open import Generic.Lib.Category
open import Generic.Lib.Data.Nat
open import Generic.Lib.Data.String
open import Generic.Lib.Data.Maybe
open import Generic.Lib.Data.Product
open import Generic.Lib.Data.List

open import Data.Vec using (toList)
open import Data.Vec.N-ary using (N-ary; curryⁿ)

infixr 5 _‵→_
infixl 3 _·_

listCurryⁿ : ∀ {α β} {A : Set α} {B : Set β} n -> (List A -> B) -> N-ary n A B
listCurryⁿ n f = curryⁿ {n = n} (f ∘ toList)

named : String -> String
named s = if s == "_" then "x" else s

record Reify {α} (A : Set α) : Set α where
  field reify : A -> Term

  macro
    reflect : A -> Term -> TC _
    reflect = unify ∘ reify
open Reify {{...}} public

pattern pureVar  n = appVar  n []
pattern pureCon  c = appCon  c []
pattern pureDef  f = appDef  f []
pattern pureMeta m = appMeta m []

{-# DISPLAY appVar  i [] = pureVar  i #-}
{-# DISPLAY appCon  c [] = pureCon  c #-}
{-# DISPLAY appDef  f [] = pureDef  f #-}
{-# DISPLAY appMeta m [] = pureMeta m #-}

pattern explInfo r = arg-info expl r
pattern implInfo r = arg-info impl r
pattern instInfo r = arg-info inst r

{-# DISPLAY arg-info expl r = explInfo r #-}
{-# DISPLAY arg-info impl r = implInfo r #-}
{-# DISPLAY arg-info inst r = instInfo r #-}

pattern explRelInfo = explInfo rel
pattern explIrrInfo = explInfo irr
pattern implRelInfo = implInfo rel
pattern implIrrInfo = implInfo irr
pattern instRelInfo = instInfo rel
pattern instIrrInfo = instInfo irr

{-# DISPLAY explInfo rel = explRelInfo #-}
{-# DISPLAY explInfo irr = explIrrInfo #-}
{-# DISPLAY implInfo rel = implRelInfo #-}
{-# DISPLAY implInfo irr = implIrrInfo #-}
{-# DISPLAY instInfo rel = instRelInfo #-}
{-# DISPLAY instInfo irr = instIrrInfo #-}

pattern explArg r x = arg (explInfo r) x
pattern implArg r x = arg (implInfo r) x
pattern instArg r x = arg (instInfo r) x

{-# DISPLAY arg (explInfo r) = explArg r #-}
{-# DISPLAY arg (implInfo r) = implArg r #-}
{-# DISPLAY arg (instInfo r) = instArg r #-}

pattern explRelArg x = explArg rel x
pattern implRelArg x = implArg rel x
pattern instRelArg x = instArg rel x

{-# DISPLAY explArg rel x = explRelArg x #-}
{-# DISPLAY implArg rel x = implRelArg x #-}
{-# DISPLAY instArg rel x = instRelArg x #-}

pattern pi s a b = absPi a (abs s b)

{-# DISPLAY absPi a (abs s b) = pi s a b #-}

pattern explPi r s a b = pi s (explArg r a) b
pattern implPi r s a b = pi s (implArg r a) b
pattern instPi r s a b = pi s (instArg r a) b

{-# DISPLAY pi (explArg r a) s b = explPi r s a b #-}
{-# DISPLAY pi (implArg r a) s b = implPi r s a b #-}
{-# DISPLAY pi (instArg r a) s b = instPi r s a b #-}

pattern explRelPi s a b = explPi rel a s b
pattern explIrrPi s a b = explPi irr a s b
pattern implRelPi s a b = implPi rel a s b
pattern implIrrPi s a b = implPi irr a s b
pattern instRelPi s a b = instPi rel a s b
pattern instIrrPi s a b = instPi irr a s b

{-# DISPLAY explPi rel a s b = explRelPi s a b #-}
{-# DISPLAY explPi irr a s b = explIrrPi s a b #-}
{-# DISPLAY implPi rel a s b = implRelPi s a b #-}
{-# DISPLAY implPi irr a s b = implIrrPi s a b #-}
{-# DISPLAY instPi rel a s b = instRelPi s a b #-}
{-# DISPLAY instPi irr a s b = instIrrPi s a b #-}

pattern lam v s t = absLam v (abs s t)

{-# DISPLAY absLam v (abs s t) = lam v s t #-}

pattern explLam s t = lam expl s t
pattern implLam s t = lam impl s t
pattern instLam s t = lam inst s t

{-# DISPLAY lam expl s t = explLam s t #-}
{-# DISPLAY lam impl s t = implLam s t #-}
{-# DISPLAY lam inst s t = instLam s t #-}

pattern _‵→_ a b = pi "_" (explRelArg a) b

-- No longer parses for whatever reason.
-- {-# DISPLAY pi "_" (explRelArg a) b = a ‵→ b #-}

mutual
  <_>_ : ∀ {α} -> Relevance -> Set α -> Set α
  <_>_ = flip RelValue

  data RelValue {α} (A : Set α) : Relevance -> Set α where
    relv :  A -> < rel > A
    irrv : .A -> < irr > A

elimRelValue : ∀ {r α π} {A : Set α}
             -> (P : ∀ {r} -> < r > A -> Set π)
             -> (∀  x -> P (relv x))
             -> (∀ .x -> P (irrv x))
             -> (x : < r > A)
             -> P x
elimRelValue P f g (relv x) = f x
elimRelValue P f g (irrv x) = g x

unrelv : ∀ {α} {A : Set α} -> < rel > A -> A
unrelv (relv x) = x

-- Is it possible to handle this in some other way that doesn't require a postulate?
-- See the `appRel` function below. Or is the postulate fine?
postulate
  .unirrv : ∀ {α} {A : Set α} -> < irr > A -> A

<_>_~>_ : ∀ {α β} -> Relevance -> Set α -> Set β -> Set (α ⊔ β)
< rel > A ~> B =  A -> B
< irr > A ~> B = .A -> B

lamRel : ∀ {r α β} {A : Set α} {B : Set β} -> (< r > A -> B) -> < r > A ~> B
lamRel {rel} f = λ x -> f (relv x)
lamRel {irr} f = λ x -> f (irrv x)

-- The laziness is intentional.
appRel : ∀ {r α β} {A : Set α} {B : Set β} -> (< r > A ~> B) -> < r > A -> B
appRel {rel} f rx = f (unrelv rx)
appRel {irr} f rx = f (unirrv rx)

Pi : ∀ {α β} i -> (A : Set α) -> (< relevance i > A -> Set β) -> Set (α ⊔ β)
Pi explRelInfo A B =   (x : A)  -> B (relv x)
Pi explIrrInfo A B = . (x : A)  -> B (irrv x)
Pi implRelInfo A B =   {x : A}  -> B (relv x)
Pi implIrrInfo A B = . {x : A}  -> B (irrv x)
Pi instRelInfo A B =  {{x : A}} -> B (relv x)
Pi instIrrInfo A B = .{{x : A}} -> B (irrv x)

lamPi : ∀ {α β} {A : Set α} i {B : < relevance i > A -> Set β} -> (∀ x -> B x) -> Pi i A B
lamPi explRelInfo f = λ x -> f (relv x)
lamPi explIrrInfo f = λ x -> f (irrv x)
lamPi implRelInfo f = f _
lamPi implIrrInfo f = f _
lamPi instRelInfo f = f _
lamPi instIrrInfo f = f _

appPi : ∀ {α β} {A : Set α} i {B : < relevance i > A -> Set β} -> Pi i A B -> ∀ x -> B x
appPi explRelInfo f (relv x) = f x
appPi explIrrInfo f (irrv x) = f x
appPi implRelInfo y (relv x) = y
appPi implIrrInfo y (irrv x) = y
appPi instRelInfo y (relv x) = y {{x}}
appPi instIrrInfo y (irrv x) = y {{x}}

RelEq : ∀ {α} -> Relevance -> Set α -> Set α
RelEq rel A = Eq A
RelEq irr A = ⊤

vis : {A : Set} -> (A -> List (Arg Term) -> Term) -> A -> List Term -> Term
vis k x = k x ∘ map explRelArg

vis# : ∀ {A : Set} n -> (A -> List (Arg Term) -> Term) -> A -> N-ary n Term Term
vis# n k = listCurryⁿ n ∘ vis k

isRelevant : Relevance -> Bool
isRelevant rel = true
isRelevant irr = false

argInfo : ∀ {α} {A : Set α} -> Arg A -> _
argInfo (arg i x) = i

argVal : ∀ {α} {A : Set α} -> Arg A -> A
argVal (arg i x) = x

unExpl : ∀ {α} {A : Set α} -> Arg A -> Maybe A
unExpl (explArg r x) = just x
unExpl  _            = nothing

absName : ∀ {α} {A : Set α} -> Abs A -> String
absName (abs s x) = s

absVal : ∀ {α} {A : Set α} -> Abs A -> A
absVal (abs s x) = x

patVars : List String -> List (Arg Pattern)
patVars = map (explRelArg ∘ patVar ∘ named)

record Data {α} (A : Set α) : Set α where
  no-eta-equality
  constructor packData
  field
    dataName  : Name
    parsTele  : Type
    indsTele  : Type
    consTypes : List A
    consNames : All (const Name) consTypes
open Data public

instance
  NameEq : Eq Name
  NameEq = viaBase Reflection.Name._≟_

  EqRelValue : ∀ {α r} {A : Set α} {{aEq : RelEq r A}} -> Eq (< r > A)
  EqRelValue {A = A} {{aEq}} = record
    { _≟_ = go
    } where
        relv-inj : {x y : A} -> relv x ≡ relv y -> x ≡ y
        relv-inj refl = refl

        go : ∀ {r} {{aEq : RelEq r A}} -> IsSet (< r > A)
        go (relv x) (relv y) = dcong relv relv-inj (x ≟ y)
        go (irrv x) (irrv y) = yes refl

  ArgFunctor : ∀ {α} -> RawFunctor {α} Arg
  ArgFunctor = record
    { _<$>_ = λ{ f (arg i x) -> arg i (f x) }
    }

  AbsFunctor : ∀ {α} -> RawFunctor {α} Abs
  AbsFunctor = record
    { _<$>_ = λ{ f (abs s x) -> abs s (f x) }
    }

  TCMonad : ∀ {α} -> RawMonad {α} TC
  TCMonad = record
    { return = Reflection.return
    ; _>>=_  = Reflection._>>=_
    }

  TCApplicative : ∀ {α} -> RawApplicative {α} TC
  TCApplicative = rawIApplicative

  TCFunctor : ∀ {α} -> RawFunctor {α} TC
  TCFunctor = rawFunctor

keep : (ℕ -> ℕ) -> ℕ -> ℕ
keep ι  0      = 0
keep ι (suc n) = suc (ι n)

{-# TERMINATING #-}
mutual
  ren : (ℕ -> ℕ) -> Term -> Term
  ren ι (appVar v xs)   = appVar (ι v) (rens ι xs)
  ren ι (appCon c xs)   = appCon c (rens ι xs)
  ren ι (appDef f xs)   = appDef f (rens ι xs)
  ren ι (lam v s t)     = lam v s (ren (keep ι) t)
  ren ι (pat-lam cs xs) = undefined where postulate undefined : _
  ren ι (pi s a b)      = pi s (ren ι <$> a) (ren (keep ι) b)
  ren ι (agda-sort s)   = agda-sort (renSort ι s)
  ren ι (lit l)         = lit l
  ren ι (appMeta x xs)  = appMeta x (rens ι xs)
  ren ι  unknown        = unknown

  rens : (ℕ -> ℕ) -> List (Arg Term) -> List (Arg Term)
  rens ι = map (fmap (ren ι))

  renSort : (ℕ -> ℕ) -> Sort -> Sort
  renSort ι (set t) = set (ren ι t)
  renSort ι (lit n) = lit n
  renSort ι unknown = unknown

shiftBy : ℕ -> Term -> Term
shiftBy = ren ∘ _+_

shift : Term -> Term
shift = shiftBy 1

unshiftBy : ℕ -> Term -> Term
unshiftBy n = ren (_∸ n)

isSomeName : Name -> Term -> Bool
isSomeName n (appDef m _) = n == m
isSomeName n (appCon m _) = n == m
isSomeName n  t           = false

{-# TERMINATING #-}
mutual
  mapName : (ℕ -> List (Arg Term) -> Term) -> Name -> Term -> Term
  mapName f n (appVar v xs)   = appVar v (mapNames f n xs)
  mapName f n (appCon m xs)   = (if n == m then f 0 else appCon m) (mapNames f n xs)
  mapName f n (appDef m xs)   = (if n == m then f 0 else appDef m) (mapNames f n xs)
  mapName f n (lam v s t)     = lam v s (mapName (f ∘ suc) n t)
  mapName f n (pat-lam cs xs) = undefined where postulate undefined : _
  mapName f n (pi s a b)      = pi s (mapName f n <$> a) (mapName (f ∘ suc) n b)
  mapName f n (agda-sort s)   = agda-sort (mapNameSort f n s)
  mapName f n (lit l)         = lit l
  mapName f n (appMeta x xs)  = appMeta x (mapNames f n xs)
  mapName f n  unknown        = unknown

  mapNames : (ℕ -> List (Arg Term) -> Term) -> Name -> List (Arg Term) -> List (Arg Term)
  mapNames f n = map (fmap (mapName f n))

  mapNameSort : (ℕ -> List (Arg Term) -> Term) -> Name -> Sort -> Sort
  mapNameSort f n (set t) = set (mapName f n t)
  mapNameSort f n (lit l) = lit l
  mapNameSort f n unknown = unknown

explsOnly : List (Arg Term) -> List Term
explsOnly = mapMaybe unExpl

initType : Type -> Type
initType (pi s a b) = pi s a (initType b)
initType  b         = unknown

lastType : Type -> Type
lastType (pi s a b) = lastType b
lastType  b         = b

-- These two should return just `Type` like everything else.
takePis : ℕ -> Type -> Maybe Type
takePis  0       a         = just unknown
takePis (suc n) (pi s a b) = pi s a <$> takePis n b
takePis  _       _         = nothing

dropPis : ℕ -> Type -> Maybe Type
dropPis  0       a         = just a
dropPis (suc n) (pi s a b) = dropPis n b
dropPis  _       _         = nothing

monoLastType : Type -> Type
monoLastType = go 0 where
  go : ℕ -> Type -> Type
  go n (pi s a b) = go (suc n) b
  go n  b         = unshiftBy n b

appendType : Type -> Type -> Type
appendType (pi s a b) c = pi s a (appendType b c)
appendType  b         c = c

explLamsBy : Type -> Term -> Term
explLamsBy (explPi r s a b) t = explLam s (explLamsBy b t)
explLamsBy (pi       s a b) t = explLamsBy b t
explLamsBy  b               t = t

implicitize : Type -> Type
implicitize (explPi r s a b) = implPi r s a (implicitize b)
implicitize (pi       s a b) = pi       s a (implicitize b)
implicitize  b               = b

leadImpls : Type -> List (Abs Term)
leadImpls (implPi r s a b) = abs s a ∷ leadImpls b
leadImpls  b               = []

pisToAbsArgTypes : Type -> List (Abs (Arg Type))
pisToAbsArgTypes (pi s a b) = abs s a ∷ pisToAbsArgTypes b
pisToAbsArgTypes  b         = []

explPisToAbsTypes : Type -> List (Abs Type)
explPisToAbsTypes (explPi r s a b) = abs s a ∷ explPisToAbsTypes b
explPisToAbsTypes (pi       s a b) = explPisToAbsTypes b
explPisToAbsTypes  b               = []

explPisToNames : Type -> List String
explPisToNames = map absName ∘ explPisToAbsTypes

countPis : Type -> ℕ
countPis = length ∘ pisToAbsArgTypes

countExplPis : Type -> ℕ
countExplPis = length ∘ explPisToAbsTypes

pisToAbsArgVars : ℕ -> Type -> List (Abs (Arg Term))
pisToAbsArgVars (suc n) (pi s (arg i a) b) = abs s (arg i (pureVar n)) ∷ pisToAbsArgVars n b
pisToAbsArgVars  n       b                 = []

pisToArgVars : ℕ -> Type -> List (Arg Term)
pisToArgVars = map absVal % ∘ pisToAbsArgVars

explPisToAbsVars : ℕ -> Type -> List (Abs Term)
explPisToAbsVars (suc n) (explPi r s a b) = abs s (pureVar n) ∷ explPisToAbsVars n b
explPisToAbsVars (suc n) (pi       s a b) = explPisToAbsVars n b
explPisToAbsVars  n       b               = []

throw : ∀ {α} {A : Set α} -> String -> TC A
throw s = typeError (strErr s ∷ [])

panic : ∀ {α} {A : Set α} -> String -> TC A
panic s = throw $ "panic: " ++ˢ s

-- I'll merge these later.
macro
  sate : Name -> Term -> TC _
  sate f ?r =
    getType f >>= λ a ->
    let res = λ app -> quoteTC (vis# (countExplPis a) app f) >>= unify ?r in
    getDefinition f >>= λ
      { (data-cons _) -> res appCon
      ;  _            -> res appDef
      }

  sateMacro : Name -> Term -> TC _
  sateMacro f ?r =
    getType f >>= λ a ->
    quoteTC (vis# (pred (countExplPis a)) appDef f) >>= unify ?r

_·_ : Term -> Term -> Term
_·_ = sate _$_

unshift′ : Term -> Term
unshift′ t = explLam "_" t · sate tt₀

-- A note for myself: `foldℕ (sate lsuc) (sate lzero) n` is not `reify n`:
-- it's damn `lsuc` -- not `suc`.
termLevelOf : Term -> Maybe Term
termLevelOf (agda-sort (set t)) = just t
termLevelOf (agda-sort (lit n)) = just (foldℕ (sate lsuc) (sate lzero) n)
termLevelOf (agda-sort unknown) = just unknown
termLevelOf _ = nothing

instance
  TermReify : Reify Term
  TermReify = record
    { reify = id
    }

  NameReify : Reify Name
  NameReify = record
    { reify = lit ∘′ name
    }

  VisibilityReify : Reify Visibility
  VisibilityReify = record
    { reify = λ
        { expl -> sate expl
        ; impl -> sate impl
        ; inst -> sate inst
        }
    }

  RelevanceReify : Reify Relevance
  RelevanceReify = record
    { reify = λ
        { rel -> sate rel
        ; irr -> sate irr
        }
    }

  ArgInfoReify : Reify ArgInfo
  ArgInfoReify = record
    { reify = λ{ (arg-info v r) -> sate arg-info (reify v) (reify r) }
    }

  ProdReify : ∀ {α β} {A : Set α} {B : A -> Set β}
                {{aReify : Reify A}} {{bReify : ∀ {x} -> Reify (B x)}} -> Reify (Σ A B)
  ProdReify = record
    { reify = uncurry λ x y -> sate _,_ (reify x) (reify y)
    }

  ℕReify : Reify ℕ
  ℕReify = record
    { reify = foldℕ (sate suc) (sate zero)
    }

  ListReify : ∀ {α} {A : Set α} {{aReify : Reify A}} -> Reify (List A)
  ListReify = record
    { reify = foldr (sate _∷_ ∘ reify) (sate [])
    }

  AllReify : ∀ {α β} {A : Set α} {B : A -> Set β} {xs} {{bReify : ∀ {x} -> Reify (B x)}}
           -> Reify (All B xs)
  AllReify {B = B} {{bReify}} = record
    { reify = go _
    } where
        go : ∀ xs -> All B xs -> Term
        go  []       tt      = sate tt₀
        go (x ∷ xs) (y , ys) = sate _,_ (reify {{bReify}} y) (go xs ys)

toTuple : List Term -> Term
toTuple = foldr₁ (sate _,_) (sate tt₀)

curryBy : Type -> Term -> Term
curryBy = go 0 where
  go : ℕ -> Type -> Term -> Term
  go n (pi s (arg (arg-info v r) a) b) t = lam v s $ go (suc n) b t
  go n  _                              t = shiftBy n t · toTuple (map pureVar (downFrom n))

explUncurryBy : Type -> Term -> Term
explUncurryBy a f = explLam "x" $ appDef (quote id) (explArg rel (shift f) ∷ go a (pureVar 0)) where
  go : Term -> Term -> List (Arg Term)
  go (explPi r s a b@(pi _ _ _)) p = explArg r (sate proj₁ p) ∷ go b (sate proj₂ p)
  go (pi       s a b@(pi _ _ _)) p = go b (sate proj₂ p)
  go (explPi r s a b)            x = explArg r x ∷ []
  go  _                          t = []

defineTerm : Name -> Term -> TC _
defineTerm n t =
  getType n >>= λ a ->
  defineFun n (clause (map (implRelArg ∘ patVar ∘ named ∘ absName) (leadImpls a)) t ∷ [])

-- Able to normalize a Setω.
normalize : Term -> TC Term
normalize (pi s (arg i a) b) =
  pi s ∘ arg i <$> normalize a <*> extendContext (arg i a) (normalize b)
normalize  t                 = normalise t

getNormType : Name -> TC Type
getNormType = getType >=> normalize

inferNormType : Term -> TC Type
inferNormType = inferType >=> normalize

getData : Name -> TC (Data Type)
getData d = getNormType d >>= λ ab -> getDefinition d >>= λ
  { (data-type p cs) ->
       mapM (λ c -> _,_ c ∘ dropPis p <$> getNormType c) cs >>= λ mans ->
         case takePis p ab ⊗ (dropPis p ab ⊗ (mapM (uncurry λ c ma -> flip _,_ c <$> ma) mans)) of λ
           {  nothing             -> panic "getData: data"
           ; (just (a , b , acs)) -> return ∘ uncurry (packData d a b) $ splitList acs
           }
  ; (record-type c _) -> getNormType c >>= dropPis (countPis ab) >>> λ
       {  nothing  -> panic "getData: record"
       ; (just a′) -> return $ packData d (initType ab) (lastType ab) (a′ ∷ []) (c , tt)
       }
  ;  _ -> throw "not a data"
  }

macro
  TypeOf : Term -> Term -> TC _
  TypeOf t ?r = inferNormType t >>= unify ?r

  runTC : ∀ {α} {A : Set α} -> TC A -> Term -> TC _
  runTC a ?r = bindTC a quoteTC >>= unify ?r

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.DiffInt where

open import Cubical.Data.DiffInt.Base public
open import Cubical.Data.DiffInt.Properties public

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Globe where

open import Level using (Level; zero)
open import Relation.Binary using (IsEquivalence; module IsEquivalence)
open import Relation.Binary.PropositionalEquality using (isEquivalence)
open import Data.Nat using (ℕ; zero; suc; _<_; _≤_; z≤n; s≤s)

open import Categories.Category

data GlobeHom : (m n : ℕ) → Set where
  I : ∀ {place : ℕ} → GlobeHom place place
  σ : ∀ {n m : ℕ} → GlobeHom (suc n) m → GlobeHom n m
  τ : ∀ {n m : ℕ} → GlobeHom (suc n) m → GlobeHom n m

data GlobeEq : {m n : ℕ} → GlobeHom m n → GlobeHom m n → Set where
  both-I : ∀ {m} → GlobeEq {m} {m} I I
  both-σ : ∀ {m n x y} → GlobeEq {m} {n} (σ x) (σ y)
  both-τ : ∀ {m n x y} → GlobeEq {m} {n} (τ x) (τ y)

GlobeEquiv : ∀ {m n} → IsEquivalence (GlobeEq {m} {n})
GlobeEquiv = record { refl = refl; sym = sym; trans = trans }
  where
  refl : ∀ {m n} {x : GlobeHom m n} → GlobeEq x x
  refl {x = I} = both-I
  refl {x = σ y} = both-σ
  refl {x = τ y} = both-τ
  sym : ∀ {m n} {x y : GlobeHom m n} → GlobeEq x y → GlobeEq y x
  sym both-I = both-I
  sym both-σ = both-σ
  sym both-τ = both-τ
  trans : ∀ {m n} {x y z : GlobeHom m n} → GlobeEq x y → GlobeEq y z → GlobeEq x z
  trans both-I y∼z = y∼z
  trans both-σ both-σ = both-σ
  trans both-τ both-τ = both-τ

infixl 7 _⊚_

_⊚_ : ∀ {l m n} → GlobeHom m n → GlobeHom l m → GlobeHom l n
x ⊚ I = x
x ⊚ σ y = σ (x ⊚ y)
x ⊚ τ y = τ (x ⊚ y)

Globe : Category Level.zero Level.zero Level.zero
Globe = record
  { Obj       = ℕ
  ; _⇒_       = GlobeHom
  ; _≈_       = GlobeEq
  ; id        = I
  ; _∘_       = _⊚_
  ; assoc     = λ {_ _ _ _ f g h} → assoc {f = f} {g} {h}
  ; sym-assoc = λ {_ _ _ _ f g h} → GlobeEquiv.sym (assoc {f = f} {g} {h})
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = GlobeEquiv
  ; ∘-resp-≈  = ∘-resp-≡
  }
  where
  module GlobeEquiv {m n} = IsEquivalence (GlobeEquiv {m} {n})
  assoc : ∀ {A B C D} {f : GlobeHom A B} {g : GlobeHom B C} {h : GlobeHom C D} → GlobeEq ((h ⊚ g) ⊚ f) (h ⊚ (g ⊚ f))
  assoc {f = I} = refl
    where open IsEquivalence GlobeEquiv
  assoc {f = σ y} = both-σ
  assoc {f = τ y} = both-τ
  identityˡ : ∀ {A B} {f : GlobeHom A B} → GlobeEq (I ⊚ f) f
  identityˡ {f = I} = both-I
  identityˡ {f = σ y} = both-σ
  identityˡ {f = τ y} = both-τ
  identityʳ : ∀ {A B} {f : GlobeHom A B} → GlobeEq (f ⊚ I) f
  identityʳ = IsEquivalence.refl GlobeEquiv
  identity² : {m : ℕ} → GlobeEq {m} (I ⊚ I) I
  identity² = both-I
  ∘-resp-≡ : ∀ {A B C} {f h : GlobeHom B C} {g i : GlobeHom A B} → GlobeEq f h → GlobeEq g i → GlobeEq (f ⊚ g) (h ⊚ i)
  ∘-resp-≡ f∼h both-I = f∼h
  ∘-resp-≡ f∼h both-σ = both-σ
  ∘-resp-≡ f∼h both-τ = both-τ

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

open import Examples.Sorting.Sequential.Comparable

module Examples.Sorting.Sequential.MergeSort.Split (M : Comparable) where

open Comparable M
open import Examples.Sorting.Sequential.Core M

open import Calf costMonoid
open import Calf.Types.Nat
open import Calf.Types.List
open import Calf.Types.Bounded costMonoid

open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂)
open import Data.Nat as Nat using (ℕ; zero; suc; _+_; _*_; ⌊_/2⌋; ⌈_/2⌉)
open import Data.Nat.Properties as N using (module ≤-Reasoning)

pair = Σ++ (list A) λ _ → (list A)

split/clocked : cmp (Π nat λ _ → Π (list A) λ _ → F pair)
split/clocked zero    l        = ret ([] , l)
split/clocked (suc k) []       = ret ([] , [])
split/clocked (suc k) (x ∷ xs) = bind (F pair) (split/clocked k xs) λ (l₁ , l₂) → ret (x ∷ l₁ , l₂)

split/clocked/correct : ∀ k k' l → k + k' ≡ length l →
  ◯ (∃ λ l₁ → ∃ λ l₂ → split/clocked k l ≡ ret (l₁ , l₂) × length l₁ ≡ k × length l₂ ≡ k' × l ↭ (l₁ ++ l₂))
split/clocked/correct zero    k' l        refl u = [] , l , refl , refl , refl , refl
split/clocked/correct (suc k) k' (x ∷ xs) h    u =
  let (l₁ , l₂ , ≡ , h₁ , h₂ , ↭) = split/clocked/correct k k' xs (N.suc-injective h) u in
  x ∷ l₁ , l₂ , Eq.cong (λ e → bind (F pair) e _) ≡ , Eq.cong suc h₁ , h₂ , prep x ↭

split/clocked/cost : cmp (Π nat λ _ → Π (list A) λ _ → cost)
split/clocked/cost _ _ = zero

split/clocked≤split/clocked/cost : ∀ k l → IsBounded pair (split/clocked k l) (split/clocked/cost k l)
split/clocked≤split/clocked/cost zero    l        = bound/ret
split/clocked≤split/clocked/cost (suc k) []       = bound/ret
split/clocked≤split/clocked/cost (suc k) (x ∷ xs) = bound/bind/const zero zero (split/clocked≤split/clocked/cost k xs) λ _ → bound/ret

split : cmp (Π (list A) λ _ → F pair)
split l = split/clocked ⌊ length l /2⌋ l

split/correct : ∀ l →
  ◯ (∃ λ l₁ → ∃ λ l₂ → split l ≡ ret (l₁ , l₂) × length l₁ ≡ ⌊ length l /2⌋ × length l₂ ≡ ⌈ length l /2⌉ × l ↭ (l₁ ++ l₂))
split/correct l = split/clocked/correct ⌊ length l /2⌋ ⌈ length l /2⌉ l (N.⌊n/2⌋+⌈n/2⌉≡n (length l))

split/cost : cmp (Π (list A) λ _ → cost)
split/cost l = split/clocked/cost ⌊ length l /2⌋ l

split≤split/cost : ∀ l → IsBounded pair (split l) (split/cost l)
split≤split/cost l = split/clocked≤split/clocked/cost ⌊ length l /2⌋ l

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Group where

open import Cubical.Data.Group.Base public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import lib.Basics
open import lib.types.Group
open import lib.types.Pi
open import lib.NType2
open import lib.types.EilenbergMacLane1.Core

module lib.types.EilenbergMacLane1.DoubleElim where

private

  emloop-emloop-helper : ∀ {i j k} {A : Type i} {B : Type j} {C : A → B → Type k}
    {a : A} (p : a == a)
    {b₀ b₁ : B} (q : b₀ == b₁)
    (f : (b : B) → C a b)
    (g : (b : B) → C a b)
    (r₀ : f b₀ == g b₀ [ (λ a → C a b₀) ↓ p ])
    (r₁ : f b₁ == g b₁ [ (λ a → C a b₁) ↓ p ])
    → ↓-ap-in (λ Z → Z) (λ a → C a b₀) r₀ ∙'ᵈ ↓-ap-in (λ Z → Z) (C a) (apd g q) ==
      ↓-ap-in (λ Z → Z) (C a) (apd f q) ∙ᵈ ↓-ap-in (λ Z → Z) (λ a → C a b₁) r₁
        [ (λ p → f b₀ == g b₁ [ (λ Z → Z) ↓ p ]) ↓ ap-comm' C p q ]
    → r₀ == r₁ [ (λ b → f b == g b [ (λ a → C a b) ↓ p ]) ↓ q ]
  emloop-emloop-helper {C = C} p {b₀} idp f g r₀ r₁ s =
    –>-is-inj (↓-ap-equiv (λ Z → Z) (λ a → C a b₀)) r₀ r₁ $
    (! (▹idp (↓-ap-in (λ Z → Z) (λ a → C a b₀) r₀)) ∙
    s ∙
    idp◃ (↓-ap-in (λ Z → Z) (λ a → C a b₀) r₁))

module _ {i j} (G : Group i) (H : Group j) where

  private
    module G = Group G
    module H = Group H

  module EM₁Level₁DoubleElim {k} {P : EM₁ G → EM₁ H → Type k}
    {{P-level : ∀ x y → has-level 1 (P x y)}}
    (embase-embase* : P embase embase)
    (embase-emloop* : ∀ h → embase-embase* == embase-embase* [ P embase ↓ emloop h ])
    (emloop-embase* : ∀ g → embase-embase* == embase-embase* [ (λ x → P x embase) ↓ emloop g ])
    (embase-emloop-comp* : ∀ h₁ h₂ →
      embase-emloop* (H.comp h₁ h₂) == embase-emloop* h₁ ∙ᵈ embase-emloop* h₂
        [ (λ p → embase-embase* == embase-embase* [ P embase ↓ p ]) ↓ emloop-comp h₁ h₂ ])
    (emloop-comp-embase* : ∀ g₁ g₂ →
      emloop-embase* (G.comp g₁ g₂) == emloop-embase* g₁ ∙ᵈ emloop-embase* g₂
        [ (λ p → embase-embase* == embase-embase* [ (λ x → P x embase) ↓ p ]) ↓ emloop-comp g₁ g₂ ])
    (emloop-emloop* : ∀ g h →
      ↓-ap-in (λ Z → Z) (λ a → P a embase) (emloop-embase* g) ∙'ᵈ
      ↓-ap-in (λ Z → Z) (P embase) (embase-emloop* h)
      ==
      ↓-ap-in (λ Z → Z) (P embase) (embase-emloop* h) ∙ᵈ
      ↓-ap-in (λ Z → Z) (λ a → P a embase) (emloop-embase* g)
        [ (λ p → embase-embase* == embase-embase* [ (λ Z → Z) ↓ p ]) ↓ ap-comm' P (emloop g) (emloop h) ])
    where

    private
      module Embase =
        EM₁Level₁Elim {P = P embase}
                      {{P-level embase}}
                      embase-embase*
                      embase-emloop*
                      embase-emloop-comp*

      P' : embase' G == embase → EM₁ H → Type k
      P' p y = Embase.f y == Embase.f y [ (λ x → P x y) ↓ p ]

      P'-level : ∀ p y → has-level 0 (P' p y)
      P'-level _ y = ↓-level (P-level embase y)

      emloop-emloop** : ∀ g h → emloop-embase* g == emloop-embase* g [ P' (emloop g) ↓ emloop h ]
      emloop-emloop** g h =
        emloop-emloop-helper
          {C = P}
          (emloop g) (emloop h)
          Embase.f Embase.f
          (emloop-embase* g) (emloop-embase* g)
          (transport!
            (λ u →
              ↓-ap-in (λ Z → Z) (λ a → P a embase) (emloop-embase* g) ∙'ᵈ
              ↓-ap-in (λ Z → Z) (P embase) u
              ==
              ↓-ap-in (λ Z → Z) (P embase) u ∙ᵈ
              ↓-ap-in (λ Z → Z) (λ a → P a embase) (emloop-embase* g)
                [ (λ p → embase-embase* == embase-embase* [ (λ Z → Z) ↓ p ]) ↓ ap-comm' P (emloop g) (emloop h) ])
            (Embase.emloop-β h)
            (emloop-emloop* g h))

      module Emloop (g : G.El) =
        EM₁SetElim {P = P' (emloop g)}
                   {{P'-level (emloop g)}}
                   (emloop-embase* g)
                   (emloop-emloop** g)

      module EmloopComp (g₁ g₂ : G.El) =
        EM₁PropElim {P = λ y → Emloop.f (G.comp g₁ g₂) y ==
                               Emloop.f g₁ y ∙ᵈ Emloop.f g₂ y
                                 [ (λ x → P' x y) ↓ emloop-comp g₁ g₂ ]}
                    {{λ y → ↓-level (P'-level _ y)}}
                    (emloop-comp-embase* g₁ g₂)

      module DoubleElim (y : EM₁ H) =
        EM₁Level₁Elim {P = λ x → P x y}
                      {{λ x → P-level x y}}
                      (Embase.f y)
                      (λ g → Emloop.f g y)
                      (λ g₁ g₂ → EmloopComp.f g₁ g₂ y)

    abstract
      f : ∀ x y → P x y
      f x y = DoubleElim.f y x

      embase-embase-β : f embase embase ↦ embase-embase*
      embase-embase-β = Embase.embase-β
      {-# REWRITE embase-embase-β #-}

      embase-emloop-β : ∀ (h : H.El) → apd (λ y → f embase y) (emloop h) == embase-emloop* h
      embase-emloop-β h = Embase.emloop-β h

      emloop-embase-β : ∀ (g : G.El) → apd (λ x → f x embase) (emloop g) == emloop-embase* g
      emloop-embase-β g = DoubleElim.emloop-β embase g

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Results concerning double negation elimination.
------------------------------------------------------------------------

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

module Axiom.DoubleNegationElimination where

open import Axiom.ExcludedMiddle
open import Level
open import Relation.Nullary
open import Relation.Nullary.Negation

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

-- The classical statement of double negation elimination says that
-- if a property is not not true then it is true.

DoubleNegationElimination : (ℓ : Level) → Set (suc ℓ)
DoubleNegationElimination ℓ = {P : Set ℓ} → ¬ ¬ P → P

------------------------------------------------------------------------
-- Properties

-- Double negation elimination is equivalent to excluded middle

em⇒dne : ∀ {ℓ} → ExcludedMiddle ℓ → DoubleNegationElimination ℓ
em⇒dne em = decidable-stable em

dne⇒em : ∀ {ℓ} → DoubleNegationElimination ℓ → ExcludedMiddle ℓ
dne⇒em dne = dne excluded-middle


text:
------------------------------------------------------------------------------
-- Group theory base
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module GroupTheory.Base where

infix  8 _⁻¹
infixl 7 _·_

------------------------------------------------------------------------------
-- First-order logic with equality.
open import Common.FOL.FOL-Eq public renaming ( D to G )

-- Group theory axioms
postulate
  ε   : G          -- The identity element.
  _·_ : G → G → G  -- The binary operation.
  _⁻¹ : G → G      -- The inverse function.

  -- We choose a non-redundant set of axioms. See for example (Mac
  -- Lane and Garret 1999, exercises 5-7, p. 50-51, or Hodges 1993,
  -- p. 37).
  assoc         : ∀ a b c → a · b · c ≡ a · (b · c)
  leftIdentity  : ∀ a → ε · a         ≡ a
  leftInverse   : ∀ a → a ⁻¹ · a      ≡ ε
{-# ATP axioms assoc leftIdentity leftInverse #-}

------------------------------------------------------------------------------
-- References
--
-- Hodges, W. (1993). Model Theory. Vol. 42. Encyclopedia of
-- Mathematics and its Applications. Cambridge University Press.
--
-- Mac Lane, S. and Birkhof, G. (1999). Algebra. 3rd ed. AMS Chelsea
-- Publishing.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module ProcessAlgebra where

open import Data.Nat
open import Data.Nat.Properties
open import Data.List

data Channel : Set where
  ℂ_ : ℕ → Channel

data ℙ : Set₁ where
  ν_[_] : List Channel → (Channel → ℙ) → ℙ
  B_,_ : Channel → ℙ → ℙ
  Send_[_],_ : ∀ {A : Set} → Channel → A → ℙ → ℙ
  Recv_,_ : ∀ {A : Set} → Channel → (A → ℙ) → ℙ
  _||_ : ℙ → ℙ → ℙ
  Dup_ : ℙ → ℙ
  Done : ℙ

data Message : Set₁ where
  _,_of_ : Channel → (A : Set) → A → Message

data Action : Set₁ where
  Out_ : Message → Action
  In_  : Message → Action

data Label : Set₁ where
  Silent : Label
  Act_ : Action → Label

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
-- Andreas, 2018-06-10, issue #3124
-- Wrong context for error IrrelevantDatatype in the coverage checker.

data Squash (A : Set) : Prop where
  squash : A → Squash A

test : ∀{A} → Squash (Squash A → A)
test = squash λ{ (squash y) → y }

-- WAS: de Bruijn index in error message

-- Expected error:
-- Cannot split on argument of irrelevant datatype (Squash .A)
-- when checking the definition of .extendedlambda0

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text: module Categories.Topos where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --universe-polymorphism #-}
module NoBlockOnLevel where

open import Common.Level

infixr 0 _,_
record ∃ {a b} {A : Set a} (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open ∃

BSetoid : ∀ c → Set (lsuc c)
BSetoid c = Set c

infixr 0 _⟶_

postulate
  _⟶_ : ∀ {f t} → BSetoid f → BSetoid t → Set (f ⊔ t)
  →-to-⟶ : ∀ {a b} {A : Set a} {B : BSetoid b} →
           (A → B) → A ⟶ B

postulate
  a b p : Level
  A : Set a
  B : Set b
  P : A → B → Set p

-- This will leave unsolved metas if we give up on an unsolved level constraint
-- when checking argument spines. Since we can't match on levels it's safe to keep
-- checking later constraints even if they depend on the unsolved levels.
f : (∃ λ x → ∃ λ y → P x y) ⟶ (∃ λ y → ∃ λ x → P x y)
f = →-to-⟶ λ p → proj₁ (proj₂ p) , proj₁ p , proj₂ (proj₂ p)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- Andreas, 2017-01-01, issue #2372, reported by m0davis

-- {-# OPTIONS -v tc.def.alias:100 -v tc.decl.instance:100 #-}

-- Expected error:
-- Terms marked as eligible for instance search should end with a name
-- when checking the definition of i

postulate
  D : Set

instance
  i = D  -- NOW: Error given here (as expected).

record R : Set₁ where
  field
    r : Set

open R {{ ... }} public

f : r → Set₁ -- WAS: Here, confusingly, is where Agda registers its complaint.
f _ = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- {-# OPTIONS -v tc.conv:10 #-}

-- 2013-11-03 Reported by sanzhiyan

module Issue933 where

record RGraph : Set₁ where
  field
    O : Set
    R : Set
    refl : O -> R

module Families (Γ : RGraph) where

 module Γ = RGraph Γ

 record RG-Fam : Set₁ where
  field
    O : Γ.O -> Set
    refl : ∀ {γo} -> (o : O γo) → O (Γ.refl γo)

-- "O (Γ.refl γo)" should be a type error.

-- Andreas: Fixed.  SyntacticEquality wrongly just skipped projections.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Luau.StrictMode.ToString where

open import FFI.Data.String using (String; _++_)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr)
open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
open import Luau.Type using (strict)
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Var.ToString using (varToString)
open import Luau.Type.ToString using (typeToString)
open import Luau.Syntax.ToString using (binOpToString)

warningToStringᴱ : ∀ {H Γ T} M → {D : Γ ⊢ᴱ M ∈ T} → Warningᴱ H D → String
warningToStringᴮ : ∀ {H Γ T} B → {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → String

warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x
warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated adress " ++ addrToString a
warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U
warningToStringᴱ (M $ N) (app₁ W) = warningToStringᴱ M W
warningToStringᴱ (M $ N) (app₂ W) = warningToStringᴱ N W
warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V
warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (function₁ W) = warningToStringᴮ B W ++ "\n  in function expression " ++ varToString f
warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) =  "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U
warningToStringᴱ block var b ∈ T is B end (block₁ W) = warningToStringᴮ B W ++ "\n  in block " ++ varToString b
warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T
warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U
warningToStringᴱ (binexp M op N) (bin₁ W) = warningToStringᴱ M W
warningToStringᴱ (binexp M op N) (bin₂ W) = warningToStringᴱ N W

warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V
warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₁ W) = warningToStringᴮ C W ++ "\n  in function declaration " ++ varToString f
warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₂ W) = warningToStringᴮ B W
warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) =  "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U
warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₁ W) = warningToStringᴱ M W ++ "\n  in local variable declaration " ++ varToString x
warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₂ W) = warningToStringᴮ B W
warningToStringᴮ (return M ∙ B) (return W) = warningToStringᴱ M W ++ "\n  in return statement"

max_stars_repo_name: gideros/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax CommGroup | CG

type
  * : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20
  neg  : *  ->  * | ⊖_ r40

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊖N⊕ᴸ) a |> add (neg (a), a) = unit
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = unit
  (⊕C) a b |> add(a, b) = add(b, a)
-}

module CommGroup.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import CommGroup.Signature

private
  variable
    Γ Δ Π : Ctx
    α : *T
    𝔛 : Familyₛ

-- Inductive term declaration
module CG:Terms (𝔛 : Familyₛ) where

  data CG : Familyₛ where
    var  : ℐ ⇾̣ CG
    mvar : 𝔛 α Π → Sub CG Π Γ → CG α Γ

    ε   : CG * Γ
    _⊕_ : CG * Γ → CG * Γ → CG * Γ
    ⊖_  : CG * Γ → CG * Γ

  infixl 20 _⊕_
  infixr 40 ⊖_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  CGᵃ : MetaAlg CG
  CGᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (unitₒ ⋮ _)     → ε
      (addₒ  ⋮ a , b) → _⊕_ a b
      (negₒ  ⋮ a)     → ⊖_  a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module CGᵃ = MetaAlg CGᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : CG ⇾̣ 𝒜
    𝕊 : Sub CG Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞  ε        = 𝑎𝑙𝑔 (unitₒ ⋮ tt)
    𝕤𝕖𝕞 (_⊕_ a b) = 𝑎𝑙𝑔 (addₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (⊖_  a)   = 𝑎𝑙𝑔 (negₒ  ⋮ 𝕤𝕖𝕞 a)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ CGᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ CG α Γ) → 𝕤𝕖𝕞 (CGᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (unitₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (addₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (negₒ  ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ CG ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : CG ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ CGᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : CG α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub CG Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! ε = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_⊕_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (⊖_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
CG:Syn : Syntax
CG:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = CG:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open CG:Terms 𝔛 in record
    { ⊥ = CG ⋉ CGᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax CG:Syn public
open CG:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands CGᵃ public
open import SOAS.Metatheory CG:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Categories.Normalise where

-- Experiments on using computation to simplify equalities

open import Level
open import Function renaming (id to idᶠ; _∘_ to _©_)
open import Data.Product
open import Categories.Support.PropositionalEquality

open import Categories.Category
import Categories.Morphisms as Mor

open import Relation.Binary hiding (_⇒_)

--open import Categories.Object.Coproduct
open import Categories.Object.BinaryCoproducts

open import Categories.Square

-- Normalizing with β and η rules for coproducts, through Yoneda
module +Reasoning {o ℓ e} (C : Category o ℓ e) (bincoprod : BinCoproducts C) where

  private module C = Category C
  open C using (Obj; _≡_; _⇒_; module Equiv)
  open Equiv
  open BinCoproducts C bincoprod
--  open BinaryCoproducts C (Bin→Binary C bincoprod) hiding ([_,_]; i₁; i₂; universal; commute₁; commute₂)

  data Ty : Set o where
    ↑_ : Obj -> Ty
    _⊎_ : Ty -> Ty -> Ty

  T : Ty -> Obj
  T (↑ x) = x
  T (t ⊎ t₁) = T t + T t₁

  data Term : Ty → Ty → Set (o ⊔ ℓ) where
    #id : ∀ {A} → Term A A
    #i₁ : ∀ {A B} → Term A (A ⊎ B)
    #i₂ : ∀ {A B} → Term B (A ⊎ B)
    #[_,_] : ∀ {A B C} → Term A C → Term B C → Term (A ⊎ B) C
    _#∘_ : ∀ {A B C} → Term B C → Term A B → Term A C
    `_` : ∀ {A B} → T A ⇒ T B → Term A B

  ↑↑ : ∀ {A B} -> A C.⇒ B -> Term (↑ A) (↑ B)
  ↑↑ {A} {B} f = `_` {↑ A} {↑ B} f

  _#⧻_ : ∀ {A B C D} → (Term A B) → (Term C D) → (Term (A ⊎ C) (B ⊎ D))
  f #⧻ g = #[ #i₁ #∘ f , #i₂ #∘ g ]

  #left : ∀ {A B C} → (Term A B) → (Term (A ⊎ C) (B ⊎ C))
  #left f = f #⧻ #id

  #right : ∀ {A C D} → (Term C D) → (Term (A ⊎ C) (A ⊎ D))
  #right g = #id #⧻ g

  eval : ∀ {A B} → Term A B → T A ⇒ T B
  eval #id = C.id
  eval #i₁ = i₁
  eval #i₂ = i₂
  eval #[ t , t₁ ] = [ (eval t) , (eval t₁) ]
  eval (t #∘ t₁)   = eval t C.∘ eval t₁
  eval ` x `       = x

  module Internal where

    _⇛_ : Ty → Ty → Set _
    _⇛_ (↑ x) t = x ⇒ T t
    _⇛_ (s ⊎ s₁) t = (s ⇛ t) × (s₁ ⇛ t)

    ⇛→⇒ : ∀ {A B} → A ⇛ B → T A ⇒ T B
    ⇛→⇒ {↑ O} f = f
    ⇛→⇒ {A ⊎ A₁} (f , g) = [ ⇛→⇒ {A} f , ⇛→⇒ {A₁} g ]

    _<∘_ : ∀ {A B C} → T B ⇒ T C → A ⇛ B → A ⇛ C
    _<∘_ {↑ x} f g = f C.∘ g
    _<∘_ {A ⊎ A₁} f (g₁ , g₂) = (_<∘_ {A} f g₁) , (_<∘_  {A₁} f  g₂)

    .<∘-comm : ∀ {A B C} (f : T B ⇒ T C) (g : A ⇛ B) → f C.∘ (⇛→⇒ {A} g) C.≡ ⇛→⇒ {A} (_<∘_ {A} {B} {C} f g)
    <∘-comm {↑ x} f g = refl
    <∘-comm {A ⊎ A₁} f g = trans ∘[] ([]-cong₂ (<∘-comm f (proj₁ g)) (<∘-comm f (proj₂ g)))

    mutual
     j₁ : ∀ {A B} → A ⇛ (A ⊎ B)
     j₁ {↑ x}    = i₁
     j₁ {A ⊎ A₁} = _<∘_ {A} i₁ (j₁ {A} {A₁}) , _<∘_ {A₁} i₁ (j₂ {A₁} {A})
     j₂ : ∀ {B A} → B ⇛ (A ⊎ B)
     j₂ {↑ x}    = i₂
     j₂ {B ⊎ B₁} = _<∘_ {B} i₂ (j₁ {B} {B₁}) , _<∘_ {B₁} i₂ (j₂ {B₁} {B})

     id : ∀ {A} → A ⇛ A
     id {↑ x}    = C.id
     id {A ⊎ A₁} = j₁ {A} {A₁} , j₂ {A₁} {A}

    ⇒→⇛ : ∀ {A B} → T A ⇒ T B → A ⇛ B
    ⇒→⇛ {↑ x} f = f
    ⇒→⇛ {A ⊎ A₁} f = _<∘_ {A} f (j₁ {A} {A₁}) , _<∘_ {A₁} f (j₂ {A₁} {A})

    mutual
     .j₁≡i₁ : ∀ {A B} → ⇛→⇒ {A} (j₁ {A} {B}) C.≡ i₁
     j₁≡i₁ {↑ x} = refl
     j₁≡i₁ {A ⊎ A₁} = universal (trans (C.∘-resp-≡ʳ (sym (j₁≡i₁ {A} {A₁}))) (<∘-comm {A} i₁ (j₁ {A} {A₁})))
                                (trans (C.∘-resp-≡ʳ (sym (j₂≡i₂ {A₁} {A}))) (<∘-comm {A₁} i₁ (j₂ {A₁} {A})))

     .j₂≡i₂ : ∀ {B A} → ⇛→⇒ {B} (j₂ {B} {A}) C.≡ i₂
     j₂≡i₂ {↑ x} = refl
     j₂≡i₂ {A ⊎ A₁} = universal (trans (C.∘-resp-≡ʳ (sym (j₁≡i₁ {A} {A₁}))) (<∘-comm {A} i₂ (j₁ {A} {A₁})))
                                (trans (C.∘-resp-≡ʳ (sym (j₂≡i₂ {A₁} {A})))
                                   (<∘-comm {A₁} i₂ (j₂ {A₁} {A})))

    .iso₁-⇒⇛ : ∀ {A B} → (f : T A ⇒ T B) → ⇛→⇒ {A} {B} (⇒→⇛ {A} {B} f) ≡ f
    iso₁-⇒⇛ {↑ x} f = refl
    iso₁-⇒⇛ {A ⊎ A₁} {B} f = universal (trans (C.∘-resp-≡ʳ (sym j₁≡i₁)) (<∘-comm {A} {A ⊎ A₁} {B} f (j₁ {A})))
                                       (trans (C.∘-resp-≡ʳ (sym j₂≡i₂)) (<∘-comm {A₁} {A ⊎ A₁} {B} f (j₂ {A₁})))

    .id≡id : ∀ A → ⇛→⇒ {A} (id {A}) ≡ C.id
    id≡id (↑ x) = refl
    id≡id (A ⊎ A₁) = universal (trans C.identityˡ (sym j₁≡i₁)) (trans C.identityˡ (sym j₂≡i₂))

    _∘_ : ∀ {A B C} → B ⇛ C → A ⇛ B → A ⇛ C
    _∘_ {↑ x} {B} f g = ⇛→⇒ {B} f C.∘ g
    _∘_ {A ⊎ A₁} f (g₁ , g₂) = (_∘_ {A} f g₁) , (_∘_ {A₁} f g₂)

    .∘-comm : ∀ {A B C} (f : B ⇛ C) (g : A ⇛ B) → (⇛→⇒ {B} f) C.∘ (⇛→⇒ {A} g) C.≡ ⇛→⇒ {A} (_∘_ {A} {B} {C} f g)
    ∘-comm {↑ x} f g = refl
    ∘-comm {A ⊎ A₁} f g = trans ∘[] ([]-cong₂ (∘-comm f (proj₁ g)) (∘-comm f (proj₂ g)))

    -- An η-expanded version of C
    Cη : Category _ _ _
    Cη = record
      { Obj = Ty
      ; _⇒_ = _⇛_
      ; _≡_ = λ {A} f g → ⇛→⇒ {A} f ≡ ⇛→⇒ {A} g
      ; _∘_ = λ {A} {B} {C} → _∘_ {A} {B} {C}
      ; id = λ {X} → id {X}
      ; assoc = λ {A} {B} {C} {D} {f} {g} {h} →
                     trans (sym (∘-comm {A} {B} {D} (h ∘ g) f))
                    (trans (C.∘-resp-≡ˡ (sym (∘-comm {B} {C} {D} h g)))
                    (trans C.assoc
                    (trans (C.∘-resp-≡ʳ (∘-comm {A} {B} {C} g f))
                           (∘-comm {A} {C} {D} h (g ∘ f)))))
      ; identityˡ = λ {A} {B} {f} → trans (sym (∘-comm {A} {B} {B} id f))
                                   (trans (C.∘-resp-≡ˡ (id≡id B)) C.identityˡ)
      ; identityʳ = λ {A} {B} {f} →
                      trans (sym (∘-comm {A} {A} {B} f id))
                     (trans (C.∘-resp-≡ʳ (id≡id A)) C.identityʳ)
      ; equiv = record
        { refl = refl
        ; sym = sym
        ; trans = trans
        }
      ; ∘-resp-≡ = λ {A} {B} {C} {f} {h} {g} {i} f≡h g≡i →
            trans (sym (∘-comm {A} {B} {C} f g)) (trans (C.∘-resp-≡ f≡h g≡i) (∘-comm {A} {B} {C} h i))
      }

    module Cη = Category Cη

    -- We need the opposite category for Yon because i₁ and i₂ simplify when precomposed.
    -- Using Eda seems to undo the simplifications instead.
    open Yon-Eda (Category.op Cη)

    Yon-i₁ : ∀ {A B} → Yon (A ⊎ B) A
    Yon-i₁ {A} {B} = record
                     { arr = j₁ {A} {B}
                     ; fun = proj₁
                     ; ok = λ {W} f → trans (trans (sym commute₁) (C.∘-resp-≡ʳ (sym (j₁≡i₁ {A} {B})))) (∘-comm {A} {A ⊎ B} {W} f (j₁ {A} {B}))
                     }

    Yon-i₂ : ∀ {A B} → Yon (A ⊎ B) B
    Yon-i₂ {A} {B} = record
                     { arr = j₂ {B} {A}
                     ; fun = proj₂
                     ; ok = λ {W} f →
                                trans (trans (sym commute₂) (C.∘-resp-≡ʳ (sym (j₂≡i₂ {B} {A}))))
                                (∘-comm {B} {A ⊎ B} {W} f (j₂ {B} {A}))
                     }

    Yon-[_,_] : ∀ {A B C} → Yon C A → Yon C B → Yon C (A ⊎ B)
    Yon-[_,_] f g = record
                    { arr = (Yon.arr f) , (Yon.arr g)
                    ; fun = λ f₁ → (Yon.fun f f₁) , (Yon.fun g f₁)
                    ; ok = λ f₁ → []-cong₂ (Yon.ok f f₁) (Yon.ok g f₁)
                    }

    eeval : ∀ {A B} → Term A B → Yon B A
    eeval #id = Yon-id
    eeval #i₁ = Yon-i₁
    eeval #i₂ = Yon-i₂
    eeval #[ t , t₁ ] = Yon-[ (eeval t) , (eeval t₁) ]
    eeval (t #∘ t₁) = Yon-compose (eeval t₁) (eeval t)
    eeval {A} ` f ` = Yon-inject (⇒→⇛ {A} f)

    yeeval : ∀ {A B} → Term A B → T A ⇒ T B
    yeeval {A} {B} t = ⇛→⇒ {A} (Yon.arr (eeval t))

    .yeeval≡eval : ∀ {A B} → (f : Term A B) → yeeval f ≡ eval f
    yeeval≡eval     #id = id≡id _
    yeeval≡eval {A} #i₁ = j₁≡i₁ {A}
    yeeval≡eval {A} #i₂ = j₂≡i₂ {A}
    yeeval≡eval   ` x ` = iso₁-⇒⇛ x
    yeeval≡eval #[ f , f₁ ] = []-cong₂ (yeeval≡eval f) (yeeval≡eval f₁)
    yeeval≡eval (f #∘ f₁) = trans
                          (trans (Yon.ok (eeval f₁) (Yon.arr (eeval f)))
                                 (sym (∘-comm (Yon.arr (eeval f)) (Yon.arr (eeval f₁)))))
                          (C.∘-resp-≡ (yeeval≡eval f) (yeeval≡eval f₁))

    +reasoning : NormReasoning C o (ℓ ⊔ o)
    +reasoning = record
                 { U = Ty
                 ; T = T
                 ; _#⇒_ = Term
                 ; eval = eval
                 ; norm = yeeval
                 ; norm≡eval = yeeval≡eval }

  open NormReasoning Internal.+reasoning public hiding (T; eval)


text:
-- The bug appeared since I forgot to keep the constraint when trying to unify
-- a blocked term (I just didn't instantiate).
module LostConstraint where

  infixr 10 _==>_ _=>_

  data Setoid : Set1 where
    setoid : Set -> Setoid

  El : Setoid -> Set
  El (setoid A) = A

  eq : (A : Setoid) -> El A -> El A -> Set
  eq (setoid A) = e
    where
      postulate e : (x, y : A) -> Set

  data _=>_ (A,B : Setoid) : Set where
    lam : (f : El A -> El B)
       -> ((x : El A) -> eq A x x
                      -> eq B (f x) (f x)
          )
       -> A => B

  app : {A,B : Setoid} -> (A => B) -> El A -> El B
  app (lam f _) = f

  postulate EqFun : {A,B : Setoid}(f, g : A => B) -> Set

  lam2 : {A,B,C : Setoid} ->
         (f : El A -> El B -> El C) ->
         (x : El A) -> B => C
  lam2 {A}{B}{C} f x = lam (f x) (lem _)
    where
      postulate
        lem : (x : El A)(y : El B) -> eq B y y -> eq C (f x y) (f x y)


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

open import Data.Product

open import Categories.Category
open import Categories.Functor
open import Categories.Product
open import Categories.FunctorCategory
open import Categories.Functor.Constant

import Categories.Power as Power

Δ : ∀ {o ℓ e} → (C : Category o ℓ e) → Functor C (Product C C)
Δ C = record
  { F₀ = λ x → x , x
  ; F₁ = λ f → f , f
  ; identity = refl , refl
  ; homomorphism = refl , refl
  ; F-resp-≡ = λ x → x , x
  }
  where
  open Category C
  open Equiv

Δ′ : ∀ {o ℓ e} → (I : Set) → (C : Category o ℓ e) → Functor C (Power.Exp C I)
Δ′ I C = record
  { F₀ = λ x _ → x
  ; F₁ = λ f _ → f
  ; identity = λ _ → refl
  ; homomorphism = λ _ → refl
  ; F-resp-≡ = λ x _ → x
  }
  where
  open Power C
  open Category C
  open Equiv

ΔF : ∀ {o ℓ e o₁ ℓ₁ e₁} {C : Category o ℓ e} (I : Category o₁ ℓ₁ e₁) → Functor C (Functors I C)
ΔF {C = C} I = record
  { F₀ = λ c → Constant c
  ; F₁ = λ f → record { η = λ X → f; commute = λ g → trans C.identityʳ (sym C.identityˡ) }
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≡ = λ x → x
  }
 where
   module C = Category C
   open C.Equiv
   module I = Category I


text:
record R : Set₁ where
  field
    A : Set

  B : Set
  B = A

  field
    C : Set

  D : Set
  D = A → B → C


text:
module Extended.FunRetRec where

open import Function
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.String
open import Data.Product
open import Data.Bool renaming (not to bnot) hiding (if_then_else_)
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Data.List hiding (and; or)
open import Data.List.Properties using (∷-injective)
open import Data.Empty
open import Data.Unit
import Level as L

open import Utils.Decidable
open import Utils.Monoid
open import Utils.NatOrdLemmas

{-
This module contains an extension of the While language and assorted semantics.
It incorporates some  of the suggested extra features in the book.

The extra features in short:

  - Function calls and recursive local function declarations
  - Local variable declarations
  - String-based bindings with name shadowing
  - Return statements with the usual jump in control flow
-}

-- Data definitions
--------------------------------------------------

data Ty : Set where
  bool nat : Ty

⟦_⟧ᵗ : Ty → Set
⟦ nat  ⟧ᵗ = ℕ
⟦ bool ⟧ᵗ = Bool

data Exp : Ty → Set where
  lit         : ℕ → Exp nat
  add mul sub : Exp nat → Exp nat → Exp nat
  var         : String → Exp nat

  {-
  Function calls. Note that we have calls as a proper *expression* that
  evaluate to a value, if they terminate. This also implies that the evaluation
  of expressions has a partial semantics just like statements.

  We apply a function to a list of arguments. The number of args must be correct.
  -}
  _$:_        : String → List (Exp nat) → Exp nat

  tt ff       : Exp bool
  eq lt lte   : Exp nat → Exp nat → Exp bool
  and         : Exp bool → Exp bool → Exp bool
  not         : Exp bool → Exp bool
  or          : Exp bool → Exp bool → Exp bool

infixr 4 _,_
infixr 5 _:=_
data St : Set where

  {- Function declarations. We specify the arguments as a list of bindings.
  They are recursive. -}
  fun           : String → List String → St → St → St

  {- variable declarations -}
  decl          : String → Exp nat → St → St

  _:=_          : String → Exp nat → St
  skip          : St
  _,_           : St → St → St
  if_then_else_ : Exp bool → St → St → St
  while_do_     : Exp bool → St → St
  ret           : Exp nat → St

{- The environment contains numbers and functions -}
data Entry : Set where
  nat : ℕ → Entry
  fun : List String → St → Entry

{- The environment is now keyed by strings (rather than de Bruijn indices) -}
Env : Set
Env = List (String × Entry)

_,ₙ_ : String → ℕ → (String × Entry)
v ,ₙ n = v , nat n
infixr 5 _,ₙ_

{-
A note on the return statement:

The book recommends two way for dealing with exceptions and jumps.

One way is to use small-step semantics. The other way is to introduce new program
states in big-step semantics. With more complicated derivation rules and many
types of non-local effects (and of course non-determinism), small-step semantics
seems to be more manageable.

But here we have just the return statement, so big-step semantics seems fine.
-}

data State : Set where
  ok  : Env → State
  ret : ℕ → State

ret-inj : ∀ {a b} → (State ∋ ret a) ≡ ret b → a ≡ b
ret-inj refl = refl

ok-inj : ∀ {s s'} → ok s ≡ ok s' → s ≡ s'
ok-inj refl = refl

-- Well-scopedness
--------------------------------------------------

{-
Scoping rules are nontrivial, but we don't want to clutter our derivations
with explicit proofs for them.

A standard Agda solution for this is to use so-called irrelevant proofs. Such
types have at most a single value up to definitional equality, therefore they
cannot influence actual computation. Agda is willing to automatically fill in
the value for some of these types once it becomes apparent that the value exists.

The simplest example of a irrelevant type is the unit type.

  record ⊤ : Set where constructor tt.

Agda has eta-extensionality for records, so Agda thinks that any value of
type ⊤ is definitionally equal to "tt".

The well-scopedness predicates below all compute to ⊤ or ⊥ (the unprovable type),
and both are irrelevant, so we get all the scoping proofs nicely inferred
and hidden.

We also augment our inference system with judicious use of instance arguments.
Agda tries to search for suitable values for these arguments from the current scope.
-}

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

{-
A note on static semantics:

Arguably, well-scopedness should belong to static semantics. After all,
it can be checked without running the program, and in real compilers
scope checking also tends to be done statically.

Here, we don't *have* static semantics at all. The static semantic rules are baked into
the dynamic semantic rules. Adding proper static semantics would be one of the many potential
extensions and improvements to this library.

Ideally, we would have a completely raw AST, and an AST for code that is correct
with respect to static semantics (so it's annotated with proofs of static correctness).

We would also have a type checker function that would decide if a raw AST can be converted
to the correct AST. It would also nice to have a type erasure function that goes in the opposite
direction (erases proofs and returns a raw AST), and we could establish correctness of type
checking with respect to erasure, for example by proving that checking is the left inverse
of erasure.

It may be also the case, although I haven't tested it, that type checking would be faster
with a separate checked AST.
-}

-- variable is in scope
InScopeVar : String → Env → Set
InScopeVar v [] = ⊥
InScopeVar v ((_ , fun _ _) ∷ s) = InScopeVar v s
InScopeVar v ((v' , nat n)  ∷ s) with v ≡⁇ v'
... | yes _ = ⊤
... | no  _ = InScopeVar v s

-- function is in scope
InScopeFun : String → Env → Set
InScopeFun v [] = ⊥
InScopeFun v ((_ , nat _) ∷ s) = InScopeFun v s
InScopeFun v ((v' , fun _ _) ∷ s) with v ≡⁇ v'
... | yes _ = ⊤
... | no  _ = InScopeFun v s

lookupVar : ∀ v s ⦃ _ : InScopeVar v s ⦄ → ℕ
lookupVar v [] ⦃ ⦄
lookupVar v ((_ , fun _ _) ∷ s) = lookupVar v s
lookupVar v ((v' , nat n) ∷ s) with v ≡⁇ v'
... | yes _ = n
... | no  _ = lookupVar v s

lookupFun : ∀ f s ⦃ _ : InScopeFun f s ⦄ → List String × St
lookupFun v [] ⦃ ⦄
lookupFun v ((_ , nat _) ∷ s) = lookupFun v s
lookupFun v ((v' , fun args body) ∷ s) with v ≡⁇ v'
... | yes _ = args , body
... | no  _ = lookupFun v s

-- perform a substitution on the environment at a name that is in scope
_[_]≔_ : ∀ s v ⦃ _ : InScopeVar v s ⦄ → ℕ → Env
_[_]≔_ [] _ ⦃ ⦄ _
_[_]≔_ ((v' , fun args body) ∷ s) v n = (v' , fun args body) ∷ (s [ v ]≔ n)
((v' , nat n) ∷ Γ) [ v ]≔ n' with v ≡⁇ v'
... | yes p = (v' , nat n') ∷ Γ
... | no ¬p = (v' , nat n ) ∷ Γ [ v ]≔ n'

-- Match the length of two lists
ArgLenMatch : List String → List ℕ → Set
ArgLenMatch []          []         = ⊤
ArgLenMatch []          (_ ∷ _)    = ⊥
ArgLenMatch (_ ∷ names) []         = ⊥
ArgLenMatch (_ ∷ names) (_ ∷ vals) = ArgLenMatch names vals

-- Create a new environment with the function arguments pushed to the front
callWith : ∀ args vals ⦃ _ : ArgLenMatch args vals ⦄ → Env
callWith []          []         = []
callWith []          (_ ∷ _) ⦃ ⦄
callWith (_ ∷ _)     []      ⦃ ⦄
callWith (n ∷ names) (v ∷ vals) = (n , nat v) ∷ callWith names vals

-- Semantics
--------------------------------------------------

mutual
  -- Evaluation of argument lists
  infixr 5 _∷_
  data _⟨_⟩ᵃ⟱_ (s : Env) : List (Exp nat) → List ℕ → Set where

    []  :
      ----------------
       s ⟨ [] ⟩ᵃ⟱ []

    _∷_ :
              ∀ {a args v vals} →
        s ⟨ a ⟩ᵉ⟱ v  →  s ⟨ args ⟩ᵃ⟱ vals
      → ---------------------------------
          s ⟨ a ∷ args ⟩ᵃ⟱ (v ∷ vals)

  -- Shorthand for the evaluation of binary expressions
  BinExp : ∀ {s t r} → (Exp t → Exp t → Exp r) → (⟦ t ⟧ᵗ → ⟦ t ⟧ᵗ → ⟦ r ⟧ᵗ) → Set
  BinExp {s} cons op =
         ∀ {a b va vb} →
    s ⟨ a ⟩ᵉ⟱ va → s ⟨ b ⟩ᵉ⟱ vb
    -----------------------------
    → s ⟨ cons a b ⟩ᵉ⟱ (op va vb)

  -- Evaluation of expressions
  data _⟨_⟩ᵉ⟱_ (s : Env) : ∀ {t} → Exp t → ⟦ t ⟧ᵗ → Set where

    add : BinExp add _+_
    eq  : BinExp eq (λ a b → ⌊ a ≡⁇ b ⌋)
    lt  : BinExp lt (λ a b → ⌊ suc a ≤⁇ b ⌋)
    lte : BinExp lte (λ a b → ⌊ a ≤⁇ b ⌋)
    and : BinExp and _∧_
    or  : BinExp or  _∨_
    mul : BinExp mul _*_
    sub : BinExp sub _∸_
    tt  : s ⟨ tt ⟩ᵉ⟱ true
    ff  : s ⟨ ff ⟩ᵉ⟱ false
    lit : ∀ {n} → s ⟨ lit n ⟩ᵉ⟱ n
    not : ∀ {e b} → s ⟨ e ⟩ᵉ⟱ b → s ⟨ not e ⟩ᵉ⟱ bnot b

    var :
              ∀ {v in-scope}
      → ----------------------------
        s ⟨ var v ⟩ᵉ⟱ lookupVar v s

    {- Evaluation of function calls -}
    _$:_ :
        {retVal       : ℕ}
        {argVals      : List ℕ}
        {f            : String}          -- if we have a function
        {args         : List (Exp nat)}  -- and a list of arguments
        ⦃ in-scope-f  : InScopeFun f s ⦄ -- and the function is in scope

        → let func     = lookupFun f s
              argNames = proj₁ func
              body     = proj₂ func in

           s ⟨ args ⟩ᵃ⟱ argVals -- we can evaluate the arguments
        →  ⦃ arg-len-match : ArgLenMatch argNames argVals ⦄ -- and the number of arguments is correct

       -- note the recursive occurence in the call environement ⇓
        → let callEnv = callWith argNames argVals <> [ (f , fun argNames body) ] in

         ⟨ body , ok callEnv ⟩⟱ ret retVal
      → -----------------------------------   -- then a function call evaluates to the return value
           s ⟨ f $: args ⟩ᵉ⟱ retVal           -- of the function body evaluated in the call environment

  -- Evaluation of statements
  data ⟨_,_⟩⟱_ : St → State → State → Set where

    fun :
                           ∀ {x s s' S args body} →
        ⟨ S , ok ((x , fun args body) ∷ s) ⟩⟱ ok ((x , fun args body) ∷ s')
      → -------------------------------------------------------------------
                      ⟨ fun x args body S , ok s ⟩⟱ ok s'

    {-- This rule propagates ("rethrows") the return statement's effect if it happens inside the
        scope of the function declaration --}
    fun-ret :
                 ∀ {x s r S args body} →
        ⟨ S , ok ((x , fun args body) ∷ s) ⟩⟱ ret r
      → --------------------------------------------
           ⟨ fun x args body S , ok s ⟩⟱ ret r

    {- variable declarations -}
    decl :
                  ∀ {s s' S x e eVal e'} →
                     s ⟨ e ⟩ᵉ⟱ eVal →
       ⟨ S , ok ((x , nat eVal) ∷ s) ⟩⟱ (ok ((x , e') ∷ s'))
      → ----------------------------------------------------
                  ⟨ decl x e S , ok s ⟩⟱ ok s'

    {- variable declarations propagating the return statement -}
    decl-ret :
               ∀ {r s S x e eVal} →
                 s ⟨ e ⟩ᵉ⟱ eVal →
        ⟨ S , ok ((x , nat eVal) ∷ s) ⟩⟱ ret r
      → ---------------------------------------
           ⟨ decl x e S , ok s ⟩⟱ ret r

    ret :
              ∀ {e eVal s}
            → s ⟨ e ⟩ᵉ⟱ eVal
      → ---------------------------
        ⟨ ret e , ok s ⟩⟱ ret eVal

    ass :
              ∀ {s e eVal x in-scope} →
                  s ⟨ e ⟩ᵉ⟱ eVal
      → --------------------------------------
        ⟨ x := e , ok s ⟩⟱ ok (s [ x ]≔ eVal)

    skip :
             ∀ {s}
      → -----------------
        ⟨ skip , s ⟩⟱ s

    _,_ :
                ∀ {s₁ s₂ s₃ S₁ S₂} →
        ⟨ S₁ , s₁ ⟩⟱ ok s₂  →  ⟨ S₂ , ok s₂ ⟩⟱ s₃
      → --------------------------------------
               ⟨ (S₁ , S₂ ) , s₁ ⟩⟱ s₃

    {-- If we return in the left statement of a composite statement,
        then we ignore the right statement and just return -}
    _ret,_ :
                 ∀ {x s₁ s₂ S₁ S₂} →
        ⟨ S₁ , s₁ ⟩⟱ ret x  →  ⟨ S₂ , ret x ⟩⟱ s₂
      → ---------------------------------------
            ⟨ (S₁ , S₂ ) , s₁ ⟩⟱ ret x

    if-true :
                ∀ {s s' S₁ S₂ b} →
        s ⟨ b ⟩ᵉ⟱ true  →  ⟨ S₁ , ok s ⟩⟱ s'
      → ------------------------------------
        ⟨ if b then S₁ else S₂ , ok s ⟩⟱ s'

    if-false :
                 ∀ {s s' S₁ S₂ b} →
        s ⟨ b ⟩ᵉ⟱ false  →  ⟨ S₂ , ok s ⟩⟱ s'
      → -------------------------------------
        ⟨ if b then S₁ else S₂ , ok s ⟩⟱ s'

    while-true :
                           ∀ {s s' s'' S b} →
       s ⟨ b ⟩ᵉ⟱ true  →  ⟨ S , ok s ⟩⟱ s'  →  ⟨ while b do S , s' ⟩⟱ s''
      → ------------------------------------------------------------------
                       ⟨ while b do S , ok s ⟩⟱ s''

    while-false :
                 ∀ {s S b} →
              s ⟨ b ⟩ᵉ⟱ false
      → ------------------------------
        ⟨ while b do S , ok s ⟩⟱ ok s

substExp : ∀ {t s}{e : Exp t}{v v'} → v ≡ v' → s ⟨ e ⟩ᵉ⟱ v → s ⟨ e ⟩ᵉ⟱ v'
substExp refl p2 = p2

-- State transition is deterministic
--------------------------------------------------

deterministic : ∀ {S s s' s''} → ⟨ S , s ⟩⟱ s' → ⟨ S , s ⟩⟱ s'' → s' ≡ s''
deterministic = st where
  mutual
    args : ∀ {s as vs vs'} → s ⟨ as ⟩ᵃ⟱ vs → s ⟨ as ⟩ᵃ⟱ vs' → vs ≡ vs'
    args [] [] = refl
    args (x ∷ p1) (x₁ ∷ p2) rewrite exp x x₁ | args p1 p2 = refl

    exp : ∀ {t s}{e : Exp t}{v v'} → s ⟨ e ⟩ᵉ⟱ v → s ⟨ e ⟩ᵉ⟱ v' → v ≡ v'
    exp (add p1 p2) (add p3 p4) rewrite exp p1 p3 | exp p2 p4 = refl
    exp (sub p1 p2) (sub p3 p4) rewrite exp p1 p3 | exp p2 p4 = refl
    exp (eq p1 p2)  (eq p3 p4)  rewrite exp p1 p3 | exp p2 p4 = refl
    exp (lt p1 p2)  (lt p3 p4)  rewrite exp p1 p3 | exp p2 p4 = refl
    exp (lte p1 p2) (lte p3 p4) rewrite exp p1 p3 | exp p2 p4 = refl
    exp (and p1 p2) (and p3 p4) rewrite exp p1 p3 | exp p2 p4 = refl
    exp (or p1 p2)  (or p3 p4)  rewrite exp p1 p3 | exp p2 p4 = refl
    exp (mul p1 p2) (mul p3 p4) rewrite exp p1 p3 | exp p2 p4 = refl
    exp tt tt = refl
    exp ff ff = refl
    exp lit lit = refl
    exp (not p1) (not p2) rewrite exp p1 p2 = refl
    exp var var = refl
    exp (_$:_ ae be) (_$:_ ae' be') rewrite args ae ae' = ret-inj (st be be')

    st : ∀ {S s s' s''} → ⟨ S , s ⟩⟱ s' → ⟨ S , s ⟩⟱ s'' → s' ≡ s''
    st (fun p1) (fun p2) = cong ok $ proj₂ $ ∷-injective $ ok-inj $ st p1 p2
    st (fun p1) (fun-ret p2) with st p1 p2
    ... | ()
    st (fun-ret p1) (fun p2) with st p1 p2
    ... | ()
    st (fun-ret p1) (fun-ret p2) = st p1 p2
    st (decl x₁ p1) (decl x₂ p2) rewrite
      exp x₁ x₂ = cong ok $ proj₂ $ ∷-injective $ ok-inj $ st p1 p2
    st (decl x₁ p1) (decl-ret x₂ p2) rewrite exp x₁ x₂ with st p1 p2
    ... | ()
    st (decl-ret x₁ p1) (decl x₂ p2) rewrite exp x₁ x₂ with st p1 p2
    ... | ()
    st (decl-ret x₁ p1) (decl-ret x₂ p2) rewrite exp x₁ x₂ = st p1 p2
    st (ret x) (ret x₁) rewrite exp x x₁ = refl
    st (ass x₁) (ass x₂) rewrite exp x₁ x₂ = refl
    st skip skip = refl
    st (p1 , p2) (p3 , p4) rewrite st p1 p3 = st p2 p4
    st (p1 , p2) (p3 ret, p4) with st p1 p3
    ... | ()
    st (p1 ret, p2) (p3 , p4) with st p1 p3
    ... | ()
    st (p1 ret, p2) (p3 ret, p4) = st p1 p3
    st (if-true x p1) (if-true x₁ p2) rewrite st p1 p2 = refl
    st (if-true x p1) (if-false x₁ p2) with exp x₁ x
    ... | ()
    st (if-false x p1) (if-true x₁ p2) with exp x x₁
    ... | ()
    st (if-false x p1) (if-false x₁ p2) rewrite st p1 p2 = refl
    st (while-true x p1 p2) (while-true x₁ p3 p4) rewrite st p1 p3 | st p2 p4 = refl
    st (while-true x p1 p2) (while-false x₁) with exp x x₁
    ... | ()
    st (while-false x) (while-true x₁ p2 p3) with exp x x₁
    ... | ()
    st (while-false x) (while-false x₁) = refl

-- Divergence
--------------------------------------------------

_divergesOn_ : St → State → Set
prog divergesOn s = ∀ {s'} → ¬ ⟨ prog , s ⟩⟱ s'

Divergent : St → Set
Divergent prog = ∀ {s} → prog divergesOn s

private
  inf-loop : Divergent (while tt do skip)
  inf-loop (while-true tt p p₁) = inf-loop p₁
  inf-loop (while-false ())

-- Semantic equivalence
--------------------------------------------------

_⇔_ : ∀ {a b} → Set a → Set b → Set (a L.⊔ b)
A ⇔ B = (A → B) × (B → A)

SemanticEq : St → St → Set
SemanticEq pa pb = ∀ {s s'} → ⟨ pa , s ⟩⟱ s' ⇔ ⟨ pb , s ⟩⟱ s'

Semantic⇒ : St → St → Set
Semantic⇒ pa pb = ∀ {s s'} → ⟨ pa , s ⟩⟱ s' → ⟨ pb , s ⟩⟱ s'

-- -- Correctness of factorial programs
-- --------------------------------------------------

private

  --- Semantics in meta-langauge
  ⟦fac⟧ : ℕ → ℕ
  ⟦fac⟧ zero    = 1
  ⟦fac⟧ (suc n) = suc n * ⟦fac⟧ n

  -- 1.  Correctness of recursive definition
  fac-rec-body : St
  fac-rec-body =
      if lte (var "n") (lit 0) then
         (ret (lit 1))
      else
         (ret (mul (var "n") ("fac" $: [ sub (var "n") (lit 1) ] )))

  fac-rec : St
  fac-rec =
    fun "fac" [ "n" ] fac-rec-body
    (ret ("fac" $: [ var "n" ]))

  fac-rec-body-ok :
    ∀ n
    → ⟨ fac-rec-body ,
      ok (("n" ,ₙ n) ∷ ("fac" , fun [ "n" ] fac-rec-body) ∷ []) ⟩⟱
      ret (⟦fac⟧ n)
  fac-rec-body-ok zero = if-true (lte var lit) (ret lit)
  fac-rec-body-ok (suc n) =
    if-false (lte var lit)
      (ret (mul var ((sub var lit ∷ []) $: (fac-rec-body-ok n))))

  fac-rec-ok :
    ∀ n → ⟨ fac-rec , ok [ ("n" ,ₙ n) ] ⟩⟱ ret (⟦fac⟧ n)
  fac-rec-ok n = fun-ret (ret ((var ∷ []) $: (fac-rec-body-ok n)))

  -- 2. Correctness of procedural definition
  fac-loop : St
  fac-loop =
    while lt (var "i") (var "n") do (
      "i"   := add (lit 1) (var "i") ,
      "acc" := mul (var "i") (var "acc")
    )

  fac-proc : St
  fac-proc =
    fun "fac" ( "n" ∷ []) (
      decl "i" (lit 0) (
      decl "acc" (lit 1) (
      fac-loop ,
      ret (var "acc") )))
    (ret ("fac" $: [ var "n" ]))

  fac-loop-ok :
    ∀ {s} d i
    → ⟨ fac-loop ,
        ok (("acc",ₙ ⟦fac⟧ i)       ∷ ("i",ₙ i    ) ∷ ("n",ₙ d + i) ∷ s) ⟩⟱
        ok (("acc",ₙ ⟦fac⟧ (d + i)) ∷ ("i",ₙ d + i) ∷ ("n",ₙ d + i) ∷ s)

  fac-loop-ok zero i = while-false (substExp (¬A→≡false (a≮a i)) (lt var var))
  fac-loop-ok (suc d) i with fac-loop-ok d (suc i)
  ... | next rewrite +-suc d i =
    while-true (substExp (A→≡true (a<sb+a i d)) (lt var var))
       ( ass (add lit var) ,
         ass (mul var var))
       next

  fac-proc-ok :
    ∀ n → ⟨ fac-proc , ok (("n",ₙ n) ∷ []) ⟩⟱ ret (⟦fac⟧ n)
  fac-proc-ok n with fac-loop-ok n 0
  ... | loop-ok rewrite +-comm n 0 =
    fun-ret (ret ((var ∷ []) $:
      decl-ret lit (
      decl-ret lit
      (loop-ok ,
      ret var))))

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
-- We define ZigZag-complete relations and prove that quasi equivalence relations
-- give rise to equivalences on the set quotients.
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.ZigZag.Base where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.PropositionalTruncation as Trunc
open import Cubical.Relation.Binary.Base

open isEquivRel

private
 variable
  ℓ ℓ' : Level

isZigZagComplete : {A B : Type ℓ} (R : A → B → Type ℓ') → Type (ℓ-max ℓ ℓ')
isZigZagComplete R = ∀ {a b a' b'} → R a b → R a' b → R a' b' → R a b'

ZigZagRel : (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
ZigZagRel A B ℓ' = Σ[ R ∈ (A → B → Type ℓ') ] (isZigZagComplete R)

record isQuasiEquivRel {A B : Type ℓ} (R : A → B → Type ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    zigzag : isZigZagComplete R
    fwd : (a : A) → ∃[ b ∈ B ] R a b
    bwd : (b : B) → ∃[ a ∈ A ] R a b

open isQuasiEquivRel

QuasiEquivRel : (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
QuasiEquivRel A B ℓ' =
  Σ[ R ∈ PropRel A B ℓ' ] isQuasiEquivRel (R .fst)

invQER : {A B : Type ℓ} {ℓ' : Level} → QuasiEquivRel A B ℓ' → QuasiEquivRel B A ℓ'
invQER (R , qer) .fst = invPropRel R
invQER (R , qer) .snd .zigzag aRb aRb' a'Rb' = qer .zigzag a'Rb' aRb' aRb
invQER (R , qer) .snd .fwd = qer .bwd
invQER (R , qer) .snd .bwd = qer .fwd

QER→EquivRel : {A B : Type ℓ}
  → QuasiEquivRel A B ℓ' → EquivPropRel A (ℓ-max ℓ ℓ')
QER→EquivRel (R , sim) .fst = compPropRel R (invPropRel R)
QER→EquivRel (R , sim) .snd .reflexive a = Trunc.map (λ {(b , r) → b , r , r}) (sim .fwd a)
QER→EquivRel (R , sim) .snd .symmetric _ _ = Trunc.map (λ {(b , r₀ , r₁) → b , r₁ , r₀})
QER→EquivRel (R , sim) .snd .transitive _ _ _ =
  Trunc.map2 (λ {(b , r₀ , r₁) (b' , r₀' , r₁') → b , r₀ , sim .zigzag r₁' r₀' r₁})

-- The following result is due to Carlo Angiuli
module QER→Equiv {A B : Type ℓ} (R : QuasiEquivRel A B ℓ') where

  Rᴸ = QER→EquivRel R .fst .fst
  Rᴿ = QER→EquivRel (invQER R) .fst .fst

  private
    sim = R .snd

  private
    f : (a : A) → ∃[ b ∈ B ] R .fst .fst a b → B / Rᴿ
    f a =
      Trunc.rec→Set squash/
        ([_] ∘ fst)
        (λ {(b , r) (b' , r') → eq/ b b' ∣ a , r , r' ∣})

    fPath :
      (a₀ : A) (s₀ : ∃[ b ∈ B ] R .fst .fst a₀ b)
      (a₁ : A) (s₁ : ∃[ b ∈ B ] R .fst .fst a₁ b)
      → Rᴸ a₀ a₁
      → f a₀ s₀ ≡ f a₁ s₁
    fPath a₀ =
      Trunc.elim (λ _ → isPropΠ3 λ _ _ _ → squash/ _ _)
        (λ {(b₀ , r₀) a₁ →
          Trunc.elim (λ _ → isPropΠ λ _ → squash/ _ _)
            (λ {(b₁ , r₁) →
              Trunc.elim (λ _ → squash/ _ _)
                (λ {(b' , r₀' , r₁') → eq/ b₀ b₁ ∣ a₀ , r₀ , sim .zigzag r₀' r₁' r₁ ∣})})})

    φ : A / Rᴸ → B / Rᴿ
    φ [ a ] = f a (sim .fwd a)
    φ (eq/ a₀ a₁ r i) =  fPath a₀ (sim .fwd a₀) a₁ (sim .fwd a₁) r i
    φ (squash/ _ _ p q j i) = squash/ _ _ (cong φ p) (cong φ q) j i

  relToFwd≡ : ∀ {a b} → R .fst .fst a b → φ [ a ] ≡ [ b ]
  relToFwd≡ {a} {b} r =
    Trunc.elim {P = λ s → f a s ≡ [ b ]} (λ _ → squash/ _ _)
      (λ {(b' , r') → eq/ b' b ∣ a , r' , r ∣})
      (sim .fwd a)

  fwd≡ToRel : ∀ {a b} → φ [ a ] ≡ [ b ] → R .fst .fst a b
  fwd≡ToRel {a} {b} =
    Trunc.elim {P = λ s → f a s ≡ [ b ] → R .fst .fst a b}
      (λ _ → isPropΠ λ _ → R .fst .snd _ _)
      (λ {(b' , r') p →
        Trunc.rec (R .fst .snd _ _)
          (λ {(a' , s' , s) → R .snd .zigzag r' s' s})
          (effective
            (QER→EquivRel (invQER R) .fst .snd)
            (QER→EquivRel (invQER R) .snd)
            b' b p)})
      (sim .fwd a)

  private
    g : (b : B) → ∃[ a ∈ A ] R .fst .fst a b → A / Rᴸ
    g b =
      Trunc.rec→Set squash/
        ([_] ∘ fst)
        (λ {(a , r) (a' , r') → eq/ a a' ∣ b , r , r' ∣})

    gPath :
      (b₀ : B) (s₀ : ∃[ a ∈ A ] R .fst .fst a b₀)
      (b₁ : B) (s₁ : ∃[ a ∈ A ] R .fst .fst a b₁)
      → Rᴿ b₀ b₁
      → g b₀ s₀ ≡ g b₁ s₁
    gPath b₀ =
      Trunc.elim (λ _ → isPropΠ3 λ _ _ _ → squash/ _ _)
        (λ {(a₀ , r₀) b₁ →
          Trunc.elim (λ _ → isPropΠ λ _ → squash/ _ _)
            (λ {(a₁ , r₁) →
              Trunc.elim (λ _ → squash/ _ _)
                (λ {(a' , r₀' , r₁') → eq/ a₀ a₁ ∣ b₀ , r₀ , sim .zigzag r₁ r₁' r₀' ∣})})})

    ψ : B / Rᴿ → A / Rᴸ
    ψ [ b ] = g b (sim .bwd b)
    ψ (eq/ b₀ b₁ r i) = gPath b₀ (sim .bwd b₀) b₁ (sim .bwd b₁) r i
    ψ (squash/ _ _ p q j i) = squash/ _ _ (cong ψ p) (cong ψ q) j i

  relToBwd≡ : ∀ {a b} → R .fst .fst a b → ψ [ b ] ≡ [ a ]
  relToBwd≡ {a} {b} r =
    Trunc.elim {P = λ s → g b s ≡ [ a ]} (λ _ → squash/ _ _)
      (λ {(a' , r') → eq/ a' a ∣ b , r' , r ∣})
      (sim .bwd b)

  private
    η : ∀ qb → φ (ψ qb) ≡ qb
    η =
      elimProp (λ _ → squash/ _ _)
        (λ b →
          Trunc.elim {P = λ s → φ (g b s) ≡ [ b ]} (λ _ → squash/ _ _)
            (λ {(a , r) → relToFwd≡ r})
            (sim .bwd b))

    ε : ∀ qa → ψ (φ qa) ≡ qa
    ε =
      elimProp (λ _ → squash/ _ _)
        (λ a →
          Trunc.elim {P = λ s → ψ (f a s) ≡ [ a ]} (λ _ → squash/ _ _)
            (λ {(b , r) → relToBwd≡ r})
            (sim .fwd a))

  bwd≡ToRel : ∀ {a b} → ψ [ b ] ≡ [ a ] → R .fst .fst a b
  bwd≡ToRel {a} {b} p = fwd≡ToRel (cong φ (sym p) ∙ η [ b ])

  Thm : (A / Rᴸ) ≃ (B / Rᴿ)
  Thm = isoToEquiv (iso φ ψ η ε)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Numeral.Natural.Sequence.Proofs where

import      Lvl
open import Data
open import Data.Either as Either using (_‖_)
open import Data.Either.Equiv as Either
open import Data.Either.Equiv.Id
open import Data.Either.Proofs as Either
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Equiv as Tuple
open import Data.Tuple.Equiv.Id
open import Data.Tuple.Proofs as Tuple
open import Functional
open import Function.Proofs
open import Lang.Inspect
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.DivMod.Proofs
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Sequence
open import Relator.Equals renaming (_≡_ to Id)
open import Relator.Equals.Proofs.Equiv{T = ℕ}
open import Relator.Equals.Proofs.Equivalence using () renaming ([≡]-equiv to Id-equiv ; [≡]-to-function to Id-to-function)
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
import      Structure.Function.Names as Names
open import Structure.Operator
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

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

alternate₂-args : ∀{n} → (alternate₂(n ⋅ 2) ≡ Either.Left(n)) ∧ (alternate₂(𝐒(n ⋅ 2)) ≡ Either.Right(n))
alternate₂-args {0}       = [∧]-intro [≡]-intro [≡]-intro
alternate₂-args {1}       = [∧]-intro [≡]-intro [≡]-intro
alternate₂-args {𝐒(𝐒(n))} with [∧]-intro l r ← alternate₂-args {n} rewrite l rewrite r = [∧]-intro [≡]-intro [≡]-intro

alternate₂-values : ∀{n} → (alternate₂(n) ≡ Either.Left(n ⌊/⌋ 2)) ∨ (alternate₂(n) ≡ Either.Right(n ⌊/⌋ 2))
alternate₂-values {0}       = Either.Left  [≡]-intro
alternate₂-values {1}       = Either.Right [≡]-intro
alternate₂-values {𝐒(𝐒(n))} with alternate₂-values {n}
... | Either.Left  eq rewrite eq = Either.Left  [≡]-intro
... | Either.Right eq rewrite eq = Either.Right [≡]-intro

instance
  alternate₂-inverseₗ : Inverseₗ(alternate₂)(unalternate₂)
  alternate₂-inverseₗ = intro proof where
    p : ∀{e} → (unalternate₂(Either.map 𝐒 𝐒 e) ≡ 𝐒(𝐒(unalternate₂ e)))
    p {Either.Left  _} = [≡]-intro
    p {Either.Right _} = [≡]-intro

    proof : Names.Inverses(unalternate₂)(alternate₂)
    proof {0}       = [≡]-intro
    proof {1}       = [≡]-intro
    proof {𝐒(𝐒(n))} =
      (unalternate₂ ∘ alternate₂) (𝐒(𝐒(n)))        🝖[ _≡_ ]-[]
      unalternate₂(alternate₂(𝐒(𝐒(n))))            🝖[ _≡_ ]-[]
      unalternate₂(Either.map 𝐒 𝐒 (alternate₂ n)) 🝖[ _≡_ ]-[ p{alternate₂ n} ]
      𝐒(𝐒(unalternate₂(alternate₂ n)))             🝖[ _≡_ ]-[ congruence₁(𝐒) (congruence₁(𝐒) (proof {n})) ]
      𝐒(𝐒(n))                                      🝖-end

instance
  alternate₂-inverseᵣ : Inverseᵣ(alternate₂)(unalternate₂)
  alternate₂-inverseᵣ = intro proof where
    proof : Names.Inverses(alternate₂)(unalternate₂)
    proof {Either.Left  n} = [∧]-elimₗ alternate₂-args
    proof {Either.Right n} = [∧]-elimᵣ alternate₂-args

instance
  alternate₂-inverse : Inverse(alternate₂)(unalternate₂)
  alternate₂-inverse = [∧]-intro alternate₂-inverseₗ alternate₂-inverseᵣ

instance
  alternate₂-bijective : Bijective(alternate₂)
  alternate₂-bijective = invertible-to-bijective ⦃ inver = [∃]-intro unalternate₂ ⦃ [∧]-intro Id-to-function alternate₂-inverse ⦄ ⦄

pairIndexing-def3 : ∀{a b} → (pairIndexing a (𝐒 b) ≡ 𝐒(pairIndexing (𝐒 a) b))
pairIndexing-def3 {𝟎}   {b} = [≡]-intro
pairIndexing-def3 {𝐒 a} {b} = [≡]-intro

instance
  {-# TERMINATING #-}
  pairIndexing-inverseₗ : Inverseₗ(Tuple.uncurry pairIndexing)(diagonalFilling)
  pairIndexing-inverseₗ = intro proof where
    proof : Names.Inverses(diagonalFilling)(Tuple.uncurry pairIndexing)
    proof {𝟎    , 𝟎}    = [≡]-intro
    proof {𝐒(a) , 𝟎}    with diagonalFilling(pairIndexing 𝟎 a) | proof {𝟎 , a}
    ... | 𝟎    , 𝟎    | [≡]-intro = [≡]-intro
    ... | 𝟎    , 𝐒(d) | [≡]-intro = [≡]-intro
    ... | 𝐒(c) , 𝟎    | ()
    ... | 𝐒(c) , 𝐒(d) | ()
    {-# CATCHALL #-}
    proof {a    , 𝐒(b)} rewrite pairIndexing-def3 {a}{b} with diagonalFilling(pairIndexing (𝐒(a)) b) | proof {𝐒(a) , b}
    ... | 𝟎    , 𝟎    | ()
    ... | 𝟎    , 𝐒(d) | ()
    ... | 𝐒(c) , 𝟎    | [≡]-intro = [≡]-intro
    ... | 𝐒(c) , 𝐒(d) | [≡]-intro = [≡]-intro

instance
  pairIndexing-inverseᵣ : Inverseᵣ(Tuple.uncurry pairIndexing)(diagonalFilling)
  pairIndexing-inverseᵣ = intro proof where
    proof : Names.Inverses(Tuple.uncurry pairIndexing)(diagonalFilling)
    proof {𝟎}    = [≡]-intro
    proof {𝐒(n)} with diagonalFilling n | proof {n}
    ... | (𝟎    , b) | q = congruence₁(𝐒) q
    ... | (𝐒(a) , b) | q rewrite pairIndexing-def3 {a}{b} = congruence₁(𝐒) q

instance
  pairIndexing-inverse : Inverse(Tuple.uncurry pairIndexing)(diagonalFilling)
  pairIndexing-inverse = [∧]-intro pairIndexing-inverseₗ pairIndexing-inverseᵣ

instance
  diagonalFilling-inverse : Inverse(diagonalFilling)(Tuple.uncurry pairIndexing)
  diagonalFilling-inverse = [∧]-intro pairIndexing-inverseᵣ pairIndexing-inverseₗ

instance
  pairIndexing-bijective : Bijective(Tuple.uncurry pairIndexing)
  pairIndexing-bijective = invertible-to-bijective ⦃ inver = [∃]-intro diagonalFilling ⦃ [∧]-intro [≡]-function pairIndexing-inverse ⦄ ⦄

instance
  diagonalFilling-bijective : Bijective(diagonalFilling)
  diagonalFilling-bijective = invertible-to-bijective ⦃ inver = [∃]-intro (Tuple.uncurry pairIndexing) ⦃ [∧]-intro Id-to-function diagonalFilling-inverse ⦄ ⦄

tupleIndexing-inverseᵣ : Inverseᵣ(tupleIndexing{𝐒(n)})(spaceFilling{𝐒(n)})
tupleIndexing-inverseᵣ{n} = intro(proof{n}) where
  proof : ∀{n} → Names.Inverses(tupleIndexing{𝐒(n)})(spaceFilling{𝐒(n)})
  proof {𝟎}   {_} = [≡]-intro
  proof {𝐒(n)}{i} with (x , y) ← diagonalFilling i | intro [≡]-intro ← inspect diagonalFilling i =
    pairIndexing x (tupleIndexing{𝐒(n)} (spaceFilling{𝐒(n)} y)) 🝖[ _≡_ ]-[ congruence₁(pairIndexing(x)) (proof{n}{y}) ]
    pairIndexing x y                                            🝖[ _≡_ ]-[ inverseᵣ(Tuple.uncurry pairIndexing)(diagonalFilling) ]
    i                                                           🝖-end

tupleIndexing-inverseₗ : Inverseₗ(tupleIndexing{𝐒(n)})(spaceFilling{𝐒(n)})
tupleIndexing-inverseₗ{n} = intro(proof{n}) where
  proof : ∀{n} → Names.Inverses(spaceFilling{𝐒(n)})(tupleIndexing{𝐒(n)})
  proof {𝟎}   {_}      = [≡]-intro
  proof {𝐒(n)}{x , xs} =
    Tuple.mapRight spaceFilling (diagonalFilling (pairIndexing x (tupleIndexing xs))) 🝖[ _≡_ ]-[ congruence₁(Tuple.mapRight spaceFilling) (inverseₗ(Tuple.uncurry pairIndexing)(diagonalFilling)) ]
    Tuple.mapRight spaceFilling (x , tupleIndexing xs)                                🝖[ _≡_ ]-[]
    (x , spaceFilling(tupleIndexing xs))                                              🝖[ _≡_ ]-[ congruence₂ᵣ(_,_)(x) (proof{n}{xs}) ]
    (x , xs)                                                                          🝖-end

instance
  tupleIndexing-inverse : Inverse(tupleIndexing{𝐒(n)})(spaceFilling{𝐒(n)})
  tupleIndexing-inverse = [∧]-intro tupleIndexing-inverseₗ tupleIndexing-inverseᵣ

instance
  tupleIndexing-bijective : Bijective(tupleIndexing{𝐒(n)})
  tupleIndexing-bijective = invertible-to-bijective ⦃ inver = [∃]-intro spaceFilling ⦃ [∧]-intro [≡]-function tupleIndexing-inverse ⦄ ⦄

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-AB : Equiv{ℓₑ}(A ‖ B) ⦄ ⦃ ext-AB : Either.Extensionality ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (equiv-AB) ⦄
  {af : ℕ → A} ⦃ bij-af : Bijective ⦃ [≡]-equiv ⦄ ⦃ equiv-A ⦄ (af) ⦄
  {bf : ℕ → B} ⦃ bij-bf : Bijective ⦃ [≡]-equiv ⦄ ⦃ equiv-B ⦄ (bf) ⦄
  where

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

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-AB : Equiv{ℓₑ}(A ⨯ B) ⦄ ⦃ ext-AB : Tuple.Extensionality ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (equiv-AB) ⦄
  {af : ℕ → A} ⦃ bij-af : Bijective ⦃ [≡]-equiv ⦄ ⦃ equiv-A ⦄ (af) ⦄
  {bf : ℕ → B} ⦃ bij-bf : Bijective ⦃ [≡]-equiv ⦄ ⦃ equiv-B ⦄ (bf) ⦄
  where

  instance
    pair-bijective : Bijective ⦃ [≡]-equiv ⦄ ⦃ equiv-AB ⦄ (pair af bf)
    pair-bijective = [∘]-bijective ⦃ bij-f = Tuple.map-bijective ⦃ Id-equiv ⦄ ⦃ Id-equiv ⦄ ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ ⦃ Id-equiv ⦄ ⦄ ⦃ bij-g = diagonalFilling-bijective ⦄

{- TODO: Old stuff. Probably okay to delete? But maybe it could be handy when the new interleave is used (it is similar to the old one)?

-- Interleaves two sequences into one, alternating between the elements from each sequence.
interleave : (ℕ → A) → (ℕ → B) → (ℕ → (A ‖ B))
interleave af bf 𝟎        = Either.Left(af(𝟎))
interleave af bf (𝐒 𝟎)    = Either.Right(bf(𝟎))
interleave af bf (𝐒(𝐒 n)) = interleave (af ∘ 𝐒) (bf ∘ 𝐒) n

private variable af : ℕ → A
private variable bf : ℕ → B

interleave-left : ∀{n} → (interleave af bf (2 ⋅ n) ≡ Either.Left(af(n)))
interleave-left {n = 𝟎}   = [≡]-intro
interleave-left {n = 𝐒 n} = interleave-left {n = n}

interleave-right : ∀{n} → (interleave af bf (𝐒(2 ⋅ n)) ≡ Either.Right(bf(n)))
interleave-right {n = 𝟎}   = [≡]-intro
interleave-right {n = 𝐒 n} = interleave-right {n = n}

interleave-values : ∀{n} → (interleave af bf n ≡ Either.Left(af(n ⌊/⌋ 2))) ∨ (interleave af bf n ≡ Either.Right(bf(n ⌊/⌋ 2)))
interleave-values                    {n = 𝟎}      = [∨]-introₗ [≡]-intro
interleave-values                    {n = 𝐒 𝟎}    = [∨]-introᵣ [≡]-intro
interleave-values {af = af}{bf = bf} {n = 𝐒(𝐒 n)} = interleave-values {af = af ∘ 𝐒}{bf = bf ∘ 𝐒} {n = n}

interleave-left-args : ⦃ _ : Injective(af) ⦄ → ∀{m n} → (interleave af bf m ≡ Either.Left(af(n))) ↔ (m ≡ 2 ⋅ n)
interleave-left-args {n = n} = [↔]-intro (\{[≡]-intro → interleave-left{n = n}}) r where
  r : ⦃ _ : Injective(af) ⦄ → ∀{m n} → (interleave af bf m ≡ Either.Left(af(n))) → (m ≡ 2 ⋅ n)
  r {af = af} {m = 𝟎}{n = n} = congruence₁(2 ⋅_) ∘ injective(af) ∘ injective(Either.Left) ⦃ Left-injective ⦄
  r {af = af}{bf = bf} {m = 𝐒 (𝐒 m)}{n = 𝟎} p with interleave-values {af = af}{bf = bf}{n = 𝐒(𝐒 m)}
  ... | [∨]-introₗ v with () ← injective(af) (injective(Either.Left) ⦃ Left-injective ⦄ (symmetry(_≡_) v 🝖 p))
  ... | [∨]-introᵣ v with () ← symmetry(_≡_) v 🝖 p
  r {af = af} {m = 𝐒 (𝐒 m)}{n = 𝐒 n} p = congruence₁(𝐒 ∘ 𝐒) (r ⦃ [∘]-injective {f = af} ⦄{m = m}{n = n} p)

interleave-right-args : ⦃ _ : Injective(bf) ⦄ → ∀{m n} → (interleave af bf m ≡ Either.Right(bf(n))) ↔ (m ≡ 𝐒(2 ⋅ n))
interleave-right-args {n = n} = [↔]-intro (\{[≡]-intro → interleave-right{n = n}}) r where
  r : ⦃ _ : Injective(bf) ⦄ → ∀{m n} → (interleave af bf m ≡ Either.Right(bf(n))) → (m ≡ 𝐒(2 ⋅ n))
  r {bf = bf} {m = 𝐒 𝟎}{n = n} = congruence₁(𝐒 ∘ (2 ⋅_)) ∘ injective(bf) ∘ injective(Either.Right) ⦃ Right-injective ⦄
  r {bf = bf}{af = af} {m = 𝐒 (𝐒 m)}{n = 𝟎} p with interleave-values {af = af}{bf = bf}{n = 𝐒(𝐒 m)}
  ... | [∨]-introₗ v with () ← symmetry(_≡_) v 🝖 p
  ... | [∨]-introᵣ v with () ← injective(bf) (injective(Either.Right) ⦃ Right-injective ⦄ (symmetry(_≡_) v 🝖 p))
  r {bf = bf} {m = 𝐒 (𝐒 m)}{n = 𝐒 n} p = congruence₁(𝐒 ∘ 𝐒) (r ⦃ [∘]-injective {f = bf} ⦄{m = m}{n = n} p)

interleave-step-left : ⦃ _ : Injective(af) ⦄ → ∀{m n} → (interleave af bf m ≡ Either.Left(af(n))) ↔ (interleave af bf (𝐒(𝐒 m)) ≡ Either.Left(af(𝐒 n)))
interleave-step-left{af = iaf}{bf = ibf}{m = m}{n = n} = [↔]-intro (l{af = iaf}{bf = ibf}{m = m}{n = n}) (r{af = iaf}{bf = ibf}{m = m}{n = n}) where
  l : ⦃ _ : Injective(af) ⦄ → ∀{m n} → (interleave af bf m ≡ Either.Left(af(n))) ← (interleave af bf (𝐒(𝐒 m)) ≡ Either.Left(af(𝐒 n)))
  l {af = af}          {m = 𝟎}      {n}   = congruence₁(Either.Left) ∘ congruence₁(af) ∘ injective(𝐒) ∘ injective(af) ∘ injective(Either.Left) ⦃ Left-injective ⦄
  l {af = af}{bf = bf} {m = 𝐒 (𝐒 m)}{𝟎}   p with interleave-values {af = af}{bf = bf}{n = 𝐒(𝐒(𝐒(𝐒 m)))}
  ... | [∨]-introₗ v with () ← injective(af) (injective(Either.Left) ⦃ Left-injective ⦄ (symmetry(_≡_) v 🝖 p))
  ... | [∨]-introᵣ v with () ← symmetry(_≡_) v 🝖 p
  l {af = af}          {m = 𝐒 (𝐒 m)}{𝐒 n} = l {af = af ∘ 𝐒} ⦃ [∘]-injective {f = af} ⦄ {m = m}{n}

  r : ⦃ _ : Injective(af) ⦄ → ∀{m n} → (interleave af bf m ≡ Either.Left(af(n))) → (interleave af bf (𝐒(𝐒 m)) ≡ Either.Left(af(𝐒 n)))
  r {af = af}          {m = 𝟎}      {n}   = congruence₁(Either.Left) ∘ congruence₁(af) ∘ congruence₁(𝐒) ∘ injective(af) ∘ injective(Either.Left) ⦃ Left-injective ⦄
  r {af = af}{bf = bf} {m = 𝐒(𝐒 m)} {𝟎}   p with interleave-values {af = af}{bf = bf}{n = 𝐒(𝐒 m)}
  ... | [∨]-introₗ v with () ← injective(af) (injective(Either.Left) ⦃ Left-injective ⦄ (symmetry(_≡_) v 🝖 p))
  ... | [∨]-introᵣ v with () ← symmetry(_≡_) v 🝖 p
  r {af = af}          {m = 𝐒(𝐒 m)} {𝐒 n} = r {af = af ∘ 𝐒} ⦃ [∘]-injective {f = af} ⦄ {m = m}{n}

postulate interleave-injective-raw : ⦃ inj-af : Injective(af) ⦄ → ⦃ inj-bf : Injective(bf) ⦄ → Names.Injective(interleave af bf)
{-interleave-injective-raw {af = af} {bf = bf} {x = 𝟎}       {y = 𝟎}       fxfy = [≡]-intro
interleave-injective-raw {af = af} {bf = bf} {x = 𝟎}       {y = 𝐒 (𝐒 y)} fxfy = symmetry(_≡_) ([↔]-to-[→] (interleave-left-args {bf = bf}) (symmetry(_≡_) fxfy))
interleave-injective-raw {af = af} {bf = bf} {x = 𝐒 (𝐒 x)} {y = 𝟎}       fxfy = [↔]-to-[→] (interleave-left-args {bf = bf}) fxfy
interleave-injective-raw {af = af} {bf = bf} {x = 𝐒 𝟎} {y = 𝐒 𝟎} fxfy = [≡]-intro
interleave-injective-raw {af = af} {bf = bf} {x = 𝐒 𝟎} {y = 𝐒 (𝐒 y)} fxfy = symmetry(_≡_) ([↔]-to-[→] (interleave-right-args {bf = bf}{af = af}) (symmetry(_≡_) fxfy))
interleave-injective-raw {af = af} {bf = bf} {x = 𝐒 (𝐒 x)} {y = 𝐒 𝟎} fxfy = [↔]-to-[→] (interleave-right-args {bf = bf}{af = af}) fxfy
interleave-injective-raw {af = af} {bf = bf} {x = 𝐒 (𝐒 x)} {y = 𝐒 (𝐒 y)} fxfy with interleave-values {af = af ∘ 𝐒}{bf = bf ∘ 𝐒}{n = x} | interleave-values {af = af ∘ 𝐒}{bf = bf ∘ 𝐒}{n = y}
... | [∨]-introₗ p | [∨]-introₗ q = {!congruence₁(𝐒) (injective(af) (injective(Either.Left) (symmetry(_≡_) p 🝖 fxfy 🝖 q)))!} -- TODO: interleave-left and a proof of the division algorihm would work here instead of using interleave-values. Or alternatively, use this, multiply by 2, prove the divisibilities for both cases so that each case have division as inverse of multiplication
... | [∨]-introₗ p | [∨]-introᵣ q = {!!}
... | [∨]-introᵣ p | [∨]-introₗ q = {!!}
... | [∨]-introᵣ p | [∨]-introᵣ q = {!congruence₁(𝐒) (injective(bf) (injective(Either.Right) (symmetry(_≡_) p 🝖 fxfy 🝖 q)))!}
-}

instance
  interleave-injective : ⦃ inj-af : Injective(af) ⦄ → ⦃ inj-bf : Injective(bf) ⦄ → Injective(interleave af bf)
  interleave-injective = intro interleave-injective-raw

instance
  interleave-surjective : ⦃ surj-af : Surjective(af) ⦄ → ⦃ surj-bf : Surjective(bf) ⦄ → Surjective(interleave af bf)
  Surjective.proof (interleave-surjective {af = af}{bf = bf}) {[∨]-introₗ y} with surjective(af){y}
  ... | [∃]-intro n ⦃ [≡]-intro ⦄ = [∃]-intro(2 ⋅ n) ⦃ interleave-left{n = n} ⦄
  Surjective.proof (interleave-surjective {af = af}{bf = bf}) {[∨]-introᵣ y} with surjective(bf){y}
  ... | [∃]-intro n ⦃ [≡]-intro ⦄ = [∃]-intro(𝐒(2 ⋅ n)) ⦃ interleave-right{n = n} ⦄

instance
  interleave-bijective : ⦃ bij-af : Bijective(af) ⦄ → ⦃ bij-bf : Bijective(bf) ⦄ → Bijective(interleave af bf)
  interleave-bijective {af = af}{bf = bf} = injective-surjective-to-bijective(interleave af bf) where
    instance
      inj-af : Injective(af)
      inj-af = bijective-to-injective af
    instance
      inj-bf : Injective(bf)
      inj-bf = bijective-to-injective bf
    instance
      surj-af : Surjective(af)
      surj-af = bijective-to-surjective af
    instance
      surj-bf : Surjective(bf)
      surj-bf = bijective-to-surjective bf
-}

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:
module Issue347 where
import Common.Irrelevance

{- Dan Doel, 2010-10-09

This is a boiling down of a problem encountered by Eric Mertens. It
seems the unifier will make up values for records without bothering
with irrelevant fields: -}

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

⊥-elimⁱ : {A : Set} → .⊥ → A
⊥-elimⁱ ()

module Bad where
  record ○ (A : Set) : Set where
    constructor poof
    field
      .inflate : A

  open ○

  -- This, for some reason, doesn't. Apparently it thinks it can
  -- make up records without bothering to infer the irrelevant fields.
  evil : ∀ A → A
  evil A = ⊥-elimⁱ (inflate _)

  -- the meta var  ?a : Squash A  eta-expands to
  -- ?a = poof Bot ?b
  -- meta var ?b should be left over


text:
data ⊤ : Set where
  t : ⊤

data ⊤⊤ : Set where
  tt : ⊤⊤

module M (x : ⊤⊤) where

  instance
    top : ⊤
    top = t

search : ∀ {ℓ} {t : Set ℓ} {{_ : t}} → t
search {{p}} = p

-- no instance is in scope, and none is found
-- correct : ⊤
-- correct = search

someDef : ⊤
someDef = top
  where
    open M tt

-- incorrect! there should be no instance available.
leak : ⊤
leak = search


text:
module IsLiteralSequent where

open import OscarPrelude
open import Sequent
open import IsLiteralFormula

record IsLiteralSequent (Φ : Sequent) : Set
 where
  constructor _╱_
  field
    isLiteralStatement : IsLiteralFormula (statement Φ)
    isLiteralSuppositions : All IsLiteralFormula (suppositions Φ)

open IsLiteralSequent public

instance EqIsLiteralSequent : ∀ {Φ} → Eq (IsLiteralSequent Φ)
Eq._==_ EqIsLiteralSequent ( φᵗ₁ ╱ φˢs₁ ) ( φᵗ₂ ╱ φˢs₂ ) = decEq₂ (cong isLiteralStatement) (cong isLiteralSuppositions) (φᵗ₁ ≟ φᵗ₂) (φˢs₁ ≟ φˢs₂)


text:
------------------------------------------------------------------------------
-- Totality properties respect to OrdTree
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.SortList.Properties.Totality.OrdTreeATP where

open import FOTC.Base
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Program.SortList.SortList
open import FOTC.Program.SortList.Properties.Totality.BoolATP
open import FOTC.Program.SortList.Properties.Totality.TreeATP

------------------------------------------------------------------------------
-- Subtrees

-- If (node t₁ i t₂) is ordered then t₁ is ordered.
postulate leftSubTree-OrdTree : ∀ {t₁ i t₂} → Tree t₁ → N i → Tree t₂ →
                                OrdTree (node t₁ i t₂) → OrdTree t₁
{-# ATP prove leftSubTree-OrdTree &&-Bool &&-list₂-t le-ItemTree-Bool le-TreeItem-Bool ordTree-Bool #-}

-- If (node t₁ i t₂) is ordered then t₂ is ordered.
postulate rightSubTree-OrdTree : ∀ {t₁ i t₂} → Tree t₁ → N i → Tree t₂ →
                                 OrdTree (node t₁ i t₂) → OrdTree t₂
-- 2018-06-28: The ATPs could not prove the theorem (300 sec), but
-- Vampire 4.2.2, via `online-atps`, could prove it.
--
-- {-# ATP prove rightSubTree-OrdTree &&-Bool &&-list₂-t le-ItemTree-Bool le-TreeItem-Bool ordTree-Bool #-}

------------------------------------------------------------------------------
-- Helper functions

toTree-OrdTree-helper₁ : ∀ {i₁ i₂ t} → N i₁ → N i₂ → i₁ > i₂ →
                         Tree t →
                         ≤-TreeItem t i₁ →
                         ≤-TreeItem (toTree · i₂ · t) i₁
toTree-OrdTree-helper₁ {i₁} {i₂} .{nil} Ni₁ Ni₂ i₁>i₂ tnil t≤i₁ = prf
  where postulate prf : ≤-TreeItem (toTree · i₂ · nil) i₁
        {-# ATP prove prf x<y→x≤y #-}

toTree-OrdTree-helper₁ {i₁} {i₂} Ni₁ Ni₂ i₁>i₂ (ttip {j} Nj) t≤i₁ =
  case prf₁ prf₂ (x>y∨x≤y Nj Ni₂)
  where
  postulate prf₁ : j > i₂ → ≤-TreeItem (toTree · i₂ · tip j) i₁
  {-# ATP prove prf₁ x>y→x≰y x<y→x≤y #-}

  postulate prf₂ : j ≤ i₂ → ≤-TreeItem (toTree · i₂ · tip j) i₁
  {-# ATP prove prf₂ x<y→x≤y #-}

toTree-OrdTree-helper₁ {i₁} {i₂} Ni₁ Ni₂ i₁>i₂
                       (tnode {t₁} {j} {t₂} Tt₁ Nj Tt₂) t≤i₁ =
  case (prf₁ (toTree-OrdTree-helper₁ Ni₁ Ni₂ i₁>i₂ Tt₁
               (&&-list₂-t₁ (le-TreeItem-Bool Tt₁ Ni₁)
                            (le-TreeItem-Bool Tt₂ Ni₁)
                            (trans (sym (le-TreeItem-node t₁ j t₂ i₁)) t≤i₁))))

       (prf₂ (toTree-OrdTree-helper₁ Ni₁ Ni₂ i₁>i₂ Tt₂
               (&&-list₂-t₂ (le-TreeItem-Bool Tt₁ Ni₁)
                            (le-TreeItem-Bool Tt₂ Ni₁)
                            (trans (sym (le-TreeItem-node t₁ j t₂ i₁)) t≤i₁))))
       (x>y∨x≤y Nj Ni₂)
  where
  postulate prf₁ : ≤-TreeItem (toTree · i₂ · t₁) i₁ →
                   j > i₂ →
                   ≤-TreeItem (toTree · i₂ · node t₁ j t₂) i₁
  {-# ATP prove prf₁ x>y→x≰y &&-list₂-t le-TreeItem-Bool #-}

  postulate prf₂ : ≤-TreeItem (toTree · i₂ · t₂) i₁ →
                   j ≤ i₂ →
                   ≤-TreeItem (toTree · i₂ · node t₁ j t₂) i₁
  {-# ATP prove prf₂ &&-list₂-t le-TreeItem-Bool #-}

toTree-OrdTree-helper₂ : ∀ {i₁ i₂ t} → N i₁ → N i₂ → i₁ ≤ i₂ →
                         Tree t →
                         ≤-ItemTree i₁ t →
                         ≤-ItemTree i₁ (toTree · i₂ · t)
toTree-OrdTree-helper₂ {i₁} {i₂} .{nil} Ni₁ Ni₂ i₁≤i₂ tnil i₁≤t = prf
  where postulate prf : ≤-ItemTree i₁ (toTree · i₂ · nil)
        {-# ATP prove prf #-}

toTree-OrdTree-helper₂ {i₁} {i₂} Ni₁ Ni₂ i₁≤i₂ (ttip {j} Nj) i₁≤t =
  case prf₁ prf₂ (x>y∨x≤y Nj Ni₂)
  where
  postulate prf₁ : j > i₂ → ≤-ItemTree i₁ (toTree · i₂ · tip j)
  {-# ATP prove prf₁ x>y→x≰y #-}

  postulate prf₂ : j ≤ i₂ → ≤-ItemTree i₁ (toTree · i₂ · tip j)
  {-# ATP prove prf₂ #-}

toTree-OrdTree-helper₂ {i₁} {i₂} Ni₁ Ni₂ i₁≤i₂
                       (tnode {t₁} {j} {t₂} Tt₁ Nj Tt₂) i₁≤t =
  case (prf₁ (toTree-OrdTree-helper₂ Ni₁ Ni₂ i₁≤i₂ Tt₁
               (&&-list₂-t₁ (le-ItemTree-Bool Ni₁ Tt₁)
                            (le-ItemTree-Bool Ni₁ Tt₂)
                            (trans (sym (le-ItemTree-node i₁ t₁ j t₂)) i₁≤t))))

       (prf₂ (toTree-OrdTree-helper₂ Ni₁ Ni₂ i₁≤i₂ Tt₂
               (&&-list₂-t₂ (le-ItemTree-Bool Ni₁ Tt₁)
                            (le-ItemTree-Bool Ni₁ Tt₂)
                            (trans (sym (le-ItemTree-node i₁ t₁ j t₂)) i₁≤t))))
       (x>y∨x≤y Nj Ni₂)
  where
  postulate prf₁ : ≤-ItemTree i₁ (toTree · i₂ · t₁) →
                   j > i₂ →
                   ≤-ItemTree i₁ (toTree · i₂ · node t₁ j t₂)
  {-# ATP prove prf₁ x>y→x≰y &&-list₂-t le-ItemTree-Bool #-}

  postulate prf₂ : ≤-ItemTree i₁ (toTree · i₂ · t₂) →
                   j ≤ i₂ →
                   ≤-ItemTree i₁ (toTree · i₂ · node t₁ j t₂)
  {-# ATP prove prf₂ &&-list₂-t le-ItemTree-Bool #-}