a type theory with equality based on setoids
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.
|
|
- let
- congComp : {A B : Type} (f : A -> B) {x : A}
- -> cong f (refl {A} {x}) == refl {B} {f x};
- congComp f = refl;
-
- congComp
|