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

[Guillaume Brunerie]

Hi Vlad,

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.
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.

Also, you don't need the []-law constructor, that should hold
automatically.

Best,
Guillaume


Den mån 25 jan. 2021 12:21Vlad Rusu <Vlad.Rusu at inria.fr> skrev:

> 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 = {!!}
>   -}
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210125/250c1bea/attachment.html>