Ansh

I made a single 0-cell, tried to edit it and it crashed. Action log: [homotopy_io_actions.txt](https://github.com/user-attachments/files/20910929/homotopy_io_actions.txt)

Failure of SR in Cubical Agda because of `transp` over a path in `Level`

2

Consider this: ```agda test : (ℓ : I → Level) → Type (ℓ i0) → Type (ℓ i1) test ℓ A = {! transp (λ i → Type (ℓ i))...

Add sharp and flat modalities (like in Agda flat). In the future we could support any modal type theory, but for now I think spatial type theory will be useful...

Arend is inconsistent

1

I found a proof of Empty in Arend without any axioms: ``` \import Logic \data Bad : \Prop | mkBad (\Pi {P : \Prop} -> P -> P) \func bad...

Typechecker loops

1

Impredicativity in Arend allows encoding the Girard-Hurken paradox in an inconsistent context; In the following code: ```arend \import HLevel \import Logic \import Paths.Meta \class Girard (all-prop : \Pi (A :...

Make `Lift`'s level argument explicit

5

See the discussion at [#1236](https://github.com/agda/cubical/issues/1236#issuecomment-3531207216)

The promised sequel to #1212

I defined heaps (aka grouds) and did the SIP boilerplate. I defined the structure group of a heap, and proved that a group is equivalently a pointed heap. I didn't...

The powerset is not universe polymorphic enough

4

Currently, for `A : Type l`, `ℙ A` is defined as `A -> hProp l`, however I frequently find myself needing to use `A -> hProp l'` where `l'` is...

New notion of equivalence: Bijective relations

3

IMO, cubically this is a very natural notion of equivalence, because from any path `p : A ≡ B` we get a bijective relation `PathP λ i → P i`...