[Agda] Cubical Agda: injection is bijection to restricted codomain

[Vlad Rusu]

Dear all,

I am trying to formalise in Cubical Agda the fact that an injective 
function f : A -> B becomes a bijection between A and f A, where f A is 
the image of A by f.

Moreover I would like to prove the bijection by exhibiting a function f' 
: f A -> A and show that the two functions are inverse to each other, 
thus obtaining an isomorphism and then the cubical equality between A 
and f A.

Below is what I did so far. I am left with one hole but can't see how to 
fill it. Does anyone have an idea what term goes there?

Best regards,

  - Vlad

---

{-# OPTIONS --cubical  #-}

module Injection where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

trans : {A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
trans a _ _  p q i = hcomp
  (λ j -> λ
   { (i = i0) -> a
   ; (i = i1) -> q j
   })
  (p i)


-- image of a function f : A → B : the elements b ∈ B for which there is 
an a ∈ A and a proof that b ≡ f a
-- the element of A and the proof are quotiented away so that they don't 
interfere in equalities

-- would an additional constructor identifying all identity proofs (like 
"squash/" in Cubical.HITs.SetQuotients) be helpful?

data Im {A B : Set}  (f : A → B) : Set where
   [_] : Σ[ b ∈ B ] (Σ[ a ∈ A ] (f a  ≡ b)) → Im  f
   []-law : forall b b' → fst b ≡ fst b' → [ b ] ≡ [ b' ]

-- from A to the image
A→fA : {A B : Set}  (f : A → B) (a : A) → Im f
A→fA f a = [ f a , a , refl  ]

-- and back. The injectiveness of the function is used here.
fA→A : {A B : Set} (f : A → B) (f-inj : ∀ a a' → f a ≡ f a' → a ≡ a') → 
Im f → A
fA→A   f f-inj   [ b , a , p ] = a
fA→A f f-inj ([]-law (b , a , P)  (b' , a' , P')  Heq i) = f-inj _ _  ( 
trans _ _ _ (trans _ _ _ P Heq)  ((sym P'))) i

-- this direction is easy
A→fA→A : {A B : Set}  (f : A → B)  (f-inj : ∀ a a' → f a ≡ f a' → a ≡ 
a') (a : A)→ fA→A  f f-inj (A→fA  f a ) ≡ a
A→fA→A   f  f-inj   a   = refl

-- this one, not so much
fA→A→fA : {A B : Set}  (f : A → B)  (f-inj : ∀ a a' → f a ≡ f a' → a ≡ 
a') (b' : Im  f)→  A→fA  f (fA→A  f f-inj b') ≡ b'
fA→A→fA f f-inj [ b , a ,  P ]  = []-law (f a , (a , refl)) (b , (a , P)) P
fA→A→fA f f-inj ([]-law (b , a ,  P)  (b' , a' ,  P' ) Heqb i)  = {!!}
{-
trans {!!} {!!} {!!} {!!} {! !} {!!}
   where
   aux :  [ b ,  a , P ] ≡ [ b' , a' , P' ]
   aux = {!!}
  -}