text:
module IlltypedPattern where

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

f : (A : Set) -> A -> A
f A zero = zero

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Rationals.SigmaQ where

open import Cubical.HITs.Rationals.SigmaQ.Base public

open import Cubical.HITs.Rationals.SigmaQ.Properties public

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
--
-- Created by Dependently-Typed Lambda Calculus on 2019-05-15
-- private-primitive-variable
-- Author: ice1000
--

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

private
 variable
  A : Set
  a : A
primitive
 primInterval : Set

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_name: dubinsky/intellij-dtlc


text:
-- Andreas, 2014-05-17

open import Common.Prelude
open import Common.Equality

test : Nat
test rewrite refl = zero

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --postfix-projections #-}

module StateSized.StackStateDependent where

open import Data.Product
open import Function
open import Data.String.Base as Str
open import Data.Nat.Base as N
open import Data.Vec as Vec using (Vec; []; _∷_; head; tail)

open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Product.Pointwise

open import NativeIO

open import SizedIO.Base
open import SizedIO.Console hiding (main)

open import StateSizedIO.GUI.BaseStateDependent
open import StateSizedIO.Object
open import StateSizedIO.IOObject

open import Size

StackStateˢ = ℕ

data StackMethodˢ (A : Set) : StackStateˢ → Set where
  push : {n : StackStateˢ} → A → StackMethodˢ A n
  pop  : {n : StackStateˢ} → StackMethodˢ A (suc n)

StackResultˢ : (A : Set) → (s : StackStateˢ) → StackMethodˢ A s → Set
StackResultˢ A .n (push { n  } x₁)  = Unit
StackResultˢ A (suc .n)  (pop {n} ) = A

nˢ : (A : Set) → (s : StackStateˢ) → (m : StackMethodˢ A s) → (r : StackResultˢ A s m) → StackStateˢ
nˢ A .n (push { n } x)     r = suc n
nˢ A (suc .n) (pop  { n }) r = n

StackInterfaceˢ : (A : Set) → Interfaceˢ
StackInterfaceˢ A .Stateˢ  = StackStateˢ
StackInterfaceˢ A .Methodˢ = StackMethodˢ A
StackInterfaceˢ A .Resultˢ = StackResultˢ A
StackInterfaceˢ A .nextˢ = nˢ A

stackP : ∀{n : ℕ} → (i : Size) → (v : Vec String n) → IOObjectˢ consoleI (StackInterfaceˢ String) i n
method (stackP { n }   i es)       {j} (push e) = return (_ , stackP j (e ∷ es))
method (stackP {suc n} i (x ∷ xs)){j} pop      = return (x , stackP j xs)

-- UNSIZED Version, without IO

stackP' : ∀{n : ℕ} → (v : Vec String n) → Objectˢ (StackInterfaceˢ String) n
stackP' es .objectMethod (push e) = (_ , stackP' (e ∷ es))
stackP' (x ∷ xs) .objectMethod pop = x , stackP' xs

stackO : ∀{E : Set} {n : ℕ} (v : Vec E n) → Objectˢ (StackInterfaceˢ E) n
objectMethod (stackO es)      (push e) = _ , stackO (e ∷ es)
objectMethod (stackO (e ∷ es)) pop      = e , stackO es

stackF : ∀{E : Set} (n : ℕ) (f : ℕ → E) → Objectˢ (StackInterfaceˢ E) n
objectMethod (stackF n f) (push x) = _ , stackF (suc n)
  \{ zero → x
   ; (suc m) → f m
   }
objectMethod (stackF (suc n) f) pop = (f zero) , stackF n (f  ∘ suc)

tabulate : ∀{E : Set} (n : ℕ) (f : ℕ → E) → Vec E n
tabulate zero    f = []
tabulate (suc n) f = f zero ∷ tabulate n λ m → f (suc m)

module _ {E : Set} where
  private
    I = StackInterfaceˢ E
    S = Stateˢ I
    O = Objectˢ I
  open Bisim I

  _≡×≅'_ : ∀{s} → (o o' : E × O s) → Set
  _≡×≅'_ = _≡_ ×-Rel _≅_

  Eq×Bisim : ∀ (s : S) → (o o' : E × O s) → Set
  Eq×Bisim s = _≡_ ×-Rel _≅_

  pop-after-push : ∀{n}{v : Vec E n} (e : E) (let stack = stackO v) →
     (objectMethod stack (push e) ▹   λ { (_ , stack₁) →
      objectMethod stack₁ pop     ▹   λ { (e₁ , stack₂) →
      ( e₁ , stack₂ )  }})
    ≡×≅' (e , stack)
  pop-after-push e = refl , refl≅ _

  push-after-pop : ∀{n}{v : Vec E n} (e : E) (let stack = stackO (e ∷ v)) →
     (objectMethod stack  pop       ▹  λ { (e₁ , stack₁) →
      objectMethod stack₁ (push e₁) ▹  λ { (_  , stack₂) →
      stack₂ }})
     ≅ stack
  push-after-pop e = refl≅ _

  -- The implementations of stacks with either vectors or functions are bisimilar.

  impl-bisim : ∀{n : ℕ} {f : ℕ → E} (v : Vec E n) (p : tabulate n f ≡ v)
    → stackF n f ≅ stackO v

  bisimMethod (impl-bisim v       p) (push e) =
    bisim (impl-bisim (e ∷ v) (cong (_∷_ e) p))

  bisimMethod (impl-bisim (x ∷ v) p) pop rewrite cong head p =
    bisim (impl-bisim v (cong tail p))

program : IOConsole ∞ Unit
program =
  exec getLine                λ str₀ →
  method s₀ (push str₀) >>= λ{ (_ , s₁) →            -- empty
  exec getLine                λ   str₁ →
  method s₁ (push str₁) >>= λ{ (_ , s₂) →            -- full
  method s₂ pop         >>= λ{ (str₂ , s₃) →
  exec (putStrLn ("first pop: " Str.++ str₂)  ) λ _ →
  exec getLine                λ   str₃ →
  method s₃ (push str₃) >>= λ{ (_ , s₄) →
  method s₄ pop         >>= λ{ (str₄ , s₅) →
  exec (putStrLn ("second pop: " Str.++ str₄)  ) λ _ →
  method s₅ pop         >>= λ{ (str₅ , s₅) →
  exec (putStrLn ("third  pop: " Str.++ str₅)  ) λ _ →
  return unit
  }}}}}}
  where
    s₀ = stackP ∞ []

main : NativeIO Unit
main = translateIOConsole program

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

module Lens.Operators where

open import Prelude
open import Lens.Definition

infixl 4 getter setter

getter : Lens A B → A → B
getter l xs = get (fst l xs)

syntax getter l xs = xs [ l ]

setter : Lens A B → A → B → A
setter l xs = set (fst l xs)

syntax setter l xs x = xs [ l ]≔ x

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Properties.Product where

infixr 5 _×_ _,_

record Σ {A : Set} (B : A → Set) : Set where

  constructor _,_
  field fst : A
  field snd : B fst

open Σ public

_×_ : Set → Set → Set
A × B = Σ (λ (a : A) → B)

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


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

{-
Truncated higher inductive types look like higher inductive types except that
they are truncated down to some fixed truncation level.
This allow to define truncations (obviously) but also free algebras for
algebraic theories, Eilenberg-MacLane spaces, etc.

The idea is that to get an n-truncated higher inductive type, you just have to
add the following two constructors, where [I] is the HIT you are defining.

    top  : (f : Sⁿ n → I) → I
    rays : (f : Sⁿ n → I) (x : Sⁿ n) → top f ≡ f x

In this file, I prove whatever is needed to go from the usual elimination rules
generated by the previous constructors to the elimination rules that we expect
from truncated higher inductive types.

We have to note that the previous definition does not work for [n = 0], because
this only adds a point to I instead of turning it into a contractible space.
0-truncated higher inductive types are not really interesting but handling
truncations is easier when 0 is not special

Hence I’m adding the following path constructor

    hack-prop : (p : n ≡ 0) (x y : τ) → (x ≡ y)

This will force [I] to be a prop (hence contractible because [top] of the empty
function is of type [I]) and does not change anything when [n] is not 0.

I may use the following syntax for [n]-truncated higher inductive types:

    (n)data I : Set i where
      …

-}

module Homotopy.TruncatedHIT where

open import Base
open import Spaces.Spheres public
open import Spaces.Suspension public

_+1 : ℕ₋₂ → ℕ
⟨-2⟩ +1 = 0
(S ⟨-2⟩) +1 = 0
(S n) +1 = S (n +1)

-- [hSⁿ n] is what is supposed to be filled to get something n-truncated
hSⁿ : ℕ₋₂ → Set
hSⁿ ⟨-2⟩ = ⊥
hSⁿ n = Sⁿ (n +1)

-- Type of fillings of a sphere
filling : ∀ {i} (n : ℕ₋₂) {A : Set i} (f : hSⁿ n → A) → Set i
filling {i} n {A} f = Σ A (λ t → ((x : hSⁿ n) → t ≡ f x))

-- Type of dependent fillings of a sphere above a ball
filling-dep : ∀ {i j} (n : ℕ₋₂) {A : Set i} (P : A → Set j) (f : hSⁿ n → A)
  (fill : filling n f) (p : (x : hSⁿ n) → P (f x)) → Set j
filling-dep {i} {j} n {A} P f fill p =
  Σ (P (π₁ fill)) (λ t → ((x : hSⁿ n) → transport P (π₂ fill x) t ≡ p x))

-- [has-n-spheres-filled n A] is inhabited iff every n-sphere in [A] can be
-- filled with an (n+1)-ball.
-- We will show that this is equivalent to being n-truncated, *for n > 0*
-- (for n = 0, having 0-spheres filled only means that A is inhabited)
has-spheres-filled : ∀ {i} (n : ℕ₋₂) (A : Set i) → Set i
has-spheres-filled n A = (f : hSⁿ n → A) → filling n f

-- [has-n-spheres-filled] satisfy the same inductive property
-- than [is-truncated]
fill-paths : ∀ {i} (n : ℕ₋₂) (A : Set i) (t : has-spheres-filled (S n) A)
  → (n ≡ ⟨-2⟩ → is-contr A) → ((x y : A) → has-spheres-filled n (x ≡ y))
fill-paths ⟨-2⟩ A t contr x y f =
  (contr-has-all-paths (contr refl) x y , abort)
fill-paths (S n) A t _ x y f =
  ((! (π₂ u (north _)) ∘ π₂ u (south _))
  , (λ z → ! (lemma (paths _ z)) ∘ suspension-β-paths-nondep _ _ _ _ f _)) where

  -- [f] is a map from [hSⁿ (S n)] to [x ≡ y], we can build from it a map
  -- from [hSⁿ (S n)] to [A]
  newf : hSⁿ (S (S n)) → A
  newf = suspension-rec-nondep _ _ x y f

  u : filling (S (S n)) newf
  u = t newf
  -- I’ve got a filling

  -- Every path in the sphere is equal (in A) to the canonical path going
  -- through the center of the filled sphere
  lemma : {p q : hSⁿ (S (S n))} (l : p ≡ q)
    → ap newf l ≡ ! (π₂ u p) ∘ π₂ u q
  lemma {p = a} refl = ! (opposite-left-inverse (π₂ u a))

-- We first prove that if n-spheres are filled, then the type is n-truncated,
-- we have to prove it for n = -1, and then use the previous lemma
abstract
  spheres-filled-is-truncated : ∀ {i} (n : ℕ₋₂) (A : Set i)
    → ((n ≡ ⟨-2⟩ → is-contr A) → has-spheres-filled n A → is-truncated n A)
  spheres-filled-is-truncated ⟨-2⟩ A contr t = contr refl
  spheres-filled-is-truncated (S ⟨-2⟩) A _ t =
    all-paths-is-prop (λ x y → ! (π₂ (t (f x y)) true) ∘ π₂ (t (f x y)) false)
    where
      f : (x y : A) → bool {zero} → A
      f x y true = x
      f x y false = y
  spheres-filled-is-truncated (S (S n)) A _ t = λ x y →
    spheres-filled-is-truncated (S n) (x ≡ y) (λ ())
      (fill-paths (S n) A t (λ ()) x y)

-- We now prove the converse
abstract
  truncated-has-spheres-filled : ∀ {i} (n : ℕ₋₂) (A : Set i)
    (t : is-truncated n A) → has-spheres-filled n A
  truncated-has-spheres-filled ⟨-2⟩ A t f = (π₁ t , abort)
  truncated-has-spheres-filled (S ⟨-2⟩) A t f =
    (f true , (λ {true → refl ; false → π₁ (t (f true) (f false))}))
  truncated-has-spheres-filled (S (S n)) A t f =
    (f (north _)
    , (suspension-rec _ _ refl (ap f (paths _ (⋆Sⁿ _)))
        (λ x → trans-cst≡app (f (north _)) f (paths _ _) _
               ∘ (! (π₂ filled-newf x) ∘ π₂ filled-newf (⋆Sⁿ _))))) where

    newf : hSⁿ (S n) → (f (north _) ≡ f (south _))
    newf x = ap f (paths _ x)

    filled-newf : filling (S n) newf
    filled-newf = truncated-has-spheres-filled (S n) _ (t _ _) newf

-- I prove that if [A] has [S n]-spheres filled, then the type of fillings
-- of [n]-spheres is a proposition. The idea is that two fillings of
-- an [n]-sphere define an [S n]-sphere, which is then filled.
filling-has-all-paths : ∀ {i} (n : ℕ₋₂) (A : Set i)
  ⦃ fill : has-spheres-filled (S n) A ⦄ (f : hSⁿ n → A)
  → has-all-paths (filling n f)
filling-has-all-paths ⟨-2⟩ A ⦃ fill ⦄ f fill₁ fill₂ =
  Σ-eq (! (π₂ big-map-filled true) ∘ π₂ big-map-filled false) (funext abort)
  where

  big-map : hSⁿ ⟨-1⟩ → A
  big-map true = π₁ fill₁
  big-map false = π₁ fill₂

  big-map-filled : filling ⟨-1⟩ big-map
  big-map-filled = fill big-map

filling-has-all-paths (S n) A ⦃ fill ⦄ f fill₁ fill₂ =
  Σ-eq (! (π₂ big-map-filled (north _)) ∘ π₂ big-map-filled (south _))
  (funext (λ x →
                   trans-Π2 _ (λ t x₁ → t ≡ f x₁)
                   (! (π₂ big-map-filled (north _)) ∘
                    π₂ big-map-filled (south _))
                   (π₂ fill₁) x
                   ∘ (trans-id≡cst
                        (! (π₂ big-map-filled (north _)) ∘
                         π₂ big-map-filled (south _))
                        (π₂ fill₁ x)
                   ∘ move!-right-on-left
                       (! (π₂ big-map-filled (north _)) ∘
                        π₂ big-map-filled (south _))
                       _ _
                    (move-left-on-right _
                       (! (π₂ big-map-filled (north _)) ∘
                        π₂ big-map-filled (south _))
                       _
                    (! (suspension-β-paths-nondep _ _ _ _ g x)
                     ∘ lemma (paths _ x)))))) where

  g : hSⁿ (S n) → (π₁ fill₁ ≡ π₁ fill₂)
  g x = π₂ fill₁ x ∘ ! (π₂ fill₂ x)

  big-map : hSⁿ (S (S n)) → A
  big-map = suspension-rec-nondep _ _ (π₁ fill₁) (π₁ fill₂) g

  big-map-filled : filling (S (S n)) big-map
  big-map-filled = fill big-map

  lemma : {u v : hSⁿ (S (S n))} (p : u ≡ v)
    → ap big-map p ≡ (! (π₂ big-map-filled u) ∘  π₂ big-map-filled v)
  lemma {u = a} refl = ! (opposite-left-inverse (π₂ big-map-filled a))

abstract
  truncated-has-filling-dep : ∀ {i j} (A : Set i) (P : A → Set j) (n : ℕ₋₂)
    ⦃ trunc : (x : A) → is-truncated n (P x) ⦄
    (contr : n ≡ ⟨-2⟩ → is-contr A)
    (fill : has-spheres-filled n A) (f : hSⁿ n → A) (p : (x : hSⁿ n) → P (f x))
    → filling-dep n P f (fill f) p
  truncated-has-filling-dep A P ⟨-2⟩ ⦃ trunc ⦄ contr fill f p =
    (π₁ (trunc (π₁ (fill f))) , abort)
  truncated-has-filling-dep A P (S n) ⦃ trunc ⦄ contr fill f p =
    transport (λ t → filling-dep (S n) P f t p) eq fill-dep  where

    -- Combining [f] and [p] we have a sphere in the total space of [P]
    newf : hSⁿ (S n) → Σ A P
    newf x = (f x , p x)

    -- But this total space is (S n)-truncated
    ΣAP-truncated : is-truncated (S n) (Σ A P)
    ΣAP-truncated =
      Σ-is-truncated (S n) (spheres-filled-is-truncated (S n) A contr fill)
                     trunc

    -- Hence the sphere is filled
    tot-fill : filling (S n) newf
    tot-fill = truncated-has-spheres-filled (S n) (Σ A P) ΣAP-truncated newf

    -- We can split this filling as a filling of [f] in [A] …
    new-fill : filling (S n) f
    new-fill = (π₁ (π₁ tot-fill) , (λ x → base-path (π₂ tot-fill x)))

    -- and a dependent filling above the previous filling of [f], along [p]
    fill-dep : filling-dep (S n) P f new-fill p
    fill-dep = (π₂ (π₁ tot-fill) , (λ x → fiber-path (π₂ tot-fill x)))

    A-has-spheres-filled-S : has-spheres-filled (S (S n)) A
    A-has-spheres-filled-S =
      truncated-has-spheres-filled (S (S n)) A
        (truncated-is-truncated-S (S n)
          (spheres-filled-is-truncated (S n) A contr fill))

    -- But both the new and the old fillings of [f] are equal, hence we will
    -- have a dependent filling above the old one
    eq : new-fill ≡ fill f
    eq = filling-has-all-paths (S n) A f new-fill (fill f)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module Categories.Category.Construction.Adjoints where

open import Level
open import Data.Product using (_×_ ; _,_)

open import Categories.Category
open import Categories.Category.Helper
open import Categories.Adjoint
open import Categories.Adjoint.Compose
open import Categories.Adjoint.Mate
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.NaturalTransformation.Equivalence renaming (_≃_ to _≊_)

import Categories.Morphism.Reasoning as MR

private
  variable
    o o′ ℓ ℓ′ e e′ : Level

-- category of adjunctions between two fixed categories
module _ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) where
  private
    module C = Category C
    module D = Category D

  record AdjointObj : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      L   : Functor C D
      R   : Functor D C
      L⊣R : L ⊣ R

    module L = Functor L
    module R = Functor R
    module L⊣R = Adjoint L⊣R

  record Adjoint⇒ (X Y : AdjointObj) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    private
      module X = AdjointObj X
      module Y = AdjointObj Y

    field
      mate : HaveMate X.L⊣R Y.L⊣R

    open HaveMate mate public

  private
    _≈_ : ∀ {A B} → Adjoint⇒ A B → Adjoint⇒ A B → Set (o ⊔ e ⊔ o′ ⊔ e′)
    f ≈ g = Adjoint⇒.α f ≊ Adjoint⇒.α g × Adjoint⇒.β f ≊ Adjoint⇒.β g

    id : {X : AdjointObj} → Adjoint⇒ X X
    id {X} = record
      { mate = record
        { α    = idN
        ; β    = idN
        ; mate = record
          { commute₁ = C.∘-resp-≈ˡ R.identity
          ; commute₂ = D.∘-resp-≈ʳ L.identity
          }
        }
      }
      where open AdjointObj X

    _∘_ : ∀ {X Y Z} → Adjoint⇒ Y Z → Adjoint⇒ X Y → Adjoint⇒ X Z
    _∘_ {X} {Y} {Z} f g = record
      { mate = record
        { α    = f.α ∘ᵥ g.α
        ; β    = g.β ∘ᵥ f.β
        ; mate = record
          { commute₁ = λ {W} →
            let open C.HomReasoning
                open MR C
            in begin
            X.R.F₁ (f.α.η W D.∘ g.α.η W) C.∘ X.L⊣R.unit.η W            ≈⟨ X.R.homomorphism ⟩∘⟨refl ⟩
            (X.R.F₁ (f.α.η W) C.∘ X.R.F₁ (g.α.η W)) C.∘ X.L⊣R.unit.η W ≈⟨ pullʳ g.commute₁ ⟩
            X.R.F₁ (f.α.η W) C.∘ g.β.η (Y.L.F₀ W) C.∘ Y.L⊣R.unit.η W   ≈⟨ pullˡ (g.β.sym-commute _) ⟩
            (g.β.η (Z.L.F₀ W) C.∘ Y.R.F₁ (f.α.η W)) C.∘ Y.L⊣R.unit.η W ≈⟨ pullʳ f.commute₁ ⟩
            g.β.η (Z.L.F₀ W) C.∘ f.β.η (Z.L.F₀ W) C.∘ Z.L⊣R.unit.η W   ≈⟨ C.sym-assoc ⟩
            (g.β.η (Z.L.F₀ W) C.∘ f.β.η (Z.L.F₀ W)) C.∘ Z.L⊣R.unit.η W ∎
          ; commute₂ = λ {W} →
            let open D.HomReasoning
                open MR D
            in begin
              X.L⊣R.counit.η W D.∘ X.L.F₁ (g.β.η W C.∘ f.β.η W)            ≈⟨ refl⟩∘⟨ X.L.homomorphism ⟩
              X.L⊣R.counit.η W D.∘ X.L.F₁ (g.β.η W) D.∘ X.L.F₁ (f.β.η W)   ≈⟨ pullˡ g.commute₂ ⟩
              (Y.L⊣R.counit.η W D.∘ g.α.η (Y.R.F₀ W)) D.∘ X.L.F₁ (f.β.η W) ≈⟨ pullʳ (g.α.commute _) ⟩
              Y.L⊣R.counit.η W D.∘ Y.L.F₁ (f.β.η W) D.∘ g.α.η (Z.R.F₀ W)   ≈⟨ pullˡ f.commute₂ ⟩
              (Z.L⊣R.counit.η W D.∘ f.α.η (Z.R.F₀ W)) D.∘ g.α.η (Z.R.F₀ W) ≈⟨ D.assoc ⟩
              Z.L⊣R.counit.η W D.∘ f.α.η (Z.R.F₀ W) D.∘ g.α.η (Z.R.F₀ W)   ∎
          }
        }
      }
      where module X = AdjointObj X
            module Y = AdjointObj Y
            module Z = AdjointObj Z
            module f = Adjoint⇒ f
            module g = Adjoint⇒ g

  Adjoints : Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ e ⊔ o′ ⊔ e′)
  Adjoints = categoryHelper record
     { Obj       = AdjointObj
     ; _⇒_       = Adjoint⇒
     ; _≈_       = _≈_
     ; id        = id
     ; _∘_       = _∘_
     ; assoc     = D.assoc , C.sym-assoc
     ; identityˡ = D.identityˡ , C.identityʳ
     ; identityʳ = D.identityʳ , C.identityˡ
     ; equiv     = record
       { refl  = D.Equiv.refl , C.Equiv.refl
       ; sym   = λ { (eq₁ , eq₂) → D.Equiv.sym eq₁ , C.Equiv.sym eq₂ }
       ; trans = λ { (eq₁ , eq₂) (eq₃ , eq₄) → D.Equiv.trans eq₁ eq₃ , C.Equiv.trans eq₂ eq₄ }
       }
     ; ∘-resp-≈  = λ { (eq₁ , eq₂) (eq₃ , eq₄) → D.∘-resp-≈ eq₁ eq₃ , C.∘-resp-≈ eq₄ eq₂ }
     }

module _ o ℓ e where
  private
    _≈_ : ∀ {A B : Category o ℓ e} → AdjointObj A B → AdjointObj A B → Set (o ⊔ ℓ ⊔ e)
    f ≈ g = f.L ≃ g.L × f.R ≃ g.R
      where module f = AdjointObj f
            module g = AdjointObj g

    id : {A : Category o ℓ e} → AdjointObj A A
    id = record
      { L   = idF
      ; R   = idF
      ; L⊣R = ⊣-id
      }

    _∘_ : {A B C : Category o ℓ e} → AdjointObj B C → AdjointObj A B → AdjointObj A C
    f ∘ g = record
      { L   = f.L ∘F g.L
      ; R   = g.R ∘F f.R
      ; L⊣R = g.L⊣R ∘⊣ f.L⊣R
      }
      where module f = AdjointObj f
            module g = AdjointObj g

  Adjunctions : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
  Adjunctions = categoryHelper record
    { Obj       = Category o ℓ e
    ; _⇒_       = AdjointObj
    ; _≈_       = _≈_
    ; id        = id
    ; _∘_       = _∘_
    ; assoc     = λ {_ _ _ _ f g h} → associator (AdjointObj.L f) (AdjointObj.L g) (AdjointObj.L h)
                                    , sym-associator (AdjointObj.R h) (AdjointObj.R g) (AdjointObj.R f)
    ; identityˡ = unitorˡ , unitorʳ
    ; identityʳ = unitorʳ , unitorˡ
    ; equiv     = record
      { refl  = ≃.refl , ≃.refl
      ; sym   = λ { (α , β) → ≃.sym α , ≃.sym β }
      ; trans = λ { (α₁ , β₁) (α₂ , β₂) → ≃.trans α₁ α₂ , ≃.trans β₁ β₂ }
      }
    ; ∘-resp-≈  = λ { (α₁ , β₁) (α₂ , β₂) → α₁ ⓘₕ α₂ , β₂ ⓘₕ β₁ }
    }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
-- Some basic structures and operation for dealing with non-deterministic values

module nondet where

open import bool
open import nat
open import list

infixr 8 _??_

----------------------------------------------------------------------
-- A tree datatype to represent non-deterministic value of some type.
-- It is either a value, a failure, or a choice between
-- non-deterministic values.
----------------------------------------------------------------------

data ND (A : Set) : Set where
  Val  : A → ND A
  _??_ : ND A → ND A → ND A

----------------------------------------------------------------------
-- Some operation to define functions working this the ND datatype:

-- Map a function on non-deterministic values:
mapND : {A B : Set} → (A → B) → ND A → ND B
mapND f (Val xs) = Val (f xs)
mapND f (t1 ?? t2) = mapND f t1 ?? mapND f t2

-- Extend the first argument to ND:
with-nd-arg : {A B : Set} → (A → ND B) → ND A → ND B
with-nd-arg f (Val x)    = f x
with-nd-arg f (t1 ?? t2) = with-nd-arg f t1 ?? with-nd-arg f t2

-- Extend the first argument of a binary function to ND:
with-nd-arg2 : {A B C : Set} → (A → B → ND C) → ND A → B → ND C
with-nd-arg2 f (Val x)    y = f x y
with-nd-arg2 f (t1 ?? t2) y = with-nd-arg2 f t1 y ?? with-nd-arg2 f t2 y

-- Extend the first argument of a ternary function to ND:
with-nd-arg3 : {A B C D : Set} → (A → B → C → ND D)
                               → ND A → B → C → ND D
with-nd-arg3 f (Val x)    y z = f x y z
with-nd-arg3 f (t1 ?? t2) y z = with-nd-arg3 f t1 y z ?? with-nd-arg3 f t2 y z

-- Apply a non-deterministic functional value to a non-determistic argument:
apply-nd : {A B : Set} → ND (A → B) → ND A → ND B
apply-nd (Val f) xs    = mapND f xs
apply-nd (t1 ?? t2) xs = apply-nd t1 xs ?? apply-nd t2 xs

-- Extend a deterministic function to one with non-deterministic result:
toND : {A B : Set} → (A → B) → A → ND B
toND f x = Val (f x)

-- Extend a deterministic function to a non-deterministic one:
det-to-nd : {A B : Set} → (A → B) → ND A → ND B
det-to-nd f = with-nd-arg (toND f)

----------------------------------------------------------------------
-- Some operations to define properties of non-deterministic values:

-- Count the number of values:
#vals : {A : Set} → ND A → ℕ
#vals (Val _) = 1
#vals (t1 ?? t2) = #vals t1 + #vals t2

-- Extract the list of all values:
vals-of : {A : Set} → ND A → 𝕃 A
vals-of (Val v)    = v :: []
vals-of (t1 ?? t2) = vals-of t1 ++ vals-of t2

-- All values in a Boolean tree are true:
always : ND 𝔹 → 𝔹
always (Val b)    = b
always (t1 ?? t2) = always t1 && always t2

-- There exists some true value in a Boolean tree:
eventually : ND 𝔹 → 𝔹
eventually (Val b)    = b
eventually (t1 ?? t2) = eventually t1 || eventually t2

-- There is not value:
failing : {A : Set} → ND A → 𝔹
failing (Val _)    = ff
failing (t1 ?? t2) = failing t1 && failing t2

-- All non-deterministic values satisfy a given predicate:
_satisfy_ : {A : Set} → ND A → (A → 𝔹) → 𝔹
(Val n)    satisfy p = p n
(t1 ?? t2) satisfy p = t1 satisfy p && t2 satisfy p

-- Every value in a tree is equal to the second argument w.r.t. a
-- comparison function provided as the first argument:
every : {A : Set} → (eq : A → A → 𝔹) → A → ND A → 𝔹
every eq x xs = xs satisfy (eq x)

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

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


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

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

open import LogicalFormulae
open import Functions.Definition

module Functions.Lemmas where

invertibleImpliesBijection : {a b : _} {A : Set a} {B : Set b} {f : A → B} → Invertible f → Bijection f
Bijection.inj (invertibleImpliesBijection {a} {b} {A} {B} {f} record { inverse = inverse ; isLeft = isLeft ; isRight = isRight }) {x} {y} fx=fy = ans
  where
    bl : inverse (f x) ≡ inverse (f y)
    bl = applyEquality inverse fx=fy
    ans : x ≡ y
    ans rewrite equalityCommutative (isRight x) | equalityCommutative (isRight y) = bl
Bijection.surj (invertibleImpliesBijection {a} {b} {A} {B} {f} record { inverse = inverse ; isLeft = isLeft ; isRight = isRight }) y = (inverse y , isLeft y)

bijectionImpliesInvertible : {a b : _} {A : Set a} {B : Set b} {f : A → B} → Bijection f → Invertible f
Invertible.inverse (bijectionImpliesInvertible record { inj = inj ; surj = surj }) b = underlying (surj b)
Invertible.isLeft (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) b with surj b
Invertible.isLeft (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) b | a , prop = prop
Invertible.isRight (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) a with surj (f a)
Invertible.isRight (bijectionImpliesInvertible {f = f} record { inj = property ; surj = surj }) a | a₁ , b = property b

injComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Injection f → Injection g → Injection (g ∘ f)
injComp {f = f} {g} propF propG pr = propF (propG pr)

surjComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Surjection f → Surjection g → Surjection (g ∘ f)
surjComp {f = f} {g} propF propG c with propG c
surjComp {f = f} {g} propF propG c | b , pr with propF b
surjComp {f = f} {g} propF propG c | b , pr | a , pr2 = a , pr'
  where
    pr' : g (f a) ≡ c
    pr' rewrite pr2 = pr

bijectionComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Bijection f → Bijection g → Bijection (g ∘ f)
Bijection.inj (bijectionComp bijF bijG) = injComp (Bijection.inj bijF) (Bijection.inj bijG)
Bijection.surj (bijectionComp bijF bijG) = surjComp (Bijection.surj bijF) (Bijection.surj bijG)

compInjRightInj : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Injection (g ∘ f) → Injection f
compInjRightInj {f = f} {g} property {x} {y} fx=fy = property (applyEquality g fx=fy)

compSurjLeftSurj : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Surjection (g ∘ f) → Surjection g
compSurjLeftSurj {f = f} {g} property b with property b
compSurjLeftSurj {f = f} {g} property b | a , b1 = f a , b1

injectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Injection f → ({x : A} → f x ≡ g x) → Injection g
injectionPreservedUnderExtensionalEq {A = A} {B} {f} {g} property prop {x} {y} gx=gy = property (transitivity (prop {x}) (transitivity gx=gy (equalityCommutative (prop {y}))))

surjectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Surjection f → ({x : A} → f x ≡ g x) → Surjection g
surjectionPreservedUnderExtensionalEq {f = f} {g} surj ext b with surj b
surjectionPreservedUnderExtensionalEq {f = f} {g} surj ext b | a , pr = a , transitivity (equalityCommutative ext) pr

bijectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Bijection f → ({x : A} → f x ≡ g x) → Bijection g
Bijection.inj (bijectionPreservedUnderExtensionalEq record { inj = inj ; surj = surj } ext) = injectionPreservedUnderExtensionalEq inj ext
Bijection.surj (bijectionPreservedUnderExtensionalEq record { inj = inj ; surj = surj } ext) = surjectionPreservedUnderExtensionalEq surj ext

inverseIsInvertible : {a b : _} {A : Set a} {B : Set b} {f : A → B} → (inv : Invertible f) → Invertible (Invertible.inverse inv)
Invertible.inverse (inverseIsInvertible {f = f} inv) = f
Invertible.isLeft (inverseIsInvertible {f = f} inv) b = Invertible.isRight inv b
Invertible.isRight (inverseIsInvertible {f = f} inv) a = Invertible.isLeft inv a

idIsBijective : {a : _} {A : Set a} → Bijection (id {a} {A})
Bijection.inj idIsBijective pr = pr
Bijection.surj idIsBijective b = b , refl

functionCompositionExtensionallyAssociative : {a b c d : _} {A : Set a} {B : Set b} {C : Set c} {D : Set d} → (f : A → B) → (g : B → C) → (h : C → D) → (x : A) → (h ∘ (g ∘ f)) x ≡ ((h ∘ g) ∘ f) x
functionCompositionExtensionallyAssociative f g h x = refl


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

open import LogicalFormulae
open import Setoids.Setoids
open import Groups.Definition

module Groups.DirectSum.Definition {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) where

open import Setoids.Product S T

directSumGroup : Group productSetoid (λ x1 y1 → (((_&&_.fst x1) ·A (_&&_.fst y1)) ,, ((_&&_.snd x1) ·B (_&&_.snd y1))))
Group.+WellDefined directSumGroup (s ,, t) (u ,, v) = Group.+WellDefined G s u ,, Group.+WellDefined H t v
Group.0G directSumGroup = (Group.0G G ,, Group.0G H)
Group.inverse directSumGroup (g1 ,, H1) = (Group.inverse G g1) ,, (Group.inverse H H1)
Group.+Associative directSumGroup = Group.+Associative G ,, Group.+Associative H
Group.identRight directSumGroup = Group.identRight G ,, Group.identRight H
Group.identLeft directSumGroup = Group.identLeft G ,, Group.identLeft H
Group.invLeft directSumGroup = Group.invLeft G ,, Group.invLeft H
Group.invRight directSumGroup = Group.invRight G ,, Group.invRight H


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.MaybeEmb {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation

-- Any level can be embedded into the highest level.
maybeEmb : ∀ {l A Γ}
         → Γ ⊩⟨ l ⟩ A
         → Γ ⊩⟨ ¹ ⟩ A
maybeEmb {⁰} [A] = emb′ 0<1 [A]
maybeEmb {¹} [A] = [A]

-- The lowest level can be embedded in any level.
maybeEmb′ : ∀ {l A Γ}
          → Γ ⊩⟨ ⁰ ⟩ A
          → Γ ⊩⟨ l ⟩ A
maybeEmb′ {⁰} [A] = [A]
maybeEmb′ {¹} [A] = emb′ 0<1 [A]

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
{-# OPTIONS --cubical --no-import-sorts #-}
module Cubical.Codata.Conat where

open import Cubical.Codata.Conat.Base public

open import Cubical.Codata.Conat.Properties public


text:
-- Andreas, 2015-07-16 issue reported by G.Allais

-- This ought to pass, ideally, but the lack of positivity polymorphism
-- does not allow for a precise analysis of the composition operator.
--
-- Subsequently, the positivity analysis for tabulate returns no
-- positivity info for all arguments, leading to a rejection of
-- Command₃.

-- {-# OPTIONS -v tc.pos:10 #-}

open import Common.Product
open import Common.List

record ⊤ {a} : Set a where

_∘_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

postulate
  String : Set

USL = List String

data _∈_ a : USL → Set where
  z : ∀ {xs}             → a ∈ (a ∷ xs)
  s : ∀ {b xs} → a ∈ xs → a ∈ (b ∷ xs)

[Fields] : (args : USL) → Set₁
[Fields] []         =  ⊤
[Fields] (_ ∷ args) = Set × [Fields] args

[tabulate] : (args : USL) (ρ : {arg : _} (pr : arg ∈ args) → Set) → [Fields] args
[tabulate] []          ρ = _
[tabulate] (arg ∷ args) ρ = ρ z , [tabulate] args (λ x → ρ (s x))

[Record] : (args : USL) (f : [Fields] args) → Set
[Record] []          _        = ⊤
[Record] (hd ∷ args) (f , fs) = f × [Record] args fs

record Fields (args : USL) : Set₁ where
  constructor mkFields
  field
    fields : [Fields] args
open Fields public

record Record (args : USL) (f : Fields args) : Set where
  constructor mkRecord
  field
    content : [Record] args (fields f)
open Record public

module WORKS where

  tabulate : {args : USL} (ρ : {arg : _} (pr : arg ∈ args) → Set) → Fields args
  tabulate {args = args} ρ = mkFields ([tabulate] args ρ)  -- WORKS
  -- tabulate {args = args} = mkFields ∘ [tabulate] args -- FAILS

  mutual

    data Command₁ : Set where
      mkCommand : (modifierNames : USL) →
                  Record modifierNames (tabulate (λ {s} _ → Modifier s)) → Command₁

    record Command₂ : Set where
      inductive
      field
        modifierNames : USL
        modifiers     : [Record] modifierNames ([tabulate] _ (λ {s} _ → Modifier s))

    record Command₃ : Set where
      inductive
      field
        modifierNames : USL
        modifiers     : Record modifierNames (tabulate (λ {s} _ → Modifier s))

    data Modifier (name : String) : Set where
      command₁ : Command₁ → Modifier name
      command₂ : Command₂ → Modifier name
      command₃ : Command₃ → Modifier name

module FAILS where

  tabulate : {args : USL} (ρ : {arg : _} (pr : arg ∈ args) → Set) → Fields args
  -- tabulate {args = args} ρ = mkFields ([tabulate] args ρ)  -- WORKS
  tabulate {args = args} = mkFields ∘ [tabulate] args -- FAILS

  mutual

    data Command₁ : Set where
      mkCommand : (modifierNames : USL) →
                  Record modifierNames (tabulate (λ {s} _ → Modifier s)) → Command₁

    record Command₂ : Set where
      inductive
      field
        modifierNames : USL
        modifiers     : [Record] modifierNames ([tabulate] _ (λ {s} _ → Modifier s))

    record Command₃ : Set where
      inductive
      field
        modifierNames : USL
        modifiers     : Record modifierNames (tabulate (λ {s} _ → Modifier s))

    data Modifier (name : String) : Set where
      command₁ : Command₁ → Modifier name
      command₂ : Command₂ → Modifier name
      command₃ : Command₃ → Modifier name

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module ReCaseSplit where

data Bool : Set where
  true : Bool
  false : Bool
  maybe : Bool

_func : Bool -> Bool
maybe func = ?
false func  = false
(true) func  = true

func2 : Bool -> Bool
func2 = λ{false → false ; (true) → true}

open import IO.Primitive

func3 : IO Bool
func3 = return false

func4 : IO Bool
func4 = do
  false <- func3
    where true -> return true
  return false

module SubModule where

 func5 : Bool -> Bool
 func5 maybe = ?
 func5 false = false
 func5 true =  func6 true
    where func6 : Bool -> Bool
          func6 maybe = ?
          func6 false = false
          func6 true = true


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

open import Fragment.Equational.Theory

module Fragment.Equational.Model.Base (Θ : Theory) where

open import Fragment.Equational.Model.Satisfaction {Σ Θ}
open import Fragment.Algebra.Algebra (Σ Θ) hiding (∥_∥/≈)
open import Fragment.Algebra.Free (Σ Θ)

open import Level using (Level; _⊔_; suc)
open import Function using (_∘_)
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ)
open import Relation.Binary using (Setoid)

private
  variable
    a ℓ : Level

Models : Algebra {a} {ℓ} → Set (a ⊔ ℓ)
Models S = ∀ {n} → (eq : eqs Θ n) → S ⊨ (Θ ⟦ eq ⟧ₑ)

module _ (S : Setoid a ℓ) where

  record IsModel : Set (a ⊔ ℓ) where
    field
      isAlgebra : IsAlgebra S
      models    : Models (algebra S isAlgebra)

    open IsAlgebra isAlgebra public

record Model : Set (suc a ⊔ suc ℓ) where
  field
    ∥_∥/≈   : Setoid a ℓ
    isModel : IsModel ∥_∥/≈

  ∥_∥ₐ : Algebra
  ∥_∥ₐ = algebra ∥_∥/≈ (IsModel.isAlgebra isModel)

  ∥_∥ₐ-models : Models ∥_∥ₐ
  ∥_∥ₐ-models = IsModel.models isModel

  open Algebra (algebra ∥_∥/≈ (IsModel.isAlgebra isModel))
    hiding (∥_∥/≈) public

open Model public

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

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

module Codata.Colist.Bisimilarity where

open import Level using (_⊔_)
open import Size
open import Codata.Thunk
open import Codata.Colist
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)

data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) :
           (xs : Colist A ∞) (ys : Colist B ∞) → Set (r ⊔ a ⊔ b) where
  []  : Bisim R i [] []
  _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys → Bisim R i (x ∷ xs) (y ∷ ys)

module _ {a r} {A : Set a} {R : A → A → Set r} where

 reflexive : Reflexive R → ∀ {i} → Reflexive (Bisim R i)
 reflexive refl^R {i} {[]}     = []
 reflexive refl^R {i} {r ∷ rs} = refl^R ∷ λ where .force → reflexive refl^R

module _ {a b} {A : Set a} {B : Set b}
         {r} {P : A → B → Set r} {Q : B → A → Set r} where

 symmetric : Sym P Q → ∀ {i} → Sym (Bisim P i) (Bisim Q i)
 symmetric sym^PQ []       = []
 symmetric sym^PQ (p ∷ ps) = sym^PQ p ∷ λ where .force → symmetric sym^PQ (ps .force)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         {r} {P : A → B → Set r} {Q : B → C → Set r} {R : A → C → Set r} where

 transitive : Trans P Q R → ∀ {i} → Trans (Bisim P i) (Bisim Q i) (Bisim R i)
 transitive trans^PQR []       []       = []
 transitive trans^PQR (p ∷ ps) (q ∷ qs) =
   trans^PQR p q ∷ λ where .force → transitive trans^PQR (ps .force) (qs .force)

-- Pointwise Equality as a Bisimilarity
------------------------------------------------------------------------

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

 infix 1 _⊢_≈_
 _⊢_≈_ : ∀ i → Colist A ∞ → Colist A ∞ → Set ℓ
 _⊢_≈_ = Bisim _≡_

 refl : ∀ {i} → Reflexive (i ⊢_≈_)
 refl = reflexive Eq.refl

 sym : ∀ {i} → Symmetric (i ⊢_≈_)
 sym = symmetric Eq.sym

 trans : ∀ {i} → Transitive (i ⊢_≈_)
 trans = transitive Eq.trans


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

module cw.examples.Examples where

open import cw.examples.Empty public
open import cw.examples.Sphere public
open import cw.examples.Unit public

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- Andreas, 2017-01-13, issue #2402
-- Error message: incomplete pattern matching

-- {-# OPTIONS -v tc.cover:20 #-}

open import Common.Bool

module _ (A B C D E F G H I J K L M O P Q R S T U V W X Y Z : Set) where

test : Bool → Bool
test true = false

-- Reports:
-- Incomplete pattern matching for test. Missing cases:
--   test _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ false

-- Expected:

-- Incomplete pattern matching for test. Missing cases:
--   test false


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

module Relation.Nullary.Discrete.Properties where

open import Relation.Nullary.Discrete
open import Relation.Nullary.Stable.Properties using (Stable≡→isSet)
open import Relation.Nullary.Decidable.Properties using (Dec→Stable; isPropDec)

open import HLevels
open import Level
open import Path

Discrete→isSet :
  Discrete A → isSet A
Discrete→isSet d = Stable≡→isSet (λ x y → Dec→Stable (x ≡ y) (d x y))

isPropDiscrete :
  isProp (Discrete A)
isPropDiscrete f g i x y = isPropDec (Discrete→isSet f x y) (f x y) (g x y) i


text:
-- Andreas, 2014-05-20 Triggered by Andrea Vezzosi & NAD
{-# OPTIONS --copatterns #-}
-- {-# OPTIONS -v tc.conv.coerce:10 #-}

open import Common.Size

-- Andreas, 2015-03-16: currently forbidden
-- Size≤ : Size → SizeUniv
-- Size≤ i = Size< ↑ i

postulate
  Dom    : Size → Set
  mapDom : ∀ i (j : Size< (↑ i)) → Dom i → Dom j

record ∞Dom i : Set where
  field
    force : ∀ (j : Size< i) → Dom j

∞mapDom : ∀ i (j : Size< (↑ i)) → ∞Dom i → ∞Dom j
∞Dom.force (∞mapDom i j x) k = mapDom k k (∞Dom.force x k)

-- The second k on the rhs has type
--   k : Size< j
-- and should have type
--   k : Size≤ k = Size< ↑ k
-- Since j <= ↑ k does not hold (we have only k < j),
-- we cannot do the usual subtyping  Size< j <= Size≤ k,
-- but we have to use the "singleton type property"
--   k : Size< ↑ k


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

open import PathInduction

module Pushout {i} {j} {k} where

{-<Pushout>-}
record Span : Type (lsucc (lmax (lmax i j) k)) where
  constructor span
  field
    A  : Type i
    B  : Type j
    C  : Type k
    f  : C → A
    g  : C → B

postulate
  Pushout : Span → Type (lmax (lmax i j) k)

module _ {d : Span} where

  open Span d

  postulate
    inl   : A → Pushout d
    inr   : B → Pushout d
    push  : (c : C) → inl (f c) == inr (g c)

  module _ {l} {P : Pushout d → Type l}
    (inl*   : (a : A) → P (inl a))
    (inr*   : (b : B) → P (inr b))
    (push*  : (c : C) → inl* (f c) == inr* (g c) [ P ↓ push c ])  where

    postulate
      Pushout-elim  : (x : Pushout d) → P x
      inl-β         : (a : A) → (Pushout-elim (inl a) ↦ inl* a)
      inr-β         : (b : B) → (Pushout-elim (inr b) ↦ inr* b)
      {-# REWRITE inl-β #-}
      {-# REWRITE inr-β #-}
      push-βd'      : (c : C) → (apd Pushout-elim (push c) == push* c)
{-</>-}

  -- Makes the arguments of [push-βd] implicit
  push-βd : ∀ {l} {P : Pushout d → Type l}
    {inl*  : (a : A) → P (inl a)}
    {inr*  : (b : B) → P (inr b)}
    {push* : (c : C) → inl* (f c) == inr* (g c) [ P ↓ push c ]}
    → (c : C) → apd (Pushout-elim inl* inr* push*) (push c) == push* c
  push-βd = push-βd' _ _ _

  -- Non-dependent elimination rule and corresponding reduction rule

{-<PushoutRec>-}
  Pushout-rec : ∀ {l} {D : Type l}
      (inl*  : A → D)
      (inr*  : B → D)
      (push* : (c : C) → inl* (f c) == inr* (g c))
      → Pushout d → D
  Pushout-rec inl* inr* push* = Pushout-elim inl* inr* (λ c → ↓-cst-in (push* c))

  push-β : ∀ {l} {D : Type l}
      {inl*  : A → D}
      {inr*  : B → D}
      {push* : (c : C) → inl* (f c) == inr* (g c)}
      → (c : C) → ap (Pushout-rec inl* inr* push*) (push c) == push* c
  push-β c = apd=cst-in (push-βd c)
{-</>-}

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


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

module Definition.Conversion.Reduction where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.Conversion

-- Weak head expansion of algorithmic equality of types.
reductionConv↑ : ∀ {A A′ B B′ Γ}
               → Γ ⊢ A ⇒* A′
               → Γ ⊢ B ⇒* B′
               → Γ ⊢ A′ [conv↑] B′
               → Γ ⊢ A  [conv↑] B
reductionConv↑ A⇒* B⇒* ([↑] A″ B″ D D′ whnfA″ whnfB″ A″<>B″) =
  [↑] A″ B″ (A⇒* ⇨* D) (B⇒* ⇨* D′) whnfA″ whnfB″ A″<>B″

-- Weak head expansion of algorithmic equality of terms.
reductionConv↑Term : ∀ {t t′ u u′ A B Γ}
                   → Γ ⊢ A ⇒* B
                   → Γ ⊢ t ⇒* t′ ∷ B
                   → Γ ⊢ u ⇒* u′ ∷ B
                   → Γ ⊢ t′ [conv↑] u′ ∷ B
                   → Γ ⊢ t  [conv↑] u  ∷ A
reductionConv↑Term A⇒* t⇒* u⇒* ([↑]ₜ B′ t″ u″ D d d′ whnfB′ whnft″ whnfu″ t″<>u″) =
  [↑]ₜ B′ t″ u″
       (A⇒* ⇨* D)
       ((conv* t⇒* (subset* D)) ⇨∷* d)
       ((conv* u⇒* (subset* D)) ⇨∷* d′)
       whnfB′ whnft″ whnfu″ t″<>u″


text:
-- 2011-09-15 posted by Nisse, variant of Issue292e
-- {-# OPTIONS --show-implicit -v tc.lhs.unify:15 #-}
module Issue292-16b where

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

postulate
  A : Set
  f : A → A

data C (A : Set)(f : A → A) : A → Set where
  c : ∀ x → C A f (f x)

record Box : Set where
  constructor box
  field
    a : A
    b : C A f a

test : ∀ {x₁ x₂} → box (f x₁) (c x₁) ≡ box (f x₂) (c x₂) → x₁ ≡ x₂
test refl = refl

-- We recover from the heteogenerous
--
--   c x₁ : C A f (f x₁) =?= c₂ x₂ : C A f (f x₂)
--
-- to the homogeneous
--
--   x₁ =?= x₂ : A
--
-- since the parameters to C are syntactically equal on lhs and rhs


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition

module Fields.CauchyCompletion.Definition {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open TotallyOrderedRing order
open Ring R
open Group additiveGroup
open Field F

open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order
open import Rings.Orders.Total.Cauchy order
open import Groups.Lemmas additiveGroup

cauchyWellDefined : {s1 s2 : Sequence A} → ((m : ℕ) → index s1 m ∼ index s2 m) → cauchy s1 → cauchy s2
cauchyWellDefined {s1} {s2} prop c e 0<e with c e 0<e
... | N , pr = N , λ {m} {n} N<m N<n → <WellDefined (absWellDefined _ _ (+WellDefined (prop m) (inverseWellDefined (prop n)))) reflexive (pr N<m N<n)

record CauchyCompletion : Set (m ⊔ o) where
  field
    elts : Sequence A
    converges : (cauchy elts)

injection : A → CauchyCompletion
CauchyCompletion.elts (injection a) = constSequence a
CauchyCompletion.converges (injection a) = (λ ε 0<e → 0 , λ {m} {n} _ _ → <WellDefined (symmetric (identityOfIndiscernablesRight _∼_ (absWellDefined (index (constSequence a) m + inverse (index (constSequence a) n)) 0R (t m n)) absZero)) reflexive 0<e)
  where
    t : (m n : ℕ) → index (constSequence a) m + inverse (index (constSequence a) n) ∼ 0R
    t m n = identityOfIndiscernablesLeft _∼_ (identityOfIndiscernablesLeft _∼_ invRight (equalityCommutative (applyEquality (λ i → a + inverse i) (indexAndConst a n)))) (applyEquality (_+ inverse (index (constSequence a) n)) (equalityCommutative (indexAndConst a m)))

-- Some slightly odd things here relating to equality rather than equivalence. Ultimately this is here so we can say Q → R is a genuine injection, not just a setoid one.
private
  lemma : {x y : CauchyCompletion} → x ≡ y → CauchyCompletion.elts x ≡ CauchyCompletion.elts y
  lemma {x} {.x} refl = refl

CInjection' : Injection injection
CInjection' pr = headInjective (lemma pr)


text:
--2010-09-28

module AbsurdIrrelevance where

data Empty : Set where

absurd : {A : Set} -> .Empty -> A
absurd ()

max_stars_repo_name: asr/agda-kanso


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

open import Cubical.Core.Everything

open import Cubical.Data.Nat

data ℤ : Type₀ where
  pos    : (n : ℕ) → ℤ
  negsuc : (n : ℕ) → ℤ

neg : (n : ℕ) → ℤ
neg zero = pos zero
neg (suc n) = negsuc n

infix 100 -_
-_ : ℕ → ℤ
-_ = neg

{-# DISPLAY pos n = n #-}
{-# DISPLAY negsuc n = - (suc n) #-}

sucInt : ℤ → ℤ
sucInt (pos n)          = pos (suc n)
sucInt (negsuc zero)    = pos zero
sucInt (negsuc (suc n)) = negsuc n

predInt : ℤ → ℤ
predInt (pos zero)    = negsuc zero
predInt (pos (suc n)) = pos n
predInt (negsuc n)    = negsuc (suc n)

-- Natural number and negative integer literals for ℤ

open import Cubical.Data.Nat.Literals public

instance
  fromNatℤ : FromNat ℤ
  fromNatℤ = record { Constraint = λ _ → ⊤ ; fromNat = λ n → pos n }

instance
  negativeℤ : Negative ℤ
  negativeℤ = record { Constraint = λ _ → ⊤ ; fromNeg = λ n → neg n }


text:
open import Oscar.Prelude

module Oscar.Class.[IsExtensionB] where

record [IsExtensionB]
  {a} {A : Ø a}
  {b} (B : A → Ø b)
  : Ø₀ where
  constructor ∁
  no-eta-equality


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

open import HoTT
open import stash.modalities.gbm.GbmUtil

module stash.modalities.gbm.PushoutMono where

  --
  --  The goal of this file is to prove the following:
  --  Suppose we have a pushout
  --
  --        g
  --    C ------> B
  --    v         |
  --    |         |
  --  f |         |
  --    v         v
  --    A ------> D
  --
  --  and the map f is a monomorphism.  Then the square
  --  is also a pullback.
  --

  is-mono : ∀ {i j} {A : Type i} {B : Type j} → (A → B) → Type _
  is-mono {B = B} f = (b : B) → has-level (S ⟨-2⟩) (hfiber f b)

  mono-eq : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a₀ a₁ : A}
    (p : f a₀ == f a₁) → is-mono f → a₀ == a₁
  mono-eq f {a₀} {a₁} p ism = ! (fst= (fst (ism (f a₁) (a₁ , idp) (a₀ , p))))

  mono-eq-idp : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a : A}
    → (is-m : is-mono f) → mono-eq f {a₀ = a} idp is-m == idp
  mono-eq-idp f {a} ism = ap (λ x → ! (fst= x)) (snd (ism (f a) (a , idp) (a , idp)) idp)

  mono-eq-ap : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a₀ a₁ : A}
    (p : f a₀ == f a₁) → (is-m : is-mono f) → ap f (mono-eq f p is-m) == p
  mono-eq-ap f {a₀} {a₁} p ism =
    ap f (! (fst= α)) =⟨ ! (!-ap f (fst= α)) ⟩
    ! (ap f (fst= α)) =⟨ ! (∙-unit-r (! (ap f (fst= α)))) ⟩
    ! (ap f (fst= α)) ∙ idp =⟨ ↓-app=cst-out (snd= α) |in-ctx (λ x → ! (ap f (fst= α)) ∙ x) ⟩
    ! (ap f (fst= α)) ∙ ap f (fst= α) ∙ p =⟨ ! (∙-assoc (! (ap f (fst= α))) (ap f (fst= α)) p) ⟩
    (! (ap f (fst= α)) ∙ ap f (fst= α)) ∙ p =⟨ !-inv-l (ap f (fst= α)) |in-ctx (λ x → x ∙ p) ⟩
    p ∎

    where α = fst (ism (f a₁) (a₁ , idp) (a₀ , p))

  ap-lem : ∀ {i j k} {A : Type i} {B : A → Type j} {C : Type k} (f : Σ A B → C)
       {a₀ a₁ : A} {p : a₀ == a₁} {b₀ : B a₀} {b₁ : B a₁}
       (q : b₀ == b₁ [ B ↓ p ]) → ap f (pair= p q) == ↓-cst-out (↓-Π-out (apd (curry f) p) q)
  ap-lem f {p = idp} idp = idp

  Lift-Unit-is-contr : ∀ {i} → is-contr (Lift {j = i} ⊤)
  Lift-Unit-is-contr = equiv-preserves-level (lower-equiv ⁻¹) Unit-is-contr

  Lift-Unit-is-prop : ∀ {i} → is-prop (Lift {j = i} ⊤)
  Lift-Unit-is-prop = contr-is-prop Lift-Unit-is-contr

  module MonoLemma {i} (s : Span {i} {i} {i}) (m : is-mono (Span.f s)) where

    open Span s

    private
      D = Pushout s

    mleft : A → D
    mleft = left

    mright : B → D
    mright = right

    mglue : (c : C) → mleft (f c) == mright (g c)
    mglue c = glue c

    -- Construct a fibration over the pushout
    -- whose total space is equivalent to B

    glue-equiv : (c : C) → hfiber f (f c) ≃ Lift {j = i} ⊤
    glue-equiv c = contr-equiv-LiftUnit (inhab-prop-is-contr (c , idp) (m (f c)))

    -- Now, I claim that the values of this fibration are props.
    -- How do you prove this?

    module B' = PushoutRec {d = s} (hfiber f) (cst (Lift ⊤)) (ua ∘ glue-equiv)

    B' : (d : D) → Type i
    B' = B'.f

    B'-β : (c : C) → ap B' (glue c) == ua (glue-equiv c)
    B'-β c = B'.glue-β c

    B'-is-prop : (d : D) → is-prop (B' d)
    B'-is-prop = Pushout-elim (λ a → m a) (λ b → Lift-Unit-is-prop)
      (λ c → prop-lemma (λ z → is-prop (B' z) , is-prop-is-prop) (mglue c) (m (f c))
      Lift-Unit-is-prop)

    B'-prop : (d : D) → hProp i
    B'-prop d = B' d , B'-is-prop d

    B'-pth-in : ∀ {a b} (p : mleft a == mright b) (x : B' (mleft a)) (y : B' (mright b))
      → x == y [ B' ↓ p ]
    B'-pth-in p x y = prop-lemma B'-prop p x y

    B'-pth-in' : ∀ {a b} (p : mright b == mleft a) (x : B' (mleft a)) (y : B' (mright b))
      → y == x [ B' ↓ p ]
    B'-pth-in' p x y = prop-lemma B'-prop p y x

    cpth : (c : C) → (c , idp) == (lift unit) [ B' ↓ glue c ]
    cpth c = fst (pths-ovr-contr B'-prop (glue c) (c , idp) (lift unit))

    -- Yeah, these triples of data seem to come up a bunch
    -- the point is, such data is contractible...
    data-contr : (c : C) → is-contr (Σ (B' (left (f c))) (λ l → Σ (B' (right (g c))) (λ r → l == r [ B' ↓ glue c ])))
    data-contr c = Σ-level (inhab-prop-is-contr (c , idp) (m (f c)))
      (λ l → Σ-level Lift-Unit-is-contr (λ r → pths-ovr-contr B'-prop (glue c) l r))

    data-elim : (c : C) (P : (l : B' (left (f c))) (r : B' (right (g c))) → (l == r [ B' ↓ glue c ]) → Type i)
                → (t : Σ (B' (left (f c))) (λ l → Σ (B' (right (g c))) (λ r → l == r [ B' ↓ glue c ])))
                → P (fst t) (fst (snd t)) (snd (snd t))
                → (l : B' (left (f c))) → (r : B' (right (g c))) → (q : l == r [ B' ↓ glue c ]) → P l r q
    data-elim c P t x l r q = transport (λ { (l₀ , r₀ , q₀) → P l₀ r₀ q₀ })
      (contr-has-all-paths (data-contr c) _ _) x

    module _ where

      private

        to : B → Σ D B'
        to b = mright b , lift unit

        module From = PushoutElim {d = s} {P = λ d → B' d → B}
          (λ a e → g (fst e))
          (λ b _ → b)
          (λ c → ↓-Π-in (λ {l} {r} q → ↓-cst-in (ap g (mono-eq f (snd l) m))))

        from : Σ D B' → B
        from = uncurry $ From.f

        to-from : (db : Σ D B') → to (from db) == db
        to-from = uncurry $ Pushout-elim lem₀ (λ b _ → idp)
          (λ c → ↓-Π-in (λ {l} {r} q → ↓-app=idf-in (lem₁ c l r q)))

          where lem₀ : (a : A) (l : B' (left a)) → to (from (left a , l)) == left a , l
                lem₀ .(f c) (c , idp) = ! (pair= (mglue c) (cpth c))

                P : (c : C) (l : B' (left (f c))) (r : B' (right (g c))) (q : l == r [ B' ↓ glue c ]) → Type i
                P c l r q = lem₀ (f c) l ∙' pair= (glue c) q ==
                            ap (λ v → to (from v)) (pair= (glue c) q) ∙ idp

                lem₂ : (c : C) → P c (c , idp) (lift unit) (cpth c)
                lem₂ c = ! (pair= (glue c) (cpth c)) ∙' pair= (glue c) (cpth c)
                           =⟨ !-inv'-l (pair= (glue c) (cpth c)) ⟩
                         idp =⟨ ! (mono-eq-idp f m) |in-ctx (λ x → ap to (ap g x))  ⟩
                         ap to (ap g (mono-eq f idp m))
                           =⟨ ! (↓-cst-β (pair= (glue c) (cpth c)) (ap g (mono-eq f idp m))) |in-ctx (λ x → ap to x) ⟩
                         ap to (↓-cst-out (↓-cst-in {p = (pair= (glue c) (cpth c))} (ap g (mono-eq f idp m))))
                           =⟨ ! (↓-Π-β (λ {l} {r} q → ↓-cst-in (ap g (mono-eq f (snd l) m))) (cpth c)) |in-ctx (λ x → ap to (↓-cst-out x)) ⟩
                         ap to (↓-cst-out (↓-Π-out (↓-Π-in (λ {l} {r} q → ↓-cst-in (ap g (mono-eq f (snd l) m)))) (cpth c)))
                           =⟨ ! (From.glue-β c) |in-ctx (λ x → ap to (↓-cst-out (↓-Π-out x (cpth c)))) ⟩
                         ap to (↓-cst-out (↓-Π-out (apd (curry from) (glue c)) (cpth c)))
                           =⟨ ! (ap-lem from (cpth c)) |in-ctx (λ x → ap to x) ⟩
                         ap to (ap from (pair= (glue c) (cpth c)))
                           =⟨ ∘-ap to from (pair= (glue c) (cpth c)) ⟩
                         ap (to ∘ from) (pair= (glue c) (cpth c))
                           =⟨ ! (∙-unit-r _) ⟩
                         ap (to ∘ from) (pair= (glue c) (cpth c)) ∙ idp ∎

                lem₁ : (c : C) (l : B' (left (f c))) (r : B' (right (g c))) (q : l == r [ B' ↓ glue c ])
                  → lem₀ (f c) l ∙' pair= (glue c) q ==
                     ap (λ v → to (from v)) (pair= (glue c) q) ∙ idp
                lem₁ c l r q = data-elim c (P c) ((c , idp) , (lift unit , cpth c)) (lem₂ c) l r q

      B≃B' : B ≃ Σ D B'
      B≃B' = equiv to from to-from (λ b → idp)

    -- From the above equivalence, we can prove that
    -- mright is also a mono
    mright-is-mono : is-mono mright
    mright-is-mono d = equiv-preserves-level (lem ⁻¹ ∘e (hfiber-fst d) ⁻¹) (B'-is-prop d)

      where lem : hfiber mright d ≃ hfiber fst d
            lem = hfiber-sq-eqv mright fst (fst B≃B') (idf D) (comm-sqr (λ b → idp)) (snd B≃B') (idf-is-equiv D) d

    -- Pulling back over A, we should have a space
    -- equivalent to C as well as the path spaces
    -- we are interested in.

    C' : Type i
    C' = Σ A (B' ∘ mleft)

    -- Given (b : B) and an element it is equal to in the
    -- the pushout, we can find an element in the fiber which
    -- witnesses that equaltiy

    witness-for : ∀ {a b} (p : mleft a == mright b) → hfiber f a
    witness-for p = transport! B' p (lift unit)

    -- Using the fact that mright is a mono, we can
    -- find a proof of the following
    witness-for-coh₀ : ∀ {a b} (p : mleft a == mright b) → g (fst (witness-for p)) == b
    witness-for-coh₀ {a} {b} p = mono-eq mright lem mright-is-mono

      where c : C
            c = fst (witness-for p)

            lem : mright (g c) == mright b
            lem = ! (mglue c) ∙ ap mleft (snd (witness-for p)) ∙ p

    witness-for-coh₁ : ∀ {a b} (p : mleft a == mright b)
      → (! (ap mleft (snd (witness-for p))) ∙ mglue (fst (witness-for p))) == p
         [ (λ ab → mleft (fst ab) == mright (snd ab)) ↓ (ap (λ x → (a , x)) (witness-for-coh₀ p)) ]
    witness-for-coh₁ {a} p = ↓-ap-in _ (λ b₀ → (a , b₀)) (↓-cst=app-in calc)

      where α = ap mleft (snd (witness-for p))
            β = mglue (fst (witness-for p))

            calc = (! α ∙ β) ∙' ap mright (witness-for-coh₀ p)
                      =⟨ mono-eq-ap mright (! β ∙ α ∙ p) mright-is-mono |in-ctx (λ x → (! α ∙ β) ∙' x) ⟩
                   (! α ∙ β) ∙' ! β ∙ α ∙ p =⟨ ∙'=∙ (! α ∙ β) (! β ∙ α ∙ p) ⟩
                   (! α ∙ β) ∙ ! β ∙ α ∙ p =⟨ ∙-assoc (! α) β (! β ∙ α ∙ p) ⟩
                   ! α ∙ β ∙ ! β ∙ α ∙ p =⟨ ! (∙-assoc β (! β) (α ∙ p)) |in-ctx (λ x → ! α ∙ x) ⟩
                   ! α ∙ (β ∙ ! β) ∙ α ∙ p =⟨ !-inv-r β |in-ctx (λ x → ! α ∙ x ∙ α ∙ p) ⟩
                   ! α ∙ α ∙ p =⟨ ! (∙-assoc (! α) α p) ⟩
                   (! α ∙ α) ∙ p =⟨ !-inv-l α |in-ctx (λ x → x ∙ p) ⟩
                   p ∎

    C'-equiv-pths : C' ≃ Σ (A × B) (λ ab → mleft (fst ab) == mright (snd ab))
    C'-equiv-pths = equiv to from to-from from-to

      where to : C' → Σ (A × B) (λ ab → mleft (fst ab) == mright (snd ab))
            to (a , c , p) = (a , g c) , ! (ap mleft p) ∙ mglue c

            from : Σ (A × B) (λ ab → mleft (fst ab) == mright (snd ab)) → C'
            from ((a , b) , p) = a , witness-for p

            to-from : (x : Σ (A × B) (λ ab → mleft (fst ab) == mright (snd ab))) → to (from x) == x
            to-from ((a , b) , p) = pair= (pair= idp (witness-for-coh₀ p)) (witness-for-coh₁ p)

            from-to : (c' : C') → from (to c') == c'
            from-to (a , c , p) = pair= idp (fst (m _ _ (c , p)))

    C-equiv-C' : C ≃ C'
    C-equiv-C' = equiv to from to-from from-to

      where to : C → C'
            to c = f c , (c , idp)

            from : C' → C
            from (a , c , p) = c

            to-from : (c' : C') → to (from c') == c'
            to-from (a , c , p) = pair= p (fst (pths-ovr-contr (λ a → hfiber f a , m a) p (c , idp) (c , p)))

            from-to : (c : C) → from (to c) == c
            from-to c = idp

    -- Combining the two equivalences from above
    -- gives us the result we want.

    pushout-mono-is-pullback : C ≃ Σ (A × B) (λ ab → mleft (fst ab) == mright (snd ab))
    pushout-mono-is-pullback = C'-equiv-pths ∘e C-equiv-C'


text:
module Examples.Syntax where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.String using (_++_)
open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩)
open import Luau.Syntax.ToString using (exprToString; blockToString)

ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡
  "function(x)\n" ++
  "  return f(x)\n" ++
  "end"
ex1 = refl

ex2 : blockToString(local var "x" ← nil ∙ return (var "x") ∙ done) ≡
  "local x = nil\n" ++
  "return x"
ex2 = refl

ex3 : blockToString(function "f" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "f") ∙ done) ≡
  "local function f(x)\n" ++
  "  return x\n" ++
  "end\n" ++
  "return f"
ex3 = refl


text:
module general-exercises.RunningHaskellCode where

-- To compile code: stack exec -- agda general-exercises/RunningHaskellCode.agda -c

open import Data.String using (String)
open import Agda.Builtin.Unit using (⊤)

-- Working directly with Haskell code, kinda dangerous stuff
--
-- This didn't actually work because all Agda stuff is wrapped around colists
-- and there is even more wrapping around printError to make it work. It is not
-- that it is impossible, it is just a matter of copying the code from
-- `IO.Primitive`, which I don't want to do right now
--
--open import Agda.Builtin.IO using (IO)
--
--{-# FOREIGN GHC import qualified System.IO as SIO #-}
--{-# FOREIGN GHC import qualified Data.Text #-}
--
--postulate printError : String → IO ⊤
--
--{-# COMPILE GHC printError = SIO.hPutStrLn SIO.stderr $ Data.Text.unpack #-}
--
--main = printError "Printing to stderr!"

-- Using the Standard Library
open import IO using (run; putStrLn)

main = run (putStrLn "Hello freaking World!")

-- Exporting Agda binaries to use in Haskell code
--open import Data.Nat using (ℕ; suc; zero)
--
--double : ℕ → ℕ
--double zero = zero
--double (suc n) = suc (suc (double n))
--{-# COMPILE GHC double as doubleNat #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some algebraic structures (not packed up with sets, operations,
-- etc.)
------------------------------------------------------------------------

open import Relation.Binary

module Algebra.Structures where

import Algebra.FunctionProperties as FunctionProperties
open import Data.Product
open import Function
open import Level using (_⊔_)
import Relation.Binary.EqReasoning as EqR

open FunctionProperties using (Op₁; Op₂)

------------------------------------------------------------------------
-- One binary operation

record IsSemigroup {a ℓ} {A : Set a} (≈ : Rel A ℓ)
                   (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isEquivalence : IsEquivalence ≈
    assoc         : Associative ∙
    ∙-cong        : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈

  open IsEquivalence isEquivalence public

record IsMonoid {a ℓ} {A : Set a} (≈ : Rel A ℓ)
                (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isSemigroup : IsSemigroup ≈ ∙
    identity    : Identity ε ∙

  open IsSemigroup isSemigroup public

record IsCommutativeMonoid {a ℓ} {A : Set a} (≈ : Rel A ℓ)
                           (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isSemigroup : IsSemigroup ≈ _∙_
    identityˡ   : LeftIdentity ε _∙_
    comm        : Commutative _∙_

  open IsSemigroup isSemigroup public

  identity : Identity ε _∙_
  identity = (identityˡ , identityʳ)
    where
    open EqR (record { isEquivalence = isEquivalence })

    identityʳ : RightIdentity ε _∙_
    identityʳ = λ x → begin
      (x ∙ ε)  ≈⟨ comm x ε ⟩
      (ε ∙ x)  ≈⟨ identityˡ x ⟩
      x        ∎

  isMonoid : IsMonoid ≈ _∙_ ε
  isMonoid = record
    { isSemigroup = isSemigroup
    ; identity    = identity
    }

record IsGroup {a ℓ} {A : Set a} (≈ : Rel A ℓ)
               (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  infixl 7 _-_
  field
    isMonoid  : IsMonoid ≈ _∙_ ε
    inverse   : Inverse ε _⁻¹ _∙_
    ⁻¹-cong   : _⁻¹ Preserves ≈ ⟶ ≈

  open IsMonoid isMonoid public

  _-_ : FunctionProperties.Op₂ A
  x - y = x ∙ (y ⁻¹)

record IsAbelianGroup
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isGroup : IsGroup ≈ ∙ ε ⁻¹
    comm    : Commutative ∙

  open IsGroup isGroup public

  isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε
  isCommutativeMonoid = record
    { isSemigroup = isSemigroup
    ; identityˡ   = proj₁ identity
    ; comm        = comm
    }

------------------------------------------------------------------------
-- Two binary operations

record IsNearSemiring {a ℓ} {A : Set a} (≈ : Rel A ℓ)
                      (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +-isMonoid    : IsMonoid ≈ + 0#
    *-isSemigroup : IsSemigroup ≈ *
    distribʳ      : * DistributesOverʳ +
    zeroˡ         : LeftZero 0# *

  open IsMonoid +-isMonoid public
         renaming ( assoc       to +-assoc
                  ; ∙-cong      to +-cong
                  ; isSemigroup to +-isSemigroup
                  ; identity    to +-identity
                  )

  open IsSemigroup *-isSemigroup public
         using ()
         renaming ( assoc    to *-assoc
                  ; ∙-cong   to *-cong
                  )

record IsSemiringWithoutOne {a ℓ} {A : Set a} (≈ : Rel A ℓ)
                            (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
    *-isSemigroup         : IsSemigroup ≈ *
    distrib               : * DistributesOver +
    zero                  : Zero 0# *

  open IsCommutativeMonoid +-isCommutativeMonoid public
         hiding (identityˡ)
         renaming ( assoc       to +-assoc
                  ; ∙-cong      to +-cong
                  ; isSemigroup to +-isSemigroup
                  ; identity    to +-identity
                  ; isMonoid    to +-isMonoid
                  ; comm        to +-comm
                  )

  open IsSemigroup *-isSemigroup public
         using ()
         renaming ( assoc       to *-assoc
                  ; ∙-cong      to *-cong
                  )

  isNearSemiring : IsNearSemiring ≈ + * 0#
  isNearSemiring = record
    { +-isMonoid    = +-isMonoid
    ; *-isSemigroup = *-isSemigroup
    ; distribʳ      = proj₂ distrib
    ; zeroˡ         = proj₁ zero
    }

record IsSemiringWithoutAnnihilatingZero
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    -- Note that these structures do have an additive unit, but this
    -- unit does not necessarily annihilate multiplication.
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
    *-isMonoid            : IsMonoid ≈ * 1#
    distrib               : * DistributesOver +

  open IsCommutativeMonoid +-isCommutativeMonoid public
         hiding (identityˡ)
         renaming ( assoc       to +-assoc
                  ; ∙-cong      to +-cong
                  ; isSemigroup to +-isSemigroup
                  ; identity    to +-identity
                  ; isMonoid    to +-isMonoid
                  ; comm        to +-comm
                  )

  open IsMonoid *-isMonoid public
         using ()
         renaming ( assoc       to *-assoc
                  ; ∙-cong      to *-cong
                  ; isSemigroup to *-isSemigroup
                  ; identity    to *-identity
                  )

record IsSemiring {a ℓ} {A : Set a} (≈ : Rel A ℓ)
                  (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero ≈ + * 0# 1#
    zero : Zero 0# *

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

  isSemiringWithoutOne : IsSemiringWithoutOne ≈ + * 0#
  isSemiringWithoutOne = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isSemigroup         = *-isSemigroup
    ; distrib               = distrib
    ; zero                  = zero
    }

  open IsSemiringWithoutOne isSemiringWithoutOne public
         using (isNearSemiring)

record IsCommutativeSemiringWithoutOne
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isSemiringWithoutOne : IsSemiringWithoutOne ≈ + * 0#
    *-comm               : Commutative *

  open IsSemiringWithoutOne isSemiringWithoutOne public

record IsCommutativeSemiring
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (_+_ _*_ : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ _+_ 0#
    *-isCommutativeMonoid : IsCommutativeMonoid ≈ _*_ 1#
    distribʳ              : _*_ DistributesOverʳ _+_
    zeroˡ                 : LeftZero 0# _*_

  private
    module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
    open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
           using () renaming (comm to *-comm)
  open EqR (record { isEquivalence = +-CM.isEquivalence })

  distrib : _*_ DistributesOver _+_
  distrib = (distribˡ , distribʳ)
    where
    distribˡ : _*_ DistributesOverˡ _+_
    distribˡ x y z = begin
      (x * (y + z))        ≈⟨ *-comm x (y + z) ⟩
      ((y + z) * x)        ≈⟨ distribʳ x y z ⟩
      ((y * x) + (z * x))  ≈⟨ *-comm y x ⟨ +-CM.∙-cong ⟩ *-comm z x ⟩
      ((x * y) + (x * z))  ∎

  zero : Zero 0# _*_
  zero = (zeroˡ , zeroʳ)
    where
    zeroʳ : RightZero 0# _*_
    zeroʳ x = begin
      (x * 0#)  ≈⟨ *-comm x 0# ⟩
      (0# * x)  ≈⟨ zeroˡ x ⟩
      0#        ∎

  isSemiring : IsSemiring ≈ _+_ _*_ 0# 1#
  isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = +-isCommutativeMonoid
      ; *-isMonoid            = *-CM.isMonoid
      ; distrib               = distrib
      }
    ; zero                              = zero
    }

  open IsSemiring isSemiring public
         hiding (distrib; zero; +-isCommutativeMonoid)

  isCommutativeSemiringWithoutOne :
    IsCommutativeSemiringWithoutOne ≈ _+_ _*_ 0#
  isCommutativeSemiringWithoutOne = record
    { isSemiringWithoutOne = isSemiringWithoutOne
    ; *-comm               = *-CM.comm
    }

record IsRing
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +-isAbelianGroup : IsAbelianGroup ≈ _+_ 0# -_
    *-isMonoid       : IsMonoid ≈ _*_ 1#
    distrib          : _*_ DistributesOver _+_

  open IsAbelianGroup +-isAbelianGroup public
         renaming ( assoc               to +-assoc
                  ; ∙-cong              to +-cong
                  ; isSemigroup         to +-isSemigroup
                  ; identity            to +-identity
                  ; isMonoid            to +-isMonoid
                  ; inverse             to -‿inverse
                  ; ⁻¹-cong             to -‿cong
                  ; isGroup             to +-isGroup
                  ; comm                to +-comm
                  ; isCommutativeMonoid to +-isCommutativeMonoid
                  )

  open IsMonoid *-isMonoid public
         using ()
         renaming ( assoc       to *-assoc
                  ; ∙-cong      to *-cong
                  ; isSemigroup to *-isSemigroup
                  ; identity    to *-identity
                  )

  zero : Zero 0# _*_
  zero = (zeroˡ , zeroʳ)
    where
    open EqR (record { isEquivalence = isEquivalence })

    zeroˡ : LeftZero 0# _*_
    zeroˡ x = begin
        0# * x                              ≈⟨ sym $ proj₂ +-identity _ ⟩
       (0# * x) +            0#             ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
       (0# * x) + ((0# * x)  + - (0# * x))  ≈⟨ sym $ +-assoc _ _ _ ⟩
      ((0# * x) +  (0# * x)) + - (0# * x)   ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
             ((0# + 0#) * x) + - (0# * x)   ≈⟨ (proj₂ +-identity _ ⟨ *-cong ⟩ refl)
                                                 ⟨ +-cong ⟩
                                               refl ⟩
                    (0# * x) + - (0# * x)   ≈⟨ proj₂ -‿inverse _ ⟩
                             0#             ∎

    zeroʳ : RightZero 0# _*_
    zeroʳ x = begin
      x * 0#                              ≈⟨ sym $ proj₂ +-identity _ ⟩
      (x * 0#) + 0#                       ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
      (x * 0#) + ((x * 0#) + - (x * 0#))  ≈⟨ sym $ +-assoc _ _ _ ⟩
      ((x * 0#) + (x * 0#)) + - (x * 0#)  ≈⟨ sym (proj₁ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
      (x * (0# + 0#)) + - (x * 0#)        ≈⟨ (refl ⟨ *-cong ⟩ proj₂ +-identity _)
                                               ⟨ +-cong ⟩
                                             refl ⟩
      (x * 0#) + - (x * 0#)               ≈⟨ proj₂ -‿inverse _ ⟩
      0#                                  ∎

  isSemiringWithoutAnnihilatingZero
    : IsSemiringWithoutAnnihilatingZero ≈ _+_ _*_ 0# 1#
  isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isMonoid            = *-isMonoid
    ; distrib               = distrib
    }

  isSemiring : IsSemiring ≈ _+_ _*_ 0# 1#
  isSemiring = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    ; zero = zero
    }

  open IsSemiring isSemiring public
         using (isNearSemiring; isSemiringWithoutOne)

record IsCommutativeRing
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isRing : IsRing ≈ + * - 0# 1#
    *-comm : Commutative *

  open IsRing isRing public

  isCommutativeSemiring : IsCommutativeSemiring ≈ + * 0# 1#
  isCommutativeSemiring = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isCommutativeMonoid = record
      { isSemigroup = *-isSemigroup
      ; identityˡ   = proj₁ *-identity
      ; comm        = *-comm
      }
    ; distribʳ              = proj₂ distrib
    ; zeroˡ                 = proj₁ zero
    }

  open IsCommutativeSemiring isCommutativeSemiring public
         using ( *-isCommutativeMonoid
               ; isCommutativeSemiringWithoutOne
               )

record IsLattice {a ℓ} {A : Set a} (≈ : Rel A ℓ)
                 (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isEquivalence : IsEquivalence ≈
    ∨-comm        : Commutative ∨
    ∨-assoc       : Associative ∨
    ∨-cong        : ∨ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
    ∧-comm        : Commutative ∧
    ∧-assoc       : Associative ∧
    ∧-cong        : ∧ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
    absorptive    : Absorptive ∨ ∧

  open IsEquivalence isEquivalence public

record IsDistributiveLattice {a ℓ} {A : Set a} (≈ : Rel A ℓ)
                             (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isLattice    : IsLattice ≈ ∨ ∧
    ∨-∧-distribʳ : ∨ DistributesOverʳ ∧

  open IsLattice isLattice public

record IsBooleanAlgebra
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    isDistributiveLattice : IsDistributiveLattice ≈ ∨ ∧
    ∨-complementʳ         : RightInverse ⊤ ¬ ∨
    ∧-complementʳ         : RightInverse ⊥ ¬ ∧
    ¬-cong                : ¬ Preserves ≈ ⟶ ≈

  open IsDistributiveLattice isDistributiveLattice public


text:
------------------------------------------------------------------------
-- A combination of the delay monad (with the possibility of crashing)
-- and a kind of writer monad yielding colists
------------------------------------------------------------------------

module Lambda.Delay-crash-trace where

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

open import Colist E.equality-with-J as C
  using (Colist; []; _∷_; force)
open import Monad E.equality-with-J
  using (Raw-monad; return; _>>=_; _⟨$⟩_)

open import Delay-monad using (now; later; force)
open import Delay-monad.Bisimilarity as D using (now; later; force)

open import Lambda.Delay-crash using (Delay-crash)

------------------------------------------------------------------------
-- The monad

mutual

  -- A kind of delay monad with the possibility of crashing that also
  -- yields a trace (colist) of values.

  data Delay-crash-trace (A B : Type) (i : Size) : Type where

    -- A result is returned now.

    now : B → Delay-crash-trace A B i

    -- The computation crashes now.

    crash : Delay-crash-trace A B i

    -- A result is possibly returned later. This constructor also
    -- functions as a coinductive cons constructor for the resulting
    -- trace.

    later : A → Delay-crash-trace′ A B i → Delay-crash-trace A B i

    -- An inductive cons constructor for the resulting trace.

    tell : A → Delay-crash-trace A B i → Delay-crash-trace A B i

  record Delay-crash-trace′ (A B : Type) (i : Size) : Type where
    coinductive
    field
      force : {j : Size< i} → Delay-crash-trace A B j

open Delay-crash-trace′ public

------------------------------------------------------------------------
-- Extracting or deleting the trace

-- Returns the trace.

trace : ∀ {A B i} → Delay-crash-trace A B i → Colist A i
trace (now x)     = []
trace crash       = []
trace (later x m) = x ∷ λ { .force → trace (m .force) }
trace (tell x m)  = x ∷ λ { .force → trace m }

-- Erases the trace.

delay-crash :
  ∀ {A B i} → Delay-crash-trace A B i → Delay-crash B i
delay-crash (now x)     = now (just x)
delay-crash crash       = now nothing
delay-crash (later x m) = later λ { .force → delay-crash (m .force) }
delay-crash (tell x m)  = delay-crash m

------------------------------------------------------------------------
-- Delay-crash-trace is a raw monad

-- Bind.

bind : ∀ {i A B C} →
       Delay-crash-trace A B i →
       (B → Delay-crash-trace A C i) →
       Delay-crash-trace A C i
bind (now x)     f = f x
bind crash       f = crash
bind (later x m) f = later x λ { .force → bind (force m) f }
bind (tell x m)  f = tell x (bind m f)

-- Delay-crash-trace is a raw monad.

instance

  raw-monad : ∀ {A i} → Raw-monad (λ B → Delay-crash-trace A B i)
  Raw-monad.return raw-monad = now
  Raw-monad._>>=_  raw-monad = bind

------------------------------------------------------------------------
-- Strong bisimilarity for Delay-crash-trace

module _ {A B : Type} where

  mutual

    -- Strong bisimilarity.

    infix 4 [_]_∼_ [_]_∼′_

    data [_]_∼_ (i : Size) :
           Delay-crash-trace A B ∞ →
           Delay-crash-trace A B ∞ → Type where
      now   : ∀ {x} → [ i ] now x ∼ now x
      crash : [ i ] crash ∼ crash
      later : ∀ {v x y} →
              [ i ] force x ∼′ force y →
              [ i ] later v x ∼ later v y
      tell  : ∀ {v x y} →
              [ i ] x ∼ y →
              [ i ] tell v x ∼ tell v y

    record [_]_∼′_ (i : Size)
             (x : Delay-crash-trace A B ∞)
             (y : Delay-crash-trace A B ∞) : Type where
      coinductive
      field
        force : {j : Size< i} → [ j ] x ∼ y

  open [_]_∼′_ public

  -- Reflexivity.

  reflexive : ∀ {i} x → [ i ] x ∼ x
  reflexive (now _)     = now
  reflexive crash       = crash
  reflexive (later v x) = later λ { .force → reflexive (force x) }
  reflexive (tell v x)  = tell (reflexive x)

  -- Symmetry.

  symmetric : ∀ {i x y} → [ i ] x ∼ y → [ i ] y ∼ x
  symmetric now       = now
  symmetric crash     = crash
  symmetric (later p) = later λ { .force → symmetric (force p) }
  symmetric (tell p)  = tell (symmetric p)

  -- Transitivity.

  transitive : ∀ {i x y z} → [ i ] x ∼ y → [ i ] y ∼ z → [ i ] x ∼ z
  transitive now       now       = now
  transitive crash     crash     = crash
  transitive (later p) (later q) = later λ { .force →
                                     transitive (force p) (force q) }
  transitive (tell p)  (tell q)  = tell (transitive p q)

  -- Equational reasoning combinators.

  infix  -1 _∎
  infixr -2 step-∼ step-≡ _∼⟨⟩_

  _∎ : ∀ {i} x → [ i ] x ∼ x
  _∎ = reflexive

  step-∼ : ∀ {i} x {y z} → [ i ] y ∼ z → [ i ] x ∼ y → [ i ] x ∼ z
  step-∼ _ y∼z x∼y = transitive x∼y y∼z

  syntax step-∼ x y∼z x∼y = x ∼⟨ x∼y ⟩ y∼z

  step-≡ : ∀ {i} x {y z} → [ i ] y ∼ z → x ≡ y → [ i ] x ∼ z
  step-≡ _ y∼z refl = y∼z

  syntax step-≡ x y∼z x≡y = x ≡⟨ x≡y ⟩ y∼z

  _∼⟨⟩_ : ∀ {i} x {y} → [ i ] x ∼ y → [ i ] x ∼ y
  _ ∼⟨⟩ x∼y = x∼y

----------------------------------------------------------------------
-- Monad laws

left-identity :
  ∀ {A B C : Type} x (f : B → Delay-crash-trace A C ∞) →
  [ ∞ ] return x >>= f ∼ f x
left-identity x f = reflexive (f x)

right-identity :
  ∀ {i} {A B : Type} (x : Delay-crash-trace A B ∞) →
  [ i ] x >>= return ∼ x
right-identity (now x)     = now
right-identity crash       = crash
right-identity (later v x) = later λ { .force →
                               right-identity (force x) }
right-identity (tell v x)  = tell (right-identity x)

associativity :
  ∀ {i} {A B C D : Type} →
  (x : Delay-crash-trace A B ∞)
  (f : B → Delay-crash-trace A C ∞)
  (g : C → Delay-crash-trace A D ∞) →
  [ i ] x >>= (λ x → f x >>= g) ∼ x >>= f >>= g
associativity (now x)     f g = reflexive (f x >>= g)
associativity crash       f g = crash
associativity (later v x) f g = later λ { .force →
                                  associativity (force x) f g }
associativity (tell v x)  f g = tell (associativity x f g)

----------------------------------------------------------------------
-- Some preservation lemmas

infixl 5 _>>=-cong_

_>>=-cong_ :
  ∀ {i} {A B C : Type}
    {x y : Delay-crash-trace A B ∞}
    {f g : B → Delay-crash-trace A C ∞} →
  [ i ] x ∼ y → (∀ z → [ i ] f z ∼ g z) →
  [ i ] x >>= f ∼ y >>= g
now     >>=-cong q = q _
crash   >>=-cong q = crash
later p >>=-cong q = later λ { .force → force p >>=-cong q }
tell p  >>=-cong q = tell (p >>=-cong q)

trace-cong :
  ∀ {i} {A B : Type} {x y : Delay-crash-trace A B ∞} →
  [ i ] x ∼ y → C.[ i ] trace x ∼ trace y
trace-cong now       = []
trace-cong crash     = []
trace-cong (later p) = refl ∷ λ { .force → trace-cong (force p) }
trace-cong (tell p)  = refl ∷ λ { .force → trace-cong p }

delay-crash-cong :
  ∀ {i} {A B : Type} {x y : Delay-crash-trace A B ∞} →
  [ i ] x ∼ y → D.[ i ] delay-crash x ∼ delay-crash y
delay-crash-cong now       = now
delay-crash-cong crash     = now
delay-crash-cong (later p) = later λ { .force →
                               delay-crash-cong (force p) }
delay-crash-cong (tell p)  = delay-crash-cong p

------------------------------------------------------------------------
-- More lemmas

-- The delay-crash function commutes with _>>=_ (in a certain sense).

delay-crash->>= :
  ∀ {i A B C} (x : Delay-crash-trace A B ∞)
    {f : B → Delay-crash-trace A C ∞} →
  D.[ i ] delay-crash (x >>= f) ∼
          delay-crash x >>= delay-crash ∘ f
delay-crash->>= (now x)     = D.reflexive _
delay-crash->>= crash       = D.reflexive _
delay-crash->>= (later x m) = later λ { .force →
                                delay-crash->>= (force m) }
delay-crash->>= (tell x m)  = delay-crash->>= m

-- Use of _⟨$⟩_ does not affect the trace.

trace-⟨$⟩ :
  ∀ {i} {A B C : Type} {f : B → C}
  (x : Delay-crash-trace A B ∞) →
  C.[ i ] trace (f ⟨$⟩ x) ∼ trace x
trace-⟨$⟩ (now x)     = []
trace-⟨$⟩ crash       = []
trace-⟨$⟩ (later _ x) = refl ∷ λ { .force → trace-⟨$⟩ (force x) }
trace-⟨$⟩ (tell _ x)  = refl ∷ λ { .force → trace-⟨$⟩ x }

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
module Examples.TestCall where

open import Prelude
open import Libraries.SelectiveReceive
open import Libraries.Call

open SelRec

AddReplyMessage : MessageType
AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ

AddReply : InboxShape
AddReply = [ AddReplyMessage ]ˡ

AddMessage : MessageType
AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ

Calculator : InboxShape
Calculator = [ AddMessage ]ˡ

calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift (lsuc lzero) ⊤) [] (λ _ → [])
calculatorActor = loop
  where
    loop : ∀ {i} → ∞ActorM i Calculator (Lift (lsuc lzero) ⊤) [] (λ _ → [])
    loop .force = receive ∞>>= λ {
      (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) → do
        Z ![t: Z ] ((lift tag) ∷ [ lift (n + m) ]ᵃ )
        strengthen []
        loop
      ; (Msg (S ()) _) }

TestBox : InboxShape
TestBox = AddReply

calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
calltestActor .force = spawn∞ calculatorActor ∞>> do
    x ← call [] Z Z 0
         ((lift 10) ∷ [ lift 32 ]ᵃ)
         ⊆-refl Z
    strengthen []
    return-result x
  where
    return-result : SelRec TestBox (call-select 0 ⊆-refl Z) →
                    ∀ {i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
module Tactic.Nat.Coprime.Problem where

open import Prelude
open import Prelude.List.Relations.All
open import Numeric.Nat.GCD

Atom = Nat

infixl 7 _⊗_
infix  3 _⋈_
infix  2 _⊨_

data Exp : Set where
  atom : (x : Atom) → Exp
  _⊗_ : (a b : Exp) → Exp

data Formula : Set where
  _⋈_ : (a b : Exp) → Formula

data Problem : Set where
  _⊨_ : (Γ : List Formula) (φ : Formula) → Problem

Env = Atom → Nat

⟦_⟧e_ : Exp → Env → Nat
⟦ atom x ⟧e ρ = ρ x
⟦ e ⊗ e₁ ⟧e ρ = ⟦ e ⟧e ρ * ⟦ e₁ ⟧e ρ

⟦_⟧f_ : Formula → Env → Set
⟦ a ⋈ b ⟧f ρ = Coprime (⟦ a ⟧e ρ) (⟦ b ⟧e ρ)

⟦_⟧p'_ : Problem → Env → Set
⟦ Γ ⊨ φ ⟧p' ρ = All (⟦_⟧f ρ) Γ → ⟦ φ ⟧f ρ

⟦_⟧p_ : Problem → Env → Set
⟦ Γ ⊨ φ ⟧p ρ = foldr (λ ψ A → ⟦ ψ ⟧f ρ → A) (⟦ φ ⟧f ρ) Γ

curryProblem : ∀ Q ρ → ⟦ Q ⟧p' ρ → ⟦ Q ⟧p ρ
curryProblem ([]    ⊨ φ) ρ H = H []
curryProblem (x ∷ Γ ⊨ φ) ρ H = λ x → curryProblem (Γ ⊨ φ) ρ (H ∘ (x ∷_))

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
------------------------------------------------------------------------------
-- Testing the erasing of the duplicate definitions required by a conjecture
------------------------------------------------------------------------------

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

module DuplicateAgdaDefinitions2 where

-- We add 4 to the fixities of the standard library.
infix 8 _<_ _≤_
infix 7 _≡_

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

postulate
  D               : Set
  zero true false : D
  succ            : D → D

data _≡_ (x : D) : D → Set where
  refl : x ≡ x

data N : D → Set where
  zN :               N zero
  sN : ∀ {n} → N n → N (succ n)

data Bool : D → Set where
  tB : Bool true
  fB : Bool false
{-# ATP axioms tB fB #-}

postulate
  _<_  : D → D → D
  <-00 : zero < zero             ≡ false
  <-0S : ∀ n → zero < succ n     ≡ true
  <-S0 : ∀ n → succ n < zero     ≡ false
  <-SS : ∀ m n → succ m < succ n ≡ m < n

_≤_ : D → D → D
m ≤ n = m < succ n
{-# ATP definition _≤_ #-}

NLE : D → D → Set
NLE m n = m ≤ n ≡ false
{-# ATP definition NLE #-}

postulate Sx≰0 : ∀ {n} → N n → NLE (succ n) zero

≤-Bool : ∀ {m n} → N m → N n → Bool (m ≤ n)
≤-Bool {n = n} zN Nn = prf
  where postulate prf : Bool (zero ≤ n)
≤-Bool (sN {m} Nm) zN = prf
  where postulate prf : Bool (succ m ≤ zero)
        {-# ATP prove prf Sx≰0 #-}
≤-Bool (sN {m} Nm) (sN {n} Nn) = prf (≤-Bool Nm Nn)
  where postulate prf : Bool (m ≤ n) → Bool (succ m ≤ succ n)

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --safe --without-K #-}
module Data.List.Membership.Propositional.Disjoint {ℓ} {A : Set ℓ} where
import Relation.Binary.PropositionalEquality as P
open import Data.List.Membership.Setoid.Disjoint (P.setoid A) public

max_stars_repo_name: tizmd/agda-distinct-disjoint

max_issues_repo_name: tizmd/agda-distinct-disjoint

max_forks_repo_name: tizmd/agda-distinct-disjoint


text:
{-# OPTIONS --type-in-type --no-pattern-matching #-}
open import Spire.DarkwingDuck.Primitive
module Spire.DarkwingDuck.Derived where

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

subst : (A : Set) (x : A) (y : A) (P : A → Set) → P x → x ≡ y → P y
subst A x y P p = elimEq A x (λ y _ → P y) p y

ISet : Set → Set
ISet I = I → Set

Scope  : Tel → Set
Scope = elimTel (λ _ → Set) ⊤ (λ A B ih → Σ A ih)

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

UncurriedBranches : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
UncurriedBranches E P X = Branches E P → X

CurriedBranchesM : Enum → Set
CurriedBranchesM E = (P : Tag E → Set) (X : Set) → Set

CurriedBranches : (E : Enum) → CurriedBranchesM E
CurriedBranches = elimEnum CurriedBranchesM
  (λ P X → X)
  (λ l E ih P X → P here → ih (λ t → P (there t)) X)

CurryBranches : Enum → Set
CurryBranches E = (P : Tag E → Set) (X : Set) → UncurriedBranches E P X → CurriedBranches E P X

curryBranches : (E : Enum) → CurryBranches E
curryBranches = elimEnum CurryBranches
  (λ P X f → f tt)
  (λ l E ih P X f c → ih (λ t → P (there t)) X (λ cs → f (c , cs)))

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

UncurriedScope : (T : Tel) (X : Scope T → Set) → Set
UncurriedScope T X = (xs : Scope T) → X xs

CurriedScope : (T : Tel) (X : Scope T → Set) → Set
CurriedScope = elimTel
  (λ T → (X : Scope T → Set) → Set)
  (λ X → X tt)
  (λ A B ih X → (a : A) → ih a (λ b → X (a , b)))

CurryScope : Tel → Set
CurryScope T = (X : Scope T → Set) → UncurriedScope T X → CurriedScope T X

curryScope : (T : Tel) → CurryScope T
curryScope = elimTel CurryScope
  (λ X f → f tt)
  (λ A B ih X f a → ih a (λ b → X (a , b)) (λ b → f (a , b)))

UncurryScope : Tel → Set
UncurryScope T = (X : Scope T → Set) → CurriedScope T X → UncurriedScope T X

uncurryScope : (T : Tel) → UncurryScope T
uncurryScope = elimTel UncurryScope
  (λ X x → elimUnit X x)
  (λ A B ih X f → elimPair A (λ a → Scope (B a)) X (λ a b → ih a (λ b → X (a , b)) (f a) b))

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

UncurriedFunc : (I : Set) (D : Desc I) (X : ISet I) → Set
UncurriedFunc I D X = (i : I) → Func I D X i → X i

CurriedFuncM : (I : Set) → Desc I → Set
CurriedFuncM I _ = (X : ISet I) → Set

CurriedFunc : (I : Set) (D : Desc I) (X : ISet I) → Set
CurriedFunc I = elimDesc I (CurriedFuncM I)
  (λ i X → X i)
  (λ i D ih X → (x : X i) → ih X)
  (λ A B ih X → (a : A) → ih a X)

CurryFunc : (I : Set) → Desc I → Set
CurryFunc I D = (X : ISet I) → UncurriedFunc I D X → CurriedFunc I D X

curryFunc : (I : Set) (D : Desc I) → CurryFunc I D
curryFunc I = elimDesc I (CurryFunc I)
  (λ i X cn → cn i refl)
  (λ i D ih X cn x → ih X (λ j xs → cn j (x , xs)))
  (λ A B ih X cn a → ih a X (λ j xs → cn j (a , xs)))

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

UncurriedHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedFunc I D X)
  → Set
UncurriedHyps I D X P cn =
  (i : I) (xs : Func I D X i) (ihs : Hyps I D X P i xs) → P i (cn i xs)

CurriedHypsM : (I : Set) (D : Desc I) → Set
CurriedHypsM I D = (X : ISet I) (P : (i : I) → X i → Set) (cn : UncurriedFunc I D X) → Set

CurriedHyps : (I : Set) (D : Desc I) → CurriedHypsM I D
CurriedHyps I = elimDesc I (CurriedHypsM I)
  (λ i X P cn → P i (cn i refl))
  (λ i D ih X P cn → (x : X i) → P i x → ih X P (λ j xs → cn j (x , xs)))
  (λ A B ih X P cn → (a : A) → ih a X P (λ j xs → cn j (a , xs)))

UncurryHyps : (I : Set) (D : Desc I) → Set
UncurryHyps I D = (X : ISet I) (P : (i : I) → X i → Set) (cn : UncurriedFunc I D X)
  → CurriedHyps I D X P cn → UncurriedHyps I D X P cn

uncurryHyps : (I : Set) (D : Desc I) → UncurryHyps I D
uncurryHyps I = elimDesc I (UncurryHyps I)
  (λ j X P cn pf i q u → elimEq I j
   (λ k r → P k (cn k r))
   pf i q
  )
  (λ j D ih X P cn pf i → elimPair (X j)
    (λ _ → Func I D X i)
    (λ xs → Hyps I (Rec j D) X P i xs → P i (cn i xs))
    (λ x xs → elimPair (P j x)
      (λ _ → Hyps I D X P i xs)
      (λ _ → P i (cn i (x , xs)))
      (λ p ps → ih X P (λ j ys → cn j (x , ys))
        (pf x p) i xs ps
      )
    )
  )
  (λ A B ih X P cn pf i → elimPair A
    (λ a → Func I (B a) X i)
    (λ xs → Hyps I (Arg A (λ a → B a)) X P i xs → P i (cn i xs))
    (λ a xs → ih a X P (λ j ys → cn j (a , ys))
      (pf a) i xs
    )
  )

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

BranchesD : Enum → Tel → Set
BranchesD E T = Branches E (λ _ → Desc (Scope T))

caseD : (E : Enum) (T : Tel) (cs : BranchesD E T) (t : Tag E) → Desc (Scope T)
caseD E T = case E (λ _ → Desc (Scope T))

sumD : (E : Enum) (T : Tel) (cs : BranchesD E T) → Desc (Scope T)
sumD E T cs = Arg (Tag E) (λ t → caseD E T cs t)

Indices : Tel → Set
Indices P = Scope P → Tel

indices : (P : Tel) → CurriedScope P (λ _ → Tel) → Indices P
indices P I = uncurryScope P (λ p → Tel) I

Constrs : (E : Enum) (P : Tel) (I : Indices P) → Set
Constrs E P I = (p : Scope P) → BranchesD E (I p)

constrs : (E : Enum) (P : Tel) (I : Indices P) → CurriedScope P (λ p → BranchesD E (I p)) → Constrs E P I
constrs E P I C = uncurryScope P (λ p → BranchesD E (I p)) C

Data : (X : (N : String) (E : Enum) (P : Tel) (I : Indices P) (C : Constrs E P I) → Set)
  → Set
Data X = (N : String) (E : Enum) (P : Tel) (I : Indices P) (C : Constrs E P I)
  → X N E P I C

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

FormUncurried : Data λ N E P I C
  → UncurriedScope P λ p
  → UncurriedScope (I p) λ i
  → Set
FormUncurried N E P I C p =
  μ N (Scope P) (Scope (I p)) (sumD E (I p) (C p)) p

Former : (P : Tel) → Indices P → Set
Former P I = CurriedScope P λ p → CurriedScope (I p) λ i → Set

Form : Data λ N E P I C → Former P I
Form N E P I C =
  curryScope P (λ p → CurriedScope (I p) λ i → Set) λ p →
  curryScope (I p) (λ i → Set) λ i →
  FormUncurried N E P I C p i

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

injUncurried : Data λ N E P I C
  → (t : Tag E)
  → UncurriedScope P λ p
  → CurriedFunc (Scope (I p)) (caseD E (I p) (C p) t) (FormUncurried N E P I C p)
injUncurried N E P I C t p = curryFunc (Scope (I p)) (caseD E (I p) (C p) t)
  (FormUncurried N E P I C p)
  (λ i xs → init (t , xs))

Inj : Data λ N E P I C → (t : Tag E) → Set
Inj N E P I C t = CurriedScope P λ p
  → CurriedFunc (Scope (I p)) (caseD E (I p) (C p) t) (FormUncurried N E P I C p)

inj : Data λ N E P I C → (t : Tag E) → Inj N E P I C t
inj N E P I C t = curryScope P
  (λ p → CurriedFunc (Scope (I p)) (caseD E (I p) (C p) t) (FormUncurried N E P I C p))
  (injUncurried N E P I C t)

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

indCurried : (ℓ : String) (P I : Set) (D : Desc I) (p : P)
  (M : (i : I) → μ ℓ P I D p i → Set)
  (f : CurriedHyps I D (μ ℓ P I D p) M (λ _ xs → init xs))
  (i : I) (x : μ ℓ P I D p i) → M i x
indCurried ℓ P I D p M f i x =
  ind ℓ P I D p M (uncurryHyps I D (μ ℓ P I D p) M (λ _ xs → init xs) f) i x

SumCurriedHyps : Data λ N E P I C
  → UncurriedScope P λ p
  → (M : CurriedScope (I p) (λ i → FormUncurried N E P I C p i → Set))
  → Tag E → Set
SumCurriedHyps N E P I C p M t =
  let unM = uncurryScope (I p) (λ i → FormUncurried N E P I C p i → Set) M in
  CurriedHyps (Scope (I p)) (caseD E (I p) (C p) t)
    (FormUncurried N E P I C p) unM (λ i xs → init (t , xs))

elimUncurried : Data λ N E P I C
  → UncurriedScope P λ p
  → (M : CurriedScope (I p) (λ i → FormUncurried N E P I C p i → Set))
  → let unM = uncurryScope (I p) (λ i → FormUncurried N E P I C p i → Set) M
  in UncurriedBranches E
     (SumCurriedHyps N E P I C p M)
     (CurriedScope (I p) (λ i → (x : FormUncurried N E P I C p i) → unM i x))
elimUncurried N E P I C p M cs = let
    unM = uncurryScope (I p) (λ i → FormUncurried N E P I C p i → Set) M
  in
  curryScope (I p) (λ i → (x : FormUncurried N E P I C p i) → unM i x)
  (indCurried N (Scope P) (Scope (I p)) (sumD E (I p) (C p)) p unM
    (case E (SumCurriedHyps N E P I C p M) cs))

Elim : Data λ N E P I C → Set
Elim N E P I C = CurriedScope P λ p
  → (M : CurriedScope (I p) (λ i → FormUncurried N E P I C p i → Set))
  → let unM = uncurryScope (I p) (λ i → FormUncurried N E P I C p i → Set) M
  in CurriedBranches E
     (SumCurriedHyps N E P I C p M)
     (CurriedScope (I p) (λ i → (x : FormUncurried N E P I C p i) → unM i x))

elim : Data λ N E P I C → Elim N E P I C
elim N E P I C = curryScope P
  (λ p → (M : CurriedScope (I p) (λ i → FormUncurried N E P I C p i → Set))
    → let unM = uncurryScope (I p) (λ i → FormUncurried N E P I C p i → Set) M
    in CurriedBranches E
       (SumCurriedHyps N E P I C p M)
       (CurriedScope (I p) (λ i → (x : FormUncurried N E P I C p i) → unM i x)))
  (λ p M → let unM = uncurryScope (I p) (λ i → FormUncurried N E P I C p i → Set) M
    in curryBranches E
    (SumCurriedHyps N E P I C p M)
    (CurriedScope (I p) (λ i → (x : FormUncurried N E P I C p i) → unM i x))
    (elimUncurried N E P I C p M))

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

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Instances.Int where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.Data.Int as Int
  renaming ( ℤ to ℤ ; _+_ to _+ℤ_; _·_ to _·ℤ_; -_ to -ℤ_)

open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing)

ℤCommRing : CommRing ℓ-zero
fst ℤCommRing = ℤ
0r (snd ℤCommRing) = 0
1r (snd ℤCommRing) = 1
_+_ (snd ℤCommRing) = _+ℤ_
_·_ (snd ℤCommRing) = _·ℤ_
- snd ℤCommRing = -ℤ_
isCommRing (snd ℤCommRing) = isCommRingℤ
  where
  abstract
    isCommRingℤ : IsCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_
    isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc (λ _ → refl)
                                 -Cancel Int.+Comm Int.·Assoc
                                 Int.·Rid ·DistR+ Int.·Comm

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2016-10-14, issue #2257, reported by m0davis
-- Bisected by Nisse.

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

-- {-# OPTIONS -v tc.ip:20 #-}
-- {-# OPTIONS -v tc:20 #-}

record R (A : Set) : Set₁ where
  field
    a : A
    F : ∀ {f} → Set

  foo : Set
  foo = ∀ {f} → {!!}

  field
    bar : Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module sets.finite.level where

open import sum
open import function.isomorphism.core
open import hott.level.core
open import hott.level.closure
open import hott.level.sets
open import sets.finite.core

finite-h2 : ∀ {i}{A : Set i} → IsFinite A → h 2 A
finite-h2 (n , fA) = iso-level (sym≅ fA) (fin-set n)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base