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

open import HoTT

open import stash.modalities.gbm.GbmUtil

module stash.modalities.gbm.PullbackSplit where

--     L --> B    K = A ×_D C / (f,h)       d₁ = A -> D <- C
--     |     |g   L = B ×_A K / (g,left)    d₂ = B -> A <- K
--     v     v                              d  = B -> D <- C
--     K --> A
--     |     |f
--     v     v
--     C --> D
--        h

module PullbackLSplit {i j k l} {A : Type i} {B : Type j} {C : Type k}
  {D : Type l} (f : A → D) (g : B → A) (h : C → D) where

  private
    d₁ : Cospan
    d₁ = cospan C A D h f

    d₂ : Cospan
    d₂ = cospan (Pullback d₁) B A Pullback.b g

    d : Cospan
    d = cospan C B D h (f ∘ g)

  split-equiv : Pullback d ≃ Pullback d₂
  split-equiv = equiv to from to-from from-to

    where to : Pullback d → Pullback d₂
          to (pullback c b p) = pullback (pullback c (g b) p) b idp

          from : Pullback d₂ → Pullback d
          from (pullback (pullback c a p) b idp) = pullback c b p

          to-from : (x : Pullback d₂) → to (from x) == x
          to-from (pullback _ b idp) = idp

          from-to : (x : Pullback d) → from (to x) == x
          from-to _ = idp

record CospanMap {i₀ j₀ k₀ i₁ j₁ k₁} (cospan₀ : Cospan {i₀} {j₀} {k₀}) (cospan₁ : Cospan {i₁} {j₁} {k₁})
  : Type (lmax (lmax (lmax i₀ j₀) k₀) (lmax (lmax i₁ j₁) k₁)) where
  constructor cospan-map
  module cospan₀ = Cospan cospan₀
  module cospan₁ = Cospan cospan₁
  field
    hA : cospan₀.A → cospan₁.A
    hB : cospan₀.B → cospan₁.B
    hC : cospan₀.C → cospan₁.C
    f-commutes : CommSquare cospan₀.f cospan₁.f hA hC
    g-commutes : CommSquare cospan₀.g cospan₁.g hB hC

CospanEquiv : ∀ {i₀ j₀ k₀ i₁ j₁ k₁} (cospan₀ : Cospan {i₀} {j₀} {k₀}) (cospan₁ : Cospan {i₁} {j₁} {k₁})
  → Type (lmax (lmax (lmax i₀ j₀) k₀) (lmax (lmax i₁ j₁) k₁))
CospanEquiv cospan₀ cospan₁ = Σ (CospanMap cospan₀ cospan₁)
  (λ cospan-map → is-equiv (CospanMap.hA cospan-map)
                 × is-equiv (CospanMap.hB cospan-map)
                 × is-equiv (CospanMap.hC cospan-map))

CospanEquiv-inverse : ∀ {i₀ j₀ k₀ i₁ j₁ k₁} {cospan₀ : Cospan {i₀} {j₀} {k₀}} {cospan₁ : Cospan {i₁} {j₁} {k₁}}
  → CospanEquiv cospan₀ cospan₁ → CospanEquiv cospan₁ cospan₀
CospanEquiv-inverse (cospan-map hA hB hC f-commutes g-commutes , hA-ise , hB-ise , hC-ise)
  = (cospan-map hA.g hB.g hC.g
        (CommSquare-inverse-v f-commutes hA-ise hC-ise)
        (CommSquare-inverse-v g-commutes hB-ise hC-ise))
      , ( is-equiv-inverse hA-ise
        , is-equiv-inverse hB-ise
        , is-equiv-inverse hC-ise)
   where module hA = is-equiv hA-ise
         module hB = is-equiv hB-ise
         module hC = is-equiv hC-ise

module PullbackFmap {i₀ j₀ k₀ i₁ j₁ k₁} {cospan₀ : Cospan {i₀} {j₀} {k₀}}
  {cospan₁ : Cospan {i₁} {j₁} {k₁}} (cospan-map : CospanMap cospan₀ cospan₁) where

  f : Pullback cospan₀ → Pullback cospan₁
  f (pullback a b h) = pullback
    (CospanMap.hA cospan-map a)
    (CospanMap.hB cospan-map b)
    (! (commutes (CospanMap.f-commutes cospan-map) a) ∙
      ap (λ x → CospanMap.hC cospan-map x) h ∙
      (commutes (CospanMap.g-commutes cospan-map) b))

Pullback-fmap = PullbackFmap.f

module _ {i₀ j₀ k₀ i₁ j₁ k₁} {cospan₀ : Cospan {i₀} {j₀} {k₀}}
  {cospan₁ : Cospan {i₁} {j₁} {k₁}} (cospan-equiv : CospanEquiv cospan₀ cospan₁) where

  private
    module cospan₀ = Cospan cospan₀
    module cospan₁ = Cospan cospan₁
    cospan-to = fst cospan-equiv
    cospan-from = fst (CospanEquiv-inverse cospan-equiv)
    module cospan-to = CospanMap cospan-to
    module cospan-from = CospanMap cospan-from
    module To = PullbackFmap cospan-to
    module From = PullbackFmap cospan-from
    cospan-ise = snd cospan-equiv
    hA-ise = fst cospan-ise
    hB-ise = fst (snd cospan-ise)
    hC-ise = snd (snd cospan-ise)
    module hA-ise = is-equiv hA-ise
    module hB-ise = is-equiv hB-ise
    module hC-ise = is-equiv hC-ise

    f = cospan₀.f
    g = cospan₀.g
    f' = cospan₁.f
    g' = cospan₁.g

    α = commutes cospan-to.f-commutes
    β = commutes cospan-to.g-commutes

    α' = commutes cospan-from.f-commutes
    β' = commutes cospan-from.g-commutes

    hA = cospan-to.hA
    hB = cospan-to.hB
    hC = cospan-to.hC

    kA = cospan-from.hA
    kB = cospan-from.hB
    kC = cospan-from.hC

    module kA-ise = is-equiv (is-equiv-inverse hA-ise)
    module kB-ise = is-equiv (is-equiv-inverse hB-ise)
    module kC-ise = is-equiv (is-equiv-inverse hC-ise)

    kA-ise = is-equiv-inverse hA-ise
    kB-ise = is-equiv-inverse hB-ise
    kC-ise = is-equiv-inverse hC-ise

    to = To.f
    from = From.f

    from-to : ∀ x → from (to x) == x
    from-to (pullback a b h) = pullback= _ (hA-ise.g-f a) (hB-ise.g-f b) goal

      where eq₀ = hC-ise.g-f (f a) ∙ h ∙ ! (hC-ise.g-f (g b))
                    =⟨ ! (ap-idf h) |in-ctx (λ x → hC-ise.g-f (f a) ∙ x ∙ ! (hC-ise.g-f (g b))) ⟩
                  hC-ise.g-f (f a) ∙ ap (idf _) h ∙ ! (hC-ise.g-f (g b))
                    =⟨ ! (∙-assoc (hC-ise.g-f (f a)) _ _) ⟩
                  (hC-ise.g-f (f a) ∙ ap (idf _) h) ∙ ! (hC-ise.g-f (g b))
                    =⟨ ↓-==-out (apd hC-ise.g-f h) |in-ctx (λ x → x ∙ ! (hC-ise.g-f (g b))) ⟩
                  (ap (kC ∘ hC) h ∙ hC-ise.g-f (g b)) ∙ ! (hC-ise.g-f (g b))
                    =⟨ ∙-assoc (ap (kC ∘ hC) h) _ _ ⟩
                  ap (kC ∘ hC) h ∙ hC-ise.g-f (g b) ∙ ! (hC-ise.g-f (g b))
                    =⟨ !-inv-r (hC-ise.g-f (g b)) |in-ctx (λ x → ap (kC ∘ hC) h ∙ x) ⟩
                  ap (kC ∘ hC) h ∙ idp
                    =⟨ ∙-unit-r (ap (kC ∘ hC) h) ⟩
                  ap (kC ∘ hC) h ∎

            eq₁ = β' (hB b)
                    =⟨ ! (hB-ise.adj b) |in-ctx (λ x → ap kC (! (β (kB (hB b)) ∙ ap g' x)) ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ap kC (! (β (kB (hB b)) ∙ ap g' (ap hB (hB-ise.g-f b)))) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ ∘-ap g' hB (hB-ise.g-f b) |in-ctx (λ x → ap kC (! (β (kB (hB b)) ∙ x)) ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ap kC (! (β (kB (hB b)) ∙ ap (g' ∘ hB) (hB-ise.g-f b))) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ ↓-==-out (apd β (hB-ise.g-f b)) |in-ctx (λ x → ap kC (! x) ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ap kC (! (ap (hC ∘ g) (hB-ise.g-f b) ∙ β b)) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ ap-! kC (ap (hC ∘ g) (hB-ise.g-f b) ∙ β b) |in-ctx (λ x → x ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ! (ap kC (ap (hC ∘ g) (hB-ise.g-f b) ∙ β b)) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ ap-∙ kC (ap (hC ∘ g) (hB-ise.g-f b)) (β b) |in-ctx (λ x → ! x ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ! (ap kC (ap (hC ∘ g) (hB-ise.g-f b)) ∙ ap kC (β b)) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ !-∙ (ap kC (ap (hC ∘ g) (hB-ise.g-f b))) (ap kC (β b)) |in-ctx (λ x → x ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  (! (ap kC (β b)) ∙ ! (ap kC (ap (hC ∘ g) (hB-ise.g-f b)))) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ ∙-assoc (! (ap kC (β b))) _ _ ⟩
                  ! (ap kC (β b)) ∙ ! (ap kC (ap (hC ∘ g) (hB-ise.g-f b))) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ ∘-ap kC (hC ∘ g) (hB-ise.g-f b) |in-ctx (λ x → ! (ap kC (β b)) ∙ ! x ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ! (ap kC (β b)) ∙ ! (ap (kC ∘ hC ∘ g) (hB-ise.g-f b)) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ ! (∘-ap (kC ∘ hC) g (hB-ise.g-f b)) |in-ctx (λ x → ! (ap kC (β b)) ∙ ! x ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ! (ap kC (β b)) ∙ ! (ap (kC ∘ hC) (ap g (hB-ise.g-f b))) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ eqv-square' (hC , hC-ise) (ap g (hB-ise.g-f b)) |in-ctx (λ x → ! (ap kC (β b)) ∙ ! x ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ! (ap kC (β b)) ∙ ! (hC-ise.g-f (g (kB (hB b))) ∙ (ap g (hB-ise.g-f b)) ∙ ! (hC-ise.g-f (g b))) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ !-∙ (hC-ise.g-f (g (kB (hB b)))) ((ap g (hB-ise.g-f b)) ∙ ! (hC-ise.g-f (g b))) |in-ctx (λ x → ! (ap kC (β b)) ∙ x ∙ hC-ise.g-f (g (kB (hB b)))) ⟩
                  ! (ap kC (β b)) ∙ (! (ap g (hB-ise.g-f b) ∙ ! (hC-ise.g-f (g b))) ∙ ! (hC-ise.g-f (g (kB (hB b))))) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ ∙-assoc (! (ap g (hB-ise.g-f b) ∙ ! (hC-ise.g-f (g b)))) _ _ |in-ctx (λ x → ! (ap kC (β b)) ∙ x) ⟩
                  ! (ap kC (β b)) ∙ ! (ap g (hB-ise.g-f b) ∙ ! (hC-ise.g-f (g b))) ∙ ! (hC-ise.g-f (g (kB (hB b)))) ∙ hC-ise.g-f (g (kB (hB b)))
                    =⟨ !-inv-l (hC-ise.g-f (g (kB (hB b)))) |in-ctx (λ x → ! (ap kC (β b)) ∙ ! (ap g (hB-ise.g-f b) ∙ ! (hC-ise.g-f (g b))) ∙ x) ⟩
                  ! (ap kC (β b)) ∙ ! (ap g (hB-ise.g-f b) ∙ ! (hC-ise.g-f (g b))) ∙ idp
                    =⟨ ∙-unit-r (! (ap g (hB-ise.g-f b) ∙ ! (hC-ise.g-f (g b)))) |in-ctx (λ x → ! (ap kC (β b)) ∙ x) ⟩
                  ! (ap kC (β b)) ∙ ! (ap g (hB-ise.g-f b) ∙ ! (hC-ise.g-f (g b)))
                    =⟨ !-∙ (ap g (hB-ise.g-f b)) (! (hC-ise.g-f (g b))) |in-ctx (λ x → ! (ap kC (β b)) ∙ x) ⟩
                  ! (ap kC (β b)) ∙ ! (! (hC-ise.g-f (g b))) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ !-! (hC-ise.g-f (g b)) |in-ctx (λ x → ! (ap kC (β b)) ∙ x ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (ap kC (β b)) ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b)) ∎

            eq₂ = α' (hA a)
                    =⟨ ! (hA-ise.adj a) |in-ctx (λ x → ap kC (! (α (kA (hA a)) ∙ ap f' x)) ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ap kC (! (α (kA (hA a)) ∙ ap f' (ap hA (hA-ise.g-f a)))) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ ∘-ap f' hA (hA-ise.g-f a) |in-ctx (λ x → ap kC (! (α (kA (hA a)) ∙ x)) ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ap kC (! (α (kA (hA a)) ∙ ap (f' ∘ hA) (hA-ise.g-f a))) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ ↓-==-out (apd α (hA-ise.g-f a)) |in-ctx (λ x → ap kC (! x) ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ap kC (! (ap (hC ∘ f) (hA-ise.g-f a) ∙ α a)) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ ap-! kC (ap (hC ∘ f) (hA-ise.g-f a) ∙ α a) |in-ctx (λ x → x ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ! (ap kC (ap (hC ∘ f) (hA-ise.g-f a) ∙ α a)) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ ap-∙ kC (ap (hC ∘ f) (hA-ise.g-f a)) (α a) |in-ctx (λ x → ! x ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ! (ap kC (ap (hC ∘ f) (hA-ise.g-f a)) ∙ ap kC (α a)) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ !-∙ (ap kC (ap (hC ∘ f) (hA-ise.g-f a))) (ap kC (α a)) |in-ctx (λ x → x ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  (! (ap kC (α a)) ∙ ! (ap kC (ap (hC ∘ f) (hA-ise.g-f a)))) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ ∙-assoc (! (ap kC (α a))) _ _ ⟩
                  ! (ap kC (α a)) ∙ ! (ap kC (ap (hC ∘ f) (hA-ise.g-f a))) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ ∘-ap kC (hC ∘ f) (hA-ise.g-f a) |in-ctx (λ x → ! (ap kC (α a)) ∙ ! x ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ! (ap kC (α a)) ∙ ! (ap (kC ∘ hC ∘ f) (hA-ise.g-f a)) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ ! (∘-ap (kC ∘ hC) f (hA-ise.g-f a)) |in-ctx (λ x → ! (ap kC (α a)) ∙ ! x ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ! (ap kC (α a)) ∙ ! (ap (kC ∘ hC) (ap f (hA-ise.g-f a))) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ eqv-square' (hC , hC-ise) (ap f (hA-ise.g-f a)) |in-ctx (λ x → ! (ap kC (α a)) ∙ ! x ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ! (ap kC (α a)) ∙ ! (hC-ise.g-f (f (kA (hA a))) ∙ (ap f (hA-ise.g-f a)) ∙ ! (hC-ise.g-f (f a))) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ !-∙ (hC-ise.g-f (f (kA (hA a)))) ((ap f (hA-ise.g-f a)) ∙ ! (hC-ise.g-f (f a))) |in-ctx (λ x → ! (ap kC (α a)) ∙ x ∙ hC-ise.g-f (f (kA (hA a)))) ⟩
                  ! (ap kC (α a)) ∙ (! (ap f (hA-ise.g-f a) ∙ ! (hC-ise.g-f (f a))) ∙ ! (hC-ise.g-f (f (kA (hA a))))) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ ∙-assoc (! (ap f (hA-ise.g-f a) ∙ ! (hC-ise.g-f (f a)))) _ _ |in-ctx (λ x → ! (ap kC (α a)) ∙ x) ⟩
                  ! (ap kC (α a)) ∙ ! (ap f (hA-ise.g-f a) ∙ ! (hC-ise.g-f (f a))) ∙ ! (hC-ise.g-f (f (kA (hA a)))) ∙ hC-ise.g-f (f (kA (hA a)))
                    =⟨ !-inv-l (hC-ise.g-f (f (kA (hA a)))) |in-ctx (λ x → ! (ap kC (α a)) ∙ ! (ap f (hA-ise.g-f a) ∙ ! (hC-ise.g-f (f a))) ∙ x) ⟩
                  ! (ap kC (α a)) ∙ ! (ap f (hA-ise.g-f a) ∙ ! (hC-ise.g-f (f a))) ∙ idp
                    =⟨ ∙-unit-r (! (ap f (hA-ise.g-f a) ∙ ! (hC-ise.g-f (f a)))) |in-ctx (λ x → ! (ap kC (α a)) ∙ x) ⟩
                  ! (ap kC (α a)) ∙ ! (ap f (hA-ise.g-f a) ∙ ! (hC-ise.g-f (f a)))
                    =⟨ !-∙ (ap f (hA-ise.g-f a)) (! (hC-ise.g-f (f a))) |in-ctx (λ x → ! (ap kC (α a)) ∙ x) ⟩
                  ! (ap kC (α a)) ∙ ! (! (hC-ise.g-f (f a))) ∙ ! (ap f (hA-ise.g-f a))
                    =⟨ !-! (hC-ise.g-f (f a)) |in-ctx (λ x → ! (ap kC (α a)) ∙ x ∙ ! (ap f (hA-ise.g-f a))) ⟩
                  ! (ap kC (α a)) ∙ hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a)) ∎

            lem = ! (α' (hA a)) ∙ ap kC (! (α a) ∙ ap hC h ∙ β b) ∙ β' (hB b)
                    =⟨ ap-∙ kC (! (α a)) (ap hC h ∙ β b) |in-ctx (λ x → ! (α' (hA a)) ∙ x ∙ β' (hB b)) ⟩
                  ! (α' (hA a)) ∙ (ap kC (! (α a)) ∙ ap kC (ap hC h ∙ β b)) ∙ β' (hB b)
                    =⟨ ∙-assoc (ap kC (! (α a))) (ap kC (ap hC h ∙ β b)) (β' (hB b)) |in-ctx (λ x → ! (α' (hA a)) ∙ x) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap kC (ap hC h ∙ β b) ∙ β' (hB b)
                    =⟨ ap-∙ kC (ap hC h) (β b) |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ x ∙ β' (hB b)) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ (ap kC (ap hC h) ∙ ap kC (β b)) ∙ β' (hB b)
                    =⟨ ∙-assoc (ap kC (ap hC h)) (ap kC (β b)) (β' (hB b)) |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ x) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap kC (ap hC h) ∙ ap kC (β b) ∙ β' (hB b)
                    =⟨ ∘-ap kC hC h |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ x ∙ ap kC (β b) ∙ β' (hB b)) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap (kC ∘ hC) h ∙ ap kC (β b) ∙ β' (hB b)
                    =⟨ eq₁ |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap (kC ∘ hC) h ∙ ap kC (β b) ∙ x) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap (kC ∘ hC) h ∙ ap kC (β b) ∙ ! (ap kC (β b)) ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ! (∙-assoc (ap kC (β b)) _ _) |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap (kC ∘ hC) h ∙ x) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap (kC ∘ hC) h ∙ (ap kC (β b) ∙ ! (ap kC (β b))) ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ !-inv-r (ap kC (β b)) |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap (kC ∘ hC) h ∙ x ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ap (kC ∘ hC) h ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ! eq₀ |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ x ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ (hC-ise.g-f (f a) ∙ h ∙ ! (hC-ise.g-f (g b))) ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ! (∙-assoc (hC-ise.g-f (f a)) _ _) |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ x ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ ((hC-ise.g-f (f a) ∙ h) ∙ ! (hC-ise.g-f (g b))) ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ∙-assoc (hC-ise.g-f (f a) ∙ h) _ _ |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ x) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ (hC-ise.g-f (f a) ∙ h) ∙ ! (hC-ise.g-f (g b)) ∙ hC-ise.g-f (g b) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ! (∙-assoc (! (hC-ise.g-f (g b))) _ _) |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ (hC-ise.g-f (f a) ∙ h) ∙ x) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ (hC-ise.g-f (f a) ∙ h) ∙ (! (hC-ise.g-f (g b)) ∙ hC-ise.g-f (g b)) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ !-inv-l (hC-ise.g-f (g b)) |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ (hC-ise.g-f (f a) ∙ h) ∙ x ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ (hC-ise.g-f (f a) ∙ h) ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ∙-assoc (hC-ise.g-f (f a)) _ _ |in-ctx (λ x → ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ x) ⟩
                  ! (α' (hA a)) ∙ ap kC (! (α a)) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ eq₂ |in-ctx (λ x → ! x ∙ ap kC (! (α a)) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (! (ap kC (α a)) ∙ hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ ap kC (! (α a)) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ !-∙ (! (ap kC (α a))) _ |in-ctx (λ x → x ∙ ap kC (! (α a)) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  (! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ ! (! (ap kC (α a)))) ∙ ap kC (! (α a)) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ∙-assoc (! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a)))) _ _ ⟩
                  ! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ ! (! (ap kC (α a))) ∙ ap kC (! (α a)) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ap-! kC (α a) |in-ctx (λ x → ! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ ! (! (ap kC (α a))) ∙ x ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ ! (! (ap kC (α a))) ∙ ! (ap kC (α a)) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ! (∙-assoc (! (! (ap kC (α a)))) _ _) |in-ctx (λ x → ! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ x) ⟩
                  ! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ (! (! (ap kC (α a))) ∙ ! (ap kC (α a))) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ !-inv-l (! (ap kC (α a))) |in-ctx (λ x → ! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ x ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (hC-ise.g-f (f a) ∙ ! (ap f (hA-ise.g-f a))) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ !-∙ (hC-ise.g-f (f a)) _  |in-ctx (λ x → x ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  (! (! (ap f (hA-ise.g-f a))) ∙ ! (hC-ise.g-f (f a))) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ∙-assoc (! (! (ap f (hA-ise.g-f a)))) _ _ ⟩
                  ! (! (ap f (hA-ise.g-f a))) ∙ ! (hC-ise.g-f (f a)) ∙ hC-ise.g-f (f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ ! (∙-assoc (! (hC-ise.g-f (f a))) _ _) |in-ctx (λ x → ! (! (ap f (hA-ise.g-f a))) ∙ x) ⟩
                  ! (! (ap f (hA-ise.g-f a))) ∙ (! (hC-ise.g-f (f a)) ∙ hC-ise.g-f (f a)) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ !-inv-l (hC-ise.g-f (f a)) |in-ctx (λ x → ! (! (ap f (hA-ise.g-f a))) ∙ x ∙ h ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ! (! (ap f (hA-ise.g-f a))) ∙ h ∙ ! (ap g (hB-ise.g-f b))
                    =⟨ !-! (ap f (hA-ise.g-f a)) |in-ctx (λ x → x ∙ h ∙ ! (ap g (hB-ise.g-f b))) ⟩
                  ap f (hA-ise.g-f a) ∙ h ∙ ! (ap g (hB-ise.g-f b)) ∎

            goal = (! (α' (hA a)) ∙ ap kC (! (α a) ∙ ap hC h ∙ β b) ∙ β' (hB b)) ∙ ap g (hB-ise.g-f b)
                     =⟨ lem |in-ctx (λ x → x ∙ ap g (hB-ise.g-f b)) ⟩
                   (ap f (hA-ise.g-f a) ∙ h ∙ ! (ap g (hB-ise.g-f b))) ∙ ap g (hB-ise.g-f b)
                     =⟨ ∙-assoc (ap f (hA-ise.g-f a)) (h ∙ ! (ap g (hB-ise.g-f b))) _ ⟩
                   ap f (hA-ise.g-f a) ∙ (h ∙ ! (ap g (hB-ise.g-f b))) ∙ ap g (hB-ise.g-f b)
                     =⟨ ∙-assoc h _ _ |in-ctx (λ x → ap f (hA-ise.g-f a) ∙ x) ⟩
                   ap f (hA-ise.g-f a) ∙ h ∙ ! (ap g (hB-ise.g-f b)) ∙ ap g (hB-ise.g-f b)
                     =⟨ !-inv-l (ap g (hB-ise.g-f b)) |in-ctx (λ x → ap f (hA-ise.g-f a) ∙ h ∙ x) ⟩
                   ap f (hA-ise.g-f a) ∙ h ∙ idp
                     =⟨ ∙-unit-r h |in-ctx (λ x → ap f (hA-ise.g-f a) ∙ x) ⟩
                   ap f (hA-ise.g-f a) ∙ h ∎

    postulate
      to-from : ∀ y → to (from y) == y
      -- to-from (pullback a b h) = pullback= _ (hA-ise.f-g a) (hB-ise.f-g b) {!!}

  Pullback-emap : Pullback cospan₀ ≃ Pullback cospan₁
  Pullback-emap = equiv to from to-from from-to


text:
{-

Closure properties of FinSet under several type constructors.

-}
{-# OPTIONS --safe #-}

module Cubical.Data.FinSet.Constructors where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv

open import Cubical.HITs.PropositionalTruncation renaming (rec to TruncRec)

open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Data.Empty renaming (rec to EmptyRec)
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.Data.Fin
open import Cubical.Data.SumFin renaming (Fin to SumFin) hiding (discreteFin)
open import Cubical.Data.FinSet.Base
open import Cubical.Data.FinSet.Properties
open import Cubical.Data.FinSet.FiniteChoice

open import Cubical.Relation.Nullary

open import Cubical.Functions.Embedding
open import Cubical.Functions.Surjection

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

module _
  (X : Type ℓ)(p : ≃Fin X) where

  ≃Fin∥∥ : ≃Fin ∥ X ∥
  ≃Fin∥∥ = ≃SumFin→Fin (_ , compEquiv (propTrunc≃ (≃Fin→SumFin p .snd)) (SumFin∥∥≃ _))

module _
  (X : Type ℓ )(p : ≃Fin X)
  (Y : Type ℓ')(q : ≃Fin Y) where

  ≃Fin⊎ : ≃Fin (X ⊎ Y)
  ≃Fin⊎ = ≃SumFin→Fin (_ , compEquiv (⊎-equiv (≃Fin→SumFin p .snd) (≃Fin→SumFin q .snd)) (SumFin⊎≃ _ _))

  ≃Fin× : ≃Fin (X × Y)
  ≃Fin× = ≃SumFin→Fin (_ , compEquiv (Σ-cong-equiv (≃Fin→SumFin p .snd) (λ _ → ≃Fin→SumFin q .snd)) (SumFin×≃ _ _))

module _
  (X : Type ℓ )(p : ≃Fin X)
  (Y : X → Type ℓ')(q : (x : X) → ≃Fin (Y x)) where

  private
    p' = ≃Fin→SumFin p

    m = p' .fst
    e = p' .snd

    q' : (x : X) → ≃SumFin (Y x)
    q' x = ≃Fin→SumFin (q x)

    f : (x : X) → ℕ
    f x = q' x .fst

  ≃SumFinΣ : ≃SumFin (Σ X Y)
  ≃SumFinΣ = _ ,
      Σ-cong-equiv {B' = λ x → Y (invEq (p' .snd) x)} (p' .snd) (transpFamily p')
    ⋆ Σ-cong-equiv-snd (λ x → q' (invEq e x) .snd)
    ⋆ SumFinΣ≃ _ _

  ≃SumFinΠ : ≃SumFin ((x : X) → Y x)
  ≃SumFinΠ = _ ,
      equivΠ {B' = λ x → Y (invEq (p' .snd) x)} (p' .snd) (transpFamily p')
    ⋆ equivΠCod (λ x → q' (invEq e x) .snd)
    ⋆ SumFinΠ≃ _ _

  ≃FinΣ : ≃Fin (Σ X Y)
  ≃FinΣ = ≃SumFin→Fin ≃SumFinΣ

  ≃FinΠ : ≃Fin ((x : X) → Y x)
  ≃FinΠ = ≃SumFin→Fin ≃SumFinΠ

module _
  (X : FinSet ℓ)
  (Y : X .fst → FinSet ℓ') where

  isFinSetΣ : isFinSet (Σ (X .fst) (λ x → Y x .fst))
  isFinSetΣ =
    elim2 (λ _ _ → isPropIsFinSet {A = Σ (X .fst) (λ x → Y x .fst)})
          (λ p q → ∣ ≃FinΣ (X .fst) p (λ x → Y x .fst) q ∣)
          (X .snd) (choice X (λ x → ≃Fin (Y x .fst)) (λ x → Y x .snd))

  isFinSetΠ : isFinSet ((x : X .fst) → Y x .fst)
  isFinSetΠ =
    elim2 (λ _ _ → isPropIsFinSet {A = ((x : X .fst) → Y x .fst)})
          (λ p q → ∣ ≃FinΠ (X .fst) p (λ x → Y x .fst) q ∣)
          (X .snd) (choice X (λ x → ≃Fin (Y x .fst)) (λ x → Y x .snd))

module _
  (X : FinSet ℓ)
  (Y : X .fst → FinSet ℓ')
  (Z : (x : X .fst) → Y x .fst → FinSet ℓ'') where

  isFinSetΠ2 : isFinSet ((x : X .fst) → (y : Y x .fst) → Z x y .fst)
  isFinSetΠ2 = isFinSetΠ X (λ x → _ , isFinSetΠ (Y x) (Z x))

module _
  (X : FinSet ℓ)
  (Y : X .fst → FinSet ℓ')
  (Z : (x : X .fst) → Y x .fst → FinSet ℓ'')
  (W : (x : X .fst) → (y : Y x .fst) → Z x y .fst → FinSet ℓ''') where

  isFinSetΠ3 : isFinSet ((x : X .fst) → (y : Y x .fst) → (z : Z x y .fst) → W x y z .fst)
  isFinSetΠ3 = isFinSetΠ X (λ x → _ , isFinSetΠ2 (Y x) (Z x) (W x))

module _
  (X : FinSet ℓ) where

  isFinSet≡ : (a b : X .fst) → isFinSet (a ≡ b)
  isFinSet≡ a b = isDecProp→isFinSet (isFinSet→isSet (X .snd) a b) (isFinSet→Discrete (X .snd) a b)

  isFinSetIsContr : isFinSet (isContr (X .fst))
  isFinSetIsContr = isFinSetΣ X (λ x → _ , (isFinSetΠ X (λ y → _ , isFinSet≡ x y)))

  isFinSet∥∥ : isFinSet ∥ X .fst ∥
  isFinSet∥∥ = TruncRec isPropIsFinSet (λ p → ∣ ≃Fin∥∥ (X .fst) p ∣) (X .snd)

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ')
  (f : X .fst → Y .fst) where

  isFinSetFiber : (y : Y .fst) → isFinSet (fiber f y)
  isFinSetFiber y = isFinSetΣ X (λ x → _ , isFinSet≡ Y (f x) y)

  isFinSetIsEquiv : isFinSet (isEquiv f)
  isFinSetIsEquiv =
    EquivPresIsFinSet
      (invEquiv (isEquiv≃isEquiv' f))
      (isFinSetΠ Y (λ y → _ , isFinSetIsContr (_ , isFinSetFiber y)))

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ') where

  isFinSet⊎ : isFinSet (X .fst ⊎ Y .fst)
  isFinSet⊎ = elim2 (λ _ _ → isPropIsFinSet) (λ p q → ∣ ≃Fin⊎ (X .fst) p (Y .fst) q ∣) (X .snd) (Y .snd)

  isFinSet× : isFinSet (X .fst × Y .fst)
  isFinSet× = elim2 (λ _ _ → isPropIsFinSet) (λ p q → ∣ ≃Fin× (X .fst) p (Y .fst) q ∣) (X .snd) (Y .snd)

  isFinSet→ : isFinSet (X .fst → Y .fst)
  isFinSet→ = isFinSetΠ X (λ _ → Y)

  isFinSet≃ : isFinSet (X .fst ≃ Y .fst)
  isFinSet≃ = isFinSetΣ (_ , isFinSet→) (λ f → _ , isFinSetIsEquiv X Y f)

module _
  (X : FinSet ℓ) where

  isFinSet¬ : isFinSet (¬ (X .fst))
  isFinSet¬ = isFinSet→ X (⊥ , ∣ 0 , uninhabEquiv (λ x → x) ¬Fin0 ∣)

module _
  (X : FinSet ℓ) where

  isFinSetNonEmpty : isFinSet (NonEmpty (X .fst))
  isFinSetNonEmpty = isFinSet¬ (_ , isFinSet¬ X)

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ')
  (f : X .fst → Y .fst) where

  isFinSetIsEmbedding : isFinSet (isEmbedding f)
  isFinSetIsEmbedding =
    isFinSetΠ2 X (λ _ → X)
      (λ a b → _ , isFinSetIsEquiv (_ , isFinSet≡ X a b) (_ , isFinSet≡ Y (f a) (f b)) (cong f))

  isFinSetIsSurjection : isFinSet (isSurjection f)
  isFinSetIsSurjection =
    isFinSetΠ Y (λ y → _ , isFinSet∥∥ (_ , isFinSetFiber X Y f y))

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ') where

  isFinSet↪ : isFinSet (X .fst ↪ Y .fst)
  isFinSet↪ = isFinSetΣ (_ , isFinSet→ X Y) (λ f → _ , isFinSetIsEmbedding X Y f)

  isFinSet↠ : isFinSet (X .fst ↠ Y .fst)
  isFinSet↠ = isFinSetΣ (_ , isFinSet→ X Y) (λ f → _ , isFinSetIsSurjection X Y f)

ext: agda

max_stars_repo_name: FernandoLarrain/cubical


text:
{-# OPTIONS --cubical --safe #-}

module Data.Sigma.Unique where

open import Data.Sigma.Base
open import Level
open import Path

∃! : ∀ {a b} {A : Type a} → (A → Type b) → Type (a ℓ⊔ b)
∃! B = ∃ x × B x × (∀ {y} → B y → x ≡ y)

infixr 4.5 ∃!-syntax
∃!-syntax : ∀ {a b} {A : Type a} (B : A → Type b) → Type (a ℓ⊔ b)
∃!-syntax = ∃!

syntax ∃!-syntax (λ x → e) = ∃ x ! × e

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the heterogeneous prefix relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Prefix.Heterogeneous where

open import Level
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise
  using (Pointwise; []; _∷_)
open import Data.Product using (∃; _×_; _,_; uncurry)
open import Relation.Binary using (REL; _⇒_)

module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where

  data Prefix : REL (List A) (List B) (a ⊔ b ⊔ r) where
    []  : ∀ {bs} → Prefix [] bs
    _∷_ : ∀ {a b as bs} → R a b → Prefix as bs → Prefix (a ∷ as) (b ∷ bs)

  data PrefixView (as : List A) : List B → Set (a ⊔ b ⊔ r) where
    _++_ : ∀ {cs} → Pointwise R as cs → ∀ ds → PrefixView as (cs List.++ ds)

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {a b as bs} where

  head : Prefix R (a ∷ as) (b ∷ bs) → R a b
  head (r ∷ rs) = r

  tail : Prefix R (a ∷ as) (b ∷ bs) → Prefix R as bs
  tail (r ∷ rs) = rs

  uncons : Prefix R (a ∷ as) (b ∷ bs) → R a b × Prefix R as bs
  uncons (r ∷ rs) = r , rs

module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where

  map : R ⇒ S → Prefix R ⇒ Prefix S
  map R⇒S []       = []
  map R⇒S (r ∷ rs) = R⇒S r ∷ map R⇒S rs

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  toView : ∀ {as bs} → Prefix R as bs → PrefixView R as bs
  toView []       = [] ++ _
  toView (r ∷ rs) with toView rs
  ... | rs′ ++ ds = (r ∷ rs′) ++ ds

  fromView : ∀ {as bs} → PrefixView R as bs → Prefix R as bs
  fromView ([]       ++ ds) = []
  fromView ((r ∷ rs) ++ ds) = r ∷ fromView (rs ++ ds)


text:
module Structure.Category.Action where

open import Structure.Category.Functor

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Fin
open import lib.types.Nat
open import lib.types.Empty
open import lib.NType2
open import lib.Equivalence2

open import Util.Misc
open import Util.Coproducts

{- Some useful lemmas about working with finite sets. E.g. An injection from a finite set
   to itself is an equivalence, an injection from a finite set to a large finite set has
   at least one element not in its image.
-}
module Util.Finite where

ℕ=-to-Fin= : {n : ℕ} {x y : Fin n} → (fst x == fst y) → x == y
ℕ=-to-Fin= p = pair= p prop-has-all-paths-↓

finite-lpo : {i : ULevel} {n : ℕ} (P : Fin n → Type i) (dec : (x : Fin n) → Dec (P x)) →
  (Σ (Fin n) P ⊔ ((x : Fin n) → ¬ (P x)))

finite-lpo {n = 0} P dec = inr (λ x _ → –> Fin-equiv-Empty x)
finite-lpo {i} {n = S n} P dec = ⊔-fmap (–> el) (–> er) lemma
  where
    P' : Fin n ⊔ ⊤ → Type i
    P' z = P (<– Fin-equiv-Coprod z)

    el : Σ (Fin n ⊔ ⊤) P' ≃ Σ (Fin (S n)) P
    el = Σ-emap-l P (Fin-equiv-Coprod ⁻¹)

    er : ((x : Fin n ⊔ ⊤) → ¬ (P' x)) ≃ ((x : Fin (S n)) → ¬ (P x))
    er = Π-emap-l (¬ ∘ P) (Fin-equiv-Coprod ⁻¹)

    lemma : Σ (Fin n ⊔ ⊤) P' ⊔ ((x : Fin n ⊔ ⊤) → ¬ (P' x))
    lemma = ⊔-rec (λ np → inl ((inl (fst np)) , (snd np)))
      (λ f → ⊔-rec (λ p → inl ((inr unit) , p)) (λ np → inr (λ { (inl k) → f k ; (inr _) → np})) (dec (n , ltS))) (finite-lpo {n = n} (P' ∘ inl) λ x → dec (<– Fin-equiv-Coprod (inl x)))

fin-img-dec : {i : ULevel} {A : Type i} (dec : has-dec-eq A) {n : ℕ} (inc : Fin n → A) → (a : A) → ((hfiber inc a) ⊔ ¬ (hfiber inc a))
fin-img-dec dec inc a = ⊔-rec (λ np → inl np) (λ f → inr (λ np → f (fst np) (snd np))) (finite-lpo (λ k → inc k == a) λ k → dec (inc k) a)

Fin-eq : {n : ℕ} {x y : Fin n} → (fst x == fst y) → x == y
Fin-eq p = pair= p prop-has-all-paths-↓

<-or-≥ : (n m : ℕ) → ((n < m) ⊔ (m ≤ n))
<-or-≥ n m = ⊔-rec (λ p → inr (inl (! p))) (⊔-rec inl (λ l → inr (inr l))) (ℕ-trichotomy n m)

≤-or-> : (n m : ℕ) → ((n ≤ m) ⊔ (m < n))
≤-or-> m n = ⊔-rec (inl ∘ inl) (⊔-fmap inr (idf _)) (ℕ-trichotomy m n)

<-≤-trans : {l m n : ℕ} → (l < m) → (m ≤ n) → (l < n)
<-≤-trans p (inl q) = transport _ q p
<-≤-trans p (inr q) = <-trans p q

≤-<-trans : {l m n : ℕ} → (l ≤ m) → (m < n) → (l < n)
≤-<-trans (inl p) q = transport _ (! p) q
≤-<-trans (inr p) q = <-trans p q

<S≠-to-< : {a b : ℕ} → (a < S b) → (a ≠ b) → (a < b)
<S≠-to-< ltS ne = ⊥-elim (ne idp)
<S≠-to-< (ltSR lt) ne = lt

module _ {n : ℕ} (k : Fin n) where
  private
    degeneracy-aux : (x : Fin (S n)) → ((fst x ≤ fst k) ⊔ (fst k < fst x)) → Fin n
    degeneracy-aux x (inl z) = (fst x) , ≤-<-trans z (snd k)
    degeneracy-aux (.(S (fst k)) , snd) (inr ltS) = k
    degeneracy-aux (.(S _) , snd) (inr (ltSR z)) = _ , (<-cancel-S snd)

    degeneracy-almost-inj-aux : {x y : Fin (S n)} → (fst x ≠ fst k) → (fst y ≠ fst k) →
      (z : ((fst x) ≤ (fst k)) ⊔ ((fst k) < (fst x))) → (w : ((fst y) ≤ (fst k)) ⊔ ((fst k) < (fst y))) →
      (degeneracy-aux x z == degeneracy-aux y w) → x == y

    degeneracy-almost-inj-aux f g (inl z) (inl w) p = ℕ=-to-Fin= (ap fst p)
    degeneracy-almost-inj-aux f g (inl z) (inr ltS) p = ⊥-rec (f (ap fst p))
    degeneracy-almost-inj-aux f g (inl z) (inr (ltSR w)) p = ⊥-rec (<-to-≠ (≤-<-trans z w) (ap fst p))
    degeneracy-almost-inj-aux f g (inr ltS) (inl w) p = ⊥-rec (g (ap fst (! p)))
    degeneracy-almost-inj-aux f g (inr (ltSR z)) (inl w) p = ⊥-rec (<-to-≠ (≤-<-trans w z) (ap fst (! p)))
    degeneracy-almost-inj-aux f g (inr ltS) (inr ltS) p = ℕ=-to-Fin= idp
    degeneracy-almost-inj-aux f g (inr ltS) (inr (ltSR w)) p = ℕ=-to-Fin= (ap S (ap fst p))
    degeneracy-almost-inj-aux f g (inr (ltSR z)) (inr ltS) p = ℕ=-to-Fin= (ap S (ap fst p))
    degeneracy-almost-inj-aux f g (inr (ltSR z)) (inr (ltSR w)) p = ℕ=-to-Fin= (ap S (ap fst p))

  abstract
    degeneracy : (x : Fin (S n)) → Fin n
    degeneracy x = degeneracy-aux x (≤-or-> _ _)

    degeneracy-almost-inj : {x y : Fin (S n)} → (fst x ≠ fst k) → (fst y ≠ fst k) →
      (degeneracy x == degeneracy y) → x == y
    degeneracy-almost-inj f g = degeneracy-almost-inj-aux f g (≤-or-> _ _) (≤-or-> _ _)

Fin-hfiber-dec : {i : ULevel} {X : Type i} {n : ℕ} (dec : has-dec-eq X) → (f : Fin n → X) →
  (x : X) → Dec (hfiber f x)

Fin-hfiber-dec dec f x = ⊔-fmap (idf _) (λ g p → g (fst p) (snd p))
  (finite-lpo (λ z → f z == x) (λ z → dec (f z) x))

Fin-inj-to-surj : (n : ℕ) → (inc : Fin n → Fin n) → (inc-inj : is-inj inc) → (y : Fin n) → hfiber inc y
Fin-inj-to-surj O inc inc-inj y = ⊥-rec (–> Fin-equiv-Empty y)
Fin-inj-to-surj (S n) inc inc-inj y =
  ⊔-rec (λ p → n<Sn , (! p))
        (λ f → ⊔-rec (λ p → case1 p f) (λ g → case2 g f) (Fin-has-dec-eq k n<Sn))
        (Fin-has-dec-eq y k)
  where
    n<Sn = (n , ltS)
    k = inc n<Sn

    case1 : k == n<Sn → (y ≠ k) → hfiber inc y
    case1 p f = Fin-S (fst x') , ℕ=-to-Fin= (ap fst (snd x'))
      where
        inc' : Fin n → Fin n
        inc' x = (fst (inc (Fin-S x))) , <S≠-to-< (snd (inc (Fin-S x))) λ q → <-to-≠ (snd x) (ap fst (inc-inj _ _ (ℕ=-to-Fin= q ∙ ! p)))

        inc-inj' : is-inj inc'
        inc-inj' x x' p = Fin-S-is-inj _ _ (inc-inj _ _ (ℕ=-to-Fin= (ap fst p)))

        y' : Fin n
        y' = (fst y) , (<S≠-to-< (snd y) (λ q → f (ℕ=-to-Fin= q ∙ ! p)))

        x' : hfiber inc' y'
        x' = Fin-inj-to-surj n inc' inc-inj' y'

    case2 : k ≠ n<Sn → (y ≠ k) → hfiber inc y
    case2 f g = Fin-S (fst x') , degeneracy-almost-inj k' (λ q → <-to-≠ (snd (fst x')) (ap fst (inc-inj (Fin-S (fst x')) n<Sn (ℕ=-to-Fin= q))))
                                                            (λ q → g (ℕ=-to-Fin= q)) (snd x')
      where
        k' = (fst k) , (<S≠-to-< (snd k) (λ q → f (ℕ=-to-Fin= q)))

        inc' : Fin n → Fin n
        inc' x = degeneracy k' (inc (Fin-S x))

        inc-inj' : is-inj inc'
        inc-inj' x x' p =
          Fin-S-is-inj _ _ (inc-inj _ _ (degeneracy-almost-inj k' (λ q → <-to-≠ (snd x) (ap fst (inc-inj _ _ (ℕ=-to-Fin= q))))
                                                                  (λ q → <-to-≠ (snd x') (ap fst (inc-inj _ _ (ℕ=-to-Fin= q))))
                                                                  p))

        x' : hfiber inc' (degeneracy k' y)
        x' = Fin-inj-to-surj n inc' inc-inj' ((degeneracy k' y))

Fin-inj-to-equiv : {n : ℕ} → (inc : Fin (S n) → Fin (S n)) → (inc-inj : is-inj inc) → (is-equiv inc)
Fin-inj-to-equiv inc inc-inj =
  contr-map-is-equiv λ x → inhab-prop-is-contr (Fin-inj-to-surj _ inc inc-inj x) ⦃ inj-to-embed ⦃ Fin-is-set ⦄ inc inc-inj x ⦄

Fin-smaller-is-smaller : {m n : ℕ} (l : m < n) (f : Fin m → Fin n) → Σ (Fin n) (λ k → ¬ (hfiber f k))
Fin-smaller-is-smaller {m} {n} l f = ⊔-cancel-r (finite-lpo _ (λ k → ⊔-rec (λ x → inr (λ g → g x)) inl (Fin-hfiber-dec Fin-has-dec-eq f k))) lemma
  where
    lemma : ((k : Fin n) → ¬ (¬ (hfiber f k))) → ⊥
    lemma g = <-to-≠ (snd (g'' (fst k))) (ap fst (snd k))
      where
        g' : (k : Fin n) → (hfiber f k)
        g' k = ⊔-cancel-r (Fin-hfiber-dec Fin-has-dec-eq f k) (g k)

        g'' : Fin n → Fin m
        g'' = fst ∘ g'

        g''-is-inj : is-inj g''
        g''-is-inj y y' p = ! (snd (g' y)) ∙ ap f p ∙ snd (g' y')

        h : Fin n → Fin n
        h k = (fst (g'' k)) , (<-trans (snd (g'' k)) l)

        h-is-inj : is-inj h
        h-is-inj x y p = g''-is-inj _ _ (ℕ=-to-Fin= (ap fst p))

        k : hfiber h (m , l)
        k = Fin-inj-to-surj n h h-is-inj ((m , l))

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


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

module UnbiasedCategory where

open import Agda.Builtin.Equality

module TypedLists where
  data TypedList (index : Set) (type : index -> index -> Set) : index -> index -> Set where
    empty : {a : index} -> TypedList index type a a
    fby : {a b c : index} -> type a b -> TypedList index type b c -> TypedList index type a c
  open TypedList public

  append : forall {index : Set} {type : index -> index -> Set} {a b c : index} ->
    TypedList index type a b -> TypedList index type b c -> TypedList index type a c
  append empty s = s
  append (fby x l) s = fby x (append l s)

  concat : forall {index : Set} {type : index -> index -> Set} {a b : index} ->
    TypedList index (TypedList index type) a b -> TypedList index type a b
  concat empty = empty
  concat (fby l s) = append l (concat s)

  map : forall {index : Set} {p : index -> index -> Set} {q : index -> index -> Set} {a b : index} ->
    (forall {a b : index} -> p a b -> q a b) ->
    TypedList index p a b -> TypedList index q a b
  map transform empty = empty
  map transform (fby x l) = fby (transform x) (map transform l)

  fold : forall {index : Set} {type : index -> index -> Set} {p : index -> index -> Set} {a b : index} ->
    (f : forall {a} {b} {c} -> type a b -> p b c -> p a c) -> (z : forall {a} -> p a a) -> TypedList index type a b -> p a b
  fold f z empty = z
  fold f z (fby x l) = f x (fold f z l)
open TypedLists public

module Equality where
  cong : {A B : Set} {x y : A} -> (f : A -> B) -> (x ≡ y) -> f x ≡ f y
  cong f refl = refl

  app : {A B : Set} {f g : A -> B} -> (f ≡ g) -> (a : A) -> f a ≡ g a
  app {A} {B} {f} {g} refl a = refl

  symm : {A : Set} {x y : A} -> (x ≡ y) -> (y ≡ x)
  symm refl = refl

  infixr 2 _≡⟨_⟩_
  _≡⟨_⟩_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
  _ ≡⟨ refl ⟩ p2 = p2

  infix  3 _∎
  _∎ : {A : Set} (x : A) → x ≡ x
  x ∎ = refl

  postulate
    funext : {A B : Set} {f g : A -> B} -> ({a : A} -> f a ≡ g a) -> (f ≡ g)
open Equality public

record Category : Set where
  field
    object : Set
    hom : object -> object -> Set
    compose : {a b : object} -> TypedList object hom a b -> hom a b
    associativity : {a b : object} -> (l : TypedList object (TypedList object hom) a b) ->
      compose (concat l) ≡ compose (map compose l)
open Category {{...}} public

record CategoryConstructor : Set where
  field
    object : Set
    hom : object -> object -> Set
    _>>_ : {a b c : object} -> hom a b -> hom b c -> hom a c
    id : {a : object} -> hom a a
    left-unital : {a b : object} {f : hom a b} -> (id >> f) ≡ f
    right-unital : {a b : object} {f : hom a b} -> (id >> f) ≡ f
    associative : {a b c d : object} {f : hom a b} {g : hom b c} {h : hom c d} ->
      (f >> g) >> h ≡ f >> (g >> h)
open CategoryConstructor public

mkCategory : CategoryConstructor -> Category
mkCategory record
  { object = object
  ; hom = hom
  ; _>>_ = _>>_
  ; id = id
  ; left-unital = left-unital
  ; right-unital = right-unital
  ; associative = associative
  } = record
  { object = object
  ; hom = hom
  ; compose = byFolding
  ; associativity = associativityTotal
  }
 where
   byFolding : {a b : object} -> TypedList object hom a b -> hom a b
   byFolding = fold _>>_ id

   lemma-fold-append : forall {a b c : object} ->
     (p : TypedList object hom a b) -> (q : TypedList object hom b c) ->
     byFolding (append p q) ≡ byFolding (fby (byFolding p) q)
   lemma-fold-append empty q = symm left-unital
   lemma-fold-append (fby f p) q =
     byFolding (fby f (append p q))
       ≡⟨ refl ⟩
     f >> byFolding (append p q)
       ≡⟨ cong (_>>_ f) (lemma-fold-append p q) ⟩
     f >> byFolding (fby (byFolding p) q)
       ≡⟨ refl ⟩
     f >> (byFolding p >> byFolding q)
       ≡⟨ symm associative ⟩
     byFolding (fby f p) >> byFolding q
       ≡⟨ refl ⟩
     byFolding (fby (byFolding (fby f p)) q) ∎

   associativityTotal : {a b : object}
      (l : TypedList object (TypedList object hom) a b) →
      byFolding (concat l) ≡ byFolding (map byFolding l)
   associativityTotal {a} {a} empty = refl
   associativityTotal {a} {b} (fby l s) =
     byFolding (append l (concat s))
       ≡⟨ lemma-fold-append l (concat s) ⟩
     byFolding (fby (byFolding l) (concat s))
       ≡⟨ refl ⟩
     byFolding l >> byFolding (concat s)
       ≡⟨ cong (_>>_ (byFolding l)) (associativityTotal s) ⟩
     byFolding l >> byFolding (map byFolding s)
       ≡⟨ refl ⟩
     byFolding (fby (byFolding l) (map byFolding s)) ∎

categoryOfSets : Category
categoryOfSets = mkCategory
  ( record
  { object = Set
  ; hom = λ A B -> (A -> B)
  ; _>>_ = λ f g a -> g (f a)
  ; id = λ x -> x
  ; left-unital = refl
  ; right-unital = refl
  ; associative = refl
  })


text:
module L.Data.Bool.Properties where

open import L.Data.Bool.Core
open import L.Base.Id.Core
open import L.Base.Coproduct.Core

!∃tt∧!∃ff : (x : Bool) → (x ≡ ff) + (x ≡ tt)
!∃tt∧!∃ff = if (λ b → (b ≡ ff) + (b ≡ tt)) (inr refl) (inl refl)

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


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

module Tools.Fin where

open import Tools.Nat
open import Tools.Nullary
open import Tools.PropositionalEquality

open import Data.Fin.Properties using (suc-injective)

open import Data.Fin public using (Fin) renaming (zero to x0 ; suc to _+1)

-- Decidability of equality

_≟ⱽ_ : {n : Nat} → (x y : Fin n) → Dec (x ≡ y)
x0 ≟ⱽ x0 = yes refl
x0 ≟ⱽ (y +1) = no (λ ())
(x +1) ≟ⱽ x0 = no (λ ())
(x +1) ≟ⱽ (y +1) = map (cong _+1) suc-injective (x ≟ⱽ y)

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
{-

  - Automatically generate UARel and DUARel instances

-}
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Displayed.Auto where

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

open import Cubical.Displayed.Base
open import Cubical.Displayed.Subst
open import Cubical.Displayed.Morphism

open import Cubical.Displayed.Constant
open import Cubical.Displayed.Function
open import Cubical.Displayed.Generic
open import Cubical.Displayed.Sigma
open import Cubical.Displayed.Unit
open import Cubical.Displayed.Universe

open import Cubical.Data.List.Base
open import Cubical.Data.Nat.Base
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Unit.Base

import Agda.Builtin.Reflection as R
open import Cubical.Reflection.Base

-- Descriptor language

mutual
  data UARelDesc : ∀ {ℓA ℓ≅A} {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) → Typeω where

    generic : ∀ {ℓA} {A : Type ℓA} → UARelDesc (𝒮-generic A)

    univ : ∀ ℓU → UARelDesc (𝒮-Univ ℓU)

    -- Having a special descriptor for non-dependent × helps to avoid
    -- combinatorial explosion. Automation will try to apply this first.
    prod : ∀ {ℓA ℓ≅A ℓB ℓ≅B}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} (dA : UARelDesc 𝒮-A)
      {B : Type ℓB} {𝒮-B : UARel B ℓ≅B} (dB : UARelDesc 𝒮-B)
      → UARelDesc (𝒮-A ×𝒮 𝒮-B)

    sigma : ∀ {ℓA ℓ≅A ℓB ℓ≅B}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} (dA : UARelDesc 𝒮-A)
      {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B} (dB : DUARelDesc 𝒮-A 𝒮ᴰ-B)
      → UARelDesc (∫ 𝒮ᴰ-B)

    param : ∀ {ℓA ℓB ℓ≅B} (A : Type ℓA)
      {B : Type ℓB} {𝒮-B : UARel B ℓ≅B} (dB : UARelDesc 𝒮-B)
      → UARelDesc (A →𝒮 𝒮-B)

    pi : ∀ {ℓA ℓ≅A ℓB ℓ≅B}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} (dA : UARelDesc 𝒮-A)
      {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B} (dB : DUARelDesc 𝒮-A 𝒮ᴰ-B)
      → UARelDesc (𝒮-Π 𝒮-A 𝒮ᴰ-B)

    unit : UARelDesc 𝒮-Unit

  -- Projections from one UARel to another
  data UARelReindex : ∀ {ℓA ℓ≅A ℓC ℓ≅C}
    {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
    {C : Type ℓC} {𝒮-C : UARel C ℓ≅C}
    (f : UARelHom 𝒮-A 𝒮-C)
    → Typeω
    where

    id : ∀ {ℓA ℓ≅A} {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      → UARelReindex (𝒮-id 𝒮-A)

    ∘fst : ∀ {ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B}
      {C : Type ℓC} {𝒮-C : UARel C ℓ≅C}
      {f : UARelHom 𝒮-A 𝒮-C}
      → UARelReindex f
      → UARelReindex (𝒮-∘ f (𝒮-fst {𝒮ᴰ-B = 𝒮ᴰ-B}))

    ∘snd : ∀ {ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : Type ℓB} {𝒮-B : UARel B ℓ≅B}
      {C : Type ℓC} {𝒮-C : UARel C ℓ≅C}
      {f : UARelHom 𝒮-B 𝒮-C}
      → UARelReindex f
      → UARelReindex (𝒮-∘ f (𝒮-snd {𝒮-A = 𝒮-A}))

    ∘app : ∀ {ℓA ℓB ℓ≅B ℓC ℓ≅C}
      {A : Type ℓA}
      {B : Type ℓB} {𝒮-B : UARel B ℓ≅B}
      {C : Type ℓC} {𝒮-C : UARel C ℓ≅C}
      {f : UARelHom 𝒮-B 𝒮-C}
      → UARelReindex f
      → (a : A) → UARelReindex (𝒮-∘ f (𝒮-app a))

  data SubstRelDesc : ∀ {ℓA ℓ≅A ℓB}
    {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
    {B : A → Type ℓB} (𝒮ˢ-B : SubstRel 𝒮-A B) → Typeω
    where

    generic : ∀ {ℓA ℓ≅A ℓB} {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} {B : A → Type ℓB}
      → SubstRelDesc 𝒮-A (𝒮ˢ-generic 𝒮-A B)

    constant : ∀ {ℓA ℓ≅A ℓB}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} {B : Type ℓB}
      → SubstRelDesc 𝒮-A (𝒮ˢ-const 𝒮-A B)

    -- We have an element DUARel over any 𝒮-A with a proejction to a universe
    -- that can be described with UARelReindex
    el : ∀ {ℓA ℓ≅A ℓU} {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {f : UARelHom 𝒮-A (𝒮-Univ ℓU)}
      → UARelReindex f
      → SubstRelDesc 𝒮-A (𝒮ˢ-reindex f (𝒮ˢ-El ℓU))

    prod : ∀ {ℓA ℓ≅A ℓB ℓC}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : A → Type ℓB} {𝒮ˢ-B : SubstRel 𝒮-A B} (dB : SubstRelDesc 𝒮-A 𝒮ˢ-B)
      {C : A → Type ℓC} {𝒮ˢ-C : SubstRel 𝒮-A C} (dC : SubstRelDesc 𝒮-A 𝒮ˢ-C)
      → SubstRelDesc 𝒮-A (𝒮ˢ-B ×𝒮ˢ 𝒮ˢ-C)

    sigma : ∀ {ℓA ℓ≅A ℓB ℓC}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : A → Type ℓB} {𝒮ˢ-B : SubstRel 𝒮-A B} (dB : SubstRelDesc 𝒮-A 𝒮ˢ-B)
      {C : Σ A B → Type ℓC} {𝒮ˢ-C : SubstRel (∫ˢ 𝒮ˢ-B) C} (dC : SubstRelDesc (∫ˢ 𝒮ˢ-B) 𝒮ˢ-C)
      → SubstRelDesc 𝒮-A (𝒮ˢ-Σ 𝒮ˢ-B 𝒮ˢ-C)

    pi : ∀ {ℓA ℓ≅A ℓB ℓC}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : A → Type ℓB} {𝒮ˢ-B : SubstRel 𝒮-A B} (dB : SubstRelDesc 𝒮-A 𝒮ˢ-B)
      {C : Σ A B → Type ℓC} {𝒮ˢ-C : SubstRel (∫ˢ 𝒮ˢ-B) C} (dC : SubstRelDesc (∫ˢ 𝒮ˢ-B) 𝒮ˢ-C)
      → SubstRelDesc 𝒮-A (𝒮ˢ-Π 𝒮ˢ-B 𝒮ˢ-C)

  data DUARelDesc : ∀ {ℓA ℓ≅A ℓB ℓ≅B}
    {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
    {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B) → Typeω
    where

    generic : ∀ {ℓA ℓ≅A ℓB} {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} {B : A → Type ℓB}
      → DUARelDesc 𝒮-A (𝒮ᴰ-generic 𝒮-A B)

    constant : ∀ {ℓA ℓ≅A ℓB ℓ≅B}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : Type ℓB} {𝒮-B : UARel B ℓ≅B}
      → UARelDesc 𝒮-B
      → DUARelDesc 𝒮-A (𝒮ᴰ-const 𝒮-A 𝒮-B)

    el : ∀ {ℓA ℓ≅A ℓU} {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {f : UARelHom 𝒮-A (𝒮-Univ ℓU)}
      → UARelReindex f
      → DUARelDesc 𝒮-A (𝒮ᴰ-reindex f (𝒮ᴰ-El ℓU))

    prod : ∀ {ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B} (dB : DUARelDesc 𝒮-A 𝒮ᴰ-B)
      {C : A → Type ℓC} {𝒮ᴰ-C : DUARel 𝒮-A C ℓ≅C} (dC : DUARelDesc 𝒮-A 𝒮ᴰ-C)
      → DUARelDesc 𝒮-A (𝒮ᴰ-B ×𝒮ᴰ 𝒮ᴰ-C)

    sigma : ∀ {ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B} (dB : DUARelDesc 𝒮-A 𝒮ᴰ-B)
      {C : Σ A B → Type ℓC} {𝒮ᴰ-C : DUARel (∫ 𝒮ᴰ-B) C ℓ≅C} (dC : DUARelDesc (∫ 𝒮ᴰ-B) 𝒮ᴰ-C)
      → DUARelDesc 𝒮-A (𝒮ᴰ-Σ 𝒮ᴰ-B 𝒮ᴰ-C)

    pi : ∀ {ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B} (dB : DUARelDesc 𝒮-A 𝒮ᴰ-B)
      {C : Σ A B → Type ℓC} {𝒮ᴰ-C : DUARel (∫ 𝒮ᴰ-B) C ℓ≅C} (dC : DUARelDesc (∫ 𝒮ᴰ-B) 𝒮ᴰ-C)
      → DUARelDesc 𝒮-A (𝒮ᴰ-Π 𝒮ᴰ-B 𝒮ᴰ-C)

    piˢ : ∀ {ℓA ℓ≅A ℓB ℓC ℓ≅C}
      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
      {B : A → Type ℓB} {𝒮ˢ-B : SubstRel 𝒮-A B} (dB : SubstRelDesc 𝒮-A 𝒮ˢ-B)
      {C : Σ A B → Type ℓC} {𝒮ᴰ-C : DUARel (∫ˢ 𝒮ˢ-B) C ℓ≅C} (dC : DUARelDesc (∫ˢ 𝒮ˢ-B) 𝒮ᴰ-C)
      → DUARelDesc 𝒮-A (𝒮ᴰ-Πˢ 𝒮ˢ-B 𝒮ᴰ-C)

private
  getUARel : ∀ {ℓA ℓ≅A} {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
    → UARelDesc 𝒮-A → UARel A ℓ≅A
  getUARel {𝒮-A = 𝒮-A} _ = 𝒮-A

  getDUARel : ∀ {ℓA ℓ≅A ℓB ℓ≅B}
    {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
    {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B}
    → DUARelDesc 𝒮-A 𝒮ᴰ-B → DUARel 𝒮-A B ℓ≅B
  getDUARel {𝒮ᴰ-B = 𝒮ᴰ-B} _ = 𝒮ᴰ-B

-- Magic number
private
  FUEL = 10000

mutual
  autoUARelDesc : ℕ → R.Term → R.TC Unit
  autoUARelDesc zero hole = R.typeError [ R.strErr "Out of fuel" ]
  autoUARelDesc (suc n) hole =
    tryUniv <|> tryProd <|> trySigma <|> tryParam <|> tryPi <|> tryUnit <|> useGeneric
    where
    tryUniv : R.TC Unit
    tryUniv = R.unify (R.con (quote UARelDesc.univ) [ varg R.unknown ]) hole

    tryBinary : R.Name → R.TC Unit
    tryBinary name =
      newMeta R.unknown >>= λ hole₁ →
      newMeta R.unknown >>= λ hole₂ →
      R.unify (R.con name (hole₁ v∷ hole₂ v∷ [])) hole >>
      autoUARelDesc n hole₁ >>
      autoDUARelDesc n hole₂

    tryParam : R.TC Unit
    tryParam =
      newMeta R.unknown >>= λ paramTy →
      newMeta R.unknown >>= λ hole₁ →
      R.unify (R.con (quote UARelDesc.param) (paramTy v∷ hole₁ v∷ [])) hole >>
      autoUARelDesc n hole₁

    tryProd = tryBinary (quote UARelDesc.prod)
    trySigma = tryBinary (quote UARelDesc.sigma)
    tryPi = tryBinary (quote UARelDesc.pi)

    tryUnit : R.TC Unit
    tryUnit = R.unify (R.con (quote UARelDesc.unit) []) hole

    useGeneric : R.TC Unit
    useGeneric = R.unify (R.con (quote UARelDesc.generic) []) hole

  autoUARelReindex : ℕ → R.Term → R.TC Unit
  autoUARelReindex zero hole = R.typeError [ R.strErr "Out of fuel" ]
  autoUARelReindex (suc n) hole =
    tryId <|> tryFst <|> trySnd <|> tryApp
    where
    tryId : R.TC Unit
    tryId = R.unify (R.con (quote UARelReindex.id) []) hole

    tryUnary : R.Name → R.TC Unit
    tryUnary name =
      newMeta R.unknown >>= λ hole₁ →
      R.unify (R.con name [ varg hole₁ ]) hole >>
      autoUARelReindex n hole₁

    tryFst = tryUnary (quote UARelReindex.∘fst)
    trySnd = tryUnary (quote UARelReindex.∘snd)

    tryApp : R.TC Unit
    tryApp =
      newMeta R.unknown >>= λ hole₁ →
      newMeta R.unknown >>= λ param →
      R.unify (R.con (quote UARelReindex.∘app) (hole₁ v∷ param v∷ [])) hole >>
      autoUARelReindex n hole₁

  autoSubstRelDesc : ℕ → R.Term → R.TC Unit
  autoSubstRelDesc zero hole = R.typeError [ R.strErr "Out of fuel" ]
  autoSubstRelDesc (suc n) hole =
    tryConstant <|> tryEl <|> tryProd <|> trySigma <|> tryPi <|> useGeneric
    where
    tryConstant : R.TC Unit
    tryConstant =
      R.unify (R.con (quote SubstRelDesc.constant) []) hole

    tryEl : R.TC Unit
    tryEl =
      newMeta R.unknown >>= λ hole₁ →
      R.unify (R.con (quote SubstRelDesc.el) [ varg hole₁ ]) hole >>
      autoUARelReindex n hole₁

    tryBinary : R.Name → R.TC Unit
    tryBinary name =
      newMeta R.unknown >>= λ hole₁ →
      newMeta R.unknown >>= λ hole₂ →
      R.unify (R.con name (hole₁ v∷ hole₂ v∷ [])) hole >>
      autoSubstRelDesc n hole₁ >>
      autoSubstRelDesc n hole₂

    tryProd = tryBinary (quote SubstRelDesc.prod)
    trySigma = tryBinary (quote SubstRelDesc.sigma)
    tryPi = tryBinary (quote SubstRelDesc.pi)

    useGeneric : R.TC Unit
    useGeneric = R.unify (R.con (quote SubstRelDesc.generic) []) hole

  autoDUARelDesc : ℕ → R.Term → R.TC Unit
  autoDUARelDesc zero hole = R.typeError [ R.strErr "Out of fuel" ]
  autoDUARelDesc (suc n) hole =
    tryConstant <|> tryEl <|> tryProd <|> trySigma <|> tryPiˢ <|> tryPi <|> useGeneric
    where
    tryConstant : R.TC Unit
    tryConstant =
      newMeta R.unknown >>= λ hole₁ →
      R.unify (R.con (quote DUARelDesc.constant) [ varg hole₁ ]) hole >>
      autoUARelDesc n hole₁

    tryEl : R.TC Unit
    tryEl =
      newMeta R.unknown >>= λ hole₁ →
      R.unify (R.con (quote DUARelDesc.el) [ varg hole₁ ]) hole >>
      autoUARelReindex n hole₁

    tryBinary : R.Name → R.TC Unit
    tryBinary name =
      newMeta R.unknown >>= λ hole₁ →
      newMeta R.unknown >>= λ hole₂ →
      R.unify (R.con name (hole₁ v∷ hole₂ v∷ [])) hole >>
      autoDUARelDesc n hole₁ >>
      autoDUARelDesc n hole₂

    tryProd = tryBinary (quote DUARelDesc.prod)
    trySigma = tryBinary (quote DUARelDesc.sigma)
    tryPi = tryBinary (quote DUARelDesc.pi)

    tryPiˢ : R.TC Unit
    tryPiˢ =
      newMeta R.unknown >>= λ hole₁ →
      newMeta R.unknown >>= λ hole₂ →
      R.unify (R.con (quote DUARelDesc.piˢ) (hole₁ v∷ hole₂ v∷ [])) hole >>
      autoSubstRelDesc n hole₁ >>
      autoDUARelDesc n hole₂

    useGeneric : R.TC Unit
    useGeneric = R.unify (R.con (quote DUARelDesc.generic) []) hole

module DisplayedAutoMacro where
  autoUARel : ∀ {ℓA} (A : Type ℓA) → ℕ → R.Term → R.TC Unit
  autoUARel A n hole =
    R.quoteTC A >>= λ `A` →
    newMeta R.unknown >>= λ desc →
    makeAuxiliaryDef "autoUA"
      (R.def (quote UARel) (`A` v∷ R.unknown v∷ []))
      (R.def (quote getUARel) [ varg desc ])
      >>= λ uaTerm →
    R.unify hole uaTerm >>
    autoUARelDesc n desc

  autoDUARel : ∀ {ℓA ℓ≅A ℓB} {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) (B : A → Type ℓB)
    → ℕ → R.Term → R.TC Unit
  autoDUARel 𝒮-A B n hole =
    R.quoteTC 𝒮-A >>= λ `𝒮-A` →
    R.quoteTC B >>= λ `B` →
    newMeta R.unknown >>= λ desc →
    makeAuxiliaryDef "autoDUA"
      (R.def (quote DUARel) (`𝒮-A` v∷ `B` v∷ R.unknown v∷ []))
      (R.def (quote getDUARel) [ varg desc ])
      >>= λ duaTerm →
    R.unify hole duaTerm >>
    autoDUARelDesc n desc

macro
  autoUARel : ∀ {ℓA} (A : Type ℓA) → R.Term → R.TC Unit
  autoUARel A = DisplayedAutoMacro.autoUARel A FUEL

  autoDUARel : ∀ {ℓA ℓ≅A ℓB} {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) (B : A → Type ℓB)
    → R.Term → R.TC Unit
  autoDUARel 𝒮-A B = DisplayedAutoMacro.autoDUARel 𝒮-A B FUEL

private
  module Example (A : Type) (a₀ : A) where

    example0 : DUARel (autoUARel Type) (λ X → X → A × X) ℓ-zero
    example0 = autoDUARel _ _

    example0' : {X Y : Type} (e : X ≃ Y)
      (f : X → A × X) (g : Y → A × Y)
      → (∀ x → (f x .fst ≡ g (e .fst x) .fst) × (e .fst (f x .snd) ≡ g (e .fst x) .snd))
      → PathP (λ i → ua e i → A × ua e i) f g
    example0' e f g = example0 .DUARel.uaᴰ f e g .fst

    -- An example where a DUARel is parameterized over a pair of types

    example1 : DUARel (autoUARel (Type × Type)) (λ (X , Z) → X → Z) ℓ-zero
    example1 = autoDUARel _ _

    example1' : {X Y : Type} (e : X ≃ Y) {Z W : Type} (h : Z ≃ W)
      (f : X → Z) (g : Y → W)
      → (∀ x → h .fst (f x) ≡ g (e .fst x))
      → PathP (λ i → ua e i → ua h i) f g
    example1' e h f g = example1 .DUARel.uaᴰ f (e , h) g .fst

    -- An example where a DUARel is parameterized over a family of types

    example2 : DUARel (autoUARel (A → Type)) (λ B → B a₀) ℓ-zero
    example2 = autoDUARel _ _

    example2' : {B C : A → Type} (e : (a : A) → B a ≃ C a)
      (b : B a₀) (c : C a₀)
      → e a₀ .fst b ≡ c
      → PathP (λ i → ua (e a₀) i) b c
    example2' e b c = example2 .DUARel.uaᴰ b e c .fst

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --cubical --safe #-}

module Diatonic where

open import Data.Bool           using (Bool; false; true; if_then_else_; _∧_)
open import Data.Empty          using (⊥)
open import Data.Fin            using (Fin; toℕ; #_; _≟_) renaming (zero to fz; suc to fs)
open import Data.Integer        using (ℤ; +_; -[1+_]; _+_)
open import Data.Integer.DivMod using (_modℕ_)
open import Data.Nat            using (ℕ; zero; suc; _∸_) renaming (_+_ to _+ℕ_; _≡ᵇ_ to _==_)
open import Data.Nat.DivMod     using (_mod_)
open import Data.Unit           using (⊤)
open import Data.Vec            using (Vec; []; _∷_; head; foldl; take; reverse; lookup; updateAt)

open import Function            using (_∘_)

open import Interval            using (Upi; maj3; min3)
open import Pitch               using (Pitch; s7; PC; pitchToClass)

data Mode : Set where
  major : Mode
  minor : Mode

DiatonicDegree : Set
DiatonicDegree = Fin s7

infix 4 _≡ᵈ_
_≡ᵈ_ : DiatonicDegree → DiatonicDegree → Bool
d ≡ᵈ e = toℕ d == toℕ e
-- round down
pitchClass→Degree : Mode → PC → DiatonicDegree

pitchClass→Degree major (fz)                                                        = # 0
pitchClass→Degree major ((fs fz))                                                   = # 0
pitchClass→Degree major ((fs (fs fz)))                                              = # 1
pitchClass→Degree major ((fs (fs (fs fz))))                                         = # 1
pitchClass→Degree major ((fs (fs (fs (fs fz)))))                                    = # 2
pitchClass→Degree major ((fs (fs (fs (fs (fs fz))))))                               = # 3
pitchClass→Degree major ((fs (fs (fs (fs (fs (fs fz)))))))                          = # 3
pitchClass→Degree major ((fs (fs (fs (fs (fs (fs (fs fz))))))))                     = # 4
pitchClass→Degree major ((fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))                = # 4
pitchClass→Degree major ((fs (fs (fs (fs (fs (fs (fs (fs (fs fz))))))))))           = # 5
pitchClass→Degree major ((fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))))      = # 5
pitchClass→Degree major ((fs (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))))) = # 6

pitchClass→Degree minor (fz)                                                        = # 0
pitchClass→Degree minor ((fs fz))                                                   = # 0
pitchClass→Degree minor ((fs (fs fz)))                                              = # 1
pitchClass→Degree minor ((fs (fs (fs fz))))                                         = # 2
pitchClass→Degree minor ((fs (fs (fs (fs fz)))))                                    = # 2
pitchClass→Degree minor ((fs (fs (fs (fs (fs fz))))))                               = # 3
pitchClass→Degree minor ((fs (fs (fs (fs (fs (fs fz)))))))                          = # 3
pitchClass→Degree minor ((fs (fs (fs (fs (fs (fs (fs fz))))))))                     = # 4
pitchClass→Degree minor ((fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))                = # 5
pitchClass→Degree minor ((fs (fs (fs (fs (fs (fs (fs (fs (fs fz))))))))))           = # 5
pitchClass→Degree minor ((fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))))      = # 6
pitchClass→Degree minor ((fs (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))))) = # 6

degree→PC : Mode → DiatonicDegree → PC

degree→PC major fz                               = (# 0)
degree→PC major (fs fz)                          = (# 2)
degree→PC major (fs (fs fz))                     = (# 4)
degree→PC major (fs (fs (fs fz)))                = (# 5)
degree→PC major (fs (fs (fs (fs fz))))           = (# 7)
degree→PC major (fs (fs (fs (fs (fs fz)))))      = (# 9)
degree→PC major (fs (fs (fs (fs (fs (fs fz)))))) = (# 11)

degree→PC minor fz                               = (# 0)
degree→PC minor (fs fz)                          = (# 2)
degree→PC minor (fs (fs fz))                     = (# 3)
degree→PC minor (fs (fs (fs fz)))                = (# 5)
degree→PC minor (fs (fs (fs (fs fz))))           = (# 7)
degree→PC minor (fs (fs (fs (fs (fs fz)))))      = (# 8)
degree→PC minor (fs (fs (fs (fs (fs (fs fz)))))) = (# 10)

pitch→DegreeCMajor : Pitch → DiatonicDegree
pitch→DegreeCMajor = pitchClass→Degree major ∘ pitchToClass

d1 d2 d3 d4 d5 d6 d7 : DiatonicDegree
d1 = # 0
d2 = # 1
d3 = # 2
d4 = # 3
d5 = # 4
d6 = # 5
d7 = # 6

data Accidental : Set where
  ♭3 : ℕ → Accidental -- 3+n flats
  𝄫  : Accidental
  ♭  : Accidental
  ♮  : Accidental
  ♯  : Accidental
  𝄪  : Accidental
  ♯3 : ℕ → Accidental -- 3+n sharps

-- pitch class letter name with accidental
data PCL : Set where
  A : Accidental → PCL
  B : Accidental → PCL
  C : Accidental → PCL
  D : Accidental → PCL
  E : Accidental → PCL
  F : Accidental → PCL
  G : Accidental → PCL

-- Accidental modifier.
accMod : Accidental → ℤ
accMod (♭3 n) = -[1+ (n +ℕ 2) ]
accMod 𝄫      = -[1+ 1 ]
accMod ♭      = -[1+ 0 ]
accMod ♮      = + 0
accMod ♯      = + 1
accMod 𝄪      = + 2
accMod (♯3 n) = + (n +ℕ 3)

flatten : (a : Accidental) → Accidental
flatten (♭3 n)       = ♭3 (suc n)
flatten 𝄫            = ♭3 zero
flatten ♭            = 𝄫
flatten ♮            = ♭
flatten ♯            = ♮
flatten 𝄪            = ♯
flatten (♯3 zero)    = 𝄪
flatten (♯3 (suc n)) = ♯3 n

sharpen : Accidental → Accidental
sharpen (♭3 (suc n)) = ♭3 n
sharpen (♭3 zero)    = 𝄫
sharpen 𝄫            = ♭
sharpen ♭            = ♮
sharpen ♮            = ♯
sharpen ♯            = 𝄪
sharpen 𝄪            = ♯3 zero
sharpen (♯3 n)       = ♯3 (suc n)

-- Convert raw PCL letter to ℕ (in range [0,11]); C normalized to 0
letter→ℕ : PCL → ℕ
letter→ℕ (A _) = 9
letter→ℕ (B _) = 11
letter→ℕ (C _) = 0
letter→ℕ (D _) = 2
letter→ℕ (E _) = 4
letter→ℕ (F _) = 5
letter→ℕ (G _) = 7

accidental : PCL → Accidental
accidental (A x) = x
accidental (B x) = x
accidental (C x) = x
accidental (D x) = x
accidental (E x) = x
accidental (F x) = x
accidental (G x) = x

modifyAccidental : (Accidental → Accidental) → PCL →  PCL
modifyAccidental f (A x) = A (f x)
modifyAccidental f (B x) = B (f x)
modifyAccidental f (C x) = C (f x)
modifyAccidental f (D x) = D (f x)
modifyAccidental f (E x) = E (f x)
modifyAccidental f (F x) = F (f x)
modifyAccidental f (G x) = G (f x)

-- Convert PCL to PC with C♮ normalized to 0.
pclToC : PCL → PC
pclToC pc = ((((+ (letter→ℕ pc)) + accMod (accidental pc)) modℕ 12) mod 12)

data Key : Set where
  key : PCL → Mode → Key

keyMode : Key → Mode
keyMode (key _ mode) = mode

data Step : Set where
  half  : Step
  whole : Step

stepUp : Step → PCL → PCL

stepUp half  (A x) = B (flatten x)
stepUp half  (B x) = C x
stepUp half  (C x) = D (flatten x)
stepUp half  (D x) = E (flatten x)
stepUp half  (E x) = F x
stepUp half  (F x) = G (flatten x)
stepUp half  (G x) = A (flatten x)

stepUp whole (A x) = B x
stepUp whole (B x) = C (sharpen x)
stepUp whole (C x) = D x
stepUp whole (D x) = E x
stepUp whole (E x) = F (sharpen x)
stepUp whole (F x) = G x
stepUp whole (G x) = A x

scaleSteps : Mode → Vec Step s7
scaleSteps major = whole ∷ whole ∷ half ∷ whole ∷ whole ∷ whole ∷ half ∷ []
scaleSteps minor = whole ∷ half ∷ whole ∷ whole ∷ half ∷ whole ∷ whole ∷ []

scaleNotes : Key → Vec PCL s7
scaleNotes (key pc m) =
  let f : {n : ℕ} → Vec PCL (suc n) → Step → Vec PCL (suc (suc n))
      f pcs step = stepUp step (head pcs) ∷ pcs
  in reverse (foldl (Vec PCL ∘ suc) f (pc ∷ []) (take 6 (scaleSteps m)))

data Root : Set where
  I   : Root
  II  : Root
  III : Root
  IV  : Root
  V   : Root
  VI  : Root
  VII : Root

data Quality : Set where
  maj : Quality
  min : Quality
  aug : Quality
  dim : Quality

_dd+_ : DiatonicDegree → ℕ → DiatonicDegree
d dd+ n = (toℕ d +ℕ n) mod s7

thirdUp : DiatonicDegree → DiatonicDegree
thirdUp d = d dd+ 2

data Triad : Set where
  triad : Root → Quality → Triad

root→DiatonicDegree : Root → DiatonicDegree
root→DiatonicDegree I   = d1
root→DiatonicDegree II  = d2
root→DiatonicDegree III = d3
root→DiatonicDegree IV  = d4
root→DiatonicDegree V   = d5
root→DiatonicDegree VI  = d6
root→DiatonicDegree VII = d7

diatonicDegree→Root : DiatonicDegree → Root
diatonicDegree→Root fz                               = I
diatonicDegree→Root (fs fz)                          = II
diatonicDegree→Root (fs (fs fz))                     = III
diatonicDegree→Root (fs (fs (fs fz)))                = IV
diatonicDegree→Root (fs (fs (fs (fs fz))))           = V
diatonicDegree→Root (fs (fs (fs (fs (fs fz)))))      = VI
diatonicDegree→Root (fs (fs (fs (fs (fs (fs fz)))))) = VII

rootQuality : Mode → Root → Quality

rootQuality major I   = maj
rootQuality major II  = min
rootQuality major III = min
rootQuality major IV  = maj
rootQuality major V   = maj
rootQuality major VI  = min
rootQuality major VII = dim

rootQuality minor I   = min
rootQuality minor II  = dim
rootQuality minor III = maj
rootQuality minor IV  = min
rootQuality minor V   = min
rootQuality minor VI  = maj
rootQuality minor VII = maj

root→PC : Key → Root → PC
root→PC (key _ mode) = degree→PC mode ∘ root→DiatonicDegree

diatonicDegree→PCL : Key → DiatonicDegree → PCL
diatonicDegree→PCL k dd = lookup (scaleNotes k) dd

root→PCL : Key → Root → PCL
root→PCL k = diatonicDegree→PCL k ∘ root→DiatonicDegree

-- Lower interval is first.
triadQuality : Upi → Upi → Quality
triadQuality i1 i2 =
  if      (i1 == maj3) ∧ (i2 == min3) then maj
  else if (i1 == min3) ∧ (i2 == maj3) then min
  else if (i1 == min3) ∧ (i2 == min3) then dim
  else if (i1 == maj3) ∧ (i2 == maj3) then aug
  else maj -- should not happen

makeTriad : Mode → Root → Triad
makeTriad m r =
  let d1 = root→DiatonicDegree r
      d2 = thirdUp d1
      d3 = thirdUp d2
      p1 = degree→PC m d1
      p2 = degree→PC m d2
      p3 = degree→PC m d3
      i1 = toℕ p2 ∸ toℕ p1 -- TODO: See if want to use ℤ
      i2 = toℕ p3 ∸ toℕ p2
  in triad r (triadQuality i1 i2)

diatonic7thNotes : Key → Root → Vec PCL 4
diatonic7thNotes k root =
  let d1 = root→DiatonicDegree root
      d2 = thirdUp d1
      d3 = thirdUp d2
      d4 = thirdUp d3
      ns = scaleNotes k
  in lookup ns d1 ∷ lookup ns d2 ∷ lookup ns d3 ∷ lookup ns d4 ∷ []

triadNotes : Key → Root → Vec PCL 3
triadNotes k = take 3 ∘ diatonic7thNotes k

_V/_ : Key → Root → Vec PCL 3
k V/ r = triadNotes (key (root→PCL k r) major) V

_V⁷/_ : Key → Root → Vec PCL 4
k V⁷/ r = diatonic7thNotes (key (root→PCL k r) major) V

_viiᵒ⁷/_ : Key → Root → Vec PCL 4
k viiᵒ⁷/ r = updateAt (# 3) (modifyAccidental flatten) (diatonic7thNotes (key (root→PCL k r) major) VII)

----------

a1 = triadNotes (key (G ♭) major) III
a2 = diatonic7thNotes (key (G ♯) major) V
a3 = diatonic7thNotes (key (E ♮) major) V
a4 = diatonic7thNotes (key (B ♭) major) VI
a5 = scaleNotes (key (G ♯) major)
a6 = scaleNotes (key (G ♭) major)
a7 = scaleNotes (key (B ♮) minor)
a8 = (key (G ♮) major) V/ V
a9 = (key (B ♭) major) V⁷/ II

a10 = (key (F ♯) minor) viiᵒ⁷/ III

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module MJSF.Examples.DynamicDispatch where

open import Prelude
open import Data.Star
open import Data.Bool
open import Data.List
open import Data.Integer
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All hiding (lookup)
open import Data.Product hiding (Σ)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

k : ℕ
k = 10

open import MJSF.Syntax k
open import ScopesFrames.ScopesFrames k Ty

{-
  class Int {

      public int x;

      public int get() {
          System.out.println("never");
          return x;
      }

      public int set(Int y) {
          x = y.x;
          return this.get();
      }
  }

  class IntInc extends Int {

      public int get() {
          return x + 1;
      }

      public int inc(Int y) {
          Int x = new Int();
          x.x = y.x + 1;
          return set(x);
      }
  }

  class Main {
      public static void main(String[] args) {
          Int y = new Int();
          y.x = 18;
          IntInc x = new IntInc();
          x.x = 0;

          // should print 20 because we use the get() of IntInc
          System.out.println(x.inc(y));
      }
  }
-}

Root : Scope
Root = # 0

Int : Scope
Int = # 1

IntInc : Scope
IntInc = # 2

-- Main class omitted; main() function is given below, as child scope
-- of the root scope.

classes : List Ty
classes = (cᵗ Root Int ∷
           cᵗ Root IntInc ∷ [])

Int-methods Int-fields : List Ty
Int-fields =
  {- x -} vᵗ int
  ∷ []
Int-methods =
  {- Int.get -} mᵗ [] int ∷
  {- Int.set -} mᵗ (ref Int ∷ []) int ∷
  []

IntInc-methods IntInc-fields : List Ty
IntInc-methods =
  -- {- IntInc.get -} mᵗ [] int ∷
  {- IntInc.inc -} mᵗ (ref Int ∷ []) int ∷
  []
IntInc-fields = []

g : Graph
-- root scope
g zero =
  classes , []

-- class scope of Int class
g (suc zero) =
  (Int-methods ++ Int-fields) , zero ∷ []
-- class scope of IntInc class
g (suc (suc zero)) =
  (IntInc-methods ++ IntInc-fields) , zero ∷ # 1 ∷ []

-- scope of Int.get method; 3
g (suc (suc (suc zero))) =
  [] , Int ∷ []
-- scope of Int.set method; 4
g (suc (suc (suc (suc zero)))) =
  vᵗ (ref Int) ∷ [] , Int ∷ []

-- scope of IntInc.get method; 5
g (suc (suc (suc (suc (suc zero))))) =
  [] , IntInc ∷ []
-- scope of IntInc.inc method; 6
g (suc (suc (suc (suc (suc (suc zero)))))) =
  vᵗ (ref Int) ∷ [] , IntInc ∷ []

-- local variable scope of Int.inc method; 7
g (suc (suc (suc (suc (suc (suc (suc zero))))))) =
  vᵗ (ref Int) ∷ [] , # 6 ∷ []

-- x local variable scope of Main.main method; 8
g (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) =
  vᵗ (ref Int) ∷ [] , Root ∷ []

-- y local variable scope of Main.main method; 9
g (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) =
  vᵗ (ref IntInc) ∷ [] , # 8 ∷ []

g (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc ()))))))))))

open SyntaxG g
open UsesGraph g

IntImpl : Class Root Int
IntImpl =
  class0 {ms = Int-methods} {fs = Int-fields}
    -- methods
    (#m' (meth (# 3)
               (body ε
                     (var (path ((here refl) ∷ []) (there (there (here refl))))))) ∷
    (#m' (meth (# 4)
               (body ( asgn (path ((here refl) ∷ [])
                                  (there (there (here refl))))
                            (get (var (path [] (here refl)))
                                 (path [] (there (there (here refl)))))
                     ◅ ε)
                     (call (this [] (here refl))
                           (path [] (here refl))
                           [])))) ∷ [])
    -- fields
    ((#v' tt) ∷ [])
    -- overrides
    []

IntIncImpl : Class Root IntInc
IntIncImpl =
  class1 {ms = IntInc-methods} {fs = IntInc-fields}
    -- path to parent
    (path [] (here refl))
    -- methods
    (#m'
      (meth
        (# 6)
        (body
        ( loc (# 7) (ref Int)
        ◅ asgn (path [] (here refl))
               (new (path ((here refl) ∷ ((here refl) ∷ ((here refl) ∷ [])))
                             (here refl)))
        ◅ set (var (path [] (here refl)))
                  (path [] (there (there (here refl))))
                  (iop Data.Integer._+_
                       (get (var (path ((here refl) ∷ []) (here refl)))
                            (path [] (there (there (here refl)))))
                       (num (+ 1)))
        ◅ ε)
      (call (this (here refl ∷ []) (here refl))
            (path (there (here refl) ∷ []) (there (here refl)))
            ((var (path [] (here refl))) ∷ [])))) ∷
    [])
    -- fields
    []
    -- overrides
    (#m'
     (path ((there (here refl)) ∷ []) (here refl) ,
     (meth
       (# 5)
       (body
         ε
         (iop Data.Integer._+_
              (var (path ((here refl) ∷ ((there (here refl)) ∷ []))
                         (there (there (here refl)))))
                   (num (+ 1)))))) ∷ [])

main : Body Root int
main =
  body
    ( (loc (# 8) (ref Int))
    ◅ asgn (path [] (here refl))
           (new (path (here refl ∷ []) (here refl)))
    ◅ set (var (path [] (here refl)))
          (path [] (there (there (here refl))))
          (num (+ 18))
    ◅ loc (# 9) (ref IntInc)
    ◅ asgn (path [] (here refl))
           (new (path (here refl ∷ here refl ∷ [])
                      (there (here refl))))
    ◅ set (var (path [] (here refl)))
          (path (there (here refl) ∷ []) (there (there (here refl))))
          (num (+ 0))
    ◅ ε)

    (call (var (path [] (here refl)))
          (path [] (here refl))
          (var (path ((here refl) ∷ []) (here refl)) ∷ []))

p : Program Root int
p = program classes
            (#c' (IntImpl , Int , obj Int ⦃ refl ⦄) ∷
            (#c' (IntIncImpl , Int , (super ⦃ refl ⦄ (obj Int ⦃ refl ⦄)))) ∷
            []) main

open import MJSF.Semantics
open Semantics _ g
open import MJSF.Values
open ValuesG _ g

test : p ⇓⟨ 100 ⟩ (λ v → v ≡ num (+ 20) )
test = refl


text:
-- Andreas, 2016-12-31, issue #2374
-- Use hiding info to disambiguate overloaded projections.

-- {-# OPTIONS -v tc.lhs.split:40 #-}

postulate A B : Set

module M where

  record R : Set₂ where
    field
      F : Set₁

module Order1 where
  open M.R
  open M.R {{...}}

  test : M.R
  F test = Set

  inst : M.R
  F {{inst}} = Set

module Order2 where
  open M.R {{...}}
  open M.R

  test : M.R
  F test = Set

  inst : M.R
  F {{inst}} = Set

module N (A : Set) where

  record R : Set₂ where
    field
      F : Set₁

module Par1 where
  open N.R {A = A}
  module RB = N.R {A = B}; open RB {{...}}

  test : N.R A
  F test = Set

  inst : N.R B
  F {{inst}} = Set

module Par2 where
  module RA = N.R {A = A}; open RA {{...}}
  open N.R {A = B}

  test : N.R B
  F test = Set

  inst : N.R A
  F {{inst}} = Set

-- All should be accepted.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.Setoid directly.
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.Vec.Relation.Equality.Setoid
  {a ℓ} (S : Setoid a ℓ) where

open import Data.Vec.Relation.Binary.Equality.Setoid S public

{-# WARNING_ON_IMPORT
"Data.Vec.Relation.Equality.Setoid was deprecated in v1.0.
Use Data.Vec.Relation.Binary.Equality.Setoid instead."
#-}