<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Guillaume,</p>
<p>Thanks for your answer. <br>
</p>
<p>My knowledge of Cubical Agda and especially of the underlying
theory is quite limited. <br>
</p>
<p>You are suggesting to restrict the statement to hSets. I don't
see them occurring in the Cubical section of Agda's documentation.
What are those, and is there other documentation/code/... that one
could use to get acquainted with them?</p>
<p>Best regards,</p>
<p> - Vlad<br>
</p>
<div class="moz-cite-prefix">Le 25/01/2021 à 12:51, Guillaume
Brunerie a écrit :<br>
</div>
<blockquote type="cite"
cite="mid:CAFJ3QWJMcQzjePnGGC6E++JSN0CinEtPoTHtxBULDh4+Vg58Yw@mail.gmail.com">
<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"
moz-do-not-send="true">Vlad.Rusu@inria.fr</a>> skrev:<br>
</div>
<blockquote class="gmail_quote">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" moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
</div>
</div>
</blockquote>
</body>
</html>