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

syntax Ring | R

type
  * : 0-ary

term
  zero : * | 𝟘
  add  : *  *  ->  * | _⊕_ l20
  one  : * | 𝟙
  mult : *  *  ->  * | _⊗_ l30
  neg  : *  ->  * | ⊖_ r50

theory
  (𝟘U⊕ᴸ) a |> add (zero, a) = a
  (𝟘U⊕ᴿ) a |> add (a, zero) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
  (𝟙U⊗ᴸ) a |> mult (one, a) = a
  (𝟙U⊗ᴿ) a |> mult (a, one) = a
  (⊗A) a b c |> mult (mult(a, b), c) = mult (a, mult(b, c))
  (⊗D⊕ᴸ) a b c |> mult (a, add (b, c)) = add (mult(a, b), mult(a, c))
  (⊗D⊕ᴿ) a b c |> mult (add (a, b), c) = add (mult(a, c), mult(b, c))
  (𝟘X⊗ᴸ) a |> mult (zero, a) = zero
  (𝟘X⊗ᴿ) a |> mult (a, zero) = zero
  (⊖N⊕ᴸ) a |> add (neg (a), a) = zero
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = zero
-}

module Ring.Syntax where

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

open import SOAS.Metatheory.Syntax

open import Ring.Signature

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

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

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

    𝟘   : R * Γ
    _⊕_ : R * Γ → R * Γ → R * Γ
    𝟙   : R * Γ
    _⊗_ : R * Γ → R * Γ → R * Γ
    ⊖_  : R * Γ → R * Γ

  infixl 20 _⊕_
  infixl 30 _⊗_
  infixr 50 ⊖_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Rᵃ : MetaAlg R
  Rᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (zeroₒ ⋮ _)     → 𝟘
      (addₒ  ⋮ a , b) → _⊕_ a b
      (oneₒ  ⋮ _)     → 𝟙
      (multₒ ⋮ a , b) → _⊗_ a b
      (negₒ  ⋮ a)     → ⊖_  a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Rᵃ = MetaAlg Rᵃ

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

    open MetaAlg 𝒜ᵃ

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

    𝕤𝕖𝕞  𝟘        = 𝑎𝑙𝑔 (zeroₒ ⋮ tt)
    𝕤𝕖𝕞 (_⊕_ a b) = 𝑎𝑙𝑔 (addₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞  𝟙        = 𝑎𝑙𝑔 (oneₒ  ⋮ tt)
    𝕤𝕖𝕞 (_⊗_ a b) = 𝑎𝑙𝑔 (multₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (⊖_  a)   = 𝑎𝑙𝑔 (negₒ  ⋮ 𝕤𝕖𝕞 a)

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

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

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

      open MetaAlg⇒ gᵃ⇒

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

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

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

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


text:
module Issue826-2 where

open import Common.Coinduction

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

data D : Set where
  c : ∞ D → D

delay : D → ∞ D
delay x = ♯ x

data P : D → Set where
  o : (x : ∞ D) → P (♭ x) → P (c x)

postulate
  h : (x : D) → P x → P x

f : (x : D) → P (c (delay x)) → P x
f x (o .(delay x) p) = h x p

g : (x : D) → P x → P (c (delay x))
g x p = h (c (delay x)) (o (delay x) p)

postulate
  bar : (x : ∞ D) (p : P (♭ x)) →
        h (c x) (o x (h (♭ x) p)) ≡ o x p

foo : (x : D) (p : P (c (delay x))) → g x (f x p) ≡ p
foo x (o .(delay x) p) = goal
  where
  x′ = _

  goal : _ ≡ o x′ p
  goal = bar x′ p

-- The following error message seems to indicate that an expression is
-- not forced properly:
--
--   Bug.agda:30,26-30
--   ♭ (.Bug.♯-0 x) != x of type D
--   when checking that the expression goal has type
--   g x (f x (o (.Bug.♯-0 x) p)) ≡ o (.Bug.♯-0 x) p
--
-- Thus it seems as if this problem affects plain type-checking as
-- well.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{- 2010-09-17 a small case study to test irrelevance -}

module IrrelevanceCaseStudyPartialFunctions where

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

record ⊤ : Set where

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

syntax Sigma A (λ x → B) = Σ x ∈ A , B

data Subset (A : Set)(P : A → Set) : Set where
  _#_ : (elem : A) → .(P elem) → Subset A P

elimSubset : ∀ {A C : Set} {P} →
             Subset A P → ((a : A) → .(P a) → C) → C
elimSubset (a # p) k = k a p

syntax Subset A (λ x → P) = ⁅ x ∈ A ∣ P ⁆

elem : {A : Set}{P : A → Set} → ⁅ x ∈ A ∣ P x ⁆ → A
elem (x # p) = x

elim₂ : ∀ {A C : Set} {P Q : A → Set} →
        Subset A (λ x → Sigma (P x) (λ _ → Q x)) →
        ((a : A) → .(P a) → .(Q a) → C) → C
elim₂ (a # (p , q)) k = k a p q

record _⇀_ (A B : Set) : Set1 where
  constructor mkParFun
  field
    dom : A → Set
    _′_ : ⁅ x ∈ A ∣ dom x ⁆ → B

open _⇀_ public

syntax mkParFun dom f = f ↾ dom

pure : {A B : Set} → (A → B) → A ⇀ B
pure f = record { dom = λ x → ⊤ ; _′_ = λ a → f (elem a) }

_∘_ : {A B C : Set} → (B ⇀ C) → (A ⇀ B) → A ⇀ C
(g ↾ Q) ∘ (f ↾ P) = gf ↾ QP where
  QP : _ → Set
  QP x             = Σ x∈P ∈ P x , Q (f (x # x∈P))
  gf : Subset _ QP → _
  gf (x # (p , q)) = g (f (x # p) # q)

_⊑_ : {A B : Set} → (f f' : A ⇀ B) → Set
(f ↾ P) ⊑ (f' ↾ P') =
  Σ φ ∈ (∀ {x} → P x → P' x) ,
    (∀ {x} (p : P x) → f (x # p) ≡ f' (x # φ p))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- P: <E[new s]> --> (vcd) <E[(c,d)]>
module Properties.StepNew where

open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All
open import Data.Product

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values
open import Session
open import Schedule

open import ProcessSyntax
open import ProcessRun

open import Properties.Base

tch : SType → Type
tch s = (TPair (TChan (SType.force s)) (TChan (SType.force (dual s))))

mknew : ∀ {Φ} → (s : SType) → Expr (tch s ∷ Φ) TUnit → Expr Φ TUnit
mknew s E = letbind (split-all-right _) (new [] s) E

mklhs : ∀ {Φ} → (s : SType) → Expr (tch s ∷ Φ) TUnit → Proc Φ
mklhs s E = exp (mknew s E)

mkrhs : ∀ {Φ} → (s : SType) → Expr (tch s ∷ Φ) TUnit → Proc Φ
mkrhs s E = res s (exp (letbind (left (left (split-all-right _))) (pair (left (rght [])) (here []) (here [])) E))

reduction : (s : SType) (E : Expr (tch s ∷ []) TUnit) →
    let lhs = (runProc [] (mklhs s E) (vnil []-inactive)) in
    let rhs = (runProc [] (mkrhs s E) (vnil []-inactive)) in
    one-step lhs ≡
    (New , proj₁ rhs , proj₂ rhs)
reduction s E
  with ssplit-refl-left-inactive []
... | G' , ina-G' , ss-GG'
  = refl

-- reduction in open context

open-reduction-type : Set
open-reduction-type = ∀ {Φ} (s : SType) (E : Expr (tch s ∷ Φ) TUnit) (ϱ : VEnv [] Φ) →
    let lhs = (runProc [] (mklhs s E) ϱ) in
    let rhs = (runProc [] (mkrhs s E) ϱ) in
    one-step lhs ≡ (New , proj₁ rhs , proj₂ rhs)

open-reduction : open-reduction-type
open-reduction{Φ} s E ϱ
  with runProc [] (exp (mknew s E)) ϱ
... | rpse
  rewrite split-env-right-lemma0 ϱ
    | split-rotate-lemma {Φ}
    | split-env-right-lemma ϱ
  with ssplit-compose (ss-left{(SType.force s) , POSNEG} ss-[]) (ss-left ss-[])
... | ssc
  = refl

{-

-- reduction in open context with further resources

pairs : ∀ {A : Set} {B : A → Set} {p1 p2 : Σ A λ x → B x }
  → p1 ≡ p2 → Σ (proj₁ p1 ≡ proj₁ p2) λ { refl → proj₂ p1 ≡ proj₂ p2 }
pairs {A} {B} refl = refl , refl

split-env-right-lemma0' :
  ∀ {Φ G} (ϱ : VEnv G Φ) →
  let gis = ssplit-refl-right-inactive G in
  (split-env (split-all-right Φ) ϱ
  ≡
  ((proj₁ gis , G) , proj₂ (proj₂ gis) , vnil (proj₁ (proj₂ gis)) , ϱ))
split-env-right-lemma0' (vnil []-inactive) = refl
split-env-right-lemma0' (vnil (::-inactive ina))
  with split-env-right-lemma0' (vnil ina)
... | ih
  with pairs ih
... | p1== , p2==
  = {!!}
split-env-right-lemma0'{t ∷ Φ} (vcons ssp v ϱ)
  with split-env-right-lemma0' ϱ
... | ih
  with split-env (split-all-right Φ) ϱ
... | sesar
    = {!!}

full-reduction-type : Set
full-reduction-type = ∀ {Φ G} (s : SType) (E : Expr (tch s ∷ Φ) TUnit) (ϱ : VEnv G Φ) →
    let lhs = runProc G (mklhs s E) ϱ in
    let rhs = runProc G (mkrhs s E) ϱ in
    single-step (proj₁ lhs ++ G , proj₂ lhs) ≡ (New , proj₁ rhs ++ G , proj₂ rhs)

full-reduction : full-reduction-type
full-reduction{Φ}{G} s E ϱ
  with ssplit-refl-left-inactive G
... | ssrli
  rewrite split-env-right-lemma0' ϱ
    | split-rotate-lemma {Φ}
  = {!!}

-}

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
-- Andreas, 2019-06-17, LAIM 2019, issue #3855
-- Only allow erased definitions in erased context.

open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Bool

@0 noWorld : String
noWorld = "Hallo, Welt!"

-- Illegal definition, should raise a type error.

world : Bool → String
world true  = "Hello world!"
world false = noWorld

main = putStrLn (world false)


text:
{-# OPTIONS --copatterns #-}

open import Common.Size

record R (i : Size) : Set where
  inductive
  constructor delay
  field
    force : (j : Size< i) → R j
open R

inh : (i : Size) → R i
force (inh i) j = inh j

-- Should give termination error

data ⊥ : Set where

elim : R ∞ → ⊥
elim (delay f) = elim (f ∞)

-- Gives termination error, as expected.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module WrongNamedArgument where

postulate
  f : {A : Set₁} → A → A

test : Set → Set
test = f {B = Set}

-- Good error:

-- Function does not accept argument {B = _}
-- when checking that {B = Set} are valid arguments to a function of
-- type {A : Set₁} → A → A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-----------------------------------
-- First order logic
-----------------------------------

module sv20.assign2.SetTheory.Logic where

infix 4 _,_
infix 3 ¬_
infix 1 _∧_
infix 1 _∨_
infix 0 _⇔_

-- Some First order logic I need.

-- ∧ data type (conjunction).

data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

∧-proj₁ : ∀ {A B} → A ∧ B → A
∧-proj₁ (a , _) = a

∧-proj₂ : ∀ {A B} → A ∧ B → B
∧-proj₂ (_ , b) = b

-- ∨ data type (disjunction), with many useful properties.

data _∨_ (A B : Set) : Set where
  inj₁ : A → A ∨ B
  inj₂ : B → A ∨ B

∨-e : (A B C : Set) → A ∨ B → (A → C) → (B → C) → C
∨-e A B C (inj₁ a) i₁ i₂ = i₁ a
∨-e A B C (inj₂ b) i₁ i₂ = i₂ b

∨-sym : (A B : Set) → A ∨ B → B ∨ A
∨-sym A B (inj₁ a) = inj₂ a
∨-sym A B (inj₂ b) = inj₁ b

trivial : (A : Set) → A → A
trivial _ A = A

∨-idem : (A : Set) → A ∨ A → A
∨-idem A (inj₁ a) = a
∨-idem A (inj₂ a) = a

∨-prop₁ : {A B C : Set} → (A ∨ B → C) → A → C
∨-prop₁ i a = i (inj₁ a)

∨-prop₂ : {A B C : Set} → (A ∨ B → C) → B → C
∨-prop₂ i b = i (inj₂ b)

∨-prop₃ : {A B C : Set} → A ∨ B → (A → C) → C ∨ B
∨-prop₃ (inj₁ x) i = inj₁ (i x)
∨-prop₃ (inj₂ x) i = inj₂ x

∨-prop₄ : {A B C : Set} → A ∨ B → (B → C) → A ∨ C
∨-prop₄ (inj₁ x) x₁ = inj₁ x
∨-prop₄ (inj₂ x) x₁ = inj₂ (x₁ x)

∨-prop₅ : {A B C D : Set} → A ∨ B → (A → C) → (B → D) → C ∨ D
∨-prop₅ (inj₁ a) a→c b→d = inj₁ (a→c a)
∨-prop₅ (inj₂ b) a→c b→d = inj₂ (b→d b)

∨-∧ : {A B : Set} → (A ∧ B) ∨ (B ∧ A) → A ∧ B
∨-∧ (inj₁ (a , b)) = a , b
∨-∧ (inj₂ (b , a)) = a , b

-- Bi-implication.

_⇔_ : Set → Set → Set
A ⇔ B = (A → B) ∧ (B → A)

⇔-p : (A B C : Set) →  A ⇔ (B ∧ C) → (C → B) → A ⇔ C
⇔-p A B C (h₁ , h₂) h₃ = prf₁ , prf₂
  where
  prf₁ : A → C
  prf₁ A = ∧-proj₂ (h₁ A)

  prf₂ : C → A
  prf₂ C = h₂ ((h₃ C) , C)

-- Empty data type.

data ⊥ : Set where

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

data ⊤ : Set where
  tt : ⊤

-- Negation

¬_ : Set → Set
¬ A = A → ⊥

cont : (A : Set) → A ∧ ¬ A → ⊥
cont _ (x , ¬x) = ¬x x


text:
module Issue690a where

postulate A : Set

data T : Set → Set where
  c : T (T A)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Oscar.Prelude
open import Oscar.Class

module Oscar.Class.Hmap where

module Hmap
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  {𝔯₁} {𝔯₂}
  (ℜ₁ : 𝔛₁ → 𝔛₂ → Ø 𝔯₁)
  (ℜ₂ : 𝔛₁ → 𝔛₂ → Ø 𝔯₂)
  = ℭLASS (ℜ₁ , ℜ₂)
          (∀ x y
           → ℜ₁ x y → ℜ₂ x y)

module _
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  {𝔯₁} {𝔯₂}
  {ℜ₁ : 𝔛₁ → 𝔛₂ → Ø 𝔯₁}
  {ℜ₂ : 𝔛₁ → 𝔛₂ → Ø 𝔯₂}
  where
  hmap = Hmap.method ℜ₁ ℜ₂

module _
  {𝔵} {𝔛 : Ø 𝔵}
  {𝔯₁} {𝔯₂}
  {ℜ₁ : 𝔛 → 𝔛 → Ø 𝔯₁}
  {ℜ₂ : 𝔛 → 𝔛 → Ø 𝔯₂}
  where
  smap : ⦃ _ : Hmap.class ℜ₁ ℜ₂ ⦄ → ∀ {x y} → ℜ₁ x y → ℜ₂ x y
  smap = Hmap.method ℜ₁ ℜ₂ _ _
  § = smap

module _
  {𝔵} {𝔛 : Ø 𝔵}
  {𝔯₁} {𝔯₂}
  {ℜ₁ : 𝔛 → 𝔛 → Ø 𝔯₁}
  (ℜ₂ : 𝔛 → 𝔛 → Ø 𝔯₂)
  where
  smap[_] : ⦃ _ : Hmap.class ℜ₁ ℜ₂ ⦄ → ∀ {x y} → ℜ₁ x y → ℜ₂ x y
  smap[_] = Hmap.method ℜ₁ ℜ₂ _ _
  §[_] = smap[_]


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Equality.DecSetoid directly.
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Equality.DecSetoid
  {a ℓ} (DS : DecSetoid a ℓ) where

open import Data.List.Relation.Binary.Equality.DecSetoid DS public


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

open import Agda.Primitive
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Naturals
open import Basic

module File1 where

{-
Let's define the integers. Answers can be found in commit 4d7aad52e014daeb48fe5fb6854d3b6e0080012a.

If you want to learn how to type something, remember the Emacs action is M-x describe-char with the cursor on a character.
-}
data ℤ : Set where
  pos : ℕ → ℤ
  neg : ℕ → ℤ
  congZero : pos 0 ≡ neg 0

{-
A bit odd! We defined an integer to be "a natural tagged as positive", "a natural tagged as negative", or "a witness that pos 0 = neg 0".
This is obvious nonsense (how can two things be equal if they were made from different constructors?! what even does it mean for "pos 0 ≡ neg 0" to be an integer?!) until you let go of your preconceptions about what it means for two things to be equal.
-}

-- Just to help you realise how odd this is, we'll use some new Cubical definitions to manifest a really weird element of ℤ which is neither a `pos` nor a `neg`. Don't worry too much about this for now.
oddThing : ℤ
oddThing = congZero i1

-- Even odder, the integer we just made is equal to 0. Think how strange this is: it's not built using the only constructor that could build `pos 0`, but it's still equal to `pos 0`.
oddThing2 : pos 0 ≡ oddThing
oddThing2 = congZero

{-
Add 1 to an integer. The first cases are easy, but the last case is very odd and we will discuss it in detail.
-}
incr : ℤ → ℤ
incr (pos x) = pos (succ x)
incr (neg zero) = pos 1
incr (neg (succ x)) = neg x

-- First of all, we have in scope an "integer" `congZero` which is of type `pos 0 ≡ neg 0` - huh?!
incr (congZero i) = {!!}
{-
This one looks different from the non-cubical world.

Goal: ℤ
———— Boundary ——————————————————————————————————————————————
i = i0 ⊢ pos 1
i = i1 ⊢ pos 1
————————————————————————————————————————————————————————————
i : I
———— Constraints ———————————————————————————————————————————
pos 1 = ?0 (i = i1) : ℤ
pos 1 = ?0 (i = i0) : ℤ

The constraints look pretty normal, telling you that goal 0 needs to be equal to `pos 1`.
But there's stuff about this `i : I` here. What's that?

Recall that Cubical alters the definition of ≡. Given any element of X, an element of X ≡ Y contains content for how that element corresponds to a Y, and vice versa.
Homotopy type theory, and Cubical Agda, prefer to think of a more general structure on top of that data, though: not only can we go from an X to a Y, but we also store *how* we get there.
More abstractly, we store how to traverse a path from X to Y. The `i` here is telling us where along that path we are; the template goes from the special symbol `i0` to the special symbol `i1`, and `i` is notionally somewhere between those two points.

This gives some nice composability properties: if we know that X ≡ Y and that Y ≡ Z, we can compose the two paths to get a path X ≡ Z.
Cubical Agda's great innovation is that all this has computational content: proofs about X can be transported along the path to obtain for free proofs about Z.

Having told Agda that `incr (pos x) = pos (succ x)`, it can infer that `incr (pos 0) = pos 1`.
So our goal of constructing a path `incr congZero : incr (pos 0) ≡ incr (neg 0)` is in fact the requirement to construct a path `pos 1 ≡ incr (neg 0)`.
Similarly, we told it that `incr (neg 0) = pos 1`, so our path `incr congZero` is actually of type `pos 1 ≡ pos 1`
The `I` from the goal is the template of the path `congZero n` which we are trying to construct from `pos 1` to `pos 1`.
The `i0` and `i1` are the templates for the start and end points of the path, i.e. they both indicate `pos 1`.

What we really wanted to write here was `incr congZero`. For reasons I don't understand, Agda doesn't accept this.
We are forced to descend to the level of actually implementing the path from `pos 1` to `pos 1` by telling Agda where each `i` goes, even though there's an obvious way (`refl`) to specify the entire path at once.

Agda can automatically infer the correct hole-fill, but you can try it with `pos 1`.
-}

{-
Let's show that successors of naturals are nonzero.
We do this using a new technique that only makes sense in Cubical-land.

Given a path from `succ a` to `0`, we need to show False.
The assumed member of `succ a ≡ 0` is a path that tells us how to get from `succ a` to `0` in a way that is preserved by function application.
That is, it tells us how to show `f (succ a) ≡ f 0` for any `f`. (The function `subst` captures this ability to move functions from one end of a path to the other.)
So if we pick `f` appropriately so that it outputs `False` at 0 but something else (anything else, as long as we can construct it!) at `succ a`, we will be done.
-}
succNonzero : {a : ℕ} → succ a ≡ 0 → False
succNonzero {a} sa=0 = subst f sa=0 {!!}
  where
    f : ℕ → Set
    f zero = False
    f (succ i) = {!!}

{-
Let's show that these equality things aren't *too* weird. We'll show that even though `pos 0` is equal to `congZero i1`, it's actually the *only* other `pos` which is equal to `congZero i1`. (You'd hope this would be the case; otherwise we'd have several `pos` being equal to each other.)

Cubical Agda gives us a magical way to do this. Recall that we can move functions along paths (the `subst` from above, which lets us take an `x ≡ y` and an `f` to get `f x → f y`); we can actually also do the same thing viewed as transforming the *entire path* `x ≡ y` using `f` into `f x ≡ f y`.
This is the function `cong`.

If we can somehow create a function that "strips off `pos`", then that function can transform the path `pos a ≡ pos b` into a path `a ≡ b`.
-}
toNat : ℤ → ℕ
toNat z = {!!}

posInjective : {a b : ℕ} → pos a ≡ pos b → a ≡ b
posInjective pr = cong toNat pr

{-
Finally, we can use the injectivity of `pos` in the obvious way to prove that only `pos 0` is `congZero i1`.
-}
notTooOdd : (n : ℕ) → (pos n ≡ congZero i1) → n ≡ 0
notTooOdd zero pr = refl
notTooOdd (succ n) pr = posInjective (pr ∙ sym congZero)

{-
Let's show that `pos` is injective in a different way, inspired by how you might do this kind of thing in a non-Cubical world. We'll go by induction, which means the interesting case will be `pos (succ a) ≡ pos (succ b) → pos a ≡ pos b`.

This is a classic example of moving a path wholesale along a function; in this case, the function is "decrement".
-}
decr : ℤ → ℤ -- TODO hole this
decr z = {!!}

posDecr : {a b : ℕ} → pos (succ a) ≡ pos (succ b) → pos a ≡ pos b
posDecr {a} {b} pr = cong decr pr

posInjective' : {a b : ℕ} → pos a ≡ pos b → a ≡ b
-- The two easy cases first
posInjective' {zero} {zero} x = refl
posInjective' {succ a} {succ b} x = cong succ (posInjective (posDecr x))
{-
We need to transform `pos zero ≡ pos (succ b)` into `zero ≡ succ b`.
We could do this using the proof of `posInjective` - moving the path along `toNat` - but it is also interesting to construct the path `zero ≡ succ b` manually using `subst`.

To use `subst`, we need to construct a function from ℤ which is "a type we can populate" at `pos zero` (i.e. at one end of the path), and `zero ≡ succ b` at `pos (succ b)` (i.e. at the other end of the path); then we will be able to move from the populated type to `zero ≡ succ b` using that function.

These two are quite hard!
-}
posInjective' {zero} {succ b} x = subst t x {!!}
  where
    t : ℤ → Set
    t z = {!!}
posInjective' {succ a} {zero} x = subst t x {!!}
  where
    t : ℤ → Set
    t z = {!!}

{-
What does equality mean on the level of types, rather than values?
Univalence, the axiom which Cubical provides computational meaning to, basically says "identity really means isomorphism".
I will gloss over a lot of detail there, but here is a witness to `ℤ ≡ ℤ` that is not `refl`!
-}
incrDecrInverse1 : (a : ℤ) → incr (decr a) ≡ a
incrDecrInverse1 (pos zero) = sym congZero
incrDecrInverse1 (pos (succ x)) = refl
incrDecrInverse1 (neg x) = refl
{-
The remaining case is worth talking about.
We need a path from incr (decr (congZero j)) to congZero j.
That is, we need a path from incr (neg 1) to congZero j; i.e. from neg 0 to congZero j.
We already have a path from neg 0 to pos 0 - namely `sym congZero`.
But `sym congZero` goes from `neg 0` to every point along `sym congZero` - and `congZero j` is also a point along `sym congZero`, because `sym` just means "reverse the path"!
So we can get the path we need by truncating `sym congZero`, using the `∧` ("min") operation (a special builtin primitive in Cubical).
The path, parameterised by `i` with `j` fixed, is "go backwards (`sym`) along `congZero` to the min of `i` and where `j` lies on this path (`~ j`), but then don't go any further".
Here, `~` means essentially "negate"; if you got to position `i` travelling forward on path `p`, then you got to position `~ i` travelling backward on path `sym p`.

This is probably best done if you draw a little picture.
-}
incrDecrInverse1 (congZero j) i = sym congZero (i ∧ (~ j))

incrDecrInverse2 : (a : ℤ) → decr (incr a) ≡ a
incrDecrInverse2 x = {!!}

incrIso : ℤ ≡ ℤ
incrIso = isoToPath (iso incr decr incrDecrInverse1 incrDecrInverse2)

{-
Unexpected! Cubical has let us prove that ℤ ≡ ℤ in a very nonstandard way. What use is this? Who knows.
-}


text:
module Issue2845 where

open import Agda.Builtin.Nat
open import Agda.Primitive.Cubical
open import Agda.Builtin.Equality

Ex1 : Nat
Ex1 = primComp (λ i → Nat) i0 (λ i → isOneEmpty) zero

test1 : Ex1 ≡ zero
test1 = refl

Ex2 : (i : I) → Nat
Ex2 i = primComp (λ i → Nat) i (λ { _ (i = i1) → zero}) zero

test2 : ∀ i → Ex2 i ≡ zero
test2 i = refl

Ex3 : (i : I) (p : I → Nat) → Nat
Ex3 i p = primComp (λ i → Nat) i (λ { k (i = i1) → suc (p k)}) (suc (p i0))

test3 : ∀ i p → Ex3 i p ≡ suc _
test3 i p = refl


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

module Universes where

open import Agda.Primitive public
 renaming (
            Level to Universe -- We speak of universes rather than of levels.
          ; lzero to 𝓤₀       -- Our first universe is called 𝓤₀
          ; lsuc to _⁺        -- The universe after 𝓤 is 𝓤 ⁺
          ; Setω to 𝓤ω        -- There is a universe 𝓤ω strictly above 𝓤₀, 𝓤₁, ⋯ , 𝓤ₙ, ⋯
          )
 using    (_⊔_)               -- Least upper bound of two universes, e.g. 𝓤₀ ⊔ 𝓤₁ is 𝓤₁

Type = λ ℓ → Set ℓ

_̇   : (𝓤 : Universe) → Type (𝓤 ⁺)

𝓤 ̇  = Type 𝓤

𝓤₁ = 𝓤₀ ⁺
𝓤₂ = 𝓤₁ ⁺
𝓤₃ = 𝓤₂ ⁺

_⁺⁺ : Universe → Universe
𝓤 ⁺⁺ = 𝓤 ⁺ ⁺

universe-of : {𝓤 : Universe} (X : 𝓤 ̇ ) → Universe
universe-of {𝓤} X = 𝓤

infix  1 _̇

max_stars_repo_name: UnsoundWitch/proofs

max_issues_repo_name: sym-cereal/proofs

max_forks_repo_name: sym-cereal/proofs


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

module Lemmas where

open import Cubical.Core.Everything    using (_≡_; Level; Type)

open import Data.Fin                   using (Fin; toℕ; fromℕ<; zero; suc)
open import Data.Integer               using (ℤ; +_; -[1+_])
open import Data.Nat
open import Data.Nat.Properties        using (≤-step)
open import Relation.Nullary.Decidable using (False)
open import Relation.Nullary           using (yes; no)

k≤n⇒n-k≤n : (k n : ℕ) → k ≤ n → n ∸ k ≤ n
k≤n⇒n-k≤n zero    zero    z≤n     = z≤n
k≤n⇒n-k≤n zero    (suc n) z≤n     = s≤s (k≤n⇒n-k≤n zero n z≤n)
k≤n⇒n-k≤n (suc k) zero    ()
k≤n⇒n-k≤n (suc k) (suc n) (s≤s p) = ≤-step (k≤n⇒n-k≤n k n p)

finN<N : {n : ℕ} → (k : Fin n) → toℕ k < n
finN<N zero    = s≤s z≤n
finN<N (suc k) = s≤s (finN<N k)

suc≤-injective : ∀ {m n : ℕ} → suc m ≤ suc n → m ≤ n
suc≤-injective (s≤s p) = p

-- revMod k = n - k
revMod : ∀ {n : ℕ} → Fin (suc n) → Fin (suc n)
revMod {n} k = fromℕ< (s≤s (k≤n⇒n-k≤n (toℕ k) n (suc≤-injective (finN<N k))))

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
open import Data.ByteString.Primitive using ( ByteStringStrict ;  ByteStringStrict² ; ByteStringLazy ; ByteStringLazy² )
open import Data.Bool using ( Bool )
open import Data.Char using ( Char )
open import Data.Natural using ( Natural )
open import Data.String using  ( String )

module Data.ByteString.UTF8.Primitive where

postulate
  fromStringStrict : String → ByteStringStrict
  toStringStrict : ByteStringStrict → String
  lengthStrict : ByteStringStrict → Natural
  spanStrict : (Char → Bool) → ByteStringStrict →  ByteStringStrict²
  breakStrict : (Char → Bool) → ByteStringStrict →  ByteStringStrict²

{-# IMPORT Data.ByteString.UTF8 #-}
{-# COMPILED fromStringStrict Data.ByteString.UTF8.fromString #-}
{-# COMPILED toStringStrict Data.ByteString.UTF8.toString #-}
{-# COMPILED lengthStrict fromIntegral . Data.ByteString.UTF8.length #-}
{-# COMPILED spanStrict Data.ByteString.UTF8.span #-}
{-# COMPILED breakStrict Data.ByteString.UTF8.break #-}

postulate
  fromStringLazy : String → ByteStringLazy
  toStringLazy : ByteStringLazy → String
  lengthLazy : ByteStringLazy → Natural
  spanLazy : (Char → Bool) → ByteStringLazy →  ByteStringLazy²
  breakLazy : (Char → Bool) → ByteStringLazy →  ByteStringLazy²

{-# IMPORT Data.ByteString.Lazy.UTF8 #-}
{-# COMPILED fromStringLazy Data.ByteString.Lazy.UTF8.fromString #-}
{-# COMPILED toStringLazy Data.ByteString.Lazy.UTF8.toString #-}
{-# COMPILED lengthLazy fromIntegral . Data.ByteString.Lazy.UTF8.length #-}
{-# COMPILED spanLazy Data.ByteString.Lazy.UTF8.span #-}
{-# COMPILED breakLazy Data.ByteString.Lazy.UTF8.break #-}

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommSemiring where

open import Cubical.Algebra.CommSemiring.Base public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import HoTT
open import cw.CW
open import cw.FinCW
open import cw.FinBoundary
open import cohomology.Theory

{- The reason that RephraseDualizedFirstFinBoundary did not handle this case
   is because [FinSkeleton n] does not compute. -}

module cw.cohomology.cochainequiv.DualizedFirstBoundary (OT : OrdinaryTheory lzero)
  (⊙fin-skel : ⊙FinSkeleton 1) where

open OrdinaryTheory OT
open FreeAbelianGroup

private
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel

  I₋₁ = AttachedFinSkeleton.skel fin-skel

  module FAG   = FreeAbelianGroup (Fin I)
  module FAG₋₁ = FreeAbelianGroup (Fin I₋₁)

  open FAG   renaming (FreeAbGroup to G)   using ()
  open FAG₋₁ renaming (FreeAbGroup to G₋₁) using ()

abstract
  rephrase-dualized-first-boundary-in-degree : ∀ g <I
    →  GroupHom.f (Freeness.extend _ (C2-abgroup 0) g) (GroupHom.f (fboundary-last fin-skel) (FAG.insert <I))
    == Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁))
  rephrase-dualized-first-boundary-in-degree g <I =
    γ.f (GroupHom.f (fboundary-last fin-skel) (FAG.insert <I))
      =⟨ ap γ.f $ app= (is-equiv.g-f (FAG.Freeness.extend-is-equiv G₋₁) (fboundary'-last fin-skel)) <I ⟩
    γ.f (G₋₁.sum (λ <I₋₁ → G₋₁.exp (FAG₋₁.insert <I₋₁) (fdegree-last fin-skel <I <I₋₁)))
      =⟨ γ.pres-sum (λ <I₋₁ → G₋₁.exp (FAG₋₁.insert <I₋₁) (fdegree-last fin-skel <I <I₋₁)) ⟩
    C⁰2.sum (λ <I₋₁ → (γ.f (G₋₁.exp (FAG₋₁.insert <I₋₁) (fdegree-last fin-skel <I <I₋₁))))
      =⟨ ap C⁰2.sum (λ= λ <I₋₁ → γ.pres-exp (FAG₋₁.insert <I₋₁) (fdegree-last fin-skel <I <I₋₁)) ⟩
    C⁰2.sum (λ <I₋₁ → (C⁰2.exp (γ.f (FAG₋₁.insert <I₋₁)) (fdegree-last fin-skel <I <I₋₁)))
      =⟨ ap C⁰2.sum
          (λ= λ <I₋₁ → ap (λ g → C⁰2.exp g (fdegree-last fin-skel <I <I₋₁)) $
            app= (is-equiv.g-f (FAG₋₁.Freeness.extend-is-equiv C⁰2) g) <I₋₁) ⟩
    C⁰2.sum (λ <I₋₁ → (C⁰2.exp (g <I₋₁) (fdegree-last fin-skel <I <I₋₁)))
      =∎
    where
      C⁰2 : AbGroup lzero
      C⁰2 = C2-abgroup 0
      module C⁰2 = AbGroup C⁰2
      γ : G₋₁.grp →ᴳ C⁰2.grp
      γ = FAG₋₁.Freeness.extend C⁰2 g
      module γ = GroupHom γ

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
-- Andreas, 2021-12-22, issue #5705 reported by ksqsf

open import Agda.Builtin.Equality

crash : Set ≡ Set9223372036854775808
crash = refl

-- This should fail, but crashes in Agda 2.6.2 due to Int overflow.


text: module Categories.Coend where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Type where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels

open import Cubical.Functions.FunExtEquiv
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Relation.Binary

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓ≅A ℓB ℓ≅B ℓ≅ᴰ ℓP : Level

-- a type is a URGStr with the relation given by its identity type
𝒮-type : (A : Type ℓ) → URGStr A ℓ
𝒮-type A = make-𝒮 {_≅_ = _≡_} (λ _ → refl) isContrSingl

𝒮ᴰ-type : {A : Type ℓA} (B : A → Type ℓB)
          → URGStrᴰ (𝒮-type A) B ℓB
𝒮ᴰ-type {A = A} B = make-𝒮ᴰ (λ b p b' → PathP (λ i → B (p i)) b b')
                    (λ _ → refl)
                    λ _ b → isContrSingl b

-- subtypes are displayed structures
𝒮ᴰ-subtype : {A : Type ℓ} (P : A → hProp ℓ')
             → URGStrᴰ (𝒮-type A)
                       (λ a → P a .fst)
                       ℓ-zero
𝒮ᴰ-subtype P
  = make-𝒮ᴰ (λ _ _ _ → Unit)
            (λ _ → tt)
            λ a p → isContrRespectEquiv (invEquiv (Σ-contractSnd (λ _ → isContrUnit)))
                                        (inhProp→isContr p (P a .snd))

-- a subtype induces a URG structure on itself
Subtype→Sub-𝒮ᴰ : {A : Type ℓA} (P : A → hProp ℓP)
                 (StrA : URGStr A ℓ≅A)
                 → URGStrᴰ StrA (λ a → P a .fst) ℓ-zero
Subtype→Sub-𝒮ᴰ P StrA =
  make-𝒮ᴰ (λ _ _ _ → Unit)
          (λ _ → tt)
          (λ a p → isContrRespectEquiv (invEquiv (Σ-contractSnd (λ _ → isContrUnit)))
                                        (inhProp→isContr p (P a .snd)))

-- uniqueness of small URG structures
private
  module _ {A : Type ℓA} (𝒮 : URGStr A ℓA) where
    open URGStr
    𝒮' = 𝒮-type A

    ≅-≡ : _≅_ 𝒮' ≡ _≅_ 𝒮
    ≅-≡ = funExt₂ (λ a a' → ua (isUnivalent→isUnivalent' (_≅_ 𝒮) (ρ 𝒮) (uni 𝒮) a a'))

    ρ-≡ : PathP (λ i → isRefl (≅-≡ i)) (ρ 𝒮') (ρ 𝒮)
    ρ-≡ = funExt (λ a → toPathP (p a))
      where
        p : (a : A) → transport (λ i → ≅-≡ i a a) refl ≡ (ρ 𝒮 a)
        p a = uaβ (isUnivalent→isUnivalent' (_≅_ 𝒮) (ρ 𝒮) (uni 𝒮) a a) refl ∙ transportRefl (ρ 𝒮 a)

        u : (a : A) → (transport (λ i → ≅-≡ i a a) refl) ≡ (subst (λ a' → (_≅_ 𝒮) a a') refl (ρ 𝒮 a))
        u a =  uaβ (isUnivalent→isUnivalent' (_≅_ 𝒮) (ρ 𝒮) (uni 𝒮) a a) refl

    uni-≡ : PathP (λ i → isUnivalent (≅-≡ i) (ρ-≡ i)) (uni 𝒮') (uni 𝒮)
    uni-≡ = isProp→PathP (λ i → isPropΠ2 (λ a a' → isPropIsEquiv (≡→R (≅-≡ i) (ρ-≡ i)))) (uni 𝒮') (uni 𝒮)

𝒮-uniqueness : (A : Type ℓA) → isContr (URGStr A ℓA)
𝒮-uniqueness A .fst = 𝒮-type A
𝒮-uniqueness A .snd 𝒮 = sym (η-URGStr (𝒮-type A)) ∙∙ (λ i → p i) ∙∙ η-URGStr 𝒮
  where
    p = λ (i : I) → urgstr (≅-≡ 𝒮 i) (ρ-≡ 𝒮 i) (uni-≡ 𝒮 i)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational numbers
------------------------------------------------------------------------

module Data.Rational where

import Algebra
import Data.Bool.Properties as Bool
open import Function
open import Data.Integer as ℤ using (ℤ; ∣_∣; +_; -_)
open import Data.Integer.Divisibility as ℤDiv using (Coprime)
import Data.Integer.Properties as ℤ
open import Data.Nat.Divisibility as ℕDiv using (_∣_)
import Data.Nat.Coprimality as C
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Sum
import Level
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; cong; cong₂)
open P.≡-Reasoning

------------------------------------------------------------------------
-- The definition

-- Rational numbers in reduced form. Note that there is exactly one
-- representative for every rational number. (This is the reason for
-- using "True" below. If Agda had proof irrelevance, then it would
-- suffice to use "isCoprime : Coprime numerator denominator".)

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ
    isCoprime     : True (C.coprime? ∣ numerator ∣ (suc denominator-1))

  denominator : ℤ
  denominator = + suc denominator-1

  coprime : Coprime numerator denominator
  coprime = toWitness isCoprime

-- Constructs rational numbers. The arguments have to be in reduced
-- form.

infixl 7 _÷_

_÷_ : (numerator : ℤ) (denominator : ℕ)
      {coprime : True (C.coprime? ∣ numerator ∣ denominator)}
      {≢0 : False (ℕ._≟_ denominator 0)} →
      ℚ
(n ÷ zero) {≢0 = ()}
(n ÷ suc d) {c} =
  record { numerator = n; denominator-1 = d; isCoprime = c }

private

  -- Note that the implicit arguments do not need to be given for
  -- concrete inputs:

  0/1 : ℚ
  0/1 = + 0 ÷ 1

  -½ : ℚ
  -½ = - + 1 ÷ 2

------------------------------------------------------------------------
-- Equality

-- Equality of rational numbers.

infix 4 _≃_

_≃_ : Rel ℚ Level.zero
p ≃ q = numerator p ℤ.* denominator q ≡
        numerator q ℤ.* denominator p
  where open ℚ

-- _≃_ coincides with propositional equality.

≡⇒≃ : _≡_ ⇒ _≃_
≡⇒≃ refl = refl

≃⇒≡ : _≃_ ⇒ _≡_
≃⇒≡ {i = p} {j = q} =
  helper (numerator p) (denominator-1 p) (isCoprime p)
         (numerator q) (denominator-1 q) (isCoprime q)
  where
  open ℚ

  helper : ∀ n₁ d₁ c₁ n₂ d₂ c₂ →
           n₁ ℤ.* + suc d₂ ≡ n₂ ℤ.* + suc d₁ →
           (n₁ ÷ suc d₁) {c₁} ≡ (n₂ ÷ suc d₂) {c₂}
  helper n₁ d₁ c₁ n₂ d₂ c₂ eq
    with Poset.antisym ℕDiv.poset 1+d₁∣1+d₂ 1+d₂∣1+d₁
    where
    1+d₁∣1+d₂ : suc d₁ ∣ suc d₂
    1+d₁∣1+d₂ = ℤDiv.coprime-divisor (+ suc d₁) n₁ (+ suc d₂)
                  (C.sym $ toWitness c₁) $
                  ℕDiv.divides ∣ n₂ ∣ (begin
                    ∣ n₁ ℤ.* + suc d₂ ∣  ≡⟨ cong ∣_∣ eq ⟩
                    ∣ n₂ ℤ.* + suc d₁ ∣  ≡⟨ ℤ.abs-*-commute n₂ (+ suc d₁) ⟩
                    ∣ n₂ ∣ ℕ.* suc d₁    ∎)

    1+d₂∣1+d₁ : suc d₂ ∣ suc d₁
    1+d₂∣1+d₁ = ℤDiv.coprime-divisor (+ suc d₂) n₂ (+ suc d₁)
                  (C.sym $ toWitness c₂) $
                  ℕDiv.divides ∣ n₁ ∣ (begin
                    ∣ n₂ ℤ.* + suc d₁ ∣  ≡⟨ cong ∣_∣ (P.sym eq) ⟩
                    ∣ n₁ ℤ.* + suc d₂ ∣  ≡⟨ ℤ.abs-*-commute n₁ (+ suc d₂) ⟩
                    ∣ n₁ ∣ ℕ.* suc d₂    ∎)

  helper n₁ d c₁ n₂ .d c₂ eq | refl with ℤ.cancel-*-right
                                           n₁ n₂ (+ suc d) (λ ()) eq
  helper n  d c₁ .n .d c₂ eq | refl | refl with Bool.proof-irrelevance c₁ c₂
  helper n  d c  .n .d .c eq | refl | refl | refl = refl

------------------------------------------------------------------------
-- Equality is decidable

infix 4 _≟_

_≟_ : Decidable {A = ℚ} _≡_
p ≟ q with ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≟
           ℚ.numerator q ℤ.* ℚ.denominator p
p ≟ q | yes pq≃qp = yes (≃⇒≡ pq≃qp)
p ≟ q | no ¬pq≃qp = no (¬pq≃qp ∘ ≡⇒≃)

------------------------------------------------------------------------
-- Ordering

infix 4 _≤_ _≤?_

data _≤_ : ℚ → ℚ → Set where
  *≤* : ∀ {p q} →
        ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≤
        ℚ.numerator q ℤ.* ℚ.denominator p →
        p ≤ q

drop-*≤* : ∀ {p q} → p ≤ q →
           ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≤
           ℚ.numerator q ℤ.* ℚ.denominator p
drop-*≤* (*≤* pq≤qp) = pq≤qp

_≤?_ : Decidable _≤_
p ≤? q with ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≤?
            ℚ.numerator q ℤ.* ℚ.denominator p
p ≤? q | yes pq≤qp = yes (*≤* pq≤qp)
p ≤? q | no ¬pq≤qp = no (λ { (*≤* pq≤qp) → ¬pq≤qp pq≤qp })

decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
  { Carrier         = ℚ
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = record
      { isTotalOrder = record
          { isPartialOrder = record
              { isPreorder = record
                  { isEquivalence = P.isEquivalence
                  ; reflexive     = refl′
                  ; trans         = trans
                  }
                ; antisym = antisym
              }
          ; total = total
          }
      ; _≟_  = _≟_
      ; _≤?_ = _≤?_
      }
  }
  where
  module ℤO = DecTotalOrder ℤ.decTotalOrder

  refl′ : _≡_ ⇒ _≤_
  refl′ refl = *≤* ℤO.refl

  trans : Transitive _≤_
  trans {i = p} {j = q} {k = r} (*≤* le₁) (*≤* le₂)
    = *≤* (ℤ.cancel-*-+-right-≤ _ _ _
            (lemma
              (ℚ.numerator p) (ℚ.denominator p)
              (ℚ.numerator q) (ℚ.denominator q)
              (ℚ.numerator r) (ℚ.denominator r)
              (ℤ.*-+-right-mono (ℚ.denominator-1 r) le₁)
              (ℤ.*-+-right-mono (ℚ.denominator-1 p) le₂)))
    where
    open Algebra.CommutativeRing ℤ.commutativeRing

    lemma : ∀ n₁ d₁ n₂ d₂ n₃ d₃ →
            n₁ ℤ.* d₂ ℤ.* d₃ ℤ.≤ n₂ ℤ.* d₁ ℤ.* d₃ →
            n₂ ℤ.* d₃ ℤ.* d₁ ℤ.≤ n₃ ℤ.* d₂ ℤ.* d₁ →
            n₁ ℤ.* d₃ ℤ.* d₂ ℤ.≤ n₃ ℤ.* d₁ ℤ.* d₂
    lemma n₁ d₁ n₂ d₂ n₃ d₃
      rewrite *-assoc n₁ d₂ d₃
            | *-comm d₂ d₃
            | sym (*-assoc n₁ d₃ d₂)
            | *-assoc n₃ d₂ d₁
            | *-comm d₂ d₁
            | sym (*-assoc n₃ d₁ d₂)
            | *-assoc n₂ d₁ d₃
            | *-comm d₁ d₃
            | sym (*-assoc n₂ d₃ d₁)
            = ℤO.trans

  antisym : Antisymmetric _≡_ _≤_
  antisym (*≤* le₁) (*≤* le₂) = ≃⇒≡ (ℤO.antisym le₁ le₂)

  total : Total _≤_
  total p q =
    [ inj₁ ∘′ *≤* , inj₂ ∘′ *≤* ]′
      (ℤO.total (ℚ.numerator p ℤ.* ℚ.denominator q)
                (ℚ.numerator q ℤ.* ℚ.denominator p))


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

module Categories.Category.Construction.Properties.Presheaves.CartesianClosed where

open import Level
open import Data.Unit
open import Data.Product using (_,_; proj₁; proj₂)
open import Function.Equality using (Π) renaming (_∘_ to _∙_)
open import Relation.Binary

open import Categories.Category.Core using (Category)
open import Categories.Category.CartesianClosed
open import Categories.Category.CartesianClosed.Canonical renaming (CartesianClosed to CCartesianClosed)
open import Categories.Category.Construction.Presheaves
open import Categories.Category.Instance.Setoids
open import Categories.Functor
open import Categories.Functor.Hom
open import Categories.Functor.Properties
open import Categories.Functor.Presheaf
open import Categories.NaturalTransformation

import Categories.Category.Construction.Properties.Presheaves.Cartesian as Preₚ
import Categories.Morphism.Reasoning as MR
import Relation.Binary.Reasoning.Setoid as SetoidR

open Π using (_⟨$⟩_)

module HasClosed {o ℓ e} (C : Category o ℓ e) where
  private
    module C = Category C
    open C

  module _ (F G : Presheaf C (Setoids ℓ e)) where
    private
      module F = Functor F
      module G = Functor G
      open Preₚ C
      open IsCartesian o o

    Presheaf^ : Presheaf C (Setoids (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e))
    Presheaf^ = record
      { F₀           = λ X → Hom[ Presheaves C ][ Presheaves× Hom[ C ][-, X ] G , F ]
      ; F₁           = λ {A B} f → record
        { _⟨$⟩_ = λ α →
          let module α = NaturalTransformation α using (η; commute)
          in ntHelper record
          { η       = λ X → record
            { _⟨$⟩_ = λ where (g , S) → α.η X ⟨$⟩ (f ∘ g , S)
            ; cong  = λ where (eq₁ , eq₂) → Π.cong (α.η X) (∘-resp-≈ʳ eq₁ , eq₂)
            }
          ; commute = λ { {Z} {W} g {h , x} {i , y} (eq₁ , eq₂) →
            let open SetoidR (F.₀ W)
            in begin
              α.η W ⟨$⟩ (f ∘ C.id ∘ h ∘ g , G.₁ g ⟨$⟩ x)   ≈⟨ Π.cong (α.η W) (Equiv.trans (pullˡ id-comm) (center Equiv.refl) , Setoid.refl (G.₀ W)) ⟩
              α.η W ⟨$⟩ (C.id ∘ (f ∘ h) ∘ g , G.₁ g ⟨$⟩ x) ≈⟨ α.commute g (∘-resp-≈ʳ eq₁ , eq₂) ⟩
              F.₁ g ⟨$⟩ (α.η Z ⟨$⟩ (f ∘ i , y))            ∎ }
          }
        ; cong  = λ eq (eq₁ , eq₂) → eq (∘-resp-≈ʳ eq₁ , eq₂)
        }
      ; identity     = λ eq (eq₁ , eq₂) → eq (Equiv.trans identityˡ eq₁ , eq₂)
      ; homomorphism = λ eq (eq₁ , eq₂) → eq (pullʳ (∘-resp-≈ʳ eq₁) , eq₂)
      ; F-resp-≈     = λ where eq eq′ (eq₁ , eq₂) → eq′ (∘-resp-≈ eq eq₁ , eq₂)
      } where open MR C

module IsCartesianClosed {o} (C : Category o o o) where
  private
    module C = Category C using (id; _∘_; _≈_; identityˡ; identityʳ; module Equiv)
    P = Presheaves′ o o C
    open HasClosed C using (Presheaf^)
    open Preₚ.IsCartesian C o o using (Presheaves-Cartesian)
    open MR C

  CanonicalCCC : CCartesianClosed P
  CanonicalCCC = record
    { ⊤            = PC.terminal.⊤
    ; _×_          = PC._×_
    ; !            = PC.!
    ; π₁           = PC.π₁
    ; π₂           = PC.π₂
    ; ⟨_,_⟩        = PC.⟨_,_⟩
    ; !-unique     = PC.!-unique
    ; π₁-comp      = λ {_ _ f} {_ g} → PC.project₁ {h = f} {g}
    ; π₂-comp      = λ {_ _ f} {_ g} → PC.project₂ {h = f} {g}
    ; ⟨,⟩-unique   = λ {_ _ _ f g h} → PC.unique {h = h} {i = f} {j = g}
    ; _^_          = Presheaf^
    ; eval         = λ {F G} →
      let module F = Functor F
          module G = Functor G
      in ntHelper record
      { η       = λ X → record
        { _⟨$⟩_ = λ { (α , x) →
          let module α = NaturalTransformation α
          in α.η X ⟨$⟩ (C.id , x) }
        ; cong  = λ where (eq₁ , eq₂) → eq₁ (C.Equiv.refl , eq₂)
        }
      ; commute = λ { {Y} {Z} f {α , x} {β , y} (eq₁ , eq₂) →
        let module α = NaturalTransformation α
            module β = NaturalTransformation β
            open SetoidR (F.₀ Z)
        in begin
        α.η Z ⟨$⟩ (f C.∘ C.id , G.₁ f ⟨$⟩ x)          ≈⟨ eq₁ ((C.Equiv.trans id-comm (C.Equiv.sym C.identityˡ)) , Setoid.refl (G.₀ Z)) ⟩
        β.η Z ⟨$⟩ (C.id C.∘ C.id C.∘ f , G.₁ f ⟨$⟩ x) ≈⟨ β.commute f (C.Equiv.refl , eq₂) ⟩
        F.₁ f ⟨$⟩ (β.η Y ⟨$⟩ (C.id , y))              ∎ }
      }
    ; curry        = λ {F G H} α →
      let module F = Functor F
          module G = Functor G
          module H = Functor H
          module α = NaturalTransformation α
      in ntHelper record
      { η       = λ X → record
        { _⟨$⟩_ = λ x → ntHelper record
          { η       = λ Y → record
            { _⟨$⟩_ = λ where (f , y) → α.η Y ⟨$⟩ (F.₁ f ⟨$⟩ x , y)
            ; cong  = λ where (eq₁ , eq₂) → Π.cong (α.η _) (F.F-resp-≈ eq₁ (Setoid.refl (F.₀ _)) , eq₂)
            }
          ; commute = λ { {Y} {Z} f {g , y} {h , z} (eq₁ , eq₂) →
            let open SetoidR (H.₀ Z)
                open Setoid  (G.₀ Z)
            in begin
              α.η Z ⟨$⟩ (F.F₁ (C.id C.∘ g C.∘ f) ⟨$⟩ x , G.F₁ f ⟨$⟩ y)
                ≈⟨ Π.cong (α.η Z) (F.F-resp-≈ C.identityˡ (Setoid.refl (F.₀ X)) , refl) ⟩
              α.η Z ⟨$⟩ (F.F₁ (g C.∘ f) ⟨$⟩ x , G.F₁ f ⟨$⟩ y)
                ≈⟨ Π.cong (α.η Z) (F.homomorphism (Setoid.refl (F.₀ X)) , refl) ⟩
              α.η Z ⟨$⟩ (F.F₁ f ⟨$⟩ (F.F₁ g ⟨$⟩ x) , G.F₁ f ⟨$⟩ y)
                ≈⟨ α.commute f (F.F-resp-≈ eq₁ (Setoid.refl (F.₀ X)) , eq₂) ⟩
              H.F₁ f ⟨$⟩ (α.η Y ⟨$⟩ (F.F₁ h ⟨$⟩ x , z))
                ∎ }
          }
          ; cong  = λ where eq (eq₁ , eq₂) → Π.cong (α.η _) (F.F-resp-≈ eq₁ eq , eq₂)
        }
      ; commute = λ { {X} {Y} f {x} {y} eq {Z} {g , z} {h , w} (eq₁ , eq₂) →
        let open SetoidR (F.₀ Z)
            helper : g C.≈ h → Setoid._≈_ (F.₀ X) x y →
                     Setoid._≈_ (F.₀ Z) (F.₁ g ⟨$⟩ (F.₁ f ⟨$⟩ x)) (F.₁ (f C.∘ h) ⟨$⟩ y)
            helper eq eq′ = begin
              F.₁ g ⟨$⟩ (F.₁ f ⟨$⟩ x) ≈⟨ F.F-resp-≈ eq (Setoid.refl (F.₀ Y)) ⟩
              F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ x) ≈˘⟨ F.homomorphism (Setoid.sym (F.₀ X) eq′) ⟩
              F.₁ (f C.∘ h) ⟨$⟩ y     ∎
        in Π.cong (α.η _) (helper eq₁ eq , eq₂) }
      }
    ; eval-comp    = λ {F G H} {α} → λ { (eq₁ , eq₂) →
      let module H  = Functor H
          module α  = NaturalTransformation α
      in Π.cong (α.η _) (H.identity eq₁ , eq₂) }
    ; curry-resp-≈ = λ { {F} {G} eq eq₁ (eq₂ , eq₃) →
      let module G = Functor G
      in eq (G.F-resp-≈ eq₂ eq₁ , eq₃) }
    ; curry-unique = λ {F G H} {α β} eq {X} {x y} eq₁ → λ { {Y} {f , z} {g , w} (eq₂ , eq₃) →
      let module F = Functor F
          module G = Functor G
          module H = Functor H
          module α = NaturalTransformation α
          module β = NaturalTransformation β
          module αXx = NaturalTransformation (α.η X ⟨$⟩ x)
          open Setoid  (H.₀ Y)
          open SetoidR (G.₀ Y)
      in begin
        αXx.η Y ⟨$⟩ (f , z)
          ≈⟨ Π.cong (αXx.η _) (C.Equiv.sym C.identityʳ , refl) ⟩
        αXx.η Y ⟨$⟩ (f C.∘ C.id , z)
          ≈⟨ α.sym-commute f (Setoid.refl (F.₀ X)) (C.Equiv.refl , refl) ⟩
        NaturalTransformation.η (α.η Y ⟨$⟩ (F.F₁ f ⟨$⟩ x)) Y ⟨$⟩ (C.id , z)
          ≈⟨ eq (F.F-resp-≈ eq₂ eq₁ , eq₃) ⟩
        β.η Y ⟨$⟩ (F.F₁ g ⟨$⟩ y , w)
          ∎ }
    }
    where module PC = Presheaves-Cartesian

  Presheaves-CartesianClosed : CartesianClosed P
  Presheaves-CartesianClosed = Equivalence.fromCanonical P CanonicalCCC

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
------------------------------------------------------------------------
-- The delay monad, defined using increasing sequences of potential
-- values
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

module Delay-monad.Alternative where

open import Equality.Propositional
open import Prelude hiding (↑)

------------------------------------------------------------------------
-- _↓_ and _↑

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

  infix 4 _↑ _↓_

  -- x ↓ y means that the computation x has the value y.

  _↓_ : Maybe A → A → Type a
  x ↓ y = x ≡ just y

  -- x ↑ means that the computation x does not have a value.

  _↑ : Maybe A → Type a
  x ↑ = x ≡ nothing

------------------------------------------------------------------------
-- An alternative definition of the delay monad

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

  -- The property of being an increasing sequence.

  LE : Maybe A → Maybe A → Type a
  LE x y = x ≡ y ⊎ (x ↑ × ¬ y ↑)

  Increasing-at : ℕ → (ℕ → Maybe A) → Type a
  Increasing-at n f = LE (f n) (f (suc n))

  Increasing : (ℕ → Maybe A) → Type a
  Increasing f = ∀ n → Increasing-at n f

-- An alternative definition of the delay monad.

Delay : ∀ {a} → Type a → Type a
Delay A = ∃ λ (f : ℕ → Maybe A) → Increasing f

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Issue481InstantiatedImportOnly where

import Common.Issue481ParametrizedModule Set
-- pointless, should yield error


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

module HITs.PropositionalTruncation where

open import Cubical.HITs.PropositionalTruncation
  using (squash; ∥_∥; ∣_∣; rec)
  renaming (rec→Set to rec→set)
  public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/masters-thesis

max_forks_repo_name: oisdk/masters-thesis


text:
------------------------------------------------------------------------
-- Lists with fast append
------------------------------------------------------------------------

module Data.DifferenceList where

open import Data.List as L using (List)
open import Data.Function
open import Data.Nat

infixr 5 _∷_ _++_

DiffList : Set → Set
DiffList a = List a → List a

lift : ∀ {a} → (List a → List a) → (DiffList a → DiffList a)
lift f xs = λ k → f (xs k)

[] : ∀ {a} → DiffList a
[] = λ k → k

_∷_ : ∀ {a} → a → DiffList a → DiffList a
_∷_ x = lift (L._∷_ x)

[_] : ∀ {a} → a → DiffList a
[ x ] = x ∷ []

_++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
xs ++ ys = λ k → xs (ys k)

toList : ∀ {a} → DiffList a → List a
toList xs = xs L.[]

-- fromList xs is linear in the length of xs.

fromList : ∀ {a} → List a → DiffList a
fromList xs = λ k → xs ⟨ L._++_ ⟩ k

-- It is OK to use L._++_ here, since map is linear in the length of
-- the list anyway.

map : ∀ {a b} → (a → b) → DiffList a → DiffList b
map f xs = λ k → L.map f (toList xs) ⟨ L._++_ ⟩ k

-- concat is linear in the length of the outer list.

concat : ∀ {a} → DiffList (DiffList a) → DiffList a
concat xs = concat' (toList xs)
  where
  concat' : ∀ {a} → List (DiffList a) → DiffList a
  concat' = L.foldr _++_ []

take : ∀ {a} → ℕ → DiffList a → DiffList a
take n = lift (L.take n)

drop : ∀ {a} → ℕ → DiffList a → DiffList a
drop n = lift (L.drop n)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module FStream.Core where

------------------------------------------------------------------------
-- Core module of effectful streams
------------------------------------------------------------------------

open import Library

mutual
  record FStream {i : Size} {ℓ₁ ℓ₂} (C : Container ℓ₁) (A : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    inductive
    field
      inF : ⟦ C ⟧ (FStream' {i} C A)
  record FStream' {i : Size} {ℓ₁ ℓ₂} (C : Container ℓ₁) (A : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    constructor _≺_
    coinductive
    field
      head : A
      tail : {j : Size< i} → FStream {j} C A
open FStream public
open FStream' public

-- TODO Remove nonworking things and put all auxiliary functions in Util.agda

postulate
  _►_ : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} →
    ⟦ C ⟧ A → FStream C A → FStream C A
--inF (a ► as) = fmap (λ x → x ≺ as) a

-- Caution, this one pushes the side effects down one tick
mutual
  _►'_ : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} →
    A → FStream {i} C A → FStream {i} C A
  inF (a ►' as) = fmap (aux a) (inF as)

  aux  : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} →
    A → FStream' {i} C A → FStream' {i} C A
  head (aux a as) = a
  tail (aux a as) = head as ►' tail as

-- TODO Write without the direct recursion
{-# TERMINATING #-}
_►⋯' : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} → A → FStream {i} C A
a ►⋯' = a ►' (a ►⋯')

mutual
  map : ∀ {i ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂} {B : Set ℓ₃} →
    (A → B) → FStream {i} C A → FStream {i} C B
  inF (map f as) = fmap (map' f) (inF as)

  map' : ∀ {i ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂} {B : Set ℓ₃} →
    (A → B) → FStream' {i} C A → FStream' {i} C B
  head (map' f as) = f (head as)
  tail (map' f as) = map f (tail as)

mutual
  constantly : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} →
    ⟦ C ⟧ A → FStream {i} C A
  inF (constantly ca) = fmap (constantly' ca) ca

  constantly' : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} →
    ⟦ C ⟧ A → A → FStream' {i} C A
  head (constantly' ca a) = a
  tail (constantly' ca a) = constantly ca

repeat : {A : Set} → {C : Container ℓ₀} → ⟦ C ⟧ A -> FStream C A
proj₁ (inF (repeat (proj₁ , proj₂))) = proj₁
head (proj₂ (inF (repeat (proj₁ , proj₂))) x) = proj₂ x
tail (proj₂ (inF (repeat (proj₁ , proj₂))) x) = repeat (proj₁ , proj₂)

mutual
  corec : ∀ {i ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂} {X : Set ℓ₃} →
    (X → A × ⟦ C ⟧ X) → ⟦ C ⟧ X → FStream {i} C A
  inF (corec f x) = fmap (corec' f) x

  corec' : ∀ {i ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂} {X : Set ℓ₃} →
    (X → A × ⟦ C ⟧ X) → X → FStream' {i} C A
  head (corec' f x) = proj₁ (f x)
  tail (corec' f x) = corec f (proj₂ (f x))

{-
Stuff that doesn't obviously work:
* drop, _at_ (Since side effects would have to be thrown away)
  (One could at most delay the side effects somehow?)
* _▸⋯  (Only if the given value is effectful or the functor is pointed, i.e. has a null effect (like Applicative or Monad), or by delaying the side effects)
-}

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
module lift-tests where

open import lib
open import cedille-types
open import convervsion
open import ctxt
open import lift
open import syntax-util
open import to-string

t0 = Lft posinfo-gen "X" (Parens posinfo-gen (mlam "x" (mlam "y" (mvar "y"))) posinfo-gen)
       (LiftArrow (LiftStar posinfo-gen) (LiftArrow (LiftStar posinfo-gen) (LiftStar posinfo-gen)))

t = TpApp (TpApp t0 (mall "X" (Tkk star) (TpArrow (mtpvar "X") (mtpvar "X")))) (mtpvar "False")

s = type-to-string t

s1 = type-to-string (hnf new-ctxt tt t)

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
-- 2012-03-08 Andreas
module NoTerminationCheck3 where

data Bool : Set where
  true false : Bool

f : Bool -> Bool
f true = true
{-# NO_TERMINATION_CHECK #-}
f false = false

-- error: cannot place pragma inbetween clauses

max_stars_repo_name: asr/agda-kanso


text:
module Foundation.Primitive where

open import Agda.Primitive

infix -65536 ℞_
℞_ : ∀ ℓ → Set _
℞_ ℓ = Set ℓ

⟰ : Level → Level
⟰ = lsuc

infix -65536 ℞₁_
℞₁_ : ∀ ℓ → Set _
℞₁_ ℓ = ℞ ⟰ ℓ

𝟘 : Level
𝟘 = lzero

open import Agda.Primitive using (_⊔_) public


text:
{-# OPTIONS --safe #-}
module Cubical.Codata.EverythingSafe where

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module OscarEverything where

open import OscarPrelude


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

open import HoTT
open import homotopy.SphereEndomorphism
open import groups.Pointed
open import groups.SphereEndomorphism
open import groups.FromSusp
open import cohomology.Theory

module cohomology.SphereEndomorphism (CT : CohomologyTheory lzero) (n : ℤ) (m : ℕ) where

  open CohomologyTheory CT
  open import cohomology.Cogroup CT n
    (Susp-cogroup-structure (⊙Sphere m))
    (⊙Sphere (S m))

  private
    C-fmap' : Trunc-⊙Sphere-endo (S m) → (C n (⊙Sphere (S m)) →ᴳ C n (⊙Sphere (S m)))
    C-fmap' = Trunc-rec λ f → C-fmap n f

    CEl-fmap' : Trunc-⊙Sphere-endo (S m) → (CEl n (⊙Sphere (S m)) → CEl n (⊙Sphere (S m)))
    CEl-fmap' f = GroupHom.f (C-fmap' f)

    C-fmap'-hom : Trunc-⊙SphereS-endo-group m →ᴳ
      (hom-group (C n (⊙Sphere (S m))) (C-abgroup n (⊙Sphere (S m))))
    C-fmap'-hom = group-hom C-fmap'
      (Trunc-elim λ f → Trunc-elim λ g → C-fmap-preserves-comp f g)

    CEl-fmap'-η : ∀ (f : Trunc-⊙Sphere-endo (S m)) (g : CEl n (⊙Sphere (S m)))
      → CEl-fmap' f g == Group.exp (C n (⊙Sphere (S m))) g (Trunc-⊙SphereS-endo-degree m f)
    CEl-fmap'-η f g =
      CEl-fmap' f g
        =⟨ ! $ ap (λ f → CEl-fmap' f g) $ is-equiv.f-g (Trunc-⊙SphereS-endo-⊙group-is-infinite-cyclic m) f ⟩
      CEl-fmap' (Group.exp (Trunc-⊙SphereS-endo-group m) [ ⊙idf _ ] (Trunc-⊙SphereS-endo-degree m f)) g
        =⟨ GroupHom.pres-exp
            (app-hom g ∘ᴳ C-fmap'-hom)
            [ ⊙idf _ ]
            (Trunc-⊙SphereS-endo-degree m f) ⟩
      Group.exp
        (C n (⊙Sphere (S m)))
        (CEl-fmap' [ ⊙idf _ ] g)
        (Trunc-⊙SphereS-endo-degree m f)
        =⟨ ap (λ g → Group.exp (C n (⊙Sphere (S m))) g (Trunc-⊙SphereS-endo-degree m f)) $
              CEl-fmap-idf n g  ⟩
      Group.exp
        (C n (⊙Sphere (S m))) g
        (Trunc-⊙SphereS-endo-degree m f)
        =∎
  abstract
    CEl-fmap-⊙Sphere-endo-η : ∀ (f : ⊙Sphere-endo (S m)) (g : CEl n (⊙Sphere (S m)))
      → CEl-fmap n f g == Group.exp (C n (⊙Sphere (S m))) g (⊙SphereS-endo-degree m f)
    CEl-fmap-⊙Sphere-endo-η f = CEl-fmap'-η [ f ]

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --rewriting #-}
module CF.Contexts.Rewriting where

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

open import Agda.Builtin.Equality.Rewrite
open import Relation.Binary.PropositionalEquality
open import CF.Types

++-assoc-← : ∀ (xs ys zs : List Ty) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
++-assoc-← = λ x y z → sym (++-assoc x y z)

++-identityʳ-← : ∀ (xs : List Ty) → xs ++ [] ≡ xs
++-identityʳ-← xs = ++-identityʳ xs

{-# REWRITE ++-assoc-← #-}
{-# REWRITE ++-identityʳ-← #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the reflective ring solver may be used.
------------------------------------------------------------------------

module README.Tactic.RingSolver where

-- You can ignore this bit! We're just overloading the literals Agda uses for
-- numbers. This bit isn't necessary if you're just using Nats, or if you
-- construct your type directly. We only really do it here so that we can use
-- different numeric types in the same file.

open import Agda.Builtin.FromNat
open import Data.Nat using (ℕ)
open import Data.Integer using (ℤ)
import Data.Nat.Literals as ℕ
import Data.Integer.Literals as ℤ

instance
  numberNat : Number ℕ
  numberNat = ℕ.number

instance
  numberInt : Number ℤ
  numberInt = ℤ.number

------------------------------------------------------------------------------
-- Imports!

open import Data.List as List using (List; _∷_; [])
open import Function
open import Relation.Binary.PropositionalEquality as ≡
  using (subst; _≡_; module ≡-Reasoning)
open import Data.Bool as Bool using (Bool; true; false; if_then_else_)
open import Data.Unit using (⊤; tt)

open import Tactic.RingSolver.Core.AlmostCommutativeRing using (AlmostCommutativeRing)

------------------------------------------------------------------------------
-- Integer examples
------------------------------------------------------------------------------

module IntegerExamples where
  open import Data.Integer.Tactic.RingSolver

  open AlmostCommutativeRing ring

  -- Everything is automatic: you just ask Agda to solve it and it does!
  lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 3 + 1 + y + x + - 1
  lemma₁ = solve-∀

  lemma₂ : ∀ x y → (x + y) ^ 2 ≈ x ^ 2 + 2 * x * y + y ^ 2
  lemma₂ = solve-∀

  -- It can interact with manual proofs as well.
  lemma₃ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x
  lemma₃ x y = begin
    x + y * 1 + 3 ≡⟨ +-comm x (y * 1) ⟨ +-cong ⟩ refl ⟩
    y * 1 + x + 3 ≡⟨ solve (x ∷ y ∷ []) ⟩
    3 + y + x     ≡⟨⟩
    2 + 1 + y + x ∎
    where open ≡-Reasoning

------------------------------------------------------------------------------
-- Natural examples
------------------------------------------------------------------------------

module NaturalExamples where
  open import Data.Nat.Tactic.RingSolver

  open AlmostCommutativeRing ring

  -- The solver is flexible enough to work with ℕ (even though it asks
  -- for rings!)
  lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x
  lemma₁ = solve-∀

------------------------------------------------------------------------------
-- Checking invariants
------------------------------------------------------------------------------
-- The solver makes it easy to prove invariants, without having to rewrite
-- proof code every time something changes in the data structure.

module _ {a} {A : Set a} (_≤_ : A → A → Bool) where
  open import Data.Nat.Tactic.RingSolver
  open AlmostCommutativeRing ring

  -- A Skew Heap, indexed by its size.
  data Tree : ℕ → Set a where
    leaf : Tree 0
    node : ∀ {n m} → A → Tree n → Tree m → Tree (1 + n + m)

  -- A substitution operator, to clean things up.
  infixr 1 _⇒_
  _⇒_ : ∀ {n} → Tree n → ∀ {m} → n ≈ m → Tree m
  x ⇒ n≈m  = subst Tree n≈m x

  open ≡-Reasoning

  _∪_ : ∀ {n m} → Tree n → Tree m → Tree (n + m)
  leaf                 ∪ ys                   = ys
  node {a} {b} x xl xr ∪ leaf                 =
    node x xl xr ⇒ solve (a ∷ b ∷ [])
  node {a} {b} x xl xr ∪ node {c} {d} y yl yr =
      if x ≤ y
        then node x (node y yl yr ∪ xr) xl ⇒ begin
          1 + (1 + c + d + b) + a ≡⟨ solve (a ∷ b ∷ c ∷ d ∷ []) ⟩
          1 + a + b + (1 + c + d) ∎
        else node y (node x xl xr ∪ yr) yl ⇒ begin
          1 + (1 + a + b + d) + c ≡⟨ solve (a ∷ b ∷ c ∷ d ∷ []) ⟩
          1 + a + b + (1 + c + d) ∎


text:
{-# OPTIONS --sized-types #-}
-- {-# OPTIONS -v tc.size.solve:100 -v tc.meta.new:50 #-}
module CheckSizeMetaBounds where

open import Common.Size

postulate
  Size< : (_ : Size) → Set
{-# BUILTIN SIZELT Size< #-}

data Nat {i : Size} : Set where
  zero : Nat
  suc  : {j : Size< i} → Nat {j} → Nat

one : Nat
one = suc {i = ∞} zero

data ⊥ : Set where
record ⊤ : Set where

NonZero : Nat → Set
NonZero zero    = ⊥
NonZero (suc n) = ⊤

-- magic conversion must of course fail
magic : {i : Size} → Nat {∞} → Nat {i}
magic zero = zero
magic (suc n) = suc (magic n)

lem : (n : Nat) → NonZero n → NonZero (magic n)
lem (zero)  ()
lem (suc n) _ = _

-- otherwise, we exploit it for an infinite loop
loop : {i : Size} → (x : Nat {i}) → NonZero x → ⊥
loop zero ()
loop (suc {j} n) p = loop {j} (magic one) (lem one _)

bot : ⊥
bot = loop one _

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- The bug documented below was exposed by the fix to issue 274.

module Issue274 where

open import Common.Level

record Q a : Set (a ⊔ a) where

record R a : Set a where
  field q : Q a

  A : Set₁
  A = Set

postulate
  ℓ : Level
  r : R (ℓ ⊔ ℓ)

foo : R ℓ
foo = r

-- Issue274.agda:32,7-8
-- ℓ ⊔ ℓ !=< ℓ of type Level
-- when checking that the expression r has type R ℓ

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --copatterns #-}

module SplitResult where

open import Common.Product

test : {A B : Set} (a : A) (b : B) → A × B
test a b = {!!}
-- expected:
-- proj₁ (test a b) = {!!}
-- proj₂ (test a b) = {!!}

testFun : {A B : Set} (a : A) (b : B) → A × B
testFun = {!!}
-- expected:
-- testFun a b = {!!}

record FunRec A : Set where
  field funField : A → A
open FunRec

testFunRec : ∀{A} → FunRec A
testFunRec = {!!}
-- expected (since 2016-05-03):
-- funField testFunRec = {!!}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


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

module lib.types.Suspension where

open import lib.types.Suspension.Core public
open import lib.types.Suspension.Flip public
open import lib.types.Suspension.Iterated public
open import lib.types.Suspension.IteratedFlip public
open import lib.types.Suspension.IteratedTrunc public
open import lib.types.Suspension.IteratedEquivs public
open import lib.types.Suspension.Trunc public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational numbers
------------------------------------------------------------------------

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

module Data.Rational where

open import Data.Integer as ℤ using (ℤ; +_)
open import Data.String using (String; _++_)

------------------------------------------------------------------------
-- Publicly re-export contents of core module

open import Data.Rational.Base public

------------------------------------------------------------------------
-- Publicly re-export queries

open import Data.Nat.Properties public
  using (_≟_; _≤?_)

------------------------------------------------------------------------
-- Method for displaying rationals

show : ℚ → String
show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)

------------------------------------------------------------------------
-- Deprecated

-- Version 1.0

open import Data.Rational.Properties public
  using (drop-*≤*; ≃⇒≡; ≡⇒≃)


text:
module Data.Num.Redundant.Properties where

open import Data.Num.Bij
open import Data.Num.Redundant renaming (_+_ to _+R_)

open import Data.Nat renaming (_<_ to _<ℕ_)
open import Data.Nat.Etc
open import Data.Nat.Properties.Simple

open import Data.Sum
open import Data.List hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; cong₂; trans; sym; inspect)
open PropEq.≡-Reasoning

--------------------------------------------------------------------------------
--  Digits
--------------------------------------------------------------------------------

⊕-comm : (a b : Digit) → a ⊕ b ≡ b ⊕ a
⊕-comm zero zero = refl
⊕-comm zero one = refl
⊕-comm zero two = refl
⊕-comm one zero = refl
⊕-comm one one = refl
⊕-comm one two = refl
⊕-comm two zero = refl
⊕-comm two one = refl
⊕-comm two two = refl

⊕-assoc : (a b c : Digit) → (a ⊕ b) ⊕ c ≡ a ⊕ (b ⊕ c)
⊕-assoc zero b c = refl
⊕-assoc one zero c = refl
⊕-assoc one one zero = refl
⊕-assoc one one one = refl
⊕-assoc one one two = refl
⊕-assoc one two zero = refl
⊕-assoc one two one = refl
⊕-assoc one two two = refl
⊕-assoc two zero c = refl
⊕-assoc two one zero = refl
⊕-assoc two one one = refl
⊕-assoc two one two = refl
⊕-assoc two two zero = refl
⊕-assoc two two one = refl
⊕-assoc two two two = refl

⊕-right-identity : (a : Digit) → a ⊕ zero ≡ a
⊕-right-identity zero = refl
⊕-right-identity one = refl
⊕-right-identity two = refl

⊙-comm : (a b : Digit) → a ⊙ b ≡ b ⊙ a
⊙-comm zero zero = refl
⊙-comm zero one = refl
⊙-comm zero two = refl
⊙-comm one zero = refl
⊙-comm one one = refl
⊙-comm one two = refl
⊙-comm two zero = refl
⊙-comm two one = refl
⊙-comm two two = refl

--------------------------------------------------------------------------------
--  Sequence of Digits
--------------------------------------------------------------------------------
{-
[x∷xs≡0⇒xs≡0] : (d : Digit) → (xs : Redundant) → [ d ∷ xs ] ≡ [ zero ∷ [] ] → [ xs ] ≡ [ zero ∷ [] ]
[x∷xs≡0⇒xs≡0] d    []          _ = refl
[x∷xs≡0⇒xs≡0] zero (zero ∷ xs) p = {! no-zero-divisor 2 (0 + 2 * [ xs ]) (λ ()) p  !}
[x∷xs≡0⇒xs≡0] zero (one  ∷ xs) p = {!   !}
[x∷xs≡0⇒xs≡0] zero (two  ∷ xs) p = {!   !}
-- no-zero-divisor 2 ([ x ] + 2 * [ xs ]) (λ ()) p
[x∷xs≡0⇒xs≡0] one  (x ∷ xs) p = contradiction p (λ ())
[x∷xs≡0⇒xs≡0] two  (x ∷ xs) p = contradiction p (λ ())

[>>xs]≡2*[xs] : (xs : Redundant) → [ >> xs ] ≡ *2 [ xs ]
[>>xs]≡2*[xs] xs = refl

[n>>>xs]≡2^n*[xs] : (n : ℕ) → (xs : Redundant) → [ n >>> xs ] ≡ 2 ^ n *Bij [ xs ]
[n>>>xs]≡2^n*[xs] zero    xs = sym (+-right-identity [ xs ])
[n>>>xs]≡2^n*[xs] (suc n) xs =
    begin
        [ n >>> (zero ∷ xs) ]
    ≡⟨ [n>>>xs]≡2^n*[xs] n (zero ∷ xs) ⟩
        2 ^ n * [ zero ∷ xs ]
    ≡⟨ sym (*-assoc (2 ^ n) 2 [ xs ]) ⟩
        2 ^ n * 2 * [ xs ]
    ≡⟨ cong (λ x → x * [ xs ]) (*-comm (2 ^ n) 2) ⟩
        2 * 2 ^ n * [ xs ]
    ∎

-- >> 0 ≈ 0
>>-zero : (xs : Redundant) → xs ≈ zero ∷ [] → >> xs ≈ zero ∷ []
>>-zero []       _           = eq refl
>>-zero (x ∷ xs) (eq x∷xs≈0) = eq (begin
        *2 [ x ∷ xs ]
    ≡⟨ cong (λ w → 2 * w) x∷xs≈0 ⟩
        2 * 0
    ≡⟨ *-right-zero 2 ⟩
        0
    ∎)

-- << 0 ≈ 0
<<-zero : (xs : Redundant) → xs ≈ zero ∷ [] → << xs ≈ zero ∷ []
<<-zero []       _           = eq refl
<<-zero (x ∷ xs) (eq x∷xs≡0) = eq ([x∷xs≡0⇒xs≡0] x xs x∷xs≡0)
-}
{-
>>>-zero : ∀ {n} (xs : Redundant) → {xs≈0 : xs ≈ zero ∷ []} → n >>> xs ≈ zero ∷ []
>>>-zero {n} xs {eq xs≡0} = eq (
    begin
        [ n >>> xs ]
    ≡⟨ [n>>>xs]≡2^n*[xs] n xs ⟩
        2 ^ n * [ xs ]
    ≡⟨ cong (λ x → 2 ^ n * x) xs≡0 ⟩
        2 ^ n * 0
    ≡⟨ *-right-zero (2 ^ n) ⟩
        0
    ∎)

<<<-zero : (n : ℕ) (xs : Redundant) → {xs≈0 : xs ≈ zero ∷ []} → n <<< xs ≈ zero ∷ []
<<<-zero zero    [] = eq refl
<<<-zero (suc n) [] = eq refl
<<<-zero zero    (x ∷ xs) {x∷xs≈0}    = x∷xs≈0
<<<-zero (suc n) (x ∷ xs) {eq x∷xs≡0} = <<<-zero n xs {eq ([x∷xs≡0⇒xs≡0] x xs x∷xs≡0)}
-}
--------------------------------------------------------------------------------
--  Properties of the relations on Redundant
--------------------------------------------------------------------------------

≈-Setoid : Setoid _ _
≈-Setoid = record
    {   Carrier = Redundant
    ;   _≈_ = _≈_
    ;   isEquivalence = record
        {   refl = ≈-refl
        ;   sym = ≈-sym
        ;   trans = ≈-trans
        }
    }
    where
        ≈-refl : Reflexive _≈_
        ≈-refl = eq refl

        ≈-sym : Symmetric _≈_
        ≈-sym (eq a≈b) = eq (sym a≈b)

        ≈-trans : Transitive _≈_
        ≈-trans (eq a≈b) (eq b≈c) = eq (trans a≈b b≈c)

private
    ≤-isDecTotalOrder = DecTotalOrder.isDecTotalOrder decTotalOrder
    ≤-isTotalOrder = IsDecTotalOrder.isTotalOrder ≤-isDecTotalOrder
    ≤-total = IsTotalOrder.total ≤-isTotalOrder
    ≤-isPartialOrder = IsTotalOrder.isPartialOrder ≤-isTotalOrder
    ≤-antisym =  IsPartialOrder.antisym ≤-isPartialOrder
    ≤-isPreorder = IsPartialOrder.isPreorder ≤-isPartialOrder
    ≤-isEquivalence = IsPreorder.isEquivalence ≤-isPreorder
    ≤-reflexive = IsPreorder.reflexive ≤-isPreorder
    ≤-trans = IsPreorder.trans ≤-isPreorder

≲-refl : _≈_ ⇒ _≲_
≲-refl (eq [x]≡[y]) = {!   !} -- le (≤-reflexive [x]≡[y])

≲-trans : Transitive _≲_
≲-trans [a]≤[b] [b]≤[c] = {!   !} -- le (≤-trans [a]≤[b] [b]≤[c])

≲-antisym : Antisymmetric _≈_ _≲_
≲-antisym [x]≤[y] [y]≤[x] = {!   !} -- eq (≤-antisym [x]≤[y] [y]≤[x])

≲-isPreorder : IsPreorder _ _
≲-isPreorder = record
    {   isEquivalence = Setoid.isEquivalence ≈-Setoid
    ;   reflexive     = ≲-refl
    ;   trans         = ≲-trans
    }

≲-isPartialOrder : IsPartialOrder _ _
≲-isPartialOrder =  record
    {   isPreorder = ≲-isPreorder
    ;   antisym = ≲-antisym
    }
{-
≲-total : Total _≲_
≲-total x y with ≤-total [ x ] [ y ]
≲-total x y | inj₁ [x]≤[y] = inj₁ ? -- (le [x]≤[y])
≲-total x y | inj₂ [y]≤[x] = inj₂ ? -- (le [y]≤[x])

≲-isTotalOrder : IsTotalOrder _ _
≲-isTotalOrder = record
    {   isPartialOrder = ≲-isPartialOrder
    ;   total = ≲-total
    }

≲-isDecTotalOrder : IsDecTotalOrder _ _
≲-isDecTotalOrder = record
    {   isTotalOrder = ≲-isTotalOrder
    ;   _≟_ = _≈?_
    ;   _≤?_ = _≲?_
    }

≲-decTotalOrder : DecTotalOrder _ _ _
≲-decTotalOrder = record
    {   Carrier = Redundant
    ;   _≈_ = _≈_
    ;   _≤_ = _≲_
    ;   isDecTotalOrder = ≲-isDecTotalOrder
    }

a≲a+1 : (a : Redundant) → a ≲ incr one a
a≲a+1 []       = le z≤n
a≲a+1 (x ∷ xs) = le {!   !}

<-asym : Asymmetric _<_
<-asym {[]}     {[]}     (le ())      (le [y]<[[]])
<-asym {[]}     {y ∷ ys} (le [x]<[y]) (le [y]<[[]]) = {!   !}
<-asym {x ∷ xs} {[]}     (le [x]<[y]) (le [y]<[x∷xs]) = {!   !}
<-asym {x ∷ xs} {y ∷ ys} (le [x]<[y]) (le [y]<[x∷xs]) = {!   !}

<-irr : Irreflexive _≈_ _<_ -- goal: ¬ (x < y)
<-irr {a} {b} (eq [a]≡[b]) (le [a]<[b]) = {!   !}

trichotomous : Trichotomous _≈_ _<_
trichotomous x y with x ≈? y
trichotomous x y | yes p = tri≈ {!   !} p {!   !}
trichotomous x y | no ¬p with incr one x ≲? y
trichotomous x y | no ¬p | yes q = tri< q ¬p {!   !}
trichotomous x y | no ¬p | no ¬q = tri> ¬q ¬p {!   !}

-}

{-
    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ∎
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
-- Andreas, 2018-03-03, issue #2989
-- Internal error, fixable with additional 'reduce'.

-- {-# OPTIONS --show-implicit --show-irrelevant #-}
-- {-# OPTIONS -v tc.rec:70 -v tc:10 #-}

postulate
  N : Set
  P : N → Set

record Σ (A : Set) (B : A → Set) : Set where
  constructor pair
  field
    fst : A
    snd : B fst

Σ' : (A : Set) → (A → Set) → Set
Σ' = Σ

record R : Set where
  constructor mkR
  field
    .p : Σ' N P

f : R → Set
f x = let mkR (pair k p) = x in N

-- WAS:
-- Internal error in Agda.TypeChecking.Records.getRecordTypeFields
-- Error goes away if Σ' is replaced by Σ
-- or field is made relevant

-- SAME Problem:
-- f x = let record { p = pair k p } = x in N
-- f x = let record { p = record { fst = k ; snd = p }} = x in N

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Derivative where

  open import Sets
  open import Functor
  import Isomorphism

  ∂ : U -> U
  ∂ (K A)   = K [0]
  ∂ Id	    = K [1]
  ∂ (F + G) = ∂ F + ∂ G
  ∂ (F × G) = ∂ F × G + F × ∂ G

  open Semantics

  -- Plugging a hole
  plug-∂ : {X : Set}(F : U) -> ⟦ ∂ F ⟧ X -> X -> ⟦ F ⟧ X
  plug-∂ (K _)	()		 x
  plug-∂ Id	<>		 x = x
  plug-∂ (F + G) (inl c)	 x = inl (plug-∂ F c x)
  plug-∂ (F + G) (inr c)	 x = inr (plug-∂ G c x)
  plug-∂ (F × G) (inl < c , g >) x = < plug-∂ F c x , g >
  plug-∂ (F × G) (inr < f , c >) x = < f , plug-∂ G c x >

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra where

open import Cubical.Algebra.CommAlgebra.Base public
open import Cubical.Algebra.CommAlgebra.Properties public

max_stars_repo_name: FernandoLarrain/cubical


text:
-- Andreas, 2012-01-12
module Common.Irrelevance where

open import Common.Level

postulate
  .irrAxiom : ∀ {a}{A : Set a} → .A → A
{-# BUILTIN IRRAXIOM irrAxiom #-}

record Squash {a}(A : Set a) : Set a where
  constructor squash
  field
    .unsquash : A

open Squash public

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
-- define ∑ and ∏ as the bigOps of a Ring when interpreted
-- as an additive/multiplicative monoid

{-# OPTIONS --safe #-}
module Cubical.Algebra.Ring.BigOps where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Bool
open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.Sigma
open import Cubical.Data.FinData

open import Cubical.Algebra.Monoid.BigOp
open import Cubical.Algebra.Ring.Base
open import Cubical.Algebra.Ring.Properties

private
  variable
    ℓ ℓ' : Level

module KroneckerDelta (R' : Ring ℓ) where
 private
  R = fst R'
 open RingStr (snd R')

 δ : {n : ℕ} (i j : Fin n) → R
 δ i j = if i == j then 1r else 0r

module Sum (R' : Ring ℓ) where
 private
  R = fst R'
 open RingStr (snd R')
 open MonoidBigOp (Ring→AddMonoid R')
 open RingTheory R'
 open KroneckerDelta R'

 ∑ = bigOp
 ∑Ext = bigOpExt
 ∑0r = bigOpε
 ∑Last = bigOpLast

 ∑Split : ∀ {n} → (V W : FinVec R n) → ∑ (λ i → V i + W i) ≡ ∑ V + ∑ W
 ∑Split = bigOpSplit +Comm

 ∑Split++ : ∀ {n m : ℕ} (V : FinVec R n) (W : FinVec R m)
          → ∑ (V ++Fin W) ≡ ∑ V + ∑ W
 ∑Split++ = bigOpSplit++ +Comm

 ∑Mulrdist : ∀ {n} → (x : R) → (V : FinVec R n)
                → x · ∑ V ≡ ∑ λ i → x · V i
 ∑Mulrdist {n = zero}  x _ = 0RightAnnihilates x
 ∑Mulrdist {n = suc n} x V =
   x · (V zero + ∑ (V ∘ suc))           ≡⟨ ·DistR+ _ _ _ ⟩
   x · V zero + x · ∑ (V ∘ suc)         ≡⟨ (λ i → x · V zero + ∑Mulrdist x (V ∘ suc) i) ⟩
   x · V zero + ∑ (λ i → x · V (suc i)) ∎

 ∑Mulldist : ∀ {n} → (x : R) → (V : FinVec R n)
                → (∑ V) · x ≡ ∑ λ i → V i · x
 ∑Mulldist {n = zero}  x _ = 0LeftAnnihilates x
 ∑Mulldist {n = suc n} x V =
   (V zero + ∑ (V ∘ suc)) · x           ≡⟨ ·DistL+ _ _ _ ⟩
   V zero · x + (∑ (V ∘ suc)) · x       ≡⟨ (λ i → V zero · x + ∑Mulldist x (V ∘ suc) i) ⟩
   V zero · x + ∑ (λ i → V (suc i) · x) ∎

 ∑Mulr0 : ∀ {n} → (V : FinVec R n) → ∑ (λ i → V i · 0r) ≡ 0r
 ∑Mulr0 V = sym (∑Mulldist 0r V) ∙ 0RightAnnihilates _

 ∑Mul0r : ∀ {n} → (V : FinVec R n) → ∑ (λ i → 0r · V i) ≡ 0r
 ∑Mul0r V = sym (∑Mulrdist 0r V) ∙ 0LeftAnnihilates _

 ∑Mulr1 : (n : ℕ) (V : FinVec R n) → (j : Fin n) → ∑ (λ i → V i · δ i j) ≡ V j
 ∑Mulr1 (suc n) V zero = (λ k → ·IdR (V zero) k + ∑Mulr0 (V ∘ suc) k) ∙ +IdR (V zero)
 ∑Mulr1 (suc n) V (suc j) =
    (λ i → 0RightAnnihilates (V zero) i + ∑ (λ x → V (suc x) · δ x j))
    ∙∙ +IdL _ ∙∙ ∑Mulr1 n (V ∘ suc) j

 ∑Mul1r : (n : ℕ) (V : FinVec R n) → (j : Fin n) → ∑ (λ i → (δ j i) · V i) ≡ V j
 ∑Mul1r (suc n) V zero = (λ k → ·IdL (V zero) k + ∑Mul0r (V ∘ suc) k) ∙ +IdR (V zero)
 ∑Mul1r (suc n) V (suc j) =
   (λ i → 0LeftAnnihilates (V zero) i + ∑ (λ i → (δ j i) · V (suc i)))
   ∙∙ +IdL _ ∙∙ ∑Mul1r n (V ∘ suc) j

 ∑Dist- : ∀ {n : ℕ} (V : FinVec R n) → ∑ (λ i → - V i) ≡ - ∑ V
 ∑Dist- V = ∑Ext (λ i → -IsMult-1 (V i)) ∙ sym (∑Mulrdist _ V) ∙ sym (-IsMult-1 _)

module SumMap
  (Ar@(A , Astr) : Ring ℓ)
  (Br@(B , Bstr) : Ring ℓ')
  (f'@(f , fstr) : RingHom Ar Br)
  where

  open IsRingHom fstr

  open RingStr Astr using ()
    renaming
    ( _+_ to _+A_ )

  open RingStr Bstr using ()
    renaming
    ( _+_ to _+B_ )

  ∑Map : {n : ℕ} → (V : FinVec A n) → f (Sum.∑ Ar V) ≡ Sum.∑ Br (λ k → f (V k))
  ∑Map {n = zero} V = pres0
  ∑Map {n = suc n} V =
                       f ((V zero) +A helper) ≡⟨ pres+ (V zero) helper ⟩
                       ((f (V zero)) +B (f helper)) ≡⟨ cong (λ X → f (V zero) +B X) (∑Map (λ k → (V ∘ suc) k)) ⟩
                       Sum.∑ Br (λ k → f (V k)) ∎
                     where
                     helper : _
                     helper = foldrFin _+A_ (RingStr.0r (snd Ar)) (λ x → V (suc x))

-- anything interesting to prove here?
module Product (R' : Ring ℓ) where
 private
  R = fst R'
 open RingStr (snd R')
 open RingTheory R'
 open MonoidBigOp (Ring→MultMonoid R')

 ∏ = bigOp
 ∏Ext = bigOpExt
 ∏0r = bigOpε
 ∏Last = bigOpLast

-- only holds in CommRings!
-- ∏Split : ∀ {n} → (V W : FinVec R n) → ∏ (λ i → V i · W i) ≡ ∏ V · ∏ W
-- ∏Split = bigOpSplit MultR' ·-comm

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module UpTo where

open import Level
open import Relation.Binary using (Rel; IsEquivalence)
open import Data.Product
open import Categories.Support.Equivalence
open import Categories.Category
open import Categories.2-Category
open import Categories.Functor
open import Categories.NaturalTransformation
  renaming (id to natId; _≡_ to _≡N_; setoid to natSetoid)
  hiding (_∘ˡ_; _∘ʳ_)
open import Categories.Support.EqReasoning

open import NaturalTransFacts

Cat₀ = Category zero zero zero

EndoFunctor : Cat₀ → Set zero
EndoFunctor C = Functor C C

record Endo⇒ (C₁ : Cat₀) (F₁ : EndoFunctor C₁)
             (C₂ : Cat₀) (F₂ : EndoFunctor C₂)
             : Set zero where
  field
    T : Functor C₁ C₂
    ρ : NaturalTransformation (T ∘ F₁) (F₂ ∘ T)

record UpTo⇒ {C₁ : Cat₀} {F : EndoFunctor C₁}
             {C₂ : Cat₀} {G : EndoFunctor C₂}
             (S₁ S₂ : Endo⇒ C₁ F C₂ G)
             : Set zero where
  module S₁ = Endo⇒ S₁
  module S₂ = Endo⇒ S₂
  field
    γ : NaturalTransformation S₁.T S₂.T
    -- The following diagram must commute
    -- T₁F - ρ₁ -> GT₁
    --  |            |
    --  γF         Gγ
    --  |            |
    --  v            v
    -- T₂G - ρ₂ -> GT₂
    .square : S₂.ρ ∘₁ (γ ∘ʳ F) ≡N (G ∘ˡ γ) ∘₁ S₁.ρ

record _≡U_ {C₁ : Cat₀} {C₂ : Cat₀}
            {F : EndoFunctor C₁} {G : EndoFunctor C₂}
            {T₁ T₂ : Endo⇒ C₁ F C₂ G}
            (A : UpTo⇒ T₁ T₂) (B : UpTo⇒ T₁ T₂) : Set where
  field
    ≡U-proof : UpTo⇒.γ A ≡N UpTo⇒.γ B

open _≡U_
infix 4 _≡U_

.≡U-equiv : {C₁ : Cat₀} {C₂ : Cat₀}
            {F : EndoFunctor C₁} {G : EndoFunctor C₂} →
            {A B : Endo⇒ C₁ F C₂ G} →
            IsEquivalence {A = UpTo⇒ A B} (_≡U_ {C₁} {C₂} {F} {G})
≡U-equiv =
  record
  { refl = λ {A} → record { ≡U-proof = Setoid.refl natSetoid {UpTo⇒.γ A} }
  ; sym = λ {A} {B} p → record {
        ≡U-proof = Setoid.sym natSetoid {UpTo⇒.γ A} {UpTo⇒.γ B} (≡U-proof p) }
  ; trans = λ {A} {B} {C} p₁ p₂ → record {
          ≡U-proof = Setoid.trans natSetoid {UpTo⇒.γ A} {UpTo⇒.γ B} {UpTo⇒.γ C}
                     (≡U-proof p₁) (≡U-proof p₂) }
  }

id-UpTo⇒ : {C₁ : Cat₀} {F : EndoFunctor C₁}
           {C₂ : Cat₀} {G : EndoFunctor C₂}
           {A : Endo⇒ C₁ F C₂ G} → UpTo⇒ A A
id-UpTo⇒ {C₁} {F} {C₂} {G} {A} =
  record
      { γ = natId
      ; square =
        begin
          Endo⇒.ρ A ∘₁ (natId {F = Endo⇒.T A} ∘ʳ F)
        ↓⟨ ∘₁-resp-≡
           {f = Endo⇒.ρ A} {h = Endo⇒.ρ A}
           {g = natId {F = Endo⇒.T A} ∘ʳ F}
           {i = natId {F = Endo⇒.T A ∘ F}}
           (Setoid.refl natSetoid {Endo⇒.ρ A})
           (identityNatʳ {F = Endo⇒.T A} F)
         ⟩
          Endo⇒.ρ A ∘₁ (natId {F = Endo⇒.T A ∘ F})
        ↓⟨ identity₁ʳ {X = Endo⇒.ρ A} ⟩
          Endo⇒.ρ A
        ↑⟨ identity₁ˡ {X = Endo⇒.ρ A} ⟩
          natId {F = G ∘ Endo⇒.T A} ∘₁ Endo⇒.ρ A
        ↑⟨ ∘₁-resp-≡
           {f = G ∘ˡ natId {F = Endo⇒.T A}}
           {h = natId {F = G ∘ Endo⇒.T A}}
           {g = Endo⇒.ρ A} {i = Endo⇒.ρ A}
           (identityNatˡ {F = Endo⇒.T A} G)
           (Setoid.refl natSetoid {Endo⇒.ρ A})
         ⟩
          (G ∘ˡ natId {F = Endo⇒.T A}) ∘₁ Endo⇒.ρ A
        ∎
      }
        where
          open SetoidReasoning (natSetoid {F = Endo⇒.T A ∘ F} {G ∘ Endo⇒.T A})

_•_ : {C₁ : Cat₀} {F : EndoFunctor C₁}
             {C₂ : Cat₀} {G : EndoFunctor C₂}
             {A B C : Endo⇒ C₁ F C₂ G} →
             UpTo⇒ B C → UpTo⇒ A B → UpTo⇒ A C
_•_ {F = F} {G = G} {A = A} {B} {C} g f =
  record
  { γ = γ ∘₁ φ
  ; square =
    --     AF - A.ρ -> GA
    --     |           |
    --    φF          Gφ
    --     |           |
    --     v           v
    --    BF - B.ρ -> GB
    --     |           |
    --     γF         Gγ
    --     |           |
    --     v           v
    --    CF - C.ρ -> GC
    begin
      C.ρ ∘₁ ((γ ∘₁ φ) ∘ʳ F)
    ↓⟨ ∘₁-resp-≡ʳ
       {f = C.ρ} {(γ ∘₁ φ) ∘ʳ F} {(γ ∘ʳ F) ∘₁ (φ ∘ʳ F)}
       (∘ʳ-distr-∘₁ γ φ F)
     ⟩
      C.ρ ∘₁ ((γ ∘ʳ F) ∘₁ (φ ∘ʳ F))
    ↑⟨ assoc₁ {X = (φ ∘ʳ F)} {(γ ∘ʳ F)} {C.ρ} ⟩
      (C.ρ ∘₁ (γ ∘ʳ F)) ∘₁ (φ ∘ʳ F)
    ↓⟨ ∘₁-resp-≡ˡ
       {f = C.ρ ∘₁ (γ ∘ʳ F)} {G ∘ˡ γ ∘₁ B.ρ} {φ ∘ʳ F}
       (UpTo⇒.square g)
     ⟩
      (G ∘ˡ γ ∘₁ B.ρ) ∘₁ (φ ∘ʳ F)
    ↓⟨ assoc₁ {X = (φ ∘ʳ F)} {B.ρ} {G ∘ˡ γ} ⟩
      (G ∘ˡ γ) ∘₁ (B.ρ ∘₁ (φ ∘ʳ F))
    ↓⟨ ∘₁-resp-≡ʳ
       {f = G ∘ˡ γ} {B.ρ ∘₁ (φ ∘ʳ F)} {(G ∘ˡ φ) ∘₁ A.ρ}
       (UpTo⇒.square f)
     ⟩
      (G ∘ˡ γ) ∘₁ ((G ∘ˡ φ) ∘₁ A.ρ)
    ↑⟨ assoc₁ {X = A.ρ} {G ∘ˡ φ} {G ∘ˡ γ} ⟩
      ((G ∘ˡ γ) ∘₁ (G ∘ˡ φ)) ∘₁ A.ρ
    ↑⟨ ∘₁-resp-≡ˡ
       {f = G ∘ˡ (γ ∘₁ φ)} {(G ∘ˡ γ) ∘₁ (G ∘ˡ φ)}  {A.ρ}
       (∘ˡ-distr-∘₁ G γ φ)
     ⟩
      (G ∘ˡ (γ ∘₁ φ)) ∘₁ A.ρ
    ∎
  }
  where
    module A = Endo⇒ A
    module B = Endo⇒ B
    module C = Endo⇒ C
    open SetoidReasoning (natSetoid {F = A.T ∘ F} {G ∘ C.T})
    φ : A.T ⇒ B.T
    φ = UpTo⇒.γ f
    γ : B.T ⇒ C.T
    γ = UpTo⇒.γ g

-- | Category of morphisms between endofunctors, where the morphisms
-- are certain natural transformations (see UpTo⇒).
-- This category will be the the setting in which we can talk about
-- properties of up-to techniques.
EndoMor : Σ Cat₀ (λ C → Functor C C) →
          Σ Cat₀ (λ C → Functor C C) →
          Cat₀
EndoMor (C₁ , F) (C₂ , G) =
  record
  { Obj = Endo⇒ C₁ F C₂ G
  ; _⇒_ = UpTo⇒
  ; _≡_ = _≡U_
  ; id = id-UpTo⇒
  ; _∘_ = _•_
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} →
          record { ≡U-proof = assoc₁ {X = UpTo⇒.γ f} {UpTo⇒.γ g} {UpTo⇒.γ h} }
  ; identityˡ = λ {_} {_} {f} →
              record { ≡U-proof = identity₁ˡ {X = UpTo⇒.γ f} }
  ; identityʳ = λ {_} {_} {f} →
              record { ≡U-proof = identity₁ʳ {X = UpTo⇒.γ f} }
  ; equiv = ≡U-equiv
  ; ∘-resp-≡ = λ {_} {_} {_} {f} {h} {g} {i} f≡h g≡i → record {
             ≡U-proof = ∘₁-resp-≡ {f = UpTo⇒.γ f} {UpTo⇒.γ h}
                                  {UpTo⇒.γ g} {UpTo⇒.γ i}
                                  (≡U-proof f≡h) (≡U-proof g≡i) }
  }

-- | The 2-category of endofunctors, their morphisms and UpTo⇒ as 2-cells.
-- This is the 2-category of endofunctors defined by Lenisa, Power and Watanabe.
{-
Endo : 2-Category (suc zero) zero zero zero
Endo = record
         { Obj = Σ Cat₀ (λ C → Functor C C)
         ; _⇒_ = EndoMor
         ; id = record
                { F₀ = λ _ → record { T = id ; ρ = natId }
                ; F₁ = λ _ → id-UpTo⇒
                ; identity = IsEquivalence.refl ≡U-equiv
                ; homomorphism = λ {_} {_} {_} {_} {F} → {!!}
                ; F-resp-≡ = {!!}
                }
         ; —∘— = {!!}
         ; assoc = {!!}
         ; identityˡ = {!!}
         ; identityʳ = {!!}
         }
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
open import Oscar.Prelude
open import Oscar.Class.IsDecidable
open import Oscar.Data.Fin
open import Oscar.Data.Decidable
open import Oscar.Data.Proposequality

module Oscar.Class.IsDecidable.Fin where

instance

  IsDecidableFin : ∀ {n} → IsDecidable (Fin n)
  IsDecidableFin .IsDecidable._≟_ ∅ ∅ = ↑ ∅
  IsDecidableFin .IsDecidable._≟_ ∅ (↑ _) = ↓ λ ()
  IsDecidableFin .IsDecidable._≟_ (↑ _) ∅ = ↓ λ ()
  IsDecidableFin .IsDecidable._≟_ (↑ x) (↑ y) with x ≟ y
  … | ↑ ∅ = ↑ ∅
  … | ↓ x≢y = ↓ λ {∅ → x≢y ∅}


text:
------------------------------------------------------------------------------
-- Even predicate
------------------------------------------------------------------------------

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

module FOTC.Even where

open import FOTC.Base
open import FOTC.Data.Nat.Type

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

data Even : D → Set where
  ezero :                  Even zero
  enext : ∀ {n} → Even n → Even (succ₁ (succ₁ n))

Even-ind : (A : D → Set) →
           A zero →
           (∀ {n} → A n → A (succ₁ (succ₁ n))) →
           ∀ {n} → Even n → A n
Even-ind A A0 h ezero      = A0
Even-ind A A0 h (enext En) = h (Even-ind A A0 h En)

Even→N : ∀ {n} → Even n → N n
Even→N ezero      = nzero
Even→N (enext En) = nsucc (nsucc (Even→N En))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

-- Category of Lawvere Theories

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Functor.Cartesian using (CartesianF)
open import Categories.NaturalTransformation.NaturalIsomorphism
 using (_≃_; associator; sym-associator; unitorˡ; unitorʳ; unitor²; refl; sym; trans; _ⓘₕ_)
open import Categories.Theory.Lawvere using (LawvereTheory; LT-Hom; LT-id; LT-∘)

LawvereTheories : (ℓ e : Level) → Category (suc (ℓ ⊔ e)) (ℓ ⊔ e) (ℓ ⊔ e)
LawvereTheories ℓ e = record
  { Obj = LawvereTheory ℓ e
  ; _⇒_ = LT-Hom
  ; _≈_ = λ H₁ H₂ → cartF.F H₁ ≃ cartF.F H₂
  ; id = LT-id
  ; _∘_ = LT-∘
  ; assoc = λ { {f = f} {g} {h} → associator (cartF.F f) (cartF.F g) (cartF.F h) }
  ; sym-assoc = λ { {f = f} {g} {h} → sym-associator (cartF.F f) (cartF.F g) (cartF.F h) }
  ; identityˡ = unitorˡ
  ; identityʳ = unitorʳ
  ; identity² = unitor²
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = _ⓘₕ_
  }
  where open LT-Hom

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Oscar.Data.Maybe where

open import Data.Maybe public using (Maybe; nothing; just)

-- open import Oscar.Data.Maybe.Core public

-- --open import Data.Maybe public using (maybe)

-- -- open import Relation.Binary.PropositionalEquality
-- -- open import Data.Empty

-- -- unMaybe : ∀ {A : Set} {x y : A} {B : Set} {m : Maybe B} → maybe (λ _ → x) y m ≡ y → x ≢ y → m ≡ nothing
-- -- unMaybe {m = just x₁} x₂ x₃ = ⊥-elim (x₃ x₂)
-- -- unMaybe {m = nothing} x₁ x₂ = refl

-- -- unMaybe' : ∀ {A : Set} {y : A} {B : Set} {x : B → A} {m : Maybe B} → maybe (λ b → x b) y m ≡ y → (∀ b → x b ≢ y) → m ≡ nothing
-- -- unMaybe' {m = just x₁} x₂ x₃ = ⊥-elim (x₃ x₁ x₂)
-- -- unMaybe' {m = nothing} x₁ x₂ = refl

-- -- just≢nothing : ∀ {A B : Set} → (x : B → A) → ∀ b → Maybe.just (x b) ≢ nothing
-- -- just≢nothing x b ()

-- -- unMaybeJust' : ∀ {A B : Set} {P : B → A} {m : Maybe B} {n : A} {x : B} → maybe (λ b → P b) n m ≡ P x → (∀ b → P b ≢ n) → (∀ {y y'} → P y ≡ P y' → y ≡ y') → m ≡ just x
-- -- unMaybeJust' {m = just x} x₂ x₃ inj rewrite inj x₂ = refl
-- -- unMaybeJust' {m = nothing} x₁ x₂ _ = ⊥-elim (x₂ _ (sym x₁))


text:
{-# OPTIONS --rewriting #-}
module CF.Transform.Compile.ToJVM.Rewriting where

open import Data.List.Properties
open import Data.List.Relation.Binary.Permutation.Propositional

open import Agda.Builtin.Equality.Rewrite

{-# REWRITE map-++-commute #-}


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.RingSolver.RawRing where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Nat using (ℕ)

open import Cubical.Algebra.RingSolver.AlmostRing hiding (⟨_⟩)

private
  variable
    ℓ : Level

record RawRing : Type (ℓ-suc ℓ) where

  constructor rawring

  field
    Carrier : Type ℓ
    0r      : Carrier
    1r      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier

  infixl 8 _·_
  infixl 7 -_
  infixl 6 _+_

⟨_⟩ : RawRing → Type ℓ
⟨_⟩ = RawRing.Carrier

AlmostRing→RawRing : AlmostRing {ℓ} → RawRing {ℓ}
AlmostRing→RawRing (almostring Carrier 0r 1r _+_ _·_ -_ isAlmostRing) =
                   rawring Carrier 0r 1r _+_ _·_ -_

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Categories.Category.Finite.Fin.Construction.Poset where

open import Data.Nat using (ℕ; z≤n; s≤s)
open import Data.Sum
open import Data.Product using (Σ; _,_; _×_)
open import Data.Fin
open import Data.Fin.Patterns

open import Relation.Binary.PropositionalEquality as ≡

open import Categories.Category.Finite.Fin
open import Categories.Category

private
  card : ∀ {n} → Fin n → Fin n → ℕ
  card {ℕ.suc n} zero y          = 1
  card {ℕ.suc n} (suc x) zero    = 0
  card {ℕ.suc n} (suc x) (suc y) = card x y

  id : ∀ n {a : Fin n} → Fin (card a a)
  id .(ℕ.suc _) {zero} = 0F
  id (ℕ.suc n) {suc a} = id n

  comp : ∀ n {a b c : Fin n} → Fin (card b c) → Fin (card a b) → Fin (card a c)
  comp (ℕ.suc n) {0F} {b} {c} f g = 0F
  comp (ℕ.suc n) {suc a} {suc b} {suc c} f g = comp n f g

  assoc : ∀ n {a b c d : Fin n} {f : Fin (card a b)} {g : Fin (card b c)} {h : Fin (card c d)} →
              comp n (comp n h g) f ≡ comp n h (comp n g f)
  assoc (ℕ.suc n) {0F} {b} {c} {d} {f} {g} {h}                = refl
  assoc (ℕ.suc n) {suc a} {suc b} {suc c} {suc d} {f} {g} {h} = assoc n

  identityˡ : ∀ n {a b : Fin n} {f : Fin (card a b)} → comp n (id n) f ≡ f
  identityˡ (ℕ.suc n) {0F} {b} {0F} = refl
  identityˡ (ℕ.suc n) {suc a} {suc b} {f} = identityˡ n

  identityʳ : ∀ n {a b : Fin n} {f : Fin (card a b)} → comp n f (id n) ≡ f
  identityʳ (ℕ.suc n) {0F} {b} {0F}       = refl
  identityʳ (ℕ.suc n) {suc a} {suc b} {f} = identityʳ n

card-rel : ∀ {n} (x y : Fin n) → card x y ≡ 1 × x ≤ y ⊎ card x y ≡ 0 × y < x
card-rel {ℕ.suc n} 0F y       = inj₁ (refl , z≤n)
card-rel {ℕ.suc n} (suc x) 0F = inj₂ (refl , s≤s z≤n)
card-rel {ℕ.suc n} (suc x) (suc y) with card-rel x y
... | inj₁ (eq , x≤y)         = inj₁ (eq , s≤s x≤y)
... | inj₂ (eq , y<x)         = inj₂ (eq , s≤s y<x)

card-sound₁ : ∀ {n} (x y : Fin n) → card x y ≡ 1 → x ≤ y
card-sound₁ 0F 0F eq           = z≤n
card-sound₁ 0F (suc y) eq      = z≤n
card-sound₁ (suc x) (suc y) eq = s≤s (card-sound₁ x y eq)

card-sound₂ : ∀ {n} (x y : Fin n) → card x y ≡ 0 → y ≤ x
card-sound₂ (suc x) 0F eq      = z≤n
card-sound₂ (suc x) (suc y) eq = s≤s (card-sound₂ x y eq)

card-complete₁ : ∀ {n} {x y : Fin n} → x ≤ y → card x y ≡ 1
card-complete₁ {.(ℕ.suc _)} {0F} {0F} x≤y             = refl
card-complete₁ {.(ℕ.suc _)} {0F} {suc y} x≤y          = refl
card-complete₁ {.(ℕ.suc _)} {suc x} {suc y} (s≤s x≤y) = card-complete₁ x≤y

card-complete₂ : ∀ {n} {x y : Fin n} → y < x → card x y ≡ 0
card-complete₂ {.(ℕ.suc _)} {suc x} {0F} y<x          = refl
card-complete₂ {.(ℕ.suc _)} {suc x} {suc y} (s≤s y<x) = card-complete₂ y<x

module _ (size : ℕ) where

  PosetShape : FinCatShape
  PosetShape = record
    { size     = size
    ; ∣_⇒_∣    = card
    ; hasShape = record
      { id        = id size
      ; _∘_       = comp size
      ; assoc     = assoc size
      ; identityˡ = identityˡ size
      ; identityʳ = identityʳ size
      }
    }

Poset : ℕ → Category _ _ _
Poset size = FinCategory (PosetShape size)

module Poset size = Category (Poset size)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2017-01-05, issue #2376
-- Ensure correct printing for termination error

-- {-# OPTIONS -v term.clause:30 #-}

postulate
  id : ∀{a}{A : Set a} → A → A
  A : Set
  P : A → Set

f : {a : A} → P a → {b : A} → P b → Set
f = λ p → f (id p)  -- id to prevent eta-contration before termination checking

-- Expected termination error:
-- ...
-- Problematic calls:
--   f (id p)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Properties where

open import Prelude hiding (⊥; ⊤)
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Definition
open import Cubical.Foundations.HLevels
open import Data.Empty.UniversePolymorphic
open import HITs.PropositionalTruncation.Sugar
open import HITs.PropositionalTruncation.Properties
open import HITs.PropositionalTruncation
open import Data.Unit.UniversePolymorphic
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Def
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Decidable.Properties
open import Relation.Nullary.Decidable.Logic

private
  variable p : Level

P∃◇ : ∀ {p} {P : A → Type p} → ∀ xs → ◇ P xs → ∥ ∃ P ∥
P∃◇ {A = A} {P = P} = ∥ P∃◇′ ∥⇓
  where
  P∃◇′ : xs ∈𝒦 A ⇒∥ (◇ P xs → ∥ ∃ P ∥) ∥
  ∥ P∃◇′ ∥-prop p q i ◇Pxs = squash (p ◇Pxs) (q ◇Pxs) i
  ∥ P∃◇′ ∥[] ()
  ∥ P∃◇′ ∥ x ∷ xs ⟨ Pxs ⟩ ◇Pxs =
    ◇Pxs >>=
      either′
        (λ Px → ∣ x , Px ∣ )
        (λ ◇Pxxs → Pxs ◇Pxxs)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.NAryOp where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Nat
open import Cubical.Data.Vec

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

private
  variable
    ℓ ℓ' : Level

-- TODO: generalize to different target type?
nAryFunStructure : (n : ℕ) → Type (ℓ-max (ℓ-suc ℓ) (nAryLevel ℓ ℓ n))
nAryFunStructure {ℓ = ℓ} n = TypeWithStr _ (λ (X : Type ℓ) → nAryOp n X X)

-- iso for n-ary functions
nAryFunIso : (n : ℕ) → StrIso (λ (X : Type ℓ) → nAryOp n X X) ℓ
nAryFunIso n (X , fX) (Y , fY) f =
  (xs : Vec X n) → equivFun f (fX $ⁿ xs) ≡ fY $ⁿ map (equivFun f) xs

nAryFunSNS : (n : ℕ) → SNS {ℓ} _ (nAryFunIso n)
nAryFunSNS n = SNS-≡→SNS-PathP (nAryFunIso n) (nAryFunExtEquiv n)

-- Some specializations that are not used at the moment, but kept as
-- they might become useful later.
private

  -- unary
  unaryFunIso : StrIso  (λ (X : Type ℓ) → nAryOp 1 X X) ℓ
  unaryFunIso (A , f) (B , g) e =
    (x : A) → equivFun e (f x) ≡ g (equivFun e x)

  unaryFunSNS : SNS {ℓ} _ unaryFunIso
  unaryFunSNS = SNS-≡→SNS-PathP unaryFunIso (λ s t → compEquiv lem (nAryFunExtEquiv 1 s t))
    where
    lem : ∀ {X} → {s t : X → X} →
            ((x : X) → s x ≡ t x) ≃
            ((xs : Vec X 1) → (s $ⁿ xs) ≡ (t $ⁿ map (λ x → x) xs))
    lem {X} {s} {t} = isoToEquiv f
      where
      f : Iso ((x : X) → s x ≡ t x)
              ((xs : Vec X 1) → (s $ⁿ xs) ≡ (t $ⁿ map (λ x → x) xs))
      Iso.fun f p (x ∷ [])           = p x
      Iso.inv f p x                  = p (x ∷ [])
      Iso.rightInv f p _ xs@(x ∷ []) = p xs
      Iso.leftInv f p _              = p

  -- binary
  binaryFunIso : StrIso  (λ (X : Type ℓ) → nAryOp 2 X X) ℓ
  binaryFunIso (A , f) (B , g) e =
    (x y : A) → equivFun e (f x y) ≡ g (equivFun e x) (equivFun e y)

  binaryFunSNS : SNS {ℓ} _ binaryFunIso
  binaryFunSNS = SNS-≡→SNS-PathP binaryFunIso (λ s t → compEquiv lem (nAryFunExtEquiv 2 s t))
    where
    lem : ∀ {X} → {s t : X → X → X} →
            ((x y : X) → s x y ≡ t x y) ≃
            ((xs : Vec X 2) → (s $ⁿ xs) ≡ (t $ⁿ map (λ x → x) xs))
    lem {X} {s} {t} = isoToEquiv f
      where
      f : Iso ((x y : X) → s x y ≡ t x y)
              ((xs : Vec X 2) → (s $ⁿ xs) ≡ (t $ⁿ map (λ x → x) xs))
      Iso.fun f p (x ∷ y ∷ [])           = p x y
      Iso.inv f p x y                    = p (x ∷ y ∷ [])
      Iso.rightInv f p _ xs@(x ∷ y ∷ []) = p xs
      Iso.leftInv f p _                  = p