diff options
Diffstat (limited to 'src/Thinning.idr')
| -rw-r--r-- | src/Thinning.idr | 566 |
1 files changed, 331 insertions, 235 deletions
diff --git a/src/Thinning.idr b/src/Thinning.idr index d2d65df..1ba5eb0 100644 --- a/src/Thinning.idr +++ b/src/Thinning.idr @@ -1,246 +1,187 @@ +||| A setoid of context thinnings. module Thinning -import Data.Singleton -import Data.SnocList.Elem +import Control.Order +import Control.Relation +import Data.Either +import Data.Nat +import Syntax.PreorderReasoning + +import public Data.SnocList.Elem %prefix_record_projections off +infix 4 <~> + -- Definition ------------------------------------------------------------------ +||| An injective, order-preserving map from one context to another. public export data Thins : SnocList a -> SnocList a -> Type where - Empty : [<] `Thins` [<] - Drop : sx `Thins` sy -> sx `Thins` sy :< z - Keep : - (thin : sx `Thins` sy) -> - sx :< z `Thins` sy :< z + ||| Identity map. + Id : sx `Thins` sx + ||| Empty map. + Empty : [<] `Thins` sx + ||| Skips over an element in the target context. + Drop : sx `Thins` sy -> sx `Thins` sy :< y + ||| Extends both contexts with a new element. + Keep : sx `Thins` sy -> sx :< z `Thins` sy :< z %name Thins thin --- Utility --------------------------------------------------------------------- - -public export -data Len : SnocList a -> Type where - Z : Len [<] - S : Len sx -> Len (sx :< x) - -%name Len k, m, n - -%hint -public export -length : (sx : SnocList a) -> Len sx -length [<] = Z -length (sx :< x) = S (length sx) - -%hint +||| Apply a thinning to an element of the source context. export -lenAppend : Len sx -> Len sy -> Len (sx ++ sy) -lenAppend k Z = k -lenAppend k (S m) = S (lenAppend k m) - -%hint -public export -lenPred : Len (sx :< x) -> Len sx -lenPred (S k) = k - -export -Cast (Len sx) Nat where - cast Z = 0 - cast (S k) = S (cast k) - --- Smart Constructors ---------------------------------------------------------- - -export -empty : (len : Len sx) => [<] `Thins` sx -empty {len = Z} = Empty -empty {len = S k} = Drop empty - -public export -id : (len : Len sx) => sx `Thins` sx -id {len = Z} = Empty -id {len = S k} = Keep id - -public export -point : Len sx => Elem ty sx -> [<ty] `Thins` sx -point Here = Keep empty -point (There i) = Drop (point i) - --- Operations ------------------------------------------------------------------ - -public export -index : sx `Thins` sy -> Elem z sx -> Elem z sy +index : sx `Thins` sy -> Elem x sx -> Elem x sy +index Id i = i index (Drop thin) i = There (index thin i) index (Keep thin) Here = Here index (Keep thin) (There i) = There (index thin i) +||| An equivalence relation on thinnings. Two thinnings are equal if they have +||| the same action on elements. public export -(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz -Empty . thin1 = thin1 -Drop thin2 . thin1 = Drop (thin2 . thin1) -Keep thin2 . Drop thin1 = Drop (thin2 . thin1) -Keep thin2 . Keep thin1 = Keep (thin2 . thin1) +record (<~>) (thin1, thin2 : sx `Thins` sy) where + constructor MkEquivalence + equiv : forall x. (i : Elem x sx) -> index thin1 i = index thin2 i -export -(++) : sx `Thins` sy -> sz `Thins` sw -> sx ++ sz `Thins` sy ++ sw -thin2 ++ Empty = thin2 -thin2 ++ (Drop thin1) = Drop (thin2 ++ thin1) -thin2 ++ (Keep thin1) = Keep (thin2 ++ thin1) +%name (<~>) prf --- Commuting Triangles and Coverings ------------------------------------------- +--- Properties -data Triangle : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz -> Type where - EmptyAny : Triangle Empty thin1 thin1 - DropAny : Triangle thin2 thin1 thin -> Triangle (Drop thin2) thin1 (Drop thin) - KeepDrop : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Drop thin1) (Drop thin) - KeepKeep : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Keep thin1) (Keep thin) +-- Relational -public export -data Overlap = Covers | Partitions +export +irrelevantEquiv : + {0 thin1, thin2 : sx `Thins` sy} -> + (0 prf : thin1 <~> thin2) -> + thin1 <~> thin2 +irrelevantEquiv prf = MkEquivalence (\i => irrelevantEq $ prf.equiv i) -namespace Covering - public export - data Covering : Overlap -> sx `Thins` sz -> sy `Thins` sz -> Type where - EmptyEmpty : Covering ov Empty Empty - DropKeep : Covering ov thin1 thin2 -> Covering ov (Drop thin1) (Keep thin2) - KeepDrop : Covering ov thin1 thin2 -> Covering ov (Keep thin1) (Drop thin2) - KeepKeep : Covering Covers thin1 thin2 -> Covering Covers (Keep thin1) (Keep thin2) +export +Reflexive (sx `Thins` sy) (<~>) where + reflexive = MkEquivalence (\i => Refl) -public export -record Coproduct {sx, sy, sz : SnocList a} (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where - constructor MkCoprod - {0 sw : SnocList a} - {thin1' : sx `Thins` sw} - {thin2' : sy `Thins` sw} - {thin : sw `Thins` sz} - 0 left : Triangle thin thin1' thin1 - 0 right : Triangle thin thin2' thin2 - 0 cover : Covering Covers thin1' thin2' +export +Symmetric (sx `Thins` sy) (<~>) where + symmetric prf = MkEquivalence (\i => sym $ prf.equiv i) export -coprod : (thin1 : sx `Thins` sz) -> (thin2 : sy `Thins` sz) -> Coproduct thin1 thin2 -coprod Empty Empty = MkCoprod EmptyAny EmptyAny EmptyEmpty -coprod (Drop thin1) (Drop thin2) = - { left $= DropAny, right $= DropAny } (coprod thin1 thin2) -coprod (Drop thin1) (Keep thin2) = - { left $= KeepDrop, right $= KeepKeep, cover $= DropKeep } (coprod thin1 thin2) -coprod (Keep thin1) (Drop thin2) = - { left $= KeepKeep, right $= KeepDrop, cover $= KeepDrop } (coprod thin1 thin2) -coprod (Keep thin1) (Keep thin2) = - { left $= KeepKeep, right $= KeepKeep, cover $= KeepKeep } (coprod thin1 thin2) +Transitive (sx `Thins` sy) (<~>) where + transitive prf1 prf2 = MkEquivalence (\i => trans (prf1.equiv i) (prf2.equiv i)) --- Splitting off Contexts ------------------------------------------------------ +export +Equivalence (sx `Thins` sy) (<~>) where -public export -data Split : (global, local : SnocList a) -> (thin : sx `Thins` global ++ local) -> Type where - MkSplit : - (thin2 : sx `Thins` global) -> - (thin1 : used `Thins` local) -> - Split global local (thin2 ++ thin1) +export +Preorder (sx `Thins` sy) (<~>) where -public export -split : Len local -> (thin : sx `Thins` global ++ local) -> Split global local thin -split Z thin = MkSplit thin Empty -split (S k) (Drop thin) with (split k thin) - split (S k) (Drop .(thin2 ++ thin1)) | MkSplit thin2 thin1 = MkSplit thin2 (Drop thin1) -split (S k) (Keep thin) with (split k thin) - split (S k) (Keep .(thin2 ++ thin1)) | MkSplit thin2 thin1 = MkSplit thin2 (Keep thin1) +export +dropCong : thin1 <~> thin2 -> Drop thin1 <~> Drop thin2 +dropCong prf = MkEquivalence (\i => cong There $ prf.equiv i) --- Thinned Things -------------------------------------------------------------- +export +keepCong : thin1 <~> thin2 -> Keep thin1 <~> Keep thin2 +keepCong prf = MkEquivalence + (\i => + case i of + Here => Refl + There i => cong There $ prf.equiv i) -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 +-- Indexing -public export -record OverlapPair (overlap : Overlap) (T, U : SnocList a -> Type) (sx : SnocList a) where - constructor MakePair - left : Thinned T sx - right : Thinned U sx - 0 cover : Covering overlap left.thin right.thin +export +indexId : (i : Elem x sx) -> index Id i = i +indexId i = Refl -public export -Pair : (T, U : SnocList a -> Type) -> SnocList a -> Type -Pair = OverlapPair Covers +export +indexDrop : + (thin : sx `Thins` sy) -> + (i : Elem x sx) -> + index (Drop thin) i = There (index thin i) +indexDrop thin i = Refl -public export -MkPair : Thinned t sx -> Thinned u sx -> Thinned (OverlapPair Covers t u) sx -MkPair (t `Over` thin1) (u `Over` thin2) = - let cp = coprod thin1 thin2 in - MakePair (t `Over` cp.thin1') (u `Over` cp.thin2') cp.cover `Over` cp.thin +export +indexKeepHere : (thin : sx `Thins` sy) -> index (Keep thin) Here = Here +indexKeepHere thin = Refl -public export -record Binds (local : SnocList a) (T : SnocList a -> Type) (sx : SnocList a) where - constructor MakeBound - {0 used : SnocList a} - value : T (sx ++ used) - thin : used `Thins` local +export +indexKeepThere : + (thin : sx `Thins` sy) -> + (i : Elem x sx) -> + index (Keep thin) (There i) = There (index thin i) +indexKeepThere thin i = Refl -public export -MkBound : Len local -> Thinned t (sx ++ local) -> Thinned (Binds local t) sx -MkBound k (value `Over` thin) with (split k thin) - MkBound k (value `Over` .(thin2 ++ thin1)) | MkSplit thin2 thin1 = - MakeBound value thin1 `Over` thin2 +-- Other -public export -map : (forall ctx. t ctx -> u ctx) -> Thinned t ctx -> Thinned u ctx -map f (value `Over` thin) = f value `Over` thin +thinToEmpty : sx `Thins` [<] -> sx = [<] +thinToEmpty Id = Refl +thinToEmpty Empty = Refl -public export -drop : Thinned t sx -> Thinned t (sx :< x) -drop (value `Over` thin) = value `Over` Drop thin +0 thinLen : sx `Thins` sy -> length sx `LTE` length sy +thinLen Id = reflexive +thinLen Empty = LTEZero +thinLen (Drop thin) = lteSuccRight (thinLen thin) +thinLen (Keep thin) = LTESucc (thinLen thin) -public export -wkn : Thinned t sx -> sx `Thins` sy -> Thinned t sy -wkn (value `Over` thin) thin' = value `Over` thin' . thin +idUnique' : (thin : sx `Thins` sx) -> (i : Elem x sx) -> index thin i = i +idUnique' Id i = Refl +idUnique' (Drop thin) i = void $ LTEImpliesNotGT (thinLen thin) reflexive +idUnique' (Keep thin) Here = Refl +idUnique' (Keep thin) (There i) = cong There $ idUnique' thin i --- Properties ------------------------------------------------------------------ +export +idUnique : (thin1, thin2 : sx `Thins` sx) -> thin1 <~> thin2 +idUnique thin1 thin2 = + MkEquivalence + (\i => trans (idUnique' thin1 i) (sym $ idUnique' thin2 i)) export -lenUnique : (k, m : Len sx) -> k = m -lenUnique Z Z = Refl -lenUnique (S k) (S m) = cong S (lenUnique k m) +emptyUnique : (thin1, thin2 : [<] `Thins` sx) -> thin1 <~> thin2 +emptyUnique thin1 thin2 = MkEquivalence (\i => absurd i) +-- Smart Constructors ---------------------------------------------------------- + +||| Point map. The representable thinning of an element. export -emptyUnique : (thin1, thin2 : [<] `Thins` sx) -> thin1 = thin2 -emptyUnique Empty Empty = Refl -emptyUnique (Drop thin1) (Drop thin2) = cong Drop (emptyUnique thin1 thin2) +Point : Elem x sx -> [<x] `Thins` sx +Point Here = Keep Empty +Point (There i) = Drop (Point i) export -identityLeft : (len : Len sy) => (thin : sx `Thins` sy) -> id @{len} . thin = thin -identityLeft {len = Z} thin = Refl -identityLeft {len = S k} (Drop thin) = cong Drop (identityLeft thin) -identityLeft {len = S k} (Keep thin) = cong Keep (identityLeft thin) +indexPoint : (i : Elem x sx) -> index (Point i) Here = i +indexPoint Here = Refl +indexPoint (There i) = cong There $ indexPoint i export -identityRight : (len : Len sx) => (thin : sx `Thins` sy) -> thin . id @{len} = thin -identityRight {len = Z} Empty = Refl -identityRight (Drop thin) = cong Drop (identityRight thin) -identityRight {len = S k} (Keep thin) = cong Keep (identityRight thin) +pointCong : {0 i, j : Elem x sx} -> i = j -> Point i <~> Point j +pointCong prf = MkEquivalence (\Here => cong (\i => index (Point i) Here) prf) export -identitySquared : (len : Len sx) -> id @{len} . id @{len} = id @{len} -identitySquared Z = Refl -identitySquared (S k) = cong Keep (identitySquared k) +dropPoint : (i : Elem x sx) -> Drop (Point i) <~> Point (There i) +dropPoint i = MkEquivalence (\Here => Refl) export -assoc : - (thin3 : sz `Thins` sw) -> - (thin2 : sy `Thins` sz) -> - (thin1 : sx `Thins` sy) -> - thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1 -assoc Empty thin2 thin1 = Refl -assoc (Drop thin3) thin2 thin1 = cong Drop (assoc thin3 thin2 thin1) -assoc (Keep thin3) (Drop thin2) thin1 = cong Drop (assoc thin3 thin2 thin1) -assoc (Keep thin3) (Keep thin2) (Drop thin1) = cong Drop (assoc thin3 thin2 thin1) -assoc (Keep thin3) (Keep thin2) (Keep thin1) = cong Keep (assoc thin3 thin2 thin1) +keepEmptyIsPoint : Keep Empty <~> Point Here +keepEmptyIsPoint = MkEquivalence (\Here => Refl) +-- Operations ------------------------------------------------------------------ + +||| Composition of two thinnings. export -indexId : (len : Len sx) => (i : Elem x sx) -> index (id @{len}) i = i -indexId {len = S k} Here = Refl -indexId {len = S k} (There i) = cong There (indexId i) +(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz +Id . thin1 = thin1 +Empty . Id = Empty +Empty . Empty = Empty +Drop thin2 . Id = Drop thin2 +Drop thin2 . Empty = Empty +Drop thin2 . Drop thin1 = Drop (thin2 . Drop thin1) +Drop thin2 . Keep thin1 = Drop (thin2 . Keep thin1) +Keep thin2 . Id = Keep thin2 +Keep thin2 . Empty = Empty +Keep thin2 . Drop thin1 = Drop (thin2 . thin1) +Keep thin2 . Keep thin1 = Keep (thin2 . thin1) + +--- Properties export indexHomo : @@ -248,69 +189,224 @@ indexHomo : (thin1 : sx `Thins` sy) -> (i : Elem x sx) -> index thin2 (index thin1 i) = index (thin2 . thin1) i +indexHomo Id thin1 i = Refl +indexHomo Empty Id i impossible indexHomo Empty Empty i impossible -indexHomo (Drop thin2) thin1 i = cong There (indexHomo thin2 thin1 i) -indexHomo (Keep thin2) (Drop thin1) i = cong There (indexHomo thin2 thin1 i) +indexHomo (Drop thin2) Id i = Refl +indexHomo (Drop thin2) (Drop thin1) i = cong There $ indexHomo thin2 (Drop thin1) i +indexHomo (Drop thin2) (Keep thin1) i = cong There $ indexHomo thin2 (Keep thin1) i +indexHomo (Keep thin2) Id i = Refl +indexHomo (Keep thin2) (Drop thin1) i = cong There $ indexHomo thin2 thin1 i indexHomo (Keep thin2) (Keep thin1) Here = Refl -indexHomo (Keep thin2) (Keep thin1) (There i) = cong There (indexHomo thin2 thin1 i) +indexHomo (Keep thin2) (Keep thin1) (There i) = cong There $ indexHomo thin2 thin1 i --- Objects +-- Categorical export -indexPoint : (len : Len sx) => (i : Elem x sx) -> index (point @{len} i) Here = i -indexPoint Here = Refl -indexPoint (There i) = cong There (indexPoint i) +identityLeft : (thin : sx `Thins` sy) -> Id . thin <~> thin +identityLeft thin = reflexive export -MkTriangle : - (thin2 : sy `Thins` sz) -> - (thin1 : sx `Thins` sy) -> - Triangle thin2 thin1 (thin2 . thin1) -MkTriangle Empty thin1 = EmptyAny -MkTriangle (Drop thin2) thin1 = DropAny (MkTriangle thin2 thin1) -MkTriangle (Keep thin2) (Drop thin1) = KeepDrop (MkTriangle thin2 thin1) -MkTriangle (Keep thin2) (Keep thin1) = KeepKeep (MkTriangle thin2 thin1) +identityRight : (thin : sx `Thins` sy) -> thin . Id <~> thin +identityRight Id = reflexive +identityRight Empty = reflexive +identityRight (Drop thin) = reflexive +identityRight (Keep thin) = reflexive export -triangleCorrect : Triangle thin2 thin1 thin -> thin2 . thin1 = thin -triangleCorrect EmptyAny = Refl -triangleCorrect (DropAny t) = cong Drop (triangleCorrect t) -triangleCorrect (KeepDrop t) = cong Drop (triangleCorrect t) -triangleCorrect (KeepKeep t) = cong Keep (triangleCorrect t) +assoc : + (thin3 : sz `Thins` sw) -> + (thin2 : sy `Thins` sz) -> + (thin1 : sx `Thins` sy) -> + thin3 . (thin2 . thin1) <~> (thin3 . thin2) . thin1 +assoc thin3 thin2 thin1 = MkEquivalence (\i => Calc $ + |~ index (thin3 . (thin2 . thin1)) i + ~~ index thin3 (index (thin2 . thin1) i) ..<(indexHomo thin3 (thin2 . thin1) i) + ~~ index thin3 (index thin2 (index thin1 i)) ..<(cong (index thin3) $ indexHomo thin2 thin1 i) + ~~ index (thin3 . thin2) (index thin1 i) ...(indexHomo thin3 thin2 (index thin1 i)) + ~~ index ((thin3 . thin2) . thin1) i ...(indexHomo (thin3 . thin2) thin1) i) -export -coprodEta : - {thin1 : sx `Thins` sz} -> - {thin2 : sy `Thins` sz} -> - (thin : sz `Thins` sw) -> - (cover : Covering Covers thin1 thin2) -> - coprod (thin . thin1) (thin . thin2) = - MkCoprod (MkTriangle thin thin1) (MkTriangle thin thin2) cover -coprodEta Empty EmptyEmpty = Refl -coprodEta (Drop thin) cover = rewrite coprodEta thin cover in Refl -coprodEta (Keep thin) (DropKeep cover) = rewrite coprodEta thin cover in Refl -coprodEta (Keep thin) (KeepDrop cover) = rewrite coprodEta thin cover in Refl -coprodEta (Keep thin) (KeepKeep cover) = rewrite coprodEta thin cover in Refl +-- Other export -dropIsWkn : (len : Len sx) => (v : Thinned t sx) -> drop {x} v = wkn v (Drop $ id @{len}) -dropIsWkn (value `Over` thin) = sym $ cong ((value `Over`) . Drop) $ identityLeft thin +dropLeft : + (thin2 : sy `Thins` sz) -> + (thin1 : sx `Thins` sy) -> + Drop thin2 . thin1 <~> Drop (thin2 . thin1) +dropLeft thin2 Id = symmetric $ dropCong $ identityRight thin2 +dropLeft thin2 Empty = emptyUnique Empty (Drop (thin2 . Empty)) +dropLeft thin2 (Drop thin1) = reflexive +dropLeft thin2 (Keep thin1) = reflexive export -wknId : (len : Len sx) => (v : Thinned t sx) -> wkn v (id @{len}) = v -wknId (value `Over` thin) = cong (value `Over`) $ identityLeft thin +keepDrop : + (thin2 : sy `Thins` sz) -> + (thin1 : sx `Thins` sy) -> + Keep thin2 . Drop thin1 <~> Drop (thin2 . thin1) +keepDrop thin2 thin1 = reflexive export -wknHomo : - (v : Thinned t sx) -> +keepHomo : (thin2 : sy `Thins` sz) -> (thin1 : sx `Thins` sy) -> - wkn (wkn v thin1) thin2 = wkn v (thin2 . thin1) -wknHomo (value `Over` thin) thin2 thin1 = cong (value `Over`) $ assoc thin2 thin1 thin + Keep thin2 . Keep thin1 <~> Keep (thin2 . thin1) +keepHomo thin2 thin1 = reflexive + +export +pointRight : + (thin : sx `Thins` sy) -> + (i : Elem x sx) -> + thin . Point i <~> Point (index thin i) +pointRight Id i = reflexive +pointRight (Drop thin) i = transitive (dropLeft thin (Point i)) (dropCong (pointRight thin i)) +pointRight (Keep thin) Here = keepCong (emptyUnique (thin . Empty) Empty) +pointRight (Keep thin) (There i) = dropCong (pointRight thin i) + +-- Coverings and Coproducts ---------------------------------------------------- -%hint +||| Proof that the thinnings are jointly surjective. +public export +record Covering (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where + constructor MkCovering + covers : + forall x. + (i : Elem x sz) -> + Either (j ** index thin1 j = i) (k ** index thin2 k = i) + +||| Unique thinning that factors into a covering. +public export +record Coproduct (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where + constructor MkCoproduct + {0 sw : SnocList _} + {thin1' : sx `Thins` sw} + {thin2' : sy `Thins` sw} + {factor : sw `Thins` sz} + 0 left : factor . thin1' <~> thin1 + 0 right : factor . thin2' <~> thin2 + 0 cover : Covering thin1' thin2' + +%name Covering cover +%name Coproduct cp + +--- Properties + +-- Coverings + +coverSym : Covering thin1 thin2 -> Covering thin2 thin1 +coverSym cover = MkCovering (\i => mirror $ cover.covers i) + +coverId : (0 thin : sx `Thins` sy) -> Covering Id thin +coverId thin = MkCovering (\i => Left (i ** Refl)) + +coverDropKeep : Covering thin1 thin2 -> Covering (Drop thin1) (Keep thin2) +coverDropKeep cover = MkCovering + (\i => case i of + Here => Right (Here ** Refl) + There i => case cover.covers i of + Left (j ** prf) => Left (j ** cong There prf) + Right (k ** prf) => Right (There k ** cong There prf)) + +coverKeepDrop : Covering thin1 thin2 -> Covering (Keep thin1) (Drop thin2) +coverKeepDrop cp = coverSym $ coverDropKeep $ coverSym cp + +coverKeepKeep : Covering thin1 thin2 -> Covering (Keep thin1) (Keep thin2) +coverKeepKeep cover = MkCovering + (\i => case i of + Here => Left (Here ** Refl) + There i => case cover.covers i of + Left (j ** prf) => Left (There j ** cong There prf) + Right (k ** prf) => Right (There k ** cong There prf)) + +-- Coproducts + +coprodSym : Coproduct thin1 thin2 -> Coproduct thin2 thin1 +coprodSym cp = MkCoproduct cp.right cp.left (coverSym cp.cover) + +coprodId : (thin : sx `Thins` sy) -> Coproduct Id thin +coprodId thin = + MkCoproduct + { thin1' = Id + , thin2' = thin + , factor = Id + , left = reflexive + , right = reflexive + , cover = coverId thin + } + +coprodEmpty : (thin : sx `Thins` sy) -> Coproduct Empty thin +coprodEmpty thin = + MkCoproduct + { thin1' = Empty + , thin2' = Id + , factor = thin + , left = emptyUnique (thin . Empty) Empty + , right = identityRight thin + , cover = coverSym $ coverId Empty + } + +||| Finds the coproduct of two thinnings. export -retractSingleton : Singleton sy -> sx `Thins` sy -> Singleton sx -retractSingleton s Empty = s -retractSingleton (Val (sy :< z)) (Drop thin) = retractSingleton (Val sy) thin -retractSingleton (Val (sy :< z)) (Keep thin) = pure (:< z) <*> retractSingleton (Val sy) thin +coprod : + (thin1 : sx `Thins` sz) -> + (thin2 : sy `Thins` sz) -> + Coproduct thin1 thin2 +coprod Id thin2 = coprodId thin2 +coprod Empty thin2 = coprodEmpty thin2 +coprod (Drop thin1) Id = coprodSym $ coprodId (Drop thin1) +coprod (Drop thin1) Empty = coprodSym $ coprodEmpty (Drop thin1) +coprod (Drop thin1) (Drop thin2) = + let cp = coprod thin1 thin2 in + MkCoproduct + { thin1' = cp.thin1' + , thin2' = cp.thin2' + , factor = Drop cp.factor + , left = transitive (dropLeft cp.factor cp.thin1') (dropCong cp.left) + , right = transitive (dropLeft cp.factor cp.thin2') (dropCong cp.right) + , cover = cp.cover + } +coprod (Drop thin1) (Keep thin2) = + let cp = coprod thin1 thin2 in + MkCoproduct + { thin1' = Drop cp.thin1' + , thin2' = Keep cp.thin2' + , factor = Keep cp.factor + , left = transitive (keepDrop cp.factor cp.thin1') (dropCong cp.left) + , right = transitive (keepHomo cp.factor cp.thin2') (keepCong cp.right) + , cover = coverDropKeep cp.cover + } +coprod (Keep thin1) Id = coprodSym $ coprodId (Keep thin1) +coprod (Keep thin1) Empty = coprodSym $ coprodEmpty (Keep thin1) +coprod (Keep thin1) (Drop thin2) = + let cp = coprod thin1 thin2 in + MkCoproduct + { thin1' = Keep cp.thin1' + , thin2' = Drop cp.thin2' + , factor = Keep cp.factor + , left = transitive (keepHomo cp.factor cp.thin1') (keepCong cp.left) + , right = transitive (keepDrop cp.factor cp.thin2') (dropCong cp.right) + , cover = coverKeepDrop cp.cover + } +coprod (Keep thin1) (Keep thin2) = + let cp = coprod thin1 thin2 in + MkCoproduct + { thin1' = Keep cp.thin1' + , thin2' = Keep cp.thin2' + , factor = Keep cp.factor + , left = transitive (keepHomo cp.factor cp.thin1') (keepCong cp.left) + , right = transitive (keepHomo cp.factor cp.thin2') (keepCong cp.right) + , cover = coverKeepKeep cp.cover + } + +-- Coproduct Equivalence ------------------------------------------------------- + +namespace Coproduct + public export + data (<~>) : + {0 thin1 : sx `Thins` sa} -> + {0 thin2 : sy `Thins` sa} -> + {0 thin3 : sz `Thins` sa} -> + {0 thin4 : sw `Thins` sa} -> + Coproduct thin1 thin2 -> + Coproduct thin3 thin4 -> + Type + where |