plt-amy

{-# OPTIONS -vtac:10 --cubical -vtc.unquote.elaborate:50 #-}
module Test37 where

open import Agda.Builtin.Reflection
open import Agda.Primitive.Cubical
open import Agda.Builtin.Sigma
open import Agda.Builtin.Maybe
open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Unit

plt-amy

open import 1Lab.Prelude

open import Data.Nat
open import Data.Dec

module wip.untruncate where

Homogeneous : ∀ {ℓ} → Type ℓ → Type (lsuc ℓ)
Homogeneous T = Σ T λ c → ∀ c′ → Path (Type∙ _) (T , c) (T , c′)

plt-amy

open import 1Lab.Prelude

module wip.replacement where

module
  Replacement
    {ℓₐ ℓₜ ℓᵢ} {A : Type ℓₐ} {T : Type ℓₜ}
    {R : T → T → Type ℓᵢ} {rr : ∀ x → R x x}
    (locally-small : is-identity-system R rr)
    (f : A → T)

plt-amy

interleaved mutual
  data Sub  : Nat → Nat → Type
  data Term : Nat → Type

  private
    consS′ : ∀ {Δ Γ} → Sub Γ Δ → Term Γ → Sub Γ (suc Δ)
    _∘s′_  : ∀ {Γ Δ Θ} → Sub Δ Θ → Sub Γ Δ → Sub Γ Θ
    π₁′    : ∀ {Δ Γ} → Sub Δ (suc Γ) → Sub Δ Γ
    idS′   : ∀ {Γ} → Sub Γ Γ

plt-amy

From 6c8f9045394fc620dc82909b99889c2e35df1d4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <[email protected]>
Date: Sun, 5 Feb 2023 15:44:03 -0300
Subject: [PATCH] fixup: unbreak the limit module a bit

---
 src/Cat/Diagram/Limit/Base.lagda.md | 168 +++++++++++++++-------------
 1 file changed, 91 insertions(+), 77 deletions(-)

diff --git a/src/Cat/Diagram/Limit/Base.lagda.md b/src/Cat/Diagram/Limit/Base.lagda.md

plt-amy

open import Data.Set.Coequaliser
open import 1Lab.Prelude
open import Data.Bool
open import Data.Fin.Base
open import Data.Vec.Base

module wip.aly where

data Tri : Type where
  zero one two : Tri

plt-amy

open import Cat.Instances.Simplex
open import Cat.Instances.Functor
open import Cat.Instances.Comma
open import Cat.Diagram.Colimit.Base
open import Cat.Displayed.Total
open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Hom
open import Cat.Functor.Base
open import Cat.Functor.Dense
open import Cat.Prelude

plt-amy

{-# OPTIONS --without-K #-}
open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

module Test15 where

data ⊥ : Set where
¬_ : ∀ {a} → Set a → Set a
¬ X = X → ⊥

plt-amy

From 12bb502c978c8aca394e45def80e0717d912f431 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <[email protected]>
Date: Sun, 21 May 2023 20:42:57 +0200
Subject: [PATCH] drop forced args from termination

---
 src/full/Agda/Termination/TermCheck.hs | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/full/Agda/Termination/TermCheck.hs b/src/full/Agda/Termination/TermCheck.hs

plt-amy

Unexpected non-cycle [Agda-2.6.4-inplace:Agda.Compiler.JS.Compiler [Agda-2.6.4-inplace:Agda.Utils.Impossible,
                                                                    Agda-2.6.4-inplace:Agda.Compiler.JS.Pretty,
                                                                    Agda-2.6.4-inplace:Agda.Compiler.JS.Pretty,
                                                                    Agda-2.6.4-inplace:Agda.Compiler.JS.Substitution,
                                                                    Agda-2.6.4-inplace:Agda.Compiler.JS.Syntax,
                                                                    Agda-2.6.4-inplace:Agda.Compiler.Backend,
                                                                    Agda-2.6.4-inplace:Agda.Compiler.Treeless.Subst,
                                                                    Agda-2.6.4-inplace:Agda.Compiler.Treeless.Erase,
                                                                    Agda-2.6.4-inplace:Agda.Compiler.Treeless.Guards