You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
25 lines
517 B
25 lines
517 B
let
|
|
congComp : {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x == y)
|
|
-> cong (λ a → g (f a)) p == cong g (cong f p);
|
|
congComp f g p = refl;
|
|
|
|
let
|
|
the : (A : Type) -> A -> A;
|
|
the A x = x;
|
|
|
|
let
|
|
congId : {A : Type} {x y : A} (p : x == y)
|
|
-> cong (λ x → x) p == p;
|
|
congId p = ();
|
|
|
|
let
|
|
axUIP : {A : Type} {x y : A} (p q : x == y)
|
|
-> p == q;
|
|
axUIP p q = ();
|
|
|
|
let
|
|
symSym : {A : Type} {x y : A} (p : x == y)
|
|
-> sym (sym p) == p;
|
|
symSym p = refl;
|
|
|
|
congComp
|