Define bijection in Agda

Question

The question is how do we define bijection in agda? definition:

We know that

2 + 2 = 2 × 2 = 2^2 = 4

for numbers. Similarly, we have that

Bool + Bool ∼= Bool × Bool ∼= Bool → Bool

where A ∼= B means that there is a bijection between A and B, that is, that there are f : A → B and g : B → A which are inverses of each other, that is, g (f x) = x for all x : A and f (g y) = y for all y : B.

Implement these bijections in Agda!

So i started by defining Bool and some functions for it:

data Bool : Set where
  true  : Bool
  false : Bool

not : Bool → Bool
not true  = false
not false = true

T : Bool → Set
T true  = ⊤
T false = ⊥

_∧_ : Bool → Bool → Bool
true  ∧ b = b
false ∧ b = false

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

_xor_ : Bool → Bool → Bool
true  xor b = not b
false xor b = b

But im stuck on the bijections, not sure at all how to solve it.

Answer 1

The text of your exam also says what a bijection should be.

there are f : A → B and g : B → A which are inverses of each other, that is, g (f x) = x for all x : A and f (g y) = y for all y : B

In Agda you can define a record to package all that up:

record Bijection (A B : Set) : Set where
  field
    to : A -> B
    from : B -> A
    from-to : (x : A) -> from (to x) ≡ x
    to-from : (y : B) -> to (from y) ≡ y

The actual bijections you are supposed to implement yourself.