text:
open import Common.Level
open import Common.Reflection
open import Common.Equality
open import Common.Prelude

postulate
  f : ∀ a → Set a

pattern expectedType =
  pi (vArg (def (quote Level) []))
     (abs "a" (sort (set (var 0 []))))

ok : ⊤
ok = _

notOk : String
notOk = "not ok"

macro
  isExpected : QName → Tactic
  isExpected x hole =
    bindTC (getType x) λ
    { expectedType → give (quoteTerm ok)    hole
    ; t            → give (quoteTerm notOk) hole }

thm : ⊤
thm = isExpected f

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Functions
open import Lists.Definition
open import Lists.Fold.Fold
open import Lists.Concat
open import Lists.Length
open import Setoids.Setoids
open import Maybe
open import Numbers.Naturals.Semiring

module Lists.Permutations {a b : _} {A : Set a} (S : Setoid {a} {b} A) (decidable : (x y : A) → (Setoid._∼_ S x y) || ((Setoid._∼_ S x y) → False)) where

open Setoid S
open Equivalence eq

indexOf : (a : A) → (l : List A) → Maybe ℕ
indexOf a [] = no
indexOf a (x :: l) with decidable a x
... | inl eq = yes 0
... | inr noneq = mapMaybe succ (indexOf a l)

eltAt : (n : ℕ) → (l : List A) → Maybe A
eltAt n [] = no
eltAt zero (x :: l) = yes x
eltAt (succ n) (x :: l) = eltAt n l

indexOfIsIndexOf : (a : A) → (l : List A) → {n : ℕ} → indexOf a l ≡ yes n → Sg A (λ b → (eltAt n l ≡ yes b) && (b ∼ a))
indexOfIsIndexOf a (x :: l) {n} ind with decidable a x
indexOfIsIndexOf a (x :: l) {.0} refl | inl a=x = x , (refl ,, symmetric a=x)
indexOfIsIndexOf a (x :: l) {zero} ind | inr a!=x with indexOf a l
indexOfIsIndexOf a (x :: l) {zero} () | inr a!=x | no
indexOfIsIndexOf a (x :: l) {zero} () | inr a!=x | yes _
indexOfIsIndexOf a (x :: l) {succ n} ind | inr a!=x with mapMaybePreservesYes ind
... | m , (pr ,, z=n) = indexOfIsIndexOf a l (transitivity pr (applyEquality yes (succInjective z=n)))

Permutation : (List A) → (List A) → Set
Permutation [] [] = True
Permutation [] (x :: l2) = False
Permutation (x :: l1) [] = False
Permutation (a :: as) (b :: bs) with decidable a b
Permutation (a :: as) (b :: bs) | inl a=b = Permutation as bs
Permutation (a :: as) (b :: bs) | inr a!=b = {!!}

ext: agda


text:
module MixfixBinders where

postulate
  M      : Set → Set
  return : ∀ {A} → A → M A
  bind   : ∀ {A B} → M A → (A → M B) → M B

infixr 40 bind
syntax bind m (λ x → m′) = x ← m , m′

postulate
  X : Set
  m₁ m₂ m₃ : M X
  f : X → X → X

foo : M X
foo = x₁ ← m₁ ,
      x₂ ← m₂ ,
      x₃ ← m₃ ,
      return (f x₁ (f x₂ x₃))

infixr 10 Σ _,_
syntax Σ A (λ x → B) = Σ x ∈ A , B
data Σ (A : Set)(B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ x ∈ A , B x

infix 50 _≤_
postulate
  _≤_ : X → X → Set
  x₁ x₂ : X
  le : x₁ ≤ x₂

p : Σ x ∈ X , Σ y ∈ X , x ≤ y
p = x₁ , x₂ , le

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text: record _ : Set where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Categories.Functor.Profunctor where

open import Level

open import Categories.Category
open import Categories.Category.Instance.Setoids
open import Categories.Functor.Bifunctor
open import Categories.Functor.Hom

Profunctor : ∀ {o ℓ e} {o′ ℓ′ e′} → Category o ℓ e → Category o′ ℓ′ e′ → Set _
Profunctor {ℓ = ℓ} {e} {ℓ′ = ℓ′} {e′} C D = Bifunctor (Category.op D) C (Setoids (ℓ ⊔ ℓ′) (e ⊔ e′))

id : ∀ {o ℓ e} → {C : Category o ℓ e} → Profunctor C C
id {C = C} = Hom[ C ][-,-]

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Showing booleans
------------------------------------------------------------------------

module Data.Bool.Show where

open import Data.Bool
open import Data.String hiding (show)

show : Bool → String
show true  = "true"
show false = "false"


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

open import Level
open import Data.Unit using (⊤)
open import Function using (flip)

open import Categories.Category
open import Categories.Support.PropositionalEquality

Discrete : ∀ {o} (A : Set o) → Category o o zero
Discrete A = record
  { Obj = A
  ; _⇒_ = _≣_
  ; _≡_ = λ _ _ → ⊤
  ; _∘_ = flip ≣-trans
  ; id = ≣-refl
  ; assoc = _
  ; identityˡ = _
  ; identityʳ = _
  ; equiv = _
  ; ∘-resp-≡ = _
  }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Equality

magic : Nat
magic = 666

macro
  by-magic : Term → TC ⊤
  by-magic hole = unify hole (def (quote magic) [])

  meta-magic : Term → TC ⊤
  meta-magic hole = unify hole (def (quote by-magic) [])

test : Nat
test = meta-magic

check : test ≡ 666
check = refl


text:
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality

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

data All₂ {A : Set} {B : Set} (R : A → B → Set) : ∀ {k} → Vec A k → Vec B k → Set where
  []   :  All₂ R [] []
  _∷_  :  ∀ {k x y} {xs : Vec A k} {ys : Vec B k}
          (r : R x y) (rs : All₂ R xs ys) → All₂ R (x ∷ xs) (y ∷ ys)

Det : ∀ {A : Set} {B : Set} (R : A → B → Set) → Set
Det R = ∀{a b c} → R a b → R a c → b ≡ c

detAll₂ : ∀ {A : Set} {B : Set} (R : A → B → Set) (h : Det R) → Det (All₂ R)
detAll₂ R h rab rac = {!rab!}


text:
-- FNF, 2019-02-06
-- Test the difference between --ignore-interfaces and --ignore-all-interfaces
-- See Issue641-all-interfaces.flags and compare with Issue641.flags

module Issue641-all-interfaces where

-- Provoke a scope checking error.

open NoSuchModule

-- Expected output is some debug messages about importing, plus the error,
-- but in particular re-typechecking Agda.Primitive


text:
-- Andreas & James, 2016-04-18 pre-AIM XXIII
-- order of clauses should not matter here!

{-# OPTIONS --exact-split #-}

open import Common.Equality
open import Common.Prelude
open import Common.Product

thing : Bool → Bool × Bool
proj₁ (thing true) = false
proj₁ (thing false) = true
proj₂ (thing b) = b

test : ∀ b → proj₂ (thing b) ≡ b
test b = refl


text:
open import FRP.JS.RSet using ( ⟦_⟧ )
open import FRP.JS.Behaviour using ( Beh )
open import FRP.JS.DOM using ( DOM )

module FRP.JS.Main where

postulate
  Main : Set
  reactimate : ⟦ Beh DOM ⟧ → Main

{-# COMPILED_JS reactimate require("agda.frp").reactimate #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
------------------------------------------------------------------------------
-- Abelian group theory properties
------------------------------------------------------------------------------

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

module GroupTheory.AbelianGroup.PropertiesATP where

open import GroupTheory.AbelianGroup.Base

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

postulate xyx⁻¹≡y : ∀ a b → a · b · a ⁻¹ ≡ b
{-# ATP prove xyx⁻¹≡y #-}

postulate x⁻¹y⁻¹≡[xy]⁻¹ : ∀ a b → a ⁻¹ · b ⁻¹ ≡ (a · b) ⁻¹
{-# ATP prove x⁻¹y⁻¹≡[xy]⁻¹ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import common
open import syntx
open import derivability

{- Here are the structural rules, as derivation rules -}

module _ (Σ : Signature) where

{-

Γ ⊢ A    (x : A) ∈ Γ
--------------------
   Γ ⊢ x : A

-}

-- The version of the variable rule we use is that Γ ⊢ x : A if Γ ⊢ A holds, and if A is the type
-- corresponding to x in Γ.
VarRule : (k : ℕ) → DerivationRule Σ (([] , (0 , Ty)) , Tm)
rule (VarRule k) ↑ Γ ([] , ◇ ⊢ A) =
  do
    (k' , A') ← get k Γ
    assume (A' ≡ A)
    return (◇ ⊢ var k' :> A)

ConvRule : DerivationRule Σ (([] , (0 , Tm) , (0 , Ty=)) , Tm)
rule ConvRule ↑ Γ ([] , ◇ ⊢ u :> A , ◇ ⊢ A' == B) =
  do
    assume (A ≡ A')
    return (◇ ⊢ u :> B)

ConvEqRule : DerivationRule Σ (([] , (0 , Tm=) , (0 , Ty=)) , Tm=)
rule ConvEqRule ↑ Γ ([] , ◇ ⊢ u == v :> A , ◇ ⊢ A' == B) =
  do
    assume (A ≡ A')
    return (◇ ⊢ u == v :> B)

TyReflRule : DerivationRule Σ (([] , (0 , Ty)) , Ty=)
rule TyReflRule ↑ Γ ([] , ◇ ⊢ A) = return (◇ ⊢ A == A)

TySymmRule : DerivationRule Σ (([] , (0 , Ty=)) , Ty=)
rule TySymmRule ↑ Γ ([] , ◇ ⊢ A == B) = return (◇ ⊢ B == A)

TyTranRule : DerivationRule Σ (([] , (0 , Ty=) , (0 , Ty=)) , Ty=)
rule TyTranRule ↑ Γ ([] , ◇ ⊢ A == B , ◇ ⊢ B' == D) =  -- Can’t use C as a bound variable as it’s a tag.
  do
    assume (B ≡ B')
    return (◇ ⊢ A == D)

TmReflRule : DerivationRule Σ (([] , (0 , Tm)) , Tm=)
rule TmReflRule ↑ Γ ([] , ◇ ⊢ u :> A) = return (◇ ⊢ u == u :> A)

TmSymmRule : DerivationRule Σ (([] , (0 , Tm=)) , Tm=)
rule TmSymmRule ↑ Γ ([] , ◇ ⊢ u == v :> A) = return (◇ ⊢ v == u :> A)

TmTranRule : DerivationRule Σ (([] , (0 , Tm=) , (0 , Tm=)) , Tm=)
rule TmTranRule ↑ Γ ([] , ◇ ⊢ u == v :> A , ◇ ⊢ v' == w :> A') =
  do
    assume (v ≡ v')
    assume (A ≡ A')
    return (◇ ⊢ u == w :> A)

{-
Small hack to make our life easier, the implicit argument [ar] of [StructuralRulesType] is
automatically inferred from the definition of [StructuralRules], but for that they need to be
mutually recursive
-}

StructuralRules : DerivabilityStructure Σ

-- See #4366
private
  ar1 = _
  ar2 = _
  ar3 = _
  ar4 = _
  ar5 = _
  ar6 = _
  ar7 = _
  ar8 = _
  ar9 = _

data StructuralRulesType : {ar : JudgmentArity} → Set where
  var : ℕ → StructuralRulesType {ar1}
  conv : StructuralRulesType {ar2}
  convEq : StructuralRulesType {ar3}
  tyRefl : StructuralRulesType {ar4}
  tySymm : StructuralRulesType {ar5}
  tyTran : StructuralRulesType {ar6}
  tmRefl : StructuralRulesType {ar7}
  tmSymm : StructuralRulesType {ar8}
  tmTran : StructuralRulesType {ar9}

Rules StructuralRules S ar = StructuralRulesType {ar}
Rules StructuralRules T ar = Empty
Rules StructuralRules C ar = Empty
Rules StructuralRules Eq ar = Empty
derivationRule StructuralRules {t = S} (var k) = VarRule k
derivationRule StructuralRules {t = S} conv = ConvRule
derivationRule StructuralRules {t = S} convEq = ConvEqRule
derivationRule StructuralRules {t = S} tyRefl = TyReflRule
derivationRule StructuralRules {t = S} tySymm = TySymmRule
derivationRule StructuralRules {t = S} tyTran = TyTranRule
derivationRule StructuralRules {t = S} tmRefl = TmReflRule
derivationRule StructuralRules {t = S} tmSymm = TmSymmRule
derivationRule StructuralRules {t = S} tmTran = TmTranRule

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


text:
open import Agda.Builtin.Float

_ : Float
_ = 1.0xA

max_forks_repo_name: shlevy/agda


text:
module proofs where

open import univ
open import cwf
open import Base
open import Nat
open import help

{-
lem-id∘ : {Γ Δ : Con}(σ : Γ ─→ Δ) -> id ∘ σ == σ
lem-id∘ (el < σ , pσ >) = eq \x -> ref

lem-∘id : {Γ Δ : Con}(σ : Γ ─→ Δ) -> σ ∘ id == σ
lem-∘id (el < σ , pσ >) = eq \x -> ref

lem-∘assoc : {Γ Δ Θ Ξ : Con}(σ : Θ ─→ Ξ)(δ : Δ ─→ Θ)(θ : Γ ─→ Δ) ->
             (σ ∘ δ) ∘ θ == σ ∘ (δ ∘ θ)
lem-∘assoc (el < σ , pσ >) (el < δ , pδ >) (el < θ , pθ >) = eq \x -> ref
-}

lem-/∘ : {Γ Δ Θ : Con}(A : Type Γ)(σ : Δ ─→ Γ)(δ : Θ ─→ Δ) ->
         A / σ ∘ δ =Ty A / σ / δ
lem-/∘ A (el < _ , _ >) (el < _ , _ >) = eqTy \x -> refS

{-
lem-//id : {Γ : Con}{A : Type Γ}{u : Elem Γ A} -> u // id =El castElem lem-/id u
lem-//id {Γ}{A}{elem (el < u , pu >)} = eqEl (eq prf)
  where
    prf : (x : El Γ) -> _
    prf x =
      chain> u x
         === _ << u (refS << x) by pu (sym (ref<< x))
         === _ << u (refS << x) by pfi _ _ _
      where open module C11 = Chain _==_ (ref {_}) (trans {_})

lem-//∘ : {Γ Δ Θ : Con}{A : Type Γ}(u : Elem Γ A)(σ : Δ ─→ Γ)(δ : Θ ─→ Δ) ->
          u // σ ∘ δ =El castElem (lem-/∘ A σ δ) (u // σ // δ)
lem-//∘ {Γ}{Δ}{Θ} (elem (el < u , pu >)) σ'@(el < σ , _ >) δ'@(el < δ , _ >) = eqEl (eq prf)
  where
    prf : (x : El Θ) -> _
    prf x =
      chain> u (σ (δ x))
         === _ << u (σ (δ (refS << x))) by pu (p─→ σ' (p─→ δ' (sym (ref<< x))))
         === _ << u (σ (δ (refS << x))) by pfi _ _ _
      where open module C12 = Chain _==_ (ref {_}) (trans {_})

lem-wk∘σ,,u : {Γ Δ : Con}{A : Type Γ}(σ : Δ ─→ Γ)(u : Elem Δ (A / σ)) ->
              wk ∘ (σ ,, u) == σ
lem-wk∘σ,,u (el < σ , pσ >) (elem (el < u , pu >)) = eq \x -> ref

lem-/wk∘σ,,u : {Γ Δ : Con}(A : Type Γ)(σ : Δ ─→ Γ)(u : Elem Δ (A / σ)) ->
               A / wk / (σ ,, u) =Ty A / σ
lem-/wk∘σ,,u A (el < σ , pσ >) (elem (el < u , pu >)) = eqTy \x -> refS

lem-vz/σ,,u : {Γ Δ : Con}{A : Type Γ}(σ : Δ ─→ Γ)(u : Elem Δ (A / σ)) ->
              vz // (σ ,, u) =El castElem (lem-/wk∘σ,,u A σ u) u
lem-vz/σ,,u (el < σ , pσ >) (elem (el < u , pu >)) = eqEl (eq \x -> prf x)
  where
    prf : (x : El _) -> u x == _ << u (refS << x)
    prf x =
      chain> u x
         === _ << u (refS << x) by pu (sym (ref<< x))
         === _ << u (refS << x) by pfi _ _ _
      where open module C15 = Chain _==_ (ref {_}) (trans {_})

lem-σ,,u∘ : {Γ Δ Θ : Con}{A : Type Γ}
            (σ : Δ ─→ Γ)(u : Elem Δ (A / σ))(δ : Θ ─→ Δ) ->
            (σ ,, u) ∘ δ == (σ ∘ δ ,, castElem (lem-/∘ A σ δ) (u // δ))
lem-σ,,u∘ (el < σ , _ >) (elem (el < u , pu >)) δ'@(el < δ , _ >) =
  eq \x -> eq < ref , prf x >
  where
    prf : (x : El _) -> u (δ x) == _ << _ << u (δ (refS << x))
    prf x =
      chain> u (δ x)
         === _ << u (δ (refS << x)) by pu (p─→ δ' (sym (ref<< x)))
         === _ << _ << u (δ (refS << x)) by sym (casttrans _ _ _ _)
      where open module C15 = Chain _==_ (ref {_}) (trans {_})

lem-wk,,vz : {Γ : Con}{A : Type Γ} -> (wk ,, vz) == id {Γ , A}
lem-wk,,vz {Γ}{A} = eq prf
  where
    prf : (x : El (Γ , A)) -> _
    prf (el < x , y >) = ref
-}

lem-Π/ : {Γ Δ : Con}{A : Type Γ}(B : Type (Γ , A))(σ : Δ ─→ Γ) ->
         Π A B / σ =Ty Π (A / σ) (B / (σ ∘ wk ,, castElem (lem-/∘ A σ wk) vz))
lem-Π/ B (el < σ , pσ >) =
  eqTy \x -> eqS < refS , (\y -> pFam B (eq < ref , prf x y >)) >
  where
    postulate prf : (x : El _)(y : El _) -> y == _ << _ << _ << _ << y
--     prf x y =
--       chain> y
--          === _ << _ << y           by sym (castref2 _ _ y)
--          === _ << _ << _ << y      by trans<< _ _ _
--          === _ << _ << _ << _ << y by trans<< _ _ _
--       where open module C16 = Chain _==_ (ref {_}) (trans {_})

{-
lem-β : {Γ : Con}{A : Type Γ}{B : Type (Γ , A)}
	(v : Elem (Γ , A) B)(u : Elem Γ A) ->
	(ƛ v) ∙ u =El v // [ u ]
lem-β {Γ}{A}{B} (elem (el < v , pv >)) (elem (el < u , pu >)) = eqEl (eq \x -> prf x _ _)
  where
    prf : (x : El Γ)(q : _ =S _)(p : _ =S _) ->
	  p << v (el < x , u x >) == v (el < x , q << u (refS << x) >)
    prf x q p =
      chain> p << v (el < x , u x >)
	 === p << q0 << v (el < x , q1 << u (refS << x) >)
	  by p<< p (pv (eqSnd (pu (sym (ref<< x)))))
	 === q2 << v (el < x , q1 << u (refS << x) >)
	  by sym (trans<< p q0 _)
	 === q2 << q3 << v (el < x , q << u (refS << x) >)
	  by p<< q2 (pv (eqSnd (pfi q1 q _)))
	 === v (el < x , q << u (refS << x) >)
	  by castref2 q2 q3 _
      where
	open module C17 = Chain _==_ (ref {_}) (trans {_})
	q0 = _
	q1 = _
	q2 = _
	q3 = _

-}


text:
module Prelude.String where

open import Agda.Primitive
open import Prelude.Unit
open import Prelude.Char
open import Prelude.Bool
open import Prelude.Nat
open import Prelude.List
open import Prelude.Maybe
open import Prelude.Equality
open import Prelude.Equality.Unsafe
open import Prelude.Decidable
open import Prelude.Ord
open import Prelude.Function
open import Prelude.Monad
open import Prelude.Semiring

open import Agda.Builtin.String public
open import Agda.Builtin.FromString public

unpackString = primStringToList
packString   = primStringFromList

unpackString-inj : ∀ {x y} → unpackString x ≡ unpackString y → x ≡ y
unpackString-inj {x} p with unpackString x
unpackString-inj refl | ._ = unsafeEqual

infixr 5 _&_
_&_ = primStringAppend

-- Eq --

instance
  EqString : Eq String
  _==_ {{EqString}} x y with primStringEquality x y
  ... | true  = yes unsafeEqual
  ... | false = no  unsafeNotEqual

-- Ord --

instance
  OrdString : Ord String
  OrdString = OrdBy unpackString-inj

  OrdLawsString : Ord/Laws String
  OrdLawsString = OrdLawsBy unpackString-inj

-- Overloaded literals --

instance
  StringIsString : IsString String
  IsString.Constraint StringIsString _ = ⊤
  IsString.fromString StringIsString s = s

  ListIsString : IsString (List Char)
  IsString.Constraint ListIsString _ = ⊤
  IsString.fromString ListIsString s = unpackString s

-- Monoid --

instance
  open import Prelude.Monoid
  SemigroupString : Semigroup String
  _<>_   {{SemigroupString}} = primStringAppend

  MonoidString : Monoid String
  Monoid.super MonoidString = it
  mempty {{MonoidString}} = ""

-- More functions --

parseNat : String → Maybe Nat
parseNat = parseNat′ ∘ unpackString
  where
    pDigit : Char → Maybe Nat
    pDigit c =
      if isDigit c then just (charToNat c - charToNat '0')
                   else nothing

    pNat : Nat → List Char → Maybe Nat
    pNat n [] = just n
    pNat n (c ∷ s) = pDigit c >>= λ d → pNat (n * 10 + d) s

    parseNat′ : List Char → Maybe Nat
    parseNat′ [] = nothing
    parseNat′ (c ∷ s) = pDigit c >>= λ d → pNat d s

onChars : (List Char → List Char) → String → String
onChars f = packString ∘ f ∘ unpackString

words : String → List String
words = map packString ∘ wordsBy isSpace ∘ unpackString

ltrim : String → String
ltrim = onChars (dropWhile isSpace)

rtrim : String → String
rtrim = onChars (reverse ∘ dropWhile isSpace ∘ reverse)

trim : String → String
trim = rtrim ∘ ltrim

strTake : Nat → String → String
strTake n = onChars (take n)

strDrop : Nat → String → String
strDrop n = onChars (drop n)

strLength : String → Nat
strLength = length ∘ unpackString

strIsPrefixOf? : String → String → Bool
strIsPrefixOf? = isPrefixOf? on unpackString

strCommonPrefix : String → String → String
strCommonPrefix s₁ s₂ = packString $ (commonPrefix! on unpackString) s₁ s₂

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
------------------------------------------------------------------------
-- Streams
------------------------------------------------------------------------

module Data.Stream where

open import Coinduction
open import Data.Colist using (Colist; []; _∷_)
open import Data.Vec    using (Vec;    []; _∷_)
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary

------------------------------------------------------------------------
-- The type

infixr 5 _∷_

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

------------------------------------------------------------------------
-- Some operations

head : forall {A} -> Stream A -> A
head (x ∷ xs) = x

tail : forall {A} -> Stream A -> Stream A
tail (x ∷ xs) = ♭ xs

map : ∀ {A B} → (A → B) → Stream A → Stream B
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

zipWith : forall {A B C} ->
          (A -> B -> C) -> Stream A -> Stream B -> Stream C
zipWith _∙_ (x ∷ xs) (y ∷ ys) = (x ∙ y) ∷ ♯ zipWith _∙_ (♭ xs) (♭ ys)

take : ∀ {A} (n : ℕ) → Stream A → Vec A n
take zero    xs       = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)

drop : ∀ {A} -> ℕ -> Stream A -> Stream A
drop zero    xs       = xs
drop (suc n) (x ∷ xs) = drop n (♭ xs)

repeat : forall {A} -> A -> Stream A
repeat x = x ∷ ♯ repeat x

iterate : ∀ {A} → (A → A) → A → Stream A
iterate f x = x ∷ ♯ iterate f (f x)

-- Interleaves the two streams.

infixr 5 _⋎_

_⋎_ : ∀ {A} → Stream A → Stream A → Stream A
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)

toColist : ∀ {A} → Stream A → Colist A
toColist (x ∷ xs) = x ∷ ♯ toColist (♭ xs)

lookup : ∀ {A} → ℕ → Stream A → A
lookup zero    (x ∷ xs) = x
lookup (suc n) (x ∷ xs) = lookup n (♭ xs)

infixr 5 _++_

_++_ : ∀ {A} → Colist A → Stream A → Stream A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)

------------------------------------------------------------------------
-- Equality and other relations

-- xs ≈ ys means that xs and ys are equal.

infix 4 _≈_

data _≈_ {A} : (xs ys : Stream A) → Set where
  _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys

-- x ∈ xs means that x is a member of xs.

infix 4 _∈_

data _∈_ {A : Set} : A → Stream A → Set where
  here  : ∀ {x   xs}                   → x ∈ x ∷ xs
  there : ∀ {x y xs} (x∈xs : x ∈ ♭ xs) → x ∈ y ∷ xs

-- xs ⊑ ys means that xs is a prefix of ys.

infix 4 _⊑_

data _⊑_ {A : Set} : Colist A → Stream A → Set where
  []  : ∀ {ys}                            → []     ⊑ ys
  _∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys

------------------------------------------------------------------------
-- Some proofs

setoid : Set → Setoid
setoid A = record
  { carrier       = Stream A
  ; _≈_           = _≈_ {A}
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≈_
  refl {x ∷ xs} = x ∷ ♯ refl

  sym : Symmetric _≈_
  sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)

  trans : Transitive _≈_
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

map-cong : ∀ {A B} (f : A → B) {xs ys : Stream A} →
           xs ≈ ys → map f xs ≈ map f ys
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

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

open import Data.Nat
open import Data.Vec
open import Data.Fin
open import Data.Product
open import Data.Unit
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Size
open import Codata.Thunk
open import Relation.Binary.PropositionalEquality as ≡

open import is-lib.SInfSys as IS
open import Examples.Lambda.Lambda

module Examples.Lambda.SmallStep where

  U : Set
  U = Term 0 × Term 0

  data SmallStepRN : Set where
    β L-APP R-APP : SmallStepRN

  β-r : FinMetaRule U
  β-r .Ctx = Term 1 × Value
  β-r .comp (t , v) =
    [] ,
    -------------------------
    (app (lambda t) (term v) , subst-0 t (term v))

  l-app-r : FinMetaRule U
  l-app-r .Ctx = Term 0 × Term 0 × Term 0
  l-app-r .comp (t1 , t1' , t2) =
    (t1 , t1') ∷ [] ,
    -------------------------
    ((app t1 t2) , (app t1' t2))

  r-app-r : FinMetaRule U
  r-app-r .Ctx = Value × Term 0 × Term 0
  r-app-r .comp (v , t2 , t2') =
    (t2 , t2') ∷ [] ,
    -------------------------
    ((app (term v) t2) , app (term v) t2')

  SmallStepIS : IS U
  SmallStepIS .Names = SmallStepRN
  SmallStepIS .rules β = from β-r
  SmallStepIS .rules L-APP = from l-app-r
  SmallStepIS .rules R-APP = from r-app-r

  _⇒_ : Term 0 → Term 0 → Set
  t ⇒ t' = Ind⟦ SmallStepIS ⟧ (t , t')

  _⇒*_ : Term 0 → Term 0 → Set
  _⇒*_ = Star _⇒_

  _ConvergesSS : Term 0 → Set
  t ConvergesSS = Σ[ v ∈ Value ] (t ⇒* term v)

  data ⇒∞ : Term 0 → Size → Set where
    step : ∀{t t' i} → t ⇒ t' → Thunk (⇒∞ t') i → ⇒∞ t i

  {- Properties -}
  inj-l-app : ∀{t1 t1'} t2 → t1 ⇒* t1' → (app t1 t2) ⇒* (app t1' t2)
  inj-l-app _ ε = ε
  inj-l-app {t1} t2 (fold x ◅ red) =
    apply-ind L-APP _ (λ {zero → IS.fold x}) ◅ inj-l-app t2 red

  inj-r-app : ∀{t2 t2'} v → t2 ⇒* t2' → (app (term v) t2) ⇒* (app (term v) t2')
  inj-r-app _ ε = ε
  inj-r-app {t2} v (fold x ◅ red) =
    apply-ind R-APP _ (λ {zero → IS.fold x}) ◅ inj-r-app v red

  val-not-reduce⇒ : ∀{v e'} → ¬ (term v ⇒ e')
  val-not-reduce⇒ {lambda _} (fold (β , c , () , pr))
  val-not-reduce⇒ {lambda _} (fold (L-APP , c , () , pr))
  val-not-reduce⇒ {lambda _} (fold (R-APP , c , () , pr))

  ⇒-deterministic : ∀{e e' e''} → e ⇒ e' → e ⇒ e'' → e' ≡ e''
  ⇒-deterministic (fold (β , (_ , lambda _) , refl , _)) (fold (β , (_ , lambda _) , refl , _)) = refl
  ⇒-deterministic (fold (β , (_ , lambda _) , refl , _)) (fold (L-APP , _ , refl , pr)) = ⊥-elim (val-not-reduce⇒ (pr zero))
  ⇒-deterministic (fold (β , (_ , lambda _) , refl , _)) (fold (R-APP , (lambda _ , _) , refl , pr)) = ⊥-elim (val-not-reduce⇒ (pr zero))
  ⇒-deterministic (fold (L-APP , _ , refl , pr)) (fold (β , _ , refl , _)) = ⊥-elim (val-not-reduce⇒ (pr zero))
  ⇒-deterministic (fold (L-APP , _ , refl , pr)) (fold (L-APP , _ , refl , pr')) = cong (λ x → app x _) (⇒-deterministic (pr zero) (pr' zero))
  ⇒-deterministic (fold (L-APP , _ , refl , pr)) (fold (R-APP , _ , refl , _)) = ⊥-elim (val-not-reduce⇒ (pr zero))
  ⇒-deterministic (fold (R-APP , (lambda _ , _) , refl , pr)) (fold (β , _ , refl , _)) = ⊥-elim (val-not-reduce⇒ (pr zero))
  ⇒-deterministic (fold (R-APP , (lambda _ , _) , refl , _)) (fold (L-APP , _ , refl , pr)) = ⊥-elim (val-not-reduce⇒ (pr zero))
  ⇒-deterministic (fold (R-APP , (lambda _ , _) , refl , pr)) (fold (R-APP , (lambda _ , _) , refl , pr')) = cong (λ x → app _ x) (⇒-deterministic (pr zero) (pr' zero))

  ⇒*-preserves-⇒∞ : ∀{e e'} → (∀{i} → ⇒∞ e i) → e ⇒* e' → (∀{i} → ⇒∞ e' i)
  ⇒*-preserves-⇒∞ ss ε = ss
  ⇒*-preserves-⇒∞ ss (x ◅ red-e) with ss
  ⇒*-preserves-⇒∞ ss (x ◅ red-e) | step x₁ x₂ =
    let e'-eq = ⇒-deterministic x₁ x in
    ⇒*-preserves-⇒∞ (≡.subst (λ x → (∀{i} → ⇒∞ x i)) e'-eq (x₂ .force)) red-e

  app-subst-⇒∞ : ∀{e v} → (∀{i} → ⇒∞ (app (lambda e) (term v)) i) → (∀{i} → ⇒∞ (subst-0 e (term v)) i)
  app-subst-⇒∞ ss with ss
  app-subst-⇒∞ {_} {lambda _} ss | step (fold (β , (_ , lambda _) , refl , _)) rec = rec .force
  app-subst-⇒∞ {_} {lambda _} ss | step (fold (L-APP , _ , refl , pr)) _ = ⊥-elim (val-not-reduce⇒ (pr zero))
  app-subst-⇒∞ {_} {lambda _} ss | step (fold (R-APP , (lambda _ , _) , refl , pr)) rec = ⊥-elim (val-not-reduce⇒ (pr zero))

  app-subst-⇒∞₁ : ∀{e1 e1' e2 v} → e1 ⇒* lambda e1' → e2 ⇒* term v → (∀{i} → ⇒∞ (app e1 e2) i) → (∀{i} → ⇒∞ (subst-0 e1' (term v)) i)
  app-subst-⇒∞₁ red-e1 red-e2 ss =
    let red-left = ⇒*-preserves-⇒∞ ss (inj-l-app _ red-e1) in
    let red-right = ⇒*-preserves-⇒∞ red-left (inj-r-app _ red-e2) in
    app-subst-⇒∞ red-right

  not-conv-next : ∀{e e'} → ¬ (Σ[ v ∈ Value ] e ⇒* term v) → e ⇒ e' → ¬ (Σ[ v ∈ Value ] e' ⇒* term v)
  not-conv-next {e} {e'} n ss-e (v , ss-e') = ⊥-elim (n (v , ss-e ◅ ss-e'))

  div-app-l-not-conv : ∀{e1 e2} → (∀{i} → ⇒∞ (app e1 e2) i) → ¬ (e1 ConvergesSS) → (∀{i} → ⇒∞ e1 i)
  div-app-l-not-conv ss n-conv with ss
  div-app-l-not-conv ss n-conv | step (fold (β , _ , refl , _)) _ = ⊥-elim (n-conv (_ , ε))
  div-app-l-not-conv ss n-conv | step (fold (L-APP , _ , refl , pr)) x₁ =
    step (pr zero) λ where .force → div-app-l-not-conv (x₁ .force) (not-conv-next n-conv (pr zero))
  div-app-l-not-conv ss n-conv | step (fold (R-APP , _ , refl , _)) _ = ⊥-elim (n-conv (_ , ε))

  div-app-r-not-conv : ∀{e1 e2 v} → (∀{i} → ⇒∞ (app e1 e2) i) → e1 ⇒* term v → ¬ (e2 ConvergesSS) → (∀{i} → ⇒∞ e2 i)
  div-app-r-not-conv ss red-e1 ¬e2-conv with ss
  div-app-r-not-conv ss red-e1 ¬e2-conv | step (fold (β , _ , refl , _)) _ = ⊥-elim (¬e2-conv (_ , ε))
  div-app-r-not-conv ss ε ¬e2-conv | step (fold (L-APP , _ , refl , pr)) _ = ⊥-elim (val-not-reduce⇒ (pr zero))
  div-app-r-not-conv ss (x ◅ red-e1) ¬e2-conv | step (fold (L-APP , _ , refl , pr)) x₁ =
    div-app-r-not-conv (λ {i} → ≡.subst (λ x → ⇒∞ (app x _) i) (⇒-deterministic (pr zero) x) (x₁ .force)) red-e1 ¬e2-conv
  div-app-r-not-conv ss red-e1 ¬e2-conv | step (fold (R-APP , (lambda _ , _) , refl , pr)) x₁ =
    step (pr zero) λ where .force → div-app-r-not-conv (x₁ .force) red-e1 (not-conv-next ¬e2-conv (pr zero))

  ⇒∞-reduce-⇒ : ∀{e} → (∀{i} → ⇒∞ e i) → Σ[ e' ∈ Term 0 ] e ⇒ e' × (∀{i} → ⇒∞ e' i)
  ⇒∞-reduce-⇒ ss with ss
  ⇒∞-reduce-⇒ ss | step s s' = _ , s , s' .force

  val-not-⇒∞ : ∀{e v} → e ⇒ term v → ¬ (∀{i} → ⇒∞ e i)
  val-not-⇒∞ {e} {v} ss ss' with ss'
  val-not-⇒∞ {.(app (lambda (var zero)) (lambda _))} {lambda _} (fold (β , (var zero , lambda _) , refl , _)) ss' | step (fold (β , (.(var zero) , lambda _) , refl , _)) rec =
    ⊥-elim (val-not-reduce⇒ (proj₁ (proj₂ (⇒∞-reduce-⇒ (rec .force)))))
  val-not-⇒∞ {.(app (lambda (lambda _)) (lambda _))} {lambda _} (fold (β , (lambda _ , lambda _) , refl , _)) ss' | step (fold (β , (.(lambda _) , lambda _) , refl , _)) rec =
    ⊥-elim (val-not-reduce⇒ (proj₁ (proj₂ (⇒∞-reduce-⇒ (rec .force)))))
  val-not-⇒∞ {.(app (lambda e1) e2)} {lambda _} (fold (β , (_ , lambda _) , _)) ss' | step (fold (L-APP , (lambda e1 , e1' , e2) , refl , pr)) rec =
    ⊥-elim (val-not-reduce⇒ (pr zero))
  val-not-⇒∞ {.(app e1 e2)} {lambda _} (fold (L-APP , _ , () , _)) ss' | step (fold (L-APP , (e1 , e1' , e2) , refl , _)) _
  val-not-⇒∞ {.(app e1 e2)} {lambda _} (fold (R-APP , (lambda _ , _) , () , _)) ss' | step (fold (L-APP , (e1 , e1' , e2) , refl , pr)) _
  val-not-⇒∞ {.(app (lambda _) (lambda e2))} {lambda _} (fold (β , (_ , lambda _) , _)) ss' | step (fold (R-APP , (lambda _ , lambda e2 , e2') , refl , pr)) rec =
    ⊥-elim (val-not-reduce⇒ (pr zero))

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

record Sg (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

app : {A : Set} {B : A → Set} → ((x' : A) → B x') → (x : A) → B x
app f x = f x

ppa : {A : Set} {B : A → Set} → (x : A) → ((x' : A) → B x') → B x
ppa x f = f x

postulate
  Bool : Set
  bar : ((Sg Bool (λ _ → Bool)) → Bool) → Bool

foo : Bool
-- foo = app bar (λ (_ , _) → {!!}) -- accepted
foo = ppa (λ (_ , _) → {!!}) bar -- rejected


text:
{-# OPTIONS --safe #-}
module STLC.Syntax where

open import Data.Nat using (ℕ; suc)
open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (Dec; yes; no)

private
  variable
    n : ℕ

data Type : Set where
  _⇒_ : Type → Type → Type
  _×'_ : Type → Type → Type
  unit : Type

data Term : ℕ → Set where
  abs : Type → Term (suc n) → Term n
  app : Term n → Term n → Term n
  var : Fin n → Term n
  ⋆ : Term n
  pair : Term n → Term n → Term n
  projₗ : Term n → Term n
  projᵣ : Term n → Term n

data Ctx : ℕ → Set where
  ● : Ctx 0
  _,-_ : Ctx n → Type → Ctx (suc n)

find : Ctx n → Fin n → Type
find (Γ ,- A) fzero = A
find (Γ ,- A) (fsuc n) = find Γ n

_=?=_ : (x : Type) → (y : Type) → Dec (x ≡ y)
unit      =?= unit        = yes refl
(a ⇒ b)   =?= (c ⇒ d) with a =?= c | b =?= d
... | yes refl | yes refl = yes refl
... | yes refl | no ne    = no λ { refl → ne refl }
... | no ne    | _        = no λ { refl → ne refl }
(a ×' b)  =?= (c ×' d) with a =?= c | b =?= d
... | yes refl | yes refl = yes refl
... | yes refl | no ne    = no λ { refl → ne refl }
... | no ne    | _        = no λ { refl → ne refl }
unit      =?= (_ ×' _)    = no λ ()
unit      =?= (_ ⇒ _)     = no λ ()
(_ ×' _)  =?= unit        = no λ ()
(_ ×' _)  =?= (_ ⇒ _)     = no λ ()
(_ ⇒ _)   =?= unit        = no λ ()
(_ ⇒ _)   =?= (_ ×' _)    = no λ ()

max_stars_repo_name: TrulyNonstrict/STLC

max_issues_repo_name: TrulyNonstrict/STLC

max_forks_repo_name: TrulyNonstrict/STLC


text:
------------------------------------------------------------------------------
-- Totality properties of the gcd
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Partial.TotalityI where

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Induction.NonAcc.LexicographicI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.PropertiesI
open import FOTC.Program.GCD.Partial.ConversionRulesI
open import FOTC.Program.GCD.Partial.Definitions
open import FOTC.Program.GCD.Partial.GCD

------------------------------------------------------------------------------
-- gcd 0 (succ n) is total.
gcd-0S-N : ∀ {n} → N n → N (gcd zero (succ₁ n))
gcd-0S-N {n} Nn = subst N (sym (gcd-0S n)) (nsucc Nn)

------------------------------------------------------------------------------
-- gcd (succ₁ n) 0 is total.
gcd-S0-N : ∀ {n} → N n → N (gcd (succ₁ n) zero)
gcd-S0-N {n} Nn = subst N (sym (gcd-S0 n)) (nsucc Nn)

------------------------------------------------------------------------------
-- gcd (succ₁ m) (succ₁ n) when succ₁ m > succ₁ n is total.
gcd-S>S-N : ∀ {m n} → N m → N n →
            N (gcd (succ₁ m ∸ succ₁ n) (succ₁ n)) →
            succ₁ m > succ₁ n →
            N (gcd (succ₁ m) (succ₁ n))
gcd-S>S-N {m} {n} Nm Nn ih Sm>Sn = subst N (sym (gcd-S>S m n Sm>Sn)) ih

------------------------------------------------------------------------------
-- gcd (succ₁ m) (succ₁ n) when succ₁ m ≯ succ₁ n is total.
gcd-S≯S-N : ∀ {m n} → N m → N n →
            N (gcd (succ₁ m) (succ₁ n ∸ succ₁ m)) →
            succ₁ m ≯ succ₁ n →
            N (gcd (succ₁ m) (succ₁ n))
gcd-S≯S-N {m} {n} Nm Nn ih Sm≯Sn = subst N (sym (gcd-S≯S m n Sm≯Sn)) ih

------------------------------------------------------------------------------
-- gcd m n when m > n is total.
gcd-x>y-N :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → x≢0≢y o p → N (gcd o p)) →
  m > n →
  x≢0≢y m n →
  N (gcd m n)
gcd-x>y-N nzero          Nn             _  0>n   _ = ⊥-elim (0>x→⊥ Nn 0>n)
gcd-x>y-N (nsucc Nm)     nzero          _  _     _ = gcd-S0-N Nm
gcd-x>y-N (nsucc {m} Nm) (nsucc {n} Nn) ah Sm>Sn _ =
  gcd-S>S-N Nm Nn ih Sm>Sn
  where
  -- Inductive hypothesis.
  ih : N (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))
  ih = ah {succ₁ m ∸ succ₁ n}
          {succ₁ n}
          (∸-N (nsucc Nm) (nsucc Nn))
          (nsucc Nn)
          ([Sx∸Sy,Sy]<[Sx,Sy] Nm Nn)
          (λ p → ⊥-elim (S≢0 (∧-proj₂ p)))

------------------------------------------------------------------------------
-- gcd m n when m ≯ n is total.
gcd-x≯y-N :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → x≢0≢y o p → N (gcd o p)) →
  m ≯ n →
  x≢0≢y m n →
  N (gcd m n)
gcd-x≯y-N nzero          nzero          _  _     h = ⊥-elim (h (refl , refl))
gcd-x≯y-N nzero          (nsucc Nn)     _  _     _ = gcd-0S-N Nn
gcd-x≯y-N (nsucc _)      nzero          _  Sm≯0  _ = ⊥-elim (S≯0→⊥ Sm≯0)
gcd-x≯y-N (nsucc {m} Nm) (nsucc {n} Nn) ah Sm≯Sn _ = gcd-S≯S-N Nm Nn ih Sm≯Sn
  where
  -- Inductive hypothesis.
  ih : N (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))
  ih = ah {succ₁ m}
          {succ₁ n ∸ succ₁ m}
          (nsucc Nm)
          (∸-N (nsucc Nn) (nsucc Nm))
          ([Sx,Sy∸Sx]<[Sx,Sy] Nm Nn)
          (λ p → ⊥-elim (S≢0 (∧-proj₁ p)))

------------------------------------------------------------------------------
-- gcd m n when m ≢ 0 and n ≢ 0 is total.
gcd-N : ∀ {m n} → N m → N n → x≢0≢y m n → N (gcd m n)
gcd-N = Lexi-wfind A h
  where
  A : D → D → Set
  A i j = x≢0≢y i j → N (gcd i j)

  h : ∀ {i j} → N i → N j → (∀ {k l} → N k → N l → Lexi k l i j → A k l) →
      A i j
  h Ni Nj ah = case (gcd-x>y-N Ni Nj ah) (gcd-x≯y-N Ni Nj ah) (x>y∨x≯y Ni Nj)


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

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

data D (A : Set) : Set where
  c c' : D A

module M (A : Set) where

  postulate rew : c {A} ≡ c' {A}

  {-# REWRITE rew #-}

  test : ∀ {B} → c {B} ≡ c' {B}
  test = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

syntax QIO

type
  T : 0-ary
  P : 0-ary

term
  new      : P.T  ->  T
  measure  : P  T  T  ->  T
  applyX   : P  P.T  ->  T
  applyI2  : P  P.T  ->  T
  applyDuv : P  P  (P,P).T  ->  T
  applyDu  : P  P.T  ->  T
  applyDv  : P  P.T  ->  T

theory
  (A) a:P   t u:T         |> applyX (a, b.measure(b, t, u)) = measure(a, u, t)
  (B) a:P   b:P  t u:P.T  |> measure(a, applyDu(b, b.t[b]), applyDv(b, b.u[b])) = applyDuv(a, b, a b.measure(a, t[b], u[b]))
  (D) t u:T               |> new(a.measure(a, t, u)) = t
  (E) b:P  t:(P, P).T     |> new(a.applyDuv(a, b, a b. t[a,b])) = applyDu(b, b.new(a.t[a,b]))
-}

module QIO.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 QIO.Signature

private
  variable
    Γ Δ Π : Ctx
    α : QIOT
    𝔛 : Familyₛ

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

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

    new      : QIO T (P ∙ Γ) → QIO T Γ
    measure  : QIO P Γ → QIO T Γ → QIO T Γ → QIO T Γ
    applyX   : QIO P Γ → QIO T (P ∙ Γ) → QIO T Γ
    applyI2  : QIO P Γ → QIO T (P ∙ Γ) → QIO T Γ
    applyDuv : QIO P Γ → QIO P Γ → QIO T (P ∙ P ∙ Γ) → QIO T Γ
    applyDu  : QIO P Γ → QIO T (P ∙ Γ) → QIO T Γ
    applyDv  : QIO P Γ → QIO T (P ∙ Γ) → QIO T Γ

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  QIOᵃ : MetaAlg QIO
  QIOᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (newₒ      ⋮ a)         → new      a
      (measureₒ  ⋮ a , b , c) → measure  a b c
      (applyXₒ   ⋮ a , b)     → applyX   a b
      (applyI2ₒ  ⋮ a , b)     → applyI2  a b
      (applyDuvₒ ⋮ a , b , c) → applyDuv a b c
      (applyDuₒ  ⋮ a , b)     → applyDu  a b
      (applyDvₒ  ⋮ a , b)     → applyDv  a b
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module QIOᵃ = MetaAlg QIOᵃ

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

    open MetaAlg 𝒜ᵃ

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

    𝕤𝕖𝕞 (new      a)     = 𝑎𝑙𝑔 (newₒ      ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (measure  a b c) = 𝑎𝑙𝑔 (measureₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b , 𝕤𝕖𝕞 c)
    𝕤𝕖𝕞 (applyX   a b)   = 𝑎𝑙𝑔 (applyXₒ   ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (applyI2  a b)   = 𝑎𝑙𝑔 (applyI2ₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (applyDuv a b c) = 𝑎𝑙𝑔 (applyDuvₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b , 𝕤𝕖𝕞 c)
    𝕤𝕖𝕞 (applyDu  a b)   = 𝑎𝑙𝑔 (applyDuₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (applyDv  a b)   = 𝑎𝑙𝑔 (applyDvₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ QIOᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ QIO α Γ) → 𝕤𝕖𝕞 (QIOᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (newₒ      ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (measureₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (applyXₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (applyI2ₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (applyDuvₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (applyDuₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (applyDvₒ  ⋮ _) = refl

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

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

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : QIO α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub QIO Π Γ)(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 ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (new a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (measure a b c) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b | 𝕤𝕖𝕞! c = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (applyX a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (applyI2 a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (applyDuv a b c) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b | 𝕤𝕖𝕞! c = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (applyDu a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (applyDv a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩

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

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


text:
module Context where

open import Level using (_⊔_)
open import Function
open import Data.List.Base

-- | `ifix`. Check `docs/fomega/deep-isorecursive/README.md` for details.
{-# NO_POSITIVITY_CHECK #-}
data IFix {ι φ} {I : Set ι} (F : (I -> Set φ) -> I -> Set φ) (i : I) : Set φ where
  Wrap : F (IFix F) i -> IFix F i

infix  3 _∈_ _⊆_
infixl 5 _▻_ _▻▻_ _▶_ _▷_

-- | A context is a snoc-list.
data Con {α} (A : Set α) : Set α where
  ε   : Con A
  _▻_ : (Γ : Con A) -> A -> Con A

-- | The left fold over a context. Note that for contexts, the left fold is the lazy one,
-- i.e. it's preferable.
foldlᶜ : ∀ {α ρ} {A : Set α} {R : Set ρ} -> (R -> A -> R) -> R -> Con A -> R
foldlᶜ f z  ε      = z
foldlᶜ f z (Γ ▻ σ) = f (foldlᶜ f z Γ) σ

-- | Concatenate two contexts.
_▻▻_ : ∀ {α} {A : Set α} -> Con A -> Con A -> Con A
Γ ▻▻ Δ = foldlᶜ _▻_ Γ Δ
{-# DISPLAY foldlᶜ _▻_ Γ Δ = Γ ▻▻ Δ #-}

-- | The right fold over a context. Note that for contexts, the right fold is the strict one,
-- i.e. it's not preferable.
foldrᶜ : ∀ {α ρ} {A : Set α} {R : Set ρ} -> (A -> R -> R) -> R -> Con A -> R
foldrᶜ f z  ε      = z
foldrᶜ f z (Γ ▻ σ) = foldrᶜ f (f σ z) Γ

-- | Mapping over a context.
mapᶜ : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> Con A -> Con B
mapᶜ f = foldlᶜ (λ Ξ x -> Ξ ▻ f x) ε

joinᶜ : ∀ {α} {A : Set α} -> Con (Con A) -> Con A
joinᶜ = foldlᶜ _▻▻_ ε

listToCon : ∀ {α} {A : Set α} -> List A -> Con A
listToCon = foldl _▻_ ε
{-# DISPLAY foldl _▻_ ε = listToCon #-}

-- | A variable is a point in a context.
data _∈_ {α} {A : Set α} σ : Con A -> Set where
  vz  : ∀ {Γ}   -> σ ∈ Γ ▻ σ
  vs_ : ∀ {Γ τ} -> (v : σ ∈ Γ) -> σ ∈ Γ ▻ τ

-- | Expand the context that a variable is defined in, but do not change the variable.
wkᵛ : ∀ {α} {A : Set α} {Γ Δ : Con A} {σ} -> σ ∈ Δ -> σ ∈ Γ ▻▻ Δ
wkᵛ  vz    = vz
wkᵛ (vs v) = vs (wkᵛ v)

-- | A variable in the middle of a context.
vsⁿ : ∀ {α} {A : Set α} {Θ : Con A} {σ} Ξ -> σ ∈ Θ ▻ σ ▻▻ Ξ
vsⁿ  ε      = vz
vsⁿ (Ξ ▻ ν) = vs (vsⁿ Ξ)

mapᵛ : ∀ {α β} {A : Set α} {B : Set β} {Γ σ} {f : A -> B} -> σ ∈ Γ -> f σ ∈ mapᶜ f Γ
mapᵛ  vz    = vz
mapᵛ (vs v) = vs (mapᵛ v)

-- -- | Order-preserving embedding. I.e. in `Γ ⊆ Δ` `Δ` contains the same elements as `Γ` and
-- -- they're in the same order, but there can be additional elements between them.
-- -- See https://fplab.bitbucket.io/posts/2008-03-07-order-preserving-embeddin.html
-- data _⊆_ {α} {A : Set α} : Con A -> Con A -> Set where
--   -- We use this instead of `ε ⊆ ε`, because we this definition we have `idᵒ ∘ᵒ idᵒ ≡ idᵒ`
--   -- definitionally and this is needed in order to type check some terms with open types.
--   stop : ∀ {Γ}     ->                Γ         ⊆ Γ
--   skip : ∀ {Γ Δ σ} -> (ι : Γ ⊆ Δ) -> Γ         ⊆ Δ ▻ σ
--   keep : ∀ {Γ Δ σ} -> (ι : Γ ⊆ Δ) -> Γ ▻ σ     ⊆ Δ ▻ σ

_⊆_ : ∀ {α} {A : Set α} -> Con A -> Con A -> Set α
Γ ⊆ Δ = ∀ {σ} -> σ ∈ Γ -> σ ∈ Δ

stop : ∀ {α} {A : Set α} {Γ : Con A} -> Γ ⊆ Γ
stop = id

dupl : ∀ {α} {A : Set α} {Γ : Con A} {σ} -> Γ ▻ σ ▻ σ ⊆ Γ ▻ σ
dupl  vz    = vz
dupl (vs v) = v

skip : ∀ {α} {A : Set α} {Γ Δ : Con A} {σ} -> Γ ⊆ Δ -> Γ ⊆ Δ ▻ σ
skip ι = vs_ ∘ ι

keep : ∀ {α} {A : Set α} {Γ Δ : Con A} {σ} -> Γ ⊆ Δ -> Γ ▻ σ ⊆ Δ ▻ σ
keep ι  vz    = vz
keep ι (vs v) = vs (ι v)

move : ∀ {α} {A : Set α} {Γ Δ : Con A} {σ} -> Γ ⊆ Δ -> Γ ▻ σ ▻ σ ⊆ Δ ▻ σ
move ι  vz    = vz
move ι (vs v) = keep ι v

skipⁿ : ∀ {α} {A : Set α} {Γ Δ : Con A} Ξ -> Γ ⊆ Δ -> Γ ⊆ Δ ▻▻ Ξ
skipⁿ  ε      ι = ι
skipⁿ (Ξ ▻ ν) ι = skip (skipⁿ Ξ ι)

keepⁿ : ∀ {α} {A : Set α} {Γ Δ : Con A} Ξ -> Γ ⊆ Δ -> Γ ▻▻ Ξ ⊆ Δ ▻▻ Ξ
keepⁿ  ε      ι = ι
keepⁿ (Ξ ▻ ν) ι = keep (keepⁿ Ξ ι)

empᵒ : ∀ {α} {A : Set α} {Γ : Con A} -> ε ⊆ Γ
empᵒ {Γ = ε}     = stop
empᵒ {Γ = Γ ▻ σ} = skip empᵒ

-- | The identity embedding.
idᵒ : ∀ {α} {A : Set α} {Γ : Con A} -> Γ ⊆ Γ
idᵒ = stop

-- | The left extension embedding.
extˡ : ∀ {α} {A : Set α} {Γ Δ : Con A} -> Γ ⊆ Δ ▻▻ Γ
extˡ {Γ = ε}     = empᵒ
extˡ {Γ = Γ ▻ σ} = keep extˡ

-- | The right extension embedding.
extʳ : ∀ {α} {A : Set α} {Γ : Con A} Δ -> Γ ⊆ Γ ▻▻ Δ
extʳ Δ = skipⁿ Δ idᵒ

-- | The one element extension embedding.
topᵒ : ∀ {α} {A : Set α} {Γ : Con A} {σ} -> Γ ⊆ Γ ▻ σ
topᵒ = extʳ (ε ▻ _)

mapᶜ-⊆ : ∀ {α β} {A : Set α} {B : Set β} {Γ Δ} {f : A -> B} -> Γ ⊆ Δ -> mapᶜ f Γ ⊆ mapᶜ f Δ
mapᶜ-⊆ {Γ = ε}     ι  ()
mapᶜ-⊆ {Γ = Γ ▻ σ} ι  vz    = mapᵛ (ι vz)
mapᶜ-⊆ {Γ = Γ ▻ σ} ι (vs v) = mapᶜ-⊆ (ι ∘ vs_) v

-- | Rename a variable.
renᵛ : ∀ {α} {A : Set α} {Γ Δ : Con A} {σ} -> Γ ⊆ Δ -> σ ∈ Γ -> σ ∈ Δ
renᵛ ι = ι

shiftᵛⁿ : ∀ {α} {A : Set α} {Γ : Con A} {σ} Δ -> σ ∈ Γ -> σ ∈ Γ ▻▻ Δ
shiftᵛⁿ Δ = renᵛ (extʳ Δ)

shiftᵛ : ∀ {α} {A : Set α} {Γ : Con A} {σ τ} -> σ ∈ Γ -> σ ∈ Γ ▻ τ
shiftᵛ = shiftᵛⁿ (ε ▻ _)

-- We need both first-order and higher-order environments, because the former are more convenient
-- for compilation and the latter are more convenient for evaluation at the type level.

-- | In `Seq P Γ` there a `P σ` for each `σ` from `Γ`.
data Seq {α π} {A : Set α} (P : A -> Set π) : Con A -> Set π where
  ø   : Seq P ε
  _▶_ : ∀ {σ Γ} -> Seq P Γ -> P σ -> Seq P (Γ ▻ σ)

-- We wrap this in `record` in order to get good inference.
-- | In `Env P Γ` there a `P σ` for each `σ` from `Γ`.
record Env {α π} {A : Set α} (P : A -> Set π) (Γ : Con A) : Set (α ⊔ π) where
  constructor PackEnv
  field unpackEnv : ∀ {σ} -> σ ∈ Γ -> P σ
open Env public

foldlˢ
  : ∀ {α π ρ} {A : Set α} {P : A -> Set π} {Γ}
  -> (R : Con A -> Set ρ) -> (∀ {Ξ σ} -> R Ξ -> P σ -> R (Ξ ▻ σ)) -> R ε -> Seq P Γ -> R Γ
foldlˢ R f z  ø      = z
foldlˢ R f z (ρ ▶ α) = f (foldlˢ R f z ρ) α

-- | Apply a natural transformation to each element of a `Seq`.
mapˢ
  : ∀ {α π₁ π₂} {A : Set α} {P₁ : A -> Set π₁} {P₂ : A -> Set π₂} {Γ}
  -> (∀ {σ} -> P₁ σ -> P₂ σ) -> Seq P₁ Γ -> Seq P₂ Γ
mapˢ f = foldlˢ (Seq _) (λ ρ x -> ρ ▶ f x) ø

mapElˢ
  : ∀ {α π₁ π₂} {A : Set α} {P₁ : A -> Set π₁} {P₂ : A -> Set π₂} {Γ}
  -> (∀ {σ} -> σ ∈ Γ -> P₁ σ -> P₂ σ) -> Seq P₁ Γ -> Seq P₂ Γ
mapElˢ f  ø      = ø
mapElˢ f (ρ ▶ α) = mapElˢ (f ∘ vs_) ρ ▶ f vz α

eraseˢ : ∀ {α π} {A : Set α} {P : Set π} {Γ : Con A} -> Seq (λ _ -> P) Γ -> Con P
eraseˢ = foldlˢ _ _▻_ ε

∅ : ∀ {α π} {A : Set α} {P : A -> Set π} -> Env P ε
∅ = PackEnv λ()

_▷_ : ∀ {α π} {A : Set α} {Γ σ} {P : A -> Set π} -> Env P Γ -> P σ -> Env P (Γ ▻ σ)
PackEnv ρ ▷ α = PackEnv λ
  {  vz    -> α
  ; (vs v) -> ρ v
  }

_∘ᵉ_ : ∀ {α π} {A : Set α} {Γ Δ} {P : A -> Set π} -> Env P Δ -> Γ ⊆ Δ -> Env P Γ
PackEnv ρ ∘ᵉ ι = PackEnv (ρ ∘ ι)

withSplitᵉ
  : ∀ {α π ρ} {A : Set α} {Γ σ} {P : A -> Set π} {R : Set ρ}
  -> Env P (Γ ▻ σ) -> (Env P Γ -> P σ -> R) -> R
withSplitᵉ (PackEnv ρ) k = k (PackEnv (ρ ∘ vs_)) (ρ vz)

foldlᵉ
  : ∀ {α π ρ} {A : Set α} {P : A -> Set π} {Γ}
  -> (R : Con A -> Set ρ) -> (∀ {Ξ σ} -> R Ξ -> P σ -> R (Ξ ▻ σ)) -> R ε -> Env P Γ -> R Γ
foldlᵉ {Γ = ε}     R f z ρ = z
foldlᵉ {Γ = Γ ▻ σ} R f z ρ = withSplitᵉ ρ λ ρ′ α -> f (foldlᵉ R f z ρ′) α

-- | Apply a natural transformation to each element of a `Env`.
mapᵉ
  : ∀ {α π₁ π₂} {A : Set α} {P₁ : A -> Set π₁} {P₂ : A -> Set π₂} {Γ}
  -> (∀ {σ} -> P₁ σ -> P₂ σ) -> Env P₁ Γ -> Env P₂ Γ
mapᵉ f = foldlᵉ (Env _) (λ ρ x -> ρ ▷ f x) ∅

mapElᵉ
  : ∀ {α π₁ π₂} {A : Set α} {P₁ : A -> Set π₁} {P₂ : A -> Set π₂} {Γ}
  -> (∀ {σ} -> σ ∈ Γ -> P₁ σ -> P₂ σ) -> Env P₁ Γ -> Env P₂ Γ
mapElᵉ f (PackEnv ρ) = PackEnv λ v -> f v (ρ v)

-- | Look up a variable in an environment.
lookupᵉ : ∀ {α π} {A : Set α} {P : A -> Set π} {Γ σ} -> σ ∈ Γ -> Env P Γ -> P σ
lookupᵉ v (PackEnv ρ) = ρ v

eraseᵉ : ∀ {α π} {A : Set α} {P : Set π} {Γ : Con A} -> Env (λ _ -> P) Γ -> Con P
eraseᵉ = foldlᵉ _ _▻_ ε

record Environment {α β} {A : Set α} (_◆_ : Con A -> A -> Set β) : Set (α ⊔ β) where
  infix 3 _⊢ᵉ_

  field
    varᵈ : ∀ {Γ σ} -> σ ∈ Γ -> Γ ◆ σ
    renᵈ : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ ◆ σ -> Δ ◆ σ

  idᵉ : ∀ {Γ} -> Env (Γ ◆_) Γ
  idᵉ = PackEnv varᵈ

  freshᵉ : ∀ {Γ σ} -> (Γ ▻ σ) ◆ σ
  freshᵉ = varᵈ vz

  _⊢ᵉ_ : Con A -> Con A -> Set (α ⊔ β)
  Ξ ⊢ᵉ Θ = Env (λ σ -> Ξ ◆ σ) Θ

  renᵉ : ∀ {Δ Ξ Γ} -> Δ ⊆ Ξ -> Δ ⊢ᵉ Γ -> Ξ ⊢ᵉ Γ
  renᵉ ι (PackEnv ρ) = PackEnv $ renᵈ ι ∘ ρ

  keepᵉ : ∀ {Δ Γ σ} -> Δ ⊢ᵉ Γ -> Δ ▻ σ ⊢ᵉ Γ ▻ σ
  keepᵉ ρ = renᵉ topᵒ ρ ▷ freshᵉ

  topᵉ : ∀ {Γ σ} -> Γ ◆ σ -> Γ ⊢ᵉ Γ ▻ σ
  topᵉ t = idᵉ ▷ t

  shiftᵉ : ∀ {Δ Γ τ} -> Δ ⊢ᵉ Γ -> Δ ▻ τ ⊢ᵉ Γ
  shiftᵉ = renᵉ topᵒ

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Limits.Terminal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.PropositionalTruncation.Base

open import Cubical.Data.Sigma

open import Cubical.Categories.Category

private
  variable
    ℓ ℓ' : Level

module _ (C : Category ℓ ℓ') where
  open Category C

  isTerminal : (x : ob) → Type (ℓ-max ℓ ℓ')
  isTerminal x = ∀ (y : ob) → isContr (C [ y , x ])

  Terminal : Type (ℓ-max ℓ ℓ')
  Terminal = Σ[ x ∈ ob ] isTerminal x

  terminalOb : Terminal → ob
  terminalOb = fst

  terminalArrow : (T : Terminal) (y : ob) → C [ y , terminalOb T ]
  terminalArrow T y = T .snd y .fst

  terminalArrowUnique : {T : Terminal} {y : ob} (f : C [ y , terminalOb T ])
                      → terminalArrow T y ≡ f
  terminalArrowUnique {T} {y} f = T .snd y .snd f

  terminalEndoIsId : (T : Terminal) (f : C [ terminalOb T , terminalOb T ])
                   → f ≡ id
  terminalEndoIsId T f = isContr→isProp (T .snd (terminalOb T)) f id

  hasTerminal : Type (ℓ-max ℓ ℓ')
  hasTerminal = ∥ Terminal ∥₁

  -- Terminality of an object is a proposition.
  isPropIsTerminal : (x : ob) → isProp (isTerminal x)
  isPropIsTerminal _ = isPropΠ λ _ → isPropIsContr

  open CatIso

  -- Objects that are initial are isomorphic.
  terminalToIso : (x y : Terminal) → CatIso C (terminalOb x) (terminalOb y)
  mor (terminalToIso x y) = terminalArrow y (terminalOb x)
  inv (terminalToIso x y) = terminalArrow x (terminalOb y)
  sec (terminalToIso x y) = terminalEndoIsId y _
  ret (terminalToIso x y) = terminalEndoIsId x _

  open isUnivalent

  -- The type of terminal objects of a univalent category is a proposition,
  -- i.e. all terminal objects are equal.
  isPropTerminal : (hC : isUnivalent C) → isProp Terminal
  isPropTerminal hC x y =
    Σ≡Prop isPropIsTerminal (CatIsoToPath hC (terminalToIso x y))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K #-}
module Simplify where

open import FT
open import HoTT

-- just flip.  It is he caller's responsibility to do other things
flip : {b₁ b₂ : FT} → b₂ ⇛ b₁ → b₁ ⇛ b₂
flip unite₊⇛ = uniti₊⇛
flip uniti₊⇛ = unite₊⇛
flip swap₊⇛ = swap₊⇛
flip assocl₊⇛ = assocr₊⇛
flip assocr₊⇛ = assocl₊⇛
flip unite⋆⇛ = uniti⋆⇛
flip uniti⋆⇛ = unite⋆⇛
flip swap⋆⇛ = swap⋆⇛
flip assocl⋆⇛ = assocr⋆⇛
flip assocr⋆⇛ = assocl⋆⇛
flip distz⇛ = factorz⇛
flip factorz⇛ = distz⇛
flip dist⇛ = factor⇛
flip factor⇛ = dist⇛
flip id⇛ = id⇛
flip (sym⇛ p) = p
flip (p ◎ q) = flip q ◎ flip p
flip (p ⊕ q) = flip p ⊕ flip q
flip (p ⊗ q) = flip p ⊗ flip q

flip-id-lemma : ∀ {b} → flip {b} {b} id⇛ ≡ id⇛
flip-id-lemma = λ {b} → refl id⇛

-- we're going to be pretty brute-force about this, for now
-- All this is going to be one huge mutual definition.
mutual
  simplify : {b₁ b₂ : FT} → b₁ ⇛ b₂ → b₁ ⇛ b₂
  -- all the basic (atomic) combinators simplify to themselves
  simplify unite₊⇛ = unite₊⇛
  simplify uniti₊⇛ = uniti₊⇛
  simplify swap₊⇛ = swap₊⇛
  simplify assocl₊⇛ = assocl₊⇛
  simplify assocr₊⇛ = assocr₊⇛
  simplify unite⋆⇛ = unite⋆⇛
  simplify uniti⋆⇛ = uniti⋆⇛
  simplify swap⋆⇛ = swap⋆⇛
  simplify assocl⋆⇛ = assocl⋆⇛
  simplify assocr⋆⇛ = assocr⋆⇛
  simplify distz⇛ = distz⇛
  simplify factorz⇛ = factorz⇛
  simplify dist⇛ = dist⇛
  simplify factor⇛ = factor⇛
  simplify id⇛ = id⇛
  simplify (sym⇛ p) = flip (simplify p)
  simplify (p ◎ q) = scomp (simplify p)  (simplify q)
  simplify (p ⊕ q) = simplify p ⊕ simplify q
  simplify (p ⊗ q) = simplify p ⊗ simplify q

  -- split on p, and then only on those q that we want to simplify
  scomp : {b₁ b₂ b₃ : FT} → b₁ ⇛ b₂ → b₂ ⇛ b₃ → b₁ ⇛ b₃
  scomp id⇛ p = p
  scomp unite₊⇛ id⇛ = unite₊⇛
  scomp unite₊⇛ uniti₊⇛ = id⇛
  scomp unite₊⇛ q = unite₊⇛ ◎ q -- more?
  scomp uniti₊⇛ unite₊⇛ = id⇛
  scomp uniti₊⇛ id⇛ = uniti₊⇛
  scomp uniti₊⇛ q = uniti₊⇛ ◎ q
  scomp swap₊⇛ swap₊⇛ = id⇛
  scomp swap₊⇛ id⇛ = swap₊⇛
  scomp swap₊⇛ (q ◎ q₁) = scomp swap₊⇛ q ◎ q₁
  scomp swap₊⇛ q = swap₊⇛ ◎ q
  scomp assocl₊⇛ assocr₊⇛ = id⇛
  scomp assocl₊⇛ id⇛ = assocl₊⇛
  scomp assocl₊⇛ q = assocl₊⇛ ◎ q
  scomp assocr₊⇛ assocl₊⇛ = id⇛
  scomp assocr₊⇛ id⇛ = assocr₊⇛
  scomp assocr₊⇛ q = assocr₊⇛ ◎ q
  scomp unite⋆⇛ uniti⋆⇛ = id⇛
  scomp unite⋆⇛ id⇛ = unite⋆⇛
  scomp unite⋆⇛ q = unite⋆⇛ ◎ q
  scomp uniti⋆⇛ unite⋆⇛ = id⇛
  scomp uniti⋆⇛ id⇛ = uniti⋆⇛
  scomp uniti⋆⇛ q = uniti⋆⇛ ◎ q
  scomp swap⋆⇛ swap⋆⇛ = id⇛
  scomp swap⋆⇛ id⇛ = swap⋆⇛
  scomp swap⋆⇛ q = swap⋆⇛ ◎ q
  scomp assocl⋆⇛ assocr⋆⇛ = id⇛
  scomp assocl⋆⇛ id⇛ = assocl⋆⇛
  scomp assocl⋆⇛ q = assocl⋆⇛ ◎ q
  scomp assocr⋆⇛ assocl⋆⇛ = id⇛
  scomp assocr⋆⇛ id⇛ = assocr⋆⇛
  scomp assocr⋆⇛ q = assocr⋆⇛ ◎ q
  scomp distz⇛ id⇛ = distz⇛
  scomp distz⇛ q = distz⇛ ◎ q
  scomp factorz⇛ distz⇛ = id⇛
  scomp factorz⇛ id⇛ = factorz⇛
  scomp factorz⇛ q = factorz⇛ ◎ q
  scomp dist⇛ q = dist⇛ ◎ q -- Can't simplify?
  scomp factor⇛ dist⇛ = id⇛
  scomp factor⇛ id⇛ = factor⇛
  scomp factor⇛ q = factor⇛ ◎ q
  scomp (sym⇛ p) q = (flip p) ◎ q -- won't happen from simplify
  scomp (p₁ ◎ p₂) id⇛ = scomp p₁ p₂
  scomp (p₁ ◎ p₂) q = scomp p₁ p₂ ◎ q
  scomp (p₁ ⊕ p₂) id⇛ = p₁ ⊕ p₂
  scomp (p₁ ⊕ p₂) (q₁ ⊕ q₂) = scomp p₁ q₁ ⊕ scomp p₂ q₂
  scomp (p₁ ⊕ p₂) q = (p₁ ⊕ p₂) ◎ q
  scomp (p₁ ⊗ p₂) id⇛ = p₁ ⊗ p₂
  scomp (p₁ ⊗ p₂) (q ◎ q₁) = scomp (p₁ ⊗ p₂) q ◎ q₁
  scomp (p₁ ⊗ p₂) (q ⊗ q₁) = scomp p₁ q ⊗ scomp p₂ q₁
  scomp (p₁ ⊗ p₂) q = (p₁ ⊗ p₂) ◎ q

-- testing
test1 : ∀ {b₁ : FT} → b₁ ⇛ b₁
test1 = simplify (id⇛ ◎ id⇛ ◎ id⇛)

test2 : ∀ {b₁ : FT} → TIMES ONE b₁ ⇛ TIMES ONE b₁
test2 = simplify ((sym⇛ uniti⋆⇛) ◎ id⇛ ◎ uniti⋆⇛)

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Prelude
open import dynamics-core

module lemmas-ground where
  -- not ground types aren't just a type constructor filled with holes
  ground-not-holes : ∀{τ} →
                     (τ ground → ⊥) →
                     (τ ≠ (⦇-⦈ ==> ⦇-⦈)) × (τ ≠ (⦇-⦈ ⊕ ⦇-⦈)) × (τ ≠ (⦇-⦈ ⊠ ⦇-⦈))
  ground-not-holes notg = (λ{refl → notg GArrHole}) ,
                          (λ{refl → notg GSumHole}) ,
                          (λ{refl → notg GProdHole})

  -- not ground types either have to be hole, an arrow, or a sum
  not-ground : ∀{τ} →
              (τ ground → ⊥) →
              ((τ == ⦇-⦈) +
               (Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] (τ == (τ1 ==> τ2))) +
               (Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] (τ == (τ1 ⊕ τ2))) +
               (Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] (τ == (τ1 ⊠ τ2))))
  not-ground {num} gnd = abort (gnd GNum)
  not-ground {⦇-⦈} gnd = Inl refl
  not-ground {τ ==> τ₁} gnd = Inr (Inl (τ , τ₁ , refl))
  not-ground {τ ⊕ τ₁} gnd = Inr (Inr (Inl (τ , τ₁ , refl)))
  not-ground {τ ⊠ τ₁} gnd = Inr (Inr (Inr (τ , τ₁ , refl)))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module _ where

open import utility
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Environment as Env
open import Esterel.Context
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import calculus
open import context-properties
open import Esterel.Lang.Binding

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module ShowNat where

open import IO
open import Data.Unit
open import Data.Nat.Show
open import Level using (0ℓ)

main = run {0ℓ} (putStrLn (Data.Nat.Show.show 10))

max_stars_repo_name: guilhermehas/agda

max_issues_repo_name: guilhermehas/agda

max_forks_repo_name: guilhermehas/agda


text:
module Avionics.SafetyEnvelopes.ExtInterface where

open import Data.Bool using (Bool)
open import Data.Float using (Float)
open import Data.List using (List; map)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Product using (_×_; _,_)

open import Avionics.Probability using (Dist; NormalDist; ND)
open import Avionics.Real renaming (fromFloat to ff; toFloat to tf)
open import Avionics.SafetyEnvelopes using (z-predictable'; sample-z-predictable)

open import ExtInterface.Data.Maybe using (just; nothing) renaming (Maybe to ExtMaybe)
open import ExtInterface.Data.Product as Ext using (⟨_,_⟩)

fromFloats-z-predictable : List (Float Ext.× Float) → Float → Float → ExtMaybe (Float Ext.× Bool)
fromFloats-z-predictable means×stds z x =
    let
      ndists = map (λ{⟨ mean , std ⟩ → ND (ff mean) (ff std)}) means×stds
      (m , b) = z-predictable' ndists (ff z) (ff x)
    in
      just ⟨ tf m , b ⟩
{-# COMPILE GHC fromFloats-z-predictable as zPredictable #-}

fromFloats-sample-z-predictable :
    List (Float Ext.× Float)
    → Float → Float → List Float → ExtMaybe (Float Ext.× Float Ext.× Bool)
fromFloats-sample-z-predictable means×stds zμ zσ xs =
    let
      ndists = map (λ{⟨ mean , std ⟩ → ND (ff mean) (ff std)}) means×stds
    in
      return (sample-z-predictable ndists (ff zμ) (ff zσ) (map ff xs))
  where
    return : Maybe (ℝ × ℝ × Bool) → ExtMaybe (Float Ext.× Float Ext.× Bool)
    return nothing = nothing
    return (just (m' , v' , b)) = just ⟨ tf m' , ⟨ tf v' , b ⟩ ⟩
{-# COMPILE GHC fromFloats-sample-z-predictable as sampleZPredictable #-}

max_stars_repo_name: RPI-WCL/safety-envelopes-sentinels

max_issues_repo_name: RPI-WCL/safety-envelopes-sentinels

max_forks_repo_name: RPI-WCL/safety-envelopes-sentinels


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

open import Level

open import Categories.Category
open import Categories.Functor hiding (_≡_; assoc; identityˡ; identityʳ)
open import Categories.NaturalTransformation renaming (id to idN)

record Monad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  field
    F : Endofunctor C
    η : NaturalTransformation id F
    μ : NaturalTransformation (F ∘ F) F

  open Functor F

  field
    .assoc     : μ ∘₁ (F ∘ˡ μ) ≡ μ ∘₁ (μ ∘ʳ F)
    .identityˡ : μ ∘₁ (F ∘ˡ η) ≡ idN
    .identityʳ : μ ∘₁ (η ∘ʳ F) ≡ idN


text:
module Cats.Category.Lift where

open import Relation.Binary using (IsEquivalence)
open import Level as L using (Level ; suc ; _⊔_ ; lift ; lower)

open import Cats.Category.Base

open IsEquivalence

LCategory : (l : Level) → Set (suc l)
LCategory l = Category l l l

Lift : ∀ {lo la l≈ lo′ la′ l≈′} → Category lo la l≈
  → Category (lo ⊔ lo′) (la ⊔ la′) (l≈ ⊔ l≈′)
Lift {lo′ = lo′} {la′} {l≈′} C = record
    { Obj = L.Lift lo′ C.Obj
    ; _⇒_ = λ A B → L.Lift la′ (lower A C.⇒ lower B)
    ; _≈_ = λ f g → L.Lift l≈′ (lower f C.≈ lower g)
    ; id = lift C.id
    ; _∘_ = λ f g → lift (lower f C.∘ lower g)
    ; equiv = record
        { refl = lift (refl C.equiv)
        ; sym = λ eq → lift (sym C.equiv (lower eq))
        ; trans = λ eq₁ eq₂ → lift (trans C.equiv (lower eq₁) (lower eq₂))
        }
    ; ∘-resp = λ eq₁ eq₂ → lift (C.∘-resp (lower eq₁) (lower eq₂))
    ; id-r = lift C.id-r
    ; id-l = lift C.id-l
    ; assoc = lift C.assoc
    }
  where
    module C = Category C

LiftEq : ∀ {lo la l≈} → Category lo la l≈
  → LCategory (lo ⊔ la ⊔ l≈)
LiftEq {lo} {la} {l≈} = Lift {lo′ = la ⊔ l≈} {la′ = lo ⊔ l≈} {l≈′ = lo ⊔ la}

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


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

open import Categories.Category

module Categories.Category.Instance.Simplex where

open import Level
open import Data.Product
open import Data.Fin.Base using (Fin; _≤_)
open import Data.Nat.Base using (ℕ; z≤n; s≤s)
open import Function renaming (id to idF; _∘_ to _∙_)

open import Relation.Binary using (_=[_]⇒_)
open import Relation.Binary.PropositionalEquality

Δ : Category 0ℓ 0ℓ 0ℓ
Δ = record
  { Obj       = ℕ
  ; _⇒_       = λ m n → Σ (Fin m → Fin n) (λ f → _≤_ =[ f ]⇒ _≤_)
  ; _≈_       = λ { (f , mf) (g , mg) → ∀ x → f x ≡ g x }
  ; id        = idF , idF
  ; _∘_       = λ { (f , mf) (g , mg) → f ∙ g , mf ∙ mg }
  ; assoc     = λ _ → refl
  ; sym-assoc = λ _ → refl
  ; identityˡ = λ _ → refl
  ; identityʳ = λ _ → refl
  ; identity² = λ _ → refl
  ; equiv     = record
    { refl  = λ _ → refl
    ; sym   = λ eq x → sym (eq x)
    ; trans = λ eq₁ eq₂ x → trans (eq₁ x) (eq₂ x)
    }
  ; ∘-resp-≈  = λ {_ _ _ f g h i} eq₁ eq₂ x → trans (cong (λ t → proj₁ f t) (eq₂ x)) (eq₁ (proj₁ i x))
  }

open Category Δ

--------------------------------------------------------------------------------
-- Face + Degeneracy Maps

face-map : ∀ {n} → Fin (ℕ.suc n) → Fin n → Fin (ℕ.suc n)
face-map Fin.zero    k           = Fin.suc k
face-map (Fin.suc i) Fin.zero    = Fin.zero
face-map (Fin.suc i) (Fin.suc k) = Fin.suc (face-map i k)

face-mono : ∀ {n} → (i : Fin (ℕ.suc n)) → _≤_ =[ face-map i ]⇒ _≤_
face-mono Fin.zero    {_}         {_}         le       = s≤s le
face-mono (Fin.suc i) {Fin.zero}  {_}         _        = z≤n
face-mono (Fin.suc i) {Fin.suc _} {Fin.suc _} (s≤s le) = s≤s (face-mono i le)

face : ∀ {n} → Fin (ℕ.suc n) → n ⇒ ℕ.suc n
face i = face-map i , face-mono i

degeneracy-map : ∀ {n} → Fin n → Fin (ℕ.suc n) → Fin n
degeneracy-map Fin.zero    Fin.zero    = Fin.zero
degeneracy-map Fin.zero    (Fin.suc k) = k
degeneracy-map (Fin.suc i) Fin.zero    = Fin.zero
degeneracy-map (Fin.suc i) (Fin.suc k) = Fin.suc (degeneracy-map i k)

degeneracy-mono : ∀ {n} → (i : Fin n) → _≤_ =[ degeneracy-map i ]⇒ _≤_
degeneracy-mono Fin.zero    {Fin.zero}  {_}         _        = z≤n
degeneracy-mono Fin.zero    {Fin.suc _} {Fin.suc _} (s≤s le) = le
degeneracy-mono (Fin.suc i) {Fin.zero}  {_}         _        = z≤n
degeneracy-mono (Fin.suc i) {Fin.suc _} {Fin.suc _} (s≤s le) = s≤s (degeneracy-mono i le)

degeneracy : ∀ {n} → Fin n → ℕ.suc n ⇒ n
degeneracy i = degeneracy-map i , degeneracy-mono i

max_stars_repo_name: jaykru/agda-categories

max_issues_repo_name: jaykru/agda-categories

max_forks_repo_name: jaykru/agda-categories


text:
-- Andreas, AIM XXIII, 2016-04-23
-- Issue 1944
-- Milestone 2.0: overload projection by fields (does not affect matching)

-- {-# OPTIONS -v tc.lhs.split:20 #-}

record R : Set2 where
  field out : Set1

r : R
R.out r = Set

s = r

open R r  -- fully applied open
open R
open R s

-- Now out is overloaded.  It is both a field and a projection.
-- We can still use it in pattern position (since a field does not make sense here).

ok : R
out ok = Set  -- out should be highlighted as projection

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module neq where

open import eq
open import negation

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infix 4 _≢_

----------------------------------------------------------------------
-- defined types
----------------------------------------------------------------------

_≢_ : ∀ {ℓ}{A : Set ℓ} → A → A → Set ℓ
x ≢ y = ¬ (x ≡ y)

sym-≢ : ∀{ℓ}{A : Set ℓ}{x y : A} → x ≢ y → y ≢ x
sym-≢ p₁ p₂ = p₁ (sym p₂)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Product of two functors
{-# OPTIONS --safe #-}

module Cubical.Categories.Functor.BinProduct where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Constructions.BinProduct
open import Cubical.Categories.Functor.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Prelude

private
  variable
    ℓA ℓA' ℓB ℓB' ℓC ℓC' ℓD ℓD' : Level
    A : Category ℓA ℓA'
    B : Category ℓB ℓB'
    C : Category ℓC ℓC'
    D : Category ℓD ℓD'

open Functor

_×F_ : Functor A C → Functor B D → Functor (A × B) (C × D)
(G ×F H) .F-ob (a , b) = (G ⟅ a ⟆ , H ⟅ b ⟆)
(G ×F H) .F-hom (g , h) = (G ⟪ g ⟫ , H ⟪ h ⟫)
(G ×F H) .F-id = ≡-× (G .F-id) (H .F-id)
(G ×F H) .F-seq _ _ = ≡-× (G .F-seq _ _) (H .F-seq _ _)

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous equality
------------------------------------------------------------------------

module Relation.Binary.HeterogeneousEquality where

open import Data.Product
open import Function
open import Function.Inverse using (Inverse)
open import Data.Unit.Core
open import Level
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.Indexed as I using (_at_)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

import Relation.Binary.HeterogeneousEquality.Core as Core

------------------------------------------------------------------------
-- Heterogeneous equality

infix 4 _≇_

open Core public using (_≅_; refl)

-- Nonequality.

_≇_ : ∀ {ℓ} {A : Set ℓ} → A → {B : Set ℓ} → B → Set ℓ
x ≇ y = ¬ x ≅ y

------------------------------------------------------------------------
-- Conversion

≡-to-≅ : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≅ y
≡-to-≅ refl = refl

open Core public using (≅-to-≡)

------------------------------------------------------------------------
-- Some properties

reflexive : ∀ {a} {A : Set a} → _⇒_ {A = A} _≡_ (λ x y → x ≅ y)
reflexive refl = refl

sym : ∀ {ℓ} {A B : Set ℓ} {x : A} {y : B} → x ≅ y → y ≅ x
sym refl = refl

trans : ∀ {ℓ} {A B C : Set ℓ} {x : A} {y : B} {z : C} →
        x ≅ y → y ≅ z → x ≅ z
trans refl eq = eq

subst : ∀ {a} {A : Set a} {p} → Substitutive {A = A} (λ x y → x ≅ y) p
subst P refl p = p

subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
         ∀ {x₁ x₂ y₁ y₂} → x₁ ≅ x₂ → y₁ ≅ y₂ → P x₁ y₁ → P x₂ y₂
subst₂ P refl refl p = p

subst-removable : ∀ {a p} {A : Set a}
                  (P : A → Set p) {x y} (eq : x ≅ y) z →
                  subst P eq z ≅ z
subst-removable P refl z = refl

≡-subst-removable : ∀ {a p} {A : Set a}
                    (P : A → Set p) {x y} (eq : x ≡ y) z →
                    P.subst P eq z ≅ z
≡-subst-removable P refl z = refl

cong : ∀ {a b} {A : Set a} {B : A → Set b} {x y}
       (f : (x : A) → B x) → x ≅ y → f x ≅ f y
cong f refl = refl

cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
           f ≅ g → (x : A) → f x ≅ g x
cong-app refl x = refl

cong₂ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c}
          {x y u v}
        (f : (x : A) (y : B x) → C x y) → x ≅ y → u ≅ v → f x u ≅ f y v
cong₂ f refl refl = refl

resp₂ : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) → ∼ Respects₂ (λ x y → x ≅ y)
resp₂ _∼_ = subst⟶resp₂ _∼_ subst

proof-irrelevance : ∀ {ℓ} {A B : Set ℓ} {x : A} {y : B}
                    (p q : x ≅ y) → p ≡ q
proof-irrelevance refl refl = refl

isEquivalence : ∀ {a} {A : Set a} →
                IsEquivalence {A = A} (λ x y → x ≅ y)
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

setoid : ∀ {a} → Set a → Setoid _ _
setoid A = record
  { Carrier       = A
  ; _≈_           = λ x y → x ≅ y
  ; isEquivalence = isEquivalence
  }

indexedSetoid : ∀ {a b} {A : Set a} → (A → Set b) → I.Setoid A _ _
indexedSetoid B = record
  { Carrier       = B
  ; _≈_           = λ x y → x ≅ y
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }

≡↔≅ : ∀ {a b} {A : Set a} (B : A → Set b) {x : A} →
      Inverse (P.setoid (B x)) (indexedSetoid B at x)
≡↔≅ B = record
  { to         = record { _⟨$⟩_ = id; cong = ≡-to-≅ }
  ; from       = record { _⟨$⟩_ = id; cong = ≅-to-≡ }
  ; inverse-of = record
    { left-inverse-of  = λ _ → refl
    ; right-inverse-of = λ _ → refl
    }
  }

decSetoid : ∀ {a} {A : Set a} →
            Decidable {A = A} {B = A} (λ x y → x ≅ y) →
            DecSetoid _ _
decSetoid dec = record
  { _≈_              = λ x y → x ≅ y
  ; isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = dec
      }
  }

isPreorder : ∀ {a} {A : Set a} →
             IsPreorder {A = A} (λ x y → x ≅ y) (λ x y → x ≅ y)
isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = id
  ; trans         = trans
  }

isPreorder-≡ : ∀ {a} {A : Set a} →
               IsPreorder {A = A} _≡_ (λ x y → x ≅ y)
isPreorder-≡ = record
  { isEquivalence = P.isEquivalence
  ; reflexive     = reflexive
  ; trans         = trans
  }

preorder : ∀ {a} → Set a → Preorder _ _ _
preorder A = record
  { Carrier    = A
  ; _≈_        = _≡_
  ; _∼_        = λ x y → x ≅ y
  ; isPreorder = isPreorder-≡
  }

------------------------------------------------------------------------
-- Convenient syntax for equational reasoning

module ≅-Reasoning where

  -- The code in Relation.Binary.EqReasoning cannot handle
  -- heterogeneous equalities, hence the code duplication here.

  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≅⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
  infix  1 begin_

  data _IsRelatedTo_ {ℓ} {A : Set ℓ} (x : A) {B : Set ℓ} (y : B) :
                     Set ℓ where
    relTo : (x≅y : x ≅ y) → x IsRelatedTo y

  begin_ : ∀ {ℓ} {A : Set ℓ} {x : A} {B} {y : B} →
           x IsRelatedTo y → x ≅ y
  begin relTo x≅y = x≅y

  _≅⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} {C} {z : C} →
           x ≅ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z)

  _≡⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {y C} {z : C} →
           x ≡ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≡⟨ x≡y ⟩ relTo y≅z = relTo (trans (reflexive x≡y) y≅z)

  _≡⟨⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} →
          x IsRelatedTo y → x IsRelatedTo y
  _ ≡⟨⟩ x≅y = x≅y

  _∎ : ∀ {a} {A : Set a} (x : A) → x IsRelatedTo x
  _∎ _ = relTo refl

------------------------------------------------------------------------
-- Functional extensionality

-- A form of functional extensionality for _≅_.

Extensionality : (a b : Level) → Set _
Extensionality a b =
  {A : Set a} {B₁ B₂ : A → Set b}
  {f₁ : (x : A) → B₁ x} {f₂ : (x : A) → B₂ x} →
  (∀ x → B₁ x ≡ B₂ x) → (∀ x → f₁ x ≅ f₂ x) → f₁ ≅ f₂

-- This form of extensionality follows from extensionality for _≡_.

≡-ext-to-≅-ext : ∀ {ℓ₁ ℓ₂} →
  P.Extensionality ℓ₁ (suc ℓ₂) → Extensionality ℓ₁ ℓ₂
≡-ext-to-≅-ext           ext B₁≡B₂ f₁≅f₂ with ext B₁≡B₂
≡-ext-to-≅-ext {ℓ₁} {ℓ₂} ext B₁≡B₂ f₁≅f₂ | P.refl =
  ≡-to-≅ $ ext′ (≅-to-≡ ∘ f₁≅f₂)
  where
  ext′ : P.Extensionality ℓ₁ ℓ₂
  ext′ = P.extensionality-for-lower-levels ℓ₁ (suc ℓ₂) ext

------------------------------------------------------------------------
-- Inspect on steroids

-- Inspect on steroids can be used when you want to pattern match on
-- the result r of some expression e, and you also need to "remember"
-- that r ≡ e.

data Reveal_is_ {a} {A : Set a} (x : Hidden A) (y : A) : Set a where
  [_] : (eq : reveal x ≅ y) → Reveal x is y

inspect : ∀ {a b} {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal (hide f x) is (f x)
inspect f x = [ refl ]


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

open import Lists.Definition

module Lists.Fold.Fold {a b : _} {A : Set a} {B : Set b} where

fold : (f : A → B → B) → B → List A → B
fold f default [] = default
fold f default (x :: l) = f x (fold f default l)


text:
module DelayMishMash where

  open import Level --public
    using (Level) renaming (zero to lzero; suc to lsuc)

  open import Size public

  open import Prelude.Monad renaming (Monad to RawMonad)
  --open import Category.Monad public
  --  using (RawMonad; module RawMonad)

  open import Data.Empty --public
    using (⊥; ⊥-elim)

  open import Data.List --public
    using (List; []; _∷_; map)

  open import Data.Maybe --public
    using (Maybe; just; nothing) renaming (map to fmap)

  open import Data.Product public
    using (∃; _×_; _,_) renaming (proj₁ to fst; proj₂ to snd)
  --infixr 1 _,_

  open import Data.Sum --public
    using (_⊎_; [_,_]′) renaming (inj₁ to inl; inj₂ to inr)

  open import Data.Unit  --public
    using (⊤)

  open import Function --public
    using (_∘_; case_of_)

  open import Relation.Nullary --public
    using (Dec; yes; no)

  open import Relation.Binary --public
    using (Setoid; module Setoid)

  import Relation.Binary.PreorderReasoning
  module Pre = Relation.Binary.PreorderReasoning

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

  --open ≡-Reasoning renaming (begin_ to proof_) public

  open import Relation.Binary.HeterogeneousEquality --public
    using (_≅_; refl; ≡-to-≅; module ≅-Reasoning)
    renaming (sym to hsym; trans to htrans; cong to hcong;
              cong₂ to hcong₂; subst to hsubst)

  hcong₃ : {A : Set}{B : A → Set}{C : ∀ a → B a → Set}{D : ∀ a b → C a b → Set}
           (f : ∀ a b c → D a b c)
           {a a′ : A} → a ≅ a′ →
           {b : B a}{b′ : B a′} → b ≅ b′ →
           {c : C a b}{c′ : C a′ b′} → c ≅ c′ →
           f a b c ≅ f a′ b′ c′
  hcong₃ f refl refl refl = refl

  ≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
  ≅-to-≡ refl = refl

  mutual
    data Delay (i : Size) (A : Set) : Set where
      now    :  A           → Delay i A
      later  :  ∞Delay i A  → Delay i A

    record ∞Delay (i : Size) (A : Set) : Set where
      coinductive
      field
        force : {j : Size< i} → Delay j A

  open ∞Delay public

  never                  :  ∀{i A} → ∞Delay i A
  force (never {i}) {j}  =  later (never {j})

  module Bind where
    mutual
      bindDelay          :  ∀ {i A B} → Delay i A → (A → Delay i B) → Delay i B
      bindDelay (now    a) f   =  f a
      bindDelay (later a∞) f   =  later (bind∞Delay a∞ f)

      bind∞Delay             :  ∀ {i A B} → ∞Delay i A → (A → Delay i B) → ∞Delay i B
      force (bind∞Delay a∞ f)  =  bindDelay (force a∞) f

  _d>>=_ : ∀ {i A B} → Delay i A → (A → Delay i B) → Delay i B
  _d>>=_ {i} = Bind.bindDelay {i}

  {-
  open import Prelude.Applicative using (Applicative)
  instance delayApplicative : ∀ {i} → Applicative (Delay i)
  Applicative.pure (delayApplicative {i}) x = now x
  Applicative._<*>_ (delayApplicative {i}) (now f) x = x d>>= (now ∘ f)
  Applicative._<*>_ (delayApplicative {i}) (later f) x = {!force f {i}!}
  {-
  Applicative._<*>_ (delayApplicative {i}) f (now x) = {!x!} -- Bind.bindDelay x (λ x₁ → {!!})
  Applicative._<*>_ (delayApplicative {i}) (now f) (later x) = {!!} -- Bind.bindDelay x (λ x₁ → {!!})
  Applicative._<*>_ (delayApplicative {i}) (later f) (later x) = {!!} -- Bind.bindDelay x (λ x₁ → {!!})
  -}
  Applicative.super (delayApplicative {i}) = {!!}
  -}
  {-
  instance delayMonad : ∀ {i} → RawMonad (Delay i)
  delayMonad {i} = record
    { {-return  =  now
    ; -}_>>=_   =  bindDelay {i}
    } where open Bind
  -}

  {-
  module _ {i : Size} where
    open module DelayMonad = RawMonad (delayMonad {i = i})
                             public -- renaming (_⊛_ to _<*>_)
  -}
  open Bind public using () renaming (bind∞Delay to _∞>>=_)

  -- Map for Delay

  dreturn : {i : Size} → {A : Set} → A → Delay i A
  dreturn {i} = Delay.now {i}

  _d<$>_ : ∀ {i A B} (f : A → B) (a : Delay i A) → Delay i B
  f d<$> a = a d>>= λ a → dreturn (f a)

  -- Map for ∞Delay

  _∞<$>_ : ∀ {i A B} (f : A → B) (∞a : ∞Delay i A) → ∞Delay i B
  f ∞<$> ∞a = ∞a ∞>>= λ a → dreturn (f a)
  -- force (f ∞<$> ∞a) = f <$> force ∞a

  -- Double bind

  _=<<2_,_ : ∀ {i A B C} → (A → B → Delay i C) → Delay i A → Delay i B → Delay i C
  f =<<2 x , y = x d>>= λ a → y d>>= λ b → f a b

  mutual
    data _∼_ {i : Size} {A : Set} : (a? b? : Delay ∞ A) → Set where
      ∼now    :  ∀ a                              →  now a     ∼ now a
      ∼later  :  ∀ {a∞ b∞} (eq : a∞ ∞∼⟨ i ⟩∼ b∞)  →  later a∞  ∼ later b∞

    _∼⟨_⟩∼_ = λ {A} a? i b? → _∼_ {i}{A} a? b?

    record _∞∼⟨_⟩∼_ {A} (a∞ : ∞Delay ∞ A) i (b∞ : ∞Delay ∞ A) : Set where
      coinductive
      field
        ∼force : {j : Size< i} → force a∞ ∼⟨ j ⟩∼ force b∞

  _∞∼_ = λ {i} {A} a∞ b∞ → _∞∼⟨_⟩∼_ {A} a∞ i b∞

  open _∞∼⟨_⟩∼_ public

  ∼never : ∀{i A} → (never {A = A}) ∞∼⟨ i ⟩∼ never
  ∼force ∼never = ∼later ∼never

  ∼refl    :  ∀{i A} (a?  : Delay ∞ A)   →  a? ∼⟨ i ⟩∼ a?
  ∞∼refl   :  ∀{i A} (a∞  : ∞Delay ∞ A)  →  a∞ ∞∼⟨ i ⟩∼ a∞

  ∼sym     :  ∀{i A}{a?  b?  : Delay ∞ A }  →  a? ∼⟨ i ⟩∼ b?   →  b? ∼⟨ i ⟩∼ a?
  ∞∼sym    :  ∀{i A}{a∞  b∞  : ∞Delay ∞ A}  →  a∞ ∞∼⟨ i ⟩∼ b∞  →  b∞ ∞∼⟨ i ⟩∼ a∞

  ∼trans   :  ∀{i A}{a? b? c? : Delay ∞ A} →
              a? ∼⟨ i ⟩∼ b? →  b? ∼⟨ i ⟩∼ c? → a? ∼⟨ i ⟩∼ c?
  ∞∼trans  :  ∀{i A}{a∞ b∞ c∞ : ∞Delay ∞ A} →
              a∞ ∞∼⟨ i ⟩∼ b∞ →  b∞ ∞∼⟨ i ⟩∼ c∞ → a∞ ∞∼⟨ i ⟩∼ c∞

  ∼refl (now a)    = ∼now a
  ∼refl (later a∞) = ∼later (∞∼refl a∞)

  ∼force (∞∼refl a∞) = ∼refl (force a∞)

  ∼sym (∼now a)    = ∼now a
  ∼sym (∼later eq) = ∼later (∞∼sym eq)

  ∼force (∞∼sym eq) = ∼sym (∼force eq)

  ∼trans (∼now a)    (∼now .a)    = ∼now a
  ∼trans (∼later eq) (∼later eq′) = ∼later (∞∼trans eq eq′)

  ∼force (∞∼trans eq eq′) = ∼trans (∼force eq) (∼force eq′)

  -- Equality reasoning

  ∼setoid : (i : Size) (A : Set) → Setoid lzero lzero
  ∼setoid i A = record
    { Carrier       = Delay ∞ A
    ; _≈_           = _∼_ {i}
    ; isEquivalence = record
      { refl  = λ {a?} → ∼refl a?
      ; sym   = ∼sym
      ; trans = ∼trans
      }
    }

  ∞∼setoid : (i : Size) (A : Set) → Setoid lzero lzero
  ∞∼setoid i A = record
    { Carrier       = ∞Delay ∞ A
    ; _≈_           = _∞∼_ {i}
    ; isEquivalence = record
      { refl  = λ {a?} → ∞∼refl a?
      ; sym   = ∞∼sym
      ; trans = ∞∼trans
      }
    }

  module ∼-Reasoning {i : Size} {A : Set} where
    open Pre (Setoid.preorder (∼setoid i A)) public
  --    using (begin_; _∎) (_≈⟨⟩_ to _∼⟨⟩_; _≈⟨_⟩_ to _∼⟨_⟩_)
      renaming (_≈⟨⟩_ to _≡⟨⟩_; _≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _∼⟨_⟩_; begin_ to proof_)

  module ∞∼-Reasoning {i : Size} {A : Set} where
    open Pre (Setoid.preorder (∞∼setoid i A)) public
  --    using (begin_; _∎) (_≈⟨⟩_ to _∼⟨⟩_; _≈⟨_⟩_ to _∼⟨_⟩_)
      renaming (_≈⟨⟩_ to _≡⟨⟩_; _≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _∞∼⟨_⟩_; begin_ to proof_)

  mutual
    bind-assoc               :  ∀{i A B C} (m : Delay ∞ A)
                                {k : A → Delay ∞ B} {l : B → Delay ∞ C} →
                                ((m d>>= k) d>>= l) ∼⟨ i ⟩∼ (m d>>= λ a → (k a d>>= l))
    bind-assoc (now a)       =  ∼refl _
    bind-assoc (later a∞)    =  ∼later (∞bind-assoc a∞)

    ∞bind-assoc              :  ∀{i A B C} (a∞ : ∞Delay ∞ A)
                                {k : A → Delay ∞ B} {l : B → Delay ∞ C} →
                                ((a∞ ∞>>= k) ∞>>= l) ∞∼⟨ i ⟩∼ (a∞ ∞>>= λ a → (k a d>>= l))
    ∼force (∞bind-assoc a∞)  =  bind-assoc (force a∞)

  bind-cong-l   :  ∀{i A B}{a? b? : Delay ∞ A} →  a? ∼⟨ i ⟩∼ b? →
                   (k : A → Delay ∞ B) → (a? d>>= k) ∼⟨ i ⟩∼ (b? d>>= k)

  ∞bind-cong-l  :  ∀{i A B}{a∞ b∞ : ∞Delay ∞ A} → a∞ ∞∼⟨ i ⟩∼ b∞ →
                   (k : A → Delay ∞ B) → (a∞ ∞>>= k) ∞∼⟨ i ⟩∼ (b∞ ∞>>= k)

  bind-cong-r   :  ∀{i A B}(a? : Delay ∞ A){k l : A → Delay ∞ B} →
                   (∀ a → (k a) ∼⟨ i ⟩∼ (l a)) → (a? d>>= k) ∼⟨ i ⟩∼ (a? d>>= l)

  ∞bind-cong-r  :  ∀{i A B}(a∞ : ∞Delay ∞ A){k l : A → Delay ∞ B} →
                   (∀ a → (k a) ∼⟨ i ⟩∼ (l a)) → (a∞ ∞>>= k) ∞∼⟨ i ⟩∼ (a∞ ∞>>= l)

  bind-cong-l (∼now a)    k = ∼refl _
  bind-cong-l (∼later eq) k = ∼later (∞bind-cong-l eq k)

  ∼force (∞bind-cong-l eq k) = bind-cong-l (∼force eq) k

  bind-cong-r (now a)    h = h a
  bind-cong-r (later a∞) h = ∼later (∞bind-cong-r a∞ h)

  ∼force (∞bind-cong-r a∞ h) = bind-cong-r (force a∞) h

  open import Prelude.Functor using (Functor; _<$>_)
{-
  instance FunctorDelay : {i : Size} → Functor (Delay i)
  Functor.fmap (FunctorDelay {i}) {A} {B} f (now x) = {!!}
  Functor.fmap (FunctorDelay {i}) {A} {B} f (later x) = {!!}
-}
  open import Prelude.Function using (_∘′_)

  map-compose     :  ∀{i A B C} (a? : Delay ∞ A) {f : A → B} {g : B → C} →
                     (g d<$> (f d<$> a?)) ∼⟨ i ⟩∼ ((g ∘ f) d<$> a?)
  map-compose a?  =  bind-assoc a?

  map-cong        :  ∀{i A B}{a? b? : Delay ∞ A} (f : A → B) →
                     a? ∼⟨ i ⟩∼ b? → (f d<$> a?) ∼⟨ i ⟩∼ (f d<$> b?)
  map-cong f eq   =  bind-cong-l eq (now ∘ f)

  data _⇓_ {A : Set} : (a? : Delay ∞ A) (a : A) → Set where
    now⇓    :  ∀{a}                                   → now a ⇓ a
    later⇓  :  ∀{a} {a∞ : ∞Delay ∞ A} → force a∞ ⇓ a  → later a∞ ⇓ a

  _⇓   :  {A : Set} (x : Delay ∞ A) → Set
  x ⇓  =  ∃ λ a → x ⇓ a

  map⇓     :  ∀{A B}{a : A}{a? : Delay ∞ A}(f : A → B) → a? ⇓ a → (f d<$> a?) ⇓ f a

  subst∼⇓  :  ∀{A}{a? a?′ : Delay ∞ A}{a : A} → a? ⇓ a → a? ∼ a?′ → a?′ ⇓ a

  bind⇓    :  ∀{A B}(f : A → Delay ∞ B){?a : Delay ∞ A}{a : A}{b : B} →
              ?a ⇓ a → f a ⇓ b → (?a d>>= f) ⇓ b

  map⇓ f now⇓        = now⇓
  map⇓ f (later⇓ a⇓) = later⇓ (map⇓ f a⇓)

  subst∼⇓ now⇓ (∼now a) = now⇓
  subst∼⇓ (later⇓ p) (∼later eq) = later⇓ (subst∼⇓ p (∼force eq))

  bind⇓ f now⇓ q = q
  bind⇓ f (later⇓ p) q = later⇓ (bind⇓ f p q)

  --infixr 6 _⇒_
  --infixl 1 _,_


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for Conats
------------------------------------------------------------------------

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

module Codata.Conat.Bisimilarity where

open import Level using (0ℓ)
open import Size
open import Codata.Thunk
open import Codata.Conat
open import Relation.Binary

infix 1 _⊢_≈_
data _⊢_≈_ i : (m n : Conat ∞) → Set where
  zero : i ⊢ zero ≈ zero
  suc  : ∀ {m n} → Thunk^R _⊢_≈_ i m n → i ⊢ suc m ≈ suc n

refl : ∀ {i m} → i ⊢ m ≈ m
refl {m = zero}  = zero
refl {m = suc m} = suc λ where .force → refl

sym : ∀ {i m n} → i ⊢ m ≈ n → i ⊢ n ≈ m
sym zero     = zero
sym (suc eq) = suc λ where .force → sym (eq .force)

trans : ∀ {i m n p} → i ⊢ m ≈ n → i ⊢ n ≈ p → i ⊢ m ≈ p
trans zero      zero      = zero
trans (suc eq₁) (suc eq₂) = suc λ where .force → trans (eq₁ .force) (eq₂ .force)

isEquivalence : ∀ {i} → IsEquivalence (i ⊢_≈_)
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

setoid : Size → Setoid 0ℓ 0ℓ
setoid i = record
  { isEquivalence = isEquivalence {i = i}
  }

module ≈-Reasoning {i} where

  open import Relation.Binary.Reasoning.Setoid (setoid i) public

infix 1 _⊢_≲_
data _⊢_≲_ i : (m n : Conat ∞) → Set where
  z≲n : ∀ {n} → i ⊢ zero ≲ n
  s≲s : ∀ {m n} → Thunk^R _⊢_≲_ i m n → i ⊢ suc m ≲ suc n

≈⇒≲ : ∀ {i m n} → i ⊢ m ≈ n → i ⊢ m ≲ n
≈⇒≲ zero     = z≲n
≈⇒≲ (suc eq) = s≲s λ where .force → ≈⇒≲ (eq .force)

≲-refl : ∀ {i m} → i ⊢ m ≲ m
≲-refl = ≈⇒≲ refl

≲-antisym : ∀ {i m n} → i ⊢ m ≲ n → i ⊢ n ≲ m → i ⊢ m ≈ n
≲-antisym z≲n      z≲n      = zero
≲-antisym (s≲s le) (s≲s ge) = suc λ where .force → ≲-antisym (le .force) (ge .force)

≲-trans : ∀ {i m n p} → i ⊢ m ≲ n → i ⊢ n ≲ p → i ⊢ m ≲ p
≲-trans z≲n       _         = z≲n
≲-trans (s≲s le₁) (s≲s le₂) = s≲s λ where .force → ≲-trans (le₁ .force) (le₂ .force)


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

$sig_string
-}

module $syn_name.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import $syn_name.Signature
open import $syn_name.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution ${sig}:Syn
open import SOAS.Metatheory.SecondOrder.Equality ${sig}:Syn

private
  variable
    α β γ τ : $type
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ ${sig}) α Γ → (𝔐 ▷ ${sig}) α Γ → Set where
  $axioms

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

$derived_eqs

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas