https://types.pl/@NathanielB/117028347854979977

puzzle.agda

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

private variable
  ℓ : Level
  A : Type ℓ

sym-∘
  : (d : A → A) (f : idfun A ≡ d)
  → cong₂ _∘S_ (sym f) f ≡ refl
sym-∘ = J> refl

switcheroo : (a : A) → transport refl a ≡ transport refl a
switcheroo {A = A} a i = transp (λ _ → A) i (transp (λ _ → A) (~ i) a)

switcheroo-refl : (a : A) → switcheroo a ≡ refl
switcheroo-refl {A = A} a i j =
  sym-∘ (transport refl) (sym (λ i a → transportRefl a i)) i j a

transport-uaIdEquiv
  : (a : A)
  → (λ i → transport (uaIdEquiv i) a)
  ≡ refl
transport-uaIdEquiv a =
  (λ i → transport (uaIdEquiv i) a)
    ≡⟨⟩
  (sym (transportRefl (transport refl a))
  ∙∙ cong (transport refl) (refl ∙∙ refl ∙∙ switcheroo a)
  ∙∙ transportRefl (transport refl a))
    ≡⟨ cong (sym (transportRefl _) ∙∙_∙∙ transportRefl _)
     $ cong (cong (transport refl))
     $ doubleCompPath≡compPath _ _ _ ∙ sym (lUnit _) ∙ sym (lUnit _)
       ∙ switcheroo-refl a ⟩
  (sym (transportRefl (transport refl a))
  ∙∙ refl
  ∙∙ transportRefl (transport refl a))
    ≡⟨ ∙∙lCancel _ ⟩
  refl
    ∎

-- uaIdEquiv i j is symmetric in the j direction, so the same proof
-- works for the backwards case.
transport⁻-uaIdEquiv
  : (a : A)
  → (λ i → transport⁻ (uaIdEquiv i) a)
  ≡ refl
transport⁻-uaIdEquiv = transport-uaIdEquiv

refl-∘-refl
  : {d : A → A} (f g : d ≡ d)
  → f ≡ refl
  → g ≡ refl
  → cong₂ _∘S_ f g ≡ refl
refl-∘-refl f g p q =
  subst2 (λ f g → cong₂ _∘S_ f g ≡ refl) (sym p) (sym q) refl

transport⁻Transport-uaIdEquiv
  : (a : A)
  → (λ i → transport⁻ (uaIdEquiv i) (transport (uaIdEquiv i) a))
  ≡ refl
transport⁻Transport-uaIdEquiv a j i =
  refl-∘-refl _ _ (λ j i a → transport⁻-uaIdEquiv a j i) (λ j i a → transport-uaIdEquiv a j i) j i a

tr⁻Tr-uaId
  : (a : A)
  → transport⁻Transport (ua (idEquiv A)) a
  ≡ transport⁻Transport refl a
tr⁻Tr-uaId {A = A} a = subst
  (λ p → PathP (λ i → p i ≡ a) (transport⁻Transport (ua (idEquiv A)) a) (transport⁻Transport refl a))
  (transport⁻Transport-uaIdEquiv a)
  (cong (λ p → transport⁻Transport p a) uaIdEquiv)