text:
module Category.Comma where

open import Level
open import Data.Product
open import Category.Core
open import Relation.Binary as B using ()
open import Relation.Binary.Indexed
open import Relation.Binary.Indexed.Extra
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)

_/_ : ∀ {𝒸 ℓ} → (C : Category 𝒸 ℓ) → (b : Category.Object C) → Category 𝒸 ℓ
_/_ {𝒸} {ℓ} C b = record
    { Objects = SliceObjectSetoid
    ; Morphisms = SliceMorphismStructure
    }
    where
        open Category C
        module ObjEq = B.IsEquivalence (B.Setoid.isEquivalence Objects)
        module MorphEq = IsEquivalence (MorphismStructure.isEquivalence Morphisms)

        SliceObject-≈ : B.Rel hom[-, b ] ℓ
        SliceObject-≈ (x , x→b) (y , y→b) = Σ[ x≈y ∈ x ≈o y ] x→b ≈ y→b

        SliceObject-≈-Symmetric : B.Symmetric SliceObject-≈
        SliceObject-≈-Symmetric (≈src , f≈g) = (ObjEq.sym ≈src) , MorphEq.sym f≈g

        SliceObject-≈-Transitive : B.Transitive SliceObject-≈
        SliceObject-≈-Transitive (≈src₁ , f≈g) (≈src₂ , g≈h) =
            (ObjEq.trans ≈src₁ ≈src₂) , (MorphEq.trans f≈g g≈h)

        SliceObject-≈-IsEquivalence : B.IsEquivalence SliceObject-≈
        SliceObject-≈-IsEquivalence = record
            { refl = ObjEq.refl , MorphEq.refl
            ; sym = SliceObject-≈-Symmetric
            ; trans = SliceObject-≈-Transitive
            }

        SliceObjectSetoid : B.Setoid 𝒸 ℓ
        SliceObjectSetoid = record
            { Carrier = hom[-, b ]
            ; _≈_ = SliceObject-≈
            ; isEquivalence = SliceObject-≈-IsEquivalence
            }

        record SliceMorphism (src tar : hom[-, b ]) : Set 𝒸 where

            source : Object
            source = proj₁ src

            target : Object
            target = proj₁ tar

            field
                morphism : source ⇒ target

        SliceMorphism-≈ : Rel (uncurry SliceMorphism) ℓ
        SliceMorphism-≈ {f-src , f-tar} {g-src , g-tar} f g =
            Σ[ source-≈ ∈ SliceObject-≈ f-src g-src ]
            Σ[ target-≈ ∈ SliceObject-≈ f-tar g-tar ]
            morphism f ≈ morphism g
            where
                open SliceMorphism

        module SliceObjectEq = B.IsEquivalence SliceObject-≈-IsEquivalence

        SliceMorphism-≈-Symmetric : Symmetric (uncurry SliceMorphism) SliceMorphism-≈ -- Symmetric SliceMorphism-≈ ?
        SliceMorphism-≈-Symmetric (≈src₁ , ≈src₂ , f≈g) =
            SliceObjectEq.sym ≈src₁ , SliceObjectEq.sym ≈src₂ , MorphEq.sym f≈g

        SliceMorphism-≈-Transitive : Transitive (uncurry SliceMorphism) SliceMorphism-≈ -- Symmetric SliceMorphism-≈ ?
        SliceMorphism-≈-Transitive (≈src₁ , ≈src₂ , f≈g) (≈src₃ , ≈src₄ , g≈h) =
            SliceObjectEq.trans ≈src₁ ≈src₃ ,
            SliceObjectEq.trans ≈src₂ ≈src₄ ,
            MorphEq.trans f≈g g≈h

        SliceMorphism-≈-IsEquivalence : IsEquivalence (uncurry SliceMorphism) SliceMorphism-≈
        SliceMorphism-≈-IsEquivalence = record
            { refl = SliceObjectEq.refl , SliceObjectEq.refl , MorphEq.refl
            ; sym = λ {i} {j} {f} {g} → SliceMorphism-≈-Symmetric {i} {j} {f} {g}
            ; trans = λ {i} {j} {k} {f} {g} {h} → SliceMorphism-≈-Transitive {i} {j} {k} {f} {g} {h} --
            }

        Slice-∘ : ∀ {a b c}
            → SliceMorphism b c
            → SliceMorphism a b
            → SliceMorphism a c
        Slice-∘ f g = record { morphism = morphism f ∘ morphism g }
            where   open SliceMorphism

        Slice-id : ∀ a → SliceMorphism a a
        Slice-id (a , _) = record { morphism = id a }

        SliceMorphismIsMorphism : IsMorphism SliceMorphism-≈ Slice-∘ Slice-id
        SliceMorphismIsMorphism = record
            { assoc = λ f g h → SliceObjectEq.refl , SliceObjectEq.refl , assoc (morphism f) (morphism g) (morphism h)
            ; left-identity = λ f → SliceObjectEq.refl , SliceObjectEq.refl , left-identity (morphism f)
            ; right-identity = λ f → SliceObjectEq.refl , SliceObjectEq.refl , right-identity (morphism f)
            ; cong = λ {x} {y} {u} {v} x≈y u≈v → proj₁ u≈v , proj₁ (proj₂ x≈y) , cong (proj₂ (proj₂ x≈y)) (proj₂ (proj₂ u≈v))
            }
            where
                open IsMorphism isMorphism
                open SliceMorphism
                open import Relation.Binary.Indexed.SetoidReasoning

        SliceMorphismStructure : MorphismStructure 𝒸 ℓ hom[-, b ]
        SliceMorphismStructure = record
            { Carrier = uncurry SliceMorphism
            ; _≈_ = SliceMorphism-≈
            ; isEquivalence = SliceMorphism-≈-IsEquivalence
            ; _∘_ = Slice-∘
            ; id = Slice-id
            ; isMorphism = SliceMorphismIsMorphism
            }

module Comma
    {𝒸₀ ℓ₀ 𝒸₁ ℓ₁ 𝒸₂ ℓ₂ : Level}
    {C : Category 𝒸₀ ℓ₀} {D : Category 𝒸₁ ℓ₁} {E : Category 𝒸₂ ℓ₂}
    (S : Functor C E) (T : Functor D E)
    where

    module C = Category C
    module D = Category D
    module S = Functor S
    module T = Functor T
    open Category E

    module ObjEq = B.IsEquivalence (B.Setoid.isEquivalence Objects)
    module MorphEq = IsEquivalence (MorphismStructure.isEquivalence Morphisms)

    record CommaObject : Set (𝒸₀ ⊔ 𝒸₁ ⊔ 𝒸₂ ⊔ ℓ₂) where
        field
            source : C.Object
            target : D.Object
            morphism : S.mapObject source ⇒ T.mapObject target

    open CommaObject

    CommaObject-≈ : B.Rel CommaObject ℓ₂
    CommaObject-≈ f g =
        Σ[ source-≈ ∈ S.mapObject (source f) ≈o S.mapObject (source g) ]
        Σ[ target-≈ ∈ T.mapObject (target f) ≈o T.mapObject (target g) ]
        morphism f ≈ morphism g

    CommaObject-≈-Symmetric : B.Symmetric CommaObject-≈
    CommaObject-≈-Symmetric (source-≈ , target-≈ , f≈g) =
        (ObjEq.sym source-≈) , (ObjEq.sym target-≈) , (MorphEq.sym f≈g)

    CommaObject-≈-Transitive : B.Transitive CommaObject-≈
    CommaObject-≈-Transitive (source-≈₁ , target-≈₁ , f≈g) (source-≈₂ , target-≈₂ , g≈h)
        =   (ObjEq.trans source-≈₁ source-≈₂) ,
            (ObjEq.trans target-≈₁ target-≈₂) ,
            (MorphEq.trans f≈g g≈h)

    CommaObject-≈-IsEquivalence : B.IsEquivalence CommaObject-≈
    CommaObject-≈-IsEquivalence = record
        { refl = ObjEq.refl , ObjEq.refl , MorphEq.refl
        ; sym = λ {i} {f} → CommaObject-≈-Symmetric {i} {f}
        ; trans = λ {f} {g} {h} → CommaObject-≈-Transitive {f} {g} {h}
        }

    CommaObjects : B.Setoid (𝒸₀ ⊔ 𝒸₁ ⊔ 𝒸₂ ⊔ ℓ₂) ℓ₂
    CommaObjects = record
        { Carrier = CommaObject
        ; _≈_ = CommaObject-≈
        ; isEquivalence = CommaObject-≈-IsEquivalence
        }

    record CommaMorphism (src : CommaObject) (tar : CommaObject) : Set (𝒸₀ ⊔ 𝒸₁ ⊔ 𝒸₂ ⊔ ℓ₂) where
        module SRC = CommaObject src
        module TAR = CommaObject tar
        field
            morphismBetweenSources : S.mapObject SRC.source ⇒ S.mapObject TAR.source
            morphismBetweenTargets : T.mapObject SRC.target ⇒ T.mapObject TAR.target
            commutes : TAR.morphism ∘ morphismBetweenSources ≈ morphismBetweenTargets ∘ SRC.morphism

    open CommaMorphism public

    CommaMorphism-≈ : Rel (uncurry CommaMorphism) ℓ₂
    CommaMorphism-≈ f g =
        (morphismBetweenSources f ≈ morphismBetweenSources g) ×
        (morphismBetweenTargets f ≈ morphismBetweenTargets g)

    CommaMorphism-≈-Symmetric : Symmetric (uncurry CommaMorphism) CommaMorphism-≈
    CommaMorphism-≈-Symmetric (source-≈ , target-≈) = (MorphEq.sym source-≈) , (MorphEq.sym target-≈)

    CommaMorphism-≈-Transitive : Transitive (uncurry CommaMorphism) CommaMorphism-≈
    CommaMorphism-≈-Transitive (source₁-≈ , target₁-≈) (source₂-≈ , target₂-≈) =
        (MorphEq.trans source₁-≈ source₂-≈) , (MorphEq.trans target₁-≈ target₂-≈)

    CommaMorphism-≈-IsEquivalence : IsEquivalence (uncurry CommaMorphism) CommaMorphism-≈
    CommaMorphism-≈-IsEquivalence = record
        { refl = MorphEq.refl , MorphEq.refl
        ; sym = λ {i} {j} {f} {g} → CommaMorphism-≈-Symmetric {i} {j} {f} {g}
        ; trans = λ {i} {j} {k} {f} {g} {h} → CommaMorphism-≈-Transitive {i} {j} {k} {f} {g} {h}
        }

    Comma-∘ : ∀ {a b c}
        → CommaMorphism b c
        → CommaMorphism a b
        → CommaMorphism a c
    Comma-∘ {a} {b} {c} f g = record
        { morphismBetweenSources = morphismBetweenSources f ∘ morphismBetweenSources g
        ; morphismBetweenTargets = morphismBetweenTargets f ∘ morphismBetweenTargets g
        ; commutes =
            begin⟨ setoid ⟩
                morphism c ∘ (morphismBetweenSources f ∘ morphismBetweenSources g)
            ≈⟨ sym (assoc (morphismBetweenSources g) (morphismBetweenSources f) (morphism c)) ⟩
                (morphism c ∘ morphismBetweenSources f) ∘ morphismBetweenSources g
            ≈⟨ cong (commutes f) MorphEq.refl ⟩
                (morphismBetweenTargets f ∘ morphism b) ∘ morphismBetweenSources g
            ≈⟨ assoc (morphismBetweenSources g) (morphism b) (morphismBetweenTargets f) ⟩
                morphismBetweenTargets f ∘ (morphism b ∘ morphismBetweenSources g)
            ≈⟨ cong MorphEq.refl (commutes g) ⟩
                morphismBetweenTargets f ∘ (morphismBetweenTargets g ∘ morphism a)
            ≈⟨ sym (assoc (morphism a) (morphismBetweenTargets g) (morphismBetweenTargets f)) ⟩
                (morphismBetweenTargets f ∘ morphismBetweenTargets g) ∘ morphism a
            ∎
        }
        where
            open CommaMorphism
            open import Relation.Binary.Indexed.SetoidReasoning
            open IsMorphism isMorphism
            open IsEquivalence (MorphismStructure.isEquivalence Morphisms)

    Comma-id : ∀ a → CommaMorphism a a
    Comma-id a = record
        { morphismBetweenSources = id (S.mapObject (source a))
        ; morphismBetweenTargets = id (T.mapObject (target a))
        ; commutes =
            begin⟨ setoid ⟩
                morphism a ∘ id (S.mapObject (source a))
            ≈⟨ right-identity (morphism a) ⟩
                morphism a
            ≈⟨ sym (left-identity (morphism a)) ⟩
                id (T.mapObject (target a)) ∘ morphism a
            ∎
        }
        where
            open IsMorphism isMorphism
            open import Relation.Binary.Indexed.SetoidReasoning
            open IsEquivalence (MorphismStructure.isEquivalence Morphisms)

    CommaMorphismIsMorphism : IsMorphism CommaMorphism-≈ Comma-∘ Comma-id
    CommaMorphismIsMorphism = record
        { assoc = λ f g h →
            assoc (morphismBetweenSources f) (morphismBetweenSources g) (morphismBetweenSources h) ,
            assoc (morphismBetweenTargets f) (morphismBetweenTargets g) (morphismBetweenTargets h)
        ; left-identity = λ f → (left-identity (morphismBetweenSources f)) , (left-identity (morphismBetweenTargets f))
        ; right-identity = λ f → (right-identity (morphismBetweenSources f)) , (right-identity (morphismBetweenTargets f))
        ; cong = λ x≈y u≈v → (cong (proj₁ x≈y) (proj₁ u≈v)) , (cong (proj₂ x≈y) (proj₂ u≈v))
        }
        where open IsMorphism isMorphism

    CommaMorphisms : MorphismStructure (𝒸₀ ⊔ 𝒸₁ ⊔ 𝒸₂ ⊔ ℓ₂) ℓ₂ CommaObject
    CommaMorphisms = record
        { Carrier = uncurry CommaMorphism
        ; _≈_ = CommaMorphism-≈
        ; isEquivalence = CommaMorphism-≈-IsEquivalence
        ; _∘_ = Comma-∘
        ; id = Comma-id
        ; isMorphism = CommaMorphismIsMorphism
        }

--     S     T
--  C --> E <-- D
--
_↓_ : {𝒸₀ ℓ₀ 𝒸₁ ℓ₁ 𝒸₂ ℓ₂ : Level}
    {C : Category 𝒸₀ ℓ₀} {D : Category 𝒸₁ ℓ₁} {E : Category 𝒸₂ ℓ₂}
    → (S : Functor C E) → (T : Functor D E)
    → Category (𝒸₀ ⊔ 𝒸₁ ⊔ 𝒸₂ ⊔ ℓ₂) ℓ₂
S ↓ T = record
    { Objects = Comma'.CommaObjects
    ; Morphisms = Comma'.CommaMorphisms
    }
    where
        module Comma' = Comma S T

max_stars_repo_name: banacorn/categories

max_issues_repo_name: banacorn/categories

max_forks_repo_name: banacorn/categories


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

module Utils where -- thing that currently do not belong anywhere and do not have many dependencies

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`

⊎-swap : ∀{x : Type ℓ} {y : Type ℓ'} → x ⊎ y → y ⊎ x
⊎-swap (inl x) = inr x
⊎-swap (inr x) = inl x

swap : ∀{x : Type ℓ} {y : Type ℓ'} → x × y → y × x
swap (x , y) = (y , x)

curry : ∀{ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : (a : A) → (b : B a) → Type ℓ''}
        → ((p : Σ A B) → C (fst p) (snd p))
        → ((x : A) → (y : B x) → C x y)
curry f x y = f (x , y)

-- NOTE: this is non-hProp logic

-- contraposition : {P : Type ℓ} {Q : Type ℓ'} → (P → Q) → ¬ Q → ¬ P
-- contraposition f ¬q p = ⊥-elim (¬q (f p))

deMorgan₂' : {P : Type ℓ} {Q : Type ℓ'} → ¬(P ⊎ Q) → (¬ P) × (¬ Q)
deMorgan₂' {P = P} {Q = Q} ¬[p⊎q] = (λ p → ⊥-elim (¬[p⊎q] (inl p))) , λ q → ⊥-elim (¬[p⊎q] (inr q))

deMorgan₂-back' : {P : Type ℓ} {Q : Type ℓ'} → (¬ P) × (¬ Q) → ¬(P ⊎ Q)
deMorgan₂-back' (¬p , ¬q) (inl p) = ¬p p
deMorgan₂-back' (¬p , ¬q) (inr q) = ¬q q

-- hPropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
-- hPropRel A B ℓ' = A → B → hProp ℓ'

{- NOTE: there is also `Relation.Binary.PropositionalEquality` where they write:

-- Inspect can be used when you want to pattern match on the result r
-- of some expression e, and you also need to "remember" that r ≡ e.

-- See README.Inspect for an explanation of how/why to use this.

record Reveal_·_is_ {A : Set a} {B : A → Set b}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set (a ⊔ b) where
  constructor [_]
  field eq : f x ≡ y

inspect : ∀ {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

-}

{- NOTE: an example is

plus-eq-with : ∀ m n → Plus-eq m n (m + n)
plus-eq-with m n with m + n | inspect (m +_) n
... | zero  | [ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
... | suc p | [ m+n≡1+p ] = m+n≡1+p

-} -- so this looks like a mechanism for "@-pattern-disribution over `with` cases"

record !_ {ℓ} (X : Type ℓ) : Type ℓ where
  inductive
  constructor !!_ -- map "into"   `!!_  : X → ! X`
  field !!!_ : X  -- map "out of" `!!!_ : ! X → X`
  infix 1 !!!_

open !_ public -- brings !!!_ into scope
infix 1 !!_
infix 1 !_

!-iso : ∀{ℓ} {X : Type ℓ} → Iso (! X) X
Iso.fun      !-iso = !!!_
Iso.inv      !-iso = !!_
Iso.rightInv !-iso = λ      x  → refl
Iso.leftInv  !-iso = λ{ (!! x) → refl }

!-≡ : ∀{ℓ} {X : Type ℓ} → (! X) ≡ X
!-≡ {X = X} = isoToPath !-iso

!-equiv : ∀{ℓ} {X : Type ℓ} → (! X) ≃ X
!-equiv = !!!_ , λ where .equiv-proof x → ((!! x) , refl) , λ{ ((!! y) , p) → λ i → (!! p (~ i)) , (λ j → p (~ i ∨ j)) }

-- `A unfold refl to B` checks `A` and `B` to be definitionally equal (with `refl`) and then uses `B`
--   this allows for a nicer Goal/Have at the very beginning of implementing and when using something
unfold' : ∀{ℓ A} → (x y : A) → _≡_ {ℓ} x y → _
unfold' x y p = y
infix -8 unfold'
syntax unfold' x y p = x unfold p to y
{-# DISPLAY unfold' x y p = p #-}

ext: agda

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --allow-unsolved-metas #-}
module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma

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

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

data All {A : Set} (P : A → Set) : List A → Set where
  []  : All P []
  _∷_ : ∀ {x xs} → P x → All P xs → All P (x ∷ xs)

data Ty : Set where

module Code where

  Schema : List Nat → Set
  Schema = All (λ k → Vec Ty k × Ty)

  data Binder : Set where
    bound unbound : Binder

  Shape : Nat → Set
  Shape n = List (Vec Binder n)

  data Code : Set₁ where
    sg : (A : Set) → (A → Code) → Code
    node : (n : Nat) (shape : Shape n) (wt : Vec Ty n → All (λ _ → Ty) shape → Ty → Set) → Code

module Ctx where
  infixr 4 _,_

  data Ctx : Set where
    ∅ : Ctx
    _,_ : Ctx → Ty → Ctx

  _<><_ : Ctx → List Ty → Ctx
  Γ <>< [] = Γ
  Γ <>< (t ∷ ts) = (Γ , t) <>< ts

module Typed (code : Code.Code) where
  open Code
  open Ctx

  visible : ∀ {n} → Vec Binder n → Vec Ty n → List Ty
  visible []             []       = []
  visible (bound ∷ bs)   (t ∷ ts) = t ∷ visible bs ts
  visible (unbound ∷ bs) (_ ∷ ts) = visible bs ts

  mutual
    data Tm (Γ : Ctx) : Ty → Set where

    data Con (Γ : Ctx) (t : Ty) : Code → Set where
      sg : ∀ {A c} x → Con Γ t (c x) → Con Γ t (sg A c)
      node : ∀ {n shape wt} (ts₀ : Vec Ty n) {ts : All (λ _ → Ty) shape} (es : Children Γ ts₀ ts) →
        {{_ : wt ts₀ ts t}} → Con Γ t (node n shape wt)

    data Children (Γ : Ctx) {n : Nat} (ts₀ : Vec Ty n) : {sh : Shape n} → All (λ _ → Ty) sh → Set where
      [] : Children Γ ts₀ []
      _∷_ : ∀ {bs sh t ts} → Tm (Γ <>< visible bs ts₀) t → Children Γ ts₀ {sh} ts → Children Γ ts₀ {bs ∷ sh} (t ∷ ts)

  module Sem₀ (P : Ctx → Ty → Set) where
    children : ∀ {n} (Γ : Ctx) (ts₀ : Vec Ty n) (shape : List (Vec Binder n)) (ts : All (λ _ → Ty) shape) → Set
    children Γ ts₀ [] [] = ⊤
    children Γ ts₀ (bs ∷ bss) (t ∷ ts) = P (Γ <>< visible bs ts₀ ) t × children Γ ts₀ bss ts

    aux : Code → Set
    aux (sg A k) = (x : A) → aux (k x)
    aux (node n shape wt) = ∀ {Γ t} {ts₀ ts} → children Γ ts₀ shape ts → wt ts₀ ts t → P Γ t

  Sem : (P : Ctx → Ty → Set) → Set
  Sem P = Sem₀.aux P code

open Code

data Phase : Set where
  input : Phase

data `STLC : Phase → Set where
  `let : `STLC input

STLC : Phase → Code
STLC p = sg (`STLC p) aux
  where
    aux : `STLC p → Code
    aux `let = node 1 ((bound ∷ []) ∷ []) λ { (t₀ ∷ _) (t₁ ∷ _) t → ⊤ }

open Ctx

open Typed (STLC input) using (Sem)

ap : Sem λ Γ t → Nat
ap = λ where `let → {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
postulate
  A : Set

record R : Set where
  field
    a : A
  b : A
  b = a
open R

test : A
test = b


text:
module IsFormula where

open import Formula

data IsFormula : Formula → Set
 where
  ⟨_⟩ : (φ : Formula) → IsFormula φ


text:
module LC.Parallel where

open import LC.Base
open import LC.Subst
open import LC.Reduction

open import Data.Nat
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

-- parallel β-reduction
infix 3 _β⇒_
data _β⇒_ : Term → Term → Set where

  β-var : {n : ℕ} → var n β⇒ var n

  β-ƛ : ∀ {M M'} → (M⇒M' : M β⇒ M') → ƛ M β⇒ ƛ M'

  β-∙ : ∀ {M M' N N'} → (M⇒M' : M β⇒ M') → (N⇒N' : N β⇒ N') → M ∙ N β⇒ M' ∙ N'

  β-ƛ-∙ : ∀ {M M' N N'} → (M⇒M' : M β⇒ M') → (N⇒N' : N β⇒ N') → (ƛ M) ∙ N β⇒ M' [ N' ]

-- properties
β⇒identity : ∀ {M} → M β⇒ M
β⇒identity {var x} = β-var
β⇒identity {ƛ M}   = β-ƛ β⇒identity
β⇒identity {M ∙ N} = β-∙ β⇒identity β⇒identity

to-parallel : ∀ {M N} → M β→ N → M β⇒ N
to-parallel β-ƛ-∙       = β-ƛ-∙ β⇒identity β⇒identity
to-parallel (β-ƛ M→N)   = β-ƛ (to-parallel M→N)
to-parallel (β-∙-l M→N) = β-∙ (to-parallel M→N) β⇒identity
to-parallel (β-∙-r M→N) = β-∙ β⇒identity (to-parallel M→N)

from-parallel : ∀ {M N} → M β⇒ N → M β→* N
from-parallel β-var             = ε
from-parallel (β-ƛ M⇒N)         = cong-ƛ (from-parallel M⇒N)
from-parallel (β-∙ M⇒M' N⇒N')   = cong-∙ (from-parallel M⇒M') (from-parallel N⇒N')
from-parallel (β-ƛ-∙ M⇒M' N⇒N') = return β-ƛ-∙ ◅◅ cong-[] (from-parallel M⇒M') (from-parallel N⇒N')

open import Relation.Binary.PropositionalEquality hiding ([_]; preorder)

≡⇒β⇒ : ∀ {M N} → M ≡ N → M β⇒ N
≡⇒β⇒ refl = β⇒identity

module Cong where

  open import LC.Subst.Term
  open import LC.Subst.Var

  β⇒cong-lift-ƛ : ∀ {n i M M' N N'} → M β⇒ M' → N β⇒ N' → (ƛ lift (suc n) i M) ∙ lift n i N β⇒ lift n i (M' [ N' ])
  β⇒cong-lift-ƛ β-var N→N' = {!   !}
  β⇒cong-lift-ƛ (β-ƛ M→M') N→N' = {!  !}
  β⇒cong-lift-ƛ (β-∙ M→M' M→M'') N→N' = {!   !}
  β⇒cong-lift-ƛ (β-ƛ-∙ M→M' M→M'') N→N' = {!    !}

  β⇒cong-lift : ∀ {n i M N} → M β⇒ N → lift n i M β⇒ lift n i N
  β⇒cong-lift β-var = β-var
  β⇒cong-lift (β-ƛ M→N) = β-ƛ (β⇒cong-lift M→N)
  β⇒cong-lift (β-∙ M→M' N→N') = β-∙ (β⇒cong-lift M→M') (β⇒cong-lift N→N')
  β⇒cong-lift (β-ƛ-∙ M→M' N→N') = β⇒cong-lift-ƛ M→M' N→N'

  β⇒cong-subst-var-match : ∀ {n i M N} → M β⇒ N → subst-var (match n i) M β⇒ subst-var (match n i) N
  β⇒cong-subst-var-match {n} {i} M→N with match n i
  ... | Under n<i = β-var
  ... | Exact n≡i = β⇒cong-lift M→N
  ... | Above v v≥i = β-var

  open import Relation.Binary.PropositionalEquality hiding ([_]; preorder)

  module Temp where

    lemma-1 : ∀ i m n o → (ƛ subst-var (match m (suc i)) (var n)) ∙ subst-var (match o i) (var n) ≡ (var m) [ var o ] [ var n / i ]
    lemma-1 i m n o with match m (suc i)
    ... | Under m<i+1 = {!   !}
    ... | Exact m≡i+1 = {!   !}
    ... | Above v v≥i+1 = {!   !}

    lemma-1-1 : ∀ i m n → subst-var (match m (suc i)) (var n) β⇒ {!   !}
    lemma-1-1 i m n = {!   !}

  β⇒cong-[]-ƛ-∙ : ∀ {i M M' N N' O O'} → M β⇒ M' → N β⇒ N' → O β⇒ O' → (ƛ M [ O / suc i ]) ∙ N [ O / i ] β⇒ (M' [ N' ]) [ O' / i ]
  β⇒cong-[]-ƛ-∙ {zero} (β-var {n}) (β-var {m}) (β-var {o}) = {!   !}
  β⇒cong-[]-ƛ-∙ {suc i} (β-var {n}) (β-var {m}) (β-var {o}) = {!   !}
  β⇒cong-[]-ƛ-∙ β-var β-var (β-ƛ O→O') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var β-var (β-∙ O→O' O→O'') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var β-var (β-ƛ-∙ O→O' O→O'') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-ƛ N→N') β-var = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-ƛ N→N') (β-ƛ O→O') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-ƛ N→N') (β-∙ O→O' O→O'') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-ƛ N→N') (β-ƛ-∙ O→O' O→O'') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-∙ N→N' N→N'') β-var = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-∙ N→N' N→N'') (β-ƛ O→O') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-∙ N→N' N→N'') (β-∙ O→O' O→O'') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-∙ N→N' N→N'') (β-ƛ-∙ O→O' O→O'') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-ƛ-∙ N→N' N→N'') β-var = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-ƛ-∙ N→N' N→N'') (β-ƛ O→O') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-ƛ-∙ N→N' N→N'') (β-∙ O→O' O→O'') = {!   !}
  β⇒cong-[]-ƛ-∙ β-var (β-ƛ-∙ N→N' N→N'') (β-ƛ-∙ O→O' O→O'') = {!   !}
  β⇒cong-[]-ƛ-∙ (β-ƛ M→M') N→N' O→O' = {!   !}
  β⇒cong-[]-ƛ-∙ (β-∙ M→M' M→M'') N→N' O→O' = {!   !}
  β⇒cong-[]-ƛ-∙ (β-ƛ-∙ M→M' M→M'') N→N' O→O' = {!   !}

  β⇒cong-[] : ∀ {i M M' N N'} → M β⇒ M' → N β⇒ N' → M [ N / i ] β⇒ M' [ N' / i ]
  β⇒cong-[] {i} (β-var {n}) N→N' = β⇒cong-subst-var-match {n} {i} N→N'
  β⇒cong-[] (β-ƛ M→M') N→N' = β-ƛ (β⇒cong-[] M→M' N→N')
  β⇒cong-[] (β-∙ M→M' M→M'') N→N' = β-∙ (β⇒cong-[] M→M' N→N') (β⇒cong-[] M→M'' N→N')
  β⇒cong-[] (β-ƛ-∙ M→M' M→M'') N→N' = {!   !}
    -- β⇒cong-[]-ƛ-∙ M→M' M→M'' N→N'
    -- β-∙ {!   !} {!   !}

    -- (ƛ M [ N₁ / suc i ]) ∙ N [ N₁ / i ] β⇒ M' [ N' ] [ N'' / i ]

    -- ((ƛ M) ∙ N) → M' [ N' ]
    -- ((ƛ M) ∙ N) [ N₁ / i ] β⇒ M' [ N' ] [ N'' / i ]
    --  M→M' N→N'  !} (β⇒cong-[] M→M'' N→N')

  -- β⇒cong-[] {i} {var x} {.(var x)} {var y} {.(var y)} β-var β-var with match x i
  -- ... | Under x<i = β-var
  -- ... | Exact x≡i = β-var
  -- ... | Above v v≥i = β-var
  -- β⇒cong-[] {i} {var x} {.(var x)} {ƛ N} {.(ƛ _)} β-var (β-ƛ N→N') with match x i
  -- ... | Under x<i = β-var
  -- ... | Exact x≡i = β-ƛ (β⇒cong-lift N→N')
  -- ... | Above v v≥i = β-var
  -- β⇒cong-[] {i} {var x} {.(var x)} {N ∙ O} {N'} β-var N→N' with match x i
  -- ... | Under x<i = β-var
  -- ... | Exact x≡i = {!   !}
  -- ... | Above v v≥i = β-var
  -- β⇒cong-[] {i} {ƛ M} {M'} {N} {N'} M→M' N→N' = {!   !}
  -- β⇒cong-[] {i} {M ∙ K} {M'} {N} {N'} M→M' N→N' = {!   !}

β⇒cong-[] : ∀ {M M' N N'} → M β⇒ M' → N β⇒ N' → M [ N ] β⇒ M' [ N' ]
β⇒cong-[] = Cong.β⇒cong-[]

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
------------------------------------------------------------------------------
-- Conversion functions i, j and k.
------------------------------------------------------------------------------

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

module FOT.FOTC.IJK where

open import FOTC.Base
open import FOTC.Data.Nat.Type

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

data ℕ : Set where
  z : ℕ
  s : ℕ → ℕ

-- Conversion functions from/to ℕ and N.
i : ℕ → D
i z     = zero
i (s n) = succ₁ (i n)

j : (n : ℕ) → N (i n)
j z     = nzero
j (s n) = nsucc (j n)

k : {n : D} → N n → ℕ
k nzero      = z
k (nsucc Nn) = s (k Nn)

_+_ : ℕ → ℕ → ℕ
z   + n = n
s m + n = s (m + n)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bounded vectors
------------------------------------------------------------------------

-- Vectors of a specified maximum length.

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

module Data.BoundedVec where

open import Data.Nat
open import Data.List.Base as List using (List)
open import Data.Vec as Vec using (Vec)
import Data.BoundedVec.Inefficient as Ineff
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Solver
open +-*-Solver

------------------------------------------------------------------------
-- The type

abstract

  data BoundedVec {a} (A : Set a) : ℕ → Set a where
    bVec : ∀ {m n} (xs : Vec A n) → BoundedVec A (n + m)

  [] : ∀ {a n} {A : Set a} → BoundedVec A n
  [] = bVec Vec.[]

  infixr 5 _∷_

  _∷_ : ∀ {a n} {A : Set a} →
        A → BoundedVec A n → BoundedVec A (suc n)
  x ∷ bVec xs = bVec (Vec._∷_ x xs)

------------------------------------------------------------------------
-- Pattern matching

infixr 5 _∷v_

data View {a} (A : Set a) : ℕ → Set a where
  []v  : ∀ {n} → View A n
  _∷v_ : ∀ {n} (x : A) (xs : BoundedVec A n) → View A (suc n)

abstract

  view : ∀ {a n} {A : Set a} → BoundedVec A n → View A n
  view (bVec Vec.[])         = []v
  view (bVec (Vec._∷_ x xs)) = x ∷v bVec xs

------------------------------------------------------------------------
-- Increasing the bound

abstract

  ↑ : ∀ {a n} {A : Set a} → BoundedVec A n → BoundedVec A (suc n)
  ↑ {A = A} (bVec {m = m} {n = n} xs) =
    subst (BoundedVec A) lemma
            (bVec {m = suc m} xs)
    where
    lemma : n + (1 + m) ≡ 1 + (n + m)
    lemma = solve 2 (λ m n → n :+ (con 1 :+ m)  :=  con 1 :+ (n :+ m))
                    refl m n

------------------------------------------------------------------------
-- Conversions

module _ {a} {A : Set a} where

 abstract

  fromList : (xs : List A) → BoundedVec A (List.length xs)
  fromList xs =
    subst (BoundedVec A) lemma
            (bVec {m = zero} (Vec.fromList xs))
    where
    lemma : List.length xs + 0 ≡ List.length xs
    lemma = solve 1 (λ m → m :+ con 0  :=  m) refl _

  toList : ∀ {n} → BoundedVec A n → List A
  toList (bVec xs) = Vec.toList xs

  toInefficient : ∀ {n} → BoundedVec A n → Ineff.BoundedVec A n
  toInefficient xs with view xs
  ... | []v     = Ineff.[]
  ... | y ∷v ys = y Ineff.∷ toInefficient ys

  fromInefficient : ∀ {n} → Ineff.BoundedVec A n → BoundedVec A n
  fromInefficient Ineff.[]       = []
  fromInefficient (x Ineff.∷ xs) = x ∷ fromInefficient xs


text:
primitive
  data D : Set where

-- Bad error message WAS:
-- A postulate block can only contain type signatures or instance blocks


text:
-- Andreas, 2016-07-29 issue #707, comment of 2012-10-31

open import Common.Nat

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

v0 v1 v2 : Vec Nat _
v0 = []
v1 = 0 ∷ v0
v2 = 1 ∷ v1

-- Works, but maybe questionable.
-- The _ is triplicated into three different internal metas.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe --no-universe-polymorphism
            --no-sized-types --no-guardedness --no-subtyping #-}

module Agda.Builtin.Unit where

record ⊤ : Set where
  instance constructor tt

{-# BUILTIN UNIT ⊤ #-}
{-# COMPILE GHC ⊤ = data () (()) #-}


text:
{- The trivial resource -}
module Relation.Ternary.Separation.Construct.Unit where

open import Data.Unit
open import Data.Product

open import Relation.Unary
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality as P
open import Relation.Ternary.Separation

open RawSep
instance unit-raw-sep : RawSep ⊤
_⊎_≣_ unit-raw-sep = λ _ _ _ → ⊤

instance unit-has-sep : IsSep unit-raw-sep
unit-has-sep = record
  { ⊎-comm  = λ _   → tt
  ; ⊎-assoc = λ _ _ → tt , tt , tt
  }

instance unit-is-unital : IsUnitalSep _ _
unit-is-unital = record
  { isSep = unit-has-sep
  ; ⊎-idˡ = tt
  ; ⊎-id⁻ˡ = λ where tt → refl }

instance unit-sep : Separation _
unit-sep = record
  { isSep = unit-has-sep }


text:
{-# OPTIONS --with-K #-}
open import Axiom.Extensionality.Propositional using (Extensionality)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Irrelevant)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Relation.Binary.PropositionalEquality.WithK using (≡-erase)

-- acursed and unmentionable
-- turn back traveller
module AKS.Unsafe where

open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe) public

postulate
  TODO : ∀ {a} {A : Set a} → A
  BOTTOM : ∀ {a} {A : Set a} → A
  .irrelevance : ∀ {a} {A : Set a} -> .A -> A
  ≡-recomp : ∀ {a} {A : Set a} {x y : A} → .(x ≡ y) → x ≡ y
  fun-ext : ∀ {ℓ₁ ℓ₂} → Extensionality ℓ₁ ℓ₂

≡-recomputable : ∀ {a} {A : Set a} {x y : A} → .(x ≡ y) → x ≡ y
≡-recomputable x≡y = ≡-erase (≡-recomp x≡y)

≢-irrelevant : ∀ {a} {A : Set a} → Irrelevant {A = A} _≢_
≢-irrelevant {x} {y} [x≉y]₁ [x≉y]₂ = trustMe

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
    module _ where

    module A where

      postulate
        !_ : Set₂ → Set₃

      infix 1 !_

    module B where

      postulate
        !_ : Set₀ → Set₁

      infix 3 !_

    open A
    open B

    postulate
      #_ : Set₁ → Set₂

    infix 2 #_

    ok₁ : Set₁ → Set₃
    ok₁ X = ! # X

    ok₂ : Set₀ → Set₂
    ok₂ X = # ! X


text:
module foldl where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning

open import lists using (List; []; _∷_; [_,_,_])

foldl : ∀ {A B : Set} → (B → A → B) → B → List A → B
foldl _⊗_ e []       = e
foldl _⊗_ e (x ∷ xs) = foldl _⊗_ (e ⊗ x) xs

test-foldl : ∀ {A B : Set} → (_⊗_ : B → A → B) → (e : B) → (x y z : A)
  → foldl _⊗_ e [ x , y , z ] ≡ ((e ⊗ x) ⊗ y) ⊗ z
test-foldl _⊗_ e x y z = refl

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The extensional sublist relation over setoid equality.
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Binary.Subset.Setoid
  {c ℓ} (S : Setoid c ℓ) where

open import Data.List using (List)
open import Data.List.Membership.Setoid S using (_∈_)
open import Level using (_⊔_)
open import Relation.Nullary using (¬_)

open Setoid S renaming (Carrier to A)

------------------------------------------------------------------------
-- Definitions

infix 4 _⊆_ _⊈_

_⊆_ : Rel (List A) (c ⊔ ℓ)
xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys

_⊈_ : Rel (List A) (c ⊔ ℓ)
xs ⊈ ys = ¬ xs ⊆ ys


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

module MJ.Semantics.Objects.Flat {c}(Ct : Core.Classtable c)(ℂ : Code.Code Ct) where

open import Prelude

open import Level renaming (suc to lsuc; zero to lzero)
open import Data.Vec hiding (_++_; lookup; drop)
open import Data.Star
open import Data.List
open import Data.List.First.Properties
open import Data.List.Membership.Propositional
open import Data.List.Any.Properties
open import Data.List.All as All
open import Data.List.All.Properties.Extra
open import Data.List.Prefix
open import Data.List.Properties.Extra
open import Data.Maybe as Maybe
open import Data.Maybe.Relation.Unary.All as MayAll using ()
open import Data.String using (String)
open import Relation.Binary.PropositionalEquality

open import MJ.Semantics.Values Ct
open import MJ.Semantics.Objects Ct
open import MJ.Syntax Ct
open Code Ct
open Core c
open Classtable Ct
open import MJ.Classtable.Membership Ct

private

  collect : ∀ {cid}(chain : Σ ⊢ cid <: Object) ns → List (String × typing ns)
  collect (super {cid} ◅ ch) ns = Class.decls (Σ (cls cid)) ns ++ collect ch ns
  collect ε ns = Class.decls (Σ Object) ns

  {-
  We define collect members by delegation to collection of members over a particular
  inheritance chain.
  This makes the definition structurally recursive and is sound by the fact that
  inheritance chains are unique.
  -}
  collect-members : ∀ cid ns → List (String × typing ns)
  collect-members cid ns = collect (rooted cid) ns

  {-
  An Object is then simply represented by a list of values for all it's members.
  -}
  Obj : (World c) → (cid : _) → Set
  Obj W cid = All (λ d → Val W (proj₂ d)) (collect-members cid FIELD)

  weaken-obj : ∀ {W W'} cid → W' ⊒ W → Obj W cid → Obj W' cid
  weaken-obj cid ext O = All.map (weaken-val ext) O

  {-
  We can relate the flat Object structure with the hierarchical notion of membership
  through the definition of `collect`.
  This allows us to get and set members on Objects.
  -}
  {-# TERMINATING #-}
  getter : ∀ {W n a} cid → Obj W cid → IsMember cid FIELD n a → Val W a
  getter cid O q with rooted cid
  getter .Object O (.Object , ε , def) | ε = ∈-all (proj₁ (first⟶∈ def)) O
  getter .Object O (_ , () ◅ _ , _) | ε
  getter ._ O (._ , ε , def) | super {cid} ◅ z
    with split-++ (Class.decls (Σ (cls _)) FIELD) _ O
  ... | own , inherited = ∈-all (proj₁ (first⟶∈ def)) own
  getter ._ O (pid , super {cid} ◅ s , def) | super ◅ z
    with split-++ (Class.decls (Σ (cls _)) FIELD) _ O
  ... | own , inherited rewrite <:-unique z (rooted (Class.parent (Σ (cls cid)))) =
    getter _ inherited (pid , s , def)

  {-# TERMINATING #-}
  setter : ∀ {W f a} cid → Obj W cid → IsMember cid FIELD f a → Val W a → Obj W cid
  setter (cls cid) O q v with rooted (cls cid)
  setter (cls cid) O (._ , ε , def) v | super ◅ z with split-++ (Class.decls (Σ (cls _)) FIELD) _ O
  ... | own , inherited =
    (own All.[ proj₁ (first⟶∈ def) ]≔ v) ++-all inherited
  setter (cls cid) O (._ , super ◅ s , def) v | super ◅ z with split-++ (Class.decls (Σ (cls _)) FIELD) _ O
  ... | own , inherited rewrite <:-unique z (rooted (Class.parent (Σ (cls cid)))) =
    own ++-all setter _ inherited (_ , s , def) v
  setter Object O mem v = ⊥-elim (∉Object mem)

  {-
  A default object instance can be created for every class simply by tabulating `default`
  over the types of all fields of a class.
  -}
  defaultObject' : ∀ {W cid} → (ch : Σ ⊢ cid <: Object) → All (λ d → Val W (proj₂ d)) (collect ch FIELD)
  defaultObject' ε rewrite Σ-Object = []
  defaultObject' {cid = Object} (() ◅ _)
  defaultObject' {cid = cls x} (super ◅ z) =
    All.tabulate {xs = Class.decls (Σ (cls x)) FIELD} (λ{ {_ , ty} _ → default ty})
    ++-all
    defaultObject' z

{-
We collect these definitions under the abstract ObjEncoding interface for usage in the semantics
-}
encoding : ObjEncoding
encoding = record {
    Obj = Obj ;
    weaken-obj = λ cid ext O → weaken-obj cid ext O ;
    getter = getter ;
    setter = setter ;
    defaultObject = λ cid → defaultObject' (rooted cid)
  }


text:
-- Andreas, 2020-05-01, issue #4631
--
-- We should not allow @-patterns to shadow constructors!

open import Agda.Builtin.Bool

test : Set → Set
test true@_ = true

-- WAS: succees

-- EXPECTED:
--
-- Bool !=< Set
-- when checking that the expression true has type Set
--
-- ———— Warning(s) ————————————————————————————————————————————
-- Name bound in @-pattern ignored because it shadows constructor
-- when scope checking the left-hand side test true@A in the
-- definition of test

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------------
-- Propositional equality on inductive PA
------------------------------------------------------------------------------

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

-- This file contains some definitions which are reexported by
-- PA.Inductive.Base.

module PA.Inductive.Relation.Binary.PropositionalEquality where

open import Common.FOL.FOL using ( ¬_ )
open import PA.Inductive.Base.Core

infix 4 _≡_ _≢_

------------------------------------------------------------------------------
-- The identity type on PA.
data _≡_ (x : ℕ) : ℕ → Set where
  refl : x ≡ x

-- Inequality.
_≢_ : ℕ → ℕ → Set
x ≢ y = ¬ x ≡ y
{-# ATP definition _≢_ #-}

-- Identity properties

sym : ∀ {x y} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
trans refl h = h

subst : (A : ℕ → Set) → ∀ {x y} → x ≡ y → A x → A y
subst A refl Ax = Ax

cong : (f : ℕ → ℕ) → ∀ {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

cong₂ : (f : ℕ → ℕ → ℕ) → ∀ {x x' y y'} → x ≡ y → x' ≡ y' → f x x' ≡ f y y'
cong₂ f refl refl = refl


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

open import lib.Basics

module lib.types.Sigma where

-- Cartesian product
_×_ : ∀ {i j} (A : Type i) (B : Type j) → Type (lmax i j)
A × B = Σ A (λ _ → B)

infixr 5 _×_

module _ {i j} {A : Type i} {B : A → Type j} where

  pair : (a : A) (b : B a) → Σ A B
  pair a b = (a , b)

  -- pair= has already been defined

  fst= : {ab a'b' : Σ A B} (p : ab == a'b') → (fst ab == fst a'b')
  fst= = ap fst

  snd= : {ab a'b' : Σ A B} (p : ab == a'b')
    → (snd ab == snd a'b' [ B ↓ fst= p ])
  snd= {._} {_} idp = idp

  fst=-β : {a a' : A} (p : a == a')
    {b : B a} {b' : B a'} (q : b == b' [ B ↓ p ])
    → fst= (pair= p q) == p
  fst=-β idp idp = idp

  snd=-β : {a a' : A} (p : a == a')
    {b : B a} {b' : B a'} (q : b == b' [ B ↓ p ])
    → snd= (pair= p q) == q [ (λ v → b == b' [ B ↓ v ]) ↓ fst=-β p q ]
  snd=-β idp idp = idp

  pair=-η : {ab a'b' : Σ A B} (p : ab == a'b')
    → p == pair= (fst= p) (snd= p)
  pair=-η {._} {_} idp = idp

  pair== : {a a' : A} {p p' : a == a'} (α : p == p')
           {b : B a} {b' : B a'} {q : b == b' [ B ↓ p ]} {q' : b == b' [ B ↓ p' ]}
           (β : q == q' [ (λ u → b == b' [ B ↓ u ]) ↓ α ])
    → pair= p q == pair= p' q'
  pair== idp idp = idp

module _ {i j} {A : Type i} {B : Type j} where

  fst×= : {ab a'b' : A × B} (p : ab == a'b') → (fst ab == fst a'b')
  fst×= = ap fst

  snd×= : {ab a'b' : A × B} (p : ab == a'b')
    → (snd ab == snd a'b')
  snd×= = ap snd

  fst×=-β : {a a' : A} (p : a == a')
    {b b' : B} (q : b == b')
    → fst×= (pair×= p q) == p
  fst×=-β idp idp = idp

  snd×=-β : {a a' : A} (p : a == a')
    {b b' : B} (q : b == b')
    → snd×= (pair×= p q) == q
  snd×=-β idp idp = idp

  pair×=-η : {ab a'b' : A × B} (p : ab == a'b')
    → p == pair×= (fst×= p) (snd×= p)
  pair×=-η {._} {_} idp = idp

module _ {i j} {A : Type i} {B : A → Type j} where

  =Σ : (x y : Σ A B) → Type (lmax i j)
  =Σ (a , b) (a' , b') = Σ (a == a') (λ p → b == b' [ B ↓ p ])

  =Σ-eqv : (x y : Σ A B) →  (=Σ x y) ≃ (x == y)
  =Σ-eqv x y =
    equiv (λ pq → pair= (fst pq) (snd pq)) (λ p → fst= p , snd= p)
          (λ p → ! (pair=-η p))
          (λ pq → pair= (fst=-β (fst pq) (snd pq)) (snd=-β (fst pq) (snd pq)))

  =Σ-path : (x y : Σ A B) → (=Σ x y) == (x == y)
  =Σ-path x y = ua (=Σ-eqv x y)

Σ= : ∀ {i j} {A A' : Type i} (p : A == A') {B : A → Type j} {B' : A' → Type j}
  (q : B == B' [ (λ X → (X → Type j)) ↓ p ]) → Σ A B == Σ A' B'
Σ= idp idp = idp

abstract

  Σ-level : ∀ {i j} {n : ℕ₋₂} {A : Type i} {P : A → Type j}
    → (has-level n A → ((x : A) → has-level n (P x))
      → has-level n (Σ A P))
  Σ-level {n = ⟨-2⟩} p q =
    ((fst p , (fst (q (fst p)))) ,
      (λ y → pair= (snd p _) (from-transp! _ _ (snd (q _) _))))
  Σ-level {n = S n} p q = λ x y → equiv-preserves-level (=Σ-eqv x y)
    (Σ-level (p _ _)
      (λ _ → equiv-preserves-level ((to-transp-equiv _ _)⁻¹) (q _ _ _)))

  ×-level : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j}
    → (has-level n A → has-level n B → has-level n (A × B))
  ×-level pA pB = Σ-level pA (λ x → pB)

-- Equivalences in a Σ-type

equiv-Σ-fst : ∀ {i j k} {A : Type i} {B : Type j} (P : B → Type k) {h : A → B}
                  → is-equiv h → (Σ A (P ∘ h)) ≃ (Σ B P)
equiv-Σ-fst {A = A} {B = B} P {h = h} e = equiv f g f-g g-f
  where f : Σ A (P ∘ h) → Σ B P
        f (a , r) = (h a , r)

        g : Σ B P → Σ A (P ∘ h)
        g (b , s) = (is-equiv.g e b , transport P (! (is-equiv.f-g e b)) s)

        f-g : ∀ y → f (g y) == y
        f-g (b , s) = pair= (is-equiv.f-g e b) (trans-↓ P (is-equiv.f-g e b) s)

        g-f : ∀ x → g (f x) == x
        g-f (a , r) =
          pair= (is-equiv.g-f e a)
                (transport (λ q → transport P (! q) r == r [ P ∘ h ↓ is-equiv.g-f e a ])
                           (is-equiv.adj e a)
                           (trans-ap-↓ P h (is-equiv.g-f e a) r) )

equiv-Σ-snd : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  → (∀ x → B x ≃ C x) → Σ A B ≃ Σ A C
equiv-Σ-snd {A = A} {B = B} {C = C} k = equiv f g f-g g-f
  where f : Σ A B → Σ A C
        f (a , b) = (a , fst (k a) b)

        g : Σ A C → Σ A B
        g (a , c) = (a , is-equiv.g (snd (k a)) c)

        f-g : ∀ p → f (g p) == p
        f-g (a , c) = pair= idp (is-equiv.f-g (snd (k a)) c)

        g-f : ∀ p → g (f p) == p
        g-f (a , b) = pair= idp (is-equiv.g-f (snd (k a)) b)

-- Two ways of simultaneously applying equivalences in each component.
module _ {i₀ i₁ j₀ j₁} {A₀ : Type i₀} {A₁ : Type i₁}
         {B₀ : A₀ → Type j₀} {B₁ : A₁ → Type j₁} where
  equiv-Σ : (u : A₀ ≃ A₁) (v : ∀ a → B₀ (<– u a) ≃ B₁ a) → Σ A₀ B₀ ≃ Σ A₁ B₁
  equiv-Σ u v = Σ A₀ B₀           ≃⟨ equiv-Σ-fst _ (snd (u ⁻¹)) ⁻¹ ⟩
                Σ A₁ (B₀ ∘ <– u)  ≃⟨ equiv-Σ-snd v ⟩
                Σ A₁ B₁           ≃∎

  equiv-Σ' : (u : A₀ ≃ A₁) (v : ∀ a → B₀ a ≃ B₁ (–> u a)) → Σ A₀ B₀ ≃ Σ A₁ B₁
  equiv-Σ' u v = Σ A₀ B₀           ≃⟨ equiv-Σ-snd v ⟩
                 Σ A₀ (B₁ ∘ –> u)  ≃⟨ equiv-Σ-fst _ (snd u) ⟩
                 Σ A₁ B₁           ≃∎

-- Implementation of [_∙'_] on Σ
Σ-∙' : ∀ {i j} {A : Type i} {B : A → Type j}
  {x y z : A} {p : x == y} {p' : y == z}
  {u : B x} {v : B y} {w : B z}
  (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
  → (pair= p q ∙' pair= p' r) == pair= (p ∙' p') (q ∙'ᵈ r)
Σ-∙' {p = idp} {p' = idp} q idp = idp

-- Implementation of [_∙_] on Σ
Σ-∙ : ∀ {i j} {A : Type i} {B : A → Type j}
  {x y z : A} {p : x == y} {p' : y == z}
  {u : B x} {v : B y} {w : B z}
  (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
  → (pair= p q ∙ pair= p' r) == pair= (p ∙ p') (q ∙ᵈ r)
Σ-∙ {p = idp} {p' = idp} idp r = idp

-- Implementation of [!] on Σ
Σ-! : ∀ {i j} {A : Type i} {B : A → Type j}
  {x y : A} {p : x == y}
  {u : B x} {v : B y}
  (q : u == v [ B ↓ p ])
  → ! (pair= p q) == pair= (! p) (!ᵈ q)
Σ-! {p = idp} idp = idp

-- Implementation of [_∙'_] on ×
×-∙' : ∀ {i j} {A : Type i} {B : Type j}
  {x y z : A} (p : x == y) (p' : y == z)
  {u v w : B} (q : u == v) (q' : v == w)
  → (pair×= p q ∙' pair×= p' q') == pair×= (p ∙' p') (q ∙' q')
×-∙' idp idp q idp = idp

-- Implementation of [_∙_] on ×
×-∙ : ∀ {i j} {A : Type i} {B : Type j}
  {x y z : A} (p : x == y) (p' : y == z)
  {u v w : B} (q : u == v) (q' : v == w)
  → (pair×= p q ∙ pair×= p' q') == pair×= (p ∙ p') (q ∙ q')
×-∙ idp idp idp r = idp

-- Implementation of [!] on ×
×-! : ∀ {i j} {A : Type i} {B : Type j}
  {x y : A} (p : x == y) {u v : B} (q : u == v)
  → ! (pair×= p q) == pair×= (! p) (! q)
×-! idp idp = idp

-- Special case of [ap-,]
ap-cst,id : ∀ {i j} {A : Type i} (B : A → Type j)
  {a : A} {x y : B a} (p : x == y)
  → ap (λ x → _,_ {B = B} a x) p == pair= idp p
ap-cst,id B idp = idp

-- hfiber fst == B
module _ {i j} {A : Type i} {B : A → Type j} where

  private
    to : ∀ a → hfiber (fst :> (Σ A B → A)) a → B a
    to a ((.a , b) , idp) = b

    from : ∀ (a : A) → B a → hfiber (fst :> (Σ A B → A)) a
    from a b = (a , b) , idp

    to-from : ∀ (a : A) (b : B a) → to a (from a b) == b
    to-from a b = idp

    from-to : ∀ a b′ → from a (to a b′) == b′
    from-to a ((.a , b) , idp) = idp

  hfiber-fst : ∀ a → hfiber (fst :> (Σ A B → A)) a ≃ B a
  hfiber-fst a = to a , is-eq (to a) (from a) (to-from a) (from-to a)

{- Dependent paths in a Σ-type -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → B a → Type k}
  where

  ↓-Σ-in : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    (q : r == r' [ B ↓ p ])
    → s == s' [ uncurry C ↓ pair= p q ]
    → (r , s) == (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ]
  ↓-Σ-in {p = idp} idp t = pair= idp t

  ↓-Σ-fst : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    → (r , s) == (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ]
    → r == r' [ B ↓ p ]
  ↓-Σ-fst {p = idp} u = fst= u

  ↓-Σ-snd : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    → (u : (r , s) == (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ])
    → s == s' [ uncurry C ↓ pair= p (↓-Σ-fst u) ]
  ↓-Σ-snd {p = idp} idp = idp

  ↓-Σ-β-fst : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    (q : r == r' [ B ↓ p ])
    (t : s == s' [ uncurry C ↓ pair= p q ])
    → ↓-Σ-fst (↓-Σ-in q t) == q
  ↓-Σ-β-fst {p = idp} idp idp = idp

  ↓-Σ-β-snd : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    (q : r == r' [ B ↓ p ])
    (t : s == s' [ uncurry C ↓ pair= p q ])
    → ↓-Σ-snd (↓-Σ-in q t) == t
      [ (λ q' → s == s' [ uncurry C ↓ pair= p q' ]) ↓ ↓-Σ-β-fst q t ]
  ↓-Σ-β-snd {p = idp} idp idp = idp

  ↓-Σ-η : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    (u : (r , s) == (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ])
    → ↓-Σ-in (↓-Σ-fst u) (↓-Σ-snd u) == u
  ↓-Σ-η {p = idp} idp = idp

{- Dependent paths in a ×-type -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  where

  ↓-×-in : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x} {s' : C x'}
    → r == r' [ B ↓ p ]
    → s == s' [ C ↓ p ]
    → (r , s) == (r' , s') [ (λ x → B x × C x) ↓ p ]
  ↓-×-in {p = idp} q t = pair×= q t

module _ where
  -- An orphan lemma.
  ↓-cst×app-in : ∀ {i j k} {A : Type i}
    {B : Type j} {C : A → B → Type k}
    {a₁ a₂ : A} (p : a₁ == a₂)
    {b₁ b₂ : B} (q : b₁ == b₂)
    {c₁ : C a₁ b₁}{c₂ : C a₂ b₂}
    → c₁ == c₂ [ uncurry C ↓ pair×= p q ]
    → (b₁ , c₁) == (b₂ , c₂) [ (λ x → Σ B (C x)) ↓ p ]
  ↓-cst×app-in idp idp idp = idp

{- pair= and pair×= where one argument is reflexivity -}
pair=-idp-l : ∀ {i j} {A : Type i} {B : A → Type j} (a : A) {b₁ b₂ : B a}
  (q : b₁ == b₂) → pair= {B = B} idp q == ap (λ y → (a , y)) q
pair=-idp-l _ idp = idp

pair×=-idp-l : ∀ {i j} {A : Type i} {B : Type j} (a : A) {b₁ b₂ : B}
  (q : b₁ == b₂) → pair×= idp q == ap (λ y → (a , y)) q
pair×=-idp-l _ idp = idp

pair×=-idp-r : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A} (p : a₁ == a₂)
  (b : B) → pair×= p idp == ap (λ x → (x , b)) p
pair×=-idp-r idp _ = idp

pair×=-split-l : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A} (p : a₁ == a₂)
  {b₁ b₂ : B} (q : b₁ == b₂)
  → pair×= p q == ap (λ a → (a , b₁)) p ∙ ap (λ b → (a₂ , b)) q
pair×=-split-l idp idp = idp

pair×=-split-r : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A} (p : a₁ == a₂)
  {b₁ b₂ : B} (q : b₁ == b₂)
  → pair×= p q == ap (λ b → (a₁ , b)) q ∙ ap (λ a → (a , b₂)) p
pair×=-split-r idp idp = idp

-- Commutativity of products and derivatives.
module _ {i j} {A : Type i} {B : Type j} where
  ×-comm : Σ A (λ _ → B) ≃ Σ B (λ _ → A)
  ×-comm = equiv (λ {(a , b) → (b , a)}) (λ {(b , a) → (a , b)}) (λ _ → idp) (λ _ → idp)

module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} where
  Σ₂-×-comm : Σ (Σ A B) (λ ab → C (fst ab)) ≃ Σ (Σ A C) (λ ac → B (fst ac))
  Σ₂-×-comm = Σ-assoc ⁻¹ ∘e equiv-Σ-snd (λ a → ×-comm) ∘e Σ-assoc

module _ {i j k} {A : Type i} {B : Type j} {C : A → B → Type k} where
  Σ₁-×-comm : Σ A (λ a → Σ B (λ b → C a b)) ≃ Σ B (λ b → Σ A (λ a → C a b))
  Σ₁-×-comm = Σ-assoc ∘e equiv-Σ-fst _ (snd ×-comm) ∘e Σ-assoc ⁻¹

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


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

module 06-universes where

import 05-identity-types
open 05-identity-types public

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

-- Section 6.3 Observational equality on the natural numbers

-- Definition 6.3.1

Eq-ℕ : ℕ → ℕ → UU lzero
Eq-ℕ zero-ℕ zero-ℕ = 𝟙
Eq-ℕ zero-ℕ (succ-ℕ n) = 𝟘
Eq-ℕ (succ-ℕ m) zero-ℕ = 𝟘
Eq-ℕ (succ-ℕ m) (succ-ℕ n) = Eq-ℕ m n

-- Lemma 6.3.2

refl-Eq-ℕ : (n : ℕ) → Eq-ℕ n n
refl-Eq-ℕ zero-ℕ = star
refl-Eq-ℕ (succ-ℕ n) = refl-Eq-ℕ n

-- Proposition 6.3.3

Eq-ℕ-eq : {x y : ℕ} → Id x y → Eq-ℕ x y
Eq-ℕ-eq {x} {.x} refl = refl-Eq-ℕ x

eq-Eq-ℕ : (x y : ℕ) → Eq-ℕ x y → Id x y
eq-Eq-ℕ zero-ℕ zero-ℕ e = refl
eq-Eq-ℕ (succ-ℕ x) (succ-ℕ y) e = ap succ-ℕ (eq-Eq-ℕ x y e)

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

-- Section 6.4 Peano's seventh and eighth axioms

-- Theorem 6.4.1

is-injective-succ-ℕ : (x y : ℕ) → Id (succ-ℕ x) (succ-ℕ y) → Id x y
is-injective-succ-ℕ x y e = eq-Eq-ℕ x y (Eq-ℕ-eq e)

Peano-7 :
  (x y : ℕ) →
  ((Id x y) → (Id (succ-ℕ x) (succ-ℕ y))) ×
  ((Id (succ-ℕ x) (succ-ℕ y)) → (Id x y))
Peano-7 x y = pair (ap succ-ℕ) (is-injective-succ-ℕ x y)

-- Theorem 6.4.2

Peano-8 :
  (x : ℕ) → ¬ (Id zero-ℕ (succ-ℕ x))
Peano-8 x p = Eq-ℕ-eq p

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

-- Exercises

-- Exercise 6.1

-- Exercise 6.1 (a)

is-injective-add-ℕ :
  (k m n : ℕ) → Id (add-ℕ m k) (add-ℕ n k) → Id m n
is-injective-add-ℕ zero-ℕ m n = id
is-injective-add-ℕ (succ-ℕ k) m n p =
  is-injective-add-ℕ k m n (is-injective-succ-ℕ (add-ℕ m k) (add-ℕ n k) p)

-- Exercise 6.1 (b)

is-injective-mul-ℕ :
  (k m n : ℕ) → Id (mul-ℕ m (succ-ℕ k)) (mul-ℕ n (succ-ℕ k)) → Id m n
is-injective-mul-ℕ k zero-ℕ zero-ℕ p = refl
is-injective-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p =
  ap succ-ℕ
    ( is-injective-mul-ℕ k m n
      ( is-injective-add-ℕ
        ( succ-ℕ k)
        ( mul-ℕ m (succ-ℕ k))
        ( mul-ℕ n (succ-ℕ k))
        ( ( inv (left-successor-law-mul-ℕ m (succ-ℕ k))) ∙
          ( ( p) ∙
            ( left-successor-law-mul-ℕ n (succ-ℕ k))))))

-- Exercise 6.1 (c)

neq-add-ℕ :
  (m n : ℕ) → ¬ (Id m (add-ℕ m (succ-ℕ n)))
neq-add-ℕ (succ-ℕ m) n p =
  neq-add-ℕ m n
    ( ( is-injective-succ-ℕ m (add-ℕ (succ-ℕ m) n) p) ∙
      ( left-successor-law-add-ℕ m n))

-- Exercise 6.1 (d)

neq-mul-ℕ :
  (m n : ℕ) → ¬ (Id (succ-ℕ m) (mul-ℕ (succ-ℕ m) (succ-ℕ (succ-ℕ n))))
neq-mul-ℕ m n p =
  neq-add-ℕ
    ( succ-ℕ m)
    ( add-ℕ (mul-ℕ m (succ-ℕ n)) n)
    ( ( p) ∙
      ( ( right-successor-law-mul-ℕ (succ-ℕ m) (succ-ℕ n)) ∙
        ( ap (add-ℕ (succ-ℕ m)) (left-successor-law-mul-ℕ m (succ-ℕ n)))))

-- Exercise 6.2

-- Exercise 6.2 (a)

Eq-𝟚 : bool → bool → UU lzero
Eq-𝟚 true true = unit
Eq-𝟚 true false = empty
Eq-𝟚 false true = empty
Eq-𝟚 false false = unit

-- Exercise 6.2 (b)

reflexive-Eq-𝟚 : (x : bool) → Eq-𝟚 x x
reflexive-Eq-𝟚 true = star
reflexive-Eq-𝟚 false = star

Eq-eq-𝟚 :
  {x y : bool} → Id x y → Eq-𝟚 x y
Eq-eq-𝟚 {x = x} refl = reflexive-Eq-𝟚 x

eq-Eq-𝟚 :
  {x y : bool} → Eq-𝟚 x y → Id x y
eq-Eq-𝟚 {true} {true} star = refl
eq-Eq-𝟚 {false} {false} star = refl

-- Exercise 6.2 (c)

neq-neg-𝟚 : (b : bool) → ¬ (Id b (neg-𝟚 b))
neq-neg-𝟚 true = Eq-eq-𝟚
neq-neg-𝟚 false = Eq-eq-𝟚

neq-false-true-𝟚 :
  ¬ (Id false true)
neq-false-true-𝟚 = Eq-eq-𝟚

-- Exercise 6.3

-- Exercise 6.3 (a)

leq-ℕ : ℕ → ℕ → UU lzero
leq-ℕ zero-ℕ m = unit
leq-ℕ (succ-ℕ n) zero-ℕ = empty
leq-ℕ (succ-ℕ n) (succ-ℕ m) = leq-ℕ n m

_≤_ = leq-ℕ

-- Some trivialities that will be useful later

leq-zero-ℕ :
  (n : ℕ) → leq-ℕ zero-ℕ n
leq-zero-ℕ n = star

eq-leq-zero-ℕ :
  (x : ℕ) → leq-ℕ x zero-ℕ → Id zero-ℕ x
eq-leq-zero-ℕ zero-ℕ star = refl

succ-leq-ℕ : (n : ℕ) → leq-ℕ n (succ-ℕ n)
succ-leq-ℕ zero-ℕ = star
succ-leq-ℕ (succ-ℕ n) = succ-leq-ℕ n

concatenate-eq-leq-eq-ℕ :
  {x1 x2 x3 x4 : ℕ} → Id x1 x2 → leq-ℕ x2 x3 → Id x3 x4 → leq-ℕ x1 x4
concatenate-eq-leq-eq-ℕ refl H refl = H

concatenate-leq-eq-ℕ :
  (m : ℕ) {n n' : ℕ} → leq-ℕ m n → Id n n' → leq-ℕ m n'
concatenate-leq-eq-ℕ m H refl = H

concatenate-eq-leq-ℕ :
  {m m' : ℕ} (n : ℕ) → Id m' m → leq-ℕ m n → leq-ℕ m' n
concatenate-eq-leq-ℕ n refl H = H

-- Exercise 6.3 (b)

reflexive-leq-ℕ : (n : ℕ) → leq-ℕ n n
reflexive-leq-ℕ zero-ℕ = star
reflexive-leq-ℕ (succ-ℕ n) = reflexive-leq-ℕ n

leq-eq-ℕ : (m n : ℕ) → Id m n → leq-ℕ m n
leq-eq-ℕ m .m refl = reflexive-leq-ℕ m

transitive-leq-ℕ :
  (n m l : ℕ) → (n ≤ m) → (m ≤ l) → (n ≤ l)
transitive-leq-ℕ zero-ℕ m l p q = star
transitive-leq-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
  transitive-leq-ℕ n m l p q

preserves-leq-succ-ℕ :
  (m n : ℕ) → leq-ℕ m n → leq-ℕ m (succ-ℕ n)
preserves-leq-succ-ℕ m n p = transitive-leq-ℕ m n (succ-ℕ n) p (succ-leq-ℕ n)

anti-symmetric-leq-ℕ : (m n : ℕ) → leq-ℕ m n → leq-ℕ n m → Id m n
anti-symmetric-leq-ℕ zero-ℕ zero-ℕ p q = refl
anti-symmetric-leq-ℕ (succ-ℕ m) (succ-ℕ n) p q =
  ap succ-ℕ (anti-symmetric-leq-ℕ m n p q)

-- Exercise 6.3 (c)

decide-leq-ℕ :
  (m n : ℕ) → coprod (leq-ℕ m n) (leq-ℕ n m)
decide-leq-ℕ zero-ℕ zero-ℕ = inl star
decide-leq-ℕ zero-ℕ (succ-ℕ n) = inl star
decide-leq-ℕ (succ-ℕ m) zero-ℕ = inr star
decide-leq-ℕ (succ-ℕ m) (succ-ℕ n) = decide-leq-ℕ m n

-- Exercise 6.3 (d)

preserves-order-add-ℕ :
  (k m n : ℕ) → leq-ℕ m n → leq-ℕ (add-ℕ m k) (add-ℕ n k)
preserves-order-add-ℕ zero-ℕ m n = id
preserves-order-add-ℕ (succ-ℕ k) m n = preserves-order-add-ℕ k m n

reflects-order-add-ℕ :
  (k m n : ℕ) → leq-ℕ (add-ℕ m k) (add-ℕ n k) → leq-ℕ m n
reflects-order-add-ℕ zero-ℕ m n = id
reflects-order-add-ℕ (succ-ℕ k) m n = reflects-order-add-ℕ k m n

-- Exercise 6.3 (e)

preserves-order-mul-ℕ :
  (k m n : ℕ) → leq-ℕ m n → leq-ℕ (mul-ℕ m k) (mul-ℕ n k)
preserves-order-mul-ℕ k zero-ℕ n p = star
preserves-order-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p =
  preserves-order-add-ℕ k
    ( mul-ℕ m k)
    ( mul-ℕ n k)
    ( preserves-order-mul-ℕ k m n p)

reflects-order-mul-ℕ :
  (k m n : ℕ) → leq-ℕ (mul-ℕ m (succ-ℕ k)) (mul-ℕ n (succ-ℕ k)) → leq-ℕ m n
reflects-order-mul-ℕ k zero-ℕ n p = star
reflects-order-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p =
  reflects-order-mul-ℕ k m n
    ( reflects-order-add-ℕ
      ( succ-ℕ k)
      ( mul-ℕ m (succ-ℕ k))
      ( mul-ℕ n (succ-ℕ k))
      ( p))

-- Exercise 6.3 (f)

leq-min-ℕ :
  (k m n : ℕ) → leq-ℕ k m → leq-ℕ k n → leq-ℕ k (min-ℕ m n)
leq-min-ℕ zero-ℕ zero-ℕ zero-ℕ H K = star
leq-min-ℕ zero-ℕ zero-ℕ (succ-ℕ n) H K = star
leq-min-ℕ zero-ℕ (succ-ℕ m) zero-ℕ H K = star
leq-min-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ n) H K = star
leq-min-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H K = leq-min-ℕ k m n H K

leq-left-leq-min-ℕ :
  (k m n : ℕ) → leq-ℕ k (min-ℕ m n) → leq-ℕ k m
leq-left-leq-min-ℕ zero-ℕ zero-ℕ zero-ℕ H = star
leq-left-leq-min-ℕ zero-ℕ zero-ℕ (succ-ℕ n) H = star
leq-left-leq-min-ℕ zero-ℕ (succ-ℕ m) zero-ℕ H = star
leq-left-leq-min-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ n) H = star
leq-left-leq-min-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
  leq-left-leq-min-ℕ k m n H

leq-right-leq-min-ℕ :
  (k m n : ℕ) → leq-ℕ k (min-ℕ m n) → leq-ℕ k n
leq-right-leq-min-ℕ zero-ℕ zero-ℕ zero-ℕ H = star
leq-right-leq-min-ℕ zero-ℕ zero-ℕ (succ-ℕ n) H = star
leq-right-leq-min-ℕ zero-ℕ (succ-ℕ m) zero-ℕ H = star
leq-right-leq-min-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ n) H = star
leq-right-leq-min-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
  leq-right-leq-min-ℕ k m n H

leq-max-ℕ :
  (k m n : ℕ) → leq-ℕ m k → leq-ℕ n k → leq-ℕ (max-ℕ m n) k
leq-max-ℕ zero-ℕ zero-ℕ zero-ℕ H K = star
leq-max-ℕ (succ-ℕ k) zero-ℕ zero-ℕ H K = star
leq-max-ℕ (succ-ℕ k) zero-ℕ (succ-ℕ n) H K = K
leq-max-ℕ (succ-ℕ k) (succ-ℕ m) zero-ℕ H K = H
leq-max-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H K = leq-max-ℕ k m n H K

leq-left-leq-max-ℕ :
  (k m n : ℕ) → leq-ℕ (max-ℕ m n) k → leq-ℕ m k
leq-left-leq-max-ℕ k zero-ℕ zero-ℕ H = star
leq-left-leq-max-ℕ k zero-ℕ (succ-ℕ n) H = star
leq-left-leq-max-ℕ k (succ-ℕ m) zero-ℕ H = H
leq-left-leq-max-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
  leq-left-leq-max-ℕ k m n H

leq-right-leq-max-ℕ :
  (k m n : ℕ) → leq-ℕ (max-ℕ m n) k → leq-ℕ n k
leq-right-leq-max-ℕ k zero-ℕ zero-ℕ H = star
leq-right-leq-max-ℕ k zero-ℕ (succ-ℕ n) H = H
leq-right-leq-max-ℕ k (succ-ℕ m) zero-ℕ H = star
leq-right-leq-max-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
  leq-right-leq-max-ℕ k m n H

-- Exercise 6.4

-- Exercise 6.4 (a)

-- We define a distance function on ℕ --

dist-ℕ : ℕ → ℕ → ℕ
dist-ℕ zero-ℕ n = n
dist-ℕ (succ-ℕ m) zero-ℕ = succ-ℕ m
dist-ℕ (succ-ℕ m) (succ-ℕ n) = dist-ℕ m n

dist-ℕ' : ℕ → ℕ → ℕ
dist-ℕ' m n = dist-ℕ n m

ap-dist-ℕ :
  {m n m' n' : ℕ} → Id m m' → Id n n' → Id (dist-ℕ m n) (dist-ℕ m' n')
ap-dist-ℕ refl refl = refl

{- We show that two natural numbers are equal if and only if their distance is
   zero. -}

eq-dist-ℕ :
  (m n : ℕ) → Id zero-ℕ (dist-ℕ m n) → Id m n
eq-dist-ℕ zero-ℕ zero-ℕ p = refl
eq-dist-ℕ (succ-ℕ m) (succ-ℕ n) p = ap succ-ℕ (eq-dist-ℕ m n p)

dist-eq-ℕ' :
  (n : ℕ) → Id zero-ℕ (dist-ℕ n n)
dist-eq-ℕ' zero-ℕ = refl
dist-eq-ℕ' (succ-ℕ n) = dist-eq-ℕ' n

dist-eq-ℕ :
  (m n : ℕ) → Id m n → Id zero-ℕ (dist-ℕ m n)
dist-eq-ℕ m .m refl = dist-eq-ℕ' m

-- The distance function is symmetric --

symmetric-dist-ℕ :
  (m n : ℕ) → Id (dist-ℕ m n) (dist-ℕ n m)
symmetric-dist-ℕ zero-ℕ zero-ℕ = refl
symmetric-dist-ℕ zero-ℕ (succ-ℕ n) = refl
symmetric-dist-ℕ (succ-ℕ m) zero-ℕ = refl
symmetric-dist-ℕ (succ-ℕ m) (succ-ℕ n) = symmetric-dist-ℕ m n

-- We compute the distance from zero --

left-zero-law-dist-ℕ :
  (n : ℕ) → Id (dist-ℕ zero-ℕ n) n
left-zero-law-dist-ℕ zero-ℕ = refl
left-zero-law-dist-ℕ (succ-ℕ n) = refl

right-zero-law-dist-ℕ :
  (n : ℕ) → Id (dist-ℕ n zero-ℕ) n
right-zero-law-dist-ℕ zero-ℕ = refl
right-zero-law-dist-ℕ (succ-ℕ n) = refl

-- We prove the triangle inequality --

ap-add-ℕ :
  {m n m' n' : ℕ} → Id m m' → Id n n' → Id (add-ℕ m n) (add-ℕ m' n')
ap-add-ℕ refl refl = refl

triangle-inequality-dist-ℕ :
  (m n k : ℕ) → leq-ℕ (dist-ℕ m n) (add-ℕ (dist-ℕ m k) (dist-ℕ k n))
triangle-inequality-dist-ℕ zero-ℕ zero-ℕ zero-ℕ = star
triangle-inequality-dist-ℕ zero-ℕ zero-ℕ (succ-ℕ k) = star
triangle-inequality-dist-ℕ zero-ℕ (succ-ℕ n) zero-ℕ =
  tr ( leq-ℕ (succ-ℕ n))
     ( inv (left-unit-law-add-ℕ (succ-ℕ n)))
     ( reflexive-leq-ℕ (succ-ℕ n))
triangle-inequality-dist-ℕ zero-ℕ (succ-ℕ n) (succ-ℕ k) =
  concatenate-eq-leq-eq-ℕ
    ( inv (ap succ-ℕ (left-zero-law-dist-ℕ n)))
    ( triangle-inequality-dist-ℕ zero-ℕ n k)
    ( ( ap (succ-ℕ ∘ (add-ℕ' (dist-ℕ k n))) (left-zero-law-dist-ℕ k)) ∙
      ( inv (left-successor-law-add-ℕ k (dist-ℕ k n))))
triangle-inequality-dist-ℕ (succ-ℕ m) zero-ℕ zero-ℕ = reflexive-leq-ℕ (succ-ℕ m)
triangle-inequality-dist-ℕ (succ-ℕ m) zero-ℕ (succ-ℕ k) =
  concatenate-eq-leq-eq-ℕ
    ( inv (ap succ-ℕ (right-zero-law-dist-ℕ m)))
    ( triangle-inequality-dist-ℕ m zero-ℕ k)
    ( ap (succ-ℕ ∘ (add-ℕ (dist-ℕ m k))) (right-zero-law-dist-ℕ k))
triangle-inequality-dist-ℕ (succ-ℕ m) (succ-ℕ n) zero-ℕ =
  concatenate-leq-eq-ℕ
    ( dist-ℕ m n)
    ( transitive-leq-ℕ
      ( dist-ℕ m n)
      ( succ-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n)))
      ( succ-ℕ (succ-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n))))
      ( transitive-leq-ℕ
        ( dist-ℕ m n)
        ( add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n))
        ( succ-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n)))
        ( triangle-inequality-dist-ℕ m n zero-ℕ)
        ( succ-leq-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n))))
      ( succ-leq-ℕ (succ-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n)))))
    ( ( ap (succ-ℕ ∘ succ-ℕ)
           ( ap-add-ℕ (right-zero-law-dist-ℕ m) (left-zero-law-dist-ℕ n))) ∙
      ( inv (left-successor-law-add-ℕ m (succ-ℕ n))))
triangle-inequality-dist-ℕ (succ-ℕ m) (succ-ℕ n) (succ-ℕ k) =
  triangle-inequality-dist-ℕ m n k

-- We show that dist-ℕ x y is a solution to a simple equation.

leq-dist-ℕ :
  (x y : ℕ) → leq-ℕ x y → Id (add-ℕ x (dist-ℕ x y)) y
leq-dist-ℕ zero-ℕ zero-ℕ H = refl
leq-dist-ℕ zero-ℕ (succ-ℕ y) star = left-unit-law-add-ℕ (succ-ℕ y)
leq-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
  ( left-successor-law-add-ℕ x (dist-ℕ x y)) ∙
  ( ap succ-ℕ (leq-dist-ℕ x y H))

rewrite-left-add-dist-ℕ :
  (x y z : ℕ) → Id (add-ℕ x y) z → Id x (dist-ℕ y z)
rewrite-left-add-dist-ℕ zero-ℕ zero-ℕ .zero-ℕ refl = refl
rewrite-left-add-dist-ℕ zero-ℕ (succ-ℕ y) .(succ-ℕ (add-ℕ zero-ℕ y)) refl =
  ( dist-eq-ℕ' y) ∙
  ( inv (ap (dist-ℕ (succ-ℕ y)) (left-unit-law-add-ℕ (succ-ℕ y))))
rewrite-left-add-dist-ℕ (succ-ℕ x) zero-ℕ .(succ-ℕ x) refl = refl
rewrite-left-add-dist-ℕ
  (succ-ℕ x) (succ-ℕ y) .(succ-ℕ (add-ℕ (succ-ℕ x) y)) refl =
  rewrite-left-add-dist-ℕ (succ-ℕ x) y (add-ℕ (succ-ℕ x) y) refl

rewrite-left-dist-add-ℕ :
  (x y z : ℕ) → leq-ℕ y z → Id x (dist-ℕ y z) → Id (add-ℕ x y) z
rewrite-left-dist-add-ℕ .(dist-ℕ y z) y z H refl =
  ( commutative-add-ℕ (dist-ℕ y z) y) ∙
  ( leq-dist-ℕ y z H)

rewrite-right-add-dist-ℕ :
  (x y z : ℕ) → Id (add-ℕ x y) z → Id y (dist-ℕ x z)
rewrite-right-add-dist-ℕ x y z p =
  rewrite-left-add-dist-ℕ y x z (commutative-add-ℕ y x ∙ p)

rewrite-right-dist-add-ℕ :
  (x y z : ℕ) → leq-ℕ x z → Id y (dist-ℕ x z) → Id (add-ℕ x y) z
rewrite-right-dist-add-ℕ x .(dist-ℕ x z) z H refl =
  leq-dist-ℕ x z H

-- We show that dist-ℕ is translation invariant

translation-invariant-dist-ℕ :
  (k m n : ℕ) → Id (dist-ℕ (add-ℕ k m) (add-ℕ k n)) (dist-ℕ m n)
translation-invariant-dist-ℕ zero-ℕ m n =
  ap-dist-ℕ (left-unit-law-add-ℕ m) (left-unit-law-add-ℕ n)
translation-invariant-dist-ℕ (succ-ℕ k)  m n =
  ( ap-dist-ℕ (left-successor-law-add-ℕ k m) (left-successor-law-add-ℕ k n)) ∙
  ( translation-invariant-dist-ℕ k m n)

-- We show that dist-ℕ is linear with respect to scalar multiplication

linear-dist-ℕ :
  (m n k : ℕ) → Id (dist-ℕ (mul-ℕ k m) (mul-ℕ k n)) (mul-ℕ k (dist-ℕ m n))
linear-dist-ℕ zero-ℕ zero-ℕ zero-ℕ = refl
linear-dist-ℕ zero-ℕ zero-ℕ (succ-ℕ k) = linear-dist-ℕ zero-ℕ zero-ℕ k
linear-dist-ℕ zero-ℕ (succ-ℕ n) zero-ℕ = refl
linear-dist-ℕ zero-ℕ (succ-ℕ n) (succ-ℕ k) =
  ap (dist-ℕ' (mul-ℕ (succ-ℕ k) (succ-ℕ n))) (right-zero-law-mul-ℕ (succ-ℕ k))
linear-dist-ℕ (succ-ℕ m) zero-ℕ zero-ℕ = refl
linear-dist-ℕ (succ-ℕ m) zero-ℕ (succ-ℕ k) =
  ap (dist-ℕ (mul-ℕ (succ-ℕ k) (succ-ℕ m))) (right-zero-law-mul-ℕ (succ-ℕ k))
linear-dist-ℕ (succ-ℕ m) (succ-ℕ n) zero-ℕ = refl
linear-dist-ℕ (succ-ℕ m) (succ-ℕ n) (succ-ℕ k) =
  ( ap-dist-ℕ
    ( right-successor-law-mul-ℕ (succ-ℕ k) m)
    ( right-successor-law-mul-ℕ (succ-ℕ k) n)) ∙
  ( ( translation-invariant-dist-ℕ
      ( succ-ℕ k)
      ( mul-ℕ (succ-ℕ k) m)
      ( mul-ℕ (succ-ℕ k) n)) ∙
    ( linear-dist-ℕ m n (succ-ℕ k)))

-- Exercise 6.6

{- In this exercise we were asked to define the relations ≤ and < on the
   integers. As a criterion of correctness, we were then also asked to show
   that the type of all integers l satisfying k ≤ l satisfy the induction
   principle of the natural numbers. -}

diff-ℤ : ℤ → ℤ → ℤ
diff-ℤ k l = add-ℤ (neg-ℤ k) l

is-non-negative-ℤ : ℤ → UU lzero
is-non-negative-ℤ (inl x) = empty
is-non-negative-ℤ (inr k) = unit

leq-ℤ : ℤ → ℤ → UU lzero
leq-ℤ k l = is-non-negative-ℤ (diff-ℤ k l)

reflexive-leq-ℤ : (k : ℤ) → leq-ℤ k k
reflexive-leq-ℤ k =
  tr is-non-negative-ℤ (inv (left-inverse-law-add-ℤ k)) star

is-non-negative-succ-ℤ :
  (k : ℤ) → is-non-negative-ℤ k → is-non-negative-ℤ (succ-ℤ k)
is-non-negative-succ-ℤ (inr (inl star)) p = star
is-non-negative-succ-ℤ (inr (inr x)) p = star

is-non-negative-add-ℤ :
  (k l : ℤ) →
  is-non-negative-ℤ k → is-non-negative-ℤ l → is-non-negative-ℤ (add-ℤ k l)
is-non-negative-add-ℤ (inr (inl star)) (inr (inl star)) p q = star
is-non-negative-add-ℤ (inr (inl star)) (inr (inr n)) p q = star
is-non-negative-add-ℤ (inr (inr zero-ℕ)) (inr (inl star)) p q = star
is-non-negative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inl star)) star star =
  is-non-negative-succ-ℤ
    ( add-ℤ (inr (inr n)) (inr (inl star)))
    ( is-non-negative-add-ℤ (inr (inr n)) (inr (inl star)) star star)
is-non-negative-add-ℤ (inr (inr zero-ℕ)) (inr (inr m)) star star = star
is-non-negative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inr m)) star star =
  is-non-negative-succ-ℤ
    ( add-ℤ (inr (inr n)) (inr (inr m)))
    ( is-non-negative-add-ℤ (inr (inr n)) (inr (inr m)) star star)

triangle-diff-ℤ :
  (k l m : ℤ) → Id (add-ℤ (diff-ℤ k l) (diff-ℤ l m)) (diff-ℤ k m)
triangle-diff-ℤ k l m =
  ( associative-add-ℤ (neg-ℤ k) l (diff-ℤ l m)) ∙
  ( ap
    ( add-ℤ (neg-ℤ k))
    ( ( inv (associative-add-ℤ l (neg-ℤ l) m)) ∙
      ( ( ap (λ x → add-ℤ x m) (right-inverse-law-add-ℤ l)) ∙
        ( left-unit-law-add-ℤ m))))

transitive-leq-ℤ : (k l m : ℤ) → leq-ℤ k l → leq-ℤ l m → leq-ℤ k m
transitive-leq-ℤ k l m p q =
  tr is-non-negative-ℤ
    ( triangle-diff-ℤ k l m)
    ( is-non-negative-add-ℤ
      ( add-ℤ (neg-ℤ k) l)
      ( add-ℤ (neg-ℤ l) m)
      ( p)
      ( q))

succ-leq-ℤ : (k : ℤ) → leq-ℤ k (succ-ℤ k)
succ-leq-ℤ k =
  tr is-non-negative-ℤ
    ( inv
      ( ( right-successor-law-add-ℤ (neg-ℤ k) k) ∙
        ( ap succ-ℤ (left-inverse-law-add-ℤ k))))
    ( star)

leq-ℤ-succ-leq-ℤ : (k l : ℤ) → leq-ℤ k l → leq-ℤ k (succ-ℤ l)
leq-ℤ-succ-leq-ℤ k l p = transitive-leq-ℤ k l (succ-ℤ l) p (succ-leq-ℤ l)

is-positive-ℤ : ℤ → UU lzero
is-positive-ℤ k = is-non-negative-ℤ (pred-ℤ k)

le-ℤ : ℤ → ℤ → UU lzero
le-ℤ (inl zero-ℕ) (inl x) = empty
le-ℤ (inl zero-ℕ) (inr y) = unit
le-ℤ (inl (succ-ℕ x)) (inl zero-ℕ) = unit
le-ℤ (inl (succ-ℕ x)) (inl (succ-ℕ y)) = le-ℤ (inl x) (inl y)
le-ℤ (inl (succ-ℕ x)) (inr y) = unit
le-ℤ (inr x) (inl y) = empty
le-ℤ (inr (inl star)) (inr (inl star)) = empty
le-ℤ (inr (inl star)) (inr (inr x)) = unit
le-ℤ (inr (inr x)) (inr (inl star)) = empty
le-ℤ (inr (inr zero-ℕ)) (inr (inr zero-ℕ)) = empty
le-ℤ (inr (inr zero-ℕ)) (inr (inr (succ-ℕ y))) = unit
le-ℤ (inr (inr (succ-ℕ x))) (inr (inr zero-ℕ)) = empty
le-ℤ (inr (inr (succ-ℕ x))) (inr (inr (succ-ℕ y))) =
  le-ℤ (inr (inr x)) (inr (inr y))

-- Extra material

-- We show that ℕ is an ordered semi-ring

left-law-leq-add-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (add-ℕ m k) (add-ℕ n k)
left-law-leq-add-ℕ zero-ℕ m n = id
left-law-leq-add-ℕ (succ-ℕ k) m n H = left-law-leq-add-ℕ k m n H

right-law-leq-add-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (add-ℕ k m) (add-ℕ k n)
right-law-leq-add-ℕ k m n H =
  concatenate-eq-leq-eq-ℕ
    ( commutative-add-ℕ k m)
    ( left-law-leq-add-ℕ k m n H)
    ( commutative-add-ℕ n k)

preserves-leq-add-ℕ :
  {m m' n n' : ℕ} → leq-ℕ m m' → leq-ℕ n n' → leq-ℕ (add-ℕ m n) (add-ℕ m' n')
preserves-leq-add-ℕ {m} {m'} {n} {n'} H K =
  transitive-leq-ℕ
    ( add-ℕ m n)
    ( add-ℕ m' n)
    ( add-ℕ m' n')
    ( left-law-leq-add-ℕ n m m' H)
    ( right-law-leq-add-ℕ m' n n' K)

{-
right-law-leq-mul-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (mul-ℕ k m) (mul-ℕ k n)
right-law-leq-mul-ℕ zero-ℕ m n H = star
right-law-leq-mul-ℕ (succ-ℕ k) m n H = {!!}
-}

{-
  preserves-leq-add-ℕ
    { m = mul-ℕ k m}
    { m' = mul-ℕ k n}
    ( right-law-leq-mul-ℕ k m n H) H

left-law-leq-mul-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (mul-ℕ m k) (mul-ℕ n k)
left-law-leq-mul-ℕ k m n H =
  concatenate-eq-leq-eq-ℕ
    ( commutative-mul-ℕ k m)
    ( commutative-mul-ℕ k n)
    ( right-law-leq-mul-ℕ k m n H)
-}

-- We show that ℤ is an ordered ring

{-
leq-add-ℤ : (m k l : ℤ) → leq-ℤ k l → leq-ℤ (add-ℤ m k) (add-ℤ m l)
leq-add-ℤ (inl zero-ℕ) k l H = {!!}
leq-add-ℤ (inl (succ-ℕ x)) k l H = {!!}
leq-add-ℤ (inr m) k l H = {!!}
-}

-- Section 5.5 Identity systems

succ-fam-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i) →
  (m n : ℕ) → Eq-ℕ m n → UU i
succ-fam-Eq-ℕ R m n e = R (succ-ℕ m) (succ-ℕ n) e

succ-refl-fam-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  (ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  (n : ℕ) → (succ-fam-Eq-ℕ R n n (refl-Eq-ℕ n))
succ-refl-fam-Eq-ℕ R ρ n = ρ (succ-ℕ n)

path-ind-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  ( ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  ( m n : ℕ) (e : Eq-ℕ m n) → R m n e
path-ind-Eq-ℕ R ρ zero-ℕ zero-ℕ star = ρ zero-ℕ
path-ind-Eq-ℕ R ρ zero-ℕ (succ-ℕ n) ()
path-ind-Eq-ℕ R ρ (succ-ℕ m) zero-ℕ ()
path-ind-Eq-ℕ R ρ (succ-ℕ m) (succ-ℕ n) e =
  path-ind-Eq-ℕ
    ( λ m n e → R (succ-ℕ m) (succ-ℕ n) e)
    ( λ n → ρ (succ-ℕ n)) m n e

comp-path-ind-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  ( ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  ( n : ℕ) → Id (path-ind-Eq-ℕ R ρ n n (refl-Eq-ℕ n)) (ρ n)
comp-path-ind-Eq-ℕ R ρ zero-ℕ = refl
comp-path-ind-Eq-ℕ R ρ (succ-ℕ n) =
  comp-path-ind-Eq-ℕ
    ( λ m n e → R (succ-ℕ m) (succ-ℕ n) e)
    ( λ n → ρ (succ-ℕ n)) n

{-
-- Graphs
Gph : (i : Level) → UU (lsuc i)
Gph i = Σ (UU i) (λ X → (X → X → (UU i)))

-- Reflexive graphs
rGph : (i : Level) →  UU (lsuc i)
rGph i = Σ (UU i) (λ X → Σ (X → X → (UU i)) (λ R → (x : X) → R x x))
-}

-- Exercise 3.7

{- With the construction of the divisibility relation we open the door to basic
   number theory. -}

divides : (d n : ℕ) → UU lzero
divides d n = Σ ℕ (λ m → Eq-ℕ (mul-ℕ d m) n)

-- We prove some lemmas about inequalities --

leq-add-ℕ :
  (m n : ℕ) → leq-ℕ m (add-ℕ m n)
leq-add-ℕ m zero-ℕ = reflexive-leq-ℕ m
leq-add-ℕ m (succ-ℕ n) =
  transitive-leq-ℕ m (add-ℕ m n) (succ-ℕ (add-ℕ m n))
    ( leq-add-ℕ m n)
    ( succ-leq-ℕ (add-ℕ m n))

leq-add-ℕ' :
  (m n : ℕ) → leq-ℕ m (add-ℕ n m)
leq-add-ℕ' m n =
  concatenate-leq-eq-ℕ m (leq-add-ℕ m n) (commutative-add-ℕ m n)

leq-leq-add-ℕ :
  (m n x : ℕ) → leq-ℕ (add-ℕ m x) (add-ℕ n x) → leq-ℕ m n
leq-leq-add-ℕ m n zero-ℕ H = H
leq-leq-add-ℕ m n (succ-ℕ x) H = leq-leq-add-ℕ m n x H

leq-leq-add-ℕ' :
  (m n x : ℕ) → leq-ℕ (add-ℕ x m) (add-ℕ x n) → leq-ℕ m n
leq-leq-add-ℕ' m n x H =
  leq-leq-add-ℕ m n x
    ( concatenate-eq-leq-eq-ℕ
      ( commutative-add-ℕ m x)
      ( H)
      ( commutative-add-ℕ x n))

leq-leq-mul-ℕ :
  (m n x : ℕ) → leq-ℕ (mul-ℕ (succ-ℕ x) m) (mul-ℕ (succ-ℕ x) n) → leq-ℕ m n
leq-leq-mul-ℕ zero-ℕ zero-ℕ x H = star
leq-leq-mul-ℕ zero-ℕ (succ-ℕ n) x H = star
leq-leq-mul-ℕ (succ-ℕ m) zero-ℕ x H =
  ex-falso
    ( concatenate-leq-eq-ℕ
      ( mul-ℕ (succ-ℕ x) (succ-ℕ m))
      ( H)
      ( right-zero-law-mul-ℕ (succ-ℕ x)))
leq-leq-mul-ℕ (succ-ℕ m) (succ-ℕ n) x H =
  leq-leq-mul-ℕ m n x
    ( leq-leq-add-ℕ' (mul-ℕ (succ-ℕ x) m) (mul-ℕ (succ-ℕ x) n) (succ-ℕ x)
      ( concatenate-eq-leq-eq-ℕ
        ( inv (right-successor-law-mul-ℕ (succ-ℕ x) m))
        ( H)
        ( right-successor-law-mul-ℕ (succ-ℕ x) n)))

leq-leq-mul-ℕ' :
  (m n x : ℕ) → leq-ℕ (mul-ℕ m (succ-ℕ x)) (mul-ℕ n (succ-ℕ x)) → leq-ℕ m n
leq-leq-mul-ℕ' m n x H =
  leq-leq-mul-ℕ m n x
    ( concatenate-eq-leq-eq-ℕ
      ( commutative-mul-ℕ (succ-ℕ x) m)
      ( H)
      ( commutative-mul-ℕ n (succ-ℕ x)))

{-
succ-relation-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) → ℕ → ℕ → UU i
succ-relation-ℕ R m n = R (succ-ℕ m) (succ-ℕ n)

succ-reflexivity-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) (ρ : (n : ℕ) → R n n) →
  (n : ℕ) → succ-relation-ℕ R n n
succ-reflexivity-ℕ R ρ n = ρ (succ-ℕ n)

{- In the book we suggest that first the order of the variables should be
   swapped, in order to make the inductive hypothesis stronger. Agda's pattern
   matching mechanism allows us to bypass this step and give a more direct
   construction. -}

least-reflexive-Eq-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) (ρ : (n : ℕ) → R n n) →
  (m n : ℕ) → Eq-ℕ m n → R m n
least-reflexive-Eq-ℕ R ρ zero-ℕ zero-ℕ star = ρ zero-ℕ
least-reflexive-Eq-ℕ R ρ zero-ℕ (succ-ℕ n) ()
least-reflexive-Eq-ℕ R ρ (succ-ℕ m) zero-ℕ ()
least-reflexive-Eq-ℕ R ρ (succ-ℕ m) (succ-ℕ n) e =
  least-reflexive-Eq-ℕ (succ-relation-ℕ R) (succ-reflexivity-ℕ R ρ) m n e
-}

-- The definition of <

le-ℕ : ℕ → ℕ → UU lzero
le-ℕ m zero-ℕ = empty
le-ℕ zero-ℕ (succ-ℕ m) = unit
le-ℕ (succ-ℕ n) (succ-ℕ m) = le-ℕ n m

_<_ = le-ℕ

anti-reflexive-le-ℕ : (n : ℕ) → ¬ (n < n)
anti-reflexive-le-ℕ zero-ℕ = ind-empty
anti-reflexive-le-ℕ (succ-ℕ n) = anti-reflexive-le-ℕ n

transitive-le-ℕ : (n m l : ℕ) → (le-ℕ n m) → (le-ℕ m l) → (le-ℕ n l)
transitive-le-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ l) p q = star
transitive-le-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
  transitive-le-ℕ n m l p q

succ-le-ℕ : (n : ℕ) → le-ℕ n (succ-ℕ n)
succ-le-ℕ zero-ℕ = star
succ-le-ℕ (succ-ℕ n) = succ-le-ℕ n

anti-symmetric-le-ℕ : (m n : ℕ) → le-ℕ m n → le-ℕ n m → Id m n
anti-symmetric-le-ℕ (succ-ℕ m) (succ-ℕ n) p q =
  ap succ-ℕ (anti-symmetric-le-ℕ m n p q)

{-
--------------------------------------------------------------------------------

data Fin-Tree : UU lzero where
  constr : (n : ℕ) → (Fin n → Fin-Tree) → Fin-Tree

root-Fin-Tree : Fin-Tree
root-Fin-Tree = constr zero-ℕ ex-falso

succ-Fin-Tree : Fin-Tree → Fin-Tree
succ-Fin-Tree t = constr one-ℕ (λ i → t)

map-assoc-coprod :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} →
  coprod (coprod A B) C → coprod A (coprod B C)
map-assoc-coprod (inl (inl x)) = inl x
map-assoc-coprod (inl (inr x)) = inr (inl x)
map-assoc-coprod (inr x) = inr (inr x)

map-coprod-Fin :
  (m n : ℕ) → Fin (add-ℕ m n) → coprod (Fin m) (Fin n)
map-coprod-Fin m zero-ℕ = inl
map-coprod-Fin m (succ-ℕ n) =
  map-assoc-coprod ∘ (functor-coprod (map-coprod-Fin m n) (id {A = unit}))

add-Fin-Tree : Fin-Tree → Fin-Tree → Fin-Tree
add-Fin-Tree (constr n x) (constr m y) =
  constr (add-ℕ n m) ((ind-coprod (λ i → Fin-Tree) x y) ∘ (map-coprod-Fin n m))

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

data labeled-Bin-Tree {l1 : Level} (A : UU l1) : UU l1 where
  leaf : A → labeled-Bin-Tree A
  constr : (bool → labeled-Bin-Tree A) → labeled-Bin-Tree A

mul-leaves-labeled-Bin-Tree :
  {l1 : Level} {A : UU l1} (μ : A → (A → A)) →
  labeled-Bin-Tree A → A
mul-leaves-labeled-Bin-Tree μ (leaf x) = x
mul-leaves-labeled-Bin-Tree μ (constr f) =
  μ ( mul-leaves-labeled-Bin-Tree μ (f false))
    ( mul-leaves-labeled-Bin-Tree μ (f true))

pick-list : {l1 : Level} {A : UU l1} → ℕ → list A → coprod A unit
pick-list zero-ℕ nil = inr star
pick-list zero-ℕ (cons a x) = inl a
pick-list (succ-ℕ n) nil = inr star
pick-list (succ-ℕ n) (cons a x) = pick-list n x
-}

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

module Number.Instances.QuoQ.Definitions where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)

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.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool as Bool using (Bool; not; true; false)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
open import Function.Base using (it; _∋_; _$_)
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.PropositionalTruncation --.Properties

open import Utils using (!_; !!_)
open import MoreLogic.Reasoning
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Structures
open import MorePropAlgebra.Bundles
open import MorePropAlgebra.Consequences
open import Number.Structures2
open import Number.Bundles2

open import Cubical.Data.NatPlusOne using (HasFromNat; 1+_; ℕ₊₁; ℕ₊₁→ℕ)
open import Cubical.HITs.SetQuotients as SetQuotient using () renaming (_/_ to _//_)

open import Cubical.Data.Nat.Literals
open import Cubical.Data.Bool
open import Number.Prelude.Nat
open import Number.Prelude.QuoInt
open import Cubical.HITs.Ints.QuoInt using (HasFromNat)
open import Cubical.HITs.Rationals.QuoQ using
  ( ℚ
  ; onCommonDenom
  ; onCommonDenomSym
  ; eq/
  ; _//_
  ; _∼_
  )
  renaming
  ( [_] to [_]ᶠ
  ; ℕ₊₁→ℤ to [1+_ⁿ]ᶻ
  )

abstract
  private
    lemma1 : ∀ a b₁ b₂ c → (a ·ᶻ b₁) ·ᶻ (b₂ ·ᶻ c) ≡ (a ·ᶻ c) ·ᶻ (b₂ ·ᶻ b₁)
    lemma1 a b₁ b₂ c =
      (a ·ᶻ b₁) ·ᶻ (b₂ ·ᶻ c) ≡⟨ sym $ ·ᶻ-assoc a b₁ (b₂ ·ᶻ c) ⟩
      a ·ᶻ (b₁ ·ᶻ (b₂ ·ᶻ c)) ≡⟨ (λ i → a ·ᶻ ·ᶻ-assoc b₁ b₂ c i) ⟩
      a ·ᶻ ((b₁ ·ᶻ b₂) ·ᶻ c) ≡⟨ (λ i → a ·ᶻ ·ᶻ-comm (b₁ ·ᶻ b₂) c i) ⟩
      a ·ᶻ (c ·ᶻ (b₁ ·ᶻ b₂)) ≡⟨ ·ᶻ-assoc a c (b₁ ·ᶻ b₂) ⟩
      (a ·ᶻ c) ·ᶻ (b₁ ·ᶻ b₂) ≡⟨ (λ i → (a ·ᶻ c) ·ᶻ ·ᶻ-comm b₁ b₂ i) ⟩
      (a ·ᶻ c) ·ᶻ (b₂ ·ᶻ b₁) ∎

    ·ᶻ-commʳ : ∀ a b c → (a ·ᶻ b) ·ᶻ c ≡ (a ·ᶻ c) ·ᶻ b
    ·ᶻ-commʳ a b c = (a ·ᶻ  b) ·ᶻ c  ≡⟨ sym $ ·ᶻ-assoc a b c ⟩
                      a ·ᶻ (b  ·ᶻ c) ≡⟨ (λ i → a ·ᶻ ·ᶻ-comm b c i) ⟩
                      a ·ᶻ (c  ·ᶻ b) ≡⟨ ·ᶻ-assoc a c b ⟩
                     (a ·ᶻ  c) ·ᶻ b  ∎

∼-preserves-<ᶻ : ∀ aᶻ aⁿ bᶻ bⁿ → (aᶻ , aⁿ) ∼ (bᶻ , bⁿ) → [ ((aᶻ <ᶻ 0) ⇒ (bᶻ <ᶻ 0)) ⊓ ((0 <ᶻ aᶻ) ⇒ (0 <ᶻ bᶻ)) ]
∼-preserves-<ᶻ aᶻ aⁿ bᶻ bⁿ r = γ where
  aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
  bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
  0<aⁿᶻ : [ 0 <ᶻ aⁿᶻ ]
  0<aⁿᶻ = ℕ₊₁.n aⁿ , +ⁿ-comm (ℕ₊₁.n aⁿ) 1
  0<bⁿᶻ : [ 0 <ᶻ bⁿᶻ ]
  0<bⁿᶻ = ℕ₊₁.n bⁿ , +ⁿ-comm (ℕ₊₁.n bⁿ) 1
  γ : [ ((aᶻ <ᶻ 0) ⇒ (bᶻ <ᶻ 0)) ⊓ ((0 <ᶻ aᶻ) ⇒ (0 <ᶻ bᶻ)) ]
  γ .fst aᶻ<0 = (
    aᶻ <ᶻ 0               ⇒ᵖ⟨ ·ᶻ-preserves-<ᶻ aᶻ 0 bⁿᶻ 0<bⁿᶻ ⟩
    aᶻ ·ᶻ bⁿᶻ <ᶻ 0 ·ᶻ bⁿᶻ ⇒ᵖ⟨ (subst (λ p → [ aᶻ ·ᶻ bⁿᶻ <ᶻ p ]) $ ·ᶻ-nullifiesˡ bⁿᶻ) ⟩
    aᶻ ·ᶻ bⁿᶻ <ᶻ 0        ⇒ᵖ⟨ subst (λ p → [ p <ᶻ 0 ]) r ⟩
    bᶻ ·ᶻ aⁿᶻ <ᶻ 0        ⇒ᵖ⟨ subst (λ p → [ bᶻ ·ᶻ aⁿᶻ <ᶻ p ]) (sym (·ᶻ-nullifiesˡ aⁿᶻ)) ⟩
    bᶻ ·ᶻ aⁿᶻ <ᶻ 0 ·ᶻ aⁿᶻ ⇒ᵖ⟨ ·ᶻ-reflects-<ᶻ bᶻ 0 aⁿᶻ 0<aⁿᶻ ⟩
    bᶻ        <ᶻ 0        ◼ᵖ) .snd aᶻ<0
  γ .snd 0<aᶻ = (
    0        <ᶻ aᶻ        ⇒ᵖ⟨ ·ᶻ-preserves-<ᶻ 0 aᶻ bⁿᶻ 0<bⁿᶻ ⟩
    0 ·ᶻ bⁿᶻ <ᶻ aᶻ ·ᶻ bⁿᶻ ⇒ᵖ⟨ (subst (λ p → [ p <ᶻ aᶻ ·ᶻ bⁿᶻ ]) $ ·ᶻ-nullifiesˡ bⁿᶻ) ⟩
    0        <ᶻ aᶻ ·ᶻ bⁿᶻ ⇒ᵖ⟨ subst (λ p → [ 0 <ᶻ p ]) r ⟩
    0        <ᶻ bᶻ ·ᶻ aⁿᶻ ⇒ᵖ⟨ subst (λ p → [ p <ᶻ bᶻ ·ᶻ aⁿᶻ ]) (sym (·ᶻ-nullifiesˡ aⁿᶻ)) ⟩
    0 ·ᶻ aⁿᶻ <ᶻ bᶻ ·ᶻ aⁿᶻ ⇒ᵖ⟨ ·ᶻ-reflects-<ᶻ 0 bᶻ aⁿᶻ 0<aⁿᶻ ⟩
    0        <ᶻ bᶻ        ◼ᵖ) .snd 0<aᶻ

-- < on ℤ × ℕ₊₁ in terms of < on ℤ
_<'_ : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → hProp ℓ-zero
(aᶻ , aⁿ) <' (bᶻ , bⁿ) =
  let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
      bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
  in (aᶻ ·ᶻ bⁿᶻ) <ᶻ (bᶻ ·ᶻ aⁿᶻ)

private
  lem1 : ∀ x y z → [ 0 <ᶻ y ] → [ 0 <ᶻ z ] → (0 <ᶻ (x ·ᶻ y)) ≡ (0 <ᶻ (x ·ᶻ z))
  lem1 x y z p q =
     0       <ᶻ (x ·ᶻ y) ≡⟨ (λ i → ·ᶻ-nullifiesˡ y (~ i) <ᶻ x ·ᶻ y) ⟩
    (0 ·ᶻ y) <ᶻ (x ·ᶻ y) ≡⟨ sym $ ·ᶻ-creates-<ᶻ-≡ 0 x y p ⟩
     0       <ᶻ  x       ≡⟨ ·ᶻ-creates-<ᶻ-≡ 0 x z q ⟩
    (0 ·ᶻ z) <ᶻ (x ·ᶻ z) ≡⟨ (λ i → ·ᶻ-nullifiesˡ z i <ᶻ x ·ᶻ z) ⟩
     0       <ᶻ (x ·ᶻ z) ∎

<'-respects-∼ˡ : ∀ a b x → a ∼ b → a <' x ≡ b <' x
<'-respects-∼ˡ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) a~b = γ where
  aⁿᶻ = [1+ aⁿ ⁿ]ᶻ; 0<aⁿᶻ : [ 0 <ᶻ aⁿᶻ ]; 0<aⁿᶻ = 0<ᶻpos[suc] _
  bⁿᶻ = [1+ bⁿ ⁿ]ᶻ; 0<bⁿᶻ : [ 0 <ᶻ bⁿᶻ ]; 0<bⁿᶻ = 0<ᶻpos[suc] _
  xⁿᶻ = [1+ xⁿ ⁿ]ᶻ
  p : aᶻ ·ᶻ bⁿᶻ ≡ bᶻ ·ᶻ aⁿᶻ
  p = a~b
  γ : ((aᶻ ·ᶻ xⁿᶻ) <ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡ ((bᶻ ·ᶻ xⁿᶻ) <ᶻ (xᶻ ·ᶻ bⁿᶻ))
  γ = aᶻ ·ᶻ xⁿᶻ        <ᶻ xᶻ ·ᶻ aⁿᶻ        ≡⟨ ·ᶻ-creates-<ᶻ-≡ (aᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ aⁿᶻ) bⁿᶻ 0<bⁿᶻ ⟩
      aᶻ ·ᶻ xⁿᶻ ·ᶻ bⁿᶻ <ᶻ xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ ≡⟨ (λ i → ·ᶻ-commʳ aᶻ xⁿᶻ bⁿᶻ i <ᶻ xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ) ⟩
      aᶻ ·ᶻ bⁿᶻ ·ᶻ xⁿᶻ <ᶻ xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ ≡⟨ (λ i → p i ·ᶻ xⁿᶻ <ᶻ xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ) ⟩
      bᶻ ·ᶻ aⁿᶻ ·ᶻ xⁿᶻ <ᶻ xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ ≡⟨ (λ i → ·ᶻ-commʳ bᶻ aⁿᶻ xⁿᶻ i <ᶻ ·ᶻ-commʳ xᶻ aⁿᶻ bⁿᶻ i) ⟩
      bᶻ ·ᶻ xⁿᶻ ·ᶻ aⁿᶻ <ᶻ xᶻ ·ᶻ bⁿᶻ ·ᶻ aⁿᶻ ≡⟨ sym $ ·ᶻ-creates-<ᶻ-≡ (bᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ bⁿᶻ) aⁿᶻ 0<aⁿᶻ ⟩
      bᶻ ·ᶻ xⁿᶻ        <ᶻ xᶻ ·ᶻ bⁿᶻ        ∎

<'-respects-∼ʳ : ∀ x a b → a ∼ b → x <' a ≡ x <' b
<'-respects-∼ʳ x@(xᶻ , xⁿ) a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) a~b =
  let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ; 0<aⁿᶻ : [ 0 <ᶻ aⁿᶻ ]; 0<aⁿᶻ = 0<ᶻpos[suc] _
      bⁿᶻ = [1+ bⁿ ⁿ]ᶻ; 0<bⁿᶻ : [ 0 <ᶻ bⁿᶻ ]; 0<bⁿᶻ = 0<ᶻpos[suc] _
      xⁿᶻ = [1+ xⁿ ⁿ]ᶻ
      p : aᶻ ·ᶻ bⁿᶻ ≡ bᶻ ·ᶻ aⁿᶻ
      p = a~b
  in xᶻ ·ᶻ aⁿᶻ        <ᶻ aᶻ  ·ᶻ  xⁿᶻ        ≡⟨ (λ i → xᶻ ·ᶻ aⁿᶻ <ᶻ ·ᶻ-comm aᶻ xⁿᶻ i) ⟩
     xᶻ ·ᶻ aⁿᶻ        <ᶻ xⁿᶻ ·ᶻ  aᶻ         ≡⟨ ·ᶻ-creates-<ᶻ-≡ (xᶻ ·ᶻ aⁿᶻ) (xⁿᶻ ·ᶻ  aᶻ) bⁿᶻ 0<bⁿᶻ ⟩
     xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ <ᶻ xⁿᶻ ·ᶻ  aᶻ ·ᶻ bⁿᶻ  ≡⟨ (λ i → xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ <ᶻ ·ᶻ-assoc xⁿᶻ aᶻ bⁿᶻ (~ i)) ⟩
     xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ <ᶻ xⁿᶻ ·ᶻ (aᶻ ·ᶻ bⁿᶻ) ≡⟨ (λ i → xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ <ᶻ xⁿᶻ ·ᶻ (p i)) ⟩
     xᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ <ᶻ xⁿᶻ ·ᶻ (bᶻ ·ᶻ aⁿᶻ) ≡⟨ (λ i → ·ᶻ-commʳ xᶻ aⁿᶻ bⁿᶻ i <ᶻ ·ᶻ-assoc xⁿᶻ bᶻ aⁿᶻ i) ⟩
     xᶻ ·ᶻ bⁿᶻ ·ᶻ aⁿᶻ <ᶻ xⁿᶻ ·ᶻ  bᶻ ·ᶻ aⁿᶻ  ≡⟨ sym $ ·ᶻ-creates-<ᶻ-≡ (xᶻ ·ᶻ bⁿᶻ) (xⁿᶻ ·ᶻ bᶻ) aⁿᶻ 0<aⁿᶻ ⟩
     xᶻ ·ᶻ bⁿᶻ        <ᶻ xⁿᶻ ·ᶻ  bᶻ         ≡⟨ (λ i → xᶻ ·ᶻ bⁿᶻ <ᶻ ·ᶻ-comm xⁿᶻ bᶻ i) ⟩
     xᶻ ·ᶻ bⁿᶻ        <ᶻ bᶻ  ·ᶻ  xⁿᶻ        ∎

infixl 4 _<_
_<_ : hPropRel ℚ ℚ ℓ-zero
a < b = SetQuotient.rec2 {R = _∼_} {B = hProp ℓ-zero} isSetHProp _<'_ <'-respects-∼ˡ <'-respects-∼ʳ a b

_≤_ : hPropRel ℚ ℚ ℓ-zero
x ≤ y = ¬ᵖ (y < x)

min' : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ
min' (aᶻ , aⁿ) (bᶻ , bⁿ) =
  let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
      bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
  in minᶻ (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ)

max' : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ
max' (aᶻ , aⁿ) (bᶻ , bⁿ) =
  let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
      bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
  in maxᶻ (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ)

min'-sym : ∀ x y → min' x y ≡ min' y x
min'-sym (aᶻ , aⁿ) (bᶻ , bⁿ) = minᶻ-comm (aᶻ ·ᶻ [1+ bⁿ ⁿ]ᶻ) (bᶻ ·ᶻ [1+ aⁿ ⁿ]ᶻ)

max'-sym : ∀ x y → max' x y ≡ max' y x
max'-sym (aᶻ , aⁿ) (bᶻ , bⁿ) = maxᶻ-comm (aᶻ ·ᶻ [1+ bⁿ ⁿ]ᶻ) (bᶻ ·ᶻ [1+ aⁿ ⁿ]ᶻ)

min'-respects-∼ : (a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) : ℤ × ℕ₊₁)
                → a ∼ b
                → [1+ bⁿ ⁿ]ᶻ ·ᶻ min' a x ≡ [1+ aⁿ ⁿ]ᶻ ·ᶻ min' b x
min'-respects-∼ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) a~b =
  bⁿᶻ ·ᶻ minᶻ (aᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ aⁿᶻ)            ≡⟨ ·ᶻ-minᶻ-distribˡ (aᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ aⁿᶻ) bⁿᶻ 0≤bⁿᶻ ⟩
  minᶻ (bⁿᶻ ·ᶻ (aᶻ ·ᶻ xⁿᶻ)) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡⟨ (λ i → minᶻ (·ᶻ-assoc bⁿᶻ aᶻ xⁿᶻ i) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ))) ⟩
  minᶻ ((bⁿᶻ ·ᶻ aᶻ) ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡⟨ (λ i → minᶻ ((·ᶻ-comm bⁿᶻ aᶻ i) ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ))) ⟩
  minᶻ ((aᶻ ·ᶻ bⁿᶻ) ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡⟨ (λ i → minᶻ (p i ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ))) ⟩
  minᶻ ((bᶻ ·ᶻ aⁿᶻ) ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡⟨ (λ i → minᶻ (·ᶻ-comm bᶻ aⁿᶻ i ·ᶻ xⁿᶻ) (·ᶻ-assoc bⁿᶻ xᶻ aⁿᶻ i)) ⟩
  minᶻ ((aⁿᶻ ·ᶻ bᶻ) ·ᶻ xⁿᶻ) ((bⁿᶻ ·ᶻ xᶻ) ·ᶻ aⁿᶻ) ≡⟨ (λ i → minᶻ (·ᶻ-assoc aⁿᶻ bᶻ xⁿᶻ (~ i)) (·ᶻ-comm (bⁿᶻ ·ᶻ xᶻ) aⁿᶻ i)) ⟩
  minᶻ (aⁿᶻ ·ᶻ (bᶻ ·ᶻ xⁿᶻ)) (aⁿᶻ ·ᶻ (bⁿᶻ ·ᶻ xᶻ)) ≡⟨ sym $ ·ᶻ-minᶻ-distribˡ (bᶻ ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ xᶻ) aⁿᶻ 0≤aⁿᶻ ⟩
  aⁿᶻ ·ᶻ minᶻ (bᶻ ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ xᶻ)            ≡⟨ (λ i → aⁿᶻ ·ᶻ minᶻ (bᶻ ·ᶻ xⁿᶻ) (·ᶻ-comm bⁿᶻ xᶻ i)) ⟩
  aⁿᶻ ·ᶻ minᶻ (bᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ bⁿᶻ)            ∎
  where
    aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
    bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
    xⁿᶻ = [1+ xⁿ ⁿ]ᶻ
    p : aᶻ ·ᶻ bⁿᶻ ≡ bᶻ ·ᶻ aⁿᶻ
    p = a~b
    0≤aⁿᶻ : [ 0 ≤ᶻ aⁿᶻ ]
    0≤aⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p
    0≤bⁿᶻ : [ 0 ≤ᶻ bⁿᶻ ]
    0≤bⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p

-- same proof as for min
max'-respects-∼ : (a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) : ℤ × ℕ₊₁)
  → a ∼ b
  → [1+ bⁿ ⁿ]ᶻ ·ᶻ max' a x ≡ [1+ aⁿ ⁿ]ᶻ ·ᶻ max' b x
max'-respects-∼ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) a~b =
  bⁿᶻ ·ᶻ maxᶻ (aᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ aⁿᶻ)            ≡⟨ ·ᶻ-maxᶻ-distribˡ (aᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ aⁿᶻ) bⁿᶻ 0≤bⁿᶻ ⟩
  maxᶻ (bⁿᶻ ·ᶻ (aᶻ ·ᶻ xⁿᶻ)) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡⟨ (λ i → maxᶻ (·ᶻ-assoc bⁿᶻ aᶻ xⁿᶻ i) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ))) ⟩
  maxᶻ ((bⁿᶻ ·ᶻ aᶻ) ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡⟨ (λ i → maxᶻ ((·ᶻ-comm bⁿᶻ aᶻ i) ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ))) ⟩
  maxᶻ ((aᶻ ·ᶻ bⁿᶻ) ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡⟨ (λ i → maxᶻ (p i ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ))) ⟩
  maxᶻ ((bᶻ ·ᶻ aⁿᶻ) ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ (xᶻ ·ᶻ aⁿᶻ)) ≡⟨ (λ i → maxᶻ (·ᶻ-comm bᶻ aⁿᶻ i ·ᶻ xⁿᶻ) (·ᶻ-assoc bⁿᶻ xᶻ aⁿᶻ i)) ⟩
  maxᶻ ((aⁿᶻ ·ᶻ bᶻ) ·ᶻ xⁿᶻ) ((bⁿᶻ ·ᶻ xᶻ) ·ᶻ aⁿᶻ) ≡⟨ (λ i → maxᶻ (·ᶻ-assoc aⁿᶻ bᶻ xⁿᶻ (~ i)) (·ᶻ-comm (bⁿᶻ ·ᶻ xᶻ) aⁿᶻ i)) ⟩
  maxᶻ (aⁿᶻ ·ᶻ (bᶻ ·ᶻ xⁿᶻ)) (aⁿᶻ ·ᶻ (bⁿᶻ ·ᶻ xᶻ)) ≡⟨ sym $ ·ᶻ-maxᶻ-distribˡ (bᶻ ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ xᶻ) aⁿᶻ 0≤aⁿᶻ ⟩
  aⁿᶻ ·ᶻ maxᶻ (bᶻ ·ᶻ xⁿᶻ) (bⁿᶻ ·ᶻ xᶻ)            ≡⟨ (λ i → aⁿᶻ ·ᶻ maxᶻ (bᶻ ·ᶻ xⁿᶻ) (·ᶻ-comm bⁿᶻ xᶻ i)) ⟩
  aⁿᶻ ·ᶻ maxᶻ (bᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ bⁿᶻ)            ∎
  where
    aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
    bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
    xⁿᶻ = [1+ xⁿ ⁿ]ᶻ
    p : aᶻ ·ᶻ bⁿᶻ ≡ bᶻ ·ᶻ aⁿᶻ
    p = a~b
    0≤aⁿᶻ : [ 0 ≤ᶻ aⁿᶻ ]
    0≤aⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p
    0≤bⁿᶻ : [ 0 ≤ᶻ bⁿᶻ ]
    0≤bⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p

min : ℚ → ℚ → ℚ
min a b = onCommonDenomSym min' min'-sym min'-respects-∼ a b

max : ℚ → ℚ → ℚ
max a b = onCommonDenomSym max' max'-sym max'-respects-∼ a b

-- injᶻⁿ⁺¹ : ∀ x → [ 0 <ᶻ x ] → Σ[ y ∈ ℕ₊₁ ] x ≡ [1+ y ⁿ]ᶻ
-- injᶻⁿ⁺¹ (signed spos zero) p = ⊥-elim {A = λ _ → Σ[ y ∈ ℕ₊₁ ] ℤ.posneg i0 ≡ [1+ y ⁿ]ᶻ}  (¬-<ⁿ-zero p)
-- injᶻⁿ⁺¹ (signed sneg  zero) p = ⊥-elim {A = λ _ → Σ[ y ∈ ℕ₊₁ ] ℤ.posneg i1 ≡ [1+ y ⁿ]ᶻ}  (¬-<ⁿ-zero p)
-- injᶻⁿ⁺¹ (ℤ.posneg i)        p = ⊥-elim {A = λ _ → Σ[ y ∈ ℕ₊₁ ] ℤ.posneg i  ≡ [1+ y ⁿ]ᶻ}  (¬-<ⁿ-zero p)
-- injᶻⁿ⁺¹ (signed spos (suc n)) p =  1+ n , refl

absᶻ⁺¹ : ℤ → ℕ₊₁
absᶻ⁺¹ (pos zero)    = 1+ 0
absᶻ⁺¹ (neg zero)    = 1+ 0
absᶻ⁺¹ (posneg i)    = 1+ 0
absᶻ⁺¹ (pos (suc n)) = 1+ n
absᶻ⁺¹ (neg (suc n)) = 1+ n

-- absᶻ⁺¹-identity⁺ : ∀ x → [ 0 <ⁿ x ] → [1+ absᶻ⁺¹ (pos x) ⁿ]ᶻ ≡ pos x
-- absᶻ⁺¹-identity⁺ zero    p = ⊥-elim {A = λ _ → [1+ absᶻ⁺¹ (pos zero) ⁿ]ᶻ ≡ pos zero} (<ⁿ-irrefl 0 p)
-- absᶻ⁺¹-identity⁺ (suc x) p = refl
--
-- absᶻ⁺¹-identity⁻ : ∀ x → [ 0 <ⁿ x ] → [1+ absᶻ⁺¹ (neg x) ⁿ]ᶻ ≡ pos x
-- absᶻ⁺¹-identity⁻ zero p = ⊥-elim {A = λ _ → [1+ absᶻ⁺¹ (neg zero) ⁿ]ᶻ ≡ pos zero} (<ⁿ-irrefl 0 p)
-- absᶻ⁺¹-identity⁻ (suc x) p = refl

absᶻ⁺¹-identity : ∀ x → [ x #ᶻ 0 ] → [1+ absᶻ⁺¹ x ⁿ]ᶻ ≡ pos (absᶻ x)
absᶻ⁺¹-identity (pos zero)    p = ⊥-elim {A = λ _ → pos 1 ≡ pos 0} $ #ᶻ⇒≢ (posneg i0) p refl
absᶻ⁺¹-identity (neg zero)    p = ⊥-elim {A = λ _ → pos 1 ≡ pos 0} $ #ᶻ⇒≢ (posneg i1) p posneg
absᶻ⁺¹-identity (posneg i)    p = ⊥-elim {A = λ _ → pos 1 ≡ pos 0} $ #ᶻ⇒≢ (posneg i ) p (λ j → posneg (i ∧ j))
absᶻ⁺¹-identity (pos (suc n)) p = refl
absᶻ⁺¹-identity (neg (suc n)) p = refl

absᶻ⁺¹-identityⁿ : ∀ x → [ x #ᶻ 0 ] → suc (ℕ₊₁.n (absᶻ⁺¹ x)) ≡ absᶻ x
absᶻ⁺¹-identityⁿ x p i = absᶻ (absᶻ⁺¹-identity x p i)

sign' : ℤ × ℕ₊₁ → Sign
sign' (z , n) = signᶻ z

sign'-preserves-∼ : (a b : ℤ × ℕ₊₁) → a ∼ b → sign' a ≡ sign' b
sign'-preserves-∼ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) p =  sym (lem aᶻ bⁿ) ∙ ψ ∙ lem bᶻ aⁿ where
  a' = absᶻ aᶻ ·ⁿ suc (ℕ₊₁.n bⁿ)
  b' = absᶻ bᶻ ·ⁿ suc (ℕ₊₁.n aⁿ)
  γ : signed (signᶻ aᶻ ⊕ spos) a' ≡ signed (signᶻ bᶻ ⊕ spos) b'
  γ = p
  ψ : signᶻ (signed (signᶻ aᶻ ⊕ spos) a') ≡ signᶻ (signed (signᶻ bᶻ ⊕ spos) b')
  ψ i = signᶻ (γ i)
  lem : ∀ x y → signᶻ (signed (signᶻ x ⊕ spos) (absᶻ x ·ⁿ suc (ℕ₊₁.n y))) ≡ signᶻ x
  lem (pos zero)    y = refl
  lem (neg zero)    y = refl
  lem (posneg i)    y = refl
  lem (pos (suc n)) y = refl
  lem (neg (suc n)) y = refl

sign : ℚ → Sign
sign = SetQuotient.rec {R = _∼_} {B = Sign} Bool.isSetBool sign' sign'-preserves-∼

sign-signᶻ-identity : ∀ z n → sign [ z , n ]ᶠ ≡ signᶻ z
sign-signᶻ-identity z n = refl


text:
-- TODO: Generalize and move to Structure.Categorical.Proofs
module Structure.Category.Proofs where

import      Lvl
open import Data
open import Data.Tuple as Tuple using (_,_)
open import Functional using (const ; swap ; _$_)
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Category
open import Structure.Categorical.Names
open import Structure.Categorical.Properties
import      Structure.Operator.Properties as Properties
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Function
open import Syntax.Transitivity
open import Type

module _
  {ℓₒ ℓₘ ℓₑ : Lvl.Level}
  {Obj : Type{ℓₒ}}
  {Morphism : Obj → Obj → Type{ℓₘ}}
  ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(Morphism x y) ⦄
  (cat : Category(Morphism))
  where

  open Category(cat)
  open Category.ArrowNotation(cat)
  open Morphism.OperModule(\{x} → _∘_ {x})
  open Morphism.IdModule(\{x} → _∘_ {x})(id)
  private open module [≡]-Equivalence {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv{x}{y} ⦄) using ()

  private variable x y z : Obj
  private variable f g h i : x ⟶ y

  associate4-123-321 : (((f ∘ g) ∘ h) ∘ i ≡ f ∘ (g ∘ (h ∘ i)))
  associate4-123-321 = Morphism.associativity(_∘_) 🝖 Morphism.associativity(_∘_)

  associate4-123-213 : (((f ∘ g) ∘ h) ∘ i ≡ (f ∘ (g ∘ h)) ∘ i)
  associate4-123-213 = congruence₂ₗ(_∘_)(_) (Morphism.associativity(_∘_))

  associate4-321-231 : (f ∘ (g ∘ (h ∘ i)) ≡ f ∘ ((g ∘ h) ∘ i))
  associate4-321-231 = congruence₂ᵣ(_∘_)(_) (symmetry(_≡_) (Morphism.associativity(_∘_)))

  associate4-213-121 : ((f ∘ (g ∘ h)) ∘ i ≡ (f ∘ g) ∘ (h ∘ i))
  associate4-213-121 = symmetry(_≡_) (congruence₂ₗ(_∘_)(_) (Morphism.associativity(_∘_))) 🝖 Morphism.associativity(_∘_)

  associate4-231-213 : f ∘ ((g ∘ h) ∘ i) ≡ (f ∘ (g ∘ h)) ∘ i
  associate4-231-213 = symmetry(_≡_) (Morphism.associativity(_∘_))

  associate4-231-123 : f ∘ ((g ∘ h) ∘ i) ≡ ((f ∘ g) ∘ h) ∘ i
  associate4-231-123 = associate4-231-213 🝖 symmetry(_≡_) associate4-123-213

  associate4-231-121 : (f ∘ ((g ∘ h) ∘ i) ≡ (f ∘ g) ∘ (h ∘ i))
  associate4-231-121 = congruence₂ᵣ(_∘_)(_) (Morphism.associativity(_∘_)) 🝖 symmetry(_≡_) (Morphism.associativity(_∘_))

  id-automorphism : Automorphism(id{x})
  ∃.witness id-automorphism = id
  ∃.proof   id-automorphism = intro(Morphism.identityₗ(_∘_)(id)) , intro(Morphism.identityᵣ(_∘_)(id))

  inverse-isomorphism : (f : x ⟶ y) → ⦃ _ : Isomorphism(f) ⦄ → Isomorphism(inv f)
  ∃.witness (inverse-isomorphism f) = f
  ∃.proof   (inverse-isomorphism f) = intro (inverseᵣ(f)(inv f)) , intro (inverseₗ(f)(inv f)) where
    open Isomorphism(f)

  module _ ⦃ op : ∀{x y z} → BinaryOperator(_∘_ {x}{y}{z}) ⦄ where
    op-closed-under-isomorphism : ∀{A B C : Obj} → (f : B ⟶ C) → (g : A ⟶ B) → ⦃ _ : Isomorphism(f) ⦄ → ⦃ _ : Isomorphism(g) ⦄ → Isomorphism(f ∘ g)
    ∃.witness (op-closed-under-isomorphism f g) = inv g ∘ inv f
    Tuple.left (∃.proof (op-closed-under-isomorphism f g)) = intro $
      (inv g ∘ inv f) ∘ (f ∘ g) 🝖-[ associate4-213-121 ]-sym
      (inv g ∘ (inv f ∘ f)) ∘ g 🝖-[ congruence₂ₗ(_∘_) ⦃ op ⦄ (g) (congruence₂ᵣ(_∘_) ⦃ op ⦄ (inv g) (Morphism.inverseₗ(_∘_)(id) (f)(inv f))) ]
      (inv g ∘ id) ∘ g          🝖-[ congruence₂ₗ(_∘_) ⦃ op ⦄ (g) (Morphism.identityᵣ(_∘_)(id)) ]
      inv g ∘ g                 🝖-[ Morphism.inverseₗ(_∘_)(id) (g)(inv g) ]
      id                        🝖-end
      where
        open Isomorphism(f)
        open Isomorphism(g)
    Tuple.right (∃.proof (op-closed-under-isomorphism f g)) = intro $
      (f ∘ g) ∘ (inv g ∘ inv f) 🝖-[ associate4-213-121 ]-sym
      (f ∘ (g ∘ inv g)) ∘ inv f 🝖-[ congruence₂ₗ(_∘_) ⦃ op ⦄ (_) (congruence₂ᵣ(_∘_) ⦃ op ⦄ (_) (Morphism.inverseᵣ(_∘_)(id) (_)(_))) ]
      (f ∘ id) ∘ inv f          🝖-[ congruence₂ₗ(_∘_) ⦃ op ⦄ (_) (Morphism.identityᵣ(_∘_)(id)) ]
      f ∘ inv f                 🝖-[ Morphism.inverseᵣ(_∘_)(id) (_)(_) ]
      id                        🝖-end
      where
        open Isomorphism(f)
        open Isomorphism(g)

  instance
    Isomorphic-reflexivity : Reflexivity(Isomorphic)
    ∃.witness (Reflexivity.proof Isomorphic-reflexivity) = id
    ∃.proof   (Reflexivity.proof Isomorphic-reflexivity) = id-automorphism

  instance
    Isomorphic-symmetry : Symmetry(Isomorphic)
    ∃.witness (Symmetry.proof Isomorphic-symmetry iso-xy) = inv(∃.witness iso-xy)
    ∃.proof   (Symmetry.proof Isomorphic-symmetry iso-xy) = inverse-isomorphism(∃.witness iso-xy)

  module _ ⦃ op : ∀{x y z} → BinaryOperator(_∘_ {x}{y}{z}) ⦄ where
    instance
      Isomorphic-transitivity : Transitivity(Isomorphic)
      ∃.witness (Transitivity.proof Isomorphic-transitivity ([∃]-intro xy) ([∃]-intro yz)) = yz ∘ xy
      ∃.proof   (Transitivity.proof Isomorphic-transitivity ([∃]-intro xy) ([∃]-intro yz)) = op-closed-under-isomorphism ⦃ op ⦄ yz xy

    instance
      Isomorphic-equivalence : Equivalence(Isomorphic)
      Isomorphic-equivalence = record{}

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 OscarEverything where

open import OscarPrelude
open import HasSubstantiveDischarge


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

module Cardinality.Finite.SplitEnumerable.Instances where

open import Cardinality.Finite.SplitEnumerable
open import Cardinality.Finite.SplitEnumerable.Inductive
open import Cardinality.Finite.ManifestBishop using (_|Π|_)
open import Data.Fin
open import Prelude
open import Data.List.Membership
open import Data.Tuple

import Data.Unit.UniversePolymorphic as Poly

private
  infixr 4 _?×_
  data _?×_ (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
    pair : A → B → A ?× B

instance
  poly-inst : ∀ {a} → Poly.⊤ {a}
  poly-inst = Poly.tt

module _ {a b} {A : Type a} (B : A → Type b) where
  Im-Type : (xs : List A) → Type (a ℓ⊔ b)
  Im-Type = foldr (λ x xs → ℰ! (B x) ?× xs) Poly.⊤

  Tup-Im-Lookup : ∀ x (xs : List A) → x ∈ xs → Im-Type xs → ℰ! (B x)
  Tup-Im-Lookup x (y ∷ xs) (f0   , y≡x ) (pair ℰ!⟨Bx⟩ _) = subst (ℰ! ∘ B) y≡x ℰ!⟨Bx⟩
  Tup-Im-Lookup x (y ∷ xs) (fs n , x∈ys) (pair _ tup) = Tup-Im-Lookup x xs (n , x∈ys) tup

  Tup-Im-Pi : (xs : ℰ! A) → Im-Type (xs .fst) → ∀ x → ℰ! (B x)
  Tup-Im-Pi xs tup x = Tup-Im-Lookup x (xs .fst) (xs .snd x) tup

instance
  inst-pair : ⦃ lhs : A ⦄ ⦃ rhs : B ⦄ → A ?× B
  inst-pair ⦃ lhs ⦄ ⦃ rhs ⦄ = pair lhs rhs

instance
  fin-sigma : ⦃ lhs : ℰ! A ⦄ {B : A → Type b} → ⦃ rhs : Im-Type B (lhs .fst) ⦄ → ℰ! (Σ A B)
  fin-sigma ⦃ lhs ⦄ ⦃ rhs ⦄ = lhs |Σ| Tup-Im-Pi _ lhs rhs

instance
  fin-pi : ⦃ lhs : ℰ! A ⦄ {B : A → Type b} → ⦃ rhs : Im-Type B (lhs .fst) ⦄ → (ℰ! ((x : A) → B x))
  fin-pi ⦃ lhs ⦄ ⦃ rhs ⦄ = lhs |Π| Tup-Im-Pi _ lhs rhs

-- instance
--   fin-prod : ⦃ lhs : ℰ! A ⦄ ⦃ rhs : ℰ! B ⦄ → ℰ! (A × B)
--   fin-prod ⦃ lhs ⦄ ⦃ rhs ⦄ = lhs |×| rhs

-- instance
--   fin-fun : {A B : Type₀} ⦃ lhs : ℰ! A ⦄ ⦃ rhs : ℰ! B ⦄ → ℰ! (A → B)
--   fin-fun ⦃ lhs ⦄ ⦃ rhs ⦄ = lhs |Π| λ _ → rhs

instance
  fin-sum : ⦃ lhs : ℰ! A ⦄ ⦃ rhs : ℰ! B ⦄ → ℰ! (A ⊎ B)
  fin-sum ⦃ lhs ⦄ ⦃ rhs ⦄ = lhs |⊎| rhs

instance
  fin-bool : ℰ! Bool
  fin-bool = ℰ!⟨2⟩

instance
  fin-top : ℰ! ⊤
  fin-top = ℰ!⟨⊤⟩

instance
  fin-bot : ℰ! ⊥
  fin-bot = ℰ!⟨⊥⟩

instance
  fin-fin : ∀ {n} → ℰ! (Fin n)
  fin-fin  = ℰ!⟨Fin⟩

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- 2012-03-08 Andreas
module _ where

{-# TERMINATING #-}

-- error: misplaced pragma


text:
-- Andreas, 2014-01-16, issue 1406
-- Agda with K again is inconsistent with classical logic

-- {-# OPTIONS --cubical-compatible #-}

open import Common.Level
open import Common.Prelude
open import Common.Equality

cast : {A B : Set} (p : A ≡ B) (a : A) → B
cast refl a = a

data HEq {α} {A : Set α} (a : A) : {B : Set α} (b : B) → Set (lsuc α) where
  refl : HEq a a

mkHet : {A B : Set} (eq : A ≡ B) (a : A) → HEq a (cast eq a)
mkHet refl a = refl

-- Type with a big forced index. (Allowed unless --cubical-compatible.)
-- This definition is allowed in Agda master since 2014-10-17
-- https://github.com/agda/agda/commit/9a4ebdd372dc0510e2d77e726fb0f4e6f56781e8
-- However, probably the consequences of this new feature have not
-- been grasped fully yet.

data SING : (F : Set → Set) → Set where
  sing : (F : Set → Set) → SING F

-- The following theorem is the culprit.
-- It needs K.
-- It allows us to unify forced indices, which I think is wrong.

thm : ∀{F G : Set → Set} (a : SING F) (b : SING G) (p : HEq a b) → F ≡ G
thm (sing F) (sing .F) refl = refl

-- Note that a direct matching fails, as it generates heterogeneous constraints.
--   thm a .a refl = refl
-- However, by matching on the constructor sing, the forced index
-- is exposed to unification.

-- As a consequence of thm,
-- SING is injective which it clearly should not be.

SING-inj : ∀ (F G : Set → Set) (p : SING F ≡ SING G) → F ≡ G
SING-inj F G p = thm (sing F) _ (mkHet p (sing F))

-- The rest is an adaption of Chung-Kil Hur's proof (2010)

data Either {α} (A B : Set α) : Set α where
  inl : A → Either A B
  inr : B → Either A B

data Inv (A : Set) : Set1 where
  inv : (F : Set → Set) (eq : SING F ≡ A) → Inv A

¬ : ∀{α} → Set α → Set α
¬ A = A → ⊥

-- Classical logic

postulate em : ∀{α} (A : Set α) → Either A (¬ A)

Cantor' : (A : Set) → Either (Inv A) (¬ (Inv A)) → Set
Cantor' A (inl (inv F eq)) = ¬ (F A)
Cantor' A (inr _)          = ⊤

Cantor : Set → Set
Cantor A = Cantor' A (em (Inv A))

C : Set
C = SING Cantor

ic : Inv C
ic = inv Cantor refl

cast' : ∀{F G} → SING F ≡ SING G → ¬ (F C) → ¬ (G C)
cast' eq = subst (λ F → ¬ (F C)) (SING-inj _ _ eq)

-- Self application 1
diag : ¬ (Cantor C)
diag c with em (Inv C)  | c
diag c | inl (inv F eq) | c' = cast' eq c' c
diag _ | inr f          | _  = f ic

-- Self application 2
diag' : Cantor C
diag' with em (Inv C)
diag' | inl (inv F eq) = cast' (sym eq) diag
diag' | inr _          = _

absurd : ⊥
absurd = diag diag'


text:
{-# OPTIONS --cubical-compatible #-}
------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------

module Common.Level where

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

-- Lifting.

record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A

open Lift public