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

[Vlad Rusu]

Hi Guillaume,

Thanks for your answer.

My knowledge of Cubical Agda and especially of the underlying theory is 
quite limited.

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?

Best regards,

  - Vlad

Le 25/01/2021 à 12:51, Guillaume Brunerie a écrit :
> 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 
> <mailto: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 <mailto: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/6c7b89a0/attachment.html>