Naïm Camille Favier

I'm using the nix shell, so just skipping the "install-deps" step is enough. I think this should probably either happen automatically, or be documented somewhere.

This seems redundant with our existing [proof](https://1lab.dev/Homotopy.Space.Sphere.html#1909) that the suspension of 2 points is equivalent to S¹?

Add a second button? :) I would still like a way to have the topic visible without scrolling.

No, ripgrep has the correct behaviour: ``` $ printf '\e[0;34mfoo\n' > foo $ rg . foo # shows "foo" in blue $ ig . foo # shows "[0;34mfoo" ``` That...

https://github.com/agda/agda/pull/7231

The weird thing is that reverting https://github.com/agda/agda/pull/4898 also fixes this... I'd expect `strengthen` to also traverse the term and have roughly the same performance characteristics as `freeIn`.

I don't have any benchmarks; this change is based on an experiment with a sample size of 1. I agree that it would be nice to figure out what exactly...

@plt-amy pointed out that we should really be calling `normalise` instead of `instantiateFull`, as otherwise the check is bogus: ```agda const : ∀ {ℓ ℓ'} {A : Type ℓ} {B...

Had this locally, don't remember why I didn't push; maybe I just forgot 😅

Cat.Site.Base looks good to me. I haven't reviewed anything too deeply.