diff --git a/Agda-HITs/CL/CL.agda b/Agda-HITs/CL/CL.agda
new file mode 100644
index 0000000..5e8570c
--- /dev/null
+++ b/Agda-HITs/CL/CL.agda
@@ -0,0 +1,98 @@
+{-# 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
new file mode 100644
index 0000000..b995c5d
--- /dev/null
+++ b/Agda-HITs/CL/Thms.agda
@@ -0,0 +1,122 @@
+{-# 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
new file mode 100644
index 0000000..1e3e41f
--- /dev/null
+++ b/Agda-HITs/Expressions/Expressions.agda
@@ -0,0 +1,59 @@
+{-# 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
new file mode 100644
index 0000000..c5eb14a
--- /dev/null
+++ b/Agda-HITs/Expressions/Thms.agda
@@ -0,0 +1,16 @@
+{-# 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
new file mode 100644
index 0000000..9efdaa4
--- /dev/null
+++ b/Agda-HITs/Imperative/Language.agda
@@ -0,0 +1,32 @@
+{-# 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
new file mode 100644
index 0000000..8ab4fef
--- /dev/null
+++ b/Agda-HITs/Imperative/Semantics.agda
@@ -0,0 +1,18 @@
+{-# 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
new file mode 100644
index 0000000..d70a487
--- /dev/null
+++ b/Agda-HITs/Imperative/Syntax.agda
@@ -0,0 +1,66 @@
+{-# 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
new file mode 100644
index 0000000..f7db3ec
--- /dev/null
+++ b/Agda-HITs/Integers/Integers.agda
@@ -0,0 +1,63 @@
+{-# 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
new file mode 100644
index 0000000..b465ae4
--- /dev/null
+++ b/Agda-HITs/Integers/Thms.agda
@@ -0,0 +1,205 @@
+{-# 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
new file mode 100644
index 0000000..61f61cb
--- /dev/null
+++ b/Agda-HITs/Interval/Interval.agda
@@ -0,0 +1,49 @@
+{-# 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
new file mode 100644
index 0000000..799d653
--- /dev/null
+++ b/Agda-HITs/Mod2/Mod2.agda
@@ -0,0 +1,59 @@
+{-# 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
new file mode 100644
index 0000000..775dc32
--- /dev/null
+++ b/Agda-HITs/Mod2/Thms.agda
@@ -0,0 +1,113 @@
+{-# 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)