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

module Fragment.Examples.CSemigroup.Arith.Functions where

open import Fragment.Examples.CSemigroup.Arith.Base

-- Fully dynamic associativity

+-dyn-assoc₁ : ∀ {f : ℕ → ℕ} {m n o} → (f m + n) + o ≡ f m + (n + o)
+-dyn-assoc₁ = fragment CSemigroupFrex +-csemigroup

+-dyn-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → ((f m + n) + o) + g p ≡ f m + (n + (o + g p))
+-dyn-assoc₂ = fragment CSemigroupFrex +-csemigroup

+-dyn-assoc₃ : ∀ {f g h : ℕ → ℕ} {m n o p q} → (f m + n) + g o + (p + h q) ≡ f m + (n + g o + p) + h q
+-dyn-assoc₃ = fragment CSemigroupFrex +-csemigroup

*-dyn-assoc₁ : ∀ {f : ℕ → ℕ} {m n o} → (f m * n) * o ≡ f m * (n * o)
*-dyn-assoc₁ = fragment CSemigroupFrex *-csemigroup

*-dyn-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → ((f m * n) * o) * g p ≡ f m * (n * (o * g p))
*-dyn-assoc₂ = fragment CSemigroupFrex *-csemigroup

*-dyn-assoc₃ : ∀ {f g h : ℕ → ℕ} {m n o p q} → (f m * n) * g o * (p * h q) ≡ f m * (n * g o * p) * h q
*-dyn-assoc₃ = fragment CSemigroupFrex *-csemigroup

-- Fully dynamic commutativity

+-dyn-comm₁ : ∀ {f : ℕ → ℕ} {m} → f m + m ≡ m + f m
+-dyn-comm₁ = fragment CSemigroupFrex +-csemigroup

+-dyn-comm₂ : ∀ {f g : ℕ → ℕ} {m n o} → f m + (n + g o) ≡ (g o + n) + f m
+-dyn-comm₂ = fragment CSemigroupFrex +-csemigroup

+-dyn-comm₃ : ∀ {f g h : ℕ → ℕ} {m n o p} → (f m + g n) + (h o + p) ≡ (p + h o) + (g n + f m)
+-dyn-comm₃ = fragment CSemigroupFrex +-csemigroup

*-dyn-comm₁ : ∀ {f : ℕ → ℕ} {m} → f m * m ≡ m * f m
*-dyn-comm₁ = fragment CSemigroupFrex *-csemigroup

*-dyn-comm₂ : ∀ {f g : ℕ → ℕ} {m n o} → f m * (n * g o) ≡ (g o * n) * f m
*-dyn-comm₂ = fragment CSemigroupFrex *-csemigroup

*-dyn-comm₃ : ∀ {f g h : ℕ → ℕ} {m n o p} → (f m * g n) * (h o * p) ≡ (p * h o) * (g n * f m)
*-dyn-comm₃ = fragment CSemigroupFrex *-csemigroup

-- Fully dynamic associavity and commutativity

+-dyn-comm-assoc₁ : ∀ {f : ℕ → ℕ} {m} → (f m + f (f m)) + f (f (f m)) ≡ f (f (f m)) + (f (f m) + f m)
+-dyn-comm-assoc₁ = fragment CSemigroupFrex +-csemigroup

+-dyn-comm-assoc₂ : ∀ {f g : ℕ → ℕ} {m n} → ((f m + f n) + g m) + g n ≡ g m + (f n + (g n + f m))
+-dyn-comm-assoc₂ = fragment CSemigroupFrex +-csemigroup

+-dyn-comm-assoc₃ : ∀ {f : ℕ → ℕ} {m n o p q} → f (m + n) + o + (p + q) ≡ f (m + n) + q + (p + o)
+-dyn-comm-assoc₃ = fragment CSemigroupFrex +-csemigroup

*-dyn-comm-assoc₁ : ∀ {f : ℕ → ℕ} {m} → (f m * f (f m)) * f (f (f m)) ≡ f (f (f m)) * (f (f m) * f m)
*-dyn-comm-assoc₁ = fragment CSemigroupFrex *-csemigroup

*-dyn-comm-assoc₂ : ∀ {f g : ℕ → ℕ} {m n} → ((f m * f n) * g m) * g n ≡ g m * (f n * (g n * f m))
*-dyn-comm-assoc₂ = fragment CSemigroupFrex *-csemigroup

*-dyn-comm-assoc₃ : ∀ {f : ℕ → ℕ} {m n o p q} → f (m + n) * o * (p * q) ≡ f (m + n) * q * (p * o)
*-dyn-comm-assoc₃ = fragment CSemigroupFrex *-csemigroup

-- Partially static associativity

+-sta-assoc₁ : ∀ {f : ℕ → ℕ} {m} → (m + 2) + (3 + f 0) ≡ m + (5 + f 0)
+-sta-assoc₁ = fragment CSemigroupFrex +-csemigroup

+-sta-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → (((f m + g n) + 5) + o) + p ≡ f m + (g n + (2 + (3 + (o + p))))
+-sta-assoc₂ = fragment CSemigroupFrex +-csemigroup

+-sta-assoc₃ : ∀ {f : ℕ → ℕ} {m n o p} → f (n + m) + (n + 2) + (3 + (o + p)) ≡ (((n + 1) + (4 + o)) + p) + f (n + m)
+-sta-assoc₃ = fragment CSemigroupFrex +-csemigroup

*-sta-assoc₁ : ∀ {f : ℕ → ℕ} {m} → (m * 2) * (3 * f 0) ≡ m * (6 * f 0)
*-sta-assoc₁ = fragment CSemigroupFrex *-csemigroup

*-sta-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → (((f m * g n) * 6) * o) * p ≡ f m * (g n * (2 * (3 * (o * p))))
*-sta-assoc₂ = fragment CSemigroupFrex *-csemigroup

*-sta-assoc₃ : ∀ {f : ℕ → ℕ} {m n o p} → f (n + m) * (n * 4) * (3 * (o * p)) ≡ (((n * 2) * (6 * o)) * p) * f (n + m)
*-sta-assoc₃ = fragment CSemigroupFrex *-csemigroup

-- Partially static commutativity

+-sta-comm₁ : ∀ {f g : ℕ → ℕ} {m} → f m + g 1 ≡ g 1 + f m
+-sta-comm₁ = fragment CSemigroupFrex +-csemigroup

+-sta-comm₂ : ∀ {f g : ℕ → ℕ} {m n} → f m + (2 + g n) ≡ (g n + 2) + f m
+-sta-comm₂ = fragment CSemigroupFrex +-csemigroup

+-sta-comm₃ : ∀ {f g h : ℕ → ℕ} {m n o p} → (1 + (f m + g n)) + ((o + p) + h 2) ≡ ((p + o) + h 2) + (1 + (g n + f m))
+-sta-comm₃ = fragment CSemigroupFrex +-csemigroup

*-sta-comm₁ : ∀ {f g : ℕ → ℕ} {m} → f m * g 1 ≡ g 1 * f m
*-sta-comm₁ = fragment CSemigroupFrex *-csemigroup

*-sta-comm₂ : ∀ {f g : ℕ → ℕ} {m n} → f m * (2 * g n) ≡ (g n * 2) * f m
*-sta-comm₂ = fragment CSemigroupFrex *-csemigroup

*-sta-comm₃ : ∀ {f g h : ℕ → ℕ} {m n o p} → (3 * (f m * g n)) * ((o * p) * h 2) ≡ ((p * o) * h 2) * (3 * (g n * f m))
*-sta-comm₃ = fragment CSemigroupFrex *-csemigroup

-- Partially static associavity and commutativity

+-sta-comm-assoc₁ : ∀ {f : ℕ → ℕ} {m n o} → 1 + (f m + n) + f o + 4 ≡ 5 + n + (f m + f o)
+-sta-comm-assoc₁ = fragment CSemigroupFrex +-csemigroup

+-sta-comm-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → 5 + ((f m + n) + o) + g p ≡ g p + ((o + 1) + (n + f m)) + 4
+-sta-comm-assoc₂ = fragment CSemigroupFrex +-csemigroup

+-sta-comm-assoc₃ : ∀ {f g h : ℕ → ℕ} {m n o p q} → (f m + g n + 1) + o + (p + h q + 4) ≡ (2 + h q) + (p + o + g n) + (f m + 3)
+-sta-comm-assoc₃ = fragment CSemigroupFrex +-csemigroup

*-sta-comm-assoc₁ : ∀ {f : ℕ → ℕ} {m n o} → 2 * (f m * n) * f o * 6 ≡ 12 * n * (f m * f o)
*-sta-comm-assoc₁ = fragment CSemigroupFrex *-csemigroup

*-sta-comm-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → 12 * ((f m * n) * o) * g p ≡ g p * ((o * 2) * (n * f m)) * 6
*-sta-comm-assoc₂ = fragment CSemigroupFrex *-csemigroup

*-sta-comm-assoc₃ : ∀ {f g h : ℕ → ℕ} {m n o p q} → (f m * g n * 2) * o * (p * h q * 6) ≡ (4 * h q) * (p * o * g n) * (f m * 3)
*-sta-comm-assoc₃ = fragment CSemigroupFrex *-csemigroup


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

syntax QIO

type
  T : 0-ary
  P : 0-ary

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

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

module QIO.Equality where

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

open import QIO.Signature
open import QIO.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution QIO:Syn
open import SOAS.Metatheory.SecondOrder.Equality QIO:Syn

private
  variable
    α β γ τ : QIOT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ QIO) α Γ → (𝔐 ▷ QIO) α Γ → Set where
  A : ⁅ P ⁆ ⁅ T ⁆ ⁅ T ⁆̣               ▹ ∅ ⊢                             applyX 𝔞 (measure x₀ 𝔟 𝔠) ≋ₐ measure 𝔞 𝔠 𝔟
  B : ⁅ P ⁆ ⁅ P ⁆ ⁅ P ⊩ T ⁆ ⁅ P ⊩ T ⁆̣ ▹ ∅ ⊢ measure 𝔞 (applyDu 𝔟 (𝔠⟨ x₀ ⟩)) (applyDv 𝔟 (𝔡⟨ x₀ ⟩)) ≋ₐ applyDuv 𝔞 𝔟 (measure x₀ (𝔠⟨ x₁ ⟩) (𝔡⟨ x₁ ⟩))
  D : ⁅ T ⁆ ⁅ T ⁆̣                     ▹ ∅ ⊢                                  new (measure x₀ 𝔞 𝔟) ≋ₐ 𝔞
  E : ⁅ P ⁆ ⁅ P · P ⊩ T ⁆̣             ▹ ∅ ⊢                    new (applyDuv x₀ 𝔞 (𝔟⟨ x₀ ◂ x₁ ⟩)) ≋ₐ applyDu 𝔞 (new (𝔟⟨ x₀ ◂ x₁ ⟩))

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

ext: agda


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

open import HoTT
import homotopy.ConstantToSetExtendsToProp as ConstExt

module homotopy.RelativelyConstantToSetExtendsViaSurjection
  {i j k} {A : Type i} {B : Type j} {C : B → Type k}
  (C-is-set : ∀ b → is-set (C b))
  (f : A → B) (f-is-surj : is-surj f)
  (g : (a : A) → C (f a))
  (g-is-const : ∀ a₁ a₂ → (p : f a₁ == f a₂) → g a₁ == g a₂ [ C ↓ p ])
  where

{-
  (b : A) ----> [ hfiber f b ] ----?----> C ?
                      ^
                      |
                  hfiber f b
-}

  private
    lemma : ∀ b → hfiber f b → C b
    lemma b (a , fa=b) = transport C fa=b (g a)

    lemma-const : ∀ b → (h₁ h₂ : hfiber f b) → lemma b h₁ == lemma b h₂
    lemma-const ._ (a₁ , fa₁=fa₂) (a₂ , idp) =
      to-transp (g-is-const a₁ a₂ fa₁=fa₂)

    module CE (b : B) =
      ConstExt {A = hfiber f b} {B = C b}
        (C-is-set b) (lemma b) (lemma-const b)

  ext : Π B C
  ext b = CE.ext b (f-is-surj b)

  β : (a : A) → ext (f a) == g a
  β a = ap (CE.ext (f a))
    (prop-has-all-paths Trunc-level (f-is-surj (f a)) [ a , idp ])

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import Cubical.HITs.Ints.IsoInt.Base public

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:
------------------------------------------------------------------------------
-- Testing an alternative definition of subtraction
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.SubtractionSL where

open import Data.Nat hiding ( _∸_ )
open import Relation.Binary.PropositionalEquality

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Data/Nat.agda).
infixl 9 _∸₁_ _∸₂_

-- First definition (from the Agda standard library 0.8.1).
_∸₁_ : ℕ → ℕ → ℕ
m     ∸₁ zero  = m
zero  ∸₁ suc n = zero
suc m ∸₁ suc n = m ∸₁ n

-- Second definition.
_∸₂_ : ℕ → ℕ → ℕ
m     ∸₂ zero  = m
{-# CATCHALL #-}
zero  ∸₂ n     = zero
suc m ∸₂ suc n = m ∸₂ n

-- Both definitions are equivalents.
thm : ∀ m n → m ∸₁ n ≡ m ∸₂ n
thm m       zero    = refl
thm zero    (suc n) = refl
thm (suc m) (suc n) = thm m n

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Issue2579.Import where

record Wrap A : Set where
  constructor wrap
  field wrapped : A

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
{-# OPTIONS --show-implicit #-}

module PragmasRespected where

postulate
  Foo : {A : Set₁} → Set
  Bar : Foo {A = Set}

-- Andreas, 2014-10-20, AIM XX:
-- This test used to check that the --show-implicit option
-- is turned on even if the module is just reloaded from
-- an interface file.
-- However, as we now always recheck when reload,
-- this test should now trivially succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------------
-- Totality of Boolean conjunction
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Bool.AndTotality where

open import FOTC.Base
open import FOTC.Data.Bool.Type

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

postulate thm : (A : D → Set) → ∀ {b} → (Bool b ∧ A true ∧ A false) → A b
-- Because the ATPs don't handle induction, them cannot prove the
-- induction principle for Bool.
-- {-# ATP prove thm #-}

postulate
  thm₁ : {A : D → Set} → ∀ {x y z} → Bool x → A y → A z → A (if x then y else z)
-- Because the ATPs don't handle induction, them cannot prove this postulate.
-- {-# ATP prove thm₁ #-}

-- Typing of the if-then-else.
if-T : (A : D → Set) → ∀ {x y z} → Bool x → A y → A z →
       A (if x then y else z)
if-T A {y = y} btrue  Ay Az = subst A (sym (if-true y)) Ay
if-T A {z = z} bfalse Ay Az = subst A (sym (if-false z)) Az

_&&_ : D → D → D
x && y = if x then y else false
{-# ATP definition _&&_ #-}

postulate &&-Bool : ∀ {x y} → Bool x → Bool y → Bool (x && y)
{-# ATP prove &&-Bool if-T #-}

&&-Bool₁ : ∀ {x y} → Bool x → Bool y → Bool (x && y)
&&-Bool₁ {y = y} btrue By = prf
  where
    postulate prf : Bool (true && y)
    {-# ATP prove prf if-T #-}
&&-Bool₁ {y = y} bfalse By = prf
  where
    postulate prf : Bool (false && y)
    {-# ATP prove prf if-T #-}

&&-Bool₂ : ∀ {x y} → Bool x → Bool y → Bool (x && y)
&&-Bool₂ btrue  By = if-T Bool btrue By bfalse
&&-Bool₂ bfalse By = if-T Bool bfalse By bfalse


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

module 16-sets where

import 15-groups
open 15-groups public

{- Equivalence relations -}

Rel-Prop :
  (l : Level) {l1 : Level} (A : UU l1) → UU ((lsuc l) ⊔ l1)
Rel-Prop l A = A → (A → UU-Prop l)

type-Rel-Prop :
  {l1 l2 : Level} {A : UU l1} (R : Rel-Prop l2 A) → A → A → UU l2
type-Rel-Prop R x y = pr1 (R x y)

is-prop-type-Rel-Prop :
  {l1 l2 : Level} {A : UU l1} (R : Rel-Prop l2 A) →
  (x y : A) → is-prop (type-Rel-Prop R x y)
is-prop-type-Rel-Prop R x y = pr2 (R x y)

is-reflexive-Rel-Prop :
  {l1 l2 : Level} {A : UU l1} → Rel-Prop l2 A → UU (l1 ⊔ l2)
is-reflexive-Rel-Prop {A = A} R =
  (x : A) → type-Rel-Prop R x x

is-symmetric-Rel-Prop :
  {l1 l2 : Level} {A : UU l1} → Rel-Prop l2 A → UU (l1 ⊔ l2)
is-symmetric-Rel-Prop {A = A} R =
  (x y : A) → type-Rel-Prop R x y → type-Rel-Prop R y x

is-transitive-Rel-Prop :
  {l1 l2 : Level} {A : UU l1} → Rel-Prop l2 A → UU (l1 ⊔ l2)
is-transitive-Rel-Prop {A = A} R =
  (x y z : A) → type-Rel-Prop R x y → type-Rel-Prop R y z → type-Rel-Prop R x z

is-equivalence-relation :
  {l1 l2 : Level} {A : UU l1} (R : Rel-Prop l2 A) → UU (l1 ⊔ l2)
is-equivalence-relation R =
  is-reflexive-Rel-Prop R ×
    ( is-symmetric-Rel-Prop R × is-transitive-Rel-Prop R)

Eq-Rel :
  (l : Level) {l1 : Level} (A : UU l1) → UU ((lsuc l) ⊔ l1)
Eq-Rel l A = Σ (Rel-Prop l A) is-equivalence-relation

rel-prop-Eq-Rel :
  {l1 l2 : Level} {A : UU l1} → Eq-Rel l2 A → Rel-Prop l2 A
rel-prop-Eq-Rel = pr1

type-Eq-Rel :
  {l1 l2 : Level} {A : UU l1} → Eq-Rel l2 A → A → A → UU l2
type-Eq-Rel R = type-Rel-Prop (rel-prop-Eq-Rel R)

is-equivalence-relation-rel-prop-Eq-Rel :
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A) →
  is-equivalence-relation (rel-prop-Eq-Rel R)
is-equivalence-relation-rel-prop-Eq-Rel R = pr2 R

refl-Eq-Rel :
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A) →
  is-reflexive-Rel-Prop (rel-prop-Eq-Rel R)
refl-Eq-Rel R = pr1 (is-equivalence-relation-rel-prop-Eq-Rel R)

symm-Eq-Rel :
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A) →
  is-symmetric-Rel-Prop (rel-prop-Eq-Rel R)
symm-Eq-Rel R = pr1 (pr2 (is-equivalence-relation-rel-prop-Eq-Rel R))

trans-Eq-Rel :
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A) →
  is-transitive-Rel-Prop (rel-prop-Eq-Rel R)
trans-Eq-Rel R = pr2 (pr2 (is-equivalence-relation-rel-prop-Eq-Rel R))

{- Section 15.2 The universal property of set quotients -}

identifies-Eq-Rel :
  {l1 l2 l3 : Level} {A : UU l1} (R : Eq-Rel l2 A) →
  {B : UU l3} → (A → B) → UU (l1 ⊔ (l2 ⊔ l3))
identifies-Eq-Rel {A = A} R f =
  (x y : A) → type-Eq-Rel R x y → Id (f x) (f y)

precomp-map-universal-property-Eq-Rel :
  {l l1 l2 l3 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  {B : UU-Set l3} (f : A → type-Set B) (H : identifies-Eq-Rel R f) →
  (X : UU-Set l) → (type-hom-Set B X) → Σ (A → type-Set X) (identifies-Eq-Rel R)
precomp-map-universal-property-Eq-Rel R f H X g =
  pair (g ∘ f) (λ x y r → ap g (H x y r))

universal-property-set-quotient :
  (l : Level) {l1 l2 l3 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  {B : UU-Set l3} (f : A → type-Set B) (H : identifies-Eq-Rel R f) → UU _
universal-property-set-quotient l R {B} f H =
  (X : UU-Set l) → is-equiv (precomp-map-universal-property-Eq-Rel R {B} f H X)

{- Effective quotients -}

is-effective-Set-Quotient :
  {l1 l2 l3 : Level} {A : UU l1} (R : Eq-Rel l2 A) (B : UU-Set l3)
  (f : A → type-Set B) (H : identifies-Eq-Rel R f) → UU (l1 ⊔ l2 ⊔ l3)
is-effective-Set-Quotient {A = A} R B f H = (x y : A) → is-equiv (H x y)

-- Section 13.4

is-small :
  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
is-small l A = Σ (UU l) (λ X → A ≃ X)

is-small-map :
  (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  (A → B) → UU (lsuc l ⊔ (l1 ⊔ l2))
is-small-map l {B = B} f = (b : B) → is-small l (fib f b)

is-locally-small :
  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
is-locally-small l A = (x y : A) → is-small l (Id x y)

total-subtype :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) → UU (l1 ⊔ l2)
total-subtype {A = A} P = Σ A (λ x → pr1 (P x))

equiv-subtype-equiv :
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} (e : A ≃ B)
  (C : A → UU-Prop l3) (D : B → UU-Prop l4) →
  ((x : A) → (C x) ↔ (D (map-equiv e x))) →
  total-subtype C ≃ total-subtype D
equiv-subtype-equiv e C D H =
  equiv-toto (λ y → type-Prop (D y)) e
    ( λ x → equiv-iff (C x) (D (map-equiv e x)) (H x))

equiv-comp-equiv' :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} →
  (A ≃ B) → (C : UU l3) → (B ≃ C) ≃ (A ≃ C)
equiv-comp-equiv' e C =
  equiv-subtype-equiv
    ( equiv-precomp-equiv e C)
    ( is-equiv-Prop)
    ( is-equiv-Prop)
    ( λ g →
      pair
        ( is-equiv-comp' g (map-equiv e) (is-equiv-map-equiv e))
        ( λ is-equiv-eg →
          is-equiv-left-factor'
            g (map-equiv e) is-equiv-eg (is-equiv-map-equiv e)))

is-prop-is-small :
  (l : Level) {l1 : Level} (A : UU l1) → is-prop (is-small l A)
is-prop-is-small l A =
  is-prop-is-contr-if-inh
    ( λ Xe →
      is-contr-equiv'
        ( Σ (UU l) (λ Y → (pr1 Xe) ≃ Y))
        ( equiv-tot ((λ Y → equiv-comp-equiv' (pr2 Xe) Y)))
        ( is-contr-total-equiv (pr1 Xe)))

is-prop-is-locally-small :
  (l : Level) {l1 : Level} (A : UU l1) → is-prop (is-locally-small l A)
is-prop-is-locally-small l A =
  is-prop-Π (λ x → is-prop-Π (λ y → is-prop-is-small l (Id x y)))

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue311 where

open import Common.Level

postulate
  A : Set
  C : (b : Level) (B : A → Set b) → Set b
  f : (b : Level) (B : A → Set b) → C b B → A
  g : (b : Level) (B : A → Set b) (d : C b B) → B (f b B d)
  P : (c : Level) → Set c
  Q : A → Set
  checkQ : ∀ a → Q a → Set

T : (c : Level) → Set c
T c = P c → A

Foo : (c : Level) (d : C c (λ _ → T c)) →
      Q (f c (λ _ → T c) d) → Set
Foo c d q with f c (λ _ → T c) d | g c (λ _ → T c) d
Foo c d q | x | y  = checkQ x q

-- C-c C-, gives:
--
-- Goal: Set₁
-- ————————————————————————————————————————————————————————————
-- q : Q (f c (λ _ → P c → A) d)
-- y : P c → A
-- x : A
-- d : C c (λ _ → P c → A)
-- c : Level
--
-- Note that q has type Q (f c (λ _ → P c → A) d); it should have type
-- Q x.

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
{-
  This uses ideas from Floris van Doorn's phd thesis and the code in
  https://github.com/cmu-phil/Spectral/blob/master/spectrum/basic.hlean
-}
module Cubical.Homotopy.Spectrum where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Unit.Pointed
open import Cubical.Foundations.Equiv

open import Cubical.Data.Int

open import Cubical.Homotopy.Prespectrum

private
  variable
    ℓ : Level

Spectrum : (ℓ : Level) → Type (ℓ-suc ℓ)
Spectrum ℓ = let open GenericPrespectrum
             in Σ[ P ∈ Prespectrum ℓ ] ((k : ℤ) → isEquiv (fst (map P k)))

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------
-- Example: Left recursive expression grammar
------------------------------------------------------------------------

module TotalParserCombinators.Recogniser.Expression where

open import Codata.Musical.Notation
open import Data.Bool
open import Data.Char as Char using (Char)
open import Data.List
open import Data.String as String using (String)
open import Function
open import Relation.Binary.PropositionalEquality

open import TotalParserCombinators.BreadthFirst
import TotalParserCombinators.Lib as Lib
open import TotalParserCombinators.Recogniser

------------------------------------------------------------------------
-- Lifted versions of some parsers

-- Specific tokens.

tok : Char → P Char []
tok c = lift $ Lib.Token.tok Char Char._≟_ c

-- Numbers.

number : P Char []
number = lift Lib.number

------------------------------------------------------------------------
-- An expression grammar

-- t ∷= t '+' f ∣ f
-- f ∷= f '*' a ∣ a
-- a ∷= '(' t ')' ∣ n

mutual

  term   = ♯ term · tok '+' · factor
         ∣ factor

  factor = ♯ factor · tok '*' · atom
         ∣ atom

  atom   = tok '(' · ♯ term · tok ')'
         ∣ number

------------------------------------------------------------------------
-- Unit tests

module Tests where

  test : ∀ {n} → P Char n → String → Bool
  test p s = not $ null $ parse ⟦ p ⟧ (String.toList s)

  ex₁ : test term "1*(2+3)" ≡ true
  ex₁ = refl

  ex₂ : test term "1*(2+3" ≡ false
  ex₂ = refl

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the binary representation of natural numbers
------------------------------------------------------------------------

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

module Data.Bin.Properties where

open import Data.Bin
open import Data.Digit using (Bit; Expansion)
import Data.Fin as Fin
import Data.Fin.Properties as 𝔽ₚ
open import Data.List.Base using (List; []; _∷_)
open import Data.List.Properties using (∷-injective)
open import Data.Nat
  using (ℕ; zero; z≤n; s≤s)
  renaming (suc to 1+_; _+_ to _+ℕ_; _*_ to _*ℕ_; _≤_ to _≤ℕ_)
import Data.Nat.Properties as ℕₚ
open import Data.Product using (proj₁; proj₂)
open import Function using (_∘_)
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; sym; isEquivalence; resp₂; decSetoid)
open import Relation.Nullary using (yes; no)

------------------------------------------------------------------------
-- (Bin, _≡_) is a decidable setoid

1#-injective : ∀ {as bs} → as 1# ≡ bs 1# → as ≡ bs
1#-injective refl = refl

infix 4 _≟_ _≟ₑ_

_≟ₑ_ : ∀ {base} → Decidable (_≡_ {A = Expansion base})
_≟ₑ_ []       []       = yes refl
_≟ₑ_ []       (_ ∷ _)  = no λ()
_≟ₑ_ (_ ∷ _) []        = no λ()
_≟ₑ_ (x ∷ xs) (y ∷ ys) with x Fin.≟ y | xs ≟ₑ ys
... | _        | no xs≢ys = no (xs≢ys ∘ proj₂ ∘ ∷-injective)
... | no  x≢y  | _        = no (x≢y   ∘ proj₁ ∘ ∷-injective)
... | yes refl | yes refl = yes refl

_≟_ : Decidable {A = Bin} _≡_
0#    ≟ 0#    = yes refl
0#    ≟ bs 1# = no λ()
as 1# ≟ 0#    = no λ()
as 1# ≟ bs 1# with as ≟ₑ bs
... | yes refl  = yes refl
... | no  as≢bs = no (as≢bs ∘ 1#-injective)

≡-isDecEquivalence : IsDecEquivalence _≡_
≡-isDecEquivalence = record
  { isEquivalence = isEquivalence
  ; _≟_           = _≟_
  }

≡-decSetoid : DecSetoid _ _
≡-decSetoid = decSetoid _≟_

------------------------------------------------------------------------
-- (Bin _≡_ _<_) is a strict total order

<-trans : Transitive _<_
<-trans (less lt₁) (less lt₂) = less (ℕₚ.<-trans lt₁ lt₂)

<-asym : Asymmetric _<_
<-asym (less lt) (less gt) = ℕₚ.<-asym lt gt

<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl (less lt) = ℕₚ.<-irrefl refl lt

∷ʳ-mono-< : ∀ {a b as bs} → as 1# < bs 1# → (a ∷ as) 1# < (b ∷ bs) 1#
∷ʳ-mono-< {a} {b} {as} {bs} (less lt) = less (begin
  1+ (m₁ +ℕ n₁ *ℕ 2) ≤⟨ s≤s (ℕₚ.+-monoˡ-≤ _ (𝔽ₚ.toℕ≤pred[n] a)) ⟩
  1+ (1 +ℕ n₁ *ℕ 2)  ≡⟨ refl ⟩
  1+ n₁ *ℕ 2         ≤⟨ ℕₚ.*-mono-≤ lt ℕₚ.≤-refl ⟩
  n₂ *ℕ 2            ≤⟨ ℕₚ.n≤m+n m₂ (n₂ *ℕ 2) ⟩
  m₂ +ℕ n₂ *ℕ 2      ∎)
  where
  open ℕₚ.≤-Reasoning
  m₁ = Fin.toℕ a;   m₂ = Fin.toℕ b
  n₁ = toℕ (as 1#); n₂ = toℕ (bs 1#)

∷ˡ-mono-< : ∀ {a b bs} → a Fin.< b → (a ∷ bs) 1# < (b ∷ bs) 1#
∷ˡ-mono-< {a} {b} {bs} lt = less (begin
  1 +ℕ (m₁  +ℕ n *ℕ 2)  ≡⟨ sym (ℕₚ.+-assoc 1 m₁ (n *ℕ 2)) ⟩
  (1 +ℕ m₁) +ℕ n *ℕ 2   ≤⟨ ℕₚ.+-monoˡ-≤ _ lt ⟩
  m₂  +ℕ n *ℕ 2   ∎)
  where
  open ℕₚ.≤-Reasoning
  m₁ = Fin.toℕ a; m₂ = Fin.toℕ b; n = toℕ (bs 1#)

1<[23] : ∀ {b} → [] 1# < (b ∷ []) 1#
1<[23] {b} = less (ℕₚ.n≤m+n (Fin.toℕ b) 2)

1<2+ : ∀ {b bs} → [] 1# < (b ∷ bs) 1#
1<2+ {_} {[]}     = 1<[23]
1<2+ {_} {b ∷ bs} = <-trans 1<[23] (∷ʳ-mono-< {a = b} 1<2+)

0<1+ : ∀ {bs} → 0# < bs 1#
0<1+ {[]}     = less (s≤s z≤n)
0<1+ {b ∷ bs} = <-trans (less (s≤s z≤n)) 1<2+

<⇒≢ : ∀ {a b} → a < b → a ≢ b
<⇒≢ lt eq = asym⟶irr (resp₂ _<_) sym <-asym eq lt

<-cmp : Trichotomous _≡_ _<_
<-cmp 0#            0#            = tri≈ (<-irrefl refl) refl (<-irrefl refl)
<-cmp 0#            (_ 1#)        = tri< 0<1+ (<⇒≢ 0<1+) (<-asym 0<1+)
<-cmp (_ 1#)        0#            = tri> (<-asym 0<1+) (<⇒≢ 0<1+ ∘ sym) 0<1+
<-cmp ([] 1#)       ([] 1#)       = tri≈ (<-irrefl refl) refl (<-irrefl refl)
<-cmp ([] 1#)       ((b ∷ bs) 1#) = tri< 1<2+ (<⇒≢ 1<2+) (<-asym 1<2+)
<-cmp ((a ∷ as) 1#) ([] 1#)       = tri> (<-asym 1<2+) (<⇒≢ 1<2+ ∘ sym) 1<2+
<-cmp ((a ∷ as) 1#) ((b ∷ bs) 1#) with <-cmp (as 1#) (bs 1#)
... | tri<  lt ¬eq ¬gt =
  tri< (∷ʳ-mono-< lt)  (<⇒≢ (∷ʳ-mono-< lt)) (<-asym (∷ʳ-mono-< lt))
... | tri> ¬lt ¬eq  gt =
  tri> (<-asym (∷ʳ-mono-< gt)) (<⇒≢ (∷ʳ-mono-< gt) ∘ sym) (∷ʳ-mono-< gt)
... | tri≈ ¬lt refl ¬gt with 𝔽ₚ.<-cmp a b
...   | tri≈ ¬lt′ refl ¬gt′ =
  tri≈ (<-irrefl refl) refl (<-irrefl refl)
...   | tri<  lt′ ¬eq  ¬gt′ =
  tri< (∷ˡ-mono-< lt′)  (<⇒≢ (∷ˡ-mono-< lt′)) (<-asym (∷ˡ-mono-< lt′))
...   | tri> ¬lt′ ¬eq  gt′  =
  tri> (<-asym (∷ˡ-mono-< gt′)) (<⇒≢ (∷ˡ-mono-< gt′) ∘ sym) (∷ˡ-mono-< gt′)

<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
  { isEquivalence = isEquivalence
  ; trans         = <-trans
  ; compare       = <-cmp
  }

<-strictTotalOrder : StrictTotalOrder _ _ _
<-strictTotalOrder = record
  { Carrier            = Bin
  ; _≈_                = _≡_
  ; _<_                = _<_
  ; isStrictTotalOrder = <-isStrictTotalOrder
  }


text:
open import Prelude
open import Nat
open import List
open import Bij

module delta-lemmas (K : Set) {{bij : bij K Nat}} where

  -- abbreviations for conversion between K and Nat
  key : Nat → K
  key = convert-inv {{bij}}

  nat : K → Nat
  nat = bij.convert bij

  -- another bij-related convenience functions
  inj-cp : ∀{k1 k2} → k1 ≠ k2 → nat k1 ≠ nat k2
  inj-cp ne eq = abort (ne (bij.inj bij eq))

  -- helper function
  delta : ∀{n m} → n < m → Nat
  delta n<m = difference (n<m→1+n≤m n<m)

  -- raw underlying list-of-pairs type
  dl : (V : Set) → Set
  dl V = List (Nat ∧ V)

  ---- helper definitions ----

  _lkup_ : {V : Set} → dl V → Nat → Maybe V
  [] lkup x = None
  ((hn , hv) :: t) lkup n with <dec n hn
  ... | Inl n<hn       = None
  ... | Inr (Inl refl) = Some hv
  ... | Inr (Inr hn<n) = t lkup (delta hn<n)

  _,,'_ : ∀{V} → dl V → (Nat ∧ V) → dl V
  [] ,,' (n , v) = (n , v) :: []
  ((hn , hv) :: t) ,,' (n , v) with <dec n hn
  ... | Inl n<hn       = (n , v) :: ((delta n<hn , hv) :: t)
  ... | Inr (Inl refl) = (n , v) :: t
  ... | Inr (Inr hn<n) = (hn , hv) :: (t ,,' (delta hn<n , v))

  data _∈'_ : {V : Set} (p : Nat ∧ V) → (d : dl V) → Set where
    InH : {V : Set} {d : dl V} {n : Nat} {v : V} →
      (n , v) ∈' ((n , v) :: d)
    InT : {V : Set} {d : dl V} {n s : Nat} {v v' : V} →
      (n , v) ∈' d →
      (n + 1+ s , v) ∈' ((s , v') :: d)

  dom' : {V : Set} → dl V → Nat → Set
  dom' {V} d n = Σ[ v ∈ V ] ((n , v) ∈' d)

  _#'_ : {V : Set} (n : Nat) → (d : dl V) → Set
  n #' d = dom' d n → ⊥

  ---- lemmas ----

  undelta : (x s : Nat) → (x<s+1+x : x < s + 1+ x) → s == delta x<s+1+x
  undelta x s x<s+1+x
    rewrite n+1+m==1+n+m {s} {x} | ! (m-n==1+m-1+n n≤m+n (n<m→1+n≤m x<s+1+x)) | +comm {s} {x}
      = ! (n+m-n==m n≤n+m)

  n#'[] : {V : Set} {n : Nat} → _#'_ {V} n []
  n#'[] (_ , ())

  too-small : {V : Set} {d : dl V} {xl xb : Nat} {v : V} →
               xl < xb →
               dom' ((xb , v) :: d) xl →
               ⊥
  too-small (_ , ne) (_ , InH) = ne refl
  too-small (x+1+xb≤xb , x+1+xb==xb) (_ , InT _) =
    x+1+xb==xb (≤antisym x+1+xb≤xb (≤trans (≤1+ ≤refl) n≤m+n))

  all-not-none : {V : Set} {d : dl V} {x : Nat} {v : V} →
                  None ≠ (((x , v) :: d) lkup x)
  all-not-none {x = x} rewrite <dec-refl x = λ ()

  all-bindings-==-rec-eq : {V : Set} {d1 d2 : dl V} {x : Nat} {v : V} →
                            ((x' : Nat) → ((x , v) :: d1) lkup x' == ((x , v) :: d2) lkup x') →
                            ((x' : Nat) → d1 lkup x' == d2 lkup x')
  all-bindings-==-rec-eq {x = x} h x'
    with h (x' + 1+ x)
  ... | eq
    with <dec (x' + 1+ x) x
  ... | Inl x'+1+x<x
          = abort (<antisym x'+1+x<x (n<m→n<s+m n<1+n))
  ... | Inr (Inl x'+1+x==x)
          = abort ((flip n≠n+1+m) (n+1+m==1+n+m · (+comm {1+ x} · x'+1+x==x)))
  ... | Inr (Inr x<x'+1+x)
          rewrite ! (undelta x x' x<x'+1+x) = eq

  all-bindings-==-rec : {V : Set} {d1 d2 : dl V} {x1 x2 : Nat} {v1 v2 : V} →
                         ((x : Nat) → ((x1 , v1) :: d1) lkup x == ((x2 , v2) :: d2) lkup x) →
                         ((x : Nat) → d1 lkup x == d2 lkup x)
  all-bindings-==-rec {x1 = x1} {x2} h x
    with h x1 | h x2
  ... | eq1 | eq2
    rewrite <dec-refl x1 | <dec-refl x2
    with <dec x1 x2 | <dec x2 x1
  ... | Inl _ | _
          = abort (somenotnone eq1)
  ... | Inr _ | Inl _
          = abort (somenotnone (! eq2))
  ... | Inr (Inl refl) | Inr (Inl refl)
          rewrite someinj eq1 | someinj eq2
            = all-bindings-==-rec-eq h x
  ... | Inr (Inl refl) | Inr (Inr x2<x2)
          = abort (<antirefl x2<x2)
  ... | Inr (Inr x2<x2) | Inr (Inl refl)
          = abort (<antirefl x2<x2)
  ... | Inr (Inr x2<x1) | Inr (Inr x1<x2)
          = abort (<antisym x1<x2 x2<x1)

  sad-lemma : {V : Set} {d : dl V} {x n : Nat} {v v' : V} →
               (x + 1+ n , v') ∈' ((n , v) :: d) →
               Σ[ x' ∈ Nat ] Σ[ d' ∈ dl V ] (
                  d' == ((n , v) :: d) ∧
                  x' == x + 1+ n ∧
                  (x' , v') ∈' d')
  sad-lemma h = _ , _ , refl , refl , h

  lemma-math' : ∀{x x1 n} → x ≠ x1 + (n + 1+ x)
  lemma-math' {x} {x1} {n}
    rewrite ! (+assc {x1} {n} {1+ x})
          | n+1+m==1+n+m {x1 + n} {x}
          | +comm {1+ x1 + n} {x}
      = n≠n+1+m

  lookup-cons-2' : {V : Set} {d : dl V} {n : Nat} {v : V} → d lkup n == Some v → (n , v) ∈' d
  lookup-cons-2' {d = []} ()
  lookup-cons-2' {d = ((hn , hv) :: t)} {n} h
    with <dec n hn
  lookup-cons-2' {d = ((hn , hv) :: t)} {n} ()     | Inl _
  lookup-cons-2' {d = ((hn , hv) :: t)} {.hn} refl | Inr (Inl refl) = InH
  lookup-cons-2' {d = ((hn , hv) :: t)} {n} {v} h  | Inr (Inr hn<n)
    = tr
        (λ y → (y , v) ∈' ((hn , hv) :: t))
        (m-n+n==m (n<m→1+n≤m hn<n))
        (InT (lookup-cons-2' {d = t} h))

  lookup-cons-1' : {V : Set} {d : dl V} {n : Nat} {v : V} →
                    (n , v) ∈' d →
                    d lkup n == Some v
  lookup-cons-1' {n = x} InH rewrite <dec-refl x = refl
  lookup-cons-1' (InT {d = d} {n = x} {s} {v} x∈d)
    with <dec (x + 1+ s) s
  ... | Inl x+1+s<s        = abort (<antisym x+1+s<s (n<m→n<s+m n<1+n))
  ... | Inr (Inl x+1+s==s) = abort ((flip n≠n+1+m) (n+1+m==1+n+m · (+comm {1+ s} · x+1+s==s)))
  ... | Inr (Inr s<x+1+s)
    with lookup-cons-1' x∈d
  ... | h rewrite ! (undelta s x s<x+1+s) = h

  n,v∈'d,,n,v : {V : Set} {d : dl V} {n : Nat} {v : V} → (n , v) ∈' (d ,,' (n , v))
  n,v∈'d,,n,v {d = []} {n} {v} = InH
  n,v∈'d,,n,v {d = ((hn , hv) :: t)} {n} {v}
    with <dec n hn
  ... | Inl _          = InH
  ... | Inr (Inl refl) = InH
  ... | Inr (Inr hn<n) =
          tr
            (λ y → (y , v) ∈' ((hn , hv) :: (t ,,' (delta hn<n , v))))
            (m-n+n==m (n<m→1+n≤m hn<n))
            (InT (n,v∈'d,,n,v {d = t} {delta hn<n}))

  n∈d+→'n∈d : {V : Set} {d : dl V} {n n' : Nat} {v v' : V} →
               n ≠ n' →
               (n , v) ∈' (d ,,' (n' , v')) →
               (n , v) ∈' d
  n∈d+→'n∈d {d = []} n≠n' InH = abort (n≠n' refl)
  n∈d+→'n∈d {d = []} n≠n' (InT ())
  n∈d+→'n∈d {d = (hn , hv) :: t} {n' = n'} n≠n' n∈d+
    with <dec n' hn
  n∈d+→'n∈d {_} {(hn , hv) :: t} {n' = n'} n≠n' InH | Inl n'<hn = abort (n≠n' refl)
  n∈d+→'n∈d {_} {(hn , hv) :: t} {n' = n'} n≠n' (InT InH) | Inl n'<hn
    rewrite m-n+n==m (n<m→1+n≤m n'<hn) = InH
  n∈d+→'n∈d {_} {(hn , hv) :: t} {n' = n'} n≠n' (InT (InT {n = n} n∈d+)) | Inl n'<hn
    rewrite +assc {n} {1+ (delta n'<hn)} {1+ n'} | m-n+n==m (n<m→1+n≤m n'<hn)
      = InT n∈d+
  n∈d+→'n∈d {_} {(hn , hv) :: t} {n' = .hn} n≠n' InH | Inr (Inl refl) = abort (n≠n' refl)
  n∈d+→'n∈d {_} {(hn , hv) :: t} {n' = .hn} n≠n' (InT n∈d+) | Inr (Inl refl) = InT n∈d+
  n∈d+→'n∈d {_} {(hn , hv) :: t} {n' = n'} n≠n' InH | Inr (Inr hn<n') = InH
  n∈d+→'n∈d {_} {(hn , hv) :: t} {n' = n'} n≠n' (InT n∈d+) | Inr (Inr hn<n')
    = InT (n∈d+→'n∈d (λ where refl → n≠n' (m-n+n==m (n<m→1+n≤m hn<n'))) n∈d+)

  n∈d→'n∈d+ : {V : Set} {d : dl V} {n n' : Nat} {v v' : V} →
               n ≠ n' →
               (n , v) ∈' d →
               (n , v) ∈' (d ,,' (n' , v'))
  n∈d→'n∈d+ {n = n} {n'} {v} {v'} n≠n' (InH {d = d'})
    with <dec n' n
  ... | Inl n'<n
    = tr
        (λ y → (y , v) ∈' ((n' , v') :: ((delta n'<n , v) :: d')))
        (m-n+n==m (n<m→1+n≤m n'<n))
        (InT InH)
  ... | Inr (Inl refl) = abort (n≠n' refl)
  ... | Inr (Inr n<n') = InH
  n∈d→'n∈d+ {n = .(_ + 1+ _)} {n'} {v} {v'} n≠n' (InT {d = d} {n} {s} {v' = v''} n∈d)
    with <dec n' s
  ... | Inl n'<s
    = tr
        (λ y → (y , v) ∈' ((n' , v') :: ((delta n'<s , v'') :: d)))
        ((+assc {b = 1+ (delta n'<s)}) · (ap1 (n +_) (1+ap (m-n+n==m (n<m→1+n≤m n'<s)))))
        (InT (InT n∈d))
  ... | Inr (Inl refl) = InT n∈d
  ... | Inr (Inr s<n') =
          InT (n∈d→'n∈d+ (λ where refl → n≠n' (m-n+n==m (n<m→1+n≤m s<n'))) n∈d)

  mem-dec' : {V : Set} (d : dl V) (n : Nat) → dom' d n ∨ n #' d
  mem-dec' [] n = Inr (λ ())
  mem-dec' ((hn , hv) :: t) n
    with <dec n hn
  ... | Inl n<hn       = Inr (too-small n<hn)
  ... | Inr (Inl refl) = Inl (hv , InH)
  ... | Inr (Inr hn<n)
    with mem-dec' t (delta hn<n)
  mem-dec' ((hn , hv) :: t) n | Inr (Inr hn<n) | Inl (v , rec) =
    Inl (v , tr
               (λ y → (y , v) ∈' ((hn , hv) :: t))
               (m-n+n==m (n<m→1+n≤m hn<n))
               (InT rec))
  mem-dec' {V} ((hn , hv) :: t) n | Inr (Inr hn<n) | Inr dne =
    Inr n∉d
      where
      n∉d : Σ[ v ∈ V ] ((n , v) ∈' ((hn , hv) :: t)) → ⊥
      n∉d (_ , n∈d) with n∈d
      ... | InH = (π2 hn<n) refl
      ... | InT {n = s} n-hn-1∈t
        rewrite ! (undelta hn s hn<n) = dne (_ , n-hn-1∈t)

  extensional' : {V : Set} {d1 d2 : dl V} →
                  ((n : Nat) → d1 lkup n == d2 lkup n) →
                  d1 == d2
  extensional' {d1 = []} {[]} all-bindings-== = refl
  extensional' {d1 = []} {(hn2 , hv2) :: t2} all-bindings-==
    = abort (all-not-none {d = t2} {x = hn2} (all-bindings-== hn2))
  extensional' {d1 = (hn1 , hv1) :: t1} {[]} all-bindings-==
    = abort (all-not-none {d = t1} {x = hn1} (! (all-bindings-== hn1)))
  extensional' {d1 = (hn1 , hv1) :: t1} {(hn2 , hv2) :: t2} all-bindings-==
    rewrite extensional' {d1 = t1} {t2} (all-bindings-==-rec all-bindings-==)
    with all-bindings-== hn1 | all-bindings-== hn2
  ... | hv1== | hv2== rewrite <dec-refl hn1 | <dec-refl hn2
    with <dec hn1 hn2 | <dec hn2 hn1
  ... | Inl hn1<hn2 | _
          = abort (somenotnone hv1==)
  ... | Inr (Inl refl) | Inl hn2<hn1
          = abort (somenotnone (! hv2==))
  ... | Inr (Inr hn2<hn1) | Inl hn2<'hn1
          = abort (somenotnone (! hv2==))
  ... | Inr (Inl refl) | Inr _
          rewrite someinj hv1== = refl
  ... | Inr (Inr hn2<hn1) | Inr (Inl refl)
          rewrite someinj hv2== = refl
  ... | Inr (Inr hn2<hn1) | Inr (Inr hn1<hn2)
          = abort (<antisym hn1<hn2 hn2<hn1)

  ==-dec' : {V : Set}
             (d1 d2 : dl V) →
             ((v1 v2 : V) → v1 == v2 ∨ v1 ≠ v2) →
             d1 == d2 ∨ d1 ≠ d2
  ==-dec' [] [] _ = Inl refl
  ==-dec' [] (_ :: _) _ = Inr (λ ())
  ==-dec' (_ :: _) [] _ = Inr (λ ())
  ==-dec' ((hn1 , hv1) :: t1) ((hn2 , hv2) :: t2) V==dec
    with natEQ hn1 hn2 | V==dec hv1 hv2 | ==-dec' t1 t2 V==dec
  ... | Inl refl | Inl refl | Inl refl = Inl refl
  ... | Inl refl | Inl refl | Inr ne   = Inr λ where refl → ne refl
  ... | Inl refl | Inr ne   | _        = Inr λ where refl → ne refl
  ... | Inr ne   | _        | _        = Inr λ where refl → ne refl

  delete' : {V : Set} {d : dl V} {n : Nat} {v : V} →
             (n , v) ∈' d →
             Σ[ d⁻ ∈ dl V ] (
                d == d⁻ ,,' (n , v) ∧
                n #' d⁻)
  delete' {d = (n' , v') :: d} {n} n∈d
    with <dec n n'
  ... | Inl n<n'       = abort (too-small n<n' (_ , n∈d))
  delete' {_} {(n' , v') :: []} {.n'} InH                 | Inr (Inl _) = [] , refl , λ ()
  delete' {_} {(n' , v') :: ((n'' , v'') :: d)} {.n'} InH | Inr (Inl _)
    = ((n'' + 1+ n' , v'') :: d) , lem , λ {(_ , n'∈d+) → abort (too-small (n<m→n<s+m n<1+n) (_ , n'∈d+))}
      where
        lem : ((n' , v') :: ((n'' , v'') :: d)) == ((n'' + 1+ n' , v'') :: d) ,,' (n' , v')
        lem
          with <dec n' (n'' + 1+ n')
        lem | Inl n'<n''+1+n' rewrite ! (undelta n' n'' n'<n''+1+n') = refl
        lem | Inr (Inl false) = abort (lemma-math' {x1 = Z} false)
        lem | Inr (Inr false) = abort (<antisym false (n<m→n<s+m n<1+n))
  delete' {d = (n' , v') :: d} InH       | Inr (Inr n'<n') = abort (<antirefl n'<n')
  delete' {d = (n' , v') :: d} (InT n∈d) | Inr _
    with delete' {d = d} n∈d
  delete' {d = (n' , v') :: d} {.(_ + 1+ n')} {v} (InT {n = x} n∈d) | Inr _ | d⁻ , refl , x#d⁻
    = _ , lem' , lem
      where
        lem : (x + 1+ n') #' ((n' , v') :: d⁻)
        lem (_ , x+1+n'∈d?)
          with sad-lemma x+1+n'∈d?
        ... | _ , _ , refl , n'==x+1+n' , InH = abort (lemma-math' {x1 = Z} n'==x+1+n')
        ... | _ , _ , refl , n'==x+1+n' , InT x+1+n'∈d'
          rewrite +inj {b = 1+ n'} n'==x+1+n'
            = x#d⁻ (_ , x+1+n'∈d')
        lem' : ((n' , v') :: (d⁻ ,,' (x , v))) == (((n' , v') :: d⁻) ,,' (x + 1+ n' , v))
        lem'
          with <dec (x + 1+ n') n'
        lem' | Inl x+1+n'<n'       = abort (<antisym x+1+n'<n' (n<m→n<s+m n<1+n))
        lem' | Inr (Inl false)     = abort (lemma-math' {x1 = Z} (! false))
        lem' | Inr (Inr n'<x+1+n') rewrite ! (undelta n' x n'<x+1+n') = refl

  extend-size' : {V : Set} {d : dl V} {n : Nat} {v : V} →
                  n #' d →
                  ∥ d ,,' (n , v) ∥ == 1+ ∥ d ∥
  extend-size' {d = []} n#d = refl
  extend-size' {d = (n' , v') :: d} {n} n#d
    with <dec n n'
  ... | Inl n<n'       = refl
  ... | Inr (Inl refl) = abort (n#d (_ , InH))
  ... | Inr (Inr n'<n)
          = 1+ap (extend-size' λ {(v , diff∈d) →
              n#d (v , tr
                         (λ y → (y , v) ∈' ((n' , v') :: d))
                         (m-n+n==m (n<m→1+n≤m n'<n))
                         (InT diff∈d))})

  ---- contrapositives of some previous lemmas ----

  lookup-dec' : {V : Set} (d : dl V) (n : Nat) →
                 Σ[ v ∈ V ] (d lkup n == Some v) ∨ d lkup n == None
  lookup-dec' d n
    with d lkup n
  ... | Some v = Inl (v , refl)
  ... | None   = Inr refl

  lookup-cp-2' : {V : Set} {d : dl V} {n : Nat} →
                  n #' d →
                  d lkup n == None
  lookup-cp-2' {d = d} {n} n#d
    with lookup-dec' d n
  ... | Inl (_ , n∈d) = abort (n#d (_ , lookup-cons-2' n∈d))
  ... | Inr n#'d      = n#'d

  n#d→'n#d+ : {V : Set} {d : dl V} {n n' : Nat} {v' : V} →
                n ≠ n' →
                n #' d →
                n #' (d ,,' (n' , v'))
  n#d→'n#d+ {d = d} {n} {n'} {v'} n≠n' n#d
    with mem-dec' (d ,,' (n' , v')) n
  ... | Inl (_ , n∈d+) = abort (n#d (_ , n∈d+→'n∈d n≠n' n∈d+))
  ... | Inr n#d+       = n#d+

  ---- union, and dlt <=> list conversion definitions

  merge' : {V : Set} → (V → V → V) → Maybe V → V → V
  merge' merge ma1 v2
    with ma1
  ... | None    = v2
  ... | Some v1 = merge v1 v2

  union' : {V : Set} → (V → V → V) → dl V → dl V → Nat → dl V
  union' merge d1 [] _ = d1
  union' merge d1 ((hn , hv) :: d2) offset
    with d1 ,,' (hn + offset , merge' merge (d1 lkup hn + offset) hv)
  ... | d1+ = union' merge d1+ d2 (1+ hn + offset)

  dlt⇒list' : {V : Set} (d : dl V) → dl V
  dlt⇒list' [] = []
  dlt⇒list' ((x , v) :: d) = (x , v) :: map (λ {(x' , v') → x' + 1+ x , v'}) (dlt⇒list' d)

  list⇒dlt' : {V : Set} (d : dl V) → dl V
  list⇒dlt' = foldr _,,'_ []

  ---- union, dlt <=> list, etc lemmas ----

  lemma-union'-0 : {V : Set} {m : V → V → V} {d1 d2 : dl V} {x n : Nat} {v : V} →
                    (x , v) ∈' d1 →
                    (x , v) ∈' (union' m d1 d2 (n + 1+ x))
  lemma-union'-0 {d2 = []} x∈d1 = x∈d1
  lemma-union'-0 {d2 = (x1 , v1) :: d2} {x} {n} x∈d1
    rewrite ! (+assc {1+ x1} {n} {1+ x})
      = lemma-union'-0 {d2 = d2} {n = 1+ x1 + n} (n∈d→'n∈d+ (lemma-math' {x1 = x1} {n}) x∈d1)

  lemma-union'-1 : {V : Set} {m : V → V → V} {d1 d2 : dl V} {x n : Nat} {v : V} →
                    (x , v) ∈' d1 →
                    (n≤x : n ≤ x) →
                    (difference n≤x) #' d2 →
                    (x , v) ∈' (union' m d1 d2 n)
  lemma-union'-1 {d2 = []} {x} x∈d1 n≤x x-n#d2 = x∈d1
  lemma-union'-1 {m = m} {d1} {(x1 , v1) :: d2} {x} {n} {v} x∈d1 n≤x x-n#d2
    with <dec x (x1 + n)
  lemma-union'-1 {m = m} {d1} {(x1 , v1) :: d2} {x} {n} {v} x∈d1 n≤x x-n#d2 | Inl x<x1+n
    with d1 lkup x1 + n
  lemma-union'-1 {m = m} {d1} {(x1 , v1) :: d2} {x} {n} {v} x∈d1 n≤x x-n#d2 | Inl x<x1+n | Some v'
    with expr-eq (λ _ → d1 ,,' (x1 + n , m v' v1))
  lemma-union'-1 {m = m} {d1} {(x1 , v1) :: d2} {x} {n} {v} x∈d1 n≤x x-n#d2 | Inl x<x1+n | Some v' | d1+ , refl
    = tr
         (λ y → (x , v) ∈' (union' m d1+ d2 y))
         (n+1+m==1+n+m {difference (π1 x<x1+n)} · 1+ap (m-n+n==m (π1 x<x1+n)))
         (lemma-union'-0 {d2 = d2} (n∈d→'n∈d+ (π2 x<x1+n) x∈d1))
  lemma-union'-1 {m = m} {d1} {(x1 , v1) :: d2} {x} {n} {v} x∈d1 n≤x x-n#d2 | Inl x<x1+n | None
    with expr-eq (λ _ → d1 ,,' (x1 + n , v1))
  lemma-union'-1 {m = m} {d1} {(x1 , v1) :: d2} {x} {n} {v} x∈d1 n≤x x-n#d2 | Inl x<x1+n | None | d1+ , refl
    = tr
         (λ y → (x , v) ∈' (union' m d1+ d2 y))
         (n+1+m==1+n+m {difference (π1 x<x1+n)} · 1+ap (m-n+n==m (π1 x<x1+n)))
         (lemma-union'-0 {d2 = d2} (n∈d→'n∈d+ (π2 x<x1+n) x∈d1))
  lemma-union'-1 {m = m} {d1} {(x1 , v1) :: d2} {x} {n} {v} x∈d1 n≤x x-n#d2 | Inr (Inl refl)
    rewrite +comm {x1} {n} | n+m-n==m n≤x
      = abort (x-n#d2 (_ , InH))
  lemma-union'-1 {m = m} {d1} {(x1 , v1) :: d2} {x} {n} {v} x∈d1 n≤x x-n#d2 | Inr (Inr x1+n<x)
    rewrite (! (a+b==c→a==c-b (+assc {delta x1+n<x} · m-n+n==m (n<m→1+n≤m x1+n<x)) n≤x))
      = lemma-union'-1
          (n∈d→'n∈d+ (flip (π2 x1+n<x)) x∈d1)
          (n<m→1+n≤m x1+n<x)
          λ {(_ , x-x1-n∈d2) → x-n#d2 (_ , InT x-x1-n∈d2)}

  lemma-union'-2 : {V : Set} {m : V → V → V} {d1 d2 : dl V} {x n : Nat} {v : V} →
                    (x + n) #' d1 →
                    (x , v) ∈' d2 →
                    (x + n , v) ∈' (union' m d1 d2 n)
  lemma-union'-2 {d1 = d1} x+n#d1 (InH {d = d2})
    rewrite lookup-cp-2' x+n#d1
      = lemma-union'-0 {d2 = d2} {n = Z} (n,v∈'d,,n,v {d = d1})
  lemma-union'-2 {d1 = d1} {n = n} x+n#d1 (InT {d = d2} {n = x} {s} x∈d2)
    rewrite +assc {x} {1+ s} {n}
    with d1 lkup s + n
  ... | Some v'
    = lemma-union'-2
        (λ {(_ , x∈d1+) →
             x+n#d1 (_ , n∈d+→'n∈d (flip (lemma-math' {x1 = Z})) x∈d1+)})
        x∈d2
  ... | None
    = lemma-union'-2
        (λ {(_ , x∈d1+) →
             x+n#d1 (_ , n∈d+→'n∈d (flip (lemma-math' {x1 = Z})) x∈d1+)})
        x∈d2

  lemma-union'-3 : {V : Set} {m : V → V → V} {d1 d2 : dl V} {x n : Nat} {v1 v2 : V} →
                    (x + n , v1) ∈' d1 →
                    (x , v2) ∈' d2 →
                    (x + n , m v1 v2) ∈' (union' m d1 d2 n)
  lemma-union'-3 {d1 = d1} x+n∈d1 (InH {d = d2})
    rewrite lookup-cons-1' x+n∈d1
      = lemma-union'-0 {d2 = d2} {n = Z} (n,v∈'d,,n,v {d = d1})
  lemma-union'-3 {d1 = d1} {n = n} x+n∈d1 (InT {d = d2} {n = x} {s} x∈d2)
    rewrite +assc {x} {1+ s} {n}
    with d1 lkup s + n
  ... | Some v'
    = lemma-union'-3 (n∈d→'n∈d+ (flip (lemma-math' {x1 = Z})) x+n∈d1) x∈d2
  ... | None
    = lemma-union'-3 (n∈d→'n∈d+ (flip (lemma-math' {x1 = Z})) x+n∈d1) x∈d2

  lemma-union'-4 : {V : Set} {m : V → V → V} {d1 d2 : dl V} {x n : Nat} →
                    dom' (union' m d1 d2 n) x →
                    dom' d1 x ∨ (Σ[ s ∈ Nat ] (x == n + s ∧ dom' d2 s))
  lemma-union'-4 {d2 = []} x∈un = Inl x∈un
  lemma-union'-4 {d1 = d1} {(x1 , _) :: d2} {x} {n} x∈un
    with lemma-union'-4 {d2 = d2} x∈un
  ... | Inr (s , refl , _ , s∈d2)
    rewrite +comm {x1} {n}
          | ! (n+1+m==1+n+m {n + x1} {s})
          | +assc {n} {x1} {1+ s}
          | +comm {x1} {1+ s}
          | ! (n+1+m==1+n+m {s} {x1})
      = Inr (_ , refl , _ , InT s∈d2)
  ... | Inl (_ , x∈d1+)
    with natEQ x (n + x1)
  ... | Inl refl   = Inr (_ , refl , _ , InH)
  ... | Inr x≠n+x1
    rewrite +comm {x1} {n}
      = Inl (_ , n∈d+→'n∈d x≠n+x1 x∈d1+)

  dlt⇒list-size' : {V : Set} {d : dl V} → ∥ dlt⇒list' d ∥ == ∥ d ∥
  dlt⇒list-size' {d = []} = refl
  dlt⇒list-size' {d = _ :: d} = 1+ap (map-len · dlt⇒list-size')

  dlt⇒list-In-1' : {V : Set} {d : dl V} {n : Nat} {v : V} →
                    (n , v) ∈' d →
                    (n , v) In dlt⇒list' d
  dlt⇒list-In-1' InH = LInH
  dlt⇒list-In-1' (InT ∈h) = LInT <| map-In <| dlt⇒list-In-1' ∈h

  too-small-list : {V : Set} {d : dl V} {m m' : Nat} {v : V} →
                    m ≤ m' →
                    (m , v) In (map (λ { (n'' , v'') → n'' + 1+ m' , v'' }) (dlt⇒list' d)) →
                    ⊥
  too-small-list {d = (n2 , v2) :: d} n≤n' LInH
    = abort (lemma-math' {x1 = Z} (≤antisym (≤trans n≤m+n (n≤m+n {m = n2})) n≤n'))
  too-small-list {d = (n2 , v2) :: d} {m} {m'} {v} m≤m' (LInT in')
    = too-small-list (≤trans m≤m' (≤trans n≤m+n (n≤m+n {m = n2}))) rec-in
    where
      rec-in =
        tr
          (λ y → (m , v) In y)
          (map^2
             {f = (λ { (n'' , v'') → n'' + 1+ m' , v'' })}
             {(λ { (n'' , v'') → n'' + 1+ n2 , v'' })}
             {dlt⇒list' d}
           ·
           map-ext (λ where (n'' , v'') → ap1 (λ y' → y' , v'') <| +assc {n''} {b = 1+ n2} {c = 1+ m'}))
          in'

  dlt⇒list-In-2' : {V : Set} {d : dl V} {n : Nat} {v : V} →
                     (n , v) In dlt⇒list' d →
                     (n , v) ∈' d
  dlt⇒list-In-2' {d = _ :: d} LInH = InH
  dlt⇒list-In-2' {d = (n' , v') :: d} {n} (LInT in')
    with <dec n n'
  ... | Inl n<n'       = abort (too-small-list (π1 n<n') in')
  ... | Inr (Inl refl) = abort (too-small-list ≤refl in')
  ... | Inr (Inr n'<n)
    with n<m→s+1+n=m n'<n
  ... | _ , refl = InT (dlt⇒list-In-2' (lem2 in'))
    where
      lem1 : ∀{V l} {m1 m2 : Nat} {vv1 vv2 : V} →
               m1 ≠ m2 →
               (in'' : (m1 , vv1) In ((m2 , vv2) :: l)) →
               Σ[ in2 ∈ ((m1 , vv1) In l) ] (in'' == LInT in2)
      lem1 ne LInH = abort (ne refl)
      lem1 ne (LInT in'') = in'' , refl
      lem2 : ∀{V s l} {vv : V} →
               (s + 1+ n' , vv) In map (λ { (n'' , v'') → n'' + 1+ n' , v'' }) l →
               (s , vv) In l
      lem2 {s = s} {(n2 , v2) :: l} in''
        with natEQ s n2
      lem2 {s = s} {(s , v2) :: l} LInH        | Inl refl = LInH
      lem2 {s = s} {(s , v2) :: l} (LInT in'') | Inl refl = LInT (lem2 in'')
      ... | Inr ne
        with lem1 (+inj-cp ne) in''
      ... | in2 , refl = LInT (lem2 in2)

  list⇒dlt-In' : {V : Set} {l : dl V} {n : Nat} {v : V} →
                  (n , v) ∈' list⇒dlt' l →
                  (n , v) In l
  list⇒dlt-In' {l = (n' , v') :: l} {n} ∈h
    rewrite foldl-++ {l1 = reverse l} {(n' , v') :: []} {_,,'_} {[]}
    with natEQ n n'
  ... | Inr ne   = LInT (list⇒dlt-In' (n∈d+→'n∈d ne ∈h))
  ... | Inl refl
    rewrite someinj <| (! <| lookup-cons-1' ∈h) · (lookup-cons-1' {n = n} {v'} <| n,v∈'d,,n,v {d = foldl _,,'_ [] (reverse l)})
      = LInH

  list⇒dlt-order' : {V : Set} {l1 l2 : dl V} {n : Nat} {v1 v2 : V} →
                     (n , v1) ∈' (list⇒dlt' ((n , v1) :: l1 ++ ((n , v2) :: l2)))
  list⇒dlt-order' {l1 = l1} {l2} {n} {v1} {v2}
    rewrite foldl-++ {l1 = reverse (l1 ++ ((n , v2) :: l2))} {(n , v1) :: []} {_,,'_} {[]}
      = n,v∈'d,,n,v {d = foldl _,,'_ [] <| reverse (l1 ++ ((n , v2) :: l2))}

  bij-pair-1 : {V : Set} (nv : Nat ∧ V) → (nat <| key <| π1 nv , π2 nv) == nv
  bij-pair-1 (n , v) rewrite convert-bij2 {t = n} = refl

  bij-pair-2 : {V : Set} (kv : K ∧ V) → (key <| nat <| π1 kv , π2 kv) == kv
  bij-pair-2 (k , v) rewrite convert-bij1 {f = k} = refl

  dltmap-func' : {V1 V2 : Set} {d : dl V1} {f : V1 → V2} {n : Nat} {v : V1} →
                  (map (λ { (hn , hv) → hn , f hv }) (d ,,' (n , v)))
                    ==
                  (map (λ { (hn , hv) → hn , f hv }) d ,,' (n , f v))
  dltmap-func' {d = []} = refl
  dltmap-func' {d = (nh , vh) :: d} {f = f} {n}
    with <dec n nh
  ... | Inl n<nh       = refl
  ... | Inr (Inl refl) = refl
  ... | Inr (Inr nh<n) = ap1 ((nh , f vh) ::_) (dltmap-func' {d = d})

  -- these proofs could use refactoring -
  -- contraction should probably make use of ==-dec'
  -- and exchange is way too long and repetitive

  contraction' : {V : Set} {d : dl V} {n : Nat} {v v' : V} → (d ,,' (n , v')) ,,' (n , v) == d ,,' (n , v)
  contraction' {d = []} {n} rewrite <dec-refl n = refl
  contraction' {d = (hn , hv) :: t} {n} {v} {v'}
    with <dec n hn
  ... | Inl _          rewrite <dec-refl n  = refl
  ... | Inr (Inl refl) rewrite <dec-refl hn = refl
  ... | Inr (Inr hn<n)
    with <dec n hn
  ... | Inl n<hn        = abort (<antisym n<hn hn<n)
  ... | Inr (Inl refl)  = abort (<antirefl hn<n)
  ... | Inr (Inr hn<'n)
    with contraction' {d = t} {delta hn<'n} {v} {v'}
  ... | eq
    rewrite diff-proof-irrelevance (n<m→1+n≤m hn<n) (n<m→1+n≤m hn<'n) | eq
      = refl

  exchange' : {V : Set} {d : dl V} {n1 n2 : Nat} {v1 v2 : V} →
               n1 ≠ n2 →
               (d ,,' (n1 , v1)) ,,' (n2 , v2) == (d ,,' (n2 , v2)) ,,' (n1 , v1)
  exchange' {V} {d} {n1} {n2} {v1} {v2} n1≠n2 = extensional' fun
    where
      fun : (n : Nat) →
             ((d ,,' (n1 , v1)) ,,' (n2 , v2)) lkup n ==
             ((d ,,' (n2 , v2)) ,,' (n1 , v1)) lkup n
      fun n
        with natEQ n n1 | natEQ n n2 | mem-dec' d n
      fun n  | Inl refl | Inl refl | _
        = abort (n1≠n2 refl)
      fun n1 | Inl refl | Inr n≠n2 | Inl (_ , n1∈d)
        with n,v∈'d,,n,v {d = d} {n1} {v1}
      ... | n∈d+1
        with n∈d→'n∈d+ {v' = v2} n≠n2 n∈d+1 | n,v∈'d,,n,v {d = d ,,' (n2 , v2)} {n1} {v1}
      ... | n∈d++1 | n∈d++2
        rewrite lookup-cons-1' n∈d++1 | lookup-cons-1' n∈d++2 = refl
      fun n1 | Inl refl | Inr n≠n2 | Inr n1#d
        with n,v∈'d,,n,v {d = d} {n1} {v1}
      ... | n∈d+1
        with n∈d→'n∈d+ {v' = v2} n≠n2 n∈d+1 | n,v∈'d,,n,v {d = d ,,' (n2 , v2)} {n1} {v1}
      ... | n∈d++1 | n∈d++2
        rewrite lookup-cons-1' n∈d++1 | lookup-cons-1' n∈d++2 = refl
      fun n2 | Inr n≠n1 | Inl refl | Inl (_ , n2∈d)
        with n,v∈'d,,n,v {d = d} {n2} {v2}
      ... | n∈d+2
        with n∈d→'n∈d+ {v' = v1} n≠n1 n∈d+2 | n,v∈'d,,n,v {d = d ,,' (n1 , v1)} {n2} {v2}
      ... | n∈d++1 | n∈d++2
        rewrite lookup-cons-1' n∈d++1 | lookup-cons-1' n∈d++2 = refl
      fun n2 | Inr n≠n1 | Inl refl | Inr n2#d
        with n,v∈'d,,n,v {d = d} {n2} {v2}
      ... | n∈d+2
        with n∈d→'n∈d+ {v' = v1} n≠n1 n∈d+2 | n,v∈'d,,n,v {d = d ,,' (n1 , v1)} {n2} {v2}
      ... | n∈d++1 | n∈d++2
        rewrite lookup-cons-1' n∈d++1 | lookup-cons-1' n∈d++2 = refl
      fun n  | Inr n≠n1 | Inr n≠n2 | Inl (_ , n∈d)
        with n∈d→'n∈d+ {v' = v1} n≠n1 n∈d   | n∈d→'n∈d+ {v' = v2} n≠n2 n∈d
      ... | n∈d+1  | n∈d+2
        with n∈d→'n∈d+ {v' = v2} n≠n2 n∈d+1 | n∈d→'n∈d+ {v' = v1} n≠n1 n∈d+2
      ... | n∈d++1 | n∈d++2
        rewrite lookup-cons-1' n∈d++1 | lookup-cons-1' n∈d++2 = refl
      fun n  | Inr n≠n1 | Inr n≠n2 | Inr n#d
        with n#d→'n#d+ {v' = v1} n≠n1 n#d   | n#d→'n#d+ {v' = v2} n≠n2 n#d
      ... | n#d+1  | n#d+2
        with n#d→'n#d+ {v' = v2} n≠n2 n#d+1 | n#d→'n#d+ {v' = v1} n≠n1 n#d+2
      ... | n#d++1 | n#d++2
        rewrite lookup-cp-2' n#d++1 | lookup-cp-2' n#d++2 = refl

max_stars_repo_name: nickcollins/dependent-dicts-agda

max_issues_repo_name: nickcollins/dependent-dicts-agda

max_forks_repo_name: nickcollins/dependent-dicts-agda


text:
module Issue335 where

postulate
  A : Set
  k : (.A -> Set) -> A

bla = k (\ .(x : A) -> A)
-- syntax for irrelevant typed lambda now exists


text:
module Data.Nat.Etc where

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Function
open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Binary

open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; trans; sym)
open PropEq.≡-Reasoning

-- exponention
_^_ : ℕ → ℕ → ℕ
a ^ zero  = 1
a ^ suc b = a * (a ^ b)

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

distrib-left-*-+ : ∀ m n o → m * (n + o) ≡ m * n + m * o
distrib-left-*-+ m n o =
        begin
            m * (n + o)
        ≡⟨ *-comm m (n + o) ⟩
            (n + o) * m
        ≡⟨ distribʳ-*-+ m n o ⟩
            n * m + o * m
        ≡⟨ cong (flip _+_ (o * m)) (*-comm n m) ⟩
            m * n + o * m
        ≡⟨ cong (_+_ (m * n)) (*-comm o m) ⟩
            m * n + m * o
        ∎
{-
no-zero-divisor : ∀ m n → m ≢ 0 → m * n ≡ 0 → n ≡ 0
no-zero-divisor zero    n       p q = contradiction q p
no-zero-divisor (suc m) zero    p q = refl
no-zero-divisor (suc m) (suc n) p ()

m^n≢0 : ∀ m n → {m≢0 : m ≢ 0} → m ^ n ≢ 0
m^n≢0 m zero    {p} = λ ()
m^n≢0 m (suc n) {p} = contraposition (no-zero-divisor m (m ^ n) p) (m^n≢0 m n {p})

m≰n⇒n<m : (m n : ℕ) → m ≰ n → m > n
m≰n⇒n<m zero n p = contradiction p (λ z → z z≤n)
m≰n⇒n<m (suc m) zero p = s≤s z≤n
m≰n⇒n<m (suc m) (suc n) p = s≤s (m≰n⇒n<m m n (λ z → p (s≤s z)))
-}

>⇒≰ : _>_ ⇒ _≰_
>⇒≰ {zero} ()
>⇒≰ {suc m} {zero} rel ()
>⇒≰ {suc m} {suc n} (s≤s rel) (s≤s x) = contradiction x (>⇒≰ rel)

>⇒≢ : _>_ ⇒ _≢_
>⇒≢ {zero}  ()      m≡n
>⇒≢ {suc m} {zero}   m>n ()
>⇒≢ {suc m} {suc n} (s≤s m>n) m≡n = >⇒≢ m>n (cong pred m≡n)

{-
≰⇒> : _≰_ ⇒ _>_
≰⇒> {zero}          z≰n with z≰n z≤n
... | ()
≰⇒> {suc m} {zero}  _   = s≤s z≤n
≰⇒> {suc m} {suc n} m≰n = s≤s (≰⇒> (m≰n ∘ s≤s))
-}
{-
    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ∎
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
-- Concrete definition of contexts over a sort T
module SOAS.Context {T : Set} where

open import SOAS.Common

open import Data.List using (List; []; _∷_; _++_)

-- Context: a list of types
data Ctx : Set where
  ∅   : Ctx
  _∙_ : (α : T) → (Γ : Ctx) → Ctx
infixr 50 _∙_

-- Singleton context
pattern _⌋ τ = τ ∙ ∅
pattern ⌈_⌋ α = α ∙ ∅
pattern ⌊_ α = α
infixr 60 _⌋
infix 70 ⌈_⌋
infix 70 ⌊_

-- Context concatenation
_∔_ : Ctx → Ctx → Ctx
∅       ∔ Δ = Δ
(α ∙ Γ) ∔ Δ = α ∙ (Γ ∔ Δ)
infixl 20 _∔_

-- Context concatenation is associative
∔-assoc : (Γ Δ Θ : Ctx) → ((Γ ∔ Δ) ∔ Θ) ≡ (Γ ∔ (Δ ∔ Θ))
∔-assoc ∅ Δ Θ = refl
∔-assoc (α ∙ Γ) Δ Θ = cong (α ∙_) (∔-assoc Γ Δ Θ)

-- Empty context is right unit of context concatenation
∔-unitʳ : (Γ : Ctx) → Γ ∔ ∅ ≡ Γ
∔-unitʳ ∅ = refl
∔-unitʳ (α ∙ Γ) = cong (α ∙_) (∔-unitʳ Γ)

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- Andreas, 2017-03-21, issue #2466

-- The unifier should not turn user-written variable patterns into
-- dot patterns.

-- {-# OPTIONS -v reify.implicit:100 -v interaction.case:100 #-}
-- {-# OPTIONS -v tc.lhs.unify:40 #-}

postulate
  A B : Set

module Explicit where

  data D : A → B → Set where
    c : ∀ p {p'} x → D p' x → D p x

  test : ∀ p x → D p x → D p x
  test .p _ (c p x pp) = {!p'!}
    where
    y = x

  -- Expected: test .p _ (c p {p'} x pp) = ?

module Implicit where

  data D : A → B → Set where
    c : ∀ {p p' x} → D p' x → D p x

  test : ∀ p {x} → D p x → D p x
  test .p (c {p} {x = x} pp) = {!p'!}
    where
    y = x

  -- Expected: test .p (c {p} {p'} {x} pp) = ?

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
module InstanceArgs where

data UnitMonoid : Set where
  u : UnitMonoid
  p : UnitMonoid → UnitMonoid → UnitMonoid

record Plus (A : Set) : Set where
  infixl 6 _+_
  field
    _+_ : A → A → A

open Plus {{...}}

instance
  plus-unitMonoid : Plus UnitMonoid
  plus-unitMonoid = record { _+_ = p }

bigValue : UnitMonoid
bigValue =
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u +
  u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u + u

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

open import Categories.Category using (Category)
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)

module Categories.Category.Monoidal.Star-Autonomous {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Level

open import Categories.Category.Product using (_⁂_; assocˡ)
open import Categories.Functor using (Functor; _∘F_; id)
open import Categories.Functor.Properties using (FullyFaithful)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Functor.Hom

open Category C renaming (op to Cᵒᵖ) hiding (id)
open Monoidal M
open Functor ⊗ renaming (op to ⊗ₒₚ)
open Hom C

record Star-Autonomous : Set (levelOfTerm M) where
  field
    symmetric : Symmetric M
    Star : Functor Cᵒᵖ C

  open Functor Star renaming (op to Starₒₚ) public

  field
    FF-Star : FullyFaithful Star
    A**≃A  : (Star ∘F Starₒₚ) ≃ id
    𝒞[A⊗B,C*]≃𝒞[A,B⊗C*] : Hom[-,-] ∘F (⊗ₒₚ ⁂ Star) ≃ Hom[-,-] ∘F (id ⁂ (Star ∘F ⊗ₒₚ)) ∘F assocˡ _ _ _

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:
------------------------------------------------------------------------
-- Recognisers built on top of the parsers
------------------------------------------------------------------------

-- Note that these recognisers are different from the ones in
-- TotalRecognisers.LeftRecursion: these allow the use of fewer sharps.
-- (Compare the examples in TotalRecognisers.LeftRecursion.Expression
-- and TotalParserCombinators.Recogniser.Expression.)

module TotalParserCombinators.Recogniser where

open import Category.Monad
open import Codata.Musical.Notation
open import Data.Bool
open import Data.List as List
import Data.List.Categorical
open import Data.Maybe
open import Data.Unit
open import Level

open RawMonadPlus {f = zero} Data.List.Categorical.monadPlus
  using () renaming (_⊛_ to _⊛′_)

open import TotalParserCombinators.Parser as Parser
  using (Parser; flatten); open Parser.Parser
import TotalParserCombinators.Lib as Lib

------------------------------------------------------------------------
-- Helper function

infixl 4 _·′_

_·′_ : (mb₁ mb₂ : Maybe (List ⊤)) → List ⊤
mb₁ ·′ nothing = []
mb₁ ·′ just b₂ = List.map _ (flatten mb₁) ⊛′ b₂

------------------------------------------------------------------------
-- Recognisers

infixl 50 _·_
infixl  5 _∣_

-- Recognisers.

mutual

  -- The index is non-empty if the corresponding language contains the
  -- empty string (is nullable).

  data P (Tok : Set) : List ⊤ → Set₁ where
    -- Parsers can be turned into recognisers.
    lift  : ∀ {R n} (p : Parser Tok R n) → P Tok (List.map _ n)

    -- Symmetric choice.
    _∣_   : ∀ {n₁ n₂}
            (p₁ : P Tok n₁) (p₂ : P Tok n₂) → P Tok (n₁ ++ n₂)

    -- Sequencing.
    _·_   : ∀ {n₁ n₂}
            (p₁ : ∞⟨ n₂ ⟩P Tok (flatten n₁))
            (p₂ : ∞⟨ n₁ ⟩P Tok (flatten n₂)) →
            P Tok (n₁ ·′ n₂)

  -- Delayed if the index is /nothing/.

  ∞⟨_⟩P : Maybe (List ⊤) → Set → List ⊤ → Set₁
  ∞⟨ nothing ⟩P Tok n = ∞ (P Tok n)
  ∞⟨ just _  ⟩P Tok n =    P Tok n

------------------------------------------------------------------------
-- Helper function related to ∞⟨_⟩P

-- Is the argument parser forced? If the result is just something,
-- then it is.

forced? : ∀ {Tok m n} → ∞⟨ m ⟩P Tok n → Maybe (List ⊤)
forced? {m = m} _ = m

------------------------------------------------------------------------
-- The semantics of the recognisers is defined by translation

⟦_⟧ : ∀ {Tok n} (p : P Tok n) → Parser Tok ⊤ n
⟦ lift p ⟧  = _ <$> p
⟦ p₁ ∣ p₂ ⟧ = ⟦ p₁ ⟧ ∣ ⟦ p₂ ⟧
⟦ p₁ · p₂ ⟧ with forced? p₁ | forced? p₂
... | just xs | nothing =    _ <$> ⟦   p₁ ⟧  ⊛ ♯ ⟦ ♭ p₂ ⟧
... | just xs | just ys =    _ <$> ⟦   p₁ ⟧  ⊛   ⟦   p₂ ⟧
... | nothing | nothing = ♯ (_ <$> ⟦ ♭ p₁ ⟧) ⊛ ♯ ⟦ ♭ p₂ ⟧
... | nothing | just ys = ♯ (_ <$> ⟦ ♭ p₁ ⟧) ⊛   ⟦   p₂ ⟧


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

--
-- Prelude.agda - Some base definitions
--

module Prelude where

  open import Agda.Primitive public

  record ⊤ : Set where
    constructor tt

  {-# BUILTIN UNIT ⊤ #-}

  record Σ {i j} (A : Set i) (B : A → Set j) : Set (i ⊔ j) where
    constructor _,_
    field
      fst : A
      snd : B fst

  open Σ public

  data ℕ : Set where
    O : ℕ
    S : ℕ → ℕ

  {-# BUILTIN NATURAL ℕ #-}

  uncurry : ∀ {i j k} {A : Set i} {B : A → Set j} {C : Set k} →
            (φ : (a : A) → (b : B a) → C) →
            Σ A B → C
  uncurry φ (a , b) = φ a b

  curry : ∀ {i j k} {A : Set i} {B : A → Set j} {C : Set k} →
          (ψ : Σ A B → C) →
          (a : A) → (b : B a) → C
  curry ψ a b = ψ (a , b)

  infix 30 _==_

  data _==_ {i} {A : Set i} (a : A) : A → Set i where
    idp : a == a

  {-# BUILTIN EQUALITY _==_ #-}
  {-# BUILTIN REFL idp #-}

  transport : ∀{i j} {A : Set i} (P : A → Set j) {a₀ a₁ : A} (p : a₀ == a₁) → P a₀ → P a₁
  transport P idp x = x

  sym : ∀ {i} {A : Set i} {a₀ a₁ : A} (p : a₀ == a₁) → a₁ == a₀
  sym idp = idp

  etrans : ∀ {i} {A : Set i} {a₀ a₁ a₂ : A} → a₀ == a₁ → a₁ == a₂ → a₀ == a₂
  etrans idp idp = idp

  proof-irrelevance : ∀ {a} {A : Set a} {x y : A} (p q : x == y) → p == q
  proof-irrelevance idp idp = idp

  elimtransport : ∀{i j} {A : Set i} (P : A → Set j) {a₀ a₁ : A} (p : a₀ == a₁) (q : a₀ == a₁) (r : p == q)  (x : P a₀) → transport P p x == transport P q x
  elimtransport P p .p idp x = idp

  tr! : ∀{i j} {A : Set i} (P : A → Set j) {a₀ a₁ : A} (p : a₀ == a₁) (q : a₀ == a₁) (x : P a₀) → transport P p x == transport P q x
  tr! P p q x = elimtransport P p q (proof-irrelevance p q) x

  tr² : ∀{i j} {A : Set i} (P : A → Set j) {a₀ a₁ a₂ : A} (p : a₀ == a₁) (q : a₁ == a₂) (x : P a₀) → transport P q (transport P p x) == transport P (etrans p q) x
  tr² P idp idp x = idp

  tr³ : ∀{i j} {A : Set i} (P : A → Set j) {a₀ a₁ a₂ a₃ : A} (p₀ : a₀ == a₁) (p₁ : a₁ == a₂) (p₂ : a₂ == a₃) (x : P a₀) → transport P p₂ (transport P p₁ (transport P p₀ x)) == transport P (etrans p₀ (etrans p₁ p₂)) x
  tr³ P idp idp idp x = idp

  tr⁴ : ∀{i j} {A : Set i} (P : A → Set j) {a₀ a₁ a₂ a₃ a₄ : A} (p₀ : a₀ == a₁) (p₁ : a₁ == a₂) (p₂ : a₂ == a₃) (p₃ : a₃ == a₄) (x : P a₀) → transport P p₃ (transport P p₂ (transport P p₁ (transport P p₀ x))) == transport P (etrans p₀ (etrans p₁ (etrans p₂ p₃))) x
  tr⁴ P idp idp idp idp x = idp

  hfiber : ∀ {i} {A B : Set i} (f : A → B) (b : B) → Set i
  hfiber {A = A} f b = Σ A (λ a → f a == b)

  PathOver : ∀ {i j} {A : Set i} (B : A → Set j) {a₀ a₁ : A} (p : a₀ == a₁) (b₉ : B a₀) (b₁ : B a₁) → Set j
  PathOver B idp b₀ b₁ = b₀ == b₁

  infix 30 PathOver
  syntax PathOver B p u v =
    u == v [ B ↓ p ]

  Σ-r : ∀ {i j k} {A : Set i} {B : A → Set j} (C : Σ A B → Set k) → A → Set (j ⊔ k)
  Σ-r {A = A} {B = B} C a = Σ (B a) (λ b → C (a , b))

  Σ-in : ∀ {i j k} {A : Set i} {B : A → Set j} (C : (a : A) → B a → Set k) → A → Set (j ⊔ k)
  Σ-in {A = A} {B = B} C a = Σ (B a) (λ b → C a b)

  infix 30 _↦_

  postulate
    _↦_ : ∀ {i} {A : Set i} → A → A → Set i

  {-# BUILTIN REWRITE _↦_ #-}

  data bool : Set where
    true  : bool
    false : bool

  data ⊥ : Set where

  if_then_else : ∀ {a} {A : Set a} →  bool → A → A → A
  if true then A else B = A
  if false then A else B = B

  _≤_ : ℕ → ℕ → bool
  O ≤ n₁ = true
  S n₀ ≤ O = false
  S n₀ ≤ S n₁ = n₀ ≤ n₁

  min : ℕ → ℕ → ℕ
  min n₀ n₁ with n₀ ≤ n₁
  min n₀ n₁ | true = n₀
  min n₀ n₁ | false = n₁

  ≤S : ∀ (n₀ n₁ : ℕ) → (n₀ ≤ n₁) == true → (n₀ ≤ S n₁) == true
  ≤S O n₁ x = idp
  ≤S (S n₀) O ()
  ≤S (S n₀) (S n₁) x = ≤S n₀ n₁ x

  S≤S : ∀ (n₀ n₁ : ℕ) → (n₀ ≤ n₁) == true → (S n₀ ≤ S n₁) == true
  S≤S n₀ n₁ x = x

max_stars_repo_name: ThiBen/catt

max_issues_repo_name: thibautbenjamin/catt

max_forks_repo_name: thibautbenjamin/catt


text:
-- Andreas, 2021-08-19, issue #5291 reported by gergoerdi
-- https://stackoverflow.com/q/66816547/477476

open import Agda.Builtin.Char
open import Agda.Builtin.String

works : Char
works = '\SOH'

-- This used to fail as the matcher was committed to finding SOH after SO.
-- (Worked only for prefix-free matching.)

test : Char
test = '\SO'

-- Here, all the silly legacy ASCII escape sequences in their glorious detail...

all : String
all = "\NUL\SOH\STX\ETX\EOT\ENQ\ACK\BEL\BS\HT\LF\VT\FF\CR\SO\SI\DEL\DLE\DC1\DC2\DC3\DC4\NAK\SYN\ETB\CAN\EM\SUB\ESC\FS\GS\RS\US"

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Bicategory.Monad.Properties where

open import Categories.Category
open import Categories.Bicategory.Instance.Cats
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.Functor using (Functor)

import Categories.Bicategory.Monad as BicatMonad
import Categories.Monad as ElemMonad

import Categories.Morphism.Reasoning as MR

--------------------------------------------------------------------------------
-- Bicategorical Monads in Cat are the same as the more elementary
-- definition of Monads.

CatMonad⇒Monad : ∀ {o ℓ e} → (T : BicatMonad.Monad (Cats o ℓ e)) → ElemMonad.Monad (BicatMonad.Monad.C T)
CatMonad⇒Monad T = record
  { F = T.T
  ; η = T.η
  ; μ = T.μ
  ; assoc = λ {X} → begin
    η T.μ X ∘ F₁ T.T (η T.μ X)               ≈⟨ intro-ids ⟩
    (η T.μ X ∘ (F₁ T.T (η T.μ X) ∘ id) ∘ id) ≈⟨ T.assoc ⟩
    (η T.μ X ∘ F₁ T.T id ∘ η T.μ (F₀ T.T X)) ≈⟨ ∘-resp-≈ʳ (∘-resp-≈ˡ (identity T.T) ○ identityˡ) ⟩
    η T.μ X ∘ η T.μ (F₀ T.T X)               ∎
  ; sym-assoc = λ {X} → begin
    η T.μ X ∘ η T.μ (F₀ T.T X)                    ≈⟨ intro-F-ids ⟩
    η T.μ X ∘ (F₁ T.T id ∘ η T.μ (F₀ T.T X)) ∘ id ≈⟨ T.sym-assoc ⟩
    η T.μ X ∘ F₁ T.T (η T.μ X) ∘ id               ≈⟨ ∘-resp-≈ʳ identityʳ ⟩
    η T.μ X ∘ F₁ T.T (η T.μ X)                    ∎
  ; identityˡ = λ {X} → begin
    η T.μ X ∘ F₁ T.T (η T.η X)             ≈⟨ intro-ids ⟩
    η T.μ X ∘ (F₁ T.T (η T.η X) ∘ id) ∘ id ≈⟨ T.identityˡ ⟩
    id                                     ∎
  ; identityʳ = λ {X} → begin
    η T.μ X ∘ η T.η (F₀ T.T X)                    ≈⟨ intro-F-ids ⟩
    η T.μ X ∘ (F₁ T.T id ∘ η T.η (F₀ T.T X)) ∘ id ≈⟨ T.identityʳ ⟩
    id                                            ∎
  }
  where
    module T = BicatMonad.Monad T
    open Category (BicatMonad.Monad.C T)
    open HomReasoning
    open Equiv
    open MR (BicatMonad.Monad.C T)

    open NaturalTransformation
    open Functor

    intro-ids : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} → f ∘ g ≈ f ∘ (g ∘ id) ∘ id
    intro-ids = ⟺ (∘-resp-≈ʳ identityʳ) ○ ⟺ (∘-resp-≈ʳ identityʳ)

    intro-F-ids : ∀ {X Y Z} {f : F₀ T.T Y ⇒ Z} {g : X ⇒ F₀ T.T Y} → f ∘ g ≈ f ∘ (F₁ T.T id ∘ g) ∘ id
    intro-F-ids = ∘-resp-≈ʳ (⟺ identityˡ ○  ⟺ (∘-resp-≈ˡ (identity T.T))) ○ ⟺ (∘-resp-≈ʳ identityʳ)

Monad⇒CatMonad : ∀ {o ℓ e} {𝒞 : Category o ℓ e} → (T : ElemMonad.Monad 𝒞) → BicatMonad.Monad (Cats o ℓ e)
Monad⇒CatMonad {𝒞 = 𝒞} T = record
  { C = 𝒞
  ; T = T.F
  ; η = T.η
  ; μ = T.μ
  ; assoc = λ {X} → begin
    T.μ.η X ∘ (T.F.F₁ (T.μ.η X) ∘ id) ∘ id ≈⟨ eliminate-ids ⟩
    T.μ.η X ∘ T.F.F₁ (T.μ.η X)             ≈⟨ T.assoc ⟩
    T.μ.η X ∘ T.μ.η (T.F.F₀ X)             ≈⟨ ∘-resp-≈ʳ (⟺ identityˡ ○ ∘-resp-≈ˡ (⟺ T.F.identity)) ⟩
    T.μ.η X ∘ T.F.F₁ id ∘ T.μ.η (T.F.F₀ X) ∎
  ; sym-assoc = λ {X} → begin
    T.μ.η X ∘ (T.F.F₁ id ∘ T.μ.η (T.F.F₀ X)) ∘ id ≈⟨ eliminate-F-ids ⟩
    T.μ.η X ∘ T.μ.η (T.F.F₀ X)                    ≈⟨ T.sym-assoc ⟩
    T.μ.η X ∘ T.F.F₁ (T.μ.η X)                    ≈⟨ ∘-resp-≈ʳ (⟺ identityʳ) ⟩
    T.μ.η X ∘ T.F.F₁ (T.μ.η X) ∘ id               ∎
  ; identityˡ = λ {X} → begin
    T.μ.η X ∘ (T.F.F₁ (T.η.η X) ∘ id) ∘ id ≈⟨ eliminate-ids ⟩
    T.μ.η X ∘ T.F.F₁ (T.η.η X)             ≈⟨ T.identityˡ ⟩
    id                                     ∎
  ; identityʳ = λ {X} → begin
    (T.μ.η X ∘ (T.F.F₁ id ∘ T.η.η (T.F.F₀ X)) ∘ id) ≈⟨ eliminate-F-ids ⟩
    T.μ.η X ∘ T.η.η (T.F.F₀ X)                      ≈⟨ T.identityʳ ⟩
    id                                              ∎
  }
  where
    module T = ElemMonad.Monad T
    open Category 𝒞
    open HomReasoning
    open MR 𝒞

    eliminate-ids : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} →  f ∘ (g ∘ id) ∘ id ≈ f ∘ g
    eliminate-ids = ∘-resp-≈ʳ identityʳ ○ ∘-resp-≈ʳ identityʳ

    eliminate-F-ids : ∀ {X Y Z} {f : T.F.F₀ Y ⇒ Z} {g : X ⇒ T.F.F₀ Y} →  f ∘ (T.F.F₁ id ∘ g) ∘ id ≈ f ∘ g
    eliminate-F-ids = ∘-resp-≈ʳ identityʳ ○ ∘-resp-≈ʳ (∘-resp-≈ˡ T.F.identity ○ identityˡ)


text:
module vtv where

open import Function.Base
open import Data.Unit.Base
open import Agda.Builtin.Nat
open import Data.Integer
open import Data.Product
open import Agda.Builtin.String
open import Data.List
open import Data.Bool
open import Data.Maybe.Base
  using (just)
  using (nothing)
open import Agda.Builtin.Coinduction
import IO.Primitive as Prim
open import IO
  renaming (_>>=_ to _>>>=_)
  renaming (_>>_ to _>>>_)
open import verify
  using (parse-verify)
open import Codata.Musical.Colist
  renaming (length to length*)
  renaming (map to map*)
  renaming ([_] to [_]*)
  renaming (_∷_ to _∷*_)
  renaming (_++_ to _++*_)
open import Codata.Musical.Costring
open import Data.Bool using (if_then_else_)
open import basic using (Chars)

postulate
  prim-get-args : Prim.IO (List String)
  prim-exit-failure : Prim.IO ⊤

{-# FOREIGN GHC import qualified System.Environment as Env #-}
{-# FOREIGN GHC import Data.Text #-}
{-# FOREIGN GHC import qualified System.Exit #-}
{-# COMPILE GHC prim-get-args = fmap (fmap pack) Env.getArgs #-}
{-# COMPILE GHC prim-exit-failure = System.Exit.exitFailure #-}

exit-failure : IO ⊤
exit-failure = lift prim-exit-failure

_>>=_ : {A : Set} {B : Set} → IO A → (A → IO B) → IO B
_>>=_ f g = ♯ f >>>= \ x → ♯ (g x)

_>>_  : {A : Set} {B : Set} →  IO A → IO B → IO B
_>>_ f g = ♯ f >>> ♯ g

skip : IO ⊤
skip = lift (Prim.return tt)

get-args : IO (List String)
get-args = lift prim-get-args

put-str-ln : String → IO ⊤
put-str-ln s = putStr s >> (putStr "\n" >> skip)

costring-to-chars : Costring → Chars
costring-to-chars (c ∷* cs) = c ∷ costring-to-chars (♭ cs)
costring-to-chars _ = []

-- print-result : Res ⊤ → IO ⊤
-- print-result (cont tt x) = put-str-ln "Proof verified (kernel = ATTV)."
-- print-result (stop s) = do
--   putStr "Invalid proof : "
--   put-str-ln s
--   exit-failure

print-result : Bool → IO ⊤
print-result true = put-str-ln "Proof verified by VTV."
print-result false = do
  putStr "Invalid proof"
  exit-failure

io-verify : IO ⊤
io-verify = do
  (pn ∷ _) ← get-args
    where _ → (put-str-ln "Missing proof file name." >> exit-failure)
  ps ← getContents
  cs ← readFiniteFile pn >>= (return ∘ primStringToList)
  print-result (parse-verify (costring-to-chars ps) cs)

main : Prim.IO ⊤
main = run io-verify

max_stars_repo_name: skbaek/tesc

max_issues_repo_name: skbaek/tesc

max_forks_repo_name: skbaek/tesc


text:
------------------------------------------------------------------------
-- Pushouts, defined using a HIT
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- This module follows the HoTT book rather closely.

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining pushouts uses path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Pushout
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (id; _∘_)
import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import Pointed-type equality-with-J using (Pointed-type)
import Suspension eq as S

private
  variable
    a b l ℓ m p r : Level
    A B           : Type a
    S             : A

-- Spans.

record Span l r m : Type (lsuc (l ⊔ r ⊔ m)) where
  field
    {Left}   : Type l
    {Right}  : Type r
    {Middle} : Type m
    left     : Middle → Left
    right    : Middle → Right

-- Pushouts.

data Pushout (S : Span l r m) : Type (l ⊔ r ⊔ m) where
  inl   : Span.Left  S → Pushout S
  inr   : Span.Right S → Pushout S
  glueᴾ : (x : Span.Middle S) →
          inl (Span.left S x) P.≡ inr (Span.right S x)

-- Glue.

glue : (x : Span.Middle S) →
       _≡_ {A = Pushout S} (inl (Span.left S x)) (inr (Span.right S x))
glue x = _↔_.from ≡↔≡ (glueᴾ x)

-- A dependent eliminator, expressed using paths.

elimᴾ :
  {S : Span l r m} (open Span S)
  (P : Pushout S → Type p)
  (h₁ : (x : Left) → P (inl x))
  (h₂ : (x : Right) → P (inr x)) →
  (∀ x → P.[ (λ i → P (glueᴾ x i)) ] h₁ (left x) ≡ h₂ (right x)) →
  (x : Pushout S) → P x
elimᴾ P h₁ h₂ g = λ where
  (inl x)     → h₁ x
  (inr x)     → h₂ x
  (glueᴾ x i) → g x i

-- A non-dependent eliminator.

recᴾ :
  {S : Span l r m} (open Span S)
  (h₁ : Left → A)
  (h₂ : Right → A) →
  (∀ x → h₁ (left x) P.≡ h₂ (right x)) →
  Pushout S → A
recᴾ = elimᴾ _

-- A dependent eliminator.

elim :
  {S : Span l r m} (open Span S)
  (P : Pushout S → Type p)
  (h₁ : (x : Left) → P (inl x))
  (h₂ : (x : Right) → P (inr x)) →
  (∀ x → subst P (glue x) (h₁ (left x)) ≡ h₂ (right x)) →
  (x : Pushout S) → P x
elim P h₁ h₂ g = elimᴾ P h₁ h₂ (subst≡→[]≡ ∘ g)

elim-glue :
  {S : Span l r m} (open Span S) {P : Pushout S → Type p}
  {h₁ : (x : Left) → P (inl x)}
  {h₂ : (x : Right) → P (inr x)}
  {g : ∀ x → subst P (glue x) (h₁ (left x)) ≡ h₂ (right x)}
  {x : Middle} →
  dcong (elim P h₁ h₂ g) (glue x) ≡ g x
elim-glue = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

rec :
  {S : Span l r m} (open Span S)
  (h₁ : Left → A)
  (h₂ : Right → A) →
  (∀ x → h₁ (left x) ≡ h₂ (right x)) →
  Pushout S → A
rec h₁ h₂ g = recᴾ h₁ h₂ (_↔_.to ≡↔≡ ∘ g)

rec-glue :
  {S : Span l r m} (open Span S)
  {h₁ : Left → A} {h₂ : Right → A}
  {g : ∀ x → h₁ (left x) ≡ h₂ (right x)}
  {x : Middle} →
  cong (rec h₁ h₂ g) (glue x) ≡ g x
rec-glue = cong-≡↔≡ (refl _)

-- Cocones.

Cocone : Span l r m → Type a → Type (a ⊔ l ⊔ r ⊔ m)
Cocone S A =
  ∃ λ (left  : Left  → A) →
  ∃ λ (right : Right → A) →
    (x : Middle) → left (Span.left S x) ≡ right (Span.right S x)
  where
  open Span S using (Left; Right; Middle)

-- Some projection functions for cocones.

module Cocone (c : Cocone S A) where
  open Span S using (Left; Right; Middle)

  left : Left → A
  left = proj₁ c

  right : Right → A
  right = proj₁ (proj₂ c)

  left-left≡right-right :
    (x : Middle) → left (Span.left S x) ≡ right (Span.right S x)
  left-left≡right-right = proj₂ (proj₂ c)

-- A universal property for pushouts.

Pushout→↔Cocone : (Pushout S → A) ↔ Cocone S A
Pushout→↔Cocone {S = S} {A = A} = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to-from
    }
  ; left-inverse-of = from-to
  }
  where
  open Span S

  to : (Pushout S → A) → Cocone S A
  to f = f ∘ inl , f ∘ inr , cong f ∘ glue

  from : Cocone S A → (Pushout S → A)
  from c = rec
    (Cocone.left c)
    (Cocone.right c)
    (Cocone.left-left≡right-right c)

  to-from : ∀ c → to (from c) ≡ c
  to-from c = cong (λ x → _ , _ , x) $ ⟨ext⟩ λ x →
    cong (from c) (glue x)            ≡⟨ rec-glue ⟩∎
    Cocone.left-left≡right-right c x  ∎

  from-to : ∀ f → from (to f) ≡ f
  from-to f = ⟨ext⟩ $ elim
    _
    (λ _ → refl _)
    (λ _ → refl _)
    (λ x →
       subst (λ y → from (to f) y ≡ f y) (glue x) (refl _)                    ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (from (to f)) (glue x)))
         (trans (refl _) (cong f (glue x)))                                   ≡⟨ cong (trans _) $ trans-reflˡ _ ⟩

       trans (sym (cong (from (to f)) (glue x))) (cong f (glue x))            ≡⟨ cong (λ eq → trans (sym eq) (cong f (glue x))) rec-glue ⟩

       trans (sym (Cocone.left-left≡right-right (to f) x)) (cong f (glue x))  ≡⟨⟩

       trans (sym (cong f (glue x))) (cong f (glue x))                        ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                                 ∎)

-- Joins.

Join : Type a → Type b → Type (a ⊔ b)
Join A B = Pushout (record
  { Middle = A × B
  ; left   = proj₁
  ; right  = proj₂
  })

-- Join is symmetric.

Join-symmetric : Join A B ≃ Join B A
Join-symmetric = Eq.↔→≃
  to
  to
  to-to
  to-to
  where
  to : Join A B → Join B A
  to = rec inr inl (sym ∘ glue ∘ swap)

  to-to : (x : Join A B) → to (to x) ≡ x
  to-to =
    elim _ (λ _ → refl _) (λ _ → refl _)
      (λ p →
         subst (λ x → to (to x) ≡ x) (glue p) (refl _)         ≡⟨ subst-in-terms-of-trans-and-cong ⟩

         trans (sym (cong (to ∘ to) (glue p)))
           (trans (refl _) (cong id (glue p)))                 ≡⟨ cong₂ (trans ∘ sym)
                                                                    (sym $ cong-∘ _ _ _)
                                                                    (trans (trans-reflˡ _) $
                                                                     sym $ cong-id _) ⟩

         trans (sym (cong to (cong to (glue p)))) (glue p)     ≡⟨ cong (flip trans _) $ cong (sym ∘ cong to) rec-glue ⟩

         trans (sym (cong to (sym (glue (swap p))))) (glue p)  ≡⟨ cong (flip trans _) $ cong sym $ cong-sym _ _ ⟩

         trans (sym (sym (cong to (glue (swap p))))) (glue p)  ≡⟨ cong (flip trans _) $ sym-sym _ ⟩

         trans (cong to (glue (swap p))) (glue p)              ≡⟨ cong (flip trans _) rec-glue ⟩

         trans (sym (glue (swap (swap p)))) (glue p)           ≡⟨⟩

         trans (sym (glue p)) (glue p)                         ≡⟨ trans-symˡ _ ⟩∎

         refl _                                                ∎)

-- The empty type is a right identity for Join.

Join-⊥ʳ : Join A (⊥ {ℓ = ℓ}) ≃ A
Join-⊥ʳ = Eq.↔→≃
  (rec id ⊥-elim (λ { (_ , ()) }))
  inl
  refl
  (elim _ (λ _ → refl _) (λ ()) (λ { (_ , ()) }))

-- The empty type is a left identity for Join.

Join-⊥ˡ : Join (⊥ {ℓ = ℓ}) A ≃ A
Join-⊥ˡ {A = A} =
  Join ⊥ A  ↝⟨ Join-symmetric ⟩
  Join A ⊥  ↝⟨ Join-⊥ʳ ⟩□
  A         □

-- Cones.

Cone : {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Cone f = Pushout (record
  { Left  = ⊤
  ; right = f
  })

-- Wedges.

Wedge : Pointed-type a → Pointed-type b → Type (a ⊔ b)
Wedge (A , a) (B , b) =
  Pushout (record
    { Middle = ⊤
    ; left   = const a
    ; right  = const b
    })

-- Smash products.

Smash-product : Pointed-type a → Pointed-type b → Type (a ⊔ b)
Smash-product PA@(A , a) PB@(B , b) = Cone f
  where
  f : Wedge PA PB → A × B
  f = rec (_, b) (a ,_) (λ _ → refl _)

-- Suspensions.

Susp : Type a → Type a
Susp A = Pushout (record
  { Left   = ⊤
  ; Middle = A
  ; Right  = ⊤
  })

-- These suspensions are equivalent to the ones defined in Suspension.

Susp≃Susp : Susp A ≃ S.Susp A
Susp≃Susp = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  })
  where
  to : Susp A → S.Susp A
  to = recᴾ (λ _ → S.north) (λ _ → S.south) S.meridianᴾ

  from : S.Susp A → Susp A
  from = S.recᴾ (inl _) (inr _) glueᴾ

  to∘from : ∀ x → to (from x) ≡ x
  to∘from =
    _↔_.from ≡↔≡ ∘
    S.elimᴾ _ P.refl P.refl (λ a i _ → S.meridianᴾ a i)

  from∘to : ∀ x → from (to x) ≡ x
  from∘to =
    _↔_.from ≡↔≡ ∘
    elimᴾ _ (λ _ → P.refl) (λ _ → P.refl) (λ a i _ → glueᴾ a i)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import MJ.Types
import MJ.Classtable.Core as Core

module MJ.Syntax.Program {c}(Ct : Core.Classtable c) where

open import Prelude
open import Data.List

open import MJ.Classtable.Code Ct
open import MJ.Syntax Ct

Prog : Ty c → Set
Prog a = Code × (Body [] a)


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

open import Cubical.Core.Everything

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

open import Cubical.Data.Nat
open import Cubical.Data.Unit.Base

isPropUnit : isProp Unit
isPropUnit _ _ i = tt

isContrUnit : isContr Unit
isContrUnit = tt , λ {tt → refl}

isOfHLevelUnit : (n : ℕ) → isOfHLevel n Unit
isOfHLevelUnit 0       = isContrUnit
isOfHLevelUnit 1       = isPropUnit
isOfHLevelUnit (suc n) = hLevelSuc n Unit (isOfHLevelUnit n)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
------------------------------------------------------------------------------
-- FOCT terms properties
------------------------------------------------------------------------------

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

module FOTC.Base.PropertiesATP where

open import FOTC.Base

------------------------------------------------------------------------------
-- Injective properties

postulate succInjective : ∀ {m n} → succ₁ m ≡ succ₁ n → m ≡ n
{-# ATP prove succInjective #-}

------------------------------------------------------------------------------
-- Discrimination rules

postulate S≢0 : ∀ {n} → succ₁ n ≢ zero
{-# ATP prove S≢0 #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.LogicalRelation

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Reducible types are well-formed.
escape : ∀ {l Γ A} → Γ ⊩⟨ l ⟩ A → Γ ⊢ A
escape (Uᵣ′ l′ l< ⊢Γ) = Uⱼ ⊢Γ
escape (ℕᵣ [ ⊢A , ⊢B , D ]) = ⊢A
escape (Emptyᵣ [ ⊢A , ⊢B , D ]) = ⊢A
escape (Unitᵣ [ ⊢A , ⊢B , D ]) = ⊢A
escape (ne′ K [ ⊢A , ⊢B , D ] neK K≡K) = ⊢A
escape (Bᵣ′ W F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext) = ⊢A
escape (emb 0<1 A) = escape A

-- Reducible type equality respect the equality relation.
escapeEq : ∀ {l Γ A B} → ([A] : Γ ⊩⟨ l ⟩ A)
            → Γ ⊩⟨ l ⟩ A ≡ B / [A]
            → Γ ⊢ A ≅ B
escapeEq (Uᵣ′ l′ l< ⊢Γ) PE.refl = ≅-Urefl ⊢Γ
escapeEq (ℕᵣ [ ⊢A , ⊢B , D ]) D′ = ≅-red D D′ ℕₙ ℕₙ (≅-ℕrefl (wf ⊢A))
escapeEq (Emptyᵣ [ ⊢A , ⊢B , D ]) D′ = ≅-red D D′ Emptyₙ Emptyₙ (≅-Emptyrefl (wf ⊢A))
escapeEq (Unitᵣ [ ⊢A , ⊢B , D ]) D′ = ≅-red D D′ Unitₙ Unitₙ (≅-Unitrefl (wf ⊢A))
escapeEq (ne′ K D neK K≡K) (ne₌ M D′ neM K≡M) =
  ≅-red (red D) (red D′) (ne neK) (ne neM) (~-to-≅ K≡M)
escapeEq (Bᵣ′ W F G D ⊢F ⊢G A≡A [F] [G] G-ext)
             (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ≅-red (red D) D′ ⟦ W ⟧ₙ ⟦ W ⟧ₙ A≡B
escapeEq (emb 0<1 A) A≡B = escapeEq A A≡B

-- Reducible terms are well-formed.
escapeTerm : ∀ {l Γ A t} → ([A] : Γ ⊩⟨ l ⟩ A)
              → Γ ⊩⟨ l ⟩ t ∷ A / [A]
              → Γ ⊢ t ∷ A
escapeTerm (Uᵣ′ l′ l< ⊢Γ) (Uₜ A [ ⊢t , ⊢u , d ] typeA A≡A [A]) = ⊢t
escapeTerm (ℕᵣ D) (ℕₜ n [ ⊢t , ⊢u , d ] t≡t prop) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (Emptyᵣ D) (Emptyₜ e [ ⊢t , ⊢u , d ] t≡t prop) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (Unitᵣ D) (Unitₜ e [ ⊢t , ⊢u , d ] prop) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (ne′ K D neK K≡K) (neₜ k [ ⊢t , ⊢u , d ] nf) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
               (Πₜ f [ ⊢t , ⊢u , d ] funcF f≡f [f] [f]₁) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
               (Σₜ p [ ⊢t , ⊢u , d ] pProd p≅p [fst] [snd]) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (emb 0<1 A) t = escapeTerm A t

-- Reducible term equality respect the equality relation.
escapeTermEq : ∀ {l Γ A t u} → ([A] : Γ ⊩⟨ l ⟩ A)
                → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
                → Γ ⊢ t ≅ u ∷ A
escapeTermEq (Uᵣ′ l′ l< ⊢Γ) (Uₜ₌ A B d d′ typeA typeB A≡B [A] [B] [A≡B]) =
  ≅ₜ-red (id (Uⱼ ⊢Γ)) (redₜ d) (redₜ d′) Uₙ (typeWhnf typeA) (typeWhnf typeB) A≡B
escapeTermEq (ℕᵣ D) (ℕₜ₌ k k′ d d′ k≡k′ prop) =
  let natK , natK′ = split prop
  in  ≅ₜ-red (red D) (redₜ d) (redₜ d′) ℕₙ
             (naturalWhnf natK) (naturalWhnf natK′) k≡k′
escapeTermEq (Emptyᵣ D) (Emptyₜ₌ k k′ d d′ k≡k′ prop) =
  let natK , natK′ = esplit prop
  in  ≅ₜ-red (red D) (redₜ d) (redₜ d′) Emptyₙ
             (ne natK) (ne natK′) k≡k′
escapeTermEq {l} {Γ} {A} {t} {u} (Unitᵣ D) (Unitₜ₌ ⊢t ⊢u) =
  let t≅u = ≅ₜ-η-unit ⊢t ⊢u
      A≡Unit = subset* (red D)
  in  ≅-conv t≅u (sym A≡Unit)
escapeTermEq (ne′ K D neK K≡K)
                 (neₜ₌ k m d d′ (neNfₜ₌ neT neU t≡u)) =
  ≅ₜ-red (red D) (redₜ d) (redₜ d′) (ne neK) (ne neT) (ne neU)
         (~-to-≅ₜ t≡u)
escapeTermEq (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                 (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
  ≅ₜ-red (red D) (redₜ d) (redₜ d′) Πₙ (functionWhnf funcF) (functionWhnf funcG) f≡g
escapeTermEq (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                 (Σₜ₌ p r d d′ pProd rProd p≅r [t] [u] [fstp] [fstr] [fst≡] [snd≡]) =
  ≅ₜ-red (red D) (redₜ d) (redₜ d′) Σₙ (productWhnf pProd) (productWhnf rProd) p≅r
escapeTermEq (emb 0<1 A) t≡u = escapeTermEq A t≡u


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.CumulativeHierarchy where

open import Cubical.HITs.CumulativeHierarchy.Base public
  hiding (elim; elimProp)
open import Cubical.HITs.CumulativeHierarchy.Properties public
open import Cubical.HITs.CumulativeHierarchy.Constructions public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2018-06-18, problem surfaced with issue #3136
-- Correct printing of a pattern lambda that has no patterns.

-- {-# OPTIONS -v extendedlambda:50 #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

record R : Set where
  no-eta-equality
  field w : Bool

f : R
f = λ where
  .R.w → λ where
    → false

triggerError : ∀ x → x ≡ f
triggerError x = refl

-- Error prints extended lambda name in error:
-- x != λ { .R.w → λ { .extendedlambda1 → false } } of type R
-- when checking that the expression refl has type x ≡ f

-- Expected:
-- x != λ { .R.w → λ { → false } } of type R
-- when checking that the expression refl has type x ≡ f


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

open import Prelude
open import Relation.Binary

module Data.AVLTree.Mapping {k} {K : Type k} {r₁ r₂} (totalOrder : TotalOrder K r₁ r₂) where

open import Relation.Binary.Construct.Bounded totalOrder
open import Data.Nat using (_+_)
open TotalOrder totalOrder using (_<?_; compare)
open TotalOrder b-ord using (<-trans) renaming (refl to <-refl)
import Data.Empty.UniversePolymorphic as Poly

open import Data.AVLTree.Internal totalOrder

private
  variable
    n m : ℕ
    v : Level
    Val : K → Type v

data Mapping (Val : K → Type v) : Type (k ℓ⊔ v ℓ⊔ r₁) where
  [_] : Tree Val [⊥] [⊤] n → Mapping Val
  quot : (xs : Tree Val [⊥] [⊤] n) (ys : Tree Val [⊥] [⊤] m) → toList xs ≡ toList ys → [ xs ] ≡ [ ys ]
  trunc : isSet (Mapping Val)

lookup′ : (x : K) → Mapping Val → Maybe (Val x)
lookup′ x [ xs ] = lookup x xs
lookup′ x (quot xs ys p j) = {!!}
lookup′ x (trunc xs xs₁ x₁ y i i₁) = {!!}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground