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

[Guillaume Brunerie]

hSets are types satisfying the predicate `isSet` (that you can find in
Cubical.Foundations.Prelude). They are also sometimes simply called
"sets", for instance in the HoTT Book (section 3.1). Note however that
Agda’s "Set" corresponds to what is usually called "Type" in homotopy
type theory.

Best,
Guillaume

Den mån 25 jan. 2021 kl 13:34 skrev Vlad Rusu <Vlad.Rusu at inria.fr>:
>
> 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> 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