text:
module Prelude where

open import Agda.Builtin.IO public
  using (IO)

open import Data.Empty public using ()
  renaming (⊥ to 𝟘 ; ⊥-elim to elim𝟘)

open import Data.Nat public
  using (ℕ ; zero ; suc ; decTotalOrder ; _⊔_)
  renaming (_≤_ to _⊑_ ; z≤n to z⊑n ; s≤s to n⊑m→sn⊑sm ;
            _≤′_ to _≤_ ; ≤′-refl to refl≤ ; ≤′-step to step≤ ;
            _≤?_ to _⊑?_ ; _≰_ to _⋢_ ; _<′_ to _<_ ; _≟_ to _≡?_)

open import Data.Nat.Properties public using ()
  renaming (≤⇒≤′ to ⊑→≤ ; ≤′⇒≤ to ≤→⊑ ; z≤′n to z≤n ; s≤′s to n≤m→sn≤sm)

open import Data.Nat.Show public
  using (show)

open import Data.Product public
  using (Σ ; _×_ ; _,_)
  renaming (proj₁ to π₁ ; proj₂ to π₂)

open import Data.String public
  using (String)
  renaming (_≟_ to _≡ₛ?_ ; _++_ to _⧺_)

open import Data.Sum public
  using (_⊎_)
  renaming (inj₁ to ι₁ ; inj₂ to ι₂)

open import Data.Unit public using ()
  renaming (⊤ to Unit ; tt to unit)

open import Function public
  using (_∘_)

open import Relation.Binary public
  using (Antisymmetric ; Decidable ; DecTotalOrder ; Reflexive ; Rel ;
         Symmetric ; Total ; Transitive ; Trichotomous ; Tri)
  renaming (tri< to τ₍ ; tri≈ to τ₌ ; tri> to τ₎)

open module NDTO = DecTotalOrder decTotalOrder public using ()
  renaming (antisym to antisym⊑ ; trans to trans⊑ ; total to total⊑)

open import Relation.Binary.PropositionalEquality public
  using (_≡_ ; _≢_ ; refl ; trans ; sym ; cong ; cong₂ ; subst)

open import Relation.Binary.HeterogeneousEquality public
  using (_≅_ ; _≇_)
  renaming (refl to refl≅ ; trans to trans≅ ; sym to sym≅ ; cong to cong≅ ;
            cong₂ to cong₂≅ ; subst to subst≅ ; ≅-to-≡ to ≅→≡ ; ≡-to-≅ to ≡→≅)

open import Relation.Nullary public
  using (¬_ ; Dec ; yes ; no)

open import Relation.Nullary.Negation public using ()
  renaming (contradiction to _↯_)

-- I/O.

postulate
  return : ∀ {a} {A : Set a} → A → IO A
  _≫=_   : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B

{-# COMPILED return (\_ _ -> return)    #-}
{-# COMPILED _≫=_   (\_ _ _ _ -> (>>=)) #-}

_≫_ : ∀ {a b} {A : Set a} {B : Set b} → IO A → IO B → IO B
m₁ ≫ m₂ = m₁ ≫= λ _ → m₂

postulate
  putStr   : String → IO Unit
  putStrLn : String → IO Unit

{-# COMPILED putStr   putStr   #-}
{-# COMPILED putStrLn putStrLn #-}

-- Notation for I/O.

infix -10 do_
do_ : ∀ {a} {A : Set a} → A → A
do x = x

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

infixr 0 do-bind
syntax do-bind m₁ (λ x → m₂) = x ← m₁ ⁏ m₂
do-bind = _≫=_

infixr 0 do-seq
syntax do-seq m₁ m₂ = m₁ ⁏ m₂
do-seq = _≫_

infixr 0 do-let
syntax do-let m₁ (λ x → m₂) = x := m₁ ⁏ m₂
do-let = case_of_

-- Properties of binary relations.

Irreflexive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Irreflexive _∼_ = ∀ {x} → ¬ (x ∼ x)

-- Properties of _≡_.

n≡m→sn≡sm : ∀ {n m} → n ≡ m → suc n ≡ suc m
n≡m→sn≡sm refl = refl

sn≡sm→n≡m : ∀ {n m} → suc n ≡ suc m → n ≡ m
sn≡sm→n≡m refl = refl

n≢m→sn≢sm : ∀ {n m} → n ≢ m → suc n ≢ suc m
n≢m→sn≢sm n≢m refl = refl ↯ n≢m

sn≢sm→n≢m : ∀ {n m} → suc n ≢ suc m → n ≢ m
sn≢sm→n≢m sn≢sm refl = refl ↯ sn≢sm

sym≢ : ∀ {a} {A : Set a} → Symmetric (_≢_ {A = A})
sym≢ x≢y refl = refl ↯ x≢y

-- Properties of _≤_.

_≰_ : ℕ → ℕ → Set
n ≰ m = ¬ (n ≤ m)

sn≤m→n≤m : ∀ {n m} → suc n ≤ m → n ≤ m
sn≤m→n≤m refl≤        = step≤ refl≤
sn≤m→n≤m (step≤ sn≤m) = step≤ (sn≤m→n≤m sn≤m)

sn≤sm→n≤m : ∀ {n m} → suc n ≤ suc m → n ≤ m
sn≤sm→n≤m refl≤        = refl≤
sn≤sm→n≤m (step≤ sn≤m) = sn≤m→n≤m sn≤m

n≰m→sn≰sm : ∀ {n m} → n ≰ m → suc n ≰ suc m
n≰m→sn≰sm n≰m refl≤        = refl≤ ↯ n≰m
n≰m→sn≰sm n≰m (step≤ sn≤m) = sn≤m→n≤m sn≤m ↯ n≰m

sn≰sm→n≰m : ∀ {n m} → suc n ≰ suc m → n ≰ m
sn≰sm→n≰m sn≰sm refl≤       = refl≤ ↯ sn≰sm
sn≰sm→n≰m sn≰sm (step≤ n≤m) = sn≰sm→n≰m (sn≰sm ∘ step≤) n≤m

sn≰n : ∀ {n} → suc n ≰ n
sn≰n {zero}  = λ ()
sn≰n {suc n} = n≰m→sn≰sm sn≰n

n≤m⊔n : (n m : ℕ) → n ≤ m ⊔ n
n≤m⊔n zero    zero    = refl≤
n≤m⊔n zero    (suc m) = z≤n
n≤m⊔n (suc n) zero    = refl≤
n≤m⊔n (suc n) (suc m) = n≤m→sn≤sm (n≤m⊔n n m)

-- Properties of _<_.

_≮_ : ℕ → ℕ → Set
n ≮ m = ¬ (n < m)

z<sn : ∀ {n} → zero < suc n
z<sn = n≤m→sn≤sm z≤n

n<m→sn<sm : ∀ {n m} → n < m → suc n < suc m
n<m→sn<sm = n≤m→sn≤sm

sn<m→n<m : ∀ {n m} → suc n < m → n < m
sn<m→n<m = sn≤m→n≤m

sn<sm→n<m : ∀ {n m} → suc n < suc m → n < m
sn<sm→n<m = sn≤sm→n≤m

n≮m→sn≮sm : ∀ {n m} → n ≮ m → suc n ≮ suc m
n≮m→sn≮sm = n≰m→sn≰sm

sn≮sm→n≮m : ∀ {n m} → suc n ≮ suc m → n ≮ m
sn≮sm→n≮m = sn≰sm→n≰m

n<s[n⊔m] : (n m : ℕ) → n < suc (n ⊔ m)
n<s[n⊔m] zero    zero    = refl≤
n<s[n⊔m] zero    (suc m) = n≤m→sn≤sm z≤n
n<s[n⊔m] (suc n) zero    = refl≤
n<s[n⊔m] (suc n) (suc m) = n≤m→sn≤sm (n<s[n⊔m] n m)

-- Conversion between _⊑_, ⊏, _≤_, _<_, and _≡_.

≰→⋢ : ∀ {n m} → n ≰ m → n ⋢ m
≰→⋢ {zero}  {zero}  n≰m = refl≤ ↯ n≰m
≰→⋢ {suc n} {zero}  n≰m = λ ()
≰→⋢ {n}     {suc m} n≰m = λ n⊑m → ⊑→≤ n⊑m ↯ n≰m

⋢→≰ : ∀ {n m} → n ⋢ m → n ≰ m
⋢→≰ {zero}  {m}     n⋢m = z⊑n ↯ n⋢m
⋢→≰ {suc n} {zero}  n⋢m = λ ()
⋢→≰ {suc n} {suc m} n⋢m = λ n≤m → ≤→⊑ n≤m ↯ n⋢m

≤×≢→< : ∀ {n m} → n ≤ m → n ≢ m → n < m
≤×≢→< refl≤       n≢m = refl ↯ n≢m
≤×≢→< (step≤ n≤m) n≢m = n≤m→sn≤sm n≤m

≤→<⊎≡ : ∀ {n m} → n ≤ m → n < m ⊎ n ≡ m
≤→<⊎≡ refl≤       = ι₂ refl
≤→<⊎≡ (step≤ n≤m) with ≤→<⊎≡ n≤m
≤→<⊎≡ (step≤ n≤m) | ι₁ sn≤m = ι₁ (step≤ sn≤m)
≤→<⊎≡ (step≤ n≤m) | ι₂ refl = ι₁ refl≤

<→≤ : ∀ {n m} → n < m → n ≤ m
<→≤ n<m = sn≤m→n≤m n<m

≡→≤ : ∀ {n m} → n ≡ m → n ≤ m
≡→≤ refl = refl≤

-- _≤_ is a decidable non-strict total order on naturals.

antisym≤ : Antisymmetric _≡_ _≤_
antisym≤ n≤m m≤n = antisym⊑ (≤→⊑ n≤m) (≤→⊑ m≤n)

total≤ : Total _≤_
total≤ n m with total⊑ n m
total≤ n m | ι₁ n⊑m = ι₁ (⊑→≤ n⊑m)
total≤ n m | ι₂ m⊑n = ι₂ (⊑→≤ m⊑n)

trans≤ : Transitive _≤_
trans≤ n≤m m≤z = ⊑→≤ (trans⊑ (≤→⊑ n≤m) (≤→⊑ m≤z))

_≤?_ : Decidable _≤_
n ≤? m with n ⊑? m
n ≤? m | yes n⊑m = yes (⊑→≤ n⊑m)
n ≤? m | no  n⋢m = no (⋢→≰ n⋢m)

-- _<_ is a decidable strict total order on naturals.

trans< : Transitive _<_
trans< n<m m<l = trans≤ (step≤ n<m) m<l

tri< : Trichotomous _≡_ _<_
tri< zero    zero    = τ₌ (λ ()) refl   (λ ())
tri< zero    (suc m) = τ₍ z<sn   (λ ()) (λ ())
tri< (suc n) zero    = τ₎ (λ ()) (λ ()) z<sn
tri< (suc n) (suc m) with tri< n m
tri< (suc n) (suc m) | τ₍ n<m n≢m m≮n = τ₍ (n<m→sn<sm n<m) (n≢m→sn≢sm n≢m) (n≮m→sn≮sm m≮n)
tri< (suc n) (suc m) | τ₌ n≮m n≡m m≮n = τ₌ (n≮m→sn≮sm n≮m) (n≡m→sn≡sm n≡m) (n≮m→sn≮sm m≮n)
tri< (suc n) (suc m) | τ₎ n≮m n≢m m<n = τ₎ (n≮m→sn≮sm n≮m) (n≢m→sn≢sm n≢m) (n<m→sn<sm m<n)

irrefl< : Irreflexive _<_
irrefl< = sn≰n

_<?_ : Decidable _<_
n <? m = suc n ≤? m

max_stars_repo_name: mietek/lamport-timestamps

max_issues_repo_name: mietek/lamport-timestamps

max_forks_repo_name: mietek/lamport-timestamps


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

-- Define Strong Monad; use the Wikipedia definition
-- https://en.wikipedia.org/wiki/Strong_monad
-- At the nLab, https://ncatlab.org/nlab/show/strong+monad
-- there are two further definitions; the 2-categorical version is too complicated
-- and the Moggi definition is a special case of the one here

module Categories.Monad.Strong  where

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

open import Categories.Category
open import Categories.Functor renaming (id to idF)
open import Categories.Category.Monoidal
open import Categories.Category.Product
open import Categories.NaturalTransformation hiding (id)
-- open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.Monad

private
  variable
    o ℓ e : Level

record Strength {C : Category o ℓ e} (V : Monoidal C) (m : Monad C) : Set (o ⊔ ℓ ⊔ e) where
  open Category C
  open Monoidal V
  open Monad m using (F)
  module M = Monad m
  open NaturalTransformation M.η using (η)
  open NaturalTransformation M.μ renaming (η to μ)
  open Functor F
  field
    strengthen : NaturalTransformation (⊗ ∘F (idF ⁂ F)) (F ∘F ⊗)

  private
    module t = NaturalTransformation strengthen

  field
    -- strengthening with 1 is irrelevant
    identityˡ : {A : Obj} → F₁ (unitorˡ.from) ∘ t.η (unit , A) ≈ unitorˡ.from
    -- commutes with unit (of monad)
    η-comm : {A B : Obj} → t.η (A , B) ∘ (id ⊗₁ η B) ≈  η (A ⊗₀ B)
    -- strength commutes with multiplication
    μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (t.η (A , B)) ∘ t.η (A , F₀ B)
      ≈ t.η (A , B) ∘ id ⊗₁ μ B
    -- consecutive applications of strength commute (i.e. strength is associative)
    strength-assoc :  {A B C : Obj} → F₁ associator.from ∘ t.η (A ⊗₀ B , C)
      ≈ t.η (A , B ⊗₀ C) ∘ id ⊗₁ t.η (B , C) ∘ associator.from

record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where
  field
    m : Monad C
    strength : Strength V m

ext: agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Relation.Binary.Raw

module Cubical.Relation.Binary.Reasoning.Base.Single {a ℓ} {A : Type a}
  (_∼_ : RawRel A ℓ) (isPreorder : IsPreorder _∼_)
  where

open IsPreorder isPreorder

------------------------------------------------------------------------
-- Reasoning combinators

-- Re-export combinators from partial reasoning

open import Cubical.Relation.Binary.Reasoning.Base.Partial _∼_ transitive public
  hiding (_∎⟨_⟩)

-- Redefine the terminating combinator now that we have reflexivity

infix 2 _∎

_∎ : ∀ x → x ∼ x
x ∎ = reflexive


text:
module PatternSyn where

data ⊤
  : Set
  where

  tt
    : ⊤

data D
  (A : Set)
  : Set
  where

  d
    : A
    → A
    → D A

pattern p
  = tt

pattern q
  = tt

pattern _,_ x y
  = d x y

f
  : ⊤
  → ⊤
f p
  = tt

g
  : {A : Set}
  → D A
  → A
g (x , _)
  = x

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


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

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian

open import MultiSorted.AlgebraicTheory
import MultiSorted.Product as Product

module MultiSorted.Interpretation
         {o ℓ e}
         {𝓈 ℴ}
         (Σ : Signature {𝓈} {ℴ})
         {𝒞 : Category.Category o ℓ e}
         (cartesian-𝒞 : Cartesian.Cartesian 𝒞) where
  open Signature Σ
  open Category.Category 𝒞

  -- An interpretation of Σ in 𝒞
  record Interpretation : Set (o ⊔ ℓ ⊔ e ⊔ 𝓈 ⊔ ℴ) where

    field
      interp-sort : sort → Obj
      interp-ctx : Product.Producted 𝒞 {Σ = Σ} interp-sort
      interp-oper : ∀ (f : oper) → Product.Producted.prod interp-ctx (oper-arity f) ⇒ interp-sort (oper-sort f)

    open Product.Producted interp-ctx

    -- the interpretation of a term
    interp-term : ∀ {Γ : Context} {A} → Term Γ A → prod Γ ⇒ interp-sort A
    interp-term (tm-var x) = π x
    interp-term (tm-oper f ts) = interp-oper f ∘ tuple (oper-arity f) (λ i → interp-term (ts i))

    -- the interpretation of a substitution
    interp-subst : ∀ {Γ Δ} → Γ ⇒s Δ → prod Γ ⇒ prod Δ
    interp-subst {Γ} {Δ} σ = tuple Δ λ i → interp-term (σ i)

    -- the equality of interpretations
    ⊨_ : (ε : Equation Σ) → Set e
    open Equation
    ⊨ ε = interp-term (eq-lhs ε) ≈ interp-term (eq-rhs ε)

    -- interpretation commutes with substitution
    open HomReasoning

    interp-[]s : ∀ {Γ Δ} {A} {t : Term Δ A} {σ : Γ ⇒s Δ} →
                 interp-term (t [ σ ]s) ≈ interp-term t ∘ interp-subst σ
    interp-[]s {Γ} {Δ} {A} {tm-var x} {σ} = ⟺ (project {Γ = Δ})
    interp-[]s {Γ} {Δ} {A} {tm-oper f ts} {σ} = (∘-resp-≈ʳ
                                                (tuple-cong
                                                  {fs = λ i → interp-term (ts i [ σ ]s)}
                                                  {gs = λ z → interp-term (ts z) ∘ interp-subst σ}
                                                  (λ i → interp-[]s {t = ts i} {σ = σ})
                                              ○ (∘-distribʳ-tuple
                                                  {Γ = oper-arity f}
                                                  {fs = λ z → interp-term (ts z)}
                                                  {g = interp-subst σ})))
                                                ○ (Equiv.refl ○ sym-assoc)

  -- -- Every signature has the trivial interpretation

  open Product 𝒞

  Trivial : Interpretation
  Trivial =
    let open Cartesian.Cartesian cartesian-𝒞 in
    record
      { interp-sort = (λ _ → ⊤)
      ; interp-ctx = StandardProducted (λ _ → ⊤) cartesian-𝒞
      ; interp-oper = λ f → ! }

  record _⇒I_ (I J : Interpretation) : Set (o ⊔ ℓ ⊔ e ⊔ 𝓈 ⊔ ℴ) where
    open Interpretation
    open Producted

    field
      hom-morphism : ∀ {A} → interp-sort I A ⇒ interp-sort J A
      hom-commute :
         ∀ (f : oper) →
         hom-morphism ∘ interp-oper I f ≈
             interp-oper J f ∘ tuple (interp-ctx J) (oper-arity f) (λ i → hom-morphism ∘ π (interp-ctx I) i)

  infix  4 _⇒I_

  -- The identity homomorphism
  id-I : ∀ {A : Interpretation} → A ⇒I A
  id-I {A} =
    let open Interpretation A in
    let open HomReasoning in
    let open Producted interp-sort in
    record
      { hom-morphism = id
      ; hom-commute = λ f →
                        begin
                          (id ∘ interp-oper f) ≈⟨ identityˡ ⟩
                          interp-oper f       ≈˘⟨ identityʳ ⟩
                          (interp-oper f ∘ id)      ≈˘⟨ refl⟩∘⟨ unique interp-ctx (λ i → identityʳ ○  ⟺ identityˡ) ⟩
                          (interp-oper f ∘
                            Product.Producted.tuple interp-ctx (oper-arity f)
                            (λ i → id ∘ Product.Producted.π interp-ctx i)) ∎
      }

  -- Compositon of homomorphisms
  _∘I_ : ∀ {A B C : Interpretation} → B ⇒I C → A ⇒I B → A ⇒I C
  _∘I_ {A} {B} {C} ϕ ψ =
     let open _⇒I_ in
     record { hom-morphism = hom-morphism ϕ ∘ hom-morphism ψ
            ; hom-commute =
                let open Interpretation in
                let open Producted in
                let open HomReasoning in
                λ f →
                  begin
                    (((hom-morphism ϕ) ∘ hom-morphism ψ) ∘ interp-oper A f) ≈⟨ assoc ⟩
                    (hom-morphism ϕ ∘ hom-morphism ψ ∘ interp-oper A f) ≈⟨ (refl⟩∘⟨ hom-commute ψ f) ⟩
                    (hom-morphism ϕ ∘
                      interp-oper B f ∘
                      tuple (interp-ctx B) (oper-arity f)
                      (λ i → hom-morphism ψ ∘ π (interp-ctx A) i)) ≈˘⟨ assoc ⟩
                    ((hom-morphism ϕ ∘ interp-oper B f) ∘
                      tuple (interp-ctx B) (oper-arity f)
                      (λ i → hom-morphism ψ ∘ π (interp-ctx A) i)) ≈⟨ (hom-commute ϕ f ⟩∘⟨refl) ⟩
                     ((interp-oper C f ∘
                       tuple (interp-ctx C) (oper-arity f)
                       (λ i → hom-morphism ϕ ∘ π (interp-ctx B) i))
                      ∘
                      tuple (interp-ctx B) (oper-arity f)
                      (λ i → hom-morphism ψ ∘ π (interp-ctx A) i)) ≈⟨ assoc ⟩
                    (interp-oper C f ∘
                      tuple (interp-ctx C) (oper-arity f)
                      (λ i → hom-morphism ϕ ∘ π (interp-ctx B) i)
                      ∘
                      tuple (interp-ctx B) (oper-arity f)
                      (λ i → hom-morphism ψ ∘ π (interp-ctx A) i)) ≈⟨ (refl⟩∘⟨ ⟺ (∘-distribʳ-tuple (interp-sort C) (interp-ctx C))) ⟩
                    (interp-oper C f ∘
                      tuple (interp-ctx C) (oper-arity f)
                      (λ x →
                         (hom-morphism ϕ ∘ π (interp-ctx B) x) ∘
                         tuple (interp-ctx B) (oper-arity f)
                         (λ i → hom-morphism ψ ∘ π (interp-ctx A) i))) ≈⟨ (refl⟩∘⟨ tuple-cong (interp-sort C) (interp-ctx C) λ i → assoc) ⟩
                    (interp-oper C f ∘
                      tuple (interp-ctx C) (oper-arity f)
                      (λ z →
                         hom-morphism ϕ ∘
                         π (interp-ctx B) z ∘
                         tuple (interp-ctx B) (oper-arity f)
                         (λ i → hom-morphism ψ ∘ π (interp-ctx A) i))) ≈⟨ (refl⟩∘⟨ tuple-cong (interp-sort C) (interp-ctx C) λ i → refl⟩∘⟨ project (interp-ctx B)) ⟩
                    (interp-oper C f ∘
                      tuple (interp-ctx C) (oper-arity f)
                      (λ z → hom-morphism ϕ ∘ hom-morphism ψ ∘ π (interp-ctx A) z)) ≈⟨ (refl⟩∘⟨ tuple-cong (interp-sort C) (interp-ctx C) λ i → sym-assoc) ⟩
                   (interp-oper C f ∘
                     tuple (interp-ctx C) (oper-arity f)
                     (λ z → (hom-morphism ϕ ∘ hom-morphism ψ) ∘ π (interp-ctx A) z)) ∎}

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
-- Andreas, 2018-10-18, issue #3289 reported by Ulf
-- Andreas, 2021-02-10, fix rhs occurrence
--
-- For postfix projections, we have no hiding info
-- for the eliminated record value.

-- Thus, contrary to the prefix case, it cannot be
-- taken into account (e.g. for projection disambiguation).

open import Agda.Builtin.Nat

record R : Set where
  field
    p : Nat

open R {{...}}

lhs : R
lhs .p = 0

rhs : R → Nat
rhs r = r .p

-- Error WAS:  Wrong hiding used for projection  R.p

-- Should work now.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts

module type-assignment-unicity where
  -- type assignment only assigns one type
  type-assignment-unicity : {Γ : tctx} {d : ihexp} {τ' τ : htyp} {Δ : hctx} →
                              Δ , Γ ⊢ d :: τ →
                              Δ , Γ ⊢ d :: τ' →
                              τ == τ'
  type-assignment-unicity TANum TANum = refl
  type-assignment-unicity (TAPlus x x₁) (TAPlus x₂ x₃) = refl
  type-assignment-unicity {Γ = Γ} (TAVar x₁) (TAVar x₂) = ctxunicity {Γ = Γ} x₁ x₂
  type-assignment-unicity (TALam _ d1) (TALam _ d2)
    with type-assignment-unicity d1 d2
  ... | refl = refl
  type-assignment-unicity (TAAp x x₁) (TAAp y y₁)
    with type-assignment-unicity x y
  ... | refl = refl
  type-assignment-unicity (TAInl x) (TAInl y)
    with type-assignment-unicity x y
  ... | refl = refl
  type-assignment-unicity (TAInr x) (TAInr y)
    with type-assignment-unicity x y
  ... | refl = refl
  type-assignment-unicity (TACase d _ x _ y) (TACase d₁ _ x₁ _ y₁)
    with type-assignment-unicity d d₁
  ... | refl with type-assignment-unicity x x₁
  ... | refl = refl
  type-assignment-unicity (TAEHole {Δ = Δ} x y) (TAEHole x₁ x₂)
    with ctxunicity {Γ = Δ} x x₁
  ... | refl = refl
  type-assignment-unicity (TANEHole {Δ = Δ} x d1 y) (TANEHole x₁ d2 x₂)
    with ctxunicity {Γ = Δ} x₁ x
  ... | refl = refl
  type-assignment-unicity (TACast d1 x) (TACast d2 x₁)
    with type-assignment-unicity d1 d2
  ... | refl = refl
  type-assignment-unicity (TAFailedCast x x₁ x₂ x₃) (TAFailedCast y x₄ x₅ x₆)
    with type-assignment-unicity x y
  ... | refl = refl
  type-assignment-unicity (TAPair x x₁) (TAPair y y₁)
    with type-assignment-unicity x y
  ... | refl with type-assignment-unicity x₁ y₁
  ... | refl = refl
  type-assignment-unicity (TAFst x) (TAFst y)
    with type-assignment-unicity x y
  ... | refl = refl
  type-assignment-unicity (TASnd x) (TASnd y)
    with type-assignment-unicity x y
  ... | refl = refl

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

open import SDG.Extra.OrderedAlgebra

module SDG.SDG {r₁ r₂} (R : OrderedCommutativeRing r₁ r₂) where

open OrderedCommutativeRing R renaming (Carrier to Rc)

open import Data.Product
open import Data.Sum

open import Algebra

-- note: SDG should probably be a record if i need to
--       use some particular topos model

--nilsqr : {!!}
nilsqr = λ x → (x * x) ≈ 0#

nilsqr-0# : nilsqr 0#
nilsqr-0# = zeroˡ 0#

--D : {!!}
D = Σ[ x ∈ Rc ] (nilsqr x)

D→R : D → Rc
D→R d = proj₁ d

R→D : (x : Rc) → nilsqr x → D
R→D x nilsqr = x , nilsqr

d0 : D
d0 = R→D 0# nilsqr-0#

postulate
  kock-lawvere : ∀ (g : D → Rc) →
                   ∃! _≈_ (λ b → ∀ (d : D) → ((g d) ≈ ((g d0) + (D→R d * b))))

-- these definitions are modified from previous development based on Bell:

gₓ : ∀ (f : Rc → Rc) (x : Rc) → (D → Rc)
gₓ f x d = f (x + D→R d)

∃!b : ∀ (f : Rc → Rc) (x : Rc) → ∃! _≈_ (λ b → ∀ (d : D) → ((gₓ f x d) ≈ ((gₓ f x d0) + (D→R d * b))))
∃!b f x = kock-lawvere (gₓ f x)

_′ : (f : Rc → Rc) → (Rc → Rc)
(f ′) x = proj₁ (∃!b f x)

max_stars_repo_name: wrrnhttn/agda-sdg

max_issues_repo_name: wrrnhttn/agda-sdg

max_forks_repo_name: wrrnhttn/agda-sdg


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

open import Cubical.Data.FinData.Base public
open import Cubical.Data.FinData.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Extensions.Fin where

open import Prelude
open import Data.Fin hiding (_<_)
open import Data.Nat


text:
------------------------------------------------------------------------------
-- Arithmetic properties
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
-- Totality properties

pred-N : ∀ {n} → N n → N (pred₁ n)
pred-N nzero = prf
  where postulate prf : N (pred₁ zero)
        {-# ATP prove prf #-}

pred-N (nsucc {n} Nn) = prf
  where postulate prf : N (pred₁ (succ₁ n))
        {-# ATP prove prf #-}

+-N : ∀ {m n} → N m → N n → N (m + n)
+-N {n = n} nzero Nn = prf
  where postulate prf : N (zero + n)
        {-# ATP prove prf #-}
+-N {n = n} (nsucc {m} Nm) Nn = prf (+-N Nm Nn)
  where postulate prf : N (m + n) → N (succ₁ m + n)
        {-# ATP prove prf #-}

∸-N : ∀ {m n} → N m → N n → N (m ∸ n)
∸-N {m} Nm nzero = prf
  where postulate prf : N (m ∸ zero)
        {-# ATP prove prf #-}
∸-N {m} Nm (nsucc {n} Nn) = prf (∸-N Nm Nn)
  where postulate prf : N (m ∸ n) → N (m ∸ succ₁ n)
        {-# ATP prove prf pred-N #-}

*-N : ∀ {m n} → N m → N n → N (m * n)
*-N {n = n} nzero Nn = prf
  where postulate prf : N (zero * n)
        {-# ATP prove prf #-}
*-N {n = n} (nsucc {m} Nm) Nn = prf (*-N Nm Nn)
  where postulate prf : N (m * n) → N (succ₁ m * n)
        {-# ATP prove prf +-N #-}

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

Sx≢x : ∀ {n} → N n → succ₁ n ≢ n
Sx≢x nzero h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}
Sx≢x (nsucc {n} Nn) h = prf (Sx≢x Nn)
  where postulate prf : succ₁ n ≢ n → ⊥
        {-# ATP prove prf #-}

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity n = +-0x n

+-rightIdentity : ∀ {n} → N n → n + zero ≡ n
+-rightIdentity nzero          = +-leftIdentity zero
+-rightIdentity (nsucc {n} Nn) = prf (+-rightIdentity Nn)
   where postulate prf : n + zero ≡ n → succ₁ n + zero ≡ succ₁ n
         {-# ATP prove prf #-}

+-assoc : ∀ {m} → N m → ∀ n o → m + n + o ≡ m + (n + o)
+-assoc nzero n o = prf
  where postulate prf : zero + n + o ≡ zero + (n + o)
        {-# ATP prove prf #-}
+-assoc (nsucc {m} Nm) n o = prf (+-assoc Nm n o)
  where postulate prf : m + n + o ≡ m + (n + o) →
                        succ₁ m + n + o ≡ succ₁ m + (n + o)
        {-# ATP prove prf #-}

x+Sy≡S[x+y] : ∀ {m} → N m → ∀ n → m + succ₁ n ≡ succ₁ (m + n)
x+Sy≡S[x+y] nzero n = prf
  where postulate prf : zero + succ₁ n ≡ succ₁ (zero + n)
        {-# ATP prove prf #-}
x+Sy≡S[x+y] (nsucc {m} Nm) n = prf (x+Sy≡S[x+y] Nm n)
  where postulate prf : m + succ₁ n ≡ succ₁ (m + n) →
                        succ₁ m + succ₁ n ≡ succ₁ (succ₁ m + n)
        {-# ATP prove prf #-}

+-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
+-comm {n = n} nzero Nn = prf
  where postulate prf : zero + n ≡ n + zero
        {-# ATP prove prf +-rightIdentity #-}
+-comm {n = n} (nsucc {m} Nm) Nn = prf (+-comm Nm Nn)
  where postulate prf : m + n ≡ n + m → succ₁ m + n ≡ n + succ₁ m
        {-# ATP prove prf x+Sy≡S[x+y] #-}

x+S0≡Sx : ∀ {n} → N n → n + succ₁ zero ≡ succ₁ n
x+S0≡Sx nzero          = +-leftIdentity (succ₁ zero)
x+S0≡Sx (nsucc {n} Nn) = prf (x+S0≡Sx Nn)
  where postulate prf : n + succ₁ zero ≡ succ₁ n →
                        succ₁ n + succ₁ zero ≡ succ₁ (succ₁ n)
        {-# ATP prove prf #-}

0∸x : ∀ {n} → N n → zero ∸ n ≡ zero
0∸x nzero          = ∸-x0 zero
0∸x (nsucc {n} Nn) = prf (0∸x Nn)
  where postulate prf : zero ∸ n ≡ zero → zero ∸ succ₁ n ≡ zero
        {-# ATP prove prf #-}

S∸S : ∀ {m n} → N m → N n → succ₁ m ∸ succ₁ n ≡ m ∸ n
S∸S {m} Nm nzero = prf
  where postulate prf : succ₁ m ∸ succ₁ zero ≡ m ∸ zero
        {-# ATP prove prf #-}

S∸S {m} Nm (nsucc {n} Nn) = prf (S∸S Nm Nn)
  where postulate prf : succ₁ m ∸ succ₁ n ≡ m ∸ n →
                        succ₁ m ∸ succ₁ (succ₁ n) ≡ m ∸ succ₁ n
        {-# ATP prove prf #-}

x∸x≡0 : ∀ {n} → N n → n ∸ n ≡ zero
x∸x≡0 nzero          = ∸-x0 zero
x∸x≡0 (nsucc {n} Nn) = prf (x∸x≡0 Nn)
  where postulate prf : n ∸ n ≡ zero → succ₁ n ∸ succ₁ n ≡ zero
        {-# ATP prove prf S∸S #-}

Sx∸x≡S0 : ∀ {n} → N n → succ₁ n ∸ n ≡ succ₁ zero
Sx∸x≡S0 nzero =  prf
  where postulate prf : succ₁ zero ∸ zero ≡ succ₁ zero
        {-# ATP prove prf #-}
Sx∸x≡S0 (nsucc {n} Nn) = prf (Sx∸x≡S0 Nn)
  where postulate prf : succ₁ n ∸ n ≡ succ₁ zero →
                        succ₁ (succ₁ n) ∸ succ₁ n ≡ succ₁ zero
        {-# ATP prove prf S∸S #-}

[x+Sy]∸y≡Sx : ∀ {m n} → N m → N n → (m + succ₁ n) ∸ n ≡ succ₁ m
[x+Sy]∸y≡Sx {n = n} nzero Nn = prf
  where postulate prf : zero + succ₁ n ∸ n ≡ succ₁ zero
        {-# ATP prove prf Sx∸x≡S0 #-}
[x+Sy]∸y≡Sx (nsucc {m} Nm) nzero = prf
  where postulate prf : succ₁ m + succ₁ zero ∸ zero ≡ succ₁ (succ₁ m)
        {-# ATP prove prf x+S0≡Sx #-}

[x+Sy]∸y≡Sx (nsucc {m} Nm) (nsucc {n} Nn) = prf ([x+Sy]∸y≡Sx (nsucc Nm) Nn)
  where postulate prf : succ₁ m + succ₁ n ∸ n ≡ succ₁ (succ₁ m) →
                        succ₁ m + succ₁ (succ₁ n) ∸ succ₁ n ≡ succ₁ (succ₁ m)
        {-# ATP prove prf S∸S +-N x+Sy≡S[x+y] #-}

[x+y]∸[x+z]≡y∸z : ∀ {m n o} → N m → N n → N o → (m + n) ∸ (m + o) ≡ n ∸ o
[x+y]∸[x+z]≡y∸z {n = n} {o} nzero Nn No = prf
  where postulate prf : (zero + n) ∸ (zero + o) ≡ n ∸ o
        {-# ATP prove prf #-}

[x+y]∸[x+z]≡y∸z {n = n} {o} (nsucc {m} Nm) Nn No = prf ([x+y]∸[x+z]≡y∸z Nm Nn No)
  where postulate prf : (m + n) ∸ (m + o) ≡ n ∸ o →
                        (succ₁ m + n) ∸ (succ₁ m + o) ≡ n ∸ o
        {-# ATP prove prf +-N S∸S #-}

*-leftZero : ∀ n → zero * n ≡ zero
*-leftZero = *-0x

*-rightZero : ∀ {n} → N n → n * zero ≡ zero
*-rightZero nzero          = *-leftZero zero
*-rightZero (nsucc {n} Nn) = prf (*-rightZero Nn)
  where postulate prf : n * zero ≡ zero → succ₁ n * zero ≡ zero
        {-# ATP prove prf #-}

postulate *-leftIdentity : ∀ {n} → N n → succ₁ zero * n ≡ n
{-# ATP prove *-leftIdentity +-rightIdentity #-}

x*Sy≡x+xy : ∀ {m n} → N m → N n → m * succ₁ n ≡ m + m * n
x*Sy≡x+xy {n = n} nzero Nn = prf
  where postulate prf : zero * succ₁ n ≡ zero + zero * n
        {-# ATP prove prf #-}
x*Sy≡x+xy {n = n} (nsucc {m} Nm) Nn = prf (x*Sy≡x+xy Nm Nn)
                                       (+-assoc Nn m (m * n))
                                       (+-assoc Nm n (m * n))
  where
  -- N.B. We had to feed the ATP with the instances of the associate law
  postulate prf :  m * succ₁ n ≡ m + m * n →
                   (n + m) + (m * n) ≡ n + (m + (m * n)) →  -- Associative law
                   (m + n) + (m * n) ≡ m + (n + (m * n)) →  -- Associateve law
                   succ₁ m * succ₁ n ≡ succ₁ m + succ₁ m * n
  {-# ATP prove prf +-comm #-}

*-comm : ∀ {m n} → N m → N n → m * n ≡ n * m
*-comm {n = n} nzero Nn = prf
  where postulate prf : zero * n ≡ n * zero
        {-# ATP prove prf *-rightZero #-}
*-comm {n = n} (nsucc {m} Nm) Nn = prf (*-comm Nm Nn)
  where postulate prf : m * n ≡ n * m → succ₁ m * n ≡ n * succ₁ m
        {-# ATP prove prf x*Sy≡x+xy #-}

*-rightIdentity : ∀ {n} → N n → n * succ₁ zero ≡ n
*-rightIdentity nzero = prf
  where postulate prf : zero * succ₁ zero ≡ zero
        {-# ATP prove prf #-}
*-rightIdentity (nsucc {n} Nn) = prf (*-rightIdentity Nn)
  where postulate prf : n * succ₁ zero ≡ n →
                        succ₁ n * succ₁ zero ≡ succ₁ n
        {-# ATP prove prf #-}

*∸-leftDistributive : ∀ {m n o} → N m → N n → N o → (m ∸ n) * o ≡ m * o ∸ n * o
*∸-leftDistributive {m} {o = o} Nm nzero No = prf
  where postulate prf : (m ∸ zero) * o ≡ m * o ∸ zero * o
        {-# ATP prove prf #-}

*∸-leftDistributive {o = o} nzero (nsucc {n} Nn) No = prf
  where postulate prf : (zero ∸ succ₁ n) * o ≡ zero * o ∸ succ₁ n * o
        {-# ATP prove prf 0∸x *-N #-}

*∸-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) nzero = prf
  where
  postulate prf : (succ₁ m ∸ succ₁ n) * zero ≡ succ₁ m * zero ∸ succ₁ n * zero
  {-# ATP prove prf ∸-N *-comm #-}

*∸-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) =
  prf (*∸-leftDistributive Nm Nn (nsucc No))
  where
  postulate prf : (m ∸ n) * succ₁ o ≡ m * succ₁ o ∸ n * succ₁ o →
                  (succ₁ m ∸ succ₁ n) * succ₁ o ≡
                  succ₁ m * succ₁ o ∸ succ₁ n * succ₁ o
  {-# ATP prove prf [x+y]∸[x+z]≡y∸z S∸S *-N #-}

*+-leftDistributive : ∀ {m n o} → N m → N n → N o → (m + n) * o ≡ m * o + n * o
*+-leftDistributive {m} {n} Nm Nn nzero = prf
  where postulate prf : (m + n) * zero ≡ m * zero + n * zero
        {-# ATP prove prf *-comm +-rightIdentity *-N +-N #-}

*+-leftDistributive {n = n} nzero Nn (nsucc {o} No) = prf
  where postulate prf :  (zero + n) * succ₁ o ≡ zero * succ₁ o + n * succ₁ o
        {-# ATP prove prf #-}

*+-leftDistributive (nsucc {m} Nm) nzero (nsucc {o} No) = prf
  where
  postulate prf : (succ₁ m + zero) * succ₁ o ≡ succ₁ m * succ₁ o + zero * succ₁ o
  {-# ATP prove prf +-rightIdentity *-N #-}

*+-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) =
  prf (*+-leftDistributive Nm (nsucc Nn) (nsucc No))
  where
  postulate
    prf : (m + succ₁ n) * succ₁ o ≡ m * succ₁ o + succ₁ n * succ₁ o →
          (succ₁ m + succ₁ n) * succ₁ o ≡ succ₁ m * succ₁ o + succ₁ n * succ₁ o
  {-# ATP prove prf +-assoc *-N #-}

xy≡0→x≡0∨y≡0 : ∀ {m n} → N m → N n → m * n ≡ zero → m ≡ zero ∨ n ≡ zero
xy≡0→x≡0∨y≡0 {n = n} nzero Nn h = prf
  where postulate prf : zero ≡ zero ∨ n ≡ zero
        {-# ATP prove prf #-}
xy≡0→x≡0∨y≡0 (nsucc {m} Nm) nzero h = prf
  where postulate prf : succ₁ m ≡ zero ∨ zero ≡ zero
        {-# ATP prove prf #-}
xy≡0→x≡0∨y≡0 (nsucc {m} Nm) (nsucc {n} Nn) SmSn≡0 = ⊥-elim (0≢S prf)
  where postulate prf : zero ≡ succ₁ (n + m * succ₁ n)
        {-# ATP prove prf #-}

xy≡1→x≡1 : ∀ {m n} → N m → N n → m * n ≡ 1' → m ≡ 1'
xy≡1→x≡1 {n = n} nzero Nn h = ⊥-elim prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}
xy≡1→x≡1 (nsucc nzero) Nn h = refl
xy≡1→x≡1 (nsucc (nsucc {m} Nm)) nzero h = ⊥-elim prf
  where postulate prf : ⊥
        {-# ATP prove prf *-rightZero #-}
xy≡1→x≡1 (nsucc (nsucc {m} Nm)) (nsucc {n} Nn) h = ⊥-elim (0≢S prf)
  where postulate prf : zero ≡ succ₁ (m + n * succ₁ (succ₁ m))
        {-# ATP prove prf *-comm #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Sometimes we can't infer a record type

module InferRecordTypes-3 where

postulate A : Set

record R : Set₁ where
  field
    x₁ : Set
    x₂ : Set

record R′ : Set₁ where
  field
    x₁ : Set
    x₃ : Set

bad = record { x₂ =  A; x₃ = A }


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

open import Base
open import Algebra.Groups
open import Integers

module Algebra.GroupIntegers where

_+_ : ℤ → ℤ → ℤ
O + m = m
pos O + m = succ m
pos (S n) + m = succ (pos n + m)
neg O + m = pred m
neg (S n) + m = pred (neg n + m)

-_ : ℤ → ℤ
- O = O
- (pos m) = neg m
- (neg m) = pos m

+-succ : (m n : ℤ) → succ m + n ≡ succ (m + n)
+-succ O n = refl _
+-succ (pos m) n = refl _
+-succ (neg O) n = ! (succ-pred n)
+-succ (neg (S m)) n = ! (succ-pred _)

+-pred : (m n : ℤ) → pred m + n ≡ pred (m + n)
+-pred O n = refl _
+-pred (pos O) n = ! (pred-succ n)
+-pred (pos (S m)) n = ! (pred-succ _)
+-pred (neg m) n = refl _

+-assoc : (m n p : ℤ) → (m + n) + p ≡ m + (n + p)
+-assoc O n p = refl _
+-assoc (pos O) n p = +-succ n p
+-assoc (pos (S m)) n p = +-succ (pos m + n) p ∘ map succ (+-assoc (pos m) n p)
+-assoc (neg O) n p = +-pred n p
+-assoc (neg (S m)) n p = +-pred (neg m + n) p ∘ map pred (+-assoc (neg m) n p)

O-right-unit : (m : ℤ) → m + O ≡ m
O-right-unit O = refl _
O-right-unit (pos O) = refl _
O-right-unit (pos (S m)) = map succ (O-right-unit (pos m))
O-right-unit (neg O) = refl _
O-right-unit (neg (S m)) = map pred (O-right-unit (neg m))

succ-+-right : (m n : ℤ) → succ (m + n) ≡ m + succ n
succ-+-right O n = refl _
succ-+-right (pos O) n = refl _
succ-+-right (pos (S m)) n = map succ (succ-+-right (pos m) n)
succ-+-right (neg O) n = succ-pred n ∘ ! (pred-succ n)
succ-+-right (neg (S m)) n = (succ-pred (neg m + n) ∘ ! (pred-succ (neg m + n)))
                             ∘ map pred (succ-+-right (neg m) n)

pred-+-right : (m n : ℤ) → pred (m + n) ≡ m + pred n
pred-+-right O n = refl _
pred-+-right (pos O) n = pred-succ n ∘ ! (succ-pred n)
pred-+-right (pos (S m)) n = (pred-succ (pos m + n) ∘ ! (succ-pred (pos m + n)))
                             ∘ map succ (pred-+-right (pos m) n)
pred-+-right (neg O) n = refl _
pred-+-right (neg (S m)) n = map pred (pred-+-right (neg m) n)

opp-right-inverse : (m : ℤ) → m + (- m) ≡ O
opp-right-inverse O = refl O
opp-right-inverse (pos O) = refl O
opp-right-inverse (pos (S m)) = succ-+-right (pos m) (neg (S m))
                                ∘ opp-right-inverse (pos m)
opp-right-inverse (neg O) = refl O
opp-right-inverse (neg (S m)) = pred-+-right (neg m) (pos (S m))
                                ∘ opp-right-inverse (neg m)

opp-left-inverse : (m : ℤ) → (- m) + m ≡ O
opp-left-inverse O = refl O
opp-left-inverse (pos O) = refl O
opp-left-inverse (pos (S m)) = pred-+-right (neg m) (pos (S m))
                               ∘ opp-left-inverse (pos m)
opp-left-inverse (neg O) = refl O
opp-left-inverse (neg (S m)) = succ-+-right (pos m) (neg (S m))
                               ∘ opp-left-inverse (neg m)
                 -- pred-+-right (neg m) (pos (S m)) ∘ opp-left-inverse (pos m)

ℤ-group : Group _
ℤ-group = group (pregroup
  ℤ
  _+_ O -_
  +-assoc O-right-unit (λ m → refl _) opp-right-inverse opp-left-inverse)
  ℤ-is-set

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------------
-- Testing the erasing of proof terms
------------------------------------------------------------------------------

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

module ProofTerm2 where

postulate
  D   : Set
  N   : D → Set
  _≡_ : D → D → Set

postulate foo : ∀ {m n} → (Nm : N m) → (Nn : N n) → m ≡ m
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module LateMetaVariableInstantiation where

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}

postulate
  yippie : (A : Set) → A

slow : (A : Set) → ℕ → A
slow A zero    = yippie A
slow A (suc n) = slow _ n

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

foo : slow ℕ 1000 ≡ yippie ℕ
foo = refl

-- Consider the function slow. Previously normalisation of slow n
-- seemed to take time proportional to n². The reason was that, even
-- though the meta-variable corresponding to the underscore was
-- solved, the stored code still contained a meta-variable:

--   slow A (suc n) = slow (_173 A n) n

-- (For some value of 173.) The evaluation proceeded as follows:

--   slow A 1000 =
--   slow (_173 A 999) 999 =
--   slow (_173 (_173 A 999) 998) 998 =
--   ...

-- Furthermore, in every iteration the Set argument was traversed, to
-- see if there was any de Bruijn index to raise.


text:
module _ where

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

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

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

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

T : Bool → Set
T false = Nat
T true  = Nat → Nat

bla : (Nat → Nat) → Nat → Nat
bla f zero = zero
bla f = f  -- underapplied clause!

pred : Nat → Nat
pred zero = zero
pred (suc n) = n

-- 0 and 1 are both solutions, so should not be solved.
bad! : Constraint
bad! = bla pred _ == zero

-- Should not fail, since 2 is a solution!
more-bad! : Constraint
more-bad! = bla pred _ == 1

-- Same thing for projections

blabla : Nat → Nat × Nat
blabla zero    = 1 , 1
blabla (suc n) = 0 , n

-- Don't fail: 0 is a valid solution
oops : Constraint
oops = fst (blabla _) == 1

bla₂ : Bool → Nat × Nat
bla₂ false = 0 , 1
bla₂ true .fst = 0
bla₂ true .snd = 1

-- Don't solve: false and true are both solutions
wrong : Constraint
wrong = bla₂ _ .fst == 0


text:
{-# OPTIONS --cubical --safe #-}
module Multidimensional.Data.Extra.Nat where

open import Multidimensional.Data.Extra.Nat.Base public

open import Multidimensional.Data.Extra.Nat.Properties public

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


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

open import HoTT

module homotopy.CircleCover {j} where

record S¹Cover : Type (lsucc j) where
  constructor s¹cover
  field
    El : Type j
    {{El-level}} : is-set El
    El-auto : El ≃ El

S¹cover-to-S¹-cover : S¹Cover → Cover S¹ j
S¹cover-to-S¹-cover sc = record {
  Fiber = S¹-rec El (ua El-auto);
  Fiber-level = λ {a} → S¹-elim {P = λ a → is-set (S¹-rec El (ua El-auto) a)} El-level prop-has-all-paths-↓ a}
  where open S¹Cover sc

S¹-cover-to-S¹cover : Cover S¹ j → S¹Cover
S¹-cover-to-S¹cover c = record {
  El = Fiber base;
  El-auto = coe-equiv (ap Fiber loop)}
  where open Cover c

S¹cover-equiv-S¹-cover : S¹Cover ≃ Cover S¹ j
S¹cover-equiv-S¹-cover = equiv to from to-from from-to where
  to = S¹cover-to-S¹-cover
  from = S¹-cover-to-S¹cover
  to-from : ∀ c → to (from c) == c
  to-from c = cover=' $ λ= $
    S¹-elim idp $ ↓-='-in' $ ! $
      ap (S¹-rec (Fiber base) (ua (coe-equiv (ap Fiber loop)))) loop
        =⟨ S¹Rec.loop-β _ _ ⟩
      ua (coe-equiv (ap Fiber loop))
        =⟨ ua-η _ ⟩
      ap Fiber loop
        =∎
    where open Cover c
  from-to : ∀ sc → from (to sc) == sc
  from-to sc = ap (λ eq → s¹cover El eq) $
    coe-equiv (ap (S¹-rec El (ua El-auto)) loop)
      =⟨ ap coe-equiv $ S¹Rec.loop-β _ _ ⟩
    coe-equiv (ua El-auto)
      =⟨ coe-equiv-β El-auto ⟩
    El-auto
      =∎
    where open S¹Cover sc

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- This module closely follows a section of Martín Escardó's HoTT lecture notes:
-- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#equivalenceinduction
{-# OPTIONS --without-K #-}
module Util.HoTT.Equiv.Induction where

open import Util.HoTT.HLevel.Core
open import Util.HoTT.Equiv
open import Util.HoTT.Univalence.ContrFormulation
open import Util.Prelude

private
  variable
    α β γ : Level

G-≃ : {A : Set α} (P : Σ[ B ∈ Set α ] (A ≃ B) → Set β)
  → P (A , ≃-refl)
  → ∀ {B} (A≃B : A ≃ B)
  → P (B , A≃B)
G-≃ {A = A} P p {B} A≃B = subst P (univalenceProp A (A , ≃-refl) (B , A≃B)) p

abstract
  G-≃-β : {A : Set α} (P : Σ[ B ∈ Set α ] (A ≃ B) → Set β)
    → (p : P (A , ≃-refl))
    → G-≃ P p ≃-refl ≡ p
  G-≃-β {A = A} P p = subst (λ q → subst P q p ≡ p) (sym go) refl
    where
      go : univalenceProp A (A , ≃-refl) (A , ≃-refl) ≡ refl
      go = IsContr→IsSet (univalenceContr A) _ _

H-≃ : {A : Set α} (P : (B : Set α) → A ≃ B → Set β)
  → P A ≃-refl
  → ∀ {B} (A≃B : A ≃ B)
  → P B A≃B
H-≃ P p A≃B = G-≃ (λ { (B , A≃B) → P B A≃B }) p A≃B

abstract
  H-≃-β : {A : Set α} (P : (B : Set α) → A ≃ B → Set β)
    → (p : P A ≃-refl)
    → H-≃ P p ≃-refl ≡ p
  H-≃-β P p = G-≃-β (λ { (B , A≃B) → P B A≃B }) p

J-≃ : (P : (A B : Set α) → A ≃ B → Set β)
  → (∀ A → P A A ≃-refl)
  → ∀ {A B} (A≃B : A ≃ B)
  → P A B A≃B
J-≃ P p {A} {B} A≃B = H-≃ (λ B A≃B → P A B A≃B) (p A) A≃B

abstract
  J-≃-β : (P : (A B : Set α) → A ≃ B → Set β)
    → (p : ∀ A → P A A ≃-refl)
    → ∀ {A}
    → J-≃ P p ≃-refl ≡ p A
  J-≃-β P p {A} = H-≃-β (λ B A≃B → P A B A≃B) (p A)

H-IsEquiv : {A : Set α} (P : (B : Set α) → (A → B) → Set β)
  → P A id
  → ∀ {B} (f : A → B)
  → IsEquiv f
  → P B f
H-IsEquiv P p f f-equiv
  = H-≃ (λ B A≃B → P B (A≃B .forth)) p
      (record { forth = f ; isEquiv = f-equiv })

J-IsEquiv : (P : (A B : Set α) → (A → B) → Set β)
  → (∀ A → P A A id)
  → ∀ {A B} (f : A → B)
  → IsEquiv f
  → P A B f
J-IsEquiv P p f f-equiv
  = J-≃ (λ A B A≃B → P A B (A≃B .forth)) p
      (record { forth = f ; isEquiv = f-equiv })

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
{-# OPTIONS --warning=error #-}

A : Set₁
A = Set

{-# POLARITY A #-}


text:
module UnSized.Console where

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

open import NativeIO

{-# TERMINATING #-}
myProgram  :  IOConsole Unit
force myProgram =  exec' getLine          λ line  →
                   delay (exec' (putStrLn line)  λ _     →
                   delay (exec' (putStrLn line)  λ _     →
                   myProgram
                   ))

main  :  NativeIO Unit
main  =  translateIOConsole myProgram

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Prelude.Variables where

open import Agda.Primitive
open import Agda.Builtin.Nat

variable
  ℓ ℓ₁ ℓ₂ ℓ₃ : Level
  A B : Set ℓ
  x y : A
  n m : Nat

max_stars_repo_name: jespercockx/agda-prelude

max_issues_repo_name: jespercockx/agda-prelude

max_forks_repo_name: jespercockx/agda-prelude


text:
open import core

module focus-formation where
  -- every ε is an evaluation context -- trivially, here, since we don't
  -- include any of the premises in red brackets about finality
  focus-formation : ∀{d d' ε} → d == ε ⟦ d' ⟧ → ε evalctx
  focus-formation FHOuter = ECDot
  focus-formation (FHAp1 sub) = ECAp1 (focus-formation sub)
  focus-formation (FHAp2 sub) = ECAp2 (focus-formation sub)
  focus-formation (FHNEHole sub) = ECNEHole (focus-formation sub)
  focus-formation (FHCast sub) = ECCast (focus-formation sub)
  focus-formation (FHFailedCast x) = ECFailedCast (focus-formation x)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


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

open import HoTT
open import homotopy.PtdAdjoint
open import homotopy.SuspAdjointLoop
open import cohomology.Exactness
open import cohomology.FunctionOver
open import cohomology.MayerVietoris
open import cohomology.Theory

{- Standard Mayer-Vietoris exact sequence (algebraic) derived from
 - the result in cohomology.MayerVietoris (topological).
 - This is a whole bunch of algebra which is not very interesting.
 -}

module cohomology.MayerVietorisExact {i} (CT : CohomologyTheory i)
  (n : ℤ) (ps : ⊙Span {i} {i} {i}) where

open MayerVietorisFunctions ps
module MV = MayerVietoris ps
open ⊙Span ps

open CohomologyTheory CT
open import cohomology.BaseIndependence CT
open import cohomology.Functor CT
open import cohomology.InverseInSusp CT
open import cohomology.LongExactSequence CT n ⊙reglue
open import cohomology.Wedge CT

mayer-vietoris-seq : HomSequence _ _
mayer-vietoris-seq =
  C n (⊙Pushout ps)
    ⟨ ×ᴳ-hom-in (CF-hom n (⊙left ps)) (CF-hom n (⊙right ps)) ⟩→
  C n X ×ᴳ C n Y
    ⟨ ×ᴳ-sum-hom (C-abelian _ _) (CF-hom n f)
                 (inv-hom _ (C-abelian _ _) ∘ᴳ (CF-hom n g)) ⟩→
  C n Z
    ⟨ CF-hom (succ n) ⊙ext-glue ∘ᴳ fst ((C-Susp n Z)⁻¹ᴳ) ⟩→
  C (succ n) (⊙Pushout ps)
    ⟨ ×ᴳ-hom-in (CF-hom _ (⊙left ps)) (CF-hom _ (⊙right ps)) ⟩→
  C (succ n) X ×ᴳ C (succ n) Y ⊣|

mayer-vietoris-exact : is-exact-seq mayer-vietoris-seq
mayer-vietoris-exact =
  transport (λ {(r , s) → is-exact-seq s})
    (pair= _ $ sequence= _ _ $
      idp
        ∥⟨ ↓-over-×-in _→ᴳ_ idp (CWedge.⊙wedge-rec-over n X Y _ _) ⟩∥
      CWedge.path n X Y
        ∥⟨ ↓-over-×-in' _→ᴳ_
             (ap↓ (λ φ → φ ∘ᴳ fst (C-Susp n (X ⊙∨ Y) ⁻¹ᴳ))
                  (CF-↓cod= (succ n) MV.ext-over)
              ∙ᵈ codomain-over-iso {χ = diff'} (codomain-over-equiv _ _))
             (CWedge.wedge-hom-η n X Y _
              ▹ ap2 (×ᴳ-sum-hom (C-abelian n Z)) inl-lemma inr-lemma) ⟩∥
      ap (C (succ n)) MV.⊙path ∙ group-ua (C-Susp n Z)
        ∥⟨ ↓-over-×-in _→ᴳ_
            (CF-↓dom= (succ n) MV.cfcod-over
             ∙ᵈ domain-over-iso
                  (! (ap (λ h → CF _ ⊙ext-glue ∘ h)
                     (λ= (is-equiv.g-f (snd (C-Susp n Z)))))
                   ◃ domain-over-equiv _ _))
            idp                                              ⟩∥
      idp
        ∥⟨ ↓-over-×-in _→ᴳ_ idp (CWedge.⊙wedge-rec-over (succ n) X Y _ _) ⟩∥
      CWedge.path (succ n) X Y ∥⊣|)
    long-cofiber-exact
  where
  {- shorthand -}
  diff' = fst (C-Susp n Z) ∘ᴳ CF-hom (succ n) MV.⊙mv-diff
                           ∘ᴳ fst (C-Susp n (X ⊙∨ Y) ⁻¹ᴳ)

  {- Variations on suspension axiom naturality -}
  natural-lemma₁ : {X Y : Ptd i} (n : ℤ) (f : fst (X ⊙→ Y))
    → (fst (C-Susp n X) ∘ᴳ CF-hom _ (⊙susp-fmap f)) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ)
      == CF-hom n f
  natural-lemma₁ {X} {Y} n f =
    ap (λ φ → φ ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ)) (C-SuspF n f)
    ∙ hom= _ _ (λ= (ap (CF n f) ∘ is-equiv.f-g (snd (C-Susp n Y))))

  natural-lemma₂ : {X Y : Ptd i} (n : ℤ) (f : fst (X ⊙→ Y))
    → CF-hom _ (⊙susp-fmap f) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ)
      == fst (C-Susp n X ⁻¹ᴳ) ∘ᴳ CF-hom n f
  natural-lemma₂ {X} {Y} n f =
    hom= _ _ (λ= (! ∘ is-equiv.g-f (snd (C-Susp n X))
                    ∘ CF _ (⊙susp-fmap f)
                    ∘ GroupHom.f (fst (C-Susp n Y ⁻¹ᴳ))))
    ∙ ap (λ φ → fst (C-Susp n X ⁻¹ᴳ) ∘ᴳ φ) (natural-lemma₁ n f)

  {- Associativity lemmas -}
  assoc-lemma : ∀ {i} {G H K L J : Group i}
    (φ : L →ᴳ J) (ψ : K →ᴳ L) (χ : H →ᴳ K) (ξ : G →ᴳ H)
    → (φ ∘ᴳ ψ) ∘ᴳ χ ∘ᴳ ξ == φ ∘ᴳ ((ψ ∘ᴳ χ) ∘ᴳ ξ)
  assoc-lemma _ _ _ _ = hom= _ _ idp

  assoc-lemma₂ : ∀ {i} {G H K L J : Group i}
    (φ : L →ᴳ J) (ψ : K →ᴳ L) (χ : H →ᴳ K) (ξ : G →ᴳ H)
    → (φ ∘ᴳ ψ ∘ᴳ χ) ∘ᴳ ξ == φ ∘ᴳ ψ ∘ᴳ χ ∘ᴳ ξ
  assoc-lemma₂ _ _ _ _ = hom= _ _ idp

  inl-lemma : diff' ∘ᴳ CF-hom n (⊙projl X Y) == CF-hom n f
  inl-lemma =
    assoc-lemma₂
      (fst (C-Susp n Z)) (CF-hom (succ n) MV.⊙mv-diff)
      (fst (C-Susp n (X ⊙∨ Y) ⁻¹ᴳ)) (CF-hom n (⊙projl X Y))
    ∙ ap (λ φ → fst (C-Susp n Z) ∘ᴳ CF-hom (succ n) MV.⊙mv-diff ∘ᴳ φ)
         (! (natural-lemma₂ n (⊙projl X Y)))
    ∙ ! (assoc-lemma₂
           (fst (C-Susp n Z)) (CF-hom _ MV.⊙mv-diff)
           (CF-hom _ (⊙susp-fmap (⊙projl X Y)))
           (fst (C-Susp n X ⁻¹ᴳ)))
    ∙ ap (λ φ → (fst (C-Susp n Z) ∘ᴳ φ) ∘ᴳ fst (C-Susp n X ⁻¹ᴳ))
         (! (CF-comp _ (⊙susp-fmap (⊙projl X Y)) MV.⊙mv-diff))
    ∙ ap (λ φ → (fst (C-Susp n Z) ∘ᴳ φ) ∘ᴳ fst (C-Susp n X ⁻¹ᴳ))
         (CF-λ= (succ n) projl-mv-diff)
    ∙ natural-lemma₁ n f
    where
    {- Compute the left projection of mv-diff -}
    projl-mv-diff : (σz : fst (⊙Susp Z))
      → susp-fmap (projl X Y) (MV.mv-diff σz)
        == susp-fmap (fst f) σz
    projl-mv-diff = Suspension-elim _ idp (merid _ (snd X)) $
      ↓-='-from-square ∘ λ z →
        (ap-∘ (susp-fmap (projl X Y)) MV.mv-diff (merid _ z)
         ∙ ap (ap (susp-fmap (projl X Y))) (MV.MVDiff.glue-β z)
         ∙ ap-∙ (susp-fmap (projl X Y))
                (merid _ (winl (fst f z))) (! (merid _ (winr (fst g z))))
         ∙ (SuspFmap.glue-β (projl X Y) (winl (fst f z))
            ∙2 (ap-! (susp-fmap _) (merid _ (winr (fst g z)))
                ∙ ap ! (SuspFmap.glue-β (projl X Y) (winr (fst g z))))))
        ∙v⊡ (vid-square {p = merid _ (fst f z)}
             ⊡h rt-square (merid _ (snd X)))
        ⊡v∙ (∙-unit-r _ ∙ ! (SuspFmap.glue-β (fst f) z))

  inr-lemma : diff' ∘ᴳ CF-hom n (⊙projr X Y)
                           == inv-hom _ (C-abelian n Z) ∘ᴳ CF-hom n g
  inr-lemma =
    assoc-lemma₂
      (fst (C-Susp n Z)) (CF-hom (succ n) MV.⊙mv-diff)
      (fst (C-Susp n (X ⊙∨ Y) ⁻¹ᴳ)) (CF-hom n (⊙projr X Y))
    ∙ ap (λ φ → fst (C-Susp n Z) ∘ᴳ CF-hom (succ n) MV.⊙mv-diff ∘ᴳ φ)
         (! (natural-lemma₂ n (⊙projr X Y)))
    ∙ ! (assoc-lemma₂
           (fst (C-Susp n Z)) (CF-hom _ MV.⊙mv-diff)
           (CF-hom _ (⊙susp-fmap (⊙projr X Y)))
           (fst (C-Susp n Y ⁻¹ᴳ)))
    ∙ ap (λ φ → (fst (C-Susp n Z) ∘ᴳ φ) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (! (CF-comp _ (⊙susp-fmap (⊙projr X Y)) MV.⊙mv-diff))
    ∙ ∘ᴳ-assoc (fst (C-Susp n Z))
        (CF-hom _ (⊙susp-fmap (⊙projr X Y) ⊙∘ MV.⊙mv-diff))
        (fst (C-Susp n Y ⁻¹ᴳ))
    ∙ ap (λ φ → fst (C-Susp n Z) ∘ᴳ φ ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (CF-λ= (succ n) projr-mv-diff)
    ∙ ap (λ φ → fst (C-Susp n Z) ∘ᴳ φ ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (CF-comp _ (⊙susp-fmap g) (⊙flip-susp Z))
    ∙ ! (assoc-lemma (fst (C-Susp n Z)) (CF-hom _ (⊙flip-susp Z))
                     (CF-hom _ (⊙susp-fmap g)) (fst (C-Susp n Y ⁻¹ᴳ)))
    ∙ ap (λ φ → (fst (C-Susp n Z) ∘ᴳ φ)
                ∘ᴳ CF-hom _ (⊙susp-fmap g) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (C-flip-susp-is-inv (succ n))
    ∙ ap (λ φ → φ ∘ᴳ CF-hom _ (⊙susp-fmap g) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (inv-hom-natural (C-abelian _ _) (C-abelian _ _)
           (fst (C-Susp n Z)))
    ∙ assoc-lemma (inv-hom _ (C-abelian n Z)) (fst (C-Susp n Z))
                  (CF-hom _ (⊙susp-fmap g)) (fst (C-Susp n Y ⁻¹ᴳ))
    ∙ ap (λ φ → inv-hom _ (C-abelian n Z) ∘ᴳ φ) (natural-lemma₁ n g)
    where
    {- Compute the right projection of mv-diff -}
    projr-mv-diff : (σz : fst (⊙Susp Z))
      → susp-fmap (projr X Y) (MV.mv-diff σz)
        == susp-fmap (fst g) (flip-susp σz)
    projr-mv-diff = Suspension-elim _ (merid _ (snd Y)) idp $
      ↓-='-from-square ∘ λ z →
        (ap-∘ (susp-fmap (projr X Y)) MV.mv-diff (merid _ z)
         ∙ ap (ap (susp-fmap (projr X Y))) (MV.MVDiff.glue-β z)
         ∙ ap-∙ (susp-fmap (projr X Y))
             (merid _ (winl (fst f z))) (! (merid _ (winr (fst g z))))
         ∙ (SuspFmap.glue-β (projr X Y) (winl (fst f z))
            ∙2 (ap-! (susp-fmap (projr X Y))
                  (merid _ (winr (fst g z)))
                ∙ ap ! (SuspFmap.glue-β (projr X Y) (winr (fst g z))))))
        ∙v⊡ ((lt-square (merid _ (snd Y))
             ⊡h vid-square {p = ! (merid _ (fst g z))}))
        ⊡v∙ ! (ap-∘ (susp-fmap (fst g)) flip-susp (merid _ z)
               ∙ ap (ap (susp-fmap (fst g))) (FlipSusp.glue-β z)
               ∙ ap-! (susp-fmap (fst g)) (merid _ z)
               ∙ ap ! (SuspFmap.glue-β (fst g) z))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda


text:
--- Sample Sit file

{-# OPTIONS --experimental-irrelevance #-}
{-# OPTIONS --sized-types #-}

open import Base

--; --- Leibniz-equality

Eq : forall (A : Set) (a b : A) -> Set1 --;
Eq = \ A a b -> (P : A -> Set) -> (P a) -> P b

--; --- Reflexivity

refl : forall (A : Set) (a : A) -> Eq A a a --;
refl = \ A a P pa -> pa

--; --- Symmetry

sym : forall (A : Set) (a b : A) -> Eq A a b -> Eq A b a --;
sym = \ A a b eq P pb ->  eq (\ x -> P x -> P a) (\ pa -> pa) pb

--; --- Transitivity

trans : forall (A : Set) (a b c : A) -> Eq A a b -> Eq A b c -> Eq A a c --;
trans = \ A a b c p q P pa -> q P (p P pa)

--; --- Congruence

cong : forall (A B : Set) (f : A -> B) (a a' : A) -> Eq A a a' -> Eq B (f a) (f a') --;
cong = \ A B f a a' eq P pfa -> eq (\ x -> P (f x)) pfa

--; --- Addition

plus : forall .i -> Nat i -> Nat oo -> Nat oo --;
plus = \ i x y ->
  fix (\ i x -> Nat oo)
      (\ _ f -> \
              { (zero _)   -> y
              ; (suc _ x) -> suc oo (f x)
              })
      x

--; --- Unit tests for plus

inc : Nat oo -> Nat oo --;
inc = \ x -> suc oo x  --;

one : Nat oo        --;
one = inc (zero oo) --;

two : Nat oo  --;
two = inc one --;

three : Nat oo  --;
three = inc two --;

four : Nat oo  --;
four = inc three --;

five : Nat oo  --;
five = inc four --;

six : Nat oo  --;
six = inc five --;

plus_one_zero : Eq (Nat oo) (plus oo one (zero oo)) one --;
plus_one_zero = refl (Nat oo) one  --;

plus_one_one : Eq (Nat oo) (plus oo one one) two --;
plus_one_one = refl (Nat oo) two  --;

--; --- Reduction rules for plus

plus_red_zero : forall .i (y : Nat oo) -> Eq (Nat oo) (plus (i + 1) (zero i) y) y  --;
plus_red_zero = \ i y -> refl (Nat oo) y  --;

plus_red_suc : forall .i (x : Nat i) (y : Nat oo) -> Eq (Nat oo) (plus (i + 1) (suc i x) y) (suc oo (plus i x y))  --;
plus_red_suc = \ i x y -> refl (Nat oo) (suc oo (plus i x y))  --;

--; --- Law: x + 0 = x

plus_zero : forall .i (x : Nat i) -> Eq (Nat oo) (plus i x (zero oo)) x  --;
plus_zero = \ i x ->
  fix (\ i x -> Eq (Nat oo) (plus i x (zero oo)) x)
      (\ j f -> \
         { (zero _)  -> refl (Nat oo) (zero oo)
         ; (suc _ y) -> cong (Nat oo) (Nat oo) inc (plus j y (zero oo)) y (f y)
         })
      x

--; --- Law: x + suc y = suc x + y

plus_suc : forall .i (x : Nat i) (y : Nat oo) -> Eq (Nat oo) (plus i x (inc y)) (inc (plus i x y))  --;
plus_suc = \ i x y ->
  fix (\ i x -> Eq (Nat oo) (plus i x (inc y)) (inc (plus i x y)))
      (\ j f -> \
         { (zero _)  -> refl (Nat oo) (inc y)
         ; (suc _ x') -> cong (Nat oo) (Nat oo) inc (plus j x' (inc y)) (inc (plus j x' y)) (f x')
         })
      x

--; --- Another definition of addition

plus' : forall .i -> Nat i -> Nat oo -> Nat oo  --;
plus' = \ i x ->
  fix (\ i x -> Nat oo -> Nat oo)
      (\ _ f -> \
         { (zero _)  -> \ y -> y
         ; (suc _ x) -> \ y -> suc oo (f x y)
         })
      x

--; --- Predecessor

pred  : forall .i -> Nat i -> Nat i  --;
pred = \ i n ->
  fix (\ i _ -> Nat i)
      (\ i _ -> \{ (zero _) -> zero i ; (suc _ y) -> y })
      n

--; --- Subtraction

sub : forall .j -> Nat j -> forall .i -> Nat i -> Nat i  --;
sub = \ j y ->
  fix (\ _ _ -> forall .i -> Nat i -> Nat i)
      (\ _ f -> \
        { (zero _) -> \ i x -> x
        ; (suc _ y) -> \ i x -> f y i (pred i x)
        }) --- pred i (f y i x) })
      y

--; --- Lemma: x - x == 0

sub_diag : forall .i (x : Nat i) -> Eq (Nat oo) (sub i x i x) (zero oo)  --;
sub_diag = \ i x ->
  fix (\ i x -> Eq (Nat oo) (sub i x i x) (zero oo))
      (\ _ f -> \
        { (zero _) -> refl (Nat oo) (zero oo)
        ; (suc _ y) -> f y
        })
      x

--- Large eliminations

--; --- Varying arity

Fun : forall .i (n : Nat i) (A : Set) (B : Set) -> Set --;
Fun = \ i n A B ->
  fix (\ _ _ -> Set)
      (\ _ f -> \
         { (zero _) -> B
         ; (suc _ x) -> A -> f x
         })
      n

--; --- Type of n-ary Sum function

Sum : forall .i (n : Nat i) -> Set  --;
Sum = \ i n -> Nat oo -> Fun i n (Nat oo) (Nat oo)

--; --- n-ary summation function

sum : forall .i (n : Nat i) -> Sum i n --;
sum = \ _ n ->
  fix (\ i n -> Sum i n)
      (\ _ f -> \
        { (zero _) -> \ acc -> acc
        ; (suc _ x) -> \ acc -> \ k -> f x (plus oo k acc)
        })
      n

--; --- Testing sum

sum123 : Eq (Nat oo) (sum oo three (zero oo) one two three) six --;
sum123 = refl (Nat oo) six

max_stars_repo_name: andreasabel/S

max_issues_repo_name: andreasabel/Sit

max_forks_repo_name: andreasabel/Sit


text:
module PosNat where

open import Nats
open import Data.Product
open import Equality

data ℕ⁺ : Set where
  psuc : ℕ → ℕ⁺

_→ℕ : ℕ⁺ → ℕ
psuc  zero   →ℕ = suc  zero
psuc (suc x) →ℕ = suc (psuc x →ℕ)

_⟨_⟩→ℕ⁺ : (a : ℕ) → ∃ (λ x → a ≡ suc x) → ℕ⁺
.(suc x) ⟨ x , refl ⟩→ℕ⁺ = psuc x


text:
module _ where

module M where

  postulate
    [_] : Set → Set

Foo = [ M.undefined ]

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Common.Prelude

record Number (A : Set) : Set where
  field fromNat : Nat → A

record Negative (A : Set) : Set where
  field fromNeg : Nat → A

open Number {{...}} public
open Negative {{...}} public

{-# BUILTIN FROMNAT fromNat #-}
{-# BUILTIN FROMNEG fromNeg #-}

instance
  NumberNat : Number Nat
  NumberNat = record { fromNat = λ n → n }

data Int : Set where
  pos : Nat → Int
  neg : Nat → Int

instance
  NumberInt : Number Int
  NumberInt = record { fromNat = pos }

  NegativeInt : Negative Int
  NegativeInt = record { fromNeg = λ { zero → pos 0 ; (suc n) → neg n } }

minusFive : Int
minusFive = -5

open import Common.Equality

thm : -5 ≡ neg 4
thm = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
import      Lvl
open import Type

module Type.Functions.Inverse.Proofs {ℓₗ : Lvl.Level}{ℓₒ₁}{ℓₒ₂} {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} where

open import Function.Domains
open import Relator.Equals
open import Type.Functions {ℓₗ}
open import Type.Functions.Inverse {ℓₗ}
open import Type.Properties.Empty
open import Type.Properties.Singleton {ℓₒ₁}{ℓₒ₂}

postulate inv-bijective : ∀{f : X → Y} → ⦃ proof : Bijective(f) ⦄ → Bijective(inv f)
-- inv-bijective {f} ⦃ Bijective.intro(proof) ⦄

private
  _≡₁_ = _≡_ {ℓₗ Lvl.⊔ ℓₒ₁}

invᵣ-is-inverseᵣ : (f : X → Y) → ⦃ _ : Surjective(f) ⦄ → ∀{y} → (f(invᵣ f(y)) ≡ y)
invᵣ-is-inverseᵣ f ⦃ Surjective.intro(proof) ⦄ {y} with proof{y}
... | ◊.intro ⦃ Unapply.intro _ ⦃ out ⦄ ⦄ = out

inv-is-inverseᵣ : (f : X → Y) → ⦃ _ : Bijective(f) ⦄ → ∀{y} → (f(inv f(y)) ≡ y)
inv-is-inverseᵣ f ⦃ Bijective.intro(proof) ⦄ {y} with proof{y}
... | IsUnit.intro (Unapply.intro _ ⦃ out ⦄) _ = out

inv-is-inverseₗ : (f : X → Y) → ⦃ _ : Bijective(f) ⦄ → ∀{x} → (inv f(f(x)) ≡₁ x)
inv-is-inverseₗ f ⦃ Bijective.intro(proof) ⦄ {x} with proof{f(x)}
... | IsUnit.intro _ uniqueness with uniqueness {Unapply.intro x ⦃ [≡]-intro ⦄}
...   | [≡]-intro = [≡]-intro

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:
{-# OPTIONS --without-K #-}

open import Types
open import Functions
open import Paths
open import HLevel

module Equivalences where

hfiber : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) (y : B) → Set (max i j)
hfiber {A = A} f y = Σ A (λ x → f x ≡ y)

is-equiv : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) → Set (max i j)
is-equiv {B = B} f = (y : B) → is-contr (hfiber f y)

_~_ : ∀ {i j} {A : Set i} {B : Set j} (f g : A → B) → Set (max i j)
_~_ {A = A} f g = (x : A) → (f x ≡ g x)

is-iso : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) → Set (max i j)
is-iso {A = A} {B = B} f = Σ (B → A) (λ g → ((f ◯ g) ~ id B) × ((g ◯ f) ~ id A))

is-hae : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) → Set (max i j)
is-hae {A = A} {B = B} f =
  Σ (B → A)          (λ g →
  Σ ((g ◯ f) ~ id A) (λ η →
  Σ ((f ◯ g) ~ id B) (λ ε →
  (x : A) → ap f (η x) ≡ ε (f x))))

iso-is-hae : ∀ {i j} {A : Set i} {B : Set j} → (f : A → B) → is-iso f → is-hae f
iso-is-hae {A = A} {B = B} f (g , (ε , η)) = g , (η , (ε' , τ)) where
  ε' : (f ◯ g) ~ id B
  ε' b = ! (ε (f (g b))) ∘ ap f (η (g b)) ∘ ε b

  lem : (a : A) → η (g (f a)) ≡ ap (g ◯ f) (η a)
  lem a =
      η (g (f a))
    ≡⟨ ! (refl-right-unit (η (g (f a))) ) ⟩
      η (g (f a)) ∘ refl
    ≡⟨ ap (λ p → η (g (f a)) ∘ p) (! (opposite-right-inverse (η a))) ⟩
      η (g (f a)) ∘ (η a ∘ (! (η a)))
    ≡⟨ ! (concat-assoc (η (g (f a))) (η a) (! (η a))) ⟩
      (η (g (f a)) ∘ η a) ∘ (! (η a))
    ≡⟨ ap (λ p → p ∘ (! (η a)) ) (! (homotopy-naturality-toid (g ◯ f) η (η a))) ⟩
      (ap (g ◯ f) (η a) ∘ η a) ∘ (! (η a))
    ≡⟨ concat-assoc (ap (g ◯ f) (η a)) (η a) (! (η a)) ⟩
      ap (g ◯ f) (η a) ∘ (η a ∘ (! (η a)))
    ≡⟨ ap (λ p → ap (g ◯ f) (η a) ∘ p) (opposite-right-inverse (η a)) ⟩
      ap (g ◯ f) (η a) ∘ refl
    ≡⟨ refl-right-unit (ap (g ◯ f) (η a)) ⟩
      ap (g ◯ f) (η a)
    ∎

  lem₂ : (a : A) →  ε (f (g (f a))) ∘ ap f (η a) ≡ ap f (η (g (f a))) ∘ ε (f a)
  lem₂ a =
    ! (ap f (η (g (f a))) ∘ ε (f a)
    ≡⟨ ap (λ p → ap f p ∘ ε (f a)) (lem a) ⟩
      ap f (ap (g ◯ f) (η a)) ∘ ε (f a)
    ≡⟨ ap (λ p → p ∘ ε (f a)) (compose-ap f (g ◯ f) (η a)) ⟩
      ap (f ◯ (g ◯ f)) (η a) ∘ ε (f a)
    ≡⟨ homotopy-naturality (f ◯ (g ◯ f)) f (λ x → ε (f x)) (η a) ⟩
      ε (f (g (f a))) ∘ ap f (η a)
    ∎)

  τ : (a : A) → ap f (η a) ≡ ε' (f a)
  τ a =
      ap f (η a)
    ≡⟨ refl ⟩
      refl ∘ ap f (η a)
    ≡⟨ ap (λ p → p ∘ ap f (η a)) (! (opposite-left-inverse (ε (f (g (f a)))))) ⟩
      (! (ε (f (g (f a)))) ∘ (ε (f (g (f a))))) ∘ ap f (η a)
    ≡⟨ concat-assoc (! (ε (f (g (f a))))) (ε (f (g (f a)))) (ap f (η a)) ⟩
      ! (ε (f (g (f a)))) ∘ ((ε (f (g (f a)))) ∘ ap f (η a))
    ≡⟨ ap (λ p → ! (ε (f (g (f a)))) ∘ p) (lem₂ a) ⟩
       ! (ε (f (g (f a)))) ∘ (ap f (η (g (f a))) ∘ ε (f a))
    ∎

hae-is-eq : ∀ {i j} {A : Set i} {B : Set j} → (f : A → B) → is-hae f → is-equiv f
hae-is-eq f (g , (η , (ε , τ))) y = (g y , ε y) , contr where
  contr : (xp : hfiber f y) → xp ≡ g y , ε y
  contr (x , p) = total-Σ-eq ( ((! (η x)) ∘ ap g p) , t) where
    t : transport (λ z → f z ≡ y) (! (η x) ∘ ap g p) p ≡ ε y
    t =
        transport (λ z → f z ≡ y) (! (η x) ∘ ap g p) p
      ≡⟨ trans-app≡cst f y (! (η x) ∘ ap g p) p ⟩
        ! (ap f (! (η x) ∘ ap g p)) ∘ p
      ≡⟨ ap (λ q → q ∘ p) (opposite-ap f (! (η x) ∘ ap g p)) ⟩
        ap f (! (! (η x) ∘ ap g p)) ∘ p
      ≡⟨ ap (λ q → ap f q ∘ p) (opposite-concat (! (η x)) (ap g p)) ⟩
        ap f (! (ap g p) ∘ ! (! (η x))) ∘ p
      ≡⟨ ap (λ q → ap f (! (ap g p) ∘ q) ∘ p) (opposite-opposite (η x)) ⟩
        ap f (! (ap g p) ∘ η x) ∘ p
      ≡⟨ ap (λ q → q ∘ p) (ap-concat f (! (ap g p)) (η x)) ⟩
        (ap f (! (ap g p)) ∘ ap f (η x)) ∘ p
      ≡⟨ ap (λ q → (q ∘ ap f (η x)) ∘ p) (ap-opposite f (ap g p)) ⟩
        (! (ap f (ap g p)) ∘ ap f (η x)) ∘ p
      ≡⟨ ap (λ q → (! q ∘ ap f (η x)) ∘ p) (compose-ap f g p) ⟩
        (! (ap (f ◯ g) p) ∘ ap f (η x)) ∘ p
      ≡⟨ ap (λ q → ((! (ap (f ◯ g) p)) ∘ q) ∘ p ) (τ x) ⟩
        (! (ap (f ◯ g) p) ∘ ε (f x)) ∘ p
      ≡⟨ ap (λ q → (q ∘ ε (f x)) ∘ p) (opposite-ap (f ◯ g) p) ⟩
        (ap (f ◯ g) (! p) ∘ ε (f x)) ∘ p
      ≡⟨ ap (λ q → q ∘ p) (homotopy-naturality-toid (f ◯ g) ε (! p)) ⟩
        (ε y ∘ ! p) ∘ p
      ≡⟨ concat-assoc (ε y) (! p) p ⟩
        ε y ∘ ((! p) ∘ p)
      ≡⟨ ap (λ q → ε y ∘ q) (opposite-left-inverse p) ⟩
        ε y ∘ refl
      ≡⟨ refl-right-unit (ε y) ⟩
        ε y
      ∎

_≃_ : ∀ {i j} (A : Set i) (B : Set j) → Set (max i j)  -- \simeq
A ≃ B = Σ (A → B) is-equiv

id-is-equiv : ∀ {i} (A : Set i) → is-equiv (id A)
id-is-equiv A = pathto-is-contr

id-equiv : ∀ {i} (A : Set i) → A ≃ A
id-equiv A = (id A , id-is-equiv A)

path-to-eq : ∀ {i} {A B : Set i} → (A ≡ B → A ≃ B)
path-to-eq refl = id-equiv _

module _ {i} {j} {A : Set i} {B : Set j} where

  -- Notation for the application of an equivalence to an argument
  _☆_ : (f : A ≃ B) (x : A) → B
  f ☆ x = (π₁ f) x

  inverse : (f : A ≃ B) → B → A
  inverse (f , e) = λ y → π₁ (π₁ (e y))

  abstract
    inverse-right-inverse : (f : A ≃ B) (y : B) → f ☆ (inverse f y) ≡ y
    inverse-right-inverse (f , e) y = π₂ (π₁ (e y))

    inverse-left-inverse : (f : A ≃ B) (x : A) → inverse f (f ☆ x) ≡ x
    inverse-left-inverse (f , e) x =
      ! (base-path (π₂ (e (f x)) (x , refl)))

    hfiber-triangle : (f : A → B) (z : B) {x y : hfiber f z} (p : x ≡ y)
      → ap f (base-path p) ∘ π₂ y ≡ π₂ x
    hfiber-triangle f z {x} {.x} refl = refl

    inverse-triangle : (f : A ≃ B) (x : A) →
      inverse-right-inverse f (f ☆ x) ≡ ap (π₁ f) (inverse-left-inverse f x)
    inverse-triangle (f , e) x = move1!-left-on-left _ _
      (hfiber-triangle f _ (π₂ (e (f x)) (x , refl)))
       ∘ opposite-ap f _

  iso-is-eq' : (f : A → B) → is-iso f → is-equiv f
  iso-is-eq' f iso = hae-is-eq f (iso-is-hae f iso)

  iso-is-eq : (f : A → B) → (g : B → A) → (∀ y → f (g y) ≡ y) → (∀ x → g (f x) ≡ x) → is-equiv f
  iso-is-eq f g η ε = iso-is-eq' _ (g , (η , ε))

  inverse-iso-is-eq : (f : A → B) → (iso : is-iso f) → inverse (f , iso-is-eq' f iso) ≡ π₁ iso
  inverse-iso-is-eq f iso = refl

-- The inverse of an equivalence is an equivalence
inverse-is-equiv : ∀ {i} {j} {A : Set i} {B : Set j} (f : A ≃ B)
  → is-equiv (inverse f)
inverse-is-equiv f =
  iso-is-eq (inverse f) (π₁ f) (inverse-left-inverse f) (inverse-right-inverse f)

_⁻¹ : ∀ {i} {j} {A : Set i} {B : Set j} (f : A ≃ B) → B ≃ A  -- \^-\^1
_⁻¹ f = (inverse f , inverse-is-equiv f)

-- Equivalences are injective
equiv-is-inj : ∀ {i} {j} {A : Set i} {B : Set j} (f : A ≃ B) (x y : A)
  → (f ☆ x ≡ f ☆ y → x ≡ y)
equiv-is-inj f x y p = ! (inverse-left-inverse f x)
                       ∘ (ap (inverse f) p ∘ inverse-left-inverse f y)

-- Any contractible type is equivalent to the unit type
contr-equiv-unit : ∀ {i j} {A : Set i} → (is-contr A → A ≃ unit {j})
contr-equiv-unit e = ((λ _ → tt) , iso-is-eq _ (λ _ → π₁ e) (λ _ → refl) (λ x → ! (π₂ e x)))

-- The composite of two equivalences is an equivalence
compose-is-equiv : ∀ {i j k} {A : Set i} {B : Set j} {C : Set k}
  (f : A ≃ B) (g : B ≃ C) → is-equiv (π₁ g ◯ π₁ f)
compose-is-equiv f g =
  iso-is-eq _
    (inverse f ◯ inverse g)
    (λ y → ap (π₁ g) (inverse-right-inverse f (inverse g y)) ∘ inverse-right-inverse g y)
    (λ x → ap (inverse f) (inverse-left-inverse g (π₁ f x)) ∘ inverse-left-inverse f x)

equiv-compose : ∀ {i j k} {A : Set i} {B : Set j} {C : Set k}
  → (A ≃ B → B ≃ C → A ≃ C)
equiv-compose f g = ((π₁ g ◯ π₁ f) , compose-is-equiv f g)

-- An equivalence induces an equivalence on the path spaces
-- The proofs here can probably be simplified
module _ {i j} {A : Set i} {B : Set j} (f : A ≃ B) (x y : A) where

  private
    ap-is-inj : (p : f ☆ x ≡ f ☆ y) → x ≡ y
    ap-is-inj p = equiv-is-inj f x y p

    abstract
      left-inverse : (p : x ≡ y) → ap-is-inj (ap (π₁ f) p) ≡ p
      left-inverse p =
        move!-right-on-left (inverse-left-inverse f x) _ p
          (move-right-on-right (ap (inverse f) (ap (π₁ f) p)) _ _
           (compose-ap (inverse f) (π₁ f) p
           ∘ move!-left-on-right (ap (inverse f ◯ π₁ f) p)
               (inverse-left-inverse f x ∘ p)
               (inverse-left-inverse f y)
               (homotopy-naturality-toid (inverse f ◯ π₁ f)
                 (inverse-left-inverse f) p)))

      right-inverse : (p : f ☆ x ≡ f ☆ y) → ap (π₁ f) (ap-is-inj p) ≡ p
      right-inverse p =
        ap-concat (π₁ f) (! (inverse-left-inverse f x)) _
        ∘ (ap (λ u → u ∘ ap (π₁ f) (ap (inverse f) p
                  ∘ inverse-left-inverse f y))
               (ap-opposite (π₁ f) (inverse-left-inverse f x))
          ∘ move!-right-on-left (ap (π₁ f) (inverse-left-inverse f x)) _ p
            (ap-concat (π₁ f) (ap (inverse f) p) (inverse-left-inverse f y)
            ∘ (ap (λ u → u ∘ ap (π₁ f) (inverse-left-inverse f y))
                   (compose-ap (π₁ f) (inverse f) p)
            ∘ (whisker-left (ap (π₁ f ◯ inverse f) p)
                            (! (inverse-triangle f y))
            ∘ (homotopy-naturality-toid (π₁ f ◯ inverse f)
                                        (inverse-right-inverse f)
                                        p
            ∘ whisker-right p (inverse-triangle f x))))))

  equiv-ap : (x ≡ y) ≃ (f ☆ x ≡ f ☆ y)
  equiv-ap = (ap (π₁ f) , iso-is-eq _ ap-is-inj right-inverse left-inverse)

abstract
  total-Σ-eq-is-equiv : ∀ {i j} {A : Set i} {P : A → Set j} {x y : Σ A P}
    → is-equiv (total-Σ-eq {xu = x} {yv = y})
  total-Σ-eq-is-equiv {P = P} =
    iso-is-eq _
      (λ totp → base-path totp , fiber-path totp)
      Σ-eq-base-path-fiber-path
      (λ p → Σ-eq (base-path-Σ-eq (π₁ p) (π₂ p)) (fiber-path-Σ-eq {P = P} (π₁ p) (π₂ p)))

total-Σ-eq-equiv : ∀ {i j} {A : Set i} {P : A → Set j} {x y : Σ A P}
  → (Σ (π₁ x ≡ π₁ y) (λ p → transport P p (π₂ x) ≡ (π₂ y))) ≃ (x ≡ y)
total-Σ-eq-equiv = (total-Σ-eq , total-Σ-eq-is-equiv)


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

open import Categories.Category

module Categories.Functor.Construction.SubCategory {o ℓ e} (C : Category o ℓ e) where

open import Categories.Category.SubCategory C

open Category C
open Equiv

open import Level
open import Function.Base using () renaming (id to id→)
open import Data.Product

open import Categories.Functor using (Functor)

private
  variable
    ℓ′ i : Level
    I : Set i
    U : I → Obj

Sub : ∀ (sub : SubCat {i} {ℓ′} I) → Functor (SubCategory sub) C
Sub (record {U = U}) = record
  { F₀ = U
  ; F₁ = proj₁
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = id→
  }

FullSub : Functor (FullSubCategory U) C
FullSub {U = U} = record
  { F₀ = U
  ; F₁ = id→
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = id→
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Andreas, 2014-10-05

{-# OPTIONS --cubical-compatible --sized-types #-}

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

open import Agda.Builtin.Size

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {↑ size}
  suc  : {size : Size} -> Nat {size} -> Nat {↑ size}

-- subtraction is non size increasing
sub : {size : Size} -> Nat {size} -> Nat {∞} -> Nat {size}
sub zero    n       = zero
sub (suc m) zero    = suc m
sub (suc m) (suc n) = sub m n

-- div' m n  computes  ceiling(m/(n+1))
div' : {size : Size} -> Nat {size} -> Nat -> Nat {size}
div' zero    n = zero
div' (suc m) n = suc (div' (sub m n) n)

-- should termination check even --cubical-compatible

-- -}


text:
module FlatDomInequality-1 where

postulate
  A : Set

g : A → A
g x = x

h : (@♭ x : A) → A
h = g

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Object.BinaryProducts.Abstract where

open import Categories.Support.PropositionalEquality
open import Categories.Category
open import Categories.Object.BinaryProducts
open import Categories.Morphisms

module AbstractBinaryProducts {o ℓ e} (C : Category o ℓ e) (BP : BinaryProducts C) where
  private module P = BinaryProducts C BP
  open P public using (_×_; π₁; π₂)
  private open Category C
  private import Categories.Object.Product as Product

  mutual
    first : ∀ {A B C} → (A ⇒ B) → ((A × C) ⇒ (B × C))
    first f = f ⁂ id

    second : ∀ {A C D} → (C ⇒ D) → ((A × C) ⇒ (A × D))
    second g = id ⁂ g

    abstract
      infix 10 _⁂_

      _⁂_ : ∀ {A B C D} → (A ⇒ B) → (C ⇒ D) → ((A × C) ⇒ (B × D))
      _⁂_ = P._⁂_

      ⟨_,_⟩ : ∀ {A B Q} → (Q ⇒ A) → (Q ⇒ B) → (Q ⇒ (A × B))
      ⟨_,_⟩ = P.⟨_,_⟩

      ⁂-convert : ∀ {A B C D} (f : A ⇒ B) (g : C ⇒ D) → f ⁂ g ≣ ⟨ f ∘ π₁ , g ∘ π₂ ⟩
      ⁂-convert f g = ≣-refl

      assocˡ : ∀ {A B C} → (((A × B) × C) ⇒ (A × (B × C)))
      assocˡ = P.assocˡ

      assocˡ-convert : ∀ {A B C} → assocˡ {A} {B} {C} ≣ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
      assocˡ-convert = ≣-refl

      assocʳ : ∀ {A B C} → ((A × (B × C)) ⇒ ((A × B) × C))
      assocʳ = P.assocʳ

      assocʳ-convert : ∀ {A B C} → assocʳ {A} {B} {C} ≣ ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩
      assocʳ-convert = ≣-refl

      .assoc-iso : ∀ {A B C′} → Iso C (assocʳ {A} {B} {C′}) assocˡ
      assoc-iso = _≅_.iso C P.×-assoc

      .⁂∘⁂ : ∀ {A B C D E F} → {f : B ⇒ C} → {f′ : A ⇒ B} {g : E ⇒ F} {g′ : D ⇒ E} → (f ⁂ g) ∘ (f′ ⁂ g′) ≡ (f ∘ f′) ⁂ (g ∘ g′)
      ⁂∘⁂ = P.⁂∘⁂

      .⁂∘⟨⟩ : ∀ {A B C D E} → {f : B ⇒ C} {f′ : A ⇒ B} {g : D ⇒ E} {g′ : A ⇒ D} → (f ⁂ g) ∘ ⟨ f′ , g′ ⟩ ≡ ⟨ f ∘ f′ , g ∘ g′ ⟩
      ⁂∘⟨⟩ = P.⁂∘⟨⟩

      .π₁∘⁂ : ∀ {A B C D} → {f : A ⇒ B} → {g : C ⇒ D} → π₁ ∘ (f ⁂ g) ≡ f ∘ π₁
      π₁∘⁂ = P.π₁∘⁂

      .π₂∘⁂ : ∀ {A B C D} → {f : A ⇒ B} → {g : C ⇒ D} → π₂ ∘ (f ⁂ g) ≡ g ∘ π₂
      π₂∘⁂ = P.π₂∘⁂

      .⟨⟩-cong₂ : ∀ {A B C} → {f f′ : C ⇒ A} {g g′ : C ⇒ B} → f ≡ f′ → g ≡ g′ → ⟨ f , g ⟩ ≡ ⟨ f′ , g′ ⟩
      ⟨⟩-cong₂ = P.⟨⟩-cong₂

      .⟨⟩∘ : ∀ {A B C D} {f : A ⇒ B} {g : A ⇒ C} {q : D ⇒ A} → ⟨ f , g ⟩ ∘ q ≡ ⟨ f ∘ q , g ∘ q ⟩
      ⟨⟩∘ = P.⟨⟩∘

      .first∘⟨⟩ : ∀ {A B C D} → {f : B ⇒ C} {f′ : A ⇒ B} {g′ : A ⇒ D} → first f ∘ ⟨ f′ , g′ ⟩ ≡ ⟨ f ∘ f′ , g′ ⟩
      first∘⟨⟩ = P.first∘⟨⟩

      .second∘⟨⟩ : ∀ {A B D E} → {f′ : A ⇒ B} {g : D ⇒ E} {g′ : A ⇒ D} → second g ∘ ⟨ f′ , g′ ⟩ ≡ ⟨ f′ , g ∘ g′ ⟩
      second∘⟨⟩ = P.second∘⟨⟩

      .η : ∀ {A B} → ⟨ π₁ , π₂ ⟩ ≡ id {A × B}
      η = P.η

      .commute₁ : ∀ {A B C} {f : C ⇒ A} {g : C ⇒ B} → π₁ ∘ ⟨ f , g ⟩ ≡ f
      commute₁ = P.commute₁

      .commute₂ : ∀ {A B C} {f : C ⇒ A} {g : C ⇒ B} → π₂ ∘ ⟨ f , g ⟩ ≡ g
      commute₂ = P.commute₂

      .universal : ∀ {A B C} {f : C ⇒ A} {g : C ⇒ B} {i : C ⇒ (A × B)}
                   → π₁ ∘ i ≡ f → π₂ ∘ i ≡ g → ⟨ f , g ⟩ ≡ i
      universal = P.universal

  module HomReasoningP {A B : Obj} where
    open HomReasoning {A} {B} public

    -- sort of a hack, if you specify the codomain for your top-level
    --   reasoning you will NOT get what you want from the below
    infix 3 ⟨_⟩,⟨_⟩
    .⟨_⟩,⟨_⟩ : ∀ {C} → {f f′ : A ⇒ B} {g g′ : A ⇒ C} → f ≡ f′ → g ≡ g′ → ⟨ f , g ⟩ ≡ ⟨ f′ , g′ ⟩
    ⟨_⟩,⟨_⟩ x y = ⟨⟩-cong₂ x y

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------------
-- Inequalities on partial natural numbers
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Inequalities where

open import LTC-PCF.Base

infix 4 _<_ _≮_ _>_ _≯_ _≤_ _≰_ _≥_ _≱_

------------------------------------------------------------------------------
-- The function terms.

lth : D → D
lth lt = lam (λ m → lam (λ n →
           if (iszero₁ n)
             then false
             else (if (iszero₁ m) then true else (lt · pred₁ m · pred₁ n))))
lt : D → D → D
lt m n = fix lth · m · n

le : D → D → D
le m n = lt m (succ₁ n)

gt : D → D → D
gt m n = lt n m

ge : D → D → D
ge m n = le n m

------------------------------------------------------------------------
-- The relations.

_<_ : D → D → Set
m < n = lt m n ≡ true

_≮_ : D → D → Set
m ≮ n = lt m n ≡ false

_>_ : D → D → Set
m > n = gt m n ≡ true

_≯_ : D → D → Set
m ≯ n = gt m n ≡ false

_≤_  : D → D → Set
m ≤ n = le m n ≡ true

_≰_  : D → D → Set
m ≰ n = le m n ≡ false

_≥_ : D → D → Set
m ≥ n = ge m n ≡ true

_≱_ : D → D → Set
m ≱ n = ge m n ≡ false

------------------------------------------------------------------------------
-- The lexicographical order.
Lexi : D → D → D → D → Set
Lexi m n m' n' = m < m' ∨ m ≡ m' ∧ n < n'


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions for types of functions.
------------------------------------------------------------------------

-- The contents of this file should usually be accessed from `Function`.

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

open import Relation.Binary

module Function.Definitions
  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
  (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
  (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
  where

open import Data.Product using (∃; _×_)
import Function.Definitions.Core1 as Core₁
import Function.Definitions.Core2 as Core₂
open import Level using (_⊔_)

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

Congruent : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y

Injective : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y

open Core₂ _≈₂_ public
  using (Surjective)

Bijective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
Bijective f = Injective f × Surjective f

open Core₂ _≈₂_ public
  using (Inverseˡ)

open Core₁ _≈₁_ public
  using (Inverseʳ)

Inverseᵇ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g


text:
-- Andreas, 2015-07-16, issue reported by Nisse

postulate
  A   : Set₁
  P   : A → Set₁
  T   : Set₁ → Set₁
  Σ   : (A : Set₁) → (A → Set₁) → Set₁
  T-Σ : {A : Set₁} {B : A → Set₁} → (∀ x → T (B x)) → T (Σ A B)

t : T (Σ Set λ _ → Σ (A → A) λ f → Σ (∀ x₁ → P (f x₁)) λ _ → Set)
t = T-Σ λ _ → T-Σ λ _ → T-Σ {!!}

-- WAS:
-- Goal type and context:
--
--   Goal: (x : (x₁ : A) → P (x₁ x₁)) → T Set
--   ————————————————————————————————————————————————————————————
--   x₁ : A → A
--   x  : Set
--
-- Note the application "x₁ x₁".

-- EXPECTED:
-- Goal: (x : (x₁ : A) → P (.x₁ x₁)) → T Set
-- ————————————————————————————————————————————————————————————
-- .x₁ : A → A
-- .x  : Set

id : (x : A) → A
-- id _ = {!!}      -- Context displays .x
id = λ _ → {!!}  -- Context should display .x


text:
module Successor where

open import OscarPrelude

record Successor {ℓᴬ} (A : Set ℓᴬ) {ℓᴮ} (B : Set ℓᴮ) : Set (ℓᴬ ⊔ ℓᴮ)
 where
  field
    ⊹ : A → B

open Successor ⦃ … ⦄ public

instance SuccessorNat : Successor Nat Nat
Successor.⊹ SuccessorNat = suc

instance SuccessorLevel : Successor Level Level
Successor.⊹ SuccessorLevel = lsuc


text:
open import Nat
open import Prelude
open import core
open import judgemental-erase
open import aasubsume-min

module determinism where
  -- the same action applied to the same type makes the same type
  actdet-type : {t t' t'' : τ̂} {α : action} →
            (t + α +> t') →
            (t + α +> t'') →
            (t' == t'')
  actdet-type TMArrChild1 TMArrChild1 = refl
  actdet-type TMArrChild2 TMArrChild2 = refl
  actdet-type TMArrParent1 TMArrParent1 = refl
  actdet-type TMArrParent1 (TMArrZip1 ())
  actdet-type TMArrParent2 TMArrParent2 = refl
  actdet-type TMArrParent2 (TMArrZip2 ())
  actdet-type TMDel TMDel = refl
  actdet-type TMConArrow TMConArrow = refl
  actdet-type TMConNum TMConNum = refl
  actdet-type (TMArrZip1 ()) TMArrParent1
  actdet-type (TMArrZip1 p1) (TMArrZip1 p2) with actdet-type p1 p2
  ... | refl = refl
  actdet-type (TMArrZip2 ()) TMArrParent2
  actdet-type (TMArrZip2 p1) (TMArrZip2 p2) with actdet-type p1 p2
  ... | refl = refl

  -- all expressions only move to one other expression
  movedet : {e e' e'' : ê} {δ : direction} →
            (e + move δ +>e e') →
            (e + move δ +>e e'') →
            e' == e''
  movedet EMAscChild1 EMAscChild1 = refl
  movedet EMAscChild2 EMAscChild2 = refl
  movedet EMAscParent1 EMAscParent1 = refl
  movedet EMAscParent2 EMAscParent2 = refl
  movedet EMLamChild1 EMLamChild1 = refl
  movedet EMLamParent EMLamParent = refl
  movedet EMPlusChild1 EMPlusChild1 = refl
  movedet EMPlusChild2 EMPlusChild2 = refl
  movedet EMPlusParent1 EMPlusParent1 = refl
  movedet EMPlusParent2 EMPlusParent2 = refl
  movedet EMApChild1 EMApChild1 = refl
  movedet EMApChild2 EMApChild2 = refl
  movedet EMApParent1 EMApParent1 = refl
  movedet EMApParent2 EMApParent2 = refl
  movedet EMNEHoleChild1 EMNEHoleChild1 = refl
  movedet EMNEHoleParent EMNEHoleParent = refl

  -- non-movement lemmas; theses show up pervasively throughout and save a
  -- lot of pattern matching.
  lem-nomove-part : ∀ {t t'} → ▹ t ◃ + move parent +> t' → ⊥
  lem-nomove-part ()

  lem-nomove-pars : ∀{Γ e t e' t'} → Γ ⊢ ▹ e ◃ => t ~ move parent ~> e' => t' → ⊥
  lem-nomove-pars (SAMove ())

  lem-nomove-para : ∀{Γ e t e'} → Γ ⊢ ▹ e ◃ ~ move parent ~> e' ⇐ t → ⊥
  lem-nomove-para (AASubsume e x x₁ x₂) = lem-nomove-pars x₁
  lem-nomove-para (AAMove ())

  -- if a move action on a synthetic action makes a new form, it's unique
  synthmovedet : {Γ : ·ctx} {e e' e'' : ê} {t' t'' : τ̇} {δ : direction} →
         (Γ ⊢ e => t' ~ move δ ~> e'' => t'') →
         (e + move δ +>e e') →
         e'' == e'
  synthmovedet (SAMove m1) m2 = movedet m1 m2
  -- all these cases lead to absurdities based on movement
  synthmovedet (SAZipAsc1 x) EMAscParent1         = abort (lem-nomove-para x)
  synthmovedet (SAZipAsc2 x _ _ _) EMAscParent2   = abort (lem-nomove-part x)
  synthmovedet (SAZipApArr _ _ _ x _) EMApParent1 = abort (lem-nomove-pars x)
  synthmovedet (SAZipApAna _ _ x) EMApParent2     = abort (lem-nomove-para x)
  synthmovedet (SAZipPlus1 x) EMPlusParent1       = abort (lem-nomove-para x)
  synthmovedet (SAZipPlus2 x) EMPlusParent2       = abort (lem-nomove-para x)
  synthmovedet (SAZipHole _ _ x) EMNEHoleParent   = abort (lem-nomove-pars x)

  anamovedet : {Γ : ·ctx} {e e' e'' : ê} {t : τ̇} {δ : direction} →
         (Γ ⊢ e ~ move δ ~> e'' ⇐ t) →
         (e + move δ +>e e') →
         e'' == e'
  anamovedet (AASubsume x₂ x x₃ x₁) m = synthmovedet x₃ m
  anamovedet (AAMove x) m = movedet x m
  anamovedet (AAZipLam x₁ x₂ d) EMLamParent = abort (lem-nomove-para d)

  mutual
    -- an action on an expression in a synthetic position produces one
    -- resultant expression and type.
    actdet-synth : {Γ : ·ctx} {e e' e'' : ê} {e◆ : ė} {t t' t'' : τ̇} {α : action} →
              (E : erase-e e e◆) →
              (Γ ⊢ e◆ => t) →
              (d1 : Γ ⊢ e => t ~ α ~> e'  => t') →
              (d2 : Γ ⊢ e => t ~ α ~> e'' => t'') →
              {p1 : aasubmin-synth d1} →
              {p2 : aasubmin-synth d2} →
              (e' == e'' × t' == t'')
    actdet-synth EETop (SAsc x) (SAMove x₁) (SAMove x₂) = movedet x₁ x₂ , refl
    actdet-synth EETop (SAsc x) SADel SADel = refl , refl
    actdet-synth EETop (SAsc x) SAConAsc SAConAsc = refl , refl
    actdet-synth EETop (SAsc x) (SAConPlus1 x₁) (SAConPlus1 x₂) = refl , refl
    actdet-synth EETop (SAsc x) (SAConPlus1 x₁) (SAConPlus2 x₂) = abort (x₂ x₁)
    actdet-synth EETop (SAsc x) (SAConPlus2 x₁) (SAConPlus1 x₂) = abort (x₁ x₂)
    actdet-synth EETop (SAsc x) (SAConPlus2 x₁) (SAConPlus2 x₂) = refl , refl
    actdet-synth EETop (SAsc x) (SAConApArr x₁) (SAConApArr x₂) with matcharrunicity x₁ x₂
    ... | refl = refl , refl
    actdet-synth EETop (SAsc x) (SAConApArr x₁) (SAConApOtw x₂) = abort (x₂ (matchconsist x₁))
    actdet-synth EETop (SAsc x) (SAConApOtw x₁) (SAConApArr x₂) = abort (x₁ (matchconsist x₂))
    actdet-synth EETop (SAsc x) (SAConApOtw x₁) (SAConApOtw x₂) = refl , refl
    actdet-synth EETop (SAsc x) SAConNEHole SAConNEHole = refl , refl

    actdet-synth (EEAscL E) (SAsc x) (SAMove x₁) (SAMove x₂) = movedet x₁ x₂ , refl
    actdet-synth (EEAscL E) (SAsc x) (SAMove EMAscParent1) (SAZipAsc1 x₂) = abort (lem-nomove-para x₂)
    actdet-synth (EEAscL E) (SAsc x) (SAZipAsc1 x₁) (SAMove EMAscParent1) = abort (lem-nomove-para x₁)
    actdet-synth (EEAscL E) (SAsc x) (SAZipAsc1 x₁) (SAZipAsc1 x₂) {p1} {p2}
     with actdet-ana E x x₁ x₂ {p1} {p2}
    ... | refl = refl , refl

    actdet-synth (EEAscR x) (SAsc x₁) (SAMove x₂) (SAMove x₃) = movedet x₂ x₃ , refl
    actdet-synth (EEAscR x) (SAsc x₁) (SAMove EMAscParent2) (SAZipAsc2 a _ _ _) = abort (lem-nomove-part a)
    actdet-synth (EEAscR x) (SAsc x₁) (SAZipAsc2 a _ _ _) (SAMove EMAscParent2) = abort (lem-nomove-part a)
    actdet-synth (EEAscR x) (SAsc x₂) (SAZipAsc2 a e1 _ _) (SAZipAsc2 b e2 _ _)
      with actdet-type a b
    ... | refl = refl , eraset-det e1 e2

    actdet-synth EETop (SVar x) (SAMove x₁) (SAMove x₂) = movedet x₁ x₂ , refl
    actdet-synth EETop (SVar x) SADel SADel = refl , refl
    actdet-synth EETop (SVar x) SAConAsc SAConAsc = refl , refl
    actdet-synth EETop (SVar x) (SAConPlus1 x₁) (SAConPlus1 x₂) = refl , refl
    actdet-synth EETop (SVar x) (SAConPlus1 x₁) (SAConPlus2 x₂) = abort (x₂ x₁)
    actdet-synth EETop (SVar x) (SAConPlus2 x₁) (SAConPlus1 x₂) = abort (x₁ x₂)
    actdet-synth EETop (SVar x) (SAConPlus2 x₁) (SAConPlus2 x₂) = refl , refl
    actdet-synth EETop (SVar x) (SAConApArr x₁) (SAConApArr x₂) with matcharrunicity x₁ x₂
    ... | refl = refl , refl
    actdet-synth EETop (SVar x) (SAConApArr x₁) (SAConApOtw x₂) = abort (x₂ (matchconsist x₁))
    actdet-synth EETop (SVar x) (SAConApOtw x₁) (SAConApArr x₂) = abort (x₁ (matchconsist x₂))
    actdet-synth EETop (SVar x) (SAConApOtw x₁) (SAConApOtw x₂) = refl , refl
    actdet-synth EETop (SVar x) SAConNEHole SAConNEHole = refl , refl

    actdet-synth EETop (SAp m wt x) (SAMove x₁) (SAMove x₂) = movedet x₁ x₂ , refl
    actdet-synth EETop (SAp m wt x) SADel SADel = refl , refl
    actdet-synth EETop (SAp m wt x) SAConAsc SAConAsc = refl , refl
    actdet-synth EETop (SAp m wt x) (SAConPlus1 x₁) (SAConPlus1 x₂) = refl , refl
    actdet-synth EETop (SAp m wt x) (SAConPlus1 x₁) (SAConPlus2 x₂) = abort (x₂ x₁)
    actdet-synth EETop (SAp m wt x) (SAConPlus2 x₁) (SAConPlus1 x₂) = abort (x₁ x₂)
    actdet-synth EETop (SAp m wt x) (SAConPlus2 x₁) (SAConPlus2 x₂) = refl , refl
    actdet-synth EETop (SAp m wt x) (SAConApArr x₁) (SAConApArr x₂) with matcharrunicity x₁ x₂
    ... | refl = refl , refl
    actdet-synth EETop (SAp m wt x) (SAConApArr x₁) (SAConApOtw x₂) = abort (x₂ (matchconsist x₁))
    actdet-synth EETop (SAp m wt x) (SAConApOtw x₁) (SAConApArr x₂) = abort (x₁ (matchconsist x₂))
    actdet-synth EETop (SAp m wt x) (SAConApOtw x₁) (SAConApOtw x₂) = refl , refl
    actdet-synth EETop (SAp m wt x) SAConNEHole SAConNEHole = refl , refl

    actdet-synth (EEApL E) (SAp m wt x) (SAMove x₁) (SAMove x₂) = movedet x₁ x₂ , refl
    actdet-synth (EEApL E) (SAp m wt x) (SAMove EMApParent1) (SAZipApArr _ x₂ x₃ d2 x₄) = abort (lem-nomove-pars d2)
    actdet-synth (EEApL E) (SAp m wt x) (SAZipApArr _ x₁ x₂ d1 x₃) (SAMove EMApParent1) = abort (lem-nomove-pars d1)
    actdet-synth (EEApL E) (SAp m wt x) (SAZipApArr a x₁ x₂ d1 x₃) (SAZipApArr b x₄ x₅ d2 x₆) {p1} {p2}
      with erasee-det x₁ x₄
    ... | refl with synthunicity x₂ x₅
    ... | refl with erasee-det E x₁
    ... | refl with actdet-synth E x₅ d1 d2 {p1} {p2}
    ... | refl , refl with matcharrunicity a b
    ... | refl = refl , refl

    actdet-synth (EEApR E) (SAp m wt x) (SAMove x₁) (SAMove x₂) = movedet x₁ x₂ , refl
    actdet-synth (EEApR E) (SAp m wt x) (SAMove EMApParent2) (SAZipApAna x₂ x₃ x₄) = abort (lem-nomove-para x₄)
    actdet-synth (EEApR E) (SAp m wt x) (SAZipApAna x₁ x₂ x₃) (SAMove EMApParent2) = abort (lem-nomove-para x₃)
    actdet-synth (EEApR E) (SAp m wt x) (SAZipApAna x₁ x₂ d1) (SAZipApAna x₄ x₅ d2)  {p1} {p2}
     with synthunicity m x₂
    ... | refl with matcharrunicity x₁ wt
    ... | refl with synthunicity m x₅
    ... | refl with matcharrunicity x₄ wt
    ... | refl with actdet-ana E x d1 d2  {p1} {p2}
    ... | refl = refl , refl

    actdet-synth EETop SNum (SAMove x) (SAMove x₁) = movedet x x₁ , refl
    actdet-synth EETop SNum SADel SADel = refl , refl
    actdet-synth EETop SNum SAConAsc SAConAsc = refl , refl
    actdet-synth EETop SNum (SAConPlus1 x) (SAConPlus1 x₁) = refl , refl
    actdet-synth EETop SNum (SAConPlus1 x) (SAConPlus2 x₁) = abort (x₁ x)
    actdet-synth EETop SNum (SAConPlus2 x) (SAConPlus1 x₁) = abort (x x₁)
    actdet-synth EETop SNum (SAConPlus2 x) (SAConPlus2 x₁) = refl , refl
    actdet-synth EETop SNum (SAConApArr x) (SAConApArr x₁) with matcharrunicity x x₁
    ... | refl = refl , refl
    actdet-synth EETop SNum (SAConApArr x) (SAConApOtw x₁) = abort (x₁ (matchconsist x))
    actdet-synth EETop SNum (SAConApOtw x) (SAConApArr x₁) = abort (x (matchconsist x₁))
    actdet-synth EETop SNum (SAConApOtw x) (SAConApOtw x₁) = refl , refl
    actdet-synth EETop SNum SAConNEHole SAConNEHole = refl , refl

    actdet-synth EETop (SPlus x x₁) (SAMove x₂) (SAMove x₃) = movedet x₂ x₃ , refl
    actdet-synth EETop (SPlus x x₁) SADel SADel = refl , refl
    actdet-synth EETop (SPlus x x₁) SAConAsc SAConAsc = refl , refl
    actdet-synth EETop (SPlus x x₁) (SAConPlus1 x₂) (SAConPlus1 x₃) = refl , refl
    actdet-synth EETop (SPlus x x₁) (SAConPlus1 x₂) (SAConPlus2 x₃) = abort (x₃ x₂)
    actdet-synth EETop (SPlus x x₁) (SAConPlus2 x₂) (SAConPlus1 x₃) = abort (x₂ x₃)
    actdet-synth EETop (SPlus x x₁) (SAConPlus2 x₂) (SAConPlus2 x₃) = refl , refl
    actdet-synth EETop (SPlus x x₁) (SAConApArr x₂) (SAConApArr x₃) with matcharrunicity x₂ x₃
    ... | refl = refl , refl
    actdet-synth EETop (SPlus x x₁) (SAConApArr x₂) (SAConApOtw x₃) = abort (matchnotnum x₂)
    actdet-synth EETop (SPlus x x₁) (SAConApOtw x₂) (SAConApArr x₃) = abort (matchnotnum x₃)
    actdet-synth EETop (SPlus x x₁) (SAConApOtw x₂) (SAConApOtw x₃) = refl , refl
    actdet-synth EETop (SPlus x x₁) SAConNEHole SAConNEHole = refl , refl

    actdet-synth (EEPlusL E) (SPlus x x₁) (SAMove x₂) (SAMove x₃) = movedet x₂ x₃ , refl
    actdet-synth (EEPlusL E) (SPlus x x₁) (SAMove EMPlusParent1) (SAZipPlus1 d2) = abort (lem-nomove-para d2)
    actdet-synth (EEPlusL E) (SPlus x x₁) (SAZipPlus1 x₂) (SAMove EMPlusParent1) = abort (lem-nomove-para x₂)
    actdet-synth (EEPlusL E) (SPlus x x₁) (SAZipPlus1 x₂) (SAZipPlus1 x₃) {p1} {p2}
      = ap1 (λ x₄ → x₄ ·+₁ _) (actdet-ana E x x₂ x₃  {p1} {p2}) , refl

    actdet-synth (EEPlusR E) (SPlus x x₁) (SAMove x₂) (SAMove x₃) = movedet x₂ x₃ , refl
    actdet-synth (EEPlusR E) (SPlus x x₁) (SAMove EMPlusParent2) (SAZipPlus2 x₃) = abort (lem-nomove-para x₃)
    actdet-synth (EEPlusR E) (SPlus x x₁) (SAZipPlus2 x₂) (SAMove EMPlusParent2) = abort (lem-nomove-para x₂)
    actdet-synth (EEPlusR E) (SPlus x x₁) (SAZipPlus2 x₂) (SAZipPlus2 x₃) {p1} {p2}
      = ap1 (_·+₂_ _) (actdet-ana E x₁ x₂ x₃ {p1} {p2}) , refl

    actdet-synth EETop SEHole (SAMove x) (SAMove x₁) = movedet x x₁ , refl
    actdet-synth EETop SEHole SADel SADel = refl , refl
    actdet-synth EETop SEHole SAConAsc SAConAsc = refl , refl
    actdet-synth EETop SEHole (SAConVar {Γ = G} p) (SAConVar p₁) = refl , (ctxunicity {Γ = G} p p₁)
    actdet-synth EETop SEHole (SAConLam x₁) (SAConLam x₂) = refl , refl
    actdet-synth EETop SEHole SAConNumlit SAConNumlit = refl , refl
    actdet-synth EETop SEHole (SAConPlus1 x) (SAConPlus1 x₁) = refl , refl
    actdet-synth EETop SEHole (SAConPlus1 x) (SAConPlus2 x₁) = abort (x₁ x)
    actdet-synth EETop SEHole (SAConPlus2 x) (SAConPlus1 x₁) = abort (x x₁)
    actdet-synth EETop SEHole (SAConPlus2 x) (SAConPlus2 x₁) = refl , refl
    actdet-synth EETop SEHole (SAConApArr x) (SAConApArr x₁) with matcharrunicity x x₁
    ... | refl = refl , refl
    actdet-synth EETop SEHole (SAConApArr x) (SAConApOtw x₁) = abort (x₁ TCHole2)
    actdet-synth EETop SEHole (SAConApOtw x) (SAConApArr x₁) = abort (x TCHole2)
    actdet-synth EETop SEHole (SAConApOtw x) (SAConApOtw x₁) = refl , refl
    actdet-synth EETop SEHole SAConNEHole SAConNEHole = refl , refl

    actdet-synth EETop (SNEHole wt) (SAMove x) (SAMove x₁) = movedet x x₁ , refl
    actdet-synth EETop (SNEHole wt) SADel SADel = refl , refl
    actdet-synth EETop (SNEHole wt) SAConAsc SAConAsc = refl , refl
    actdet-synth EETop (SNEHole wt) (SAConPlus1 x) (SAConPlus1 x₁) = refl , refl
    actdet-synth EETop (SNEHole wt) (SAConPlus1 x) (SAConPlus2 x₁) = abort (x₁ x)
    actdet-synth EETop (SNEHole wt) (SAConPlus2 x) (SAConPlus1 x₁) = abort (x x₁)
    actdet-synth EETop (SNEHole wt) (SAConPlus2 x) (SAConPlus2 x₁) = refl , refl
    actdet-synth EETop (SNEHole wt) (SAFinish x) (SAFinish x₁) = refl , synthunicity x x₁
    actdet-synth EETop (SNEHole wt) (SAConApArr x) (SAConApArr x₁) with matcharrunicity x x₁
    ... | refl = refl , refl
    actdet-synth EETop (SNEHole wt) (SAConApArr x) (SAConApOtw x₁) = abort (x₁ TCHole2)
    actdet-synth EETop (SNEHole wt) (SAConApOtw x) (SAConApArr x₁) = abort (x TCHole2)
    actdet-synth EETop (SNEHole wt) (SAConApOtw x) (SAConApOtw x₁) = refl , refl
    actdet-synth EETop (SNEHole wt) SAConNEHole SAConNEHole = refl , refl

    actdet-synth (EENEHole E) (SNEHole wt) (SAMove x) (SAMove x₁) = movedet x x₁ , refl
    actdet-synth (EENEHole E) (SNEHole wt) (SAMove EMNEHoleParent) (SAZipHole _ x₁ d2) = abort (lem-nomove-pars d2)
    actdet-synth (EENEHole E) (SNEHole wt) (SAZipHole _ x d1) (SAMove EMNEHoleParent) = abort (lem-nomove-pars d1)
    actdet-synth (EENEHole E) (SNEHole wt) (SAZipHole a x d1) (SAZipHole b x₁ d2) {p1} {p2}
      with erasee-det a b
    ... | refl with synthunicity x x₁
    ... | refl with actdet-synth a x d1 d2  {p1} {p2}
    ... | refl , refl = refl , refl

    -- an action on an expression in an analytic position produces one
    -- resultant expression and type.
    actdet-ana : {Γ : ·ctx} {e e' e'' : ê} {e◆ : ė} {t : τ̇} {α : action} →
              (erase-e e e◆) →
              (Γ ⊢ e◆ <= t) →
              (d1 : Γ ⊢ e ~ α ~> e' ⇐ t) →
              (d2 : Γ ⊢ e ~ α ~> e'' ⇐ t) →
              {p1 : aasubmin-ana d1} →
              {p2 : aasubmin-ana d2} →
              e' == e''
    ---- lambda cases first
    -- an erased lambda can't be typechecked with subsume
    actdet-ana (EELam _) (ASubsume () _) _ _

    -- for things paired with movements, punt to the move determinism case
    actdet-ana _ _ D (AAMove y) = anamovedet D y
    actdet-ana _ _ (AAMove y) D =  ! (anamovedet D y)

    -- lambdas never match with subsumption actions, because it won't be well typed.
    actdet-ana EETop      (ALam x₁ x₂ wt) (AASubsume EETop () x₅ x₆) _
    actdet-ana (EELam _) (ALam x₁ x₂ wt) (AASubsume (EELam x₃) () x₅ x₆) _
    actdet-ana EETop      (ALam x₁ x₂ wt) _ (AASubsume EETop () x₅ x₆)
    actdet-ana (EELam _) (ALam x₁ x₂ wt) _ (AASubsume (EELam x₃) () x₅ x₆)

    -- with the cursor at the top, there are only two possible actions
    actdet-ana EETop (ALam x₁ x₂ wt) AADel AADel = refl
    actdet-ana EETop (ALam x₁ x₂ wt) AAConAsc AAConAsc = refl

    -- and for the remaining case, recurr on the smaller derivations
    actdet-ana (EELam er) (ALam x₁ x₂ wt) (AAZipLam x₃ x₄ d1) (AAZipLam x₅ x₆ d2) {p1} {p2}
       with matcharrunicity x₄ x₆
    ... | refl with matcharrunicity x₄ x₂
    ... | refl with actdet-ana er wt d1 d2  {p1} {p2}
    ... | refl = refl

    ---- now the subsumption cases
      -- subsume / subsume, so pin things down then recurr
    actdet-ana er (ASubsume a b) (AASubsume x x₁ x₂ x₃) (AASubsume x₄ x₅ x₆ x₇) {p1} {p2}
      with erasee-det x₄ x
    ... | refl with erasee-det er x₄
    ... | refl with synthunicity x₅ x₁
    ... | refl = π1 (actdet-synth x x₅ x₂ x₆ {min-ana-lem x₂ p1} {min-ana-lem x₆ p2})

    -- (these are all repeated below, irritatingly.)
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x SADel x₁) AADel = refl
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x SAConAsc x₁) AAConAsc {p1} = abort p1
    actdet-ana EETop (ASubsume SEHole b) (AASubsume EETop SEHole (SAConVar {Γ = Γ} p) x₂) (AAConVar x₅ p₁)
      with ctxunicity {Γ = Γ} p p₁
    ... | refl = abort (x₅ x₂)
    actdet-ana EETop (ASubsume SEHole b) (AASubsume EETop SEHole (SAConLam x₄) x₂) (AAConLam1 x₅ m) {p1} = abort p1
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x₁ (SAConLam x₃) x₂) (AAConLam2 x₅ x₆) = abort (x₆ x₂)
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x₁ SAConNumlit x₂) (AAConNumlit x₄) = abort (x₄ x₂)
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x (SAFinish x₂) x₁) (AAFinish x₄) = refl

      -- subsume / del
    actdet-ana er (ASubsume a b) AADel (AASubsume x x₁ SADel x₃) = refl
    actdet-ana er (ASubsume a b) AADel AADel = refl

      -- subsume / conasc
    actdet-ana EETop (ASubsume a b) AAConAsc (AASubsume EETop x₁ SAConAsc x₃) {p2 = p2} = abort p2
    actdet-ana er (ASubsume a b) AAConAsc AAConAsc = refl

      -- subsume / convar
    actdet-ana EETop (ASubsume SEHole b) (AAConVar x₁ p) (AASubsume EETop SEHole (SAConVar {Γ = Γ} p₁) x₅)
      with ctxunicity {Γ = Γ} p p₁
    ... | refl = abort (x₁ x₅)
    actdet-ana er (ASubsume a b) (AAConVar x₁ p) (AAConVar x₂ p₁) = refl

      -- subsume / conlam1
    actdet-ana EETop (ASubsume SEHole b) (AAConLam1 x₁ x₂) (AASubsume EETop SEHole (SAConLam x₃) x₆) {p2 = p2} = abort p2
    actdet-ana er (ASubsume a b) (AAConLam1 x₁ MAHole) (AAConLam2 x₃ x₄) = abort (x₄ TCHole2)
    actdet-ana er (ASubsume a b) (AAConLam1 x₁ MAArr) (AAConLam2 x₃ x₄) = abort (x₄ (TCArr TCHole1 TCHole1))
    actdet-ana er (ASubsume a b) (AAConLam1 x₁ x₂) (AAConLam1 x₃ x₄) = refl

      -- subsume / conlam2
    actdet-ana EETop (ASubsume SEHole TCRefl) (AAConLam2 x₁ x₂) (AASubsume EETop SEHole x₅ x₆) = abort (x₂ TCHole2)
    actdet-ana EETop (ASubsume SEHole TCHole1) (AAConLam2 x₁ x₂) (AASubsume EETop SEHole (SAConLam x₃) x₆) = abort (x₂ x₆)
    actdet-ana EETop (ASubsume SEHole TCHole2) (AAConLam2 x₁ x₂) (AASubsume EETop SEHole x₅ x₆) = abort (x₂ TCHole2)
    actdet-ana EETop (ASubsume a b) (AAConLam2 x₂ x₁) (AAConLam1 x₃ MAHole) = abort (x₁ TCHole2)
    actdet-ana EETop (ASubsume a b) (AAConLam2 x₂ x₁) (AAConLam1 x₃ MAArr) = abort (x₁ (TCArr TCHole1 TCHole1))
    actdet-ana er (ASubsume a b) (AAConLam2 x₂ x) (AAConLam2 x₃ x₄) = refl

      -- subsume / numlit
    actdet-ana er (ASubsume a b) (AAConNumlit x) (AASubsume x₁ x₂ SAConNumlit x₄) = abort (x x₄)
    actdet-ana er (ASubsume a b) (AAConNumlit x) (AAConNumlit x₁) = refl

      -- subsume / finish
    actdet-ana er (ASubsume a b) (AAFinish x) (AASubsume x₁ x₂ (SAFinish x₃) x₄) = refl
    actdet-ana er (ASubsume a b) (AAFinish x) (AAFinish x₁) = refl