text:
open import Data.List renaming (_∷_ to _∷ₗ_ ; [_] to [_]ₗ)
open import Data.Maybe
open import Data.Product
open import Data.Sum

open import AEff
open import EffectAnnotations
open import Preservation
open import Renamings
open import Substitutions
open import Types

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary

module ProcessPreservation where

-- REDUCTION OF PROCESS TYPES

infix 10 _⇝_

data _⇝_ : {o o' : O} → PType o → PType o' → Set where

  id  : {X : VType}
        {o : O}
        {i : I} →
        ----------------------
        X ‼ o , i ⇝ X ‼ o , i

  act : {X : VType}
        {o o' o'' : O}
        {i i' i'' : I} →
        (ops : List Σₛ) →
        (op : Σₛ) →
        (o' , i') ≡ ops ↓↓ₑ (o , i) →
        (o'' , i'') ≡ ((ops ++ [ op ]ₗ) ↓↓ₑ (o , i)) →
        ----------------------------------------------
        (X ‼ o' , i') ⇝ (X ‼ o'' , i'')

  par : {o o' o'' o''' : O}
        {PP : PType o}
        {QQ : PType o'}
        {PP' : PType o''}
        {QQ' : PType o'''} →
        PP ⇝ PP' →
        QQ ⇝ QQ' →
        ----------------------
        (PP ∥ QQ) ⇝ (PP' ∥ QQ')

-- REDUCTION OF PROCESS TYPES IS REFLEXIVE

{- LEMMA 4.4 (1) -}

⇝-refl : {o : O} {PP : PType o} → PP ⇝ PP
⇝-refl {o} {X ‼ o , i} =
  id
⇝-refl {.(_ ∪ₒ _)} {PP ∥ QQ} =
  par ⇝-refl ⇝-refl

-- ACTION OF INTERRUPTS ON GENERAL PROCESS TYPES IS A REDUCTION

{- LEMMA 4.4 (2) -}

⇝-↓ₚ : {o : O}
       {PP : PType o}
       {op : Σₛ} →
       --------------
       PP ⇝ op ↓ₚ PP

⇝-↓ₚ {.o} {X ‼ o , i} {op} =
  act [] op refl refl
⇝-↓ₚ {.(_ ∪ₒ _)} {PP ∥ QQ} {op} =
  par ⇝-↓ₚ ⇝-↓ₚ

-- ACTION OF INTERRUPTS PRESERVES PROCESS TYPE REDUCTION

{- LEMMA 4.4 (3) -}

⇝-↓ₚ-cong : {o o' : O}
            {PP : PType o}
            {QQ : PType o'}
            {op : Σₛ} →
            PP ⇝ QQ →
            --------------------
            op ↓ₚ PP ⇝ op ↓ₚ QQ

⇝-↓ₚ-cong id =
  id
⇝-↓ₚ-cong {_} {_} {_} {_} {op} (act {_} {o} {o'} {o''} {i} {i'} {i''} ops op' p q) =
  act {o = o} {i = i} (op ∷ₗ ops) op' (cong (λ oi → op ↓ₑ oi) p) (cong (λ oi → op ↓ₑ oi) q)
⇝-↓ₚ-cong (par p q) =
  par (⇝-↓ₚ-cong p) (⇝-↓ₚ-cong q)

-- PROCESS TYPE REDUCTION INCREASES SIGNAL INDEX

{- LEMMA 4.4 (4) -}

inj-proj₁ : {X Y : Set} {xy xy' : X × Y} → xy ≡ xy' → proj₁ xy ≡ proj₁ xy'
inj-proj₁ refl = refl

⇝-⊑ₒ : {o o' : O}
       {PP : PType o}
       {QQ : PType o'} →
       PP ⇝ QQ →
       ------------------
       o ⊑ₒ o'

⇝-⊑ₒ id =
  ⊑ₒ-refl
⇝-⊑ₒ (act {_} {o} {o'} {o''} {i} ops op p q) with inj-proj₁ p | inj-proj₁ q
... | r | s =
  subst (λ o → o ⊑ₒ o'')
        (sym r)
        (subst (λ o'' → proj₁ (ops ↓↓ₑ (o , i)) ⊑ₒ o'')
               (sym s)
               (subst (λ v → proj₁ (ops ↓↓ₑ (o , i)) ⊑ₒ proj₁ v)
                      (sym (↓↓ₑ-act ops [ op ]ₗ))
                      (↓↓ₑ-⊑ₒ-act ops op)))
⇝-⊑ₒ (par p q) =
  ∪ₒ-fun (⇝-⊑ₒ p) (⇝-⊑ₒ q)

-- EVALUATION CONTEXTS FOR PROCESSES

infix 10 _⊢F⦂_

data _⊢F⦂_ (Γ : Ctx) : {o : O} → PType o → Set where

  [-]     : {o : O} →
            {PP : PType o} →
            --------------
            Γ ⊢F⦂ PP

  _∥ₗ_    : {o o' : O}
            {PP : PType o}
            {QQ : PType o'} →
            Γ ⊢F⦂ PP →
            Γ ⊢P⦂ QQ →
            ------------------
            Γ ⊢F⦂ (PP ∥ QQ)

  _∥ᵣ_    : {o o' : O}
            {PP : PType o}
            {QQ : PType o'} →
            Γ ⊢P⦂ PP →
            Γ ⊢F⦂ QQ →
            ------------------
            Γ ⊢F⦂ (PP ∥ QQ)

  ↑       : {o : O}
            {PP : PType o}  →
            (op : Σₛ) →
            op ∈ₒ o →
            Γ ⊢V⦂ ``(payload op) →
            Γ ⊢F⦂ PP →
            ----------------------
            Γ ⊢F⦂ PP

  ↓       : {o : O}
            {PP : PType o}
            (op : Σₛ) →
            Γ ⊢V⦂ ``(payload op) →
            Γ ⊢F⦂ PP →
            ----------------------
            Γ ⊢F⦂ op ↓ₚ PP

-- FINDING THE TYPE OF THE HOLE OF A WELL-TYPED PROCESS EVALUATION CONTEXT

hole-ty-f : {Γ : Ctx} {o : O} {PP : PType o} → Γ ⊢F⦂ PP → Σ[ o' ∈ O ] (PType o')
hole-ty-f {_} {o} {PP} [-] =
  o , PP
hole-ty-f (_∥ₗ_ {o} {o'} {PP} {QQ} F Q) =
  proj₁ (hole-ty-f F) , proj₂ (hole-ty-f F)
hole-ty-f (_∥ᵣ_ {o} {o'} {PP} {QQ} P F) =
  proj₁ (hole-ty-f F) , proj₂ (hole-ty-f F)
hole-ty-f (↑ op p V F) =
  proj₁ (hole-ty-f F) , proj₂ (hole-ty-f F)
hole-ty-f (↓ op V F) =
  proj₁ (hole-ty-f F) , proj₂ (hole-ty-f F)

-- FILLING A WELL-TYPED PROCESS EVALUATION CONTEXT

infix 30 _[_]f

_[_]f : {Γ : Ctx} {o : O} {PP : PType o} → (F : Γ ⊢F⦂ PP) → (P : Γ ⊢P⦂ proj₂ (hole-ty-f F)) → Γ ⊢P⦂ PP
[-] [ P ]f =
  P
(F ∥ₗ Q) [ P ]f =
  (F [ P ]f) ∥ Q
(Q ∥ᵣ F) [ P ]f =
  Q ∥ (F [ P ]f)
(↑ op p V F) [ P ]f =
  ↑ op p V (F [ P ]f)
(↓ op V F) [ P ]f =
  ↓ op V (F [ P ]f)

-- TYPES OF WELL-TYPED PROCESS EVALUATION CONTEXTS ALSO REDUCE

⇝-f-⇝ : {Γ : Ctx}
        {o o' : O}
        {PP : PType o}
        {QQ : PType o'} →
        (F : Γ ⊢F⦂ PP) →
        proj₂ (hole-ty-f F) ⇝ QQ →
        ------------------------------------------
        Σ[ o'' ∈ O ] Σ[ RR ∈ PType o'' ] (PP ⇝ RR)

⇝-f-⇝ {_} {_} {o'} {_} {QQ} [-] p =
  o' , QQ , p
⇝-f-⇝ (_∥ₗ_ {o} {o'} {PP} {QQ} F Q) p with ⇝-f-⇝ F p
... | o'' , RR , q =
  (o'' ∪ₒ o') , (RR ∥ QQ) , par q ⇝-refl
⇝-f-⇝ (_∥ᵣ_ {o} {o'} {PP} {QQ} P F) p with ⇝-f-⇝ F p
... | o'' , RR , q =
  (o ∪ₒ o'') , (PP ∥ RR) , par ⇝-refl q
⇝-f-⇝ (↑ op p V F) q with ⇝-f-⇝ F q
... | o'' , RR , r =
  o'' , RR , r
⇝-f-⇝ (↓ op V F) p with ⇝-f-⇝ F p
... | o'' , RR , q =
  proj₁ (op ↓ₚₚ RR) , (op ↓ₚ RR) , ⇝-↓ₚ-cong q

⇝-f-∈ₒ : {Γ : Ctx}
         {o o' : O}
         {PP : PType o}
         {QQ : PType o'}
         (F : Γ ⊢F⦂ PP) →
         (p : proj₂ (hole-ty-f F) ⇝ QQ) →
         --------------------------------
         o ⊑ₒ proj₁ (⇝-f-⇝ F p)

⇝-f-∈ₒ [-] p =
  ⇝-⊑ₒ p
⇝-f-∈ₒ (F ∥ₗ Q) p =
  ∪ₒ-fun (⇝-f-∈ₒ F p) ⊑ₒ-refl
⇝-f-∈ₒ (P ∥ᵣ F) p =
  ∪ₒ-fun ⊑ₒ-refl (⇝-f-∈ₒ F p)
⇝-f-∈ₒ (↑ op p V F) q =
  ⇝-f-∈ₒ F q
⇝-f-∈ₒ (↓ {o} {PP} op V F) p =
  ⇝-f-∈ₒ-aux (⇝-f-⇝ F p) refl

  where
    ⇝-f-∈ₒ-aux : (orp : Σ[ o'' ∈ O ] Σ[ RR ∈ PType o'' ] (PP ⇝ RR)) →
                 orp ≡ ⇝-f-⇝ F p →
                 ----------------------------------------------------
                 proj₁ (op ↓ₚₚ PP) ⊑ₒ proj₁ (op ↓ₚₚ proj₁ (proj₂ orp))

    ⇝-f-∈ₒ-aux (o'' , RR , r) q =
      ⇝-⊑ₒ (⇝-↓ₚ-cong r)

{- LEMMA 4.6 -}

⇝-f : {Γ : Ctx}
      {o o' : O}
      {PP : PType o}
      {QQ : PType o'} →
      (F : Γ ⊢F⦂ PP) →
      (p : proj₂ (hole-ty-f F) ⇝ QQ) →
      ---------------------------------
      Γ ⊢F⦂ (proj₁ (proj₂ (⇝-f-⇝ F p)))

⇝-f [-] p =
  [-]
⇝-f (F ∥ₗ Q) p with ⇝-f F p
... | q =
  q ∥ₗ Q
⇝-f (Q ∥ᵣ F) p with ⇝-f F p
... | q =
  Q ∥ᵣ q
⇝-f (↑ op p V F) q with ⇝-f F q
... | r =
  ↑ op (⇝-f-∈ₒ F q op p) V r
⇝-f (↓ op V F) p with ⇝-f F p
... | q =
  ↓ op V q

⇝-f-tyₒ : {Γ : Ctx}
          {o o' : O}
          {PP : PType o}
          {QQ : PType o'} →
          (F : Γ ⊢F⦂ PP) →
          (p : proj₂ (hole-ty-f F) ⇝ QQ) →
          --------------------------------
          o' ≡ proj₁ (hole-ty-f (⇝-f F p))

⇝-f-tyₒ [-] p =
  refl
⇝-f-tyₒ (F ∥ₗ Q) p =
  ⇝-f-tyₒ F p
⇝-f-tyₒ (P ∥ᵣ F) p =
  ⇝-f-tyₒ F p
⇝-f-tyₒ (↑ op p V F) q =
  ⇝-f-tyₒ F q
⇝-f-tyₒ (↓ op V F) p =
  ⇝-f-tyₒ F p

⇝-f-ty : {Γ : Ctx}
         {o o' : O}
         {PP : PType o}
         {QQ : PType o'} →
         (F : Γ ⊢F⦂ PP) →
         (p : proj₂ (hole-ty-f F) ⇝ QQ) →
         --------------------------------------
         subst (λ o → PType o) (⇝-f-tyₒ F p) QQ
         ≡
         proj₂ (hole-ty-f (⇝-f F p))

⇝-f-ty [-] p =
  refl
⇝-f-ty (F ∥ₗ Q) p =
  ⇝-f-ty F p
⇝-f-ty (P ∥ᵣ F) p =
  ⇝-f-ty F p
⇝-f-ty (↑ op p V F) q =
  ⇝-f-ty F q
⇝-f-ty (↓ op V F) p =
  ⇝-f-ty F p

-- AUXILIARY TWO-LEVEL INDEXED SUBSTITUTION

subst-i : {X : Set} {x x' : X} → (Y : X → Set) → {y : Y x} {y' : Y x'} →
          (Z : (x : X) → Y x → Set) → (p : x ≡ x') → subst Y p y ≡ y' → Z x y → Z x' y'
subst-i Y Z refl refl z = z

-- SMALL-STEP OPERATIONAL SEMANTICS FOR WELL-TYPED PROCESSES
-- (ADDITIONALLY SERVES AS THE PRESERVATION THEOREM)

{- THEOREM 4.7 -}

infix 10 _[_]↝_

data _[_]↝_ {Γ : Ctx} : {o o' : O} {PP : PType o} {QQ : PType o'} → Γ ⊢P⦂ PP → PP ⇝ QQ → Γ ⊢P⦂ QQ → Set where

  -- RUNNING INDIVIDUAL COMPUTATIONS

  run     : {X : VType}
            {o : O}
            {i : I}
            {M N : Γ ⊢M⦂ X ! (o , i)} →
            M ↝ N →
            ---------------------------
            (run M) [ id ]↝ (run N)

  -- BROADCAST RULES

  ↑-∥ₗ    : {o o' : O}
            {PP : PType o}
            {QQ : PType o'}
            {op : Σₛ} →
            (p : op ∈ₒ o) →
            (V : Γ ⊢V⦂ `` (payload op)) →
            (P : Γ ⊢P⦂ PP) →
            (Q : Γ ⊢P⦂ QQ) →
            ------------------------------------------
            ((↑ op p V P) ∥ Q)
            [ par ⇝-refl (⇝-↓ₚ {op = op}) ]↝
            ↑ op (∪ₒ-inl op p) V (P ∥ ↓ op V Q)

  ↑-∥ᵣ    : {o o' : O}
            {PP : PType o}
            {QQ : PType o'}
            {op : Σₛ} →
            (p : op ∈ₒ o') →
            (V : Γ ⊢V⦂ `` (payload op)) →
            (P : Γ ⊢P⦂ PP) →
            (Q : Γ ⊢P⦂ QQ) →
            ------------------------------------------
            (P ∥ (↑ op p V Q))
            [ par (⇝-↓ₚ {op = op}) ⇝-refl ]↝
            ↑ op (∪ₒ-inr op p) V (↓ op V P ∥ Q)

  -- INTERRUPT PROPAGATION RULES

  ↓-run   : {X : VType}
            {o : O}
            {i : I}
            {op : Σₛ} →
            (V : Γ ⊢V⦂ `` (payload op)) →
            (M : Γ ⊢M⦂ X ! (o , i)) →
            -----------------------------
            ↓ op V (run M)
            [ id ]↝
            run (↓ op V M)

  ↓-∥     : {o o' : O}
            {PP : PType o}
            {QQ : PType o'}
            {op : Σₛ}
            (V : Γ ⊢V⦂ `` (payload op)) →
            (P : Γ ⊢P⦂ PP) →
            (Q : Γ ⊢P⦂ QQ) →
            -----------------------------
            ↓ op V (P ∥ Q)
            [ ⇝-refl ]↝
            ((↓ op V P) ∥ (↓ op V Q))

  ↓-↑     : {o : O}
            {PP : PType o}
            {op : Σₛ}
            {op' : Σₛ} →
            (p : op' ∈ₒ o) →
            (V : Γ ⊢V⦂ ``(payload op)) →
            (W : Γ ⊢V⦂ ``(payload op')) →
            (P : Γ ⊢P⦂ PP) →
            -----------------------------------
            ↓ op V (↑ op' p W P)
            [ ⇝-refl ]↝
            ↑ op' (↓ₚₚ-⊑ₒ PP op' p) W (↓ op V P)

  -- SIGNAL HOISTING RULE

  ↑       : {X : VType}
            {o : O}
            {i : I} →
            {op : Σₛ} →
            (p : op ∈ₒ o) →
            (V : Γ ⊢V⦂ `` (payload op)) →
            (M : Γ ⊢M⦂ X ! (o , i)) →
            -----------------------------
            run (↑ op p V M)
            [ id ]↝
            ↑ op p V (run M)

  -- EVALUATION CONTEXT RULE

  context : {o o' : O}
            {PP : PType o}
            {QQ : PType o'}
            (F : Γ ⊢F⦂ PP) →
            {P : Γ ⊢P⦂ proj₂ (hole-ty-f F)}
            {Q : Γ ⊢P⦂ QQ}
            {r : proj₂ (hole-ty-f F) ⇝ QQ} →
            P [ r ]↝ Q →
            -----------------------------------------------------------------------------
            F [ P ]f
            [ proj₂ (proj₂ (⇝-f-⇝ F r)) ]↝
            (⇝-f F r) [ subst-i PType (λ o QQ → Γ ⊢P⦂ QQ) (⇝-f-tyₒ F r) (⇝-f-ty F r) Q ]f

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


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

module TheSame where

open import Level using (_⊔_) renaming (zero to l0; suc to lsuc)
open import Universe using (Universe)

open import Categories.Category using (Category)
open import Categories.Groupoid using (Groupoid)
open import Categories.Functor using (Functor)

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum hiding ([_,_])
open import Data.Product
open import Relation.Binary.PropositionalEquality as P
open import Function using (flip)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Integer using (+_)

open import Categories.Groupoid.Sum using () renaming (Sum to GSum)
open import Categories.Groupoid.Product using () renaming (Product to GProduct)

open import PiU using (U; ZERO; ONE; PLUS; TIMES; toℕ)
open import PiLevel0
open import PiLevel1
open import PiEquiv
open import Equiv

open import PiIter

-- our values come in three flavours, base, up and down (i.e. #p and 1/# p)
data Flavour : Set where
  base up down : Flavour

-- all our values will be 'subtypes' of this:
record V (fl : Flavour) (t₀ t₁ : U) (p : t₁ ⟷ t₁) : Set where
  constructor v
  field
    pt : ⟦ t₀ ⟧
    auto : Iter p

-- we need t₀ and t₁ to potentially be different to embed
-- #p and 1/#p.  The values of these are the same, but
-- the homomorphisms will be different, and thus how to count them.

-- We can embed our (current) values into V easily:
embedBase : {t : U} → ⟦ t ⟧ → V base t ONE id⟷
embedBase w = v w (iter (+ 0) id⟷ id⇔)

embed#p : {t : U} → {p : t ⟷ t} → Iter p → V up ONE t p
embed#p it = v tt it

embed1/#p : {t : U} → {p : t ⟷ t} → Iter p → V down ONE t p
embed1/#p it = v tt it

-- We can then define combinators on V as two actions, one on each part
record C (s₀ s₁ t₀ t₁ : U) : Set where
  constructor cc
  field
    comb : s₀ ⟷ t₀
    transp : s₁ ⟷ t₁

-- evaluation is then straightforward, just follow the types:
evalV : {s₀ s₁ t₀ t₁ : U} {fl : Flavour} {p₀ : s₁ ⟷ s₁} →
  (c : C s₀ s₁ t₀ t₁) → (val : V fl s₀ s₁ p₀) →
  V fl t₀ t₁ (! (C.transp c) ◎ p₀ ◎ (C.transp c))
evalV {p₀ = p} (cc comb transp) (v pt (iter i q α)) =
  v (eval comb pt) (iter i (! transp ◎ (q ◎ transp)) {!!}) --

-- we should go backwards too
evalVB : {s₀ s₁ t₀ t₁ : U} {fl : Flavour} {p₁ : t₁ ⟷ t₁} →
  (c : C s₀ s₁ t₀ t₁) → (val : V fl t₀ t₁ p₁) →
    V fl s₀ s₁ ((C.transp c) ◎ p₁ ◎ ! (C.transp c))
evalVB (cc comb transp) (v pt (iter i q α)) =
  v (evalB comb pt) (iter (+ 1) (transp ◎ (q ◎ ! transp)) {!!})

-- Next comes the (generic) type of morphisms. Note that this type is
-- 'too big', in practice we use particular sub-types.
record H {s₀ s₁ t₀ t₁ : U} {fl : Flavour} {p : s₁ ⟷ s₁} {q : t₁ ⟷ t₁}
  (a : V fl s₀ s₁ p) (b : V fl t₀ t₁ q) : Set where
  constructor mor
  open V
  field
    combi : C s₀ s₁ t₀ t₁

  vb = evalV combi a

  field
    pt-eq : pt vb P.≡ pt b
    t-eq : Iter.p' (auto vb) ⇔ Iter.p' (auto b)
    -- should p transport to ⇔ q ?

-- The above gives, implicitly, a notion of equality, which can
-- be extracted as below.  Note how we insist on the types being
-- the same.  This is basically the same as H when combi is id⟷ id⟷
record _≡V_ {s₀ s₁ : U} {fl : Flavour} {p q : s₁ ⟷ s₁}
  (a : V fl s₀ s₁ p) (b : V fl s₀ s₁ q) : Set where
  constructor veq
  open V
  field
    pt-eq : pt a P.≡ pt b
    t-eq : Iter.p' (auto a) ⇔ Iter.p' (auto b)
    p⇔q : p ⇔ q

-- And now we can say what back-and-forth do:
evBF : {s₀ s₁ t₀ t₁ : U} {fl : Flavour} {p₀ : s₁ ⟷ s₁} →
  (c : C s₀ s₁ t₀ t₁) → (val : V fl s₀ s₁ p₀) →
  evalVB c (evalV c val) ≡V val
evBF (cc comb transp) (v pt (iter i p' α)) =
  veq (P.trans (lemma1 comb (eval comb pt)) (
       P.trans (P.cong (proj₁ (sym≃ (c2equiv comb))) (lemma0 comb pt))
               (isqinv.β (proj₂ (c2equiv comb)) pt)))
      {!!} {!!}

-- and Homs.  Note how the range of this is quite restricted
embedBaseHom : {τ : U} → (s t : ⟦ τ ⟧) → s ≡ t → H (embedBase s) (embedBase t)
embedBaseHom s .s P.refl = mor (cc id⟷ id⟷) P.refl (trans⇔ idl◎l idr◎l )

-- for #p.  The only Homs are when p ^ i ⇔ p ^ j
embed#pHom : {τ : U} → {p : τ ⟷ τ} → (v₀ v₁ : Iter p) → (Iter.p' v₀) ⇔ (Iter.p' v₁) →
  H (embed#p v₀) (embed#p v₁)
embed#pHom {_} {p} (iter i q α) (iter j r β) iso = mor (cc id⟷ p) P.refl (
  trans⇔ (id⇔ ⊡ (α ⊡ id⇔)) (trans⇔ (trans⇔ (id⇔ ⊡ (2! (assoc1g i)))
  (trans⇔ assoc◎l (trans⇔ (rinv◎l ⊡ (2! α)) idl◎l))) iso))

-- for 1/#p; a bit lazy here, q should be Iter p, but the core of the
-- idea remains the same.
embed1/#pHom : {τ : U} → (p : τ ⟷ τ) → (q : Iter p) →
  H (embed1/#p q) (embed1/#p q)
embed1/#pHom p (iter i q α) = mor (cc id⟷ p) P.refl (trans⇔
  (id⇔ ⊡ (α ⊡ id⇔)) (trans⇔ (id⇔ ⊡ 2! (assoc1g i)) (trans⇔
  assoc◎l (trans⇔ (rinv◎l ⊡ id⇔) (trans⇔ idl◎l (2! α))))))

-- infix 40 _⇿_
infixl 50 ↑_

-- let's make the relationship much clearer
data U↑ : Set where
  ↑_ : U → U↑
  -- we need to do a more complicated lift of 1
  𝟙 : {t : U} → (p : t ⟷ t) → U↑
  #p   : {t : U} → (p : t ⟷ t) → U↑
  1/#p : {t : U} → (p : t ⟷ t) → U↑

-- This corresponds exactly to Obj (proj₁ ⟦ t ⟧ ) from 2D/Frac.agda
⟦_⟧↑ : U↑ → Set
⟦ ↑ x ⟧↑ = ⟦ x ⟧
⟦ 𝟙 p ⟧↑ = {!!}
⟦ #p p ⟧↑ = Iter p
⟦ 1/#p p ⟧↑ = ⊤

flavour : U↑ → Flavour
flavour (↑ _) = base
flavour (𝟙 p) = {!!}
flavour (#p _) = up
flavour (1/#p _) = down

t₀↑ : U↑ → U
t₀↑ (↑ t) = t
t₀↑ (𝟙 p) = {!!}
t₀↑ (#p p) = ONE
t₀↑ (1/#p p) = ONE

t₁↑ : U↑ → U
t₁↑ (↑ t) = ONE
t₁↑ (𝟙 p) = {!!}
t₁↑ (#p {t} _) = t
t₁↑ (1/#p {t} _) = t

auto↑ : (t : U↑) → (t₁↑ t ⟷ t₁↑ t)
auto↑ (↑ x) = id⟷
auto↑ (𝟙 p) = {!!}
auto↑ (#p p) = p
auto↑ (1/#p p) = id⟷

iter↑ : (t : U↑) → Iter (auto↑ t)
iter↑ (↑ x) = iter (+ 0) id⟷ id⇔
iter↑ (𝟙 p) = {!!}
iter↑ (#p p) = iter (+ 1) p idr◎r
iter↑ (1/#p p) = iter (+ 0) id⟷ id⇔

⟦_⟧V : (t : U↑)  → Set
⟦ t ⟧V = V (flavour t) (t₀↑ t) (t₁↑ t) (auto↑ t)

fwd : {t : U↑} → ⟦ t ⟧↑ → ⟦ t ⟧V
fwd {↑ x} val = embedBase val
fwd {𝟙 p} val = {!!}
fwd {#p p} val = embed#p val
fwd {1/#p p} tt = embed1/#p (iter (+ 0) id⟷ id⇔)

bwd : {t : U↑} → ⟦ t ⟧V → ⟦ t ⟧↑
bwd {↑ x} val = V.pt val
bwd {𝟙 p} val = {!!}
bwd {#p p} val = V.auto val
bwd {1/#p p} val = tt

-- (This should be packed up to use ≡V)
fwdbwd≈id : {t : U↑} → (x : ⟦ t ⟧V) → V.pt (fwd {t} (bwd x)) P.≡ V.pt x
fwdbwd≈id {↑ x} (v pt auto) = P.refl
fwdbwd≈id {𝟙 p} (v pt auto) = {!!}
fwdbwd≈id {#p p} (v tt auto) = P.refl
fwdbwd≈id {1/#p p} (v tt auto) = P.refl

fb-auto : {t : U↑} → (x : ⟦ t ⟧V) → Iter.p' (V.auto (fwd {t} (bwd x))) ⇔ Iter.p' (V.auto x)
fb-auto {↑ x} (v pt (iter i p' α)) = 2! (trans⇔ α (id^i≡id i))
fb-auto {𝟙 p} vv = {!!}
fb-auto {#p p} (v pt (iter i p' α)) = id⇔
fb-auto {1/#p p} (v pt (iter i p' α)) = 2! (trans⇔ α (id^i≡id i))

bf-x : {t : U↑} → (x : ⟦ t ⟧↑) → bwd (fwd {t} x) P.≡ x
bf-x {↑ x} x₁ = P.refl
bf-x {𝟙 p} x = {!!}
bf-x {#p p} x = P.refl
bf-x {1/#p p} tt = P.refl

{-
data _⇿_ : U↑ → U↑ → Set where
  prim : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (↑ t₁ ⇿ ↑ t₂)
-}

ext: agda

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Data.List
open import Data.Product
open import Relation.Unary hiding (_∈_)
open import Relation.Ternary.Separation

module Relation.Ternary.Separation.Monad.State where

open import Level hiding (Lift)
open import Function using (_∘_; case_of_)
open import Relation.Binary.PropositionalEquality using (refl; _≡_)
import Relation.Binary.HeterogeneousEquality as HEq
open import Relation.Unary.PredicateTransformer hiding (_⊔_; [_])
open import Relation.Ternary.Separation.Construct.List
open import Relation.Ternary.Separation.Construct.Product
open import Relation.Ternary.Separation.Construct.Market
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad

open import Data.Unit
open import Data.Product
open import Data.List.Relation.Ternary.Interleaving.Propositional as I

open Monads

module _ {ℓ} {C : Set ℓ} {{r : RawSep C}} {u} {{s : IsUnitalSep r u}} where

  open Morphism (market {A = C}) public

  STATET : (M : Pt (Market C) ℓ) → (l r : Pred (C × C) ℓ) → Pt C ℓ
  STATET M St St' P = (● St ─✴ M (J P ✴ ● St')) ∘ demand

  StateT : (M : Pt (Market C) ℓ) → Pred (C × C) ℓ → Pt C ℓ
  StateT M St = STATET M St St

  open import Relation.Ternary.Separation.Monad.Identity

  State : Pred (C × C) ℓ → Pt C ℓ
  State St = STATET Identity.Id St St

module StateTransformer {ℓ}
  {C : Set ℓ} {u}
  {{r : RawSep C}}
  {{s : IsUnitalSep r u}}
  (M : Pt (Market C) ℓ)
  {{monad : Monads.Monad ⊤ ℓ (λ _ _ → M) }}
  {St : Pred (C × C) ℓ}
  where

  instance
    state-monad : Monad ⊤ _ (λ _ _ → StateT M St)
    app (Monad.return state-monad px) st σ₂ = return (inj px ×⟨ σ₂ ⟩ st )
    app (app (Monad.bind state-monad {P = P} {Q = Q} f) m σ₁) st@(lift _ _) σ₂@(offerᵣ σ₅) with ⊎-assoc (demand σ₁) σ₂
    ... | _ , σ₃ , σ₄ = app (bind bound) (app m st σ₄) σ₃
      where
        bound : ((J P ✴ ● St) ─✴ M (J Q ✴ ● St)) (demand _)
        app bound (inj px ×⟨ offerᵣ σ₅ ⟩ st') (offerᵣ σ₆) with ⊎-unassoc σ₅ σ₆
        ... | _ , τ₁ , τ₂ = let mq = app f px (⊎-comm τ₁) in app mq st' (offerᵣ τ₂)

  {- Lift an M computation into a transformed state operation -}
  liftM : ∀ {Φ P} → M P (demand Φ) → StateT M St (P ∘ demand) Φ
  app (liftM mp) (lift μ k) σ@(offerᵣ _) =
    app (mapM′ (wand λ where px σ@(offerₗ _) → inj px ×⟨ ⊎-comm σ ⟩ (lift μ k))) mp (⊎-comm σ)

  {- Lift a state computation into a transformed state operation -}
  liftState : ∀ {P} → ∀[ State St P ⇒ StateT M St P ]
  app (liftState mp) st σ = Monad.return monad (app mp st σ)

module StateWithErr {ℓ}
  {C : Set ℓ} {u}
  {{r : RawSep C}}
  {{s : IsUnitalSep r u}}
  (Exc : Set ℓ) where

  open import Relation.Ternary.Separation.Monad.Error
  open ExceptMonad {A = Market C} Exc public
  open StateTransformer {C = C} (Except Exc) {{ monad = except-monad }} public

  open import Data.Sum

  State? : ∀ (S : Pred (C × C) ℓ) → Pt C ℓ
  State? = StateT (Except Exc)

  _orElse_ : ∀ {S P} {M : Pt (Market C) ℓ} {{monad : Monads.Monad ⊤ ℓ (λ _ _ → M) }}
                → ∀[ State? S P ⇒ (⋂[ _ ∶ Exc ] StateT M S P) ⇒ StateT M S P ]
  app (mp orElse mq) μ σ with app mp μ σ
  ... | error e = app (mq e) μ σ
  ... | ✓ px    = return px

  try : ∀ {S P} → ε[ State? S P ] → ε[ State S (Emp ∪ P) ]
  app (try mp?) st σ with app mp? st σ
  ... | error e                = inj (inj₁ empty) ×⟨ σ ⟩ st
  ... | ✓ (inj px ×⟨ σ' ⟩ st') = inj (inj₂ px) ×⟨ σ' ⟩ st'

  raise : ∀ {S P} → Exc → ∀[ State? S P ]
  app (raise {P} e) μ σ = partial (inj₁ e)


text:
module Formalization.Monoid where

import      Lvl
open import Numeral.Finite using (𝕟)
open import Numeral.Natural using (ℕ)
open import Type
open import Type.Dependent
open import Syntax.Function

private variable ℓ ℓₑ : Lvl.Level
private variable T : Type{ℓ}
private variable n n₁ n₂ : ℕ

module Semigroup where
  -- A term in the language of a semigroup.
  -- It consists of a finite number of variables and a binary operator on its elements.
  data Term (n : ℕ) : Type{Lvl.𝟎} where
    var : 𝕟(n) → Term(n)
    _▫_ : Term(n) → Term(n) → Term(n)

module Monoid where
  open import Data.List
  open import Data.List.Functions

  -- A term in the language of a monoid.
  -- It consists of a finite number of variables, an identity element, and a binary operator on its elements.
  data Term (n : ℕ) : Type{Lvl.𝟎} where
    var : 𝕟(n) → Term(n)
    _▫_ : Term(n) → Term(n) → Term(n)
    id : Term(n)

  -- A fully normalised term in the language of a monoid is always able to be represented as a list of variables.
  -- See `normalize` for how a term is represented as a list.
  NormalForm : ℕ → Type
  NormalForm(n) = List(𝕟(n))

  -- Normalizes a term to its normal form.
  normalize : Term(n) → NormalForm(n)
  normalize (var v) = singleton v
  normalize (x ▫ y) = normalize x ++ normalize y
  normalize id      = ∅

  open import Structure.Function
  open import Structure.Function.Multi
  open import Structure.Operator
  open import Structure.Operator.Monoid
  open import Structure.Operator.Properties
  open import Structure.Relator.Properties
  open import Structure.Setoid
  open import Syntax.Transitivity

  module Semantics ⦃ equiv : Equiv{ℓₑ}(T) ⦄ (_∙_ : T → T → T) ⦃ monoid : Monoid(_∙_) ⦄ where
    open Structure.Operator.Monoid.Monoid(monoid) using () renaming (id to 𝑒)

    -- The environment for evaluating an expression is just a mapping from its variables to the values.
    Env : ℕ → Type
    Env(n) = (𝕟(n) → T)

    -- The semantics of the terms.
    eval : Env(n) → Term(n) → T
    eval env (var n) = env n
    eval env (x ▫ y) = eval env x ∙ eval env y
    eval env id      = 𝑒

    -- The semantics of the normal form.
    evalNormal : Env(n) → NormalForm(n) → T
    evalNormal env ∅       = 𝑒
    evalNormal env (v ⊰ l) = env v ∙ evalNormal env l

    module Proofs where
      private variable env : Env(n)
      private variable e : Term(n)

      instance
        eval-preserves : Preserving₂(eval env)(_▫_)(_∙_)
        eval-preserves = intro(reflexivity(_≡_))

      instance
        evalNormal-preserves : Preserving₂(evalNormal env)(_++_)(_∙_)
        evalNormal-preserves {env = env} = intro(\{x y} → proof{x}{y}) where
          proof : Names.Preserving₂(evalNormal env)(_++_)(_∙_)
          proof {∅}      {ys} = symmetry(_≡_) (identityₗ(_∙_)(𝑒))
          proof {x ⊰ xs} {ys} =
            evalNormal env ((x ⊰ xs) ++ ys)                 🝖[ _≡_ ]-[]
            evalNormal env (x ⊰ (xs ++ ys))                 🝖[ _≡_ ]-[]
            env x ∙ evalNormal env (xs ++ ys)               🝖[ _≡_ ]-[ congruence₂ᵣ(_∙_)(_) (proof {xs}{ys}) ]
            env x ∙ (evalNormal env xs ∙ evalNormal env ys) 🝖[ _≡_ ]-[ associativity(_∙_) ]-sym
            (env x ∙ evalNormal env xs) ∙ evalNormal env ys 🝖[ _≡_ ]-[]
            evalNormal env (x ⊰ xs) ∙ evalNormal env ys     🝖-end

      normalize-eval-correctness : (evalNormal env (normalize e) ≡ eval env e)
      normalize-eval-correctness {env = env} {var v} = identityᵣ(_∙_)(𝑒)
      normalize-eval-correctness {env = env} {x ▫ y} =
        evalNormal env (normalize (x ▫ y))                          🝖[ _≡_ ]-[]
        evalNormal env (normalize x ++ normalize y)                 🝖[ _≡_ ]-[ preserving₂(evalNormal env)(_++_)(_∙_) {normalize x}{normalize y} ]
        evalNormal env (normalize x) ∙ evalNormal env (normalize y) 🝖[ _≡_ ]-[ congruence₂(_∙_) (normalize-eval-correctness{env = env}{x}) (normalize-eval-correctness{env = env}{y}) ]
        eval env x ∙ eval env y                                     🝖[ _≡_ ]-[]
        eval env (x ▫ y)                                            🝖-end
      normalize-eval-correctness {env = env} {id}    = reflexivity(_≡_)

module CommutativeMonoid where

module CommutativeRig where
  open import Data.ListSized
  open import Formalization.Polynomial as Polynomial using (Polynomial)

  -- A term in the language of a commutative rig.
  -- It consists of a finite number of variables and a binary operator on its elements.
  data Term (n : ℕ) : Type{Lvl.𝟎} where
    var : 𝕟(n) → Term(n)
    _➕_ : Term(n) → Term(n) → Term(n)
    _✖_ : Term(n) → Term(n) → Term(n)
    𝟎 : Term(n)
    𝟏 : Term(n)

  NormalForm : ℕ → Type
  NormalForm = Polynomial

  {-
  normalize : Term(n) → NormalForm(n)
  normalize (var x) = {!!}
  normalize (t ➕ t₁) = {!!}
  normalize (t ✖ t₁) = {!!}
  normalize 𝟎 = {!!}
  normalize 𝟏 = {!!}
  -}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Issue452 where

data Bool : Set where
  true false : Bool

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

abstract

  id : Bool → Bool
  id b = b

If_then_else_ : Bool → Set → Set → Set
If true  then t else f = t
If false then t else f = f

data D : (b : Bool) → If b then ⊤ else ⊥ → Set where
  d : D (id true) _  -- this meta variable (type If (id true) ...) is unsolvable

foo : D true tt → ⊥
foo ()
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Rules/LHS/Unify.hs:402

{- Trying to unify

  D true tt = D (id true) _

true = id true is postponed, but then tt is handled of type

  If (id true)...

which is not a data or record type, causing the panic

Solution: do not postpone but fail, since in D : (b : Bool) -> X

  X depends on b

-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Delta (K : Set) \{\{bij : bij K Nat\}\} where

DL : (V : Set) \altRArr Set
DL V = List (Nat \altAnd V)

data DD (V : Set) : Set where
  DD : DL V \altRArr DD V

delta
  : \altFAll\{n m\} \altRArr n < m \altRArr Nat
delta n<m =
  difference (n<m\altRArr1+n\ensuremath{\leq}m n<m) -- i.e. m - n - 1

-- lookup
_\altLAng_\altRAng
  : \altFAll\{V\} \altRArr DD V \altRArr K \altRArr Maybe V
(DD dd) \altLAng k \altRAng =
  lkup dd (toNat k)
  where
    lkup : \altFAll\{V\} \altRArr DL V \altRArr Nat \altRArr Maybe V
    lkup [] n = None
    lkup ((hn , ha) :: t) n
      with <dec n hn
\fourChars{}... | Inl n<hn       = None
\fourChars{}... | Inr (Inl refl) = Some ha
\fourChars{}... | Inr (Inr hn<n) = lkup t (delta hn<n)

-- insert/extend
_,,_
  : \altFAll\{V\} \altRArr DD V \altRArr (K \altAnd V) \altRArr DD V
(DD dd) ,, (k , v) =
  DD (ins dd (toNat k , v))
  where
    ins : \altFAll\{V\} \altRArr DL V \altRArr (Nat \altAnd V) \altRArr DL V
    ins [] (n , v) = (n , v) :: []
    ins ((hn , hv) :: t) (n , v)
      with <dec n hn
\fourChars{}... | Inl n<hn =
          (n , v) :: (delta n<hn , hv) :: t
\fourChars{}... | Inr (Inl refl) =
          (n , v) :: t
\fourChars{}... | Inr (Inr hn<n) =
          (hn , hv) :: ins t (delta hn<n , v)

destruct
  : \altFAll\{V\} \altRArr DD V \altRArr Maybe ((K \altAnd V) \altAnd DD V)
destruct (DD []) = None
destruct (DD ((n , v) :: [])) =
  Some ((fromNat n , v) , DD [])
destruct (DD ((n , v) :: (m , v') :: t)) =
  Some ((fromNat n , v) , DD ((n + m + 1 , v') :: t))

max_stars_repo_name: nickcollins/dependent-dicts

max_issues_repo_name: nickcollins/dependent-dicts

max_forks_repo_name: nickcollins/dependent-dicts


text:
{-# OPTIONS --prop --rewriting #-}

open import Calf.CostMonoid

module Calf.Types.BoundedFunction (costMonoid : CostMonoid) where

open CostMonoid costMonoid

open import Calf.Prelude
open import Calf.Metalanguage
open import Calf.Step costMonoid
open import Calf.Types.Bounded costMonoid

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

bounded : (A : tp pos) → cmp cost → tp neg
bounded A n = Σ+- (U (F A)) λ u → IsBounded⁻ A u n

Ψ : (A : tp pos) → (B : val A → tp pos) → (val A → ℂ) → tp neg
Ψ A B p =
  Σ+- (U(Π A (λ a → F (B a)))) λ f →
    Π A λ a → IsBounded⁻ (B a) (f a) (p a)

dom : ∀ {ℓ} {a} {A : Set a} {B : Set a} → Rel B ℓ → Rel (A → B) (a ⊔ ℓ)
dom {A = A} r f1 f2 = ∀ (a : A) → r (f1 a) (f2 a)

Ψ/relax : ∀ A B {p p'} → dom _≤_ p p' →
                 (f : cmp (Ψ A B p)) →
                 cmp (Ψ A B p')
Ψ/relax A B h (func , prf) = func ,
  λ a → bound/relax (λ _ → h a) (prf a)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

{-
  Adapted from Ulrik's work in Lean (released under Apache License 2.0)
  https://github.com/leanprover/lean/blob/master/hott/homotopy/cellcomplex.hlean
-}

open import HoTT renaming (pt to pt⊙)
open import homotopy.DisjointlyPointedSet

module cw.CW {i} where

open import cw.Attached public

{-
  Naming convention: most of them have the "cw-" prefix
-}

-- skeleton
{-
  Disadvantages of alternative definitions:

  [Skeleton] as a data type: No η. ([Skeleton (S n)] does not expand.)
  [Skeleton] as a recursive record type: No η.
  [Skeleton] as a recursive fuction giving recursive Σ types:
    the current Agda sees that [Skeleton 0] and [Skeleton (S n)]
    have the same head symbol [Σ] and will not invert [Skeleton]
    during unification.

  The following is combines a recursive funcition and a non-recursive
  record type which should strike a good balance.
-}

record AttachedSkeleton n (Skel : Type (lsucc i)) (Real : Skel → Type i)
  : Type (lsucc i) where
  constructor attached-skeleton
  field
    skel : Skel
    cells : hSet i
    attaching : Attaching (Real skel) (fst cells) (Sphere n)

Skeleton : ℕ → Type (lsucc i)
Realizer : {n : ℕ} → Skeleton n → Type i

Skeleton O = hSet i
Skeleton (S n) = AttachedSkeleton n (Skeleton n) Realizer

Realizer {n = O} A = fst A
Realizer {n = S n} (attached-skeleton _ _ α) = Attached α

⟦_⟧ = Realizer

-- Pointedness

-- this function is needed for pointedness
cw-head : ∀ {n : ℕ} → Skeleton n → Type i
cw-head {n = O} cells = fst cells
cw-head {n = S n} (attached-skeleton skel _ _) = cw-head skel

-- this function is needed for pointedness
incl^ : ∀ {n : ℕ} (skel : Skeleton n)
  → cw-head skel → ⟦ skel ⟧
incl^ {n = O} cells a = a
incl^ {n = S n} (attached-skeleton skel _ _) a = incl (incl^ skel a)

-- disjointly pointed skeletons
record ⊙Skeleton (n : ℕ) : Type (lsucc i) where
  constructor ⊙skeleton
  field
    skel : Skeleton n
    pt : cw-head skel
    pt-dec : is-separable ⊙[ cw-head skel , pt ]

⊙Realizer : {n : ℕ} → ⊙Skeleton n → Ptd i
⊙Realizer (⊙skeleton skel pt _) = ⊙[ ⟦ skel ⟧ , incl^ skel pt ]

⊙⟦_⟧ = ⊙Realizer

-- Take a prefix of a skeleton

cw-init : ∀ {n} → Skeleton (S n) → Skeleton n
cw-init (attached-skeleton skel _ _) = skel

⊙cw-init : ∀ {n} → ⊙Skeleton (S n) → ⊙Skeleton n
⊙cw-init (⊙skeleton skel pt dec) = ⊙skeleton (cw-init skel) pt dec

cw-take : ∀ {m n : ℕ} (m≤n : m ≤ n) → Skeleton n → Skeleton m
cw-take (inl idp)        skel = skel
cw-take (inr ltS)        skel = cw-init skel
cw-take (inr (ltSR m<n)) skel = cw-take (inr m<n) (cw-init skel)

cw-init-take : ∀ {m n : ℕ} (Sm≤n : S m ≤ n) skel
  → cw-init (cw-take Sm≤n skel) == cw-take (≤-trans lteS Sm≤n) skel
cw-init-take (inl idp) skel = idp
cw-init-take (inr ltS) skel = idp
cw-init-take (inr (ltSR lt)) skel = cw-init-take (inr lt) (cw-init skel)

⊙cw-take : ∀ {m n : ℕ} (m≤n : m ≤ n) → ⊙Skeleton n → ⊙Skeleton m
⊙cw-take (inl idp)        ⊙skel = ⊙skel
⊙cw-take (inr ltS)        ⊙skel = ⊙cw-init ⊙skel
⊙cw-take (inr (ltSR m<n)) ⊙skel = ⊙cw-take (inr m<n) (⊙cw-init ⊙skel)

⊙cw-head : ∀ {n : ℕ} → ⊙Skeleton n → Ptd i
⊙cw-head (⊙skeleton skel pt _) = ⊙[ cw-head skel , pt ]

⊙cw-init-take : ∀ {m n : ℕ} (Sm≤n : S m ≤ n) ⊙skel
  → ⊙cw-init (⊙cw-take Sm≤n ⊙skel) == ⊙cw-take (≤-trans lteS Sm≤n) ⊙skel
⊙cw-init-take (inl idp) ⊙skel = idp
⊙cw-init-take (inr ltS) ⊙skel = idp
⊙cw-init-take (inr (ltSR lt)) ⊙skel = ⊙cw-init-take (inr lt) (⊙cw-init ⊙skel)

-- Access the [m]th cells

cells-last : ∀ {n : ℕ} → Skeleton n → Type i
cells-last {n = O} cells = fst cells
cells-last {n = S n} (attached-skeleton _ cells _) = fst cells

⊙cells-last : ∀ {n : ℕ} → ⊙Skeleton n → Type i
⊙cells-last (⊙skeleton skel _ _) = cells-last skel

cells-nth : ∀ {m n : ℕ} (m≤n : m ≤ n) → Skeleton n → Type i
cells-nth m≤n = cells-last ∘ cw-take m≤n

⊙cells-nth : ∀ {m n : ℕ} (m≤n : m ≤ n) → ⊙Skeleton n → Type i
⊙cells-nth m≤n = ⊙cells-last ∘ ⊙cw-take m≤n

-- Access the [m]th dimensional attaching map

Realizer₋₁ : ∀ {n : ℕ} → Skeleton (S n) → Type i
Realizer₋₁ = ⟦_⟧ ∘ cw-init

⟦_⟧₋₁ = Realizer₋₁

⊙Realizer₋₁ : ∀ {n : ℕ} → ⊙Skeleton (S n) → Ptd i
⊙Realizer₋₁ = ⊙⟦_⟧ ∘ ⊙cw-init

⊙⟦_⟧₋₁ = ⊙Realizer₋₁

attaching-last : ∀ {n : ℕ} (skel : Skeleton (S n))
  → cells-last skel → (Sphere n → ⟦ skel ⟧₋₁)
attaching-last (attached-skeleton _ _ attaching) = attaching

⊙attaching-last : ∀ {n : ℕ} (⊙skel : ⊙Skeleton (S n))
  → ⊙cells-last ⊙skel → (Sphere n → de⊙ ⊙⟦ ⊙skel ⟧₋₁)
⊙attaching-last = attaching-last ∘ ⊙Skeleton.skel

attaching-nth : ∀ {m n : ℕ} (Sm≤n : S m ≤ n) (skel : Skeleton n)
  → cells-nth Sm≤n skel → (Sphere m → ⟦ cw-take Sm≤n skel ⟧₋₁)
attaching-nth Sm≤n = attaching-last ∘ cw-take Sm≤n

⊙attaching-nth : ∀ {m n : ℕ} (Sm≤n : S m ≤ n) (⊙skel : ⊙Skeleton n)
  → ⊙cells-nth Sm≤n ⊙skel → Sphere m → de⊙ ⊙⟦ ⊙cw-take Sm≤n ⊙skel ⟧₋₁
⊙attaching-nth Sm≤n = ⊙attaching-last ∘ ⊙cw-take Sm≤n

-- Access the [m]th dimensional inclusion map

cw-incl-last : ∀ {n} (skel : Skeleton (S n))
  → (⟦ skel ⟧₋₁ → ⟦ skel ⟧)
cw-incl-last _ = incl

⊙cw-incl-last : ∀ {n} (⊙skel : ⊙Skeleton (S n))
  → (⊙⟦ ⊙skel ⟧₋₁ ⊙→ ⊙⟦ ⊙skel ⟧)
⊙cw-incl-last _ = incl , idp

cw-incl-nth : ∀ {m n : ℕ} (Sm≤n : S m ≤ n) (skel : Skeleton n)
  → ⟦ cw-take Sm≤n skel ⟧₋₁ → ⟦ cw-take Sm≤n skel ⟧
cw-incl-nth Sm≤n = cw-incl-last ∘ cw-take Sm≤n

⊙cw-incl-nth : ∀ {m n : ℕ} (Sm≤n : S m ≤ n) (⊙skel : ⊙Skeleton n)
  → (⊙⟦ ⊙cw-take Sm≤n ⊙skel ⟧₋₁ ⊙→ ⊙⟦ ⊙cw-take Sm≤n ⊙skel ⟧)
⊙cw-incl-nth Sm≤n = ⊙cw-incl-last ∘ ⊙cw-take Sm≤n

cw-incl-tail : ∀ {m n : ℕ} (m≤n : m ≤ n) (skel : Skeleton n)
  → (⟦ cw-take m≤n skel ⟧ → ⟦ skel ⟧)
cw-incl-tail (inl idp) skel = idf ⟦ skel ⟧
cw-incl-tail (inr ltS) skel = cw-incl-last skel
cw-incl-tail (inr (ltSR lt)) skel =
  cw-incl-last skel ∘ cw-incl-tail (inr lt) (cw-init skel)

⊙cw-incl-tail : ∀ {m n : ℕ} (m≤n : m ≤ n) (⊙skel : ⊙Skeleton n)
  → (⊙⟦ ⊙cw-take m≤n ⊙skel ⟧ ⊙→ ⊙⟦ ⊙skel ⟧)
⊙cw-incl-tail (inl idp) ⊙skel = ⊙idf ⊙⟦ ⊙skel ⟧
⊙cw-incl-tail (inr ltS) ⊙skel = ⊙cw-incl-last ⊙skel
⊙cw-incl-tail (inr (ltSR lt)) ⊙skel =
  ⊙cw-incl-last ⊙skel ⊙∘ ⊙cw-incl-tail (inr lt) (⊙cw-init ⊙skel)

-- Extra conditions on CW complexes

-- 1. decidable equalities
has-cells-with-dec-eq : ∀ {n} → Skeleton n → Type i
has-cells-with-dec-eq {n = O} skel = has-dec-eq (cells-last skel)
has-cells-with-dec-eq {n = S n} skel =
  has-cells-with-dec-eq (cw-init skel) × has-dec-eq (cells-last skel)

⊙has-cells-with-dec-eq : ∀ {n} → ⊙Skeleton n → Type i
⊙has-cells-with-dec-eq = has-cells-with-dec-eq ∘ ⊙Skeleton.skel

cells-last-has-dec-eq : ∀ {n} (skel : Skeleton n)
  → has-cells-with-dec-eq skel → has-dec-eq (cells-last skel)
cells-last-has-dec-eq {n = O} skel dec = dec
cells-last-has-dec-eq {n = S n} skel dec = snd dec

init-has-cells-with-dec-eq : ∀ {n} (skel : Skeleton (S n))
  → has-cells-with-dec-eq skel
  → has-cells-with-dec-eq (cw-init skel)
init-has-cells-with-dec-eq skel dec = fst dec

take-has-cells-with-dec-eq : ∀ {m n} (m≤n : m ≤ n) (skel : Skeleton n)
  → has-cells-with-dec-eq skel
  → has-cells-with-dec-eq (cw-take m≤n skel)
take-has-cells-with-dec-eq (inl idp) skel dec = dec
take-has-cells-with-dec-eq (inr ltS) skel dec = init-has-cells-with-dec-eq skel dec
take-has-cells-with-dec-eq (inr (ltSR lt)) skel dec
  = take-has-cells-with-dec-eq (inr lt) (cw-init skel) (init-has-cells-with-dec-eq skel dec)

cells-nth-has-dec-eq : ∀ {m n} (m≤n : m ≤ n) (skel : Skeleton n)
  → has-cells-with-dec-eq skel → has-dec-eq (cells-nth m≤n skel)
cells-nth-has-dec-eq m≤n skel dec =
  cells-last-has-dec-eq (cw-take m≤n skel)
    (take-has-cells-with-dec-eq m≤n skel dec)

has-cells-with-dec-eq-is-prop : ∀ {n} {skel : Skeleton n}
  → is-prop (has-cells-with-dec-eq skel)
has-cells-with-dec-eq-is-prop {n = O} = has-dec-eq-is-prop
has-cells-with-dec-eq-is-prop {n = S n} =
  ×-level has-cells-with-dec-eq-is-prop has-dec-eq-is-prop

-- 2. choice
has-cells-with-choice : TLevel → {n : ℕ} → Skeleton n → (j : ULevel) → Type (lmax i (lsucc j))
has-cells-with-choice t {n = O} skel j = has-choice t (cells-last skel) j
has-cells-with-choice t {n = S n} skel j =
  has-cells-with-choice t (cw-init skel) j × has-choice t (cells-last skel) j

⊙has-cells-with-choice : TLevel → {n : ℕ} → ⊙Skeleton n → (j : ULevel) → Type (lmax i (lsucc j))
⊙has-cells-with-choice t ⊙skel j = has-cells-with-choice t (⊙Skeleton.skel ⊙skel) j

⊙cells-last-has-choice : {t : TLevel} {n : ℕ} (⊙skel : ⊙Skeleton n) {j : ULevel}
  → ⊙has-cells-with-choice t ⊙skel j
  → has-choice t (⊙cells-last ⊙skel) j
⊙cells-last-has-choice {n = O} ⊙skel ac = ac
⊙cells-last-has-choice {n = S n} ⊙skel ac = snd ac

⊙init-has-cells-with-choice : {t : TLevel} {n : ℕ} (⊙skel : ⊙Skeleton (S n)) {j : ULevel}
  → ⊙has-cells-with-choice t ⊙skel j
  → ⊙has-cells-with-choice t (⊙cw-init ⊙skel) j
⊙init-has-cells-with-choice ⊙skel ac = fst ac

⊙take-has-cells-with-choice : {t : TLevel} {m n : ℕ} (m≤n : m ≤ n) (⊙skel : ⊙Skeleton n) {j : ULevel}
  → ⊙has-cells-with-choice t ⊙skel j
  → ⊙has-cells-with-choice t (⊙cw-take m≤n ⊙skel) j
⊙take-has-cells-with-choice (inl idp) ⊙skel ac = ac
⊙take-has-cells-with-choice (inr ltS) ⊙skel ac = ⊙init-has-cells-with-choice ⊙skel ac
⊙take-has-cells-with-choice (inr (ltSR lt)) ⊙skel ac
  = ⊙take-has-cells-with-choice (inr lt) (⊙cw-init ⊙skel) (⊙init-has-cells-with-choice ⊙skel ac)

⊙cells-nth-has-choice : {t : TLevel} {m n : ℕ} (m≤n : m ≤ n) (⊙skel : ⊙Skeleton n) {j : ULevel}
  → ⊙has-cells-with-choice t ⊙skel j
  → has-choice t (⊙cells-nth m≤n ⊙skel) j
⊙cells-nth-has-choice m≤n ⊙skel ac = ⊙cells-last-has-choice (⊙cw-take m≤n ⊙skel)
  (⊙take-has-cells-with-choice m≤n ⊙skel ac)

{-
The following are not needed.

-- Dimensional lifting

cw-lift₁ : ∀ {n : ℕ} → Skeleton n → Skeleton (S n)
cw-lift₁ skel = attached-skeleton skel
  (Lift Empty , Lift-level Empty-is-set)
  λ{(lift ()) _}

-- This slightly stretches the naming convension
-- to two skeletons being extensionally equal.
cw-lift₁-equiv : ∀ {n} (skel : Skeleton n)
  → ⟦ cw-lift₁ skel ⟧ ≃ ⟦ skel ⟧
cw-lift₁-equiv skel = equiv to incl to-incl incl-to
  where
    to : ⟦ cw-lift₁ skel ⟧ → ⟦ skel ⟧
    to = Attached-rec (idf ⟦ skel ⟧) (λ{(lift ())}) (λ{(lift ()) _})

    to-incl : ∀ x → to (incl x) == x
    to-incl _ = idp

    incl-to : ∀ x → incl (to x) == x
    incl-to = Attached-elim (λ _ → idp) (λ{(lift ())}) (λ{(lift ()) _})

cw-lift : ∀ {n m : ℕ} → n < m → Skeleton n → Skeleton m
cw-lift ltS = cw-lift₁
cw-lift (ltSR lt) = cw-lift₁ ∘ cw-lift lt
-}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module MLib.Finite where

open import MLib.Prelude
import MLib.Fin.Parts as P
import MLib.Fin.Parts.Simple as PS
open import MLib.Prelude.RelProps

open import Data.List.All as All using (All; []; _∷_) hiding (module All)
open import Data.List.Any as Any using (Any; here; there) hiding (module Any)
import Data.List.Membership.Setoid as Membership
import Data.List.Membership.Propositional as PropMembership

import Relation.Binary.Indexed as I
import Relation.Unary as U using (Decidable)
open LeftInverse using () renaming (_∘_ to _ⁱ∘_)
open FE using (_⇨_; cong)
open import Function.Related using () renaming (module EquationalReasoning to RelReasoning)

import Data.Product.Relation.SigmaPropositional as OverΣ

open Algebra using (IdempotentCommutativeMonoid)

--------------------------------------------------------------------------------
--  Main Definition
--------------------------------------------------------------------------------

record IsFiniteSetoid {c ℓ} (setoid : Setoid c ℓ) (N : ℕ) : Set (c ⊔ˡ ℓ) where
  open Setoid setoid public
  open Setoid setoid using () renaming (Carrier to A)

  OntoFin : ℕ → Set _
  OntoFin N = LeftInverse setoid (≡.setoid (Fin N))

  field
    ontoFin : OntoFin N

  fromIx : Fin N → A
  fromIx i = LeftInverse.from ontoFin ⟨$⟩ i

  toIx : A → Fin N
  toIx x = LeftInverse.to ontoFin ⟨$⟩ x

  fromIx-toIx : ∀ x → fromIx (toIx x) ≈ x
  fromIx-toIx = LeftInverse.left-inverse-of ontoFin

  enumₜ : Table A N
  enumₜ = tabulate fromIx

  enumₗ : List A
  enumₗ = Table.toList enumₜ

IsFiniteSet : ∀ {a} → Set a → ℕ → Set a
IsFiniteSet = IsFiniteSetoid ∘ ≡.setoid

record FiniteSet c ℓ : Set (sucˡ (c ⊔ˡ ℓ)) where
  field
    setoid : Setoid c ℓ
    N : ℕ
    isFiniteSetoid : IsFiniteSetoid setoid N

  open IsFiniteSetoid isFiniteSetoid public

--------------------------------------------------------------------------------
--  Combinators
--------------------------------------------------------------------------------

-- An enumerable setoid is finite

module _ {c ℓ} (setoid : Setoid c ℓ) where
  open Setoid setoid
  open Membership setoid

  Any-cong : ∀ {xs} → (∀ x → x ∈ xs) → Set _
  Any-cong f = ∀ {x y} → x ≈ y → Any.index (f x) ≡ Any.index (f y)

  private
    from : ∀ xs → Fin (List.length xs) → Carrier
    from List.[] ()
    from (x List.∷ xs) Fin.zero = x
    from (x List.∷ xs) (Fin.suc i) = from xs i

    left-inverse-of : ∀ {xs} (f : ∀ x → x ∈ xs) x → from xs (Any.index (f x)) ≈ x
    left-inverse-of f x = go (f x)
      where
      go : ∀ {xs} (p : x ∈ xs) → from xs (Any.index p) ≈ x
      go (here px) = sym px
      go (there p) = go p

  enumerable-isFiniteSetoid : ∀ {xs} (f : ∀ x → x ∈ xs) → Any-cong f → IsFiniteSetoid setoid (List.length xs)
  enumerable-isFiniteSetoid {xs} f f-cong = record
    { ontoFin = record
      { to = record
        { _⟨$⟩_ = Any.index ∘ f
        ; cong = f-cong
        }
      ; from = ≡.→-to-⟶ (from xs)
      ; left-inverse-of = left-inverse-of f
      }
    }

-- As a special case of the previous theorem requiring fewer conditions, an
-- enumerable set is finite.

module _ {a} {A : Set a} where
  open PropMembership

  enumerable-isFiniteSet : (xs : List A) (f : ∀ x → x ∈ xs) → IsFiniteSet A (List.length xs)
  enumerable-isFiniteSet _ f = enumerable-isFiniteSetoid (≡.setoid _) f (≡.cong (Any.index ∘ f))

-- Given a function with a left inverse from some 'A' to a finite set, 'A' must also be finite.

extendedIsFinite : ∀ {c ℓ c′ ℓ′} {S : Setoid c ℓ} (F : FiniteSet c′ ℓ′) → LeftInverse S (FiniteSet.setoid F) → IsFiniteSetoid S (FiniteSet.N F)
extendedIsFinite finiteSet ontoF = record
  { ontoFin = ontoFin ⁱ∘ ontoF
  }
  where
    open FiniteSet finiteSet using (ontoFin)

extendFinite : ∀ {c ℓ c′ ℓ′} {S : Setoid c ℓ} (F : FiniteSet c′ ℓ′) → LeftInverse S (FiniteSet.setoid F) → FiniteSet c ℓ
extendFinite finiteSet ontoF = record
  { isFiniteSetoid = extendedIsFinite finiteSet ontoF
  }

module _ {c ℓ c′ ℓ′} {S : Setoid c ℓ} (F : FiniteSet c′ ℓ′) where

  extendedIsFinite′N : (¬ Setoid.Carrier S) ⊎ LeftInverse S (FiniteSet.setoid F) → ℕ
  extendedIsFinite′N (inj₁ x) = 0
  extendedIsFinite′N (inj₂ y) = FiniteSet.N F

  extendedIsFinite′ : (inj : (¬ Setoid.Carrier S) ⊎ LeftInverse S (FiniteSet.setoid F)) → IsFiniteSetoid S (extendedIsFinite′N inj)
  extendedIsFinite′ (inj₂ f) = extendedIsFinite F f
  extendedIsFinite′ (inj₁ p) = record
    { ontoFin = record
      { to = record { _⟨$⟩_ = ⊥-elim ∘ p ; cong = λ {i} → ⊥-elim (p i) }
      ; from = ≡.→-to-⟶ λ ()
      ; left-inverse-of = ⊥-elim ∘ p
      }
    }

-- Given a family of finite sets, indexed by a finite set, the sum over the entire family is finite.

module _ {c} {A : Set c} {N} (isFiniteSet : IsFiniteSet A N) where
  private
    finiteSet : FiniteSet c c
    finiteSet = record { isFiniteSetoid = isFiniteSet }
    module F = FiniteSet finiteSet

    Σᶠ : ∀ {p} → (A → Set p) → Set p
    Σᶠ P = ∃ (P ∘ lookup F.enumₜ)

  module _ {p ℓ} (finiteAt : A → FiniteSet p ℓ) where
    private
      module PW x = FiniteSet (finiteAt x)
      open PW using () renaming (Carrier to P)

      parts : P.Parts A PW.N
      parts = record
        { numParts = N
        ; parts = F.enumₜ
        }

      open P.Parts parts hiding (parts)

    Σ-isFiniteSetoid : IsFiniteSetoid (OverΣ.setoid PW.setoid) totalSize
    Σ-isFiniteSetoid = record
      { ontoFin
        =  Inverse.left-inverse (Inverse.sym asParts)
        ⁱ∘ intoCoords
        ⁱ∘ Σ-↞′ {B-setoid = PW.setoid} F.ontoFin
      }
      where
        P-setoidᶠ : Fin N → Setoid _ _
        P-setoidᶠ i = record
          { Carrier = P (F.fromIx i)
          ; _≈_ = PW._≈_ _
          ; isEquivalence = record
            { refl = PW.refl _
            ; sym = PW.sym _
            ; trans = PW.trans _
            }
          }

        ΣᶠP-setoid = OverΣ.setoid P-setoidᶠ

        open Setoid ΣᶠP-setoid using ()
          renaming (_≈_ to _≈ᶠ_)

        to : Σᶠ P → Σ (Fin N) (Fin ∘ sizeAt)
        to (_ , px) = _ , PW.toIx _ px

        to-cong : ∀ {x y} → x ≈ᶠ y → to x ≡ to y
        to-cong (≡.refl , q) = OverΣ.to-≡ (≡.refl , cong (LeftInverse.to (PW.ontoFin _)) q)

        from : Σ (Fin N) (Fin ∘ sizeAt) → Σᶠ P
        from (i , j) = _ , PW.fromIx _ j

        left-inverse-of : ∀ x → from (to x) ≈ᶠ x
        left-inverse-of (i , x) = ≡.refl , PW.fromIx-toIx _ _

        intoCoords : LeftInverse ΣᶠP-setoid (≡.setoid (Σ (Fin N) (Fin ∘ sizeAt)))
        intoCoords = record
          { to = record { _⟨$⟩_ = to ; cong = to-cong }
          ; from = ≡.→-to-⟶ from
          ; left-inverse-of = left-inverse-of
          }

    Σ-finiteSet : FiniteSet _ _
    Σ-finiteSet = record { isFiniteSetoid = Σ-isFiniteSetoid }

module All′ {a} {A : Set a} where
  module _ {p ℓ} (setoid : A → Setoid p ℓ) where
    module P′ x = Setoid (setoid x)
    module P′′ {x} = P′ x
    open P′ using () renaming (Carrier to P)
    open P′′ using (_≈_)

    data PW : {xs : List A} → All P xs → All P xs → Set (p ⊔ˡ ℓ) where
      [] : PW [] []
      _∷_ : ∀ {x xs} {px py : P x} {apx apy : All P xs} → px ≈ py → PW apx apy → PW (px ∷ apx) (py ∷ apy)

    PW-setoid : List A → Setoid _ _
    Setoid.Carrier (PW-setoid xs) = All P xs
    Setoid._≈_ (PW-setoid xs) = PW
    IsEquivalence.refl (Setoid.isEquivalence (PW-setoid .[])) {[]} = []
    IsEquivalence.refl (Setoid.isEquivalence (PW-setoid .(_ ∷ _))) {px ∷ ap} =
      P′′.refl ∷ IsEquivalence.refl (Setoid.isEquivalence (PW-setoid _))
    IsEquivalence.sym (Setoid.isEquivalence (PW-setoid .[])) [] = []
    IsEquivalence.sym (Setoid.isEquivalence (PW-setoid .(_ ∷ _))) (p ∷ q) =
      P′′.sym p ∷ IsEquivalence.sym (Setoid.isEquivalence (PW-setoid _)) q
    IsEquivalence.trans (Setoid.isEquivalence (PW-setoid .[])) [] [] = []
    IsEquivalence.trans (Setoid.isEquivalence (PW-setoid .(_ ∷ _))) (p ∷ q) (p′ ∷ q′) =
      P′′.trans p p′ ∷ IsEquivalence.trans (Setoid.isEquivalence (PW-setoid _)) q q′

  module _ {p} (P : A → Set p) where
    PW-≡ : ∀ {xs} {apx apy : All P xs} → PW (≡.setoid ∘ P) apx apy → apx ≡ apy
    PW-≡ [] = ≡.refl
    PW-≡ (p ∷ q) = ≡.cong₂ _∷_ p (PW-≡ q)

-- module _ {c ℓ} (finiteSet : FiniteSet c ℓ) where
--   private
--     module A = FiniteSet finiteSet

--   open A using (_≈_) renaming (Carrier to A)

--   open IsFiniteSetoid
--   open LeftInverse

--   private
--     boolToFin : Bool → Fin 2
--     boolToFin false = Fin.zero
--     boolToFin true = Fin.suc Fin.zero

--     open Nat using (_^_; _+_; _*_)

--     _ℕ+_ : ∀ {n} (m : ℕ) → Fin n → Fin (m + n)
--     zero ℕ+ i = i
--     suc m ℕ+ i = Fin.suc (m ℕ+ i)

--     -- ℕ*-+ m "i" "k" = "i + m * k"
--     ℕ*-+′ : ∀ {n} (m : ℕ) → Fin m → Fin n → Fin (n * m)
--     ℕ*-+′ {zero} m i ()
--     ℕ*-+′ {suc n} m i Fin.zero = Fin.inject+ (n * m) i
--     ℕ*-+′ {suc n} m i (Fin.suc k) = m ℕ+ (ℕ*-+′ m i k)

--     -- ℕ*-+ m "i" "k" = "i + m * k"
--     ℕ*-+ : ∀ {n} m → Fin m → Fin n → Fin (m * n)
--     ℕ*-+ m i k = ≡.subst Fin (Nat.*-comm _ m) (ℕ*-+′ m i k)

--     from-n-ary : ∀ {n m} → Table (Fin n) m → Fin (n ^ m)
--     from-n-ary {m = zero} _ = Fin.zero -- an empty table represents an empty n-ary string
--     from-n-ary {n} {suc m} t = ℕ*-+ n (Table.lookup t Fin.zero) (from-n-ary (Table.tail t))

--     from-n-ary-cong : ∀ {n m} (t t′ : Table (Fin n) m) → t Table.≗ t′ → from-n-ary t ≡ from-n-ary t′
--     from-n-ary-cong {m = zero} t t′ eq = ≡.refl
--     from-n-ary-cong {n} {suc m} t t′ eq = ≡.cong₂ (ℕ*-+ n) (eq Fin.zero) (from-n-ary-cong (Table.tail t) (Table.tail t′) (eq ∘ Fin.suc))

--     -- div-rem m i = "i % m" , "i / m"
--     div-rem : ∀ {n} m → Fin (m * n) → Fin m × Fin n
--     div-rem zero ()
--     div-rem {zero} (suc m) i with ≡.subst Fin (Nat.*-zeroʳ m) i
--     div-rem {zero} (suc m) i | ()
--     div-rem {suc n} (suc m) Fin.zero = Fin.zero , Fin.zero
--     div-rem {suc n} (suc m) (Fin.suc i) = {!!}

--     to-n-ary : ∀ {n m} → Fin (n ^ m) → Table (Fin n) m
--     to-n-ary {m = zero} _ = tabulate λ ()
--     to-n-ary {n} {suc m} k =
--       let r , d = div-rem n k
--           ind = to-n-ary {n} {m} d
--       in tabulate λ
--          { Fin.zero → r
--          ; (Fin.suc i) → lookup ind i
--          }

--   boolF-isFiniteSetoid : IsFiniteSetoid (A.setoid ⇨ ≡.setoid Bool) (2 Nat.^ A.N)
--   _⟨$⟩_ (to (ontoFin boolF-isFiniteSetoid)) f =
--     let digits = Table.map (boolToFin ∘ (f ⟨$⟩_)) A.enumₜ
--     in from-n-ary digits
--   cong (to (ontoFin boolF-isFiniteSetoid)) {f} {f′} p =
--     let t = Table.map (boolToFin ∘ (f ⟨$⟩_)) A.enumₜ
--     in from-n-ary-cong t _ λ _ → ≡.cong boolToFin (p A.refl)
--   _⟨$⟩_ (_⟨$⟩_ (from (ontoFin boolF-isFiniteSetoid)) i) x = {!!}
--   cong (_⟨$⟩_ (from (ontoFin boolF-isFiniteSetoid)) i) = {!!}
--   cong (from (ontoFin boolF-isFiniteSetoid)) ≡.refl = {!≡.cong ?!}
--   left-inverse-of (ontoFin boolF-isFiniteSetoid) = {!!}

-- module _ {c₁ ℓ₁ c₂ ℓ₂} (A-finiteSet : FiniteSet c₁ ℓ₁) (B-finiteSet : FiniteSet c₂ ℓ₂) where
--   private
--     module A = FiniteSet A-finiteSet
--     module B = FiniteSet B-finiteSet

--   open A using (_≈_) renaming (Carrier to A)
--   open B using () renaming (Carrier to B; _≈_ to _≈′_)

--   open IsFiniteSetoid
--   open LeftInverse

--   function-isFiniteSetoid : IsFiniteSetoid (A.setoid ⇨ B.setoid) (B.N Nat.^ A.N)
--   _⟨$⟩_ (to (ontoFin function-isFiniteSetoid)) f = {!!}
--   cong (to (ontoFin function-isFiniteSetoid)) = {!!}
--   _⟨$⟩_ (from (ontoFin function-isFiniteSetoid)) i = {!!}
--   cong (from (ontoFin function-isFiniteSetoid)) = {!!}
--   left-inverse-of (ontoFin function-isFiniteSetoid) = {!!}

-- TODO: Prove dependent function spaces with finite domain and codomain are
-- finite sets, and recast as an instance of that.

module _ {a p ℓ} {A : Set a} (finiteAt : A → FiniteSet p ℓ) where
  private
    module PW x = FiniteSet (finiteAt x)
    module PW′ {x} = PW x
    open PW using () renaming (Carrier to P; N to boundAt)
    open PW′ using (_≈_)

    All≈ = All′.PW PW.setoid
    All-setoid = All′.PW-setoid PW.setoid
    open All′.PW PW.setoid

  finiteAllSize : List A → ℕ
  finiteAllSize = List.product ∘ List.map boundAt

  All-isFiniteSetoid : (xs : List A) → IsFiniteSetoid (All-setoid xs) _
  All-isFiniteSetoid _ = record
    { ontoFin = record
      { to = record { _⟨$⟩_ = to ; cong = to-cong }
      ; from = ≡.→-to-⟶ from
      ; left-inverse-of = left-inverse-of
      }
    }
    where
      to : ∀ {xs} → All P xs → Fin (finiteAllSize xs)
      to [] = Fin.zero
      to (_∷_ {x} {xs} px ap) = PS.fromParts (PW.toIx _ px , to ap)

      to-cong : ∀ {xs}{apx apy : All P xs} → All≈ apx apy → to apx ≡ to apy
      to-cong [] = ≡.refl
      to-cong (p ∷ q) = ≡.cong₂ (curry PS.fromParts) (cong (LeftInverse.to PW′.ontoFin) p) (to-cong q)

      from : ∀ {xs} → Fin (finiteAllSize xs) → All P xs
      from {List.[]} _ = []
      from {x List.∷ xs} i =
        (PW.fromIx _ (proj₁ (PS.toParts i))) ∷
        from {xs} (proj₂ (PS.toParts {boundAt x} i))

      left-inverse-of : ∀ {xs} (ap : All P xs) → All≈ (from (to ap)) ap
      left-inverse-of [] = Setoid.refl (All-setoid _)
      left-inverse-of (px ∷ ap) rewrite Inverse.right-inverse-of PS.asParts (PW.toIx _ px , to ap) =
        PW′.fromIx-toIx px ∷ left-inverse-of ap

  All-finiteSet : List A → FiniteSet _ _
  All-finiteSet xs = record { isFiniteSetoid = All-isFiniteSetoid xs }

1-Truncate : ∀ {c ℓ} (setoid : Setoid c ℓ) → Setoid _ _
1-Truncate setoid = record
  { Carrier = Carrier
  ; _≈_ = λ _ _ → ⊤
  ; isEquivalence = record { refl = _ ; sym = _ ; trans = _ }
  }
  where open Setoid setoid

module DecFinite {a p} {A : Set a} {P : A → Set p} (decP : U.Decidable P) where
  P-setoid : A → Setoid _ _
  P-setoid = 1-Truncate ∘ ≡.setoid ∘ P

  P-size : A → ℕ
  P-size x = if ⌊ decP x ⌋ then 1 else 0

  P-isFinite : ∀ x → IsFiniteSetoid (P-setoid x) (P-size x)
  P-isFinite x with decP x
  P-isFinite x | yes p = record
    { ontoFin = record
      { to = record
        { _⟨$⟩_ = λ _ → Fin.zero ; cong = λ _ → ≡.refl }
        ; from = ≡.→-to-⟶ λ _ → p
        ; left-inverse-of = _
      }
    }
  P-isFinite x | no ¬p = record
    { ontoFin = record
      { to = record { _⟨$⟩_ = ⊥-elim ∘ ¬p ; cong = λ {x} → ⊥-elim (¬p x) }
      ; from = ≡.→-to-⟶ λ ()
      ; left-inverse-of = _
      }
    }

  Decidable-finite : A → FiniteSet p _
  Decidable-finite x = record { isFiniteSetoid = P-isFinite x }

module _ {c} {A : Set c} {N} (isFiniteSet : IsFiniteSet A N) {p} {P : A → Set p} (decP : U.Decidable P) where
  open IsFiniteSetoid isFiniteSet

  subsetFinite : FiniteSet _ _
  subsetFinite = Σ-finiteSet isFiniteSet (DecFinite.Decidable-finite decP)

  subset-isFiniteSet : ∀ {a′} {A′ : Set a′} → LeftInverse (≡.setoid A′) (FiniteSet.setoid subsetFinite) → IsFiniteSet A′ _
  subset-isFiniteSet = extendedIsFinite subsetFinite


text:
open import Prelude
open import MJ.Classtable.Core

module MJ.LexicalScope c where

open import Data.List
open import Data.List.Membership.Propositional
open import MJ.Types

Ctx : Set
Ctx = List (Ty c)

Var : Ctx → Ty c → Set
Var Γ a = a ∈ Γ

_+local_ : Ctx → Ty c → Ctx
_+local_ Γ a = a ∷ Γ


text:
{-# OPTIONS --no-qualified-instances #-}
module JVM.Printer.Printer {t} (T : Set t) where

open import Function using (_$_; _∘_)
open import Data.Unit
open import Data.Nat
open import Data.Nat.Show as Nat
open import Data.Product
open import Data.List as List
open import Data.List.Relation.Unary.All
open import Relation.Unary hiding (Empty)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax

open import JVM.Model T
open Disjoint using (bags; bags-isMonoid)
open import Relation.Ternary.Data.Bigstar
open import Relation.Ternary.Construct.Market intf-rel
open import Relation.Ternary.Monad.Identity as Id hiding (id-monad; id-functor)
open import Relation.Ternary.Monad.State intf-rel

open import JVM.Syntax.Labeling T public
open import JVM.Printer.Jasmin

Names : List T → Set _
Names = All (λ _ → ℕ)

LabelNames : Pred Intf _
LabelNames (u ⇅ d) = Names u × Names d

PState : Pred Intf _
PState = (λ _ → ℕ × List Stat) ∩ LabelNames

counter : ∀ {Φ} → PState Φ → ℕ
counter = proj₁ ∘ proj₁

Printer : Pt Intf _
Printer = StateT Id PState

open StateTransformer Id {{Id.id-strong}} {PState} public
open import Relation.Ternary.Construct.Bag.Properties
open import Level

module Envs where

  open import Category.Monad
  open import Category.Monad.State as S

  Fresh : Set t → Set _
  Fresh = S.State (Lift t ℕ)

  open RawMonadState (StateMonadState (Lift t ℕ)) public

  open import Relation.Ternary.Construct.List duplicate as L
  open import Data.List.Relation.Binary.Permutation.Propositional
  open import Data.List.Relation.Binary.Permutation.Propositional.Properties

  fresh : Fresh (Lift _ ℕ)
  fresh (lift n) = let n' = ℕ.suc n in lift n , lift n'

  freshNames : ∀ xs → Fresh (Names xs)
  freshNames [] = return []
  freshNames (x ∷ xs) = do
    lift n ← fresh
    ns     ← freshNames xs
    return (n ∷ ns)

  env-split-list : ∀ {xs ys zs} → Names xs → L.Split xs ys zs → Fresh (Names ys × Names zs)
  env-split-list nxs []        = return ([] , [])
  env-split-list nxs (consʳ σ) = do
    lift n    ← fresh
    nys , nzs ← env-split-list nxs σ
    return (n ∷ nys , n ∷ nzs)
  env-split-list (nx ∷ nxs) (divide x σ) = do
    nys , nzs ← env-split-list nxs σ
    return (nx ∷ nys , nx ∷ nzs)
  env-split-list (nx ∷ nxs) (consˡ σ) = do
    nys , nzs ← env-split-list nxs σ
    return (nys , nx ∷ nzs)

  env-split-bag : ∀ {xs ys zs} → Names xs → Overlap.BagSplit xs ys zs → Fresh (Names ys × Names zs)
  env-split-bag nxs (Overlap.hustle ρx ρy ρz σ) = do
    let nxs'    = All-resp-↭ (↭-sym ρx) nxs
    (nys , nzs) ← env-split-list nxs' σ
    return (All-resp-↭ ρy nys , All-resp-↭ ρz nzs)

  splitEnv : ∀ {xs ys zs} → xs ∙ ys ≣ zs → LabelNames zs → Fresh (LabelNames xs × LabelNames ys)
  splitEnv (ex (sub {e = e} x x₁) (sub {e = e'} x₄ x₅) σ↑ σ↓) (unv , dnv) = do
      let nu₁' , nu₂' = splitAll (λ ()) σ↑ unv
      let nd₁' , nd₂' = splitAll (λ dup px → px , px ) σ↓ dnv
      nse  , nu₂   ← env-split-bag nu₂' x₁
      nse' , nu₁   ← env-split-bag nu₁' x₅
      let nd₁     = joinAll (λ ()) x  nd₂' nse
      let nd₂     = joinAll (λ ()) x₄ nd₁' nse'
      return ((nu₁ , nd₁) , (nu₂ , nd₂))

module _ where
  open import Relation.Ternary.Monad

  lookUp : ∀ {τ} → ∀[ Up (One τ) ⇒ Printer (Empty ℕ) ]
  lookUp (↑ u) ⟨ supplyᵣ σ ⟩ lift ((n , st) , env) with Envs.splitEnv σ env (lift n)
  ... | ((lab ∷ [] , []) , env₂) , lift n' = lift (emp lab) ∙⟨ ∙-idˡ ⟩ lift ((n' , st) , env₂)

  lookDown : ∀ {τ} → ∀[ Down (One τ) ⇒ Printer (Empty ℕ) ]
  lookDown (↓ u) ⟨ supplyᵣ σ ⟩ lift ((n , st) , env) with Envs.splitEnv σ env (lift n)
  ... | (([] , lab ∷ []) , env₂) , lift n' = lift (emp lab) ∙⟨ ∙-idˡ ⟩ lift ((n' , st) , env₂)

  print : Stat → ε[ Printer Emp ]
  print s ⟨ σ ⟩ lift ((n , st) , env) = lift refl ∙⟨ σ ⟩ lift ((n , s ∷ st) , env)

  print-label : ∀ {τ}  → ∀[ Up (One τ) ⇒ Printer Emp ]
  print-label l = do
    emp n  ← lookUp l
    print (label (Nat.show n))

  {-# TERMINATING #-}
  print-labels' : ∀ {τ} → ∀[ Up (Bigstar (One τ)) ⇒ Printer Emp ]
  print-labels' (↑ emp)                  = return refl
  print-labels' (↑ (cons (x ∙⟨ σ ⟩ xs))) = do
    xs ← ✴-id⁻ʳ ⟨$⟩ (print-label (↑ x) &⟨ ∙-comm $ liftUp σ ⟩ ↑ xs)
    print-labels' xs
    where open Disjoint using (bags; bags-isMonoid)

  print-labels : ∀ {τ} → ∀[ Up (Labeling τ) ⇒ Printer Emp ]
  print-labels (↑ (x ∙⟨ σ ⟩ xs)) = do
    xs ← ✴-id⁻ʳ ⟨$⟩ (print-label (↑ x) &⟨ ∙-comm $ liftUp σ ⟩ ↑ xs)
    print-labels' xs

-- give it a kick
execPrinter : ∀ {P Φ} → Printer P Φ → List Stat
execPrinter pr with pr ⟨ supplyᵣ ∙-idʳ ⟩ proj₁ (initState (lift 0))
  where
    open Envs

    initState : ∀ {Φ} → Envs.Fresh (● PState (supply Φ))
    initState {Φ↑ ⇅ Φ↓} = do
      ns↑ ← freshNames Φ↑
      ns↓ ← freshNames Φ↓
      lift n ← get
      return (lift ((n , []) , (ns↑ , ns↓)))

... | (lift px ∙⟨ σ ⟩ lift ((_ , st) , _)) = reverse st


text:
{-# OPTIONS --without-K -v 2 #-}
module Leftovers.Monad where

open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Level
open import Data.Unit

open import Data.List
import Reflection as TC
open import Reflection.TypeChecking.Monad.Instances

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)

open import Reflection using (ErrorPart ; strErr; termErr ; nameErr) public

open import Data.Bool

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

private
  variable
    ℓ : Level
    A : Set ℓ
    B : Set ℓ

record Hole : Set  where
  constructor mkHole
  field
    holeMeta : Meta
    hole : Term
    context : List (Arg Type)

import Relation.Binary.PropositionalEquality as Eq
import Relation.Binary.Definitions as D
open import Data.Empty using (⊥)
EquivHole : ∀ (x y : Hole) → Set
EquivHole (mkHole x _ _ ) (mkHole y _ _) = x Eq.≡ y

open import Relation.Nullary using (yes ; no)

equivDec : D.Decidable EquivHole
equivDec (mkHole x _ _) (mkHole y _ _) = x Meta.≟ y
  where import Reflection.Meta as Meta
-- equivDec (mkHole (var x args) _) (mkHole y _) =  no (λ z → z)
-- equivDec (mkHole (con c args) _) (mkHole y _) = no (λ z → z)
-- equivDec (mkHole (def f args) _) (mkHole y _) = no (λ z → z)
-- equivDec (mkHole (lam v t) _) (mkHole y _) = no (λ z → z)
-- equivDec (mkHole (pat-lam cs args) _) (mkHole y _) = no (λ z → z)
-- equivDec (mkHole (pi a b) _) (mkHole y _) = no (λ z → z)
-- equivDec (mkHole (Term.sort s) _) (mkHole y _) = no (λ z → z)
-- equivDec (mkHole (lit l) _) (mkHole y _) = no (λ z → z)
-- equivDec (mkHole unknown _) (mkHole y _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole (var x₂ args) _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole (con c args) _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole (def f args) _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole (lam v t) _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole (pat-lam cs args) _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole (pi a b) _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole (Term.sort s) _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole (lit l) _) = no (λ z → z)
-- equivDec (mkHole (meta x x₁) _) (mkHole unknown _) = no (λ z → z)

open import Category.Monad.State
open import Category.Monad.Indexed using (RawIMonad ; RawIMonadPlus)
open import Category.Applicative.Indexed using (RawIApplicative ; RawIAlternative)
open import Data.Product using (_×_ ; _,_)

Leftovers : Set ℓ  → Set ℓ
Leftovers = StateT (Lift _ (List Hole)) TC.TC

leftoversMonad : RawMonad {f = ℓ}  Leftovers
leftoversMonad = StateTMonad _ tcMonad

leftoversApplicative : RawApplicative {f = ℓ}  Leftovers
leftoversApplicative = RawIMonad.rawIApplicative leftoversMonad

leftoversFunctor : RawFunctor {ℓ = ℓ}  Leftovers
leftoversFunctor = RawIApplicative.rawFunctor leftoversApplicative

leftoversMonadZero : RawMonadZero {f = ℓ} Leftovers
leftoversMonadZero = StateTMonadZero _ tcMonadZero

leftoversMonadPlus : RawMonadPlus {f = ℓ}  Leftovers
leftoversMonadPlus = StateTMonadPlus _ tcMonadPlus

private

  -- Lift a TC operation into the Leftovers Monad
  -- WARNING: this will *NOT* track metas declared in the TC operation
  -- and should only be used for primitive operations
  liftTC :  TC.TC A → Leftovers A
  liftTC comp s = TC.bindTC comp λ a → TC.return (a , s)

  liftTCA1 : (B → TC.TC A) → B → Leftovers A
  liftTCA1 comp x  = liftTC (comp x)

  liftTCA2 : ∀ {A B C : Set ℓ} → (C → B → TC.TC A) → C → B → Leftovers A
  liftTCA2 comp x y = liftTC (comp x y)
------------------------------------------------------------------------
-- Monad syntax

returnLeftovers : A → Leftovers A
returnLeftovers = RawMonad.return leftoversMonad

bindLeftovers : ∀ {A B : Set ℓ } ->  Leftovers A → (A → Leftovers B)  → Leftovers B
bindLeftovers a f = RawMonad._=<<_ leftoversMonad f a

pure : A → Leftovers A
pure = returnLeftovers
{-# INLINE pure #-}

infixl 3 _<|>_
_<|>_ : Leftovers A → Leftovers A → Leftovers A
_<|>_ = RawIAlternative._∣_ (RawIMonadPlus.alternative leftoversMonadPlus)
{-# INLINE _<|>_ #-}

infixl 1 _>>=_ _>>_ _<&>_
_>>=_ : ∀ {A B : Set ℓ} → Leftovers A → (A → Leftovers B) → Leftovers B
_>>=_ = bindLeftovers
{-# INLINE _>>=_ #-}

_>>_ : ∀ {A B : Set ℓ} → Leftovers A → Leftovers B → Leftovers B
xs >> ys = bindLeftovers xs (λ _ → ys)
{-# INLINE _>>_ #-}

infixl 4 _<$>_ _<*>_ _<$_
_<*>_ : ∀ {A B : Set ℓ} → Leftovers (A → B) → Leftovers A → Leftovers B
fs <*> xs = bindLeftovers fs (λ f → bindLeftovers xs (λ x → returnLeftovers (f x)))
{-# INLINE _<*>_ #-}

_<$>_ : ∀ {A B : Set ℓ} →(A → B) → Leftovers A → Leftovers B
f <$> xs = bindLeftovers xs (λ x → returnLeftovers (f x))
{-# INLINE _<$>_ #-}

_<$_ : ∀ {A B : Set ℓ} →A → Leftovers B → Leftovers A
x <$ xs = bindLeftovers xs (λ _ → returnLeftovers x)
{-# INLINE _<$_ #-}

_<&>_ : ∀ {A B : Set ℓ} → Leftovers A → (A → B) → Leftovers B
xs <&> f = bindLeftovers xs (λ x → returnLeftovers (f x))
{-# INLINE _<&>_ #-}

logHole : Hole → Leftovers ⊤
logHole hole = do
  RawMonadState.modify (StateTMonadState _ tcMonad) λ { (lift lst) → lift (hole ∷ lst)}
  pure tt
-- logHole hole = RawMonadState.modify (StateTMonadState _ tcMonad)
--   (λ {lst → ?})
--   pure tt

freshMeta : Type → Leftovers Term
freshMeta t = do
  theMeta ← liftTC (TC.newMeta t)
  liftTC (TC.debugPrint "freshMeta" 2 (strErr "Fresh meta " ∷ termErr theMeta ∷ strErr " with type " ∷ termErr t ∷ []))
  ctx ← liftTC TC.getContext
  m ← liftTC (getMeta theMeta)
  logHole (mkHole m theMeta ctx)
  pure theMeta
  where
    getMeta : Term → TC.TC Meta
    getMeta (meta m _ ) = TC.return m
    getMeta t =  (TC.typeError (strErr "Foo" ∷ []))

open import Data.String

-- Re-export all of the TC functions
unify            : Term → Term → Leftovers ⊤
unify = liftTCA2 TC.unify

typeError        : ∀ {A : Set ℓ} → List TC.ErrorPart → Leftovers A
typeError x = liftTC (TC.typeError x)

inferType        : Term → Leftovers Type
inferType = liftTCA1 TC.inferType

checkType        : Term → Type → Leftovers Term
checkType = liftTCA2 TC.checkType

normalise        : Term → Leftovers Term
normalise = liftTCA1 TC.normalise

reduce           : Term → Leftovers Term
reduce = liftTCA1 TC.reduce

catchLeftovers          : ∀  {A : Set ℓ} → Leftovers A → Leftovers A → Leftovers A
catchLeftovers comp fallback s =
  --We revert any state changes if we have to go to the fallback
  TC.catchTC (comp s) (fallback s)

quoteLeftovers          : ∀  {A : Set ℓ} → A → Leftovers Term
quoteLeftovers = liftTCA1 TC.quoteTC

unquoteLeftovers        : ∀  {A : Set ℓ} → Term → Leftovers A
unquoteLeftovers = liftTCA1 TC.unquoteTC

getContext       : Leftovers (List (Arg Type))
getContext = liftTC TC.getContext

extendContext    : ∀  {A : Set ℓ} → Arg Type → Leftovers A → Leftovers A
extendContext x comp s = TC.extendContext x (comp s)

extendContexts :  ∀  {A : Set ℓ} → List (Arg Type) → Leftovers A → Leftovers A
extendContexts [] x = x
extendContexts (h ∷ t) x = extendContext h (extendContexts t x)

inContext        : ∀  {A : Set ℓ} → List (Arg Type) → Leftovers A → Leftovers A
inContext ctx comp s = TC.inContext ctx (comp s)

freshName        : String → Leftovers Name
freshName = liftTCA1 TC.freshName

declareDef       : Arg Name → Type → Leftovers ⊤
declareDef = liftTCA2 TC.declareDef

declarePostulate : Arg Name → Type → Leftovers ⊤
declarePostulate = liftTCA2 TC.declarePostulate

defineFun        : Name → List Clause → Leftovers ⊤
defineFun = liftTCA2 TC.defineFun

getType          : Name → Leftovers Type
getType = liftTCA1 TC.getType

getDefinition    : Name → Leftovers Definition
getDefinition = liftTCA1 TC.getDefinition

blockOnMeta      : ∀  {A : Set ℓ} → Meta → Leftovers A
blockOnMeta = liftTCA1 TC.blockOnMeta

--TODO: is there state stuff to do here?
commitLeftovers         : Leftovers ⊤
commitLeftovers = liftTC TC.commitTC

isMacro          : Name → Leftovers Bool
isMacro = liftTCA1 TC.isMacro

open import Data.Nat

  -- If the argument is 'true' makes the following primitives also normalise
  -- their results: inferType, checkType, quoteLeftovers, getType, and getContext
withNormalisation : ∀ {a} {A : Set a} → Bool → Leftovers A → Leftovers A
withNormalisation flag comp s = TC.withNormalisation flag (comp s)

  -- Prints the third argument if the corresponding verbosity level is turned
  -- on (with the -v flag to Agda).
debugPrint : String → ℕ → List TC.ErrorPart → Leftovers ⊤
debugPrint s n err = liftTC (TC.debugPrint s n err)

  -- Fail if the given computation gives rise to new, unsolved
  -- "blocking" constraints.
noConstraints : ∀ {a} {A : Set a} → Leftovers A → Leftovers A
noConstraints comp s = TC.noConstraints (comp s)

  -- Run the given Leftovers action and return the first component. Resets to
  -- the old Leftovers state if the second component is 'false', or keep the
  -- new Leftovers state if it is 'true'.
runSpeculative : ∀ {a} {A : Set a} → Leftovers (A × Bool) → Leftovers A
runSpeculative comp oldState =
  TC.bindTC
    (TC.runSpeculative (TC.bindTC (comp oldState) λ{((a , flag) , midState) → TC.return (((a , flag) , midState) , flag)}))
    λ {
      -- Only keep state if the computation succeeds
      ((a , false) , newState) → TC.return ((a , oldState)) ;
      ((a , true) , newState) → TC.return (a , newState)}

runLeftovers : Leftovers A → TC.TC (A × List Hole)
runLeftovers comp  = TC.bindTC (comp (lift []))
  ((λ { (a , lift holes) → TC.return (a , holes) }) )

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Higher where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Univalence

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base
open import Cubical.Homotopy.Connected

open import Cubical.Data.Sigma
open import Cubical.Data.Nat

open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Higher
open import Cubical.Algebra.Group.EilenbergMacLane1

open import Cubical.HITs.EilenbergMacLane1

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

open import Cubical.DStructures.Meta.Isomorphism
open import Cubical.DStructures.Structures.Universe
open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.Constant

private
  variable
    ℓ ℓ' : Level

𝒮ᴰ-connected : {ℓ : Level} (k : ℕ) → URGStrᴰ (𝒮-universe {ℓ}) (isConnected k) ℓ-zero
𝒮ᴰ-connected k =
  Subtype→Sub-𝒮ᴰ (λ A → isConnected k A , isPropIsContr)
                 𝒮-universe

𝒮ᴰ-truncated : {ℓ : Level} (n : ℕ) → URGStrᴰ (𝒮-universe {ℓ}) (isOfHLevel n) ℓ-zero
𝒮ᴰ-truncated n =
  Subtype→Sub-𝒮ᴰ (λ A → isOfHLevel n A , isPropIsOfHLevel n)
                 𝒮-universe

𝒮ᴰ-BGroup : (n k : ℕ)
            → URGStrᴰ (𝒮-universe {ℓ})
                      (λ A → A × (isConnected (k + 1) A) × (isOfHLevel (n + k + 2) A))
                      ℓ
𝒮ᴰ-BGroup n k =
  combine-𝒮ᴰ 𝒮ᴰ-pointed
             (combine-𝒮ᴰ (𝒮ᴰ-connected (k + 1))
                         (𝒮ᴰ-truncated (n + k + 2)))

𝒮-BGroup : (n k : ℕ) → URGStr (Σ[ A ∈ Type ℓ ] A × (isConnected (k + 1) A) × (isOfHLevel (n + k + 2) A)) ℓ
𝒮-BGroup n k = ∫⟨ 𝒮-universe ⟩ 𝒮ᴰ-BGroup n k

𝒮-1BGroup : URGStr 1BGroupΣ ℓ
𝒮-1BGroup = 𝒮-BGroup 0 1

𝒮-Iso-BGroup-Group : {ℓ : Level} → 𝒮-PIso (𝒮-group ℓ) 𝒮-1BGroup
RelIso.fun 𝒮-Iso-BGroup-Group G = EM₁ G , embase , EM₁Connected G , EM₁Groupoid G
RelIso.inv 𝒮-Iso-BGroup-Group = π₁-1BGroupΣ
RelIso.leftInv 𝒮-Iso-BGroup-Group = π₁EM₁≃
RelIso.rightInv 𝒮-Iso-BGroup-Group BG = basetype-≅ , basepoint-≅ , tt , tt
  where
    -- notation
    type = fst BG
    * = fst (snd BG)
    conn = fst (snd (snd BG))
    trunc = snd (snd (snd BG))
    BG' = (bgroup (type , *) conn trunc)

    π₁BG : Group
    π₁BG = π₁-1BGroupΣ BG

    EM₁π₁BG : 1BGroupΣ
    EM₁π₁BG = EM₁ π₁BG , embase , EM₁Connected π₁BG , EM₁Groupoid π₁BG

    -- equivalences
    basetype-≅ : EM₁ π₁BG ≃ type
    fst basetype-≅ = EM₁-functor-lInv-function π₁BG BG' (GroupEquiv.hom (π₁EM₁≃ π₁BG))
    snd basetype-≅ = EM₁-functor-lInv-onIso-isEquiv π₁BG BG' (π₁EM₁≃ π₁BG)

    basepoint-≅ : * ≡ *
    basepoint-≅ = refl

𝒮ᴰ-BGroupHom : (n k : ℕ) → URGStrᴰ (𝒮-BGroup {ℓ} n k ×𝒮 𝒮-BGroup {ℓ'} n k)
                                  (λ (BG , BH) → BGroupHomΣ BG BH)
                                  (ℓ-max ℓ ℓ')
𝒮ᴰ-BGroupHom n k =
  make-𝒮ᴰ
    (λ {(BG , BH)} {(BG' , BH')} f (((eᴳ , _) , eᴳ-pt , _), ((eᴴ , _) , eᴴ-pt , _)) f'
       → ((eᴴ , eᴴ-pt) ∘∙ f) ∙∼ (f' ∘∙ (eᴳ , eᴳ-pt)))
    (λ {(BG , BH)} f → q {(BG , BH)} f)
    contrSingl
    where
      module _ {(BG , BH) : BGroupΣ n k × BGroupΣ n k} (f : BGroupHomΣ BG BH) where
        q : (id∙ (baseΣ BH) ∘∙ f) ∙∼ (f ∘∙ id∙ (baseΣ BG))
        q = funExt∙⁻ (id∙ (baseΣ BH) ∘∙ f
                       ≡⟨ ∘∙-idʳ f ⟩
                     f
                       ≡⟨ sym (∘∙-idˡ f) ⟩
                     (f ∘∙ id∙ (baseΣ BG)) ∎)

      module _ ((BG , BH) : BGroupΣ n k × BGroupΣ n k) (f : BGroupHomΣ BG BH) where
        contrSingl : isContr (Σ[ f' ∈ BGroupHomΣ BG BH ] ((id∙ (baseΣ BH) ∘∙ f) ∙∼ (f' ∘∙ id∙ (baseΣ BG))))
        contrSingl =
                isContrRespectEquiv (Σ-cong-equiv-snd (λ f' → f ≡ f'
                                                                ≃⟨ invEquiv (funExt∙≃ f f') ⟩
                                                               f ∙∼ f'
                                                                ≃⟨ pathToEquiv (cong (_∙∼ f')
                                                                                (sym (∘∙-idʳ f))
                                                                               ∙ cong ((id∙ (baseΣ BH) ∘∙ f) ∙∼_)
                                                                                (sym (∘∙-idˡ f'))) ⟩
                                                              (id∙ (baseΣ BH) ∘∙ f) ∙∼ (f' ∘∙ id∙ (baseΣ BG)) ■))

                                    (isContrSingl f)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical