text:
module Haskell.Prim.List where

open import Agda.Builtin.List public
open import Agda.Builtin.Nat

open import Haskell.Prim
open import Haskell.Prim.Tuple
open import Haskell.Prim.Bool
open import Haskell.Prim.Int

--------------------------------------------------
-- List

map : (a → b) → List a → List b
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

infixr 5 _++_
_++_ : ∀ {ℓ} {a : Set ℓ} → List a → List a → List a
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys

filter : (a → Bool) → List a → List a
filter p []       = []
filter p (x ∷ xs) = if p x then x ∷ filter p xs else filter p xs

scanl : (b → a → b) → b → List a → List b
scanl f z []       = z ∷ []
scanl f z (x ∷ xs) = z ∷ scanl f (f z x) xs

scanr : (a → b → b) → b → List a → List b
scanr f z [] = z ∷ []
scanr f z (x ∷ xs) =
  case scanr f z xs of λ where
    []         → [] -- impossible
    qs@(q ∷ _) → f x q ∷ qs

scanl1 : (a → a → a) → List a → List a
scanl1 f []       = []
scanl1 f (x ∷ xs) = scanl f x xs

scanr1 : (a → a → a) → List a → List a
scanr1 f []       = []
scanr1 f (x ∷ []) = x ∷ []
scanr1 f (x ∷ xs) =
  case scanr1 f xs of λ where
    []         → [] -- impossible
    qs@(q ∷ _) → f x q ∷ qs

takeWhile : (a → Bool) → List a → List a
takeWhile p [] = []
takeWhile p (x ∷ xs) = if p x then x ∷ takeWhile p xs else []

dropWhile : (a → Bool) → List a → List a
dropWhile p [] = []
dropWhile p (x ∷ xs) = if p x then dropWhile p xs else x ∷ xs

span : (a → Bool) → List a → List a × List a
span p [] = [] , []
span p (x ∷ xs) = if p x then first (x ∷_) (span p xs)
                         else ([] , x ∷ xs)

break : (a → Bool) → List a → List a × List a
break p = span (not ∘ p)

zipWith : (a → b → c) → List a → List b → List c
zipWith f []       _        = []
zipWith f _        []       = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

zip : List a → List b → List (a × b)
zip = zipWith _,_

zipWith3 : (a → b → c → d) → List a → List b → List c → List d
zipWith3 f []       _        _        = []
zipWith3 f _        []       _        = []
zipWith3 f _        _        []       = []
zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs

zip3 : List a → List b → List c → List (a × b × c)
zip3 = zipWith3 _,_,_

unzip : List (a × b) → List a × List b
unzip []              = [] , []
unzip ((x , y) ∷ xys) = (x ∷_) *** (y ∷_) $ unzip xys

unzip3 : List (a × b × c) → List a × List b × List c
unzip3 []                   = [] , [] , []
unzip3 ((x , y , z) ∷ xyzs) =
  case unzip3 xyzs of λ where
    (xs , ys , zs) → x ∷ xs , y ∷ ys , z ∷ zs

takeNat : Nat → List a → List a
takeNat n       [] = []
takeNat zero    xs = []
takeNat (suc n) (x ∷ xs) = x ∷ takeNat n xs

take : (n : Int) → ⦃ IsNonNegativeInt n ⦄ → List a → List a
take n xs = takeNat (intToNat n) xs

dropNat : Nat → List a → List a
dropNat n       [] = []
dropNat zero    xs = xs
dropNat (suc n) (_ ∷ xs) = dropNat n xs

drop : (n : Int) → ⦃ IsNonNegativeInt n ⦄ → List a → List a
drop n xs = dropNat (intToNat n) xs

splitAtNat : (n : Nat) → List a → List a × List a
splitAtNat _       []       = [] , []
splitAtNat 0       xs       = [] , xs
splitAtNat (suc n) (x ∷ xs) = first (x ∷_) (splitAtNat n xs)

splitAt : (n : Int) → ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a
splitAt n xs = splitAtNat (intToNat n) xs

head : (xs : List a) → ⦃ NonEmpty xs ⦄ → a
head (x ∷ _) = x

tail : (xs : List a) → ⦃ NonEmpty xs ⦄ → List a
tail (_ ∷ xs) = xs

last : (xs : List a) → ⦃ NonEmpty xs ⦄ → a
last (x ∷ [])         = x
last (_ ∷ xs@(_ ∷ _)) = last xs

init : (xs : List a) → ⦃ NonEmpty xs ⦄ → List a
init (x ∷ [])         = []
init (x ∷ xs@(_ ∷ _)) = x ∷ init xs


text:
module Type.Properties.Homotopy.Proofs where

import      Data.Tuple as Tuple
open import Functional
open import Function.Axioms
open import Logic
open import Logic.Classical
open import Logic.Predicate
open import Logic.Propositional
import      Lvl
open import Numeral.Natural
open import Type
open import Type.Dependent
open import Type.Properties.Homotopy
open import Type.Properties.MereProposition
open import Type.Properties.Singleton
open import Type.Properties.Singleton.Proofs
open import Structure.Function.Domain
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Structure.Type.Identity
open import Syntax.Function
open import Syntax.Transitivity

private variable ℓ ℓₑ ℓₑₑ ℓₚ ℓ₁ ℓ₂ : Lvl.Level
private variable n : ℕ

module _ {ℓ} ⦃ equiv : ∀{T : Type{ℓ}} → Equiv{ℓ}(T) ⦄ where
  private variable T : Type{ℓ}
  {-
  private open module EquivEquiv{T} = Equiv(equiv{T}) using () renaming (_≡_ to _≡ₑ_)
  module _ ⦃ identElim : ∀{ℓ}{T : Type{ℓ}} → IdentityEliminator(_≡ₑ_ {T = T}) ⦄ where
    constant-endofunction-existence-on-equivalence-is-hset : ∀{x y : T} → ∃{Obj = (x ≡ y) → (x ≡ y)}(Constant) → HomotopyLevel(2)(T)
    HomotopyLevel.proof (constant-endofunction-existence-on-equivalence-is-hset ([∃]-intro const)) {x = x} {y} {xy₁} {xy₂} = {!!} where
      equivalence-endofunction-invertibleₗ : ∀{f : ∀{x y : T} → (x ≡ y) → (x ≡ y)} → (∀{x y : T} → Invertibleₗ(f{x}{y}))
      ∃.witness (equivalence-endofunction-invertibleₗ {T = T}{f = f} {x}{y}) xy =
        xy 🝖 symmetry(_≡ₑ_) (f(reflexivity _))
      Tuple.left (∃.proof equivalence-endofunction-invertibleₗ) = {!!}
      Inverseₗ.proof (Tuple.right (∃.proof (equivalence-endofunction-invertibleₗ {T = T}{f = f} {x}{y}))) {xy} = idElim(_≡ₑ_) ⦃ inst = identElim{T = T} ⦄ (xy ↦ (f(xy) 🝖 symmetry(_≡ₑ_) (f(reflexivity(_≡ₑ_))) ≡ₑ xy)) {!!} xy
  -}

  HomotopyLevel-zero-step-is-one : (∀{x y : T} → HomotopyLevel(0)(x ≡ y)) → HomotopyLevel(1)(T)
  HomotopyLevel.proof (HomotopyLevel-zero-step-is-one p) {x}{y} = Σ.left(HomotopyLevel.proof(p{x}{y}))

  HomotopyLevel-step-is-successor : (∀{x y : T} → HomotopyLevel(n)(x ≡ y)) → HomotopyLevel(𝐒(n))(T)
  HomotopyLevel-step-is-successor {n = 𝟎}      = HomotopyLevel-zero-step-is-one
  HomotopyLevel-step-is-successor {n = 𝐒(n)} p = intro(\{x}{y} → HomotopyLevel.proof(p{x}{y}))

module _
  ⦃ equiv : ∀{ℓ}{T : Type{ℓ}} → Equiv{ℓ}(T) ⦄
  ⦃ funcExt : ∀{ℓ₁ ℓ₂}{T : Type{ℓ₁}}{P : T → Stmt{ℓ₂}} → DependentImplicitFunctionExtensionality(T)(P) ⦄
  ⦃ prop-eq : ∀{ℓ}{T : Type{ℓ}}{x y : T} → MereProposition(x ≡ y) ⦄
  where

  private variable T : Type{ℓ}

  HomotopyLevel-prop₊ : MereProposition(Names.HomotopyLevel(𝐒(n))(T))
  HomotopyLevel-prop₊ {𝟎}    = prop-universal ⦃ prop-p = prop-universal ⦃ prop-p = prop-eq ⦄ ⦄
  HomotopyLevel-prop₊ {𝐒(n)} = prop-universal ⦃ prop-p = prop-universal ⦃ prop-p = HomotopyLevel-prop₊ {n} ⦄ ⦄

  module _
    (base₁ : ∀{ℓ}{A : Type{ℓ}} → HomotopyLevel(1)(A) → HomotopyLevel(2)(A))
    where

    HomotopyLevel-one-is-zero-step : HomotopyLevel(1)(T) → (∀{x y : T} → HomotopyLevel(0)(x ≡ y))
    HomotopyLevel.proof(HomotopyLevel-one-is-zero-step h1 {x} {y}) = intro (HomotopyLevel.proof h1) (HomotopyLevel.proof(base₁ h1))

    HomotopyLevel-successor-step : HomotopyLevel(𝐒(n))(T) → (∀{x y : T} → HomotopyLevel(n)(x ≡ y))
    HomotopyLevel-successor-step {n = 𝟎}      = HomotopyLevel-one-is-zero-step
    HomotopyLevel-successor-step {n = 𝐒(n)} p = intro(HomotopyLevel.proof p)

    HomotopyLevel-successor : HomotopyLevel(n)(T) → HomotopyLevel(𝐒(n))(T)
    HomotopyLevel-successor {n = 0}       h0   = MereProposition.uniqueness(unit-is-prop ⦃ proof = intro (Σ.left h0) (Σ.right h0) ⦄)
    HomotopyLevel-successor {n = 1}            = base₁
    HomotopyLevel-successor {n = 𝐒(𝐒(n))} hssn = HomotopyLevel-successor {n = 𝐒(n)} hssn

{-
    {- TODO: The zero case needs assumptions about the sigma type because it is not a mere proposition unless both A and equality are mere propositions. So first, prove if equality on the sigma type depends only on its components, and its types are mere propositions, then the sigma type is a mere proposition. Secondly, one can use that proof here
    HomotopyLevel-prop : MereProposition(HomotopyLevel(n)(A))
    HomotopyLevel-prop {𝟎} = intro {!!}
    HomotopyLevel-prop {𝐒 n} = {!!}
    -}

{-
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ equiv-equiv : Equiv{ℓₑ}(Equiv._≡_ equiv) ⦄ where
    -- TODO: ComputablyDecidable → UIP (https://homotopytypetheory.org/2012/03/30/a-direct-proof-of-hedbergs-theorem/)
    -- TODO: http://www.cse.chalmers.se/~nad/listings/equality/Equality.Decidable-UIP.html
  classical-to-uip : (∀{x y : T} → ((x ≡ y) ∨ (x ≢ y))) → UniqueIdentityProofs(T)
  MereProposition.uniqueness (classical-to-uip {T = T} dec {x} {y}) {xy₁} {xy₂} = {!p xy₁!} where
    {-
    p : ∀{x y : T} → (x ≡ y) → Stmt
    p {x}{y} eq with dec{x}{x} | dec{x}{y}
    ... | [∨]-introₗ xx  | [∨]-introₗ xy  = eq ≡ transitivity(_≡_) xx xy
    ... | [∨]-introₗ xx  | [∨]-introᵣ nxy with () ← nxy eq
    ... | [∨]-introᵣ nxx | [∨]-introₗ _   with () ← nxx [≡]-intro
    -}

    dec-eq : ∀{x y} → (x ≡ y) → (x ≡ y)
    dec-eq {x}{y} eq with dec{x}{y}
    ... | [∨]-introₗ xy  = xy
    ... | [∨]-introᵣ nxy with () ← nxy eq

    dec-eq-unique : ∀{x y}{xy₁ xy₂ : x ≡ y} → (dec-eq xy₁ ≡ dec-eq xy₂)
    dec-eq-unique {x}{y} {xy₁} with dec{x}{y}
    ... | [∨]-introₗ _   = ?
    ... | [∨]-introᵣ nxy with () ← nxy xy₁

    dec-eq-unit : ∀{x y}{eq : x ≡ y} → (eq ≡ dec-eq eq)
    dec-eq-unit  {x}{y}{eq} with dec{y}{y} | dec{x}{y}
    ... | [∨]-introₗ yy | [∨]-introₗ xy = {!!}
    ... | [∨]-introₗ yy | [∨]-introᵣ x₂ = {!!}
    ... | [∨]-introᵣ x₁ | [∨]-introₗ x₂ = {!!}
    ... | [∨]-introᵣ x₁ | [∨]-introᵣ x₂ = {!!}

{-    p : ∀{x y : T} → (xy : x ≡ y) → (xy ≡ dec-eq(xy))
    p {x}{y} [≡]-intro with dec{x}{x} | dec{x}{y}
    ... | [∨]-introₗ a | [∨]-introₗ x₁ = {![≡]-intro!}
    ... | [∨]-introₗ a | [∨]-introᵣ x₁ = {!!}
    ... | [∨]-introᵣ a | [∨]-introₗ x₁ = {!!}
    ... | [∨]-introᵣ a | [∨]-introᵣ x₁ = {!!}
-}
-}
-}

ext: agda

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:
--
-- Created by Dependently-Typed Lambda Calculus on 2019-05-15
-- records
-- Author: ice10
--

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

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

-- | Bisimulation as equality
record _==_ (x : List A) (y : List A) : Set where
  coinductive
  field
    refl-head : head x ≡ head y
    refl-tail : tail x == tail y
open _==_

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_name: dubinsky/intellij-dtlc


text:
-- This module introduces implicit arguments.

module Implicit where

-- In Agda you can omit things that the type checker can figure out for itself.
-- This is a crucial feature in a monomorphic language, since you would
-- otherwise be overwhelmed by type arguments.

-- Let's revisit the identity function from 'Introduction.Basics'.

id' : (A : Set) -> A -> A
id' A x = x

-- Since Agda is monomorphic we have to take the type A as an argument. So when
-- using the identity function we have to provide the type explicitly.

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

one : Nat
one = id' Nat (suc zero)

-- Always having to provide the type argument to the identity function would of
-- course be very tedious, and seemingly unnecessary. We would expect the type
-- checker to be able to figure out what it should be by looking at the second
-- argument. And indeed the type checker can do this.

-- One way of indicating that the type checker will have figure something out
-- for itself is to write an underscore (_) instead of the term. So when
-- applying the identity function we can write

two : Nat
two = id' _ (suc one)

-- Now the type checker will try to figure out what the _ should be, and in
-- this case it will have no problems doing so. If it should fail to infer the
-- value of an _ it will issue an error message.

-- In the case of the identity function we expect the type argument to always
-- be inferrable so it would be nice if we could avoid having to write the _.
-- This can be achieved by declaring the first argument as an implicit
-- argument.

id : {A : Set} -> A -> A        -- implicit arguments are enclosed in curly braces
id x = x  -- now we don't have to mention A in the left-hand side

three : Nat
three = id (suc two)

-- If, for some reason, an implicit argument cannot be inferred it can be given
-- explicitly by enclosing it in curly braces :

four : Nat
four = id {Nat} (suc three)

-- To summarise we give a bunch of possible variants of the identity function
-- and its use.

-- Various definitions of the identity function. Definitions 0 through 3 are
-- all equivalent, as are definitions 4 through 6.

id0 : (A : Set) -> A -> A
id0 A x = x

id1 : (A : Set) -> A -> A
id1 _ x = x     -- in left-hand sides _ means "don't care"

id2 : (A : Set) -> A -> A
id2 = \A x -> x

id3 = \(A : Set)(x : A) -> x  -- the type signature can be omitted for definitions
                          -- of the form x = e if the type of e can be
                          -- inferred.

id4 : {A : Set} -> A -> A
id4 x = x

id5 : {A : Set} -> A -> A
id5 {A} x = x

id6 : {A : Set} -> A -> A
id6 = \x -> x

id7 = \{A : Set}(x : A) -> x

id8 : {A : Set} -> A -> A
id8 = \{A} x -> x        -- this doesn't work since the type checker assumes
                            -- that the implicit A has been has been omitted in
                            -- the left-hand side (as in id6).

-- Various uses of the identity function.
zero0 = id0 Nat zero
zero1 = id0 _   zero  -- in right-hand sides _ means "go figure"

zero2 = id4       zero
zero3 = id4 {Nat} zero
zero4 = id4 {_}   zero  -- This is equivalent to zero2, but it can be useful if
                        -- a function has two implicit arguments and you need
                        -- to provide the second one (when you provide an
                        -- implicit argument explicitly it is assumed to be the
                        -- left-most one).

-- In this module we have looked at implicit arguments as a substitute for
-- polymorphism. The implicit argument mechanism is more general than that and
-- not limited to inferring the values of type arguments. For more information
-- on implicit arguments see, for instance
--  'Introduction.Data.ByRecursion'

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------------
-- FOTC looping (error) combinator
------------------------------------------------------------------------------

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

module FOTC.Base.Loop where

open import FOTC.Base

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

postulate error : D

-- Conversion rule
--
-- The equation error-eq adds anything to the logic (because
-- reflexivity is already an axiom of equality), therefore we won't
-- add this equation as a first-order logic axiom.
--
-- postulate error-eq : error ≡ error

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Categories.Category

module Categories.Functor.Hom.Properties {o ℓ e} (C : Category o ℓ e) where

open import Categories.Functor.Hom.Properties.Covariant C public
open import Categories.Functor.Hom.Properties.Contra C public

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --safe #-}
module Cubical.Data.FinData.DepFinVec where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ; zero; suc; _+_; _·_; +-assoc)

open import Cubical.Data.FinData.Base
open import Cubical.Data.FinData.Properties

private
  variable
    ℓ ℓ' : Level

{-

  WARNING : If someone use dependent vector in a general case.
            One always think about the following definition.
            Yet because of the definition one to add (toℕ k).
            Which is going to introduce a lot of issues.
            One may consider depVec rather than depFinVec to avoid this issue?
-}

depFinVec : ((n : ℕ) → Type ℓ) → (m : ℕ) → Type ℓ
depFinVec G m = (k : Fin m) → G (toℕ k)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
open import homotopy.WedgeExtension

module homotopy.Pi2HSusp where

module Pi2HSusp {i} {X : Ptd i}
  {{_ : has-level 1 (de⊙ X)}}
  {{_ : is-connected 0 (de⊙ X)}}
  (H-X : HSS X) where

  {- TODO this belongs somewhere else, but where? -}
  private
    Type=-ext : ∀ {i} {A B : Type i} (p q : A == B)
      → (coe p ∼ coe q) → p == q
    Type=-ext p q α =
      ! (ua-η p)
      ∙ ap ua (Subtype=-out is-equiv-prop (λ= α))
      ∙ ua-η q

  module μ = ConnectedHSpace H-X
  μ = μ.μ
  private
    A = de⊙ X
    e = pt X

  back : south == north
  back = ! (merid e)

  private
    P : Susp A → Type i
    P x = Trunc 1 (north == x)

  module Codes = SuspRec A A (λ a → ua (μ.r-equiv a))

  Codes : Susp A → Type i
  Codes = Codes.f

  Codes-level : (x : Susp A) → has-level 1 (Codes x)
  Codes-level = Susp-elim ⟨⟩ ⟨⟩
    (λ _ → prop-has-all-paths-↓)

  encode'₀ : {x : Susp A} → (north == x) → Codes x
  encode'₀ α = transport Codes α e

  encode' : {x : Susp A} → P x → Codes x
  encode' {x} = Trunc-rec {{Codes-level x}} encode'₀

  import homotopy.SuspAdjointLoop as SAL
  η : A → north == north
  η = fst (SAL.η X)

  decodeN' : A → P north
  decodeN' = [_] ∘ η

  abstract
    transport-Codes-mer : (a a' : A)
      → transport Codes (merid a) a' == μ a a'
    transport-Codes-mer a a' =
      coe (ap Codes (merid a)) a'
        =⟨ Codes.merid-β a |in-ctx (λ w → coe w a') ⟩
      coe (ua (μ.r-equiv a)) a'
        =⟨ coe-β (μ.r-equiv a) a' ⟩
      μ a a' ∎

    transport-Codes-mer-e-! : (a : A)
      → transport Codes back a == a
    transport-Codes-mer-e-! a =
      coe (ap Codes back) a
        =⟨ ap-! Codes (merid e) |in-ctx (λ w → coe w a) ⟩
      coe (! (ap Codes (merid e))) a
        =⟨ Codes.merid-β e |in-ctx (λ w → coe (! w) a) ⟩
      coe (! (ua (μ.r-equiv e))) a
        =⟨ Type=-ext (ua (μ.r-equiv e)) idp (λ x → coe-β _ x ∙ μ.unit-l x)
          |in-ctx (λ w → coe (! w) a) ⟩
      coe (! idp) a ∎

  abstract
    encode'-decodeN' : (a : A) → encode' (decodeN' a) == a
    encode'-decodeN' a =
      transport Codes (merid a ∙ back) e
        =⟨ transp-∙ {B = Codes} (merid a) back e ⟩
      transport Codes back (transport Codes (merid a) e)
        =⟨ transport-Codes-mer a e ∙ μ.unit-r a
          |in-ctx (λ w → transport Codes back w) ⟩
      transport Codes back a
        =⟨ transport-Codes-mer-e-! a ⟩
      a ∎

  add-path-and-inverse-l : ∀ {k} {B : Type k} {x y z : B}
    → (p : y == x) (q : y == z)
    → q == (p ∙ ! p) ∙ q
  add-path-and-inverse-l p q = ap (λ s → s ∙ q) (! (!-inv-r p))

  add-path-and-inverse-r : ∀ {k} {B : Type k} {x y z : B}
    → (p : x == y) (q : z == y)
    → p == (p ∙ ! q) ∙ q
  add-path-and-inverse-r p q =
    ! (∙-unit-r p) ∙ ap (λ s → p ∙ s) (! (!-inv-l q)) ∙ ! (∙-assoc p (! q) q)

  homomorphism-l : (a' : A) → merid (μ e a') == (merid a' ∙ back) ∙ merid e
  homomorphism-l a' = ap merid (μ.unit-l a') ∙ add-path-and-inverse-r (merid a') (merid e)

  homomorphism-r : (a : A) → merid (μ a e) == (merid e ∙ back) ∙ merid a
  homomorphism-r a = ap merid (μ.unit-r a) ∙ add-path-and-inverse-l (merid e) (merid a)

  homomorphism-l₁ : (a' : A) → [ merid (μ e a') ]₁ == [ (merid a' ∙ back) ∙ merid e ]₁
  homomorphism-l₁ = ap [_]₁ ∘ homomorphism-l

  homomorphism-r₁ : (a : A) → [ merid (μ a e) ]₁ == [ (merid e ∙ back) ∙ merid a ]₁
  homomorphism-r₁ = ap [_]₁ ∘ homomorphism-r

  abstract
    homomorphism-args : args {i} {i} {A} {e} {A} {e}
    homomorphism-args =
      record {
        m = -1; n = -1;
        P = λ a a' → (Q a a' , ⟨⟩);
        f = homomorphism-r₁;
        g = homomorphism-l₁;
        p = ap (λ {(p₁ , p₂) → ap [_] (ap merid p₁ ∙ p₂)})
               (pair×= (! μ.coh) (coh (merid e)))
      }
      where
        Q : A → A → Type i
        Q a a' = [ merid (μ a a' ) ]₁ == [ (merid a' ∙ back) ∙ merid a ]₁
        coh : {B : Type i} {b b' : B} (p : b == b')
          → add-path-and-inverse-l p p == add-path-and-inverse-r p p
        coh idp = idp

    module HomomorphismExt =
      WedgeExt {i} {i} {A} {e} {A} {e} homomorphism-args

    homomorphism : (a a' : A)
      → [ merid (μ a a' ) ]₁ == [ (merid a' ∙ back) ∙ merid a ]₁
    homomorphism = HomomorphismExt.ext

    homomorphism-β-l : (a' : A) → homomorphism e a' == homomorphism-l₁ a'
    homomorphism-β-l = HomomorphismExt.β-r

    homomorphism-β-r : (a : A) → homomorphism a e == homomorphism-r₁ a
    homomorphism-β-r = HomomorphismExt.β-l

  decode' : {x : Susp A} → Codes x → P x
  decode' {x} = Susp-elim {P = λ x → Codes x → P x}
                 decodeN'
                 (λ a → [ merid a ])
                 (λ a → ↓-→-from-transp (λ= $ STS a))
                 x
    where
    abstract
      STS : (a a' : A) → transport P (merid a) (decodeN' a')
                         == [ merid (transport Codes (merid a) a') ]
      STS a a' =
        transport P (merid a) [ merid a' ∙ back ]
          =⟨ transport-Trunc' (north ==_) (merid a) _ ⟩
        [ transport (north ==_) (merid a) (merid a' ∙ back) ]
          =⟨ ap [_] (transp-cst=idf {A = Susp A} (merid a) _) ⟩
        [ (merid a' ∙ back) ∙ merid a ]
          =⟨ ! (homomorphism a a') ⟩
        [ merid (μ a a') ]
          =⟨ ap ([_] ∘ merid) (! (transport-Codes-mer a a')) ⟩
        [ merid (transport Codes (merid a) a') ] ∎

  decode'-encode' : {x : Susp A} (tα : P x)
    → decode' {x} (encode' {x} tα) == tα
  decode'-encode' {x} = Trunc-elim
    {P = λ tα → decode' {x} (encode' {x} tα) == tα}
    -- FIXME: Agda very slow (looping?) when omitting the next line
    {{λ _ → =-preserves-level Trunc-level}}
    (J (λ y p → decode' {y} (encode' {y} [ p ]) == [ p ])
        (ap [_] (!-inv-r (merid e))))

  eq' : Trunc 1 (Ω (⊙Susp (de⊙ X))) ≃ A
  eq' = equiv encode' decodeN' encode'-decodeN' decode'-encode'

  ⊙decodeN : ⊙Trunc 1 X ⊙→ ⊙Trunc 1 (⊙Ω (⊙Susp (de⊙ X)))
  ⊙decodeN = ⊙Trunc-fmap (SAL.η X)

  decodeN : Trunc 1 A → Trunc 1 (Ω (⊙Susp (de⊙ X)))
  decodeN = fst ⊙decodeN

  encodeN : Trunc 1 (Ω (⊙Susp (de⊙ X))) → Trunc 1 A
  encodeN = [_] ∘ encode' {x = north}

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

  eq : Trunc 1 (Ω (⊙Susp (de⊙ X))) ≃ Trunc 1 A
  eq = encodeN ,
    replace-inverse (snd ((unTrunc-equiv A)⁻¹ ∘e eq'))
      {decodeN}
      (Trunc-elim (λ _ → idp))

  ⊙eq : ⊙Trunc 1 (⊙Ω (⊙Susp (de⊙ X))) ⊙≃ ⊙Trunc 1 X
  ⊙eq = ≃-to-⊙≃ eq idp

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

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

    ⊙encodeN-⊙decodeN : ⊙encodeN ⊙∘ ⊙decodeN == ⊙idf _
    ⊙encodeN-⊙decodeN =
      ⊙encodeN ⊙∘ ⊙decodeN
        =⟨ ap (⊙encodeN ⊙∘_) (! ⊙<–-⊙eq) ⟩
      ⊙encodeN ⊙∘ ⊙<– ⊙eq
        =⟨ ⊙<–-inv-r ⊙eq ⟩
      ⊙idf _ =∎

  ⊙eq⁻¹ : ⊙Trunc 1 X ⊙≃ ⊙Trunc 1 (⊙Ω (⊙Susp (de⊙ X)))
  ⊙eq⁻¹ = ⊙decodeN , snd (eq ⁻¹)

  iso : Ω^S-group 0 (⊙Trunc 1 (⊙Ω (⊙Susp (de⊙ X))))
      ≃ᴳ Ω^S-group 0 (⊙Trunc 1 X)
  iso = Ω^S-group-emap 0 ⊙eq

  abstract
    π₂-Susp : πS 1 (⊙Susp (de⊙ X)) ≃ᴳ πS 0 X
    π₂-Susp =
      πS 1 (⊙Susp (de⊙ X))
        ≃ᴳ⟨ πS-Ω-split-iso 0 (⊙Susp (de⊙ X)) ⟩
      πS 0 (⊙Ω (⊙Susp (de⊙ X)))
        ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso 0 (⊙Ω (⊙Susp (de⊙ X))) ⁻¹ᴳ ⟩
      Ω^S-group 0 (⊙Trunc 1 (⊙Ω (⊙Susp (de⊙ X))))
        ≃ᴳ⟨ iso ⟩
      Ω^S-group 0 (⊙Trunc 1 X)
        ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso 0 X ⟩
      πS 0 X ≃ᴳ∎

module Pi2HSuspNaturality {i} {X Y : Ptd i}
  (f : X ⊙→ Y)
  {{_ : has-level 1 (de⊙ X)}} {{_ : has-level 1 (de⊙ Y)}}
  {{_ : is-connected 0 (de⊙ X)}} {{_ : is-connected 0 (de⊙ Y)}}
  (H-X : HSS X) (H-Y : HSS Y) where

  import homotopy.SuspAdjointLoop as SAL
  private
    module Π₂X = Pi2HSusp H-X
    module Π₂Y = Pi2HSusp H-Y

  ⊙decodeN-natural :
    Π₂Y.⊙decodeN ◃⊙∘
    ⊙Trunc-fmap f ◃⊙idf
    =⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-fmap (fst f))) ◃⊙∘
    Π₂X.⊙decodeN ◃⊙idf
  ⊙decodeN-natural = =⊙∘-in $
    Π₂Y.⊙decodeN ⊙∘ ⊙Trunc-fmap f
      =⟨ ⊙λ= (⊙Trunc-fmap-⊙∘ (SAL.η Y) f) ⟩
    ⊙Trunc-fmap (SAL.η Y ⊙∘ f)
      =⟨ ap ⊙Trunc-fmap (SAL.η-natural f) ⟩
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-fmap (fst f)) ⊙∘ SAL.η X)
      =⟨ ! (⊙λ= (⊙Trunc-fmap-⊙∘ (⊙Ω-fmap (⊙Susp-fmap (fst f))) (SAL.η X))) ⟩
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-fmap (fst f))) ⊙∘ Π₂X.⊙decodeN =∎

  ⊙encodeN-natural :
    Π₂Y.⊙encodeN ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-fmap (fst f))) ◃⊙idf
    =⊙∘
    ⊙Trunc-fmap f ◃⊙∘
    Π₂X.⊙encodeN ◃⊙idf
  ⊙encodeN-natural =
    Π₂Y.⊙encodeN ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-fmap (fst f))) ◃⊙idf
      =⊙∘⟨ 2 & 0 & =⊙∘-in {gs = Π₂X.⊙decodeN ◃⊙∘ Π₂X.⊙encodeN ◃⊙idf} $
           ! Π₂X.⊙decodeN-⊙encodeN ⟩
    Π₂Y.⊙encodeN ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-fmap (fst f))) ◃⊙∘
    Π₂X.⊙decodeN ◃⊙∘
    Π₂X.⊙encodeN ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ ⊙decodeN-natural ⟩
    Π₂Y.⊙encodeN ◃⊙∘
    Π₂Y.⊙decodeN ◃⊙∘
    ⊙Trunc-fmap f ◃⊙∘
    Π₂X.⊙encodeN ◃⊙idf
      =⊙∘⟨ 0 & 2 & =⊙∘-in {gs = ⊙idf-seq} Π₂Y.⊙encodeN-⊙decodeN ⟩
    ⊙Trunc-fmap f ◃⊙∘
    Π₂X.⊙encodeN ◃⊙idf ∎⊙∘

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Ex2 where

----------------------------------------------------------------------------
-- EXERCISE 2 -- STRUCTURE WITH VECTORS
--
-- VALUE:     15%
-- DEADLINE:  5pm, Friday 23 October (week 5)
--
-- DON'T SUBMIT, COMMIT!
--
-- The purpose of this exercise is to introduce you to some useful
-- mathematical structures and build good tools for working with
-- vectors
----------------------------------------------------------------------------

open import CS410-Prelude
open import CS410-Monoid
open import CS410-Nat
open import CS410-Vec
open import CS410-Functor

-- HINT: your tasks are heralded with the eminently searchable tag, "???"

----------------------------------------------------------------------------
-- ??? 2.1 replicattion to make a constant vector             (score: 1 / 1)
----------------------------------------------------------------------------

vec : forall {n X} -> X -> Vec X n
vec {zero} x = []
vec {suc n} x = x :: vec x

-- HINT: you may need to override default invisibility

-- SUSPICIOUS: no specification? why not?

----------------------------------------------------------------------------
-- ??? 2.2 vectorised application                             (score: 1 / 1)
----------------------------------------------------------------------------

-- implement the operator which takes the same number of functions
-- and arguments and computes the applications in corresponding
-- positions

vapp : forall {n X Y} -> Vec (X -> Y) n -> Vec X n -> Vec Y n
vapp [] xs = []
vapp (x :: fs) (y :: xs) = x y :: vapp fs xs

----------------------------------------------------------------------------
-- ??? 2.3 one-liners                                         (score: 1 / 1)
----------------------------------------------------------------------------

-- implement map and zip for vectors using vec and vapp
-- no pattern matching or recursion permitted

vmap : forall {n X Y} -> (X -> Y) -> Vec X n -> Vec Y n
vmap f xs = vapp (vec f) xs

vzip : forall {n X Y} -> Vec X n -> Vec Y n -> Vec (X * Y) n
vzip xs ys = vapp (vmap _,_ xs) ys

----------------------------------------------------------------------------
-- ??? 2.4 unzipping                                          (score: 2 / 2)
----------------------------------------------------------------------------

-- implement unzipping as a view, showing that every vector of pairs
-- is given by zipping two vectors

-- you'll need to complete the view type yourselfiew type yourself

data Unzippable {X Y n} : Vec (X * Y) n -> Set where
     unzipped : (xs : Vec X n)(ys : Vec Y n) -> Unzippable (vzip xs ys)

unzip : forall {X Y n}(xys : Vec (X * Y) n) -> Unzippable xys
unzip [] = unzipped [] []
unzip (fst , snd :: []) = unzipped (fst :: []) (snd :: [])  -- Conor: redundant line
unzip (fst , snd :: xys) with unzip xys
unzip (fst , snd :: .(vapp (vapp (vec _,_) xs) ys)) | unzipped xs ys =
                                            unzipped (fst :: xs) (snd :: ys)

----------------------------------------------------------------------------
-- ??? 2.5 vectors are applicative                            (score: 2 / 2)
----------------------------------------------------------------------------

-- prove the Applicative laws for vectors

VecApp : forall n -> Applicative \X -> Vec X n
VecApp n = record
  { pure         = vec
  ; _<*>_        = vapp
  ; identity     = \ {X} v -> VecAppIdentity v
  ; composition  = λ u v w →  VecAppComposition w v u
  ; homomorphism = λ f x →  VecAppHomomorphism n x f
  ; interchange  = λ {X} {Y} u y → VecAppInterchange y u
  } where
  -- lemmas go here

  --  Goal: vapp (vec (λ x → x)) v == v
  VecAppIdentity : {X : Set} -> {n : Nat} -> (v : Vec X n) ->
                                       vapp (vec (\ x -> x)) v == v
  VecAppIdentity [] = refl
  VecAppIdentity (x :: v) rewrite VecAppIdentity v =  refl

  --  Goal: vapp (vapp (vapp (vec (λ f g x → f (g x))) u) v) w == vapp u (vapp v w)

  VecAppComposition : {Z : Set} -> {Y : Set} -> {X : Set} -> {n : Nat} ->
                      (w : Vec X n) -> (v : Vec (X → Z) n) -> (u : Vec (Z → Y) n)->
                      vapp (vapp (vapp (vec (λ f g x → f (g x))) u) v) w == vapp u (vapp v w)
  VecAppComposition [] [] [] = refl
  VecAppComposition (x :: w) (x₁ :: v) (x₂ :: u)rewrite VecAppComposition w v u  = refl

  --  Goal: vec (f x) == vapp (vec f) (vec x)
  VecAppHomomorphism : {X : Set} -> {Y : Set} -> (q : Nat) -> (x : X) -> (f : X → Y) ->
                       vec {q} (f x)  == vapp (vec f) (vec x)
  VecAppHomomorphism zero x f = refl
  VecAppHomomorphism (suc q) x f rewrite VecAppHomomorphism q x f =  refl

  --  Goal: vapp u (vec y) == vapp (vec (λ f → f y)) u
  VecAppInterchange : {Y : Set} -> {X : Set} -> {n : Nat} -> (y : X) -> (u : Vec (X → Y) n) -> vapp u (vec y) == vapp (vec (λ f → f y)) u

  VecAppInterchange u [] = refl
  VecAppInterchange u (x :: y)  rewrite VecAppInterchange u y = refl

----------------------------------------------------------------------------
-- ??? 2.6 vectors are traversable                            (score: ? / 1)
----------------------------------------------------------------------------

-- show that vectors are traversable; make sure your traverse function
-- acts on the elements of the input once each, left-to-right

  VecTrav : forall n -> Traversable \X -> Vec X n
  VecTrav zero = record { traverse = λ {F} z {A} {B} _ _ → Applicative.pure z [] }
  VecTrav (suc n) = record { traverse = λ x x₁ x₂ → {!!} }

--VecTrav zero = record { traverse = λ {F} z {A} {B} _ _ → Applicative.pure z [] }
--VecTrav (suc n) =  record { traverse = λ {F} x y z → {!!} }

----------------------------------------------------------------------------
-- ??? 2.7 monoids make constant applicatives                 (score: ? / 1)
----------------------------------------------------------------------------

-- Show that every monoid gives rise to a degenerate applicative functor

MonCon : forall {X} -> Monoid X -> Applicative \_ -> X
MonCon M = record
             { pure          = λ x → Monoid.e M
             ; _<*>_         = op
             ; identity      = λ v → Monoid.lunit M v
             ; composition   = λ u v w → {!!}
             ; homomorphism  = λ f x → {!!}
             ; interchange   = λ u y → {!!}
             } where open Monoid M

       --MonConCoposition : (w : Set) -> (v : Set) -> (u : Set) -> op (op (op e u) v) w == op u (op v w)
       --MonConCoposition x = ?

----------------------------------------------------------------------------
-- ??? 2.8 vector combine                                     (score: ? / 1)
----------------------------------------------------------------------------

-- Using your answers to 2.6 and 2.7, rather than any new vector recursion,
-- show how to compute the result of combining all the elements of a vector
-- when they belong to some monoid.

vcombine : forall {X} -> Monoid X -> forall {n} -> Vec X n -> X
vcombine M = {!!}

----------------------------------------------------------------------------
-- ??? 2.9 scalar product                                     (score: ? / 1)
----------------------------------------------------------------------------

-- Show how to compute the scalar ("dot") product of two vectors of numbers.
-- (Multiply elements in corresponding positions; compute total of products.)
-- HINT: think zippily, then combine

vdot : forall {n} -> Vec Nat n -> Vec Nat n -> Nat
vdot xs ys = ?

----------------------------------------------------------------------------
-- MATRICES
----------------------------------------------------------------------------

-- let's say that an h by w matrix is a column h high of rows w wide

Matrix : Set -> Nat * Nat -> Set
Matrix X (h , w) = Vec (Vec X w) h

----------------------------------------------------------------------------
-- ??? 2.11 identity matrix                                   (score: ? / 1)
----------------------------------------------------------------------------

-- show how to construct the identity matrix of a given size, with
-- 1 on the main diagonal and 0 everywhere else, e.g,
-- (1 :: 0 :: 0 :: []) ::
-- (0 :: 1 :: 0 :: []) ::
-- (0 :: 0 :: 1 :: []) ::
-- []

idMat : forall {n} -> Matrix Nat (n , n)
idMat = {!!}

-- HINT: you may need to do recursion on the side, but then you
-- can make good use of vec and vapp

----------------------------------------------------------------------------
-- ??? 2.10 transposition                                     (score: ? / 1)
----------------------------------------------------------------------------

-- show how to transpose matrices
-- HINT: use traverse, and it's a one-liner

transpose : forall {X m n} -> Matrix X (m , n) -> Matrix X (n , m)
transpose = {!!}

----------------------------------------------------------------------------
-- ??? 2.11 multiplication                                    (score: ? / 2)
----------------------------------------------------------------------------

-- implement matrix multiplication
-- HINT: transpose and vdot can be useful

matMult : forall {m n p} ->
          Matrix Nat (m , n) -> Matrix Nat (n , p) -> Matrix Nat (m , p)
matMult xmn xnp = {!!}


text:
module Data.Vec.Membership where

open import Data.Vec as Vec
open import Data.Vec.Any
open import Data.Vec.Any.Membership.Propositional
open import Data.Product as Prod hiding (map)
open import Function using (_∘_; id)

find : ∀ {a p}{A : Set a}{P : A → Set p}{n}{xs : Vec A n} →
  Any P xs → ∃ λ x → x ∈ xs × P x
-- find = Prod.map id (Prod.map ∈′→∈ id) ∘ find′
find (here px) = , here , px
find (there p) = Prod.map id (Prod.map there id) (find p)

lose : ∀ {a p}{A : Set a}{P : A → Set p}{n x}{xs : Vec A n} →
  x ∈ xs → P x → Any P xs
lose = lose′ ∘ ∈→∈′

open import Function.Related as Related public using (Kind; Symmetric-kind)
            renaming (implication to subset
              ;  reverse-implication to superset
              ;  equivalence to set
              ;  injection to subbag
              ;  reverse-injection to superbag
              ;  bijection to bag)

_∼[_]_ : ∀ {a m n}{A : Set a} → Vec A m → Kind → Vec A n → Set _
xs ∼[ k ] ys = ∀ {x} → (x ∈ xs) Related.∼[ k ] (x ∈ ys)

max_stars_repo_name: tizmd/agda-vector-any

max_issues_repo_name: tizmd/agda-vector-any

max_forks_repo_name: tizmd/agda-vector-any


text:
-- Andreas, 2022-03-02, issue #5784, reported by Trebor-Huang
-- Test case by Ulf Norell

-- primEraseEquality needs to normalized the sides of the equation,
-- not just reduce them.

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Erase

data Wrap : Set where
  wrap : Nat → Wrap

test : wrap (1 + 1) ≡ wrap 2
test = primEraseEquality refl

thm : test ≡ refl
thm = refl

-- Should succeed
-- WAS: primEraseEquality refl != refl


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

module group-completion where

import 15-groups
open 15-groups public

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


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

-- Category With Families (as model of dependent type theory)
-- see https://ncatlab.org/nlab/show/categorical+model+of+dependent+types#categories_with_families
-- for more details.

open import Level
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Categories.Category
open import Categories.Functor
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.Object.Terminal

open import Categories.Category.Instance.FamilyOfSets
open import Categories.Functor.Presheaf
open import Categories.Category.Slice
open import Categories.Category.Instance.Sets

private
  variable
    o ℓ e a b : Level
-- We want to re-interpret the members of C as
-- the various parts of a type theory -- Context, types, terms, etc.
module UnpackFam {C : Category o ℓ e}
                 (T : Presheaf C (FamilyOfSets a b)) where
  private
    module C = Category C
    module T = Functor T

  Context : Set o
  Context = C.Obj

  Ty : C.Obj → Set a
  Ty Γ = Fam.U (T.F₀ Γ)

  -- remember that context morphisms are substitutions
  -- which are here applied postfix
  _[_] : ∀ {Γ Δ} → (T : Ty Γ) → (σ : Δ C.⇒ Γ) → Ty Δ
  _[_] T σ = Hom.f (T.F₁ σ) T

  Tm : ∀ Γ → Ty Γ → Set b
  Tm Γ = Fam.T (T.F₀ Γ)

  -- substitute into a term
  _[_⁺] : {Γ Δ : Context} {tp : Ty Γ} → (term : Tm Γ tp) → (σ : Δ C.⇒ Γ) → Tm Δ (tp [ σ ])
  _[_⁺] term σ = Hom.φ (T.F₁ σ) _ term

-- This is the original definition from Dybjer. The one from nLab is too tricky to do quite yet.
record CwF : Set (suc (o ⊔ ℓ ⊔ e ⊔ a ⊔ b)) where
  field
    C : Category o ℓ e
    T : Presheaf C (FamilyOfSets a b)
    Empty : Terminal C

  infix 5 _>_

  module C = Category C
  module T = Functor T
  open UnpackFam T
  module Empty = Terminal Empty

  field
    -- context snoc
    _>_ : ∀ Γ → Ty Γ → Context
    -- projections
    p : ∀ {Γ A} → (Γ > A) C.⇒ Γ
    v : ∀ {Γ A} → Tm (Γ > A) (A [ p ])
    -- constructor
    <_,_>         : ∀ {Γ A} → ∀ {Δ} (γ : Δ C.⇒ Γ) (a : Tm Δ (A [ γ ])) → Δ C.⇒ (Γ > A)

  v[_] : ∀ {Γ A Δ} → (γ : Δ C.⇒ Γ) -> Tm (Δ > A [ γ ]) (A [ γ C.∘ p ])
  v[_] {Γ} {A} {Δ} γ = ≡.subst (Tm (Δ > A [ γ ])) (Eq.g≡f (T.homomorphism {Γ})) v

  -- Note that the original used Heterogenenous equality (yuck). So here we use
  -- explicit transport. Explicit yuck.
  field
    p∘<γ,a>≡γ    : ∀ {Γ A} → ∀ {Δ} {γ : Δ C.⇒ Γ} {a : Tm Δ (A [ γ ])} → p C.∘ < γ , a > C.≈ γ

  patch : ∀ {Γ A} → ∀ {Δ} {γ : Δ C.⇒ Γ} {δ : Δ C.⇒ (Γ > A)} (a : Tm Δ (A [ γ ])) (pδ≈γ : p C.∘ δ C.≈ γ)
          → Fam.T (T.F₀ Δ) ((A [ p ]) [ δ ])
  patch {Γ} {A} {Δ} {γ} a pδ≈γ = ≡.subst (Fam.T (T.F₀ Δ)) (≡.trans (Eq.g≡f (T.F-resp-≈ pδ≈γ)) (≡.sym (Eq.g≡f (T.homomorphism {Γ})))) a
  field
    v[<γ,a>]≡a   : ∀ {Γ A} → ∀ {Δ} {γ : Δ C.⇒ Γ} {a : Tm Δ (A [ γ ])} → v [ < γ , a > ⁺] ≡  patch a p∘<γ,a>≡γ
    <γ,a>-unique : ∀ {Γ A} → ∀ {Δ} {γ : Δ C.⇒ Γ} {a : Tm Δ (A [ γ ])} →
                      (δ : Δ C.⇒ (Γ > A)) → (pδ≈γ : p C.∘ δ C.≈ γ) → ( v [ δ ⁺] ≡ patch a pδ≈γ) → δ C.≈ < γ , a >

  _[id] : ∀ {Γ A} -> Tm Γ A -> Tm Γ (A [ C.id ])
  _[id] {Γ} {A} x = ≡.subst (Tm Γ) (Eq.g≡f (T.identity {Γ}) {A}) x

  open UnpackFam T public
  open Empty public using () renaming (⊤ to <>)

-- inside a CwF, we can sort-of 'define' a λ-calculus with Π, but the results are way too
-- heterogeneous to contemplate...
{-
record Pi {o ℓ e a b} (Cwf : CwF {o} {ℓ} {e} {a} {b}) : Set (o ⊔ ℓ ⊔ a ⊔ b) where
  open CwF Cwf
  field
    Π : ∀ {Γ} -> (A : Ty Γ) (B : Ty (Γ > A)) -> Ty Γ
    lam : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (b : Tm (Γ > A) B) -> Tm Γ (Π A B)
    _$_ : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} ->
            (f : Tm Γ (Π A B)) (x : Tm Γ A) -> Tm Γ (B [ < C.id , x [id] > ])

    -- naturality laws
    Π-nat   : ∀ {Γ} -> (A : Ty Γ) (B : Ty (Γ > A)) -> ∀ {Δ} (γ : Δ C.⇒ Γ)
                     -> Π A B [ γ ] ≡ Π (A [ γ ]) (B [ < (γ C.∘ p) , v[ γ ] > ])
    lam-nat : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (b : Tm (Γ > A) B) -> ∀ {Δ} (γ : Δ C.⇒ Γ)
                     -> lam b [ γ ⁺] ≡ {! lam {A = A [ γ ]} (b [ < γ C.∘ p , v[ γ ] > ⁺]) !}
    app-nat : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (f : Tm Γ (Π A B)) (x : Tm Γ A) -> ∀ {Δ} (γ : Δ C.⇒ Γ)
                     -> (f $ x) [ γ ⁺] ≡ {! ≡.subst (Tm Δ) (Π-nat A B γ) (f [ γ ⁺]) $ (x [ γ ⁺]) !}

    -- proofs of the lam/_$_ isomorphism
    β : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (b : Tm (Γ > A) B) (x : Tm Γ A)
           -> (lam b $ x) ≡ b [ < C.id , x [id] > ⁺]

    η : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (f : Tm Γ (Π A B))
           -> lam (≡.subst (Tm (Γ > A)) (Π-nat A B p) (f [ p ⁺]) $ v) ≡ {! f !}
-}

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
------------------------------------------------------------------------
-- Some properties about integers
------------------------------------------------------------------------

module Data.Integer.Properties where

open import Algebra
import Algebra.Morphism as Morphism
open import Data.Empty
open import Data.Function
open import Data.Integer hiding (suc)
open import Data.Nat as ℕ renaming (_*_ to _ℕ*_)
import Data.Nat.Properties as ℕ
open import Data.Sign as Sign using () renaming (_*_ to _S*_)
import Data.Sign.Properties as SignProp
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open Morphism.Definitions ℤ ℕ _≡_

-- Some properties relating sign and ∣_∣ to _◃_.

sign-◃ : ∀ s n → sign (s ◃ suc n) ≡ s
sign-◃ Sign.- _ = refl
sign-◃ Sign.+ _ = refl

sign-cong : ∀ {s₁ s₂ n₁ n₂} →
            s₁ ◃ suc n₁ ≡ s₂ ◃ suc n₂ → s₁ ≡ s₂
sign-cong {s₁} {s₂} {n₁} {n₂} eq = begin
  s₁                  ≡⟨ sym $ sign-◃ s₁ n₁ ⟩
  sign (s₁ ◃ suc n₁)  ≡⟨ cong sign eq ⟩
  sign (s₂ ◃ suc n₂)  ≡⟨ sign-◃ s₂ n₂ ⟩
  s₂                  ∎

abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n
abs-◃ _      zero    = refl
abs-◃ Sign.- (suc n) = refl
abs-◃ Sign.+ (suc n) = refl

abs-cong : ∀ {s₁ s₂ n₁ n₂} →
           s₁ ◃ n₁ ≡ s₂ ◃ n₂ → n₁ ≡ n₂
abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin
  n₁           ≡⟨ sym $ abs-◃ s₁ n₁ ⟩
  ∣ s₁ ◃ n₁ ∣  ≡⟨ cong ∣_∣ eq ⟩
  ∣ s₂ ◃ n₂ ∣  ≡⟨ abs-◃ s₂ n₂ ⟩
  n₂           ∎

-- ∣_∣ commutes with multiplication.

abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_
abs-*-commute i j = abs-◃ _ _

-- Multiplication is right cancellative for non-zero integers.

cancel-*-right : ∀ i j k →
                 k ≢ + 0 → i * k ≡ j * k → i ≡ j
cancel-*-right i j k            ≢0 eq with signAbs k
cancel-*-right i j .(+ 0)       ≢0 eq | s ◂ zero  = ⊥-elim (≢0 refl)
cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n
  with ∣ s ◃ suc n ∣ | abs-◃ s (suc n) | sign (s ◃ suc n) | sign-◃ s n
...  | .(suc n)      | refl            | .s               | refl =
  ◃-cong (sign-i≡sign-j i j eq) $
         ℕ.cancel-*-right ∣ i ∣ ∣ j ∣ $ abs-cong eq
  where
  sign-i≡sign-j : ∀ i j →
                  sign i S* s ◃ ∣ i ∣ ℕ* suc n ≡
                  sign j S* s ◃ ∣ j ∣ ℕ* suc n →
                  sign i ≡ sign j
  sign-i≡sign-j i              j              eq with signAbs i | signAbs j
  sign-i≡sign-j .(+ 0)         .(+ 0)         eq | s₁ ◂ zero   | s₂ ◂ zero   = refl
  sign-i≡sign-j .(+ 0)         .(s₂ ◃ suc n₂) eq | s₁ ◂ zero   | s₂ ◂ suc n₂
    with ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂)
  ... | .(suc n₂) | refl
    with abs-cong {s₁} {sign (s₂ ◃ suc n₂) S* s} {0} {suc n₂ ℕ* suc n} eq
  ...   | ()
  sign-i≡sign-j .(s₁ ◃ suc n₁) .(+ 0)         eq | s₁ ◂ suc n₁ | s₂ ◂ zero
    with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁)
  ... | .(suc n₁) | refl
    with abs-cong {sign (s₁ ◃ suc n₁) S* s} {s₁} {suc n₁ ℕ* suc n} {0} eq
  ...   | ()
  sign-i≡sign-j .(s₁ ◃ suc n₁) .(s₂ ◃ suc n₂) eq | s₁ ◂ suc n₁ | s₂ ◂ suc n₂
    with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁)
       | sign (s₁ ◃ suc n₁) | sign-◃ s₁ n₁
       | ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂)
       | sign (s₂ ◃ suc n₂) | sign-◃ s₂ n₂
  ... | .(suc n₁) | refl | .s₁ | refl | .(suc n₂) | refl | .s₂ | refl =
    SignProp.cancel-*-right s₁ s₂ (sign-cong eq)

max_issues_repo_name: larrytheliquid/Lemmachine


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

module Cubical.Data.FinSet.Binary.Large where

open import Cubical.Functions.Embedding
open import Cubical.Functions.Involution

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

open import Cubical.Data.Bool
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation

private
  variable
    ℓ : Level

isBinary : Type ℓ → Type ℓ
isBinary B = ∥ Bool ≃ B ∥

Binary : ∀ ℓ → Type _
Binary ℓ = Σ (Type ℓ) isBinary

isBinary→isSet : ∀{B : Type ℓ} → isBinary B → isSet B
isBinary→isSet {B} = rec isPropIsSet λ eqv → isOfHLevelRespectEquiv 2 eqv isSetBool

private
  Σ≡Prop²
    : ∀{ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
    → {w x : Σ A B}
    → isOfHLevelDep 1 B
    → (p q : w ≡ x)
    → cong fst p ≡ cong fst q
    → p ≡ q
  Σ≡Prop² _ _ _ r i j .fst = r i j
  Σ≡Prop² {B = B} {w} {x} Bprp p q r i j .snd
    = isPropDep→isSetDep Bprp (w .snd) (x .snd) (cong snd p) (cong snd q) r i j

BinaryEmbedding : isEmbedding (λ(B : Binary ℓ) → map-snd isBinary→isSet B)
BinaryEmbedding w x = isoToIsEquiv theIso
  where
  open Iso
  f = map-snd isBinary→isSet

  theIso : Iso (w ≡ x) (f w ≡ f x)
  theIso .fun = cong f
  theIso .inv p i .fst = p i .fst
  theIso .inv p i .snd
    = ∥∥-isPropDep (Bool ≃_) (w .snd) (x .snd) (λ i → p i .fst) i
  theIso .rightInv p
    = Σ≡Prop² (isOfHLevel→isOfHLevelDep 1 (λ _ → isPropIsSet)) _ p refl
  theIso .leftInv p
    = Σ≡Prop² (∥∥-isPropDep (Bool ≃_)) _ p refl

Base : Binary _
Base .fst = Bool
Base .snd = ∣ idEquiv Bool ∣

Loop : Base ≡ Base
Loop i .fst = notEq i
Loop i .snd = ∥∥-isPropDep (Bool ≃_) (Base .snd) (Base .snd) notEq i

private
  notEq² : Square notEq refl refl notEq
  notEq² = involPath² {f = not} notnot

Loop² : Square Loop refl refl Loop
Loop² i j .fst = notEq² i j
Loop² i j .snd
  = isPropDep→isSetDep' (∥∥-isPropDep (Bool ≃_))
      notEq² (cong snd Loop) refl refl (cong snd Loop) i j

isGroupoidBinary : isGroupoid (Binary ℓ)
isGroupoidBinary
  = Embedding-into-hLevel→hLevel 2
      (map-snd isBinary→isSet , BinaryEmbedding)
      (isOfHLevelTypeOfHLevel 2)

record BinStructure (B : Type ℓ) : Type ℓ where
  field
    base : B
    loop : base ≡ base
    loop² : Square loop refl refl loop
    trunc : isGroupoid B

structure₀ : BinStructure (Binary ℓ-zero)
structure₀ .BinStructure.base = Base
structure₀ .BinStructure.loop = Loop
structure₀ .BinStructure.loop² = Loop²
structure₀ .BinStructure.trunc = isGroupoidBinary

module Parameterized (B : Type ℓ) where
  Baseᴾ : Bool ≃ B → Binary ℓ
  Baseᴾ P = B , ∣ P ∣

  Loopᴾ : (P Q : Bool ≃ B) → Baseᴾ P ≡ Baseᴾ Q
  Loopᴾ P Q i = λ where
      .fst → ua first i
      .snd → ∥∥-isPropDep (Bool ≃_) ∣ P ∣ ∣ Q ∣ (ua first) i
    where
    first : B ≃ B
    first = compEquiv (invEquiv P) Q

  Loopᴾ² : (P Q R : Bool ≃ B) → Square (Loopᴾ P Q) (Loopᴾ P R) refl (Loopᴾ Q R)
  Loopᴾ² P Q R i = Σ≡Prop (λ _ → squash) (S i)
    where
    PQ : B ≃ B
    PQ = compEquiv (invEquiv P) Q
    PR : B ≃ B
    PR = compEquiv (invEquiv P) R
    QR : B ≃ B
    QR = compEquiv (invEquiv Q) R
    Q-Q : Bool ≃ Bool
    Q-Q = compEquiv Q (invEquiv Q)

    PQRE : compEquiv PQ QR ≡ PR
    PQRE = compEquiv PQ QR
             ≡[ i ]⟨ compEquiv-assoc (invEquiv P) Q QR (~ i) ⟩
           compEquiv (invEquiv P) (compEquiv Q QR)
             ≡[ i ]⟨ compEquiv (invEquiv P) (compEquiv-assoc Q (invEquiv Q) R i) ⟩
           compEquiv (invEquiv P) (compEquiv Q-Q R)
             ≡[ i ]⟨ compEquiv (invEquiv P) (compEquiv (invEquiv-is-rinv Q i) R) ⟩
           compEquiv (invEquiv P) (compEquiv (idEquiv _) R)
             ≡[ i ]⟨ compEquiv (invEquiv P) (compEquivIdEquiv R i) ⟩
           PR ∎

    PQR : ua PQ ∙ ua QR ≡ ua PR
    PQR = ua PQ ∙ ua QR
            ≡[ i ]⟨ uaCompEquiv PQ QR (~ i) ⟩
          ua (compEquiv PQ QR)
            ≡⟨ cong ua PQRE ⟩
          ua PR ∎

    S : Square (ua PQ) (ua PR) refl (ua QR)
    S i j
      = hcomp (λ k → λ where
            (j = i0) → B
            (i = i0) → compPath-filler (ua PQ) (ua QR) (~ k) j
            (i = i1) → ua PR j
            (j = i1) → ua QR (i ∨ ~ k))
          (PQR i j)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Avionics.SafetyEnvelopes.Properties where

open import Data.Bool using (Bool; true; false; _∧_; T)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List as List using (List; []; _∷_; any)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there; satisfied)
open import Data.Maybe using (Maybe; just; nothing; is-just; _>>=_)
open import Data.Product as Prod using (∃-syntax; _×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong; cong₂; inspect; [_]; sym; trans)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡˘⟨_⟩_; _≡⟨_⟩_; _∎)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (toWitness; fromWitness)
open import Relation.Unary using (_∈_)

open import Avionics.Bool using (≡→T; T∧→×; ×→T∧; lem∧)
open import Avionics.List using (≡→any; any-map; any-map-rev; any→≡)
open import Avionics.Real
    using (ℝ; _+_; _-_; -_; _*_; _÷_; _^_; _<ᵇ_; _≤_; _<_; _<?_; _≤?_; _≢0;
           0ℝ; 1ℝ; 2ℝ; 1/2; abs; 1/_; _^2; √_; fromℕ;
           double-neg;
           ⟨0,∞⟩; [0,∞⟩;
           <-transˡ; 2>0; ⟨0,∞⟩→0<; 0<→⟨0,∞⟩; >0→≢0; >0→≥0;
           0≟0≡yes0≡0;
           abs<x→<x∧-x<; neg-involutive; neg-distrib-+; neg-mono-<->; neg-def; m-m≡0;
           +-comm; +-assoc; *-comm; *-assoc; +-monoˡ-<; m÷n<o≡m<o*n; m<o÷n≡m*n<o; neg-distribˡ-*; √x^2≡absx;
           x*x≡x^2; x^2*y^2≡⟨xy⟩^2; 1/x^2≡⟨1/x⟩^2)
open import Avionics.Probability using (NormalDist; Dist)
open import Avionics.SafetyEnvelopes
    using (inside; inside'; mahalanobis1; z-predictable'; P[_|X=_]_; classify''; classify; M→pbs;
           StallClasses; Stall; NoStall; Uncertain;
           no-uncertain;
           safety-envelope; z-predictable; Model; τ-confident;
           Stall≡1-NoStall; NoStall≡1-Stall; ≤p→¬≤1-p; ≤1-p→¬≤p
           )

open NormalDist using (σ; μ)

--<ᵇ→< : ∀ {x y} → T (x <ᵇ y) → x < y
--<ᵇ→< = toWitness

-- Preliminary defitinions

-- `pi` is the prediction interval for the z score, i.e.,
-- pi(N (μ, σ), z) = [μ − zσ, μ + zσ]
pi : NormalDist → ℝ → ℝ → Set
pi nd z x =  (μ nd) - z * (σ nd) < x
          ×  x < (μ nd) + z * (σ nd)

extractDists : Model → List NormalDist
extractDists M = List.map (proj₁ ∘ proj₂) (Model.fM M)

------------------------------ Starting point - Theorem 2 ------------------------------
-- Theorem 1 says:
-- In the case of univariate normal distributions, the z-predictability condition
-- >   mahalanobis(μ, x, σ²-¹) < z
-- reduces to
-- >   μ - zσ < x <ᵇ (μ + zσ)
-- the prediction interval with a z-score of z
z-pred-interval≡mahalanobis<z : ∀ (nd z x)
                              → inside nd z x ≡ inside' nd z x
z-pred-interval≡mahalanobis<z nd z x =
  begin
    inside nd z x
  ≡⟨⟩
    (u - z * s <ᵇ x) ∧ (x <ᵇ (u + z * s))
  ≡⟨ cong (λ e → ((u - z * s) <ᵇ x) ∧ (x <ᵇ e)) (
    begin
      u + z * s
    ≡˘⟨ cong₂ (_+_) (neg-involutive _) (neg-involutive _) ⟩
      -(- u) + -(-(z * s))
    ≡˘⟨ neg-distrib-+ _ _ ⟩
      -((- u) + (- (z * s)))
    ≡⟨⟩
      -(- u - z * s)
    ∎
  ) ⟩
    (u - z * s <ᵇ x) ∧ (x <ᵇ -(- u - z * s))
  ≡⟨ cong (λ e → (e <ᵇ x) ∧ (x <ᵇ -(- u - z * s))) (
    begin
      u - z * s
    ≡˘⟨ cong (_+ (- (z * s))) (neg-involutive _) ⟩
      -(- u) + (- (z * s))
    ≡˘⟨ neg-distrib-+ _ _ ⟩
      -(- u + z * s)
    ∎
  ) ⟩
    (-(- u + z * s) <ᵇ x) ∧ (x <ᵇ -(- u - z * s))
  ≡˘⟨ cong (λ e → (-(- u + z * s) <ᵇ e) ∧ (e <ᵇ -(- u - z * s))) (neg-involutive _) ⟩
    (-(- u + z * s) <ᵇ -(- x)) ∧ (-(- x) <ᵇ -(- u - z * s))
  ≡˘⟨ cong ((-(- u + z * s) <ᵇ -(- x)) ∧_) (neg-mono-<-> _ _) ⟩
    (-(- u + z * s) <ᵇ -(- x)) ∧ (- u - z * s <ᵇ - x)
  ≡˘⟨ cong (_∧ (- u - z * s <ᵇ - x)) (neg-mono-<-> _ _) ⟩
    (- x <ᵇ - u + z * s) ∧ (- u - z * s <ᵇ - x)
  ≡⟨ cong (_∧ (- u - z * s <ᵇ - x)) (
    begin
      - x <ᵇ - u + z * s
    ≡˘⟨ cong (_<ᵇ - u + z * s) (neg-def _) ⟩
      0ℝ - x <ᵇ - u + z * s
    ≡˘⟨ cong (λ e → e - x <ᵇ - u + z * s) (trans (+-comm _ _) (m-m≡0 _)) ⟩
      (- u + u) - x <ᵇ - u + z * s
    ≡˘⟨ cong (_<ᵇ - u + z * s) (+-assoc _ _ _) ⟩
      (- u) + (u - x) <ᵇ - u + z * s
    ≡˘⟨ +-monoˡ-< _ _ _ ⟩
      u - x <ᵇ z * s
    ∎
  ) ⟩
    (u - x <ᵇ z * s) ∧ (- u - z * s <ᵇ - x)
  ≡⟨ cong ((u - x <ᵇ z * s) ∧_) (
    begin
      - u - z * s <ᵇ - x
    ≡˘⟨ cong (- u - z * s <ᵇ_) (neg-def _) ⟩
      - u - z * s <ᵇ 0ℝ - x
    ≡˘⟨ cong (λ e → - u - z * s <ᵇ e - x) (trans (+-comm _ _) (m-m≡0 _)) ⟩
      - u - z * s <ᵇ (- u + u) - x
    ≡˘⟨ cong (- u - z * s <ᵇ_) (+-assoc _ _ _) ⟩
      - u - z * s <ᵇ - u + (u - x)
    ≡˘⟨ +-monoˡ-< _ _ _ ⟩
      - (z * s) <ᵇ u - x
    ∎
  ) ⟩
    (u - x <ᵇ z * s) ∧ (- (z * s) <ᵇ u - x)
  ≡˘⟨ cong ((u - x <ᵇ z * s) ∧_) (
    begin
      - z <ᵇ (u - x) ÷ s
    ≡⟨ m<o÷n≡m*n<o _ _ _ ⟩
      (- z) * s <ᵇ (u - x)
    ≡˘⟨ cong (_<ᵇ (u - x)) (neg-distribˡ-* _ _) ⟩
      - (z * s) <ᵇ u - x
    ∎
  ) ⟩
    (u - x <ᵇ z * s) ∧ (- z <ᵇ (u - x) ÷ s)
  ≡˘⟨ cong (_∧ (- z <ᵇ (u - x) ÷ s)) (m÷n<o≡m<o*n _ _ _) ⟩
    ((u - x) ÷ s <ᵇ z) ∧ (- z <ᵇ (u - x) ÷ s)
  ≡˘⟨ abs<x→<x∧-x< ⟩
    abs ((u - x) ÷ s) <ᵇ z
  ≡˘⟨ cong (_<ᵇ z) (√x^2≡absx _) ⟩
    √(((u - x) ÷ s)^2) <ᵇ z
  ≡⟨⟩
    √(((u - x) * (1/ s))^2) <ᵇ z
  ≡˘⟨ cong (λ e → √ e <ᵇ z) (
    begin
      (u - x) * (1/ (s * s)) * (u - x)
    ≡⟨ *-comm _ _ ⟩
      (u - x) * ((u - x) * (1/ (s * s)))
    ≡⟨ *-assoc _ _ _ ⟩
      (u - x) * (u - x) * (1/ (s * s))
    ≡⟨ cong (λ e → (u - x) * (u - x) * (1/ e)) (x*x≡x^2 _) ⟩
      (u - x) * (u - x) * (1/ (s ^2))
    ≡⟨ cong ((u - x) * (u - x) *_) (1/x^2≡⟨1/x⟩^2 _) ⟩
      (u - x) * (u - x) * (1/ s) ^2
    ≡⟨ cong (_* (1/ s) ^2) (x*x≡x^2 _) ⟩
      (u - x)^2 * (1/ s) ^2
    ≡⟨ x^2*y^2≡⟨xy⟩^2 _ _ ⟩
      ((u - x) * (1/ s))^2
    ∎
  )⟩
    √((u - x) * (1/ (s * s)) * (u - x)) <ᵇ z
  ≡⟨⟩
    mahalanobis1 u x (1/ (s * s)) <ᵇ z
  ≡⟨⟩
    inside' nd z x
  ∎
  where u = μ nd
        s = σ nd
---- ############ Theorem 1 END ############

------------------------------ Starting point - Theorem 2 ------------------------------
-- Proof of Theorem 2 (paper)
--
-- In words, the Property 1 says that:
--    The energy signal x is z-predictable iff there exist ⟨α, v⟩ s.t.
--    M(⟨α, v⟩)1 = di and x ∈ pi(di , z).
--
-- Notice that `Any (λ nd → x ∈ pi nd z) nds` translates to:
-- there exists nd such that `nd ∈ nds` and `x ∈ pi(nd, z)`
follows-def←' : ∀ (nds z x)
              → z-predictable' nds z x ≡ ⟨ x , true ⟩
              → Any (λ nd → x ∈ pi nd z) nds
follows-def←' nds z x res≡x,true = Any-x∈pi
  where
    res≡true = cong proj₂ res≡x,true

    -- the first `toWitness` takes a result `(μ nd - z * σ nd) <ᵇ x` (a
    -- boolean) and produces a proof of the type `(μ nd) - z * (σ nd) < x`
    -- assuming we have provided an operator `<?`
    toWitness' = λ nd → Prod.map (toWitness {Q = (μ nd - z * σ nd) <? x})
                                 (toWitness {Q = x <? (μ nd + z * σ nd)})

    -- We find the value for which `inside z x` becomes true in the list `nds`
    Any-bool = ≡→any (λ nd → inside nd z x) nds res≡true
    -- Converting the boolean proof into a proof at the type level
    Any-x∈pi = Any.map (λ {nd} → toWitness' nd ∘ T∧→×) Any-bool

-- forward proof
follows-def→' : ∀ (nds z x)
              → Any (λ nd → x ∈ pi nd z) nds
              → z-predictable' nds z x ≡ ⟨ x , true ⟩
follows-def→' nds z x any[x∈pi-z]nds = let
    -- converts a tuple of `(μ nd) - z * (σ nd) < x , x < (μ nd + z * σ nd)`
    -- (a proof) into a boolean
    fromWitness' nd = λ{⟨ μ-zσ<x , x<μ+zσ ⟩ →
                ×→T∧ ⟨ (fromWitness {Q = (μ nd - z * σ nd) <? x} μ-zσ<x)
                     , (fromWitness {Q = x <? (μ nd + z * σ nd)} x<μ+zσ)
                     ⟩}

    -- Converting from a proof on `_<_` to a proof on `_<ᵇ_`
    any[inside]nds = (Any.map (λ {nd} → fromWitness' nd) any[x∈pi-z]nds)

    -- Transforming the prove from Any into equality (_≡_)
    z-pred-x≡⟨x,true⟩ = any→≡ (λ nd → inside nd z x) nds any[inside]nds

     -- Extending the result from a single Bool value to a pair `ℝ × Bool`
  in cong (⟨ x ,_⟩) z-pred-x≡⟨x,true⟩

-- From the prove above we can obtain the value `nd` and its prove `x ∈ pi nd z`
-- Note: An element of ∃[ nd ] (x ∈ pi nd z) is a tuple of the form ⟨ nd , proof ⟩
--prop1← : ∀ (nds z x)
--       → z-predictable' nds z x ≡ ⟨ x , true ⟩
--       → ∃[ nd ] (x ∈ pi nd z)
--prop1← nds z x res≡x,true = satisfied (follows-def←' nds z x res≡x,true)

-- This proofs is telling us that `z-predictable` follows from the definition
follows-def← : ∀ (M z x)
             → z-predictable M z x ≡ ⟨ x , true ⟩
             → Any (λ nd → x ∈ pi nd z) (extractDists M)
follows-def← M z x res≡x,true = follows-def←' (extractDists M) z x res≡x,true

follows-def→ : ∀ (M z x)
             → Any (λ nd → x ∈ pi nd z) (extractDists M)
             → z-predictable M z x ≡ ⟨ x , true ⟩
follows-def→ M z x Any[x∈pi-nd-z]M = follows-def→' (extractDists M) z x Any[x∈pi-nd-z]M

-- ############ FINAL RESULT - Theorem 1 ############

-- In words: Given a Model `M` and parameter `z`, if `x` is z-predictable, then
-- there exists θ (a flight state) such that they are associated to a `nd`
-- (Normal Distribution) and `x` falls withing the Predictable Interval
theorem1← : ∀ (M z x)
          → z-predictable M z x ≡ ⟨ x , true ⟩
          → Any (λ{⟨ θ , ⟨ nd , p ⟩ ⟩ → x ∈ pi nd z}) (Model.fM M)
theorem1← M z x res≡x,true = any-map (proj₁ ∘ proj₂) (follows-def← M z x res≡x,true)

-- The reverse of theorem1←
theorem1→ : ∀ (M z x)
          → Any (λ{⟨ θ , ⟨ nd , p ⟩ ⟩ → x ∈ pi nd z}) (Model.fM M)
          → z-predictable M z x ≡ ⟨ x , true ⟩
theorem1→ M z x Any[θ→x∈pi-nd-z]M = follows-def→ M z x (any-map-rev (proj₁ ∘ proj₂) Any[θ→x∈pi-nd-z]M)

-- ################# Theorem 2 END ##################

------------------------------ Starting point - Theorem 2 ------------------------------
lem← : ∀ (pbs τ x k)
     → classify'' pbs τ x ≡ k
     → k ≡ Uncertain ⊎ ∃[ p ] ((P[ k |X= x ] pbs ≡ just p) × (τ ≤ p))
lem← pbs τ x k _ with P[ Stall |X= x ] pbs | inspect (P[ Stall |X=_] pbs) x
lem← _ _ _ Uncertain _ | nothing | [ P[k|X=x]≡nothing ] = inj₁ refl
lem← _ τ _ _       _   | just p  | [ _ ] with τ ≤? p | τ ≤? (1ℝ - p)
lem← _ _ _ Stall   _   | just p  | [ P[k|X=x]≡justp ] | yes τ≤p | no ¬τ≤1-p = inj₂ ⟨ p , ⟨ P[k|X=x]≡justp , τ≤p ⟩ ⟩
lem← _ _ _ NoStall _   | just p  | [ P[k|X=x]≡justp ] | no ¬τ≤p | yes τ≤1-p =
  let P[NoStall|X=x]≡just1-p = Stall≡1-NoStall P[k|X=x]≡justp
  in inj₂ ⟨ 1ℝ - p , ⟨ P[NoStall|X=x]≡just1-p , τ≤1-p ⟩ ⟩
lem← _ _ _ Uncertain _ | _       | _ | _ | _ = inj₁ refl

lem→' : ∀ (pbs τ x p)
      -- This line is asking for the main assumptions for the code to work properly:
      --   * 0.5 < τ ≤ 1
      --   * 0 ≤ p ≤ 1
      → (1/2 < τ × τ ≤ 1ℝ) × (0ℝ ≤ p × p ≤ 1ℝ)
      → (P[ Stall |X= x ] pbs) ≡ just p
      → τ ≤ (1ℝ - p)
      → classify'' pbs τ x ≡ NoStall
lem→' pbs _ x _ _ _ _ with P[ Stall |X= x ] pbs
lem→' _ τ _ _ _ _    _     | just p with τ ≤? p | τ ≤? (1ℝ - p)
lem→' _ _ _ _ _ _    _     | just p | no _    | yes _     = refl
lem→' _ _ _ _ _ refl τ≤1-p | just p | _       | no ¬τ≤1-p = ⊥-elim (¬τ≤1-p τ≤1-p)
lem→' _ _ _ _ assumpts refl τ≤1-p | just p | yes τ≤p | yes _     = ⊥-elim (¬τ≤p τ≤p)
  where
    1/2<τ = proj₁ (proj₁ assumpts)
    τ≤1 = proj₂ (proj₁ assumpts)
    0≤p = proj₁ (proj₂ assumpts)
    p≤1 = proj₂ (proj₂ assumpts)
    ¬τ≤p = ≤1-p→¬≤p 1/2<τ τ≤1 0≤p p≤1 τ≤1-p

τ≤p→τ≤1-⟨1-p⟩ : ∀ τ p → τ ≤ p → τ ≤ 1ℝ - (1ℝ - p)
τ≤p→τ≤1-⟨1-p⟩ τ p τ≤p rewrite double-neg p 1ℝ = τ≤p

lem→ : ∀ (pbs τ x k)
     → (1/2 < τ × τ ≤ 1ℝ)
     → ∃[ p ] (((P[ k |X= x ] pbs) ≡ just p) × (τ ≤ p))
     → classify'' pbs τ x ≡ k
lem→ pbs _ x Stall _ _ with P[ Stall |X= x ] pbs
lem→ _ τ _ _ _       _                      | just p with τ ≤? p | τ ≤? (1ℝ - p)
lem→ _ _ _ _ _       _                      | just p | yes _   | no  _     = refl
lem→ _ _ _ _ _       ⟨ _ , ⟨ refl , τ≤p ⟩ ⟩ | just p | no ¬τ≤p | _         = ⊥-elim (¬τ≤p τ≤p)
lem→ _ _ _ _ 1/2<τ≤1 ⟨ _ , ⟨ refl , τ≤p ⟩ ⟩ | just p | yes _   | yes τ≤1-p = ⊥-elim (¬τ≤1-p τ≤1-p)
  where 1/2<τ = proj₁ 1/2<τ≤1
        τ≤1 = proj₂ 1/2<τ≤1
        postulate 0≤p : 0ℝ ≤ p
                  p≤1 : p ≤ 1ℝ
        ¬τ≤1-p = ≤p→¬≤1-p 1/2<τ τ≤1 0≤p p≤1 τ≤p
lem→ pbs τ x NoStall 1/2<τ≤1 ⟨ p , ⟨ P[k|X=x]≡justp , τ≤p ⟩ ⟩ = let
    P[S|X=x]≡just1-p = NoStall≡1-Stall P[k|X=x]≡justp
    τ≤1-⟨1-p⟩ = τ≤p→τ≤1-⟨1-p⟩ τ p τ≤p
    assumptions = ⟨ 1/2<τ≤1 , 0≤p≤1 ⟩
  in lem→' pbs τ x (1ℝ - p) assumptions P[S|X=x]≡just1-p τ≤1-⟨1-p⟩
  where postulate 0≤p≤1 : (0ℝ ≤ 1ℝ - p × 1ℝ - p ≤ 1ℝ)

prop2M-prior← : ∀ (M τ x k)
              → classify M τ x ≡ k
              → k ≡ Uncertain ⊎ ∃[ p ] (((P[ k |X= x ] (M→pbs M)) ≡ just p) × (τ ≤ p))
prop2M-prior← M = lem← (M→pbs M)

prop2M-prior←' : ∀ (M τ x k)
               → k ≡ Stall ⊎ k ≡ NoStall
               → classify M τ x ≡ k
               → ∃[ p ] (((P[ k |X= x ] (M→pbs M)) ≡ just p) × (τ ≤ p))
prop2M-prior←' M τ x k _ cMτx≡k with prop2M-prior← M τ x k cMτx≡k
prop2M-prior←' _ _ _ Stall   (inj₁ _) _ | inj₂ P[k|X=x]≥τ = P[k|X=x]≥τ
prop2M-prior←' _ _ _ NoStall _        _ | inj₂ P[k|X=x]≥τ = P[k|X=x]≥τ

prop2M-prior→ : ∀ (M τ x k)
              → (1/2 < τ × τ ≤ 1ℝ)
              → ∃[ p ] (((P[ k |X= x ] (M→pbs M)) ≡ just p) × (τ ≤ p))
              → classify M τ x ≡ k
prop2M-prior→ M τ x k 1/2<τ≤1 = lem→ (M→pbs M) τ x k 1/2<τ≤1

prop2M← : ∀ (M τ x)
       → τ-confident M τ x ≡ true
       → ∃[ k ] ((classify M τ x ≡ k) × (k ≡ Stall ⊎ k ≡ NoStall))
prop2M← M τ x τconf≡true with classify M τ x
... | Stall   = ⟨ Stall ,   ⟨ refl , inj₁ refl ⟩ ⟩
... | NoStall = ⟨ NoStall , ⟨ refl , inj₂ refl ⟩ ⟩

prop2M→ : ∀ (M τ x k)
        → k ≡ Stall ⊎ k ≡ NoStall
        → classify M τ x ≡ k
        → τ-confident M τ x ≡ true
prop2M→ M τ x Stall   (inj₁ k≡Stall)   cMτx≡k = cong no-uncertain cMτx≡k
prop2M→ M τ x NoStall (inj₂ k≡NoStall) cMτx≡k = cong no-uncertain cMτx≡k

---- ############ FINAL RESULT - Theorem 3 ############
-- Theorem 3 says:
-- a classification k is τ-confident iff τ ≤ P[ k | X = x ]
theorem2← : ∀ (M τ x)
          → τ-confident M τ x ≡ true
          → ∃[ k ] (∃[ p ] (((P[ k |X= x ] (M→pbs M)) ≡ just p) × (τ ≤ p))) -- which means: τ ≤ P[ k | X = x ]
theorem2← M τ x τconf≡true = let -- prop2M-prior← M τ x k (prop2M← M τ x k τconf≡true)
  ⟨ k , ⟨ cMτx≡k , k≢Uncertain ⟩ ⟩ = prop2M← M τ x τconf≡true
  in ⟨ k , prop2M-prior←' M τ x k k≢Uncertain cMτx≡k ⟩

theorem2→ : ∀ (M τ x k)
          → (1/2 < τ × τ ≤ 1ℝ)
          → k ≡ Stall ⊎ k ≡ NoStall
          → ∃[ p ] (((P[ k |X= x ] (M→pbs M)) ≡ just p) × (τ ≤ p)) -- which means: τ ≤ P[ k | X = x ]
          → τ-confident M τ x ≡ true
theorem2→ M τ x k 1/2<τ≤1 k≢Uncertain ⟨p,⟩ =
    prop2M→ M τ x k k≢Uncertain (prop2M-prior→ M τ x k 1/2<τ≤1 ⟨p,⟩)
---- ############ Theorem 3 END ############

------------------------------ Starting point - Theorem 3 ------------------------------
---- ############ FINAL RESULT - Theorem 4 ############
-- The final theorem is more a corolary. It follows from Theorem 1 and 2
prop3M← : ∀ (M z τ x)
        → safety-envelope M z τ x ≡ true
        → (Any (λ{⟨ θ , ⟨ nd , p ⟩ ⟩ → x ∈ pi nd z}) (Model.fM M))
          × ∃[ k ] (∃[ p ] (((P[ k |X= x ] (M→pbs M)) ≡ just p) × (τ ≤ p)))
prop3M← M z τ x seM≡true = let
    -- Taking from the safety-envelope definition its components
    ⟨ left , τ-conf ⟩ =
              lem∧ {a = proj₂ (z-predictable M z x)}
                   {b = τ-confident M τ x}
                   seM≡true
    z-pred-x≡⟨x,true⟩ = cong (⟨ x ,_⟩) left
  in ⟨ theorem1← M z x z-pred-x≡⟨x,true⟩ , theorem2← M τ x τ-conf ⟩

prop3M→ : ∀ (M z τ x k)
        → (1/2 < τ × τ ≤ 1ℝ)
        → k ≡ Stall ⊎ k ≡ NoStall
        → (Any (λ{⟨ θ , ⟨ nd , p ⟩ ⟩ → x ∈ pi nd z}) (Model.fM M))
          × ∃[ p ] (((P[ k |X= x ] (M→pbs M)) ≡ just p) × (τ ≤ p))
        → safety-envelope M z τ x ≡ true
prop3M→ M z τ x k 1/2<τ≤1 k≢Uncertain ⟨ Any[θ→x∈pi-nd-z]M , ⟨p,⟩ ⟩ = let
  z-pred≡⟨x,true⟩ = theorem1→ M z x Any[θ→x∈pi-nd-z]M
  τ-conf          = theorem2→ M τ x k 1/2<τ≤1 k≢Uncertain ⟨p,⟩
  in cong₂ (_∧_) (cong proj₂ z-pred≡⟨x,true⟩) τ-conf
---- ############ Theorem 4 END ############

max_stars_repo_name: helq/safety-envelopes-sentinels

max_issues_repo_name: helq/safety-envelopes-sentinels

max_forks_repo_name: helq/safety-envelopes-sentinels


text:
postulate
  _+_ : Set₁ → Set₁ → Set₁
  _+  : Set₁ → Set₁ → Set₁

Foo : Set₁ → Set₁
Foo = _+ Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Erased-cubical.Erased where

open import Agda.Builtin.Cubical.Glue
open import Agda.Builtin.Cubical.Path
open import Agda.Primitive
open import Agda.Primitive.Cubical

-- Glue can be used in erased contexts.

@0 _ : SSet (lsuc lzero)
_ =
  (φ : I) (A : Set) (B : Partial φ Set)
  (f : PartialP φ (λ x → B x ≃ A)) →
  primGlue A B f

-- Erased higher constructors are allowed.

data ∥_∥ (A : Set) : Set where
  ∣_∣     : A → ∥ A ∥
  @0 trivial : (x y : ∥ A ∥) → x ≡ y

-- Modules that use --cubical can be imported.

import Erased-cubical.Cubical as C

-- Definitions from such modules can be used in erased contexts.

@0 _ : {A : Set} → A → C.∥ A ∥
_ = C.∣_∣

-- One can re-export Cubical Agda code using open public.

open import Erased-cubical.Cubical public
  renaming (∥_∥ to ∥_∥ᶜ; ∣_∣ to ∣_∣ᶜ; trivial to trivialᶜ)

-- And also code that uses --without-K.

open import Erased-cubical.Without-K public

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Structure.Setoid.Size.Proofs where

open import Data
open import Data.Proofs
import      Data.Either        as Either
import      Data.Either.Proofs as Either
import      Lvl
open import Functional
open import Function.Proofs
open import Function.Inverseₗ
open import Function.Inverse
open import Function.Iteration
open import Lang.Instance
open import Logic
open import Logic.Classical
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Setoid.Size
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Function
open import Structure.Relator.Equivalence
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type.Properties.Empty
open import Type.Properties.Inhabited
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₗ : Lvl.Level
private variable A B C : Setoid{ℓₑ}{ℓ}
private variable X Y Z : Type{ℓ}

module _ where
  instance
    [≍]-to-[≼] : (_≍_ {ℓₑ₁}{ℓ₁}{ℓₑ₂}{ℓ₂}) ⊆₂ (_≼_)
    _⊆₂_.proof [≍]-to-[≼] ([∃]-intro(f) ⦃ [∧]-intro f-function f-bijective ⦄) =
      ([∃]-intro(f) ⦃ [∧]-intro f-function (bijective-to-injective(f) ⦃ f-bijective ⦄) ⦄)

  instance
    [≍]-to-[≽] : (_≍_ {ℓₑ₁}{ℓ₁}{ℓₑ₂}{ℓ₂}) ⊆₂ (_≽_)
    _⊆₂_.proof [≍]-to-[≽] ([∃]-intro(f) ⦃ [∧]-intro f-function f-bijective ⦄) =
      ([∃]-intro(f) ⦃ [∧]-intro f-function (bijective-to-surjective(f) ⦃ f-bijective ⦄) ⦄)

  [≼]-empty-is-minimal : (([∃]-intro(Empty{ℓ})) ≼ A)
  [≼]-empty-is-minimal = [∃]-intro empty ⦃ [∧]-intro empty-function empty-injective ⦄

  [≽]-empty-is-not-minimal : ¬(∀{A : Setoid{ℓ}} → (A ≽ ([∃]-intro(Empty{ℓ}))))
  [≽]-empty-is-not-minimal proof with () ← [∃]-witness(proof {[∃]-intro Unit}) <>

  [≼]-to-[≽]-not-all : ¬((_≼_ {ℓ}) ⊆₂ swap(_≽_))
  [≼]-to-[≽]-not-all (intro proof) = [≽]-empty-is-not-minimal(proof [≼]-empty-is-minimal)

  [≼]-to-[≽]-for-inhabited : ⦃ _ : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ ⦃ inh-A : (◊([∃]-witness A)) ⦄ → ((A ≼ B) → (B ≽ A))
  [≼]-to-[≽]-for-inhabited {A = [∃]-intro a} {B = [∃]-intro b} ([∃]-intro f ⦃ [∧]-intro f-func f-inj ⦄) = [∃]-intro (invₗ-construction(const [◊]-existence) f) ⦃ [∧]-intro (invₗ-construction-function ⦃ inj = f-inj ⦄) (inverseₗ-surjective ⦃ inverₗ = invₗ-construction-inverseₗ ⦃ inj = f-inj ⦄ ⦄) ⦄

  {- TODO: Maybe this proof could be made to a proof about invertibility instead
  [≼][≍]-almost-antisymmetry : ⦃ _ : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ → (A ≼ B) → (B ≼ A) → (A ≽ B)
  [≼][≍]-almost-antisymmetry {A = A}{B = B} ([∃]-intro f ⦃ [∧]-intro func-f inj-f ⦄) ([∃]-intro g ⦃ [∧]-intro func-g inj-g ⦄) = [∃]-intro h ⦃ [∧]-intro func-h surj-h ⦄ where
    h : [∃]-witness A → [∃]-witness B
    h(a) = Either.map1 [∃]-witness (const(f(a))) (excluded-middle(∃(b ↦ g(b) ≡ a)))

    func-h : Function(h)
    Function.congruence func-h {a₁} {a₂} a₁a₂ with excluded-middle(∃(b ↦ g(b) ≡ a₁)) | excluded-middle(∃(b ↦ g(b) ≡ a₂)) | a₁a₂ -- TODO: Not sure why the last a₁a₂ is neccessary for the result to normalize from the cases, if this is a bug in Agda or if it is intended. An alternative is to just use two-layered Either.map1-values
    ... | [∨]-introₗ ([∃]-intro b₁ ⦃ gba1 ⦄) | [∨]-introₗ ([∃]-intro b₂ ⦃ gba2 ⦄) | _ = injective(g) ⦃ inj-g ⦄ (gba1 🝖 a₁a₂ 🝖 symmetry(_≡_) gba2)
    ... | [∨]-introₗ ([∃]-intro b₁ ⦃ gba1 ⦄) | [∨]-introᵣ ngba2                   | _ = [⊥]-elim(ngba2([∃]-intro b₁ ⦃ gba1 🝖 a₁a₂ ⦄))
    ... | [∨]-introᵣ ngba1                   | [∨]-introₗ ([∃]-intro b₂ ⦃ gba2 ⦄) | _ = [⊥]-elim(ngba1([∃]-intro b₂ ⦃ gba2 🝖 symmetry(_≡_) a₁a₂ ⦄))
    ... | [∨]-introᵣ _                       | [∨]-introᵣ _                       | _ = congruence₁(f) ⦃ func-f ⦄ a₁a₂

      {- TODO: This choice of h probably does not work for proving antisymmetry because nothing states that f and g are inverses, which is neccessary for this kind of proof
      inj-h : Injective(h)
      Injective.proof inj-h {a₁} {a₂} ha₁ha₂ with excluded-middle(∃(b ↦ g(b) ≡ a₁)) | excluded-middle(∃(b ↦ g(b) ≡ a₂)) | ha₁ha₂
      ... | [∨]-introₗ ([∃]-intro b₁ ⦃ gba1 ⦄) | [∨]-introₗ ([∃]-intro b₂ ⦃ gba2 ⦄) | b₁b₂ =
        a₁    🝖-[ gba1 ]-sym
        g(b₁) 🝖-[ congruence₁(g) ⦃ func-g ⦄ b₁b₂ ]
        g(b₂) 🝖-[ gba2 ]
        a₂    🝖-end
      ... | [∨]-introₗ ([∃]-intro b₁ ⦃ gba1 ⦄) | [∨]-introᵣ nega₂                   | b₁fa₂ = [⊥]-elim(nega₂ ([∃]-intro (f(a₂)) ⦃ p ⦄)) where
        p =
          g(f(a₂)) 🝖-[ congruence₁(g) ⦃ func-g ⦄ b₁fa₂ ]-sym
          g(b₁)    🝖-[ gba1 ]
          a₁       🝖-[ {!gba1!} ]
          a₂       🝖-end
        q =
          f(a₁)    🝖-[ congruence₁(f) ⦃ func-f ⦄ gba1 ]-sym
          f(g(b₁)) 🝖-[ {!!} ]
          b₁       🝖-[ b₁fa₂ ]
          f(a₂)    🝖-end
      ... | [∨]-introᵣ nega₁                   | [∨]-introₗ ([∃]-intro b₂ ⦃ gba2 ⦄) | fa₁b₂ = {!!}
      ... | [∨]-introᵣ nega₁                   | [∨]-introᵣ nega₂                   | fa₁fa₂ = injective(f) ⦃ inj-f ⦄ fa₁fa₂
      -}

    -- TODO: Is it possible to use [≼]-to-[≽]-for-inhabited instead or maybe this should be moved out?
    surj-h : Surjective(h)
    Surjective.proof surj-h {b} with Either.map1-values{f = [∃]-witness}{g = const(f(g(b)))}{e = excluded-middle(∃(x ↦ g(x) ≡ g(b)))}
    ... | [∨]-introₗ ([∃]-intro ([∃]-intro b₂ ⦃ gb₂gb ⦄) ⦃ fgbb₂ ⦄) = [∃]-intro (g(b)) ⦃ fgbb₂ 🝖 injective(g) ⦃ inj-g ⦄ gb₂gb ⦄
    ... | [∨]-introᵣ([∃]-intro neggb ⦃ p ⦄) = [⊥]-elim(neggb ([∃]-intro b ⦃ reflexivity(_≡_) ⦄))
  -}

  open import Structure.Operator
  open import Structure.Setoid.Uniqueness
  module _ ⦃ equiv-X : Equiv{ℓₑ₁}(X) ⦄ ⦃ equiv-Y : Equiv{ℓₑ₂}(Y) ⦄ (P : X → Type{ℓₗ}) ⦃ classical-P : Classical(∃ P) ⦄ (c : ¬(∃ P) → Y) (f : X → Y) ⦃ func-f : Function(f) ⦄ where -- TODO: Maybe f should also be able to depend on P, so that (f : (x : X) → P(x) → Y)?
    -- TODO: This is a generalization of both h in [≼][≍]-antisymmetry-raw and invₗ-construction from Function.Inverseₗ
    existence-decider : Y
    existence-decider = Either.map1 (f ∘ [∃]-witness) c (excluded-middle(∃ P))

    existence-decider-satisfaction-value : Unique(P) → ∀{x} → P(x) → (f(x) ≡ existence-decider)
    existence-decider-satisfaction-value unique-P {x} px with Classical.excluded-middle classical-P
    ... | Either.Left  ([∃]-intro y ⦃ py ⦄) = congruence₁(f) (unique-P px py)
    ... | Either.Right nep with () ← nep ([∃]-intro x ⦃ px ⦄)

    existence-decider-unsatisfaction-value : ⦃ Constant(c) ⦄ → (p : ¬(∃ P)) → (c(p) ≡ existence-decider)
    existence-decider-unsatisfaction-value nep with Classical.excluded-middle classical-P
    ... | Either.Left  ep with () ← nep ep
    ... | Either.Right _ = constant(c)

  module _ ⦃ equiv-X : Equiv{ℓₑ₁}(X) ⦄ ⦃ equiv-Y : Equiv{ℓₑ₂}(Y) ⦄ ⦃ equiv-Z : Equiv{ℓₑ₃}(Z) ⦄ (P : X → Y → Type{ℓₗ}) ⦃ classical-P : ∀{x} → Classical(∃(P(x))) ⦄ (c : (x : X) → ¬(∃(P(x))) → Z) (f : X → Y → Z) ⦃ func-f : BinaryOperator(f) ⦄ where
    existence-decider-fn : X → Z
    existence-decider-fn(x) = existence-decider (P(x)) (c(x)) (f(x)) ⦃ BinaryOperator.right func-f ⦄

    open import Structure.Relator
    existence-decider-fn-function : (∀{x} → Unique(P(x))) → (∀{x₁ x₂}{p₁ p₂} → (x₁ ≡ x₂) → (c x₁ p₁ ≡ c x₂ p₂)) → ⦃ ∀{y} → UnaryRelator(swap P y) ⦄ → Function(existence-decider-fn)
    Function.congruence (existence-decider-fn-function unique constant) {x₁} {x₂} x₁x₂ with excluded-middle(∃(P(x₁))) | excluded-middle(∃(P(x₂))) | x₁x₂
    ... | [∨]-introₗ ([∃]-intro y₁ ⦃ p₁ ⦄) | [∨]-introₗ ([∃]-intro y₂ ⦃ p₂ ⦄) | _
      = congruence₂(f) x₁x₂ (unique (substitute₁(swap P y₁) x₁x₂ p₁) p₂)
    ... | [∨]-introₗ ([∃]-intro y₁ ⦃ p₁ ⦄) | [∨]-introᵣ ngba2 | _
      with () ← ngba2 ([∃]-intro y₁ ⦃ substitute₁(swap P y₁) x₁x₂ p₁ ⦄)
    ... | [∨]-introᵣ ngba1 | [∨]-introₗ ([∃]-intro y₂ ⦃ p₂ ⦄) | _
      with () ← ngba1 ([∃]-intro y₂ ⦃ substitute₁(swap P y₂) (symmetry(_≡_) x₁x₂) p₂ ⦄)
    ... | [∨]-introᵣ _ | [∨]-introᵣ _ | _ = constant x₁x₂

    existence-decider-fn-surjective : (∀{x} → Unique(P(x))) → ⦃ ∀{x} → Constant(c(x)) ⦄ → (∀{z} → ∃(x ↦ (∀{y} → P(x)(y) → (f x y ≡ z)) ∧ ((nepx : ¬ ∃(P(x))) → (c x nepx ≡ z)))) → Surjective(existence-decider-fn)
    Surjective.proof (existence-decider-fn-surjective unique-p property) {z} with [∃]-intro x ⦃ px ⦄ ← property{z} with excluded-middle(∃(P(x)))
    ... | [∨]-introₗ ([∃]-intro y ⦃ pxy ⦄)
      = [∃]-intro x ⦃ symmetry(_≡_) (existence-decider-satisfaction-value(P(x)) (c(x)) (f(x)) ⦃ BinaryOperator.right func-f ⦄ unique-p pxy) 🝖 [∧]-elimₗ px pxy ⦄
    ... | [∨]-introᵣ nepx
      = [∃]-intro x ⦃ symmetry(_≡_) (existence-decider-unsatisfaction-value(P(x)) (c(x)) (f(x)) ⦃ BinaryOperator.right func-f ⦄ nepx) 🝖 [∧]-elimᵣ px nepx ⦄

    existence-decider-fn-surjective2 : (∀{x} → Unique(P(x))) → ⦃ ∀{x} → Constant(c(x)) ⦄ → (∃{Obj = Z → X}(x ↦ (∀{z}{y} → P(x(z))(y) → (f (x(z)) y ≡ z)) ∧ (∀{z} → (nepx : ¬ ∃(P(x(z)))) → (c (x(z)) nepx ≡ z)))) → Surjective(existence-decider-fn)
    Surjective.proof (existence-decider-fn-surjective2 unique-p property) {z} with [∃]-intro x ⦃ px ⦄ ← property with excluded-middle(∃(P(x(z))))
    ... | [∨]-introₗ ([∃]-intro y ⦃ pxy ⦄)
      = [∃]-intro (x(z)) ⦃ symmetry(_≡_) (existence-decider-satisfaction-value(P(x(z))) (c(x(z))) (f(x(z))) ⦃ BinaryOperator.right func-f ⦄ unique-p pxy) 🝖 [∧]-elimₗ px pxy ⦄
    ... | [∨]-introᵣ nepx
      = [∃]-intro (x(z)) ⦃ symmetry(_≡_) (existence-decider-unsatisfaction-value(P(x(z))) (c(x(z))) (f(x(z))) ⦃ BinaryOperator.right func-f ⦄ nepx) 🝖 [∧]-elimᵣ px nepx ⦄

    module _
      (inj-f   : ∀{x₁ x₂}{y₁ y₂} → P(x₁)(y₁) → P(x₂)(y₂) → (f x₁ y₁ ≡ f x₂ y₂) → (x₁ ≡ x₂))
      (inj-c   : ∀{x₁ x₂} → (nep₁ : ¬ ∃(P(x₁))) → (nep₂ : ¬ ∃(P(x₂))) → (c x₁ nep₁ ≡ c x₂ nep₂) → (x₁ ≡ x₂))
      (inj-mix : ∀{x₁ x₂}{y₁} → P(x₁)(y₁) → (nep₂ : ¬ ∃(P(x₂))) → (f x₁ y₁ ≡ c x₂ nep₂) → (x₁ ≡ x₂))
      where

      existence-decider-fn-injective : Injective(existence-decider-fn)
      Injective.proof existence-decider-fn-injective {x₁}{x₂} dx₁dx₂ with excluded-middle(∃(P(x₁))) | excluded-middle(∃(P(x₂))) | dx₁dx₂
      ... | Either.Left ([∃]-intro y₁ ⦃ p₁ ⦄) | Either.Left ([∃]-intro y₂ ⦃ p₂ ⦄) | fx₁y₁fx₂y₂ = inj-f p₁ p₂ fx₁y₁fx₂y₂
      ... | Either.Left ([∃]-intro y₁ ⦃ p₁ ⦄) | Either.Right nep₂                 | fxy₁cxp₂   = inj-mix p₁ nep₂ fxy₁cxp₂
      ... | Either.Right nep₁                 | Either.Left ([∃]-intro y₂ ⦃ p₂ ⦄) | cxp₁fxy₂   = symmetry(_≡_) (inj-mix p₂ nep₁ (symmetry(_≡_) cxp₁fxy₂))
      ... | Either.Right nep₁                 | Either.Right nep₂                 | cxp₁cxp₂   = inj-c nep₁ nep₂ cxp₁cxp₂

  -- The property of antisymmetry for injection existence.
  -- Also called: Cantor-Schröder-Bernstein Theorem, Schröder-Bernstein Theorem, Cantor–Bernstein theorem
  -- Source: https://artofproblemsolving.com/wiki/index.php/Schroeder-Bernstein_Theorem
  [≼][≍]-antisymmetry-raw : ⦃ _ : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ → (A ≼ B) → (B ≼ A) → (A ≍ B) -- TODO: Not everything needs to be classical, only forall, exists, and equality
  [≼][≍]-antisymmetry-raw {A = [∃]-intro A}{B = [∃]-intro B} ⦃ classical ⦄ ([∃]-intro f ⦃ [∧]-intro func-f inj-f ⦄) ([∃]-intro g ⦃ [∧]-intro func-g inj-g ⦄) = [∃]-intro h ⦃ [∧]-intro func-h (injective-surjective-to-bijective(h)) ⦄ where
    open import Logic.Predicate.Theorems
    open import Function.Inverseₗ
    open import Numeral.Natural
    open import Structure.Relator

    -- A lone point `b` of `B` is a point not in the image of `f`.
    Lone : B → Stmt
    Lone(b) = ∀{a} → (f(a) ≢ b)

    -- A point `b₁` is a descendent from a point `b₀` in `B` when a number of compositions of `(f ∘ g)` on `b₀` yields `b₁`.
    Desc : B → B → Stmt
    Desc(b₁)(b₀) = ∃(n ↦ (b₁ ≡ ((f ∘ g) ^ n)(b₀)))

    instance
      lone-desc-rel : ∀{y} → UnaryRelator(x ↦ Lone(y) ∧ Desc(f(x)) y)
      UnaryRelator.substitution lone-desc-rel xy = [∧]-map id (ep ↦ [∃]-map-proof-dependent ep (symmetry(_≡_) (congruence₁(f) ⦃ func-f ⦄ xy) 🝖_))

    f⁻¹ : B → A
    f⁻¹ = invₗ-construction g f

    g⁻¹ : A → B
    g⁻¹ = invₗ-construction f g

    instance
      func-f⁻¹ : Function(f⁻¹)
      func-f⁻¹ = invₗ-construction-function ⦃ inj = inj-f ⦄ ⦃ func-g ⦄

    instance
      func-g⁻¹ : Function(g⁻¹)
      func-g⁻¹ = invₗ-construction-function ⦃ inj = inj-g ⦄ ⦃ func-f ⦄

    instance
      inverₗ-f⁻¹ : Inverseₗ(f)(f⁻¹)
      inverₗ-f⁻¹ = invₗ-construction-inverseₗ ⦃ inj = inj-f ⦄ ⦃ func-g ⦄

    instance
      inverₗ-g⁻¹ : Inverseₗ(g)(g⁻¹)
      inverₗ-g⁻¹ = invₗ-construction-inverseₗ ⦃ inj = inj-g ⦄ ⦃ func-f ⦄

    instance
      func-const-invₗ-construction : BinaryOperator(const ∘ g⁻¹)
      func-const-invₗ-construction = functions-to-binaryOperator _ ⦃ r = const-function ⦄

    -- The to-be-proven bijection.
    -- `h` is a mapping such that:
    -- • If `f(a)` is a descendent of a lonely point,     then `h(a) = g⁻¹(a)`.
    -- • If `f(a)` is not a descendent of a lonely point, then `h(a) = f(a)`.
    -- Note: The construction of this function requires excluded middle.
    h : A → B
    h = existence-decider-fn (a ↦ b ↦ Lone(b) ∧ Desc(f(a))(b)) (\a _ → f(a)) (\a _ → g⁻¹(a))

    -- The left inverse of `g` is a right inverse on a point `a` when `f(a)` is a descendent of a lonely point.
    inverᵣ-g⁻¹-specific : ∀{a}{b} → Lone(b) → Desc(f(a))(b) → (g(g⁻¹(a)) ≡ a)
    inverᵣ-g⁻¹-specific        lone-b ([∃]-intro 𝟎      ⦃ desc-b ⦄) with () ← lone-b desc-b
    inverᵣ-g⁻¹-specific {a}{b} lone-b ([∃]-intro (𝐒(n)) ⦃ desc-b ⦄) =
      g(g⁻¹(a))                   🝖[ _≡_ ]-[ congruence₁(g) ⦃ func-g ⦄ (congruence₁(g⁻¹) (injective(f) ⦃ inj-f ⦄ desc-b)) ]
      g(g⁻¹(g(((f ∘ g) ^ n)(b)))) 🝖[ _≡_ ]-[ congruence₁(g) ⦃ func-g ⦄ (inverseₗ(g)(g⁻¹)) ]
      g(((f ∘ g) ^ n)(b))         🝖[ _≡_ ]-[ inverseₗ(f)(f⁻¹) ]-sym
      f⁻¹(f(g(((f ∘ g) ^ n)(b)))) 🝖[ _≡_ ]-[]
      f⁻¹(((f ∘ g) ^ 𝐒(n))(b))    🝖[ _≡_ ]-[ congruence₁(f⁻¹) desc-b ]-sym
      f⁻¹(f(a))                   🝖[ _≡_ ]-[ inverseₗ(f)(f⁻¹) ]
      a                           🝖-end

    inj-different-fgn : ∀{n₁ n₂}{b₁ b₂} → (((f ∘ g) ^ n₁)(b₁) ≡ ((f ∘ g) ^ n₂)(b₂)) → ∃(n ↦ (b₁ ≡ ((f ∘ g) ^ 𝐒(n))(b₂)) ∨ (((f ∘ g) ^ 𝐒(n))(b₁) ≡ b₂) ∨ (b₁ ≡ b₂))
    inj-different-fgn {𝟎}    {𝟎}    p = [∃]-intro 𝟎 ⦃ [∨]-introᵣ p ⦄
    inj-different-fgn {𝟎}    {𝐒 n₂} p = [∃]-intro n₂ ⦃ [∨]-introₗ([∨]-introₗ p) ⦄
    inj-different-fgn {𝐒 n₁} {𝟎}    p = [∃]-intro n₁ ⦃ [∨]-introₗ([∨]-introᵣ p) ⦄
    inj-different-fgn {𝐒 n₁} {𝐒 n₂} p = inj-different-fgn {n₁} {n₂} (Injective.proof inj-g(Injective.proof inj-f p))

    -- The lonely points are unique for all descendents from the image of `f`.
    unique-lone-descendant : ∀{a} → Unique(b ↦ Lone(b) ∧ Desc(f(a))(b))
    unique-lone-descendant {a} {b₁} {b₂} ([∧]-intro lone-b₁ ([∃]-intro n₁ ⦃ desc-b₁ ⦄)) ([∧]-intro lone-b₂ ([∃]-intro n₂ ⦃ desc-b₂ ⦄)) with inj-different-fgn{n₁}{n₂}{b₁}{b₂} (symmetry(_≡_) desc-b₁ 🝖 desc-b₂)
    ... | [∃]-intro n ⦃ Either.Left(Either.Left  p) ⦄ with () ← lone-b₁ (symmetry(_≡_) p)
    ... | [∃]-intro n ⦃ Either.Left(Either.Right p) ⦄ with () ← lone-b₂ p
    ... | [∃]-intro n ⦃ Either.Right b₁b₂ ⦄ = b₁b₂

    instance
      func-h : Function(h)
      func-h = existence-decider-fn-function (a ↦ b ↦ Lone(b) ∧ Desc(f(a))(b)) (\x _ → f(x)) (const ∘ g⁻¹) unique-lone-descendant (congruence₁(f) ⦃ func-f ⦄)

    -- What it means to not have a lonely descendent.
    not-lone-desc : ∀{a} → ¬ ∃(b ↦ Lone(b) ∧ Desc(f(a)) b) → (∀{b} → (∃(x ↦ f(x) ≡ b) ∨ (∀{n} → (f(a) ≢ ((f ∘ g) ^ n)(b)))))
    not-lone-desc {z} = (\nepx {x} → (Either.map ([∃]-map-proof [¬¬]-elim ∘ [¬∀]-to-[∃¬] ⦃ classical ⦄ ⦃ classical ⦄) [¬∃]-to-[∀¬] ∘ [¬]-preserves-[∧][∨]ᵣ) (nepx{x})) ∘ [¬∃]-to-[∀¬]

    instance
      surj-h : Surjective(h)
      Surjective.proof surj-h {z} with excluded-middle(∃(y ↦ Lone(y) ∧ Desc(f(g(z))) y))
      ... | [∨]-introₗ ([∃]-intro y ⦃ pxy ⦄)
        = [∃]-intro (g(z)) ⦃ symmetry(_≡_) (existence-decider-satisfaction-value(y ↦ Lone(y) ∧ Desc(f(g(z))) y) (\_ → f(g(z))) (\_ → g⁻¹(g(z))) unique-lone-descendant pxy) 🝖 inverseₗ(g)(g⁻¹) ⦄
      ... | [∨]-introᵣ nepx
        = [∨]-elim
          (\([∃]-intro x ⦃ p ⦄) → [∃]-intro x ⦃ symmetry(_≡_) (existence-decider-unsatisfaction-value(y ↦ Lone(y) ∧ Desc(f(x)) y) (\_ → f(x)) (\_ → g⁻¹(x)) ⦃ const-function ⦄ ⦃ intro(reflexivity(_≡_)) ⦄ \([∃]-intro xx ⦃ [∧]-intro pp₁ ([∃]-intro n ⦃ pp₂ ⦄) ⦄) → nepx ([∃]-intro xx ⦃ [∧]-intro (\{xxx} ppp → pp₁ ppp) ([∃]-intro (𝐒(n)) ⦃ congruence₁(f) ⦃ func-f ⦄ (congruence₁(g) ⦃ func-g ⦄ (symmetry(_≡_) p 🝖 pp₂)) ⦄) ⦄)) 🝖 p ⦄)
          (\p → [∃]-intro (g(z)) ⦃ symmetry(_≡_) (existence-decider-unsatisfaction-value(y ↦ Lone(y) ∧ Desc(f(g(z))) y) (\_ → f(g(z))) (\_ → g⁻¹(g(z))) ⦃ const-function ⦄ ⦃ intro(reflexivity(_≡_)) ⦄ nepx) 🝖 [⊥]-elim(p{1} (reflexivity(_≡_))) ⦄)
          (not-lone-desc nepx {z})
      {-TODO: How to define surj-h using existence-decider-fn-surjective? Should existence-decider-fn-surjective be more general?
      surj-h = existence-decider-fn-surjective
        (a ↦ b ↦ Lone(b) ∧ Desc(f(a))(b))
        (\x _ → f(x))
        (const ∘ invₗ-construction f g)
        unique-lone-descendant
        ⦃ intro (reflexivity(_≡_)) ⦄
        (\{z} → [∃]-intro (g(z)) ⦃ [∧]-intro
          (\{y} ([∧]-intro lone-y desc-y) → inverseₗ(g)(g⁻¹))
          -- ((\nepx → [⊥]-elim(nepx{z} ([∧]-intro (\{x} fxz → nepx{f(x)} ([∧]-intro (\{x'} p → {!!}) {!!})) ([∃]-intro 1 ⦃ reflexivity(_≡_) ⦄)))) ∘ [¬∃]-to-[∀¬])
          ((\nepx → Either.map1
              ((\([∃]-intro x ⦃ p ⦄) → {!!}) ∘ [∃]-map-proof [¬¬]-elim)
              (\p → [⊥]-elim(p{1} (reflexivity(_≡_))))
              (Either.map ([¬∀]-to-[∃¬] ⦃ classical ⦄ ⦃ classical ⦄) [¬∃]-to-[∀¬] ([¬]-preserves-[∧][∨]ᵣ (nepx{z})))
          ) ∘ [¬∃]-to-[∀¬])
        ⦄)
      -}

    instance
      inj-h : Injective(h)
      inj-h = existence-decider-fn-injective
        (a ↦ b ↦ Lone(b) ∧ Desc(f(a))(b))
        (\x _ → f(x))
        (const ∘ invₗ-construction f g)
        (\{x₁ x₂}{y₁ y₂} ([∧]-intro lone₁ desc₁) ([∧]-intro lone₂ desc₂) g⁻¹x₁g⁻¹x₂ →
          x₁            🝖[ _≡_ ]-[ inverᵣ-g⁻¹-specific lone₁ desc₁ ]-sym
          (g ∘ g⁻¹)(x₁) 🝖[ _≡_ ]-[ congruence₁(g) ⦃ func-g ⦄ g⁻¹x₁g⁻¹x₂ ]
          (g ∘ g⁻¹)(x₂) 🝖[ _≡_ ]-[ inverᵣ-g⁻¹-specific lone₂ desc₂ ]
          x₂            🝖-end
        )
        (\_ _ → Injective.proof inj-f)
        (\{
          {_} {_} {_}  ([∧]-intro lone₁ ([∃]-intro 𝟎       ⦃ desc₁ ⦄)) no g⁻¹x₁fx₂ → [⊥]-elim(lone₁ desc₁) ;
          {x₁}{x₂}{y₁} ([∧]-intro lone₁ ([∃]-intro (𝐒(n₁)) ⦃ desc₁ ⦄)) no g⁻¹x₁fx₂ → [⊥]-elim(no([∃]-intro y₁ ⦃ [∧]-intro lone₁ ([∃]-intro n₁ ⦃
            f(x₂)                      🝖[ _≡_ ]-[ g⁻¹x₁fx₂ ]-sym
            g⁻¹(x₁)                    🝖[ _≡_ ]-[ congruence₁(g⁻¹) (injective(f) ⦃ inj-f ⦄ desc₁) ]
            g⁻¹(g(((f ∘ g) ^ n₁)(y₁))) 🝖[ _≡_ ]-[ inverseₗ(g)(g⁻¹) ]
            ((f ∘ g) ^ n₁)(y₁)         🝖-end
          ⦄) ⦄))
        })

  instance
    [≼][≍]-antisymmetry : ⦃ _ : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ → Antisymmetry(_≼_ {ℓₑ}{ℓ})(_≍_)
    [≼][≍]-antisymmetry = intro [≼][≍]-antisymmetry-raw

  instance
    [≍]-reflexivity : Reflexivity(_≍_ {ℓₑ}{ℓ})
    Reflexivity.proof([≍]-reflexivity) = [∃]-intro(id) ⦃ [∧]-intro id-function id-bijective ⦄

  instance
    [≍]-symmetry : Symmetry(_≍_ {ℓₑ}{ℓ})
    Symmetry.proof [≍]-symmetry ([∃]-intro(f) ⦃ [∧]-intro f-function f-bijective ⦄) = ([∃]-intro(inv f) ⦃ [∧]-intro inv-function (inv-bijective ⦃ func = f-function ⦄) ⦄) where
      instance
        f-invertible : Invertible(f)
        f-invertible = bijective-to-invertible ⦃ bij = f-bijective ⦄

      instance
        invf-invertible : Invertible(inv f)
        ∃.witness invf-invertible = f
        ∃.proof invf-invertible = [∧]-intro f-function (Inverse-symmetry ([∧]-elimᵣ([∃]-proof f-invertible)))

  instance
    [≍]-transitivity : Transitivity(_≍_ {ℓₑ}{ℓ})
    Transitivity.proof([≍]-transitivity) ([∃]-intro(f) ⦃ [∧]-intro f-function f-bijective ⦄) ([∃]-intro(g) ⦃ [∧]-intro g-function g-bijective ⦄)
      = [∃]-intro(g ∘ f) ⦃ [∧]-intro
          ([∘]-function  {f = g}{g = f} ⦃ g-function ⦄ ⦃ f-function ⦄)
          ([∘]-bijective {f = g} ⦃ g-function ⦄ {g = f} ⦃ g-bijective ⦄ ⦃ f-bijective ⦄)
        ⦄

  instance
    [≍]-equivalence : Equivalence(_≍_ {ℓₑ}{ℓ})
    [≍]-equivalence = intro

  instance
    [≼]-reflexivity : Reflexivity(_≼_ {ℓₑ}{ℓ})
    Reflexivity.proof([≼]-reflexivity) = [∃]-intro(id) ⦃ [∧]-intro id-function id-injective ⦄

  instance
    [≼]-transitivity : Transitivity(_≼_ {ℓₑ}{ℓ})
    Transitivity.proof([≼]-transitivity) ([∃]-intro(f) ⦃ [∧]-intro f-function f-injective ⦄) ([∃]-intro(g) ⦃ [∧]-intro g-function g-injective ⦄)
      = [∃]-intro(g ∘ f) ⦃ [∧]-intro
          ([∘]-function  {f = g}{g = f} ⦃ g-function ⦄ ⦃ f-function ⦄)
          ([∘]-injective {f = g}{g = f} ⦃ g-injective ⦄ ⦃ f-injective ⦄)
        ⦄

  instance
    [≽]-reflexivity : Reflexivity(_≽_ {ℓₑ}{ℓ})
    Reflexivity.proof([≽]-reflexivity) = [∃]-intro(id) ⦃ [∧]-intro id-function id-surjective ⦄

  instance
    [≽]-transitivity : Transitivity(_≽_ {ℓₑ}{ℓ})
    Transitivity.proof([≽]-transitivity) ([∃]-intro(f) ⦃ [∧]-intro f-function f-surjective ⦄) ([∃]-intro(g) ⦃ [∧]-intro g-function g-surjective ⦄)
      = [∃]-intro(g ∘ f) ⦃ [∧]-intro
          ([∘]-function  {f = g}{g = f} ⦃ g-function ⦄ ⦃ f-function ⦄)
          ([∘]-surjective {f = g} ⦃ g-function ⦄ {g = f} ⦃ g-surjective ⦄ ⦃ f-surjective ⦄)
        ⦄

  module _  where
    -- This is variant of the "extensional axiom of choice" and is unprovable in Agda, though it is a possible axiom.
    -- A proof of `(A ≽ B)` means that a right inverse exist, but if the surjection is non-injective (it could be in general), then the right inverse is not a function (two equal values in the codomain of the surjection may point to two inequal objects in the domain).
    -- Example:
    --   For X: Set, Y: Set, f: X → Y, a: X, b: X, c₁: Y, c₂: Y
    --   Assume:
    --     X = {a,b}
    --     Y = {c₁,c₂}
    --     a ≢ b
    --     c₁ ≡ c₂
    --     f(a) = c₁
    --     f(b) = c₂
    --   This means that f is surjective (maps to both c₁ and c₂) but not injective ((c₁ ≡ c₂) implies (f(a) ≡ f(b)) implies (a ≡ b) which is false).
    --   Then an inverse f⁻¹ to f can be constructed from the witnesses in surjectivity:
    --     f⁻¹: Y → X
    --     f⁻¹(c₁) = a
    --     f⁻¹(c₂) = b
    --   f⁻¹ is obviously injective, but it is also not a function: ((c₁ ≡ c₂) would imply (a ≡ b) if it were a function, but that is false).
    --   This example shows that not all surjections are injective.
    --   But looking at the example, there are functions that are injective:
    --     g₁: Y → X
    --     g₁(c₁) = a
    --     g₁(c₂) = a
    --
    --     g₂: Y → X
    --     g₂(c₁) = b
    --     g₂(c₂) = b
    --   They are, because: ((a ≡ a) implies (g₁(c₁) ≡ g₁(c₂)) implies (c₁ ≡ c₂) which is true).
    --   and              : ((b ≡ b) implies (g₂(c₁) ≡ g₂(c₂)) implies (c₁ ≡ c₂) which is true).
    --   This is a simplified example for finite sets, and a restriction of this proposition for finite sets is actually provable because it is possible to enumerate all functions up to function extensionality.
    --   The real problem comes when the sets are non-finite because then, there is no general way to enumerate the elements. How would an injection be chosen in this case?
    -- Note that if the surjection is injective, then it is a bijection, and therefore also an injection.
    record SurjectionInjectionChoice (A : Setoid{ℓₑ₁}{ℓ₁}) (B : Setoid{ℓₑ₂}{ℓ₂}) : Stmt{ℓₑ₁ Lvl.⊔ ℓ₁ Lvl.⊔ ℓₑ₂ Lvl.⊔ ℓ₂} where
      constructor intro
      field proof : (A ≽ B) → (B ≼ A)
    open SurjectionInjectionChoice ⦃ … ⦄ using () renaming (proof to [≽]-to-[≼]) public

    record SurjectionInvertibleFunctionChoice (A : Setoid{ℓₑ₁}{ℓ₁}) (B : Setoid{ℓₑ₂}{ℓ₂}) : Stmt{ℓₑ₁ Lvl.⊔ ℓ₁ Lvl.⊔ ℓₑ₂ Lvl.⊔ ℓ₂} where
      constructor intro
      field
        invertibleᵣ : ∀{f : ∃.witness A → ∃.witness B} → Surjective(f) → Invertibleᵣ(f)
        function    : ∀{f : ∃.witness A → ∃.witness B}{surj : Surjective(f)} → Function(∃.witness(invertibleᵣ surj))

  module _ ⦃ classical : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ ⦃ surjChoice-ab : SurjectionInjectionChoice A B ⦄ ⦃ surjChoice-ba : SurjectionInjectionChoice B A ⦄ where
    [≽][≍]-antisymmetry-raw : (A ≽ B) → (B ≽ A) → (A ≍ B)
    [≽][≍]-antisymmetry-raw ab ba = [≼][≍]-antisymmetry-raw ([≽]-to-[≼] ba) ([≽]-to-[≼] ab)

  module _ ⦃ classical : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ ⦃ surjChoice-ab : SurjectionInjectionChoice A B ⦄ where
    [≼][≽][≍]-antisymmetry-raw : (A ≼ B) → (A ≽ B) → (A ≍ B)
    [≼][≽][≍]-antisymmetry-raw lesser greater = [≼][≍]-antisymmetry-raw lesser ([≽]-to-[≼] greater)

  module _ ⦃ classical : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ ⦃ surjChoice : ∀{ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂}{A : Setoid{ℓₑ₁}{ℓ₁}}{B : Setoid{ℓₑ₂}{ℓ₂}} → SurjectionInjectionChoice A B ⦄ where
    instance
      [≽][≍]-antisymmetry : Antisymmetry(_≽_ {ℓₑ}{ℓ})(_≍_)
      [≽][≍]-antisymmetry = intro [≽][≍]-antisymmetry-raw

    -- TODO: Totality of (_≼_).  Is this difficult to prove?
    -- [≼]-total : ((A ≼ B) ∨ (B ≼ A))

  -- TODO: Move
  global-equiv : ∀{ℓ}{T : Type{ℓ}} → Equiv{ℓₑ}(T)
  Equiv._≡_                                   global-equiv  = const(const Unit)
  Equivalence.reflexivity  (Equiv.equivalence global-equiv) = intro <>
  Equivalence.symmetry     (Equiv.equivalence global-equiv) = intro(const <>)
  Equivalence.transitivity (Equiv.equivalence global-equiv) = intro(const(const <>))

  [≼]-to-[≽]-for-inhabited-to-excluded-middle : (∀{ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂}{A : Setoid{ℓₑ₁}{ℓ₁}}{B : Setoid{ℓₑ₂}{ℓ₂}} → ⦃ ◊([∃]-witness A) ⦄ → (A ≼ B) → (B ≽ A)) → (∀{P : Type{ℓ}} → Classical(P))
  Classical.excluded-middle ([≼]-to-[≽]-for-inhabited-to-excluded-middle p {P = P}) = proof where
    open import Data.Boolean
    open import Data.Option
    open import Data.Option.Setoid
    open import Relator.Equals.Proofs.Equivalence
    f : Option(◊ P) → Bool
    f (Option.Some _) = 𝑇
    f Option.None     = 𝐹

    instance
      equiv-bool : Equiv(Bool)
      equiv-bool = [≡]-equiv

    instance
      equiv-pos-P : Equiv{Lvl.𝟎}(◊ P)
      equiv-pos-P = global-equiv

    func-f : Function(f)
    Function.congruence func-f {None}   {None}   _ = reflexivity(_≡_ ⦃ [≡]-equiv ⦄)
    Function.congruence func-f {Some _} {Some _} _ = reflexivity(_≡_ ⦃ [≡]-equiv ⦄)

    inj-f : Injective(f)
    Injective.proof inj-f {None}   {None}   _ = <>
    Injective.proof inj-f {Some _} {Some _} _ = <>

    surjection : ([∃]-intro Bool ⦃ [≡]-equiv ⦄) ≽ ([∃]-intro (Option(◊ P)))
    surjection = p ⦃ intro ⦃ None ⦄ ⦄ ([∃]-intro f ⦃ [∧]-intro func-f inj-f ⦄)

    g : Bool → Option(◊ P)
    g = [∃]-witness surjection

    g-value-elim : ∀{y} → (g(𝑇) ≡ y) → (g(𝐹) ≡ y) → (∀{b} → (g(b) ≡ y))
    g-value-elim l r {𝑇} = l
    g-value-elim l r {𝐹} = r

    open Equiv(Option-equiv ⦃ equiv-pos-P ⦄) using () renaming (transitivity to Option-trans ; symmetry to Option-sym)
    proof : (P ∨ ¬ P)
    proof with g(𝐹) | g(𝑇) | (\p → Surjective.proof ([∧]-elimᵣ([∃]-proof surjection)) {Some(intro ⦃ p ⦄)}) | g-value-elim{Option.None}
    ... | Some l | Some r | _    | _ = [∨]-introₗ (◊.existence l)
    ... | Some l | None   | _    | _ = [∨]-introₗ (◊.existence l)
    ... | None   | Some r | _    | _ = [∨]-introₗ (◊.existence r)
    ... | None   | None   | surj | tttest = [∨]-introᵣ
      (\p →
        empty(transitivity _ ⦃ Option-trans ⦄ {Some(intro ⦃ p ⦄)}{g([∃]-witness(surj p))}{None} (symmetry _ ⦃ Option-sym ⦄ {g([∃]-witness(surj p))}{Some(intro ⦃ p ⦄)} ([∃]-proof(surj p))) (tttest <> <>))
      )
      {-
        Some(intro ⦃ p ⦄)      🝖[ Equiv._≡_ Option-equiv ]-[ [∃]-proof(surj p) ]-sym
        g([∃]-witness(surj p)) 🝖[ Equiv._≡_ Option-equiv ]-[ tttest <> <> ]
        None                   🝖[ Equiv._≡_ Option-equiv ]-end
      -}

  {-module _ ⦃ surjChoice : ∀{A B : Setoid{ℓ}} → SurjectionInjectionChoice A B ⦄ where
    surjection-injection-choice-to-excluded-middle : ∀{P : Type{ℓ}} → Classical(P)
    Classical.excluded-middle (surjection-injection-choice-to-excluded-middle {P = P}) = {!!}
  -}


text:
------------------------------------------------------------------------------
-- Testing the conjectures inside a @where@ clause
------------------------------------------------------------------------------

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

module Where2 where

infixl 6 _+_
infix  4 _≡_

postulate
  D      : Set
  zero   : D
  succ   : D → D
  _≡_    : D → D → Set

data N : D → Set where
  nzero : N zero
  nsucc : ∀ {n} → N n → N (succ n)

N-ind : (A : D → Set) →
        A zero →
        (∀ {n} → A n → A (succ n)) →
        ∀ {n} → N n → A n
N-ind A A0 h nzero      = A0
N-ind A A0 h (nsucc Nn) = h (N-ind A A0 h Nn)

postulate
  _+_  : D → D → D
  +-0x : ∀ n → zero + n     ≡ n
  +-Sx : ∀ m n → succ m + n ≡ succ (m + n)
{-# ATP axioms +-0x +-Sx #-}

+-assoc : ∀ {m n o} → N m → N n → N o → m + n + o ≡ m + (n + o)
+-assoc {n = n} {o} Nm Nn No = N-ind A A0 is Nm
  where
  A : D → Set
  A i = i + n + o ≡ i + (n + o)

  postulate A0 : zero + n + o ≡ zero + (n + o)
  {-# ATP prove A0 #-}

  postulate is : ∀ {i} → i + n + o ≡ i + (n + o) →
                 succ i + n + o ≡ succ i + (n + o)
  {-# ATP prove is #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- Andreas, 2017-07-28, issue #883
-- Was fixed by making rewrite not go through abstract syntax.

open import Agda.Builtin.Equality

test : (A : Set) → (a : A) → A
test A a rewrite refl {x = a} = a

-- WAS:
-- Setω !=< Level of type Setω
-- when checking that the type
-- (A : Set) (a w : A) →
-- _≡_ {_6 A w} {_A_9 A w} (_x_10 A w) (_x_10 A w) → A
-- of the generated with function is well-formed

-- Should succeed.