text:
module ExpressionChanging where
open import ParseTree
open import Data.Maybe hiding (map)
open import Data.List.NonEmpty
open import ParseTreeOperations
open import AgdaHelperFunctions
open import Data.List
open import Data.Nat
open import Data.Vec using (Vec)
open import Data.Fin
open import ScopeState
import Data.Nat.Properties
open import Relation.Nullary
import Data.String
open import Data.Nat.Show
open import Data.Bool

{-# TERMINATING #-}
applyToExpressionsAndSubExpressions : (List⁺ Expr -> List⁺ Expr) -> Expr -> Expr
applyToExpressionsAndSubExpressions i e = listToExpression $ head newTop ∷ newRest
    where newTop = i  $ expressionToList e
          newRest = Data.List.map (applyToExpressionsAndSubExpressions i) $ tail newTop

applyToAllInSignature : (List⁺ Expr -> List⁺ Expr) -> TypeSignature -> TypeSignature
applyToAllInSignature i (typeSignature funcName funcType) = typeSignature funcName $ applyToExpressionsAndSubExpressions i funcType

applyToAllExpressions : (List⁺ Expr -> List⁺ Expr) -> ParseTree -> ParseTree
applyToAllExpressions instructions (signature signature₁ range₁) =
  signature (applyToAllInSignature instructions signature₁) range₁
applyToAllExpressions instructions (functionDefinition definitionOf params body range₁) =
  functionDefinition definitionOf (tail newParams)
  (applyToExpressionsAndSubExpressions instructions body) range₁
    where newParams = instructions (ident definitionOf ∷ Data.List.map (applyToExpressionsAndSubExpressions instructions) params)

applyToAllExpressions instructions (dataStructure dataName parameters indexInfo constructors range₁ {c} ) =
  dataStructure
  dataName
  (Data.List.map (applyToAllInSignature instructions) parameters)
  (applyToExpressionsAndSubExpressions instructions indexInfo)
  (Data.List.map (applyToAllInSignature instructions) constructors)
  range₁ {c}
applyToAllExpressions instructions x = x

applyToProgram : (List⁺ Expr -> List⁺ Expr) -> Data.List.List ParseTree -> Data.List.List ParseTree
applyToProgram i c = Data.List.map (applyToAllExpressions i) c

makeFin : {n : ℕ} -> Vec Expr (n) -> ℕ -> ScopeState (Fin n)
makeFin {n} v number with number Data.Nat.Properties.<? n
makeFin {n} v number | yes p = return $ fromℕ≤ p
makeFin {n} v number | no ¬p = fail $ "Got a non-existing argument: " Data.String.++ Data.Nat.Show.show n Data.String.++ Data.Nat.Show.show (Data.List.length $ Data.Vec.toList v)

makeFin2 : {n : ℕ} -> Vec Expr (suc n) -> ℕ -> ScopeState (Fin n)
makeFin2 {n} v number with number Data.Nat.Properties.<? n
makeFin2 {n} v number | yes p = return $ fromℕ≤ p
makeFin2 {n} v number | no ¬p = fail $ "Got a non-existing argument: " Data.String.++ Data.Nat.Show.show n Data.String.++ Data.Nat.Show.show (Data.List.length $ Data.Vec.toList v)

--TODO: try to give this a better type
updateSignature :  ℕ -> List⁺ Expr ->
  (alterSignature : {n : ℕ} -> Vec Expr (suc n)  -> Fin n -> ScopeState (Vec Expr (suc n))) ->
  ScopeState (List⁺ Expr)
updateSignature argNo type f
  with toVec type
... | c = do
-- In a signature, we always have at least one item which is not an argument: the result type
  newFin <- makeFin2 c argNo
  newVec <- f c newFin
  return  $ Data.List.NonEmpty.fromVec newVec

doForArgument : List ParseTree -> ℕ -> ℕ ->
  (alterSignature : {n : ℕ} -> Vec Expr (suc n)  -> Fin n -> ScopeState (Vec Expr (suc n))) ->
  (alterExpression : TypeSignature -> ℕ -> ScopeState (List⁺ Expr -> List⁺ Expr)) ->
  ScopeState (List ParseTree)
doForArgument [] funcID whichArgument f1 f2 = fail "funcId not found in doForArgument"
doForArgument (signature (typeSignature (identifier name isInRange scope declaration) funcType) range₁ ∷ code) funcID whichArgument f1 f2 with Data.Nat.compare declaration funcID
doForArgument (signature (typeSignature (identifier name isInRange scope declaration {e}{b} {a}) funcType) range₁ ∷ code) .declaration whichArgument f1 f2 | equal .declaration = do
    newType <- updateSignature whichArgument (typeToList funcType) f1
    instruction <- f2 ((typeSignature (identifier name isInRange scope declaration {e}{b} {a})) funcType) whichArgument
    return $ applyToProgram instruction $
      signature (typeSignature
                  (identifier name isInRange scope declaration {e}{b} {a})
                  (listToType newType)) range₁ ∷ code
doForArgument (signature (typeSignature (identifier name isInRange scope declaration {e}{b} {a}) funcType) range₁ ∷ code) funcID whichArgument f1 f2 | _ = do
  newxs <- doForArgument code funcID whichArgument f1 f2
  return $ (signature (typeSignature (identifier name isInRange scope declaration {e}{b} {a}) funcType) range₁) ∷ newxs
doForArgument (x ∷ xs) funcID whichArgument f1 f2 = do
  newxs <- doForArgument xs funcID whichArgument f1 f2
  return $ x ∷ newxs

makeInstruction : TypeSignature -> ℕ -> (makeIns : {n : ℕ} -> Vec Expr n -> Fin n -> (List Expr -> List Expr)) -> ScopeState (List⁺ Expr -> List⁺ Expr)
makeInstruction (typeSignature funcName funcType) argNo f
  with toVec (typeToList funcType)
... | c = do
    newFin <- makeFin c argNo
    return $ function $ f c newFin
    where function : (List Expr -> List Expr) -> (List⁺ Expr -> List⁺ Expr)
          function f (ident identifier₁ ∷ tail₁)
              with sameId identifier₁ funcName
          function f (ident identifier₁ ∷ tail₁) | false =
            (ident identifier₁ ∷ tail₁)
          function f (ident identifier₁ ∷ tail₁) | true =
              ident identifier₁ ∷ f tail₁
          function f list = list


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

module Categories.Adjoint.Instance.Core where

-- The adjunction between the forgetful functor from Cats to Groupoids
-- and the Core functor.

open import Level using (_⊔_)
import Function

open import Categories.Adjoint using (_⊣_)
open import Categories.Category using (Category)
import Categories.Category.Construction.Core as C
open import Categories.Category.Groupoid using (Groupoid)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Instance.Groupoids using (Groupoids)
open import Categories.Functor using (Functor; _∘F_; id)
open import Categories.Functor.Instance.Core using (Core)
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MR
open import Categories.Morphism.IsoEquiv using (⌞_⌟)
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (refl; _≃_)

-- The forgetful functor from Groupoids to Cats

Forgetful : ∀ {o ℓ e} → Functor (Groupoids o ℓ e) (Cats o ℓ e)
Forgetful = record
  { F₀ = category
  ; F₁ = Function.id
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = Function.id
  }
  where open Groupoid

-- Core is right-adjoint to the forgetful functor from Groupoids to
-- Cats

CoreAdj : ∀ {o ℓ e} → Forgetful {o} {ℓ ⊔ e} {e} ⊣ Core
CoreAdj = record
  { unit   = ntHelper record { η = unit   ; commute = λ {G} {H} F → unit-commute {G} {H} F }
  ; counit = ntHelper record { η = counit ; commute = counit-commute }
  ; zig    = λ {G} → zig {G}
  ; zag    = zag
  }
  where
    open Groupoid using (category)
    module Core = Functor Core

    unit : ∀ G → Functor (category G) (C.Core (category G))
    unit G = record
      { F₀ = Function.id
      ; F₁ = λ f → record { from = f ; to = f ⁻¹ ; iso = iso }
      ; identity     = ⌞ Equiv.refl ⌟
      ; homomorphism = ⌞ Equiv.refl ⌟
      ; F-resp-≈     = λ eq → ⌞ eq ⌟
      }
      where open Groupoid G

    unit-commute : ∀ {G H} (F : Functor (category G) (category H)) →
                   unit H ∘F F ≃ Core.F₁ F ∘F unit G
    unit-commute {G} {H} F = record
      { F⇒G = record { η = λ _ → ≅.refl ; commute = λ _ → ⌞ MR.id-comm-sym (category H) ⌟ ; sym-commute = λ _ → ⌞ MR.id-comm (category H) ⌟ }
      ; F⇐G = record { η = λ _ → ≅.refl ; commute = λ _ → ⌞ MR.id-comm-sym (category H) ⌟ ; sym-commute = λ _ → ⌞ MR.id-comm (category H) ⌟  }
      ; iso = λ _ → record { isoˡ = ⌞ identityˡ ⌟ ; isoʳ = ⌞ identityˡ ⌟ }
      }
      where
        open Category (category H)
        open Morphism (category H)

    counit : ∀ C → Functor (C.Core C) C
    counit C = record
      { F₀ = Function.id
      ; F₁ = _≅_.from
      ; identity     = Equiv.refl
      ; homomorphism = Equiv.refl
      ; F-resp-≈     = λ where ⌞ eq ⌟ → eq
      }
      where
        open Category C
        open Morphism C

    counit-commute : ∀ {C D} (F : Functor C D) →
                     counit D ∘F Core.F₁ F ≃ F ∘F counit C
    counit-commute {C} {D} F = record
      { F⇒G = record { η = λ _ → D.id ; commute = λ _ → MR.id-comm-sym D ; sym-commute = λ _ → MR.id-comm D }
      ; F⇐G = record { η = λ _ → D.id ; commute = λ _ → MR.id-comm-sym D ; sym-commute = λ _ → MR.id-comm D }
      ; iso = λ _ → _≅_.iso ≅.refl
      }
      where
        module D = Category D
        open Morphism D

    zig : ∀ {G} → counit (category G) ∘F unit G ≃ id
    zig {G} = record
      { F⇒G = record { η = λ _ → G.id ; commute = λ _ → MR.id-comm-sym (category G) ; sym-commute = λ _ → MR.id-comm (category G) }
      ; F⇐G = record { η = λ _ → G.id ; commute = λ _ → MR.id-comm-sym (category G) ; sym-commute = λ _ → MR.id-comm (category G) }
      ; iso = λ _ → _≅_.iso ≅.refl
      }
      where
        module G = Groupoid G
        open Morphism G.category

    zag : ∀ {B} → Core.F₁ (counit B) ∘F unit (Core.F₀ B) ≃ id
    zag {B} = record
      { F⇒G = record { η = λ _ → ≅.refl ; commute = λ _ → ⌞ MR.id-comm-sym B ⌟ ; sym-commute = λ _ → ⌞ MR.id-comm B ⌟ }
      ; F⇐G = record { η = λ _ → ≅.refl ; commute = λ _ → ⌞ MR.id-comm-sym B ⌟ ; sym-commute = λ _ → ⌞ MR.id-comm B ⌟ }
      ; iso = λ _ → record { isoˡ = ⌞ identityˡ ⌟ ; isoʳ = ⌞ identityˡ ⌟ }
      }
      where
        open Category B
        open Morphism B

ext: agda

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --without-K #-}
module Fiber where

open import Equivalence
open import NTypes.Contractible
open import PathOperations
open import Types

fib : ∀ {a b} {A : Set a} {B : Set b}
  (f : A → B) (y : B) →
  Set _
fib {A = A} f y = Σ A λ x → f x ≡ y

fib→dom : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) →
  Σ B (fib f) → A
fib→dom f (b , a , p) = a

dom→fib : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) →
  A → Σ B (fib f)
dom→fib f a = f a , a , refl

fib-dom-eq :  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) →
  Σ B (fib f) ≃ A
fib-dom-eq {A = A} {B = B} f
  = fib→dom f
  , (dom→fib f , λ _ → refl)
  , (dom→fib f , λ {(b , a , p) →
      ap (swap ∘ _,_ a) (π₂ (pp-space-contr (f a)) (b , p))})
  where
  swap : (Σ A λ x → Σ B λ y → f x ≡ y) → Σ B (fib f)
  swap (b , a , p) = a , b , p

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monoidal.Braided.Helpers where

open import Categories.Monoidal.Helpers

open import Data.Nat using (_+_)
open import Function using (flip)

open import Categories.Category
import Categories.Functor

open import Categories.Bifunctor hiding (identityˡ; identityʳ; assoc) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation using (_∘₀_; _∘₁_; _∘ˡ_; _∘ʳ_; NaturalTransformation) renaming (_≡_ to _≡ⁿ_; id to idⁿ)

module BraidedHelperFunctors {o ℓ e} (C : Category o ℓ e) (—⊗— : Bifunctor C C C) (id : Category.Obj C) where
  open MonoidalHelperFunctors C —⊗— id

  private module C = Category C
  open C hiding (id; identityˡ; identityʳ)

  import Categories.Power.NaturalTransformation
  private module PowNat = Categories.Power.NaturalTransformation C
  open PowNat

  private module ⊗ = Functor —⊗— renaming (F₀ to ⊗₀; F₁ to ⊗₁; F-resp-≡ to ⊗-resp-≡)
  open ⊗

  module Braiding (identityˡ : NaturalIsomorphism id⊗x x)
                  (identityʳ : NaturalIsomorphism x⊗id x)
                  (assoc : NaturalIsomorphism [x⊗y]⊗z x⊗[y⊗z])
                  (braid : NaturalIsomorphism x⊗y y⊗x) where
    open NaturalIsomorphism identityˡ using () renaming (F⇒G to υˡ)
    open NaturalIsomorphism identityʳ using () renaming (F⇒G to υʳ)
    open NaturalIsomorphism assoc using () renaming (F⇒G to α; F⇐G to α₂)
    open NaturalIsomorphism braid using () renaming (F⇒G to B)

    α-over : ∀ {n} (F₁ F₂ F₃ : Powerendo n) → NaturalTransformation ((F₁ ⊗₂ F₂) ⊗₂ F₃) (overlap2ʳ —⊗— F₁ F₂ F₃)
    α-over F₁ F₂ F₃ = α ∘ʳ plex {3} F₁ F₂ F₃ -- ((hyp F₁ ∥ hyp F₂) ∥ hyp F₃)

    α₂-over : ∀ {n} (F₁ F₂ F₃ : Powerendo n) → NaturalTransformation (overlap2ʳ —⊗— F₁ F₂ F₃) ((F₁ ⊗₂ F₂) ⊗₂ F₃)
    α₂-over F₁ F₂ F₃ = α₂ ∘ʳ plex {3} F₁ F₂ F₃

    B-over : ∀ {n} (F₁ F₂ : Powerendo n) → NaturalTransformation (F₁ ⊗₂ F₂) (F₂ ⊗₂ F₁)
    B-over F₁ F₂ = B ∘ʳ plex {2} F₁ F₂

    BTriangleTop   : NaturalTransformation id⊗x x⊗id
    BTriangleTop   = B-over (widenˡ 1 id↑) x

    BTriangleLeft  : NaturalTransformation id⊗x x
    BTriangleLeft  = υˡ

    BTriangleRight : NaturalTransformation x⊗id x
    BTriangleRight = υʳ

    Hexagon1TopA    : NaturalTransformation [x⊗y]⊗z x⊗[y⊗z]
    Hexagon1TopA    = α-over (select 0) (select 1) (select 2)
    Hexagon1TopB    : NaturalTransformation x⊗[y⊗z] [y⊗z]⊗x
    Hexagon1TopB    = B-over (select 0) (select 1 ⊗₂ select 2)
    Hexagon1SideB   : NaturalTransformation [y⊗z]⊗x y⊗[z⊗x]
    Hexagon1SideB   = α-over (select 1) (select 2) (select 0)

    Hexagon1SideA   : NaturalTransformation [x⊗y]⊗z [y⊗x]⊗z
    Hexagon1SideA   = B-over (select 0) (select 1) ⊗ⁿ′ id3 {select 2}
    Hexagon1BottomA : NaturalTransformation [y⊗x]⊗z y⊗[x⊗z]
    Hexagon1BottomA = α-over (select 1) (select 0) (select 2)
    Hexagon1BottomB : NaturalTransformation y⊗[x⊗z] y⊗[z⊗x]
    Hexagon1BottomB = id3 {select 1} ⊗ⁿ′ B-over (select 0) (select 2)

    Hexagon2TopA    : NaturalTransformation x⊗[y⊗z] [x⊗y]⊗z
    Hexagon2TopA    = α₂-over (select 0) (select 1) (select 2)
    Hexagon2TopB    : NaturalTransformation [x⊗y]⊗z z⊗[x⊗y]
    Hexagon2TopB    = B-over (select 0 ⊗₂ select 1) (select 2)
    Hexagon2SideB   : NaturalTransformation z⊗[x⊗y] [z⊗x]⊗y
    Hexagon2SideB   = α₂-over (select 2) (select 0) (select 1)

    Hexagon2SideA   : NaturalTransformation x⊗[y⊗z] x⊗[z⊗y]
    Hexagon2SideA   = id3 {select 0} ⊗ⁿ′ B-over (select 1) (select 2)
    Hexagon2BottomA : NaturalTransformation x⊗[z⊗y] [x⊗z]⊗y
    Hexagon2BottomA = α₂-over (select 0) (select 2) (select 1)
    Hexagon2BottomB : NaturalTransformation [x⊗z]⊗y [z⊗x]⊗y
    Hexagon2BottomB = B-over (select 0) (select 2) ⊗ⁿ′ id3 {select 1}

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Data.ListNonEmpty where

open import Data.Boolean
import      Data.IndexedList
open import Functional
import      Lvl
open import Numeral.Natural
open import Type

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

module _ (T : Type{ℓ}) where
  open Data.IndexedList(T){Bool} using (IndexedList ; intro)

  -- A non-empty list.
  List₊ : Type{ℓ}
  List₊ = IndexedList(intro 𝐹 (const(const 𝑇)))(𝑇)

module _ {T : Type{ℓ}} where
  open Data.IndexedList(T){Bool} using (∅ ; _⊰_ ; singleton) public

pattern ‥ = _ ⊰ _

open import Data.List
import      Data.List.Functions as List

-- A list from a non-empty list.
list : List₊(T) → List(T)
list (singleton(x)) = List.singleton(x)
list (x ⊰ l@‥)      = x List.⊰ list(l)

-- A list without its first element.
tail₀ : List₊(T) → List(T)
tail₀ (singleton(_)) = List.∅
tail₀ (_ ⊰ l@‥)      = list(l)

-- List concatenation.
_++_ : List₊(T) → List₊(T) → List₊(T)
singleton(x) ++ y = x ⊰ y
(x ⊰ xl@‥)   ++ y = x ⊰ (xl ++ y)

-- The first element of the list.
head : List₊(T) → T
head(singleton x)   = x
head(x ⊰ l@‥) = x

-- Applies a binary operator to each element in the list starting with the initial element.
-- Example:
--   reduceᵣ(_▫_) [a]         = a
--   reduceᵣ(_▫_) [a,b]       = a ▫ b
--   reduceᵣ(_▫_) [a,b,c]     = a ▫ (b ▫ c)
--   reduceᵣ(_▫_) [a,b,c,d,e] = a ▫ (b ▫ (c ▫ (d ▫ e)))
reduceᵣ : (T → T → T) → List₊(T) → T
reduceᵣ(_)   (singleton(x)) = x
reduceᵣ(_▫_) (x ⊰ l@‥)      = x ▫ (reduceᵣ(_▫_) l)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category
open import Categories.Support.Equivalence

module Categories.Morphism.Indexed {o ℓ e c q} (C : Category o ℓ e) (B : Setoid c q) where

open import Level using (_⊔_)
open import Data.Product as P using (_,_; _×_)
open import Function as F using () renaming (_∘_ to _⋆_; _∘′_ to _⋆′_)
open import Relation.Binary as B using ()
open import Relation.Binary.HeterogeneousEquality as HE using (_≅_)

open import Categories.Support.PropositionalEquality
open import Categories.Support.SetoidFunctions as SF using (_⟶_; ⟪_,_⟫′)
open import Categories.Support.SetoidPi as SΠ public using (Π; IndexedSetoid) renaming (_⟨$⟩_ to _‼_; cong to cong₁)

import Categories.Object.Indexed as IxOb
open IxOb C B
open Category C
open Heterogeneous C

open Setoid B using () renaming (Carrier to Bc; _≈_ to _≈B_)

open Setoid using () renaming (_≈_ to _[_≈_])

ihom-setoid : {S : Set o} → (S → (Obj × Obj)) → (B ⟶ (set→setoid S)) → IndexedSetoid Bc _≈B_ _ _
ihom-setoid {S} F Xs = record
      -- ok, this is massively ugly, but it gets around some weird problems introduced in 2.5.1.1 (JC)
  { Carrier = λ i → (P.proj₁ (F (_⟶_._⟨$⟩_ Xs i)) ⇒ P.proj₂ (F (_⟶_._⟨$⟩_ Xs i)))
  ; _≈_ = λ f g → f ∼ g
  ; isEquivalence = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  ; resp = λ {i} {j} i≈j → SΠ.resp-per′ (at′ i) (at′ j) (resp₁ i≈j) (resp₂ i≈j)
  }
  where

  -- fake 'at' for resp
  at′ : Bc → Setoid _ _
  at′ i = record
    { Carrier = (P.proj₁ (F (_⟶_._⟨$⟩_ Xs i)) ⇒ P.proj₂ (F (_⟶_._⟨$⟩_ Xs i)))
    ; _≈_ = λ f g → f ∼ g
    ; isEquivalence = record { refl = refl; sym = sym; trans = trans }
    }

  at-≈ : (X : S) → B.Rel ((P.uncurry _⇒_ ⋆′ F) X) (ℓ ⊔ e)
  at-≈ X = λ f g → f ∼ g

  .resp₁ : ∀ {i j} → (i ≈B j) → (P.proj₁ (F (_⟶_._⟨$⟩_ Xs i)) ⇒ P.proj₂ (F (_⟶_._⟨$⟩_ Xs i))) ≣ (P.proj₁ (F (_⟶_._⟨$⟩_ Xs j)) ⇒ P.proj₂ (F (_⟶_._⟨$⟩_ Xs j)))
  resp₁ i≈j = ≣-cong (P.uncurry _⇒_ ⋆′ F) (cong₀ Xs i≈j)

  .resp₂ : ∀ {i j} → (i ≈B j) → Setoid._≈_ (at′ i) ≅ Setoid._≈_ (at′ j)
  resp₂ i≈j = HE.cong at-≈ (HE.≡-to-≅ (cong₀ Xs i≈j))

Fan : Obj → Dust → Set _
Fan X Ys = Π B (ihom-setoid (λ Y → X , Y) Ys)

fan-setoid : Obj → Dust → Setoid _ _
fan-setoid X Ys = SΠ.setoid B (ihom-setoid (λ Y → X , Y) Ys)

_⇒∗_ = Fan
_⇨∗_ = fan-setoid

Plume : Dust → Obj → Set _
Plume Xs Y = Π B (ihom-setoid (λ X → X , Y) Xs)

plume-setoid : Dust → Obj → Setoid _ _
plume-setoid Xs Y = SΠ.setoid B (ihom-setoid (λ X → X , Y) Xs)

_∗⇒_ = Plume
_∗⇨_ = plume-setoid

Dance : Dust → Dust → Set _
Dance Xs Ys = Π B (ihom-setoid F.id ⟪ Xs , Ys ⟫′)

dance-setoid : Dust → Dust → Setoid _ _
dance-setoid Xs Ys = SΠ.setoid B (ihom-setoid F.id ⟪ Xs , Ys ⟫′)

_∗⇒∗_ = Dance
_∗⇨∗_ = dance-setoid

_◃_ : ∀ {Xs Y Z} (f : Y ⇒ Z) (g : Xs ∗⇒ Y) → Xs ∗⇒ Z
f ◃ g = record { _⟨$⟩_ = λ x → f ∘ (g ‼ x)
               ; cong = λ x≈y → ∘-resp-∼ʳ (cong₁ g x≈y) }

_▹_ : ∀ {X Y Zs} (f : Y ⇒∗ Zs) (g : X ⇒ Y) → X ⇒∗ Zs
f ▹ g = record { _⟨$⟩_ = λ x → (f ‼ x) ∘ g
               ; cong = λ x≈y → ∘-resp-∼ˡ (cong₁ f x≈y) }

_⋊_ : ∀ {Xs Ys Z} (f : Ys ∗⇒ Z) (g : Xs ∗⇒∗ Ys) → Xs ∗⇒ Z
f ⋊ g = record { _⟨$⟩_ = λ x → (f ‼ x) ∘ (g ‼ x)
               ; cong = λ x≈y → ∘-resp-∼ (cong₁ f x≈y) (cong₁ g x≈y) }

_⋉_ : ∀ {X Ys Zs} (f : Ys ∗⇒∗ Zs) (g : X ⇒∗ Ys) → X ⇒∗ Zs
f ⋉ g = record { _⟨$⟩_ = λ x → (f ‼ x) ∘ (g ‼ x)
               ; cong = λ x≈y → ∘-resp-∼ (cong₁ f x≈y) (cong₁ g x≈y) }

_⋈_ : ∀ {Xs Y Zs} (f : Y ⇒∗ Zs) (g : Xs ∗⇒ Y) → Xs ∗⇒∗ Zs
f ⋈ g = record { _⟨$⟩_ = λ x → (f ‼ x) ∘ (g ‼ x)
               ; cong = λ x≈y → ∘-resp-∼ (cong₁ f x≈y) (cong₁ g x≈y) }

_◽_ : ∀ {Xs Ys Zs} (f : Ys ∗⇒∗ Zs) (g : Xs ∗⇒∗ Ys) → Xs ∗⇒∗ Zs
f ◽ g = record { _⟨$⟩_ = λ x → (f ‼ x) ∘ (g ‼ x)
               ; cong = λ x≈y → ∘-resp-∼ (cong₁ f x≈y) (cong₁ g x≈y) }

.assoc-◽⋉ : ∀ {X Ys Zs Ws} {f : Zs ∗⇒∗ Ws} {g : Ys ∗⇒∗ Zs} {h : X ⇒∗ Ys}
          → (X ⇨∗ Ws) [ _⋉_ {Ys = Ys} {Ws} (_◽_ {Ys} {Zs} {Ws} f g) h ≈ _⋉_ {Ys = Zs} {Ws} f (_⋉_ {Ys = Ys} {Zs} g h) ]
assoc-◽⋉ {Ys = Ys} {Zs} {Ws} {f = f} {g} {h} {i} {j} i≈j with Ys _⟶_.⟨$⟩ j | cong₀ Ys i≈j | Zs _⟶_.⟨$⟩ j | cong₀ Zs i≈j | Ws _⟶_.⟨$⟩ j | cong₀ Ws i≈j | f ‼ j | cong₁ f i≈j | g ‼ j | cong₁ g i≈j | h ‼ j | cong₁ h i≈j
assoc-◽⋉ {f = f} {g} {h} {i} i≈j | ._ | ≣-refl | ._ | ≣-refl | ._ | ≣-refl | fj | ≡⇒∼ fi≡fj | gj | ≡⇒∼ gi≡gj | hj | ≡⇒∼ hi≡hj =
  ≡⇒∼ (begin
    ((f ‼ i) ∘ (g ‼ i)) ∘ (h ‼ i)
  ↓⟨ ∘-resp-≡ (∘-resp-≡ fi≡fj gi≡gj) hi≡hj ⟩
    (fj ∘ gj) ∘ hj
  ↓⟨ assoc ⟩
    fj ∘ (gj ∘ hj)
  ∎)
  where
  open Heterogeneous C hiding (≡⇒∼)
  open HomReasoning


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

-- Counterpoint Exercises

module Exercises where

open import MidiEvent
open import Note
open import Pitch

open import Data.Fin
open import Data.List
open import Data.Nat

-- Exercise 5.4

cantusFirmus : List Pitch
cantusFirmus = a 4 ∷ c 5 ∷ b 4 ∷ c 5 ∷ d 5 ∷ e 5 ∷ c 5 ∷ b 4 ∷ a 4 ∷ []

cfNotes : List Note
cfNotes = Data.List.map (λ p → tone whole p) cantusFirmus

----

instrument : InstrumentNumber-1
instrument = # 0 -- piano

channel : Channel-1
channel = # 0

tempo : ℕ
tempo = 120

cfTrack : List MidiTrack
cfTrack = track "Piano" instrument channel tempo (notes→events defaultVelocity cfNotes) ∷ []

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module examplesPaperJFP.SpaceShipSimpleVar where

open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent

open import Data.Bool.Base
open import Data.List.Base
open import Data.Integer

open import Data.Product hiding (map)
open import SizedIO.Object
open import SizedIO.IOObject

open import NativeIO

open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.VariableList

open import StateSizedIO.GUI.WxGraphicsLib

open import StateSized.GUI.BitMaps

VarType = ℤ

varInit : VarType
varInit = (+ 150)

onPaint : ∀{i} → VarType → DC → Rect → IO GuiLev1Interface i VarType
onPaint z dc rect      =  exec (drawBitmap dc ship (z , (+ 150)) true) λ _ →
                          return z

moveSpaceShip  : ∀{i} → Frame → VarType → IO GuiLev1Interface i VarType
moveSpaceShip  fra z   =  return (z + (+ 20))

callRepaint    : ∀{i} → Frame → VarType → IO GuiLev1Interface i VarType
callRepaint    fra z   =  exec (repaint fra) λ _ → return z

buttonHandler : ∀{i} → Frame → List (VarType  → IO GuiLev1Interface i VarType)
buttonHandler fra = moveSpaceShip fra ∷ [ callRepaint fra ]

program : ∀{i} → IOˢ GuiLev2Interface i (λ _ → Unit) []
program =  execˢ (level1C makeFrame)           λ fra →
           execˢ (level1C (makeButton fra))    λ bt →
           execˢ (level1C (addButton fra bt))  λ _ →
           execˢ (createVar varInit)           λ _ →
           execˢ (setButtonHandler bt (moveSpaceShip fra
                                     ∷ [ callRepaint fra ])) λ _ →
           execˢ (setOnPaint       fra [ onPaint  ])
           returnˢ

main : NativeIO Unit
main = start (translateLev2 program)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- {-# OPTIONS --no-coverage #-}
-- {-# OPTIONS -v tc.cover:20 #-}

open import Common.Bool
open import Common.Equality

_∨_ : Bool → Bool → Bool
a ∨ b = if a then true else b

module Works where
  data Term : Bool → Set where
    I   : Term false
    App : ∀ a b c → a ∨ b ≡ c → Term a → Term b → Term c

  -- The following clause works for the coverage checker:

  test : Term false → Set
  test (App false false .false refl I x) = Bool

module Fails where

  data Term : Bool -> Set where
    I   : Term false
    App : ∀ a b c → Term a → Term b → a ∨ b ≡ c → Term c

  -- If we put the equality proof later in App, it fails:

  test : Term false → Set
  test (App false false .false I x refl) = Bool
  -- The following checks, until you split at p.
  -- test (App false false .false I x p) = {!p!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Algebra

module Data.FingerTree.View
  {r m}
  (ℳ : Monoid r m)
  where

open import Level using (_⊔_)
open import Data.Product
open import Function

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

open import Data.FingerTree.Structures ℳ
open import Data.FingerTree.Reasoning ℳ
open import Data.FingerTree.Measures ℳ
open import Data.FingerTree.Cons ℳ
open σ ⦃ ... ⦄
{-# DISPLAY σ.μ _ = μ #-}
{-# DISPLAY μ-tree _ x = μ x #-}
{-# DISPLAY μ-deep _ x = μ x #-}

open Monoid ℳ renaming (Carrier to 𝓡)

infixr 5 _◃_
data Viewₗ {a b} (A : Set a) (Σ : Set b) : Set (a ⊔ b) where
  nilₗ : Viewₗ A Σ
  _◃_ : A → Σ → Viewₗ A Σ

instance
  σ-Viewₗ : ∀ {a b} {A : Set a} {Σ : Set b} ⦃ _ : σ A ⦄ ⦃ _ : σ Σ ⦄ → σ (Viewₗ A Σ)
  μ ⦃ σ-Viewₗ ⦄ nilₗ = ε
  μ ⦃ σ-Viewₗ ⦄ (x ◃ xs) = μ x ∙ μ xs

viewₗ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (xs : Tree Σ) → μ⟨ Viewₗ Σ (Tree Σ) ⟩≈ (μ xs)
viewₗ empty = nilₗ ⇑
viewₗ (single x) = (x ◃ empty) ⇑[ ℳ ↯ ]
viewₗ (deep (𝓂 ↤ (D₂ a b     & m & rs) ⇑[ 𝓂≈ ])) = a ◃ deep ⟪ D₁ b     & m & rs ⇓⟫ ⇑[ ℳ ↯ ] ≈[ 𝓂≈ ]′
viewₗ (deep (𝓂 ↤ (D₃ a b c   & m & rs) ⇑[ 𝓂≈ ])) = a ◃ deep ⟪ D₂ b c   & m & rs ⇓⟫ ⇑[ ℳ ↯ ] ≈[ 𝓂≈ ]′
viewₗ (deep (𝓂 ↤ (D₄ a b c d & m & rs) ⇑[ 𝓂≈ ])) = a ◃ deep ⟪ D₃ b c d & m & rs ⇓⟫ ⇑[ ℳ ↯ ] ≈[ 𝓂≈ ]′
viewₗ (deep (𝓂 ↤ (D₁ a & m & rs) ⇑[ 𝓂≈ ])) with viewₗ m
... | (μ⟨y⟩ ↤ N₂ y₁ y₂    ⇑[ yp ]) ◃ ys ⇑[ p ] = a ◃ deep (μ m ∙ μ rs ↤ D₂ y₁ y₂    & ys & rs ⇑[ ℳ ↯ ] ≈[ ≪∙ (≪∙ yp ⍮ p) ]′) ⇑[ 𝓂≈ ]
... | (μ⟨y⟩ ↤ N₃ y₁ y₂ y₃ ⇑[ yp ]) ◃ ys ⇑[ p ] = a ◃ deep (μ m ∙ μ rs ↤ D₃ y₁ y₂ y₃ & ys & rs ⇑[ ℳ ↯ ] ≈[ ≪∙ (≪∙ yp ⍮ p) ]′) ⇑[ 𝓂≈ ]
... | nilₗ ⇑[ p ] = (digitToTree rs [ _ ∙> r ⟿ r ] >>= (λ rs′ → (a ◃ rs′) ⇑)) ≈[ ∙≫ sym (identityˡ _) ⍮ (∙≫ ≪∙ p) ⍮ 𝓂≈ ]

infixl 5 _▹_
data Viewᵣ {a b} (A : Set a) (Σ : Set b) : Set (a ⊔ b) where
  nilᵣ : Viewᵣ A Σ
  _▹_ : Σ → A → Viewᵣ A Σ

instance
  σ-Viewᵣ : ∀ {a b} {A : Set a} {Σ : Set b} ⦃ _ : σ A ⦄ ⦃ _ : σ Σ ⦄ → σ (Viewᵣ A Σ)
  μ ⦃ σ-Viewᵣ ⦄ nilᵣ = ε
  μ ⦃ σ-Viewᵣ ⦄ (xs ▹ x) = μ xs ∙ μ x

viewᵣ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (xs : Tree Σ) → μ⟨ Viewᵣ Σ (Tree Σ) ⟩≈ (μ xs)
viewᵣ empty = nilᵣ ⇑
viewᵣ (single x) = empty ▹ x ⇑[ ℳ ↯ ]
viewᵣ (deep (𝓂 ↤ (ls & m & D₂ a b    ) ⇑[ 𝓂≈ ])) = (deep ⟪ ls & m & D₁ a     ⇓⟫ ▹ b) ⇑[ ℳ ↯ ] ≈[ 𝓂≈ ]′
viewᵣ (deep (𝓂 ↤ (ls & m & D₃ a b c  ) ⇑[ 𝓂≈ ])) = (deep ⟪ ls & m & D₂ a b   ⇓⟫ ▹ c) ⇑[ ℳ ↯ ] ≈[ 𝓂≈ ]′
viewᵣ (deep (𝓂 ↤ (ls & m & D₄ a b c d) ⇑[ 𝓂≈ ])) = (deep ⟪ ls & m & D₃ a b c ⇓⟫ ▹ d) ⇑[ ℳ ↯ ] ≈[ 𝓂≈ ]′
viewᵣ (deep (𝓂 ↤ (ls & m & D₁ a) ⇑[ 𝓂≈ ])) with viewᵣ m
... | ys ▹ (μ⟨y⟩ ↤ N₂ y₁ y₂    ⇑[ yp ]) ⇑[ p ] = deep (μ ls ∙ μ m ↤ ls & ys & D₂ y₁ y₂    ⇑[ ℳ ↯ ] ≈[ ∙≫ (∙≫ yp ⍮ p) ]′) ▹ a ⇑[ ℳ ↯ ] ≈[ 𝓂≈ ]′
... | ys ▹ (μ⟨y⟩ ↤ N₃ y₁ y₂ y₃ ⇑[ yp ]) ⇑[ p ] = deep (μ ls ∙ μ m ↤ ls & ys & D₃ y₁ y₂ y₃ ⇑[ ℳ ↯ ] ≈[ ∙≫ (∙≫ yp ⍮ p) ]′) ▹ a ⇑[ ℳ ↯ ] ≈[ 𝓂≈ ]′
... | nilᵣ ⇑[ p ] = (digitToTree ls [ l <∙ _ ⟿ l ] >>= (λ ls′ → (ls′ ▹ a) ⇑)) ≈[ ℳ ↯ ↣ μ ls ∙ (ε ∙ μ a) ] ≈[ ∙≫ ≪∙ p ⍮ 𝓂≈ ]′

deepₗ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (l : List Σ) → (m : Tree ⟪ Node Σ ⟫) → (r : Digit Σ) → μ⟨ Tree Σ ⟩≈ (μ l ∙ (μ m ∙ μ r))
deepₗ [] m r with viewₗ m
deepₗ [] m r | nilₗ ⇑[ n≈ ] = digitToTree r ≈[ ℳ ↯ ↣ ε ∙ (ε ∙ μ r) ] ≈[ ∙≫ ≪∙ n≈ ]′
deepₗ [] m r | ((μ⟨y⟩ ↤ N₂ y₁ y₂    ⇑[ yp ]) ◃ ys) ⇑[ ys≈ ] = deep (μ m ∙ μ r ↤ D₂ y₁ y₂    & ys & r ⇑[ ≪∙ yp ⍮ sym (assoc _ _ _) ⍮ ≪∙ ys≈ ]) ⇑[ ℳ ↯ ]
deepₗ [] m r | ((μ⟨y⟩ ↤ N₃ y₁ y₂ y₃ ⇑[ yp ]) ◃ ys) ⇑[ ys≈ ] = deep (μ m ∙ μ r ↤ D₃ y₁ y₂ y₃ & ys & r ⇑[ ≪∙ yp ⍮ sym (assoc _ _ _) ⍮ ≪∙ ys≈ ]) ⇑[ ℳ ↯ ]
deepₗ (l ∷ ls) m r = go l ls m r
  where
  go : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (l : Σ) → (ls : List Σ) → (m : Tree ⟪ Node Σ ⟫) → (r : Digit Σ) → μ⟨ Tree Σ ⟩≈ (μ l ∙ μ ls ∙ (μ m ∙ μ r))
  go l [] m r = deep ⟪ D₁ l & m & r ⇓⟫ ⇑[ ℳ ↯ ]
  go l₁ (l₂ ∷ ls) m r = (go l₂ ls m r [ _ ∙> ls′ ⟿ ls′ ] >>= (l₁ ◂_)) ≈[ ℳ ↯ ]

deepᵣ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (l : Digit Σ) → (m : Tree ⟪ Node Σ ⟫) → (r : List Σ) → μ⟨ Tree Σ ⟩≈ (μ l ∙ (μ m ∙ μ r))
deepᵣ l m [] with viewᵣ m
deepᵣ l m [] | nilᵣ ⇑[ p ] = digitToTree l ≈[ sym (identityʳ _) ⍮ ∙≫ (p ⍮ sym (identityʳ _)) ]
deepᵣ l m [] | (ys ▹ (μ⟨y⟩ ↤ N₂ y₁ y₂    ⇑[ μ⟨y⟩≈ ])) ⇑[ p ] = deep (μ l ∙ μ m ↤ l & ys & D₂ y₁ y₂    ⇑[ ∙≫ (∙≫ μ⟨y⟩≈ ⍮ p) ]) ⇑[ ℳ ↯ ]
deepᵣ l m [] | (ys ▹ (μ⟨y⟩ ↤ N₃ y₁ y₂ y₃ ⇑[ μ⟨y⟩≈ ])) ⇑[ p ] = deep (μ l ∙ μ m ↤ l & ys & D₃ y₁ y₂ y₃ ⇑[ ∙≫ (∙≫ μ⟨y⟩≈ ⍮ p) ]) ⇑[ ℳ ↯ ]
deepᵣ l m (r ∷ rs) = go  (deep ⟪ l & m & D₁ r ⇓⟫ ⇑) rs ≈[ ℳ ↯ ]
  where
  go : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → ∀ {xs} → μ⟨ Tree Σ ⟩≈ xs → (rs : List Σ) → μ⟨ Tree Σ ⟩≈ (xs ∙ μ rs)
  go xs [] = xs ≈[ sym (identityʳ _) ]
  go xs (r ∷ rs) = go (xs [ sz <∙ _ ⟿ sz ] >>= (_▸ r)) rs ≈[ ℳ ↯ ]

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
module Logic.Predicate.Multi where

open import Data.Tuple.RaiseTypeᵣ
open import Function.Multi
open import Function.Multi.Functions
open import Numeral.Natural
open import Logic.Predicate
open import Logic

-- Universal quantification of multiple variables.
-- Example:
--   ∀₊(3) P = ∀{x}{y}{z} → P(x)(y)(z)
∀₊ : (n : ℕ) → ∀{ℓ}{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (As ⇉ Stmt{ℓ}) → Stmt
∀₊(n) = quantifier₊(n) ∀ₗ

-- Existential quantification of multiple variables.
-- Example:
--   ∃₊(3) P = ∃(x ↦ ∃(y ↦ ∃(z ↦ P(x)(y)(z))))
∃₊ : (n : ℕ) → ∀{ℓ}{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (As ⇉ Stmt{ℓ}) → Stmt
∃₊(n) = quantifier₊(n) ∃


text:
{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Cubical.Glue where

open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
                                             primHComp to hcomp; primTransp to transp; primComp to comp;
                                             itIsOne to 1=1)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to ouc)
import Agda.Builtin.Cubical.HCompU as HCompU

module Helpers = HCompU.Helpers

open Helpers

-- We make this a record so that isEquiv can be proved using
-- copatterns. This is good because copatterns don't get unfolded
-- unless a projection is applied so it should be more efficient.
record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
  no-eta-equality
  field
    equiv-proof : (y : B) → isContr (fiber f y)

open isEquiv public

infix 4 _≃_

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) \ f → (isEquiv f)

equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B
equivFun e = fst e

-- Improved version of equivProof compared to Lemma 5 in CCHM. We put
-- the (φ = i0) face in contr' making it be definitionally c in this
-- case. This makes the computational behavior better, in particular
-- for transp in Glue.
equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A)
           → ∀ ψ → (Partial ψ (fiber (w .fst) a)) → fiber (w .fst) a
equivProof A B w a ψ fb = contr' {A = fiber (w .fst) a} (w .snd .equiv-proof a) ψ fb
  where
    contr' : ∀ {ℓ} {A : Set ℓ} → isContr A → (φ : I) → (u : Partial φ A) → A
    contr' {A = A} (c , p) φ u = hcomp (λ i → λ { (φ = i1) → p (u 1=1) i
                                                ; (φ = i0) → c }) c

{-# BUILTIN EQUIV      _≃_        #-}
{-# BUILTIN EQUIVFUN   equivFun   #-}
{-# BUILTIN EQUIVPROOF equivProof #-}

primitive
    primGlue    : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
      → (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
      → Set ℓ'
    prim^glue   : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
      → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
      → (t : PartialP φ T) → (a : A) → primGlue A T e
    prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
      → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
      → primGlue A T e → A

    -- Needed for transp in Glue.
    primFaceForall : (I → I) → I

module _ {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) where
  private
    E : (i : I) → Set (ℓ i)
    E  = λ i → P i
    ~E : (i : I) → Set (ℓ (~ i))
    ~E = λ i → P (~ i)

    A = P i0
    B = P i1

    f : A → B
    f x = transp E i0 x

    g : B → A
    g y = transp ~E i0 y

    u : ∀ i → A → E i
    u i x = transp (λ j → E (i ∧ j)) (~ i) x

    v : ∀ i → B → E i
    v i y = transp (λ j → ~E ( ~ i ∧ j)) i y

    fiberPath : (y : B) → (xβ0 xβ1 : fiber f y) → xβ0 ≡ xβ1
    fiberPath y (x0 , β0) (x1 , β1) k = ω , λ j → δ (~ j) where
      module _ (j : I) where
        private
          sys : A → ∀ i → PartialP (~ j ∨ j) (λ _ → E (~ i))
          sys x i (j = i0) = v (~ i) y
          sys x i (j = i1) = u (~ i) x
        ω0 = comp ~E (sys x0) ((β0 (~ j)))
        ω1 = comp ~E (sys x1) ((β1 (~ j)))
        θ0 = fill ~E (sys x0) (inc (β0 (~ j)))
        θ1 = fill ~E (sys x1) (inc (β1 (~ j)))
      sys = λ {j (k = i0) → ω0 j ; j (k = i1) → ω1 j}
      ω = hcomp sys (g y)
      θ = hfill sys (inc (g y))
      δ = λ (j : I) → comp E
            (λ i → λ { (j = i0) → v i y ; (k = i0) → θ0 j (~ i)
                     ; (j = i1) → u i ω ; (k = i1) → θ1 j (~ i) })
             (θ j)

    γ : (y : B) → y ≡ f (g y)
    γ y j = comp E (λ i → λ { (j = i0) → v i y
                            ; (j = i1) → u i (g y) }) (g y)

  pathToisEquiv : isEquiv f
  pathToisEquiv .equiv-proof y .fst .fst = g y
  pathToisEquiv .equiv-proof y .fst .snd = sym (γ y)
  pathToisEquiv .equiv-proof y .snd = fiberPath y _

  pathToEquiv : A ≃ B
  pathToEquiv .fst = f
  pathToEquiv .snd = pathToisEquiv

max_stars_repo_name: asr/my-agda

max_issues_repo_name: asr/my-agda

max_forks_repo_name: asr/my-agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Algebra.RingSolver.AlmostRing
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup

ℕAsAlmostRing : AlmostRing {ℓ-zero}
ℕAsAlmostRing = almostring ℕ 0 1 _+_ _·_ (λ n → n) (isalmostring
                    (ismonoid (issemigroup isSetℕ +-assoc) (λ n → (+-zero n) , refl))
                    (ismonoid (issemigroup isSetℕ ·-assoc) λ n → (·-identityʳ n) , (·-identityˡ n))
                    +-comm
                    ·-comm
                    (λ k l n → sym (·-distribˡ k l n) )
                    (λ k l n → sym (·-distribʳ k l n))
                    (λ _ _ → refl) (λ _ _ → refl)
                    (λ _ → refl) λ x → sym (0≡m·0 x))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
open import Nat
open import Prelude
open import core
open import contexts

open import lemmas-consistency
open import type-assignment-unicity
open import binders-disjoint-checks

open import lemmas-subst-ta

module preservation where
  -- if d and d' both result from filling the hole in ε with terms of the
  -- same type, they too have the same type.
  wt-different-fill : ∀{ Δ Γ d ε d1 d2 d' τ τ1 } →
            d == ε ⟦ d1 ⟧ →
            Δ , Γ ⊢ d :: τ →
            Δ , Γ ⊢ d1 :: τ1 →
            Δ , Γ ⊢ d2 :: τ1 →
            d' == ε ⟦ d2 ⟧ →
            Δ , Γ ⊢ d' :: τ
  wt-different-fill FHOuter D1 D2 D3 FHOuter
    with type-assignment-unicity D1 D2
  ... | refl = D3
  wt-different-fill (FHAp1 eps) (TAAp D1 D2) D3 D4 (FHAp1 D5) = TAAp (wt-different-fill eps D1 D3 D4 D5) D2
  wt-different-fill (FHAp2 eps) (TAAp D1 D2) D3 D4 (FHAp2 D5) = TAAp D1 (wt-different-fill eps D2 D3 D4 D5)
  wt-different-fill (FHNEHole eps) (TANEHole x D1 x₁) D2 D3 (FHNEHole D4) = TANEHole x (wt-different-fill eps D1 D2 D3 D4) x₁
  wt-different-fill (FHCast eps) (TACast D1 x) D2 D3 (FHCast D4) = TACast (wt-different-fill eps D1 D2 D3 D4) x
  wt-different-fill (FHFailedCast x) (TAFailedCast y x₁ x₂ x₃) D3 D4 (FHFailedCast eps) = TAFailedCast (wt-different-fill x y D3 D4 eps) x₁ x₂ x₃

  -- if a well typed term results from filling the hole in ε, then the term
  -- that filled the hole is also well typed
  wt-filling : ∀{ ε Δ Γ d τ d' } →
             Δ , Γ ⊢ d :: τ →
             d == ε ⟦ d' ⟧ →
             Σ[ τ' ∈ htyp ] (Δ , Γ ⊢ d' :: τ')
  wt-filling TAConst FHOuter = _ , TAConst
  wt-filling (TAVar x₁) FHOuter = _ , TAVar x₁
  wt-filling (TALam f ta) FHOuter = _ , TALam f ta

  wt-filling (TAAp ta ta₁) FHOuter = _ , TAAp ta ta₁
  wt-filling (TAAp ta ta₁) (FHAp1 eps) = wt-filling ta eps
  wt-filling (TAAp ta ta₁) (FHAp2 eps) = wt-filling ta₁ eps

  wt-filling (TAEHole x x₁) FHOuter = _ , TAEHole x x₁
  wt-filling (TANEHole x ta x₁) FHOuter = _ , TANEHole x ta x₁
  wt-filling (TANEHole x ta x₁) (FHNEHole eps) = wt-filling ta eps
  wt-filling (TACast ta x) FHOuter = _ , TACast ta x
  wt-filling (TACast ta x) (FHCast eps) = wt-filling ta eps
  wt-filling (TAFailedCast x y z w) FHOuter = _ , TAFailedCast x y z w
  wt-filling (TAFailedCast x x₁ x₂ x₃) (FHFailedCast y) = wt-filling x y

  -- instruction transitions preserve type
  preserve-trans : ∀{ Δ Γ d τ d' } →
            binders-unique d →
            Δ , Γ ⊢ d :: τ →
            d →> d' →
            Δ , Γ ⊢ d' :: τ
  preserve-trans bd TAConst ()
  preserve-trans bd (TAVar x₁) ()
  preserve-trans bd (TALam _ ta) ()
  preserve-trans (BUAp (BULam bd x₁) bd₁ (BDLam x₂ x₃)) (TAAp (TALam apt ta) ta₁) ITLam = lem-subst apt x₂ bd₁ ta ta₁
  preserve-trans bd (TAAp (TACast ta TCRefl) ta₁) ITApCast = TACast (TAAp ta (TACast ta₁ TCRefl)) TCRefl
  preserve-trans bd (TAAp (TACast ta (TCArr x x₁)) ta₁) ITApCast = TACast (TAAp ta (TACast ta₁ (~sym x))) x₁
  preserve-trans bd (TAEHole x x₁) ()
  preserve-trans bd (TANEHole x ta x₁) ()
  preserve-trans bd (TACast ta x) (ITCastID) = ta
  preserve-trans bd (TACast (TACast ta x) x₁) (ITCastSucceed x₂) = ta
  preserve-trans bd (TACast ta x) (ITGround (MGArr x₁)) = TACast (TACast ta (TCArr TCHole1 TCHole1)) TCHole1
  preserve-trans bd (TACast ta TCHole2) (ITExpand (MGArr x₁)) = TACast (TACast ta TCHole2) (TCArr TCHole2 TCHole2)
  preserve-trans bd (TACast (TACast ta x) x₁) (ITCastFail w y z) = TAFailedCast ta w y z
  preserve-trans bd (TAFailedCast x y z q) ()

  lem-bd-ε1 : ∀{ d ε d0} → d == ε ⟦ d0 ⟧ → binders-unique d → binders-unique d0
  lem-bd-ε1 FHOuter bd = bd
  lem-bd-ε1 (FHAp1 eps) (BUAp bd bd₁ x) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHAp2 eps) (BUAp bd bd₁ x) = lem-bd-ε1 eps bd₁
  lem-bd-ε1 (FHNEHole eps) (BUNEHole bd x) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHCast eps) (BUCast bd) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHFailedCast eps) (BUFailedCast bd) = lem-bd-ε1 eps bd

  -- this is the main preservation theorem, gluing together the above
  preservation : {Δ : hctx} {d d' : ihexp} {τ : htyp} {Γ : tctx} →
             binders-unique d →
             Δ , Γ ⊢ d :: τ →
             d ↦ d' →
             Δ , Γ ⊢ d' :: τ
  preservation bd D (Step x x₁ x₂)
    with wt-filling D x
  ... | (_ , wt) = wt-different-fill x D wt (preserve-trans (lem-bd-ε1 x bd) wt x₁) x₂

  -- note that the exact statement of preservation in the paper, where Γ is
  -- empty indicating that the terms are closed, is an immediate corrolary
  -- of the slightly more general statement above.
  preservation' : {Δ : hctx} {d d' : ihexp} {τ : htyp} →
             binders-unique d →
             Δ , ∅ ⊢ d :: τ →
             d ↦ d' →
             Δ , ∅ ⊢ d' :: τ
  preservation' = preservation

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


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

module Categories.NaturalTransformation.NaturalIsomorphism.Properties where

open import Level

open import Categories.Category
open import Categories.Category.Instance.Setoids
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Construction.LiftSetoids
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.NaturalTransformation.Properties

import Categories.Morphism as Mor
import Categories.Morphism.Properties as Morₚ
import Categories.Morphism.Reasoning as MR

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

module _ {F G : Functor C D} (α : NaturalIsomorphism F G) where
  private module C = Category C
  open Category D
  open Mor D
  open Functor F
  open Functor G renaming (F₀ to G₀; F₁ to G₁)
  open NaturalIsomorphism α

  -- We can move equations along natural isomorphism.

  module _ {A B} {f g : A C.⇒ B} where

    push-eq : F₁ f ≈ F₁ g → G₁ f ≈ G₁ g
    push-eq hyp = MR.push-eq D FX≅GX (⇒.commute f) (⇒.commute g) hyp

    pull-eq : G₁ f ≈ G₁ g → F₁ f ≈ F₁ g
    pull-eq hyp = MR.push-eq D (≅.sym FX≅GX) (⇐.commute f) (⇐.commute g) hyp

-- properties of natural isomorphisms over an endofunctor
module _ {F : Endofunctor C} where
  private
    module C = Category C
    module F = Functor F
    module MC = Mor C

  module _ (α : F ≃ idF) where
    open C
    open HomReasoning
    open F
    open MC
    open MR C
    open Mor C
    open Morₚ C
    open NaturalIsomorphism α

    F≃id-comm₁ : ∀ {A} → ⇒.η (F₀ A) ≈ F₁ (⇒.η A)
    F≃id-comm₁ {A} = begin
      ⇒.η (F₀ A)                           ≈⟨ introʳ (F-resp-≈ (iso.isoˡ _) ○ identity) ⟩
      ⇒.η (F₀ A) ∘ F₁ (⇐.η A ∘ ⇒.η A)      ≈⟨ refl⟩∘⟨ homomorphism ⟩
      ⇒.η (F₀ A) ∘ F₁ (⇐.η A) ∘ F₁ (⇒.η A) ≈⟨ cancelˡ (⇒.commute _ ○ iso.isoˡ _) ⟩
      F₁ (⇒.η A)                           ∎

    F≃id-comm₂ : ∀ {A} → ⇐.η (F₀ A) ≈ F₁ (⇐.η A)
    F≃id-comm₂ {A} = begin
      ⇐.η (F₀ A)                             ≈⟨ introˡ (F-resp-≈ (iso.isoˡ _) ○ identity) ⟩
      F₁ (⇐.η A ∘ ⇒.η A) ∘ ⇐.η (F₀ A)        ≈⟨ homomorphism ⟩∘⟨refl ⟩
      (F₁ (⇐.η A) ∘ F₁ (⇒.η A)) ∘ ⇐.η (F₀ A) ≈⟨ cancelʳ (⟺ (⇐.commute _) ○ iso.isoˡ _) ⟩
      F₁ (⇐.η A)                             ∎

    F≃id⇒id : ∀ {A} {f : A ⇒ A} → F₁ f ≈ id → f ≈ id
    F≃id⇒id {A} {f} eq = Iso⇒Mono (Iso-swap (iso A)) _ _ helper
      where helper : ⇐.η A ∘ f ≈ ⇐.η A ∘ id
            helper = begin
              ⇐.η A ∘ f    ≈⟨ ⇐.commute f ⟩
              F₁ f ∘ ⇐.η A ≈⟨ eq ⟩∘⟨refl ⟩
              id ∘ ⇐.η A   ≈˘⟨ id-comm ⟩
              ⇐.η A ∘ id   ∎

-- unlift universe level
module _ {c ℓ ℓ′ e} {F G : Functor C (Setoids c ℓ)} (α : LiftSetoids ℓ′ e ∘F F ≃ LiftSetoids ℓ′ e ∘F G) where
  open NaturalIsomorphism α

  unlift-≃ : F ≃ G
  unlift-≃ = record
    { F⇒G = unlift-nat F⇒G
    ; F⇐G = unlift-nat F⇐G
    ; iso = λ X → record
      { isoˡ = λ eq → lower (iso.isoˡ X (lift eq))
      ; isoʳ = λ eq → lower (iso.isoʳ X (lift eq))
      }
    }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Standard where

module Data where
      module Empty where open import Light.Implementation.Standard.Data.Empty public
      module Unit where open import Light.Implementation.Standard.Data.Unit public
      module These where open import Light.Implementation.Standard.Data.These public
      module Product where open import Light.Implementation.Standard.Data.Product public

module Relation where
      module Decidable where open import Light.Implementation.Standard.Relation.Decidable public
      module Sets where open import Light.Implementation.Standard.Relation.Sets public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module Oscar.Data where

open import Agda.Builtin.Unit
open import Oscar.Function
open import Oscar.Level

infixr 20 ∷_
infixr 20 _∷_

data NAT : Set where
  ∅ : NAT
  ∷_ : NAT → NAT

testNAT : NAT
testNAT = ∷ ∷ ∷ ∅

-- List
data ⟦_⟧ {a} (A : Set a) : Set a where
  ∅ : ⟦ A ⟧
  _∷_ : A → ⟦ A ⟧ → ⟦ A ⟧

-- Nat
⟦⟧ = ⟦ ⊤ ⟧

test⟦⟧ : ⟦⟧
test⟦⟧ = {!(tt ∷_) ∅ !}

infix 21 ¡_
pattern ¡_ ⟦A⟧ = tt ∷ ⟦A⟧
--¡ : ⟦⟧ → ⟦⟧
--¡ ⟦A⟧ = tt ∷ ⟦A⟧

-- Fin (with a payload)
-- n-1 , ... 0
data ⟦_⟧[_] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ¡ n ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ] → ⟦ A ⟧[ ¡ n ]

⟦⟧[_] = ⟦ const ⊤ ⟧[_]

-- Vec (with an (optional) index)
-- 0 ≤ n, counting down from n to 0
data ⟦_⟧[_₀] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ ∅ ₀]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ₀] → ⟦ A ⟧[ ¡ n ₀]

⟦⟧[_₀] = ⟦ const ⊤ ⟧[_₀]

-- Interval↓
-- Interval⟨_⟩［_↙_）
-- Descenderval
-- m ≤ n, counting down from n-1 to m
data ⟦_⟧[_≤_↓] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ≤ m ↓]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ m ≤ n ↓] → ⟦ A ⟧[ m ≤ ¡ n ↓]

⟦⟧[_≤_↓] = ⟦ const ⊤ ⟧[_≤_↓]

-- Fin⟨_⟩ = λ A n → Interval↓ A 0 n
-- Vec n = Descenderval 0 (↑ n)

-- Interval⟨_⟩［_↗_）
-- Ascenderval
-- m ≤ n, counting up from m to n-1
data ⟦_⟧[↑_≤_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[↑ m ≤ m ]
  _∷_ : ∀ {n} → A m → ⟦ A ⟧[↑ ¡ m ≤ n ] → ⟦ A ⟧[↑ m ≤ n ]

⟦⟧[↑_≤_] = ⟦ const ⊤ ⟧[↑_≤_]

-- Inj (almost)
-- m ≤ n, m-1...0, n-1...n-m
-- Paradescenderval
data ⟦_⟧[↓_≤_↓] {a} (A : ⟦⟧ → ⟦⟧ → Set a) : ⟦⟧ → ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[↓ ∅ ≤ n ↓]
  _∷_ : ∀ {m n} → A m n → ⟦ A ⟧[↓ m ≤ n ↓] → ⟦ A ⟧[↓ ¡ m ≤ ¡ n ↓]

-- Inj = Paradescenderval (λ _ → Fin ∘ ↑_)

⟦⟧[↓_≤_↓] = ⟦ const const ⊤ ⟧[↓_≤_↓]

infix 21 ‼_
pattern ‼_ ⟦A⟧ = tt ∷ ⟦A⟧ -- tricky, works for all above _∷_ constructors only because it is defined afterwards, won't work for any later-defined constructors

{-

Function (B m → B n)

Fin
Term
AList (SubstitutionList) Substilist
Step
List

FinTerm (SubstitutionFunction) Substifunction

SubstitutionFunction.internal
SubstitutionFunction.Morphism
SubstitutionFunction.IsSemigroupoid
SubstitutionFunction.IsCategory

IsSemigroupoid
IsCategory

-}
--Nat = ⟦⟧
--Vec :

-- mutual

--   Terms : Nat → Nat → Set 𝔣
--   Terms N m = Vec (Term m) N

--   data Term (m : Nat) : Set 𝔣 where
--     i : (x : Fin m) → Term m
--     leaf : Term m
--     _fork_ : (s t : Term m) → Term m
--     function : FunctionName → ∀ {N} → Terms N m → Term m


text:
open import Agda.Builtin.Nat

record R : Set where
  field
    x : Nat

open R {{...}}

f₁ f₂ : R

-- This is fine.
x ⦃ f₁ ⦄ = 0

-- THIS WORKS BUT MAKES NO SENSE!!!
f₂ ⦃ .x ⦄ = 0

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text: {-# POLARITY F #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module Imports.Issue1913-M where

data D : Set where
  d : D


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

   Copyright (c) 2021 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
import      LibraBFT.Yasm.Base as LYB

-- This module provides a single import for all Yasm modules

module LibraBFT.Yasm.Yasm
   (ℓ-EC        : Level)
   (EpochConfig : Set ℓ-EC)
   (epochId     : EpochConfig → EpochId)
   (authorsN    : EpochConfig → ℕ)
   (parms       : LYB.SystemParameters ℓ-EC EpochConfig epochId authorsN)
   (senderPKOK  : (ec : EpochConfig) → PK → LYB.SystemParameters.PeerId parms → Set)
  where
 open LYB.SystemParameters parms
 open import LibraBFT.Yasm.AvailableEpochs PeerId ℓ-EC EpochConfig epochId authorsN
             using (AvailableEpochs) renaming (lookup' to EC-lookup; lookup'' to EC-lookup') public
 open import LibraBFT.Yasm.Base       ℓ-EC EpochConfig epochId authorsN                      public
 open import LibraBFT.Yasm.System     ℓ-EC EpochConfig epochId authorsN parms                public
 open import LibraBFT.Yasm.Properties ℓ-EC EpochConfig epochId authorsN parms senderPKOK     public
 open import Util.FunctionOverride    PeerId _≟PeerId_                                       public

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
module Vehicle.Data.Tensor where

open import Level using (Level)
open import Data.Empty.Polymorphic using (⊥)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.List.Base using (List; []; _∷_)
open import Data.Vec.Functional using (Vector)

private
  variable
    a : Level
    A : Set a
    n : ℕ

Tensor : Set a → List ℕ → Set a
Tensor A []           = ⊥
Tensor A (n ∷ [])     = Vector A n
Tensor A (m ∷ n ∷ ns) = Vector (Tensor A (n ∷ ns)) m

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
postulate
  X A : Set

module Foo {{x : X}} where

  postulate
    B C : Set
    foo : A → B → C → Set

module Bar {{x : X}} where
  open Foo

  postulate
    -- The following fails to infer the instance argument if we do not either:
    --   * apply {{x}} explicitly to foo
    --   * apply {{x}} explicitly when opening module Foo
    --   * define fail1 in module Foo
    fail1 : ∀ {a b b' c c'} → foo a b c → foo a b' c'

    -- However, the following works
    work1 : ∀ {a b c} → foo a b c → foo a b c
    work2 : ∀ {a a' b c} → foo a b c → foo a' b c
    work3 : ∀ {a b b' c} → foo a b c → foo a b' c
    work4 : ∀ {a a' b b' c} → foo a b c → foo a' b' c
    work5 : ∀ {a b c c'} → foo a b c → foo a b c'
    work6 : ∀ {a a' b c c'} → foo a b c → foo a' b c'
    work7 : ∀ {a a' b b' c c'} → foo a b c → foo a' b' c'

data Nat : Set where
  suc : Nat → Nat
  instance
    zero : Nat

instance
  one = suc zero

data IsSuc : Nat → Set where
  isSuc : ∀{n} → IsSuc (suc n)

postulate
  F : {{x : Nat}} (p : IsSuc x) → Set

test = F isSuc  -- yellow, but should not be


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

open import HoTT
open import homotopy.WedgeExtension
import homotopy.SuspAdjointLoop as SAL

module homotopy.Freudenthal where

{- lemma (move this where?) -}
private
  move1-left-on-left : ∀ {i} {A : Type i} {x y : A} (p : x == y) (q : x == y)
    → ((! q) ∙ p == idp → p == q)
  move1-left-on-left p idp h = h

module FreudenthalEquiv
  {i} (n k : ℕ₋₂) (kle : k ≤T S n +2+ S n)
  (X : Ptd i) {{cX : is-connected (S (S n)) (de⊙ X)}} where

  Q : Susp (de⊙ X) → Type i
  Q x = Trunc k (north == x)

  ⊙up : X ⊙→ ⊙Ω (⊙Susp (de⊙ X))
  ⊙up = SAL.η _

  up = fst ⊙up

  Codes-mer-args : args {a₀ = pt X} {b₀ = [_] {n = k} (pt X)}
  Codes-mer-args = record {n = S n; m = S n;
    P = λ _ _ → (Trunc k (de⊙ X) , raise-level-≤T kle Trunc-level);
    f = [_]; g = idf _; p = idp}

  module CodesExt =
    WedgeExt {a₀ = pt X} {b₀ = [_] {n = k} (pt X)} Codes-mer-args

  Codes-mer : de⊙ X → Trunc k (de⊙ X) → Trunc k (de⊙ X)
  Codes-mer = CodesExt.ext

  Codes-mer-β-l : (λ a → Codes-mer a [ pt X ]) == [_]
  Codes-mer-β-l = λ= CodesExt.β-l

  Codes-mer-β-r : (λ b → Codes-mer (pt X) b) == idf _
  Codes-mer-β-r = λ= $ CodesExt.β-r

  Codes-mer-coh : app= Codes-mer-β-l (pt X) == app= Codes-mer-β-r [ pt X ]
  Codes-mer-coh =
    app= Codes-mer-β-l (pt X)
      =⟨ app=-β CodesExt.β-l (pt X) ⟩
    CodesExt.β-l (pt X)
      =⟨ ! (move1-left-on-left _ _ CodesExt.coh) ⟩
    CodesExt.β-r [ pt X ]
      =⟨ ! (app=-β CodesExt.β-r [ pt X ]) ⟩
    app= Codes-mer-β-r [ pt X ] ∎

  Codes-mer-is-equiv : (x : de⊙ X) → is-equiv (Codes-mer x)
  Codes-mer-is-equiv =
    conn-extend (pointed-conn-out {n = S n} (de⊙ X) (pt X))
      (λ x' → (is-equiv (Codes-mer x') , is-equiv-level))
      (λ tt → transport is-equiv (! (Codes-mer-β-r)) (idf-is-equiv _))

  Codes-mer-equiv : (x : de⊙ X) → Trunc k (de⊙ X) ≃ Trunc k (de⊙ X)
  Codes-mer-equiv x = (Codes-mer x , Codes-mer-is-equiv x)

  Codes-mer-inv-x₀ : <– (Codes-mer-equiv (pt X)) == idf _
  Codes-mer-inv-x₀ =
       ap is-equiv.g (conn-extend-β
          (pointed-conn-out (de⊙ X) (pt X))
          (λ x' → (is-equiv (Codes-mer x') , is-equiv-level))
          _ unit)
     ∙ lemma (! (Codes-mer-β-r)) (snd $ ide _)
    where lemma : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
            (α : f == g) (e : is-equiv f)
            → is-equiv.g (transport is-equiv α e) == is-equiv.g e
          lemma idp e = idp

  module CodesRec = SuspRec (Trunc k (de⊙ X)) (Trunc k (de⊙ X)) (ua ∘ Codes-mer-equiv)

  Codes : Susp (de⊙ X) → Type i
  Codes = CodesRec.f

  Codes-has-level : (x : Susp (de⊙ X)) → has-level k (Codes x)
  Codes-has-level = Susp-elim Trunc-level Trunc-level
                      (λ _ → prop-has-all-paths-↓)

  {-
    favonia:

    This equation should be true: [⊙Trunc-fmap ⊙up = (decodeN , decodeN-pt)].
    Maybe there is a way to refactor the following code so that
    pointedness is handled more elegantly.
  -}

  decodeN : Codes north → Trunc k (north' (de⊙ X) == north)
  decodeN = Trunc-fmap up

  decodeN-pt : decodeN [ pt X ] == [ idp ]
  decodeN-pt = snd (⊙Trunc-fmap ⊙up)

  decodeS : Codes south → Q south
  decodeS = Trunc-fmap merid

  encode₀ : {x : Susp (de⊙ X)} → north == x → Codes x
  encode₀ α = transport Codes α [ pt X ]

  encode : {x : Susp (de⊙ X)} → Trunc k (north == x) → Codes x
  encode {x} tα = Trunc-rec {{Codes-has-level x}} encode₀ tα

  ⊙decodeN : ⊙Trunc k X ⊙→ ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X)))
  ⊙decodeN = decodeN , ap [_] (!-inv-r (merid (pt X)))

  ⊙encodeN : ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X))) ⊙→ ⊙Trunc k X
  ⊙encodeN = encode , idp

  abstract
    encode-decodeN : (c : Codes north) → encode (decodeN c) == c
    encode-decodeN = Trunc-elim
      {{λ _ → =-preserves-level Trunc-level}}
      (λ x →
        encode (decodeN [ x ])
          =⟨ idp ⟩
        coe (ap Codes (merid x ∙ ! (merid (pt X)))) [ pt X ]
          =⟨ ap-∙ Codes (merid x) (! (merid (pt X))) |in-ctx (λ w → coe w [ pt X ]) ⟩
        coe (ap Codes (merid x) ∙ ap Codes (! (merid (pt X)))) [ pt X ]
          =⟨ coe-∙ (ap Codes (merid x)) (ap Codes (! (merid (pt X)))) [ pt X ] ⟩
        coe (ap Codes (! (merid (pt X)))) (coe (ap Codes (merid x)) [ pt X ])
          =⟨ SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) x
            |in-ctx (λ w → coe (ap Codes (! (merid (pt X)))) (coe w [ pt X ])) ⟩
        coe (ap Codes (! (merid (pt X)))) (coe (ua (Codes-mer-equiv x)) [ pt X ])
          =⟨ coe-β (Codes-mer-equiv x) [ pt X ]
            |in-ctx (λ w → coe (ap Codes (! (merid (pt X)))) w) ⟩
        coe (ap Codes (! (merid (pt X)))) (Codes-mer x [ pt X ])
          =⟨ app= Codes-mer-β-l x
            |in-ctx (λ w → coe (ap Codes (! (merid (pt X)))) w) ⟩
        coe (ap Codes (! (merid (pt X)))) [ x ]
          =⟨ coe-ap-! Codes (merid (pt X)) [ x ] ⟩
        coe! (ap Codes (merid (pt X))) [ x ]
          =⟨ SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) (pt X)
            |in-ctx (λ w → coe! w [ x ]) ⟩
        coe! (ua (Codes-mer-equiv (pt X))) [ x ]
          =⟨ coe!-β (Codes-mer-equiv (pt X)) [ x ] ⟩
        <– (Codes-mer-equiv (pt X)) [ x ]
          =⟨ app= Codes-mer-inv-x₀ [ x ] ⟩
        [ x ] ∎)

  decode : {x : Susp (de⊙ X)} → Codes x → Q x
  decode {x} = Susp-elim
    {P = λ y → Codes y → Q y}
    decodeN decodeS
    (λ x' → ↓-→-from-transp (λ= (STS x')))
    x
    where
    abstract
      coh : {s₁ s₂ : Susp (de⊙ X)} (p : s₁ == s₂)
        → (ap (λ s → s ∙ p) (!-inv-r p))
          == ∙-assoc p (! p) p ∙ ap (λ s → p ∙ s) (!-inv-l p) ∙ ∙-unit-r p
      coh idp = idp

      P : de⊙ X → de⊙ X → (S (n +2+ (S n))) -Type (lmax i i)
      P = λ x₁ x₂ →
        ((transport Q (merid x₁) (Trunc-fmap up [ x₂ ])
          == Trunc-fmap merid (transport Codes (merid x₁) [ x₂ ])),
         =-preserves-level (raise-level-≤T kle Trunc-level))

      f : (a : de⊙ X) → fst (P a (pt X))
      f a =
        transport Q (merid a) [ up (pt X) ]
          =⟨ transport-Trunc' (north ==_) (merid a) (up (pt X)) ⟩
        [ transport (north ==_) (merid a) (up (pt X)) ]
          =⟨ ap [_] $ transp-cst=idf {A = Susp (de⊙ X)} (merid a) (up (pt X)) ⟩
        [ (merid (pt X) ∙ ! (merid (pt X))) ∙ merid a ]
          =⟨ ap [_] $ ap (λ s → s ∙ merid a) (!-inv-r (merid (pt X))) ⟩
        [ merid a ]
          =⟨ idp ⟩
        Trunc-fmap merid [ a ]
          =⟨ ap (Trunc-fmap merid) (! (app= Codes-mer-β-l a)) ⟩
        Trunc-fmap merid (Codes-mer a [ pt X ])
          =⟨ ap (Trunc-fmap merid) (! (coe-β (Codes-mer-equiv a) [ pt X ])) ⟩
        Trunc-fmap merid (coe (ua (Codes-mer-equiv a)) [ pt X ])
          =⟨ ! (SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) a)
            |in-ctx (λ w → Trunc-fmap merid (coe w [ pt X ])) ⟩
        Trunc-fmap merid (transport Codes (merid a) [ pt X ]) ∎

      g : (b : de⊙ X) → fst (P (pt X) b)
      g b =
        transport Q (merid (pt X)) [ up b ]
          =⟨ transport-Trunc' (north ==_) (merid (pt X)) (up b) ⟩
        [ transport (north ==_) (merid (pt X)) (up b) ]
          =⟨ ap [_] $ transp-cst=idf {A = Susp (de⊙ X)} (merid (pt X)) (up b)  ⟩
        [ (merid b ∙ ! (merid (pt X))) ∙ merid (pt X) ]
          =⟨ ap [_] $ ∙-assoc (merid b) (! (merid (pt X))) (merid (pt X))
                      ∙ ap (λ s → merid b ∙ s) (!-inv-l (merid (pt X)))
                      ∙ ∙-unit-r (merid b) ⟩
        [ merid b ]
          =⟨ idp ⟩
        Trunc-fmap merid [ b ]
          =⟨ ap (Trunc-fmap merid) (! (app= Codes-mer-β-r [ b ])) ⟩
        Trunc-fmap merid (Codes-mer (pt X) [ b ])
          =⟨ ap (Trunc-fmap merid) (! (coe-β (Codes-mer-equiv (pt X)) [ b ])) ⟩
        Trunc-fmap merid (coe (ua (Codes-mer-equiv (pt X))) [ b ])
          =⟨ ! (SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) (pt X))
            |in-ctx (λ w → Trunc-fmap merid (coe w [ b ])) ⟩
        Trunc-fmap merid (transport Codes (merid (pt X)) [ b ]) ∎

      p : f (pt X) == g (pt X)
      p = ap2
        (λ p₁ p₂ →
          transport Q (merid (pt X)) [ up (pt X) ]
            =⟨ transport-Trunc' (north ==_) (merid (pt X)) (up (pt X)) ⟩
          [ transport (north ==_) (merid (pt X)) (up (pt X)) ]
            =⟨ ap [_] $ transp-cst=idf {A = Susp (de⊙ X)} (merid (pt X)) (up (pt X)) ⟩
          [ (merid (pt X) ∙ ! (merid (pt X))) ∙ merid (pt X) ]
            =⟨ ap [_] p₁ ⟩
          [ merid (pt X) ]
            =⟨ idp ⟩
          Trunc-fmap merid [ pt X ]
            =⟨ ap (Trunc-fmap merid) (! p₂) ⟩
          Trunc-fmap merid (Codes-mer (pt X) [ pt X ])
            =⟨ ap (Trunc-fmap merid) (! (coe-β (Codes-mer-equiv (pt X)) [ pt X ])) ⟩
          Trunc-fmap merid (coe (ua (Codes-mer-equiv (pt X))) [ pt X ])
            =⟨ ! (SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) (pt X))
              |in-ctx (λ w → Trunc-fmap merid (coe w [ pt X ])) ⟩
          Trunc-fmap merid (transport Codes (merid (pt X)) [ pt X ]) ∎)
        (coh (merid (pt X))) Codes-mer-coh

      STS-args : args {a₀ = pt X} {b₀ = pt X}
      STS-args =
        record {n = S n; m = S n; P = P; f = f; g = g; p = p}

      STS : (x' : de⊙ X) (c : Codes north) →
        transport Q (merid x') (Trunc-fmap up c)
        == Trunc-fmap merid (transport Codes (merid x') c)
      STS x' = Trunc-elim {{λ _ → =-preserves-level Trunc-level}}
                          (WedgeExt.ext STS-args x')

  abstract
    decode-encode : {x : Susp (de⊙ X)} (tα : Q x)
      → decode {x} (encode {x} tα) == tα
    decode-encode {x} = Trunc-elim
      {P = λ tα → decode {x} (encode {x} tα) == tα}
      {{λ _ → =-preserves-level Trunc-level}}
      (J (λ y p → decode {y} (encode {y} [ p ]) == [ p ])
         (ap [_] (!-inv-r (merid (pt X)))))

  eq : Trunc k (de⊙ X) ≃ Trunc k (north' (de⊙ X) == north)
  eq = equiv decodeN encode decode-encode encode-decodeN

  ⊙eq : ⊙Trunc k X ⊙≃ ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X)))
  ⊙eq = ≃-to-⊙≃ eq (snd ⊙decodeN)

  abstract
    ⊙decodeN-⊙encodeN : ⊙decodeN ⊙∘ ⊙encodeN == ⊙idf _
    ⊙decodeN-⊙encodeN =
      ⊙λ=' {X = ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X)))}
           {Y = ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X)))}
           decode-encode $
      ↓-idf=cst-in $
      ! (∙-unit-r (ap [_] (!-inv-r (merid (pt X)))))

    ⊙<–-⊙eq : ⊙<– ⊙eq == ⊙encodeN
    ⊙<–-⊙eq =
      –>-is-inj (post⊙∘-equiv {Z = ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X)))} ⊙eq) (⊙<– ⊙eq) ⊙encodeN $
      ⊙decodeN ⊙∘ ⊙<– ⊙eq
        =⟨ ⊙<–-inv-r ⊙eq ⟩
      ⊙idf _
        =⟨ ! ⊙decodeN-⊙encodeN ⟩
      ⊙decodeN ⊙∘ ⊙encodeN =∎

  path : Trunc k (de⊙ X) == Trunc k (north' (de⊙ X) == north)
  path = ua eq

  ⊙path : ⊙Trunc k X == ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X)))
  ⊙path = ⊙ua ⊙eq

{- timjb: it is probably easier to show the naturality of ⊙decodeN
   and deduce the naturality of ⊙encodeN from that than to show
   the naturality of ⊙encodeN directly (as done below) -}
module FreudenthalEquivNatural
  {i} (n k : ℕ₋₂) (kle : k ≤T S n +2+ S n)
  {X Y : Ptd i} (f : X ⊙→ Y)
  {{cX : is-connected (S (S n)) (de⊙ X)}}
  {{cY : is-connected (S (S n)) (de⊙ Y)}} where

  private
    module FX = FreudenthalEquiv n k kle X {{cX}}
    module FY = FreudenthalEquiv n k kle Y {{cY}}

  Codes-mer-map : ∀ (x : de⊙ X) (tx : Trunc k (de⊙ X))
    → Trunc-fmap (fst f) (FX.Codes-mer x tx) ==
      FY.Codes-mer (fst f x) (Trunc-fmap (fst f) tx)
  Codes-mer-map =
    WedgeExt.ext {A = de⊙ X} {a₀ = pt X} {B = Trunc k (de⊙ X)} {b₀ = [ pt X ]} $
    record
    { n = S n; m = S n
    ; P = λ x tx → (P x tx , P-level x tx)
    ; f = λ x → ↯ (f-seq x)
    ; g = λ tx → ↯ (g-seq tx)
    ; p = =ₛ-out p
    }
    where
    P : de⊙ X → Trunc k (de⊙ X) → Type i
    P x tx =
      Trunc-fmap (fst f) (FX.Codes-mer x tx) ==
      FY.Codes-mer (fst f x) (Trunc-fmap (fst f) tx)
    P-level : ∀ x tx → has-level (S n +2+ S n) (P x tx)
    P-level x tx = =-preserves-level (raise-level-≤T kle Trunc-level)
    f-seq : ∀ x → Trunc-fmap (fst f) (FX.Codes-mer x [ pt X ]) =-=
                  FY.Codes-mer (fst f x) (Trunc-fmap (fst f) [ pt X ])
    f-seq x =
      Trunc-fmap (fst f) (FX.Codes-mer x [ pt X ])
        =⟪ ap (Trunc-fmap (fst f)) (FX.CodesExt.β-l x) ⟫
      [ fst f x ]
        =⟪ ! (FY.CodesExt.β-l (fst f x)) ⟫
      FY.Codes-mer (fst f x) [ pt Y ]
        =⟪ ap (FY.Codes-mer (fst f x) ∘ [_]) (! (snd f)) ⟫
      FY.Codes-mer (fst f x) [ fst f (pt X) ] ∎∎
    g-seq : ∀ tx → Trunc-fmap (fst f) (FX.Codes-mer (pt X) tx) =-=
                   FY.Codes-mer (fst f (pt X)) (Trunc-fmap (fst f) tx)
    g-seq tx =
      Trunc-fmap (fst f) (FX.Codes-mer (pt X) tx)
        =⟪ ap (Trunc-fmap (fst f)) (FX.CodesExt.β-r tx) ⟫
      Trunc-fmap (fst f) tx
        =⟪ ! (FY.CodesExt.β-r (Trunc-fmap (fst f) tx)) ⟫
      FY.Codes-mer (pt Y) (Trunc-fmap (fst f) tx)
        =⟪ ap (λ y → FY.Codes-mer y (Trunc-fmap (fst f) tx)) (! (snd f)) ⟫
      FY.Codes-mer (fst f (pt X)) (Trunc-fmap (fst f) tx) ∎∎
    p : f-seq (pt X) =ₛ g-seq [ pt X ]
    p =
      ap (Trunc-fmap (fst f)) (FX.CodesExt.β-l (pt X)) ◃∙
      ! (FY.CodesExt.β-l (fst f (pt X))) ◃∙
      ap (FY.Codes-mer (fst f (pt X)) ∘ [_]) (! (snd f)) ◃∎
        =ₛ⟨ 0 & 1 & ap-seq-=ₛ (Trunc-fmap (fst f)) $
                    pre-rotate-out {p = FX.CodesExt.β-l (pt X)} {q = []} {r = FX.CodesExt.β-r [ pt X ] ◃∎} $
                    =ₛ-in $ ! $ FX.CodesExt.coh ⟩
      ap (Trunc-fmap (fst f)) (FX.CodesExt.β-r [ pt X ]) ◃∙
      ! (FY.CodesExt.β-l (fst f (pt X))) ◃∙
      ap (FY.Codes-mer (fst f (pt X)) ∘ [_]) (! (snd f)) ◃∎
        =ₛ⟨ 1 & 1 & pre-rotate-in $
            homotopy-naturality
              [_]
              (λ y → FY.Codes-mer y [ pt Y ])
              (! ∘ FY.CodesExt.β-l)
              (! (snd f)) ⟩
      ap (Trunc-fmap (fst f)) (FX.CodesExt.β-r [ pt X ]) ◃∙
      ! (ap [_] (! (snd f))) ◃∙
      ! (FY.CodesExt.β-l (pt Y)) ◃∙
      ap (λ y → FY.Codes-mer y [ pt Y ]) (! (snd f)) ◃∙
      ap (FY.Codes-mer (fst f (pt X)) ∘ [_]) (! (snd f)) ◃∎
        =ₛ⟨ 3 & 2 & ap-comm-=ₛ (λ y y' → FY.Codes-mer y [ y' ]) (! (snd f)) (! (snd f)) ⟩
      ap (Trunc-fmap (fst f)) (FX.CodesExt.β-r [ pt X ]) ◃∙
      ! (ap [_] (! (snd f))) ◃∙
      ! (FY.CodesExt.β-l (pt Y)) ◃∙
      ap (λ y → FY.Codes-mer (pt Y) [ y ]) (! (snd f)) ◃∙
      ap (λ y → FY.Codes-mer y [ fst f (pt X) ]) (! (snd f)) ◃∎
        =ₛ⟨ 2 & 1 & !-=ₛ $
            pre-rotate-out {p = FY.CodesExt.β-l (pt Y)} {q = []} {r = FY.CodesExt.β-r [ pt Y ] ◃∎} $
            =ₛ-in $ ! $ FY.CodesExt.coh ⟩
      ap (Trunc-fmap (fst f)) (FX.CodesExt.β-r [ pt X ]) ◃∙
      ! (ap [_] (! (snd f))) ◃∙
      ! (FY.CodesExt.β-r [ pt Y ]) ◃∙
      ap (λ y → FY.Codes-mer (pt Y) [ y ]) (! (snd f)) ◃∙
      ap (λ y → FY.Codes-mer y [ fst f (pt X) ]) (! (snd f)) ◃∎
        =ₛ⟨ 1 & 3 & !ₛ $ pre-rotate-in $
            homotopy-naturality
              [_]
              (FY.Codes-mer (pt Y) ∘ [_])
              (! ∘ FY.CodesExt.β-r ∘ [_])
              (! (snd f)) ⟩
      ap (Trunc-fmap (fst f)) (FX.CodesExt.β-r [ pt X ]) ◃∙
      ! (FY.CodesExt.β-r (Trunc-fmap (fst f) [ pt X ])) ◃∙
      ap (λ y → FY.Codes-mer y [ fst f (pt X) ]) (! (snd f)) ◃∎ ∎ₛ

  Codes-fmap : ∀ {x : Susp (de⊙ X)}
    → FX.Codes x
    → FY.Codes (Susp-fmap (fst f) x)
  Codes-fmap {x} =
    Susp-elim
      {P = λ x → FX.Codes x → FY.Codes (Susp-fmap (fst f) x)}
      (Trunc-fmap (fst f))
      (Trunc-fmap (fst f))
      (λ x → ↓-→-from-transp $ λ= $
        Trunc-elim {{λ tx → =-preserves-level Trunc-level}} $ λ x' →
        transport (FY.Codes ∘ Susp-fmap (fst f)) (merid x) [ fst f x' ]
          =⟨ ap (λ q → coe q [ fst f x' ]) (ap-∘ FY.Codes (Susp-fmap (fst f)) (merid x)) ⟩
        transport FY.Codes (ap (Susp-fmap (fst f)) (merid x)) [ fst f x' ]
          =⟨ ap (λ p → transport FY.Codes p [ fst f x' ]) $
             SuspFmap.merid-β (fst f) x ⟩
        transport FY.Codes (merid (fst f x)) [ fst f x' ]
          =⟨ ap (λ p → coe p [ fst f x' ]) (FY.CodesRec.merid-β (fst f x)) ⟩
        coe (ua (FY.Codes-mer-equiv (fst f x))) [ fst f x' ]
          =⟨ coe-β (FY.Codes-mer-equiv (fst f x)) [ fst f x' ] ⟩
        FY.Codes-mer (fst f x) [ fst f x' ]
          =⟨ ! (Codes-mer-map x [ x' ])  ⟩
        Trunc-fmap (fst f) (FX.Codes-mer x [ x' ])
          =⟨ ap (Trunc-fmap (fst f)) (! (coe-β (FX.Codes-mer-equiv x) [ x' ])) ⟩
        Trunc-fmap (fst f) (coe (ua (FX.Codes-mer-equiv x)) [ x' ])
          =⟨ ap (λ p → Trunc-fmap (fst f) (coe p [ x' ])) (! (FX.CodesRec.merid-β x)) ⟩
        Trunc-fmap (fst f) (transport FX.Codes (merid x) [ x' ]) =∎)
      x

  encode-natural : ∀ {x : Susp (de⊙ X)}
    (tα : Trunc k (north == x))
    → FY.encode (Trunc-fmap (ap (Susp-fmap (fst f))) tα)
      ==
      Codes-fmap {x} (FX.encode tα)
  encode-natural {x} =
    Trunc-elim {{λ tα → =-preserves-level (FY.Codes-has-level (Susp-fmap (fst f) x))}} $
    J (λ x p → FY.encode (Trunc-fmap (ap (Susp-fmap (fst f))) [ p ]) == Codes-fmap {x} (FX.encode [ p ])) $
    ! (ap [_] (snd f))

  ⊙encodeN-natural :
    FY.⊙encodeN ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-fmap (fst f))) ◃⊙idf
    =⊙∘
    ⊙Trunc-fmap f ◃⊙∘
    FX.⊙encodeN ◃⊙idf
  ⊙encodeN-natural =
    =⊙∘-in $
    ⊙λ=' {X = ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X)))} {Y = ⊙Trunc k Y} (encode-natural {north}) $
    ↓-idf=cst-in {p = ! (ap [_] (snd f))} $
    ! $ !-inv-l (ap [_] (snd f))

{- Used to prove stability in iterated suspensions -}
module FreudenthalIso
  {i} (n : ℕ₋₂) (k : ℕ) (kle : ⟨ S k ⟩ ≤T S n +2+ S n)
  (X : Ptd i) {{_ : is-connected (S (S n)) (de⊙ X)}} where

  open FreudenthalEquiv n ⟨ S k ⟩ kle X public

  hom : Ω^S-group k (⊙Trunc ⟨ S k ⟩ X)
     →ᴳ Ω^S-group k (⊙Trunc ⟨ S k ⟩ (⊙Ω (⊙Susp (de⊙ X))))
  hom = Ω^S-group-fmap k (decodeN , decodeN-pt)

  iso : Ω^S-group k (⊙Trunc ⟨ S k ⟩ X)
     ≃ᴳ Ω^S-group k (⊙Trunc ⟨ S k ⟩ (⊙Ω (⊙Susp (de⊙ X))))
  iso = Ω^S-group-emap k ⊙eq

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Equality.Setoid directly.
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid)

module Data.List.Relation.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where

open import Data.List.Relation.Binary.Equality.Setoid S public

{-# WARNING_ON_IMPORT
"Data.List.Relation.Equality.Setoid was deprecated in v1.0.
Use Data.List.Relation.Binary.Equality.Setoid instead."
#-}


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

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

data ⊥ : Set where

postulate
  T : Set
  t0 : T
  t1 : T

postulate
  foo : ⊥ → t0 ≡ t1
  {-# REWRITE foo #-}

test : t0 ≡ t1
test = refl


text:
open import Common.Prelude
open import Common.Reflection

data D (A : Set) : Nat → Set where
  d : ∀ {n} → A → D A n

term : Term
term = con (quote d) (hArg (def (quote Nat) []) ∷ vArg (con (quote zero) []) ∷ [])

-- There was a bug where extra implicit arguments were inserted for the parameters, resulting in
-- the unquoted value 'd {_} {Nat} zero' instead of 'd {Nat} zero'.
value : D Nat zero
value = unquote (give term)


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

module Data.Empty.Base where

open import Cubical.Data.Empty using (⊥; ⊥-elim; isProp⊥) public
open import Level

infix 4.5 ¬_
¬_ : Type a → Type a
¬ A = A → ⊥

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Andreas, 2016-06-20
-- Issue #1653 reported by Jesper
-- Fixed by Ulf's AIM XXIII code sprint "instantiating module parameters"

open import Common.Equality

module _ (A : Set₁) where

  -- Matching on refl works with new instantiateable module parameters.

  test : A ≡ Set → Set₁
  test refl = A

  -- Case splitting thus should also work.

  foo : A ≡ Set → Set₁
  foo e = {!e!} -- C-c C-c


text:
open import Algebra.Apartness using (HeytingField)

module Data.Real.Abstract.Bundles
  c ℓ₁ ℓ₂ r
  where

open import Relation.Binary using (Rel)
open import Data.Real.Abstract.Structures
open import Level using (_⊔_; suc)

record OrderedHeytingField : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ ⊔ r)) where
  field
    f : HeytingField c ℓ₁ ℓ₂

  open HeytingField f public

  field
    _<_ : Rel Carrier r
    isOrderedHeytingField : IsOrderedHeytingField f _<_

record ArchimedanHeytingField : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ ⊔ r)) where
  field
    f : HeytingField c ℓ₁ ℓ₂

  open HeytingField f public

  field
    _<_ : Rel Carrier r
    isArchimedanHeytingField : IsArchimedanHeytingField f _<_

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


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

open import Cubical.Foundations.Everything hiding (_⁻¹)

open import Cubical.HITs.Ints.QuoInt as ℤ using (ℤ; Sign; signed; pos; neg; posneg; sign)
open import Cubical.HITs.SetQuotients as SetQuotient using () renaming (_/_ to _//_)

open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc)
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Sigma

open import Cubical.Data.Sum
open import Cubical.Relation.Nullary

open import Cubical.HITs.Rationals.QuoQ.Base

ℚ-cancelˡ : ∀ {a b} (c : ℕ₊₁) → [ ℕ₊₁→ℤ c ℤ.· a / c ·₊₁ b ] ≡ [ a / b ]
ℚ-cancelˡ {a} {b} c = eq/ _ _
  (cong (ℤ._· ℕ₊₁→ℤ b) (ℤ.·-comm (ℕ₊₁→ℤ c) a) ∙ sym (ℤ.·-assoc a (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)))

ℚ-cancelʳ : ∀ {a b} (c : ℕ₊₁) → [ a ℤ.· ℕ₊₁→ℤ c / b ·₊₁ c ] ≡ [ a / b ]
ℚ-cancelʳ {a} {b} c = eq/ _ _
  (sym (ℤ.·-assoc a (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)) ∙ cong (a ℤ.·_) (ℤ.·-comm (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)))

-- useful functions for defining operations on ℚ

onCommonDenom :
  (g : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ)
  (g-eql : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
           → ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) ≡ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)))
  (g-eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
           → (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d)
  → ℚ → ℚ → ℚ
onCommonDenom g g-eql g-eqr = SetQuotient.rec2 isSetℚ
  (λ { (a , b) (c , d) → [ g (a , b) (c , d) / b ·₊₁ d ] })
  (λ { (a , b) (c , d) (e , f) p → eql (a , b) (c , d) (e , f) p })
  (λ { (a , b) (c , d) (e , f) p → eqr (a , b) (c , d) (e , f) p })
  where eql : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
              → [ g (a , b) (e , f) / b ·₊₁ f ] ≡ [ g (c , d) (e , f) / d ·₊₁ f ]
        eql (a , b) (c , d) (e , f) p =
          [ g (a , b) (e , f) / b ·₊₁ f ]
            ≡⟨ sym (ℚ-cancelˡ d) ⟩
          [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / d ·₊₁ (b ·₊₁ f) ]
            ≡[ i ]⟨ [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / ·₊₁-assoc d b f i ] ⟩
          [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / (d ·₊₁ b) ·₊₁ f ]
            ≡[ i ]⟨ [ g-eql (a , b) (c , d) (e , f) p i / ·₊₁-comm d b i ·₊₁ f ] ⟩
          [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / (b ·₊₁ d) ·₊₁ f ]
            ≡[ i ]⟨ [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / ·₊₁-assoc b d f (~ i) ] ⟩
          [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / b ·₊₁ (d ·₊₁ f) ]
            ≡⟨ ℚ-cancelˡ b ⟩
          [ g (c , d) (e , f) / d ·₊₁ f ] ∎
        eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
             → [ g (a , b) (c , d) / b ·₊₁ d ] ≡ [ g (a , b) (e , f) / b ·₊₁ f ]
        eqr (a , b) (c , d) (e , f) p =
          [ g (a , b) (c , d) / b ·₊₁ d ]
            ≡⟨ sym (ℚ-cancelʳ f) ⟩
          [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / (b ·₊₁ d) ·₊₁ f ]
            ≡[ i ]⟨ [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / ·₊₁-assoc b d f (~ i) ] ⟩
          [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / b ·₊₁ (d ·₊₁ f) ]
            ≡[ i ]⟨ [ g-eqr (a , b) (c , d) (e , f) p i / b ·₊₁ ·₊₁-comm d f i ] ⟩
          [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / b ·₊₁ (f ·₊₁ d) ]
            ≡[ i ]⟨ [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / ·₊₁-assoc b f d i ] ⟩
          [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / (b ·₊₁ f) ·₊₁ d ]
            ≡⟨ ℚ-cancelʳ d ⟩
          [ g (a , b) (e , f) / b ·₊₁ f ] ∎

onCommonDenomSym :
  (g : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ)
  (g-sym : ∀ x y → g x y ≡ g y x)
  (g-eql : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
           → ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) ≡ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)))
  → ℚ → ℚ → ℚ
onCommonDenomSym g g-sym g-eql = onCommonDenom g g-eql q-eqr
  where q-eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
                → (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d
        q-eqr (a , b) (c , d) (e , f) p =
          (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡[ i ]⟨ ℤ.·-comm (g-sym (a , b) (c , d) i) (ℕ₊₁→ℤ f) i ⟩
          ℕ₊₁→ℤ f ℤ.· (g (c , d) (a , b)) ≡⟨ g-eql (c , d) (e , f) (a , b) p ⟩
          ℕ₊₁→ℤ d ℤ.· (g (e , f) (a , b)) ≡[ i ]⟨ ℤ.·-comm (ℕ₊₁→ℤ d) (g-sym (e , f) (a , b) i) i ⟩
          (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d ∎

onCommonDenomSym-comm : ∀ {g} g-sym {g-eql} (x y : ℚ)
                        → onCommonDenomSym g g-sym g-eql x y ≡
                          onCommonDenomSym g g-sym g-eql y x
onCommonDenomSym-comm g-sym = SetQuotient.elimProp2 (λ _ _ → isSetℚ _ _)
  (λ { (a , b) (c , d) i → [ g-sym (a , b) (c , d) i / ·₊₁-comm b d i ] })

-- basic arithmetic operations on ℚ

infixl 6 _+_
infixl 7 _·_

private
  lem₁ : ∀ a b c d e (p : a ℤ.· b ≡ c ℤ.· d) → b ℤ.· (a ℤ.· e) ≡ d ℤ.· (c ℤ.· e)
  lem₁ a b c d e p =   ℤ.·-assoc b a e
                     ∙ cong (ℤ._· e) (ℤ.·-comm b a ∙ p ∙ ℤ.·-comm c d)
                     ∙ sym (ℤ.·-assoc d c e)

  lem₂ : ∀ a b c → a ℤ.· (b ℤ.· c) ≡ c ℤ.· (b ℤ.· a)
  lem₂ a b c =   cong (a ℤ.·_) (ℤ.·-comm b c) ∙ ℤ.·-assoc a c b
               ∙ cong (ℤ._· b) (ℤ.·-comm a c) ∙ sym (ℤ.·-assoc c a b)
               ∙ cong (c ℤ.·_) (ℤ.·-comm a b)

_+_ : ℚ → ℚ → ℚ
_+_ = onCommonDenomSym
  (λ { (a , b) (c , d) → a ℤ.· (ℕ₊₁→ℤ d) ℤ.+ c ℤ.· (ℕ₊₁→ℤ b) })
  (λ { (a , b) (c , d) → ℤ.+-comm (a ℤ.· (ℕ₊₁→ℤ d)) (c ℤ.· (ℕ₊₁→ℤ b)) })
  (λ { (a , b) (c , d) (e , f) p →
    ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ b)
      ≡⟨ sym (ℤ.·-distribˡ (ℕ₊₁→ℤ d) (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b)) ⟩
    ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f) ℤ.+ ℕ₊₁→ℤ d ℤ.· (e ℤ.· ℕ₊₁→ℤ b)
      ≡[ i ]⟨ lem₁ a (ℕ₊₁→ℤ d) c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) p i ℤ.+ lem₂ (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ b) i ⟩
    ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f) ℤ.+ ℕ₊₁→ℤ b ℤ.· (e ℤ.· ℕ₊₁→ℤ d)
      ≡⟨ ℤ.·-distribˡ (ℕ₊₁→ℤ b) (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) ⟩
    ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d) ∎ })

+-comm : ∀ x y → x + y ≡ y + x
+-comm = onCommonDenomSym-comm
  (λ { (a , b) (c , d) → ℤ.+-comm (a ℤ.· (ℕ₊₁→ℤ d)) (c ℤ.· (ℕ₊₁→ℤ b)) })

+-identityˡ : ∀ x → 0 + x ≡ x
+-identityˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
  (λ { (a , b) i → [ ℤ.·-identityʳ a i / ·₊₁-identityˡ b i ] })

+-identityʳ : ∀ x → x + 0 ≡ x
+-identityʳ x = +-comm x _ ∙ +-identityˡ x

+-assoc : ∀ x y z → x + (y + z) ≡ (x + y) + z
+-assoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
  (λ { (a , b) (c , d) (e , f) i → [ eq a (ℕ₊₁→ℤ b) c (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ f) i / ·₊₁-assoc b d f i ] })
  where eq₁ : ∀ a b c → (a ℤ.· b) ℤ.· c ≡ a ℤ.· (c ℤ.· b)
        eq₁ a b c = sym (ℤ.·-assoc a b c) ∙ cong (a ℤ.·_) (ℤ.·-comm b c)
        eq₂ : ∀ a b c → (a ℤ.· b) ℤ.· c ≡ (a ℤ.· c) ℤ.· b
        eq₂ a b c = eq₁ a b c ∙ ℤ.·-assoc a c b

        eq : ∀ a b c d e f → Path ℤ _ _
        eq a b c d e f =
          a ℤ.· (d ℤ.· f) ℤ.+ (c ℤ.· f ℤ.+ e ℤ.· d) ℤ.· b
            ≡[ i ]⟨ a ℤ.· (d ℤ.· f) ℤ.+ ℤ.·-distribʳ (c ℤ.· f) (e ℤ.· d) b (~ i) ⟩
          a ℤ.· (d ℤ.· f) ℤ.+ ((c ℤ.· f) ℤ.· b ℤ.+ (e ℤ.· d) ℤ.· b)
            ≡[ i ]⟨ ℤ.+-assoc (ℤ.·-assoc a d f i) (eq₂ c f b i) (eq₁ e d b i) i ⟩
          ((a ℤ.· d) ℤ.· f ℤ.+ (c ℤ.· b) ℤ.· f) ℤ.+ e ℤ.· (b ℤ.· d)
            ≡[ i ]⟨ ℤ.·-distribʳ (a ℤ.· d) (c ℤ.· b) f i ℤ.+ e ℤ.· (b ℤ.· d) ⟩
          (a ℤ.· d ℤ.+ c ℤ.· b) ℤ.· f ℤ.+ e ℤ.· (b ℤ.· d) ∎

_·_ : ℚ → ℚ → ℚ
_·_ = onCommonDenomSym
  (λ { (a , _) (c , _) → a ℤ.· c })
  (λ { (a , _) (c , _) → ℤ.·-comm a c })
  (λ { (a , b) (c , d) (e , _) p → lem₁ a (ℕ₊₁→ℤ d) c (ℕ₊₁→ℤ b) e p })

·-comm : ∀ x y → x · y ≡ y · x
·-comm = onCommonDenomSym-comm (λ { (a , _) (c , _) → ℤ.·-comm a c })

·-identityˡ : ∀ x → 1 · x ≡ x
·-identityˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
  (λ { (a , b) i → [ ℤ.·-identityˡ a i / ·₊₁-identityˡ b i ] })

·-identityʳ : ∀ x → x · 1 ≡ x
·-identityʳ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
  (λ { (a , b) i → [ ℤ.·-identityʳ a i / ·₊₁-identityʳ b i ] })

·-zeroˡ : ∀ x → 0 · x ≡ 0
·-zeroˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
  (λ { (a , b) → (λ i → [ p a b i / 1 ·₊₁ b ]) ∙ ℚ-cancelʳ b })
  where p : ∀ a b → 0 ℤ.· a ≡ 0 ℤ.· ℕ₊₁→ℤ b
        p a b = ℤ.·-zeroˡ {ℤ.spos} a ∙ sym (ℤ.·-zeroˡ {ℤ.spos} (ℕ₊₁→ℤ b))

·-zeroʳ : ∀ x → x · 0 ≡ 0
·-zeroʳ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
  (λ { (a , b) → (λ i → [ p a b i / b ·₊₁ 1 ]) ∙ ℚ-cancelˡ b })
  where p : ∀ a b → a ℤ.· 0 ≡ ℕ₊₁→ℤ b ℤ.· 0
        p a b = ℤ.·-zeroʳ {ℤ.spos} a ∙ sym (ℤ.·-zeroʳ {ℤ.spos} (ℕ₊₁→ℤ b))

·-assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z
·-assoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
  (λ { (a , b) (c , d) (e , f) i → [ ℤ.·-assoc a c e i / ·₊₁-assoc b d f i ] })

·-distribˡ : ∀ x y z → (x · y) + (x · z) ≡ x · (y + z)
·-distribˡ = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
  (λ { (a , b) (c , d) (e , f) → eq a b c d e f })
  where lem : ∀ {ℓ} {A : Type ℓ} (_·_ : A → A → A)
                (·-comm : ∀ x y → x · y ≡ y · x)
                (·-assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z)
                a c b d
              → (a · c) · (b · d) ≡ (a · (c · d)) · b
        lem _·_ ·-comm ·-assoc a c b d =
          (a · c) · (b · d) ≡[ i ]⟨ (a · c) · ·-comm b d i ⟩
          (a · c) · (d · b) ≡⟨ ·-assoc (a · c) d b ⟩
          ((a · c) · d) · b ≡[ i ]⟨ ·-assoc a c d (~ i) · b ⟩
          (a · (c · d)) · b ∎

        lemℤ   = lem ℤ._·_ ℤ.·-comm ℤ.·-assoc
        lemℕ₊₁ = lem _·₊₁_ ·₊₁-comm ·₊₁-assoc

        eq : ∀ a b c d e f →
               [ (a ℤ.· c) ℤ.· ℕ₊₁→ℤ (b ·₊₁ f) ℤ.+ (a ℤ.· e) ℤ.· ℕ₊₁→ℤ (b ·₊₁ d)
                 / (b ·₊₁ d) ·₊₁ (b ·₊₁ f) ]
             ≡ [ a ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d)
                / b ·₊₁ (d ·₊₁ f) ]
        eq a b c d e f =
          (λ i → [ lemℤ a c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) i ℤ.+ lemℤ a e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) i
                   / lemℕ₊₁ b d b f i ]) ∙
          (λ i → [ ℤ.·-distribʳ (a ℤ.· (c ℤ.· ℕ₊₁→ℤ f)) (a ℤ.· (e ℤ.· ℕ₊₁→ℤ d)) (ℕ₊₁→ℤ b) i
                   / (b ·₊₁ (d ·₊₁ f)) ·₊₁ b ]) ∙
          ℚ-cancelʳ {a ℤ.· (c ℤ.· ℕ₊₁→ℤ f) ℤ.+ a ℤ.· (e ℤ.· ℕ₊₁→ℤ d)} {b ·₊₁ (d ·₊₁ f)} b ∙
          (λ i → [ ℤ.·-distribˡ a (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) i
                   / b ·₊₁ (d ·₊₁ f) ])

·-distribʳ : ∀ x y z → (x · z) + (y · z) ≡ (x + y) · z
·-distribʳ x y z = (λ i → ·-comm x z i + ·-comm y z i) ∙ ·-distribˡ z x y ∙ ·-comm z (x + y)

-_ : ℚ → ℚ
- x = -1 · x

negate-invol : ∀ x → - - x ≡ x
negate-invol x = ·-assoc -1 -1 x ∙ ·-identityˡ x

negateEquiv : ℚ ≃ ℚ
negateEquiv = isoToEquiv (iso -_ -_ negate-invol negate-invol)

negateEq : ℚ ≡ ℚ
negateEq = ua negateEquiv

+-inverseˡ : ∀ x → (- x) + x ≡ 0
+-inverseˡ x = (λ i → (-1 · x) + ·-identityˡ x (~ i)) ∙ ·-distribʳ -1 1 x ∙ ·-zeroˡ x

_-_ : ℚ → ℚ → ℚ
x - y = x + (- y)

+-inverseʳ : ∀ x → x - x ≡ 0
+-inverseʳ x = +-comm x (- x) ∙ +-inverseˡ x

+-injˡ : ∀ x y z → x + y ≡ x + z → y ≡ z
+-injˡ x y z p = sym (q y) ∙ cong ((- x) +_) p ∙ q z
  where q : ∀ y → (- x) + (x + y) ≡ y
        q y = +-assoc (- x) x y ∙ cong (_+ y) (+-inverseˡ x) ∙ +-identityˡ y

+-injʳ : ∀ x y z → x + y ≡ z + y → x ≡ z
+-injʳ x y z p = +-injˡ y x z (+-comm y x ∙ p ∙ +-comm z y)


text:
{-# OPTIONS --copatterns #-}
module CopatternCheckingNYI where

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream

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

alternate : Stream Nat
(     (head alternate)) = zero
(head (tail alternate)) = suc zero
(tail (tail alternate)) = tail alternate

-- does not yet termination-check

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary.Raw

module Cubical.Relation.Binary.Reasoning.Base.Partial
  {a ℓ} {A : Type a} (_∼_ : RawRel A ℓ) (transitive : Transitive _∼_)
  where

open import Cubical.Foundations.Prelude

infix  4 _IsRelatedTo_

infix  2 _∎⟨_⟩
infixr 1 _∼⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_
infixr 1 _≡⟨⟩_
infix  0 begin_

------------------------------------------------------------------------
-- Definition of "related to"

-- This seemingly unnecessary type is used to make it possible to
-- infer arguments even if the underlying equality evaluates.

data _IsRelatedTo_ (x y : A) : Type ℓ where
  relTo : (x∼y : x ∼ y) → x IsRelatedTo y

------------------------------------------------------------------------
-- Reasoning combinators

-- Beginning of a proof

begin_ : ∀ {x y} → x IsRelatedTo y → x ∼ y
begin relTo x∼y = x∼y

-- Standard step with the relation

_∼⟨_⟩_ : ∀ x {y z} → x ∼ y → y IsRelatedTo z → x IsRelatedTo z
_ ∼⟨ x∼y ⟩ relTo y∼z = relTo (transitive x∼y y∼z)

-- Step with a non-trivial propositional equality

_≡⟨_⟩_ : ∀ x {y z} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
_≡⟨_⟩_ x {_} {z} x≡y y∼z = J (λ w _ → w IsRelatedTo z) y∼z (sym x≡y)

-- Step with a flipped non-trivial propositional equality

_≡˘⟨_⟩_ : ∀ x {y z} → y ≡ x → y IsRelatedTo z → x IsRelatedTo z
x ≡˘⟨ y≡x ⟩ y∼z = x ≡⟨ sym y≡x ⟩ y∼z

-- Step with a trivial propositional equality

_≡⟨⟩_ : ∀ x {y} → x IsRelatedTo y → x IsRelatedTo y
_ ≡⟨⟩ x∼y = x∼y

-- Syntax for path definition

≡⟨⟩-syntax : ∀ x {y z : A} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
≡⟨⟩-syntax = _≡⟨_⟩_
infixr 1 ≡⟨⟩-syntax
syntax ≡⟨⟩-syntax x (λ i → B) y = x ≡[ i ]⟨ B ⟩ y

≡˘⟨⟩-syntax : ∀ x {y z : A} → y ≡ x → y IsRelatedTo z → x IsRelatedTo z
≡˘⟨⟩-syntax = _≡˘⟨_⟩_
infixr 1 ≡˘⟨⟩-syntax
syntax ≡˘⟨⟩-syntax x (λ i → B) y = x ≡˘[ i ]⟨ B ⟩ y

-- Termination step

_∎⟨_⟩ : ∀ x → x ∼ x → x IsRelatedTo x
_ ∎⟨ x∼x ⟩ = relTo x∼x