"Please merge my slides" - normal sentence (#434)

Help! I am being perceived

src/1Lab/Reflection/Subst.agda

@@ -89,6 +89,9 @@ instance
   Has-subst-Telescope : Has-subst Telescope
   Has-subst-Telescope = record { applyS = subst-tel }
 
+  Has-subst-Abs : ∀ {ℓ} {A : Type ℓ} ⦃ _ : Has-subst A ⦄ → Has-subst (Abs A)
+  Has-subst-Abs = record { applyS = λ rho (abs nm a) → abs nm (applyS (liftS 1 rho) a) }
+
 subst-tm* ρ []             = []
 subst-tm* ρ (arg ι x ∷ ls) = arg ι (subst-tm ρ x) ∷ subst-tm* ρ ls
 
@@ -128,7 +131,7 @@ subst-tm ρ (def f args)      = def f $ subst-tm* ρ args
 subst-tm ρ (meta x args)     = meta x $ subst-tm* ρ args
 subst-tm ρ (pat-lam cs args) = pat-lam (map (subst-clause ρ) cs) (subst-tm* ρ args)
 subst-tm ρ (lam v (abs n b)) = lam v (abs n (subst-tm (liftS 1 ρ) b))
-subst-tm ρ (pi (arg ι a) (abs n b)) = pi (arg ι (subst-tm ρ a)) (abs n (subst-tm (liftS 1 ρ)  b))
+subst-tm ρ (pi (arg ι a) (abs n b)) = pi (arg ι (subst-tm ρ a)) (abs n (subst-tm (liftS 1 ρ) b))
 subst-tm ρ (lit l) = (lit l)
 subst-tm ρ unknown = unknown
 subst-tm ρ (agda-sort s) with s
@@ -145,6 +148,9 @@ subst-tel ρ ((x , arg ai t) ∷ xs) = (x , arg ai (subst-tm ρ t)) ∷ subst-te
 subst-clause σ (clause tel ps t)      = clause (subst-tel σ tel) ps (subst-tm (liftS (length tel) σ) t)
 subst-clause σ (absurd-clause tel ps) = absurd-clause (subst-tel σ tel) ps
 
+apply-abs : ∀ {ℓ} {A : Type ℓ} ⦃ _ : Has-subst A ⦄ → Abs A → Term → A
+apply-abs (abs _ x) a = applyS (a ∷ ids) x
+
 _<#>_ : Term → Arg Term → Term
 f <#> x = apply-tm f x
 

src/Cat/Functor/Amnestic.lagda.md

@@ -29,7 +29,7 @@ private variable
 ```
 -->
 
-# Amnestic functors
+# Amnestic functors {defines="amnestic"}
 
 The notion of **amnestic functor** was introduced by Adámek, Herrlich
 and Strecker in their book "The Joy of Cats"^[Cats are, indeed, very

src/Data/Set/Coequaliser.lagda.md

@@ -1,8 +1,10 @@
 <!--
 ```agda
 open import 1Lab.Reflection.Induction
+open import 1Lab.Reflection using (_v∷_ ; typeError)
 open import 1Lab.Prelude
 
+open import Data.List.Base
 open import Data.Dec
 
 open is-iso
@@ -469,6 +471,38 @@ Discrete-quotient cong rdec {x} {y} =
   ... | yes xRy = yes (quot xRy)
   ... | no ¬xRy = no λ p → ¬xRy (Congruence.effective cong p)
 
+open hlevel-projection
+private
+  sim-prop : ∀ (R : Congruence A ℓ) {x y} → is-prop (R .Congruence._∼_ x y)
+  sim-prop R = R .Congruence.has-is-prop _ _
+
+instance
+  hlevel-proj-congr : hlevel-projection (quote Congruence._∼_)
+  hlevel-proj-congr .has-level = quote sim-prop
+  hlevel-proj-congr .get-level _ = pure (quoteTerm (suc zero))
+  hlevel-proj-congr .get-argument (_ ∷ _ ∷ _ ∷ c v∷ _) = pure c
+  {-# CATCHALL #-}
+  hlevel-proj-congr .get-argument _ = typeError []
+
+private unquoteDecl eqv = declare-record-iso eqv (quote Congruence)
+module _ {R R' : Congruence A ℓ} (p : ∀ x y → Congruence._∼_ R x y ≃ Congruence._∼_ R' x y) where
+  private
+    module R = Congruence R
+    module R' = Congruence R'
+
+  open Congruence
+
+  private
+    lemma : ∀ {x y} i → is-prop (ua (p x y) i)
+    lemma {x} {y} i = is-prop→pathp (λ i → is-prop-is-prop {A = ua (p x y) i}) (R.has-is-prop x y) (R'.has-is-prop x y) i
+
+  Congruence-path : R ≡ R'
+  Congruence-path i ._∼_ x y = ua (p x y) i
+  Congruence-path i .has-is-prop x y = lemma i
+  Congruence-path i .reflᶜ = is-prop→pathp lemma R.reflᶜ R'.reflᶜ i
+  Congruence-path i ._∙ᶜ_ = is-prop→pathp (λ i → Π-is-hlevel² {A = ua (p _ _) i} {B = λ _ → ua (p _ _) i} 1 λ _ _ → lemma i) R._∙ᶜ_ R'._∙ᶜ_ i
+  Congruence-path i .symᶜ = is-prop→pathp (λ i → Π-is-hlevel {A = ua (p _ _) i} 1 λ _ → lemma i) R.symᶜ R'.symᶜ i
+
 open Congruence
 
 Congruence-pullback