Scratch.agda

{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Everything
open import Function.Base

module Scratch {ℓ} {A B : Type ℓ} where

-- The following is supposed to be the type of inhabitants of (unbiasedly) A
-- and B where A ≡ B. It contains an inhabitant of A, an inhabitant of B, and
-- a proof that these are the same inhabitant when transported over q.

record Equivalently (q : A ≡ B) : Type ℓ where
  constructor mk
  field
    getl : A
    getr : B
    path : (λ i → q i) [ getl ≡ getr ]
open Equivalently public

-- The smart constructors take an inhabitant of A (resp. B) and produce the
-- equivalent inhabitant of B (resp. A) by doing the transport.

mkl : ∀ {q} → A → Equivalently q
mkl {q} a = mk a (transport q a) (toPathP refl)

mkr : ∀ {q} → B → Equivalently q
mkr {q} b = mk (transport (sym q) b) b
               (symP {A = λ i → q (~ i)} (toPathP refl))

-- I want to show that Equivalently {A} {B} q is equivalent to A (and
-- eventually B).
-- I think this is true by similar reasoning as the contractibility of
-- singletons (for each x : A, the type Σ[ y ] x ≡ y is contractible).
-- With getl fixed, (getr , path) at least looks a lot like an inhabitant of
-- such a singleton, as long as we can ignore the extra heterogeneity.

Equivalently-≡l : ∀ {q} → Equivalently q ≡ A
Equivalently-≡l {q} = isoToPath
  (iso getl mkl (λ _ → refl) (λ a/b →
    mk (getl a/b) (transport q (getl a/b)) (toPathP refl) ≡
    mk (getl a/b) (getr a/b) (path a/b)
    ∋ λ i → mk (getl a/b) (fromPathP (a/b .path) i)
               (((λ i → (λ j → q j) [ getl a/b ≡ fromPathP (a/b .path) i ])
                 [ toPathP refl ≡ path a/b ]
                 ∋ {!!}) i)))

-- I proceed directly. I get stuck trying to fill ?0, where I think the
-- required square looks like this:
--
--               ? i : fromPathP (a/b .path) i
--      transport q (getl a/b) ------- getr a/b
--                |                        |
-- toPathP refl j |          ? i j         | path a/b j
--                |                        |
--            getl a/b --------------- getl a/b
--                        refl i : A
--
-- It feels like this should be easy, but I don't understand it well enough to
-- solve it.