Naïm Camille Favier

Boundaries not printed properly inside λ-expressions

2

```agda {-# OPTIONS --cubical #-} open import Agda.Primitive.Cubical open import Agda.Builtin.Cubical.Path data S¹ : Set where base : S¹ loop : base ≡ base bug : PathP (λ i →...


- [ ] `Type`. Should this be implemented using univalence? - [ ] `n-Type`

Detect nix-shell shebangs

2

Fixes https://github.com/LnL7/vim-nix/issues/10 To do: - [ ] expose and use vim's interpreter → filetype [conversion logic](https://github.com/vim/vim/blob/5bf042810b19a627eda2f170624a0cfd7b4f6ed6/runtime/autoload/dist/script.vim#L56-L200). Currently the filetype is set to the interpreter, which breaks for things like `python3`...

```toml foo = { "bar" = "baz" } ``` Results in the literal string `"bar"` for the key. The quotes should be stripped.

```hs data Config = Config { foo :: Map Text Text } deriving Generic ``` ```toml foo = { "bar" = "baz" } ``` ``` tomland decode error: The following...

[BUG] RDNS_NONE despite PTR record present

5

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Read about bug reporting in general: https://rspamd.com/doc/faq.html#how-to-report-bugs-found-in-rspamd *...

"ad" is not defined

1

$\mathrm{ad}$ is used here: https://github.com/UniMath/SymmetryBook/blob/33011ebf1fc139cc6f17ab45b5f8db7ae4b4a00a/group.tex#L2356 But is not defined. I guess it means conjugation?

I think this was carried over from an earlier version of this section

> Exercise 7.3. Show that if A is an n-type and B : A → n-Type is a family of n-types, where n ≥ −1, then the W-type W(a:A) B(a)...