Useless code

Int.agda

{-# OPTIONS --cubical #-}

open import Cubical.Data.Int
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.SetTruncation

-- Maps out of a set-truncated int can only target sets,
-- yet it's equivalent to the normal int
data Int : Type where
  inj : ℤ → Int
  trunc : isSet Int

fwd : Int → ∥ ℤ ∥₂
fwd (inj x) = ∣ x ∣₂
fwd (trunc x y p q i j) = squash₂ (fwd x) (fwd y) (cong fwd p) (cong fwd q) i j

open Iso
basic : Iso Int ∥ ℤ ∥₂
fun basic = fwd
inv basic = rec trunc inj
rightInv basic = lem
  where
  lem : ∀ x → fwd (rec trunc inj x) ≡ x
  lem ∣ x ∣₂ = refl
  lem (squash₂ x y p q i j) k =
    squash₂ (lem x k) (lem y k)
      (λ l → lem (p l) k)
      (λ l → lem (q l) k)
      i j

leftInv basic = lem
  where
  lem : ∀ x → rec trunc inj (fwd x) ≡ x
  lem (inj x) = refl
  lem (trunc x y p q i j) k =
    trunc (lem x k) (lem y k)
      (λ l → lem (p l) k)
      (λ l → lem (q l) k)
      i j

thm : Iso Int ℤ
thm = compIso basic (setTruncIdempotentIso isSetℤ)

-- unwrap : Int → ℤ
-- unwrap (inj x) = x
-- unwrap (trunc x y p q i j) =
--   isSetℤ (unwrap x) (unwrap y) (cong unwrap p) (cong unwrap q) i j

-- theorem : ∀ x → inj (unwrap x) ≡ x
-- theorem (inj x) = refl
-- theorem (trunc x y p q i j) = {!lemma isSetℤ!}
--  where
--  lemma : (r : isSet ℤ) →
--   inj (r (unwrap x) (unwrap y) (cong unwrap p) (cong unwrap q) i j) ≡ trunc x y p q i j
--  lemma r = lem2 ∙∙ theorem x ∙∙ lem1
--   where
--   lem1 : x ≡ trunc x y p q i j
--   lem1 k = trunc x y p q (i ∧ k) (j ∧ k)
--   lem2' : ∀ x y p q → r x y p q i j ≡ x
--   lem2' x y p q k = r x y p q (i ∧ ~ k) (j ∧ ~ k)
--   lem2 : inj (r (unwrap x) (unwrap y) (cong unwrap p) (cong unwrap q) i j) ≡ inj (unwrap x)
--   lem2 = cong inj (lem2' (unwrap x) (unwrap y) (cong unwrap p) (cong unwrap q))

-- thm : Iso Int ℤ
-- fun thm = unwrap
-- inv thm = inj
-- rightInv thm _ = refl
-- leftInv thm = theorem