There should a lemma says Bijective implies Inverse^b in Function.Consequences

[onestruggler]

agda-stdlib/src/Function/Consequences.agda

Line 58 in 54f5c38

inverseᵇ⇒bijective : ∀ (≈₂ : Rel B ℓ₂) →

I tried to add this implication, but failed because I cannot specify the type of inv-f : B -> A, due to the use of generalized variables.

I showed it in my own code. The following is checked by Agda.

{-# OPTIONS --cubical-compatible --safe #-}

module BijectiveImpliesInverse where
open import Data.Product.Base as Product
open import Function.Definitions
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
open import Relation.Nullary.Negation.Core using (¬_; contraposition)

open import Function.Definitions
open import Relation.Binary.Definitions
------------------------------------------------------------------------
-- Bijective

bijective⇒inverseᵇ : ∀ {A B : Set} {f} {ℓ₁ ℓ₂} (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
                     Reflexive ≈₂ →
                     Symmetric ≈₁ →
                     Symmetric ≈₂ →
                     Transitive ≈₁ →
                     Transitive ≈₂ →
                     Bijective ≈₁ ≈₂ f →
                     ∃ \f⁻¹ -> Inverseᵇ ≈₁ ≈₂ f f⁻¹

bijective⇒inverseᵇ {A} {B} {f} {ℓ₁} {ℓ₂} ≈₁ ≈₂ ref sym1 sym2 trans1 trans2 (inj , surj) =
  inv-f , (l , r)
  where
  inv-f : B -> A
  inv-f x with surj x
  ... | (y , _) = y
  

  l : Inverseˡ ≈₁ ≈₂ f inv-f
  l {y} {x} x=inv-fy with surj y
  ... | (x , p) = p x=inv-fy

  aux : ∀ y -> ≈₂ (f (inv-f y)) y
  aux y with surj y
  ... | (x , p) = p (inj ref)

  aux2 : ∀ x -> ≈₁ (inv-f (f x)) x
  aux2 x with surj (f x)
  ... | (z , p) = inj (p (inj ref))

  inv-f-cong : ∀ y1 y2 -> ≈₂ y1 y2 -> ≈₁ (inv-f y1) (inv-f y2)
  inv-f-cong y1 y2 eq = inj (trans2 (aux y1) (trans2 eq (sym2 (aux y2))))
  
  r : Inverseʳ ≈₁ ≈₂ f inv-f
  r {x} {y} y=fx with surj (f x)
  ... | (z , p) = trans1 (inv-f-cong y (f x) y=fx) (aux2 x)

[Taneb]

Agreed! There's already a proof of this hidden in Function.Properties.Bijection, which could be cleaned up a little if we had this in Function.Consequences

[jamesmckinna]

Two thoughts:

• see [ refactor ] Symmetry of Bijection as a consequence of properties of a given Surjective function #2583 for a lot of machinery associated with Bijections, but perhaps can be simplified with your lemma?
• your proof

  r : Inverseʳ ≈₁ ≈₂ f inv-f
  r {x} {y} y=fx with surj (f x)
    ... | (z , p) = trans1 (inv-f-cong y (f x) y=fx) (aux2 x)

doesn't make use of z or p, so the with can be deleted in favour of simply writing

r {x} {y} y=fx = trans1 (inv-f-cong y (f x) y=fx) (aux2 x)

???

And a third, meta question:
Do we need this as a Consequence, rather than in some more richly articulated context? It's hard to imagine an instance of the lemma outside a setting where we don't already have the hypotheses in scope...?

[jamesmckinna]

agda-stdlib/src/Function/Consequences.agda

Line 58 in 54f5c38
inverseᵇ⇒bijective : ∀ (≈₂ : Rel B ℓ₂) →

I tried to add this implication, but failed because I cannot specify the type of inv-f : B -> A, due to the use of generalized variables.

Looping back to the OP, I'm not clear how/why the variable declarations cause you problems? (That's not to say that they don't themselves need refactoring... because some of the implicits need inferring, where making them explicit would be... better/preferable)

[onestruggler]

Looping back to the OP, I'm not clear how/why the variable declarations cause you problems? (That's not to say that they don't themselves need refactoring... because some of the implicits need inferring, where making them explicit would be... better/preferable)

Now I see variable declaration is not a problem, if we also provide the needed varible in the function definition.

Check the following code. Agda won't let me put A and x in the hole in the first module, but no problem if we provide the implicit parameter {A} in the second module.

{-# OPTIONS --cubical-compatible --safe #-}

module BijectiveImpliesInverse where
open import Data.Product.Base as Product
open import Function.Definitions
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
open import Relation.Nullary.Negation.Core using (¬_; contraposition)

open import Function.Definitions
open import Relation.Binary.Definitions

module UsingVariableKeyword where

  variable
    A : Set
  ------------------------------------------------------------------------
  -- Bijective

  bijective⇒inverseᵇ : ∀ {B : Set} {f} {ℓ₁ ℓ₂} (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
                       Reflexive ≈₂ →
                       Symmetric ≈₁ →
                       Symmetric ≈₂ →
                       Transitive ≈₁ →
                       Transitive ≈₂ →
                       Bijective ≈₁ ≈₂ f →
                       ∃ \f⁻¹ -> Inverseᵇ ≈₁ ≈₂ f f⁻¹

  bijective⇒inverseᵇ {B} {f} {ℓ₁} {ℓ₂} ≈₁ ≈₂ ref sym1 sym2 trans1 trans2 (inj , surj) =
    {!!}
    where
    inv-f : B -> {!A!}
    inv-f x with surj {!x!}
    ... | (y , _) = y

module UsingVariableKeyword-ButAlsoProvideParameterA where

  variable
    A : Set
  ------------------------------------------------------------------------
  -- Bijective

  bijective⇒inverseᵇ : ∀ {B : Set} {f} {ℓ₁ ℓ₂} (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
                       Reflexive ≈₂ →
                       Symmetric ≈₁ →
                       Symmetric ≈₂ →
                       Transitive ≈₁ →
                       Transitive ≈₂ →
                       Bijective ≈₁ ≈₂ f →
                       ∃ \f⁻¹ -> Inverseᵇ ≈₁ ≈₂ f f⁻¹

  bijective⇒inverseᵇ {A} {B} {f} {ℓ₁} {ℓ₂} ≈₁ ≈₂ ref sym1 sym2 trans1 trans2 (inj , surj) =
    {!!}
    where
    inv-f : B -> A
    inv-f x with surj x
    ... | (y , _) = y

[onestruggler]

doesn't make use of z or p, so the with can be deleted in favour of simply writing

r {x} {y} y=fx = trans1 (inv-f-cong y (f x) y=fx) (aux2 x)

Yes, Indeed. Thanks. I overlooked it.

And a third, meta question: Do we need this as a Consequence, rather than in some more richly articulated context? It's hard to imagine an instance of the lemma outside a setting where we don't already have the hypotheses in scope...?

The Consequence.Setoid and Consequence.Propositional file cite the lemmas in Consequence file to prove their versions in a rich context. I think this is a good way in that 1) it avoids the code duplication; 2) it uses minimum assumptions, which helps clear up the dependences.

Another thing is that, no matter where they go, I think it's better to put two directions bijective⇒inverseᵇ and inverseᵇ⇒bijective together, just in case someone mistakenly think only one direction holds.

[jamesmckinna]

Regarding the use of variables: it may be that Agda's documentation isn't up to the task (I see no explanation of this, at least under https://agda.readthedocs.io/en/stable/language/generalization-of-declared-variables.html, and the account in https://agda.readthedocs.io/en/stable/language/implicit-arguments.html doesn't focus on this use case for the syntax), but I believe your problem can be solved using named telescopes, as:

module UsingVariableKeyword where

  variable
    A : Set
  ------------------------------------------------------------------------
  -- Bijective

  bijective⇒inverseᵇ : ∀ {B : Set} {f} {ℓ₁ ℓ₂} (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
                       Reflexive ≈₂ →
                       Symmetric ≈₁ →
                       Symmetric ≈₂ →
                       Transitive ≈₁ →
                       Transitive ≈₂ →
                       Bijective ≈₁ ≈₂ f →
                       ∃ \f⁻¹ -> Inverseᵇ ≈₁ ≈₂ f f⁻¹

  bijective⇒inverseᵇ {A = A} {B} {f} {ℓ₁} {ℓ₂} ≈₁ ≈₂ ref sym1 sym2 trans1 trans2 (inj , surj) =
    {!!}
    where
    inv-f : B -> {!A!}
    inv-f x with surj {!x!}
    ... | (y , _) = y

The additional binding {A = A} refers to the A implicitly bound by the variable A occurring in the subsequent binding (≈₁ : Rel A ℓ₁).

Alternatively, you could write inv-f : B -> _, because the typechecker can infer the (hidden) type?

NB.

• B can similarly be generalised, and this delegated to a top-level variable declaration...
• regardless of other considerations, in this code fragment at least, if not in the full version, I think you don't even need a type signature for inv-f, as its definition can simply be inlined as inv-f = proj₁ ∘ surj?

[onestruggler]

The additional binding {A = A} refers to the A implicitly bound by the variable A occurring in the subsequent binding (≈₁ : Rel A ℓ₁).
This works and is a nice way.

Alternatively, you could write inv-f : B -> _, because the typechecker can infer the (hidden) type?
This way desn't work. I cannot put x in the hole still.

• regardless of other considerations, in this code fragment at least, if not in the full version, I think you don't even need a type signature for inv-f, as its definition can simply be inlined as inv-f = proj₁ ∘ surj?
  This way works for defining inv-f, but later, I cannot put f in the hole.

    inv-f : B -> _
    inv-f x with surj {!x!}
    ... | (y , _) = y

    inv-f' = proj₁ ∘ surj


    l : Inverseˡ ≈₁ ≈₂ {!f!} inv-f'
    l {y} {x} x=inv-fy with surj y
    ... | (x , p) = p x=inv-fy

[onestruggler]

• B can similarly be generalised, and this delegated to a top-level variable declaration...
  Similar situation for B too. I can specify the type, and I cannot define inv-f.

module UsingVariableKeywordForB where

  variable
    B : Set

  ------------------------------------------------------------------------
  -- Bijective

  bijective⇒inverseᵇ : ∀ {A : Set} {f} {ℓ₁ ℓ₂} (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
                       Reflexive ≈₂ →
                       Symmetric ≈₁ →
                       Symmetric ≈₂ →
                       Transitive ≈₁ →
                       Transitive ≈₂ →
                       Bijective ≈₁ ≈₂ f →
                       ∃ \f⁻¹ -> Inverseᵇ ≈₁ ≈₂ f f⁻¹

  bijective⇒inverseᵇ {A} {f} {ℓ₁} {ℓ₂} ≈₁ ≈₂ ref sym1 sym2 trans1 trans2 (inj , surj) =
    {!!} , ({!!} , {!!})
    where
    inv-f : B -> A
    inv-f x with surj {!x!}
    ... | (y , _) = {!y!}

Anyways, just explicitly mentioning the variables in the definition is a very nice way, and it's just the implicit parameters, mentioning them when needed.

[jamesmckinna]

Maybe the best thing would be to submit a PR, and then we can debug any further problems you're having? I'm still not understanding why you (still?) can't define inv-f... UPDATED perhaps it's a case of using too much with, when each such binding could be replaced by a pattern-matching let with better definitional behaviour cf. #2123 and related issues/PRs:

bijective⇒inverseᵇ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
                     Reflexive ≈₂ →
                     Symmetric ≈₂ →
                     Transitive ≈₁ →
                     Transitive ≈₂ →
                     Bijective ≈₁ ≈₂ f →
                     ∃ (Inverseᵇ ≈₁ ≈₂ f)

bijective⇒inverseᵇ {A = A} {B = B} {f = f} ≈₁ ≈₂ refl₂ sym₂ trans₁ trans₂ (inj , surj) = inv-f , inverseˡ , inverseʳ
  where
  inv-f : B -> A
  inv-f = proj₁ ∘ surj

  inverseˡ : Inverseˡ ≈₁ ≈₂ f inv-f
  inverseˡ {x = x} = proj₂ (surj x)

  aux : ∀ y -> ≈₂ (f (inv-f y)) y
  aux y = let x , p = surj y in p (inj refl₂)

  aux2 : ∀ x -> ≈₁ (inv-f (f x)) x
  aux2 x = let z , p = surj (f x) in inj (p (inj refl₂))

  inv-f-cong : ∀ {y1 y2} -> ≈₂ y1 y2 -> ≈₁ (inv-f y1) (inv-f y2)
  inv-f-cong {y1} {y2} eq = inj (trans₂ (aux y1) (trans₂ eq (sym₂ (aux y2))))
  
  inverseʳ : Inverseʳ ≈₁ ≈₂ f inv-f
  inverseʳ = strictlyInverseʳ⇒inverseʳ {f⁻¹ = inv-f} trans₁ inv-f-cong aux2

[jamesmckinna]

Arguably, a preferable alternative (because it scales to arbitrary Setoid-based algebras: pulling back an IsX structure on the codomain along an IsXMonomorphism yields an IsX structure on the domain, would be to assume Congruent ≈₁ ≈₂ f, and then we obtain, after some additional tidying up (see #2583 again):

bijective⇒inverseᵇ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
                     Reflexive ≈₂ →
                     Symmetric ≈₂ →
                     Transitive ≈₂ →
                     Congruent ≈₁ ≈₂ f →
                     Bijective ≈₁ ≈₂ f →
                     ∃ $ Inverseᵇ ≈₁ ≈₂ f

bijective⇒inverseᵇ {A = A} {B = B} {f = f} ≈₁ ≈₂ refl₂ sym₂ trans₂ f-cong (inj , surj) = inv-f , inverseˡ , inverseʳ
  where
  isRelHomomorphism : IsRelHomomorphism ≈₁ ≈₂ f
  isRelHomomorphism = record { cong = f-cong }

  isRelMonomorphism : IsRelMonomorphism ≈₁ ≈₂ f
  isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = inj }

  refl₁ : Reflexive ≈₁
  refl₁ = Mono.refl isRelMonomorphism refl₂
  
  trans₁ : Transitive ≈₁
  trans₁ = Mono.trans isRelMonomorphism trans₂
  
  inv-f : B -> A
  inv-f = proj₁ ∘ surj

  inverseˡ : Inverseˡ ≈₁ ≈₂ f inv-f
  inverseˡ {x = x} = proj₂ (surj x)

  aux : ∀ y -> ≈₂ (f (inv-f y)) y
  aux _ = inverseˡ refl₁

  inv-f-cong : ∀ {y₁ y₂} -> ≈₂ y₁ y₂ -> ≈₁ (inv-f y₁) (inv-f y₂)
  inv-f-cong {y₁} {y₂} eq = inj (trans₂ (aux y₁) (trans₂ eq (sym₂ (aux y₂))))

  inverseʳ : Inverseʳ ≈₁ ≈₂ f inv-f
  inverseʳ = strictlyInverseʳ⇒inverseʳ {f⁻¹ = inv-f} trans₁ inv-f-cong (inj ∘ aux ∘ f)