text:
module With where

open import Reflection
open import Function using (_∘_ ; _$_ ; _∋_ ; id ; const)
open import Data.List
open import Data.Nat hiding (_+_)
open import Relation.Binary using (Setoid ; Decidable)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality hiding ( [_] ; subst )

open import Helper.CodeGeneration

{-# TERMINATING #-}
mutual

  s_arg : (n : ℕ) -> (ℕ -> Term -> Term) -> Arg Term -> Arg Term
  s_arg n f (arg i x) = arg i (s_term' n f x)

  s_type : (n : ℕ) -> (ℕ -> Term -> Term) -> Type -> Type
  s_type n f (el s t) = el s (s_term' n f t)

  s_term : (n : ℕ) -> (ℕ -> Term -> Term) -> Term -> Term
  s_term n f (var x args) = var x (map (s_arg n f) args)
  s_term n f (con c args) = con c (map (s_arg n f) args)
  s_term n f (def f₁ args) = def f₁ (map (s_arg n f) args)
  s_term n f (lam v (abs s x)) = lam v (abs s (s_term' n f x))
  s_term n f (pat-lam cs args) = pat-lam cs (map (s n arg f) args)
  s_term n f (pi (arg i x) (abs s x₁)) = pi (arg i (s_type n f x)) (abs s (s_type n f x₁))
  s_term n f t = t

  s_term' : (n : ℕ) -> (ℕ -> Term -> Term) -> Term -> Term
  s_term' n f t = f n (s_term n f t)

inc_debruijn_indices : Term -> Term
inc_debruijn_indices t = s_term' zero alg t
  where
    alg : ℕ -> Term -> Term
    alg n (var x args) = var (suc x) args
    alg n t2 = t2

subst : Term -> Term -> Term -> Term
subst t ti to = s_term' zero alg t
  where
    alg : ℕ -> Term -> Term
    alg n ti1 with ti Reflection.≟ ti1
    alg n ti1 | yes p = to
    alg n ti1 | no ¬p = ti1

getType : {T : Set} -> (t : T) -> Term
getType {T} t = quoteTerm T

with' : Term -> Term -> Term
with' w l = quote-goal (abs "g" lam_body)
  where
    sub_term = def (quote subst) ( (a $ var 1 []) ∷ (a $ w) ∷ (a $ quote-term $ var 0 []) ∷ [] )
    lam_type_q = unquote-term sub_term []
    lam_type = pi (a $ t0 unknown) (abs "i" $ t0 $ lam_type_q)
    lam_body = def (quote _$_) ((a $ lam_type ∋-t l) ∷ (a $ inc_debruijn_indices $ unquote-term w []) ∷ [])

postulate
   A     : Set
   _+_   : A → A → A
   T     : A → Set
   mkT   : ∀ x → T x
   P     : ∀ x → T x → Set

-- the type A of the with argument has no free variables, so the with
-- argument will come first
f₁ : (x y : A) (t : T (x + y)) → T (x + y)
f₁ x y t with x + y
f₁ x y t    | w = mkT w

f₂ : (x y : A) → T (x + y)
f₂ x y = unquote (with' (quoteTerm (quoteTerm (x + y))) (quoteTerm (\w -> mkT w)))

  -- def (quote inc_var_indices) [ a $ var 1 [] ] --
    -- sub_term = def (quote subst) ( (a $ var 1 []) ∷ (a $ w) ∷ (a $ (quote-term (var 0 []))) ∷ [] )
    -- lam_type = pi (a $ t0 $ (def (quote _≡_) ((a $ var 3 []) ∷ (a $ var 2 []) ∷ []))) (abs "i" $ t0 $ lam_type_q)

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Graph.Examples where

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

open import Cubical.Data.Empty
open import Cubical.Data.Unit renaming (Unit to ⊤)
open import Cubical.Data.Nat
open import Cubical.Data.SumFin
open import Cubical.Relation.Nullary

open import Cubical.Data.Sum
open import Cubical.Data.Prod

open import Cubical.Data.Graph.Base

-- Some small graphs of common shape

⇒⇐ : Graph ℓ-zero ℓ-zero
Obj ⇒⇐ = Fin 3
Hom ⇒⇐ fzero               (fsuc fzero) = ⊤
Hom ⇒⇐ (fsuc (fsuc fzero)) (fsuc fzero) = ⊤
Hom ⇒⇐ _ _ = ⊥

⇐⇒ : Graph ℓ-zero ℓ-zero
Obj ⇐⇒ = Fin 3
Hom ⇐⇒ (fsuc fzero) fzero               = ⊤
Hom ⇐⇒ (fsuc fzero) (fsuc (fsuc fzero)) = ⊤
Hom ⇐⇒ _ _ = ⊥

-- paralell pair graph
⇉ : Graph ℓ-zero ℓ-zero
Obj ⇉ = Fin 2
Hom ⇉ fzero (fsuc fzero) = Fin 2
Hom ⇉ _ _ = ⊥

-- The graph ω = 0 → 1 → 2 → ···

data Adj : ℕ → ℕ → Type₀ where
  adj : ∀ n → Adj n (suc n)

areAdj : ∀ m n → Dec (Adj m n)
areAdj zero zero          = no λ ()
areAdj zero (suc zero)    = yes (adj zero)
areAdj zero (suc (suc n)) = no λ ()
areAdj (suc m) zero       = no λ ()
areAdj (suc m) (suc n)    = mapDec (λ { (adj .m) → adj (suc m) })
                                   (λ { ¬a (adj .(suc m)) → ¬a (adj m) })
                                   (areAdj m n)

ωGr : Graph ℓ-zero ℓ-zero
Obj ωGr = ℕ
Hom ωGr m n with areAdj m n
... | yes _ = ⊤ -- if n ≡ (suc m)
... | no  _ = ⊥ -- otherwise

record ωDiag ℓ : Type (ℓ-suc ℓ) where
  field
    ωObj : ℕ → Type ℓ
    ωHom : ∀ n → ωObj n → ωObj (suc n)

  asDiag : Diag ℓ ωGr
  asDiag $ n = ωObj n
  _<$>_ asDiag {m} {n} f with areAdj m n
  asDiag <$> tt | yes (adj m) = ωHom m

-- The finite connected subgraphs of ω: 𝟘,𝟙,𝟚,𝟛,...

data AdjFin : ∀ {k} → Fin k → Fin k → Type₀ where
  adj : ∀ {k} (n : Fin k) → AdjFin (finj n) (fsuc n)

adj-fsuc : ∀ {k} {m n : Fin k} → AdjFin (fsuc m) (fsuc n) → AdjFin m n
adj-fsuc {suc k} {.(finj n)} {fsuc n} (adj .(fsuc n)) = adj n

areAdjFin : ∀ {k} (m n : Fin k) → Dec (AdjFin m n)
areAdjFin {suc k}       fzero fzero           = no λ ()
areAdjFin {suc (suc k)} fzero (fsuc fzero)    = yes (adj fzero)
areAdjFin {suc (suc k)} fzero (fsuc (fsuc n)) = no λ ()
areAdjFin {suc k}       (fsuc m) fzero        = no λ ()
areAdjFin {suc k}       (fsuc m) (fsuc n)     = mapDec (λ { (adj m) → adj (fsuc m) })
                                                       (λ { ¬a a → ¬a (adj-fsuc a) })
                                                       (areAdjFin {k} m n)

[_]Gr : ℕ → Graph ℓ-zero ℓ-zero
Obj [ k ]Gr = Fin k
Hom [ k ]Gr m n with areAdjFin m n
... | yes _ = ⊤ -- if n ≡ (suc m)
... | no  _ = ⊥ -- otherwise

𝟘Gr 𝟙Gr 𝟚Gr 𝟛Gr : Graph ℓ-zero ℓ-zero
𝟘Gr = [ 0 ]Gr; 𝟙Gr = [ 1 ]Gr; 𝟚Gr = [ 2 ]Gr; 𝟛Gr = [ 3 ]Gr

record [_]Diag ℓ (k : ℕ) : Type (ℓ-suc ℓ) where
  field
    []Obj : Fin (suc k) → Type ℓ
    []Hom : ∀ (n : Fin k) → []Obj (finj n) → []Obj (fsuc n)

  asDiag : Diag ℓ [ suc k ]Gr
  asDiag $ n = []Obj n
  _<$>_ asDiag {m} {n} f with areAdjFin m n
  _<$>_ asDiag {.(finj n)} {fsuc n} f | yes (adj .n) = []Hom n

-- Disjoint union of graphs

module _ {ℓv ℓe ℓv' ℓe'} where

  _⊎Gr_ : ∀ (G : Graph ℓv ℓe) (G' : Graph ℓv' ℓe') → Graph (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe')
  Obj (G ⊎Gr G') = Obj G ⊎ Obj G'
  Hom (G ⊎Gr G') (inl x) (inl y) = Lift {j = ℓe'} (Hom G x y)
  Hom (G ⊎Gr G') (inr x) (inr y) = Lift {j = ℓe } (Hom G' x y)
  Hom (G ⊎Gr G') _ _ = Lift ⊥

  record ⊎Diag ℓ (G : Graph ℓv ℓe) (G' : Graph ℓv' ℓe')
               : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe'))) where
    field
      ⊎Obj : Obj G ⊎ Obj G' → Type ℓ
      ⊎Homl : ∀ {x y} → Hom G  x y → ⊎Obj (inl x) → ⊎Obj (inl y)
      ⊎Homr : ∀ {x y} → Hom G' x y → ⊎Obj (inr x) → ⊎Obj (inr y)

    asDiag : Diag ℓ (G ⊎Gr G')
    asDiag $ x = ⊎Obj x
    _<$>_ asDiag {inl x} {inl y} f = ⊎Homl (lower f)
    _<$>_ asDiag {inr x} {inr y} f = ⊎Homr (lower f)

-- Cartesian product of graphs

module _ {ℓv ℓe ℓv' ℓe'} where

  -- We need decidable equality in order to define the cartesian product
  DecGraph : ∀ ℓv ℓe → Type (ℓ-suc (ℓ-max ℓv ℓe))
  DecGraph ℓv ℓe = Σ[ G ∈ Graph ℓv ℓe ] Discrete (Obj G)

  _×Gr_ : (G : DecGraph ℓv ℓe) (G' : DecGraph ℓv' ℓe') → Graph (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe')
  Obj (G ×Gr G') = Obj (fst G) × Obj (fst G')
  Hom (G ×Gr G') (x , x') (y , y') with snd G x y | snd G' x' y'
  ... | yes _ | yes _ = Hom (fst G) x y ⊎ Hom (fst G') x' y'
  ... | yes _ | no  _ = Lift {j = ℓe } (Hom (fst G') x' y')
  ... | no  _ | yes _ = Lift {j = ℓe'} (Hom (fst G) x y)
  ... | no  _ | no  _ = Lift ⊥

  record ×Diag ℓ (G : DecGraph ℓv ℓe) (G' : DecGraph ℓv' ℓe')
               : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe'))) where
    field
      ×Obj : Obj (fst G) × Obj (fst G') → Type ℓ
      ×Hom₁ : ∀ {x y} (f : Hom (fst G) x y) (x' : Obj (fst G'))    → ×Obj (x , x') → ×Obj (y , x')
      ×Hom₂ : ∀ (x : Obj (fst G)) {x' y'} (f : Hom (fst G') x' y') → ×Obj (x , x') → ×Obj (x , y')

    asDiag : Diag ℓ (G ×Gr G')
    asDiag $ x = ×Obj x
    _<$>_ asDiag {x , x'} {y , y'} f with snd G x y | snd G' x' y'
    _<$>_ asDiag {x , x'} {y , y'} (inl f) | yes _ | yes p' = subst _ p' (×Hom₁ f x')
    _<$>_ asDiag {x , x'} {y , y'} (inr f) | yes p | yes _  = subst _ p  (×Hom₂ x f )
    _<$>_ asDiag {x , x'} {y , y'} f | yes p | no  _  = subst _ p  (×Hom₂ x (lower f) )
    _<$>_ asDiag {x , x'} {y , y'} f | no  _ | yes p' = subst _ p' (×Hom₁ (lower f) x')

ext: agda

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
open import bool

module list-merge-sort (A : Set) (_<A_ : A → A → 𝔹) where

open import braun-tree A _<A_
open import eq
open import list
open import nat
open import nat-thms

merge : (l1 l2 : 𝕃 A) → 𝕃 A
merge [] ys = ys
merge xs [] = xs
merge (x :: xs) (y :: ys) with x <A y
merge (x :: xs) (y :: ys) | tt = x :: (merge xs (y :: ys))
merge (x :: xs) (y :: ys) | ff = y :: (merge (x :: xs) ys)

merge-sort-h : ∀{n : ℕ} → braun-tree' n → 𝕃 A
merge-sort-h (bt'-leaf a) = [ a ]
merge-sort-h (bt'-node l r p) = merge (merge-sort-h l) (merge-sort-h r)

merge-sort : 𝕃 A → 𝕃 A
merge-sort [] = []
merge-sort (a :: as) with 𝕃-to-braun-tree' a as
merge-sort (a :: as) | t = merge-sort-h t

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed monads
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

module Category.Monad.Indexed where

open import Category.Applicative.Indexed
open import Function
open import Level

record RawIMonad {i f} {I : Set i} (M : IFun I f) :
                 Set (i ⊔ suc f) where
  infixl 1 _>>=_ _>>_ _>=>_
  infixr 1 _=<<_ _<=<_

  field
    return : ∀ {i A} → A → M i i A
    _>>=_  : ∀ {i j k A B} → M i j A → (A → M j k B) → M i k B

  _>>_ : ∀ {i j k A B} → M i j A → M j k B → M i k B
  m₁ >> m₂ = m₁ >>= λ _ → m₂

  _=<<_ : ∀ {i j k A B} → (A → M j k B) → M i j A → M i k B
  f =<< c = c >>= f

  _>=>_ : ∀ {i j k a} {A : Set a} {B C} →
          (A → M i j B) → (B → M j k C) → (A → M i k C)
  f >=> g = _=<<_ g ∘ f

  _<=<_ : ∀ {i j k B C a} {A : Set a} →
          (B → M j k C) → (A → M i j B) → (A → M i k C)
  g <=< f = f >=> g

  join : ∀ {i j k A} → M i j (M j k A) → M i k A
  join m = m >>= id

  rawIApplicative : RawIApplicative M
  rawIApplicative = record
    { pure = return
    ; _⊛_  = λ f x → f >>= λ f' → x >>= λ x' → return (f' x')
    }

  open RawIApplicative rawIApplicative public

record RawIMonadZero {i f} {I : Set i} (M : IFun I f) :
                     Set (i ⊔ suc f) where
  field
    monad : RawIMonad M
    ∅     : ∀ {i j A} → M i j A

  open RawIMonad monad public

record RawIMonadPlus {i f} {I : Set i} (M : IFun I f) :
                     Set (i ⊔ suc f) where
  infixr 3 _∣_
  field
    monadZero : RawIMonadZero M
    _∣_       : ∀ {i j A} → M i j A → M i j A → M i j A

  open RawIMonadZero monadZero public


text:
------------------------------------------------------------------------
-- Raw monads
------------------------------------------------------------------------

-- Note that this module is not parametrised by an axiomatisation of
-- equality. This module is reexported from Monad.

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

module Monad.Raw where

open import Prelude

-- Raw monads.

record Raw-monad {d c} (M : Type d → Type c) : Type (lsuc d ⊔ c) where
  constructor mk
  infixl 6 _⟨$⟩_ _⊛_
  infixl 5 _>>=_ _>>_
  infixr 5 _=<<_
  field
    return : ∀ {A} → A → M A
    _>>=_  : ∀ {A B} → M A → (A → M B) → M B

  -- Variants of _>>=_.

  _>>_ : ∀ {A B} → M A → M B → M B
  x >> y = x >>= const y

  _=<<_ : ∀ {A B} → (A → M B) → M A → M B
  _=<<_ = flip _>>=_

  -- A map function.

  map : ∀ {A B} → (A → B) → M A → M B
  map f x = x >>= return ∘ f

  -- A synonym.

  _⟨$⟩_ : ∀ {A B} → (A → B) → M A → M B
  _⟨$⟩_ = map

  -- Applicative functor application.

  _⊛_ : ∀ {A B} → M (A → B) → M A → M B
  f ⊛ x = f >>= λ f → x >>= λ x → return (f x)

  -- The sequence function (for lists).

  sequence : ∀ {A} → List (M A) → M (List A)
  sequence []       = return []
  sequence (x ∷ xs) = _∷_ ⟨$⟩ x ⊛ sequence xs

open Raw-monad ⦃ … ⦄ public

-- Raw monad transformers.

record Raw-monad-transformer
         {d c₁ c₂} (F : (Type d → Type c₁) → (Type d → Type c₂)) :
         Type (lsuc (c₁ ⊔ d) ⊔ c₂) where
  constructor mk
  field
    transform : ∀ {M}   ⦃ is-raw-monad : Raw-monad M ⦄ → Raw-monad (F M)
    liftʳ     : ∀ {M A} ⦃ is-raw-monad : Raw-monad M ⦄ → M A → F M A

open Raw-monad-transformer ⦃ … ⦄ public using (liftʳ)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Oscar.Data.Vec.Injectivity where

open import Oscar.Data.Equality
open import Oscar.Data.Vec

Vec-head-inj : ∀ {a} {A : Set a} {x₁ x₂ : A} {N} {xs₁ xs₂ : Vec A N} → x₁ ∷ xs₁ ≡ x₂ ∷ xs₂ → x₁ ≡ x₂
Vec-head-inj refl = refl

Vec-tail-inj : ∀ {a} {A : Set a} {x₁ x₂ : A} {N} {xs₁ xs₂ : Vec A N} → x₁ ∷ xs₁ ≡ x₂ ∷ xs₂ → xs₁ ≡ xs₂
Vec-tail-inj refl = refl


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

module old.Sharp where

  open import Basics
  open import Flat

  open import lib.Equivalence2

  {- I want sthing like this
  record ♯ {@♭ l : ULevel} (A : Type l) : Type l where
    constructor _^♯
    field
      _/♯ :{♭} A
  open ♯ publ
-}

  -- Following Licata

  postulate
    -- Given a type A, ♯ A is a type
    ♯ : {i : ULevel} → Type i → Type i

    -- Given an element a : A, we have an element ♯i a : ♯ A
    ♯i : {i : ULevel} {A : Type i} → A → ♯ A

    -- To map out of ♯ A into some type ♯ (B a) depending on it, you may just map out of A.
    ♯-elim : {i j : ULevel} {A : Type i} (B : ♯ A → Type j)
            → ((a : A) → ♯ (B (♯i a)))
            → ((a : ♯ A) → ♯ (B a))

    -- The resulting map out of ♯ A ``computes'' to the original map out of A on ♯i
    ♯-elim-β : {i j : ULevel} {A : Type i} {B : ♯ A → Type j}
               (f : (a : A) → ♯ (B (♯i a))) (a : A)
               → (♯-elim B f (♯i a)) ↦ (f a)
    {-# REWRITE ♯-elim-β #-}

    -- The type of equalities in a codiscrete type are codiscrete
    ♯path : {i : ULevel} {A : Type i} {x y : ♯ A}
            → (♯i {A = x == y}) is-an-equiv

    -- Given a crisp map into ♯ B, we get a cohesive map into it
    -- This encodes the adjunction between ♭ and ♯ on the level of types.
    uncrisp : {@♭ i : ULevel} {j : ULevel} {@♭ A : Type i} (B : A → Type j)
              → ((@♭ a : A) → ♯ (B a))
              → (a : A) → ♯ (B a)

    -- If we uncrispen a function and then apply it to a crisp variable, we get the original result judgementally
    uncrisp-β : {@♭ i : ULevel} {j : ULevel} {@♭ A : Type i} (B : A → Type j)
                → (f : (@♭ a : A) → ♯ (B a))
                → (@♭ a : A) → (uncrisp B f a) ↦ (f a)
    {-# REWRITE uncrisp-β #-}

    -- We can pull crisp elements out of ♯ A
    ♭♯e : {@♭ i : ULevel} {@♭ A : Type i} → ♯ A ::→ A

    -- If we take a crisp element of A, put it into ♯ A, and pull it out again, we get where we were judgementally
    ♭♯β : {@♭ i : ULevel} {@♭ A : Type i} (@♭ a : A)
          → (♭♯e (♯i a)) ↦ a
    {-# REWRITE ♭♯β #-}

    -- If we pull out a crisp element of ♯ A and then put it back in, we get back where we were
    -- Not sure why this isn't judgemental.
    ♭♯η : {@♭ i : ULevel} {@♭ A : Type i} (@♭ a : ♯ A) → a == ♯i (♭♯e a)

    -- We also posulate the half-adjoint needed for this to be a coherent adjunction.
    ♭♯η-▵ : {@♭ i : ULevel} {@♭ A : Type i} (@♭ a : A) → ♭♯η (♯i a) == refl

  ♯path-eq : {i : ULevel} {A : Type i} {x y : ♯ A}
             → (x == y) ≃ (♯ (x == y))
  ♯path-eq = ♯i , ♯path

  ♯-rec : {i j : ULevel} {A : Type i} {B : Type j} →
          (A → ♯ B) → (♯ A → ♯ B)
  ♯-rec {B = B} = ♯-elim (λ _ → B)

{-
  Given a family B : (@♭ a : A) → Type j crisply varying over A,
  we can form the family B' ≡ (λ (@♭ a : A) → ♯ (B a)).

  According to Shulman, we should be able to then get a cohesive variation
  B'' : (a : A) → Type j
  with the property that if (@♭ a : A) , B'' a ≡ B' a

  Or, shorter, from B : (@♭ a : A) → Type j, we should get C : (a : A) → Type j
  with the property that for (@♭ a : A), C a ≡ ♯ (B a)

  The signature of the operation B ↦ C must be ((@♭ a : A) → Type j) → (a : A) → Type j.
  Unfortunately, this doesn't tell us anything about where its landing
-}
  postulate
    ♯' : {@♭ @♭ i : ULevel} {Γ : Type i} {j : ULevel}
         (A : Γ ::→ Type j)
         → Γ → Type j
    ♯'-law : {@♭ @♭ i : ULevel} {Γ : Type i} {j : ULevel}
             (A : Γ ::→ Type j) (@♭ x : Γ)
             → (♯' A) x ↦ ♯ (A x)
    {-# REWRITE ♯'-law #-}

  {-
    Here, we define let notations for ♯ to approximate the upper and lower ♯s
    that Shulman uses in his paper.

    We also define versions of the eliminator and uncrisper that take an implicit family argument, so
    we can use the let notation without explicitly noting the family.
  -}
  syntax ♯-elim B (λ u → t) a = let♯ a :=♯i u in♯ t in-family B
  syntax uncrisp B (λ u → t) a = let♯ a ↓♯:= u in♯ t in-family B

  ♯-elim' : {i j : ULevel} {A : Type i} {B : ♯ A → Type j}
            → ((a : A) → ♯ (B (♯i a)))
            → (a : ♯ A) → ♯ (B a)
  ♯-elim' {B = B} f = ♯-elim B f
  syntax ♯-elim' (λ u → t) a = let♯ a :=♯i u in♯ t

  uncrisp' : {@♭ i : ULevel} {j : ULevel} {@♭ A : Type i} {B : A → Type j}
         → (f : (@♭ a : A) → ♯ (B a))
         → (a : A) → ♯ (B a)
  uncrisp' {B = B} f = uncrisp B f
  syntax uncrisp' (λ u → t) a = let♯ u := a ↓♯in♯ t

  -- A type A is codiscrete if the counit ♯i : A → ♯ A is an equivalence.
  _is-codiscrete : {i : ULevel} (A : Type i) → Type i
  _is-codiscrete {i} A = (♯i {A = A}) is-an-equiv

  -- To prove a type is an equivalence, it suffices to give a retract of ♯i
  _is-codiscrete-because_is-retract-by_ : {i : ULevel} (A : Type i)
                                          (r : ♯ A → A) (p : (a : A) → r (♯i a)  == a)
                                          → A is-codiscrete
  A is-codiscrete-because r is-retract-by p =
    (♯i {A = A}) is-an-equivalence-because r is-inverse-by
        (λ a → -- Given an a : ♯ A,
             (let♯ a :=♯i b in♯ -- We suppose a is ♯i b
                   (♯i (ap ♯i (p b))) -- apply p to b to get r (♯i b) == b,
                                      -- then apply ♯i to get ♯i r ♯i b == ♯i b
                                      -- then hit it with ♯i to get ♯ (♯i r ♯i b == ♯i b)
              in-family (λ (b : ♯ A) → ♯i (r b) == b) -- which is ♯ (♯i r a == a) by our hypothesis,
             )
          |> (<– ♯path-eq) -- and we can strip the ♯ becacuse equality types are codiscrete.
        )
      and p

  -- (λ a → (<– ♯path-eq) ((♯-elim  (λ (b : ♯ A) → ♯i (r b) == b)
  --     (λ b → ♯i (ap ♯i (p b)))) a))

  ♯→ : {i j : ULevel} {A : Type i} {B : Type j}
       (f : A → B) → (♯ A) → (♯ B)
  ♯→ {A = A} {B = B} f = ♯-rec (♯i ∘ f)

  -- Of course, ♯ A is codiscrete for any type A
  ♯-is-codiscrete : {i : ULevel} (A : Type i) → (♯ A) is-codiscrete
  ♯-is-codiscrete A =
    (♯ A) is-codiscrete-because
      (λ (a : ♯ (♯ A)) → let♯ a :=♯i x in♯ x) is-retract-by
        (λ a → refl)

  -- This is the actual equivalence A ≃ ♯ A, given that A is codiscrete
  codisc-eq : {i : ULevel} {A : Type i} (p : A is-codiscrete)
              → A ≃ (♯ A)
  codisc-eq = ♯i ,_

  -- Theorem 3.7 of Shulman
  module _ {@♭ i : ULevel} {@♭ A : Type i} where
    code : (a b : ♯ A) → Type i
    code a = ♯' {Γ = ♯ A} {!!}
         {-
                 (let♯ u := a ↓♯in♯
                     (let♯ v := b ↓♯in♯
                       (♯i (♯ (u == v)))
                     )
                  )
-}

    ♯-identity-eq : (a b : A) → ((♯i a) == (♯i b)) ≃ ♯ (a == b)
    ♯-identity-eq a b = equiv {!!} fro {!!} {!!}
      where
        to : (♯i a) == (♯i b) → ♯ (a == b)
        to p = {!!}

        fro : ♯ (a == b) → ♯i a == ♯i b
        fro p = (let♯ p :=♯i q in♯
                      ♯i (ap ♯i q)
                )
                |> (<– ♯path-eq)

  -- Theorem 6.22 of Shulman
  -- ♭ and ♯ reflect into eachothers categories.
  ♭♯-eq : {@♭ i : ULevel} {@♭ A : Type i} → ♭ (♯ A) ≃ ♭ A
  ♭♯-eq {A = A} = equiv to fro to-fro fro-to
    where
      to : ♭ (♯ A) → ♭ A
      to (a ^♭) = (♭♯e a) ^♭

      fro : ♭ A → ♭ (♯ A)
      fro (a ^♭) = (♯i a) ^♭

      to-fro : (a : ♭ A) → to (fro a) == a
      to-fro (a ^♭) = refl

      fro-to : (a : ♭ (♯ A)) → fro (to a) == a
      fro-to (a ^♭) = ♭-ap _^♭ (! (♭♯η a))

  ♯♭-eq : {@♭ i : ULevel} {@♭ A : Type i} → ♯ (♭ A) ≃ ♯ A
  ♯♭-eq {A = A} = equiv to fro to-fro fro-to
    where
      to : ♯ (♭ A) → ♯ A
      to = ♯-rec (λ { (a ^♭) → (♯i a)})

      fro : ♯ A → ♯ (♭ A)
      fro = ♯-rec (uncrisp _ (λ (a : A) → ♯i (a ^♭)))

      to-fro : (a : ♯ A) → to (fro a) == a
      to-fro = (<– ♯path-eq) ∘
               (♯-elim (λ a → to (fro a) == a) (λ a → ♯i refl))

      fro-to : (a : ♯ (♭ A)) → fro (to a) == a
      fro-to = (<– ♯path-eq) ∘
               (♯-elim (λ a → fro (to a) == a) (λ { (a ^♭) → ♯i refl }))

  -- Theorem 6.27 of Shulman
  ♭♯-adjoint : {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : A → Type j}
               → ♭ ((a : ♭ A) → B (♭i a)) ≃ ♭ ((a : A) → ♯ (B a))
  ♭♯-adjoint {i} {j} {A} {B}  = equiv to fro to-fro fro-to
    where
      to : ♭ ((a : ♭ A) → B (♭i a)) → ♭ ((a : A) → ♯ (B a))
      to (f ^♭) = (uncrisp B (λ (@♭ a : A) → ♯i (f (a ^♭)))) ^♭

      fro : ♭ ((a : A) → ♯ (B a)) → ♭ ((a : ♭ A) → B (♭i a))
      fro (f ^♭) = (λ { (a ^♭) → ♭♯e (f a) }) ^♭

      to-fro : (f : ♭ ((a : A) → ♯ (B a))) → to (fro f) == f
      to-fro (f ^♭)= ♭-ap _^♭ {!!}

      fro-to : (f : ♭ ((a : ♭ A) → B (♭i a))) → fro (to f) == f
      fro-to (@♭ f ^♭) = ♭-ap _^♭ (λ= (λ a → {!(λ { (a₁ ^♭) → ♭♯e (uncrisp B (λ (a₂ : _) → ♯i (f (a₂ ^♭))) a₁) })!}))

  has-level-is-codiscrete : {i : ULevel} {A : Type i} {n : ℕ₋₂}
                            → (has-level n A) is-codiscrete
  has-level-is-codiscrete = {!!}

  ♯-preserves-level : {i : ULevel} {A : Type i}
                      {n : ℕ₋₂} (p : has-level n A)
                      → has-level n (♯ A)
  ♯-preserves-level {i} {A} {⟨-2⟩} p =
    has-level-in (♯i (contr-center p) ,
      (<– ♯path-eq) ∘ (♯-elim (λ a → ♯i (contr-center p) == a)
        (λ a → ♯i (ap ♯i (contr-path p a)))))
  ♯-preserves-level {i} {A} {S n} p =
    has-level-in (λ x y → (<– (codisc-eq has-level-is-codiscrete))
                           ((♯-elim (λ y → has-level n (x == y)) {!!}) y)
                           )

  {-

  to-crisp : {@♭ i : ULevel} {j : ULevel} {A : ♭ (Type i)} {B : Type j}
        → (♭i A → B) → (A ♭:→ B)
  to-crisp {A = (A ^♭)} f = (<– ♭-recursion-eq) (f ∘ ♭i)

  _is-codiscrete : {@♭ j : ULevel} (B : Type j) → Type (lsucc j)
  _is-codiscrete {j} B = (A : ♭ (Type j)) → to-crisp {A = A} {B = B} is-an-equiv

  codisc-eq : {@♭ j : ULevel} {B : Type j} (p : B is-codiscrete)
              {A : ♭ (Type j)} → (♭i A → B) ≃ (A ♭:→ B)
  codisc-eq {j} {B} p {A} = (to-crisp {A = A} {B = B}) , (p A)

  codisc-promote : {@♭ j : ULevel} {B : Type j} (p : B is-codiscrete)
                   {A : ♭ (Type j)} → (A ♭:→ B) → (♭i A → B)
  codisc-promote p = <– (codisc-eq p)

  _is-codiscrete-is-a-prop : {@♭ j : ULevel} (B : Type j) → (B is-codiscrete) is-a-prop
  _is-codiscrete-is-a-prop {j} B =
    mapping-into-prop-is-a-prop (λ { (A ^♭) → is-equiv-is-prop })

  _is-codiscrete₀ : {@♭ j : ULevel} (B : Type j) → Type₀
  _is-codiscrete₀ {j} B = (resize₀ ((B is-codiscrete) , (B is-codiscrete-is-a-prop))) holds

  ⊤-is-codiscrete : ⊤ is-codiscrete
  ⊤-is-codiscrete =
    λ { (A ^♭) → to-crisp is-an-equivalence-because
      (λ _ _ → unit) is-inverse-by
        (λ f → refl) and (λ f → refl) }

 {-
  Π-codisc : {@♭ i : ULevel} {A : Type i} {B : A → Type i}
             → ((a : A) → (B a) is-codiscrete)
             → ((a : A) → B a) is-codiscrete
  Π-codisc {i} {A} {B} f =
     λ { (T ^♭) → to-crisp is-an-equivalence-because
      (λ g → λ t a → {!codisc-promote (f a)!}) is-inverse-by
        {!!} and {!!}}
  -}

  {-
  question : {@♭ i : ULevel} (B : Type i)
             (r : (A : ♭ (Type i)) → (to-crisp {A = A} {B = B}) is-split-inj)
             → B is-codiscrete
  question {i = i} B r =
    λ { (A ^♭) → to-crisp is-an-equivalence-because
      fst (r (A ^♭)) is-inverse-by
        (λ f → {!!})
        and snd (r (A ^♭)) } -}

  {-  The idea from this proof is to map out of the suspension

  =-is-codiscrete : {@♭ i : ULevel} {B : Type i} (p : B is-codiscrete)
                    (x y : B) → (x == y) is-codiscrete
  =-is-codiscrete {i} {B} p x y =
    λ { (A ^♭) → to-crisp is-an-equivalence-because
      {!!} is-inverse-by {!!} and {!!} }

  -}

  -}

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


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

module Definition.Conversion.Decidable where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Whnf
open import Definition.Conversion.Soundness
open import Definition.Conversion.Symmetry
open import Definition.Conversion.Stability
open import Definition.Conversion.Conversion
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Reduction
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.Inequality as IE
open import Definition.Typed.Consequences.NeTypeEq
open import Definition.Typed.Consequences.SucCong
open import Definition.Typed.Consequences.Inversion

open import Tools.Nat
open import Tools.Product
open import Tools.Empty
open import Tools.Nullary
import Tools.PropositionalEquality as PE

-- Algorithmic equality of variables infers propositional equality.
strongVarEq : ∀ {m n A Γ} → Γ ⊢ var n ~ var m ↑ A → n PE.≡ m
strongVarEq (var-refl x x≡y) = x≡y

-- Helper function for decidability of applications.
dec~↑-app : ∀ {k k₁ l l₁ F F₁ G G₁ B Γ}
          → Γ ⊢ k ∷ Π F ▹ G
          → Γ ⊢ k₁ ∷ Π F₁ ▹ G₁
          → Γ ⊢ k ~ k₁ ↓ B
          → Dec (Γ ⊢ l [conv↑] l₁ ∷ F)
          → Dec (∃ λ A → Γ ⊢ k ∘ l ~ k₁ ∘ l₁ ↑ A)
dec~↑-app k k₁ k~k₁ (yes p) =
  let whnfA , neK , neL = ne~↓ k~k₁
      ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ k~k₁)
      ΠFG₁≡A = neTypeEq neK k ⊢k
      H , E , A≡ΠHE = Π≡A ΠFG₁≡A whnfA
      F≡H , G₁≡E = injectivity (PE.subst (λ x → _ ⊢ _ ≡ x) A≡ΠHE ΠFG₁≡A)
  in  yes (E [ _ ] , app-cong (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) A≡ΠHE k~k₁)
                              (convConvTerm p F≡H))
dec~↑-app k₂ k₃ k~k₁ (no ¬p) =
  no (λ { (_ , app-cong x x₁) →
      let whnfA , neK , neL = ne~↓ x
          ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ x)
          ΠFG≡ΠF₂G₂ = neTypeEq neK k₂ ⊢k
          F≡F₂ , G≡G₂ = injectivity ΠFG≡ΠF₂G₂
      in  ¬p (convConvTerm x₁ (sym F≡F₂)) })

-- Helper function for decidability for neutrals of natural number type.
decConv↓Term-ℕ-ins : ∀ {t u Γ}
                    → Γ ⊢ t [conv↓] u ∷ ℕ
                    → Γ ⊢ t ~ t ↓ ℕ
                    → Γ ⊢ t ~ u ↓ ℕ
decConv↓Term-ℕ-ins (ℕ-ins x) t~t = x
decConv↓Term-ℕ-ins (ne-ins x x₁ () x₃) t~t
decConv↓Term-ℕ-ins (zero-refl x) ([~] A D whnfB ())
decConv↓Term-ℕ-ins (suc-cong x) ([~] A D whnfB ())

-- Helper function for decidability for neutrals of empty type.
decConv↓Term-Empty-ins : ∀ {t u Γ}
                    → Γ ⊢ t [conv↓] u ∷ Empty
                    → Γ ⊢ t ~ t ↓ Empty
                    → Γ ⊢ t ~ u ↓ Empty
decConv↓Term-Empty-ins (Empty-ins x) t~t = x
decConv↓Term-Empty-ins (ne-ins x x₁ () x₃) t~t

-- Helper function for decidability for neutrals of a neutral type.
decConv↓Term-ne-ins : ∀ {t u A Γ}
                    → Neutral A
                    → Γ ⊢ t [conv↓] u ∷ A
                    → ∃ λ B → Γ ⊢ t ~ u ↓ B
decConv↓Term-ne-ins () (ℕ-ins x)
decConv↓Term-ne-ins () (Empty-ins x)
decConv↓Term-ne-ins neA (ne-ins x x₁ x₂ x₃) = _ , x₃
decConv↓Term-ne-ins () (univ x x₁ x₂)
decConv↓Term-ne-ins () (zero-refl x)
decConv↓Term-ne-ins () (suc-cong x)
decConv↓Term-ne-ins () (η-eq x₁ x₂ x₃ x₄ x₅)

-- Helper function for decidability for impossibility of terms not being equal
-- as neutrals when they are equal as terms and the first is a neutral.
decConv↓Term-ℕ : ∀ {t u Γ}
                → Γ ⊢ t [conv↓] u ∷ ℕ
                → Γ ⊢ t ~ t ↓ ℕ
                → ¬ (Γ ⊢ t ~ u ↓ ℕ)
                → ⊥
decConv↓Term-ℕ (ℕ-ins x) t~t ¬u~u = ¬u~u x
decConv↓Term-ℕ (ne-ins x x₁ () x₃) t~t ¬u~u
decConv↓Term-ℕ (zero-refl x) ([~] A D whnfB ()) ¬u~u
decConv↓Term-ℕ (suc-cong x) ([~] A D whnfB ()) ¬u~u

-- Helper function for extensional equality of Unit.
decConv↓Term-Unit : ∀ {t u Γ}
              → Γ ⊢ t [conv↓] t ∷ Unit → Γ ⊢ u [conv↓] u ∷ Unit
              → Dec (Γ ⊢ t [conv↓] u ∷ Unit)
decConv↓Term-Unit tConv uConv =
  let t≡t = soundnessConv↓Term tConv
      u≡u = soundnessConv↓Term uConv
      _ , [t] , _ = syntacticEqTerm t≡t
      _ , [u] , _ = syntacticEqTerm u≡u
      _ , tWhnf , _ = whnfConv↓Term tConv
      _ , uWhnf , _ = whnfConv↓Term uConv
  in  yes (η-unit [t] [u] tWhnf uWhnf)

mutual
  -- Decidability of algorithmic equality of neutrals.
  dec~↑ : ∀ {k l R T Γ}
        → Γ ⊢ k ~ k ↑ R → Γ ⊢ l ~ l ↑ T
        → Dec (∃ λ A → Γ ⊢ k ~ l ↑ A)
  dec~↑ (var-refl {n} x₂ x≡y) (var-refl {m} x₃ x≡y₁) with n ≟ m
  ... | yes PE.refl = yes (_ , var-refl x₂ x≡y₁)
  ... | no ¬p = no (λ { (A , k~l) → ¬p (strongVarEq k~l) })
  dec~↑ (var-refl x₁ x≡y) (app-cong x₂ x₃) = no (λ { (_ , ()) })
  dec~↑ (var-refl x₁ x≡y) (fst-cong x₂) = no (λ { (_ , ()) })
  dec~↑ (var-refl x₁ x≡y) (snd-cong x₂) = no (λ { (_ , ()) })
  dec~↑ (var-refl x₁ x≡y) (natrec-cong x₂ x₃ x₄ x₅) = no (λ { (_ , ()) })
  dec~↑ (var-refl x₁ x≡y) (Emptyrec-cong x₂ x₃) = no (λ { (_ , ()) })

  dec~↑ (app-cong x x₁) (app-cong x₂ x₃)
        with dec~↓ x x₂
  ... | yes (A , k~l) =
    let whnfA , neK , neL = ne~↓ k~l
        ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ k~l)
        _ , ⊢l₁ , _ = syntacticEqTerm (soundness~↓ x)
        _ , ⊢l₂ , _ = syntacticEqTerm (soundness~↓ x₂)
        ΠFG≡A = neTypeEq neK ⊢l₁ ⊢k
        ΠF′G′≡A = neTypeEq neL ⊢l₂ ⊢l
        F≡F′ , G≡G′ = injectivity (trans ΠFG≡A (sym ΠF′G′≡A))
    in  dec~↑-app ⊢l₁ ⊢l₂ k~l (decConv↑TermConv F≡F′ x₁ x₃)
  ... | no ¬p = no (λ { (_ , app-cong x₄ x₅) → ¬p (_ , x₄) })
  dec~↑ (app-cong x₁ x₂) (var-refl x₃ x≡y) = no (λ { (_ , ()) })
  dec~↑ (app-cong x x₁) (fst-cong x₂) = no (λ { (_ , ()) })
  dec~↑ (app-cong x x₁) (snd-cong x₂) = no (λ { (_ , ()) })
  dec~↑ (app-cong x x₁) (natrec-cong x₂ x₃ x₄ x₅) = no (λ { (_ , ()) })
  dec~↑ (app-cong x x₁) (Emptyrec-cong x₂ x₃) = no (λ { (_ , ()) })

  dec~↑ (fst-cong {k} k~k) (fst-cong {l} l~l) with dec~↓ k~k l~l
  ... | yes (A , k~l) =
    let whnfA , neK , neL = ne~↓ k~l
        ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ k~l)
        _ , ⊢k₁ , _ = syntacticEqTerm (soundness~↓ k~k)
        ΣFG≡A = neTypeEq neK ⊢k₁ ⊢k
        F , G , A≡ΣFG = Σ≡A ΣFG≡A whnfA
    in  yes (F , fst-cong (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x)
                          A≡ΣFG
                          k~l))
  ... | no ¬p = no (λ { (_ , fst-cong x₂) → ¬p (_ , x₂) })
  dec~↑ (fst-cong x) (var-refl x₁ x₂) = no (λ { (_ , ()) })
  dec~↑ (fst-cong x) (app-cong x₁ x₂) = no (λ { (_ , ()) })
  dec~↑ (fst-cong x) (snd-cong x₁) = no (λ { (_ , ()) })
  dec~↑ (fst-cong x) (natrec-cong x₁ x₂ x₃ x₄) = no (λ { (_ , ()) })
  dec~↑ (fst-cong x) (Emptyrec-cong x₁ x₂) = no (λ { (_ , ()) })

  dec~↑ (snd-cong {k} k~k) (snd-cong {l} l~l) with dec~↓ k~k l~l
  ... | yes (A , k~l) =
    let whnfA , neK , neL = ne~↓ k~l
        ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ k~l)
        _ , ⊢k₁ , _ = syntacticEqTerm (soundness~↓ k~k)
        ΣFG≡A = neTypeEq neK ⊢k₁ ⊢k
        F , G , A≡ΣFG = Σ≡A ΣFG≡A whnfA
    in  yes (G [ fst k ] , snd-cong (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x)
                                    A≡ΣFG
                                    k~l))
  ... | no ¬p = no (λ { (_ , snd-cong x₂) → ¬p (_ , x₂) })
  dec~↑ (snd-cong x) (var-refl x₁ x₂) = no (λ { (_ , ()) })
  dec~↑ (snd-cong x) (app-cong x₁ x₂) = no (λ { (_ , ()) })
  dec~↑ (snd-cong x) (fst-cong x₁) = no (λ { (_ , ()) })
  dec~↑ (snd-cong x) (natrec-cong x₁ x₂ x₃ x₄) = no (λ { (_ , ()) })
  dec~↑ (snd-cong x) (Emptyrec-cong x₁ x₂) = no (λ { (_ , ()) })

  dec~↑ (natrec-cong x x₁ x₂ x₃) (natrec-cong x₄ x₅ x₆ x₇)
        with decConv↑ x x₄
  ... | yes p
        with decConv↑TermConv
               (substTypeEq (soundnessConv↑ p)
                            (refl (zeroⱼ (wfEqTerm (soundness~↓ x₃)))))
               x₁ x₅
           | decConv↑TermConv (sucCong (soundnessConv↑ p)) x₂ x₆
           | dec~↓ x₃ x₇
  ... | yes p₁ | yes p₂ | yes (A , k~l) =
    let whnfA , neK , neL = ne~↓ k~l
        ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ k~l)
        _ , ⊢l∷ℕ , _ = syntacticEqTerm (soundness~↓ x₃)
        ⊢ℕ≡A = neTypeEq neK ⊢l∷ℕ ⊢k
        A≡ℕ = ℕ≡A ⊢ℕ≡A whnfA
        k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) A≡ℕ k~l
    in  yes (_ , natrec-cong p p₁ p₂ k~l′)
  ... | yes p₁ | yes p₂ | no ¬p =
    no (λ { (_ , natrec-cong x₈ x₉ x₁₀ x₁₁) → ¬p (_ , x₁₁) })
  ... | yes p₁ | no ¬p | r =
    no (λ { (_ , natrec-cong x₈ x₉ x₁₀ x₁₁) → ¬p x₁₀ })
  ... | no ¬p | w | r =
    no (λ { (_ , natrec-cong x₈ x₉ x₁₀ x₁₁) → ¬p x₉ })
  dec~↑ (natrec-cong x x₁ x₂ x₃) (natrec-cong x₄ x₅ x₆ x₇)
    | no ¬p = no (λ { (_ , natrec-cong x₈ x₉ x₁₀ x₁₁) → ¬p x₈ })
  dec~↑ (natrec-cong _ _ _ _) (var-refl _ _) = no (λ { (_ , ()) })
  dec~↑ (natrec-cong _ _ _ _) (fst-cong _) = no (λ { (_ , ()) })
  dec~↑ (natrec-cong _ _ _ _) (snd-cong _) = no (λ { (_ , ()) })
  dec~↑ (natrec-cong _ _ _ _) (app-cong _ _) = no (λ { (_ , ()) })
  dec~↑ (natrec-cong _ _ _ _) (Emptyrec-cong _ _) = no (λ { (_ , ()) })

  dec~↑ (Emptyrec-cong x x₁) (Emptyrec-cong x₄ x₅)
        with decConv↑ x x₄ | dec~↓ x₁ x₅
  ... | yes p | yes (A , k~l) =
    let whnfA , neK , neL = ne~↓ k~l
        ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ k~l)
        _ , ⊢l∷Empty , _ = syntacticEqTerm (soundness~↓ x₁)
        ⊢Empty≡A = neTypeEq neK ⊢l∷Empty ⊢k
        A≡Empty = Empty≡A ⊢Empty≡A whnfA
        k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) A≡Empty k~l
    in  yes (_ , Emptyrec-cong p k~l′)
  ... | yes p | no ¬p = no (λ { (_ , Emptyrec-cong a b) → ¬p (_ , b) })
  ... | no ¬p | r = no (λ { (_ , Emptyrec-cong a b) → ¬p a })
  dec~↑ (Emptyrec-cong _ _) (var-refl _ _) = no (λ { (_ , ()) })
  dec~↑ (Emptyrec-cong _ _) (fst-cong _) = no (λ { (_ , ()) })
  dec~↑ (Emptyrec-cong _ _) (snd-cong _) = no (λ { (_ , ()) })
  dec~↑ (Emptyrec-cong _ _) (app-cong _ _) = no (λ { (_ , ()) })
  dec~↑ (Emptyrec-cong _ _) (natrec-cong _ _ _ _) = no (λ { (_ , ()) })

  dec~↑′ : ∀ {k l R T Γ Δ}
        → ⊢ Γ ≡ Δ
        → Γ ⊢ k ~ k ↑ R → Δ ⊢ l ~ l ↑ T
        → Dec (∃ λ A → Γ ⊢ k ~ l ↑ A)
  dec~↑′ Γ≡Δ k~k l~l = dec~↑ k~k (stability~↑ (symConEq Γ≡Δ) l~l)

  -- Decidability of algorithmic equality of neutrals with types in WHNF.
  dec~↓ : ∀ {k l R T Γ}
        → Γ ⊢ k ~ k ↓ R → Γ ⊢ l ~ l ↓ T
        → Dec (∃ λ A → Γ ⊢ k ~ l ↓ A)
  dec~↓ ([~] A D whnfB k~l) ([~] A₁ D₁ whnfB₁ k~l₁) with dec~↑ k~l k~l₁
  dec~↓ ([~] A D whnfB k~l) ([~] A₁ D₁ whnfB₁ k~l₁) | yes (B , k~l₂) =
    let ⊢B , _ , _ = syntacticEqTerm (soundness~↑ k~l₂)
        C , whnfC , D′ = whNorm ⊢B
    in  yes (C , [~] B (red D′) whnfC k~l₂)
  dec~↓ ([~] A D whnfB k~l) ([~] A₁ D₁ whnfB₁ k~l₁) | no ¬p =
    no (λ { (A₂ , [~] A₃ D₂ whnfB₂ k~l₂) → ¬p (A₃ , k~l₂) })

  -- Decidability of algorithmic equality of types.
  decConv↑ : ∀ {A B Γ}
           → Γ ⊢ A [conv↑] A → Γ ⊢ B [conv↑] B
           → Dec (Γ ⊢ A [conv↑] B)
  decConv↑ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′)
               ([↑] A″ B″ D₁ D″ whnfA″ whnfB″ A′<>B″)
           rewrite whrDet* (D , whnfA′) (D′ , whnfB′)
                 | whrDet* (D₁ , whnfA″) (D″ , whnfB″)
           with decConv↓ A′<>B′ A′<>B″
  decConv↑ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′)
               ([↑] A″ B″ D₁ D″ whnfA″ whnfB″ A′<>B″) | yes p =
    yes ([↑] B′ B″ D′ D″ whnfB′ whnfB″ p)
  decConv↑ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′)
               ([↑] A″ B″ D₁ D″ whnfA″ whnfB″ A′<>B″) | no ¬p =
    no (λ { ([↑] A‴ B‴ D₂ D‴ whnfA‴ whnfB‴ A′<>B‴) →
        let A‴≡B′  = whrDet* (D₂ , whnfA‴) (D′ , whnfB′)
            B‴≡B″ = whrDet* (D‴ , whnfB‴)
                                (D″ , whnfB″)
        in  ¬p (PE.subst₂ (λ x y → _ ⊢ x [conv↓] y) A‴≡B′ B‴≡B″ A′<>B‴) })

  decConv↑′ : ∀ {A B Γ Δ}
            → ⊢ Γ ≡ Δ
            → Γ ⊢ A [conv↑] A → Δ ⊢ B [conv↑] B
            → Dec (Γ ⊢ A [conv↑] B)
  decConv↑′ Γ≡Δ A B = decConv↑ A (stabilityConv↑ (symConEq Γ≡Δ) B)

  -- Decidability of algorithmic equality of types in WHNF.
  decConv↓ : ∀ {A B Γ}
           → Γ ⊢ A [conv↓] A → Γ ⊢ B [conv↓] B
           → Dec (Γ ⊢ A [conv↓] B)
  -- True cases
  decConv↓ (U-refl x) (U-refl x₁) = yes (U-refl x)
  decConv↓ (ℕ-refl x) (ℕ-refl x₁) = yes (ℕ-refl x)
  decConv↓ (Empty-refl x) (Empty-refl x₁) = yes (Empty-refl x)
  decConv↓ (Unit-refl x) (Unit-refl x₁) = yes (Unit-refl x)

  -- Inspective cases
  decConv↓ (ne x) (ne x₁) with dec~↓ x x₁
  decConv↓ (ne x) (ne x₁) | yes (A , k~l) =
    let whnfA , neK , neL = ne~↓ k~l
        ⊢A , ⊢k , _ = syntacticEqTerm (soundness~↓ k~l)
        _ , ⊢k∷U , _ = syntacticEqTerm (soundness~↓ x)
        ⊢U≡A = neTypeEq neK ⊢k∷U ⊢k
        A≡U = U≡A ⊢U≡A
        k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) A≡U k~l
    in  yes (ne k~l′)
  decConv↓ (ne x) (ne x₁) | no ¬p =
    no (λ x₂ → ¬p (U , decConv↓-ne x₂ x))

  decConv↓ (Π-cong x x₁ x₂) (Π-cong x₃ x₄ x₅)
           with decConv↑ x₁ x₄
  ... | yes p with decConv↑′ (reflConEq (wf x) ∙ soundnessConv↑ p) x₂ x₅
  ... | yes p₁ = yes (Π-cong x p p₁)
  ... | no ¬p = no (λ { (ne ([~] A D whnfB ())) ; (Π-cong x₆ x₇ x₈) → ¬p x₈ })
  decConv↓ (Π-cong x x₁ x₂) (Π-cong x₃ x₄ x₅) | no ¬p =
    no (λ { (ne ([~] A D whnfB ())) ; (Π-cong x₆ x₇ x₈) → ¬p x₇ })

  decConv↓ (Σ-cong x x₁ x₂) (Σ-cong x₃ x₄ x₅)
           with decConv↑ x₁ x₄
  ... | yes p with decConv↑′ (reflConEq (wf x) ∙ soundnessConv↑ p) x₂ x₅
  ... | yes p₁ = yes (Σ-cong x p p₁)
  ... | no ¬p = no (λ { (ne ([~] A D whnfB ())) ; (Σ-cong x₆ x₇ x₈) → ¬p x₈ })
  decConv↓ (Σ-cong x x₁ x₂) (Σ-cong x₃ x₄ x₅) | no ¬p =
    no (λ { (ne ([~] A D whnfB ())) ; (Σ-cong x₆ x₇ x₈) → ¬p x₇ })

  -- False cases
  decConv↓ (U-refl x) (ℕ-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (U-refl x) (Empty-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (U-refl x) (Unit-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (U-refl x) (ne x₁) =
    no (λ x₂ → let whnfA , neK , neL = ne~↓ x₁
               in  ⊥-elim (IE.U≢ne neK (soundnessConv↓ x₂)))
  decConv↓ (U-refl x) (Π-cong x₁ x₂ x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (U-refl x) (Σ-cong x₁ x₂ x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (ℕ-refl x) (U-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (ℕ-refl x) (Empty-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (ℕ-refl x) (Unit-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (ℕ-refl x) (ne x₁) =
    no (λ x₂ → let whnfA , neK , neL = ne~↓ x₁
               in  ⊥-elim (IE.ℕ≢ne neK (soundnessConv↓ x₂)))
  decConv↓ (ℕ-refl x) (Π-cong x₁ x₂ x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (ℕ-refl x) (Σ-cong x₁ x₂ x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Empty-refl x) (U-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Empty-refl x) (ℕ-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Empty-refl x) (Unit-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Empty-refl x) (ne x₁) =
    no (λ x₂ → let whnfA , neK , neL = ne~↓ x₁
               in  ⊥-elim (IE.Empty≢neⱼ neK (soundnessConv↓ x₂)))
  decConv↓ (Empty-refl x) (Π-cong x₁ x₂ x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Empty-refl x) (Σ-cong x₁ x₂ x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Unit-refl x) (U-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Unit-refl x) (ℕ-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Unit-refl x) (Empty-refl x₁) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Unit-refl x) (ne x₁) =
    no (λ x₂ → let whnfA , neK , neL = ne~↓ x₁
               in  ⊥-elim (IE.Unit≢neⱼ neK (soundnessConv↓ x₂)))
  decConv↓ (Unit-refl x) (Π-cong x₁ x₂ x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Unit-refl x) (Σ-cong x₁ x₂ x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (ne x) (U-refl x₁) =
    no (λ x₂ → let whnfA , neK , neL = ne~↓ x
               in  ⊥-elim (IE.U≢ne neK (sym (soundnessConv↓ x₂))))
  decConv↓ (ne x) (ℕ-refl x₁) =
    no (λ x₂ → let whnfA , neK , neL = ne~↓ x
               in  ⊥-elim (IE.ℕ≢ne neK (sym (soundnessConv↓ x₂))))
  decConv↓ (ne x) (Empty-refl x₁) =
    no (λ x₂ → let whnfA , neK , neL = ne~↓ x
               in  ⊥-elim (IE.Empty≢neⱼ neK (sym (soundnessConv↓ x₂))))
  decConv↓ (ne x) (Unit-refl x₁) =
    no (λ x₂ → let whnfA , neK , neL = ne~↓ x
               in  ⊥-elim (IE.Unit≢neⱼ neK (sym (soundnessConv↓ x₂))))
  decConv↓ (ne x) (Π-cong x₁ x₂ x₃) =
    no (λ x₄ → let whnfA , neK , neL = ne~↓ x
               in  ⊥-elim (IE.Π≢ne neK (sym (soundnessConv↓ x₄))))
  decConv↓ (ne x) (Σ-cong x₁ x₂ x₃) =
    no (λ x₄ → let whnfA , neK , neL = ne~↓ x
               in  ⊥-elim (IE.Σ≢ne neK (sym (soundnessConv↓ x₄))))
  decConv↓ (Π-cong x x₁ x₂) (U-refl x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Π-cong x x₁ x₂) (ℕ-refl x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Π-cong x x₁ x₂) (Empty-refl x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Π-cong x x₁ x₂) (Unit-refl x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Π-cong x x₁ x₂) (Σ-cong x₃ x₄ x₅) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Π-cong x x₁ x₂) (ne x₃) =
    no (λ x₄ → let whnfA , neK , neL = ne~↓ x₃
               in  ⊥-elim (IE.Π≢ne neK (soundnessConv↓ x₄)))
  decConv↓ (Σ-cong x x₁ x₂) (U-refl x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Σ-cong x x₁ x₂) (ℕ-refl x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Σ-cong x x₁ x₂) (Empty-refl x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Σ-cong x x₁ x₂) (Unit-refl x₃) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Σ-cong x x₁ x₂) (Π-cong x₃ x₄ x₅) = no (λ { (ne ([~] A D whnfB ())) })
  decConv↓ (Σ-cong x x₁ x₂) (ne x₃) =
    no (λ x₄ → let whnfA , neK , neL = ne~↓ x₃
               in  ⊥-elim (IE.Σ≢ne neK (soundnessConv↓ x₄)))

  -- Helper function for decidability of neutral types.
  decConv↓-ne : ∀ {A B Γ}
              → Γ ⊢ A [conv↓] B
              → Γ ⊢ A ~ A ↓ U
              → Γ ⊢ A ~ B ↓ U
  decConv↓-ne (U-refl x) A~A = A~A
  decConv↓-ne (ℕ-refl x) A~A = A~A
  decConv↓-ne (Empty-refl x) A~A = A~A
  decConv↓-ne (ne x) A~A = x
  decConv↓-ne (Π-cong x x₁ x₂) ([~] A D whnfB ())

  -- Decidability of algorithmic equality of terms.
  decConv↑Term : ∀ {t u A Γ}
               → Γ ⊢ t [conv↑] t ∷ A → Γ ⊢ u [conv↑] u ∷ A
               → Dec (Γ ⊢ t [conv↑] u ∷ A)
  decConv↑Term ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
               ([↑]ₜ B₁ t″ u″ D₁ d₁ d″ whnfB₁ whnft″ whnfu″ t<>u₁)
               rewrite whrDet* (D , whnfB) (D₁ , whnfB₁)
                     | whrDet*Term  (d , whnft′) (d′ , whnfu′)
                     | whrDet*Term  (d₁ , whnft″) (d″ , whnfu″)
               with decConv↓Term t<>u t<>u₁
  decConv↑Term ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
               ([↑]ₜ B₁ t″ u″ D₁ d₁ d″ whnfB₁ whnft″ whnfu″ t<>u₁)
               | yes p =
    yes ([↑]ₜ B₁ u′ u″ D₁
                  d′ d″ whnfB₁ whnfu′ whnfu″ p)
  decConv↑Term ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
               ([↑]ₜ B₁ t″ u″ D₁ d₁ d″ whnfB₁ whnft″ whnfu″ t<>u₁)
               | no ¬p =
    no (λ { ([↑]ₜ B₂ t‴ u‴ D₂ d₂ d‴ whnfB₂ whnft‴ whnfu‴ t<>u₂) →
        let B₂≡B₁ = whrDet* (D₂ , whnfB₂)
                             (D₁ , whnfB₁)
            t‴≡u′ = whrDet*Term (d₂ , whnft‴)
                              (PE.subst (λ x → _ ⊢ _ ⇒* _ ∷ x) (PE.sym B₂≡B₁) d′
                              , whnfu′)
            u‴≡u″ = whrDet*Term (d‴ , whnfu‴)
                               (PE.subst (λ x → _ ⊢ _ ⇒* _ ∷ x)
                                         (PE.sym B₂≡B₁)
                                         d″
                               , whnfu″)
        in  ¬p (PE.subst₃ (λ x y z → _ ⊢ x [conv↓] y ∷ z)
                          t‴≡u′ u‴≡u″ B₂≡B₁ t<>u₂) })

  decConv↑Term′ : ∀ {t u A Γ Δ}
                → ⊢ Γ ≡ Δ
                → Γ ⊢ t [conv↑] t ∷ A → Δ ⊢ u [conv↑] u ∷ A
                → Dec (Γ ⊢ t [conv↑] u ∷ A)
  decConv↑Term′ Γ≡Δ t u = decConv↑Term t (stabilityConv↑Term (symConEq Γ≡Δ) u)

  -- Decidability of algorithmic equality of terms in WHNF.
  decConv↓Term : ∀ {t u A Γ}
               → Γ ⊢ t [conv↓] t ∷ A → Γ ⊢ u [conv↓] u ∷ A
               → Dec (Γ ⊢ t [conv↓] u ∷ A)
  -- True cases
  decConv↓Term (zero-refl x) (zero-refl x₁) = yes (zero-refl x)
  decConv↓Term (Unit-ins t~t) uConv = decConv↓Term-Unit (Unit-ins t~t) uConv
  decConv↓Term (η-unit [t] _ tUnit _) uConv =
    decConv↓Term-Unit (η-unit [t] [t] tUnit tUnit) uConv

  -- Inspective cases
  decConv↓Term (ℕ-ins x) (ℕ-ins x₁) with dec~↓ x x₁
  decConv↓Term (ℕ-ins x) (ℕ-ins x₁) | yes (A , k~l) =
    let whnfA , neK , neL = ne~↓ k~l
        ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ k~l)
        _ , ⊢l∷ℕ , _ = syntacticEqTerm (soundness~↓ x)
        ⊢ℕ≡A = neTypeEq neK ⊢l∷ℕ ⊢k
        A≡ℕ = ℕ≡A ⊢ℕ≡A whnfA
        k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) A≡ℕ k~l
    in  yes (ℕ-ins k~l′)
  decConv↓Term (ℕ-ins x) (ℕ-ins x₁) | no ¬p =
    no (λ x₂ → ¬p (ℕ , decConv↓Term-ℕ-ins x₂ x))
  decConv↓Term (Empty-ins x) (Empty-ins x₁) with dec~↓ x x₁
  decConv↓Term (Empty-ins x) (Empty-ins x₁) | yes (A , k~l) =
    let whnfA , neK , neL = ne~↓ k~l
        ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓ k~l)
        _ , ⊢l∷Empty , _ = syntacticEqTerm (soundness~↓ x)
        ⊢Empty≡A = neTypeEq neK ⊢l∷Empty ⊢k
        A≡Empty = Empty≡A ⊢Empty≡A whnfA
        k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) A≡Empty k~l
    in  yes (Empty-ins k~l′)
  decConv↓Term (Empty-ins x) (Empty-ins x₁) | no ¬p =
    no (λ x₂ → ¬p (Empty , decConv↓Term-Empty-ins x₂ x))
  decConv↓Term (ne-ins x x₁ x₂ x₃) (ne-ins x₄ x₅ x₆ x₇)
               with dec~↓ x₃ x₇
  decConv↓Term (ne-ins x x₁ x₂ x₃) (ne-ins x₄ x₅ x₆ x₇) | yes (A , k~l) =
    yes (ne-ins x₁ x₄ x₆ k~l)
  decConv↓Term (ne-ins x x₁ x₂ x₃) (ne-ins x₄ x₅ x₆ x₇) | no ¬p =
    no (λ x₈ → ¬p (decConv↓Term-ne-ins x₆ x₈))
  decConv↓Term (univ x x₁ x₂) (univ x₃ x₄ x₅)
               with decConv↓  x₂ x₅
  decConv↓Term (univ x x₁ x₂) (univ x₃ x₄ x₅) | yes p =
    yes (univ x₁ x₃ p)
  decConv↓Term (univ x x₁ x₂) (univ x₃ x₄ x₅) | no ¬p =
    no (λ { (ne-ins x₆ x₇ () x₉)
          ; (univ x₆ x₇ x₈) → ¬p x₈ })
  decConv↓Term (suc-cong x) (suc-cong x₁) with decConv↑Term  x x₁
  decConv↓Term (suc-cong x) (suc-cong x₁) | yes p =
    yes (suc-cong p)
  decConv↓Term (suc-cong x) (suc-cong x₁) | no ¬p =
    no (λ { (ℕ-ins ([~] A D whnfB ()))
          ; (ne-ins x₂ x₃ () x₅)
          ; (suc-cong x₂) → ¬p x₂ })
  decConv↓Term (Σ-η ⊢t _ tProd _ fstConvT sndConvT)
               (Σ-η ⊢u _ uProd _ fstConvU sndConvU)
    with decConv↑Term fstConvT fstConvU
  ... | yes P with let ⊢F , ⊢G = syntacticΣ (syntacticTerm ⊢t)
                       fstt≡fstu = soundnessConv↑Term P
                       Gfstt≡Gfstu = substTypeEq (refl ⊢G) fstt≡fstu
                   in  decConv↑TermConv Gfstt≡Gfstu sndConvT sndConvU
  ... | yes Q = yes (Σ-η ⊢t ⊢u tProd uProd P Q)
  ... | no ¬Q = no (λ { (Σ-η _ _ _ _ _ Q) → ¬Q Q } )
  decConv↓Term (Σ-η _ _ _ _ _ _) (Σ-η _ _ _ _ _ _)
    | no ¬P = no (λ { (Σ-η _ _ _ _ P _) → ¬P P } )
  decConv↓Term (η-eq x₁ x₂ x₃ x₄ x₅) (η-eq x₇ x₈ x₉ x₁₀ x₁₁)
               with decConv↑Term x₅ x₁₁
  decConv↓Term (η-eq x₁ x₂ x₃ x₄ x₅) (η-eq x₇ x₈ x₉ x₁₀ x₁₁) | yes p =
    yes (η-eq x₂ x₇ x₄ x₁₀ p)
  decConv↓Term (η-eq x₁ x₂ x₃ x₄ x₅) (η-eq x₇ x₈ x₉ x₁₀ x₁₁) | no ¬p =
    no (λ { (ne-ins x₁₂ x₁₃ () x₁₅)
          ; (η-eq x₁₃ x₁₄ x₁₅ x₁₆ x₁₇) → ¬p x₁₇ })

  -- False cases
  decConv↓Term  (ℕ-ins x) (zero-refl x₁) =
    no (λ x₂ → decConv↓Term-ℕ x₂ x (λ { ([~] A D whnfB ()) }))
  decConv↓Term  (ℕ-ins x) (suc-cong x₁) =
    no (λ x₂ → decConv↓Term-ℕ x₂ x (λ { ([~] A D whnfB ()) }))
  decConv↓Term  (zero-refl x) (ℕ-ins x₁) =
    no (λ x₂ → decConv↓Term-ℕ (symConv↓Term′ x₂) x₁ (λ { ([~] A D whnfB ()) }))
  decConv↓Term  (zero-refl x) (suc-cong x₁) =
    no (λ { (ℕ-ins ([~] A D whnfB ())) ; (ne-ins x₂ x₃ () x₅) })
  decConv↓Term  (suc-cong x) (ℕ-ins x₁) =
    no (λ x₂ → decConv↓Term-ℕ (symConv↓Term′ x₂) x₁ (λ { ([~] A D whnfB ()) }))
  decConv↓Term  (suc-cong x) (zero-refl x₁) =
    no (λ { (ℕ-ins ([~] A D whnfB ())) ; (ne-ins x₂ x₃ () x₅) })

  -- Decidability of algorithmic equality of terms of equal types.
  decConv↑TermConv : ∀ {t u A B Γ}
                → Γ ⊢ A ≡ B
                → Γ ⊢ t [conv↑] t ∷ A
                → Γ ⊢ u [conv↑] u ∷ B
                → Dec (Γ ⊢ t [conv↑] u ∷ A)
  decConv↑TermConv A≡B t u =
    decConv↑Term t (convConvTerm u (sym A≡B))


text:
module _ where

record R : Set₁ where
  field
    Type : Set

postulate
  A : Set

module M (x : A) (r₁ : R) (y : A) where

  open R r₁

  r₂ : R
  r₂ = record { Type = A }

  foo : R.Type r₂
  foo = {!!}  -- R.Type r₂

  bar : R.Type r₁
  bar = {!!}  -- Type

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Data.Tuple where

open import Data.Tuple.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Relation.Binary using (Rel; Setoid; IsEquivalence)

module GGT.Structures
  {a b ℓ₁ ℓ₂}
  {G : Set a}      -- The underlying group carrier
  {Ω : Set b}      -- The underlying set space
  (_≈_ : Rel G ℓ₁) -- The underlying group equality
  (_≋_ : Rel Ω ℓ₂) -- The underlying space equality
  where

open import Level using (_⊔_)
open import Algebra.Core
open import Algebra.Structures {a} {ℓ₁} {G} using (IsGroup)
open import GGT.Definitions

record IsAction
  (· : Opᵣ G Ω)
  (∙ : Op₂ G)
  (ε : G)
  (⁻¹ : Op₁ G)
  : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
  where

  field
    isEquivalence : IsEquivalence _≋_
    isGroup       : IsGroup _≈_ ∙ ε ⁻¹
    actAssoc      : ActAssoc _≈_ _≋_ · ∙
    actId         : ActLeftIdentity _≈_ _≋_ ε ·
    ·-cong        : ·-≋-Congruence _≈_ _≋_ ·
    G-ext         : ≈-Ext _≈_ _≋_ ·

  setoid : Setoid b ℓ₂
  setoid = record
    { Carrier = Ω;
      _≈_ = _≋_;
      isEquivalence = isEquivalence }

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


text:
------------------------------------------------------------------------
-- Soundness and completeness
------------------------------------------------------------------------

module TotalParserCombinators.Derivative.SoundComplete where

open import Category.Monad
open import Codata.Musical.Notation
open import Data.List
import Data.List.Categorical
open import Data.Maybe hiding (_>>=_)
open import Data.Product
open import Level
open import Relation.Binary.PropositionalEquality

open RawMonad {f = zero} Data.List.Categorical.monad
  using () renaming (_>>=_ to _>>=′_; _⊛_ to _⊛′_)

open import TotalParserCombinators.Derivative.Definition
import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics

------------------------------------------------------------------------
-- Soundness

sound : ∀ {Tok R xs x s} {t} (p : Parser Tok R xs) →
        x ∈ D t p · s → x ∈ p · t ∷ s
sound token                   return            = token
sound (p₁ ∣ p₂)               (∣-left     x∈p₁) = ∣-left      (sound p₁ x∈p₁)
sound (_∣_ {xs₁ = xs₁} p₁ p₂) (∣-right ._ x∈p₂) = ∣-right xs₁ (sound p₂ x∈p₂)
sound (f <$> p)               (<$> x∈p)         = <$> sound p x∈p
sound (_⊛_ {fs = nothing} {xs = just _}  p₁ p₂)             (f∈p₁′  ⊛ x∈p₂)       = [ ○ - ◌ ] sound p₁ f∈p₁′ ⊛ x∈p₂
sound (_⊛_ {fs = just _}  {xs = just _}  p₁ p₂) (∣-left     (f∈p₁′  ⊛ x∈p₂))      = [ ○ - ○ ] sound p₁ f∈p₁′ ⊛ x∈p₂
sound (_⊛_ {fs = just fs} {xs = just _}  p₁ p₂) (∣-right ._ (f∈ret⋆ ⊛ x∈p₂′))     with Return⋆.sound fs f∈ret⋆
sound (_⊛_ {fs = just fs} {xs = just _}  p₁ p₂) (∣-right ._ (f∈ret⋆ ⊛ x∈p₂′))     | (refl , f∈fs) =
                                                                                [ ○ - ○ ] I.sound p₁ f∈fs ⊛ sound p₂ x∈p₂′
sound (_⊛_ {fs = nothing} {xs = nothing} p₁ p₂)             (f∈p₁′  ⊛ x∈p₂)       = [ ◌ - ◌ ] sound (♭ p₁) f∈p₁′ ⊛ x∈p₂
sound (_⊛_ {fs = just _}  {xs = nothing} p₁ p₂) (∣-left     (f∈p₁′  ⊛ x∈p₂))      = [ ◌ - ○ ] sound (♭ p₁) f∈p₁′ ⊛ x∈p₂
sound (_⊛_ {fs = just fs} {xs = nothing} p₁ p₂) (∣-right ._ (f∈ret⋆ ⊛ x∈p₂′))     with Return⋆.sound fs f∈ret⋆
sound (_⊛_ {fs = just fs} {xs = nothing} p₁ p₂) (∣-right ._ (f∈ret⋆ ⊛ x∈p₂′))     | (refl , f∈fs) =
                                                                                [ ◌ - ○ ] I.sound (♭ p₁) f∈fs ⊛ sound p₂ x∈p₂′
sound (_>>=_ {xs = nothing} {f = just _}  p₁ p₂)             (x∈p₁′  >>= y∈p₂x)   = [ ○ - ◌ ] sound p₁ x∈p₁′ >>= y∈p₂x
sound (_>>=_ {xs = just xs} {f = just _}  p₁ p₂) (∣-right ._ (y∈ret⋆ >>= z∈p₂′y)) with Return⋆.sound xs y∈ret⋆
sound (_>>=_ {xs = just xs} {f = just _}  p₁ p₂) (∣-right ._ (y∈ret⋆ >>= z∈p₂′y)) | (refl , y∈xs) =
                                                                                [ ○ - ○ ] I.sound p₁ y∈xs >>= sound (p₂ _) z∈p₂′y
sound (_>>=_ {xs = just xs} {f = just _}  p₁ p₂) (∣-left     (x∈p₁′  >>= y∈p₂x))  = [ ○ - ○ ] sound p₁ x∈p₁′ >>= y∈p₂x
sound (_>>=_ {xs = nothing} {f = nothing} p₁ p₂)             (x∈p₁′  >>= y∈p₂x)   = [ ◌ - ◌ ] sound (♭ p₁) x∈p₁′ >>= y∈p₂x
sound (_>>=_ {xs = just xs} {f = nothing} p₁ p₂) (∣-right ._ (y∈ret⋆ >>= z∈p₂′y)) with Return⋆.sound xs y∈ret⋆
sound (_>>=_ {xs = just xs} {f = nothing} p₁ p₂) (∣-right ._ (y∈ret⋆ >>= z∈p₂′y)) | (refl , y∈xs) =
                                                                                [ ◌ - ○ ] I.sound (♭ p₁) y∈xs >>= sound (p₂ _) z∈p₂′y
sound (_>>=_ {xs = just xs} {f = nothing} p₁ p₂) (∣-left     (x∈p₁′  >>= y∈p₂x))  = [ ◌ - ○ ] sound (♭ p₁) x∈p₁′ >>= y∈p₂x
sound (nonempty p) x∈p = nonempty (sound p x∈p)
sound (cast _ p)   x∈p = cast (sound p x∈p)

sound (return _) ()
sound fail       ()

------------------------------------------------------------------------
-- Completeness

mutual

  complete : ∀ {Tok R xs x s t} {p : Parser Tok R xs} →
             x ∈ p · t ∷ s → x ∈ D t p · s
  complete x∈p = complete′ _ x∈p refl

  complete′ : ∀ {Tok R xs x s s′ t} (p : Parser Tok R xs) →
                x ∈ p · s′ → s′ ≡ t ∷ s → x ∈ D t p · s
  complete′ token     token       refl = return

  complete′ (p₁ ∣ p₂) (∣-left    x∈p₁) refl = ∣-left               (complete x∈p₁)
  complete′ (p₁ ∣ p₂) (∣-right _ x∈p₂) refl = ∣-right (D-bag _ p₁) (complete x∈p₂)

  complete′ (f <$> p) (<$> x∈p)   refl = <$> complete x∈p

  complete′ (_⊛_ {fs = nothing} {xs = just _}  p₁ p₂)
            (_⊛_ {s₁ = _ ∷ _} f∈p₁ x∈p₂) refl =         _⊛_ {fs = ○} {xs = ○}  (complete f∈p₁) x∈p₂
  complete′ (_⊛_ {fs = just _}  {xs = just _}  p₁ p₂)
            (_⊛_ {s₁ = _ ∷ _} f∈p₁ x∈p₂) refl = ∣-left (_⊛_ {fs = ○} {xs = ○}  (complete f∈p₁) x∈p₂)
  complete′ (_⊛_ {fs = just _}  {xs = just xs} p₁ p₂)
            (_⊛_ {s₁ = []}    f∈p₁ x∈p₂) refl = ∣-right (D-bag _ p₁ ⊛′ xs)
                                                   (_⊛_ {fs = ○} {xs = ○}
                                                        (Return⋆.complete (I.complete f∈p₁)) (complete x∈p₂))
  complete′ (_⊛_ {fs = nothing} {xs = nothing} p₁ p₂)
            (_⊛_ {s₁ = _ ∷ _} f∈p₁ x∈p₂) refl =         _⊛_ {fs = ○} {xs = ◌} (complete f∈p₁) x∈p₂
  complete′ (_⊛_ {fs = just _}  {xs = nothing} p₁ p₂)
            (_⊛_ {s₁ = _ ∷ _} f∈p₁ x∈p₂) refl = ∣-left (_⊛_ {fs = ○} {xs = ◌} (complete f∈p₁) x∈p₂)
  complete′ (_⊛_ {fs = just _}  {xs = nothing} p₁ p₂)
            (_⊛_ {s₁ = []}    f∈p₁ x∈p₂) refl = ∣-right []
                                                   (_⊛_ {fs = ○} {xs = ○}
                                                        (Return⋆.complete (I.complete f∈p₁)) (complete x∈p₂))

  complete′ (_>>=_ {xs = nothing} {f = just _}  p₁ p₂)
            (_>>=_ {s₁ = _ ∷ _} x∈p₁ y∈p₂x) refl =         _>>=_ {xs = ○} {f = ○} (complete x∈p₁) y∈p₂x
  complete′ (_>>=_ {xs = just _}  {f = just _}  p₁ p₂)
            (_>>=_ {s₁ = _ ∷ _} x∈p₁ y∈p₂x) refl = ∣-left (_>>=_ {xs = ○} {f = ○} (complete x∈p₁) y∈p₂x)
  complete′ (_>>=_ {xs = just _}  {f = just f}  p₁ p₂)
            (_>>=_ {s₁ = []}    x∈p₁ y∈p₂x) refl = ∣-right (D-bag _ p₁ >>=′ f)
                                                      (_>>=_ {xs = ○} {f = ○}
                                                             (Return⋆.complete (I.complete x∈p₁)) (complete y∈p₂x))

  complete′ (_>>=_ {xs = nothing} {f = nothing} p₁ p₂)
            (_>>=_ {s₁ = _ ∷ _} x∈p₁ y∈p₂x) refl =         _>>=_ {xs = ○} {f = ◌} (complete x∈p₁) y∈p₂x
  complete′ (_>>=_ {xs = just _}  {f = nothing} p₁ p₂)
            (_>>=_ {s₁ = _ ∷ _} x∈p₁ y∈p₂x) refl = ∣-left (_>>=_ {xs = ○} {f = ◌} (complete x∈p₁) y∈p₂x)
  complete′ (_>>=_ {xs = just _}  {f = nothing} p₁ p₂)
            (_>>=_ {s₁ = []}    x∈p₁ y∈p₂x) refl = ∣-right []
                                                      (_>>=_ {xs = ○} {f = ○}
                                                             (Return⋆.complete (I.complete x∈p₁)) (complete y∈p₂x))

  complete′ (nonempty p) (nonempty x∈p) refl = complete x∈p

  complete′ (cast _ p) (cast x∈p) refl = complete x∈p

  complete′ (return _) () refl
  complete′ fail       () refl
  complete′ (_⊛_   {fs = nothing} _ _) (_⊛_   {s₁ = []} f∈p₁ _) _ with I.complete f∈p₁
  ... | ()
  complete′ (_>>=_ {xs = nothing} _ _) (_>>=_ {s₁ = []} x∈p₁ _) _ with I.complete x∈p₁
  ... | ()

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module _ where

id : {A : Set} → A → A
id x = x

const : {A : Set₁} {B : Set} → A → (B → A)
const x = λ _ → x

{-# DISPLAY const x y = x #-}

infixr 4 _,_
infixr 2 _×_

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

_×_ : (A B : Set) → Set
A × B = Σ A (const B)

Σ-map : ∀ {A B : Set} {P : A → Set} {Q : B → Set} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ A P → Σ B Q
Σ-map f g = λ p → (f (proj₁ p) , g (proj₂ p))

foo : {A B : Set} → A × B → A × B
foo = Σ-map id {!!}


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

module Cubical.Algebra.CommRing.Instances.UnivariatePoly where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Polynomials.Univariate.Base
open import Cubical.Algebra.Polynomials.Univariate.Properties

private
  variable
    ℓ : Level

UnivariatePoly : (CommRing ℓ) → CommRing ℓ
UnivariatePoly R = (PolyMod.Poly R) , str
    where
      open CommRingStr --(snd R)
      str : CommRingStr (PolyMod.Poly R)
      0r str = PolyModTheory.0P R
      1r str = PolyModTheory.1P R
      _+_ str = PolyModTheory._Poly+_ R
      _·_ str = PolyModTheory._Poly*_ R
      - str = PolyModTheory.Poly- R
      isCommRing str = makeIsCommRing (PolyMod.isSetPoly R)
                                      (PolyModTheory.Poly+Assoc R)
                                      (PolyModTheory.Poly+Rid R)
                                      (PolyModTheory.Poly+Inverses R)
                                      (PolyModTheory.Poly+Comm  R)
                                      (PolyModTheory.Poly*Associative R)
                                      (PolyModTheory.Poly*Rid R)
                                      (PolyModTheory.Poly*LDistrPoly+ R)
                                      (PolyModTheory.Poly*Commutative R)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{- This example used to fail but after the point-free evaluation fix
   it seems to work #-}
module Issue259c where

postulate
  A : Set
  a : A
  b : ({x : A} → A) → A
  C : A → Set

d : {x : A} → A
d {x} = a

e : A
e = b (λ {x} → d {x})

F : C e → Set₁
F _ with Set
F _ | _ = Set


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

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

isPropUnit : isProp Unit
isPropUnit _ _ i = tt -- definitionally equal to: isContr→isProp isContrUnit

isOfHLevelUnit : (n : ℕ) → isOfHLevel n Unit
isOfHLevelUnit n = isContr→isOfHLevel n isContrUnit

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
-- The NO_POSITIVITY_CHECK pragma is not allowed in safe mode.

module Issue1614a where

{-# NO_POSITIVITY_CHECK #-}
data D : Set where
  lam : (D → D) → D


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

module BottomBottom where

open import Common.FOL.FOL

postulate bot bot' : ⊥
{-# ATP prove bot bot' #-}
{-# ATP prove bot' bot #-}

-- $ apia-fot BottomBottom.agda
-- Proving the conjecture in /tmp/BottomBottom/8-bot.tptp ...
-- Vampire 0.6 (revision 903) proved the conjecture
-- Proving the conjecture in /tmp/BottomBottom/8-bot39.tptp ...
-- Vampire 0.6 (revision 903) proved the conjecture

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------------
-- The gcd is a common divisor
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Partial.CommonDivisorATP where

open import FOTC.Base
open import FOTC.Base.PropertiesATP
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Divisibility.NotBy0
open import FOTC.Data.Nat.Divisibility.NotBy0.PropertiesATP
open import FOTC.Data.Nat.Induction.NonAcc.LexicographicATP
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesATP
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.PropertiesATP
open import FOTC.Program.GCD.Partial.Definitions
open import FOTC.Program.GCD.Partial.GCD
open import FOTC.Program.GCD.Partial.TotalityATP

------------------------------------------------------------------------------
-- Some cases of the gcd-∣₁.

-- We don't prove that
--
-- gcd-∣₁ : ... → (gcd m n) ∣ m

-- because this proof should be defined mutually recursive with the
-- proof
--
-- gcd-∣₂ : ... → (gcd m n) ∣ n.
--
-- Therefore, instead of proving
--
-- gcdCD : ... → CD m n (gcd m n)
--
-- using these proofs (i.e. the conjunction of them), we proved it
-- using well-founded induction.

-- gcd 0 (succ n) ∣ 0.
postulate gcd-0S-∣₁ : ∀ {n} → N n → gcd zero (succ₁ n) ∣ zero
{-# ATP prove gcd-0S-∣₁ #-}

-- gcd (succ₁ m) 0 ∣ succ₁ m.
postulate gcd-S0-∣₁ : ∀ {n} → N n → gcd (succ₁ n) zero ∣ succ₁ n
{-# ATP prove gcd-S0-∣₁ ∣-refl-S #-}

-- gcd (succ₁ m) (succ₁ n) ∣ succ₁ m, when succ₁ m ≯ succ₁ n.
postulate gcd-S≯S-∣₁ : ∀ {m n} → N m → N n →
                       (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ succ₁ m) →
                       succ₁ m ≯ succ₁ n →
                       gcd (succ₁ m) (succ₁ n) ∣ succ₁ m
{-# ATP prove gcd-S≯S-∣₁ #-}

-- gcd (succ₁ m) (succ₁ n) ∣ succ₁ m when succ₁ m > succ₁ n.
{- Proof:
1. gcd (Sm ∸ Sn) Sn | (Sm ∸ Sn)        IH
2. gcd (Sm ∸ Sn) Sn | Sn               gcd-∣₂
3. gcd (Sm ∸ Sn) Sn | (Sm ∸ Sn) + Sn   m∣n→m∣o→m∣n+o 1,2
4. Sm > Sn                             Hip
5. gcd (Sm ∸ Sn) Sn | Sm               arith-gcd-m>n₂ 3,4
6. gcd Sm Sn = gcd (Sm ∸ Sn) Sn        gcd eq. 4
7. gcd Sm Sn | Sm                      subst 5,6
-}

-- For the proof using the ATP we added the helper hypothesis:
-- 1. gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ (succ₁ m ∸ succ₁ n) + succ₁ n.
-- 2. (succ₁ m ∸ succ₁ n) + succ₁ n ≡ succ₁ m.
postulate
  gcd-S>S-∣₁-ah :
    ∀ {m n} → N m → N n →
    (gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ (succ₁ m ∸ succ₁ n)) →
    (gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ succ₁ n) →
    succ₁ m > succ₁ n →
    gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ (succ₁ m ∸ succ₁ n) + succ₁ n →
    ((succ₁ m ∸ succ₁ n) + succ₁ n ≡ succ₁ m) →
    gcd (succ₁ m) (succ₁ n) ∣ succ₁ m
{-# ATP prove gcd-S>S-∣₁-ah #-}

gcd-S>S-∣₁ :
  ∀ {m n} → N m → N n →
  (gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ (succ₁ m ∸ succ₁ n)) →
  (gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ succ₁ n) →
  succ₁ m > succ₁ n →
  gcd (succ₁ m) (succ₁ n) ∣ succ₁ m
gcd-S>S-∣₁ {m} {n} Nm Nn ih gcd-∣₂ Sm>Sn =
  gcd-S>S-∣₁-ah Nm Nn ih gcd-∣₂ Sm>Sn
    (x∣y→x∣z→x∣y+z gcd-Sm-Sn,Sn-N Sm-Sn-N (nsucc Nn) ih gcd-∣₂)
    (x>y→x∸y+y≡x (nsucc Nm) (nsucc Nn) Sm>Sn)

  where
  Sm-Sn-N : N (succ₁ m ∸ succ₁ n)
  Sm-Sn-N = ∸-N (nsucc Nm) (nsucc Nn)

  gcd-Sm-Sn,Sn-N : N (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))
  gcd-Sm-Sn,Sn-N = gcd-N Sm-Sn-N (nsucc Nn) (λ p → ⊥-elim (S≢0 (∧-proj₂ p)))

------------------------------------------------------------------------------
-- Some case of the gcd-∣₂.
-- We don't prove that gcd-∣₂ : ... → gcd m n ∣ n. The reason is
-- the same to don't prove gcd-∣₁ : ... → gcd m n ∣ m.

-- gcd 0 (succ₁ n) ∣₂ succ₁ n.
postulate gcd-0S-∣₂ : ∀ {n} → N n → gcd zero (succ₁ n) ∣ succ₁ n
{-# ATP prove gcd-0S-∣₂ ∣-refl-S #-}

-- gcd (succ₁ m) 0 ∣ 0.
postulate gcd-S0-∣₂ : ∀ {m} → N m → gcd (succ₁ m) zero ∣ zero
{-# ATP prove gcd-S0-∣₂ #-}

-- gcd (succ₁ m) (succ₁ n) ∣ succ₁ n when succ₁ m ≯ succ₁ n.
{- Proof:
1. gcd Sm (Sn ∸ Sm) | (Sn ∸ Sm)        IH
2  gcd Sm (Sn ∸ Sm) | Sm               gcd-∣₁
3. gcd Sm (Sn ∸ Sm) | (Sn ∸ Sm) + Sm   m∣n→m∣o→m∣n+o 1,2
4. Sm ≯ Sn                             Hip
5. gcd (Sm ∸ Sn) Sn | Sm               arith-gcd-m≤n₂ 3,4
6. gcd Sm Sn = gcd Sm (Sn ∸ Sm)        gcd eq. 4
7. gcd Sm Sn | Sn                      subst 5,6
-}

-- For the proof using the ATP we added the helper hypothesis:
-- 1. gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ (succ₁ n ∸ succ₁ m) + succ₁ m.
-- 2 (succ₁ n ∸ succ₁ m) + succ₁ m ≡ succ₁ n.
postulate
  gcd-S≯S-∣₂-ah :
    ∀ {m n} → N m → N n →
    (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ (succ₁ n ∸ succ₁ m)) →
    (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ succ₁ m) →
    succ₁ m ≯ succ₁ n →
    (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ (succ₁ n ∸ succ₁ m) + succ₁ m) →
    ((succ₁ n ∸ succ₁ m) + succ₁ m ≡ succ₁ n) →
    gcd (succ₁ m) (succ₁ n) ∣ succ₁ n
{-# ATP prove gcd-S≯S-∣₂-ah #-}

gcd-S≯S-∣₂ :
  ∀ {m n} → N m → N n →
  (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ (succ₁ n ∸ succ₁ m)) →
  (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ succ₁ m) →
  succ₁ m ≯ succ₁ n →
  gcd (succ₁ m) (succ₁ n) ∣ succ₁ n
gcd-S≯S-∣₂ {m} {n} Nm Nn ih gcd-∣₁ Sm≯Sn =
  gcd-S≯S-∣₂-ah Nm Nn ih gcd-∣₁ Sm≯Sn
    (x∣y→x∣z→x∣y+z gcd-Sm,Sn-Sm-N Sn-Sm-N (nsucc Nm) ih gcd-∣₁)
    (x≤y→y∸x+x≡y (nsucc Nm) (nsucc Nn) (x≯y→x≤y (nsucc Nm) (nsucc Nn) Sm≯Sn))

  where
  Sn-Sm-N : N (succ₁ n ∸ succ₁ m)
  Sn-Sm-N = ∸-N (nsucc Nn) (nsucc Nm)

  gcd-Sm,Sn-Sm-N : N (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))
  gcd-Sm,Sn-Sm-N = gcd-N (nsucc Nm) (Sn-Sm-N) (λ p → ⊥-elim (S≢0 (∧-proj₁ p)))

-- gcd (succ₁ m) (succ₁ n) ∣ succ₁ n when succ₁ m > succ₁ n.
postulate gcd-S>S-∣₂ : ∀ {m n} → N m → N n →
                       (gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ succ₁ n) →
                       succ₁ m > succ₁ n →
                       gcd (succ₁ m) (succ₁ n) ∣ succ₁ n
{-# ATP prove gcd-S>S-∣₂ #-}

------------------------------------------------------------------------------
-- The gcd is CD.
-- We will prove that gcdCD : ... → CD m n (gcd m n).

-- The gcd 0 (succ₁ n) is CD.
gcd-0S-CD : ∀ {n} → N n → CD zero (succ₁ n) (gcd zero (succ₁ n))
gcd-0S-CD Nn = (gcd-0S-∣₁ Nn , gcd-0S-∣₂ Nn)

-- The gcd (succ₁ m) 0 is CD.
gcd-S0-CD : ∀ {m} → N m → CD (succ₁ m) zero (gcd (succ₁ m) zero)
gcd-S0-CD Nm = (gcd-S0-∣₁ Nm , gcd-S0-∣₂ Nm)

-- The gcd (succ₁ m) (succ₁ n) when succ₁ m > succ₁ n is CD.
gcd-S>S-CD :
  ∀ {m n} → N m → N n →
  (CD (succ₁ m ∸ succ₁ n) (succ₁ n) (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))) →
  succ₁ m > succ₁ n →
  CD (succ₁ m) (succ₁ n) (gcd (succ₁ m) (succ₁ n))
gcd-S>S-CD {m} {n} Nm Nn acc Sm>Sn =
   (gcd-S>S-∣₁ Nm Nn acc-∣₁ acc-∣₂ Sm>Sn , gcd-S>S-∣₂ Nm Nn acc-∣₂ Sm>Sn)
  where
  acc-∣₁ : gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ (succ₁ m ∸ succ₁ n)
  acc-∣₁ = ∧-proj₁ acc

  acc-∣₂ : gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ succ₁ n
  acc-∣₂ = ∧-proj₂ acc

-- The gcd (succ₁ m) (succ₁ n) when succ₁ m ≯ succ₁ n is CD.
gcd-S≯S-CD :
  ∀ {m n} → N m → N n →
  (CD (succ₁ m) (succ₁ n ∸ succ₁ m) (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))) →
  succ₁ m ≯ succ₁ n →
  CD (succ₁ m) (succ₁ n) (gcd (succ₁ m) (succ₁ n))
gcd-S≯S-CD {m} {n} Nm Nn acc Sm≯Sn =
  (gcd-S≯S-∣₁ Nm Nn acc-∣₁ Sm≯Sn , gcd-S≯S-∣₂ Nm Nn acc-∣₂ acc-∣₁ Sm≯Sn)
  where
  acc-∣₁ : gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ succ₁ m
  acc-∣₁ = ∧-proj₁ acc

  acc-∣₂ : gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ (succ₁ n ∸ succ₁ m)
  acc-∣₂ = ∧-proj₂ acc

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

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

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

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


text:
-- A DSL example in the language Agda: "polynomial types"
module TypeDSL where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Data.Nat

data E : Set1 where
  Add   : E -> E -> E
  Mul   : E -> E -> E
  Zero  : E
  One   : E

eval : E -> Set
eval (Add x y)  = (eval x) ⊎ (eval y)
eval (Mul x y)  = (eval x) × (eval y)
eval Zero       = ⊥
eval One        = ⊤

two   = Add One One
three = Add One two

test1 : eval One
test1 = tt

false : eval two
false = inj₁ tt
true : eval two
true = inj₂ tt

test3 : eval three
test3 = inj₁ tt

card : E -> ℕ
card (Add x y)  = card x + card y
card (Mul x y)  = card x * card y
card Zero       = 0
card One        = 1

open import Data.Vec as V

variable
    m n : ℕ
    A B : Set

enumAdd : Vec A m -> Vec B n -> Vec (A ⊎ B) (m + n)
enumAdd xs ys = V.map inj₁ xs ++ V.map inj₂ ys

-- cartesianProduct
enumMul : Vec A m → Vec B n → Vec (A × B) (m * n)
enumMul xs ys = concat (V.map  (\a -> V.map  ((a ,_)) ys)  xs)

enumerate : (t : E) -> Vec (eval t) (card t)
enumerate (Add x y)  =  enumAdd  (enumerate x) (enumerate y)
enumerate (Mul x y)  =  enumMul  (enumerate x) (enumerate y)
enumerate Zero       =  []
enumerate One        =  [ tt ]

test : Vec (eval three) 3
test = enumerate three
-- inj₁ tt ∷ inj₂ (inj₁ tt) ∷ inj₂ (inj₂ tt) ∷ []

-- Exercise: add a constructor for function types to the syntax E

max_stars_repo_name: felixwellen/DSLsofMath

max_issues_repo_name: felixwellen/DSLsofMath

max_forks_repo_name: felixwellen/DSLsofMath


text:
module _ where

open import Agda.Builtin.List
open import Agda.Builtin.Nat hiding (_==_)
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool

infix -1 _,_
record _×_ {a} (A B : Set a) : Set a where
  constructor _,_
  field fst : A
        snd : B
open _×_

data Constraint : Set₁ where
  mkConstraint : {A : Set} (x y : A) → x ≡ y → Constraint

infix 0 _==_
pattern _==_ x y = mkConstraint x y refl

infixr 5 _++_
_++_ : {A : Set} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

deepId : {A : Set} → List A → List A
deepId []       = []
deepId (x ∷ xs) = x ∷ deepId xs

nil : Constraint
nil = _ ++ [] == 1 ∷ 2 ∷ []

neutral : List Nat → Constraint
neutral ys = _ ++ deepId ys == 1 ∷ 2 ∷ deepId ys

spine : (ys zs : List Nat) → Constraint
spine ys zs = _ ++ zs == 1 ∷ ys ++ zs

N-ary : Nat → Set → Set
N-ary zero    A = A
N-ary (suc n) A = A → N-ary n A

foo : N-ary _ Nat
foo = λ x y z → x

sum : (n : Nat) → Nat → N-ary n Nat
sum zero    m = m
sum (suc n) m = λ p → sum n (m + p)

nary-sum : Nat
nary-sum = sum _ 1 2 3 4

plus : Nat → Constraint
plus n = _ + n == 2 + n

plus-lit : Constraint
plus-lit = _ + 0 == 3

dont-fail : Nat → Nat → Constraint × Constraint
dont-fail n m =
  let X = _ in
  X + (m + 0) == n + (m + 0) , X == n

-- Harder problems --

data Color : Set where
  red green blue : Color

isRed : Color → Bool
isRed red   = true
isRed green = false
isRed blue  = false

non-unique : Constraint
non-unique = isRed _ == true

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

sumJust : Maybe Nat → Nat → Nat
sumJust nothing  _ = 0
sumJust (just x) n = x + n

unknown-head : Nat → Constraint
unknown-head n = sumJust _ n == n

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

{-# TERMINATING #-}
makeloop : {P : Prop} → P → P
makeloop p = makeloop p

postulate
  P : Prop
  p : P
  Q : P → Set

record X : Set where
  field
    f : Q (makeloop p)

data Y : Set where
  f : Q (makeloop p) → Y


text:
-- {-# OPTIONS -v reify:80 #-}

open import Common.Prelude
open import Common.Reflection
open import Common.Equality

module Issue1345 (A : Set) where

-- Andreas, 2016-07-17
-- Also test correct handling of abstract

abstract
  unquoteDecl idNat = define (vArg idNat)
    (funDef (pi (vArg (def (quote Nat) [])) (abs "" (def (quote Nat) [])))
            (clause (vArg (var "") ∷ []) (var 0 []) ∷ []))
  -- This raised the UselessAbstract error in error.
  -- Should work.

abstract
  thm : ∀ n → idNat n ≡ n
  thm n = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
open import Common.Prelude
open import TestHarness
open import TestBool using ( not; _∧_ ; _↔_ )

module TestNat where

_*_ : Nat → Nat → Nat
zero  * n = zero
suc m * n = n + (m * n)

{-# COMPILED_JS _*_ function (x) { return function (y) { return x*y; }; } #-}

fact : Nat → Nat
fact zero    = 1
fact (suc x) = suc x * fact x

_≟_ : Nat → Nat → Bool
zero  ≟ zero  = true
suc x ≟ suc y = x ≟ y
x     ≟ y     = false

{-# COMPILED_JS _≟_ function (x) { return function (y) { return x === y; }; } #-}

tests : Tests
tests _ = (
    assert (0 ≟ 0) "0=0" ,
    assert (not (0 ≟ 1)) "0≠1" ,
    assert ((1 + 2) ≟ 3) "1+2=3" ,
    assert ((2 ∸ 1) ≟ 1) "2∸1=1" ,
    assert ((1 ∸ 2) ≟ 0) "1∸2=0" ,
    assert ((2 * 3) ≟ 6) "2+3=6" ,
    assert (fact 0 ≟ 1) "0!=1" ,
    assert (fact 1 ≟ 1) "1!=1" ,
    assert (fact 2 ≟ 2) "2!=2" ,
    assert (fact 3 ≟ 6) "3!=6" ,
    assert (fact 4 ≟ 24) "4!=24"
  )

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing where the integers and some related
-- operations and properties are defined, and how they can be used
------------------------------------------------------------------------

module README.Integer where

-- The integers and various arithmetic operations are defined in
-- Data.Integer.

open import Data.Integer

-- The +_ function converts natural numbers into integers.

ex₁ : ℤ
ex₁ = + 2

-- The -_ function negates an integer.

ex₂ : ℤ
ex₂ = - + 4

-- Some binary operators are also defined, including addition,
-- subtraction and multiplication.

ex₃ : ℤ
ex₃ = + 1  +  + 3 * - + 2  -  + 4

-- Propositional equality and some related properties can be found
-- in Relation.Binary.PropositionalEquality.

open import Relation.Binary.PropositionalEquality as P using (_≡_)

ex₄ : ex₃ ≡ - + 9
ex₄ = P.refl

-- Data.Integer.Properties contains a number of properties related to
-- integers. Algebra defines what a commutative ring is, among other
-- things.

open import Algebra
import Data.Integer.Properties as Integer
private
  module CR = CommutativeRing Integer.commutativeRing

ex₅ : ∀ i j → i * j ≡ j * i
ex₅ i j = CR.*-comm i j

-- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
-- provides some combinators for equational reasoning.

open P.≡-Reasoning
open import Data.Product

ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
ex₆ i j = begin
  i * (j + + 0)  ≡⟨ P.cong (_*_ i) (proj₂ CR.+-identity j) ⟩
  i * j          ≡⟨ CR.*-comm i j ⟩
  j * i          ∎

-- The module RingSolver in Data.Integer.Properties contains a solver
-- for integer equalities involving variables, constants, _+_, _*_, -_
-- and _-_.

ex₇ : ∀ i j → i * - j - j * i ≡ - + 2 * i * j
ex₇ = solve 2 (λ i j → i :* :- j :- j :* i  :=  :- con (+ 2) :* i :* j)
              P.refl
  where open Integer.RingSolver


text:
-- Issue #80.

-- The disjunction data type.
data _∨_ (A B : Set) : Set where
  inj₁ : A → A ∨ B
  inj₂ : B → A ∨ B

-- A different symbol for disjunction.
_⊕_ : Set → Set → Set
P ⊕ Q = P ∨ Q
{-# ATP definition _⊕_ #-}

postulate
  P Q : Set
  ⊕-comm : P ⊕ Q → Q ⊕ P
{-# ATP prove ⊕-comm #-}

-- The previous error was:

-- $ apia Issue80.agda
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/Apia/Translation/Functions.hs:188

-- The current error is:

-- $ apia Issue80.agda
-- apia: the translation of ‘IssueXX._⊕_’ failed because it is not a FOL-definition

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- {-# OPTIONS -v tc.meta:20 #-}
module UnifyWithIrrelevantArgument where

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

fail : (A : Set) ->
       let X : .A -> A
           X = _
       in  (x : A) -> X x ≡ x
fail A x = refl
-- error: X cannot depend on its first argument


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

open import LogicalFormulae
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Lists.Lists
open import Maybe

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

module Groups.Polynomials.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where

open Setoid S
open Equivalence eq
open Group G

NaivePoly : Set a
NaivePoly = List A

0P : NaivePoly
0P = []

polysEqual : NaivePoly → NaivePoly → Set (a ⊔ b)
polysEqual [] [] = True'
polysEqual [] (x :: b) = (x ∼ 0G) && polysEqual [] b
polysEqual (x :: a) [] = (x ∼ 0G) && polysEqual a []
polysEqual (x :: a) (y :: b) = (x ∼ y) && polysEqual a b

polysReflexive : {x : NaivePoly} → polysEqual x x
polysReflexive {[]} = record {}
polysReflexive {x :: y} = reflexive ,, polysReflexive

polysSymmetricZero : {x : NaivePoly} → polysEqual [] x → polysEqual x []
polysSymmetricZero {[]} 0=x = record {}
polysSymmetricZero {x :: y} (fst ,, snd) = fst ,, polysSymmetricZero snd

polysSymmetricZero' : {x : NaivePoly} → polysEqual x [] → polysEqual [] x
polysSymmetricZero' {[]} 0=x = record {}
polysSymmetricZero' {x :: y} (fst ,, snd) = fst ,, polysSymmetricZero' snd

polysSymmetric : {x y : NaivePoly} → polysEqual x y → polysEqual y x
polysSymmetric {[]} {y} x=y = polysSymmetricZero x=y
polysSymmetric {x :: xs} {[]} x=y = polysSymmetricZero' {x :: xs} x=y
polysSymmetric {x :: xs} {y :: ys} (fst ,, snd) = symmetric fst ,, polysSymmetric {xs} {ys} snd

polysTransitive : {x y z : NaivePoly} → polysEqual x y → polysEqual y z → polysEqual x z
polysTransitive {[]} {[]} {[]} x=y y=z = record {}
polysTransitive {[]} {[]} {x :: z} x=y y=z = y=z
polysTransitive {[]} {x :: y} {[]} (fst ,, snd) y=z = record {}
polysTransitive {[]} {x :: y} {x₁ :: z} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric fst2) fst ,, polysTransitive snd snd2
polysTransitive {x :: xs} {[]} {[]} x=y y=z = x=y
polysTransitive {x :: xs} {[]} {z :: zs} (fst ,, snd) (fst2 ,, snd2) = transitive fst (symmetric fst2) ,, polysTransitive snd snd2
polysTransitive {x :: xs} {y :: ys} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive fst fst2 ,, polysTransitive snd snd2
polysTransitive {x :: xs} {y :: ys} {z :: zs} (fst ,, snd) (fst2 ,, snd2) = transitive fst fst2 ,, polysTransitive snd snd2

naivePolySetoid : Setoid NaivePoly
Setoid._∼_ naivePolySetoid = polysEqual
Equivalence.reflexive (Setoid.eq naivePolySetoid) = polysReflexive
Equivalence.symmetric (Setoid.eq naivePolySetoid) = polysSymmetric
Equivalence.transitive (Setoid.eq naivePolySetoid) = polysTransitive

polyInjection : A → NaivePoly
polyInjection a = a :: []

polyInjectionIsInj : SetoidInjection S naivePolySetoid polyInjection
SetoidInjection.wellDefined polyInjectionIsInj x=y = x=y ,, record {}
SetoidInjection.injective polyInjectionIsInj {x} {y} (fst ,, snd) = fst

-- the zero polynomial has no degree
-- all other polynomials have a degree

degree : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False)) → NaivePoly → Maybe ℕ
degree decide [] = no
degree decide (x :: poly) with decide x
degree decide (x :: poly) | inl x=0 with degree decide poly
degree decide (x :: poly) | inl x=0 | no = no
degree decide (x :: poly) | inl x=0 | yes deg = yes (succ deg)
degree decide (x :: poly) | inr x!=0 with degree decide poly
degree decide (x :: poly) | inr x!=0 | no = yes 0
degree decide (x :: poly) | inr x!=0 | yes n = yes (succ n)

degreeWellDefined : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) {x y : NaivePoly} → polysEqual x y → degree decide x ≡ degree decide y
degreeWellDefined decide {[]} {[]} x=y = refl
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) with decide x
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 with inspect (degree decide y)
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 | yes bad with≡ pr rewrite pr = exFalso (noNotYes (transitivity (degreeWellDefined decide {[]} {y} snd) pr))
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 with inspect (degree decide y)
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 | no with≡ pr rewrite pr = exFalso (x!=0 fst)
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 | yes deg with≡ pr rewrite pr = exFalso (x!=0 fst)
degreeWellDefined decide {x :: xs} {[]} x=y with decide x
degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 with inspect (degree decide xs)
degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 | yes bad with≡ pr rewrite pr = exFalso (noNotYes (transitivity (equalityCommutative (degreeWellDefined decide snd)) pr))
degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inr x!=0 = exFalso (x!=0 fst)
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) with decide x
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 with decide y
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 with inspect (degree decide ys)
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 | no with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 | (yes th) with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inr y!=0 = exFalso (y!=0 (transitive (symmetric fst) x=0))
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 with decide y
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inl y=0 = exFalso (x!=0 (transitive fst y=0))
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 with inspect (degree decide ys)
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 | no with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 | yes x₁ with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl

degreeNoImpliesZero : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) → (a : NaivePoly) → degree decide a ≡ no → polysEqual a []
degreeNoImpliesZero decide [] not = record {}
degreeNoImpliesZero decide (x :: a) not with decide x
degreeNoImpliesZero decide (x :: a) not | inl x=0 with inspect (degree decide a)
degreeNoImpliesZero decide (x :: a) not | inl x=0 | no with≡ pr rewrite pr = x=0 ,, degreeNoImpliesZero decide a pr
degreeNoImpliesZero decide (x :: a) not | inl x=0 | (yes deg) with≡ pr rewrite pr = exFalso (noNotYes (equalityCommutative not))
degreeNoImpliesZero decide (x :: a) not | inr x!=0 with degree decide a
degreeNoImpliesZero decide (x :: a) () | inr x!=0 | no
degreeNoImpliesZero decide (x :: a) () | inr x!=0 | yes x₁

emptyImpliesDegreeZero : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) → (a : NaivePoly) → polysEqual a [] → degree decide a ≡ no
emptyImpliesDegreeZero decide [] a=[] = refl
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) with decide x
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 with inspect (degree decide a)
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 | (yes deg) with≡ pr rewrite pr = exFalso (noNotYes (transitivity (equalityCommutative (emptyImpliesDegreeZero decide a snd)) pr))
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inr x!=0 = exFalso (x!=0 fst)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- M-types (the dual of W-types)
------------------------------------------------------------------------

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

module Codata.M where

open import Size
open import Level
open import Codata.Thunk using (Thunk; force)
open import Data.Product hiding (map)
open import Data.Container.Core as C hiding (map)

data M {s p} (C : Container s p) (i : Size) : Set (s ⊔ p) where
  inf : ⟦ C ⟧ (Thunk (M C) i) → M C i

module _ {s p} {C : Container s p} where

  head : ∀ {i} → M C i → Shape C
  head (inf (x , f)) = x

  tail : (x : M C ∞) → Position C (head x) → M C ∞
  tail (inf (x , f)) = λ p → f p .force

-- map

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         (m : C₁ ⇒ C₂) where

  map : ∀ {i} → M C₁ i → M C₂ i
  map (inf t) = inf (⟪ m ⟫ (C.map (λ t → λ where .force → map (t .force)) t))

-- unfold

module _ {s p ℓ} {C : Container s p} (open Container C)
         {S : Set ℓ} (alg : S → ⟦ C ⟧ S) where

  unfold : S → ∀ {i} → M C i
  unfold seed = let (x , next) = alg seed in
                inf (x , λ p → λ where .force → unfold (next p))


text:
module builtin where

open import Agda.Builtin.IO
open import Agda.Builtin.Unit
open import Agda.Builtin.String

postulate putStrLn : String -> IO ⊤

{-# COMPILE GHC putStrLn = putStrLn . Data.Text.unpack #-}

main : IO ⊤
main = putStrLn "hallo"

max_stars_repo_name: neosimsim/merkdas

max_issues_repo_name: neosimsim/merkdas

max_forks_repo_name: neosimsim/merkdas


text:
import MJ.Classtable

import MJ.Syntax.Untyped as Syntax
import MJ.Classtable.Core as Core

module MJ.Semantics.Smallstep {c} (Ct : Core.Classtable c)(ℂ : Syntax.Classes Ct) where

open import Prelude

open import Data.Vec as V hiding (init; _>>=_; _∈_; _[_]=_)
open import Data.Vec.All.Properties.Extra as Vec∀++
open import Data.Sum
open import Data.String
open import Data.List.Most as List
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Relation.Nullary.Decidable
open import Data.Star hiding (return; _>>=_)

import Data.Vec.All as Vec∀

open Syntax Ct
open Core c
open Classtable Ct
open import MJ.Classtable.Membership Ct

open import MJ.Types

{-}
-- fragment of a typed smallstep semantics;
-- this is tedious, because there are so many indices to repeat and keep track of

readvar : ∀ {W Γ a} → Var Γ a → Env Γ W → Store W → Val W a
readvar v E μ = {!!}

data Cont (Γ : Ctx) : Ty c → Ty c → Set where
  k-iopₗ : ∀ {a} → NativeBinOp → Cont int a → Expr Γ

data State : Ty c → Set where
  exp  : ∀ {Γ W a b} → Store W → Env Γ W → Expr Γ a → Cont a b → State b
  skip : ∀ {Γ W a b} → Store W → Env Γ W → Val W a → Cont a b → State b

data _⟶_ {b} : State b → State b → Set where

  exp-var : ∀ {W Γ a}{μ : Store W}{E : Env Γ W}{x k} →
    exp μ E (var {a = a} x) k ⟶ skip μ E (readvar x E μ) k

  iopₗ     : ∀ {W Γ a}{μ : Store W}{E : Env Γ W}{x k l r f} →
    exp μ E (iop f l r) k ⟶ k-iopₗ
-}

Loc = ℕ

data Val : Set where
  num  : ℕ → Val
  unit : Val
  null : Val
  ref  : Cid c → Loc → Val

default : Ty c → Val
default a = {!!}

data StoreVal : Set where
  val  : Val → StoreVal

Env : ℕ → Set
Env = Vec Val

Store = List StoreVal

data Focus (n : ℕ) : ℕ → Set where
  stmt : ∀ {o} → Stmt n o → Focus n o
  continue : Focus n n
  exp  : Expr n → Focus n n
  val  : Val    → Focus n n
  vals : List Val → Focus n n

data Cont (n : ℕ) : Set where
  k-done : Cont n
  k-iopₗ  : NativeBinOp → Cont n → Expr n → Cont n
  k-iopᵣ  : NativeBinOp → Val → Cont n → Cont n
  k-new  : Cid c → Cont n → Cont n
  k-args  : List Val → List (Expr n) → Cont n → Cont n
  k-get  : String → Cont n → Cont n
  k-call : String → Cont n → Cont n

  k-asgn : Fin n → Cont n → Cont n
  k-seq  : ∀ {o} → Stmts n o → Cont o → Cont n
  k-set₁ : String → Expr n → Cont n → Cont n
  k-set₂ : Val → String → Cont n → Cont n

data Config : Set where
  ⟨_,_,_,_⟩ : ∀ {n o} → Store → Env n → Focus n o → Cont o → Config

data _⟶_ : Config → Config → Set where
  ----
  -- expressions
  ----

  num : ∀ {n}{E : Env n}{μ i k} →
    ⟨ μ , E , exp (num i) , k ⟩ ⟶ ⟨ μ , E , val (num i) , k ⟩
  unit : ∀ {n}{E : Env n}{μ k} →
    ⟨ μ , E , exp unit , k ⟩ ⟶ ⟨ μ , E , val unit , k ⟩
  null : ∀ {n}{E : Env n}{μ k} →
    ⟨ μ , E , exp null , k ⟩ ⟶ ⟨ μ , E , val null , k ⟩

  var : ∀ {n}{E : Env n}{μ x k ℓ v} →
    μ [ ℓ ]= (val v) →
    ⟨ μ , E , exp (var x) , k ⟩ ⟶ ⟨ μ , E , val v , k ⟩

  iopₗ     : ∀ {n}{E : Env n}{μ k f l r} →
    ⟨ μ , E , exp (iop f l r) , k ⟩ ⟶ ⟨ μ , E , exp l , k-iopₗ f k r ⟩
  iopᵣ     : ∀ {n}{E : Env n}{μ k f v r} →
    ⟨ μ , E , val v , (k-iopₗ f k r) ⟩ ⟶ ⟨ μ , E , exp r , k-iopᵣ f v k ⟩
  iop-red : ∀ {n}{E : Env n}{μ k f vᵣ vₗ} →
    ⟨ μ , E , val (num vᵣ) , (k-iopᵣ f (num vₗ) k) ⟩ ⟶ ⟨ μ , E , val (num (f vₗ vᵣ)) , k ⟩

  new : ∀ {n}{E : Env n}{μ k cid e es} →
    ⟨ μ , E , exp (new cid (e ∷ es)), k ⟩ ⟶ ⟨ μ , E , exp e , k-args [] es (k-new cid k) ⟩
  new-nil : ∀ {n}{E : Env n}{μ k cid} →
    ⟨ μ , E , exp (new cid []), k ⟩ ⟶ ⟨ μ List.∷ʳ {!!} , E , {!!} , k ⟩
  new-red : ∀ {n}{E : Env n}{μ k cid vs} →
    ⟨ μ , E , vals vs , k-new cid k ⟩ ⟶ ⟨ μ List.∷ʳ {!!} , E , {!!} , k ⟩

  args : ∀ {n}{E : Env n}{μ k e es v vs} →
    ⟨ μ , E , val v , k-args vs (e ∷ es) k ⟩ ⟶ ⟨ μ , E , exp e , k-args (vs List.∷ʳ v) es k ⟩
  args-red : ∀ {n}{E : Env n}{μ k v vs} →
    ⟨ μ , E , val v , k-args vs [] k ⟩ ⟶ ⟨ μ , E , vals (vs List.∷ʳ v) , k ⟩

  get : ∀ {n}{E : Env n}{μ k e m} →
    ⟨ μ , E , exp (get e m) , k ⟩ ⟶ ⟨ μ , E , exp e , k-get m k ⟩
  get-red : ∀ {n}{E : Env n}{μ k c o m} →
    ⟨ μ , E , val (ref c o) , k-get m k ⟩ ⟶ ⟨ μ , E , {!!} , k ⟩

  call : ∀ {n}{E : Env n}{μ k e m args} →
    ⟨ μ , E , exp (call e m args), k ⟩ ⟶ ⟨ μ , E , exp e , k-args [] args (k-call m k) ⟩
  call-red : ∀ {n}{E : Env n}{μ k m v vs} →
    ⟨ μ , E , vals (v ∷ vs) , k-call m k ⟩ ⟶ ⟨ μ , E , {!!} , k ⟩

  ----
  -- statements
  ----

  next : ∀ {n}{E : Env n}{μ j o}{s : Stmt n j}{st : Stmts j o}{k} →
    ⟨ μ , E , continue , k-seq (s ◅ st) k ⟩ ⟶ ⟨ μ , E , stmt s , k-seq st k ⟩

  loc  : ∀ {n}{E : Env n}{μ k a} →
    ⟨ μ , E , stmt (loc a) , k ⟩ ⟶ ⟨ μ , default a ∷ E , continue , k ⟩

  asgn : ∀ {n}{E : Env n}{μ k e x} →
    ⟨ μ , E , stmt (asgn x e) , k ⟩ ⟶ ⟨ μ , E , exp e , k-asgn x k ⟩
  asgn-red : ∀ {n}{E : Env n}{μ k v x} →
    ⟨ μ , E , val v , k-asgn x k ⟩ ⟶ ⟨ μ , (E V.[ x ]≔ v) , continue , k ⟩

  set₁ : ∀ {n}{E : Env n}{μ m k e e'} →
    ⟨ μ , E , stmt (set e m e') , k ⟩ ⟶ ⟨ μ , E , exp e , k-set₁ m e' k ⟩
  set₂ : ∀ {n}{E : Env n}{μ m k v e'} →
    ⟨ μ , E , val v , k-set₁ m e' k ⟩ ⟶ ⟨ μ , E , exp e' , k-set₂ v m k ⟩
  set-red : ∀ {n}{E : Env n}{μ μ' m C k v o O} →
    maybe-lookup     o μ ≡ just O →
    maybe-write o {!!} μ ≡ just μ' →
    ⟨ μ , E , val v , k-set₂ (ref C o) m k ⟩ ⟶ ⟨ μ' , E , continue , k ⟩

-- A few useful predicates on configurations

Stuck : Config → Set
Stuck φ = ¬ ∃ λ φ' → φ ⟶ φ'

data Done : Config → Set where
  done : ∀ {n}{E : Env n}{μ v} → Done ⟨ μ , E , val v , k-done ⟩

-- reflexive, transitive-closure of step
_⟶ₖ_ : Config → Config → Set
_⟶ₖ_ = Star _⟶_


text:
{-# OPTIONS -WnoMissingDefinitions #-}

postulate
  A : Set
  B : A → Set

variable
  a : A

data D : B a → Set

-- Expected: Warning about missing definition
-- Not expected: Complaint about generalizable variable


text:
-- Andreas, 2017-01-01, issue 2372, reported by m0davis

open import Issue2372Inst

f : r → Set₁
f _ = Set

-- WAS: No instance of type R was found in scope.

-- Should succeed


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Data.Vec.OperationsNat where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat renaming(_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec.Base
open import Cubical.Data.Sigma

private variable
  ℓ : Level

_+n-vec_ : {m : ℕ} → Vec ℕ m → Vec ℕ m → Vec ℕ m
_+n-vec_ {.zero} [] [] = []
_+n-vec_ {.(suc _)} (k ∷ v) (l ∷ v') = (k +n l) ∷ (v +n-vec v')

+n-vec-lid : {m : ℕ} → (v : Vec ℕ m) → replicate 0 +n-vec v ≡ v
+n-vec-lid {.zero} [] = refl
+n-vec-lid {.(suc _)} (k ∷ v) = cong (_∷_ k) (+n-vec-lid v)

+n-vec-rid : {m : ℕ} → (v : Vec ℕ m) → v +n-vec replicate 0 ≡ v
+n-vec-rid {.zero} [] = refl
+n-vec-rid {.(suc _)} (k ∷ v) = cong₂ _∷_ (+-zero k) (+n-vec-rid v)

+n-vec-assoc : {m : ℕ} → (v v' v'' : Vec ℕ m) → v +n-vec (v' +n-vec v'') ≡ (v +n-vec v') +n-vec v''
+n-vec-assoc [] [] [] = refl
+n-vec-assoc (k ∷ v) (l ∷ v') (p ∷ v'') = cong₂ _∷_ (+-assoc k l p) (+n-vec-assoc v v' v'')

+n-vec-comm : {m : ℕ} → (v v' : Vec ℕ m) → v +n-vec v' ≡ v' +n-vec v
+n-vec-comm {.zero} [] [] = refl
+n-vec-comm {.(suc _)} (k ∷ v) (l ∷ v') = cong₂ _∷_ (+-comm k l) (+n-vec-comm v v')

sep-vec : (k l : ℕ) → Vec ℕ (k +n l) → (Vec ℕ k) ×  (Vec ℕ l )
sep-vec zero l v = [] , v
sep-vec (suc k) l (x ∷ v) = (x ∷ fst (sep-vec k l v)) , (snd (sep-vec k l v))

sep-vec-fst : (k l : ℕ) → (v : Vec ℕ k) → (v' : Vec ℕ l) → fst (sep-vec k l (v ++ v')) ≡ v
sep-vec-fst zero l [] v' = refl
sep-vec-fst (suc k) l (x ∷ v) v' = cong (λ X → x ∷ X) (sep-vec-fst k l v v')

sep-vec-snd : (k l : ℕ) → (v : Vec ℕ k) → (v' : Vec ℕ l) → snd (sep-vec k l (v ++ v')) ≡ v'
sep-vec-snd zero l [] v' = refl
sep-vec-snd (suc k) l (x ∷ v) v' = sep-vec-snd k l v v'

sep-vec-id : (k l : ℕ) → (v : Vec ℕ (k +n l)) → fst (sep-vec k l v) ++ snd (sep-vec k l v) ≡ v
sep-vec-id zero l v = refl
sep-vec-id (suc k) l (x ∷ v) = cong (λ X → x ∷ X) (sep-vec-id k l v)

rep-concat : (k l : ℕ) → {B : Type ℓ} → (b : B) →
             replicate {_} {k} {B} b ++ replicate {_} {l} {B} b ≡ replicate {_} {k +n l} {B} b
rep-concat zero l b = refl
rep-concat (suc k) l b = cong (λ X → b ∷ X) (rep-concat k l b)

+n-vec-concat : (k l : ℕ) → (v w : Vec ℕ k) → (v' w' : Vec ℕ l)
                → (v +n-vec w) ++ (v' +n-vec w') ≡ (v ++ v') +n-vec (w ++ w')
+n-vec-concat zero l [] [] v' w' = refl
+n-vec-concat (suc k) l (x ∷ v) (y ∷ w) v' w' = cong (λ X → x +n y ∷ X) (+n-vec-concat k l v w v' w')


text:
module Type.Dependent.Functions where

import      Lvl
open import Functional.Dependent
open import Type
open import Type.Dependent
open import Syntax.Function

module _ {ℓ₁ ℓ₂ ℓ₃}
         {A : Type{ℓ₁}}
         {B : A → Type{ℓ₂}}
         {C : ∀{x} → B(x) → Type{ℓ₃}}
         where
  _[Π]-∘_ : (∀{x} → Π(B(x))(C)) → (g : Π(A)(B)) → Π(A)(\x → C(Π.apply g x))
  Π.apply (f [Π]-∘ g) x = Π.apply f (Π.apply g x)

  depCurry : (Π(Σ A B) (C ∘ Σ.right)) → (Π A (a ↦ (Π(B(a)) C)))
  Π.apply (Π.apply (depCurry f) a) b = Π.apply f (intro a b)

  depUncurry : (Π A (a ↦ Π(B(a)) C)) → (Π(Σ A B) (C ∘ Σ.right))
  Π.apply (depUncurry f) (intro a b) = Π.apply(Π.apply f a) b

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
         {A₁ : Type{ℓ₁}}
         {B₁ : A₁ → Type{ℓ₂}}
         {A₂ : Type{ℓ₃}}
         {B₂ : A₂ → Type{ℓ₄}}
         where
  [Σ]-apply : (x : Σ(A₁)(B₁)) → (l : A₁ → A₂) → (r : B₁(Σ.left x) → B₂(l(Σ.left x))) → Σ(A₂)(B₂)
  [Σ]-apply x l r = intro(l(Σ.left x))(r(Σ.right x))

  [ℰ]-apply : (x : Σ(A₁)(B₁)) → {l : A₁ → A₂} → (r : B₁(Σ.left x) → B₂(l(Σ.left x))) → Σ(A₂)(B₂)
  [ℰ]-apply x {l} r = [Σ]-apply x l r

  [Σ]-map : (l : A₁ → A₂) → (∀{a} → B₁(a) → B₂(l(a))) → (Σ(A₁)(B₁) → Σ(A₂)(B₂))
  [Σ]-map l r (intro left right) = intro (l left) (r right)

  [ℰ]-map : ∀{l : A₁ → A₂} → (∀{a} → B₁(a) → B₂(l(a))) → (Σ(A₁)(B₁) → Σ(A₂)(B₂))
  [ℰ]-map {l} = [Σ]-map l

module _ {ℓ₁ ℓ₂ ℓ₃}
         {A : Type{ℓ₁}}
         {B₁ : A → Type{ℓ₂}}
         {B₂ : A → Type{ℓ₃}}
         where
  [Σ]-applyᵣ : (x : Σ(A)(B₁)) → (r : B₁(Σ.left x) → B₂(Σ.left x)) → Σ(A)(B₂)
  [Σ]-applyᵣ x r = intro(Σ.left x)(r(Σ.right x))

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆}
         {A₁ : Type{ℓ₁}}
         {B₁ : A₁ → Type{ℓ₂}}
         {A₂ : Type{ℓ₃}}
         {B₂ : A₂ → Type{ℓ₄}}
         {A₃ : Type{ℓ₅}}
         {B₃ : A₃ → Type{ℓ₆}}
         where
  [Σ]-apply₂ : (x : Σ(A₁)(B₁)) → (y : Σ(A₂)(B₂)) → (l : A₁ → A₂ → A₃) → (r : B₁(Σ.left x) → B₂(Σ.left y) → B₃(l(Σ.left x)(Σ.left y))) → Σ(A₃)(B₃)
  [Σ]-apply₂ x y l r = intro(l(Σ.left x)(Σ.left y))(r(Σ.right x)(Σ.right y))

  [ℰ]-apply₂ : (x : Σ(A₁)(B₁)) → (y : Σ(A₂)(B₂)) → {l : A₁ → A₂ → A₃} → (r : B₁(Σ.left x) → B₂(Σ.left y) → B₃(l(Σ.left x)(Σ.left y))) → Σ(A₃)(B₃)
  [ℰ]-apply₂ x y {l} r = [Σ]-apply₂ x y l r

  [Σ]-map₂ : (l : A₁ → A₂ → A₃) → (∀{a₁}{a₂} → B₁(a₁) → B₂(a₂) → B₃(l a₁ a₂)) → (Σ(A₁)(B₁) → Σ(A₂)(B₂) → Σ(A₃)(B₃))
  [Σ]-map₂ l r (intro left₁ right₁) (intro left₂ right₂) = intro (l left₁ left₂) (r right₁ right₂)

  [ℰ]-map₂ : ∀{l : A₁ → A₂ → A₃} → (∀{a₁}{a₂} → B₁(a₁) → B₂(a₂) → B₃(l a₁ a₂)) → (Σ(A₁)(B₁) → Σ(A₂)(B₂) → Σ(A₃)(B₃))
  [ℰ]-map₂ {l} = [Σ]-map₂ l

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda