text:
{-# OPTIONS --without-K --rewriting --termination-depth=2 #-}

open import HoTT
open import cohomology.ChainComplex
open import cohomology.Theory
open import groups.KernelImage
open import cw.CW

module cw.cohomology.ReconstructedHigherCohomologyGroups {i : ULevel} (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT
  import cw.cohomology.HigherCoboundary OT as HC
  open import cw.cohomology.WedgeOfCells OT
  open import cw.cohomology.Descending OT
  open import cw.cohomology.ReconstructedCochainComplex OT
  import cw.cohomology.HigherCohomologyGroups OT as HCG
  import cw.cohomology.HigherCohomologyGroupsOnDiag OT as HCGD
  import cw.cohomology.CohomologyGroupsTooHigh OT as CGTH

  private
    ≤-dec-has-all-paths : {m n : ℕ} → has-all-paths (Dec (m ≤ n))
    ≤-dec-has-all-paths = prop-has-all-paths (Dec-level ≤-is-prop)

  private
    abstract
      higher-cohomology-group-descend : ∀ {n} (⊙skel : ⊙Skeleton {i} (2 + n)) {m} (Sm<n : S m < n)
        →  cohomology-group (cochain-complex ⊙skel) (ℕ-to-ℤ (2 + m))
        == cohomology-group (cochain-complex (⊙cw-init ⊙skel)) (ℕ-to-ℤ (2 + m))
      higher-cohomology-group-descend ⊙skel {m} ltS -- n = 2 + m
        = ap3
            (λ Sm≤4+m? SSm≤4+m? SSSm≤4+m? → Ker/Im
              (coboundary-template ⊙skel SSm≤4+m? SSSm≤4+m?)
              (coboundary-template ⊙skel Sm≤4+m? SSm≤4+m?)
              (cochain-is-abelian-template ⊙skel SSm≤4+m?))
            (≤-dec-has-all-paths (≤-dec (1 + m) (4 + m)) (inl (lteSR $ lteSR lteS)))
            (≤-dec-has-all-paths (≤-dec (2 + m) (4 + m)) (inl (lteSR lteS)))
            (≤-dec-has-all-paths (≤-dec (3 + m) (4 + m)) (inl lteS))
        ∙ ap2 (λ δ₁ δ₂ → Ker/Im δ₂ δ₁ (CXₙ/Xₙ₋₁-is-abelian (⊙cw-take (lteSR lteS) ⊙skel) (ℕ-to-ℤ (2 + m))))
            (coboundary-higher-template-descend-from-far {n = 3 + m} ⊙skel {m = m} (ltSR ltS) ltS)
            (coboundary-higher-template-descend-from-one-above ⊙skel)
        ∙ ap3
            (λ Sm≤3+m? SSm≤3+m? SSSm≤3+m? → Ker/Im
              (coboundary-template (⊙cw-init ⊙skel) SSm≤3+m? SSSm≤3+m?)
              (coboundary-template (⊙cw-init ⊙skel) Sm≤3+m? SSm≤3+m?)
              (cochain-is-abelian-template (⊙cw-init ⊙skel) SSm≤3+m?))
            (≤-dec-has-all-paths (inl (lteSR lteS)) (≤-dec (1 + m) (3 + m)))
            (≤-dec-has-all-paths (inl lteS)         (≤-dec (2 + m) (3 + m)))
            (≤-dec-has-all-paths (inl lteE)         (≤-dec (3 + m) (3 + m)))
      higher-cohomology-group-descend {n = S n} ⊙skel {m} (ltSR Sm<n) -- n = S n
        = ap3
            (λ Sm≤3+n? SSm≤3+n? SSSm≤3+n? → Ker/Im
              (coboundary-template ⊙skel SSm≤3+n? SSSm≤3+n?)
              (coboundary-template ⊙skel Sm≤3+n? SSm≤3+n?)
              (cochain-is-abelian-template ⊙skel SSm≤3+n?))
            (≤-dec-has-all-paths (≤-dec (1 + m) (3 + n)) (inl (lteSR $ lteSR $ lteSR (inr Sm<n))))
            (≤-dec-has-all-paths (≤-dec (2 + m) (3 + n)) (inl (≤-+-l 1 (lteSR $ lteSR $ inr Sm<n))))
            (≤-dec-has-all-paths (≤-dec (3 + m) (3 + n)) (inl (≤-+-l 2 (lteSR (inr Sm<n)))))
        ∙ ap2
            (λ δ₁ δ₂ → Ker/Im δ₂ δ₁
              (CXₙ/Xₙ₋₁-is-abelian (⊙cw-take (≤-+-l 1 (lteSR $ lteSR $ inr Sm<n)) ⊙skel) (ℕ-to-ℤ (2 + m))))
            (coboundary-higher-template-descend-from-far {n = 2 + n} ⊙skel {m = m}   (ltSR (ltSR Sm<n))    (<-+-l 1 (ltSR Sm<n)))
            (coboundary-higher-template-descend-from-far {n = 2 + n} ⊙skel {m = S m} (<-+-l 1 (ltSR Sm<n)) (<-+-l 2 Sm<n))
        ∙ ap3
            (λ Sm≤2+n? SSm≤2+n? SSSm≤2+n? → Ker/Im
              (coboundary-template (⊙cw-init ⊙skel) SSm≤2+n? SSSm≤2+n?)
              (coboundary-template (⊙cw-init ⊙skel) Sm≤2+n? SSm≤2+n?)
              (cochain-is-abelian-template (⊙cw-init ⊙skel) SSm≤2+n?))
            (≤-dec-has-all-paths (inl (lteSR $ lteSR $ inr Sm<n))   (≤-dec (1 + m) (2 + n)))
            (≤-dec-has-all-paths (inl (≤-+-l 1 (lteSR $ inr Sm<n))) (≤-dec (2 + m) (2 + n)))
            (≤-dec-has-all-paths (inl (≤-+-l 2 (inr Sm<n)))         (≤-dec (3 + m) (2 + n)))

      higher-cohomology-group-β : ∀ {n} (⊙skel : ⊙Skeleton {i} (3 + n))
        →  cohomology-group (cochain-complex ⊙skel) (ℕ-to-ℤ (2 + n))
        == Ker/Im
            (HC.cw-co∂-last ⊙skel)
            (HC.cw-co∂-last (⊙cw-init ⊙skel))
            (CXₙ/Xₙ₋₁-is-abelian (⊙cw-init ⊙skel) (ℕ-to-ℤ (2 + n)))
      higher-cohomology-group-β {n} ⊙skel
        = ap3
            (λ 1+n≤3+n? 2+n≤3+n? 3+n≤3+n? → Ker/Im
              (coboundary-template ⊙skel 2+n≤3+n? 3+n≤3+n?)
              (coboundary-template ⊙skel 1+n≤3+n? 2+n≤3+n?)
              (cochain-is-abelian-template ⊙skel 2+n≤3+n?))
            (≤-dec-has-all-paths (≤-dec (1 + n) (3 + n)) (inl (lteSR lteS)))
            (≤-dec-has-all-paths (≤-dec (2 + n) (3 + n)) (inl lteS))
            (≤-dec-has-all-paths (≤-dec (3 + n) (3 + n)) (inl lteE))
        ∙ ap2 (λ δ₁ δ₂ → Ker/Im δ₂ δ₁ (CXₙ/Xₙ₋₁-is-abelian (⊙cw-init ⊙skel) (ℕ-to-ℤ (2 + n))))
            ( coboundary-higher-template-descend-from-one-above ⊙skel
            ∙ coboundary-higher-template-β (⊙cw-init ⊙skel))
            (coboundary-higher-template-β ⊙skel)

      higher-cohomology-group-β-one-below : ∀ {n} (⊙skel : ⊙Skeleton {i} (2 + n))
        →  cohomology-group (cochain-complex ⊙skel) (ℕ-to-ℤ (2 + n))
        == Ker/Im
            (cst-hom {H = Lift-group {j = i} Unit-group})
            (HC.cw-co∂-last ⊙skel)
            (CXₙ/Xₙ₋₁-is-abelian ⊙skel (ℕ-to-ℤ (2 + n)))
      higher-cohomology-group-β-one-below {n} ⊙skel
        = ap3
            (λ 1+n≤2+n? 2+n≤2+n? 3+n≤2+n? → Ker/Im
              (coboundary-template ⊙skel 2+n≤2+n? 3+n≤2+n?)
              (coboundary-template ⊙skel 1+n≤2+n? 2+n≤2+n?)
              (cochain-is-abelian-template ⊙skel 2+n≤2+n?))
            (≤-dec-has-all-paths (≤-dec (1 + n) (2 + n)) (inl lteS))
            (≤-dec-has-all-paths (≤-dec (2 + n) (2 + n)) (inl lteE))
            (≤-dec-has-all-paths (≤-dec (3 + n) (2 + n)) (inr (<-to-≱ ltS)))
        ∙ ap
            (λ δ₁ → Ker/Im
              (cst-hom {H = Lift-group {j = i} Unit-group})
              δ₁ (CXₙ/Xₙ₋₁-is-abelian ⊙skel (ℕ-to-ℤ (2 + n))))
            (coboundary-higher-template-β ⊙skel)

      higher-cohomology-group-β-far-below : ∀ {n} (⊙skel : ⊙Skeleton {i} n) {m} (SSm≰n : ¬ (2 + m ≤ n))
        →  cohomology-group (cochain-complex ⊙skel) (ℕ-to-ℤ (2 + m))
        == Ker/Im
            (cst-hom {H = Lift-group {j = i} Unit-group})
            (cst-hom
              {G = AbGroup.grp (cochain-template ⊙skel (≤-dec (1 + m) n))}
              {H = Lift-group {j = i} Unit-group})
            (snd (Lift-abgroup {j = i} Unit-abgroup))
      higher-cohomology-group-β-far-below {n} ⊙skel {m} SSm≰n
        = ap2
            (λ 2+m≤n? 3+m≤n? → Ker/Im
              (coboundary-template ⊙skel 2+m≤n? 3+m≤n?)
              (coboundary-template ⊙skel (≤-dec (1 + m) n) 2+m≤n?)
              (cochain-is-abelian-template ⊙skel 2+m≤n?))
            (≤-dec-has-all-paths (≤-dec (2 + m) n) (inr SSm≰n))
            (≤-dec-has-all-paths (≤-dec (3 + m) n) (inr (λ SSSm≤n → SSm≰n (≤-trans lteS SSSm≤n))))

  abstract
    higher-cohomology-group : ∀ m {n} (⊙skel : ⊙Skeleton {i} n)
      → ⊙has-cells-with-choice 0 ⊙skel i
      → C (ℕ-to-ℤ (2 + m)) ⊙⟦ ⊙skel ⟧ ≃ᴳ cohomology-group (cochain-complex ⊙skel) (ℕ-to-ℤ (2 + m))
    higher-cohomology-group m {n = 0} ⊙skel ac =
      CGTH.C-cw-iso-ker/im (2 + m) (O<S (S m)) (Lift-group {j = i} Unit-group) ⊙skel ac
    higher-cohomology-group m {n = 1} ⊙skel ac =
      CGTH.C-cw-iso-ker/im (2 + m) (<-+-l 1 (O<S m))
        (AbGroup.grp (cochain-template ⊙skel (≤-dec (1 + m) 1)))
        ⊙skel ac
    higher-cohomology-group m {n = S (S n)} ⊙skel ac with ℕ-trichotomy (S m) (S n)
    ... | inl idp = coe!ᴳ-iso (higher-cohomology-group-β-one-below ⊙skel)
                ∘eᴳ HCGD.C-cw-iso-ker/im ⊙skel ac
    ... | inr (inl ltS) = coe!ᴳ-iso (higher-cohomology-group-β ⊙skel)
                      ∘eᴳ HCG.C-cw-iso-ker/im ⊙skel ac
    ... | inr (inl (ltSR Sm<n)) =
                coe!ᴳ-iso (higher-cohomology-group-descend ⊙skel Sm<n)
            ∘eᴳ higher-cohomology-group m {n = S n} (⊙cw-init ⊙skel) (⊙init-has-cells-with-choice ⊙skel ac)
            ∘eᴳ C-cw-descend-at-lower ⊙skel (<-+-l 1 Sm<n) ac
    ... | inr (inr Sn<Sm) =
                coe!ᴳ-iso (higher-cohomology-group-β-far-below ⊙skel (<-to-≱ (<-+-l 1 Sn<Sm)))
            ∘eᴳ CGTH.C-cw-iso-ker/im (2 + m) (<-+-l 1 Sn<Sm)
                  (AbGroup.grp (cochain-template ⊙skel (≤-dec (1 + m) (2 + n))))
                  ⊙skel ac

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Verifier
    (down : Set₁ -> Set)
    (up : Set → Set₁)
    (iso : ∀ {A} → down (up A) -> A)
    (osi : ∀ {A} → up (down A) -> A) where

import UniverseCollapse as UC
open UC down up iso osi using (anything)

check : (A : Set) -> A
check = anything

ext: agda

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
module Data.Bin.DivMod where

 import Data.Fin
 import Data.Product
 import Data.Bin
 import Data.Nat
 import Relation.Binary.PropositionalEquality
 import Data.Digit hiding (0b; 1b)
 import Data.List
 import Algebra
 import Algebra.Structures
 import Data.Bin.NatHelpers

 open Data.Bin using (Bin; toℕ; toBits; fromBits; _1#; 0#; 2+_; 0b; 1b)
 module PropEq = Relation.Binary.PropositionalEquality

 open Data.List using (_∷_; []; List)
 open Data.Nat using (ℕ; zero; suc)
 import Data.Nat.Properties

 open import Data.Bin.Utils

 open import Data.Bin.Bijection using (fromℕ-bijection; fromℕ; toℕ-inj; toFromℕ-inverse)

 import Data.Bin.Addition

 module Properties where

  open import Data.Bin.Multiplication
  open Data.Bin using () renaming (_+_ to _B+_; _*_ to _B*_)
  open Algebra.Structures using (IsCommutativeMonoid; module IsCommutativeSemiring)
  open PropEq
  open Data.Nat using (_+_; _*_)
  open Data.Nat.Properties using (isCommutativeSemiring)
  open IsCommutativeSemiring isCommutativeSemiring

 module Everything where

  open Data.Bin using (_1#; 0#; Bin; _+_; _*2; _*2+1; toℕ; ⌊_/2⌋; _*_; less)
  open import Data.Bin.Properties using (<-strictTotalOrder)
  open import Function
  open Data.Product
  open import Relation.Binary
  open Relation.Binary.PropositionalEquality renaming (setoid to ≡-setoid)
  open import Relation.Nullary
  open import Relation.Nullary.Decidable
  open Data.Fin using (zero; suc)
  open Data.List using (_∷_; [])

  open StrictTotalOrder <-strictTotalOrder hiding (trans)

  open import Data.Bin.Minus using (_-_)

  BinFin : Bin → Set
  BinFin n = ∃ λ x → x < n

  toBin : ∀ {x} → BinFin x → Bin
  toBin = proj₁

{-  data DivMod : Bin → Bin → Set where
    result : ∀ {divisor : Bin} (q : Bin) (r : BinFin divisor) → DivMod (toBin r + q * divisor) divisor-}

  data DivMod' (dividend : Bin) (divisor : Bin) : Set where
    result : (q : Bin) (r : BinFin divisor) → (eq : dividend ≡ toBin r + q * divisor) → DivMod' dividend divisor

  open Data.Digit

  open Data.Bin using (addBitLists; addBits; toBits; fromBits)

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

  import Data.Bin.Bijection

  import Data.Bin.Multiplication

  open Algebra.Structures using (module IsCommutativeMonoid)

  import Data.Bin.Props
  open Data.Bin.Props using (*-distrib; *2-is-2*; *2-distrib)
  open IsCommutativeMonoid Data.Bin.Props.bin-+-is-comm-monoid using ()
    renaming (identity to +-identity; comm to +-comm; assoc to +-assoc)

  open IsCommutativeMonoid Data.Bin.Props.bin-*-is-comm-monoid using () renaming (comm to *-comm)

  *-distribˡ : ∀ {a b c} → c * (a + b) ≡ c * a + c * b
  *-distribˡ {a} {b} {c} = *-comm c (a + b) ⟨ trans ⟩ *-distrib {a} {b} {c} ⟨ trans ⟩ cong₂ _+_ (*-comm a c) (*-comm b c)

  *-*2-assoc : ∀ {a b} → (a * b) *2 ≡ a *2 * b
  *-*2-assoc {a} {b} = Data.Bin.Multiplication.*-*2-comm a b

  *2-cong : ∀ {a b} → a ≡ b → a *2 ≡ b *2
  *2-cong = cong _*2

  +-cong₁ : ∀ {a b c} → a ≡ b → a + c ≡ b + c
  +-cong₁ {c = c} = cong (λ z → z + c)

  +-cong₂ : ∀ {a b c} → a ≡ b → c + a ≡ c + b
  +-cong₂ {c = c} = cong (λ z → c + z)

  +-identityʳ = proj₂ +-identity

  divMod2-lem : ∀ {a} → a ≡ ⌊ a /2⌋ *2 + a %2
  divMod2-lem {0#} = refl
  divMod2-lem {[] 1#} = refl
  divMod2-lem {(zero ∷ xs) 1#} = sym (+-identityʳ (⌊ (zero ∷ xs) 1# /2⌋ *2))
  divMod2-lem {(suc zero ∷ xs) 1#} = Data.Bin.Multiplication.∷1#-interpretation (suc zero) xs
                               ⟨ trans ⟩ +-comm ([] 1#) ((zero ∷ xs) 1#)
  divMod2-lem {(suc (suc ()) ∷ xs) 1#}

  import Relation.Binary.EqReasoning
  open import Data.Bin.Props

  helper' : ∀ l → ⌊ l 1# /2⌋ < l 1#
  helper' [] = Data.Bin.less (Data.Nat.s≤s Data.Nat.z≤n)
  helper' (x ∷ xs) = Data.Bin.less (Data.Bin.NatHelpers.kojojo x (toℕ (xs 1#)) (1+≢0 xs))

  helper : ∀ {a} {d} → (≢0 : False (d ≟ fromℕ 0)) → ¬ (a < d) → ⌊ a /2⌋ < a
  helper {_} {0#} () _
  helper {0#} {l 1#} _ a≮d = ⊥-elim (a≮d (z<nz l))
  helper {l 1#} _ _ = helper' l

  open import Data.Sum

  _≤_ : Bin → Bin → Set
  a ≤ b = a ≡ b ⊎ a < b

  ¬>→< : ∀ {a b} → ¬ (b ≤ a) → a < b
  ¬>→< {a} {b} a≰b with compare a b
  ... | tri< a<b _ _ = a<b
  ... | tri≈ _ a≡b _ = ⊥-elim (a≰b (inj₁ (sym a≡b)))
  ... | tri> _ _ a>b = ⊥-elim (a≰b (inj₂ a>b))

  *2-gives-space : ∀ {x y z} → (x < y) → z < fromℕ 2 → x *2 + z < y *2
  *2-gives-space {x} {y} {z} (less x<y) (less z<2) = less (finalize (Data.Bin.NatHelpers.*2-gives-space x<y z<2)) where
    open Data.Nat using () renaming (_*_ to _ℕ*_; _+_ to _ℕ+_; _<_ to _ℕ<_)

    eq1 : toℕ x ℕ* 2 ℕ+ toℕ z ≡ toℕ (x *2 + z)
    eq1 = sym (Data.Bin.Addition.+-is-addition (x *2) z ⟨ trans ⟩ cong (λ q → q ℕ+ toℕ z) (Data.Bin.Multiplication.*2-is-*2 x))
    eq2 : toℕ y ℕ* 2 ≡ toℕ (y *2)
    eq2 = sym (Data.Bin.Multiplication.*2-is-*2 y)

    finalize : toℕ x ℕ* 2 ℕ+ toℕ z ℕ< toℕ y ℕ* 2 → toℕ (x *2 + z) ℕ< toℕ (y *2)
    finalize = subst₂  _ℕ<_ eq1 eq2

  <-pres₁ : ∀ {a b c} → a ≡ b → a < c → b < c
  <-pres₁ refl eq = eq

  <-pres₂ : ∀ {a b c} → a ≡ b → c < a → c < b
  <-pres₂ refl eq = eq

  *-identityˡ : ∀ {x} → [] 1# * x ≡ x
  *-identityˡ = refl

  x*2≡x+x : ∀ {x} → x *2 ≡ x + x
  x*2≡x+x {x} = *2-is-2* x ⟨ trans ⟩ *-distrib {[] 1#} {[] 1#} {x} ⟨ trans ⟩ cong₂ _+_ (*-identityˡ {x}) (*-identityˡ {x})

  %2<2 : ∀ {x} → x %2 < fromℕ 2
  %2<2 {0#} = Data.Bin.less (Data.Nat.s≤s Data.Nat.z≤n)
  %2<2 {[] 1#} = Data.Bin.less (Data.Nat.s≤s (Data.Nat.s≤s Data.Nat.z≤n))
  %2<2 {(zero ∷ xs) 1#} = Data.Bin.less (Data.Nat.s≤s Data.Nat.z≤n)
  %2<2 {(suc zero ∷ xs) 1#} = Data.Bin.less (Data.Nat.s≤s (Data.Nat.s≤s Data.Nat.z≤n))
  %2<2 {(suc (suc ()) ∷ xs) 1#}

  -+-elim : ∀ {x z} → ¬ x < z → x - z + z ≡ x
  -+-elim = Data.Bin.Minus.-+-elim'

  open import Data.Bin.Addition using (+-is-addition)

  open import Data.Bin.Minus using (_-?_; positive; negative; equal; Greater; greater)

  lemma1 : ∀ (f d q : Bin) → (d + f) + q * d ≡ f + (fromℕ 1 + q) * d
  lemma1 f d q =
    let open ≡-Reasoning in
    begin
      (d + f) + q * d
        ≡⟨ +-cong₁ {c = q * d} (+-comm d f) ⟩
      (f + d) + q * d
        ≡⟨ +-assoc f d (q * d) ⟩
      f + (d + q * d)
        ≡⟨ +-cong₂ {c = f} (+-cong₁ {c = q * d} (*-identityˡ {d})) ⟩
      f + ((fromℕ 1 * d) + q * d)
        ≡⟨ +-cong₂ {c = f} (PropEq.sym (*-distrib {fromℕ 1} {q} {d}))  ⟩
      f + (fromℕ 1 + q) * d
    ∎

  lemma2 : ∀ d q → d + q * d ≡ d + 0# + q * d
  lemma2 d q =  cong₂ _+_ (sym (proj₂ +-identity d)) (refl {x = q * d})

  open import Algebra.FunctionProperties
    using (LeftCancellative; RightCancellative; Cancellative)

  +-cancelˡ-< : LeftCancellative Data.Nat._<_ Data.Nat._+_
  +-cancelˡ-< c {y} {z} le =
    Data.Nat.Properties.+-cancelˡ-≤ c
      (subst₂ Data.Nat._≤_
        (PropEq.sym (Data.Nat.Properties.+-suc c y))
        (PropEq.refl {x = (Data.Nat._+_ c z)}) le)

  +-<-left-cancellative : LeftCancellative _<_ _+_
  +-<-left-cancellative c {a} {b} (less le) = less (+-cancelˡ-< (toℕ c) brr) where
     brr : toℕ c Data.Nat.+ toℕ a Data.Nat.< toℕ c Data.Nat.+ toℕ b
     brr = (subst₂ Data.Nat._<_
         (Data.Bin.Addition.+-is-addition c a)
         (Data.Bin.Addition.+-is-addition c b) le)

  +-elim₂ : RightCancellative _<_ _+_
  +-elim₂ {z} x y (less lt) rewrite +-is-addition x z | +-is-addition y z = less (Data.Bin.NatHelpers.+-elim₂ {toℕ x} {toℕ y} {toℕ z} lt)

  fixup-divmod :
    ∀ a d q r
    → a ≡ r + q * d
    → r < d + d
    → DivMod' a d
  fixup-divmod a d q r eq not-too-big =
    case r -? d of λ {
      (positive (greater diff PropEq.refl)) →
        result
          (fromℕ 1 + q)
          (diff 1# , +-<-left-cancellative d not-too-big)
          (PropEq.trans eq (lemma1 (diff 1#) d q));
      (negative x) → result q (r , Data.Bin.Minus.greater-to-< _ _ x) eq ;
      (equal PropEq.refl) →
        result
          (fromℕ 1 + q)
          (0# ,
            (+-<-left-cancellative
              d
              (subst (λ z → z < d + d) (PropEq.sym (proj₂ +-identity _)) not-too-big )) )
          (PropEq.trans eq (PropEq.trans (lemma2 d q) (lemma1 0# d q)))
       }

  lemma3 : ∀ r q d bit → (r + q * d) *2 + bit ≡ (r *2 + bit) + q *2 * d
  lemma3 r q d bit =
    let open ≡-Reasoning in
    begin
      (r + q * d) *2 + bit
        ≡⟨ +-cong₁ {c = bit}
           (begin
             (r + q * d) *2
               ≡⟨ *2-distrib r (q * d) ⟩
             r *2 + (q * d) *2
               ≡⟨ +-comm (r *2) ((q * d) *2) ⟩
             (q * d) *2 + r *2
           ∎) ⟩
      ((q * d) *2 + r *2) + bit
        ≡⟨ +-assoc ((q * d) *2) (r *2) (bit) ⟩
      (q * d) *2 + (r *2 + bit)
        ≡⟨ +-comm ((q * d) *2) (r *2 + bit) ⟩
      (r *2 + bit) + (q * d) *2
        ≡⟨ +-cong₂ {c = r *2 + bit} (*-*2-assoc {q} {d})  ⟩
      (r *2 + bit) + q *2 * d
    ∎

  dm-step :
    ∀ a d q (r : BinFin d) → a ≡ toBin r + q * d →
    ∀ w (bit : BinFin (fromℕ 2))
    → w ≡ (a *2 + proj₁ bit)
    → DivMod' w d
  dm-step ._ d q (r' , r'<d) refl ._ (bit , bit<2) refl =
    fixup-divmod
      _ d (q *2) (r' *2 + bit)
      (lemma3 r' q d bit)
      (<-pres₂ x*2≡x+x (*2-gives-space {r'} {d} {bit} r'<d (bit<2)))

  dmRec : (d : Bin) → {≢0 : False (d ≟ fromℕ 0)} → (a : Bin) → ((a' : Bin) → (a' < a) → DivMod' a' d) → DivMod' a d
  dmRec d {≢0} a rec =
    case a <? d of λ {
      (yes a<d) → result (0#) (a , a<d) (sym (+-identityʳ _)) ;
      (no ¬a<d) →
        case rec ⌊ a /2⌋ (helper ≢0 ¬a<d) of
          λ { (result q r eq) →
            dm-step ⌊ a /2⌋ d q r eq a (a %2 , %2<2) divMod2-lem } }

  import Data.Bin.Rec

  _divMod_ : (a : Bin) → (d : Bin) → {≢0 : False (d ≟ fromℕ 0)} → DivMod' a d
  _divMod_ a d {≡0} = Data.Bin.Rec.rec (λ x → DivMod' x d) (dmRec d {≡0}) a

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.ZariskiLattice.Base where

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

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_
                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm
                                      ; ·-identityʳ to ·ℕ-rid)
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Data.Unit
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Poset

open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.BinomialThm
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.RadicalIdeal
open import Cubical.Algebra.RingSolver.Reflection
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.Matrix

open import Cubical.HITs.SetQuotients as SQ

open Iso
open BinaryRelation
open isEquivRel

private
  variable
    ℓ ℓ' : Level

module ZarLat (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 open RingTheory (CommRing→Ring R')
 open Sum (CommRing→Ring R')
 open CommRingTheory R'
 open Exponentiation R'
 open BinomialThm R'
 open CommIdeal R'
 open RadicalIdeal R'
 open isCommIdeal
 open ProdFin R'

 private
  R = fst R'
  A = Σ[ n ∈ ℕ ] (FinVec R n)
  ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
  ⟨ V ⟩ = ⟨ V ⟩[ R' ]

 _∼_ : A → A → Type (ℓ-suc ℓ)
 (_ , α) ∼ (_ , β) = √ ⟨ α ⟩ ≡ √ ⟨ β ⟩

 ∼EquivRel : isEquivRel (_∼_)
 reflexive ∼EquivRel _ = refl
 symmetric ∼EquivRel _ _ = sym
 transitive ∼EquivRel _ _ _ = _∙_

 ZL : Type (ℓ-suc ℓ)
 ZL = A / _∼_

 0z : ZL
 0z = [ 0 , (λ ()) ]

 1z : ZL
 1z = [ 1 , (replicateFinVec 1 1r) ]

 _∨z_ : ZL → ZL → ZL
 _∨z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
                          (λ (_ , α) (_ , β) → (_ , α ++Fin β))
   (λ (_ , α) (_ , β) → cong √ (FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α)))
    λ (_ , α) (_ , β) (_ , γ) α∼β → --need to show α∨γ ∼ β∨γ
      √ ⟨ α ++Fin γ ⟩      ≡⟨ cong √ (FGIdealAddLemma _ α γ) ⟩
      √ (⟨ α ⟩ +i ⟨ γ ⟩)    ≡⟨ sym (√+LContr _ _) ⟩
      √ (√ ⟨ α ⟩ +i ⟨ γ ⟩) ≡⟨ cong (λ I → √ (I +i ⟨ γ ⟩)) α∼β ⟩
      √ (√ ⟨ β ⟩ +i ⟨ γ ⟩) ≡⟨ √+LContr _ _ ⟩
      √ (⟨ β ⟩ +i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealAddLemma _ β γ)) ⟩
      √ ⟨ β ++Fin γ ⟩ ∎

 _∧z_ : ZL → ZL → ZL
 _∧z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
                          (λ (_ , α) (_ , β) → (_ , α ··Fin β))
   (λ (_ , α) (_ , β) → cong √ (FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α)))
    λ (_ , α) (_ , β) (_ , γ) α∼β → --need to show α∧γ ∼ β∧γ
      √ ⟨ α ··Fin γ ⟩       ≡⟨ cong √ (FGIdealMultLemma _ α γ) ⟩
      √ (⟨ α ⟩ ·i ⟨ γ ⟩)    ≡⟨ sym (√·LContr _ _) ⟩
      √ (√ ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong (λ I → √ (I ·i ⟨ γ ⟩)) α∼β ⟩
      √ (√ ⟨ β ⟩ ·i ⟨ γ ⟩) ≡⟨ √·LContr _ _ ⟩
      √ (⟨ β ⟩ ·i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealMultLemma _ β γ)) ⟩
      √ ⟨ β ··Fin γ ⟩ ∎

 -- join axioms
 ∨zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∨z (𝔟 ∨z 𝔠) ≡ (𝔞 ∨z 𝔟) ∨z 𝔠
 ∨zAssoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
          λ (_ , α) (_ , β) (_ , γ) → eq/ _ _ (cong √ (IdealAddAssoc _ _ _ _))

 ∨zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∨z 𝔟 ≡ 𝔟 ∨z 𝔞
 ∨zComm = SQ.elimProp2 (λ _ _ → squash/ _ _)
        λ (_ , α) (_ , β) → eq/ _ _
          (cong √ (FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α)))

 ∨zLid : ∀ (𝔞 : ZL) → 0z ∨z 𝔞 ≡ 𝔞
 ∨zLid = SQ.elimProp (λ _ → squash/ _ _) λ _ → eq/ _ _ refl

 ∨zRid : ∀ (𝔞 : ZL) → 𝔞 ∨z 0z ≡ 𝔞
 ∨zRid _ = ∨zComm _ _ ∙ ∨zLid _

 -- -- meet axioms
 ∧zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∧z 𝔠) ≡ (𝔞 ∧z 𝔟) ∧z 𝔠
 ∧zAssoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
    λ (_ , α) (_ , β) (_ , γ) → eq/ _ _
      (√ ⟨ α ··Fin (β ··Fin γ) ⟩     ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
       √ (⟨ α ⟩ ·i ⟨ β ··Fin γ ⟩)    ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealMultLemma _ _ _) ⟩
       √ (⟨ α ⟩ ·i (⟨ β ⟩ ·i ⟨ γ ⟩)) ≡⟨ cong √ (·iAssoc _ _ _) ⟩
       √ ((⟨ α ⟩ ·i ⟨ β ⟩) ·i ⟨ γ ⟩) ≡⟨ cong (λ x → √ (x ·i ⟨ γ ⟩)) (sym (FGIdealMultLemma _ _ _)) ⟩
       √ (⟨ α ··Fin β ⟩ ·i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealMultLemma _ _ _)) ⟩
       √ ⟨ (α ··Fin β) ··Fin γ ⟩     ∎)

 ∧zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z 𝔟 ≡ 𝔟 ∧z 𝔞
 ∧zComm = SQ.elimProp2 (λ _ _ → squash/ _ _)
        λ (_ , α) (_ , β) → eq/ _ _
          (cong √ (FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α)))

 ∧zRid : ∀ (𝔞 : ZL) → 𝔞 ∧z 1z ≡ 𝔞
 ∧zRid = SQ.elimProp (λ _ → squash/ _ _)
   λ (_ , α) → eq/ _ _ (cong √
     (⟨ α ··Fin (replicateFinVec 1 1r) ⟩ ≡⟨ FGIdealMultLemma _ _ _ ⟩
      ⟨ α ⟩ ·i ⟨ (replicateFinVec 1 1r) ⟩ ≡⟨ cong (⟨ α ⟩ ·i_) (contains1Is1 _ (indInIdeal _ _ zero)) ⟩
      ⟨ α ⟩ ·i 1Ideal                     ≡⟨ ·iRid _ ⟩
      ⟨ α ⟩ ∎))

 -- absorption and distributivity
 ∧zAbsorb∨z : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z (𝔞 ∨z 𝔟) ≡ 𝔞
 ∧zAbsorb∨z = SQ.elimProp2 (λ _ _ → squash/ _ _)
            λ (_ , α) (_ , β) → eq/ _ _
              (√ ⟨ α ··Fin (α ++Fin β) ⟩     ≡⟨ cong √ (FGIdealMultLemma _ α (α ++Fin β)) ⟩
               √ (⟨ α ⟩ ·i ⟨ α ++Fin β ⟩)    ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ α β) ⟩
               √ (⟨ α ⟩ ·i (⟨ α ⟩ +i ⟨ β ⟩)) ≡⟨ √·Absorb+ _ _ ⟩
               √ ⟨ α ⟩ ∎)

 ∧zLDist∨z : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∨z 𝔠) ≡ (𝔞 ∧z 𝔟) ∨z (𝔞 ∧z 𝔠)
 ∧zLDist∨z = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
   λ (_ , α) (_ , β) (_ , γ) → eq/ _ _
     (√ ⟨ α ··Fin (β ++Fin γ) ⟩            ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
      √ (⟨ α ⟩ ·i ⟨ β ++Fin γ ⟩)           ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ _ _) ⟩
      √ (⟨ α ⟩ ·i (⟨ β ⟩ +i ⟨ γ ⟩))        ≡⟨ cong √ (·iRdist+i _ _ _) ⟩
      -- L/R-dist are swapped
      -- in Lattices vs Rings
      √ (⟨ α ⟩ ·i ⟨ β ⟩ +i ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong₂ (λ x y → √ (x +i y))
                                                     (sym (FGIdealMultLemma _ _ _))
                                                     (sym (FGIdealMultLemma _ _ _)) ⟩
      √ (⟨ α ··Fin β ⟩ +i ⟨ α ··Fin γ ⟩)   ≡⟨ cong √ (sym (FGIdealAddLemma _ _ _)) ⟩
      √ ⟨ (α ··Fin β) ++Fin (α ··Fin γ) ⟩  ∎)

 ZariskiLattice : DistLattice (ℓ-suc ℓ)
 fst ZariskiLattice = ZL
 DistLatticeStr.0l (snd ZariskiLattice) = 0z
 DistLatticeStr.1l (snd ZariskiLattice) = 1z
 DistLatticeStr._∨l_ (snd ZariskiLattice) = _∨z_
 DistLatticeStr._∧l_ (snd ZariskiLattice) = _∧z_
 DistLatticeStr.isDistLattice (snd ZariskiLattice) =
   makeIsDistLattice∧lOver∨l squash/ ∨zAssoc ∨zRid ∨zComm
                                       ∧zAssoc ∧zRid ∧zComm ∧zAbsorb∨z ∧zLDist∨z

-- An equivalent definition that doesn't bump up the unviverse level
module SmallZarLat (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 open CommIdeal R'
 open RadicalIdeal R'
 open ZarLat R'

 open Iso

 private
  R = fst R'
  A = Σ[ n ∈ ℕ ] (FinVec R n)
  ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
  ⟨ V ⟩ = ⟨ V ⟩[ R' ]
  -- This is small!
  _≼_ : A → A → Type ℓ
  (_ , α) ≼ (_ , β) = ∀ i → α i ∈ √ ⟨ β ⟩

 _∼'_ :  A → A → Type ℓ
 α ∼' β = (α ≼ β) × (β ≼ α)

 -- lives in the same universe as R
 ZL' : Type ℓ
 ZL' = A / (_∼'_)

 IsoLarLatSmall : Iso ZL ZL'
 IsoLarLatSmall = relBiimpl→TruncIso ~→∼' ~'→∼
  where
  ~→∼' : ∀ {a b : A} → a ∼ b → a ∼' b
  ~→∼' r = √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) r h)
         , √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) (sym r) h)

  ~'→∼ : ∀ {a b : A} → a ∼' b → a ∼ b
  ~'→∼ r = CommIdeal≡Char (√FGIdealCharRImpl _ ⟨ _ ⟩ (fst r))
                          (√FGIdealCharRImpl _ ⟨ _ ⟩ (snd r))

 ZL≃ZL' : ZL ≃ ZL'
 ZL≃ZL' = isoToEquiv IsoLarLatSmall

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Theorems with different connectives.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems.Mixies ( n : ℕ ) where

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

open import Data.PropFormula.Syntax n
open import Data.PropFormula.Theorems.Classical n
open import Data.PropFormula.Theorems.Biimplication n
  using ( ⇔-¬-to-¬; ⊃-⇔-¬∨ )
open import Data.PropFormula.Theorems.Disjunction n
  using ( ∨-dmorgan; ∨-dmorgan₁ )
open import Data.PropFormula.Theorems.Implication n
  using ( vanDalen244e; ⊃-equiv )
open import Data.PropFormula.Theorems.Weakening n

open import Function using ( _$_ ; _∘_ )

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

-- Theorem.
e245b
  : ∀ {Γ Δ} {φ ψ}
  → Γ ⊢ φ → Δ , φ ⊢ ψ
  → Γ ⨆ Δ ⊢ ψ

-- Proof.
e245b {Γ}{Δ} Γ⊢φ Δ,φ⊢ψ =
  ⊃-elim
    (weaken-Δ₂ Γ $ ⊃-intro Δ,φ⊢ψ)
    (weaken-Δ₁ Δ Γ⊢φ)
-------------------------------------------------------------------------- ∎

-- Theorem.
¬⊃-to-∧¬
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ (φ ⊃ ψ)
  → Γ ⊢ φ ∧ ¬ ψ

-- Proof.
¬⊃-to-∧¬ {Γ}{φ}{ψ} Γ⊢¬⟪φ⊃ψ⟫ =
  ∧-intro
    (⊃-elim vanDalen244e (∧-proj₁ p2))
    (∧-proj₂ p2)
  where
    p1 : Γ ⊢ ¬ (¬ φ ∨ ψ)
    p1 = ⇔-¬-to-¬ ⊃-⇔-¬∨ Γ⊢¬⟪φ⊃ψ⟫

    p2 : Γ ⊢ ¬ (¬ φ) ∧  ¬ ψ
    p2 = ∨-dmorgan₁ p1
-------------------------------------------------------------------------- ∎

-- Theorem.
⊃¬∧¬⊃-to-¬⇔
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ (φ ⊃ ¬ ψ) ∧ (¬ ψ ⊃ φ)
  → Γ ⊢ ¬ (φ ⇔ ψ)

-- Proof.
⊃¬∧¬⊃-to-¬⇔ {Γ}{φ}{ψ} thm =
 ¬-intro
   (¬-elim
     (¬-intro
       (¬-elim
         (⊃-elim
           (weaken ψ (weaken (φ ⇔ ψ) (∧-proj₁ thm)))
           (⇔-elim₂
             (assume {Γ = Γ , φ ⇔ ψ} ψ)
             (weaken ψ (assume (φ ⇔ ψ)))))
         (assume {Γ = Γ , φ ⇔ ψ} ψ)))
    (RAA
      (¬-elim
         (¬-intro
           (¬-elim
             (⊃-elim
               (weaken φ (weaken (¬ ψ ) (weaken (φ ⇔ ψ) (∧-proj₁ thm))))
               (assume {Γ = Γ , φ ⇔ ψ , ¬ ψ} φ))
             (⇔-elim₁
               (assume {Γ = Γ , φ ⇔ ψ , ¬ ψ} φ)
               (weaken φ (weaken (¬ ψ) (assume (φ ⇔ ψ)))))))
         (⊃-elim
           (weaken (¬ ψ) (weaken (φ ⇔ ψ) (∧-proj₂ thm)))
           (assume {Γ = Γ , φ ⇔ ψ} (¬ ψ))))))
-------------------------------------------------------------------------- ∎

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of non-empty lists
------------------------------------------------------------------------

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

module Data.List.NonEmpty.Properties where

open import Category.Monad
open import Data.List as List using (List; []; _∷_; _++_)
open import Data.List.Categorical using () renaming (monad to listMonad)
open import Data.List.NonEmpty.Categorical using () renaming (monad to list⁺Monad)
open import Data.List.NonEmpty as List⁺
open import Data.List.Properties
open import Function
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
private
  open module LMo {a} =
         RawMonad {f = a} listMonad
           using () renaming (_>>=_ to _⋆>>=_)
  open module L⁺Mo {a} =
         RawMonad {f = a} list⁺Monad

η : ∀ {a} {A : Set a}
    (xs : List⁺ A) → head xs ∷ tail xs ≡ List⁺.toList xs
η _ = refl

toList-fromList : ∀ {a} {A : Set a} x (xs : List A) →
                  x ∷ xs ≡ List⁺.toList (x ∷ xs)
toList-fromList _ _ = refl

toList-⁺++ : ∀ {a} {A : Set a} (xs : List⁺ A) ys →
             List⁺.toList xs ++ ys ≡
             List⁺.toList (xs ⁺++ ys)
toList-⁺++ _ _ = refl

toList-⁺++⁺ : ∀ {a} {A : Set a} (xs ys : List⁺ A) →
              List⁺.toList xs ++ List⁺.toList ys ≡
              List⁺.toList (xs ⁺++⁺ ys)
toList-⁺++⁺ _ _ = refl

toList->>= : ∀ {ℓ} {A B : Set ℓ}
             (f : A → List⁺ B) (xs : List⁺ A) →
             (List⁺.toList xs ⋆>>= List⁺.toList ∘ f) ≡
             (List⁺.toList (xs >>= f))
toList->>= f (x ∷ xs) = begin
  List.concat (List.map (List⁺.toList ∘ f) (x ∷ xs))
    ≡⟨ cong List.concat $ map-compose {g = List⁺.toList} (x ∷ xs) ⟩
  List.concat (List.map List⁺.toList (List.map f (x ∷ xs)))
    ∎


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

module Categories.Bicategory where

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

open import Categories.Category using (Category; module Commutation)
open import Categories.Category.Monoidal.Instance.Cats using (module Product)
open import Categories.Enriched.Category using () renaming (Category to Enriched)
open import Categories.Functor using (module Functor)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

-- https://ncatlab.org/nlab/show/bicategory
-- notice that some axioms in nLab are inconsistent. they have been fixed in this definition.
record Bicategory o ℓ e t : Set (suc (o ⊔ ℓ ⊔ e ⊔ t)) where
  field
    enriched : Enriched (Product.Cats-Monoidal {o} {ℓ} {e}) t

  open Enriched enriched public
  module hom {A B} = Category (hom A B)
  module ComHom {A B} = Commutation (hom A B)

  infix 4 _⇒₁_ _⇒₂_ _≈_
  infixr 7 _∘ᵥ_ _∘₁_
  infixr 9 _▷_
  infixl 9 _◁_
  infixr 11 _⊚₀_ _⊚₁_  _∘ₕ_

  _⇒₁_ : Obj → Obj → Set o
  A ⇒₁ B = Category.Obj (hom A B)

  _⇒₂_ : {A B : Obj} → A ⇒₁ B → A ⇒₁ B → Set ℓ
  _⇒₂_ = hom._⇒_

  _⊚₀_ : {A B C : Obj} → B ⇒₁ C → A ⇒₁ B → A ⇒₁ C
  f ⊚₀ g = Functor.F₀ ⊚ (f , g)

  _⊚₁_ : {A B C : Obj} {f h : B ⇒₁ C} {g i : A ⇒₁ B} → f ⇒₂ h → g ⇒₂ i → f ⊚₀ g ⇒₂ h ⊚₀ i
  α ⊚₁ β = Functor.F₁ ⊚ (α , β)

  _≈_ : {A B : Obj} {f g : A ⇒₁ B} → Rel (f ⇒₂ g) e
  _≈_ = hom._≈_

  id₁ : {A : Obj} → A ⇒₁ A
  id₁ {_} = Functor.F₀ id _

  id₂ : {A B : Obj} {f : A ⇒₁ B} → f ⇒₂ f
  id₂ {A} {B} = Category.id (hom A B)

  -- 1-cell composition
  _∘₁_ : {A B C : Obj} → B ⇒₁ C → A ⇒₁ B → A ⇒₁ C
  _∘₁_ = _⊚₀_

  -- horizontal composition
  _∘ₕ_ : {A B C : Obj} {f h : B ⇒₁ C} {g i : A ⇒₁ B} → f ⇒₂ h → g ⇒₂ i → f ⊚₀ g ⇒₂ h ⊚₀ i
  _∘ₕ_ = _⊚₁_

  -- vertical composition
  _∘ᵥ_ : {A B : Obj} {f g h : A ⇒₁ B} (α : g ⇒₂ h) (β : f ⇒₂ g) → f ⇒₂ h
  _∘ᵥ_ = hom._∘_

  _◁_ : {A B C : Obj} {g h : B ⇒₁ C} (α : g ⇒₂ h) (f : A ⇒₁ B) → g ∘₁ f ⇒₂ h ∘₁ f
  α ◁ _ = α ⊚₁ id₂

  _▷_ : {A B C : Obj} {f g : A ⇒₁ B} (h : B ⇒₁ C) (α : f ⇒₂ g) → h ∘₁ f ⇒₂ h ∘₁ g
  _ ▷ α = id₂ ⊚₁ α

  private
    λ⇒ : {A B : Obj} {f : A ⇒₁ B} → id₁ ⊚₀ f hom.⇒ f
    λ⇒ {_} {_} {f} = NaturalIsomorphism.⇒.η unitˡ (_ , f)

    ρ⇒ : {A B : Obj} {f : A ⇒₁ B} → f ⊚₀ id₁ hom.⇒ f
    ρ⇒ {_} {_} {f} = NaturalIsomorphism.⇒.η unitʳ (f , _)

    α⇒ : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} →
          ((f ⊚₀ g) ⊚₀ h) hom.⇒ (f ⊚₀ (g ⊚₀ h))
    α⇒ {_} {_} {_} {_} {f} {g} {h} = NaturalIsomorphism.⇒.η ⊚-assoc ((f , g) , h)

  field
    triangle : {A B C : Obj} {f : A ⇒₁ B} {g : B ⇒₁ C} →
                 let open ComHom {A} {C} in
                 [ (g ∘₁ id₁) ∘₁ f ⇒ g ∘₁ f ]⟨
                   α⇒                 ⇒⟨ g ∘₁ id₁ ∘₁ f ⟩
                   g ▷ λ⇒
                 ≈ ρ⇒ ◁ f
                 ⟩
    pentagon : {A B C D E : Obj} {f : A ⇒₁ B} {g : B ⇒₁ C} {h : C ⇒₁ D} {i : D ⇒₁ E} →
                 let open ComHom {A} {E} in
                 [ ((i ∘₁ h) ∘₁ g) ∘₁ f ⇒ i ∘₁ h ∘₁ g ∘₁ f ]⟨
                   α⇒ ◁ f                     ⇒⟨ (i ∘₁ h ∘₁ g) ∘₁ f ⟩
                   α⇒                         ⇒⟨ i ∘₁ (h ∘₁ g) ∘₁ f ⟩
                   i ▷ α⇒
                 ≈ α⇒                         ⇒⟨ (i ∘₁ h) ∘₁ g ∘₁ f ⟩
                   α⇒
                 ⟩

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
{-

Pointed structure: X ↦ X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Pointed where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP

open import Cubical.Foundations.Pointed.Base

private
  variable
    ℓ : Level

-- Structured isomorphisms

PointedStructure : Type ℓ → Type ℓ
PointedStructure X = X

PointedEquivStr : StrEquiv PointedStructure ℓ
PointedEquivStr A B f = equivFun f (pt A) ≡ pt B

pointedUnivalentStr : UnivalentStr {ℓ} PointedStructure PointedEquivStr
pointedUnivalentStr f = invEquiv (ua-ungluePath-Equiv f)

pointedSIP : (A B : Pointed ℓ) → A ≃[ PointedEquivStr ] B ≃ (A ≡ B)
pointedSIP = SIP pointedUnivalentStr

pointed-sip : (A B : Pointed ℓ) → A ≃[ PointedEquivStr ] B → (A ≡ B)
pointed-sip A B = equivFun (pointedSIP A B) -- ≡ λ (e , p) i → ua e i , ua-gluePath e p i

pointedEquivAction : EquivAction {ℓ} PointedStructure
pointedEquivAction e = e

pointedTransportStr : TransportStr {ℓ} pointedEquivAction
pointedTransportStr e s = sym (transportRefl _)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --safe #-}
{-
Builds bismulation for the cumulative hierarchy and shows that it
is equivalent to equality though it lives in a lower universe.
-}

module Cubical.HITs.CumulativeHierarchy.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Functions.Embedding
open import Cubical.Functions.Logic as L
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation as P hiding (elim; elim2)
open import Cubical.HITs.SetQuotients as Q using (_/_; setQuotUniversal; eq/; squash/)

open import Cubical.HITs.CumulativeHierarchy.Base
  renaming (elim to elimInternal)
import Cubical.HITs.PropositionalTruncation.Monad as PropMonad

private
  variable
    ℓ ℓ' : Level
    X Y : Type ℓ
    a b : V ℓ

infix 4 _≊_
infix 7 _∈ₛ_ _⊆_ _⊆ₛ_

------------
-- "bisimulation"
-----------

-- bisimulation is needed to define a quotient in the correct universe when
-- implementing the map : V ℓ → Σ[ X : Type ℓ ] (X → V ℓ)
-- Quotienting by Path (V ℓ) or via eqImage would lead to X : Type (ℓ-suc ℓ)

_∼_ : (s t : V ℓ) → hProp ℓ
_∼_ = elim2 eliminator where
  goalProp : (X : Type ℓ) (ix : X → V ℓ)
           → (Y : Type ℓ) (iy : Y → V ℓ)
           → (rec : X → Y → hProp ℓ)
           → hProp ℓ
  goalProp X ix Y iy rec = (∀[ a ∶ X ] ∃[ b ∶ Y ] rec a b) ⊓ (∀[ b ∶ Y ] ∃[ a ∶ X ] rec a b)

  ⇔-swap : X ⊓′ Y → Y ⊓′ X
  ⇔-swap (p , q) = (q , p)

  open PropMonad
  lemma : {X₁ X₂ Y : Type ℓ} {ix₁ : X₁ → V ℓ} {ix₂ : X₂ → V ℓ} (iy : Y → V ℓ)
        → {rec₁ : X₁ → Y → hProp ℓ} {rec₂ : X₂ → Y → hProp ℓ}
        → (rec₁→₂ : (x₁ : X₁) → ∃[ (x₂ , p) ∈ fiber ix₂ (ix₁ x₁) ] rec₂ x₂ ≡ rec₁ x₁)
        → (rec₂→₁ : (x₂ : X₂) → ∃[ (x₁ , p) ∈ fiber ix₁ (ix₂ x₂) ] rec₁ x₁ ≡ rec₂ x₂)
        → ⟨ goalProp X₁ ix₁ Y iy rec₁ ⇒ goalProp X₂ ix₂ Y iy rec₂ ⟩
  lemma _ rec₁→₂ rec₂→₁ (X₁→Y , Y→X₁) =
    (λ x₂ → do ((x₁ , c_) , xr₁) ← rec₂→₁ x₂
               (y , yr) ← X₁→Y x₁
               ∣ y , subst fst (λ i → xr₁ i y) yr ∣₁
    ) ,
    (λ y → do (x₁ , xr₁) ← Y→X₁ y
              ((x₂ , _) , xr₂) ← rec₁→₂ x₁
              ∣ x₂ , subst fst (λ i → xr₂ (~ i) y) xr₁ ∣₁
    )

  open Elim2Set
  eliminator : Elim2Set (λ _ _ → isSetHProp)
  ElimSett2 eliminator = goalProp
  ElimEqSnd eliminator X ix Y₁ Y₂ iy₁ iy₂ eq rec₁ rec₂ rec₁→₂ rec₂→₁ =
    ⇔toPath (⇔-swap ∘ lemma ix rec₁→₂ rec₂→₁ ∘ ⇔-swap)
            (⇔-swap ∘ lemma ix rec₂→₁ rec₁→₂ ∘ ⇔-swap)
  ElimEqFst eliminator X₁ X₂ ix₁ ix₂ eq Y iy rec₁ rec₂ rec₁→₂ rec₂→₁ =
    ⇔toPath (lemma iy rec₁→₂ rec₂→₁)
            (lemma iy rec₂→₁ rec₁→₂)

_≊_ : (s t : V ℓ) → Type ℓ
s ≊ t = ⟨ s ∼ t ⟩

∼refl : (a : V ℓ) → a ≊ a
∼refl = elimProp (λ a → isProp⟨⟩ (a ∼ a))
                 (λ X ix rec → (λ x → ∣ x , rec x ∣₁) , (λ x → ∣ x , rec x ∣₁))

-- keep in mind that the left and right side here live in different universes
identityPrinciple : (a ≊ b) ≃ (a ≡ b)
identityPrinciple {a = a} {b = b} =
  isoToEquiv (iso from into (λ _ → setIsSet _ _ _ _) (λ _ → isProp⟨⟩ (a ∼ b) _ _))
  where
  open PropMonad

  eqImageXY : {X Y : Type ℓ} {ix : X → V ℓ} {iy : Y → V ℓ} → (∀ x y → ⟨ ix x ∼ iy y ⟩ → ix x ≡ iy y)
            → ⟨ sett X ix ∼ sett Y iy ⟩ → eqImage ix iy
  eqImageXY rec rel = (λ x → do (y , y∼x) ← fst rel x ; ∣ y , sym (rec _ _ y∼x) ∣₁)
                    , (λ y → do (x , x∼y) ← snd rel y ; ∣ x ,      rec _ _ x∼y  ∣₁)

  from : a ≊ b → a ≡ b
  from = elimProp propB eliminator a b where
    prop∼ : {a : V ℓ} → ∀ b → isProp (a ≊ b → a ≡ b)
    prop∼ {a = a} b = isPropΠ λ _ → setIsSet a b
    propB : (a : V ℓ) → isProp (∀ b → a ≊ b → a ≡ b)
    propB a = isPropΠ prop∼
    eliminator :
      ∀ (X : Type _) (ix : X → V _)
      → ((x : X) (b₁ : V _) → ix x ≊ b₁ → ix x ≡ b₁)
      → (b₁ : V _) → sett X ix ≊ b₁ → sett X ix ≡ b₁
    eliminator X ix rec =
      elimProp prop∼ λ Y iy _ → seteq X Y ix iy ∘ eqImageXY (λ x y → rec x (iy y))

  into : a ≡ b → a ≊ b
  into = J (λ b _ → a ≊ b) (∼refl a)

------------
-- Monic presentation of sets
-----------

-- like fiber, but in a lower universe
repFiber : (f : X → V ℓ) (b : V ℓ) → Type _
repFiber f b = Σ[ a ∈ _ ] f a ≊ b

repFiber≃fiber : (f : X → V ℓ) (b : V ℓ) → repFiber f b ≃ fiber f b
repFiber≃fiber f b = Σ-cong-equiv (idEquiv _) (λ _ → identityPrinciple)

-- projecting out a representing type together with the embedding
MonicPresentation : (a : V ℓ) → Type (ℓ-suc ℓ)
MonicPresentation {ℓ} a =  Σ[ (X , ix , _) ∈ Embedding (V ℓ) ℓ ] (a ≡ sett X ix)

isPropMonicPresentation : (a : V ℓ) → isProp (MonicPresentation a)
isPropMonicPresentation a ((X₁ , ix₁ , isEmb₁) , p) ((X₂ , ix₂ , isEmb₂) , q) =
  ΣPathP ( equivFun (EmbeddingIP _ _) (fiberwise1 , fiberwise2)
         , isProp→PathP (λ i → setIsSet a _) p q)
  where
  open PropMonad
  fiberwise1 : ∀ b → fiber ix₁ b → fiber ix₂ b
  fiberwise1 b fbx₁ =
    proof (_ , isEmbedding→hasPropFibers isEmb₂ b)
    by subst (λ A → ⟨ b ∈ A ⟩) (sym p ∙ q) ∣ fbx₁ ∣₁

  fiberwise2 : ∀ b → fiber ix₂ b → fiber ix₁ b
  fiberwise2 b fbx₂ =
    proof (_ , isEmbedding→hasPropFibers isEmb₁ b)
    by subst (λ A → ⟨ b ∈ A ⟩) (sym q ∙ p) ∣ fbx₂ ∣₁

sett-repr : (X : Type ℓ) (ix : X → V ℓ) → MonicPresentation (sett X ix)
sett-repr {ℓ} X ix = (Rep , ixRep , isEmbIxRep) , seteq X Rep ix ixRep eqImIxRep where
  Kernel : X → X → Type ℓ
  Kernel x y = ix x ≊ ix y
  Rep : Type ℓ
  Rep = X / Kernel
  ixRep : Rep → V ℓ
  ixRep = invEq (setQuotUniversal setIsSet) (ix , λ _ _ → equivFun identityPrinciple)
  isEmbIxRep : isEmbedding ixRep
  isEmbIxRep = hasPropFibers→isEmbedding propFibers where
    propFibers : ∀ y → (a b : Σ[ p ∈ Rep ] (ixRep p ≡ y)) → a ≡ b
    propFibers y (p₁ , m) (p₂ , n) =
      ΣPathP {B = λ _ p → ixRep p ≡ y} (goal , isProp→PathP (λ _ → setIsSet _ _) _ _)
      where
      lemma : ∀ {p₁ p₂} → (p : ixRep Q.[ p₁ ] ≡ y) (q : ixRep Q.[ p₂ ] ≡ y) → Kernel p₁ p₂
      lemma m n = invEquiv identityPrinciple .fst (m ∙ sym n)
      prop₁ : ∀ p₁ → isProp ((ixRep p₁ ≡ y) → p₁ ≡ p₂)
      prop₁ p₁ = isPropΠ λ eq → squash/ p₁ p₂
      prop₂ : ∀ {p₁} p₂ → isProp ((ixRep p₂ ≡ y) → Q.[ p₁ ] ≡ p₂)
      prop₂ {p₁} p₂ = isPropΠ λ eq → squash/ Q.[ p₁ ] p₂
      goal : p₁ ≡ p₂
      goal = Q.elimProp prop₁ (λ p₁ m → Q.elimProp prop₂ (λ p₂ n → eq/ p₁ p₂ (lemma m n)) p₂ n) p₁ m

  eqImIxRep : eqImage ix ixRep
  eqImIxRep = (λ x → ∣ Q.[ x ] , refl ∣₁) , Q.elimProp (λ _ → P.squash₁) (λ b → ∣ b , refl ∣₁)

data DeepMonicPresentation (a : V ℓ) : Type (ℓ-suc ℓ) where
  dmp : (mp@((_ , ix , _) , _) : MonicPresentation a)
      → (rec : ∀ x → DeepMonicPresentation (ix x))
      → DeepMonicPresentation a

isPropDeepMonicPresentation : (a : V ℓ) → isProp (DeepMonicPresentation a)
isPropDeepMonicPresentation a (dmp mx rx) (dmp my ry) i = dmp (mx≡my i) (recprop i) where
  mx≡my : mx ≡ my
  mx≡my = isPropMonicPresentation a mx my
  recprop : PathP (λ i → (x : mx≡my i .fst .fst) → DeepMonicPresentation (mx≡my i .fst .snd .fst x)) rx ry
  recprop = toPathP (funExt λ x → isPropDeepMonicPresentation _ _ _)

V-deeprepr : (a : V ℓ) → DeepMonicPresentation a
V-deeprepr = elimProp isPropDeepMonicPresentation λ X ix rec → dmp (sett-repr X ix) (Q.elimProp (λ _ → isPropDeepMonicPresentation _) rec)

V-repr : (a : V ℓ) → MonicPresentation a
-- "Cannot eliminate fibrant type DeepMonicPresentation a
--  unless target type is also fibrant"
-- V-repr = let (dmp mp _) = (V-deeprepr a) in mp
V-repr a = case (V-deeprepr a) return (λ _ → MonicPresentation a) of λ { (dmp mp _) → mp }

private
  MonicDataF : Type (ℓ-suc ℓ) → Type (ℓ-suc ℓ)
  MonicDataF {ℓ} T = Embedding T ℓ

  V-fixpoint : V ℓ ≃ MonicDataF (V ℓ)
  V-fixpoint {ℓ} =
    V ℓ ≃⟨ invEquiv (Σ-contractSnd λ a → inhProp→isContr (V-repr a) (isPropMonicPresentation a)) ⟩
    (Σ[ a ∈ V ℓ ] MonicPresentation a) ≃⟨ boringswap ⟩
    (Σ[ (X , ix , _) ∈ MonicDataF (V ℓ) ] singl (sett X ix)) ≃⟨ Σ-contractSnd (λ _ → isContrSingl _) ⟩
    MonicDataF (V ℓ) ■ where
    boringswap : (Σ[ a ∈ V ℓ ] MonicPresentation a) ≃ (Σ[ (X , ix , _) ∈ MonicDataF (V ℓ) ] singl (sett X ix))
    boringswap = isoToEquiv (iso
      (λ (a , (X , ix , emb) , p) → (X , ix , emb) , a , sym p)
      (λ ((X , ix , emb) , a , p) → a , (X , ix , emb) , sym p)
      (λ _ → refl)
      λ _ → refl)

  -- note the problem of making this a datatype directly: MonicDataF is *not* strictly positive!

-- an elimination principle based on the monic presentation
elim : (B : V ℓ → Type ℓ')
     → ((X : Type ℓ) (ix : X → V ℓ) (emb : isEmbedding ix) (rec : ∀ x → B (ix x)) → B (sett X ix))
     → (a : V ℓ) → B a
elim B alg = elimDMP ∘ V-deeprepr where
  elimDMP : ∀ {a} → DeepMonicPresentation a → B a
  elimDMP (dmp ((X , ix , emb) , p) rec) = subst B (sym p) (alg X ix emb (λ x → elimDMP (rec x)))

⟪_⟫ : (s : V ℓ) → Type ℓ
⟪ X ⟫ = V-repr X .fst .fst

⟪_⟫↪ : (s : V ℓ) → ⟪ s ⟫ → V ℓ
⟪ X ⟫↪ = V-repr X .fst .snd .fst

isEmb⟪_⟫↪ : (s : V ℓ) → isEmbedding ⟪ s ⟫↪
isEmb⟪ X ⟫↪ = V-repr X .fst .snd .snd

⟪_⟫-represents : (s : V ℓ) → s ≡ sett ⟪ s ⟫ ⟪ s ⟫↪
⟪ X ⟫-represents = V-repr X .snd

isPropRepFiber : (a b : V ℓ) → isProp (repFiber ⟪ a ⟫↪ b)
isPropRepFiber a b =
  Embedding-into-isProp→isProp
    (Equiv→Embedding (repFiber≃fiber ⟪ a ⟫↪ b))
    (isEmbedding→hasPropFibers isEmb⟪ a ⟫↪ b)

-- while ∈ is hProp (ℓ-suc ℓ), ∈ₛ is in ℓ
_∈ₛ_ : (a b : V ℓ) → hProp ℓ
a ∈ₛ b = repFiber ⟪ b ⟫↪ a , isPropRepFiber b a

∈-asFiber : {a b : V ℓ} → ⟨ a ∈ b ⟩ → fiber ⟪ b ⟫↪ a
∈-asFiber {a = a} {b = b} =
  subst (λ br → ⟨ a ∈ br ⟩ → fiber ⟪ b ⟫↪ a) (sym ⟪ b ⟫-represents) asRep
  where
  asRep : ⟨ a ∈ sett ⟪ b ⟫ ⟪ b ⟫↪ ⟩ → fiber ⟪ b ⟫↪ a
  asRep = P.propTruncIdempotent≃ (isEmbedding→hasPropFibers isEmb⟪ b ⟫↪ a) .fst
∈-fromFiber : {a b : V ℓ} → fiber ⟪ b ⟫↪ a → ⟨ a ∈ b ⟩
∈-fromFiber {a = a} {b = b} = subst (λ br → ⟨ a ∈ br ⟩) (sym ⟪ b ⟫-represents) ∘ ∣_∣₁

∈∈ₛ : {a b : V ℓ} → ⟨ a ∈ b ⇔ a ∈ₛ b ⟩
∈∈ₛ {a = a} {b = b} = leftToRight , rightToLeft where
  repEquiv : repFiber ⟪ b ⟫↪ a ≃ fiber ⟪ b ⟫↪ a
  repEquiv = repFiber≃fiber ⟪ b ⟫↪ a
  leftToRight : ⟨ (a ∈ b) ⇒ a ∈ₛ b ⟩
  leftToRight a∈b = invEq repEquiv (∈-asFiber {b = b} a∈b)
  rightToLeft : ⟨ a ∈ₛ b ⇒ (a ∈ b) ⟩
  rightToLeft a∈ₛb = ∈-fromFiber {b = b} (equivFun repEquiv a∈ₛb)

ix∈ₛ : {X : Type ℓ} {ix : X → V ℓ}
     → (x : X) → ⟨ ix x ∈ₛ sett X ix ⟩
ix∈ₛ {X = X} {ix = ix} x = ∈∈ₛ {a = ix x} {b = sett X ix} .fst ∣ x , refl ∣₁

∈ₛ⟪_⟫↪_ : (a : V ℓ) (ix : ⟪ a ⟫) → ⟨ ⟪ a ⟫↪ ix ∈ₛ a ⟩
∈ₛ⟪ a ⟫↪ ix = ix , ∼refl (⟪ a ⟫↪ ix)

-- also here, the left side is in level (ℓ-suc ℓ) while the right is in ℓ
presentation : (a : V ℓ) → (Σ[ v ∈ V ℓ ] ⟨ v ∈ₛ a ⟩) ≃ ⟪ a ⟫
presentation a = isoToEquiv (iso into from (λ _ → refl) retr) where
  into : Σ[ v ∈ V _ ] ⟨ v ∈ₛ a ⟩ → ⟪ a ⟫
  into = fst ∘ snd
  from : ⟪ a ⟫ → Σ[ v ∈ V _ ] ⟨ v ∈ₛ a ⟩
  from ⟪a⟫ = ⟪ a ⟫↪ ⟪a⟫ , ∈ₛ⟪ a ⟫↪ ⟪a⟫
  retr : retract into from
  retr s = Σ≡Prop (λ v → (v ∈ₛ a) .snd) (equivFun identityPrinciple (s .snd .snd))

-- subset relation, once in level (ℓ-suc ℓ) and once in ℓ
_⊆_ : (a b : V ℓ) → hProp (ℓ-suc ℓ)
a ⊆ b = ∀[ x ] x ∈ₛ a ⇒ x ∈ₛ b

⊆-refl : (a : V ℓ) → ⟨ a ⊆ a ⟩
⊆-refl a = λ _ xa → xa

_⊆ₛ_ : (a b : V ℓ) → hProp ℓ
a ⊆ₛ b = ∀[ x ] ⟪ a ⟫↪ x ∈ₛ b

⊆⇔⊆ₛ : (a b : V ℓ) → ⟨ a ⊆ b ⇔ a ⊆ₛ b ⟩
⊆⇔⊆ₛ a b =
    (λ s → invEq curryEquiv s ∘ invEq (presentation a))
  , (λ s x xa → subst (λ x → ⟨ x ∈ₛ b ⟩) (equivFun identityPrinciple (xa .snd)) (s (xa .fst)))

-- the homotopy definition of equality as an hProp, we know this is equivalent to bisimulation
infix 4 _≡ₕ_
_≡ₕ_ : (a b : V ℓ) → hProp (ℓ-suc ℓ)
_≡ₕ_ a b = (a ≡ b) , setIsSet a b

-- extensionality
extensionality : ⟨ ∀[ a ∶ V ℓ ] ∀[ b ] (a ⊆ b) ⊓ (b ⊆ a) ⇒ (a ≡ₕ b) ⟩
extensionality {ℓ = ℓ} a b imeq = ⟪ a ⟫-represents ∙∙ settab ∙∙ sym ⟪ b ⟫-represents where
  abpth : Path (Embedding _ _) (⟪ a ⟫ , ⟪ a ⟫↪ , isEmb⟪ a ⟫↪) (⟪ b ⟫ , ⟪ b ⟫↪ , isEmb⟪ b ⟫↪)
  abpth = equivFun (EmbeddingIP _ _)
    ( (λ p → equivFun (repFiber≃fiber ⟪ b ⟫↪ p) ∘ imeq .fst p ∘ invEq (repFiber≃fiber ⟪ a ⟫↪ p))
    , (λ p → equivFun (repFiber≃fiber ⟪ a ⟫↪ p) ∘ imeq .snd p ∘ invEq (repFiber≃fiber ⟪ b ⟫↪ p))
    )
  settab : sett ⟪ a ⟫ ⟪ a ⟫↪ ≡ sett ⟪ b ⟫ ⟪ b ⟫↪
  settab i = sett (abpth i .fst) (abpth i .snd .fst)

extInverse : ⟨ ∀[ a ∶ V ℓ ] ∀[ b ] (a ≡ₕ b) ⇒ (a ⊆ b) ⊓ (b ⊆ a) ⟩
extInverse a b a≡b = subst (λ b → ⟨ (a ⊆ b) ⊓ (b ⊆ a) ⟩) a≡b (⊆-refl a , ⊆-refl a)

set≡-characterization : {a b : V ℓ} → (a ≡ₕ b) ≡ (a ⊆ b) ⊓ (b ⊆ a)
set≡-characterization = ⇔toPath (extInverse _ _) (extensionality _ _)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module PiFrac.Properties where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Maybe
open import PiFrac.Syntax
open import PiFrac.Opsem
open import PiFrac.AuxLemmas
open import PiFrac.NoRepeat
open import PiFrac.Eval
open import PiFrac.Interp
open import PiFrac.Invariants

-- Forward evaluator is reversible
evalIsRev : ∀ {A B} → (c : A ↔ B) (v₁ : ⟦ A ⟧) (v₂ : ⟦ B ⟧)
          → eval c v₁ ≡ (just v₂) → evalᵣₑᵥ c v₂ ≡ (just v₁)
evalIsRev c v₁ v₂ eq with ev {κ = ☐} c v₁
evalIsRev c v₁ v₂ refl | inj₁ (v₂ , rs) with evᵣₑᵥ {κ = ☐} c v₂
... | inj₁ (v₁' , rs') with deterministicᵣₑᵥ* rs' (Rev↦ rs) (λ ()) (λ ()) (λ ())
... | refl = refl
evalIsRev c v₁ v₂ refl | inj₁ (v₂ , rs) | inj₂ (_ , v , _ , _ , neq , rs') with deterministicᵣₑᵥ* rs' (Rev↦ rs) (λ ()) (Lemma₆ neq) (λ ())
... | ()

-- Backward evaluator is reversible
evalᵣₑᵥIsRev : ∀ {A B} → (c : A ↔ B) (v₁ : ⟦ B ⟧) (v₂ : ⟦ A ⟧)
             → evalᵣₑᵥ c v₁ ≡ (just v₂) → eval c v₂ ≡ (just v₁)
evalᵣₑᵥIsRev c v₁ v₂ eq with evᵣₑᵥ {κ = ☐} c v₁
evalᵣₑᵥIsRev c v₁ v₂ refl | inj₁ (v₂ , rs) with ev {κ = ☐} c v₂
... | inj₁ (_ , rs') with deterministic* rs' (Rev↦ᵣₑᵥ rs) (λ ()) (λ ())
... | refl = refl
evalᵣₑᵥIsRev c v₁ v₂ refl | inj₁ (v₂ , rs) | inj₂ rs' with deterministic* rs' (Rev↦ᵣₑᵥ rs) (λ ()) (λ ())
... | ()

-- The abstract machine semantics is equivalent to the big-step semantics
eval≡interp : ∀ {A B} → (c : A ↔ B) → (v : ⟦ A ⟧) → eval c v ≡ interp c v
eval≡interp uniti₊l v = refl
eval≡interp unite₊l (inj₂ v) = refl
eval≡interp swap₊ (inj₁ x) = refl
eval≡interp swap₊ (inj₂ y) = refl
eval≡interp assocl₊ (inj₁ x) = refl
eval≡interp assocl₊ (inj₂ (inj₁ y)) = refl
eval≡interp assocl₊ (inj₂ (inj₂ z)) = refl
eval≡interp assocr₊ (inj₁ (inj₁ x)) = refl
eval≡interp assocr₊ (inj₁ (inj₂ y)) = refl
eval≡interp assocr₊ (inj₂ z) = refl
eval≡interp unite⋆l (tt , v) = refl
eval≡interp uniti⋆l v = refl
eval≡interp swap⋆ (x , y) = refl
eval≡interp assocl⋆ (x , (y , z)) = refl
eval≡interp assocr⋆ ((x , y) , z) = refl
eval≡interp dist (inj₁ x , z) = refl
eval≡interp dist (inj₂ y , z) = refl
eval≡interp factor (inj₁ (x , z)) = refl
eval≡interp factor (inj₂ (y , z)) = refl
eval≡interp id↔ v = refl
eval≡interp (c₁ ⨾ c₂) v with ev {κ = ☐} c₁ v | inspect (ev {κ = ☐} c₁) v
eval≡interp (c₁ ⨾ c₂) v | inj₁ (v' , rs) | [ eq ] with ev {κ = ☐} c₂ v' | inspect (ev {κ = ☐} c₂) v'
eval≡interp (c₁ ⨾ c₂) v | inj₁ (v' , rs) | [ eq ] | inj₁ (v'' , rs') | [ eq' ] with ev {κ = ☐} (c₁ ⨾ c₂) v | inspect (ev {κ = ☐} (c₁ ⨾ c₂)) v
eval≡interp (c₁ ⨾ c₂) v | inj₁ (v' , rs) | [ eq ] | inj₁ (v'' , rs') | [ eq' ] | inj₁ (u , rs'') | [ eq'' ] rewrite (sym (eval≡interp c₁ v)) | eq | (sym (eval≡interp c₂ v')) | eq' with deterministic* ((↦₃ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (☐⨾ c₂ • ☐) ++↦ (↦₇ ∷ ◾) ++↦ appendκ↦* rs' (λ ()) (λ ()) refl (c₁ ⨾☐• ☐) ++↦ (↦₁₀ ∷ ◾)) rs'' (λ ()) (λ ())
... | refl = refl
eval≡interp (c₁ ⨾ c₂) v | inj₁ (v' , rs) | [ eq ] | inj₁ (v'' , rs') | [ eq' ] | inj₂ rs'' | [ eq'' ] rewrite (sym (eval≡interp c₁ v)) | eq | (sym (eval≡interp c₂ v')) | eq' with deterministic* ((↦₃ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (☐⨾ c₂ • ☐) ++↦ (↦₇ ∷ ◾) ++↦ appendκ↦* rs' (λ ()) (λ ()) refl (c₁ ⨾☐• ☐) ++↦ (↦₁₀ ∷ ◾)) rs'' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⨾ c₂) v | inj₁ (v' , rs) | [ eq ] | inj₂ rs' | [ eq' ] with ev {κ = ☐} (c₁ ⨾ c₂) v | inspect (ev {κ = ☐} (c₁ ⨾ c₂)) v
eval≡interp (c₁ ⨾ c₂) v | inj₁ (v' , rs) | [ eq ] | inj₂ rs' | [ eq' ] | inj₁ (u , rs'') | [ eq'' ] rewrite (sym (eval≡interp c₁ v)) | eq | (sym (eval≡interp c₂ v')) | eq' with deterministic* ((↦₃ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (☐⨾ c₂ • ☐) ++↦ (↦₇ ∷ ◾) ++↦ appendκ↦*⊠ rs' (λ ()) (c₁ ⨾☐• ☐)) rs'' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⨾ c₂) v | inj₁ (v' , rs) | [ eq ] | inj₂ rs' | [ eq' ] | inj₂ rs'' | [ eq'' ] rewrite (sym (eval≡interp c₁ v)) | eq | (sym (eval≡interp c₂ v')) | eq' = refl
eval≡interp (c₁ ⨾ c₂) v | inj₂ rs | [ eq ] with ev {κ = ☐} (c₁ ⨾ c₂) v | inspect (ev {κ = ☐} (c₁ ⨾ c₂)) v
eval≡interp (c₁ ⨾ c₂) v | inj₂ rs | [ eq ] | inj₁ (v'' , rs') | [ eq' ] with deterministic* ((↦₃ ∷ ◾) ++↦ appendκ↦*⊠ rs (λ ()) (☐⨾ c₂ • ☐)) rs' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⨾ c₂) v | inj₂ rs | [ eq ] | inj₂ rs' | [ eq' ] rewrite (sym (eval≡interp c₁ v)) | eq = refl
eval≡interp (c₁ ⊕ c₂) (inj₁ x) with ev {κ = ☐} c₁ x | inspect (ev {κ = ☐} c₁) x
eval≡interp (c₁ ⊕ c₂) (inj₁ x) | inj₁ (x' , rs) | [ eq ] with ev {κ = ☐} (c₁ ⊕ c₂) (inj₁ x) | inspect (ev {κ = ☐} (c₁ ⊕ c₂)) (inj₁ x)
eval≡interp (c₁ ⊕ c₂) (inj₁ x) | inj₁ (x' , rs) | [ eq ] | inj₁ (x'' , rs') | [ eq' ] rewrite (sym (eval≡interp c₁ x)) | eq with deterministic* ((↦₄ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (☐⊕ c₂ • ☐) ++↦ (↦₁₁ ∷ ◾)) rs' (λ ()) (λ ())
... | refl = refl
eval≡interp (c₁ ⊕ c₂) (inj₁ x) | inj₁ (x' , rs) | [ eq ] | inj₂ rs' | [ eq' ] rewrite (sym (eval≡interp c₁ x)) | eq with deterministic* ((↦₄ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (☐⊕ c₂ • ☐) ++↦ (↦₁₁ ∷ ◾)) rs' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⊕ c₂) (inj₁ x) | inj₂ rs | [ eq ] with ev {κ = ☐} (c₁ ⊕ c₂) (inj₁ x) | inspect (ev {κ = ☐} (c₁ ⊕ c₂)) (inj₁ x)
eval≡interp (c₁ ⊕ c₂) (inj₁ x) | inj₂ rs | [ eq ] | inj₁ (x'' , rs') | [ eq' ] rewrite (sym (eval≡interp c₁ x)) | eq with deterministic* ((↦₄ ∷ ◾) ++↦ appendκ↦*⊠ rs (λ ()) (☐⊕ c₂ • ☐)) rs' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⊕ c₂) (inj₁ x) | inj₂ rs | [ eq ] | inj₂ rs' | [ eq' ] rewrite (sym (eval≡interp c₁ x)) | eq = refl
eval≡interp (c₁ ⊕ c₂) (inj₂ y) with ev {κ = ☐} c₂ y | inspect (ev {κ = ☐} c₂) y
eval≡interp (c₁ ⊕ c₂) (inj₂ y) | inj₁ (y' , rs) | [ eq ] with ev {κ = ☐} (c₁ ⊕ c₂) (inj₂ y) | inspect (ev {κ = ☐} (c₁ ⊕ c₂)) (inj₂ y)
eval≡interp (c₁ ⊕ c₂) (inj₂ y) | inj₁ (y' , rs) | [ eq ] | inj₁ (y'' , rs') | [ eq' ] rewrite (sym (eval≡interp c₂ y)) | eq with deterministic* ((↦₅ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (c₁ ⊕☐• ☐) ++↦ (↦₁₂ ∷ ◾)) rs' (λ ()) (λ ())
... | refl = refl
eval≡interp (c₁ ⊕ c₂) (inj₂ y) | inj₁ (y' , rs) | [ eq ] | inj₂ rs'         | [ eq' ] rewrite (sym (eval≡interp c₂ y)) | eq with deterministic* ((↦₅ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (c₁ ⊕☐• ☐) ++↦ (↦₁₂ ∷ ◾)) rs' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⊕ c₂) (inj₂ y) | inj₂ rs        | [ eq ] with ev {κ = ☐} (c₁ ⊕ c₂) (inj₂ y) | inspect (ev {κ = ☐} (c₁ ⊕ c₂)) (inj₂ y)
eval≡interp (c₁ ⊕ c₂) (inj₂ y) | inj₂ rs        | [ eq ] | inj₁ (y'' , rs') | [ eq' ] rewrite (sym (eval≡interp c₂ y)) | eq with deterministic* ((↦₅ ∷ ◾) ++↦ appendκ↦*⊠ rs (λ ()) (c₁ ⊕☐• ☐)) rs' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⊕ c₂) (inj₂ y) | inj₂ rs        | [ eq ] | inj₂ rs'         | [ eq' ] rewrite (sym (eval≡interp c₂ y)) | eq = refl
eval≡interp (c₁ ⊗ c₂) (x , y) with ev {κ = ☐} c₁ x | inspect (ev {κ = ☐} c₁) x
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₁ (x' , rs) | [ eq ] with ev {κ = ☐} c₂ y | inspect (ev {κ = ☐} c₂) y
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₁ (x' , rs) | [ eq ] | inj₁ (y' , rs') | [ eq' ] with ev {κ = ☐} (c₁ ⊗ c₂) (x , y) | inspect (ev {κ = ☐} (c₁ ⊗ c₂)) (x , y)
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₁ (x' , rs) | [ eq ] | inj₁ (y' , rs') | [ eq' ] | inj₁ (_ , rs'') | [ eq'' ] rewrite (sym (eval≡interp c₁ x)) | eq | (sym (eval≡interp c₂ y)) | eq' with deterministic* (((↦₆ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (☐⊗[ c₂ , y ]• ☐)) ++↦ (↦₈ ∷ ◾) ++↦ appendκ↦* rs' (λ ()) (λ ()) refl ([ c₁ , x' ]⊗☐• ☐) ++↦ (↦₉ ∷ ◾)) rs'' (λ ()) (λ ())
... | refl = refl
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₁ (x' , rs) | [ eq ] | inj₁ (y' , rs') | [ eq' ] | inj₂ rs''       | [ eq'' ] rewrite (sym (eval≡interp c₁ x)) | eq | (sym (eval≡interp c₂ y)) | eq' with deterministic* (((↦₆ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (☐⊗[ c₂ , y ]• ☐)) ++↦ (↦₈ ∷ ◾) ++↦ appendκ↦* rs' (λ ()) (λ ()) refl ([ c₁ , x' ]⊗☐• ☐) ++↦ (↦₉ ∷ ◾)) rs'' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₁ (x' , rs) | [ eq ] | inj₂ rs'        | [ eq' ] with ev {κ = ☐} (c₁ ⊗ c₂) (x , y) | inspect (ev {κ = ☐} (c₁ ⊗ c₂)) (x , y)
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₁ (x' , rs) | [ eq ] | inj₂ rs'        | [ eq' ] | inj₁ (y' , rs'') | [ eq'' ] rewrite (sym (eval≡interp c₁ x)) | eq | (sym (eval≡interp c₂ y)) | eq' with deterministic* (((↦₆ ∷ ◾) ++↦ appendκ↦* rs (λ ()) (λ ()) refl (☐⊗[ c₂ , y ]• ☐)) ++↦ (↦₈ ∷ ◾) ++↦ appendκ↦*⊠ rs' (λ ()) ([ c₁ , x' ]⊗☐• ☐)) rs'' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₁ (x' , rs) | [ eq ] | inj₂ rs'        | [ eq' ] | inj₂ rs''        | [ eq'' ] rewrite (sym (eval≡interp c₁ x)) | eq | (sym (eval≡interp c₂ y)) | eq' = refl
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₂ rs        | [ eq ] with ev {κ = ☐} (c₁ ⊗ c₂) (x , y) | inspect (ev {κ = ☐} (c₁ ⊗ c₂)) (x , y)
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₂ rs        | [ eq ] | inj₁ (_ , rs') | [ eq' ] rewrite (sym (eval≡interp c₁ x)) | eq with deterministic* ((↦₆ ∷ ◾) ++↦ appendκ↦*⊠ rs (λ ()) (☐⊗[ c₂ , y ]• ☐)) rs' (λ ()) (λ ())
... | ()
eval≡interp (c₁ ⊗ c₂) (x , y) | inj₂ rs        | [ eq ] | inj₂ rs''      | [ eq' ] rewrite (sym (eval≡interp c₁ x)) | eq = refl
eval≡interp (ηₓ v) tt = refl
eval≡interp (εₓ v) (v' , ↻) with v ≟ v'
... | yes refl = refl
... | no  _    = refl

-- !c is the inverse computation of c
interp! : ∀ {A B} (c : A ↔ B) (a : ⟦ A ⟧) (b : ⟦ B ⟧) → interp c a ≡ just b → interp (! c) b ≡ just a
interp! unite₊l (inj₂ y) .y refl = refl
interp! uniti₊l y .(inj₂ y) refl = refl
interp! swap₊ (inj₁ x) .(inj₂ x) refl = refl
interp! swap₊ (inj₂ y) .(inj₁ y) refl = refl
interp! assocl₊ (inj₁ x) .(inj₁ (inj₁ x)) refl = refl
interp! assocl₊ (inj₂ (inj₁ y)) .(inj₁ (inj₂ y)) refl = refl
interp! assocl₊ (inj₂ (inj₂ z)) .(inj₂ z) refl = refl
interp! assocr₊ (inj₁ (inj₁ x)) .(inj₁ x) refl = refl
interp! assocr₊ (inj₁ (inj₂ y)) .(inj₂ (inj₁ y)) refl = refl
interp! assocr₊ (inj₂ z) .(inj₂ (inj₂ z)) refl = refl
interp! unite⋆l (tt , v) .v refl = refl
interp! uniti⋆l v .(tt , v) refl = refl
interp! swap⋆ (x , y) .(y , x) refl = refl
interp! assocl⋆ (x , y , z) .((x , y) , z) refl = refl
interp! assocr⋆ ((x , y) , z) .(x , y , z) refl = refl
interp! dist (inj₁ x , z) .(inj₁ (x , z)) refl = refl
interp! dist (inj₂ y , z) .(inj₂ (y , z)) refl = refl
interp! factor (inj₁ (x , z)) .(inj₁ x , z) refl = refl
interp! factor (inj₂ (y , z)) .(inj₂ y , z) refl = refl
interp! id↔ v .v refl = refl
interp! (c₁ ⨾ c₂) a c eq with interp c₁ a | inspect (interp c₁) a
... | just b  | [ eq₁ ] with interp c₂ b | inspect (interp c₂) b
... | just c' | [ eq₂ ] with eq
... | refl rewrite interp! c₂ b c eq₂ | interp! c₁ a b eq₁ = refl
interp! (c₁ ⊕ c₂) (inj₁ x) b eq with interp c₁ x | inspect (interp c₁) x
... | just x' | [ eqx ] with b
... | inj₁ _ with eq
... | refl rewrite interp! c₁ x x' eqx = refl
interp! (c₁ ⊕ c₂) (inj₂ y) b eq with interp c₂ y | inspect (interp c₂) y
... | just y' | [ eqy ] with b
... | inj₂ _ with eq
... | refl rewrite interp! c₂ y y' eqy = refl
interp! (c₁ ⊗ c₂) (x , y) (x' , y') eq with interp c₁ x | inspect (interp c₁) x | interp c₂ y | inspect (interp c₂) y
... | just x'' | [ eqx ] | just y'' | [ eqy ] with eq
... | refl rewrite interp! c₁ x x' eqx | interp! c₂ y y' eqy = refl
interp! (ηₓ v) tt .(v , ↻) refl with v ≟ v
... | yes refl = refl
... | no  neq  = ⊥-elim (neq refl)
interp! (εₓ v) (v' , ↻) b eq with v ≟ v'
... | yes refl = refl
interp! (εₓ _) (v' , ↻) b () | no neq


text:
{-# OPTIONS --no-irrelevant-projections #-}
module ScopeIrrelevantRecordField where

record Bla : Set1 where
  constructor mkBla
  field
    .bla0 bla1 .{bla2 bla3} {bla4 .bla5} : Set

bla0' : Bla -> Set
bla0' = Bla.bla0  -- should fail with bla0 not in scope

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import FRP.JS.Behaviour using ( Beh ; [_] ; map )
open import FRP.JS.Event using ( Evt ; tag )
open import FRP.JS.DOM using
  ( DOM ; click ; element ; text ; _++_ ; element+ ; text+ ; listen+ ; _+++_ )
open import FRP.JS.RSet using ( RSet ; ⟦_⟧ ; ⟨_⟩ ; _⇒_ )
open import FRP.JS.Product using ( _∧_ ; _,_ )
open import FRP.JS.Demo.Calculator.Model using
  ( Button ; State ; digit ; op ; clear ; eq ; plus ; minus ; times ; button$ ; state$ ; model )

module FRP.JS.Demo.Calculator.View where

button : ∀ {w} → Button → ⟦ Beh (DOM w) ∧ Evt ⟨ Button ⟩ ⟧
button b = listen+ click (λ _ → b) (element+ "button" (text+ [ button$ b ]))

keypad : ∀ {w} → ⟦ Beh (DOM w) ∧ Evt ⟨ Button ⟩ ⟧
keypad =
  element+ "div" (button (digit 7) +++ button (digit 8)  +++ button (digit 9) ) +++
  element+ "div" (button (digit 4) +++ button (digit 5)  +++ button (digit 6) ) +++
  element+ "div" (button (digit 1) +++ button (digit 2)  +++ button (digit 3) ) +++
  element+ "div" (button (op eq)   +++ button (digit 0)  +++ button clear     ) +++
  element+ "div" (button (op plus) +++ button (op minus) +++ button (op times))

display : ∀ {w} → ⟦ Beh ⟨ State ⟩ ⇒ Beh (DOM w) ⟧
display σ = element "div" (text (map state$ σ))

view : ∀ {w} → ⟦ Beh (DOM w) ⟧
view with keypad
... | (dom , evt) = display (model evt) ++ dom

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

----------------------------------------------------------------------
-- Gaps
----------------------------------------------------------------------
-- Polynomials can be represented as lists of their coefficients,
-- stored in increasing powers of x:
--
--   3 + 2x² + 4x⁵ + 2x⁷
-- ≡⟨ making the missing xs explicit ⟩
--   3x⁰ + 0x¹ + 2x² + 0x³ + 0x⁴ + 4x⁵ + 0x⁶ + 2x⁷
-- ≡⟨ in list notation ⟩
--   [3,0,2,0,0,4,0,2]
--
-- This approach is wasteful with space. Instead, we will pair each
-- coefficient with the size of the preceding gap, meaning that the
-- above expression is instead written as:
--
--   [(3,0),(2,1),(4,2),(2,1)]
--
-- Which can be thought of as a representation of the expression:
--
--   x⁰ * (3 + x * x¹ * (2 + x * x² * (4 + x * x¹ * (2 + x * 0))))
--
-- To add multiple variables to a polynomial, you can *nest* them,
-- making the coefficients of the outer polynomial polynomials
-- themselves. However, this is *also* wasteful, in a similar way to
-- above: the constant polynomial, for instance, will be represented
-- as many nestings of constant polynomials around a final variable.
-- However, this approach presents a difficulty: the polynomial will
-- have the kind ℕ → Set (...). In other words, it's indexed by the
-- number of variables it contains. The gap we store, then, has to
-- be accomanied with some information about how it relates to that
-- index.
--
-- The first approach I tried was to forget about storing the gaps,
-- and instead store the number of variables in the nested coefficient,
-- along with a proof that the number was smaller than the outer. The
-- proof was _≤_ from Data.Nat:
--
-- data _≤_ : Rel ℕ 0ℓ where
--   z≤n : ∀ {n}                 → zero  ≤ n
--   s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
--
-- While this worked, this will actually give you a worse complexity
-- than the naive encoding without gaps.
--
-- For any of the binary operations, you need to be able to "line up"
-- the two arguments in terms of the gaps. For addition, for instance,
-- the argument with fewer variables should be added to the constant
-- term of the argument with more. To do this, you need to compare the
-- gaps.
--
-- To see why that's a problem, consider the following sequence of
-- nestings:
--
--   (5 ≤ 6), (4 ≤ 5), (3 ≤ 4), (1 ≤ 3), (0 ≤ 1)
--
-- The outer polynomial has 6 variables, but it has a gap to its inner
-- polynomial of 5, and so on. What we compare in this case is the
-- number of variables in the tail: like repeatedly taking the length of
-- the tail of a list, it's quadratic.
--
-- The second approach was to try and mimic the powers structure
-- (which only compared the gaps, which is linear), and store the gaps
-- in a proof like the following:
--
-- record _≤″_ (m n : ℕ) : Set where
--   constructor less-than-or-equal
--   field
--     {k}   : ℕ
--     proof : m + k ≡ n
--
-- Here, k is the size of the gap. The problem of this approach was
-- twofold: it was difficult to show that comparisons on the k
-- corresponded to comparisons on the m, and working with ≡ instead of
-- some inductive structure was messy. However, it had the advantage
-- of being erasable: both proofs of the correspondence and the
-- equality proof itself. That said, I'm not very familiar with the
-- soundness of erasure, and in particular how it interacts with axiom
-- K (which I'd managed to avoid up until this point, but started to
-- creep in).
--
-- I may have had more luck if I swapped the arguments too +:
--
-- record _≤″_ (m n : ℕ) : Set where
--   constructor less-than-or-equal
--   field
--     {k}   : ℕ
--     proof : k + m ≡ n
--
-- But I did not try it. The solution I ended up with was superior,
-- regardless:
--
-- infix 4 _≤_
-- data _≤_ (m : ℕ) : ℕ → Set where
--   m≤m : m ≤ m
--   ≤-s : ∀ {n} → (m≤n : m ≤ n) → m ≤ suc n
--
-- (This is a rewritten version of _≤′_ from Data.Nat.Base).
--
-- While this structure stores the same information as ≤, it does so
-- by induction on the *gap*. This became apparent when I realised you
-- could use it to write a comparison function which was linear in the
-- size of the gap (even though it was comparing the length of the
-- tail):

-- data Ordering : ℕ → ℕ → Set where
--   less    : ∀ {n m} → n ≤ m → Ordering n (suc m)
--   greater : ∀ {n m} → m ≤ n → Ordering (suc n) m
--   equal   : ∀ {n}           → Ordering n n

-- ≤-compare : ∀ {i j n}
--           → (i≤n : i ≤ n)
--           → (j≤n : j ≤ n)
--           → Ordering i j
-- ≤-compare m≤m m≤m = equal
-- ≤-compare m≤m (≤-s m≤n) = greater m≤n
-- ≤-compare (≤-s m≤n) m≤m = less m≤n
-- ≤-compare (≤-s i≤n) (≤-s j≤n) = ≤-compare i≤n j≤n
--
-- A few things to note here:
--
-- 1. The ≤-compare function is one of those reassuring ones for which
--    Agda can completely fill in the type for me.
-- 2. This function looks somewhat similar to the one for comparing ℕ
--    in Data.Nat, and as a result, the "matching" logic for degree
--    and number of variables began too look similar.
--
-- While this approach allowed me too write all the functions I
-- needed, I hit another roadblock when it came time to prove the
-- ring homomorphism. The first thing I realised I needed to prove was
-- basically the following:
--
--   ∀ {i j n}
--   → (i≤n : i ≤ n)
--   → (j≤n : j ≤ n)
--   → ∀ xs Ρ
--   → Σ⟦ xs ⟧ (drop-1 i≤n Ρ) ≈ Σ⟦ xs ⟧ (drop-1 j≤n Ρ)
--
-- In effect, if the inequalities are over the same numbers, then
-- they'll behave the same way when used in evaluation.
--
-- The above is really just a consequence of ≤ being irrelevant:
--
--   ∀ {i n}
--   → (x : i ≤ n)
--   → (y : i ≤ n)
--   → x ≡ y
--
-- Trying to prove this convinced me that it might not even be possible
-- without K. On top of that, I also noticed that I would need to
-- prove things like:
--
--   ∀ {i j n}
--   → (i≤j : i ≤ j)
--   → (j≤n : j ≤ n)
--   → (x : FlatPoly i)
--   → (Ρ : Vec Carrier n)
--   → ⟦ x Π (i≤j ⟨ ≤′-trans ⟩ j≤n) ⟧ Ρ ≈ ⟦ x Π i≤j ⟧ (drop j≤n Ρ)
--
-- Effectively, I needed to prove that transitivity was a
-- homomorphism.
--
-- I realised that I had not run into these difficulties with the
-- comparison function I was using for the exponent gaps: why? Well
-- that function provides a proof about its *arguments* whereas the
-- one I wrote above only provides a proof about the i and j.
--
-- data Ordering : Rel ℕ 0ℓ where
--   less    : ∀ m k → Ordering m (suc (m + k))
--   equal   : ∀ m   → Ordering m m
--   greater : ∀ m k → Ordering (suc (m + k)) m
--
-- If I tried to mimick the above as closely as possible, I would also
-- need an analogue to +: of course this was ≤′-trans, so I was going
-- to get my transitivity proof as well as everything else. The result
-- is as follows.

module Polynomial.NormalForm.InjectionIndex where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Nat using (_≤′_; ≤′-refl; ≤′-step; _<′_) public
open import Data.Nat.Properties using (≤′-trans) public
open import Function

data InjectionOrdering {n : ℕ} : ∀ {i j}
                      → (i≤n : i ≤′ n)
                      → (j≤n : j ≤′ n)
                      → Set
                      where
  inj-lt : ∀ {i j-1}
     → (i≤j-1 : i ≤′ j-1)
     → (j≤n : suc j-1 ≤′ n)
     → InjectionOrdering (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) j≤n
  inj-gt : ∀ {i-1 j}
     → (i≤n : suc i-1 ≤′ n)
     → (j≤i-1 : j ≤′ i-1)
     → InjectionOrdering i≤n (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n)
  inj-eq : ∀ {i} → (i≤n : i ≤′ n) → InjectionOrdering i≤n i≤n

inj-compare : ∀ {i j n}
    → (x : i ≤′ n)
    → (y : j ≤′ n)
    → InjectionOrdering x y
inj-compare ≤′-refl ≤′-refl = inj-eq ≤′-refl
inj-compare ≤′-refl (≤′-step y) = inj-gt ≤′-refl y
inj-compare (≤′-step x) ≤′-refl = inj-lt x ≤′-refl
inj-compare (≤′-step x) (≤′-step y) = case inj-compare x y of
    λ { (inj-lt i≤j-1 .y) → inj-lt i≤j-1 (≤′-step y)
      ; (inj-gt .x j≤i-1) → inj-gt (≤′-step x) j≤i-1
      ; (inj-eq .x) → inj-eq (≤′-step x)
      }

open import Data.Fin as Fin using (Fin)

space : ∀ {n} → Fin n → ℕ
space f = suc (go f)
  where
  go : ∀ {n} → Fin n → ℕ
  go {suc n} Fin.zero = n
  go (Fin.suc x) = go x

Fin⇒≤ : ∀ {n} (x : Fin n) → space x ≤′ n
Fin⇒≤ Fin.zero = ≤′-refl
Fin⇒≤ (Fin.suc x) = ≤′-step (Fin⇒≤ x)

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
open import cedille-types
import spans
open import ctxt
import cedille-options
open import general-util

module type-inf
  (options : cedille-options.options)
  {mF : Set → Set}
  ⦃ _ : monad mF ⦄
  (check-term : ctxt → ex-tm → (T? : maybe type) →
                spans.spanM options {mF} (spans.check-ret options {mF} T? term))
  (check-type : ctxt → ex-tp → (k? : maybe kind) →
                spans.spanM options {mF} (spans.check-ret options {mF} k? type))
  where

open import spans options {mF}
open import rename
open import syntax-util
open import type-util
open import meta-vars options {mF}
open import resugar
open import subst
open import conversion
open import free-vars
open import constants

record spine-data : Set where
  constructor mk-spine-data
  field
    spine-mvars : meta-vars
    spine-type : decortype
    spine-locale : ℕ
    spine-elab : meta-vars → term

check-term-spine-elim : ctxt → spine-data → term × type
check-term-spine-elim Γ (mk-spine-data Xs dt locl f~) =
  f~ Xs , meta-vars-subst-type' ff Γ Xs (decortype-to-type dt)
--  elim-pair (maybe-else' (meta-vars-to-args Xs) ([] , Hole pi-gen) f~) recompose-apps ,
--  meta-vars-subst-type' ff Γ Xs (decortype-to-type dt)

check-term-spine : ctxt → ex-tm → (m : prototype) → 𝔹 → spanM (maybe spine-data)

check-term-spine-return : meta-vars → decortype → ℕ → (meta-vars → term) → spanM (maybe spine-data)
check-term-spine-return Xs dt locl f~ = return (just (mk-spine-data Xs dt locl f~))

-- a flag indicating how aggresively we should be unfolding during matching.
-- "both" is the backtracking flag. We will attempt "both" matches, which means
-- first matching without unfolding, then if that fails unfolding the type once
-- and continue matching the subexpresions with "both"
data match-unfolding-state : Set where
  match-unfolding-both match-unfolding-approx match-unfolding-hnf : match-unfolding-state

-- main matching definitions
-- --------------------------------------------------

-- NOTE: these functions don't actually ever emit spans
match-types : ctxt → meta-vars → local-vars → match-unfolding-state → (tpₓ tp : type) → spanM $ match-error-t meta-vars
match-kinds : ctxt → meta-vars → local-vars → match-unfolding-state → (kₓ k : kind) → spanM $ match-error-t meta-vars
match-tpkds : ctxt → meta-vars → local-vars → match-unfolding-state → (tkₓ tk : tpkd) → spanM $ match-error-t meta-vars

record match-prototype-data : Set where
  constructor mk-match-prototype-data
  field
    match-proto-mvars : meta-vars
    match-proto-dectp : decortype
    match-proto-error : 𝔹
open match-prototype-data
match-prototype : ctxt → (Xs : meta-vars) (is-hnf : 𝔹) (tp : type) (pt : prototype) → spanM match-prototype-data

-- substitutions used during matching
-- --------------------------------------------------

-- These have to be in the spanM monad because substitution can unlock a `stuck`
-- decoration, causing another round of prototype matching (which invokes type matching)

substh-decortype : ctxt → renamectxt → trie (Σi exprd ⟦_⟧) → decortype → spanM decortype
substh-decortype Γ ρ σ (decor-type tp) = return $ decor-type (substh Γ ρ σ tp)
substh-decortype Γ ρ σ (decor-arrow e? dom cod) =
  substh-decortype Γ ρ σ cod
  >>= λ cod → return $ decor-arrow e? (substh Γ ρ σ dom) cod
substh-decortype Γ ρ σ (decor-decor e? x tk sol dt) =
  let x' = subst-rename-var-if Γ ρ x σ (decortype-to-type dt)
      Γ' = ctxt-var-decl x' Γ
      ρ' = renamectxt-insert ρ x x'
  in substh-decortype Γ' ρ' σ dt
  >>= λ dt' → return $ decor-decor e? x' (substh Γ ρ σ -tk tk) (substh-meta-var-sort Γ ρ σ sol) dt'
substh-decortype Γ ρ σ (decor-stuck tp pt) =
  match-prototype Γ meta-vars-empty ff (substh Γ ρ σ tp) pt
  -- NOTE: its an invariant that if you start with no meta-variables,
  -- prototype matching produces no meta-variables as output
  >>= λ ret → return (match-proto-dectp ret)

substh-decortype Γ ρ σ (decor-error tp pt) =
  return $ decor-error (substh Γ ρ σ tp) pt

subst-decortype : {ed : exprd} → ctxt → ⟦ ed ⟧ → var → decortype → spanM decortype
subst-decortype Γ s x dt = substh-decortype Γ empty-renamectxt (trie-single x (, s)) dt

meta-vars-subst-decortype' : (unfold : 𝔹) → ctxt → meta-vars → decortype → spanM decortype
meta-vars-subst-decortype' uf Γ Xs dt =
  substh-decortype Γ empty-renamectxt (meta-vars-get-sub Xs) dt
  >>= λ dt' → return $
    if uf then hnf-decortype Γ unfold-head-elab dt' tt else dt'

meta-vars-subst-decortype : ctxt → meta-vars → decortype → spanM decortype
meta-vars-subst-decortype = meta-vars-subst-decortype' tt

-- unfolding a decorated type to reveal a term / type abstraction
-- --------------------------------------------------

{-# TERMINATING #-}
meta-vars-peel' : ctxt → span-location → meta-vars → decortype → spanM (𝕃 meta-var × decortype)
meta-vars-peel' Γ sl Xs (decor-decor e? x _ (meta-var-tp k mtp) dt) =
  let Y   = meta-var-fresh-tp Xs x sl (k , mtp)
      Xs' = meta-vars-add Xs Y
  in subst-decortype Γ (meta-var-to-type-unsafe Y) x dt
  >>= λ dt' → meta-vars-peel' Γ sl Xs' dt'
  >>= λ ret → let Ys = fst ret ; rdt = snd ret
  in return $ Y :: Ys , rdt
meta-vars-peel' Γ sl Xs dt@(decor-decor e? x _ (meta-var-tm _ _) _) = return $ [] , dt
meta-vars-peel' Γ sl Xs dt@(decor-arrow _ _ _) = return $ [] , dt
-- NOTE: vv The clause below will later generate a type error vv
meta-vars-peel' Γ sl Xs dt@(decor-stuck _ _) = return $ [] , dt
-- NOTE: vv The clause below is an internal error, if reached vv
meta-vars-peel' Γ sl Xs dt@(decor-type _) = return $ [] , dt
meta-vars-peel' Γ sl Xs dt@(decor-error _ _) = return $ [] , dt

meta-vars-unfold-tmapp' : ctxt → span-location → meta-vars → decortype → spanM (𝕃 meta-var × is-tmabsd?)
meta-vars-unfold-tmapp' Γ sl Xs dt =
  meta-vars-subst-decortype Γ Xs dt
  >>= λ dt' → meta-vars-peel' Γ sl Xs dt'
  >>= λ where
    (Ys , dt'@(decor-arrow e? dom cod)) →
      return $ Ys , yes-tmabsd dt' e? ignored-var dom ff cod
    (Ys , dt'@(decor-decor e? x _ (meta-var-tm dom _) cod)) →
      return $ Ys , yes-tmabsd dt' e? x dom (is-free-in x (decortype-to-type cod)) cod
    (Ys , dt@(decor-decor _ _ _ (meta-var-tp _ _) _)) →
      return $ Ys , not-tmabsd dt
-- NOTE: vv this is a type error vv
    (Ys , dt@(decor-stuck _ _)) →
      return $ Ys , not-tmabsd dt
-- NOTE: vv this is an internal error, if reached vv
    (Ys , dt@(decor-type _)) →
      return $ Ys , not-tmabsd dt
    (Ys , dt@(decor-error _ _)) →
      return $ Ys , not-tmabsd dt

meta-vars-unfold-tpapp' : ctxt → meta-vars → decortype → spanM is-tpabsd?
meta-vars-unfold-tpapp' Γ Xs dt =
  meta-vars-subst-decortype Γ Xs dt
  >>= λ where
   (dt″@(decor-decor e? x _ (meta-var-tp k mtp) dt')) →
    return $ yes-tpabsd dt″ e? x k (flip maybe-map mtp meta-var-sol.sol) dt'
   (dt″@(decor-decor _ _ _ (meta-var-tm _ _) _)) →
    return $ not-tpabsd dt″
   (dt″@(decor-arrow _ _ _)) → return $ not-tpabsd dt″
   (dt″@(decor-stuck _ _)) → return $ not-tpabsd dt″
   (dt″@(decor-type _)) → return $ not-tpabsd dt″
   (dt″@(decor-error _ _)) → return $ not-tpabsd dt″

-- errors
-- --------------------------------------------------

-- general type errors for applications
module check-term-app-tm-errors
  {A : Set} (t₁ t₂ : ex-tm) (htp : type) (Xs : meta-vars) (is-locale : 𝔹) (m : checking-mode) (Γ : ctxt)
  where

  inapplicable : erased? → decortype → prototype → spanM (maybe A)
  inapplicable e? dt pt =
    spanM-add
      (App-span is-locale (term-start-pos t₁) (term-end-pos t₂) m
        (head-type Γ (meta-vars-subst-type Γ Xs htp)
          -- :: decortype-data Γ dt
          -- :: prototype-data Γ pt
          :: meta-vars-data-all Γ Xs)
        (just $ "The type of the head does not allow the head to be applied to "
         ^ h e? ^ " argument"))
    >> return nothing
    where h : erased? → string
          h Erased = "an erased term"
          h NotErased = "a term"

  bad-erasure : erased? → spanM (maybe A)
  bad-erasure e? =
    spanM-add
      (App-span is-locale (term-start-pos t₁) (term-end-pos t₂) m
        (head-type Γ (meta-vars-subst-type Γ Xs htp) :: meta-vars-data-all Γ Xs)
        (just (msg e?)))
    >> return nothing
    where
    msg : erased? → string
    msg Erased =
      "The type computed for the head requires an explicit (non-erased) argument,"
      ^ " but the application is marked as erased"
    msg NotErased =
      "The type computed for the head requires an implicit (erased) argument,"
      ^ " but the application is marked as not erased"

  unmatchable : (tpₓ tp : type) (msg : string) → 𝕃 tagged-val → spanM (maybe A)
  unmatchable tpₓ tp msg tvs =
    spanM-add
      (App-span is-locale (term-start-pos t₁) (term-end-pos t₂) m
        (arg-exp-type Γ tpₓ :: arg-type Γ tp :: tvs ++ meta-vars-data-all Γ Xs)
        (just msg))
    >> return nothing

  unsolved-meta-vars : type → 𝕃 tagged-val → spanM (maybe A)
  unsolved-meta-vars tp tvs =
    spanM-add
      (App-span tt (term-start-pos t₁) (term-end-pos t₂) m
        (type-data Γ tp :: meta-vars-data-all Γ Xs ++ tvs)
        (just "There are unsolved meta-variables in this maximal application"))
    >> return nothing

module check-term-app-tp-errors
  {A : Set} (t : ex-tm) (tp : ex-tp) (htp : type) (Xs : meta-vars) (m : checking-mode) (Γ : ctxt)
  where

  inapplicable : decortype → spanM (maybe A)
  inapplicable dt =
    spanM-add
      (AppTp-span tt (term-start-pos t) (type-end-pos tp) synthesizing
        (head-type Γ (meta-vars-subst-type Γ Xs htp)
          -- :: decortype-data Γ dt
          :: meta-vars-data-all Γ Xs)
        (just "The type of the head does not allow the head to be applied to a type argument"))
    >> return nothing

  ctai-disagree : (ctai-sol : type) → spanM (maybe A)
  ctai-disagree ctai-sol =
    spanM-add (AppTp-span tt (term-start-pos t) (type-end-pos tp) m
      (head-type Γ (meta-vars-subst-type Γ Xs htp)
        :: contextual-type-argument Γ ctai-sol
        :: meta-vars-data-all Γ Xs)
      (just "The given and contextually inferred type argument differ"))
    >> return nothing

-- meta-variable locality
-- --------------------------------------------------

-- for debugging -- prepend to the tvs returned by check-spine-locality if you're having trouble
private
  locale-tag : ℕ → tagged-val
  locale-tag n = "locale n" , [[ ℕ-to-string n ]] , []

private
  is-locale : (max : 𝔹) → (locl : maybe ℕ) → 𝔹
  is-locale max locl = max || maybe-else' locl ff iszero

check-spine-locality : ctxt → meta-vars → type → (max : 𝔹) → (locl : ℕ)
                       → spanM (maybe (meta-vars × ℕ × 𝔹))
check-spine-locality Γ Xs tp max locl =
  let new-locl  = if iszero locl then num-arrows-in-type Γ tp else locl
      new-Xs    = if iszero locl then meta-vars-empty else Xs
      left-locl = is-locale max (just locl)
  in if left-locl && (~ meta-vars-solved? Xs)
        then return nothing
     else return (just (new-Xs , new-locl , left-locl))

-- main definition
--------------------------------------------------

data check-term-app-ret : Set where
  check-term-app-return : (t~ : term) (Xs : meta-vars) (cod : decortype) (arg-mode : checking-mode) → (tvs : 𝕃 tagged-val) → check-term-app-ret

check-term-app : ctxt → (Xs : meta-vars) (Ys : 𝕃 meta-var) → (t₁ t₂ : ex-tm) → is-tmabsd → 𝔹 → spanM (maybe check-term-app-ret)

check-term-spine Γ t'@(ExApp t₁ e? t₂) pt max =
  -- 1) type the applicand, extending the prototype
    let pt' = proto-arrow e? pt in
    check-term-spine Γ t₁ pt' ff
      on-fail handleApplicandTypeError
  -- 2) make sure the applicand type reveals an arrow (term abstraction)
  >>=m λ ret → let mk-spine-data Xs dt locl fₕ~ = ret in
    -- the meta-vars need to know the span they were introduced in
    let sloc = span-loc $ ctxt.fn Γ in
    -- see if the decorated type of the head `dt` reveals an arrow
    meta-vars-unfold-tmapp' Γ sloc Xs dt
  >>=c λ Ys tm-arrow? →
    return tm-arrow? on-fail (λ _ → genInapplicableError Xs dt pt' locl)
    -- if so, get the (plain, undecorated) type of the head `htp`
  >>=s λ arr → let htp = decortype-to-type ∘ is-tmabsd-dt $ arr in
  -- 3) make sure erasures of the applicand type + syntax of application match
    checkErasuresMatch e? (is-tmabsd-e? arr) htp Xs locl
  -- 4) type the application, filling in missing type arguments with meta-variables
  >>=m λ _ → check-term-app Γ Xs Ys t₁ t₂ arr (islocl locl)
  -- 5) check no unsolved mvars, if the application is maximal (or a locality)
  >>=m λ {(check-term-app-return t₂~ Xs' rtp' arg-mode tvs) →
    let rtp = decortype-to-type rtp' in
    checkLocality Γ Xs' htp rtp max (pred locl) tvs
  >>=m uncurry₂ λ Xs'' locl' is-loc →
  -- 6) generate span
    genAppSpan Γ Xs Xs' Ys pt rtp is-loc tvs
  >> check-term-spine-return Xs'' rtp' locl'
  -- 7) fill in solutions to meta-vars introduced here and return the rest
    λ sols →
      let sols = if max then Xs' else sols
--          num-sols-here = length Ys
--          sols-here = take num-sols-here sols
--          sols-rest = drop num-sols-here sols
--          as = maybe-else' (meta-vars-to-args (meta-vars-from-list sols-here)) [] id
--          tₕ~ = recompose-apps as tₕₓ~
          tₕ~ = foldl (λ X t → maybe-else' (meta-vars-lookup sols (meta-var.name X)) t
                         λ {(meta-var-mk X' (meta-var-tp k T?) _) →
                              maybe-else' T? t (AppTp t ∘ meta-var-sol.sol);
                            (meta-var-mk X' (meta-var-tm T t?) _) →
                              maybe-else' t? t (AppEr t ∘ meta-var-sol.sol)})
                      (fₕ~ sols) Ys
          app = if e? then AppEr else App in
      app tₕ~ t₂~
  }

  where
  mode = prototype-to-checking pt

  expected-type-if-pt : ctxt → prototype → 𝕃 tagged-val
  expected-type-if-pt Γ pt = case pt of λ where
    (proto-maybe mt) → maybe-else [] (λ tp → [ expected-type Γ tp ]) mt
    (proto-arrow _ _) → []

  span-loc : (fn : string) → span-location
  span-loc fn = fn , term-start-pos t₁ , term-end-pos t₂

  islocl : ℕ → 𝔹
  islocl locl = is-locale max (just $ pred locl)

  handleApplicandTypeError : spanM (maybe _)
  handleApplicandTypeError =
      spanM-add (App-span max (term-start-pos t₁) (term-end-pos t₂) mode (expected-type-if-pt Γ pt) nothing)
    >> check-term Γ t₂ nothing
    >>= (const $ return nothing)

  genInapplicableError : meta-vars → decortype → prototype → (locl : ℕ) → spanM (maybe _)
  genInapplicableError Xs dt pt locl =
    check-term-app-tm-errors.inapplicable
      t₁ t₂ (decortype-to-type dt) Xs (islocl locl) mode Γ e? dt (proto-arrow e? pt)

  checkErasuresMatch : (e?₁ e?₂ : erased?) → type → meta-vars → (locl : ℕ) → spanM (maybe ⊤)
  checkErasuresMatch e?₁ e?₂ htp Xs locl =
    if e?₁ xor e?₂
      then check-term-app-tm-errors.bad-erasure t₁ t₂ htp Xs (islocl locl) mode Γ e?₁
    else (return ∘ just $ triv)

  checkLocality : ctxt → meta-vars → (htp rtp : type) → (max : 𝔹) (locl : ℕ) → 𝕃 tagged-val → spanM ∘ maybe $ _
  checkLocality Γ Xs htp rtp max locl tvs =
    check-spine-locality Γ Xs rtp max locl
      on-fail check-term-app-tm-errors.unsolved-meta-vars
        t₁ t₂ htp Xs (islocl locl) mode Γ rtp tvs
    >>=m (return ∘ just)

  genAppSpan : ctxt → (Xs Xs' : meta-vars) → (Ys : 𝕃 meta-var) → prototype → type → (is-locl : 𝔹) → 𝕃 tagged-val → spanM ⊤
  genAppSpan Γ Xs Xs' Ys pt rtp is-loc tvs =
    spanM-add $ elim-pair
      (meta-vars-check-type-mismatch-if (prototype-to-maybe pt) Γ "synthesized" meta-vars-empty rtp)
      λ tvs' → App-span is-loc (term-start-pos t₁) (term-end-pos t₂) mode
        (tvs' ++ meta-vars-intro-data Γ (meta-vars-from-list Ys)
          ++ meta-vars-sol-data Γ Xs Xs' ++ tvs)

check-term-spine Γ t'@(ExAppTp t tp) pt max =
  -- 1) type the applicand `t`
    check-term-spine Γ t pt max
      on-fail handleApplicandTypeError
  -- 1a) Xs: spine meta-variables; dt: decorated type of t ; htp: plain type of `t`
  >>=m λ ret → let mk-spine-data Xs dt locl fₕ~ = ret ; htp = decortype-to-type dt in
  -- 2) make sure it reveals a type abstraction
    meta-vars-unfold-tpapp' Γ Xs dt
     on-fail (λ _ → genInapplicableError Xs htp dt)
  -- 3) ensure the type argument has the expected kind,
  --    but don't compare with the contextually infered type argument (for now)
  >>=s λ ret → let mk-tpabsd dt' e? x k sol rdt = ret in
    check-type Γ tp (just (meta-vars-subst-kind Γ Xs k))
  -- 4) produce the result type of the application
  >>= λ tp~ → subst-decortype-if Γ tp~ Xs x k sol rdt
  >>= λ ret → let Xs = fst ret ; rdt = snd ret ; rtp = decortype-to-type rdt in
  -- 5) generate span data
    genAppTpSpan Γ Xs pt rtp htp
  >> check-term-spine-return Xs rdt locl
  -- 7) fill in solutions to meta-vars introduced here and return the rest
    λ sols → AppTp (fₕ~ sols) tp~
    --(map-snd (λ tₕ~ → AppE tₕ~ (Ttp tp~)) ∘ fₕ~)

  where
  mode = prototype-to-checking pt

  span-loc : ctxt → span-location
  span-loc Γ = (ctxt.fn Γ) , term-start-pos t , type-end-pos tp

  handleApplicandTypeError : spanM ∘ maybe $ spine-data
  handleApplicandTypeError =
      [- AppTp-span tt (term-start-pos t) (type-end-pos tp) synthesizing [] nothing -]
    check-type Γ tp nothing >>= λ _ → return nothing

  genInapplicableError : meta-vars → type → decortype → spanM ∘ maybe $ spine-data
  genInapplicableError Xs htp dt =
    check-term-app-tp-errors.inapplicable t tp htp Xs mode Γ dt

  subst-decortype-if : ctxt → type → meta-vars → var → kind → maybe type → decortype → spanM (meta-vars × decortype)
  subst-decortype-if Γ tp Xs x k sol rdt =
    if ~ is-hole tp
      then subst-decortype Γ tp x rdt >>= (λ res → return (Xs , res))
      else let sol = maybe-map (λ t → mk-meta-var-sol t checking) sol
               Y   = meta-var-fresh-tp Xs x (span-loc Γ) (k , sol)
               Xs' = meta-vars-add Xs Y
           in subst-decortype Γ (meta-var-to-type-unsafe Y) x rdt >>= λ rdt' → return (Xs' , rdt')

  genAppTpSpan : ctxt → meta-vars → prototype → (ret-tp head-tp : type) → spanM ⊤
  genAppTpSpan Γ Xs pt ret-tp head-tp = spanM-add ∘ elim-pair
    -- check for a type mismatch, if there even is an expected type
    (meta-vars-check-type-mismatch-if (prototype-to-maybe pt) Γ "synthesizing" Xs ret-tp) $
    -- then take the generated 𝕃 tagged-val and add to the span
    λ tvs → AppTp-span ff (term-start-pos t) (type-end-pos tp) mode $
              tvs {- ++ [ head-type Γ head-tp ] -}
              ++ meta-vars-data-all Γ Xs
              {- ++ (prototype-data Γ tp :: [ decortype-data Γ dt ]) -}

check-term-spine Γ (ExParens _ t _) pt max =
  check-term-spine Γ t pt max

check-term-spine Γ t pt max =
  check-term Γ t nothing >>=c λ t~ htp →
  let locl = num-arrows-in-type Γ htp
  in match-prototype Γ meta-vars-empty ff htp pt
  -- NOTE: it is an invariant that the variables solved in the
  -- solution set of the fst of this are a subset of the variables given
  -- to match-* -- that is, for (σ , W) = match-prototype ...
  -- we have dom(σ) = ∅
  >>= λ ret → let dt = match-proto-dectp ret in
  check-term-spine-return meta-vars-empty dt locl λ _ → t~

-- check-term-app
-- --------------------------------------------------
--
-- If `dom` has unsolved meta-vars in it, synthesize argument t₂ and try to solve for them.
-- Otherwise, check t₂ against a fully known expected type
check-term-app Γ Xs Zs t₁ t₂ (mk-tmabsd dt e? x dom occurs cod) is-locl =
   let Xs' = meta-vars-add* Xs Zs ; tp = decortype-to-type dt in
  -- 1) either synth or check arg type, depending on available info
  --    checking "exits early", as well as failure
  checkArgWithMetas Xs' tp (genAppRetType Γ)
    on-fail return
  -- 2) match *synthesized* type with expected (partial) type
  >>=s uncurry₂ λ rdt t₂~ atp → match-types Γ Xs' empty-trie match-unfolding-both dom atp
  >>= (handleMatchResult Xs' t₂~ atp tp rdt)

  where
  mode = synthesizing

  genAppRetType : ctxt → term → spanM decortype
  genAppRetType Γ t₂~ = if occurs then subst-decortype Γ t₂~ x cod else return cod

  genAppRetTypeHole : ctxt → spanM decortype
  genAppRetTypeHole Γ = if occurs then subst-decortype Γ (Hole posinfo-gen) x cod else return cod

  checkArgWithMetas : meta-vars → type → (term → spanM decortype) → spanM (maybe check-term-app-ret ∨ (decortype × term × type))
  checkArgWithMetas Xs' tp rdt-f =
    -- check arg against fully known type
    if ~ meta-vars-are-free-in-type Xs' dom
      then (check-term Γ t₂ (just dom) >>= λ t₂~ →
            rdt-f t₂~ >>= λ rdt →
            return (inj₁ (just $ check-term-app-return t₂~ Xs' rdt mode [])))
    -- synthesize type for the argument
      else (check-term Γ t₂ nothing >>=c λ t tp →
            rdt-f t >>= λ rdt →
            return (inj₂ $ rdt , t , tp))

  handleMatchResult : meta-vars → (t₂~ : term) → (atp tp : type) → decortype → match-error-t meta-vars → spanM ∘ maybe $ check-term-app-ret
  handleMatchResult Xs' t₂~ atp tp rdt (match-error (msg , tvs)) =
    check-term-app-tm-errors.unmatchable
      t₁ t₂ tp Xs' is-locl mode Γ dom atp msg tvs
  handleMatchResult Xs' t₂~ atp tp rdt (match-ok Xs) =
      meta-vars-subst-decortype' ff Γ Xs rdt
    >>= λ rdt → return ∘ just $ check-term-app-return t₂~ Xs rdt mode []

match-unfolding-next : match-unfolding-state → match-unfolding-state
match-unfolding-next match-unfolding-both = match-unfolding-both
match-unfolding-next match-unfolding-approx = match-unfolding-approx
match-unfolding-next match-unfolding-hnf = match-unfolding-both

module m-err = meta-vars-match-errors

check-type-for-match : ctxt → type → spanM $ match-error-t kind
check-type-for-match Γ tp =
  (with-clear-error $
      check-type (qualified-ctxt Γ) (resugar tp) nothing >>=c λ _ k → return (match-ok $ k)) >>=spand return

-- match-types
-- --------------------------------------------------

match-types-ok : meta-vars → spanM $ match-error-t meta-vars
match-types-ok = return ∘ match-ok

match-types-error : match-error-data → spanM $ match-error-t meta-vars
match-types-error = return ∘ match-error

match-types Γ Xs Ls match-unfolding-both tpₓ tp =
    match-types Γ Xs Ls match-unfolding-approx tpₓ tp
  >>= λ where
    (match-ok Xs) → match-types-ok Xs
    (match-error msg) →
      match-types Γ Xs Ls match-unfolding-hnf
        (hnf Γ unfold-head-elab tpₓ)
        (hnf Γ unfold-head-elab tp)

match-types Γ Xs Ls unf tpₓ@(TpVar x) tp =
  -- check that x is a meta-var
  maybe-else' (meta-vars-lookup-with-kind Xs x)
    -- if not, make sure the two variables are the same
    -- TODO: above assumes no term meta-variables
    (return (err⊎-guard (~ conv-type Γ tpₓ tp) m-err.e-match-failure
            >> match-ok Xs))
  -- scope check the solution
  λ ret → let X = fst ret ; kₓ = snd ret in
  if are-free-in Ls tp then
    match-types-error $ m-err.e-meta-scope Γ tpₓ tp
  else (check-type-for-match Γ tp
  >>=s λ k → match-kinds Γ Xs empty-trie match-unfolding-both kₓ k
    on-fail (λ _ → return ∘ match-error $ m-err.e-bad-sol-kind Γ x tp)
  >>=s λ Xs → return (meta-vars-solve-tp Γ Xs x tp synthesizing)
  >>=s λ Xs → match-types-ok $ meta-vars-update-kinds Γ Xs Xs)

match-types Γ Xs Ls unf (TpApp tpₓ₁ (Ttp tpₓ₂)) (TpApp tp₁ (Ttp tp₂)) =
    match-types Γ Xs Ls unf tpₓ₁ tp₁
  >>=s λ Xs' → match-types Γ Xs' Ls (match-unfolding-next unf) tpₓ₂ tp₂

match-types Γ Xs Ls unf (TpApp tpₓ (Ttm tmₓ)) (TpApp tp (Ttm tm)) =
    match-types Γ Xs Ls unf tpₓ tp
  >>=s λ Xs' →
    return $ if ~ conv-term Γ tmₓ tm
      then (match-error m-err.e-match-failure) else
    match-ok Xs'

match-types Γ Xs Ls unf tpₓ'@(TpAbs bₓ xₓ tkₓ tpₓ) tp'@(TpAbs b x tk tp) =
  if bₓ xor b
    then (match-types-error m-err.e-match-failure)
    else (match-tpkds Γ Xs Ls (match-unfolding-next unf) tkₓ tk >>=s λ Xs' →
          match-types (Γ→Γ' Γ) Xs' Ls' (match-unfolding-next unf) tpₓ tp)
  where
  Γ→Γ' : ctxt → ctxt
  Γ→Γ' Γ = ctxt-rename xₓ x (ctxt-var-decl-if x Γ)
  Ls' = stringset-insert Ls x

match-types Γ Xs Ls unf (TpIota xₓ mₓ tpₓ) (TpIota x m tp) =
  match-types Γ Xs Ls (match-unfolding-next unf) mₓ m
  >>=s λ Xs →
    match-types (Γ→Γ' Γ) Xs Ls' (match-unfolding-next unf) tpₓ tp
  where
  Γ→Γ' : ctxt → ctxt
  Γ→Γ' Γ = ctxt-rename xₓ x (ctxt-var-decl-if x Γ)
  Ls' = stringset-insert Ls x

match-types Γ Xs Ls unf (TpEq t₁ₓ t₂ₓ) (TpEq t₁ t₂) =
  if ~ conv-term Γ t₁ₓ t₁
    then match-types-error $ m-err.e-match-failure else
  if ~ conv-term Γ t₂ₓ t₂
    then match-types-error $ m-err.e-match-failure else
  match-types-ok Xs

match-types Γ Xs Ls unf (TpLam xₓ atkₓ tpₓ) (TpLam x atk tp) =
  match-tpkds Γ Xs Ls (match-unfolding-next unf) atkₓ atk >>=s λ Xs →
  match-types (Γ→Γ' Γ) Xs Ls' (match-unfolding-next unf) tpₓ tp
  where
  Γ→Γ' : ctxt → ctxt
  Γ→Γ' Γ = ctxt-rename xₓ x (ctxt-var-decl-if x Γ)
  Ls' = stringset-insert Ls x

match-types Γ Xs Ls unf tpₓ tp =
  match-types-error m-err.e-match-failure

-- match-kinds
-- --------------------------------------------------

-- match-kinds-norm: match already normalized kinds
match-kinds-norm : ctxt → meta-vars → local-vars → match-unfolding-state → (kₓ k : kind) → spanM $ match-error-t meta-vars

-- kind pi
match-kinds-norm Γ Xs Ls uf (KdAbs xₓ tkₓ kₓ) (KdAbs x tk k) =
  match-tpkds Γ Xs Ls uf tkₓ tk >>=s λ Xs →
  match-kinds (Γ→Γ' Γ) Xs Ls' uf kₓ k
  where
  Γ→Γ' = ctxt-rename xₓ x ∘ ctxt-var-decl-if x
  Ls' = stringset-insert Ls x

match-kinds-norm Γ Xs Ls uf KdStar KdStar =
  match-types-ok $ Xs
match-kinds-norm Γ Xs Ls uf kₓ k =
  match-types-error $ m-err.e-matchk-failure -- m-err.e-kind-ineq Γ kₓ k

match-kinds Γ Xs Ls uf kₓ k =
  match-kinds-norm Γ Xs Ls uf
    (hnf Γ unfold-head-elab kₓ)
    (hnf Γ unfold-head-elab k)

-- match-tk
-- --------------------------------------------------
match-tpkds Γ Xs Ls uf (Tkk kₓ) (Tkk k) = match-kinds Γ Xs Ls uf kₓ k
match-tpkds Γ Xs Ls uf (Tkt tpₓ) (Tkt tp) = match-types Γ Xs Ls uf tpₓ tp
match-tpkds Γ Xs Ls uf tkₓ tk =
  match-types-error m-err.e-matchk-failure -- m-err.e-tk-ineq Γ tkₓ tk

-- match-prototype
-- --------------------------------------------------

match-prototype-err : type → prototype → spanM match-prototype-data
match-prototype-err tp pt = return $ mk-match-prototype-data meta-vars-empty (decor-error tp pt) tt

{-
  --------------------
  Xs ⊢? T ≔ ⁇ ⇒ (∅ , T)
-}
match-prototype Γ Xs uf tp (proto-maybe nothing) =
  return $ mk-match-prototype-data Xs (decor-type tp) ff

{-
  Xs ⊢= T ≔ S ⇒ σ
  --------------------
  Xs ⊢? T ≔ S ⇒ (σ , T)
-}
match-prototype Γ Xs uf tp pt@(proto-maybe (just tp')) =
  match-types Γ Xs empty-trie match-unfolding-both tp tp'
    on-fail (λ _ → return $ mk-match-prototype-data Xs (decor-error tp pt) tt)
  >>=s λ Xs' → return $ mk-match-prototype-data Xs' (decor-type tp) ff

{-
  Xs,X ⊢? T ≔ ⁇ → P ⇒ (σ , W)
  -----------------------------------------------
  Xs ⊢? ∀ X . T ≔ ⁇ → P ⇒ (σ - X , ∀ X = σ(X) . W)
-}
match-prototype Γ Xs uf (TpAbs bₓ x (Tkk k) tp) pt'@(proto-arrow e? pt) =
  -- 1) generate a fresh meta-var Y, add it to the meta-vars, and rename
  --    occurences of x in tp to Y
  let ret = meta-vars-add-from-tpabs Γ missing-span-location Xs Erased x k tp
      Y = fst ret ; Xs' = snd ret ; tp' = subst Γ (meta-var-to-type-unsafe Y) x tp
  -- 2) match the body against the original prototype to generate a decorated type
  --    and find some solutions
  in match-prototype Γ Xs' ff tp' pt'
  >>= λ ret →
  let mk-match-prototype-data Xs' dt err = ret
      Y' = maybe-else' (meta-vars-lookup Xs' (meta-var-name Y)) Y λ Y → Y
      x' = subst-rename-var-if{TYPE} Γ empty-renamectxt x empty-trie tp'
  -- 3) replace the meta-vars with the bound type variable
  in subst-decortype (ctxt-var-decl x' Γ) (TpVar x') (meta-var-name Y) dt
  -- 4) leave behind the solution for Y as a decoration and drop Y from Xs
  >>= λ dt' →
  let sort' = meta-var.sort (meta-var-set-src Y' checking)
      dt″ = decor-decor Erased x (Tkk k) sort' dt' in
  return $ mk-match-prototype-data (meta-vars-remove Xs' Y) dt″ err

{-
  Xs ⊢? T ≔ P ⇒ (σ , P)
  -----------------------------
  Xs ⊢? S → T ≔ ⁇ → P ⇒ (σ , P)
-}
match-prototype Γ Xs uf (TpAbs b x (Tkt dom) cod) (proto-arrow e? pt) =
  match-prototype Γ Xs ff cod pt
  >>= λ ret →
  let mk-match-prototype-data Xs dt err = ret
      dt' = decor-decor b x (Tkt dom) (meta-var-tm dom nothing) dt
  in return $ if b xor e?
    then mk-match-prototype-data meta-vars-empty dt' tt
  else mk-match-prototype-data Xs dt' err

{-
  X ∈ Xs
  -----------------------------------
  Xs ⊢? X ≔ ⁇ → P ⇒ (σ , (X , ⁇ → P))
-}
match-prototype Γ Xs tt tp@(TpVar x) pt@(proto-arrow _ _) =
  return $ mk-match-prototype-data Xs (decor-stuck tp pt) ff

-- everything else...
-- Types for which we should keep digging
match-prototype Γ Xs ff tp@(TpVar x) pt@(proto-arrow _ _) =
  match-prototype Γ Xs tt (hnf Γ unfold-head-elab tp) pt
match-prototype Γ Xs ff tp@(TpApp _ _) pt@(proto-arrow _ _) =
  match-prototype Γ Xs tt (hnf Γ unfold-head-elab tp) pt
-- types for which we should suspend disbelief
match-prototype Γ Xs tt tp@(TpApp _ _) pt@(proto-arrow _ _) =
  return $ mk-match-prototype-data Xs (decor-stuck tp pt) ff
-- types which clearly do not match the prototype
match-prototype Γ Xs uf tp@(TpEq _ _) pt@(proto-arrow _ _) =
  match-prototype-err tp pt
match-prototype Γ Xs uf tp@(TpHole _) pt@(proto-arrow _ _) =
  match-prototype-err tp pt
match-prototype Γ Xs uf tp@(TpLam _ _ _) pt@(proto-arrow _ _) =
  match-prototype-err tp pt
match-prototype Γ Xs uf tp@(TpIota _ _ _) pt@(proto-arrow _ _) =
  match-prototype-err tp pt