text:
{-# OPTIONS --without-K #-}
module semisimplicial where
  open import Agda.Primitive
  open import Data.Nat
  open import big-endian

  -- N-truncated, augmented semisimplicial types.
  -- Universe polymorphism has not been added yet
  -- (should be very easy, at the cost of even more bloat of type signatures).
  -- There is a canonical bijection between natural numbers (thought of in big-endian encoding) and
  -- simplices of Δ^∞. An *ideal* is a downward-closed set of simplices in this ordering.
  -- Each nontrivial ideal is principal, so the ideals are well-ordered by inclusion,
  -- or equivalently by looking at their last face (the generator of the ideal) and ordering as a natural number.
  -- Not every simplicial subset of a simplex is an ideal, but among the ideals are the simplices themselves
  -- (in binary, a simplex is 11...11), as well as the boundaries of simplices (11...10).
  -- The definition here defines an N-truncated, augmented semismplicial type X by starting with
  -- an N-1 -truncated, augmented semisimplicial type XUnd, and then inductively defining the set of maps
  -- into X from each ideal in turn, until we reach the boundary of the N-simplex.
  -- Then we supply a set of fillers for these boundaries, i.e. the set of N-simplices.
  -- Along the way we keep track of face relationships to know how to glue to get from one ideal to the next.

  -- A truncated augmented simplicial set which has simplices of augmented dimension =< N
  data sSet : ∀ (N : ℕ) → Set₁
  -- Filling data for spheres of augmented dimension N required to promote from sSet N to sSet (suc N)
  record FillData {N : ℕ} (XUnd : sSet N) : Set₁

  -- Build by induction on dimension.
  data sSet where
    Aug : Set → sSet 0
    reedy : ∀ {N : ℕ} → ∀ (XUnd : sSet N) →
            ∀ (XFill : FillData XUnd) →
            sSet (suc N)

  -- Given X and F, tells you the set of ideals in X of the shape "weakly preceeding F"
  -- Note that "a face with N+1 digits" is a sneaky equivalent to "a simplex with at most N+1 digits"
  IdealIn : ∀ {N : ℕ} → ∀ (X : sSet N) →
            ∀ {d : ℕ} → ∀ (F : Face N d) →
            Set
  -- Given X G, x, x', tells you whether x' is the G-shaped face of x.
  -- F' will be the pullback of F by G, but padded out with zeros to have N bits.
  -- (It is not explicitly enforced that F' is the pullback, but the constructors will be such
  -- that no "isFaceOf" relation ever gets built when that is not the case)
  isFaceOf : ∀ {N : ℕ} → ∀ (X : sSet N) →
             ∀ {d : ℕ} → {F : Face N d} → ∀ (x : IdealIn X F ) →
             ∀ {d' : ℕ} → ∀ {F' : Face N d'} → ∀ (x' : IdealIn X F') →
             ∀ {n' : ℕ} → ∀ (G : Face N n') →
             Set

  -- The filling data just needs to tell you how to fill spheres.
  record FillData {N} XUnd where
    constructor fillData
    field
      FillX : IdealIn XUnd (PreDelta+ N) →
                          Set

  -- The following type deals with wrapping issues.
  -- When building an N-truncated semisimplicial type X, we will need to know
  -- when one ideal x in X was constructed from another ideal y in X
  -- via particular constructors. But this constructor could have been applied at *any*
  -- earlier stage k, and so x and y will be wrapped N-k times in the passage from a
  -- k-truncated semisimplicial set to an N-truncated one. Thus we won't be able to
  -- directly look at the constructors used to form y from x.
  -- The type isBuildOf keeps track of this information for us as we wrap things to increasing depth.
  --
  -- Let sx be of shape one bigger than x, let y be the last face of x,
  -- and let sy be of shape one bigger than y.
  -- Then isBuildOf x sx y sy will tell you if sx was built from x by attaching sy at y.
  isBuildOf : ∀ {N : ℕ} → ∀ (X : sSet N) →
              ∀ {d : ℕ} → ∀ {F : Face N d} → ∀ (x : IdealIn X F) →
              ∀ {sd : ℕ} → ∀ {sF : Face N sd} →
              -- ∀ (fsf : isSucF F sF) →
              ∀ (sx : IdealIn X sF) →
              ∀ {e : ℕ} → ∀ {G : Face N e} → ∀ (y : IdealIn X G) →
              ∀ {se : ℕ} → ∀ {sG : Face N se} →
              -- ∀ (gsg : isSucF G sG) →
              ∀ (sy : IdealIn X sG) →
              Set

  --These things will be defined inductively, with special cases for N = 0.
  data IdealIn0 (X0 : Set) :
                ∀ {d : ℕ} → ∀ (F : Face zero d) →
                Set where
    taut0 : ∀ (x : X0) → IdealIn0 X0 (inc emp)

  data isFaceOf0 (X0 : Set) :
                ∀ {d : ℕ} → ∀ {F : Face zero d} → IdealIn0 X0 F →
                ∀ {d' : ℕ} → ∀ {F' : Face zero d'} → IdealIn0 X0 F' →
                ∀ {n' : ℕ} → ∀ (G : Face zero n') →
                Set where
    refl0 : ∀ (x : X0) → isFaceOf0 X0 (taut0 x) (taut0 x) (inc emp)

  data isBuildOf0 (X0 : Set) :
              ∀ {d : ℕ} → ∀ {F : Face 0 d} → ∀ (x : IdealIn0 X0 F) →
              ∀ {sd : ℕ} → ∀ {sF : Face 0 sd} →
              -- ∀ (fsf : isSucF F sF) →
              ∀ (sx : IdealIn0 X0 sF) →
              ∀ {e : ℕ} → ∀ {G : Face 0 e} → ∀ (y : IdealIn0 X0 G) →
              ∀ {se : ℕ} → ∀ {sG : Face 0 se} →
              -- ∀ (gsg : isSucF G sG) →
              ∀ (sy : IdealIn0 X0 sG) →
              Set where

  -- In dimension N+1, the definitions will be more complicated.
  data IdealInN {N : ℕ} (XUnd : sSet N) (XFill : FillData XUnd) :
                ∀ {d : ℕ} → ∀ (F : Face (suc N) d) →
                Set
  data isFaceOfN {N : ℕ} (XUnd : sSet N) (XFill : FillData XUnd) :
                  ∀ {d : ℕ} → ∀ {F : Face (suc N) d} → IdealInN XUnd XFill F →
                  ∀ {d' : ℕ} → ∀ {F' : Face (suc N) d'} → IdealInN XUnd XFill F' →
                  ∀ {n' : ℕ} → ∀ (G : Face (suc N) n') →
                  Set

  data isBuildOfN {N : ℕ} (XUnd : sSet N) (XFill : FillData XUnd) :
              ∀ {d : ℕ} → ∀ {F : Face (suc N) d} → ∀ (x : IdealInN XUnd XFill F) →
              ∀ {sd : ℕ} → ∀ {sF : Face (suc N) sd} →
              -- ∀ (fsf : isSucF F sF) →
              ∀ (sx : IdealInN XUnd XFill sF) →
              ∀ {e : ℕ} → ∀ {G : Face (suc N) e} → ∀ (y : IdealInN XUnd XFill G) →
              ∀ {se : ℕ} → ∀ {sG : Face (suc N) se} →
              -- ∀ (gsg : isSucF G sG) →
              ∀ (sy : IdealInN XUnd XFill sG) →
              Set

  --Inductive definitions of all of this data.
  IdealIn (Aug X0) = IdealIn0 X0
  IdealIn (reedy XUnd XFill) = IdealInN XUnd XFill

  isFaceOf (Aug X0) = isFaceOf0 X0
  isFaceOf (reedy XUnd XFill) = isFaceOfN XUnd XFill

  -- isBuildOf (reedy XUnd XFill) = isBuildOfN XUnd XFill
  isBuildOf (Aug X0) = isBuildOf0 X0
  isBuildOf (reedy XUnd XFill) = isBuildOfN XUnd XFill

  data IdealInN {N} XUnd XFill where
    --Inherit ideals from the previous dimension. Need to tack on a leading zero.
    oldN : ∀ {d : ℕ} → ∀ {F : Face N d} → ∀ (x : IdealIn XUnd F) →
            IdealInN XUnd XFill (0x F)
    -- Promote the ideal given by filling a sphere from the previous dimension.
    fillN : ∀ {x : IdealIn XUnd (PreDelta+ N)} → ∀ (z : FillData.FillX XFill x) →
             IdealInN XUnd XFill (0x (inc (Delta+ N)))

    --Build a new closed ideal from an open ideal and some previously-constructed filling data.
    -- sF is required to be a simplex, so that it is a *new* thing to build and not already previously constructed.
    -- x is of shape "strictly below sF".
    -- y is the sF-face of x, i.e. the boundary of the next simplex to be added to complete to "weakly below sF".
    -- so y ought to be of shape "boundary of a simplex", but this is not enforced explicitly.
    -- sy is an ideal (so should be in fact a simplex) filling y.
    -- We obtain buildN z xy of shape "weakly below S" by gluing z onto x along y.
    buildN :  ∀ {d : ℕ} → ∀ {F : Face (suc N) d} → ∀ (x : IdealInN XUnd XFill F) →
              ∀ {sd : ℕ} → ∀ {sF : Simp (suc N) (suc sd)} → ∀ (fsf : isSucF F (inc sF)) →
              ∀ {e : ℕ} → ∀ {G : Face (suc N) e} → ∀ {y : IdealInN XUnd XFill G} →  ∀ (xy : isFaceOfN XUnd XFill x y (inc sF)) →
              ∀ {se : ℕ} → ∀ {sG : Face (suc N) (suc se)} → ∀ (gsg : isSucF G sG) →
              ∀ (sy : IdealInN XUnd XFill sG) →
              ∀ (ysy : isBuildOfN XUnd XFill y sy y sy) →
              IdealInN XUnd XFill (inc sF)

  data isFaceOfN {N} XUnd XFill where
    --Inherit face relations from the previous dimension. Need to tack on a leading zero.
    -- If x' is a G - face of x in the previous dimension,
    -- then oldN x' is a 0x G - face of oldN x, and also a 1x G -face of oldN x.
    oldOld0N : ∀ {d : ℕ} → ∀ {F : Face N d} → ∀ {d' : ℕ} → ∀ {F' : Face N d'} → ∀ {n' : ℕ} → ∀ {G : Face N n'} →
                          ∀ {x : IdealIn XUnd F} → ∀ {x' : IdealIn XUnd F'} → ∀ (xx' : isFaceOf XUnd x x' G) →
              isFaceOfN XUnd XFill (oldN x) (oldN x') (0x G)
    oldOld1N : ∀ {d : ℕ} → ∀ {F : Face N d} → ∀ {d' : ℕ} → ∀ {F' : Face N d'} → ∀ {n' : ℕ} → ∀ {G : Face N n'} →
                          ∀ {x : IdealIn XUnd F} → ∀ {x' : IdealIn XUnd F'} → ∀ (xx' : isFaceOf XUnd x x' G) →
              isFaceOfN XUnd XFill (oldN x) (oldN x') (inc (1x G))

    -- When filling a top-dimensional sphere from the previous dimension, need to inherit faces from the boundary being filled.
    -- If x is an N-sphere filled by z, and x' is an old G-face of x,
    -- then oldN x' is a 0x G - face of fillN z, and also a 1x G - face of fillN z.
    oldFill0N : ∀ {x : IdealIn XUnd (PreDelta+ N)} → ∀ (z : FillData.FillX XFill x) →
               ∀ {d : ℕ} → ∀ {F : Face N d} → ∀ {x' : IdealIn XUnd F} → ∀ {n' : ℕ} → ∀ {G : Face N n'} → ∀ (xx' : isFaceOf XUnd x x' G) →
               isFaceOfN XUnd XFill (fillN z)  (oldN x') (0x G)
    oldFill1N : ∀ {x : IdealIn XUnd (PreDelta+ N)} → ∀ (z : FillData.FillX XFill x) →
               ∀ {d : ℕ} → ∀ {F : Face N d} → ∀ {x' : IdealIn XUnd F} → ∀ {n' : ℕ} → ∀ {G : Face N n'} → ∀ (xx' : isFaceOf XUnd x x' G) →
               isFaceOfN XUnd XFill (fillN z)  (oldN x') (inc (1x G))

    -- When filling a top-dimensional sphere from the previous dimension, need to put in a reflexivity face relation.
    -- There are actually two -- one for the face 111111 and one for the face 011111
    reflFill0N : ∀ {x : IdealIn XUnd (PreDelta+ N)} → ∀ (z : FillData.FillX XFill x) →
                isFaceOfN XUnd XFill (fillN z) (fillN z) (0x (inc (Delta+ N)))
    reflFill1N : ∀ {x : IdealIn XUnd (PreDelta+ N)} → ∀ (z : FillData.FillX XFill x) →
                isFaceOfN XUnd XFill (fillN z) (fillN z) (inc (1x (inc (Delta+ N))))

    -- When building a new ideal, need to inherit faces from the open ideal being filled.
    -- This function takes 21 arguments, 7 of them explicit. I believe it is the second-longest type signature in the file.
    -- sF is required to be a simplex, so that it is a *new* thing to build and not already previously constructed.
    -- x is of shape "strictly below sF".
    -- y is the sF-face of x, i.e. the boundary of the next simplex to be added to complete to "weakly below sF".
    -- so y ought to be of shape "boundary of a simplex", but this is not enforced explicitly.
    -- sy is an ideal (so should be in fact a simplex) filling y.
    -- x' is a face of x.
    -- conclude that, when you glue sy to x along y, you have x' as a face.
    oldBuildN : ∀ {d : ℕ} → ∀ {F : Face (suc N) d} → ∀ (x : IdealInN XUnd XFill F) →
              ∀ {sd : ℕ} → ∀ {sF : Simp (suc N) (suc sd)} → ∀ (fsf : isSucF F (inc sF)) →
              ∀ {e : ℕ} → ∀ {G : Face (suc N) e} → ∀ {y : IdealInN XUnd XFill G} →  ∀ (xy : isFaceOfN XUnd XFill x y (inc sF)) →
              ∀ {se : ℕ} → ∀ {sG : Face (suc N) (suc se)} → ∀ (gsg : isSucF G sG) →
              ∀ (sy : IdealInN XUnd XFill sG) →
              ∀ (ysy : isBuildOfN XUnd XFill y sy y sy) →
              ∀ {d' : ℕ} → ∀ {F' : Face (suc N) d'} →  ∀ {x' : IdealInN XUnd XFill F'} →
                             ∀ {n' : ℕ} → ∀ {H : Face (suc N) n'} → ∀ (xx' : isFaceOfN XUnd XFill x x' H) →
              isFaceOfN XUnd XFill (buildN x fsf xy gsg sy ysy) x' H

    -- When building a new ideal, need to put in "mixed" faces, built from faces of the open ideal being filled and the filling data.
    -- This constructor takes 32 arguments, 13 of them explicit. I believe that's the longest in the file.
    -- sF is required to be a simplex, so that it is a *new* thing to build and not already previously constructed.
    -- x is of shape "strictly below sF".
    -- y is the sF-face of x, i.e. the boundary of the next simplex to be added to complete to "weakly below sF".
    -- so y ought to be of shape "boundary of a simplex", but this is not enforced explicitly.
    -- sy is an ideal (so should be in fact a simplex) filling y.
    -- x' is a face of x.
    -- conclude that when you glue sy to x along y, then sx' is a face.
    mixBuildN : ∀ {d : ℕ} → ∀ {F : Face (suc N) d} → ∀ (x : IdealInN XUnd XFill F) →
              ∀ {sd : ℕ} → ∀ {sF : Simp (suc N) (suc sd)} → ∀ (fsf : isSucF F (inc sF)) →
              ∀ {e : ℕ} → ∀ {G : Face (suc N) e} → ∀ {y : IdealInN XUnd XFill G} →  ∀ (xy : isFaceOfN XUnd XFill x y (inc sF)) →
              ∀ {se : ℕ} → ∀ {sG : Face (suc N) (suc se)} → ∀ (gsg : isSucF G sG) →
              ∀ (sy : IdealInN XUnd XFill sG) →
              ∀ (ysy : isBuildOfN XUnd XFill y sy y sy) →
              ∀ {d' : ℕ} → ∀ {F' : Face (suc N) d'} →  ∀ {x' : IdealInN XUnd XFill F'} →
                             ∀ {n' : ℕ} → ∀ {H : Face (suc N) n'} → ∀ (xx' : isFaceOfN XUnd XFill x x' H) →
              ∀ {sd' : ℕ} → ∀ {sF' : Simp (suc N) (suc sd)} → ∀ (f'sf' : isSucF F' (inc sF')) →
              ∀ (x'y : isFaceOfN XUnd XFill x' y (inc sF')) →
              ∀ {sx' : IdealInN XUnd XFill (inc sF')} → ∀ (x'sx'ysy : isBuildOfN XUnd XFill x' sx' y sy) →
              ∀ {n'' : ℕ} → ∀ {F'' : Face n' n''} → ∀ (shf'' : isPB (inc sF) H F'') →
              ∀ {00F'' : Face (suc N) n''} → ∀ (00f'' : isPadOf F'' 00F'') →
              isFaceOfN XUnd XFill (buildN x fsf xy gsg sy ysy) sx' 00F''

  data isBuildOfN {N} XUnd XFill where
    -- Carry forward the old build relations from XUnd.
    oldIsBuildN : ∀ {d : ℕ} → ∀ {F : Face N d} → ∀ (x : IdealIn XUnd F) →
              ∀ {sd : ℕ} → ∀ {sF : Face N (suc sd)} → ∀ (fsf : isSucF F sF) →
              ∀ (sx : IdealIn XUnd sF) →
              ∀ {e : ℕ} → ∀ {G : Face N e} → ∀ (y : IdealIn XUnd G) →
              ∀ {se : ℕ} → ∀ {sG : Face N (suc se)} → ∀ (gsg : isSucF G sG) →
              ∀ (sy : IdealIn XUnd sG) →
              isBuildOf XUnd x sx y sy →
              isBuildOfN XUnd XFill (oldN x) (oldN sx) (oldN y) (oldN sy)
    -- When filling an N-boundary, we have a reflexive build relationship.
    fillIsBuildN : ∀ {x : IdealIn XUnd (PreDelta+ N)} → ∀ (z : FillData.FillX XFill x) →
                 isBuildOfN XUnd XFill (oldN x) (fillN z) (oldN x) (fillN z)
    -- When we build a new ideal, record it here.
    buildIsBuildN : ∀ {d : ℕ} → ∀ {F : Face (suc N) d} → ∀ (x : IdealInN XUnd XFill F) →
              ∀ {sd : ℕ} → ∀ {sF : Simp (suc N) (suc sd)} → ∀ (fsf : isSucF F (inc sF)) →
              ∀ {e : ℕ} → ∀ {G : Face (suc N) e} → ∀ {y : IdealInN XUnd XFill G} →  ∀ (xy : isFaceOfN XUnd XFill x y (inc sF)) →
              ∀ {se : ℕ} → ∀ {sG : Face (suc N) (suc se)} → ∀ (gsg : isSucF G sG) →
              ∀ (sy : IdealInN XUnd XFill sG) →
              ∀ (ysy : isBuildOfN XUnd XFill y sy y sy) →
              isBuildOfN XUnd XFill x (buildN x fsf xy gsg sy ysy) y sy

max_stars_repo_name: tcampion/Semisimplicial

max_issues_repo_name: tcampion/Semisimplicial

max_forks_repo_name: tcampion/Semisimplicial


text:
-- Andreas, 2020-04-15, issue #4586
-- Better error for invalid let pattern.

test : Set₁
test = let () = Set
       in  Set

-- WAS:
-- Set₁ should be empty, but that's not obvious to me
-- when checking that the pattern () has type Set₁

-- EXPECTED:
-- Not a valid let pattern
-- when scope checking let () = Set in Set

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
module Preliminaries where

open import lib.Basics hiding (_⊔_)
open import lib.NType2

open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma hiding (×-comm)
open import lib.types.Unit
open import lib.types.TLevel

open import lib.types.Paths

-- Most of the contents of Chapter 2.1 are in the library, e.g.
-- natural numbers. We only do the following two adaptions here:

-- A readable notation for the join of universe levels.
infixr 8  _⊔_

_⊔_ : ULevel → ULevel → ULevel
_⊔_ = lmax

-- Addition operator adjustment.
_+_ : ℕ → ℕ → ℕ
a + b = b lib.types.Nat.+ a  -- n + 1 should mean S n (author preference)!

-- Chapter 2.2: We list the lemmata and other statements here.

-- Lemma 2.2.1
transport-is-comp : ∀ {i j} {X : Type i} {Y : Type j} → {x₁ x₂ : X}
  → (h k : X → Y) → (t : x₁ == x₂) → (p : h x₁ == k x₁)
  → (transport _ t p) == ! (ap h t) ∙ p ∙ ap k t
transport-is-comp h k idp p = ! (∙-unit-r _)

-- Lemma 2.2.2 is in the library:
-- lib.NType2.raise-level-<T

-- Lemma 2.2.3 is in the library as well:
-- lib.types.Sigma.Σ-level

-- ... and so is Definition 2.2.4:
-- lib.NType2._-Type_

-- Lemma 2.2.6 as well:
-- lib.types.Pi.Π-level

-- Lemma 2.2.7:
-- lib.NType2.has-level-is-prop

module _ {i j} {A : Type i} {B : A → Type j} where
  module _ (h : (a : A) → is-contr (B a)) where

    -- Lemma 2.2.8 (i)
    Σ₂-contr : Σ A B ≃ A
    Σ₂-contr = Σ₂-Unit ∘e equiv-Σ-snd (λ _ → contr-equiv-Unit (h _))

    -- Lemma 2.2.8 (ii)
    Π₂-contr : Π A B ≃ ⊤
    Π₂-contr = Π₂-Unit ∘e equiv-Π-r (λ _ → contr-equiv-Unit (h _))

  module _ (h : is-contr A) where

    -- Lemma 2.2.9 (i)
    Σ₁-contr : Σ A B ≃ B (fst h)
    Σ₁-contr = Σ₁-Unit ∘e equiv-Σ-fst _ (snd (contr-equiv-Unit h ⁻¹)) ⁻¹

    -- Lemma 2.2.9 (ii)
    Π₁-contr : Π A B ≃ B (fst h)
    Π₁-contr = Π₁-Unit ∘e equiv-Π-l _ (snd (contr-equiv-Unit h ⁻¹)) ⁻¹

-- Lemma 2.2.10 - we refer to the library again
-- lib.types.Sigma.Σ-level
-- and
-- lib.types.Sigma.×-level

-- Lemma 2.2.11
-- lib.Equivalences.equiv-ap

-- Lemma 2.2.12 and Remark 2.2.13
module TT-AC {i j k : ULevel} {A : Type i}
                          {B : A → Type j}
                          {C : (Σ A B) → Type k} where
  -- the two types:
  ONE = (a : A) → Σ (B a) λ b → C (a , b)
  TWO = Σ ((a : A) -> B a) λ g → (a : A) → C (a , g a)

  -- the two canonical functions:
  f : ONE → TWO
  f one = fst ∘ one , snd ∘ one

  g : TWO → ONE
  g two = λ a → (fst two) a , (snd two) a

  -- the compositions are indeed pointwise judgmentally
  -- the identity!
  f∘g : (two : TWO) → f (g two) == two
  f∘g two = idp

  g∘f : (one : ONE) → g (f one) == one
  g∘f one = idp

-- Lemma 2.2.14 is in the library:
-- lib.NType.pathto-is-contr
-- lib.NType.pathfrom-is-contr

-- This formalisation has a separated file for Pointed
-- types, called 'Pointed.agda', which contains
-- (among other things) Definition 2.2.15
-- and Lemma 2.2.17

-- Definition 2.2.19
LEM : ∀ {i} → Type (lsucc i)
LEM {i} = (X : Type i) → is-prop X → Coprod X (¬ X)

LEM∞ : ∀ {i} → Type (lsucc i)
LEM∞ {i} = (X : Type i) → Coprod X (¬ X)

-- The following are some auxiliary lemmata/definitions
-- (not numbered in the thesis)

{- The (function) exponentiation operator. For convenience, we
   choose to define it via postcomposition in the recursion step. -}
infix 10 _^_
_^_ : ∀ {i} {A : Set i} → (A → A) → ℕ → A → A
f ^ 0   = idf _
f ^ S n = (f ^ n) ∘ f

-- Logical equivalence: maps in both directions
_↔_ : ∀ {i j} → Type i → Type j → Type (i ⊔ j)
X ↔ Y = (X → Y) × (Y → X)

-- Composition of ↔
_◎_ : ∀ {i j k} {X : Type i} {Y : Type j} {Z : Type k} → (X ↔ Y) → (Y ↔ Z) → (X ↔ Z)
e₁ ◎ e₂ = fst e₂ ∘ fst e₁ , snd e₁ ∘ snd e₂

-- Subsection 2.3.3
module wtrunc where
  postulate
    -- Definition 2.3.2
    ∣∣_∣∣ : ∀ {i} → (X : Type i) → Type i
    tr-is-prop : ∀ {i} {X : Type i} → is-prop (∣∣ X ∣∣)
    ∣_∣ : ∀ {i} {X : Type i} → X → ∣∣ X ∣∣
    tr-rec : ∀ {i j} {X : Type i} {P : Type j} → (is-prop P) → (X → P) →   ∣∣ X ∣∣ → P

  -- Lemma 2.3.4
  -- the induction principle is derivable:
  module _ {i j : _} {X : Type i} {P : ∣∣ X ∣∣ → Type j} (h : (z : ∣∣ X ∣∣) → is-prop (P z)) (k : (x : X) → P ∣ x ∣) where

    total : Type (i ⊔ j)
    total = Σ ∣∣ X ∣∣ P

    jj : X → total
    jj x = ∣ x ∣ , k x

    total-prop : is-prop total
    total-prop = Σ-level tr-is-prop h

    total-map : ∣∣ X ∣∣ → total
    total-map = tr-rec total-prop jj

    tr-ind : (z : ∣∣ X ∣∣) → P z
    tr-ind z = transport P (prop-has-all-paths tr-is-prop _ _) (snd (total-map z))

  -- Remark 2.3.5
  -- further, the propositional β-rule is derivable:
  trunc-β : ∀ {i j} {X : Type i} {P : Type j} → (pp : is-prop P) → (f : X → P) → (x : X) → tr-rec pp f ∣ x ∣ == f x
  trunc-β pp f x = prop-has-all-paths pp _ _

  -- comment: Trunc is functorial
  trunc-functorial : ∀ {i} {j} {X : Type i} {Y : Type j} → (X → Y) → ∣∣ X ∣∣ → ∣∣ Y ∣∣
  trunc-functorial f = tr-rec tr-is-prop (∣_∣ ∘ f)

  -- Proposition 2.3.6
  impred : ∀ {i} {X : Type i} → ∣∣ X ∣∣ ↔ ((P : Type i) → is-prop P → (X → P) → P)
  impred {X = X} = (λ z P pp f → tr-rec pp f z) , λ h → h ∣∣ X ∣∣ tr-is-prop ∣_∣

  -- Proposition 2.3.6 (second part) - note that we use funext (in the form: Π preserves truncation level)
  impr-equiv : ∀ {i} {X : Type i} → is-equiv (fst (impred {X = X}))
  impr-equiv {i} {X} = is-eq (fst (impred {X = X})) (snd (impred {X = X}))
    (λ top → prop-has-all-paths (Π-level (λ P → Π-level (λ pp → (Π-level (λ _ → pp))))) _ _)
    (λ z → prop-has-all-paths tr-is-prop _ _)

-- The rest of the file contains various useful lemmata
-- and definitions that are NOT in the thesis (at least
-- not as numbered statements).

{- Since natural numbers and universe levels use
   different types, we require a translation operation.
   We will only make use of this in chapter 7: Higher
   Homotopies in a Hierarchy of Univalent Universes. -}
｢_｣ : ℕ → ULevel
｢ 0   ｣ = lzero
｢ S n ｣ = lsucc ｢ n ｣

-- A trivial, but useful lemma. The only thing we do is hiding the arguments.
prop-eq-triv : ∀ {i} {P : Type i} → {p₁ p₂ : P} → is-prop P → p₁ == p₂
prop-eq-triv h = prop-has-all-paths h _ _

-- A second such useful lemma
second-comp-triv : ∀ {i} {X : Type i} → {P : X → Type i} → ((x : X) → is-prop (P x)) → (a b : Σ X P) → (fst a == fst b) → a == b
second-comp-triv {P = P} h a b q = pair= q (from-transp P q (prop-eq-triv (h (fst b))))

-- the following is the function which the univalence
-- axiom postulates to be an equivalence
-- (we define it ourselves as we do not want to
-- implicitly import the whole univalence library)
path-to-equiv : ∀ {i} {X : Type i} {Y : Type i} → X == Y → X ≃ Y
path-to-equiv {X = X} idp = ide X

-- some rather silly lemmata

delete-idp : ∀ {i} {X : Type i} → {x₁ x₂ : X} → (p q : x₁ == x₂) → (p ∙ idp == q) ≃ (p == q)
delete-idp idp q = ide _

add-path : ∀ {i} {X : Type i} → {x₁ x₂ x₃ : X} → (p q : x₁ == x₂) → (r : x₂ == x₃) → (p == q) == (p ∙ r == q ∙ r)
add-path idp q idp = transport (λ q₁ → (idp == q₁) == (idp == q ∙ idp)) {x = q ∙ idp} {y = q} (∙-unit-r _) idp

reverse-paths : ∀ {i} {X : Type i} → {x₁ x₂ : X} → (p : x₂ == x₁) → (q : x₁ == x₂) → (! p == q) ≃ (p == ! q)
reverse-paths p idp =
  ! p == idp   ≃⟨ path-to-equiv (add-path _ _ _) ⟩
  ! p ∙ p == p ≃⟨ path-to-equiv (transport (λ p₁ → (! p ∙ p == p) == (p₁ == p)) (!-inv-l p) idp) ⟩
  idp == p     ≃⟨ !-equiv ⟩
  p == idp     ≃∎

switch-args : ∀ {i j k} {X : Type i} {Y : Type j} {Z : X → Y → Type k} → ((x : X) → (y : Y) → Z x y) ≃ ((y : Y) → (x : X) → Z x y)
switch-args = equiv f g h₁ h₂ where
  f = λ k y x → k x y
  g = λ i x y → i y x
  h₁ = λ _ → idp
  h₂ = λ _ → idp

-- another useful (but simple) lemma: if we have a proof of (x , y₁) == (x , y₂) and the type of x is a set, we get a proof of y₁ == y₂.
set-lemma : ∀ {i j} {X : Type i} → (is-set X) → {Y : X → Type j} → (x₀ : X) → (y₁ y₂ : Y x₀) → _==_ {A = Σ X Y} (x₀ , y₁) (x₀ , y₂) → y₁ == y₂
set-lemma {X = X} h {Y = Y} x₀ y₁ y₂ p =
  y₁ =⟨ idp ⟩
  transport Y idp        y₁ =⟨ transport {A = x₀ == x₀} (λ q → y₁ == transport Y q y₁)
                                 {x = idp} {y = ap fst p}
                                 (prop-has-all-paths (h x₀ x₀) _ _)
                                 idp ⟩
  transport Y (ap fst p) y₁ =⟨ snd-of-p ⟩
  y₂ ∎ where
    pairs : =Σ {B = Y} (x₀ , y₁) (x₀ , y₂)
    pairs = <– (=Σ-eqv _ _) p

    paov : y₁ == y₂ [ Y ↓ fst (pairs) ]
    paov = snd pairs

    snd-of-p : transport Y (ap fst p) y₁ == y₂
    snd-of-p = to-transp paov

×-comm : ∀ {i j} {A : Type i} {B : Type j} → (A × B) ≃ (B × A)
×-comm = equiv (λ {(a , b) → (b , a)})
               (λ {(b , a) → (a , b)})
               (λ _ → idp) (λ _ → idp)

Σ-comm-snd : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
           → Σ (Σ A B) (λ ab → C (fst ab)) ≃ Σ (Σ A C) (λ ac → B (fst ac))
Σ-comm-snd {A = A} {B} {C} =
  Σ (Σ A B) (λ ab → C (fst ab))  ≃⟨ Σ-assoc ⟩
  Σ A (λ a → B a × C a)          ≃⟨ equiv-Σ-snd (λ _ → ×-comm) ⟩
  Σ A (λ a → C a × B a)          ≃⟨ Σ-assoc ⁻¹ ⟩
  Σ (Σ A C) (λ ac → B (fst ac))  ≃∎

flip : ∀ {i j k} {A : Type i} {B : Type j} {C : A → B → Type k}
       → ((a : A) (b : B) → C a b) → ((b : B) (a : A) → C a b)
flip = –> (curry-equiv ∘e equiv-Π-l _ (snd ×-comm) ∘e curry-equiv ⁻¹)

module _ {i j k} {A : Type i} {B : Type j} {C : A → B → Type k} where
  ↓-cst→app-equiv : {x x' : A} {p : x == x'} {u : (b : B) → C x b} {u' : (b : B) → C x' b}
                  → ((b : B) → u b == u' b [ (λ x → C x b) ↓ p ]) ≃ (u == u' [ (λ x → (b : B) → C x b) ↓ p ])
  ↓-cst→app-equiv {p = idp} = equiv λ= app= (! ∘ λ=-η) (λ= ∘ app=-β)

module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} where
  ↓-cst2-equiv : {x y : A} (p : x == y) {b : C x} {c : C y}
    (q : b == c [ C ↓ p ]) {u : B x} {v : B y}
    → (u == v [ B ↓ p ]) ≃ (u == v [ (λ xy → B (fst xy)) ↓ (pair= p q) ])
  ↓-cst2-equiv idp idp = ide _

module _ {i} {A B : Type i} (e : A ≃ B) {u : A} {v : B} where
  ↓-idf-ua-equiv : (–> e u == v) ≃ (u == v [ (λ x → x) ↓ (ua e) ])
  ↓-idf-ua-equiv = to-transp-equiv _ _ ⁻¹ ∘e (_ , pre∙-is-equiv (ap (λ z → z u) (ap coe (ap-idf (ua e)) ∙ ap –> (coe-equiv-β e))))

-- On propositions, equivalence coincides with logical equivalence.
module _ {i j} {A : Type i} {B : Type j} where
  prop-equiv' : (B → is-prop A) → (A → is-prop B) → (A → B) → (B → A) → A ≃ B
  prop-equiv' h k f g = equiv f g (λ b → prop-has-all-paths (k (g b)) _ _)
                                  (λ a → prop-has-all-paths (h (f a)) _ _)

  prop-equiv : is-prop A → is-prop B → (A → B) → (B → A) → A ≃ B
  prop-equiv h k f g = prop-equiv' (cst h) (cst k) f g

-- Equivalent types have equivalent truncatedness propositions.
equiv-level : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂}
            → A ≃ B → has-level n A ≃ has-level n B
equiv-level u = prop-equiv has-level-is-prop
                           has-level-is-prop
                           (equiv-preserves-level u)
                           (equiv-preserves-level (u ⁻¹))

prop-equiv-inhab-to-contr : ∀ {i} {A : Type i} → is-prop A ≃ (A → is-contr A)
prop-equiv-inhab-to-contr = prop-equiv is-prop-is-prop
                                       (Π-level (λ _ → is-contr-is-prop))
                                       (flip inhab-prop-is-contr)
                                       inhab-to-contr-is-prop

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --type-in-type   #-} -- NOT SOUND!

open import Data.Empty      using (⊥)
open import Data.Nat        renaming (ℕ to Nat)
open import Data.Nat.DivMod
open import Data.Product    hiding (map)
open import Data.Unit       using (⊤)

module x where

{-
https://webspace.science.uu.nl/~swier004/publications/2019-icfp-submission-a.pdf

A predicate transformer semantics for effects

WOUTER SWIERSTRA and TIM BAANEN, Universiteit Utrecht

abstract

reasoning about effectful code harder than pure code

predicate transformer (PT) semantics gives a refinement relation that can be used to
- relate a program to its specification, or
- calculate effectful programs that are correct by construction

INTRODUCTION

key techniques
- syntax of effectful computations represented as free monads
  - assigning meaning to these monads gives meaning to the syntactic ops each effect provides
- paper shows how to assign PT semantics to computations arising
  from Kleisli arrows on free monads
  - enables computing the weakest precondition associated with a given postcondition
- using weakest precondition semantics
  - define refinement on computations
  - show how to
    - use this refinement relation to show a program satisfies its specification, or
    - calculate a program from its specification.
- show how programs and specifications may be mixed,
  enabling verified programs to be calculated from their specification one step at a time

2 BACKGROUND

Free monads
-}

-- C          : type of commands
-- Free C R   : returns an 'a' or issues command c : C
-- For each c : C, there is a set of responses R c
-- 2nd arg of Step is continuation : how to proceed after receiving response R c
data Free (C : Set) (R : C → Set) (a : Set) : Set where
  Pure :                           a  → Free C R a
  Step : (c : C) → (R c → Free C R a) → Free C R a

-- show that 'Free' is a monad:

map : ∀ {a b C : Set} {R : C → Set} → (a → b) → Free C R a → Free C R b
map f (Pure x)   = Pure (f x)
map f (Step c k) = Step c (λ r → map f (k r))

return : ∀ {a C : Set} {R : C → Set} → a → Free C R a
return = Pure

_>>=_ : ∀ {a b C : Set} {R : C → Set} → Free C R a → (a → Free C R b) → Free C R b
Pure   x >>= f = f x
Step c x >>= f = Step c (λ r → x r >>= f)

{-
different effects choose C and R differently, depending on their ops

Weakest precondition semantics

idea of associating weakest precondition semantics with imperative programs
dates to Dijkstra’s Guarded Command Language [1975]

ways to specify behaviour of function f : a → b
- reference implementation
- define a relation R : a → b → Set
- write contracts and test cases
- PT semantics

call values of type a → Set : predicate on type a

PTs are functions between predicates
e.g., weakest precondition:
-}

-- "maps"
-- function f : a → b and
-- desired postcondition on the function’s output, b → Set
-- to weakest precondition a → Set on function’s input that ensures postcondition satisfied
--
-- note: definition is just reverse function composition
-- wp0 : ∀ {a b : Set} → (f : a → b) → (b → Set) → (a → Set)
wp0 : ∀ {a : Set} {b :     Set} (f :       a → b)   →           (b   → Set) → (a → Set)
wp0 f P = λ x → P   (f x)
{-
above wp semantics is sometimes too restrictive
- no way to specify that output is related to input
- fix via making f dependent:
-}
wp  : ∀ {a : Set} {b : a → Set} (f : (x : a) → b x) → ((x : a) → b x → Set) → (a → Set)
wp  f P = λ x → P x (f x)

-- shorthand for working with predicates and predicates transformers
_⊆_ : ∀ {a : Set} → (a → Set) → (a → Set) → Set
P ⊆ Q = ∀ x → P x → Q x

-- refinement relation defined between PTs
_⊑_ : ∀ {a : Set} {b : a → Set} → (pt1 pt2 : ((x : a) → b x → Set) → (a → Set)) → Set₁
pt1 ⊑ pt2 = ∀ P → pt1 P ⊆ pt2 P

{-
use refinement relation
- to relate PT semantics between programs and specifications
- to show a program satisfies its specification; or
- to show that one program is somehow ‘better’ than another,
  where ‘better’ is defined by choice of PT semantics

in pure setting, this refinement relation is not interesting:
the refinement relation corresponds to extensional equality between functions:

lemma follows from the ‘Leibniz rule’ for equality in intensional type theory:
refinement : ∀ (f g : a → b) → (wp f ⊑ wp g) ↔ (∀ x → f x ≡ g x)

this paper defines PT semantics for Kleisli arrows of form

    a → Free C R b

could use 'wp' to assign semantics to these computations directly,
but typically not interested in syntactic equality between free monads

rather want to study semantics of effectful programs they represent

to define a PT semantics for effects
define a function with form:

  -- how to lift a predicate on 'a' over effectful computation returning 'a'
  pt : (a → Set) → Free C R a → Set

'pt' def depends on semantics desired for a particulr free monad

Crucially,
choice of pt and weakest precondition semantics, wp, together
give a way to assign weakest precondition semantics to Kleisli arrows
representing effectful computations

3 PARTIALITY

Partial computations : i.e., 'Maybe'

make choices for commands C and responses R
-}

data C : Set where
  Abort : C -- no continuation

R : C → Set
R Abort = ⊥ -- since C has no continuation, valid responses is empty

Partial : Set → Set
Partial = Free C R

-- smart constructor for failure:
abort : ∀ {a : Set} → Partial a
abort = Step Abort (λ ())

{-
computation of type Partial a will either
- return a value of type a or
- fail, issuing abort command

Note that responses to Abort command are empty;
abort smart constructor abort uses this to discharge the continuation
in the second argument of the Step constructor

Example: division

expression language, closed under division and natural numbers:
-}

data Expr : Set where
  Val : Nat  → Expr
  Div : Expr → Expr → Expr

-- semantics specified using inductively defined RELATION:
-- def rules out erroneous results by requiring the divisor evaluates to non-zero
data _⇓_ : Expr → Nat → Set where
  Base : ∀ {x : Nat}
       → Val x ⇓ x
  Step : ∀ {l r : Expr} {v1 v2 : Nat}
       →       l ⇓  v1
       →       r ⇓         (suc v2)
       → Div l r ⇓ (v1 div (suc v2))

-- Alternatively
-- evaluate Expr via monadic INTERPRETER, using Partial to handle division-by-zero

-- op used by ⟦_⟧ interpreter
_÷_ : Nat → Nat → Partial Nat
n ÷ zero    = abort
n ÷ (suc k) = return (n div (suc k))

⟦_⟧ : Expr → Partial Nat
⟦ Val x ⟧     = return x
⟦ Div e1 e2 ⟧ = ⟦ e1 ⟧ >>= λ v1 → ⟦ e2 ⟧ >>= λ v2 → v1 ÷ v2

{-
std lib 'div' requires implicit proof that divisor is non-zero

when divisor is zero, interpreter fail explicitly with abort

How to relate these two definitions?

Assign a weakest precondition semantics to Kleisli arrows of the form

    a → Partial b
-}

wpPartial : ∀ {a : Set} {b : a → Set}
          → (f : (x : a) → Partial (b x))
          → (P : (x : a) →          b x → Set)
          → (a → Set)
wpPartial f P = wp f (mustPT P)
 where
  mustPT : ∀ {a : Set} {b : a → Set}
         → (P : (x : a) → b x → Set)
         →      (x : a)
         → Partial       (b x) → Set
  mustPT P _ (Pure y)       = P _ y
  mustPT P _ (Step Abort _) = ⊥
{-
To call 'wp', must show how to transform
-      predicate                  P :         b → Set
- to a predicate on partial results : Partial b → Set
Done via proposition 'mustPT P c'
- holds when computation c of type Partial b successfully returns a 'b' that satisfies P

particular PT semantics of partial computations determined by def mustPT
here: rule out failure entirely
- so case Abort returns empty type

Given this PT semantics for Kleisli arrows in general,
can now study semantics of above monadic interpreter
via passing
- interpreter: ⟦_⟧
- desired postcondition : _⇓_
as arguments to wpPartial:

  wpPartial ⟦_⟧ _⇓_ : Expr → Set

resulting in a predicate on expressions

for all expressions satisfying this predicate,
the monadic interpreter and the relational specification, _⇓_,
must agree on the result of evaluation

What does this say about correctness of interpreter?
To understand the predicate better, consider defining this predicate on expressions:
-}

SafeDiv : Expr → Set
SafeDiv (Val x)     = ⊤
SafeDiv (Div e1 e2) = (e2 ⇓ zero → ⊥) {-∧-} × SafeDiv e1 {-∧-} × SafeDiv e2

{-
Expect : any expr e for which SafeDiv e holds
can be evaluated without division-by-zero

can prove SafeDiv is sufficient condition for two notions of evaluation to coincide:

-- lemma relates the two semantics
-- expressed as a relation and an evaluator
-- for those expressions that satisfy the SafeDiv property
correct : SafeDiv ⊆ wpPartial ⟦_⟧ _⇓_

Instead of manually defining SafeDiv, define more general predicate
characterising the domain of a partial function:
-}

dom : ∀ {a : Set} {b : a → Set}
    → ((x : a)
    → Partial (b x))
    → (a → Set)
dom f = wpPartial f (λ _ _ → ⊤)

{-
can show that the two semantics agree precisely on the domain of the interpreter:

sound    : dom       ⟦_⟧ ⊆ wpPartial ⟦_⟧ _⇓_
complete : wpPartial ⟦_⟧ _⇓_ ⊆ dom ⟦_⟧

both proofs proceed by induction on the argument expression

Refinement

weakest precondition semantics on partial computations give rise
to a refinement relation on Kleisli arrows of the form a → Partial b

can characterise this relation by proving:

refinement : (f g : a → Maybe b)
           → (wpPartial f ⊑ wpPartial g) ↔ (∀ x → (f x ≡ g x) ∨ (f x ≡ Nothing))

use refinement to relate Kleisli morphisms,
and to relate a program to a specification given by a pre- and postcondition

Example: Add (interpreter for stack machine)

add top two elements; can fail fail if stack has too few elements

below shows how to prove the definition meets its specification

Define specification in terms of a pre/post condition.
The specification of a function of type (x : a) → b x consists of
-}
record Spec (a : Set) (b : a → Set) : Set where
  constructor [_,_]
  field
    pre  : a → Set             -- a precondition on a, and
    post : (x : a) → b x → Set -- a postcondition relating inputs that satisfy this precondition
                               -- and the corresponding outputs

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Issue228 where

open import Common.Level

postulate
  ∞ : Level

data _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  _,_ : A → B → A × B

data Large : Set ∞ where
  large : Large

data Small : Set₁ where
  small : Set → Small

P : Set
P = Large × Small

[_] : Set → P
[ A ] = (large , small A)

potentially-bad : P
potentially-bad = [ P ]

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Papers.HigherGroupsViaDURG where

-- Johannes Schipp von Branitz,
-- "Higher Groups via Displayed Univalent Reflexive Graphs in Cubical Type Theory".

import Cubical.Algebra.Group as Group

import Cubical.Core.Glue as Glue

import Cubical.Data.Sigma.Properties as Sigma
import Cubical.Data.Unit as Unit

import Cubical.DStructures.Base as DSBase

import Cubical.DStructures.Meta.Properties as DSProperties
import Cubical.DStructures.Meta.Isomorphism as DSIsomorphism

import Cubical.DStructures.Structures.Action as DSAction
import Cubical.DStructures.Structures.Category as DSCategory
import Cubical.DStructures.Structures.Constant as DSConstant
import Cubical.DStructures.Structures.Group as DSGroup
import Cubical.DStructures.Structures.Higher as DSHigher
import Cubical.DStructures.Structures.Nat as DSNat
import Cubical.DStructures.Structures.PeifferGraph as DSPeifferGraph
import Cubical.DStructures.Structures.ReflGraph as DSReflGraph
import Cubical.DStructures.Structures.SplitEpi as DSSplitEpi
import Cubical.DStructures.Structures.Strict2Group as DSStrict2Group
import Cubical.DStructures.Structures.Type as DSType
import Cubical.DStructures.Structures.Universe as DSUniverse
import Cubical.DStructures.Structures.VertComp as DSVertComp
import Cubical.DStructures.Structures.XModule as DSXModule
import Cubical.DStructures.Equivalences.GroupSplitEpiAction as DSGroupSplitEpiAction
import Cubical.DStructures.Equivalences.PreXModReflGraph as DSPreXModReflGraph
import Cubical.DStructures.Equivalences.XModPeifferGraph as DSXModPeifferGraph
import Cubical.DStructures.Equivalences.PeifferGraphS2G as DSPeifferGraphS2G

import Cubical.Foundations.GroupoidLaws as GroupoidLaws
import Cubical.Foundations.Equiv as Equiv
import Cubical.Foundations.Equiv.Fiberwise as Fiberwise
import Cubical.Foundations.Filler as Filler
import Cubical.Foundations.HLevels as HLevels
import Cubical.Foundations.HLevels' as HLevels'
import Cubical.Foundations.Isomorphism as Isomorphism
import Cubical.Foundations.Prelude as Prelude
import Cubical.Foundations.Path as FPath
import Cubical.Foundations.Pointed as Pointed
import Cubical.Foundations.Univalence as Univalence
import Cubical.Foundations.Transport as Transport

import Cubical.Functions.FunExtEquiv as FunExtEquiv
import Cubical.Functions.Fibration as Fibration

import Cubical.Relation.Binary as Binary

import Cubical.HITs.EilenbergMacLane1 as EM1

import Cubical.Homotopy.Base as HomotopyBase
import Cubical.Homotopy.Connected as Connected
import Cubical.Homotopy.PointedFibration as PointedFibration
import Cubical.Homotopy.Loopspace as Loopspace

import Cubical.Structures.Subtype as Subtype

import Cubical.HITs.Truncation as Truncation

----------------------------------------------------------------------------
-- 2.  Cubical Type Theory
-- 2.1 Dependent Type Theory
-- 2.2 Path Types
-- 2.3 Cubical Groupoid Laws
-- 2.4 Functions, Equivalences and Univalence
-- 2.5 Truncated and Connected Types
-- 2.6 Groups
----------------------------------------------------------------------------

-- 2.2 Path Types

-- Example 2.1
open Sigma using (ΣPath≡PathΣ) public

open Prelude using (transport) public

-- Proposition 2.2
open FPath using (PathP≡Path) public

-- 2.3 Cubical Groupoid Laws

open Prelude using (refl;
                   transportRefl;
                   subst;
                   J) public
             renaming (cong to ap) public
open Prelude using (_∙∙_∙∙_;
                   doubleCompPath-filler;
                   compPath-unique) public
open Prelude using (_∙_) public

-- Lemma 2.5
open FPath using (PathP≡doubleCompPathˡ) public

-- Lemma 2.5
open GroupoidLaws using (doubleCompPath-elim) public

-- Lemma 2.6
open Filler using (cube-cong) public

-- 2.4 Functions, Equivalences and Univalence

open Unit renaming (Unit to 𝟙) public
open Prelude using (isContr) public
open Unit using (isContrUnit) public

-- Proposition 2.7
open Prelude using (singl;
                   isContrSingl) public

-- Definition 2.8
open Equiv renaming (fiber to fib) public
open Glue using (isEquiv;
                _≃_;
                equivFun) public
open Isomorphism using (Iso) public

-- Proposition 2.9
open Transport using (isEquivTransport) public

-- Proposition 2.10
open Fiberwise using (fiberEquiv;
                     totalEquiv) public

-- Proposition 2.11
open Sigma using (Σ-cong-equiv) public

-- Definition 2.12
open HomotopyBase using (_∼_) public

-- Theorem 2.13
open FunExtEquiv using (funExtEquiv) public

-- Theorem 2.14
open Univalence using (univalence) public
                renaming (ua to idToEquiv⁻¹;
                          uaβ to idToEquiv-β;
                          uaη to idToEquiv-η) public

-- Lemma 2.15
open Univalence using (ua→) public

-- 2.5 Truncated and Connected Types

open Prelude using (isProp;
                   isSet) public
open HLevels using (isOfHLevel;
                   TypeOfHLevel) public

-- Lemma 2.16
open Sigma using (Σ-contractFst;
                 Σ-contractSnd) public

-- Lemma 2.17
open Prelude using (isProp→PathP) public

-- Lemma 2.18
open Subtype using (subtypeWitnessIrrelevance) public
open Sigma using (Σ≡Prop) public

-- Definition 2.19
open HLevels using (isOfHLevelDep) public

-- Proposition 2.20
open HLevels' using (truncSelfId→truncId) public

-- Proposition 2.21
open HLevels using (isOfHLevelΣ) public

-- Proposition 2.22
open HLevels using (isPropIsOfHLevel) public

-- Proposition 2.23
open HLevels using (isOfHLevelΠ) public

-- Theorem 2.24
open Truncation using (∥_∥_;
                      rec;
                      elim) public

-- Definition 2.25
open Connected using (isConnected;
                     isConnectedFun) public

-- Lemma 2.26
open Connected using (isConnectedPoint) public

-- 2.6 Groups

-- Proposition 2.28
open Group using (isPropIsGroupHom;
                 isSetGroupHom) public

-- Proposition 2.29
open Group.Kernel using (ker) public

-- Proposition 2.30
open Group using (GroupMorphismExt) public

-- Theorem 2.31
open Group using (GroupPath) public

-- Definition 2.32
open Group using (isGroupSplitEpi) public

-- Definition 2.33
open Group using (GroupAction;
                 IsGroupAction) public

-- Proposition 2.34
open Group using (semidirectProd) public

-----------------------------------------------------------------------------
-- 3.  Displayed Structures
-- 3.1 Motivation
-- 3.2 Displayed Categories
-- 3.3 Univalent Reflexive Graphs
-- 3.4 Displayed Univalent Reflexive Graphs
-- 3.5 Operations on Displayed Univalent Reflexive Graphs
-- 3.6 Constructing Equivalences Using Displayed Univalent Reflexive Graphs
-----------------------------------------------------------------------------

-- 3.1 Motivation

-- Proposition 3.1
open Fibration using (dispTypeIso) public

-- 3.2 Displayed Categories

-- Definition 3.2
-- not implemented

-- Theorem 3.3
-- not implemented

-- 3.3 Univalent Reflexive Graphs

-- Definition 3.4, 3.5
open DSBase using (URGStr) public

-- Example 3.6
open DSGroup using (𝒮-group) public

-- Example 3.7
open DSCategory using (Cat→𝒮) public

-- Proposition 3.8
-- not implemented

-- Example 3.9
open DSNat using (𝒮-Nat) public

-- Theorem 3.10
open Binary using (contrRelSingl→isUnivalent;
                  isUnivalent→contrRelSingl) public

-- Example 3.11
open DSType using (𝒮-type) public
open DSUniverse using (𝒮-universe) public

-- Proposition 3.12
open DSType using (𝒮-uniqueness) public

-- 3.4 Displayed Univalent Reflexive Graphs

-- Proposition 3.13
open DSBase using (URGStrᴰ) public

open DSBase using (make-𝒮ᴰ) public

-- Proposition 3.14
open DSType using (Subtype→Sub-𝒮ᴰ) public

-- Example 3.15
open DSHigher using (𝒮ᴰ-connected;
                    𝒮ᴰ-truncated) public

-- 3.5 Operations on Displayed Univalent Reflexive Graphs

-- Theorem 3.16
open DSProperties using (∫⟨_⟩_) public

-- Corollary 3.17
open DSConstant using (𝒮ᴰ-const) public

-- Definition 3.18
open DSConstant using (_×𝒮_) public

-- Theorem 3.19
open DSProperties using (splitTotal-𝒮ᴰ) public

-- Proposition 3.20
open DSProperties using (VerticalLift-𝒮ᴰ) public

-- Corollary 3.21
open DSProperties using (combine-𝒮ᴰ) public

-- 3.6 Constructing Equivalences Using Displayed Univalent Reflexive Graphs

-- Definition 3.22
open Binary using (RelIso) public

-- Proposition 3.23
open DSIsomorphism using (𝒮-PIso;
                         𝒮-PIso→Iso) public

-- Definition 3.24, Theorem 3.25
open Binary using (RelFiberIsoOver→Iso) public
open DSIsomorphism using (𝒮ᴰ-♭PIso-Over→TotalIso) public

-----------------------------------------------------------------------------
-- 4.  Equivalence of Strict 2-Groups and Crossed Modules
-- 4.1 Strict 2-Groups
-- 4.2 Crossed Modules
-- 4.3 Group Actions and Split Monomorphisms
-- 4.4 Precrossed Modules and Internal Reflexive Graphs
-- 4.5 Crossed Modules and Peiffer Graphs
-- 4.6 Peiffer Graphs and Strict 2-Groups
----------------------------------------------------------------------------

-- 4.1 Strict 2-Groups

-- Example 4.1
-- not implemented

-- 4.2 Crossed Modules

-- Definition 4.2, Example 4.3
-- not implemented

-- 4.3 Group Actions and Split Monomorphisms

-- Proposition 4.4
open DSGroup using (𝒮ᴰ-G²\F;
                   𝒮ᴰ-G²\B;
                   𝒮ᴰ-G²\FB) public

-- Lemma 4.5
open DSSplitEpi using (𝒮ᴰ-SplitEpi) public

-- Lemma 4.6
open DSAction using (𝒮ᴰ-G²\Las) public

-- Lemma 4.7
open DSAction using (𝒮ᴰ-G²Las\Action) public

-- Proposition 4.8, Proposition 4.9, Lemma 4.10, Theorem 4.11
open DSGroupSplitEpiAction using (𝒮ᴰ-Iso-GroupAct-SplitEpi-*;
                                 IsoActionSplitEpi) public

-- 4.4 Precrossed Modules and Internal Reflexive Graphs

-- Lemma 4.12
open DSXModule using (𝒮ᴰ-Action\PreXModuleStr) public

-- Definition 4.13
open DSXModule using (isEquivariant;
                     isPropIsEquivariant;
                     PreXModule) public

-- Lemma 4.14
open DSSplitEpi using (𝒮ᴰ-G²FBSplit\B) public

-- Lemma 4.15
open DSReflGraph using (𝒮ᴰ-ReflGraph; ReflGraph) public

-- Lemma 4.16, Lemma 4.17, Lemma 4.18, Theorem 4.19
open DSPreXModReflGraph using (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph';
                              Iso-PreXModule-ReflGraph) public

-- 4.5 Crossed Modules and Peiffer Graphs

-- Definition 4.20
open DSXModule using (XModule;
                     isPeiffer;
                     isPropIsPeiffer) public

-- Definition 4.21
open DSPeifferGraph using (isPeifferGraph;
                          isPropIsPeifferGraph) public

-- Lemma 4.22, Lemma 4.2.3, Theorem 4.24
open DSXModPeifferGraph public

-- 4.6 Peiffer Graphs and Strict 2-Groups

-- Definition 4.25
open DSVertComp using (VertComp) public

-- Proposition 4.26
open DSVertComp using (VertComp→+₁) public

-- Proposition 4.27
open DSVertComp using (isPropVertComp) public

-- Proposition 4.28, Proposition 4.29, Theorem 4.30
open DSPeifferGraphS2G public

--------------------------------------------------------
-- 5.  Higher Groups in Cubical Type Theory
-- 5.1 Pointed Types
-- 5.2 Homotopy Groups
-- 5.3 Higher Groups
-- 5.4 Eilenberg-MacLane-Spaces
-- 5.5 Delooping Groups
-------------------------------------------------------

-- 5.1 Pointed Types

-- Proposition 5.1
open DSUniverse using (𝒮ᴰ-pointed) public

-- Definition 5.2
open Pointed using (Π∙) public

-- Definition 5.3
open Pointed using (_∙∼_;
                   _∙∼P_) public

-- Proposition 5.4
open Pointed using (∙∼≃∙∼P) public

-- Theorem 5.5
open Pointed using (funExt∙≃) public

-- Theorem 5.6
open PointedFibration using (sec∙Trunc') public

-- 5.2 Homotopy Groups

-- Definition 5.7
open Loopspace using (Ω) public

-- Definition 5.8
open Group using (π₁-1BGroup) public

-- 5.3 Higher Groups

-- Lemma 5.9
open DSHigher using (𝒮-BGroup) public

-- Definition 5.10
open Group using (BGroup) public

-- Proposition 5.11
open DSHigher using (𝒮ᴰ-BGroupHom) public

-- Corollary 5.12
-- not implemented

-- 5.4 Eilenberg-MacLane-Spaces

-- Definition 5.13
open EM1 using (EM₁) public

-- Lemma 5.14
open EM1 using (emloop-comp) public

-- Lemma 5.15
open EM1 using (elimEq) public

-- Theorem 5.16
open EM1 renaming (elim to EM₁-elim;
                  rec to EM₁-rec) public

-- Lemma 5.17
open Group using (emloop-id;
                 emloop-inv) public

-- Theorem 5.18
open Group using (π₁EM₁≃) public

-- 5.5 Delooping Groups

-- Proposition 5.19, Theorem 5.20
open DSHigher using (𝒮-Iso-BGroup-Group) public

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
open import Mockingbird.Forest using (Forest)

-- Aristocratic Birds
module Mockingbird.Problems.Chapter19 {ℓb ℓ} (forest : Forest {ℓb} {ℓ}) where

open import Data.Product using (_×_; _,_; ∃-syntax)
open import Function using (_$_)
open import Level using (_⊔_)
open import Data.Vec using ([]; _∷_)
open import Relation.Unary using (Pred; _∈_; _⊆_; _⊇_)

open Forest forest
open import Mockingbird.Forest.Birds forest
open import Mockingbird.Forest.Combination.Vec forest
open import Mockingbird.Forest.Combination.Vec.Properties forest
open import Mockingbird.Forest.Extensionality forest
import Mockingbird.Problems.Chapter11 forest as Chapter₁₁
import Mockingbird.Problems.Chapter12 forest as Chapter₁₂

problem₁″ : ⦃ _ : HasEagle ⦄ ⦃ _ : HasCardinalOnceRemoved ⦄ ⦃ _ : HasCardinalTwiceRemoved ⦄ ⦃ _ : HasWarbler ⦄ → HasJaybird
problem₁″ = record
  { J = C** ∙ (W ∙ (C* ∙ E))
  ; isJaybird = λ x y z w → begin
      C** ∙ (W ∙ (C* ∙ E)) ∙ x ∙ y ∙ z ∙ w  ≈⟨ isCardinalTwiceRemoved (W ∙ (C* ∙ E)) x y z w ⟩
      W ∙ (C* ∙ E) ∙ x ∙ y ∙ w ∙ z          ≈⟨ congʳ $ congʳ $ congʳ $ isWarbler (C* ∙ E) x ⟩
      C* ∙ E ∙ x ∙ x ∙ y ∙ w ∙ z            ≈⟨ congʳ $ congʳ $ isCardinalOnceRemoved E x x y ⟩
      E ∙ x ∙ y ∙ x ∙ w ∙ z                 ≈⟨ isEagle x y x w z ⟩
      x ∙ y ∙ (x ∙ w ∙ z)                   ∎
  }

problem₁′ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasWarbler ⦄ → HasJaybird
problem₁′ = record
  { J = B ∙ (B ∙ C) ∙ (W ∙ (B ∙ C ∙ (B ∙ (B ∙ B ∙ B))))
  ; isJaybird = isJaybird ⦃ problem₁″ ⦄
  } where
  instance
    hasEagle = Chapter₁₁.problem₇
    hasCardinalOnceRemoved = Chapter₁₁.problem₃₁
    hasCardinalTwiceRemoved = Chapter₁₁.problem₃₅-C**

problem₁ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasMockingbird ⦄ → HasJaybird
problem₁ = problem₁′
  where
    instance
      hasCardinal = Chapter₁₁.problem₂₁′
      hasWarbler = Chapter₁₂.problem₇

problem₂ : ⦃ _ : HasJaybird ⦄ ⦃ _ : HasIdentity ⦄ → HasQuixoticBird
problem₂ = record
  { Q₁ = J ∙ I
  ; isQuixoticBird = λ x y z → begin
      J ∙ I ∙ x ∙ y ∙ z    ≈⟨ isJaybird I x y z ⟩
      I ∙ x ∙ (I ∙ z ∙ y)  ≈⟨ congʳ $ isIdentity x ⟩
      x ∙ (I ∙ z ∙ y)      ≈⟨ congˡ $ congʳ $ isIdentity z ⟩
      x ∙ (z ∙ y)          ∎
  }

problem₃ : ⦃ _ : HasQuixoticBird ⦄ ⦃ _ : HasIdentity ⦄ → HasThrush
problem₃ = record
  { T = Q₁ ∙ I
  ; isThrush = λ x y → begin
      Q₁ ∙ I ∙ x ∙ y  ≈⟨ isQuixoticBird I x y ⟩
      I ∙ (y ∙ x)     ≈⟨ isIdentity $ y ∙ x ⟩
      y ∙ x           ∎
  }

problem₄ : ⦃ _ : HasJaybird ⦄ ⦃ _ : HasThrush ⦄ → HasRobin
problem₄ = record
  { R = J ∙ T
  ; isRobin = λ x y z → begin
      J ∙ T ∙ x ∙ y ∙ z    ≈⟨ isJaybird T x y z ⟩
      T ∙ x ∙ (T ∙ z ∙ y)  ≈⟨ isThrush x $ T ∙ z ∙ y ⟩
      T ∙ z ∙ y ∙ x        ≈⟨ congʳ $ isThrush z y ⟩
      y ∙ z ∙ x            ∎
  }

problem₅-C* : ⦃ _ : HasCardinal ⦄ ⦃ _ : HasQuixoticBird ⦄ → HasCardinalOnceRemoved
problem₅-C* = record
  { C* = C ∙ (Q₁ ∙ C)
  ; isCardinalOnceRemoved = λ x y z w → begin
      C ∙ (Q₁ ∙ C) ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ isCardinal (Q₁ ∙ C) x y ⟩
      Q₁ ∙ C ∙ y ∙ x ∙ z ∙ w        ≈⟨ congʳ $ congʳ $ isQuixoticBird C y x ⟩
      C ∙ (x ∙ y) ∙ z ∙ w           ≈⟨ isCardinal (x ∙ y) z w ⟩
      x ∙ y ∙ w ∙ z                 ∎
  }

problem₅ : ⦃ _ : HasRobin ⦄ ⦃ _ : HasQuixoticBird ⦄ → HasBluebird
problem₅ = record
  { B = C* ∙ Q₁
  ; isBluebird = λ x y z → begin
      C* ∙ Q₁ ∙ x ∙ y ∙ z  ≈⟨ isCardinalOnceRemoved Q₁ x y z ⟩
      Q₁ ∙ x ∙ z ∙ y       ≈⟨ isQuixoticBird x z y ⟩
      x ∙ (y ∙ z)          ∎
  } where
  instance
    hasCardinal = Chapter₁₁.problem₂₁
    hasCardinalOnceRemoved = problem₅-C*

problem₆ : ⦃ _ : HasJaybird ⦄ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄
  → ∃[ J₁ ] (∀ x y z w → J₁ ∙ x ∙ y ∙ z ∙ w ≈ y ∙ x ∙ (w ∙ x ∙ z))
problem₆ =
  ( B ∙ J ∙ T
  , λ x y z w → begin
      B ∙ J ∙ T ∙ x ∙ y ∙ z ∙ w    ≈⟨ (congʳ $ congʳ $ congʳ $ isBluebird J T x) ⟩
      J ∙ (T ∙ x) ∙ y ∙ z ∙ w      ≈⟨ isJaybird (T ∙ x) y z w ⟩
      T ∙ x ∙ y ∙ (T ∙ x ∙ w ∙ z)  ≈⟨ congʳ $ isThrush x y ⟩
      y ∙ x ∙ (T ∙ x ∙ w ∙ z)      ≈⟨ congˡ $ congʳ $ isThrush x w ⟩
      y ∙ x ∙ (w ∙ x ∙ z)          ∎
  )

problem₇ : ⦃ _ : HasCardinal ⦄ ⦃ _ : HasThrush ⦄
  → ∃[ J₁ ] (∀ x y z w → J₁ ∙ x ∙ y ∙ z ∙ w ≈ y ∙ x ∙ (w ∙ x ∙ z))
  → HasMockingbird
problem₇ (J₁ , isJ₁) = record
  { M = C ∙ (C ∙ (C ∙ J₁ ∙ T) ∙ T) ∙ T
  ; isMockingbird = λ x → begin
      C ∙ (C ∙ (C ∙ J₁ ∙ T) ∙ T) ∙ T ∙ x  ≈⟨ isCardinal _ T x ⟩
      C ∙ (C ∙ J₁ ∙ T) ∙ T ∙ x ∙ T        ≈⟨ congʳ $ isCardinal _ T x ⟩
      C ∙ J₁ ∙ T ∙ x ∙ T ∙ T              ≈⟨ congʳ $ congʳ $ isCardinal J₁ T x ⟩
      J₁ ∙ x ∙ T ∙ T ∙ T                  ≈⟨ isJ₁ x T T T ⟩
      T ∙ x ∙ (T ∙ x ∙ T)                 ≈⟨ isThrush x (T ∙ x ∙ T) ⟩
      T ∙ x ∙ T ∙ x                       ≈⟨ congʳ $ isThrush x T ⟩
      T ∙ x ∙ x                           ≈⟨ isThrush x x ⟩
      x ∙ x                               ∎
  }

module _  ⦃ _ : HasJaybird ⦄ ⦃ hasIdentity′ : HasIdentity ⦄ where
  private
    instance
      hasQuixoticBird = problem₂

  hasThrush : HasThrush
  hasThrush = problem₃

  private
    instance
      _ = hasThrush
      hasRobin = problem₄

  hasBluebird : HasBluebird
  hasBluebird = problem₅

  private
    instance
      _ = hasBluebird
      hasCardinal = Chapter₁₁.problem₂₁′

  hasMockingbird : HasMockingbird
  hasMockingbird = problem₇ problem₆

  hasIdentity : HasIdentity
  hasIdentity = hasIdentity′

-- Equality of predicates.
infix 4 _≐_
_≐_ : ∀ {a ℓ} {A : Set a} (P Q : Pred A ℓ) → Set (a ⊔ ℓ)
P ≐ Q = P ⊆ Q × Q ⊆ P

module _ ⦃ _ : Extensional ⦄
         ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasThrush ⦄
         ⦃ _ : HasIdentity ⦄ ⦃ _ : HasJaybird ⦄ where
  private
    ⟨B,M,T,I⟩ = ⟨ B ∷ M ∷ T ∷ I ∷ [] ⟩
    ⟨J,I⟩ = ⟨ J ∷ I ∷ [] ⟩

  module _ where
    private
      instance
        hasCardinal = Chapter₁₁.problem₂₁′
        hasWarbler = Chapter₁₂.problem₇

      b : B ∈ ⟨B,M,T,I⟩
      b = [ here refl ]

      m : M ∈ ⟨B,M,T,I⟩
      m = [ there (here refl) ]

      t : T ∈ ⟨B,M,T,I⟩
      t = [ there (there (here refl)) ]

      c : C ∈ ⟨B,M,T,I⟩
      c = b ⟨∙⟩ b ⟨∙⟩ t ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ t) ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ t)

      w : W ∈ ⟨B,M,T,I⟩
      w = b ⟨∙⟩ (t ⟨∙⟩ (b ⟨∙⟩ m ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ t))) ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ t)

    ⟨J,I⟩⊆⟨B,M,T,I⟩ : ⟨J,I⟩ ⊆ ⟨B,M,T,I⟩
    ⟨J,I⟩⊆⟨B,M,T,I⟩ [ here x≈J ] = subst′
      (trans x≈J $ ext′ $ ext′ $ ext′ $ ext′ $ trans
        (isJaybird _ _ _ _)
        (sym $ isJaybird ⦃ problem₁′ ⦄ _ _ _ _))
      (b ⟨∙⟩ (b ⟨∙⟩ c) ⟨∙⟩ (w ⟨∙⟩ (b ⟨∙⟩ c ⟨∙⟩ (b ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ b)))))
    ⟨J,I⟩⊆⟨B,M,T,I⟩ [ there (here x≈I) ] = [ there (there (there (here x≈I))) ]
    ⟨J,I⟩⊆⟨B,M,T,I⟩ (x∈⟨J,I⟩ ⟨∙⟩ y∈⟨J,I⟩ ∣ xy≈z) = ⟨J,I⟩⊆⟨B,M,T,I⟩ x∈⟨J,I⟩ ⟨∙⟩ ⟨J,I⟩⊆⟨B,M,T,I⟩ y∈⟨J,I⟩ ∣ xy≈z

  module _ where
    private
      instance
        hasQuixoticBird = problem₂
        hasRobin = problem₄
        hasCardinal = Chapter₁₁.problem₂₁
        hasCardinalOnceRemoved = problem₅-C*

      j : J ∈ ⟨J,I⟩
      j = [ here refl ]

      i : I ∈ ⟨J,I⟩
      i = [ there (here refl) ]

      q₁ : Q₁ ∈ ⟨J,I⟩
      q₁ = j ⟨∙⟩ i

      t : T ∈ ⟨J,I⟩
      t = subst′ (ext′ (ext′ (trans (isThrush _ _) (sym (isThrush ⦃ problem₃ ⦄ _ _))))) $
        j ⟨∙⟩ i ⟨∙⟩ i

      r : R ∈ ⟨J,I⟩
      r = j ⟨∙⟩ t

      c : C ∈ ⟨J,I⟩
      c = r ⟨∙⟩ r ⟨∙⟩ r

      c* : C* ∈ ⟨J,I⟩
      c* = c ⟨∙⟩ (q₁ ⟨∙⟩ c)

      b : B ∈ ⟨J,I⟩
      b = subst′ (ext′ (ext′ (ext′ (trans (isBluebird _ _ _) (sym (isBluebird ⦃ problem₅ ⦄ _ _ _)))))) $
        c* ⟨∙⟩ q₁

      m : M ∈ ⟨J,I⟩
      m = subst′ (ext′ (trans (isMockingbird _) (sym (isMockingbird ⦃ problem₇ problem₆ ⦄ _)))) $
        c ⟨∙⟩ (c ⟨∙⟩ (c ⟨∙⟩ (b ⟨∙⟩ j ⟨∙⟩ t) ⟨∙⟩ t) ⟨∙⟩ t) ⟨∙⟩ t

    ⟨J,I⟩⊇⟨B,M,T,I⟩ : ⟨J,I⟩ ⊇ ⟨B,M,T,I⟩
    ⟨J,I⟩⊇⟨B,M,T,I⟩ [ here x≈B ] = subst′ x≈B b
    ⟨J,I⟩⊇⟨B,M,T,I⟩ [ there (here x≈M) ] = subst′ x≈M m
    ⟨J,I⟩⊇⟨B,M,T,I⟩ [ there (there (here x≈T)) ] = subst′ x≈T t
    ⟨J,I⟩⊇⟨B,M,T,I⟩ [ there (there (there (here x≈I))) ] = [ there (here x≈I) ]
    ⟨J,I⟩⊇⟨B,M,T,I⟩ (x∈⟨B,M,T,I⟩ ⟨∙⟩ y∈⟨B,M,T,I⟩ ∣ xy≈z) = ⟨J,I⟩⊇⟨B,M,T,I⟩ x∈⟨B,M,T,I⟩ ⟨∙⟩ ⟨J,I⟩⊇⟨B,M,T,I⟩ y∈⟨B,M,T,I⟩ ∣ xy≈z

  ⟨J,I⟩≐⟨B,M,T,I⟩ : ⟨ J ∷ I ∷ [] ⟩ ≐ ⟨ B ∷ M ∷ T ∷ I ∷ [] ⟩
  ⟨J,I⟩≐⟨B,M,T,I⟩ = (⟨J,I⟩⊆⟨B,M,T,I⟩ , ⟨J,I⟩⊇⟨B,M,T,I⟩)

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
{-
  Define finitely generated ideals of commutative rings and
  show that they are an ideal.
  Parts of this should be reusable for explicit constructions
  of free modules over a finite set.
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.FGIdeal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Vec
open import Cubical.Data.Nat using (ℕ)

open import Cubical.HITs.PropositionalTruncation hiding (map)

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.Ring.QuotientRing
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

module _ (Ring@(R , str) : CommRing ℓ) (r : R) where
  infixr 5 _holds
  _holds : hProp ℓ → Type ℓ
  P holds = fst P
  open CommRingStr str
  open RingTheory (CommRing→Ring Ring)

  linearCombination : {n : ℕ} → Vec R n → Vec R n → R
  linearCombination [] [] = 0r
  linearCombination (c ∷ coefficients) (x ∷ l) = c · x + linearCombination coefficients l

  coefficientSum : {n : ℕ} → Vec R n → Vec R n → Vec R n
  coefficientSum [] [] = []
  coefficientSum (x ∷ c) (y ∷ c′) = x + y ∷ coefficientSum c c′

  sumDist+ : (n : ℕ) (c c′ l : Vec R n)
            → linearCombination (coefficientSum c c′) l
              ≡ linearCombination c l + linearCombination c′ l
  sumDist+ ℕ.zero [] [] [] = solve Ring
  sumDist+ (ℕ.suc n) (x ∷ c) (y ∷ c′) (a ∷ l) =
    linearCombination (coefficientSum (x ∷ c) (y ∷ c′)) (a ∷ l)            ≡⟨ refl ⟩
    (x + y) · a + linearCombination (coefficientSum c c′) l                ≡⟨ step1 ⟩
    (x + y) · a + (linearCombination c l + linearCombination c′ l)         ≡⟨ step2 ⟩
    (x · a + linearCombination c l) + (y · a + linearCombination c′ l)     ≡⟨ refl ⟩
    linearCombination (x ∷ c) (a ∷ l) + linearCombination (y ∷ c′) (a ∷ l) ∎
    where
      step1 = cong (λ z → (x + y) · a + z) (sumDist+ n c c′ l)
      autoSolve : (x y a t1 t2 : R)
                  → (x + y) · a + (t1 + t2) ≡ (x · a + t1) + (y · a + t2)
      autoSolve = solve Ring
      step2 = autoSolve x y a _ _

  dist- : (n : ℕ) (c l : Vec R n)
          → linearCombination (map -_ c) l
            ≡ - linearCombination c l
  dist- ℕ.zero [] [] = solve Ring
  dist- (ℕ.suc n) (x ∷ c) (a ∷ l) =
      - x · a + linearCombination (map -_ c) l    ≡[ i ]⟨ - x · a + dist- n c l i ⟩
      - x · a - linearCombination c l             ≡⟨ step1 x a _ ⟩
      - (x · a + linearCombination c l)           ∎
      where step1 : (x a t1 : R) → - x · a - t1 ≡ - (x · a + t1)
            step1 = solve Ring

  dist0 : (n : ℕ) (l : Vec R n)
          → linearCombination (replicate 0r) l ≡ 0r
  dist0 ℕ.zero [] = refl
  dist0 (ℕ.suc n) (a ∷ l) =
    0r · a + linearCombination (replicate 0r) l ≡[ i ]⟨  0r · a + dist0 n l i ⟩
    0r · a + 0r                                 ≡⟨ step1 a ⟩
    0r ∎
    where step1 : (a : R) → 0r · a + 0r ≡ 0r
          step1 = solve Ring

  isLinearCombination : {n : ℕ} → Vec R n → R → Type ℓ
  isLinearCombination l x =
    ∥ Σ[ coefficients ∈ Vec R _ ] x ≡ linearCombination coefficients l ∥

  {- If x and y are linear combinations of l, then (x + y) is
     a linear combination. -}
  isLinearCombination+ : {n : ℕ} {x y : R} → (l : Vec R n)
                         → isLinearCombination l x
                         → isLinearCombination l y
                         → isLinearCombination l (x + y)
  isLinearCombination+ l =
    elim (λ _ → isOfHLevelΠ 1 (λ _ → isPropPropTrunc))
         (λ {(cx , px) → elim (λ _ → isPropPropTrunc)
          λ {(cy , py) →
            ∣  coefficientSum cx cy ,
                (_ + _                                           ≡[ i ]⟨ px i + py i ⟩
                 linearCombination cx l + linearCombination cy l ≡⟨ sym (sumDist+ _ cx cy l) ⟩
                 linearCombination (coefficientSum cx cy) l ∎) ∣}})

  {- If x is a linear combinations of l, then -x is
     a linear combination. -}
  isLinearCombination- : {n : ℕ} {x y : R} (l : Vec R n)
                         → isLinearCombination l x
                         → isLinearCombination l (- x)
  isLinearCombination- l =
    elim (λ _ → isPropPropTrunc)
         λ {(cx , px) → ∣ map -_ cx ,
                         ( - _                             ≡⟨ cong -_ px ⟩
                           - linearCombination cx l        ≡⟨ sym (dist- _ cx l) ⟩
                           linearCombination (map -_ cx) l ∎) ∣}

  {- 0r is the trivial linear Combination -}
  isLinearCombination0 : {n : ℕ} (l : Vec R n)
                        → isLinearCombination l 0r
  isLinearCombination0 l = ∣ replicate 0r , sym (dist0 _ l) ∣

  {- Linear combinations are stable under left multiplication -}
  isLinearCombinationL· : {n : ℕ} (l : Vec R n)
                        → (r x : R)
                        → isLinearCombination l x
                        → isLinearCombination l (r · x)
  isLinearCombinationL· l r x =
    elim (λ _ → isPropPropTrunc)
         λ {(cx , px) →
            ∣ map (r ·_) cx ,
             (r · _                               ≡[ i ]⟨ r · px i ⟩
              r · linearCombination cx l          ≡⟨ step1 _ cx l r  ⟩
              linearCombination (map (r ·_) cx) l ∎) ∣}
    where
      step2 : (r c a t1 : R) → r · (c · a + t1) ≡ r · (c · a) + r · t1
      step2 = solve Ring
      step3 : (r c a t1 : R) → r · (c · a) + t1 ≡ r · c · a + t1
      step3 = solve Ring
      step1 : (k : ℕ) (cx l : Vec R k)
              → (r : R)
              → r · linearCombination cx l ≡ linearCombination (map (r ·_) cx) l
      step1 ℕ.zero [] [] r = 0RightAnnihilates _
      step1 (ℕ.suc k) (c ∷ cx) (a ∷ l) r =
        r · (c · a + linearCombination cx l)               ≡⟨ step2 r c a _ ⟩
        r · (c · a) + r · linearCombination cx l           ≡[ i ]⟨ r · (c · a) + step1 _ cx l r i ⟩
        r · (c · a) + linearCombination (map (_·_ r) cx) l ≡⟨ step3 r c a _ ⟩
        r · c · a + linearCombination (map (_·_ r) cx) l ∎

  generatedIdeal : {n : ℕ} → Vec R n → IdealsIn Ring
  generatedIdeal l = makeIdeal Ring
                               (λ x → isLinearCombination l x , isPropPropTrunc)
                               (isLinearCombination+ l)
                               (isLinearCombination0 l)
                               λ r → isLinearCombinationL· l r _


text:
module Luau.Var where

open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.String using (String; primStringEquality)
open import Agda.Builtin.TrustMe using (primTrustMe)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Equality using (_≢_)

Var : Set
Var = String

_≡ⱽ_ : (a b : Var) → Dec (a ≡ b)
a ≡ⱽ b with primStringEquality a b
a ≡ⱽ b | false = no p where postulate p : (a ≢ b)
a ≡ⱽ b | true = yes primTrustMe

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
------------------------------------------------------------------------------
-- Testing the translation of the propositional functions
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module PropositionalFunction1 where

------------------------------------------------------------------------------

postulate
  D  : Set
  A  : D → Set
  a  : D

-- In this case, the propositional function does not use logical
-- constants.
postulate foo : A a → A a
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
open import Prelude

module Implicits.Semantics.Term where

open import Implicits.Syntax
open import Implicits.WellTyped
open import Implicits.Semantics.Type
open import Implicits.Semantics.Context
open import Implicits.Semantics.Lemmas
open import Implicits.Semantics.RewriteContext
open import SystemF.Everything as F using ()

module TermSemantics
  (_⊢ᵣ_ : ∀ {ν} → ICtx ν → Type ν → Set)
  (⟦_,_⟧r : ∀ {ν n} {K : Ktx ν n} {a} → (proj₂ K) ⊢ᵣ a → K# K →
            ∃ λ t → ⟦ proj₁ K ⟧ctx→ F.⊢ t ∈ ⟦ a ⟧tp→) where

  open TypingRules _⊢ᵣ_

  -- denotational semantics of well-typed terms
  ⟦_,_⟧ : ∀ {ν n} {K : Ktx ν n} {t} {a : Type ν} → K ⊢ t ∈ a → K# K → F.Term ν n
  ⟦_,_⟧ (var x) m = F.var x
  ⟦_,_⟧ (Λ t) m = F.Λ ⟦ t , #tvar m ⟧
  ⟦_,_⟧ (λ' a x) m = F.λ' ⟦ a ⟧tp→ ⟦ x , #var a m ⟧
  ⟦_,_⟧ (f [ b ]) m = F._[_] ⟦ f , m ⟧ ⟦ b ⟧tp→
  ⟦_,_⟧ (f · e) m = ⟦ f , m ⟧ F.· ⟦ e , m ⟧
  ⟦_,_⟧ (ρ {a = a} _ x) m = F.λ' ⟦ a ⟧tp→ ⟦ x , #ivar a m ⟧
  ⟦_,_⟧ (f ⟨ e∈Δ ⟩) m = ⟦ f , m ⟧ F.· (proj₁ ⟦ e∈Δ , m ⟧r)
  ⟦_,_⟧ (_with'_ r e) m = ⟦ r , m ⟧ F.· ⟦ e , m ⟧


text:
open import Agda.Builtin.String
open import Agda.Builtin.Equality

_ : primShowChar 'c' ≡ "'c'"
_ = refl

_ : primShowString "ccc" ≡ "\"ccc\""
_ = refl


text:
module GGT.Bundles where

open import Level
open import Relation.Unary
open import Relation.Binary -- using (Rel)
open import Algebra.Core
open import Algebra.Bundles
open import GGT.Structures
open import Data.Product
-- do we need a left action definition?
-- parametrize over Op r/l?

record Action a b ℓ₁ ℓ₂ : Set (suc (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂))  where
  infixl 6 _·_
  infix 3 _≋_
  open Group hiding (setoid)
  field
    G : Group a ℓ₁
    Ω : Set b
    _≋_ : Rel Ω ℓ₂
    _·_ : Opᵣ (Carrier G) Ω
    isAction : IsAction (_≈_ G) _≋_ _·_ (_∙_ G) (ε G) (_⁻¹ G)

  open IsAction isAction public

  -- the (raw) pointwise stabilizer
  stab : Ω → Pred (Carrier G) ℓ₂
  stab o = λ (g : Carrier G) → o · g ≋ o

  -- Orbital relation
  _ω_  : Rel Ω (a ⊔ ℓ₂)
  o ω o' = ∃[ g ] (o · g ≋ o')

  _·G : Ω → Pred Ω (a ⊔ ℓ₂)
  o ·G = o ω_

  -- Orbits
  open import GGT.Setoid setoid (a ⊔ ℓ₂)
  Orbit : Ω → Setoid (b ⊔ (a ⊔ ℓ₂)) ℓ₂
  Orbit o = subSetoid (o ·G)

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Support for reflection
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Reflection where

import Agda.Builtin.Reflection as Builtin

------------------------------------------------------------------------
-- Names, Metas, and Literals re-exported publicly

open import Reflection.Abstraction as Abstraction public
  using (Abs; abs)
open import Reflection.Argument as Argument public
  using (Arg; arg; Args; vArg; hArg; iArg)
open import Reflection.Definition as Definition  public
  using (Definition)
open import Reflection.Meta as Meta public
  using (Meta)
open import Reflection.Name as Name public
  using (Name; Names)
open import Reflection.Literal as Literal public
  using (Literal)
open import Reflection.Pattern as Pattern public
  using (Pattern)
open import Reflection.Term as Term public
  using (Term; Type; Clause; Clauses; Sort)

import Reflection.Argument.Relevance as Relevance
import Reflection.Argument.Visibility as Visibility
import Reflection.Argument.Information as Information

open Definition.Definition public
open Information.ArgInfo public
open Literal.Literal public
open Relevance.Relevance public
open Term.Term public
open Visibility.Visibility public

------------------------------------------------------------------------
-- Fixity

open Builtin public
  using (non-assoc; related; unrelated; fixity)
  renaming
  ( left-assoc      to assocˡ
  ; right-assoc     to assocʳ
  ; primQNameFixity to getFixity
  )

------------------------------------------------------------------------
-- Type checking monad

-- Type errors
open Builtin public using (ErrorPart; strErr; termErr; nameErr)

-- The monad
open Builtin public
  using ( TC; bindTC; unify; typeError; inferType; checkType
        ; normalise; reduce
        ; catchTC; quoteTC; unquoteTC
        ; getContext; extendContext; inContext; freshName
        ; declareDef; declarePostulate; defineFun; getType; getDefinition
        ; blockOnMeta; commitTC; isMacro; withNormalisation
        ; debugPrint; noConstraints; runSpeculative)
  renaming (returnTC to return)

-- Standard monad operators

open import Reflection.TypeChecking.MonadSyntax public
  using (_>>=_; _>>_)

newMeta : Type → TC Term
newMeta = checkType unknown

------------------------------------------------------------------------
-- Show

open import Reflection.Show public

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

returnTC = return
{-# WARNING_ON_USAGE returnTC
"Warning: returnTC was deprecated in v1.1.
Please use return instead."
#-}

-- Version 1.3

Arg-info = Information.ArgInfo
{-# WARNING_ON_USAGE Arg-info
"Warning: Arg-info was deprecated in v1.3.
Please use Reflection.Argument.Information's ArgInfo instead."
#-}

infix 4 _≟-Lit_ _≟-Name_ _≟-Meta_ _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_
        _≟-Pattern_ _≟-ArgPatterns_

_≟-Lit_ = Literal._≟_
{-# WARNING_ON_USAGE _≟-Lit_
"Warning: _≟-Lit_ was deprecated in v1.3.
Please use Reflection.Literal's _≟_ instead."
#-}

_≟-Name_ = Name._≟_
{-# WARNING_ON_USAGE _≟-Name_
"Warning: _≟-Name_ was deprecated in v1.3.
Please use Reflection.Name's _≟_ instead."
#-}

_≟-Meta_ = Meta._≟_
{-# WARNING_ON_USAGE _≟-Meta_
"Warning: _≟-Meta_ was deprecated in v1.3.
Please use Reflection.Meta's _≟_ instead."
#-}

_≟-Visibility_ = Visibility._≟_
{-# WARNING_ON_USAGE _≟-Visibility_
"Warning: _≟-Visibility_ was deprecated in v1.3.
Please use Reflection.Argument.Visibility's _≟_ instead."
#-}

_≟-Relevance_ = Relevance._≟_
{-# WARNING_ON_USAGE _≟-Relevance_
"Warning: _≟-Relevance_ was deprecated in v1.3.
Please use Reflection.Argument.Relevance's _≟_ instead."
#-}

_≟-Arg-info_ = Information._≟_
{-# WARNING_ON_USAGE _≟-Arg-info_
"Warning: _≟-Arg-info_ was deprecated in v1.3.
Please use Reflection.Argument.Information's _≟_ instead."
#-}

_≟-Pattern_ = Pattern._≟_
{-# WARNING_ON_USAGE _≟-Pattern_
"Warning: _≟-Pattern_ was deprecated in v1.3.
Please use Reflection.Pattern's _≟_ instead."
#-}

_≟-ArgPatterns_ = Pattern._≟s_
{-# WARNING_ON_USAGE _≟-ArgPatterns_
"Warning: _≟-ArgPatterns_ was deprecated in v1.3.
Please use Reflection.Pattern's _≟s_ instead."
#-}

map-Abs = Abstraction.map
{-# WARNING_ON_USAGE map-Abs
"Warning: map-Abs was deprecated in v1.3.
Please use Reflection.Abstraction's map instead."
#-}

map-Arg = Argument.map
{-# WARNING_ON_USAGE map-Arg
"Warning: map-Arg was deprecated in v1.3.
Please use Reflection.Argument's map instead."
#-}

map-Args = Argument.map-Args
{-# WARNING_ON_USAGE map-Args
"Warning: map-Args was deprecated in v1.3.
Please use Reflection.Argument's map-Args instead."
#-}

visibility = Information.visibility
{-# WARNING_ON_USAGE visibility
"Warning: visibility was deprecated in v1.3.
Please use Reflection.Argument.Information's visibility instead."
#-}

relevance = Information.relevance
{-# WARNING_ON_USAGE relevance
"Warning: relevance was deprecated in v1.3.
Please use Reflection.Argument.Information's relevance instead."
#-}

infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_
        _≟-Clause_ _≟-Clauses_ _≟_
        _≟-Sort_

_≟-AbsTerm_ = Term._≟-AbsTerm_
{-# WARNING_ON_USAGE _≟-AbsTerm_
"Warning: _≟-AbsTerm_ was deprecated in v1.3.
Please use Reflection.Term's _≟-AbsTerm_ instead."
#-}

_≟-AbsType_ = Term._≟-AbsType_
{-# WARNING_ON_USAGE _≟-AbsType_
"Warning: _≟-AbsType_ was deprecated in v1.3.
Please use Reflection.Term's _≟-AbsType_ instead."
#-}

_≟-ArgTerm_ = Term._≟-ArgTerm_
{-# WARNING_ON_USAGE _≟-ArgTerm_
"Warning: _≟-ArgTerm_ was deprecated in v1.3.
Please use Reflection.Term's _≟-ArgTerm_ instead."
#-}

_≟-ArgType_ = Term._≟-ArgType_
{-# WARNING_ON_USAGE _≟-ArgType_
"Warning: _≟-ArgType_ was deprecated in v1.3.
Please use Reflection.Term's _≟-ArgType_ instead."
#-}

_≟-Args_    = Term._≟-Args_
{-# WARNING_ON_USAGE _≟-Args_
"Warning: _≟-Args_ was deprecated in v1.3.
Please use Reflection.Term's _≟-Args_ instead."
#-}

_≟-Clause_  = Term._≟-Clause_
{-# WARNING_ON_USAGE _≟-Clause_
"Warning: _≟-Clause_ was deprecated in v1.3.
Please use Reflection.Term's _≟-Clause_ instead."
#-}

_≟-Clauses_ = Term._≟-Clauses_
{-# WARNING_ON_USAGE _≟-Clauses_
"Warning: _≟-Clauses_ was deprecated in v1.3.
Please use Reflection.Term's _≟-Clauses_ instead."
#-}

_≟_         = Term._≟_
{-# WARNING_ON_USAGE _≟_
"Warning: _≟_ was deprecated in v1.3.
Please use Reflection.Term's _≟_ instead."
#-}

_≟-Sort_    = Term._≟-Sort_
{-# WARNING_ON_USAGE _≟-Sort_
"Warning: _≟-Sort_ was deprecated in v1.3.
Please use Reflection.Term's _≟-Sort_ instead."
#-}


text:
{-# OPTIONS --without-K --safe #-}

open import Algebra

module Data.FingerTree.Structures
  {r m}
  (ℳ : Monoid r m)
  where

open import Level using (_⊔_)
open import Data.Product
open import Relation.Unary

open import Data.FingerTree.Measures ℳ
open import Data.FingerTree.Reasoning ℳ

open Monoid ℳ renaming (Carrier to 𝓡)
open σ ⦃ ... ⦄
{-# DISPLAY σ.μ _ = μ #-}

data Digit {a} (Σ : Set a) : Set a where
  D₁ : Σ → Digit Σ
  D₂ : Σ → Σ → Digit Σ
  D₃ : Σ → Σ → Σ → Digit Σ
  D₄ : Σ → Σ → Σ → Σ → Digit Σ

instance
  σ-Digit : ∀ {a} {Σ : Set a} → ⦃ _ : σ Σ ⦄ → σ (Digit Σ)
  μ ⦃ σ-Digit ⦄ (D₁ x₁) = μ x₁
  μ ⦃ σ-Digit ⦄ (D₂ x₁ x₂) = μ x₁ ∙ μ x₂
  μ ⦃ σ-Digit ⦄ (D₃ x₁ x₂ x₃) = μ x₁ ∙ (μ x₂ ∙ μ x₃)
  μ ⦃ σ-Digit ⦄ (D₄ x₁ x₂ x₃ x₄) = μ x₁ ∙ (μ x₂ ∙ (μ x₃ ∙ μ x₄))

data Node {a} (Σ : Set a) : Set a where
  N₂ : Σ → Σ → Node Σ
  N₃ : Σ → Σ → Σ → Node Σ

instance
  σ-Node : ∀ {a} {Σ : Set a} → ⦃ _ : σ Σ ⦄ → σ (Node Σ)
  μ ⦃ σ-Node ⦄ (N₂ x₁ x₂) = μ x₁ ∙ μ x₂
  μ ⦃ σ-Node ⦄ (N₃ x₁ x₂ x₃) = μ x₁ ∙ (μ x₂ ∙ μ x₃)

mutual
  infixr 5 _&_&_
  record Deep {a} (Σ : Set a) ⦃ _ : σ Σ ⦄ : Set (r ⊔ a ⊔ m) where
    constructor _&_&_
    inductive
    field
      lbuff : Digit Σ
      tree  : Tree ⟪ Node Σ ⟫
      rbuff : Digit Σ

  data Tree {a} (Σ : Set a) ⦃ _ : σ Σ ⦄ : Set (r ⊔ a ⊔ m) where
    empty : Tree Σ
    single : Σ → Tree Σ
    deep : ⟪ Deep Σ ⟫  → Tree Σ

  μ-deep : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → Deep Σ → 𝓡
  μ-deep (l & x & r) = μ l ∙ (μ-tree x ∙ μ r)

  μ-tree : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → Tree Σ → 𝓡
  μ-tree empty = ε
  μ-tree (single x) = μ x
  μ-tree (deep xs) = xs .𝔐

  instance
    σ-Deep : ∀ {a} {Σ : Set a} → ⦃ _ : σ Σ ⦄ → σ (Deep Σ)
    μ ⦃ σ-Deep ⦄ = μ-deep

  instance
    σ-Tree : ∀ {a} {Σ : Set a} → ⦃ _ : σ Σ ⦄ → σ (Tree Σ)
    μ ⦃ σ-Tree ⦄ = μ-tree
open Deep

{-# DISPLAY μ-tree _ x = μ x #-}
{-# DISPLAY μ-deep _ x = μ x #-}

nodeToDigit : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (xs : Node Σ) →  μ⟨ Digit Σ ⟩≈ μ xs
nodeToDigit (N₂ x₁ x₂) = D₂ x₁ x₂ ⇑[ refl ]
nodeToDigit (N₃ x₁ x₂ x₃) = D₃ x₁ x₂ x₃ ⇑[ refl ]

digitToTree : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (xs : Digit Σ) → μ⟨ Tree Σ ⟩≈ μ xs
digitToTree (D₁ x₁) = single x₁ ⇑[ refl ]
digitToTree (D₂ x₁ x₂) = deep ⟪ D₁ x₁ & empty & D₁ x₂ ⇓⟫ ⇑[ μ x₁ ∙ (ε ∙ μ x₂) ↢ ℳ ↯ ]
digitToTree (D₃ x₁ x₂ x₃) = deep ⟪ D₂ x₁ x₂ & empty & D₁ x₃ ⇓⟫ ⇑[ μ (D₂ x₁ x₂) ∙ (ε ∙ μ x₃) ↢ ℳ ↯ ]
digitToTree (D₄ x₁ x₂ x₃ x₄) = deep ⟪ D₂ x₁ x₂ & empty & D₂ x₃ x₄ ⇓⟫ ⇑[ μ (D₂ x₁ x₂) ∙ (ε ∙ μ (D₂ x₃ x₄)) ↢ ℳ ↯ ]

open import Data.List using (List; _∷_; [])

nodeToList : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (xs : Node Σ) → μ⟨ List Σ ⟩≈ (μ xs)
nodeToList (N₂ x₁ x₂) = x₁ ∷ x₂ ∷ [] ⇑[ ℳ ↯ ]
nodeToList (N₃ x₁ x₂ x₃) = x₁ ∷ x₂ ∷ x₃ ∷ [] ⇑[ ℳ ↯ ]

digitToList : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (xs : Digit Σ) → μ⟨ List Σ ⟩≈ (μ xs)
digitToList (D₁ x₁) = x₁ ∷ [] ⇑[ ℳ ↯ ]
digitToList (D₂ x₁ x₂) = x₁ ∷ x₂ ∷ [] ⇑[ ℳ ↯ ]
digitToList (D₃ x₁ x₂ x₃) = x₁ ∷ x₂ ∷ x₃ ∷ [] ⇑[ ℳ ↯ ]
digitToList (D₄ x₁ x₂ x₃ x₄) = x₁ ∷ x₂ ∷ x₃ ∷ x₄ ∷ [] ⇑[ ℳ ↯ ]

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
postulate
  foo = Foo

-- Error message is:
-- A postulate block can only contain type signatures or instance blocks


text:
module Haskell.Prim.Monoid where

open import Agda.Builtin.Unit

open import Haskell.Prim
open import Haskell.Prim.Bool
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either
open import Haskell.Prim.Tuple

--------------------------------------------------
-- Semigroup

record Semigroup (a : Set) : Set where
  infixr 6 _<>_
  field
    _<>_ : a → a → a

open Semigroup ⦃ ... ⦄ public

instance
  iSemigroupList : Semigroup (List a)
  iSemigroupList ._<>_ = _++_

  iSemigroupMaybe : ⦃ Semigroup a ⦄ → Semigroup (Maybe a)
  iSemigroupMaybe ._<>_          Nothing m = m
  iSemigroupMaybe ._<>_ m        Nothing   = m
  iSemigroupMaybe ._<>_ (Just x) (Just y)  = Just (x <> y)

  iSemigroupEither : Semigroup (Either a b)
  iSemigroupEither ._<>_ (Left _) e = e
  iSemigroupEither ._<>_ e        _ = e

  iSemigroupFun : ⦃ Semigroup b ⦄ → Semigroup (a → b)
  iSemigroupFun ._<>_ f g x = f x <> g x

  iSemigroupUnit : Semigroup ⊤
  iSemigroupUnit ._<>_ _ _ = tt

  iSemigroupTuple₀ : Semigroup (Tuple [])
  iSemigroupTuple₀ ._<>_ _ _ = []

  iSemigroupTuple : ∀ {as} → ⦃ Semigroup a ⦄ → ⦃ Semigroup (Tuple as) ⦄ → Semigroup (Tuple (a ∷ as))
  iSemigroupTuple ._<>_ (x ∷ xs) (y ∷ ys) = x <> y ∷ xs <> ys

--------------------------------------------------
-- Monoid

record Monoid (a : Set) : Set where
  field
    mempty : a
    overlap ⦃ super ⦄ : Semigroup a

  mappend : a → a → a
  mappend = _<>_

  mconcat : List a → a
  mconcat []       = mempty
  mconcat (x ∷ xs) = x <> mconcat xs

open Monoid ⦃ ... ⦄ public

instance
  iMonoidList : Monoid (List a)
  iMonoidList .mempty = []

  iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a)
  iMonoidMaybe .mempty = Nothing

  iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b)
  iMonoidFun .mempty _ = mempty

  iMonoidUnit : Monoid ⊤
  iMonoidUnit .mempty = tt

  iMonoidTuple₀ : Monoid (Tuple [])
  iMonoidTuple₀ .mempty = []

  iMonoidTuple : ∀ {as} → ⦃ Monoid a ⦄ → ⦃ Monoid (Tuple as) ⦄ → Monoid (Tuple (a ∷ as))
  iMonoidTuple .mempty = mempty ∷ mempty

MonoidEndo : Monoid (a → a)
MonoidEndo .mempty      = id
MonoidEndo .super ._<>_ = _∘_

MonoidEndoᵒᵖ : Monoid (a → a)
MonoidEndoᵒᵖ .mempty      = id
MonoidEndoᵒᵖ .super ._<>_ = flip _∘_

MonoidConj : Monoid Bool
MonoidConj .mempty      = true
MonoidConj .super ._<>_ = _&&_

MonoidDisj : Monoid Bool
MonoidDisj .mempty      = false
MonoidDisj .super ._<>_ = _||_


text:
module RewriteAndUniversePolymorphism where

open import Common.Equality

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

test : (a b : ℕ) → a ≡ b → b ≡ a
test a b eq rewrite eq = refl


text:
-- Basic intuitionistic logic of proofs, without ∨, ⊥, or +.
-- Gentzen-style formalisation of syntax with context pairs.
-- Simple terms.

module BasicILP.Syntax.DyadicGentzen where

open import BasicILP.Syntax.Common public

-- Types, or propositions.
-- [ Ψ ⁏ Ω ⊢ t ] A means t is a proof of the fact that the type A is inhabited given assumptions in the context Ψ and the modal context Ω.

mutual
  syntax □ Π A t = [ Π ⊢ t ] A

  infixr 10 □
  infixl 9 _∧_
  infixr 7 _▻_
  data Ty : Set where
    α_  : Atom → Ty
    _▻_ : Ty → Ty → Ty
    □   : (Π : Cx² Ty Box) → (A : Ty) → Π ⊢ A → Ty
    _∧_ : Ty → Ty → Ty
    ⊤  : Ty

  -- Context/modal context/type/term quadruples.

  record Box : Set where
    inductive
    constructor □
    field
      Π : Cx² Ty Box
      A : Ty
      x : Π ⊢ A

  -- Derivations.

  -- NOTE: Only var is an instance constructor, which allows the instance argument for mvar to be automatically inferred, in many cases.

  infix 3 _⊢_
  data _⊢_ : Cx² Ty Box → Ty → Set where
    instance
      var : ∀ {A Γ Δ}         → A ∈ Γ → Γ ⁏ Δ ⊢ A
    lam   : ∀ {A B Γ Δ}       → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ▻ B
    app   : ∀ {A B Γ Δ}       → Γ ⁏ Δ ⊢ A ▻ B → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B

    mvar  : ∀ {Ψ Ω A x Γ Δ}   → [ Ψ ⁏ Ω ⊢ x ] A ∈ Δ
                              → {{_ : Γ ⁏ Δ ⊢⋆ Ψ}}
                              → {{_ : Γ ⁏ Δ ⊢⍟ Ω}}
                              → Γ ⁏ Δ ⊢ A

    box   : ∀ {Ψ Ω A Γ Δ}     → (x : Ψ ⁏ Ω ⊢ A)
                              → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] A

    unbox : ∀ {Ψ Ω A C x Γ Δ} → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] A
                              → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ C
                              → Γ ⁏ Δ ⊢ C

    pair  : ∀ {A B Γ Δ}       → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ∧ B
    fst   : ∀ {A B Γ Δ}       → Γ ⁏ Δ ⊢ A ∧ B → Γ ⁏ Δ ⊢ A
    snd   : ∀ {A B Γ Δ}       → Γ ⁏ Δ ⊢ A ∧ B → Γ ⁏ Δ ⊢ B
    unit  : ∀ {Γ Δ}           → Γ ⁏ Δ ⊢ ⊤

  infix 3 _⊢⋆_
  data _⊢⋆_ : Cx² Ty Box → Cx Ty → Set where
    instance
      ∙   : ∀ {Γ Δ}     → Γ ⁏ Δ ⊢⋆ ∅
      _,_ : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢⋆ Ξ , A

  infix 3 _⊢⍟_
  data _⊢⍟_ : Cx² Ty Box → Cx Box → Set where
    instance
      ∙   : ∀ {Γ Δ}           → Γ ⁏ Δ ⊢⍟ ∅
      _,_ : ∀ {Ξ Ψ Ω A x Γ Δ} → Γ ⁏ Δ ⊢⍟ Ξ
                              → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] A
                              → Γ ⁏ Δ ⊢⍟ Ξ , [ Ψ ⁏ Ω ⊢ x ] A

-- Monotonicity with respect to context inclusion.

mutual
  mono⊢ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ A → Γ′ ⁏ Δ ⊢ A
  mono⊢ η (var i)                = var (mono∈ η i)
  mono⊢ η (lam t)                = lam (mono⊢ (keep η) t)
  mono⊢ η (app t u)              = app (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (mvar i {{ts}} {{us}}) = mvar i {{mono⊢⋆ η ts}} {{mono⊢⍟ η us}}
  mono⊢ η (box t)                = box t
  mono⊢ η (unbox t u)            = unbox (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (pair t u)             = pair (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (fst t)                = fst (mono⊢ η t)
  mono⊢ η (snd t)                = snd (mono⊢ η t)
  mono⊢ η unit                   = unit

  mono⊢⋆ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ′ ⁏ Δ ⊢⋆ Ξ
  mono⊢⋆ η ∙        = ∙
  mono⊢⋆ η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

  mono⊢⍟ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⍟ Ξ → Γ′ ⁏ Δ ⊢⍟ Ξ
  mono⊢⍟ η ∙        = ∙
  mono⊢⍟ η (ts , t) = mono⊢⍟ η ts , mono⊢ η t

-- Monotonicity with respect to modal context inclusion.

mutual
  mmono⊢ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ′ ⊢ A
  mmono⊢ θ (var i)                = var i
  mmono⊢ θ (lam t)                = lam (mmono⊢ θ t)
  mmono⊢ θ (app t u)              = app (mmono⊢ θ t) (mmono⊢ θ u)
  mmono⊢ θ (mvar i {{ts}} {{us}}) = mvar (mono∈ θ i) {{mmono⊢⋆ θ ts}} {{mmono⊢⍟ θ us}}
  mmono⊢ θ (box t)                = box t
  mmono⊢ θ (unbox t u)            = unbox (mmono⊢ θ t) (mmono⊢ (keep θ) u)
  mmono⊢ θ (pair t u)             = pair (mmono⊢ θ t) (mmono⊢ θ u)
  mmono⊢ θ (fst t)                = fst (mmono⊢ θ t)
  mmono⊢ θ (snd t)                = snd (mmono⊢ θ t)
  mmono⊢ θ unit                   = unit

  mmono⊢⋆ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ′ ⊢⋆ Ξ
  mmono⊢⋆ θ ∙        = ∙
  mmono⊢⋆ θ (ts , t) = mmono⊢⋆ θ ts , mmono⊢ θ t

  mmono⊢⍟ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⍟ Ξ → Γ ⁏ Δ′ ⊢⍟ Ξ
  mmono⊢⍟ θ ∙        = ∙
  mmono⊢⍟ θ (ts , t) = mmono⊢⍟ θ ts , mmono⊢ θ t

-- Monotonicity using context pairs.

mono²⊢ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ A → Π′ ⊢ A
mono²⊢ (η , θ) = mono⊢ η ∘ mmono⊢ θ

-- Shorthand for variables.

v₀ : ∀ {A Γ Δ} → Γ , A ⁏ Δ ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ Δ} → Γ , A , B ⁏ Δ ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ Δ} → Γ , A , B , C ⁏ Δ ⊢ A
v₂ = var i₂

mv₀ : ∀ {Ψ Ω A x Γ Δ}
      → {{_ : Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢⋆ Ψ}}
      → {{_ : Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢⍟ Ω}}
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ A
mv₀ = mvar i₀

mv₁ : ∀ {Ψ Ψ′ Ω Ω′ A B x y Γ Δ}
      → {{_ : Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A , [ Ψ′ ⁏ Ω′ ⊢ y ] B ⊢⋆ Ψ}}
      → {{_ : Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A , [ Ψ′ ⁏ Ω′ ⊢ y ] B ⊢⍟ Ω}}
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A , [ Ψ′ ⁏ Ω′ ⊢ y ] B ⊢ A
mv₁ = mvar i₁

mv₂ : ∀ {Ψ Ψ′ Ψ″ Ω Ω′ Ω″ A B C x y z Γ Δ}
      → {{_ : Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A , [ Ψ′ ⁏ Ω′ ⊢ y ] B , [ Ψ″ ⁏ Ω″ ⊢ z ] C ⊢⋆ Ψ}}
      → {{_ : Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A , [ Ψ′ ⁏ Ω′ ⊢ y ] B , [ Ψ″ ⁏ Ω″ ⊢ z ] C ⊢⍟ Ω}}
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A , [ Ψ′ ⁏ Ω′ ⊢ y ] B , [ Ψ″ ⁏ Ω″ ⊢ z ] C ⊢ A
mv₂ = mvar i₂

-- Generalised reflexivity.

instance
  refl⊢⋆ : ∀ {Γ Ψ Δ} → {{_ : Ψ ⊆ Γ}} → Γ ⁏ Δ ⊢⋆ Ψ
  refl⊢⋆ {∅}     {{done}}   = ∙
  refl⊢⋆ {Γ , A} {{skip η}} = mono⊢⋆ weak⊆ (refl⊢⋆ {{η}})
  refl⊢⋆ {Γ , A} {{keep η}} = mono⊢⋆ weak⊆ (refl⊢⋆ {{η}}) , v₀

  mrefl⊢⍟ : ∀ {Δ Ω Γ} → {{_ : Ω ⊆ Δ}} → Γ ⁏ Δ ⊢⍟ Ω
  mrefl⊢⍟ {∅}                     {{done}}   = ∙
  mrefl⊢⍟ {Δ , [ Ψ ⁏ Ω ⊢ x ] A } {{skip θ}} = mmono⊢⍟ weak⊆ (mrefl⊢⍟ {{θ}})
  mrefl⊢⍟ {Δ , [ Ψ ⁏ Ω ⊢ x ] A } {{keep θ}} = mmono⊢⍟ weak⊆ (mrefl⊢⍟ {{θ}}) , box x

-- Deduction theorem is built-in.

-- Modal deduction theorem.

mlam : ∀ {Ψ Ω A B x Γ Δ}
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ B
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] A ▻ B
mlam t = lam (unbox v₀ (mono⊢ weak⊆ t))

-- Detachment theorems.

det : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B → Γ , A ⁏ Δ ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

-- FIXME: Is this correct?
mdet : ∀ {Ψ Ω A B x Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] A ▻ B
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ B
mdet {x = x} t = app (mmono⊢ weak⊆ t) (box x)

-- Cut and multicut.

cut : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ B
cut t u = app (lam u) t

mcut : ∀ {Ψ Ω A B x Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] A
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ B
      → Γ ⁏ Δ ⊢ B
mcut t u = app (mlam u) t

multicut : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Ξ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A
multicut ∙        u = mono⊢ bot⊆ u
multicut (ts , t) u = app (multicut ts (lam u)) t

-- Contraction.

ccont : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ Δ} → Γ , A , A ⁏ Δ ⊢ B → Γ , A ⁏ Δ ⊢ B
cont t = det (app ccont (lam (lam t)))

mcont : ∀ {Ψ Ω A B x Γ Δ}
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A , [ Ψ ⁏ Ω ⊢ x ] A ⊢ B
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ B
mcont t = mdet (app ccont (mlam (mlam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ Δ} → Γ , A , B ⁏ Δ ⊢ C → Γ , B , A ⁏ Δ ⊢ C
exch t = det (det (app cexch (lam (lam t))))

mexch : ∀ {Ψ Ψ′ Ω Ω′ A B C x y Γ Δ}
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A , [ Ψ′ ⁏ Ω′ ⊢ y ] B ⊢ C
      → Γ ⁏ Δ , [ Ψ′ ⁏ Ω′ ⊢ y ] B , [ Ψ ⁏ Ω ⊢ x ] A ⊢ C
mexch t = mdet (mdet (app cexch (mlam (mlam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ Δ} → Γ , B ⁏ Δ ⊢ C → Γ , A ⁏ Δ ⊢ B → Γ , A ⁏ Δ ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

mcomp : ∀ {Ψ Ψ′ Ψ″ Ω Ω′ Ω″ A B C x y z Γ Δ}
      → Γ ⁏ Δ , [ Ψ′ ⁏ Ω′ ⊢ y ] B ⊢ [ Ψ″ ⁏ Ω″ ⊢ z ] C
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ [ Ψ′ ⁏ Ω′ ⊢ y ] B
      → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ [ Ψ″ ⁏ Ω″ ⊢ z ] C
mcomp t u = mdet (app (app ccomp (mlam t)) (mlam u))

-- Useful theorems in functional form.

dist : ∀ {Ψ Ω A B x y Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] (A ▻ B)
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ y ] A
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω , [ Ψ ⁏ Ω ⊢ x ] (A ▻ B) , [ Ψ ⁏ Ω ⊢ y ] A ⊢ app mv₁ mv₀ ] B
dist t u = unbox t (unbox (mmono⊢ weak⊆ u) (box
             (app mv₁ mv₀)))

up : ∀ {Ψ Ω A x Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] A
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ box mv₀ ] [ Ψ ⁏ Ω , [ Ψ ⁏ Ω ⊢ x ] A ⊢ mv₀ ] A
up t = unbox t (box (box mv₀))

down : ∀ {Ψ Ω A x Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ x ] A
      → {{_ : Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢⋆ Ψ}}
      → {{_ : Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢⍟ Ω}}
      → Γ ⁏ Δ ⊢ A
down t = unbox t mv₀

-- Useful theorems in combinatory form.

ci : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A ▻ A
ci = lam v₀

ck : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B ▻ A
ck = lam (lam v₁)

cs : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
cs = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

cdist : ∀ {Ψ Ω A B t u Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ t ] (A ▻ B) ▻
                  [ Ψ ⁏ Ω ⊢ u ] A ▻
                  [ Ψ ⁏ Ω , [ Ψ ⁏ Ω ⊢ t ] (A ▻ B) , [ Ψ ⁏ Ω ⊢ u ] A ⊢ app mv₁ mv₀ ] B
cdist = lam (lam (dist v₁ v₀))

cup : ∀ {Ψ Ω A t Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ t ] A ▻
                  [ Ψ ⁏ Ω ⊢ box mv₀ ] [ Ψ ⁏ Ω , [ Ψ ⁏ Ω ⊢ t ] A ⊢ mv₀ ] A
cup = lam (up v₀)

cunbox : ∀ {Ψ Ω A C t Γ Δ} → Γ ⁏ Δ ⊢ [ Ψ ⁏ Ω ⊢ t ] A ▻ ([ Ψ ⁏ Ω ⊢ t ] A ▻ C) ▻ C
cunbox = lam (lam (app v₀ v₁))

cpair : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B ▻ A ∧ B
cpair = lam (lam (pair v₁ v₀))

cfst : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B ▻ A
cfst = lam (fst v₀)

csnd : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B ▻ B
csnd = lam (snd v₀)

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ {Δ} → Γ , A ⁏ Δ ⊢ B → Γ′ ⁏ Δ ⊢ A → Γ ⧺ Γ′ ⁏ Δ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

mconcat : ∀ {Ψ Ω A B t Γ Δ} Δ′ → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ t ] A ⊢ B → Γ ⁏ Δ′ ⊢ [ Ψ ⁏ Ω ⊢ t ] A → Γ ⁏ Δ ⧺ Δ′ ⊢ B
mconcat Δ′ t u = app (mmono⊢ (weak⊆⧺₁ Δ′) (mlam t)) (mmono⊢ weak⊆⧺₂ u)

-- Substitution.

mutual
  [_≔_]_ : ∀ {A C Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ C → Γ ∖ i ⁏ Δ ⊢ C
  [ i ≔ s ] var j                with i ≟∈ j
  [ i ≔ s ] var .i               | same   = s
  [ i ≔ s ] var ._               | diff j = var j
  [ i ≔ s ] lam t                = lam ([ pop i ≔ mono⊢ weak⊆ s ] t)
  [ i ≔ s ] app t u              = app ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] mvar j {{ts}} {{us}} = mvar j {{[ i ≔ s ]⋆ ts}} {{[ i ≔ s ]⍟ us}}
  [ i ≔ s ] box t                = box t
  [ i ≔ s ] unbox t u            = unbox ([ i ≔ s ] t) ([ i ≔ mmono⊢ weak⊆ s ] u)
  [ i ≔ s ] pair t u             = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] fst t                = fst ([ i ≔ s ] t)
  [ i ≔ s ] snd t                = snd ([ i ≔ s ] t)
  [ i ≔ s ] unit                 = unit

  [_≔_]⋆_ : ∀ {Ξ A Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢⋆ Ξ → Γ ∖ i ⁏ Δ ⊢⋆ Ξ
  [_≔_]⋆_ i s ∙        = ∙
  [_≔_]⋆_ i s (ts , t) = [ i ≔ s ]⋆ ts , [ i ≔ s ] t

  [_≔_]⍟_ : ∀ {Ξ A Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢⍟ Ξ → Γ ∖ i ⁏ Δ ⊢⍟ Ξ
  [_≔_]⍟_ i s ∙        = ∙
  [_≔_]⍟_ i s (ts , t) = [ i ≔ s ]⍟ ts , [ i ≔ s ] t

-- Modal substitution.

mutual
  m[_≔_]_ : ∀ {Ψ Ω A C t Γ Δ} → (i : [ Ψ ⁏ Ω ⊢ t ] A ∈ Δ) → Ψ ⁏ Δ ∖ i ⊢ A → Γ ⁏ Δ ⊢ C → Γ ⁏ Δ ∖ i ⊢ C
  m[ i ≔ s ] var j                 = var j
  m[ i ≔ s ] lam t                 = lam (m[ i ≔ s ] t)
  m[ i ≔ s ] app t u               = app (m[ i ≔ s ] t) (m[ i ≔ s ] u)
  m[ i ≔ s ] mvar j  {{ts}} {{us}} with i ≟∈ j
  m[ i ≔ s ] mvar .i {{ts}} {{us}} | same   = multicut (m[ i ≔ s ]⋆ ts) s
  m[ i ≔ s ] mvar ._ {{ts}} {{us}} | diff j = mvar j {{m[ i ≔ s ]⋆ ts}} {{m[ i ≔ s ]⍟ us}}
  m[ i ≔ s ] box t                 = box t
  m[ i ≔ s ] unbox t u             = unbox (m[ i ≔ s ] t) (m[ pop i ≔ mmono⊢ weak⊆ s ] u)
  m[ i ≔ s ] pair t u              = pair (m[ i ≔ s ] t) (m[ i ≔ s ] u)
  m[ i ≔ s ] fst t                 = fst (m[ i ≔ s ] t)
  m[ i ≔ s ] snd t                 = snd (m[ i ≔ s ] t)
  m[ i ≔ s ] unit                  = unit

  m[_≔_]⋆_ : ∀ {Ξ Ψ Ω A t Γ Δ} → (i : [ Ψ ⁏ Ω ⊢ t ] A ∈ Δ) → Ψ ⁏ Δ ∖ i ⊢ A → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ∖ i ⊢⋆ Ξ
  m[_≔_]⋆_ i s ∙        = ∙
  m[_≔_]⋆_ i s (ts , t) = m[ i ≔ s ]⋆ ts , m[ i ≔ s ] t

  m[_≔_]⍟_ : ∀ {Ξ Ψ Ω A t Γ Δ} → (i : [ Ψ ⁏ Ω ⊢ t ] A ∈ Δ) → Ψ ⁏ Δ ∖ i ⊢ A → Γ ⁏ Δ ⊢⍟ Ξ → Γ ⁏ Δ ∖ i ⊢⍟ Ξ
  m[_≔_]⍟_ i s ∙        = ∙
  m[_≔_]⍟_ i s (ts , t) = m[ i ≔ s ]⍟ ts , m[ i ≔ s ] t

-- TODO: Convertibility.

-- Examples from the Nanevski-Pfenning-Pientka paper.

-- NOTE: In many cases, the instance argument for mvar can be automatically inferred, but not always.

module Examples₁ where
  e₁ : ∀ {A C D Γ Δ t}
        → Γ ⁏ Δ ⊢ [ ∅ , C ⁏ Δ ⊢ t ] A ▻
                    [ ∅ , C , D ⁏ Δ , [ ∅ , C ⁏ Δ ⊢ t ] A ⊢ mv₀ ] A
  e₁ = lam (unbox v₀ (box mv₀))

  e₂ : ∀ {A C Γ Δ t}
        → Γ ⁏ Δ ⊢ [ ∅ , C , C ⁏ Δ ⊢ t ] A ▻
                    [ ∅ , C ⁏ Δ , [ ∅ , C , C ⁏ Δ ⊢ t ] A ⊢ mv₀ ] A
  e₂ = lam (unbox v₀ (box mv₀))

  e₃ : ∀ {A Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ , A ⁏ Δ ⊢ v₀ ] A
  e₃ = box v₀

  e₄ : ∀ {A B C Γ Δ t u v}
        → Γ ⁏ Δ ⊢ [ ∅ , A ⁏ Δ ⊢ t ] B ▻
                    [ ∅ , A ⁏ Δ ⊢ v ] [ ∅ , B ⁏ Δ ⊢ u ] C ▻
                    [ ∅ , A ⁏ Δ , [ ∅ , A ⁏ Δ ⊢ t ] B
                                , [ ∅ , A ⁏ Δ ⊢ v ] [ ∅ , B ⁏ Δ ⊢ u ] C
                                ⊢ unbox mv₀ (mv₀ {{∙ , mv₂}}) ] C
  e₄ = lam (lam (unbox v₁ (unbox v₀ (box
         (unbox mv₀ (mv₀ {{∙ , mv₂}}))))))

  e₅ : ∀ {A Γ Δ t}
        → Γ ⁏ Δ ⊢ [ ∅ ⁏ Δ ⊢ t ] A ▻ A
  e₅ = lam (unbox v₀ mv₀)

  e₆ : ∀ {A C D Γ Δ t}
        → Γ ⁏ Δ ⊢ [ ∅ , C ⁏ Δ ⊢ t ] A ▻
                    [ ∅ , D ⁏ Δ ⊢ box mv₀ ]
                      [ ∅ , C ⁏ Δ , [ ∅ , C ⁏ Δ ⊢ t ]
                        A ⊢ mv₀ ] A
  e₆ = lam (unbox v₀ (box (box mv₀)))

  e₇ : ∀ {A B C D Γ Δ t u}
        → Γ ⁏ Δ ⊢ [ ∅ , C ⁏ Δ ⊢ t ] (A ▻ B) ▻
                    [ ∅ , D ⁏ Δ ⊢ u ] A ▻
                    [ ∅ , C , D ⁏ Δ , [ ∅ , C ⁏ Δ ⊢ t ] (A ▻ B)
                                    , [ ∅ , D ⁏ Δ ⊢ u ] A
                                    ⊢ app mv₁ mv₀ ] B
  e₇ = lam (lam (unbox v₁ (unbox v₀ (box
         (app mv₁ mv₀)))))

  e₈ : ∀ {A B C Γ Δ t u}
        → Γ ⁏ Δ ⊢ [ ∅ , A ⁏ Δ ⊢ t ] (A ▻ B) ▻
                    [ ∅ , B ⁏ Δ ⊢ u ] C ▻
                    [ ∅ , A ⁏ Δ , [ ∅ , A ⁏ Δ ⊢ t ] (A ▻ B)
                                , [ ∅ , B ⁏ Δ ⊢ u ] C
                                ⊢ mv₀ {{∙ , app mv₁ v₀}} ] C
  e₈ = lam (lam (unbox v₁ (unbox v₀ (box
         (mv₀ {{∙ , app mv₁ v₀}})))))

-- Examples from the Alt-Artemov paper.

module Examples₂ where
  e₁ : ∀ {A Γ Δ t}
        → Γ ⁏ Δ ⊢ [ ∅ ⁏ Δ ⊢ lam (down v₀) ]
                      ([ ∅ ⁏ Δ ⊢ t ] A ▻ A)
  e₁ = box (lam (down v₀))

  e₂ : ∀ {A Γ Δ t}
        → Γ ⁏ Δ ⊢ [ ∅ ⁏ Δ ⊢ lam (up v₀) ]
                      ([ ∅ ⁏ Δ ⊢ t ] A ▻
                       [ ∅ ⁏ Δ ⊢ box mv₀ ]
                         [ ∅ ⁏ Δ , [ ∅ ⁏ Δ ⊢ t ]
                           A ⊢ mv₀ ] A)
  e₂ = box (lam (up v₀))

  e₃ : ∀ {A B Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ ⁏ Δ ⊢ box (lam (lam (pair v₁ v₀))) ]
                      [ ∅ ⁏ Δ ⊢ lam (lam (pair v₁ v₀)) ]
                        (A ▻ B ▻ A ∧ B)
  e₃ = box (box (lam (lam (pair v₁ v₀))))

  e₄ : ∀ {A B Γ Δ t u}
        → Γ ⁏ Δ ⊢ [ ∅ ⁏ Δ ⊢ lam (lam (unbox v₁ (unbox v₀ (box
                                 (box (pair mv₁ mv₀)))))) ]
                      ([ ∅ ⁏ Δ ⊢ t ] A ▻
                       [ ∅ ⁏ Δ ⊢ u ] B ▻
                       [ ∅ ⁏ Δ ⊢ box (pair mv₁ mv₀) ]
                         [ ∅ ⁏ Δ , [ ∅ ⁏ Δ ⊢ t ] A
                                 , [ ∅ ⁏ Δ ⊢ u ] B
                                 ⊢ pair mv₁ mv₀ ]
                           (A ∧ B))
  e₄ = box (lam (lam (unbox v₁ (unbox v₀ (box
         (box (pair mv₁ mv₀)))))))

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen