diff --git a/Agda-HITs/CL/CL.agda b/Agda-HITs/CL/CL.agda deleted file mode 100644 index 5e8570c..0000000 --- a/Agda-HITs/CL/CL.agda +++ /dev/null @@ -1,98 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT - -module CL where - -private - data CL' : Set where - K' : CL' - S' : CL' - app' : CL' -> CL' -> CL' - -CL : Set -CL = CL' - -K : CL -K = K' - -Sc : CL -Sc = S' - -app : CL -> CL -> CL -app = app' - -postulate - KConv : {x y : CL} -> app (app K x) y == x - SConv : {x y z : CL} -> app (app (app Sc x) y) z == app (app x z) (app y z) - -CLind : (Y : CL -> Set) - (KY : Y K) - (SY : Y Sc) - (appY : (x y : CL) -> Y x -> Y y -> Y (app x y)) - (KConvY : (x y : CL) (a : Y x) (b : Y y) -> PathOver Y KConv (appY (app K x) y (appY K x KY a) b) a) - (SConvY : (x y z : CL) (a : Y x) (b : Y y) (c : Y z) -> - PathOver Y SConv - (appY - (app (app Sc x) y) - z - (appY - (app Sc x) - y - (appY Sc x SY a) - b - ) - c - ) - (appY (app x z) (app y z) (appY x z a c) (appY y z b c)) - ) - (x : CL) -> Y x -CLind Y KY SY appY _ _ K' = KY -CLind Y KY SY appY _ _ S' = SY -CLind Y KY SY appY KConvY SConvY (app' x x₁) = appY x x₁ (CLind Y KY SY appY KConvY SConvY x) (CLind Y KY SY appY KConvY SConvY x₁) - -postulate - CLind_βKConv : (Y : CL -> Set) - (KY : Y K) - (SY : Y Sc) - (appY : (x y : CL) -> Y x -> Y y -> Y (app x y)) - (KConvY : (x y : CL) (a : Y x) (b : Y y) -> PathOver Y KConv (appY (app K x) y (appY K x KY a) b) a) - (SConvY : (x y z : CL) (a : Y x) (b : Y y) (c : Y z) -> - PathOver Y SConv - (appY - (app (app Sc x) y) - z - (appY - (app Sc x) - y - (appY Sc x SY a) - b - ) - c - ) - (appY (app x z) (app y z) (appY x z a c) (appY y z b c)) - ) - (x y : CL) -> - apd (CLind Y KY SY appY KConvY SConvY) KConv == KConvY x y (CLind Y KY SY appY KConvY SConvY x) (CLind Y KY SY appY KConvY SConvY y) - CLind_βSConv : (Y : CL -> Set) - (KY : Y K) - (SY : Y Sc) - (appY : (x y : CL) -> Y x -> Y y -> Y (app x y)) - (KConvY : (x y : CL) (a : Y x) (b : Y y) -> PathOver Y KConv (appY (app K x) y (appY K x KY a) b) a) - (SConvY : (x y z : CL) (a : Y x) (b : Y y) (c : Y z) -> - PathOver Y SConv - (appY - (app (app Sc x) y) - z - (appY - (app Sc x) - y - (appY Sc x SY a) - b - ) - c - ) - (appY (app x z) (app y z) (appY x z a c) (appY y z b c)) - ) - (x y z : CL) -> - apd (CLind Y KY SY appY KConvY SConvY) SConv == SConvY x y z (CLind Y KY SY appY KConvY SConvY x) (CLind Y KY SY appY KConvY SConvY y) (CLind Y KY SY appY KConvY SConvY z) diff --git a/Agda-HITs/CL/Thms.agda b/Agda-HITs/CL/Thms.agda deleted file mode 100644 index b995c5d..0000000 --- a/Agda-HITs/CL/Thms.agda +++ /dev/null @@ -1,122 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT -open import CL - -module Thms where - -trans-cst : (A : Set) {x y : A} (B : Set) (p : x == y) (z : B) -> transport (\x -> B) p z == z -trans-cst A B idp z = idp - -I : CL -I = app (app Sc K) K - -IConv : {x : CL} -> app I x == x -IConv {x} = SConv ∙ KConv - -B : CL -B = app (app Sc (app K Sc)) K - -BConv : {x y z : CL} -> app (app (app B x) y) z == app x (app y z) -BConv {x} {y} {z} = - ap (λ p -> app (app p y) z) SConv - ∙ ap (λ p -> app (app (app (p) (app K x)) y) z) KConv - ∙ SConv - ∙ ap (λ p -> app p (app y z)) KConv - -M : CL -M = app (app Sc I) I - -MConv : {x : CL} -> app M x == app x x -MConv {x} = - SConv - ∙ ap (λ p -> app p (app I x)) IConv - ∙ ap (app x) IConv - -T : CL -T = app (app B (app Sc I)) K - -TConv : {x y : CL} -> app (app T x) y == app y x -TConv {x} {y} = - ap (λ p -> app p y) BConv - ∙ SConv - ∙ ap (λ p -> app p (app (app K x) y)) IConv - ∙ ap (app y) KConv - -C : CL -C = - app - (app - B - (app - T - (app - (app - B - B - ) - T - ) - ) - ) - (app - (app - B - B - ) - T - ) - -CConv : {x y z : CL} -> app (app (app C x) y) z == app (app x z) y -CConv {x} {y} {z} = - ap (λ p -> app (app p y) z) BConv - ∙ ap (λ p -> app (app p y) z) TConv - ∙ ap (λ p -> app (app (app p (app (app B B) T)) y) z) BConv - ∙ ap (λ p -> app p z) BConv - ∙ ap (λ p -> app p z) TConv - ∙ ap (λ p -> app (app p x) z) BConv - ∙ BConv - ∙ TConv - -W : CL -W = app (app C Sc) I - -WConv : {x y : CL} -> app (app W x) y == app (app x y) y -WConv {x} {y} = - ap (λ p -> app p y) CConv - ∙ SConv - ∙ ap (app (app x y)) IConv - -B' : CL -B' = app C B - -B'Conv : {x y z : CL} -> app (app (app B' x) y) z == app y (app x z) -B'Conv {x} {y} {z} = - ap (λ p -> app p z) CConv - ∙ BConv - -V : CL -V = app (app B C) T - -VConv : {x y z : CL} -> app (app (app V x) y) z == app (app z x) y -VConv {x} {y} {z} = - ap (λ p -> app (app p y) z) BConv - ∙ CConv - ∙ ap (λ p -> app p y) TConv - -Y : CL -Y = app (app B' (app B' M)) M - -YConv : {x : CL} -> app Y x == app x (app Y x) -YConv {x} = - B'Conv - ∙ MConv - ∙ B'Conv - ∙ ap (app x) (! B'Conv) - -fixpoint : (x : CL) -> Σ CL (λ y -> app x y == y) -fixpoint x = app Y x , ! YConv - -S' : CL -S' = app C Sc - diff --git a/Agda-HITs/Expressions/Expressions.agda b/Agda-HITs/Expressions/Expressions.agda deleted file mode 100644 index 1e3e41f..0000000 --- a/Agda-HITs/Expressions/Expressions.agda +++ /dev/null @@ -1,59 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT - -module Expressions where - -private - data Exp' : Set where - value : Nat -> Exp' - addition : Exp' -> Exp' -> Exp' - -Exp : Set -Exp = Exp' - -val : Nat -> Exp -val = value - -plus : Exp -> Exp -> Exp -plus = addition - -postulate - add : (n m : Nat) -> plus (val n) (val m) == val (n + m) - trunc : is-set Exp - -Exp-ind : (C : Exp -> Set) - -> (vC : (n : Nat) -> C (val n)) - -> (pC : (e₁ e₂ : Exp) -> C e₁ -> C e₂ -> C(plus e₁ e₂)) - -> (addC : (n m : Nat) -> PathOver C (add n m) (pC (val n) (val m) (vC n) (vC m)) (vC (n + m))) - -> (t : (e : Exp) -> is-set (C e)) - -> (x : Exp) -> C x -Exp-ind C vC pC addC t (value n) = vC n -Exp-ind C vC pC addC t (addition e₁ e₂) = pC e₁ e₂ (Exp-ind C vC pC addC t e₁) (Exp-ind C vC pC addC t e₂) - -postulate - Exp-ind-βadd : (C : Exp -> Set) - -> (vC : (n : Nat) -> C (val n)) - -> (pC : (e₁ e₂ : Exp) -> C e₁ -> C e₂ -> C(plus e₁ e₂)) - -> (addC : (n m : Nat) -> PathOver C (add n m) (pC (val n) (val m) (vC n) (vC m)) (vC (n + m))) - -> (t : (e : Exp) -> is-set (C e)) - -> (n m : Nat) - -> apd (Exp-ind C vC pC addC t) (add n m) == addC n m - -Exp-rec : {C : Set} - -> (vC : Nat -> C) - -> (pC : C -> C -> C) - -> (addC : (n m : Nat) -> pC (vC n) (vC m) == vC (n + m)) - -> (t : is-set C) - -> Exp -> C -Exp-rec vC pC addC t (value n) = vC n -Exp-rec vC pC addC t (addition e₁ e₂) = pC (Exp-rec vC pC addC t e₁) (Exp-rec vC pC addC t e₂) - -postulate - Exp-rec-βadd : {C : Set} - -> (vC : Nat -> C) - -> (pC : C -> C -> C) - -> (addC : (n m : Nat) -> pC (vC n) (vC m) == vC (n + m)) - -> (t : is-set C) - -> (n m : Nat) - -> ap (Exp-rec vC pC addC t) (add n m) == addC n m diff --git a/Agda-HITs/Expressions/Thms.agda b/Agda-HITs/Expressions/Thms.agda deleted file mode 100644 index c5eb14a..0000000 --- a/Agda-HITs/Expressions/Thms.agda +++ /dev/null @@ -1,16 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT -open import Expressions - -module Thms where - -value : (e : Exp) -> Σ Nat (\n -> e == val n) -value = Exp-ind - (\e -> Σ Nat (\n -> e == val n)) - (\n -> n , idp) - (\e₁ e₂ v₁ v₂ -> fst v₁ + fst v₂ , - (ap (\e -> plus e e₂) (snd v₁) ∙ ap (plus (val (fst v₁))) (snd v₂)) ∙ add (fst v₁) (fst v₂) - ) - (\n m -> from-transp! (\e -> Σ Nat (\n -> e == val n)) (add n m) (pair= {!!} {!!})) - (\e -> {!!}) diff --git a/Agda-HITs/Imperative/Language.agda b/Agda-HITs/Imperative/Language.agda deleted file mode 100644 index 9efdaa4..0000000 --- a/Agda-HITs/Imperative/Language.agda +++ /dev/null @@ -1,32 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT -open import Syntax - -module Language where - -data Program : Set where - fail : Program - exec : Syntax -> State -> Program - -postulate - assignp : (z : State) (x n : Nat) -> exec (x := n) z == exec skip ( z [ x :== n ]) - comp₁ : (z : State) (S : Syntax) -> exec (conc skip S) z == exec S z - comp₂ : (z z' : State) (S₁ S₂ S₁' : Syntax) -> exec S₁ z == exec S₁' z' -> exec (conc S₁ S₂) z == exec (conc S₁' S₂) z' - while₁ : (z : State) (x n : Nat) (S : Syntax) -> defined z x -> equals z x n -> exec (while x == n do S) z == exec (conc S (while x == n do S)) z - while₂ : (z : State) (x n : Nat) (S : Syntax) -> defined z x -> unequals z x n -> exec (while x == n do S) z == exec skip z - while₃ : (z : State) (x n : Nat) (S : Syntax) -> undefined z x -> exec (while x == n do S) z == fail - -Program-elim : - (Y : Set) - -> (failY : Y) - -> (execY : Syntax -> State -> Y) - -> (assignY : (z : State) (x n : Nat) -> execY (x := n) z == execY skip ( z [ x :== n ]) ) - -> (compY₁ : (z : State) (S : Syntax) -> execY (conc skip S) z == execY S z ) - -> (compY₂ : (z z' : State) (S₁ S₂ S₁' : Syntax) -> execY S₁ z == execY S₁' z' -> execY (conc S₁ S₂) z == execY (conc S₁' S₂) z') - -> (whileY₁ : (z : State) (x n : Nat) (S : Syntax) -> defined z x -> equals z x n -> execY (while x == n do S) z == execY (conc S (while x == n do S)) z) - -> (whileY₂ : (z : State) (x n : Nat) (S : Syntax) -> defined z x -> unequals z x n -> execY (while x == n do S) z == execY skip z) - -> (whileY₃ : (z : State) (x n : Nat) (S : Syntax) -> undefined z x -> execY (while x == n do S) z == failY) - -> Program -> Y -Program-elim _ failY _ _ _ _ _ _ _ fail = failY -Program-elim _ _ execY _ _ _ _ _ _ (exec s z) = execY s z diff --git a/Agda-HITs/Imperative/Semantics.agda b/Agda-HITs/Imperative/Semantics.agda deleted file mode 100644 index 8ab4fef..0000000 --- a/Agda-HITs/Imperative/Semantics.agda +++ /dev/null @@ -1,18 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT - -module Semantics where - -data koe : Set where - a : koe - b : koe - -postulate - kek : a ↦ b - {-# REWRITE kek #-} - - -Y : koe -> Set -Y a = Nat -Y b = Bool diff --git a/Agda-HITs/Imperative/Syntax.agda b/Agda-HITs/Imperative/Syntax.agda deleted file mode 100644 index d70a487..0000000 --- a/Agda-HITs/Imperative/Syntax.agda +++ /dev/null @@ -1,66 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT - -module Syntax where - -data Maybe (A : Set) : Set where - Just : A -> Maybe A - Nothing : Maybe A - -eqN : Nat -> Nat -> Bool -eqN 0 0 = true -eqN 0 _ = false -eqN (S _) 0 = false -eqN (S n) (S m) = eqN n m - --- first coordinate represents the variable x_i, second the value -State : Set -State = List (Nat × Nat) - -_[_:==_] : State -> Nat -> Nat -> State -nil [ x :== n ] = (x , n) :: nil -((y , m) :: s) [ x :== n ] = - if eqN x y - then (x , n) :: s - else ((y , m) :: (s [ x :== n ])) - -equals : State -> Nat -> Nat -> Set -equals nil _ _ = Empty -equals ((x , n) :: s) y m = - if eqN x y - then - if eqN n m - then Unit - else Empty - else equals s y m - -unequals : State -> Nat -> Nat -> Set -unequals nil _ _ = Unit -unequals ((x , n) :: s) y m = - if eqN x y - then - if eqN n m - then Empty - else Unit - else unequals s y m - -defined : State -> Nat -> Set -defined nil y = Empty -defined ((x , n) :: s) y = - if eqN x y - then Unit - else defined s y - -undefined : State -> Nat -> Set -undefined nil y = Unit -undefined ((x , n) :: s) y = - if eqN x y - then Empty - else undefined s y - -data Syntax : Set where - skip : Syntax - _:=_ : Nat -> Nat -> Syntax - conc : Syntax -> Syntax -> Syntax - while_==_do_ : Nat -> Nat -> Syntax -> Syntax diff --git a/Agda-HITs/Integers/Integers.agda b/Agda-HITs/Integers/Integers.agda deleted file mode 100644 index f7db3ec..0000000 --- a/Agda-HITs/Integers/Integers.agda +++ /dev/null @@ -1,63 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT - -module Integers where - -private - data Integers : Set where - z : Integers - S : Integers -> Integers - P : Integers -> Integers - -Ints : Set -Ints = Integers - -nul : Ints -nul = z - -Succ : Ints -> Ints -Succ = S - -Pred : Ints -> Ints -Pred = P - -postulate - invl : (x : Integers) -> P(S x) == x - invr : (x : Integers) -> S(P x) == x - trunc : is-set Ints - -Zind : (Y : Integers -> Set) - -> (zY : Y z) - -> (SY : (x : Integers) -> Y x -> Y(S x)) - -> (PY : (x : Integers) -> Y x -> Y(P x)) - -> (invYl : (x : Integers) (y : Y x) -> PathOver Y (invl x) (PY (S x) (SY x y)) y) - -> (invYr : (x : Integers) (y : Y x) -> PathOver Y (invr x) (SY (P x) (PY x y)) y) - -> (t : (x : Integers) -> is-set (Y x)) - -> (x : Integers) -> Y x -Zind Y zY SY PY invYl invYr t z = zY -Zind Y zY SY PY invYl invYr t (S x) = SY x (Zind Y zY SY PY invYl invYr t x) -Zind Y zY SY PY invYl invYr t (P x) = PY x (Zind Y zY SY PY invYl invYr t x) - -postulate - Zind-βinvl : - (Y : Integers -> Set) - -> (zY : Y z) - -> (SY : (x : Integers) -> Y x -> Y(S x)) - -> (PY : (x : Integers) -> Y x -> Y(P x)) - -> (invYl : (x : Integers) (y : Y x) -> PathOver Y (invl x) (PY (S x) (SY x y)) y) - -> (invYr : (x : Integers) (y : Y x) -> PathOver Y (invr x) (SY (P x) (PY x y)) y) - -> (t : (x : Integers) -> is-set (Y x)) - -> (x : Integers) - -> apd (Zind Y zY SY PY invYl invYr t) (invl x) == invYl x (Zind Y zY SY PY invYl invYr t x) - - Zind-βinvr : - (Y : Integers -> Set) - -> (zY : Y z) - -> (SY : (x : Integers) -> Y x -> Y(S x)) - -> (PY : (x : Integers) -> Y x -> Y(P x)) - -> (invYl : (x : Integers) (y : Y x) -> PathOver Y (invl x) (PY (S x) (SY x y)) y) - -> (invYr : (x : Integers) (y : Y x) -> PathOver Y (invr x) (SY (P x) (PY x y)) y) - -> (t : (x : Integers) -> is-set (Y x)) - -> (x : Integers) - -> apd (Zind Y zY SY PY invYl invYr t) (invr x) == invYr x (Zind Y zY SY PY invYl invYr t x) diff --git a/Agda-HITs/Integers/Thms.agda b/Agda-HITs/Integers/Thms.agda deleted file mode 100644 index b465ae4..0000000 --- a/Agda-HITs/Integers/Thms.agda +++ /dev/null @@ -1,205 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT -open import Integers - -module Thms where - -paths_set : (A B : Set) (m : is-set B) (f g : A -> B) (a : A) -> is-set (f a == g a) -paths_set A B m f g a = \c₁ c₂ q₁ q₂ -> - prop-has-level-S - (contr-is-prop (m (f a) (g a) c₁ c₂)) - q₁ - q₂ - -trunc_paths : (A : Set) (Y : A -> Set) {x y : A} (p : x == y) (t : is-prop (Y x)) (c₁ : Y x) (c₂ : Y y) -> PathOver Y p c₁ c₂ -trunc_paths A Y p t c₁ c₂ = from-transp! Y p ((prop-has-all-paths t) c₁ (transport! Y p c₂)) - -trans-cst : (A : Set) {x y : A} (B : Set) (p : x == y) (z : B) -> transport (\x -> B) p z == z -trans-cst A B idp z = idp - -plus : Ints -> Ints -> Ints -plus n = Zind - (\m -> Ints) - n - (\m -> Succ) - (\m -> Pred) - (\x y -> from-transp (λ _ → Ints) (invl x) (trans-cst Ints Ints (invl x) (Pred (Succ y)) ∙ invl y)) - (\x y -> from-transp (λ _ → Ints) (invr x) (trans-cst Ints Ints (invr x) (Succ (Pred y)) ∙ invr y)) - (\x -> trunc) - -negate : Ints -> Ints -negate = Zind - (λ _ → Ints) - nul - (λ _ -> Pred) - (λ _ -> Succ) - (λ x y -> from-transp (λ _ -> Ints) (invl x) (trans-cst Ints Ints (invl x) (Succ (Pred y)) ∙ invr y)) - (λ x y -> from-transp (λ _ -> Ints) (invr x) (trans-cst Ints Ints (invr x) (Pred (Succ y)) ∙ invl y)) - (\x -> trunc) - -min : Ints -> Ints -> Ints -min x y = plus x (negate y) - -plus_0n : (x : Ints) -> plus x nul == x -plus_0n x = idp - -plus_n0 : (x : Ints) -> plus nul x == x -plus_n0 = Zind - (\x -> plus nul x == x) - idp - (\x p -> ap Succ p) - (\x p -> ap Pred p) - (\x y -> - trunc_paths - Ints - (\m -> plus nul m == m) - (invl x) - (trunc (plus nul (Pred (Succ x))) - (Pred(Succ x))) - (ap Pred (ap Succ y)) - y - ) - (\x y -> - trunc_paths - Ints - (\m -> plus nul m == m) - (invr x) - (trunc (plus nul (Succ (Pred x))) - (Succ(Pred x))) - (ap Succ (ap Pred y)) - y - ) - (\x -> paths_set Ints Ints trunc (\m -> plus nul m) (\m -> m) x) - -plus_assoc : (x y z : Ints) -> plus x (plus y z) == plus (plus x y) z -plus_assoc x = Zind - (λ y -> (z : Ints) -> plus x (plus y z) == plus (plus x y) z) - ( - Zind - (λ z -> plus x (plus nul z) == plus (plus x nul) z) - idp - (λ x p -> ap Succ p) - (λ x p -> ap Pred p) - {!!} - {!!} - {!!} - ) - (λ y p -> - Zind - (λ z -> plus x (plus (Succ y) z) == plus (plus x (Succ y)) z) - (p (Succ nul)) - (λ y' p' -> ap Succ p') - (λ y' p' -> ap Pred p') - {!!} - {!!} - {!!} - ) - (λ y p -> - Zind - (λ z -> plus x (plus (Pred y) z) == plus (plus x (Pred y)) z) - (p (Pred nul)) - (λ y' p' -> ap Succ p') - (λ y' p' -> ap Pred p') - {!!} - {!!} - {!!} - ) - {!!} - {!!} - {!!} - -plus_Succ : (x y : Ints) -> plus x (Succ y) == Succ(plus x y) -plus_Succ x y = idp - -Succ_plus : (x y : Ints) -> plus (Succ x) y == Succ(plus x y) -Succ_plus x = Zind - (λ y -> plus (Succ x) y == Succ(plus x y)) - idp - (λ y' p -> ap Succ p) - (λ y' p -> ap Pred p ∙ invl (plus x y') ∙ ! (invr (plus x y'))) - {!!} - {!!} - {!!} - -plus_Pred : (x y : Ints) -> plus x (Pred y) == Pred(plus x y) -plus_Pred x y = idp - -Pred_plus : (x y : Ints) -> plus (Pred x) y == Pred(plus x y) -Pred_plus x = Zind - (λ y -> plus (Pred x) y == Pred(plus x y)) - idp - (λ y' p -> ap Succ p ∙ invr (plus x y') ∙ ! (invl (plus x y'))) - (λ y' p -> ap Pred p) - {!!} - {!!} - {!!} - -plus_negr : (y : Ints) -> plus y (negate y) == nul -plus_negr = Zind - (λ y -> plus y (negate y) == nul) - idp - (λ x p -> - Succ_plus x (negate (Succ x)) - ∙ invr (plus x (negate x)) - ∙ p - ) - (λ x p -> - Pred_plus x (negate (Pred x)) - ∙ invl (plus x (negate x)) - ∙ p - ) - {!!} - {!!} - {!!} - -plus_negl : (y : Ints) -> plus (negate y) y == nul -plus_negl = Zind - (λ y -> plus (negate y) y == nul) - idp - (λ y' p -> - Pred_plus (negate y') (Succ y') - ∙ invl (plus (negate y') y') - ∙ p - ) - (λ y' p -> - Succ_plus (negate y') (Pred y') - ∙ invr (plus (negate y') y') - ∙ p - ) - {!!} - {!!} - {!!} - -plus_com : (x y : Ints) -> plus x y == plus y x -plus_com x = Zind - (λ y -> plus x y == plus y x) - (plus_0n x ∙ ! (plus_n0 x)) - (λ y' p -> - plus_Succ x y' - ∙ ap Succ p - ∙ ! (Succ_plus y' x)) - (λ y' p -> - plus_Pred x y' - ∙ ap Pred p - ∙ ! (Pred_plus y' x) - ) - {!!} - {!!} - {!!} - -times : Ints -> Ints -> Ints -times n = Zind - (λ _ → Ints) - nul - (\x y -> plus y n) - (\x y -> min y n) - (λ x y -> from-transp (λ _ → Ints) (invl x) (trans-cst Ints Ints (invl x) (min (plus y n) n) - ∙ ! (plus_assoc y n (negate n)) - ∙ ap (plus y) (plus_negr n) - ∙ plus_0n y)) - (λ x y -> from-transp (λ _ → Ints) (invr x) (trans-cst Ints Ints (invr x) (plus (min y n) n) - ∙ ! (plus_assoc y (negate n) n) - ∙ ap (λ z -> plus y z) (plus_negl n) - ∙ plus_0n y)) - (\x -> trunc) diff --git a/Agda-HITs/Interval/Interval.agda b/Agda-HITs/Interval/Interval.agda deleted file mode 100644 index 61f61cb..0000000 --- a/Agda-HITs/Interval/Interval.agda +++ /dev/null @@ -1,49 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT - -module Interval where - -postulate - I : Set - z : I - o : I - s : z == o - I-ind : (Y : I -> Set) - (zY : Y z) - (oY : Y o) - (sY : PathOver Y s zY oY) - (x : I) - -> Y x - I-ind-βz : (Y : I -> Set) - (zY : Y z) - (oY : Y o) - (sY : PathOver Y s zY oY) - -> I-ind Y zY oY sY z ↦ zY - {-# REWRITE I-ind-βz #-} - I-ind-βo : (Y : I -> Set) - (zY : Y z) - (oY : Y o) - (sY : PathOver Y s zY oY) - -> I-ind Y zY oY sY o ↦ oY - {-# REWRITE I-ind-βo #-} - I-ind-βs : (Y : I -> Set) - (zY : Y z) - (oY : Y o) - (sY : PathOver Y s zY oY) - -> apd (I-ind Y zY oY sY) s == sY - -transp-cst : (A : Set) {x y : A} (B : Set) (p : x == y) (z : B) -> transport (\x -> B) p z == z -transp-cst A B idp z = idp - -transp-fun : (A B : Set) (a b : A) (p : a == b) (f : A -> B) -> transport (λ _ -> A -> B) p f == transport (λ _ -> B) p (f a) -transp-fun = ? - -fe : {A B : Set} (f g : A -> B) -> ( (x : A) -> f x == g x) -> f == g -fe {A} {B} f g p = - ap - (I-ind (λ _ → (x : A) → B) f g - (from-transp (λ _ → (x : A) → B) s ( - {!!} - ))) - s diff --git a/Agda-HITs/Mod2/Mod2.agda b/Agda-HITs/Mod2/Mod2.agda deleted file mode 100644 index 799d653..0000000 --- a/Agda-HITs/Mod2/Mod2.agda +++ /dev/null @@ -1,59 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT - -module Mod2 where - -private - data M' : Set where - Zero : M' - S : M' -> M' - -M : Set -M = M' - -z : M -z = Zero - -Succ : M -> M -Succ = S - -postulate - mod : (n : M) -> n == Succ(Succ n) - trunc : is-set M - -M-ind : (C : M -> Set) - -> (a : C Zero) - -> (sC : (x : M) -> C x -> C (S x)) - -> (p : (n : M) (c : C n) -> PathOver C (mod n) c (sC (Succ n) (sC n c))) - -> (t : (m : M) -> is-set (C m)) - -> (x : M) -> C x -M-ind C a sC _ t Zero = a -M-ind C a sC p t (S x) = sC x (M-ind C a sC p t x) - -postulate - M-ind-βmod : (C : M -> Set) - -> (a : C Zero) - -> (sC : (x : M) -> C x -> C (S x)) - -> (p : (n : M) (c : C n) -> PathOver C (mod n) c (sC (Succ n) (sC n c))) - -> (t : (m : M) -> is-set (C m)) - -> (n : M) - -> apd (M-ind C a sC p t) (mod n) == p n (M-ind C a sC p t n) - -M-rec : {C : Set} - -> (a : C) - -> (sC : C -> C) - -> (p : (c : C) -> c == sC (sC c)) - -> (t : is-set C) - -> M -> C -M-rec a sC _ _ Zero = a -M-rec a sC p t (S x) = sC (M-rec a sC p t x) - -postulate - M-rec-βmod : {C : Set} - -> (a : C) - -> (sC : C -> C) - -> (p : (c : C) -> c == sC (sC c)) - -> (t : is-set C) - -> (n : M) - -> ap (M-rec a sC p t) (mod n) == p (M-rec a sC p t n) diff --git a/Agda-HITs/Mod2/Thms.agda b/Agda-HITs/Mod2/Thms.agda deleted file mode 100644 index 775dc32..0000000 --- a/Agda-HITs/Mod2/Thms.agda +++ /dev/null @@ -1,113 +0,0 @@ -{-# OPTIONS --without-K --rewriting #-} - -open import HoTT -open import Mod2 - -module Thms where - -paths_set : (A B : Set) (m : is-set B) (f g : A -> B) (a : A) -> is-set (f a == g a) -paths_set A B m f g a = \c₁ c₂ q₁ q₂ -> - prop-has-level-S - (contr-is-prop (m (f a) (g a) c₁ c₂)) - q₁ - q₂ - -trunc_paths : (A : Set) (Y : A -> Set) {x y : A} (p : x == y) (t : is-prop (Y x)) (c₁ : Y x) (c₂ : Y y) -> PathOver Y p c₁ c₂ -trunc_paths A Y p t c₁ c₂ = from-transp! Y p ((prop-has-all-paths t) c₁ (transport! Y p c₂)) - -plus : M -> M -> M -plus n = M-rec - n - Succ - mod - trunc - -plus_0n : (n : M) -> plus z n == n -plus_0n = M-ind - (\n -> plus z n == n) - idp - (\x -> \p -> ap Succ p) - (\x -> \c -> - trunc_paths M (\ n → plus z n == n) (mod x) (trunc (plus z x) x) c (ap Succ (ap Succ c)) - ) - (\m -> - paths_set M M trunc (\x -> plus z x) (\x -> x) m - ) - -plus_n0 : (n : M) -> plus n z == n -plus_n0 = M-ind - (\n -> plus n z == n) - idp - (\x p -> idp) - (\x c -> - trunc_paths M (\x -> plus x z == x) (mod x) (trunc x x) c idp - ) - (\m -> paths_set M M trunc (\x -> plus x z) (\x -> x) m ) - -plus_Sn : (n m : M) -> plus (Succ n) m == Succ (plus n m) -plus_Sn n = M-ind - (\m -> plus (Succ n) m == Succ (plus n m)) - idp - (\x p -> ap Succ p) - (\x c -> - trunc_paths M (\x -> plus (Succ n) x == Succ (plus n x)) (mod x) (trunc (plus (Succ n) x) (Succ (plus n x))) c (ap Succ (ap Succ c)) - ) - (\m -> paths_set M M trunc (\x -> plus (Succ x) m) (\x -> Succ(plus x m)) n) - -plus_nS : (n m : M) -> plus n (Succ m) == Succ (plus n m) -plus_nS n m = idp - -not : Bool -> Bool -not true = false -not false = true - -not-not : (x : Bool) -> x == not (not x) -not-not true = idp -not-not false = idp - -toBool : M -> Bool -toBool = M-rec - true - not - ((\x -> not-not x)) - Bool-is-set - -toBoolS : (n : M) -> toBool (Succ n) == not (toBool n) -toBoolS = M-ind - (\n -> toBool (Succ n) == not (toBool n)) - idp - (\x p -> idp) - (\n c -> - trunc_paths M (\x -> toBool (Succ x) == not (toBool x)) (mod n) (Bool-is-set (not (toBool n)) (not (toBool n))) c idp) - (\m -> paths_set M Bool Bool-is-set (\n -> toBool(Succ n)) (\n -> not(toBool n)) m) - -fromBool : Bool -> M -fromBool true = z -fromBool false = Succ z - -fromBoolNot : (b : Bool) -> fromBool (not b) == Succ (fromBool b) -fromBoolNot true = idp -fromBoolNot false = mod z - -iso₁ : (b : Bool) -> toBool (fromBool b) == b -iso₁ true = idp -iso₁ false = idp - -iso₂ : (n : M) -> fromBool (toBool n) == n -iso₂ = M-ind - (\n -> fromBool (toBool n) == n) - idp - (\x p -> - ap fromBool (toBoolS x) - ∙ fromBoolNot (toBool x) - ∙ ap Succ p) - (\n p -> trunc_paths M - (λ z₁ → fromBool (toBool z₁) == z₁) - (mod n) - (trunc (fromBool (toBool n)) n) - p - (ap fromBool (toBoolS (Succ n)) - ∙ fromBoolNot (toBool (Succ n)) - ∙ ap Succ (ap fromBool (toBoolS n) ∙ fromBoolNot (toBool n) ∙ ap Succ p)) - ) - (\m -> paths_set M M trunc (\n -> fromBool (toBool n)) (\n -> n) m) diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject index d7c3a24..f758dc6 100644 --- a/FiniteSets/_CoqProject +++ b/FiniteSets/_CoqProject @@ -18,6 +18,7 @@ fsets/monad.v FSets.v Sub.v representations/T.v +implementations/interface.v implementations/lists.v variations/enumerated.v variations/k_finite.v diff --git a/FiniteSets/implementations/interface.v b/FiniteSets/implementations/interface.v new file mode 100644 index 0000000..5c7afe0 --- /dev/null +++ b/FiniteSets/implementations/interface.v @@ -0,0 +1,43 @@ +Require Import HoTT. +Require Import FSets. + +Section structure. + Variable (T : Type -> Type). + + Class hasMembership : Type := + member : forall A : Type, A -> T A -> hProp. + + Class hasEmpty : Type := + empty : forall A, T A. + + Class hasSingleton : Type := + singleton : forall A, A -> T A. + + Class hasUnion : Type := + union : forall A, T A -> T A -> T A. + + Class hasComprehension : Type := + filter : forall A, (A -> Bool) -> T A -> T A. +End structure. + +Arguments member {_} {_} {_} _ _. +Arguments empty {_} {_} {_}. +Arguments singleton {_} {_} {_} _. +Arguments union {_} {_} {_} _ _. +Arguments filter {_} {_} {_} _ _. + +Section interface. + Context `{Univalence}. + Variable (T : Type -> Type) + (f : forall A, T A -> FSet A). + Context `{hasMembership T, hasEmpty T, hasSingleton T, hasUnion T, hasComprehension T}. + + Class sets := + { + f_empty : forall A, f A empty = E ; + f_singleton : forall A a, f A (singleton a) = L a; + f_union : forall A X Y, f A (union X Y) = U (f A X) (f A Y); + f_filter : forall A ϕ X, f A (filter ϕ X) = comprehension ϕ (f A X); + f_member : forall A a X, member a X = isIn a (f A X) + }. +End interface. \ No newline at end of file diff --git a/FiniteSets/implementations/lists.v b/FiniteSets/implementations/lists.v index 2994b41..37328e8 100644 --- a/FiniteSets/implementations/lists.v +++ b/FiniteSets/implementations/lists.v @@ -1,113 +1,69 @@ (* Implementation of [FSet A] using lists *) Require Import HoTT HitTactics. -Require Import representations.cons_repr FSets. -From fsets Require Import operations_cons_repr isomorphism length. +Require Import FSets implementations.interface. Section Operations. - Variable A : Type. - Context {A_deceq : DecidablePaths A}. + Context `{Univalence}. + + Global Instance list_empty : hasEmpty list := fun A => nil. + + Global Instance list_single : hasSingleton list := fun A a => cons a nil. - Fixpoint member (l : list A) (a : A) : Bool := + Global Instance list_union : hasUnion list. + Proof. + intros A l1 l2. + induction l1. + * apply l2. + * apply (cons a IHl1). + Defined. + + Global Instance list_membership : hasMembership list. + Proof. + intros A. + intros a l. + induction l as [ | b l IHl]. + - apply False_hp. + - apply (hor (a = b) IHl). + Defined. + + Global Instance list_comprehension : hasComprehension list. + Proof. + intros A ϕ l. + induction l as [ | b l IHl]. + - apply nil. + - apply (if ϕ b then cons b IHl else IHl). + Defined. + + Fixpoint list_to_set A (l : list A) : FSet A := match l with - | nil => false - | cons b l => if (dec (a = b)) then true else member l a - end. - - Fixpoint append (l1 l2 : list A) := - match l1 with - | nil => l2 - | cons a l => cons a (append l l2) - end. - - Definition empty : list A := nil. - - Definition singleton (a : A) : list A := cons a nil. - - Fixpoint filter (ϕ : A -> Bool) (l : list A) : list A := - match l with - | nil => nil - | cons a l => if ϕ a then cons a (filter ϕ l) else filter ϕ l - end. - - Fixpoint cardinality (l : list A) : nat := - match l with - | nil => 0 - | cons a l => if member l a then cardinality l else 1 + cardinality l + | nil => E + | cons a l => U (L a) (list_to_set A l) end. End Operations. -Arguments nil {_}. -Arguments cons {_} _ _. -Arguments member {_} {_} _ _. -Arguments singleton {_} _. -Arguments append {_} _ _. -Arguments empty {_}. -Arguments filter {_} _ _. -Arguments cardinality {_} {_} _. - Section ListToSet. Variable A : Type. - Context {A_deceq : DecidablePaths A} `{Univalence}. + Context `{Univalence}. + + Lemma member_isIn (a : A) (l : list A) : + member a l = isIn a (list_to_set A l). + Proof. + induction l ; unfold member in * ; simpl in *. + - reflexivity. + - rewrite IHl. + unfold hor, merely, lor. + apply path_iff_hprop ; intros z ; strip_truncations ; destruct z as [z1 | z2]. + * apply (tr (inl (tr z1))). + * apply (tr (inr z2)). + * strip_truncations ; apply (tr (inl z1)). + * apply (tr (inr z2)). + Defined. - Fixpoint list_to_setC (l : list A) : FSetC A := - match l with - | nil => Nil - | cons a l => Cns a (list_to_setC l) - end. + Definition empty_empty : list_to_set A empty = E := idpath. - Definition list_to_set (l : list A) := FSetC_to_FSet(list_to_setC l). - - Lemma list_to_setC_surj : forall X : FSetC A, Trunc (-1) ({l : list A & list_to_setC l = X}). - Proof. - hrecursion ; try (intros ; apply hprop_allpath ; apply (istrunc_truncation (-1) _)). - - apply tr ; exists nil ; cbn. reflexivity. - - intros a x P. - simple refine (Trunc_rec _ P). - intros [l Q]. - apply tr. - exists (cons a l). - simpl. - apply (ap (fun y => a;;y) Q). - Defined. - - Lemma member_isIn (l : list A) (a : A) : - member l a = isIn_b a (FSetC_to_FSet (list_to_setC l)). - Proof. - induction l ; cbn in *. - - reflexivity. - - destruct (dec (a = a0)) ; cbn. - * rewrite ?p. simplify_isIn. reflexivity. - * rewrite IHl. simplify_isIn. rewrite L_isIn_b_false ; auto. - Defined. - - Lemma append_FSetCappend (l1 l2 : list A) : - list_to_setC (append l1 l2) = operations_cons_repr.append (list_to_setC l1) (list_to_setC l2). - Proof. - induction l1 ; simpl in *. - - reflexivity. - - apply (ap (fun y => a ;; y) IHl1). - Defined. - - Lemma append_FSetappend (l1 l2 : list A) : - list_to_set (append l1 l2) = U (list_to_set l1) (list_to_set l2). - Proof. - induction l1 ; cbn in *. - - symmetry. apply nl. - - rewrite <- assoc. - refine (ap (fun y => U {|a|} y) _). - rewrite <- append_union. - rewrite <- append_FSetCappend. - reflexivity. - Defined. - - Lemma empty_empty : list_to_set empty = E. - Proof. - reflexivity. - Defined. - - Lemma filter_comprehension (l : list A) (ϕ : A -> Bool) : - list_to_set (filter ϕ l) = comprehension ϕ (list_to_set l). + Lemma filter_comprehension (ϕ : A -> Bool) (l : list A) : + list_to_set A (filter ϕ l) = comprehension ϕ (list_to_set A l). Proof. induction l ; cbn in *. - reflexivity. @@ -118,32 +74,33 @@ Section ListToSet. apply IHl. Defined. - Lemma length_sizeC (l : list A) : - cardinality l = length (list_to_setC l). + Definition singleton_single (a : A) : list_to_set A (singleton a) = L a := + nr (L a). + + Lemma append_union (l1 l2 : list A) : + list_to_set A (union l1 l2) = U (list_to_set A l1) (list_to_set A l2). Proof. - induction l. - - cbn. - reflexivity. - - simpl. - rewrite IHl. - rewrite member_isIn. - reflexivity. + induction l1 ; induction l2 ; cbn. + - apply (union_idem _)^. + - apply (nl _)^. + - rewrite IHl1. + apply assoc. + - rewrite IHl1. + cbn. + apply assoc. Defined. +End ListToSet. - Lemma length_size (l : list A) : - cardinality l = length_FSet (list_to_set l). +Section lists_are_sets. + Context `{Univalence}. + + Instance lists_sets : sets list list_to_set. Proof. - unfold length_FSet. - unfold list_to_set. - rewrite repr_iso_id_r. - apply length_sizeC. + split ; intros. + - apply empty_empty. + - apply singleton_single. + - apply append_union. + - apply filter_comprehension. + - apply member_isIn. Defined. - - Lemma singleton_single (a : A) : - list_to_set (singleton a) = L a. - Proof. - cbn. - apply nr. - Defined. - -End ListToSet. \ No newline at end of file +End lists_are_sets.