text:
-- An ATP conjecture must be used with postulates.

-- This error is detected by TypeChecking.Rules.Decl.

module ATPBadConjecture2 where

data Bool : Set where
  false true : Bool

{-# ATP prove Bool #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
{-# OPTIONS --sized-types #-}

module Automaton.Deterministic.FormalLanguage where

open import Automaton.Deterministic.Finite
open import Automaton.Deterministic
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.List renaming (∅ to [])
open import Functional
import      Lvl
open import Type
open import Type.Size.Finite

private variable ℓ ℓ₁ ℓ₂ ℓₚ : Lvl.Level
private variable Q Q₁ Q₂ State : Type{ℓ}
private variable Σ Σ₁ Σ₂ Alphabet : Type{ℓ}

module Language where
  open import Logic.Propositional
  open import Logic.Predicate
  open import FormalLanguage
  open import FormalLanguage.Equals
  open import Relator.Equals
  open import Relator.Equals.Proofs
  import      Type.Dependent as Type

  -- The language accepted by a DFA.
  -- This is a linguistic interpretation of an automaton, that it is a grammar of the language.
  -- A language accepts the empty word when the start state is a final state.
  -- The language of a suffix is the transition function applied to the start state.
  𝔏 : ∀{s} → DFA{ℓₚ = ℓₚ}(Q)(Σ) → Language(Σ){s}
  Language.accepts-ε   (𝔏(d))   = DFA.isFinal d (DFA.start d)
  Language.suffix-lang (𝔏(d)) c = 𝔏(DFA.transitionedAutomaton d c)

  RegularLanguage : ∀{s}{ℓₚ ℓₑ₁} → Language(Σ) → Type
  RegularLanguage{Σ = Σ}{s = s}{ℓₚ = ℓₚ}{ℓₑ₁ = ℓₑ₁} L = ∃{Obj = Type.Σ(Type{ℓₑ₁})(Q ↦ DFA{ℓₚ = ℓₚ}(Q)(Σ))}(\(Type.intro _ auto) → (𝔏(auto) ≅[ s ]≅ L))

module Proofs where
  open        Language
  open import Logic.Propositional
  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import FormalLanguage
  open        FormalLanguage.Oper hiding (∁_)
  open import Syntax.Transitivity

  -- TODO: Is this wrong?
  -- step-isWordAccepted : ∀{Q}{Σ} → (auto : DFA(Q)(Σ)) → ∀{c}{w} → DFA.isWordAccepted(auto)(c ⊰ w) ≡ DFA.isWordAccepted(Dfa (DFA.δ auto) (DFA.δ(auto)(DFA.q₀(auto))(c)) (DFA.F auto))(w)
  -- step-isWordAccepted auto {c}{[]} = [≡]-intro
  -- step-isWordAccepted auto {c}{w} = congruence₁(DFA.F(auto)) [≡]-intro

  Language-isWordAccepted : ∀{Q}{Σ} → (auto : DFA(Q)(Σ)) → ∀{w} → ({!DFA.isWordAccepted auto w!} ≡ (w ∈? 𝔏(auto)))

  {-
  Language-isWordAccepted : ∀{Q}{Σ} → (auto : DFA(Q)(Σ)) → ∀{w} → (DFA.isWordAccepted(auto)(w) ≡ w ∈? 𝔏(auto))
  Language-isWordAccepted auto {[]}    = [≡]-intro
  Language-isWordAccepted auto {x ⊰ w} =
    DFA.isWordAccepted(auto)(x ⊰ w)                    🝖[ _≡_ ]-[]
    δ̂(q₀)(x ⊰ w) ∈ F                                   🝖[ _≡_ ]-[]
    δ̂(δ(q₀) x) w ∈ F                                   🝖[ _≡_ ]-[ {!Language-isWordAccepted (transitionedAutomaton auto x) {w}!} ]
    DFA.isWordAccepted(transitionedAutomaton auto x) w 🝖[ _≡_ ]-[ Language-isWordAccepted (transitionedAutomaton auto x) {w} ]
    w ∈? Language.suffix-lang(𝔏(auto))(x)              🝖[ _≡_ ]-[]
    (x ⊰ w) ∈? 𝔏(auto)                                 🝖-end
    where
      open DFA(auto)
      open LetterNotation
  -- [≡]-with {!DFA.F(auto)!} (Language-isWordAccepted {Σ = Σ} auto {w})
  -}

  -- Language-isWordAccepted (_)          {[]}    = [≡]-intro
  -- Language-isWordAccepted (Dfa δ q₀ F) {c ⊰ w} = test(Dfa δ q₀ F){c ⊰ w} -- Language-isWordAccepted (Dfa δ (δ(q₀)(c)) F) {w}
    -- DFA.isWordAccepted(auto)(c ⊰ w)
    -- DFA.isWordAccepted(Dfa δ q₀ F)(c ⊰ w)
    -- F(δ̂(q₀)(c ⊰ w))
    -- F(δ̂(δ(q₀)(c))(w))

    -- (c ⊰ w) ∈? (𝔏(auto))
    -- (c ⊰ w) ∈? (𝔏(Dfa δ q₀ F))
    -- w ∈? (Language.suffix-lang(𝔏(Dfa δ q₀ F))(c))
    -- w ∈? (𝔏(Dfa δ (δ(q₀)(c)) F))
{-
  module _ (auto : Deterministic(Q)(Σ)) where
    δ̂-with-[++] : ∀{q : Q}{w₁ w₂ : Word(Σ)} → Deterministic.δ̂(auto)(q)(w₁ ++ w₂) ≡ DFA.δ̂(auto)(DFA.δ̂(auto)(q)(w₁))(w₂)
    δ̂-with-[++] {_}{[]}         = [≡]-intro
    δ̂-with-[++] {q}{a ⊰ w₁}{w₂} = δ̂-with-[++] {Deterministic.δ(auto)(q)(a)}{w₁}{w₂}

    [∁]-δ̂ : ∀{q : Q}{w : Word(Σ)} → DFA.δ̂(∁ auto)(q)(w) ≡ DFA.δ̂(auto)(q)(w)
    [∁]-δ̂ {_}{[]}    = [≡]-intro
    [∁]-δ̂ {q}{a ⊰ w} = [∁]-δ̂ {DFA.δ(∁ auto)(q)(a)}{w}

    [∁]-isWordAccepted : ∀{w} → DFA.isWordAccepted(∁ auto)(w) ≡ !(DFA.isWordAccepted(auto)(w))
    [∁]-isWordAccepted {w} = [≡]-with(x ↦ !(DFA.F(auto)(x))) ([∁]-δ̂{DFA.q₀(auto)}{w})

    -- TODO: Prove ∁ postulates regarding languages before accepting them, because the definition of ∁ for languages might be wrong.
    -- [∁]-language : 𝔏(∁ auto) ≡ Oper.∁(𝔏(auto))
    -- [∁]-language = proof(auto) where
    --   proof : (auto : DFA(Q)(Σ)) → 𝔏(∁ auto) ≡ Oper.∁(𝔏(auto))
    --   proof(Dfa δ q₀ F) = [≡]-substitutionₗ {Lvl.𝟎}{Lvl.𝐒(Lvl.𝟎)} [∁]-language {expr ↦ Lang (! F(q₀)) (c ↦ expr(c))} ([≡]-intro {Lvl.𝟎}{Lvl.𝐒(Lvl.𝟎)})
      -- [≡]-substitution-fnₗ : ∀{T₁ T₂}{x y : T₁ → T₂} → ((c : T₁) → (x(c) ≡ y(c))) → ∀{f : (T₁ → T₂) → TypeN{ℓ₃}} → f(x) ← f(y)
      -- [≡]-substitution-fnₗ [≡]-intro = id?

      -- 𝔏(∁(Dfa δ q₀ F))
      -- = 𝔏(Dfa δ q₀ ((!_) ∘ F))
      -- = Lang ((!_) ∘ F)(q₀)) (c ↦ 𝔏(Dfa δ (δ(q₀)(c)) ((!_) ∘ F)))

      -- Oper.∁(𝔏(Dfa δ q₀ F))
      -- = Lang (! F(q₀)) (c ↦ ∁(𝔏(Dfa δ (δ(q₀)(c)) F)))
      -- = ?

    -- testtt : ∀{auto} → Language.accepts-ε(𝔏{Q}{Σ}(∁ auto)) ≡ ! Language.accepts-ε(𝔏(auto))
    -- testtt : ∀{auto} → Language.accepts-ε(𝔏{Q}{Σ}(∁ auto)) ≡ Language.accepts-ε(Oper.∁ 𝔏(auto))
    -- testtt {_} = [≡]-intro

    -- testtt2 : ∀{auto}{c} → Language.suffix-lang(𝔏(∁ auto))(c) ≡ Oper.∁(Language.suffix-lang(𝔏(auto))(c))
    -- testtt2 : ∀{auto}{c} → Language.suffix-lang(𝔏(∁ auto))(c) ≡ Language.suffix-lang(Oper.∁(𝔏(auto)))(c)
    -- testtt2 : ∀{auto}{c} → Language.suffix-lang(Oper.∁(𝔏{Q}{Σ}(auto)))(c) ≡ Oper.∁(Language.suffix-lang(𝔏(auto))(c))
    -- testtt2 {Dfa δ q₀ F}{_} = [≡]-intro

  module _ (auto : DFA(Q₁)(Σ)) (auto₂ : DFA(Q₂)(Σ)) where
    [⨯]-δ̂ : ∀{q₁ : Q₁}{q₂ : Q₂}{w : Word(Σ)} → DFA.δ̂(auto ⨯ auto₂)(q₁ , q₂)(w) ≡ (DFA.δ̂(auto)(q₁)(w) , DFA.δ̂(auto₂)(q₂)(w))
    [⨯]-δ̂ {_}{_}{[]}      = [≡]-intro
    [⨯]-δ̂ {q₁}{q₂}{a ⊰ w} = [⨯]-δ̂ {DFA.δ(auto)(q₁)(a)}{DFA.δ(auto₂)(q₂)(a)}{w}

    [+]-δ̂ : ∀{q₁ : Q₁}{q₂ : Q₂}{w : Word(Σ)} → DFA.δ̂(auto + auto₂)(q₁ , q₂)(w) ≡ (DFA.δ̂(auto)(q₁)(w) , DFA.δ̂(auto₂)(q₂)(w))
    [+]-δ̂ {_}{_}{[]}      = [≡]-intro
    [+]-δ̂ {q₁}{q₂}{a ⊰ w} = [+]-δ̂ {DFA.δ(auto)(q₁)(a)}{DFA.δ(auto₂)(q₂)(a)}{w}

    -- TODO: δ̂-on-[𝁼]

    [⨯]-isWordAccepted : ∀{w} → DFA.isWordAccepted(auto ⨯ auto₂)(w) ≡ DFA.isWordAccepted(auto)(w) && DFA.isWordAccepted(auto₂)(w)
    [⨯]-isWordAccepted {w} = [≡]-with(DFA.F(auto ⨯ auto₂)) ([⨯]-δ̂{DFA.q₀(auto)}{DFA.q₀(auto₂)}{w})

    [+]-isWordAccepted : ∀{w} → DFA.isWordAccepted(auto + auto₂)(w) ≡ DFA.isWordAccepted(auto)(w) || DFA.isWordAccepted(auto₂)(w)
    [+]-isWordAccepted {w} = [≡]-with(DFA.F(auto + auto₂)) ([+]-δ̂{DFA.q₀(auto)}{DFA.q₀(auto₂)}{w})

    -- TODO: Prove postulates
    postulate [⨯]-language : 𝔏(auto ⨯ auto₂) ≡ 𝔏(auto) ∩ 𝔏(auto₂)
    postulate [+]-language : 𝔏(auto + auto₂) ≡ 𝔏(auto) ∪ 𝔏(auto₂)
-}

ext: agda

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:
module Array.Repr where

open import Array.Base

open import Data.Nat
open import Data.Vec as V
open import Data.Fin using (Fin; zero; suc; raise)
open import Relation.Binary.PropositionalEquality
open import Function

-- This is a function that inductively generates a Vec-based type
-- for the given arguments of Ar.
repr-t : ∀ {a} → (X : Set a) → (n : ℕ) → (s : Vec ℕ n) → Set a
repr-t X zero s = X
repr-t X (suc n) (x ∷ s) = Vec (repr-t X n s) x

a→rt : ∀ {a}{X : Set a}{n s} → Ar X n s → repr-t X n s
a→rt {n = zero}  {s = []} (imap f) = f []
a→rt {n = suc n} {x ∷ s} (imap f) = tabulate λ i → a→rt (imap (λ iv → f (i ∷ iv)))

rt→a : ∀ {a}{X : Set a}{n s} → repr-t X n s → Ar X n s
rt→a {n = zero} {s} x = imap (λ _ → x)
rt→a {n = suc n} {s ∷ _} x = imap λ where
                                (i ∷ iv) → case rt→a (lookup x i) of λ where
                                              (imap f) → f iv

-- This is an inductive type for tensors
data Tensor {a} (X : Set a) : (n : ℕ) → (s : Vec ℕ n) → Set a where
  zz : (x : X) → Tensor X 0 []
  ss : ∀ {n m}{s : Vec ℕ n} → (v : Vec (Tensor X n s) m) → Tensor X (1 + n) (m ∷ s)

-- Ugh, well...  This is big because we have to formulate point-wise equality.
data EqTen {a} (X : Set a) : (n : ℕ) → ∀ {s s₁} → Tensor X n s → Tensor X n s₁ → Set a where
  zeq : ∀ {x} → EqTen X 0 (zz x) (zz x)
  s[] : ∀ {n}{s s₁ : Vec ℕ n}
        → (∀ i → lookup s i ≡ lookup s₁ i)
        → EqTen X (1 + n) (ss {s = s} []) (ss {s = s₁} [])
  s∷ : ∀ {n}{s s₁ : Vec ℕ n}{m}
        → (∀ i → lookup s i ≡ lookup s₁ i)
        → ∀ {x y xs ys}
        → EqTen X n {s = s} {s₁ = s₁} x y
        → EqTen X (1 + n) (ss {m = m} xs) (ss {m = m} ys)
        → EqTen X (1 + n) (ss (x ∷ xs)) (ss (y ∷ ys))

a→tensor : ∀ {a}{X : Set a}{n s} → Ar X n s → Tensor X n s
a→tensor {n = zero} {s = []} (imap f) = zz (f [])
a→tensor {n = suc n}{s = s ∷ _} (imap f) = ss $ tabulate λ i → a→tensor (imap (λ iv → f (i ∷ iv)))

tensor→a : ∀ {a}{X : Set a}{n s} → Tensor X n s → Ar X n s --(lookup s)
tensor→a {s = []} (zz x) = imap (λ _ → x)
tensor→a {s = a ∷ s} (ss v) = imap λ where
                                 (i ∷ iv) → case tensor→a (lookup v i) of λ where
                                               (imap f) → f iv

t→rt : ∀ {a}{X : Set a}{n s} → Tensor X n s → repr-t X n s
t→rt {s = []} (zz x) = x
t→rt {s = x₁ ∷ s} (ss v) = V.map t→rt v

rt→t : ∀ {a}{X : Set a}{n s} → repr-t X n s → Tensor X n s
rt→t {s = []}     x = zz x
rt→t {s = _ ∷ _} x = ss (V.map rt→t x)

module test-repr where
    a : Ar ℕ 2 (3 ∷ 3 ∷ [])
    a = cst 42

    at = (a→tensor a)
    aₜ = tensor→a at

    rt = a→rt a
    a₁ = rt→a {n = 2} {s = 3 ∷ 3 ∷ []} rt

    test₁ : t→rt at ≡ rt
    test₁ = refl

    -- This one is quite tricky to show
    --test₂ : ∀ iv → sel a₁ iv ≡ sel aₜ iv
    --test₂ iv = {!!}

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Cost.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Data.Nat
open import Cubical.Data.Sigma

private
  variable
    ℓ : Level
    A B C : Type ℓ

Cost : (A : Type ℓ) → Type ℓ
Cost A = A × ∥ ℕ ∥

-- To compare two elements of Cost A we only need to look at the first parts
Cost≡ : (x y : Cost A) → x .fst ≡ y .fst → x ≡ y
Cost≡ _ _ = Σ≡Prop λ _ → squash

-- To make it easier to program with Cost A we prove that it forms a
-- monad which counts the number of calls to >>=. We could also turn
-- it into a proper state monad which tracks the cost, but for the
-- programs we write later this simple version suffices
_>>=_ : Cost A → (A → Cost B) → Cost B
(x , m) >>= g with g x
... | (y , n) = (y , map suc (map2 _+_ m n))

return : A → Cost A
return x = (x , ∣ 0 ∣)

-- The monad laws all hold by Cost≡

>>=-return : (f : Cost A) → f >>= return ≡ f
>>=-return f = Cost≡ _ _ refl

return->>= : (a : A) (f : A → Cost B) → return a >>= f ≡ f a
return->>= a f = Cost≡ _ _ refl

>>=-assoc : (f : Cost A) (g : A → Cost B) (h : B → Cost C)
          → (f >>= g) >>= h ≡ f >>= (λ x → g x >>= h)
>>=-assoc f g h = Cost≡ _ _ refl

-- An inefficient version of addition which recurses on both arguments
addBad : ℕ → ℕ → Cost ℕ
addBad 0 0       = return 0
addBad 0 (suc y) = do
  x ← addBad 0 y
  return (suc x)
addBad (suc x) y = do
  z ← addBad x y
  return (suc z)

-- More efficient addition which only recurse on the first argument
add : ℕ → ℕ → Cost ℕ
add 0       y = return y
add (suc x) y = do
  z ← add x y
  return (suc z)

private
  -- addBad x y will do x + y calls
  _ : addBad 3 5 ≡ (8 , ∣ 8 ∣)
  _ = refl

  -- add x y will only do x recursive calls
  _ : add 3 5 ≡ (8 , ∣ 3 ∣)
  _ = refl

-- Despite addBad and add having different cost we can still prove
-- that they are equal functions
add≡addBad : add ≡ addBad
add≡addBad i x y = Cost≡ (add x y) (addBad x y) (rem x y) i
  where
  rem : (x y : ℕ) → add x y .fst ≡ addBad x y .fst
  rem 0 0       = refl
  rem 0 (suc y) = cong suc (rem 0 y)
  rem (suc x) y = cong suc (rem x y)

-- Another example: computing Fibonacci numbers

fib : ℕ → Cost ℕ
fib 0 = return 0
fib 1 = return 1
fib (suc (suc x)) = do
  y ← fib (suc x)
  z ← fib x
  return (y + z)

fibTail : ℕ → Cost ℕ
fibTail 0       = return 0
fibTail (suc x) = fibAux x 1 0
  where
  fibAux : ℕ → ℕ → ℕ → Cost ℕ
  fibAux 0 res _          = return res
  fibAux (suc x) res prev = do
    r ← fibAux x (res + prev) res
    return r

private
  _ : fib 10 ≡ (55 , ∣ 176 ∣)
  _ = refl

  _ : fibTail 10 ≡ (55 , ∣ 9 ∣)
  _ = refl

  _ : fib 20 ≡ (6765 , ∣ 21890 ∣)
  _ = refl

  _ : fibTail 20 ≡ (6765 , ∣ 19 ∣)
  _ = refl

-- Exercise left to the reader: prove that fib and fibTail are equal functions
-- fib≡fibTail : fib ≡ fibTail
-- fib≡fibTail i x = Cost≡ (fib x) (fibTail x) (rem x) i
--   where
--   rem : (x : ℕ) → fib x .fst ≡ fibTail x .fst
--   rem zero = refl
--   rem (suc zero) = refl
--   rem (suc (suc x)) = {!!}

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.MultiSet where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.SIP
open import Cubical.Functions.FunExtEquiv

open import Cubical.Structures.Auto

open import Cubical.Data.Nat
open import Cubical.Data.Sigma

private
  variable
    ℓ : Level

module _ (A : Type ℓ) (Aset : isSet A) where

 CountStructure : Type ℓ → Type ℓ
 CountStructure X = A → X → ℕ

 CountEquivStr = AutoEquivStr CountStructure

 countUnivalentStr : UnivalentStr _ CountEquivStr
 countUnivalentStr = autoUnivalentStr CountStructure

 Count : Type (ℓ-suc ℓ)
 Count = TypeWithStr ℓ CountStructure

 MultiSetStructure : Type ℓ → Type ℓ
 MultiSetStructure X = X × (A → X → X) × (A → X → ℕ)

 MultiSetEquivStr = AutoEquivStr MultiSetStructure

 multiSetUnivalentStr : UnivalentStr _ MultiSetEquivStr
 multiSetUnivalentStr = autoUnivalentStr MultiSetStructure

 MultiSet : Type (ℓ-suc ℓ)
 MultiSet = TypeWithStr ℓ MultiSetStructure


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

open import lib.Basics
open import lib.PathOver
open import lib.PathGroupoid
open import lib.types.Pushout
open import lib.types.Span
open import lib.types.Coproduct
open import lib.types.Sigma

open import Graphs.Definition hiding (π₀ ; π₁)

open import Util.Misc

module Coequalizers.Definition where

Coeq : ∀ {i j} {E : Type i} {V : Type j} → (Graph E V) → Type (lmax i j)
Coeq {E = E} {V = V} (graph π₀ π₁) = Pushout (span V V (V ⊔ E) (⊔-rec (idf V) π₀) (⊔-rec (idf V) π₁))

{- It's often clearer to write coequalizers as V / E, where V and E are the
   vertex and egde types, ommiting the endpoint maps. We implement this idea in
   agda using instance arguments.
-}
module _ {i j : ULevel} where
  _/_ : (V : Type j) (E : Type i) ⦃ gph : Graph E V ⦄ → Type (lmax i j)
  _/_ V E ⦃ gph ⦄ = Coeq gph

  infix 80 _/_

module _ {i j : ULevel} {V : Type i} {E : Type j} {gph : Graph E V} where
  open Graph gph

  cspan : Span
  cspan = span V V (V ⊔ E) (⊔-rec (idf V) π₀) (⊔-rec (idf V) π₁)

  c[_] : V → Coeq gph
  c[ v ] = left v

  quot : (e : E) → c[ π₀ e ] == c[ π₁ e ]
  quot e = glue (inr e) ∙ ! (glue (inl (π₁ e)))

  private
    lemma : {j : ULevel} {X : Coeq gph → Type j} {a b c : Coeq gph} (p : a == b) (q : c == b) {x : X a} {y : X b} {z : X c} → (x == z [ X ↓ (p ∙ ! q) ]) →
            (z == y [ X ↓ q ]) → (x == y [ X ↓ p ])
    lemma idp idp r s = r ∙ s

  module _ {j : ULevel} (X : Coeq gph → Type j) (x : (v : V) → X c[ v ])
    (p : (e : E) → x (π₀ e) == x (π₁ e) [ X ↓ quot e ]) where

    Coeq-elim : (z : Coeq gph) → X z
    Coeq-elim = Pushout-elim x (λ v → transport X (glue (inl v)) (x v)) λ {(inl v) → transp-↓' _ _ _ ; (inr e) → lemma _ _ (p e) (transp-↓' _ _ _)}

    Coeq-β= : (e : E) → apd Coeq-elim (quot e) == p e
    Coeq-β= e =
      apd Coeq-elim (quot e)
        =⟨ apd-∙ Coeq-elim (glue (inr e)) (! (glue (inl (π₁ e)))) ⟩
      apd Coeq-elim (glue (inr e)) ∙ᵈ apd Coeq-elim (! (glue (inl (π₁ e))))
        =⟨ PushoutElim.glue-β _ _ _ _ ∙ᵈᵣ apd Coeq-elim (! (glue (inl (π₁ e)))) ⟩
      lemma _ _ (p e) (transp-↓' _ _ _) ∙ᵈ apd Coeq-elim (! (glue (inl (π₁ e))))
        =⟨ lemma _ _ (p e) (transp-↓' _ _ _) ∙ᵈₗ apd-! Coeq-elim (glue (inl (π₁ e))) ⟩
      lemma _ _ (p e) (transp-↓' _ _ _) ∙ᵈ !ᵈ (apd Coeq-elim (glue (inl (π₁ e))))
        =⟨ lemma _ _ (p e) (transp-↓' _ _ _) ∙ᵈₗ ap !ᵈ (PushoutElim.glue-β x ((λ v → transport X (glue (inl v)) (x v))) _ (inl (π₁ e))) ⟩
      lemma _ _ (p e) (transp-↓' _ _ _) ∙ᵈ !ᵈ (transp-↓' X (glue (inl (π₁ e))) _)
        =⟨ lemma2 _ _ (p e) (transp-↓' X (glue (inl (π₁ e))) _) ⟩
      p e
        =∎
      where
        lemma2 : {a b c : Coeq gph} (p : a == b) (q : c == b) {x : X a} {y : X b} {z : X c} → (r : x == z [ X ↓ (p ∙ ! q) ]) →
               (s : z == y [ X ↓ q ]) → lemma p q r s ∙ᵈ !ᵈ s == r
        lemma2 idp idp idp idp = idp

  Coeq-rec : ∀ {j} {X : Type j} (x : V → X) (p : (e : E) → x (π₀ e) == x (π₁ e)) →
            Coeq gph → X
  Coeq-rec {X = X} x p = Coeq-elim (λ _ → X) x λ e → ↓-cst-in (p e)

  Coeq-rec-β= : ∀ {j} {X : Type j} (x : V → X) (p : (e : E) → x (π₀ e) == x (π₁ e))
    (e : E) → ap (Coeq-rec x p) (quot e) == p e
  Coeq-rec-β= {X = X} x p e = apd=cst-in (Coeq-β= _ _ _ _)

  private
    E' : V → V → Type (lmax i j)
    E' u v = Σ E (λ e → (u == π₀ e) × (π₁ e == v))

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
{-# OPTIONS --sized-types #-}
module SNat.Properties where

open import Size
open import SNat
open import SNat.Order
open import SNat.Order.Properties
open import SNat.Sum

lemma-≅subtyping : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≅ n → m ≅ subtyping n
lemma-≅subtyping z≅z = z≅z
lemma-≅subtyping (s≅s m≅n) = s≅s (lemma-≅subtyping m≅n)

lemma-subtyping≅ : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≅ n → subtyping m ≅ n
lemma-subtyping≅ z≅z = z≅z
lemma-subtyping≅ (s≅s m≅n) = s≅s (lemma-subtyping≅ m≅n)

lemma-subtyping≅subtyping : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≅ n → subtyping m ≅ subtyping n
lemma-subtyping≅subtyping z≅z = z≅z
lemma-subtyping≅subtyping (s≅s m≅n) = s≅s (lemma-subtyping≅subtyping m≅n)

lemma-≤′subtyping : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≤′ n → m ≤′ subtyping n
lemma-≤′subtyping (≤′-eq m≅n) = ≤′-eq (lemma-≅subtyping m≅n)
lemma-≤′subtyping (≤′-step m≤′n) = ≤′-step (lemma-≤′subtyping m≤′n)

lemma-subtyping≤′ : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≤′ n → subtyping m ≤′ n
lemma-subtyping≤′ (≤′-eq m≅n) = ≤′-eq (lemma-subtyping≅ m≅n)
lemma-subtyping≤′ (≤′-step m≤′n) = ≤′-step (lemma-subtyping≤′ m≤′n)

lemma-subtyping≤subtyping : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≤ n → subtyping m ≤ subtyping n
lemma-subtyping≤subtyping (z≤n n) = z≤n (subtyping n)
lemma-subtyping≤subtyping (s≤s m≤n) = s≤s (lemma-subtyping≤subtyping m≤n)

lemma-subtyping≤′subtyping : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≤′ n → subtyping m ≤′ subtyping n
lemma-subtyping≤′subtyping m≤′n = lemma-≤-≤′ (lemma-subtyping≤subtyping (lemma-≤′-≤ m≤′n))

--

lemma-≅-/2 : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≅ n → m /2 ≅ n /2
lemma-≅-/2 z≅z = z≅z
lemma-≅-/2 (s≅s z≅z) = z≅z
lemma-≅-/2 (s≅s (s≅s m≅n)) = s≅s (lemma-subtyping≅subtyping  (lemma-≅-/2 m≅n))

lemma-n/2≤′sn/2 : {ι : Size}(n : SNat {ι}) → n /2 ≤′ (succ n) /2
lemma-n/2≤′sn/2 zero = lemma-z≤′n zero
lemma-n/2≤′sn/2 (succ zero) = lemma-z≤′n (succ zero)
lemma-n/2≤′sn/2 (succ (succ n)) = lemma-s≤′s (lemma-subtyping≤′subtyping (lemma-n/2≤′sn/2 n))

--

lemma-m≤′m+n : (m n : SNat) → m ≤′ (m + n)
lemma-m≤′m+n zero n = lemma-z≤′n n
lemma-m≤′m+n (succ m) n = lemma-s≤′s (lemma-m≤′m+n m n)

lemma-2m≤′m+n+m+n : (m n : SNat) → (m + m) ≤′ ((m + n) + (m + n))
lemma-2m≤′m+n+m+n m n rewrite +-assoc-left (m + n) m n | +-comm (m + n) m | +-assoc-left m m n | +-assoc-right (m + m) n n = lemma-m≤′m+n (m + m) (n + n)

lemma-2m≅2n : {m n : SNat} → m ≅ n →  (m + m) ≅ (n + n)
lemma-2m≅2n z≅z = z≅z
lemma-2m≅2n (s≅s {m = m} {n = n} m≅n) rewrite +-assoc-succ m m | +-assoc-succ n n = s≅s (s≅s (lemma-2m≅2n m≅n))

lemma-2m≤′2n : {m n : SNat} → m ≤′ n →  (m + m) ≤′ (n + n)
lemma-2m≤′2n (≤′-eq m≅n) = ≤′-eq (lemma-2m≅2n m≅n)
lemma-2m≤′2n (≤′-step {n = n} m≤′n) rewrite +-assoc-succ n n = ≤′-step (≤′-step (lemma-2m≤′2n m≤′n))

lemma-n≤′2n : (n : SNat) → n ≤′ (n + n)
lemma-n≤′2n n = lemma-m≤′m+n n n

+-right-monotony-≅ : {m n : SNat}(k : SNat) → m ≅ n → (m + k) ≅ (n + k)
+-right-monotony-≅ k z≅z = refl≅
+-right-monotony-≅ k (s≅s m≅n) = s≅s (+-right-monotony-≅ k m≅n)

+-right-monotony-≤′ : {m n : SNat}(k : SNat) → m ≤′ n → (m + k) ≤′ (n + k)
+-right-monotony-≤′ k (≤′-eq m≅n) = ≤′-eq (+-right-monotony-≅ k m≅n)
+-right-monotony-≤′ k (≤′-step m≤′n) = ≤′-step (+-right-monotony-≤′ k m≤′n)

+-left-monotony-≤′ : {m n : SNat}(k : SNat) → m ≤′ n → (k + m) ≤′ (k + n)
+-left-monotony-≤′ {m} {n} k m≤′n rewrite +-comm k m | +-comm k n = +-right-monotony-≤′ k m≤′n

lemma-4m≤′n+m+n+m : {m n : SNat} → m ≤′ n → ((m + m) + (m + m)) ≤′ ((n + m) + (n + m))
lemma-4m≤′n+m+n+m {m} {n} m≤′n rewrite +-comm n m = lemma-2m≤′2n (+-left-monotony-≤′ m m≤′n)

lemma-n≤′2n/2 : (n : SNat) → n ≤′ (n + n) /2
lemma-n≤′2n/2 zero = ≤′-eq z≅z
lemma-n≤′2n/2 (succ n) rewrite +-assoc-succ (succ n) n = lemma-s≤′s (lemma-≤′subtyping (lemma-n≤′2n/2 n))

lemma-2n/2≤′n : (n : SNat) → (n + n) /2 ≤′ n
lemma-2n/2≤′n zero = refl≤′
lemma-2n/2≤′n (succ n) rewrite +-assoc-succ (succ n) n = lemma-s≤′s (lemma-subtyping≤′ (lemma-2n/2≤′n n))

lemma-n+1≤′2n+2/2 : (n : SNat) → succ n ≤′ (succ (succ (n + n))) /2
lemma-n+1≤′2n+2/2 zero = refl≤′
lemma-n+1≤′2n+2/2 (succ n) rewrite +-assoc-succ (succ n) n = lemma-s≤′s (lemma-≤′subtyping (lemma-s≤′s (lemma-≤′subtyping (lemma-n≤′2n/2 n))))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module FreeTheorems where

open import Level using () renaming (zero to ℓ₀)
open import Data.Nat using (ℕ)
open import Data.List using (List ; map)
open import Data.Vec using (Vec) renaming (map to mapV)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≗_)

import GetTypes

module ListList where
  get-type : Set₁
  get-type = {A : Set} → List A → List A

  open GetTypes.ListList public

  postulate
    free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get

  assume-get : get-type → Get
  assume-get get = record { get = get; free-theorem = free-theorem get }

module VecVec where
  get-type : (ℕ → ℕ) → Set₁
  get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)

  open GetTypes.VecVec public

  postulate
    free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get

  assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
  assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }

module PartialVecVec where
  get-type : {I : Set} → (I → ℕ) → (I → ℕ) → Set₁
  get-type {I} gl₁ gl₂ = {A : Set} {i : I} → Vec A (gl₁ i) → Vec A (gl₂ i)

  open GetTypes.PartialVecVec public

  postulate
    free-theorem : {I : Set} → (gl₁ : I → ℕ) → (gl₂ : I → ℕ) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get

  assume-get : {I : Set} → (gl₁ : I → ℕ) → (gl₂ : I → ℕ) (get : get-type gl₁ gl₂) → Get
  assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get }

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
module SyntaxForOperators where

postulate _+_ : Set → Set → Set

syntax _+_ A B = A ⊎ B

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Formalization.LambdaCalculus.Terms.Combinators where

import      Lvl
open import Data
open import Formalization.LambdaCalculus
open import Numeral.Natural
open import Numeral.Finite
open import Syntax.Number
open import Type

module _ where
  open ExplicitLambdaSyntax

  I = 𝜆 0 0                               -- Identity
  K = 𝜆 0 (𝜆 1 0)                         -- Constant / Left of pair
  𝈲 = 𝜆 0 (𝜆 1 1)                         -- Right of pair
  S = 𝜆 0 (𝜆 1 (𝜆 2 ((0 ← 2) ← (1 ← 2)))) -- General composition
  B = 𝜆 0 (𝜆 1 (𝜆 2 (0 ← (1 ← 2))))       -- Composition
  C = 𝜆 0 (𝜆 1 (𝜆 2 ((0 ← 2) ← 1)))
  W = 𝜆 0 (𝜆 1 ((0 ← 1) ← 1))
  U = 𝜆 0 (0 ← 0)                         -- Self application
  ω = U
  Ω = ω ← ω
  Y = 𝜆 0 ((𝜆 1 (0 ← (1 ← 1))) ← (𝜆 1 (0 ← (1 ← 1))))

-- TODO: Move everything below

open import Formalization.LambdaCalculus.SyntaxTransformation

module Boolean where
  open ExplicitLambdaSyntax

  𝑇 = K
  𝐹 = 𝈲
  If = 𝜆 0 (𝜆 1 (𝜆 2 (0 ← 1 ← 2)))

module Tuple where
  open Boolean
  open ExplicitLambdaSyntax

  Pair = 𝜆 0 (𝜆 1 (𝜆 2 (2 ← 0 ← 1)))
  Projₗ = 𝜆 0 (0 ← var-𝐒 K)
  Projᵣ = 𝜆 0 (0 ← var-𝐒 𝈲)

-- Natural numbers (Church numerals).
module Natural where
  open ExplicitLambdaSyntax

  λ𝟎 = 𝈲
  λ𝐒 = 𝜆 0 (𝜆 1 (𝜆 2 (1 ← (0 ← 1 ← 2))))

  ℕrepr₂ : ℕ → Term(2)
  ℕrepr₂ 𝟎      = 1
  ℕrepr₂ (𝐒(n)) = 0 ← ℕrepr₂ n

  ℕrepr = \n → 𝜆 0 (𝜆 1 (ℕrepr₂ n))

  -- TODO: Prove (λ𝐒 ←ⁿ λ𝟎) β-reduces to (ℕrepr n)

module β-proofs where
  open import Formalization.LambdaCalculus.Semantics.Reduction
  open import Logic.Propositional hiding (_←_)
  open import Logic.Predicate
  open import ReductionSystem
  open import Relator.ReflexiveTransitiveClosure renaming (trans to _🝖_)
  open import Structure.Relator
  open import Structure.Relator.Properties
  open import Type.Dependent

  open ExplicitLambdaSyntax

  private variable n : ℕ
  private variable f g h x y z : Term(n)

  Ω-self-reduces : Ω β⇴ Ω
  Ω-self-reduces = β

  Ω-no-normal-form : ¬ NormalForm(_β⇴_)(Ω)
  Ω-no-normal-form (intro p) = p(Ω-self-reduces)

  -- Also called: Church-Rosser's theorem.
  -- TODO: Seems like the proof can be a bit complicated?
  postulate β-star-confluence : ∀{d} → Confluence(_β⇴*_ {d})

  I-reduction : ((I ← x) β⇴ x)
  I-reduction = β

  K-reduction : ((K ← x ← y) β⇴* x)
  K-reduction {x}{y} = super(cong-applyₗ β) 🝖 super β -- 🝖 substitute₂ₗ(_β⇴*_) (symmetry(_≡_) (substitute-var-𝐒 {0}{x}{y})) refl

  𝈲-reduction : ((𝈲 ← x ← y) β⇴* y)
  𝈲-reduction {x}{y} = super(cong-applyₗ β) 🝖 super β

  B-reduction : ((B ← f ← g ← x) β⇴* (f ← (g ← x)))
  B-reduction = super(cong-applyₗ(cong-applyₗ β)) 🝖 super(cong-applyₗ β) 🝖 super β

  C-reduction : ((C ← f ← g ← x) β⇴* ((f ← x) ← g))
  C-reduction = super(cong-applyₗ(cong-applyₗ β)) 🝖 super(cong-applyₗ β) 🝖 super β

  S-reduction : ((S ← f ← g ← x) β⇴* ((f ← x) ← (g ← x)))
  S-reduction = super(cong-applyₗ(cong-applyₗ β)) 🝖 super(cong-applyₗ β) 🝖 super β

  Y-reduction : ∀{f} → ((Y ← f) β⥈* (f ← (Y ← f)))
  Y-reduction = super([∨]-introᵣ β) 🝖 super([∨]-introᵣ β) 🝖 super([∨]-introₗ(cong-applyᵣ β))

  module _ where
    open Boolean

    If-𝑇-reduction : ((If ← 𝑇 ← x ← y) β⇴* x)
    If-𝑇-reduction = super(cong-applyₗ(cong-applyₗ β)) 🝖 super(cong-applyₗ β) 🝖 super β 🝖 K-reduction

    If-𝐹-reduction : ((If ← 𝐹 ← x ← y) β⇴* y)
    If-𝐹-reduction = super(cong-applyₗ(cong-applyₗ β)) 🝖 super(cong-applyₗ β) 🝖 super β 🝖 𝈲-reduction

  module _ where
    open Tuple

    Pair-projₗ-reduction : (Projₗ ← (Pair ← x ← y)) β⇴* x
    Pair-projₗ-reduction = super β 🝖 super(cong-applyₗ(cong-applyₗ β)) 🝖 super(cong-applyₗ β) 🝖 super β 🝖 super(cong-applyₗ β) 🝖 super β

    Pair-projᵣ-reduction : (Projᵣ ← (Pair ← x ← y)) β⇴* y
    Pair-projᵣ-reduction = super β 🝖 super(cong-applyₗ(cong-applyₗ β)) 🝖 super(cong-applyₗ β) 🝖 super β 🝖 super(cong-applyₗ β) 🝖 super β

  module _ where
    open import Function.Iteration

    open Natural

    {-
    -- λ𝟎 β⇴* ℕrepr 𝟎
    λ𝐒-of-ℕrepr : (λ𝐒 ← ℕrepr(n)) β⇴* ℕrepr(𝐒(n))
    λ𝐒-of-ℕrepr = super {!cong-applyₗ ?!}

    ℕrepr-correctness : (((λ𝐒 ←_) ^ n) λ𝟎) β⇴* (ℕrepr n)
    ℕrepr-correctness {𝟎} = refl
    ℕrepr-correctness {𝐒 n} = super {!!} 🝖 super {!ℕrepr-correctness {n}!}
    -}


text:
open import Common.Prelude

postulate
  foo_bar_ : (b : Bool) → if b then Nat else Bool → Set

Test : Set
Test = foo_bar 5


text:
module AbstractModuleMacro where

import Common.Issue481Parametrized as P

abstract
  module M = P Set

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Properties where

open import Cubical.ZCohomology.Base
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.Data.Empty
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.Nullification
open import Cubical.Data.Int hiding (_+_)
open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec ; elim3 to trElim3)
open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Freudenthal
open import Cubical.HITs.SmashProduct.Base
open import Cubical.Structures.Group

open import Cubical.HITs.Pushout
open import Cubical.Data.Sum.Base
open import Cubical.Data.HomotopyGroup
open import Cubical.Data.Bool hiding (_⊕_)

open import Cubical.ZCohomology.KcompPrelims

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'
    A' : Pointed ℓ

{- Equivalence between cohomology of A and reduced cohomology of (A + 1) -}
coHomRed+1Equiv : (n : ℕ) →
                  (A : Type ℓ) →
                  (coHom n A) ≡ (coHomRed n ((A ⊎ Unit , inr (tt))))
coHomRed+1Equiv zero A i = ∥ helpLemma {C = (Int , pos 0)} i ∥₂
  module coHomRed+1 where
  helpLemma : {C : Pointed ℓ} → ( (A → (typ C)) ≡  ((((A ⊎ Unit) , inr (tt)) →∙ C)))
  helpLemma {C = C} = isoToPath (iso map1
                                     map2
                                     (λ b → linvPf b)
                                     (λ _  → refl))
    where
    map1 : (A → typ C) → ((((A ⊎ Unit) , inr (tt)) →∙ C))
    map1 f = map1' , refl
      module helpmap where
      map1' : A ⊎ Unit → fst C
      map1' (inl x) = f x
      map1' (inr x) = pt C

    map2 : ((((A ⊎ Unit) , inr (tt)) →∙ C)) → (A → typ C)
    map2 (g , pf) x = g (inl x)

    linvPf : (b :((((A ⊎ Unit) , inr (tt)) →∙ C))) →  map1 (map2 b) ≡ b
    linvPf (f , snd) i = (λ x → helper x i)  , λ j → snd ((~ i) ∨ j)
      where
      helper : (x : A ⊎ Unit) → ((helpmap.map1') (map2 (f , snd)) x) ≡ f x
      helper (inl x) = refl
      helper (inr tt) = sym snd

coHomRed+1Equiv (suc n) A i = ∥ coHomRed+1.helpLemma A i {C = ((coHomK (suc n)) , ∣ north ∣)} i ∥₂

-----------

Kn→ΩKn+1 : (n : ℕ) → coHomK n → typ (Ω (coHomK-ptd (suc n)))
Kn→ΩKn+1 n = Iso.fun (Iso2-Kn-ΩKn+1 n)

ΩKn+1→Kn : {n : ℕ} → typ (Ω (coHomK-ptd (suc n))) → coHomK n
ΩKn+1→Kn {n = n} = Iso.inv (Iso2-Kn-ΩKn+1 n)

Kn≃ΩKn+1 : {n : ℕ} → coHomK n ≃ typ (Ω (coHomK-ptd (suc n)))
Kn≃ΩKn+1 {n = n} = isoToEquiv (Iso-Kn-ΩKn+1 n)

---------- Algebra/Group stuff --------

0ₖ : {n : ℕ} → coHomK n
0ₖ {n = zero} = pt (coHomK-ptd 0)
0ₖ {n = suc n} = pt (coHomK-ptd (suc n))

infixr 35 _+ₖ_

_+ₖ_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
_+ₖ_ {n = n} x y  = ΩKn+1→Kn (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y)

-ₖ_ : {n : ℕ} → coHomK n → coHomK n
-ₖ_ {n = n} x = ΩKn+1→Kn (sym (Kn→ΩKn+1 n x))

Kn→ΩKn+10ₖ : (n : ℕ) → Kn→ΩKn+1 n 0ₖ ≡ refl
Kn→ΩKn+10ₖ zero = refl
Kn→ΩKn+10ₖ (suc n) = (λ i → cong ∣_∣ (rCancel (merid north) i))

rUnitₖ : {n : ℕ} (x : coHomK n) → x +ₖ 0ₖ ≡ x
rUnitₖ {n = zero} x = cong ΩKn+1→Kn (sym (rUnit (Kn→ΩKn+1 zero x))) ∙
                      Iso.leftInv (Iso2-Kn-ΩKn+1 zero) x
rUnitₖ {n = suc n} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) x ∙ Kn→ΩKn+10ₖ (suc n) i)) ∙
                       (λ i → ΩKn+1→Kn (rUnit (Kn→ΩKn+1 (suc n) x) (~ i))) ∙
                       Iso.leftInv (Iso2-Kn-ΩKn+1 (suc n)) x

lUnitₖ : {n : ℕ} (x : coHomK n) → 0ₖ +ₖ x ≡ x
lUnitₖ {n = zero} x = cong ΩKn+1→Kn (sym (lUnit (Kn→ΩKn+1 zero x))) ∙
                      Iso.leftInv (Iso2-Kn-ΩKn+1 zero) x
lUnitₖ {n = suc n} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) i ∙ Kn→ΩKn+1 (suc n) x)) ∙
                       (λ i → ΩKn+1→Kn (lUnit (Kn→ΩKn+1 (suc n) x) (~ i))) ∙
                       Iso.leftInv (Iso2-Kn-ΩKn+1 (suc n)) x

rCancelₖ  : {n : ℕ} (x : coHomK n) → x +ₖ (-ₖ x) ≡ 0ₖ
rCancelₖ {n = zero} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+1 zero x ∙ Iso.rightInv (Iso2-Kn-ΩKn+1 zero) (sym (Kn→ΩKn+1 zero x)) i)) ∙
                        cong ΩKn+1→Kn (rCancel (Kn→ΩKn+1 zero x))
rCancelₖ {n = suc zero} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+1 1 x ∙ Iso.rightInv (Iso2-Kn-ΩKn+1 1) (sym (Kn→ΩKn+1 1 x)) i)) ∙
                            cong ΩKn+1→Kn (rCancel (Kn→ΩKn+1 1 x))
rCancelₖ {n = suc (suc n)} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+1 (2 + n) x ∙ Iso.rightInv (Iso2-Kn-ΩKn+1 (2 + n)) (sym (Kn→ΩKn+1 (2 + n) x)) i)) ∙
                               cong ΩKn+1→Kn (rCancel (Kn→ΩKn+1 (2 + n) x)) ∙
                               (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc (suc n)) (~ i))) ∙
                               Iso.leftInv (Iso2-Kn-ΩKn+1 (suc (suc n))) 0ₖ

lCancelₖ : {n : ℕ} (x : coHomK n) → (-ₖ x) +ₖ x  ≡ 0ₖ
lCancelₖ {n = zero} x = (λ i → ΩKn+1→Kn (Iso.rightInv (Iso2-Kn-ΩKn+1 zero) (sym (Kn→ΩKn+1 zero x)) i ∙ Kn→ΩKn+1 zero x)) ∙
                        cong ΩKn+1→Kn (lCancel (Kn→ΩKn+1 zero x))
lCancelₖ {n = suc zero} x = ((λ i → ΩKn+1→Kn (Iso.rightInv (Iso2-Kn-ΩKn+1 1) (sym (Kn→ΩKn+1 1 x)) i ∙ Kn→ΩKn+1 1 x))) ∙
                            cong ΩKn+1→Kn (lCancel (Kn→ΩKn+1 1 x))
lCancelₖ {n = suc (suc n)} x = (λ i → ΩKn+1→Kn (Iso.rightInv (Iso2-Kn-ΩKn+1 (2 + n)) (sym (Kn→ΩKn+1 (2 + n) x)) i ∙ Kn→ΩKn+1 (2 + n) x)) ∙
                               cong ΩKn+1→Kn (lCancel (Kn→ΩKn+1 (2 + n) x)) ∙
                               (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc (suc n)) (~ i))) ∙
                               Iso.leftInv (Iso2-Kn-ΩKn+1 (suc (suc n))) 0ₖ

assocₖ : {n : ℕ} (x y z : coHomK n) → ((x +ₖ y) +ₖ z) ≡ (x +ₖ (y +ₖ z))
assocₖ {n = n} x y z = (λ i → ΩKn+1→Kn (Kn→ΩKn+1 n (ΩKn+1→Kn (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y)) ∙ Kn→ΩKn+1 n z)) ∙
                          (λ i → ΩKn+1→Kn (Iso.rightInv (Iso2-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y) i ∙ Kn→ΩKn+1 n z)) ∙
                          (λ i → ΩKn+1→Kn (assoc (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) (Kn→ΩKn+1 n z) (~ i))) ∙
                          (λ i → ΩKn+1→Kn ((Kn→ΩKn+1 n x) ∙ Iso.rightInv (Iso2-Kn-ΩKn+1 n) ((Kn→ΩKn+1 n y ∙ Kn→ΩKn+1 n z)) (~ i)))

commₖ : {n : ℕ} (x y : coHomK n) → (x +ₖ y) ≡ (y +ₖ x)
commₖ {n = n} x y i = ΩKn+1→Kn (EH-instance (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) i)
  where
  EH-instance : (p q : typ (Ω ((∥ S₊ (suc n) ∥ (2 + (suc n))) , ∣ north ∣))) → p ∙ q ≡ q ∙ p
  EH-instance = transport (λ i → (p q : K-Id n (~ i)) → p ∙ q ≡ q ∙ p)
                          λ p q → Eckmann-Hilton 0 p q
    where
    K-Id : (n : HLevel) → typ (Ω (hLevelTrunc (3 + n) (S₊ (1 + n)) , ∣ north ∣)) ≡ typ ((Ω^ 2) (hLevelTrunc (4 + n) (S₊ (2 + n)) , ∣  north ∣ ))
    K-Id n = (λ i → typ (Ω (isoToPath (Iso2-Kn-ΩKn+1 (suc n)) i , hcomp (λ k → λ { (i = i0) → ∣ north ∣
                                                                                ;  (i = i1) → transportRefl (λ j → ∣ rCancel (merid north) k j ∣) k})
                                                                         (transp (λ j → isoToPath (Iso2-Kn-ΩKn+1 (suc n)) (i ∧ j)) (~ i)  ∣ north ∣))))

-distrₖ : {n : ℕ} → (x y : coHomK n) → -ₖ (x +ₖ y) ≡ (-ₖ x) +ₖ (-ₖ y)
-distrₖ {n = n} x y = (λ i → ΩKn+1→Kn (sym (Kn→ΩKn+1 n (ΩKn+1→Kn (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y))))) ∙
                      (λ i → ΩKn+1→Kn (sym (Iso.rightInv (Iso2-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y) i))) ∙
                      (λ i → ΩKn+1→Kn (symDistr (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) i)) ∙
                      (λ i → ΩKn+1→Kn (Iso.rightInv (Iso2-Kn-ΩKn+1 n) (sym (Kn→ΩKn+1 n y)) (~ i) ∙ (Iso.rightInv (Iso2-Kn-ΩKn+1 n) (sym (Kn→ΩKn+1 n x)) (~ i)))) ∙
                      commₖ (-ₖ y) (-ₖ x)

---- Group structure of cohomology groups ---

private
  § : isSet ∥ A ∥₂
  § = setTruncIsSet

_+ₕ_ : {n : ℕ} → coHom n A → coHom n A → coHom n A
_+ₕ_ = sElim2 (λ _ _ → §) λ a b → ∣ (λ x → a x +ₖ b x) ∣₂

-ₕ  : {n : ℕ} → coHom n A → coHom n A
-ₕ  = sRec § λ a → ∣ (λ x → -ₖ a x) ∣₂

0ₕ : {n : ℕ} → coHom n A
0ₕ = ∣ (λ _ → 0ₖ) ∣₂

rUnitₕ : {n : ℕ} (x : coHom n A) → x +ₕ 0ₕ ≡ x
rUnitₕ  = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                λ a i → ∣ funExt (λ x → rUnitₖ (a x)) i ∣₂

lUnitₕ : {n : ℕ} (x : coHom n A) → 0ₕ +ₕ x ≡ x
lUnitₕ = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
               λ a i → ∣ funExt (λ x → lUnitₖ (a x)) i ∣₂

rCancelₕ : {n : ℕ} (x : coHom n A) → x +ₕ (-ₕ x) ≡ 0ₕ
rCancelₕ = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                 λ a i → ∣ funExt (λ x → rCancelₖ (a x)) i ∣₂

lCancelₕ : {n : ℕ} (x : coHom n A) → (-ₕ x) +ₕ x  ≡ 0ₕ
lCancelₕ = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                 λ a i → ∣ funExt (λ x → lCancelₖ (a x)) i ∣₂

assocₕ : {n : ℕ} (x y z : coHom n A) → ((x +ₕ y) +ₕ z) ≡ (x +ₕ (y +ₕ z))
assocₕ = elim3 (λ _ _ _ → isOfHLevelPath 1 (§ _ _))
               λ a b c i → ∣ funExt (λ x → assocₖ (a x) (b x) (c x)) i ∣₂

commₕ : {n : ℕ} (x y : coHom n A) → (x +ₕ y) ≡ (y +ₕ x)
commₕ {n = n} = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                       λ a b i → ∣ funExt (λ x → commₖ (a x) (b x)) i ∣₂

---- Group structure of reduced cohomology groups (in progress - might need K to compute properly first) ---

+ₕ∙ : {A : Pointed ℓ} (n : ℕ) → coHomRed n A → coHomRed n A → coHomRed n A
+ₕ∙ zero = sElim2 (λ _ _ → §) λ { (a , pa) (b , pb) → ∣ (λ x → a x +ₖ b x) , (λ i → (pa i +ₖ pb i)) ∣₂ }
+ₕ∙ (suc n) = sElim2 (λ _ _ → §) λ { (a , pa) (b , pb) → ∣ (λ x → a x +ₖ b x) , (λ i → pa i +ₖ pb i) ∙ lUnitₖ 0ₖ ∣₂ }

-ₕ∙  : {A : Pointed ℓ} (n : ℕ) → coHomRed n A → coHomRed n A
-ₕ∙ zero = sRec § λ {(a , pt) → ∣ (λ x → -ₖ a x ) , (λ i → -ₖ (pt i)) ∣₂}
-ₕ∙ (suc zero) = sRec § λ {(a , pt) → ∣ (λ x → -ₖ a x ) , (λ i → -ₖ (pt i)) ∙ (λ i → ΩKn+1→Kn (sym (Kn→ΩKn+10ₖ (suc zero) i))) ∣₂}
-ₕ∙ (suc (suc n)) = sRec § λ {(a , pt) → ∣ (λ x → -ₖ a x ) , (λ i → -ₖ (pt i)) ∙
                                                              (λ i → ΩKn+1→Kn (sym (Kn→ΩKn+10ₖ (suc (suc n)) i))) ∙
                                                              (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc (suc n)) (~ i))) ∙
                                                              Iso.leftInv (Iso2-Kn-ΩKn+1 (suc (suc n))) ∣ north ∣ ∣₂}

0ₕ∙ : {A : Pointed ℓ} (n : ℕ) → coHomRed n A
0ₕ∙ zero = ∣ (λ _ → 0ₖ) , refl ∣₂
0ₕ∙ (suc n) = ∣ (λ _ → 0ₖ) , refl ∣₂


text:
------------------------------------------------------------------------
-- Some partiality algebra properties
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

open import Prelude hiding (T)

open import Partiality-algebra as PA hiding (id; _∘_)

module Partiality-algebra.Properties
  {a p q} {A : Type a} (P : Partiality-algebra p q A) where

open import Equality.Propositional.Cubical

open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
open import Nat equality-with-J as Nat

open Partiality-algebra P

------------------------------------------------------------------------
-- Some predicates

-- A termination predicate: x ⇓ y means that x terminates with the
-- value y.

infix 4 _⇓_ _⇑

_⇓_ : T → A → Type p
x ⇓ y = x ≡ now y

-- A non-termination predicate.

_⇑ : T → Type p
x ⇑ = x ≡ never

------------------------------------------------------------------------
-- Preorder reasoning combinators

infix  -1 finally-⊑
infix  -1 _■
infixr -2 _⊑⟨_⟩_ _⊑⟨⟩_ _≡⟨_⟩⊑_

_⊑⟨_⟩_ : (x {y z} : T) → x ⊑ y → y ⊑ z → x ⊑ z
_ ⊑⟨ x⊑y ⟩ y⊑z = ⊑-trans x⊑y y⊑z

_⊑⟨⟩_ : (x {y} : T) → x ⊑ y → x ⊑ y
_ ⊑⟨⟩ x⊑y = x⊑y

_≡⟨_⟩⊑_ : (x {y z} : T) → x ≡ y →
          y ⊑ z → x ⊑ z
_ ≡⟨ refl ⟩⊑ y⊑z = y⊑z

_■ : (x : T) → x ⊑ x
x ■ = ⊑-refl x

finally-⊑ : (x y : T) → x ⊑ y → x ⊑ y
finally-⊑ _ _ x⊑y = x⊑y

syntax finally-⊑ x y x⊑y = x ⊑⟨ x⊑y ⟩■ y ■

------------------------------------------------------------------------
-- Some simple lemmas

-- If every element in one increasing sequence is bounded by some
-- element in another, then the least upper bound of the first
-- sequence is bounded by the least upper bound of the second one.

⊑→⨆⊑⨆ : ∀ {s₁ s₂} {f : ℕ → ℕ} →
        (∀ n → s₁ [ n ] ⊑ s₂ [ f n ]) → ⨆ s₁ ⊑ ⨆ s₂
⊑→⨆⊑⨆ {s₁} {s₂} {f} s₁⊑s₂ =
  least-upper-bound _ _ λ n →
    s₁ [ n ]    ⊑⟨ s₁⊑s₂ n ⟩
    s₂ [ f n ]  ⊑⟨ upper-bound _ _ ⟩■
    ⨆ s₂        ■

-- A variant of the previous lemma.

∃⊑→⨆⊑⨆ : ∀ {s₁ s₂} →
         (∀ m → ∃ λ n → s₁ [ m ] ⊑ s₂ [ n ]) → ⨆ s₁ ⊑ ⨆ s₂
∃⊑→⨆⊑⨆ s₁⊑s₂ = ⊑→⨆⊑⨆ (proj₂ ∘ s₁⊑s₂)

-- ⨆ is monotone.

⨆-mono : {s₁ s₂ : Increasing-sequence} →
         (∀ n → s₁ [ n ] ⊑ s₂ [ n ]) → ⨆ s₁ ⊑ ⨆ s₂
⨆-mono = ⊑→⨆⊑⨆

-- Later elements in an increasing sequence are larger.

later-larger : (s : Increasing-sequence) →
               ∀ {m n} → m ≤ n → s [ m ] ⊑ s [ n ]
later-larger s {m} (≤-refl′ refl)           = s [ m ] ■
later-larger s {m} (≤-step′ {k = n} p refl) =
  s [ m ]      ⊑⟨ later-larger s p ⟩
  s [ n ]      ⊑⟨ increasing s n ⟩■
  s [ suc n ]  ■

-- If the final elements of an increasing sequence have an upper
-- bound, then all elements have this upper bound.

upper-bound-≤→upper-bound :
  ∀ (s : Increasing-sequence) {m x} →
  (∀ n → m ≤ n → s [ n ] ⊑ x) →
  ∀ n → s [ n ] ⊑ x
upper-bound-≤→upper-bound s {m} {x} is-ub n with Nat.total m n
... | inj₁ m≤n = is-ub n m≤n
... | inj₂ n≤m =
  s [ n ]  ⊑⟨ later-larger s n≤m ⟩
  s [ m ]  ⊑⟨ is-ub m ≤-refl ⟩■
  x        ■

-- Only never is smaller than or equal to never.

only-never-⊑-never : {x : T} → x ⊑ never → x ≡ never
only-never-⊑-never x⊑never = antisymmetry x⊑never (never⊑ _)

------------------------------------------------------------------------
-- Tails

-- The tail of an increasing sequence.

tailˢ : Increasing-sequence → Increasing-sequence
tailˢ = Σ-map (_∘ suc) (_∘ suc)

-- The tail has the same least upper bound as the full sequence.

⨆tail≡⨆ : ∀ s → ⨆ (tailˢ s) ≡ ⨆ s
⨆tail≡⨆ s = antisymmetry
  (⊑→⨆⊑⨆ λ n → s [ suc n ]  ⊑⟨⟩
               s [ suc n ]  ■)
  (⨆-mono λ n → s [ n ]      ⊑⟨ increasing s n ⟩■
                s [ suc n ]  ■)

------------------------------------------------------------------------
-- Constant sequences

-- One way to form a constant sequence.

constˢ : T → Increasing-sequence
constˢ x = const x , const (⊑-refl x)

-- The least upper bound of a constant sequence is equal to the
-- value in the sequence.

⨆-const : ∀ {x : T} {inc} → ⨆ (const x , inc) ≡ x
⨆-const {x} =
  antisymmetry (least-upper-bound _ _ (λ _ → ⊑-refl x))
               (upper-bound _ 0)

------------------------------------------------------------------------
-- Box and diamond

-- Box.

□ : ∀ {ℓ} → (A → Type ℓ) → T → Type (a ⊔ p ⊔ ℓ)
□ P x = ∀ y → x ⇓ y → P y

-- Diamond.

◇ : ∀ {ℓ} → (A → Type ℓ) → T → Type (a ⊔ p ⊔ ℓ)
◇ P x = ∥ (∃ λ y → x ⇓ y × P y) ∥

-- All h-levels are closed under box.

□-closure : ∀ {ℓ} {P : A → Type ℓ} {x} n →
            (∀ x → H-level n (P x)) → H-level n (□ P x)
□-closure n h =
  Π-closure ext n λ y →
  Π-closure ext n λ _ →
  h y

-- A "constructor" for ◇. For more "constructors" for □ and ◇, see
-- Partiality-monad.Inductive.Alternative-order.

◇-now :
  ∀ {ℓ} {P : A → Type ℓ} →
  ∀ {x} → P x → ◇ P (now x)
◇-now p = ∣ _ , refl , p ∣

------------------------------------------------------------------------
-- An alternative characterisation of _⊑_

-- A relation which, /for the partiality monad/, is pointwise
-- equivalent to _⊑_. See
-- Partiality-monad.Inductive.Alternative-order.≼≃⊑ for the proof.

_≼_ : T → T → Type (a ⊔ p)
x ≼ y = ∀ z → x ⇓ z → y ⇓ z

-- _≼_ is propositional.

≼-propositional : ∀ {x y} → Is-proposition (x ≼ y)
≼-propositional =
  Π-closure ext 1 λ _ →
  Π-closure ext 1 λ _ →
  T-is-set

-- _≼_ is transitive.

≼-trans : ∀ {x y z} → x ≼ y → y ≼ z → x ≼ z
≼-trans {x} {y} {z} x≼y y≼z u =
  x ⇓ u  ↝⟨ x≼y u ⟩
  y ⇓ u  ↝⟨ y≼z u ⟩□
  z ⇓ u  □

------------------------------------------------------------------------
-- Combinators that can be used to prove that two least upper bounds
-- are equal

-- For an example of how these combinators can be used, see
-- Lambda.Partiality-monad.Inductive.Compiler-correctness.

-- A relation between sequences.

infix 4 _≳[_]_

record _≳[_]_ (s₁ : ℕ → T) (n : ℕ) (s₂ : ℕ → T) : Type p where
  constructor wrap
  field
    run : ∃ λ k → s₁ (k + n) ≡ s₂ n

open _≳[_]_ public

steps-≳ : ∀ {s₁ n s₂} → s₁ ≳[ n ] s₂ → ℕ
steps-≳ = proj₁ ∘ run

-- If two increasing sequences are related in a certain way, then
-- their least upper bounds are equal.

≳→⨆≡⨆ : ∀ {s₁ s₂} k →
        (∀ {n} → proj₁ s₁ ≳[ n ] proj₁ s₂ ∘ (k +_)) →
        ⨆ s₁ ≡ ⨆ s₂
≳→⨆≡⨆ {s₁} {s₂} k s₁≳s₂ = antisymmetry
  (⊑→⨆⊑⨆ λ n →
     let m , s₁[m+n]≡s₂[k+n] = run s₁≳s₂ in

     s₁ [ n ]      ⊑⟨ later-larger s₁ (m≤n+m _ m) ⟩
     s₁ [ m + n ]  ≡⟨ s₁[m+n]≡s₂[k+n] ⟩⊑
     s₂ [ k + n ]  ■)
  (⊑→⨆⊑⨆ λ n →
     let m , s₁[m+n]≡s₂[k+n] = run s₁≳s₂ in

     s₂ [ n ]      ⊑⟨ later-larger s₂ (m≤n+m _ k) ⟩
     s₂ [ k + n ]  ≡⟨ sym s₁[m+n]≡s₂[k+n] ⟩⊑
     s₁ [ m + n ]  ■)

-- Preorder-like reasoning combinators.

infix  -1 _∎≳
infixr -2 _≳⟨⟩_ trans-≳ trans-≡≳ trans-∀≡≳

_∎≳ : ∀ s {n} → s ≳[ n ] s
run (_ ∎≳) = 0 , refl

_≳⟨⟩_ : ∀ {n} s₁ {s₂} → s₁ ≳[ n ] s₂ → s₁ ≳[ n ] s₂
_ ≳⟨⟩ s₁≳s₂ = s₁≳s₂

trans-≳ : ∀ {n} s₁ {s₂ s₃}
          (s₂≳s₃ : s₂ ≳[ n ] s₃) →
          s₁ ≳[ steps-≳ s₂≳s₃ + n ] s₂ →
          s₁ ≳[ n ] s₃
run (trans-≳ {n} s₁ {s₂} {s₃} s₂≳s₃ s₁≳s₂) =
  let k₁ , eq₁ = run s₂≳s₃
      k₂ , eq₂ = run s₁≳s₂
  in
    k₂ + k₁
  , (s₁ ((k₂ + k₁) + n)  ≡⟨ cong s₁ (sym $ +-assoc k₂) ⟩
     s₁ (k₂ + (k₁ + n))  ≡⟨ eq₂ ⟩
     s₂       (k₁ + n)   ≡⟨ eq₁ ⟩∎
     s₃             n    ∎)

trans-≡≳ : ∀ {n} s₁ {s₂ s₃}
           (s₂≳s₃ : s₂ ≳[ n ] s₃) →
           s₁ (steps-≳ s₂≳s₃ + n) ≡ s₂ (steps-≳ s₂≳s₃ + n) →
           s₁ ≳[ n ] s₃
trans-≡≳ _ s₂≳s₃ s₁≡s₂ = _ ≳⟨ wrap (0 , s₁≡s₂) ⟩ s₂≳s₃

trans-∀≡≳ : ∀ {n} s₁ {s₂ s₃} →
            s₂ ≳[ n ] s₃ →
            (∀ n → s₁ n ≡ s₂ n) →
            s₁ ≳[ n ] s₃
trans-∀≡≳ _ s₂≳s₃ s₁≡s₂ = trans-≡≳ _ s₂≳s₃ (s₁≡s₂ _)

syntax trans-≳   s₁ s₂≳s₃ s₁≳s₂ = s₁ ≳⟨  s₁≳s₂ ⟩  s₂≳s₃
syntax trans-≡≳  s₁ s₂≳s₃ s₁≡s₂ = s₁ ≡⟨  s₁≡s₂ ⟩≳ s₂≳s₃
syntax trans-∀≡≳ s₁ s₂≳s₃ s₁≡s₂ = s₁ ∀≡⟨ s₁≡s₂ ⟩≳ s₂≳s₃

-- Some "stepping" combinators.

later : ∀ {n s₁ s₂} →
        s₁ ∘ suc ≳[ n ] s₂ ∘ suc → s₁ ≳[ suc n ] s₂
run (later {n} {s₁} {s₂} s₁≳s₂) =
  let k , eq = run s₁≳s₂
  in
    k
  , (s₁ (k + suc n)  ≡⟨ cong s₁ (sym $ suc+≡+suc k) ⟩
     s₁ (suc k + n)  ≡⟨ eq ⟩∎
     s₂ (suc n)      ∎)

earlier : ∀ {n s₁ s₂} →
          s₁ ≳[ suc n ] s₂ → s₁ ∘ suc ≳[ n ] s₂ ∘ suc
run (earlier {n} {s₁} {s₂} s₁≳s₂) =
  let k , eq = run s₁≳s₂
  in
    k
  , (s₁ (suc k + n)  ≡⟨ cong s₁ (suc+≡+suc k) ⟩
     s₁ (k + suc n)  ≡⟨ eq ⟩∎
     s₂ (suc n)      ∎)

laterˡ : ∀ {n s₁ s₂} → s₁ ∘ suc ≳[ n ] s₂ → s₁ ≳[ n ] s₂
run (laterˡ s₁≳s₂) = Σ-map suc id (run s₁≳s₂)

step⇓ : ∀ {n s} → s ≳[ n ] s ∘ suc
step⇓ = laterˡ (_ ∎≳)

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
-- You can use _ in a binding position in notation.
module WildcardNotation where

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : ∀ x → B x → Σ A B

syntax Σ A (λ _ → B) = A × B

swap : ∀ {A B} → A × B → B × A
swap (x , y) = y , x

syntax compose (λ _ → x) (λ _ → y) = x instead-of y
compose : {A B C : Set} → (B → C) → (A → B) → (A → C)
compose f g = λ x → f (g x)

open import Common.Prelude
open import Common.Equality

thm₁ : swap (1 , 2) ≡ (2 , 1)
thm₁ = refl

thm₂ : (a b : Nat) → (5 instead-of a) b ≡ 5
thm₂ a b = refl


text:
module Data.Either.Proofs where

import      Lvl
open import Data
open import Data.Either as Either
open import Data.Either.Equiv
open import Function.Equals
open import Functional
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ ℓₑ₅ ℓₑ₆ : Lvl.Level
private variable A B C A₁ A₂ A₃ B₁ B₂ B₃ : Type{ℓ}

module _ ⦃ equiv-C : Equiv{ℓₑ₃}(C) ⦄ where
  map1-values : {f : A → C}{g : B → C}{e : A ‖ B} → (∃(x ↦ map1 f g e ≡ f(x)) ∨ ∃(x ↦ map1 f g e ≡ g(x)))
  map1-values {e = Either.Left  a} = [∨]-introₗ ([∃]-intro a ⦃ reflexivity(_≡_) ⦄)
  map1-values {e = Either.Right b} = [∨]-introᵣ ([∃]-intro b ⦃ reflexivity(_≡_) ⦄)

module _ where
  module _ ⦃ _ : Equiv{ℓₑ}(A ‖ B) ⦄ where
    mapLeft-preserves-id : Names.Preserving₀ ⦃ [⊜]-equiv ⦄ (mapLeft {A₁ = A}{B = B})(id)(id)
    _⊜_.proof (mapLeft-preserves-id) {Left  x} = reflexivity(_≡_)
    _⊜_.proof (mapLeft-preserves-id) {Right x} = reflexivity(_≡_)

    mapRight-preserves-id : Names.Preserving₀ ⦃ [⊜]-equiv ⦄ (mapRight {A = A}{B₁ = B})(id)(id)
    _⊜_.proof (mapRight-preserves-id) {Left  x} = reflexivity(_≡_)
    _⊜_.proof (mapRight-preserves-id) {Right x} = reflexivity(_≡_)

    swap-involution : (Either.swap ∘ Either.swap {A = A}{B = B} ⊜ id)
    _⊜_.proof swap-involution {Left  _} = reflexivity(_≡_)
    _⊜_.proof swap-involution {Right _} = reflexivity(_≡_)

  module _ ⦃ _ : let _ = A₁ ; _ = A₂ ; _ = A₃ ; _ = B in Equiv{ℓₑ}(A₃ ‖ B) ⦄ {f : A₂ → A₃} {g : A₁ → A₂} where
    mapLeft-preserves-[∘] : (mapLeft(f ∘ g) ⊜ (mapLeft f) ∘ (mapLeft g))
    _⊜_.proof mapLeft-preserves-[∘] {Left  x} = reflexivity(_≡_)
    _⊜_.proof mapLeft-preserves-[∘] {Right x} = reflexivity(_≡_)

  module _ ⦃ _ : let _ = A ; _ = B₁ ; _ = B₂ ; _ = B₃ in Equiv{ℓₑ}(A ‖ B₃) ⦄ {f : B₂ → B₃} {g : B₁ → B₂} where
    mapRight-preserves-[∘] : (mapRight(f ∘ g) ⊜ (mapRight f) ∘ (mapRight g))
    _⊜_.proof mapRight-preserves-[∘] {Left  x} = reflexivity(_≡_)
    _⊜_.proof mapRight-preserves-[∘] {Right x} = reflexivity(_≡_)

  module _ ⦃ _ : Equiv{ℓₑ}(A ‖ B) ⦄ where
    map-preserves-id : (map id id ⊜ id)
    _⊜_.proof map-preserves-id {Left  x} = reflexivity(_≡_)
    _⊜_.proof map-preserves-id {Right x} = reflexivity(_≡_)

module _
  ⦃ equiv-A₁ : Equiv{ℓₑ₁}(A₁) ⦄
  ⦃ equiv-B₁ : Equiv{ℓₑ₂}(B₁) ⦄
  ⦃ equiv-A₂ : Equiv{ℓₑ₃}(A₂) ⦄
  ⦃ equiv-B₂ : Equiv{ℓₑ₄}(B₂) ⦄
  ⦃ equiv-AB₁ : Equiv{ℓₑ₅}(A₁ ‖ B₁) ⦄ ⦃ ext-AB₁ : Extensionality(equiv-AB₁) ⦄
  ⦃ equiv-AB₂ : Equiv{ℓₑ₆}(A₂ ‖ B₂) ⦄ ⦃ ext-AB₂ : Extensionality(equiv-AB₂) ⦄
  {f : A₁ → A₂}
  {g : B₁ → B₂}
  where

  open Extensionality ⦃ … ⦄

  instance
    map-function : BinaryOperator(Either.map {A₁ = A₁}{A₂ = A₂}{B₁ = B₁}{B₂ = B₂})
    _⊜_.proof (BinaryOperator.congruence map-function (intro p₁) (intro p₂)) {Left  _} = congruence₁(Left)  p₁
    _⊜_.proof (BinaryOperator.congruence map-function (intro p₁) (intro p₂)) {Right _} = congruence₁(Right) p₂

  instance
    map-injective : ⦃ inj-f : Injective(f) ⦄ → ⦃ inj-g : Injective(g) ⦄ → Injective(Either.map f g)
    Injective.proof map-injective {Left x}  {Left  y} p = congruence₁(Either.Left)  (injective(f) (injective(Either.Left)  p))
    Injective.proof map-injective {Left x}  {Right y} p with () ← Left-Right-inequality p
    Injective.proof map-injective {Right x} {Left  y} p with () ← Left-Right-inequality (symmetry(_≡_) p)
    Injective.proof map-injective {Right x} {Right y} p = congruence₁(Either.Right) (injective(g) (injective(Either.Right) p))

  instance
    map-surjective : ⦃ surj-f : Surjective(f) ⦄ → ⦃ surj-g : Surjective(g) ⦄ → Surjective(Either.map f g)
    Surjective.proof map-surjective {Left  y} with [∃]-intro x ⦃ p ⦄ ← surjective(f){y} = [∃]-intro (Left  x) ⦃ congruence₁(Left)  p ⦄
    Surjective.proof map-surjective {Right y} with [∃]-intro x ⦃ p ⦄ ← surjective(g){y} = [∃]-intro (Right x) ⦃ congruence₁(Right) p ⦄

  instance
    map-bijective : ⦃ bij-f : Bijective(f) ⦄ → ⦃ bij-g : Bijective(g) ⦄ → Bijective(Either.map f g)
    map-bijective = injective-surjective-to-bijective(Either.map f g) where
      instance
        inj-f : Injective(f)
        inj-f = bijective-to-injective(f)
      instance
        inj-g : Injective(g)
        inj-g = bijective-to-injective(g)
      instance
        surj-f : Surjective(f)
        surj-f = bijective-to-surjective(f)
      instance
        surj-g : Surjective(g)
        surj-g = bijective-to-surjective(g)

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-AB : Equiv{ℓₑ}(A ‖ B) ⦄ ⦃ ext-AB : Extensionality(equiv-AB) ⦄
  where

  map-mapLeft-mapRight : ∀{f : B → A}{g : C → B} → (map f g ≡ mapLeft f ∘ mapRight g)
  _⊜_.proof (map-mapLeft-mapRight) {[∨]-introₗ _} = reflexivity(_≡_)
  _⊜_.proof (map-mapLeft-mapRight) {[∨]-introᵣ _} = reflexivity(_≡_)

  instance
    map1-function : ⦃ equiv-C : Equiv{ℓₑ₃}(C) ⦄ → BinaryOperator{B = (A ‖ B) → C}(map1)
    _⊜_.proof (BinaryOperator.congruence map1-function (intro p₁) (intro p₂)) {Left  _} = p₁
    _⊜_.proof (BinaryOperator.congruence map1-function (intro p₁) (intro p₂)) {Right _} = p₂


text:
{-# OPTIONS --guardedness #-}

open import Agda.Builtin.Equality
open import Data.Empty

-- base : Size
-- next : Delay → Size
-- later : Size → Delay
record Delay : Set
data Size : Set

record Delay where
  coinductive
  constructor later
  field now : Size
open Delay

data Size where
  base : Size
  next : Delay → Size

-- ω ≡ next ω' ≡ next (later (next ω')) ≡ ...
--   ≡ next (later ω) ≡ ...
ω : Size
ω = next ω' -- next (later (next ω))
  where
  ω' : Delay
  -- ω' = later (next ω')
  now ω' = next ω'

next' : Size → Size
next' s = next (later s)

{-# ETA Delay #-}
lim : ω ≡ next' ω
lim = refl

data FSize : Size → Set where
  fbase : FSize base
  fnext : {d : Delay} → FSize (now d) → FSize (next d)

inf : FSize ω → ⊥
inf (fnext s) = inf s

data Nat : Size → Set where
  zero : (s : Size) → Nat (next' s)
  succ : (s : Size) → Nat s → Nat (next' s)

shift : ∀ s → Nat s → Nat (next' s)
shift _ (zero s) = zero (next' s)
shift _ (succ s n) = succ (next' s) (shift s n)

postulate blocker : ∀ s → Nat s → Nat s

-- The guard condition passes due to recursion on n,
-- not due to recusion on the size, since it doesn't know that
-- `now s` is in fact smaller than s without using Agda's sized types
-- (or the old version of coinductive types with musical notation).
zeroify : ∀ s → Nat s → Nat s
zeroify base ()
zeroify (next s) (zero _) = zero _
zeroify (next s) (succ _ n) = shift (now s) (zeroify (now s) (blocker (now s) n))

max_stars_repo_name: ionathanch/msc-thesis

max_issues_repo_name: ionathanch/msc-thesis

max_forks_repo_name: ionathanch/msc-thesis


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

open import BaseOver

module Spaces.FlatteningTypes {i j k}
  (A : Set i) (B : Set j) (f g : B → A)
  (C : A → Set k) (D : (b : B) → C (f b) ≃ C (g b)) where

ijk = max i (max j k)

module BaseHIT where
  {-
    data W : Set where
      cc : A → W
      pp : (b : B) → cc (f b) ≡ cc (g b)
  -}

  private
    data #W : Set ijk where
      #cc : A → #W

  W : Set ijk
  W = #W

  cc : A → W
  cc = #cc

  postulate
    pp : (b : B) → cc (f b) ≡ cc (g b)

  W-rec : ∀ {ℓ} (P : W → Set ℓ) (cc* : (a : A) → P (cc a))
    (pp* : (b : B) → cc* (f b) == cc* (g b) [ P ↓ pp b ])
    → ((w : W) → P w)
  W-rec P cc* pp* (#cc a) = cc* a

  postulate
    W-rec-β : ∀ {ℓ} (P : W → Set ℓ) (cc* : (a : A) → P (cc a))
      (pp* : (b : B) → cc* (f b) == cc* (g b) [ P ↓ pp b ])
      → ((b : B) → apd (W-rec P cc* pp*) (pp b) ≡ pp* b)

  W-rec-nondep : ∀ {ℓ} (P : Set ℓ) (cc* : A → P)
    (pp* : (b : B) → cc* (f b) ≡ cc* (g b))
    → (W → P)
  W-rec-nondep P cc* pp* (#cc a) = cc* a

  postulate
    W-rec-nondep-β : ∀ {ℓ} (P : Set ℓ) (cc* : A → P)
      (pp* : (b : B) → cc* (f b) ≡ cc* (g b))
      → ((b : B) → ap (W-rec-nondep P cc* pp*) (pp b) ≡ pp* b)

open BaseHIT public

module FlattenedHIT where
  {-
    data Wt : Set where
      cct : (a : A) → C a → Wt
      pp : (b : B) (d : C (f b)) → cct (f b) d ≡ cct (g b) (π₁ (D b) d)
  -}

  private
    data #Wt : Set ijk where
      #cct : (a : A) (c : C a) → #Wt

  Wt : Set ijk
  Wt = #Wt

  cct : (a : A) → C a → Wt
  cct = #cct

  postulate
    ppt : (b : B) (d : C (f b)) → cct (f b) d ≡ cct (g b) (π₁ (D b) d)

  Wt-rec : ∀ {ℓ} (P : Wt → Set ℓ) (cct* : (a : A) (c : C a) → P (cct a c))
    (ppt* : (b : B) (d : C (f b)) →
           cct* (f b) d == cct* (g b) (π₁ (D b) d) [ P ↓ ppt b d ])
    → ((w : Wt) → P w)
  Wt-rec P cct* ppt* (#cct a c) = cct* a c

  postulate
    Wt-rec-β : ∀ {ℓ} (P : Wt → Set ℓ) (cct* : (a : A) (c : C a) → P (cct a c))
      (ppt* : (b : B) (d : C (f b)) →
             cct* (f b) d == cct* (g b) (π₁ (D b) d) [ P ↓ ppt b d ])
      → ((b : B) (d : C (f b)) → apd (Wt-rec P cct* ppt*) (ppt b d) ≡ ppt* b d)

  Wt-rec-nondep : ∀ {ℓ} (P : Set ℓ) (cct* : (a : A) → C a → P)
    (ppt* : (b : B) (d : C (f b)) → cct* (f b) d ≡ cct* (g b) (π₁ (D b) d))
    → (Wt → P)
  Wt-rec-nondep P cct* ppt* (#cct a c) = cct* a c

  postulate
    Wt-rec-nondep-β : ∀ {ℓ} (P : Set ℓ) (cct* : (a : A) → C a → P)
      (ppt* : (b : B) (d : C (f b)) → cct* (f b) d ≡ cct* (g b) (π₁ (D b) d))
      → ((b : B) (d : C (f b))
        → ap (Wt-rec-nondep P cct* ppt*) (ppt b d) ≡ ppt* b d)

open FlattenedHIT public

-- Here is the fibration

D-eq : (b : B) → C (f b) ≡ C (g b)
D-eq b = ua-in (D b)

P : W → Set k
P = W-rec-nondep _ C D-eq

pp-path : (b : B) (d : C (f b)) → π₁ (ua-out (ap P (pp b))) d ≡ π₁ (D b) d
pp-path b d =
  π₁ (ua-out (ap P (pp b))) d
            ≡⟨ W-rec-nondep-β _ C D-eq _ |in-ctx (λ u → π₁ (ua-out u) d) ⟩
  π₁ (ua-out (ua-in (D b))) d
            ≡⟨ ua-β (D b) |in-ctx (λ u → π₁ u d) ⟩
  π₁ (D b) d ∎

lem : ∀ {i} {A : Set i} {x y z : A} (p : x ≡ y) (q : y ≡ z)
  → ! p ∘ (p ∘' q) ≡ q
lem refl refl = refl

-- Dependent path in [P] over [pp b]
module _ {b : B} {d : C (f b)} {d' : C (g b)} where
  ↓-pp-in : (π₁ (D b) d ≡ d' → d == d' [ P ↓ pp b ])
  ↓-pp-in p = to-transp-in P (pp b) (pp-path b d ∘' p)

  ↓-pp-out : (d == d' [ P ↓ pp b ] → π₁ (D b) d ≡ d')
  ↓-pp-out p = ! (pp-path b d) ∘ to-transp-out p

  ↓-pp-β : (q : π₁ (D b) d ≡ d') → ↓-pp-out (↓-pp-in q) ≡ q
  ↓-pp-β q =
    ↓-pp-out (↓-pp-in q)
               ≡⟨ refl ⟩
    ! (pp-path b d) ∘ to-transp-out (to-transp-in P (pp b) (pp-path b d ∘' q))
               ≡⟨ to-transp-β P (pp b) (pp-path b d ∘' q) |in-ctx (λ u → ! (pp-path b d) ∘ u) ⟩
    ! (pp-path b d) ∘ (pp-path b d ∘' q)
               ≡⟨ lem (pp-path b d) q ⟩
    q ∎

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS -v treeless.opt:20 #-}
module _ where

open import Agda.Builtin.Nat renaming (_<_ to _<?_)
open import Common.Prelude
open import Common.Equality

data _<_ (a b : Nat) : Set where
  diff : (k : Nat) → b ≡ suc k + a → a < b

data Comparison {a} {A : Set a} (_<_ : A → A → Set a) (x y : A) : Set a where
  less    : x < y → Comparison _<_ x y
  equal   : x ≡ y → Comparison _<_ x y
  greater : y < x → Comparison _<_ x y

compare : (a b : Nat) → Comparison _<_ a b
compare a b with a <? b
... | true  = less (diff (b ∸ suc a) primTrustMe)
... | false with b <? a
...   | true  = greater (diff (a ∸ suc b) primTrustMe)
...   | false = equal primTrustMe

{-# INLINE compare #-}

-- This should compile to two calls of _<?_ and only the possible cases.
compare-lots : (a b : Nat) → String
compare-lots a b with compare a b | compare (suc a) (suc b)
compare-lots a b | less (diff k eq) | less (diff k₁ eq₁) = "less-less"
compare-lots a .a | less (diff k eq) | equal refl = "less-equal"
compare-lots a _ | less (diff k refl) | greater (diff j eq) = "less-greater"
compare-lots a .a | equal refl | less (diff k eq₁) = "equal-less"
compare-lots a b | equal eq | equal eq₁ = "equal-equal"
compare-lots a .a | equal refl | greater (diff k eq₁) = "equal-greater"
compare-lots _ b | greater (diff k refl) | less (diff j eq) = "greater-less"
compare-lots _ b | greater (diff k refl) | equal eq = "greater-equal"
compare-lots a b | greater (diff k eq) | greater (diff k₁ eq₁) = "greater-greater"

main : IO Unit
main = putStrLn (compare-lots 1500 2000) ,,
       putStrLn (compare-lots 2000 1500) ,,
       putStrLn (compare-lots 2000 2000)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --without-K #-}
module hott.equivalence.inverse where

open import level
open import sum
open import function.core
open import function.isomorphism.core
open import function.isomorphism.utils
open import function.isomorphism.properties
open import function.extensionality
open import function.overloading
open import equality.core
open import sets.unit
open import sets.nat.core using (suc)
open import hott.level
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.univalence

module _ {i j}{A : Set i}{B : Set j} where
  record inverse (f : A → B) : Set (i ⊔ j) where
    constructor mk-inverse
    field
      g : B → A
      α : (x : A) → g (f x) ≡ x
      β : (y : B) → f (g y) ≡ y

    isom : A ≅ B
    isom = iso f g α β

  iso⇒inv : (f : A ≅ B) → inverse (apply f)
  iso⇒inv (iso f g α β) = mk-inverse g α β

  inverse-struct-iso : (f : A → B)
                     → inverse f
                     ≅ ( Σ (B → A) λ g
                       → Σ ((x : A) → g (f x) ≡ x) λ α
                       → ((y : B) → f (g y) ≡ y) )
  inverse-struct-iso f = record
    { to = λ { (mk-inverse g α β) → (g , α , β) }
    ; from = λ { (g , α , β) → (mk-inverse g α β) }
    ; iso₁ = λ _ → refl
    ; iso₂ = λ _ → refl }

  ≅-inv-struct-iso : (A ≅ B) ≅ Σ (A → B) inverse
  ≅-inv-struct-iso = trans≅ ≅-struct-iso
    (Σ-ap-iso₂ (λ f → sym≅ (inverse-struct-iso f)))

ind-≈ : (P : ∀ {i}{A B : Set i} → A ≈ B → Set i)
      → (∀ {i}{A : Set i} → P {A = A} (≡⇒≈ refl))
      → ∀ {i}{A B : Set i}(eq : A ≈ B) → P eq
ind-≈ P d {A = A} eq = subst P (_≅_.iso₂ uni-iso eq)
                               (lem (≈⇒≡ eq))
  where
    lem : ∀ {i}{A B : Set i}
        → (p : A ≡ B)
        → P (≡⇒≈ p)
    lem refl = d

inverse-nonprop' : ∀ {i}{A : Set i}
                 → inverse (λ (x : A) → x)
                 ≅ ((x : A) → x ≡ x)
inverse-nonprop' {i}{A} = begin
    inverse id'
  ≅⟨ inverse-struct-iso id' ⟩
    ( Σ (A → A) λ g
    → Σ ((x : A) → g x ≡ x) λ α
    → ((y : A) → g y  ≡ y) )
  ≅⟨ ( Σ-ap-iso₂ λ g
      → Σ-ap-iso₁ strong-funext-iso ) ⟩
    ( Σ (A → A) λ g
    → Σ (g ≡ id') λ α
    → ((y : A) → g y ≡ y) )
  ≅⟨ sym≅ Σ-assoc-iso ⟩
    ( Σ (singleton' id') λ { (g , α)
    → ((y : A) → g y ≡ y) } )
  ≅⟨ trans≅ (Σ-ap-iso' (contr-⊤-iso (singl-contr' id'))
                       (λ _ → refl≅))
            ×-left-unit ⟩
    ((x : A) → x ≡ x)
  ∎
  where
    open ≅-Reasoning
    id' : A → A
    id' x = x

inverse-nonprop : ∀ {i}{A B : Set i}
                → (f : A → B)
                → weak-equiv f
                → inverse f
                ≅ ((x : A) → x ≡ x)
inverse-nonprop {i}{A} f we = ind-≈ P inverse-nonprop' (f , we)
  where
    P : ∀ {i}{A B : Set i} → A ≈ B → Set _
    P {A = A} (f , we) = inverse f ≅ ((x : A) → x ≡ x)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

module _ where

data D {ℓ} (A : Set ℓ) : Set ℓ where
  c : PathP _ _ _

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

-- Pi combinators inspired by duals and traced monoidal categories

module Trace where

open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; subst)

open import PiFrac

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

dual : {A B : 𝕌} → (f : A ⟷ B) → (v : ⟦ A ⟧ ) →
                   (𝟙/● B [ eval f v ] ⟷ 𝟙/● A [ v ])
dual f v = uniti⋆l ⊚ (η v ⊗ id⟷) ⊚ ((lift f ⊗ id⟷) ⊗ id⟷) ⊚
  assocr⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚ assocl⋆ ⊚ (ε (eval f v) ⊗ id⟷) ⊚ unite⋆l

-- name, coname
name : {A B : 𝕌} → (f : A ⟷ B) → (v : ⟦ A ⟧ ) → 𝟙 ⟷ ● B [ eval f v ] ×ᵤ 𝟙/● A [ v ]
name f v = η v ⊚ (lift f ⊗ id⟷)

coname : {A B : 𝕌} → (f : A ⟷ B) → (v : ⟦ A ⟧ ) → ● A [ v ] ×ᵤ 𝟙/● B [ eval f v ] ⟷ 𝟙
coname f v = (lift f ⊗ id⟷) ⊚ ε (eval f v)

-- and 'trace' reveals something neat: we can't choose just any random 'a' and 'c'
-- to start with, but we need that make a coherence choice of a and c !!
trace : {A B C : 𝕌} (a : ⟦ A ⟧ ) → (f : A ×ᵤ C ⟷ B ×ᵤ C) →
  (coh : Σ ⟦ C ⟧ (λ c → proj₂ (eval f (a , c)) ≡ c)) →
  ● A [ a ] ⟷ ● B [ proj₁ (eval f (a , proj₁ coh)) ]
trace {A} {B} {C} a f (c , choice) =
  uniti⋆r ⊚        -- A ×ᵤ 1
  (id⟷ ⊗ η c) ⊚   -- A ×ᵤ (C ×ᵤ 1/C)
  assocl⋆ ⊚       -- (A ×ᵤ C) ×ᵤ 1/C
  (tensorr ⊗ id⟷) ⊚ -- bring in the ●
  (lift f ⊗ id⟷) ⊚ -- (B ×ᵤ C) ×ᵤ 1/C
  (tensorl ⊗ id⟷) ⊚ -- bring out the ●
  assocr⋆ ⊚          -- B ×ᵤ (C ×ᵤ 1/C)
  (id⟷ ⊗ (subst fixer choice id⟷ ⊚ ε c)) ⊚ -- B ×ᵤ 1
  unite⋆r
  where
    fixer : ⟦ C ⟧ → Set
    fixer d = (● C [ proj₂ (eval f (a , c)) ] ×ᵤ 𝟙/● C [ d ]) ⟷ (● C [ d ] ×ᵤ 𝟙/● C [ d ])

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The unit type
------------------------------------------------------------------------

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

module Data.Unit where

import Relation.Binary.PropositionalEquality as PropEq

------------------------------------------------------------------------
-- Re-export contents of base module

open import Data.Unit.Base public

------------------------------------------------------------------------
-- Re-export query operations

open import Data.Unit.Properties public
  using (_≟_; _≤?_)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

setoid = Data.Unit.Properties.≡-setoid
{-# WARNING_ON_USAGE setoid
"Warning: setoid was deprecated in v1.1.
Please use ≡-setoid from Data.Unit.Properties instead."
#-}
decSetoid = Data.Unit.Properties.≡-decSetoid
{-# WARNING_ON_USAGE decSetoid
"Warning: decSetoid was deprecated in v1.1.
Please use ≡-decSetoid from Data.Unit.Properties instead."
#-}
total = Data.Unit.Properties.≡-total
{-# WARNING_ON_USAGE total
"Warning: total was deprecated in v1.1.
Please use ≡-total from Data.Unit.Properties instead"
#-}
poset = Data.Unit.Properties.≡-poset
{-# WARNING_ON_USAGE poset
"Warning: poset was deprecated in v1.1.
Please use ≡-poset from Data.Unit.Properties instead."
#-}
decTotalOrder = Data.Unit.Properties.≡-decTotalOrder
{-# WARNING_ON_USAGE decTotalOrder
"Warning: decTotalOrder was deprecated in v1.1.
Please use ≡-decTotalOrder from Data.Unit.Properties instead."
#-}
preorder = PropEq.preorder ⊤
{-# WARNING_ON_USAGE decTotalOrder
"Warning: preorder was deprecated in v1.1.
Please use ≡-preorder from Data.Unit.Properties instead."
#-}


text:
module Logic where

data True : Set where
  tt : True

data False : Set where


text:
module Data.Option.Equiv where

import      Lvl
open import Data.Option
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ ℓₑₐ : Lvl.Level
private variable A : Type{ℓ}

record Extensionality ⦃ equiv-A : Equiv{ℓₑₐ}(A) ⦄ (equiv : Equiv{ℓₑ}(Option(A))) : Type{Lvl.of(A) Lvl.⊔ ℓₑₐ Lvl.⊔ ℓₑ} where
  constructor intro
  private instance _ = equiv
  field
    ⦃ Some-function ⦄ : Function Some
    ⦃ Some-injective ⦄ : Injective Some
    cases-inequality : ∀{x : A} → (None ≢ Some(x))


text:
{-# OPTIONS --copatterns --sized-types --experimental-irrelevance #-}
-- {-# OPTIONS --show-implicit --show-irrelevant #-}
-- {-# OPTIONS -v tc.polarity:10 -v tc.pos:15 -v tc.size.solve:100 #-}

module SizedCoinductiveRecords where

open import Common.Size

{- THIS WOULD BE A BETTER TYPING FOR sizeSuc, but it requires builtin Size<
sizeSuc : (i : Size) → Size< (↑ (↑ i))
sizeSuc i = ↑ i
-}

-- -- Subtyping for Size<
-- Andreas, 2015-03-15: Functions returning sizes are now illegal:
-- emb< : {i : Size} → Size< i → Size
-- emb< {i} j = j

-- Use Size< hypotheses

data Empty : {i : Size} → Set where
  empty : {i : Size} → Empty {i} → Empty {↑ i}

subEmpty : {i : Size}{j : Size< i} → Empty {j} → Empty {i}
subEmpty x = x

-- SHOULD FAIL:
-- fail : {i : Size}{j : Size< i} → Empty {i} → Empty {j}
-- fail x = x

-- -- Covariance for Size<
-- Andreas, 2015-03-15: Functions returning sizes are now illegal:
-- co : {i : Size}{j : Size< i} → Size< j → Size< i
-- co k = k

-- Contravariance for bounded quantification

Bounded : Size → Set
Bounded i = (j : Size< i) → Empty {j}

contra : {i : Size}{j : Size< i} → Bounded i → Bounded j
contra k = k

-- sized naturals

data Nat {i : Size} : Set where
  zero : Nat
  suc  : {j : Size< i} → Nat {j} → Nat

-- polarity of successor

data Bool : Set where
  true false : Bool

-- a natural number

one : Nat
one = suc {i = ∞} zero

mySuc : {i : Size} → Nat {i} → Nat {↑ i}
mySuc x = suc x

pred : {i : Size} → Nat {↑ i} → Nat {i}
pred zero = zero
pred (suc n) = n

shift : {i : Size} → (Nat → Nat {↑ i}) → Nat → Nat {i}
shift f n = pred (f (suc n))

{- Does not type check
loop : {i : Size} → Nat {i} → (Nat → Nat {i}) → Set
loop (suc n) f = loop n (shift f)
loop zero      = Nat
-}

data ⊥ : Set where
record ⊤ : Set where

mono : {i : Size}{j : Size< i} → Nat {j} → Nat {i}
mono n = n

id : {i : Size} → Nat {i} → Nat {i}
id (zero) = zero
id (suc n) = suc (id n)

monus : {i : Size} → Nat {i} → Nat → Nat {i}
monus x zero = x
monus zero y = zero
monus (suc x) (suc y) = monus x y

div : {i : Size} → Nat {i} → Nat → Nat {i}
div zero    y = zero
div (suc x) y = suc (div (monus x y) y)

-- postulate _∪_ : {i : Size} → Size< i → Size< i → Size< i

{-
max : {i : Size} → Nat {i} → Nat {i} → Nat {i}
max zero n = n
max m zero = m
max {i} (suc {j = j} m) (suc {j = k} n) = suc {j = j ∪ k} (max {j ∪ k} m n)
-}

-- omega inst

{- DOES NOT MAKE SENSE:
omegaBad' : (F : Size → Set) (i : Size) (j : Size< i)
            (f : (k : Size< (↑ j)) → F k) → F j
omegaBad' F i j f = f j
-}

-- fix

A : Size → Set
A i = Nat {i} → Nat

{-# TERMINATING #-}
fix : (f : (i : Size) → ((j : Size< i) → A j) → A i) → (i : Size) → A i
fix f i zero        = zero
fix f i (suc {j} n) = f i (λ j → fix f j) (suc n)

-- forever : {i : Size} → ({j : Size< i} → Nat {i} → Nat {j}) → Nat {i} → ⊥
-- forever {i} f n = forever f (f {{!!}} n)

-- sized streams

module STREAM where

  record Stream (A : Set) {i : Size} : Set where
    coinductive
    constructor _∷_
    field
      head : A
      tail : {j : Size< i} → Stream A {j}
  open Stream

  map : {A B : Set}(f : A → B){i : Size} → Stream A {i} → Stream B {i}
  head (map f s) = f (head s)
  tail (map f s) = map f (tail s)

  -- stream antitone

  anti : {A : Set}{i : Size}{j : Size< i} → Stream A {i} → Stream A {j}
  anti s = s

  anti' : {A : Set}{i : Size}{j : Size< i} → (Stream A {j} → A) → (Stream A {i} → A)
  anti' f = f

-- Spanning tree

data List (A : Set) {i : Size} : Set where
  []  : List A
  _∷_ : {j : Size< i}(x : A)(xs : List A {j}) → List A

map : {A B : Set}(f : A → B){i : Size} → List A {i} → List B {i}
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

module Graph (I : Set)(adj : I → List I) where

  record Span {i : Size} : Set where
    coinductive
    constructor span
    field
      root  : I
      nodes : {j : Size< i} → List (Span {j})
  open Span

  tree : {i : Size} → I → Span {i}
  root  (tree root) = root
  nodes (tree root) = map (tree) (adj root)


text:
module Validation where

open import OscarPrelude
open import 𝓐ssertion
open import HasSatisfaction
open import Interpretation

module _ {A} ⦃ _ : HasSatisfaction A ⦄
 where

   ⊨_ : A → Set
   ⊨ x = (I : Interpretation) → I ⊨ x

   ⊭_ : A → Set
   ⊭_ = ¬_ ∘ ⊨_


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

open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Group.SuspensionMap

open import Cubical.Relation.Nullary

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Wedge
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.GradedCommutativity
open import Cubical.ZCohomology.Gysin

open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv

open import Cubical.Data.Sigma
open import Cubical.Data.Int hiding (_+'_)
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _·_ to _·ℕ_)
open import Cubical.Data.Unit

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Exact
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Instances.Unit

open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.Truncation
  renaming (rec to trRec)
open import Cubical.HITs.SetTruncation
  renaming (rec to sRec ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation
  renaming (rec to pRec)

-- The pushout of the hopf invariant
HopfInvariantPush : (n : ℕ)
             → (f : S₊ (3 +ℕ n +ℕ n) → S₊ (2 +ℕ n))
             → Type _
HopfInvariantPush n f = Pushout (λ _ → tt) f

Hopfα : (n : ℕ)
     → (f : S₊∙ (3 +ℕ n +ℕ n) →∙ S₊∙ (2 +ℕ n))
     → coHom (2 +ℕ n) (HopfInvariantPush n (fst f))
Hopfα n f = ∣ (λ { (inl x) → 0ₖ _
                ; (inr x) → ∣ x ∣
                ; (push a i) → help a (~ i)}) ∣₂
  where
  help : (a : S₊ (3 +ℕ n +ℕ n)) → ∣ fst f a ∣ ≡ 0ₖ (2 +ℕ n)
  help = sphereElim _ (λ _ → isOfHLevelPlus' {n = n} (3 +ℕ n)
         (isOfHLevelPath' (3 +ℕ n) (isOfHLevelTrunc (4 +ℕ n)) _ _))
                                    (cong ∣_∣ₕ (snd f))

Hopfβ : (n : ℕ)
     → (f : S₊∙ (3 +ℕ n +ℕ n) →∙ S₊∙ (2 +ℕ n))
     → coHom (4 +ℕ (n +ℕ n)) (HopfInvariantPush n (fst f))
Hopfβ n f = fst (MV.d _ _ _ (λ _ → tt) (fst f) (3 +ℕ n +ℕ n)) ∣ ∣_∣ ∣₂

-- To define the Hopf invariant, we need to establish the
-- non-trivial isos of Hⁿ(HopfInvariant).
module _ (n : ℕ) (f : S₊∙ (3 +ℕ n +ℕ n) →∙ S₊∙ (2 +ℕ n)) where
  module M = MV _ _ _ (λ _ → tt) (fst f)
  ¬lemHopf : (n m : ℕ) → ¬ suc (suc (m +ℕ n)) ≡ suc n
  ¬lemHopf zero zero p = snotz (cong predℕ p)
  ¬lemHopf (suc n) zero p = ¬lemHopf n zero (cong predℕ p)
  ¬lemHopf zero (suc m) p = snotz (cong predℕ p)
  ¬lemHopf (suc n) (suc m) p =
    ¬lemHopf n (suc m) (cong (suc ∘ suc )
      (sym (+-suc m n)) ∙ (cong predℕ p))

  SphereHopfCohomIso :
    GroupEquiv
      (coHomGr (3 +ℕ n +ℕ n) (S₊ (3 +ℕ n +ℕ n)))
      ((coHomGr (suc (3 +ℕ n +ℕ n)) (HopfInvariantPush _ (fst f))))
  fst (fst SphereHopfCohomIso) =
    fst (MV.d _ _ _ (λ _ → tt) (fst f) (3 +ℕ n +ℕ n))
  snd (fst SphereHopfCohomIso) = help
    where
      abstract
        help : isEquiv (fst (MV.d _ _ _ (λ _ → tt) (fst f)
                                 (3 +ℕ n +ℕ n)))
        help =
          SES→isEquiv
            (isContr→≡UnitGroup
              (isContrΣ (GroupIsoUnitGroup→isContr (invGroupIso (Hⁿ-Unit≅0 _)))
                        λ _ → GroupIsoUnitGroup→isContr
                            (invGroupIso (Hⁿ-Sᵐ≅0 _ _ (¬lemHopf n n)))))
            (isContr→≡UnitGroup
              (isContrΣ (GroupIsoUnitGroup→isContr
                        (invGroupIso (Hⁿ-Unit≅0 _)))
                        λ _ → GroupIsoUnitGroup→isContr
                          (invGroupIso (Hⁿ-Sᵐ≅0 _ _ (¬lemHopf n (suc n))))))
              (M.Δ (3 +ℕ n +ℕ n))
              (M.d (3 +ℕ n +ℕ n))
              (M.i (4 +ℕ n +ℕ n))
              (M.Ker-d⊂Im-Δ _)
              (M.Ker-i⊂Im-d _)
  snd SphereHopfCohomIso = d-inv
    where
      -- Currently, type checking is very slow without the abstract flag.
      -- TODO : Remove abstract
      abstract
        d-inv : IsGroupHom (snd (coHomGr (3 +ℕ n +ℕ n) (S₊ (3 +ℕ n +ℕ n))))
                  (fst (MV.d _ _ _ (λ _ → tt) (fst f) (3 +ℕ n +ℕ n)))
                  (snd (coHomGr (suc (3 +ℕ n +ℕ n))
                       (Pushout (λ _ → tt) (fst f))))
        d-inv = snd (MV.d _ _ _ (λ _ → tt) (fst f) (3 +ℕ n +ℕ n))

  Hopfβ-Iso : GroupIso (coHomGr (suc (3 +ℕ n +ℕ n))
                                (HopfInvariantPush _ (fst f)))
                       ℤGroup
  fst Hopfβ-Iso = compIso (invIso (equivToIso (fst SphereHopfCohomIso)))
                           (fst (Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n)))))
  snd Hopfβ-Iso = grHom
    where
      abstract
        grHom :
          IsGroupHom (coHomGr (suc (3 +ℕ n +ℕ n))
                              (Pushout (λ _ → tt) (fst f)) .snd)
                     (λ x → Iso.fun (fst ((Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n))))))
                       (invEq (fst SphereHopfCohomIso) x))
                     (ℤGroup .snd)
        grHom = snd (compGroupIso
                  (GroupEquiv→GroupIso (invGroupEquiv (SphereHopfCohomIso)))
                  (Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n)))))

Hⁿ-Sⁿ≅ℤ-nice-generator : (n : ℕ) → Iso.inv (fst (Hⁿ-Sⁿ≅ℤ (suc n))) 1 ≡ ∣ ∣_∣ ∣₂
Hⁿ-Sⁿ≅ℤ-nice-generator zero = Iso.leftInv (fst (Hⁿ-Sⁿ≅ℤ (suc zero))) _
Hⁿ-Sⁿ≅ℤ-nice-generator (suc n) =
  (λ i → Iso.inv (fst (suspensionAx-Sn (suc n) (suc n)))
                  (Hⁿ-Sⁿ≅ℤ-nice-generator n i))
     ∙ cong ∣_∣₂
       (funExt λ { north → refl
                 ; south → cong ∣_∣ₕ (merid north)
                 ; (merid a i) j → ∣ compPath-filler (merid a)
                                      (sym (merid north)) (~ j) i ∣ₕ})

Hopfβ↦1 : (n : ℕ) (f : S₊∙ (3 +ℕ n +ℕ n) →∙ S₊∙ (2 +ℕ n))
  → Iso.fun (fst (Hopfβ-Iso n f)) (Hopfβ n f) ≡ 1
Hopfβ↦1 n f =
    sym (cong (Iso.fun (fst (Hopfβ-Iso n f))) lem)
  ∙ Iso.rightInv (fst (Hopfβ-Iso n f)) (pos 1)
  where
  lem : Iso.inv (fst (Hopfβ-Iso n f)) (pos 1) ≡ Hopfβ n f
  lem = (λ i → fst (MV.d _ _ _ (λ _ → tt) (fst f) (3 +ℕ n +ℕ n))
               (Hⁿ-Sⁿ≅ℤ-nice-generator _ i))
    ∙ cong ∣_∣₂ (funExt (λ { (inl x) → refl
                          ; (inr x) → refl
                          ; (push a i) → refl}))

module _ (n : ℕ) (f : S₊∙ (3 +ℕ n +ℕ n) →∙ S₊∙ (2 +ℕ n)) where
  private
    2+n = 2 +ℕ n
    H = HopfInvariantPush n (fst f)

    H→Sphere : coHom 2+n H → coHom 2+n (S₊ (suc (suc n)))
    H→Sphere = sMap (_∘ inr)

    grHom : IsGroupHom (snd (coHomGr 2+n H))
                       H→Sphere (snd (coHomGr 2+n (S₊ (suc (suc n)))))
    grHom =
      makeIsGroupHom
        (sElim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
          λ f g → refl)

    preSphere→H : (g : (S₊ (suc (suc n)) → coHomK 2+n))
                 → H → coHomK (2 +ℕ n)
    preSphere→H g (inl x) = 0ₖ _
    preSphere→H g (inr x) = g x -ₖ g north
    preSphere→H g (push a i) = lem a i
      where
      lem : (a : S₊ (suc (suc (suc (n +ℕ n)))))
          → 0ₖ (suc (suc n)) ≡ g (fst f a) -ₖ g north
      lem =
        sphereElim _
          (λ x → isOfHLevelPlus' {n = n} (3 +ℕ n)
                    (isOfHLevelTrunc (4 +ℕ n) _ _))
                    (sym (rCancelₖ _ (g north))
                     ∙ cong (λ x → g x -ₖ g north) (sym (snd f)))

    Sphere→H : coHom 2+n (S₊ (suc (suc n))) → coHom 2+n H
    Sphere→H = sMap preSphere→H

    conCohom2+n : (x : _) → ∥ x ≡ 0ₖ (suc (suc n)) ∥₁
    conCohom2+n =
      coHomK-elim _ (λ _ → isProp→isOfHLevelSuc (suc n) squash₁) ∣ refl ∣₁

  HIPSphereCohomIso :
    Iso (coHom (2 +ℕ n) (HopfInvariantPush n (fst f)))
        (coHom (2 +ℕ n) (S₊ (2 +ℕ n)))
  Iso.fun HIPSphereCohomIso = H→Sphere
  Iso.inv HIPSphereCohomIso = Sphere→H
  Iso.rightInv HIPSphereCohomIso =
    sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
      λ g → pRec (squash₂ _ _)
                  (λ p → cong ∣_∣₂ (funExt λ x → cong (g x +ₖ_) (cong (-ₖ_) p)
                                 ∙ rUnitₖ _ (g x)))
                  (conCohom2+n (g north))
  Iso.leftInv HIPSphereCohomIso =
    sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
      λ g →
       pRec (squash₂ _ _)
        (pRec (isPropΠ (λ _ → squash₂ _ _))
         (λ gn gtt →
          trRec (isProp→isOfHLevelSuc n (squash₂ _ _))
            (λ r → cong ∣_∣₂ (funExt λ {
                          (inl x) → sym gtt
                        ; (inr x) → (λ i → g (inr x) -ₖ gn i)
                                    ∙ rUnitₖ _ (g (inr x))
                        ; (push a i)
                          → sphereElim _
                               {A = λ a →
                                 PathP (λ i → preSphere→H (λ x → g (inr x))
                                                            (push a i)
                                      ≡ g (push a i))
                                     (sym gtt)
                                     ((λ i → g (inr (fst f a)) -ₖ gn i)
                                     ∙ rUnitₖ _ (g (inr (fst f a))))}
               (λ _ → isOfHLevelPathP' (suc (suc (suc (n +ℕ n))))
                        (isOfHLevelPath (suc (suc (suc (suc (n +ℕ n)))))
                         (isOfHLevelPlus' {n = n} (suc (suc (suc (suc n))))
                          (isOfHLevelTrunc (suc (suc (suc (suc n)))))) _ _) _ _)
                               r a i}))
                       (push-helper g gtt gn))
               (conCohom2+n (g (inr north))))
             (conCohom2+n (g (inl tt)))
    where
    push-helper : (g : HopfInvariantPush n (fst f) → coHomK (suc (suc n)))
     → (gtt : g (inl tt) ≡ 0ₖ (suc (suc n)))
     → (gn : g (inr north) ≡ 0ₖ (suc (suc n)))
     → hLevelTrunc (suc n)
             (PathP (λ i → preSphere→H (λ x → g (inr x)) (push north i)
                          ≡ g (push north i))
             (sym gtt)
             ((λ i → g (inr (fst f north)) -ₖ gn i)
              ∙ rUnitₖ _ (g (inr (fst f north)))))
    push-helper g gtt gn =
      isConnectedPathP _ (isConnectedPath _ (isConnectedKn _) _ _) _ _ .fst

  Hopfα-Iso : GroupIso (coHomGr (2 +ℕ n) (HopfInvariantPush n (fst f))) ℤGroup
  Hopfα-Iso =
    compGroupIso
      (HIPSphereCohomIso , grHom)
      (Hⁿ-Sⁿ≅ℤ (suc n))

Hopfα-Iso-α : (n : ℕ) (f : _)
            → Iso.fun (fst (Hopfα-Iso n f)) (Hopfα n f)
            ≡ 1
Hopfα-Iso-α n f =
    sym (cong (Iso.fun (fst (Hⁿ-Sⁿ≅ℤ (suc n)))) (Hⁿ-Sⁿ≅ℤ-nice-generator n))
  ∙ Iso.rightInv (fst (Hⁿ-Sⁿ≅ℤ (suc n))) (pos 1)
  where
  hz : Iso.fun (HIPSphereCohomIso n f) (Hopfα n f) ≡ ∣ ∣_∣ ∣₂
  hz = refl

⌣-α : (n : ℕ) → (f : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n)) → _
⌣-α n f = Hopfα n f ⌣ Hopfα n f

HopfInvariant : (n : ℕ)
             → (f : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
             → ℤ
HopfInvariant n f = Iso.fun (fst (Hopfβ-Iso n f))
  (subst (λ x → coHom x (HopfInvariantPush n (fst f)))
         (λ i → suc (suc (suc (+-suc n n i))))
         (⌣-α n f))

HopfInvariant-π' : (n : ℕ) → π' (3 +ℕ (n +ℕ n)) (S₊∙ (2 +ℕ n)) → ℤ
HopfInvariant-π' n = sRec isSetℤ (HopfInvariant n)

HopfInvariant-π : (n : ℕ) → π (3 +ℕ (n +ℕ n)) (S₊∙ (2 +ℕ n)) → ℤ
HopfInvariant-π n =  sRec isSetℤ λ x → HopfInvariant-π' n ∣ Ω→SphereMap _ x ∣₂

-- Elimination principle for the pushout defining the Hopf Invariant
HopfInvariantPushElim :
       ∀ {ℓ} n → (f : _)
    → {P : HopfInvariantPush n f → Type ℓ}
    → (isOfHLevel (suc (suc (suc (suc (n +ℕ n))))) (P (inl tt)))
    → (e : P (inl tt))
       (g : (x : _) → P (inr x))
       (r : PathP (λ i → P (push north i)) e (g (f north)))
    → (x : _) → P x
HopfInvariantPushElim n f {P = P} hlev e g r (inl x) = e
HopfInvariantPushElim n f {P = P} hlev e g r (inr x) = g x
HopfInvariantPushElim n f {P = P} hlev e g r (push a i₁) = help a i₁
  where
  help : (a : Susp (Susp (S₊ (suc (n +ℕ n)))))
       → PathP (λ i → P (push a i)) e (g (f a))
  help =
    sphereElim _
      (sphereElim _
        (λ _ → isProp→isOfHLevelSuc (suc (suc (n +ℕ n)))
                                      (isPropIsOfHLevel _))
                  (isOfHLevelPathP' (suc (suc (suc (n +ℕ n))))
                    (subst (isOfHLevel (suc (suc (suc (suc (n +ℕ n))))))
                           (cong P (push north))
                           hlev) _ _)) r

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Truncation where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ₁ : Level

data Susp (A : Type ℓ) : Type ℓ where
  north : Susp A
  south : Susp A
  merid : A → north ≡ south

SuspF : {A : Type ℓ} {B : Type ℓ₁} → (A → B) → Susp A → Susp B
SuspF f north = north
SuspF f south = south
SuspF f (merid a i) = merid (f a) i

data ℕ : Type where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

data ⊥ : Type where

S : ℕ → Type
S 0 = ⊥
S (suc n) = Susp (S n)

data ⊤ : Type where
  ⋆ : ⊤

D : ℕ → Type
D 0 = ⊤
D (suc n) = Susp (D n)

S→D : {n : ℕ} → S n → D n
S→D {suc n} = SuspF S→D

data ∥_∥_ (A : Type ℓ) (n : ℕ) : Type ℓ where
  ∣_∣ : A → ∥ A ∥ n
  hub : (f : S n → ∥ A ∥ n) (u : D n) → ∥ A ∥ n
  spoke : (f : S n → ∥ A ∥ n) (s : S n) → f s ≡ hub f (S→D s)

isOfHLevel : ℕ → Type ℓ → Type ℓ
isOfHLevel 0 A = A
isOfHLevel (suc n) A = (x y : A) → isOfHLevel n (x ≡ y)

sphereFill : (n : ℕ) (A : Type ℓ) (f : S n → A) → Type ℓ
sphereFill n A f = Σ (D n → A) (λ f' → (s : S n) → f s ≡ f' (S→D s))

isSphereFilled : ℕ → Type ℓ → Type ℓ
isSphereFilled n A = (f : S n → A) → sphereFill n A f

isSphereFilled∥∥ : (n : ℕ) (A : Type ℓ) → isSphereFilled n (∥ A ∥ n)
isSphereFilled∥∥ n A f = hub f , spoke f

isSphereFilledDesc : (n : ℕ) (A : Type ℓ)
  → isSphereFilled (suc n) A → (x y : A) → isSphereFilled n (x ≡ y)
isSphereFilledDesc n A h x y g = g' , r
  where
  f : S (suc n) → A
  f north = x
  f south = y
  f (merid u i) = g u i

  g' : D n → x ≡ y
  g' u i =
    hcomp
      (λ j →
        λ { (i = i0) → h f .snd north (~ j)
          ; (i = i1) → h f .snd south (~ j) })
      (h f .fst (merid u i))

  r : (s : S n) → g s ≡ g' (S→D s)
  r s i j =
    hcomp
      (λ k →
        λ { (i = i0) → g s j
          ; (j = i0) → h f .snd north (i ∧ ~ k)
          ; (j = i1) → h f .snd south (i ∧ ~ k) })
      (h f .snd (merid s j) i)

isSphereFilled→isOfHLevel : (n : ℕ) (A : Type ℓ)
  → isSphereFilled n A → isOfHLevel n A
isSphereFilled→isOfHLevel zero A h = h (λ ()) .fst ⋆
isSphereFilled→isOfHLevel (suc n) A h x y =
  isSphereFilled→isOfHLevel n (x ≡ y) (isSphereFilledDesc n A h x y)

isSphereFilledAsc : (n : ℕ) (A : Type ℓ)
  → ((x y : A) → isSphereFilled n (x ≡ y)) → isSphereFilled (suc n) A
isSphereFilledAsc n A h f = f' , r
  where
  g : S n → f north ≡ f south
  g s i = f (merid s i)

  f' : D (suc n) → A
  f' north = f north
  f' south = f south
  f' (merid u i) = h (f north) (f south) g .fst u i

  r : (s : S (suc n)) → f s ≡ f' (S→D s)
  r north = refl
  r south = refl
  r (merid s i) j = h (f north) (f south) g .snd s j i

isOfHLevel→isSphereFilled : (n : ℕ) (A : Type ℓ)
  → isOfHLevel n A → isSphereFilled n A
isOfHLevel→isSphereFilled 0 A h f = (λ _ → h) , λ ()
isOfHLevel→isSphereFilled (suc n) A h f =
  isSphereFilledAsc n A
    (λ x y → isOfHLevel→isSphereFilled n (x ≡ y) (h x y)) f

isOfHLevelTrunc : (n : ℕ) (A : Type ℓ) → isOfHLevel n (∥ A ∥ n)
isOfHLevelTrunc n A = isSphereFilled→isOfHLevel n (∥ A ∥ n) (isSphereFilled∥∥ n A)

rec : {n : ℕ} {A : Type ℓ} {B : Type ℓ₁}
  → isOfHLevel n B
  → (A → B) → ∥ A ∥ n → B
rec {n = n} {A = A} {B = B} hB g = helper
  where
  h : isSphereFilled n B
  h = isOfHLevel→isSphereFilled n B hB

  helper : ∥ A ∥ n → B
  helper ∣ x ∣ = g x
  helper (hub f u) = h (λ s → helper (f s)) .fst u
  helper (spoke f s i) = h (λ s → helper (f s)) .snd s i

sphereFillDep : (n : ℕ) (A : Type ℓ) (B : A → Type ℓ₁)
  (f₀' : D n → A)
  → ((s : S n) → B (f₀' (S→D s)))
  → Type _
sphereFillDep n A B f₀' f = Σ ((u : D n) → B (f₀' u)) (λ f' → (s : S n) → f s ≡ f' (S→D s))

isSphereFilledDep : ℕ → (A : Type ℓ) (B : A → Type ℓ₁) → Type _
isSphereFilledDep n A B =
  (f₀' : D n → A)
  (f : (s : S n) → B (f₀' (S→D s)))
  → sphereFillDep n A B f₀' f

isSphereFilledDepAsc : (n : ℕ) {A : Type ℓ} (B : A → Type ℓ₁)
  → ((x₀ y₀ : A) (x₁ : B x₀) (y₁ : B y₀) → isSphereFilledDep n (x₀ ≡ y₀) (λ p → PathP (λ i → B (p i)) x₁ y₁))
  → isSphereFilledDep (suc n) A B
isSphereFilledDepAsc n {A = A} B hB f₀' f = f' , r
  where
  g₀' : (u : D n) → f₀' north ≡ f₀' south
  g₀' u i = f₀' (merid u i)

  g : (s : S n)  → PathP (λ i → B (g₀' (S→D s) i)) (f north) (f south)
  g s i = f (merid s i)

  f' : (u : D (suc n)) → B (f₀' u)
  f' north = f north
  f' south = f south
  f' (merid u i) = hB (f₀' north) (f₀' south) (f north) (f south) g₀' g .fst u i

  r : (s : S (suc n)) → f s ≡ f' (S→D s)
  r north = refl
  r south = refl
  r (merid s i) j = hB (f₀' north) (f₀' south) (f north) (f south) g₀' g .snd s j i

isOfHLevel→isSphereFilledDep : (n : ℕ) {A : Type ℓ} (B : A → Type ℓ₁)
  → ((a : A) → isOfHLevel n (B a)) → isSphereFilledDep n A B
isOfHLevel→isSphereFilledDep 0 B hB f₀' f = (λ u → hB (f₀' u)) , λ ()
isOfHLevel→isSphereFilledDep (suc n) {A = A} B hB =
  isSphereFilledDepAsc n B
    (λ x₀ y₀ x₁ y₁ →
      isOfHLevel→isSphereFilledDep n {A = x₀ ≡ y₀} (λ p → PathP (λ i → B (p i)) x₁ y₁)
        (λ p → J (λ y₀ p → (y₁ : B y₀) → isOfHLevel n (PathP (λ i → B (p i)) x₁ y₁)) (hB x₀ x₁) p y₁))

elim : {n : ℕ} {A : Type ℓ} {B : ∥ A ∥ n → Type ℓ₁}
  (hB : (x : ∥ A ∥ n) → isOfHLevel n (B x))
  (g : (a : A) → B (∣ a ∣)) (x : ∥ A ∥ n) → B x
elim {n = n} {A = A} {B = B} hB g = helper
  where
  h : isSphereFilledDep n (∥ A ∥ n) B
  h = isOfHLevel→isSphereFilledDep n B hB

  helper : (x : ∥ A ∥ n) → B x
  helper ∣ a ∣ = g a
  helper (hub f u) = h (hub f) (λ s → subst B (spoke f s) (helper (f s))) .fst u
  helper (spoke f s i) =
    hcomp
      (λ j →
        λ { (i = i0) → helper (f s)
          ; (i = i1) →  h (hub f) (λ s → subst B (spoke f s) (helper (f s))) .snd s j })
      (subst-filler B (spoke f s) (helper (f s)) i)

max_stars_repo_name: howsiyu/hott-notes

max_issues_repo_name: howsiyu/hott-notes

max_forks_repo_name: howsiyu/hott-notes


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
-}

module Haskell.Modules.Either where

open import Data.Bool using (Bool; true; false; not)
import      Data.Sum  as DS renaming ([_,_] to either)
open import Function  using (_∘_)
open import Level           renaming (_⊔_ to _ℓ⊔_)

Either : ∀ {a b} → Set a → Set b → Set (a ℓ⊔ b)
Either A B = A DS.⊎ B
pattern Left  x = DS.inj₁ x
pattern Right x = DS.inj₂ x

either = DS.either

isLeft : ∀ {a b} {A : Set a} {B : Set b} → Either A B → Bool
isLeft (Left _)  = true
isLeft (Right _) = false

isRight : ∀ {a b} {A : Set a} {B : Set b} → Either A B → Bool
isRight = not ∘ isLeft