1 files changed, 140 insertions, 0 deletions
diff --git a/src/Thinned.idr b/src/Thinned.idr
new file mode 100644
index 0000000..7f5d2ac
--- /dev/null
+++ b/src/Thinned.idr
@@ -0,0 +1,140 @@
+module Thinned
+
+import Control.Order
+import Control.Relation
+
+import public Thinning
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+||| Data embedded in a wider context via a thinning.
+public export
+record Thinned (t : SnocList a -> Type) (sx : SnocList a) where
+  constructor Over
+  {0 support : SnocList a}
+  value : t support
+  thin : support `Thins` sx
+
+%name Thinned v, u
+
+||| An equivalence relation on thinned objects.
+public export
+data (<~>) : Thinned t sx -> Thinned t sx -> Type where
+  UpToThin :
+    {0 v : t sx} ->
+    {0 thin1, thin2 : sx `Thins` sy} ->
+    thin1 <~> thin2 ->
+    (<~>) {t} (v `Over` thin1) (v `Over` thin2)
+
+%name Thinned.(<~>) prf
+
+export (.supportPrf) :
+  {0 v, u : Thinned t sx} ->
+  v <~> u ->
+  v.support = u.support
+(UpToThin prf) .supportPrf = Refl
+
+export (.valuePrf) :
+  {0 v, u : Thinned t sx} ->
+  (e : v <~> u) ->
+  v.value = (rewrite e.supportPrf in u.value)
+(UpToThin prf) .valuePrf = Refl
+
+export (.thinPrf) :
+  {0 v, u : Thinned t sx} ->
+  (e : v <~> u) ->
+  v.thin <~> (rewrite e.supportPrf in u.thin)
+(UpToThin prf) .thinPrf = prf
+
+--- Properties
+
+export
+irrelevantEquiv :
+  {0 v, u : Thinned t sx} ->
+  (0 prf : v <~> u) ->
+  v <~> u
+irrelevantEquiv {v = v `Over` thin1, u = u `Over` thin2} prf =
+  rewrite prf.supportPrf in
+  rewrite prf.valuePrf in
+  UpToThin (rewrite sym prf.supportPrf in irrelevantEquiv prf.thinPrf)
+
+export
+Reflexive (Thinned t sx) (<~>) where
+  reflexive {x = t `Over` thin} = UpToThin reflexive
+
+export
+Symmetric (Thinned t sx) (<~>) where
+  symmetric (UpToThin prf) = UpToThin (symmetric prf)
+
+export
+Transitive (Thinned t sx) (<~>) where
+  transitive (UpToThin prf1) (UpToThin prf2) = UpToThin (transitive prf1 prf2)
+
+export
+Equivalence (Thinned t sx) (<~>) where
+
+export
+Preorder (Thinned t sx) (<~>) where
+
+-- Operations ------------------------------------------------------------------
+
+||| Map the underlying value.
+public export
+map : (forall sx. t sx -> u sx) -> Thinned t sx -> Thinned u sx
+map f (value `Over` thin) = f value `Over` thin
+
+||| Weaken the surrounding context.
+public export
+wkn : Thinned t sx -> sx `Thins` sy -> Thinned t sy
+wkn (value `Over` thin') thin = value `Over` thin . thin'
+
+||| Shift the surrounding context.
+public export
+shift : Thinned t sx -> Thinned t (sx :< x)
+shift (value `Over` thin) = value `Over` Drop thin
+
+--- Properties
+
+export
+mapCong :
+  {0 t, u : SnocList a -> Type} ->
+  (0 f : forall sx. t sx -> u sx) ->
+  {0 v1, v2 : Thinned t sx} ->
+  v1 <~> v2 ->
+  map f v1 <~> map f v2
+mapCong f (UpToThin prf) = UpToThin prf
+
+export
+shiftCong : {0 v, u : Thinned t sx} -> v <~> u -> shift v <~> shift u
+shiftCong (UpToThin prf) = UpToThin (dropCong prf)
+
+-- Pairs -----------------------------------------------------------------------
+
+||| Product of two values ensuring the whole context is used.
+public export
+record Pair (t, u : SnocList a -> Type) (sx : SnocList a) where
+  constructor MakePair
+  fst : Thinned t sx
+  snd : Thinned u sx
+  0 cover : Covering fst.thin snd.thin
+
+||| Smart constructor for thinned pairs.
+export
+MkPair : Thinned t sx -> Thinned u sx -> Thinned (Pair t u) sx
+MkPair (v `Over` thin1) (u `Over` thin2) =
+  let cp = coprod thin1 thin2 in
+  MakePair (v `Over` cp.thin1') (u `Over` cp.thin2') cp.cover `Over` cp.factor
+
+--- Properties
+
+export
+mkPairCong :
+  {0 v1, w1 : Thinned t sx} ->
+  {0 v2, w2 : Thinned u sx} ->
+  v1 <~> w1 ->
+  v2 <~> w2 ->
+  MkPair v1 v2 <~> MkPair w1 w2
+mkPairCong (UpToThin prf1) (UpToThin prf2) =
+  ?mkPairCong_rhs_1