text:
{-

In this file we apply the cubical machinery to Martin Hötzel-Escardó's
structure identity principle:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#sns

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.SIP where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence renaming (ua-pathToEquiv to ua-pathToEquiv')
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.FunExtEquiv
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HAEquiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Data.Prod.Base hiding (_×_) renaming (_×Σ_ to _×_)

private
 variable
  ℓ ℓ' ℓ'' ℓ''' ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ : Level

-- For technical reasons we reprove ua-pathToEquiv using the
-- particular proof constructed by iso→HAEquiv. The reason is that we
-- want to later be able to extract
--
--   eq : ua-au (ua e) ≡ cong ua (au-ua e)
--
uaHAEquiv : (A B : Type ℓ) → HAEquiv (A ≃ B) (A ≡ B)
uaHAEquiv A B = iso→HAEquiv (iso ua pathToEquiv ua-pathToEquiv' pathToEquiv-ua)
open isHAEquiv

-- We now extract the particular proof constructed from iso→HAEquiv
-- for reasons explained above.
ua-pathToEquiv : {A B : Type ℓ} (e : A ≡ B) → ua (pathToEquiv e) ≡ e
ua-pathToEquiv e = uaHAEquiv _ _ .snd .ret e

-- A structure is a type-family S : Type ℓ → Type ℓ', i.e. for X : Type ℓ and s : S X, the pair (X , s)
-- means that X is equipped with a S-structure, which is witnessed by s.
-- An S-structure should have a notion of S-homomorphism, or rather S-isomorphism.
-- This will be implemented by a function ι
-- that gives us for any two types with S-structure (X , s) and (Y , t) a family:
--    ι (X , s) (Y , t) : (X ≃ Y) → Type ℓ''
-- Note that for any equivalence (f , e) : X ≃ Y the type  ι (X , s) (Y , t) (f , e) need not to be
-- a proposition. Indeed this type should correspond to the ways s and t can be identified
-- as S-structures. This we call a standard notion of structure or SNS.
-- We will use a different definition, but the two definitions are interchangeable.
SNS : (S : Type ℓ → Type ℓ')
    → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
    → Type (ℓ-max (ℓ-max(ℓ-suc ℓ) ℓ') ℓ'')
SNS  {ℓ = ℓ} S ι = ∀ {X : (Type ℓ)} (s t : S X) → ((s ≡ t) ≃ ι (X , s) (X , t) (idEquiv X))

-- We introduce the notation for structure preserving equivalences a bit differently,
-- but this definition doesn't actually change from Escardó's notes.
_≃[_]_ : {S : Type ℓ → Type ℓ'}
       → (A : Σ[ X ∈ (Type ℓ) ] (S X))
       → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
       → (B : Σ[ X ∈ (Type ℓ) ] (S X))
       → Type (ℓ-max ℓ ℓ'')
A ≃[ ι ] B = Σ[ f ∈ ((A .fst) ≃ (B. fst)) ] (ι A B f)

-- Before we can formulate our version of an SNS we introduce a bit of
-- notation and prove a few basic results. First, we define the
-- "cong-≃":
_⋆_ : (S : Type ℓ → Type ℓ') → {X Y : Type ℓ} → (X ≃ Y) → S X ≃ S Y
S ⋆ f = pathToEquiv (cong S (ua f))

-- Next, we prove a couple of helpful results about this ⋆ operation:
⋆-idEquiv : (S : Type ℓ → Type ℓ') (X : Type ℓ) → S ⋆ (idEquiv X) ≡ idEquiv (S X)
⋆-idEquiv S X = S ⋆ (idEquiv X)  ≡⟨ cong (λ p → pathToEquiv (cong S p)) uaIdEquiv  ⟩
                pathToEquiv refl ≡⟨ pathToEquivRefl ⟩
                idEquiv (S X)    ∎

⋆-char : (S : Type ℓ → Type ℓ') {X Y : Type ℓ} (f : X ≃ Y) → ua (S ⋆ f) ≡ cong S (ua f)
⋆-char S f = ua-pathToEquiv (cong S (ua f))

PathP-⋆-lemma : (S : Type ℓ → Type ℓ') (A B : Σ[ X ∈ (Type ℓ) ] (S X)) (f : A .fst ≃ B .fst)
    → (PathP (λ i →  ua (S ⋆ f) i) (A .snd) (B .snd)) ≡ (PathP (λ i → S ((ua f) i)) (A .snd) (B .snd))
PathP-⋆-lemma S A B f i = PathP (λ j → (⋆-char S f) i j) (A .snd) (B .snd)

-- Our new definition of standard notion of structure SNS' using the ⋆ notation.
-- This is easier to work with than SNS wrt Glue-types
SNS' : (S : Type ℓ → Type ℓ')
     → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
     → Type (ℓ-max (ℓ-max(ℓ-suc ℓ) ℓ') ℓ'')
SNS' S ι = (A B : Σ[ X ∈ (Type _) ] (S X)) → (f : A .fst ≃ B .fst)
         → (equivFun (S ⋆ f) (A .snd) ≡ (B .snd)) ≃ (ι A B f)

-- We can unfold SNS' as follows:
SNS'' : (S : Type ℓ → Type ℓ')
     → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
     → Type (ℓ-max (ℓ-max(ℓ-suc ℓ) ℓ') ℓ'')
SNS''  S ι = (A B : Σ[ X ∈ (Type _) ] (S X)) → (f : A .fst ≃ B .fst)
          → (transport (λ i → S (ua f i)) (A .snd) ≡ (B .snd)) ≃ (ι A B f)

SNS'≡SNS'' : (S : Type ℓ → Type ℓ')
           → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
           → SNS' S ι ≡ SNS'' S ι
SNS'≡SNS'' S ι = refl

-- A quick sanity-check that our definition is interchangeable with
-- Escardó's. The direction SNS→SNS' corresponds more or less to an
-- EquivJ formulation of Escardó's homomorphism-lemma.
SNS'→SNS : (S : Type ℓ → Type ℓ')
         → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
         → SNS' S ι → SNS S ι
SNS'→SNS S ι θ {X = X} s t = subst (λ x → (equivFun x s ≡ t) ≃ ι (X , s) (X , t) (idEquiv X)) (⋆-idEquiv S X) θ-id
  where
   θ-id = θ (X , s) (X , t) (idEquiv X)

SNS→SNS' : (S : Type ℓ → Type ℓ')
         → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
         → SNS S ι → SNS' S ι
SNS→SNS' S ι θ A B f = EquivJ P C (B .fst) (A .fst) f (B .snd) (A .snd)
  where
   P : (X Y : Type _) → Y ≃ X → Type _
   P X Y g = (s : S X) (t : S Y) → (equivFun (S ⋆ g) t ≡ s) ≃ ι (Y , t) (X , s) g

   C : (X : Type _) → (s t : S X) → (equivFun (S ⋆ (idEquiv X)) t ≡ s) ≃ ι (X , t) (X , s) (idEquiv X)
   C X s t = subst (λ u →  (u ≡ s) ≃ (ι (X , t) (X , s) (idEquiv X)))
                   (sym ( cong (λ f → (equivFun f) t) (⋆-idEquiv S X))) (θ t s)

-- The following transport-free version of SNS'' is a bit easier to
-- work with for the proof of the SIP
SNS''' : (S : Type ℓ → Type ℓ')
       → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
       → Type (ℓ-max (ℓ-max(ℓ-suc ℓ) ℓ') ℓ'')
SNS''' S ι = (A B : Σ[ X ∈ (Type _) ] (S X)) → (e : A .fst ≃ B .fst)
          → (PathP (λ i → S (ua e i)) (A .snd) (B .snd)) ≃ ι A B e

-- We can easily go between SNS'' (which is def. equal to SNS') and SNS'''
-- We should be able to find are more direct version of PathP≃Path for the family (λ i → S (ua f i))
-- using glue and unglue terms.
SNS''→SNS''' : {S : Type ℓ → Type ℓ'}
             → {ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ''}
             → SNS'' S ι → SNS''' S ι
SNS''→SNS''' {S = S} h A B f =  PathP (λ i → S (ua f i)) (A .snd) (B .snd)
                             ≃⟨ PathP≃Path (λ i → S (ua f i)) (A .snd) (B .snd) ⟩
                                h A B f

SNS'''→SNS'' : (S : Type ℓ → Type ℓ')
             → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
             → SNS''' S ι → SNS'' S ι
SNS'''→SNS'' S ι h A B f =  transport (λ i → S (ua f i)) (A .snd) ≡ (B .snd)
                         ≃⟨ invEquiv (PathP≃Path (λ i → S (ua f i)) (A .snd) (B .snd)) ⟩
                            h A B f

-- We can now directly define a function
--    sip : A ≃[ ι ] B → A ≡ B
-- together with is inverse.
-- Here, these functions use SNS''' and are expressed using a Σ-type instead as it is a bit
-- easier to work with
sip : (S : Type ℓ → Type ℓ')
    → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
    → (θ : SNS''' S ι)
    → (A B : Σ[ X ∈ (Type ℓ) ] (S X))
    → A ≃[ ι ] B
    → Σ (A .fst ≡ B .fst) (λ p → PathP (λ i → S (p i)) (A .snd) (B .snd))
sip S ι θ A B (e , p) = ua e , invEq (θ A B e) p

-- The inverse to sip using the following little lemma
lem : (S : Type ℓ → Type ℓ')
      (A B : Σ[ X ∈ (Type ℓ) ] (S X))
      (e : A .fst ≡ B .fst)
    → PathP (λ i → S (ua (pathToEquiv e) i)) (A .snd) (B .snd) ≡
      PathP (λ i → S (e i)) (A .snd) (B .snd)
lem S A B e i = PathP (λ j → S (ua-pathToEquiv e i j)) (A .snd) (B .snd)

sip⁻ : (S : Type ℓ → Type ℓ')
     → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
     → (θ : SNS''' S ι)
     → (A B : Σ[ X ∈ (Type ℓ) ] (S X))
     → Σ (A .fst ≡ B .fst) (λ p → PathP (λ i → S (p i)) (A .snd) (B .snd))
     → A ≃[ ι ] B
sip⁻ S ι θ A B (e , r) = pathToEquiv e , θ A B (pathToEquiv e) .fst q
  where
  q : PathP (λ i → S (ua (pathToEquiv e) i)) (A .snd) (B .snd)
  q = transport (λ i → lem S A B e (~ i)) r

-- we can rather directly show that sip and sip⁻ are mutually inverse:
sip-sip⁻ : (S : Type ℓ → Type ℓ')
         → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
         → (θ : SNS''' S ι)
         → (A B : Σ[ X ∈ (Type ℓ) ] (S X))
         → (r : Σ (A .fst ≡ B .fst) (λ p → PathP (λ i → S (p i)) (A .snd) (B .snd)))
         → sip S ι θ A B (sip⁻ S ι θ A B r) ≡ r
sip-sip⁻ S ι θ A B (p , q) =
    sip S ι θ A B (sip⁻ S ι θ A B (p , q))
  ≡⟨ refl ⟩
    ua (pathToEquiv p) , invEq (θ A B (pathToEquiv p)) (θ A B (pathToEquiv p) .fst (transport (λ i → lem S A B p (~ i)) q))
  ≡⟨ (λ i → ua (pathToEquiv p) , secEq (θ A B (pathToEquiv p)) (transport (λ i → lem S A B p (~ i)) q) i) ⟩
    ua (pathToEquiv p) , transport (λ i → lem S A B p (~ i)) q
  ≡⟨ (λ i → ua-pathToEquiv p i ,
            transp (λ k → PathP (λ j → S (ua-pathToEquiv p (i ∧ k) j)) (A .snd) (B .snd))
                   (~ i)
                   (transport (λ i → lem S A B p (~ i)) q)) ⟩
    p , transport (λ i → lem S A B p i) (transport (λ i → lem S A B p (~ i)) q)
  ≡⟨ (λ i → p , transportTransport⁻ (lem S A B p) q i) ⟩
    p , q ∎

-- The trickier direction:
sip⁻-sip : (S : Type ℓ → Type ℓ')
         → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
         → (θ : SNS''' S ι)
         → (A B : Σ[ X ∈ (Type ℓ) ] (S X))
         → (r : A ≃[ ι ] B)
         → sip⁻ S ι θ A B (sip S ι θ A B r) ≡ r
sip⁻-sip S ι θ A B (e , p) =
    sip⁻ S ι θ A B (sip S ι θ A B (e , p))
  ≡⟨ refl ⟩
    pathToEquiv (ua e) , θ A B (pathToEquiv (ua e)) .fst (f⁺ p')
  ≡⟨ (λ i → pathToEquiv-ua e i , θ A B (pathToEquiv-ua e i) .fst (pth' i)) ⟩
    e , θ A B e .fst (f⁻ (f⁺ p'))
  ≡⟨ (λ i → e , θ A B e .fst (transportTransport⁻ (lem S A B (ua e)) p' i)) ⟩
    e , θ A B e .fst (invEq (θ A B e) p)
  ≡⟨ (λ i → e , (retEq (θ A B e) p i)) ⟩
    e , p ∎
  where
  p' : PathP (λ i → S (ua e i)) (A .snd) (B .snd)
  p' = invEq (θ A B e) p

  f⁺ : PathP (λ i → S (ua e i)) (A .snd) (B .snd)
     → PathP (λ i → S (ua (pathToEquiv (ua e)) i)) (A .snd) (B .snd)
  f⁺ = transport (λ i → PathP (λ j → S (ua-pathToEquiv (ua e) (~ i) j)) (A .snd) (B .snd))

  f⁻ : PathP (λ i → S (ua (pathToEquiv (ua e)) i)) (A .snd) (B .snd)
     → PathP (λ i → S (ua e i)) (A .snd) (B .snd)
  f⁻ = transport (λ i → PathP (λ j → S (ua-pathToEquiv (ua e) i j)) (A .snd) (B .snd))

  -- We can prove the following as in sip∘pis-id, but the type is not
  -- what we want as it should be "cong ua (pathToEquiv-ua e)"
  pth : PathP (λ j → PathP (λ k → S (ua-pathToEquiv (ua e) j k)) (A .snd) (B .snd))
              (f⁺ p') (f⁻ (f⁺ p'))
  pth i = transp (λ k → PathP (λ j → S (ua-pathToEquiv (ua e) (i ∧ k) j)) (A .snd) (B .snd))
                 (~ i)
                 (f⁺ p')

  -- So we build an equality that we want to cast the types with
  casteq : PathP (λ j → PathP (λ k → S (ua-pathToEquiv (ua e) j k)) (A .snd) (B .snd))
                 (f⁺ p') (f⁻ (f⁺ p'))
         ≡ PathP (λ j → PathP (λ k → S (cong ua (pathToEquiv-ua e) j k)) (A .snd) (B .snd))
                 (f⁺ p') (f⁻ (f⁺ p'))
  casteq i = PathP (λ j → PathP (λ k → S (eq i j k)) (A .snd) (B .snd)) (f⁺ p') (f⁻ (f⁺ p'))
    where
    -- This is where we need the half-adjoint equivalence property
    eq : ua-pathToEquiv (ua e) ≡ cong ua (pathToEquiv-ua e)
    eq = sym (uaHAEquiv (A .fst) (B .fst) .snd .com e)

  -- We then get a term of the type we need
  pth' : PathP (λ j → PathP (λ k → S (cong ua (pathToEquiv-ua e) j k)) (A .snd) (B .snd))
               (f⁺ p') (f⁻ (f⁺ p'))
  pth' = transport (λ i → casteq i) pth

-- Finally package everything up to get the cubical SIP
SIP : (S : Type ℓ → Type ℓ')
    → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
    → (θ : SNS''' S ι)
    → (A B : Σ[ X ∈ (Type ℓ) ] (S X))
    → A ≃[ ι ] B ≃ (A ≡ B)
SIP S ι θ A B = (A ≃[ ι ] B ) ≃⟨ eq ⟩ Σ≡
  where
  eq : A ≃[ ι ] B ≃ Σ (A .fst ≡ B .fst) (λ p → PathP (λ i → S (p i)) (A .snd) (B .snd))
  eq = isoToEquiv (iso (sip S ι θ A B) (sip⁻ S ι θ A B)
                       (sip-sip⁻ S ι θ A B) (sip⁻-sip S ι θ A B))

-- Now, we want to add axioms (i.e. propositions) to our Structure S that don't affect the ι.
-- For this and the remainder of this file we will work with SNS'
-- We use a lemma due to Zesen Qian, which can now be found in Foundations.Prelude:
-- https://github.com/riaqn/cubical/blob/hgroup/Cubical/Data/Group/Properties.agda#L83
add-to-structure : (S : Type ℓ → Type ℓ')
                   (axioms : (X : Type ℓ) → (S X) → Type ℓ''')
                 → Type ℓ → Type (ℓ-max ℓ' ℓ''')
add-to-structure S axioms X = Σ[ s ∈ S X ] (axioms X s)

add-to-iso : (S : Type ℓ → Type ℓ')
             (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
             (axioms : (X : Type ℓ) → (S X) → Type ℓ''')
           → (A B : Σ[ X ∈ (Type ℓ) ] (add-to-structure S axioms X)) → A .fst ≃ B .fst
           → Type ℓ''
add-to-iso S ι axioms (X , (s , a)) (Y , (t , b)) f = ι (X , s) (Y , t) f

add-⋆-lemma : (S : Type ℓ → Type ℓ')
              (axioms : (X : Type ℓ) → (S X) → Type ℓ''')
              (axioms-are-Props : (X : Type ℓ) (s : S X) → isProp (axioms X s))
              {X Y : Type ℓ} {s : S X} {t : S Y} {a : axioms X s} {b : axioms Y t}
              (f : X ≃ Y)
            → (equivFun (add-to-structure S axioms ⋆ f) (s , a) ≡ (t , b)) ≃ (equivFun (S ⋆ f) s ≡ t)
add-⋆-lemma S axioms axioms-are-Props {Y = Y} {s = s} {t = t} {a = a} {b = b} f = isoToEquiv (iso φ ψ η ε)
      where
       φ : equivFun ((add-to-structure S axioms) ⋆ f) (s , a) ≡ (t , b)
         → equivFun (S ⋆ f) s ≡ t
       φ r i = r i .fst

       ψ : equivFun (S ⋆ f) s ≡ t
         → equivFun ((add-to-structure S axioms) ⋆ f) (s , a) ≡ (t , b)
       ψ p i = p i , isProp→PathP (λ j → axioms-are-Props Y (p j)) (equivFun (add-to-structure S axioms ⋆ f) (s , a) .snd) b i

       η : section φ ψ
       η p = refl

       ε : retract φ ψ
       ε r i j = r j .fst
               , isProp→isSet-PathP (λ k → axioms-are-Props Y (r k .fst)) _ _
                                    (isProp→PathP (λ j → axioms-are-Props Y (r j .fst))
                                                  (equivFun (add-to-structure S axioms ⋆ f) (s , a) .snd) b)
                                    (λ k → r k .snd) i j

add-axioms-SNS' : (S : Type ℓ → Type ℓ')
                  (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A .fst ≃ B .fst → Type ℓ'')
                  (axioms : (X : Type ℓ) → (S X) → Type ℓ''')
                  (axioms-are-Props : (X : Type ℓ) (s : S X) → isProp (axioms X s))
                  (θ : SNS' S ι)
                → SNS' (add-to-structure S axioms) (add-to-iso S ι axioms)
add-axioms-SNS' S ι axioms axioms-are-Props θ (X , (s , a)) (Y , (t , b)) f =
               equivFun (add-to-structure S axioms ⋆ f) (s , a) ≡ (t , b) ≃⟨ add-⋆-lemma S axioms axioms-are-Props f ⟩
               equivFun (S ⋆ f) s ≡ t                                     ≃⟨ θ (X , s) (Y , t) f ⟩
               add-to-iso S ι axioms (X , (s , a)) (Y , (t , b)) f ■

-- Now, we want to join two structures. Together with the adding of
-- axioms this will allow us to prove that a lot of mathematical
-- structures are a standard notion of structure
technical-×-lemma : {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} {D : Type ℓ₄}
                  → A ≃ C → B ≃ D → A × B ≃ C × D
technical-×-lemma {A = A} {B = B} {C = C} {D = D} f g = isoToEquiv (iso φ ψ η ε)
 where
  φ : (A × B) → (C × D)
  φ (a , b) = equivFun f a , equivFun g b

  ψ : (C × D) → (A × B)
  ψ (c , d) = equivFun (invEquiv f) c , equivFun (invEquiv g) d

  η : section φ ψ
  η (c , d) i = retEq f c i , retEq g d i

  ε : retract φ ψ
  ε (a , b) i = secEq f a i , secEq g b i

join-structure : (S₁ : Type ℓ₁ → Type ℓ₂) (S₂ : Type ℓ₁ → Type ℓ₄)
                → Type ℓ₁ → Type (ℓ-max ℓ₂ ℓ₄)
join-structure S₁ S₂ X = S₁ X × S₂ X

join-iso : {S₁ : Type ℓ₁ → Type ℓ₂}
           (ι₁ : (A B : Σ[ X ∈ (Type ℓ₁) ] (S₁ X)) → A .fst ≃ B .fst → Type ℓ₃)
           {S₂ : Type ℓ₁ → Type ℓ₄}
           (ι₂ : (A B : Σ[ X ∈ (Type ℓ₁) ] (S₂ X)) → A .fst ≃ B .fst → Type ℓ₅)
           (A B : Σ[ X ∈ (Type ℓ₁) ] (join-structure S₁ S₂ X))
         → A .fst ≃ B .fst
         → Type (ℓ-max ℓ₃ ℓ₅)
join-iso ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) f = (ι₁ (X , s₁) (Y , t₁) f) × (ι₂ (X , s₂) (Y , t₂) f)

join-⋆-lemma : (S₁ : Type ℓ₁ → Type ℓ₂) (S₂ : Type ℓ₁ → Type ℓ₄)
               {X Y : Type ℓ₁} {s₁ : S₁ X} {s₂ : S₂ X} {t₁ : S₁ Y} {t₂ : S₂ Y} (f : X ≃ Y)
             → (equivFun (join-structure S₁ S₂ ⋆ f) (s₁ , s₂) ≡ (t₁ , t₂)) ≃
               (equivFun (S₁ ⋆ f) s₁ ≡ t₁) × (equivFun (S₂ ⋆ f) s₂ ≡ t₂)
join-⋆-lemma S₁ S₂ {Y = Y} {s₁ = s₁} {s₂ = s₂} {t₁ = t₁} {t₂ = t₂} f = isoToEquiv (iso φ ψ η ε)
   where
    φ : equivFun (join-structure S₁ S₂ ⋆ f) (s₁ , s₂) ≡ (t₁ , t₂)
      → (equivFun (S₁ ⋆ f) s₁ ≡ t₁) × (equivFun (S₂ ⋆ f) s₂ ≡ t₂)
    φ p = (λ i → p i .fst) , (λ i → p i .snd)

    ψ : (equivFun (S₁ ⋆ f) s₁ ≡ t₁) × (equivFun (S₂ ⋆ f) s₂ ≡ t₂)
      → equivFun (join-structure S₁ S₂ ⋆ f) (s₁ , s₂) ≡ (t₁ , t₂)
    ψ (p , q) i = (p i) , (q i)

    η : section φ ψ
    η (p , q) = refl

    ε : retract φ ψ
    ε p = refl

join-SNS' : (S₁ : Type ℓ₁ → Type ℓ₂)
            (ι₁ : (A B : Σ[ X ∈ (Type ℓ₁) ] (S₁ X)) → A .fst ≃ B .fst → Type ℓ₃)
            (θ₁ : SNS' S₁ ι₁)
            (S₂ : Type ℓ₁ → Type ℓ₄)
            (ι₂ : (A B : Σ[ X ∈ (Type ℓ₁) ] (S₂ X)) → A .fst ≃ B .fst → Type ℓ₅)
            (θ₂ : SNS' S₂ ι₂)
          → SNS' (join-structure S₁ S₂) (join-iso ι₁ ι₂)
join-SNS' S₁ ι₁ θ₁ S₂ ι₂ θ₂ (X , s₁ , s₂) (Y , t₁ , t₂) f =
    equivFun (join-structure S₁ S₂ ⋆ f) (s₁ , s₂) ≡ (t₁ , t₂)
  ≃⟨ join-⋆-lemma S₁ S₂ f ⟩
    (equivFun (S₁ ⋆ f) s₁ ≡ t₁) × (equivFun (S₂ ⋆ f) s₂ ≡ t₂)
  ≃⟨ technical-×-lemma (θ₁ (X , s₁) (Y , t₁) f) (θ₂ (X , s₂) (Y , t₂) f)  ⟩
    join-iso ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) f ■

-- Now, we want to do Monoids as an example. We begin by showing SNS' for simple structures, i.e. pointed types and ∞-magmas.
-- Pointed types with SNS'
pointed-structure : Type ℓ → Type ℓ
pointed-structure X = X

Pointed-Type : Type (ℓ-suc ℓ)
Pointed-Type {ℓ = ℓ} = Σ (Type ℓ) pointed-structure

pointed-iso : (A B : Pointed-Type) → A .fst ≃ B .fst → Type ℓ
pointed-iso A B f = equivFun f (A .snd) ≡ B .snd

pointed-is-SNS' : SNS' {ℓ = ℓ} pointed-structure pointed-iso
pointed-is-SNS' A B f = transportEquiv (λ i → transportRefl (equivFun f (A .snd)) i ≡ B .snd)

-- ∞-Magmas with SNS'
-- We need function extensionality for binary functions.
-- TODO: upstream
funExtBin : {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''} {f g : (x : A) → (y : B x) → C x y}
           → ((x : A) (y : B x) → f x y ≡ g x y) → f ≡ g
funExtBin p i x y = p x y i
module _ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''} {f g : (x : A) → (y : B x) → C x y} where
  private
    appl : f ≡ g → ∀ x y → f x y ≡ g x y
    appl eq x y i = eq i x y

    fib : (p : f ≡ g) → fiber funExtBin p
    fib p = (appl p , refl)

    funExtBin-fiber-isContr
      : (p : f ≡ g)
      → (fi : fiber funExtBin p)
      → fib p ≡ fi
    funExtBin-fiber-isContr p (h , eq) i = (appl (eq (~ i)) , λ j → eq (~ i ∨ j))

  funExtBin-isEquiv : isEquiv funExtBin
  equiv-proof funExtBin-isEquiv p = (fib p , funExtBin-fiber-isContr p)

  funExtBinEquiv : (∀ x y → f x y ≡ g x y) ≃ (f ≡ g)
  funExtBinEquiv = (funExtBin , funExtBin-isEquiv)

-- ∞-Magmas
∞-magma-structure : Type ℓ → Type ℓ
∞-magma-structure X = X → X → X

∞-Magma : Type (ℓ-suc ℓ)
∞-Magma {ℓ = ℓ} = Σ (Type ℓ) ∞-magma-structure

∞-magma-iso : (A B : ∞-Magma) → A .fst ≃ B .fst → Type ℓ
∞-magma-iso (X , _·_) (Y , _∗_) f = (x x' : X) → equivFun f (x · x') ≡ (equivFun f x) ∗ (equivFun f x')

∞-magma-is-SNS' : SNS' {ℓ = ℓ} ∞-magma-structure ∞-magma-iso
∞-magma-is-SNS' (X , _·_) (Y , _∗_) f = SNS→SNS' ∞-magma-structure ∞-magma-iso C (X , _·_) (Y , _∗_) f
 where
  C : {X : Type ℓ} (_·_ _∗_ : X → X → X) → (_·_ ≡ _∗_) ≃ ((x x' : X) → (x · x') ≡ (x ∗ x'))
  C _·_ _∗_ = invEquiv funExtBinEquiv

-- Now we're getting serious: Monoids
raw-monoid-structure : Type ℓ → Type ℓ
raw-monoid-structure X = X × (X → X → X)

raw-monoid-iso : (M N : Σ (Type ℓ) raw-monoid-structure) → (M .fst) ≃ (N .fst) → Type ℓ
raw-monoid-iso (M , e , _·_) (N , d , _∗_) f = (equivFun f e ≡ d)
                        × ((x y : M) → equivFun f (x · y) ≡ (equivFun f x) ∗ (equivFun f y))

-- If we ignore the axioms we get something like a "raw" monoid, which essentially is the join of a pointed type and an ∞-magma
raw-monoid-is-SNS' : SNS' {ℓ = ℓ} raw-monoid-structure raw-monoid-iso
raw-monoid-is-SNS' = join-SNS' pointed-structure pointed-iso pointed-is-SNS'
                               ∞-magma-structure ∞-magma-iso ∞-magma-is-SNS'

-- Now define monoids
monoid-axioms : (X : Type ℓ) → raw-monoid-structure X → Type ℓ
monoid-axioms X (e , _·_ ) = isSet X
                           × ((x y z : X) → (x · (y · z)) ≡ ((x · y) · z))
                           × ((x : X) → (x · e) ≡ x)
                           × ((x : X) → (e · x) ≡ x)

monoid-structure : Type ℓ → Type ℓ
monoid-structure = add-to-structure (raw-monoid-structure) monoid-axioms

-- TODO: it might be nicer to formulate the SIP lemmas so that they're
-- easier to use for things that are not "completely packaged"
Monoids : Type (ℓ-suc ℓ)
Monoids = Σ (Type _) monoid-structure

monoid-iso : (M N : Monoids) → M .fst ≃ N .fst → Type ℓ
monoid-iso = add-to-iso raw-monoid-structure raw-monoid-iso monoid-axioms

-- We have to show that the monoid axioms are indeed Propositions
monoid-axioms-are-Props : (X : Type ℓ) (s : raw-monoid-structure X) → isProp (monoid-axioms X s)
monoid-axioms-are-Props X (e , _·_) s = β s
   where
   α = s .fst
   β =      isOfHLevelΣ 1 isPropIsSet
      λ _ → isOfHLevelΣ 1 (hLevelPi 1 (λ x → hLevelPi 1 λ y → hLevelPi 1 λ z → α (x · (y · z)) ((x · y) · z)))
      λ _ → isOfHLevelΣ 1 (hLevelPi 1 λ x → α (x · e) x)
      λ _ →                hLevelPi 1 λ x → α (e · x) x

monoid-is-SNS' : SNS' {ℓ = ℓ} monoid-structure monoid-iso
monoid-is-SNS' = add-axioms-SNS' raw-monoid-structure raw-monoid-iso
                                 monoid-axioms monoid-axioms-are-Props raw-monoid-is-SNS'

MonoidPath : (M N : Monoids {ℓ}) → (M ≃[ monoid-iso ] N) ≃ (M ≡ N)
MonoidPath M N = SIP monoid-structure monoid-iso (SNS''→SNS''' monoid-is-SNS') M N

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module WrongHidingInApplication where

id : (A : Set) -> A -> A
id A x = x

foo : (A : Set) -> A -> A
foo A x = id {A} x

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module GTFL where

open import Data.Nat hiding (_⊓_; erase; _≟_; _≤_)
open import Data.Bool hiding (_≟_)
open import Data.Fin using (Fin; zero; suc; toℕ)
open import Data.Vec
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty
open import Function using (_∘_)

-- | Types
infixr 30 _⇒_
data GType : Set where
    nat  : GType
    bool : GType
    _⇒_  : GType → GType → GType
    ✭    : GType
    err  : GType    -- easier to model this as a type in Agda

-- | Untyped Expressions
data Expr : Set where
    litNat      : ℕ → Expr
    litBool     : Bool → Expr
    dyn         : Expr
    err         : Expr
    var         : ℕ → Expr
    lam         : GType → Expr → Expr
    _∙_         : Expr → Expr → Expr
    _⊕_         : Expr → Expr → Expr
    if_thn_els_ : Expr → Expr → Expr → Expr

Ctx : ℕ → Set
Ctx = Vec GType

infixr 10 _~_
data _~_ {A B : Set} (x : A) (y : B) : Set where
    cons : x ~ y

~dom : ∀ (t : GType) → GType
~dom (t ⇒ t₁) = t₁
~dom _ = err

~cod : ∀ (t : GType) → GType
~cod (t ⇒ t₁) = t₁
~cod _ = err

_⊓_ : ∀ (t₁ t₂ : GType) → GType
nat ⊓ nat = nat
bool ⊓ bool = bool
t₁ ⊓ ✭ = t₁
✭ ⊓ t₂ = t₂
(t₁ ⇒ t₂) ⊓ (t₃ ⇒ t₄) = (t₁ ⊓ t₃) ⇒ (t₂ ⊓ t₄)
_ ⊓ _ = err

-- | Typed Terms
data Term {n} (Γ : Ctx n) : GType → Set where
    Tx   : ∀ {t} (v : Fin n) → t ≡ lookup v Γ → Term Γ t
    Tn   : ℕ → Term Γ nat
    Tb   : Bool → Term Γ bool
    Tdy  : Term Γ ✭
    _T∙_ : ∀ {t₁ t₂} → Term Γ t₁ → Term Γ t₂ → t₂ ~ (~dom t₁) → Term Γ (~cod t₁)
    _T⊕_ : ∀ {t₁ t₂} → Term Γ t₁ → Term Γ t₂ → (t₁ ~ nat) → (t₂ ~ nat) → Term Γ (t₁ ⊓ t₂)
    Tif  : ∀ {t₁ t₂ t₃} → Term Γ t₁ → Term Γ t₂ → Term Γ t₃ → (t₁ ~ bool) → Term Γ (t₂ ⊓ t₃)
    Tlam : ∀ t₁ {t₂} → Term (t₁ ∷ Γ) t₂ → Term Γ (t₁ ⇒ t₂)

erase : ∀ {n} {Γ : Ctx n} {t} → Term Γ t → Expr
erase (Tx v x) = var (toℕ v)
erase (Tn x) = litNat x
erase (Tb x) = litBool x
erase Tdy    = dyn
erase ((term T∙ term₁) _) = (erase term) ∙ (erase term₁)
erase ((term T⊕ term₁) _ _) = (erase term) ⊕ (erase term₁)
erase (Tif b tt ff  _) = if erase b thn erase tt els erase ff
erase (Tlam t₁ term) = lam t₁ (erase term)

data Fromℕ (n : ℕ) : ℕ → Set where
    yes : (m : Fin n) → Fromℕ n (toℕ m)
    no  : (m : ℕ) → Fromℕ n (n + m)

fromℕ : ∀ n m → Fromℕ n m
fromℕ zero m = no m
fromℕ (suc n) zero = yes zero
fromℕ (suc n) (suc m) with fromℕ n m
fromℕ (suc n) (suc .(toℕ m)) | yes m = yes (suc m)
fromℕ (suc n) (suc .(n + m)) | no m = no m

data Check {n} (Γ : Ctx n) : Expr → Set where
    yes : (τ : GType) (t : Term Γ τ) → Check Γ (erase t)
    no  : {e : Expr} → Check Γ e

staticCheck : ∀ {n} (Γ : Ctx n) (t : Expr) → Check Γ t
-- | primitives
staticCheck Γ (litNat x)  = yes nat (Tn x)
staticCheck Γ (litBool x) = yes bool (Tb x)
staticCheck {n} Γ dyn     = yes ✭ Tdy
staticCheck Γ err         = no

-- | var lookup
staticCheck {n} Γ (var v) with fromℕ n v
staticCheck {n} Γ (var .(toℕ m)) | yes m = yes (lookup m Γ) (Tx m refl)
staticCheck {n} Γ (var .(n + m)) | no m  = no

-- | lambda abstraction
staticCheck Γ (lam x t) with staticCheck (x ∷ Γ) t
staticCheck Γ (lam x .(erase t)) | yes τ t = yes (x ⇒ τ) (Tlam x t) -- double check this
staticCheck Γ (lam x t)          | no      = no

-- | application
staticCheck Γ (t₁ ∙ t₂) with staticCheck Γ t₁ | staticCheck Γ t₂
staticCheck Γ (.(erase t₁) ∙ .(erase t)) | yes (τ₁ ⇒ τ₂) t₁ | (yes τ t) = yes τ₂ ((t₁ T∙ t) cons)
staticCheck Γ (.(erase t₁) ∙ .(erase t)) | yes _ t₁         | (yes τ t) = no -- not sure about this
staticCheck Γ (t₁ ∙ t₂)                  | _                | _         = no

-- | addition
staticCheck Γ (t₁ ⊕ t₂) with staticCheck Γ t₁ | staticCheck Γ t₂
staticCheck Γ (.(erase t₁) ⊕ .(erase t)) | yes nat t₁ | (yes nat t) = yes nat ((t₁ T⊕ t) cons cons)
staticCheck Γ (.(erase t₁) ⊕ .(erase t)) | yes ✭ t₁ | (yes nat t) = yes (✭ ⊓ nat) ((t₁ T⊕ t) cons cons)
staticCheck Γ (.(erase t₁) ⊕ .(erase t)) | yes nat t₁ | (yes ✭ t) = yes (nat ⊓ ✭) ((t₁ T⊕ t) cons cons)
staticCheck Γ (.(erase t₁) ⊕ .(erase t)) | yes ✭ t₁ | (yes ✭ t) = yes ✭ ((t₁ T⊕ t) cons cons)
staticCheck Γ (t₁ ⊕ t₂)                  | _ | _ = no

-- | if ... then ... else
staticCheck Γ (if t thn t₁ els t₂) with staticCheck Γ t
staticCheck Γ (if .(erase t) thn t₁ els t₂) | yes bool t with staticCheck Γ t₁ | staticCheck Γ t₂
staticCheck Γ (if .(erase t₂) thn .(erase t₁) els .(erase t)) | yes bool t₂ | (yes τ₁ t₁) | (yes τ₂ t) = yes (τ₁ ⊓ τ₂) (Tif t₂ t₁ t cons)
staticCheck Γ (if .(erase t₁) thn .(erase t) els t₂) | yes bool t₁ | (yes τ t) | no = no
staticCheck Γ (if .(erase t₂) thn t₁ els .(erase t)) | yes bool t₂ | no | (yes τ t) = no
staticCheck Γ (if .(erase t) thn t₁ els t₂) | yes bool t | no | _ = no

staticCheck Γ (if .(erase t) thn t₁ els t₂) | yes ✭ t with staticCheck Γ t₁ | staticCheck Γ t₂
staticCheck Γ (if .(erase t₂) thn .(erase t₁) els .(erase t)) | yes ✭ t₂ | (yes τ₁ t₁) | (yes τ₂ t) = yes (τ₁ ⊓ τ₂) (Tif t₂ t₁ t cons)
staticCheck Γ (if .(erase t₁) thn .(erase t) els t₂)          | yes ✭ t₁ | (yes τ t) | no = no
staticCheck Γ (if .(erase t₂) thn t₁ els .(erase t))          | yes ✭ t₂ | no | (yes τ t) = no
staticCheck Γ (if .(erase t) thn t₁ els t₂)                   | yes ✭ t | no | no = no

staticCheck Γ (if .(erase t) thn t₁ els t₂) | yes _ t = no
staticCheck Γ (if t thn t₁ els t₂) | no               = no

extractType : ∀ {n} {Γ : Ctx n} {t : Expr} → Check Γ t → GType
extractType (yes τ t) = τ
extractType no = err

-- Type Precision
data _⊑_ : GType → GType → Set where
    n⊑✭ : nat ⊑ ✭
    b⊑✭ : bool ⊑ ✭
    ⇒⊑ : ∀ (t₁ t₂ : GType) → (t₁ ⇒ t₂) ⊑ ✭
    n⊑n : nat ⊑ nat
    b⊑b : bool ⊑ bool
    ✭⊑✭ : ✭ ⊑ ✭
    app⊑ : ∀ (t₁ t₂ t₃ t₄ : GType) → t₁ ⊑ t₃ → t₂ ⊑ t₄ → (t₁ ⇒ t₃) ⊑ (t₃ ⇒ t₄)

-- Term Precision
data _≤_ : Expr → Expr → Set where
    n≤n : ∀ {n} → litNat n ≤ litNat n
    b≤b : ∀ {b} → litBool b ≤ litBool b
    n≤✭ : ∀ {n} → litNat n ≤ dyn
    b≤✭ : ∀ {b} → litBool b ≤ dyn
    d≤d : dyn ≤ dyn

ssG : ∀ {n} {Γ : Ctx n} {e₁ e₂ : Expr} → e₁ ≤ e₂ → extractType (staticCheck Γ e₁) ⊑ extractType (staticCheck Γ e₂)
ssG n≤n = n⊑n
ssG b≤b = b⊑b
ssG n≤✭ = n⊑✭
ssG b≤✭ = b⊑✭
ssG d≤d = ✭⊑✭

max_stars_repo_name: kellino/TypeSystems

max_issues_repo_name: kellino/TypeSystems

max_forks_repo_name: kellino/TypeSystems


text:
------------------------------------------------------------------------------
-- Arithmetic properties
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Data.Nat
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.TotalityI

------------------------------------------------------------------------------
-- Congruence properties

+-leftCong : ∀ {m n o} → m ≡ n → m + o ≡ n + o
+-leftCong refl = refl

+-rightCong : ∀ {m n o} → n ≡ o → m + n ≡ m + o
+-rightCong refl = refl

∸-leftCong : ∀ {m n o} → m ≡ n → m ∸ o ≡ n ∸ o
∸-leftCong refl = refl

∸-rightCong : ∀ {m n o} → n ≡ o → m ∸ n ≡ m ∸ o
∸-rightCong refl = refl

*-leftCong : ∀ {m n o} → m ≡ n → m * o ≡ n * o
*-leftCong refl = refl

*-rightCong : ∀ {m n o} → n ≡ o → m * n ≡ m * o
*-rightCong refl = refl

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

Sx≢x : ∀ {n} → N n → succ₁ n ≢ n
Sx≢x nzero h      = ⊥-elim (0≢S (sym h))
Sx≢x (nsucc Nn) h = ⊥-elim (Sx≢x Nn (succInjective h))

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity = +-0x

+-rightIdentity : ∀ {n} → N n → n + zero ≡ n
+-rightIdentity nzero          = +-leftIdentity zero
+-rightIdentity (nsucc {n} Nn) =
  trans (+-Sx n zero) (succCong (+-rightIdentity Nn))

pred-N : ∀ {n} → N n → N (pred₁ n)
pred-N nzero          = subst N (sym pred-0) nzero
pred-N (nsucc {n} Nn) = subst N (sym (pred-S n)) Nn

+-N : ∀ {m n} → N m → N n → N (m + n)
+-N {n = n} nzero          Nn = subst N (sym (+-leftIdentity n)) Nn
+-N {n = n} (nsucc {m} Nm) Nn = subst N (sym (+-Sx m n)) (nsucc (+-N Nm Nn))

∸-N : ∀ {m n} → N m → N n → N (m ∸ n)
∸-N {m} Nm nzero          = subst N (sym (∸-x0 m)) Nm
∸-N {m} Nm (nsucc {n} Nn) = subst N (sym (∸-xS m n)) (pred-N (∸-N Nm Nn))

+-assoc : ∀ {m} → N m → ∀ n o → m + n + o ≡ m + (n + o)
+-assoc nzero n o =
  zero + n + o   ≡⟨ +-leftCong (+-leftIdentity n) ⟩
  n + o          ≡⟨ sym (+-leftIdentity (n + o)) ⟩
  zero + (n + o) ∎

+-assoc (nsucc {m} Nm) n o =
  succ₁ m + n + o     ≡⟨ +-leftCong (+-Sx m n) ⟩
  succ₁ (m + n) + o   ≡⟨ +-Sx (m + n) o ⟩
  succ₁ (m + n + o)   ≡⟨ succCong (+-assoc Nm n o) ⟩
  succ₁ (m + (n + o)) ≡⟨ sym (+-Sx m (n + o)) ⟩
  succ₁ m + (n + o)   ∎

x+Sy≡S[x+y] : ∀ {m} → N m → ∀ n → m + succ₁ n ≡ succ₁ (m + n)
x+Sy≡S[x+y] nzero n =
  zero + succ₁ n   ≡⟨ +-leftIdentity (succ₁ n) ⟩
  succ₁ n          ≡⟨ succCong (sym (+-leftIdentity n)) ⟩
  succ₁ (zero + n) ∎

x+Sy≡S[x+y] (nsucc {m} Nm) n =
  succ₁ m + succ₁ n     ≡⟨ +-Sx m (succ₁ n) ⟩
  succ₁ (m + succ₁ n)   ≡⟨ succCong (x+Sy≡S[x+y] Nm n) ⟩
  succ₁ (succ₁ (m + n)) ≡⟨ succCong (sym (+-Sx m n)) ⟩
  succ₁ (succ₁ m + n)   ∎

+-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
+-comm {n = n} nzero Nn =
  zero + n ≡⟨ +-leftIdentity n ⟩
  n        ≡⟨ sym (+-rightIdentity Nn) ⟩
  n + zero ∎

+-comm {n = n} (nsucc {m} Nm) Nn =
  succ₁ m + n   ≡⟨ +-Sx m n ⟩
  succ₁ (m + n) ≡⟨ succCong (+-comm Nm Nn) ⟩
  succ₁ (n + m) ≡⟨ sym (x+Sy≡S[x+y] Nn m) ⟩
  n + succ₁ m   ∎

0∸x : ∀ {n} → N n → zero ∸ n ≡ zero
0∸x nzero          = ∸-x0 zero
0∸x (nsucc {n} Nn) =
  zero ∸ succ₁ n   ≡⟨ ∸-xS zero n ⟩
  pred₁ (zero ∸ n) ≡⟨ predCong (0∸x Nn) ⟩
  pred₁ zero       ≡⟨ pred-0 ⟩
  zero             ∎

S∸S : ∀ {m n} → N m → N n → succ₁ m ∸ succ₁ n ≡ m ∸ n
S∸S {m} _ nzero =
  succ₁ m ∸ succ₁ zero   ≡⟨ ∸-xS (succ₁ m) zero ⟩
  pred₁ (succ₁ m ∸ zero) ≡⟨ predCong (∸-x0 (succ₁ m)) ⟩
  pred₁ (succ₁ m)        ≡⟨ pred-S m ⟩
  m                      ≡⟨ sym (∸-x0 m) ⟩
  m ∸ zero               ∎

S∸S {m} Nm (nsucc {n} Nn) =
  succ₁ m ∸ succ₁ (succ₁ n) ≡⟨ ∸-xS (succ₁ m) (succ₁ n) ⟩
  pred₁ (succ₁ m ∸ succ₁ n) ≡⟨ predCong (S∸S Nm Nn) ⟩
  pred₁ (m ∸ n)             ≡⟨ sym (∸-xS m n) ⟩
  m ∸ succ₁ n               ∎

x∸x≡0 : ∀ {n} → N n → n ∸ n ≡ zero
x∸x≡0 nzero      = ∸-x0 zero
x∸x≡0 (nsucc Nn) = trans (S∸S Nn Nn) (x∸x≡0 Nn)

Sx∸x≡1 : ∀ {n} → N n → succ₁ n ∸ n ≡ 1'
Sx∸x≡1 nzero      = ∸-x0 1'
Sx∸x≡1 (nsucc Nn) = trans (S∸S (nsucc Nn) Nn) (Sx∸x≡1 Nn)

[x+Sy]∸y≡Sx : ∀ {m n} → N m → N n → m + succ₁ n ∸ n ≡ succ₁ m
[x+Sy]∸y≡Sx {n = n} nzero Nn =
  zero + succ₁ n ∸ n ≡⟨ ∸-leftCong (+-leftIdentity (succ₁ n)) ⟩
  succ₁ n ∸ n        ≡⟨ Sx∸x≡1 Nn ⟩
  1'                 ∎

[x+Sy]∸y≡Sx (nsucc {m} Nm) nzero =
  succ₁ m + 1' ∸ zero      ≡⟨ ∸-leftCong (+-Sx m 1') ⟩
  succ₁ (m + 1') ∸ zero    ≡⟨ ∸-x0 (succ₁ (m + 1')) ⟩
  succ₁ (m + 1')           ≡⟨ succCong (+-comm Nm 1-N) ⟩
  succ₁ (1' + m)           ≡⟨ succCong (+-Sx zero m) ⟩
  succ₁ (succ₁ (zero + m)) ≡⟨ succCong (succCong (+-leftIdentity m)) ⟩
  succ₁ (succ₁ m)          ∎

[x+Sy]∸y≡Sx (nsucc {m} Nm) (nsucc {n} Nn) =
  succ₁ m + succ₁ (succ₁ n) ∸ succ₁ n
    ≡⟨ ∸-leftCong (+-Sx m (succ₁ (succ₁ n))) ⟩
  succ₁ (m + succ₁ (succ₁ n)) ∸ succ₁ n
    ≡⟨ S∸S (+-N Nm (nsucc (nsucc Nn))) Nn ⟩
  m + succ₁ (succ₁ n) ∸ n
    ≡⟨ ∸-leftCong (x+Sy≡S[x+y] Nm (succ₁ n)) ⟩
  succ₁ (m + succ₁ n) ∸ n
    ≡⟨ ∸-leftCong (sym (+-Sx m (succ₁ n))) ⟩
  succ₁ m + succ₁ n ∸ n
    ≡⟨ [x+Sy]∸y≡Sx (nsucc Nm) Nn ⟩
  succ₁ (succ₁ m) ∎

[x+y]∸[x+z]≡y∸z : ∀ {m n o} → N m → N n → N o → (m + n) ∸ (m + o) ≡ n ∸ o
[x+y]∸[x+z]≡y∸z {n = n} {o} nzero _ _ =
  (zero + n) ∸ (zero + o) ≡⟨ ∸-leftCong (+-leftIdentity n) ⟩
    n ∸ (zero + o)        ≡⟨ ∸-rightCong (+-leftIdentity o) ⟩
    n ∸ o                 ∎

[x+y]∸[x+z]≡y∸z {n = n} {o} (nsucc {m} Nm) Nn No =
  (succ₁ m + n) ∸ (succ₁ m + o) ≡⟨ ∸-leftCong (+-Sx m n) ⟩
  succ₁ (m + n) ∸ (succ₁ m + o) ≡⟨ ∸-rightCong (+-Sx m o) ⟩
  succ₁ (m + n) ∸ succ₁ (m + o) ≡⟨ S∸S (+-N Nm Nn) (+-N Nm No) ⟩
  (m + n) ∸ (m + o)             ≡⟨ [x+y]∸[x+z]≡y∸z Nm Nn No ⟩
  n ∸ o                         ∎

*-leftZero : ∀ n → zero * n ≡ zero
*-leftZero = *-0x

*-rightZero : ∀ {n} → N n → n * zero ≡ zero
*-rightZero nzero          = *-leftZero zero
*-rightZero (nsucc {n} Nn) =
  trans (*-Sx n zero)
        (trans (+-leftIdentity (n * zero)) (*-rightZero Nn))

*-N : ∀ {m n} → N m → N n → N (m * n)
*-N {n = n} nzero          Nn = subst N (sym (*-leftZero n)) nzero
*-N {n = n} (nsucc {m} Nm) Nn = subst N (sym (*-Sx m n)) (+-N Nn (*-N Nm Nn))

*-leftIdentity : ∀ {n} → N n → 1' * n ≡ n
*-leftIdentity {n} Nn =
  1' * n       ≡⟨ *-Sx zero n ⟩
  n + zero * n ≡⟨ +-rightCong (*-leftZero n) ⟩
  n + zero     ≡⟨ +-rightIdentity Nn ⟩
  n            ∎

x*Sy≡x+xy : ∀ {m n} → N m → N n → m * succ₁ n ≡ m + m * n
x*Sy≡x+xy {n = n} nzero Nn = sym
  (
    zero + zero * n ≡⟨ +-rightCong (*-leftZero n) ⟩
    zero + zero     ≡⟨ +-leftIdentity zero ⟩
    zero            ≡⟨ sym (*-leftZero (succ₁ n)) ⟩
    zero * succ₁ n  ∎
  )

x*Sy≡x+xy {n = n} (nsucc {m} Nm) Nn =
  succ₁ m * succ₁ n
    ≡⟨ *-Sx m (succ₁ n) ⟩
  succ₁ n + m * succ₁ n
    ≡⟨ +-rightCong (x*Sy≡x+xy Nm Nn) ⟩
  succ₁ n + (m + m * n)
    ≡⟨ +-Sx n (m + m * n) ⟩
  succ₁ (n + (m + m * n))
    ≡⟨ succCong (sym (+-assoc Nn m (m * n))) ⟩
  succ₁ (n + m + m * n)
    ≡⟨ succCong (+-leftCong (+-comm Nn Nm)) ⟩
  succ₁ (m + n + m * n)
    ≡⟨ succCong (+-assoc Nm n (m * n)) ⟩
  succ₁ (m + (n + m * n))
    ≡⟨ sym (+-Sx m (n + m * n)) ⟩
  succ₁ m + (n + m * n)
    ≡⟨ +-rightCong (sym (*-Sx m n)) ⟩
  succ₁ m + succ₁ m * n ∎

*-comm : ∀ {m n} → N m → N n → m * n ≡ n * m
*-comm {n = n} nzero Nn          = trans (*-leftZero n) (sym (*-rightZero Nn))
*-comm {n = n} (nsucc {m} Nm) Nn =
  succ₁ m * n ≡⟨ *-Sx m n ⟩
  n + m * n   ≡⟨ +-rightCong (*-comm Nm Nn) ⟩
  n + n * m   ≡⟨ sym (x*Sy≡x+xy Nn Nm) ⟩
  n * succ₁ m ∎

*-rightIdentity : ∀ {n} → N n → n * 1' ≡ n
*-rightIdentity {n} Nn = trans (*-comm Nn (nsucc nzero)) (*-leftIdentity Nn)

*∸-leftDistributive : ∀ {m n o} → N m → N n → N o → (m ∸ n) * o ≡ m * o ∸ n * o
*∸-leftDistributive {m} {o = o} _ nzero _ =
  (m ∸ zero) * o   ≡⟨ *-leftCong (∸-x0 m) ⟩
  m * o            ≡⟨ sym (∸-x0 (m * o)) ⟩
  m * o ∸ zero     ≡⟨ ∸-rightCong (sym (*-leftZero o)) ⟩
  m * o ∸ zero * o ∎

*∸-leftDistributive {o = o} nzero (nsucc {n} Nn) No =
  (zero ∸ succ₁ n) * o   ≡⟨ *-leftCong (0∸x (nsucc Nn)) ⟩
  zero * o               ≡⟨ *-leftZero o ⟩
  zero                   ≡⟨ sym (0∸x (*-N (nsucc Nn) No)) ⟩
  zero ∸ succ₁ n * o     ≡⟨ ∸-leftCong (sym (*-leftZero o)) ⟩
  zero * o ∸ succ₁ n * o ∎

*∸-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) nzero =
  (succ₁ m ∸ succ₁ n) * zero
    ≡⟨ *-comm (∸-N (nsucc Nm) (nsucc Nn)) nzero ⟩
  zero * (succ₁ m ∸ succ₁ n)
    ≡⟨ *-leftZero (succ₁ m ∸ succ₁ n) ⟩
  zero
    ≡⟨ sym (0∸x (*-N (nsucc Nn) nzero)) ⟩
  zero ∸ succ₁ n * zero
    ≡⟨ ∸-leftCong (sym (*-leftZero (succ₁ m))) ⟩
  zero * succ₁ m ∸ succ₁ n * zero
    ≡⟨ ∸-leftCong (*-comm nzero (nsucc Nm)) ⟩
  succ₁ m * zero ∸ succ₁ n * zero ∎

*∸-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) =
  (succ₁ m ∸ succ₁ n) * succ₁ o
    ≡⟨ *-leftCong (S∸S Nm Nn) ⟩
  (m ∸ n) * succ₁ o
     ≡⟨ *∸-leftDistributive Nm Nn (nsucc No) ⟩
  m * succ₁ o ∸ n * succ₁ o
    ≡⟨ sym ([x+y]∸[x+z]≡y∸z (nsucc No) (*-N Nm (nsucc No)) (*-N Nn (nsucc No))) ⟩
  (succ₁ o + m * succ₁ o) ∸ (succ₁ o + n * succ₁ o)
    ≡⟨ ∸-leftCong (sym (*-Sx m (succ₁ o))) ⟩
  (succ₁ m * succ₁ o) ∸ (succ₁ o + n * succ₁ o)
    ≡⟨ ∸-rightCong (sym (*-Sx n (succ₁ o))) ⟩
  (succ₁ m * succ₁ o) ∸ (succ₁ n * succ₁ o) ∎

*+-leftDistributive : ∀ {m n o} → N m → N n → N o → (m + n) * o ≡ m * o + n * o
*+-leftDistributive {m} {n} Nm Nn nzero =
  (m + n) * zero
    ≡⟨ *-comm (+-N Nm Nn) nzero ⟩
  zero * (m + n)
    ≡⟨ *-leftZero (m + n) ⟩
  zero
    ≡⟨ sym (*-leftZero m) ⟩
  zero * m
    ≡⟨ *-comm nzero Nm ⟩
  m * zero
    ≡⟨ sym (+-rightIdentity (*-N Nm nzero)) ⟩
  m * zero + zero
    ≡⟨ +-rightCong (trans (sym (*-leftZero n)) (*-comm nzero Nn)) ⟩
  m * zero + n * zero ∎

*+-leftDistributive {n = n} nzero Nn (nsucc {o} No) =
  (zero + n) * succ₁ o         ≡⟨ *-leftCong (+-leftIdentity n) ⟩
  n * succ₁ o                  ≡⟨ sym (+-leftIdentity (n * succ₁ o)) ⟩
  zero + n * succ₁ o           ≡⟨ +-leftCong (sym (*-leftZero (succ₁ o))) ⟩
  zero * succ₁ o + n * succ₁ o ∎

*+-leftDistributive (nsucc {m} Nm) nzero (nsucc {o} No) =
  (succ₁ m + zero) * succ₁ o
    ≡⟨ *-leftCong (+-rightIdentity (nsucc Nm)) ⟩
  succ₁ m * succ₁ o
    ≡⟨ sym (+-rightIdentity (*-N (nsucc Nm) (nsucc No))) ⟩
  succ₁ m * succ₁ o + zero
    ≡⟨ +-rightCong (sym (*-leftZero (succ₁ o))) ⟩
  succ₁ m * succ₁ o + zero * succ₁ o ∎

*+-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) =
  (succ₁ m + succ₁ n) * succ₁ o
    ≡⟨ *-leftCong (+-Sx m (succ₁ n)) ⟩
  succ₁ (m + succ₁ n) * succ₁ o
    ≡⟨ *-Sx (m + succ₁ n) (succ₁ o) ⟩
  succ₁ o + (m + succ₁ n) * succ₁ o
    ≡⟨ +-rightCong (*+-leftDistributive Nm (nsucc Nn) (nsucc No)) ⟩
  succ₁ o + (m * succ₁ o + succ₁ n * succ₁ o)
    ≡⟨ sym (+-assoc (nsucc No) (m * succ₁ o) (succ₁ n * succ₁ o)) ⟩
  succ₁ o + m * succ₁ o + succ₁ n * succ₁ o
    ≡⟨ +-leftCong (sym (*-Sx m (succ₁ o))) ⟩
  succ₁ m * succ₁ o + succ₁ n * succ₁ o ∎

xy≡0→x≡0∨y≡0 : ∀ {m n} → N m → N n → m * n ≡ zero → m ≡ zero ∨ n ≡ zero
xy≡0→x≡0∨y≡0 nzero          _              _      = inj₁ refl
xy≡0→x≡0∨y≡0 (nsucc Nm)     nzero          _      = inj₂ refl
xy≡0→x≡0∨y≡0 (nsucc {m} Nm) (nsucc {n} Nn) SmSn≡0 = ⊥-elim (0≢S prf)
  where
  prf : zero ≡ succ₁ (n + m * succ₁ n)
  prf = zero                    ≡⟨ sym SmSn≡0 ⟩
        succ₁ m * succ₁ n       ≡⟨ *-Sx m (succ₁ n) ⟩
        succ₁ n + m * succ₁ n   ≡⟨ +-Sx n (m * succ₁ n) ⟩
        succ₁ (n + m * succ₁ n) ∎

xy≡1→x≡1 : ∀ {m n} → N m → N n → m * n ≡ 1' → m ≡ 1'
xy≡1→x≡1 {n = n} nzero Nn h = ⊥-elim (0≢S (trans (sym (*-leftZero n)) h))
xy≡1→x≡1 (nsucc nzero) Nn h = refl
xy≡1→x≡1 (nsucc (nsucc {m} Nm)) nzero h =
  ⊥-elim (0≢S (trans (sym (*-rightZero (nsucc (nsucc Nm)))) h))
xy≡1→x≡1 (nsucc (nsucc {m} Nm)) (nsucc {n} Nn) h = ⊥-elim (0≢S prf₂)
  where
  prf₁ : 1' ≡ succ₁ (succ₁ (m + n * succ₁ (succ₁ m)))
  prf₁ = 1'
           ≡⟨ sym h ⟩
         succ₁ (succ₁ m) * succ₁ n
           ≡⟨ *-comm (nsucc (nsucc Nm)) (nsucc Nn) ⟩
         succ₁ n * succ₁ (succ₁ m)
           ≡⟨ *-Sx n (succ₁ (succ₁ m)) ⟩
         succ₁ (succ₁ m) + n * succ₁ (succ₁ m)
           ≡⟨ +-Sx (succ₁ m) (n * succ₁ (succ₁ m)) ⟩
         succ₁ (succ₁ m + n * succ₁ (succ₁ m))
           ≡⟨ succCong (+-Sx m (n * succ₁ (succ₁ m))) ⟩
         succ₁ (succ₁ (m + n * succ₁ (succ₁ m))) ∎

  prf₂ : zero ≡ succ₁ (m + n * succ₁ (succ₁ m))
  prf₂ = succInjective prf₁

xy≡1→y≡1 : ∀ {m n} → N m → N n → m * n ≡ 1' → n ≡ 1'
xy≡1→y≡1 Nm Nn h = xy≡1→x≡1 Nn Nm (trans (*-comm Nn Nm) h)

-- Feferman's axiom as presented by (Beeson 1986, p. 74).
succOnto : ∀ {n} → N n → n ≢ zero → succ₁ (pred₁ n) ≡ n
succOnto nzero          h = ⊥-elim (h refl)
succOnto (nsucc {n} Nn) h = succCong (pred-S n)

------------------------------------------------------------------------------
-- References
--
-- Beeson, M. J. (1986). Proving Programs and Programming Proofs. In:
-- Logic, Methodology and Philosophy of Science VII (1983). Ed. by
-- Barcan Marcus, Ruth, Dorn, George J. W. and Weingartner,
-- Paul. Vol. 114. Studies in Logic and the Foundations of
-- Mathematics. Elsevier, pp. 51–82.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module datatype-util where
open import constants
open import ctxt
open import syntax-util
open import general-util
open import type-util
open import cedille-types
open import subst
open import rename
open import free-vars

{-# TERMINATING #-}
decompose-arrows : ctxt → type → params × type
decompose-arrows Γ (TpAbs me x atk T) =
  let x' = fresh-var-new Γ x in
  case decompose-arrows (ctxt-var-decl x' Γ) (rename-var Γ x x' T) of λ where
    (ps , T') → Param me x' atk :: ps , T'
decompose-arrows Γ T = [] , T

decompose-ctr-type : ctxt → type → type × params × 𝕃 tmtp
decompose-ctr-type Γ T with decompose-arrows Γ T
...| ps , Tᵣ with decompose-tpapps Tᵣ
...| Tₕ , as = Tₕ , ps , as

{-# TERMINATING #-}
kind-to-indices : ctxt → kind → indices
kind-to-indices Γ (KdAbs x atk k) =
  let x' = fresh-var-new Γ x in
  Index x' atk :: kind-to-indices (ctxt-var-decl x' Γ) (rename-var Γ x x' k)
kind-to-indices Γ _ = []

rename-indices-h : ctxt → renamectxt → indices → 𝕃 tmtp → indices
rename-indices-h Γ ρ (Index x atk :: is) (ty :: tys) =
  Index x' atk' ::
    rename-indices-h (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') is tys
  where
  x' = fresh-var-renamectxt Γ ρ (maybe-else x id (is-var-unqual ty))
  atk' = subst-renamectxt Γ ρ -tk atk
rename-indices-h Γ ρ (Index x atk :: is) [] =
  let x' = fresh-var-renamectxt Γ ρ x in
  Index x' (subst-renamectxt Γ ρ -tk atk) ::
    rename-indices-h (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') is []
rename-indices-h _ _ [] _ = []

rename-indices : ctxt → indices → 𝕃 tmtp → indices
rename-indices Γ = rename-indices-h Γ empty-renamectxt

positivity : Set
positivity = 𝔹 × 𝔹 -- occurs positively × occurs negatively

pattern occurs-nil = ff , ff
pattern occurs-pos = tt , ff
pattern occurs-neg = ff , tt
pattern occurs-all = tt , tt

--positivity-inc : positivity → positivity
--positivity-dec : positivity → positivity
positivity-neg : positivity → positivity
positivity-add : positivity → positivity → positivity

--positivity-inc = map-fst λ _ → tt
--positivity-dec = map-snd λ _ → tt
positivity-neg = uncurry $ flip _,_
positivity-add (+ₘ , -ₘ) (+ₙ , -ₙ) = (+ₘ || +ₙ) , (-ₘ || -ₙ)

data ctorCheckT : Set where
  ctorOk : ctorCheckT
  ctorNotInReturnType : ctorCheckT
  ctorNegative : ctorCheckT

posₒ = fst
negₒ = snd

occurs : positivity → ctorCheckT
occurs p = if (negₒ p) then ctorNegative else ctorOk

or-ctorCheckT : ctorCheckT → ctorCheckT → ctorCheckT
or-ctorCheckT ctorOk r = r
or-ctorCheckT ctorNegative  _ = ctorNegative
or-ctorCheckT ctorNotInReturnType _ = ctorNotInReturnType

posM : Set → Set
posM A = 𝕃 tpkd → A × 𝕃 tpkd

run-posM : ∀{A : Set} → posM A → A × 𝕃 tpkd
run-posM p = p []

extract-pos : ∀{A : Set} → posM A → A
extract-pos = fst ∘ run-posM

instance
  posM-monad : monad posM
  return ⦃ posM-monad ⦄ a = λ l → a , l
  _>>=_ ⦃ posM-monad ⦄ p ap l with p l
  _>>=_ ⦃ posM-monad ⦄ p ap l | a , l' = ap a l'

  posM-functor : functor posM
  fmap ⦃ posM-functor ⦄ g m l with m l
  fmap ⦃ posM-functor ⦄ g m l | a , l' = g a , l'

  posM-applicative : applicative posM
  pure ⦃ posM-applicative ⦄ = return
  _<*>_ ⦃ posM-applicative ⦄ mab ma l with mab l
  _<*>_ ⦃ posM-applicative ⦄ mab ma l | f , l' with ma l'
  _<*>_ ⦃ posM-applicative ⦄ mab ma l | f , l' | a , l'' =
    f a , l''

add-posM : tpkd → posM ⊤
add-posM x = λ l → triv , x :: l

module positivity (x : var) where

  open import conversion

  if-free : ∀ {ed} → ⟦ ed ⟧ → positivity
  if-free t with is-free-in x t
  ...| f = f , f

  if-free-args : args → positivity
  if-free-args as =
    let c = stringset-contains (free-vars-args as) x in c , c

  hnf' : ∀ {ed} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
  hnf' Γ T = hnf Γ unfold-no-defs T

  mtt = maybe-else tt id
  mff = maybe-else ff id

  {-# TERMINATING #-}
  type+ : ctxt → type → posM positivity
  kind+ : ctxt → kind → posM positivity
  tpkd+ : ctxt → tpkd → posM positivity
  tpapp+ : ctxt → type → posM positivity
  type+h : ctxt → type → posM positivity
  kind+h : ctxt → kind → posM positivity
  tpkd+h : ctxt → tpkd → posM positivity
  tpapp+h : ctxt → type → posM positivity

  type+ Γ T = type+h Γ T -- >>= λ p → add-posM (Tkt T) >> return p
  kind+ Γ k = kind+h Γ k
  tpkd+ Γ x = tpkd+h Γ x
  tpapp+ Γ T = tpapp+h Γ T

  type+h Γ (TpAbs me x' atk T) =
    let Γ' = ctxt-var-decl x' Γ in
      pure positivity-add <*>
        (fmap positivity-neg $ tpkd+ Γ $ hnf' Γ -tk atk) <*>
        (type+ Γ' $ hnf' Γ' T)
  type+h Γ (TpIota x' T T') =
    let Γ' = ctxt-var-decl x' Γ in
      pure positivity-add <*>
        (type+ Γ $ hnf' Γ T) <*>
        (type+ Γ' $ hnf' Γ' T')
  type+h Γ (TpApp T tT) = tpapp+ Γ $ hnf' Γ $ TpApp T tT
  type+h Γ (TpEq tₗ tᵣ) = pure occurs-nil
  type+h Γ (TpHole _) = pure occurs-nil
  type+h Γ (TpLam x' atk T)=
    let Γ' = ctxt-var-decl x' Γ in
      pure positivity-add <*>
        (fmap positivity-neg $ tpkd+ Γ $ hnf' Γ -tk atk) <*>
        (type+ Γ' (hnf' Γ' T))
  type+h Γ (TpVar x') = pure $ x =string x' , ff

  kind+h Γ (KdAbs x' atk k) =
    let Γ' = ctxt-var-decl x' Γ in
      pure positivity-add <*>
      (fmap positivity-neg $ tpkd+ Γ $ hnf' Γ -tk atk) <*>
      (kind+ Γ' k)
  kind+h Γ _ = pure occurs-nil

  tpkd+h Γ (Tkt T) = type+ Γ (hnf' Γ T)
  tpkd+h Γ (Tkk k) = kind+ Γ k

  tpapp+h Γ T with decompose-tpapps T
  tpapp+h Γ T | TpVar x' , as =
    let f = if-free-args (tmtps-to-args NotErased as) in
    if x =string x'
      then pure (positivity-add occurs-pos f)
      else maybe-else' (data-lookup Γ x' as) (pure f)
        λ {(mk-data-info x'' xₒ'' asₚ asᵢ ps kᵢ k cs csₚₛ eds gds) →
          let s = (inst-type Γ ps asₚ (hnf' Γ $ TpAbs tt x'' (Tkk k) $ foldr (uncurry λ cₓ cₜ → TpAbs ff ignored-var (Tkt cₜ)) (TpVar x'') cs)) in
          add-posM (Tkt s) >>
          type+ Γ s }
  tpapp+h Γ T | _ , _ = pure $ if-free T

  {-# TERMINATING #-}
  arrs+ : ctxt → type → posM ctorCheckT

  arrs+ Γ (TpAbs me x' atk T) =
    let Γ' = ctxt-var-decl x' Γ in
     pure or-ctorCheckT <*>
       (fmap occurs (tpkd+ Γ $ hnf' Γ -tk atk)) <*>
       (arrs+ Γ' (hnf' Γ' T))
  arrs+ Γ (TpApp T tT) = fmap occurs (tpapp+ Γ $ hnf' Γ (TpApp T tT))
  arrs+ Γ (TpLam x' atk T) =
    let Γ' = ctxt-var-decl x' Γ in
      pure or-ctorCheckT <*>
        (fmap occurs (tpkd+ Γ $ hnf' Γ -tk atk)) <*>
        (arrs+ Γ' (hnf' Γ' T))
  arrs+ Γ (TpVar x') = return $ if (x =string x') then ctorOk else ctorNotInReturnType

  arrs+ _ _ = return ctorNegative

  ctr-positive : ctxt → type → posM ctorCheckT
  ctr-positive Γ = (arrs+ Γ ∘ hnf' Γ)

-- build the evidence for a sigma-term, given datatype X with associated info μ
sigma-build-evidence : var → datatype-info → term
sigma-build-evidence X μ =
  if datatype-info.name μ =string X then recompose-apps (datatype-info.asₚ μ) (Var (data-is/ X)) else Var (mu-isType/' X)


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Ring.DirectProd where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Algebra.Ring.Base

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

module _
  (A'@(A , Ar) : Ring ℓ)
  (B'@(B , Br) : Ring ℓ')
  where

  open RingStr Ar using ()
    renaming
    ( 0r        to 0A
    ; 1r        to 1A
    ; _+_       to _+A_
    ; -_        to -A_
    ; _·_       to _·A_
    ; +Assoc    to +AAssoc
    ; +IdR      to +AIdR
    ; +IdL      to +AIdL
    ; +InvR     to +AInvR
    ; +InvL     to +AInvL
    ; +Comm     to +AComm
    ; ·Assoc    to ·AAssoc
    ; ·IdL      to ·AIdL
    ; ·IdR      to ·AIdR
    ; ·DistR+   to ·ADistR+
    ; ·DistL+   to ·ADistL+
    ; is-set    to isSetA     )

  open RingStr Br using ()
    renaming
    ( 0r        to 0B
    ; 1r        to 1B
    ; _+_       to _+B_
    ; -_        to -B_
    ; _·_       to _·B_
    ; +Assoc    to +BAssoc
    ; +IdR      to +BIdR
    ; +IdL      to +BIdL
    ; +InvR     to +BInvR
    ; +InvL     to +BInvL
    ; +Comm     to +BComm
    ; ·Assoc    to ·BAssoc
    ; ·IdL      to ·BIdL
    ; ·IdR      to ·BIdR
    ; ·DistR+   to ·BDistR+
    ; ·DistL+   to ·BDistL+
    ; is-set    to isSetB     )

  DirectProd-Ring : Ring (ℓ-max ℓ ℓ')
  fst DirectProd-Ring = A × B
  RingStr.0r (snd DirectProd-Ring) = 0A , 0B
  RingStr.1r (snd DirectProd-Ring) = 1A , 1B
  (snd DirectProd-Ring RingStr.+ (a , b)) (a' , b') = (a +A a') , (b +B b')
  (snd DirectProd-Ring RingStr.· (a , b)) (a' , b') = (a ·A a') , (b ·B b')
  (RingStr.- snd DirectProd-Ring) (a , b) = (-A a) , (-B b)
  RingStr.isRing (snd DirectProd-Ring) =
    makeIsRing (isSet× isSetA isSetB)
    (λ x y z i → +AAssoc (fst x) (fst y) (fst z) i , +BAssoc (snd x) (snd y) (snd z) i)
    (λ x i → (+AIdR (fst x) i) , (+BIdR (snd x) i))
    (λ x i → (+AInvR (fst x) i) , +BInvR (snd x) i)
    (λ x y i → (+AComm (fst x) (fst y) i) , (+BComm (snd x) (snd y) i))
    (λ x y z i → (·AAssoc (fst x) (fst y) (fst z) i) , (·BAssoc (snd x) (snd y) (snd z) i))
    (λ x i → (·AIdR (fst x) i) , (·BIdR (snd x) i))
    (λ x i → (·AIdL (fst x) i) , (·BIdL (snd x) i))
    (λ x y z i → (·ADistR+ (fst x) (fst y) (fst z) i) , (·BDistR+ (snd x) (snd y) (snd z) i))
    (λ x y z i → (·ADistL+ (fst x) (fst y) (fst z) i) , (·BDistL+ (snd x) (snd y) (snd z) i))

module Coproduct-Equiv
  {Xr@(X , Xstr) : Ring ℓ}
  {Yr@(Y , Ystr) : Ring ℓ'}
  {X'r@(X' , X'str) : Ring ℓ''}
  {Y'r@(Y' , Y'str) : Ring ℓ'''}
  where

  open Iso
  open IsRingHom
  open RingStr

  _+X×X'_ : X × X' → X × X' → X × X'
  _+X×X'_ = _+_ (snd (DirectProd-Ring Xr X'r))

  _+Y×Y'_ : Y × Y' → Y × Y' → Y × Y'
  _+Y×Y'_ = _+_ (snd (DirectProd-Ring Yr Y'r))

  _·X×X'_ : X × X' → X × X' → X × X'
  _·X×X'_ = _·_ (snd (DirectProd-Ring Xr X'r))

  _·Y×Y'_ : Y × Y' → Y × Y' → Y × Y'
  _·Y×Y'_ = _·_ (snd (DirectProd-Ring Yr Y'r))

  re×re' : (re : RingEquiv Xr Yr) → (re' : RingEquiv X'r Y'r) → (X × X') ≃ (Y × Y')
  re×re' re re' = ≃-× (fst re) (fst re')

  Coproduct-Equiv-12 : (re : RingEquiv Xr Yr) → (re' : RingEquiv X'r Y'r) →
                        RingEquiv (DirectProd-Ring Xr X'r) (DirectProd-Ring Yr Y'r)
  fst (Coproduct-Equiv-12 re re') = re×re' re re'
  snd (Coproduct-Equiv-12 re re') = makeIsRingHom fun-pres1 fun-pres+ fun-pres·
    where
    fun-pres1 : (fst (re×re' re re')) (1r Xstr , 1r X'str) ≡ (1r (Yr .snd) , 1r (Y'r .snd))
    fun-pres1 = ≡-× (pres1 (snd re)) (pres1 (snd re'))

    fun-pres+ : (x1 x2 : X × X') → (fst (re×re' re re')) (x1 +X×X' x2) ≡ (( (fst (re×re' re re')) x1) +Y×Y' ( (fst (re×re' re re')) x2))
    fun-pres+ (x1 , x'1) (x2 , x'2) = ≡-× (pres+ (snd re) x1 x2) (pres+ (snd re') x'1 x'2)

    fun-pres· : (x1 x2 : X × X') → (fst (re×re' re re')) (x1 ·X×X' x2) ≡ (( (fst (re×re' re re')) x1) ·Y×Y' ( (fst (re×re' re re')) x2))
    fun-pres· (x1 , x'1) (x2 , x'2) = ≡-× (pres· (snd re) x1 x2) (pres· (snd re') x'1 x'2)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Issue213 where

postulate
  Prod : Set → Set → Set
  A    : Set

Foo : Set
Foo = let infixr 3 _×_
          _×_ : Set → Set → Set
          _×_ = Prod
      in A × A × A


text:
module Categories.Functor.Construction.Product where

open import Categories.Category
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Functor.Bifunctor

open import Data.Product using (_,_)

module _ {o ℓ e} (𝒞 : Category o ℓ e) (cartesian : Cartesian 𝒞) where
  open Cartesian cartesian
  open BinaryProducts products

  open Category 𝒞

  Product : Bifunctor 𝒞 𝒞 𝒞
  Product = record
              { F₀ = λ (x , y) → x × y
              ; F₁ = λ (f , g) → f ⁂ g
              ; identity = Equiv.trans (⟨⟩-cong₂ identityˡ identityˡ) η
              ; homomorphism = Equiv.sym ⁂∘⁂
              ; F-resp-≈ = λ (x , y) → ⁂-cong₂ x y
              }

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
{-# OPTIONS --allow-unsolved-metas #-} -- FIXME

open import Everything

module Test.Test3 where

  module _
    {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂}
    where
    postulate instance functor : Functor 𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂
    open Functor ⦃ … ⦄
    test : asInstance `IsFunctor $ {!Transextensionality!.type _∼₁_ _∼̇₁_!}
    test = asInstance `IsFunctor transextensionality
    -- -- Test1.test-functor-transextensionality


text:
{-# OPTIONS --type-in-type #-}
module Record where

open import Prelude

record Sigma (A : Set)(B : A -> Set) : Set
record Sigma A B where
  constructor pair
  field
    fst : A
    snd : B fst

open Sigma

data Unit : Set
data Unit where
  tt : Unit

Cat : Set
Cat =
  Sigma Set                                                  (\ Obj ->
  Sigma (Obj -> Obj -> Set)                                  (\ Hom ->
  Sigma ((X : _) -> Hom X X)                                 (\ id ->
  Sigma ((X Y Z : _) -> Hom Y Z -> Hom X Y -> Hom X Z)       (\ comp ->
  Sigma ((X Y : _)(f : Hom X Y) -> comp _ _ _ (id Y) f == f) (\ idl ->
  Sigma ((X Y : _)(f : Hom X Y) -> comp _ _ _ f (id X) == f) (\ idr ->
  Sigma ((W X Y Z : _)
         (f : Hom W X)(g : Hom X Y)(h : Hom Y Z) ->
           comp _ _ _ (comp _ _ _ h g) f ==
           comp _ _ _ h (comp _ _ _ g f))                    (\ assoc ->
  Unit)))))))

Obj : (C : Cat) -> Set
Obj C = fst C

Hom : (C : Cat) -> Obj C -> Obj C -> Set
Hom C = fst (snd C)

id : (C : Cat) -> (X : _) -> Hom C X X
id C = fst (snd (snd C))

comp : (C : Cat) -> (X Y Z : _) -> Hom C Y Z -> Hom C X Y -> Hom C X Z
comp C = fst (snd (snd (snd C)))

idl : (C : Cat) -> (X Y : _)(f : Hom C X Y) ->
      comp C _ _ _ (id C Y) f == f
idl C = fst (snd (snd (snd (snd C))))

idr : (C : Cat) -> (X Y : _)(f : Hom C X Y) ->
      comp C _ _ _ f (id C X) == f
idr C = fst (snd (snd (snd (snd (snd C)))))

assoc : (C : Cat) ->
        (W X Y Z : _) (f : Hom C W X)(g : Hom C X Y)(h : Hom C Y Z) ->
        comp C _ _ _ (comp C _ _ _ h g) f ==
        comp C _ _ _ h (comp C _ _ _ g f)
assoc C = fst (snd (snd (snd (snd (snd (snd C))))))

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- By Philipp Hausmann.

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Float

data ⊥ : Set where

_/_ = primFloatDiv
_<_ = primFloatNumericalLess

cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

0eq : 0.0 ≡ -0.0
0eq = refl

bug : ⊥
bug = f (cong (λ x → (1.0 / x) < 0.0) 0eq)
  where
    f : false ≡ true → ⊥
    f ()

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module Data.BinaryTree.Properties where

import      Lvl
open import Data hiding (empty)
open import Data.BinaryTree
open import Data.Boolean
open import Functional as Fn
open import Logic.Propositional
open import Numeral.Natural
open import Type

private variable ℓ ℓᵢ ℓₗ ℓₙ ℓₒ : Lvl.Level
private variable n : ℕ
private variable N N₁ N₂ L T A B : Type{ℓ}

-- A tree is full when every node has no or all children.
data Full {L : Type{ℓₗ}}{N : Type{ℓₙ}} : BinaryTree L N → Type{ℓₗ Lvl.⊔ ℓₙ} where
  leaf   : ∀{l} → Full(Leaf l)
  single : ∀{a}{l₁ l₂} → Full(Node a (Leaf l₁) (Leaf l₂))
  step   : ∀{al ar a}{cll clr crl crr} → Full(Node al cll clr) → Full(Node ar crl crr) → Full(Node a (Node al cll clr) (Node ar crl crr))

-- A tree is perfect at depth `n` when all leaves are at height `n`.
-- In other words, a tree is perfect when all leaves are at the same height.
data Perfect {L : Type{ℓₗ}}{N : Type{ℓₙ}} : BinaryTree L N → ℕ → Type{ℓₗ Lvl.⊔ ℓₙ} where
  leaf : ∀{l} → Perfect(Leaf l)(𝟎)
  step : ∀{a}{l r}{h} → Perfect(l)(h) → Perfect(r)(h) → Perfect(Node a l r)(𝐒(h))

data Complete {L : Type{ℓₗ}}{N : Type{ℓₙ}} : BinaryTree L N → ℕ → Bool → Type{ℓₗ Lvl.⊔ ℓₙ} where
  perfect-leaf : ∀{l} → Complete(Leaf l)(𝟎)(𝑇)
  imperfect-leaf : ∀{l} → Complete(Leaf l)(𝐒(𝟎))(𝐹)
  step₀ : ∀{a}{l r}{h} → Complete(l)(h)(𝐹) → Complete(r)(h)(𝐹) → Complete(Node a l r)(𝐒(h))(𝐹)
  step₁ : ∀{a}{l r}{h} → Complete(l)(h)(𝑇) → Complete(r)(h)(𝐹) → Complete(Node a l r)(𝐒(h))(𝐹)
  step₂ : ∀{a}{l r}{h} → Complete(l)(h)(𝑇) → Complete(r)(h)(𝑇) → Complete(Node a l r)(𝐒(h))(𝑇)

data DepthOrdered {L : Type{ℓₗ}}{N : Type{ℓₙ}} (_≤_ : N → N → Type{ℓₒ}) : BinaryTree L N → Type{ℓₗ Lvl.⊔ ℓₙ Lvl.⊔ ℓₒ} where
  leaf : ∀{l} → DepthOrdered(_≤_)(Leaf l)
  step : ∀{a}{l₁ l₂} → DepthOrdered(_≤_)(Node a (Leaf l₁) (Leaf l₂))
  stepₗ : ∀{a al ar}{l}{rl rr} → (a ≤ al) → DepthOrdered(_≤_)(Node al rl rr)
                                          → DepthOrdered(_≤_)(Node a (Leaf l) (Node ar rl rr))
  stepᵣ : ∀{a al ar}{l}{ll lr} → (a ≤ ar) → DepthOrdered(_≤_)(Node ar ll lr)
                                          → DepthOrdered(_≤_)(Node a (Node al ll lr) (Leaf l))
  stepₗᵣ : ∀{a al ar}{ll lr rl rr} → (a ≤ al) → DepthOrdered(_≤_)(Node al ll lr)
                                   → (a ≤ ar) → DepthOrdered(_≤_)(Node ar rl rr)
                                   → DepthOrdered(_≤_)(Node a (Node al ll lr) (Node ar rl rr))

Heap : ∀{L : Type{ℓₗ}}{N : Type{ℓₙ}} → (N → N → Type{ℓₒ}) → BinaryTree L N → ℕ → Bool → Type
Heap(_≤_) tree height perfect = DepthOrdered(_≤_)(tree) ∧ Complete(tree)(height)(perfect)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
record Unit : Set where
  constructor unit

module S {A : Set} where
  id : {A : Set} → A → A
  id a = a

module T {A : Set} = S

Sid : (A : Set) → A → A
Sid A = S.id {A = Unit} {A = A}

Tid : (A : Set) → A → A
Tid A = T.id {A = Unit} {A = Unit} {A = A}


text:
module trie-thms where

open import bool
open import bool-thms
open import bool-thms2
open import char
open import eq
open import list
open import list-thms
open import maybe
open import product
open import product-thms
open import sum
open import string
open import trie

trie-lookup-empty-h : ∀ {A} x → trie-lookup-h{A} empty-trie x ≡ nothing
trie-lookup-empty-h [] = refl
trie-lookup-empty-h (_ :: _) = refl

trie-lookup-empty : ∀ {A} x → trie-lookup{A} empty-trie x ≡ nothing
trie-lookup-empty x = trie-lookup-empty-h (string-to-𝕃char x)

trie-cal-insert-nonempty : ∀{A : Set}(ts : cal (trie A))(c : char)(t : trie A) → trie-nonempty t ≡ tt →
                            trie-cal-nonempty (cal-insert ts c t) ≡ tt
trie-cal-insert-nonempty [] c t p rewrite p = refl
trie-cal-insert-nonempty ((c , t') :: ts) c' t p with c' =char c
trie-cal-insert-nonempty ((c , t') :: ts) c' t p | tt rewrite p = refl
trie-cal-insert-nonempty ((c , t') :: ts) c' t p | ff rewrite (trie-cal-insert-nonempty ts c' t p) =
  ||-tt (trie-nonempty t')

trie-insert-h-nonempty : ∀{A : Set}(t : trie A)(cs : 𝕃 char)(a : A) → trie-nonempty (trie-insert-h t cs a) ≡ tt
trie-insert-h-nonempty (Node x x₁) [] a = refl
trie-insert-h-nonempty (Node x ts) (c :: cs) a with cal-lookup ts c
trie-insert-h-nonempty (Node (just x) ts) (c :: cs) a | just t = refl
trie-insert-h-nonempty (Node nothing ts) (c :: cs) a | just t =
  trie-cal-insert-nonempty ts c (trie-insert-h t cs a) (trie-insert-h-nonempty t cs a)
trie-insert-h-nonempty (Node (just x) ts) (c :: cs) a | nothing = refl
trie-insert-h-nonempty (Node nothing ts) (c :: cs) a | nothing rewrite (trie-insert-h-nonempty empty-trie cs a) = refl

trie-insert-nonempty : ∀{A : Set}(t : trie A)(s : string)(a : A) → trie-nonempty (trie-insert t s a) ≡ tt
trie-insert-nonempty t s a = trie-insert-h-nonempty t (string-to-𝕃char s) a

trie-mappings-h-nonempty : ∀ {A : Set}(t : trie A)(prev-str : 𝕃 char) →
                             trie-nonempty t ≡ tt → is-empty (trie-mappings-h t prev-str) ≡ ff
trie-cal-mappings-h-nonempty : ∀ {A : Set}(ts : cal (trie A))(prev-str : 𝕃 char) →
                                 trie-cal-nonempty ts ≡ tt → is-empty (trie-cal-mappings-h ts prev-str) ≡ ff
trie-mappings-h-nonempty (Node (just x) x₁) prev-str _ = refl
trie-mappings-h-nonempty (Node nothing ts) prev-str p = trie-cal-mappings-h-nonempty ts prev-str p
trie-cal-mappings-h-nonempty [] prev-str ()
trie-cal-mappings-h-nonempty ((a , t) :: ts) prev-str p rewrite is-empty-++ (trie-mappings-h t (a :: prev-str)) (trie-cal-mappings-h ts prev-str) with ||-elim{trie-nonempty t} p
trie-cal-mappings-h-nonempty ((a , t) :: ts) prev-str _ | inj₁ p rewrite trie-mappings-h-nonempty t (a :: prev-str) p = refl
trie-cal-mappings-h-nonempty ((a , t) :: ts) prev-str _ | inj₂ p rewrite trie-cal-mappings-h-nonempty ts prev-str p | &&-ff (is-empty (trie-mappings-h t (a :: prev-str))) = refl

trie-mappings-nonempty : ∀ {A : Set}(t : trie A) →
                           trie-nonempty t ≡ tt → is-empty (trie-mappings t) ≡ ff
trie-mappings-nonempty t p = trie-mappings-h-nonempty t [] p

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Level polymorphic Empty type
------------------------------------------------------------------------

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

module Data.Empty.Polymorphic where

open import Level

data ⊥ {ℓ : Level} : Set ℓ where

⊥-elim : ∀ {w ℓ} {Whatever : Set w} → ⊥ {ℓ} → Whatever
⊥-elim ()


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Functions.Definition
open import Fields.Fields

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Fields.Orders.Partial.Definition {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (F : Field R) where

open Ring R

record PartiallyOrderedField {p} {_<_ : Rel {_} {p} A} (pOrder : SetoidPartialOrder S _<_) : Set (lsuc (m ⊔ n ⊔ p)) where
  field
    oRing : PartiallyOrderedRing R pOrder


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

open import Algebra
open import Relation.Binary
open import Algebra.Monus

module Data.MonoidalHeap {s} (monus : TMPOM s) where

open TMPOM monus

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

𝒮 : Type s
𝒮 = 𝑆 → 𝑆

⟦_⇑⟧ : 𝑆 → 𝒮
⟦_⇑⟧ = _∙_

⟦_⇓⟧ : 𝒮 → 𝑆
⟦ x ⇓⟧ = x ε

infixl 10 _⊙_
_⊙_ : (𝑆 → A) → 𝑆 → 𝑆 → A
f ⊙ x = λ y → f (x ∙ y)

infixr 6 _∹_&_
data Heap (V : 𝑆 → Type a) : Type (a ℓ⊔ s) where
  [] : Heap V
  _∹_&_ : (key : 𝑆) (val : V key) (children : List (Heap (V ⊙ key))) → Heap V

Heap⋆ : (V : 𝑆 → Type a) → Type (a ℓ⊔ s)
Heap⋆ V = List (Heap V)

private
  variable
    v : Level
    V : 𝑆 → Type v

⊙ε : V ≡ V ⊙ ε
⊙ε {V = V} i x = V (sym (ε∙ x) i)

lemma : ∀ x y k → x ≡ y ∙ k → ⟦ x ⇑⟧ ≡ ⟦ y ⇑⟧ ∘ ⟦ k ⇑⟧
lemma x y k x≡y∙k i z = (cong (_∙ z) x≡y∙k ; assoc y k z) i

merge : Heap V → Heap V → Heap V
merge [] ys = ys
merge (x ∹ xv & xs) [] = x ∹ xv & xs
merge {V = V} (x ∹ xv & xs) (y ∹ yv & ys) with x ≤|≥ y
... | inl (k , x≤y) = x ∹ xv & (k ∹ subst V x≤y yv & subst (List ∘ Heap ∘ _∘_ V) (lemma y x k x≤y) ys ∷ xs)
... | inr (k , x≥y) = y ∹ yv & (k ∹ subst V x≥y xv & subst (List ∘ Heap ∘ _∘_ V) (lemma x y k x≥y) xs ∷ ys)

mergeQs⁺ : Heap V → Heap⋆ V → Heap V
mergeQs⁺ x₁ [] = x₁
mergeQs⁺ x₁ (x₂ ∷ []) = merge x₁ x₂
mergeQs⁺ x₁ (x₂ ∷ x₃ ∷ xs) = merge (merge x₁ x₂) (mergeQs⁺ x₃ xs)

mergeQs : Heap⋆ V → Heap V
mergeQs [] = []
mergeQs (x ∷ xs) = mergeQs⁺ x xs

singleton : ∀ x → V x → Heap V
singleton x xv = x ∹ xv & []

insert : ∀ x → V x → Heap V → Heap V
insert x xv = merge (singleton x xv)

minView : Heap V → Maybe (∃ p × V p × Heap (V ⊙ p))
minView [] = nothing
minView (x ∹ xv & xs) = just (x , xv , mergeQs xs)

variable
  v₁ v₂ : Level
  V₁ : 𝑆 → Type v₁
  V₂ : 𝑆 → Type v₂

mutual
  maps : (∀ {x} → V₁ x → V₂ x) → Heap⋆ V₁ → Heap⋆ V₂
  maps f [] = []
  maps f (x ∷ xs) = map f x ∷ maps f xs

  map : (∀ {x} → V₁ x → V₂ x) → Heap V₁ → Heap V₂
  map f [] = []
  map f (k ∹ v & xs) = k ∹ f v & maps f xs

mutual
  size : Heap V → ℕ
  size [] = zero
  size (_ ∹ _ & xs) = suc (sizes xs)

  sizes : Heap⋆ V → ℕ
  sizes [] = 0
  sizes (x ∷ xs) = size x ℕ.+ sizes xs

open import Data.Maybe using (maybe)
open import Path.Reasoning
open import Cubical.Foundations.Prelude using (substRefl)

lemma₂ : ∀ {x y : 𝑆 → 𝑆} xs (p : x ≡ y) → sizes (subst (List ∘ Heap ∘ _∘_ V) p xs) ≡ sizes xs
lemma₂ {V = V} xs = J (λ _ p → sizes (subst (List ∘ Heap ∘ _∘_ V) p xs) ≡ sizes xs) (cong sizes (substRefl {B = List ∘ Heap ∘ _∘_ V} xs))

merge-size : (xs ys : Heap V) → size (merge xs ys) ≡ size xs ℕ.+ size ys
merge-size [] ys = refl
merge-size (x ∹ xv & xs) [] = sym (ℕ.+-idʳ _)
merge-size {V = V} (x ∹ xv & xs) (y ∹ yv & ys) with x ≤|≥ y
merge-size {V = V} (x ∹ xv & xs) (y ∹ yv & ys) | inr (k , x≥y) =
  suc (suc (sizes (subst (List ∘ Heap ∘ _∘_ V) (lemma x y k x≥y) xs)) ℕ.+ sizes ys) ≡˘⟨ ℕ.+-suc _ (sizes ys) ⟩
  suc (sizes (subst (List ∘ Heap ∘ _∘_ V) (lemma x y k x≥y) xs)) ℕ.+ suc (sizes ys) ≡⟨ cong (ℕ._+ suc (sizes ys)) (cong suc (lemma₂ {V = V} xs (lemma x y k x≥y))) ⟩
  suc (sizes xs) ℕ.+ suc (sizes ys) ∎
merge-size {V = V} (x ∹ xv & xs) (y ∹ yv & ys) | inl (k , x≤y) =
  suc (suc (sizes (subst (List ∘ Heap ∘ _∘_ V) (lemma y x k x≤y) ys)) ℕ.+ sizes xs) ≡˘⟨ ℕ.+-suc _ (sizes xs) ⟩
  suc (sizes (subst (List ∘ Heap ∘ _∘_ V) (lemma y x k x≤y) ys)) ℕ.+ suc (sizes xs) ≡⟨ cong (ℕ._+ suc (sizes xs)) (cong suc (lemma₂ {V = V} ys (lemma y x k x≤y))) ⟩
  suc (sizes ys) ℕ.+ suc (sizes xs) ≡⟨ ℕ.+-comm (suc (sizes ys)) (suc (sizes xs)) ⟩
  suc (sizes xs) ℕ.+ suc (sizes ys) ∎

mutual
  minViewSizes : (xs : Heap⋆ V) → sizes xs ≡ size (mergeQs xs)
  minViewSizes [] = refl
  minViewSizes (x ∷ xs) = minViewSizes⁺ x xs

  minViewSizes⁺ : (x : Heap V) → (xs : Heap⋆ V) → sizes (x ∷ xs) ≡ size (mergeQs⁺ x xs)
  minViewSizes⁺ x₁ [] = ℕ.+-idʳ _
  minViewSizes⁺ x₁ (x₂ ∷ []) = cong (λ z → size x₁ ℕ.+ z) (ℕ.+-idʳ _) ; sym (merge-size x₁ x₂)
  minViewSizes⁺ x₁ (x₂ ∷ x₃ ∷ xs) =
    size x₁ ℕ.+ (size x₂ ℕ.+ sizes (x₃ ∷ xs)) ≡˘⟨ ℕ.+-assoc (size x₁) (size x₂) (sizes (x₃ ∷ xs)) ⟩
    (size x₁ ℕ.+ size x₂) ℕ.+ sizes (x₃ ∷ xs) ≡⟨ cong ((size x₁ ℕ.+ size x₂) ℕ.+_) (minViewSizes⁺ x₃ xs) ⟩
    (size x₁ ℕ.+ size x₂) ℕ.+ size (mergeQs⁺ x₃ xs) ≡˘⟨ cong (ℕ._+ size (mergeQs⁺ x₃ xs)) (merge-size x₁ x₂) ⟩
    size (merge x₁ x₂) ℕ.+ size (mergeQs⁺ x₃ xs) ≡˘⟨ merge-size (merge x₁ x₂) (mergeQs⁺ x₃ xs) ⟩
    size (merge (merge x₁ x₂) (mergeQs⁺ x₃ xs)) ∎

minViewSize : (xs : Heap V) → size xs ≡ maybe zero (suc ∘ size ∘ snd ∘ snd) (minView xs)
minViewSize [] = refl
minViewSize (x ∹ xv & xs) = cong suc (minViewSizes xs)

zer : Heap⋆ V
zer = []

one : Heap⋆ V
one = [] ∷ []

open import Data.List using (_++_; concatMap)

_<+>_ : Heap⋆ V → Heap⋆ V → Heap⋆ V
_<+>_ = _++_

multIn : (p : 𝑆 → 𝑆) → (c : ∀ {x y} → V (p x) → V y → V (p (x ∙ y))) → (V ⇒ V ∘ p) → Heap⋆ (V ∘ p) → Heap⋆ V → Heap⋆ (V ∘ p)
multIn {V = V} p c f [] ys = []
multIn {V = V} p c f ([] ∷ xs) ys = maps f ys ++ multIn p c f xs ys
multIn {V = V} p c f (x ∹ xv & xc ∷ xs) ys = x ∹ xv & multIn (p ∘ ⟦ x ⇑⟧) (λ v₁ v₂ → subst V (cong p (assoc x _ _)) (c v₁ v₂)) (c xv) xc ys ∷ multIn p c f xs ys

appl : (∀ {x y} → V x → V y → V (x ∙ y)) → Heap⋆ V → Heap⋆ V → Heap⋆ V
appl {V = V} f xs ys = multIn {V = V} id f id xs ys

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import lib.Basics
open import lib.types.Group
open import lib.types.List
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Word
open import lib.groups.Homomorphism
open import lib.groups.GeneratedGroup
open import lib.groups.GeneratedAbelianGroup
open import lib.groups.Isomorphism

module lib.groups.TensorProduct where

module TensorProduct₀ {i} {j} (G : AbGroup i) (H : AbGroup j) where

  private
    module G = AbGroup G
    module H = AbGroup H

  ⊗-pair : Type (lmax i j)
  ⊗-pair = G.El × H.El

  data ⊗-rel : Word ⊗-pair → Word ⊗-pair → Type (lmax i j) where
    linear-l : (g₁ g₂ : G.El) (h : H.El) →
      ⊗-rel (inl (G.comp g₁ g₂ , h) :: nil) (inl (g₁ , h) :: inl (g₂ , h) :: nil)
    linear-r : (g : G.El) (h₁ h₂ : H.El) →
      ⊗-rel (inl (g , H.comp h₁ h₂) :: nil) (inl (g , h₁) :: inl (g , h₂) :: nil)

  private
    module Gen = GeneratedAbelianGroup ⊗-pair ⊗-rel
  open Gen hiding (GenGroup; GenAbGroup; El) public

  abstract
    abgroup : AbGroup (lmax i j)
    abgroup = Gen.GenAbGroup

  open AbGroup abgroup public

  abstract
    infixr 80 _⊗_
    _⊗_ : G.El → H.El → El
    _⊗_ g h = insert (g , h)

    ⊗-lin-l : ∀ g₁ g₂ h → G.comp g₁ g₂ ⊗ h == comp (g₁ ⊗ h) (g₂ ⊗ h)
    ⊗-lin-l g₁ g₂ h = rel-holds (linear-l g₁ g₂ h)

    ⊗-lin-r : ∀ g h₁ h₂ → g ⊗ H.comp h₁ h₂ == comp (g ⊗ h₁) (g ⊗ h₂)
    ⊗-lin-r g h₁ h₂ = rel-holds (linear-r g h₁ h₂)

    ⊗-unit-l : ∀ h → G.ident ⊗ h == ident
    ⊗-unit-l h = cancel-l (G.ident ⊗ h) $
      comp (G.ident ⊗ h) (G.ident ⊗ h)
        =⟨ ! (⊗-lin-l G.ident G.ident h) ⟩
      G.comp G.ident G.ident ⊗ h
        =⟨ ap (_⊗ h) (G.unit-l G.ident) ⟩
      G.ident ⊗ h
        =⟨ ! (unit-r (G.ident ⊗ h)) ⟩
      comp (G.ident ⊗ h) ident =∎

    ⊗-unit-r : ∀ g → g ⊗ H.ident == ident
    ⊗-unit-r g = cancel-r (g ⊗ H.ident) $
      comp (g ⊗ H.ident) (g ⊗ H.ident)
        =⟨ ! (⊗-lin-r g H.ident H.ident) ⟩
      g ⊗ H.comp H.ident H.ident
        =⟨ ap (g ⊗_) (H.unit-l H.ident) ⟩
      g ⊗ H.ident
        =⟨ ! (unit-r (g ⊗ H.ident)) ⟩
      comp (g ⊗ H.ident) ident =∎

  ins-l-hom : H.El → G.grp →ᴳ grp
  ins-l-hom h = group-hom (_⊗ h) (λ g₁ g₂ → ⊗-lin-l g₁ g₂ h)

  ins-r-hom : G.El → H.grp →ᴳ grp
  ins-r-hom g = group-hom (g ⊗_) (⊗-lin-r g)

  module BilinearMaps {k} (L : AbGroup k) where

    private
      module L = AbGroup L
      module HE = Gen.HomomorphismEquiv L

    is-linear-l : (G.El → H.El → L.El) → Type (lmax i (lmax j k))
    is-linear-l b = ∀ g₁ g₂ h → b (G.comp g₁ g₂) h == L.comp (b g₁ h) (b g₂ h)

    is-linear-l-is-prop : (b : G.El → H.El → L.El) → is-prop (is-linear-l b)
    is-linear-l-is-prop b =
      Π-level $ λ g₁ →
      Π-level $ λ g₂ →
      Π-level $ λ h →
      has-level-apply L.El-level _ _

    is-linear-r : (G.El → H.El → L.El) → Type (lmax i (lmax j k))
    is-linear-r b = ∀ g h₁ h₂ → b g (H.comp h₁ h₂) == L.comp (b g h₁) (b g h₂)

    is-linear-r-is-prop : (b : G.El → H.El → L.El) → is-prop (is-linear-r b)
    is-linear-r-is-prop b =
      Π-level $ λ g →
      Π-level $ λ h₁ →
      Π-level $ λ h₂ →
      has-level-apply L.El-level _ _

    record BilinearMap : Type (lmax i (lmax j k)) where
      field
        bmap : G.El → H.El → L.El
        linearity-l : is-linear-l bmap
        linearity-r : is-linear-r bmap

    BilinearMap= : {b b' : BilinearMap}
      → BilinearMap.bmap b == BilinearMap.bmap b'
      → b == b'
    BilinearMap= {b} {b'} idp =
      ap2 mk-bilinear-map
        (prop-path (is-linear-l-is-prop b.bmap) b.linearity-l b'.linearity-l)
        (prop-path (is-linear-r-is-prop b.bmap) b.linearity-r b'.linearity-r)
      where
      module b  = BilinearMap b
      module b' = BilinearMap b'
      mk-bilinear-map : is-linear-l b.bmap → is-linear-r b.bmap → BilinearMap
      mk-bilinear-map lin-l lin-r =
        record { bmap = b.bmap; linearity-l = lin-l; linearity-r = lin-r }

    bilinear-to-legal-equiv : BilinearMap ≃ HE.RelationRespectingFunction
    bilinear-to-legal-equiv =
      equiv to from
            (λ lf → HE.RelationRespectingFunction= idp)
            (λ b  → BilinearMap= idp)
      where
      to : BilinearMap → HE.RelationRespectingFunction
      to b = HE.rel-res-fun f f-respects
        where
        module b = BilinearMap b
        f : ⊗-pair → L.El
        f (g , h) = b.bmap g h
        f-respects : HE.respects-rel f
        f-respects (linear-l g₁ g₂ h) = b.linearity-l g₁ g₂ h
        f-respects (linear-r g h₁ h₂) = b.linearity-r g h₁ h₂
      from : HE.RelationRespectingFunction → BilinearMap
      from (HE.rel-res-fun f f-respects) =
        record { bmap = bmap; linearity-l = linearity-l; linearity-r = linearity-r }
        where
        bmap : G.El → H.El → L.El
        bmap g h = f (g , h)
        linearity-l : is-linear-l bmap
        linearity-l g₁ g₂ h = f-respects (linear-l g₁ g₂ h)
        linearity-r : is-linear-r bmap
        linearity-r g h₁ h₂ = f-respects (linear-r g h₁ h₂)

  module UniversalProperty {k} (L : AbGroup k) where

    open BilinearMaps L public
    private
      module HE = Gen.HomomorphismEquiv L

    abstract
      extend-equiv : BilinearMap ≃ (grp →ᴳ AbGroup.grp L)
      extend-equiv =
        HE.extend-equiv ∘e bilinear-to-legal-equiv

      extend : BilinearMap → (grp →ᴳ AbGroup.grp L)
      extend = –> extend-equiv

      restrict : (grp →ᴳ AbGroup.grp L) → BilinearMap
      restrict = <– extend-equiv

      extend-β : ∀ b g h → GroupHom.f (extend b) (g ⊗ h) == BilinearMap.bmap b g h
      extend-β b g h = idp

      hom= : ∀ {ϕ ψ : grp →ᴳ AbGroup.grp L}
        → (∀ g h → GroupHom.f ϕ (g ⊗ h) == GroupHom.f ψ (g ⊗ h))
        → ϕ == ψ
      hom= {ϕ} {ψ} e =
        ϕ
          =⟨ ! (<–-inv-r extend-equiv ϕ) ⟩
        extend (restrict ϕ)
          =⟨ ap extend (BilinearMap= (λ= (λ g → λ= (λ h → e g h)))) ⟩
        extend (restrict ψ)
          =⟨ <–-inv-r extend-equiv ψ ⟩
        ψ =∎

module TensorProduct₁ {i} {j} (G : AbGroup i) (H : AbGroup j) where

  private
    module G⊗H = TensorProduct₀ G H
    module H⊗G = TensorProduct₀ H G
    module F = G⊗H.UniversalProperty H⊗G.abgroup

    b : F.BilinearMap
    b =
      record
      { bmap = λ g h → h H⊗G.⊗ g
      ; linearity-l = λ g₁ g₂ h → H⊗G.⊗-lin-r h g₁ g₂
      ; linearity-r = λ g h₁ h₂ → H⊗G.⊗-lin-l h₁ h₂ g
      }

  swap : (G⊗H.grp →ᴳ H⊗G.grp)
  swap = F.extend b

  swap-β : ∀ g h →
    GroupHom.f swap (g G⊗H.⊗ h) == h H⊗G.⊗ g
  swap-β g h = F.extend-β b g h

  open G⊗H public

module TensorProduct₂ {i} {j} (G : AbGroup i) (H : AbGroup j) where

  private
    module G⊗H = TensorProduct₁ G H
    module H⊗G = TensorProduct₁ H G

  swap-swap : ∀ s → GroupHom.f (H⊗G.swap ∘ᴳ G⊗H.swap) s == s
  swap-swap s =
    ap (λ ϕ → GroupHom.f ϕ s) $
    G⊗H.UniversalProperty.hom= G⊗H.abgroup {ϕ = H⊗G.swap ∘ᴳ G⊗H.swap} {ψ = idhom _} $
    λ g h → ap (GroupHom.f H⊗G.swap) (G⊗H.swap-β g h) ∙ H⊗G.swap-β h g

  swap-swap-idhom : H⊗G.swap ∘ᴳ G⊗H.swap == idhom G⊗H.grp
  swap-swap-idhom = group-hom= (λ= swap-swap)

  open G⊗H public

module TensorProduct {i} {j} (G : AbGroup i) (H : AbGroup j) where

  private
    module G⊗H = TensorProduct₂ G H
    module H⊗G = TensorProduct₂ H G

  swap-is-equiv : is-equiv (GroupHom.f G⊗H.swap)
  swap-is-equiv = is-eq _ (GroupHom.f H⊗G.swap) H⊗G.swap-swap G⊗H.swap-swap

  commutative : G⊗H.grp ≃ᴳ H⊗G.grp
  commutative = G⊗H.swap , swap-is-equiv

  open G⊗H public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

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

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

open import LibraBFT.Base.Types
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Crypto
open import Optics.All
open import Util.Encode
open import Util.KVMap                            as Map
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId

-- This module defines types for connecting abstract and concrete
-- votes by defining what constitutes enough "evidence" that a
-- vote was cast, which is passed around in the abstract model as
-- the variable (𝓥 : VoteEvidence); here we instantiate it to
-- 'ConcreteVoteEvidence'.
--
-- Some of the types in this module depend on an EpochConfig, but
-- never inspect it. Consequently, we define everything over an
-- abstract 𝓔 passed around as module parameter to an inner module
-- WithEC.  Before that, we define some definitions relevant to
-- constructing EpochConfigs from RoundManager.

module LibraBFT.ImplShared.Consensus.Types.EpochDep where

-- Note that the definitions below are relevant only to the verification, not the implementation.
-- They should probably move somewhere else.

-- ValidatorVerifier-correct imposes requirements on a ValidatorVerifier that are sufficient to
-- ensure that we can construct an abstract EpochConfig based on it (see α-EC-VV below).
ValidatorVerifier-correct : ValidatorVerifier → Set
ValidatorVerifier-correct vv =
  let authorsInfo    = List-map proj₂ (kvm-toList (vv ^∙ vvAddressToValidatorInfo))
      totalVotPower  = f-sum (_^∙ vciVotingPower) authorsInfo
      quorumVotPower = vv ^∙ vvQuorumVotingPower
      bizF           = totalVotPower ∸ quorumVotPower
      pksAll≢        = ∀ v₁ v₂ nId₁ nId₂ → nId₁ ≢ nId₂
                       → lookup nId₁ (vv ^∙ vvAddressToValidatorInfo) ≡ just v₁
                       → lookup nId₂ (vv ^∙ vvAddressToValidatorInfo) ≡ just v₂
                       → v₁ ^∙ vciPublicKey ≢ v₂ ^∙ vciPublicKey
   in   3 * bizF       < totalVotPower
      × quorumVotPower ≤ totalVotPower
      × pksAll≢
      × f-sum (_^∙ vciVotingPower) (List-filter (Meta-DishonestPK? ∘ (_^∙ vciPublicKey)) authorsInfo) ≤ bizF

open DecLemmas {A = NodeId} _≟_
import LibraBFT.Abstract.BFT

-- α-EC-VV computes an abstract EpochConfig given a ValidatorVerifier
-- that satisfies the conditions stipulated by ValidVerifier-correct
α-EC-VV : Σ ValidatorVerifier ValidatorVerifier-correct → Epoch → EpochConfig
α-EC-VV (vv , ok) epoch =
      EpochConfig∙new bsId
                      epoch
                      numAuthors
                      toNodeId
                      (list-index (_≟_ ∘ proj₁) authors)
                      (index∘lookup-id authors proj₁ authorsIDs≢)
                      (λ lkp≡α → lookup∘index-id authors proj₁ authorsIDs≢ lkp≡α)
                      getPubKey
                      getPKey-Inj
                      (λ quorum → qsize ≤ VotPowerMembers quorum
                                   × allDistinct quorum)
                      λ q₁ q₂ → LibraBFT.Abstract.BFT.bft-lemma
                                  numAuthors
                                  (_^∙ vciVotingPower ∘ getAuthorInfo)
                                  (f-sum (_^∙ vciVotingPower) authorsInfo ∸ qsize)
                                  (≤-trans (proj₁ ok) (≡⇒≤ totalVotPower≡))
                                  getPubKey
                                  (let disMembers  = List-filter (Meta-DishonestPK? ∘ getPubKey) members
                                       sumDisM≡    = sum-f∘g disMembers (_^∙ vciVotingPower) getAuthorInfo
                                       disM≡disNId = map∘filter members authorsInfo getAuthorInfo
                                                                (Meta-DishonestPK? ∘ (_^∙ vciPublicKey)) getAuthInfo≡VCI
                                       sumDis≤bizF = (proj₂ ∘ proj₂ ∘ proj₂) ok
                                   in ≤-trans (≡⇒≤ (trans sumDisM≡ (cong (f-sum _vciVotingPower) disM≡disNId))) sumDis≤bizF)
                                  (proj₂ q₁) (proj₂ q₂)
                                  (≤-trans (≡⇒≤ N∸bizF≡Qsize) (proj₁ q₁))
                                  (≤-trans (≡⇒≤ N∸bizF≡Qsize) (proj₁ q₂))
                              -- TODO-2: this takes the per-epoch genesisUID from the GenesisInfo
                              -- for the *first* epoch (soon to be renamed to BootStrapInfo avoid
                              -- this confusion).  This is temporary until we do epoch change; then
                              -- it will need to be provided by the caller.
      where bsId            = fakeBootstrapInfo ^∙ bsiLIWS ∙ liwsLedgerInfo ∙ liConsensusDataHash
            authorsMap      = vv ^∙ vvAddressToValidatorInfo
            authors         = kvm-toList authorsMap
            authorsIDs≢     = kvm-keys-All≢ authorsMap
            authorsInfo     = List-map proj₂ authors
            numAuthors      = length authors
            members         = allFin numAuthors
            qsize           = vv ^∙ vvQuorumVotingPower
            toNodeId        = proj₁ ∘ List-lookup authors
            getAuthorInfo   = proj₂ ∘ List-lookup authors
            getPubKey       = _^∙ vciPublicKey ∘ getAuthorInfo
            VotPowerMembers = f-sum (_^∙ vciVotingPower ∘ getAuthorInfo)
            VotPowerAuthors = f-sum (_^∙ vciVotingPower)
            bizF            = VotPowerAuthors authorsInfo ∸ qsize
            getAuthInfo≡VCI : List-map getAuthorInfo members ≡ authorsInfo
            getAuthInfo≡VCI = trans (List-map-compose members) (cong (List-map proj₂) (map-lookup-allFin authors))
            totalVotPower≡  : VotPowerAuthors authorsInfo ≡ VotPowerMembers members
            totalVotPower≡  = let sumf∘g = sum-f∘g members (_^∙ vciVotingPower) getAuthorInfo
                              in sym (trans sumf∘g (cong (f-sum (_^∙ vciVotingPower)) getAuthInfo≡VCI))
            N∸bizF≡Qsize    = subst ((_≡ qsize) ∘ (_∸ bizF)) totalVotPower≡ (m∸[m∸n]≡n ((proj₁ ∘ proj₂) ok))
            getPKey-Inj   : ∀ {m₁ m₂} → getPubKey m₁ ≡ getPubKey m₂ → m₁ ≡ m₂
            getPKey-Inj {m₁} {m₂} pk≡
              with m₁ ≟Fin m₂
            ...| yes m₁≡m₂ = m₁≡m₂
            ...| no  m₁≢m₂ = let nIdm₁≢nIdm₂ = allDistinct-Map {xs = authors} proj₁ authorsIDs≢ m₁≢m₂
                                 pksAll≢ = (proj₁ ∘ proj₂ ∘ proj₂) ok
                             in ⊥-elim (pksAll≢ (getAuthorInfo m₁) (getAuthorInfo m₂)
                                                (toNodeId m₁) (toNodeId m₂) nIdm₁≢nIdm₂
                                                (kvm-toList-lookup authorsMap) (kvm-toList-lookup authorsMap)
                                         pk≡)

postulate -- TODO-2: define BootstrapInfo to match implementation and write these functions
  init-EC : BootstrapInfo → EpochConfig

module WithEC (𝓔 : EpochConfig) where
  open EpochConfig 𝓔
  open WithAbsVote 𝓔

  -- A 'ConcreteVoteEvidence' is a piece of information that
  -- captures that the 'vd : AbsVoteData' in question was not /invented/
  -- but instead, comes from a concrete vote that is /valid/ (that is,
  -- signature has been checked and author belongs to this epoch).
  --
  -- Moreover, we will also store the RecordChain that leads to the vote;
  -- this requires some mutually-recursive shenanigans, so we first declare
  -- ConcreteVoteEvidence, then import the necessary modules, and then define it.
  record ConcreteVoteEvidence (vd : AbsVoteData) : Set

  open import LibraBFT.Abstract.Abstract UID _≟UID_ NodeId 𝓔 ConcreteVoteEvidence as Abs hiding (qcVotes; Vote)

  data VoteCoherence (v : Vote) (b : Abs.Block) : Set where
    initial  : v ^∙ vParentId    ≡ genesisUID
             → v ^∙ vParentRound ≡ 0
             → Abs.bPrevQC b     ≡ nothing
             → VoteCoherence v b

    ¬initial : ∀{b' q}
             → v ^∙ vParentId    ≢ genesisUID
             → v ^∙ vParentRound ≢ 0
             → v ^∙ vParentId    ≡ Abs.bId b'
             → v ^∙ vParentRound ≡ Abs.bRound b'
             → (Abs.B b') ← (Abs.Q q)
             → (Abs.Q q)  ← (Abs.B b)
             → VoteCoherence v b

  -- Estabilishing validity of a concrete vote involves checking:
  --
  --   i) Vote author belongs to the current epoch
  --  ii) Vote signature is correctly verified
  -- iii) Existence of a RecordChain up to the voted-for block.
  --  iv) Coherence of 'vdParent' field with the above record chain.
  --
  record IsValidVote (v : Vote) : Set where
    constructor IsValidVote∙new
    inductive
    field
      _ivvMember   : Member
      _ivvAuthor   : isMember? (_vAuthor v) ≡ just _ivvMember
      _ivvSigned   : WithVerSig (getPubKey _ivvMember) v

      _ivvVDhash   : v ^∙ vLedgerInfo ∙ liConsensusDataHash ≡ hashVD (v ^∙ vVoteData)

      -- A valid vote must vote for a block that exists and is
      -- inserted in a RecordChain.
      _ivvBlock    : Abs.Block
      _ivvBlockId  : v ^∙ vProposedId ≡ Abs.bId _ivvBlock

      -- Moreover; we must check that the 'parent' field of the vote is coherent.
      _ivvCoherent : VoteCoherence v _ivvBlock

      -- Finally, the vote is for the correct epoch
      _ivvEpoch    : v ^∙ vEpoch ≡ epoch
      _ivvEpoch2   : v ^∙ vParent ∙ biEpoch ≡ epoch  -- Not needed?
  open IsValidVote public

  -- A valid vote can be directly mapped to an AbsVoteData. Abstraction of QCs
  -- and blocks will be given in LibraBFT.Concrete.Records, since those are
  -- more involved functions.
  α-ValidVote : (v : Vote) → Member → AbsVoteData
  α-ValidVote v mbr = AbsVoteData∙new (v ^∙ vProposed ∙ biRound)
                                      mbr
                                      (v ^∙ vProposed ∙ biId)

  -- α-ValidVote is the same for two votes that have the same vAuthor, vdProposed and vOrder
  α-ValidVote-≡ : ∀ {cv v'} {m : Member}
                → _vdProposed (_vVoteData cv) ≡ _vdProposed (_vVoteData v')
                → α-ValidVote cv m ≡ α-ValidVote v' m
  α-ValidVote-≡ {cv} {v'} prop≡ =
    AbsVoteData-η (cong _biRound prop≡) refl (cong _biId prop≡)

  -- Finally; evidence for some abstract vote consists of a concrete valid vote
  -- that is coherent with the abstract vote data.
  record ConcreteVoteEvidence vd where
    constructor CVE∙new
    inductive
    field
      _cveVote        : Vote
      _cveIsValidVote : IsValidVote _cveVote
      _cveIsAbs       : α-ValidVote _cveVote (_ivvMember _cveIsValidVote) ≡ vd
  open ConcreteVoteEvidence public

  -- Gets the signature of a concrete vote evidence
  _cveSignature : ∀{vd} → ConcreteVoteEvidence vd → Signature
  _cveSignature = _vSignature ∘ _cveVote

  -- A valid quorum certificate contains a collection of valid votes, such that
  -- the members represented by those votes (which exist because the votes are valid)
  -- constitutes a quorum.
  record MetaIsValidQC (qc : QuorumCert) : Set where
    field
      _ivqcMetaVotesValid      : All (IsValidVote ∘ rebuildVote qc) (qcVotes qc)
      _ivqcMetaIsQuorum        : IsQuorum (All-reduce _ivvMember _ivqcMetaVotesValid)
  open MetaIsValidQC public

  -- A valid TimeoutCertificate has a quorum of signatures that are valid for the current
  -- EpochConfig.  There will be a lot of overlap with MetaIsValidQc and IsValidVote.
  -- TODO-2: flesh out the details.
  postulate -- TODO-1: defined if needed (see draft below)
    MetaIsValidTimeoutCert : TimeoutCertificate → Set

  {-
  record MetaIsValidTimeoutCert (tc : TimeoutCertificate) : Set where
    field
      _ivtcMetaSigsValid :
      _ivtcMetaIsQuorum  :
  -}

  vqcMember : (qc : QuorumCert) → MetaIsValidQC qc
             → ∀ {as} → as ∈ qcVotes qc → Member
  vqcMember qc v {α , _ , _} as∈qc with All-lookup (_ivqcMetaVotesValid v) as∈qc
  ...| prf = _ivvMember prf


text:
{-# OPTIONS --without-K #-}
module isos-examples where

open import Function
open import Function.Related.TypeIsomorphisms.NP
import Function.Inverse.NP as FI
open FI using (_↔_; inverses; module Inverse) renaming (_$₁_ to to; _$₂_ to from)
import Function.Related as FR
open import Type hiding (★)
open import Data.Product.NP
open import Data.Bool.NP using (✓)
open import Data.One using (𝟙)
open import Data.Bits
open import Relation.Binary
import Relation.Binary.PropositionalEquality as ≡
open ≡ using (_≡_; subst)

_≈₂_ : ∀ {a} {A : ★ a} (f g : A → Bit) → ★ _
_≈₂_ {A = A} f g = Σ A (✓ ∘ f) ↔ Σ A (✓ ∘ g)

module _ {a r} {A : ★ a} {R : ★ r} where
  _≈_ : (f g : A → R) → ★ _
  f ≈ g = ∀ (O : R → ★ r) → Σ A (O ∘ f) ↔ Σ A (O ∘ g)

  ≈-refl : Reflexive {A = A → R} _≈_
  ≈-refl _ = FI.id

  ≈-trans : Transitive {A = A → R} _≈_
  ≈-trans p q O = q O FI.∘ p O

  ≈-sym : Symmetric {A = A → R} _≈_
  ≈-sym p O = FI.sym (p O)

module _ {a r} {A : ★ a} {R : ★ r} (f : A → R) (p : A ↔ A) where
  stable : f ≈ (f ∘ from p)
  stable _ = first-iso p

  stable′ : f ≈ (f ∘ to p)
  stable′ _ = first-iso (FI.sym p)

module _ {a b r} {A : ★ a} {B : ★ b} {R : ★ r} where
  _≋_ : (f : A → R) (g : B → R) → ★ _
  f ≋ g = (f ∘ proj₁) ≈ (g ∘ proj₂)

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

  _≋′_ : (f : A → R) (g : B → R) → ★ _
  f ≋′ g = ∀ (O : R → ★ r) →
            (B × Σ A (O ∘ f)) ↔ (A × Σ B (O ∘ g))

  module _ {f : A → R} {g : B → R} where
    open FR.EquationalReasoning

    ≋′→≋ : f ≋′ g → f ≋ g
    ≋′→≋ h O = Σ (A × B) (O ∘ f ∘ proj₁)
             ↔⟨ Σ×-swap ⟩
               Σ (B × A) (O ∘ f ∘ proj₂)
             ↔⟨ Σ-assoc ⟩
               (B × Σ A (O ∘ f))
             ↔⟨ h O ⟩
               (A × Σ B (O ∘ g))
             ↔⟨ FI.sym Σ-assoc ⟩
               Σ (A × B) (O ∘ g ∘ proj₂)
             ∎

    ≋→≋′ : f ≋ g → f ≋′ g
    ≋→≋′ h O = (B × Σ A (O ∘ f))
             ↔⟨ FI.sym Σ-assoc ⟩
               Σ (B × A) (O ∘ f ∘ proj₂)
             ↔⟨ Σ×-swap ⟩
               Σ (A × B) (O ∘ f ∘ proj₁)
             ↔⟨ h O ⟩
               Σ (A × B) (O ∘ g ∘ proj₂)
             ↔⟨ Σ-assoc ⟩
               (A × Σ B (O ∘ g))
             ∎
             -- -}
             -- -}
             -- -}
             -- -}
             -- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
{-# OPTIONS --without-K #-}
open import container.core

module container.w.algebra
  {li la lb}(c : Container li la lb) where

open import sum
open import equality
open import container.w.core
open import function.extensionality
open import function.isomorphism
open import hott.level.core

open Container c

Alg : ∀ ℓ → Set _
Alg ℓ = Σ (I → Set ℓ) λ X → F X →ⁱ X

carrier : ∀ {ℓ} → Alg ℓ → I → Set ℓ
carrier (X , _) = X

IsMor : ∀ {ℓ₁ ℓ₂}(𝓧 : Alg ℓ₁)(𝓨 : Alg ℓ₂)
      → (carrier 𝓧 →ⁱ carrier 𝓨) → Set _
IsMor (X , θ) (Y , ψ) f = ψ ∘ⁱ imap f ≡ f ∘ⁱ θ

Mor : ∀ {ℓ₁ ℓ₂} → Alg ℓ₁ → Alg ℓ₂ → Set _
Mor 𝓧 𝓨 = Σ (carrier 𝓧 →ⁱ carrier 𝓨) (IsMor 𝓧 𝓨)

𝓦 : Alg _
𝓦 = W c , inW c

module _ {ℓ₁ ℓ₂}(𝓧 : Alg ℓ₁)(𝓨 : Alg ℓ₂) where
  private
    X = proj₁ 𝓧; θ = proj₂ 𝓧
    Y = proj₁ 𝓨; ψ = proj₂ 𝓨

  is-mor-transp : {f g : X →ⁱ Y}(p : f ≡ g)
                → (α : IsMor 𝓧 𝓨 f)
                → sym (ap (λ h → ψ ∘ⁱ imap h) p) · α · ap (λ h → h ∘ⁱ θ) p
                ≡ subst (IsMor 𝓧 𝓨) p α
  is-mor-transp {f} {.f} refl α = left-unit α

  MorEq : Mor 𝓧 𝓨 → Mor 𝓧 𝓨 → Set _
  MorEq (f , α) (g , β) = Σ (f ≡ g) λ p
    → sym (ap (λ h → ψ ∘ⁱ imap h) p) · α · ap (λ h → h ∘ⁱ θ) p ≡ β

  MorH : Mor 𝓧 𝓨 → Mor 𝓧 𝓨 → Set _
  MorH (f , α) (g , β) = Σ (∀ i x → f i x ≡ g i x) λ p
    → ∀ i x → sym (ap (ψ i) (hmap p i x)) · funext-invⁱ α i x · p i (θ i x)
            ≡ funext-invⁱ β i x

  mor-eq-h-iso : (f g : Mor 𝓧 𝓨) → MorEq f g ≅ MorH f g
  mor-eq-h-iso (f , α) (g , β) = Σ-ap-iso (sym≅ funext-isoⁱ) λ p → lem f g α β p
    where
      lem : (f g : X →ⁱ Y)(α : IsMor 𝓧 𝓨 f)(β : IsMor 𝓧 𝓨 g)(p : f ≡ g)
          → (sym (ap (λ h → ψ ∘ⁱ imap h) p) · α · ap (λ h → h ∘ⁱ θ) p ≡ β)
          ≅ (∀ i x → sym (ap (ψ i) (hmap (funext-invⁱ p) i x))
                   · funext-invⁱ α i x
                   · funext-invⁱ p i (θ i x)
                   ≡ funext-invⁱ β i x)
      lem f .f α β refl = begin
          (α · refl ≡ β)
        ≅⟨ sym≅ (trans≡-iso (left-unit α)) ⟩
          (α ≡ β)
        ≅⟨ iso≡ (sym≅ funext-isoⁱ) ⟩
          (funext-invⁱ α ≡ funext-invⁱ β)
        ≅⟨ sym≅ ((Π-ap-iso refl≅ λ _ → strong-funext-iso) ·≅ strong-funext-iso) ⟩
          (∀ i x → funext-invⁱ α i x ≡ funext-invⁱ β i x)
        ≅⟨ ( Π-ap-iso refl≅ λ i
            → Π-ap-iso refl≅ λ x
            → trans≡-iso (comp i x) ) ⟩
          (∀ i x → sym (ap (ψ i) (hmap (funext-invⁱ p₀) i x))
                 · funext-invⁱ α i x
                 · refl
                 ≡ funext-invⁱ β i x)
        ∎
        where
          open ≅-Reasoning

          p₀ : f ≡ f
          p₀ = refl

          comp : ∀ i x → sym (ap (ψ i) (hmap (funext-invⁱ (refl {x = f})) i x))
                       · funext-invⁱ α i x
                       · refl
                       ≡ funext-invⁱ α i x
          comp i x = ap (λ q → sym (ap (ψ i) q) · funext-invⁱ α i x · refl)
                        (hmap-id f i x)
                   · left-unit (funext-invⁱ α i x)

  eq-mor-iso : {f g : Mor 𝓧 𝓨} → (f ≡ g) ≅ MorH f g
  eq-mor-iso {f , α} {g , β} = begin
      ((f , α) ≡ (g , β))
    ≅⟨ sym≅ Σ-split-iso ⟩
      (Σ (f ≡ g) λ p → subst (IsMor 𝓧 𝓨) p α ≡ β)
    ≅⟨ (Σ-ap-iso refl≅ λ p → trans≡-iso (is-mor-transp p α)) ⟩
      MorEq (f , α) (g , β)
    ≅⟨ mor-eq-h-iso _ _ ⟩
      MorH (f , α) (g , β)
    ∎
    where
      open ≅-Reasoning

module _ {ℓ} (𝓧 : Alg ℓ) where
  private
    X = proj₁ 𝓧; θ = proj₂ 𝓧

    lem : ∀ {ℓ}{A : Set ℓ}{x y z w : A}
        → (p : x ≡ w) (q : y ≡ x) (r : y ≡ z) (s : z ≡ w)
        → p ≡ sym q · r · s → sym r · q · p ≡ s
    lem p refl refl refl α = α

  W-mor-prop : (f g : Mor 𝓦 𝓧) → f ≡ g
  W-mor-prop (f , α) (g , β) = invert (eq-mor-iso 𝓦 𝓧) (p , p-h)
    where
      p : ∀ i x → f i x ≡ g i x
      p i (sup a u)
        = sym (funext-invⁱ α i (a , u))
        · ap (θ i) (ap (_,_ a) (funext (λ b → p (r b) (u b))))
        · funext-invⁱ β i (a , u)

      p-h : ∀ i x
          → sym (ap (θ i) (hmap p i x))
          · funext-invⁱ α i x
          · p i (inW c i x)
          ≡ funext-invⁱ β i x
      p-h i (a , u) = lem (p i (sup a u))
                          (funext-invⁱ α i (a , u)) _
                          (funext-invⁱ β i (a , u))
                          refl

  W-mor : Mor 𝓦 𝓧
  W-mor = fold c θ , funextⁱ (λ i x → fold-β c θ x)

W-initial : ∀ {ℓ} (𝓧 : Alg ℓ) → contr (Mor 𝓦 𝓧)
W-initial 𝓧 = W-mor 𝓧 , W-mor-prop 𝓧 (W-mor 𝓧)

-- special case of the isomorphism above, with better
-- computational behaviour
W-initial-W : contr (Mor 𝓦 𝓦)
W-initial-W = id-mor , W-mor-prop 𝓦 id-mor
  where
    id-mor : Mor 𝓦 𝓦
    id-mor = (λ i x → x) , refl

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
open import Agda.Builtin.Nat using (Nat; suc; zero; _+_)

module test where

data _even : Nat → Set where
  ZERO : zero even
  STEP : ∀ x → x even → suc (suc x) even

proof₁ : suc (suc (suc (suc zero))) even
proof₁ = ?

max_stars_repo_name: ixaxaar/refl

max_issues_repo_name: ixaxaar/refl

max_forks_repo_name: ixaxaar/refl


text:
module Data.Char.Classifier where

open import Data.Char.Classifier.Primitive public

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module Data.Option.Equiv.Id where

import      Lvl
open import Data.Option
open import Data.Option.Functions
open import Data.Option.Equiv
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function
open import Structure.Function.Domain
open import Type

private variable ℓ : Lvl.Level
private variable T A B : Type{ℓ}
private variable f : A → B
private variable o : Option T

instance
  Some-injectivity : Injective {B = Option(T)} (Some)
  Injective.proof Some-injectivity [≡]-intro = [≡]-intro

instance
  Id-Option-extensionality : Extensionality{A = T} ([≡]-equiv)
  Extensionality.cases-inequality Id-Option-extensionality ()

map-injectivity : ⦃ inj-f : Injective(f) ⦄ → Injective(map f)
Injective.proof map-injectivity           {None}   {None}   [≡]-intro = [≡]-intro
Injective.proof (map-injectivity {f = f}) {Some x} {Some y} p         = congruence₁(Some) (injective f(injective(Some) p))

-- TODO: Generalize and move
map-None : (map f o ≡ None) → (o ≡ None)
map-None {o = None} p = [≡]-intro


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

open import Common.Size

-- An abuse of sized types, but as you wish...

data D (i : Size) : Set where
  c  : (j : Size< i) (k : Size< j) (l : Size< k) (m : Size< l) → D m → D i
  c' : (j : Size< i) → D j → D i

works : ∀ i → D i → Set
works i (c j k l m d) = works j (c' k (c' l (c' m d)))
works i (c' j d)      = works j d

test : ∀ i → D i → Set
test i (c j k l m d) = test ? (c' ? (c' ? (c' ? ?)))
test i (c' j d) = ?

-- Should not give a termination error as there is an instantiation
-- of meta variables that gives a terminating function.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
-- Andreas, 2011-04-07

module IrrelevantTelescope where

data Wrap .(A : Set) : Set where
  wrap : A -> Wrap A
-- cannot use A, because it is declared irrelevant

max_stars_repo_name: asr/agda-kanso