diff options
Diffstat (limited to 'docs/background.agda')
| -rw-r--r-- | docs/background.agda | 150 |
1 files changed, 150 insertions, 0 deletions
diff --git a/docs/background.agda b/docs/background.agda new file mode 100644 index 0000000..15e04d7 --- /dev/null +++ b/docs/background.agda @@ -0,0 +1,150 @@ +module background where + +import Level + +module Core where + data Exists (A : Set) (B : A -> Set) : Set where + _,_ : (x : A) -> B x -> Exists A B + + fst : forall {A B} -> Exists A B -> A + fst (x , _) = x + + snd : forall {A B} -> (s : Exists A B) -> B (fst s) + snd (_ , x) = x + + data Bot : Set where + + absurd : {A : Set} -> Bot -> A + absurd () + + data Top : Set where + <> : Top + + data Bool : Set where + true : Bool + false : Bool + + if_/_then_else_ : forall {a} (x : Bool) -> + (P : Bool -> Set a) -> P true -> P false -> P x + if true / _ then x else _ = x + if false / _ then _ else x = x + + if_then_else_ : forall {a} {P : Bool -> Set a} -> + (x : Bool) -> P true -> P false -> P x + if true then x else _ = x + if false then _ else y = y + + data W (A : Set) (B : A -> Set) : Set where + _<!_ : (a : A) -> (B a -> W A B) -> W A B + + -- Ugh! Comments and definiton stolen from + -- <http://www.e-pig.org/epilogue/?p=324> + rec : forall {S P} + (C : W S P -> Set) -> -- some conclusion we hope holds + ((s : S) -> -- given a shape... + (f : P s -> W S P) -> -- ...and a bunch of kids… + ((p : P s) -> C (f p)) -> -- ...and C for each kid in the bunch… + C (s <! f)) -> -- ...does C hold for the node? + (x : W S P) -> -- If so, ... + C x -- ...C always holds. + rec C c (s <! f) = c s f (\ p -> rec C c (f p)) + + _\/_ : (A B : Set) -> Set + A \/ B = Exists Bool (\ b -> if b then A else B) + + inl : forall {A B} -> A -> A \/ B + inl x = true , x + + inr : forall {A B} -> B -> A \/ B + inr x = false , x + + case : {A B C : Set} -> A \/ B -> (A -> C) -> (B -> C) -> C + case {A} {B} {C} x f g = + (if (fst x) / (\ b -> (if b then A else B) -> C) then f else g) + (snd x) + + Tr : Bool -> Set + Tr b = if b then Top else Bot + + Nat : Set + Nat = W Bool Tr + + zero : Nat + zero = false <! absurd + + suc : Nat -> Nat + suc n = true <! \ _ -> n + + plus : Nat -> Nat -> Nat + plus x y = + rec (\ _ -> Nat) + (\ b -> if b / (\ b -> (Tr b -> Nat) -> (Tr b -> Nat) -> Nat) + then (\ _ f -> suc (f <>)) else (\ _ _ -> y)) x + + data _==_ {A : Set} : A -> A -> Set where + refl : {x : A} -> x == x + + subst : forall {A x y} -> (x == y) -> (T : A -> Set) -> T x -> T y + subst refl T t = t + + _/==_ : forall {A} -> A -> A -> Set + x /== y = x == y -> Bot + +module Ext where + data List (A : Set) : Set where + nil : List A + _::_ : A -> List A -> List A + + data Nat : Set where + zero : Nat + suc : Nat -> Nat + + data Vec (A : Set) : Nat -> Set where + nil : Vec A zero + _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n) + + head : forall {A n} -> Vec A (suc n) -> A + head (x :: _) = x + + data Fin : Nat -> Set where + fzero : forall {n} -> Fin (suc n) + fsuc : forall {n} -> Fin n -> Fin (suc n) + + _!!_ : forall {A n} -> Vec A n -> Fin n -> A + (x :: _) !! fzero = x + (x :: xs) !! fsuc i = xs !! i + + open Core using (_==_; refl; subst) + + id : {A : Set} -> A -> A + id x = x + + map : forall {A B} -> (A -> B) -> List A -> List B + map _ nil = nil + map f (x :: xs) = f x :: map f xs + + cong : forall {A B} {x y : A} -> (f : A -> B) -> x == y -> f x == f y + cong f refl = refl + + map-id==id : {A : Set} (xs : List A) -> map id xs == id xs + map-id==id nil = refl + map-id==id (x :: xs) = cong (_::_ x) (map-id==id xs) + + _#_ : forall {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C) + f # g = \ x -> f (g x) + + map-#==#-map : forall {A B C} (f : B -> C) (g : A -> B) (xs : List A) -> + map (f # g) xs == (map f # map g) xs + map-#==#-map f g nil = refl + map-#==#-map f g (x :: xs) = cong (_::_ (f (g x))) (map-#==#-map f g xs) + + -- If we could have this... + postulate ext : forall {A B} {f g : A -> B} -> + ((x : A) -> f x == g x) -> f == g + + map-id==id' : {A : Set} -> map {A} id == id + map-id==id' = ext map-id==id + + map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) -> + map (f # g) == (map f # map g) + map-#==#-map' f g = ext (map-#==#-map f g)
\ No newline at end of file |