- Codice:
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
A ⇔ A
. In effetti è sufficiente dimostrare che - Codice:
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
- Codice:
⇔-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:
- Codice:
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?)