78 lines
1.8 KiB
Agda
78 lines
1.8 KiB
Agda
module extraexercises where
|
|
|
|
open import Data.Nat
|
|
open import Relation.Binary.PropositionalEquality as Eq
|
|
open Eq.≡-Reasoning
|
|
|
|
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
|
|
|
|
-- Translation to PMLTT concepts
|
|
|
|
id : {A : Set} (a : A) → a ≡ a
|
|
id a = refl
|
|
|
|
idpeel : {A : Set} {a b : A}
|
|
→ (c : a ≡ b)
|
|
→ {C : (x y : A) → (z : x ≡ y) → Set}
|
|
→ (d : (x : A) → C x x (id x))
|
|
→ C a b c
|
|
idpeel {A} {a} {b} c {C} d = J C d a b c
|
|
|
|
-- Problem 2
|
|
|
|
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
|
|
|
|
-- 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 = (λ f → J (λ x y p → trans (trans x f) y ≡ trans x (trans f y)) (λ x → {! !}) {! !} {! !} {! !}) in
|
|
-- {! !}
|
|
|
|
-- Problem 3
|
|
|
|
unitl : {A : Set}
|
|
→ (a : A)
|
|
→ {b : A}
|
|
→ (d : a ≡ b)
|
|
→ trans (id a) d ≡ d
|
|
unitl a d = id d
|
|
|
|
-- Problem 4
|
|
|
|
unitr : {A : Set}
|
|
→ {a : A}
|
|
→ (b : A)
|
|
→ (d : a ≡ b)
|
|
→ trans d (id b) ≡ d
|
|
unitr {A} {a} b d = J (λ x y p → trans p (id y) ≡ p) (λ x → id (id x)) a b d
|
|
|
|
-- Problem 5
|
|
|
|
-- ap : {A : Set}
|
|
|
|
-- 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
|
|
-- {! !} |