[Agda] proprietà dell'equipotenza

[caulacau]

La relazione di equipotenza tra due tipi in Agda si definisce così:

record _⇔_ (A B : Set) : Set where
  constructor Bijection
  field
    A→B : A → B
    B→A : B → A
    A→B→A : ∀ (a : A) → B→A (A→B a) ≡ a
    B→A→B : ∀ (b : B) → A→B (B→A b) ≡ b

open _⇔_

Sarebbe bello, ora, saper dimostrare almeno che [inline]A ⇔ A[/inline]. In effetti è sufficiente dimostrare che

Idempotent : ∀ {a} → (a → a) → Set
Idempotent f = ∀ b → f (f b) ≡ f b

idIdem : ∀ a → Idempotent (id {A = a})
idIdem _ _ = refl

per poter poi dire

⇔-refl : ∀ {A : Set} → A ⇔ A
⇔-refl = Bijection id id idIdem idIdem

Purtroppo però non funziona, e non riesco a interpretare l'errore che ricevo, che è chiaramete un type-mismatch, ma che non so come correggere perché a me sembra giusto:

A !=< Set of type Set
when checking that the expression id∘id=id has type (a : A) → a ≡ a

(PS: davvero questo obbrobrio verde vomito è l'unica maniera di inserire degli snippet di codice?)

[Indrjo Dedej]

Riporta il testo dell'errore che ricevi. Anche se laconico, qualcuno potrà aiutarti più facilmente.

[caulacau]

Alla fine ci sono riuscito, ma ho un altro problema.

Intanto, sono riuscito a dimostrare che l'equipotenza è una relazione di equivalenza.

id : ∀ {A : Set} → A → A
id x = x

Idempotent : ∀ {a} → (a → a) → Set
Idempotent f = ∀ b → f (f b) ≡ f b

idIdem : ∀ a → Idempotent (id {A = a})
idIdem _ _ = refl

⇔-refl : ∀ {A : Set} → A ⇔ A
⇔-refl = Bijection id id (idIdem _) (idIdem _)

E per la proprietà simmetrica,

⇔-sym : ∀ {A B : Set} → A ⇔ B → B ⇔ A
⇔-sym (Bijection f g gf=id fg=id) = Bijection g f fg=id gf=id

E per la proprietà transitiva, che com'era giusto aspettarsi è la più dura, servono due lemmi preliminari:

oneId : ∀ {A B C : Set}
  (f : A → B) →
  (g : B → A) →
  (u : B → C) →
  (v : C → B) →
  (vu=id : ∀ x → v (u x) ≡ x)
  (gf=id : ∀ x → g (f x) ≡ x)
  (a : A) →
  g (v (u (f a))) ≡ a
oneId f g u v vu=id gf=id x =
  begin
    g (v (u (f x)))
  ≡⟨ cong' g (vu=id (f x)) ⟩
    g (f x)
  ≡⟨ gf=id x ⟩
    x
  ∎

otherId : ∀ {A B C : Set}
  (f : A → B) →
  (g : B → A) →
  (u : B → C) →
  (v : C → B) →
  (fg=id : ∀ x → f (g x) ≡ x)
  (uv=id : ∀ x → u (v x) ≡ x)
  (c : C) →
  u (f (g (v c))) ≡ c
otherId f g u v fg=id uv=id c =
  begin
    u (f (g (v c)))
  ≡⟨ cong' u (fg=id (v c)) ⟩
    u (v c)
  ≡⟨ uv=id c ⟩
    c
  ∎

-- Task 1-3. Prove that _⇔_ relation is transitive.
⇔-trans : ∀ {A B C : Set} → A ⇔ B → B ⇔ C → A ⇔ C
⇔-trans (Bijection f g gf=id fg=id) (Bijection u v vu=id uv=id) =
  Bijection (u o f) (g o v) (oneId f g u v vu=id gf=id) (otherId f g u v fg=id uv=id)