text:
{-# OPTIONS --safe --experimental-lossy-unification #-}

module Cubical.Algebra.Group.EilenbergMacLane.WedgeConnectivity where

open import Cubical.Algebra.Group.EilenbergMacLane.Base
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Algebra.Group.Base
open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec; elim to trElim)
open import Cubical.HITs.EilenbergMacLane1
open import Cubical.Algebra.AbGroup.Base
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)
open import Cubical.Data.Nat
open import Cubical.HITs.Susp

{-
This file contains a direct construction of the wedge connectivity lemma for EM
spaces. This direct construction gives nicer reductions and computes better than
the more general theorem. The main results are in the module "wedgeConEM" at the
end of this file.
-}

private
  variable ℓ ℓ' ℓ'' : Level

-- One of the base cases, stated separately to avoid termination issues
  wedgeConFun' : (G : AbGroup ℓ) (H : AbGroup ℓ') (n : ℕ)
              → {A : EM-raw G (suc n) → EM-raw H (suc zero) → Type ℓ''}
              → ((x : _) (y : _) → isOfHLevel (suc n + suc zero) (A x y))
              → (f : (x : _) → A ptEM-raw x)
              → (g : (x : _) → A x ptEM-raw)
              → f ptEM-raw ≡ g ptEM-raw
              → (x : _) (y : _) → A x y
  wedgeConFun'ᵣ : (G : AbGroup ℓ) (H : AbGroup ℓ') (n : ℕ)
              → {A : EM-raw G (suc n) → EM-raw H (suc zero) → Type ℓ''}
              → (hLev : ((x : _) (y : _) → isOfHLevel (suc n + suc zero) (A x y)))
              → (f : (x : _) → A ptEM-raw x)
              → (g : (x : _) → A x ptEM-raw)
              → (p : f ptEM-raw ≡ g ptEM-raw)
              → (x : _) → wedgeConFun' G H n hLev f g p x ptEM-raw ≡ g x
  wedgeConFun' G H zero {A = A} hlev f g p =
    elimSet _ (λ _ → isSetΠ λ _ → hlev _ _) f mainpath
    where
    I→A : (x : fst G) → (i : I) → A (emloop x i) embase
    I→A x i =
      hcomp (λ k → λ {(i = i0) → p (~ k) ; (i = i1) → p (~ k)})
            (g (emloop x i))

    SquareP2 : (x : _) (z : _)
      → SquareP (λ i j → A (emloop x i) (emloop z j))
          (cong f (emloop z)) (cong f (emloop z))
          (λ i → I→A x i) λ i → I→A x i
    SquareP2 x z =
      toPathP (isOfHLevelPathP' 1 (λ _ _ → hlev _ _ _ _) _ _ _ _)

    CubeP2 : (x : _) (g h : _)
      → PathP (λ k → PathP (λ j → PathP (λ i → A (emloop x i) (emcomp g h j k))
              (f (emcomp g h j k)) (f (emcomp g h j k)))
              (λ i → SquareP2 x g i k) λ i → SquareP2 x ((snd (AbGroup→Group H) GroupStr.· g) h) i k)
              (λ _ i → I→A x i) λ j i → SquareP2 x h i j
    CubeP2 x g h = toPathP (isOfHLevelPathP' 1 (isOfHLevelPathP 2 (hlev _ _) _ _) _ _ _ _)

    mainpath : (x : _) → PathP (λ i → (y : EM₁ (AbGroup→Group H)) → A (emloop x i) y) f f
    mainpath x i embase = I→A x i
    mainpath x i (emloop z j) = SquareP2 x z i j
    mainpath x i (emcomp g h j k) = CubeP2 x g h k j i
    mainpath x i (emsquash y z p q r s j k' l) = mega i j k' l
      where
      mega :
        PathP (λ i → PathP (λ j → PathP (λ k →
          PathP (λ l → A (emloop x i) (emsquash y z p q r s j k l))
                    (mainpath x i y)
                    (mainpath x i z))
                    (λ l → mainpath x i (p l))
                     λ l → mainpath x i (q l))
                    (λ k l → mainpath x i (r k l))
                     λ k l → mainpath x i (s k l))
                    (λ j mainpath l → f (emsquash y z p q r s j mainpath l))
                     λ j mainpath l → f (emsquash y z p q r s j mainpath l)
      mega =
        toPathP (isOfHLevelPathP' 1
          (isOfHLevelPathP 2 (isOfHLevelPathP 2 (hlev _ _) _ _) _ _) _ _ _ _)
  wedgeConFun' G H (suc n) {A = A} hLev f g p north y = f y
  wedgeConFun' G H (suc n) {A = A} hLev f g p south y = subst (λ x → A x y) (merid ptEM-raw) (f y)
  wedgeConFun' G H (suc n) {A = A} hLev f g p (merid a i) y = mainₗ a y i
    module _ where
    llem₁ : g south ≡ subst (λ x₁ → A x₁ ptEM-raw) (merid ptEM-raw) (f ptEM-raw)
    llem₁ = (λ i → transp (λ j → A (merid ptEM-raw (j ∨ ~ i)) ptEM-raw) (~ i) (g (merid ptEM-raw (~ i))))
          ∙ cong (subst (λ x₁ → A x₁ ptEM-raw) (merid ptEM-raw)) (sym p)

    llem₁' :
      Square
       (λ i → transp (λ j → A (merid ptEM-raw (i ∨ j)) ptEM-raw) i (g (merid ptEM-raw i))) refl
       (cong (subst (λ x → A x ptEM-raw) (merid ptEM-raw)) (sym p)) llem₁
    llem₁' i j =
      hcomp (λ k → λ { (i = i0) → transp (λ z → A (merid ptEM-raw (j ∨ z)) ptEM-raw) j
                                            (g (merid ptEM-raw j))
                      ; (i = i1) → subst (λ x₁ → A x₁ ptEM-raw) (merid ptEM-raw) (p (~ k))
                      ; (j = i0) → (subst (λ x → A x ptEM-raw) (merid ptEM-raw)) (p (~ k ∨ ~ i))})
            (transp (λ k → A (merid ptEM-raw (k ∨ ~ i ∧ j)) ptEM-raw) (~ i ∧ j) (g (merid ptEM-raw (~ i ∧ j))))

    llem₂ : (λ i₁ → transp (λ j → A (merid ptEM-raw (i₁ ∧ j)) ptEM-raw) (~ i₁) (f ptEM-raw))
        ≡ (λ i₁ →  hcomp (λ k → λ { (i₁ = i0) → p (~ k) ; (i₁ = i1) → llem₁ k })
                          (g (merid ptEM-raw i₁)))
    llem₂ i j =
      hcomp (λ k → λ { (i = i0) → transp (λ j₁ → A (merid ptEM-raw (j ∧ j₁)) ptEM-raw) (~ j) (p (~ k))
                      ; (j = i0) → p (~ k)
                      ; (j = i1) → llem₁' k i})
        (transp (λ k → A (merid ptEM-raw ((i ∨ k) ∧ j)) ptEM-raw) (i ∨ ~ j) (g (merid ptEM-raw (i ∧ j))))

    mainₗ : (a : _) (y : _)
      → PathP (λ i → A (merid a i) y) (f y) (subst (λ x → A x y) (merid ptEM-raw) (f y))
    mainₗ =
      wedgeConFun' G H n
        (λ _ _ → isOfHLevelPathP' (suc (n + 1)) (hLev _ _) _ _)
        (λ x i → transp (λ j → A (merid ptEM-raw (i ∧ j)) x) (~ i) (f x))
        (λ x i → hcomp (λ k → λ { (i = i0) → p (~ k)
                                 ; (i = i1) → llem₁ k})
                        (g (merid x i)))
        llem₂

    mainP : (y : _)
      → mainₗ y ptEM-raw
      ≡ λ i → hcomp (λ k → λ { (i = i0) → p (~ k)
                               ; (i = i1) → llem₁ k})
                      (g (merid y i))
    mainP y =
      wedgeConFun'ᵣ G H n
        (λ _ _ → isOfHLevelPathP' (suc (n + 1)) (hLev _ _) _ _)
        (λ x i → transp (λ j → A (merid ptEM-raw (i ∧ j)) x) (~ i) (f x))
        (λ x i → hcomp (λ k → λ { (i = i0) → p (~ k)
                                 ; (i = i1) → llem₁ k})
                        (g (merid x i)))
        llem₂ y
  wedgeConFun'ᵣ G H zero {A = A} hLev f g p =
    elimProp _ (λ _ → hLev _ _ _ _) p
  wedgeConFun'ᵣ G H (suc n) {A = A} hLev f g p north = p
  wedgeConFun'ᵣ G H (suc n) {A = A} hLev f g p south = sym (llem₁ G H n hLev f g p ptEM-raw i0 ptEM-raw)
  wedgeConFun'ᵣ G H (suc n) {A = A} hLev f g p (merid a i) k = P k i
    where
    llem : _
    llem i j =
      hcomp (λ k → λ { (i = i1) → g (merid a j)
                      ; (j = i0) → p (i ∨ ~ k)
                      ; (j = i1) → llem₁ G H n hLev f g p ptEM-raw i0 ptEM-raw (~ i ∧ k)})
        (g (merid a j))

    P : PathP (λ k → PathP (λ i → A (merid a i) ptEM-raw)
              (p k) (llem₁ G H n hLev f g p ptEM-raw i0 ptEM-raw (~ k)))
              (λ i → mainₗ G H n hLev f g p a i ptEM-raw a ptEM-raw i) λ i → g (merid a i)
    P = mainP G H n hLev f g p a i0 ptEM-raw a ◁ llem

-- Here, the actual stuff gets proved. However an additional natural number is stuck into the context
-- to convince the termination checker
private
  wedgeConFun : (G : AbGroup ℓ) (H : AbGroup ℓ')
                 (k n m : ℕ) → (n + m ≡ k) → {A : EM-raw G (suc n) → EM-raw H (suc m) → Type ℓ''}
              → ((x : _) (y : _) → isOfHLevel (suc n + suc m) (A x y))
              → (f : (x : _) → A ptEM-raw x)
              → (g : (x : _) → A x ptEM-raw)
              → f ptEM-raw ≡ g ptEM-raw
              → (x : _) (y : _) → A x y
  wedgeconLeft : (G : AbGroup ℓ) (H : AbGroup ℓ') (k n m : ℕ) (P : n + m ≡ k)
                 {A : EM-raw G (suc n) → EM-raw H (suc m) → Type ℓ''}
              → (hLev : ((x : _) (y : _) → isOfHLevel (suc n + suc m) (A x y)))
              → (f : (x : _) → A ptEM-raw x)
              → (g : (x : _) → A x ptEM-raw)
              → (p : f ptEM-raw ≡ g ptEM-raw)
               → (x : _) → wedgeConFun G H k n m P hLev f g p ptEM-raw x ≡ f x
  wedgeconRight : (G : AbGroup ℓ) (H : AbGroup ℓ')
                 (k n m : ℕ) (P : n + m ≡ k) {A : EM-raw G (suc n) → EM-raw H (suc m) → Type ℓ''}
              → (hLev : ((x : _) (y : _) → isOfHLevel (suc n + suc m) (A x y)))
              → (f : (x : _) → A ptEM-raw x)
              → (g : (x : _) → A x ptEM-raw)
              → (p : f ptEM-raw ≡ g ptEM-raw)
               → (x : _) → wedgeConFun G H k n m P hLev f g p x ptEM-raw ≡ g x
  wedgeConFun G H k n zero P {A = A} hLev f g p = wedgeConFun' G H n hLev f g p
  wedgeConFun G H k zero (suc m) P {A = A} hLev f g p x y =
    wedgeConFun' H G (suc m) {A = λ x y → A y x}
      (λ x y → subst (λ n → isOfHLevel (2 + n) (A y x)) (+-comm 1 m) (hLev y x))
      g f (sym p) y x
  wedgeConFun G H l (suc n) (suc m) P {A = A} hlev f g p north y = f y
  wedgeConFun G H l (suc n) (suc m) P {A = A} hlev f g p south y = subst (λ x → A x y) (merid ptEM-raw) (f y)
  wedgeConFun G H zero (suc n) (suc m) P {A = A} hlev f g p (merid a i) y = ⊥-path i
    where
    ⊥-path : PathP (λ i → A (merid a i) y) (f y) (subst (λ x → A x y) (merid ptEM-raw) (f y))
    ⊥-path = ⊥-rec (snotz P)
  wedgeConFun G H (suc l) (suc n) (suc m) P {A = A} hlev f g p (merid a i) y = mmain a y i
    module _ where
    llem₃ : g south ≡ (subst (λ x → A x ptEM-raw) (merid ptEM-raw) (f ptEM-raw))
    llem₃ = ((λ i → transp (λ j → A (merid ptEM-raw (~ i ∨ j)) ptEM-raw) (~ i) (g (merid ptEM-raw (~ i)))))
          ∙ cong (subst (λ x → A x ptEM-raw) (merid ptEM-raw)) (sym p)

    llem₃' :
      Square
        (λ i → transp (λ j → A (merid ptEM-raw (~ i ∨ j)) ptEM-raw) (~ i) (g (merid ptEM-raw (~ i))))
        (refl {x = subst (λ x → A x ptEM-raw) (merid ptEM-raw) (f ptEM-raw)})
        llem₃
        ((cong (transport (λ z → A (merid ptEM-raw z) ptEM-raw)) (sym p)))
    llem₃' i j =
      hcomp (λ k → λ { (i = i0) → transp (λ j₁ → A (merid ptEM-raw (~ j ∨ j₁)) ptEM-raw) (~ j) (g (merid ptEM-raw (~ j)))
                      ; (i = i1) → subst (λ x → A x ptEM-raw) (merid ptEM-raw) (p (~ k))
                      ; (j = i1) → cong (transport (λ z → A (merid ptEM-raw z) ptEM-raw)) (sym p) (i ∧ k)})
             (transp (λ j₁ → A (merid ptEM-raw ((~ j ∧ ~ i) ∨ j₁)) ptEM-raw) (~ j ∧ ~ i) (g (merid ptEM-raw (~ j ∧ ~ i))))

    llem₄ : (λ i₁ → transp (λ j → A (merid ptEM-raw (j ∧ i₁)) ptEM-raw) (~ i₁) (f ptEM-raw))
        ≡ (λ i₁ → hcomp (λ k → λ { (i₁ = i0) → p (~ k) ; (i₁ = i1) → llem₃ k })
           (g (merid ptEM-raw i₁)))
    llem₄ i j =
      hcomp (λ k → λ { (i = i0) → transp (λ z → A (merid ptEM-raw (z ∧ j)) ptEM-raw) (~ j) (p (~ k))
                      ; (j = i0) → p (~ k)
                      ; (j = i1) → llem₃' k (~ i)})
            (transp (λ z → A (merid ptEM-raw ((i ∨ z) ∧ j)) ptEM-raw) (i ∨ ~ j) (g (merid ptEM-raw (i ∧ j))))

    mmain : (a : _) (y : _)
          → PathP (λ i → A (merid a i) y) (f y)
                   (subst (λ x → A x y) (merid ptEM-raw) (f y))
    mmain =
      wedgeConFun G H l n (suc m) (cong predℕ P)
        (λ _ _ → isOfHLevelPathP' (suc (n + (suc (suc m)))) (hlev _ _) _ _)
        (λ x i → transp (λ j → A (merid ptEM-raw (j ∧ i)) x) (~ i) (f x))
        (λ y i → hcomp (λ k → λ { (i = i0) → p (~ k)
                                  ; (i = i1) → llem₃ k})
                       (g (merid y i)))
        llem₄

    mainR : (x : _) → mmain x ptEM-raw
                    ≡ λ i → hcomp (λ k → λ { (i = i0) → p (~ k)
                                             ; (i = i1) → llem₃ k})
                                               (g (merid x i))
    mainR x =
      wedgeconRight G H l n (suc m) (cong predℕ P)
        (λ _ _ → isOfHLevelPathP' (suc (n + (suc (suc m)))) (hlev _ _) _ _)
        (λ x i → transp (λ j → A (merid ptEM-raw (j ∧ i)) x) (~ i) (f x))
        (λ y i → hcomp (λ k → λ { (i = i0) → p (~ k)
                                  ; (i = i1) → llem₃ k})
                       (g (merid y i)))
        llem₄ x
  wedgeconLeft G H k zero zero P {A = A} hLev f g p _ = refl
  wedgeconLeft G H k (suc n) zero P {A = A} hLev f g p _ = refl
  wedgeconLeft G H k zero (suc m) P {A = A} hLev f g p x =
    wedgeConFun'ᵣ H G (suc m)
        (λ x₁ y →
           subst (λ n → (x₂ y₁ : A y x₁) → isOfHLevel (suc n) (x₂ ≡ y₁))
           (+-comm 1 m) (hLev y x₁))
        g f (λ i → p (~ i)) x
  wedgeconLeft G H k (suc n) (suc m) P {A = A} hLev f g p _ = refl
  wedgeconRight G H k n zero P {A = A} hLev f g p = wedgeConFun'ᵣ G H n hLev f g p
  wedgeconRight G H k zero (suc m) P {A = A} hLev f g p _ = refl
  wedgeconRight G H zero (suc n) (suc m) P {A = A} hLev f g p x = ⊥-rec (snotz P)
  wedgeconRight G H l (suc n) (suc m) P {A = A} hLev f g p north = p
  wedgeconRight G H l (suc n) (suc m) P {A = A} hLev f g p south =
    sym (llem₃ G H _ n m refl hLev f g p ptEM-raw i0 ptEM-raw)
  wedgeconRight G H (suc l) (suc n) (suc m) P {A = A} hLev f g p (merid a i) k =
    help k i
    where
    llem : _
    llem i j =
      hcomp (λ k → λ { (i = i1) → g (merid a j)
                      ; (j = i0) → p (i ∨ ~ k)
                      ; (j = i1) → llem₃ G H l n m P hLev f g p ptEM-raw i0 ptEM-raw (~ i ∧ k)})
            (g (merid a j))

    help : PathP (λ k → PathP (λ i → A (merid a i) ptEM-raw)
                 (p k) (llem₃ G H l n m P hLev f g p ptEM-raw i0 ptEM-raw (~ k)))
                 (λ i → mmain G H l n m P hLev f g p a i north a north i) (cong g (merid a))
    help = mainR G H l n m P hLev f g p a i0 ptEM-raw a ◁ llem

module wedgeConEM (G : AbGroup ℓ) (H : AbGroup ℓ') (n m : ℕ)
                  {A : EM-raw G (suc n) → EM-raw H (suc m) → Type ℓ''}
                  (hLev : ((x : _) (y : _) → isOfHLevel (suc n + suc m) (A x y)))
                  (f : (x : _) → A ptEM-raw x)
                  (g : (x : _) → A x ptEM-raw)
                  (p : f ptEM-raw ≡ g ptEM-raw) where
  fun : (x : EM-raw G (suc n)) (y : EM-raw H (suc m)) → A x y
  fun = wedgeConFun G H (n + m) n m refl hLev f g p

  left : (x : EM-raw H (suc m)) → fun ptEM-raw x ≡ f x
  left = wedgeconLeft G H (n + m) n m refl hLev f g p

  right : (x : EM-raw G (suc n)) → fun x ptEM-raw ≡ g x
  right = wedgeconRight G H (n + m) n m refl hLev f g p

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2014-10-23
-- If you must, you can split on a shadowed hidden var...

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

f : {n n : ℕ}  → Set₁
f = Set
  where
  g : {n n : ℕ} → Set → Set
  g _ = {!.n!}

ext: agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.Block      as Block
import      LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert as QuorumCert
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Hash
open import Util.Prelude

module LibraBFT.Impl.Consensus.LedgerRecoveryData where

postulate -- TODO-2: compareX, sortBy, findIndex, deleteAt, find
  compareX  : (Epoch × Round) → (Epoch × Round) → Ordering
  sortBy    : (Block → Block → Ordering) → List Block → List Block
  findIndex : (Block → Bool) → List Block → Maybe ℕ
  deleteAt  : ℕ → List Block → List Block
  find      : (QuorumCert → Bool) → List QuorumCert -> Maybe QuorumCert

findRoot : List Block → List QuorumCert → LedgerRecoveryData
         → Either ErrLog (RootInfo × List Block × List QuorumCert)
findRoot blocks0 quorumCerts0 (LedgerRecoveryData∙new storageLedger) = do
  (rootId , (blocks1 , quorumCerts)) ←
        if storageLedger ^∙ liEndsEpoch
        then (do
          genesis       ← Block.makeGenesisBlockFromLedgerInfo storageLedger
          let genesisQC = QuorumCert.certificateForGenesisFromLedgerInfo storageLedger (genesis ^∙ bId)
          pure (genesis ^∙ bId , (genesis ∷ blocks0 , genesisQC ∷ quorumCerts0)))
        else
          pure (storageLedger ^∙ liConsensusBlockId , (blocks0 , quorumCerts0))
  let sorter : Block → Block → Ordering
      sorter bl br = compareX (bl ^∙ bEpoch , bl ^∙ bRound) (br ^∙ bEpoch , br ^∙ bRound)
      sortedBlocks = sortBy sorter blocks1
  rootIdx          ← maybeS
        (findIndex (λ x → x ^∙ bId == rootId) sortedBlocks)
        (Left fakeErr) -- ["unable to find root", show rootId]
        (pure ∘ id)
  rootBlock         ← maybeS
        (sortedBlocks !? rootIdx)
        (Left fakeErr) -- ["sortedBlocks !? rootIdx"]
        (pure ∘ id)
  let blocks       = deleteAt rootIdx sortedBlocks
  rootQuorumCert   ← maybeS
        (find (λ x → x ^∙ qcCertifiedBlock ∙ biId == rootBlock ^∙ bId) quorumCerts)
        (Left fakeErr) -- ["No QC found for root", show rootId]
        (pure ∘ id)
  rootLedgerInfo   ← maybeS
        (find (λ x → x ^∙ qcCommitInfo ∙ biId == rootBlock ^∙ bId) quorumCerts)
        (Left fakeErr) -- ["No LI found for root", show rootId]
        (pure ∘ id)
  pure (RootInfo∙new rootBlock rootQuorumCert rootLedgerInfo , blocks , quorumCerts)
{-
 where
  here t = "LedgerRecoveryData":"findRoot":t
  deleteAt idx xs = lft ++ tail rgt where (lft, rgt) = splitAt idx xs
  tail = \case [] -> []; (_:xs) -> xs
-}


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

-- a categorical (i.e. non-skeletal) version of Lawvere Theory,
-- as per https://ncatlab.org/nlab/show/Lawvere+theory

module Categories.Theory.Lawvere where

open import Data.Nat using (ℕ)
open import Data.Product using (Σ; _,_)
open import Level

open import Categories.Category.Cartesian.Structure
open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Instance.Setoids
open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-CartesianCategory)
open import Categories.Category.Product
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Cartesian
open import Categories.Functor.Cartesian.Properties
import Categories.Morphism as Mor
open import Categories.NaturalTransformation using (NaturalTransformation)

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level

record FiniteProduct (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    T : CartesianCategory o ℓ e

  module T = CartesianCategory T
  open Mor T.U

  field
    generic : T.Obj

  field
    obj-iso-to-generic-power : ∀ x → Σ ℕ (λ n → x ≅ T.power generic n)

record LT-Hom (T₁ : FiniteProduct o ℓ e) (T₂ : FiniteProduct o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module T₁ = FiniteProduct T₁
    module T₂ = FiniteProduct T₂

  field
    cartF : CartesianF T₁.T T₂.T

  module cartF = CartesianF cartF

LT-id : {A : FiniteProduct o ℓ e} → LT-Hom A A
LT-id = record { cartF = idF-CartesianF _ }

LT-∘ : {A : FiniteProduct o ℓ e} {B : FiniteProduct o′ ℓ′ e′} {C : FiniteProduct o″ ℓ″ e″} →
       LT-Hom B C → LT-Hom A B → LT-Hom A C
LT-∘ G H = record { cartF = ∘-CartesianF (cartF G) (cartF H) }
  where open LT-Hom

record T-Algebra (FP : FiniteProduct o ℓ e) : Set (o ⊔ ℓ ⊔ e ⊔ suc (ℓ′ ⊔ e′)) where
  private
    module FP = FiniteProduct FP
  field
    cartF : CartesianF FP.T (Setoids-CartesianCategory ℓ′ e′)

  module cartF = CartesianF cartF

  mod : Functor FP.T.U (Setoids ℓ′ e′)
  mod = cartF.F

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

module Data.Maybe.Base where

open import Level

data Maybe (A : Type a) : Type a where
  nothing  : Maybe A
  just     : A → Maybe A

maybe : {B : Maybe A → Type b} → B nothing → ((x : A) → B (just x)) → (x : Maybe A) → B x
maybe b f nothing = b
maybe b f (just x) = f x

mapMaybe : (A → B) → Maybe A → Maybe B
mapMaybe f nothing  = nothing
mapMaybe f (just x) = just (f x)

infixr 2 _|?_
_|?_ : Maybe A → A → A
nothing |? x = x
just x  |? _ = x

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

-- First and second species counterpoint
module Counterpoint where

open import Data.Bool using (Bool; true; false; if_then_else_; _∨_; _∧_; not)
open import Data.Fin using (Fin; #_)
open import Data.Integer using (+_)
open import Data.List using (List; []; _∷_; mapMaybe; map; zip; _++_; concatMap)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (suc; _+_; _<ᵇ_; compare; _∸_; ℕ; zero) renaming (_≡ᵇ_ to _==_)
open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.Vec using ([]; _∷_; Vec; lookup; drop; reverse)

open import Function using (_∘_)

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Music
open import Note
open import Pitch
open import Interval
open import Util using (pairs)

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

-- First species

-- Beginning must be the 1st, 5th, or 8th
data BeginningError : Set where
  not158   : PitchInterval → BeginningError

checkBeginning : PitchInterval → Maybe BeginningError
checkBeginning pi@(_ , i) =
  if ((i == per1) ∨ (i == per5) ∨ (i == per8))
  then nothing
  else just (not158 pi)

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

-- Intervals in middle bars must be consonant and non-unison
data IntervalError : Set where
  dissonant : Upi   → IntervalError
  unison    : Pitch → IntervalError

intervalCheck : PitchInterval → Maybe IntervalError
intervalCheck (p , i) with isConsonant i | isUnison i
intervalCheck (p , i) | false | _    = just (dissonant i)
intervalCheck (p , i) | _     | true = just (unison p)
intervalCheck (p , i) | _     | _    = nothing

checkIntervals : List PitchInterval → List IntervalError
checkIntervals = mapMaybe intervalCheck

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

-- Perfect intervals must not approached by parallel or similar motion
data Motion : Set where
  contrary : Motion
  parallel : Motion
  similar  : Motion
  oblique  : Motion

motion : PitchInterval → PitchInterval → Motion
motion (p , i) (q , j) =
  let p' = p + i; q' = q + j
  in if i == j then parallel
     else (if (p == q) ∨ (p' == q') then oblique
           else (if p <ᵇ q then (if p' <ᵇ q' then similar  else contrary)
                 else           (if p' <ᵇ q' then contrary else similar)))

data MotionError : Set where
  parallel : PitchInterval → PitchInterval → MotionError
  similar  : PitchInterval → PitchInterval → MotionError

motionCheck : PitchInterval → PitchInterval → Maybe MotionError
motionCheck i1 i2 with motion i1 i2 | isPerfect (proj₂ i2)
motionCheck i1 i2 | contrary | _     = nothing
motionCheck i1 i2 | oblique  | _     = nothing
motionCheck i1 i2 | parallel | false = nothing
motionCheck i1 i2 | parallel | true  = just (parallel i1 i2)
motionCheck i1 i2 | similar  | false = nothing
motionCheck i1 i2 | similar  | true  = just (similar i1 i2)

checkMotion : List PitchInterval → List MotionError
checkMotion = mapMaybe (uncurry motionCheck) ∘ pairs

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

-- Ending must be the 1st or 8th approached by a cadence
data EndingError : Set where
  not18    : PitchInterval → EndingError
  not27    : PitchInterval → EndingError
  tooShort : List PitchInterval → EndingError

endingCheck : PitchInterval → PitchInterval → Maybe EndingError
endingCheck pi1@(p , i) (q , 0)  =
  if ((p + 1 == q) ∧ (i == min3)) then nothing else just (not27 pi1)
endingCheck pi1@(p , i) (q , 12) =
  if ((q + 2 == p) ∧ (i == maj6) ∨ (p + 1 == q) ∧ (i == min10))
  then nothing
  else just (not27 pi1)
endingCheck pi1               pi2                     =
  just (not18 pi2)

checkEnding : List PitchInterval → PitchInterval → Maybe EndingError
checkEnding []       _ = just (tooShort [])
checkEnding (p ∷ []) q = endingCheck p q
checkEnding (p ∷ ps) q = checkEnding ps q

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

-- Correct first species counterpoint
record FirstSpecies : Set where
  constructor firstSpecies
  field
    firstBar    : PitchInterval
    middleBars  : List PitchInterval
    lastBar     : PitchInterval
    beginningOk : checkBeginning firstBar ≡ nothing
    intervalsOk : checkIntervals middleBars ≡ []
    motionOk    : checkMotion (firstBar ∷ middleBars) ≡ []
                  -- no need to include the last bar,
                  -- since endingOK guarantees contrary motion in the ending
    endingOk    : checkEnding middleBars lastBar ≡ nothing

------------------------------------------------
-- Second Species

PitchInterval2 : Set
PitchInterval2 = Pitch × Upi × Upi

strongBeat : PitchInterval2 → PitchInterval
strongBeat (p , i , _) = p , i

weakBeat : PitchInterval2 → PitchInterval
weakBeat (p , _ , i) = p , i

expandPitchInterval2 : PitchInterval2 → List PitchInterval
expandPitchInterval2 (p , i , j) = (p , i) ∷ (p , j) ∷ []

expandPitchIntervals2 : List PitchInterval2 → List PitchInterval
expandPitchIntervals2 = concatMap expandPitchInterval2

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

-- Beginning must be the 5th or 8th
data BeginningError2 : Set where
  not58    : PitchInterval → BeginningError2

checkBeginning2 : PitchInterval → Maybe BeginningError2
checkBeginning2 pi@(_ , i) =
  if ((i == per5) ∨ (i == per8))
  then nothing
  else just (not58 pi)

checkEnding2 : List PitchInterval2 → PitchInterval → Maybe EndingError
checkEnding2 []           _   = just (tooShort [])
checkEnding2 (p ∷ [])     q   = endingCheck (weakBeat p) q
checkEnding2 (_ ∷ p ∷ ps) q   = checkEnding2 (p ∷ ps) q

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

-- Strong beats must be consonant and non-unison
checkStrongBeats : List PitchInterval2 → List IntervalError
checkStrongBeats = checkIntervals ∘ map strongBeat

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

-- Weak beats may be dissonant or unison
checkWeakBeat : PitchInterval2 → Pitch → Maybe IntervalError
checkWeakBeat (p , i , j) q with isConsonant j | isUnison j
checkWeakBeat (p , i , j) q | false | _ =
  if isPassingTone (secondPitch (p , i)) (secondPitch (p , j)) q
  then nothing
  else just (dissonant j)
checkWeakBeat (p , i , j) q | _ | true =
  if isOppositeStep (secondPitch (p , i)) (secondPitch (p , j)) q
  then nothing
  else just (unison p)
checkWeakBeat (p , i , j) q | _ | _    =
  nothing

checkWeakBeats : List PitchInterval2 → Pitch → List IntervalError
checkWeakBeats []            p = []
checkWeakBeats pis@(_ ∷ qis) p =
  mapMaybe (uncurry checkWeakBeat)
           (zip pis
                (map (λ {(q , i , j) → proj₂ (pitchIntervalToPitchPair (q , i))}) qis ++ (p ∷ [])))

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

-- Perfect intervals on strong beats must not be approached by parallel or similar motion
checkMotion2 : List PitchInterval → List MotionError
checkMotion2 []           = []
checkMotion2 (_ ∷ [])     = []
checkMotion2 (p ∷ q ∷ ps) = checkMotion (p ∷ q ∷ []) ++ checkMotion2 ps

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

-- Correct second species counterpoint
record SecondSpecies : Set where
  constructor secondSpecies
  field
    firstBar      : PitchInterval -- require counterpont to start with a rest, which is preferred
    middleBars    : List PitchInterval2
    lastBar       : PitchInterval -- require counterpoint to end with only a single whole note, which is preferred
    beginningOk   : checkBeginning2 firstBar ≡ nothing
    strongBeatsOk : checkStrongBeats middleBars ≡ []
    weakBeatsOk   : checkWeakBeats middleBars (secondPitch lastBar) ≡ []
    motionOk      : checkMotion2 (firstBar ∷ (expandPitchIntervals2 middleBars)) ≡ []
    endingOk      : checkEnding2 middleBars lastBar ≡ nothing

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Unit

postulate
  A : Set
  a : A
  f : {X : Set} → X → A
  g : {X : Set} → A → X
  rew-fg : {X : Set} (a : A) → f (g {X} a) ≡ a
{-# REWRITE rew-fg #-}

test : f tt ≡ a
test = refl


text:
module VecFlip where

open import AgdaPrelude

goodNil : Vec Nat Zero
goodNil = Nil Nat

badNil : Vec Zero Nat
badNil = Nil Nat

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


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

open import HoTT

module groups.HomSequence where

infix 15 _⊣|ᴳ
infixr 10 _→⟨_⟩ᴳ_

data HomSequence {i} : (G : Group i) (H : Group i) → Type (lsucc i) where
  _⊣|ᴳ : (G : Group i) → HomSequence G G
  _→⟨_⟩ᴳ_ : (G : Group i) {H K : Group i}
    → (G →ᴳ H) → HomSequence H K
    → HomSequence G K

HomSeq-++ : ∀ {i} {G H K : Group i}
  → HomSequence G H → HomSequence H K → HomSequence G K
HomSeq-++ (_ ⊣|ᴳ) seq = seq
HomSeq-++ (_ →⟨ φ ⟩ᴳ seq₁) seq₂ = _ →⟨ φ ⟩ᴳ HomSeq-++ seq₁ seq₂

HomSeq-snoc : ∀ {i} {G H K : Group i}
  → HomSequence G H → (H →ᴳ K) → HomSequence G K
HomSeq-snoc seq φ = HomSeq-++ seq (_ →⟨ φ ⟩ᴳ _ ⊣|ᴳ)

{- maps between two hom sequences -}

infix 15 _↓|ᴳ
infixr 10 _↓⟨_⟩ᴳ_

data HomSeqMap {i₀ i₁} : {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
  → HomSequence G₀ H₀ → HomSequence G₁ H₁
  → (G₀ →ᴳ G₁) → (H₀ →ᴳ H₁) → Type (lsucc (lmax i₀ i₁)) where
  _↓|ᴳ : {G₀ : Group i₀} {G₁ : Group i₁} (ξ : G₀ →ᴳ G₁) → HomSeqMap (G₀ ⊣|ᴳ) (G₁ ⊣|ᴳ) ξ ξ
  _↓⟨_⟩ᴳ_ : {G₀ H₀ K₀ : Group i₀} {G₁ H₁ K₁ : Group i₁}
    → {φ : G₀ →ᴳ H₀} {seq₀ : HomSequence H₀ K₀}
    → {ψ : G₁ →ᴳ H₁} {seq₁ : HomSequence H₁ K₁}
    → (ξG : G₀ →ᴳ G₁) {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
    → CommSquareᴳ φ ψ ξG ξH
    → HomSeqMap seq₀ seq₁ ξH ξK
    → HomSeqMap (G₀ →⟨ φ ⟩ᴳ seq₀) (G₁ →⟨ ψ ⟩ᴳ seq₁) ξG ξK

HomSeqMap-snoc : ∀ {i₀ i₁} {G₀ H₀ K₀ : Group i₀} {G₁ H₁ K₁ : Group i₁}
  {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
  {φ₀ : H₀ →ᴳ K₀} {φ₁ : H₁ →ᴳ K₁}
  {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
  → HomSeqMap seq₀ seq₁ ξG ξH
  → CommSquareᴳ φ₀ φ₁ ξH ξK
  → HomSeqMap (HomSeq-snoc seq₀ φ₀) (HomSeq-snoc seq₁ φ₁) ξG ξK
HomSeqMap-snoc (ξG ↓|ᴳ) □ = ξG ↓⟨ □ ⟩ᴳ _ ↓|ᴳ
HomSeqMap-snoc (ξG ↓⟨ □₁ ⟩ᴳ seq) □₂ = ξG ↓⟨ □₁ ⟩ᴳ HomSeqMap-snoc seq □₂

{- equivalences between two hom sequences -}

is-seqᴳ-equiv : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
  {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
  {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
  → HomSeqMap seq₀ seq₁ ξG ξH
  → Type (lmax i₀ i₁)
is-seqᴳ-equiv (ξ ↓|ᴳ) = is-equiv (GroupHom.f ξ)
is-seqᴳ-equiv (ξ ↓⟨ _ ⟩ᴳ seq) = is-equiv (GroupHom.f ξ) × is-seqᴳ-equiv seq

is-seqᴳ-equiv-snoc : ∀ {i₀ i₁} {G₀ H₀ K₀ : Group i₀} {G₁ H₁ K₁ : Group i₁}
  {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
  {φ₀ : H₀ →ᴳ K₀} {φ₁ : H₁ →ᴳ K₁}
  {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
  {seq-map : HomSeqMap seq₀ seq₁ ξG ξH}
  {cs : CommSquareᴳ φ₀ φ₁ ξH ξK}
  → is-seqᴳ-equiv seq-map → is-equiv (GroupHom.f ξK)
  → is-seqᴳ-equiv (HomSeqMap-snoc seq-map cs)
is-seqᴳ-equiv-snoc {seq-map = ξG ↓|ᴳ} ξG-is-equiv ξH-is-equiv = ξG-is-equiv , ξH-is-equiv
is-seqᴳ-equiv-snoc {seq-map = ξG ↓⟨ _ ⟩ᴳ seq} (ξG-is-equiv , seq-is-equiv) ξH-is-equiv =
  ξG-is-equiv , is-seqᴳ-equiv-snoc seq-is-equiv ξH-is-equiv

private
  is-seqᴳ-equiv-head : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
    {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    {seq-map : HomSeqMap seq₀ seq₁ ξG ξH}
    → is-seqᴳ-equiv seq-map → is-equiv (GroupHom.f ξG)
  is-seqᴳ-equiv-head {seq-map = ξ ↓|ᴳ} ise = ise
  is-seqᴳ-equiv-head {seq-map = ξ ↓⟨ _ ⟩ᴳ _} ise = fst ise

  is-seqᴳ-equiv-last : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
    {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    {seq-map : HomSeqMap seq₀ seq₁ ξG ξH}
    → is-seqᴳ-equiv seq-map → is-equiv (GroupHom.f ξH)
  is-seqᴳ-equiv-last {seq-map = ξ ↓|ᴳ} ise = ise
  is-seqᴳ-equiv-last {seq-map = _ ↓⟨ _ ⟩ᴳ rest} (_ , rest-ise) = is-seqᴳ-equiv-last rest-ise

module is-seqᴳ-equiv {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
  {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
  {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
  {seq-map : HomSeqMap seq₀ seq₁ ξG ξH}
  (seq-map-is-equiv : is-seqᴳ-equiv seq-map) where

  head = is-seqᴳ-equiv-head seq-map-is-equiv
  last = is-seqᴳ-equiv-last seq-map-is-equiv

HomSeqEquiv : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
  (seq₀ : HomSequence G₀ H₀) (seq₁ : HomSequence G₁ H₁)
  (ξG : G₀ →ᴳ G₁) (ξH : H₀ →ᴳ H₁) → Type (lsucc (lmax i₀ i₁))
HomSeqEquiv seq₀ seq₁ ξG ξH = Σ (HomSeqMap seq₀ seq₁ ξG ξH) is-seqᴳ-equiv

HomSeqEquiv-inverse : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
  {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
  {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
  (equiv : HomSeqEquiv seq₀ seq₁ ξG ξH)
  → HomSeqEquiv seq₁ seq₀
      (GroupIso.g-hom (ξG , is-seqᴳ-equiv-head (snd equiv)))
      (GroupIso.g-hom (ξH , is-seqᴳ-equiv-last (snd equiv)))
HomSeqEquiv-inverse ((ξ ↓|ᴳ) , ξ-ise) =
  (GroupIso.g-hom (ξ , ξ-ise) ↓|ᴳ) , is-equiv-inverse ξ-ise
HomSeqEquiv-inverse ((ξ ↓⟨ □ ⟩ᴳ rest) , (ξ-ise , rest-ise)) =
  (GroupIso.g-hom (ξ , ξ-ise)
    ↓⟨ CommSquareᴳ-inverse-v □ ξ-ise (is-seqᴳ-equiv-head rest-ise) ⟩ᴳ
  fst rest-inverse-equiv) ,
  is-equiv-inverse ξ-ise , snd rest-inverse-equiv
  where
    rest-inverse-equiv = HomSeqEquiv-inverse (rest , rest-ise)

{- Doesn't seem useful.

infix 15 _↕|ᴳ
infixr 10 _↕⟨_⟩ᴳ_

_↕|ᴳ : ∀ {i} {G₀ G₁ : Group i} (iso : G₀ ≃ᴳ G₁)
  → HomSeqEquiv (G₀ ⊣|ᴳ) (G₁ ⊣|ᴳ) (fst iso) (fst iso)
iso ↕|ᴳ = (fst iso ↓|ᴳ) , snd iso

_↕⟨_⟩ᴳ_ : ∀ {i} {G₀ G₁ H₀ H₁ K₀ K₁ : Group i}
  → {φ : G₀ →ᴳ H₀} {seq₀ : HomSequence H₀ K₀}
  → {ψ : G₁ →ᴳ H₁} {seq₁ : HomSequence H₁ K₁}
  → (isoG : G₀ ≃ᴳ G₁) {isoH : H₀ ≃ᴳ H₁} {isoK : K₀ ≃ᴳ K₁}
  → HomCommSquare φ ψ (fst isoG) (fst isoH)
  → HomSeqEquiv seq₀ seq₁ (fst isoH) (fst isoK)
  → HomSeqEquiv (G₀ →⟨ φ ⟩ᴳ seq₀) (G₁ →⟨ ψ ⟩ᴳ seq₁) (fst isoG) (fst isoK)
(ξG , hG-is-equiv) ↕⟨ sqr ⟩ᴳ (seq-map , seq-map-is-equiv) =
  (ξG ↓⟨ sqr ⟩ᴳ seq-map) , hG-is-equiv , seq-map-is-equiv
-}

private
  hom-seq-map-index-type : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
    {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    → ℕ → HomSeqMap seq₀ seq₁ ξG ξH → Type (lmax i₀ i₁)
  hom-seq-map-index-type _     (_ ↓|ᴳ) = Lift ⊤
  hom-seq-map-index-type O     (_↓⟨_⟩ᴳ_ {φ = φ} {ψ = ψ} ξG {ξH} _ _)
    = CommSquareᴳ φ ψ ξG ξH
  hom-seq-map-index-type (S n) (_ ↓⟨ _ ⟩ᴳ seq-map)
    = hom-seq-map-index-type n seq-map

abstract
  hom-seq-map-index : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
    {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    (n : ℕ) (seq-map : HomSeqMap seq₀ seq₁ ξG ξH)
    → hom-seq-map-index-type n seq-map
  hom-seq-map-index _     (_ ↓|ᴳ) = lift tt
  hom-seq-map-index O     (_ ↓⟨ □ ⟩ᴳ _) = □
  hom-seq-map-index (S n) (_ ↓⟨ _ ⟩ᴳ seq-map)
    = hom-seq-map-index n seq-map

private
  hom-seq-equiv-index-type : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
    {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    → ℕ → HomSeqMap seq₀ seq₁ ξG ξH → Type (lmax i₀ i₁)
  hom-seq-equiv-index-type {ξG = ξG} O _ = is-equiv (GroupHom.f ξG)
  hom-seq-equiv-index-type (S _) (_ ↓|ᴳ) = Lift ⊤
  hom-seq-equiv-index-type (S n) (_ ↓⟨ _ ⟩ᴳ seq-map)
    = hom-seq-equiv-index-type n seq-map

abstract
  hom-seq-equiv-index : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
    {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    (n : ℕ) (seq-equiv : HomSeqEquiv seq₀ seq₁ ξG ξH)
    → hom-seq-equiv-index-type n (fst seq-equiv)
  hom-seq-equiv-index O     (seq-map , ise) = is-seqᴳ-equiv-head ise
  hom-seq-equiv-index (S _) ((_ ↓|ᴳ) , _) = lift tt
  hom-seq-equiv-index (S n) ((_ ↓⟨ _ ⟩ᴳ seq-map) , ise)
    = hom-seq-equiv-index n (seq-map , snd ise)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------------
-- Conversion rules for inequalities
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Inequalities.ConversionRules where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat.Inequalities

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

private

  -- Before to prove some properties for lt it is convenient
  -- to descompose the behavior of the function step by step.

  -- Initially, we define the possible states (lt-s₁,
  -- lt-s₂, ...). Then we write down the proof for
  -- the execution step from the state p to the state q, e.g.
  --
  -- proof₁→proof₂ : ∀ m n → lt-s₂ m n → lt-s₃ m n.

  -- The terms lt-00, lt-0S, lt-S0 and lt-SS show the use of the
  -- states lt-s₁, lt-s₂, ..., and the proofs associated with the
  -- execution steps.

  ----------------------------------------------------------------------
  -- The steps of lt.

  -- Initially, the conversion rule fix-eq is applied.
  lt-s₁ : D → D → D
  lt-s₁ m n = lth (fix lth) · m · n

  -- First argument application.
  lt-s₂ : D → D
  lt-s₂ m = lam (λ n →
              if (iszero₁ n)
                then false
                else (if (iszero₁ m)
                        then true
                        else (fix lth · pred₁ m · pred₁ n)))

  -- Second argument application.
  lt-s₃ : D → D → D
  lt-s₃ m n = if (iszero₁ n)
                then false
                else (if (iszero₁ m)
                        then true
                        else (fix lth · pred₁ m · pred₁ n))

  -- Reduction iszero₁ n ≡ b.
  lt-s₄ : D → D → D → D
  lt-s₄ m n b = if b
                  then false
                  else (if (iszero₁ m)
                          then true
                          else (fix lth · pred₁ m · pred₁ n))

  -- Reduction iszero₁ n ≡ true.
  -- It should be
  -- lt-s₅ : D → D → D
  -- lt-s₅ m n = false
  -- but we do not give a name to this step.

  -- Reduction iszero₁ n ≡ false.
  lt-s₅ : D → D → D
  lt-s₅ m n = if (iszero₁ m) then true else (fix lth · pred₁ m · pred₁ n)

  -- Reduction iszero₁ m ≡ b.
  lt-s₆ : D → D → D → D
  lt-s₆ m n b = if b then true else (fix lth · pred₁ m · pred₁ n)

  -- Reduction iszero₁ m ≡ true.
  -- It should be
  -- lt-s₇ : D → D → D
  -- lt-s₇ m n = true
  -- but we do not give a name to this step.

   -- Reduction iszero₁ m ≡ false.
  lt-s₇ : D → D → D
  lt-s₇ m n = fix lth · pred₁ m · pred₁ n

  -- Reduction pred₁ (succ m) ≡ m.
  lt-s₈ : D → D → D
  lt-s₈ m n = fix lth · m · pred₁ n

  -- Reduction pred₁ (succ n) ≡ n.
  lt-s₉ : D → D → D
  lt-s₉ m n = fix lth · m · n

  ----------------------------------------------------------------------
  -- The execution steps

  {-

    To prove the execution steps, e.g.

    proof₃→proof₄ : ∀ m n → lt-s₃ m n → lt-s₄ m n)

    we usually need to prove that

                         C [m] ≡ C [n]    (1)

    given that
                             m ≡ n,       (2)

    where (2) is a conversion rule usually.

    We prove (1) using

    subst : ∀ {x y} (A : D → Set) → x ≡ y → A x → A y

    where
      • P is given by λ t → C [m] ≡ C [t],
      • x ≡ y is given m ≡ n and
      • P x is given by C [m] ≡ C [m] (i.e. refl).
  -}

  -- Application of the conversion rule fix-eq.
  proof₀₋₁ : ∀ m n → fix lth · m · n  ≡ lt-s₁ m n
  proof₀₋₁ m n = subst (λ x → x · m · n  ≡ lth (fix lth) · m · n)
                       (sym (fix-eq lth))
                       refl

  -- Application of the first argument.
  proof₁₋₂ : ∀ m n → lt-s₁ m n ≡ lt-s₂ m · n
  proof₁₋₂ m n = subst (λ x → x · n ≡ lt-s₂ m · n)
                       (sym (beta lt-s₂ m))
                       refl

  -- Application of the second argument.
  proof₂₋₃ : ∀ m n → lt-s₂ m · n ≡ lt-s₃ m n
  proof₂₋₃ m n = beta (lt-s₃ m) n

  -- Reduction iszero n ≡ b using that proof.
  proof₃₋₄ : ∀ m n b → iszero₁ n ≡ b → lt-s₃ m n ≡ lt-s₄ m n b
  proof₃₋₄ m n .(iszero₁ n) refl = refl

  -- Reduction of iszero₁ n ≡ true using the conversion rule if-true.
  proof₄₊ : ∀ m n → lt-s₄ m n true ≡ false
  proof₄₊ m n = if-true false

  -- Reduction of iszero₁ n ≡ false ... using the conversion rule
  -- if-false.
  proof₄₋₅ : ∀ m n → lt-s₄ m n false ≡ lt-s₅ m n
  proof₄₋₅ m n = if-false (lt-s₅ m n)

  -- Reduction iszero₁ m ≡ b using that proof.
  proof₅₋₆ : ∀ m n b → iszero₁ m ≡ b → lt-s₅ m n ≡ lt-s₆ m n b
  proof₅₋₆ m n .(iszero₁ m) refl = refl

  -- Reduction of iszero₁ m ≡ true using the conversion rule if-true.
  proof₆₊ : ∀ m n → lt-s₆ m n true ≡ true
  proof₆₊ m n = if-true true

  -- Reduction of iszero₁ m ≡ false ... using the conversion rule
  -- if-false.
  proof₆₋₇ : ∀ m n → lt-s₆ m n false ≡ lt-s₇ m n
  proof₆₋₇ m n = if-false (lt-s₇ m n)

  -- Reduction pred (succ m) ≡ m using the conversion rule pred-S.
  proof₇₋₈ : ∀ m n → lt-s₇ (succ₁ m) n ≡ lt-s₈ m n
  proof₇₋₈ m n = subst (λ x → lt-s₈ x n ≡ lt-s₈ m n)
                       (sym (pred-S m))
                       refl

  -- Reduction pred (succ n) ≡ n using the conversion rule pred-S.
  proof₈₋₉ : ∀ m n → lt-s₈ m (succ₁ n) ≡ lt-s₉ m n
  proof₈₋₉ m n = subst (λ x → lt-s₉ m x ≡ lt-s₉ m n)
                       (sym (pred-S n))
                       refl

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

private
  X≮0 : ∀ n → n ≮ zero
  X≮0 n = fix lth · n · zero  ≡⟨ proof₀₋₁ n zero ⟩
          lt-s₁ n zero        ≡⟨ proof₁₋₂ n zero ⟩
          lt-s₂ n · zero      ≡⟨ proof₂₋₃ n zero ⟩
          lt-s₃ n zero        ≡⟨ proof₃₋₄ n zero true iszero-0 ⟩
          lt-s₄ n zero true   ≡⟨ proof₄₊ n zero ⟩
          false              ∎

lt-00 : zero ≮ zero
lt-00 = X≮0 zero

lt-0S : ∀ n → zero < succ₁ n
lt-0S n =
  fix lth · zero · (succ₁ n)    ≡⟨ proof₀₋₁ zero (succ₁ n) ⟩
  lt-s₁ zero (succ₁ n)          ≡⟨ proof₁₋₂ zero (succ₁ n) ⟩
  lt-s₂ zero · (succ₁ n)        ≡⟨ proof₂₋₃ zero (succ₁ n) ⟩
  lt-s₃ zero (succ₁ n)          ≡⟨ proof₃₋₄ zero (succ₁ n) false (iszero-S n) ⟩
  lt-s₄ zero (succ₁ n) false    ≡⟨ proof₄₋₅ zero (succ₁ n) ⟩
  lt-s₅ zero (succ₁ n)          ≡⟨ proof₅₋₆ zero (succ₁ n) true iszero-0 ⟩
  lt-s₆ zero (succ₁ n) true     ≡⟨ proof₆₊  zero (succ₁ n) ⟩
  true                         ∎

lt-S0 : ∀ n → succ₁ n ≮ zero
lt-S0 n = X≮0 (succ₁ n)

lt-SS : ∀ m n → lt (succ₁ m) (succ₁ n) ≡ lt m n
lt-SS m n =
  fix lth · (succ₁ m) · (succ₁ n)  ≡⟨ proof₀₋₁ (succ₁ m) (succ₁ n) ⟩
  lt-s₁ (succ₁ m) (succ₁ n)        ≡⟨ proof₁₋₂ (succ₁ m) (succ₁ n) ⟩
  lt-s₂ (succ₁ m) · (succ₁ n)      ≡⟨ proof₂₋₃ (succ₁ m) (succ₁ n) ⟩
  lt-s₃ (succ₁ m) (succ₁ n)        ≡⟨ proof₃₋₄ (succ₁ m) (succ₁ n) false (iszero-S n) ⟩
  lt-s₄ (succ₁ m) (succ₁ n) false  ≡⟨ proof₄₋₅ (succ₁ m) (succ₁ n) ⟩
  lt-s₅ (succ₁ m) (succ₁ n)        ≡⟨ proof₅₋₆ (succ₁ m) (succ₁ n) false (iszero-S m) ⟩
  lt-s₆ (succ₁ m) (succ₁ n) false  ≡⟨ proof₆₋₇ (succ₁ m) (succ₁ n) ⟩
  lt-s₇ (succ₁ m) (succ₁ n)        ≡⟨ proof₇₋₈ m (succ₁ n) ⟩
  lt-s₈ m (succ₁ n)                ≡⟨ proof₈₋₉ m n ⟩
  lt-s₉ m n                        ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Data
open import Data.Tuple using (_⨯_ ; _,_)
open import Logic.Predicate
import      Lvl
open import Syntax.Number
import      Type as Meta

-- `Constants` is the type of all possible constant terms.
-- `Sort` is a subset of `Constants` that indicate the sorts of the type system (the types of types).
-- `Axioms` pairs constant terms with types.
-- `Rules` pairs product terms with types.
module Formalization.PureTypeSystem (Constants : Meta.Type{0}) where -- TODO: I don't really have a reference for any of the definitions so they may be incorrect

open import Numeral.Natural
open import Numeral.Finite

private variable ℓ ℓ₁ ℓ₂ ℓ₃ : Lvl.Level
private variable d d₁ d₂ d₃ : ℕ

data Term : ℕ → Meta.Type{0} where
  Apply    : Term(d) → Term(d) → Term(d)
  Abstract : Term(d) → Term(𝐒(d)) → Term(d)
  Var      : 𝕟(d) → Term(d)
  Constant : Constants → Term(d)
  Product  : Term(d) → Term(𝐒(d)) → Term(d)

Expression : Meta.Type{0}
Expression = Term(0)

module VarNumeralSyntax where
  -- Syntax for writing Var as a numeral.
  instance
    Term-from-ℕ : ∀{N} → Numeral(Term(N))
    Numeral.restriction-ℓ ( Term-from-ℕ {N} ) = Numeral.restriction-ℓ ( 𝕟-from-ℕ {N} )
    Numeral.restriction   ( Term-from-ℕ {N} ) = Numeral.restriction ( 𝕟-from-ℕ {N} )
    num                   ⦃ Term-from-ℕ {N} ⦄ (n) ⦃ proof ⦄ = Var(num n)

module ExplicitLambdaSyntax where
  open VarNumeralSyntax public

  infixr 100 𝜆[_::_] Π[_::_]
  infixl 101 _←_

  pattern 𝜆[_::_] d type expr = Term.Abstract{d} type expr
  pattern Π[_::_] d type expr = Term.Product{d} type expr
  pattern _←_ a b  = Term.Apply a b

module _ where
  var-𝐒 : Term(d) → Term(𝐒(d))
  var-𝐒 (Apply f x)             = Apply (var-𝐒(f)) (var-𝐒(x))
  var-𝐒 (Abstract{d} type body) = Abstract{𝐒(d)} (var-𝐒 type) (var-𝐒(body))
  var-𝐒 (Var{𝐒(d)} n)           = Var{𝐒(𝐒(d))} (𝐒(n))
  var-𝐒 (Constant c)            = Constant c
  var-𝐒 (Product a b)           = Product (var-𝐒 a) (var-𝐒 b)

  substituteVar0 : Term(d) → Term(𝐒(d)) → Term(d)
  substituteVar0 val (Apply f x)          = Apply (substituteVar0 val f) (substituteVar0 val x)
  substituteVar0 val (Abstract type body) = Abstract (substituteVar0 val type) (substituteVar0 (var-𝐒 val) body)
  substituteVar0 val (Var 𝟎)              = val
  substituteVar0 val (Var(𝐒 i))           = Var i
  substituteVar0 val (Constant c)         = Constant c
  substituteVar0 val (Product a b)        = Product (substituteVar0 val a) (substituteVar0 (var-𝐒 val) b)

  open import Relator.Equals

  private variable x y : Term(d)

  substituteVar0-var-𝐒 : (substituteVar0 y (var-𝐒 x) ≡ x)
  substituteVar0-var-𝐒 {d}{y}{Apply f x}
    rewrite substituteVar0-var-𝐒 {d}{y}{f}
    rewrite substituteVar0-var-𝐒 {d}{y}{x}
    = [≡]-intro
  substituteVar0-var-𝐒 {d}{y}{Abstract t x}
    rewrite substituteVar0-var-𝐒 {d}{y}{t}
    rewrite substituteVar0-var-𝐒 {𝐒 d}{var-𝐒 y}{x}
    = [≡]-intro
  substituteVar0-var-𝐒 {_}{_}{Var 𝟎}      = [≡]-intro
  substituteVar0-var-𝐒 {_}{_}{Var(𝐒 _)}   = [≡]-intro
  substituteVar0-var-𝐒 {_}{_}{Constant c} = [≡]-intro
  substituteVar0-var-𝐒 {d}{y}{Product t x}
    rewrite substituteVar0-var-𝐒 {d}{y}{t}
    rewrite substituteVar0-var-𝐒 {𝐒 d}{var-𝐒 y}{x}
    = [≡]-intro
  {-# REWRITE substituteVar0-var-𝐒 #-}

module _ where
  -- postulate _β⥈*_ : Term(d) → Term(d) → Meta.Type{0}
  open import Relator.ReflexiveTransitiveClosure

  private variable f g x y : Term(d)

  -- β-reduction (beta) with its compatible closure over `Apply`.
  -- Reduces a term of form `f(x)` to `f[0 ≔ x]`.
  data _β⇴_ : Term(d₁) → Term(d₂) → Meta.Type{1} where
    β : ∀{f : Term(𝐒(d))}{x ty : Term(d)} → (Apply(Abstract ty (f))(x) β⇴ substituteVar0(x)(f))
    cong-applyₗ : (f β⇴ g) → (Apply f(x) β⇴ Apply g(x))
    cong-applyᵣ : (x β⇴ y) → (Apply f(x) β⇴ Apply f(y))

  _β⇴*_ : Term(d) → Term(d) → Meta.Type
  _β⇴*_ = ReflexiveTransitiveClosure(_β⇴_)

  _β⥈_ : Term(d) → Term(d) → Meta.Type
  _β⥈_ = SymmetricClosure(_β⇴_)

  _β⥈*_ : Term(d) → Term(d) → Meta.Type
  _β⥈*_ = ReflexiveTransitiveClosure(_β⥈_)

{-
module _ where
  open import Data.Boolean
  open import Data.Boolean.Stmt
  open import Data.Option
  import      Data.Option.Functions as Option
  open import Logic.Propositional
  open import Functional

  private variable T A B : Meta.Type{ℓ}
  private variable x : A
  private variable y : B
  private variable m m₁ m₂ : T
  private variable f : A → B

  open import Relator.Equals
  record MapContainer (A : Meta.Type{ℓ₁}) (B : A → Meta.Type{ℓ₂}) (Map : Meta.Type{ℓ₃}) : Meta.Type{Lvl.𝐒(ℓ₁) Lvl.⊔ Lvl.𝐒(ℓ₂) Lvl.⊔ ℓ₃} where
    field
      ∅     : Map
      has   : A → Map → Bool
      get   : (a : A) → Map → Option(B(a))
      set   : (a : A) → B(a) → Map → Map
      unset : A → Map → Map
      union : Map → Map → Map
      -- map   : (B → B) → (Map → Map)
      _⊆_   : Map → Map → Meta.Type{0}
      _≡ₘ_  : Map → Map → Meta.Type{0}

    field
      get-of-∅     : (get x ∅ ≡ None)
      get-has      : (Option.isSome(get x m) ≡ has x m)
      get-of-set   : (get x (set x y m) ≡ Some(y))
      get-of-unset : (get x (unset x m) ≡ None)
      get-of-union : (get x (union m₁ m₂) ≡ (get x m₁) Option.Same.orᵣ (get x m₂))
      -- get-of-map   : (get x (map f m) ≡ Option.map f(get x m))
      submap-get   : (m₁ ⊆ m₂) ↔ (∀{x} → (IsFalse(has x m₁) ∨ (get x m₁ ≡ get x m₂)))
      equiv-get    : (m₁ ≡ₘ m₂) ↔ (∀{x} → (get x m₁ ≡ get x m₂))
-}

open import Numeral.CoordinateVector
open import Type.Dependent
module Typing
  (Sort : ∀{d} → Term(d) → Meta.Type{0})
  (Axioms : Constants → Expression → Meta.Type{0})
  (Rules : ∀{d₁ d₂ d₃} → ∃(Sort{d₁}) → ∃(Sort{d₂}) → ∃(Sort{d₃}) → Meta.Type{0})
  where

  data Context : ℕ → Meta.Type{0} where
    ∅   : Context(𝟎)
    _⊱_ : Context(d) → Term(d) → Context(𝐒(d))

  get : (i : 𝕟(𝐒(d))) → Context(𝐒(d)) → Term(d)
  get       𝟎     (_ ⊱ x) = x
  get {𝐒 _} (𝐒 i) (l ⊱ _) = var-𝐒(get i l)

  private variable A A₁ A₂ B B₁ B₂ F F₁ F₂ X X₁ X₂ BX T T₁ T₂ : Term(d)
  private variable c : Constants
  private variable i i₁ i₂ : 𝕟(d)
  private variable s s₁ s₂ s₃ : ∃(Sort)
  private variable Γ Δ : Context(d)

  -- Subtyping rules.
  _<:_ = _β⥈*_

  open import Data.Option
  open import Relator.Equals

  -- Typing rules. (TODO: I think there are some issues with the depth indexing)
  data _⊢_::_ : Context(d₁) → Term(d₂) → Term(d₃) → Meta.Type{1} where
    constants   : (Axioms c A) → (Γ ⊢ (Constant{d₂} c) :: A)
    variables   : (Γ ⊢ (get i Γ) :: ([∃]-witness s)) → (Γ ⊢ (Var i) :: (get i Γ))
    weakening   : (Γ ⊢ B :: ([∃]-witness s)) → (Γ ⊢ X :: A) → ((Γ ⊱ B) ⊢ X :: A)
    product     : (Rules s₁ s₂ s₃) → (Γ ⊢ A :: ([∃]-witness s₁)) → ((Γ ⊱ A) ⊢ B :: ([∃]-witness s₂)) → (Γ ⊢ (Product A B) :: ([∃]-witness s₃))
    application : (Γ ⊢ F :: Product A B) → (Γ ⊢ X :: A) → (Γ ⊢ Apply F X :: substituteVar0 X B)
    abstraction : (Γ ⊢ (Product A B) :: ([∃]-witness s)) → ((Γ ⊱ A) ⊢ F :: B) → (Γ ⊢ (Abstract A F) :: (Product A B))
    -- conversion  : (Γ ⊢ B :: Constant([∃]-witness s)) → (A <: B) → (Γ ⊢ X :: A) → (Γ ⊢ X :: B)

{-
3: 6
4: 7

0: 3
1: 4

𝕟-to-ℕ (Wrapping.[−] i₁) ≡ 𝕟-to-ℕ (Wrapping.[−] i₂)
-}
  data _≡d_ : Term(d₁) → Term(d₂) → Meta.Type{0} where
    application : (F₁ ≡d F₂) → (X₁ ≡d X₂) → (Apply F₁ X₁ ≡d Apply F₂ X₂)
    abstraction : (T₁ ≡d T₂) → (B₁ ≡d B₂) → Abstract T₁ B₁ ≡d Abstract T₂ B₂
    var-left    : (Var{𝐒(d₁)} {!d₁ −₀ d₂!} ≡d Var{𝐒(d₂)} 𝟎)
    var-right   : (Var{𝐒(d₁)} 𝟎 ≡d Var{𝐒(d₂)} {!d₁ −₀ d₂!})
    var-step    : (Var i₁ ≡d Var i₂) → (Var(𝐒(i₁)) ≡d Var(𝐒(i₂)))
    constant    : Constant{d₁} c ≡d Constant{d₂} c
    product     : (A₁ ≡d A₂) → (B₁ ≡d B₂) → Product A₁ B₁ ≡d Product A₂ B₂

  open import Logic.Propositional
  open import Syntax.Function
  open import Type.Dependent.Functions

  -- typing-substitution : ((set Var0 B (Γ ∪ Δ)) ⊢ A :: B) → ((Γ ∪ map(\(intro e p) → {!substituteVar0 X p!}) Δ) ⊢ (substituteVar0 X A) :: (substituteVar0 X B))

  import      Data.Either as Either
  open import Logic.Classical
  module _
    ⦃ classical-sort : ∀{d}{c} → Classical(Sort{d} c) ⦄
    -- (axioms-term-or-sort : ∀{A B} → (Axioms A B) → (Sort(B) ∨ ∃(d ↦ ∃{Obj = ∃(Sort{d})}(s ↦ Γ ⊢ B :: ([∃]-witness s)))))
    where

    sort-substituteVar0 : Sort(X) → Sort(A) → Sort(substituteVar0 X A)
    sort-substituteVar0 {A = Apply F X}    _      sort-A = {!!}
    sort-substituteVar0 {A = Abstract T B} _      sort-A = {!!}
    sort-substituteVar0 {A = Var 𝟎}        sort-X sort-A = sort-X
    sort-substituteVar0 {A = Var (𝐒 i)}    _      sort-A = {!!}
    sort-substituteVar0 {A = Constant c}   _      sort-A = {!sort-A!}
    sort-substituteVar0 {A = Product A B}  _      sort-A = {!!}

    -- When a term has a type, the type is either a sort or its type is a sort.
    type-is-term-or-sort : (Γ ⊢ A :: B) → (Sort(B) ∨ ∃{Obj = ∃(d ↦ ∃(Sort{d}))}(s ↦ Γ ⊢ B :: ([∃]-witness([∃]-proof s))))
    type-is-term-or-sort (constants {c} axiom) = {!!}
    type-is-term-or-sort (variables {s = s} ty) = [∨]-introᵣ ([∃]-intro ([∃]-intro _ ⦃ s ⦄) ⦃ ty ⦄)
    type-is-term-or-sort (weakening{s = s} pre post) = Either.mapRight ([∃]-map-proof (weakening{s = s} pre)) (type-is-term-or-sort post)
    type-is-term-or-sort (product{s₃ = s₃} r a b) = [∨]-introₗ ([∃]-proof s₃)
    type-is-term-or-sort (application {F = F} ab a) = {!!}
    type-is-term-or-sort (abstraction{s = s} ab f) = [∨]-introᵣ ([∃]-intro ([∃]-intro _ ⦃ s ⦄) ⦃ ab ⦄)
    {-type-is-term-or-sort (constants {c} axiom) = ? -- axioms-term-or-sort axiom
    type-is-term-or-sort (variables {s = s} ty) = [∨]-introᵣ {!!}
    type-is-term-or-sort (product{s₃ = s₃} r a b) = [∨]-introₗ ([∃]-proof s₃)
    type-is-term-or-sort (application {F = Apply F F₁} ab a) = {!!}
    type-is-term-or-sort (application {F = Abstract F F₁} (abstraction ab ab₁) a) = {!!}
    type-is-term-or-sort (application {F = Constant x} ab a) = {!!}
    type-is-term-or-sort (application {F = Product F F₁} ab a) = {!!}
    type-is-term-or-sort (abstraction{s = s} ab f) = [∨]-introᵣ ([∃]-intro s ⦃ ab ⦄)
    -}

  -- A supermap of the context have the same typings.
  -- typing-supercontext : (Γ ⊆ Δ) → ((Γ ⊢ A :: B) → (Δ ⊢ A :: B))

  -- TODO: Confluence, subject reduction

  open import Data.Option.Equiv.Id
  open import Data.Option.Proofs
  open import Relator.Equals.Proofs
  open import Structure.Function
  open import Structure.Function.Domain hiding (Constant)
  open import Structure.Relator.Properties
  open import Structure.Setoid.Uniqueness
  open import Syntax.Transitivity

  instance
    Constant-injective : Injective(Constant{d})
    Injective.proof Constant-injective [≡]-intro = [≡]-intro

  instance
    Var-injective : Injective(Var{d})
    Injective.proof Var-injective [≡]-intro = [≡]-intro

  Productₗ-injective : ∀{ty₁ ty₂}{f₁ f₂} → (Product{d} ty₁ f₁ ≡ Product{d} ty₂ f₂) → (ty₁ ≡ ty₂)
  Productₗ-injective [≡]-intro = [≡]-intro

  Productᵣ-injective : ∀{ty₁ ty₂}{f₁ f₂} → (Product{d} ty₁ f₁ ≡ Product{d} ty₂ f₂) → (f₁ ≡ f₂) -- TODO: Here is an example of what axiom K does. If one had `Product ty f₁ ≡ Product ty f₂` instead, then it cannot pattern match on the identity because of `ty` being the same on both sides.
  Productᵣ-injective [≡]-intro = [≡]-intro

  Applyₗ-injective : ∀{f₁ f₂}{x₁ x₂} → (Apply{d} f₁ x₁ ≡ Apply{d} f₂ x₂) → (f₁ ≡ f₂)
  Applyₗ-injective [≡]-intro = [≡]-intro

  Applyᵣ-injective : ∀{f₁ f₂}{x₁ x₂} → (Apply{d} f₁ x₁ ≡ Apply{d} f₂ x₂) → (x₁ ≡ x₂)
  Applyᵣ-injective [≡]-intro = [≡]-intro

  Abstractₗ-injective : ∀{T₁ T₂}{body₁ body₂} → (Abstract{d} T₁ body₁ ≡ Abstract{d} T₂ body₂) → (T₁ ≡ T₂)
  Abstractₗ-injective [≡]-intro = [≡]-intro

  Abstractᵣ-injective : ∀{T₁ T₂}{body₁ body₂} → (Abstract{d} T₁ body₁ ≡ Abstract{d} T₂ body₂) → (body₁ ≡ body₂)
  Abstractᵣ-injective [≡]-intro = [≡]-intro

  open import Functional
  open import Logic.Predicate.Equiv
  import      Structure.Relator.Function.Multi as Relator
  open import Structure.Operator

  -- Every typable term have an unique type when all constants and products also have an unique type.
  {-typing-uniqueness : Relator.Names.Function(1)(Axioms) → (∀{d₁ d₂ d₃ : ℕ} → Relator.Names.Function(2) ⦃ [≡∃]-equiv ⦄ ⦃ [≡∃]-equiv ⦄ ⦃ [≡∃]-equiv ⦄ (Rules{d₁}{d₂}{d₃})) → Unique(Γ ⊢ X ::_)
  typing-uniqueness ax rul (constants px)       (constants py)       = ax [≡]-intro px py
  typing-uniqueness ax rul (variables _ pix)    (variables _ piy)    = injective(Some) (transitivity(_≡_) (symmetry(_≡_) pix) piy)
  typing-uniqueness ax rul (product rx px px₁)  (product ry py py₁)
    rewrite typing-uniqueness ax rul px py
    = rul (typing-uniqueness ax rul px py) (typing-uniqueness ax rul px₁ py₁) rx ry
  typing-uniqueness ax rul (application px px₁) (application py py₁) = congruence₁(substituteVar0 _) (Productᵣ-injective (typing-uniqueness ax rul px py))
  typing-uniqueness ax rul (abstraction px px₁) (abstraction py py₁)

    = congruence₁(Product _) {!!}  -- (typing-uniqueness ax rul px₁ {!!})
  -- typing-uniqueness {𝐒 d} ax rul {x}{y} px (conversion py x₁ py₁) rewrite typing-uniqueness ax rul px py₁ = {!x!}
  -- typing-uniqueness {𝐒 d} ax rul (conversion px x px₁) py = {!!}
  -}

  {-
  typing-uniqueness : Relator.Names.Function(1)(Axioms) → (∀{d₁ d₂ d₃ : ℕ} → Relator.Names.Function(2) ⦃ [≡∃]-equiv ⦄ ⦃ [≡∃]-equiv ⦄ ⦃ [≡∃]-equiv ⦄ (Rules{d₁}{d₂}{d₃})) → (∀{d : ℕ} → Relator.Names.Function(2)(_⊢_::_ {d = d}))
  typing-uniqueness ax rul                  gam exp           (constants px)       (constants py)       = ax (injective(Constant) exp) px py
  typing-uniqueness ax rul {x = Γ₁}{y = Γ₂} gam exp {y₁} {y₂} (variables _ pix)    (variables _ piy)    = injective(Some) $
    Some y₁  🝖[ _≡_ ]-[ pix ]-sym
    get _ Γ₁ 🝖[ _≡_ ]-[ congruence₂(get) (injective(Var) exp) gam ]
    get _ Γ₂ 🝖[ _≡_ ]-[ piy ]
    Some y₂ 🝖-end
  typing-uniqueness ax rul gam exp (product rx px px₁)  (product ry py py₁)  = rul XY AB rx ry where
    XY = typing-uniqueness ax rul gam (Productₗ-injective exp) px py
    AB = typing-uniqueness ax rul (congruence₃(push) (Productₗ-injective exp) XY gam) (Productᵣ-injective exp) px₁ py₁
  typing-uniqueness ax rul gam exp (application px px₁) (application py py₁) = congruence₂(substituteVar0) (Applyᵣ-injective exp) (Productᵣ-injective (typing-uniqueness ax rul gam (Applyₗ-injective exp) px py))
  typing-uniqueness ax rul gam exp (abstraction px px₁) (abstraction py py₁) = congruence₂(Product) {!!} {!!} where
    X₁X₂ = Abstractₗ-injective exp
    AB : _
    Y₁Y₂ : _
    Y₁Y₂ = typing-uniqueness ax rul (congruence₃(push) X₁X₂ AB gam) (Abstractᵣ-injective exp) px₁ py₁
    AB = typing-uniqueness ax rul gam (congruence₂(Product) X₁X₂ Y₁Y₂) px py
  -- congruence₂(Product) (Abstractₗ-injective exp) (typing-uniqueness ax rul (congruence₃(push) (Abstractₗ-injective exp) (typing-uniqueness ax rul gam {!!} px py) gam) (Abstractᵣ-injective exp) px₁ py₁)
  -}

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:
------------------------------------------------------------------------
-- Vectors
------------------------------------------------------------------------

module Data.Vec where

open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.List as List using (List)
open import Data.Product using (_×_; _,_)

------------------------------------------------------------------------
-- Types

infixr 5 _∷_

data Vec (a : Set) : ℕ → Set where
  []  : Vec a zero
  _∷_ : ∀ {n} (x : a) (xs : Vec a n) → Vec a (suc n)

infix 4 _∈_ _[_]=_

data _∈_ {a : Set} : a → {n : ℕ} → Vec a n → Set where
  here  : ∀ {n} {x}   {xs : Vec a n} → x ∈ x ∷ xs
  there : ∀ {n} {x y} {xs : Vec a n} (x∈xs : x ∈ xs) → x ∈ y ∷ xs

data _[_]=_ {a : Set} : {n : ℕ} → Vec a n → Fin n → a → Set where
  here  : ∀ {n}     {x}   {xs : Vec a n} → x ∷ xs [ zero ]= x
  there : ∀ {n} {i} {x y} {xs : Vec a n}
          (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x

------------------------------------------------------------------------
-- Some operations

head : ∀ {a n} → Vec a (1 + n) → a
head (x ∷ xs) = x

tail : ∀ {a n} → Vec a (1 + n) → Vec a n
tail (x ∷ xs) = xs

[_] : ∀ {a} → a → Vec a 1
[ x ] = x ∷ []

infixr 5 _++_

_++_ : ∀ {a m n} → Vec a m → Vec a n → Vec a (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

map : ∀ {a b n} → (a → b) → Vec a n → Vec b n
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

zipWith :  ∀ {a b c n}
        → (a → b → c) → Vec a n → Vec b n → Vec c n
zipWith _⊕_ []       []       = []
zipWith _⊕_ (x ∷ xs) (y ∷ ys) = (x ⊕ y) ∷ zipWith _⊕_ xs ys

zip : ∀ {a b n} → Vec a n → Vec b n → Vec (a × b) n
zip = zipWith _,_

replicate : ∀ {a n} → a → Vec a n
replicate {n = zero}  x = []
replicate {n = suc n} x = x ∷ replicate x

foldr :  ∀ {a} (b : ℕ → Set) {m}
      → (∀ {n} → a → b n → b (suc n))
      → b zero
      → Vec a m → b m
foldr b _⊕_ n []       = n
foldr b _⊕_ n (x ∷ xs) = x ⊕ foldr b _⊕_ n xs

foldr₁ :  ∀ {a : Set} {m}
       → (a → a → a) → Vec a (suc m) → a
foldr₁ _⊕_ (x ∷ [])     = x
foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys)

foldl :  ∀ {a : Set} (b : ℕ → Set) {m}
      → (∀ {n} → b n → a → b (suc n))
      → b zero
      → Vec a m → b m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs

foldl₁ :  ∀ {a : Set} {m}
       → (a → a → a) → Vec a (suc m) → a
foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs

concat : ∀ {a m n} → Vec (Vec a m) n → Vec a (n * m)
concat []         = []
concat (xs ∷ xss) = xs ++ concat xss

infixr 5 _++'_

data SplitAt {a : Set} (m : ℕ) {n : ℕ} : Vec a (m + n) → Set where
  _++'_ : (xs : Vec a m) (ys : Vec a n) → SplitAt m (xs ++ ys)

splitAt : ∀ {a} m {n} (xs : Vec a (m + n)) → SplitAt m xs
splitAt zero    xs                = [] ++' xs
splitAt (suc m) (x ∷ xs)          with splitAt m xs
splitAt (suc m) (x ∷ .(ys ++ zs)) | ys ++' zs = (x ∷ ys) ++' zs

take : ∀ {a} m {n} → Vec a (m + n) → Vec a m
take m xs with splitAt m xs
take m .(xs ++ ys) | xs ++' ys = xs

drop : ∀ {a} m {n} → Vec a (m + n) → Vec a n
drop m xs with splitAt m xs
drop m .(xs ++ ys) | xs ++' ys = ys

data Group {a : Set} (n k : ℕ) : Vec a (n * k) → Set where
  concat' : (xss : Vec (Vec a k) n) → Group n k (concat xss)

group : ∀ {a} n k (xs : Vec a (n * k)) → Group n k xs
group zero    k []                  = concat' []
group (suc n) k xs                  with splitAt k xs
group (suc n) k .(ys ++ zs)         | ys ++' zs with group n k zs
group (suc n) k .(ys ++ concat zss) | ys ++' ._ | concat' zss = concat' (ys ∷ zss)

reverse : ∀ {a n} → Vec a n → Vec a n
reverse {a} = foldl (Vec a) (λ rev x → x ∷ rev) []

sum : ∀ {n} → Vec ℕ n → ℕ
sum = foldr _ _+_ 0

toList : ∀ {a n} → Vec a n → List a
toList []       = List.[]
toList (x ∷ xs) = List._∷_ x (toList xs)

fromList : ∀ {a} → (xs : List a) → Vec a (List.length xs)
fromList List.[]         = []
fromList (List._∷_ x xs) = x ∷ fromList xs

-- Snoc.

infixl 5 _∷ʳ_

_∷ʳ_ : ∀ {a n} → Vec a n → a → Vec a (1 + n)
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)

infixl 5 _∷ʳ'_

data InitLast {a : Set} (n : ℕ) : Vec a (1 + n) → Set where
  _∷ʳ'_ : (xs : Vec a n) (x : a) → InitLast n (xs ∷ʳ x)

initLast : ∀ {a n} (xs : Vec a (1 + n)) → InitLast n xs
initLast {n = zero}  (x ∷ [])         = [] ∷ʳ' x
initLast {n = suc n} (x ∷ xs)         with initLast xs
initLast {n = suc n} (x ∷ .(ys ∷ʳ y)) | ys ∷ʳ' y = (x ∷ ys) ∷ʳ' y

init : ∀ {a n} → Vec a (1 + n) → Vec a n
init xs with initLast xs
init .(ys ∷ʳ y) | ys ∷ʳ' y = ys

last : ∀ {a n} → Vec a (1 + n) → a
last xs with initLast xs
last .(ys ∷ʳ y) | ys ∷ʳ' y = y

infixl 1 _>>=_

_>>=_ : ∀ {A B m n} → Vec A m → (A → Vec B n) → Vec B (m * n)
xs >>= f = concat (map f xs)

infixl 4 _⊛_

_⊛_ : ∀ {A B m n} → Vec (A → B) m → Vec A n → Vec B (m * n)
fs ⊛ xs = fs >>= λ f → map f xs

-- Interleaves the two vectors.

infixr 5 _⋎_

_⋎_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m +⋎ n)
[]       ⋎ ys = ys
(x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs)

lookup : ∀ {a n} → Fin n → Vec a n → a
lookup zero    (x ∷ xs) = x
lookup (suc i) (x ∷ xs) = lookup i xs

-- Update.

infixl 6 _[_]≔_

_[_]≔_ : ∀ {A n} → Vec A n → Fin n → A → Vec A n
[]       [ ()    ]≔ y
(x ∷ xs) [ zero  ]≔ y = y ∷ xs
(x ∷ xs) [ suc i ]≔ y = x ∷ xs [ i ]≔ y

-- Generates a vector containing all elements in Fin n. This function
-- is not placed in Data.Fin since Data.Vec depends on Data.Fin.

allFin : ∀ n → Vec (Fin n) n
allFin zero    = []
allFin (suc n) = zero ∷ map suc (allFin n)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module bool where

open import level

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

open import unit
open import empty

data 𝔹 : Set where
 tt : 𝔹
 ff : 𝔹

-- this is an alias for Mac users who cannot see blackboard b.
bool : Set
bool = 𝔹

{-# BUILTIN BOOL  𝔹  #-}
{-# BUILTIN TRUE  tt  #-}
{-# BUILTIN FALSE ff #-}

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infix  7 ~_
infix 6 _xor_ _nand_
infixr 6 _&&_
infixr 5 _||_
infix  4 if_then_else_   if*_then_else_
infixr 4 _imp_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

toSet : 𝔹 → Set
toSet tt = ⊤
toSet ff = ⊥

-- not
~_ : 𝔹 → 𝔹
~ tt = ff
~ ff = tt

-- and
_&&_ : 𝔹 → 𝔹 → 𝔹
tt && b = b
ff && b = ff

-- or
_||_ : 𝔹 → 𝔹 → 𝔹
tt || b = tt
ff || b = b

if_then_else_ : ∀ {ℓ} {A : Set ℓ} → 𝔹 → A → A → A
if tt then y else z = y
if ff then y else z = z

if*_then_else_ : ∀ {ℓ} {A B : Set ℓ} → (b : 𝔹) → A → B → if b then A else B
if* tt then a else b = a
if* ff then a else b = b

_xor_ : 𝔹 → 𝔹 → 𝔹
tt xor ff = tt
ff xor tt = tt
tt xor tt = ff
ff xor ff = ff

-- implication
_imp_ : 𝔹 → 𝔹 → 𝔹
tt imp b2 = b2
ff imp b2 = tt

-- also called the Sheffer stroke
_nand_ : 𝔹 → 𝔹 → 𝔹
tt nand tt = ff
tt nand ff = tt
ff nand tt = tt
ff nand ff = tt

_nor_ : 𝔹 → 𝔹 → 𝔹
x nor y = ~ (x || y)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import HoTT
open import homotopy.PushoutSplit

module cw.cohomology.CofiberGrid {i j k}
  {A : Type i} {B : Type j} {C : Type k}
  (f : A → B) (g : B → C) where

  {-
    A -------> B -----------> C
    |          |           _/|
    |          |         _/  |
    |          |     __.D_   |
    v          v .--'   | `-.v
    1 ------> B/A ------|-> C/A
               |        |    |
               |        v    |
               |     __.E_   |
               v .--'     `-.v
               1 ---------> C/B
  -}

  open import cw.cohomology.GridMap f g

  private
    B-to-B/A : B → B/A
    B-to-B/A = cfcod' f

    D-span : Span
    D-span = span B/A C B B-to-B/A g
    D : Type (lmax i (lmax j k))
    D = Pushout D-span

  private
    module VSplit = PushoutRSplit (λ _ → tt) f g
    module C/AToD = VSplit.Split
  C/A-to-D : C/A → D
  C/A-to-D = C/AToD.f

  B/A-to-D : B/A → D
  B/A-to-D = left

  private
    E : Type (lmax i (lmax j k))
    E = Cofiber B/A-to-D

  private
    module HSplit = PushoutLSplit B-to-B/A (λ _ → tt) g
    module C/BToE = HSplit.Split
  C/B-to-E : C/B → E
  C/B-to-E = C/BToE.f

  private
    module DToC/B = HSplit.Inner
    D-to-C/B : D → C/B
    D-to-C/B = DToC/B.f

    D-to-E : D → E
    D-to-E = cfcod

    C/A-to-D-to-C/B : ∀ c/a → D-to-C/B (C/A-to-D c/a) == C/A-to-C/B c/a
    C/A-to-D-to-C/B = Cofiber-elim
      idp
      (λ c → idp)
      (λ a → ↓-='-in' $ ! $
        ap (D-to-C/B ∘ C/A-to-D) (glue a)
          =⟨ ap-∘ D-to-C/B C/A-to-D (glue a) ⟩
        ap D-to-C/B (ap C/A-to-D (glue a))
          =⟨ C/AToD.glue-β a |in-ctx ap D-to-C/B ⟩
        ap D-to-C/B (ap left (glue a) ∙ glue (f a))
          =⟨ ap-∙ D-to-C/B (ap left (glue a)) (glue (f a)) ⟩
        ap D-to-C/B (ap left (glue a)) ∙ ap D-to-C/B (glue (f a))
          =⟨ ap2 _∙_ (∘-ap D-to-C/B left (glue a)) (DToC/B.glue-β (f a)) ⟩
        ap (λ _ → cfbase) (glue a) ∙ glue (f a)
          =⟨ ap-cst cfbase (glue a) |in-ctx _∙ glue (f a) ⟩
        glue (f a)
          =⟨ ! $ C/AToC/B.glue-β a ⟩
        ap C/A-to-C/B (glue a)
          =∎)

    D-to-C/B-to-E : ∀ d → C/B-to-E (D-to-C/B d) == D-to-E d
    D-to-C/B-to-E = HSplit.split-inner

  {- The public interface -}

  C/A-to-C/B-comm-square : CommSquare C/A-to-C/B D-to-E C/A-to-D C/B-to-E
  C/A-to-C/B-comm-square = comm-sqr λ c/a → ap C/B-to-E (! (C/A-to-D-to-C/B c/a))
                                     ∙ D-to-C/B-to-E (C/A-to-D c/a)

  B/A-to-C/A-comm-square : CommSquare B/A-to-C/A B/A-to-D (idf B/A) C/A-to-D
  B/A-to-C/A-comm-square = comm-sqr VSplit.split-inner

  C/A-to-D-is-equiv : is-equiv C/A-to-D
  C/A-to-D-is-equiv = snd VSplit.split-equiv

  C/B-to-E-is-equiv : is-equiv C/B-to-E
  C/B-to-E-is-equiv = snd HSplit.split-equiv

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import Categories.Category

module Categories.Diagram.Pullback.Limit {o ℓ e} (C : Category o ℓ e) where

open import Data.Product using (∃₂; _,_)
open import Function using (_$_)

open import Categories.Category.Instance.Span
open import Categories.Functor
open import Categories.Diagram.Pullback C
open import Categories.Morphism.Reasoning C as MR hiding (center)

import Relation.Binary.PropositionalEquality as ≡

import Categories.Category.Construction.Cones as Con
import Categories.Diagram.Limit as Lim

private
  module C = Category C
  module Span = Category Span
  open Category C
  variable
    X Y Z : Obj
    f g h : X ⇒ Y

open HomReasoning

module _ {F : Functor Span.op C} where
  open Functor F
  open Lim F
  open Con F

  private
    W = F₀ center
    A = F₀ left
    B = F₀ right

    A⇒W : A ⇒ W
    A⇒W = F₁ span-arrˡ

    B⇒W : B ⇒ W
    B⇒W = F₁ span-arrʳ

  limit⇒pullback : Limit → Pullback A⇒W B⇒W
  limit⇒pullback lim = record
    { p₁              = proj left
    ; p₂              = proj right
    ; commute         = trans (limit-commute span-arrˡ) (sym (limit-commute span-arrʳ))
    ; universal       = universal
    ; unique          = commute′
    ; p₁∘universal≈h₁ = commute
    ; p₂∘universal≈h₂ = commute
    }
    where open Limit lim
          universal : A⇒W ∘ f ≈ B⇒W ∘ g → dom f ⇒ apex
          universal {f = f} {g = g} eq = rep $ record
            { apex = record
              { ψ       = λ { center → B⇒W ∘ g
                            ; left   → f
                            ; right  → g
                            }
            ; commute = λ { {center} {center} span-id  → elimˡ identity
                          ; {left} {center} span-arrˡ  → eq
                          ; {left} {left} span-id      → elimˡ identity
                          ; {right} {center} span-arrʳ → refl
                          ; {right} {right} span-id    → elimˡ identity
                          }
              }
            }

          proj-center : proj center ≈ B⇒W ∘ proj right
          proj-center = sym (limit-commute span-arrʳ)

          commute′ : ∀ {eq : A⇒W ∘ f ≈ B⇒W ∘ g} → proj left ∘ h ≈ f → proj right ∘ h ≈ g → h ≈ universal eq
          commute′ {f = f} {g = g} {h = h} {eq = eq} eq₁ eq₂ = sym $ terminal.!-unique $ record
            { arr     = h
            ; commute = λ { {center} → begin
                              proj center ∘ h      ≈⟨ pushˡ proj-center ⟩
                              B⇒W ∘ proj right ∘ h ≈⟨ refl⟩∘⟨ eq₂ ⟩
                              B⇒W ∘ g              ∎
                          ; {left}   → eq₁
                          ; {right}  → eq₂
                          }
            }

module _ (p : Pullback f g) where
  open Pullback p

  pullback⇒limit-F : Functor Span.op C
  pullback⇒limit-F = record
    { F₀           = λ { center → cod f
                       ; left   → dom f
                       ; right  → dom g
                       }
    ; F₁           = λ { {center} {.center} span-id   → C.id
                       ; {left} {.left} span-id       → C.id
                       ; {right} {.right} span-id     → C.id
                       ; {.left} {.center} span-arrˡ  → f
                       ; {.right} {.center} span-arrʳ → g
                       }
    ; identity     = λ { {center} → refl
                       ; {left}   → refl
                       ; {right}  → refl
                       }
    ; homomorphism = λ { {center} {.center} {.center} {span-id} {span-id}   → sym identityˡ
                       ; {left} {.left} {.left} {span-id} {span-id}         → sym identityˡ
                       ; {right} {.right} {.right} {span-id} {span-id}      → sym identityˡ
                       ; {.left} {.left} {.center} {span-id} {span-arrˡ}    → sym identityʳ
                       ; {.right} {.right} {.center} {span-id} {span-arrʳ}  → sym identityʳ
                       ; {.left} {.center} {.center} {span-arrˡ} {span-id}  → sym identityˡ
                       ; {.right} {.center} {.center} {span-arrʳ} {span-id} → sym identityˡ
                       }
    ; F-resp-≈     = λ { {center} {.center} {span-id} {.span-id} ≡.refl     → refl
                       ; {left} {.left} {span-id} {.span-id} ≡.refl         → refl
                       ; {right} {.right} {span-id} {.span-id} ≡.refl       → refl
                       ; {.left} {.center} {span-arrˡ} {.span-arrˡ} ≡.refl  → refl
                       ; {.right} {.center} {span-arrʳ} {.span-arrʳ} ≡.refl → refl
                       }
    }

  open Functor pullback⇒limit-F
  open Lim pullback⇒limit-F
  open Con pullback⇒limit-F

  pullback⇒limit : Limit
  pullback⇒limit = record
    { terminal = record
      { ⊤        = ⊤
      ; !        = !
      ; !-unique = !-unique
      }
    }
    where ⊤ : Cone
          ⊤ = record
            { apex = record
              { ψ       = λ { center → g ∘ p₂
                            ; left   → p₁
                            ; right  → p₂
                            }
              ; commute = λ { {center} {.center} span-id   → identityˡ
                            ; {left} {.left} span-id       → identityˡ
                            ; {right} {.right} span-id     → identityˡ
                            ; {.left} {.center} span-arrˡ  → commute
                            ; {.right} {.center} span-arrʳ → refl
                            }
              }
            }

          ! : ∀ {A : Cone} → Cone⇒ A ⊤
          ! {A} = record
            { arr     = universal commute′
            ; commute = λ { {center} → begin
                            (g ∘ p₂) ∘ universal _ ≈⟨ pullʳ p₂∘universal≈h₂ ⟩
                            g ∘ A.ψ right          ≈⟨ A.commute span-arrʳ ⟩
                            A.ψ center             ∎
                          ; {left}   → p₁∘universal≈h₁
                          ; {right}  → p₂∘universal≈h₂
                          }
            }
            where module A = Cone A
                  commute′ = trans (A.commute span-arrˡ) (sym (A.commute span-arrʳ))

          !-unique : ∀ {A : Cone} (h : Cone⇒ A ⊤) → Cones [ ! ≈ h ]
          !-unique {A} h = sym (unique h.commute h.commute)
            where module h = Cone⇒ h

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

module Dodo.Binary.Domain where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Function.Base using (flip; _∘_)
open import Data.Product using (_×_; _,_; ∃; ∃-syntax; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂; swap)
open import Relation.Unary using (Pred; _∈_; _∉_)
open import Relation.Binary using (Rel; REL)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Unary.Union
open import Dodo.Binary.Equality
open import Dodo.Binary.Composition

-- # Definitions

-- | The domain of the binary relation
dom : ∀ {a b ℓ : Level} {A : Set a} {B : Set b}
  → REL A B ℓ
    --------------
  → Pred A (b ⊔ ℓ)
dom R x = ∃[ y ] (R x y)

-- | The co-domain (or range) of the binary relation
--
--
-- # Design decision: Not range
--
-- It is somewhat arbitrary what constitutes the /co-domain/ of a binary relation,
-- and how it differs from its /range/. Usually, the /co-domain/ denotes the set of
-- /possible/ outputs of a function, while the /range/ denotes the set of /actual/
-- outputs. When considering functions, the /domain/ is a set of /independent/ variables,
-- while the /co-domain/ is the set variables that are /dependent/ on the domain.
--
-- However, when considering /relations/ (as opposed to mere functions), this dependency
-- is (usually) absent; Or could be inverted, where the domain "depends on" the codomain.
-- Under such interpretation, distinguishing co-domain from range is rather arbitrary.
codom : ∀ {a b ℓ : Level} {A : Set a} {B : Set b}
  → REL A B ℓ
    --------------
  → Pred B (a ⊔ ℓ)
codom R y = ∃[ x ] (R x y)

-- | The domain and co-domain of the binary relation
--
-- Conventionally named after: Union (of) Domain (and) Range
udr : ∀ {a ℓ : Level} {A : Set a}
  → Rel A ℓ
    --------------
  → Pred A (a ⊔ ℓ)
udr R = dom R ∪₁ codom R

-- # Operations

-- ## Operations: dom / codom / udr

-- | Weakens an element of a relation's domain to an element of its udr.
--
-- Note that Agda is unable to infer `R` from `x ∈ dom R`.
-- (As `R` may be beta-reduced inside the latter, I think)
dom⇒udr : ∀ {a ℓ : Level} {A : Set a} (R : Rel A ℓ) {x : A} → x ∈ dom R → x ∈ udr R
dom⇒udr _ = inj₁

-- | Weakens an element of a relation's co-domain to an element of its udr.
--
-- Note that Agda is unable to infer `R` from `x ∈ dom R`.
-- (As `R` may be beta-reduced inside the latter, I think)
codom⇒udr : ∀ {a ℓ : Level} {A : Set a} (R : Rel A ℓ) {x : A} → x ∈ codom R → x ∈ udr R
codom⇒udr _ = inj₂

module _ {a b ℓ : Level} {A : Set a} {B : Set b} where

  -- | Takes an inhabitant of `R x y` as proof that `x` is in the domain of `R`.
  --
  -- Note that `R` must be provided /explicitly/, as it may not always be inferred
  -- from its applied type.
  take-dom : (R : REL A B ℓ) → {x : A} {y : B} → R x y → x ∈ dom R
  take-dom R {x} {y} Rxy = (y , Rxy)

  -- | Takes an inhabitant of `R x y` as proof that `y` is in the co-domain of `R`.
  --
  -- Note that `R` must be provided /explicitly/, as it may not always be inferred
  -- from its applied type.
  take-codom : (R : REL A B ℓ) → {x : A} {y : B} → R x y → y ∈ codom R
  take-codom R {x} {y} Rxy = (x , Rxy)

module _ {a ℓ : Level} {A : Set a} where

  -- | Takes an inhabitant of `R x y` as proof that `x` is in the udr of `R`.
  --
  -- Note that `R` must be provided /explicitly/, as it may not always be inferred
  -- from its applied type.
  take-udrˡ : (R : Rel A ℓ) → {x y : A} → R x y → x ∈ udr R
  take-udrˡ R Rxy = dom⇒udr R (take-dom R Rxy)

  -- | Takes an inhabitant of `R x y` as proof that `y` is in the udr of `R`.
  --
  -- Note that `R` must be provided /explicitly/, as it may not always be inferred
  -- from its applied type.
  take-udrʳ : (R : Rel A ℓ) → {x y : A} → R x y → y ∈ udr R
  take-udrʳ R Rxy = codom⇒udr R (take-codom R Rxy)

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} where

  dom-preserves-⊆ : P ⊆₂ Q → dom P ⊆₁ dom Q
  dom-preserves-⊆ P⊆Q = ⊆: λ{x (y , Pxy) → (y , un-⊆₂ P⊆Q x y Pxy)}

  codom-preserves-⊆ : P ⊆₂ Q → codom P ⊆₁ codom Q
  codom-preserves-⊆ P⊆Q = ⊆: λ{y (x , Pxy) → (x , un-⊆₂ P⊆Q x y Pxy)}

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a}
    {P : Rel A ℓ₁} {Q : Rel A ℓ₂} where

  udr-preserves-⊆ : P ⊆₂ Q → udr P ⊆₁ udr Q
  udr-preserves-⊆ P⊆Q = ⊆: lemma
    where
    lemma : udr P ⊆₁' udr Q
    lemma x (inj₁ x∈dom)   = dom⇒udr Q (⊆₁-apply (dom-preserves-⊆ P⊆Q) x∈dom)
    lemma y (inj₂ y∈codom) = codom⇒udr Q (⊆₁-apply (codom-preserves-⊆ P⊆Q) y∈codom)

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a}
    {P : Rel A ℓ₁} {Q : Rel A ℓ₂} where

  udr-combine-⨾ : udr (P ⨾ Q) ⊆₁ udr P ∪₁ udr Q
  udr-combine-⨾ = ⊆: lemma
    where
    lemma : udr (P ⨾ Q) ⊆₁' (udr P ∪₁ udr Q)
    lemma _ (inj₁ (a , (Pxb ⨾[ b ]⨾ Qba))) = inj₁ (inj₁ (b , Pxb))
    lemma _ (inj₂ (a , (Pab ⨾[ b ]⨾ Qbx))) = inj₂ (inj₂ (b , Qbx))

module _ {a ℓ : Level} {A : Set a}
    {P : Rel A ℓ} where

  udr-flip : udr P ⇔₁ udr (flip P)
  udr-flip = ⇔: (λ _ → swap) (λ _ → swap)

  dom-flip : dom P ⇔₁ codom (flip P)
  dom-flip = ⇔: (λ _ z → z) (λ _ z → z)

  codom-flip : codom P ⇔₁ dom (flip P)
  codom-flip = ⇔: (λ _ z → z) (λ _ z → z)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

module Dodo.Binary.Empty where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Relation.Nullary using (¬_)
open import Relation.Binary using (REL; Rel)

-- # Definitions

-- | A predicate stating no inhabitants exist for the given relation
Empty₂ : ∀ {a b ℓ : Level} {A : Set a} {B : Set b} → REL A B ℓ → Set (a ⊔ b ⊔ ℓ)
Empty₂ {A = A} {B = B} r = ∀ (x : A) (y : B) → ¬ r x y

-- | Negation of a binary relation
¬₂_ : ∀ {a b ℓ : Level} {A : Set a} {B : Set b} → REL A B ℓ → REL A B ℓ
¬₂_ r x y = ¬ r x y