plt-amy

module Test498 where

open import Agda.Builtin.Equality
open import Agda.Builtin.String
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open Agda.Primitive renaming (Set to Type)

_×_ : ∀ {l l'} → Type l → Type l' → Type _
A × B = Σ A λ _ → B

plt-amy

#!/usr/bin/env bash

set -euo pipefail

# just some sanity checks to make sure the arguments make sense
if ! test -f "${1}"; then
  echo "usage: ${0} <file>"
  exit 1
fi
file="${1}"

plt-amy

From 681d6cab3a00f0a224b6a86af8e0765a27440fa4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Tue, 17 Dec 2024 11:26:35 -0300
Subject: [PATCH] speed up product solver

---
 src/Cat/Diagram/Product/Solver.lagda.md | 42 ++++++++++++++++++++++---
 1 file changed, 38 insertions(+), 4 deletions(-)

diff --git a/src/Cat/Diagram/Product/Solver.lagda.md b/src/Cat/Diagram/Product/Solver.lagda.md

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

plt-amy

From 12bb502c978c8aca394e45def80e0717d912f431 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
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

{-# 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

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

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

From 6c8f9045394fc620dc82909b99889c2e35df1d4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
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

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 Γ Γ