text:
{-# OPTIONS --without-K --safe #-}
module Source.Size where

open import Util.HoTT.HLevel.Core
open import Util.Prelude

infix  4 _<_
infixl 4 _∙_

mutual
  data Ctx : Set where
    [] : Ctx
    _∙_ : (Δ : Ctx) (n : Size Δ) → Ctx

  data Var : (Δ : Ctx) → Set where
    zero : ∀ {Δ n} → Var (Δ ∙ n)
    suc : ∀ {Δ n} (x : Var Δ) → Var (Δ ∙ n)

  data Size : (Δ : Ctx) → Set where
    var : ∀ {Δ} (x : Var Δ) → Size Δ
    ∞ zero : ∀ {Δ} → Size Δ
    suc : ∀ {Δ} (n : Size Δ) → Size Δ

pattern ⋆ = suc ∞

variable
  Δ Ω Δ′ Ω′ Δ″ Ω″ : Ctx
  x y z : Var Δ
  n m o p b n′ m′ o′ p′ b′ : Size Δ

wk : Size Δ → Size (Δ ∙ n)
wk (var x) = var (suc x)
wk ∞ = ∞
wk zero = zero
wk (suc m) = suc (wk m)

bound : Var Δ → Size Δ
bound (zero {Δ} {n}) = wk n
bound (suc x) = wk (bound x)

data _<_ {Δ} : (n m : Size Δ) → Set where
  var : n ≡ bound x → var x < n
  zero<suc : zero < suc n
  zero<∞ : zero < ∞
  suc<suc : (n<m : n < m) → suc n < suc m
  suc<∞ : (n<∞ : n < ∞) → suc n < ∞
  <-trans : n < m → m < o → n < o
  <suc : n < suc n

data _≤_ {Δ} : (n m : Size Δ) → Set where
  reflexive : n ≡ m → n ≤ m
  <→≤ : n < m → n ≤ m

pattern ≤-refl = reflexive refl

pattern v0 = var zero
pattern v1 = var (suc zero)
pattern v2 = var (suc (suc zero))

abstract
  n<m→n<Sm : n < m → n < suc m
  n<m→n<Sm n<m = <-trans n<m <suc

  n≤m→n<Sm : n ≤ m → n < suc m
  n≤m→n<Sm ≤-refl = <suc
  n≤m→n<Sm (<→≤ n<m) = n<m→n<Sm n<m

  var<suc : var x ≤ n → var x < suc n
  var<suc = n≤m→n<Sm

  ∞<suc : ∞ ≤ n → ∞ < suc n
  ∞<suc = n≤m→n<Sm

  Sn<m→n<m : suc n < m → n < m
  Sn<m→n<m (suc<suc n<m) = <-trans n<m <suc
  Sn<m→n<m (suc<∞ n<∞) = n<∞
  Sn<m→n<m (<-trans Sn<o o<m) = <-trans (Sn<m→n<m Sn<o) o<m
  Sn<m→n<m <suc = <-trans <suc (suc<suc <suc)

  suc-inj-Var : Var.suc {n = n} x ≡ suc y → x ≡ y
  suc-inj-Var refl = refl

  suc≡-prop-Var : (p : Var.suc {n = n} x ≡ suc y) → p ≡ cong suc (suc-inj-Var p)
  suc≡-prop-Var refl = refl

  Var-IsSet : (p q : x ≡ y) → p ≡ q
  Var-IsSet {x = zero} {zero} refl refl = refl
  Var-IsSet {x = suc x} {suc .x} p refl
    = trans (suc≡-prop-Var p) (cong (cong suc) (Var-IsSet _ _))

  suc-inj-Size : Size.suc n ≡ suc m → n ≡ m
  suc-inj-Size refl = refl

  suc≡-prop-Size : (p : Size.suc n ≡ suc m) → p ≡ cong suc (suc-inj-Size p)
  suc≡-prop-Size refl = refl

  var-inj-Size : Size.var x ≡ var y → x ≡ y
  var-inj-Size refl = refl

  var≡-prop-Size : (p : Size.var x ≡ var y) → p ≡ cong var (var-inj-Size p)
  var≡-prop-Size refl = refl

  Size-IsSet : (p q : n ≡ m) → p ≡ q
  Size-IsSet {n = var x} {var .x} p refl
    = trans (var≡-prop-Size p) (cong (cong var) (Var-IsSet _ _))
  Size-IsSet {n = ∞} {∞} refl refl = refl
  Size-IsSet {n = zero} {zero} refl refl = refl
  Size-IsSet {n = suc n} {suc .n} p refl
    = trans (suc≡-prop-Size p) (cong (cong suc) (Size-IsSet _ _))

  wk-resp-< : n < m → wk {n = o} n < wk m
  wk-resp-< (var p) = var (cong wk p)
  wk-resp-< zero<suc = zero<suc
  wk-resp-< zero<∞ = zero<∞
  wk-resp-< (suc<suc n<m) = suc<suc (wk-resp-< n<m)
  wk-resp-< (suc<∞ n<∞) = suc<∞ (wk-resp-< n<∞)
  wk-resp-< (<-trans n<o o<m) = <-trans (wk-resp-< n<o) (wk-resp-< o<m)
  wk-resp-< <suc = <suc

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Prelude where
  open import Agda.Primitive using (Level; lzero; lsuc) renaming (_⊔_ to lmax)

  -- empty type
  data ⊥ : Set where

  -- from false, derive whatever
  abort : ∀ {C : Set} → ⊥ → C
  abort ()

  -- unit
  data ⊤ : Set where
    <> : ⊤

  -- sums
  data _+_ (A B : Set) : Set where
    Inl : A → A + B
    Inr : B → A + B

  -- pairs
  infixr 1 _,_
  record Σ {l1 l2 : Level} (A : Set l1) (B : A → Set l2) : Set (lmax l1 l2) where
    constructor _,_
    field
      π1 : A
      π2 : B π1
  open Σ public

  syntax Σ A (\ x -> B) = Σ[ x ∈ A ] B

  _×_ : {l1 : Level} {l2 : Level} → (Set l1) → (Set l2) → Set (lmax l1 l2)
  A × B = Σ A λ _ → B

  infixr 1 _×_

  -- equality
  data _==_ {l : Level} {A : Set l} (M : A) : A → Set l where
    refl : M == M

  infixr 9 _==_

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

  _·_ : {l : Level} {α : Set l} {x y z : α} → x == y → y == z → x == z
  refl · refl = refl

  -- β: ! (refl m)  == refl m
  ! : {l : Level} {α : Set l} {x y : α} → x == y → y == x
  ! refl = refl

  -- β: (ap f (refl m)) == refl (f m)
  ap1 : {l1 l2 : Level} {α : Set l1} {β : Set l2} {x y : α} (F : α → β)
          → x == y → F x == F y
  ap1 F refl = refl

  -- β? : tr β (refl x) y == y
  tr : {l1 l2 : Level} {α : Set l1} {x y : α}
                    (B : α → Set l2)
                    → x == y
                    → B x
                    → B y
  tr B refl x₁ = x₁

  ap2 : {l1 l2 l3 : Level}
        {A : Set l1} {B : Set l2} {C : Set l3}
        {M N : A} {M' N' : B}
        (f : A -> B -> C) -> M == N -> M' == N' -> (f M M') == (f N N')
  ap2 f refl refl = refl

  infix  2 _■
  infixr 2 _=<_>_

  _=<_>_ : {l : Level} {A : Set l} (x : A) {y z : A} → x == y → y == z → x == z
  _ =< p1 > p2 = p1 · p2

  _■ : {l : Level} {A : Set l} (x : A) → x == x
  _■ _ = refl

  -- options
  data Maybe (A : Set) : Set where
    Some : A → Maybe A
    None : Maybe A

  -- the some constructor is injective. perhaps unsurprisingly.
  someinj : {A : Set} {x y : A} → Some x == Some y → x == y
  someinj refl = refl

  -- order
  data Order : Set where
    Less : Order
    Equal : Order
    Greater : Order

  -- function extensionality
  postulate
     funext : {A : Set} {B : A → Set} {f g : (x : A) → (B x)} →
              ((x : A) → f x == g x) → f == g

ext: agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monoidal.Cartesian.Pentagon where

open import Categories.Support.PropositionalEquality using (_≣_; ≣-refl)
open import Categories.Category using (Category; module Category)
open import Categories.Object.BinaryProducts
open import Categories.Square

module Law {o ℓ e} (C : Category o ℓ e) (P : BinaryProducts C) where
  open Category C
  open BinaryProducts P

  shave3ˡ : ∀ {A B C} → ((A × B) × C) ⇒ (B × C)
  shave3ˡ = ⟨ π₂ ∘ π₁ , π₂ ⟩ -- in real life, 'first π₂'

  shave4ˡʳ : ∀ {A B C D} → (((A × B) × C) × D) ⇒ (B × C)
  shave4ˡʳ = ⟨ (π₂ ∘ π₁) ∘ π₁ , π₂ ∘ π₁ ⟩

  shave4ˡ : ∀ {A B C D} → (((A × B) × C) × D) ⇒ ((B × C) × D)
  shave4ˡ = ⟨ shave4ˡʳ , π₂ ⟩

  .π₁∘assocˡ : ∀ {X Y Z} → π₁ ∘ assocˡ {X} {Y} {Z} ≡ π₁ ∘ π₁
  π₁∘assocˡ = commute₁

  .π₂∘assocˡ : ∀ {X Y Z} → π₂ ∘ assocˡ {X} {Y} {Z} ≡ shave3ˡ
  π₂∘assocˡ = commute₂

  .π₂₁-assocˡ : ∀ {X Y Z W} → (π₂ ∘ π₁) ∘ assocˡ {X × Y} {Z} {W} ≡ (π₂ ∘ π₁) ∘ π₁
  π₂₁-assocˡ =
    begin
      (π₂ ∘ π₁) ∘ assocˡ
    ↓⟨ assoc ⟩
      π₂ ∘ (π₁ ∘ assocˡ)
    ↓⟨ ∘-resp-≡ʳ π₁∘assocˡ ⟩
      π₂ ∘ (π₁ ∘ π₁)
    ↑⟨ assoc ⟩
      (π₂ ∘ π₁) ∘ π₁
    ∎
    where
    open HomReasoning

  .π₁₁-assocˡ : ∀ {X Y Z W} → (π₁ ∘ π₁) ∘ assocˡ {_} {Z} {W} ≡ (π₁ ∘ π₁) ∘ first (assocˡ {X} {Y} {Z})
  π₁₁-assocˡ =
    begin
      (π₁ ∘ π₁) ∘ assocˡ
    ↓⟨ glue (sym π₁∘assocˡ) π₁∘assocˡ ⟩
      π₁ ∘ (assocˡ ∘ π₁)
    ↑⟨ ∘-resp-≡ʳ π₁∘⁂ ⟩
      π₁ ∘ (π₁ ∘ first assocˡ)
    ↑⟨ assoc ⟩
      (π₁ ∘ π₁) ∘ first assocˡ
    ∎
    where
    open HomReasoning {_} {_}
    open Equiv
    open GlueSquares C

  .π₁∘shave4ˡʳ : ∀ {A B C D} → π₁ ∘ shave4ˡʳ {A} {B} {C} {D} ≡ (π₂ ∘ π₁) ∘ π₁
  π₁∘shave4ˡʳ = commute₁

  .π₂∘shave4ˡʳ : ∀ {A B C D} → π₂ ∘ shave4ˡʳ {A} {B} {C} {D} ≡ π₂ ∘ π₁
  π₂∘shave4ˡʳ = commute₂

  .shave3ˡ∘π₁ : ∀ {A B C D} → shave3ˡ ∘ π₁ ≡ shave4ˡʳ {A} {B} {C} {D}
  shave3ˡ∘π₁ = ⟨⟩∘

  .π₁∘shave4ˡ : ∀ {A B C D} → π₁ ∘ shave4ˡ ≡ shave4ˡʳ {A} {B} {C} {D}
  π₁∘shave4ˡ = commute₁

  .π₂∘shave4ˡ : ∀ {A B C D} → π₂ ∘ shave4ˡ {A} {B} {C} {D} ≡ π₂
  π₂∘shave4ˡ = commute₂

  private
    infix 3 ⟨_⟩,⟨_⟩
    .⟨_⟩,⟨_⟩ : ∀ {A B C} → {f f′ : A ⇒ B} {g g′ : A ⇒ C} → f ≡ f′ → g ≡ g′ → ⟨ f , g ⟩ ≡ ⟨ f′ , g′ ⟩
    ⟨_⟩,⟨_⟩ x y = ⟨⟩-cong₂ x y

  .shave3ˡ∘assocˡ : ∀ {X Y Z W} → shave3ˡ ∘ assocˡ ≡ assocˡ ∘ shave4ˡ {X} {Y} {Z} {W}
  shave3ˡ∘assocˡ =
    begin
      shave3ˡ ∘ assocˡ
    ↓⟨ ⟨⟩∘ ⟩
      ⟨ (π₂ ∘ π₁) ∘ assocˡ , π₂ ∘ assocˡ ⟩
    ↓⟨ ⟨ π₂₁-assocˡ ⟩,⟨ π₂∘assocˡ ⟩ ⟩
      ⟨ (π₂ ∘ π₁) ∘ π₁ , shave3ˡ ⟩
    ↑⟨ ⟨ π₁∘shave4ˡʳ ⟩,⟨ ⟨⟩-congˡ π₂∘shave4ˡʳ ⟩ ⟩
      ⟨ π₁ ∘ shave4ˡʳ , ⟨ π₂ ∘ shave4ˡʳ , π₂ ⟩ ⟩
    ↑⟨ ⟨ ∘-resp-≡ʳ π₁∘shave4ˡ ⟩,⟨ ⟨ ∘-resp-≡ʳ π₁∘shave4ˡ ⟩,⟨ π₂∘shave4ˡ ⟩ ⟩ ⟩
      ⟨ π₁ ∘ (π₁ ∘ shave4ˡ) , ⟨ π₂ ∘ (π₁ ∘ shave4ˡ) , π₂ ∘ shave4ˡ ⟩ ⟩
    ↑⟨ ⟨ assoc ⟩,⟨ ⟨⟩-congˡ assoc ⟩ ⟩
      ⟨ (π₁ ∘ π₁) ∘ shave4ˡ , ⟨ (π₂ ∘ π₁) ∘ shave4ˡ , π₂ ∘ shave4ˡ ⟩ ⟩
    ↑⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
      ⟨ (π₁ ∘ π₁) ∘ shave4ˡ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ shave4ˡ ⟩
    ↑⟨ ⟨⟩∘ ⟩
      assocˡ ∘ shave4ˡ
    ∎
    where
    open HomReasoning
    open Equiv

  .shave3ˡ∘first-assocˡ : ∀ {X Y Z W} → shave3ˡ ∘ first assocˡ ≡ shave4ˡ {X} {Y} {Z} {W}
  shave3ˡ∘first-assocˡ =
    begin
      shave3ˡ ∘ first assocˡ
    ↓⟨ ⟨⟩∘ ⟩
      ⟨ (π₂ ∘ π₁) ∘ first assocˡ , π₂ ∘ first assocˡ ⟩
    ↓⟨ ⟨ glue◃◽ π₂∘assocˡ π₁∘⁂ ⟩,⟨ π₂∘⁂ ⟩ ⟩
      ⟨ shave3ˡ ∘ π₁ , id ∘ π₂ ⟩
    ↓⟨ ⟨ shave3ˡ∘π₁ ⟩,⟨ identityˡ ⟩ ⟩
      shave4ˡ
    ∎
    where
    open HomReasoning
    open Equiv
    open GlueSquares C

  .pentagon : ∀ {X Y Z W} → assocˡ {X} {Y} ∘ assocˡ ≡ second (assocˡ {Y} {Z} {W}) ∘ (assocˡ ∘ first (assocˡ {X}))
  pentagon =
    begin
      assocˡ ∘ assocˡ
    ↓⟨ ⟨⟩∘ ⟩
      ⟨ (π₁ ∘ π₁) ∘ assocˡ , shave3ˡ ∘ assocˡ ⟩
    ↓⟨ ⟨⟩-congʳ shave3ˡ∘assocˡ ⟩
      ⟨ (π₁ ∘ π₁) ∘ assocˡ , assocˡ ∘ shave4ˡ ⟩
    ↑⟨ ⟨ sym π₁₁-assocˡ ⟩,⟨ ∘-resp-≡ʳ shave3ˡ∘first-assocˡ ⟩ ⟩
      ⟨ (π₁ ∘ π₁) ∘ first assocˡ , assocˡ ∘ (shave3ˡ ∘ first assocˡ) ⟩
    ↑⟨ ⟨ ∘-resp-≡ˡ identityˡ ⟩,⟨ assoc ⟩ ⟩
      ⟨ (id ∘ (π₁ ∘ π₁)) ∘ first assocˡ , (assocˡ ∘ shave3ˡ) ∘ first assocˡ ⟩
    ↑⟨ ⟨⟩∘ ⟩
      ⟨ id ∘ (π₁ ∘ π₁) , assocˡ ∘ shave3ˡ ⟩ ∘ first assocˡ
    ↑⟨ ∘-resp-≡ˡ ⁂∘⟨⟩ ⟩
      (second assocˡ ∘ assocˡ) ∘ first assocˡ
    ↓⟨ assoc ⟩
      second assocˡ ∘ (assocˡ ∘ first assocˡ)
    ∎
    where
    open HomReasoning
    open Equiv

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Data.Vec.Membership.Propositional.Disjoint where
open import Data.Vec
open import Data.Vec.Membership.Propositional
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Function using (flip)

Disjoint : ∀ {a} {A : Set a} {n m} → Vec A n → Vec A m → Set a
Disjoint xs ys = ∀ {x} → x ∈ xs → x ∈ ys → ⊥

disjoint-sim : ∀ {a} {A : Set a} {n m} {xs : Vec A n}{ys :  Vec A m} → Disjoint xs ys → Disjoint ys xs
disjoint-sim dis = flip dis

disjoint-[]ˡ : ∀ {a} {A : Set a} {n} {xs : Vec A n} → Disjoint [] xs
disjoint-[]ˡ ()

disjoint-[]ʳ : ∀ {a} {A : Set a} {n} {xs : Vec A n} → Disjoint xs []
disjoint-[]ʳ = disjoint-sim disjoint-[]ˡ

disjointness :  ∀ {a} {A : Set a} {n m} {xs : Vec A n}{ys :  Vec A m} → Disjoint xs ys →
             ∀ {x y} → x ∈ xs → y ∈ ys → x ≢ y
disjointness dis x∈xs y∈ys x≡y rewrite x≡y = dis x∈xs y∈ys

max_stars_repo_name: tizmd/agda-distinct-disjoint

max_issues_repo_name: tizmd/agda-distinct-disjoint

max_forks_repo_name: tizmd/agda-distinct-disjoint


text:
module Formalization.SimplyTypedLambdaCalculus where

import      Lvl
open import Numeral.Natural
open import Type as _ using (TYPE)

data Type (B : TYPE) : TYPE₁ where
  Base : B → Type(B)
  Function : Type(B) → Type(B) → Type(B)

data Term (B : TYPE) : TYPE₁ where
  Apply : Term(B) → Term(B) → Term(B)
  Abstract : Type(B) → Term(B) → Term(B)
  Var : ℕ → Term(B)
  Const : B → Term(B)

module _ {B} where
  data _⊢_::_ (Γ : Term(B) → Type(B) → TYPE) : Term(B) → Type(B) → TYPE₁ where
    intro : ∀{a}{T} → Γ(a)(T) → (Γ ⊢ a :: T)
    -- const : ∀{a}{T} → Γ(a)(T) → (Γ ⊢ a :: T)
    abstr : ∀{body}{A B} → (Γ ⊢ body :: B) → (Γ ⊢ Abstract A body :: Function A B)
    apply : ∀{f x}{A B} → (Γ ⊢ f :: Function A B) → (Γ ⊢ x :: A) → (Γ ⊢ Apply f x :: B)

{-
A,B ::= Base | A ⟶ B
t ::= k | t t | λ t | Const b
b = true | false

Γ ⊢ Const b : Base
v ::= Const b | λ t
(⊢ t : Base) → ∃ v t ⟶* v
(⊢ t : A) → ∃ v t ⟶* v

Red(A)(t) definition "to be reducible"
Red(Base)(t) = ∃v(t ⟶* v)
Red(A→B)(t) = ∀u. Red(A)(u) → Red(B)(t u)

(t ⟶ t') → Red(A)(t') → Red(A)(t)
  • A = Base:
    ∃v(t* ⟶* v) → ∃v(t ⟶* v)
    t → t' ⟶* v
  • A = B→C:
    ∀u. Red(B)(u) → Red(C)(t' u)
    to show ∀u. Red(B)(u) → Red(C)(t u)
    and just use induction on the first thing mentioned
    Red(C)(t' u)
    to get
    Red(C)(t u)

data ⟶β : Set where
  red1 : t ⟶β u
  red2 : (λ t) u ⟶β substitute t u
  red3 : (t ⟶β t') → ((t u) ⟶β (t' u))
  red4 : (u ⟶β u') → (t u ⟶β t u')

⟶β-confluent : Confluent (_⟶β_)

module CallByName where
  data ⟶β : Set where
    red2 : (λ t) u ⟶β substitute t u
    red3 : (t ⟶β t') → ((t u) ⟶β (t' u))

substitute-preservation : (Γ ⊢ ((λ u) u' : A)) → (Γ ⊢ (substitute u u' : A))
β⟶-preservation : (Γ ⊢ (t : A)) → (t ⟶β t') → (Γ ⊢ (t' : A))

Red(Γ)(σ)
Γ = () | Γ.A -- context
σ : ℕ → Term
∀k. Γ ⊢ k : A
Represent variable as a context
σ is a formal definition of "reducible" substitution
Example:
Γ.A ⊢ 0 : A
Γ.A.B ⊢ 1 : A

σ-substitution?:

Red(Γ)(σ) ∧ (Γ ⊢ t:A) → Red(A)(t σ)
  Proof by induction on t
  • t = Ref k
    Red(A)(k σ) = Red(A)(σ(k))
  • t = t₀ t₁
    t_σ = (t₀ σ) (t₁ σ)
    Γ ⊢ t₀ : B → A
    Γ ⊢ t₁ : B
    by induction hypothesis:
    Red(B→A)(t₀ σ)
    Red(B)(t₁ σ)
    so Red(A)(t₀ σ)(t₁ σ)
  • t = λ u
    A = B → C
    Γ.B ⊢ u : C
    To show: Red(B→C)((λ u) σ)
    it means: ∀ u',Red(B)(u'), show Red(C)((λv) σ u')
    Define:
      (_,_) : (σ : ℕ → Term) (u' : Term) : ℕ → Term
      (σ,u')(0) = u'
      (σ,u')(𝐒 n) = σ(n)
    Claim: (λu) σ u' ⟶ u(σ,u')
    Γ.B ⊢ (k : T) → Red(T)((σ,u') k)
      k=0: Γ.B ⊢ 0
      k=n+1 (Γ ⊢ u : T) → (Γ ,B ⊢ n+1 : T)
    Summary:
      This is all to prove ∃v(t ⟶* v) if ⊢ t : Base, which is Red(A)(t)?
      Direct proof for application.
      Generalize the statement to: (⊢ t : A) → Red(A)(t)
      and then to: (Γ ⊢ t:A) → Red(Γ)(σ) → Red(A)(t σ)

  Something else: Krivine abstract machine
  How to evaluate λ-terms without substitution (defined before LISP eval with substitution)
  Term: k | tt | λ t
  Closure: t, ρ -- note: first mention of closure in this field? (denoted u v,‥)
  Environment: list of closures
  Stack: list of closures in stack order (denoted S)
  3 components: Term t,ENv ρ, Stack S → Term Env STack
  t₁ | ρ₁ | S₁ | t₂ | ρ₂ | S₂
  λ t | ρ | u : S | t | (ρ,u) | S
  t₀t1 | ρ | S | t₀ | ρ | (t₁,ρ) : S
  0 | ρ,(t,ρ') | S | t | ρ' | S
  k+1 | ρ,(t,p') | S | k | ρ | S
  Those are the transformations/reductions of the machine.
  Simplified description of how functional programs are evaluated.

-}

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

open import Common.Prelude
open import Common.Equality

primitive primForce : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x

force = primForce

not-stuck : (b : Bool) → force b not ≡ not b
not-stuck true = refl
not-stuck false = refl

stuck : (b : Bool) → force b not ≡ not b
stuck b = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT

{- Useful lemmas for computing the effect of transporting a function
 - across an equivalence in the domain or codomain.
 - TODO move these lemmas into lib.types.Pi or lib.types.PointedPi -}

-- XXX Naming convensions?

module stash.homotopy.FunctionOver where

{- transporting a ptd function along a equivalence or path in the domain -}
module _ {i} {j} {Y : Ptd i} {Z : Ptd j} (g : Y ⊙→ Z) where

  domain-over-⊙path : {X : Ptd i} (p : de⊙ X == de⊙ Y)
    (q : coe p (pt X) == pt Y)
    → g ⊙∘ (coe p , q) == g [ (λ W → W ⊙→ Z) ↓ ptd= p (↓-idf-in p q) ]
  domain-over-⊙path idp idp = idp

  domain-over-⊙equiv : {X : Ptd i} (e : X ⊙≃ Y)
    → g ⊙∘ ⊙–> e == g [ (λ W → W ⊙→ Z) ↓ ⊙ua e ]
  domain-over-⊙equiv {X = X} e =
    ap (λ w → g ⊙∘ w) (! $ ⊙λ= (coe-β (⊙≃-to-≃ e)) (↓-idf=cst-in idp))
    ◃ domain-over-⊙path (ua (⊙≃-to-≃ e))
                        (coe-β (⊙≃-to-≃ e) (pt X) ∙ snd (⊙–> e))

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

  domain!-over-⊙path : {Y : Ptd i} (p : de⊙ X == de⊙ Y)
    (q : coe p (pt X) == pt Y)
    → f == f ⊙∘ (coe! p , ap (coe! p) (! q) ∙ coe!-inv-l p (pt X))
      [ (λ W → W ⊙→ Z) ↓ ptd= p (↓-idf-in p q) ]
  domain!-over-⊙path idp idp = idp

  domain!-over-⊙equiv : {Y : Ptd i} (e : X ⊙≃ Y)
    → f == f ⊙∘ (⊙<– e) [ (λ W → W ⊙→ Z) ↓ ⊙ua e ]
  domain!-over-⊙equiv {Y = Y} e =
    (! (ap (λ w → f ⊙∘ w) (⊙<–-inv-l e)) ∙ ! (⊙∘-assoc f _ (⊙–> e)))
    ◃ domain-over-⊙equiv (f ⊙∘ (⊙<– e)) e

{- transporting a ptd function along a equivalence or path in the codomain -}
module _ {i} {j} {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y) where

  codomain-over-⊙path : {Z : Ptd j} (p : de⊙ Y == de⊙ Z)
    (q : coe p (pt Y) == pt Z)
    → f == (coe p , q) ⊙∘ f [ (λ W → X ⊙→ W) ↓ ptd= p (↓-idf-in p q) ]
  codomain-over-⊙path idp idp = pair= idp (! (∙-unit-r _ ∙ ap-idf (snd f)))

  codomain-over-⊙equiv : {Z : Ptd j} (e : Y ⊙≃ Z)
    → f == (⊙–> e) ⊙∘ f [ (λ W → X ⊙→ W) ↓ ⊙ua e ]
  codomain-over-⊙equiv {Z = Z} e =
    codomain-over-⊙path (ua (⊙≃-to-≃ e))
      (coe-β (⊙≃-to-≃ e) (pt Y) ∙ snd (⊙–> e))
    ▹ ap (λ w → w ⊙∘ f) (⊙λ= (coe-β (⊙≃-to-≃ e)) (↓-idf=cst-in idp))

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

  codomain!-over-⊙path : {Y : Ptd j} (p : de⊙ Y == de⊙ Z)
    (q : coe p (pt Y) == pt Z)
    → (coe! p , ap (coe! p) (! q) ∙ coe!-inv-l p (pt Y)) ⊙∘ g == g
      [ (λ W → X ⊙→ W) ↓ ptd= p (↓-idf-in p q) ]
  codomain!-over-⊙path idp idp = pair= idp (∙-unit-r _ ∙ ap-idf (snd g))

  codomain!-over-⊙equiv : {Y : Ptd j} (e : Y ⊙≃ Z)
    → (⊙<– e) ⊙∘ g == g [ (λ W → X ⊙→ W) ↓ ⊙ua e ]
  codomain!-over-⊙equiv {Y = Y} e =
    codomain-over-⊙equiv (⊙<– e ⊙∘ g) e
    ▹ ! (⊙∘-assoc (⊙–> e) _ g) ∙ ap (λ w → w ⊙∘ g) (⊙<–-inv-r e) ∙ ⊙∘-unit-l g

{- transporting a group homomorphism along an isomorphism -}

domain-over-iso : ∀ {i j} {G H : Group i} {K : Group j}
  {φ : G →ᴳ H} {ie : is-equiv (GroupHom.f φ)} {ψ : G →ᴳ K} {χ : H →ᴳ K}
  → GroupHom.f ψ == GroupHom.f χ
    [ (λ A → A → Group.El K) ↓ ua (GroupHom.f φ , ie) ]
  → ψ == χ [ (λ J → J →ᴳ K) ↓ uaᴳ (φ , ie) ]
domain-over-iso {K = K} {φ = φ} {ie} {ψ} {χ} p =
  group-hom=-↓ $ ↓-ap-out _ Group.El _ $
    transport
      (λ q → GroupHom.f ψ == GroupHom.f χ [ (λ A → A → Group.El K) ↓ q ])
      (! (El=-β (φ , ie)))
      p

codomain-over-iso : ∀ {i j} {G : Group i} {H K : Group j}
  {φ : H →ᴳ K} {ie : is-equiv (GroupHom.f φ)} {ψ : G →ᴳ H} {χ : G →ᴳ K}
  → GroupHom.f ψ == GroupHom.f χ
    [ (λ A → Group.El G → A) ↓ ua (GroupHom.f φ , ie) ]
  → ψ == χ [ (λ J → G →ᴳ J) ↓ uaᴳ (φ , ie) ]
codomain-over-iso {G = G} {φ = φ} {ie} {ψ} {χ} p =
  group-hom=-↓ $ ↓-ap-out _ Group.El _ $
    transport
      (λ q → GroupHom.f ψ == GroupHom.f χ [ (λ A → Group.El G → A) ↓ q ])
      (! (El=-β (φ , ie)))
      p

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- Example by Simon Huber

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

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

ap : {A B : Set} (f : A → B) {a b : A} (p : a ≡ b) → f a ≡ f b
ap f refl = refl

-- \bub
_•_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
p • refl = p

infixr 30 _•_

! : {A : Set} {a b : A} → a ≡ b → b ≡ a
! refl = refl

-- \.  (NB: not • aka \bub)
_∙_ : {A : Set} {B : A → Set}
      {f g : (a : A) → B a} →
      f ≡ g →
      (x : A) → f x ≡ g x
refl ∙ x = refl

infix 30 _∙_

dotap : {A B : Set} {f g : A → B}
        (p : f ≡ g) (x : A)
      → p  ∙ x ≡ ap (λ F → F x) p
dotap refl x = refl

apcomp : {A B C : Set} (f : B → C) (g : A → B)
         {x y : A} (p : x ≡ y)
       → ap (λ a → f (g a)) p ≡ ap f (ap g p)
apcomp f g refl = refl

-- combinators for equality reasoning
_≡⟨_⟩_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ p ⟩ q = p • q

infixr 2 _≡⟨_⟩_

_□ : {A : Set} (x : A) → x ≡ x
x □ = refl

module Wrong (A B : Set) (a0 : A) where
  const : B → (A → B)
  const = λ x _ → x

  to : {x y : B} → x ≡ y → const x ≡ const y
  to = ap const

  from : {x y : B} → const x ≡ const y → x ≡ y
  from = ap (λ F → F a0)

  -- This lemma should not typecheck:
  lem : {x y : B} (p : const x ≡ const y) (a : A)
      → p ∙ a ≡ to (from p) ∙ a
  lem p a = p ∙ a
            ≡⟨ dotap p a ⟩
            ap (λ F → F a) p
            ≡⟨ refl ⟩
            ap (λ F → const (F a) a) p
            ≡⟨ apcomp _ _ p ⟩
            ap (λ G → G a) (ap (λ F → const (F a)) p)
            ≡⟨ ap (ap (λ G → G a)) (apcomp const (λ F → F a) p) ⟩
            ap(λ G → G a) (ap const (ap (λ (F : A → B) → F a) p))
            ≡⟨ ! (dotap (ap const (ap (λ F → F a) p)) a) ⟩
            (to (from p) ∙ a) □


text:
-- Andreas, 2016-01-22
-- special size checking j : Size< i |- j : Size< ↑ j
-- was missing from checkInternal

-- {-# OPTIONS -v tc.polarity:10 #-}
-- {-# OPTIONS -v tc.with.type:50 #-}
-- {-# OPTIONS -v tc.check.internal:30 -v tc.infer.internal:30 #-}

open import Common.Unit
open import Common.Size

postulate
  axiom : Unit
  anything : ∀{A : Set} → A

-- An inductive-coinductive unit type.

mutual

  record IC i : Set where
    coinductive
    field force : ∀(j : Size< i) → IC' j

  data IC' i : Set where
    cons : (xs : IC i) → IC' i -- necessary

-- The recursive identity on IC.

mutual

  idIC  : ∀ i (p : IC i) → IC  i
  IC.force (idIC i p) j = idIC' (↑ j) j (IC.force p j)
    -- (↑ j) is triggering the error
    -- if we write i here, things work

  idIC' : ∀ i (j : Size< i) (p : IC' j) → IC' j
  idIC' i j (cons p) = cons (idIC j p)

-- An inhabitant defined using with.

-- some : ∀ i  → IC i
-- IC.force (some i) j with axiom   -- with is necessary here!
-- ... | unit  = cons (some j)

some  : ∀ i  → IC i
some' : ∀ i (j : Size< i) (u : Unit) → IC' j

IC.force (some i) j = some' i j axiom
some' i j unit  = cons (some j)

-- A coindutive predicate with non-linear use of size i.

mutual

  -- use of i in IC i is necessary, works with IC ∞
  record All i (s : IC i) : Set where
    coinductive
    field force : ∀(j : Size< i) → All' j (IC.force s j)

  data All' i : (s : IC' i) → Set where

-- With abstracted type is well-formed.
-- This means the type-checker can deal with it.

Test : Set₄
Test = (w : Set₃) (i : Size) (j : Size< i) →
       All' j (idIC' (↑ j) j (some' i j axiom))

-- Agda claims: With abstracted type is ill-formed.
-- This means that checkInternal cannot deal with it.

test : ∀ i → All i (idIC i (some i))
All.force (test i) j with Set₂  -- any with expression does it here
... | w = anything

-- i !=< ↑ j of type Size
-- when checking that the type
-- (w : Set₃) (i : Size) (j : Size< i) →
-- All' j (idIC' (↑ j) j (some' i j axiom))
-- of the generated with function is well-formed

{-
candidate type:
  (w : Set₃) (i : Size) (j : Size< i) →
  All' j (idIC' (↑ j) j (some' i j axiom))
candidate type:
  El {_getSort = Type (Max [ClosedLevel 4]), unEl =
  Pi []r(El {_getSort = Type (Max [ClosedLevel 4]), unEl =
    Sort (Type (Max [ClosedLevel 3]))}) (Abs "w"
  El {_getSort = Type (Max []), unEl =
  Pi []r(El {_getSort = SizeUniv, unEl =
    Def Common.Size.Size []}) (Abs "i"
  El {_getSort = Type (Max []), unEl =
  Pi []r(El {_getSort = SizeUniv, unEl =
    Def Common.Size.Size<_ [Apply []?(Var 0 [])]}) (Abs "j"
  El {_getSort = Type (Max []), unEl =
  Def Issue1795.All' [Apply []r(Var 0 []),Apply []r(
    Def Issue1795.idIC' [Apply []r(Def Common.Size.↑_ [Apply []r(Var 0 [])]),Apply []r(Var 0 []),Apply []r(
      Def Issue1795.some' [Apply []r(Var 1 []),Apply []r(Var 0 []),Apply []r(
        Def Issue1795.axiom [])])])]})})})}

Last words:
type t =  (j : Size< (↑ j)) → IC' j → IC' j
self =  idIC' (↑ j)
eliminated by e =  $ j
checking internal  j  :  Size< (↑ j)
checking spine  ( j  :  Size< i ) []  :  Size< (↑ j)
-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

-- There are really all 'private' sub-pieces of
-- Categories.Category.Monoidal.Closed.IsClosed, but that is taking
-- forever to typecheck, so the idea is to split things into pieces and
-- hope that that will help.

open import Categories.Category using (Category)
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Closed using (Closed)

module Categories.Category.Monoidal.Closed.IsClosed.Identity
  {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (Cl : Closed M) where

open import Function using (_$_) renaming (_∘_ to _∙_)

open import Categories.Category.Monoidal.Utilities M
open import Categories.Morphism C using (Iso)
open import Categories.Morphism.Properties C using (Iso-resp-≈)
open import Categories.Morphism.Reasoning C using (pullʳ; pullˡ; pushˡ; cancelʳ)
open import Categories.Functor using (Functor) renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Bifunctor.Properties
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Dinatural
  using (Extranaturalʳ; extranaturalʳ; DinaturalTransformation)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism)
import Categories.Category.Closed as Cls

open Closed Cl
open Category C       -- most of it is used

open HomReasoning
open adjoint renaming (unit to η; counit to ε; Ladjunct to 𝕃)

private
  λ⇒ = unitorˡ.from
  λ⇐ = unitorˡ.to
  ρ⇒ = unitorʳ.from
  ρ⇐ = unitorʳ.to

identity : NaturalIsomorphism idF [ unit ,-]
identity = record
  { F⇒G = F∘id⇒F ∘ᵥ ([ unit ,-] ∘ˡ (unitorʳ-natural.F⇒G)) ∘ᵥ η
  ; F⇐G = ε ∘ᵥ (unitorʳ-natural.F⇐G ∘ʳ [ unit ,-]) ∘ᵥ F⇒id∘F
  ; iso = λ X → Iso-resp-≈ (iso X) (⟺ identityˡ) (⟺ (∘-resp-≈ʳ identityʳ))
  }
  where
  open Functor
  iso : ∀ X → Iso (𝕃 unitorʳ.from) (ε.η X ∘ unitorʳ.to)
  iso X = record
    { isoˡ = begin
      (ε.η X ∘ ρ⇐) ∘ 𝕃 ρ⇒      ≈⟨ pullʳ unitorʳ-commute-to ⟩
      ε.η X ∘ 𝕃 ρ⇒ ⊗₁ id ∘ ρ⇐  ≈˘⟨ assoc ⟩
      Radjunct (𝕃 ρ⇒) ∘ ρ⇐     ≈⟨ RLadjunct≈id ⟩∘⟨refl ⟩
      ρ⇒ ∘ ρ⇐                  ≈⟨ unitorʳ.isoʳ ⟩
      id                       ∎
    ; isoʳ = begin
      𝕃 ρ⇒ ∘ ε.η X ∘ ρ⇐                      ≈⟨ pullʳ (η.commute _) ⟩
      [ id , ρ⇒ ]₁ ∘ 𝕃 ((ε.η X ∘ ρ⇐) ⊗₁ id) ≈˘⟨ pushˡ (homomorphism [ unit ,-]) ⟩
      𝕃 (ρ⇒ ∘ (ε.η X ∘ ρ⇐) ⊗₁ id)           ≈⟨ F-resp-≈ [ unit ,-] unitorʳ-commute-from ⟩∘⟨refl ⟩
      𝕃 ((ε.η X ∘ ρ⇐) ∘ ρ⇒)                 ≈⟨ F-resp-≈ [ unit ,-] (cancelʳ unitorʳ.isoˡ) ⟩∘⟨refl ⟩
      𝕃 (ε.η X)                              ≈⟨ zag ⟩
      id                                     ∎
    }

module identity = NaturalIsomorphism identity

diagonal : Extranaturalʳ unit [-,-]
diagonal = extranaturalʳ (λ X → 𝕃 λ⇒)
  $ λ {X Y f} → begin
    [ id , f ]₁ ∘ 𝕃 λ⇒                             ≈˘⟨ pushˡ (homomorphism [ X ,-]) ⟩
    [ id , f ∘ λ⇒ ]₁ ∘ η.η unit                    ≈˘⟨ F-resp-≈ [ X ,-] unitorˡ-commute-from ⟩∘⟨refl ⟩
    [ id , λ⇒ ∘ id ⊗₁ f ]₁ ∘ η.η unit              ≈⟨ homomorphism [ X ,-] ⟩∘⟨refl ⟩
    ([ id , λ⇒ ]₁ ∘ [ id , id ⊗₁ f ]₁) ∘ η.η unit  ≈⟨ pullʳ (mate.commute₁ f) ⟩
    [ id , λ⇒ ]₁ ∘ [ f , id ]₁ ∘ η.η unit          ≈⟨ pullˡ [ [-,-] ]-commute ⟩
    ([ f , id ]₁ ∘ [ id , λ⇒ ]₁) ∘ η.η unit        ≈⟨ assoc ⟩
    [ f , id ]₁ ∘ 𝕃 λ⇒                             ∎
  where open Functor

module diagonal = DinaturalTransformation diagonal

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


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

module H where

open import Data.Product using (_×_; _,_)
import Relation.Binary.Core as C
import Relation.Binary.PropositionalEquality as P
open P.≡-Reasoning

------------------------------------------------------------------------------
-- Some abbreviations and lemmas about paths

infix  4  _≡_

_≡_ : ∀ {ℓ} {A : Set ℓ} → (x y : A) → Set ℓ
_≡_ {ℓ} {A} x y = C._≡_ {ℓ} {A} x y

refl : ∀ {ℓ} {A} → (x : A) → x ≡ x
refl {ℓ} {A} x = C.refl {ℓ} {A} {x}

infixr 8 _•_

_•_ : ∀ {ℓ} {A : Set ℓ} {x y z : A} →
      (x ≡ y) → (y ≡ z) → (x ≡ z)
_•_ = P.trans

unitTransR : ∀ {ℓ} {A : Set ℓ} {x y : A} → (p : x ≡ y) → (p ≡ p • refl y)
unitTransR {x = x} C.refl = refl (refl x)

unitTransL : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ refl x • p)
unitTransL {x = x} C.refl = refl (refl x)

-- ap, transport, apd at level 1

ap : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} →
     (f : A → B) → {x y : A} → (x ≡ y) → (f x ≡ f y)
ap = P.cong

transport : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} (B : A → Set ℓ₂) →
            {x y : A} → (x ≡ y) → B x → B y
transport = P.subst

-- binary version
transport₂ : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Set ℓ₁} {B : Set ℓ₂} (P : A → B → Set ℓ₃) →
            {x₁ x₂ : A} {y₁ y₂ : B} → (x₁ ≡ x₂) → (y₁ ≡ y₂) →
            P x₁ y₁ → P x₂ y₂
transport₂ = P.subst₂

apd : ∀ {ℓ₁ ℓ₂} → {A : Set ℓ₁} {B : A → Set ℓ₂} →
      (f : (x : A) → B x) → {x y : A} → (p : x ≡ y) →
      transport B p (f x) ≡ f y
apd f C.refl = C.refl

-- ap, transport, apd at level 2

ap² : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} →
      (f : A → B) → {x y : A} {p q : x ≡ y} → (r : p ≡ q) →
      (ap f p ≡ ap f q)
ap² f C.refl = C.refl

transport² : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} (P : A → Set ℓ₂) →
      {x y : A} {p q : x ≡ y} → (r : p ≡ q) → (u : P x) →
      (transport P p u ≡ transport P q u)
transport² P {p = C.refl} C.refl u = refl u

apd² : ∀ {ℓ₁ ℓ₂} → {A : Set ℓ₁} {B : A → Set ℓ₂} →
      (f : (x : A) → B x) → {x y : A} {p q : x ≡ y} → (r : p ≡ q) →
      apd f p ≡ (transport² B r (f x)) • (apd f q)
apd² f {p = C.refl} C.refl = C.refl

------------------------------------------------------------------------------
-- Some higher-inductive types from Ch. 6

module S¹ where

  postulate
    S¹ : Set
    base : S¹
    loop : base ≡ base

  record rec (B : Set) (b : B) (p : b ≡ b) : Set₁ where
    field
      f : S¹ → B
      α : f base ≡ b
      β : transport (λ x → x ≡ x) α (ap f loop) ≡ p

  record ind (P : S¹ → Set) (b : P base) (p : transport P loop b ≡ b) : Set₁ where
    field
      f : (x : S¹) → P x
      α : f base ≡ b
      β : transport (λ x → transport P loop x ≡ x) α (apd f loop) ≡ p

------------------------------------------------------------------------------
-- Interval

module I where

  postulate
    I : Set
    𝟘 : I
    𝟙 : I
    seg : 𝟘 ≡ 𝟙

  record rec (B : Set) (b₀ b₁ : B) (s : b₀ ≡ b₁) : Set₁ where
    postulate
      f : I → B
      α₀ : f 𝟘 ≡ b₀
      α₁ : f 𝟙 ≡ b₁
      β : transport₂ (λ x y → x ≡ y) α₀ α₁ (ap f seg) ≡ s

  record ind (P : I → Set) (b₀ : P 𝟘) (b₁ : P 𝟙)
             (s : transport P seg b₀ ≡ b₁) : Set₁ where
    postulate
      f : (x : I) → P x
      α₀ : f 𝟘 ≡ b₀
      α₁ : f 𝟙 ≡ b₁
      β : transport₂ (λ x y → transport P seg x ≡ y) α₀ α₁ (apd f seg) ≡ s

------------------------------------------------------------------------------
-- S²

module S² where

  postulate
    S² : Set
    base : S²
    surf : refl base ≡ refl base

  record rec (B : Set) (b : B) (s : refl b ≡ refl b) : Set₁ where
    postulate
      f : S² → B
      α : f base ≡ b
      β : transport (λ p → refl p ≡ refl p) α (ap² f surf) ≡ s

  record ind (P : S² → Set) (b : P base)
             (s : refl b ≡ transport² P surf b • (refl b)) : Set₁ where
    postulate
      f : (x : S²) → P x
      α : f base ≡ b
      β : transport
            (λ p → refl p ≡ transport² P surf p • refl p) α (apd² f surf)
          ≡ s

------------------------------------------------------------------------------
-- Suspensions

module Susp (A : Set) where

  postulate
    Σ : Set → Set₁
    N : Σ A
    S : Σ A
    merid : A → (N ≡ S)

------------------------------------------------------------------------------
-- Torus

module T² where

  postulate
    T² : Set
    b  : T²
    p  : b ≡ b
    q  : b ≡ b
    t  : p • q ≡ q • p

------------------------------------------------------------------------------
-- Torus (alternative definition)

module T²' where

  open S¹

  T² : Set
  T² = S¹ × S¹

------------------------------------------------------------------------------
-- Torus (second alternative definition)

module T²'' where

  open S¹

  postulate
    T² : Set
    b : T²
    p : b ≡ b
    q : b ≡ b
    h : T²
    f : S¹ → T²
    fb : f base ≡ b
    floop : transport (λ x → x ≡ x) fb (ap f loop) ≡ p • q • P.sym p • P.sym q
    s : (x : S¹) → f x ≡ h

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

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT


text:
module helloworld where
  open import IO
  main = run (putStrLn "Hello, World!")


text:
module FairStream where

open import Level as Level using (zero)
open import Size
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

-- open import Data.List using (List; module List; []; _∷_; _++_; length)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product renaming (map to pmap)

open import Stream

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

mutual
  data LFin (A B : Set) : Set where
    lin : A × LFin A B → LFin A B
    rinl : RFin A B → LFin A B

  data RFin (A B : Set) : Set where
    rin : B × RFin A B → RFin A B
    linr : LFin A B → RFin A B

Fair Fair' : Set → Set → Set

Fair A B = Stream (LFin A B)

Fair' A B = Stream (List⁺ A × List⁺ B)

α : ∀{A B} → Fair A B → Fair' A B
hd (α {A} {B} u) = (f₁ (hd u) , g (hd u))
  where
    f₁ : LFin A B → List⁺ A
    f₂ : RFin A B → List⁺ A

    f₁ (lin (a , x)) = a ∷ f₁ x
    f₁ (rinl x) = f₂ x

    f₂ (rin (b , y)) = f₂ y
    f₂ (linr x) = f₁ x

    g : LFin A B → List⁺ B
    g (lin x) = {![]!}
    g (rinl x) = {!!}
tl (α u) = {!!}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

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

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

open SuspensionRec public using () renaming (f to Susp-rec)

open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas
open import nicolai.pseudotruncations.pointed-O-Sphere

module nicolai.pseudotruncations.LoopsAndSpheres where

{- We greatly benefit from Evan Cavallo's code - thank you! -}
open import homotopy.PtdAdjoint
open import homotopy.SuspAdjointLoop

isNull : ∀ {i j} {A : Type i} {B : Type j} (b : B) (f : A → B) → Type _
isNull {A = A} b f = (a : A) → f a == b

module null {i} {j} {Â : Ptd i} {B̂ : Ptd j} (ĝ : Â →̇ B̂) where

  A = fst Â
  a₀ = snd Â
  B = fst B̂
  b₀ = snd B̂
  g = fst ĝ
  p = snd ĝ

  -- derived isNull
  isNulld = (a : fst Â) → g a == b₀

  -- pointed isNull; we state it in the equivalence form (slightly easier to handle)
  isNull∙' = Σ ((a : A) → g a == b₀) λ pr → pr a₀ == p

  -- the 'real' pointed isNull
  isNull∙ = ĝ == ((λ _ → b₀) , idp)

  {- The two versions are equivalent -}
  isNull-equiv : isNull∙ ≃ isNull∙'
  isNull-equiv =
               ĝ == ((λ _ → b₀) , idp)
                 ≃⟨ (=Σ-eqv _ _) ⁻¹ ⟩
               =Σ ĝ ((λ _ → b₀) , idp)
                 ≃⟨ equiv-Σ' {A₀ = g == λ _ → b₀}
                             app=-equiv
                             (λ h → (p == idp [ (λ f → f a₀ == b₀) ↓ h ])
                                      ≃⟨ to-transp-equiv _ _ ⟩
                                    (transport (λ f → f a₀ == b₀) h p) == idp
                                      ≃⟨ coe-equiv
                                           (ap (λ x → x == idp)
                                               (trans-ap₁ (λ f → f a₀)
                                                          b₀ h p)) ⟩
                                    (! (app= h a₀) ∙ p) == idp
                                      ≃⟨ adhoc-=-eqv (app= h a₀) p ⟩
                                    (app= h a₀ == p)
                                      ≃∎) ⟩
               (Σ ((a : A) → g a == b₀) λ pr → pr a₀ == p)
                 ≃∎

-- Lemma 4.4: pointed and non-pointed 'nullness' are logically equivalent;
-- First, one direction:
  null-lequiv : isNulld → isNull∙'
  null-lequiv isnull = (λ a → isnull a ∙ ! (isnull a₀) ∙ p) , (
                 isnull a₀ ∙ ! (isnull a₀) ∙ p
                   =⟨ ! (∙-assoc (isnull a₀) _ _) ⟩
                 (isnull a₀ ∙ ! (isnull a₀)) ∙ p
                   =⟨ ap (λ t → t ∙ p) (!-inv-r (isnull a₀)) ⟩
                 p
                   ∎)

-- The other direction is very easy; we do it using the non-prime variant:
  null-lequiv-easy : isNull∙ → isNulld
  null-lequiv-easy isn = app= (ap fst isn)

-- uncomment this if you want to wait forever for typechecking...
-- Σ⊣Ω-unitCounit : CounitUnitAdjoint Σ⊣Ω.SuspFunctor Σ⊣Ω.LoopFunctor
Σ⊣Ω-unitCounit = Σ⊣Ω.adj

Σ⊣Ω-homset : ∀ {i} → HomAdjoint {i} {i} Σ⊣Ω.SuspFunctor Σ⊣Ω.LoopFunctor
Σ⊣Ω-homset = counit-unit-to-hom Σ⊣Ω-unitCounit

module hom-adjoint {i} (Â : Ptd i) (B̂ : Ptd i) where

  A = fst Â
  B = fst B̂
  a₀ = snd Â
  b₀ = snd B̂

  Φeq : (⊙Susp Â →̇ B̂) ≃ (Â →̇ ⊙Ω B̂)
  Φeq = HomAdjoint.eq Σ⊣Ω-homset Â B̂

  {- This is Lemma 4.1 -}
  Φ : (⊙Susp Â →̇ B̂) → (Â →̇ ⊙Ω B̂)
  Φ = –> Φeq

  Φ⁻¹ : (Â →̇ ⊙Ω B̂) → (⊙Susp Â →̇ B̂)
  Φ⁻¹ = <– Φeq

  open PtdFunctor
  open Σ⊣Ω
  open CounitUnitAdjoint

  {- Some lemmas which are easy on paper and thus not explicitly
     mentioned in the paper. It still takes some effort to
     formalize them. -}
  module simplify where

    simpl-⊙ap : (⊙ap {X = obj SuspFunctor Â} ((λ _ → b₀) , idp))
                 ==
                ((λ _ → idp) , idp)
    simpl-⊙ap =  →̇-maps-to
                   ⊙ap ((λ _ → b₀) , idp)
                   ((λ _ → idp) , idp)
                   (λ= (λ _ → ap-cst b₀ _))

                   ((app= (λ= (λ _ → ap-cst b₀ _)) _) ∙ idp
                     =⟨ ∙-unit-r _ ⟩
                   app= (λ= (λ _ → ap-cst b₀ _)) _
                     =⟨ app=-β _ _ ⟩
                   ap-cst b₀ (idp {a = snd B̂})
                     =⟨ idp ⟩ --  !
                   idp
                     =⟨ idp ⟩ --  !
                   snd (⊙ap {X = obj SuspFunctor Â} ((λ _ → b₀) , idp))
                     ∎ )

    simpl-comp : ((λ (_ : Ω (⊙Susp Â)) → idp {a = b₀}) , idp)
                   ⊙∘ (⊙η Â)
                  ==
                 (λ _ → idp) , idp
    simpl-comp = pair= idp ((ap-cst idp (snd (⊙η Â))) ∙ᵣ idp)

  open simplify

  {- Lemma 4.2 -}
  Φ-is-pointed-map : Φ ((λ _ → b₀) , idp) == ((λ _ → idp) , idp)
  Φ-is-pointed-map = Φ ((λ _ → b₀) , idp)
                       =⟨ idp ⟩
                     (    arr LoopFunctor ((λ _ → b₀) , idp)
                      ⊙∘ (CounitUnitAdjoint.η adj Â))
                       =⟨ idp ⟩
                     (    (⊙ap {X = obj SuspFunctor Â} ((λ _ → b₀) , idp)
                      ⊙∘ (⊙η Â)))
                       =⟨ ap (λ f → f ⊙∘ (⊙η Â)) simpl-⊙ap ⟩
                     ((λ _ → idp) , idp) ⊙∘ (⊙η Â)
                       =⟨ simpl-comp ⟩
                     (λ _ → idp) , idp
                       ∎

-- fix i
module _ {i} where

  open hom-adjoint

  open HomAdjoint
  open null

  -- Lemma 4.3
  Φ-snd-nat : {Â B̂ Ĉ : Ptd i} (f : ⊙Susp Â →̇ B̂) (g : B̂ →̇ Ĉ)
              → Φ Â Ĉ (g ⊙∘ f) == ⊙ap g ⊙∘ Φ Â B̂ f
  Φ-snd-nat {Â} {B̂} {Ĉ} f g = ! (nat-cod Σ⊣Ω-homset Â {B̂} {Ĉ} g f)

  -- Lemma 4.4 is above (before 4.2).

  -- Lemma 4.5
  isnull-Φ : {Â B̂ : Ptd i} (g : ⊙Susp Â →̇ B̂) → (isNull∙ g) ≃ isNull∙ (Φ Â B̂ g)
  isnull-Φ {Â} {B̂} g =
    isNull∙ g
      ≃⟨ equiv-ap (Φeq Â B̂) _ _ ⟩
    (Φ Â B̂ g) == Φ Â B̂ ((λ _ → snd B̂) , idp)
      ≃⟨ coe-equiv
           {A = (Φ Â B̂ g) == Φ Â B̂ ((λ _ → snd B̂) , idp)}
           {B = (Φ Â B̂ g) == (λ _ → idp) , idp}
           (ap (λ q → (Φ Â B̂ g == q)) (Φ-is-pointed-map _ _ )) ⟩
    (Φ Â B̂ g) == (λ _ → idp) , idp
      ≃∎

  -- combination of 4.3 and 4.5
  combine-isnull-nat : {Â B̂ Ĉ : Ptd i} (f : ⊙Susp Â →̇ B̂) (g : B̂ →̇ Ĉ)
               → (isNull∙ (g ⊙∘ f)) ≃ (isNull∙ (⊙ap g ⊙∘ Φ Â B̂ f)) --
  combine-isnull-nat {Â} {B̂} {Ĉ} f g =
    isNull∙ (g ⊙∘ f)
      ≃⟨ isnull-Φ _ ⟩
    isNull∙ (Φ Â Ĉ (g ⊙∘ f))
      ≃⟨ coe-equiv (ap (λ q → isNull∙ q) (Φ-snd-nat f g)) ⟩
    isNull∙ (⊙ap g ⊙∘ Φ Â B̂ f)
      ≃∎

  combine-isnull-nat' : {Â B̂ Ĉ : Ptd i} (f : Â →̇ ⊙Ω B̂) (g : B̂ →̇ Ĉ)
               → (isNull∙ (g ⊙∘ (Φ⁻¹ Â B̂ f))) ≃ (isNull∙ (⊙ap g ⊙∘ f))
  combine-isnull-nat' {Â} {B̂} {Ĉ} f g =
   isNull∙ (g ⊙∘ (Φ⁻¹ Â B̂ f))
      ≃⟨ combine-isnull-nat (Φ⁻¹ Â B̂ f) g ⟩
    isNull∙ (⊙ap g ⊙∘ (Φ Â B̂ (Φ⁻¹ Â B̂ f)))
      ≃⟨ coe-equiv (ap (λ h → isNull∙ (⊙ap g ⊙∘ h)) (<–-inv-r (Φeq Â B̂) f)) ⟩
    isNull∙ (⊙ap g ⊙∘ f)
      ≃∎

module _ {i} where

  open hom-adjoint

  -- This was tricky (todo: could explain why)
  Φ-iter : (Â B̂ : Ptd i) (n : Nat)
           → ((⊙Susp-iter' n Â) →̇ B̂)
           → (Â →̇ (⊙Ω^ n B̂))
  Φ-iter Â B̂ O f = f
  Φ-iter Â B̂ (S n) f = Φ Â (⊙Ω^ n B̂) (Φ-iter (⊙Susp Â) B̂ n f)

  Φ-iter-equiv : (Â B̂ : Ptd i) (n : Nat) → is-equiv (Φ-iter Â B̂ n)
  Φ-iter-equiv Â B̂ O = snd (ide _)
  Φ-iter-equiv Â B̂ (S n) =
    snd ((Φeq Â (⊙Ω^ n B̂)) ∘e ((Φ-iter (⊙Susp Â) B̂ n) , Φ-iter-equiv (⊙Susp Â) B̂ n) )

module _ {i} where

  open null
  open hom-adjoint

  -- Lemma 4.7 -- generalized, because we need to do it for Susp first before it works for Sphere!
  isNull-Φ-many : (m : Nat)
                  → (Â B̂ Ĉ : Ptd i)
                  → (f : ⊙Susp-iter' m Â →̇ B̂) (g : B̂ →̇ Ĉ)
                  → isNull∙ (g ⊙∘ f)
                    ≃
                    isNull∙ ((ap^ m g) ⊙∘ Φ-iter Â B̂ m f)
  isNull-Φ-many O Â B̂ Ĉ f g = ide _
  isNull-Φ-many (S m) Â B̂ Ĉ f g =
                    isNull∙ (g ⊙∘ f)
                      ≃⟨ isNull-Φ-many m (⊙Susp Â) B̂ Ĉ f g   ⟩
                    isNull∙ ((ap^ m g) ⊙∘ Φ-iter (⊙Susp Â) B̂ m f)
                      ≃⟨ combine-isnull-nat (Φ-iter (⊙Susp Â) B̂ m f) (ap^ m g) ⟩
                    (isNull∙
                      (⊙ap (ap^ m g) ⊙∘
                        Φ Â (⊙Ω^ m B̂)
                          (Φ-iter (⊙Susp Â) B̂ m f)))
                      ≃∎

  -- Lemma 4.7 (special with k = 0)
  module _ {B̂ Ĉ : Ptd i} (m : Nat)
           (f : ⊙Sphere' {i} m →̇ B̂) (g : B̂ →̇ Ĉ) where

    isNull-Φ-Sphere : isNull∙ (g ⊙∘ f)
                      ≃
                      isNull∙ ((ap^ m g) ⊙∘ Φ-iter (⊙Sphere' {i} O) B̂ m f)
    isNull-Φ-Sphere = isNull-Φ-many m _ _ _ f g

  open bool-neutral

  module _ {B̂ Ĉ : Ptd i} (m : Nat)
           (g : B̂ →̇ Ĉ) where

    c₀ = snd (⊙Ω^ m Ĉ)

    {- Lemma 4.8 -}
    null-on-pspaces :
      ((f : (⊙Sphere' {i} m) →̇ B̂) → isNull∙ (g ⊙∘ f))
      ≃
      isNulld (ap^ m g)

    null-on-pspaces = -- {!equiv-Π-l!}

      ((f : (⊙Sphere' {i} m) →̇ B̂) → isNull∙ (g ⊙∘ f))

        ≃⟨ equiv-Π-r (λ f → isNull-Φ-Sphere m f g) ⟩

      ((f : (⊙Sphere' {i} m) →̇ B̂) → isNull∙ ((ap^ m g) ⊙∘ Φ-iter (⊙Sphere' {i} O) B̂ m f))

        ≃⟨ equiv-Π-l
             {A = (⊙Sphere' {i} m) →̇ B̂}
             {B = (⊙Sphere' {i} O) →̇ (⊙Ω^ m B̂)}
             (λ f' → isNull∙ ((ap^ m g) ⊙∘ f'))
             {h = Φ-iter (⊙Sphere' {i} O) B̂ m}
             (Φ-iter-equiv _ _ m)
              ⟩

      ((f' : (⊙Sphere' {i} O) →̇ (⊙Ω^ m B̂)) → isNull∙ ((ap^ m g) ⊙∘ f'))

        ≃⟨ equiv-Π-r {A = ⊙Sphere' {i} O →̇ (⊙Ω^ m B̂)} (λ _ → isNull-equiv _) ⟩

      ((f' : (⊙Sphere' {i} O) →̇ (⊙Ω^ m B̂)) → isNull∙' ((ap^ m g) ⊙∘ f'))

        ≃⟨ ide _ ⟩

      ((f' : (⊙Sphere' {i} O) →̇ (⊙Ω^ m B̂)) → Σ ((x : bool) → fst ((ap^ m g) ⊙∘ f') x == _) λ h → h tt₀ == _)

        ≃⟨ equiv-Π-r {A = ⊙Sphere' {i} O →̇ (⊙Ω^ m B̂)}
                     (λ fp → reduction (λ b → fst (ap^ m g ⊙∘ fp) b == null.b₀ (ap^ m g ⊙∘ fp)) _) ⟩

      ((f' : (⊙Sphere' {i} O) →̇ (⊙Ω^ m B̂)) → fst ((ap^ m g) ⊙∘ f') ff₀ == _)

        ≃⟨ ide _ ⟩

      ((f' : (⊙Sphere' {i} O) →̇ (⊙Ω^ m B̂)) → fst (ap^ m g) (fst f' ff₀) == _)

        ≃⟨ equiv-Π-l {A = (⊙Sphere' {i} O) →̇ (⊙Ω^ m B̂)}
                     {B = fst (⊙Ω^ m B̂)}
                     _
                     (snd (reduction (λ _ → fst (⊙Ω^ m B̂)) _)) ⟩

      ((x : fst (⊙Ω^ m B̂)) → fst (ap^ m g) x == c₀)

        ≃⟨ ide _ ⟩

      isNulld (ap^ m g)
        ≃∎

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Reflection.StrictEquiv

open import Cubical.Structures.Axioms
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring.Base

open Iso

private
  variable
    ℓ : Level

record IsCommRing {R : Type ℓ}
                  (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where

  constructor iscommring

  field
    isRing : IsRing 0r 1r _+_ _·_ -_
    ·-comm : (x y : R) → x · y ≡ y · x

  open IsRing isRing public

record CommRingStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor commringstr

  field
    0r         : A
    1r         : A
    _+_        : A → A → A
    _·_        : A → A → A
    -_         : A → A
    isCommRing : IsCommRing 0r 1r _+_ _·_ -_

  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsCommRing isCommRing public

CommRing : Type (ℓ-suc ℓ)
CommRing = TypeWithStr _ CommRingStr

makeIsCommRing : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
                 (is-setR : isSet R)
                 (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
                 (+-rid : (x : R) → x + 0r ≡ x)
                 (+-rinv : (x : R) → x + (- x) ≡ 0r)
                 (+-comm : (x y : R) → x + y ≡ y + x)
                 (·-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
                 (·-rid : (x : R) → x · 1r ≡ x)
                 (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
                 (·-comm : (x y : R) → x · y ≡ y · x)
               → IsCommRing 0r 1r _+_ _·_ -_
makeIsCommRing {_+_ = _+_} is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm =
  iscommring (makeIsRing is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid
                         (λ x → ·-comm _ _ ∙ ·-rid x) ·-rdist-+
                         (λ x y z → ·-comm _ _ ∙∙ ·-rdist-+ z x y ∙∙ λ i → (·-comm z x i) + (·-comm z y i))) ·-comm

makeCommRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
               (is-setR : isSet R)
               (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
               (+-rid : (x : R) → x + 0r ≡ x)
               (+-rinv : (x : R) → x + (- x) ≡ 0r)
               (+-comm : (x y : R) → x + y ≡ y + x)
               (·-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
               (·-rid : (x : R) → x · 1r ≡ x)
               (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
               (·-comm : (x y : R) → x · y ≡ y · x)
             → CommRing
makeCommRing 0r 1r _+_ _·_ -_ is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm =
  _ , commringstr _ _ _ _ _ (makeIsCommRing is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm)

CommRing→Ring : CommRing {ℓ} → Ring
CommRing→Ring (_ , commringstr _ _ _ _ _ H) = _ , ringstr _ _ _ _ _ (IsCommRing.isRing H)

CommRingEquiv : (R S : CommRing) (e : ⟨ R ⟩ ≃ ⟨ S ⟩) → Type ℓ
CommRingEquiv R S e = RingEquiv (CommRing→Ring R) (CommRing→Ring S) e

CommRingHom : (R S : CommRing) → Type ℓ
CommRingHom R S = RingHom (CommRing→Ring R) (CommRing→Ring S)

module CommRingΣTheory {ℓ} where

  open RingΣTheory

  CommRingAxioms : (R : Type ℓ) (s : RawRingStructure R) → Type ℓ
  CommRingAxioms R (_+_ , 1r , _·_) = RingAxioms R (_+_ , 1r , _·_)
                                      × ((x y : R) → x · y ≡ y · x)
  CommRingStructure : Type ℓ → Type ℓ
  CommRingStructure = AxiomsStructure RawRingStructure CommRingAxioms

  CommRingΣ : Type (ℓ-suc ℓ)
  CommRingΣ = TypeWithStr ℓ CommRingStructure

  CommRingEquivStr : StrEquiv CommRingStructure ℓ
  CommRingEquivStr = AxiomsEquivStr RawRingEquivStr CommRingAxioms

  isPropCommRingAxioms : (R : Type ℓ) (s : RawRingStructure R)
                       → isProp (CommRingAxioms R s)
  isPropCommRingAxioms R (_·_ , 0r , _+_) =
    isPropΣ (isPropRingAxioms R (_·_ , 0r , _+_))
            λ { (_ , x , _) → isPropΠ2 λ _ _ →
                  x .IsMonoid.isSemigroup .IsSemigroup.is-set _ _}

  CommRing→CommRingΣ : CommRing → CommRingΣ
  CommRing→CommRingΣ (_ , commringstr _ _ _ _ _ (iscommring G C)) =
    _ , _ , Ring→RingΣ (_ , ringstr _ _ _ _ _ G) .snd .snd , C

  CommRingΣ→CommRing : CommRingΣ → CommRing
  CommRingΣ→CommRing (_ , _ , G , C) =
    _ , commringstr _ _ _ _ _ (iscommring (RingΣ→Ring (_ , _ , G) .snd .RingStr.isRing) C)

  CommRingIsoCommRingΣ : Iso CommRing CommRingΣ
  CommRingIsoCommRingΣ =
    iso CommRing→CommRingΣ CommRingΣ→CommRing (λ _ → refl) (λ _ → refl)

  commRingUnivalentStr : UnivalentStr CommRingStructure CommRingEquivStr
  commRingUnivalentStr = axiomsUnivalentStr _ isPropCommRingAxioms rawRingUnivalentStr

  CommRingΣPath : (R S : CommRingΣ) → (R ≃[ CommRingEquivStr ] S) ≃ (R ≡ S)
  CommRingΣPath = SIP commRingUnivalentStr

  CommRingEquivΣ : (R S : CommRing) → Type ℓ
  CommRingEquivΣ R S = CommRing→CommRingΣ R ≃[ CommRingEquivStr ] CommRing→CommRingΣ S

  CommRingPath : (R S : CommRing) → (Σ[ e ∈ ⟨ R ⟩ ≃ ⟨ S ⟩ ] CommRingEquiv R S e) ≃ (R ≡ S)
  CommRingPath R S =
    Σ[ e ∈ ⟨ R ⟩ ≃ ⟨ S ⟩ ] CommRingEquiv R S e ≃⟨ strictIsoToEquiv RingIsoΣPath ⟩
    CommRingEquivΣ R S  ≃⟨ CommRingΣPath _ _ ⟩
    CommRing→CommRingΣ R ≡ CommRing→CommRingΣ S
      ≃⟨ isoToEquiv (invIso (congIso CommRingIsoCommRingΣ)) ⟩
    R ≡ S ■

CommRingPath : (R S : CommRing {ℓ}) → (Σ[ e ∈ ⟨ R ⟩ ≃ ⟨ S ⟩ ] CommRingEquiv R S e) ≃ (R ≡ S)
CommRingPath = CommRingΣTheory.CommRingPath

isSetCommRing : ((R , str) : CommRing {ℓ}) → isSet R
isSetCommRing (R , str) = str .CommRingStr.is-set

isPropIsCommRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
             → isProp (IsCommRing 0r 1r _+_ _·_ -_)
isPropIsCommRing 0r 1r _+_ _·_ -_ (iscommring RR RC) (iscommring SR SC) =
  λ i → iscommring (isPropIsRing _ _ _ _ _ RR SR i)
                   (isPropComm RC SC i)
  where
  isSetR : isSet _
  isSetR = RR .IsRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropComm : isProp ((x y : _) → x · y ≡ y · x)
  isPropComm = isPropΠ2 λ _ _ → isSetR _ _

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
postulate
  S : Set
  id : S
  comp : S → S → S

module C where
  _∘_ = comp

postulate
  R : (S → S) → Set
  T : R (C._∘ id) → R (id C.∘_) → Set

t : Set
t = T {!!} {!!}


text:
module Issue124 where

module A where
  data A : Set where
    c : A

module B where
  data B : Set where
    c : B

module C where
  open A public
  open B public

open C

f : B → B
f c = c

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Linear where

open import Data.Product
open import Data.Sum
open import Data.Empty

-- 1. PROPOSITIONAL FRAGMENT

infixr 0 _⊸_
infixr 1 _⊕_ _⅋_
infixr 2 _&_ _⊗_

-- Linear propositions consist of a positive part (affirmation, φ₊) and a negative
-- part (refutation, φ₋). We prove a linear proposition by proving its affirmation.
-- If we have a refutation then we cannot have an affirmation, on pain of contra-
-- diction.
data LProp : Set₁ where
  lprop : (φ₊ : Set) → (φ₋ : Set) → (φ₋ → φ₊ → ⊥) → LProp

-- Linear negation exchanges affirmations and refutations.
~ : LProp → LProp
~ (lprop φ₊ φ₋ p) = lprop φ₋ φ₊ (λ a b → p b a)

-- Additive conjunction
_&_ : LProp → LProp → LProp
(lprop φ₊ φ₋ p) & (lprop ψ₊ ψ₋ q) = lprop (φ₊ × ψ₊) (φ₋ ⊎ ψ₋) pq where
  pq : (φ₋ ⊎ ψ₋) → (φ₊ × ψ₊) → ⊥
  pq (inj₁ ~a) (a , b) = p ~a a
  pq (inj₂ ~b) (a , b) = q ~b b

-- Additive disjunction: notice the symmetry between the proofs `pq` between
-- additive conjunctions and additive disjunctions.
_⊕_ : LProp → LProp → LProp
(lprop φ₊ φ₋ p) ⊕ (lprop ψ₊ ψ₋ q) = lprop (φ₋ ⊎ ψ₋) (φ₊ × ψ₊) pq where
  pq : (φ₊ × ψ₊) → (φ₋ ⊎ ψ₋) → ⊥
  pq (a , b) (inj₁ ~a) = p ~a a
  pq (a , b) (inj₂ ~b) = q ~b b

-- Multiplicative conjunction
_⊗_ : LProp → LProp → LProp
(lprop φ₊ φ₋ p) ⊗ (lprop ψ₊ ψ₋ q) = lprop (φ₊ × ψ₊) ((φ₊ → ψ₋) × (ψ₊ → φ₋)) pq where
  pq : ((φ₊ → ψ₋) × (ψ₊ → φ₋)) → (φ₊ × ψ₊) → ⊥
  pq (f , g) (a , b) = q (f a) b

-- Multiplicative disjunction
_⅋_ : LProp → LProp → LProp
(lprop φ₊ φ₋ p) ⅋ (lprop ψ₊ ψ₋ q) = lprop ((ψ₋ → φ₊) × (φ₋ → ψ₊)) (φ₋ × ψ₋) pq where
  pq : (φ₋ × ψ₋) → ((ψ₋ → φ₊) × (φ₋ → ψ₊)) → ⊥
  pq (~a , ~b) (f , g) = q ~b (g ~a)

-- Linear implication
_⊸_ : LProp → LProp → LProp
p ⊸ q = (~ p) ⅋ q

⟦_⟧ : LProp → Set
⟦ lprop φ₊ _ _ ⟧ = φ₊

_⊢_ : LProp → LProp → Set
Γ ⊢ P = ⟦ Γ ⊸ P ⟧

----------
-- Here we prove that these connectives satisfy Hesselink's axioms and rules
-- for the multiplicative fragment of linear logic. See also:
-- W. H. Hesselink: Axioms and models of linear logic, in Formal Aspects of Computing, 1990)

-- Identity axiom.
axiom-1 : (P : LProp) → ⟦ P ⊸ P ⟧
axiom-1 (lprop φ₊ φ₋ p) =
  (λ x → x) ,
  (λ x → x)

-- Commutativity of ⅋.
axiom-2 : (P Q : LProp) → ⟦ (P ⅋ Q) ⊸ (Q ⅋ P) ⟧
axiom-2 (lprop φ₊ φ₋ p) (lprop ψ₊ ψ₋ q) =
  (λ x → proj₂ x , proj₁ x) ,
  (λ x → proj₂ x , proj₁ x)

-- Associativity of ⅋: the proof looks ugly, but we really just re-associate ×.
axiom-3 : (P Q R : LProp) → ⟦ ((P ⅋ Q) ⅋ R) ⊸ (P ⅋ (Q ⅋ R)) ⟧
axiom-3
  (lprop φ₊ φ₋ p)
  (lprop ψ₊ ψ₋ q)
  (lprop ρ₊ ρ₋ r) =
    (λ x → (proj₁ x , proj₁ (proj₂ x)) , proj₂ (proj₂ x)) ,
    (λ x → (λ y → proj₁ (proj₁ x (proj₂ y)) (proj₁ y)) ,
    (λ y → (λ (z : ρ₋) → proj₂ (proj₁ x z) y) ,
    (λ z → proj₂ x (y , z))))

-- Finally, the analogues of the rules of inferece work as expected.
mp-rule : (P Q : LProp) → ⟦ P ⟧ → ⟦ P ⊸ Q ⟧ → ⟦ Q ⟧
mp-rule
  (lprop φ₊ φ₋ p)
  (lprop ψ₊ ψ₋ q) a ab =
    proj₂ ab a

mp-rule-ctx : (Γ P Q : LProp) → ⟦ Γ ⅋ P ⟧ → ⟦ P ⊸ Q ⟧ → ⟦ Γ ⅋ Q ⟧
mp-rule-ctx
  (lprop γ₊ γ₋ g)
  (lprop φ₊ φ₋ p)
  (lprop ψ₊ ψ₋ q) a ab =
    (λ x → proj₁ a (proj₁ ab x)) ,
    (λ x → proj₂ ab (proj₂ a x))

-- A deduction-like variant of the same result.
deduction : (Γ P Q : LProp) → (Γ ⅋ P) ⊢ Q → Γ ⊢ (P ⊸ Q)
deduction
  (lprop γ₊ γ₋ _)
  (lprop φ₊ φ₋ _)
  (lprop ψ₊ ψ₋ _) gpq =
    (λ pq → helper1 (proj₂ pq)) ,
    (λ g → helper2 ,
    (λ p → helper3 (λ _ → g) (λ _ → p))) where
      helper1 : ψ₋ → γ₋
      helper1 x = proj₁ (proj₁ gpq x)
      helper2 : ψ₋ → φ₋
      helper2 x = proj₂ (proj₁ gpq x)
      helper3 : (φ₋ → γ₊) → (γ₋ → φ₊) → ψ₊
      helper3 x y = proj₂ gpq (x , y)

----------
-- Here we prove the involutive property of negation.

open import Relation.Binary.PropositionalEquality

theorem : (P : LProp) → ~ (~ P) ≡ P
theorem (lprop φ₊ φ₋ x) = refl

-- 2. PROPOSITIONAL-EXPONENTIAL FRAGMENT

-- The "of course!" modality
! : LProp → LProp
! (lprop φ₊ φ₋ _) = lprop φ₊ (φ₊ → ⊥) λ z → z

-- The "why not?" modality
⁇ : LProp → LProp
⁇ (lprop φ₊ φ₋ _) = lprop (φ₋ → ⊥) φ₋ λ x y → y x

----------
-- Here we verify that the H-CLL axioms hold for the modalities.

-- A weakening axiom
axiom-1! : (P Q : LProp) → ⟦ P ⊸ (! Q ⊸ P) ⟧
axiom-1!
  (lprop φ₊ φ₋ p)
  (lprop ψ₊ ψ₋ q) =
    proj₂ ,
    λ y → (λ x _ → p x y) , (λ _ → y)

axiom-2! : (P Q : LProp) → ⟦ ! (P ⊸ Q) ⊸ (! P ⊸ ! Q) ⟧
axiom-2!
  (lprop φ₊ φ₋ p)
  (lprop ψ₊ ψ₋ q) =
    (λ x y → proj₂ x (proj₂ y (proj₁ x))) ,
    (λ x → (λ y z → y (proj₂ x z)) , proj₂ x)

axiom-3! : (P : LProp) → ⟦ ! P ⊸ P ⟧
axiom-3! (lprop φ₊ φ₋ p) = p , (λ x → x)

axiom-4! : (P : LProp) → ⟦ ! P ⊸ ! (! P) ⟧
axiom-4! (lprop φ₊ φ₋ p) = (λ x → x) , (λ x → x)

-- A contraction axiom
axiom-5! : (P Q : LProp) → ⟦ (! P ⊸ (! P ⊸ Q)) ⊸ (! P ⊸ Q) ⟧
axiom-5!
  (lprop φ₊ φ₋ p)
  (lprop ψ₊ ψ₋ q) =
  (λ pq → proj₁ pq , proj₁ pq , proj₂ pq) ,
  (λ x → (λ y z → proj₁ x (z , y) z) ,
  (λ y → proj₂ (proj₂ x y) y))

-- Fortunately, the modal inference rule is trivially verified.

modal-rule : (P : LProp) → ⟦ P ⟧ → ⟦ ! P ⟧
modal-rule (lprop φ₊ φ₋ p) x = x

max_stars_repo_name: guoshimin/linear-constructive

max_issues_repo_name: guoshimin/linear-constructive

max_forks_repo_name: guoshimin/linear-constructive


text:
module Data.Show where

import Prelude
import Data.Nat
import Data.Integer
import Data.String
import Data.List

open Prelude
open Data.Nat
open Data.Integer using (Int; pos; neg)
open Data.String
open Data.List hiding (_++_)

showNat : Nat -> String
showNat zero = "0"
showNat n    = fromList $ reverse $ toList $ show n
  where
    digit : Nat -> String
    digit 0 = "0"
    digit 1 = "1"
    digit 2 = "2"
    digit 3 = "3"
    digit 4 = "4"
    digit 5 = "5"
    digit 6 = "6"
    digit 7 = "7"
    digit 8 = "8"
    digit 9 = "9"
    digit _ = "?"

    show : Nat -> String
    show zero = ""
    show n    = digit (mod n 10) ++ show (div n 10)

showInt : Int -> String
showInt (pos n) = showNat n
showInt (neg n) = "-" ++ showNat (suc n)


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

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

module Number.Postulates where

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 -- Rel
open import Function.Base using (_∋_)

ℕℓ  = ℓ-zero
ℕℓ' = ℓ-zero

postulate
  ℤℓ ℤℓ' : Level
  ℚℓ ℚℓ' : Level
  ℝℓ ℝℓ' : Level
  ℂℓ ℂℓ' : Level

open import Number.Structures
open import Number.Bundles
import Number.Inclusions

import MoreAlgebra

module ℕ* where
  import Cubical.Data.Nat as Nat
  import Cubical.Data.Nat.Order as Order

  open import Agda.Builtin.Nat using () renaming (Nat to ℕ) public

  module Postulates where
    postulate
      min max : ℕ → ℕ → ℕ
      isROrderedCommSemiring : IsROrderedCommSemiring
        (Order._<_)
        (Order._≤_)
        ((MoreAlgebra.Definitions._#'_ {_<_ = Order._<_}))
        (min)
        (max)
        (Nat.zero)
        (1)
        (Nat._+_)
        (Nat._*_)

  module Bundle = ROrderedCommSemiring {ℕℓ} {ℕℓ'}
  Bundle = ROrderedCommSemiring {ℕℓ} {ℕℓ'}

  Carrier = ℕ

  bundle : Bundle
  bundle = (record
    { Carrier = ℕ
    ; _<_ = Order._<_
    ; _≤_ = Order._≤_
    ; _#_ = (MoreAlgebra.Definitions._#'_ { _<_ = Order._<_ })
    ; min = Postulates.min
    ; max = Postulates.max
    ; 0f  = Nat.zero
    ; 1f  = (Nat.suc Nat.zero)
    ; _+_ = Nat._+_
    ; _·_ = Nat._*_
    ; isROrderedCommSemiring = Postulates.isROrderedCommSemiring
    })

  open import Cubical.Data.Nat.Order using (_≤_; _<_) public
  import MoreAlgebra
  open MoreAlgebra.Definitions using (_#'_) public
  open import Agda.Builtin.Nat using () renaming (zero to 0f)  public

  -- _<_ = Bundle._<_ bundle
  -- _≤_ = Bundle._≤_ bundle
  _#_ = Bundle._#_ bundle
  min = Bundle.min bundle
  max = Bundle.max bundle
  -- 0f  = Bundle.0f  bundle
  1f  = Bundle.1f  bundle
  _+_ = Bundle._+_ bundle
  _·_ = Bundle._·_ bundle
  isROrderedCommSemiring = Bundle.isROrderedCommSemiring bundle

  abs : ℕ → ℕ
  abs x = x

  open IsROrderedCommSemiring isROrderedCommSemiring public

module ℕ  = ℕ* hiding (ℕ)
module ℕⁿ = ℕ*
    renaming
    ( Carrier to Carrierⁿ
    ; _<_ to _<ⁿ_
    ; _≤_ to _≤ⁿ_
    ; _#_ to _#ⁿ_
    ; min to minⁿ
    ; max to maxⁿ
    ; 0f  to 0ⁿ
    ; 1f  to 1ⁿ
    ; _+_ to _+ⁿ_
    ; _·_ to _·ⁿ_
    ; isROrderedCommSemiring to isROrderedCommSemiringⁿ
    ; abs to absⁿ
    )

module ℤ* where
  module Postulates where
    postulate
      ℤ           : Type ℤℓ
      _<_ _≤_ _#_ : Rel ℤ ℤ ℤℓ'
      min max     : ℤ → ℤ → ℤ
      0f 1f       : ℤ
      _+_ _·_     : ℤ → ℤ → ℤ
      -_          : ℤ → ℤ

    abs : ℤ → ℤ
    abs x = max x (- x)

    postulate
      isROrderedCommRing : IsROrderedCommRing _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_
      isAbsOrderedCommRing : IsAbsOrderedCommRing _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_ abs

  module Bundle = ROrderedCommRing {ℤℓ} {ℤℓ'}
  Bundle = ROrderedCommRing {ℤℓ} {ℤℓ'}

  open Postulates public

  Carrier = ℤ

  bundle : Bundle
  bundle = (record
    { Carrier = ℤ
    ; _<_ = _<_
    ; _≤_ = _≤_
    ; _#_ = _#_
    ; min = min
    ; max = max
    ; 0f  = 0f
    ; 1f  = 1f
    ; _+_ = _+_
    ; _·_ = _·_
    ; -_  = -_
    ; isROrderedCommRing = isROrderedCommRing
    ; isAbsOrderedCommRing = isAbsOrderedCommRing
    })

  open IsROrderedCommRing isROrderedCommRing public

  -- abs : ℤ → ℤ
  -- abs x = max x (- x)

module ℤ  = ℤ* hiding (ℤ)
module ℤᶻ = ℤ*
    renaming
    ( Carrier to Carrierᶻ
    ; _<_ to _<ᶻ_
    ; _≤_ to _≤ᶻ_
    ; _#_ to _#ᶻ_
    ; min to minᶻ
    ; max to maxᶻ
    ; 0f  to 0ᶻ
    ; 1f  to 1ᶻ
    ; _+_ to _+ᶻ_
    ; _·_ to _·ᶻ_
    ; -_  to -ᶻ_
    ; isROrderedCommRing to isROrderedCommRingᶻ
    ; abs to absᶻ
    )

module ℚ* where
  module Postulates where
    postulate
      ℚ           : Type ℚℓ
      _<_ _≤_ _#_ : Rel ℚ ℚ ℚℓ'
      min max     : ℚ → ℚ → ℚ
      0f 1f       : ℚ
      _+_ _·_     : ℚ → ℚ → ℚ
      -_          : ℚ → ℚ
      _⁻¹         : (x : ℚ) → {{ x # 0f }} → ℚ

    abs : ℚ → ℚ
    abs x = max x (- x)

    postulate
      isROrderedField : IsROrderedField _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_ _⁻¹
      isAbsOrderedCommRing : IsAbsOrderedCommRing _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_ abs

  module Bundle = ROrderedField {ℚℓ} {ℚℓ'}
  Bundle = ROrderedField {ℚℓ} {ℚℓ'}

  open Postulates public

  Carrier = ℚ

  bundle : Bundle
  bundle = (record
    { Carrier = ℚ
    ; _<_ = _<_
    ; _≤_ = _≤_
    ; _#_ = _#_
    ; min = min
    ; max = max
    ; 0f  = 0f
    ; 1f  = 1f
    ; _+_ = _+_
    ; _·_ = _·_
    ; -_  = -_
    ; _⁻¹ = _⁻¹
    ; isROrderedField = isROrderedField
    ; isAbsOrderedCommRing = isAbsOrderedCommRing
    })

  -- abs : ℚ → ℚ
  -- abs x = max x (- x)

  open IsROrderedField isROrderedField public

module ℚ  = ℚ* hiding (ℚ)
module ℚᶠ = ℚ*
  renaming
  ( Carrier to Carrierᶠ
  ; _<_ to _<ᶠ_
  ; _≤_ to _≤ᶠ_
  ; _#_ to _#ᶠ_
  ; min to minᶠ
  ; max to maxᶠ
  ; 0f  to 0ᶠ
  ; 1f  to 1ᶠ
  ; _+_ to _+ᶠ_
  ; _·_ to _·ᶠ_
  ; -_  to -ᶠ_
  ; _⁻¹ to _⁻¹ᶠ
  ; isROrderedField to isROrderedFieldᶠ
  ; abs to absᶠ
  )

module ℝ* where
  private
    module Postulates where
      postulate
        ℝ           : Type ℝℓ
        _<_ _≤_ _#_ : Rel ℝ ℝ ℝℓ'
        min max     : ℝ → ℝ → ℝ
        0f 1f       : ℝ
        _+_ _·_     : ℝ → ℝ → ℝ
        -_          : ℝ → ℝ
        _⁻¹         : (x : ℝ) → {{ x # 0f }} → ℝ

      abs : ℝ → ℝ
      abs x = max x (- x)

      postulate
        isROrderedField : IsROrderedField _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_ _⁻¹
        isAbsOrderedCommRing : IsAbsOrderedCommRing _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_ abs

        -- square root on ℝ₀⁺
        sqrt : (x : ℝ) → {{0f ≤ x}} → ℝ
        0≤sqrt : ∀ x → {{p : 0f ≤ x}} → 0f ≤ sqrt x {{p}}
        sqrt-reflects-≡ : ∀ x y → {{px : 0f ≤ x}} → {{py : 0f ≤ y}} → sqrt x {{px}} ≡ sqrt y {{py}} → x ≡ y
        sqrt-inv : ∀ x → {{p : 0f ≤ x}} → {{q : 0f ≤ (x · x)}}→ sqrt (x · x) {{q}} ≡ x
        sqrt²-id : ∀ x → {{p : 0f ≤ x}} → sqrt x {{p}} · sqrt x {{p}} ≡ x

  module Bundle = ROrderedField {ℝℓ} {ℝℓ'}
  Bundle = ROrderedField {ℝℓ} {ℝℓ'}

  open Postulates public

  Carrier = ℝ

  bundle : Bundle
  bundle = (record
    { Carrier = ℝ
    ; _<_ = _<_
    ; _≤_ = _≤_
    ; _#_ = _#_
    ; min = min
    ; max = max
    ; 0f  = 0f
    ; 1f  = 1f
    ; _+_ = _+_
    ; _·_ = _·_
    ; -_  = -_
    ; _⁻¹ = _⁻¹
    ; isROrderedField = isROrderedField
    ; isAbsOrderedCommRing = isAbsOrderedCommRing
    })

  -- abs : ℝ → ℝ
  -- abs x = max x (- x)

  open IsROrderedField isROrderedField public

module ℝ  = ℝ* hiding (ℝ)
module ℝʳ = ℝ*
    renaming
    ( Carrier to Carrierʳ
    ; _<_ to _<ʳ_
    ; _≤_ to _≤ʳ_
    ; _#_ to _#ʳ_
    ; min to minʳ
    ; max to maxʳ
    ; 0f  to 0ʳ
    ; 1f  to 1ʳ
    ; _+_ to _+ʳ_
    ; _·_ to _·ʳ_
    ; -_  to -ʳ_
    ; _⁻¹ to _⁻¹ʳ
    ; isROrderedField to isROrderedFieldʳ
    ; isRField to isRFieldʳ
    ; Bundle to Bundleʳ
    ; bundle to bundleʳ
    ; abs to absʳ
    )

module ℂ* where
  open ℝʳ
  module Postulates where
    postulate
      ℂ           : Type ℂℓ
      _#_         : Rel ℂ ℂ ℂℓ'
      0f 1f       : ℂ
      _+_ _·_     : ℂ → ℂ → ℂ
      -_          : ℂ → ℂ
      _⁻¹         : (x : ℂ) → {{ x # 0f }} → ℂ
      isRField : IsRField _#_ 0f 1f _+_ _·_ -_ _⁻¹
      abs         : ℂ → ℝ
      0≤abs       : ∀ x → 0ʳ ≤ʳ abs x
      abs-preserves-0 : ∀ x → x ≡ 0f → abs x ≡ 0ʳ
      abs-reflects-0  : ∀ x → abs x ≡ 0ʳ → x ≡ 0f
      abs-preserves-· : ∀ x y → abs (x · y) ≡ (abs x) ·ʳ (abs y)
      abs-preserves-#0 : ∀ x → x # 0f → abs x #ʳ 0ʳ
      abs-reflects-#0 : ∀ x → abs x #ʳ 0ʳ → x # 0f

  module Bundle = RField {ℂℓ} {ℂℓ'}
  Bundle = RField {ℂℓ} {ℂℓ'}

  open Postulates public

  Carrier = ℂ

  bundle : Bundle
  bundle = (record
    { Carrier  = ℂ
    ; _#_      = _#_
    ; 0f       = 0f
    ; 1f       = 1f
    ; _+_      = _+_
    ; _·_      = _·_
    ; -_       = -_
    ; _⁻¹      = _⁻¹
    ; isRField = isRField
    })

  open IsRField isRField public

module ℂ  = ℂ* hiding (ℂ)
module ℂᶜ = ℂ*
    renaming
    ( Carrier to Carrierᶜ
    ; _#_ to _#ᶜ_
    ; 0f  to 0ᶜ
    ; 1f  to 1ᶜ
    ; _+_ to _+ᶜ_
    ; _·_ to _·ᶜ_
    ; -_  to -ᶜ_
    ; _⁻¹ to _⁻¹ᶜ
    ; isRField to isRFieldᶜ
    ; abs to absᶜ
    )

Isℕ↪ℤ = Number.Inclusions.IsROrderedCommSemiringInclusion
Isℕ↪ℚ = Number.Inclusions.IsROrderedCommSemiringInclusion
Isℕ↪ℂ = Number.Inclusions.IsRCommSemiringInclusion
Isℕ↪ℝ = Number.Inclusions.IsROrderedCommSemiringInclusion
Isℤ↪ℚ = Number.Inclusions.IsROrderedCommRingInclusion
Isℤ↪ℝ = Number.Inclusions.IsROrderedCommRingInclusion
Isℤ↪ℂ = Number.Inclusions.IsRCommRingInclusion
Isℚ↪ℝ = Number.Inclusions.IsROrderedFieldInclusion
Isℚ↪ℂ = Number.Inclusions.IsRFieldInclusion
Isℝ↪ℂ = Number.Inclusions.IsRFieldInclusion

module Isℕ↪ℤ = Number.Inclusions.IsROrderedCommSemiringInclusion
module Isℕ↪ℚ = Number.Inclusions.IsROrderedCommSemiringInclusion
module Isℕ↪ℂ = Number.Inclusions.IsRCommSemiringInclusion
module Isℕ↪ℝ = Number.Inclusions.IsROrderedCommSemiringInclusion
module Isℤ↪ℚ = Number.Inclusions.IsROrderedCommRingInclusion
module Isℤ↪ℝ = Number.Inclusions.IsROrderedCommRingInclusion
module Isℤ↪ℂ = Number.Inclusions.IsRCommRingInclusion
module Isℚ↪ℝ = Number.Inclusions.IsROrderedFieldInclusion
module Isℚ↪ℂ = Number.Inclusions.IsRFieldInclusion
module Isℝ↪ℂ = Number.Inclusions.IsRFieldInclusion

module _ where
  open ℕ* using (ℕ)
  open ℤ* using (ℤ)
  open ℚ* using (ℚ)
  open ℝ* using (ℝ)
  open ℂ* using (ℂ)
  postulate
    ℕ↪ℤ : ℕ → ℤ
    ℕ↪ℚ : ℕ → ℚ
    ℕ↪ℂ : ℕ → ℂ
    ℕ↪ℝ : ℕ → ℝ
    ℤ↪ℚ : ℤ → ℚ
    ℤ↪ℝ : ℤ → ℝ
    ℤ↪ℂ : ℤ → ℂ
    ℚ↪ℝ : ℚ → ℝ
    ℚ↪ℂ : ℚ → ℂ
    ℝ↪ℂ : ℝ → ℂ

    ℕ↪ℤinc : Isℕ↪ℤ (record {ℕ*}) (record {ℤ*}) ℕ↪ℤ
    ℕ↪ℚinc : Isℕ↪ℚ (record {ℕ*}) (record {ℚ*}) ℕ↪ℚ
    ℕ↪ℂinc : Isℕ↪ℂ (record {ℕ*}) (record {ℂ*}) ℕ↪ℂ
    ℕ↪ℝinc : Isℕ↪ℝ (record {ℕ*}) (record {ℝ*}) ℕ↪ℝ
    ℤ↪ℚinc : Isℤ↪ℚ (record {ℤ*}) (record {ℚ*}) ℤ↪ℚ
    ℤ↪ℝinc : Isℤ↪ℝ (record {ℤ*}) (record {ℝ*}) ℤ↪ℝ
    ℤ↪ℂinc : Isℤ↪ℂ (record {ℤ*}) (record {ℂ*}) ℤ↪ℂ
    ℚ↪ℝinc : Isℚ↪ℝ (record {ℚ*}) (record {ℝ*}) ℚ↪ℝ
    ℚ↪ℂinc : Isℚ↪ℂ (record {ℚ*}) (record {ℂ*}) ℚ↪ℂ
    ℝ↪ℂinc : Isℝ↪ℂ (record {ℝ*}) (record {ℂ*}) ℝ↪ℂ

    {-
    ℕ↪ℤinc : Isℕ↪ℤ                    ℕ.bundle    (record { ℤ.Bundle ℤ.bundle }) ℕ↪ℤ
    ℕ↪ℚinc : Isℕ↪ℚ                    ℕ.bundle    (record { ℚ.Bundle ℚ.bundle }) ℕ↪ℚ
    ℕ↪ℂinc : Isℕ↪ℂ                    ℕ.bundle                       ℂ.bundle    ℕ↪ℂ
    ℕ↪ℝinc : Isℕ↪ℝ                    ℕ.bundle    (record { ℝ.Bundle ℝ.bundle }) ℕ↪ℝ
    ℤ↪ℚinc : Isℤ↪ℚ                    ℤ.bundle    (record { ℚ.Bundle ℚ.bundle }) ℤ↪ℚ
    ℤ↪ℝinc : Isℤ↪ℝ                    ℤ.bundle    (record { ℝ.Bundle ℝ.bundle }) ℤ↪ℝ
    ℤ↪ℂinc : Isℤ↪ℂ                    ℤ.bundle                       ℂ.bundle    ℤ↪ℂ
    ℚ↪ℝinc : Isℚ↪ℝ                    ℚ.bundle    (record { ℝ.Bundle ℝ.bundle }) ℚ↪ℝ
    ℚ↪ℂinc : Isℚ↪ℂ (record { ℚ.Bundle ℚ.bundle }) (record { ℂ.Bundle ℂ.bundle }) ℚ↪ℂ
    ℝ↪ℂinc : Isℝ↪ℂ (record { ℝ.Bundle ℝ.bundle }) (record { ℂ.Bundle ℂ.bundle }) ℝ↪ℂ
    -}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

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

postulate
  A : Set
  a b : A
  f : A → A
  rew₁ : f a ≡ b
  rew₂ : f ≡ λ _ → a

{-# REWRITE rew₁ #-}
{-# REWRITE rew₂ #-}


text:
{-# OPTIONS --no-termination-check #-}

module qsort where

  _o_ : {a : Set} -> {b : Set} -> {c : Set} -> (b -> c) -> (a -> b) -> a -> c
  f o g = \x -> f (g x)

  data Bool : Set where
    true  : Bool
    false : Bool

  not : Bool -> Bool
  not true  = false
  not false = true

  if_then_else_ : {a : Set} -> Bool -> a -> a -> a
  if true  then x else _ = x
  if false then _ else y = y

  data List (a : Set) : Set where
    nil  : List a
    _::_ : a -> List a -> List a

  listrec : {a : Set} -> List a -> (a -> List a -> List a) -> List a -> List a
  listrec e _  nil    = e
  listrec e b (x :: xs) = b x (listrec e b xs)

  filter : {a : Set} -> (a -> Bool) -> List a -> List a
  filter f = listrec nil (\x ih -> if (f x) then (x :: ih) else ih)

  _++_ : {a : Set} -> List a -> List a -> List a
  nil ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

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

  _+_ : Nat -> Nat -> Nat
  zero   + m = m
  succ n + m = succ (n + m)

  _*_ : Nat -> Nat -> Nat
  zero   * m = zero
  succ n * m = m + (n * m)

  one : Nat
  one = succ zero

  fact : Nat -> Nat
  fact  zero    = one
  fact (succ n) = succ n * fact n

  _<_ : Nat -> Nat -> Bool
  zero     < zero     = false
  zero     < n        = true
  n        < zero     = false
  (succ n) < (succ m) = n < m

  --

  qsort : {a : Set} -> (a -> a -> Bool) -> List a -> List a
  qsort f nil       = nil
  qsort f (x :: xs) = (qsort f (filter (not o (f x)) xs)) ++
                    (x :: (qsort f (filter (f x) xs)))


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.EquivCarac.A[X]X-A where

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

open import Cubical.Data.Nat
open import Cubical.Data.Vec
open import Cubical.Data.Sigma
open import Cubical.Data.FinData

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-notationZ

open import Cubical.Relation.Nullary

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Functions

module Properties-Equiv-QuotientXn-A
  (Ar@(A , Astr) : CommRing ℓ)
  where

  private
    A[X] : CommRing ℓ
    A[X] = A[X1,···,Xn] Ar 1

    A[x] : Type ℓ
    A[x] = A[x1,···,xn] Ar 1

    A[X]/X : CommRing ℓ
    A[X]/X = A[X1,···,Xn]/<Xkʲ> Ar 1 0 1

    A[x]/x : Type ℓ
    A[x]/x = A[x1,···,xn]/<xkʲ> Ar 1 0 1

  open CommRingStr Astr using ()
    renaming
    ( 0r        to 0A
    ; 1r        to 1A
    ; _+_       to _+A_
    ; -_        to -A_
    ; _·_       to _·A_
    ; +Assoc    to +AAssoc
    ; +Identity to +AIdentity
    ; +Lid      to +ALid
    ; +Rid      to +ARid
    ; +Inv      to +AInv
    ; +Linv     to +ALinv
    ; +Rinv     to +ARinv
    ; +Comm     to +AComm
    ; ·Assoc    to ·AAssoc
    ; ·Identity to ·AIdentity
    ; ·Lid      to ·ALid
    ; ·Rid      to ·ARid
    ; ·Rdist+   to ·ARdist+
    ; ·Ldist+   to ·ALdist+
    ; is-set    to isSetA     )

  open CommRingStr (snd A[X] ) using ()
    renaming
    ( 0r        to 0PA
    ; 1r        to 1PA
    ; _+_       to _+PA_
    ; -_        to -PA_
    ; _·_       to _·PA_
    ; +Assoc    to +PAAssoc
    ; +Identity to +PAIdentity
    ; +Lid      to +PALid
    ; +Rid      to +PARid
    ; +Inv      to +PAInv
    ; +Linv     to +PALinv
    ; +Rinv     to +PARinv
    ; +Comm     to +PAComm
    ; ·Assoc    to ·PAAssoc
    ; ·Identity to ·PAIdentity
    ; ·Lid      to ·PALid
    ; ·Rid      to ·PARid
    ; ·Comm     to ·PAComm
    ; ·Rdist+   to ·PARdist+
    ; ·Ldist+   to ·PALdist+
    ; is-set    to isSetPA     )

  open CommRingStr (snd A[X]/X) using ()
    renaming
    ( 0r        to 0PAI
    ; 1r        to 1PAI
    ; _+_       to _+PAI_
    ; -_        to -PAI_
    ; _·_       to _·PAI_
    ; +Assoc    to +PAIAssoc
    ; +Identity to +PAIIdentity
    ; +Lid      to +PAILid
    ; +Rid      to +PAIRid
    ; +Inv      to +PAIInv
    ; +Linv     to +PAILinv
    ; +Rinv     to +PAIRinv
    ; +Comm     to +PAIComm
    ; ·Assoc    to ·PAIAssoc
    ; ·Identity to ·PAIIdentity
    ; ·Lid      to ·PAILid
    ; ·Rid      to ·PAIRid
    ; ·Rdist+   to ·PAIRdist+
    ; ·Ldist+   to ·PAILdist+
    ; is-set    to isSetPAI     )

  open RingTheory

-----------------------------------------------------------------------------
-- Direct sens

  A[x]→A : A[x] → A
  A[x]→A = Poly-Rec-Set.f _ _ _ isSetA
          0A
          base-trad
          _+A_
          +AAssoc
          +ARid
          +AComm
          base-neutral-eq
          base-add-eq

       where
       base-trad : _
       base-trad (zero ∷ []) a = a
       base-trad (suc k ∷ []) a = 0A

       base-neutral-eq : _
       base-neutral-eq (zero ∷ []) = refl
       base-neutral-eq (suc k ∷ []) = refl

       base-add-eq : _
       base-add-eq (zero ∷ []) a b = refl
       base-add-eq (suc k ∷ []) a b = +ARid _

  A[x]→A-pres1 : A[x]→A 1PA ≡ 1A
  A[x]→A-pres1 = refl

  A[x]→A-pres+ : (x y : A[x]) → (A[x]→A (x +PA y)) ≡ A[x]→A x +A A[x]→A y
  A[x]→A-pres+ x y = refl

  A[x]→A-pres· : (x y : A[x]) → (A[x]→A (x ·PA y)) ≡ A[x]→A x ·A A[x]→A y
  A[x]→A-pres· = Poly-Ind-Prop.f _ _ _
               (λ x u v i y → isSetA _ _ (u y) (v y) i)
               (λ y → sym (0LeftAnnihilates (CommRing→Ring Ar) _))
               (λ v a → Poly-Ind-Prop.f _ _ _ (λ _ → isSetA _ _)
                         (sym (0RightAnnihilates (CommRing→Ring Ar) _))
                         (λ v' a' → base-eq a a' v v')
                         (λ {U V} ind-U ind-V → cong₂ _+A_ ind-U ind-V ∙ sym (·ARdist+ _ _ _)))
               λ {U V} ind-U ind-V y → cong₂ _+A_ (ind-U y) (ind-V y) ∙ sym (·ALdist+ _ _ _)
            where
            base-eq : (a a' : A) → (v v' : Vec ℕ 1) → (A[x]→A (base v a ·PA base v' a')) ≡ A[x]→A (base v a) ·A A[x]→A (base v' a')
            base-eq a a' (zero ∷ []) (zero ∷ []) = refl
            base-eq a a' (zero ∷ []) (suc k' ∷ []) = sym (0RightAnnihilates (CommRing→Ring Ar) _)
            base-eq a a' (suc k ∷ []) (k' ∷ []) = sym (0LeftAnnihilates (CommRing→Ring Ar) _)

  A[X]→A : CommRingHom A[X] Ar
  fst A[X]→A = A[x]→A
  snd A[X]→A = makeIsRingHom A[x]→A-pres1 A[x]→A-pres+ A[x]→A-pres·

  A[x]→A-cancel : (k : Fin 1) → A[x]→A (<Xkʲ> Ar 1 0 1 k) ≡ 0A
  A[x]→A-cancel zero = refl

  A[X]/X→A : CommRingHom A[X]/X Ar
  A[X]/X→A = Quotient-FGideal-CommRing-CommRing.f A[X] Ar A[X]→A (<Xkʲ> Ar 1 0 1) A[x]→A-cancel

  A[x]/x→A : A[x]/x → A
  A[x]/x→A = fst A[X]/X→A

-----------------------------------------------------------------------------
-- Converse sens

  A→A[x] : A → A[x]
  A→A[x] a = base (0 ∷ []) a

  A→A[x]-pres+ : (a a' : A) → A→A[x] (a +A a') ≡ A→A[x] a +PA A→A[x] a'
  A→A[x]-pres+ a a' = sym (base-poly+ (0 ∷ []) a a')

  A→A[x]/x : A → A[x]/x
  A→A[x]/x = [_] ∘ A→A[x]

  A→A[x]/x-pres+ : (a a' : A) → A→A[x]/x (a +A a') ≡ A→A[x]/x a +PAI A→A[x]/x a'
  A→A[x]/x-pres+ a a' = cong [_] (A→A[x]-pres+ a a')

-----------------------------------------------------------------------------
-- Section sens

  e-sect : (a : A) → A[x]→A (A→A[x] a) ≡ a
  e-sect a = refl

-----------------------------------------------------------------------------
-- Retraction sens

  open IsRing

  e-retr : (x : A[x]/x) → A→A[x]/x (A[x]/x→A x) ≡ x
  e-retr = SQ.elimProp (λ x → isSetPAI _ _)
           (Poly-Ind-Prop.f _ _ _ (λ x → isSetPAI _ _)
           (cong [_] (base-0P _))
           (λ v a → base-eq a v)
           λ {U V} ind-U ind-V → cong [_] ((A→A[x]-pres+ _ _)) ∙ cong₂ _+PAI_ ind-U ind-V)

         where
         base-eq : (a : A) → (v : Vec ℕ 1) → A→A[x]/x (A[x]/x→A [ (base v a) ]) ≡ [ (base v a) ]
         base-eq a (zero ∷ []) = cong [_] refl
         base-eq a (suc k ∷ []) = eq/ (base (0 ∷ []) 0A) (base (suc k ∷ []) a) ∣ ((λ x → base (k ∷ []) (-A a)) , helper) ∣₁
           where
           helper : _
           helper = cong (λ X → X poly+ base (suc k ∷ []) (-A a)) (base-0P _)
                     ∙ +PALid _
                     ∙ sym (+PARid _
                            ∙ cong₂ base
                                    (cong (λ X → X ∷ []) (+-suc _ _ ∙ +-zero _))
                                    (·ARid _))

module _
  (Ar@(A , Astr) : CommRing ℓ)
  where

  open Iso
  open Properties-Equiv-QuotientXn-A Ar

  Equiv-A[X]/X-A : CommRingEquiv (A[X1,···,Xn]/<Xkʲ> Ar 1 0 1) Ar
  fst Equiv-A[X]/X-A = isoToEquiv is
    where
    is : Iso (A[x1,···,xn]/<xkʲ> Ar 1 0 1) A
    fun is = A[x]/x→A
    inv is = A→A[x]/x
    rightInv is = e-sect
    leftInv is = e-retr
  snd Equiv-A[X]/X-A = snd A[X]/X→A

Equiv-ℤ[X]/X-ℤ : RingEquiv (CommRing→Ring ℤ[X]/X) (CommRing→Ring ℤCR)
Equiv-ℤ[X]/X-ℤ = Equiv-A[X]/X-A ℤCR

max_stars_repo_name: xekoukou/cubical

max_issues_repo_name: xekoukou/cubical

max_forks_repo_name: xekoukou/cubical


text:
module builtinInModule where

module Str where

  {-# BUILTIN STRING S #-}
  primitive primStringAppend : S → S → S

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

{- In this module, we derive the truncations of
  * a truncated type,
  * the unit type,
  * dependent sums (and product types),
  * path spaces
  given truncations of their components.

  More commonly later on, we will be given a truncation operator Tr
  that returns a truncation for any given input type (at a fixed level).
  Instead of trying to show, say,

    Tr (Σ A (B ∘ cons (Tr A))) ≃ Σ (Tr A) (Tr ∘ B),

  directly, it turns out to be much easier to just *derive* the truncation on
  the left-hand side from Tr A and Tr ∘ B and then use unicity of truncation to
  deduce the above equivalence. Significant parts of the unicity proof would be
  duplicated in any direct proof of equivalence, while this approach allows us
  to avoid a number of manual elimination and propositional reduction steps. -}
module Universe.Trunc.TypeConstructors where

open import lib.Basics
open import lib.NType2
open import lib.Equivalences2
open import lib.types.Unit
open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Paths

open import Universe.Utility.General
open import Universe.Utility.TruncUniverse

open import Universe.Trunc.Universal
open import Universe.Trunc.Basics

open trunc-ty
open trunc-props

module trunc-self {i} {n : ℕ₋₂} (A : n -Type i) where
  trunc : ∀ {j} → trunc-ty n ⟦ A ⟧ j
  trunc = record
    { type = A
    ; cons = idf _
    ; univ = λ _ → snd (ide _) }

module trunc-⊤ {n : ℕ₋₂} = trunc-self {n = n} ⊤-≤

-- *** Lemma 6.9 ***
{- The truncation of a dependent sum type (where the family depends
   only on the truncation of the first component) is the dependent sums
   of the truncations. -}
module trunc-Σ {ia ib j} {n : ℕ₋₂} {A : Type ia}
               (TrA : trunc-ty n A (ia ⊔ ib ⊔ j))
               {B : ⟦ type TrA ⟧ → Type ib}
               (TrB : (ta : ⟦ type TrA ⟧) → trunc-ty n (B ta) (ib ⊔ j)) where

  trunc : trunc-ty n (Σ A (B ∘ cons TrA)) (ib ⊔ j)
  trunc = record
    { type = Σ-≤ (type TrA) (type ∘ TrB)
    ; cons = λ {(a , b) → (cons TrA a , cons (TrB (cons TrA a)) b)}
    ; univ = snd ∘ e } where

    e : (U : n -Type _) → _
    e U =
      (⟦ Σ-≤ (type TrA) (type ∘ TrB) ⟧         → ⟦ U ⟧)  ≃⟨ curry-equiv ⟩
      ((ta : ⟦ type TrA ⟧) → ⟦ type (TrB ta) ⟧ → ⟦ U ⟧)  ≃⟨ equiv-Π-r eb ⟩
      ((ta : ⟦ type TrA ⟧) → B ta              → ⟦ U ⟧)  ≃⟨ ea ⟩
      ((a : A)             → B (cons TrA a)    → ⟦ U ⟧)  ≃⟨ curry-equiv ⁻¹ ⟩
      (Σ A (B ∘ cons TrA)                      → ⟦ U ⟧)  ≃∎ where

      ea = dup {j = ib ⊔ j} TrA (λ ta → B ta →-≤ U)
      eb = λ ta → up {j = ib ⊔ j} (TrB ta) U

-- Products are a special case of dependent sums.
module trunc-× {ia ib j} {n : ℕ₋₂} {A : Type ia} {B : Type ib}
               (TrA : trunc-ty n A (ia ⊔ ib ⊔ j))
               (TrB : trunc-ty n B (ib ⊔ j)) =
  trunc-Σ {j = j} TrA (λ _ → TrB)

-- *** Lemma 6.10 ***
{- The n-truncation of a path space is the path space of the (n+1)-truncation.
   The use of the encode-decode method is the reason why we have to assume
   elimination into Type (lsucc i): large recursion is used to define
   the type of codes. -}
module trunc-path {i j} {n : ℕ₋₂} {A : Type i} (TrA : trunc-ty (S n) A (lsucc (i ⊔ j))) where
  private
    l : ULevel
    l = i ⊔ j

    TrAA : trunc-ty (S n) (A × A) (lsucc l)
    TrAA = trunc-×.trunc {j = lsucc l} TrA TrA

    module MA  = trunc-props {j = lsucc l} {k = l} TrA
    module MAA = trunc-props {j = lsucc l} {k = l} TrAA
--    module MAL = trunc-elim {j = _} TrAA

  {- There is some Yoneda hidden here that would enable us to express the final
     equivalence e neatly as a sequence of trivial steps like in trunc-Σ;
     unfortunately we lack the necessary category theoretic framework
     in this code base. -}
  module code (U : n -Type l) where
    abstract
      {- Large recursion used here.
         Since we cannot talk about the truncation of a₀ == a₁ yet,
         we instead talk about the continuation type (a₀ == a₁ → U) → U
         for any n-type U instead. -}
      code : ⟦ type TrAA ⟧ → n -Type l
      code = rec {j = lsucc l} TrAA (n -Type-≤ l)
                 (λ {(a₀ , a₁) → (a₀ == a₁ → ⟦ U ⟧) →-≤ U})

      code-β : {a₀ a₁ : A} → ⟦ code (cons TrAA (a₀ , a₁)) ⟧
                           ≃ ((a₀ == a₁ → ⟦ U ⟧) → ⟦ U ⟧)
      code-β = coe-equiv (ap ⟦_⟧ (rec-β TrAA _))

    -- We can encode a path in the truncation, ...
    encode : {ta₀ ta₁ : ⟦ type TrA ⟧} → ta₀ == ta₁ → ⟦ code (ta₀ , ta₁) ⟧
    encode idp = MA.elim (λ ta → raise (code (ta , ta)))
                         (λ _ → <– code-β (λ f → f idp)) _

    --- ...reducing when coming from a path in the original type.
    encode-β : {a₀ a₁ : A} (p : a₀ == a₁) (f : a₀ == a₁ → ⟦ U ⟧)
             → –> code-β (encode (ap (cons TrA) p)) f == f p
    encode-β idp = app= (ap (–> code-β) (MA.elim-β _) ∙ <–-inv-r code-β _)

    -- We can decode into the U-continuation of a path in the truncation, ...
    decode : {ta₀ ta₁ : ⟦ type TrA ⟧}
           → ⟦ code (ta₀ , ta₁) ⟧ → (ta₀ == ta₁ → ⟦ U ⟧) → ⟦ U ⟧
    decode = MAA.elim
      (λ {(ta₀ , ta₁) → _ →-≤ (ta₀ == ta₁ → ⟦ U ⟧) →-≤ raise U})
      (λ _ c g → –> code-β c (g ∘ ap (cons TrA))) _ where

    -- ...reducing
    decode-β : {a₀ a₁ : A} (c : ⟦ code (cons TrAA (a₀ , a₁)) ⟧)
               (g : cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧)
             → decode c g == –> code-β c (g ∘ ap (cons TrA))
    decode-β = app= ∘ app= (MAA.elim-β _)

    -- encoding followed by decoding produces the expected continuation
    decode-encode : {ta₀ ta₁ : ⟦ type TrA ⟧} (q : ta₀ == ta₁)
                    (g : ta₀ == ta₁ → ⟦ U ⟧) → decode (encode q) g == g q
    decode-encode idp = MA.elim
      (λ ta → Π-≤ (ta == ta → ⟦ U ⟧)
                  (λ g → Path-≤ (raise U) (decode (encode idp) g) (g idp)))
      (λ _ g → decode-β (encode idp) g ∙ encode-β idp (g ∘ ap (cons TrA))) _

  trunc : (a₀ a₁ : A) → trunc-ty n (a₀ == a₁) l
  trunc a₀ a₁ = record
    { type = Path-< (type TrA) (cons TrA a₀) (cons TrA a₁)
    ; cons = ap (cons TrA)
    ; univ = snd ∘ e } where

    e : (U : _) → (cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧) ≃ (a₀ == a₁ → ⟦ U ⟧)
    e U = equiv u v u-v v-u where
      open code U

      u : (cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧) → a₀ == a₁ → ⟦ U ⟧
      u g = g ∘ ap (cons TrA)

      v : (a₀ == a₁ → ⟦ U ⟧) → cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧
      v f q = –> code-β (encode q) f

      u-v : (f : a₀ == a₁ → ⟦ U ⟧) → u (v f) == f
      u-v f = λ= (λ p → encode-β p f)

      v-u : (g : cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧) → v (u g) == g
      v-u g = λ= (λ q → ! (decode-β (encode q) g) ∙ decode-encode q g)

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
-- Categories with objects parameterised by a sort
module SOAS.Sorting {T : Set} where

open import SOAS.Common

import Categories.Category.CartesianClosed.Canonical as Canonical
import Categories.Category.CartesianClosed as CCC
open import Categories.Category.Cocartesian
open import Categories.Category.BicartesianClosed
import Categories.Category.Monoidal as Monoidal
import Categories.Category.Monoidal.Closed as MonClosed
open import Categories.Object.Product
open import Categories.Functor.Bifunctor

-- Add sorting to a set
Sorted : Set₁ → Set₁
Sorted Obj = T → Obj

-- Lift a function on Obj to one on sorted Obj
sorted : {O₁ O₂ : Set₁} → (O₁ → O₂) → Sorted O₁ → Sorted O₂
sorted f 𝒳 τ = f (𝒳 τ)

-- Lift a binary operation on Obj to one on sorted Obj
sorted₂ : {O₁ O₂ O₃ : Set₁} → (O₁ → O₂ → O₃)
                            → Sorted O₁ → Sorted O₂ → Sorted O₃
sorted₂ op 𝒳 𝒴 τ = op (𝒳 τ) (𝒴 τ)

sortedᵣ : {O₁ O₂ O₃ : Set₁} → (O₁ → O₂ → O₃)
                            → O₁ → Sorted O₂ → Sorted O₃
sortedᵣ op X 𝒴 τ = op X (𝒴 τ)

sortedₗ : {O₁ O₂ O₃ : Set₁} → (O₁ → O₂ → O₃)
                           → Sorted O₁ → O₂ → Sorted O₃
sortedₗ op 𝒳 Y τ = op (𝒳 τ) Y

-- Turn a category into a sorted category
𝕊orted : Category 1ℓ 0ℓ 0ℓ → Category 1ℓ 0ℓ 0ℓ
𝕊orted Cat = categoryHelper (record
  { Obj = Sorted Obj
  ; _⇒_ = λ A B → ∀{τ : T} → A τ ⇒ B τ
  ; _≈_ = λ f g → ∀{α : T} → f {α} ≈ g {α}
  ; id = id Cat
  ; _∘_ = λ g f → Category._∘_ Cat g f
  ; assoc = assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv = record { refl = E.refl equiv ; sym = λ p → E.sym equiv p
                   ; trans = λ p q → E.trans equiv p q }
  ; ∘-resp-≈ = λ p q → ∘-resp-≈ p q
  })
  where
  open Category Cat
  open import Relation.Binary.Structures renaming (IsEquivalence to E)

-- Lift functors to functors between sorted categories
𝕊orted-Functor : {ℂ 𝔻 : Category 1ℓ 0ℓ 0ℓ} → Functor ℂ 𝔻 → Functor (𝕊orted ℂ) (𝕊orted 𝔻)
𝕊orted-Functor F = record
  { F₀ = λ X τ → Functor.₀ F (X τ)
  ; F₁ = λ f → Functor.₁ F f
  ; identity = Functor.identity F
  ; homomorphism = Functor.homomorphism F
  ; F-resp-≈ = λ z → Functor.F-resp-≈ F z
  }

-- Lift bifunctors to bifunctors between sorted categories
𝕊orted-Bifunctor : {ℂ 𝔻 𝔼 : Category 1ℓ 0ℓ 0ℓ} → Bifunctor ℂ 𝔻 𝔼 → Bifunctor (𝕊orted ℂ) (𝕊orted 𝔻) (𝕊orted 𝔼)
𝕊orted-Bifunctor F = record
  { F₀ = λ{ (X , Y) τ → Functor.₀ F (X τ , Y τ)}
  ; F₁ = λ{ (f , g) → Functor.₁ F (f , g)}
  ; identity = Functor.identity F
  ; homomorphism = Functor.homomorphism F
  ; F-resp-≈ = λ{ (p , q) → Functor.F-resp-≈ F (p , q)}
  }

private
  variable C : Category 1ℓ 0ℓ 0ℓ

-- A sorted CCC is itself a CCC
𝕊orted-CanCCC : Canonical.CartesianClosed C
              → Canonical.CartesianClosed (𝕊orted C)
𝕊orted-CanCCC CCC = record
  { ⊤ = λ τ → 𝓒.terminal.⊤
  ; _×_ = λ A B τ → (A τ) 𝓒.× (B τ)
  ; ! = 𝓒.terminal.!
  ; π₁ = 𝓒.π₁
  ; π₂ = 𝓒.π₂
  ; ⟨_,_⟩ = λ f g → 𝓒.⟨ f , g ⟩
  ; !-unique = λ f → 𝓒.terminal.!-unique f
  ; π₁-comp = 𝓒.π₁-comp
  ; π₂-comp = 𝓒.π₂-comp
  ; ⟨,⟩-unique = λ p₁ p₂ → 𝓒.⟨,⟩-unique p₁ p₂
  ; _^_ = λ B A τ → B τ 𝓒.^ A τ
  ; eval = 𝓒.eval
  ; curry = λ f → 𝓒.curry f
  ; eval-comp = 𝓒.eval-comp
  ; curry-resp-≈ = λ p → 𝓒.curry-resp-≈ p
  ; curry-unique = λ p → 𝓒.curry-unique p
  } where private module 𝓒 = Canonical.CartesianClosed CCC

-- A sorted co-Cartesian category is co-Cartesian
𝕊orted-Cocartesian : Cocartesian C
                   → Cocartesian (𝕊orted C)
𝕊orted-Cocartesian Cocart = record
  { initial = record
    { ⊥ = λ τ → 𝓒.⊥ ; ⊥-is-initial = record
      { ! = 𝓒.initial.! ; !-unique = λ f → 𝓒.initial.!-unique f } }
  ; coproducts = record { coproduct = λ {A}{B} → record
    { A+B = λ τ → 𝓒.coproduct.A+B {A τ}{B τ}
    ; i₁ = 𝓒.i₁
    ; i₂ = 𝓒.i₂
    ; [_,_] = λ f g → 𝓒.[ f , g ]
    ; inject₁ = 𝓒.inject₁
    ; inject₂ = 𝓒.inject₂
    ; unique = λ p₁ p₂ → 𝓒.coproduct.unique p₁ p₂
    } }
  } where private module 𝓒 = Cocartesian Cocart

-- A sorted bi-Cartesian closed category is itself bi-Cartesian closed
𝕊orted-BCCC : BicartesianClosed C
            → BicartesianClosed (𝕊orted C)
𝕊orted-BCCC BCCC = record
  { cartesianClosed = fromCanonical _ (𝕊orted-CanCCC (toCanonical _ cartesianClosed))
  ; cocartesian = 𝕊orted-Cocartesian cocartesian
  }
  where
  open BicartesianClosed BCCC
  open Canonical.Equivalence

-- A sorted monoidal category is itself monoidal
𝕊orted-Monoidal : Monoidal.Monoidal C
                → Monoidal.Monoidal (𝕊orted C)
𝕊orted-Monoidal {C} Mon = record
  { ⊗ = record
    { F₀ = λ{ (X , Y) τ → X τ 𝓒.⊗₀ Y τ }
    ; F₁ = λ{ (f , g) → f 𝓒.⊗₁ g}
    ; identity = Functor.identity 𝓒.⊗
    ; homomorphism = Functor.homomorphism 𝓒.⊗
    ; F-resp-≈ = λ{ (p₁ , p₂) {α} → Functor.F-resp-≈ 𝓒.⊗ (p₁ , p₂) }
    }
  ; unit = λ τ → 𝓒.unit
  ; unitorˡ = record { from = λ {τ} → 𝓒.unitorˡ.from ; to = 𝓒.unitorˡ.to
                     ; iso = record { isoˡ = Iso.isoˡ 𝓒.unitorˡ.iso ; isoʳ = Iso.isoʳ 𝓒.unitorˡ.iso } }
  ; unitorʳ = record { from = λ {τ} → 𝓒.unitorʳ.from ; to = 𝓒.unitorʳ.to
                     ; iso = record { isoˡ = Iso.isoˡ 𝓒.unitorʳ.iso ; isoʳ = Iso.isoʳ 𝓒.unitorʳ.iso } }
  ; associator = record { from = λ {τ} → 𝓒.associator.from ; to = 𝓒.associator.to
                        ; iso = record { isoˡ = Iso.isoˡ 𝓒.associator.iso ; isoʳ = Iso.isoʳ 𝓒.associator.iso } }
  ; unitorˡ-commute-from = 𝓒.unitorˡ-commute-from
  ; unitorˡ-commute-to = 𝓒.unitorˡ-commute-to
  ; unitorʳ-commute-from = 𝓒.unitorʳ-commute-from
  ; unitorʳ-commute-to = 𝓒.unitorʳ-commute-to
  ; assoc-commute-from = 𝓒.assoc-commute-from
  ; assoc-commute-to = 𝓒.assoc-commute-to
  ; triangle = 𝓒.triangle
  ; pentagon = 𝓒.pentagon
  }
  where
  private module 𝓒 = Monoidal.Monoidal Mon
  open import Categories.Morphism C

-- A sorted monoidal closed category is itself monoidal closed
𝕊orted-MonClosed : {Mon : Monoidal.Monoidal C}
                 → MonClosed.Closed Mon
                 → MonClosed.Closed (𝕊orted-Monoidal Mon)
𝕊orted-MonClosed {Mon} Cl = record
  { [-,-] = record
    { F₀ = λ (X , Y) τ → 𝓒.[ X τ , Y τ ]₀
    ; F₁ = λ (f , g) → 𝓒.[ f , g ]₁
    ; identity = λ {A} {α} → Functor.identity 𝓒.[-,-]
    ; homomorphism = Functor.homomorphism 𝓒.[-,-]
    ; F-resp-≈ = λ{ (p₁ , p₂) {α} → Functor.F-resp-≈ 𝓒.[-,-] (p₁ , p₂) }
    }
  ; adjoint = record
    { unit = ntHelper record
      { η = λ X {τ} → NT.η 𝓒.adjoint.unit (X τ)
      ; commute = λ f → NT.commute 𝓒.adjoint.unit f
      }
    ; counit = ntHelper record
      { η = λ X {τ} → NT.η 𝓒.adjoint.counit (X τ)
      ; commute = λ f → NT.commute 𝓒.adjoint.counit f
      }
    ; zig = 𝓒.adjoint.zig
    ; zag = 𝓒.adjoint.zag
    }
  ; mate = λ f → record { commute₁ = 𝓒.mate.commute₁ f ; commute₂ = 𝓒.mate.commute₂ f }
  } where private module 𝓒 = MonClosed.Closed Cl

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------------
-- Conversion rules for the division
------------------------------------------------------------------------------

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

module FOTC.Program.Division.ConversionRulesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Program.Division.Division

------------------------------------------------------------------------------
-- Division properties

private
    -- Before to prove some properties for div it is convenient
    -- to have a proof for each possible execution step.

    -- Initially, we define the possible states (div-s₁, div-s₂, ...)
    -- and after that, we write down the proof for the execution step
    -- from the state p to the state q, e.g.
    --
    -- proof₂₋₃ : ∀ i j → div-s₂ i j ≡ div-s₃ i j.

    -- Initially, the conversion rule div-eq is applied.
    div-s₁ : D → D → D
    div-s₁ i j = if (lt i j) then zero else succ₁ (div (i ∸ j) j)

    -- lt i j ≡ true.
    div-s₂ : D → D → D
    div-s₂ i j = if true
                   then zero
                   else succ₁ (div (i ∸ j) j)

    -- lt i j ≡ false.
    div-s₃ : D → D → D
    div-s₃ i j = if false
                   then zero
                   else succ₁ (div (i ∸ j) j)

    -- The conditional is true.
    div-s₄ : D
    div-s₄ = zero

    -- The conditional is false.
    div-s₅ : D → D → D
    div-s₅ i j = succ₁ (div (i ∸ j) j)

    {-

    To prove the execution steps, e.g.

    proof₃₋₄ : ∀ i j → div-s₃ i j → divh_s₄ i j,

    we usually need to prove that

                             ... m ... ≡ ... n ...    (1)

    given that
                                  m ≡ n,              (2)

    where (2) is a conversion rule usually.

    We prove (1) using

    subst : ∀ {x y} (A : D → Set) → x ≡ y → A x → A y

    where
      • P is given by \m → ... m ... ≡ ... n ...,
      • x ≡ y is given n ≡ m (actually, we use ≡-sym (m ≡ n)) and
      • P x is given by ... n ... ≡ ... n ... (i.e. ≡-refl)

    -}

    -- From div i j to div-s₁ using the equation div-eq.
    proof₀₋₁ : ∀ i j → div i j ≡ div-s₁ i j
    proof₀₋₁ i j = div-eq i j

    -- From div-s₁ to div-s₂ using the proof i<j.
    proof₁₋₂ : ∀ i j → i < j → div-s₁ i j ≡ div-s₂ i j
    proof₁₋₂ i j i<j =
      subst (λ t → (if t
                      then zero
                      else succ₁ (div (i ∸ j) j))
                   ≡
                   (if true
                      then zero
                      else succ₁ (div (i ∸ j) j))
            )
            (sym i<j)
            refl

    -- From div-s₁ to div-s₃ using the proof i≮j.
    proof₁₋₃ : ∀ i j → i ≮ j → div-s₁ i j ≡ div-s₃ i j
    proof₁₋₃ i j i≮j =
      subst (λ t → (if t
                      then zero
                      else succ₁ (div (i ∸ j) j))
                   ≡
                   (if false
                      then zero
                      else succ₁ (div (i ∸ j) j))
            )
            (sym i≮j)
            refl

    -- From div-s₂ to div-s₄ using the conversion rule if-true.
    proof₂₋₄ : ∀ i j → div-s₂ i j ≡ div-s₄
    proof₂₋₄ i j = if-true zero

    -- From div-s₃ to div-s₅ using the conversion rule if-false.
    proof₃₋₅ : ∀ i j → div-s₃ i j ≡ div-s₅ i j
    proof₃₋₅ i j = if-false (succ₁ (div (i ∸ j) j))

----------------------------------------------------------------------
-- The division result when the dividend is minor than the
-- the divisor.
div-x<y : ∀ {i j} → i < j → div i j ≡ zero
div-x<y {i} {j} i<j =
  div i j    ≡⟨ proof₀₋₁ i j ⟩
  div-s₁ i j ≡⟨ proof₁₋₂ i j i<j ⟩
  div-s₂ i j ≡⟨ proof₂₋₄ i j ⟩
  div-s₄     ∎

----------------------------------------------------------------------
-- The division result when the dividend is greater or equal than the
-- the divisor.
div-x≮y : ∀ {i j} → i ≮ j → div i j ≡ succ₁ (div (i ∸ j) j)
div-x≮y {i} {j} i≮j =
  div i j    ≡⟨ proof₀₋₁ i j ⟩
  div-s₁ i j ≡⟨ proof₁₋₃ i j i≮j ⟩
  div-s₃ i j ≡⟨ proof₃₋₅ i j ⟩
  div-s₅ i j ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Imports from the standard library

module Library where

-- open import Level using () renaming (suc to lsuc) public

open import Data.Fin using (Fin; zero; suc) public
open import Data.List using (List; []; _∷_; map) public
open import Data.Nat
  using    (ℕ; zero; suc; z≤n; s≤s; pred; _≤′_; ≤′-refl; ≤′-step )
  renaming (_≤_ to _≤ℕ_;  _⊔_ to max)
  public
open import Data.Nat.Properties
  using (_+-mono_; ≤⇒≤′)
  renaming (≤-decTotalOrder to decTotalOrderℕ)
  public
open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂) renaming (map to map×) public

open import Function using (id; _∘_) public

open import Induction.WellFounded using (Acc; acc) public

open import Relation.Binary using (module DecTotalOrder)
open import Relation.Binary.List.Pointwise as ListEq using ([]; _∷_) renaming (Rel to ≅L) hiding (module Rel) public
module ≅L = ListEq
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; module ≡-Reasoning) public
module ≡ = PropEq
open import Size public

module DecTotalOrderℕ = DecTotalOrder decTotalOrderℕ
module ≤ℕ = DecTotalOrderℕ

caseMax : ∀{m n} (P : ℕ → Set)
          → (pn : (m≤n : m ≤ℕ n) → P n)
          → (pm : (n≤m : n ≤ℕ m) → P m)
          → P (max m n)
caseMax {zero } {n    } P pn pm = pn z≤n
caseMax {suc m} {zero } P pn pm = pm z≤n
caseMax {suc m} {suc n} P pn pm = caseMax (P ∘ suc) (pn ∘ s≤s) (pm ∘ s≤s)

n≤sn : ∀{n} → n ≤ℕ suc n
n≤sn = (z≤n {1}) +-mono DecTotalOrderℕ.refl

pred≤ℕ : ∀{n m} → suc n ≤ℕ suc m → n ≤ℕ m
pred≤ℕ (s≤s p) = p

record ⊤ {a} : Set a where

-- TODOs

postulate
  TODO : ∀ {a}{A : Set a} → A

-- -}

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization