2023-10-23 00:39:02 +00:00
|
|
|
module extraexercises where
|
|
|
|
|
|
|
|
|
|
open import Data.Nat
|
|
|
|
|
open import Relation.Binary.PropositionalEquality as Eq
|
|
|
|
|
open Eq.≡-Reasoning
|
2023-11-02 08:36:58 +00:00
|
|
|
|
|
|
|
|
J : {A : Set}
|
|
|
|
|
→ (C : (x y : A) → x ≡ y → Set)
|
|
|
|
|
→ (c : (x : A) → C x x refl)
|
|
|
|
|
→ (x y : A) → (p : x ≡ y) → C x y p
|
|
|
|
|
J C c x x refl = c x
|
|
|
|
|
|
|
|
|
|
inv : {A : Set} {a b : A}
|
|
|
|
|
→ (d : a ≡ b)
|
|
|
|
|
→ sym (sym d) ≡ d
|
|
|
|
|
inv {A} {a} {b} d =
|
|
|
|
|
J (λ x y p → sym (sym p) ≡ p ) (λ x → refl) a b d
|
|
|
|
|
|
|
|
|
|
-- Problem 2
|
|
|
|
|
|
|
|
|
|
assoc : {A : Set} {a b c d : A}
|
|
|
|
|
→ (e : a ≡ b)
|
|
|
|
|
→ (f : b ≡ c)
|
|
|
|
|
→ (g : c ≡ d)
|
|
|
|
|
→ trans (trans e f) g ≡ trans e (trans f g)
|
|
|
|
|
assoc {a} {b} {c} {d} e f g =
|
|
|
|
|
let whatever = J {! !} {! !} {! !} {! !} {! !} in
|
|
|
|
|
{! !}
|
|
|
|
|
|
|
|
|
|
-- Problem 6
|
|
|
|
|
|
|
|
|
|
-- id : {A : Set} → (a : A) → a ≡ a
|
|
|
|
|
-- id a = refl
|
|
|
|
|
|
|
|
|
|
-- interchange : {A : Set}
|
|
|
|
|
-- → (a : A)
|
|
|
|
|
-- → (d : id a ≡ id a)
|
|
|
|
|
-- → (e : id a ≡ id a)
|
|
|
|
|
-- → trans d e ≡ trans e d
|
|
|
|
|
-- interchange a d e =
|
|
|
|
|
-- let transde = trans d e in
|
|
|
|
|
-- let transed = trans e d in
|
|
|
|
|
-- let tmpl = J (λ x y p → {! !}) (λ x → {! !}) (id a) (id a) transde in
|
|
|
|
|
-- {! !}
|
