Restrict type of equivProof; Remove primIdJ; Rename ouc→outS everywhere

[plt-amy]

Supersedes #6012, which I screwed up in my fork. Closes #5661, by ensuring that the fibre returned from equivTransp must be an extension of the given partial fibre: this implies that EQUIVFUN must have contractible fibres.

Closes #3714, by.. well, renaming inc and ouc everywhere.

Removes primIdJ, which can be recovered as either

idJ′ : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ') →
     P x (conid i1 (λ i → x)) → ∀ {y} (p : Id x y) → P y p
idJ′ {x = x} P prefl =
  primIdElim P
    (λ φ y w →
      comp (λ i → P (outS w i) (conid (φ ∨ ~ i) λ j → outS w (i ∧ j)))
        (λ { i (φ = i1) → prefl }) prefl)

Or as

  IdJ : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ') →
      P x (conid i1 (λ i → x)) → ∀ {y} (p : Id x y) → P y p
  IdJ {x = x} P prefl reflId = prefl

Updates the docs to mention pattern matching on reflId and to mention that cubical builtins are touchy even when they aren't deep magic.

[plt-amy]

Someone should stop me from using DVCS.. "I'm not owned, I'm not owned, I continue to insist as I slowly shrink and turn into an octopus merge."

[andreasabel]

Looks like you need to update a testcase:

+Issue5955.agda:6,39-81
+The module Agda.Builtin.Cubical.Sub doesn't export the following:
+  inc (did you mean 'inS'?)
+when scope checking the declaration
+  open import Agda.Builtin.Cubical.Sub renaming (primSubOut to outS;
+                                                 inc to inS)

https://github.com/agda/agda/runs/7866031500?check_suite_focus=true#step:9:30

[plt-amy]

I'm gonna go ahead and merge this since it's unlikely anyone will weep for primIdJ — the cubical library hides it when importing, and defines their own in terms of primIdElim (like in the OP).

[andreasabel]

@plt-amy: Thanks for this fix! Would you mind adding this to the CHANGELOG?

[andreasabel]

Excellent, thanks!