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

module Math.Googology.Function.Properties where

-- agda-stdlib
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.GeneralisedArithmetic using (fold)
open import Data.List
open import Function
open import Relation.Binary.PropositionalEquality

-- agda-misc
open import Math.Googology.Function

open ≤-Reasoning

------------------------------------------------------------------------
-- Properties of hyperoperation

H-rec : ∀ n a b → H (suc n) a (suc b) ≡ H n a (H (suc n) a b)
H-rec zero          a b = refl
H-rec (suc zero)    a b = refl
H-rec (suc (suc n)) a b = refl

-- H₀ is successor.
H-suc : ∀ a b → H 0 a b ≡ suc b
H-suc a b = refl

-- H₁ is addition.
H-+ : ∀ a b → H 1 a b ≡ a + b
H-+ a 0       = sym $ +-identityʳ a
H-+ a (suc b) = begin-equality
  suc (H 1 a b) ≡⟨ cong suc $ H-+ a b ⟩
  suc (a + b)   ≡⟨⟩
  suc a + b     ≡⟨ sym $ +-suc a b ⟩
  a + suc b     ∎

-- H₂ is multiplication.
H-* : ∀ a b → H 2 a b ≡ a * b
H-* a 0       = sym $ *-zeroʳ a
H-* a (suc b) = begin-equality
  H 1 a (H 2 a b) ≡⟨ cong (H 1 a) $ H-* a b ⟩
  H 1 a (a * b)   ≡⟨ H-+ a (a * b) ⟩
  a + a * b       ≡⟨ sym $ *-suc a b ⟩
  a * suc b       ∎

-- H₃ is exponentiation.
H-^ : ∀ a b → H 3 a b ≡ a ^ b
H-^ a 0       = refl
H-^ a (suc b) = begin-equality
  H 2 a (H 3 a b) ≡⟨ cong (H 2 a) $ H-^ a b ⟩
  H 2 a (a ^ b)   ≡⟨ H-* a (a ^ b) ⟩
  a * (a ^ b)     ∎

-- Hₙ(a, 1) = a  (n ≥ 2)
H[2+n,a,1]≡a : ∀ n a → H (2 + n) a 1 ≡ a
H[2+n,a,1]≡a 0       a = refl
H[2+n,a,1]≡a (suc n) a = begin-equality
  H (suc (suc (suc n))) a 1 ≡⟨ H-rec (suc (suc n)) a 0 ⟩
  H (2 + n) a 1             ≡⟨ H[2+n,a,1]≡a n a ⟩
  a                         ∎

-- a ↑ⁿ 1 ≡ a
a↑ⁿ1≡a : ∀ a n → a ↑[ n ] 1 ≡ a
a↑ⁿ1≡a a n = H[2+n,a,1]≡a n a

-- Hₙ(2, 2) = 4  (n ≥ 1)
H[1+n,2,2]≡4 : ∀ n → H (1 + n) 2 2 ≡ 4
H[1+n,2,2]≡4 0       = refl
H[1+n,2,2]≡4 (suc n) = begin-equality
  H (suc (suc n)) 2 (suc 1)         ≡⟨ H-rec (suc n) 2 1 ⟩
  H (suc n) 2 (H (suc (suc n)) 2 1) ≡⟨ cong (H (suc n) 2) $ H[2+n,a,1]≡a n 2 ⟩
  H (suc n) 2 2                     ≡⟨ H[1+n,2,2]≡4 n ⟩
  4                                 ∎

-- Hₙ(1, b) = 1  (n ≥ 3)
H[3+n,1,b]≡1 : ∀ n b → H (3 + n) 1 b ≡ 1
H[3+n,1,b]≡1 0       b       = trans (H-^ 1 b) (^-zeroˡ b)
H[3+n,1,b]≡1 (suc n) 0       = refl
H[3+n,1,b]≡1 (suc n) (suc b) = H[3+n,1,b]≡1 n (H (4 + n) 1 b)

-- Hₙ(a, a) = H₁₊ₙ(a, 2)  (n ≥ 1)
H[1+n,a,a]≡H[2+n,a,2] : ∀ n a → H (1 + n) a a ≡ H (2 + n) a 2
H[1+n,a,a]≡H[2+n,a,2] n a = sym lemma where
  lemma : H (2 + n) a 2 ≡ H (1 + n) a a
  lemma = begin-equality
    H (suc (suc n)) a 2
      ≡⟨ H-rec (suc n) a 1 ⟩
    H (suc n) a (H (suc (suc n)) a 1)
      ≡⟨ cong (H (suc n) a) $ H[2+n,a,1]≡a n a ⟩
    H (suc n) a a
      ∎

H-is-fold : ∀ n a b → H (3 + n) a b ≡ fold 1 (H (2 + n) a) b
H-is-fold n a 0       = refl
H-is-fold n a (suc b) = cong (H (2 + n) a) $ H-is-fold n a b

H[1+n,2,3]≡H[n,2,4] : ∀ n → H (1 + n) 2 3 ≡ H n 2 4
H[1+n,2,3]≡H[n,2,4] 0       = refl
H[1+n,2,3]≡H[n,2,4] (suc n) = begin-equality
  H (2 + n) 2 3
    ≡⟨ H-rec (1 + n) 2 2 ⟩
  H (1 + n) 2 (H (2 + n) 2 2)
    ≡⟨ cong (H (1 + n) 2) $ H[1+n,2,2]≡4 (1 + n) ⟩
  H (1 + n) 2 4
    ∎

H[2+n,0,1]≡0 : ∀ n → H (2 + n) 0 1 ≡ 0
H[2+n,0,1]≡0 zero    = refl
H[2+n,0,1]≡0 (suc n) = H[2+n,0,1]≡0 n

H[4+n,0,2*b]≡1   : ∀ n b → H (4 + n) 0 (2 * b) ≡ 1
H[4+n,0,1+2*b]≡0 : ∀ n b → H (4 + n) 0 (1 + 2 * b) ≡ 0
H[4+n,0,2*b]≡1 n zero    = refl
H[4+n,0,2*b]≡1 n (suc b) = begin-equality
  H (3 + n) 0 (H (4 + n) 0 (b + (suc (b + 0))))
    ≡⟨ cong (λ v → H (3 + n) 0 (H (4 + n) 0 v)) $ +-suc b (b + 0) ⟩
  H (3 + n) 0 (H (4 + n) 0 (1 + 2 * b))
    ≡⟨ cong (H (3 + n) 0) $ H[4+n,0,1+2*b]≡0 n b ⟩
  H (3 + n) 0 0
    ≡⟨⟩
  1
    ∎
H[4+n,0,1+2*b]≡0 n b = begin-equality
  H (3 + n) 0 (H (4 + n) 0 (2 * b))
    ≡⟨ cong (H (3 + n) 0) $ H[4+n,0,2*b]≡1 n b ⟩
  H (3 + n) 0 1
    ≡⟨ H[2+n,0,1]≡0 (suc n) ⟩
  0
    ∎

------------------------------------------------------------------------
-- Properties of `ack`

private
  ack-H-helper :
    (P : ℕ → ℕ → Set) →
    (∀ n → P 0 n) →
    (∀ m → P m 1 → P (suc m) 0) →
    (∀ m n → P (suc m) n → (∀ n′ → P m n′) → P (suc m) (suc n)) →
    ∀ m n → P m n
  ack-H-helper P P[0,n] P[m,0] P[m,n] = go where
    go : ∀ m n → P m n
    go 0       n       = P[0,n] n
    go (suc m) 0       = P[m,0] m (go m 1)
    go (suc m) (suc n) = P[m,n] m n (go (suc m) n) (go m)

-- Ackermann function can be expressed in terms of hyperoperation.
-- 3 + Ack(m, n) = Hₙ(2, 3 + n)
ack-H : ∀ m n → 3 + ack m n ≡ H m 2 (3 + n)
ack-H = ack-H-helper P (λ _ → refl) P[m,0] P[m,n]
  where
  P : ℕ → ℕ → Set
  P m n = 3 + ack m n ≡ H m 2 (3 + n)

  P[m,0] : ∀ m → P m 1 → P (suc m) 0
  P[m,0] m P[m,1] = trans P[m,1] (sym $ H[1+n,2,3]≡H[n,2,4] m)

  P[m,n] : ∀ m n → P (suc m) n → (∀ n′ → P m n′) → P (suc m) (suc n)
  P[m,n] m n P[m′,n] P[m,n′] = begin-equality
    3 + ack m (ack (1 + m) n)   ≡⟨ P[m,n′] (ack (1 + m) n) ⟩
    H m 2 (3 + ack (1 + m) n)   ≡⟨ cong (H m 2) $ P[m′,n] ⟩
    H m 2 (H (1 + m) 2 (3 + n)) ≡⟨ sym $ H-rec m 2 (3 + n) ⟩
    H (1 + m) 2 (4 + n)         ∎

iter : (ℕ → ℕ) → ℕ → ℕ
iter f 0       = f 1
iter f (suc n) = f (iter f n)

iter-is-fold : ∀ f n → iter f n ≡ fold (f 1) f n
iter-is-fold f zero    = refl
iter-is-fold f (suc n) = cong f (iter-is-fold f n)

ack-is-fold′ : ∀ m n → ack m n ≡ fold suc iter m n
ack-is-fold′ 0       n       = refl
ack-is-fold′ (suc m) 0       = ack-is-fold′ m 1
ack-is-fold′ (suc m) (suc n) = begin-equality
  ack m (ack (suc m) n)
    ≡⟨ ack-is-fold′ m (ack (suc m) n) ⟩
  fold suc iter m (ack (suc m) n)
    ≡⟨ cong (fold suc iter m) $ ack-is-fold′ (suc m) n ⟩
  fold suc iter m (iter (fold suc iter m) n)
    ∎

ack-is-fold : ∀ m n → ack m n ≡ fold suc (λ f n → fold (f 1) f n) m n
ack-is-fold zero    n       = refl
ack-is-fold (suc m) zero    = ack-is-fold m 1
ack-is-fold (suc m) (suc n) =
 trans (ack-is-fold m (ack (suc m) n))
       (cong (fold suc (λ f n → fold (f 1) f n) m) (ack-is-fold (suc m) n))


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence

module HoTT.Identity.Unit where

open variables

=𝟏-equiv : {x y : 𝟏 {i}} → (x == y) ≃ 𝟏 {j}
=𝟏-equiv {i} {j} {★} {★} = f , qinv→isequiv (g , η , ε)
  where
    f : {x y : 𝟏} → x == y → 𝟏 {j}
    f _ = ★
    g : {x y : 𝟏} → 𝟏 {j} → x == y
    g {★} {★} _ = refl
    η : g ∘ f ~ id
    η refl = refl
    ε : f ∘ g {★} {★} ~ id
    ε ★ = refl

ext: agda

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module Algebra.FreeSemiring where

open import Prelude
open import Algebra

data 𝑅 : Type where
  _+_ : 𝑅 → 𝑅 → 𝑅
  _*_ : 𝑅 → 𝑅 → 𝑅
  1# : 𝑅
  0# : 𝑅

  +-comm : Commutative _+_
  +-assoc : Associative _+_
  *-assoc : Associative _*_
  0+ : Identityˡ _+_ 0#
  +0 : Identityʳ _+_ 0#
  1* : Identityˡ _*_ 1#
  *1 : Identityʳ _*_ 1#
  0* : Zeroˡ _*_ 0#
  *0 : Zeroʳ _*_ 0#
  ⟨+⟩* : _*_ Distributesˡ _+_
  *⟨+⟩ : _*_ Distributesʳ _+_

semiring𝑅 : Semiring ℓzero
semiring𝑅 .Semiring.nearSemiring .NearSemiring.𝑅 = 𝑅
semiring𝑅 .Semiring.nearSemiring .NearSemiring._+_ = _+_
semiring𝑅 .Semiring.nearSemiring .NearSemiring._*_ = _*_
semiring𝑅 .Semiring.nearSemiring .NearSemiring.1# = 1#
semiring𝑅 .Semiring.nearSemiring .NearSemiring.0# = 0#
semiring𝑅 .Semiring.nearSemiring .NearSemiring.+-assoc = +-assoc
semiring𝑅 .Semiring.nearSemiring .NearSemiring.*-assoc = *-assoc
semiring𝑅 .Semiring.nearSemiring .NearSemiring.0+ = 0+
semiring𝑅 .Semiring.nearSemiring .NearSemiring.+0 = +0
semiring𝑅 .Semiring.nearSemiring .NearSemiring.1* = 1*
semiring𝑅 .Semiring.nearSemiring .NearSemiring.*1 = *1
semiring𝑅 .Semiring.nearSemiring .NearSemiring.0* = 0*
semiring𝑅 .Semiring.nearSemiring .NearSemiring.⟨+⟩* = ⟨+⟩*
semiring𝑅 .Semiring.+-comm = +-comm
semiring𝑅 .Semiring.*0 = *0
semiring𝑅 .Semiring.*⟨+⟩ = *⟨+⟩

-- open import Algebra.SemiringLiterals semiring𝑅
-- open import Literals.Number
-- open import Data.Unit.UniversePolymorphic

-- ex : 𝑅
-- ex = 410928

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Agda where

open import Level
import Relation.Binary
import Function.Equality

import Categories.Support.Equivalence
import Categories.Support.SetoidFunctions

open import Categories.Support.PropositionalEquality
open import Categories.Category
open import Categories.Functor using (Functor)

Sets : ∀ o → Category _ _ _
Sets o = record
  { Obj = Set o
  ; _⇒_ = λ d c → d → c
  ; _≡_ = λ f g → ∀ {x} → f x ≣ g x

  ; _∘_ = λ f g x → f (g x)
  ; id = λ x → x

  ; assoc = ≣-refl
  ; identityˡ = ≣-refl
  ; identityʳ = ≣-refl
  ; equiv = record { refl = ≣-refl; sym = s; trans = t }
  ; ∘-resp-≡ = ∘-resp-≡′
  }
  where
  s : {A B : Set o} → {i j : A → B} → ({x : A} → i x ≣ j x) → {x : A} → j x ≣ i x
  s f {x} rewrite f {x} = ≣-refl

  t : {A B : Set o} {i j k : A → B} → ({x : A} → i x ≣ j x) → ({x : A} → j x ≣ k x) → {x : A} → i x ≣ k x
  t f g {x} rewrite f {x} | g {x} = ≣-refl

  ∘-resp-≡′ : {A B C : Set o} {f h : B → C} {g i : A → B} →
             (∀ {x} → f x ≣ h x) →
             (∀ {x} → g x ≣ i x) →
             (∀ {x} → f (g x) ≣ h (i x))
  ∘-resp-≡′ {g = g} f≡h g≡i {x} rewrite f≡h {g x} | g≡i {x} = ≣-refl

-- use standard library setoids here, not our special irrelevant ones
Setoids : ∀ c ℓ → Category (suc (ℓ ⊔ c)) (ℓ ⊔ c) (ℓ ⊔ c)
Setoids c ℓ = record
  { Obj = Setoid c ℓ
  ; _⇒_ = _⟶_
  ; _≡_ = λ {X} {Y} → _≡′_ {X} {Y}
  ; _∘_ = _∘′_
  ; id = id′
  ; assoc = λ {_} {_} {_} {D} → Setoid.refl D
  ; identityˡ = λ {_} {B} → Setoid.refl B
  ; identityʳ = λ {_} {B} → Setoid.refl B
  ; equiv = λ {A} {B} → record
    { refl = Setoid.refl B
    ; sym = λ f → Setoid.sym B f
    ; trans = λ f g → Setoid.trans B f g
    }
  ; ∘-resp-≡ = λ {A} {B} {C} {f} {h} {g} {i} → ∘-resp-≡′ {A} {B} {C} {f} {h} {g} {i}
  }
  where
  infix  4 _≡′_
  open Function.Equality using (_⟨$⟩_; cong; _⟶_) renaming (_∘_ to _∘′_; id to id′)
  open Relation.Binary using (Setoid; module Setoid; Rel)

  _≡′_ : ∀ {X Y} → Rel (X ⟶ Y) _
  _≡′_ {X} {Y} f g = ∀ {x} → Setoid._≈_ Y (f ⟨$⟩ x) (g ⟨$⟩ x)

  .∘-resp-≡′ : ∀ {A B C} {f h : B ⟶ C} {g i : A ⟶ B} → f ≡′ h → g ≡′ i → f ∘′ g ≡′ h ∘′ i
  ∘-resp-≡′ {C = C} {h = h} f≡h g≡i {x} = Setoid.trans C f≡h (cong h g≡i)

-- setoids with irrelevant equality
ISetoids : ∀ c ℓ → Category (suc (ℓ ⊔ c)) (ℓ ⊔ c) (ℓ ⊔ c)
ISetoids c ℓ = record
  { Obj = Setoid c ℓ
  ; _⇒_ = _⟶_
  ; _≡_ = λ {A B} → Setoid._≈_ (A ⇨ B)
  ; _∘_ = _∙_
  ; id = id′
  ; assoc = λ {A B C D} {f g h} →
                cong (h ∙ g ∙ f)
  ; identityˡ = λ {A B f} → cong f
  ; identityʳ = λ {A B f} → cong f
  ; equiv = λ {A B} → Setoid.isEquivalence (A ⇨ B)
  ; ∘-resp-≡ = λ f≡h g≡i x≡y → f≡h (g≡i x≡y)
  }
  where
  open Relation.Binary using (Rel)
  open Categories.Support.Equivalence
  open Categories.Support.SetoidFunctions renaming (id to id′)

Lift-IS : ∀ {c ℓ} a b → Functor (ISetoids c ℓ) (ISetoids (c ⊔ a) (ℓ ⊔ b))
Lift-IS {c} {ℓ} a b = record {
                   F₀ = Lift-setoid {c} {ℓ} {a} {b};
                   F₁ = λ f → record { _⟨$⟩_ = λ x → lift (f ⟨$⟩ (lower x)); cong = λ eq → lift (cong f (lower eq)) };
                   identity = λ x → x;
                   homomorphism = λ {_} {_} {_} {f} {g} eq → lift (cong g (cong f (lower eq)));
                   F-resp-≡ = λ eq₀ eq₁ → lift (eq₀ (lower eq₁)) }
  where
    open import Categories.Support.Equivalence
    open Categories.Support.SetoidFunctions renaming (id to id′)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
--
-- Created by Dependently-Typed Lambda Calculus on 2021-03-18
-- lambe
-- Author: dplaindoux
--

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

module Lambe where

open import Relation.Nullary
     using (yes; no)

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

open import Data.String
     using (String; _≟_)

open import Relation.Binary.PropositionalEquality
     using (_≢_; refl; _≡_)

module Kind where
    {-
    κ =
    | ⋆
    | κ → κ
    | K

    K = {mi:κi}I
    -}

    data t : Set where
      *    : t
      _->_ : t → t → t
      K    : List (String*t) → t

max_stars_repo_name: d-plaindoux/lambe-spec

max_issues_repo_name: d-plaindoux/lambe

max_forks_repo_name: d-plaindoux/lambe


text:
open import Prelude
open import Nat

module List where
  data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

  map : {A B : Set} → (A → B) → (List A) → List B
  map f [] = []
  map f (x :: L) = (f x) :: map f L

  foldr : {A B : Set} → (A → B → B) → B → List A → B
  foldr f b [] = b
  foldr f b (x :: l) = f x (foldr f b l)

  -- list  membership
  data _∈_ {A : Set} : A → List A → Set where
    ∈h : {x : A} {l : List A} → x ∈ (x :: l)
    ∈t : {x y : A} {l : List A} → x ∈ l → x ∈ y :: l

  infixr 99 _::_

  data Unique {A B : Set} (f : A → B) : List A → Set where
    U[] : Unique f []
    U:: : {x : A} {xs : List A}
           → Unique f xs
           → (f x ∈ map f xs → ⊥)
           → Unique f (x :: xs)

  L : List (Nat × Nat)
  L = ((1 , 9) :: (2 , 9) :: [])

  ex1 : Unique π1 L
  ex1 = U:: (U:: U[] notemp) notin
    where
      notemp : {x : Nat} → x ∈ [] → ⊥
      notemp ()

      notin : 1 ∈ (2 :: []) → ⊥
      notin (∈t p) = notemp p

  ex2 : Unique π2 L → ⊥
  ex2 (U:: p x) = x ∈h

  maxl : List Nat → Nat
  maxl = foldr max 0

  -- addmax : {L : List Nat} (p : Unique (\x → x) L) → Unique (\x → x) ((1+ (maxl L)) :: L)
  -- addmax U[] = U:: U[] (λ ())
  -- addmax (U:: p x₁) with addmax p
  -- ... | ih = U:: (U:: p x₁) (λ x → x₁ {!!})


text:
module Playground where

-- Equality type, and its only constructor refl
data _==_ {A : Set} (x : A) : A → Set where
  refl : x == x

-- identity map of a type
id : {A : Set} → A → A
id x = x

-- action on paths
ap : {A B : Set} (f : A → B) {x y : A} → (x == y -> f x == f y)
ap f refl = refl

-- transport
transport : {A : Set} (B : A → Set) {x y : A} (p : x == y) → (B x → B y)
transport _ refl = id

-- Pi types
Π : (A : Set) (P : A → Set) → Set
Π A P = (x : A) → P x

-- Sigma types
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ public

-- empty type
data ⊥ : Set where

-- not operator
¬ : (A : Set) → Set
¬ A = A → ⊥


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

open import Agda.Builtin.Nat

postulate
  _≡_   : {A : Set} → A → A → Set
  refl  : (A : Set) (x : A) → x ≡ x
  cong  : (A B : Set) (x y : A) (f : A → B) (x≡y : x ≡ y) → f x ≡ f y
  subst : (A : Set) (x y : A) (P : A → Set) → x ≡ y → P x → P y

apply : (A : Set) (B : A → Set) → ((x : A) → B x) → ((x : A) → B x)
apply _ _ f x = f x

postulate
  A : Set

record R (f : A → A) : Set where

postulate
  P : (f : A → A) → R f → Set

  _ :
    (f : A → A) (r : R f) →
    P f (subst (A → A) _ f R
           (cong _ _ _ _ (λ f → apply _ _ f 0) (refl _ (λ _ → {!!}))) r)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Boolean.Operators where

open import Data.Boolean

-- Definition of boolean operators with conventions from logic
module Logic where
  infixl 1005 _∧_
  infixl 1004 _∨_ _⊕_
  infixl 1003 _⟵_ _⟷_ _⟶_

  _∧_ : Bool → Bool → Bool
  _∧_ 𝑇 𝑇 = 𝑇
  _∧_ 𝐹 𝑇 = 𝐹
  _∧_ 𝑇 𝐹 = 𝐹
  _∧_ 𝐹 𝐹 = 𝐹

  _∨_ : Bool → Bool → Bool
  _∨_ 𝑇 𝑇 = 𝑇
  _∨_ 𝐹 𝑇 = 𝑇
  _∨_ 𝑇 𝐹 = 𝑇
  _∨_ 𝐹 𝐹 = 𝐹

  open Data.Boolean using () renaming (not to ¬) public

  _⊕_ : Bool → Bool → Bool
  _⊕_ 𝑇 𝑇 = 𝐹
  _⊕_ 𝐹 𝑇 = 𝑇
  _⊕_ 𝑇 𝐹 = 𝑇
  _⊕_ 𝐹 𝐹 = 𝐹

  _⟶_ : Bool → Bool → Bool
  _⟶_ 𝑇 𝑇 = 𝑇
  _⟶_ 𝐹 𝑇 = 𝑇
  _⟶_ 𝑇 𝐹 = 𝐹
  _⟶_ 𝐹 𝐹 = 𝑇

  _⟵_ : Bool → Bool → Bool
  _⟵_ 𝑇 𝑇 = 𝑇
  _⟵_ 𝐹 𝑇 = 𝐹
  _⟵_ 𝑇 𝐹 = 𝑇
  _⟵_ 𝐹 𝐹 = 𝑇

  _⟷_ : Bool → Bool → Bool
  _⟷_ 𝑇 𝑇 = 𝑇
  _⟷_ 𝐹 𝑇 = 𝐹
  _⟷_ 𝑇 𝐹 = 𝐹
  _⟷_ 𝐹 𝐹 = 𝑇

  _⊼_ : Bool → Bool → Bool
  _⊼_ 𝑇 𝑇 = 𝐹
  _⊼_ 𝐹 𝑇 = 𝑇
  _⊼_ 𝑇 𝐹 = 𝑇
  _⊼_ 𝐹 𝐹 = 𝑇

  _⊽_ : Bool → Bool → Bool
  _⊽_ 𝑇 𝑇 = 𝐹
  _⊽_ 𝐹 𝑇 = 𝐹
  _⊽_ 𝑇 𝐹 = 𝐹
  _⊽_ 𝐹 𝐹 = 𝑇

  ⊤ : Bool
  ⊤ = 𝑇

  ⊥ : Bool
  ⊥ = 𝐹

-- Definition of boolean operators with conventions from typical programming languages
module Programming where
  open Logic using () renaming
    (_∧_  to _&&_
    ; _∨_ to _||_
    ; ¬   to !
    ; _⟷_ to _==_
    ; _⊕_ to _!=_
    ; _⟶_ to _→?_
    ; _⟵_ to _←?_
    ) public

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:
-- Andreas, 2017-09-18, issue #2754 reported by nad.
-- Command line options
--
--   --ignore-interfaces -v tc:10
--
-- caused internal error when processing Agda.Primitive.
--
-- Reason: trying to debug print levels while level built-ins
-- are not yet bound.
--
-- Should work now, printing
--
--   .#Lacking_Level_Builtins#
--
-- where levels should be printed.

-- This file is left black intentionally.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists, based on the Kleene star and plus, basic types and operations.
------------------------------------------------------------------------

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

module Data.List.Kleene.Base where

open import Data.Product as Product using (_×_; _,_; map₂; map₁; proj₁; proj₂)
open import Data.Nat     as ℕ       using (ℕ; suc; zero)
open import Data.Maybe   as Maybe   using (Maybe; just; nothing)
open import Data.Sum     as Sum     using (_⊎_; inj₁; inj₂)
open import Level        as Level   using (Level)

open import Algebra.Core using (Op₂)
open import Function.Base

private
  variable
    a b c : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Definitions
--
-- These lists are exactly equivalent to normal lists, except the "cons"
-- case is split into its own data type. This lets us write all the same
-- functions as before, but it has 2 advantages:
--
-- * Some functions are easier to express on the non-empty type. Head,
--   for instance, has a natural safe implementation. Having the
--   non-empty type be defined mutually with the normal type makes the
--   use of this non-empty type occasionally more ergonomic.
-- * It can make some proofs easier. By using the non-empty type where
--   possible, we can avoid an extra pattern match, which can really
--   simplify certain proofs.

infixr 5 _&_ ∹_

record _+ {a} (A : Set a) : Set a
data _* {a} (A : Set a) : Set a

-- Non-Empty Lists
record _+ A where
  inductive
  constructor _&_
  field
    head : A
    tail : A *

-- Possibly Empty Lists
data _* A where
  [] : A *
  ∹_ : A + → A *
open _+ public

------------------------------------------------------------------------
-- Uncons

uncons : A * → Maybe (A +)
uncons []     = nothing
uncons (∹ xs) = just xs

------------------------------------------------------------------------
-- FoldMap

foldMap+ : Op₂ B → (A → B) → A + → B
foldMap+ _∙_ f (x & [])   = f x
foldMap+ _∙_ f (x & ∹ xs) = f x ∙ foldMap+ _∙_ f xs

foldMap* : Op₂ B → B → (A → B) → A * → B
foldMap* _∙_ ε f []     = ε
foldMap* _∙_ ε f (∹ xs) = foldMap+ _∙_ f xs

------------------------------------------------------------------------
-- Folds

module _ (f : A → B → B) (b : B) where
  foldr+ : A + → B
  foldr* : A * → B

  foldr+ (x & xs) = f x (foldr* xs)

  foldr* []     = b
  foldr* (∹ xs) = foldr+ xs

module _ (f : B → A → B) where
  foldl+ : B → A + → B
  foldl* : B → A * → B

  foldl+ b (x & xs) = foldl* (f b x) xs

  foldl* b []     = b
  foldl* b (∹ xs) = foldl+ b xs

------------------------------------------------------------------------
-- Concatenation

module Concat where
  _++++_ : A + → A + → A +
  _+++*_ : A + → A * → A +
  _*+++_ : A * → A + → A +
  _*++*_ : A * → A * → A *

  head (xs +++* ys) = head xs
  tail (xs +++* ys) = tail xs *++* ys

  xs *++* ys = foldr* (λ x zs → ∹ x & zs) ys xs

  xs ++++ ys = foldr+ (λ x zs → x & ∹ zs) ys xs

  []     *+++ ys = ys
  (∹ xs) *+++ ys = xs ++++ ys
open Concat public using () renaming (_++++_ to _+++_; _*++*_ to _++*_)

------------------------------------------------------------------------
-- Mapping

module _  (f : A → B) where
  map+ : A + → B +
  map* : A * → B *

  head (map+ xs) = f (head xs)
  tail (map+ xs) = map* (tail xs)

  map* []     = []
  map* (∹ xs) = ∹ map+ xs

module _ (f : A → Maybe B) where
  mapMaybe+ : A + → B *
  mapMaybe* : A * → B *

  mapMaybe+ (x & xs) with f x
  ... | just y  = ∹ y & mapMaybe* xs
  ... | nothing = mapMaybe* xs

  mapMaybe* []     = []
  mapMaybe* (∹ xs) = mapMaybe+ xs

------------------------------------------------------------------------
-- Applicative Operations

pure+ : A → A +
head (pure+ x) = x
tail (pure+ x) = []

pure* : A → A *
pure* x = ∹ pure+ x

module Apply where
  _*<*>*_ : (A → B) * → A * → B *
  _+<*>*_ : (A → B) + → A * → B *
  _*<*>+_ : (A → B) * → A + → B *
  _+<*>+_ : (A → B) + → A + → B +

  []     *<*>* xs = []
  (∹ fs) *<*>* xs = fs +<*>* xs

  fs +<*>* xs = map* (head fs) xs ++* (tail fs *<*>* xs)

  []     *<*>+ xs = []
  (∹ fs) *<*>+ xs = ∹ fs +<*>+ xs

  fs +<*>+ xs = map+ (head fs) xs Concat.+++* (tail fs *<*>+ xs)
open Apply public using () renaming (_*<*>*_ to _<*>*_; _+<*>+_ to _<*>+_)

------------------------------------------------------------------------
-- Monadic Operations

module Bind where
  _+>>=+_ : A + → (A → B +) → B +
  _+>>=*_ : A + → (A → B *) → B *
  _*>>=+_ : A * → (A → B +) → B *
  _*>>=*_ : A * → (A → B *) → B *

  (x & xs) +>>=+ k = k x Concat.+++* (xs *>>=+ k)

  (x & xs) +>>=* k = k x Concat.*++* (xs *>>=* k)

  []     *>>=* k = []
  (∹ xs) *>>=* k = xs +>>=* k

  []     *>>=+ k = []
  (∹ xs) *>>=+ k = ∹ xs +>>=+ k
open Bind public using () renaming (_*>>=*_ to _>>=*_; _+>>=+_ to _>>=+_)

------------------------------------------------------------------------
-- Scans

module Scanr (f : A → B → B) (b : B) where
  cons : A → B + → B +
  head (cons x xs) = f x (head xs)
  tail (cons x xs) = ∹ xs

  scanr+ : A + → B +
  scanr* : A * → B +

  scanr* = foldr* cons (b & [])
  scanr+ = foldr+ cons (b & [])
open Scanr public using (scanr+; scanr*)

module _ (f : B → A → B) where
  scanl* : B → A * → B +
  head (scanl* b xs)     = b
  tail (scanl* b [])     = []
  tail (scanl* b (∹ xs)) = ∹ scanl* (f b (head xs)) (tail xs)

  scanl+ : B → A + → B +
  head (scanl+ b xs) = b
  tail (scanl+ b xs) = ∹ scanl* (f b (head xs)) (tail xs)

  scanl₁ : B → A + → B +
  scanl₁ b xs = scanl* (f b (head xs)) (tail xs)

------------------------------------------------------------------------
-- Accumulating maps

module _ (f : B → A → (B × C)) where
  mapAccumˡ* : B → A * → (B × C *)
  mapAccumˡ+ : B → A + → (B × C +)

  mapAccumˡ* b []     = b , []
  mapAccumˡ* b (∹ xs) = map₂ ∹_ (mapAccumˡ+ b xs)

  mapAccumˡ+ b (x & xs) =
    let y , ys = f b x
        z , zs = mapAccumˡ* y xs
    in z , ys & zs

module _ (f : A → B → (C × B)) (b : B) where
  mapAccumʳ* : A * → (C * × B)
  mapAccumʳ+ : A + → (C + × B)

  mapAccumʳ* [] = [] , b
  mapAccumʳ* (∹ xs) = map₁ ∹_ (mapAccumʳ+ xs)

  mapAccumʳ+ (x & xs) =
    let ys , y = mapAccumʳ* xs
        zs , z = f x y
    in zs & ys , z

------------------------------------------------------------------------
-- Non-Empty Folds

last : A + → A
last (x & [])   = x
last (_ & ∹ xs) = last xs

module _ (f : A → A → A) where
  foldr₁ : A + → A
  foldr₁ (x & [])   = x
  foldr₁ (x & ∹ xs) = f x (foldr₁ xs)

  foldl₁ : A + → A
  foldl₁ (x & xs) = foldl* f x xs

module _ (f : A → Maybe B → B) where
  foldrMaybe* : A * → Maybe B
  foldrMaybe+ : A + → B

  foldrMaybe* []     = nothing
  foldrMaybe* (∹ xs) = just (foldrMaybe+ xs)

  foldrMaybe+ xs = f (head xs) (foldrMaybe* (tail xs))

------------------------------------------------------------------------
-- Indexing

_[_]* : A * → ℕ → Maybe A
_[_]+ : A + → ℕ → Maybe A

[]     [ _ ]* = nothing
(∹ xs) [ i ]* = xs [ i ]+

xs [ zero  ]+ = just (head xs)
xs [ suc i ]+ = tail xs [ i ]*

applyUpTo* : (ℕ → A) → ℕ → A *
applyUpTo+ : (ℕ → A) → ℕ → A +

applyUpTo* f zero    = []
applyUpTo* f (suc n) = ∹ applyUpTo+ f n

head (applyUpTo+ f n) = f zero
tail (applyUpTo+ f n) = applyUpTo* (f ∘ suc) n

upTo* : ℕ → ℕ *
upTo* = applyUpTo* id

upTo+ : ℕ → ℕ +
upTo+ = applyUpTo+ id

------------------------------------------------------------------------
-- Manipulation

module ZipWith (f : A → B → C) where
  +zipWith+ : A + → B + → C +
  *zipWith+ : A * → B + → C *
  +zipWith* : A + → B * → C *
  *zipWith* : A * → B * → C *

  head (+zipWith+ xs ys) = f (head xs) (head ys)
  tail (+zipWith+ xs ys) = *zipWith* (tail xs) (tail ys)

  *zipWith+ [] ys     = []
  *zipWith+ (∹ xs) ys = ∹ +zipWith+ xs ys

  +zipWith* xs []     = []
  +zipWith* xs (∹ ys) = ∹ +zipWith+ xs ys

  *zipWith* [] ys     = []
  *zipWith* (∹ xs) ys = +zipWith* xs ys
open ZipWith public renaming (+zipWith+ to zipWith+; *zipWith* to zipWith*)

module Unzip (f : A → B × C) where
  cons : B × C → B * × C * → B + × C +
  cons = Product.zip′ _&_ _&_

  unzipWith* : A * → B * × C *
  unzipWith+ : A + → B + × C +

  unzipWith* = foldr* (λ x xs → Product.map ∹_ ∹_ (cons (f x) xs)) ([] , [])

  unzipWith+ xs = cons (f (head xs)) (unzipWith* (tail xs))
open Unzip using (unzipWith+; unzipWith*) public

module Partition (f : A → B ⊎ C) where
  cons : B ⊎ C → B * × C * → B * × C *
  proj₁ (cons (inj₁ x) xs) = ∹ x & proj₁ xs
  proj₂ (cons (inj₁ x) xs) = proj₂ xs
  proj₂ (cons (inj₂ x) xs) = ∹ x & proj₂ xs
  proj₁ (cons (inj₂ x) xs) = proj₁ xs

  partitionSumsWith* : A * → B * × C *
  partitionSumsWith+ : A + → B * × C *

  partitionSumsWith* = foldr* (cons ∘ f) ([] , [])

  partitionSumsWith+ = foldr+ (cons ∘ f) ([] , [])
open Partition using (partitionSumsWith+; partitionSumsWith*) public

tails* : A * → (A +) *
tails+ : A + → (A +) +

head (tails+ xs) = xs
tail (tails+ xs) = tails* (tail xs)

tails* []     = []
tails* (∹ xs) = ∹ tails+ xs

reverse* : A * → A *
reverse* = foldl* (λ xs x → ∹ x & xs) []

reverse+ : A + → A +
reverse+ (x & xs) = foldl* (λ ys y → y & ∹ ys) (x & []) xs


text:
-- TODO: Move these to stuff related to metric spaces

module Derivative where
  open Limit using (Lim ; lim)

  -- Statement that the point x of function f is a differentiable point
  DifferentiablePoint : (ℝ → ℝ) → ℝ → Stmt
  DifferentiablePoint f(p) = Lim(x ↦ ((f(x) − f(p))/(x − p)))(p)

  -- Statement that function f is differentiable
  Differentiable : (ℝ → ℝ) → Stmt
  Differentiable f = ∀{x} → DifferentiablePoint f(x)

  -- Derivative value of function f at point x (if the point is differentiable)
  𝐷 : (f : ℝ → ℝ) → (x : ℝ) → ⦃ _ : DifferentiablePoint f(x) ⦄ → ℝ
  𝐷 _ _ ⦃ l ⦄ = Lim.L(l)

module Proofs where
  instance postulate Differentiable-constant     : ∀{a} → Differentiable(const(a))
  instance postulate Differentiable-id           : Differentiable(id)
  instance postulate Differentiable-monomial     : ∀{a} → Differentiable(x ↦ x ^ a)
  instance postulate Differentiable-[eˣ]         : Differentiable(x ↦ e ^ x)
  instance postulate Differentiable-[⋅]-scalar   : ∀{a} → Differentiable(x ↦ a ⋅ x)
  instance postulate Differentiable-[+]-function : ∀{f g} → ⦃ _ : Differentiable(f) ⦄ → ⦃ _ : Differentiable(g) ⦄ → Differentiable(x ↦ f(x) + g(x))
  instance postulate Differentiable-[−]-function : ∀{f g} → ⦃ _ : Differentiable(f) ⦄ → ⦃ _ : Differentiable(g) ⦄ → Differentiable(x ↦ f(x) − g(x))
  instance postulate Differentiable-[⋅]-function : ∀{f g} → ⦃ _ : Differentiable(f) ⦄ → ⦃ _ : Differentiable(g) ⦄ → Differentiable(x ↦ f(x) ⋅ g(x))
  instance postulate Differentiable-[/]-function : ∀{f g} → ⦃ _ : Differentiable(f) ⦄ → ⦃ _ : Differentiable(g) ⦄ → Differentiable(x ↦ f(x) / g(x))
  instance postulate Differentiable-[∘]-function : ∀{f g} → ⦃ _ : Differentiable(f) ⦄ → ⦃ _ : Differentiable(g) ⦄ → Differentiable(f ∘ g)

  instance postulate [𝐷]-constant     : ∀{a} → ⦃ diff : Differentiable(const(a)) ⦄ → ∀{x} → 𝐷(const(a))(x)⦃ diff ⦄ ≡ a
  instance postulate [𝐷]-id           : ⦃ diff : Differentiable(id) ⦄ → ∀{x} → 𝐷(id)(x)⦃ diff ⦄ ≡ #(1)
  instance postulate [𝐷]-monomial     : ∀{a} → ⦃ diff : Differentiable(x ↦ x ^ a) ⦄ → ∀{x} → 𝐷(x ↦ x ^ a)(x)⦃ diff ⦄ ≡ a ⋅ x ^ (a − #(1))
  instance postulate [𝐷]-[eˣ]         : ⦃ diff : Differentiable(x ↦ e ^ x) ⦄ → ∀{x} → 𝐷(x ↦ e ^ x)(x)⦃ diff ⦄ ≡ e ^ x
  instance postulate [𝐷]-[+]-function : ∀{f g} → ⦃ diff-f : Differentiable(f) ⦄ → ⦃ diff-g : Differentiable(g) ⦄ → ∀{x} → 𝐷(x ↦ f(x) + g(x))(x)⦃ Differentiable-[+]-function ⦃ diff-f ⦄ ⦃ diff-g ⦄ ⦄ ≡ 𝐷(f)(x)⦃ diff-f ⦄ + 𝐷(g)(x)⦃ diff-g ⦄
  instance postulate [𝐷]-[−]-function : ∀{f g} → ⦃ diff-f : Differentiable(f) ⦄ → ⦃ diff-g : Differentiable(g) ⦄ → ∀{x} → 𝐷(x ↦ f(x) − g(x))(x)⦃ Differentiable-[−]-function ⦃ diff-f ⦄ ⦃ diff-g ⦄ ⦄ ≡ 𝐷(f)(x)⦃ diff-f ⦄ − 𝐷(g)(x)⦃ diff-g ⦄
  instance postulate [𝐷]-[⋅]-function : ∀{f g} → ⦃ diff-f : Differentiable(f) ⦄ → ⦃ diff-g : Differentiable(g) ⦄ → ∀{x} → 𝐷(x ↦ f(x) ⋅ g(x))(x)⦃ Differentiable-[⋅]-function ⦃ diff-f ⦄ ⦃ diff-g ⦄ ⦄ ≡ 𝐷(f)(x)⦃ diff-f ⦄ ⋅ g(x) + f(x) ⋅ 𝐷(g)(x)⦃ diff-g ⦄
  instance postulate [𝐷]-[/]-function : ∀{f g} → ⦃ diff-f : Differentiable(f) ⦄ → ⦃ diff-g : Differentiable(g) ⦄ → ∀{x} → 𝐷(x ↦ f(x) / g(x))(x)⦃ Differentiable-[/]-function ⦃ diff-f ⦄ ⦃ diff-g ⦄ ⦄ ≡ (𝐷(f)(x)⦃ diff-f ⦄ ⋅ g(x) − f(x) ⋅ 𝐷(g)(x)⦃ diff-g ⦄)/(g(x) ^ #(2))
  instance postulate [𝐷]-[∘]-function : ∀{f g} → ⦃ diff-f : Differentiable(f) ⦄ → ⦃ diff-g : Differentiable(g) ⦄ → ∀{x} → 𝐷(x ↦ f(g(x)))(x)⦃ Differentiable-[∘]-function ⦃ diff-f ⦄ ⦃ diff-g ⦄ ⦄ ≡ 𝐷(f)(g(x))⦃ diff-f ⦄ ⋅ 𝐷(g)(x)⦃ diff-g ⦄


text:
module Show where

open import Data.Char hiding (show)
open import Data.List
open import Data.String hiding (show)
open import Function

record Show (A : Set) : Set where
  field
    show : A → String

open Show {{...}} public

fromHaskell : {A : Set} → (A → List Char) → Show A
fromHaskell primShow = record { show = fromList ∘ primShow }

max_stars_repo_name: cruhland/agda-editor

max_issues_repo_name: cruhland/agda-editor

max_forks_repo_name: cruhland/agda-editor


text:
{-# OPTIONS --universe-polymorphism #-}

module 13-implicitProofObligations where

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Nat
open import Data.Fin using (Fin; toℕ)
open import Data.Product using (_×_; _,_)
open import Data.Nat.DivMod
open import Relation.Binary.PropositionalEquality
open import Function

postulate
  d : ℕ
  d≢0 : d ≢ 0
--  d≢0' : d ≢ 0

fromWitnessFalse : ∀ {p} {P : Set p} {Q : Dec P} → ¬ P → False Q
fromWitnessFalse {Q = yes p} ¬P = ⊥-elim $ ¬P p
fromWitnessFalse {Q = no ¬p} ¬P = tt

⋯ : {A : Set} → {{v : A}} → A
⋯ {{v}} = v

_divMod′_ : (dividend divisor : ℕ) {{ ≢0 : divisor ≢ 0 }} → ℕ × ℕ
a divMod′ d with _divMod_ a d { fromWitnessFalse ⋯ }
._ divMod′ d | (result q r) = q , toℕ r

_div′_ : (dividend divisor : ℕ) {{ ≢0 : divisor ≢ 0 }} → ℕ
a div′ b with a divMod′ b
a div′ b | (q , _) = q

--Agda can't resolve hiddens
-- test : {d≢0 : False (d ≟ 0)} → ℕ
-- test = 5 div d
-- test2 : {{d≢0 : d ≢ 0}} → ℕ
-- test2 = 5 div′ d

test3 = 5 div 2
test4 = 5 div′ 2
  where nz : 2 ≢ 0
        nz ()

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.ABox.Interp using ( _*_ ; ⌊_⌋ ; ind )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _,_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; on-bnode ; bnodes ; ⊨a-resp-≲ ; ⊨a-resp-≡³ ; _,_ )
open import Web.Semantic.DL.Category.Object using
  ( Object ; IN ; iface )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; BN ; impl ; _≣_ ; _⊑_ ; _,_ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Wiring using ( identity )
open import Web.Semantic.DL.Category.Properties.Composition.Lemmas using
  ( compose-left ; compose-right ; compose-resp-⊨a
  ; identity-intro ; identity-elim )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( ≲-refl )
open import Web.Semantic.Util using
  ( _∘_ ; _⊕_⊕_ ; False ; inode ; bnode ; enode ; left ; right )

module Web.Semantic.DL.Category.Properties.Composition.LeftUnit
  {Σ : Signature} {S T : TBox Σ} where

compose-unit₁ : ∀ {A B : Object S T} (F : A ⇒ B) →
  (identity A ∙ F ≣ F)
compose-unit₁ {A} {B} F = ( idF⊑F , F⊑idF ) where

  idF⊑F : identity A ∙ F ⊑ F
  idF⊑F I I⊨STA I⊨idF = (f , I⊨F) where

    Iˡ⊨id : left * I ⊨a impl (identity A)
    Iˡ⊨id = compose-left (identity A) F I I⊨idF

    Iʳ⊨F : right * I ⊨a impl F
    Iʳ⊨F = compose-right (identity A) F I I⊨idF

    f : BN F → Δ ⌊ I ⌋
    f w = ind I (bnode (enode w))

    f✓ : ∀ x → ⌊ I ⌋ ⊨ ind I (right x) ≈ on-bnode f (ind I) x
    f✓ (inode x) = ≈-sym ⌊ I ⌋ (identity-elim A (left * I) Iˡ⊨id x)
    f✓ (bnode v) = ≈-refl ⌊ I ⌋
    f✓ (enode y) = ≈-refl ⌊ I ⌋

    I⊨F : bnodes I f ⊨a impl F
    I⊨F = ⊨a-resp-≲ (≲-refl ⌊ I ⌋ , f✓) (impl F) Iʳ⊨F

  F⊑idF : F ⊑ identity A ∙ F
  F⊑idF I I⊨STA I⊨F = (f , I⊨idF) where

    f : (False ⊕ IN A ⊕ BN F) → Δ ⌊ I ⌋
    f (inode ())
    f (bnode x) = ind I (inode x)
    f (enode v) = ind I (bnode v)

    Iˡ⊨id : left * bnodes I f ⊨a impl (identity A)
    Iˡ⊨id = identity-intro A (left * bnodes I f) (λ x → ≈-refl ⌊ I ⌋)

    Iʳ⊨F : right * bnodes I f ⊨a impl F
    Iʳ⊨F = ⊨a-resp-≡³ I (on-bnode f (ind I) ∘ right) refl (impl F) I⊨F

    I⊨idF : bnodes I f ⊨a impl (identity A ∙ F)
    I⊨idF = compose-resp-⊨a (identity A) F (bnodes I f) Iˡ⊨id Iʳ⊨F

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


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

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

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Data.Empty            -- ⊥
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; ⊥ to ⊥ᵖ)
-- open import Cubical.Relation.Binary.Base using (PropRel)

-- data ⊥ : Set where
-- ¬_ : ∀{ℓ} → Set ℓ → Set ℓ
-- ¬ A = A → ⊥

inst-¬ : ∀{ℓ} {A : Set ℓ} → (A → ⊥) → {{a : A }} → ⊥
inst-¬ f {{a}} = f a

-- record SquareRootSpace {ℓ ℓ' : Level} : Set (ℓ-suc (ℓ-max ℓ ℓ')) where
--   field
--     X : Set ℓ
--     0ˣ : X
--     _<_ : X → X → Set ℓ'

module TestA {ℓ ℓ'} (X : Set ℓ) (0ˣ : X) (_<_ : X → X → Set ℓ') where

  _≤_ : X → X → Set ℓ'
  a ≤ b = (b < a) → ⊥ -- ¬(b < a)

  _≤ᵢ_ : X → X → Set ℓ'
  a ≤ᵢ b = {{p : b < a}} → ⊥

  -- postulate _≤'_ : X → X → Set ℓ'

  _≤'_ : X → X → Set ℓ'
  abstract a ≤' b = (b < a) → ⊥

  -- field
  postulate
    sqrt  : (x : X) → {{p : (0ˣ ≤ᵢ x)}} → X
    sqrt' : (x : X) → {{p : (0ˣ ≤' x)}} → X

-- module _ {ℓ ℓ'} (SQS : SquareRootSpace {ℓ} {ℓ'}) where
--   open SquareRootSpace SQS
  test1 : (x : X) → (0ˣ ≤ x) → X
  test1 x 0≤x = let instance _ = inst-¬ 0≤x
                in sqrt x -- works!

  -- test2 : (x y z : X) → (0ˣ ≤ x) → (0ˣ ≤ y) → (0ˣ ≤ z) → X
  -- test2 x y z 0≤x 0≤y 0≤z =
  --   let instance 0≤xᵢ : 0ˣ ≤ᵢ x
  --                0≤xᵢ = inst-¬ 0≤x
  --                0≤yᵢ : 0ˣ ≤ᵢ y
  --                0≤yᵢ = inst-¬ 0≤y
  --                0≤zᵢ : 0ˣ ≤ᵢ z
  --                0≤zᵢ = inst-¬ 0≤z
  --   -- Goal: X
  --   -- Have: ⦃ p : 0ˣ ≤ᵢ x ⦄ → X
  --   in sqrt y -- error!

  test3 : (x y z : X) → (0ˣ ≤' x) → (0ˣ ≤' y) → (0ˣ ≤' z) → X
  test3 x y z 0≤x 0≤y 0≤z =
    let instance _ = 0≤x ; _ = 0≤y ; _ = 0≤z
    in sqrt' y -- works!

-- _p_51 : 0ˣ ≤ᵢ y
-- errorFailed to solve the following constraints:
--   Resolve instance argument
--     _p_51
--       : {ℓ = ℓ₁ : Agda.Primitive.Level} {ℓ' = ℓ'' : Agda.Primitive.Level}
--         (X₁ : Set ℓ₁) (0ˣ₁ : X₁) (_<₁_ : X₁ → X₁ → Set ℓ'') (x₁ y₁ z₁ : X₁)
--         (0≤x₁ : 0ˣ₁ ≤ x₁) (0≤y₁ : 0ˣ₁ ≤ y₁) (0≤z₁ : 0ˣ₁ ≤ z₁) →
--         0ˣ₁ ≤ᵢ y₁
--   Candidates
--     λ ⦃ a ⦄ → z a : ⦃ p : 0ˣ _<_ X ⦄ → ⊥
--     λ ⦃ a ⦄ → 0≤x a : ⦃ p : 0ˣ x X ⦄ → ⊥
--     λ ⦃ a ⦄ → 0≤y a : ⦃ p : 0ˣ y X ⦄ → ⊥

-- Instance arguments with explicit arguments are never considered by
-- instance search, so having an instance argument ⦃ p : 0ˣ ≤ x ⦄ has
-- no effect.
-- when checking that the expression ⦃ p : 0ˣ ≤ x ⦄ → X is a type

{- there is an email of Apostolis Xekoukoulotakis from 03.11.17, 11:52

data ⊥ : Set where

infix 3 ¬ᵢ_

¬ᵢ_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ᵢ P = {{p : P}} → ⊥

infix 3 ¬_

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = (p : P) → ⊥

-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

module Lecture2 where

import Basics
open Basics public

-- Definition 2.2.3 define the identity function, and show lambda-abstraction in so doing
id : {i : Level} {A : UU i} → A → A
id = λ a → a -- can also use plain backslash \ instead of lambda (as it resembles lambda?)

-- Definition 2.2.4
comp : {i j k : Level} {A : UU i} {B : UU j} {C : UU k} → (B → C) → ((A → B) → (A → C))
comp = λ g f a → g(f(a)) -- the lambda extends to cover g, f and a
_∘_ : {i j k : Level} {A : UU i} {B : UU j} {C : UU k} → (B → C) → ((A → B) → (A → C))
g ∘ f = comp g f

data ℕ : U where
  Nzero : ℕ
  Nsucc : ℕ → ℕ

add : ℕ → ℕ → ℕ
add Nzero = id
add (Nsucc n) = Nsucc ∘ (add n)

-- try some examples, hit C-c C-n (or whatever "compute normal form" is bound to)
-- and try entering "add (Nsucc Nzero) (Nsucc (Nsucc Nzero))"
-- you should get "Nsucc (Nsucc (Nsucc Nzero))"

_+_ : ℕ → ℕ → ℕ
n + m = add n m

-- Exercise 2.3
const : {i j : Level} (A : UU i) (B : UU j) (b : B) → A → B
const A B b x = b

-- Exercise 2.4
Pi-swap : {i j k : Level} {A : UU i} {B : UU j} {C : A → (B → UU k)} →
  ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
Pi-swap f y x = f x y

-- Exercise 2.5(a)
_**_ : ℕ → (ℕ → ℕ)
Nzero ** n = Nzero
(Nsucc m) ** n = (m ** n) + n

-- Exercise 2.5(b)
_^_ : ℕ → (ℕ → ℕ)
m ^ Nzero = Nsucc Nzero
m ^ (Nsucc n) = m ** (m ^ n)

-- Exercise 2.5(c)
factorial : ℕ → ℕ
factorial Nzero = Nsucc Nzero
factorial (Nsucc m) = (Nsucc m) ** (factorial m)

-- Exercise 2.6(a)
Nmax : ℕ → (ℕ → ℕ)
Nmax Nzero n = n
Nmax (Nsucc m) Nzero = Nsucc m
Nmax (Nsucc m) (Nsucc n) = Nsucc (Nmax m n)

-- Exercise 2.6(b)
Nmin : ℕ → (ℕ → ℕ)
Nmin Nzero n = Nzero
Nmin (Nsucc m) Nzero = Nzero
Nmin (Nsucc m) (Nsucc n) = Nsucc (Nmin m n)

-- Exercise 2.7
-- induction: for any dependent type P over ℕ, define a section of P
-- built out of a term in P 0 and a section of P n → P(Nsucc n)
ind-N : {i : Level} {P : ℕ → UU i} → P Nzero → ((n : ℕ) → P n → P(Nsucc n)) → ((n : ℕ) → P n)
ind-N p0 pS Nzero = p0
ind-N p0 pS (Nsucc n) = pS n (ind-N p0 pS n)


text:
-- 2012-03-15, example by Nisse
module Issue585-11 where

data D₁ : Set where
  d₁ : D₁

f₁ : D₁ → D₁ → D₁
f₁ x d₁ = x

data D₂ : Set where
  d₂ : D₂ → D₂

postulate
  P  : D₁ → Set
  f₂ : ∀ {n₁ n₂} → P n₁ → P n₂ → P (f₁ n₁ n₂)

mutual

  f₃ : D₁ → D₂ → D₁
  f₃ _ (d₂ _) = _

  f₄ : ∀ {n} → P n → (i : D₂) → P (f₃ n i)
  f₄ p (d₂ i) = f₂ p (f₄ p i)

-- This worked until Agda 2.3.0
-- Now, recursive solutions  [here: f₃ n (d₂ i) = f₁ n (f₃ n i)]
-- are no longer found, since termination is not be guaranteed by the occurs check.


text:
-- Andreas, 2014-11-02

record U : Set where
  coinductive
  constructor inn
  field       out : U

f : U → U
f u = {!u!}


text:
module SafeFlagPrimTrustMe where

open import Agda.Builtin.Equality
open import Agda.Builtin.TrustMe

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
open import Agda.Builtin.Bool

open import Issue4166.Import {b = true} as A′

it : ⦃ Bool ⦄ → Bool
it ⦃ b ⦄ = b

b : Bool
b = it

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

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

module Data.List.Relation.Pointwise where

open import Data.List.Relation.Binary.Pointwise public

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


text:
module Thesis.SIRelBigStep.Syntax where

open import Data.Nat

open import Thesis.SIRelBigStep.Types public

data Primitive : (τ : Type) → Set where
  succ : Primitive (nat ⇒ nat)
  add : Primitive (pair nat nat ⇒ nat)

data Const : (τ : Type) → Set where
  lit : (n : ℕ) → Const nat

data Term (Γ : Context) (τ : Type) : Set
-- Source values
data SVal (Γ : Context) : (τ : Type) → Set where
  var : ∀ {τ} →
    (x : Var Γ τ) →
    SVal Γ τ
  abs : ∀ {σ τ}
    (t : Term (σ • Γ) τ) →
    SVal Γ (σ ⇒ τ)
  cons : ∀ {τ1 τ2}
    (sv1 : SVal Γ τ1)
    (sv2 : SVal Γ τ2) →
    SVal Γ (pair τ1 τ2)
  const : ∀ {τ} → (c : Const τ) → SVal Γ τ

data Term (Γ : Context) (τ : Type) where
  val :
    SVal Γ τ →
    Term Γ τ
  primapp : ∀ {σ}
    (p : Primitive (σ ⇒ τ)) →
    (sv : SVal Γ σ) →
    Term Γ τ
  -- we use de Bruijn indices, so we don't need binding occurrences.
  app : ∀ {σ}
    (vs : SVal Γ (σ ⇒ τ)) →
    (vt : SVal Γ σ) →
    Term Γ τ
  lett : ∀ {σ}
    (s : Term Γ σ) →
    (t : Term (σ • Γ) τ) →
    Term Γ τ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Proof where

open import Prelude
open import Lambda
open import Subst
open import Trans
open import Reduction
import Chain

open module C = Chain _≤_ (\x -> refl-≤) (\x y z -> trans-≤)
     renaming (_===_by_ to _<≤>_by_)

data SN {Γ : Ctx}{τ : Type}(t : Term Γ τ) : Set where
  bound : (n : Nat) ->
          ({u : Term Γ τ}(r : t ⟶β* u) -> length r ≤ n) -> SN t

SNˢ : forall {Γ Δ} -> Terms Γ Δ -> Set
SNˢ ts = All² SN ts

-- Let's prove a simple lemma
lem-SN⟶β : {Γ : Ctx}{τ : Type}{t u : Term Γ τ} ->
           SN t -> t ⟶β* u -> SN u
lem-SN⟶β {Γ}{τ}{t}{u}(bound n cap) r = bound n \r' ->
  chain> length r'
     <≤> length r + length r' by lem-≤+L (length r)
     <≤> length (r ▹◃ r')     by refl-≤' (lem-length▹◃ r r')
     <≤> n                    by cap (r ▹◃ r')
  qed

lem-SN-map : {Γ Δ : Ctx}{σ τ : Type}
             (tm : Term Γ σ -> Term Δ τ) ->
             (f  : {t u : Term Γ σ} -> t ⟶β u -> tm t ⟶β tm u)
             {t : Term Γ σ} -> SN (tm t) -> SN t
lem-SN-map tm f (bound n p) = bound n \r ->
  chain> length r
     <≤> length {R = _⟶β_} (map tm f r)
                by refl-≤' (lem-length-map tm f r)
     <≤> n      by p (map tm f r)
  qed

lem-SN•L : {Γ : Ctx}{σ τ : Type}{t : Term Γ (σ ⟶ τ)}{u : Term Γ σ} ->
          SN (t • u) -> SN t
lem-SN•L {u = u} = lem-SN-map (\v -> v • u) •⟶L

lem-SN↑ : {Γ : Ctx}(Δ : Ctx){σ : Type}{t : Term Γ σ} ->
          SN (t ↑ Δ) -> SN t
lem-SN↑ Δ = lem-SN-map (\v -> v ↑ Δ) (↑⟶β Δ)

lem-SN-x : {Γ Δ : Ctx}{σ : Type}(x : Var Γ (Δ ⇒ σ))
           {ts : Terms Γ Δ} -> SNˢ ts -> SN (var x •ˢ ts)
lem-SN-x x ∅²            = bound zero red-var
  where
    red-var : forall {u} -> (r : var x ⟶β* u) -> length r ≤ 0
    red-var ()
lem-SN-x x (_◄²_ {x = t}{xs = ts} snts snt) = {! !}
  where
    sn-xts : SN (var x •ˢ ts)
    sn-xts = lem-SN-x x snts

infix 30 ⟦_⟧ ∋_

⟦_⟧ ∋_ : (τ : Type){Γ : Ctx} -> Term Γ τ -> Set
⟦ ι     ⟧ ∋ t = SN t
⟦ σ ⟶ τ ⟧ ∋ t = forall {Δ}(u : Term (_ ++ Δ) σ) ->
                ⟦ σ ⟧ ∋ u -> ⟦ τ ⟧ ∋ t ↑ Δ • u

mutual

  lem-⟦⟧⊆SN : (σ : Type){Γ : Ctx}{t : Term Γ σ} ->
              ⟦ σ ⟧ ∋ t -> SN t
  lem-⟦⟧⊆SN ι              okt = okt
  lem-⟦⟧⊆SN (σ ⟶ τ) {Γ}{t} okt = lem-SN↑ (ε , σ) sn-t↑
    where
      ih : {Δ : Ctx}{u : Term Δ τ} -> ⟦ τ ⟧ ∋ u -> SN u
      ih = lem-⟦⟧⊆SN τ

      sn• : (Δ : Ctx)(u : Term (Γ ++ Δ) σ) -> ⟦ σ ⟧ ∋ u -> SN (t ↑ Δ • u)
      sn• Δ u h = ih (okt {Δ} u h)

      sn-t↑ : SN (wk t)
      sn-t↑ = lem-SN•L (sn• (ε , σ) vz (lem-⟦⟧ˣ σ vzero ∅²))

  lem-⟦⟧ˣ : (σ : Type){Γ Δ : Ctx}(x : Var Γ (Δ ⇒ σ)){ts : Terms Γ Δ} ->
            SNˢ ts -> ⟦ σ ⟧ ∋ var x •ˢ ts
  lem-⟦⟧ˣ ι       x snts = lem-SN-x x snts
  lem-⟦⟧ˣ (σ ⟶ τ) {Γ}{Δ} x {ts} snts = \u oku -> {! !}
    where
      snts↑ : (Δ : Ctx) -> SNˢ (ts ↑ˢ Δ)
      snts↑ Δ = {! !}

      rem : (Δ : Ctx)(u : Term (Γ ++ Δ) σ) ->
            ⟦ σ ⟧ ∋ u -> ⟦ τ ⟧ ∋ var (x ↑ˣ Δ) •ˢ ts ↑ˢ Δ • u
      rem Δ u oku = lem-⟦⟧ˣ τ (x ↑ˣ Δ) (snts↑ Δ ◄² lem-⟦⟧⊆SN σ oku)

lem-⟦⟧subst : {Γ Δ : Ctx}{τ : Type}(σ : Type)
              {t : Term (Γ , τ) (Δ ⇒ σ)}{u : Term Γ τ}{vs : Terms Γ Δ} ->
              ⟦ σ ⟧ ∋ (t / [ u ]) •ˢ vs -> ⟦ σ ⟧ ∋ (ƛ t) • u •ˢ vs
lem-⟦⟧subst ι         h = {!h !}
lem-⟦⟧subst (σ₁ ⟶ σ₂) h = {! !}


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Profunctor where

open import Level hiding (lift)

open import Categories.Category
open import Categories.Agda
open import Categories.Bifunctor using (Functor; Bifunctor; _∘_)
open import Categories.Functor.Hom
open import Categories.Lan
open import Categories.Yoneda

Profunctor : ∀ {o ℓ e} {o′ ℓ′ e′} → Category o ℓ e → Category o′ ℓ′ e′ → Set _
Profunctor {ℓ = ℓ} {e} {ℓ′ = ℓ′} {e′} C D = Bifunctor (Category.op D) C (ISetoids (ℓ ⊔ ℓ′) (e ⊔ e′))

id : ∀ {o ℓ e} → {C : Category o ℓ e} → Profunctor C C
id {C = C} = Hom[ C ][-,-]

{-
_∘_ : ∀ {o ℓ e} {o′ ℓ′ e′} {o′′ ℓ′′ e′′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o′′ ℓ′′ e′′}
    → Profunctor D E → Profunctor C D → Profunctor C E
F ∘ G = {!!}
-}


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.Typed.Weakening
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Reflexivity
open import Definition.LogicalRelation.Properties.Transitivity
open import Definition.LogicalRelation.Properties.Symmetry
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Conversion

open import Tools.Product
open import Tools.Empty
import Tools.PropositionalEquality as PE

import Data.Fin as Fin
import Data.Nat as Nat

-- Weak head expansion of reducible types.
redSubst* : ∀ {A B r l Γ}
          → Γ ⊢ A ⇒* B ^ r
          → Γ ⊩⟨ l ⟩ B ^ r
          → ∃ λ ([A] : Γ ⊩⟨ l ⟩ A ^ r)
          → Γ ⊩⟨ l ⟩ A ≡ B ^ r / [A]
redSubst* {A = A} D (Uᵣ′ B .(next l′) rU l′ l< PE.refl [[ ⊢A , ⊢B , D' ]]) =
  let ⊢A = redFirst* D
  in  Uᵣ′ A (next l′) rU l′ l< PE.refl [[ ⊢A , ⊢B , D ⇨* D' ]] , D'
redSubst* D (ℕᵣ [[ ⊢B , ⊢ℕ , D′ ]]) =
  let ⊢A = redFirst* D
  in  ℕᵣ ([[ ⊢A , ⊢ℕ , D ⇨* D′ ]]) , D′
redSubst* D (Emptyᵣ [[ ⊢B , ⊢Empty , D′ ]]) =
  let ⊢A = redFirst* D
  in  Emptyᵣ ([[ ⊢A , ⊢Empty , D ⇨* D′ ]]) , D′
redSubst* D (ne′ K [[ ⊢B , ⊢K , D′ ]] neK K≡K) =
  let ⊢A = redFirst* D
  in  (ne′ K [[ ⊢A , ⊢K , D ⇨* D′ ]] neK K≡K)
  ,   (ne₌ _ [[ ⊢B , ⊢K , D′ ]] neK K≡K)
redSubst* D (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢B , ⊢ΠFG , D′ ]] ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢A = redFirst* D
  in  (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢ΠFG , D ⇨* D′ ]] ⊢F ⊢G A≡A [F] [G] G-ext)
  ,   (Π₌ _ _ D′ A≡A (λ ρ ⊢Δ → reflEq ([F] ρ ⊢Δ))
        (λ ρ ⊢Δ [a] → reflEq ([G] ρ ⊢Δ [a])))
redSubst* D (∃ᵣ′ F G [[ ⊢B , ⊢ΠFG , D′ ]] ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢A = redFirst* D
  in  (∃ᵣ′ F G [[ ⊢A , ⊢ΠFG , D ⇨* D′ ]] ⊢F ⊢G A≡A [F] [G] G-ext)
  ,   (∃₌ _ _ D′ A≡A (λ ρ ⊢Δ → reflEq ([F] ρ ⊢Δ))
        (λ ρ ⊢Δ [a] → reflEq ([G] ρ ⊢Δ [a])))
redSubst* {l = ι ¹} D (emb l< X) with redSubst* D X
redSubst* {l = ι ¹} D (emb l< X) | y , y₁ = emb l< y , y₁
redSubst* {l = ∞} D (emb l< X) with redSubst* D X
redSubst* {l = ∞} D (emb ∞< X) | y , y₁ = emb {l′ = ι ¹} ∞< y , y₁

redSubst*Term⁰ : ∀ {A t u ll Γ} → let l = ι ⁰ in
                Γ ⊢ t ⇒* u ∷ A ^ ll
              → ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ll ])
              → Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ll ] / [A]
              → Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ll ] / [A]
              × Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ ! , ll ] / [A]
redSubst*Term⁰ t⇒u (ℕᵣ D) (ℕₜ n [[ ⊢u , ⊢n , d ]] n≡n prop) =
  let A≡ℕ  = subset* (red D)
      ⊢t   = conv (redFirst*Term t⇒u) A≡ℕ
      t⇒u′ = conv* t⇒u A≡ℕ
  in  ℕₜ n [[ ⊢t , ⊢n , t⇒u′ ⇨∷* d ]] n≡n prop
  ,   ℕₜ₌ n n [[ ⊢t , ⊢n , t⇒u′ ⇨∷* d ]] [[ ⊢u , ⊢n , d ]]
          n≡n (reflNatural-prop prop)
redSubst*Term⁰ t⇒u (ne′ K D neK K≡K) (neₜ k [[ ⊢t , ⊢u , d ]] (neNfₜ neK₁ ⊢k k≡k)) =
  let A≡K  = subset* (red D)
      [d]  = [[ ⊢t , ⊢u , d ]]
      [d′] = [[ conv (redFirst*Term t⇒u) A≡K , ⊢u , conv* t⇒u A≡K ⇨∷* d ]]
  in  neₜ k [d′] (neNfₜ neK₁ ⊢k k≡k) , neₜ₌ k k [d′] [d] (neNfₜ₌ neK₁ neK₁ k≡k)
redSubst*Term⁰ {A} {t} {u} {l} {Γ} t⇒u (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                  (Πₜ f [[ ⊢t , ⊢u , d ]] funcF f≡f [f] [f]₁) =
  let A≡ΠFG = subset* (red D)
      t⇒u′  = conv* t⇒u A≡ΠFG
      [d]  = [[ ⊢t , ⊢u , d ]]
      [d′] = [[ conv (redFirst*Term t⇒u) A≡ΠFG , ⊢u , conv* t⇒u A≡ΠFG ⇨∷* d ]]
  in  Πₜ f [d′] funcF f≡f [f] [f]₁
  ,   Πₜ₌ f f [d′] [d] funcF funcF f≡f
          (Πₜ f [d′] funcF f≡f [f] [f]₁)
          (Πₜ f [d] funcF f≡f [f] [f]₁)
          (λ [ρ] ⊢Δ [a] → reflEqTerm ([G] [ρ] ⊢Δ [a]) ([f]₁ [ρ] ⊢Δ [a]))

-- Weak head expansion of reducible terms.
redSubst*Term : ∀ {A t u l ll Γ}
              → Γ ⊢ t ⇒* u ∷ A ^ ll
              → ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ll ])
              → Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ll ] / [A]
              → Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ll ] / [A]
              × Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ ! , ll ] / [A]
redSubst*Term {t = t} {l = ι ¹} {Γ = Γ} t⇒u (Uᵣ′ A .(next ⁰) rU ⁰ l< PE.refl D) (Uₜ K [[ ⊢u , ⊢K , d ]] typeA A≡A [u]) =
  let
    A≡U  = subset* (red D)
    ⊢t   = conv (redFirst*Term t⇒u) A≡U
    t⇒u′ = conv* t⇒u A≡U
    [t] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ → proj₁ (redSubst* {l = ι ⁰} (wkRed* [ρ] ⊢Δ (univ* t⇒u′)) ([u] [ρ] ⊢Δ))
    [t≡u] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ → proj₂ (redSubst* {l = ι ⁰} (wkRed* [ρ] ⊢Δ (univ* t⇒u′)) ([u] [ρ] ⊢Δ))
    [[t]] = Uₜ K [[ ⊢t , ⊢K , t⇒u′ ⇨∷* d ]] typeA A≡A [t]
  in
  ([[t]] , Uₜ₌ [[t]] (Uₜ K [[ ⊢u , ⊢K , d ]] typeA A≡A [u]) A≡A [t≡u])
redSubst*Term {t = t} {l = ∞} {Γ = Γ} t⇒u (Uᵣ′ A .(next ¹) rU ¹ l< PE.refl D) (Uₜ K [[ ⊢u , ⊢K , d ]] typeA A≡A [u]) =
  let
    A≡U  = subset* (red D)
    ⊢t   = conv (redFirst*Term t⇒u) A≡U
    t⇒u′ = conv* t⇒u A≡U
    [t] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ → proj₁ (redSubst* {l = ι ¹} (wkRed* [ρ] ⊢Δ (univ* t⇒u′)) ([u] [ρ] ⊢Δ))
    [t≡u] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ → proj₂ (redSubst* {l = ι ¹} (wkRed* [ρ] ⊢Δ (univ* t⇒u′)) ([u] [ρ] ⊢Δ))
    [[t]] = Uₜ K [[ ⊢t , ⊢K , t⇒u′ ⇨∷* d ]] typeA A≡A [t]
  in
  ([[t]] , Uₜ₌ [[t]] (Uₜ K [[ ⊢u , ⊢K , d ]] typeA A≡A [u]) A≡A [t≡u])
redSubst*Term t⇒u (ℕᵣ D) (ℕₜ n [[ ⊢u , ⊢n , d ]] n≡n prop) =
  let A≡ℕ  = subset* (red D)
      ⊢t   = conv (redFirst*Term t⇒u) A≡ℕ
      t⇒u′ = conv* t⇒u A≡ℕ
  in  ℕₜ n [[ ⊢t , ⊢n , t⇒u′ ⇨∷* d ]] n≡n prop
  ,   ℕₜ₌ n n [[ ⊢t , ⊢n , t⇒u′ ⇨∷* d ]] [[ ⊢u , ⊢n , d ]]
          n≡n (reflNatural-prop prop)
redSubst*Term t⇒u (ne′ K D neK K≡K) (neₜ k [[ ⊢t , ⊢u , d ]] (neNfₜ neK₁ ⊢k k≡k)) =
  let A≡K  = subset* (red D)
      [d]  = [[ ⊢t , ⊢u , d ]]
      [d′] = [[ conv (redFirst*Term t⇒u) A≡K , ⊢u , conv* t⇒u A≡K ⇨∷* d ]]
  in  neₜ k [d′] (neNfₜ neK₁ ⊢k k≡k) , neₜ₌ k k [d′] [d] (neNfₜ₌ neK₁ neK₁ k≡k)
redSubst*Term {A} {t} {u} {l} {Γ} t⇒u (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                  (Πₜ f [[ ⊢t , ⊢u , d ]] funcF f≡f [f] [f]₁) =
  let A≡ΠFG = subset* (red D)
      t⇒u′  = conv* t⇒u A≡ΠFG
      [d]  = [[ ⊢t , ⊢u , d ]]
      [d′] = [[ conv (redFirst*Term t⇒u) A≡ΠFG , ⊢u , conv* t⇒u A≡ΠFG ⇨∷* d ]]
  in  Πₜ f [d′] funcF f≡f [f] [f]₁
  ,   Πₜ₌ f f [d′] [d] funcF funcF f≡f
          (Πₜ f [d′] funcF f≡f [f] [f]₁)
          (Πₜ f [d] funcF f≡f [f] [f]₁)
          (λ [ρ] ⊢Δ [a] → reflEqTerm ([G] [ρ] ⊢Δ [a]) ([f]₁ [ρ] ⊢Δ [a]))
redSubst*Term {l = ι ¹} D (emb l< X) [u] = redSubst*Term D X [u]
redSubst*Term {l = ∞} D (emb l< X) [u] = redSubst*Term D X [u]

-- Weak head expansion of reducible types with single reduction step.
redSubst : ∀ {A B r l Γ}
         → Γ ⊢ A ⇒ B ^ r
         → Γ ⊩⟨ l ⟩ B ^ r
         → ∃ λ ([A] : Γ ⊩⟨ l ⟩ A ^ r)
         → Γ ⊩⟨ l ⟩ A ≡ B ^ r / [A]
redSubst A⇒B [B] = redSubst* (A⇒B ⇨ id (escape [B])) [B]

-- Weak head expansion of reducible terms with single reduction step.
redSubstTerm : ∀ {A t u l ll Γ}
             → Γ ⊢ t ⇒ u ∷ A ^ ll
             → ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ll ])
             → Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ll ] / [A]
             → Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ll ] / [A]
             × Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ ! , ll ] / [A]
redSubstTerm t⇒u [A] [u] = redSubst*Term (t⇒u ⇨ id (escapeTerm [A] [u])) [A] [u]

-- Equalities
redSubst*EqTerm : ∀ {A B t t′ u u′ l ll Γ}
                → Γ ⊢ t ⇒* t′ ∷ A ^ ll
                → Γ ⊢ u ⇒* u′ ∷ B ^ ll
                → ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ll ])
                → ([B] : Γ ⊩⟨ l ⟩ B ^ [ ! , ll ])
                → Γ ⊩⟨ l ⟩ A ≡ B ^ [ ! , ll ] / [A]
                → Γ ⊩⟨ l ⟩ t′ ∷ A ^ [ ! , ll ] / [A]
                → Γ ⊩⟨ l ⟩ u′ ∷ B ^ [ ! , ll ] / [B]
                → Γ ⊩⟨ l ⟩ t′ ≡ u′ ∷ A ^ [ ! , ll ] / [A]
                → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ ! , ll ] / [A]
redSubst*EqTerm D D′ [A] [B] [A≡B] [t′] [u′] [t′≡u′] =
  let
    [t≡t′] = proj₂ (redSubst*Term D [A] [t′])
    [u≡u′:B] = proj₂ (redSubst*Term D′ [B] [u′])
    [u≡u′] = convEqTerm₂ [A] [B] [A≡B] [u≡u′:B]
  in transEqTerm [A] [t≡t′] (transEqTerm [A] [t′≡u′] (symEqTerm [A] [u≡u′]))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
open import Data.String using ( String )
open import Data.List.Primitive using ( #List )
open import Data.Maybe.Primitive using ( #Maybe )
open import Web.URI.Port.Primitive using ( Port? )
open import Web.URI.Scheme.Primitive using ( Scheme? )

module Web.URI.Primitive where
{-# IMPORT Data.Maybe #-}
{-# IMPORT Web.URI.AgdaFFI #-}

data #URI : Set where
  #abs : Scheme? → String → Port? → (#List String) → (#Maybe String) → #URI
  #rel : (#List String) → (#Maybe String) → #URI
{-# COMPILED_DATA #URI Web.URI.AgdaFFI.URI Web.URI.AgdaFFI.Abs Web.URI.AgdaFFI.Rel #-}

postulate #toString : #URI → String
{-# COMPILED #toString Web.URI.AgdaFFI.toString #-}

postulate #fromString : String → (#Maybe #URI)
{-# COMPILED #fromString Web.URI.AgdaFFI.fromString #-}

max_stars_repo_name: agda/agda-web-uri

max_issues_repo_name: agda/agda-web-uri

max_forks_repo_name: agda/agda-web-uri


text:
open import Oscar.Prelude
open import Oscar.Class.IsPrefunctor
open import Oscar.Class.Smap
open import Oscar.Class.Surjection
open import Oscar.Class.Transitivity

module Oscar.Class.Prefunctor where

record Prefunctor 𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂ : Ø ↑̂ (𝔬₁ ∙̂ 𝔯₁ ∙̂ ℓ₁ ∙̂ 𝔬₂ ∙̂ 𝔯₂ ∙̂ ℓ₂) where
  constructor ∁
  field
    {𝔒₁} : Ø 𝔬₁
    _∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁
    _∼̇₁_ : ∀ {x y} → x ∼₁ y → x ∼₁ y → Ø ℓ₁
    _↦₁_ : Transitivity.type _∼₁_
    {𝔒₂} : Ø 𝔬₂
    _∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂
    _∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂
    _↦₂_ : Transitivity.type _∼₂_
    {μ} : Surjection.type 𝔒₁ 𝔒₂
    prefunctor-smap : Smap.type _∼₁_ _∼₂_ μ μ
    ⦃ `IsPrefunctor ⦄ : IsPrefunctor _∼₁_ _∼̇₁_ _↦₁_ _∼₂_ _∼̇₂_ _↦₂_ prefunctor-smap


text:
module Negative5 where

data Funny (A : Set) : Set where
  funny : A -> Funny (Funny A -> A) -> Funny A


text:
module _ where

-- Check that previous clauses reduce in later ones

open import Agda.Builtin.Nat hiding (_==_)

record Σ (A : Set) (B : A → Set) : Set where
  field
    fst : A
    snd : B fst

open Σ

postulate
  T : Nat → Set
  mkT : ∀ n → T n

t5 : Σ Nat T
fst t5 = 5
snd t5 = mkT 5

-- Also with instance projections --

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

record Eq (A : Set) : Set where
  field
    _==_ : A → A → Bool
    reflexive : ∀ x → true ≡ (x == x)

open Eq {{...}}

instance
  EqNat : Eq Nat
  _==_ {{EqNat}} zero    zero    = true
  _==_ {{EqNat}} zero    (suc y) = false
  _==_ {{EqNat}} (suc x) zero    = false
  _==_ {{EqNat}} (suc x) (suc y) = x == y
  reflexive {{EqNat}} zero = refl
  reflexive {{EqNat}} (suc x) rewrite reflexive x = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers represented in binary.
------------------------------------------------------------------------

-- This module aims to create an alternative formulation of ℕ that is
-- still reasonably computationally efficient without having to call out
-- to Haskell.

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

module Data.Nat.Binary.Base where

open import Algebra.Core using (Op₂)
open import Data.Nat.Base as ℕ using (ℕ)
open import Data.Sum.Base using (_⊎_)
open import Function using (_on_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary using (¬_)

------------------------------------------------------------------------
-- Definition

data ℕᵇ : Set where
  zero   : ℕᵇ
  2[1+_] : ℕᵇ → ℕᵇ    -- n → 2*(1+n) = nonzero even numbers
  1+[2_] : ℕᵇ → ℕᵇ    -- n → 1 + 2*n = odd numbers

------------------------------------------------------------------------
-- Ordering relations

infix 4 _<_ _>_ _≤_ _≮_ _≯_ _≰_ _≱_

data _<_ : Rel ℕᵇ 0ℓ  where
  0<even    : ∀ {x} → zero < 2[1+ x ]
  0<odd     : ∀ {x} → zero < 1+[2 x ]
  even<even : ∀ {x y} → x < y → 2[1+ x ] < 2[1+ y ]
  even<odd  : ∀ {x y} → x < y → 2[1+ x ] < 1+[2 y ]
  odd<even  : ∀ {x y} → x < y ⊎ x ≡ y → 1+[2 x ] < 2[1+ y ]
  odd<odd   : ∀ {x y} → x < y → 1+[2 x ] < 1+[2 y ]
  -- In these constructors "even" stands for nonzero even.

_>_ : Rel ℕᵇ 0ℓ
x > y = y < x

_≤_ : Rel ℕᵇ 0ℓ
x ≤ y = x < y ⊎ x ≡ y

_≥_ : Rel ℕᵇ 0ℓ
x ≥ y = y ≤ x

_≮_ : Rel ℕᵇ 0ℓ
x ≮ y = ¬ (x < y)

_≯_ : Rel ℕᵇ 0ℓ
x ≯ y = ¬ (x > y)

_≰_ : Rel ℕᵇ 0ℓ
x ≰ y = ¬ (x ≤ y)

_≱_ : Rel ℕᵇ 0ℓ
x ≱ y = ¬ (x ≥ y)

------------------------------------------------------------------------
-- Basic operations

double : ℕᵇ → ℕᵇ
double zero     = zero
double 2[1+ x ] = 2[1+ 1+[2 x ] ]
double 1+[2 x ] = 2[1+ (double x) ]

suc : ℕᵇ → ℕᵇ
suc zero     =  1+[2 zero ]
suc 2[1+ x ] =  1+[2 (suc x) ]
suc 1+[2 x ] =  2[1+ x ]

pred : ℕᵇ → ℕᵇ
pred zero     = zero
pred 2[1+ x ] = 1+[2 x ]
pred 1+[2 x ] = double x

------------------------------------------------------------------------
-- Addition, multiplication and certain related functions

infixl 6 _+_
infixl 7 _*_

_+_ : Op₂ ℕᵇ
zero     + y        =  y
x        + zero     =  x
2[1+ x ] + 2[1+ y ] =  2[1+ suc (x + y) ]
2[1+ x ] + 1+[2 y ] =  suc 2[1+ (x + y) ]
1+[2 x ] + 2[1+ y ] =  suc 2[1+ (x + y) ]
1+[2 x ] + 1+[2 y ] =  suc 1+[2 (x + y) ]

_*_ : Op₂ ℕᵇ
zero     * _        =  zero
_        * zero     =  zero
2[1+ x ] * 2[1+ y ] =  double 2[1+ x + (y + x * y) ]
2[1+ x ] * 1+[2 y ] =  2[1+ x + y * 2[1+ x ] ]
1+[2 x ] * 2[1+ y ] =  2[1+ y + x * 2[1+ y ] ]
1+[2 x ] * 1+[2 y ] =  1+[2 x + y * 1+[2 x ] ]

------------------------------------------------------------------------
-- Conversion between ℕᵇ and ℕ

toℕ : ℕᵇ → ℕ
toℕ zero     =  0
toℕ 2[1+ x ] =  2 ℕ.* (ℕ.suc (toℕ x))
toℕ 1+[2 x ] =  ℕ.suc (2 ℕ.* (toℕ x))

-- Costs O(n), could be improved using `_/_` and `_%_`
fromℕ : ℕ → ℕᵇ
fromℕ 0         = zero
fromℕ (ℕ.suc n) = suc (fromℕ n)

-- An alternative ordering lifted from ℕ

infix 4 _<ℕ_

_<ℕ_ :  Rel ℕᵇ 0ℓ
_<ℕ_ =  ℕ._<_ on toℕ

------------------------------------------------------------------------
-- Other functions

-- Useful in some termination proofs.
size : ℕᵇ → ℕ
size zero     = 0
size 2[1+ x ] = ℕ.suc (size x)
size 1+[2 x ] = ℕ.suc (size x)

------------------------------------------------------------------------
-- Constants

0ᵇ = zero
1ᵇ = suc 0ᵇ
2ᵇ = suc 1ᵇ
3ᵇ = suc 2ᵇ
4ᵇ = suc 3ᵇ
5ᵇ = suc 4ᵇ
6ᵇ = suc 5ᵇ
7ᵇ = suc 6ᵇ
8ᵇ = suc 7ᵇ
9ᵇ = suc 8ᵇ


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for reasoning with a setoid
------------------------------------------------------------------------

-- Example use:

-- n*0≡0 : ∀ n → n * 0 ≡ 0
-- n*0≡0 zero    = refl
-- n*0≡0 (suc n) = begin
--   suc n * 0 ≈⟨ refl ⟩
--   n * 0 + 0 ≈⟨ ... ⟩
--   n * 0     ≈⟨ n*0≡0 n ⟩
--   0         ∎

-- Module `≡-Reasoning` in `Relation.Binary.PropositionalEquality`
-- is recommended for equational reasoning when the underlying equality is
-- `_≡_`.

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

open import Relation.Binary

module Relation.Binary.Reasoning.Setoid {s₁ s₂} (S : Setoid s₁ s₂) where

open Setoid S

------------------------------------------------------------------------
-- Publicly re-export base contents

open import Relation.Binary.Reasoning.Base.Single _≈_ refl trans public
  renaming (_∼⟨_⟩_ to _≈⟨_⟩_)

infixr 2 _≈˘⟨_⟩_

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


text:
module bee2 where

open import Bee2.Crypto.Belt

open import Data.ByteString.Utf8
open import Data.ByteString.IO
open import Data.String using (toList)
open import Data.Product using (proj₁)
open import IO

-- beltPBKDF : Password → ℕ → Salt → Kek

main = run (writeBinaryFile "pbkdf2" (proj₁ (beltPBKDF (packStrict "zed") 1000 (packStrict "salt"))))


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

module Dodo.Binary.Union where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Data.Sum using (_⊎_; inj₁; inj₂; swap)
open import Relation.Binary using (REL)
-- Local imports
open import Dodo.Binary.Equality

-- # Definitions

infixl 19 _∪₂_

_∪₂_ : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
  → REL A B ℓ₁
  → REL A B ℓ₂
  → REL A B (ℓ₁ ⊔ ℓ₂)
_∪₂_ p q x y = p x y ⊎ q x y

-- # Properties

module _ {a b ℓ : Level} {A : Set a} {B : Set b}
    {R : REL A B ℓ} where

  ∪₂-idem : (R ∪₂ R) ⇔₂ R
  ∪₂-idem = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : (R ∪₂ R) ⊆₂' R
    ⊆-proof _ _ (inj₁ Rxy) = Rxy
    ⊆-proof _ _ (inj₂ Rxy) = Rxy
    ⊇-proof : R ⊆₂' (R ∪₂ R)
    ⊇-proof _ _ = inj₁

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} where

  ∪₂-comm : (P ∪₂ Q) ⇔₂ (Q ∪₂ P)
  ∪₂-comm = ⇔: (λ _ _ → swap) (λ _ _ → swap)

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {P : REL A B ℓ₁}
    {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∪₂-assoc : (P ∪₂ Q) ∪₂ R ⇔₂ P ∪₂ (Q ∪₂ R)
  ∪₂-assoc = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : ((P ∪₂ Q) ∪₂ R) ⊆₂' (P ∪₂ (Q ∪₂ R))
    ⊆-proof _ _ (inj₁ (inj₁ Pxy)) = inj₁ Pxy
    ⊆-proof _ _ (inj₁ (inj₂ Qxy)) = inj₂ (inj₁ Qxy)
    ⊆-proof _ _ (inj₂ Rxy)        = inj₂ (inj₂ Rxy)
    ⊇-proof : (P ∪₂ (Q ∪₂ R)) ⊆₂' ((P ∪₂ Q) ∪₂ R)
    ⊇-proof _ _ (inj₁ Pxy)        = inj₁ (inj₁ Pxy)
    ⊇-proof _ _ (inj₂ (inj₁ Qxy)) = inj₁ (inj₂ Qxy)
    ⊇-proof _ _ (inj₂ (inj₂ Rxy)) = inj₂ Rxy

-- # Operations

-- ## Operations: ⊆₂

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∪₂-combine-⊆₂ : P ⊆₂ Q → R ⊆₂ Q → (P ∪₂ R) ⊆₂ Q
  ∪₂-combine-⊆₂ (⊆: P⊆Q) (⊆: R⊆Q) = ⊆: (λ{x y → λ{(inj₁ Px) → P⊆Q x y Px; (inj₂ Rx) → R⊆Q x y Rx}})

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} where

  ∪₂-introˡ : P ⊆₂ (Q ∪₂ P)
  ∪₂-introˡ = ⊆: λ{_ _ → inj₂}

  ∪₂-introʳ : P ⊆₂ (P ∪₂ Q)
  ∪₂-introʳ = ⊆: λ{_ _ → inj₁}

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∪₂-introˡ-⊆₂ : P ⊆₂ R → P ⊆₂ (Q ∪₂ R)
  ∪₂-introˡ-⊆₂ (⊆: P⊆R) = ⊆: (λ x y Pxy → inj₂ (P⊆R x y Pxy))

  ∪₂-introʳ-⊆₂ : P ⊆₂ Q → P ⊆₂ (Q ∪₂ R)
  ∪₂-introʳ-⊆₂ (⊆: P⊆Q) = ⊆: (λ x y Pxy → inj₁ (P⊆Q x y Pxy))

  ∪₂-elimˡ-⊆₂ : (P ∪₂ Q) ⊆₂ R → Q ⊆₂ R
  ∪₂-elimˡ-⊆₂ (⊆: [P∪Q]⊆R) = ⊆: (λ x y Qxy → [P∪Q]⊆R x y (inj₂ Qxy))

  ∪₂-elimʳ-⊆₂ : (P ∪₂ Q) ⊆₂ R → P ⊆₂ R
  ∪₂-elimʳ-⊆₂ (⊆: [P∪Q]⊆R) = ⊆: (λ x y Pxy → [P∪Q]⊆R x y (inj₁ Pxy))

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∪₂-substˡ-⊆₂ : P ⊆₂ Q → (P ∪₂ R) ⊆₂ (Q ∪₂ R)
  ∪₂-substˡ-⊆₂ (⊆: P⊆Q) = ⊆: (λ{x y → λ{(inj₁ Pxy) → inj₁ (P⊆Q x y Pxy); (inj₂ Rxy) → inj₂ Rxy}})

  ∪₂-substʳ-⊆₂ : P ⊆₂ Q → (R ∪₂ P) ⊆₂ (R ∪₂ Q)
  ∪₂-substʳ-⊆₂ (⊆: P⊆Q) = ⊆: (λ{x y → λ{(inj₁ Rxy) → inj₁ Rxy; (inj₂ Pxy) → inj₂ (P⊆Q x y Pxy)}})

-- ## Operations: ⇔₂

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∪₂-substˡ : P ⇔₂ Q → (P ∪₂ R) ⇔₂ (Q ∪₂ R)
  ∪₂-substˡ = ⇔₂-compose ∪₂-substˡ-⊆₂ ∪₂-substˡ-⊆₂

  ∪₂-substʳ : P ⇔₂ Q → (R ∪₂ P) ⇔₂ (R ∪₂ Q)
  ∪₂-substʳ = ⇔₂-compose ∪₂-substʳ-⊆₂ ∪₂-substʳ-⊆₂

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
postulate
  F : @0 Set → Set

G : @0 Set → Set
G A = F (λ { → A })


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

open import HoTT
open import cohomology.Theory
open import homotopy.PushoutSplit
open import cw.CW

module cw.cohomology.WedgeOfCells {i} (OT : OrdinaryTheory i)
  {n} (⊙skel : ⊙Skeleton {i} (S n)) where

open OrdinaryTheory OT
open import cohomology.Bouquet OT
open import cw.WedgeOfCells (⊙Skeleton.skel ⊙skel)

module _ (m : ℤ) where
  CXₙ/Xₙ₋₁ : Group i
  CXₙ/Xₙ₋₁ = C m ⊙Xₙ/Xₙ₋₁

  CEl-Xₙ/Xₙ₋₁ : Type i
  CEl-Xₙ/Xₙ₋₁ = Group.El CXₙ/Xₙ₋₁

  abstract
    CXₙ/Xₙ₋₁-is-abelian : is-abelian CXₙ/Xₙ₋₁
    CXₙ/Xₙ₋₁-is-abelian = C-is-abelian m ⊙Xₙ/Xₙ₋₁

  CXₙ/Xₙ₋₁-abgroup : AbGroup i
  CXₙ/Xₙ₋₁-abgroup = CXₙ/Xₙ₋₁ , CXₙ/Xₙ₋₁-is-abelian

CXₙ/Xₙ₋₁-diag-β : ⊙has-cells-with-choice 0 ⊙skel i
  → CXₙ/Xₙ₋₁ (ℕ-to-ℤ (S n)) ≃ᴳ Πᴳ (⊙cells-last ⊙skel) (λ _ → C2 0)
CXₙ/Xₙ₋₁-diag-β ac = C-Bouquet-diag (S n) (⊙cells-last ⊙skel) (⊙cells-last-has-choice ⊙skel ac)
                 ∘eᴳ C-emap (ℕ-to-ℤ (S n)) Bouquet-⊙equiv-Xₙ/Xₙ₋₁

abstract
  CXₙ/Xₙ₋₁-≠-is-trivial : ∀ {m} (m≠Sn : m ≠ ℕ-to-ℤ (S n))
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (CXₙ/Xₙ₋₁ m)
  CXₙ/Xₙ₋₁-≠-is-trivial {m} m≠Sn ac =
    iso-preserves'-trivial (C-emap m Bouquet-⊙equiv-Xₙ/Xₙ₋₁) $
      C-Bouquet-≠-is-trivial m (⊙cells-last ⊙skel) (S n) m≠Sn (⊙cells-last-has-choice ⊙skel ac)

  CXₙ/Xₙ₋₁-<-is-trivial : ∀ {m} (m<Sn : m < S n)
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (CXₙ/Xₙ₋₁ (ℕ-to-ℤ m))
  CXₙ/Xₙ₋₁-<-is-trivial m<Sn = CXₙ/Xₙ₋₁-≠-is-trivial (ℕ-to-ℤ-≠ (<-to-≠ m<Sn))

  CXₙ/Xₙ₋₁->-is-trivial : ∀ {m} (m>Sn : S n < m)
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (CXₙ/Xₙ₋₁ (ℕ-to-ℤ m))
  CXₙ/Xₙ₋₁->-is-trivial m>Sn = CXₙ/Xₙ₋₁-≠-is-trivial (≠-inv (ℕ-to-ℤ-≠ (<-to-≠ m>Sn)))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

module Literals.Number where

open import Agda.Builtin.FromNat public

open Number ⦃ ... ⦄ public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module StateSizedIO.Base where

open import Size
open import SizedIO.Base

open import Data.Product

record IOInterfaceˢ  : Set₁ where
  field
    IOStateˢ   :  Set
    Commandˢ   :  IOStateˢ → Set
    Responseˢ  :  (s : IOStateˢ) → (m : Commandˢ s) → Set
    IOnextˢ    :  (s : IOStateˢ) → (m : Commandˢ s) → (Responseˢ s m)
                  → IOStateˢ
open IOInterfaceˢ public

record Interfaceˢ : Set₁ where
 field
  Stateˢ   :  Set
  Methodˢ  :  Stateˢ → Set
  Resultˢ  :  (s : Stateˢ) → (m : Methodˢ s) → Set
  nextˢ    :  (s : Stateˢ) → (m : Methodˢ s) → (Resultˢ s m)
              → Stateˢ
open Interfaceˢ public

{-
module _
 (ioinf   : IOInterface) --  (let C  = Command ioi)  (let R   = Response ioi)
 (objinf  : Interfaceˢ)   {-(let S = Stateˢ oi)-} --(let M  = Methodˢ objinf)    (let Rt  = Resultˢ objinf)
                               -- (let n = nextˢ objinf)
 where
 @BEGIN@IOObject
  record IOObjectˢ (i : Size) (s : Stateˢ objinf) : Set where
    coinductive
    field
 HIDE-END
      method :
        ∀{j : Size< i}
        (m : Methodˢ objinf s) →
        IO ioinf ∞ ( Σ[ r ∈ objinf .Resultˢ s m ]
                     IOObjectˢ j (objinf .nextˢ s m r))
  @END
-}

module _
  (ioinf  : IOInterface)
  (oinf  :  Interfaceˢ)
  where
 record IOObjectˢ (i : Size) (s : oinf .Stateˢ) : Set where
  coinductive
  field
   method :
    ∀{j : Size< i}
     (m : oinf .Methodˢ s) →
     IO ioinf ∞ (Σ[  r ∈ oinf .Resultˢ s m ]
                     IOObjectˢ j (oinf .nextˢ s m r))

module _
  (ioi   : IOInterface) (let C  = Command ioi)  (let R   = Response ioi)
  (oi  : Interfaceˢ)  (let S = Stateˢ oi) (let M  = Methodˢ oi)    (let Rt  = Resultˢ oi)
                                (let n = nextˢ oi)
  where
  record IOObjectˢ- (i : Size) (s : S) : Set where
    coinductive
    field
      method : ∀{j : Size< i} (m : M s) → IO ioi ∞ (Rt s m )

open IOObjectˢ public
open IOObjectˢ- public

module _ (I : IOInterfaceˢ )
         (let S = IOStateˢ I) (let C = Commandˢ I)
         (let R = Responseˢ I) (let n = IOnextˢ I)
           where

  mutual
    record IOˢ (i : Size)  (A : S → Set) (s : S) : Set where
      coinductive
      -- constructor delay
      field
        forceˢ : {j : Size< i} → IOˢ' j A s

    data IOˢ' (i : Size)  (A : S → Set) (s : S) : Set where
      doˢ'      :  (c : C s) (f : (r : R s c) → IOˢ i A (n s c r)) → IOˢ' i A s
      returnˢ'  :  (a : A s) → IOˢ' i A s

    data IOˢ+ (i : Size)  (A : S → Set) (s : S) : Set where
      doˢ' : (c : C s)  (f : (r : R s c) → IOˢ i A (n s c r)) → IOˢ+ i A s

open IOˢ public

delayˢ : {i : Size}{I : IOInterfaceˢ}{A : IOStateˢ I → Set}{s : IOStateˢ I} → IOˢ' I i A s → IOˢ I (↑ i) A s
delayˢ p .forceˢ = p

module _  {I : IOInterfaceˢ }
          (let S = IOStateˢ I) (let C = Commandˢ I)
          (let R = Responseˢ I) (let n = IOnextˢ I)
           where
  returnˢ : ∀{i}{A : S → Set} (s : S) (a : A s) → IOˢ I i A s
  returnˢ s a .forceˢ = returnˢ' a

  -- 2017-04-05: Argument s is hidden now.
  doˢ : ∀{i}{A : S → Set} {s : S} (c : C s)
           (f : (r : R s c) → IOˢ I i A (n s c r))
           → IOˢ I i A s
  doˢ c f .forceˢ = doˢ' c f

  mutual
    fmapˢ : (i : Size) → {A B : S → Set} → (f : (s : S) → A s → B s)
            → (s : S)
            → IOˢ I i A s
            → IOˢ I i B s
    fmapˢ i {A} {B} f s p .forceˢ {j} = fmapˢ' j {A} {B} f s (p .forceˢ {j})

    fmapˢ' : (i : Size) → {A B : S → Set} → (f : (s : S) → A s → B s)
            → (s : S)
            → IOˢ' I i A s
            → IOˢ' I i B s
    fmapˢ' i {A} {B} f s (doˢ' c f₁) = doˢ' c (λ r → fmapˢ i {A} {B} f (IOnextˢ I s c r)  (f₁ r))
    fmapˢ' i {A} {B} f s (returnˢ' a) = returnˢ' (f s a)

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
module Untyped.Abstract where

open import Function

open import Data.String
open import Data.Nat
open import Data.Unit
open import Data.Product
open import Data.List
open import Data.Sum as Sum
open import Data.Maybe
open import Strict

open import Debug.Trace
open import Category.Monad

open import Untyped.Monads

postulate fail : ∀ {a : Set} → a

willneverhappenipromise : ∀ {a : Set} → String → a
willneverhappenipromise m = trace m fail

module _ where

  Var  = ℕ
  Chan = ℕ

  mutual
    record Closure : Set where
      inductive
      constructor ⟨_⊢_⟩
      field
        env  : Env
        body : Exp

    data Val : Set where
      tt    : Val
      nat   : ℕ → Val
      chan  : Chan → Val
      ⟨_,_⟩ : Val → Val → Val -- pairs
      clos  : Closure → Val -- closures

    Env = List Val

    data Exp : Set where
      -- the functional core
      nat     : ℕ → Exp
      var     : Var → Exp
      ƛ       : Exp → Exp
      _·_     : Exp → Exp → Exp

      -- products
      pair    : Exp → Exp → Exp
      letp    : Exp → Exp → Exp

      -- communication
      close   : Exp → Exp
      receive : Exp → Exp
      send    : (ch : Exp) → (v : Exp) → Exp

      -- threading
      fork    : Exp → Exp

  extend  : Val → Env → Env
  extend = _∷_

  unsafeLookup : ∀ {a} → ℕ → List a → a
  unsafeLookup _ [] = willneverhappenipromise "lookup fail"
  unsafeLookup zero (x ∷ xs)    = x
  unsafeLookup (suc n) (x ∷ xs) = unsafeLookup n xs

  unsafeUpdate : ∀ {a} → ℕ → List a → a → List a
  unsafeUpdate n [] a = willneverhappenipromise "update fail"
  unsafeUpdate zero (x ∷ xs) a = a ∷ xs
  unsafeUpdate (suc n) (x ∷ xs) a = x ∷ unsafeUpdate n xs a

  -- Ideally this should be two different dispatch sets
  data Comm : Set where
    -- communication
    send  : Chan → Val → Comm
    recv  : Chan → Comm
    clos  : Chan → Comm

  data Threading : Set where
    -- threading
    fork  : Closure → Threading
    yield : Threading

  Cmd = Comm ⊎ Threading

  ⟦_⟧-comm : Comm → Set
  ⟦ clos x ⟧-comm = ⊤
  ⟦ send x x₁ ⟧-comm = ⊤
  ⟦ recv x ⟧-comm = Val

  ⟦_⟧-thr : Threading → Set
  ⟦ fork x ⟧-thr = Chan
  ⟦ yield ⟧-thr  = ⊤

  ⟦_⟧ : Cmd → Set
  ⟦ inj₁ x ⟧ = ⟦ x ⟧-comm
  ⟦ inj₂ y ⟧ = ⟦ y ⟧-thr

  data Thread : Set where
    thread : Free Cmd ⟦_⟧ Val → Thread

  ThreadPool = List Thread

  Links  = Chan → Chan

  data Blocked : Set where
    blocked : Blocked

  {- Free an expression from its earthly -}
  module _ {m}
    ⦃ m-monad : RawMonad m ⦄
    ⦃ m-read  : MonadReader m Env ⦄
    ⦃ m-res   : MonadResumption m Closure Chan ⦄
    ⦃ m-comm  : MonadComm m Chan Val ⦄
    where

    open M

    {-# NON_TERMINATING #-}
    eval : Exp → m Val
    eval (nat n) = do
      return (nat n)
    eval (var x) = do
      asks (unsafeLookup x)
    eval (ƛ e) = do
      asks (clos ∘ ⟨_⊢ e ⟩)
    eval (f · e) = do
      clos ⟨ env ⊢ body ⟩ ← eval f
        where _ → willneverhappenipromise "not a closure"
      v ← eval e
      local (λ _ → extend v env) (eval body)

    -- products
    eval (pair e₁ e₂) = do
      v₁ ← eval e₁
      v₂ ← eval e₂
      return ⟨ v₁ , v₂ ⟩

    eval (letp b e) = do
      ⟨ v₁ , v₂ ⟩ ← eval b
        where _ → willneverhappenipromise "not a pair"
      local (extend v₂ ∘ extend v₁) $ eval e

    -- communication
    eval (close e) = do
      chan c ← eval e
        where _ → willneverhappenipromise "not a channel to close"
      M.close c
      return tt
    eval (receive e) = do
      chan c ← eval e
        where _ → willneverhappenipromise "not a channel to receive on"
      M.recv c
    eval (send e₁ e₂) = do
      chan c ← eval e₁
        where _ → willneverhappenipromise "not a channel to send on"
      v ← eval e₂
      M.send c v
      return tt

    -- threading
    eval (fork e) = do
      clos cl ← eval e
        where _ → willneverhappenipromise "not a closure to fork"
      c ← M.fork cl
      return (chan c)

  {- Interpreting communication commands -}
  module _ {com}
    ⦃ com-comm  : MonadComm com Chan Val ⦄ where

    communicate : (cmd : Comm) → com ⟦ cmd ⟧-comm
    communicate (Comm.send c v) = M.send c v
    communicate (Comm.recv x)   = M.recv x
    communicate (clos x)        = M.close x

  {- Interpreting threading commands -}
  module _ {thr}
    ⦃ thr-res   : MonadResumption thr Closure Chan ⦄ where

    threading : (cmd : Threading) → thr ⟦ cmd ⟧-thr
    threading (Threading.fork cl) = M.fork cl
    threading Threading.yield     = M.yield

  module _ {cmd}
    ⦃ cmd-comm  : MonadComm cmd Chan Val ⦄
    ⦃ cmd-res   : MonadResumption cmd Closure Chan ⦄ where

    handle : (c : Cmd) → cmd ⟦ c ⟧
    handle = Sum.[ communicate , threading ]

  {- Round robin scheduling -}
  module _ {w : Set} {m}

    ⦃ monad : RawMonad m ⦄
    ⦃ read  : MonadState m (List w) ⦄

    (atomic : w → m ⊤) where

    open M

    {-# NON_TERMINATING #-}
    robin : m ⊤
    robin = do
      (h ∷ tl) ← get
        where [] → return tt
      put tl
      atomic h
      robin


text:
-- Andreas, 2011-05-09
-- {-# OPTIONS -v tc.inj:40 -v tc.meta:30 #-}
module Issue383b where

postulate
  Σ  : (A : Set) → (A → Set) → Set
  U  : Set
  El : U → Set

mutual

  data Ctxt : Set where
    _▻_ : (Γ : Ctxt) → (Env Γ → U) → Ctxt

  Env : Ctxt → Set
  Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (σ γ)

postulate
  Δ : Ctxt
  σ : Env Δ → U
  δ : U → Env (Δ ▻ σ)

data Foo : (Γ : Ctxt) → (U → Env Γ) → Set where
  foo : Foo _ δ

-- WORKS NOW;  OLD COMPLAINT:
-- Agda does not solve or simplify the following constraint. Why? Env
-- is constructor-headed.
--
-- _40 := δ  if  [(Σ (Env Δ) (λ γ → El (σ γ))) =< (Env _39) : Set]


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Level using (0ℓ)

-- This module defines utility functions to help working on proofs.

module LibraBFT.Base.Util where

  -- This is obviously not something that should be used in any legitimate proof.  It's just for
  -- convenience when we want to avoid importing a module with open holes while working on
  -- something else.
  obm-dangerous-magic! : ∀ {ℓ} {A : Set ℓ} → A
  obm-dangerous-magic! {ℓ} {A} = magic
    where postulate magic : A

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; []; _∷_; map)
open import Dipsy.Polarity renaming (pos to +; neg to -)

module Dipsy.Struct
  (FOp : {n : ℕ} (as : Vec Polarity n) (b : Polarity) → Set)
  (SOp : {n : ℕ} (as : Vec Polarity n) (b : Polarity) → Set)
  where

open import Dipsy.Form FOp

mutual
  data Struct : (b : Polarity) → Set where
    ·_· : {b : Polarity} → Form → Struct b
    op  : {n : ℕ} {as : Vec Polarity n} {b : Polarity}
        → SOp as b → Structs as → Struct b

  data Structs : {n : ℕ} (as : Vec Polarity n) → Set where
    []  : Structs []
    _∷_ : {n : ℕ} {a : Polarity} {as : Vec Polarity n}
        → Struct a → Structs as → Structs (a ∷ as)

mutual
  data Context : (b c : Polarity) → Set where
    [] : {b : Polarity} → Context b b
    op : {n : ℕ} {as : Vec Polarity n} {b c : Polarity}
       → SOp as c → (i : Fin n) → Contexts as b i → Context b c

  data Contexts : {n : ℕ} (as : Vec Polarity n) (b : Polarity) (i : Fin n) → Set where
    _<∷_ : {n : ℕ} {b c : Polarity} {as : Vec Polarity n}
         → Context b c → Structs as → Contexts (c ∷ as) b zero
    _∷>_ : {n : ℕ} {a b : Polarity} {as : Vec Polarity n} {i : Fin n}
         → Struct a → Contexts as b i → Contexts (a ∷ as) b (suc i)

max_stars_repo_name: wenkokke/Dipsy

max_issues_repo_name: wenkokke/dipsy

max_forks_repo_name: wenkokke/dipsy


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

open import FT using (FT; ⟦_⟧; _⇛_; _◎_; sym⇛)
open import Equivalences using (_≃_)
open import FT-Nat using (normal; bridge)

equiv2path : {B₁ B₂ : FT} → (⟦ B₁ ⟧ ≃ ⟦ B₂ ⟧) → (B₁ ⇛ B₂)
equiv2path {B₁} {B₂} eq = ((normal B₁) ◎ bridge eq) ◎ (sym⇛ (normal B₂))

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------------
-- Inequalities on partial natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.Inequalities where

open import FOTC.Base

infix 4 _<_ _≮_ _>_ _≯_ _≤_ _≰_ _≥_ _≱_

------------------------------------------------------------------------------
-- The function terms.

postulate
  lt    : D → D → D
  lt-00 : lt zero zero                   ≡ false
  lt-0S : ∀ n → lt zero (succ₁ n)        ≡ true
  lt-S0 : ∀ n → lt (succ₁ n) zero        ≡ false
  lt-SS : ∀ m n → lt (succ₁ m) (succ₁ n) ≡ lt m n
{-# ATP axioms lt-00 lt-0S lt-S0 lt-SS #-}

le : D → D → D
le m n = lt m (succ₁ n)
{-# ATP definition le #-}

gt : D → D → D
gt m n = lt n m
{-# ATP definition gt #-}

ge : D → D → D
ge m n = le n m
{-# ATP definition ge #-}

------------------------------------------------------------------------
-- The relations.

_<_ : D → D → Set
m < n = lt m n ≡ true
{-# ATP definition _<_ #-}

_≮_ : D → D → Set
m ≮ n = lt m n ≡ false
{-# ATP definition _≮_ #-}

_>_ : D → D → Set
m > n = gt m n ≡ true
{-# ATP definition _>_ #-}

_≯_ : D → D → Set
m ≯ n = gt m n ≡ false
{-# ATP definition _≯_ #-}

_≤_  : D → D → Set
m ≤ n = le m n ≡ true
{-# ATP definition _≤_ #-}

_≰_  : D → D → Set
m ≰ n = le m n ≡ false
{-# ATP definition _≰_ #-}

_≥_ : D → D → Set
m ≥ n = ge m n ≡ true
{-# ATP definition _≥_ #-}

_≱_ : D → D → Set
m ≱ n = ge m n ≡ false
{-# ATP definition _≱_ #-}

------------------------------------------------------------------------------
-- The lexicographical order.
Lexi : D → D → D → D → Set
Lexi m n m' n' = m < m' ∨ m ≡ m' ∧ n < n'
{-# ATP definition Lexi #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Cubical.Algebra.Group
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Relation.Binary

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties
open import Cubical.DStructures.Meta.Isomorphism
open import Cubical.DStructures.Structures.XModule

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓ≅A ℓA' ℓ≅A' ℓB ℓB' ℓ≅B' ℓ≅B ℓC ℓ≅C ℓ≅ᴰ ℓP : Level

{-
  Goals of the project:
  - define strict 2-groups
  - define crossed modules
  - prove their equivalence
  - do something with the classifying space
    perspective on groups

  Problems:
  - performance
  - the maps going back and forth were fine,
    but the identity types stating that these maps
    are inverse to each other were too complex

  How did we solve this?
  - Copatterns
  - Ulrik's idea: displayed univalent reflexive graphs
    - Provide a fiberwise characterization of the identity types
      of a type family to obtain a characterization of the
      identity types of the total space
    - Avoid equality on objects in proofs
    - Modular and abstract
-}

-- DEFINITION
-- - URG structure
-- - alternative constructors

record URGStr' (A : Type ℓA) (ℓ≅A : Level) : Type (ℓ-max ℓA (ℓ-suc ℓ≅A)) where
  no-eta-equality
  constructor urgstr'

  field
    _≅_ : Rel A A ℓ≅A
    ρ : isRefl _≅_
    uni : isUnivalent _≅_ ρ

-- substituted version
record URGStr'' (A : Type ℓA) (ℓ≅A : Level) : Type (ℓ-max ℓA (ℓ-suc ℓ≅A)) where
  field
    -- a binary relation
    _≅_ : A → A → Type ℓ≅A
    -- a witness of reflexivity
    ρ : (a : A) → a ≅ a
  -- these two fields induce a map that turns
  -- a path into a proof the endpoints are related
  ≡→≅ : {a a' : A} → a ≡ a' → a ≅ a'
  ≡→≅ {a} {a'} p = subst (λ z → a ≅ z) p (ρ a)
  field
    -- that natural map is a fiberwise equivalence
    uni : (a a' : A) → isEquiv (≡→≅ {a} {a'})

  -- alternatively, we could ask for any fiberwise equivalence
  uni' = (a a' : A) → (a ≡ a') ≃ (a ≅ a')
  -- another alternative: all ≅-singletons should be contractible
  contrRelSingl' = (a : A) → isContr (Σ[ a' ∈ A ] (a ≅ a'))

  -- We can prove that these are equivalent:
  -- uni ↔ uni' ↔ contrRelSingl'

  -- This gives rise to alternative constructors for URGs:

make-𝒮' : {A : Type ℓA}
         {_≅_ : Rel A A ℓ≅A}
         (ρ : isRefl _≅_)
         (contrTotal : contrRelSingl _≅_)
         → URGStr A ℓ≅A
make-𝒮' {_≅_ = _≅_} ρ contrTotal =
  urgstr _≅_
         ρ
         (contrRelSingl→isUnivalent _≅_ ρ contrTotal)

-- EXAMPLES
-- - groups
-- - univalent categories
-- - observational equality on ℕ
-- - universe
-- - identity types

-- The SIP for groups produces a URG structure on the type of groups
𝒮-group' : (ℓ : Level) → URGStr (Group {ℓ}) ℓ
𝒮-group' ℓ .URGStr._≅_ = GroupEquiv
𝒮-group' ℓ .URGStr.ρ = idGroupEquiv
𝒮-group' ℓ .URGStr.uni =
  isUnivalent'→isUnivalent GroupEquiv
                            idGroupEquiv
                            λ G H → invEquiv (GroupPath G H)

-- Every univalent Category induces a URG on its type of objects
open import Cubical.Categories.Category renaming (isUnivalent to isUnivalentCat)
Cat→𝒮 : (𝒞 : Precategory ℓ ℓ')
         → (uni : isUnivalentCat 𝒞)
         → URGStr (𝒞 .ob) ℓ'
Cat→𝒮 𝒞 uni
  = urgstr (CatIso {𝒞 = 𝒞})
           idCatIso
           λ x y → isUnivalentCat.univ uni x y

-- observational equality on ℕ
ℕ-≅ : ℕ → ℕ → Type ℓ-zero
ℕ-≅ 0 0 = Unit
ℕ-≅ 0 (suc _) = ⊥
ℕ-≅ (suc _) 0 = ⊥
ℕ-≅ (suc n) (suc m) = ℕ-≅ n m
-- observational equality on ℕ is a URG
𝒮-Nat' : URGStr ℕ ℓ-zero
𝒮-Nat' = {!!}
  where
    import Cubical.DStructures.Structures.Nat using (𝒮-Nat)

-- equivalences determine a URG on any universe
𝒮-universe : URGStr (Type ℓ) ℓ
𝒮-universe
  = make-𝒮 {_≅_ = _≃_}
            idEquiv
            λ A → isContrRespectEquiv (Σ-cong-equiv-snd (λ A' → isoToEquiv (equivInv A' A)))
                                       (equivContr' A)
  where
    module _ (A : Type ℓ) where
      equivInv : (A' : Type ℓ) → Iso (A ≃ A') (A' ≃ A)
      Iso.fun (equivInv A') = invEquiv
      Iso.inv (equivInv A') = invEquiv
      Iso.leftInv (equivInv A') = λ e → equivEq (invEquiv (invEquiv e)) e (funExt (λ x → refl))
      Iso.rightInv (equivInv A') = λ e → equivEq (invEquiv (invEquiv e)) e (funExt (λ x → refl))
      equivContr' : isContr (Σ[ A' ∈ Type ℓ ] A' ≃ A)
      equivContr' = EquivContr A

-- trivially, a type is a URGStr with the relation given by its identity types
𝒮-type : (A : Type ℓ) → URGStr A ℓ
𝒮-type A = make-𝒮 {_≅_ = _≡_}
                  (λ _ → refl)
                  isContrSingl

-- THEOREM:
-- uniqueness of small URGs

𝒮-uniqueness' : (A : Type ℓA) → isContr (URGStr A ℓA)
𝒮-uniqueness' = {!!}
  where
    import Cubical.DStructures.Structures.Type using (𝒮-uniqueness)

-- DEFINITION
-- - displayed URG

record URGStrᴰ' {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
                (B : A → Type ℓB) (ℓ≅ᴰ : Level) : Type (ℓ-max (ℓ-max (ℓ-max ℓA ℓB) ℓ≅A) (ℓ-suc ℓ≅ᴰ)) where
  no-eta-equality
  constructor urgstrᴰ'
  open URGStr 𝒮-A

  field
    _≅ᴰ⟨_⟩_ : {a a' : A} → B a → a ≅ a' → B a' → Type ℓ≅ᴰ
    ρᴰ : {a : A} → isRefl _≅ᴰ⟨ ρ a ⟩_
    uniᴰ : {a : A} → isUnivalent _≅ᴰ⟨ ρ a ⟩_ ρᴰ

  -- Of course, this also has the alternative constructor make-𝒮ᴰ
  -- using that the uniᴰ field follows from
  uniᴰ' = {a : A} → (b : B a) → isContr (Σ[ b' ∈ B a ] b ≅ᴰ⟨ ρ a ⟩ b')

-- EXAMPLE
-- - pointedness displayed over the universe
𝒮ᴰ-pointed : {ℓ : Level} → URGStrᴰ (𝒮-universe {ℓ}) (λ A → A) ℓ
𝒮ᴰ-pointed {ℓ} =
  make-𝒮ᴰ (λ a e b → equivFun e a ≡ b)
          (λ _ → refl)
          p
          where
            p : (A : Type ℓ) (a : A) → isContr (Σ[ b ∈ A ] a ≡ b)
            p _ a = isContrSingl a

-- THEOREM
-- Every DURG on a type family B induces
-- a URG on the total space Σ[ a ∈ A ] B a

∫⟨_⟩'_ : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
        {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
        → URGStr (Σ A B) (ℓ-max ℓ≅A ℓ≅B)
∫⟨_⟩'_ = {!!}

{-
  B   ∫
  |   ↦   A × B
  A
-}

-- EXAMPLE
-- A characterization of the identity types of pointed types
𝒮-pointed : {ℓ : Level} → URGStr (Σ[ A ∈ Type ℓ ] A) ℓ
𝒮-pointed = ∫⟨ 𝒮-universe ⟩ 𝒮ᴰ-pointed

-- EXAMPLE
-- - constant DURG
-- - URG product
-- - URG structure on pairs of groups

𝒮ᴰ-const : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
           {B : Type ℓB} (𝒮-B : URGStr B ℓ≅B)
           → URGStrᴰ 𝒮-A (λ _ → B) ℓ≅B
𝒮ᴰ-const {A = A} 𝒮-A {B} 𝒮-B
  = urgstrᴰ (λ b _ b' → b ≅ b') ρ uni
    where
      open URGStr 𝒮-B

_×𝒮_ : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
        {B : Type ℓB} (𝒮-B : URGStr B ℓ≅B)
        → URGStr (A × B) (ℓ-max ℓ≅A ℓ≅B)
_×𝒮_ 𝒮-A 𝒮-B = ∫⟨ 𝒮-A ⟩ (𝒮ᴰ-const 𝒮-A 𝒮-B)

{-
        const   B    ∫
  A, B   ↦     |    ↦ A × B
                A
-}

-- EXAMPLE
-- Group Homomorphisms displayed over pairs of groups

𝒮ᴰ-G²\F' : URGStrᴰ (𝒮-group' ℓ ×𝒮 𝒮-group' ℓ')
                  (λ (G , H) → GroupHom G H)
                  (ℓ-max ℓ ℓ')
𝒮ᴰ-G²\F' =
    make-𝒮ᴰ (λ {(G , H)} {(G' , H')} f (eG , eH) f'
               → (g : ⟨ G ⟩)
               → GroupEquiv.eq eH .fst ((f .fun) g) ≡ (f' .fun) (GroupEquiv.eq eG .fst g))
            (λ _ _ → refl)
            λ (G , H) f → isContrRespectEquiv (Σ-cong-equiv-snd (λ f' → isoToEquiv (invIso (GroupMorphismExtIso f f'))))
                                              (isContrSingl f)
    where open GroupHom

{-
The displayed relation is defined as

  f ≅⟨ eG , eH ⟩ f = commutativity of

         f
   G --------> H
   |           |
eG |           | eH
   |           |
   G'--------> H'
        f'

Reflexivity is trivial

Univalence follows from contractibility of
Σ[ (f' , _) ∈ GroupHom G H ] (f ∼ f')
for all (f , _) ∈ GroupHom G H
-}

{-
  Overview of Crossed Modules and Strict 2-Groups

  Definition: Crossed module
    - group action α of G₀ on H
    - homomorphism φ : H → G₀
    - equivariance condition
      (g : G₀) → (h : H) → φ (g α h) ≡ g + (φ h) - g
    - peiffer condition
      (h h' : ⟨ H ⟩) → (φ h) α h' ≡ h + h' - h

  Definition: Strict 2-Group
    - internal category in the category of groups
    This means
    - split mono ι with two retractions
      ι : G₀ ↔ G : σ τ₁
    - vertical composition operation which satisfies the interchange law
      _∘⟨_⟩_ : (g f : G₁) → isComposable g f → G₁
    - equivalent to type of vertical compositions on internal reflexive graph: PFG
      (a b :  G₁) → ι(σ b) + a - ι(τ a) - ι(σ b) + b + ι(τ a) ≡ b + a

  Produce this tree of displayed structures:

  PFXM                    PFG     VertComp
  |                       |      /
  |                       |     /
  isEquivar               isSecRet
  |                       |
  |                       |
  B                       B
  |                       |
  |                       |
  isAction                isSecRet
  |                       |
  |                       |
  LAS       F      B      F×B
  \         |      |      /
    \       |      |    /
      \     |      /   /
        \   |     /  /
            Grp
            |
            |
             Grp

use the next result to display propositions like isAction, isEquivariant and isSecRet
-}

-- THEOREM
-- Subtypes have a simple DURG structure given by 𝟙
-- This makes it easy to impose axioms on a structure
Subtype→Sub-𝒮ᴰ : {A : Type ℓA}
                 → (P : A → hProp ℓP)
                 → (𝒮-A : URGStr A ℓ≅A)
                 → URGStrᴰ 𝒮-A (λ a → P a .fst) ℓ-zero
Subtype→Sub-𝒮ᴰ P 𝒮-A =
  make-𝒮ᴰ (λ _ _ _ → Unit)
          (λ _ → tt)
          (λ a p → isContrRespectEquiv (invEquiv (Σ-contractSnd (λ _ → isContrUnit)))
                                        (inhProp→isContr p (P a .snd)))

-- EXAMPLE
-- isAction axioms on pairs of groups together with a left action structure
module _ (ℓ ℓ' : Level) where
  ℓℓ' = ℓ-max ℓ ℓ'

  open import Cubical.DStructures.Structures.Action
  𝒮ᴰ-G²Las\Action' : URGStrᴰ (𝒮-G²Las ℓ ℓ')
                     (λ ((G , H) , _α_) → IsGroupAction G H _α_)
                     ℓ-zero
  𝒮ᴰ-G²Las\Action' = Subtype→Sub-𝒮ᴰ (λ ((G , H) , _α_) → IsGroupAction G H _α_ , isPropIsGroupAction G H _α_)
                                    (𝒮-G²Las ℓ ℓ')
  𝒮-G²LasAction' : URGStr (Action ℓ ℓ') (ℓ-max ℓ ℓ')
  𝒮-G²LasAction' = ∫⟨ 𝒮-G²Las ℓ ℓ' ⟩ 𝒮ᴰ-G²Las\Action'

{-
-- THEOREM
-- DURGs can be lifted to be displayed over the total space of
-- another DURG on the same base URG

                 B
                 |
  B   C   Lift   C
   \ /     ↦    |
    A            A
-}

VerticalLift-𝒮ᴰ' : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
                   {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                   {C : A → Type ℓC} (𝒮ᴰ-C : URGStrᴰ 𝒮-A C ℓ≅C)
                   → URGStrᴰ (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-C) (λ (a , _) → B a) ℓ≅B
VerticalLift-𝒮ᴰ' {ℓ≅B = ℓ≅B} 𝒮-A {B = B} 𝒮ᴰ-B 𝒮ᴰ-C =
  urgstrᴰ (λ b (pA , _) b' → b ≅ᴰ⟨ pA ⟩ b')
          ρᴰ
          uniᴰ
  where open URGStrᴰ 𝒮ᴰ-B

{-
-- THEOREM
-- A tower of two DURGs can be reassociated

   C
   |
   B  split  B × C
   |   ↦      |
   A           A
(but C depends on B)

-}
splitTotal-𝒮ᴰ' : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
                {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                {C : Σ A B → Type ℓC} (𝒮ᴰ-C : URGStrᴰ (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B) C ℓ≅C)
                → URGStrᴰ 𝒮-A
                          (λ a → Σ[ b ∈ B a ] C (a , b))
                          (ℓ-max ℓ≅B ℓ≅C)
splitTotal-𝒮ᴰ' {A = A} 𝒮-A {B} 𝒮ᴰ-B {C} 𝒮ᴰ-C
  = make-𝒮ᴰ (λ (b , c) eA (b' , c') → Σ[ eB ∈ b B≅ᴰ⟨ eA ⟩ b' ] c ≅ᴰ⟨ eA , eB ⟩ c')
            (λ (b , c) → Bρᴰ b , ρᴰ c)
            {!!}
  where
    open URGStrᴰ 𝒮ᴰ-C
    open URGStr 𝒮-A
    _B≅ᴰ⟨_⟩_ = URGStrᴰ._≅ᴰ⟨_⟩_ 𝒮ᴰ-B
    Bρᴰ = URGStrᴰ.ρᴰ 𝒮ᴰ-B
    Buniᴰ = URGStrᴰ.uniᴰ 𝒮ᴰ-B

{-
-- THEOREM
-- two DURGs over the same URGs can be combined

                 B
                 |
  B   C   Lift   C   split  B × C
   \ /     ↦    |     ↦     |
    A            A           A
-}
combine-𝒮ᴰ' : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
             {B : A → Type ℓB} {C : A → Type ℓC}
             (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
             (𝒮ᴰ-C : URGStrᴰ 𝒮-A C ℓ≅C)
             → URGStrᴰ 𝒮-A (λ a → B a × C a) (ℓ-max ℓ≅B ℓ≅C)
combine-𝒮ᴰ' {𝒮-A = 𝒮-A} 𝒮ᴰ-B 𝒮ᴰ-C = splitTotal-𝒮ᴰ 𝒮-A 𝒮ᴰ-B (VerticalLift-𝒮ᴰ 𝒮-A 𝒮ᴰ-C 𝒮ᴰ-B)

-- REMARK: DURG is equivalent to URG + morphism of URG via fibrant replacement

module _ (C : Type ℓ) where
  dispTypeIso :  Iso (C → Type ℓ) (Σ[ X ∈ Type ℓ ] (X → C))
  Iso.fun dispTypeIso D = (Σ[ c ∈ C ] D c) , fst
  Iso.inv dispTypeIso (X , F) c = Σ[ x ∈ X ] F x ≡ c
  Iso.leftInv dispTypeIso = {!!}
  Iso.rightInv dispTypeIso = {!!}

-- → combine is pullback in the (∞,1)-topos of DURGs

{-
With these operations we can construct the entire tree, but how
to get equivalences?

  PFXM                    PFG     VertComp
  |                       |      /
  |                       |     /
  isEquivar               isSecRet
  |                       |
  |                       |
  B                       B
  |                       |
  |                       |
  isAction                isSecRet
  |                       |
  |                       |
  LAS       F      B      F×B
  \         |      |      /
    \       |      |    /
      \     |      /   /
        \   |     /  /
            Grp
            |
            |
            Grp

-- For URGs: relational isomorphisms
-}

record RelIso' {A : Type ℓA} (_≅_ : Rel A A ℓ≅A)
              {A' : Type ℓA'} (_≅'_ : Rel A' A' ℓ≅A') : Type (ℓ-max (ℓ-max ℓA ℓA') (ℓ-max ℓ≅A ℓ≅A')) where
  constructor reliso'
  field
    fun : A → A'
    inv : A' → A
    rightInv : (a' : A') → fun (inv a') ≅' a'
    leftInv : (a : A) → inv (fun a) ≅ a

RelIso→Iso' : {A : Type ℓA} {A' : Type ℓA'}
             (_≅_ : Rel A A ℓ≅A) (_≅'_ : Rel A' A' ℓ≅A')
             {ρ : isRefl _≅_} {ρ' : isRefl _≅'_}
             (uni : isUnivalent _≅_ ρ) (uni' : isUnivalent _≅'_ ρ')
             (f : RelIso _≅_ _≅'_)
             → Iso A A'
Iso.fun (RelIso→Iso' _ _ _ _ f) = RelIso.fun f
Iso.inv (RelIso→Iso' _ _ _ _ f) = RelIso.inv f
Iso.rightInv (RelIso→Iso' _ _≅'_ {ρ' = ρ'} _ uni' f) a'
  = invEquiv (≡→R _≅'_ ρ' , uni' (RelIso.fun f (RelIso.inv f a')) a') .fst (RelIso.rightInv f a')
Iso.leftInv (RelIso→Iso' _≅_ _ {ρ = ρ} uni _ f) a
  = invEquiv (≡→R _≅_ ρ , uni (RelIso.inv f (RelIso.fun f a)) a) .fst (RelIso.leftInv f a)

{-
  For DURGs:
  pull back one of the DURGs
  along an equivalence and show that
  there is a fiberwise relational isomorphism
  between B and f*B'

  B   f*B' B'
  |  /     |
  | /      |
  A   ≃   A'
      f
-}

𝒮ᴰ-*-Iso-Over→TotalIso : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
                         {A' : Type ℓA'} {𝒮-A' : URGStr A' ℓ≅A'}
                         (ℱ : Iso A A')
                         {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                         {B' : A' → Type ℓB'} (𝒮ᴰ-B' : URGStrᴰ 𝒮-A' B' ℓ≅B')
                         (𝒢 : 𝒮ᴰ-♭PIso (Iso.fun ℱ) 𝒮ᴰ-B 𝒮ᴰ-B')
                         → Iso (Σ A B) (Σ A' B')
𝒮ᴰ-*-Iso-Over→TotalIso  ℱ 𝒮ᴰ-B 𝒮ᴰ-B' 𝒢
  = RelFiberIsoOver→Iso ℱ
                        (𝒮ᴰ→relFamily 𝒮ᴰ-B) (𝒮ᴰ-B .uniᴰ)
                        (𝒮ᴰ→relFamily 𝒮ᴰ-B') (𝒮ᴰ-B' .uniᴰ)
                        𝒢
  where open URGStrᴰ

{-
  Let's apply this machinery to our tower of DURGs.
-}

import Cubical.DStructures.Equivalences.GroupSplitEpiAction
import Cubical.DStructures.Equivalences.PreXModReflGraph
import Cubical.DStructures.Equivalences.XModPeifferGraph
import Cubical.DStructures.Equivalences.PeifferGraphS2G

{-
DISCUSSION
- alternate definition of URGs
- how to layer the cake
- uniformity, abstraction, no equality on objects,
  results transferrable across proof assistants
  and type theories
- unlike displayed categories not limited to
  1-truncated types and type families
- easy to set up
- associates the other way compared to SNS
- every SNS gives DURG on the URG of the universe (not implemented)

OTHER THINGS WE DID
- Define (n,k)-groups
- Display homomorphisms of (n,k)-groups over pairs of such groups
- prove the equivalence of (0,1)-groups and axiomatic groups via EM-spaces

FUTURE WORK
- construct more operations
- use reflection to automate steps
- construct URG on the type of URG or even DURG structures
  - meta-theory
  - model of type theory
- more higher group theory ...
-}

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical