<div dir="auto"><div>Hi Vlad,<div dir="auto"><br></div><div dir="auto">I don't think that what you are trying to prove is true, or at least not in the way you formulated it. If you take for instance the map from Unit to the higher inductive circle, it is injective in your sense, but its image is the whole circle, so it is not going to be bijective.</div><div dir="auto">You need to change something in the statement, for instance restricting it to hSets, or having a stronger definition of "injective" that works differently for arbitrary types.</div><div dir="auto"><br></div><div dir="auto">Also, you don't need the []-law constructor, that should hold automatically. </div><div dir="auto"><br></div><div dir="auto">Best, </div><div dir="auto">Guillaume </div><br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Den mån 25 jan. 2021 12:21Vlad Rusu <<a href="mailto:Vlad.Rusu@inria.fr">Vlad.Rusu@inria.fr</a>> skrev:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear all,<br>
<br>
I am trying to formalise in Cubical Agda the fact that an injective <br>
function f : A -> B becomes a bijection between A and f A, where f A is <br>
the image of A by f.<br>
<br>
Moreover I would like to prove the bijection by exhibiting a function f' <br>
: f A -> A and show that the two functions are inverse to each other, <br>
thus obtaining an isomorphism and then the cubical equality between A <br>
and f A.<br>
<br>
Below is what I did so far. I am left with one hole but can't see how to <br>
fill it. Does anyone have an idea what term goes there?<br>
<br>
Best regards,<br>
<br>
  - Vlad<br>
<br>
---<br>
<br>
{-# OPTIONS --cubical  #-}<br>
<br>
module Injection where<br>
<br>
open import Cubical.Core.Everything<br>
open import Cubical.Foundations.Prelude<br>
<br>
trans : {A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c<br>
trans a _ _  p q i = hcomp<br>
  (λ j -> λ<br>
   { (i = i0) -> a<br>
   ; (i = i1) -> q j<br>
   })<br>
  (p i)<br>
<br>
<br>
-- image of a function f : A → B : the elements b ∈ B for which there is <br>
an a ∈ A and a proof that b ≡ f a<br>
-- the element of A and the proof are quotiented away so that they don't <br>
interfere in equalities<br>
<br>
-- would an additional constructor identifying all identity proofs (like <br>
"squash/" in Cubical.HITs.SetQuotients) be helpful?<br>
<br>
data Im {A B : Set}  (f : A → B) : Set where<br>
   [_] : Σ[ b ∈ B ] (Σ[ a ∈ A ] (f a  ≡ b)) → Im  f<br>
   []-law : forall b b' → fst b ≡ fst b' → [ b ] ≡ [ b' ]<br>
<br>
-- from A to the image<br>
A→fA : {A B : Set}  (f : A → B) (a : A) → Im f<br>
A→fA f a = [ f a , a , refl  ]<br>
<br>
-- and back. The injectiveness of the function is used here.<br>
fA→A : {A B : Set} (f : A → B) (f-inj : ∀ a a' → f a ≡ f a' → a ≡ a') → <br>
Im f → A<br>
fA→A   f f-inj   [ b , a , p ] = a<br>
fA→A f f-inj ([]-law (b , a , P)  (b' , a' , P')  Heq i) = f-inj _ _  ( <br>
trans _ _ _ (trans _ _ _ P Heq)  ((sym P'))) i<br>
<br>
-- this direction is easy<br>
A→fA→A : {A B : Set}  (f : A → B)  (f-inj : ∀ a a' → f a ≡ f a' → a ≡ <br>
a') (a : A)→ fA→A  f f-inj (A→fA  f a ) ≡ a<br>
A→fA→A   f  f-inj   a   = refl<br>
<br>
-- this one, not so much<br>
fA→A→fA : {A B : Set}  (f : A → B)  (f-inj : ∀ a a' → f a ≡ f a' → a ≡ <br>
a') (b' : Im  f)→  A→fA  f (fA→A  f f-inj b') ≡ b'<br>
fA→A→fA f f-inj [ b , a ,  P ]  = []-law (f a , (a , refl)) (b , (a , P)) P<br>
fA→A→fA f f-inj ([]-law (b , a ,  P)  (b' , a' ,  P' ) Heqb i)  = {!!}<br>
{-<br>
trans {!!} {!!} {!!} {!!} {! !} {!!}<br>
   where<br>
   aux :  [ b ,  a , P ] ≡ [ b' , a' , P' ]<br>
   aux = {!!}<br>
  -}<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div></div>