text:
-- Andreas, 2015-10-28 Issue 1407
-- (Issue 1023 raised its ugly head again!)

{-# OPTIONS -v term.with.inline:30 #-} --KEEP! Triggered bug on agda-2.4.2.5.
-- {-# OPTIONS -v term.with.inline:70 #-}
-- {-# OPTIONS -v tc.with.display:30 #-}

record _×_ (A B : Set) : Set where
  constructor pair
  field fst : A
        snd : B
open _×_

data Unit : Set where
  unit : Unit

data List (A : Set) : Set where
  _∷_ : A → List A → List A

map : ∀ A B → (A → B) → List A → List B
map A B f (x ∷ xs) = f x ∷ map A B f xs

record Setoid : Set₁ where
  field Carrier : Set
open Setoid

module Assoc (Key : Setoid) (_ : Set) where -- FAILS
-- module Assoc (_ : Set) (Key : Setoid) where -- WORKS

  data _∈_ (x : Carrier Key) : List (Carrier Key) → Set where
    here  : ∀ xs → Unit → x ∈ xs
    there : ∀ {xs} → x ∈ xs

  postulate
    foo : Carrier Key → Carrier Key → Unit

  lem : (p : Carrier Key × Unit)
      → (ps : List (Carrier Key × Unit))
      → fst p ∈ map (Carrier Key × Unit) (Carrier Key) fst ps
      → Set
  lem (pair k v) ((pair k' v') ∷ ps) (here .(k' ∷ map (Carrier Key × Unit) (Carrier Key) fst ps) u) with foo k k'
  ... | unit = Unit
  lem p (_ ∷ ps) there = lem p ps there -- to force termination checking

--     7   6       5 4        3  2     1              7       0
-- lem Key _ (pair k v) (pair k' v') ∷ ps) (here .(...Key...) u)
--          8   7 6 5   4         3 2  1  0
-- lem-with Key _ k k' (w = unit) v v' ps u = Unit
{-
inlinedClauses (raw)
  QNamed {qname = Issue1407.Assoc.lem, qnamed = Clause
  { clauseRange = /home/abel/agda/test/bugs/Issue1407.agda:40,3-13
  , clauseTel =
    ExtendTel (Def Issue1407.Setoid []) (Abs "Key"
    ExtendTel (Sort (Type (Max []))) (Abs "_"
    ExtendTel (Var 1 [Proj Issue1407.Setoid.Carrier]}) (Abs "k"
    ExtendTel (Var 2 [Proj Issue1407.Setoid.Carrier]}) (Abs "k'"
    ExtendTel (Def Issue1407.Unit []}) (Abs "v"
    ExtendTel (Def Issue1407.Unit []}) (Abs "v'"
    ExtendTel (Def Issue1407.List [Apply []r(Def Issue1407._×_ [Apply []r(Var 5 [Proj Issue1407.Setoid.Carrier]),Apply []r(Def Issue1407.Unit [])])]}) (Abs "ps"
    ExtendTel (Def Issue1407.Unit []}) (Abs "u"
    EmptyTel))))))))
  , clausePerm = x0,x1,x2,x3,x4,x5,x6,x7,x8 -> x0,x1,x2,x4,x3,x5,x6,x8
  , namedClausePats =
    [[]r(VarP "Key")
    ,[]r(VarP "x")
    ,[]r(ConP Issue1407._×_._,_(inductive)[Issue1407._×_.fst,Issue1407._×_.snd] (ConPatternInfo {conPRecord = Nothing, conPType = Nothing}) [[]r(VarP "k"),[]r(VarP "v")])
    ,[]r(ConP Issue1407.List._∷_(inductive)[] (ConPatternInfo {conPRecord = Nothing, conPType = Nothing}) [[]r(ConP Issue1407._×_._,_(inductive)[Issue1407._×_.fst,Issue1407._×_.snd] (ConPatternInfo {conPRecord = Nothing, conPType = Nothing}) [[]r(VarP "k'"),[]r(VarP "v'")]),[]r(VarP "ps")])
    ,[]r(ConP Issue1407.Assoc._∈_.here(inductive)[] (ConPatternInfo {conPRecord = Nothing, conPType = Nothing})
      [[]r{DotP (Con Issue1407.List._∷_(inductive)[]
        [[]r(Var 4 [])
        ,[]r(Def Issue1407.map
          [Apply []r{Def Issue1407._×_ [Apply []r(Def Issue1407.Assoc._.Carrier [Apply []r(Con Issue1407.Unit.unit(inductive)[] []),Apply []r(Var 3 [])])
                                       ,Apply []r(Def Issue1407.Unit [])]}
          ,Apply []r{Def Issue1407.Assoc._.Carrier [Apply []r(Con Issue1407.Unit.unit(inductive)[] [])
                                                   ,Apply []r(Var 3 [])]}
          ,Apply []r(Lam (ArgInfo {argInfoHiding = NotHidden, argInfoRelevance = Relevant, argInfoColors = []}) (Abs "r" Var 0 [Proj Issue1407._×_.fst]))
          ,Apply []r(Var 1 [])
          ])
        ])}
      ,[]r(VarP "u")
      ])
    ,[]r(ConP Issue1407.Unit.unit(inductive)[] (ConPatternInfo {conPRecord = Nothing, conPType = Nothing}) [])
    ]
  , clauseBody = Bind (Abs "h8" Bind (Abs "h7" Bind (Abs "h6" Bind (Abs "h5" Bind (Abs "h4" Bind (Abs "h3" Bind (Abs "h2" Bind (Abs "h1" Bind (Abs "h0" Body (Def Issue1407.Unit [])))))))))), clauseType = Nothing}}

-}


text:
open import Type

module Graph.Walk.Properties {ℓ₁ ℓ₂} {V : Type{ℓ₁}} where

open import Lang.Instance
open import Logic
import      Lvl
open import Graph{ℓ₁}{ℓ₂}(V)
open import Graph.Walk{ℓ₁}{ℓ₂}{V}
open import Relator.Equals.Proofs.Equiv
open import Type.Properties.MereProposition

module _ (_⟶_ : Graph) where
  -- `Passes edge walk` states that the walk `walk` contains the edge `edge`.
  -- In other words, there is a step in the walk which is `edge`.
  -- Note: Passes is a generalized containment relation for paths instead of lists.
  data Passes {v₁ v₂ : V} (edge : v₁ ⟶ v₂) : ∀{a b : V} → Walk(_⟶_) a b → Type{ℓ₁ Lvl.⊔ ℓ₂} where
    current : ∀{c}{rest : Walk(_⟶_) v₂ c} → Passes edge (Walk.prepend edge rest)
    skip    : ∀{b c}{rest : Walk(_⟶_) b c} → Passes edge rest → ∀{a}{e : (a ⟶ b)} → Passes edge (Walk.prepend e rest)

  -- `Visits v walk` states that the walk `walk` visits the vertex `v`.
  -- In other words, one of the steps/edges in the walk mention the vertex v.
  data Visits (v : V) : ∀{a b : V} → Walk(_⟶_) a b → Type{ℓ₁ Lvl.⊔ ℓ₂} where
    current : ∀{b}{path : Walk(_⟶_) v b} → Visits v path
    skip    : ∀{a b c}{e : (a ⟶ b)}{rest : Walk(_⟶_) b c} → Visits v rest → Visits v (Walk.prepend e rest)

  module _ {a b : V} (walk₁ : Walk(_⟶_) a b) {c d : V} (walk₂ : Walk(_⟶_) c d) where
    record Subwalk : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field proof : ∀{v₁ v₂ : V}{edge : v₁ ⟶ v₂} → Passes edge walk₁ → Passes edge walk₂

module _ {_⟶_ : Graph} {a b : V} (walk : Walk(_⟶_) a b) where
  -- A walk that never visits the same edge twice.
  -- Note: Equality on edges must respect uniqueness. In other words, one edge must not have multiple constructions.
  record Trail : Type{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{v₁ v₂ : V}{edge : v₁ ⟶ v₂} → MereProposition(Passes(_⟶_) edge walk)

  -- A walk that never visits the same vertex twice.
  -- Also called "Simple path".
  -- Note: Equality on edges must respect uniqueness. In other words, one edge must not have multiple constructions.
  record Path : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{v : V} → MereProposition(Visits(_⟶_) v walk)
  path = inst-fn Path.proof

  -- A walk that visits every vertex in the graph.
  record Traceable : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{v : V} → Visits(_⟶_) v walk
  traceable = inst-fn Traceable.proof

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:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Arithmetic where

open import Light.Level using (Setω ; Level)
open import Light.Variable.Levels

record Arithmetic (Operand : Set ℓ) : Setω where
      field _+_ _∗_ : Operand → Operand → Operand
open Arithmetic ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Classical.NaturalDeduction (𝔏 : Signature) where
open Signature(𝔏)

open import Data.ListSized
import      Lvl
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Formalization.PredicateLogic.Syntax.Substitution(𝔏)
open import Functional using (_∘_ ; _∘₂_ ; swap)
open import Numeral.Finite
open import Numeral.Natural
open import Relator.Equals.Proofs.Equiv
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇]) renaming (•_ to · ; _≡_ to _≡ₛ_)
open import Type

private variable ℓ : Lvl.Level
private variable args vars : ℕ
private variable Γ : PredSet{ℓ}(Formula(vars))

data _⊢_ {ℓ} : PredSet{ℓ}(Formula(vars)) → Formula(vars) → Type{Lvl.𝐒(ℓₚ Lvl.⊔ ℓₒ Lvl.⊔ ℓ)} where
  direct : (Γ ⊆ (Γ ⊢_))

  [⊤]-intro : (Γ ⊢ ⊤)

  [⊥]-elim  : ∀{φ} → ((Γ ∪ ·(¬ φ)) ⊢ ⊥) → (Γ ⊢ φ)

  [∧]-intro : ∀{φ ψ} → (Γ ⊢ φ) → (Γ ⊢ ψ) → (Γ ⊢ (φ ∧ ψ))
  [∧]-elimₗ : ∀{φ ψ} → (Γ ⊢ (φ ∧ ψ)) → (Γ ⊢ φ)
  [∧]-elimᵣ : ∀{φ ψ} → (Γ ⊢ (φ ∧ ψ)) → (Γ ⊢ ψ)

  [∨]-introₗ : ∀{φ ψ} → (Γ ⊢ φ) → (Γ ⊢ (φ ∨ ψ))
  [∨]-introᵣ : ∀{φ ψ} → (Γ ⊢ ψ) → (Γ ⊢ (φ ∨ ψ))
  [∨]-elim   : ∀{φ ψ χ} → ((Γ ∪ · φ) ⊢ χ) → ((Γ ∪ · ψ) ⊢ χ) → (Γ ⊢ (φ ∨ ψ)) → (Γ ⊢ χ)

  [⟶]-intro : ∀{φ ψ} → ((Γ ∪ · φ) ⊢ ψ) → (Γ ⊢ (φ ⟶ ψ))
  [⟶]-elim  : ∀{φ ψ} → (Γ ⊢ φ) → (Γ ⊢ (φ ⟶ ψ)) → (Γ ⊢ ψ)

  [Ɐ]-intro : ∀{φ} → (∀{t} → (Γ ⊢ (substitute0 t φ))) → (Γ ⊢ (Ɐ φ))
  [Ɐ]-elim  : ∀{φ} → (Γ ⊢ (Ɐ φ)) → ∀{t} → (Γ ⊢ (substitute0 t φ))

  [∃]-intro : ∀{φ}{t} → (Γ ⊢ (substitute0 t φ)) → (Γ ⊢ (∃ φ))
  [∃]-elim  : ∀{φ ψ} → (∀{t} → (Γ ∪ ·(substitute0 t φ)) ⊢ ψ) → (Γ ⊢ (∃ φ)) → (Γ ⊢ ψ)

module _ where
  open import Data.Either as Either
  import      Logic.Propositional as Meta
  open import Relator.Equals

  private variable Γ₁ Γ₂ : PredSet{ℓ}(Formula(vars))
  private variable φ ψ : Formula(vars)

  _⊬_ : PredSet{ℓ}(Formula(vars)) → Formula(vars) → Type
  _⊬_ = Meta.¬_ ∘₂ (_⊢_)

  [⟵]-intro : ((Γ ∪ · φ) ⊢ ψ) → (Γ ⊢ (ψ ⟵ φ))
  [⟵]-intro = [⟶]-intro

  [⟵]-elim : (Γ ⊢ φ) → (Γ ⊢ (ψ ⟵ φ)) → (Γ ⊢ ψ)
  [⟵]-elim = [⟶]-elim

  [¬]-intro : ((Γ ∪ · φ) ⊢ ⊥) → (Γ ⊢ (¬ φ))
  [¬]-intro = [⟶]-intro

  [⟷]-intro : ∀{φ ψ} → ((Γ ∪ · ψ) ⊢ φ) → ((Γ ∪ · φ) ⊢ ψ) → (Γ ⊢ (φ ⟷ ψ))
  [⟷]-intro l r = [∧]-intro ([⟶]-intro l) ([⟶]-intro r)

  [⟷]-elimₗ : ∀{φ ψ} → (Γ ⊢ ψ) → (Γ ⊢ (φ ⟷ ψ)) → (Γ ⊢ φ)
  [⟷]-elimₗ Γψ Γφψ = [⟶]-elim Γψ ([∧]-elimₗ Γφψ)

  [⟷]-elimᵣ : ∀{φ ψ} → (Γ ⊢ φ) → (Γ ⊢ (φ ⟷ ψ)) → (Γ ⊢ ψ)
  [⟷]-elimᵣ Γφ Γφψ = [⟶]-elim Γφ ([∧]-elimᵣ Γφψ)

  weaken-union-singleton : (Γ₁ ⊆ Γ₂) → (((Γ₁ ∪ · φ) ⊢_) ⊆ ((Γ₂ ∪ · φ) ⊢_))
  weaken : (Γ₁ ⊆ Γ₂) → ((Γ₁ ⊢_) ⊆ (Γ₂ ⊢_))

  weaken Γ₁Γ₂ {φ}                  (direct p)       = direct (Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.⊤}                 [⊤]-intro        = [⊤]-intro
  weaken Γ₁Γ₂ {φ}                  ([⊥]-elim p)     = [⊥]-elim (weaken-union-singleton Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(_ ∧ _)}           ([∧]-intro p q)  = [∧]-intro (weaken Γ₁Γ₂ p) (weaken Γ₁Γ₂ q)
  weaken Γ₁Γ₂ {φ}                  ([∧]-elimₗ p)    = [∧]-elimₗ (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {φ}                  ([∧]-elimᵣ p)    = [∧]-elimᵣ (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(_ ∨ _)}           ([∨]-introₗ p)   = [∨]-introₗ (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(_ ∨ _)}           ([∨]-introᵣ p)   = [∨]-introᵣ (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {φ}                  ([∨]-elim p q r) = [∨]-elim (weaken-union-singleton Γ₁Γ₂ p) (weaken-union-singleton Γ₁Γ₂ q) (weaken Γ₁Γ₂ r)
  weaken Γ₁Γ₂ {.(_ ⟶ _)}           ([⟶]-intro p)    = [⟶]-intro (weaken-union-singleton Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {φ}                  ([⟶]-elim p q)   = [⟶]-elim (weaken Γ₁Γ₂ p) (weaken Γ₁Γ₂ q)
  weaken Γ₁Γ₂ {.(Ɐ _)}             ([Ɐ]-intro p)    = [Ɐ]-intro (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(substitute0 _ _)} ([Ɐ]-elim p)     = [Ɐ]-elim (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(∃ _)}             ([∃]-intro p)    = [∃]-intro (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {φ}                  ([∃]-elim p q)   = [∃]-elim (weaken-union-singleton Γ₁Γ₂ p) (weaken Γ₁Γ₂ q)
  weaken-union-singleton Γ₁Γ₂ p = weaken (Either.mapLeft Γ₁Γ₂) p

  weaken-union : (Γ₁ ⊢_) ⊆ ((Γ₁ ∪ Γ₂) ⊢_)
  weaken-union = weaken Left

  [⊥]-elim-constructive : (Γ ⊢ ⊥) → (Γ ⊢ φ)
  [⊥]-elim-constructive Γ⊥ = [⊥]-elim (weaken-union Γ⊥)

  [¬¬]-elim : (Γ ⊢ ¬(¬ φ)) → (Γ ⊢ φ)
  [¬¬]-elim nnφ =
    ([⊥]-elim
      ([⟶]-elim
        (direct(Right [≡]-intro))
        (weaken-union nnφ)
      )
    )

  [¬¬]-intro : (Γ ⊢ φ) → (Γ ⊢ ¬(¬ φ))
  [¬¬]-intro Γφ =
    ([¬]-intro
      ([⟶]-elim
        (weaken-union Γφ)
        (direct (Right [≡]-intro))
      )
    )


text:
module Tactic.Reflection where

open import Prelude hiding (abs; _>>=_) renaming (_>>=′_ to _>>=_)
open import Builtin.Reflection           public
open import Tactic.Reflection.DeBruijn   public
open import Tactic.Reflection.Telescope  public
open import Tactic.Reflection.Substitute public
open import Tactic.Reflection.Free       public
open import Tactic.Reflection.Equality   public
open import Tactic.Reflection.Meta       public

set₀ : Type
set₀ = agda-sort (lit 0)

set! : Type
set! = agda-sort unknown

pattern var₀ x         = var x []
pattern var₁ x a       = var x (vArg a ∷ [])
pattern var₂ x a b     = var x (vArg a ∷ vArg b ∷ [])
pattern var₃ x a b c   = var x (vArg a ∷ vArg b ∷ vArg c ∷ [])
pattern var₄ x a b c d = var x (vArg a ∷ vArg b ∷ vArg c ∷ vArg d ∷ [])

pattern con₀ c         = con c []
pattern con₁ c x       = con c (vArg x ∷ [])
pattern con₂ c x y     = con c (vArg x ∷ vArg y ∷ [])
pattern con₃ c x y z   = con c (vArg x ∷ vArg y ∷ vArg z ∷ [])
pattern con₄ c x y z u = con c (vArg x ∷ vArg y ∷ vArg z ∷ vArg u ∷ [])

pattern def₀ f         = def f []
pattern def₁ f x       = def f (vArg x ∷ [])
pattern def₂ f x y     = def f (vArg x ∷ vArg y ∷ [])
pattern def₃ f x y z   = def f (vArg x ∷ vArg y ∷ vArg z ∷ [])
pattern def₄ f x y z u = def f (vArg x ∷ vArg y ∷ vArg z ∷ vArg u ∷ [])

infixr 4 _`→_ _`→ʰ_ _`→ⁱ_
_`→_ _`→ʰ_ _`→ⁱ_ : Type → Type → Type
_`→_  a b = pi (vArg a) (abs "_" b)
_`→ʰ_ a b = pi (hArg a) (abs "_" b)
_`→ⁱ_ a b = pi (iArg a) (abs "_" b)

`λ : Term → Term
`λ b = lam visible (abs "_" b)

infixl 9 _`∘_
_`∘_ : Term → Term → Term
_`∘_ = def₂ (quote _∘_)

infixr -20 _`$_
_`$_ : Term → Term → Term
_`$_ = def₂ (quote _$_)

_:′_ : Term → Type → TC Term
_:′_ = checkType

λ′ : ∀ {a} {A : Set a} → Arg Type → TC A → TC A
λ′ = extendContext

infix 2 _=′_
_=′_ : Term → Term → TC ⊤
_=′_ = unify

on-goal : (Type → Tactic) → Tactic
on-goal tac hole = inferNormalisedType hole >>= λ goal → tac goal hole

forceFun : Type → TC Type
forceFun a = do
  dom ← newMeta set!
  rng ← newMeta set!
  unify a (dom `→ weaken 1 rng)
  normalise a

inferFunRange : Term → TC Type
inferFunRange hole = unPi =<< forceFun =<< inferType hole where
  unPi : Type → TC Type
  unPi (pi _ (abs _ (meta x _))) = blockOnMeta! x
  unPi (pi _ (abs _ b)) = maybe (typeError ( strErr "Must be applied in a non-dependent function position"
                                           ∷ termErr b ∷ [])) pure $ strengthen 1 b
  unPi x = typeError (strErr "Invalid goal" ∷ termErr x ∷ [])

macro
  runT : Tactic → Tactic
  runT t = t

evalTC : ∀ {a} {A : Set a} → TC A → Tactic
evalTC {A = A} c hole = do
  v  ← c
  `v ← quoteTC v
  `A ← quoteTC A
  checkedHole ← checkType hole `A
  unify checkedHole `v

macro
  evalT : ∀ {a} {A : Set a} → TC A → Tactic
  evalT = evalTC

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
------------------------------------------------------------------------------
-- The unary numbers are LTC-PCF total natural numbers
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.UnaryNumbers.Totality where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat.Type
open import LTC-PCF.Data.Nat.UnaryNumbers

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

0-N : N [0]
0-N = nzero

1-N : N [1]
1-N = nsucc 0-N

2-N : N [2]
2-N = nsucc 1-N

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue204.Dependency where

postulate
  Level : Set
  zero : Level
  suc  : Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

record R (ℓ : Level) : Set (suc ℓ) where

data D (ℓ : Level) : Set (suc ℓ) where

module M {ℓ : Level} (d : D ℓ) where

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Algebra.Category where

open import Algebra.Category.Category public
open import Algebra.Category.Groupoid public
open import Algebra.Category.Semigroupoid public

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.ExecutedBlock as ExecutedBlock
import      LibraBFT.Impl.Consensus.ConsensusTypes.Vote          as Vote
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.OBM.Prelude
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.ByteString
open import Util.Hash
import      Util.KVMap                                           as Map
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                          using (String)

module LibraBFT.Impl.Consensus.BlockStorage.BlockTree where

postulate -- TODO-2: implement linkableBlockNew
  linkableBlockNew : ExecutedBlock → LinkableBlock

module addChild (lb : LinkableBlock) (hv : HashValue) where
  VariantFor : ∀ {ℓ} EL → EL-func {ℓ} EL
  VariantFor EL = EL ErrLog LinkableBlock

  postulate -- TODO-2: implement addChild
    step₀ : VariantFor EitherD
    -- addChild : LinkableBlock → HashValue → Either ErrLog LinkableBlock
    -- addChild lb hv =
    --   if Set.member hv (lb ^∙ lbChildren)
    --   then Left  fakeErr
    --   else Right (lb & lbChildren %~ Set.insert hv)

  E : VariantFor Either
  E = toEither step₀

  D : VariantFor EitherD
  D = fromEither E

addChild = addChild.D

new : ExecutedBlock → QuorumCert → QuorumCert → Usize → Maybe TimeoutCertificate
    → Either ErrLog BlockTree
new root0 rootQuorumCert rootLedgerInfo maxPruned mHighestTimeoutCert = do
  lcheck ((root0 ^∙ ebId) == (rootLedgerInfo ^∙ qcCommitInfo ∙ biId))
         ("BlockTree" ∷ "newBlockTree" ∷ "inconsistent root and ledger info" ∷ [])
  let idToBlock      = Map.insert (root0 ^∙ ebId) (linkableBlockNew root0) Map.empty
      idToQuorumCert = Map.insert (rootQuorumCert ^∙ qcCertifiedBlock ∙ biId) rootQuorumCert Map.empty
      prunedBlockIds = vdNew -- TODO
   in pure $ mkBlockTree
    idToBlock
    (root0 ^∙ ebId)     -- _btRootId
    (root0 ^∙ ebId)     -- _btHighestCertifiedBlockId
    rootQuorumCert      -- _btHighestQuorumCert
    mHighestTimeoutCert
    rootLedgerInfo      -- _btHighestCommitCert
    idToQuorumCert
    prunedBlockIds
    maxPruned

replaceTimeoutCertM : TimeoutCertificate → LBFT Unit
replaceTimeoutCertM tc = do
  lBlockStore ∙ bsInner ∙ btHighestTimeoutCert ?= tc
  logInfo fakeInfo -- lTO (InfoUpdateHighestTimeoutCert (Just tc))

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

module insertBlockE (block : ExecutedBlock)(bt : BlockTree) where
  VariantFor : ∀ {ℓ} EL → EL-func {ℓ} EL
  VariantFor EL = EL ErrLog (BlockTree × ExecutedBlock)

  -- TODO: break into smaller steps to take advantage of the EitherD-weakestpre machinery to prove
  -- the contract.
  step₀ = do
    let blockId = block ^∙ ebId
    caseMD btGetBlock blockId bt of λ where
      (just existingBlock) → pure (bt , existingBlock)
      nothing → caseMD btGetLinkableBlock (block ^∙ ebParentId) bt of λ where
        nothing → LeftD fakeErr
        (just parentBlock) → (do
          parentBlock' ← addChild parentBlock blockId
          let bt' = bt & btIdToBlock ∙~ Map.kvm-insert-Haskell (block ^∙ ebParentId) parentBlock' (bt ^∙ btIdToBlock)
          pure (  (bt' & btIdToBlock ∙~ Map.kvm-insert-Haskell blockId (LinkableBlock∙new block) (bt' ^∙ btIdToBlock))
               , block))

  E : VariantFor Either
  E = toEither step₀

  D : VariantFor EitherD
  D = fromEither E

-- We make the EitherD variant the default, because the only call in code
-- modeled is in EitherD, so it's nice to keep it exactly like the Haskell
-- code being modeled.  However, insertBlockESpec.Contract and the proof of
-- executeAndInsertBlockESpec.contract' (which was written before EitherD
-- support was developed) both want an Either variant, so they use
-- insertBlockE.E.  This demonstrates the flexibility of the VariantOf
-- approach, providing variants for any EitherLike, and means to convert
-- between them easily.
insertBlockE = insertBlockE.D

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

module insertQuorumCertE (qc : QuorumCert) (bt0 : BlockTree) where

  VariantFor : ∀ {ℓ} EL → EL-func {ℓ} EL
  VariantFor EL = EL ErrLog (BlockTree × List InfoLog)

  step₁     : HashValue → VariantFor EitherD
  step₂     : HashValue → ExecutedBlock → VariantFor EitherD
  step₃     : HashValue → ExecutedBlock → ExecutedBlock → VariantFor EitherD
  continue1 : BlockTree → HashValue → ExecutedBlock → List InfoLog → (BlockTree × List InfoLog)
  continue2 : BlockTree → List InfoLog → (BlockTree × List InfoLog)
  here' : List String → List String
  here' t = "BlockTree" ∷ "insertQuorumCert" ∷ t

  blockId = qc ^∙ qcCertifiedBlock ∙ biId

  safetyInvariant = forM_ (Map.elems (bt0 ^∙ btIdToQuorumCert)) $ \x →
          lcheck (   (x  ^∙ qcLedgerInfo ∙ liwsLedgerInfo ∙ liConsensusDataHash
                  ==  qc ^∙ qcLedgerInfo ∙ liwsLedgerInfo ∙ liConsensusDataHash)
                  ∨  (x  ^∙ qcCertifiedBlock ∙ biRound
                  /=  qc ^∙ qcCertifiedBlock ∙ biRound))
                 (here' ("failed check" ∷ "existing qc == qc || existing qc.round /= qc.round" ∷ []))
  step₀ =
    case safetyInvariant of λ where
      (Left  e)    → LeftD e
      (Right unit) → step₁ blockId

  step₁ blockId =
        maybeSD (btGetBlock blockId bt0) (LeftD fakeErr) $ step₂ blockId

  step₂ blockId block =
        maybeSD (bt0 ^∙ btHighestCertifiedBlock) (LeftD fakeErr) $ step₃ blockId block

  step₃ blockId block hcb =
        ifD ((block ^∙ ebRound) >? (hcb ^∙ ebRound))
        then
         (let bt   = bt0 & btHighestCertifiedBlockId ∙~ block ^∙ ebId
                         & btHighestQuorumCert       ∙~ qc
              info = (fakeInfo ∷ [])
           in pure (continue1 bt  blockId block info))
        else  pure (continue1 bt0 blockId block [])

  continue1 bt blockId block info =
    continue2 ( bt & btIdToQuorumCert ∙~ lookupOrInsert blockId qc (bt ^∙ btIdToQuorumCert))
              ( (fakeInfo ∷ info) ++ (if ExecutedBlock.isNilBlock block then fakeInfo ∷ [] else [] ))

  continue2 bt info =
    if-dec (bt ^∙ btHighestCommitCert ∙ qcCommitInfo ∙ biRound) <? (qc ^∙ qcCommitInfo ∙ biRound)
    then ((bt & btHighestCommitCert ∙~ qc) , info)
    else (bt , info)

  E : VariantFor Either
  E = toEither step₀

  D : VariantFor EitherD
  D = fromEither E

insertQuorumCertE = insertQuorumCertE.E

insertQuorumCertM : QuorumCert → LBFT Unit
insertQuorumCertM qc = do
  bt ← use lBlockTree
  case insertQuorumCertE qc bt of λ where
    (Left  e)   → logErr e
    (Right (bt' , info)) → do
      forM_ info logInfo
      lBlockTree ∙= bt'

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

module pathFromRoot (blockId : HashValue) (blockTree : BlockTree) where

  -- TODO-1 PROVE IT TERMINATES
  {-# TERMINATING #-}
  loop : ExecutedBlock → HashValue → List ExecutedBlock → Maybe (HashValue × List ExecutedBlock)
  loop btr curBlockId res = case btGetBlock curBlockId blockTree of λ where
    (just block) → if-dec (block ^∙ ebRound) ≤?ℕ (btr ^∙ ebRound)
                     then just (curBlockId , res)
                     else loop btr (block ^∙ ebParentId) (block ∷ res)
    nothing      → nothing

pathFromRoot : HashValue → BlockTree → Either ErrLog (List ExecutedBlock)
pathFromRoot blockId blockTree =
  maybeS (blockTree ^∙ btRoot) (Left fakeErr) $ λ btr →
  maybeS (loop btr blockId []) (pure []) (pure ∘ continue)
 where

  open pathFromRoot blockId blockTree

  continue : (HashValue × List ExecutedBlock) → List ExecutedBlock
  continue (curBlockId , res) =
    if not (curBlockId /= (blockTree ^∙ btRootId))
    then []
    else res

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

getAllBlockIdM : LBFT (List HashValue)
getAllBlockIdM = Map.kvm-keys <$> use (lBlockTree ∙ btIdToBlock)


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
-}
-- This module defines an intermediate (between an implementation and Abstract) notion
-- of a system state.  The goal is to enable proving for a particular implementation
-- the properties required to provide to Abstract.Properties in order to get the high
-- level correctness conditions, while moving the obligations for the implementation
-- closer to notions more directly provable for an implementation.  However, as our
-- experience has developed with this, it seems that this was not a very effective
-- choice, as it leaves too much burden on the implementation (e.g., proving
-- ∈QC⇒HasBeenSent). Therefore, ...
--
-- TODO-3: Revisit assumptions of the IntermediateSystemState to enable more proof work
-- to be done under Concrete, which can be used by multiple implementations.  As it
-- currently stands, we have specific notions under LibraBFT.Impl that possibly should
-- be provided as module parameters to LibraBFT.Concrete (including IsValidVote and
-- α-ValidVote)

open import LibraBFT.Prelude
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open WithAbsVote

module LibraBFT.Concrete.Intermediate
    (𝓔 : EpochConfig)
    (𝓥 : VoteEvidence 𝓔)
   where
   open import LibraBFT.Abstract.Abstract UID _≟UID_ NodeId 𝓔 𝓥

   -- Since the invariants we want to specify (votes-once and preferred-round-rule),
   -- are predicates over a /System State/, we must factor out the necessary
   -- functionality.
   --
   -- An /IntermediateSystemState/ supports a few different notions; namely,
   record IntermediateSystemState (ℓ : Level) : Set (ℓ+1 ℓ) where
     field
       -- A notion of membership of records
       InSys : Record → Set ℓ

       -- A predicate about whether votes have been transfered
       -- amongst participants
       HasBeenSent : Vote → Set ℓ

       -- Such that, the votes that belong to honest participants inside a
       -- QC that exists in the system must have been sent
       ∈QC⇒HasBeenSent : ∀{q α} → InSys (Q q) → Meta-Honest-Member α
                       → (va : α ∈QC q) → HasBeenSent (∈QC-Vote q va)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
------------------------------------------------------------------------
-- An implementation of tree sort, formally proved to return a
-- permutation of the input
------------------------------------------------------------------------

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

open import Equality
open import Prelude hiding (id; _∘_; List; module List; []; _∷_)

module Container.Tree-sort
  {c⁺}
  (eq : ∀ {a p} → Equality-with-J a p c⁺)
  {A : Type}
  (_≤_ : A → A → Bool) -- A comparison function.
  where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (module _⇔_)

open import Bijection eq using (_↔_; module _↔_)
open import Container eq
open import Container.List eq as List
open import Container.Tree eq as Tree
open import Function-universe eq

------------------------------------------------------------------------
-- Boring lemmas

private

  -- The following lemma is easy to prove automatically (for
  -- instance by using a ring solver).

  lemma₁ : (A B C D : Type) → A ⊎ B ⊎ C ⊎ D ↔ C ⊎ A ⊎ B ⊎ D
  lemma₁ A B C D =
    A ⊎ B ⊎ C ⊎ D      ↔⟨ id ⊎-cong ⊎-assoc ⟩
    A ⊎ (B ⊎ C) ⊎ D    ↔⟨ id ⊎-cong ⊎-comm ⊎-cong id ⟩
    A ⊎ (C ⊎ B) ⊎ D    ↔⟨ ⊎-assoc ⟩
    (A ⊎ C ⊎ B) ⊎ D    ↔⟨ ⊎-assoc ⊎-cong id ⟩
    ((A ⊎ C) ⊎ B) ⊎ D  ↔⟨ (⊎-comm ⊎-cong id) ⊎-cong id ⟩
    ((C ⊎ A) ⊎ B) ⊎ D  ↔⟨ inverse ⊎-assoc ⊎-cong id ⟩
    (C ⊎ A ⊎ B) ⊎ D    ↔⟨ inverse ⊎-assoc ⟩
    C ⊎ (A ⊎ B) ⊎ D    ↔⟨ id ⊎-cong inverse ⊎-assoc ⟩
    C ⊎ A ⊎ B ⊎ D      □

  lemma₂ : {A B C D : Type} (b : Bool) →
           T b × ((A ⊎ B) ⊎ C ⊎ D) ⊎ T (not b) × (B ⊎ C ⊎ A ⊎ D) ↔
           A ⊎ B ⊎ C ⊎ D
  lemma₂ = if-lemma (λ _ → _) (inverse ⊎-assoc) (lemma₁ _ _ _ _)

------------------------------------------------------------------------
-- Insertion into trees

-- Inserts an element into the tree.

insert : A → ⟦ Tree ⟧ A → ⟦ Tree ⟧ A
insert x = Tree.fold
  (singleton x)
  (λ l y r x+l x+r →
     if x ≤ y then node x+l y r
              else node l y x+r)

-- The insert function inserts.

Any-insert : ∀ (P : A → Type) x t →
             Any P (insert x t) ↔ P x ⊎ Any P t
Any-insert P x = Tree.fold-lemma
  (λ t t′ → Any P t′ ↔ P x ⊎ Any P t)

  (λ t₁ t₂ t₁≈t₂ t hyp →
     Any P t         ↔⟨ hyp ⟩
     P x ⊎ Any P t₁  ↔⟨ id ⊎-cong _⇔_.to (∼⇔∼″ t₁ t₂) t₁≈t₂ P ⟩
     P x ⊎ Any P t₂  □)

  (Any P (singleton x)  ↔⟨ Any-singleton P ⟩
   P x                  ↔⟨ inverse ⊎-right-identity ⟩
   P x ⊎ ⊥              ↔⟨ id ⊎-cong inverse (Any-leaf P) ⟩
   P x ⊎ Any P leaf     □)

  (λ l y r l′ r′ ih-l ih-r →
     Any P (if x ≤ y then node l′ y r else node l y r′)   ↔⟨ Any-if P (node l′ y r) (node l y r′) (x ≤ y) ⟩

     T (x ≤ y) × Any P (node l′ y r) ⊎
       T (not (x ≤ y)) × Any P (node l y r′)              ↔⟨ id ×-cong Any-node P ⊎-cong
                                                             id ×-cong Any-node P ⟩
     T (x ≤ y) × (Any P l′ ⊎ P y ⊎ Any P r) ⊎
       T (not (x ≤ y)) × (Any P l ⊎ P y ⊎ Any P r′)       ↔⟨ id ×-cong (ih-l ⊎-cong id) ⊎-cong
                                                             id ×-cong (id ⊎-cong id ⊎-cong ih-r) ⟩
     T (x ≤ y) × ((P x ⊎ Any P l) ⊎ P y ⊎ Any P r) ⊎
       T (not (x ≤ y)) × (Any P l ⊎ P y ⊎ P x ⊎ Any P r)  ↔⟨ lemma₂ (x ≤ y) ⟩

     P x ⊎ Any P l ⊎ P y ⊎ Any P r                        ↔⟨ id ⊎-cong inverse (Any-node P) ⟩

     P x ⊎ Any P (node l y r)                             □)

------------------------------------------------------------------------
-- Turning a list into a search tree

-- Converts the list to a search tree.

to-search-tree : ⟦ List ⟧ A → ⟦ Tree ⟧ A
to-search-tree = List.fold leaf (λ x _ t → insert x t)

-- No elements are added or removed.

to-search-tree≈ : ∀ xs → to-search-tree xs ≈-bag xs
to-search-tree≈ = List.fold-lemma
  (λ xs t → t ≈-bag xs)

  (λ xs ys xs≈ys t t≈xs z →
     z ∈ t   ↔⟨ t≈xs z ⟩
     z ∈ xs  ↔⟨ xs≈ys z ⟩
     z ∈ ys  □)

  (λ z →
     z ∈ leaf  ↔⟨ Any-leaf (λ x → z ≡ x) ⟩
     ⊥         ↔⟨ inverse $ Any-[] (λ x → z ≡ x) ⟩
     z ∈ []    □)

  (λ x xs t t≈xs z →
     z ∈ insert x t  ↔⟨ Any-insert (λ x → z ≡ x) _ _ ⟩
     z ≡ x ⊎ z ∈ t   ↔⟨ id ⊎-cong t≈xs z ⟩
     z ≡ x ⊎ z ∈ xs  ↔⟨ inverse $ Any-∷ (λ x → z ≡ x) ⟩
     z ∈ x ∷ xs      □)

------------------------------------------------------------------------
-- Sorting

-- Sorts a list.

sort : ⟦ List ⟧ A → ⟦ List ⟧ A
sort = flatten ∘ to-search-tree

-- The result is a permutation of the input.

sort≈ : ∀ xs → sort xs ≈-bag xs
sort≈ xs = λ z →
  z ∈ sort xs                      ↔⟨⟩
  z ∈ flatten (to-search-tree xs)  ↔⟨ flatten≈ (to-search-tree xs) _ ⟩
  z ∈ to-search-tree xs            ↔⟨ to-search-tree≈ xs _ ⟩
  z ∈ xs                           □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Type.Identity where

import      Lvl
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

-- Identity type.
-- Also called: Propositional equality.
-- Two terms are identical/equal when their data representation are the same.
data Id {T : Type{ℓ}} : T → T → Type{ℓ} where
  instance intro : ∀{x : T} → Id x x
  -- Interpretation:
  --   The only way to construct something of type Id is to use identical objects for both arguments.
  --   When matching on the constructor, the type checker "unifies" the two terms making them the same.
  --   This is how the builtin pattern matching by intro works, and therefore many propositions for identity becomes "trivial" syntactically.

{-# BUILTIN EQUALITY Id #-}
{-# BUILTIN REWRITE  Id #-}

elim : (P : ∀{x y : T} → (Id x y) → Type{ℓ}) → (∀{x} → P(intro{x = x})) → (∀{x y} → (eq : (Id x y)) → P(eq))
elim _ p intro = p


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" using a partial order
------------------------------------------------------------------------

-- Example uses:
--
--    u≤x : u ≤ x
--    u≤x = begin
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  <⟨ w≤x ⟩
--      x  ∎
--
--    u<x : u < x
--    u<x = begin-strict
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  <⟨ w≤x ⟩
--      x  ∎
--
--    u<e : u < e
--    u<e = begin-strict
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  <⟨ w<x ⟩
--      x  ≤⟨ x≤y ⟩
--      y  <⟨ y<z ⟩
--      z  ≡˘⟨ d≡z ⟩
--      d  ≈˘⟨ e≈d ⟩
--      e  ∎
--
--    u≈w : u ≈ w
--    u≈w = begin-equality
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  ∎

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

open import Relation.Binary

module Relation.Binary.Reasoning.PartialOrder
  {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where

open Poset P
import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as Strict

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

open import Relation.Binary.Reasoning.Base.Triple
  isPreorder
  (Strict.trans isPartialOrder)
  (Strict.<-resp-≈ isEquivalence ≤-resp-≈)
  Strict.<⇒≤
  (Strict.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈)
  (Strict.≤-<-trans trans antisym ≤-respˡ-≈)
  public

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

-- Version 1.0

infixr 2 _≈⟨⟩_

_≈⟨⟩_ = _≡⟨⟩_
{-# WARNING_ON_USAGE _≈⟨⟩_
"Warning: _≈⟨⟩_ was deprecated in v1.0.
Please use _≡⟨⟩_ instead."
#-}


text:
{-

  Homotopy colimits of graphs

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Colimit.Base where

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Graph

-- Cones under a diagram

record Cocone ℓ {ℓd ℓv ℓe} {I : Graph ℓv ℓe} (F : Diag ℓd I) (X : Type ℓ)
              : Type (ℓ-suc (ℓ-max ℓ (ℓ-max (ℓ-max ℓv ℓe) (ℓ-suc ℓd)))) where
  field
    leg : ∀ (j : Obj I) → F $ j → X
    com : ∀ {j k} (f : Hom I j k) → leg k ∘ F <$> f ≡ leg j

  postcomp : ∀ {ℓ'} {Y : Type ℓ'} → (X → Y) → Cocone ℓ' F Y
  leg (postcomp h) j = h ∘ leg j
  com (postcomp h) f = cong (h ∘_) (com f)

open Cocone public

-- Σ (Type ℓ) (Cocone ℓ F) forms a category:

module _ {ℓd ℓv ℓe} {I : Graph ℓv ℓe} {F : Diag ℓd I} where

  private
    -- the "lower star" functor
    _* : ∀ {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'} → (X → Y) → Cocone _ F X → Cocone _ F Y
    (h *) C = postcomp C h

  CoconeMor : ∀ {ℓ ℓ'} → Σ (Type ℓ) (Cocone ℓ F) → Σ (Type ℓ') (Cocone ℓ' F) → Type _
  CoconeMor (X , C) (Y , D) = Σ[ h ∈ (X → Y) ] (h *) C ≡ D

  idCoconeMor : ∀ {ℓ} (Cp : Σ (Type ℓ) (Cocone ℓ F)) → CoconeMor Cp Cp
  idCoconeMor Cp = (λ x → x) , refl

  compCoconeMor : ∀ {ℓ ℓ' ℓ''} {C : Σ (Type ℓ) (Cocone ℓ F)} {D : Σ (Type ℓ') (Cocone ℓ' F)}
                    {E : Σ (Type ℓ'') (Cocone ℓ'' F)}
                  → CoconeMor D E → CoconeMor C D → CoconeMor C E
  compCoconeMor (g , q) (f , p) = g ∘ f , (cong (g *) p) ∙ q

-- Universal cocones are initial objects in the category Σ (Type ℓ) (Cocone ℓ F)

module _ {ℓ ℓd ℓv ℓe} {I : Graph ℓv ℓe} {F : Diag ℓd I} {X : Type ℓ} where

  isUniversalAt : ∀ ℓq → Cocone ℓ F X → Type (ℓ-max ℓ (ℓ-suc (ℓ-max ℓq (ℓ-max (ℓ-max ℓv ℓe) (ℓ-suc ℓd)))))
  isUniversalAt ℓq C = ∀ (Y : Type ℓq) → isEquiv {A = (X → Y)} {B = Cocone ℓq F Y} (postcomp C)
                  -- (unfolding isEquiv, this ^ is equivalent to what one might expect:)
                  -- ∀ (Y : Type ℓ) (D : Cocone ℓ F Y) → isContr (Σ[ h ∈ (X → Y) ] (h *) C ≡ D)
                  --                                  (≡ isContr (CoconeMor (X , C) (Y , D)))

  isPropIsUniversalAt : ∀ ℓq (C : Cocone ℓ F X) → isProp (isUniversalAt ℓq C)
  isPropIsUniversalAt ℓq C = propPi (λ Y → isPropIsEquiv (postcomp C))

  isUniversal : Cocone ℓ F X → Typeω
  isUniversal C = ∀ ℓq → isUniversalAt ℓq C

-- Colimits are universal cocones

record isColimit {ℓ ℓd ℓv ℓe} {I : Graph ℓv ℓe} (F : Diag ℓd I) (X : Type ℓ) : Typeω where
  field
    cone : Cocone ℓ F X
    univ : isUniversal cone
open isColimit public

module _ {ℓ ℓ' ℓd ℓv ℓe} {I : Graph ℓv ℓe} {F : Diag ℓd I} {X : Type ℓ} {Y : Type ℓ'} where

  postcomp⁻¹ : isColimit F X → Cocone ℓ' F Y → (X → Y)
  postcomp⁻¹ cl = invEq (_ , univ cl _ Y)

  postcomp⁻¹-inv : (cl : isColimit F X) (D : Cocone ℓ' F Y) → (postcomp (cone cl) (postcomp⁻¹ cl D)) ≡ D
  postcomp⁻¹-inv cl D = retEq (_ , univ cl _ Y) D

  postcomp⁻¹-mor : (cl : isColimit F X) (D : Cocone ℓ' F Y) → CoconeMor (X , cone cl) (Y , D)
  postcomp⁻¹-mor cl D = (postcomp⁻¹ cl D) , (postcomp⁻¹-inv cl D)

-- Colimits are unique

module _ {ℓ ℓ' ℓd ℓv ℓe} {I : Graph ℓv ℓe} {F : Diag ℓd I} {X : Type ℓ} {Y : Type ℓ'} where

  uniqColimit : isColimit F X → isColimit F Y → X ≃ Y
  uniqColimit cl cl'
    = isoToEquiv (iso (fst fwd) (fst bwd)
                      (λ x i → fst (isContr→isProp (equiv-proof (univ cl' ℓ' Y) (cone cl'))
                                                   (compCoconeMor fwd bwd)
                                                   (idCoconeMor (Y , cone cl')) i) x)
                      (λ x i → fst (isContr→isProp (equiv-proof (univ cl ℓ  X) (cone cl))
                                                   (compCoconeMor bwd fwd)
                                                   (idCoconeMor (X , cone cl)) i) x))
    where fwd : CoconeMor (X , cone cl ) (Y , cone cl')
          bwd : CoconeMor (Y , cone cl') (X , cone cl )
          fwd = postcomp⁻¹-mor cl (cone cl')
          bwd = postcomp⁻¹-mor cl' (cone cl)

-- Colimits always exist

data colim {ℓd ℓe ℓv} {I : Graph ℓv ℓe} (F : Diag ℓd I) : Type (ℓ-suc (ℓ-max (ℓ-max ℓv ℓe) (ℓ-suc ℓd))) where
  colim-leg : ∀ (j : Obj I) → F $ j → colim F
  colim-com : ∀ {j k} (f : Hom I j k) → colim-leg k ∘ F <$> f ≡ colim-leg j

module _ {ℓd ℓv ℓe} {I : Graph ℓv ℓe} {F : Diag ℓd I} where

  colimCone : Cocone _ F (colim F)
  leg colimCone = colim-leg
  com colimCone = colim-com

  colim-rec : ∀ {ℓ} {X : Type ℓ} → Cocone ℓ F X → (colim F → X)
  colim-rec C (colim-leg j A)   = leg C j A
  colim-rec C (colim-com f i A) = com C f i A

  colimIsColimit : isColimit F (colim F)
  cone colimIsColimit = colimCone
  univ colimIsColimit ℓq Y
    = isoToIsEquiv record { fun = postcomp colimCone
                          ; inv = colim-rec
                          ; rightInv = λ C → refl
                          ; leftInv  = λ h → funExt (eq h) }
    where eq : ∀ h (x : colim _) → colim-rec (postcomp colimCone h) x ≡ h x
          eq h (colim-leg j A)   = refl
          eq h (colim-com f i A) = refl

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Pos where

  import Prelude
  import Equiv
  import Datoid
  import Nat

  open Prelude
  open Equiv
  open Datoid

  abstract

    Pos : Set
    Pos = Nat.Nat

    one : Pos
    one = Nat.zero

    suc : Pos -> Pos
    suc = Nat.suc

    suc' : Nat.Nat -> Pos
    suc' n = n

    _+_ : Pos -> Pos -> Pos
    m + n = suc (Nat._+_ m n)

    -- Returns Nothing if input is 1.
    pred : Pos -> Maybe Pos
    pred Nat.zero    = Nothing
    pred (Nat.suc n) = Just n

    toNat : Pos -> Nat.Nat
    toNat = suc

    decidableEquiv : DecidableEquiv Pos
    decidableEquiv = Nat.decidableEquiv

  posDatoid : Datoid
  posDatoid = datoid Pos decidableEquiv

  sucPred : Maybe Pos -> Pos
  sucPred Nothing  = one
  sucPred (Just p) = suc p

  data Pred (p : Pos) (mP : Maybe Pos) : Set where
    ok : datoidRel posDatoid (sucPred mP) p -> Pred p mP

  abstract

    -- Returns Nothing if input is 1.
    predOK : (p : Pos) -> Pred p (pred p)
    predOK Nat.zero    = ok (dRefl posDatoid {one})
    predOK (Nat.suc n) = ok (dRefl posDatoid {n})

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Monad where

open import Level

open import Category
import Functor
import Nat
import Adjoint

open Category.Category
open Functor.Functor
open Nat.Export
open Nat.Nat
open Adjoint.Export

record Monad {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) : Set (suc (c₀ ⊔ c₁ ⊔ ℓ)) where
  field
    MFunctor : Functor.Functor C C
    Mjoin : Nat.Nat (Functor.exp MFunctor 2) MFunctor
    Munit : Nat.Nat (Functor.identity C) MFunctor

  field
    join_join : {A : Obj C} → C [ C [ component Mjoin A ∘ component Mjoin (fobj MFunctor A) ] ≈ C [ component Mjoin A ∘ fmap MFunctor (component Mjoin A) ] ]
    unit_MFunctor : {A : Obj C} → C [ C [ component Mjoin A ∘ component Munit (fobj MFunctor A) ] ≈ id C ]
    MFunctor_unit : {A : Obj C} → C [ C [ component Mjoin A ∘ fmap MFunctor (component Munit A) ] ≈ id C ]

Adjoint-Monad : ∀ {C₀ C₁ ℓ} {C D : Category C₀ C₁ ℓ} {F : Functor.Functor C D} {G : Functor.Functor D C} → F ⊣ G → Monad C
Adjoint-Monad {C = C} {D} {F} {G} F⊣G = record {
  MFunctor = T;
  Mjoin = record {
    component = λ X → component (G F∘N ε N∘F F) X ;
    naturality = λ {a} {b} {f} → begin⟨ C ⟩
      C [ component (G F∘N ε N∘F F) b ∘ fmap G (fmap (Functor.compose F T) f) ] ≈⟨ sym-hom C (preserveComp G) ⟩
      fmap G (D [ component ε (fobj F b) ∘ fmap (Functor.compose F G) (fmap F f) ]) ≈⟨ Functor.preserveEq G (naturality ε) ⟩
      fmap G (D [ fmap F f ∘ component ε (fobj F a) ]) ≈⟨ preserveComp G ⟩
      C [ fmap T f ∘ component (G F∘N ε N∘F F) a ]
      ∎ };
  Munit = Adjoint.unit F⊣G;
  join_join = λ {A} → begin⟨ C ⟩
    C [ component (G F∘N ε N∘F F) A ∘ component (G F∘N ε N∘F F) (fobj T A) ] ≈⟨ sym-hom C (preserveComp G) ⟩
    fmap G (D [ component ε (fobj F A) ∘ component ε (fobj (Functor.compose F G) (fobj F A)) ]) ≈⟨ Functor.preserveEq G (sym-hom D (naturality ε)) ⟩
    fmap G (D [ component ε (fobj F A) ∘ fmap (Functor.compose F G) (component ε (fobj F A)) ]) ≈⟨ preserveComp G ⟩
    C [ component (G F∘N ε N∘F F) A ∘ fmap T (component (G F∘N ε N∘F F) A) ]
    ∎ ;
  unit_MFunctor = λ {A} → begin⟨ C ⟩
    C [ component (G F∘N ε N∘F F) A ∘ component η (fobj T A) ] ≈⟨ refl-hom C ⟩
    C [ component (G F∘N ε) (fobj F A) ∘ component (η N∘F G) (fobj F A) ] ≈⟨ sym-hom C (≈-composite C (leftId C) (trans-hom C (leftId C) (rightId C))) ⟩
    C [ C [ id C ∘ component (G F∘N ε) (fobj F A) ] ∘ C [ id C ∘ C [ component (η N∘F G) (fobj F A) ∘ id C ] ] ] ≈⟨ refl-hom C ⟩
    component (Nat.compose (Nat.compose {H = G} Nat.rightIdNat→ (G F∘N ε)) (Nat.compose (Nat.assocNat→ {F = G} {F} {G}) (Nat.compose (η N∘F G) Nat.leftIdNat←))) (fobj F A) ≈⟨ Adjoint.triangularR F⊣G {fobj F A} ⟩
    component (id [ D , C ] {G}) (fobj F A) ≈⟨ refl-hom C ⟩
    id C
    ∎ ;
  MFunctor_unit = λ {A} → begin⟨ C ⟩
    C [ component (G F∘N ε N∘F F) A ∘ fmap T (component η A) ] ≈⟨ refl-hom C ⟩
    C [ fmap G (component ε (fobj F A)) ∘ fmap G (fmap F (component η A)) ] ≈⟨ sym-hom C (preserveComp G) ⟩
    fmap G (D [ component ε (fobj F A) ∘ fmap F (component η A) ]) ≈⟨ Functor.preserveEq G (≈-composite D (sym-hom D (leftId D)) (sym-hom D (trans-hom D (leftId D) (rightId D)))) ⟩
    fmap G (D [ D [ id D ∘ component ε (fobj F A) ] ∘ D [ id D ∘ D [ fmap F (component η A) ∘ id D ] ] ]) ≈⟨ Functor.preserveEq G (refl-hom D) ⟩
    fmap G (component (Nat.compose (Nat.compose Nat.leftIdNat→ (Adjoint.counit F⊣G N∘F F)) (Nat.compose {F = F} (Nat.assocNat← {F = F} {G} {F}) (Nat.compose {F = F} (F F∘N Adjoint.unit F⊣G) Nat.rightIdNat←))) A ) ≈⟨ Functor.preserveEq G (Adjoint.triangularL F⊣G {A}) ⟩
    fmap G (component (id [ C , D ] {F}) A) ≈⟨ preserveId G ⟩
    id C
    ∎ }
  where
    T = Functor.compose G F
    η = Adjoint.unit F⊣G
    ε = Adjoint.counit F⊣G

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


text:
module char where

open import bool
open import nat
open import eq
open import product
open import product-thms

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

postulate
  char : Set

{-# BUILTIN CHAR char #-}

----------------------------------------------------------------------
-- primitive operations
----------------------------------------------------------------------

private
 primitive
  primCharToNat    : char → ℕ
  primCharEquality : char → char → 𝔹

toNat : char → ℕ
toNat = primCharToNat

infix 4 _=char_

_=char_ : char → char → 𝔹
_=char_ = primCharEquality

postulate
  ≡char-to-= : (c1 c2 : char) → c1 ≡ c2 → _=char_ c1 c2 ≡ tt
  =char-to-≡ : (c1 c2 : char) → _=char_ c1 c2 ≡ tt → c1 ≡ c2

=char-sym : (c1 c2 : char) → (c1 =char c2) ≡ (c2 =char c1)
=char-sym c1 c2 with keep (c1 =char c2)
=char-sym c1 c2 | tt , p rewrite =char-to-≡ c1 c2 p = refl
=char-sym c1 c2 | ff , p with keep (c2 =char c1)
=char-sym c1 c2 | ff , p | tt , p' rewrite =char-to-≡ c2 c1 p' = refl
=char-sym c1 c2 | ff , p | ff , p' rewrite p | p' = refl

postulate
  _<char_ : char → char → 𝔹

{-# COMPILED _<char_ (<)   #-}

----------------------------------------------------------------------
-- defined operations
----------------------------------------------------------------------

-- is a decimal digit
is-digit : char → 𝔹
is-digit '0' = tt
is-digit '1' = tt
is-digit '2' = tt
is-digit '3' = tt
is-digit '4' = tt
is-digit '5' = tt
is-digit '6' = tt
is-digit '7' = tt
is-digit '8' = tt
is-digit '9' = tt
is-digit _ = ff

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


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

-- https://personal.cis.strath.ac.uk/conor.mcbride/pub/DepRep/DepRep.pdf

module Experiment.Outrageous.#03 where

open import Experiment.Outrageous.#02

data U : Set
El : U → Set

data U where
  :Zero: :𝟏: :𝟐: :ℕ: : U
  :Π: :Σ: : (S : U) → (El S → U) → U
El :Zero: = Zero
El :𝟏:    = 𝟏
El :𝟐:    = 𝟐
El :ℕ:    = ℕ
El (:Π: S T) = (s : El S) → El (T s)
El (:Σ: S T) = Σ (El S) λ s → El (T s)

_:→:_ : U → U → U
S :→: T = :Π: S λ _ → T

_:×:_ : U → U → U
S :×: T = :Σ: S λ _ → T

:If: : 𝟐 → U → U → U
:If: tt T F = T
:If: ff T F = F

:Vec: : U → ℕ → U
:Vec: X ze     = :𝟏:
:Vec: X (su n) = X :×: :Vec: X n


text:
------------------------------------------------------------------------------
-- Fairness of the ABP channels
------------------------------------------------------------------------------

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

module FOTC.Program.ABP.Fair.Type where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- The Fair co-inductive predicate

-- From (Dybjer and Sander 1989): al : F*T if al is a list of zero or
-- more 0's followed by a final 1.
data F*T : D → Set where
  f*tnil  : F*T (T ∷ [])
  f*tcons : ∀ {ft} → F*T ft → F*T (F ∷ ft)

-- Functor for the Fair type.
-- FairF : (D → Set) → D → Set
-- FairF A os = ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ A os'

-- Fair is the greatest fixed of FairF (by Fair-out and Fair-coind).

postulate Fair : D → Set

-- Fair a is post-fixed point of FairF, i.e.
--
-- Fair ≤ FairF Fair.
postulate Fair-out : ∀ {os} → Fair os →
                     ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ Fair os'
{-# ATP axiom Fair-out #-}

-- Fair is the greatest post-fixed point of FairF, i.e.
--
-- ∀ A. A ≤ FairF A ⇒ A ≤ Fair.
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  Fair-coind :
    (A : D → Set) →
    -- A is post-fixed point of FairF.
    (∀ {os} → A os → ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ A os') →
    -- Fair is greater than A.
    ∀ {os} → A os → Fair os

------------------------------------------------------------------------------
-- References
--
-- Dybjer, Peter and Sander, Herbert P. (1989). A Functional
-- Programming Approach to the Specification and Verification of
-- Concurrent Systems. Formal Aspects of Computing 1, pp. 303–319.


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

module Math.NumberTheory.Fibonacci.Nat where

-- agda-stdlib
open import Data.Nat
open import Data.Nat.Properties

-- agda-misc
open import Math.NumberTheory.Fibonacci.Generic +-0-commutativeMonoid 0 1
  renaming
  ( fibRec≈fib to fibRec≡fib
  ; fib[2+n]≈fib[1+n]∙fib[n] to fib[2+n]≡fib[1+n]+fib[n]
  ; fib[1+n]∙fib[n]≈fib[2+n] to fib[1+n]+fib[n]≡fib[2+n]
  ; fib[n]∙fib[1+n]≈fib[2+n] to fib[n]+fib[1+n]≡fib[2+n]
  ) public


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

open import Base
open import Homotopy.PushoutDef
open import Homotopy.VanKampen.Guide

module Homotopy.VanKampen.SplitCode {i} (d : pushout-diag i)
  (l : legend i (pushout-diag.C d)) (a₁ : pushout-diag.A d) where

  open pushout-diag d
  open legend l

  open import Homotopy.Truncation
  open import Homotopy.PathTruncation

  -- Definition.
  module _ where
    private
      data #code-a (a₂ : A) : Set i
      data #code-b (b₂ : B) : Set i

      data #code-a a₂ where
        #a : a₁ ≡₀ a₂ → #code-a a₂
        #ba : ∀ n → #code-b (g $ loc n) → f (loc n) ≡₀ a₂ → #code-a a₂
      data #code-b b₂ where
        #ab : ∀ n → #code-a (f $ loc n) → g (loc n) ≡₀ b₂ → #code-b b₂

    code-b : B → Set i
    code-b = #code-b

    code-a : A → Set i
    code-a = #code-a

    postulate -- HIT
      code-a-is-set : ∀ a → is-set (code-a a)
      code-b-is-set : ∀ b → is-set (code-b b)

    a : ∀ {a₂} → a₁ ≡₀ a₂ → code-a a₂
    a = #a

    infixl 6 a
    syntax a co = ⟧a co

    ba : ∀ {a₂} n → code-b (g $ loc n) → f (loc n) ≡₀ a₂ → code-a a₂
    ba = #ba

    infixl 6 ba
    syntax ba n co p = co b⟦ n ⟧a p

    ab : ∀ {b₂} n → code-a (f $ loc n) → g (loc n) ≡₀ b₂ → code-b b₂
    ab = #ab

    infixl 6 ab
    syntax ab n co p = co a⟦ n ⟧b p

    postulate -- HIT
      code-a-refl-refl : ∀ n (co : code-a (f $ loc n))
        → co a⟦ n ⟧b refl₀ b⟦ n ⟧a refl₀ ≡ co
      code-b-refl-refl : ∀ n (co : code-b (g $ loc n))
        → co b⟦ n ⟧a refl₀ a⟦ n ⟧b refl₀ ≡ co
      -- The other diriction is fine.
      -- There's no canonical choice between two, I think.
      code-ab-swap : ∀ n₁ co n₂ (r : loc n₁ ≡₀ loc n₂)
        → co a⟦ n₁ ⟧b ap₀ g r b⟦ n₂ ⟧a refl₀
        ≡ co a⟦ n₁ ⟧b refl₀ b⟦ n₁ ⟧a ap₀ f r

    -- Dependent recursor.
    code-rec : ∀ {j}
      (P-a : ∀ {a₂} → code-a a₂ → Set j) ⦃ _ : ∀ {a₂} co → is-set $ P-a {a₂} co ⦄
      (P-b : ∀ {b₂} → code-b b₂ → Set j) ⦃ _ : ∀ {b₂} co → is-set $ P-b {b₂} co ⦄
      (h₀-a : ∀ {a₂} (p : _ ≡₀ a₂) → P-a (a p))
      (h₀-ba : ∀ {a₂} n {co} (_ : P-b co) (p : _ ≡₀ a₂)
        → P-a (co b⟦ n ⟧a p))
      (h₀-ab : ∀ {b₂} n {co} (_ : P-a co) (p : _ ≡₀ b₂)
        → P-b (co a⟦ n ⟧b p))
      (h₁-a-rr : ∀ n {co} (pco : P-a co) →
        transport (P-a {f $ loc n}) (code-a-refl-refl n co)
          (h₀-ba n (h₀-ab n pco $ refl₀) $ refl₀)
        ≡ pco)
      (h₁-b-rr : ∀ n {co} (pco : P-b co) →
        transport (P-b {g $ loc n}) (code-b-refl-refl n co)
          (h₀-ab n (h₀-ba n pco $ refl₀) $ refl₀)
        ≡ pco)
      (h₁-ab-s : ∀ n₁ {co} (pco : P-a co) n₂ r →
        transport (P-a {f $ loc n₂}) (code-ab-swap n₁ co n₂ r)
          (h₀-ba n₂ (h₀-ab n₁ pco $ ap₀ g r) $ refl₀)
        ≡ (h₀-ba n₁ (h₀-ab n₁ pco $ refl₀) $ ap₀ f r))
      → (∀ {a₂} (co : code-a a₂) → P-a co)
      × (∀ {b₂} (co : code-b b₂) → P-b co)
    code-rec P-a P-b h₀-a h₀-ba h₀-ab _ _ _ = elim-a , elim-b
      where
        elim-a : ∀ {a₂} (co : code-a a₂) → P-a co
        elim-b : ∀ {b₂} (co : code-b b₂) → P-b co
        elim-a (#a       p) = h₀-a                p
        elim-a (#ba n co p) = h₀-ba n (elim-b co) p
        elim-b (#ab n co p) = h₀-ab n (elim-a co) p

    -- This is actually "partially dependent".
    -- P-a and P-b are indexed by the end points.
    -- This is fine because they are fixed in
    -- all transports in 1-cells.
    code-rec-nondep : ∀ {j}
      (P-a : A → Set j) ⦃ _ : ∀ a → is-set $ P-a a ⦄
      (P-b : B → Set j) ⦃ _ : ∀ b → is-set $ P-b b ⦄
      (h₀-a : ∀ {a₂} (p : a₁ ≡₀ a₂) → P-a a₂)
      (h₀-ba : ∀ {a₂} n {co : code-b (g $ loc n)} → P-b (g $ loc n)
        → f (loc n) ≡₀ a₂ → P-a a₂)
      (h₀-ab : ∀ {b₂} n {co : code-a (f $ loc n)} → P-a (f $ loc n)
        → g (loc n) ≡₀ b₂ → P-b b₂)
      (h₁-a-rr : ∀ n {co} (pco : P-a (f $ loc n))
        → h₀-ba n {co a⟦ n ⟧b refl₀} (h₀-ab n {co} pco $ refl₀) refl₀ ≡ pco)
      (h₁-b-rr : ∀ n {co} (pco : P-b (g $ loc n))
        → h₀-ab n {co b⟦ n ⟧a refl₀} (h₀-ba n {co} pco $ refl₀) refl₀ ≡ pco)
      (h₁-ab-s : ∀ n₁ {co : code-a $ f $ loc n₁} (pco : P-a $ f $ loc n₁) n₂ (r : loc n₁ ≡₀ loc n₂) →
          h₀-ba n₂ {co a⟦ n₁ ⟧b ap₀ g r} (h₀-ab n₁ {co} pco $ ap₀ g r) refl₀
        ≡ h₀-ba n₁ {co a⟦ n₁ ⟧b refl₀} (h₀-ab n₁ {co} pco $ refl₀) (ap₀ f r))
      → (∀ {a₂} (co : code-a a₂) → P-a a₂)
      × (∀ {b₂} (co : code-b b₂) → P-b b₂)
    code-rec-nondep P-a P-b h₀-a h₀-ba h₀-ab _ _ _ = elim-a , elim-b
      where
        elim-a : ∀ {a₂} (co : code-a a₂) → P-a a₂
        elim-b : ∀ {b₂} (co : code-b b₂) → P-b b₂
        elim-a (#a       p) = h₀-a                     p
        elim-a (#ba c co p) = h₀-ba c {co} (elim-b co) p
        elim-b (#ab c co p) = h₀-ab c {co} (elim-a co) p

  module _ where
    trans-a : ∀ {y z} (q : y ≡ z) (p : a₁ ≡₀ y)
      → transport code-a q (⟧a p) ≡ ⟧a (p ∘₀ proj q)
    trans-a refl p = ap a (! (refl₀-right-unit p))

    trans-ba : ∀ {y z} (q : y ≡ z) n co (p : f (loc n) ≡₀ y)
      → transport code-a q (co b⟦ n ⟧a p) ≡ co b⟦ n ⟧a p ∘₀ proj q
    trans-ba refl n co p = ap (ba n co) (! (refl₀-right-unit p))

    trans-ab : ∀ {y b} (q : y ≡ b) n co (p : g (loc n) ≡₀ y)
      → transport code-b q (co a⟦ n ⟧b p) ≡ co a⟦ n ⟧b p ∘₀ proj q
    trans-ab refl n co p = ap (ab n co) (! (refl₀-right-unit p))

  module _ where
    -- all-paths
    abstract
      code-has-all-cells₂-a : ∀ {a} {x y : code-a a} (p q : x ≡ y) → p ≡ q
      code-has-all-cells₂-a = prop-has-all-paths $ code-a-is-set _ _ _

      code-has-all-cells₂-b : ∀ {b} {x y : code-b b} (p q : x ≡ y) → p ≡ q
      code-has-all-cells₂-b = prop-has-all-paths $ code-b-is-set _ _ _

    code-a-rec : ∀ {j}
      (P-a : ∀ {a₂} → code-a a₂ → Set j) ⦃ _ : ∀ {a₂} co → is-set $ P-a {a₂} co ⦄
      (h₀-a : ∀ {a₂} (p : _ ≡₀ a₂) → P-a (⟧a p))
      (h₀-ba : ∀ {a₂} n co (p : _ ≡₀ a₂)
        → P-a (co b⟦ n ⟧a p))
      (h₁-a-rr : ∀ n {co} (pco : P-a co) →
        transport (P-a {f $ loc n}) (code-a-refl-refl n co)
          (h₀-ba n (co a⟦ n ⟧b refl₀) $ refl₀)
        ≡ pco)
      → (∀ {a₂} (co : code-a a₂) → P-a co)
    code-a-rec {j} P-a ⦃ P-a-is-set ⦄ h₀-a h₀-ba h₁-a-rr = π₁ $ code-rec
      P-a ⦃ P-a-is-set ⦄
      (λ _ → unit) ⦃ λ _ → unit-is-set ⦄
      h₀-a
      (λ n {co} _ p → h₀-ba n co p)
      (λ _ _ _ → tt)
      h₁-a-rr
      (λ _ _ → prop-has-all-paths unit-is-prop _ _)
      -- FIXME This proof is too ugly.
      (λ n₁ {co} (pco : P-a co) n₂ r →
        transport (P-a {f $ loc n₂}) (code-ab-swap n₁ co n₂ r)
          (h₀-ba n₂ (co a⟦ n₁ ⟧b ap₀ g r) $ refl₀)
            ≡⟨ ! $ h₁-a-rr n₂ _ ⟩
        transport (P-a {f $ loc n₂}) (code-a-refl-refl n₂ _)
          (h₀-ba n₂ (_ a⟦ n₂ ⟧b refl₀) $ refl₀)
            ≡⟨ ap (λ x → transport (P-a {f $ loc n₂}) (code-a-refl-refl n₂ _)
                $ h₀-ba n₂ (_ a⟦ n₂ ⟧b refl₀) $ refl₀) $ code-ab-swap n₁ co n₂ r ⟩
        transport (P-a {f $ loc n₂}) (code-a-refl-refl n₂ _)
          (h₀-ba n₂ (_ a⟦ n₂ ⟧b refl₀) $ refl₀)
            ≡⟨ h₁-a-rr n₂ _ ⟩∎
        h₀-ba n₁ (co a⟦ n₁ ⟧b refl₀) (ap₀ f r)
            ∎)

    code-b-rec : ∀ {j}
      (P-b : ∀ {b₂} → code-b b₂ → Set j) ⦃ _ : ∀ {b₂} co → is-set $ P-b {b₂} co ⦄
      (h₀-ab : ∀ {b₂} n co (p : _ ≡₀ b₂)
        → P-b (co a⟦ n ⟧b p))
      (h₁-b-rr : ∀ n {co} (pco : P-b co) →
        transport (P-b {g $ loc n}) (code-b-refl-refl n co)
          (h₀-ab n (co b⟦ n ⟧a refl₀) $ refl₀)
        ≡ pco)
      → (∀ {b₂} (co : code-b b₂) → P-b co)
    code-b-rec {j} P-b ⦃ P-b-is-set ⦄ h₀-ab h₁-b-rr = π₂ $ code-rec
      (λ _ → unit) ⦃ λ _ → unit-is-set ⦄
      P-b ⦃ P-b-is-set ⦄
      (λ _ → tt)
      (λ _ _ _ → tt)
      (λ n {co} _ p → h₀-ab n co p)
      (λ _ _ → prop-has-all-paths unit-is-prop _ _)
      h₁-b-rr
      (λ _ _ _ _ → prop-has-all-paths unit-is-prop _ _)

  -- Derived 1-cells.
  module _ where
    abstract
      code-ba-swap : ∀ n₁ co n₂ (r : loc n₁ ≡₀ loc n₂)
        → co b⟦ n₁ ⟧a ap₀ f r a⟦ n₂ ⟧b refl₀
        ≡ co b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b ap₀ g r
      code-ba-swap n₁ co n₂ r =
        co                                   b⟦ n₁ ⟧a ap₀ f r a⟦ n₂ ⟧b refl₀
          ≡⟨ ap (λ x → x b⟦ n₁ ⟧a ap₀ f r a⟦ n₂ ⟧b refl₀) $ ! $ code-b-refl-refl n₁ co ⟩
        co b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b refl₀ b⟦ n₁ ⟧a ap₀ f r a⟦ n₂ ⟧b refl₀
          ≡⟨ ap (λ x → x a⟦ n₂ ⟧b refl₀) $ ! $ code-ab-swap n₁ (co b⟦ n₁ ⟧a refl₀) n₂ r ⟩
        co b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b ap₀ g r b⟦ n₂ ⟧a refl₀ a⟦ n₂ ⟧b refl₀
          ≡⟨ code-b-refl-refl n₂ $ co b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b ap₀ g r ⟩∎
        co b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b ap₀ g r
          ∎

    abstract
      -- Old (provable) rules.
      code-a-merge : ∀ {a₂} n p₁ (p₂ : _ ≡₀ a₂)
        → ⟧a p₁ a⟦ n ⟧b refl₀ b⟦ n ⟧a p₂
        ≡ ⟧a p₁            ∘₀           p₂
      code-a-merge {a₂} n p₁ = π₀-extend
        ⦃ λ _ → ≡-is-set $ code-a-is-set a₂ ⦄
        ( λ p₂ →
            ⟧a p₁ a⟦ n ⟧b refl₀ b⟦ n ⟧a proj p₂
              ≡⟨ ! $ trans-ba p₂ n (⟧a p₁ a⟦ n ⟧b refl₀) refl₀ ⟩
            transport code-a p₂ (⟧a p₁ a⟦ n ⟧b refl₀ b⟦ n ⟧a refl₀)
              ≡⟨ ap (transport code-a p₂) $ code-a-refl-refl n (⟧a p₁) ⟩
            transport code-a p₂ (⟧a p₁)
              ≡⟨ trans-a p₂ p₁ ⟩∎
            ⟧a p₁ ∘₀ proj p₂
              ∎)

    abstract
      code-ab-merge : ∀ {b₂} n₁ co n₂ p₁ (p₂ : _ ≡₀ b₂)
        → co a⟦ n₁ ⟧b p₁ b⟦ n₂ ⟧a refl₀ a⟦ n₂ ⟧b p₂
        ≡ co a⟦ n₁ ⟧b p₁             ∘₀            p₂
      code-ab-merge {b₂} n₁ co n₂ p₁ = π₀-extend
        ⦃ λ _ → ≡-is-set $ code-b-is-set b₂ ⦄
        ( λ p₂ →
            co a⟦ n₁ ⟧b p₁ b⟦ n₂ ⟧a refl₀ a⟦ n₂ ⟧b proj p₂
              ≡⟨ ! $ trans-ab p₂ n₂ (co a⟦ n₁ ⟧b p₁ b⟦ n₂ ⟧a refl₀) refl₀ ⟩
            transport code-b p₂ (co a⟦ n₁ ⟧b p₁ b⟦ n₂ ⟧a refl₀ a⟦ n₂ ⟧b refl₀)
              ≡⟨ ap (transport code-b p₂) $ code-b-refl-refl n₂ (co a⟦ n₁ ⟧b p₁) ⟩
            transport code-b p₂ (co a⟦ n₁ ⟧b p₁)
              ≡⟨ trans-ab p₂ n₁ co p₁ ⟩∎
            co a⟦ n₁ ⟧b p₁ ∘₀ proj p₂
              ∎)

    abstract
      code-ba-merge : ∀ {a₂} n₁ co n₂ p₁ (p₂ : _ ≡₀ a₂)
        → co b⟦ n₁ ⟧a p₁ a⟦ n₂ ⟧b refl₀ b⟦ n₂ ⟧a p₂
        ≡ co b⟦ n₁ ⟧a p₁             ∘₀            p₂
      code-ba-merge {a₂} n₁ co n₂ p₁ = π₀-extend
        ⦃ λ _ → ≡-is-set $ code-a-is-set a₂ ⦄
        ( λ p₂ →
            co b⟦ n₁ ⟧a p₁ a⟦ n₂ ⟧b refl₀ b⟦ n₂ ⟧a proj p₂
              ≡⟨ ! $ trans-ba p₂ n₂ (co b⟦ n₁ ⟧a p₁ a⟦ n₂ ⟧b refl₀) refl₀ ⟩
            transport code-a p₂ (co b⟦ n₁ ⟧a p₁ a⟦ n₂ ⟧b refl₀ b⟦ n₂ ⟧a refl₀)
              ≡⟨ ap (transport code-a p₂) $ code-a-refl-refl n₂ (co b⟦ n₁ ⟧a p₁) ⟩
            transport code-a p₂ (co b⟦ n₁ ⟧a p₁)
              ≡⟨ trans-ba p₂ n₁ co p₁ ⟩∎
            co b⟦ n₁ ⟧a p₁ ∘₀ proj p₂
              ∎)

    abstract
      code-a-shift : ∀ {b₂} n₁ p₁ n₂ (r : loc n₁ ≡₀ loc n₂) (p₂ : _ ≡₀ b₂)
        → ⟧a p₁ ∘₀ ap₀ f r a⟦ n₂ ⟧b            p₂
        ≡ ⟧a p₁            a⟦ n₁ ⟧b ap₀ g r ∘₀ p₂
      code-a-shift n₁ p₁ n₂ r p₂ =
        ⟧a p₁             ∘₀            ap₀ f r a⟦ n₂ ⟧b p₂
          ≡⟨ ap (λ x → x a⟦ n₂ ⟧b p₂) $ ! $ code-a-merge n₁ p₁ (ap₀ f r) ⟩
        ⟧a p₁ a⟦ n₁ ⟧b refl₀ b⟦ n₁ ⟧a ap₀ f r a⟦ n₂ ⟧b p₂
          ≡⟨ ap (λ x → x a⟦ n₂ ⟧b p₂) $ ! $ code-ab-swap n₁ (⟧a p₁) n₂ r ⟩
        ⟧a p₁ a⟦ n₁ ⟧b ap₀ g r b⟦ n₂ ⟧a refl₀ a⟦ n₂ ⟧b p₂
          ≡⟨ code-ab-merge n₁ (⟧a p₁) n₂ (ap₀ g r) p₂ ⟩∎
        ⟧a p₁ a⟦ n₁ ⟧b ap₀ g r             ∘₀            p₂
          ∎

    abstract
      code-ba-shift : ∀ {b₂} n₁ co n₂ p₁ n₃ (r : loc n₂ ≡₀ loc n₃) (p₂ : _ ≡₀ b₂)
        → co b⟦ n₁ ⟧a p₁ ∘₀ ap₀ f r a⟦ n₃ ⟧b            p₂
        ≡ co b⟦ n₁ ⟧a p₁            a⟦ n₂ ⟧b ap₀ g r ∘₀ p₂
      code-ba-shift n₁ co n₂ p₁ n₃ r p₂ =
        co b⟦ n₁ ⟧a p₁             ∘₀            ap₀ f r a⟦ n₃ ⟧b p₂
          ≡⟨ ap (λ x → x a⟦ n₃ ⟧b p₂) $ ! $ code-ba-merge n₁ co n₂ p₁ (ap₀ f r) ⟩
        co b⟦ n₁ ⟧a p₁ a⟦ n₂ ⟧b refl₀ b⟦ n₂ ⟧a ap₀ f r a⟦ n₃ ⟧b p₂
          ≡⟨ ap (λ x → x a⟦ n₃ ⟧b p₂) $ ! $ code-ab-swap n₂ (co b⟦ n₁ ⟧a p₁) n₃ r ⟩
        co b⟦ n₁ ⟧a p₁ a⟦ n₂ ⟧b ap₀ g r b⟦ n₃ ⟧a refl₀ a⟦ n₃ ⟧b p₂
          ≡⟨ code-ab-merge n₂ (co b⟦ n₁ ⟧a p₁) n₃ (ap₀ g r) p₂ ⟩∎
        co b⟦ n₁ ⟧a p₁ a⟦ n₂ ⟧b ap₀ g r             ∘₀            p₂
          ∎

    abstract
      code-ab-shift : ∀ {a₂} n₁ co n₂ p₁ n₃ (r : loc n₂ ≡₀ loc n₃) (p₂ : _ ≡₀ a₂)
        → co a⟦ n₁ ⟧b p₁ ∘₀ ap₀ g r b⟦ n₃ ⟧a            p₂
        ≡ co a⟦ n₁ ⟧b p₁            b⟦ n₂ ⟧a ap₀ f r ∘₀ p₂
      code-ab-shift n₁ co n₂ p₁ n₃ r p₂ =
        co a⟦ n₁ ⟧b p₁             ∘₀            ap₀ g r b⟦ n₃ ⟧a p₂
          ≡⟨ ap (λ x → x b⟦ n₃ ⟧a p₂) $ ! $ code-ab-merge n₁ co n₂ p₁ (ap₀ g r) ⟩
        co a⟦ n₁ ⟧b p₁ b⟦ n₂ ⟧a refl₀ a⟦ n₂ ⟧b ap₀ g r b⟦ n₃ ⟧a p₂
          ≡⟨ ap (λ x → x b⟦ n₃ ⟧a p₂) $ ! $ code-ba-swap n₂ (co a⟦ n₁ ⟧b p₁) n₃ r ⟩
        co a⟦ n₁ ⟧b p₁ b⟦ n₂ ⟧a ap₀ f r a⟦ n₃ ⟧b refl₀ b⟦ n₃ ⟧a p₂
          ≡⟨ code-ba-merge n₂ (co a⟦ n₁ ⟧b p₁) n₃ (ap₀ f r) p₂ ⟩∎
        co a⟦ n₁ ⟧b p₁ b⟦ n₂ ⟧a ap₀ f r             ∘₀            p₂
          ∎

  -- Definition of code
  module _ where
    P : Set i
    P = pushout d

    -- Basic conversion
    a⇒b : ∀ n → code-a (f $ loc n) → code-b (g $ loc n)
    a⇒b n co = co a⟦ n ⟧b refl₀

    b⇒a : ∀ n → code-b (g $ loc n) → code-a (f $ loc n)
    b⇒a n co = co b⟦ n ⟧a refl₀

    private
      -- The head of the code
      code-glue-eq-loc : ∀ n → code-a (f $ loc n) ≃ code-b (g $ loc n)
      code-glue-eq-loc n = a⇒b n ,
        iso-is-eq (a⇒b n) (b⇒a n) (code-b-refl-refl n) (code-a-refl-refl n)

    abstract
      trans-code-a-r : ∀ n₁ n₂ (r : loc n₁ ≡ loc n₂) (co : code-a $ f $ loc n₁)
        → transport (code-a ◯ f) r co ≡ co a⟦ n₁ ⟧b refl₀ b⟦ n₁ ⟧a proj (ap f r)
      trans-code-a-r n₁ n₂ r co =
        transport (code-a ◯ f) r co
          ≡⟨ ! $ trans-ap code-a f r co ⟩
        transport code-a (ap f r) co
          ≡⟨ ap (transport code-a $ ap f r) $ ! $ code-a-refl-refl n₁ co ⟩
        transport code-a (ap f r) (co a⟦ n₁ ⟧b refl₀ b⟦ n₁ ⟧a refl₀)
          ≡⟨ trans-ba (ap f r) n₁ _ refl₀ ⟩∎
        co a⟦ n₁ ⟧b refl₀ b⟦ n₁ ⟧a proj (ap f r)
          ∎

    abstract
      trans-code-b-r : ∀ n₁ n₂ (r : loc n₁ ≡ loc n₂) (co : code-b $ g $ loc n₁)
        → transport (code-b ◯ g) r co ≡ co b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b proj (ap g r)
      trans-code-b-r n₁ n₂ r co =
        transport (code-b ◯ g) r co
          ≡⟨ ! $ trans-ap code-b g r co ⟩
        transport code-b (ap g r) co
          ≡⟨ ap (transport code-b $ ap g r) $ ! $ code-b-refl-refl n₁ co ⟩
        transport code-b (ap g r) (co b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b refl₀)
          ≡⟨ trans-ab (ap g r) n₁ _ refl₀ ⟩∎
        co b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b proj (ap g r)
          ∎

    private
      abstract
        code-glue-eq-route : ∀ n₁ n₂ r
          → transport (λ c → code-a (f c) ≃ code-b (g c)) r (code-glue-eq-loc n₁)
          ≡ code-glue-eq-loc n₂
        code-glue-eq-route n₁ n₂ r = equiv-eq $ funext λ co →
          π₁ (transport (λ c → code-a (f c) ≃ code-b (g c)) r (code-glue-eq-loc n₁)) co
              ≡⟨ ap (λ x → x co) $ app-trans
                (λ c →  code-a (f c) ≃ code-b (g c))
                (λ c → code-a (f c) → code-b (g c))
                (λ _ → π₁) r (code-glue-eq-loc n₁) ⟩
          transport (λ c → code-a (f c) → code-b (g c)) r (a⇒b n₁) co
              ≡⟨ trans-→ (code-a ◯ f) (code-b ◯ g) r (a⇒b n₁) co ⟩
          transport (code-b ◯ g) r (a⇒b n₁ $ transport (code-a ◯ f) (! r) co)
              ≡⟨ ap (transport (code-b ◯ g) r ◯ a⇒b n₁) $ trans-code-a-r _ _ (! r) co ⟩
          transport (code-b ◯ g) r (co a⟦ n₂ ⟧b refl₀ b⟦ n₂ ⟧a proj (ap f $ ! r) a⟦ n₁ ⟧b refl₀)
              ≡⟨ ap (λ x → transport (code-b ◯ g) r $ x a⟦ n₁ ⟧b refl₀) $ ! $ code-ab-swap _ co _ (proj $ ! r) ⟩
          transport (code-b ◯ g) r (co a⟦ n₂ ⟧b proj (ap g $ ! r) b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b refl₀)
              ≡⟨ ap (transport (code-b ◯ g) r) $ code-b-refl-refl n₁ _ ⟩
          transport (code-b ◯ g) r (co a⟦ n₂ ⟧b proj (ap g $ ! r))
              ≡⟨ trans-code-b-r _ _ r _ ⟩
          co a⟦ n₂ ⟧b proj (ap g $ ! r) b⟦ n₁ ⟧a refl₀ a⟦ n₁ ⟧b proj (ap g r)
              ≡⟨ code-ab-merge n₂ co n₁ _ _ ⟩
          co a⟦ n₂ ⟧b proj (ap g (! r) ∘ ap g r)
              ≡⟨ ap (λ x → co a⟦ n₂ ⟧b proj x) $ concat-ap g (! r) r ⟩
          co a⟦ n₂ ⟧b proj (ap g $ ! r ∘ r)
              ≡⟨ ap (λ x → co a⟦ n₂ ⟧b proj (ap g x)) $ opposite-left-inverse r ⟩∎
          a⇒b n₂ co
              ∎

    private
      code-glue-eq : ∀ c → code-a (f c) ≃ code-b (g c)
      code-glue-eq = visit-fiber-rec l
        (λ c → code-a (f c) ≃ code-b (g c))
        ⦃ λ _ → ≃-is-set (code-a-is-set _) (code-b-is-set _) ⦄
        code-glue-eq-loc
        code-glue-eq-route

    -- The data type!
    code : P → Set i
    code = pushout-rec-nondep (Set i) code-a code-b (eq-to-path ◯ code-glue-eq)

    -- Useful lemma
    abstract
      trans-code-glue-loc : ∀ n₂ co → transport code (glue $ loc n₂) co ≡ a⇒b n₂ co
      trans-code-glue-loc n₂ co =
        transport code (glue $ loc n₂) co
          ≡⟨ ! $ trans-ap (λ X → X) code (glue $ loc n₂) co ⟩
        transport (λ X → X) (ap code $ glue $ loc n₂) co
          ≡⟨ ap (λ x → transport (λ X → X) x co)
              $ pushout-β-glue-nondep (Set i) code-a code-b (eq-to-path ◯ code-glue-eq) (loc n₂) ⟩
        transport (λ X → X) (eq-to-path $ code-glue-eq $ loc n₂) co
          ≡⟨ ap (λ x → transport (λ X → X) (eq-to-path x) co)
                $ visit-fiber-β-loc l
                    (λ c → code-a (f c) ≃ code-b (g c))
                    ⦃ λ _ → ≃-is-set (code-a-is-set _) (code-b-is-set _) ⦄
                    code-glue-eq-loc
                    code-glue-eq-route
                    n₂ ⟩
        transport (λ X → X) (eq-to-path $ code-glue-eq-loc n₂) co
          ≡⟨ trans-id-eq-to-path (code-glue-eq-loc n₂) co ⟩∎
        a⇒b n₂ co
          ∎

    abstract
      trans-code-!glue-loc : ∀ n₂ co → transport code (! $ glue $ loc n₂) co ≡ b⇒a n₂ co
      trans-code-!glue-loc n₂ co = move!-transp-right code (glue $ loc n₂) co (b⇒a n₂ co) $ ! $
        transport code (glue $ loc n₂) (b⇒a n₂ co)
          ≡⟨ trans-code-glue-loc n₂ (b⇒a n₂ co) ⟩
        a⇒b n₂ (b⇒a n₂ co)
          ≡⟨ code-b-refl-refl n₂ co ⟩∎
        co
          ∎

    -- Truncation level
    abstract
      code-is-set : ∀ p → is-set $ code p
      code-is-set = pushout-rec
        (λ p → is-set $ code p)
        code-a-is-set
        code-b-is-set
        (λ _ → prop-has-all-paths is-set-is-prop _ _)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Oscar.Prelude
open import Oscar.Class.IsEquivalence

module Oscar.Class.Setoid where

record Setoid 𝔬 ℓ : Ø ↑̂ (𝔬 ∙̂ ℓ) where
  constructor ∁
  field
    {Object} : Ø 𝔬
    ObjectEquivalence : Object → Object → Ø ℓ
    ⦃ `IsEquivalence ⦄ : IsEquivalence ObjectEquivalence


text:
module Issue4267.B where

open import Issue4267.A0

postulate
  X : Set

-- Crucial for bug: omitting signature of ra,
-- letting Agda infer its type.
ra = record {A = X}


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

open import HoTT
open import homotopy.elims.SuspSmash
open import homotopy.elims.CofPushoutSection

-- Σ(X∧Y) ≃ X * Y

module homotopy.SuspSmash {i j} (X : Ptd i) (Y : Ptd j) where

private

  {- path lemmas -}
  private
    reduce-x : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : z == y)
      → p ∙ ! q ∙ q ∙ ! p ∙ p == p
    reduce-x idp idp = idp

    reduce-y : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : x == z)
      → p ∙ ! p ∙ q ∙ ! q ∙ p == p
    reduce-y idp idp = idp

  module Into = SuspensionRec {A = Smash X Y}
    {C = fst (X ⊙* Y)}
    (left (snd X))
    (right (snd Y))
    (CofPushoutSection.rec (λ _ → tt) (λ _ → idp)
      (glue (snd X , snd Y))
      (λ {(x , y) →
        glue (snd X , snd Y) ∙ ! (glue (x , snd Y))
        ∙ glue (x , y)
        ∙ ! (glue (snd X , y)) ∙ glue (snd X , snd Y)})
      (λ x → ! (reduce-x (glue (snd X , snd Y)) (glue (x , snd Y))))
      (λ y → ! (reduce-y (glue (snd X , snd Y)) (glue (snd X , y)))))

  into = Into.f

  module Out = PushoutRec {d = ⊙span-out (*-⊙span X Y)}
    {D = Suspension (Smash X Y)}
    (λ _ → north)
    (λ _ → south)
    (λ {(x , y) → merid (cfcod (x , y))})

  out = Out.f

  into-out : (j : fst (X ⊙* Y)) → into (out j) == j
  into-out = Pushout-elim
    (λ x → glue (snd X , snd Y) ∙ ! (glue (x , snd Y)))
    (λ y → ! (glue (snd X , snd Y)) ∙ glue (snd X , y))
    (↓-∘=idf-from-square into out ∘ λ {(x , y) →
      (ap (ap into) (Out.glue-β (x , y))
       ∙ Into.merid-β (cfcod (x ,  y)))
      ∙v⊡ lemma (glue (snd X , snd Y)) (glue (x , snd Y))
                (glue (snd X , y)) (glue (x , y))})
    where
    lemma : ∀ {i} {A : Type i} {x y z w : A}
      (p : x == y) (q : z == y) (r : x == w) (s : z == w)
      → Square (p ∙ ! q) (p ∙ ! q ∙ s ∙ ! r ∙ p) s (! p ∙ r)
    lemma idp idp idp s =
      vert-degen-square (∙-unit-r s)

  out-into : (σ : Suspension (Smash X Y)) → out (into σ) == σ
  out-into = susp-smash-elim
    idp
    idp
    (↓-∘=idf-in out into ∘ λ {(x , y) →
      ap (ap out) (Into.merid-β (cfcod (x , y)))
      ∙ lemma₁ out (Out.glue-β (snd X , snd Y))
                   (Out.glue-β (x , snd Y))
                   (Out.glue-β (x , y))
                   (Out.glue-β (snd X , y))
                   (Out.glue-β (snd X , snd Y))
      ∙ lemma₂ {p = merid (cfcod (snd X , snd Y))}
               {q = merid (cfcod (x , snd Y))}
               {r = merid (cfcod (x , y))}
               {s = merid (cfcod (snd X , y))}
               {t = merid (cfcod (snd X , snd Y))}
          (ap merid (! (cfglue (winl (snd X))) ∙ cfglue (winl x)))
          (ap merid (! (cfglue (winr y)) ∙ cfglue (winr (snd Y))))})
    where
    lemma₁ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
      {x y z u v w : A}
      {p : x == y} {q : z == y} {r : z == u} {s : v == u} {t : v == w}
      {p' : f x == f y} {q' : f z == f y} {r' : f z == f u}
      {s' : f v == f u} {t' : f v == f w}
      (α : ap f p == p') (β : ap f q == q') (γ : ap f r == r')
      (δ : ap f s == s') (ε : ap f t == t')
      → ap f (p ∙ ! q ∙ r ∙ ! s ∙ t) == p' ∙ ! q' ∙ r' ∙ ! s' ∙ t'
    lemma₁ f {p = idp} {q = idp} {r = idp} {s = idp} {t = idp}
          idp idp idp idp idp
      = idp

    lemma₂ : ∀ {i} {A : Type i} {x y z u : A}
      {p q : x == y} {r : x == z} {s t : u == z}
      (α : p == q) (β : s == t)
      → p ∙ ! q  ∙ r ∙ ! s ∙ t == r
    lemma₂ {p = idp} {r = idp} {s = idp} idp idp = idp

module SuspSmash where

  eq : Suspension (Smash X Y) ≃ fst (X ⊙* Y)
  eq = equiv into out into-out out-into

  path : Suspension (Smash X Y) == fst (X ⊙* Y)
  path = ua eq

  ⊙path : ⊙Susp (⊙Smash X Y) == (X ⊙* Y)
  ⊙path = ⊙ua (⊙≃-in eq idp)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import MJ.Types
import MJ.Classtable.Core as Core

module MJ.Syntax.Erase {c}(Ct : Core.Classtable c) where

open import Prelude hiding (erase)
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.Maybe.All as MayAll
open import Data.Vec as Vec hiding (_∈_)
open import Data.Star as Star
open import Data.List.Most as List
open import Data.List.Properties.Extra as List+
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Data.String

import Data.Vec.All as Vec∀

open Core c
open Classtable Ct
open import MJ.Classtable.Membership Ct
open import MJ.Classtable.Code Ct
open import MJ.LexicalScope Ct
open import MJ.Syntax.Typed Ct
open import MJ.Syntax.Program Ct
import MJ.Syntax.Untyped Ct as AST

{-# TERMINATING #-}
erase-expr : ∀ {Γ a} → Expr Γ a → AST.Expr (length Γ)
erase-expr (new C x) = AST.new C (List.erase erase-expr x)
erase-expr unit = AST.unit
erase-expr null = AST.null
erase-expr (num x) = AST.num x
erase-expr (iop x e e₁) = AST.iop x (erase-expr e) (erase-expr e₁)
erase-expr (call e m x) = AST.call (erase-expr e) m (List.erase erase-expr x)
erase-expr (var x) = AST.var (index x)
erase-expr (get e f) = AST.get (erase-expr e) f
erase-expr (upcast s e) = erase-expr e

mutual
  erase-stmt : ∀ {I r O} → Stmt I r O → AST.Stmt (length I) (length O)
  erase-stmt (loc a) = AST.loc a
  erase-stmt (asgn x e) = AST.asgn (index x) (erase-expr e)
  erase-stmt (set x f e) = AST.set (erase-expr x) f (erase-expr e)
  erase-stmt (do x) = AST.do (erase-expr x)
  erase-stmt (ret x) = AST.ret (erase-expr x)
  erase-stmt raise = AST.raise
  erase-stmt (try s catch s₁) = AST.try erase-stmt s catch erase-stmt s₁
  erase-stmt (while x do s) = AST.while erase-expr x do erase-stmt s
  erase-stmt (block x) = AST.block (erase-stmts x)

  -- this is an instance of Star.gmap, but the higher order version
  -- fails to pass the termination checker
  erase-stmts : ∀ {I r O} → Stmts I r O → AST.Stmts (length I) (length O)
  erase-stmts ε = ε
  erase-stmts (x ◅ st) = erase-stmt x ◅ erase-stmts st

erase-body : ∀ {I a} → Body I a → AST.Body (length I)
erase-body (body s* e) = AST.body (erase-stmts s*) (erase-expr e)

erase-constructor : ∀ {cid} → Constructor cid → AST.Constructor (length (Class.constr (Σ cid)))
erase-constructor (super args then b) = AST.super (List.erase erase-expr args) then (erase-body b)
erase-constructor (body x) = AST.body (erase-body x)

erase-method : ∀ {cid m as b} → Method cid m (as , b) → AST.Method (length as)
erase-method (super _ ⟨ args ⟩then b) = AST.super⟨ List.erase erase-expr args ⟩then (erase-body b)
erase-method (body x) = AST.body (erase-body x)

erase-implementation : ∀ {cid} → Implementation cid → AST.Implementation cid
erase-implementation (implementation construct mbodies) =
  AST.implementation (erase-constructor construct) (map-all erase-method mbodies)

erase-prog : ∀ {a} → Prog a → AST.Prog
erase-prog (ℂ , b) = (λ cid → erase-implementation (ℂ cid)) , erase-body b


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use Data.Vec.Recursive.Categorical
-- instead.
------------------------------------------------------------------------

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

module Data.Product.N-ary.Categorical where

{-# WARNING_ON_IMPORT
"Data.Product.N-ary.Categorical was deprecated in v1.1.
Use Data.Vec.Recursive.Categorical instead."
#-}

open import Data.Vec.Recursive.Categorical public


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

{- A typeclass for converting between type disciplines #-}
module CF.Transform.Compile.ToJVM where

open import Level
open import Function
open import Data.Product as P
open import Data.List as L
open import Data.List.Properties as LP
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Morphisms

open import CF.Types  as CF
open import CF.Contexts.Lexical
open import JVM.Types as JVM

record To {l r} (L : Set l) (R : Set r) : Set (l ⊔ r) where
  field
    ⟦_⟧ : L → R

open To {{...}} public

instance ⟦⟧-list : ∀ {a} {A B : Set a} {{_ : To A B}} → To (List A) (List B)
To.⟦_⟧ ⟦⟧-list = L.map ⟦_⟧

instance ⟦⟧-prod : ∀ {a} {A B C D : Set a} {{_ : To A B}} {{_ : To C D}} → To (A × C) (B × D)
To.⟦_⟧ ⟦⟧-prod = P.map ⟦_⟧ ⟦_⟧

instance cfToJvm-ty : To CF.Ty JVM.Ty
To.⟦_⟧ cfToJvm-ty = ‵_
  where
    ‵_ : CF.Ty → JVM.Ty
    ‵ void  = boolean
    ‵ int   = int
    ‵ bool  = boolean

instance cfToJvm-var : ∀ {ℓ} {A B : Set ℓ} {{_ : To A B}} {a : A} {as} →
                       To (a ∈ as) (⟦ a ⟧ ∈ ⟦ as ⟧)
To.⟦_⟧ cfToJvm-var = ∈-map⁺ ⟦_⟧

private
  module _ {t} {T : Set t} where
    open import JVM.Model T public

instance on-intf : ∀ {ℓ} {A B : Set ℓ} {{_ : To A B}} → To (Intf {T = A}) (Intf {T = B})
To.⟦ on-intf ⟧ (u ⇅ d) = ⟦ u ⟧ ⇅ ⟦ d ⟧


text:
------------------------------------------------------------------------------
-- Arithmetic properties used by the McCarthy 91 function
------------------------------------------------------------------------------

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

module FOTC.Program.McCarthy91.ArithmeticATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP
  using ( x≤y+x∸y
        ; x≤y→x≯y
        ; x≤y→x+k≤y+k
        )
open import FOTC.Data.Nat.PropertiesATP
  using ( +-N
        ; ∸-N
        ; +-comm
        ; [x+Sy]∸y≡Sx
        )
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.TotalityATP
  using ( 10-N
        ; 11-N
        ; 89-N
        ; 100-N
        )

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

postulate 91≡100+11∸10∸10 : 91' ≡ 100' + 11' ∸ 10' ∸ 10'
{-# ATP prove 91≡100+11∸10∸10 #-}

postulate
  100≡89+11  : 100' ≡ 89' + 11'
  101≡90+11  : 101' ≡ 90' + 11'
  102≡91+11  : 102' ≡ 91' + 11'
  103≡92+11  : 103' ≡ 92' + 11'
  104≡93+11  : 104' ≡ 93' + 11'
  105≡94+11  : 105' ≡ 94' + 11'
  106≡95+11  : 106' ≡ 95' + 11'
  107≡96+11  : 107' ≡ 96' + 11'
  108≡97+11  : 108' ≡ 97' + 11'
  109≡98+11  : 109' ≡ 98' + 11'
  110≡99+11  : 110' ≡ 99' + 11'
  111≡100+11 : 111' ≡ 100' + 11'
{-# ATP prove 100≡89+11 #-}
{-# ATP prove 101≡90+11 #-}
{-# ATP prove 102≡91+11 #-}
{-# ATP prove 103≡92+11 #-}
{-# ATP prove 104≡93+11 #-}
{-# ATP prove 105≡94+11 #-}
{-# ATP prove 106≡95+11 #-}
{-# ATP prove 107≡96+11 #-}
{-# ATP prove 108≡97+11 #-}
{-# ATP prove 109≡98+11 #-}
{-# ATP prove 110≡99+11 #-}
{-# ATP prove 111≡100+11 #-}

postulate 101≡100+11∸10 : 101' ≡ 100' + 11' ∸ 10'
{-# ATP prove 101≡100+11∸10 #-}

postulate
  100+11∸10>100 : 100' + 11' ∸ 10' > 100'
  100+11>100    : 100' + 11'       > 100'
{-# ATP prove 100+11∸10>100 101≡100+11∸10 #-}
{-# ATP prove 100+11>100 111≡100+11 #-}

postulate
  99+11>100 : 99' + 11' > 100'
  98+11>100 : 98' + 11' > 100'
  97+11>100 : 97' + 11' > 100'
  96+11>100 : 96' + 11' > 100'
  95+11>100 : 95' + 11' > 100'
  94+11>100 : 94' + 11' > 100'
  93+11>100 : 93' + 11' > 100'
  92+11>100 : 92' + 11' > 100'
  91+11>100 : 91' + 11' > 100'
  90+11>100 : 90' + 11' > 100'
{-# ATP prove 99+11>100 110≡99+11 #-}
{-# ATP prove 98+11>100 109≡98+11 #-}
{-# ATP prove 97+11>100 108≡97+11 #-}
{-# ATP prove 96+11>100 107≡96+11 #-}
{-# ATP prove 95+11>100 106≡95+11 #-}
{-# ATP prove 94+11>100 105≡94+11 #-}
{-# ATP prove 93+11>100 104≡93+11 #-}
{-# ATP prove 92+11>100 103≡92+11 #-}
{-# ATP prove 91+11>100 102≡91+11 #-}
{-# ATP prove 90+11>100 101≡90+11 #-}

x+11-N : ∀ {n} → N n → N (n + 11')
x+11-N Nn = +-N Nn 11-N

x+11∸10≡Sx : ∀ {n} → N n → n + 11' ∸ 10' ≡ succ₁ n
x+11∸10≡Sx Nn = [x+Sy]∸y≡Sx Nn 10-N

postulate x+1≤x∸10+11 : ∀ {n} → N n → n + 1' ≤ (n ∸ 10') + 11'
{-# ATP prove x+1≤x∸10+11 x≤y+x∸y 10-N 11-N +-N ∸-N +-comm #-}

postulate x≤89→x+11≯100 : ∀ {n} → N n → n ≤ 89' → n + 11' ≯ 100'
{-# ATP prove x≤89→x+11≯100 x≤y→x≯y x≤y→x+k≤y+k x+11-N 89-N 100-N 100≡89+11 #-}


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax CTLC | ΛC

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  ¬_  : 1-ary | r30

term
  app    : α ↣ β  α  ->  β | _$_ l20
  lam    : α.β  ->  α ↣ β | ƛ_ r10
  throw  : α  ¬ α  ->  β
  callcc : ¬ α.α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
-}

module CTLC.Signature where

open import SOAS.Context

-- Type declaration
data ΛCT : Set where
  N   : ΛCT
  _↣_ : ΛCT → ΛCT → ΛCT
  ¬_  : ΛCT → ΛCT
infixr 30 _↣_
infixr 30 ¬_

open import SOAS.Syntax.Signature ΛCT public
open import SOAS.Syntax.Build ΛCT public

-- Operator symbols
data ΛCₒ : Set where
  appₒ lamₒ throwₒ : {α β : ΛCT} → ΛCₒ
  callccₒ : {α : ΛCT} → ΛCₒ

-- Term signature
ΛC:Sig : Signature ΛCₒ
ΛC:Sig = sig λ
  { (appₒ    {α}{β}) → (⊢₀ α ↣ β) , (⊢₀ α) ⟼₂ β
  ; (lamₒ    {α}{β}) → (α ⊢₁ β) ⟼₁ α ↣ β
  ; (throwₒ  {α}{β}) → (⊢₀ α) , (⊢₀ ¬ α) ⟼₂ β
  ; (callccₒ {α})    → (¬ α ⊢₁ α) ⟼₁ α
  }

open Signature ΛC:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
open import DeBruijn

infix 8 _*

_* : ∀ {n} → Term n → Term n
(# x) *       = # x
(ƛ M) *       = ƛ M *
((ƛ M) · N) * = M * [ N * ]
(L · N) *     = L * · N *

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


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

open import lib.Basics
open import lib.NType2
open import lib.PathFunctor
open import lib.PathGroupoid

open import lib.types.Bool
open import lib.types.IteratedSuspension
open import lib.types.LoopSpace
open import lib.types.Nat
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Suspension
open import lib.types.TLevel
open import lib.types.Unit

open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas
open import nicolai.pseudotruncations.SeqColim
open import nicolai.pseudotruncations.wconstSequence

module nicolai.pseudotruncations.PseudoTruncs where

{- Definition of the Pseudo-truncation -}
module _ {i} where

  private
    data #Pseudotrunc-aux (n : ℕ) (A : Type i) : Type i where
      #point : A → #Pseudotrunc-aux n A
      #hub : (r : Sphere' n → A) → #Pseudotrunc-aux n A

    data #Pseudotrunc (n : ℕ) (A : Type i) : Type i where
      #trick-aux : #Pseudotrunc-aux n A → (Unit → Unit) → #Pseudotrunc n A

  Pseudo_-1-trunc : (n : ℕ) (A : Type i) → Type i
  Pseudo_-1-trunc = #Pseudotrunc

  point_-1 : {A : Type i} → (n : ℕ) → A → Pseudo n -1-trunc A
  point_-1 {A} n a = #trick-aux (#point a) _

  hub_-1 : {A : Type i} (n : ℕ) (r : Sphere' n → A) → Pseudo n -1-trunc A
  hub_-1 {A} n r = #trick-aux (#hub r) _

  postulate
    spoke_-1 : {A : Type i} (n : ℕ) (r : Sphere' n → A) (x : Sphere' n)
               → point n -1 (r x) == hub n -1 r

  {- The induction principle -}
  module PseudotruncInduction
    {A : Type i} (n : ℕ) {j}
    {P : Pseudo n -1-trunc A → Type j}
    (Point-1 : (a : A) → P (point n -1 a))
    (Hub-1 : (r : Sphere' n → A) → P (hub n -1 r))
    (Spoke-1 : (r : Sphere' n → A) → (x : Sphere' n)
               → Point-1 (r x) == Hub-1 r [ P ↓ spoke n -1 r x ])
    where

    f : Π (Pseudo n -1-trunc A) P
    f = f-aux phantom where
      f-aux : Phantom Spoke-1 → Π (Pseudo n -1-trunc A) P
      f-aux phantom (#trick-aux (#point x) _) = Point-1 x
      f-aux phantom (#trick-aux (#hub r) _) = Hub-1 r

    postulate
      pathβ : (r : Sphere' {i} n → A)
              → (x : Sphere' {i} n)
              → apd f (spoke n -1 r x) == Spoke-1 r x

open PseudotruncInduction public renaming
  (f to Pseudotrunc-ind ; pathβ to Pseudotrunc-ind-pathβ)

{- We derive the recursion principle from the induction principle -}
module PseudotruncRecursion
  {i j} {A : Type i}
  {P : Type j} (n : ℕ)
  (Point-1 : A → P)
  (Hub-1 : (r : Sphere' {i} n → A) → P)
  (Spoke-1 : (r : Sphere' n → A) (x : Sphere' n) → Point-1 (r x) == Hub-1 r)
  where

  rec : Pseudo n -1-trunc A → P
  rec = Pseudotrunc-ind n  {P = λ _ → P} Point-1 Hub-1
          (λ r x → from-transp
                    (λ _ → P)
                    (spoke n -1 r x)
                    ((transport (λ _ → P) (spoke n -1 r x) (Point-1 (r x)))
                        =⟨ transport-const-fam (spoke n -1 r x) (Point-1 (r x)) ⟩
                      Point-1 (r x)
                        =⟨ Spoke-1 r x ⟩
                      Hub-1 r
                        ∎))

open PseudotruncRecursion public renaming (rec to Pseudotrunc-rec)

{- A lemma that will be important later: any map from
   the sphere, composed with the points constructor,
   is null. -}

open import nicolai.pseudotruncations.pointed-O-Sphere
open import nicolai.pseudotruncations.LoopsAndSpheres
open null

module _ {i} {A : Type i} (n : ℕ) where

  from-sphere-null : (g : Sphere' {i} n → A)
                   → isNull (point n -1 (g (nor' n))) ((point n -1) ∘ g)
  from-sphere-null g x = point n -1 (g x)
                           =⟨ spoke n -1 g x ⟩
                         hub n -1 g
                           =⟨ ! (spoke n -1 g (nor' n)) ⟩
                         point n -1 (g (nor' n))
                           ∎

module cmp-nll {i} {Â : Ptd i} (n : ℕ) (g : ⊙Sphere' {i} n →̇ Â) where

  {- Pointed version of first constructor -}
  -- points∙ : Â →̇ (Pseudo n -1-trunc (fst Â) , point n -1 (snd Â))
  -- points∙ = point n -1 , idp

  from-sphere-null∙ : isNulld ((point n -1 , idp) ⊙∘ g)
  from-sphere-null∙ = λ x →
                         point n -1 ((fst g) x)
                           =⟨ spoke n -1 (fst g) x ⟩
                         hub n -1 (fst g)
                           =⟨ ! (spoke n -1 (fst g) (nor' n)) ⟩
                         point n -1 ((fst g) (nor' n))
                           =⟨ ap (point n -1) (snd g) ⟩
                         point n -1 (snd Â)
                           ∎

  {- Unfortunately, we will need this lemma not for maps
        g : Sphere' (S n) → A,
     but we will need it for maps
        g : Susp (Sphere' n) → A,
     and Sphere' (S n) is NOT judgmentally equal to Susp (Sphere' n).
     We have to give a second proof. -}

module cmp-nll' {i} {Â : Ptd i} (n : ℕ) (g : ⊙Susp (⊙Sphere' {i} n) →̇ Â) where

  {- "translate" equivalence -}
  tr≃⊙ : ⊙Sphere' {i} (S n) ⊙≃ ⊙Susp (⊙Sphere' {i} n)
  tr≃⊙ = coe-equiv∙ (susp'-switch n)

  tr≃ : Sphere' {i} (S n) ≃ fst (⊙Susp (⊙Sphere' {i} n))
  tr≃ = fst (fst tr≃⊙) , snd tr≃⊙

  tr–̇> : (⊙Sphere' {i} (S n)) →̇ ⊙Susp (⊙Sphere' {i} n)
  tr–̇> = fst tr≃⊙ -- –> (fst (fst tr-eq) , snd tr-eq) , {!!}

  from-sphere-null'∙ : isNulld ((point S n -1 , idp) ⊙∘ g)
  from-sphere-null'∙ = λ x →

    fst ((point S n -1 , idp) ⊙∘ g) x
      =⟨ ap (fst ((point S n -1 , idp) ⊙∘ g)) (! (<–-inv-r tr≃ x)) ⟩
    fst ((point S n -1 , idp) ⊙∘ g) (–> tr≃ (<– tr≃ x))
      =⟨ cmp-nll.from-sphere-null∙ {i} {Â} (S n) (g ⊙∘ tr–̇>) (<– tr≃ x) ⟩
    point S n -1 (snd Â)
      ∎

max_stars_repo_name: nicolaikraus/HoTT-Agda


text:
-- Jesper, 2019-05-28: test case for #3812

{-# OPTIONS --rewriting #-}

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

record Box (A : Set) : Set where
  constructor box
  field unbox : A

open Box

postulate
  A : Set
  r s : Box A
  rew₂ : r .unbox ≡ s .unbox

{-# REWRITE rew₂ #-}

Box-η : {x y : Box A} → x .unbox ≡ y .unbox → x ≡ y
Box-η refl = refl

-- WAS: `ext` reduces to `refl`, but giving `ext = refl` directly
-- leads to a type error.
ext : r ≡ s
ext = Box-η refl

ext' : r ≡ s
ext' = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT
open import homotopy.HSpace
open import homotopy.PushoutComm using (flip; Pushout-comm)

module homotopy.HopfConstruction {i} (A : Type i) (c : is-connected 0 A)
  (hA : HSpaceStructure A) where

open HSpaceStructure hA
open ConnectedHSpace A c hA

{-
Using the fact that [μ a] is an equivalence, we define a fibration over the
suspension of [A] with fiber [A] and applying [μ a] when you move along
[merid a].
-}

module H = SuspensionRecType A A μ-e-r-equiv

{-
The total space of the previous fibration is the pushout of the following span
(thanks to the flattening lemma).
-}

s : Span
s = span (⊤ × A) (⊤ × A) (A × A)
         (λ cc' → (tt , snd cc')) (λ cc' → (tt , uncurry μ cc'))

lemma : Σ (Suspension A) H.f == Pushout s
lemma = H.flattening

{-
But that span is equal to the following span, which is almost the same as
the span for the join.
-}

x : s == flip (*-span A A)
x = span= (equiv snd (_,_ tt) (λ b → idp) (λ a → idp))
          (equiv snd (_,_ tt) (λ b → idp) (λ a → idp))
          eq (λ a → idp) (λ a → idp)  where

  eq : (A × A) ≃ (A × A)
  eq = equiv to from to-from from-to  where

    to : A × A → A × A
    to (a , a') = (μ a a' , a')

    from : A × A → A × A
    from (a , a') = (<– (μ-e-l-equiv a') a , a')

    to-from : (a : A × A) → to (from a) == a
    to-from (a , a') = pair×= (<–-inv-r (μ-e-l-equiv a') a) idp

    from-to : (a : A × A) → from (to a) == a
    from-to (a , a') = pair×= (<–-inv-l (μ-e-l-equiv a') a) idp

lemma2 : (A * A) ≃ (Pushout (flip (*-span A A)))
lemma2 = Pushout-comm (*-span A A)

theorem : Σ (Suspension A) H.f == (A * A)
theorem = lemma ∙ ap Pushout x ∙ ! (ua lemma2)

-- record FibSeq {i j k ℓ} (A : Type i) (B : Type j) (C : Type k) (c : C)
--   : Type (lmax (lmax i j) (lmax k (lsucc ℓ))) where
--   constructor fibSeq
--   field
--     fibration : C → Type ℓ
--     fiber : fibration c ≃ A
--     total : Σ C fibration ≃ B


text:
module WarningOnImport.Impo where

B = Set
A = B

{-# WARNING_ON_USAGE A "Deprecated: Use B instead" #-}
{-# WARNING_ON_IMPORT "Deprecated: Use Impossible instead" #-}


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Impl.Consensus.PersistentLivenessStorage
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.PersistentLivenessStorage.Properties where

module saveVoteMSpec (vote : Vote) where
  open OutputProps
  postulate -- TODO-2: refine and prove
    contract
      : ∀ P pre
        → (∀ outs → NoMsgs outs → NoErrors outs → P (inj₁ fakeErr) pre outs)
        → (∀ outs → NoMsgs outs → NoErrors outs
           → P (inj₂ unit) pre outs)
        → RWS-weakestPre (saveVoteM vote) P unit pre


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

open import HoTT
open import cohomology.Exactness
open import cohomology.Theory

module cohomology.Sn {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT

C-Sphere-≠ : (n : ℤ) (m : ℕ) → (n ≠ ℕ-to-ℤ m)
  → C n (⊙Sphere m) == LiftUnit-Group
C-Sphere-≠ n O neq = C-dimension n neq
C-Sphere-≠ n (S m) neq =
  ap (λ k → C k (⊙Sphere (S m))) (! (succ-pred n))
  ∙ C-Susp (pred n) (⊙Sphere m)
  ∙ C-Sphere-≠ (pred n) m (λ p → neq (pred-injective n (pos m) p))

C-Sphere-diag : (m : ℕ) → C (ℕ-to-ℤ m) (⊙Sphere m) == C O (⊙Sphere O)
C-Sphere-diag O = idp
C-Sphere-diag 1 = C-Susp O (⊙Sphere O)
C-Sphere-diag (S (S m)) =
  C-Susp (pos m) (⊙Sphere (S m)) ∙ C-Sphere-diag (S m)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the heterogeneous sublist relation
-- This is a generalisation of what is commonly known as Order
-- Preserving Embeddings (OPE).
------------------------------------------------------------------------

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

open import Relation.Binary using (REL)

module Data.List.Relation.Binary.Sublist.Heterogeneous
  {a b r} {A : Set a} {B : Set b} {R : REL A B r}
  where

open import Level using (_⊔_)
open import Data.List.Base using (List; []; _∷_; [_])
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Function
open import Relation.Unary using (Pred)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Re-export core definitions

open import Data.List.Relation.Binary.Sublist.Heterogeneous.Core public

------------------------------------------------------------------------
-- Type and basic combinators

module _ {s} {S : REL A B s} where

  map : R ⇒ S → Sublist R ⇒ Sublist S
  map f []        = []
  map f (y ∷ʳ rs) = y ∷ʳ map f rs
  map f (r ∷ rs)  = f r ∷ map f rs

minimum : Min (Sublist R) []
minimum []       = []
minimum (x ∷ xs) = x ∷ʳ minimum xs

------------------------------------------------------------------------
-- Conversion to and from Any

toAny : ∀ {a bs} → Sublist R [ a ] bs → Any (R a) bs
toAny (y ∷ʳ rs) = there (toAny rs)
toAny (r ∷ rs)  = here r

fromAny : ∀ {a bs} → Any (R a) bs → Sublist R [ a ] bs
fromAny (here r)  = r ∷ minimum _
fromAny (there p) = _ ∷ʳ fromAny p

------------------------------------------------------------------------
-- Generalised lookup based on a proof of Any

module _ {p q} {P : Pred A p} {Q : Pred B q} (resp : P ⟶ Q Respects R) where

  lookup : ∀ {xs ys} → Sublist R xs ys → Any P xs → Any Q ys
  lookup []       ()
  lookup (y ∷ʳ p)  k         = there (lookup p k)
  lookup (rxy ∷ p) (here px) = here (resp rxy px)
  lookup (rxy ∷ p) (there k) = there (lookup p k)