15/07/2019, 20:49
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 _⇔_
A ⇔ A
. 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
⇔-refl : ∀ {A : Set} → A ⇔ A
⇔-refl = Bijection id id idIdem idIdem
A !=< Set of type Set
when checking that the expression id∘id=id has type (a : A) → a ≡ a
17/07/2019, 09:29
17/07/2019, 10:07
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 _)
⇔-sym : ∀ {A B : Set} → A ⇔ B → B ⇔ A
⇔-sym (Bijection f g gf=id fg=id) = Bijection g f fg=id gf=id
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)
Skuola.net News è una testata giornalistica iscritta al Registro degli Operatori della Comunicazione.
Registrazione: n° 20792 del 23/12/2010.
©2000—
Skuola Network s.r.l. Tutti i diritti riservati. — P.I. 10404470014.
Powered by phpBB © phpBB Group - Privacy policy - Cookie privacy
phpBB Mobile / SEO by Artodia.