39 lines
797 B
Agda
39 lines
797 B
Agda
module 0Trinitarianism.Quest4 where
|
|
|
|
open import 0Trinitarianism.Preambles.P4
|
|
|
|
data Id {A : Type} : (x y : A) → Type where
|
|
rfl : {x : A} → Id x x
|
|
|
|
private
|
|
variable
|
|
A : Type
|
|
x y z w : A
|
|
|
|
sym : Id x y → Id y x
|
|
sym rfl = rfl
|
|
|
|
trans : Id x y → Id y z → Id x z
|
|
trans rfl rfl = rfl
|
|
|
|
_*_ : Id x y → Id y z → Id x z
|
|
_*_ = trans
|
|
|
|
rfl* : (p : Id x y) → Id (rfl * p) p
|
|
rfl* rfl = rfl
|
|
|
|
*rfl : (p : Id x y) → Id (p * rfl) p
|
|
*rfl rfl = rfl
|
|
|
|
*sym : (p : Id x y) → Id (sym p * p) rfl
|
|
*sym rfl = rfl
|
|
|
|
sym* : (p : Id x y) → Id (p * sym p) rfl
|
|
sym* rfl = rfl
|
|
|
|
assoc : (p : Id x y) (q : Id y z) (r : Id z w) → Id ((p * q) * r) (p * (q * r))
|
|
assoc rfl rfl rfl = rfl
|
|
|
|
outOfId : (M : (y : A) → Id x y → Type) → M x rfl → {y : A} → (p : Id x y) → M y p
|
|
outOfId M x rfl = x
|