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

open import Categories.Category

-- Reasoning facilities about morphism equivalences (not necessarily 'squares')

module Categories.Morphism.Reasoning {o ℓ e} (C : Category o ℓ e) where

-- some items are defined in sub-modules
open import Categories.Morphism.Reasoning.Core C public
open import Categories.Morphism.Reasoning.Iso C public

open Category C
open Definitions C
open HomReasoning

-- create a commutative square from an equivalence
toSquare : ∀ {A B} {f g : A ⇒ B} → f ≈ g → CommutativeSquare f id id g
toSquare {_} {_} {f} {g} f≈g = begin
      id ∘ f   ≈⟨ identityˡ ⟩
      f        ≈⟨ f≈g ⟩
      g        ≈˘⟨ identityʳ ⟩
      g ∘ id   ∎


text:
module Prelude where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

data _==_ {A : Set} (x : A) : A → Set where
  refl : x == x

data Vec (A : Set) : Nat -> Set where
  nil : Vec A 0
  cons : forall {n} -> A -> Vec A n -> Vec A (suc n)

data List (A : Set) : Set where
  nil : List A
  cons : A -> List A -> List A

data Empty : Set where

data Not (A : Set) : Set where
  is-absurd : (A -> Empty) -> Not A

data Dec (A : Set) : Set where
  yes : A -> Dec A
  no : Not A -> Dec A

ext: agda

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Everything where

open import Cubical.Data.BinNat public
open import Cubical.Data.Bool public
open import Cubical.Data.Empty public
open import Cubical.Data.Fin public
open import Cubical.Data.Nat public
open import Cubical.Data.Int public renaming (_+_ to _+Int_ ; +-assoc to +Int-assoc; +-comm to +Int-comm)
open import Cubical.Data.Sum public
open import Cubical.Data.Prod public
open import Cubical.Data.Unit public
open import Cubical.Data.Sigma public
open import Cubical.Data.DiffInt public
open import Cubical.Data.Group public hiding (_≃_)
open import Cubical.Data.HomotopyGroup public
open import Cubical.Data.List public
open import Cubical.Data.Graph public

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


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

syntax Inception | IA

type
  L : 0-ary
  P : 0-ary
  A : 0-ary

term
  rec : L  P  ->  A
  inc : L.A  P.A  ->  A

theory
  (S) p : P   a : P.A |> inc (l. rec (l, p[]), x. a[x]) = a[p[]]
  (E) a : L.A  |> k : L |- inc (l. a[l], x. rec(k, x)) = a[k]
  (W) m : A  a : P.A  |> inc (l. m[], x. a[x]) = m[]
  (A) p : (L,L).A  a : (L,P).A  b : P.A |>         inc (l. inc (k. p[l, k], x. a[l,x]), y. b[y])       = inc (k. inc(l. p[l,k], y.b[y]), x. inc(l. a[l,x], y.b[y]))
-}

module Inception.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Inception.Signature

private
  variable
    Γ Δ Π : Ctx
    α : IAT
    𝔛 : Familyₛ

-- Inductive term declaration
module IA:Terms (𝔛 : Familyₛ) where

  data IA : Familyₛ where
    var  : ℐ ⇾̣ IA
    mvar : 𝔛 α Π → Sub IA Π Γ → IA α Γ

    rec : IA L Γ → IA P Γ → IA A Γ
    inc : IA A (L ∙ Γ) → IA A (P ∙ Γ) → IA A Γ

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  IAᵃ : MetaAlg IA
  IAᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (recₒ ⋮ a , b) → rec a b
      (incₒ ⋮ a , b) → inc a b
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module IAᵃ = MetaAlg IAᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : IA ⇾̣ 𝒜
    𝕊 : Sub IA Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (rec a b) = 𝑎𝑙𝑔 (recₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (inc a b) = 𝑎𝑙𝑔 (incₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ IAᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ IA α Γ) → 𝕤𝕖𝕞 (IAᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (recₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (incₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ IA ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : IA ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ IAᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : IA α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub IA Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (rec a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (inc a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
IA:Syn : Syntax
IA:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = IA:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open IA:Terms 𝔛 in record
    { ⊥ = IA ⋉ IAᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax IA:Syn public
open IA:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands IAᵃ public
open import SOAS.Metatheory IA:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- The unit type; also used as proposition ``Truth''.

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

module Tools.Unit where

-- We reexport Agda's built-in unit type.

open import Agda.Builtin.Unit public using (⊤; tt)
open import Agda.Primitive

record ⊤′ : Setω where
  instance constructor tt

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
import      Lvl
open import Structure.Category
open import Structure.Setoid
open import Type

module Structure.Category.Morphism.Transport
  {ℓₒ ℓₘ ℓₑ : Lvl.Level}
  (cat : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ})
  where

import      Functional.Dependent as Fn
import      Function.Equals
open        Function.Equals.Dependent
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Relator.Equals using ([≡]-intro) renaming (_≡_ to _≡ₑ_)
open import Relator.Equals.Proofs
import      Structure.Category.Morphism.IdTransport as IdTransport
import      Structure.Categorical.Names as Names
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Relator.Properties

open CategoryObject(cat)
open Category(category)
open Category.ArrowNotation(category)
open Morphism.OperModule ⦃ morphism-equiv ⦄ (\{x} → _∘_ {x})
open Morphism.IdModule   ⦃ morphism-equiv ⦄ (\{x} → _∘_ {x})(id)

module _ {P : Object → Object} (p : ∀{x} → (x ⟶ P(x))) ⦃ isomorphism : ∀{x} → Isomorphism(p{x}) ⦄ where
  private variable a b c : Object

  transport : (a ≡ₑ b) → (P(a) ⟶ P(b))
  transport ab = p ∘ IdTransport.transport(cat) ab ∘ inv(p)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module ModuleArityMismatch where

 module M (A : Set) where

 postulate
   A : Set

 module M′ = M A A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Prelude where

-- Function composition
_∘_ : ∀ {x y z : Set} -> (y -> z) -> (x -> y) -> (x -> z)
(f ∘ g) x = f (g x)

-- Product type
data _×_ (A B : Set) : Set where
    _,_ : A -> B -> A × B

uncurry : ∀ {x y z : Set} -> (x -> y -> z) -> (x × y) -> z
uncurry f (a , b) = f a b

-- Lists
data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

infixr 20 _::_
infixr 15 _++_

[_] : ∀ {A} -> A -> List A
[ x ] = x :: []

_++_ : ∀ {A} -> List A -> List A -> List A
[] ++ l = l
(x :: xs) ++ l = x :: (xs ++ l)

foldr : ∀ {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr f b [] = b
foldr f b (x :: xs) = f x (foldr f b xs)

map : ∀ {A B} -> (A -> B) -> List A -> List B
map f [] = []
map f (x :: xs) = f x :: map f xs

zip : ∀ {A B} -> List A -> List B -> List (A × B)
zip [] _                = []
zip _  []               = []
zip (x :: xs) (y :: ys) = (x , y) :: zip xs ys

max_stars_repo_name: snowleopard/alga-proofs

max_issues_repo_name: snowleopard/alga-proofs

max_forks_repo_name: snowleopard/alga-proofs


text:
module Issue49 where

module Dummy {A : Set1} where
  postulate D : Set

T : Set
T = Dummy.D {Set}

T' : Set
T' = Dummy.D {A = Set}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module NatCat where

open import Relation.Binary.PropositionalEquality

-- If you can show that a relation only ever has one inhabitant
-- you get the category laws for free
module
  EasyCategory
  (obj : Set)
  (_⟶_ : obj → obj → Set)
  (_∘_ : ∀ {x y z} → x ⟶ y → y ⟶ z → x ⟶ z)
  (id : ∀ x → x ⟶ x)
  (single-inhabitant : (x y : obj) (r s : x ⟶ y) → r ≡ s)
  where

  idʳ : ∀ x y (r : x ⟶ y) → r ∘ id y ≡ r
  idʳ x y r = single-inhabitant x y (r ∘ id y) r

  idˡ : ∀ x y (r : x ⟶ y) → id x ∘ r ≡ r
  idˡ x y r = single-inhabitant x y (id x ∘ r) r

  ∘-assoc : ∀ w x y z (r : w ⟶ x) (s : x ⟶ y) (t : y ⟶ z) → (r ∘ s) ∘ t ≡ r ∘ (s ∘ t)
  ∘-assoc w x y z r s t = single-inhabitant w z ((r ∘ s) ∘ t) (r ∘ (s ∘ t))

open import Data.Nat

same : (x y : ℕ) (r s : x ≤ y) → r ≡ s
same .0 y z≤n z≤n = refl
same .(suc m) .(suc n) (s≤s {m} {n} r) (s≤s s) = cong s≤s (same m n r s)

≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z
≤-trans .0 y z z≤n s = z≤n
≤-trans .(suc m) .(suc n) .(suc n₁) (s≤s {m} {n} r) (s≤s {.n} {n₁} s) = s≤s (≤-trans m n n₁ r s)

≤-refl : ∀ x → x ≤ x
≤-refl zero = z≤n
≤-refl (suc x) = s≤s (≤-refl x)

module Nat-EasyCategory = EasyCategory ℕ _≤_ (λ {x}{y}{z} → ≤-trans x y z) ≤-refl same

max_stars_repo_name: alexgracianoarj/detect-languages

max_issues_repo_name: alexgracianoarj/detect-languages

max_forks_repo_name: alexgracianoarj/detect-languages


text:
module Structure.Relator.Properties where

open import Functional
import      Lvl
open import Lang.Instance
open import Logic
import      Structure.Relator.Names as Names
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Lvl.Level
private variable T A B C D E : Type{ℓ}

-- Definition of a reflexive binary relation
module _ {T : Type{ℓ₁}} (_▫_ : T → T → Stmt{ℓ₂}) where
  record Reflexivity : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Reflexivity(_▫_)
  reflexivity = inst-fn Reflexivity.proof

-- Definition of a transitive binary relation
module _ {T : Type{ℓ₁}} (_▫_ : T → T → Stmt{ℓ₂}) where
  record Transitivity : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Transitivity(_▫_)
  transitivity = inst-fn Transitivity.proof

-- Definition of a antisymmetric binary relation
module _ {T : Type{ℓ₁}} (_▫₁_ : T → T → Stmt{ℓ₂}) (_▫₂_ : T → T → Stmt{ℓ₃}) where
  record Antisymmetry : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    constructor intro
    field proof : Names.Antisymmetry(_▫₁_)(_▫₂_)
  antisymmetry = inst-fn Antisymmetry.proof

-- Definition of a irreflexive binary relation
module _ {T : Type{ℓ₁}} (_▫_ : T → T → Stmt{ℓ₂}) where
  record Irreflexivity : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Irreflexivity(_▫_)
  irreflexivity = inst-fn Irreflexivity.proof

-- Definition of a total binary relation.
-- Total in the sense that it, or its converse, holds.
module _ {T : Type{ℓ₁}} (_▫_ : T → T → Stmt{ℓ₂}) where
  record ConverseTotal : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.ConverseTotal(_▫_)
  converseTotal = inst-fn ConverseTotal.proof

-- Definition of a converse dichotomy.
-- It or its converse always holds, but never both at the same time.
module _ {T : Type{ℓ₁}} (_▫_ : T → T → Stmt{ℓ₂}) where
  record ConverseDichotomy : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.ConverseDichotomy(_▫_)
  dichotomy = inst-fn ConverseDichotomy.proof

module _ {T : Type{ℓ₁}} (_▫₁_ : T → T → Stmt{ℓ₂}) (_▫₂_ : T → T → Stmt{ℓ₃}) where
  record ConverseTrichotomy : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    constructor intro
    field proof : Names.ConverseTrichotomy(_▫₁_)(_▫₂_)
  trichotomy = inst-fn ConverseTrichotomy.proof

-- Definition of a converse binary operation for a binary operation
-- record Converse {T₁ T₂ : Type} (_▫₁_ : T₁ → T₂ → Stmt) (_▫₂_ : T₂ → T₁ → Stmt) : Stmt where
--   constructor intro
--
--   field
--     converseₗ : Names.ConversePattern (_▫₂_) (_▫₁_)
--     converseᵣ : Names.ConversePattern (_▫₁_) (_▫₂_)
-- open Converse ⦃ ... ⦄ public
-- {x : T₁}{y : T₂} → (x ▫₁ y) ↔ (y ▫₂ x)

-- Definition of a symmetric binary operation
module _ {T : Type{ℓ₁}} (_▫_ : T → T → Stmt{ℓ₂}) where
  record Symmetry : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Symmetry(_▫_)
  symmetry = inst-fn Symmetry.proof
-- {x y : T} → (x ▫ y) → (y ▫ x)

-- Definition of an asymmetric binary operation
module _ {T : Type{ℓ₁}} (_▫_ : T → T → Stmt{ℓ₂}) where
  record Asymmetry : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Asymmetry(_▫_)
  asymmetry = inst-fn Asymmetry.proof
-- {x y : T} → (x ▫ y) → ¬(y ▫ x)

module _ (_▫₁_ : A → B → Stmt{ℓ₁}) (_▫₂_ : A → B → Stmt{ℓ₂}) where
  record _⊆₂_ : Stmt{Lvl.of(A) Lvl.⊔ Lvl.of(B) Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Subrelation(_▫₁_)(_▫₂_)
  sub₂ = inst-fn _⊆₂_.proof

module _ (_▫₁_ : A → B → Stmt{ℓ₁}) (_▫₂_ : A → B → Stmt{ℓ₂}) where
  _⊇₂_ = (_▫₂_) ⊆₂ (_▫₁_)
  module _⊇₂_ inst = _⊆₂_ {_▫₁_ = _▫₂_}{_▫₂_ = _▫₁_} inst
  super₂ = inst-fn _⊇₂_.proof

module _ (_▫₁_ : A → B → Stmt{ℓ₁}) (_▫₂_ : A → A → Stmt{ℓ₂}) where
  record Subtransitivityₗ : Stmt{Lvl.of(A) Lvl.⊔ Lvl.of(B) Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Subtransitivityₗ(_▫₁_)(_▫₂_)
  subtransitivityₗ = inst-fn Subtransitivityₗ.proof

module _ (_▫₁_ : A → B → Stmt{ℓ₁}) (_▫₂_ : B → B → Stmt{ℓ₂}) where
  record Subtransitivityᵣ : Stmt{Lvl.of(A) Lvl.⊔ Lvl.of(B) Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Subtransitivityᵣ(_▫₁_)(_▫₂_)
  subtransitivityᵣ = inst-fn Subtransitivityᵣ.proof

-- Definition of a cotransitive binary relation
module _ {T : Type{ℓ₁}} (_▫_ : T → T → Stmt{ℓ₂}) where
  record CoTransitivity : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.CoTransitivity(_▫_)
  cotransitivity = inst-fn CoTransitivity.proof


text:
module Issue2486.ImportB where

open import Issue2486.Haskell

{-# FOREIGN GHC data BBool = BTrue | BFalse #-}
data BBool : Set where
  BTrue BFalse : BBool

{-# COMPILE GHC BBool = data BBool ( BTrue | BFalse ) #-}

postulate BList : Set → Set
{-# FOREIGN GHC import MAlonzo.Code.Issue2486.Haskell (MyList) #-}
{-# COMPILE GHC BList = type MyList #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-
  This is mostly for convenience, when working with ideals
  (which are defined for general rings) in a commutative ring.
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Ideal where

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

open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.FinData

open import Cubical.Algebra.CommRing.Base
open import Cubical.Algebra.Ring.Ideal renaming (IdealsIn to IdealsInRing)
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

IdealsIn : (R : CommRing ℓ) → Type _
IdealsIn R = IdealsInRing (CommRing→Ring R)

module _ (Ring@(R , str) : CommRing ℓ) where
  open CommRingStr str
  makeIdeal : (I : R → hProp ℓ)
              → (+-closed : {x y : R} → x ∈ I → y ∈ I → (x + y) ∈ I)
              → (0r-closed : 0r ∈ I)
              → (·-closedLeft : {x : R} → (r : R) → x ∈ I → r · x ∈ I)
              → IdealsIn (R , str)
  makeIdeal I +-closed 0r-closed ·-closedLeft = I ,
    (record
       { +-closed = +-closed
       ; -closed = λ x∈I → subst-∈ I (useSolver _)
                             (·-closedLeft (- 1r) x∈I)
       ; 0r-closed = 0r-closed
       ; ·-closedLeft = ·-closedLeft
       ; ·-closedRight = λ r x∈I →
                       subst-∈ I
                             (·-comm r _)
                             (·-closedLeft r x∈I)
       })
       where useSolver : (x : R) → - 1r · x ≡ - x
             useSolver = solve Ring

-- better?
module _ (R' : CommRing ℓ) where
 private R = fst R'
 open CommRingStr (snd R')
 open Sum (CommRing→Ring R')

 record isCommIdeal (I : ℙ R) : Type ℓ where
  constructor
   makeIsCommIdeal
  field
   +Closed : ∀ {x y : R} → x ∈ I → y ∈ I → (x + y) ∈ I
   contains0 : 0r ∈ I
   ·Closed : ∀ {x : R} (r : R) → x ∈ I → r · x ∈ I

 open isCommIdeal
 isPropIsCommIdeal : (I : ℙ R) → isProp (isCommIdeal I)
 +Closed (isPropIsCommIdeal I ici₁ ici₂ i) x∈I y∈I =
         I _ .snd (ici₁ .+Closed x∈I y∈I) (ici₂ .+Closed x∈I y∈I) i
 contains0 (isPropIsCommIdeal I ici₁ ici₂ i) = I 0r .snd (ici₁ .contains0) (ici₂ .contains0) i
 ·Closed (isPropIsCommIdeal I ici₁ ici₂ i) r x∈I =
         I _ .snd (ici₁ .·Closed r x∈I) (ici₂ .·Closed r x∈I) i

 CommIdeal : Type _
 CommIdeal = Σ[ I ∈ ℙ R ] isCommIdeal I

 ∑Closed : (I : CommIdeal) {n : ℕ} (V : FinVec R n)
         → (∀ i → V i ∈ fst I) → ∑ V ∈ fst I
 ∑Closed I {n = zero} _ _ = I .snd .contains0
 ∑Closed I {n = suc n} V h = I .snd .+Closed (h zero) (∑Closed I (V ∘ suc) (h ∘ suc))

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
------------------------------------------------------------------------------
-- Equality reasoning on inductive PA
------------------------------------------------------------------------------

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

-- This module only re-export the preorder reasoning instanced on
-- the inductive PA propositional equality.

module PA.Inductive.Relation.Binary.EqReasoning where

open import PA.Inductive.Base

import Common.Relation.Binary.PreorderReasoning
open module ≡-Reasoning =
  Common.Relation.Binary.PreorderReasoning _≡_ refl trans public
    renaming ( _∼⟨_⟩_ to _≡⟨_⟩_ )

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- One can construct combinators which do not preserve equality
------------------------------------------------------------------------

module TotalParserCombinators.NotACongruence where

open import Codata.Musical.Notation
open import Data.Bool
open import Data.List
open import Function
open import Function.Equality
open import Function.Inverse as Inv
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary

open import TotalParserCombinators.Congruence using (_≅P_; _∷_)
open import TotalParserCombinators.Derivative
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics as S using (_∈_·_; _≅_)

-- It is easy to construct a combinator which does not preserve
-- equality. All it takes is to inspect the input combinator's
-- structure (or that of its index), and make some suitable decision
-- based on this information. Examples:

module Example₁ where

  -- A combinator which removes ambiguity.

  unambiguous : ∀ {Tok R xs} →
                Parser Tok R xs → Parser Tok R (take 1 xs)
  unambiguous {xs = xs} p =
      token >>= (λ t → ♯ unambiguous (D t p))
    ∣ return⋆ (take 1 xs)

  -- The following two parsers are (parser) equal.

  p₁ : Parser Bool Bool (true ∷ (false ∷ []))
  p₁ = return true ∣ return false

  p₂ : Parser Bool Bool (false ∷ (true ∷ []))
  p₂ = return false ∣ return true

  equal : p₁ ≅P p₂
  equal = AdditiveMonoid.commutative (return true) (return false)

  -- However, unambiguous does not respect this equality.

  unambiguous-is-not-a-congruence :
    ¬ (unambiguous p₁ ≅ unambiguous p₂)
  unambiguous-is-not-a-congruence eq =
    case Inverse.to eq ⟨$⟩ S.∣-right [] (S.∣-left S.return) of λ
      { (S.∣-right .[] (S.∣-left               ()))
      ; (S.∣-right .[] (S.∣-right .([ false ]) ()))
      ; (S.∣-left []∈) → helper refl []∈
      }
    where
    helper : ∀ {s} {f : Bool → List Bool}
               {p : ∀ b → ∞ (Parser Bool Bool (f b))} →
               s ≡ [] →
             ¬ (true ∈ token >>= p · s)
    helper () (S._>>=_ S.token _)

module Example₂ where

  -- A combinator which returns true (without consuming input) if its
  -- argument is "fail", and false otherwise.

  is-fail-bag : ∀ {Tok R xs} → Parser Tok R xs → List Bool
  is-fail-bag fail = [ true  ]
  is-fail-bag _    = [ false ]

  is-fail : ∀ {Tok R xs}
            (p : Parser Tok R xs) → Parser Tok Bool (is-fail-bag p)
  is-fail fail             = return true
  is-fail (return x)       = return false
  is-fail token            = return false
  is-fail (p₁ ∣ p₂)        = return false
  is-fail (f <$> p)        = return false
  is-fail (p₁ ⊛ p₂)        = return false
  is-fail (p₁ >>= p₂)      = return false
  is-fail (nonempty p)     = return false
  is-fail (cast xs₁≈xs₂ p) = return false

  -- The following parsers are equal, but is-fail treats them
  -- differently.

  p₁ : Parser Bool Bool []
  p₁ = fail

  p₂ : Parser Bool Bool []
  p₂ = fail ∣ fail

  equal : p₁ ≅P p₂
  equal = Inv.id ∷ λ _ → ♯ equal

  is-fail-is-not-a-congruence : ¬ (is-fail p₁ ≅ is-fail p₂)
  is-fail-is-not-a-congruence eq with Inverse.to eq ⟨$⟩ S.return
  ... | ()

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat   using (ℕ; _+_)

private
  variable
    ℓ : Level
    A : Type ℓ

infixr 5 ⟨_,_⟩∷_

data AssocList (A : Type ℓ) : Type ℓ where
 ⟨⟩ : AssocList A
 ⟨_,_⟩∷_ : (a : A) (n : ℕ) (xs : AssocList A) → AssocList A
 per : ∀ a b xs →   ⟨ a , 1 ⟩∷ ⟨ b , 1 ⟩∷ xs
                  ≡ ⟨ b , 1 ⟩∷ ⟨ a , 1 ⟩∷ xs
 agg : ∀ a m n xs →  ⟨ a , m ⟩∷ ⟨ a , n ⟩∷ xs
                   ≡ ⟨ a , m + n ⟩∷ xs
 del : ∀ a xs → ⟨ a , 0 ⟩∷ xs ≡ xs
 trunc : isSet (AssocList A)

pattern ⟨_⟩ a = ⟨ a , 1 ⟩∷ ⟨⟩

-- Elimination and recursion principle for association lists
module Elim {ℓ'} {B : AssocList A → Type ℓ'}
       (⟨⟩* : B ⟨⟩) (⟨_,_⟩∷*_ : (x : A) (n : ℕ) {xs : AssocList A} → B xs → B (⟨ x , n ⟩∷ xs))
       (per* :  (x y : A) {xs : AssocList A} (b : B xs)
              → PathP (λ i → B (per x y xs i)) (⟨ x , 1 ⟩∷* ⟨ y , 1 ⟩∷* b) (⟨ y , 1 ⟩∷* ⟨ x , 1 ⟩∷* b))
       (agg* :  (x : A) (m n : ℕ) {xs : AssocList A} (b : B xs)
              → PathP (λ i → B (agg x m n xs i)) (⟨ x , m ⟩∷* ⟨ x , n ⟩∷* b) (⟨ x , m + n ⟩∷* b))
       (del* :  (x : A) {xs : AssocList A} (b : B xs)
              → PathP (λ i → B (del x xs i)) (⟨ x , 0 ⟩∷* b) b)
       (trunc* : (xs : AssocList A) → isSet (B xs)) where

 f : (xs : AssocList A) → B xs
 f ⟨⟩ = ⟨⟩*
 f (⟨ a , n ⟩∷ xs) = ⟨ a , n ⟩∷* f xs
 f (per a b xs i) = per* a b (f xs) i
 f (agg a m n xs i) = agg* a m n (f xs) i
 f (del a xs i) = del* a (f xs) i
 f (trunc xs ys p q i j) = isOfHLevel→isOfHLevelDep 2 trunc*  (f xs) (f ys) (cong f p) (cong f q) (trunc xs ys p q) i j

module ElimProp {ℓ'} {B : AssocList A → Type ℓ'} (BProp : {xs : AssocList A} → isProp (B xs))
       (⟨⟩* : B ⟨⟩) (⟨_,_⟩∷*_ : (x : A) (n : ℕ) {xs : AssocList A} → B xs → B (⟨ x , n ⟩∷ xs)) where

 f : (xs : AssocList A) → B xs
 f = Elim.f ⟨⟩* ⟨_,_⟩∷*_
      (λ x y {xs} b → toPathP (BProp (transp (λ i → B (per x y xs i)) i0 (⟨ x , 1 ⟩∷* ⟨ y , 1 ⟩∷* b)) (⟨ y , 1 ⟩∷* ⟨ x , 1 ⟩∷* b)))
      (λ x m n {xs} b → toPathP (BProp (transp (λ i → B (agg x m n xs i)) i0 (⟨ x , m ⟩∷* ⟨ x , n ⟩∷* b)) (⟨ x , m + n ⟩∷* b)))
      (λ x {xs} b → toPathP (BProp (transp (λ i → B (del x xs i)) i0 (⟨ x , 0 ⟩∷* b)) b))
      (λ xs → isProp→isSet BProp)

module Rec {ℓ'} {B : Type ℓ'} (BType : isSet B)
       (⟨⟩* : B) (⟨_,_⟩∷*_ : (x : A) (n : ℕ) → B → B)
       (per* :  (x y : A) (b : B) → (⟨ x , 1 ⟩∷* ⟨ y , 1 ⟩∷* b) ≡ (⟨ y , 1 ⟩∷* ⟨ x , 1 ⟩∷* b))
       (agg* :  (x : A) (m n : ℕ) (b : B) → (⟨ x , m ⟩∷* ⟨ x , n ⟩∷* b) ≡ (⟨ x , m + n ⟩∷* b))
       (del* :  (x : A) (b : B) → (⟨ x , 0 ⟩∷* b) ≡ b) where

 f : AssocList A → B
 f = Elim.f ⟨⟩* (λ x n b → ⟨ x , n ⟩∷* b) (λ x y b → per* x y b) (λ x m n b → agg* x m n b) (λ x b → del* x b) (λ _ → BType)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Categories.Diagram.Finite where

open import Level

open import Categories.Category
open import Categories.Category.Finite renaming (Finite to FiniteC)
open import Categories.Functor

private
  variable
    o ℓ e : Level
    J C : Category o ℓ e

record Finite (F : Functor J C) : Set (levelOfTerm F) where
  field
    finite : FiniteC J

  open Functor F public
  open FiniteC finite public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Exercises for session 2
--
-- If unsure which exercises to do start with those marked with *
--
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module ExerciseSession2 where

open import Part1
open import Part2
open import ExerciseSession1

open import Cubical.Foundations.Equiv

-- Exercises about Part 2:

-- Exercise* 1: prove that the computation rule for J on refl
-- holds up to a path.
-- (hint: normalize the goal using C-u C-u C-c C-,)
JEq : {x : A} (P : (z : A) → x ≡ z → Type ℓ'')
      (d : P x refl) → J P d refl ≡ d
JEq P p d = {!!}

-- Exercise* 2: prove that isContr implies isProp
isContr→isProp : isContr A → isProp A
isContr→isProp = {!!}

-- Exercise 3: prove that isProp implies isProp'
-- (hint: use isProp→isSet from the Part2)
isProp→isProp' : isProp A → isProp' A
isProp→isProp' = {!!}

-- Exercise 4: prove the following lemma
-- (hint: use the solutions to exercises 2 and 3)
isContr→isContr≡ : isContr A → (x y : A) → isContr (x ≡ y)
isContr→isContr≡ = {!!}

-- Exercise 5: use transp to turn a PathP into a transport
fromPathP : {A : I → Type ℓ} {x : A i0} {y : A i1}
          → PathP A x y
          → transport (λ i → A i) x ≡ y
fromPathP {A = A} p i = {!!}

-- The converse is harder to prove so we give it:
toPathP : {A : I → Type ℓ} {x : A i0} {y : A i1}
        → transport (λ i → A i) x ≡ y
        → PathP A x y
toPathP {A = A} {x = x} p i =
  hcomp (λ j → λ { (i = i0) → x
                 ; (i = i1) → p j })
        (transp (λ j → A (i ∧ j)) (~ i) x)

-- Exercise* 6: prove that two Σ-types where the second component is a
-- proposition is equal if the first projections are equal.
-- (hint: use ΣPathP and toPathP)
Σ≡Prop : {B : A → Type ℓ'} {u v : Σ A B} (h : (x : A) → isProp (B x))
       → (p : fst u ≡ fst v) → u ≡ v
Σ≡Prop {B = B} {u = u} {v = v} h p = {!!}

-- Exercice 7 (harder): prove that being contractible is a proposition.
-- (hint: the second component can be given by a suitable higher
-- dimensional hcomp)
isPropIsContr : isProp (isContr A)
isPropIsContr = {!!}

-- Exercises about Part 3:

-- Exercise* 8: compose sucPathInt with itself n times. Transporting
-- along this will be addition, transporting with it backwards will be
-- subtraction.

open import Cubical.Data.Nat
open import Cubical.Data.Int hiding (addEq ; subEq)

-- a) Define a path "addEq n" by composing sucPathInt with itself n times.
addEq : ℕ → Int ≡ Int
addEq n = {!!}

-- b) Define another path "subEq n" by composing "sym sucPathInt" with
-- itself n times.
subEq : ℕ → Int ≡ Int
subEq n = {!!}

-- c) Define addition on integers by pattern-matching and transporting
-- along addEq/subEq appropriately.
_+Int_ : Int → Int → Int
m +Int n = {!!}

-- d) Do some concrete computations using _+Int_ (this would not work
-- in HoTT as the transport would be stuck!)

-- e) Use isEquivTransport from

open import Cubical.Foundations.Transport

-- to prove that +Int with a fixed number is an equivalence.
--
-- Note that proving this for the usual _+_ function would be a lot
-- longer, but now we get it for free as addition is defined using
-- transport which we already know is an equivalence.

-- Exercise* 9 (harder): prove that hSet is not a set

-- Let's import Bool instead so that we get it from the library
open import Cubical.Data.Bool renaming (notEq to notPath)

-- The empty type ⊥ (written \bot)
open import Cubical.Data.Empty

-- Just define hSets of level 0 for simplicity
hSet : Type₁
hSet = Σ[ A ∈ Type₀ ] isSet A

-- Bool is an hSet
BoolSet : hSet
BoolSet = Bool , isSetBool

-- (hint: use a suitable nested transport)
notPath≢refl : (notPath ≡ refl) → ⊥
notPath≢refl e = true≢false {!!}

-- (hint: use notPath≢refl and define two elements of BoolSet ≡
-- BoolSet, one based on notPath and one based on refl. Σ≡Prop and
-- isPropIsSet is probably handy)
¬isSet-hSet : isSet hSet → ⊥
¬isSet-hSet h = {!!}

-- Exercise 10 (more work): prove that FinData and Fin are equivalent
-- and hence equal. Transport some functions and proofs between the
-- two.

-- Orderings on ℕ
open import Cubical.Data.Nat.Order

data FinData : ℕ → Type₀ where
  zero : {n : ℕ} → FinData (suc n)
  suc  : {n : ℕ} (i : FinData n) → FinData (suc n)

Fin : ℕ → Type₀
Fin n = Σ[ k ∈ ℕ ] k < n


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

module Cubical.Homotopy.PointedFibration where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Homotopy.Base
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Loopspace
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open LowerBoundedInduction
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Foundations.HLevels'
open import Cubical.Foundations.Structure

private
  variable
    ℓ ℓ' : Level

-- Different versions of Theorem 9. We abstract ℓ' again here
-- to avoid some issues with implicit arguments.
module _ {ℓ' : Level} (X : Pointed ℓ) where
  -- block of private stuff to reduce redundancy in the proof of the theorem
  private
    module _ (n k : ℕ) where
      -- A, together with its paramenters/context, is just the statement of the theorem.
      A : Type (ℓ-max ℓ (ℓ-suc ℓ'))
      A = (isConnX : isConnected (k + 1) (typ X))
          → (Y : typ X → Σ[ Yx ∈ Pointed ℓ' ] (isOfHLevel (n + k) (typ Yx)))
          → isOfHLevel (n) (Π∙ X (λ x → typ (fst (Y x))) (pt (fst (Y (pt X)))))

    module PointSec (n k : ℕ)
                    (isConnX : isConnected (k + 1) (typ X))
                    (Y : typ X → Σ[ Yx ∈ Pointed ℓ' ] (isOfHLevel (n + k) (typ Yx))) where
      -- The type of pointed sections (x : X) →ₚₜ Y x
      sec∙ : Type (ℓ-max ℓ ℓ')
      sec∙ = Π∙ X (λ x → typ (fst (Y x))) (pt (fst (Y (pt X))))

      -- Note that if isOfHLevel had a uniform interface for n ≥ 1 then this should be a part of the where
      -- clause in the theorem.
      module PointSecProps where
        -- Given s, the type of pointed sections (x : X) →ₚₜ Ω(Y x, s x)
        sec∙' : (s : sec∙) → Type (ℓ-max ℓ ℓ')
        sec∙' s = Π∙ X (λ x → s .fst x ≡ s .fst x) refl

        -- towards sec∙' s ≃ (s ≡ s)
        secIso : (s : sec∙) → Iso (sec∙' s) (s ∙∼ s)
        secIso (_ , s₂) = iso (λ (H , p) → H , p ∙ sym (rCancel s₂))
                        (λ (H , p) → H , p ∙ rCancel s₂)
                        (λ (H , p) → ΣPathP (refl ,
                                            sym (assoc p (rCancel s₂) (sym (rCancel s₂))) ∙∙
                                            cong (p ∙_) (rCancel (rCancel s₂)) ∙∙
                                            sym (rUnit p)))
                        (λ (H , p) → ΣPathP (refl ,
                                            sym (assoc p
                                                       (sym (rCancel s₂))
                                                       (rCancel s₂)) ∙∙
                                            cong (p ∙_) (lCancel (rCancel s₂)) ∙∙
                                            sym (rUnit p)))

        -- compose the equivalences
        sec≃ : (s : sec∙) → sec∙' s ≃ (s ≡ s)
        sec≃ = λ (s : sec∙) → compEquiv (isoToEquiv (secIso s)) (funExt∙≃ s s)

  -- p.9 Theorem 3 of Higher Types in HoTT
  sec∙Trunc : {n k : ℕ} → A (n + 1) (k)
  sec∙Trunc {n = 0} {k} isConnX Y = isContr→isProp (s₀ , λ s → funExt∙ (s₀∙∼s s))
    where
      sec∙ : Type (ℓ-max ℓ ℓ')
      sec∙ = Π∙ X (λ x → typ (fst (Y x))) (pt (fst (Y (pt X))))

      module _ where
        -- trivial section
        s₀ : sec∙
        s₀ = (λ a → pt (fst (Y a))) , refl

        -- abbreviations
        s₀₁ = fst s₀
        ⋆ = pt X

        -- the k-connected map 𝟙 → X
        f : Unit → typ X
        f tt = ⋆

        -- proof that f is k-connected
        fkconn : isConnectedFun k f
        fkconn = UnitConnectedFunElim isConnX f

        -- notation
        module _ (s : sec∙) where
          s₁ = fst s
          s₂ = snd s

          -- the regular homotopies between the trivial section and s coincide with the
          -- identity type s₀₁ ⋆ ≡ s₁ ⋆
          -- the Unit type will be eliminated in the next step
          IsoHtpy𝟙Idpt : Iso (s₀₁ ∼ s₁) (Unit → s₀₁ ⋆ ≡ s₁ ⋆)
          IsoHtpy𝟙Idpt = elim.isIsoPrecompose f k (λ (x : typ X) → (s₀₁ x ≡ s₁ x) , HL← (HL→ (snd (Y x)) (s₀₁ x) (s₁ x))) fkconn

          IsoHtpyIdpt : Iso (s₀₁ ∼ s₁) (s₀₁ ⋆ ≡ s₁ ⋆)
          IsoHtpyIdpt = compIso IsoHtpy𝟙Idpt (𝟙-universal (s₀₁ ⋆ ≡ s₁ ⋆))

          -- judgementally,
          -- (s₀ ∙∼ s) ≡ (Σ[ h ∈ (s₀₁ ∼ s₁) ] (h ⋆ ≡ (snd s₀) ∙ s₂ ⁻¹))
          -- The right inverse of IsoHtpyIdpt gives such a pointed homotopy
          s₀∙∼s : s₀ ∙∼ s
          fst s₀∙∼s = Iso.inv IsoHtpyIdpt (refl ∙ s₂ ⁻¹)
          snd s₀∙∼s =
            Iso.inv IsoHtpyIdpt (refl ∙ s₂ ⁻¹) ⋆
              ≡⟨ refl ⟩
            Iso.fun IsoHtpyIdpt (Iso.inv IsoHtpyIdpt (refl ∙ s₂ ⁻¹))
              ≡⟨ Iso.rightInv IsoHtpyIdpt (refl ∙ s₂ ⁻¹) ⟩
            refl ∙ s₂ ⁻¹ ∎

  sec∙Trunc {n = 1} {k} isConnX Y = truncSelfId→truncId {n = 0} (λ s → EquivPresHLevel {n = 1} (sec≃ s) (sec∙Trunc {n = 0} {k} isConnX λ x → ((s .fst x ≡ s .fst x) , refl) , (snd (Y x) (s .fst x) (s .fst x))))
    where
      open PointSec 2 k isConnX Y
      open PointSecProps

  sec∙Trunc {n = suc (suc m)} {k} isConnX Y =
    -- suffices to show that loop spaces are truncated
    truncSelfId→truncId
      -- each self-identity type of a section s is equivalent to a type of sections
      λ s → EquivPresHLevel (sec≃ s)
        -- that the induction hypothesis can be applied to
        (sec∙Trunc {n = suc m} isConnX λ x → ((s .fst x ≡ s .fst x) , refl) , snd (Y x) (s .fst x) (s .fst x))
    where
      open PointSec (suc (suc m) + 1) k isConnX Y
      open PointSecProps

  -- alternate version of sec∙Trunc with bound on n instead of adding a bound
  sec∙Trunc' : {n k : ℕ} (1≤n : 1 ≤ n) → A n k
  sec∙Trunc' {n = n} {k = k} 1≤n
    = +Type→≤Type 1 (λ n → A n k) (λ r isConnX Y → sec∙Trunc {n = r} {k = k} isConnX Y) n 1≤n

module _ (X : Pointed ℓ) (Y : Pointed ℓ') where
  pointed-maps-truncated : {n k : ℕ}
                           → 1 ≤ n
                           → isConnected (k + 1) (typ X)
                           → isOfHLevel (n + k) (typ Y)
                           → isOfHLevel (n) (X →∙ Y)
  pointed-maps-truncated {n = n} 1≤n connX truncY =
    sec∙Trunc' X 1≤n connX λ _ → Y , truncY

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --without-K #-}
module Wow-It-is-FV where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Primitive

levelEq : lzero ≡ lzero
levelEq = refl

levelEq′ : lsuc lzero ≡ lsuc lzero
levelEq′ = refl

trans : {l : Level} {Q : Set l} {a b c : Q}
      → a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

J : {A : Set} (P : (x y : A) → x ≡ y → Set)
  → ((x : A) → P x x refl)
  → (x y : A) (xy : x ≡ y) → P x y xy
J P p x .x refl = p x

cong : {A B : Set} (f : A → B)
     → {m n : A} → m ≡ n → f m ≡ f n
cong f refl = refl

sym : {A : Set} {m n : A} → m ≡ n → n ≡ m
sym refl = refl

theorem : suc zero + suc zero ≡ _
theorem = refl

theorem′ : 1 + 1 ≡ 2
theorem′ = refl

trivialEq : {a : _} {A : Set a} → A ≡ A
trivialEq = refl

trivialEq′ : ∀ {a} {A : Set a} → A ≡ A
trivialEq′ = refl

trivialEq′′ : ∀ a b → a + b ≡ a + b
trivialEq′′ a b = refl

trans′ : ∀ {a} {A : Set a} (a b c : A)
       → a ≡ b → b ≡ c → a ≡ c
trans′ a .a c refl bc = bc

data _<=_ : (a b : Nat) → Set where
  0ltn : ∀ {n}   → 0 <= n
  nltm : ∀ {n m} → n <= m → suc n <= suc m

7lt13 : 7 <= 13
7lt13 = nltm (nltm (nltm (nltm (nltm (nltm (nltm 0ltn))))))

abc : ∀ {a b c} → a <= b → b <= c → a <= c
abc 0ltn bc = 0ltn
abc (nltm ab) (nltm bc) = nltm (abc ab bc)

data ⊥ : Set where

ridiculous : ⊥ → ⊥
ridiculous a = a

ridiculous′ : 1 ≡ 0 → ⊥
ridiculous′ ()

⊥-elim : ∀ {a} {A : Set a} → ⊥ → A
⊥-elim ()

4lt3 : 4 <= 3 → ⊥
4lt3 (nltm (nltm (nltm ())))

infix 3 ¬_
¬_ : ∀ {a} → Set a → Set a
¬ P = P → ⊥

_!=_ : ∀ {a} {A : Set a} → A → A → Set a
x != y = ¬ x ≡ y

_≡⟨_⟩_ : ∀ {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ refl ⟩ c = c

_QED : ∀ {A : Set} (x : A) → x ≡ x
_ QED = refl

lemma₀ : ∀ n → n + 0 ≡ n
lemma₀ zero = refl
lemma₀ (suc n) = cong suc (lemma₀ n)

lemma₁ : ∀ n m → suc (n + m) ≡ n + suc m
lemma₁ zero _ = refl
lemma₁ (suc n) m = cong suc (lemma₁ n m)

comm : ∀ n m → n + m ≡ m + n
comm zero n = sym (lemma₀ n)
comm (suc n) m = suc n + m
  ≡⟨ refl ⟩ suc (n + m)
  ≡⟨ cong suc (comm n m) ⟩ suc (m + n)
  ≡⟨ lemma₁ m n ⟩ m + suc n QED

infixr 2 _≡⟨_⟩_
infix 3 _QED


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

module lemmas-general where
  Coerce-unicity : ∀{r ex1 ex2} →
                     Coerce r := ex1 →
                     Coerce r := ex2 →
                     ex1 == ex2
  Coerce-unicity CoerceUnit CoerceUnit = refl
  Coerce-unicity (CoercePair C1 C2) (CoercePair C3 C4)
    rewrite Coerce-unicity C1 C3 | Coerce-unicity C2 C4
      = refl
  Coerce-unicity (CoerceCtor C1) (CoerceCtor C2)
    rewrite Coerce-unicity C1 C2
      = refl

  Fuel-depletion-unicity : ∀{⛽ ⛽↓1 ⛽↓2} →
                             ⛽ ⛽⇓ ⛽↓1 →
                             ⛽ ⛽⇓ ⛽↓2 →
                             ⛽↓1 == ⛽↓2
  Fuel-depletion-unicity CF∞ CF∞ = refl
  Fuel-depletion-unicity CF⛽ CF⛽ = refl

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Lex.Core where

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit.Base using (⊤; tt)
open import Function using (_∘_; flip; id)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.List.Base using (List; []; _∷_)
open import Level using (_⊔_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary
open import Data.List.Relation.Binary.Pointwise
   using (Pointwise; []; _∷_; head; tail)

-- The lexicographic ordering itself can be either strict or non-strict,
-- depending on whether type P is inhabited.

data Lex {a ℓ₁ ℓ₂} {A : Set a} (P : Set)
         (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) :
         Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂) where
  base : P                             → Lex P _≈_ _≺_ []       []
  halt : ∀ {y ys}                      → Lex P _≈_ _≺_ []       (y ∷ ys)
  this : ∀ {x xs y ys} (x≺y : x ≺ y)   → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
  next : ∀ {x xs y ys} (x≈y : x ≈ y)
         (xs<ys : Lex P _≈_ _≺_ xs ys) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)

-- Properties

module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
         {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where

  private
    _≋_ = Pointwise _≈_
    _<_ = Lex P _≈_ _≺_

  ¬≤-this : ∀ {x y xs ys} → ¬ (x ≈ y) → ¬ (x ≺ y) →
            ¬ (x ∷ xs) < (y ∷ ys)
  ¬≤-this x≉y x≮y (this x≺y)       = x≮y x≺y
  ¬≤-this x≉y x≮y (next x≈y xs<ys) = x≉y x≈y

  ¬≤-next : ∀ {x y xs ys} → ¬ x ≺ y → ¬ xs < ys →
            ¬ (x ∷ xs) < (y ∷ ys)
  ¬≤-next x≮y xs≮ys (this x≺y)     = x≮y x≺y
  ¬≤-next x≮y xs≮ys (next _ xs<ys) = xs≮ys xs<ys

  transitive : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → Transitive _≺_ →
               Transitive _<_
  transitive eq resp tr = trans
    where
    trans : Transitive (Lex P _≈_ _≺_)
    trans (base p)         (base _)         = base p
    trans (base y)         halt             = halt
    trans halt             (this y≺z)       = halt
    trans halt             (next y≈z ys<zs) = halt
    trans (this x≺y)       (this y≺z)       = this (tr x≺y y≺z)
    trans (this x≺y)       (next y≈z ys<zs) = this (proj₁ resp y≈z x≺y)
    trans (next x≈y xs<ys) (this y≺z)       =
      this (proj₂ resp (IsEquivalence.sym eq x≈y) y≺z)
    trans (next x≈y xs<ys) (next y≈z ys<zs) =
      next (IsEquivalence.trans eq x≈y y≈z) (trans xs<ys ys<zs)

  antisymmetric : Symmetric _≈_ → Irreflexive _≈_ _≺_ →
                  Asymmetric _≺_ → Antisymmetric _≋_ _<_
  antisymmetric sym ir asym = as
    where
    as : Antisymmetric _≋_ _<_
    as (base _)         (base _)         = []
    as halt             ()
    as (this x≺y)       (this y≺x)       = ⊥-elim (asym x≺y y≺x)
    as (this x≺y)       (next y≈x ys<xs) = ⊥-elim (ir (sym y≈x) x≺y)
    as (next x≈y xs<ys) (this y≺x)       = ⊥-elim (ir (sym x≈y) y≺x)
    as (next x≈y xs<ys) (next y≈x ys<xs) = x≈y ∷ as xs<ys ys<xs

  respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → _<_ Respects₂ _≋_
  respects₂ eq (resp₁ , resp₂) = resp¹ , resp²
    where
    open IsEquivalence eq using (sym; trans)
    resp¹ : ∀ {xs} → Lex P _≈_ _≺_ xs Respects _≋_
    resp¹ []            xs<[]            = xs<[]
    resp¹ (_   ∷ _)     halt             = halt
    resp¹ (x≈y ∷ _)     (this z≺x)       = this (resp₁ x≈y z≺x)
    resp¹ (x≈y ∷ xs≋ys) (next z≈x zs<xs) =
      next (trans z≈x x≈y) (resp¹ xs≋ys zs<xs)

    resp² : ∀ {ys} → flip (Lex P _≈_ _≺_) ys Respects _≋_
    resp² []            []<ys            = []<ys
    resp² (x≈z ∷ _)     (this x≺y)       = this (resp₂ x≈z x≺y)
    resp² (x≈z ∷ xs≋zs) (next x≈y xs<ys) =
      next (trans (sym x≈z) x≈y) (resp² xs≋zs xs<ys)

  decidable : Dec P → Decidable _≈_ → Decidable _≺_ → Decidable _<_
  decidable (yes p) dec-≈ dec-≺ []       []       = yes (base p)
  decidable (no ¬p) dec-≈ dec-≺ []       []       = no λ{(base p) → ¬p p}
  decidable dec-P   dec-≈ dec-≺ []       (y ∷ ys) = yes halt
  decidable dec-P   dec-≈ dec-≺ (x ∷ xs) []       = no λ()
  decidable dec-P   dec-≈ dec-≺ (x ∷ xs) (y ∷ ys) with dec-≺ x y
  ... | yes x≺y = yes (this x≺y)
  ... | no x≮y with dec-≈ x y
  ...   | no x≉y = no (¬≤-this x≉y x≮y)
  ...   | yes x≈y with decidable dec-P dec-≈ dec-≺ xs ys
  ...     | yes xs<ys = yes (next x≈y xs<ys)
  ...     | no  xs≮ys = no (¬≤-next x≮y xs≮ys)


text:
-- ----------------------------------------------------------------------
-- The Agda σ-library
--
-- Substitutions
-- ----------------------------------------------------------------------

-- A substitution on T is defined as a mapping from
-- indices to T (w/ explicit bounds).
--
-- Since the domain is bounded, we may think
-- of substitutions as vectors.

module Sigma.Subst.Base where

open import Data.Nat using (ℕ; suc; zero; _+_)
open import Data.Fin using (Fin; zero; suc)

open import Function using (_∘_)

open import Data.Product using (_×_) renaming ( _,_ to ⟨_,_⟩ )

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

-- A subsitution σ : 𝕀ⁿ → T is denoted { i ↦ x : i ∈ 𝕀ⁿ, x ∈ T }
Sub : Set → ℕ → Set
Sub T m = Fin m → T

-- The empty subsitution.
-- Note that 𝕀⁰ ≡ ⊥. We note σ : 𝕀⁰ → T by []
-- Intuitively, this mimics an empty vector.
[] : ∀ { T } → Sub T 0
[] = λ ()

infixr 5 _∷_

-- The σ-cons operator ∷ ∶ T → (𝕀ⁿ → T) → (𝕀¹⁺ⁿ → T)
--
-- Intuitively, the σ-cons operator mimics the
-- semantics of cons operator on vectors.
--
-- x ∷ σ = { 0 ↦ x } ∪ { 1 + i ↦ σ i : i ∈ 𝕀ⁿ }
_∷_ : ∀ { n } { T } → T → Sub T n → Sub T (1 + n)
(x ∷ σ) zero = x
(x ∷ σ) (suc n) = σ n

[_] : ∀ { T } → T → Sub T 1
[ x ] = x ∷ []

head : ∀ { n } { T } → Sub T (1 + n) → T
head σ = σ zero

tail : ∀ { n } { T } → Sub T (1 + n) → Sub T n
tail σ = σ ∘ suc

map : ∀ { n } { T U } → (T → U) → Sub T n → Sub U n
map f σ = f ∘ σ

uncons : ∀ { n } { T } → Sub T (1 + n) → T × Sub T n
uncons σ = ⟨ head σ , tail σ ⟩

infixr 5 _++_

-- The σ-append operator ++ : (𝕀ᵐ → T) → (𝕀ⁿ → T) → (𝕀ᵐ⁺ⁿ → T)
--
-- σ₁ ++ σ₂ = { i ↦ σ₁ i : i ∈ 𝕀ᵐ⁺ⁿ, i < m } ∪ { i ↦ σ₂ i : i ∈ 𝕀ᵐ⁺ⁿ, i ≥ m }
_++_ : ∀ { m n } { T } → Sub T m → Sub T n → Sub T (m + n)
_++_ {zero} σ₁ σ₂ = σ₂
_++_ {suc m} σ₁ σ₂ = σ₁ zero ∷ (σ₁ ∘ suc) ++ σ₂

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma


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

open import Cubical.Relation.Binary.Base public
open import Cubical.Relation.Binary.Properties public
open import Cubical.Relation.Binary.Fiberwise public


text:
module RewriteAndWhere where

open import Common.Equality

data ℕ : Set where
  zero : ℕ

good : (a b : ℕ) → a ≡ b → b ≡ a
good a b eq with a | eq
... | .b | refl = foo
  where
    foo : b ≡ b
    foo = refl

mutual
  aux : (a b : ℕ)(w : ℕ) → w ≡ b → b ≡ w
  aux a b .b refl = foo
    where
     foo : b ≡ b
     foo = refl

  good₂ : (a b : ℕ) → a ≡ b → b ≡ a
  good₂ a b eq = aux a b a eq

bad : (a b : ℕ) → a ≡ b → b ≡ a
bad a b eq rewrite eq = foo
  where
    foo : b ≡ b
    foo rewrite sym eq = bar
      where
        bar : a ≡ a
        bar = refl

max_stars_repo_name: larrytheliquid/agda


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

module Strict.Properties where

open import Path
open import Level
open import Strict
open import Agda.Builtin.Strict
open import Function

$!-≡ : {A : Type a} {B : A → Type b} → (f : ∀ x → B x) → ∀ x → (f $! x) ≡ f x
$!-≡ f x = builtin-eq-to-path (primForceLemma x f)

$!≡$ : {A : Type a} {B : A → Type b} → _$!_ {A = A} {B = B} ≡ _$_ {A = A} {B = B}
$!≡$ i f x = $!-≡ f x i

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where

open Group G
open import Algebra.FunctionProperties _≈_
open import Relation.Binary.Reasoning.Setoid setoid
open import Function
open import Data.Product

⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x
⁻¹-involutive x = begin
  x ⁻¹ ⁻¹               ≈⟨ sym $ identityʳ _ ⟩
  x ⁻¹ ⁻¹ ∙ ε           ≈⟨ ∙-congˡ $ sym (inverseˡ _) ⟩
  x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x)  ≈⟨ sym $ assoc _ _ _ ⟩
  x ⁻¹ ⁻¹ ∙ x ⁻¹ ∙ x    ≈⟨ ∙-congʳ $ inverseˡ _ ⟩
  ε ∙ x                 ≈⟨ identityˡ _ ⟩
  x                     ∎

private

  left-helper : ∀ x y → x ≈ (x ∙ y) ∙ y ⁻¹
  left-helper x y = begin
    x              ≈⟨ sym (identityʳ x) ⟩
    x ∙ ε          ≈⟨ ∙-congˡ $ sym (inverseʳ y) ⟩
    x ∙ (y ∙ y ⁻¹) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
    (x ∙ y) ∙ y ⁻¹ ∎

  right-helper : ∀ x y → y ≈ x ⁻¹ ∙ (x ∙ y)
  right-helper x y = begin
    y              ≈⟨ sym (identityˡ y) ⟩
    ε          ∙ y ≈⟨ ∙-congʳ $ sym (inverseˡ x) ⟩
    (x ⁻¹ ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
    x ⁻¹ ∙ (x ∙ y) ∎

left-identity-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
left-identity-unique x y eq = begin
  x              ≈⟨ left-helper x y ⟩
  (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩
       y  ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
  ε              ∎

right-identity-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε
right-identity-unique x y eq = begin
  y              ≈⟨ right-helper x y ⟩
  x ⁻¹ ∙ (x ∙ y) ≈⟨ refl ⟨ ∙-cong ⟩ eq ⟩
  x ⁻¹ ∙  x      ≈⟨ inverseˡ x ⟩
  ε              ∎

identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
identity-unique {x} id = left-identity-unique x x (proj₂ id x)

left-inverse-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
left-inverse-unique x y eq = begin
  x              ≈⟨ left-helper x y ⟩
  (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩
       ε  ∙ y ⁻¹ ≈⟨ identityˡ (y ⁻¹) ⟩
            y ⁻¹ ∎

right-inverse-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹
right-inverse-unique x y eq = begin
  y       ≈⟨ sym (⁻¹-involutive y) ⟩
  y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (left-inverse-unique x y eq)) ⟩
  x ⁻¹    ∎


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------

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

module Data.Vec.Relation.Unary.All.Properties where

open import Data.List using ([]; _∷_)
open import Data.List.Relation.Unary.All as List using ([]; _∷_)
open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
open import Data.Vec as Vec
open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
open import Function using (_∘_; id)
open import Function.Inverse using (_↔_; inverse)
open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; cong₂; →-to-⟶)

------------------------------------------------------------------------
-- map

module _ {a b p} {A : Set a} {B : Set b} {P : Pred B p} {f : A → B} where

  map⁺ : ∀ {n} {xs : Vec A n} → All (P ∘ f) xs → All P (map f xs)
  map⁺ []         = []
  map⁺ (px ∷ pxs) = px ∷ map⁺ pxs

  map⁻ : ∀ {n} {xs : Vec A n} → All P (map f xs) → All (P ∘ f) xs
  map⁻ {xs = []}    []       = []
  map⁻ {xs = _ ∷ _} (px ∷ pxs) = px ∷ map⁻ pxs

-- A variant of All.map

module _ {a b p q} {A : Set a} {B : Set b} {f : A → B}
         {P : Pred A p} {Q : Pred B q} where

  gmap : ∀ {n} → P ⋐ Q ∘ f → All P {n} ⋐ All Q {n} ∘ map f
  gmap g = map⁺ ∘ All.map g

------------------------------------------------------------------------
-- _++_

module _ {a n p} {A : Set a} {P : Pred A p} where

  ++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
        All P xs → All P ys → All P (xs ++ ys)
  ++⁺ []         pys = pys
  ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys

  ++ˡ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
         All P (xs ++ ys) → All P xs
  ++ˡ⁻ []       _          = []
  ++ˡ⁻ (x ∷ xs) (px ∷ pxs) = px ∷ ++ˡ⁻ xs pxs

  ++ʳ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
         All P (xs ++ ys) → All P ys
  ++ʳ⁻ []       pys        = pys
  ++ʳ⁻ (x ∷ xs) (px ∷ pxs) = ++ʳ⁻ xs pxs

  ++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
        All P (xs ++ ys) → All P xs × All P ys
  ++⁻ []       p          = [] , p
  ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map₁ (px ∷_) (++⁻ _ pxs)

  ++⁺∘++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
            (p : All P (xs ++ ys)) →
            uncurry′ ++⁺ (++⁻ xs p) ≡ p
  ++⁺∘++⁻ []       p          = refl
  ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = cong (px ∷_) (++⁺∘++⁻ xs pxs)

  ++⁻∘++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
            (p : All P xs × All P ys) →
            ++⁻ xs (uncurry ++⁺ p) ≡ p
  ++⁻∘++⁺ ([]       , pys) = refl
  ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = refl

  ++↔ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
        (All P xs × All P ys) ↔ All P (xs ++ ys)
  ++↔ {xs = xs} = inverse (uncurry ++⁺) (++⁻ xs) ++⁻∘++⁺ (++⁺∘++⁻ xs)

------------------------------------------------------------------------
-- concat

module _ {a m p} {A : Set a} {P : Pred A p} where

  concat⁺ : ∀ {n} {xss : Vec (Vec A m) n} →
            All (All P) xss → All P (concat xss)
  concat⁺ []           = []
  concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)

  concat⁻ : ∀ {n} (xss : Vec (Vec A m) n) →
            All P (concat xss) → All (All P) xss
  concat⁻ []         []   = []
  concat⁻ (xs ∷ xss) pxss = ++ˡ⁻ xs pxss ∷ concat⁻ xss (++ʳ⁻ xs pxss)

------------------------------------------------------------------------
-- toList

module _ {a p} {A : Set a} {P : A → Set p} where

  toList⁺ : ∀ {n} {xs : Vec A n} → All P xs → List.All P (toList xs)
  toList⁺ []         = []
  toList⁺ (px ∷ pxs) = px ∷ toList⁺ pxs

  toList⁻ : ∀ {n} {xs : Vec A n} → List.All P (toList xs) → All P xs
  toList⁻ {xs = []}     []         = []
  toList⁻ {xs = x ∷ xs} (px ∷ pxs) = px ∷ toList⁻ pxs

------------------------------------------------------------------------
-- fromList

module _ {a p} {A : Set a} {P : A → Set p} where

  fromList⁺ : ∀ {xs} → List.All P xs → All P (fromList xs)
  fromList⁺ []         = []
  fromList⁺ (px ∷ pxs) = px ∷ fromList⁺ pxs

  fromList⁻ : ∀ {xs} → All P (fromList xs) → List.All P xs
  fromList⁻ {[]}     []         = []
  fromList⁻ {x ∷ xs} (px ∷ pxs) = px ∷ (fromList⁻ pxs)

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

-- Version 0.16

All-map     = map⁺
{-# WARNING_ON_USAGE All-map
"Warning: All-map was deprecated in v0.16.
Please use map⁺ instead."
#-}
map-All     = map⁻
{-# WARNING_ON_USAGE map-All
"Warning: map-All was deprecated in v0.16.
Please use map⁻ instead."
#-}
All-++⁺     = ++⁺
{-# WARNING_ON_USAGE All-++⁺
"Warning: All-++⁺ was deprecated in v0.16.
Please use ++⁺ instead."
#-}
All-++ˡ⁻    = ++ˡ⁻
{-# WARNING_ON_USAGE All-++ˡ⁻
"Warning: All-++ˡ⁻ was deprecated in v0.16.
Please use ++ˡ⁻ instead."
#-}
All-++ʳ⁻    = ++ʳ⁻
{-# WARNING_ON_USAGE All-++ʳ⁻
"Warning: All-++ʳ⁻ was deprecated in v0.16.
Please use ++ʳ⁻ instead."
#-}
All-++⁻     = ++⁻
{-# WARNING_ON_USAGE All-++⁻
"Warning: All-++⁻ was deprecated in v0.16.
Please use ++⁻ instead."
#-}
All-++⁺∘++⁻ = ++⁺∘++⁻
{-# WARNING_ON_USAGE All-++⁺∘++⁻
"Warning: All-++⁺∘++⁻ was deprecated in v0.16.
Please use ++⁺∘++⁻ instead."
#-}
All-++⁻∘++⁺ = ++⁻∘++⁺
{-# WARNING_ON_USAGE All-++⁻∘++⁺
"Warning: All-++⁻∘++⁺ was deprecated in v0.16.
Please use ++⁻∘++⁺ instead."
#-}
All-concat⁺ = concat⁺
{-# WARNING_ON_USAGE All-concat⁺
"Warning: All-concat⁺ was deprecated in v0.16.
Please use concat⁺ instead."
#-}
All-concat⁻ = concat⁻
{-# WARNING_ON_USAGE All-concat⁻
"Warning: All-concat⁻ was deprecated in v0.16.
Please use concat⁻ 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
-}

module Haskell.Modules.RWS.Lens where

open import Haskell.Modules.RWS
open import Haskell.Prelude
open import Optics.All

private
  variable
    Ev Wr St : Set
    A B C    : Set

-- Lens functionality
--
-- If we make RWS work for different level State types, we will break use and
-- modify because Lens does not support different levels, we define use and
-- modify' here for RoundManager. We are ok as long as we can keep
-- RoundManager in Set. If we ever need to make RoundManager at some higher
-- Level, we will have to consider making Lens level-agnostic. Preliminary
-- exploration by @cwjnkins showed this to be somewhat painful in particular
-- around composition, so we are not pursuing it for now.
use : Lens St A → RWS Ev Wr St A
use f = gets (_^∙ f)

modifyL : Lens St A → (A → A) → RWS Ev Wr St Unit
modifyL l f = modify (over l f)
syntax modifyL l f = l %= f

setL : Lens St A → A → RWS Ev Wr St Unit
setL l x = l %= const x
syntax setL l x = l ∙= x

setL? : Lens St (Maybe A) → A → RWS Ev Wr St Unit
setL? l x = l ∙= just x
syntax setL? l x = l ?= x


text:
module Nat where

open import Base

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_=N_ : Nat -> Nat -> Set
zero  =N zero  = True
zero  =N suc _ = False
suc _ =N zero  = False
suc n =N suc m = n =N m

refN : Refl _=N_
refN {zero}  = T
refN {suc n} = refN {n}

symN : Sym _=N_
symN {zero}{zero} p   = p
symN {suc n}{suc m} p = symN {n}{m} p
symN {zero}{suc _} ()
symN {suc _}{zero} ()

transN : Trans _=N_
transN {zero }{zero }{zero } p _ = p
transN {suc n}{suc m}{suc l} p q = transN {n}{m}{l} p q
transN {zero }{zero }{suc _} _ ()
transN {zero }{suc _}{_    } () _
transN {suc _}{zero }{_    } () _
transN {suc _}{suc _}{zero } _ ()


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- Power Functors, Exponentials over a Category C

-- Mainly categories where the objects are functions (Fin n -> Obj) considered pointwise
--   and then upgraded to Functors.

module Categories.Functor.Power {o ℓ e} (C : Category o ℓ e) where

open Category C
open HomReasoning

open import Level using (Level; _⊔_)
open import Data.Nat using (ℕ; _+_; zero; suc; _<_)
open import Data.Product using (_,_)
open import Data.Fin using (Fin; inject+; raise; zero; suc; fromℕ<)
open import Data.Sum using (_⊎_; inj₁; inj₂; map) renaming ([_,_] to ⟦_,_⟧; [_,_]′ to ⟦_,_⟧′)
open import Data.Vec.N-ary hiding (curryⁿ)
open import Function as Fun using (flip; _$_) renaming (_∘_ to _∙_; id to idf)

open import Categories.Category.Product using (Product; _⁂_)
open import Categories.Functor hiding (id)
open import Categories.Functor.Bifunctor using (Bifunctor; overlap-×)

private
  variable
    i j k : Level
    I I′ J J′ : Set i
    D E : Category i j k
    n n′ m m′ : ℕ

Exp : Set i → Category _ _ _
Exp I = record
  { Obj       = I → Obj
  ; _⇒_       = λ x y → ∀ i → x i ⇒ y i
  ; _≈_       = λ f g → ∀ i → f i ≈ g i
  ; id        = λ _ → id
  ; _∘_       = λ f g i → f i ∘ g i
  ; assoc     = λ _ → assoc
  ; sym-assoc = λ _ → sym-assoc
  ; identityˡ = λ _ → identityˡ
  ; identityʳ = λ _ → identityʳ
  ; identity² = λ _ → identity²
  ; equiv     = record
    { refl  = λ _ → refl
    ; sym   = λ eq i → sym $ eq i
    ; trans = λ eq₁ eq₂ i → trans (eq₁ i) (eq₂ i)
    }
  ; ∘-resp-≈  = λ eq₁ eq₂ i → ∘-resp-≈ (eq₁ i) (eq₂ i)
  }

Power : (n : ℕ) → Category o ℓ e
Power n = Exp (Fin n)

-- Convention: the ′ version is for a general index set, unprimed for a ℕ
-- representing Fin n.  So Powerfunctor D n is Exp C (Fin n) ⇒ D, i.e.
-- essentially C ^ n ⇒ D.
Powerfunctor′ : (D : Category o ℓ e) (I : Set i) → Set (i ⊔ e ⊔ ℓ ⊔ o)
Powerfunctor′ D I = Functor (Exp I) D

Powerfunctor : (D : Category o ℓ e) (n : ℕ) → Set (e ⊔ ℓ ⊔ o)
Powerfunctor D n = Powerfunctor′ D (Fin n)

-- With C = D, so Powerendo n is C ^ n => C
Powerendo′ : (I : Set i) → Set (i ⊔ e ⊔ ℓ ⊔ o)
Powerendo′ I = Powerfunctor′ C I

Powerendo : (n : ℕ) → Set (e ⊔ ℓ ⊔ o)
Powerendo n = Powerfunctor C n

-- Hyperendo n m is C ^ n ⇒ C ^ m
Hyperendo : (n m : ℕ) → Set (e ⊔ ℓ ⊔ o)
Hyperendo n m = Functor (Power n) (Power m)

-- Hyperendo′ I J is C ^ I → C ^ J
Hyperendo′ : (I : Set i) (J : Set j) → Set (i ⊔ j ⊔ e ⊔ ℓ ⊔ o)
Hyperendo′ I J = Functor (Exp I) (Exp J)

-- Parallel composition of Hyperendo′ (via disjoint union of index sets)
infixr 9 _par_

_par_ : (F : Hyperendo′ I I′) (G : Hyperendo′ J J′) → Hyperendo′ (I ⊎ J) (I′ ⊎ J′)
F par G = record
  { F₀           = λ xs →  ⟦ F.F₀ (xs ∙ inj₁) , G.F₀ (xs ∙ inj₂) ⟧′
  ; F₁           = λ fs → ⟦ F.F₁ (fs ∙ inj₁) , G.F₁ (fs ∙ inj₂) ⟧
  ; identity     = ⟦ F.identity , G.identity ⟧
  ; homomorphism = ⟦ F.homomorphism , G.homomorphism ⟧
  ; F-resp-≈     = λ fs≈gs → ⟦ F.F-resp-≈ (fs≈gs ∙ inj₁) , G.F-resp-≈ (fs≈gs ∙ inj₂) ⟧
  }
  where module F = Functor F
        module G = Functor G

-- "flattening" means going from a general disjoint union of Fin to a single Fin,
-- which has the effect of doing from Powerfunctor′ to Powerfunctor
flattenP : (F : Powerfunctor′ D (Fin n ⊎ Fin m)) → Powerfunctor D (n + m)
flattenP {n = n} {m = m} F = record
  { F₀           = λ As → F₀ (As ∙ pack)
  ; F₁           = λ fs → F₁ (fs ∙ pack)
  ; identity     = identity
  ; homomorphism = homomorphism
  ; F-resp-≈     = λ fs≈gs → F-resp-≈ (fs≈gs ∙ pack)
  }
  where open Functor F
        pack = ⟦ inject+ m , raise n ⟧′

-- TODO unpackFun (and pack above) should be in stdlib
private
  unpackFin : ∀ n → Fin (n + m) → Fin n ⊎ Fin m
  unpackFin zero f          = inj₂ f
  unpackFin (suc n) zero    = inj₁ zero
  unpackFin (suc n) (suc f) = map suc idf (unpackFin n f)

-- needs a better name?
unflattenP : Powerfunctor D (n + m) → Powerfunctor′ D (Fin n ⊎ Fin m)
unflattenP {n = n} {m = m} F = record
  { F₀           = λ As → F₀ (As ∙ unpackFin _)
  ; F₁           = λ fs → F₁ (fs ∙ unpackFin _)
  ; identity     = identity
  ; homomorphism = homomorphism
  ; F-resp-≈     = λ fs≈gs → F-resp-≈ (fs≈gs ∙ unpackFin _)
  }
  where open Functor F

-- flatten a Hyperendo′ "on the right" when over a union of Fin
flattenHʳ : (F : Hyperendo′ I (Fin n ⊎ Fin m)) → Hyperendo′ I (Fin (n + m))
flattenHʳ {n = n} {m = m} F = record
  { F₀           = λ As → F₀ As ∙ unpackFin n
  ; F₁           = λ fs → F₁ fs ∙ unpackFin n
  ; identity     = identity ∙ unpackFin n
  ; homomorphism = homomorphism ∙ unpackFin n
  ; F-resp-≈     = λ fs≈gs → F-resp-≈ fs≈gs ∙ unpackFin n
  }
  where open Functor F

-- flatten on both sides.
flattenH : (F : Hyperendo′ (Fin n ⊎ Fin m) (Fin n′ ⊎ Fin m′)) → Hyperendo (n + m) (n′ + m′)
flattenH = flattenHʳ ∙ flattenP

-- Pretty syntax for flattening of parallel composition of Hyperendo
infixr 9 _∥_

_∥_ : (F : Hyperendo n n′) (G : Hyperendo m m′) → Hyperendo (n + m) (n′ + m′)
F ∥ G = flattenH (F par G)

-- split is C ^ (I ⊎ J) to C ^ I × C ^ J, as a Functor
split : Functor (Exp (I ⊎ J)) (Product (Exp I) (Exp J))
split = record
  { F₀           = λ As → As ∙ inj₁ , As ∙ inj₂
  ; F₁           = λ fs → fs ∙ inj₁ , fs ∙ inj₂
  ; identity     = (λ _ → refl) , λ _ → refl
  ; homomorphism = (λ _ → refl) , λ _ → refl
  ; F-resp-≈     = λ eq → (λ i → eq (inj₁ i)) , λ i → eq (inj₂ i)
  }

reduce′ : (H : Bifunctor C C C) (F : Powerendo′ I) (G : Powerendo′ J) → Powerendo′ (I ⊎ J)
reduce′ H F G = H ∘F (F ⁂ G) ∘F split

reduce : ∀ (H : Bifunctor C C C) {n m} (F : Powerendo n) (G : Powerendo m) → Powerendo (n + m)
reduce H F G = flattenP $ reduce′ H F G

flattenP-assocʳ : ∀ {n₁ n₂ n₃} (F : Powerendo′ (Fin n₁ ⊎ Fin n₂ ⊎ Fin n₃)) → Powerendo (n₁ + n₂ + n₃)
flattenP-assocʳ {n₁} {n₂} {n₃} F = record
  { F₀           = λ As → F.F₀ (As ∙ pack)
  ; F₁           = λ fs → F.F₁ (fs ∙ pack)
  ; identity     = F.identity
  ; homomorphism = F.homomorphism
  ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ (fs≈gs ∙ pack)
  }
  where module F = Functor F
        pack = ⟦ inject+ n₃ ∙ inject+ n₂ , ⟦ inject+ n₃ ∙ raise n₁ , raise (n₁ + n₂) ⟧′ ⟧′

reduce2ʳ : ∀ (G : Bifunctor C C C) {n₁ n₂ n₃} (F₁ : Powerendo n₁) (F₂ : Powerendo n₂) (F₃ : Powerendo n₃) → Powerendo ((n₁ + n₂) + n₃)
reduce2ʳ G F₁ F₂ F₃ = flattenP-assocʳ $ reduce′ G F₁ $ reduce′ G F₂ F₃

overlaps : (H : Bifunctor D D E) (F G : Powerfunctor′ D I) → Powerfunctor′ E I
overlaps = overlap-×

overlap2ʳ : (G : Bifunctor C C C) (F₁ F₂ F₃ : Powerendo n) → Powerendo n
overlap2ʳ G F₁ F₂ F₃ = overlaps G F₁ (overlaps G F₂ F₃)

-- select′ i always evaluates at i
select′ : (i : I) → Powerendo′ I
select′ i = record
  { F₀           = _$ i
  ; F₁           = _$ i
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = _$ i
  }

-- select (m < n) is really select′ (Fin n), but only for m < n
select : m < n → Powerendo n
select m<n = select′ (fromℕ< m<n)

triv : (n : ℕ) → Hyperendo n n
triv n = record
  { F₀           = idf
  ; F₁           = idf
  ; identity     = λ _ → refl
  ; homomorphism = λ _ → refl
  ; F-resp-≈     = idf
  }

-- pad a Hyperendo on the left and right by trivial (i.e. identity) endofunctors
pad : ∀ (l r : ℕ) (F : Hyperendo n m) → Hyperendo ((l + n) + r) ((l + m) + r)
pad l r F = (triv l ∥ F) ∥ triv r

padˡ : ∀ (l : ℕ) (F : Hyperendo n m) → Hyperendo (l + n) (l + m)
padˡ l F = triv l ∥ F

padʳ : ∀ (r : ℕ) (F : Hyperendo n m) → Hyperendo (n + r) (m + r)
padʳ r F = F ∥ triv r

unary : Endofunctor C → Powerendo 1
unary F = record
  { F₀           = λ As → F.F₀ (As zero)
  ; F₁           = λ fs → F.F₁ (fs zero)
  ; identity     = F.identity
  ; homomorphism = F.homomorphism
  ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ (fs≈gs zero)
  }
  where module F = Functor F

unaryH : Endofunctor C → Hyperendo 1 1
unaryH F = record
  { F₀           = λ As → F.F₀ ∙ As
  ; F₁           = λ fs → F.F₁ ∙ fs
  ; identity     = λ _ → F.identity
  ; homomorphism = λ _ → F.homomorphism
  ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ ∙ fs≈gs
  }
  where module F = Functor F

-- "constant"
nullary : Obj → Powerendo 0
nullary X = record
  { F₀           = λ _ → X
  ; F₁           = λ _ → id
  ; identity     = refl
  ; homomorphism = sym identity²
  ; F-resp-≈     = λ _ → refl
  }

nullaryH : Obj → Hyperendo 0 1
nullaryH X = record
  { F₀           = λ _ _ → X
  ; F₁           = λ _ _ → id
  ; identity     = λ _ → refl
  ; homomorphism = λ _ → sym identity²
  ; F-resp-≈     = λ _ _ → refl
  }

binary : Bifunctor C C C → Powerendo 2
binary F = record
  { F₀           = λ As → F.F₀ (As zero , As (suc zero))
  ; F₁           = λ fs → F.F₁ (fs zero , fs (suc zero))
  ; identity     = F.identity
  ; homomorphism = F.homomorphism
  ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ (fs≈gs zero , fs≈gs (suc zero))
  }
  where module F = Functor F

binaryH : Bifunctor C C C → Hyperendo 2 1
binaryH F = record
  { F₀           = λ As _ → F.F₀ (As zero , As (suc zero))
  ; F₁           = λ fs _ → F.F₁ (fs zero , fs (suc zero))
  ; identity     = λ _ → F.identity
  ; homomorphism = λ _ → F.homomorphism
  ; F-resp-≈     = λ fs≈gs _ → F.F-resp-≈ (fs≈gs zero , fs≈gs (suc zero))
  }
  where module F = Functor F

hyp : Powerendo n → Hyperendo n 1
hyp F = record
  { F₀           = λ As _ → F.F₀ As
  ; F₁           = λ fs _ → F.F₁ fs
  ; identity     = λ _ → F.identity
  ; homomorphism = λ _ → F.homomorphism
  ; F-resp-≈     = λ fs≈gs _ → F.F-resp-≈ fs≈gs
  }
  where module F = Functor F

private
  curryⁿ : ∀ n {a b} {A : Set a} {B : Set b} → ((Fin n → A) → B) → N-ary n A B
  curryⁿ zero f     = f (λ ())
  curryⁿ (suc n) {A = A} f = λ x → curryⁿ n (f ∙ addon x)
    where addon : A → (Fin n → A) → Fin (suc n) → A
          addon x _ zero    = x
          addon _ g (suc i) = g i

plex′ : (J → Powerendo′ I) → Hyperendo′ I J
plex′ Fs = record
  { F₀           = flip (Functor.F₀ ∙ Fs)
  ; F₁           = flip (λ j → Functor.F₁ (Fs j))
  ; identity     = λ j → Functor.identity (Fs j)
  ; homomorphism = λ j → Functor.homomorphism (Fs j)
  ; F-resp-≈     = flip (λ j → Functor.F-resp-≈ (Fs j))
  }

plex : N-ary n (Powerendo′ I) (Hyperendo′ I (Fin n))
plex {n = n} = curryⁿ n plex′

-- like pad, but for Powerendo -- on left or right.
widenˡ : ∀ (l : ℕ) (F : Powerendo n) → Powerendo (l + n)
widenˡ l F = record
  { F₀           = λ As → F.F₀ (As ∙ pack)
  ; F₁           = λ {As Bs} fs → F.F₁ (fs ∙ pack)
  ; identity     = F.identity
  ; homomorphism = F.homomorphism
  ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ (fs≈gs ∙ pack)
  }
  where module F = Functor F
        pack = raise l

widenʳ : ∀ (r : ℕ) (F : Powerendo n) → Powerendo (n + r)
widenʳ r F = record
  { F₀           = λ As → F.F₀ (As ∙ pack)
  ; F₁           = λ fs → F.F₁ (fs ∙ pack)
  ; identity     = F.identity
  ; homomorphism = F.homomorphism
  ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ (fs≈gs ∙ pack)
  }
  where module F = Functor F
        pack = inject+ r


text:
------------------------------------------------------------------------
-- Possibly infinite binary trees
------------------------------------------------------------------------

module Tree where

open import Codata.Musical.Notation
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)

data Tree (A : Set) : Set where
  leaf : Tree A
  node : (l : ∞ (Tree A)) (x : A) (r : ∞ (Tree A)) → Tree A

map : ∀ {A B} → (A → B) → Tree A → Tree B
map f leaf         = leaf
map f (node l x r) = node (♯ map f (♭ l)) (f x) (♯ map f (♭ r))

data _≈_ {A : Set} : (t₁ t₂ : Tree A) → Set where
  leaf : leaf ≈ leaf
  node : ∀ {l₁ l₂ x₁ x₂ r₁ r₂}
         (l≈ : ∞ (♭ l₁ ≈ ♭ l₂)) (x≡ : x₁ ≡ x₂) (r≈ : ∞ (♭ r₁ ≈ ♭ r₂)) →
         node l₁ x₁ r₁ ≈ node l₂ x₂ r₂

refl : ∀ {A} (t : Tree A) → t ≈ t
refl leaf         = leaf
refl (node l x r) = node (♯ refl (♭ l)) PropEq.refl (♯ refl (♭ r))

trans : ∀ {A} {t₁ t₂ t₃ : Tree A} →
        t₁ ≈ t₂ → t₂ ≈ t₃ → t₁ ≈ t₃
trans leaf            leaf               = leaf
trans (node l≈ x≡ r≈) (node l≈′ x≡′ r≈′) =
  node (♯ trans (♭ l≈) (♭ l≈′)) (PropEq.trans x≡ x≡′)
       (♯ trans (♭ r≈) (♭ r≈′))

map-cong : ∀ {A B} (f : A → B) {t₁ t₂ : Tree A} →
           t₁ ≈ t₂ → map f t₁ ≈ map f t₂
map-cong f leaf            = leaf
map-cong f (node l≈ x≡ r≈) =
  node (♯ map-cong f (♭ l≈)) (PropEq.cong f x≡) (♯ map-cong f (♭ r≈))

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- N-ary products
------------------------------------------------------------------------

-- Vectors (as in Data.Vec) also represent n-ary products, so what is
-- the point of this module? The n-ary products below are intended to
-- be used with a fixed n, in which case the nil constructor can be
-- avoided: pairs are represented as pairs (x , y), not as triples
-- (x , y , unit).

module Data.Product.N-ary where

open import Data.Nat
open import Data.Product
open import Data.Unit
open import Data.Vec
open import Function.Inverse
open import Level using (Lift; lift)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

-- N-ary product.

infix 8 _^_

_^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
A ^ 0           = Lift ⊤
A ^ 1           = A
A ^ suc (suc n) = A × A ^ suc n

-- Conversions.

↔Vec : ∀ {a} {A : Set a} n → A ^ n ↔ Vec A n
↔Vec n = record
  { to         = P.→-to-⟶ (toVec n)
  ; from       = P.→-to-⟶ fromVec
  ; inverse-of = record
    { left-inverse-of  = fromVec∘toVec n
    ; right-inverse-of = toVec∘fromVec
    }
  }
  where
  toVec : ∀ {a} {A : Set a} n → A ^ n → Vec A n
  toVec 0             (lift tt) = []
  toVec 1             x         = [ x ]
  toVec (suc (suc n)) (x , xs)  = x ∷ toVec _ xs

  fromVec : ∀ {a} {A : Set a} {n} → Vec A n → A ^ n
  fromVec []           = lift tt
  fromVec (x ∷ [])     = x
  fromVec (x ∷ y ∷ xs) = (x , fromVec (y ∷ xs))

  fromVec∘toVec : ∀ {a} {A : Set a} n (xs : A ^ n) →
                  fromVec (toVec n xs) ≡ xs
  fromVec∘toVec 0                   (lift tt)    = P.refl
  fromVec∘toVec 1                   x            = P.refl
  fromVec∘toVec 2                   (x , y)      = P.refl
  fromVec∘toVec (suc (suc (suc n))) (x , y , xs) =
    P.cong (_,_ x) (fromVec∘toVec (suc (suc n)) (y , xs))

  toVec∘fromVec : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
                  toVec n (fromVec xs) ≡ xs
  toVec∘fromVec []           = P.refl
  toVec∘fromVec (x ∷ [])     = P.refl
  toVec∘fromVec (x ∷ y ∷ xs) = P.cong (_∷_ x) (toVec∘fromVec (y ∷ xs))


text:
module Properties.Equality where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Properties.Contradiction using (¬)

sym : ∀ {A : Set} {a b : A} → (a ≡ b) → (b ≡ a)
sym refl = refl

trans : ∀ {A : Set} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c)
trans refl refl = refl

cong : ∀ {A B : Set} {a b : A} (f : A → B) → (a ≡ b) → (f a ≡ f b)
cong f refl = refl

subst₁ : ∀ {A : Set} {a b : A} (F : A → Set) → (a ≡ b) → (F a) → (F b)
subst₁ F refl x = x

subst₂ : ∀ {A B : Set} {a b : A} {c d : B} (F : A → B → Set) → (a ≡ b) → (c ≡ d) → (F a c) → (F b d)
subst₂ F refl refl x = x

_≢_ : ∀ {A : Set} → A → A → Set
(a ≢ b) = ¬(a ≡ b)

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


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

{-
  Ribbon is an explicit covering space construction.

  This construction is given by Daniel Grayson, Favonia
  and Guillaume Brunerie together.
-}

open import HoTT

-- A is the pointed base space.
-- El is intended to be a (group-)set,
module homotopy.RibbonCover {i : ULevel} where

  -- The HIT ribbon---reconstructed covering space

  private
    π1 = fundamental-group

  private
    module _ (A∙ : Ptd i) {j} (gs : Gset (π1 A∙) j) where
      private
        A = fst A∙
        a = snd A∙
        El = Gset.El gs
        El-level = Gset.El-level gs
        _⊙_ = Gset.act gs

      {-
        What the following data type definition should be
        when we have a proof assistant for HoTT:

        data Ribbon (a₂ : A) : Set where
          trace : El → a =₀ a₂ → Ribbon a₂
          paste : ∀ el loop (p : a =₀ a₂)
                → trace (el ⊙ loop) p == trace el (loop ∙₀ p)
      -}

      data #Ribbon-aux (a₂ : A) : Type (lmax i j) where
        #trace : El → a =₀ a₂ → #Ribbon-aux a₂

      data #Ribbon (a₂ : A) : Type (lmax i j) where
        #ribbon : #Ribbon-aux a₂ → (Unit → Unit) → #Ribbon a₂

  Ribbon : ∀ (A∙ : Ptd i) {j} (gs : Gset (π1 A∙) j)
    → fst A∙ → Type (lmax i j)
  Ribbon = #Ribbon

  module _ {A∙ : Ptd i} {j} {gs : Gset (fundamental-group A∙) j} {a₂ : fst A∙} where
    private
      A = fst A∙
      a = snd A∙
      El = Gset.El gs
      El-level = Gset.El-level gs
      _⊙_ = Gset.act gs

    -- A point in the fiber [a₂].
    {-
      [e] is a point in the [fiber a], and
      [p] is a path to transport [y] to fiber [a₂].
    -}
    trace : El → a =₀ a₂ → Ribbon A∙ gs a₂
    trace el p = #ribbon (#trace el p) _

    {-
      A loop based at [a] can used as a group action
      or for concatination.  Both should be equivalent.
    -}
    postulate -- HIT
      paste : ∀ el loop (p : a =₀ a₂)
        → trace (el ⊙ loop) p == trace el (loop ∙₀ p)

    {-
      Make each fiber a set and cancel all higher structures
      due to [paste].
    -}
    postulate -- HIT
      Ribbon-is-set : is-set (Ribbon A∙ gs a₂)

    Ribbon-level = Ribbon-is-set

    -- Elimination rules.
    module RibbonElim {j} {P : Ribbon A∙ gs a₂ → Type j}
      (P-level : ∀ {r} → is-set (P r))
      (trace* : ∀ el p → P (trace el p))
      (paste* : ∀ el loop p
                → trace* (el ⊙ loop) p == trace* el (loop ∙₀ p)
                  [ P ↓ paste el loop p ]) where

      f : Π (Ribbon A∙ gs a₂) P
      f = f-aux phantom phantom where

        f-aux : Phantom trace* → Phantom paste* → Π (Ribbon A∙ gs a₂) P
        f-aux phantom phantom (#ribbon (#trace el p) _) = trace* el p

    open RibbonElim public using () renaming (f to Ribbon-elim)

    module RibbonRec {j} {P : Type j}
      (P-level : is-set P)
      (trace* : ∀ el p → P)
      (paste* : ∀ el loop p
                → trace* (el ⊙ loop) p == trace* el (loop ∙₀ p)) where

      private
        module M = RibbonElim P-level trace*
          (λ el loop p → ↓-cst-in (paste* el loop p))

      f : Ribbon A∙ gs a₂ → P
      f = M.f

    open RibbonRec public using () renaming (f to Ribbon-rec)

  -- This data structure gives a cover.
  Ribbon-cover : ∀ (A∙ : Ptd i) {j} (gs : Gset (π1 A∙) j)
    → Cover (fst A∙) (lmax i j)
  Ribbon-cover A∙ gs = record
    { Fiber = Ribbon A∙ gs
    ; Fiber-level = λ a → Ribbon-level
    }

  trans-trace : ∀ {A : Type i} {a₁} {j}
    {gs : Gset (π1 (A , a₁)) j}
    {a₂} (q : a₁ == a₂) y p
    → transport (Ribbon (A , a₁) gs) q (trace y p) == trace y (p ∙₀ [ q ])
  trans-trace idp y p = ap (trace y) $ ! $ ∙₀-unit-r p

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


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

module Equality where

import Algebra.FunctionProperties
import Algebra.Structures
open import Cubical.Core.Everything public hiding (module Σ)
open import Data.Empty
open import Data.Nat as ℕ
open import Data.Nat.Properties
open import Data.Product as Σ
open import Data.Unit
open import Function
open import Quotient
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as ♥ public using () renaming (refl to ♥)

open module FunctionProperties {a} {A : Set a} =
  Algebra.FunctionProperties {A = A} _≡_

open module Structures {a} {A : Set a} =
  Algebra.Structures {A = A} _≡_

coe : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
coe = subst id

infix 1 _$⃗_
_$⃗_ : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
_$⃗_ = coe

infix 1 _$⃖_
_$⃖_ : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → B → A
p $⃖ x = sym p $⃗ x

≡-isEquivalence : ∀ {ℓ} {A : Set ℓ} → IsEquivalence {A = A} _≡_
≡-isEquivalence = record
  { refl = refl
  ; sym = sym
  ; trans = compPath
  }

≡-isPreorder : ∀ {ℓ} {A : Set ℓ} → IsPreorder {A = A} _≡_ _≡_
≡-isPreorder = record
  { isEquivalence = ≡-isEquivalence
  ; reflexive = id
  ; trans = compPath
  }

module _ {ℓ} {A : Set ℓ} {a b : A} where
  ⟨_⟩ : a ♥.≡ b → a ≡ b
  ⟨ ♥ ⟩ = refl

  ⟪_⟫ : a ≡ b → a ♥.≡ b
  ⟪_⟫ = J (λ x _ → _ ♥.≡ x) ♥

infixl 5 _≫_
_≫_ : ∀ {ℓ} {A : Set ℓ} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
_≫_ = compPath

module _ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} {f f′ : A → B} where
  happly : ∀ a → f ≡ f′ → f a ≡ f′ a
  happly a = cong λ g → g a

  congApp : ∀ {a a′} → f ≡ f′ → a ≡ a′ → f a ≡ f′ a′
  congApp p q = compPath (happly _ p) (cong f′ q)

cong₂ : ∀
  {ℓ₁ ℓ₂ ℓ₃} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  {a a′} {b b′}
  (f : A → B → C) →
  a ≡ a′ → b ≡ b′ →
  f a b ≡ f a′ b′
cong₂ f p q = congApp (cong f p) q


text:
open import Level
module ordinal where

open import logic
open import nat
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions
open import Data.Nat.Properties
open import Relation.Nullary
open import Relation.Binary.Core

----
--
-- Countable Ordinals
--

data OrdinalD {n : Level} :  (lv : Nat) → Set n where
   Φ : (lv : Nat) → OrdinalD  lv
   OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv

record Ordinal {n : Level} : Set n where
   constructor ordinal
   field
     lv : Nat
     ord : OrdinalD {n} lv

data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
   Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
   s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y

open Ordinal

_o<_ : {n : Level} ( x y : Ordinal ) → Set n
_o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )

s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
s<refl {n} {lv} {Φ lv}  = Φ<
s<refl {n} {lv} {OSuc lv x}  = s< s<refl

trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()

d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
d<→lv Φ< = refl
d<→lv (s< lt) = refl

o∅ : {n : Level} → Ordinal {n}
o∅  = record { lv = Zero ; ord = Φ Zero }

open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)

ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
      lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
ordinal-cong refl refl = refl

≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t

trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
trio<≡ refl = ≡→¬d<

trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
trio>≡ refl = ≡→¬d<

triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> (  λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)

osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
osuc record { lv = lx ; ord = ox } = record { lv = lx ; ord = OSuc lx ox }

<-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
<-osuc {n} {record { lv = lx ; ord = Φ .lx }} =  case2 Φ<
<-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl )

o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy  → ox o< oy  → ⊥
o<¬≡ {_} {ox} {ox} refl (case1 lt) =  =→¬< lt
o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt

¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
¬x<0 {n} {x} (case1 ())
¬x<0 {n} {x} (case2 ())

o<> : {n : Level} →  {x y : Ordinal {n}  }  →  y o< x → x o< y → ⊥
o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<>  x₁ x₂
o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁
o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂
o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) (case2 ())
o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) =
   o<> (case2 y<x) (case2 x<y)

orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ<
orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )

osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)
osuc-≡< {n} {a} {x} (case1 lt) = case2 (case1 lt)
osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case1 refl
osuc-≡< {n} {record { lv = lv₁ ; ord = OSuc .lv₁ ord₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case2 (case2 Φ<)
osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< ()))
osuc-≡< {n} {record { lv = la ; ord = OSuc la oa }} {record { lv = la ; ord = (OSuc la ox) }} (case2 (s< lt)) with
      osuc-≡< {n} {record { lv = la ; ord = oa }} {record { lv = la ; ord = ox }} (case2 lt )
... | case1 refl = case1 refl
... | case2 (case2 x) = case2 (case2( s< x) )
... | case2 (case1 x) = ⊥-elim (¬a≤a  x)

osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x  → x o< y → ⊥
osuc-< {n} {x} {y} y<ox x<y with osuc-≡< y<ox
osuc-< {n} {x} {x} y<ox (case1 x₁) | case1 refl = ⊥-elim (¬a≤a x₁)
osuc-< {n} {x} {x} (case1 x₂) (case2 x₁) | case1 refl = ⊥-elim (¬a≤a x₂)
osuc-< {n} {x} {x} (case2 x₂) (case2 x₁) | case1 refl = ≡→¬d<  x₁
osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₂ x₁
osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case2 x₁) = nat-≡< (sym (d<→lv x₁)) x₂
osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 y<x = o<> (case2 x<y) y<x

ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with  d<→lv x₂
... | refl = case1 x₁
ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂)  with  d<→lv x₁
... | refl = case1 x₂
ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
... | refl | refl = case2 ( orddtrans x₁ x₂ )

trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_
trio< a b with <-cmp (lv a) (lv b)
trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
   lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
   lemma1 (case1 x) = ¬c x
   lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) a₁  )
trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
   lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
   lemma1 (case1 x) = ¬a x
   lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) c  )
trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
   lemma1 refl = refl
   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
   lemma2 (case1 x) = ¬a x
   lemma2 (case2 x) = trio<> x a
trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
   lemma1 refl = refl
   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
   lemma2 (case1 x) = ¬a x
   lemma2 (case2 x) = trio<> x c
trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
   lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
   lemma1 (case1 x) = ¬a x
   lemma1 (case2 x) = ≡→¬d< x

open _∧_

TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
  → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
  → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
  →  ∀ (x : Ordinal)  → ψ x
TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where
  TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
  TransFinite1 Zero (Φ 0) = ⟪  caseΦ Zero lemma , lemma1 ⟫ where
      lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
      lemma x (case1 ())
      lemma x (case2 ())
      lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
      lemma1 x (case1 ())
      lemma1 x (case2 ())
  TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where
      lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
      lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
      lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
      lemma lx1 ox1            (case1 lt) with <-∨ lt
      lemma lx (Φ lx)          (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
      lemma lx (Φ lx)          (case1 lt) | case2 lt1 = lemma0  lx (Φ lx) (case1 lt1)
      lemma lx (OSuc lx ox1)   (case1 lt) | case1 refl = caseOSuc lx ox1 lemma2 where
          lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx ox1) → ψ y
          lemma2 y lt1 with osuc-≡< lt1
          lemma2 y lt1 | case1 refl = lemma lx ox1 (case1 a<sa)
          lemma2 y lt1 | case2 t = proj2 (TransFinite1 lx ox1) y t
      lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 lemma2 where
          lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx1) ∨ (ord y d< OSuc lx1 ox1) → ψ y
          lemma2 y lt2 with osuc-≡< lt2
          lemma2 y lt2 | case1 refl = lemma lx1 ox1 (ordtrans lt2 (case1 lt))
          lemma2 y lt2 | case2 (case1 lt3) = proj2 (TransFinite1 lx (Φ lx)) y (case1 (<-trans lt3 lt1 ))
          lemma2 y lt2 | case2 (case2 lt3) with d<→lv lt3
          ... | refl = proj2 (TransFinite1 lx (Φ lx)) y (case1 lt1)
  TransFinite1 lx (OSuc lx ox)  = ⟪ caseOSuc lx ox lemma , lemma ⟫ where
      lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y
      lemma y lt with osuc-≡< lt
      lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )
      lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1

--  record CountableOrdinal {n : Level} : Set (suc (suc n)) where
--     field
--         ctl→ : Nat → Ordinal {suc n}
--         ctl← : Ordinal → Nat
--         ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x
--         ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
--
--  is-C-Ordinal : {n : Level} → CountableOrdinal {n}
--  is-C-Ordinal {n} = record {
--         ctl→ = {!!}
--      ;  ctl← = λ x → TransFinite {n} (λ lx lt → Zero ) ctl01 x
--      ;  ctl-iso→ = {!!}
--      ;  ctl-iso← = {!!}
--    } where
--        ctl01 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → Nat) → Nat
--        ctl01 Zero (Φ Zero) prev = Zero
--        ctl01 Zero (OSuc Zero x) prev = Suc ( prev (ordinal Zero x) (ordtrans <-osuc <-osuc ))
--        ctl01 (Suc lx) (Φ (Suc lx)) prev = Suc ( prev (ordinal lx {!!}) {!!})
--        ctl01 (Suc lx) (OSuc (Suc lx) x) prev = Suc ( prev (ordinal (Suc lx) x) (ordtrans <-osuc <-osuc ))

open import Ordinals

C-Ordinal : {n : Level} →  Ordinals {suc n}
C-Ordinal {n} = record {
     Ordinal = Ordinal {suc n}
   ; o∅ = o∅
   ; osuc = osuc
   ; _o<_ = _o<_
   ; next = next
   ; isOrdinal = record {
       ordtrans = ordtrans
     ; trio< = trio<
     ; ¬x<0 = ¬x<0
     ; <-osuc = <-osuc
     ; osuc-≡< = osuc-≡<
     ; TransFinite = TransFinite2
     ; Oprev-p  = Oprev-p
   } ;
   isNext = record {
        x<nx = x<nx
      ; osuc<nx = λ {x} {y} → osuc<nx {x} {y}
      ; ¬nx<nx = ¬nx<nx
   }
  } where
     next : Ordinal {suc n} → Ordinal {suc n}
     next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
     x<nx :    { y : Ordinal } → (y o< next y )
     x<nx = case1 a<sa
     osuc<nx : { x y : Ordinal } → x o< next y → osuc x o< next y
     osuc<nx (case1 lt) = case1 lt
     ¬nx<nx :  {x y : Ordinal} → y o< x → x o< next y →  ¬ ((z : Ordinal) → ¬ (x ≡ osuc z))
     ¬nx<nx {x} {y} = lemma2 x where
         lemma2 : (x : Ordinal) → y o< x → x o< next y → ¬ ((z : Ordinal) → ¬ x ≡ osuc z)
         lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not
         lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl
         lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl
         lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl
         lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
             lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
             lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
     open Oprev
     Oprev-p  : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n})  osuc x )
     Oprev-p  (ordinal lv (Φ lv)) = no (λ not → lemma (oprev not) (oprev=x not) ) where
          lemma : (x : Ordinal) → osuc x ≡ (ordinal lv (Φ lv)) → ⊥
          lemma x ()
     Oprev-p  (ordinal lv (OSuc lv ox)) = yes record { oprev = ordinal lv ox ; oprev=x = refl }
     ord1 : Set (suc n)
     ord1 = Ordinal {suc n}
     TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
          →  ∀ (x : ord1)  → ψ x
     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
            ψ (record { lv = lx ; ord = Φ lx })
        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
            ψ (record { lv = lx ; ord = OSuc lx x₁ })
        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
{-# OPTIONS --sized-types #-}
-- {-# OPTIONS -v tc.size.solve:20 -v tc.decl.ax:10 #-}
module SizeUnsolvedConstraintsInTypeSignature where

open import Common.Size

data Nat : (i : Size) -> Set where
  Z : {i : Size} -> Nat (↑ i)
  S : {i : Size} -> Nat i → Nat (↑ i)

one1 : (i : Size) → Nat (↑ (↑ i))
one1 i = S Z

one2 : (i : Size) → Nat (↑ (↑ (↑ i)))
one2 i = S Z

postulate
  _≡_   : {A : Set} → A → A → Set
  works : (i : Size) → one2 i ≡ one1 i

  bug   : (i : Size) → one1 i ≡ one2 i
  -- bug caused an interal error due to absense of range info
  -- should not print a proper error message (or better, work!)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda