text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Well-founded induction
------------------------------------------------------------------------

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

open import Relation.Binary

module Induction.WellFounded where

open import Data.Product
open import Function
open import Induction
open import Level
open import Relation.Binary.PropositionalEquality hiding (trans)
open import Relation.Unary

private
  variable
    a b ℓ ℓ₁ ℓ₂ r : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Definitions

-- When using well-founded recursion you can recurse arbitrarily, as
-- long as the arguments become smaller, and "smaller" is
-- well-founded.

WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
WfRec _<_ P x = ∀ y → y < x → P y

-- The accessibility predicate: x is accessible if everything which is
-- smaller than x is also accessible (inductively).

data Acc {A : Set a} (_<_ : Rel A ℓ) (x : A) : Set (a ⊔ ℓ) where
  acc : (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x

acc-inverse : ∀ {_<_ : Rel A ℓ} {x : A} (q : Acc _<_ x) →
              (y : A) → y < x → Acc _<_ y
acc-inverse (acc rs) y y<x = rs y y<x

-- The accessibility predicate encodes what it means to be
-- well-founded; if all elements are accessible, then _<_ is
-- well-founded.

WellFounded : Rel A ℓ → Set _
WellFounded _<_ = ∀ x → Acc _<_ x

Well-founded = WellFounded
{-# WARNING_ON_USAGE Well-founded
"Warning: Well-founded was deprecated in v0.15.
Please use WellFounded instead."
#-}

------------------------------------------------------------------------
-- Basic properties

Acc-resp-≈ : {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} → Symmetric _≈_ →
             _<_ Respectsʳ _≈_ → (Acc _<_) Respects _≈_
Acc-resp-≈ sym respʳ x≈y (acc rec) =
  acc (λ z z<y → rec z (respʳ (sym x≈y) z<y))

------------------------------------------------------------------------
-- Well-founded induction for the subset of accessible elements:

module Some {_<_ : Rel A r} {ℓ} where

  wfRecBuilder : SubsetRecursorBuilder (Acc _<_) (WfRec _<_ {ℓ = ℓ})
  wfRecBuilder P f x (acc rs) = λ y y<x →
    f y (wfRecBuilder P f y (rs y y<x))

  wfRec : SubsetRecursor (Acc _<_) (WfRec _<_)
  wfRec = subsetBuild wfRecBuilder

  unfold-wfRec : (P : Pred A ℓ) (f : WfRec _<_ P ⊆′ P) {x : A} (q : Acc _<_ x) →
                 wfRec P f x q ≡ f x (λ y y<x → wfRec P f y (acc-inverse q y y<x))
  unfold-wfRec P f (acc rs) = refl

  wfRec-builder = wfRecBuilder
  {-# WARNING_ON_USAGE wfRec-builder
  "Warning: wfRec-builder was deprecated in v0.15.
\ \Please use wfRecBuilder instead."
  #-}

------------------------------------------------------------------------
-- Well-founded induction for all elements, assuming they are all
-- accessible:

module All {_<_ : Rel A r} (wf : WellFounded _<_) ℓ where

  wfRecBuilder : RecursorBuilder (WfRec _<_ {ℓ = ℓ})
  wfRecBuilder P f x = Some.wfRecBuilder P f x (wf x)

  wfRec : Recursor (WfRec _<_)
  wfRec = build wfRecBuilder

  wfRec-builder = wfRecBuilder
  {-# WARNING_ON_USAGE wfRec-builder
  "Warning: wfRec-builder was deprecated in v0.15.
\ \Please use wfRecBuilder instead."
  #-}

module FixPoint
  {_<_ : Rel A ℓ} (wf : WellFounded _<_)
  (P : Pred A ℓ) (f : WfRec _<_ P ⊆′ P)
  (f-ext : (x : A) {IH IH' : WfRec _<_ P x} → (∀ {y} y<x → IH y y<x ≡ IH' y y<x) → f x IH ≡ f x IH')
  where

  some-wfRec-irrelevant : ∀ x → (q q' : Acc _<_ x) → Some.wfRec P f x q ≡ Some.wfRec P f x q'
  some-wfRec-irrelevant = All.wfRec wf _
                                   (λ x → (q q' : Acc _<_ x) → Some.wfRec P f x q ≡ Some.wfRec P f x q')
                                   (λ { x IH (acc rs) (acc rs') → f-ext x (λ y<x → IH _ y<x (rs _ y<x) (rs' _ y<x)) })

  open All wf ℓ
  wfRecBuilder-wfRec : ∀ {x y} y<x → wfRecBuilder P f x y y<x ≡ wfRec P f y
  wfRecBuilder-wfRec {x} {y} y<x with wf x
  ... | acc rs = some-wfRec-irrelevant y (rs y y<x) (wf y)

  unfold-wfRec : ∀ {x} → wfRec P f x ≡ f x (λ y _ → wfRec P f y)
  unfold-wfRec {x} = f-ext x wfRecBuilder-wfRec

------------------------------------------------------------------------
-- It might be useful to establish proofs of Acc or Well-founded using
-- combinators such as the ones below (see, for instance,
-- "Constructing Recursion Operators in Intuitionistic Type Theory" by
-- Lawrence C Paulson).

module Subrelation {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂}
                   (<₁⇒<₂ : ∀ {x y} → x <₁ y → x <₂ y) where

  accessible : Acc _<₂_ ⊆ Acc _<₁_
  accessible (acc rs) = acc (λ y y<x → accessible (rs y (<₁⇒<₂ y<x)))

  wellFounded : WellFounded _<₂_ → WellFounded _<₁_
  wellFounded wf = λ x → accessible (wf x)

  well-founded = wellFounded
  {-# WARNING_ON_USAGE well-founded
  "Warning: well-founded was deprecated in v0.15.
\ \Please use wellFounded instead."
  #-}

module InverseImage {_<_ : Rel B ℓ} (f : A → B) where

  accessible : ∀ {x} → Acc _<_ (f x) → Acc (_<_ on f) x
  accessible (acc rs) = acc (λ y fy<fx → accessible (rs (f y) fy<fx))

  wellFounded : WellFounded _<_ → WellFounded (_<_ on f)
  wellFounded wf = λ x → accessible (wf (f x))

  well-founded = wellFounded
  {-# WARNING_ON_USAGE well-founded
  "Warning: well-founded was deprecated in v0.15.
\ \Please use wellFounded instead."
  #-}

module TransitiveClosure {A : Set a} (_<_ : Rel A ℓ) where

  infix 4 _<⁺_

  data _<⁺_ : Rel A (a ⊔ ℓ) where
    [_]   : ∀ {x y} (x<y : x < y) → x <⁺ y
    trans : ∀ {x y z} (x<y : x <⁺ y) (y<z : y <⁺ z) → x <⁺ z

  downwardsClosed : ∀ {x y} → Acc _<⁺_ y → x <⁺ y → Acc _<⁺_ x
  downwardsClosed (acc rs) x<y = acc (λ z z<x → rs z (trans z<x x<y))

  mutual

    accessible : ∀ {x} → Acc _<_ x → Acc _<⁺_ x
    accessible acc-x = acc (accessible′ acc-x)

    accessible′ : ∀ {x} → Acc _<_ x → WfRec _<⁺_ (Acc _<⁺_) x
    accessible′ (acc rs) y [ y<x ]         = accessible (rs y y<x)
    accessible′ acc-x    y (trans y<z z<x) =
      downwardsClosed (accessible′ acc-x _ z<x) y<z

  wellFounded : WellFounded _<_ → WellFounded _<⁺_
  wellFounded wf = λ x → accessible (wf x)

  downwards-closed = downwardsClosed
  {-# WARNING_ON_USAGE downwards-closed
  "Warning: downwards-closed was deprecated in v0.15.
\ \Please use downwardsClosed instead."
  #-}
  well-founded     = wellFounded
  {-# WARNING_ON_USAGE well-founded
  "Warning: well-founded was deprecated in v0.15.
\ \Please use wellFounded instead."
  #-}

-- DEPRECATED in v1.3.
-- Please use `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict` instead.
module Lexicographic {A : Set a} {B : A → Set b}
                     (RelA : Rel A ℓ₁)
                     (RelB : ∀ x → Rel (B x) ℓ₂) where

  data _<_ : Rel (Σ A B) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    left  : ∀ {x₁ y₁ x₂ y₂} (x₁<x₂ : RelA   x₁ x₂) → (x₁ , y₁) < (x₂ , y₂)
    right : ∀ {x y₁ y₂}     (y₁<y₂ : RelB x y₁ y₂) → (x  , y₁) < (x  , y₂)

  mutual

    accessible : ∀ {x y} →
                 Acc RelA x → (∀ {x} → WellFounded (RelB x)) →
                 Acc _<_ (x , y)
    accessible accA wfB = acc (accessible′ accA (wfB _) wfB)

    accessible′ :
      ∀ {x y} →
      Acc RelA x → Acc (RelB x) y → (∀ {x} → WellFounded (RelB x)) →
      WfRec _<_ (Acc _<_) (x , y)
    accessible′ (acc rsA) _    wfB ._ (left  x′<x) = accessible (rsA _ x′<x) wfB
    accessible′ accA (acc rsB) wfB ._ (right y′<y) =
      acc (accessible′ accA (rsB _ y′<y) wfB)

  wellFounded : WellFounded RelA → (∀ {x} → WellFounded (RelB x)) →
                WellFounded _<_
  wellFounded wfA wfB p = accessible (wfA (proj₁ p)) wfB

  well-founded = wellFounded

  {-# WARNING_ON_USAGE _<_
  "Warning: _<_ was deprecated in v1.3.
\ \Please use `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict` instead."
  #-}
  {-# WARNING_ON_USAGE accessible
  "Warning: accessible was deprecated in v1.3."
  #-}
  {-# WARNING_ON_USAGE accessible′
  "Warning: accessible′ was deprecated in v1.3."
  #-}
  {-# WARNING_ON_USAGE wellFounded
  "Warning: wellFounded was deprecated in v1.3.
\ \Please use `×-wellFounded` from `Data.Product.Relation.Binary.Lex.Strict` instead."
  #-}
  {-# WARNING_ON_USAGE well-founded
  "Warning: well-founded was deprecated in v0.15.
\ \Please use wellFounded instead."
  #-}

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

module Inverse-image = InverseImage
module Transitive-closure = TransitiveClosure


text:
-- Andreas, 2016-02-02 postpone type checking of extended lambda
-- See also issue 480 and 1159

open import Common.Maybe
open import Common.String

record ⊤ : Set where

record IOInterface : Set₁ where
  field  Command   :  Set
         Response  :  (m : Command) → Set
open IOInterface

data IO I A : Set where
  do'      :  (c : Command I) (f : Response I c → IO I A)  → IO I A
  return   :  (a : A)                                      → IO I A

-- Alias of constructor which is a function
do :  ∀{I A} (c : Command I) (f : Response I c → IO I A) → IO I A
do c f    =  do' c f

data C : Set where
  getLine   :  C
  putStrLn  :  String → C

R : C → Set
R  getLine      =  Maybe String
R (putStrLn s)  =  ⊤

I : IOInterface
Command   I  =  C
Response  I  =  R

works : IO I ⊤
works = do'  getLine        λ{ nothing → return _ ; (just line) →
        do (putStrLn line)  λ _ →
        return _            }

test : IO I ⊤
test = do  getLine         λ{ nothing → return _ ; (just line) →
       do (putStrLn line)  λ _ →
       return _            }

ext: agda


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

open import HoTT
open import cohomology.FunctionOver
open import homotopy.elims.CofPushoutSection

module cohomology.MayerVietoris {i} where

{- Mayer-Vietoris Sequence: Given a span X ←f– Z –g→ Y, the cofiber space
   of the natural map [reglue : X ∨ Y → X ⊔_Z Y] (defined below) is equivalent
   to the suspension of Z. -}

{- Relevant functions -}
module MayerVietorisFunctions (ps : ⊙Span {i} {i} {i}) where

  open ⊙Span ps

  module Reglue = ⊙WedgeRec (⊙left ps) (⊙right ps)

  reglue : X ∨ Y → fst (⊙Pushout ps)
  reglue = Reglue.f

  ⊙reglue : fst (X ⊙∨ Y ⊙→ ⊙Pushout ps)
  ⊙reglue = Reglue.⊙f

  module MVDiff = SuspensionRec (fst Z) {C = Suspension (X ∨ Y)}
    (north _)
    (north _)
    (λ z → merid _ (winl (fst f z)) ∙ ! (merid _ (winr (fst g z))))

  mv-diff : Suspension (fst Z) → Suspension (X ∨ Y)
  mv-diff = MVDiff.f

  ⊙mv-diff : fst (⊙Susp Z ⊙→ ⊙Susp (X ⊙∨ Y))
  ⊙mv-diff = (mv-diff , idp)

{- We use path induction (via [⊙pushout-J]) to assume that the
   basepoint preservation paths of the span maps are [idp]. The module
   [MayerVietorisBase] contains the proof of the theorem for this case. -}
module MayerVietorisBase
  {A B : Type i} (Z : Ptd i) (f : fst Z → A) (g : fst Z → B) where

  X = ⊙[ A , f (snd Z) ]
  Y = ⊙[ B , g (snd Z) ]
  ps = ⊙span X Y Z (f , idp) (g , idp)
  F : fst (Z ⊙→ X)
  F = (f , idp)
  G : fst (Z ⊙→ Y)
  G = (g , idp)

  open MayerVietorisFunctions ps

  {- Definition of the maps
       into : Cofiber reglue → ΣZ
       out  : ΣZ → Cofiber reglue
   -}

  private
    into-glue-square :
      Square idp idp (ap (ext-glue ∘ reglue) wglue) (merid _ (snd Z))
    into-glue-square =
      connection ⊡v∙
      ! (ap-∘ ext-glue reglue wglue
         ∙ ap (ap ext-glue) (Reglue.glue-β ∙ !-! (glue (snd Z)))
         ∙ ExtGlue.glue-β (snd Z))

    module IntoGlue = WedgeElim {P = λ xy → north _ == ext-glue (reglue xy)}
      (λ _ → idp)
      (λ _ → merid _ (snd Z))
      (↓-cst=app-from-square into-glue-square)

    into-glue = IntoGlue.f

  module Into = CofiberRec reglue (north _) ext-glue into-glue

  private
    out-glue-and-square : (z : fst Z)
      → Σ (cfbase reglue == cfbase reglue)
          (λ p → Square (cfglue _ (winl (f z))) p
                   (ap (cfcod _) (glue z)) (cfglue _ (winr (g z))))
    out-glue-and-square z = fill-square-top _ _ _

    out-glue = fst ∘ out-glue-and-square
    out-square = snd ∘ out-glue-and-square

  module Out = SuspensionRec (fst Z) {C = Cofiber reglue}
    (cfbase _)
    (cfbase _)
    out-glue

  into = Into.f
  out = Out.f

  {- [out] is a right inverse for [into] -}

  private
    into-out-sq : (z : fst Z) →
      Square idp (ap into (ap out (merid _ z))) (merid _ z) (merid _ (snd Z))
    into-out-sq z =
      (ap (ap into) (Out.glue-β z) ∙v⊡
        (! (Into.glue-β (winl (f z)))) ∙h⊡
          ap-square into (out-square z)
        ⊡h∙ (Into.glue-β (winr (g z))))
      ⊡v∙ (∘-ap into (cfcod _) (glue z) ∙ ExtGlue.glue-β z)

  into-out : ∀ σ → into (out σ) == σ
  into-out = Suspension-elim (fst Z)
    idp
    (merid _ (snd Z))
    (λ z → ↓-∘=idf-from-square into out (into-out-sq z))

  {- [out] is a left inverse for [into] -}

  {- [out] is left inverse on codomain part of cofiber space,
   - i.e. [out (into (cfcod _ γ)) == cfcod _ γ] -}

  private
    out-into-cod-square : (z : fst Z) →
      Square (cfglue reglue (winl (f z)))
             (ap (out ∘ ext-glue {s = ⊙span-out ps}) (glue z))
             (ap (cfcod _) (glue z)) (cfglue _ (winr (g z)))
    out-into-cod-square z =
      (ap-∘ out ext-glue (glue z)
        ∙ ap (ap out) (ExtGlue.glue-β z) ∙ Out.glue-β z)
      ∙v⊡ out-square z

    module OutIntoCod = PushoutElim
      {d = ⊙span-out ps} {P = λ γ → out (into (cfcod _ γ)) == cfcod _ γ}
      (λ x → cfglue _ (winl x))
      (λ y → cfglue _ (winr y))
      (λ z → ↓-='-from-square (out-into-cod-square z))

    out-into-cod = OutIntoCod.f

  out-into : ∀ κ → out (into κ) == κ
  out-into = CofPushoutSection.elim reglue
    (λ _ → unit) (λ _ → idp)
    idp
    out-into-cod
    (↓-='-from-square ∘ λ x →
      (ap-∘ out into (cfglue _ (winl x))
       ∙ ap (ap out) (Into.glue-β (winl x)))
      ∙v⊡ connection
      ⊡v∙ ! (ap-idf (glue (winl x))))
    (↓-='-from-square ∘ λ y →
      (ap-∘ out into (cfglue _ (winr y))
       ∙ ap (ap out) (Into.glue-β (winr y))
       ∙ Out.glue-β (snd Z)
       ∙ square-top-unique (out-square (snd Z))
           (! (ap-cst (cfbase _) wglue) ∙v⊡
            natural-square (cfglue _) wglue
            ⊡v∙ (ap-∘ (cfcod _) reglue wglue
                 ∙ ap (ap (cfcod _)) (Reglue.glue-β ∙ !-! (glue (snd Z))))))
      ∙v⊡ connection
      ⊡v∙ ! (ap-idf (glue (winr y))))

  {- equivalence and path -}

  eq : Cofiber reglue ≃ Suspension (fst Z)
  eq = equiv into out into-out out-into

  ⊙eq : ⊙Cof ⊙reglue ⊙≃ ⊙Susp Z
  ⊙eq = ⊙≃-in eq idp

  path = ua eq
  ⊙path = ⊙ua ⊙eq

  {- Transporting [cfcod reglue] over the equivalence -}

  cfcod-over : cfcod reglue == ext-glue
              [ (λ W → fst (⊙Pushout ps) → fst W) ↓ ⊙path ]
  cfcod-over = ↓-cst2-in _ _ $ codomain-over-equiv _ _

  {- Transporting [ext-glue] over the equivalence. -}

  ext-over : ext-glue == mv-diff
             [ (λ W → fst W → fst (⊙Susp (X ⊙∨ Y))) ↓ ⊙path ]
  ext-over = ↓-cst2-in _ _ $ ! (λ= fn-lemma) ◃ domain-over-equiv _ _
    where
    fn-lemma : ∀ κ → mv-diff (into κ) == ext-glue κ
    fn-lemma = CofPushoutSection.elim reglue
      (λ _ → unit) (λ _ → idp)
      idp
      (Pushout-elim
        (λ x → merid _ (winl x))
        (λ y → merid _ (winr y))
        (↓-='-from-square ∘ λ z →
          (ap-∘ mv-diff ext-glue (glue z)
           ∙ ap (ap mv-diff) (ExtGlue.glue-β z)
           ∙ MVDiff.glue-β z)
          ∙v⊡ (lt-square (merid _ (winl (f z)))
               ⊡h rt-square (merid _ (winr (g z))))
          ⊡v∙ ! (ap-cst (south _) (glue z))))
      (↓-='-from-square ∘ λ x →
        (ap-∘ mv-diff into (cfglue _ (winl x))
         ∙ ap (ap mv-diff) (Into.glue-β (winl x)))
        ∙v⊡ connection
        ⊡v∙ ! (ExtGlue.glue-β (winl x)))
      (↓-='-from-square ∘ λ y →
        (ap-∘ mv-diff into (cfglue _ (winr y))
         ∙ ap (ap mv-diff) (Into.glue-β (winr y))
         ∙ MVDiff.glue-β (snd Z)
         ∙ ap (λ w → merid _ w ∙ ! (merid _ (winr (g (snd Z))))) wglue
         ∙ !-inv-r (merid _ (winr (g (snd Z)))))
        ∙v⊡ connection
        ⊡v∙ ! (ExtGlue.glue-β (winr y)))

{- Main results -}
module MayerVietoris (ps : ⊙Span {i} {i} {i}) where

  private
    record Results (ps : ⊙Span {i} {i} {i}) : Type (lsucc i) where
      open ⊙Span ps
      open MayerVietorisFunctions ps public
      field
        eq : Cofiber reglue ≃ Suspension (fst Z)
        ⊙eq : ⊙Cof ⊙reglue ⊙≃ ⊙Susp Z
        path : Cofiber reglue == Suspension (fst Z)
        ⊙path : ⊙Cof ⊙reglue == ⊙Susp Z
        cfcod-over : cfcod reglue == ext-glue
                     [ (λ W → fst (⊙Pushout ps) → fst W) ↓ ⊙path ]
        ext-over : ext-glue == mv-diff
                   [ (λ W → fst W → fst (⊙Susp (X ⊙∨ Y))) ↓ ⊙path ]

    results : Results ps
    results = ⊙pushout-J Results base-results ps
      where
      base-results : ∀ {A} {B} Z (f : fst Z → A) (g : fst Z → B) →
        Results (⊙span _ _ Z (f , idp) (g , idp))
      base-results Z f g = record {
        eq = eq;
        ⊙eq = ⊙eq;
        path = path;
        ⊙path = ⊙path;
        cfcod-over = cfcod-over;
        ext-over = ext-over}
        where open MayerVietorisBase Z f g

  open Results results public

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module hnf-tests where

open import bool
open import list
open import nat
open import product
open import string

open import cedille-types
open import conversion
open import ctxt
open import is-free
open import rename
open import subst
open import syntax-util
open import to-string

S : term
S = mlam "n" (mlam "s" (mlam "z" (mapp (mvar "s") (mapp (mapp (mvar "n") (mvar "s")) (mvar "z")))))

plus : term
plus = mlam "n" (mlam "m" (mapp (mapp (mvar "n") S) (mvar "m")))

run : term → term
run t = hnf new-ctxt unfold-head t

show : term → string
show t = term-to-string t

s2 = show (run (mapp S (mvar "z")))

-- λ s . (λ x . λ s . x λ s' . f s' s) s

t1 = mlam "s" (mapp (mlam "x" (mlam "s" (mapp (mvar "x") (mlam "s'" (mapp (mapp (mvar "f") (mvar "s'")) (mvar "s")))))) (mvar "s"))

s1 = show (run t1)

Γ = ctxt-var-decl "s" new-ctxt

q = show (subst-term Γ (mvar "s") "x" (mlam "s" (mapp (mvar "x") (mlam "s'" (mapp (mapp (mvar "f") (mvar "s'")) (mvar "s"))))))

r = show (subst-term Γ (mvar "s") "x" (mlam "s" (mlam "s'" (mapp (mapp (mvar "f") (mvar "s'")) (mvar "s")))))

aa = rename-var-if Γ empty-renamectxt "s" (mvar "s")

Γ' = ctxt-var-decl "s'" Γ
ρ = renamectxt-insert empty-renamectxt "s" "s'"

bb = show (substh-term Γ' ρ (mvar "s") "x" (mlam "s'" (mapp (mapp (mvar "f") (mvar "s'")) (mvar "s"))))

cc = rename-var-if Γ' ρ "s'" (mvar "s")

try-pull-lift-types : type → type → type
try-pull-lift-types tp1 tp2 with decompose-tpapps tp1 | decompose-tpapps (hnf new-ctxt unfold-head tp2)
try-pull-lift-types tp1 tp2 | Lft _ _ X t l , args1 | Lft _ _ X' t' l' , args2 =
   if conv-tty* new-ctxt args1 args2 then
      try-pull-term-in t l (length args1) [] []
   else
      TpApp tp1 tp2
   where try-pull-term-in : term → liftingType → ℕ → 𝕃 var → 𝕃 liftingType → type
         try-pull-term-in t (LiftParens _ l _) n vars ltps = try-pull-term-in t l n vars ltps
         try-pull-term-in t (LiftArrow _ l) 0 vars ltps =
           recompose-tpapps
             (Lft posinfo-gen posinfo-gen X (Lam* vars (hnf Γ no-unfolding (App t NotErased (App* t' (map mvar vars)))))
               (LiftArrow* ltps l) , args1)
         try-pull-term-in (Lam _ _ _ x _ t) (LiftArrow l1 l2) (suc n) vars ltps =
           try-pull-term-in t l2 n (x :: vars) (l1 :: ltps)
         try-pull-term-in t (LiftArrow l1 l2) (suc n) vars ltps =
           let x = fresh-var "x" (ctxt-binds-var Γ) empty-renamectxt in
             try-pull-term-in (App t NotErased (mvar x)) l2 n (x :: vars) (l1 :: ltps)
         try-pull-term-in t l n vars ltps = TpApp tp1 tp2

try-pull-lift-types tp1 tp2 | h , a | h' , a' = TpApp tp1 tp2

lta = (TpApp (Lft posinfo-gen posinfo-gen "X" (mvar "f")
               (LiftArrow (LiftStar posinfo-gen) (LiftArrow (LiftStar posinfo-gen) (LiftStar posinfo-gen))))
             (mtpvar "doit"))
ltb = (TpApp (Lft posinfo-gen posinfo-gen "X" (mvar "t") (LiftStar posinfo-gen)) (mtpvar "doit"))

lt = try-pull-lift-types lta ltb

lts = to-string lt

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

open import Categories.Bicategory

-- The two Hom 2-functors from (op C) and C to Cats.

module Categories.Pseudofunctor.Hom {o ℓ e t} (C : Bicategory o ℓ e t) where

open import Data.Product using (_,_)

import Categories.Bicategory.Extras as BicategoryExtras
open import Categories.Bicategory.Opposite using (op)
open import Categories.Bicategory.Instance.Cats using (Cats)
import Categories.Category.Construction.Core as Core
open import Categories.Functor.Bifunctor.Properties
open import Categories.Pseudofunctor using (Pseudofunctor)
import Categories.Morphism.Reasoning as MorphismReasoning
import Categories.Morphism as Morphism
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (niHelper)

open BicategoryExtras C
open Shorthands
open hom.HomReasoning
private
  module MR {A} {B} where
    open Core.Shorthands (hom A B) public
    open MorphismReasoning (hom A B) public
  open MR

-- The left and right hom-pseudofunctors for a given bicategory.
--
-- Note that these are *not* simply partial applications of a single
-- *binary* hom-pseudofunctor because pre-/post-composition with
-- identity 1-cells in bicategories is only weakly unitary, i.e. the
-- partial applications Hom[ id , f ] and Hom[ g , id ] would send a
-- 1-cell h to (id ∘ h ∘ f) and (g ∘ h ∘ id) which are isomorphic but
-- not strictly equal to (h ∘ f) and (g ∘ h).

-- The right hom-pseudofunctor (post-composition)

Hom[_,-] : Obj → Pseudofunctor C (Cats o ℓ e)
Hom[ A ,-] = record
  { P₀ = hom A
  ; P₁ = [-]⊚-
  -- A curried version of the left unitor
  ; P-identity  = niHelper (record
    { η         = λ _ → ntHelper (record
      { η       = λ f → unitˡ.⇐.η (_ , f)
      ; commute = λ _ → ⟺ ▷-∘ᵥ-λ⇐
      })
    ; η⁻¹       = λ _ → ntHelper (record
      { η       = λ f → unitˡ.⇒.η (_ , f)
      ; commute = λ _ → λ⇒-∘ᵥ-▷
      })
    ; commute = λ _ → unitˡ.⇐.commute (_ , hom.id)
    ; iso     = λ _ → record
      { isoˡ  = λ {f} → unitˡ.iso.isoʳ (_ , f)
      ; isoʳ  = λ {f} → unitˡ.iso.isoˡ (_ , f)
      }
    })
  -- A curried version of the associator
  ; P-homomorphism = niHelper (record
    { η         = λ{ (f , g) → ntHelper (record
      { η       = λ h → ⊚-assoc.⇐.η ((f , g) , h)
      ; commute = λ _ → α⇐-▷-∘₁
      }) }
    ; η⁻¹       = λ{ (f , g) → ntHelper (record
      { η       = λ h → ⊚-assoc.⇒.η ((f , g) , h)
      ; commute = λ _ → α⇒-▷-∘₁
      }) }
    ; commute = λ{ {f₁ , g₁} {f₂ , g₂} (β , γ) {h} → begin
          α⇐ ∘ᵥ f₂ ▷ (γ ◁ h) ∘ᵥ β ◁ (g₁ ⊚₀ h)
        ≈˘⟨ refl⟩∘⟨ [ ⊚ ]-decompose₂ ⟩
          α⇐ ∘ᵥ β ⊚₁ (γ ◁ h)
        ≈⟨ ⊚-assoc.⇐.commute ((β , γ) , id₂) ⟩
          (β ⊚₁ γ) ◁ h ∘ᵥ α⇐
        ∎ }
    ; iso    = λ{ (f , g) → record
      { isoˡ = λ {h} → ⊚-assoc.iso.isoʳ ((f , g) , h)
      ; isoʳ = λ {h} → ⊚-assoc.iso.isoˡ ((f , g) , h) }
      }
    })
  ; unitaryˡ = λ {_ _ f g} → begin
      λ⇒ ◁ g ∘ᵥ α⇐ ∘ᵥ (id₂ ◁ (f ⊚₀ g)) ∘ᵥ λ⇐
                                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊚.identity ⟩∘⟨refl ⟩
      λ⇒ ◁ g ∘ᵥ α⇐ ∘ᵥ id₂ ∘ᵥ λ⇐  ≈⟨ unitorˡ-coherence ⟩∘⟨ refl⟩∘⟨ hom.identityˡ ⟩
      (λ⇒ ∘ᵥ α⇒) ∘ᵥ α⇐ ∘ᵥ λ⇐     ≈⟨ isoʳ (unitorˡ ∘ᵢ associator) ⟩
      id₂                        ∎
  ; unitaryʳ = λ {_ _ f g} → begin
        ρ⇒ ◁ g ∘ᵥ α⇐ ∘ᵥ f ▷ λ⇐ ∘ᵥ id₂
      ≈⟨ pushʳ (refl⟩∘⟨ hom.identityʳ) ⟩
        (ρ⇒ ◁ g ∘ᵥ α⇐) ∘ᵥ f ▷ λ⇐
      ≈˘⟨ switch-tofromʳ (associator ⁻¹) triangle ⟩∘⟨refl ⟩
        f ▷ λ⇒ ∘ᵥ f ▷ λ⇐
      ≈⟨ isoʳ (f ▷ᵢ unitorˡ) ⟩
        id₂
      ∎
  ; assoc = λ {_ _ _ _ f g h e} → begin
        α⇒ ◁ e ∘ᵥ α⇐ ∘ᵥ (id₂ ⊚₁ id₂) ∘ᵥ α⇐
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊚.identity ⟩∘⟨refl ⟩
        α⇒ ◁ e ∘ᵥ α⇐ ∘ᵥ id₂ ∘ᵥ α⇐
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ hom.identityˡ ⟩
        α⇒ ◁ e ∘ᵥ α⇐ ∘ᵥ α⇐
      ≈˘⟨ switch-fromtoˡ ((associator ◁ᵢ e) ⁻¹)
                         (hom.sym-assoc ○ pentagon-inv) ⟩
        α⇐ ∘ᵥ h ▷ α⇐
      ≈˘⟨ pushʳ hom.identityʳ ○ hom.identityʳ  ⟩
        α⇐ ∘ᵥ (h ▷ α⇐ ∘ᵥ id₂) ∘ᵥ id₂
      ∎
  }

-- The left hom-pseudofunctor (pre-composition)

Hom[-,_] : Obj → Pseudofunctor (op C) (Cats o ℓ e)
Hom[-, B ] = record
  { P₀ = λ A → hom A B
  ; P₁ = -⊚[-]
  -- A curried version of the right unitor
  ; P-identity  = niHelper (record
    { η         = λ _ → ntHelper (record
      { η       = λ f → unitʳ.⇐.η (f , _)
      ; commute = λ _ → ⟺ ◁-∘ᵥ-ρ⇐
      })
    ; η⁻¹       = λ _ → ntHelper (record
      { η       = λ f → unitʳ.⇒.η (f , _)
      ; commute = λ _ → ρ⇒-∘ᵥ-◁
      })
    ; commute = λ _ → unitʳ.⇐.commute (hom.id , _)
    ; iso     = λ _ → record
      { isoˡ  = λ {f} → unitʳ.iso.isoʳ (f , _)
      ; isoʳ  = λ {f} → unitʳ.iso.isoˡ (f , _)
      }
    })
  -- A curried version of the associator
  ; P-homomorphism = niHelper (record
    { η         = λ{ (f , g) → ntHelper (record
      { η       = λ h → ⊚-assoc.⇒.η ((h , g) , f)
      ; commute = λ _ → α⇒-◁-∘₁
      }) }
    ; η⁻¹       = λ{ (f , g) → ntHelper (record
      { η       = λ h → ⊚-assoc.⇐.η ((h , g) , f)
      ; commute = λ _ → α⇐-◁-∘₁
      }) }
    ; commute = λ{ {f₁ , g₁} {f₂ , g₂} (β , γ) {h} → begin
          α⇒ ∘ᵥ (h ▷ γ) ◁ f₂ ∘ᵥ (h ⊚₀ g₁) ▷ β
        ≈˘⟨ refl⟩∘⟨ [ ⊚ ]-decompose₁ ⟩
          α⇒ ∘ᵥ (h ▷ γ) ⊚₁ β
        ≈⟨ ⊚-assoc.⇒.commute ((id₂ , γ) , β) ⟩
          h ▷ (γ ⊚₁ β) ∘ᵥ α⇒
        ∎ }
    ; iso    = λ{ (f , g) → record
      { isoˡ = λ {h} → ⊚-assoc.iso.isoˡ ((h , g) , f)
      ; isoʳ = λ {h} → ⊚-assoc.iso.isoʳ ((h , g) , f) }
      }
    })
  ; unitaryˡ = λ {_ _ f g} → begin
      g ▷ ρ⇒ ∘ᵥ α⇒ ∘ᵥ ((g ⊚₀ f) ▷ id₂) ∘ᵥ ρ⇐
                                   ≈⟨ pushʳ (refl⟩∘⟨ ⊚.identity ⟩∘⟨refl) ⟩
      (g ▷ ρ⇒ ∘ᵥ α⇒) ∘ᵥ id₂ ∘ᵥ ρ⇐  ≈⟨ ⟺ unitorʳ-coherence ⟩∘⟨ hom.identityˡ ⟩
      ρ⇒ ∘ᵥ ρ⇐                     ≈⟨ isoʳ unitorʳ ⟩
      id₂                          ∎
  ; unitaryʳ = λ {_ _ f g} → begin
        g ▷ λ⇒ ∘ᵥ α⇒ ∘ᵥ ρ⇐ ◁ f ∘ᵥ id₂
      ≈⟨ pushʳ (refl⟩∘⟨ hom.identityʳ) ⟩
        (g ▷ λ⇒ ∘ᵥ α⇒) ∘ᵥ ρ⇐ ◁ f
      ≈⟨ triangle ⟩∘⟨refl ⟩
        ρ⇒ ◁ f ∘ᵥ ρ⇐ ◁ f
      ≈⟨ isoʳ (unitorʳ ◁ᵢ f) ⟩
        id₂
      ∎
  ; assoc = λ {_ _ _ _ f g h e} → begin
        e ▷ α⇐ ∘ᵥ α⇒ ∘ᵥ (id₂ ⊚₁ id₂) ∘ᵥ α⇒
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊚.identity ⟩∘⟨refl ⟩
        e ▷ α⇐ ∘ᵥ α⇒ ∘ᵥ id₂ ∘ᵥ α⇒
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ hom.identityˡ ⟩
        e ▷ α⇐ ∘ᵥ α⇒ ∘ᵥ α⇒
      ≈˘⟨ switch-fromtoˡ (e ▷ᵢ associator) pentagon ⟩
        α⇒ ∘ᵥ α⇒ ◁ h
      ≈˘⟨ pushʳ hom.identityʳ ○ hom.identityʳ  ⟩
        α⇒ ∘ᵥ (α⇒ ◁ h ∘ᵥ id₂) ∘ᵥ id₂
      ∎
  }

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
------------------------------------------------------------------------
-- A counterexample: The trace of stack sizes produced by the virtual
-- machine is not necessarily bisimilar to that produced by the
-- instrumented interpreter
------------------------------------------------------------------------

module Lambda.Interpreter.Stack-sizes.Counterexample where

open import Equality.Propositional as E using (_≡_)
open import Prelude
open import Prelude.Size

open import Colist E.equality-with-J
open import Function-universe E.equality-with-J
open import Vec.Data E.equality-with-J

import Lambda.Compiler
import Lambda.Interpreter.Stack-sizes
import Lambda.Virtual-machine
import Lambda.Virtual-machine.Instructions

-- This module uses a name type with two inhabitants.

open import Lambda.Syntax Bool

open Closure Tm

-- Two unary functions.

def : Bool → Tm 1
def true  = call false (con true)
def false = con true

-- The instrumented interpreter, compiler and virtual machine are
-- instantiated with this definition.

module I = Lambda.Interpreter.Stack-sizes def
open Lambda.Compiler def
open Lambda.Virtual-machine.Instructions Bool
open module VM = Lambda.Virtual-machine comp-name

-- A top-level term to get things going. The important property of
-- this term is that when it is compiled and the resulting code is
-- executed on the virtual machine, then one tail call is made to a
-- function that terminates successfully.

go : Tm 0
go = call true (con true)

-- The trace of stack sizes produced by the virtual machine is not
-- necessarily bisimilar to that produced by the instrumented
-- interpreter.

stack-sizes-not-bisimilar :
  ¬ [ ∞ ] VM.stack-sizes ⟨ comp₀ go , [] , [] ⟩ ∼ I.stack-sizes go
stack-sizes-not-bisimilar =
  [ ∞ ] VM.stack-sizes ⟨ comp₀ go , [] , [] ⟩ ∼ I.stack-sizes go  ↝⟨ take-cong 8 ⟩

  take 8 (VM.stack-sizes ⟨ comp₀ go , [] , [] ⟩) ≡
  take 8 (I.stack-sizes go)                                       ↔⟨⟩

  0 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ 2 ∷ 1 ∷ [] ≡
  0 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ 2 ∷ 2 ∷ 1 ∷ []                              ↝⟨ (λ ()) ⟩□

  ⊥                                                               □

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


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

module Categories.2-Category where

open import Level

open import Categories.Category.Monoidal.Instance.StrictCats using (module Product)
open import Categories.Enriched.Category using (Category)

2-Category : (o ℓ e t : Level) → Set (suc (o ⊔ ℓ ⊔ e ⊔ t))
2-Category o ℓ e t = Category (Product.Cats-Monoidal {o} {ℓ} {e}) t

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- {-# OPTIONS -v tc.with:40 #-}

module RewriteAndWhere where

open import Common.Equality

data ℕ : Set where
  zero : ℕ

-- good : (a b : ℕ) → a ≡ b → b ≡ a
-- good a b eq with a | eq
-- ... | .b | refl = foo
--   where
--     foo : b ≡ b
--     foo = refl

mutual
  aux : (a b : ℕ)(w : ℕ) → w ≡ b → b ≡ w
  aux a b .b refl = foo
    where
     foo : b ≡ b
     foo = refl

  good₂ : (a b : ℕ) → a ≡ b → b ≡ a
  good₂ a b eq = aux a b a eq

bad : (a b : ℕ) → a ≡ b → b ≡ a
bad a b eq rewrite eq = foo
  where
    foo : b ≡ b
    foo = refl
    -- Andreas, 2014-11-06: this rewrite is trying to touch
    -- variable b bound in pattern of parent function, which is
    -- illegal.
    --
    -- foo rewrite sym eq = bar
    --   where
    --     bar : a ≡ a
    --     bar = refl

-- Andreas, 2015-11-18 added test during exploration of issue 1692.
-- Ulf, 2016-02-25 after fix to #745 this no longer works.
-- test : (a b : ℕ) → a ≡ b → b ≡ a
-- test a b eq with a | eq
-- test a b eq | .b | refl = eq

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --type-in-type #-}  -- yes, I will let you cheat in this exercise
{-# OPTIONS --allow-unsolved-metas #-}  -- allows import, unfinished

------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CS410 2017/18 Exercise 3  WINDOWS AND OTHER STORIES (worth 25%)
------------------------------------------------------------------------------
------------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Dependencies
------------------------------------------------------------------------------

open import CS410-Prelude
open import CS410-Categories
open import Ex2

------------------------------------------------------------------------------
--  PART I:  Splittings
------------------------------------------------------------------------------

-- The type    ls <[ ms ]> rs
-- is similar to that found in Lec2.agda, but it works on lists, not numbers.
-- It provides the evidence that a list ms can be split into a left sublist ls
-- and a right sublist rs. In effect, it's a vector of bits that say which
-- elements of ms go left and which go right.

data _<[_]>_ {X : Set} : List X -> List X -> List X -> Set where
  sz : [] <[ [] ]> []
  sl : forall {l ls ms rs} -> ls <[ ms ]> rs -> (l ,- ls) <[ l ,- ms ]> rs
  sr : forall {r ls ms rs} -> ls <[ ms ]> rs -> ls <[ r ,- ms ]> (r ,- rs)

--??--3.1---------------------------------------------------------------------

-- Adapt _>[_]<_ from Lec2 to work for All. Given a P for each element of
-- ls and rs, riffle them together to get Ps for all the ms.

_>[_]<_ : {X : Set}{ls ms rs : List X} -> {P : X -> Set} ->
          All P ls -> ls <[ ms ]> rs -> All P rs ->
          All P ms
pl >[ s ]< pr = {!!}

-- Now, buikd the view that shows riffling can be inverted, using a splitting
-- as the instructions to discover how to split an All in two.

data IsRiffle {X : Set}{ls ms rs : List X}(s : ls <[ ms ]> rs){P : X -> Set}
  : All P ms -> Set where
  mkRiffle : (pl : All P ls)(pr : All P rs) -> IsRiffle s (pl >[ s ]< pr)

isRiffle : {X : Set}{ls ms rs : List X}(s : ls <[ ms ]> rs)
           {P : X -> Set}(pm : All P ms) -> IsRiffle s pm
isRiffle s pm = {!!}

--??--------------------------------------------------------------------------

--??--3.2---------------------------------------------------------------------

-- Construct the "all on the right" splitting.

srs : forall {X : Set}{xs : List X} -> [] <[ xs ]> xs
srs = {!!}

-- Construct a view to show that any "none on the left" splitting is
-- "all on the right". Come up with the type yourself.

-- Construct the splitting that corresponds to concatenation.

slrs : forall {X : Set}(xs ys : List X) -> xs <[ xs +L ys ]> ys
slrs xs ys = {!!}

--??--------------------------------------------------------------------------

--??--3.3---------------------------------------------------------------------

-- Invent other useful operations which transform splittings.
-- You will need some to do later parts of the exercise, so maybe
-- wait until you see what you need.

-- I expect you will need at least something that takes a pair of splittings
-- that make a tree, like
--
--                  ms
--               <[    ]>
--            ls          rs
--                     <[    ]>
--                 lrs          rrs
--
-- and compute a "rotated" pair of splittings like
--
--                  ms
--               <[    ]>
--            ??          rrs
--         <[    ]>
--      ls          lrs

-- HINT: Sg is your friend

-- You'll probably need some other stuff, too.

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
--  PART II:  Permutations
------------------------------------------------------------------------------

-- When is one list a permutation of another?

data _~_ {X : Set} : List X -> List X -> Set where

  -- [] is a permutation of []
  []   : [] ~ []

  -- if xs ~ ys, then (x ,- xs) is a permutation of any list made by
  -- shoving x somewhere into ys
  _,-_ : forall {x xs ys' ys} ->
           (x ,- []) <[ ys' ]> ys ->
           xs ~ ys ->
           (x ,- xs) ~ ys'

--??--3.4---------------------------------------------------------------------

-- Show that every list is a permutation of itself.

reflP : {X : Set}{xs : List X} -> xs ~ xs
reflP = {!!}

--??--------------------------------------------------------------------------

--??--3.5---------------------------------------------------------------------

-- Construct an "unbiased" insertion operator which lets you grow a
-- permutation by inserting a new element anywhere, left and right

insP : forall {X : Set}{z : X}{xs xs' ys ys'} ->
         (z ,- []) <[ xs' ]> xs ->
         (z ,- []) <[ ys' ]> ys ->
         xs ~ ys -> xs' ~ ys'
insP l r p = {!!}

-- Now show that, given a permutation, and any element on the left,
-- you can find out where it ended up on the right, and why the
-- remaining elements form a permutation.

findLonR : forall {X : Set}{z : X}{xs xs' ys'} ->
                  (z ,- []) <[ xs' ]> xs ->
                  xs' ~ ys' ->
                  {!!}
findLonR l p = {!!}

-- HINT: again, you may need Sg to give a sensible return type.

--??--------------------------------------------------------------------------

--??--3.6---------------------------------------------------------------------

-- Show that permutation is transitive.

transP : {X : Set}{xs ys zs : List X} -> xs ~ ys -> ys ~ zs -> xs ~ zs
transP p q = {!!}

-- HINT: you will need to define some useful operations on splittings to
-- get this to work.

-- HINT: this may help you figure out what you need for findLonR

-- For a small bonus, show that permutations are the morphisms of a
-- Category.

-- Show that permutation is symmetric.

symP : {X : Set}{xs ys : List X} -> xs ~ ys -> ys ~ xs
symP p = {!!}

-- A category where all morphisms are invertible is called a "groupoid".

--??--------------------------------------------------------------------------

--??--3.7---------------------------------------------------------------------

-- Make permutations act on All.

permute : {X : Set}{xs ys : List X} -> xs ~ ys ->
          {Q : X -> Set} -> All Q xs -> All Q ys

permute p qs = {!!}

--??--------------------------------------------------------------------------

-- MORE TO FOLLOW


text:
------------------------------------------------------------------------------
-- Totality properties for Forest
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Forest.TotalityI where

open import FOTC.Base
open import FOTC.Data.List
open import FOTC.Program.Mirror.Type

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

++-Forest : ∀ {xs ys} → Forest xs → Forest ys → Forest (xs ++ ys)
++-Forest {ys = ys} fnil Fys = subst Forest (sym (++-[] ys)) Fys
++-Forest {ys = ys} (fcons {x} {xs} Tx Fxs) Fys =
  subst Forest (sym (++-∷ x xs ys)) (fcons Tx (++-Forest Fxs Fys))

map-Forest : ∀ {xs} f → (∀ {x} → Tree x → Tree (f · x)) →
             Forest xs → Forest (map f xs)
map-Forest f fTree fnil = subst Forest (sym (map-[] f)) fnil
map-Forest f fTree (fcons {x} {xs} Tx Fxs) =
  subst Forest
        (sym (map-∷ f x xs))
        (fcons (fTree Tx) (map-Forest f fTree Fxs))

rev-Forest : ∀ {xs ys} → Forest xs → Forest ys → Forest (rev xs ys)
rev-Forest {ys = ys} fnil Fys = subst Forest (sym (rev-[] ys)) Fys
rev-Forest {ys = ys} (fcons {x} {xs} Tx Fxs) Fys =
  subst Forest (sym (rev-∷ x xs ys)) (rev-Forest Fxs (fcons Tx Fys))

reverse-Forest : ∀ {xs} → Forest xs → Forest (reverse xs)
reverse-Forest Fxs = rev-Forest Fxs fnil

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Oscar.Builtin.Objectevel where

open import Agda.Primitive public
  using ()
  renaming (Level to Ł̂; lzero to Ø̂; lsuc to ↑̂_; _⊔_ to _∙̂_)

infix 0 Ø_
Ø_ : ∀ 𝔬 → Set (↑̂ 𝔬)
Ø_ 𝔬 = Set 𝔬


text:
module DigitsInNames where

data 1D : Set where
  1d : 1D
  2d : 1D -> 1D


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between monoid-like structures
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

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

open import Algebra.Bundles
open import Algebra.Morphism.Structures
open import Relation.Binary.Core

module Algebra.Morphism.MonoidMonomorphism
  {a b ℓ₁ ℓ₂} {M₁ : RawMonoid a ℓ₁} {M₂ : RawMonoid b ℓ₂} {⟦_⟧}
  (isMonoidMonomorphism : IsMonoidMonomorphism M₁ M₂ ⟦_⟧)
  where

open IsMonoidMonomorphism isMonoidMonomorphism
open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁)
open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)

open import Algebra.Definitions
open import Algebra.Structures
open import Data.Product using (map)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

------------------------------------------------------------------------
-- Re-export all properties of magma monomorphisms

open import Algebra.Morphism.MagmaMonomorphism
  isMagmaMonomorphism public

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

module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where

  open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
  open SetoidReasoning setoid

  identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_
  identityˡ idˡ x = injective (begin
    ⟦ ε₁ ∙ x ⟧      ≈⟨ homo ε₁ x ⟩
    ⟦ ε₁ ⟧ ◦ ⟦ x ⟧  ≈⟨ ◦-cong ε-homo refl ⟩
    ε₂ ◦ ⟦ x ⟧      ≈⟨ idˡ ⟦ x ⟧ ⟩
    ⟦ x ⟧           ∎)

  identityʳ : RightIdentity _≈₂_ ε₂ _◦_ → RightIdentity _≈₁_ ε₁ _∙_
  identityʳ idʳ x = injective (begin
    ⟦ x ∙ ε₁ ⟧      ≈⟨ homo x ε₁ ⟩
    ⟦ x ⟧ ◦ ⟦ ε₁ ⟧  ≈⟨ ◦-cong refl ε-homo ⟩
    ⟦ x ⟧ ◦ ε₂      ≈⟨ idʳ ⟦ x ⟧ ⟩
    ⟦ x ⟧           ∎)

  identity : Identity _≈₂_ ε₂ _◦_ → Identity _≈₁_ ε₁ _∙_
  identity = map identityˡ identityʳ

  zeroˡ : LeftZero _≈₂_ ε₂ _◦_ → LeftZero _≈₁_ ε₁ _∙_
  zeroˡ zeˡ x = injective (begin
    ⟦ ε₁ ∙ x ⟧     ≈⟨  homo ε₁ x ⟩
    ⟦ ε₁ ⟧ ◦ ⟦ x ⟧ ≈⟨  ◦-cong ε-homo refl ⟩
    ε₂   ◦ ⟦ x ⟧   ≈⟨  zeˡ ⟦ x ⟧ ⟩
    ε₂             ≈˘⟨ ε-homo ⟩
    ⟦ ε₁ ⟧         ∎)

  zeroʳ : RightZero _≈₂_ ε₂ _◦_ → RightZero _≈₁_ ε₁ _∙_
  zeroʳ zeʳ x = injective (begin
    ⟦ x ∙ ε₁ ⟧     ≈⟨  homo x ε₁ ⟩
    ⟦ x ⟧ ◦ ⟦ ε₁ ⟧ ≈⟨  ◦-cong refl ε-homo ⟩
    ⟦ x ⟧ ◦ ε₂     ≈⟨  zeʳ ⟦ x ⟧ ⟩
    ε₂             ≈˘⟨ ε-homo ⟩
    ⟦ ε₁ ⟧         ∎)

  zero : Zero _≈₂_ ε₂ _◦_ → Zero _≈₁_ ε₁ _∙_
  zero = map zeroˡ zeroʳ

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

isMonoid : IsMonoid _≈₂_ _◦_ ε₂ → IsMonoid _≈₁_ _∙_ ε₁
isMonoid isMonoid = record
  { isSemigroup = isSemigroup M.isSemigroup
  ; identity    = identity    M.isMagma M.identity
  } where module M = IsMonoid isMonoid

isCommutativeMonoid : IsCommutativeMonoid _≈₂_ _◦_ ε₂ →
                      IsCommutativeMonoid _≈₁_ _∙_ ε₁
isCommutativeMonoid isCommMonoid = record
  { isMonoid = isMonoid C.isMonoid
  ; comm     = comm     C.isMagma C.comm
  } where module C = IsCommutativeMonoid isCommMonoid


text:
------------------------------------------------------------------------------
-- Testing the --without-K flag
------------------------------------------------------------------------------

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

module WithoutK where

-- The following code fails with the --without-K flag.

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

K : {A : Set} (P : {x : A} → x ≡ x → Set) →
    (∀ x → P (refl x)) →
    ∀ {x} (x≡x : x ≡ x) → P x≡x
K P p (refl x) = p x


text:
open import Level
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Fin
open import Data.Sum
open import Data.Maybe
open import Data.Product
open import Data.Vec using (Vec; _∷_; [])
import Data.Vec as Vec
open import Data.List
open import Relation.Binary.PropositionalEquality

--------------- lenses

Lens : Set → Set → Set
Lens A B = A → B × (B → A)

idₗ : {A : Set} → Lens A A
idₗ = λ z → z , λ x → x

_∘ₗ_ : {A B C : Set} → Lens A B → Lens B C → Lens A C
l ∘ₗ k = λ a → let (l₁ , l₂) = l a; (k₁ , k₂) = k l₁ in k₁ , λ x → l₂ (k₂ x)

infixl 9 _∘ₗ_

--- composition laws

_≡ₗ_ : {A B : Set} (k l : Lens A B) → Set
_≡ₗ_ {A} {B} k l = (a : A) → let (k₁ , k₂) = k a; (l₁ , l₂) = l a in k₁ ≡ l₁ × ((b : B) → k₂ b ≡ l₂ b)

infix 4 _≡ₗ_

id-left : {A B : Set} (k : Lens A B) → idₗ ∘ₗ k ≡ₗ k
id-left k a = refl , λ b → refl

id-right : {A B : Set} (k : Lens A B) → k ≡ₗ idₗ ∘ₗ k
id-right k a = refl , λ b → refl

comp-assoc : {A B C D : Set} (k : Lens A B) (l : Lens B C) (m : Lens C D) → k ∘ₗ (l ∘ₗ m) ≡ₗ (k ∘ₗ l) ∘ₗ m
comp-assoc k l m a = refl , λ b → refl

--------------- heterogeneous lists

TList : Set₁
TList = List Set

data HList : TList → Set where
  [] : HList []
  _∷_ : ∀ {t : Set} {ts : TList} → (v : t) → HList ts → HList (t ∷ ts)

--- operations

_+++_ : ∀ {ts xs : TList} → HList ts → HList xs → HList (ts ++ xs)
[] +++ y = y
(v ∷ x) +++ y = v ∷ (x +++ y)

splitH : ∀ {ts xs : TList} → HList (ts ++ xs) → HList ts × HList xs
splitH {ts = []} xs₁ = [] , xs₁
splitH {ts = x ∷ ts} (v ∷ xs₁) = let (r₁ , r₂) = splitH {ts = ts} xs₁ in v ∷ r₁ , r₂

---------------- auxiliary stuff

TList′ : ℕ → Set₁
TList′ = Vec Set

data HList′ : {n : ℕ} → TList′ n → Set where
  [] : HList′ []
  _∷_ : ∀ {n} {t : Set} {ts : TList′ n} → (v : t) → HList′ ts → HList′ (t ∷ ts)

pattern ex a = ._ , a

toVec : ∀ {ℓ} {A : Set ℓ} (as : List A) → Σ ℕ λ n → (n ≡ length as) × Vec A n
toVec [] = 0 , refl , []
toVec (x ∷ as) with toVec as
toVec (x ∷ as) | ex (refl , as′) = _ , refl , x ∷ as′

toVec′ : ∀ {ts : TList} → HList ts → let (_ , _ , ts′) = toVec ts in HList′ ts′ × (HList′ ts′ → HList ts)
toVec′ {[]} [] = [] , (λ _ → [])
toVec′ {x ∷ ts} (v ∷ xs) with toVec ts | toVec′ xs
toVec′ {x ∷ ts} (v ∷ xs) | ex (refl , _) | xs′ , f = v ∷ xs′ , λ { (v₁ ∷ x₁) → v₁ ∷ f x₁ }

----------

lookup : (ts : TList) → Fin (length ts) → Set
lookup x i with toVec x
lookup x i | ex (refl , v) = Vec.lookup i v

---------------------------------------------- signals

Signal : ∀ {ℓ} → TList → Set ℓ → Set ℓ
Signal ts A = HList ts → A

widenSignal : ∀ {ts xs : TList} {A : Set} → Signal ts A → Signal (ts ++ xs) A
widenSignal s vs = s (proj₁ (splitH vs))

sig : ∀ {ts : TList} (i : Fin (length ts)) → Signal ts (lookup ts i)
sig {ts} i st with toVec ts | toVec′ st
sig i st | ex (refl , v) | z , _ = sig′ i z
  where
    sig′ : ∀ {n} {ts : Vec Set n} (i : Fin n) → HList′ ts → Vec.lookup i ts
    sig′ zero (v ∷ x) = v
    sig′ (suc i) (v ∷ x) = sig′ i x

join : ∀ {ts : TList} {A : Set} → Signal ts (Signal ts A) → Signal ts A
join s vs = s vs vs

ret : ∀ {ts : TList} {A : Set} → A → Signal ts A
ret a _ = a

-- TODO: ret + join  monad laws

------------------------------------ references

Ref : TList → Set → Set
Ref ts = Lens (HList ts)

widenRef : {ts xs : TList} {A : Set} → Ref ts A → Ref (ts ++ xs) A
widenRef r vs = let (vs₁ , vs₂) = splitH vs; (r₁ , r₂) = r vs₁ in r₁ , λ x → r₂ x +++ vs₂

ref : {ts : TList} (i : Fin (length ts)) → Ref ts (lookup ts i)
ref {ts} i st with toVec ts | toVec′ st
ref {ts} i st | ex (refl , v) | z , tr = let (r₁ , r₂) = ref′ i z in r₁ , λ x → tr (r₂ x)
  where
    ref′ : ∀ {n} {ts : TList′ n} (i : Fin n) → Lens (HList′ ts) (Vec.lookup i ts)
    ref′ zero (v ∷ x) = v , λ v → v ∷ x
    ref′ (suc i) (v ∷ x) with ref′ i x
    ref′ (suc i) (v ∷ x) | z , f = z , λ z → v ∷ f z

unitRef : ∀ {ts : TList} → Ref ts ⊤
unitRef st = tt , λ tt → st

joinRef : ∀ {ts : TList} {A : Set} → Signal ts (Ref ts A) → Ref ts A
joinRef s st = s st st

lensMap : ∀ {ts : TList} {A B : Set} → Ref ts A → Lens A B → Ref ts B
lensMap = _∘ₗ_

readRef : ∀ {ts : TList} {A : Set} → Ref ts A → Signal ts A
readRef r st = proj₁ (r st)

---------------------------------- programs

open import Coinduction

Event : TList → Set
Event ts = Σ (Fin (length ts)) λ i → lookup ts i

mutual
  data R (ts : TList) : Set₁ where
    step : HList ts → (Event ts → ∞ (W ts)) → R ts

  W : TList → Set₁
  W ts = Σ TList λ vs → R (ts ++ vs)

Prog : Set₁
Prog = W []

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

Gen : TList → TList → Set → Set
Gen ts xs A = HList ts → A × HList (ts ++ xs)

Gen′ : TList → Set → Set₁
Gen′ ts A = HList ts → A × Σ TList λ xs → HList (ts ++ xs)

-- TODO: widenGen

data Trigger (ts : TList) (A : Set) : Set₁ where
    extend : {B : Set} → Ref ts B → Lens A B → Trigger ts A
    stabilize : (A → A → Bool) → Signal ts A → Trigger ts A
    onChange : Signal ts (Gen′ ts A) → Trigger ts A

runTrigger : ∀ {ts : TList} {A : Set} → Trigger ts A → Gen′ ts A
runTrigger (extend x x₁) x₂ = {!!}
runTrigger (stabilize x x₁) x₂ = {!!}
runTrigger (onChange x) x₁ = {!!}

-- ...

max_stars_repo_name: divipp/lensref

max_issues_repo_name: silky/lensref

max_forks_repo_name: silky/lensref


text:
module Binding where

open import Agda.Primitive

data Freer {ℓ} (F : Set ℓ → Set (lsuc ℓ)) (A : Set (lsuc ℓ)) : Set (lsuc ℓ) where
  pure : A → Freer F A
  free : ∀ {a : Set ℓ} → (a → Freer F A) → F a → Freer F A


text:
{- LEMMAS FOR BOUNDING THEOREM WITH NEW COMPLEXITY LANGUAGE -}

open import Preliminaries
open import Source
open import Pilot
open import Translation-New

module Bounding-Lemmas-New where

  mutual
    valBound : ∀{τ} → (e : [] Source.|- τ) → val e → [] Pilot.|- ⟨⟨ τ ⟩⟩ → Set
    valBound .z z-isval E = z ≤s E
    valBound .(suc e) (suc-isval e v) E = Σ (λ E' → valBound e v E' × s E' ≤s E)
    valBound .(prod e1 e2) (pair-isval e1 e2 v1 v2) E = valBound e1 v1 (l-proj E) × valBound e2 v2 (r-proj E)
    valBound {τ1 ->s τ2} .(lam e) (lam-isval e) E = (v₁ : [] Source.|- τ1) (vv : val v₁)
                                                    (E1 : [] Pilot.|- ⟨⟨ τ1 ⟩⟩) →
                                                    valBound v₁ vv E1 →
                                                    expBound (Source.subst e (Source.q v₁)) (app E E1)
    valBound .unit unit-isval E = Unit
    valBound .(delay e) (delay-isval e) E = expBound e E
    valBound .nil nil-isval E = nil ≤s E
    valBound .(x ::s xs) (cons-isval x xs v v₁) E = Σ (λ E' → Σ (λ E'' → (valBound x v E' × valBound xs v₁ E'') × (E' ::c E'') ≤s E))
    valBound .true true-isval E = true ≤s E
    valBound .false false-isval E = false ≤s E

    expBound : ∀{τ} → [] Source.|- τ → [] Pilot.|- || τ || → Set
    expBound {τ} e b = (v₁ : [] Source.|- τ) (vv : val v₁) (n : Cost) →
                         evals e v₁ n → interp-Cost n ≤s l-proj b × valBound v₁ vv (r-proj b)

  mutual
    weakeningExp : ∀{τ} → (e : [] Source.|- τ) → (E E' : [] Pilot.|- || τ ||) → expBound e E → E ≤s E' → expBound e E'
    weakeningExp e c1 c2 d c1≤c2 e' ve' n i = trans-s (fst (d e' ve' n i)) (cong-lproj c1≤c2) ,
                                                      weakeningVal e' ve' (r-proj c1) (r-proj c2) (snd (d e' ve' n i)) (cong-rproj c1≤c2)

    weakeningVal : ∀{τ} → (v : [] Source.|- τ) → (vv : val v) → (E E' : [] Pilot.|- ⟨⟨ τ ⟩⟩) → valBound v vv E → E ≤s E' → valBound v vv E'
    weakeningVal {unit} unit unit-isval E E' vb e≤e' = <>
    weakeningVal {nat} .z z-isval E E' vb e≤e' = vb trans e≤e'
    weakeningVal {nat} .(suc e) (suc-isval e vv) E E' (i , vbi , si≤se) e≤e' = i , (vbi , (trans-s si≤se e≤e'))
    weakeningVal {susp τ} .(delay e) (delay-isval e) E E' vb e≤e' v₁ vv n x = weakeningExp e _ E' vb e≤e' v₁ vv n x
    weakeningVal {τ ->s τ₁} .(lam e) (lam-isval e) E E' vb e≤e' v₁ vv c1 x v₂ vv₁ n x₁ = (λ a va a' vba b b' n₁ x₂ →
                                                                                fst (vb a va a' vba b b' n₁ x₂) trans cong-lproj (cong-app e≤e') ,
                                                                                weakeningVal b b' (r-proj (app E a')) (r-proj (app E' a'))
                                                                                (snd (vb a va a' vba b b' n₁ x₂)) (cong-rproj (cong-app e≤e')))
                                                                                v₁ vv c1 x v₂ vv₁ n x₁
    weakeningVal {τ ×s τ₁} .(prod e1 e2) (pair-isval e1 e2 vv1 vv2) E E' vb e≤e' =
                    weakeningVal e1 vv1 (l-proj E) (l-proj E') (fst vb) (cong-lproj e≤e') ,
                    weakeningVal e2 vv2 (r-proj E) (r-proj E') (snd vb) (cong-rproj e≤e')
    weakeningVal {list τ} .nil nil-isval E E' vb e≤e' = vb trans e≤e'
    weakeningVal {list τ} .(x ::s xs) (cons-isval x xs vv vv₁) E E' (h , t , (hvb , tvb) , steps) e≤e' = h , (t , ((hvb , tvb) , (steps trans e≤e')))
    weakeningVal {bool} .true true-isval E E' vb e≤e' = vb trans e≤e'
    weakeningVal {bool} .false false-isval E E' vb e≤e' = vb trans e≤e'

  weakeningExp' : ∀{τ} {e : [] Source.|- τ} {E E' : [] Pilot.|- || τ ||} → expBound e E → E ≤s E' → expBound e E'
  weakeningExp' eb e≤ = weakeningExp _ _ _ eb e≤

  weakeningVal' : ∀{τ} { v : [] Source.|- τ} (vv : val v) {E E' : [] Pilot.|- ⟨⟨ τ ⟩⟩}
                → valBound v vv E → E ≤s E' → valBound v vv E'
  weakeningVal' vv v e = weakeningVal _ vv _ _ v e

  substVal : ∀{Γ} → (Θ : Source.sctx [] Γ) → Set
  substVal {Γ} Θ = {τ : _} (x : τ Source.∈ Γ) → val (Θ x)

  extend-substVal : ∀ {Γ' τ} {Θ : Source.sctx [] Γ'} {e : [] Source.|- τ}
                  → substVal Θ
                  → val e
                  → substVal (Source.lem3' Θ e)
  extend-substVal sv vv i0 = vv
  extend-substVal sv vv (iS x) = sv x

  extend-substVal2 : ∀ {Γ' τ1 τ2} {Θ : Source.sctx [] Γ'} {e : [] Source.|- τ1} {e' : [] Source.|- τ2}
                   → substVal Θ
                   → val e → val e'
                   → substVal (Source.lem4' Θ e e')
  extend-substVal2 sv vv vv' i0 = vv
  extend-substVal2 sv vv vv' (iS i0) = vv'
  extend-substVal2 sv vv vv' (iS (iS x)) = sv x

  extend-substVal3 : ∀ {Γ' τ1 τ2 τ3} {Θ : Source.sctx [] Γ'} {e : [] Source.|- τ1} {e' : [] Source.|- τ2} {e'' : [] Source.|- τ3}
                   → substVal Θ
                   → val e → val e' → val e''
                   → substVal (Source.lem5' Θ e e' e'')
  extend-substVal3 sv vv vv' vv'' i0 = vv
  extend-substVal3 sv vv vv' vv'' (iS i0) = vv'
  extend-substVal3 sv vv vv' vv'' (iS (iS i0)) = vv''
  extend-substVal3 sv vv vv' vv'' (iS (iS (iS x))) = sv x

  substBound : ∀{Γ} → (Θ : Source.sctx [] Γ) → substVal Θ → (Θ' : Pilot.sctx [] ⟨⟨ Γ ⟩⟩c) → Set
  substBound {Γ} Θ vΘ Θ' = {τ : _} (x : τ Source.∈ Γ) → valBound (Θ x) (vΘ x) (Θ' (lookup x))

  extend-substBound : ∀{Γ τ} → {Θ : Source.sctx [] Γ} {vΘ : substVal Θ} {Θ' : Pilot.sctx [] ⟨⟨ Γ ⟩⟩c}
                    → {e : [] Source.|- τ} {ve : val e} {E : [] Pilot.|- ⟨⟨ τ ⟩⟩}
                    → substBound Θ vΘ Θ'
                    → valBound e ve E
                    → substBound (Source.lem3' Θ e) (extend-substVal vΘ ve) (Pilot.lem3' Θ' E)
  extend-substBound sb vb i0 = vb
  extend-substBound sb vb (iS x) = sb x

  extend-substBound2 : ∀{Γ τ1 τ2} → {Θ : Source.sctx [] Γ} {vΘ : substVal Θ} {Θ' : Pilot.sctx [] ⟨⟨ Γ ⟩⟩c}
                     → {e : [] Source.|- τ1} {ve : val e} {e' : [] Source.|- τ2} {ve' : val e'}
                       {E : [] Pilot.|- ⟨⟨ τ1 ⟩⟩} {E' : [] Pilot.|- ⟨⟨ τ2 ⟩⟩}
                     → substBound Θ vΘ Θ'
                     → valBound e ve E → valBound e' ve' E'
                     → substBound (Source.lem4' Θ e e') (extend-substVal2 vΘ ve ve') (Pilot.lem4' Θ' E E')
  extend-substBound2 sb vbE vbE' i0 = vbE
  extend-substBound2 sb vbE vbE' (iS i0) = vbE'
  extend-substBound2 sb vbE vbE' (iS (iS x)) = sb x

  extend-substBound3 : ∀{Γ τ1 τ2 τ3} → {Θ : Source.sctx [] Γ} {vΘ : substVal Θ} {Θ' : Pilot.sctx [] ⟨⟨ Γ ⟩⟩c}
                     → {e : [] Source.|- τ1} {ve : val e} {e' : [] Source.|- τ2} {ve' : val e'} {e'' : [] Source.|- τ3} {ve'' : val e''}
                       {E : [] Pilot.|- ⟨⟨ τ1 ⟩⟩} {E' : [] Pilot.|- ⟨⟨ τ2 ⟩⟩} {E'' : [] Pilot.|- ⟨⟨ τ3 ⟩⟩}
                     → substBound Θ vΘ Θ'
                     → valBound e ve E → valBound e' ve' E' → valBound e'' ve'' E''
                     → substBound (Source.lem5' Θ e e' e'') (extend-substVal3 vΘ ve ve' ve'') (Pilot.lem5' Θ' E E' E'')
  extend-substBound3 sb vbE vbE' vbE'' i0 = vbE
  extend-substBound3 sb vbE vbE' vbE'' (iS i0) = vbE'
  extend-substBound3 sb vbE vbE' vbE'' (iS (iS i0)) = vbE''
  extend-substBound3 sb vbE vbE' vbE'' (iS (iS (iS x))) = sb x

  -- inversion lemma
  inv1 : ∀ {τ} {v v' : [] Source.|- τ} {n : Cost} → val v → evals v v' n → _≤s_{[]} (interp-Cost n) 0C
  inv1 z-isval z-evals = refl-s
  inv1 (suc-isval e v) (s-evals evals) = inv1 v evals
  inv1 (pair-isval e1 e2 v v₁) (pair-evals evals evals₁) = cong-+ (inv1 v evals) (inv1 v₁ evals₁) trans +-unit-l trans refl-s
  inv1 (lam-isval e) lam-evals = refl-s
  inv1 unit-isval unit-evals = refl-s
  inv1 (delay-isval e) delay-evals = refl-s
  inv1 nil-isval nil-evals = refl-s
  inv1 (cons-isval x xs v v₁) (cons-evals evals evals₁) = cong-+ (inv1 v evals) (inv1 v₁ evals₁) trans +-unit-l
  inv1 true-isval true-evals = refl-s
  inv1 false-isval false-evals = refl-s

  inv2 : ∀ {τ} {v e : [] Source.|- τ} {n : Cost} -> val v → evals v e n → v == e
  inv2 z-isval z-evals = Refl
  inv2 (suc-isval e₁ v) (s-evals evals) = ap suc (inv2 v evals)
  inv2 (pair-isval e1 e2 v v₁) (pair-evals evals evals₁) = ap2 prod (inv2 v evals) (inv2 v₁ evals₁)
  inv2 (lam-isval e₁) lam-evals = Refl
  inv2 unit-isval unit-evals = Refl
  inv2 (delay-isval e₁) delay-evals = Refl
  inv2 nil-isval nil-evals = Refl
  inv2 (cons-isval x xs v v₁) (cons-evals evals evals₁) = ap2 _::s_ (inv2 v evals) (inv2 v₁ evals₁)
  inv2 true-isval true-evals = Refl
  inv2 false-isval false-evals = Refl

  val-hprop : ∀ {τ} {v : [] Source.|- τ} → (d1 d2 : val v) → d1 == d2
  val-hprop z-isval z-isval = Refl
  val-hprop (suc-isval e d1) (suc-isval .e d2) = ap (suc-isval e) (val-hprop d1 d2)
  val-hprop (pair-isval e1 e2 d1 d2) (pair-isval .e1 .e2 d3 d4) = ap2 (pair-isval e1 e2) (val-hprop d1 d3) (val-hprop d2 d4)
  val-hprop (lam-isval e) (lam-isval .e) = Refl
  val-hprop unit-isval unit-isval = Refl
  val-hprop (delay-isval e) (delay-isval .e) = Refl
  val-hprop nil-isval nil-isval = Refl
  val-hprop (cons-isval x xs d1 d2) (cons-isval .x .xs d3 d4) = ap2 (cons-isval x xs) (val-hprop d1 d3) (val-hprop d2 d4)
  val-hprop true-isval true-isval = Refl
  val-hprop false-isval false-isval = Refl

  transport-valBound :  ∀{τ} {e e' : [] Source.|- τ} {d : val e} {d' : val e'}
                     → (α : e == e')
                     → transport val α d == d'
                     → (E : [] Pilot.|- ⟨⟨ τ ⟩⟩)
                     → valBound e d E → valBound e' d' E
  transport-valBound Refl Refl E vb = vb

  Eq0C-≤0 : ∀ {n} → Equals0c n → _≤s_{[]} (interp-Cost n) 0C
  Eq0C-≤0 Eq0-0c = refl-s
  Eq0C-≤0 (Eq0-+c e e₁) = cong-+ (Eq0C-≤0 e) (Eq0C-≤0 e₁) trans +-unit-l

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
module StateSizedIO.Object where

open import Data.Product
open import StateSizedIO.Base public
{-
--  This definition was probably moved to StateSizedIO.Base
--  and by accident left here. Delete this.
record Interfaceˢ : Set₁ where
  field
    Stateˢ    : Set
    Methodˢ   : Stateˢ → Set
    Resultˢ   : (s : Stateˢ) → (m : Methodˢ s) → Set
    nextˢ     : (s : Stateˢ) → (m : Methodˢ s) → Resultˢ s m → Stateˢ
open Interfaceˢ public
-}

module _ (I : Interfaceˢ)(let S = Stateˢ I) (let M = Methodˢ I)
         (let R = Resultˢ I) (let next = nextˢ I) where
  -- A simple object just returns for a method the response
  -- and the object itself
  record Objectˢ (s : S) : Set where
    coinductive
    field
      objectMethod : (m : M s) → Σ[ r ∈ R s m ] Objectˢ (next s m r)

  open Objectˢ public

_▹_  : {A : Set } → { B : Set } →  A → (A → B) → B
a ▹ f = f a

-- Bisimilation for Objectˢ

module Bisim (I : Interfaceˢ)
  (let S    = Stateˢ  I)
  (let M    = Methodˢ I)
  (let R    = Resultˢ I)
  (let next = nextˢ   I)
  (let O = Objectˢ I)
  where

    mutual

      record _≅_ {s : S} (o o' : O s) : Set where
        coinductive
        field bisimMethod : (m : M s) → objectMethod o m ≡×≅ objectMethod o' m

      data _≡×≅_ {s m} : (p p' :  Σ[ r ∈ R s m ] O (next s m r)) → Set where
        bisim : ∀{r} (let s' = next s m r) {o o' : O s'} (p : o ≅ o')
              → (r , o) ≡×≅ (r , o')

    open _≅_ public

    refl≅ : ∀{s} (o : O s) → o ≅ o
    bisimMethod (refl≅ o) m = bisim (refl≅ (proj₂ (objectMethod o m)))

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
{-# OPTIONS --type-in-type #-}
open import Data.Unit
open import Data.Product
open import Data.List hiding ( concat )
open import Data.String
open import Relation.Binary.PropositionalEquality
module Spire.Examples.InferredPropositionalDesc where

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

elimEq : {A : Set} (x : A) (P : (y : A) → x ≡ y → Set)
  → P x refl
  → (y : A) (p : x ≡ y) → P y p
elimEq .x P prefl x refl = prefl

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

Label : Set
Label = String

Enum : Set
Enum = List Label

data Tag : Enum → Set where
  here : ∀{l E} → Tag (l ∷ E)
  there : ∀{l E} → Tag E → Tag (l ∷ E)

Cases : {E : Enum} (P : Tag E → Set) → Set
Cases {[]} P = ⊤
Cases {l ∷ E} P = P here × Cases λ t → P (there t)

case : {E : Enum} (P : Tag E → Set) (cs : Cases P) (t : Tag E) → P t
case {l ∷ E} P (c , cs) here = c
case {l ∷ E} P (c , cs) (there t) = case (λ t → P (there t)) cs t

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

data Desc (I : Set) : Set₁ where
  `End : (i : I) → Desc I
  `Rec : (i : I) (D : Desc I) → Desc I
  `Arg : (A : Set) (B : A → Desc I) → Desc I
  `RecFun : (A : Set) (B : A → I) (D : Desc I) → Desc I

ISet : Set → Set₁
ISet I = I → Set

El : {I : Set} (D : Desc I) (X : ISet I) → ISet I
El (`End j) X i = j ≡ i
El (`Rec j D) X i = X j × El D X i
El (`Arg A B) X i = Σ A (λ a → El (B a) X i)
El (`RecFun A B D) X i = ((a : A) → X (B a)) × El D X i

data μ {I : Set} (D : Desc I) (i : I) : Set where
  con : El D (μ D) i → μ D i

All : {I : Set} (D : Desc I) {X : ISet I} (P : (i : I) → X i → Set) (i : I) (xs : El D X i) → Set
All (`End j) P i q = ⊤
All (`Rec j D) P i (x , xs) = P j x × All D P i xs
All (`Arg A B) P i (a , b) = All (B a) P i b
All (`RecFun A B D) P i (f , xs) = ((a : A) → P (B a) (f a)) × All D P i xs

caseD : (E : Enum) (I : Set) (cs : Cases (λ _ → Desc I)) (t : Tag E) → Desc I
caseD E I cs t = case (λ _ → Desc I) cs t

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

ind :
  {I : Set}
  (D : Desc I)
  (P : (i : I) → μ D i → Set)
  (pcon : (i : I) (xs : El D (μ D) i) → All D P i xs → P i (con xs))
  {i : I}
  (x : μ D i)
  → P i x

hyps :
  {I : Set}
  (D₁ : Desc I)
  (P : (i : I) → μ D₁ i → Set)
  (pcon : (i : I) (xs : El D₁ (μ D₁) i) → All D₁ P i xs → P i (con xs))
  (D₂ : Desc I)
  {i : I}
  (xs : El D₂ (μ D₁) i)
  → All D₂ P i xs

ind D P pcon (con xs) = pcon _ xs (hyps D P pcon D xs)

hyps D P pcon (`End j) q = tt
hyps D P pcon (`Rec j A) (x , xs) = ind D P pcon x , hyps D P pcon A xs
hyps D P pcon (`Arg A B) (a , b) = hyps D P pcon (B a) b
hyps D P pcon (`RecFun A B E) (f , xs) = (λ a → ind D P pcon (f a)) , hyps D P pcon E xs

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

module Desugared where

  ℕT : Enum
  ℕT = "zero" ∷ "suc" ∷ []

  VecT : Enum
  VecT = "nil" ∷ "cons" ∷ []

  ℕC : Tag ℕT → Desc ⊤
  ℕC = caseD ℕT ⊤
    ( `End tt
    , `Rec tt (`End tt)
    , tt
    )

  ℕD : Desc ⊤
  ℕD = `Arg (Tag ℕT) ℕC

  ℕ : ⊤ → Set
  ℕ = μ ℕD

  zero : ℕ tt
  zero = con (here , refl)

  suc : ℕ tt → ℕ tt
  suc n = con (there here , n , refl)

  VecC : (A : Set) → Tag VecT → Desc (ℕ tt)
  VecC A = caseD VecT (ℕ tt)
    ( `End zero
    , `Arg (ℕ tt) (λ n → `Arg A λ _ → `Rec n (`End (suc n)))
    , tt
    )

  VecD : (A : Set) → Desc (ℕ tt)
  VecD A = `Arg (Tag VecT) (VecC A)

  Vec : (A : Set) (n : ℕ tt) → Set
  Vec A n = μ (VecD A) n

  nil : (A : Set) → Vec A zero
  nil A = con (here , refl)

  cons : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
  cons A n x xs = con (there here , n , x , xs , refl)

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

  module Induction where

    add : ℕ tt → ℕ tt → ℕ tt
    add = ind ℕD (λ _ _ → ℕ tt → ℕ tt)
      (λ u t,c → case
        (λ t → (c : El (ℕC t) ℕ u)
               (ih : All ℕD (λ u n → ℕ u → ℕ u) u (t , c))
               → ℕ u → ℕ u
        )
        ( (λ q ih n → n)
        , (λ m,q ih,tt n → suc (proj₁ ih,tt n))
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

    mult : ℕ tt → ℕ tt → ℕ tt
    mult = ind ℕD (λ _ _ → ℕ tt → ℕ tt)
      (λ u t,c → case
        (λ t → (c : El (ℕC t) ℕ u)
               (ih : All ℕD (λ u n → ℕ u → ℕ u) u (t , c))
               → ℕ u → ℕ u
        )
        ( (λ q ih n → zero)
        , (λ m,q ih,tt n → add n (proj₁ ih,tt n))
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

    append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
    append A m = ind (VecD A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n))
      (λ m t,c → case
        (λ t → (c : El (VecC A t) (Vec A) m)
               (ih : All (VecD A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)) m (t , c))
               (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
        )
        ( (λ q ih n ys → subst (λ m → Vec A (add m n)) q ys)
        , (λ m',x,xs,q ih,tt n ys →
            let m' = proj₁ m',x,xs,q
                x = proj₁ (proj₂ m',x,xs,q)
                q = proj₂ (proj₂ (proj₂ m',x,xs,q))
                ih = proj₁ ih,tt
            in
            subst (λ m → Vec A (add m n)) q (cons A (add m' n) x (ih n ys))
          )
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

    concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
    concat A m n = ind (VecD (Vec A m)) (λ n xss → Vec A (mult n m))
      (λ n t,c → case
        (λ t → (c : El (VecC (Vec A m) t) (Vec (Vec A m)) n)
               (ih : All (VecD (Vec A m)) (λ n xss → Vec A (mult n m)) n (t , c))
               → Vec A (mult n m)
        )
        ( (λ q ih → subst (λ n → Vec A (mult n m)) q (nil A))
        , (λ n',xs,xss,q ih,tt →
            let n' = proj₁ n',xs,xss,q
                xs = proj₁ (proj₂ n',xs,xss,q)
                q = proj₂ (proj₂ (proj₂ n',xs,xss,q))
                ih = proj₁ ih,tt
            in
            subst (λ n → Vec A (mult n m)) q (append A m xs (mult n' m) ih)
          )
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

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

  module Eliminator where

    elimℕ : (P : (ℕ tt) → Set)
      (pzero : P zero)
      (psuc : (m : ℕ tt) → P m → P (suc m))
      (n : ℕ tt)
      → P n
    elimℕ P pzero psuc = ind ℕD (λ u n → P n)
      (λ u t,c → case
        (λ t → (c : El (ℕC t) ℕ u)
               (ih : All ℕD (λ u n → P n) u (t , c))
               → P (con (t , c))
        )
        ( (λ q ih →
            elimEq tt (λ u q → P (con (here , q)))
              pzero
              u q
          )
        , (λ n,q ih,tt →
            elimEq tt (λ u q → P (con (there here , proj₁ n,q , q)))
              (psuc (proj₁ n,q) (proj₁ ih,tt))
              u (proj₂ n,q)
          )
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

    elimVec : (A : Set) (P : (n : ℕ tt) → Vec A n → Set)
      (pnil : P zero (nil A))
      (pcons : (n : ℕ tt) (a : A) (xs : Vec A n) → P n xs → P (suc n) (cons A n a xs))
      (n : ℕ tt)
      (xs : Vec A n)
      → P n xs
    elimVec A P pnil pcons n = ind (VecD A) (λ n xs → P n xs)
      (λ n t,c → case
        (λ t → (c : El (VecC A t) (Vec A) n)
               (ih : All (VecD A) (λ n xs → P n xs) n (t , c))
               → P n (con (t , c))
        )
        ( (λ q ih →
            elimEq zero (λ n q → P n (con (here , q)))
              pnil
              n q
          )
        , (λ n',x,xs,q ih,tt →
            let n' = proj₁ n',x,xs,q
                x = proj₁ (proj₂ n',x,xs,q)
                xs = proj₁ (proj₂ (proj₂ n',x,xs,q))
                q = proj₂ (proj₂ (proj₂ n',x,xs,q))
                ih = proj₁ ih,tt
            in
            elimEq (suc n') (λ n q → P n (con (there here , n' , x , xs , q)))
              (pcons n' x xs ih )
              n q
          )
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

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

    add : ℕ tt → ℕ tt → ℕ tt
    add = elimℕ (λ _ → ℕ tt → ℕ tt)
      (λ n → n)
      (λ m ih n → suc (ih n))

    mult : ℕ tt → ℕ tt → ℕ tt
    mult = elimℕ (λ _ → ℕ tt → ℕ tt)
      (λ n → zero)
      (λ m ih n → add n (ih n))

    append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
    append A = elimVec A (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n))
      (λ n ys → ys)
      (λ m x xs ih n ys → cons A (add m n) x (ih n ys))

    concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
    concat A m = elimVec (Vec A m) (λ n xss → Vec A (mult n m))
      (nil A)
      (λ n xs xss ih → append A m xs (mult n m) ih)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


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

module Midi where

open import Agda.Builtin.String using (String)
open import Data.Fin using (toℕ)
open import Data.Nat using (ℕ)
open import Data.List
open import Data.Product using (_,_)

open import Note
open import Pitch
open import MidiEvent
open import Music

{-# FOREIGN GHC
  import Codec.Midi
  import Data.Text (Text, unpack)
  import Data.List (sort)

  type HsTicksPerBeat = Integer
  type HsTicks        = Integer
  type HsKey          = Integer
  type HsVelocity     = Integer
  type HsPreset       = Integer
  type HsChannel      = Integer
  type HsTempo        = Integer

  type HsAbsTime      = Integer

  type HsTrackName    = Text

  -- convert beats per minute to microseconds per beat
  bpmToTempo :: Int -> Tempo
  bpmToTempo bpm = round $ 1000000 * 60 / fromIntegral bpm

  data HsMidiMessage = HsNoteOn HsVelocity HsTicks HsKey | HsNoteOff HsVelocity HsTicks HsKey
    deriving Eq

  getTicks :: HsMidiMessage -> HsTicks
  getTicks (HsNoteOn  _ t _) = t
  getTicks (HsNoteOff _ t _) = t

  instance Ord HsMidiMessage where
    a <= b = getTicks a <= getTicks b

  data HsMidiTrack = HsMidiTrack HsTrackName HsPreset HsChannel HsTempo [HsMidiMessage]

  fi = fromInteger

  makeTrack :: Channel -> HsAbsTime -> [HsMidiMessage] -> (Track Ticks , HsAbsTime)
  makeTrack c t []                      = ([(0, TrackEnd)], t)
  makeTrack c t (HsNoteOn  v t' k : ms) = let (rest, t'') = makeTrack c t' ms
                                          in ((fi (t' - t), NoteOn  c (fi k) (fi v)) : rest, t'')
  makeTrack c t (HsNoteOff v t' k : ms) = let (rest, t'') = makeTrack c t' ms
                                          in ((fi (t' - t), NoteOff c (fi k) (fi v)) : rest, t'')

  toTrack :: HsMidiTrack -> Track Ticks
  toTrack (HsMidiTrack name preset channel tempo messages) =
    (0, TrackName (unpack name)) :
    (0, ProgramChange (fi channel) (fi preset)) :
    (0, TempoChange (bpmToTempo (fi tempo))) :
    fst (makeTrack (fi channel) 0 (sort messages))

  toMidi :: HsTicksPerBeat -> [HsMidiTrack] -> Midi
  toMidi ticks tracks = let mtracks = map toTrack tracks
                        in Midi MultiTrack (TicksPerBeat (fi ticks)) mtracks

  exportTracks :: Text -> HsTicksPerBeat -> [HsMidiTrack] -> IO ()
  exportTracks filePath ticksPerBeat tracks = do
    let path = unpack filePath
    putStrLn $ "Writing file " ++ path
    -- putStrLn $ show $ toMidi ticksPerBeat tracks
    exportFile path (toMidi ticksPerBeat tracks)
#-}

data Unit : Set where
  unit : Unit

{-# COMPILE GHC Unit = data () (()) #-}

postulate
  IO : Set → Set

{-# BUILTIN IO IO #-}
{-# COMPILE GHC IO = type IO #-}

FilePath = String

data Pair (A : Set) (B : Set) : Set where
  pair : A → B → Pair A B

{-# COMPILE GHC Pair = data (,) ((,)) #-}

HInstrument HPitch HVelocity : Set
HInstrument = ℕ
HPitch      = ℕ
HVelocity   = ℕ
HChannel    = ℕ
HTempo      = ℕ

data MidiMessage : Set where
  noteOn  : HVelocity → Tick → HPitch → MidiMessage
  noteOff : HVelocity → Tick → HPitch → MidiMessage

{-# COMPILE GHC MidiMessage = data HsMidiMessage (HsNoteOn | HsNoteOff) #-}

event→messages : MidiEvent → List MidiMessage
event→messages (midiEvent p start stop v) =
  let v' = toℕ v
      p' = unpitch p
  in noteOn v' start p' ∷ noteOff v' stop p' ∷ []

data HMidiTrack : Set where
  htrack : String → HInstrument → HChannel → HTempo → List MidiMessage → HMidiTrack

{-# COMPILE GHC HMidiTrack = data HsMidiTrack (HsMidiTrack) #-}

track→htrack : MidiTrack → HMidiTrack
track→htrack (track n i c t m) = htrack n (toℕ i) (toℕ c) t (concatMap event→messages m)

postulate
  exportTracks : FilePath        → -- path to the file to save the MIDI data to
                 ℕ               → -- number of ticks per beat (by default a beat is a quarter note)
                 List HMidiTrack → -- tracks, one per instrument
                 IO Unit

{-# COMPILE GHC exportTracks = exportTracks #-}

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
-- | In this module we show that the substream relation is transitive.

open import Size
open import Streams
open import Relation.Binary.PropositionalEquality as P
open import Data.Product
open import Function

tl' : ∀{A} → Stream A → Stream A
tl' s = tl s {∞}

{-
data Reachable {A : Set} (P : A → Set) : Stream A → Set where
  nowR : (s : Stream A) → P (hd s) → Reachable P s
  laterR : (s : Stream A) → Reachable P (tl s) → Reachable P (tl s)
-}

{-
data Eventually {A : Set} (P : A → Set) (s : Stream A) : Set where
  now : P (hd s) → Eventually P s
  later : Eventually P (tl s) → Eventually P s

-}

record Always {A : Set} (P : A → Set) (s : Stream A) : Set where
  coinductive
  field
    hd-valid : P (hd s)
    tl-valid : Always P (tl s)

open Always public

Always-coiter : ∀{A} {P : A → Set} {B : Stream A → Set}
                (hv : ∀ s → B s → P (hd s))
                (tv : ∀ s → B s → B (tl s)) →
                ∀ s → B s → Always P s
hd-valid (Always-coiter hv tv s b) = hv s b
tl-valid (Always-coiter hv tv s b) = Always-coiter hv tv (tl s) (tv s b)

data E {A : Set} (P : A → Set) (F : Stream A → Set) (s : Stream A) : Set where
  now : P (hd s) → F (tl s) → E P F s
  later : E P F (tl s) → E P F s

record Fair {A : Set} (P : A → Set) (s : Stream A) : Set where
  coinductive
  field
    step : E P (Fair P) s

open Fair public

Eventually : ∀{A} → (P : A → Set) → Stream A → Set
Eventually P = E P (Fair P)

Fair-coiter : ∀{A} {P : A → Set} {B : Stream A → Set}
              (st : ∀ s → B s → E P B s) →
              ∀ s → B s → Fair P s
xFair-coiter : ∀{A} {P : A → Set} {B : Stream A → Set}
               (st : ∀ s → B s → E P B s) →
               ∀ s → E P B s → Eventually P s

step (Fair-coiter st s b) = xFair-coiter st s (st s b)

xFair-coiter st s (now p b) = now p (Fair-coiter st (tl s) b)
xFair-coiter st s (later e) = later (xFair-coiter st (tl s) e)

Stream-coiter : ∀{A B : Set} → (B → A) → (B → B) → B → Stream A
hd (Stream-coiter h t b) = h b
tl (Stream-coiter h t b) = Stream-coiter h t (t b)

∃-elim : ∀{A : Set} {B : A → Set} {C : Set} →
         ((a : A) → B a → C) →
         Σ A B → C
∃-elim f (a , b) = f a b

≡-elim : ∀{A : Set} {B : A → A → Set} →
         ((x : A) → B x x) →
         {x y : A} → x ≡ y → B x y
≡-elim f {x = x} refl = f x

Always-coind : ∀{A} {P : A → Set} {B : Set} -- {C : Stream A → Set}
               {h : B → A} {t : B → B}
               (hv : ∀ b → P (h b))
               → ∀ b → Always P (Stream-coiter h t b)
Always-coind {A} {P = P} {B} {h} {t} hv b =
  Always-coiter {B = λ s → ∃ λ b → s ≡ Stream-coiter h t b}
                f g (Stream-coiter h t b) (b , refl)
  where
    f : (s : Stream A) → ∃ (λ b → s ≡ Stream-coiter h t b) → P (hd s)
    f s = ∃-elim u
      where
        u : (b : B) → s ≡ Stream-coiter h t b → P (hd s)
        u b p = subst P (sym (cong hd p)) (hv b)

    g : (s : Stream A) →
        ∃ (λ b → s ≡ Stream-coiter h t b) →
        ∃ (λ b → tl s ≡ Stream-coiter h t b)
    g s = ∃-elim u
      where
        u : (b : B) → s ≡ Stream-coiter h t b →
            ∃ (λ b₁ → tl s ≡ Stream-coiter h t b₁)
        u b p = (t b , cong tl' p)
{-
hd-valid (Always-coind h t hv b) = hv b
tl-valid (Always-coind h t hv b) = Always-coind h t hv (t b)
-}

dcoiter-Fair : ∀{A} {P : A → Set} {B : Set} {C : Stream A → Set}
  {h : B → A} {t : B → B}
  (st : ∀ b → C (Stream-coiter h t b) → E P C (Stream-coiter h t b)) →
  ∀ b → C (Stream-coiter h t b) → Fair P (Stream-coiter h t b)
xdcoiter-Fair : ∀{A} {P : A → Set} {B : Set} {C : Stream A → Set}
  {h : B → A} {t : B → B}
  (st : ∀ b → C (Stream-coiter h t b) → E P C (Stream-coiter h t b)) →
  ∀ b → E P C (Stream-coiter h t b) → Eventually P (Stream-coiter h t b)
step (dcoiter-Fair st b c) = xdcoiter-Fair st b (st b c)

xdcoiter-Fair st b (now p c) = now p (dcoiter-Fair st _ c)
xdcoiter-Fair st b (later e) = later (xdcoiter-Fair st _ e)

E-iter : ∀{A} {P : A → Set} {F : Stream A → Set} {B : Stream A → Set}
         (n : ∀ s → P (hd s) → F (tl s) → B s)
         (l : ∀ s → B (tl s) → B s) →
         ∀ s → E P F s → B s
E-iter n l s (now p f) = n s p f
E-iter n l s (later e) = l s (E-iter n l (tl s) e)

{-
Ev-iter : ∀{A} {P : A → Set} {F : Stream A → Set} {B : Stream A → Set}
          (st : ∀ s → Fair P s → F s)
          (n : ∀ s → F (tl s) → B s)
          (l : ∀ s → B (tl s) → B s) →
          ∀ s → Eventually P s → B s
Ev-iter st n l s (now p f) = n s (st (tl s) f)
Ev-iter st n l s (later e) = l s (Ev-iter st n l (tl s) e)
-}

{-
Ev-iter : ∀{A} {P : A → Set} {B : Stream A → Set}
          (n : ∀ s → Fair P (tl s) → B s)
          (l : ∀ s → B (tl s) → B s) →
          ∀ s → Eventually P s → B s
Ev-iter n l s (now p f) = n s f
Ev-iter n l s (later e) = l s (Ev-iter n l (tl s) e)
-}

{-
Ev-ind : ∀{A} {P : A → Set} (F : (t : Stream A) → Set)
         (B : (t : Stream A) → Eventually P t → Set)
         (st : ∀{t} → Fair P t → F t)
         (n : ∀{t} → (p : P (hd t)) → (f : F (tl t)) → B t (now p f)) →
         (l : ∀{t e} → B (tl t) e → B t (later e)) →
         (s : Stream A) → (e : Eventually P s) → B s e
Ev-ind F B st n l s (now p f) =
  let r = n p {!st!}
  in {!!}
Ev-ind F B st n l s (later e) = l (Ev-ind F B st n l (tl s) e)
-}

filter : ∀{A} {P : A → Set} (s : Stream A) → Fair P s → Stream A
xfilter : ∀{A} {P : A → Set} (s : Stream A) → Eventually P s → Stream A

filter s p = xfilter s (step p)

hd (xfilter s (now p q)) = hd s
tl (xfilter s (now p q)) = filter (tl s) q
xfilter s (later p)      = xfilter (tl s) p

filter-find : ∀{A} {P : A → Set} (s : Stream A) →
              Eventually P s → A × ∃ (Fair P)
filter-find = E-iter (λ s p f → (hd s , tl s , f)) (λ s → id)

filter-h : ∀{A} {P : A → Set} → ∃ (Fair P) → A
filter-h (s , f) = proj₁ (filter-find s (step f))

filter-t : ∀{A} {P : A → Set} → ∃ (Fair P) → ∃ (Fair P)
filter-t {A} {P} (s , f) = proj₂ (filter-find s (step f))

filter' : ∀{A} {P : A → Set} → ∃ (Fair P) → Stream A
filter' = Stream-coiter filter-h filter-t

-- filter' : ∀{A} {P : A → Set} (s : Stream A) → Fair P s → Stream A
-- filter' s f = filter'' (s , f)

{-
filter-pres-fair : ∀{A} {P : A → Set} (u : ∃ (Fair P)) →
                   Fair P (filter' u)
filter-pres-fair u = {!!}

filter-always' : ∀{A} {P : A → Set} (u : ∃ (Fair P)) →
                 Always P (filter' u)
filter-always' {A} {P} (s , f) = Always-coiter {B = Fair P} {!!} {!!} (filter' (s , f)) {!!}

-}

filter-always' : ∀{A} {P : A → Set} (u : ∃ (Fair P)) →
                 Always P (filter' u)
filter-always' {A} {P} = Always-coind f
  where
    xf : (s : Stream A) (e : Eventually P s) → P (proj₁ (filter-find s e))
    xf s (now p _) = p
    xf s (later e) = xf (tl s) e

    f : (u : ∃ (Fair P)) → P (filter-h u)
    f (s , f) = xf s (step f)

filter-always : ∀{A} {P : A → Set} (s : Stream A) → (f : Fair P s) →
                Always P (filter s f)
xfilter-always : ∀{A} {P : A → Set} (s : Stream A) → (e : Eventually P s) →
                 Always P (xfilter s e)

filter-always s f = xfilter-always s (step f)
hd-valid (xfilter-always s (now p f)) = p
tl-valid (xfilter-always s (now p f)) = filter-always (tl s) f
xfilter-always s (later e)            = xfilter-always (tl s) e

{-
filter-pres : ∀{A} {P Q : A → Set} (s : Stream A) → (f : Fair P s) →
              Always Q s → Always Q (filter s f)
xfilter-pres : ∀{A} {P Q : A → Set} (s : Stream A) → (e : Eventually P s) →
               Always Q s → Always Q (xfilter s e)

filter-pres s f a = xfilter-pres s (step f) a

xfilter-pres = {!!}
-}
-- xfilter-pres {Q = Q} s e a =
--   Ev-ind (λ t e → Always Q (xfilter t e))
--          (λ p f → record { hd-valid = {!hd-valid a!} ; tl-valid = {!!} })
--          {!!}
--          s
--          e

{-
hd-valid (xfilter-pres s (now p f) a) = hd-valid a
tl-valid (xfilter-pres s (now p f) a) = filter-pres (tl s) f (tl-valid a)
xfilter-pres s (later e) a = xfilter-pres (tl s) e (tl-valid a)
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Bools where

open import Agda.Builtin.Bool public
  renaming (Bool to 𝔹)

not : 𝔹 → 𝔹
not true  = false
not false = true

-- T : 𝔹 → Set
-- T true  = ⊤
-- T false = ⊥

if_then_else_ : ∀ {a} {A : Set a} → 𝔹 → A → A → A
if true  then t else _ = t
if false then _ else f = f

_∧_ : 𝔹 → 𝔹 → 𝔹
true  ∧ b = b
false ∧ _ = false

_∨_ : 𝔹 → 𝔹 → 𝔹
true  ∨ _ = true
false ∨ b = b

_xor_ : 𝔹 → 𝔹 → 𝔹
true  xor b = not b
false xor b = b


text:
{-

Definition of finitely indexed types

A type is finitely indexed if, for some `n`, there merely exists a
surjective function from `Fin n` to it. Note that a type doesn't need
to be a set in order for it to be finitely indexed. For example, the
circle is finitely indexed.

This definition is weaker than `isFinSet`.

-}

{-# OPTIONS --safe #-}

module Cubical.Data.FinInd where

open import Cubical.Data.Nat
open import Cubical.Data.SumFin
open import Cubical.Data.Sigma
open import Cubical.Data.FinSet
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Functions.Surjection
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.S1

private
  variable
    ℓ : Level
    A : Type ℓ

isFinInd : Type ℓ → Type ℓ
isFinInd A = ∃[ n ∈ ℕ ] Fin n ↠ A

isFinSet→isFinInd : isFinSet A → isFinInd A
isFinSet→isFinInd h = PT.elim
  (λ _ → squash)
  (λ equiv →
    ∣ _ , invEq equiv , section→isSurjection (retEq equiv) ∣) (h .snd)

isFinInd-S¹ : isFinInd S¹
isFinInd-S¹ = ∣ 1 , f , isSurjection-f ∣
  where
    f : Fin 1 → S¹
    f _ = base
    isSurjection-f : isSurjection f
    isSurjection-f b = PT.map (λ base≡b → fzero , base≡b) (isConnectedS¹ b)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --without-K #-}
module higher.circle.core where

open import equality

data S¹ : Set where
  base : S¹

postulate loop : base ≡ base

private
  module Eliminators' {i}(B : S¹ → Set i)
                      (m : B base)
                      (l : subst B loop m ≡ m) where
    elim' : (x : S¹) → B x
    elim' base = m

    β-base' : elim' base ≡ m
    β-base' = refl

    postulate β-loop' : ap' elim' loop ≡ l

private
  module Eliminators {i} {B : Set i}
                     (m : B) (l : m ≡ m) where
    open Eliminators' (λ _ → B) m (subst-const loop m · l)

    elim : S¹ → B
    elim = elim'

    β-base : elim base ≡ m
    β-base = refl

    postulate β-loop : ap elim loop ≡ l

open Eliminators public
open Eliminators' public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base