text:
module Ambient where

open import Relation.Nullary
     using (yes; no)

open import Data.String
     using (String; _≟_)

open import Data.Bool
     using (Bool; true; false)

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

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

-- Local modules ---------------------------------------------------------------

open import Common
     using (Id)

open import Capability
     using (Capability; `_; In; Out; Open; ε; _∙_)
     renaming (_[_/_] to _[_/_]-capa; freeVar to freeVar-capa)

-- Process Definition ----------------------------------------------------------

infix  40 _[_/_]
infixr 30 Λ_∙_
infix  20 _[_]
infixr 10 _||_

data Process : Set where
  ν_∙_   : Id → Process → Process                 -- Restriction
  Zero   : Process                                -- Inactivity
  _||_   : Process → Process → Process            -- Composition
  !_     : Process → Process                      -- Replication
  _[_]   : Capability → Process → Process         -- Ambient
  _∙_    : Capability → Process → Process         -- Action
  Λ_∙_ : Id → Process → Process                 -- Input Action
  <_>    : Capability → Process                   -- Message

-- Free variable ---------------------------------------------------------------

_-_ : List Id → Id → List Id
[] - _      = []
(x ∷ xs) - y with x ≟ y
... | yes _ = xs - y
... | no _  = x ∷ (xs - y)

freeVar : Process → List Id
freeVar (ν x ∙ P) = freeVar P
freeVar Zero      = []
freeVar (P || Q)  = (freeVar P) ++ (freeVar Q)
freeVar (! P)     = freeVar P
freeVar (M [ P ]) = (freeVar-capa M) ++ (freeVar P)
freeVar (M ∙ P)   = (freeVar-capa M) ++ (freeVar P)
freeVar (Λ x ∙ P) = (freeVar P) - x
freeVar (< M >)   = freeVar-capa M

_∉_ : Id → List Id → Set
y ∉ l = member y l ≡≡ false
    where member : Id → List Id →  Bool -- Should propably use the List filter instead!
          member y []     = false
          member y (x ∷ xs) with x ≟ y
          ... | yes _ = true
          ... | no _  = member y xs

-- Process substitution --------------------------------------------------------

_[_/_] : Process → Id → Capability → Process

Zero [ _ / _ ]       = Zero
(P || Q) [ x / M ]   = P [ x / M ] || Q [ x / M ]
(! P) [ x / M ]      = ! (P [ x / M ])
(x [ P ]) [ y / M ]  = (x [ y / M ]-capa) [ P [ y / M ] ]
(ν x ∙ P) [ y / M ] with x ≟ y
... | yes _          = ν x ∙ P
... | no _           = ν x ∙ (P [ y / M ])
< N > [ x / M ]      = < N [ x / M ]-capa >
(Λ x ∙ P) [ y / M ] with x ≟ y
... | yes _          = Λ x ∙ P
... | no _           = Λ x ∙ (P [ y / M ])
( N ∙ P) [ x / M ]   = (N [ x / M ]-capa) ∙ (P [ x / M ])

module Test where
  a = "a"
  b = "b"

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

  _ : (` a [ < ` b > ]) [ b / Open a ] ≡≡ ` a [ < Open a > ]
  _ = refl

  _ : (< ` a > || < ` b >) [ b / Open a ] ≡≡ < ` a > || < Open a >
  _ = refl

-- Congruence ------------------------------------------------------------------

infix 5 _≡_

data _≡_ : Process → Process → Set where
  Struct-Refl    : ∀ {P}
                   -----
                 → P ≡ P

  Struct-Symm    : ∀ {P Q}
                 → P ≡ Q
                   -----
                 → Q ≡ P

  Struct-Trans   : ∀ {P Q R}
                 → P ≡ Q → Q ≡ R
                   -------------
                 → P ≡ R

  Struct-Res     : ∀ {n P Q}
                 → P ≡ Q
                   -----------------
                 → ν n ∙ P ≡ ν n ∙ Q

  Struct-Par     : ∀ {P Q R}
                 → P ≡ Q
                   ---------------
                 → P || R ≡ Q || R

  Struct-Repl    : ∀ {P Q}
                 → P ≡ Q
                   ---------
                 → ! P ≡ ! Q

  Struct-Amb     : ∀ {M P Q}
                 → P ≡ Q
                   -----------------
                 → M [ P ] ≡ M [ Q ]

  Struct-Action  : ∀ {M P Q}
                 → P ≡ Q
                   -------------
                 → M ∙ P ≡ M ∙ Q

  Struct-Input   : ∀ {x P Q}
                 → P ≡ Q
                   ---------------------
                 → Λ x ∙ P ≡ Λ x ∙ Q

  Struct-Comm    : ∀ {P Q}
                 → P ≡ Q
                   -----
                 → Q ≡ P

  Struct-Assoc   : ∀ {P Q R}
                   -----------------------------
                 → (P || Q) || R ≡ P || (Q || R)

  Struct-ResRes  : ∀ {n m P}
                 → n ≢ m
                   -----------------------------
                 → ν n ∙ ν m ∙ P ≡ ν m ∙ ν n ∙ P

  Struct-ResPar  : ∀ {n P Q}
                 → n ∉ freeVar(P)
                   -----------------------------
                 → ν n ∙ (P || Q) ≡ P || ν n ∙ Q

  Struct-ResAmb  : ∀ {n m P}
                 → n ≢ m
                   -----------------------------------
                 → ν n ∙ (` m [ P ]) ≡ ` m [ ν n ∙ P ]

  Struct-ZeroPar : ∀ {P}
                   -------------
                 → P || Zero ≡ P

  Struct-ZeroRes : ∀ {n}
                   -----------------
                 → ν n ∙ Zero ≡ Zero

  Struct-ZeroRep : ! Zero ≡ Zero

  Struct-ε       : ---------------
                   ε ∙ Zero ≡ Zero

  Struct-∙       : ∀ {M M' P}
                   ---------------------------
                 → (M ∙ M') ∙ P ≡ M ∙ (M' ∙ P)

-- Reduction rules -------------------------------------------------------------

infix 5 _~>_

data _~>_ : Process → Process → Set where
  Red-In    : ∀ {m n P Q R}
              -----------------------------------------------------------------
            → ` m [ In n ∙ P || Q ] || ` n [ R ] ~> ` n [ ` m [ P || Q ] || R ]

  Red-Out   : ∀ {m n P Q R}
              ------------------------------------------------------------------
            → ` m [ ` n [ Out m ∙ P || R ] || Q ] ~> ` m [ Q ] || ` n [ P || R ]

  Red-Open  : ∀ {m P Q}
              ---------------------------------
            → ` m [ P ] || Open m ∙ Q ~> P || Q

  Red-I/O   : ∀ {M x P}
              ---------------------------------
            → < M > || Λ x ∙ P ~> P [ x / M ]

  Red-Par   : ∀ {P Q R}
            → P ~> Q
              ------------------
            → P || R ~> Q || R

  Red-Res   : ∀ {n P Q}
            → P ~> Q
              --------------------
            → ν n ∙ P ~> ν n ∙ Q

  Red-Amb   : ∀ {M P Q}
            → P ~> Q
              --------------------
            → M [ P ] ~> M [ Q ]

  Red-≡     : ∀ {P P' Q Q'}
            → P' ≡ P  → P ~> Q → Q ≡ Q'
              -------------------------
            → P' ~> Q'

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

ext: agda

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


text:
------------------------------------------------------------------------
-- The untyped SKI combinator calculus
------------------------------------------------------------------------

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

module FOmegaInt.Undecidable.SK where

open import Data.Bool
open import Data.Product as Prod using (_,_; ∃; _×_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- The untyped SK(I) combinator calculus

infixl 9 _·_
infixl 4 _≡SK_ _≤SK?_ _⇛[_]_ _⇛[_]*_ _⇛≤_ _⇛≤*_ _⇛≥_ _⇛≥*_ _⇛≤*≤⇚_

-- Terms of the SK combinator calculus.

data SKTerm : Set where
  S   : SKTerm
  K   : SKTerm
  _·_ : SKTerm → SKTerm → SKTerm

-- Equality of SK terms.

data _≡SK_ : SKTerm → SKTerm → Set where
  ≡-refl  : ∀ {t}     → t ≡SK t
  ≡-trans : ∀ {s t u} → s ≡SK t → t ≡SK u → s ≡SK u
  ≡-sym   : ∀ {s t}   → s ≡SK t → t ≡SK s
  ≡-Sred  : ∀ {s t u} → S · s · t · u ≡SK s · u · (t · u)
  ≡-Kred  : ∀ {s t}   →     K · s · t ≡SK s
  ≡-·     : ∀ {s₁ s₂ t₁ t₂} →
            s₁ ≡SK s₂ → t₁ ≡SK t₂ → s₁ · t₁ ≡SK s₂ · t₂

-- A well-known encoding of the I combinator.

I : SKTerm
I = S · K · K

-- Some admissible equality rules.

≡-Ired : ∀ {t} → I · t ≡SK t
≡-Ired = ≡-trans ≡-Sred ≡-Kred

≡-Sexp : ∀ {s t u} → s · u · (t · u) ≡SK S · s · t · u
≡-Sexp = ≡-sym ≡-Sred

≡-Kexp : ∀ {s t} → s ≡SK K · s · t
≡-Kexp = ≡-sym ≡-Kred

≡-Iexp : ∀ {t} → t ≡SK I · t
≡-Iexp = ≡-sym ≡-Ired

------------------------------------------------------------------------
-- A variant of the untyped SK calculus with extra term formers

data SK?Term : Set where
  ⊥   : SK?Term                                 -- degenerate term
  ⊤   : SK?Term                                 -- degenerate term
  S   : SK?Term
  K   : SK?Term
  _·_ : SK?Term → SK?Term → SK?Term

-- An SK? term is pure if it is an SK term.

data Pure : SK?Term → Set where
  S    : Pure S
  K    : Pure K
  _·_  : ∀ {s t} → Pure s → Pure t → Pure (s · t)

-- A partial order on SK? terms that resembles subtyping.

data _≤SK?_ : SK?Term → SK?Term → Set where
  ≤?-refl  : ∀ {t} → t ≤SK? t
  ≤?-trans : ∀ {s t u} → s ≤SK? t → t ≤SK? u → s ≤SK? u
  ≤?-⊥     : ∀ {t} → ⊥ ≤SK? t
  ≤?-⊤     : ∀ {t} → t ≤SK? ⊤
  ≤?-Sred  : ∀ {s t u} →   S · s · t · u ≤SK? s · u · (t · u)
  ≤?-Kred  : ∀ {s t}   →       K · s · t ≤SK? s
  ≤?-Sexp  : ∀ {s t u} → s · u · (t · u) ≤SK? S · s · t · u
  ≤?-Kexp  : ∀ {s t}   →               s ≤SK? K · s · t
  ≤?-·     : ∀ {s₁ s₂ t₁ t₂} →
             s₁ ≤SK? s₂ → t₁ ≤SK? t₂ → s₁ · t₁ ≤SK? s₂ · t₂

-- Parallel one-step and multi-step reduction of SK? terms, possibly
-- containing instances of ⊥-elim and ⊤-intro.
--
-- The `i' index in `_⇛[ i ]_' indicates whether the relation is
-- increasing (true) or decreasing (false).  The increasing
-- single/multi-step relations are (strict) subrelations of _≤SK?_,
-- while the decreasing ones are subrelations of _≥SK?_ (i.e. the
-- inverse of _≤SK?_).

data _⇛[_]_ : SK?Term → Bool → SK?Term → Set where
  ⇛-refl : ∀ {t i} → t ⇛[ i ] t
  ⇛-Sred : ∀ {s₁ s₂ t₁ t₂ u₁ u₂ i} →
           s₁ ⇛[ i ] s₂ → t₁ ⇛[ i ] t₂ → u₁ ⇛[ i ] u₂ →
           S · s₁ · t₁ · u₁ ⇛[ i ] s₂ · u₂ · (t₂ · u₂)
  ⇛-Kred : ∀ {s₁ s₂ t i} → s₁ ⇛[ i ] s₂ → K · s₁ · t ⇛[ i ] s₂
  ⇛-·    : ∀ {s₁ s₂ t₁ t₂ i} →
           s₁ ⇛[ i ] s₂ → t₁ ⇛[ i ] t₂ → s₁ · t₁ ⇛[ i ] s₂ · t₂
  ⇛-⊥    : ∀ {t} → ⊥ ⇛[ true  ] t
  ⇛-⊤    : ∀ {t} → ⊤ ⇛[ false ] t

_⇛[_]*_ : SK?Term → Bool → SK?Term → Set
s ⇛[ i ]* t = (Star _⇛[ i ]_) s t

_⇛≤_ : SK?Term → SK?Term → Set
_⇛≤_ = _⇛[ true ]_

_⇛≤*_ : SK?Term → SK?Term → Set
_⇛≤*_ = _⇛[ true ]*_

_⇛≥_ : SK?Term → SK?Term → Set
_⇛≥_ = _⇛[ false ]_

_⇛≥*_ : SK?Term → SK?Term → Set
_⇛≥*_ = _⇛[ false ]*_

-- A combination of the two multi-step reductions that is equivalent
-- to _≤SK?_ modulo "squashing" of intermediate terms (see ≤SK?--⇛≤*≤⇚
-- below).

_⇛≤*≤⇚_ : SK?Term → SK?Term → Set
s ⇛≤*≤⇚ t = ∃ λ u → s ⇛≤* u × t ⇛≥* u

-- SK terms are SK? terms

inject : SKTerm → SK?Term
inject S       = S
inject K       = K
inject (s · t) = inject s · inject t

inject-Pure : ∀ t → Pure (inject t)
inject-Pure S = S
inject-Pure K = K
inject-Pure (s · t) = inject-Pure s · inject-Pure t

-- The inverse of inject on pure terms.

inject⁻¹ : ∀ {t} → Pure t → SKTerm
inject⁻¹ S       = S
inject⁻¹ K       = K
inject⁻¹ (p · q) = inject⁻¹ p · inject⁻¹ q

inject⁻¹-inject-Pure : ∀ t → inject⁻¹ (inject-Pure t) ≡ t
inject⁻¹-inject-Pure S       = refl
inject⁻¹-inject-Pure K       = refl
inject⁻¹-inject-Pure (s · t) =
  cong₂ _·_ (inject⁻¹-inject-Pure s) (inject⁻¹-inject-Pure t)

inject⁻¹-unique : ∀ {t} → (p q : Pure t) → inject⁻¹ p ≡ inject⁻¹ q
inject⁻¹-unique S         S         = refl
inject⁻¹-unique K         K         = refl
inject⁻¹-unique (p₁ · p₂) (q₁ · q₂) =
  cong₂ _·_ (inject⁻¹-unique p₁ q₁) (inject⁻¹-unique p₂ q₂)

-- Equality of SK terms is a subrelation of the SK? term order and its
-- inverse.

mutual

  ≡SK-≤SK? : ∀ {s t} → s ≡SK t → inject s ≤SK? inject t
  ≡SK-≤SK? ≡-refl            = ≤?-refl
  ≡SK-≤SK? (≡-trans s≡t t≡u) = ≤?-trans (≡SK-≤SK? s≡t) (≡SK-≤SK? t≡u)
  ≡SK-≤SK? (≡-sym s≡t)       = ≡SK-≥SK? s≡t
  ≡SK-≤SK? ≡-Sred            = ≤?-Sred
  ≡SK-≤SK? ≡-Kred            = ≤?-Kred
  ≡SK-≤SK? (≡-· s₁≡t₁ s₂≡t₂) = ≤?-· (≡SK-≤SK? s₁≡t₁) (≡SK-≤SK? s₂≡t₂)

  ≡SK-≥SK? : ∀ {s t} → s ≡SK t → inject t ≤SK? inject s
  ≡SK-≥SK? ≡-refl            = ≤?-refl
  ≡SK-≥SK? (≡-trans s≡t t≡u) = ≤?-trans (≡SK-≥SK? t≡u) (≡SK-≥SK? s≡t)
  ≡SK-≥SK? (≡-sym s≡t)       = ≡SK-≤SK? s≡t
  ≡SK-≥SK? ≡-Sred            = ≤?-Sexp
  ≡SK-≥SK? ≡-Kred            = ≤?-Kexp
  ≡SK-≥SK? (≡-· s₁≡t₁ s₂≡t₂) = ≤?-· (≡SK-≥SK? s₁≡t₁) (≡SK-≥SK? s₂≡t₂)

-- Admissible constructors for multi-step reduction

⇛*-· : ∀ {ab s₁ s₂ t₁ t₂} →
       s₁ ⇛[ ab ]* s₂ → t₁ ⇛[ ab ]* t₂ → s₁ · t₁ ⇛[ ab ]* s₂ · t₂
⇛*-· ε ε                = ε
⇛*-· ε (t₁⇛t₂ ◅ t₂⇛*t₃) = (⇛-· ⇛-refl t₁⇛t₂) ◅ (⇛*-· ε t₂⇛*t₃)
⇛*-· (s₁⇛s₂ ◅ s₂⇛*s₃) ε = (⇛-· s₁⇛s₂ ⇛-refl) ◅ (⇛*-· s₂⇛*s₃ ε)
⇛*-· (s₁⇛s₂ ◅ s₂⇛*s₃) (t₁⇛t₂ ◅ t₂⇛*t₃) = (⇛-· s₁⇛s₂ t₁⇛t₂) ◅ (⇛*-· s₂⇛*s₃ t₂⇛*t₃)

-- A Church-Rosser theorem for SK? reductions.

⇛-CR : ∀ {s t₁ t₂} → s ⇛≤ t₁ → s ⇛≥ t₂ → ∃ λ u → t₁ ⇛≥ u × t₂ ⇛≤ u
⇛-CR ⇛-refl s⇛t₂ = _ , s⇛t₂ , ⇛-refl
⇛-CR (⇛-Sred s₁⇛t₁₁ s₂⇛t₂₁ s₃⇛t₃₁) (⇛-Sred s₁⇛t₁₂ s₂⇛t₂₂ s₃⇛t₃₂) =
  let u₁ , t₁₁⇛u₁ , t₁₂⇛u₁ = ⇛-CR s₁⇛t₁₁ s₁⇛t₁₂
      u₂ , t₂₁⇛u₂ , t₂₂⇛u₂ = ⇛-CR s₂⇛t₂₁ s₂⇛t₂₂
      u₃ , t₃₁⇛u₃ , t₃₂⇛u₃ = ⇛-CR s₃⇛t₃₁ s₃⇛t₃₂
  in  u₁ · u₃ · (u₂ · u₃) ,
      ⇛-· (⇛-· t₁₁⇛u₁ t₃₁⇛u₃)  (⇛-· t₂₁⇛u₂ t₃₁⇛u₃) ,
      ⇛-· (⇛-· t₁₂⇛u₁  t₃₂⇛u₃) (⇛-· t₂₂⇛u₂ t₃₂⇛u₃)
⇛-CR (⇛-Sred s₁⇛t₁₁ s₂⇛t₂₁ s₃⇛t₃₁) (⇛-· ⇛-refl s₃⇛t₃₂) =
  let u₃ , t₃₁⇛u₃ , t₃₂⇛u₃ = ⇛-CR s₃⇛t₃₁ s₃⇛t₃₂
  in  _ · u₃ · (_ · u₃) ,
      ⇛-· (⇛-· ⇛-refl t₃₁⇛u₃) (⇛-· ⇛-refl t₃₁⇛u₃) ,
      ⇛-Sred s₁⇛t₁₁ s₂⇛t₂₁ t₃₂⇛u₃
⇛-CR (⇛-Sred s₁⇛t₁₁ s₂⇛t₂₁ s₃⇛t₃₁) (⇛-· (⇛-· ⇛-refl s₂⇛t₂₂) s₃⇛t₃₂) =
  let u₂ , t₂₁⇛u₂ , t₂₂⇛u₂ = ⇛-CR s₂⇛t₂₁ s₂⇛t₂₂
      u₃ , t₃₁⇛u₃ , t₃₂⇛u₃ = ⇛-CR s₃⇛t₃₁ s₃⇛t₃₂
  in  _ · u₃ · (u₂ · u₃) ,
      ⇛-· (⇛-· ⇛-refl t₃₁⇛u₃) (⇛-· t₂₁⇛u₂ t₃₁⇛u₃) ,
      ⇛-Sred s₁⇛t₁₁ t₂₂⇛u₂ t₃₂⇛u₃
⇛-CR (⇛-Sred s₁⇛t₁₁ s₂⇛t₂₁ s₃⇛t₃₁)
     (⇛-· (⇛-· (⇛-· ⇛-refl s₁⇛t₁₂) s₂⇛t₂₂) s₃⇛t₃₂) =
  let u₁ , t₁₁⇛u₁ , t₁₂⇛u₁ = ⇛-CR s₁⇛t₁₁ s₁⇛t₁₂
      u₂ , t₂₁⇛u₂ , t₂₂⇛u₂ = ⇛-CR s₂⇛t₂₁ s₂⇛t₂₂
      u₃ , t₃₁⇛u₃ , t₃₂⇛u₃ = ⇛-CR s₃⇛t₃₁ s₃⇛t₃₂
  in  u₁ · u₃ · (u₂ · u₃) ,
      ⇛-· (⇛-· t₁₁⇛u₁ t₃₁⇛u₃)  (⇛-· t₂₁⇛u₂ t₃₁⇛u₃) ,
      ⇛-Sred t₁₂⇛u₁ t₂₂⇛u₂ t₃₂⇛u₃
⇛-CR (⇛-Kred s⇛t₁) (⇛-Kred s⇛t₂) =
  let u , t₁⇛u , t₂⇛u = ⇛-CR s⇛t₁ s⇛t₂
  in  u , t₁⇛u , t₂⇛u
⇛-CR (⇛-Kred s₁⇛t₁₁) (⇛-· ⇛-refl _) = _ , ⇛-refl , ⇛-Kred s₁⇛t₁₁
⇛-CR (⇛-Kred s₁⇛t₁₁) (⇛-· (⇛-· ⇛-refl s₁⇛t₂₁) _) =
  let u₁ , t₁₁⇛u₁ , t₂₁⇛u₁ = ⇛-CR s₁⇛t₁₁ s₁⇛t₂₁
  in  u₁ , t₁₁⇛u₁ , ⇛-Kred t₂₁⇛u₁
⇛-CR (⇛-· ⇛-refl s₃⇛t₃₁) (⇛-Sred s₁⇛t₁₂ s₂⇛t₂₂ s₃⇛t₃₂) =
  let u₃ , t₃₁⇛u₃ , t₃₂⇛u₃ = ⇛-CR s₃⇛t₃₁ s₃⇛t₃₂
  in  _ · u₃ · (_ · u₃) ,
      ⇛-Sred s₁⇛t₁₂ s₂⇛t₂₂ t₃₁⇛u₃ ,
      ⇛-· (⇛-· ⇛-refl t₃₂⇛u₃) (⇛-· ⇛-refl t₃₂⇛u₃)
⇛-CR (⇛-· (⇛-· ⇛-refl s₂⇛t₂₁) s₃⇛t₃₁) (⇛-Sred s₁⇛t₁₂ s₂⇛t₂₂ s₃⇛t₃₂) =
  let u₂ , t₂₁⇛u₂ , t₂₂⇛u₂ = ⇛-CR s₂⇛t₂₁ s₂⇛t₂₂
      u₃ , t₃₁⇛u₃ , t₃₂⇛u₃ = ⇛-CR s₃⇛t₃₁ s₃⇛t₃₂
  in  _ · u₃ · (u₂ · u₃) ,
      ⇛-Sred s₁⇛t₁₂ t₂₁⇛u₂ t₃₁⇛u₃ ,
      ⇛-· (⇛-· ⇛-refl t₃₂⇛u₃) (⇛-· t₂₂⇛u₂ t₃₂⇛u₃)
⇛-CR (⇛-· (⇛-· (⇛-· ⇛-refl s₁⇛t₁₁) s₂⇛t₂₁) s₃⇛t₃₁)
     (⇛-Sred s₁⇛t₁₂ s₂⇛t₂₂ s₃⇛t₃₂) =
  let u₁ , t₁₁⇛u₁ , t₁₂⇛u₁ = ⇛-CR s₁⇛t₁₁ s₁⇛t₁₂
      u₂ , t₂₁⇛u₂ , t₂₂⇛u₂ = ⇛-CR s₂⇛t₂₁ s₂⇛t₂₂
      u₃ , t₃₁⇛u₃ , t₃₂⇛u₃ = ⇛-CR s₃⇛t₃₁ s₃⇛t₃₂
  in  u₁ · u₃ · (u₂ · u₃) ,
      ⇛-Sred t₁₁⇛u₁ t₂₁⇛u₂ t₃₁⇛u₃ ,
      ⇛-· (⇛-· t₁₂⇛u₁ t₃₂⇛u₃)  (⇛-· t₂₂⇛u₂ t₃₂⇛u₃)
⇛-CR (⇛-· ⇛-refl _) (⇛-Kred s₁⇛t₂₁) =
  _ , ⇛-Kred s₁⇛t₂₁ , ⇛-refl
⇛-CR (⇛-· (⇛-· ⇛-refl s₁⇛t₁₁) _) (⇛-Kred s₁⇛t₂₁) =
  let u₁ , t₁₁⇛u₁ , t₂₁⇛u₁ = ⇛-CR s₁⇛t₁₁ s₁⇛t₂₁
  in  u₁ , ⇛-Kred t₁₁⇛u₁ , t₂₁⇛u₁
{-# CATCHALL #-}
⇛-CR (⇛-· s₁⇛t₁₁ s₂⇛t₂₁) (⇛-· s₁⇛t₁₂ s₂⇛t₂₂) =
  let u₁ , t₁₁⇛u₁ , t₁₂⇛u₁ = ⇛-CR s₁⇛t₁₁ s₁⇛t₁₂
      u₂ , t₂₁⇛u₂ , t₂₂⇛u₂ = ⇛-CR s₂⇛t₂₁ s₂⇛t₂₂
  in  u₁ · u₂ , ⇛-· t₁₁⇛u₁ t₂₁⇛u₂ , ⇛-· t₁₂⇛u₁ t₂₂⇛u₂
{-# CATCHALL #-}
⇛-CR s⇛t₁ ⇛-refl = _ , ⇛-refl , s⇛t₁

⇛-⇛*-CR : ∀ {s t₁ t₂} → s ⇛≤ t₁ → s ⇛≥* t₂ → ∃ λ u → t₁ ⇛≥* u × t₂ ⇛≤ u
⇛-⇛*-CR s⇛≤t  ε                 = _ , ε , s⇛≤t
⇛-⇛*-CR s⇛≤u₁ (s⇛≥t₁ ◅ t₁⇛≥*t₂) =
  let u₂ , u₁⇛≥u₂  , t₁⇛≤u₂ = ⇛-CR    s⇛≤u₁  s⇛≥t₁
      u₃ , u₂⇛≥*u₃ , t₂⇛≤u₃ = ⇛-⇛*-CR t₁⇛≤u₂ t₁⇛≥*t₂
  in  u₃ , u₁⇛≥u₂ ◅ u₂⇛≥*u₃ , t₂⇛≤u₃

⇛*-CR : ∀ {s t₁ t₂} → s ⇛≤* t₁ → s ⇛≥* t₂ → ∃ λ u → t₁ ⇛≥* u × t₂ ⇛≤* u
⇛*-CR ε                 s⇛≥*t  = _ , s⇛≥*t , ε
⇛*-CR (s⇛≤t₁ ◅ t₁⇛≤*t₂) s⇛≥*u₁ =
  let u₂ , t₁⇛≥*u₂ , u₁⇛≤u₂  = ⇛-⇛*-CR s⇛≤t₁   s⇛≥*u₁
      u₃ , t₂⇛≥*u₃ , u₂⇛≤*u₃ = ⇛*-CR   t₁⇛≤*t₂ t₁⇛≥*u₂
  in  u₃ , t₂⇛≥*u₃ , u₁⇛≤u₂ ◅ u₂⇛≤*u₃

-- Thanks to Church-Rosser, thee combined multi-step reduction is
-- transitive.

⇛≤*≤⇚-trans : ∀ {s t u} → s ⇛≤*≤⇚ t → t ⇛≤*≤⇚ u → s ⇛≤*≤⇚ u
⇛≤*≤⇚-trans (v , s⇛≤*v , t⇛≥*v) (w , t⇛≤*w , u⇛≥*w) =
  let u′ , w⇛≥*u′ , v⇛≤*u′ = ⇛*-CR t⇛≤*w t⇛≥*v
  in u′ , (s⇛≤*v ◅◅ v⇛≤*u′ , u⇛≥*w ◅◅ w⇛≥*u′)

-- The order on SK? terms is a subrelation of the combined multi-step
-- reduction (modulo squashing).
--
-- The two orders are in fact equivalent, but we don't need that
-- result here, so we omit its proof.  Instead we will establish that
-- the two relations are both equivalent to _≡SK_ on pure SK terms
-- (see inject-⇛≤*≤⇚-≡SK below).

≤SK?--⇛≤*≤⇚ : ∀ {s t} → s ≤SK? t → s ⇛≤*≤⇚ t
≤SK?--⇛≤*≤⇚ ≤?-refl = (_ , ε , ε)
≤SK?--⇛≤*≤⇚ (≤?-trans s≤t t≤u) =
  ⇛≤*≤⇚-trans (≤SK?--⇛≤*≤⇚ s≤t) (≤SK?--⇛≤*≤⇚ t≤u)
≤SK?--⇛≤*≤⇚ ≤?-⊥ = (_ , ⇛-⊥ ◅ ε , ε)
≤SK?--⇛≤*≤⇚ ≤?-⊤ = (_ , ε , ⇛-⊤ ◅ ε)
≤SK?--⇛≤*≤⇚ ≤?-Sred = _ , ⇛-Sred ⇛-refl ⇛-refl ⇛-refl ◅ ε , ε
≤SK?--⇛≤*≤⇚ ≤?-Kred = _ , ⇛-Kred ⇛-refl ◅ ε , ε
≤SK?--⇛≤*≤⇚ ≤?-Sexp = _ , ε , ⇛-Sred ⇛-refl ⇛-refl ⇛-refl ◅ ε
≤SK?--⇛≤*≤⇚ ≤?-Kexp = _ , ε , ⇛-Kred ⇛-refl ◅ ε
≤SK?--⇛≤*≤⇚ (≤?-· s₁≤t₁ s₂≤t₂) =
  let u₁ , s₁⇛u₁ , t₁⇛u₁ = ≤SK?--⇛≤*≤⇚ s₁≤t₁
      u₂ , s₂⇛u₂ , t₂⇛u₂ = ≤SK?--⇛≤*≤⇚ s₂≤t₂
  in u₁ · u₂ , ⇛*-· s₁⇛u₁ s₂⇛u₂ , ⇛*-· t₁⇛u₁ t₂⇛u₂

-- Reduction preserves pure terms.

⇛-Pure : ∀ {ab s t} (ps : Pure s) → s ⇛[ ab ] t →
         ∃ λ pt → inject⁻¹ ps ≡SK inject⁻¹ {t} pt
⇛-Pure p ⇛-refl = p , ≡-refl
⇛-Pure (S · ps₁ · pt₁ · pu₁) (⇛-Sred s₁⇛s₂ t₁⇛t₂ u₁⇛u₂) =
  let ps₂ , s₁≡s₂ = ⇛-Pure ps₁ s₁⇛s₂
      pt₂ , t₁≡t₂ = ⇛-Pure pt₁ t₁⇛t₂
      pu₂ , u₁≡u₂ = ⇛-Pure pu₁ u₁⇛u₂
  in ps₂ · pu₂ · (pt₂ · pu₂) ,
     ≡-trans (≡-· (≡-· (≡-· ≡-refl s₁≡s₂) t₁≡t₂) u₁≡u₂) ≡-Sred
⇛-Pure (K · ps₁ · _) (⇛-Kred s₁⇛s₂) =
  let ps₂ , s₁≡s₂ = ⇛-Pure ps₁ s₁⇛s₂
  in ps₂ , ≡-trans ≡-Kred s₁≡s₂
⇛-Pure (ps · pt) (⇛-· s₁⇛s₂ t₁⇛t₂)  =
  Prod.zip _·_ ≡-· (⇛-Pure ps s₁⇛s₂) (⇛-Pure pt t₁⇛t₂)

⇛*-Pure : ∀ {ab s t} (ps : Pure s) → s ⇛[ ab ]* t →
          ∃ λ pt → inject⁻¹ ps ≡SK inject⁻¹ {t} pt
⇛*-Pure p  ε            = p , ≡-refl
⇛*-Pure ps (s⇛t ◅ t⇛*u) =
  let pt , s≡t = ⇛-Pure  ps s⇛t
      pu , t≡u = ⇛*-Pure pt t⇛*u
  in pu , ≡-trans s≡t t≡u

-- The combined multi-step reduction is a subrelation of ≡SK on pure terms.

inject-⇛≤*≤⇚-≡SK : ∀ {s t} → inject s ⇛≤*≤⇚ inject t → s ≡SK t
inject-⇛≤*≤⇚-≡SK {s} {t} (u , s⇛≤*u , t⇛≥*u) =
  let pu  , s≡u = ⇛*-Pure (inject-Pure s) s⇛≤*u
      pu′ , t≡u = ⇛*-Pure (inject-Pure t) t⇛≥*u
  in ≡-trans (subst (_≡SK (inject⁻¹ pu)) (inject⁻¹-inject-Pure s) s≡u)
             (subst₂ (_≡SK_) (inject⁻¹-unique pu′ pu) (inject⁻¹-inject-Pure t)
                     (≡-sym t≡u))

-- The order on SK? terms is a subrelation of the equality on pure SK
-- terms.
--
-- NOTE. This establishes a circular equivalence between the three
-- relations _≡SK_, _⇛≤*≤⇚_ and _≤SK?_ when restricted to pure SK
-- terms:
--
--           _≡SK_  ⊆  _≤SK?_  ⊆  _⇛≤*≤⇚_  ⊆  _≡SK_
--
-- This equivalence will allow us to encode/extract equivalence proofs
-- on (pure) SK terms from typing derivations.

inject-≤SK?-≡SK : ∀ {s t} → inject s ≤SK? inject t → s ≡SK t
inject-≤SK?-≡SK {s} {t} s≤t = inject-⇛≤*≤⇚-≡SK (≤SK?--⇛≤*≤⇚ s≤t)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


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

   Copyright (c) 2020 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 Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Hash
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS

open import LibraBFT.Abstract.Types
open EpochConfig

open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle sha256 sha256-cr

open import LibraBFT.Concrete.System.Parameters

open import LibraBFT.Yasm.Base
open import LibraBFT.Yasm.AvailableEpochs using (AvailableEpochs ; lookup'; lookup'')
open import LibraBFT.Yasm.System     ConcSysParms
open import LibraBFT.Yasm.Properties ConcSysParms

-- In this module, we define two "implementation obligations"
-- (ImplObligationᵢ for i ∈ {1 , 2}), which are predicates over
-- reachable states of a system defined by
-- 'LibraBFT.Concrete.System.Parameters'.  These two properties relate
-- votes sent by the same sender, ensuring that if they are for the
-- same epoch and round, then they vote for the same blockID; the
-- first relates a vote output by the handler to a vote sent
-- previously, and the second relates two votes both sent by the
-- handler.
--
-- We then prove that, if an implementation satisfies these two
-- semantic obligations, along with a structural one about messages
-- sent by honest peers in the implementation, then the implemenation
-- satisfies the LibraBFT.Abstract.Properties.VotesOnce invariant.
module LibraBFT.Concrete.Properties.VotesOnce where

 -- TODO-3: This may not be the best way to state the implementation obligation.  Why not reduce
 -- this as much as possible before giving the obligation to the implementation?  For example, this
 -- will still require the implementation to deal with hash collisons (v and v' could be different,
 -- but yield the same bytestring and therefore same signature).  Also, avoid the need for the
 -- implementation to reason about messages sent by step-cheat, or give it something to make this
 -- case easy to eliminate.

 ImplObligation₁ : Set₁
 ImplObligation₁ =
   ∀{e pid sndr s' outs pk}{pre : SystemState e}
   → ReachableSystemState pre
   -- For any honest call to /handle/ or /init/,
   → StepPeerState pid (availEpochs pre) (msgPool pre) (Map-lookup pid (peerStates pre)) s' outs
   → ∀{v m v' m'} → Meta-Honest-PK pk
   -- For signed every vote v of every outputted message
   → v  ⊂Msg m  → m ∈ outs → (sig : WithVerSig pk v)
   -- If v is really new and valid
     -- Note that this does not directly exclude possibility of previous message with
     -- same signature, but sent by someone else.  We could prove it implies it though.
   → ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool pre)) → ValidPartForPK (availEpochs pre) v pk
   -- And if there exists another v' that has been sent before
   → v' ⊂Msg m' → (sndr , m') ∈ (msgPool pre) → WithVerSig pk v'
   -- If v and v' share the same epoch and round
   → (v ^∙ vEpoch) ≡ (v' ^∙ vEpoch)
   → (v ^∙ vProposed ∙ biRound) ≡ (v' ^∙ vProposed ∙ biRound)
   ----------------------------------------------------------
   -- Then an honest implemenation promises v and v' vote for the same blockId.
   → (v ^∙ vProposed ∙ biId) ≡ (v' ^∙ vProposed ∙ biId)

 ImplObligation₂ : Set₁
 ImplObligation₂ =
   ∀{e pid s' outs pk}{pre : SystemState e}
   → ReachableSystemState pre
   -- For any honest call to /handle/ or /init/,
   → StepPeerState pid (availEpochs pre) (msgPool pre) (Map-lookup pid (peerStates pre)) s' outs
   → ∀{v m v' m'} → Meta-Honest-PK pk
   -- For every vote v represented in a message output by the call
   → v  ⊂Msg m  → m ∈ outs → (sig : WithVerSig pk v)
   -- If v is really new and valid
   → ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool pre)) → ValidPartForPK (availEpochs pre) v pk

   -- And if there exists another v' that is also new and valid
   → v' ⊂Msg m'  → m' ∈ outs → (sig' : WithVerSig pk v')
   → ¬ (MsgWithSig∈ pk (ver-signature sig') (msgPool pre)) → ValidPartForPK (availEpochs pre) v' pk

   -- If v and v' share the same epoch and round
   → (v ^∙ vEpoch) ≡ (v' ^∙ vEpoch)
   → (v ^∙ vProposed ∙ biRound) ≡ (v' ^∙ vProposed ∙ biRound)
   ----------------------------------------------------------
   -- Then, an honest implemenation promises v and v' vote for the same blockId.
   → (v ^∙ vProposed ∙ biId) ≡ (v' ^∙ vProposed ∙ biId)

 -- Next, we prove that, given the necessary obligations,
 module Proof
   (sps-corr : StepPeerState-AllValidParts)
   (Impl-VO1 : ImplObligation₁)
   (Impl-VO2 : ImplObligation₂)
   where

  -- Any reachable state satisfies the VO rule for any epoch in the system.
  module _ {e}(st : SystemState e)(r : ReachableSystemState st)(eid : Fin e) where
   -- Bring in 'unwind', 'ext-unforgeability' and friends
   open Structural sps-corr

   -- Bring in ConcSystemState
   open import LibraBFT.Concrete.System sps-corr
   open PerState st r
   open PerEpoch eid

   open import LibraBFT.Abstract.Obligations.VotesOnce 𝓔 Hash _≟Hash_ (ConcreteVoteEvidence 𝓔) as VO

   -- The VO proof is done by induction on the execution trace leading to 'st'. In
   -- Agda, this is 'r : RechableSystemState st' above. We will use induction to
   -- construct a predicate Pred'' below, which holds for every state on the trace.

   private
    -- First we specify the predicate we need: it relates two votes verified
    -- by the same public key, such that both are elements of the same message pool
    Pred'' : PK → Vote → Vote → SentMessages → Set
    Pred'' pk v v' pool
      = Meta-Honest-PK pk
      → (ver  : WithVerSig pk v)  → MsgWithSig∈ pk (ver-signature ver) pool
      → (ver' : WithVerSig pk v') → MsgWithSig∈ pk (ver-signature ver') pool
      → v ^∙ vEpoch ≡ v' ^∙ vEpoch
      → v ^∙ vRound ≡ v' ^∙ vRound
      → v ^∙ vProposedId ≡ v' ^∙ vProposedId

    -- Usually, we want to universally quantify Pred'' over arbitrary votes and pks
    Pred' : SentMessages → Set
    Pred' pool = ∀{pk}{v v' : Vote} → Pred'' pk v v' pool

    -- Finally, we state Pred' in terms of SystemSate
    Pred : ∀{e} → SystemState e → Set
    Pred = Pred' ∘ msgPool

    -------------------
    -- * Base Case * --
    -------------------

    -- Pred above is trivially true for the initial state: there are no messages in the pool
    Pred₀ : Pred initialState
    Pred₀ _ _ ()

    --------------------------------------------------
    -- * Inductive Case: New Epochs in the System * --
    --------------------------------------------------

    -- Because pushEpoch does not alter the msgPool, the proof is trivial.
    Pred𝓔 : ∀{e}{st : SystemState e}(𝓔 : EpochConfigFor e) → Pred st → Pred (pushEpoch 𝓔 st)
    Pred𝓔 𝓔 p = p

    ----------------------------------------------
    -- * Inductive Case: Transition by a Peer * --
    ----------------------------------------------

    -- From this point onwards, it might be easier to read this proof starting at 'voo'
    -- at the end of the file. Next, we provide an overview the proof.
    --
    -- We wish to prove that, for any two votes v and v' cast by an honest α in the message pool of
    -- a state st, if v and v' have equal rounds and epochs, then they vote for the same block. As
    -- we have seen above, the base case and the case for a new epoch in the system are
    -- trivial. Next, we look at the PeerStep case.
    --
    -- The induction hypothesis tells us that the property holds in the pre-state.  Next, we reason
    -- about the post-state.  We start by analyzing whether v and v' have been sent as outputs of
    -- the PeerStep under scrutiny or were already in the pool before (captured by the PredStep
    -- function).  There are four possibilities:
    --
    --   i) v and v' were aleady present in the msgPool before: use induction hypothesis.
    --  ii) v and v' are both in the output produced by the PeerStep under scrutiny.
    -- iii) v was present before, but v' is new.
    --  iv) v' was present before, but v is new.
    --
    -- Case (i) is trivial; cases (iii) and (iv) are symmetric and reduce to an implementation
    -- obligation (Impl-VO1) and case (ii) reduces to a different implementation obligation (Impl-VO2).
    --
    -- The proofs of cases (iii) and (iv) are in PredStep-wlog-ht and PredStep-wlog-ht'.  The 'ht'
    -- suffix refers to 'Here-There' as in one vote is "here" and the other is old, or "there".  We
    -- first analyze whether the new vote is really new or a replay; sps-cor provides us this
    -- information.  If the new vote is, in fact, a replay of an old message, we have two old
    -- messages and can call the induction hypothesis. If it is really new, we must rely on the
    -- implementation obligation. But to do so, we must prove that the old vote was also sent by
    -- the same peer.  We can see that is the case by reasoning about PK-inj and IsValidEpochMember.
    --
    -- Finally, the proof of case (ii) also branches on whether either of the "new" votes
    -- are replays or are really new. In case at least one is a replay we fallback to cases (iii) and (iv)
    -- or just call the induction hypothesis when both are replays.
    -- When both votes are in fact new, we rely on Impl-VO2 to conclude.
    --
    -- In both PredSetp-wlog-ht and PredStep-wlog-hh, we must eliminate the possibility of
    -- either vote being produced by a cheat step. This is easy because we received
    -- a proof that the PK in question is honest, hence, it must be the case that a cheat
    -- step is at most replaying these votes, not producing them. Producing them would
    -- require the cheater to forge a signature. This is the purpose of the isCheat constraint.

    PredStep-wlog-ht' : ∀{e pid pid' s' outs pk}{pre : SystemState e}
            → ReachableSystemState pre
            → Pred pre
            → StepPeerState pid (availEpochs pre) (msgPool pre) (Map-lookup pid (peerStates pre)) s' outs
            → ∀{v m v' m'}
            → v  ⊂Msg m  → m ∈ outs
            → v' ⊂Msg m' → (pid' , m') ∈ msgPool pre
            → WithVerSig pk v → WithVerSig pk v' → Meta-Honest-PK pk
            → (v ^∙ vEpoch) ≡ (v' ^∙ vEpoch)
            → (v ^∙ vProposed ∙ biRound) ≡ (v' ^∙ vProposed ∙ biRound)
            → (v ^∙ vProposed ∙ biId) ≡ (v' ^∙ vProposed ∙ biId)
    PredStep-wlog-ht' {pre = pre} preach hip ps {v} v⊂m m∈outs v'⊂m' m'∈pool ver ver' hpk eids≡ r≡
    -- (1) The first step is branching on whether 'v' above is a /new/ vote or not.
    -- (1.1) If it's new:
      with sps-corr preach hpk ps m∈outs v⊂m ver
    ...| inj₁ (vValid , vNew)
      with honestPartValid preach hpk v'⊂m' m'∈pool ver'
    ...| v'Old , vOldValid
      with sameHonestSig⇒sameVoteData hpk ver' (msgSigned v'Old) (sym (msgSameSig v'Old))
    ...| inj₁ abs  = ⊥-elim (meta-sha256-cr abs)
    ...| inj₂ refl = Impl-VO1 preach ps hpk v⊂m m∈outs ver vNew vValid
                       (msg⊆ v'Old) (msg∈pool v'Old)
                       (msgSigned v'Old) eids≡ r≡
    -- (1.1) If 'v' is not new, then there exists a msg sent with the
    -- same signature.
    PredStep-wlog-ht' preach hip ps {v} v⊂m m∈outs v'⊂m' m'∈pool ver ver' hpk e≡ r≡
       | inj₂ vOld
      with honestPartValid preach hpk v'⊂m' m'∈pool ver'
    ...| sv' , _ = hip hpk ver vOld ver' sv' e≡ r≡

    -- Here we prove a modified version of Pred'' where we assume w.l.o.g that
    -- one vote is sent by "pstep" and another was present in the prestate.
    PredStep-wlog-ht
      : ∀{e pid st' outs}{pre : SystemState e}
      → ReachableSystemState pre
      → (pstep : StepPeer pre pid st' outs)
      → Pred pre
      → ∀{pk v v'}
      -- Below is a inline expansion of "Pred'' pk v v' (msgPool (StepPeer-post pstep))",
      -- but with the added information that one vote (v) was sent by pstep whereas the
      -- other (v') was in the pool of the prestate.
      → let pool = msgPool (StepPeer-post pstep)
         in Meta-Honest-PK pk
          → (ver  : WithVerSig pk v )(sv  : MsgWithSig∈ pk (ver-signature ver ) pool)
          → (msgSender sv , msgWhole sv) ∈ List-map (pid ,_) outs
          → (ver' : WithVerSig pk v')(sv' : MsgWithSig∈ pk (ver-signature ver') pool)
          → (msgSender sv' , msgWhole sv') ∈ msgPool pre
          → v ^∙ vEpoch ≡ v' ^∙ vEpoch
          → v ^∙ vRound ≡ v' ^∙ vRound
          → v ^∙ vProposedId ≡ v' ^∙ vProposedId
    PredStep-wlog-ht preach (step-cheat fm isCheat) hip hpk ver sv (here refl) ver' sv' furtherBack' epoch≡ r≡
      with isCheat (msg⊆ sv) (msgSigned sv)
    ...| inj₁ abs    = ⊥-elim (hpk abs) -- The key was honest by hypothesis.
    ...| inj₂ sentb4
       -- the cheater replayed the message; which means the message was sent before this
       -- step; hence, call induction hypothesis.
      with msgSameSig sv
    ...| refl = hip hpk ver sentb4 ver' (MsgWithSig∈-transp sv' furtherBack') epoch≡ r≡
    PredStep-wlog-ht preach (step-honest x) hip hpk ver sv thisStep ver' sv' furtherBack' epoch≡ r≡
      with sameHonestSig⇒sameVoteData hpk ver (msgSigned sv) (sym (msgSameSig sv))
    ...| inj₁ abs  = ⊥-elim (meta-sha256-cr abs)
    ...| inj₂ refl
      with sameHonestSig⇒sameVoteData hpk ver' (msgSigned sv') (sym (msgSameSig sv'))
    ...| inj₁ abs  = ⊥-elim (meta-sha256-cr abs)
    ...| inj₂ refl
       = PredStep-wlog-ht' preach hip x
                 (msg⊆ sv) (Any-map (cong proj₂) (Any-map⁻ thisStep))
                 (msg⊆ sv') furtherBack'
                 (msgSigned sv) (msgSigned sv') hpk epoch≡ r≡

    -- Analogous to PredStep-wlog-ht', but here we must reason about two messages that are in the
    -- outputs of a step.
    PredStep-hh' : ∀{e pid s' outs pk}{pre : SystemState e}
            → ReachableSystemState pre → Pred pre
            → StepPeerState pid (availEpochs pre) (msgPool pre) (Map-lookup pid (peerStates pre)) s' outs
            → ∀{v m v' m'}
            → v  ⊂Msg m  → m  ∈ outs
            → v' ⊂Msg m' → m' ∈ outs
            → WithVerSig pk v → WithVerSig pk v' → Meta-Honest-PK pk
            → (v ^∙ vEpoch) ≡ (v' ^∙ vEpoch)
            → (v ^∙ vProposed ∙ biRound) ≡ (v' ^∙ vProposed ∙ biRound)
            → (v ^∙ vProposed ∙ biId) ≡ (v' ^∙ vProposed ∙ biId)
    -- Since the step is from an honest peer, we can check whether the messages are in fact
    -- new or not.
    PredStep-hh' preach hip ps {v} v⊂m m∈outs v'⊂m' m'∈outs ver ver' hpk e≡ r≡
      with sps-corr preach hpk ps m∈outs v⊂m ver | sps-corr preach hpk ps m'∈outs v'⊂m' ver'
    -- (A) Both are old: call induction hypothesis
    ...| inj₂ vOld            | inj₂ v'Old = hip hpk ver vOld ver' v'Old e≡ r≡

    -- (B) One is new, one is old: use PredStep-wlog-ht'
    PredStep-hh' preach hip ps {v} v⊂m m∈outs v'⊂m' m'∈outs ver ver' hpk e≡ r≡
       | inj₁ (vValid , vNew) | inj₂ v'Old
      with sameHonestSig⇒sameVoteData hpk ver' (msgSigned v'Old) (sym (msgSameSig v'Old))
    ...| inj₁ abs  = ⊥-elim (meta-sha256-cr abs)
    ...| inj₂ refl
       = PredStep-wlog-ht' preach hip ps v⊂m m∈outs (msg⊆ v'Old) (msg∈pool v'Old) ver (msgSigned v'Old) hpk e≡ r≡

    -- (C) One is old, one is new: use PredStep-wlog-ht'
    PredStep-hh' preach hip ps {v} v⊂m m∈outs v'⊂m' m'∈outs ver ver' hpk e≡ r≡
       | inj₂ vOld            | inj₁ (v'Valid , v'New)
      with sameHonestSig⇒sameVoteData hpk ver (msgSigned vOld) (sym (msgSameSig vOld))
    ...| inj₁ abs  = ⊥-elim (meta-sha256-cr abs)
    ...| inj₂ refl
       = sym (PredStep-wlog-ht' preach hip ps v'⊂m' m'∈outs (msg⊆ vOld) (msg∈pool vOld) ver' (msgSigned vOld) hpk (sym e≡) (sym r≡))

    -- (D) Finally, both votes are new in this step. The proof is then trivially
    -- forwarded to the implementation obligation.
    PredStep-hh' preach hip ps {v} v⊂m m∈outs v'⊂m' m'∈outs ver ver' hpk e≡ r≡
       | inj₁ (vValid , vNew) | inj₁ (v'Valid , v'New)
       = Impl-VO2 preach ps hpk v⊂m m∈outs ver vNew vValid v'⊂m' m'∈outs ver' v'New v'Valid e≡ r≡

    PredStep-hh
      : ∀{e pid st' outs}{pre : SystemState e}
      → ReachableSystemState pre
      → (pstep : StepPeer pre pid st' outs)
      → Pred pre
      → ∀{pk v v'}
      → let pool = msgPool (StepPeer-post pstep)
         in Meta-Honest-PK pk
          → (ver  : WithVerSig pk v )(sv  : MsgWithSig∈ pk (ver-signature ver ) pool)
          → (msgSender sv  , msgWhole sv)  ∈ List-map (pid ,_) outs
          → (ver' : WithVerSig pk v')(sv' : MsgWithSig∈ pk (ver-signature ver') pool)
          → (msgSender sv' , msgWhole sv') ∈ List-map (pid ,_) outs
          → v ^∙ vEpoch ≡ v' ^∙ vEpoch
          → v ^∙ vRound ≡ v' ^∙ vRound
          → v ^∙ vProposedId ≡ v' ^∙ vProposedId
    PredStep-hh preach (step-cheat fm isCheat) hip hpk ver sv (here refl) ver' sv' (here refl) epoch≡ r≡
      with isCheat (msg⊆ sv) (msgSigned sv)
    ...| inj₁ abs    = ⊥-elim (hpk abs) -- The key was honest by hypothesis.
    ...| inj₂ sentb4
      with isCheat (msg⊆ sv') (msgSigned sv')
    ...| inj₁ abs     = ⊥-elim (hpk abs) -- The key was honest by hypothesis.
    ...| inj₂ sentb4'
      with msgSameSig sv | msgSameSig sv'
    ...| refl | refl = hip hpk ver sentb4 ver' sentb4' epoch≡ r≡
    PredStep-hh preach (step-honest x) hip hpk ver sv thisStep ver' sv' thisStep' epoch≡ r≡
      with sameHonestSig⇒sameVoteData hpk ver (msgSigned sv) (sym (msgSameSig sv))
    ...| inj₁ abs  = ⊥-elim (meta-sha256-cr abs)
    ...| inj₂ refl
      with sameHonestSig⇒sameVoteData hpk ver' (msgSigned sv') (sym (msgSameSig sv'))
    ...| inj₁ abs  = ⊥-elim (meta-sha256-cr abs)
    ...| inj₂ refl
       = PredStep-hh' preach hip x
                 (msg⊆ sv ) (Any-map (cong proj₂) (Any-map⁻ thisStep))
                 (msg⊆ sv') (Any-map (cong proj₂) (Any-map⁻ thisStep'))
                 (msgSigned sv) (msgSigned sv') hpk epoch≡ r≡

    PredStep : ∀{e pid st' outs}{pre : SystemState e}
             → ReachableSystemState pre
             → (pstep : StepPeer pre pid st' outs)
             → Pred pre
             → Pred (StepPeer-post pstep)
    PredStep {e} {pid} {st'} {outs} {pre} preach pstep hip hpk ver sv ver' sv' epoch≡ r≡
    -- First we check when have the votes been sent:
      with Any-++⁻ (List-map (pid ,_) outs) {msgPool pre} (msg∈pool sv)
         | Any-++⁻ (List-map (pid ,_) outs) {msgPool pre} (msg∈pool sv')
    -- (A) Neither vote has been sent by the step under scrutiny: invoke inductive hypothesis
    ...| inj₂ furtherBack | inj₂ furtherBack'
       = hip hpk ver  (MsgWithSig∈-transp sv furtherBack)
                 ver' (MsgWithSig∈-transp sv' furtherBack') epoch≡ r≡
    -- (B) One vote was cast here; the other was cast in the past.
    PredStep {e} {pid} {st'} {outs} {pre} preach pstep hip hpk ver sv ver' sv' epoch≡ r≡
       | inj₁ thisStep    | inj₂ furtherBack'
       = PredStep-wlog-ht preach pstep hip hpk ver sv thisStep ver' sv' furtherBack' epoch≡ r≡
    -- (C) Symmetric to (B)
    PredStep {e} {pid} {st'} {outs} {pre} preach pstep hip hpk ver sv ver' sv' epoch≡ r≡
       | inj₂ furtherBack | inj₁ thisStep'
       = sym (PredStep-wlog-ht preach pstep hip hpk ver' sv' thisStep' ver sv furtherBack (sym epoch≡) (sym r≡))
    -- (D) Both votes were cast here
    PredStep {e} {pid} {st'} {outs} {pre} preach pstep hip hpk ver sv ver' sv' epoch≡ r≡
       | inj₁ thisStep    | inj₁ thisStep'
       = PredStep-hh preach pstep hip hpk ver sv thisStep ver' sv' thisStep' epoch≡ r≡

   voo : VO.Type ConcSystemState
   voo hpk refl sv refl sv' round≡
     with Step*-Step-fold Pred (λ {e} {st} _ → Pred𝓔 {e} {st}) PredStep Pred₀ r
   ...| res
     with vmsg≈v (vmFor sv) | vmsg≈v (vmFor sv')
   ...| refl | refl
      = res hpk (vmsgSigned (vmFor sv))
                (mkMsgWithSig∈ (nm (vmFor sv)) (cv (vmFor sv)) (cv∈nm (vmFor sv))
                               _ (nmSentByAuth sv) (vmsgSigned (vmFor sv)) refl)
                (vmsgSigned (vmFor sv'))
                (mkMsgWithSig∈ (nm (vmFor sv')) (cv (vmFor sv')) (cv∈nm (vmFor sv'))
                               _ (nmSentByAuth sv') (vmsgSigned (vmFor sv')) refl)
                (trans (vmsgEpoch (vmFor sv)) (sym (vmsgEpoch (vmFor sv'))))
                round≡


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

data D : Set → Set₁ where
  c : (@0 A : Set) → D A


text:
module ANF where

open import Data.List
open import Data.List.All

open import Typing
open import DSyntax
open import Syntax

-- transform a direct style expression into and anf expression

anf : ∀ {φ t} → DExpr φ t → Expr φ t
anf (var x) = var x
anf (nat unr-φ i) = nat unr-φ i
anf (unit unr-φ) = unit unr-φ
anf (pair sp de de₁) = letbind sp (anf de) (letbind (rght (split-all-left _)) (anf de₁) (pair (rght (left [])) (here []) (here [])))
anf (letpair sp de de₁) = letbind sp (anf de) (letpair (left (split-all-right _)) (here []) (anf de₁))
anf (fork de) = fork (anf de)
anf (new unr-φ s) = new unr-φ s
anf (send sp de de₁) = letbind sp (anf de) (letbind (rght (split-all-left _)) (anf de₁) (send (rght (left [])) (here []) (here [])))
anf (recv de) = letbind (split-all-left _) (anf de) (recv (here []))
anf (close de) = letbind (split-all-left _) (anf de) (close (here []))
anf (wait de) = letbind (split-all-left _) (anf de) (wait (here []))
anf (select lab de) = letbind (split-all-left _) (anf de) (select lab (here []))
anf (branch sp de de₁ de₂) = letbind sp (anf de) (branch (left (split-all-right _)) (here []) (anf de₁) (anf de₂))
anf (ulambda unr-φ de) = ulambda (split-all-left _) unr-φ [] (anf de)
anf (llambda de) = llambda (split-all-left _) [] (anf de)
anf (app sp de de₁) = letbind sp (anf de) (letbind (rght (split-all-left _)) (anf de₁) (app (rght (left [])) (here []) (here [])))
anf (subsume de t≤t') = subsume (anf de) t≤t'

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


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

open import homotopy.3x3.Common
open import homotopy.3x3.PushoutPushout

module homotopy.3x3.Transpose where

open M using (Pushout^2)

type-of : ∀ {i} {A : Type i} (u : A) → Type i
type-of {A = A} _ = A

module _ {i} (d : Span^2 {i}) where

  open Span^2 d

  transpose-f : (f : type-of H₁₁ → _) (g : type-of H₃₃ → _) → Span^2
  transpose-f f g = span^2 A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄
                     f₁₀ f₃₀ f₁₂ f₃₂ f₁₄ f₃₄ f₀₁ f₀₃ f₂₁ f₂₃ f₄₁ f₄₃
                     (f H₁₁) H₃₁ H₁₃ (g H₃₃)

  transpose : Span^2
  transpose = span^2 A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄
                     f₁₀ f₃₀ f₁₂ f₃₂ f₁₄ f₃₄ f₀₁ f₀₃ f₂₁ f₂₃ f₄₁ f₄₃
                     (! ∘ H₁₁) H₃₁ H₁₃ (! ∘ H₃₃)

ch1 : ∀ {i j} {A : Type i} {x y : A} {p : x == y} {f g : A → Type j} {a : f x → g x} {b : f y → g y}
  → (a == b [ (λ u → f u → g u) ↓ p ]) → (a == b [ (λ u → fst u → snd u) ↓ pair×= (ap f p) (ap g p)])
ch1 {p = idp} α = α

ch2 : ∀ {i j} {X : Type i} {x y : X} {p : x == y}
  {A B₁ B₂ C : X → Type j}
  {f₁ : (x : X) → A x → B₁ x} {g₁ : (x : X) → B₁ x → C x}
  {f₂ : (x : X) → A x → B₂ x} {g₂ : (x : X) → B₂ x → C x}
  {a : _} {b : _}
  → (a == b [ (λ z → (x : A z) → g₁ z (f₁ z x) == g₂ z (f₂ z x)) ↓ p ])
  → (a == b [ (λ u → (x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x))
            ↓ square=-raw (ap A p) (ap B₁ p) (ap B₂ p) (ap C p) (ch1 (apd f₁ p)) (ch1 (apd f₂ p)) (ch1 (apd g₁ p)) (ch1 (apd g₂ p)) ])
ch2 {p = idp} α = α

ap-span^2=-priv : ∀ {i} {d d' : Span^2 {i}} (p : d == d')
    → ap transpose p == span^2=-raw (ap Span^2.A₀₀ p) (ap Span^2.A₂₀ p) (ap Span^2.A₄₀ p)
                                    (ap Span^2.A₀₂ p) (ap Span^2.A₂₂ p) (ap Span^2.A₄₂ p)
                                    (ap Span^2.A₀₄ p) (ap Span^2.A₂₄ p) (ap Span^2.A₄₄ p)
                                    (ch1 (apd Span^2.f₁₀ p)) (ch1 (apd Span^2.f₃₀ p))
                                    (ch1 (apd Span^2.f₁₂ p)) (ch1 (apd Span^2.f₃₂ p))
                                    (ch1 (apd Span^2.f₁₄ p)) (ch1 (apd Span^2.f₃₄ p))
                                    (ch1 (apd Span^2.f₀₁ p)) (ch1 (apd Span^2.f₀₃ p))
                                    (ch1 (apd Span^2.f₂₁ p)) (ch1 (apd Span^2.f₂₃ p))
                                    (ch1 (apd Span^2.f₄₁ p)) (ch1 (apd Span^2.f₄₃ p))
                                    (ch2 (ap↓ (λ u → ! ∘ u) (apd Span^2.H₁₁ p))) (ch2 (apd Span^2.H₃₁ p))
                                    (ch2 (apd Span^2.H₁₃ p)) (ch2 (ap↓ (λ u → ! ∘ u) (apd Span^2.H₃₃ p)))
ap-span^2=-priv {i} {d} {.d} idp = idp

ap-span^2=-priv2 : ∀ {i}
  {A₀₀ A₀₀' : Type i} (eq-A₀₀ : A₀₀ == A₀₀')
  {A₀₂ A₀₂' : Type i} (eq-A₀₂ : A₀₂ == A₀₂')
  {A₀₄ A₀₄' : Type i} (eq-A₀₄ : A₀₄ == A₀₄')
  {A₂₀ A₂₀' : Type i} (eq-A₂₀ : A₂₀ == A₂₀')
  {A₂₂ A₂₂' : Type i} (eq-A₂₂ : A₂₂ == A₂₂')
  {A₂₄ A₂₄' : Type i} (eq-A₂₄ : A₂₄ == A₂₄')
  {A₄₀ A₄₀' : Type i} (eq-A₄₀ : A₄₀ == A₄₀')
  {A₄₂ A₄₂' : Type i} (eq-A₄₂ : A₄₂ == A₄₂')
  {A₄₄ A₄₄' : Type i} (eq-A₄₄ : A₄₄ == A₄₄')
  {f₀₁ : A₀₂ → A₀₀} {f₀₁' : A₀₂' → A₀₀'} (eq-f₀₁ : f₀₁ == f₀₁' [ (λ u → fst u → snd u) ↓ pair×= eq-A₀₂ eq-A₀₀ ])
  {f₀₃ : A₀₂ → A₀₄} {f₀₃' : A₀₂' → A₀₄'} (eq-f₀₃ : f₀₃ == f₀₃' [ (λ u → fst u → snd u) ↓ pair×= eq-A₀₂ eq-A₀₄ ])
  {f₂₁ : A₂₂ → A₂₀} {f₂₁' : A₂₂' → A₂₀'} (eq-f₂₁ : f₂₁ == f₂₁' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₂ eq-A₂₀ ])
  {f₂₃ : A₂₂ → A₂₄} {f₂₃' : A₂₂' → A₂₄'} (eq-f₂₃ : f₂₃ == f₂₃' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₂ eq-A₂₄ ])
  {f₄₁ : A₄₂ → A₄₀} {f₄₁' : A₄₂' → A₄₀'} (eq-f₄₁ : f₄₁ == f₄₁' [ (λ u → fst u → snd u) ↓ pair×= eq-A₄₂ eq-A₄₀ ])
  {f₄₃ : A₄₂ → A₄₄} {f₄₃' : A₄₂' → A₄₄'} (eq-f₄₃ : f₄₃ == f₄₃' [ (λ u → fst u → snd u) ↓ pair×= eq-A₄₂ eq-A₄₄ ])
  {f₁₀ : A₂₀ → A₀₀} {f₁₀' : A₂₀' → A₀₀'} (eq-f₁₀ : f₁₀ == f₁₀' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₀ eq-A₀₀ ])
  {f₃₀ : A₂₀ → A₄₀} {f₃₀' : A₂₀' → A₄₀'} (eq-f₃₀ : f₃₀ == f₃₀' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₀ eq-A₄₀ ])
  {f₁₂ : A₂₂ → A₀₂} {f₁₂' : A₂₂' → A₀₂'} (eq-f₁₂ : f₁₂ == f₁₂' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₂ eq-A₀₂ ])
  {f₃₂ : A₂₂ → A₄₂} {f₃₂' : A₂₂' → A₄₂'} (eq-f₃₂ : f₃₂ == f₃₂' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₂ eq-A₄₂ ])
  {f₁₄ : A₂₄ → A₀₄} {f₁₄' : A₂₄' → A₀₄'} (eq-f₁₄ : f₁₄ == f₁₄' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₄ eq-A₀₄ ])
  {f₃₄ : A₂₄ → A₄₄} {f₃₄' : A₂₄' → A₄₄'} (eq-f₃₄ : f₃₄ == f₃₄' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₄ eq-A₄₄ ])
  {H₁₁ : (x : A₂₂) → f₁₀ (f₂₁ x) == f₀₁ (f₁₂ x)} {H₁₁' : (x : A₂₂') → f₁₀' (f₂₁' x) == f₀₁' (f₁₂' x)}
  (eq-H₁₁ : H₁₁ == H₁₁' [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x)))
                        ↓ square=-raw eq-A₂₂ eq-A₂₀ eq-A₀₂ eq-A₀₀ eq-f₂₁ eq-f₁₂ eq-f₁₀ eq-f₀₁ ])
  {H₁₃ : (x : A₂₂) → f₀₃ (f₁₂ x) == f₁₄ (f₂₃ x)} {H₁₃' : (x : A₂₂') → f₀₃' (f₁₂' x) == f₁₄' (f₂₃' x)}
  (eq-H₁₃ : H₁₃ == H₁₃' [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x)))
                        ↓ square=-raw eq-A₂₂ eq-A₀₂ eq-A₂₄ eq-A₀₄ eq-f₁₂ eq-f₂₃ eq-f₀₃ eq-f₁₄ ])
  {H₃₁ : (x : A₂₂) → f₃₀ (f₂₁ x) == f₄₁ (f₃₂ x)} {H₃₁' : (x : A₂₂') → f₃₀' (f₂₁' x) == f₄₁' (f₃₂' x)}
  (eq-H₃₁ : H₃₁ == H₃₁' [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x)))
                        ↓ square=-raw eq-A₂₂ eq-A₂₀ eq-A₄₂ eq-A₄₀ eq-f₂₁ eq-f₃₂ eq-f₃₀ eq-f₄₁ ])
  {H₃₃ : (x : A₂₂) → f₄₃ (f₃₂ x) == f₃₄ (f₂₃ x)} {H₃₃' : (x : A₂₂') → f₄₃' (f₃₂' x) == f₃₄' (f₂₃' x)}
  (eq-H₃₃ : H₃₃ == H₃₃' [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x)))
                        ↓ square=-raw eq-A₂₂ eq-A₄₂ eq-A₂₄ eq-A₄₄ eq-f₃₂ eq-f₂₃ eq-f₄₃ eq-f₃₄ ])
    → ap transpose (span^2=-raw eq-A₀₀ eq-A₀₂ eq-A₀₄ eq-A₂₀ eq-A₂₂ eq-A₂₄ eq-A₄₀ eq-A₄₂ eq-A₄₄ eq-f₀₁ eq-f₀₃ eq-f₂₁ eq-f₂₃ eq-f₄₁ eq-f₄₃ eq-f₁₀ eq-f₃₀ eq-f₁₂ eq-f₃₂ eq-f₁₄ eq-f₃₄ eq-H₁₁ eq-H₁₃ eq-H₃₁ eq-H₃₃)
   == span^2=-raw eq-A₀₀ eq-A₂₀ eq-A₄₀ eq-A₀₂ eq-A₂₂ eq-A₄₂ eq-A₀₄ eq-A₂₄ eq-A₄₄ eq-f₁₀ eq-f₃₀ eq-f₁₂ eq-f₃₂ eq-f₁₄ eq-f₃₄ eq-f₀₁ eq-f₀₃ eq-f₂₁ eq-f₂₃ eq-f₄₁ eq-f₄₃ (square-thing _ _ _ _ _ _ _ _ (ap↓ (λ u → ! ∘ u) eq-H₁₁)) eq-H₃₁ eq-H₁₃ (square-thing _ _ _ _ _ _ _ _ (ap↓ (λ u → ! ∘ u) eq-H₃₃))
ap-span^2=-priv2 idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp = idp

module _ {i} (d : Span^2 {i}) where

  open Span^2 d

  transpose-transpose : transpose (transpose d) == d
  transpose-transpose = span^2=-raw idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp
                        (λ= (!-! ∘ Span^2.H₁₁ d)) idp idp (λ= (!-! ∘ Span^2.H₃₃ d))

module _ {i} (d : Span^2 {i}) where

  transpose-equiv : Span^2 {i} ≃ Span^2
  transpose-equiv = equiv transpose transpose transpose-transpose transpose-transpose

module _ {i} (d : Span^2 {i}) where

  open Span^2 d

  d' : (H₁₁' : type-of H₁₁) (H₃₃' : type-of H₃₃) → Span^2
  d' H₁₁' H₃₃' = record d {H₁₁ = H₁₁'; H₃₃ = H₃₃'}

  e : {H₁₁' : type-of H₁₁} (eq₁ : H₁₁ == H₁₁') {H₃₃' : type-of H₃₃} (eq₃ : H₃₃ == H₃₃') (c : M.A₂∙ (d' H₁₁' H₃₃'))
      → left (M.f₁∙ (d' H₁₁' H₃₃') c) == right (M.f₃∙ (d' H₁₁' H₃₃') c)
  e {H₁₁'} eq₁ {H₃₃'} eq₃ = E.f  module _ where

    e-glue : {H₁₁' : type-of H₁₁} (eq₁ : H₁₁ == H₁₁') {H₃₃' : type-of H₃₃} (eq₃ : H₃₃ == H₃₃') (c : Span^2.A₂₂ (d' H₁₁' H₃₃'))
      → glue (left (f₂₁ c)) == glue (right (f₂₃ c)) [ (λ z → left (M.f₁∙ (d' H₁₁' H₃₃') z) == right (M.f₃∙ (d' H₁₁' H₃₃') z)) ↓ glue c ]
    e-glue idp idp c = apd glue (glue c)

    module E = PushoutElim {P = λ c → left (M.f₁∙ (d' H₁₁' H₃₃') c) == right (M.f₃∙ (d' H₁₁' H₃₃') c) :> Pushout^2 d} (glue ∘ left) (glue ∘ right) (e-glue eq₁ eq₃)

  module F {H₁₁' : type-of H₁₁} (eq₁ : H₁₁ == H₁₁') {H₃₃' : type-of H₃₃} (eq₃ : H₃₃ == H₃₃')
    = PushoutRec {d = M.v-h-span (d' H₁₁' H₃₃')} {D = Pushout^2 d}
                 left right (e eq₁ eq₃)

  tr-tr-fun : Pushout^2 (transpose (transpose d)) → Pushout^2 d
  tr-tr-fun = F.f (! (λ= (!-! ∘ H₁₁))) (! (λ= (!-! ∘ H₃₃)))

  lemma12 : (c : M.A₂∙ d) → e idp idp c == glue c
  lemma12 = Pushout-elim (λ a → idp) (λ b → idp) (λ c → ↓-=-in (! (E.glue-β idp idp c)))

  result' : {H₁₁' : type-of H₁₁} (eq₁ : H₁₁ == H₁₁') {H₃₃' : type-of H₃₃} (eq₃ : H₃₃ == H₃₃') (x : Pushout^2 (d' H₁₁' H₃₃'))
    → transport Pushout^2 (span^2=-raw idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp (! eq₁) idp idp (! eq₃) :> (d' H₁₁' H₃₃' == d)) x == F.f eq₁ eq₃ x
  result' idp idp = Pushout-elim (λ a → idp) (λ b → idp) (λ c → ↓-='-in (F.glue-β idp idp c ∙ lemma12 c ∙ ! (ap-idf (glue c))))

  result : {H₁₁' : type-of H₁₁} (eq₁ : H₁₁' == H₁₁) {H₃₃' : type-of H₃₃} (eq₃ : H₃₃' == H₃₃) (x : Pushout^2 (d' H₁₁' H₃₃'))
    → transport Pushout^2 (span^2=-raw idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp eq₁ idp idp eq₃ :> (d' H₁₁' H₃₃' == d)) x == F.f (! eq₁) (! eq₃) x
  result eq₁ eq₃ x = ap (λ u → transport Pushout^2 (span^2=-raw idp idp idp idp idp idp idp idp idp idp idp idp idp
                                                                idp idp idp idp idp idp idp idp (fst u) idp idp (snd u) :> (_ == d)) x)
                        (pair×= (! (!-! eq₁)) (! (!-! eq₃)))
                     ∙ result' (! eq₁) (! eq₃) x

  result2 : (x : Pushout^2 (transpose (transpose d))) → transport Pushout^2 (transpose-transpose d) x == tr-tr-fun x
  result2 = result (λ= (!-! ∘ Span^2.H₁₁ d)) (λ= (!-! ∘ Span^2.H₃₃ d))

-- module _ {i} where

--   postulate
--     to : (d : Span^2 {i}) → Pushout^2 d → Pushout^2 (transpose d)

--   from : (d : Span^2 {i}) → Pushout^2 (transpose d) → Pushout^2 d
--   from d = tr-tr-fun d ∘ to (transpose d)

--   postulate
--     from-to : (d : Span^2 {i}) (x : Pushout^2 d) → from d (to d x) == x

--   lemma3 : {d d' : Span^2 {i}} (p : d == d') (x : Pushout^2 d) → transport (Pushout^2 ∘ transpose) p (to d x) == to d' (transport Pushout^2 p x)
--   lemma3 {d} {.d} idp x = idp

--   lemma34 : (d : Span^2 {i}) (x : Pushout^2 (transpose (transpose d))) → transport (Pushout^2 ∘ transpose) (transpose-transpose d) (to (transpose (transpose d)) x) == to d (tr-tr-fun d x)
--   lemma34 d x = lemma3 (transpose-transpose d) x ∙ ap (to d) (result2 d x)

--   lm2 : (d : Span^2 {i}) → ap transpose (transpose-transpose d) == transpose-transpose (transpose d)
--   lm2 d = ap-span^2=-priv2 idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp
--                         (! (! (λ= (!-! ∘ Span^2.H₁₁ d)))) idp idp (! (! (λ= (!-! ∘ Span^2.H₃₃ d)))) ∙ ap (λ u → span^2=-raw idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp (fst u) idp idp (snd u)) (pair×= (lm3 (Span^2.H₁₁ d)) (lm3 (Span^2.H₃₃ d))) where

--     lm3 : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B} (p : (a : A) → f a == g a)
--       → ap (λ f → ! ∘ f) (! (! (λ= (!-! ∘ p)))) == ! (! (λ= (!-! ∘ ! ∘ p)))
--     lm3 p = transport (λ u → ap (λ f → ! ∘ f) (! (! (λ= (!-! ∘ u)))) == ! (! (λ= (!-! ∘ ! ∘ u)))) (λ= (app=-β p)) (lm3' (λ= p))  where

--       lm3' : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B} (p : f == g)
--         → ap (λ f → ! ∘ f) (! (! (λ= (!-! ∘ app= p)))) == ! (! (λ= (!-! ∘ ! ∘ app= p)))
--       lm3' idp = ap (λ u → ap (λ u → ! ∘ u) (! (! u))) (! (λ=-η idp)) ∙ ap (! ∘ !) (λ=-η idp)

--   lemma345 : (d : Span^2 {i}) (x : Pushout^2 (transpose (transpose (transpose d))))
--     → transport (Pushout^2 ∘ transpose) (transpose-transpose d) x == tr-tr-fun (transpose d) x
--   lemma345 d x =
--     transport (Pushout^2 ∘ transpose) (transpose-transpose d) x
--       =⟨ ap (λ u → coe u x) (ap-∘ Pushout^2 transpose (transpose-transpose d)) ⟩
--     transport Pushout^2 (ap transpose (transpose-transpose d)) x
--       =⟨ ap (λ u → transport Pushout^2 u x) (lm2 d) ⟩
--     transport Pushout^2 (transpose-transpose (transpose d)) x
--       =⟨ result2 (transpose d) x ⟩
--     tr-tr-fun (transpose d) x ∎

--   to-from : (d : Span^2 {i}) (x : Pushout^2 (transpose d)) → to d (from d x) == x
--   to-from d x =
--     to d (tr-tr-fun d (to (transpose d) x))
--       =⟨ ! (lemma34 d (to (transpose d) x)) ⟩
--     transport (Pushout^2 ∘ transpose) (transpose-transpose d) (to (transpose (transpose d)) (to (transpose d) x))
--       =⟨ lemma345 d (to (transpose (transpose d)) (to (transpose d) x)) ⟩
--     tr-tr-fun (transpose d) (to (transpose (transpose d)) (to (transpose d) x))
--       =⟨ from-to (transpose d) x ⟩
--     x ∎

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Issue443 where

module M (A : Set) where
  record R : Set where
    field
      a : A

postulate
  A : Set
  I : A → Set
  i : (x : A) → I x
  r : M.R A

a = M.R.a A r

Foo : Set₁
Foo with i (M.R.a A r)
Foo | _ = Set

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.RingSolver.CommRingHornerForms where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.FinData
open import Cubical.Data.Vec
open import Cubical.Data.Bool using (Bool; true; false; if_then_else_; _and_)

open import Cubical.Algebra.RingSolver.RawRing
open import Cubical.Algebra.RingSolver.RawAlgebra renaming (⟨_⟩ to ⟨_⟩ₐ)
open import Cubical.Algebra.RingSolver.AlmostRing renaming (⟨_⟩ to ⟨_⟩ᵣ)

private
  variable
    ℓ ℓ′ : Level

{-
  This defines the type of multivariate Polynomials over the RawRing R.
  The construction is based on the algebraic fact

    R[X₀][X₁]⋯[Xₙ] ≅ R[X₀,⋯,Xₙ]

  BUT: Contrary to algebraic convetions, we will give 'Xₙ' the lowest index
  in the definition of 'Variable' below. So if 'Variable n R k' is identified
  with 'Xₖ', then the RawRing we construct should rather be denoted with

    R[Xₙ][Xₙ₋₁]⋯[X₀]

  or, to be precise about the evaluation order:

    (⋯((R[Xₙ])[Xₙ₋₁])⋯)[X₀]

-}

data IteratedHornerForms (A : RawAlgebra ℤAsRawRing ℓ) : ℕ → Type ℓ where
  const : ℤ → IteratedHornerForms A ℕ.zero
  0H : {n : ℕ} → IteratedHornerForms A (ℕ.suc n)
  _·X+_ : {n : ℕ} → IteratedHornerForms A (ℕ.suc n) → IteratedHornerForms A n
                  → IteratedHornerForms A (ℕ.suc n)

module _ (A : RawAlgebra ℤAsRawRing ℓ′) where
  open RawRing ℤAsRawRing
  isZero : {n : ℕ} → IteratedHornerForms A n
                   → Bool
  isZero (const (pos ℕ.zero)) = true
  isZero (const (pos (ℕ.suc _))) = false
  isZero (const (negsuc _)) = false
  isZero 0H = true
  isZero (P ·X+ P₁) = false

eval : {A : RawAlgebra ℤAsRawRing ℓ′}
       (n : ℕ) (P : IteratedHornerForms A n)
       → Vec ⟨ A ⟩ₐ n → ⟨ A ⟩ₐ
eval {A = A} ℕ.zero (const r) [] = RawAlgebra.scalar A r
eval {A = A} .(ℕ.suc _) 0H (_ ∷ _) = RawAlgebra.0r A
eval {A = A} (ℕ.suc n) (P ·X+ Q) (x ∷ xs) =
     let open RawAlgebra A
         P' = (eval (ℕ.suc n) P (x ∷ xs))
         Q' = eval n Q xs
     in if (isZero A P)
        then Q'
        else P' · x + Q'

module IteratedHornerOperations (A : RawAlgebra ℤAsRawRing ℓ) where
  open RawRing ℤAsRawRing

  private
    1H' : (n : ℕ) → IteratedHornerForms A n
    1H' ℕ.zero = const 1r
    1H' (ℕ.suc n) = 0H ·X+ 1H' n

    0H' : (n : ℕ) → IteratedHornerForms A n
    0H' ℕ.zero = const 0r
    0H' (ℕ.suc n) = 0H

  1ₕ : {n : ℕ} → IteratedHornerForms A n
  1ₕ {n = n} = 1H' n

  0ₕ : {n : ℕ} → IteratedHornerForms A n
  0ₕ {n = n} = 0H' n

  X : (n : ℕ) (k : Fin n) → IteratedHornerForms A n
  X (ℕ.suc m) zero = 1ₕ ·X+ 0ₕ
  X (ℕ.suc m) (suc k) = 0ₕ ·X+ X m k

  _+ₕ_ : {n : ℕ} → IteratedHornerForms A n → IteratedHornerForms A n
               → IteratedHornerForms A n
  (const r) +ₕ (const s) = const (r + s)
  0H +ₕ Q = Q
  (P ·X+ r) +ₕ 0H = P ·X+ r
  (P ·X+ r) +ₕ (Q ·X+ s) =
    let left = (P +ₕ Q)
        right = (r +ₕ s)
    in if ((isZero A left) and (isZero A right))
       then 0ₕ
       else left ·X+ right

  -ₕ : {n : ℕ} → IteratedHornerForms A n → IteratedHornerForms A n
  -ₕ (const x) = const (- x)
  -ₕ 0H = 0H
  -ₕ (P ·X+ Q) = (-ₕ P) ·X+ (-ₕ Q)

  _⋆_ : {n : ℕ} → IteratedHornerForms A n → IteratedHornerForms A (ℕ.suc n)
                → IteratedHornerForms A (ℕ.suc n)
  _·ₕ_ : {n : ℕ} → IteratedHornerForms A n → IteratedHornerForms A n
                → IteratedHornerForms A n
  r ⋆ 0H = 0H
  r ⋆ (P ·X+ Q) =
    if (isZero A r)
    then 0ₕ
    else (r ⋆ P) ·X+ (r ·ₕ Q)

  const x ·ₕ const y = const (x · y)
  0H ·ₕ Q = 0H
  (P ·X+ Q) ·ₕ S =
     let
        z = (P ·ₕ S)
     in if (isZero A z)
        then (Q ⋆ S)
        else (z ·X+ 0ₕ) +ₕ (Q ⋆ S)

  asRawRing : (n : ℕ) → RawRing {ℓ}
  RawRing.Carrier (asRawRing n) = IteratedHornerForms A n
  RawRing.0r (asRawRing n) = 0ₕ
  RawRing.1r (asRawRing n) = 1ₕ
  RawRing._+_ (asRawRing n) = _+ₕ_
  RawRing._·_ (asRawRing n) = _·ₕ_
  RawRing.- (asRawRing n) =  -ₕ

Variable : (n : ℕ) (R : RawAlgebra ℤAsRawRing ℓ′) (k : Fin n) → IteratedHornerForms R n
Variable n R k = IteratedHornerOperations.X R n k

Constant : (n : ℕ) (R : RawAlgebra ℤAsRawRing ℓ′) (r : ℤ) → IteratedHornerForms R n
Constant ℕ.zero R r = const r
Constant (ℕ.suc n) R r = IteratedHornerOperations.0ₕ R ·X+ Constant n R r

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import HoTT

module cw.cohomology.GridPtdMap {i j k}
  {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (f : X ⊙→ Y) (g : Y ⊙→ Z) where

  open import cw.cohomology.GridMap (fst f) (fst g) public

  Y/X = ⊙Cofiber f
  Z/X = ⊙Cofiber (g ⊙∘ f)
  Z/Y = ⊙Cofiber g

  Y/X-to-Z/X : Y/X ⊙→ Z/X
  Y/X-to-Z/X = B/A-to-C/A , idp

  Z/X-to-Z/Y : Z/X ⊙→ Z/Y
  Z/X-to-Z/Y = C/A-to-C/B , idp

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels

module Cubical.Algebra.Semigroup.Construct.Left {ℓ} (Aˢ : hSet ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Semigroup

import Cubical.Algebra.Magma.Construct.Left Aˢ as LMagma
open LMagma public hiding (Left-isMagma; LeftMagma)

private
  A = ⟨ Aˢ ⟩
  isSetA = Aˢ .snd

◂-assoc : Associative _◂_
◂-assoc _ _ _ = refl

Left-isSemigroup : IsSemigroup A _◂_
Left-isSemigroup = record
  { isMagma = LMagma.Left-isMagma
  ; assoc   = ◂-assoc
  }

LeftSemigroup : Semigroup ℓ
LeftSemigroup = record { isSemigroup = Left-isSemigroup }


text:
{-

Base facts about that the ring ℤ is Bézout domain

-}
{-# OPTIONS --safe #-}
module Cubical.Data.Int.Divisibility where

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

open import Cubical.Data.Nat
  hiding   (+-assoc ; +-comm ; ·-comm)
  renaming (_·_ to _·ℕ_; _+_ to _+ℕ_ ; ·-assoc to ·ℕ-assoc)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Nat.Divisibility
  using    (m∣n→m≤n)
  renaming (_∣_ to _∣ℕ_ ; isProp∣ to isProp∣ℕ ; stDivIneq to stDivIneqℕ)
open import Cubical.Data.Nat.Mod
open import Cubical.Data.Int
  hiding   (_+_ ; _·_ ; _-_ ; -_ ; addEq ; ·Comm ; ·Assoc ; +Comm ; +Assoc)

open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation as Prop
open import Cubical.Relation.Nullary

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int
  renaming (ℤ to Ringℤ)
open import Cubical.Algebra.RingSolver.Reflection

private
  variable
    m n k : ℤ

-- It seems there are bugs when applying ring solver to integers.
-- The following is a work-around.
private
  module Helper {ℓ : Level}(𝓡 : CommRing ℓ) where
    open CommRingStr (𝓡 .snd)

    helper1 : (a b m d r : 𝓡 .fst) → (- a · d + b) · m + a · (d · m + r) ≡ a · r + b · m
    helper1 = solve 𝓡

    helper2 : (d m r : 𝓡 .fst) → (d · m + r) + (- d) · m ≡ r
    helper2 = solve 𝓡

    helper3 : (n m d r : 𝓡 .fst) → n ≡ d · m + r → n + (- d) · m ≡ r
    helper3 n m d r p = (λ t → p t + (- d) · m) ∙ helper2 d m r

open Helper Ringℤ

open CommRingStr      (Ringℤ .snd)

-- The Divisibility Relation
-- Most definitions are the same as in Cubical.Data.Nat.Divisibility

_∣_ : ℤ → ℤ → Type
m ∣ n = ∃[ c ∈ ℤ ] c · m ≡ n

isProp∣ : isProp (m ∣ n)
isProp∣ = squash

-- Untruncated divisiblility relation

_∣'_ : ℤ → ℤ → Type
pos 0  ∣' n = 0 ≡ n
pos (suc m) ∣' n = Σ[ c ∈ ℤ ] c · (pos (suc m)) ≡ n
(negsuc m)  ∣' n = Σ[ c ∈ ℤ ] c · (negsuc m)    ≡ n

isProp∣' : isProp (m ∣' n)
isProp∣' {m = pos 0} {n = n} = isSetℤ 0 n
isProp∣' {m = pos (suc m)} {n = n} p q =
  Σ≡Prop (λ _ → isSetℤ _ _) (·rCancel (pos (suc m)) _ _ (p .snd ∙ sym (q .snd)) (λ r → snotz (injPos r)))
isProp∣' {m = negsuc m} {n = n} p q =
  Σ≡Prop (λ _ → isSetℤ _ _) (·rCancel (negsuc m) _ _ (p .snd ∙ sym (q .snd)) (negsucNotpos _ 0))

∣→∣' : (m n : ℤ) → m ∣ n → m ∣' n
∣→∣' (pos 0) n ∣ c , p ∣ = ·Comm 0 c ∙ p
∣→∣' (pos (suc m)) n ∣ p ∣ = p
∣→∣' (negsuc m) n ∣ p ∣ = p
∣→∣' m n (squash p q i) = isProp∣' (∣→∣' _ _ p) (∣→∣' _ _ q) i

∣'→∣ : (m n : ℤ) → m ∣' n → m ∣ n
∣'→∣ (pos 0) n p = ∣ 0 , p ∣
∣'→∣ (pos (suc m)) n p = ∣ p ∣
∣'→∣ (negsuc m) n p = ∣ p ∣

∣≃∣' : (m n : ℤ) → (m ∣ n) ≃ (m ∣' n)
∣≃∣' m n = propBiimpl→Equiv isProp∣ isProp∣' (∣→∣' _ _) (∣'→∣ _ _)

-- Properties of divisibility

∣-left : m ∣ (m · k)
∣-left {k = k} = ∣ k , ·Comm k _ ∣

∣-right : m ∣ (k · m)
∣-right {k = k} =  ∣ k , refl ∣

∣-refl : m ≡ n → m ∣ n
∣-refl p = ∣ 1 , p ∣

∣-zeroˡ : 0 ∣ m → 0 ≡ m
∣-zeroˡ = ∣→∣' _ _

∣-zeroʳ : m ∣ 0
∣-zeroʳ = ∣ 0 , refl ∣

∣-+ : k ∣ m → k ∣ n → k ∣ (m + n)
∣-+ =
  Prop.map2
    λ {(c₁ , p) (c₂ , q) → (c₁ + c₂ , ·DistL+ c₁ c₂ _ ∙ (λ t → p t + q t))}

∣-trans : k ∣ m → m ∣ n → k ∣ n
∣-trans =
  Prop.map2
    λ {(c₁ , p) (c₂ , q) → (c₂ · c₁ , sym (·Assoc c₂ c₁ _) ∙ cong (c₂ ·_) p ∙ q)}

∣-left· : k ∣ n → k ∣ (n · m)
∣-left· {k = k} {m = m} p = ∣-trans p (∣-left {k = m})

∣-right· : k ∣ m → k ∣ (n · m)
∣-right· {k = k} {n = n} p = ∣-trans p (∣-right {k = n})

-- Natural numbers back and forth (using abs)

∣→∣ℕ : m ∣ n → abs m ∣ℕ abs n
∣→∣ℕ {m = m} = Prop.rec isProp∣ℕ (λ (c , h) → ∣ abs c , sym (abs· c m) ∙ cong abs h ∣)

private
  ∣ℕ→∣-helper : (m n : ℤ)
    → (c : ℕ)(h : c ·ℕ abs m ≡ abs n)
    → (m ≡ pos (abs m)) ⊎ (m ≡ - pos (abs m))
    → (n ≡ pos (abs n)) ⊎ (n ≡ - pos (abs n))
    → Σ[ d ∈ ℤ ] d · m ≡ n
  ∣ℕ→∣-helper _ _ c _ (inl _) (inl _) .fst = pos c
  ∣ℕ→∣-helper m n c h (inl p) (inl q) .snd =
      (λ t → pos c · p t)
    ∙ sym (pos·pos c (abs m))
    ∙ cong pos h
    ∙ sym q
  ∣ℕ→∣-helper _ _ c _ (inl _) (inr _) .fst = - pos c
  ∣ℕ→∣-helper m n c h (inl p) (inr q) .snd =
      (λ t → - pos c · p t)
    ∙ sym (-DistL· (pos c) (pos (abs m)))
    ∙ (λ t → - pos·pos c (abs m) (~ t))
    ∙ cong (-_) (cong pos h)
    ∙ sym q
  ∣ℕ→∣-helper _ _ c _ (inr _) (inl _) .fst = - pos c
  ∣ℕ→∣-helper m n c h (inr p) (inl q) .snd =
      (λ t → - pos c · p t)
    ∙ sym (-DistLR· (pos c) (pos (abs m)))
    ∙ sym (pos·pos c (abs m))
    ∙ cong pos h
    ∙ sym q
  ∣ℕ→∣-helper _ _ c _ (inr _) (inr _) .fst = pos c
  ∣ℕ→∣-helper m n c h (inr p) (inr q) .snd =
      (λ t → pos c · p t)
    ∙ sym (-DistR· (pos c) (pos (abs m)))
    ∙ (λ t → - pos·pos c (abs m) (~ t))
    ∙ cong (-_) (cong pos h)
    ∙ sym q

∣ℕ→∣ : abs m ∣ℕ abs n → m ∣ n
∣ℕ→∣ = Prop.rec isProp∣ (λ (c , h) → ∣ ∣ℕ→∣-helper _ _ c h (abs→⊎ _ _ refl) (abs→⊎ _ _ refl) ∣)

¬∣→¬∣ℕ : ¬ m ∣ n → ¬ abs m ∣ℕ abs n
¬∣→¬∣ℕ p q = p (∣ℕ→∣ q)

-- Inequality for strict divisibility

stDivIneq : ¬ m ≡ 0 → ¬ m ∣ n → k ∣ m → k ∣ n → abs k < abs m
stDivIneq p q h h' = stDivIneqℕ (¬x≡0→¬abs≡0 p) (¬∣→¬∣ℕ q) (∣→∣ℕ h) (∣→∣ℕ h')

-- Exact division

divide : m ∣ n → ℤ
divide {m = pos 0} _ = 0
divide {m = pos (suc m)} p = ∣→∣' _ _ p .fst
divide {m = negsuc m} p = ∣→∣' _ _ p .fst

divideEq : (p : m ∣ n) → divide p · m ≡ n
divideEq {m = pos 0} = ∣→∣' _ _
divideEq {m = pos (suc m)} p = ∣→∣' _ _ p .snd
divideEq {m = negsuc m} p = ∣→∣' _ _ p .snd

-- Bézout and Euclidean Domain

record Bézout (m n : ℤ) : Type where
  constructor bezout
  field
    coef₁ : ℤ
    coef₂ : ℤ
    gcd   : ℤ
    identity : coef₁ · m + coef₂ · n ≡ gcd
    isCD  : (gcd ∣ m) × (gcd ∣ n)

open Bézout

Bézout0 : (n : ℤ) → Bézout 0 n
Bézout0 n .coef₁ = 0
Bézout0 n .coef₂ = 1
Bézout0 n .gcd   = n
Bézout0 n .identity = +Comm 0 n
Bézout0 n .isCD  = ∣-zeroʳ , ∣-refl refl

bézoutReduction : (m d r : ℤ) → Bézout r m → Bézout m (d · m + r)
bézoutReduction m d r b .coef₁ = - b .coef₁ · d + b .coef₂
bézoutReduction m d r b .coef₂ = b .coef₁
bézoutReduction m d r b .gcd   = b .gcd
bézoutReduction m d r b .identity = helper1 (b .coef₁) (b .coef₂) m d r ∙ b .identity
bézoutReduction m d r b .isCD .fst = b .isCD .snd
bézoutReduction m d r b .isCD .snd = ∣-+ (∣-right· {n = d} (b .isCD .snd)) (b .isCD .fst)

-- Properties of Bézout identity

module _
  (b : Bézout m n) where

  private
    g = b .gcd

  gcdIsGCD : k ∣ m → k ∣ n → k ∣ g
  gcdIsGCD {k = k} p q =
    subst (k ∣_) (b .identity) (∣-+ (∣-right· {n = b .coef₁} p) (∣-right· {n = b .coef₂} q))

  gcd≡0 : g ≡ 0 → (m ≡ 0) × (n ≡ 0)
  gcd≡0 p .fst = sym (∣-zeroˡ (subst (λ a → a ∣ _) p (b .isCD .fst)))
  gcd≡0 p .snd = sym (∣-zeroˡ (subst (λ a → a ∣ _) p (b .isCD .snd)))

  ¬m≡0→¬gcd≡0 : ¬ m ≡ 0 → ¬ g ≡ 0
  ¬m≡0→¬gcd≡0 p q = p (gcd≡0 q .fst)

  div₁ div₂ : ℤ
  div₁ = divide (b .isCD .fst)
  div₂ = divide (b .isCD .snd)

  div·-helper : g · (div₁ · n) ≡ g · (div₂ · m)
  div·-helper =
      ·Assoc g div₁ n
    ∙ (λ i → ·Comm g div₁ i · n)
    ∙ (λ i → divideEq (b .isCD .fst) i · n)
    ∙ ·Comm m n
    ∙ (λ i → divideEq (b .isCD .snd) (~ i) · m)
    ∙ (λ i → ·Comm div₂ g i · m)
    ∙ sym (·Assoc g div₂ m)

  div·-g≠0 : ¬ g ≡ 0 → div₁ · n ≡ div₂ · m
  div·-g≠0 p = ·lCancel _ _ _ div·-helper p

  div·-g≡0 : g ≡ 0 → div₁ · n ≡ div₂ · m
  div·-g≡0 p =
      (λ i → div₁ · gcd≡0 p .snd i)
    ∙ ·Comm div₁ 0
    ∙ ·Comm 0 div₂
    ∙ (λ i → div₂ · gcd≡0 p .fst (~ i))

  div·-case : Dec (g ≡ 0) → div₁ · n ≡ div₂ · m
  div·-case (yes p) = div·-g≡0  p
  div·-case (no ¬p) = div·-g≠0 ¬p

  div· : div₁ · n ≡ div₂ · m
  div· = div·-case (discreteℤ g 0)

  div·- : - div₂ · m + div₁ · n ≡ 0
  div·- =   (λ i → -DistL· div₂ m (~ i) + div₁ · n)
          ∙ subst (λ a → - a + div₁ · n ≡ 0) div· (-Cancel' (div₁ · n))

-- Quotient and Remainder

record QuotRem (m n : ℤ) : Type where
  constructor quotrem
  field
    div : ℤ
    rem : ℤ
    quotEq : n ≡ div · m + rem
    normIneq : (rem ≡ 0) ⊎ ((¬ rem ≡ 0) × (abs rem < abs m))

open QuotRem

-- Using remainder to decide divisibility

module _
  (m n : ℤ)(qr : QuotRem m n) where

  rem≡0→m∣n : qr .rem ≡ 0 → m ∣ n
  rem≡0→m∣n p = ∣ qr .div , (λ i → qr .div · m + p (~ i)) ∙ sym (qr .quotEq) ∣

  m∣n→rem≡0 : m ∣ n → qr .rem ≡ 0
  m∣n→rem≡0 p =
    case qr .normIneq
    return _ of λ
    { (inl q) → q
    ; (inr q) →
        let ∣+  = ∣-+ p (∣-right {m = m} {k = - qr .div})
            m∣r = subst (m ∣_) (helper3 _ _ (qr .div) (qr .rem) (qr .quotEq)) ∣+
            m≤r = m∣n→m≤n (¬x≡0→¬abs≡0 (q .fst)) (∣→∣ℕ m∣r)
        in  Empty.rec (<-asym (q .snd) m≤r) }

  m∣n→rem≡0' : (p : m ∣ n) → qr .normIneq ≡ inl (m∣n→rem≡0 p)
  m∣n→rem≡0' p =
    case (qr .normIneq)
    return (λ x → x ≡ inl (m∣n→rem≡0 p)) of λ
    { (inl q) → cong inl (isSet→SquareP (λ i j → isSetℤ) q (m∣n→rem≡0 p) refl refl)
    ; (inr q) → Empty.rec (q .fst (m∣n→rem≡0 p)) }

  rem≢0→m∤n : ¬ qr .rem ≡ 0 → ¬ m ∣ n
  rem≢0→m∤n p q = p (m∣n→rem≡0 q)

-- The Euclidean Algorithm
module _
  (decEq0  : (n : ℤ) → Dec (n ≡ 0))
  (quotRem : (m n : ℤ)(¬z : ¬ m ≡ 0) → QuotRem m n) where

  euclidStep : (norm : ℕ)
    → (m n : ℤ)(h : abs m < norm)
    → (b : QuotRem m n)
    → Bézout m n
  euclidStep 0 _ _ h _ = Empty.rec (¬-<-zero h)
  euclidStep (suc N) m n h (quotrem div rem quotEq (inl p)) =
    let q = subst (λ r → n ≡ div · m + r) p quotEq
    in  bezout 1 0 m refl (∣-refl refl , subst (λ k → m ∣ k) (sym q) (∣-right {k = div}))
  euclidStep (suc N) m n h (quotrem div rem quotEq (inr p)) =
    let b = euclidStep N rem m (<≤-trans (p .snd) (pred-≤-pred h)) (quotRem _ _ (p .fst))
    in  subst (λ x → Bézout m x) (sym quotEq) (bézoutReduction _ div _ b)

  private
    euclid-helper : (m n : ℤ)(dec : Dec (m ≡ 0)) → Bézout m n
    euclid-helper m n (yes z) = subst (λ x → Bézout x n) (sym z) (Bézout0 n)
    euclid-helper m n (no ¬z) = euclidStep (suc (abs m)) m n ≤-refl (quotRem m n ¬z)

  euclid : (m n : ℤ) → Bézout m n
  euclid m n = euclid-helper m n (decEq0 _)

  -- Euclid algorithm when divisibility holds
  euclid∣ : (m n : ℤ) → ¬ m ≡ 0 → m ∣ n → (euclid m n .coef₁ ≡ 1) × (euclid m n .coef₂ ≡ 0)
  euclid∣ _ _ = euclid∣-helper _ _ (decEq0 _)
    where
    euclid∣-helper : (m n : ℤ)(dec : Dec (m ≡ 0)) → ¬ m ≡ 0 → m ∣ n
      → (euclid-helper m n dec .coef₁ ≡ 1) × (euclid-helper m n dec .coef₂ ≡ 0)
    euclid∣-helper _ _ (yes z) q = Empty.rec (q z)
    euclid∣-helper m n (no ¬z) _ q =
      let qr = quotRem m n ¬z
          path : qr ≡ quotrem _ _ _ _
          path t = record qr { normIneq = m∣n→rem≡0' _ _ qr q t }
      in  (λ t → euclidStep (suc (abs m)) m n ≤-refl (path t) .coef₁) ,
          (λ t → euclidStep (suc (abs m)) m n ≤-refl (path t) .coef₂)

-- The ring ℤ is an Euclidean domain

private
  dec-helper : {ℓ ℓ' : Level}{A : Type ℓ}{B : Type ℓ'} → Dec A → B → A ⊎ ((¬ A) × B)
  dec-helper (yes p) _ = inl p
  dec-helper (no ¬p) b = inr (¬p , b)

quotRemPosPos : (m n : ℕ)(¬z : ¬ pos m ≡ 0) → QuotRem (pos m) (pos n)
quotRemPosPos m n _ .div = pos (quotient  n / m)
quotRemPosPos m n _ .rem = pos (remainder n / m)
quotRemPosPos m n _ .quotEq =
    (λ t → pos (≡remainder+quotient m n (~ t)))
  ∙ pos+ (remainder n / m) (m ·ℕ (quotient n / m))
  ∙ +Comm (pos (remainder n / m)) (pos (m ·ℕ (quotient n / m)))
  ∙ (λ t → pos·pos m (quotient n / m) t + pos (remainder n / m))
  ∙ (λ t → ·Comm (pos m) (pos (quotient n / m)) t + pos (remainder n / m))
quotRemPosPos 0       n ¬z .normIneq = Empty.rec (¬z refl)
quotRemPosPos (suc m) n ¬z .normIneq = dec-helper (discreteℤ _ 0) (mod< m n)

quotRemNegPos : (m n : ℕ)(¬z : ¬ - pos m ≡ 0) → QuotRem (- pos m) (pos n)
quotRemNegPos m n ¬z .div = - (quotRemPosPos m n (λ p → ¬z (λ t → - p t)) .div)
quotRemNegPos m n ¬z .rem = quotRemPosPos m n (λ p → ¬z (λ t → - p t)) .rem
quotRemNegPos m n ¬z .quotEq =
    quotRemPosPos m n (λ p → ¬z (λ t → - p t)) .quotEq
  ∙ (λ t → -DistLR· (pos (quotient n / m)) (pos m) t + (pos (remainder n / m)))
quotRemNegPos 0       n ¬z .normIneq = Empty.rec (¬z refl)
quotRemNegPos (suc m) n ¬z .normIneq = quotRemPosPos (suc m) n (λ p → ¬z (λ t → - p t)) .normIneq

private
  quotRemPos-helper : (m : ℤ)(k n : ℕ)(¬z : ¬ m ≡ 0) → (m ≡ pos k) ⊎ (m ≡ - pos k) → QuotRem m (pos n)
  quotRemPos-helper m k n ¬z (inl p) =
    subst (λ l → QuotRem l (pos n)) (sym p) (quotRemPosPos k n (λ r → ¬z (p ∙ r)))
  quotRemPos-helper m k n ¬z (inr p) =
    subst (λ l → QuotRem l (pos n)) (sym p) (quotRemNegPos k n (λ r → ¬z (p ∙ r)))

quotRemPos : (m : ℤ)(n : ℕ)(¬z : ¬ m ≡ 0) → QuotRem m (pos n)
quotRemPos m n ¬z = quotRemPos-helper m (abs m) n ¬z (abs→⊎ _ _ refl)

private
  sum-helper : (m r : ℤ)
    → (r ≡ 0)   ⊎ ((¬ r ≡ 0)   × (abs r < abs m))
    → (- r ≡ 0) ⊎ ((¬ - r ≡ 0) × (abs (- r) < abs m))
  sum-helper m r (inl p) = inl (λ t → - p t)
  sum-helper m r (inr p) =
    inr ((λ q → p .fst (sym (-Involutive r) ∙ (λ t → - q t)))
      , subst (λ k → k < abs m) (sym (abs- r)) (p .snd))

quotRemNeg : (m : ℤ)(n : ℕ)(¬z : ¬ m ≡ 0) → QuotRem m (- pos n)
quotRemNeg m n ¬z .div = - (quotRemPos m n ¬z .div)
quotRemNeg m n ¬z .rem = - (quotRemPos m n ¬z .rem)
quotRemNeg m n ¬z .quotEq =
    (λ t → - quotRemPos m n ¬z .quotEq t)
  ∙ -Dist+ (quotRemPos m n ¬z .div · m) (quotRemPos m n ¬z .rem)
  ∙ (λ t → -DistL· (quotRemPos m n ¬z .div) m t + - quotRemPos m n ¬z .rem)
quotRemNeg m n ¬z .normIneq = sum-helper m _ (quotRemPos m n ¬z .normIneq)

private
  quotRem-helper : (m n : ℤ)(k : ℕ)(¬z : ¬ m ≡ 0) → (n ≡ pos k) ⊎ (n ≡ - pos k) → QuotRem m n
  quotRem-helper m n k ¬z (inl p) = subst (λ l → QuotRem m l) (sym p) (quotRemPos m k ¬z)
  quotRem-helper m n k ¬z (inr p) = subst (λ l → QuotRem m l) (sym p) (quotRemNeg m k ¬z)

-- The quotient-remainder Theorem and the Bézout identity

quotRem : (m n : ℤ)(¬z : ¬ m ≡ 0) → QuotRem m n
quotRem m n ¬z = quotRem-helper m n (abs n) ¬z (abs→⊎ _ _ refl)

bézout : (m n : ℤ) → Bézout m n
bézout = euclid (λ m → discreteℤ m 0) quotRem

bézout∣ : (m n : ℤ) → ¬ m ≡ 0 → m ∣ n → (bézout m n .coef₁ ≡ 1) × (bézout m n .coef₂ ≡ 0)
bézout∣ = euclid∣ (λ m → discreteℤ m 0) quotRem

-- Divisibility is decidable
dec∣ : (m n : ℤ) → Dec (m ∣ n)
dec∣ m n =
  case discreteℤ m 0
  return (λ _ → Dec (m ∣ n)) of λ
  { (yes p) →
      case discreteℤ n 0
      return (λ _ → Dec (m ∣ n)) of λ
      { (yes p) → yes (subst (m ∣_) (sym p) ∣-zeroʳ)
      ; (no ¬p) → no  (λ r → ¬p (sym (∣-zeroˡ (subst (_∣ n) p r)))) }
  ; (no ¬p) →
      let qr = quotRem m n ¬p in
      case discreteℤ (qr .rem) 0
      return (λ _ → Dec (m ∣ n)) of λ
      { (yes p) → yes (rem≡0→m∣n _ _ qr  p)
      ; (no ¬p) → no  (rem≢0→m∤n _ _ qr ¬p) }}

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Constructions.Product where

open import Data.Bool using (Bool ; true ; false ; not)
open import Data.Empty using (⊥)
open import Data.Product using (_,_ ; proj₁ ; proj₂) renaming (_×_ to _×T_)
open import Level

open import Cats.Category.Base
open import Cats.Category.Constructions.Terminal as Terminal using (HasTerminal)
open import Cats.Functor using (Functor)
open import Cats.Util.Conv

import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Unique as Unique

Bool-elim : ∀ {a} {A : Bool → Set a} → A true → A false → (i : Bool) → A i
Bool-elim x y true = x
Bool-elim x y false = y

module Build {lo la l≈} (Cat : Category lo la l≈) where

  private open module Cat = Category Cat
  open Cat.≈-Reasoning
  open Iso.Build Cat
  open Unique.Build Cat
  open Terminal.Build Cat
  open _≅_

  IsProduct : ∀ {li} {I : Set li} (O : I → Obj) P → (∀ i → P ⇒ O i)
    → Set (lo ⊔ la ⊔ l≈ ⊔ li)
  IsProduct O P proj
      = ∀ {X} (x : ∀ i → X ⇒ O i) → ∃![ u ] (∀ i → x i ≈ proj i ∘ u)

  -- TODO The types of the equalities in IsBinaryProducts are backwards, since
  -- we want the RHS to be simpler than the LHS. So, projl ∘ u ≈ xl instead
  -- of xl ≈ projl ∘ u.
  IsBinaryProduct : ∀ {A B} P → (P ⇒ A) → (P ⇒ B) → Set (lo ⊔ la ⊔ l≈)
  IsBinaryProduct {A} {B} P projl projr
      = ∀ {X} (xl : X ⇒ A) (xr : X ⇒ B)
        → ∃![ u ] (xl ≈ projl ∘ u ×T xr ≈ projr ∘ u)

  IsBinaryProduct→IsProduct : ∀ {A B P} {pl : P ⇒ A} {pr : P ⇒ B}
    → IsBinaryProduct P pl pr
    → IsProduct (Bool-elim A B) P (Bool-elim pl pr)
  IsBinaryProduct→IsProduct isBinProd x = record
      { arr = f ⃗
      ; prop = Bool-elim (proj₁ (∃!′.prop f)) (proj₂ (∃!′.prop f))
      ; unique = λ eq → ∃!′.unique f (eq true , eq false)
      }
    where
      f = isBinProd (x true) (x false)

  record Product {li} {I : Set li} (O : I → Obj) : Set (lo ⊔ la ⊔ l≈ ⊔ li) where
    field
      prod : Obj
      proj : ∀ i → prod ⇒ O i
      isProduct : IsProduct O prod proj

  open Product using (proj ; isProduct)

  instance
    HasObj-Product : ∀ {li} {I : Set li} {O : I → Obj}
      → HasObj (Product O) lo la l≈
    HasObj-Product = record { Cat = Cat ; _ᴼ = Product.prod }

  BinaryProduct : Obj → Obj → Set (lo ⊔ la ⊔ l≈)
  BinaryProduct A B = Product (Bool-elim A B)

  mkBinaryProduct : ∀ {A B P} (pl : P ⇒ A) (pr : P ⇒ B)
    → IsBinaryProduct P pl pr
    → BinaryProduct A B
  mkBinaryProduct {P = P} pl pr isBinProd = record
      { isProduct = IsBinaryProduct→IsProduct isBinProd }

  nullaryProduct-Terminal : (P : Product {I = ⊥} (λ())) → IsTerminal (P ᴼ)
  nullaryProduct-Terminal P X with isProduct P {X = X} λ()
  ... | ∃!-intro arr _ unique = ∃!-intro arr _ (λ _ → unique λ())

  module _ {li} {I : Set li} {O : I → Obj} (P : Product O) where

    factorizer : ∀ {X} → (∀ i → X ⇒ O i) → X ⇒ P ᴼ
    factorizer proj = isProduct P proj ⃗

    factorizer-unique : ∀ {X} (fact : X ⇒ P ᴼ)
      → {x : ∀ i → X ⇒ O i}
      → (∀ i → x i ≈ proj P i ∘ fact)
      → factorizer x ≈ fact
    factorizer-unique fact {x} eq = ∃!′.unique (isProduct P x) eq

    factorizer-proj : ∀ {X} {x : ∀ i → X ⇒ O i} {i}
      → proj P i ∘ factorizer x ≈ x i
    factorizer-proj {x = x} {i} = ≈.sym (∃!′.prop (isProduct P x) i)

    factorizer-resp : ∀ {X} {x y : ∀ i → X ⇒ O i}
      → (∀ i → x i ≈ y i)
      → factorizer x ≈ factorizer y
    factorizer-resp {x = x} {y} eq = factorizer-unique (factorizer y)
      λ i → ≈.trans (eq _) (≈.sym factorizer-proj)

    factorizer-∘ : ∀ {X} {x : ∀ i → X ⇒ O i} {Z} {f : Z ⇒ X}
      → factorizer x ∘ f ≈ factorizer (λ i → x i ∘ f)
    factorizer-∘ {x = x} {f = f} = ≈.sym
      (factorizer-unique (factorizer x ∘ f)
        λ _ → ≈.sym (≈.trans unassoc (∘-resp-l factorizer-proj)))

    factorizer-id : factorizer (proj P) ≈ id
    factorizer-id = factorizer-unique id λ i → ≈.sym id-r

  module _ {li} {I : Set li}
    {O : I → Obj}  (P : Product O)
    {O′ : I → Obj} (P′ : Product O′)
    where

    times : (∀ i → O i ⇒ O′ i) → P ᴼ ⇒ P′ ᴼ
    times x = factorizer P′ (λ i → x i ∘ proj P i)

    times-proj : ∀ {x : ∀ i → O i ⇒ O′ i} {i}
      → proj P′ i ∘ times x ≈ x i ∘ proj P i
    times-proj = factorizer-proj P′

    times-resp : {x y : ∀ i → O i ⇒ O′ i}
      → (∀ i → x i ≈ y i)
      → times x ≈ times y
    times-resp {x} {y} eq = factorizer-resp P′ (λ i → ∘-resp-l (eq i))

  times-id : ∀ {li} {I : Set li} {O : I → Obj} (P : Product O)
    → times P P (λ _ → id) ≈ id
  times-id P = factorizer-unique P id λ _ → ≈.trans id-l (≈.sym id-r)

  times-∘ : ∀ {li} {I : Set li}
    → {O O′ O″ : I → Obj}
    → (P : Product O) (P′ : Product O′) (P″ : Product O″)
    → {x : ∀ i → O i ⇒ O′ i} {y : ∀ i → O′ i ⇒ O″ i}
    → times P′ P″ y ∘ times P P′ x ≈ times P P″ (λ i → y i ∘ x i)
  times-∘ P P′ P″ {x} {y} =
    begin
      times P′ P″ y ∘ times P P′ x
    ≈⟨ factorizer-∘ P″ ⟩
      factorizer P″ (λ i → (y i ∘ proj P′ i) ∘ times P P′ x)
    ≈⟨ factorizer-resp P″ (λ i → assoc) ⟩
      factorizer P″ (λ i → y i ∘ proj P′ i ∘ times P P′ x)
    ≈⟨ factorizer-resp P″ (λ i → ∘-resp-r (times-proj P P′)) ⟩
      factorizer P″ (λ i → y i ∘ x i ∘ proj P i)
    ≈⟨ factorizer-resp P″ (λ i → unassoc) ⟩
      times P P″ (λ i → y i ∘ x i)
    ∎

  times-factorizer : ∀ {li} {I : Set li}
    → {O O′ : I → Obj}
    → (P : Product O) (P′ : Product O′)
    → ∀ {X} {x : ∀ i → X ⇒ O i} {y : ∀ i → O i ⇒ O′ i}
    → times P P′ y ∘ factorizer P x ≈ factorizer P′ (λ i → y i ∘ x i)
  times-factorizer P P′
    = ≈.trans (factorizer-∘ P′)
        (factorizer-resp P′ λ i → ≈.trans assoc (∘-resp-r (factorizer-proj P)))

  proj-cancel : ∀ {li} {I : Set li} {O : I → Obj} {P proj}
    → IsProduct O P proj
    → ∀ {X} {f g : X ⇒ P}
    → (∀ i → proj i ∘ f ≈ proj i ∘ g)
    → f ≈ g
  proj-cancel {proj = proj} prod {f = f} {g} eq with prod (λ i → proj i ∘ g)
  ... | ∃!-intro u _ u-uniq
      = begin
          f
        ≈⟨ ≈.sym (u-uniq (λ i → ≈.sym (eq i))) ⟩
          u
        ≈⟨ u-uniq (λ i → ≈.refl) ⟩
          g
        ∎

  Product-resp-≅ : ∀ {li} {I : Set li} {O O′ : I → Obj}
    → (∀ i → O i ≅ O′ i)
    → (P : Product O) (P′ : Product O′)
    → P ᴼ ≅ P′ ᴼ
  Product-resp-≅ O≅O′ P P′ = record
    { forth = factorizer P′ (λ i → O≅O′ i .forth ∘ proj P i)
    ; back = factorizer P (λ i → O≅O′ i .back ∘ proj P′ i)
    ; back-forth = ≈.trans (factorizer-∘ P)
        (factorizer-unique P id λ i →
          ≈.trans assoc (≈.trans (∘-resp-r (factorizer-proj P′))
            (≈.trans unassoc (≈.trans (∘-resp-l (O≅O′ i .back-forth))
              (≈.trans id-l (≈.sym id-r))))))
    ; forth-back = ≈.trans (factorizer-∘ P′)
        (factorizer-unique P′ id λ i →
          ≈.trans assoc (≈.trans (∘-resp-r (factorizer-proj P))
            (≈.trans unassoc (≈.trans (∘-resp-l (O≅O′ i .forth-back))
              (≈.trans id-l (≈.sym id-r))))))
    }

open Build public using
  (IsProduct ; IsBinaryProduct ; Product ; BinaryProduct ; HasObj-Product)

record HasProducts {lo la l≈} li (C : Category lo la l≈)
  : Set (suc li ⊔ lo ⊔ la ⊔ l≈ )
  where
  private module Bld = Build C
  open Category C
  open Iso.Build C

  field
    Π′ : {I : Set li} (O : I → Obj) → Product C O

  module _ {I : Set li} where

    Π : ∀ (O : I → Obj) → Obj
    Π O = Product.prod (Π′ O)

    syntax Π (λ i → O) = Π[ i ] O

    proj : ∀ {O : I → Obj} i → Π O ⇒ O i
    proj {O} = Bld.Product.proj (Π′ O)

    factorizer : ∀ {O : I → Obj} {X} → (∀ i → X ⇒ O i) → X ⇒ Π O
    factorizer {O} = Bld.factorizer (Π′ O)

    times : ∀ {O O′ : I → Obj} → (∀ i → O i ⇒ O′ i) → Π O ⇒ Π O′
    times {O} {O′} = Bld.times (Π′ O) (Π′ O′)

    factorizer-proj : ∀ {O : I → Obj} {X} {x : ∀ i → X ⇒ O i} {i}
      → proj i ∘ factorizer x ≈ x i
    factorizer-proj {O} = Bld.factorizer-proj (Π′ O)

    factorizer-resp : ∀ {O : I → Obj} {X} {x y : ∀ i → X ⇒ O i}
      → (∀ i → x i ≈ y i)
      → factorizer x ≈ factorizer y
    factorizer-resp {O} = Bld.factorizer-resp (Π′ O)

    factorizer-unique : ∀ {O : I → Obj} {X} {x : ∀ i → X ⇒ O i} {u}
      → (∀ i → x i ≈ proj i ∘ u)
      → factorizer x ≈ u
    factorizer-unique {O} eq = Bld.factorizer-unique (Π′ O) _ eq

    factorizer-∘ : ∀ {O : I → Obj} {X} {x : ∀ i → X ⇒ O i} {Z} {f : Z ⇒ X}
      → factorizer x ∘ f ≈ factorizer (λ i → x i ∘ f)
    factorizer-∘ {O} = Bld.factorizer-∘ (Π′ O)

    factorizer-id : ∀ {O} → factorizer {O} proj ≈ id
    factorizer-id {O} = Bld.factorizer-id (Π′ O)

    times-proj : ∀ {O O′ : I → Obj} {x : ∀ i → O i ⇒ O′ i} {i}
      → proj i ∘ times x ≈ x i ∘ proj i
    times-proj {O} {O′} = Bld.times-proj (Π′ O) (Π′ O′)

    times-resp : ∀ {O O′ : I → Obj} {x y : ∀ i → O i ⇒ O′ i}
      → (∀ i → x i ≈ y i)
      → times x ≈ times y
    times-resp {O} {O′} = Bld.times-resp (Π′ O) (Π′ O′)

    times-id : ∀ {O : I → Obj} → times {O} (λ _ → id) ≈ id
    times-id {O} = Bld.times-id (Π′ O)

    times-∘ : ∀ {O O′ O″ : I → Obj} {x : ∀ i → O i ⇒ O′ i} {y : ∀ i → O′ i ⇒ O″ i}
      → times y ∘ times x ≈ times (λ i → y i ∘ x i)
    times-∘ {O} {O′} {O″} = Bld.times-∘ (Π′ O) (Π′ O′) (Π′ O″)

    times-factorizer : ∀ {O O′ : I → Obj} {X}
      → {x : ∀ i → X ⇒ O i} {y : ∀ i → O i ⇒ O′ i}
      → times y ∘ factorizer x ≈ factorizer (λ i → y i ∘ x i)
    times-factorizer {O} {O′} = Bld.times-factorizer (Π′ O) (Π′ O′)

    Π-resp-≅ : ∀ {O O′ : I → Obj}
      → (∀ i → O i ≅ O′ i)
      → Π O ≅ Π O′
    Π-resp-≅ {O} {O′} O≅O′ = Bld.Product-resp-≅ O≅O′ (Π′ O) (Π′ O′)

HasProducts→HasTerminal : ∀ {lo la l≈} {C : Category lo la l≈}
  → HasProducts zero C
  → HasTerminal C
HasProducts→HasTerminal {C = C} record { Π′ = Π }
    = let P = Π {I = ⊥} λ() in
      record
        { ⊤ = Product.prod P
        ; isTerminal = Build.nullaryProduct-Terminal C P
        }

record HasBinaryProducts {lo la l≈} (C : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈)
  where
  private module Bld = Build C
  open Category C
  open Iso.Build C
  open ≈-Reasoning

  infixr 2 _×_ _×′_ ⟨_×_⟩ ⟨_,_⟩

  field
    _×′_ : ∀ A B → BinaryProduct C A B

  _×_ : Obj → Obj → Obj
  A × B = (A ×′ B) ᴼ

  projl : ∀ {A B} → A × B ⇒ A
  projl {A} {B} = Product.proj (A ×′ B) true

  projr : ∀ {A B} → A × B ⇒ B
  projr {A} {B} = Product.proj (A ×′ B) false

  ⟨_,_⟩ : ∀ {A B Z} → Z ⇒ A → Z ⇒ B → Z ⇒ A × B
  ⟨_,_⟩ {A} {B} f g
      = Bld.factorizer (A ×′ B) (Bool-elim f g)

  ⟨_×_⟩ : ∀ {A B A′ B′} → A ⇒ A′ → B ⇒ B′ → A × B ⇒ A′ × B′
  ⟨_×_⟩ {A} {B} {A′} {B′} f g
      = Bld.times (A ×′ B) (A′ ×′ B′) (Bool-elim f g)

  first : ∀ {A A′ B} → A ⇒ A′ → A × B ⇒ A′ × B
  first f = ⟨ f × id ⟩

  second : ∀ {A B B′} → B ⇒ B′ → A × B ⇒ A × B′
  second f = ⟨ id × f ⟩

  swap : ∀ {A B} → A × B ⇒ B × A
  swap = ⟨ projr , projl ⟩

  ⟨,⟩-resp : ∀ {A B Z} {f f′ : Z ⇒ A} {g g′ : Z ⇒ B}
    → f ≈ f′
    → g ≈ g′
    → ⟨ f , g ⟩ ≈ ⟨ f′ , g′ ⟩
  ⟨,⟩-resp {A} {B} f≈f′ g≈g′
      = Bld.factorizer-resp (A ×′ B) (Bool-elim f≈f′ g≈g′)

  ⟨,⟩-projl : ∀ {A B Z} {f : Z ⇒ A} {g : Z ⇒ B} → projl ∘ ⟨ f , g ⟩ ≈ f
  ⟨,⟩-projl {A} {B} = Bld.factorizer-proj (A ×′ B)

  ⟨,⟩-projr : ∀ {A B Z} {f : Z ⇒ A} {g : Z ⇒ B} → projr ∘ ⟨ f , g ⟩ ≈ g
  ⟨,⟩-projr {A} {B} = Bld.factorizer-proj (A ×′ B)

  ⟨,⟩-unique : ∀ {A B Z} {f : Z ⇒ A} {g : Z ⇒ B} {u}
    → f ≈ projl ∘ u
    → g ≈ projr ∘ u
    → ⟨ f , g ⟩ ≈ u
  ⟨,⟩-unique {A} {B} eql eqr
    = Bld.factorizer-unique (A ×′ B) _ (Bool-elim eql eqr)

  ⟨,⟩-∘ : ∀ {A B Y Z} {f : Y ⇒ Z} {g : Z ⇒ A} {h : Z ⇒ B}
    → ⟨ g , h ⟩ ∘ f ≈ ⟨ g ∘ f , h ∘ f ⟩
  ⟨,⟩-∘ {A} {B} {Y} {Z} {f} {g} {h}
      = begin
          ⟨ g , h ⟩ ∘ f
        ≈⟨ Bld.factorizer-∘ (A ×′ B) ⟩
          Bld.factorizer (A ×′ B)
            (λ i → Bool-elim {A = λ i → Z ⇒ Bool-elim A B i} g h i ∘ f)
        ≈⟨ Bld.factorizer-resp (A ×′ B) (Bool-elim ≈.refl ≈.refl) ⟩
          ⟨ g ∘ f , h ∘ f ⟩
        ∎

  ⟨,⟩-id : ∀ {A B} → ⟨ projl , projr ⟩ ≈ id {A × B}
  ⟨,⟩-id {A} {B} = ⟨,⟩-unique (≈.sym id-r) (≈.sym id-r)

  ⟨×⟩-resp : ∀ {A A′ B B′} {f f′ : A ⇒ A′} {g g′ : B ⇒ B′}
    → f ≈ f′
    → g ≈ g′
    → ⟨ f × g ⟩ ≈ ⟨ f′ × g′ ⟩
  ⟨×⟩-resp {A} {A′} {B} {B′} f≈f′ g≈g′
      = Bld.times-resp (A ×′ B) (A′ ×′ B′) (Bool-elim f≈f′ g≈g′)

  ⟨×⟩-projl : ∀ {A A′ B B′} {f : A ⇒ A′} {g : B ⇒ B′}
    → projl ∘ ⟨ f × g ⟩ ≈ f ∘ projl
  ⟨×⟩-projl {A} {A′} {B} {B′} = Bld.times-proj (A ×′ B) (A′ ×′ B′)

  ⟨×⟩-projr : ∀ {A A′ B B′} {f : A ⇒ A′} {g : B ⇒ B′}
    → projr ∘ ⟨ f × g ⟩ ≈ g ∘ projr
  ⟨×⟩-projr {A} {A′} {B} {B′} = Bld.times-proj (A ×′ B) (A′ ×′ B′)

  ⟨×⟩-id : ∀ {A B} → ⟨ id {A} × id {B} ⟩ ≈ id
  ⟨×⟩-id {A} {B} = Bld.factorizer-unique (A ×′ B) id
    (Bool-elim (≈.trans id-l (≈.sym id-r)) (≈.trans id-l (≈.sym id-r)))

  ⟨×⟩-∘ : ∀ {A A′ A″ B B′ B″}
    → {f : A′ ⇒ A″} {f′ : A ⇒ A′} {g : B′ ⇒ B″} {g′ : B ⇒ B′}
    → ⟨ f × g ⟩ ∘ ⟨ f′ × g′ ⟩ ≈ ⟨ f ∘ f′ × g ∘ g′ ⟩
  ⟨×⟩-∘ {A} {A′} {A″} {B} {B′} {B″} {f} {f′} {g} {g′} = ≈.trans
    (Bld.times-∘ (A ×′ B) (A′ ×′ B′) (A″ ×′ B″))
    (Bld.times-resp (A ×′ B) (A″ ×′ B″) (Bool-elim ≈.refl ≈.refl))

  ⟨×⟩-⟨,⟩ : ∀ {A B C B′ C′} {f : A ⇒ B} {g : A ⇒ C} {f′ : B ⇒ B′} {g′ : C ⇒ C′}
    → ⟨ f′ × g′ ⟩ ∘ ⟨ f , g ⟩ ≈ ⟨ f′ ∘ f , g′ ∘ g ⟩
  ⟨×⟩-⟨,⟩ {A} {B} {C} {B′} {C′} = ≈.trans
    (Bld.times-factorizer (B ×′ C) (B′ ×′ C′))
    (Bld.factorizer-resp (B′ ×′ C′) (Bool-elim ≈.refl ≈.refl))

  ×-resp-≅ : ∀ {A A′ B B′}
    → A ≅ A′
    → B ≅ B′
    → (A × B) ≅ (A′ × B′)
  ×-resp-≅ {A} {A′} {B} {B′} A≅A′ B≅B′
    = Bld.Product-resp-≅ (Bool-elim A≅A′ B≅B′) (A ×′ B) (A′ ×′ B′)

-- The following is conceptually trivial, but we have to dig quite deep to
-- avoid level-related nonsense.
HasProducts→HasBinaryProducts : ∀ {lp lo la l≈} {C : Category lo la l≈}
  → HasProducts lp C
  → HasBinaryProducts C
HasProducts→HasBinaryProducts {lp} {C = C} record { Π′ = Π }
    = record { _×′_ = _×_ }
  where
    open Category C
    open Unique.Build C
    open Product using (proj)
    open ∃!′ using (arr ; prop ; unique)

    _×_ : ∀ A B → Build.BinaryProduct C A B
    A × B = record
        { prod = prod′
        ; proj = proj′
        ; isProduct = isProduct′
        }
      where
        O : Lift lp Bool → _
        O (lift true) = A
        O (lift false) = B

        prod′ = Product.prod (Π O)

        proj′ = Bool-elim (proj (Π O) (lift true)) (proj (Π O) (lift false))

        isProduct′ : IsProduct C (Bool-elim A B) prod′ proj′
        isProduct′ {X} x = record
            { arr = arr′ ⃗
            ; prop = Bool-elim (prop arr′ (lift true)) (prop arr′ (lift false))
            ; unique = λ eq → unique arr′
                (λ { (lift true) → eq true ; (lift false) → eq false})
            }
          where
            arr′ = Product.isProduct (Π O)
              λ { (lift true) → x true ; (lift false) → x false}

record HasFiniteProducts {lo la l≈} (Cat : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈)
  where

  field
    {{hasTerminal}} : HasTerminal Cat
    {{hasBinaryProducts}} : HasBinaryProducts Cat

  open HasTerminal hasTerminal public
  open HasBinaryProducts hasBinaryProducts public

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈}
  {D : Category lo′ la′ l≈′}
  where

  open Category C
  open Functor

  PreservesBinaryProducts : (F : Functor C D) → Set _
  PreservesBinaryProducts F
    = ∀ {A B A×B} {projl : A×B ⇒ A} {projr : A×B ⇒ B}
    → IsBinaryProduct C A×B projl projr
    → IsBinaryProduct D (fobj F A×B) (fmap F projl) (fmap F projr)

  PreservesProducts : ∀ {i} (I : Set i) (F : Functor C D) → Set _
  PreservesProducts I F
    = ∀ {O : I → Obj} {P} {proj : ∀ i → P ⇒ O i}
    → IsProduct C O P proj
    → IsProduct D (λ i → fobj F (O i)) (fobj F P) (λ i → fmap F (proj i))

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


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

   Copyright (c) 2020 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.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Abstract.Types

module LibraBFT.Abstract.BFT where

  -- This is a utility function to make it easy to provide the bft-assumption
  -- for the abstract EpochConfig by by assuming that at most bizF members are byzantine
  -- and that authorsN ≥ suc (3 * bizF) and that a list of Members is a quorum if it
  -- contains at least authorsN ∸ bizF distinct Members.


text:
module Luau.Syntax.ToString where

open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_is_end)
open import FFI.Data.String using (String; _++_)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Var.ToString using (varToString)

exprToString′ : String → Expr → String
statToString′ : String → Stat → String
blockToString′ : String → Block → String

exprToString′ lb nil =
  "nil"
exprToString′ lb (addr a) =
  addrToString(a)
exprToString′ lb (var x) =
  varToString(x)
exprToString′ lb (M $ N) =
  (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
exprToString′ lb (function⟨ x ⟩ B end) =
  "function(" ++ x ++ ")" ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end"
exprToString′ lb (block b is B end) =
  "(function " ++ b ++ "()" ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end)()"

statToString′ lb (function f ⟨ x ⟩ B end) =
  "local function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end"
statToString′ lb (local x ← M) =
  "local " ++ x ++ " = " ++ (exprToString′ lb M)
statToString′ lb (return M) =
  "return " ++ (exprToString′ lb M)

blockToString′ lb (S ∙ done) = statToString′ lb S
blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
blockToString′ lb (done) = ""

exprToString : Expr → String
exprToString = exprToString′ "\n"

statToString : Stat → String
statToString = statToString′ "\n"

blockToString : Block → String
blockToString = blockToString′ "\n"

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
-- This module is responsible for adding the missing scope information to the parse tree.

module ScopeParseTree where
open import ParseTree
open import Data.Empty
open import ScopeState
open import Data.List hiding (_++_)
open import Data.Product hiding (map)
open import Data.Fin
open import Data.Nat
open import Data.Sum
open import Data.String
open import Data.Bool
open import AgdaHelperFunctions

scopeSignature : TypeSignature -> ScopeType -> ScopeState TypeSignature

scopeExpr : Expr -> ScopeState Expr
scopeExpr (ident identifier₁) = do
  -- first try to find identifier among already declared (simplification for constructor), then assume new declaration (simplification for parameter or out-of-file declaration)
  inj₂ r <- try $ fillInIdentifier identifier₁
   where _ ->  do x <- addIdentifier identifier₁
                  return $ ident x
  return $ ident r
scopeExpr (functionApp e e₁ {b} ) = do
  r1 <- scopeExpr e
  r2 <- scopeExpr e₁
  return $ functionApp r1 r2 {b}
scopeExpr (namedArgument arg {b} {bef} {aft}) = do
  x <- scopeSignature arg addVariableToType
  return $ namedArgument x {b}{bef}{aft}
scopeExpr x = return x

scopeSignature (typeSignature funcName funcType) scopeT = do
    newType <- saveAndReturnToScope $ scopeExpr funcType
    addScope scopeT
    newId <- addIdentifier funcName
    return $ typeSignature newId newType

scopePragma : Pragma -> ScopeState Pragma
scopePragma (builtin concept definition) = do
  x <- fillInIdentifier definition
  return $ builtin concept x
scopePragma x = return x

scopeParseTree : ParseTree -> ScopeState ParseTree
scopeParseTree (signature signature₁ range₁) = do
  x <- scopeSignature signature₁ addFuncToModule
  return $ signature x range₁
scopeParseTree (functionDefinition definitionOf params body range₁) = do
  newId <- fillInIdentifier definitionOf
  x <- saveAndReturnToScope $ do
          addScope funcDef
          newParams <- mapState scopeExpr params
          newBody <- scopeExpr body
          return $ functionDefinition newId newParams newBody range₁
  return x
scopeParseTree
  (dataStructure dataName parameters indexInfo constructors range₁ {comments}) = do
    addScope $ moduleDef dataName
    newDataName <- addIdentifier dataName
    ( newParams , newIndex) , newCons <- saveAndReturnToScope $ do
              newParams <- mapState (λ x -> scopeSignature x addVariableToType) parameters
              newIndex <- scopeExpr indexInfo
              newCons <- mapState (λ x -> scopeSignature x addFuncToModule) constructors
              return ((newParams , newIndex) , newCons)
    r <- mapState addContentReferenceToModuleTop newCons
    return $ dataStructure newDataName newParams newIndex newCons range₁ {comments}
scopeParseTree (moduleName moduleName₁ range₁) = do
  newMod <- addIdentifier moduleName₁
  addScope $ moduleDef moduleName₁
  return $ moduleName newMod range₁
scopeParseTree (pragma pragma₁ range₁) = do
  x <- scopePragma pragma₁
  return $ pragma x range₁
scopeParseTree x = return x

scopeParseTreeList : List ParseTree -> ScopeState (List ParseTree)
scopeParseTreeList program = do
  --TODO: fix sloppy workaround
  put newEnv
  addIdentifier (identifier "Set" (λ _ -> before) 0 0 {true}{[]} {[]})
  mapState scopeParseTree program


text:
-- Andreas, 2017-10-17, issue #2807
--
-- Refining with an extended lambda gave internal error.
-- Seemed to be triggered only when giving resulted in an error.

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v scope.extendedLambda:60 #-}
-- {-# OPTIONS -v impossible:10 #-}

data ⊥ : Set where
  actuallyNotEmpty : ⊥

data D : Set where
  c : ⊥ → D

test : D → ⊥
test = {! λ{ (c ()) }!}  -- C-c C-r

-- WAS: internal error in ConcreteToAbstract (insertApp)
--
-- Expected:
-- Succeed with unsolved constraints and metas.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence
open import HoTT.Identity.Pi
open import HoTT.Identity.Sigma

module HoTT.Exercises.Chapter2.Exercise11 where

private
  variable
    i j k : Level
    A B C D : 𝒰 i

pullback : (A : 𝒰 i) (B : 𝒰 j) → (A → C) → (B → C) → 𝒰 _
pullback A B ac bc = Σ[ a ∶ A ] Σ[ b ∶ B ] (ac a == bc b)

module Square (ab : A → B) (ac : A → C) (bd : B → D) (cd : C → D)
  where
  IsCommutative = bd ∘ ab ~ cd ∘ ac

  module Commutative (comm : IsCommutative)
    where
    inducedMap : {X : 𝒰 i} → (X → A) → pullback (X → B) (X → C) (bd ∘_) (cd ∘_)
    inducedMap xa = ab ∘ xa , ac ∘ xa , funext (comm ∘ xa)

    IsPullback : ∀ {i} → 𝒰 _
    IsPullback {i} = (X : 𝒰 i) → isequiv (inducedMap {X = X})

  open Commutative public

module _ {ac : A → C} {bc : B → C}
  where
  P = pullback A B ac bc

  open Square.Commutative {A = P} pr₁ (pr₁ ∘ pr₂) ac bc (pr₂ ∘ pr₂)

  prop : IsPullback {i}
  prop X = qinv→isequiv (g , η , ε)
    where
    f = inducedMap
    g : pullback (X → A) (X → B) (ac ∘_) (bc ∘_) → (X → P)
    g (h' , k' , p) x = h' x , k' x , happly p x
    η : g ∘ f ~ id
    η xp = funext λ x → pair⁼ (refl , pair⁼ (refl ,
      happly (=Π-β (pr₂ ∘ pr₂ ∘ xp)) x))
    ε : f ∘ g ~ id
    ε (_ , _ , p) = pair⁼ (refl , pair⁼ (refl , =Π-η p))

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott