-
Notifications
You must be signed in to change notification settings - Fork 0
/
equal.ya
28 lines (22 loc) · 872 Bytes
/
equal.ya
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
package equal where
type Equal (A: Type) (a: A): ∀ (ω b: A) -> Type {
Refl: Equal A a a
}
// if a ~ b then b ~ a
def Equal.sym (0 A: Type) (a b: A) (e: Equal A a b) : Equal A b a
= (case e) (λ b e => Equal A b a) (Equal.Refl A a)
// ∀ a, b, c if a ~ b and b ~ c then a ~ c
def Equal.trans (0 A: Type) (a b c: A) (ab: Equal A a b) (bc: Equal A b c)
: Equal A a c
= (case bc) (λ b' _ => Equal A a b') ab
// if a ~A b then f(a) ~B f(b)
def Equal.cong (0 A B: Type) (a b: A) (f: ∀ A -> B) (e: Equal A a b)
: Equal B (f a) (f b)
= (case e) (λ b' _ => Equal B (f a) (f b')) (Equal.Refl B (f a))
def Equal.rewrite (A: Type) (a b: A) (e: Equal A a b) (P: ∀ A -> Type) (x: P a)
: P b
= (case e) (λ b e => P b) x
//def Equal.cast
// (0 A: Type) (0 a b: A) (0 P: ∀ A -> Type) (e: Equal A a b) (x: P a)
// : P b
// = (case e) (λ b' _ => P b') x