text:
module plfa-exercises.part1.Decidable where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; pred)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using ()
  renaming (contradiction to ¬¬-intro)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import plfa.part1.Relations using (_<_; z<s; s<s)
open import plfa.part1.Isomorphism using (_⇔_)
open import Function.Base using (_∘_)

infix 4 _≤_

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

_ : 2 ≤ 4
_ = s≤s (s≤s z≤n)

¬4≤2 : ¬ (4 ≤ 2)
--¬4≤2 (s≤s (s≤s ())) = ? -- This causes Agda to die! TODO: Report
¬4≤2 (s≤s (s≤s ()))

data Bool : Set where
  true  : Bool
  false : Bool

infix 4 _≤ᵇ_

_≤ᵇ_ : ℕ → ℕ → Bool
zero ≤ᵇ n       =  true
suc m ≤ᵇ zero   =  false
suc m ≤ᵇ suc n  =  m ≤ᵇ n

_ : (2 ≤ᵇ 4) ≡ true
_ = refl
_ : (5 ≤ᵇ 4) ≡ false
_ = refl

T : Bool → Set
T true = ⊤
T false = ⊥

≤→≤ᵇ : ∀ {m n} → (m ≤ n) → T (m ≤ᵇ n)
≤→≤ᵇ z≤n = tt
≤→≤ᵇ (s≤s m≤n) = ≤→≤ᵇ m≤n

≤ᵇ→≤ : ∀ {m n} → T (m ≤ᵇ n) → (m ≤ n)
≤ᵇ→≤ {zero} {_} tt = z≤n
-- What is going on in here? Left `t` has type `T (suc m ≤ᵇ suc n)` and the right `t` has type `T (m ≤ᵇ n)`
-- λ m n → T (suc m ≤ᵇ suc n)   => reduces to:  λ m n → T (m ≤ᵇ n)
-- Ohh! Ok. It is because the third rule of `≤ᵇ` reduces `suc m ≤ᵇ suc n` to `m ≤ᵇ n`
≤ᵇ→≤ {suc m} {suc n} t = s≤s (≤ᵇ→≤ {m} {n} t)
-- λ m → T (suc m ≤ᵇ zero)   => reduces to:  λ m → ⊥
-- which means that there are no rules for `fromᵇ {suc m} {zero}`
≤ᵇ→≤ {suc m} {zero} ()

proof≡computation : ∀ {m n} → (m ≤ n) ⇔ T (m ≤ᵇ n)
proof≡computation {m} {n} =
  record
    { from = ≤ᵇ→≤
    ; to = ≤→≤ᵇ
    }

T→≡ : ∀ (b : Bool) → T b → b ≡ true
T→≡ true tt = refl
T→≡ false ()

--postulate
--  lie : false ≡ true

≡→T : ∀ {b : Bool} → b ≡ true → T b
--≡→T {false} refl = ? -- This is impossible because of refl's definition. Unification forces `b` to be `true`
--≡→T {false} rewrite lie = λ refl → ? -- Even postulating a lie, it is impossible to create a bottom value
≡→T refl = tt

_ : 2 ≤ 4
_ = ≤ᵇ→≤ tt

¬4≤2₂ : ¬ (4 ≤ 2)
--¬4≤2₂ 4≤2 = ≤→≤ᵇ 4≤2
--¬4≤2₂ = ≤→≤ᵇ {4} {2}
-- The type of `T (4 ≤ᵇ 2)` which reduces to `T false` and then `⊥`
¬4≤2₂ = ≤→≤ᵇ
-- Notice how defining ≤ᵇ lifts from us the demand of computing the correct
-- `evidence` (implementation) for the `proof` (function type)

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

¬s≤z : {m : ℕ} → ¬ (suc m) ≤ zero
--¬s≤z = ≤→≤ᵇ
¬s≤z ()

¬s≤s : {m n : ℕ} → ¬ m ≤ n → ¬ suc m ≤ suc n
¬s≤s ¬m≤n = λ { (s≤s m≤n) → ¬m≤n m≤n }

_≤?_ : (m n : ℕ) → Dec (m ≤ n)
zero    ≤? n       = yes z≤n
(suc m) ≤? zero    = no ¬s≤z
(suc m) ≤? (suc n) with m ≤? n
...                   | yes  m≤n = yes (s≤s m≤n)
...                   | no  ¬m≤n = no  (¬s≤s ¬m≤n)

-- `2 ≤? 4` reduces to `yes (s≤s (s≤s z≤n))`
_ : Dec (2 ≤ 4)
_ = 2 ≤? 4
_ = yes (s≤s (s≤s (z≤n {2})))

⌊_⌋ : ∀ {A : Set} → Dec A → Bool
⌊ yes x ⌋  =  true
⌊ no ¬x ⌋  =  false

_ : Bool
_ = true
_ = ⌊ 3 ≤? 4 ⌋

_ : ⌊ 3 ≤? 4 ⌋ ≡ true
_ = refl

_ : ⌊ 3 ≤? 2 ⌋ ≡ false
_ = refl

toWitness : ∀ {A : Set} {D : Dec A} → T ⌊ D ⌋ → A
toWitness {_} {yes v} tt = v
--toWitness {_} {no _} = ? -- `T ⌊ no x ⌋ → A` reduces to `⊥ → A`
toWitness {_} {no _} () -- Empty because there is no value for `⊥`

fromWitness : ∀ {A : Set} {D : Dec A} → A → T ⌊ D ⌋
fromWitness {_} {yes _} _ = tt
fromWitness {_} {no ¬a} a = ¬a a -- with type ⊥

_ : 2 ≤ 4
--_ = toWitness {D = 2 ≤? 4} tt
_ = toWitness {_} {2 ≤? 4} tt

¬4≤2₃ : ¬ (4 ≤ 2)
--¬4≤2₃ = fromWitness {D = 4 ≤? 2}
¬4≤2₃ = fromWitness {_} {4 ≤? 2}

¬z<z : ¬ (zero < zero)
¬z<z ()

¬s<z : ∀ {m : ℕ} → ¬ (suc m < zero)
¬s<z ()

_<?_ : ∀ (m n : ℕ) → Dec (m < n)
zero <? zero = no ¬z<z
zero <? suc n = yes z<s
suc m <? zero = no ¬s<z
suc m <? suc n with m <? n
...               | yes m<n = yes (s<s m<n)
...               | no ¬m<n = no λ{(s<s m<n) → ¬m<n m<n}

_ : ⌊ 2 <? 4 ⌋ ≡ true
_ = refl

¬z≡sn : ∀ {n : ℕ} → ¬ zero ≡ suc n
¬z≡sn ()

_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
zero    ≡ℕ? zero    = yes refl
zero    ≡ℕ? (suc n) = no ¬z≡sn
--(suc m) ≡ℕ? zero    = no (λ{sn≡z → ¬z≡sn (sym sn≡z)})
--(suc m) ≡ℕ? zero    = no (¬z≡sn ∘ sym)
(suc m) ≡ℕ? zero    = no ((λ()) ∘ sym)
--The following doesn't work though
--(suc m) ≡ℕ? zero    with zero ≡ℕ? (suc m)
--...                 | yes  z≡sm = yes (sym z≡sm)
--...                 | no  ¬z≡sm = no (¬z≡sm ∘ sym)
(suc m) ≡ℕ? (suc n) with m ≡ℕ? n
...               | yes m≡n = yes (cong suc m≡n)
...               | no ¬m≡n = no  (¬m≡n ∘ (cong pred))

infixr 6 _×-dec_

_×-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A × B)
yes x ×-dec yes y = yes ⟨ x , y ⟩
no ¬x ×-dec _     = no λ{ ⟨ x , y ⟩ → ¬x x }
_     ×-dec no ¬y = no λ{ ⟨ x , y ⟩ → ¬y y }

infixr 6 _⊎-dec_

_⊎-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⊎ B)
yes x ⊎-dec _     = yes (inj₁ x)
_     ⊎-dec yes y = yes (inj₂ y)
no ¬x ⊎-dec no ¬y = no λ{(inj₁ x) → ¬x x; (inj₂ y) → ¬y y}

¬? : ∀ {A : Set} → Dec A → Dec (¬ A)
¬? (yes x) = no (¬¬-intro x)
¬? (no ¬x) = yes ¬x

_→-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A → B)
_     →-dec yes y = yes (λ _ → y)
--no ¬x →-dec _     = yes ((λ()) ∘ ¬x)
no ¬x →-dec _     = yes (⊥-elim ∘ ¬x)
yes x →-dec no ¬y = no (λ{x→y → ¬y (x→y x)})

infixr 6 _∧_

_∧_ : Bool → Bool → Bool
true  ∧ true  = true
false ∧ _     = false
_     ∧ false = false

∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
∧-× (yes x) (yes y) = refl
∧-× (no ¬x) _       = refl
∧-× (yes x) (no ¬y) = refl

_iff_ : Bool → Bool → Bool
true  iff true  = true
false iff false = true
_     iff _     = false

_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
yes x ⇔-dec yes y = yes (record { from = λ{_ → x} ; to = λ{_ → y} })
no ¬x ⇔-dec no ¬y = yes (record { from = (λ()) ∘ ¬y ; to = (λ()) ∘ ¬x })
yes x ⇔-dec no ¬y = no (λ x⇔y → ¬y (_⇔_.to   x⇔y x))
no ¬x ⇔-dec yes y = no (λ x⇔y → ¬x (_⇔_.from x⇔y y))

iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
iff-⇔ (yes x) (yes y) = refl
iff-⇔ (no ¬x) (no ¬y) = refl
iff-⇔ (no ¬x) (yes y) = refl
iff-⇔ (yes x) (no ¬y) = refl


text:
-- Andreas, 2014-08-28, reported by Jacques Carette

{-# OPTIONS --cubical-compatible #-}

-- {-# OPTIONS -v term:20 #-}

module _ where

data Bool : Set where true false : Bool

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

module Sort (A : Set) ( _≤_ : A → A → Bool) where

  insert : A → List A → List A
  insert x [] = []
  insert x (y ∷ ys) with x ≤ y
  ... | true = x ∷ (y ∷ ys)
  ... | false = y ∷ insert x ys

-- Should termination check.
-- (Did not because while with lhss were not inlined, with-calls still were.)

ext: agda


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

record Box (B : Set) : Set₁ where
  constructor box
  field
    unbox   : B
open Box public

=box :{B : Set}{Γ₀ Γ₁ : Box B} → _≡_ {A = B} (unbox Γ₀) (unbox Γ₁) → Γ₀ ≡ Γ₁
=box {b} {box unbox} {box .unbox} refl = ?

-- WAS: internal error at src/full/Agda/TypeChecking/Rules/LHS.hs:294
-- SHOULD: complain about misplaced projection pattern

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module _ where

open import Agda.Builtin.Nat hiding (_+_)
import Agda.Builtin.Nat as N
open import Agda.Builtin.TrustMe
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

data ⊥ : Set where

module SimplifiedTestCase where

  record Fin : Set where
    constructor mkFin
    field m .p : Nat

  module _ (m : Nat) .(k : Nat) where

    w : Fin
    w = mkFin m k

    mutual

      X : Fin
      X = _

      -- Worked if removing this
      constr₁ : Fin.m X ≡ m
      constr₁ = refl

      constr₂ : X ≡ w
      constr₂ = refl

module OriginalTestCase where

  record Fin (n : Nat) : Set where
    constructor mkFin
    field
      m : Nat
      .p : Σ Nat λ k → (Nat.suc k N.+ m) ≡ n

  apply2 : {t₁ : Set} {t₂ : Set} {a b : t₁} → (f : t₁ → t₂) → a ≡ b → f a ≡ f b
  apply2 f refl = refl

  private
    lem : ∀ m → .(Σ Nat λ x → (suc (x N.+ m) ≡ 0)) → ⊥
    lem _ (_ , ())

  S : ∀ {n} → Fin n → Fin (suc n)
  S (mkFin a (k , p)) = mkFin (suc a) (suc k , primTrustMe)

  to : ∀ {n} → Fin n → Fin n
  to record { m = zero ; p = p } = record { m = zero ; p = p }
  to {zero} record { m = (suc m) ; p = p } with lem (suc m) p
  ... | ()
  to {suc n} record { m = (suc m) ; p = (k , p) } = S (to record { m = m ; p = k , primTrustMe })

  from = to

  iso : ∀ {n} → (x : Fin n) → from (to x) ≡ x
  iso {zero} record { m = m ; p = p } with lem m p
  ... | ()
  iso {suc n} record { m = zero ; p = p } = refl
  iso {suc n} record { m = (suc m) ; p = p@(k , _) } =
    let
      w : Fin n
      w = mkFin m (k , primTrustMe)
      v : S (from (to w)) ≡ S w
      v = apply2 {b = _} S (iso w)
    in v

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

syntax UTLC | Λ

type
  * : 0-ary

term
  app  : *  *  ->  * | _$_ l20
  lam  : *.*  ->  * | ƛ_ r10

theory
  (ƛβ) b : *.*  a : * |> app (lam (x.b[x]), a) = b[a]
  (ƛη) f : *          |> lam (x.app (f, x))    = f
  (lβ) b : *.*  a : * |> letd (a, x. b) = b[a]
-}

module UTLC.Syntax where

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

open import SOAS.Metatheory.Syntax

open import UTLC.Signature

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

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

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

    _$_  : Λ * Γ → Λ * Γ → Λ * Γ
    ƛ_   : Λ * (* ∙ Γ) → Λ * Γ

  infixl 20 _$_
  infixr 10 ƛ_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Λᵃ : MetaAlg Λ
  Λᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (appₒ  ⋮ a , b) → _$_  a b
      (lamₒ  ⋮ a)     → ƛ_   a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Λᵃ = MetaAlg Λᵃ

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

    open MetaAlg 𝒜ᵃ

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

    𝕤𝕖𝕞 (_$_  a b) = 𝑎𝑙𝑔 (appₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (ƛ_   a)   = 𝑎𝑙𝑔 (lamₒ  ⋮ 𝕤𝕖𝕞 a)

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

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

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

      open MetaAlg⇒ gᵃ⇒

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

      𝕤𝕖𝕞! (_$_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (ƛ_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

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

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

-- Derived operations
letd : Λ 𝔛 * Γ → Λ 𝔛 * (* ∙ Γ) → Λ 𝔛 * Γ
letd a b = (ƛ b) $ a

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Typed
open import Definition.Typed.Properties
import Definition.Typed.Weakening as Wk
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Reflexivity
open import Definition.LogicalRelation.Properties.Universe
open import Definition.LogicalRelation.Properties.Escape

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Weak head expansion of reducible types.
redSubst* : ∀ {A B l Γ}
          → Γ ⊢ A ⇒* B
          → Γ ⊩⟨ l ⟩ B
          → ∃ λ ([A] : Γ ⊩⟨ l ⟩ A)
          → Γ ⊩⟨ l ⟩ A ≡ B / [A]
redSubst* D (Uᵣ′ l′ l< ⊢Γ) rewrite redU* D =
  Uᵣ′ l′ l< ⊢Γ , PE.refl
redSubst* D (ℕᵣ [ ⊢B , ⊢ℕ , D′ ]) =
  let ⊢A = redFirst* D
  in  ℕᵣ ([ ⊢A , ⊢ℕ , D ⇨* D′ ]) , D′
redSubst* D (Emptyᵣ [ ⊢B , ⊢Empty , D′ ]) =
  let ⊢A = redFirst* D
  in  Emptyᵣ ([ ⊢A , ⊢Empty , D ⇨* D′ ]) , D′
redSubst* D (Unitᵣ [ ⊢B , ⊢Unit , D′ ]) =
  let ⊢A = redFirst* D
  in  Unitᵣ ([ ⊢A , ⊢Unit , D ⇨* D′ ]) , D′
redSubst* D (ne′ K [ ⊢B , ⊢K , D′ ] neK K≡K) =
  let ⊢A = redFirst* D
  in  (ne′ K [ ⊢A , ⊢K , D ⇨* D′ ] neK K≡K)
  ,   (ne₌ _ [ ⊢B , ⊢K , D′ ] neK K≡K)
redSubst* D (Bᵣ′ W F G [ ⊢B , ⊢ΠFG , D′ ] ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢A = redFirst* D
  in  (Bᵣ′ W F G [ ⊢A , ⊢ΠFG , D ⇨* D′ ] ⊢F ⊢G A≡A [F] [G] G-ext)
  ,   (B₌ _ _ D′ A≡A (λ ρ ⊢Δ → reflEq ([F] ρ ⊢Δ))
        (λ ρ ⊢Δ [a] → reflEq ([G] ρ ⊢Δ [a])))
redSubst* D (emb 0<1 x) with redSubst* D x
redSubst* D (emb 0<1 x) | y , y₁ = emb 0<1 y , y₁

-- Weak head expansion of reducible terms.
redSubst*Term : ∀ {A t u l Γ}
              → Γ ⊢ t ⇒* u ∷ A
              → ([A] : Γ ⊩⟨ l ⟩ A)
              → Γ ⊩⟨ l ⟩ u ∷ A / [A]
              → Γ ⊩⟨ l ⟩ t ∷ A / [A]
              × Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
redSubst*Term t⇒u (Uᵣ′ .⁰ 0<1 ⊢Γ) (Uₜ A [ ⊢t , ⊢u , d ] typeA A≡A [u]) =
  let [d]  = [ ⊢t , ⊢u , d ]
      [d′] = [ redFirst*Term t⇒u , ⊢u , t⇒u ⇨∷* d ]
      q = redSubst* (univ* t⇒u) (univEq (Uᵣ′ ⁰ 0<1 ⊢Γ) (Uₜ A [d] typeA A≡A [u]))
  in Uₜ A [d′] typeA A≡A (proj₁ q)
  ,  Uₜ₌ A A [d′] [d] typeA typeA A≡A (proj₁ q) [u] (proj₂ q)
redSubst*Term t⇒u (ℕᵣ D) (ℕₜ n [ ⊢u , ⊢n , d ] n≡n prop) =
  let A≡ℕ  = subset* (red D)
      ⊢t   = conv (redFirst*Term t⇒u) A≡ℕ
      t⇒u′ = conv* t⇒u A≡ℕ
  in  ℕₜ n [ ⊢t , ⊢n , t⇒u′ ⇨∷* d ] n≡n prop
  ,   ℕₜ₌ n n [ ⊢t , ⊢n , t⇒u′ ⇨∷* d ] [ ⊢u , ⊢n , d ]
          n≡n (reflNatural-prop prop)
redSubst*Term t⇒u (Emptyᵣ D) (Emptyₜ n [ ⊢u , ⊢n , d ] n≡n prop) =
  let A≡Empty  = subset* (red D)
      ⊢t   = conv (redFirst*Term t⇒u) A≡Empty
      t⇒u′ = conv* t⇒u A≡Empty
  in  Emptyₜ n [ ⊢t , ⊢n , t⇒u′ ⇨∷* d ] n≡n prop
  ,   Emptyₜ₌ n n [ ⊢t , ⊢n , t⇒u′ ⇨∷* d ] [ ⊢u , ⊢n , d ]
          n≡n (reflEmpty-prop prop)
redSubst*Term t⇒u (Unitᵣ D) (Unitₜ n [ ⊢u , ⊢n , d ] prop) =
  let A≡Unit  = subset* (red D)
      ⊢t   = conv (redFirst*Term t⇒u) A≡Unit
      t⇒u′ = conv* t⇒u A≡Unit
  in  Unitₜ n [ ⊢t , ⊢n , t⇒u′ ⇨∷* d ] prop
  ,   Unitₜ₌ ⊢t ⊢u
redSubst*Term t⇒u (ne′ K D neK K≡K) (neₜ k [ ⊢t , ⊢u , d ] (neNfₜ neK₁ ⊢k k≡k)) =
  let A≡K  = subset* (red D)
      [d]  = [ ⊢t , ⊢u , d ]
      [d′] = [ conv (redFirst*Term t⇒u) A≡K , ⊢u , conv* t⇒u A≡K ⇨∷* d ]
  in  neₜ k [d′] (neNfₜ neK₁ ⊢k k≡k) , neₜ₌ k k [d′] [d] (neNfₜ₌ neK₁ neK₁ k≡k)
redSubst*Term {A} {t} {u} {l} {Γ} t⇒u (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                  [u]@(Πₜ f [d]@([ ⊢t , ⊢u , d ]) funcF f≡f [f] [f]₁) =
  let A≡ΠFG = subset* (red D)
      t⇒u′  = conv* t⇒u A≡ΠFG
      [d′] = [ conv (redFirst*Term t⇒u) A≡ΠFG , ⊢u , conv* t⇒u A≡ΠFG ⇨∷* d ]
      [u′] = Πₜ f [d′] funcF f≡f [f] [f]₁
  in  [u′]
  ,   Πₜ₌ f f [d′] [d] funcF funcF f≡f [u′] [u]
          (λ [ρ] ⊢Δ [a] → reflEqTerm ([G] [ρ] ⊢Δ [a]) ([f]₁ [ρ] ⊢Δ [a]))
redSubst*Term {A} {t} {u} {l} {Γ} t⇒u (Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                  [u]@(Σₜ p [d]@([ ⊢t , ⊢u , d ]) pProd p≅p [fst] [snd]) =
  let A≡ΣFG = subset* (red D)
      t⇒u′  = conv* t⇒u A≡ΣFG
      [d′] = [ conv (redFirst*Term t⇒u) A≡ΣFG , ⊢u , conv* t⇒u A≡ΣFG ⇨∷* d ]
      [u′] = Σₜ p [d′] pProd p≅p [fst] [snd]
  in  [u′]
  ,   Σₜ₌ p p [d′] [d] pProd pProd p≅p [u′] [u] [fst] [fst]
          (reflEqTerm ([F] Wk.id (wf ⊢F)) [fst])
          (reflEqTerm ([G] Wk.id (wf ⊢F) [fst]) [snd])
redSubst*Term t⇒u (emb 0<1 x) [u] = redSubst*Term t⇒u x [u]

-- Weak head expansion of reducible types with single reduction step.
redSubst : ∀ {A B l Γ}
         → Γ ⊢ A ⇒ B
         → Γ ⊩⟨ l ⟩ B
         → ∃ λ ([A] : Γ ⊩⟨ l ⟩ A)
         → Γ ⊩⟨ l ⟩ A ≡ B / [A]
redSubst A⇒B [B] = redSubst* (A⇒B ⇨ id (escape [B])) [B]

-- Weak head expansion of reducible terms with single reduction step.
redSubstTerm : ∀ {A t u l Γ}
             → Γ ⊢ t ⇒ u ∷ A
             → ([A] : Γ ⊩⟨ l ⟩ A)
             → Γ ⊩⟨ l ⟩ u ∷ A / [A]
             → Γ ⊩⟨ l ⟩ t ∷ A / [A]
             × Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
redSubstTerm t⇒u [A] [u] = redSubst*Term (t⇒u ⇨ id (escapeTerm [A] [u])) [A] [u]


text:
------------------------------------------------------------------------
-- Call-by-value (CBV) reduction in Fω with interval kinds.
------------------------------------------------------------------------

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

module FOmegaInt.Reduction.Cbv where

open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
import Relation.Binary.Construct.Closure.Equivalence as EqClos
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (map; gmap)
import Relation.Binary.PropositionalEquality as PropEq
open import Relation.Binary.Reduction

open import FOmegaInt.Syntax
open import FOmegaInt.Reduction.Full

open Syntax
open Substitution using (_[_])

----------------------------------------------------------------------
-- Call-by-value (CBV) reduction and equivalence relations

-- Untyped term values with up to n free variables.
data Val {n} : Term n → Set where
  Λ : ∀ k a → Val (Λ k a)   -- type abstraction
  ƛ : ∀ a b → Val (ƛ a b)   -- term abstraction

infixl 9  _·₁_ _·₂_ _⊡_
infix  5  _→v_

-- One-step CBV reduction.
data _→v_ {n} : Term n → Term n → Set where
  cont-· : ∀ a b {c} (v : Val c)              → (ƛ a b) · c →v b [ c ]
  cont-⊡ : ∀ k a b                            → (Λ k a) ⊡ b →v a [ b ]
  _·₁_   : ∀ {a₁ a₂} → a₁ →v a₂ → ∀ b         →      a₁ · b →v a₂ · b
  _·₂_   : ∀ {a b₁ b₂} (v : Val a) → b₁ →v b₂ →      a · b₁ →v a · b₂
  _⊡_    : ∀ {a₁ a₂} → a₁ →v a₂ → ∀ b         →      a₁ ⊡ b →v a₂ ⊡ b

reduction : Reduction Term
reduction = record { _→1_ = _→v_ }

-- CBV reduction and equivalence.
open Reduction reduction public renaming (_→*_ to _→v*_; _↔_ to _≡v_)

----------------------------------------------------------------------
-- Simple properties of the CBV reductions/equivalence

-- Inclusions.
→v⇒→v* = →1⇒→* reduction
→v*⇒≡v = →*⇒↔  reduction
→v⇒≡v  = →1⇒↔  reduction

-- CBV reduction is a preorder.
→v*-predorder = →*-preorder reduction

-- Preorder reasoning for CBV reduction.
module →v*-Reasoning = →*-Reasoning reduction

-- Terms together with CBV equivalence form a setoid.
≡v-setoid = ↔-setoid reduction

-- Equational reasoning for CBV equivalence.
module ≡v-Reasoning = ↔-Reasoning reduction

----------------------------------------------------------------------
-- Relationships between CBV reduction and full β-reduction

-- One-step CBV reduction implies one-step β-reduction.
→v⇒→β : ∀ {n} {a b : Term n} → a →v b → a →β b
→v⇒→β (cont-· a b c) = ⌈ cont-Tm· a b _ ⌉
→v⇒→β (cont-⊡ k a b) = ⌈ cont-⊡ k a b ⌉
→v⇒→β (a₁→a₂ ·₁ b) = →v⇒→β a₁→a₂ ·₁ b
→v⇒→β (a ·₂ b₁→b₂) = _ ·₂ →v⇒→β b₁→b₂
→v⇒→β (a₁→a₂ ⊡ b)  = →v⇒→β a₁→a₂ ⊡₁ b

-- CBV reduction implies β-reduction.
→v*⇒→β* : ∀ {n} {a b : Term n} → a →v* b → a →β* b
→v*⇒→β* = map →v⇒→β

-- CBV equivalence implies β-equivalence.
≡v⇒≡β : ∀ {n} {a b : Term n} → a ≡v b → a ≡β b
≡v⇒≡β = EqClos.map →v⇒→β

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
module int-tests where

open import int
open import eq
open import product

three : ℤ
three = , next next unit{pos}

-two : ℤ
-two = , next unit{neg}

one = -two +ℤ three

one-lem : one ≡ ,_ { a = nonzero pos } unit
one-lem = refl

six = three +ℤ three

-four = -two +ℤ -two

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Luau.Heap where

open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (Maybe; just)
open import FFI.Data.Vector using (Vector; length; snoc; empty)
open import Luau.Addr using (Addr)
open import Luau.Var using (Var)
open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; addr; function_is_end)

data HeapValue (a : Annotated) : Set where
  function_is_end : FunDec a → Block a → HeapValue a

Heap : Annotated → Set
Heap a = Vector (HeapValue a)

data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → HeapValue a → Set where

  defn : ∀ {H val} →

    -----------------------------------
    (snoc H val) ≡ H ⊕ (length H) ↦ val

_[_] : ∀ {a} → Heap a → Addr → Maybe (HeapValue a)
_[_] = FFI.Data.Vector.lookup

∅ : ∀ {a} → Heap a
∅ = empty

data AllocResult a (H : Heap a) (V : HeapValue a) : Set where
  ok : ∀ b H′ → (H′ ≡ H ⊕ b ↦ V) → AllocResult a H V

alloc : ∀ {a} H V → AllocResult a H V
alloc H V = ok (length H) (snoc H V) defn

next : ∀ {a} → Heap a → Addr
next = length

allocated : ∀ {a} → Heap a → HeapValue a → Heap a
allocated = snoc

-- next-emp : (length ∅ ≡ 0)
next-emp = FFI.Data.Vector.length-empty

-- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V)
lookup-next = FFI.Data.Vector.lookup-snoc

-- lookup-next-emp : ∀ V → (lookup (allocated emp V) 0 ≡ just V)
lookup-next-emp = FFI.Data.Vector.lookup-snoc-empty


text:
open import Functional hiding (Domain)
import      Structure.Logic.Classical.NaturalDeduction
import      Structure.Logic.Classical.SetTheory.ZFC

module Structure.Logic.Classical.SetTheory.ZFC.BinaryRelatorSet {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ (_∈_ : Domain → Domain → Formula) ⦃ signature : _ ⦄ where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)
open Structure.Logic.Classical.SetTheory.ZFC.Signature {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic ⦄ {_∈_} (signature)

open import Structure.Logic.Classical.SetTheory.SetBoundedQuantification ⦃ classicLogic ⦄ (_∈_)

-- Like:
--   (x,f(x)) = (x , y)
--   f = {(x , y)}
--   = {{{x},{x,y}}}
--   ⋃f = {{x},{x,y}}
--   ⋃²f = {x,y}
lefts : Domain → Domain
lefts(s) = filter(⋃(⋃ s)) (x ↦ ∃ₗ(y ↦ (x , y) ∈ s))

rights : Domain → Domain
rights(s) = filter(⋃(⋃ s)) (y ↦ ∃ₗ(x ↦ (x , y) ∈ s))

leftsOfMany : Domain → Domain → Domain
leftsOfMany f(S) = filter(⋃(⋃ f)) (a ↦ ∃ₛ(S)(y ↦ (a , y) ∈ f))

rightsOfMany : Domain → Domain → Domain
rightsOfMany f(S) = filter(⋃(⋃ f)) (a ↦ ∃ₛ(S)(x ↦ (x , a) ∈ f))

leftsOf : Domain → Domain → Domain
leftsOf f(y) = leftsOfMany f(singleton(y))

rightsOf : Domain → Domain → Domain
rightsOf f(x) = rightsOfMany f(singleton(x))

-- swap : Domain → Domain
-- swap(s) = filter(rights(s) ⨯ left(s)) (xy ↦ )

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Data.Bool using ( Bool ; true ; false ; _∧_ )
open import Data.Product using ( _×_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.Concept using
  ( Concept ; ⟨_⟩ ; ¬⟨_⟩ ; ⊤ ; ⊥ ; _⊓_ ; _⊔_ ; ∀[_]_ ; ∃⟨_⟩_ ; ≤1 ; >1 )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using
  ( TBox ; ε ; _,_ ;_⊑₁_ ; _⊑₂_ ; Dis ; Ref ; Irr ; Tra )
open import Web.Semantic.Util using ( Subset ; □ ; □-proj₁ ; □-proj₂ )

module Web.Semantic.DL.TBox.Minimizable {Σ : Signature} where

data LHS : Subset (Concept Σ) where
  ⟨_⟩ : ∀ c → ⟨ c ⟩ ∈ LHS
  ⊤ : ⊤ ∈ LHS
  ⊥ : ⊥ ∈ LHS
  _⊓_ : ∀ {C D} → (C ∈ LHS) → (D ∈ LHS) → ((C ⊓ D) ∈ LHS)
  _⊔_ : ∀ {C D} → (C ∈ LHS) → (D ∈ LHS) → ((C ⊔ D) ∈ LHS)
  ∃⟨_⟩_ : ∀ R {C} → (C ∈ LHS) → ((∃⟨ R ⟩ C) ∈ LHS)

data RHS : Subset (Concept Σ) where
  ⟨_⟩ : ∀ c → ⟨ c ⟩ ∈ RHS
  ⊤ : ⊤ ∈ RHS
  _⊓_ : ∀ {C D} → (C ∈ RHS) → (D ∈ RHS) → ((C ⊓ D) ∈ RHS)
  ∀[_]_ : ∀ R {C} → (C ∈ RHS) → ((∀[ R ] C) ∈ RHS)
  ≤1 : ∀ R → ((≤1 R) ∈ RHS)

data μTBox : Subset (TBox Σ) where
  ε : μTBox ε
  _,_ : ∀ {T U} → (T ∈ μTBox) → (U ∈ μTBox) → ((T , U) ∈ μTBox)
  _⊑₁_ : ∀ {C D} → (C ∈ LHS) → (D ∈ RHS) → ((C ⊑₁ D) ∈ μTBox)
  _⊑₂_ : ∀ Q R → ((Q ⊑₂ R) ∈ μTBox)
  Ref : ∀ R → (Ref R ∈ μTBox)
  Tra : ∀ R → (Tra R ∈ μTBox)

lhs? : Concept Σ → Bool
lhs? ⟨ c ⟩      = true
lhs? ¬⟨ c ⟩     = false
lhs? ⊤          = true
lhs? ⊥          = true
lhs? (C ⊓ D)    = lhs? C ∧ lhs? D
lhs? (C ⊔ D)    = lhs? C ∧ lhs? D
lhs? (∀[ R ] C) = false
lhs? (∃⟨ R ⟩ C) = lhs? C
lhs? (≤1 R)     = false
lhs? (>1 R)     = false

lhs : ∀ C {C✓ : □(lhs? C)} → LHS C
lhs ⟨ c ⟩             = ⟨ c ⟩
lhs ⊤                 = ⊤
lhs ⊥                 = ⊥
lhs (C ⊓ D)    {C⊓D✓} = lhs C {□-proj₁ C⊓D✓} ⊓ lhs D {□-proj₂ {lhs? C} C⊓D✓}
lhs (C ⊔ D)    {C⊔D✓} = lhs C {□-proj₁ C⊔D✓} ⊔ lhs D {□-proj₂ {lhs? C} C⊔D✓}
lhs (∃⟨ R ⟩ C) {C✓}   = ∃⟨ R ⟩ (lhs C {C✓})
lhs ¬⟨ c ⟩     {}
lhs (∀[ R ] C) {}
lhs (≤1 R)     {}
lhs (>1 R)     {}

rhs? : Concept Σ → Bool
rhs? ⟨ c ⟩      = true
rhs? ¬⟨ c ⟩     = false
rhs? ⊤          = true
rhs? ⊥          = false
rhs? (C ⊓ D)    = rhs? C ∧ rhs? D
rhs? (C ⊔ D)    = false
rhs? (∀[ R ] C) = rhs? C
rhs? (∃⟨ R ⟩ C) = false
rhs? (≤1 R)     = true
rhs? (>1 R)     = false

rhs : ∀ C {C✓ : □(rhs? C)} → RHS C
rhs ⟨ c ⟩             = ⟨ c ⟩
rhs ⊤                 = ⊤
rhs (C ⊓ D)    {C⊓D✓} = rhs C {□-proj₁ C⊓D✓} ⊓ rhs D {□-proj₂ {rhs? C} C⊓D✓}
rhs (∀[ R ] C) {C✓}   = ∀[ R ] (rhs C {C✓})
rhs (≤1 R)            = ≤1 R
rhs ⊥          {}
rhs ¬⟨ c ⟩     {}
rhs (C ⊔ D)    {}
rhs (∃⟨ R ⟩ C) {}
rhs (>1 R)     {}

μTBox? : TBox Σ → Bool
μTBox? ε         = true
μTBox? (T , U)   = μTBox? T ∧ μTBox? U
μTBox? (C ⊑₁ D)  = lhs? C ∧ rhs? D
μTBox? (Q ⊑₂ R)  = true
μTBox? (Dis Q R) = false
μTBox? (Ref R)   = true
μTBox? (Irr R)   = false
μTBox? (Tra R)   = true

μtBox : ∀ T {T✓ : □(μTBox? T)} → μTBox T
μtBox ε               = ε
μtBox (T , U)  {TU✓}  = (μtBox T {□-proj₁ TU✓} , μtBox U {□-proj₂ {μTBox? T} TU✓})
μtBox (C ⊑₁ D) {C⊑D✓} = lhs C {□-proj₁ C⊑D✓} ⊑₁ rhs D {□-proj₂ {lhs? C} C⊑D✓}
μtBox (Q ⊑₂ R)        = Q ⊑₂ R
μtBox (Ref R)         = Ref R
μtBox (Tra R)         = Tra R
μtBox (Dis Q R) {}
μtBox (Irr R) {}

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
-- Jesper, 2018-05-17: Fixed internal error.  Now the second clause is
-- marked as unreachable (which is perhaps reasonable) and the first
-- clause is marked as not satisfying --exact-split (which is perhaps
-- unreasonable). To fix this properly, we would need to keep track of
-- excluded literals for not just pattern variables but also dot
-- patterns (and perhaps in other places as well).

open import Agda.Builtin.Char
open import Agda.Builtin.Equality

test : (c : Char) → c ≡ 'a' → Set
test 'a' _ = Char
test .'a' refl = Char

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- We only translate first-order definitions
------------------------------------------------------------------------------

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

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

postulate
  D    : Set
  _≡_  : D → D → Set
  succ : D → D

-- A higher-order definition
twice : (D → D) → D → D
twice f x = f (f x)
{-# ATP definition twice #-}

postulate twice-succ : ∀ n → twice succ n ≡ succ (succ n)
{-# ATP prove twice-succ #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- "Finite" sets indexed on coinductive "natural" numbers
------------------------------------------------------------------------

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

module Codata.Cofin where

open import Size
open import Codata.Thunk
open import Codata.Conat as Conat using (Conat; zero; suc; infinity; _ℕ<_; sℕ≤s; _ℕ≤infinity)
open import Codata.Conat.Bisimilarity as Bisim using (_⊢_≲_ ; s≲s)
open import Data.Nat
open import Data.Fin as Fin hiding (fromℕ; fromℕ≤; toℕ)
open import Function
open import Relation.Binary.PropositionalEquality

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

-- Note that `Cofin infnity` is /not/ finite. Note also that this is not a
-- coinductive type, but it is indexed on a coinductive type.

data Cofin : Conat ∞ → Set where
  zero : ∀ {n} → Cofin (suc n)
  suc  : ∀ {n} → Cofin (n .force) → Cofin (suc n)

suc-injective : ∀ {n} {p q : Cofin (n .force)} →
                (Cofin (suc n) ∋ suc p) ≡ suc q → p ≡ q
suc-injective refl = refl

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

fromℕ< : ∀ {n k} → k ℕ< n → Cofin n
fromℕ< {zero}  ()
fromℕ< {suc n} {zero}  (sℕ≤s p) = zero
fromℕ< {suc n} {suc k} (sℕ≤s p) = suc (fromℕ< p)

fromℕ : ℕ → Cofin infinity
fromℕ k = fromℕ< (suc k ℕ≤infinity)

toℕ : ∀ {n} → Cofin n → ℕ
toℕ zero    = zero
toℕ (suc i) = suc (toℕ i)

fromFin : ∀ {n} → Fin n → Cofin (Conat.fromℕ n)
fromFin zero    = zero
fromFin (suc i) = suc (fromFin i)

toFin : ∀ n → Cofin (Conat.fromℕ n) → Fin n
toFin zero    ()
toFin (suc n) zero    = zero
toFin (suc n) (suc i) = suc (toFin n i)


text:
-- Andreas, 2016-11-02, issue #2290

postulate
  A : Set
  a : A
  F : Set → Set

mutual
  data D : A → _ where
  FDa = F (D a)

-- ERROR WAS:
-- The sort of D cannot depend on its indices in the type A → Set _7

-- Should pass.

mutual
  data E : (x : A) → _ where
  FEa = F (E a)


text:
open import Agda.Primitive using (_⊔_)

-- Set being type of all types (which is infinitely nested as Set₀ Set₁ etc
postulate
  String : Set

{-# BUILTIN STRING String #-}

data bool : Set where
  tt : bool
  ff : bool

ex₀ : bool → String
ex₀ tt = "true"
ex₀ ff = "false"

-- parameterization over all "Sets"
-- otherwise we are limited to types that ∈ Set
if_then_else_ : ∀ { ℓ } { A : Set ℓ } → bool → A → A → A
if tt then x else y = x
if ff then x else y = y

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_plus_ : ℕ → ℕ → ℕ
zero   plus n = n
succ m plus n = succ (m plus n)

ex₁ : ℕ
ex₁ = 5

data [_] (A : Set) : Set where
  ♢   : [ A ]
  _,_ : A → [ A ] → [ A ]

infixr 6 _,_

_++_ : ∀{ α } → [ α ] → [ α ] → [ α ]
♢ ++ ys        = ys
(x , xs) ++ ys = x , xs ++ ys

ex₂ : [ ℕ ]
ex₂ = 5 , 6 , ♢

-- why is this equivalent to
--data _≡_ { α : Set } (x : α) : α → Set where
--  refl : x ≡ x

-- syntactical identity
data _≡_ { ℓ } { α : Set ℓ} : α → α → Set ℓ where
  refl : ∀ { x : α } → x ≡ x

{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

data ⊥ : Set where

ex₃ : (2 plus 3) ≡ 5
ex₃ = refl

-- logical negation in intutionistic logic
ex₄ : 0 ≡ 1 → ⊥
ex₄ ()

cong : ∀ { ℓ } { A B : Set ℓ } → { a b : A } { f : A → B } → a ≡ b → f a ≡ f b
cong refl = refl

ex₅ : ∀ { n } → (n plus 0) ≡ n
ex₅ {zero}    = refl
ex₅ {succ n1} = cong { f = succ } ex₅

-- rewrites and dot patterns ??

data _+_ (α : Set) (β : Set) : Set where
  left  : α → α + β
  right : β → α + β

ex₆ : String + ℕ
ex₆ = left "foo"

ex₇ : String + ℕ
ex₇ = right 5

record _∨_ (α β : Set) : Set where
  constructor _,_
  field
    fst : bool
    snd : if fst then β else α

tosum : ∀ { α β } → α + β → α ∨ β
tosum (left a)  = ff , a
tosum (right b) = tt  , b

unsum : ∀ { α β } → α ∨ β → α + β
unsum (ff , a) = left a
unsum (tt , b) = right b

tosum∘unsum : ∀ { α β } → (p : α ∨ β) → (tosum (unsum p)) ≡ p
tosum∘unsum (tt , b) = refl
tosum∘unsum (ff , b) = refl

unsum∘tosum : ∀ { α β } → (p : α + β) → (unsum (tosum p)) ≡ p
unsum∘tosum (left a)  = refl
unsum∘tosum (right b) = refl

--- Thus α + β is same as dependently typed α ∨ β. Further generalizing

record Σ (I : Set) (V : I -> Set) : Set where
  constructor _,_
  field
    fst : I
    snd : V fst

--- now α ∨ β can be written as
-- this is on the types, not on values
or : Set → Set → Set
or x y = Σ bool (λ b → if b then x else y)

-- assume V does not depend on I, we get products
twice : Set → Set
twice x = Σ bool (λ b → x)

max_stars_repo_name: curriedbanana/agda-exercises

max_issues_repo_name: curriedbanana/agda-exercises

max_forks_repo_name: curriedbanana/agda-exercises


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

open import HoTT
open import groups.Cokernel
open import groups.Image
import homotopy.ConstantToSetExtendsToProp as ConstExt

-- A collection of useful lemmas about exactness

module groups.Exactness where

module Exact {i j k} {G : Group i} {H : Group j} {K : Group k}
  {φ : G →ᴳ H} {ψ : H →ᴳ K} (φ-ψ-is-exact : is-exact φ ψ) where

  private
    module G = Group G
    module H = Group H
    module K = Group K
    module φ = GroupHom φ
    module ψ = GroupHom ψ
    module E = is-exact φ-ψ-is-exact

  abstract
    φ-const-implies-ψ-is-inj : (∀ g →  φ.f g == H.ident) → is-injᴳ ψ
    φ-const-implies-ψ-is-inj φ-is-const =
      has-trivial-ker-is-injᴳ ψ λ h ψh=0 →
        Trunc-rec (H.El-is-set _ _)
          (λ{(g , φg=h) → ! φg=h ∙ φ-is-const g})
          (E.ker-sub-im h ψh=0)

    G-trivial-implies-ψ-is-inj : is-trivialᴳ G → is-injᴳ ψ
    G-trivial-implies-ψ-is-inj G-is-triv =
      φ-const-implies-ψ-is-inj λ g → ap φ.f (G-is-triv g) ∙ φ.pres-ident

  G-to-ker : G →ᴳ Ker.grp ψ
  G-to-ker = Ker.inject-lift ψ φ (λ g → E.im-sub-ker (φ.f g) [ g , idp ])

  abstract
    φ-inj-implies-G-to-ker-is-equiv : is-injᴳ φ → is-equiv (GroupHom.f G-to-ker)
    φ-inj-implies-G-to-ker-is-equiv φ-is-inj = is-eq _ from to-from from-to
      where
        to : G.El → Ker.El ψ
        to = GroupHom.f G-to-ker

        module From (k : Ker.El ψ)
          = ConstExt {A = hfiber φ.f (fst k)} {B = G.El}
              G.El-is-set (λ hf → fst hf)
              (λ hf₁ hf₂ → φ-is-inj _ _ (snd hf₁ ∙ ! (snd hf₂)))

        from : Ker.El ψ → G.El
        from = λ k → From.ext k (uncurry E.ker-sub-im k)

        to-from : ∀ k → to (from k) == k
        to-from k = Ker.El=-out ψ $
          Trunc-elim
            {P = λ hf → φ.f (From.ext k hf) == fst k}
            (λ _ → H.El-is-set _ _)
            (λ{(g , p) → p})
            (uncurry E.ker-sub-im k)

        from-to : ∀ g → from (to g) == g
        from-to g = From.ext-is-const (to g) (uncurry E.ker-sub-im (to g)) [ g , idp ]

  φ-inj-implies-G-iso-ker : is-injᴳ φ → G ≃ᴳ Ker.grp ψ
  φ-inj-implies-G-iso-ker φ-is-inj = G-to-ker , φ-inj-implies-G-to-ker-is-equiv φ-is-inj

  abstract
    K-trivial-implies-φ-is-surj : is-trivialᴳ K → is-surjᴳ φ
    K-trivial-implies-φ-is-surj K-is-triv h = E.ker-sub-im h (K-is-triv (ψ.f h))

  coker-to-K : (H-is-abelian : is-abelian H) → Coker φ H-is-abelian →ᴳ K
  coker-to-K H-is-abelian = record {M} where
    module M where
      module Cok = Coker φ H-is-abelian
      abstract
        f-rel : ∀ {h₁ h₂ : H.El} (h₁h₂⁻¹-in-im : SubgroupProp.prop (im-propᴳ φ) (H.diff h₁ h₂))
          → ψ.f h₁ == ψ.f h₂
        f-rel {h₁} {h₂} h₁h₂⁻¹-in-im = K.zero-diff-same _ _ $
          ! (ψ.pres-diff h₁ h₂) ∙ E.im-sub-ker (H.diff h₁ h₂) h₁h₂⁻¹-in-im

      f : Cok.El → K.El
      f = SetQuot-rec K.El-is-set ψ.f f-rel
      abstract
        pres-comp : ∀ h₁ h₂ → f (Cok.comp h₁ h₂) == K.comp (f h₁) (f h₂)
        pres-comp = SetQuot-elim
          (λ _ → Π-is-set λ _ → =-preserves-set K.El-is-set)
          (λ h₁ → SetQuot-elim
            (λ _ → =-preserves-set K.El-is-set)
            (λ h₂ → ψ.pres-comp h₁ h₂)
            (λ _ → prop-has-all-paths-↓ (K.El-is-set _ _)))
          (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → K.El-is-set _ _))

  abstract
    ψ-surj-implies-coker-to-K-is-equiv : (H-is-abelian : is-abelian H)
      → is-surjᴳ ψ → is-equiv (GroupHom.f (coker-to-K H-is-abelian))
    ψ-surj-implies-coker-to-K-is-equiv H-is-abelian ψ-is-surj =
      is-eq to from to-from from-to
      where
        module Cok = Coker φ H-is-abelian

        to : Cok.El → K.El
        to = GroupHom.f (coker-to-K H-is-abelian)

        module From (k : K.El)
          = ConstExt {A = hfiber ψ.f k} {B = Cok.El}
              Cok.El-is-set (λ hf → q[ fst hf ])
              (λ{(h₁ , p₁) (h₂ , p₂) → quot-rel $
                E.ker-sub-im (H.diff h₁ h₂) $
                  ψ.pres-diff h₁ h₂ ∙ ap2 K.diff p₁ p₂ ∙ K.inv-r k})

        from : K.El → Cok.El
        from k = From.ext k (ψ-is-surj k)

        to-from : ∀ k → to (from k) == k
        to-from k = Trunc-elim
          {P = λ hf → to (From.ext k hf) == k}
          (λ _ → K.El-is-set _ _)
          (λ{(h , p) → p})
          (ψ-is-surj k)

        from-to : ∀ c → from (to c) == c
        from-to = SetQuot-elim
          (λ _ → =-preserves-set Cok.El-is-set)
          (λ h → From.ext-is-const (ψ.f h) (ψ-is-surj (ψ.f h)) [ h , idp ])
          (λ _ → prop-has-all-paths-↓ (Cok.El-is-set _ _))

  ψ-surj-implies-coker-iso-K : (H-is-abelian : is-abelian H)
    → is-surjᴳ ψ → Coker φ H-is-abelian ≃ᴳ K
  ψ-surj-implies-coker-iso-K H-is-abelian ψ-is-surj =
    coker-to-K H-is-abelian , ψ-surj-implies-coker-to-K-is-equiv H-is-abelian ψ-is-surj

  -- right split lemma
  module _ (H-is-abelian : is-abelian H) (φ-inj : is-injᴳ φ)
    (χ : K →ᴳ H) (χ-inv-r : (k : Group.El K) → GroupHom.f (ψ ∘ᴳ χ) k == k) where

    {- Splitting Lemma - Right Split
       Assume an exact sequence:

                 φ   ψ
           0 → G → H → K

       where H is abelian. If ψ has a right inverse χ, then H == G × K. Over
       this path φ becomes the natural injection and ψ the natural projection.
    -}

    private
      module χ = GroupHom χ

      {- H ≃ᴳ Ker ψ × Im χ -}

      ker-part : H →ᴳ Ker ψ
      ker-part = Ker.inject-lift ψ
        (hom-comp H (H , H-is-abelian) (idhom H) (inv-hom (H , H-is-abelian) ∘ᴳ (χ ∘ᴳ ψ)))
        (λ h →
          ψ.f (H.comp h (H.inv (χ.f (ψ.f h))))
            =⟨ ψ.pres-comp h (H.inv (χ.f (ψ.f h))) ⟩
          K.comp (ψ.f h) (ψ.f (H.inv (χ.f (ψ.f h))))
            =⟨ ! (χ.pres-inv (ψ.f h))
               |in-ctx (λ w → K.comp (ψ.f h) (ψ.f w)) ⟩
          K.comp (ψ.f h) (ψ.f (χ.f (K.inv (ψ.f h))))
            =⟨ χ-inv-r (K.inv (ψ.f h)) |in-ctx K.comp (ψ.f h) ⟩
          K.comp (ψ.f h) (K.inv (ψ.f h))
            =⟨ K.inv-r (ψ.f h) ⟩
          K.ident ∎)

      abstract
        ker-part-kerψ : (ker : Ker.El ψ) → GroupHom.f ker-part (fst ker) == ker
        ker-part-kerψ (h , p) = Ker.El=-out ψ $
          H.comp h (H.inv (χ.f (ψ.f h)))
            =⟨ p |in-ctx (λ w → H.comp h (H.inv (χ.f w))) ⟩
          H.comp h (H.inv (χ.f K.ident))
            =⟨ χ.pres-ident |in-ctx (λ w → H.comp h (H.inv w)) ⟩
          H.comp h (H.inv H.ident)
            =⟨ H.inv-ident |in-ctx H.comp h ⟩
          H.comp h H.ident
            =⟨ H.unit-r h ⟩
          h =∎

        ker-part-imχ : (im : Im.El χ) → GroupHom.f ker-part (fst im) == Ker.ident ψ
        ker-part-imχ (h , s) = Trunc-rec (Ker.El-level ψ _ _)
          (λ {(k , p) → Ker.El=-out ψ $
            H.comp h (H.inv (χ.f (ψ.f h)))
              =⟨ ! p |in-ctx (λ w → H.comp w (H.inv (χ.f (ψ.f w)))) ⟩
            H.comp (χ.f k) (H.inv (χ.f (ψ.f (χ.f k))))
              =⟨ χ-inv-r k |in-ctx (λ w → H.comp (χ.f k) (H.inv (χ.f w))) ⟩
            H.comp (χ.f k) (H.inv (χ.f k))
              =⟨ H.inv-r (χ.f k) ⟩
            H.ident
              =∎})
          s

      im-part : H →ᴳ Im χ
      im-part = im-lift χ ∘ᴳ ψ

      abstract
        im-part-kerψ : (ker : Ker.El ψ) → GroupHom.f im-part (fst ker) == Im.ident χ
        im-part-kerψ (h , p) = Im.El=-out χ (ap χ.f p ∙ χ.pres-ident)

        im-part-imχ : (im : Im.El χ) → GroupHom.f im-part (fst im) == im
        im-part-imχ (h , s) = Trunc-rec (Im.El-level χ _ _)
            (λ {(k , p) → Im.El=-out χ $
              χ.f (ψ.f h)        =⟨ ! p |in-ctx (χ.f ∘ ψ.f) ⟩
              χ.f (ψ.f (χ.f k))  =⟨ χ-inv-r k |in-ctx χ.f ⟩
              χ.f k              =⟨ p ⟩
              h                  =∎})
            s

      decomp : H →ᴳ Ker ψ ×ᴳ Im χ
      decomp = ×ᴳ-fanout ker-part im-part

      decomp-is-equiv : is-equiv (GroupHom.f decomp)
      decomp-is-equiv = is-eq _ dinv decomp-dinv dinv-decomp
        where
        dinv : Group.El (Ker ψ ×ᴳ Im χ) → H.El
        dinv ((h₁ , _) , (h₂ , _)) = H.comp h₁ h₂

        abstract
          decomp-dinv : ∀ s → GroupHom.f decomp (dinv s) == s
          decomp-dinv ((h₁ , kr) , (h₂ , im)) = pair×=
            (GroupHom.f ker-part (H.comp h₁ h₂)
               =⟨ GroupHom.pres-comp ker-part h₁ h₂ ⟩
             Ker.comp ψ (GroupHom.f ker-part h₁) (GroupHom.f ker-part h₂)
               =⟨ ap2 (Ker.comp ψ) (ker-part-kerψ (h₁ , kr)) (ker-part-imχ (h₂ , im)) ⟩
             Ker.comp ψ (h₁ , kr) (Ker.ident ψ)
               =⟨ Ker.unit-r ψ (h₁ , kr) ⟩
             (h₁ , kr)
               =∎)
            (GroupHom.f im-part (H.comp h₁ h₂)
               =⟨ GroupHom.pres-comp im-part h₁ h₂ ⟩
             Im.comp χ (GroupHom.f im-part h₁) (GroupHom.f im-part h₂)
               =⟨ ap2 (Im.comp χ) (im-part-kerψ (h₁ , kr)) (im-part-imχ (h₂ , im)) ⟩
             Im.comp χ (Im.ident χ) (h₂ , im)
               =⟨ Im.unit-l χ (h₂ , im) ⟩
             (h₂ , im) ∎)

          dinv-decomp : ∀ h → dinv (GroupHom.f decomp h) == h
          dinv-decomp h =
            H.comp (H.comp h (H.inv (χ.f (ψ.f h)))) (χ.f (ψ.f h))
              =⟨ H.assoc h (H.inv (χ.f (ψ.f h))) (χ.f (ψ.f h)) ⟩
            H.comp h (H.comp (H.inv (χ.f (ψ.f h))) (χ.f (ψ.f h)))
              =⟨ H.inv-l (χ.f (ψ.f h)) |in-ctx H.comp h ⟩
            H.comp h H.ident
              =⟨ H.unit-r h ⟩
            h ∎

      decomp-equiv : H.El ≃ Group.El (Ker ψ ×ᴳ Im χ)
      decomp-equiv = (_ , decomp-is-equiv)

      decomp-iso : H ≃ᴳ Ker ψ ×ᴳ Im χ
      decomp-iso = decomp , decomp-is-equiv

      {- K == Im χ -}

      K-iso-Imχ : K ≃ᴳ Im χ
      K-iso-Imχ = surjᴳ-and-injᴳ-iso (im-lift χ) (im-lift-is-surj χ) inj where
        abstract
          inj = has-trivial-ker-is-injᴳ (im-lift χ)
                  (λ k p → ! (χ-inv-r k) ∙ ap ψ.f (ap fst p) ∙ ψ.pres-ident)

    φ-inj-and-ψ-has-rinv-split : H ≃ᴳ G ×ᴳ K
    φ-inj-and-ψ-has-rinv-split =
      ×ᴳ-emap (φ-inj-implies-G-iso-ker φ-inj ⁻¹ᴳ) (K-iso-Imχ ⁻¹ᴳ) ∘eᴳ decomp-iso

    abstract
      φ-inj-and-ψ-has-rinv-implies-φ-comm-inl : CommSquareᴳ φ ×ᴳ-inl
        (idhom _) (–>ᴳ φ-inj-and-ψ-has-rinv-split )
      φ-inj-and-ψ-has-rinv-implies-φ-comm-inl = comm-sqrᴳ λ g → pair×=
        (ap (GroupIso.g (φ-inj-implies-G-iso-ker φ-inj))
              (ker-part-kerψ (GroupHom.f G-to-ker g))
          ∙ GroupIso.g-f (φ-inj-implies-G-iso-ker φ-inj) g)
        (im-sub-ker-out φ ψ E.im-sub-ker g)

    φ-inj-and-ψ-has-rinv-implies-ψ-comm-snd : CommSquareᴳ ψ (×ᴳ-snd {G = G})
      (–>ᴳ φ-inj-and-ψ-has-rinv-split ) (idhom _)
    φ-inj-and-ψ-has-rinv-implies-ψ-comm-snd = comm-sqrᴳ λ h → idp

abstract
  pre∘-is-exact : ∀ {i j k l} {G : Group i} {H : Group j} {K : Group k} {L : Group l}
    (φ : G →ᴳ H) {ψ : H →ᴳ K} {ξ : K →ᴳ L} → is-surjᴳ φ → is-exact ψ ξ → is-exact (ψ ∘ᴳ φ) ξ
  pre∘-is-exact φ {ψ = ψ} φ-is-surj ψ-ξ-is-exact = record {
    ker-sub-im = λ k → im-sub-im-∘ ψ φ φ-is-surj k ∘ ker-sub-im ψ-ξ-is-exact k;
    im-sub-ker = λ k → im-sub-ker ψ-ξ-is-exact k ∘ im-∘-sub-im ψ φ k}

module Exact2 {i j k l} {G : Group i} {H : Group j} {K : Group k} {L : Group l}
  {φ : G →ᴳ H} {ψ : H →ᴳ K} {ξ : K →ᴳ L}
  (φ-ψ-is-exact : is-exact φ ψ) (ψ-ξ-is-exact : is-exact ψ ξ) where

  private
    module G = Group G
    module H = Group H
    module K = Group K
    module L = Group L
    module φ = GroupHom φ
    module ψ = GroupHom ψ
    module ξ = GroupHom ξ
    module E1 = is-exact φ-ψ-is-exact
    module E2 = is-exact ψ-ξ-is-exact
    {- [L] for "lemmas" -}
    module EL1 = Exact φ-ψ-is-exact
    module EL2 = Exact ψ-ξ-is-exact

  abstract
    G-trivial-and-L-trivial-implies-H-iso-K :
      is-trivialᴳ G → is-trivialᴳ L → H ≃ᴳ K
    G-trivial-and-L-trivial-implies-H-iso-K G-is-triv L-is-triv
      = surjᴳ-and-injᴳ-iso ψ
          (EL2.K-trivial-implies-φ-is-surj L-is-triv)
          (EL1.G-trivial-implies-ψ-is-inj G-is-triv)

  G-trivial-implies-H-iso-ker :
    is-trivialᴳ G → H ≃ᴳ Ker.grp ξ
  G-trivial-implies-H-iso-ker G-is-triv
    = EL2.φ-inj-implies-G-iso-ker $
        EL1.G-trivial-implies-ψ-is-inj G-is-triv

  L-trivial-implies-coker-iso-K : (H-is-abelian : is-abelian H)
    → is-trivialᴳ L → Coker φ H-is-abelian ≃ᴳ K
  L-trivial-implies-coker-iso-K H-is-abelian L-is-triv
    = EL1.ψ-surj-implies-coker-iso-K H-is-abelian $
        EL2.K-trivial-implies-φ-is-surj L-is-triv

abstract
  equiv-preserves-exact : ∀ {i₀ i₁ j₀ j₁ l₀ l₁}
    {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁} {K₀ : Group l₀} {K₁ : Group l₁}
    {φ₀ : G₀ →ᴳ H₀} {ψ₀ : H₀ →ᴳ K₀} {φ₁ : G₁ →ᴳ H₁} {ψ₁ : H₁ →ᴳ K₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
    → CommSquareᴳ φ₀ φ₁ ξG ξH → CommSquareᴳ ψ₀ ψ₁ ξH ξK
    → is-equiv (GroupHom.f ξG) → is-equiv (GroupHom.f ξH) → is-equiv (GroupHom.f ξK)
    → is-exact φ₀ ψ₀ → is-exact φ₁ ψ₁
  equiv-preserves-exact {K₀ = K₀} {K₁} {φ₀ = φ₀} {ψ₀} {φ₁} {ψ₁} {ξG} {ξH} {ξK}
    (comm-sqrᴳ φ□) (comm-sqrᴳ ψ□) ξG-is-equiv ξH-is-equiv ξK-is-equiv exact₀
    = record {
      im-sub-ker = λ h₁ → Trunc-rec (SubgroupProp.level (ker-propᴳ ψ₁) h₁)
        (λ{(g₁ , φ₁g₁=h₁) →
          ψ₁.f h₁
            =⟨ ap ψ₁.f $ ! $ ξH.f-g h₁ ⟩
          ψ₁.f (ξH.f (ξH.g h₁))
            =⟨ ! $ ψ□ (ξH.g h₁) ⟩
          ξK.f (ψ₀.f (ξH.g h₁))
            =⟨ ap ξK.f $ im-sub-ker exact₀ (ξH.g h₁) [ ξG.g g₁ ,_ $
                φ₀.f (ξG.g g₁)
                  =⟨ ! (ξH.g-f (φ₀.f (ξG.g g₁))) ⟩
                ξH.g (ξH.f (φ₀.f (ξG.g g₁)))
                  =⟨ ap ξH.g $ φ□ (ξG.g g₁) ∙ ap φ₁.f (ξG.f-g g₁) ∙ φ₁g₁=h₁ ⟩
                ξH.g h₁
                  =∎ ] ⟩
          ξK.f (Group.ident K₀)
            =⟨ ξK.pres-ident ⟩
          Group.ident K₁
            =∎});
      ker-sub-im = λ h₁ ψ₁h₁=0 →
        Trunc-rec (SubgroupProp.level (im-propᴳ φ₁) h₁)
          (λ{(g₀ , φ₀g₀=ξH⁻¹h₁) → [ ξG.f g₀ ,_ $
            φ₁.f (ξG.f g₀)
              =⟨ ! $ φ□ g₀ ⟩
            ξH.f (φ₀.f g₀)
              =⟨ ap ξH.f φ₀g₀=ξH⁻¹h₁ ⟩
            ξH.f (ξH.g h₁)
              =⟨ ξH.f-g h₁ ⟩
            h₁
              =∎ ]})
          (ker-sub-im exact₀ (ξH.g h₁) $
            ψ₀.f (ξH.g h₁)
              =⟨ ! $ ξK.g-f (ψ₀.f (ξH.g h₁)) ⟩
            ξK.g (ξK.f (ψ₀.f (ξH.g h₁)))
              =⟨ ap ξK.g $ ψ□ (ξH.g h₁) ∙ ap ψ₁.f (ξH.f-g h₁) ∙ ψ₁h₁=0 ⟩
            ξK.g (Group.ident K₁)
              =⟨ GroupHom.pres-ident ξK.g-hom ⟩
            Group.ident K₀
              =∎)}
    where
      module φ₀ = GroupHom φ₀
      module φ₁ = GroupHom φ₁
      module ψ₀ = GroupHom ψ₀
      module ψ₁ = GroupHom ψ₁
      module ξG = GroupIso (ξG , ξG-is-equiv)
      module ξH = GroupIso (ξH , ξH-is-equiv)
      module ξK = GroupIso (ξK , ξK-is-equiv)

abstract
  equiv-preserves'-exact : ∀ {i₀ i₁ j₀ j₁ l₀ l₁}
    {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁} {K₀ : Group l₀} {K₁ : Group l₁}
    {φ₀ : G₀ →ᴳ H₀} {ψ₀ : H₀ →ᴳ K₀} {φ₁ : G₁ →ᴳ H₁} {ψ₁ : H₁ →ᴳ K₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
    → CommSquareᴳ φ₀ φ₁ ξG ξH → CommSquareᴳ ψ₀ ψ₁ ξH ξK
    → is-equiv (GroupHom.f ξG) → is-equiv (GroupHom.f ξH) → is-equiv (GroupHom.f ξK)
    → is-exact φ₁ ψ₁ → is-exact φ₀ ψ₀
  equiv-preserves'-exact cs₀ cs₁ ξG-ise ξH-ise ξK-ise ex =
    equiv-preserves-exact
      (CommSquareᴳ-inverse-v cs₀ ξG-ise ξH-ise)
      (CommSquareᴳ-inverse-v cs₁ ξH-ise ξK-ise)
      (is-equiv-inverse ξG-ise)
      (is-equiv-inverse ξH-ise)
      (is-equiv-inverse ξK-ise)
      ex

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Extensions.VecFirst where

open import Data.Vec
open import Data.Product
open import Level
open import Relation.Nullary
open import Function using (_∘_; _$_)

-- proof that an element is the first in a vector to satisfy the predicate B
data First {a b} {A : Set a} (B : A → Set b) : ∀ {n} (x : A) → Vec A n → Set (a ⊔ b) where

  here  : ∀ {n} {x : A} → (p : B x) → (v : Vec A n) → First B x (x ∷ v)
  there : ∀ {n x} {v : Vec A n} (x' : A) → ¬ (B x') → First B x v → First B x (x' ∷ v)

-- more likable syntax for the above structure
first_∈_⇔_ : ∀ {n} {A : Set} → A → Vec A n → (B : A → Set) → Set
first_∈_⇔_ x v p = First p x v

-- a decision procedure to find the first element in a vector that satisfies a predicate
find : ∀ {n} {A : Set} (P : A → Set) → ((a : A) → Dec (P a)) → (v : Vec A n) →
       Dec (∃ λ e → first e ∈ v ⇔ P)
find P dec [] = no (λ{ (e , ()) })
find P dec (x ∷ v) with dec x
find P dec (x ∷ v) | yes px = yes (x , here px v)
find P dec (x ∷ v) | no ¬px with find P dec v
find P dec (x ∷ v) | no ¬px | yes firstv = yes (, there x ¬px (proj₂ firstv))
find P dec (x ∷ v) | no ¬px | no ¬firstv = no $ helper ¬px ¬firstv
  where
    helper : ¬ (P x) → ¬ (∃ λ e → First P e v) → ¬ (∃ λ e → First P e (x ∷ v))
    helper ¬px ¬firstv (.x , here p .v) = ¬px p
    helper ¬px ¬firstv (u  , there ._ _ firstv) = ¬firstv (u , firstv)


text:
{-# OPTIONS --without-K #-}
module function.core where

open import level

-- copied from Agda's standard library

infixr 9 _∘'_
infixr 0 _$_

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

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x = λ _ → x

_$_ : ∀ {a b} {A : Set a} {B : A → Set b} →
      ((x : A) → B x) → ((x : A) → B x)
f $ x = f x

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

record Composition u₁ u₂ u₃ u₁₂ u₂₃ u₁₃
        : Set (lsuc (u₁ ⊔ u₂ ⊔ u₃ ⊔ u₁₂ ⊔ u₂₃ ⊔ u₁₃)) where
  infixl 9 _∘_
  field
    U₁ : Set u₁
    U₂ : Set u₂
    U₃ : Set u₃

    hom₁₂ : U₁ → U₂ → Set u₁₂
    hom₂₃ : U₂ → U₃ → Set u₂₃
    hom₁₃ : U₁ → U₃ → Set u₁₃

    _∘_ : {X₁ : U₁}{X₂ : U₂}{X₃ : U₃} → hom₂₃ X₂ X₃ → hom₁₂ X₁ X₂ → hom₁₃ X₁ X₃

record Identity u e : Set (lsuc (u ⊔ e)) where
  field
    U : Set u
    endo : U → Set e
    id : {X : U} → endo X

  id- : (X : U) → endo X
  id- X = id {X}

instance
  func-comp : ∀ {i j k} → Composition _ _ _ _ _ _
  func-comp {i}{j}{k} = record
    { U₁ = Set i
    ; U₂ = Set j
    ; U₃ = Set k
    ; hom₁₂ = λ X Y → X → Y
    ; hom₂₃ = λ X Y → X → Y
    ; hom₁₃ = λ X Y → X → Y
    ; _∘_ = λ f g x → f (g x) }

instance
  func-id : ∀ {i} → Identity _ _
  func-id {i} = record
    { U = Set i
    ; endo = λ X → X → X
    ; id = λ x → x }

module ComposeInterface {u₁ u₂ u₃ u₁₂ u₂₃ u₁₃}
                        ⦃ comp : Composition u₁ u₂ u₃ u₁₂ u₂₃ u₁₃ ⦄ where
  open Composition comp public using (_∘_)
open ComposeInterface public

module IdentityInterface {i e}
                         ⦃ identity : Identity i e ⦄ where
  open Identity identity public using (id; id-)
open IdentityInterface public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module _ where

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

open Semiring {{...}} public

infix 4 _≡_

postulate
  Ord : Set → Set
  Nat Bool  : Set
  zero  : Nat
  _≡_   : Nat → Nat → Set
  refl  : ∀ {x} → x ≡ x
  to    : ∀ {x} y → x ≡ y
  trans : {x y z : Nat} → x ≡ y → y ≡ z → x ≡ z

  instance
    ringNat′ : Semiring Nat

  _+N_ : Nat → Nat → Nat

instance
  ringNat : Semiring Nat
  ringNat ._+_ = _+N_

bad : (a b c : Nat) → a +N b ≡ c +N a
bad a b c =
  trans (to (a + c)) refl

-- Should list the errors from testing both ringNat and ringNat′


text:
module Itse.Checking where

open import Itse.Grammar
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Bool
open import Data.List hiding (lookup)
open import Data.Product
open import Data.Maybe

{-
# Checking

-}

{-
## Context

-}

data Context : Set
Closure : Set

infixr 6 _⦂_,_ [_],_

data Context where
  ∅ : Context
  _⦂_,_ : ∀ {e} → Name e → Expr (TypeOf e) → Context → Context
  [_],_ : Closure → Context → Context

{-
## Closure

-}

Closure = List (∃[ e ] (Name e × Expr e × Expr (TypeOf e)))

lookup-μ : ∀ {e} → Name e → Closure → Maybe (Expr e × Expr (TypeOf e))
lookup-μ {p} ξ []                    = nothing
lookup-μ {p} ξ ((p , υ , α , A) ∷ μ) with ξ ≟-Name υ
lookup-μ {p} ξ ((p , υ , α , A) ∷ μ)    | yes refl = just (α , A)
lookup-μ {p} ξ ((p , υ , α , A) ∷ μ)    | no  _    = lookup-μ ξ μ
lookup-μ {p} ξ ((t , _)         ∷ μ) = lookup-μ ξ μ
lookup-μ {t} x []                    = nothing
lookup-μ {t} x ((p , _)         ∷ μ) = lookup-μ x μ
lookup-μ {t} x ((t , y , a , α) ∷ μ) with x ≟-Name y
lookup-μ {t} x ((t , y , a , α) ∷ μ)    | yes refl = just (a , α)
lookup-μ {t} x ((t , y , a , α) ∷ μ)    | no  _    = lookup-μ x μ

lookup : ∀ {e} → Name e → Context → Maybe (Expr e × Expr (TypeOf e))
lookup x ∅ = nothing
lookup x (_ ⦂ _ , Γ) = lookup x Γ
lookup x ([ μ  ], Γ) = lookup-μ x μ

{-
## Substitution

-}

infix 6 ⟦_↦_⟧_

⟦_↦_⟧_ : ∀ {e e′} → Name e → Expr e → Expr e′ → Expr e′
⟦_↦_⟧_ = {!!}

{-
## Wellformed-ness

-}

infix 5 _⊢wf _⊢_ok _⊢_⦂_

data _⊢wf : Context → Set
data _⊢_ok : Context → Closure → Set
data _⊢_⦂_ : ∀ {e} → Context → Expr e → Expr (TypeOf e) → Set

data _⊢wf where

  ∅⊢wf :
    ∅ ⊢wf

  judgeₚ : ∀ {Γ} {X : Kind} {ξ} →
    Γ ⊢wf →
    Γ ⊢ X ⦂ `□ₛ →
    ----
    ξ ⦂ X , Γ ⊢wf

  judgeₜ : ∀ {Γ} {ξ : Type} {x : Nameₜ} →
    Γ ⊢wf →
    Γ ⊢ ξ ⦂ `●ₖ →
    ----
    x ⦂ ξ , Γ ⊢wf

  closure : ∀ {Γ} {μ} →
    Γ ⊢wf →
    Γ ⊢ μ ok →
    [ μ ], Γ ⊢wf

-- Closure = List (∃[ e ] ∃[ e≢k ] (Name e × Expr e × Expr (TypeOf e {e≢k})))
data _⊢_ok where

  -- type :
  --   Γ ⊢ μ ok →
  --   [ μ ], Γ ⊢

data _⊢_⦂_ where

  -- sorting (well-formed kinds)

  ●ₖ : ∀ {Γ} →
    Γ ⊢ `●ₖ ⦂ `□ₛ

  λₖₚ-intro : ∀ {Γ} {ξ} {X A} →
    ξ ⦂ X , Γ ⊢ A ⦂ `□ₛ →
    Γ ⊢ X ⦂ `□ₛ →
    ----
    Γ ⊢ `λₖₚ[ ξ ⦂ X ] A ⦂ `□ₛ

  λₖₜ-intro : ∀ {Γ} {ξ} {A} {x} →
    x ⦂ ξ , Γ ⊢ A ⦂ `□ₛ →
    Γ ⊢ ξ ⦂ `●ₖ →
    ----
    Γ ⊢ `λₖₜ[ x ⦂ ξ ] A ⦂ `□ₛ

  -- kinding

  λₚₚ-intro : ∀ {Γ} {X} {β} {ξ} →
    Γ ⊢ X ⦂ `□ₛ →
    ξ ⦂ X , Γ ⊢ β ⦂ `●ₖ →
    ----
    Γ ⊢ `λₚₚ[ ξ ⦂ X ] β ⦂ `λₖₚ[ ξ ⦂ X ] `●ₖ

  λₚₜ-intro : ∀ {Γ} {ξ} {β} {x} →
    Γ ⊢ ξ ⦂ `●ₖ →
    x ⦂ ξ , Γ ⊢ β ⦂ `●ₖ →
    ----
    Γ ⊢ `λₚₜ[ x ⦂ ξ ] β ⦂ `λₖₜ[ x ⦂ ξ ] `●ₖ

  λₚₚ-elim : ∀ {Γ} {A B} {ξ φ α} →
    Γ ⊢ φ ⦂ `λₖₚ[ ξ ⦂ A ] B →
    Γ ⊢ α ⦂ A →
    ----
    Γ ⊢ φ `∙ₚₚ α ⦂ B

  λₚₜ-elim : ∀ {Γ} {B} {φ α} {a} {x} →
    Γ ⊢ φ ⦂ `λₖₜ[ x ⦂ α ] B →
    Γ ⊢ a ⦂ α →
    ----
    Γ ⊢ φ `∙ₚₜ a ⦂ B

  -- typing

  λₜₚ-intro : ∀ {Γ} {X} {α} {a} {ξ} →
    Γ ⊢ X ⦂ `□ₛ →
    ξ ⦂ X , Γ ⊢ a ⦂ α →
    ----
    Γ ⊢ `λₜₚ[ ξ ⦂ X ] a ⦂ `λₚₚ[ ξ ⦂ X ] α

  λₜₜ-intro : ∀ {Γ} {α ξ} {a} {x} →
    Γ ⊢ α ⦂ `●ₖ →
    x ⦂ ξ , Γ ⊢ a ⦂ α →
    ----
    Γ ⊢ `λₜₜ[ x ⦂ ξ ] a ⦂ `λₚₜ[ x ⦂ ξ ] α

  λₜₚ-elim : ∀ {Γ} {A} {α β} {f} {ξ} →
    Γ ⊢ f ⦂ `λₚₚ[ ξ ⦂ A ] β →
    Γ ⊢ α ⦂ A →
    ----
    Γ ⊢ f `∙ₜₚ α ⦂ β

  λₜₜ-elim : ∀ {Γ} {α β} {f a x} →
    Γ ⊢ f ⦂ `λₚₜ[ x ⦂ α ] β →
    Γ ⊢ a ⦂ α →
    ----
    Γ ⊢ f `∙ₜₜ a ⦂ β

  -- "SelfGen"
  ι-intro : ∀ {Γ} {α} {a} {x} →
    Γ ⊢ a ⦂ ⟦ x ↦ a ⟧ α →
    Γ ⊢ `ι[ x ] α ⦂ `●ₖ →
    ----
    Γ ⊢ a ⦂ `ι[ x ] α

  -- "SelfInst"
  ι-elim : ∀ {Γ} {α} {a} {x} →
    Γ ⊢ a ⦂ `ι[ x ] α →
    ----
    Γ ⊢ a ⦂ ⟦ x ↦ a ⟧ α


text:
-- Andreas, 2016-01-22, issue 1790
-- Projections should be highlighted as such everywhere,
-- even in the parts of a record declaration that
-- make the record constructor type.

record Σ A (B : A → Set) : Set where
  field
    fst : A
    snd : B fst  -- fst should be highlighted as projection here

-- Should also work under 'mutual'.

mutual
  record IOInterface : Set₁ where
    constructor ioInterface
    field  Command   :  Set
           Response  :  (m : Command) → Set


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

module Data.Tuple.Base where

open import Prelude hiding (⊤; tt)
open import Data.Unit.UniversePolymorphic
open import Data.Fin

Tuple : ∀ n → (Lift a (Fin n) → Type b) → Type b
Tuple zero    f = ⊤
Tuple {a = a} {b = b} (suc n) f = f (lift f0) × Tuple {a = a} {b = b} n (f ∘ lift ∘ fs ∘ lower)

private
  variable
    n : ℕ
    u : Level
    U : Lift a (Fin n) → Type u

ind : Tuple n U → (i : Lift a (Fin n)) → U i
ind {n = suc n} (x , xs) (lift f0)     = x
ind {n = suc n} (x , xs) (lift (fs i)) = ind xs (lift i)

tab : ((i : Lift a (Fin n)) → U i) → Tuple n U
tab {n = zero}  f = tt
tab {n = suc n} f = f (lift f0) , tab (f ∘ lift ∘ fs ∘ lower)

Π→Tuple→Π : ∀ {a n u} {U : Lift a (Fin n) → Type u} (xs : (i : Lift a (Fin n)) → U i) i → ind (tab xs) i ≡ xs i
Π→Tuple→Π {n = suc n} f (lift f0) = refl
Π→Tuple→Π {n = suc n} f (lift (fs i)) = Π→Tuple→Π (f ∘ lift ∘ fs ∘ lower) (lift i)

Tuple→Π→Tuple : ∀ {n} {U : Lift a (Fin n) → Type u} (xs : Tuple n U) → tab (ind xs) ≡ xs
Tuple→Π→Tuple {n = zero} tt = refl
Tuple→Π→Tuple {n = suc n} (x , xs) i .fst = x
Tuple→Π→Tuple {n = suc n} (x , xs) i .snd = Tuple→Π→Tuple xs i

Tuple⇔ΠFin : ∀ {a n u} {U : Lift a (Fin n) → Type u} → Tuple n U ⇔ ((i : Lift a (Fin n)) → U i)
Tuple⇔ΠFin .fun = ind
Tuple⇔ΠFin .inv = tab
Tuple⇔ΠFin .leftInv = Tuple→Π→Tuple
Tuple⇔ΠFin .rightInv x = funExt (Π→Tuple→Π x)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
import Issue2217.M

{-# TERMINATING #-}

A : Set
A = ?

a : A
a = ?


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

open import HoTT

module cohomology.WithCoefficients where

→Ω-group-structure : ∀ {i j} (X : Ptd i) (Y : Ptd j)
  → GroupStructure (fst (X ⊙→ ⊙Ω Y))
→Ω-group-structure X Y = record {
  ident = ⊙cst;
  inv = λ F → ((! ∘ fst F) , ap ! (snd F));
  comp = λ F G → ⊙conc ⊙∘ ⊙×-in F G;
  unitl = λ G → pair= idp (unitl-lemma (snd G));
  unitr = λ F → ⊙λ= (∙-unit-r ∘ fst F) (unitr-lemma (snd F));
  assoc = λ F G H → ⊙λ=
    (λ x → ∙-assoc (fst F x) (fst G x) (fst H x))
    (assoc-lemma (snd F) (snd G) (snd H));
  invl = λ F → ⊙λ= (!-inv-l ∘ fst F) (invl-lemma (snd F));
  invr = λ F → ⊙λ= (!-inv-r ∘ fst F) (invr-lemma (snd F))}
  where
  unitl-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
    → ap (uncurry _∙_) (ap2 _,_ idp α) ∙ idp == α
  unitl-lemma idp = idp

  unitr-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
    → ap (uncurry _∙_) (ap2 _,_ α idp) ∙ idp == ∙-unit-r p ∙ α
  unitr-lemma idp = idp

  assoc-lemma : ∀ {i} {A : Type i} {x : A} {p q r : x == x}
    (α : p == idp) (β : q == idp) (γ : r == idp)
    → ap (uncurry _∙_) (ap2 _,_ (ap (uncurry _∙_) (ap2 _,_ α β) ∙ idp) γ) ∙ idp
      == ∙-assoc p q r
         ∙ ap (uncurry _∙_) (ap2 _,_ α (ap (uncurry _∙_) (ap2 _,_ β γ) ∙ idp)) ∙ idp
  assoc-lemma idp idp idp = idp

  invl-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
    → ap (uncurry _∙_) (ap2 _,_ (ap ! α) α) ∙ idp == !-inv-l p ∙ idp
  invl-lemma idp = idp

  invr-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
    → ap (uncurry _∙_) (ap2 _,_ α (ap ! α)) ∙ idp == !-inv-r p ∙ idp
  invr-lemma idp = idp

→Ω-group : ∀ {i j} (X : Ptd i) (Y : Ptd j) → Group (lmax i j)
→Ω-group X Y = Trunc-group (→Ω-group-structure X Y)

{- →Ω-group is functorial in the first argument -}

→Ω-group-dom-act : ∀ {i j k} {X : Ptd i} {Y : Ptd j}
  (f : fst (X ⊙→ Y)) (Z : Ptd k)
  → (→Ω-group Y Z →ᴳ →Ω-group X Z)
→Ω-group-dom-act {Y = Y} f Z =
  Trunc-group-hom (λ g → g ⊙∘ f)
    (λ g₁ g₂ → ⊙∘-assoc ⊙conc (⊙×-in g₁ g₂) f
               ∙ ap (λ w → ⊙conc ⊙∘ w) (⊙×-in-pre∘ g₁ g₂ f))

→Ω-group-dom-idf : ∀ {i j} {X : Ptd i} (Y : Ptd j)
  → →Ω-group-dom-act (⊙idf X) Y == idhom (→Ω-group X Y)
→Ω-group-dom-idf Y = hom= _ _ $ λ= $ Trunc-elim
  (λ _ → =-preserves-level _ Trunc-level) (λ _ → idp)

→Ω-group-dom-∘ : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y)) (W : Ptd l)
  → →Ω-group-dom-act (g ⊙∘ f) W
    == →Ω-group-dom-act f W ∘ᴳ →Ω-group-dom-act g W
→Ω-group-dom-∘ g f W = hom= _ _ $ λ= $
  Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
    (λ h → ap [_] (! (⊙∘-assoc h g f)))

{- Pointed maps out of bool -}

Bool⊙→-out : ∀ {i} {X : Ptd i}
  → fst (⊙Lift {j = i} ⊙Bool ⊙→ X) → fst X
Bool⊙→-out (h , _) = h (lift false)

Bool⊙→-equiv : ∀ {i} (X : Ptd i)
  → fst (⊙Lift {j = i} ⊙Bool ⊙→ X) ≃ fst X
Bool⊙→-equiv {i} X = equiv Bool⊙→-out g f-g g-f
  where
  g : fst X → fst (⊙Lift {j = i} ⊙Bool ⊙→ X)
  g x = ((λ {(lift b) → if b then snd X else x}) , idp)

  f-g : ∀ x → Bool⊙→-out (g x) == x
  f-g x = idp

  g-f : ∀ H → g (Bool⊙→-out H) == H
  g-f (h , hpt) = pair=
    (λ= lemma)
    (↓-app=cst-in $
      idp
        =⟨ ! (!-inv-l hpt) ⟩
      ! hpt ∙ hpt
        =⟨ ! (app=-β lemma (lift true)) |in-ctx (λ w → w ∙ hpt) ⟩
      app= (λ= lemma) (lift true) ∙ hpt ∎)
    where lemma : ∀ b → fst (g (h (lift false))) b == h b
          lemma (lift true) = ! hpt
          lemma (lift false) = idp

abstract
  Bool⊙→-path : ∀ {i} (X : Ptd i)
    → fst (⊙Lift {j = i} ⊙Bool ⊙→ X) == fst X
  Bool⊙→-path X = ua (Bool⊙→-equiv X)

abstract
  Bool⊙→Ω-is-π₁ : ∀ {i} (X : Ptd i)
    → →Ω-group (⊙Lift {j = i} ⊙Bool) X == πS 0 X
  Bool⊙→Ω-is-π₁ {i} X = group-ua $
    Trunc-group-iso Bool⊙→-out (λ _ _ → idp) (snd (Bool⊙→-equiv (⊙Ω X)))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Support for reflection
------------------------------------------------------------------------

{-# OPTIONS --with-K #-}

module Reflection where

open import Data.Unit.Base using (⊤)
open import Data.Bool.Base using (Bool; false; true)
open import Data.List.Base using (List); open Data.List.Base.List
open import Data.Nat using (ℕ) renaming (_≟_ to _≟-ℕ_)
open import Data.Nat.Show renaming (show to showNat)
open import Data.Float using (Float) renaming (show to showFloat)
open import Data.Float.Unsafe using () renaming (_≟_ to _≟f_)
open import Data.Char using (Char)
  renaming ( show to showChar
           ; _≟_ to _≟c_
           )
open import Data.String using (String)
  renaming ( show to showString
           ; _≟_ to _≟s_
           )
open import Data.Word using (Word64) renaming (toℕ to wordToℕ)
open import Data.Word.Unsafe using () renaming (_≟_ to _≟w_)
open import Data.Product
open import Function
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe
open import Relation.Nullary hiding (module Dec)
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product

import Agda.Builtin.Reflection as Builtin

------------------------------------------------------------------------
-- Names

-- Names.

open Builtin public using (Name)

-- Equality of names is decidable.

infix 4 _==_ _≟-Name_

private

  _==_ : Name → Name → Bool
  _==_ = Builtin.primQNameEquality

_≟-Name_ : Decidable {A = Name} _≡_
s₁ ≟-Name s₂ with s₁ == s₂
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _

-- Names can be shown.

showName : Name → String
showName = Builtin.primShowQName

------------------------------------------------------------------------
-- Metavariables

-- Metavariables.

open Builtin public using (Meta)

-- Equality of metavariables is decidable.

infix 4 _==-Meta_ _≟-Meta_

private

  _==-Meta_ : Meta → Meta → Bool
  _==-Meta_ = Builtin.primMetaEquality

_≟-Meta_ : Decidable {A = Meta} _≡_
s₁ ≟-Meta s₂ with s₁ ==-Meta s₂
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _

-- Metas can be shown.

showMeta : Meta → String
showMeta = Builtin.primShowMeta

------------------------------------------------------------------------
-- Terms

-- Is the argument visible (explicit), hidden (implicit), or an
-- instance argument?
open Builtin public using (Visibility; visible; hidden; instance′)

-- Arguments can be relevant or irrelevant.
open Builtin public using (Relevance; relevant; irrelevant)

-- Arguments.
open Builtin public
  renaming ( ArgInfo to Arg-info )
  using    ( arg-info )

visibility : Arg-info → Visibility
visibility (arg-info v _) = v

relevance : Arg-info → Relevance
relevance (arg-info _ r) = r

open Builtin public using (Arg; arg)
open Builtin public using (Abs; abs)

-- Literals.

open Builtin public using (Literal; nat; word64; float; char; string; name; meta)

-- Patterns.

open Builtin public using (Pattern; con; dot; var; lit; proj; absurd)

-- Terms.

open Builtin public
  using    ( Type; Term; var; con; def; lam; pat-lam; pi; lit; meta; unknown
           ; Sort; set
           ; Clause; clause; absurd-clause )
  renaming ( agda-sort to sort )

Clauses = List Clause

------------------------------------------------------------------------
-- Definitions

open Builtin public
  using    ( Definition
           ; function
           ; data-type
           ; axiom
           )
  renaming ( record-type to record′
           ; data-cons   to constructor′
           ; prim-fun    to primitive′ )

showLiteral : Literal → String
showLiteral (nat x)    = showNat x
showLiteral (word64 x) = showNat (wordToℕ x)
showLiteral (float x)  = showFloat x
showLiteral (char x)   = showChar x
showLiteral (string x) = showString x
showLiteral (name x)   = showName x
showLiteral (meta x)   = showMeta x

------------------------------------------------------------------------
-- Type checking monad

-- Type errors
open Builtin public using (ErrorPart; strErr; termErr; nameErr)

-- The monad
open Builtin public
  using ( TC; returnTC; bindTC; unify; typeError; inferType; checkType
        ; normalise; catchTC; getContext; extendContext; inContext
        ; freshName; declareDef; defineFun; getType; getDefinition
        ; blockOnMeta; quoteTC; unquoteTC )

newMeta : Type → TC Term
newMeta = checkType unknown

------------------------------------------------------------------------
-- Term equality is decidable

-- Boring helper functions.

private

  cong₂′ : ∀ {a b c : Level} {A : Set a} {B : Set b} {C : Set c}
          (f : A → B → C) {x y u v} →
          x ≡ y × u ≡ v → f x u ≡ f y v
  cong₂′ f = uncurry (cong₂ f)

  cong₃′ : ∀ {a b c d : Level} {A : Set a} {B : Set b} {C : Set c}
             {D : Set d} (f : A → B → C → D) {x y u v r s} →
           x ≡ y × u ≡ v × r ≡ s → f x u r ≡ f y v s
  cong₃′ f (refl , refl , refl) = refl

  arg₁ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → i ≡ i′
  arg₁ refl = refl

  arg₂ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → x ≡ x′
  arg₂ refl = refl

  abs₁ : ∀ {A i i′} {x x′ : A} → abs i x ≡ abs i′ x′ → i ≡ i′
  abs₁ refl = refl

  abs₂ : ∀ {A i i′} {x x′ : A} → abs i x ≡ abs i′ x′ → x ≡ x′
  abs₂ refl = refl

  arg-info₁ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′
  arg-info₁ refl = refl

  arg-info₂ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → r ≡ r′
  arg-info₂ refl = refl

  cons₁ : ∀ {a} {A : Set a} {x y} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → x ≡ y
  cons₁ refl = refl

  cons₂ : ∀ {a} {A : Set a} {x y} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
  cons₂ refl = refl

  var₁ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → x ≡ x′
  var₁ refl = refl

  var₂ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → args ≡ args′
  var₂ refl = refl

  con₁ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → c ≡ c′
  con₁ refl = refl

  con₂ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → args ≡ args′
  con₂ refl = refl

  def₁ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → f ≡ f′
  def₁ refl = refl

  def₂ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → args ≡ args′
  def₂ refl = refl

  meta₁ : ∀ {x x′ args args′} → Term.meta x args ≡ meta x′ args′ → x ≡ x′
  meta₁ refl = refl

  meta₂ : ∀ {x x′ args args′} → Term.meta x args ≡ meta x′ args′ → args ≡ args′
  meta₂ refl = refl

  lam₁ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → v ≡ v′
  lam₁ refl = refl

  lam₂ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → t ≡ t′
  lam₂ refl = refl

  pat-lam₁ : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → cs ≡ cs′
  pat-lam₁ refl = refl

  pat-lam₂ : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → args ≡ args′
  pat-lam₂ refl = refl

  pi₁ : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₁ ≡ t₁′
  pi₁ refl = refl

  pi₂ : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₂ ≡ t₂′
  pi₂ refl = refl

  sort₁ : ∀ {x y} → sort x ≡ sort y → x ≡ y
  sort₁ refl = refl

  lit₁ : ∀ {x y} → Term.lit x ≡ lit y → x ≡ y
  lit₁ refl = refl

  pcon₁ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′
  pcon₁ refl = refl

  pcon₂ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → args ≡ args′
  pcon₂ refl = refl

  pvar : ∀ {x y} → Pattern.var x ≡ var y → x ≡ y
  pvar refl = refl

  plit₁ : ∀ {x y} → Pattern.lit x ≡ lit y → x ≡ y
  plit₁ refl = refl

  pproj₁ : ∀ {x y} → proj x ≡ proj y → x ≡ y
  pproj₁ refl = refl

  set₁ : ∀ {x y} → set x ≡ set y → x ≡ y
  set₁ refl = refl

  slit₁ : ∀ {x y} → Sort.lit x ≡ lit y → x ≡ y
  slit₁ refl = refl

  nat₁ : ∀ {x y} → nat x ≡ nat y → x ≡ y
  nat₁ refl = refl

  word64₁ : ∀ {x y} → word64 x ≡ word64 y → x ≡ y
  word64₁ refl = refl

  float₁ : ∀ {x y} → float x ≡ float y → x ≡ y
  float₁ refl = refl

  char₁ : ∀ {x y} → char x ≡ char y → x ≡ y
  char₁ refl = refl

  string₁ : ∀ {x y} → string x ≡ string y → x ≡ y
  string₁ refl = refl

  name₁ : ∀ {x y} → name x ≡ name y → x ≡ y
  name₁ refl = refl

  lmeta₁ : ∀ {x y} → Literal.meta x ≡ meta y → x ≡ y
  lmeta₁ refl = refl

  clause₁ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → ps ≡ ps′
  clause₁ refl = refl

  clause₂ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → b ≡ b′
  clause₂ refl = refl

  absurd-clause₁ : ∀ {ps ps′} → absurd-clause ps ≡ absurd-clause ps′ → ps ≡ ps′
  absurd-clause₁ refl = refl

infix 4 _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_ _≟-Lit_ _≟-AbsTerm_
        _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-ArgPattern_ _≟-Args_
        _≟-Clause_ _≟-Clauses_ _≟-Pattern_ _≟-ArgPatterns_ _≟_
        _≟-Sort_

_≟-Visibility_ : Decidable (_≡_ {A = Visibility})
visible   ≟-Visibility visible   = yes refl
hidden    ≟-Visibility hidden    = yes refl
instance′ ≟-Visibility instance′ = yes refl
visible   ≟-Visibility hidden    = no λ()
visible   ≟-Visibility instance′ = no λ()
hidden    ≟-Visibility visible   = no λ()
hidden    ≟-Visibility instance′ = no λ()
instance′ ≟-Visibility visible   = no λ()
instance′ ≟-Visibility hidden    = no λ()

_≟-Relevance_ : Decidable (_≡_ {A = Relevance})
relevant   ≟-Relevance relevant   = yes refl
irrelevant ≟-Relevance irrelevant = yes refl
relevant   ≟-Relevance irrelevant = no λ()
irrelevant ≟-Relevance relevant   = no λ()

_≟-Arg-info_ : Decidable (_≡_ {A = Arg-info})
arg-info v r ≟-Arg-info arg-info v′ r′ =
  Dec.map′ (cong₂′ arg-info)
           < arg-info₁ , arg-info₂ >
           (v ≟-Visibility v′ ×-dec r ≟-Relevance r′)

_≟-Lit_ : Decidable (_≡_ {A = Literal})
nat x ≟-Lit nat x₁ = Dec.map′ (cong nat) nat₁ (x ≟-ℕ x₁)
nat x ≟-Lit word64 x₁ = no (λ ())
nat x ≟-Lit float x₁ = no (λ ())
nat x ≟-Lit char x₁ = no (λ ())
nat x ≟-Lit string x₁ = no (λ ())
nat x ≟-Lit name x₁ = no (λ ())
nat x ≟-Lit meta x₁ = no (λ ())
word64 x ≟-Lit word64 x₁ = Dec.map′ (cong word64) word64₁ (x ≟w x₁)
word64 x ≟-Lit nat x₁ = no (λ ())
word64 x ≟-Lit float x₁ = no (λ ())
word64 x ≟-Lit char x₁ = no (λ ())
word64 x ≟-Lit string x₁ = no (λ ())
word64 x ≟-Lit name x₁ = no (λ ())
word64 x ≟-Lit meta x₁ = no (λ ())
float x ≟-Lit nat x₁ = no (λ ())
float x ≟-Lit word64 x₁ = no (λ ())
float x ≟-Lit float x₁ = Dec.map′ (cong float) float₁ (x ≟f x₁)
float x ≟-Lit char x₁ = no (λ ())
float x ≟-Lit string x₁ = no (λ ())
float x ≟-Lit name x₁ = no (λ ())
float x ≟-Lit meta x₁ = no (λ ())
char x ≟-Lit nat x₁ = no (λ ())
char x ≟-Lit word64 x₁ = no (λ ())
char x ≟-Lit float x₁ = no (λ ())
char x ≟-Lit char x₁ = Dec.map′ (cong char) char₁ (x ≟c x₁)
char x ≟-Lit string x₁ = no (λ ())
char x ≟-Lit name x₁ = no (λ ())
char x ≟-Lit meta x₁ = no (λ ())
string x ≟-Lit nat x₁ = no (λ ())
string x ≟-Lit word64 x₁ = no (λ ())
string x ≟-Lit float x₁ = no (λ ())
string x ≟-Lit char x₁ = no (λ ())
string x ≟-Lit string x₁ = Dec.map′ (cong string) string₁ (x ≟s x₁)
string x ≟-Lit name x₁ = no (λ ())
string x ≟-Lit meta x₁ = no (λ ())
name x ≟-Lit nat x₁ = no (λ ())
name x ≟-Lit word64 x₁ = no (λ ())
name x ≟-Lit float x₁ = no (λ ())
name x ≟-Lit char x₁ = no (λ ())
name x ≟-Lit string x₁ = no (λ ())
name x ≟-Lit name x₁ = Dec.map′ (cong name) name₁ (x ≟-Name x₁)
name x ≟-Lit meta x₁ = no (λ ())
meta x ≟-Lit nat x₁ = no (λ ())
meta x ≟-Lit word64 x₁ = no (λ ())
meta x ≟-Lit float x₁ = no (λ ())
meta x ≟-Lit char x₁ = no (λ ())
meta x ≟-Lit string x₁ = no (λ ())
meta x ≟-Lit name x₁ = no (λ ())
meta x ≟-Lit meta x₁ = Dec.map′ (cong meta) lmeta₁ (x ≟-Meta x₁)

mutual
  _≟-AbsTerm_ : Decidable (_≡_ {A = Abs Term})
  abs s a ≟-AbsTerm abs s′ a′ =
    Dec.map′ (cong₂′ abs)
             < abs₁ , abs₂ >
             (s ≟s s′ ×-dec a ≟ a′)

  _≟-AbsType_ : Decidable (_≡_ {A = Abs Type})
  abs s a ≟-AbsType abs s′ a′ =
    Dec.map′ (cong₂′ abs)
             < abs₁ , abs₂ >
             (s ≟s s′ ×-dec a ≟ a′)

  _≟-ArgTerm_ : Decidable (_≡_ {A = Arg Term})
  arg i a ≟-ArgTerm arg i′ a′ =
    Dec.map′ (cong₂′ arg)
             < arg₁ , arg₂ >
             (i ≟-Arg-info i′ ×-dec a ≟ a′)

  _≟-ArgType_ : Decidable (_≡_ {A = Arg Type})
  arg i a ≟-ArgType arg i′ a′ =
    Dec.map′ (cong₂′ arg)
             < arg₁ , arg₂ >
             (i ≟-Arg-info i′ ×-dec a ≟ a′)

  _≟-ArgPattern_ : Decidable (_≡_ {A = Arg Pattern})
  arg i a ≟-ArgPattern arg i′ a′ =
    Dec.map′ (cong₂′ arg)
             < arg₁ , arg₂ >
             (i ≟-Arg-info i′ ×-dec a ≟-Pattern a′)

  _≟-Args_ : Decidable (_≡_ {A = List (Arg Term)})
  []       ≟-Args []       = yes refl
  (x ∷ xs) ≟-Args (y ∷ ys) = Dec.map′ (cong₂′ _∷_) < cons₁ , cons₂ > (x ≟-ArgTerm y ×-dec xs ≟-Args ys)
  []       ≟-Args (_ ∷ _)  = no λ()
  (_ ∷ _)  ≟-Args []       = no λ()

  _≟-Clause_ : Decidable (_≡_ {A = Clause})
  clause ps b ≟-Clause clause ps′ b′ = Dec.map′ (cong₂′ clause) < clause₁ , clause₂ > (ps ≟-ArgPatterns ps′ ×-dec b ≟ b′)
  absurd-clause ps ≟-Clause absurd-clause ps′ = Dec.map′ (cong absurd-clause) absurd-clause₁ (ps ≟-ArgPatterns ps′)
  clause _ _      ≟-Clause absurd-clause _ = no λ()
  absurd-clause _ ≟-Clause clause _ _      = no λ()

  _≟-Clauses_ : Decidable (_≡_ {A = Clauses})
  []       ≟-Clauses []       = yes refl
  (x ∷ xs) ≟-Clauses (y ∷ ys) = Dec.map′ (cong₂′ _∷_) < cons₁ , cons₂ > (x ≟-Clause y ×-dec xs ≟-Clauses ys)
  []       ≟-Clauses (_ ∷ _)  = no λ()
  (_ ∷ _)  ≟-Clauses []       = no λ()

  _≟-Pattern_ : Decidable (_≡_ {A = Pattern})
  con c ps ≟-Pattern con c′ ps′ = Dec.map′ (cong₂′ con) < pcon₁ , pcon₂ > (c ≟-Name c′ ×-dec ps ≟-ArgPatterns ps′)
  con x x₁ ≟-Pattern dot = no (λ ())
  con x x₁ ≟-Pattern var x₂ = no (λ ())
  con x x₁ ≟-Pattern lit x₂ = no (λ ())
  con x x₁ ≟-Pattern proj x₂ = no (λ ())
  con x x₁ ≟-Pattern absurd = no (λ ())
  dot ≟-Pattern con x x₁ = no (λ ())
  dot ≟-Pattern dot = yes refl
  dot ≟-Pattern var x = no (λ ())
  dot ≟-Pattern lit x = no (λ ())
  dot ≟-Pattern proj x = no (λ ())
  dot ≟-Pattern absurd = no (λ ())
  var s ≟-Pattern con x x₁ = no (λ ())
  var s ≟-Pattern dot = no (λ ())
  var s ≟-Pattern var s′ = Dec.map′ (cong var) pvar (s ≟s s′)
  var s ≟-Pattern lit x = no (λ ())
  var s ≟-Pattern proj x = no (λ ())
  var s ≟-Pattern absurd = no (λ ())
  lit x ≟-Pattern con x₁ x₂ = no (λ ())
  lit x ≟-Pattern dot = no (λ ())
  lit x ≟-Pattern var _ = no (λ ())
  lit l ≟-Pattern lit l′ = Dec.map′ (cong lit) plit₁ (l ≟-Lit l′)
  lit x ≟-Pattern proj x₁ = no (λ ())
  lit x ≟-Pattern absurd = no (λ ())
  proj x ≟-Pattern con x₁ x₂ = no (λ ())
  proj x ≟-Pattern dot = no (λ ())
  proj x ≟-Pattern var _ = no (λ ())
  proj x ≟-Pattern lit x₁ = no (λ ())
  proj x ≟-Pattern proj x₁ = Dec.map′ (cong proj) pproj₁ (x ≟-Name x₁)
  proj x ≟-Pattern absurd = no (λ ())
  absurd ≟-Pattern con x x₁ = no (λ ())
  absurd ≟-Pattern dot = no (λ ())
  absurd ≟-Pattern var _ = no (λ ())
  absurd ≟-Pattern lit x = no (λ ())
  absurd ≟-Pattern proj x = no (λ ())
  absurd ≟-Pattern absurd = yes refl

  _≟-ArgPatterns_ : Decidable (_≡_ {A = List (Arg Pattern)})
  []       ≟-ArgPatterns []       = yes refl
  (x ∷ xs) ≟-ArgPatterns (y ∷ ys) = Dec.map′ (cong₂′ _∷_) < cons₁ , cons₂ > (x ≟-ArgPattern y ×-dec xs ≟-ArgPatterns ys)
  []       ≟-ArgPatterns (_ ∷ _)  = no λ()
  (_ ∷ _)  ≟-ArgPatterns []       = no λ()

  _≟_ : Decidable (_≡_ {A = Term})
  var x args ≟ var x′ args′ = Dec.map′ (cong₂′ var) < var₁ , var₂ > (x ≟-ℕ x′          ×-dec args ≟-Args args′)
  con c args ≟ con c′ args′ = Dec.map′ (cong₂′ con) < con₁ , con₂ > (c ≟-Name c′       ×-dec args ≟-Args args′)
  def f args ≟ def f′ args′ = Dec.map′ (cong₂′ def) < def₁ , def₂ > (f ≟-Name f′       ×-dec args ≟-Args args′)
  meta x args ≟ meta x′ args′ = Dec.map′ (cong₂′ meta) < meta₁ , meta₂ > (x ≟-Meta x′   ×-dec args ≟-Args args′)
  lam v t    ≟ lam v′ t′    = Dec.map′ (cong₂′ lam) < lam₁ , lam₂ > (v ≟-Visibility v′ ×-dec t ≟-AbsTerm t′)
  pat-lam cs args ≟ pat-lam cs′ args′ =
                              Dec.map′ (cong₂′ pat-lam) < pat-lam₁ , pat-lam₂ > (cs ≟-Clauses cs′ ×-dec args ≟-Args args′)
  pi t₁ t₂   ≟ pi t₁′ t₂′   = Dec.map′ (cong₂′ pi)  < pi₁  , pi₂  > (t₁ ≟-ArgType t₁′  ×-dec t₂ ≟-AbsType t₂′)
  sort s     ≟ sort s′      = Dec.map′ (cong sort)  sort₁           (s ≟-Sort s′)
  lit l      ≟ lit l′       = Dec.map′ (cong lit)   lit₁           (l ≟-Lit l′)
  unknown    ≟ unknown      = yes refl

  var x args ≟ con c args′ = no λ()
  var x args ≟ def f args′ = no λ()
  var x args ≟ lam v t     = no λ()
  var x args ≟ pi t₁ t₂    = no λ()
  var x args ≟ sort _      = no λ()
  var x args ≟ lit _      = no λ()
  var x args ≟ meta _ _    = no λ()
  var x args ≟ unknown     = no λ()
  con c args ≟ var x args′ = no λ()
  con c args ≟ def f args′ = no λ()
  con c args ≟ lam v t     = no λ()
  con c args ≟ pi t₁ t₂    = no λ()
  con c args ≟ sort _      = no λ()
  con c args ≟ lit _      = no λ()
  con c args ≟ meta _ _    = no λ()
  con c args ≟ unknown     = no λ()
  def f args ≟ var x args′ = no λ()
  def f args ≟ con c args′ = no λ()
  def f args ≟ lam v t     = no λ()
  def f args ≟ pi t₁ t₂    = no λ()
  def f args ≟ sort _      = no λ()
  def f args ≟ lit _      = no λ()
  def f args ≟ meta _ _    = no λ()
  def f args ≟ unknown     = no λ()
  lam v t    ≟ var x args  = no λ()
  lam v t    ≟ con c args  = no λ()
  lam v t    ≟ def f args  = no λ()
  lam v t    ≟ pi t₁ t₂    = no λ()
  lam v t    ≟ sort _      = no λ()
  lam v t    ≟ lit _      = no λ()
  lam v t    ≟ meta _ _    = no λ()
  lam v t    ≟ unknown     = no λ()
  pi t₁ t₂   ≟ var x args  = no λ()
  pi t₁ t₂   ≟ con c args  = no λ()
  pi t₁ t₂   ≟ def f args  = no λ()
  pi t₁ t₂   ≟ lam v t     = no λ()
  pi t₁ t₂   ≟ sort _      = no λ()
  pi t₁ t₂   ≟ lit _      = no λ()
  pi t₁ t₂   ≟ meta _ _    = no λ()
  pi t₁ t₂   ≟ unknown     = no λ()
  sort _     ≟ var x args  = no λ()
  sort _     ≟ con c args  = no λ()
  sort _     ≟ def f args  = no λ()
  sort _     ≟ lam v t     = no λ()
  sort _     ≟ pi t₁ t₂    = no λ()
  sort _     ≟ lit _       = no λ()
  sort _     ≟ meta _ _    = no λ()
  sort _     ≟ unknown     = no λ()
  lit _     ≟ var x args  = no λ()
  lit _     ≟ con c args  = no λ()
  lit _     ≟ def f args  = no λ()
  lit _     ≟ lam v t     = no λ()
  lit _     ≟ pi t₁ t₂    = no λ()
  lit _     ≟ sort _      = no λ()
  lit _     ≟ meta _ _    = no λ()
  lit _     ≟ unknown     = no λ()
  meta _ _   ≟ var x args  = no λ()
  meta _ _   ≟ con c args  = no λ()
  meta _ _   ≟ def f args  = no λ()
  meta _ _   ≟ lam v t     = no λ()
  meta _ _   ≟ pi t₁ t₂    = no λ()
  meta _ _   ≟ sort _      = no λ()
  meta _ _   ≟ lit _       = no λ()
  meta _ _   ≟ unknown     = no λ()
  unknown    ≟ var x args  = no λ()
  unknown    ≟ con c args  = no λ()
  unknown    ≟ def f args  = no λ()
  unknown    ≟ lam v t     = no λ()
  unknown    ≟ pi t₁ t₂    = no λ()
  unknown    ≟ sort _      = no λ()
  unknown    ≟ lit _       = no λ()
  unknown    ≟ meta _ _    = no λ()
  pat-lam _ _ ≟ var x args  = no λ()
  pat-lam _ _ ≟ con c args  = no λ()
  pat-lam _ _ ≟ def f args  = no λ()
  pat-lam _ _ ≟ lam v t     = no λ()
  pat-lam _ _ ≟ pi t₁ t₂    = no λ()
  pat-lam _ _ ≟ sort _      = no λ()
  pat-lam _ _ ≟ lit _       = no λ()
  pat-lam _ _ ≟ meta _ _    = no λ()
  pat-lam _ _ ≟ unknown     = no λ()
  var x args  ≟ pat-lam _ _ = no λ()
  con c args  ≟ pat-lam _ _ = no λ()
  def f args  ≟ pat-lam _ _ = no λ()
  lam v t     ≟ pat-lam _ _ = no λ()
  pi t₁ t₂    ≟ pat-lam _ _ = no λ()
  sort _      ≟ pat-lam _ _ = no λ()
  lit _       ≟ pat-lam _ _ = no λ()
  meta _ _    ≟ pat-lam _ _ = no λ()
  unknown     ≟ pat-lam _ _ = no λ()

  _≟-Sort_ : Decidable (_≡_ {A = Sort})
  set t   ≟-Sort set t′  = Dec.map′ (cong set) set₁ (t ≟ t′)
  lit n   ≟-Sort lit n′  = Dec.map′ (cong lit) slit₁ (n ≟-ℕ n′)
  unknown ≟-Sort unknown = yes refl
  set _   ≟-Sort lit _   = no λ()
  set _   ≟-Sort unknown = no λ()
  lit _   ≟-Sort set _   = no λ()
  lit _   ≟-Sort unknown = no λ()
  unknown ≟-Sort set _   = no λ()
  unknown ≟-Sort lit _   = no λ()


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

module Data.Empty.UniversePolymorphic where

open import Prelude hiding (⊥)
import Data.Empty as Monomorphic

data ⊥ {ℓ} : Type ℓ where

Poly⊥⇔Mono⊥ : ∀ {ℓ} → ⊥ {ℓ} ⇔ Monomorphic.⊥
Poly⊥⇔Mono⊥ .fun      ()
Poly⊥⇔Mono⊥ .inv      ()
Poly⊥⇔Mono⊥ .leftInv  ()
Poly⊥⇔Mono⊥ .rightInv ()


text:
module Cats.Util.Reflection where

open import Reflection public

open import Data.List using ([])
open import Data.Unit using (⊤)
open import Function using (_∘_)
open import Level using (zero ; Lift)

open import Cats.Util.Monad using (RawMonad ; _>>=_ ; _>>_ ; return ; mapM′)

instance
  tcMonad : ∀ {l} → RawMonad {l} TC
  tcMonad = record
      { return = returnTC
      ; _>>=_ = bindTC
      }

pattern argH x = arg (arg-info hidden relevant) x
pattern argD x = arg (arg-info visible relevant) x
pattern defD x = def x []

fromArg : ∀ {A} → Arg A → A
fromArg (arg _ x) = x

fromAbs : ∀ {A} → Abs A → A
fromAbs (abs _ x) = x

blockOnAnyMeta-clause : Clause → TC (Lift zero ⊤)

-- This may or may not loop if there are metas in the input term that cannot be
-- solved when this tactic is called.
{-# TERMINATING #-}
blockOnAnyMeta : Term → TC (Lift zero ⊤)
blockOnAnyMeta (var x args) = mapM′ (blockOnAnyMeta ∘ fromArg) args
blockOnAnyMeta (con c args) = mapM′ (blockOnAnyMeta ∘ fromArg) args
blockOnAnyMeta (def f args) = mapM′ (blockOnAnyMeta ∘ fromArg) args
blockOnAnyMeta (lam v t) = blockOnAnyMeta (fromAbs t)
blockOnAnyMeta (pat-lam cs args) = do
    mapM′ blockOnAnyMeta-clause cs
    mapM′ (blockOnAnyMeta ∘ fromArg) args
blockOnAnyMeta (pi a b) = do
    blockOnAnyMeta (fromArg a)
    blockOnAnyMeta (fromAbs b)
blockOnAnyMeta (sort (set t)) = blockOnAnyMeta t
blockOnAnyMeta (sort (lit n)) = return _
blockOnAnyMeta (sort unknown) = return _
blockOnAnyMeta (lit l) = return _
blockOnAnyMeta (meta x _) = blockOnMeta x
blockOnAnyMeta unknown = return _

blockOnAnyMeta-clause (clause ps t) = blockOnAnyMeta t
blockOnAnyMeta-clause (absurd-clause ps) = return _

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


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

module Demos.Binary where

open import Data.Nat
open import Testers
open import Prelude

infixl 5 _1𝕓 _2𝕓
data 𝔹 : Type where
  0𝕓  : 𝔹
  _1𝕓 : 𝔹 → 𝔹
  _2𝕓 : 𝔹 → 𝔹

⟦_⇓⟧ : 𝔹 → ℕ
⟦ 0𝕓 ⇓⟧ = 0
⟦ n 1𝕓 ⇓⟧ = 1 + ⟦ n ⇓⟧ * 2
⟦ n 2𝕓 ⇓⟧ = 2 + ⟦ n ⇓⟧ * 2

inc : 𝔹 → 𝔹
inc 0𝕓 = 0𝕓 1𝕓
inc (xs 1𝕓) = xs 2𝕓
inc (xs 2𝕓) = inc xs 1𝕓

⟦_⇑⟧ : ℕ → 𝔹
⟦ zero  ⇑⟧ = 0𝕓
⟦ suc n ⇑⟧ = inc ⟦ n ⇑⟧

inc-suc : ∀ x → ⟦ inc x ⇓⟧ ≡ suc ⟦ x ⇓⟧
inc-suc 0𝕓     i = 1
inc-suc (x 1𝕓) i = 2 + ⟦ x ⇓⟧ * 2
inc-suc (x 2𝕓) i = suc (inc-suc x i * 2)

inc-2*-1𝕓 : ∀ n → inc ⟦ n * 2 ⇑⟧ ≡ ⟦ n ⇑⟧ 1𝕓
inc-2*-1𝕓 zero    i = 0𝕓 1𝕓
inc-2*-1𝕓 (suc n) i = inc (inc (inc-2*-1𝕓 n i))

𝔹-rightInv : ∀ x → ⟦ ⟦ x ⇑⟧ ⇓⟧ ≡ x
𝔹-rightInv zero    = refl
𝔹-rightInv (suc x) = inc-suc ⟦ x ⇑⟧ ; cong suc (𝔹-rightInv x)

𝔹-leftInv : ∀ x → ⟦ ⟦ x ⇓⟧ ⇑⟧ ≡ x
𝔹-leftInv 0𝕓 = refl
𝔹-leftInv (x 1𝕓) =           inc-2*-1𝕓 ⟦ x ⇓⟧  ; cong _1𝕓 (𝔹-leftInv x)
𝔹-leftInv (x 2𝕓) = cong inc (inc-2*-1𝕓 ⟦ x ⇓⟧) ; cong _2𝕓 (𝔹-leftInv x)

ℕ⇔𝔹 : 𝔹 ⇔ ℕ
ℕ⇔𝔹 .fun = ⟦_⇓⟧
ℕ⇔𝔹 .inv = ⟦_⇑⟧
ℕ⇔𝔹 .rightInv = 𝔹-rightInv
ℕ⇔𝔹 .leftInv = 𝔹-leftInv

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- This contains material which used to be in the Sane module, but is no
-- longer used.  It is not junk, so it is kept here, as we may need to
-- resurrect it.

module Obsolete where

import Data.Fin as F
--
open import Data.Empty
open import Data.Unit
open import Data.Unit.Core
open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Sum renaming (map to _⊎→_)
open import Data.Product renaming (map to _×→_)
open import Data.Vec
open import Function renaming (_∘_ to _○_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- start re-splitting things up, as this is getting out of hand
open import FT -- Finite Types
open import VecHelpers
open import NatSimple
open import Eval

open import Sane

{-
swap≡ind₀ : {n : ℕ} →
            ((F.suc F.zero) ∷ F.zero ∷ (vmap (λ i → F.suc (F.suc i)) (upTo n)))
            ≡ (swapInd F.zero (F.suc F.zero))
swap≡ind₀ {n} = ap (λ v → F.suc F.zero ∷ F.zero ∷ v)
               ((vmap (λ i → F.suc (F.suc i)) (upTo n)) ≡⟨ mapTab _ _ ⟩
               (tabulate (id ○ (λ i → F.suc (F.suc i)))) ≡⟨ tabf∼g _ _ swapIndIdAfterOne ⟩
               ((tabulate (((swapIndFn F.zero (F.suc F.zero)) ○ F.suc) ○ F.suc)) ∎))
-}

{-- For reference
swapmn : {lim : ℕ} → (m : F.Fin lim) → F.Fin′ m → (fromℕ lim) ⇛ (fromℕ lim)
swapmn F.zero ()
swapmn (F.suc m) (F.zero) = swapUpTo m ◎ swapi m ◎ swapDownFrom m
swapmn (F.suc m) (F.suc n) = id⇛ ⊕ swapmn m n
--}

{--
  foldrWorks
    {fromℕ n ⇛ fromℕ n}
    {n}
    (λ i → fromℕ n ⇛ fromℕ n)
    -- I think we need to rewrite vecToComb using an indexed fold to have all
    -- the information here that we need for the correctness proof [Z]
    (λ n′ v c → (i : F.Fin n′) → {!!})
    -- (evalVec {n′} v i) ≡ (evalComb c (finToVal i)))
    _◎_
    id⇛
    {!!} -- combination lemma
    {!!} -- base case lemma
    (zipWith makeSingleComb v (upTo n))
--}
-- Maybe we won't end up needing these to plug in to vecToCombWorks,
-- but I'm afraid we will, which means we'll have to fix them eventually.
-- I'm not sure how to do this right now and I've spent too much time on
-- it already when there are other, more tractable problems that need to
-- be solved. If someone else wants to take a shot, be my guest. [Z]

{-
foldri : {A : Set} → (B : ℕ → Set) → {m : ℕ} →
       ({n : ℕ} → F.Fin m → A → B n → B (suc n)) →
       B zero →
       Vec A m → B m
foldri {A} b {m} combine base vec =
  foldr
    b
    (uncurry combine)
    base
    (Data.Vec.zip (upTo _) vec)

postulate foldriWorks : {A : Set} → {m : ℕ} →
              (B : ℕ → Set) → (P : (n : ℕ) → Vec A n → B n → Set) →
              (combine : {n : ℕ} → F.Fin m → A → B n → B (suc n)) →
              (base : B zero) →
              ({n : ℕ} → (i : F.Fin m) → (a : A) → (v : Vec A n) → (b : B n)
                → P n v b
                → P (suc n) (a ∷ v) (combine i a b)) →
              P zero [] base →
              (v : Vec A m) →
              P m v (foldri B combine base v)
-}
-- following definition doesn't work, or at least not obviously
-- need a more straightforward definition of foldri, but none comes to mind
-- help? [Z]
{--
foldriWorks {A} {m} B P combine base pcombine pbase vec =
  foldrWorks {F.Fin m × A}
    B
    (λ n v b → P n (map proj₂ v) b)
    (uncurry combine)
    base
    ? -- (uncurry pcombine)
    pbase
    (Data.Vec.zip (upTo _) vec)
--}

-- Second argument is an accumulator
-- plf′ max i acc = (i + acc) + 1 mod (max + acc) if (i + acc) <= (max + acc), (max + acc) ow
-- This is the simplest way I could come up with to do this without
-- using F.compare or something similar
{-
plf′ : {m n : ℕ} → F.Fin (suc m) → F.Fin (suc m) → F.Fin n → F.Fin (m + n)
plf′ {n = zero}    F.zero           F.zero          ()
plf′ {m} {suc n}   F.zero           F.zero          acc =
  hetType F.zero (ap F.Fin (! (m+1+n≡1+m+n m _))) -- m mod m == 0
plf′               F.zero          (F.suc i)        acc = (F.suc i) +F acc -- above the threshold, so just id
plf′              (F.suc {zero} ()) _               _
plf′              (F.suc {suc m} max) F.zero        acc =  -- we're in range, so take succ of acc
  hetType (inj+ {n = m} (F.suc acc)) (ap F.Fin (m+1+n≡1+m+n m _))
plf′              (F.suc {suc m} max) (F.suc i)     acc = -- we don't know what to do yet, so incr acc & recur
  hetType (plf′ max i (F.suc acc))
          (ap F.Fin ((m+1+n≡1+m+n m _)))
-}

-- Seems important to prove!  (but not used, so commenting it out [JC])
{-
shuffle : {n : ℕ} → (i : F.Fin n) →
           (permLeftID (F.inject₁ i)
          ∘̬ swapInd (F.inject₁ i) (F.suc i)
          ∘̬ permRightID (F.inject₁ i))
        ≡ swapInd F.zero (F.suc i)
shuffle {zero} ()
shuffle {suc n} F.zero = {!!}
shuffle {suc n} (F.suc i) = {!!}
-}

-- helper lemmas for vecRepWorks
swapElsewhere : {n : ℕ} → (x : ⟦ fromℕ n ⟧) →
                inj₂ (inj₂ x) ≡ (evalComb (swapi F.zero) (inj₂ (inj₂ x)))
swapElsewhere x = refl

-- Lemma for proving things about calls to foldr; possibly not needed.
foldrWorks : {A : Set} → {m : ℕ} →
             (B : ℕ → Set) → (P : (n : ℕ) → Vec A n → B n → Set)
           → (_⊕_ : {n : ℕ} → A → B n → B (suc n)) → (base : B zero)
           → ({n : ℕ} → (a : A) → (v : Vec A n) → (b : B n) → P n v b
              → P (suc n) (a ∷ v) (a ⊕ b))
           → P zero [] base
           → (v : Vec A m)
           → P m v (foldr B _⊕_ base v)
foldrWorks B P combine base pcombine pbase [] = pbase
foldrWorks B P combine base pcombine pbase (x ∷ v) =
  pcombine x v (foldr B combine base v)
    (foldrWorks B P combine base pcombine pbase v)

-- evalComb on foldr becomes a foldl of flipped evalComb
evalComb∘foldr : {n j : ℕ} → (i : ⟦ fromℕ n ⟧ ) → (c-vec : Vec (fromℕ n ⇛ fromℕ n) j) →  evalComb (foldr (λ _ → fromℕ n ⇛ fromℕ n) _◎_ id⇛ c-vec) i ≡ foldl (λ _ → ⟦ fromℕ n ⟧) (λ i c → evalComb c i) i c-vec
evalComb∘foldr {zero} () v
evalComb∘foldr {suc _} i [] = refl -- i
evalComb∘foldr {suc n} i (c ∷ cv) = evalComb∘foldr {suc n} (evalComb c i) cv

-- foldl on a map: move the function in; specialize to this case.
foldl∘map : {n m : ℕ} {A C : Set} (f : C → A → C)
    (j : C) (g : F.Fin m → F.Fin m → A) → (v : Vec (F.Fin m) m) → (z : Vec (F.Fin m) n) →
  foldl (λ _ → C) f j (map (λ i → g (v !! i) i) z) ≡
  foldl (λ _ → C) (λ h i → i h) j (map (λ x₂ → λ w → f w (g (v !! x₂) x₂)) z)
foldl∘map {zero} f j g v [] = refl -- j
foldl∘map {suc n} {zero} f j g [] (() ∷ z)
foldl∘map {suc n} {suc m} f j g v (x ∷ z) = foldl∘map f (f j (g (lookup x v) x)) g v z

lemma3 : {n : ℕ} →
         (v : Vec (F.Fin n) n) → (i : F.Fin n) →
         (evalComb (vecToComb v) (finToVal i)) ≡
           foldl
             (λ _ → ⟦ fromℕ n ⟧)
             (λ h i₁ → i₁ h)
             (finToVal i)
             (replicate
               (λ x₂ → evalComb (makeSingleComb (lookup x₂ v) x₂)) ⊛
               tabulate (λ x → x))
lemma3 {n} v i = begin
   evalComb (vecToComb v) (finToVal i)
 ≡⟨ evalComb∘foldr
     (finToVal i)
     (map (λ i → makeSingleComb (v !! i) i) (upTo n)) ⟩
   foldl
     (λ _ → ⟦ fromℕ n ⟧)
     (λ j c → evalComb c j)
     (finToVal i)
     (map (λ i → makeSingleComb (v !! i) i) (upTo n))
 ≡⟨ foldl∘map (λ j c → evalComb c j) (finToVal i) makeSingleComb v (upTo n) ⟩
      foldl
        (λ _ → ⟦ fromℕ n ⟧)
        (λ h i₁ → i₁ h)
        (finToVal i)
        (replicate
          (λ x₂ → evalComb (makeSingleComb (lookup x₂ v) x₂)) ⊛
          tabulate id)
 ∎

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Math.NumberTheory.Summation.Nat.Properties.Lemma where

-- agda-stdlib
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Relation.Binary.PropositionalEquality
open import Function.Base

lemma₁ : ∀ n → n * (1 + n) * (1 + 2 * n) + 6 * ((1 + n) ^ 2) ≡
               (1 + n) * (2 + n) * (1 + 2 * (1 + n))
lemma₁ = solve 1 (λ n →
  (n :* (con 1 :+ n) :* (con 1 :+ con 2 :* n) :+ con 6 :* (con 1 :+ n) :^ 2) :=
  (con 1 :+ n) :* (con 2 :+ n) :* (con 1 :+ con 2 :* (con 1 :+ n))
  ) refl
  where open +-*-Solver


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts
open import htype-decidable
open import lemmas-matching
open import lemmas-consistency
open import disjointness
open import typed-elaboration

module elaborability where

  mutual
    elaborability-synth : {Γ : tctx} {e : hexp} {τ : htyp} →
                          holes-unique e →
                          Γ ⊢ e => τ →
                          Σ[ d ∈ ihexp ] Σ[ Δ ∈ hctx ]
                            (Γ ⊢ e ⇒ τ ~> d ⊣ Δ)
    elaborability-synth HUNum SNum = _ , _ , ESNum
    elaborability-synth (HUPlus hu1 hu2 hd) (SPlus wt1 wt2)
      with elaborability-ana hu1 wt1 | elaborability-ana hu2 wt2
    ... | _ , _ , _ , D1 | _ , _ , _ , D2 =
      _ , _ , ESPlus hd (elab-ana-disjoint hd D1 D2) D1 D2
    elaborability-synth (HUAsc hu) (SAsc wt)
      with elaborability-ana hu wt
    ... | _ , _ , _ , D = _ , _ , ESAsc D
    elaborability-synth HUVar (SVar x) = _ , _ , ESVar x
    elaborability-synth (HULam2 hu) (SLam apt wt)
      with elaborability-synth hu wt
    ... | _ , _ , D = _ , _ , ESLam apt D
    elaborability-synth (HUAp hu1 hu2 hd) (SAp wt1 m wt2)
      with elaborability-ana hu1 (ASubsume wt1 (~sym (▸arr-consist m))) |
           elaborability-ana hu2 wt2
    ... | _ , _ , _ , D1 | _ , _ , _ , D2 =
      _ , _ , ESAp hd (elab-ana-disjoint hd D1 D2) wt1 m D1 D2
    elaborability-synth (HUPair hu1 hu2 hd) (SPair wt1 wt2)
      with elaborability-synth hu1 wt1 | elaborability-synth hu2 wt2
    ... | _ , _ , D1 | _ , _ ,  D2 = _ , _ , ESPair hd (elab-synth-disjoint hd D1 D2) D1 D2
    elaborability-synth (HUFst hu) (SFst wt m)
      with elaborability-ana hu (ASubsume wt (~sym (▸prod-consist m)))
    ... | _ , _ , _ , D = _ , _ , ESFst wt m D
    elaborability-synth (HUSnd hu) (SSnd wt m)
      with elaborability-ana hu (ASubsume wt (~sym (▸prod-consist m)))
    ... | _ , _ , _ , D = _ , _ , ESSnd wt m D
    elaborability-synth HUHole SEHole = _ , _ , ESEHole
    elaborability-synth (HUNEHole hu hnn) (SNEHole wt)
      with elaborability-synth hu wt
    ... | _ , _ , D = _ , _ , ESNEHole (elab-new-disjoint-synth hnn D) D

    elaborability-ana : {Γ : tctx} {e : hexp} {τ : htyp} →
                        holes-unique e →
                        Γ ⊢ e <= τ →
                        Σ[ d ∈ ihexp ] Σ[ Δ ∈ hctx ] Σ[ τ' ∈ htyp ]
                          (Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ)
    elaborability-ana {e = e} hu (ASubsume wt con)
      with elaborability-synth hu wt
    elaborability-ana {e = N x} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = e ·+ e₁} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = e ·: x} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = X x} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = ·λ x ·[ x₁ ] e} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = e ∘ e₁} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = ⟨ e , e₁ ⟩} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = fst e} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = snd e} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) wt' con
    elaborability-ana {e = ⦇-⦈[ u ]} hu (ASubsume wt con)
      | _ , _ , wt' = _ , _ , _ , EAEHole
    elaborability-ana {e = ⦇⌜ e ⌟⦈[ u ]} (HUNEHole hu hnn) (ASubsume (SNEHole wt) con)
      | _ , _ , ESNEHole apt wt' with elaborability-synth hu wt
    ... | _ , _ , wt'' = _ , _ , _ , EANEHole (elab-new-disjoint-synth hnn wt'') wt''
    elaborability-ana (HULam1 hu) (ALam apt m wt)
      with elaborability-ana hu wt
    ... | _ , _ , _ , wt' = _ , _ , _ , EALam apt m wt'
    elaborability-ana (HUInl hu) (AInl m wt)
      with elaborability-ana hu wt
    ... | _ , _ , _ , wt' = _ , _ , _ , EAInl m wt'
    elaborability-ana (HUInr hu) (AInr m wt)
      with elaborability-ana hu wt
    ... | _ , _ , _ , wt' = _ , _ , _ , EAInr m wt'
    elaborability-ana (HUCase hu hu1 hu2 hd1 hd2 hd12) (ACase apt1 apt2 m wt wt1 wt2)
      with elaborability-synth hu wt | elaborability-ana hu1 wt1 | elaborability-ana hu2 wt2
    ... | _ , _ , wt' | _ , _ , _ , wt1' | _ , _ , _ , wt2' =
      _ , _ , _ , EACase hd1 hd2 hd12 (elab-synth-ana-disjoint hd1 wt' wt1')
                                      (elab-synth-ana-disjoint hd2 wt' wt2')
                                      (elab-ana-disjoint hd12 wt1' wt2')
                                      apt1 apt2 wt' m wt1' wt2'

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda