boollib/bool.ktt

Booleans and negation as a path Bool = Bool.

4 declarations, all certified by the kernel · source

1import equiv
2 
3✓data Bool : U := false | true
4 
5✓def not : Bool -> Bool
6  | false => true
7  | true => false
8 
9✓def notnot : (b : Bool) -> Path Bool (not (not b)) b
10  | false => \i -> false
11  | true => \i -> true
12 
13✓def notPath : Path U Bool Bool := isoToPath not not notnot notnot