text:
module NativePolyIO where

open import Data.String.Base using (String) public
open import Level

record Unit {α} : Set α where
  constructor unit

{-# HASKELL type AgdaUnit a = () #-}

{-# COMPILED_DATA Unit AgdaUnit () #-}

postulate
  NativeIO : ∀ {ℓ} → Set ℓ → Set ℓ
  nativeReturn : ∀ {a} {A : Set a} → A → NativeIO A
  _native>>=_  : ∀ {a b} {A : Set a} {B : Set b} → NativeIO A → (A → NativeIO B) → NativeIO B

{-# COMPILED_TYPE NativeIO MAlonzo.Code.NativePolyIO.AgdaIO #-}
{-# BUILTIN IO NativeIO #-}

{-# HASKELL type AgdaIO a b = IO b #-}

{-# COMPILED nativeReturn (\_ _ -> return :: a -> IO a) #-}
{-# COMPILED _native>>=_  (\_ _ _ _ ->
                        (>>=) :: IO a -> (a -> IO b) -> IO b) #-}

{-# IMPORT Data.Text.IO #-}

postulate
  nativePutStrLn : ∀ {ℓ} → String → NativeIO (Unit{ℓ})
  nativeGetLine  : NativeIO String

{-# COMPILED nativePutStrLn (\ _ s -> Data.Text.IO.putStrLn s) #-}
{-# COMPILED nativeGetLine  Data.Text.IO.getLine #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Products of nullary relations
------------------------------------------------------------------------

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

module Relation.Nullary.Product where

open import Data.Bool.Base
open import Data.Product
open import Function
open import Level
open import Relation.Nullary.Reflects
open import Relation.Nullary

private
  variable
    p q : Level
    P : Set p
    Q : Set q

------------------------------------------------------------------------
-- Some properties which are preserved by _×_.

infixr 2 _×-reflects_ _×-dec_

_×-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq →
                           Reflects (P × Q) (bp ∧ bq)
ofʸ  p ×-reflects ofʸ  q = ofʸ (p , q)
ofʸ  p ×-reflects ofⁿ ¬q = ofⁿ (¬q ∘ proj₂)
ofⁿ ¬p ×-reflects _      = ofⁿ (¬p ∘ proj₁)

_×-dec_ : Dec P → Dec Q → Dec (P × Q)
does  (p? ×-dec q?) = does p? ∧ does q?
proof (p? ×-dec q?) = proof p? ×-reflects proof q?

ext: agda


text:
module Issue512 where

postulate
  Level : Set

{-# BUILTIN LEVEL Level #-}

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

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

data A : Set where
  a b : A

proof : a ≡ a
proof = refl

f : A → A → A
f x y rewrite proof = ? -- gave error below (now complains about LEVELZERO instead of STRING)

{-
{-
No binding for builtin thing STRING, use {-# BUILTIN STRING name
#-} to bind it to 'name'
when checking that the type of the generated with function
(w : A) → _≡_ {"Max []"} {A} w w → (x y : A) → A is well-formed
-}
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Operations.Stateful where

import      Data.Bool as B
open import Data.Fin
open import Data.Nat
open import Data.Vec hiding (head; tail)
open import Function
open import Relation.Binary.PropositionalEquality

open import Eval
open import Operations.Combinatorial
open import Types

alternator : Closed 𝔹 → Closed (ℂ 𝔹)
alternator x = reg x (lam (pair (not ∙ var zero refl) (var zero refl)))

constant : ∀ {τ} → Closed τ → Closed (ℂ τ)
constant x = reg x (lam (pair (var zero refl) (var zero refl)))

max_stars_repo_name: bens/hwlc

max_issues_repo_name: bens/hwlc

max_forks_repo_name: bens/hwlc


text:
module Categories.Initial where

open import Library
open import Categories
open import Categories.Sets
open Cat

record Init {a b} (C : Cat {a}{b})(I : Obj C) : Set (a ⊔ b) where
  constructor init
  field i : ∀{X} → Hom C I X
        law : ∀{X}{f : Hom C I X} → i {X} ≅ f

ZeroSet : Init Sets ⊥
ZeroSet = record {i = λ(); law = ext λ()}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
-- Andreas, 2015-07-07 continuation of issue 665

-- Jesper, 2015-12-18 some of these don't work anymore with the new unifier,
-- but a few others that weren't accepted are now.

{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.with.strip:10 #-}
-- {-# OPTIONS -v tc.with.strip:60 -v tc.lhs:20 -v tc.lhs.unify:20 #-}

postulate
  C : Set
  anything : C

record I : Set where
  constructor c
  field
    {f} : C

data Wrap : (i : I) → Set where
  wrap : ∀ {i} → Wrap i

-- Test 0: first argument not given

test0 : ∀ {j} → Wrap j → C
test0 wrap with anything
test0 wrap | z = z

test0a : ∀ {j} → Wrap j → C
test0a (wrap {c {x}}) with anything
test0a  wrap | z = z

test0b : ∀ {j} → Wrap j → C
test0b (wrap {c {_}}) with anything
test0b wrap | z = z

test0c : ∀ {j} → Wrap j → C
test0c (wrap {c}) with anything
test0c wrap | z = z

test0d : ∀ {j} → Wrap j → C
test0d (wrap {c {._}}) with anything
test0d  wrap | z = z

test0e : ∀ {j} → Wrap j → C
test0e (wrap .{c}) with anything
test0e  wrap | z = z

test0f : ∀ {j} → Wrap j → C
test0f (wrap .{c {_}}) with anything
test0f  wrap | z = z

test00 : ∀ {j} → Wrap j → C
test00 wrap with anything
test00 {.c} wrap | z = z

test00a : ∀ {j} → Wrap j → C
test00a (wrap {c {x}}) with anything
test00a {.c} wrap | z = z

test00b : ∀ {j} → Wrap j → C
test00b (wrap {c {_}}) with anything
test00b {.c} wrap | z = z

test00c : ∀ {j} → Wrap j → C
test00c (wrap {c}) with anything
test00c {.c} wrap | z = z

test00d : ∀ {j} → Wrap j → C
test00d (wrap {c {._}}) with anything
test00d {.c} wrap | z = z

test00e : ∀ {j} → Wrap j → C
test00e (wrap .{c}) with anything
test00e {.c} wrap | z = z

test00f : ∀ {j} → Wrap j → C
test00f (wrap .{c {_}}) with anything
test00f {.c} wrap | z = z

test000 : ∀ {j} → Wrap j → C
test000 wrap with anything
test000 .{c {_}} wrap | z = z

test000a : ∀ {j} → Wrap j → C
test000a (wrap {c {x}}) with anything
test000a .{c {_}} wrap | z = z

test000b : ∀ {j} → Wrap j → C
test000b (wrap {c {_}}) with anything
test000b .{c {_}} wrap | z = z

test000c : ∀ {j} → Wrap j → C
test000c (wrap {c}) with anything
test000c .{c {_}} wrap | z = z

test000d : ∀ {j} → Wrap j → C
test000d (wrap {c {._}}) with anything
test000d .{c {_}} wrap | z = z

test000e : ∀ {j} → Wrap j → C
test000e (wrap .{c}) with anything
test000e .{c {_}} wrap | z = z

test000f : ∀ {j} → Wrap j → C
test000f (wrap .{c {_}}) with anything
test000f .{c {_}} wrap | z = z

-- Test 1: first argument is dot pattern

test1a : ∀ {j} → Wrap j → C
test1a .{c} (wrap {c {x}}) with anything
test1a .{c} wrap | z = z

test1b : ∀ {j} → Wrap j → C
test1b .{c} (wrap {c {_}}) with anything
test1b .{c} wrap | z = z

test1c : ∀ {j} → Wrap j → C
test1c .{c} (wrap {c}) with anything
test1c .{c} wrap | z = z

test11a : ∀ {j} → Wrap j → C
test11a .{c} (wrap {c {x}}) with anything
test11a wrap | z = z

test11b : ∀ {j} → Wrap j → C
test11b .{c} (wrap {c {_}}) with anything
test11b wrap | z = z

test11c : ∀ {j} → Wrap j → C
test11c .{c} (wrap {c}) with anything
test11c wrap | z = z

test111a : ∀ {j} → Wrap j → C
test111a (wrap {c {x}}) with anything
test111a .{c} wrap | z = z

test111b : ∀ {j} → Wrap j → C
test111b (wrap {c {_}}) with anything
test111b .{c} wrap | z = z

test111c : ∀ {j} → Wrap j → C
test111c (wrap {c}) with anything
test111c .{c} wrap | z = z

-- Test 2: First argument is record pattern

test2a : ∀ {j} → Wrap j → C
test2a {c} wrap with anything
test2a {c} wrap | z = z

test2b : ∀ {j} → Wrap j → C
test2b {c} wrap with anything
test2b wrap | z = z

test2c : ∀ {j} → Wrap j → C
test2c {c} (wrap {c}) with anything
test2c {c} wrap | z = z

test2d : ∀ {j} → Wrap j → C
test2d {c} (wrap {c}) with anything
test2d wrap | z = z

test2e : ∀ {j} → Wrap j → C
test2e {c} (wrap {c {._}}) with anything
test2e {c} wrap | z = z

test2f : ∀ {j} → Wrap j → C
test2f {c} (wrap {c {._}}) with anything
test2f wrap | z = z

test2g : ∀ {j} → Wrap j → C
test2g {c} (wrap {c {x}}) with anything
test2g {c} wrap | z = z

test2h : ∀ {j} → Wrap j → C
test2h {c} (wrap {c {x}}) with anything
test2h wrap | z = z

test2i : ∀ {j} → Wrap j → C
test2i {c} (wrap {c {_}}) with anything
test2i {c} wrap | z = z

test2j : ∀ {j} → Wrap j → C
test2j {c} (wrap {c {_}}) with anything
test2j wrap | z = z

-- Test 3: First argument is record of dot pattern, second is record pattern

test3a : ∀ {j} → Wrap j → C
test3a {c {._}} wrap with anything
test3a {c {._}} wrap | z = z

test3b : ∀ {j} → Wrap j → C
test3b {c {._}} wrap with anything
test3b wrap | z = z

test3c : ∀ {j} → Wrap j → C
test3c {c {._}} (wrap {c}) with anything
test3c {c {._}} wrap | z = z

test3d : ∀ {j} → Wrap j → C
test3d {c {._}} (wrap {c}) with anything
test3d wrap | z = z

test3e : ∀ {j} → Wrap j → C
test3e {c {._}} (wrap {c {._}}) with anything
test3e {c {._}} wrap | z = z

test3f : ∀ {j} → Wrap j → C
test3f {c {._}} (wrap {c {._}}) with anything
test3f wrap | z = z

test3g : ∀ {j} → Wrap j → C
test3g {c {_}} (wrap {c {x}}) with anything
test3g {c {_}} wrap | z = z

test3h : ∀ {j} → Wrap j → C
test3h {c {_}} (wrap {c {x}}) with anything
test3h wrap | z = z

test3i : ∀ {j} → Wrap j → C
test3i {c {_}} (wrap {c {_}}) with anything
test3i {c {_}} wrap | z = z

test3j : ∀ {j} → Wrap j → C
test3j {c {_}} (wrap {c {_}}) with anything
test3j wrap | z = z

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 Level
open import Categories.Category using () renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal using (Monoidal)

module Categories.Bicategory.Instance.EnrichedCats
  {o ℓ e} {V : Setoid-Category o ℓ e} (M : Monoidal V) (v : Level) where

-- The 2-category of V-enriched categories

open import Data.Product as Prod using (_,_)

open import Categories.Bicategory using (Bicategory)
open import Categories.Category.Construction.EnrichedFunctors M
open import Categories.Enriched.Category M
open import Categories.Enriched.Functor M renaming (id to idF)
open import Categories.Enriched.NaturalTransformation M hiding (id)
import Categories.Enriched.NaturalTransformation.NaturalIsomorphism M as NI
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Construction.Constant using (const)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)

private
  module V = Setoid-Category V
  module UnderlyingReasoning {c} (C : Category c) where
    open Underlying C public hiding (id)
    open HomReasoning public
  open NaturalTransformation
  open NI.NaturalIsomorphism

  -- Aliases used to shorten some proof expressions

  module UF = UnderlyingFunctor
  infixr 14 _$₀_ _$₁_
  _$₀_ = UF.F₀
  _$₁_ = UF.F₁

-- The bicategory of V-enriched categories, functors and natural
-- transformations.
--
-- Note that all the equational reasoning happens in the underlying
-- (ordinary) categories!

EnrichedCats : Bicategory (ℓ ⊔ e ⊔ v) (ℓ ⊔ e ⊔ v) (e ⊔ v) (o ⊔ ℓ ⊔ e ⊔ suc v)
EnrichedCats = record
  { enriched = record
    { Obj = Category v
    ; hom = EnrichedFunctors
    ; id  = const idF
    ; ⊚   = ⊚
    ; ⊚-assoc = λ {_ _ C D} →
      let module C = Underlying C
          module D = Underlying D
          open UnderlyingReasoning D
      in niHelper record
        { η       = λ { ((F , G) , H) → from (NI.associator {F = F} {G} {H}) }
        ; η⁻¹     = λ { ((F , G) , H) → to   (NI.associator {F = F} {G} {H}) }
        ; commute = λ { {(_ , G₁) , H₁} {(F₂ , G₂) , _} ((α , β) , γ) {X} →
          begin
            D.id ∘ (F₂ ∘F G₂) $₁ γ [ X ] ∘ F₂ $₁ β [ H₁ $₀ X ] ∘
            α [ G₁ $₀ H₁ $₀ X ]
          ≈⟨ identityˡ ○ ⟺ assoc ⟩
            ((F₂ ∘F G₂) $₁ γ [ X ] ∘ F₂ $₁ β [ H₁ $₀ X ]) ∘ α [ G₁ $₀ H₁ $₀ X ]
          ≈⟨ V.assoc ⟩∘⟨refl ⟩∘⟨refl ⟩
            (F₂ $₁ G₂ $₁ γ [ X ] ∘ F₂ $₁ β [ H₁ $₀ X ]) ∘ α [ G₁ $₀ H₁ $₀ X ]
          ≈˘⟨ UF.homomorphism F₂ ⟩∘⟨refl ⟩
            F₂ $₁ (G₂ $₁ γ [ X ] C.∘ β [ H₁ $₀ X ]) ∘ α [ G₁ $₀ H₁ $₀ X ]
          ≈˘⟨ identityʳ ⟩
            (F₂ $₁ (G₂ $₁ γ [ X ] C.∘ β [ H₁ $₀ X ]) ∘ α [ G₁ $₀ H₁ $₀ X ]) ∘
            D.id
          ∎ }
        ; iso = λ{ ((F , G) , H) → iso (NI.associator {F = F} {G} {H}) }
        }
    ; unitˡ = λ {A B} →
      let module A = Underlying A
          module B = Underlying B
          open UnderlyingReasoning B
      in niHelper record
        { η       = λ _ → from NI.unitorˡ
        ; η⁻¹     = λ _ → to   NI.unitorˡ
        ; commute = λ { {_ , F} {_ , G} (_ , α) {X} →
          begin
            B.id ∘ (V.id V.∘ α [ X ]) ∘ B.id   ≈⟨ identityˡ ⟩
            (V.id V.∘ α [ X ]) ∘ B.id          ≈⟨ V.identityˡ ⟩∘⟨refl ⟩
            α [ X ] ∘ B.id                     ∎ }
        ; iso = λ _ → iso NI.unitorˡ
        }
    ; unitʳ = λ {A B} →
      let module A = Underlying A
          module B = Underlying B
          open UnderlyingReasoning B
      in niHelper record
        { η       = λ _ → from NI.unitorʳ
        ; η⁻¹     = λ _ → to   NI.unitorʳ
        ; commute = λ{ {_} {G , _} (α , _) {X} →
          begin
            B.id ∘ G $₁ A.id ∘ α [ X ]  ≈⟨ identityˡ ⟩
            G $₁ A.id ∘ α [ X ]         ≈⟨ UF.identity G ⟩∘⟨refl ⟩
            B.id ∘ α [ X ]              ≈⟨ identityˡ ○ ⟺ identityʳ ⟩
            α [ X ] ∘ B.id              ∎ }
        ; iso     = λ _ → iso NI.unitorʳ
        }
    }
  ; triangle = λ {_ B C _ G} →
    let module B = Underlying B
        module C = Underlying C
        open UnderlyingReasoning C
    in begin
      (G $₁ B.id ∘ C.id) ∘ C.id   ≈⟨ identityʳ ⟩
      G $₁ B.id ∘ C.id            ∎
  ; pentagon = λ {_ B _ D E _ G H I} →
    let module B  = Category B
        module D  = Category D
        module E  = Category E
        open UnderlyingReasoning E
    in begin
      (I $₁ D.id ∘ E.id) ∘ E.id ∘ (I ∘F H ∘F G) $₁ B.id ∘ E.id
    ≈⟨ identityʳ ⟩∘⟨ (identityˡ ○ identityʳ) ⟩
      I $₁ D.id ∘ (I ∘F H ∘F G) $₁ B.id
    ≈⟨ UF.identity I ⟩∘⟨ UF.identity (I ∘F H ∘F G) ⟩
      E.id ∘ E.id
    ∎
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)-- ¬ᵗ_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Function.Base using (_∋_; _$_; it; typeOf)
open import Cubical.Foundations.Logic renaming
  ( inl to inlᵖ
  ; inr to inrᵖ
  ; _⇒_ to infixr 0 _⇒_                  -- shifting by -6
  ; _⇔_ to infixr -2 _⇔_                 --
  ; ∃[]-syntax  to infix -4 ∃[]-syntax   --
  ; ∃[∶]-syntax to infix -4 ∃[∶]-syntax  --
  ; ∀[∶]-syntax to infix -4 ∀[∶]-syntax  --
  ; ∀[]-syntax  to infix -4 ∀[]-syntax   --
  )
-- open import Cubical.Data.Unit.Base using (Unit)
open import Cubical.HITs.PropositionalTruncation.Base -- ∣_∣

open import Utils
open import MoreLogic.Reasoning
open import MoreLogic.Definitions renaming
  ( _ᵗ⇒_ to infixr 0 _ᵗ⇒_
  ; ∀ᵖ[∶]-syntax  to infix -4 ∀ᵖ[∶]-syntax
  ; ∀ᵖ〚∶〛-syntax  to infix -4 ∀ᵖ〚∶〛-syntax
  ; ∀ᵖ!〚∶〛-syntax to infix -4 ∀ᵖ!〚∶〛-syntax
  ; ∀〚∶〛-syntax   to infix -4 ∀〚∶〛-syntax
  ; Σᵖ[]-syntax   to infix -4 Σᵖ[]-syntax
  ; Σᵖ[∶]-syntax  to infix -4 Σᵖ[∶]-syntax
  ) hiding (≡ˢ-syntax)
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Consequences
open import MorePropAlgebra.Bundles

module MorePropAlgebra.Booij2020 where

module Chapter4 {ℓ ℓ'} (assumptions : AlmostPartiallyOrderedField {ℓ} {ℓ'}) where
  open import MorePropAlgebra.Properties.AlmostPartiallyOrderedField assumptions
  open AlmostPartiallyOrderedField assumptions renaming (Carrier to F; _-_ to _-_) -- atlernative to module telescope

  Item-1  = ∀[ x ] ∀[ y ]                                 x ≤ y ⇔ ¬(y < x)                          -- (definition of _≤_)
  Item-2  = ∀[ x ] ∀[ y ]                                 x # y ⇔ [ <-asym x y ] (x < y) ⊎ᵖ (y < x) -- (definition of _#_)
  Item-3  = ∀[ x ] ∀[ y ] ∀[ z ]                          x ≤ y ⇔ x + z ≤ y + z                     -- +-creates-≤
  Item-4  = ∀[ x ] ∀[ y ] ∀[ z ]                          x < y ⇔ x + z < y + z                     -- +-creates-<
  Item-5  = ∀[ x ] ∀[ y ]        0f < x + y          ⇒ (0f < x) ⊔ (0f < y)                          -- 0<-reflects-+
  Item-6  = ∀[ x ] ∀[ y ] ∀[ z ]  x < y     ⇒  y ≤ z ⇒    x     <     z                             -- <-≤-trans
  Item-7  = ∀[ x ] ∀[ y ] ∀[ z ]  x ≤ y     ⇒  y < z ⇒    x     <     z                             -- ≤-<-trans
  Item-8  = ∀[ x ] ∀[ y ] ∀[ z ]  x ≤ y     ⇒ 0f ≤ z ⇒    x · z ≤ y · z                             -- ·-preserves-≤
  Item-9  = ∀[ x ] ∀[ y ] ∀[ z ] 0f < z     ⇒            (x < y ⇔ x · z < y · z)                    -- ·-creates-<
  Item-10 =                      0f < 1f                                                            -- 0<1

  item-1 : ∀ x y   → [ x ≤ y ⇔                          ¬(y < x) ]; _ = [ Item-1 ] ∋ item-1
  item-2 : ∀ x y   → [ x # y ⇔ [ <-asym x y ] (x < y) ⊎ᵖ (y < x) ]; _ = [ Item-2 ] ∋ item-2

  item-6 : ∀ x y z → [ x < y ⇒ y ≤ z ⇒ x < z ]; _ : [ Item-6 ]; _ = item-6
  item-7 : ∀ x y z → [ x ≤ y ⇒ y < z ⇒ x < z ]; _ : [ Item-7 ]; _ = item-7

  --  1. x ≤ y ⇔ ¬(y < x),
  item-1 _ _ .fst x≤y = x≤y -- holds definitionally
  item-1 _ _ .snd x≤y = x≤y

  --  2. x # y ⇔ (x < y) ∨ (y < x)
  item-2 _ _ .fst  x#y        =  x#y -- holds definitionally
  item-2 _ _ .snd [x<y]⊎[y<x] = [x<y]⊎[y<x]

  item-6 = <-≤-trans
  item-7 = ≤-<-trans

  module +-<-ext+·-preserves-<⇒
    (+-<-ext       : [ is-+-<-Extensional _+_ _<_ ])
    (·-preserves-< : [ operation _·_ preserves _<_ when (λ z → 0f < z) ])
    where
    abstract
      +-reflects-<      : ∀ x y z → [           x + z < y + z ⇒     x < y      ]
      +-preserves-<     : ∀ x y z → [               x < y     ⇒ x + z < y + z  ]
      +-creates-<       : ∀ x y z → [               x < y     ⇔ x + z < y + z  ]; _ : [ Item-4  ]; _ = +-creates-<
      +-creates-≤       : ∀ x y z → [               x ≤ y     ⇔ x + z ≤ y + z  ]; _ : [ Item-3  ]; _ = +-creates-≤
      ·-reflects-<      : ∀ x y z → [ 0f < z ⇒ (x · z < y · z ⇒ x < y        ) ]
      ·-creates-<       : ∀ x y z → [ 0f < z ⇒ (    x < y     ⇔ x · z < y · z) ]; _ : [ Item-9  ]; _ = ·-creates-<
      ·-preserves-≤     : ∀ x y z → [  x ≤ y ⇒     0f ≤ z     ⇒ x · z ≤ y · z  ]; _ : [ Item-8  ]; _ = ·-preserves-≤

      0<-reflects-+     : ∀ x y   → [ 0f < x + y ⇒ (0f < x) ⊔ (0f < y)     ]; _ : [ Item-5  ]; _ = 0<-reflects-+

      ⁻¹-preserves-sign : ∀ z z⁻¹ → [ 0f < z ] → z · z⁻¹ ≡ 1f → [ 0f < z⁻¹ ]

      is-0<1            :           [ 0f < 1f ]                             ; _ : [ Item-10 ]; _ = is-0<1

      item-3            : [ Item-3 ]
      item-4            : [ Item-4 ]
      item-5            : [ Item-5 ]
      item-8            : [ Item-8 ]
      item-9            : [ Item-9 ]
      item-10           : [ Item-10 ]

      -- NOTE: just a plain copy of the previous proof
      +-preserves-< a b x = snd (
         a            <  b            ⇒ᵖ⟨ transport (λ i → [ sym (fst (+-identity a)) i < sym (fst (+-identity b)) i ]) ⟩
         a +    0f    <  b +    0f    ⇒ᵖ⟨ transport (λ i → [ a + sym (+-rinv x) i < b + sym (+-rinv x) i ]) ⟩
         a + (x  - x) <  b + (x  - x) ⇒ᵖ⟨ transport (λ i → [ +-assoc a x (- x) i < +-assoc b x (- x) i ]) ⟩
        (a +  x) - x  < (b +  x) - x  ⇒ᵖ⟨ +-<-ext (a + x) (- x) (b + x) (- x) ⟩
        (a + x < b + x) ⊔ (- x < - x) ⇒ᵖ⟨ (λ q → case q as (a + x < b + x) ⊔ (- x < - x) ⇒ a + x < b + x of λ
                                          { (inl a+x<b+x) → a+x<b+x -- somehow ⊥-elim needs a hint in the next line
                                          ; (inr  -x<-x ) → ⊥-elim {A = λ _ → [ a + x < b + x ]} (<-irrefl (- x) -x<-x)
                                          }) ⟩
         a + x < b + x ◼ᵖ)

      +-reflects-< x y z = snd
        ( x + z < y + z              ⇒ᵖ⟨ +-preserves-< _ _ (- z) ⟩
          (x + z) - z  < (y + z) - z ⇒ᵖ⟨ transport (λ i → [ +-assoc x z (- z) (~ i) < +-assoc y z (- z) (~ i) ]) ⟩
          x + (z - z) < y + (z - z)  ⇒ᵖ⟨ transport (λ i → [ x + +-rinv z i < y + +-rinv z i ]) ⟩
          x + 0f < y + 0f            ⇒ᵖ⟨ transport (λ i → [ fst (+-identity x) i < fst (+-identity y) i ]) ⟩
          x < y                      ◼ᵖ)

      --  3. x ≤ y ⇔ x + z ≤ y + z,
      +-creates-≤ x y z .fst = snd ( -- unfold the definition
         x     ≤ y          ⇒ᵖ⟨ (λ z → z) ⟩
        (y     < x     ⇒ ⊥) ⇒ᵖ⟨ (λ f → f ∘ (+-reflects-< y x z) ) ⟩
        (y + z < x + z ⇒ ⊥) ⇒ᵖ⟨ (λ z → z) ⟩
         x + z ≤ y + z      ◼ᵖ) -- refold the definition
      +-creates-≤ x y z .snd = snd (
         x + z ≤ y + z      ⇒ᵖ⟨ (λ z → z) ⟩ -- unfold the definition
        (y + z < x + z ⇒ ⊥) ⇒ᵖ⟨ (λ f p → f (+-preserves-< y x z p)) ⟩ -- just a variant of the above
        (y     < x     ⇒ ⊥) ⇒ᵖ⟨ (λ z → z) ⟩ -- refold the definition
         x     ≤ y          ◼ᵖ)

      item-3 = +-creates-≤

      --  4. x < y ⇔ x + z < y + z,
      +-creates-< x y z .fst = +-preserves-< x y z
      +-creates-< x y z .snd = +-reflects-<  x y z

      item-4 = +-creates-<

      --  5. 0 < x + y ⇒ 0 < x ∨ 0 < y,
      0<-reflects-+ x y = snd (
        (0f      < x + y)   ⇒ᵖ⟨ transport (λ i → [ fst (+-identity 0f) (~ i) < x + y ]) ⟩
        (0f + 0f < x + y)   ⇒ᵖ⟨ +-<-ext 0f 0f x y ⟩
        (0f < x) ⊔ (0f < y) ◼ᵖ)

      item-5 = 0<-reflects-+

      -- --  6. x < y ≤ z ⇒ x < z,
      -- item-6 x y z x<y y≤z = snd (
      --    x      <  y      ⇒ᵖ⟨ +-preserves-< _ _ _ ⟩
      --    x + z  <  y + z  ⇒ᵖ⟨ pathTo⇒ (λ i → x + z < +-comm y z i) ⟩
      --    x + z  <  z + y  ⇒ᵖ⟨ +-<-ext x z z y ⟩
      --   (x < z) ⊔ (z < y) ⇒ᵖ⟨ (λ q → case q as (x < z) ⊔ (z < y) ⇒ (x < z) of λ
      --                         { (inl x<z) → x<z
      --                         ; (inr z<y) → ⊥-elim (y≤z z<y)
      --                         }) ⟩
      --    x < z            ◼ᵖ) x<y
      --
      -- --  7. x ≤ y < z ⇒ x < z,
      -- item-7 x y z x≤y = snd ( -- very similar to the previous one
      --    y      <  z      ⇒ᵖ⟨ +-preserves-< y z x ⟩
      --    y + x  <  z + x  ⇒ᵖ⟨ pathTo⇒ (λ i → +-comm y x i < z + x) ⟩
      --    x + y  <  z + x  ⇒ᵖ⟨ +-<-ext x y z x ⟩
      --   (x < z) ⊔ (y < x) ⇒ᵖ⟨ (λ q → case q as (x < z) ⊔ (y < x) ⇒ (x < z) of λ
      --                         { (inl x<z) → x<z
      --                         ; (inr y<x) → ⊥-elim (x≤y y<x)
      --                         }) ⟩
      --    x < z  ◼ᵖ)

      -- 10. 0f < 1f
      item-10 = is-0<1

      ⁻¹-preserves-sign z z⁻¹ 0<z z·z⁻¹≡1 with snd (·-inv#0 z z⁻¹ z·z⁻¹≡1)
      ... | inl z⁻¹<0 = snd (
        z⁻¹     < 0f     ⇒ᵖ⟨ ·-preserves-< _ _ z 0<z ⟩
        z⁻¹ · z < 0f · z ⇒ᵖ⟨ transport (λ i → [ (·-comm _ _ ∙ z·z⁻¹≡1) i < RingTheory'.0-leftNullifies z i ]) ⟩
        1f      < 0f     ⇒ᵖ⟨ <-trans _ _ _ item-10 ⟩
        0f      < 0f     ⇒ᵖ⟨ <-irrefl _ ⟩
                ⊥        ⇒ᵖ⟨ ⊥-elim ⟩
             0f < z⁻¹    ◼ᵖ) z⁻¹<0
      ... | inr 0<z⁻¹ = 0<z⁻¹

      --  8. x ≤ y ∧ 0 ≤ z ⇒ x z ≤ y z,
      -- For item 8, suppose x ≤ y and 0 ≤ z and yz < xz.
      ·-preserves-≤ x y z x≤y 0≤z y·z<x·z = let
        -- Then 0 < z (x − y) by (†),
        i   = (  y · z            <  x · z                ⇒ᵖ⟨ pathTo⇒ (λ i → ·-comm y z i < ·-comm x z i) ⟩
                 z · y            <  z · x                ⇒ᵖ⟨ +-preserves-< _ _ _ ⟩
                (z · y) - (z · y) < (z · x) - (z ·    y ) ⇒ᵖ⟨ pathTo⇒ (cong₂ _<_ (+-rinv (z · y))
                                                               ( λ i → (z · x) + sym (RingTheory'.-commutesWithRight-· z y) i )) ⟩
                               0f < (z · x) + (z · (- y)) ⇒ᵖ⟨ pathTo⇒ (cong₂ _<_ refl (sym (fst (is-dist z x (- y))))) ⟩ -- [XX]
                               0f <  z · (x - y)          ◼ᵖ) .snd y·z<x·z
        instance z·[x-y]#0 = [ z · (x - y) # 0f ] ∋ inr i
        -- and so, being apart from 0, z (x − y) has a multiplicative inverse w.
        w   = (z · (x - y)) ⁻¹
        ii  : 1f ≡ (z · (x - y)) · w
        ii  = sym (·-rinv _ _)
        -- Hence z itself has a multiplicative inverse w (x − y),
        iii : 1f ≡ z · ((x - y) · w)
        iii = transport (λ i → 1f ≡ ·-assoc z (x - y) w (~ i)) ii
        instance z#0f = [ z # 0f ] ∋ fst (·-inv#0 _ _ (sym iii))
        -- and so 0 < z ∨ z < 0, where the latter case contradicts the assumption 0 ≤ z, so that we have 0 < z.
        instance _    = [ 0f < z ] ∋ case z#0f of λ where
                        (inl z<0) → ⊥-elim (0≤z z<0)
                        (inr 0<z) → 0<z
        -- Now w (x − y) has multiplicative inverse z, so it is apart from 0,
        iv  : [ (x - y) · w # 0f ]
        iv  = snd (·-inv#0 _ _ (sym iii))
        -- that is (0 < w (x − y)) ∨ (w (x − y) < 0).
        in case iv of λ where
          -- By (∗), from 0 < w (x − y) and yz < xz we get yzw (x − y) < xzw (x − y), so y < x, contradicting our assumption that x ≤ y.
          (inr 0<[x-y]·w) → (
             y ·  z                   <  x ·  z                    ⇒ᵖ⟨ ·-preserves-< _ _ _ 0<[x-y]·w ⟩
            (y ·  z) · ((x - y) · w)  < (x ·  z) · ((x - y) · w)   ⇒ᵖ⟨ pathTo⇒ (λ i →
                                                                          (·-assoc y z ((x - y) · w)) (~ i)
                                                                        < (·-assoc x z ((x - y) · w)) (~ i)) ⟩
             y · (z  · ((x - y) · w)) <  x · (z  · ((x - y) · w))  ⇒ᵖ⟨ pathTo⇒ (λ i →
                                                                         y · (iii (~ i)) < x · (iii (~ i))) ⟩
             y · 1f                   <  x · 1f                    ⇒ᵖ⟨ pathTo⇒ (cong₂ _<_
                                                                        (fst (·-identity y)) (fst (·-identity x))) ⟩
             y                        <  x                         ⇒ᵖ⟨ x≤y ⟩
                                      ⊥                            ◼ᵖ) .snd y·z<x·z
          -- In the latter case, from (∗) we get zw (x − y) < 0, i.e.
          -- 1 < 0 which contradicts item 10, so that we have 0 < w (x − y).
          (inl p) → (
                 (x - y) · w      < 0f     ⇒ᵖ⟨ ·-preserves-< _ _ _ it ⟩
                ((x - y) · w) · z < 0f · z ⇒ᵖ⟨ pathTo⇒ (cong₂ _<_ (·-comm _ _) (RingTheory'.0-leftNullifies z)) ⟩
            z · ((x - y) · w)     < 0f     ⇒ᵖ⟨ pathTo⇒ (λ i → iii (~ i) < 0f) ⟩
                               1f < 0f     ⇒ᵖ⟨ <-trans _ _ _  item-10 ⟩
                               0f < 0f     ⇒ᵖ⟨ <-irrefl _ ⟩
                                  ⊥        ◼ᵖ) .snd p

      item-8 = ·-preserves-≤

      --  9. 0 < z ⇒ (x < y ⇔ x z < y z),
      ·-creates-< x y z 0<z .fst = ·-preserves-< x y z 0<z
      -- For the other direction of item 9, assume 0 < z and xz < yz,
      ·-creates-< x y z 0<z .snd x·z<y·z = let
        instance _ = (          x · z  <  y · z            ⇒ᵖ⟨ +-preserves-< _ _ _ ⟩
                     (x · z) - (x · z) < (y · z) - (x · z) ⇒ᵖ⟨ pathTo⇒ (cong₂ _<_ (+-rinv (x · z)) refl) ⟩
                                    0f < (y · z) - (x · z) ◼ᵖ) .snd x·z<y·z
                 _ = [ (y · z) - (x · z) # 0f ] ∋ inr it
        -- so that yz − xz has a multiplicative inverse w,
        w = ((y · z) - (x · z)) ⁻¹
        o = ( (y · z) - (   x  · z) ≡⟨ ( λ i → (y · z) + (RingTheory'.-commutesWithLeft-· x z) (~ i)) ⟩
              (y · z) + ((- x) · z) ≡⟨ sym (snd (is-dist y (- x) z)) ⟩
              (y - x) · z           ∎)
        instance _ = [ (y - x) · z # 0f ] ∋ pathTo⇒ (λ i → o i # 0f) it
        -- and so z itself has multiplicative inverse w (y − x).
        instance _ = (          x · z  <  y · z            ⇒ᵖ⟨ +-preserves-< _ _ _ ⟩
                     (x · z) - (x · z) < (y · z) - (x · z) ⇒ᵖ⟨ pathTo⇒ (cong₂ _<_ (+-rinv (x · z)) refl) ⟩
                                    0f < (y · z) - (x · z) ◼ᵖ) .snd x·z<y·z
                 _ = [ (y · z) - (x · z) # 0f ] ∋ inr it
        1≡z·[w·[y-x]] = (
          1f                      ≡⟨ (λ i → ·-linv ((y · z) - (x · z)) it (~ i)) ⟩
          w · ((y · z) - (x · z)) ≡⟨ (λ i → w · o i) ⟩
          w · ((y - x) · z)       ≡⟨ (λ i → w · ·-comm (y - x) z i ) ⟩
          w · (z · (y - x))       ≡⟨ (λ i → ·-assoc w z (y - x) i) ⟩
          (w · z) · (y - x)       ≡⟨ (λ i → ·-comm w z i · (y - x)) ⟩
          (z · w) · (y - x)       ≡⟨ (λ i → ·-assoc z w (y - x) (~ i)) ⟩
          z · (w · (y - x))       ∎)
        1≡[w·[y-x]]·z : 1f ≡ (w · (y - x)) · z
        1≡[w·[y-x]]·z = transport (λ i → 1f ≡ ·-comm z (w · (y - x)) i) 1≡z·[w·[y-x]]
        -- Then since 0 < z and xz < yz, by (∗), we get xzw (y − x) < yzw (y − x), and hence x < y.
        instance _ = [ z # 0f ] ∋ inr 0<z
        z⁻¹ = w · (y - x)
        z⁻¹≡w·[y-x] : z ⁻¹ ≡ (w · (y - x))
        z⁻¹≡w·[y-x] = sym ((·-linv-unique (w · (y - x)) z (sym 1≡[w·[y-x]]·z)) it)
        instance _ = 0<z
        0<z⁻¹ : [ 0f < z ⁻¹ ]
        0<z⁻¹ = ⁻¹-preserves-sign z (z ⁻¹) it (·-rinv z it)
        instance _ = [ 0f < w · (y - x) ] ∋ pathTo⇒ (λ i → 0f < z⁻¹≡w·[y-x] i) 0<z⁻¹
        in (  x ·  z         <  y ·  z         ⇒ᵖ⟨ ·-preserves-< _ _ z⁻¹ it ⟩
             (x ·  z) · z⁻¹  < (y ·  z) · z⁻¹  ⇒ᵖ⟨ pathTo⇒ (λ i → ·-assoc x z z⁻¹ (~ i) < ·-assoc y z z⁻¹ (~ i)) ⟩
              x · (z  · z⁻¹) <  y · (z  · z⁻¹) ⇒ᵖ⟨ pathTo⇒ (λ i → x · 1≡z·[w·[y-x]] (~ i) < y · 1≡z·[w·[y-x]] (~ i)) ⟩
              x · 1f         <  y · 1f         ⇒ᵖ⟨ pathTo⇒ (cong₂ _<_ (fst (·-identity x)) (fst (·-identity y))) ⟩
              x              <  y              ◼ᵖ) .snd x·z<y·z

      ·-reflects-< x y z 0<z = ·-creates-< x y z 0<z .snd

      item-9 = ·-creates-<

      -- 10. 0 < 1.
      is-0<1 with ·-inv#0 _ _ (·-identity 1f .fst) .fst
      -- For item 10, since 1 has multiplicative inverse 1, it is apart from 0, hence 0 < 1 ∨ 1 < 0.
      ... | inl 1<0 = snd (
        -- If 1 < 0 then by item 4 we have 0 < −1 and so by (∗) we get 0 < (−1) · (−1), that is, 0 < 1, so by transitivity 1 < 1, contradicting irreflexivity of <.
          1f          < 0f                ⇒ᵖ⟨ +-preserves-< 1f 0f (- 1f) ⟩
          1f    - 1f  < 0f - 1f           ⇒ᵖ⟨ transport (λ i → [ +-rinv 1f i < snd (+-identity (- 1f)) i ]) ⟩
          0f          <    - 1f           ⇒ᵖ⟨ ( λ 0<-1 → ·-preserves-< 0f (- 1f) (- 1f) 0<-1 0<-1) ⟩
          0f · (- 1f) <   (- 1f) · (- 1f) ⇒ᵖ⟨ pathTo⇒ (cong₂ _<_ (RingTheory'.0-leftNullifies (- 1f)) refl) ⟩
          0f          <   (- 1f) · (- 1f) ⇒ᵖ⟨ transport (λ i → [ 0f < RingTheory'.-commutesWithRight-· (- 1f) (1f)   i  ]) ⟩
          0f          < -((- 1f) ·    1f )⇒ᵖ⟨ transport (λ i → [ 0f < RingTheory'.-commutesWithLeft-·  (- 1f)  1f (~ i) ]) ⟩
          0f          < (-(- 1f))·    1f  ⇒ᵖ⟨ transport (λ i → [ 0f < (Group'Properties.-involutive 1f i · 1f) ]) ⟩
          0f          <      1f  ·    1f  ⇒ᵖ⟨ transport (λ i → [ 0f < fst (·-identity 1f) i ]) ⟩
          0f          <      1f           ⇒ᵖ⟨ <-trans _ _ _ 1<0 ⟩
          1f          <      1f           ⇒ᵖ⟨ <-irrefl 1f ⟩
                      ⊥                   ⇒ᵖ⟨ ⊥-elim ⟩
          0f          <      1f           ◼ᵖ) 1<0
      ... | inr 0<1 = 0<1

  -- Conversely, assume the 10 listed items—in particular, items 4, 5 and 9.
  module item459⇒ -- 4. 5. 9. ⇒ 6.
    (item-4 : [ Item-4 ]) -- ∀[ x ] ∀[ y ] ∀[ z ]                          x < y ⇔ x + z < y + z
    (item-5 : [ Item-5 ]) -- ∀[ x ] ∀[ y ]        0f < x + y          ⇒ (0f < x) ⊔ (0f < y)
    (item-9 : [ Item-9 ]) -- ∀[ x ] ∀[ y ] ∀[ z ] 0f < z              ⇒   (x < y ⇔ x · z < y · z)
    where
    abstract
      +-<-ext       : ∀ x y z w → [ (x + y) < (z + w) ⇒ (x < z) ⊔ (y < w) ]; _ : [ is-+-<-Extensional _+_ _<_ ]; _ = +-<-ext
      ·-preserves-< : ∀ x y z   → [  0f < z ⇒  x < y  ⇒ (x · z) < (y · z) ]; _ : [ operation _·_ preserves _<_ when (λ z → 0f < z) ]; _ = ·-preserves-<
      private
        item-4'     : ∀ x y     → [      0f <  x - y  ⇒  y < x            ]
        lemma       : ∀ x y z w → (z + w) + ((- x) + (- y)) ≡ (z - x) + (w - y)

      item-4' x y = snd (
        0f     <  x - y         ⇒ᵖ⟨ fst (item-4 0f (x + (- y)) y) ⟩
        0f + y < (x - y) + y    ⇒ᵖ⟨ transport (λ i → [ snd (+-identity y) i < sym (+-assoc x (- y) y) i ]) ⟩
             y <  x + (- y + y) ⇒ᵖ⟨ transport (λ i → [ y < x + snd (+-inv y) i ]) ⟩
             y <  x + 0f        ⇒ᵖ⟨ transport (λ i → [ y < fst (+-identity x) i ]) ⟩
             y <  x ◼ᵖ)

      lemma x y z w = (
        -- NOTE: there has to be a shorter way to to this kind of calculations ...
        --       also I got not much introspection while creating the paths
        (z +   w) + ((- x)  + (- y))   ≡⟨ ( λ i → +-assoc z w ((- x)  + (- y)) (~ i)) ⟩
        (z + ( w  + ((- x)  + (- y)))) ≡⟨ ( λ i → z + (+-assoc w (- x) (- y) i)) ⟩
        (z + ((w  +  (- x)) + (- y)))  ≡⟨ ( λ i → z + ((+-comm w (- x) i) + (- y)) ) ⟩
        (z + (((- x) +  w)  + (- y)))  ≡⟨ ( λ i → z + (+-assoc (- x) w (- y) (~ i))) ⟩
        (z + (( - x) + (w - y)))       ≡⟨ ( λ i → +-assoc z (- x) (w  - y) i ) ⟩
        (z - x) + (w - y) ∎)

      -- 6. (†)
      -- In order to show (†), suppose x + y < z + w.
      -- So, by item 4, we get (x + y) − (x + y) < (z + w) − (x + y), that is, 0 < (z − x) + (w − y).
      -- By item 5, (0 < z − x) ∨ (0 < w − y), and so by item 4 in either case, we get x < z ∨ y < w.
      +-<-ext x y z w = snd (
        (x + y)           < (z + w)                     ⇒ᵖ⟨ fst (item-4 (x + y) (z + w) (- (x + y))) ⟩
        (x + y) - (x + y) < (z + w) - (x + y)           ⇒ᵖ⟨ transport (λ i → [ +-rinv (x + y) i < (z + w) + (-dist x y) i ]) ⟩
                       0f < (z +   w) + ((- x) + (- y)) ⇒ᵖ⟨ transport (λ i → [ 0f < lemma x y z w i ]) ⟩
                       0f < (z - x) + (w - y)           ⇒ᵖ⟨ item-5 (z - x) (w - y) ⟩
        (0f < z - x) ⊔ (0f < w - y)                     ⇒ᵖ⟨ (λ q → case q as (0f < z - x) ⊔ (0f < w - y) ⇒ ((x < z) ⊔ (y < w)) of λ
                                                            { (inl p) → inlᵖ (item-4' z x p)
                                                            ; (inr p) → inrᵖ (item-4' w y p)
                                                            }) ⟩
        ( x < z    ) ⊔ ( y < w    ) ◼ᵖ)

      -- 6. (∗)
      ·-preserves-< x y z 0<z = item-9 x y z 0<z .fst

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
import      Lvl
open import Type

module Type.Singleton.Proofs {ℓ : Lvl.Level} {X : Type{ℓ}} where

open import Functional
open import Function.Domains
open import Logic.Predicate
open import Relator.Equals
open import Relator.Equals.Proofs
open import Type.Properties.Empty
open import Type.Singleton
open import Type.Properties.Singleton
open import Structure.Type.Identity

instance
  -- There is always a construction of a singleton type
  Singleton-existence : ∀{x : X} → Singleton(x)
  Singleton-existence {x} = [∃]-intro(x) ⦃ [≡]-intro ⦄

instance
  -- There is an unique construction of a singleton type
  Singleton-is-unit : ∀{x : X} → IsUnit(Singleton(x))
  Singleton-is-unit {x} = intro (Singleton-existence{x}) (g{x}) where
    A : ∀{y x : X} → (y ≡ x) → Type{ℓ}
    A {y}{x} (xy-proof) = ([∃]-intro y ⦃ xy-proof ⦄ ≡ Singleton-existence{x})

    f : ∀{x : X} → A{x}{x}([≡]-intro {_}{_} {x})
    f{x} = [≡]-intro {_}{_} {Singleton-existence{x}}

    Φ : ∀{y x : X}{xy-proof : (y ≡ x)} → ([∃]-intro y ⦃ xy-proof ⦄ ≡ Singleton-existence{x})
    Φ {y}{x}{xy-proof} = idElim(_≡_ {T = X}) (A)(f) {y}{x}(xy-proof)

    g : ∀{x : X}{σ : Singleton(x)} → (σ ≡ Singleton-existence{x})
    g{x}{[∃]-intro y ⦃ proof ⦄} = Φ{y}{x}{proof}

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 _ {a} {A : Set a} where

open import Agda.Builtin.Equality
open import Agda.Builtin.List

infix 4 _⊆_

postulate
  _⊆_ : (xs ys : List A) → Set a
  ⊆-trans : ∀{xs ys zs} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs

private
  variable
    xs ys zs : List A
    σ τ : ys ⊆ zs
    x y : A
    x≈y : x ≡ y

lemma : ∀ us (ρ : us ⊆ zs) (τ' : x ∷ xs ⊆ us) (σ' : ys ⊆ us)
         (τ'∘ρ≡τ : ⊆-trans τ' ρ ≡ τ)
         (σ'∘ρ≡σ : ⊆-trans σ' ρ ≡ σ)
      → us ⊆ us
lemma {τ = τ} {σ = σ} us ρ τ' σ' τ'∘ρ≡τ σ'∘ρ≡σ =
  lem {τ = τ} {σ} us ρ τ' σ' τ'∘ρ≡τ σ'∘ρ≡σ
  where
    lem : ∀ {ys zs} {τ : (x ∷ xs) ⊆ zs} {σ : ys ⊆ zs}
         us (ρ : us ⊆ zs) (τ' : x ∷ xs ⊆ us) (σ' : ys ⊆ us)
         (τ'∘ρ≡τ : ⊆-trans τ' ρ ≡ τ)
         (σ'∘ρ≡σ : ⊆-trans σ' ρ ≡ σ) →
       {!!}
    lem = {!!}


text:
module B where

open import A

B : Set
B = A


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

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

module Data.Product.Nary.NonDependent where

------------------------------------------------------------------------
-- Concrete examples can be found in README.Nary. This file's comments
-- are more focused on the implementation details and the motivations
-- behind the design decisions.
------------------------------------------------------------------------

open import Level as L using (Level; _⊔_; Lift; 0ℓ)
open import Agda.Builtin.Unit
open import Data.Product as Prod
import Data.Product.Properties as Prodₚ
open import Data.Sum.Base using (_⊎_)
open import Data.Nat.Base using (ℕ; zero; suc; pred)
open import Data.Fin.Base using (Fin; zero; suc)
open import Function
open import Relation.Nullary
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂)

open import Function.Nary.NonDependent.Base

-- Provided n Levels and a corresponding "vector" of `n` Sets, we can build a big
-- right-nested product type packing a value for each one of these Sets.
-- We have two distinct but equivalent definitions:
-- the first which is always ⊤-terminated
-- the other which has a special case for n = 1 because we want our `(un)curryₙ`
-- functions to work for user-written functions and products and they rarely are
-- ⊤-terminated.

Product⊤ : ∀ n {ls} → Sets n ls → Set (⨆ n ls)
Product⊤ zero    as       = ⊤
Product⊤ (suc n) (a , as) = a × Product⊤ n as

Product : ∀ n {ls} → Sets n ls → Set (⨆ n ls)
Product 0       _        = ⊤
Product 1       (a , _)  = a
Product (suc n) (a , as) = a × Product n as

-- Pointwise lifting of a relation on products

Allₙ : (∀ {a} {A : Set a} → Rel A a) →
        ∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
Allₙ R 0               l       r       = _
Allₙ R 1               a       b       = R a b , _
Allₙ R (suc n@(suc _)) (a , l) (b , r) = R a b , Allₙ R n l r

Equalₙ : ∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
Equalₙ = Allₙ _≡_

------------------------------------------------------------------------
-- Generic Programs

-- Once we have these type definitions, we can write generic programs
-- over them. They will typically be split into two or three definitions:

-- 1. action on the vector of n levels (if any)
-- 2. action on the corresponding vector of n Sets
-- 3. actual program, typed thank to the function defined in step 2.
------------------------------------------------------------------------

-- see Relation.Binary.PropositionalEquality for congₙ and substₙ, two
-- equality-related generic programs.

------------------------------------------------------------------------
-- equivalence of Product and Product⊤

toProduct : ∀ n {ls} {as : Sets n ls} → Product⊤ n as → Product n as
toProduct 0             _        = _
toProduct 1             (v , _)  = v
toProduct (suc (suc n)) (v , vs) = v , toProduct _ vs

toProduct⊤ : ∀ n {ls} {as : Sets n ls} → Product n as → Product⊤ n as
toProduct⊤ 0             _        = _
toProduct⊤ 1             v        = v , _
toProduct⊤ (suc (suc n)) (v , vs) = v , toProduct⊤ _ vs

------------------------------------------------------------------------
-- (un)curry

-- We start by defining `curryₙ` and `uncurryₙ` converting back and forth
-- between `A₁ → ⋯ → Aₙ → B` and `(A₁ × ⋯ × Aₙ) → B` by induction on `n`.

curryₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
         (Product n as → b) → as ⇉ b
curryₙ 0               f = f _
curryₙ 1               f = f
curryₙ (suc n@(suc _)) f = curryₙ n ∘′ curry f

uncurryₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
           as ⇉ b → (Product n as → b)
uncurryₙ 0               f = const f
uncurryₙ 1               f = f
uncurryₙ (suc n@(suc _)) f = uncurry (uncurryₙ n ∘′ f)

-- Variants for Product⊤

curry⊤ₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
          (Product⊤ n as → b) → as ⇉ b
curry⊤ₙ zero    f = f _
curry⊤ₙ (suc n) f = curry⊤ₙ n ∘′ curry f

uncurry⊤ₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
            as ⇉ b → (Product⊤ n as → b)
uncurry⊤ₙ zero    f = const f
uncurry⊤ₙ (suc n) f = uncurry (uncurry⊤ₙ n ∘′ f)

------------------------------------------------------------------------
-- decidability

Product⊤-dec : ∀ n {ls} {as : Sets n ls} → Product⊤ n (Dec <$> as) → Dec (Product⊤ n as)
Product⊤-dec zero    _          = yes _
Product⊤-dec (suc n) (p? , ps?) = p? ×-dec Product⊤-dec n ps?

Product-dec : ∀ n {ls} {as : Sets n ls} → Product n (Dec <$> as) → Dec (Product n as)
Product-dec 0               _          = yes _
Product-dec 1               p?         = p?
Product-dec (suc n@(suc _)) (p? , ps?) = p? ×-dec Product-dec n ps?

------------------------------------------------------------------------
-- pointwise liftings

toEqualₙ : ∀ n {ls} {as : Sets n ls} {l r : Product n as} →
           l ≡ r → Product n (Equalₙ n l r)
toEqualₙ 0               eq = _
toEqualₙ 1               eq = eq
toEqualₙ (suc n@(suc _)) eq = Prod.map₂ (toEqualₙ n) (Prodₚ.,-injective eq)

fromEqualₙ : ∀ n {ls} {as : Sets n ls} {l r : Product n as} →
             Product n (Equalₙ n l r) → l ≡ r
fromEqualₙ 0               eq = refl
fromEqualₙ 1               eq = eq
fromEqualₙ (suc n@(suc _)) eq = uncurry (cong₂ _,_) (Prod.map₂ (fromEqualₙ n) eq)

------------------------------------------------------------------------
-- projection of the k-th component

-- To know at which Set level the k-th projection out of an n-ary product
-- lives, we need to extract said level, by induction on k.

Levelₙ : ∀ {n} → Levels n → Fin n → Level
Levelₙ (l , _)  zero    = l
Levelₙ (_ , ls) (suc k) = Levelₙ ls k

-- Once we have the Sets used in the product, we can extract the one we
-- are interested in, once more by induction on k.

Projₙ : ∀ {n ls} → Sets n ls → ∀ k → Set (Levelₙ ls k)
Projₙ (a , _)  zero    = a
Projₙ (_ , as) (suc k) = Projₙ as k

-- Finally, provided a Product of these sets, we can extract the k-th value.
-- `projₙ` takes both `n` and `k` explicitly because we expect the user will
-- be using a concrete `k` (potentially manufactured using `Data.Fin`'s `#_`)
-- and it will not be possible to infer `n` from it.

projₙ : ∀ n {ls} {as : Sets n ls} k → Product n as → Projₙ as k
projₙ 1               zero    v        = v
projₙ (suc n@(suc _)) zero    (v , _)  = v
projₙ (suc n@(suc _)) (suc k) (_ , vs) = projₙ n k vs
projₙ 1 (suc ()) v

------------------------------------------------------------------------
-- removal of the k-th component

Levelₙ⁻ : ∀ {n} → Levels n → Fin n → Levels (pred n)
Levelₙ⁻               (_ , ls) zero    = ls
Levelₙ⁻ {suc (suc _)} (l , ls) (suc k) = l , Levelₙ⁻ ls k
Levelₙ⁻ {1} _ (suc ())

Removeₙ : ∀ {n ls} → Sets n ls → ∀ k → Sets (pred n) (Levelₙ⁻ ls k)
Removeₙ               (_ , as) zero    = as
Removeₙ {suc (suc _)} (a , as) (suc k) = a , Removeₙ as k
Removeₙ {1} _ (suc ())

removeₙ : ∀ n {ls} {as : Sets n ls} k →
          Product n as → Product (pred n) (Removeₙ as k)
removeₙ (suc zero)          zero    _        = _
removeₙ (suc (suc _))       zero    (_ , vs) = vs
removeₙ (suc (suc zero))    (suc k) (v , _)  = v
removeₙ (suc (suc (suc _))) (suc k) (v , vs) = v , removeₙ _ k vs
removeₙ (suc zero) (suc ()) _

------------------------------------------------------------------------
-- insertion of a k-th component

Levelₙ⁺ : ∀ {n} → Levels n → Fin (suc n) → Level → Levels (suc n)
Levelₙ⁺         ls       zero    l⁺ = l⁺ , ls
Levelₙ⁺ {suc _} (l , ls) (suc k) l⁺ = l , Levelₙ⁺ ls k l⁺
Levelₙ⁺ {0} _ (suc ())

Insertₙ : ∀ {n ls l⁺} → Sets n ls → ∀ k (a⁺ : Set l⁺) → Sets (suc n) (Levelₙ⁺ ls k l⁺)
Insertₙ         as       zero    a⁺ = a⁺ , as
Insertₙ {suc _} (a , as) (suc k) a⁺ = a , Insertₙ as k a⁺
Insertₙ {zero} _ (suc ()) _

insertₙ : ∀ n {ls l⁺} {as : Sets n ls} {a⁺ : Set l⁺} k (v⁺ : a⁺) →
          Product n as → Product (suc n) (Insertₙ as k a⁺)
insertₙ 0             zero    v⁺ vs       = v⁺
insertₙ (suc n)       zero    v⁺ vs       = v⁺ , vs
insertₙ 1             (suc k) v⁺ vs       = vs , insertₙ 0 k v⁺ _
insertₙ (suc (suc n)) (suc k) v⁺ (v , vs) = v , insertₙ _ k v⁺ vs
insertₙ 0 (suc ()) _ _

------------------------------------------------------------------------
-- update of a k-th component

Levelₙᵘ : ∀ {n} → Levels n → Fin n → Level → Levels n
Levelₙᵘ (_ , ls) zero    lᵘ = lᵘ , ls
Levelₙᵘ (l , ls) (suc k) lᵘ = l , Levelₙᵘ ls k lᵘ

Updateₙ : ∀ {n ls lᵘ} (as : Sets n ls) k (aᵘ : Set lᵘ) → Sets n (Levelₙᵘ ls k lᵘ)
Updateₙ (_ , as) zero    aᵘ = aᵘ , as
Updateₙ (a , as) (suc k) aᵘ = a , Updateₙ as k aᵘ

updateₙ : ∀ n {ls lᵘ} {as : Sets n ls} k {aᵘ : _ → Set lᵘ} (f : ∀ v → aᵘ v)
          (vs : Product n as) → Product n (Updateₙ as k (aᵘ (projₙ n k vs)))
updateₙ 1             zero    f v        = f v
updateₙ (suc (suc _)) zero    f (v , vs) = f v , vs
updateₙ (suc (suc _)) (suc k) f (v , vs) = v , updateₙ _ k f vs
updateₙ 1 (suc ()) _ _

updateₙ′ : ∀ n {ls lᵘ} {as : Sets n ls} k {aᵘ : Set lᵘ} (f : Projₙ as k → aᵘ) →
           Product n as → Product n (Updateₙ as k aᵘ)
updateₙ′ n k = updateₙ n k


text:
module Numeral.Finite.Category where

open import Functional
import      Lvl
open import Numeral.Finite
open import Numeral.Natural
open import Type
open import Syntax.Function

-- Equality category on the type of finite natural numbers.
module _ where
  open import Relator.Equals
  open import Relator.Equals.Proofs.Equiv
  open import Relator.Equals.Category
  open import Structure.Category
  open import Structure.Category.Categories
  import      Structure.Category.Functor as Category
  open import Structure.Function
  open import Structure.Function.Domain
  import      Structure.Function.Names as Names
  open import Structure.Groupoid
  open import Structure.Groupoid.Groupoids
  import      Structure.Groupoid.Functor as Groupoid

  𝕟-identityTypeGroupoid : Groupoid((_≡_) on₂ 𝕟)
  𝕟-identityTypeGroupoid = on₂-groupoid identityTypeGroupoid 𝕟

  -- The type constructor `𝕟` is a functor.
  -- This means:
  -- • `map: ∀(a: ℕ)(b: ℕ). (a ≡ b) → (𝕟(a) ≡ 𝕟(b))`
  -- • `map(reflexivity(_≡_)) ≡ reflexivity(_≡_)`
  -- • `transitivity(_≡_) (map p) (map q) ≡ map(transitivity(_≡_) p q)`
  𝕟-functor : Groupoid.Functor(identityTypeGroupoid{T = ℕ})(𝕟-identityTypeGroupoid) id
  𝕟-functor = idTransportFunctor

  instance
    𝕟-injectivity : Injective(𝕟)
    𝕟-injectivity = intro proof where
      proof : Names.Injective(𝕟)
      proof {𝟎}   {𝟎}    [≡]-intro = [≡]-intro
      proof {𝐒 a} {𝐒 .a} [≡]-intro = [≡]-with(𝐒) (proof [≡]-intro)

  𝕟-inverse-functor : Groupoid.Functor(𝕟-identityTypeGroupoid)(identityTypeGroupoid{T = ℕ}) id
  Groupoid.Functor.map 𝕟-inverse-functor = injective(𝕟)
  Function.congruence (Groupoid.Functor.map-function 𝕟-inverse-functor) [≡]-intro = [≡]-intro
  Groupoid.Functor.op-preserving 𝕟-inverse-functor {x} {x} {x} {[≡]-intro} {[≡]-intro} = proof{x} where
    proof : ∀{x} → Groupoid.Functor.map 𝕟-inverse-functor (Groupoid._∘_ 𝕟-identityTypeGroupoid {x} [≡]-intro [≡]-intro) ≡ Groupoid._∘_ identityTypeGroupoid (Groupoid.Functor.map 𝕟-inverse-functor [≡]-intro) (Groupoid.Functor.map 𝕟-inverse-functor [≡]-intro)
    proof {𝟎} = [≡]-intro
    proof {𝐒 x}
      rewrite proof{x}
      rewrite Groupoid.Functor.id-preserving 𝕟-inverse-functor {x}
      = [≡]-intro
  Groupoid.Functor.id-preserving 𝕟-inverse-functor {x} = proof{x} where
    proof : ∀{x} → (injective(𝕟) (Groupoid.id 𝕟-identityTypeGroupoid {x}) ≡ Category.id identityTypeCategory)
    proof {𝟎} = [≡]-intro
    proof {𝐒 x} rewrite proof{x} = [≡]-intro
  Groupoid.Functor.inv-preserving 𝕟-inverse-functor {x} {x} {[≡]-intro} = proof where
    proof : ∀{x} → Groupoid.Functor.map 𝕟-inverse-functor (Groupoid.inv 𝕟-identityTypeGroupoid {x} [≡]-intro) ≡ Groupoid.inv identityTypeGroupoid (Groupoid.Functor.map 𝕟-inverse-functor [≡]-intro)
    proof {𝟎} = [≡]-intro
    proof {𝐒 x}
      rewrite proof{x}
      rewrite Groupoid.Functor.id-preserving 𝕟-inverse-functor {x}
      = [≡]-intro

  open import Function.Equals
  open import Numeral.Finite.Bound
  open import Numeral.Natural.Relation.Order.Category
  open import Numeral.Natural.Relation.Order.Proofs
  open import Numeral.Natural.Relation.Order
  open import Type.Category.ExtensionalFunctionsCategory
  open import Structure.Relator.Properties

  -- A functor for boundary changing of finite numeral types (𝕟).
  bound-functor : Category.Functor [≤]-category (on₂-category typeExtensionalFnCategory 𝕟) id
  Category.Functor.map bound-functor = bound-[≤]
  Function.congruence (Category.Functor.map-function bound-functor) [≡]-intro = reflexivity(_⊜_)
  Category.Functor.op-preserving bound-functor {x}{y}{z} {p}{q} = proof{x}{y}{z} {p}{q} where
    proof : ∀{x y z}{p : (y ≤ z)}{q : (x ≤ y)} → (bound-[≤] (transitivity(_≤_) q p) ⊜ (bound-[≤] p) ∘ (bound-[≤] q))
    _⊜_.proof (proof {𝐒 x} {𝐒 y} {𝐒 z} {succ _} {succ _}) {𝟎}   = [≡]-intro
    _⊜_.proof (proof {𝐒 x} {𝐒 y} {𝐒 z} {succ _} {succ _}) {𝐒 n} = congruence₁(𝐒) (_⊜_.proof (proof {x} {y} {z}) {n})
  Category.Functor.id-preserving bound-functor {n} = proof{n} where
    proof : ∀{n} → (bound-[≤] (reflexivity(_≤_) {n}) ⊜ id)
    _⊜_.proof (proof {𝟎})   {()}
    _⊜_.proof (proof {𝐒 n}) {𝟎}   = [≡]-intro
    _⊜_.proof (proof {𝐒 n}) {𝐒 x} = congruence₁(𝐒) (_⊜_.proof (proof {n}) {x})


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Neutral {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
import Definition.Typed.Weakening as Wk
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties.Reflexivity
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Symmetry

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Neutral reflexive types are reducible.
neu : ∀ {l Γ A} (neA : Neutral A)
    → Γ ⊢ A
    → Γ ⊢ A ~ A ∷ U
    → Γ ⊩⟨ l ⟩ A
neu neA A A~A = ne′ _ (idRed:*: A) neA A~A

  -- Helper function for reducible neutral equality of a specific type of derivation.
neuEq′ : ∀ {l Γ A B} ([A] : Γ ⊩⟨ l ⟩ne A)
         (neA : Neutral A)
         (neB : Neutral B)
       → Γ ⊢ A → Γ ⊢ B
       → Γ ⊢ A ~ B ∷ U
       → Γ ⊩⟨ l ⟩ A ≡ B / ne-intr [A]
neuEq′ (noemb (ne K [ ⊢A , ⊢B , D ] neK K≡K)) neA neB A B A~B =
  let A≡K = whnfRed* D (ne neA)
  in  ne₌ _ (idRed:*: B) neB (PE.subst (λ x → _ ⊢ x ~ _ ∷ _) A≡K A~B)
neuEq′ (emb 0<1 x) neB A:≡:B = neuEq′ x neB A:≡:B

-- Neutrally equal types are of reducible equality.
neuEq : ∀ {l Γ A B} ([A] : Γ ⊩⟨ l ⟩ A)
        (neA : Neutral A)
        (neB : Neutral B)
      → Γ ⊢ A → Γ ⊢ B
      → Γ ⊢ A ~ B ∷ U
      → Γ ⊩⟨ l ⟩ A ≡ B / [A]
neuEq [A] neA neB A B A~B =
  irrelevanceEq (ne-intr (ne-elim neA [A]))
                [A]
                (neuEq′ (ne-elim neA [A]) neA neB A B A~B)

mutual
  -- Neutral reflexive terms are reducible.
  neuTerm : ∀ {l Γ A n} ([A] : Γ ⊩⟨ l ⟩ A) (neN : Neutral n)
          → Γ ⊢ n ∷ A
          → Γ ⊢ n ~ n ∷ A
          → Γ ⊩⟨ l ⟩ n ∷ A / [A]
  neuTerm (Uᵣ′ .⁰ 0<1 ⊢Γ) neN n n~n =
    Uₜ _ (idRedTerm:*: n) (ne neN) (~-to-≅ₜ n~n) (neu neN (univ n) n~n)
  neuTerm (ℕᵣ [ ⊢A , ⊢B , D ]) neN n n~n =
    let A≡ℕ  = subset* D
        n~n′ = ~-conv n~n A≡ℕ
        n≡n  = ~-to-≅ₜ n~n′
    in  ℕₜ _ (idRedTerm:*: (conv n A≡ℕ)) n≡n (ne (neNfₜ neN (conv n A≡ℕ) n~n′))
  neuTerm (Emptyᵣ [ ⊢A , ⊢B , D ]) neN n n~n =
    let A≡Empty  = subset* D
        n~n′ = ~-conv n~n A≡Empty
        n≡n  = ~-to-≅ₜ n~n′
    in  Emptyₜ _ (idRedTerm:*: (conv n A≡Empty)) n≡n (ne (neNfₜ neN (conv n A≡Empty) n~n′))
  neuTerm (Unitᵣ [ ⊢A , ⊢B , D ]) neN n n~n =
    let A≡Unit  = subset* D
        n~n′ = ~-conv n~n A≡Unit
    in  Unitₜ _ (idRedTerm:*: (conv n A≡Unit)) (ne neN)
  neuTerm (ne′ K [ ⊢A , ⊢B , D ] neK K≡K) neN n n~n =
    let A≡K = subset* D
    in  neₜ _ (idRedTerm:*: (conv n A≡K)) (neNfₜ neN (conv n A≡K)
            (~-conv n~n A≡K))
  neuTerm (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN n n~n =
    let A≡ΠFG = subset* (red D)
    in  Πₜ _ (idRedTerm:*: (conv n A≡ΠFG)) (ne neN) (~-to-≅ₜ (~-conv n~n A≡ΠFG))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let A≡ΠFG = subset* (red D)
                  ρA≡ρΠFG = Wk.wkEq [ρ] ⊢Δ (subset* (red D))
                  G[a]≡G[b] = escapeEq ([G] [ρ] ⊢Δ [b])
                                          (symEq ([G] [ρ] ⊢Δ [a]) ([G] [ρ] ⊢Δ [b])
                                                 (G-ext [ρ] ⊢Δ [a] [b] [a≡b]))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  b = escapeTerm ([F] [ρ] ⊢Δ) [b]
                  a≡b = escapeTermEq ([F] [ρ] ⊢Δ) [a≡b]
                  ρn = conv (Wk.wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG
                  neN∘a = ∘ₙ (wkNeutral ρ neN)
                  neN∘b = ∘ₙ (wkNeutral ρ neN)
              in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∘a neN∘b
                            (ρn ∘ⱼ a)
                            (conv (ρn ∘ⱼ b) (≅-eq G[a]≡G[b]))
                            (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡b))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let ρA≡ρΠFG = Wk.wkEq [ρ] ⊢Δ (subset* (red D))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  a≡a = escapeTermEq ([F] [ρ] ⊢Δ) (reflEqTerm ([F] [ρ] ⊢Δ) [a])
              in  neuTerm ([G] [ρ] ⊢Δ [a]) (∘ₙ (wkNeutral ρ neN))
                          (conv (Wk.wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG ∘ⱼ a)
                          (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡a))
  neuTerm (Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN ⊢n n~n =
    let A≡ΣFG = subset* (red D)
        ⊢Γ = wf ⊢F
        ⊢n = conv ⊢n A≡ΣFG
        n~n = ~-conv n~n A≡ΣFG

        [F] = [F] Wk.id ⊢Γ
        [fst] = neuTerm [F] (fstₙ neN)
                        (PE.subst
                          (λ x → _ ⊢ fst _ ∷ x)
                          (PE.sym (wk-id F))
                          (fstⱼ ⊢F ⊢G ⊢n))
                        (PE.subst
                          (λ x → _ ⊢ _ ~ _ ∷ x)
                          (PE.sym (wk-id F))
                          (~-fst ⊢F ⊢G n~n))
        [Gfst] = [G] Wk.id ⊢Γ [fst]
        [snd] = neuTerm [Gfst] (sndₙ neN)
                        (PE.subst
                          (λ x → _ ⊢ snd _ ∷ x)
                          (PE.cong (λ x → x [ fst _ ]) (PE.sym (wk-lift-id G)))
                          (sndⱼ ⊢F ⊢G ⊢n))
                        (PE.subst
                          (λ x → _ ⊢ _ ~ _ ∷ x)
                          (PE.cong (λ x → x [ fst _ ]) (PE.sym (wk-lift-id G)))
                          (~-snd ⊢F ⊢G n~n))
    in  Σₜ _ (idRedTerm:*: ⊢n) (ne neN) (~-to-≅ₜ n~n)
           [fst]
           [snd]
  neuTerm (emb 0<1 x) neN n = neuTerm x neN n

  -- Neutrally equal terms are of reducible equality.
  neuEqTerm : ∀ {l Γ A n n′} ([A] : Γ ⊩⟨ l ⟩ A)
              (neN : Neutral n) (neN′ : Neutral n′)
            → Γ ⊢ n  ∷ A
            → Γ ⊢ n′ ∷ A
            → Γ ⊢ n ~ n′ ∷ A
            → Γ ⊩⟨ l ⟩ n ≡ n′ ∷ A / [A]
  neuEqTerm (Uᵣ′ .⁰ 0<1 ⊢Γ) neN neN′ n n′ n~n′ =
    let [n]  = neu neN  (univ n) (~-trans n~n′ (~-sym n~n′))
        [n′] = neu neN′ (univ n′) (~-trans (~-sym n~n′) n~n′)
    in  Uₜ₌ _ _ (idRedTerm:*: n) (idRedTerm:*: n′) (ne neN) (ne neN′)
            (~-to-≅ₜ n~n′) [n] [n′] (neuEq [n] neN neN′ (univ n) (univ n′) n~n′)
  neuEqTerm (ℕᵣ [ ⊢A , ⊢B , D ]) neN neN′ n n′ n~n′ =
    let A≡ℕ = subset* D
        n~n′₁ = ~-conv n~n′ A≡ℕ
        n≡n′ = ~-to-≅ₜ n~n′₁
    in  ℕₜ₌ _ _ (idRedTerm:*: (conv n A≡ℕ)) (idRedTerm:*: (conv n′ A≡ℕ))
            n≡n′ (ne (neNfₜ₌ neN neN′ n~n′₁))
  neuEqTerm (Emptyᵣ [ ⊢A , ⊢B , D ]) neN neN′ n n′ n~n′ =
    let A≡Empty = subset* D
        n~n′₁ = ~-conv n~n′ A≡Empty
        n≡n′ = ~-to-≅ₜ n~n′₁
    in  Emptyₜ₌ _ _ (idRedTerm:*: (conv n A≡Empty)) (idRedTerm:*: (conv n′ A≡Empty))
            n≡n′ (ne (neNfₜ₌ neN neN′ n~n′₁))
  neuEqTerm (Unitᵣ [ ⊢A , ⊢B , D ]) neN neN′ n n′ n~n′ =
    let A≡Unit = subset* D
    in  Unitₜ₌ (conv n A≡Unit) (conv n′ A≡Unit)
  neuEqTerm (ne (ne K [ ⊢A , ⊢B , D ] neK K≡K)) neN neN′ n n′ n~n′ =
    let A≡K = subset* D
    in  neₜ₌ _ _ (idRedTerm:*: (conv n A≡K)) (idRedTerm:*: (conv n′ A≡K))
             (neNfₜ₌ neN neN′ (~-conv n~n′ A≡K))
  neuEqTerm (Πᵣ′ F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ n n′ n~n′ =
    let [ΠFG] = Πᵣ′ F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext
        A≡ΠFG = subset* D
        n~n′₁ = ~-conv n~n′ A≡ΠFG
        n≡n′ = ~-to-≅ₜ n~n′₁
        n~n = ~-trans n~n′ (~-sym n~n′)
        n′~n′ = ~-trans (~-sym n~n′) n~n′
    in  Πₜ₌ _ _ (idRedTerm:*: (conv n A≡ΠFG)) (idRedTerm:*: (conv n′ A≡ΠFG))
            (ne neN) (ne neN′) n≡n′
            (neuTerm [ΠFG] neN n n~n) (neuTerm [ΠFG] neN′ n′ n′~n′)
            (λ {ρ} [ρ] ⊢Δ [a] →
               let ρA≡ρΠFG = Wk.wkEq [ρ] ⊢Δ A≡ΠFG
                   ρn = Wk.wkTerm [ρ] ⊢Δ n
                   ρn′ = Wk.wkTerm [ρ] ⊢Δ n′
                   a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                   a≡a = escapeTermEq ([F] [ρ] ⊢Δ)
                                          (reflEqTerm ([F] [ρ] ⊢Δ) [a])
                   neN∙a   = ∘ₙ (wkNeutral ρ neN)
                   neN′∙a′ = ∘ₙ (wkNeutral ρ neN′)
               in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∙a neN′∙a′
                             (conv ρn  ρA≡ρΠFG ∘ⱼ a)
                             (conv ρn′ ρA≡ρΠFG ∘ⱼ a)
                             (~-app (~-wk [ρ] ⊢Δ n~n′₁) a≡a))
  neuEqTerm (Σᵣ′ F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ ⊢n ⊢n′ n~n′ =
    let [ΣFG] = Σᵣ′ F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext
        A≡ΣFG = subset* D
        n~n = ~-trans n~n′ (~-sym n~n′)
        n′~n′ = ~-trans (~-sym n~n′) n~n′

        ⊢Γ = wf ⊢F
        ⊢nΣ = conv ⊢n A≡ΣFG
        ⊢n′Σ = conv ⊢n′ A≡ΣFG
        n~n′Σ = ~-conv n~n′ A≡ΣFG
        n~nΣ = ~-conv n~n A≡ΣFG
        n′~n′Σ = ~-conv n′~n′ A≡ΣFG
        [F] = [F] Wk.id ⊢Γ
        ⊢fstnΣ = (PE.subst
                (λ x → _ ⊢ fst _ ∷ x)
                (PE.sym (wk-id F))
                (fstⱼ ⊢F ⊢G ⊢nΣ))
        ⊢fstn′Σ = (PE.subst
                    (λ x → _ ⊢ fst _ ∷ x)
                    (PE.sym (wk-id F))
                    (fstⱼ ⊢F ⊢G ⊢n′Σ))
        [fstn] = neuTerm [F] (fstₙ neN)
                         ⊢fstnΣ
                         (PE.subst
                           (λ x → _ ⊢ _ ~ _ ∷ x)
                           (PE.sym (wk-id F))
                           (~-fst ⊢F ⊢G n~nΣ))
        [fstn′] = neuTerm [F] (fstₙ neN′)
                          ⊢fstn′Σ
                          (PE.subst
                            (λ x → _ ⊢ _ ~ _ ∷ x)
                            (PE.sym (wk-id F))
                            (~-fst ⊢F ⊢G n′~n′Σ))
        [fstn≡fstn′] = neuEqTerm [F] (fstₙ neN) (fstₙ neN′)
                         ⊢fstnΣ
                         ⊢fstn′Σ
                         (PE.subst
                           (λ x → _ ⊢ _ ~ _ ∷ x)
                           (PE.sym (wk-id F))
                           (~-fst ⊢F ⊢G n~n′Σ))
        [Gfstn] = [G] Wk.id ⊢Γ [fstn]
        [Gfstn′] = PE.subst (λ x → _ ⊩⟨ _ ⟩ x [ fst _ ]) (wk-lift-id G) ([G] Wk.id ⊢Γ [fstn′])
        [fstn′≡fstn] = symEqTerm [F] [fstn≡fstn′]
        [Gfstn′≡Gfstn] = irrelevanceEq″
                           (PE.cong (λ x → x [ fst _ ]) (wk-lift-id G))
                           (PE.cong (λ x → x [ fst _ ]) (wk-lift-id G))
                           ([G] Wk.id ⊢Γ [fstn′]) [Gfstn′]
                           (G-ext Wk.id ⊢Γ [fstn′] [fstn] [fstn′≡fstn])
        Gfstn′≡Gfstn = ≅-eq (escapeEq [Gfstn′] [Gfstn′≡Gfstn])
        [sndn≡sndn′] = neuEqTerm [Gfstn] (sndₙ neN) (sndₙ neN′)
                          (PE.subst
                            (λ x → _ ⊢ snd _ ∷ x)
                            (PE.cong (λ x → x [ fst _ ]) (PE.sym (wk-lift-id G)))
                            (sndⱼ ⊢F ⊢G ⊢nΣ))
                          (PE.subst
                            (λ x → _ ⊢ snd _ ∷ x)
                            (PE.cong (λ x → x [ fst _ ]) (PE.sym (wk-lift-id G)))
                            (conv (sndⱼ ⊢F ⊢G ⊢n′Σ) Gfstn′≡Gfstn))
                          (PE.subst
                            (λ x → _ ⊢ _ ~ _ ∷ x)
                            (PE.cong (λ x → x [ fst _ ]) (PE.sym (wk-lift-id G)))
                            (~-snd ⊢F ⊢G n~n′Σ))
    in  Σₜ₌ _ _ (idRedTerm:*: ⊢nΣ) (idRedTerm:*: ⊢n′Σ)
            (ne neN) (ne neN′) (~-to-≅ₜ n~n′Σ)
            (neuTerm [ΣFG] neN ⊢n n~n) (neuTerm [ΣFG] neN′ ⊢n′ n′~n′)
            [fstn] [fstn′] [fstn≡fstn′] [sndn≡sndn′]
  neuEqTerm (emb 0<1 x) neN neN′ n:≡:n′ = neuEqTerm x neN neN′ n:≡:n′


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlattening
open import lib.types.PushoutFmap
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Unit

-- Wedge of two pointed types is defined as a particular case of pushout

module lib.types.Wedge where

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙∨-span : ⊙Span
  ⊙∨-span = ⊙span X Y ⊙Unit ⊙cst ⊙cst
  ⊙wedge-span = ⊙∨-span

  ∨-span : Span
  ∨-span = ⊙Span-to-Span ⊙∨-span
  wedge-span = ∨-span

  Wedge : Type (lmax i j)
  Wedge = Pushout wedge-span

  infix 80 _∨_
  _∨_ = Wedge

  ⊙Wedge : Ptd (lmax i j)
  ⊙Wedge = ⊙Pushout ⊙wedge-span

  infix 80 _⊙∨_
  _⊙∨_ = ⊙Wedge

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  winl : de⊙ X → X ∨ Y
  winl x = left x

  winr : de⊙ Y → X ∨ Y
  winr y = right y

  wglue : winl (pt X) == winr (pt Y)
  wglue = glue tt

  ⊙winl : X ⊙→ X ⊙∨ Y
  ⊙winl = (winl , idp)

  ⊙winr : Y ⊙→ X ⊙∨ Y
  ⊙winr = (winr , ! wglue)

  module WedgeElim {k} {P : X ∨ Y → Type k}
    (winl* : (x : de⊙ X) → P (winl x)) (winr* : (y : de⊙ Y) → P (winr y))
    (glue* : winl* (pt X) == winr* (pt Y) [ P ↓ wglue ]) where

    private
      module M = PushoutElim winl* winr* (λ _ → glue*)

    f = M.f
    glue-β = M.glue-β unit

  ∨-elim = WedgeElim.f
  Wedge-elim = WedgeElim.f

  module WedgeRec {k} {C : Type k} (winl* : de⊙ X → C) (winr* : de⊙ Y → C)
    (glue* : winl* (pt X) == winr* (pt Y)) where

    private
      module M = PushoutRec {d = wedge-span X Y} winl* winr* (λ _ → glue*)

    f = M.f
    glue-β = M.glue-β unit

  ∨-rec = WedgeRec.f
  Wedge-rec = WedgeRec.f

  module ⊙WedgeRec {k} {Z : Ptd k} (g : X ⊙→ Z) (h : Y ⊙→ Z) where

    open WedgeRec (fst g) (fst h) (snd g ∙ ! (snd h)) public

    ⊙f : X ⊙∨ Y ⊙→ Z
    ⊙f = (f , snd g)

    ⊙winl-β : ⊙f ⊙∘ ⊙winl == g
    ⊙winl-β = idp

    ⊙winr-β : ⊙f ⊙∘ ⊙winr == h
    ⊙winr-β = ⊙λ=' (λ _ → idp) lemma where
      abstract
        lemma : snd (⊙f ⊙∘ ⊙winr) == snd h
        lemma =
          ap (_∙ snd g)
             (ap-! f wglue ∙ ap ! glue-β ∙ !-∙ (snd g) (! (snd h)))
          ∙ ∙-assoc (! (! (snd h))) (! (snd g)) (snd g)
          ∙ ap (! (! (snd h)) ∙_) (!-inv-l (snd g))
          ∙ ∙-unit-r (! (! (snd h)))
          ∙ !-! (snd h)

  ⊙∨-rec = ⊙WedgeRec.⊙f
  ⊙Wedge-rec = ⊙WedgeRec.⊙f

  ⊙Wedge-rec-post∘ : ∀ {k l} {Z : Ptd k} {W : Ptd l}
    (k : Z ⊙→ W) (g : X ⊙→ Z) (h : Y ⊙→ Z)
    → k ⊙∘ ⊙Wedge-rec g h ⊙∼ ⊙Wedge-rec (k ⊙∘ g) (k ⊙∘ h)
  ⊙Wedge-rec-post∘ k g h =
    (Wedge-elim (λ _ → idp) (λ _ → idp)
      (↓-='-in' $ ⊙WedgeRec.glue-β (k ⊙∘ g) (k ⊙∘ h)
                 ∙ lemma (fst k) (snd g) (snd h) (snd k)
                 ∙ ! (ap (ap (fst k)) (⊙WedgeRec.glue-β g h))
                 ∙ ∘-ap (fst k) (fst (⊙Wedge-rec g h)) wglue)) ,
    idp
    where
    lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {x y z : A} {w : B}
      (p : x == z) (q : y == z) (r : f z == w)
      → (ap f p ∙ r) ∙ ! (ap f q ∙ r) == ap f (p ∙ ! q)
    lemma f idp idp idp = idp
  ⊙∨-rec-post∘ = ⊙Wedge-rec-post∘

  ⊙Wedge-rec-η : ⊙Wedge-rec ⊙winl ⊙winr == ⊙idf (X ⊙∨ Y)
  ⊙Wedge-rec-η = ⊙λ='
    (Wedge-elim (λ _ → idp) (λ _ → idp)
      (↓-='-in' $ ap-idf wglue
                 ∙ ! (!-! wglue)
                 ∙ ! (⊙WedgeRec.glue-β ⊙winl ⊙winr)))
    idp
  ⊙∨-rec-η = ⊙Wedge-rec-η

  add-wglue : de⊙ (X ⊙⊔ Y) → X ∨ Y
  add-wglue (inl x) = winl x
  add-wglue (inr y) = winr y

  ⊙add-wglue : X ⊙⊔ Y ⊙→ X ⊙∨ Y
  ⊙add-wglue = add-wglue , idp

  module Projl = ⊙WedgeRec (⊙idf X) (⊙cst {X = Y})
  module Projr = ⊙WedgeRec (⊙cst {X = X}) (⊙idf Y)

  projl = Projl.f
  projr = Projr.f
  ⊙projl = Projl.⊙f
  ⊙projr = Projr.⊙f

  module WedgeToProduct = ⊙WedgeRec ((_, pt Y) , idp) ((pt X ,_), idp)

  ∨-⊙to-× : X ⊙∨ Y ⊙→ X ⊙× Y
  ∨-⊙to-× = WedgeToProduct.⊙f

  ∨-to-× : X ∨ Y → de⊙ (X ⊙× Y)
  ∨-to-× = WedgeToProduct.f

  ∨-to-×-glue-β : ap ∨-to-× wglue == idp
  ∨-to-×-glue-β = WedgeToProduct.glue-β

  abstract
    ↓-∨to×=cst-in : ∀ {x y} {p p' : (pt X , pt Y) == (x , y)}
      → p == p'
      → p == p' [ (λ w → ∨-to-× w == (x , y)) ↓ wglue ]
    ↓-∨to×=cst-in {p' = idp} q =
      ↓-app=cst-in' (q ∙ ! WedgeToProduct.glue-β)

    ↓-∨to×=cst-out : ∀ {x y} {p p' : (pt X , pt Y) == (x , y)}
      → p == p' [ (λ w → ∨-to-× w == (x , y)) ↓ wglue ]
      → p == p'
    ↓-∨to×=cst-out {p' = idp} q =
      ↓-app=cst-out' q ∙ WedgeToProduct.glue-β

    ↓-∨to×=cst-β : ∀ {x y} {p p' : (pt X , pt Y) == (x , y)}
      (q : p == p')
      → ↓-∨to×=cst-out (↓-∨to×=cst-in q) == q
    ↓-∨to×=cst-β {p' = idp} idp =
        ap (_∙ WedgeToProduct.glue-β) (↓-app=cst-β' {p = wglue} (! WedgeToProduct.glue-β))
      ∙ !-inv-l WedgeToProduct.glue-β

    ↓-∨to×=cst-η : ∀ {x y} {p p' : (pt X , pt Y) == (x , y)}
      (q : p == p' [ (λ w → ∨-to-× w == (x , y)) ↓ wglue ])
      → ↓-∨to×=cst-in (↓-∨to×=cst-out q) == q
    ↓-∨to×=cst-η {p = p} {p' = idp} q =
        ap ↓-app=cst-in'
          ( ∙-assoc (↓-app=cst-out' q) WedgeToProduct.glue-β (! WedgeToProduct.glue-β)
          ∙ ap (↓-app=cst-out' q ∙_) (!-inv-r WedgeToProduct.glue-β)
          ∙ ∙-unit-r (↓-app=cst-out' q))
      ∙ ↓-app=cst-η' q

module Fold {i} {X : Ptd i} = ⊙WedgeRec (⊙idf X) (⊙idf X)
fold = Fold.f
⊙fold = Fold.⊙f

module _ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'}
  (fX : X ⊙→ X') (fY : Y ⊙→ Y') where

  wedge-span-map : SpanMap (wedge-span X Y) (wedge-span X' Y')
  wedge-span-map = span-map (fst fX) (fst fY) (idf _)
                      (comm-sqr λ _ → snd fX)
                      (comm-sqr λ _ → snd fY)

  module WedgeFmap where
    private
      module M = PushoutFmap wedge-span-map
    f = M.f
    glue-β = M.glue-β unit

  ∨-fmap : X ∨ Y → X' ∨ Y'
  ∨-fmap = WedgeFmap.f

  ⊙∨-fmap : X ⊙∨ Y ⊙→ X' ⊙∨ Y'
  ⊙∨-fmap = ∨-fmap , ap winl (snd fX)

  Wedge-fmap = ∨-fmap
  ⊙Wedge-fmap = ⊙∨-fmap

module _ {i₀ i₁ i₂ j₀ j₁ j₂} {X₀ : Ptd i₀} {X₁ : Ptd i₁} {X₂ : Ptd i₂}
  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {Y₂ : Ptd j₂}
  where

  ∨-fmap-∘ :
    (gX : X₁ ⊙→ X₂) (fX : X₀ ⊙→ X₁)
    (gY : Y₁ ⊙→ Y₂) (fY : Y₀ ⊙→ Y₁)
    → ∨-fmap (gX ⊙∘ fX) (gY ⊙∘ fY) ∼ ∨-fmap gX gY ∘ ∨-fmap fX fY
  ∨-fmap-∘ (gX , idp) (fX , idp) (gY , idp) (fY , idp) =
    Pushout-fmap-∘ (wedge-span-map (gX , idp) (gY , idp)) (wedge-span-map (fX , idp) (fY , idp))

  ⊙∨-fmap-∘ :
    (gX : X₁ ⊙→ X₂) (fX : X₀ ⊙→ X₁)
    (gY : Y₁ ⊙→ Y₂) (fY : Y₀ ⊙→ Y₁)
    → ⊙∨-fmap (gX ⊙∘ fX) (gY ⊙∘ fY) ⊙∼ ⊙∨-fmap gX gY ⊙∘ ⊙∨-fmap fX fY
  ⊙∨-fmap-∘ (gX , idp) (fX , idp) (gY , idp) (fY , idp) =
    ∨-fmap-∘ (gX , idp) (fX , idp) (gY , idp) (fY , idp) , idp

  Wedge-fmap-∘ = ∨-fmap-∘
  ⊙Wedge-fmap-∘ = ⊙∨-fmap-∘

module _ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'}
  (eqX : X ⊙≃ X') (eqY : Y ⊙≃ Y') where

  wedge-span-emap : SpanEquiv (wedge-span X Y) (wedge-span X' Y')
  wedge-span-emap = wedge-span-map (⊙–> eqX) (⊙–> eqY)
                  , snd eqX , snd eqY , idf-is-equiv _

  ∨-emap : X ∨ Y ≃ X' ∨ Y'
  ∨-emap = Pushout-emap wedge-span-emap

  ⊙∨-emap : X ⊙∨ Y ⊙≃ X' ⊙∨ Y'
  ⊙∨-emap = ≃-to-⊙≃ ∨-emap (ap winl (⊙–>-pt eqX))

  Wedge-emap = ∨-emap
  ⊙Wedge-emap = ⊙∨-emap

module _ {i i' j j' k} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j}
  {Y' : Ptd j'} {Z : Ptd k} (winl* : X' ⊙→ Z) (winr* : Y' ⊙→ Z)
  (f : X ⊙→ X') (g : Y ⊙→ Y') where

  ⊙Wedge-rec-fmap :
       ⊙Wedge-rec winl* winr* ⊙∘ ⊙∨-fmap f g
    ⊙∼ ⊙Wedge-rec (winl* ⊙∘ f) (winr* ⊙∘ g)
  ⊙Wedge-rec-fmap =
    Wedge-elim (λ _ → idp) (λ _ → idp) (↓-='-in' $ ! $ lemma₀ winl* winr* f g) ,
    lemma₁ winl* winr* f
    where
      abstract
        lemma₀ : ∀ {X' Y' Z} (winl* : X' ⊙→ Z) (winr* : Y' ⊙→ Z)
          (f : X ⊙→ X') (g : Y ⊙→ Y')
          →  ap (⊙WedgeRec.f winl* winr* ∘ ∨-fmap f g) wglue
          == ap (⊙WedgeRec.f (winl* ⊙∘ f) (winr* ⊙∘ g)) wglue
        lemma₀ (winl* , idp) (winr* , winr*-pt) (f , idp) (g , idp) =
          ap (Wedge-rec winl* winr* (! winr*-pt) ∘ ∨-fmap (f , idp) (g , idp)) wglue
            =⟨ ap-∘ (Wedge-rec winl* winr* (! winr*-pt)) (∨-fmap (f , idp) (g , idp)) wglue ⟩
          ap (Wedge-rec winl* winr* (! winr*-pt)) (ap (∨-fmap (f , idp) (g , idp)) wglue)
            =⟨ ap (ap (Wedge-rec winl* winr* (! winr*-pt))) $ WedgeFmap.glue-β (f , idp) (g , idp) ⟩
          ap (Wedge-rec winl* winr* (! winr*-pt)) wglue
            =⟨ WedgeRec.glue-β winl* winr* (! winr*-pt) ⟩
          ! winr*-pt
            =⟨ ! $ WedgeRec.glue-β (winl* ∘ f) (winr* ∘ g) (! winr*-pt) ⟩
          ap (Wedge-rec (winl* ∘ f) (winr* ∘ g) (! winr*-pt)) wglue
            =∎

        lemma₁ : ∀ {X' Z} (winl* : X' ⊙→ Z) (winr* : Y' ⊙→ Z) (f : X ⊙→ X')
          →  snd (⊙Wedge-rec winl* winr* ⊙∘ ⊙∨-fmap f g)
          == snd (⊙Wedge-rec (winl* ⊙∘ f) (winr* ⊙∘ g))
        lemma₁ (f , idp) _ (winl* , idp) = idp
  ⊙∨-rec-fmap = ⊙Wedge-rec-fmap

module _ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j}
  {Y' : Ptd j'} (f : X ⊙→ X') (g : Y ⊙→ Y') where

  ⊙projl-fmap : ⊙projl ⊙∘ ⊙∨-fmap f g ⊙∼ ⊙Wedge-rec f ⊙cst
  ⊙projl-fmap =
    Wedge-elim (λ _ → idp) (λ _ → idp) (↓-='-in' $ ! $ lemma₀ f g) , lemma₁ f g
    where
      abstract
        lemma₀ : ∀ {X' Y'} (f : X ⊙→ X') (g : Y ⊙→ Y')
          →  ap (projl ∘ ∨-fmap f g) wglue
          == ap (⊙WedgeRec.f f ⊙cst) wglue
        lemma₀ (f , idp) (g , idp) =
          ap (projl ∘ ∨-fmap (f , idp) (g , idp)) wglue
            =⟨ ap-∘ projl (∨-fmap (f , idp) (g , idp)) wglue ⟩
          ap projl (ap (∨-fmap (f , idp) (g , idp)) wglue)
            =⟨ ap (ap projl) (WedgeFmap.glue-β (f , idp) (g , idp)) ⟩
          ap projl wglue
            =⟨ Projl.glue-β ⟩
          idp
            =⟨ ! $ ⊙WedgeRec.glue-β (f , idp) ⊙cst ⟩
          ap (⊙WedgeRec.f (f , idp) ⊙cst) wglue
            =∎

        lemma₁ : ∀ {X' Y'} (f : X ⊙→ X') (g : Y ⊙→ Y')
          →  snd (⊙projl ⊙∘ ⊙∨-fmap f g)
          == snd (⊙Wedge-rec {Y = Y} f ⊙cst)
        lemma₁ (f , idp) (g , idp) = idp

  ⊙projr-fmap : ⊙projr ⊙∘ ⊙∨-fmap f g ⊙∼ ⊙Wedge-rec ⊙cst g
  ⊙projr-fmap =
    Wedge-elim (λ _ → idp) (λ _ → idp) (↓-='-in' $ ! $ lemma₀ f g) , lemma₁ f g
    where
      abstract
        lemma₀ : ∀ {X' Y'} (f : X ⊙→ X') (g : Y ⊙→ Y')
          →  ap (projr ∘ ∨-fmap f g) wglue
          == ap (⊙WedgeRec.f ⊙cst g) wglue
        lemma₀ (f , idp) (g , idp) =
          ap (projr ∘ ∨-fmap (f , idp) (g , idp)) wglue
            =⟨ ap-∘ projr (∨-fmap (f , idp) (g , idp)) wglue ⟩
          ap projr (ap (∨-fmap (f , idp) (g , idp)) wglue)
            =⟨ ap (ap projr) (WedgeFmap.glue-β (f , idp) (g , idp)) ⟩
          ap projr wglue
            =⟨ Projr.glue-β ⟩
          idp
            =⟨ ! $ ⊙WedgeRec.glue-β ⊙cst (g , idp) ⟩
          ap (⊙WedgeRec.f ⊙cst (g , idp)) wglue
            =∎

        lemma₁ : ∀ {X' Y'} (f : X ⊙→ X') (g : Y ⊙→ Y')
          →  snd (⊙projr ⊙∘ ⊙∨-fmap f g)
          == snd (⊙Wedge-rec {X = X} ⊙cst g)
        lemma₁ (f , idp) (g , idp) = idp

module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (f : X ⊙→ Z) (g : Y ⊙→ Z) where

  {- favonia: This is a special case, but still proved separately to make sure
     it has good computational content. (Maybe this is overkilling.) -}
  ⊙fold-fmap : ⊙fold ⊙∘ ⊙∨-fmap f g ⊙∼ ⊙Wedge-rec f g
  ⊙fold-fmap =
    Wedge-elim (λ _ → idp) (λ _ → idp) (↓-='-in' $ ! $ lemma₀ f g) , lemma₁ f g
    where
      abstract
        lemma₀ : ∀ {Z} (f : X ⊙→ Z) (g : Y ⊙→ Z)
          →  ap (⊙WedgeRec.f (⊙idf _) (⊙idf _) ∘ ∨-fmap f g) wglue
          == ap (⊙WedgeRec.f f g) wglue
        lemma₀ (f , idp) (g , g-pt) =
          ap (⊙WedgeRec.f (⊙idf _) (⊙idf _) ∘ ∨-fmap (f , idp) (g , g-pt)) wglue
            =⟨ ap-∘
                (⊙WedgeRec.f (⊙idf _) (⊙idf _))
                (∨-fmap (f , idp) (g , g-pt))
                wglue ⟩
          ap (⊙WedgeRec.f (⊙idf _) (⊙idf _)) (ap (∨-fmap (f , idp) (g , g-pt)) wglue)
            =⟨ ap (ap (⊙WedgeRec.f (⊙idf _) (⊙idf _)))
                  (WedgeFmap.glue-β (f , idp) (g , g-pt)) ⟩
          ap (⊙WedgeRec.f (⊙idf _) (⊙idf _)) (wglue ∙' ap winr (! g-pt))
            =⟨ ap-∙' (⊙WedgeRec.f (⊙idf _) (⊙idf _)) wglue (ap winr (! g-pt)) ⟩
          ap (⊙WedgeRec.f (⊙idf _) (⊙idf _)) wglue
            ∙' ap (⊙WedgeRec.f (⊙idf _) (⊙idf _)) (ap winr (! g-pt))
            =⟨ ap2 _∙'_
                (⊙WedgeRec.glue-β (⊙idf _) (⊙idf _))
                ( ∘-ap (⊙WedgeRec.f (⊙idf _) (⊙idf _)) winr (! g-pt)
                ∙ ap-idf (! g-pt)) ⟩
          idp ∙' ! g-pt
            =⟨ ∙'-unit-l (! g-pt) ⟩
          ! g-pt
            =⟨ ! $ ⊙WedgeRec.glue-β (f , idp) (g , g-pt) ⟩
          ap (⊙WedgeRec.f (f , idp) (g , g-pt) ) wglue
            =∎

        lemma₁ : ∀ {Z} (f : X ⊙→ Z) (g : Y ⊙→ Z)
          →  snd (⊙Wedge-rec (⊙idf _) (⊙idf _) ⊙∘ ⊙∨-fmap f g)
          == snd (⊙Wedge-rec f g)
        lemma₁ (f , idp) (g , g-pt) = idp

module _ {i j k} (X : Ptd i) (Y : Ptd j) (Z : Ptd k) where

  module WedgeAssocInl = WedgeRec {C = X ∨ (Y ⊙∨ Z)} winl (winr ∘ winl) wglue
  module WedgeAssoc = WedgeRec {X = X ⊙∨ Y} WedgeAssocInl.f (winr ∘ winr) (wglue ∙ ap winr wglue)

  ∨-assoc : (X ⊙∨ Y) ∨ Z ≃ X ∨ (Y ⊙∨ Z)
  ∨-assoc = equiv to from to-from from-to where

    to : (X ⊙∨ Y) ∨ Z → X ∨ (Y ⊙∨ Z)
    to = WedgeAssoc.f

    module FromInr = WedgeRec {C = (X ⊙∨ Y) ∨ Z} (winl ∘ winr) winr (! (ap winl wglue) ∙ wglue)
    module From = WedgeRec {Y = Y ⊙∨ Z} (winl ∘ winl) FromInr.f (ap winl wglue)

    from : X ∨ (Y ⊙∨ Z) → (X ⊙∨ Y) ∨ Z
    from = From.f

    abstract
      to-from : ∀ x → to (from x) == x
      to-from = Wedge-elim
        (λ x → idp)
        (Wedge-elim (λ y → idp) (λ z → idp) $ ↓-='-in' $ ! $
          ap (to ∘ FromInr.f) wglue
            =⟨ ap-∘ to FromInr.f wglue ⟩
          ap to (ap FromInr.f wglue)
            =⟨ ap (ap to) FromInr.glue-β ⟩
          ap to (! (ap winl wglue) ∙ wglue)
            =⟨ ap-∙ to (! (ap winl wglue)) wglue ⟩
          ap to (! (ap winl wglue)) ∙ ap to wglue
            =⟨ _∙2_ (ap-! to (ap winl wglue) ∙ ap ! (∘-ap to winl wglue ∙ WedgeAssocInl.glue-β)) WedgeAssoc.glue-β ⟩
          ! wglue ∙ wglue ∙ ap winr wglue
            =⟨ ! $ ∙-assoc (! wglue) wglue (ap winr wglue) ⟩
          (! wglue ∙ wglue) ∙ ap winr wglue
            =⟨ ap (_∙ ap winr wglue) (!-inv-l wglue) ⟩
          ap winr wglue
            =∎)
        (↓-∘=idf-in' to from (ap (ap to) From.glue-β ∙ ∘-ap to winl wglue ∙ WedgeAssocInl.glue-β))

      from-to : ∀ x → from (to x) == x
      from-to = Wedge-elim
        (Wedge-elim (λ x → idp) (λ y → idp) $ ↓-='-in' $ ! $
          ap-∘ from WedgeAssocInl.f wglue ∙ ap (ap from) WedgeAssocInl.glue-β ∙ From.glue-β)
        (λ z → idp)
        (↓-∘=idf-in' from to $
          ap from (ap to wglue)
            =⟨ ap (ap from) WedgeAssoc.glue-β ⟩
          ap from (wglue ∙ ap winr wglue)
            =⟨ ap-∙ from wglue (ap winr wglue) ⟩
          ap from wglue ∙ ap from (ap winr wglue)
            =⟨ From.glue-β ∙2 (∘-ap from winr wglue ∙ FromInr.glue-β) ⟩
          ap winl wglue ∙ ! (ap winl wglue) ∙ wglue
            =⟨ ! $ ∙-assoc (ap winl wglue) (! (ap winl wglue)) wglue ⟩
          (ap winl wglue ∙ ! (ap winl wglue)) ∙ wglue
            =⟨ ap (_∙ wglue) (!-inv-r (ap winl wglue)) ⟩
          wglue
            =∎)

  ⊙∨-assoc : (X ⊙∨ Y) ⊙∨ Z ⊙≃ X ⊙∨ (Y ⊙∨ Z)
  ⊙∨-assoc = ≃-to-⊙≃ ∨-assoc idp

{-
module _ {i₀ i₁ j₀ j₁ k₀ k₁}
  {X₀ : Ptd i₀} {Y₀ : Ptd j₀} {Z₀ : Ptd k₀}
  {X₁ : Ptd i₁} {Y₁ : Ptd j₁} {Z₁ : Ptd k₁}
  where

  ⊙∨-assoc-nat : ∀ (f : X₀ ⊙→ X₁) (g : Y₀ ⊙→ Y₁) (h : Z₀ ⊙→ Z₁)
    →  ⊙–> (⊙∨-assoc X₁ Y₁ Z₁) ⊙∘ ⊙∨-fmap (⊙∨-fmap f g) h
    ⊙∼ ⊙∨-fmap f (⊙∨-fmap g h) ⊙∘ ⊙–> (⊙∨-assoc X₀ Y₀ Z₀)
  ⊙∨-assoc-nat (f , idp) (g , idp) (h , idp) =
    (Wedge-elim
      -- {P = –> (∨-assoc X₁ Y₁ Z₁) ∘ ∨-fmap (⊙∨-fmap f g) h ∼ ∨-fmap f (⊙∨-fmap g h) ∘ –> (∨-assoc X₀ Y₀ Z₀)}
      (Wedge-elim (λ _ → idp) (λ _ → idp)
        (↓-='-in' $
          ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp)) ∘ WedgeAssocInl.f X₀ Y₀ Z₀) wglue
            =⟨ ap-∘ (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) (WedgeAssocInl.f X₀ Y₀ Z₀) wglue ⟩
          ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) (ap (WedgeAssocInl.f X₀ Y₀ Z₀) wglue)
            =⟨ ap (ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp)))) (WedgeAssocInl.glue-β X₀ Y₀ Z₀) ⟩
          ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) wglue
            =⟨ WedgeFmap.glue-β (f , idp) (⊙∨-fmap (g , idp) (h , idp)) ⟩
          wglue
            =⟨ ! $ WedgeAssocInl.glue-β X₁ Y₁ Z₁ ⟩
          ap (WedgeAssocInl.f X₁ Y₁ Z₁) wglue
            =⟨ ! $ ap (ap (WedgeAssocInl.f X₁ Y₁ Z₁)) $ WedgeFmap.glue-β (f , idp) (g , idp) ⟩
          ap (WedgeAssocInl.f X₁ Y₁ Z₁) (ap (∨-fmap (f , idp) (g , idp)) wglue)
            =⟨ ∘-ap (WedgeAssocInl.f X₁ Y₁ Z₁) (∨-fmap (f , idp) (g , idp)) wglue ⟩
          ap (WedgeAssocInl.f X₁ Y₁ Z₁ ∘ ∨-fmap (f , idp) (g , idp)) wglue
            =∎))
      (λ _ → idp)
      (↓-='-in' $
        ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp)) ∘ WedgeAssoc.f X₀ Y₀ Z₀) wglue
          =⟨ ap-∘ (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) (WedgeAssoc.f X₀ Y₀ Z₀) wglue ⟩
        ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) (ap (WedgeAssoc.f X₀ Y₀ Z₀) wglue)
          =⟨ ap (ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp)))) (WedgeAssoc.glue-β X₀ Y₀ Z₀) ⟩
        ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) (wglue ∙ ap winr wglue)
          =⟨ ap-∙ (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) wglue (ap winr wglue) ⟩
        ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) wglue
        ∙ ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) (ap winr wglue)
          =⟨ ap2 _∙_
               (WedgeFmap.glue-β (f , idp) (⊙∨-fmap (g , idp) (h , idp)))
               ( ∘-ap (∨-fmap (f , idp) (⊙∨-fmap (g , idp) (h , idp))) winr wglue
               ∙ ap-∘ winr (∨-fmap (g , idp) (h , idp)) wglue
               ∙ ap (ap winr) (WedgeFmap.glue-β (g , idp) (h , idp))) ⟩
        wglue ∙ ap winr wglue
          =⟨ ! $ WedgeAssoc.glue-β X₁ Y₁ Z₁ ⟩
        ap (WedgeAssoc.f X₁ Y₁ Z₁) wglue
          =⟨ ! $ ap (ap (WedgeAssoc.f X₁ Y₁ Z₁)) $ WedgeFmap.glue-β (⊙∨-fmap (f , idp) (g , idp)) (h , idp) ⟩
        ap (WedgeAssoc.f X₁ Y₁ Z₁) (ap (∨-fmap (⊙∨-fmap (f , idp) (g , idp)) (h , idp)) wglue)
          =⟨ ∘-ap (WedgeAssoc.f X₁ Y₁ Z₁) (∨-fmap (⊙∨-fmap (f , idp) (g , idp)) (h , idp)) wglue ⟩
        ap (WedgeAssoc.f X₁ Y₁ Z₁ ∘ ∨-fmap (⊙∨-fmap (f , idp) (g , idp)) (h , idp)) wglue
          =∎))
    ,
    idp
-}

module _ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (f : X ⊙→ W) (g : Y ⊙→ W) (h : Z ⊙→ W) where

  ⊙Wedge-rec-assoc : ⊙Wedge-rec (⊙Wedge-rec f g) h
    ⊙∼ ⊙Wedge-rec f (⊙Wedge-rec g h) ⊙∘ ⊙–> (⊙∨-assoc X Y Z)
  ⊙Wedge-rec-assoc =
    (Wedge-elim
      (Wedge-elim (λ x → idp) (λ y → idp)
        (↓-='-in' $
            ap-∘ (⊙WedgeRec.f f (⊙Wedge-rec g h)) (WedgeAssocInl.f X Y Z) wglue
          ∙ ap (ap (⊙WedgeRec.f f (⊙Wedge-rec g h))) (WedgeAssocInl.glue-β X Y Z)
          ∙ ⊙WedgeRec.glue-β f (⊙Wedge-rec g h)
          ∙ ! (⊙WedgeRec.glue-β f g)))
      (λ z → idp)
      (↓-='-in' $
          ap-∘ (⊙WedgeRec.f f (⊙Wedge-rec g h)) (WedgeAssoc.f X Y Z) wglue
        ∙ ap (ap (⊙WedgeRec.f f (⊙Wedge-rec g h))) (WedgeAssoc.glue-β X Y Z)
        ∙ ap-∙ (⊙WedgeRec.f f (⊙Wedge-rec g h)) wglue (ap winr wglue)
        ∙ _∙2_ (⊙WedgeRec.glue-β f (⊙Wedge-rec g h))
               ( ∘-ap (⊙WedgeRec.f f (⊙Wedge-rec g h)) winr wglue
               ∙ ⊙WedgeRec.glue-β g h)
        ∙ ∙-assoc (snd f) (! (snd g)) (snd g ∙ ! (snd h))
        ∙ ap (snd f ∙_) (! $ ∙-assoc (! (snd g)) (snd g) (! (snd h)))
        ∙ ap (λ p → snd f ∙ p ∙ ! (snd h)) (!-inv-l (snd g))
        ∙ ! (⊙WedgeRec.glue-β (⊙Wedge-rec f g) h)))
    ,
    idp
  ⊙∨-rec-assoc = ⊙Wedge-rec-assoc

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.StrictCats where

-- The (large) 'strict' category of (small) categories.
-- The difference here is that _≈_ is not |NaturalIsomorphism| but |_≈F_|

open import Level
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Category using (Category)
open import Categories.Functor using (Functor; id; _∘F_)
open import Categories.Functor.Equivalence

private
  variable
    o ℓ e : Level

Cats : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔  e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Cats o ℓ e = record
  { Obj       = Category o ℓ e
  ; _⇒_       = Functor
  ; _≈_       = _≡F_
  ; id        = id
  ; _∘_       = _∘F_
  ; assoc     = λ {_ _ _ _ F G H} → ≡F-assoc {F = F} {G} {H}
  ; sym-assoc = λ {_ _ _ _ F G H} → ≡F-sym-assoc {F = F} {G} {H}
  ; identityˡ = ≡F-identityˡ
  ; identityʳ = ≡F-identityʳ
  ; identity² = ≡F-identity²
  ; equiv     = ≡F-equiv
  ; ∘-resp-≈  = ∘F-resp-≡F
  }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Ideals.Definition

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

module Rings.Ideals.Prime.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) where

record PrimeIdeal : Set (a ⊔ c) where
  field
    isPrime : {a b : A} → pred (a * b) → ((pred a) → False) → pred b
    notContained : A
    notContainedIsNotContained : (pred notContained) → False


text:
-- {-# OPTIONS -v interaction:100 #-}
module Issue810 where

record T (A : Set) : Set where
  constructor mkT
  field unT : A

introHid : {A : Set} → T A
introHid = {!!}

data Sg {A : Set} : A → Set where
  sg : (a : A) → Sg a

intro : ∀ {A}{a : A} → Sg a
intro = {!!}

intro′ : ∀ {A}(a : A) → Sg a
intro′ = {!!}


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

module Definition.Typed.Consequences.InverseUniv where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Consequences.Syntactic

import Tools.Sum as Sum
open import Tools.Sum using (_⊎_; inj₁; inj₂)
open import Tools.Product
open import Tools.Empty
open import Tools.Nullary

-- Proposition for terms if they contain a U.
data UFull : Term → Set where
  ∃U  : UFull U
  ∃Π₁ : ∀ {F G} → UFull F → UFull (Π F ▹ G)
  ∃Π₂ : ∀ {F G} → UFull G → UFull (Π F ▹ G)

-- Terms cannot contain U.
noU : ∀ {t A Γ} → Γ ⊢ t ∷ A → ¬ (UFull t)
noU (ℕⱼ x) ()
noU (Πⱼ t ▹ t₁) (∃Π₁ ufull) = noU t ufull
noU (Πⱼ t ▹ t₁) (∃Π₂ ufull) = noU t₁ ufull
noU (var x₁ x₂) ()
noU (lamⱼ x t₁) ()
noU (t ∘ⱼ t₁) ()
noU (zeroⱼ x) ()
noU (sucⱼ t) ()
noU (natrecⱼ x t t₁ t₂) ()
noU (conv t₁ x) ufull = noU t₁ ufull

-- Neutrals cannot contain U.
noUNe : ∀ {A} → Neutral A → ¬ (UFull A)
noUNe (var n) ()
noUNe (∘ₙ neA) ()
noUNe (natrecₙ neA) ()

-- Helper function where if at least one Π-type does not contain U,
-- one of F and H will not contain U and one of G and E will not contain U.
pilem : ∀ {F G H E}
      → (¬ UFull (Π F ▹ G)) ⊎ (¬ UFull (Π H ▹ E))
      → (¬ UFull F) ⊎ (¬ UFull H) × (¬ UFull G) ⊎ (¬ UFull E)
pilem (inj₁ x) = inj₁ (λ x₁ → x (∃Π₁ x₁)) , inj₁ (λ x₁ → x (∃Π₂ x₁))
pilem (inj₂ x) = inj₂ (λ x₁ → x (∃Π₁ x₁)) , inj₂ (λ x₁ → x (∃Π₂ x₁))

-- If type A does not contain U, then A can be a term of type U.
inverseUniv : ∀ {A Γ} → ¬ (UFull A) → Γ ⊢ A → Γ ⊢ A ∷ U
inverseUniv q (ℕⱼ x) = ℕⱼ x
inverseUniv q (Uⱼ x) = ⊥-elim (q ∃U)
inverseUniv q (Πⱼ A ▹ A₁) = Πⱼ inverseUniv (λ x → q (∃Π₁ x)) A ▹ inverseUniv (λ x → q (∃Π₂ x)) A₁
inverseUniv q (univ x) = x

-- If A is a neutral type, then A can be a term of U.
inverseUnivNe : ∀ {A Γ} → Neutral A → Γ ⊢ A → Γ ⊢ A ∷ U
inverseUnivNe neA ⊢A = inverseUniv (noUNe neA) ⊢A

-- Helper function where if at least one type does not contain U, then the
-- equality of types can be an equality of term of type U.
inverseUnivEq′ : ∀ {A B Γ} → (¬ (UFull A)) ⊎ (¬ (UFull B)) → Γ ⊢ A ≡ B → Γ ⊢ A ≡ B ∷ U
inverseUnivEq′ q (univ x) = x
inverseUnivEq′ q (refl x) = refl (inverseUniv (Sum.id q) x)
inverseUnivEq′ q (sym A≡B) = sym (inverseUnivEq′ (Sum.sym q) A≡B)
inverseUnivEq′ (inj₁ x) (trans A≡B A≡B₁) =
  let w = inverseUnivEq′ (inj₁ x) A≡B
      _ , _ , t = syntacticEqTerm w
      y = noU t
  in  trans w (inverseUnivEq′ (inj₁ y) A≡B₁)
inverseUnivEq′ (inj₂ x) (trans A≡B A≡B₁) =
  let w = inverseUnivEq′ (inj₂ x) A≡B₁
      _ , t , _ = syntacticEqTerm w
      y = noU t
  in  trans (inverseUnivEq′ (inj₂ y) A≡B) w
inverseUnivEq′ q (Π-cong x A≡B A≡B₁) =
  let w , e = pilem q
  in  Π-cong x (inverseUnivEq′ w A≡B) (inverseUnivEq′ e A≡B₁)

-- If A is a term of U, then the equality of types is an equality of terms of type U.
inverseUnivEq : ∀ {A B Γ} → Γ ⊢ A ∷ U → Γ ⊢ A ≡ B → Γ ⊢ A ≡ B ∷ U
inverseUnivEq A A≡B = inverseUnivEq′ (inj₁ (noU A)) A≡B

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:
{-# OPTIONS --cubical #-}

module Erased-cubical-Open-public.Cubical where

-- It instantiates and exports code from
-- Erased-cubical-Open-public.Erased.

open import Erased-cubical-Open-public.Erased Set public

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-

   The flattening lemma for pushouts (Lemma 8.5.3 in the HoTT book) proved in a cubical style.

   The proof in the HoTT book (the core lying in Lemma 6.12.2, the flattening lemma for coequalizers)
    consists mostly of long strings of equalities about transport. This proof follows almost
    entirely from definitional equalities involving glue/unglue.

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Pushout.Flattening where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma

open import Cubical.HITs.Pushout.Base

module FlatteningLemma {ℓa ℓb ℓc} {A : Type ℓa} {B : Type ℓb} {C : Type ℓc} (f : A → B) (g : A → C)
                       {ℓ} (F : B → Type ℓ) (G : C → Type ℓ) (e : ∀ a → F (f a) ≃ G (g a)) where

  E : Pushout f g → Type ℓ
  E (inl x) = F x
  E (inr x) = G x
  E (push a i) = ua (e a) i

  Σf : Σ[ a ∈ A ] F (f a) → Σ[ b ∈ B ] F b
  Σf (a , x) = (f a , x)

  Σg : Σ[ a ∈ A ] F (f a) → Σ[ c ∈ C ] G c
  Σg (a , x) = (g a , (e a) .fst x)

  module FlattenIso where

    fwd : Pushout Σf Σg → Σ (Pushout f g) E
    fwd (inl (b , x)) = (inl b , x)
    fwd (inr (c , x)) = (inr c , x)
    fwd (push (a , x) i) = (push a i , ua-gluePt (e a) i x)

    bwd : Σ (Pushout f g) E → Pushout Σf Σg
    bwd (inl b , x) = inl (b , x)
    bwd (inr c , x) = inr (c , x)
    bwd (push a i , x) = hcomp (λ j → λ { (i = i0) → push (a , x) (~ j)
                                        ; (i = i1) → inr (g a , x) })
                               (inr (g a , ua-unglue (e a) i x))

    bwd-fwd : ∀ x → bwd (fwd x) ≡ x
    bwd-fwd (inl (b , x)) = refl
    bwd-fwd (inr (c , x)) = refl
    bwd-fwd (push (a , x) i) j =
      hcomp (λ k → λ { (i = i0) → push (a , ua-gluePt (e a) i0 x) (~ k)
                     ; (i = i1) → inr (g a , ua-gluePt (e a) i1 x)
                     ; (j = i1) → push (a , x) (i ∨ ~ k) })
            (inr (g a , ua-unglue (e a) i (ua-gluePt (e a) i x)))
      -- Note: the (j = i1) case typechecks because of the definitional equalities:
      --  ua-gluePt e i0 x ≡ x , ua-gluePt e i1 x ≡ e .fst x,
      --  ua-unglue-glue : ua-unglue e i (ua-gluePt e i x) ≡ e .fst x

    -- essentially: ua-glue e (i ∨ ~ k) ∘ ua-unglue e i
    sq : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B)
         → SquareP (λ i k → ua e i → ua e (i ∨ ~ k))
      {- i = i0 -} (λ k x → ua-gluePt e (~ k) x)
      {- i = i1 -} (λ k x → x)
      {- k = i0 -} (λ i x → ua-unglue e i x)
      {- k = i1 -} (λ i x → x)
    sq e i k x = ua-glue e (i ∨ ~ k) (λ { ((i ∨ ~ k) = i0) → x })
                                     (inS (ua-unglue e i x))
      -- Note: this typechecks because of the definitional equalities:
      --  ua-unglue e i0 x ≡ e .fst x, ua-glue e i1 _ (inS y) ≡ y, ua-unglue e i1 x ≡ x,
      --  ua-glue-unglue : ua-glue e i (λ { (i = i0) → x }) (inS (ua-unglue e i x)) ≡ x

    fwd-bwd : ∀ x → fwd (bwd x) ≡ x
    fwd-bwd (inl b , x) = refl
    fwd-bwd (inr c , x) = refl
    fwd-bwd (push a i , x) j =
      -- `fwd` (or any function) takes hcomps to comps on a constant family, so we must use a comp here
      comp (λ _ → Σ (Pushout f g) E)
           (λ k → λ { (i = i0) → push a (~ k) , ua-gluePt (e a) (~ k) x
                    ; (i = i1) → inr (g a) , x
                    ; (j = i1) → push a (i ∨ ~ k) , sq (e a) i k x })
            (inr (g a) , ua-unglue (e a) i x)

    isom : Iso (Σ (Pushout f g) E) (Pushout Σf Σg)
    isom = iso bwd fwd bwd-fwd fwd-bwd

  flatten : Σ (Pushout f g) E ≃ Pushout Σf Σg
  flatten = isoToEquiv FlattenIso.isom

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:
module Issue794a where

open import Common.Prelude
open import Common.MAlonzo

postulate A : Set

id : .A → A → A
id x y = y

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{- Definition of vectors. Inspired by the Agda Standard Library -}

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Vec.Base where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.FinData

private
  variable
    ℓ ℓ' : Level

    A : Type ℓ

infixr 5 _∷_

data Vec (A : Type ℓ) : ℕ → Type ℓ where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

-- Basic functions

length : ∀ {n} → Vec A n → ℕ
length {n = n} _ = n

head : ∀ {n} → Vec A (1 + n) → A
head (x ∷ xs) = x

tail : ∀ {n} → Vec A (1 + n) → Vec A n
tail (x ∷ xs) = xs

map : ∀ {A : Type ℓ} {B : Type ℓ'} {n} → (A → B) → Vec A n → Vec B n
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

replicate : ∀ {n} {A : Type ℓ} → A → Vec A n
replicate {n = zero}  x = []
replicate {n = suc n} x = x ∷ replicate x

-- Concatenation

infixr 5 _++_

_++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

concat : ∀ {m n} → Vec (Vec A m) n → Vec A (n · m)
concat []         = []
concat (xs ∷ xss) = xs ++ concat xss

lookup : ∀ {n} {A : Type ℓ} → Fin n → Vec A n → A
lookup zero    (x ∷ xs) = x
lookup (suc i) (x ∷ xs) = lookup i xs


text:
{-# OPTIONS --without-K #-}
module HIT.Interval where

open import PathOperations
open import PathStructure.Id.Tr
open import Types

module I-Definition where
  private
    data #I : Set where
      #0 : #I
      #1 : #I

  I : Set
  I = #I

  0ᵢ : I
  0ᵢ = #0

  1ᵢ : I
  1ᵢ = #1

  postulate
    seg : 0ᵢ ≡ 1ᵢ

  I-ind : ∀ {p} (P : I → Set p)
    (x₀ : P 0ᵢ) (x₁ : P 1ᵢ) (p : tr P seg x₀ ≡ x₁) →
    ∀ i → P i
  I-ind P x₀ x₁ p #0 = x₀
  I-ind P x₀ x₁ p #1 = x₁

  postulate
    I-β-i : ∀ {p} (P : I → Set p)
      (x₀ : P 0ᵢ) (x₁ : P 1ᵢ)
      (p : tr P seg x₀ ≡ x₁) →
      apd (I-ind P x₀ x₁ p) seg ≡ p

  I-rec : ∀ {p} {P : Set p}
    (x₀ x₁ : P) (p : x₀ ≡ x₁)
    (i : I) → P
  I-rec x₀ x₁ p #0 = x₀
  I-rec x₀ x₁ p #1 = x₁

  postulate
    I-β-r : ∀ {p} {P : Set p}
      (x₀ x₁ : P) (p : x₀ ≡ x₁) →
      ap (I-rec x₀ x₁ p) seg ≡ p

open I-Definition public

from-path-space : ∀ {a} {A : Set a} →
  (Σ A λ x → Σ A λ y → x ≡ y) → I → A
from-path-space (x , y , p) = I-rec x y p

to-path-space : ∀ {a} {A : Set a} →
  (I → A) → Σ A λ x → Σ A λ y → x ≡ y
to-path-space f = f 0ᵢ , f 1ᵢ , ap f seg

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties of equivalence closures.
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Closure.Equivalence.Properties where

open import Data.Sum.Base using (inj₁)
open import Function using (_∘′_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Construct.Closure.Equivalence
open import Relation.Binary.Construct.Closure.ReflexiveTransitive as RTrans

module _ {a ℓ} {A : Set a} {_⟶_ : Rel A ℓ} where

  private
    _—↠_ = Star _⟶_
    _↔_  = EqClosure _⟶_

  a—↠b⇒a↔b : ∀ {a b} → a —↠ b → a ↔ b
  a—↠b⇒a↔b = RTrans.map inj₁

  a—↠b⇒b↔a : ∀ {a b} → a —↠ b → b ↔ a
  a—↠b⇒b↔a = symmetric _ ∘′ a—↠b⇒a↔b

  a—↠b&a—↠c⇒b↔c : ∀ {a b c} → a —↠ b → a —↠ c → b ↔ c
  a—↠b&a—↠c⇒b↔c a—↠b b—↠c = a—↠b⇒b↔a a—↠b ◅◅ a—↠b⇒a↔b b—↠c


text:
module Bin-predicates where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (+-identityʳ; +-suc; +-assoc; +-comm)

-- 2進数の表現
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

-- 2進数のインクリメント
inc : Bin → Bin
inc ⟨⟩    = ⟨⟩ I
inc (b O) = b I
inc (b I) = inc b O

-- 自然数から2進数への変換
to : ℕ → Bin
to zero    = ⟨⟩ O
to (suc n) = inc (to n)

-- 2進数から自然数への変換
from : Bin → ℕ
from ⟨⟩    = zero
from (b O) = 2 * (from b)
from (b I) = 2 * (from b) + 1

2*n≡n+n : ∀ (n : ℕ) → 2 * n ≡ n + n
2*n≡n+n n rewrite +-identityʳ n = refl

+-suc-suc : ∀ (m n : ℕ) → (suc m) + (suc n) ≡ suc (suc (m + n))
+-suc-suc m n rewrite +-suc (suc m) n | sym (+-assoc 1 m n) = refl

-- 変換の前後どちらでインクリメントしても結果は等しい
from∘inc≡suc∘from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from∘inc≡suc∘from ⟨⟩ = refl
from∘inc≡suc∘from (b O) rewrite +-suc (from (b O)) zero | +-identityʳ (from (b O)) = refl
from∘inc≡suc∘from (b I) rewrite from∘inc≡suc∘from b | 2*n≡n+n (suc (from b)) | +-suc-suc (from b) (from b) | sym (2*n≡n+n (from b)) | +-comm 1 (2 * (from b)) = refl

data One : Bin → Set where
  ⟨⟩I : One (⟨⟩ I)
  _O : ∀ {b : Bin} → One b → One (b O)
  _I : ∀ {b : Bin} → One b → One (b I)

data Can : Bin → Set where
  ⟨⟩O : Can (⟨⟩ O)
  can : ∀ {b : Bin} → One b → Can b

-- Can b
-- ------------
-- Can (inc b)

inc-one : ∀ {b : Bin} → One b → One (inc b)
inc-one ⟨⟩I    = ⟨⟩I O
inc-one (ob O) = ob I
inc-one (ob I) = (inc-one ob) O

inc-can : ∀ {b : Bin} → Can b → Can (inc b)
inc-can ⟨⟩O          = can ⟨⟩I
inc-can (can ⟨⟩I)    = can (⟨⟩I O)
inc-can (can (ob O)) = can (ob I)
inc-can (can (ob I)) = can (inc-one (ob I))

-- ----------
-- Can (to n)

can-ℕ : ∀ (n : ℕ) → Can (to n)
can-ℕ zero    = ⟨⟩O
can-ℕ (suc n) = inc-can (can-ℕ n)

-- Can b
-- ---------------
-- to (from b) ≡ b

to∘from∘inc≡inc∘to∘from : ∀ (b : Bin) → to (from (inc b)) ≡ inc (to (from b))
to∘from∘inc≡inc∘to∘from ⟨⟩ =
  begin
    to (from (inc ⟨⟩))
  ≡⟨⟩
    to (from (⟨⟩ I))
  ≡⟨⟩
    to 1
  ≡⟨⟩
    ⟨⟩ I
  ≡⟨⟩
    inc ⟨⟩
  ≡⟨⟩
    inc (to zero)
  ≡⟨⟩
    inc (to (from ⟨⟩))
  ∎
to∘from∘inc≡inc∘to∘from (b O) =
  begin
    to (from (inc (b O)))
  ≡⟨⟩
    to (from (b I))
  ≡⟨⟩
    to (2 * (from b) + 1)
  ≡⟨⟩
    to (2 * (from b) + (suc zero))
  ≡⟨ cong to (+-suc (2 * (from b)) zero) ⟩
    to (suc (2 * (from b) + zero))
  ≡⟨ cong (λ 2*fromb → to (suc 2*fromb)) (+-identityʳ (2 * (from b))) ⟩
    to (suc (2 * (from b)))
  ≡⟨⟩
    inc (to (2 * (from b)))
  ≡⟨⟩
    inc (to (from (b O)))
  ∎
to∘from∘inc≡inc∘to∘from (b I) =
  begin
    to (from (inc (b I)))
  ≡⟨⟩
    to (from ((inc b) O))
  ≡⟨⟩
    to (2 * (from (inc b)))
  ≡⟨ cong (λ suc∘fromb → to (2 * suc∘fromb)) (from∘inc≡suc∘from b) ⟩
    to (2 * (suc (from b)))
  ≡⟨ cong to (2*n≡n+n (suc (from b))) ⟩
    to ((suc (from b)) + (suc (from b)))
  ≡⟨ cong to (+-suc-suc (from b) (from b)) ⟩
    to (suc (suc ((from b) + (from b))))
  ≡⟨ cong (λ 2*fromb → to (suc (suc 2*fromb))) (sym (2*n≡n+n (from b))) ⟩
    to (suc (suc (2 * (from b))))
  ≡⟨ cong (λ 2*fromb+1 → to (suc 2*fromb+1)) (+-comm 1 (2 * (from b))) ⟩
    to (suc (2 * (from b) + 1))
  ≡⟨⟩
    to (suc (from (b I)))
  ≡⟨⟩
    inc (to (from (b I)))
  ∎

to∘from : ∀ {b : Bin} → Can b → to (from b) ≡ b
to∘from ⟨⟩O =
  begin
    to (from (⟨⟩ O))
  ≡⟨⟩
    to (2 * from ⟨⟩)
  ≡⟨⟩
    to (2 * zero)
  ≡⟨⟩
    to zero
  ≡⟨⟩
    ⟨⟩ O
  ∎
to∘from (can ⟨⟩I) =
  begin
    to (from (⟨⟩ I))
  ≡⟨⟩
    to (2 * from ⟨⟩ + 1)
  ≡⟨⟩
    to (2 * zero + 1)
  ≡⟨⟩
    to 1
  ≡⟨⟩
    ⟨⟩ I
  ∎
to∘from {b O} (can (ob O)) = {!!} -- TODO
to∘from {b I} (can (ob I)) =
  begin
    to (from (b I))
  ≡⟨⟩
    to (from (inc (b O)))
  ≡⟨ to∘from∘inc≡inc∘to∘from (b O) ⟩
    inc (to (from (b O)))
  ≡⟨ cong inc (to∘from (can (ob O))) ⟩
    inc (b O)
  ≡⟨⟩
    b I
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module Issue1258-2 where

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

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

data Bool : Set where
  true false : Bool

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

_×_ : Set → Set → Set
A × B = Σ A (λ _ → B)

postulate f : (A : Set) -> A -> Bool

record Wrap (A : Set) : Set where
  constructor wrap
  field wrapped : A

data ⊥ : Set where

Foo : Bool -> Set
Foo true  = ⊥
Foo false = ⊥

Alpha : Bool
Stuck = Foo Alpha
Beta : Stuck

test : f (Bool × Wrap Nat) (true , wrap zero) == f (Stuck × Stuck) (Beta , Beta)
Alpha = _
Beta  = _
test  = refl