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

open import LogicalFormulae
open import Groups.Lemmas
open import Groups.Definition
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Orders.Total.Definition
open import Rings.IntegralDomains.Definition

module Rings.Orders.Total.Lemmas {n m p : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} {pOrderRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pOrderRing) where

open Ring R
open Group additiveGroup
open Setoid S
open SetoidPartialOrder pOrder
open TotallyOrderedRing order
open SetoidTotalOrder total
open PartiallyOrderedRing pOrderRing
open import Rings.Lemmas R
open import Rings.Orders.Partial.Lemmas pOrderRing

abstract

  lemm2 : (a : A) → a < 0G → 0G < inverse a
  lemm2 a a<0 with totality 0R (inverse a)
  lemm2 a a<0 | inl (inl 0<-a) = 0<-a
  lemm2 a a<0 | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (<WellDefined (invLeft {a}) (identLeft {a}) (orderRespectsAddition -a<0 a)) a<0))
  lemm2 a a<0 | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq identRight) t) (Equivalence.reflexive eq) a<0))
    where
      t : a + 0G ∼ 0G
      t = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) 0=-a) (invRight {a})

  lemm2' : (a : A) → 0G < a → inverse a < 0G
  lemm2' a 0<a with totality 0R (inverse a)
  lemm2' a 0<a | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<a (<WellDefined (identLeft {a}) (invLeft {a}) (orderRespectsAddition 0<-a a))))
  lemm2' a 0<a | inl (inr -a<0) = -a<0
  lemm2' a 0<a | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq identRight) t) 0<a))
    where
      t : a + 0G ∼ 0G
      t = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) 0=-a) (invRight {a})

  ringMinusFlipsOrder : {x : A} → (Ring.0R R) < x → (Group.inverse (Ring.additiveGroup R) x) < (Ring.0R R)
  ringMinusFlipsOrder {x = x} 0<x with totality (Ring.0R R) (Group.inverse (Ring.additiveGroup R) x)
  ringMinusFlipsOrder {x} 0<x | inl (inl 0<inv) = exFalso (SetoidPartialOrder.irreflexive pOrder bad')
    where
    bad : (Group.0G (Ring.additiveGroup R) + Group.0G (Ring.additiveGroup R)) < (x + Group.inverse (Ring.additiveGroup R) x)
    bad = ringAddInequalities 0<x 0<inv
    bad' : (Group.0G (Ring.additiveGroup R)) < (Group.0G (Ring.additiveGroup R))
    bad' = SetoidPartialOrder.<WellDefined pOrder (Group.identRight (Ring.additiveGroup R)) (Group.invRight (Ring.additiveGroup R)) bad
  ringMinusFlipsOrder {x} 0<x | inl (inr inv<0) = inv<0
  ringMinusFlipsOrder {x} 0<x | inr 0=inv = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (Equivalence.reflexive (Setoid.eq S)) (groupLemmaMove0G (Ring.additiveGroup R) 0=inv) 0<x))

  ringMinusFlipsOrder' : {x : A} → (Group.inverse (Ring.additiveGroup R) x) < (Ring.0R R) → (Ring.0R R) < x
  ringMinusFlipsOrder' {x} -x<0 with totality (Ring.0R R) x
  ringMinusFlipsOrder' {x} -x<0 | inl (inl 0<x) = 0<x
  ringMinusFlipsOrder' {x} -x<0 | inl (inr x<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (Group.invLeft (Ring.additiveGroup R)) (Group.identRight (Ring.additiveGroup R)) bad))
    where
    bad : ((Group.inverse (Ring.additiveGroup R) x) + x) < (Group.0G (Ring.additiveGroup R) + Group.0G (Ring.additiveGroup R))
    bad = ringAddInequalities -x<0 x<0
  ringMinusFlipsOrder' {x} -x<0 | inr 0=x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (symmetric (groupLemmaMove0G' (Ring.additiveGroup R) (symmetric 0=x))) (Equivalence.reflexive (Setoid.eq S)) -x<0))
    where
    open Equivalence eq

  ringMinusFlipsOrder'' : {x : A} → x < (Ring.0R R) → (Ring.0R R) < Group.inverse (Ring.additiveGroup R) x
  ringMinusFlipsOrder'' {x} x<0 = ringMinusFlipsOrder' (SetoidPartialOrder.<WellDefined pOrder {x} {Group.inverse (Ring.additiveGroup R) (Group.inverse (Ring.additiveGroup R) x)} {Ring.0R R} {Ring.0R R} (Equivalence.symmetric (Setoid.eq S) (invInv (Ring.additiveGroup R))) (Equivalence.reflexive (Setoid.eq S)) x<0)

  ringMinusFlipsOrder''' : {x : A} → (Ring.0R R) < (Group.inverse (Ring.additiveGroup R) x) → x < (Ring.0R R)
  ringMinusFlipsOrder''' {x} 0<-x = SetoidPartialOrder.<WellDefined pOrder (invInv (Ring.additiveGroup R)) (Equivalence.reflexive (Setoid.eq S)) (ringMinusFlipsOrder 0<-x)

  ringCanCancelPositive : {x y c : A} → (Ring.0R R) < c → (x * c) < (y * c) → x < y
  ringCanCancelPositive {x} {y} {c} 0<c xc<yc = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.identRight additiveGroup))) q''
    where
      open Equivalence (Setoid.eq S)
      have : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
      have = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) reflexive (orderRespectsAddition xc<yc (Group.inverse additiveGroup _))
      p1 : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
      p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (symmetric (Equivalence.transitive eq (*Commutative) (Equivalence.transitive eq ringMinusExtracts (inverseWellDefined additiveGroup *Commutative))))) have
      q : 0R < ((y + Group.inverse additiveGroup x) * c)
      q = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq (Equivalence.transitive eq (Group.+WellDefined additiveGroup *Commutative *Commutative) (symmetric *DistributesOver+)) *Commutative) p1
      q' : 0R < (y + Group.inverse additiveGroup x)
      q' with totality 0R (y + Group.inverse additiveGroup x)
      q' | inl (inl pr) = pr
      q' | inl (inr y-x<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq *Commutative (Ring.timesZero R)) k))
        where
          f : ((y + inverse x) + (inverse (y + inverse x))) < (0G + inverse (y + inverse x))
          f = orderRespectsAddition y-x<0 _
          g : 0G < inverse (y + inverse x)
          g = SetoidPartialOrder.<WellDefined pOrder invRight identLeft f
          h : (0G * c) < ((inverse (y + inverse x)) * c)
          h = ringCanMultiplyByPositive 0<c g
          i : (0R + (0G * c)) < (((y + inverse x) * c) + ((inverse (y + inverse x)) * c))
          i = ringAddInequalities q h
          j : 0R < (((y + inverse x) + (inverse (y + inverse x))) * c)
          j = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq identLeft (Equivalence.transitive eq *Commutative (Ring.timesZero R))) (symmetric (Equivalence.transitive eq *Commutative (Equivalence.transitive eq *DistributesOver+ (Group.+WellDefined additiveGroup *Commutative *Commutative)))) i
          k : 0R < (0R * c)
          k = SetoidPartialOrder.<WellDefined pOrder reflexive (*WellDefined invRight reflexive) j
      q' | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (*WellDefined x=y reflexive) reflexive xc<yc))
        where
          f : inverse 0G ∼ inverse (y + inverse x)
          f = inverseWellDefined additiveGroup 0=y-x
          g : 0G ∼ (inverse y) + x
          g = Equivalence.transitive eq (symmetric (invIdent additiveGroup)) (Equivalence.transitive eq f (Equivalence.transitive eq (Equivalence.transitive eq (invContravariant additiveGroup) groupIsAbelian) (+WellDefined reflexive (invInv additiveGroup))))
          x=y : x ∼ y
          x=y = transferToRight additiveGroup (symmetric (Equivalence.transitive eq g groupIsAbelian))
      q'' : (0R + x) < ((y + Group.inverse additiveGroup x) + x)
      q'' = orderRespectsAddition q' x

  ringCanCancelNegative : {x y c : A} → c < (Ring.0R R) → (x * c) < (y * c) → y < x
  ringCanCancelNegative {x} {y} {c} c<0 xc<yc = r
    where
      open Equivalence eq
      p0 : 0R < ((y * c) + inverse (x * c))
      p0 = SetoidPartialOrder.<WellDefined pOrder invRight reflexive (orderRespectsAddition xc<yc (inverse (x * c)))
      p1 : 0R < ((y * c) + ((inverse x) * c))
      p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (Equivalence.transitive eq (inverseWellDefined additiveGroup *Commutative) (Equivalence.transitive eq (symmetric ringMinusExtracts) *Commutative))) p0
      p2 : 0R < ((y + inverse x) * c)
      p2 = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq (Group.+WellDefined additiveGroup *Commutative *Commutative) (Equivalence.transitive eq (symmetric *DistributesOver+) *Commutative)) p1
      q : (y + inverse x) < 0R
      q with totality 0R (y + inverse x)
      q | inl (inl pr) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder bad c<0))
        where
          bad : 0R < c
          bad = ringCanCancelPositive pr (SetoidPartialOrder.<WellDefined pOrder (symmetric (Equivalence.transitive eq *Commutative (Ring.timesZero R))) *Commutative p2)
      q | inl (inr pr) = pr
      q | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (*WellDefined x=y reflexive) reflexive xc<yc))
        where
          x=y : x ∼ y
          x=y = Equivalence.transitive eq (symmetric identLeft) (Equivalence.transitive eq (Group.+WellDefined additiveGroup 0=y-x reflexive) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive invLeft) identRight)))
      r : y < x
      r = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (invLeft)) identRight)) (Group.identLeft additiveGroup) (orderRespectsAddition q x)

  posTimesNeg : (a b : A) → (0G < a) → (b < 0G) → (a * b) < 0G
  posTimesNeg a b 0<a b<0 with orderRespectsMultiplication 0<a (lemm2 _ b<0)
  ... | bl = <WellDefined (invTwice additiveGroup _) (Equivalence.reflexive eq) (lemm2' _ (<WellDefined (Equivalence.reflexive eq) ringMinusExtracts bl))

  negTimesPos : (a b : A) → (a < 0G) → (b < 0G) → 0G < (a * b)
  negTimesPos a b a<0 b<0 with orderRespectsMultiplication (lemm2 _ a<0) (lemm2 _ b<0)
  ... | bl = <WellDefined (Equivalence.reflexive eq) twoNegativesTimes bl

  halvePositive : (a : A) → 0R < (a + a) → 0R < a
  halvePositive a 0<2a with totality 0R a
  halvePositive a 0<2a | inl (inl x) = x
  halvePositive a 0<2a | inl (inr a<0) = exFalso (irreflexive {a + a} (SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.reflexive eq) identRight (ringAddInequalities a<0 a<0)) 0<2a))
  halvePositive a 0<2a | inr x = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq x) (Equivalence.symmetric eq x)) identRight) 0<2a))

  halvePositive' : {a b : A} → (a + a) ∼ b → 0R < b → 0R < a
  halvePositive' {a} {b} pr 0<b = halvePositive a (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<b)

  0<1 : (0R ∼ 1R → False) → 0R < 1R
  0<1 0!=1 with totality 0R 1R
  0<1 0!=1 | inl (inl x) = x
  0<1 0!=1 | inl (inr x) = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq twoNegativesTimes identIsIdent) (orderRespectsMultiplication (lemm2 1R x) (lemm2 1R x))
  0<1 0!=1 | inr x = exFalso (0!=1 x)

  1<0False : (1R < 0R) → False
  1<0False 1<0 with orderRespectsMultiplication (lemm2 _ 1<0) (lemm2 _ 1<0)
  ... | bl = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder 1<0 (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (twoNegativesTimes) identIsIdent) bl)))

  orderedImpliesCharNot2 : (0R ∼ 1R → False) → 1R + 1R ∼ 0R → False
  orderedImpliesCharNot2 0!=1 x = irreflexive (<WellDefined (identRight {0R}) x (ringAddInequalities (0<1 0!=1) (0<1 0!=1)))

open import Rings.InitialRing R
open Equivalence eq

fromNPreservesOrder' : (0R ∼ 1R → False) → {a b : ℕ} → (fromN a) < (fromN b) → a <N b
fromNPreservesOrder' nontrivial {a} {b} a<b with TotalOrder.totality ℕTotalOrder a b
... | inl (inl x) = x
... | inl (inr x) = exFalso (irreflexive (<Transitive a<b (fromNPreservesOrder (0<1 nontrivial) x)))
... | inr x = exFalso (irreflexive (<WellDefined (fromNWellDefined x) reflexive a<b))

reciprocalPositive : (a b : A) → .(0<a : 0R < a) → (a * b ∼ 1R) → 0R < b
reciprocalPositive a 1/a 0<a ab=1 with totality 0G 1/a
... | inl (inl x) = x
... | inl (inr x) = exFalso (1<0False (<WellDefined (transitive *Commutative ab=1) timesZero' (ringCanMultiplyByPositive 0<a x)))
... | inr x = exFalso (anyComparisonImpliesNontrivial 0<a (transitive (transitive (symmetric timesZero) (*WellDefined reflexive x)) ab=1))

reciprocalPositive' : (a b : A) → .(0<a : 0R < a) → (b * a ∼ 1R) → 0R < b
reciprocalPositive' a 1/a 0<a ab=1 = reciprocalPositive a 1/a 0<a (transitive *Commutative ab=1)

reciprocal<1 : (a b : A) → .(1<a : 1R < a) → (a * b ∼ 1R) → b < 1R
reciprocal<1 a b 0<a ab=1 with totality b 1R
... | inl (inl x) = x
... | inr b=1 = exFalso (irreflexive (<WellDefined (symmetric ab=1) (transitive (symmetric identIsIdent) (transitive *Commutative ((*WellDefined reflexive (symmetric b=1))))) 0<a))
... | inl (inr x) = exFalso (irreflexive (<WellDefined identIsIdent ab=1 (ringMultiplyPositives (0<1 (anyComparisonImpliesNontrivial 0<a)) (0<1 (anyComparisonImpliesNontrivial 0<a)) 0<a x)))

isIntDom : (nonempty : 1R ∼ 0R → False) → IntegralDomain R
IntegralDomain.intDom (isIntDom n) {a} {b} ab=0 a!=0 with totality 0R b
... | inr 0=b = symmetric 0=b
IntegralDomain.intDom (isIntDom n) {a} {b} ab=0 a!=0 | inl (inl 0<b) with totality 0R a
... | inl (inl x) = exFalso (irreflexive (<WellDefined reflexive ab=0 (orderRespectsMultiplication x 0<b)))
... | inl (inr x) = exFalso (irreflexive (<WellDefined ab=0 timesZero' (ringCanMultiplyByPositive 0<b x)))
... | inr x = exFalso (a!=0 (symmetric x))
IntegralDomain.intDom (isIntDom n) {a} {b} ab=0 a!=0 | inl (inr b<0) with totality 0R a
... | inl (inl x) = exFalso (irreflexive (<WellDefined (transitive *Commutative ab=0) timesZero' (ringCanMultiplyByPositive x b<0)))
... | inl (inr x) = exFalso (irreflexive (<WellDefined reflexive (transitive twoNegativesTimes ab=0) (orderRespectsMultiplication (lemm2 a x) (lemm2 b b<0))))
... | inr x = exFalso (a!=0 (symmetric x))
IntegralDomain.nontrivial (isIntDom n) = n


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

-- This is a utility module.
module Utils where

open import Induction.WellFounded as Wf
open import Data.List as List
open import Data.List.All
open import Data.Nat
open import Data.Maybe
open import Data.Product as ,
open import Data.Empty
open import Function

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

infix 6 _!
_! : ∀ {a} {A : Set a} → A → List A
a ! = a ∷ []

infixl 5 _‣_
_‣_ : ∀ {a} {A : Set a} → List A → List A → List A
l₁ ‣ l₂ = l₂ ++ l₁

lookupOpt : ∀ {a} {A : Set a} → List A → ℕ → Maybe A
lookupOpt [] n            = nothing
lookupOpt (x ∷ l) zero    = just x
lookupOpt (x ∷ l) (suc n) = lookupOpt l n

module _ {a} {A : Set a} where
  lookupOpt-map-inv : ∀ {b} {B : Set b} {f : A → B} l {n e} →
                        lookupOpt (List.map f l) n ≡ just e →
                        ∃[ e' ] (e ≡ f e' × lookupOpt l n ≡ just e')
  lookupOpt-map-inv [] {n} ()
  lookupOpt-map-inv (x ∷ l) {zero} refl = x , refl , refl
  lookupOpt-map-inv (x ∷ l) {suc n} eq  = lookupOpt-map-inv l eq

  lookupOpt-map : ∀ {b} {B : Set b} l (f : A → B) {n e} →
                    lookupOpt l n ≡ just e →
                    lookupOpt (List.map f l) n ≡ just (f e)
  lookupOpt-map [] f ()
  lookupOpt-map (x ∷ l) f {zero} refl = refl
  lookupOpt-map (x ∷ l) f {suc n} eq  = lookupOpt-map l f eq

  lookupOpt-All : ∀ {b} {P : A → Set b} {l n e} →
                    lookupOpt l n ≡ just e →
                    All P l →
                    P e
  lookupOpt-All {n = n} () []
  lookupOpt-All {n = zero} refl (px ∷ all) = px
  lookupOpt-All {n = suc n} eq (px ∷ all)  = lookupOpt-All eq all

  lookupOpt-app₁ : ∀ (l₁ l₂ : List A) {n} →
                     n < length l₁ →
                     lookupOpt (l₁ ++ l₂) n ≡ lookupOpt l₁ n
  lookupOpt-app₁ [] l₂ {n} ()
  lookupOpt-app₁ (x ∷ l₁) l₂ {zero} (s≤s n<l) = refl
  lookupOpt-app₁ (x ∷ l₁) l₂ {suc n} (s≤s n<l) = lookupOpt-app₁ l₁ l₂ n<l

  lookupOpt-app₂ : ∀ (l₁ l₂ : List A) n →
                     lookupOpt (l₁ ++ l₂) (length l₁ + n) ≡ lookupOpt l₂ n
  lookupOpt-app₂ [] l₂ n       = refl
  lookupOpt-app₂ (x ∷ l₁) l₂ n = lookupOpt-app₂ l₁ l₂ n

repeat : ∀ {a} {A : Set a} → ℕ → (f : A → A) → A → A
repeat zero f = id
repeat (suc n) f = f ∘ (repeat n f)

≤?-yes : ∀ {m n} (m≤n : m ≤ n) → (m ≤? n) ≡ yes m≤n
≤?-yes z≤n           = refl
≤?-yes (s≤s m≤n)
  rewrite ≤?-yes m≤n = refl

≤?-no : ∀ {m n} (m>n : ¬ m ≤ n) → ∃ λ ¬p → (m ≤? n) ≡ no ¬p
≤?-no {m} {n} m>n with m ≤? n
... | yes p = ⊥-elim $ m>n p
... | no _  = -, refl

module Measure {a b ℓ} {A : Set a} {B : Set b} {_≺_ : Rel A ℓ}
               (≺-wf : WellFounded _≺_)
               (m : B → A) where

  open import Level using () renaming (zero to lzero)
  import Relation.Binary.Reasoning.Base.Triple as Triple
  open Wf.Inverse-image {_<_ = _≺_} m using (wellFounded)

  open Wf.All (wellFounded ≺-wf) lzero using (wfRec) public

module LexicographicMeasure {a b c d ℓ₁ ℓ₂}
                            {A : Set a} {B : A → Set b}
                            {C : Set c} {D : C → Set d}
                            {_≺A_ : Rel A ℓ₁}
                            {[_]_≺B_ : ∀ x → Rel (B x) ℓ₂}
                            (≺A-wf : WellFounded _≺A_)
                            (≺B-wf : ∀ {x} → WellFounded ([ x ]_≺B_))
                            (mC : C → A)
                            (mD : ∀ {c} → D c → B (mC c)) where
  open import Level using () renaming (zero to lzero)
  module Lex = Wf.Lexicographic _≺A_ [_]_≺B_
  open Lex renaming (wellFounded to lex-wf ; _<_ to _≺′_)
  open Lex using (left ; right) public
  open Wf.Inverse-image renaming (wellFounded to m-wf)

  measure : Σ C D → Σ A B
  measure (c , d) = mC c , mD d

  ΣAB-wf : WellFounded _≺′_
  ΣAB-wf = lex-wf ≺A-wf ≺B-wf

  infix 3 _≺_
  _≺_ = _≺′_ on ,.map mC mD

  measure-wf : WellFounded _≺_
  measure-wf = m-wf measure ΣAB-wf

  open Wf.All measure-wf lzero using (wfRec) public

ext: agda


text:
-- Andreas, 2015-02-24

data N : Set where
  zero : N
  suc  : N → N

data Sing : (n : N) → Set where
  sing : ∀ n → Sing n

data D : Set → Set where
  c : ∀ n → D (Sing n)

test : (A : Set) → D A → N
test .(Sing n) (c n) = n

-- this should crash Epic as long as n is considered forced in constructor c

-- should succeed now


text:
{- Cubical Agda with K

This file demonstrates the incompatibility of the --cubical
and --with-K flags, relying on the well-known incosistency of K with
univalence.

The --safe flag can be used to prevent accidentally mixing such
incompatible flags.

-}

{-# OPTIONS --cubical --no-import-sorts --with-K #-}

module Cubical.WithK where

open import Cubical.Data.Equality
open import Cubical.Data.Bool
open import Cubical.Data.Empty

private
 variable
  ℓ : Level
  A : Type ℓ
  x y : A

uip : (prf : x ≡p x) → prf ≡c reflp
uip reflp i = reflp

transport-uip : (prf : A ≡p A) → transport (ptoc prf) x ≡c x
transport-uip {x = x} prf =
  cong (λ m → transport (ptoc m) x) (uip prf) ∙ transportRefl x

transport-not : transport (ptoc (ctop notEq)) true ≡c false
transport-not = cong (λ a → transport a true) (ptoc-ctop notEq)

false-true : false ≡c true
false-true = sym transport-not ∙ transport-uip (ctop notEq)

absurd : (X : Type) → X
absurd X = transport (cong sel false-true) true
  where
    sel : Bool → Type
    sel false = Bool
    sel true = X

inconsistency : ⊥
inconsistency = absurd ⊥

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:
{-# OPTIONS --without-K --rewriting #-}

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

module lib.types.Join  where

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

  *-span : Span
  *-span = span A B (A × B) fst snd

  infix 80 _*_

  _*_ : Type _
  _*_ = Pushout *-span

module JoinElim {i j} {A : Type i} {B : Type j} {k} {P : A * B → Type k}
  (left* : (a : A) → P (left a)) (right* : (b : B) → P (right b))
  (glue* : (ab : A × B) → left* (fst ab) == right* (snd ab) [ P ↓ glue ab ])
  = PushoutElim left* right* glue*
open JoinElim public using () renaming (f to Join-elim)

module JoinRec {i j} {A : Type i} {B : Type j} {k} {D : Type k}
  (left* : (a : A) → D) (right* : (b : B) → D)
  (glue* : (ab : A × B) → left* (fst ab) == right* (snd ab))
  = PushoutRec left* right* glue*
open JoinRec public using () renaming (f to Join-rec)

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

  ⊙*-span : ⊙Span
  ⊙*-span = ⊙span X Y (X ⊙× Y) ⊙fst ⊙snd

  infix 80 _⊙*_

  _⊙*_ : Ptd _
  _⊙*_ = ⊙Pushout ⊙*-span

module _ {i i' j j'} {A : Type i} {A' : Type i'} {B : Type j} {B' : Type j'}
  (eqA : A ≃ A') (eqB : B ≃ B') where

  *-span-emap : SpanEquiv (*-span A B) (*-span A' B')
  *-span-emap = ( span-map (fst eqA) (fst eqB) (×-fmap (fst eqA) (fst eqB)) (comm-sqr λ _ → idp) (comm-sqr λ _ → idp)
                , snd eqA , snd eqB , ×-isemap (snd eqA) (snd eqB))

  *-emap : A * B ≃ A' * B'
  *-emap = Pushout-emap *-span-emap

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

  ⊙*-emap : X ⊙≃ X' → Y ⊙≃ Y' → X ⊙* Y ⊙≃ X' ⊙* Y'
  ⊙*-emap ⊙eqX ⊙eqY = ≃-to-⊙≃ (*-emap (⊙≃-to-≃ ⊙eqX) (⊙≃-to-≃ ⊙eqY)) (ap left (snd (⊙–> ⊙eqX)))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Auto.Prelude where

open import Agda.Primitive public
  using    (Level)

data ⊥ : Set where

¬ : Set → Set
¬ A = A → ⊥

⊥-e : (A : Set) → ⊥ → A
⊥-e A ()

record ⊤ : Set where

record _∧_ (A B : Set) : Set where
 constructor ∧-i
 field fst : A
       snd : B

data _∨_ (A B : Set) : Set where
 ∨-i₁ : A → A ∨ B
 ∨-i₂ : B → A ∨ B

∨-e : (A B C : Set) → A ∨ B → (A → C) → (B → C) → C
∨-e A B C (∨-i₁ x) h₁ h₂ = h₁ x
∨-e A B C (∨-i₂ x) h₁ h₂ = h₂ x

data Π (A : Set) (F : A → Set) : Set where
  fun : ((a : A) → F a) → Π A F

record Σ (X : Set) (P : X → Set) : Set where
 constructor Σ-i
 field wit : X
       prf : P wit

data ℕ : Set where
 zero : ℕ
 succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero   + n = n
succ m + n = succ (m + n)

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (succ n)
  suc  : ∀ {n} → Fin n → Fin (succ n)

data List (X : Set) : Set where
  []  : List X
  _∷_ : X → List X → List X

_++_ : {X : Set} → List X → List X → List X
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data Vec (X : Set) : ℕ → Set where
  []  : Vec X zero
  _∷_ : ∀ {n} → X → Vec X n → Vec X (succ n)

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

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

subst : {i j : Level} {X : Set i} → (P : X → Set j) → (x y : X) → y ≡ x → P x → P y
subst P x .x refl h = h

trans : ∀ {a} {A : Set a} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

sym : ∀ {a} {A : Set a} → {x y : A} → x ≡ y → y ≡ x
sym refl = refl

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

data _IsRelatedTo_ {a : Level} {Carrier : Set a} (x y : Carrier) : Set a where
  relTo : (x∼y : x ≡ y) → x IsRelatedTo y

begin_ : {a : Level} {Carrier : Set a} → {x y : Carrier} → x IsRelatedTo y → x ≡ y
begin relTo x∼y = x∼y

_∎ : {a : Level} {Carrier : Set a} → (x : Carrier) → x IsRelatedTo x
_∎ _ = relTo refl

_≡⟨_⟩_ : {a : Level} {Carrier : Set a} → (x : Carrier) {y z : Carrier} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
_ ≡⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

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

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- A specification of the language χ
------------------------------------------------------------------------

open import Atom

-- The specification is parametrised by an instance of χ-atoms.

module Chi (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)

open χ-atoms atoms

-- Abstract syntax.

mutual

  data Exp : Type where
    apply  : Exp → Exp → Exp
    lambda : Var → Exp → Exp
    case   : Exp → List Br → Exp
    rec    : Var → Exp → Exp
    var    : Var → Exp
    const  : Const → List Exp → Exp

  data Br : Type where
    branch : Const → List Var → Exp → Br

-- Substitution.

mutual

  infix 6 _[_←_] _[_←_]B _[_←_]⋆ _[_←_]B⋆

  _[_←_] : Exp → Var → Exp → Exp
  apply e₁ e₂ [ x ← e′ ] = apply (e₁ [ x ← e′ ]) (e₂ [ x ← e′ ])
  lambda y e  [ x ← e′ ] = lambda y (if x V.≟ y
                                     then e
                                     else e [ x ← e′ ])
  case e bs [ x ← e′ ]   = case (e [ x ← e′ ]) (bs [ x ← e′ ]B⋆)
  rec y e   [ x ← e′ ]   = rec y (if x V.≟ y
                                  then e
                                  else e [ x ← e′ ])

  var y [ x ← e′ ]       = if x V.≟ y then e′ else var y
  const c es  [ x ← e′ ] = const c (es [ x ← e′ ]⋆)

  _[_←_]B : Br → Var → Exp → Br
  branch c xs e [ x ← e′ ]B with V.member x xs
  ... | yes _ = branch c xs e
  ... | no  _ = branch c xs (e [ x ← e′ ])

  _[_←_]⋆ : List Exp → Var → Exp → List Exp
  []       [ x ← e′ ]⋆ = []
  (e ∷ es) [ x ← e′ ]⋆ = e [ x ← e′ ] ∷ es [ x ← e′ ]⋆

  _[_←_]B⋆ : List Br → Var → Exp → List Br
  []       [ x ← e′ ]B⋆ = []
  (b ∷ bs) [ x ← e′ ]B⋆ = b [ x ← e′ ]B ∷ bs [ x ← e′ ]B⋆

infix 5 ∷_
infix 4 _[_←_]↦_

data _[_←_]↦_ (e : Exp) : List Var → List Exp → Exp → Type where
  [] : e [ [] ← [] ]↦ e
  ∷_ : ∀ {x xs e′ es′ e″} →
       e [ xs ← es′ ]↦ e″ → e [ x ∷ xs ← e′ ∷ es′ ]↦ e″ [ x ← e′ ]

-- Operational semantics.

data Lookup (c : Const) : List Br → List Var → Exp → Type where
  here  : ∀ {xs e bs} → Lookup c (branch c xs e ∷ bs) xs e
  there : ∀ {c′ xs′ e′ bs xs e} →
          c ≢ c′ → Lookup c bs xs e →
          Lookup c (branch c′ xs′ e′ ∷ bs) xs e

infixr 5 _∷_
infix 4 _⇓_ _⇓⋆_

mutual

  data _⇓_ : Exp → Exp → Type where
    apply  : ∀ {e₁ e₂ x e v₂ v} →
             e₁ ⇓ lambda x e → e₂ ⇓ v₂ → e [ x ← v₂ ] ⇓ v →
             apply e₁ e₂ ⇓ v
    case   : ∀ {e bs c es xs e′ e″ v} →
             e ⇓ const c es → Lookup c bs xs e′ →
             e′ [ xs ← es ]↦ e″ → e″ ⇓ v →
             case e bs ⇓ v
    rec    : ∀ {x e v} → e [ x ← rec x e ] ⇓ v → rec x e ⇓ v
    lambda : ∀ {x e} → lambda x e ⇓ lambda x e
    const  : ∀ {c es vs} → es ⇓⋆ vs → const c es ⇓ const c vs

  data _⇓⋆_ : List Exp → List Exp → Type where
    []  : [] ⇓⋆ []
    _∷_ : ∀ {e es v vs} → e ⇓ v → es ⇓⋆ vs → e ∷ es ⇓⋆ v ∷ vs

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the sublist relation with respect to a
-- setoid which is decidable. This is a generalisation of what is
-- commonly known as Order Preserving Embeddings (OPE).
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Binary.Sublist.DecSetoid
  {c ℓ} (S : DecSetoid c ℓ) where

import Data.List.Relation.Binary.Equality.DecSetoid as DecSetoidEquality
import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
  as HeterogeneousProperties
open import Level using (_⊔_)

open DecSetoid S
open DecSetoidEquality S

------------------------------------------------------------------------
-- Re-export core definitions

open SetoidSublist setoid public

------------------------------------------------------------------------
-- Additional relational properties

_⊆?_ : Decidable _⊆_
_⊆?_ = HeterogeneousProperties.sublist? _≟_

⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_
⊆-isDecPartialOrder = record
  { isPartialOrder = ⊆-isPartialOrder
  ; _≟_            = _≋?_
  ; _≤?_           = _⊆?_
  }

⊆-decPoset : DecPoset c (c ⊔ ℓ) (c ⊔ ℓ)
⊆-decPoset = record
  { isDecPartialOrder = ⊆-isDecPartialOrder
  }


text:
module DifferentArities where

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

f : Nat -> Nat -> Nat
f zero      = \x -> x
f (suc n) m = f n (suc m)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
-- This file derives some of the Cartesian Kan operations using transp
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.CartesianKanOps where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

coe0→1 : ∀ {ℓ} (A : I → Type ℓ) → A i0 → A i1
coe0→1 A a = transp A i0 a

-- "coe filler"
coe0→i : ∀ {ℓ} (A : I → Type ℓ) (i : I) → A i0 → A i
coe0→i A i a = transp (λ j → A (i ∧ j)) (~ i) a

-- Check the equations for the coe filler
coe0→i1 : ∀ {ℓ} (A : I → Type ℓ) (a : A i0) → coe0→i A i1 a ≡ coe0→1 A a
coe0→i1 A a = refl

coe0→i0 : ∀ {ℓ} (A : I → Type ℓ) (a : A i0) → coe0→i A i0 a ≡ a
coe0→i0 A a = refl

-- coe backwards
coe1→0 : ∀ {ℓ} (A : I → Type ℓ) → A i1 → A i0
coe1→0 A a = transp (λ i → A (~ i)) i0 a

-- coe backwards filler
coe1→i : ∀ {ℓ} (A : I → Type ℓ) (i : I) → A i1 → A i
coe1→i A i a = transp (λ j → A (i ∨ ~ j)) i a

-- Check the equations for the coe backwards filler
coe1→i0 : ∀ {ℓ} (A : I → Type ℓ) (a : A i1) → coe1→i A i0 a ≡ coe1→0 A a
coe1→i0 A a = refl

coe1→i1 : ∀ {ℓ} (A : I → Type ℓ) (a : A i1) → coe1→i A i1 a ≡ a
coe1→i1 A a = refl

-- "squeezeNeg"
coei→0 : ∀ {ℓ} (A : I → Type ℓ) (i : I) → A i → A i0
coei→0 A i a = transp (λ j → A (i ∧ ~ j)) (~ i) a

coei0→0 : ∀ {ℓ} (A : I → Type ℓ) (a : A i0) → coei→0 A i0 a ≡ a
coei0→0 A a = refl

coei1→0 : ∀ {ℓ} (A : I → Type ℓ) (a : A i1) → coei→0 A i1 a ≡ coe1→0 A a
coei1→0 A a = refl

-- "master coe"
-- defined as the filler of coei→0, coe0→i, and coe1→i
-- unlike in cartesian cubes, we don't get coei→i = id definitionally
coei→j : ∀ {ℓ} (A : I → Type ℓ) (i j : I) → A i → A j
coei→j A i j a =
  fill A
    (λ j → λ { (i = i0) → coe0→i A j a
             ; (i = i1) → coe1→i A j a
             })
    (inS (coei→0 A i a))
    j

-- "squeeze"
-- this is just defined as the composite face of the master coe
coei→1 : ∀ {ℓ} (A : I → Type ℓ) (i : I) → A i → A i1
coei→1 A i a = coei→j A i i1 a

coei0→1 : ∀ {ℓ} (A : I → Type ℓ) (a : A i0) → coei→1 A i0 a ≡ coe0→1 A a
coei0→1 A a = refl

coei1→1 : ∀ {ℓ} (A : I → Type ℓ) (a : A i1) → coei→1 A i1 a ≡ a
coei1→1 A a = refl

-- equations for "master coe"
coei→i0 : ∀ {ℓ} (A : I → Type ℓ) (i : I) (a : A i) → coei→j A i i0 a ≡ coei→0 A i a
coei→i0 A i a = refl

coei0→i : ∀ {ℓ} (A : I → Type ℓ) (i : I) (a : A i0) → coei→j A i0 i a ≡ coe0→i A i a
coei0→i A i a = refl

coei→i1 : ∀ {ℓ} (A : I → Type ℓ) (i : I) (a : A i) → coei→j A i i1 a ≡ coei→1 A i a
coei→i1 A i a = refl

coei1→i : ∀ {ℓ} (A : I → Type ℓ) (i : I) (a : A i1) → coei→j A i1 i a ≡ coe1→i A i a
coei1→i A i a = refl

-- only non-definitional equation
coei→i : ∀ {ℓ} (A : I → Type ℓ) (i : I) (a : A i) → coei→j A i i a ≡ a
coei→i A i = coe0→i (λ i → (a : A i) → coei→j A i i a ≡ a) i (λ _ → refl)

-- do the same for fill

fill1→i : ∀ {ℓ} (A : ∀ i → Type ℓ)
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (u1 : A i1 [ φ ↦ u i1 ])
       ---------------------------
       (i : I) → A i
fill1→i A {φ = φ} u u1 i =
  comp (λ j → A (i ∨ ~ j))
       (λ j → λ { (φ = i1) → u (i ∨ ~ j) 1=1
                ; (i = i1) → outS u1 })
       (outS u1)

filli→0 : ∀ {ℓ} (A : ∀ i → Type ℓ)
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (i : I)
       (ui : A i [ φ ↦ u i ])
       ---------------------------
       → A i0
filli→0 A {φ = φ} u i ui =
  comp (λ j → A (i ∧ ~ j))
       (λ j → λ { (φ = i1) → u (i ∧ ~ j) 1=1
                ; (i = i0) → outS ui })
       (outS ui)

filli→j : ∀ {ℓ} (A : ∀ i → Type ℓ)
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (i : I)
       (ui : A i [ φ ↦ u i ])
       ---------------------------
       (j : I) → A j
filli→j A {φ = φ} u i ui j =
  fill A
    (λ j → λ { (φ = i1) → u j 1=1
             ; (i = i0) → fill A u ui j
             ; (i = i1) → fill1→i A u ui j
             })
    (inS (filli→0 A u i ui))
    j

-- We can reconstruct fill from hfill, coei→j, and the path coei→i ≡ id.
-- The definition does not rely on the computational content of the coei→i path.
fill' : ∀ {ℓ} (A : I → Type ℓ)
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (u0 : A i0 [ φ ↦ u i0 ])
       ---------------------------
       (i : I) → A i [ φ ↦ u i ]
fill' A {φ = φ} u u0 i =
  inS (hcomp (λ j → λ {(φ = i1) → coei→i A i (u i 1=1) j; (i = i0) → coei→i A i (outS u0) j}) t)
  where
  t : A i
  t = hfill {φ = φ} (λ j v → coei→j A j i (u j v)) (inS (coe0→i A i (outS u0))) i

fill'-cap :  ∀ {ℓ} (A : I → Type ℓ)
             {φ : I}
             (u : ∀ i → Partial φ (A i))
             (u0 : A i0 [ φ ↦ u i0 ])
             ---------------------------
             → outS (fill' A u u0 i0) ≡ outS (u0)
fill'-cap A u u0 = refl

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Numeral.Natural.Oper.DivMod.Proofs where

import Lvl
open import Data
open import Data.Boolean.Stmt
open import Logic.Predicate
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.FlooredDivision.Proofs.DivisibilityWithRemainder
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Modulo.Proofs.DivisibilityWithRemainder
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.DivisibilityWithRemainder
open import Numeral.Natural.Relation.DivisibilityWithRemainder.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Syntax.Transitivity

-- The division theorem.
[⌊/⌋][mod]-is-division-with-remainder : ∀{x y} → (((x ⌊/⌋ 𝐒(y)) ⋅ 𝐒(y)) + (x mod 𝐒(y)) ≡ x)
[⌊/⌋][mod]-is-division-with-remainder {x}{y} with [∃]-intro r ⦃ p ⦄ ← [∣ᵣₑₘ]-existence-alt {x}{y} =
  ((x ⌊/⌋ 𝐒(y)) ⋅ 𝐒(y)) + (x mod 𝐒(y))                         🝖[ _≡_ ]-[ congruence₂(_+_) (congruence₂ₗ(_⋅_)(𝐒(y)) ([⌊/⌋][∣ᵣₑₘ]-quotient-equality {x}{y}{r}{p})) ([mod][∣ᵣₑₘ]-remainder-equality {x}{y}{r}{p}) ]
  (([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y)) + (𝕟-to-ℕ ([∣ᵣₑₘ]-remainder p)) 🝖[ _≡_ ]-[ [∣ᵣₑₘ]-is-division-with-remainder {x}{𝐒(y)}{r} p ]
  x                                                            🝖-end

[⌊/⌋][mod]-is-division-with-remainder-pred-commuted : ∀{x y} ⦃ _ : IsTrue(positive?(y)) ⦄ → ((y ⋅ (x ⌊/⌋ y)) + (x mod y) ≡ x)
[⌊/⌋][mod]-is-division-with-remainder-pred-commuted {x} {𝐒 y} = [≡]-with(_+ (x mod 𝐒(y))) (commutativity(_⋅_) {𝐒(y)}{x ⌊/⌋ 𝐒(y)}) 🝖 [⌊/⌋][mod]-is-division-with-remainder {x}{y}

-- Floored division and multiplication is not inverse operators for all numbers.
-- This shows why it is not exactly.
[⌊/⌋][⋅]-semiInverseOperatorᵣ : ∀{a b} → ((a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b) ≡ a −₀ (a mod 𝐒(b)))
[⌊/⌋][⋅]-semiInverseOperatorᵣ {a}{b} =
  (a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b) 🝖[ _≡_ ]-[ OneTypeTwoOp.moveᵣ-to-invOp {b = a mod 𝐒(b)}{c = a} (([⌊/⌋][mod]-is-division-with-remainder {y = b})) ]
  a −₀ (a mod 𝐒(b))   🝖-end

-- Floored division and multiplication is not inverse operators for all numbers.
-- This theorem shows that modulo is the error term (difference between the actual value for it to be inverse and value of the operation).
[⌊/⌋][⋅]-inverseOperatorᵣ-error : ∀{a b} → (a mod 𝐒(b) ≡ a −₀ (a ⌊/⌋ 𝐒(b) ⋅ 𝐒(b)))
[⌊/⌋][⋅]-inverseOperatorᵣ-error {a}{b} =
  (a mod 𝐒(b))             🝖[ _≡_ ]-[ OneTypeTwoOp.moveᵣ-to-invOp {a = a mod 𝐒(b)}{b = (a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b)}{c = a} (commutativity(_+_) {a mod 𝐒(b)}{(a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b)} 🝖 [⌊/⌋][mod]-is-division-with-remainder {y = b}) ]
  a −₀ (a ⌊/⌋ 𝐒(b) ⋅ 𝐒(b)) 🝖-end

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:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

cong : {A B : Set} (f : A → B)
     → {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

+-identityʳ : (x : Nat) → x + 0 ≡ x
+-identityʳ zero    = refl
+-identityʳ (suc n) = cong suc (+-identityʳ n)

+-assoc : (x y z : Nat) → (x + y) + z ≡ x + (y + z)
+-assoc zero    _ _ = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil = x1 nil
inc (x0 x) = x1 x
inc (x1 x) = x0 (inc x)

to : Nat → Bin
to zero = (x0 nil)
to (suc x) = inc (to x)

postulate
  from : Bin → Nat

data Can : Bin → Set where
  Can- : ∀ {n} → from (to n) ≡ n → Can (to n)

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

postulate
  to'' : (x : Nat) → Σ Bin Can

to∘from' : (a : Bin) → (b : Can a) → to'' (from a) ≡ ⟨ a , b ⟩
to∘from' .(to _) (Can- x) = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-09-03, issue #2730:
-- Skip termination check when giving.

-- C-c C-SPC fails because of termination problems, but
-- C-u C-c C-SPC should succeed here.

f : Set
f = {! f !}


text:
module Prelude.IO where

open import Prelude.Bool
open import Prelude.Char
open import Prelude.Nat
open import Prelude.String
open import Prelude.Unit
open import Prelude.Vec
open import Prelude.Float

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}

infixl 1 _>>=_

postulate
  return  : ∀ {A} → A → IO A
  _>>=_   : ∀ {A B} → IO A → (A → IO B) → IO B
  numArgs : Nat
  getArg  : Nat -> String

args : Vec String numArgs
args = buildArgs numArgs
  where
    buildArgs : (n : Nat) -> Vec String n
    buildArgs Z     = []
    buildArgs (S n) = snoc (buildArgs n) (getArg n)

{-# COMPILED_EPIC return (u1 : Unit, a : Any) -> Any = ioreturn(a) #-}
{-# COMPILED_EPIC _>>=_ (u1 : Unit, u2 : Unit, x : Any, f : Any) -> Any = iobind(x,f) #-}
{-# COMPILED_EPIC numArgs () -> BigInt = foreign BigInt "numArgsBig" () #-}
{-# COMPILED_EPIC getArg  (n : BigInt) -> Any = foreign Any "getArgBig" (n : BigInt) #-}

postulate
  natToString : Nat -> String
  readNat    : IO Nat
  readStr    : IO String
  putStr     : String -> IO Unit
  printChar  : Char   -> IO Unit

putStrLn   : String -> IO Unit
putStrLn s = putStr s >>= \_ -> putStr "\n"

printFloat : Float  -> IO Unit
printFloat f = putStr (floatToString f)

printNat : Nat -> IO Unit
printNat n = putStr (natToString n)

printBool : Bool -> IO Unit
printBool true = putStr "true"
printBool false = putStr "false"

{-# COMPILED_EPIC natToString (n : Any) -> String = bigToStr(n) #-}
{-# COMPILED_EPIC readNat (u : Unit) -> Any = strToBig(readStr(u)) #-}

{-# COMPILED_EPIC putStr (a : String, u : Unit) -> Unit = foreign Int "wputStr" (mkString(a) : String); primUnit #-}
-- {-# COMPILED_EPIC putStrLn (a : String, u : Unit) -> Unit = putStrLn (a) #-}
{-# COMPILED_EPIC readStr (u : Unit) -> Data = readStr(u) #-}
{-# COMPILED_EPIC printChar (c : Int, u : Unit) -> Unit = printChar(c) #-}

infixr 2 _<$>_
_<$>_ : {A B : Set}(f : A -> B)(m : IO A) -> IO B
f <$> x = x >>= λ y -> return (f y)

infixr 0 bind
bind : ∀ {A B} → IO A → (A → IO B) → IO B
bind m f = m >>= f

infixr 0 then
then : ∀ {A B} -> IO A -> IO B -> IO B
then m f = m >>= λ _ -> f

syntax bind e (\ x -> f) = x <- e , f
syntax then e f          = e ,, f

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

module Categories.NaturalTransformation.Properties where

open import Level
open import Data.Product using (Σ; _,_)
open import Function.Equality using (Π)

open import Categories.Category
open import Categories.Category.Product
open import Categories.Category.Instance.Setoids
open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.Functor.Construction.LiftSetoids
open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.NaturalTransformation.Dinatural hiding (_≃_)

import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ ℓ′ e : Level
    C D E : Category o ℓ e

module _ {F G : Functor C D} where
  private
    module C = Category C
    module D = Category D
    open D
    open MR D
    open HomReasoning
    open Functor

    F′ : Bifunctor C.op C D
    F′ = F ∘F πʳ

    G′ : Bifunctor C.op C D
    G′ = G ∘F πʳ

  NT⇒Dinatural : NaturalTransformation F G → DinaturalTransformation F′ G′
  NT⇒Dinatural β = dtHelper record
    { α       = η
    ; commute = λ f → ∘-resp-≈ʳ (elimʳ (identity F)) ○ ⟺ (commute f) ○ introˡ (identity G)
    }
    where open NaturalTransformation β

  Dinatural⇒NT : DinaturalTransformation F′ G′ → NaturalTransformation F G
  Dinatural⇒NT θ = ntHelper record
    { η       = α
    ; commute = λ f → introˡ (identity G) ○ ⟺ (commute f) ○ ∘-resp-≈ʳ (elimʳ (identity F))
    }
    where open DinaturalTransformation θ

  replaceˡ : ∀ {F′} → NaturalTransformation F G → F ≃ F′ → NaturalTransformation F′ G
  replaceˡ {F′} α F≃F′ = ntHelper record
    { η       = λ X → η X ∘ ⇐.η X
    ; commute = λ {X Y} f → begin
      (η Y ∘ ⇐.η Y) ∘ F₁ F′ f ≈⟨ pullʳ (⇐.commute f) ⟩
      η Y ∘ F₁ F f ∘ ⇐.η X    ≈⟨ pullˡ (commute f) ○ assoc ⟩
      F₁ G f ∘ η X ∘ ⇐.η X    ∎
    }
    where open NaturalIsomorphism F≃F′
          open NaturalTransformation α

  replaceʳ : ∀ {G′} → NaturalTransformation F G → G ≃ G′ → NaturalTransformation F G′
  replaceʳ {G′} α G≃G′ = ntHelper record
    { η       = λ X → ⇒.η X ∘ η X
    ; commute = λ {X Y} f → begin
      (⇒.η Y ∘ η Y) ∘ F₁ F f ≈⟨ pullʳ (commute f) ⟩
      ⇒.η Y ∘ F₁ G f ∘ η X   ≈⟨ pullˡ (⇒.commute f) ○ assoc ⟩
      F₁ G′ f ∘ ⇒.η X ∘ η X  ∎
    }
    where open NaturalIsomorphism G≃G′
          open NaturalTransformation α

module _ (F : Bifunctor C D E) where

  -- there is natural transformation between two partially applied bifunctors.

  appˡ-nat : ∀ {X Y} → (f : Category._⇒_ C X Y) → NaturalTransformation (appˡ F X) (appˡ F Y)
  appˡ-nat f = F ∘ˡ (constNat f ※ⁿ idN)

  appʳ-nat : ∀ {X Y} → (f : Category._⇒_ D X Y) → NaturalTransformation (appʳ F X) (appʳ F Y)
  appʳ-nat f = F ∘ˡ (idN ※ⁿ constNat f)

module _ {F G : Bifunctor C D E} (α : NaturalTransformation F G) where
  private
    module C = Category C
    module D = Category D
    module E = Category E

  appˡ′ : ∀ X → NaturalTransformation (appˡ F X) (appˡ G X)
  appˡ′ X = α ∘ₕ idN

  appʳ′ : ∀ X → NaturalTransformation (appʳ F X) (appʳ G X)
  appʳ′ X = α ∘ₕ idN

-- unlift universe level
module _ {c ℓ ℓ′ e} {F G : Functor C (Setoids c ℓ)} (α : NaturalTransformation (LiftSetoids ℓ′ e ∘F F) (LiftSetoids ℓ′ e ∘F G)) where
  open NaturalTransformation α
  open Π

  unlift-nat : NaturalTransformation F G
  unlift-nat = ntHelper record
    { η       = λ X → record
      { _⟨$⟩_ = λ x → lower (η X ⟨$⟩ lift x)
      ; cong = λ eq → lower (cong (η X) (lift eq))
      }
    ; commute = λ f eq → lower (commute f (lift eq))
    }

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:
-- Decidability in the context of types means that it is possible to decide whether a type is empty or have inhabitants.
-- In the case of it having inhabitants, it is possible to extract a witness of the type.
-- Note: When using the types as propositions interpretation of types as a logic system, decidability is equivalent to excluded middle.
module Type.Properties.Decidable where

open import Data
open import Data.Tuple.RaiseTypeᵣ
import      Lvl
import      Lvl.MultiFunctions as Lvl
open import Data.Boolean using (Bool ; 𝑇 ; 𝐹)
open import Function.Multi
open import Logic.Predicate
open import Numeral.Natural
open import Type

private variable ℓ ℓₚ : Lvl.Level
private variable A B C P Q : Type{ℓ}

-- Decider₀(P)(b) states that the boolean value b decides whether the type P is empty or inhabited.
-- When interpreting P as a proposition, the boolean value b decides the truth value of P.
-- Base case of Decider.
data Decider₀ {ℓ} (P : Type{ℓ}) : Bool → Type{Lvl.𝐒(ℓ)} where
  true  : P                  → Decider₀(P)(𝑇)
  false : (P → Empty{Lvl.𝟎}) → Decider₀(P)(𝐹)

-- Elimination rule of Decider₀.
elim : ∀{P} → (Proof : ∀{b} → Decider₀{ℓₚ}(P)(b) → Type{ℓ}) → ((p : P) → Proof(true p)) → ((np : P → Empty) → Proof(false np)) → (∀{b} → (d : Decider₀(P)(b)) → Proof(d))
elim _ fp fnp (true  p)  = fp p
elim _ fp fnp (false np) = fnp np

step : ∀{f : Bool → Bool} → (P → Decider₀(Q)(f(𝑇))) → ((P → Empty) → Decider₀(Q)(f(𝐹))) → (∀{b} → Decider₀(P)(b) → Decider₀(Q)(f(b)))
step{f = f} = elim (\{b} _ → Decider₀(_)(f(b)))

-- Decider(n)(P)(f) states that the values of the n-ary function f decides whether the values of P is empty or inhabited for a given number of arguments.
-- When interpreting P as an n-ary predicate (proposition), the n-ary function f decides the truth values of P.
Decider : (n : ℕ) → ∀{ℓ}{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (As ⇉ Type{ℓ}) → (As ⇉ Bool) → Type{Lvl.𝐒(ℓ) Lvl.⊔ Lvl.⨆(ℓ𝓈)}
Decider(0)           = Decider₀
Decider(1)       P f = ∀{x} → Decider₀(P(x))(f(x))
Decider(𝐒(𝐒(n))) P f = ∀{x} → Decider(𝐒(n))(P(x))(f(x))

-- Whether there is a boolean decider for the inhabitedness of a type function.
Decidable : (n : ℕ) → ∀{ℓ}{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (As ⇉ Type{ℓ}) → Type
Decidable(n)(P) = ∃(Decider(n)(P))

-- The boolean n-ary inhabitedness decider function for a decidable n-ary type function.
decide : (n : ℕ) → ∀{ℓ}{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (P : As ⇉ Type{ℓ}) → ⦃ dec : Decidable(n)(P) ⦄ → (As ⇉ Bool)
decide(_)(_) ⦃ dec ⦄ = [∃]-witness dec


text:
module logic where

open import empty public
open import eq public
open import level public
open import negation public
open import neq public
open import product public
open import sum public
open import unit public

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module EtaBug where

record ⊤ : Set where
data ⊥ : Set where

data Bool : Set where
  true  : Bool
  false : Bool

T : Bool → Set
T true  = ⊤
T false = ⊥

record ∃ {A : Set} (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

postulate
  G : Set → Set
  D : ∀ {A} → G A → A → Set

P : {A : Set} → G A → Set
P g = ∀ x → D g x

postulate
  f : ∀ {A} {g : G A} → P g → P g
  g : (p : ⊥ → Bool) → G (∃ λ t → T (p t))
  h : ∀ {p : ⊥ → Bool} {t pt} → D (g p) (t , pt)
  p : ⊥ → Bool

works : P (g p)
works = f (λ _ → h {p = p})

fails : P (g p)
fails = f (λ _ → h)

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------
-- Isomorphisms and equalities relating an arbitrary "equality with J"
-- to path equality, along with a proof of extensionality for the
-- "equality with J"
------------------------------------------------------------------------

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

import Equality.Path as P

module Equality.Path.Isomorphisms
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude

import Bijection
import Embedding
import Equivalence
import Equivalence.Contractible-preimages
import Equivalence.Half-adjoint
import Function-universe
import H-level
import Surjection
import Univalence-axiom

private
  module B  = Bijection equality-with-J
  module CP = Equivalence.Contractible-preimages equality-with-J
  module HA = Equivalence.Half-adjoint equality-with-J
  module Eq = Equivalence equality-with-J
  module F  = Function-universe equality-with-J

  module PB  = Bijection P.equality-with-J
  module PM  = Embedding P.equality-with-J
  module PE  = Equivalence P.equality-with-J
  module PCP = Equivalence.Contractible-preimages P.equality-with-J
  module PHA = Equivalence.Half-adjoint P.equality-with-J
  module PF  = Function-universe P.equality-with-J
  module PH  = H-level P.equality-with-J
  module PS  = Surjection P.equality-with-J
  module PU  = Univalence-axiom P.equality-with-J

open B using (_↔_)
open Embedding equality-with-J hiding (id; _∘_)
open Eq using (_≃_; Is-equivalence)
open F hiding (id; _∘_)
open H-level equality-with-J
open Surjection equality-with-J using (_↠_)
open Univalence-axiom equality-with-J

private
  variable
    a b c p q ℓ : Level
    A           : Type a
    B           : A → Type b
    u v x y z   : A
    f g h       : (x : A) → B x
    n           : ℕ

------------------------------------------------------------------------
-- Extensionality

-- The proof bad-ext is perhaps not less "good" than ext (I don't
-- know), it is called this simply because it is not defined using
-- good-ext.

bad-ext : Extensionality a b
apply-ext bad-ext {f = f} {g = g} =
  (∀ x → f x ≡ g x)    ↝⟨ (λ p x → _↔_.to ≡↔≡ (p x)) ⟩
  (∀ x → f x P.≡ g x)  ↝⟨ P.apply-ext P.ext ⟩
  f P.≡ g              ↔⟨ inverse ≡↔≡ ⟩□
  f ≡ g                □

-- Extensionality.

ext : Extensionality a b
ext = Eq.good-ext bad-ext

⟨ext⟩ : Extensionality′ A B
⟨ext⟩ = apply-ext ext

abstract

  -- The function ⟨ext⟩ is an equivalence.

  ext-is-equivalence : Is-equivalence {A = ∀ x → f x ≡ g x} ⟨ext⟩
  ext-is-equivalence = Eq.good-ext-is-equivalence bad-ext

  -- Equality rearrangement lemmas for ⟨ext⟩.

  ext-refl : ⟨ext⟩ (λ x → refl (f x)) ≡ refl f
  ext-refl = Eq.good-ext-refl bad-ext _

  ext-const :
    (x≡y : x ≡ y) →
    ⟨ext⟩ (const {B = A} x≡y) ≡ cong const x≡y
  ext-const = Eq.good-ext-const bad-ext

  cong-ext :
    ∀ (f≡g : ∀ x → f x ≡ g x) {x} →
    cong (_$ x) (⟨ext⟩ f≡g) ≡ f≡g x
  cong-ext = Eq.cong-good-ext bad-ext

  ext-cong :
    {B : Type b} {C : B → Type c}
    {f : A → (x : B) → C x} {x≡y : x ≡ y} →
    ⟨ext⟩ (λ z → cong (flip f z) x≡y) ≡ cong f x≡y
  ext-cong = Eq.good-ext-cong bad-ext

  subst-ext :
    ∀ {f g : (x : A) → B x}
    (P : B x → Type p) {p} (f≡g : ∀ x → f x ≡ g x) →
    subst (λ f → P (f x)) (⟨ext⟩ f≡g) p ≡ subst P (f≡g x) p
  subst-ext = Eq.subst-good-ext bad-ext

  elim-ext :
    (P : B x → B x → Type p)
    (p : (y : B x) → P y y)
    {f g : (x : A) → B x}
    (f≡g : ∀ x → f x ≡ g x) →
    elim (λ {f g} _ → P (f x) (g x)) (p ∘ (_$ x)) (⟨ext⟩ f≡g) ≡
    elim (λ {x y} _ → P x y) p (f≡g x)
  elim-ext = Eq.elim-good-ext bad-ext

  -- I based the statements of the following three lemmas on code in
  -- the Lean Homotopy Type Theory Library with Jakob von Raumer and
  -- Floris van Doorn listed as authors. The file was claimed to have
  -- been ported from the Coq HoTT library. (The third lemma has later
  -- been generalised.)

  ext-sym :
    (f≡g : ∀ x → f x ≡ g x) →
    ⟨ext⟩ (sym ∘ f≡g) ≡ sym (⟨ext⟩ f≡g)
  ext-sym = Eq.good-ext-sym bad-ext

  ext-trans :
    (f≡g : ∀ x → f x ≡ g x) (g≡h : ∀ x → g x ≡ h x) →
    ⟨ext⟩ (λ x → trans (f≡g x) (g≡h x)) ≡ trans (⟨ext⟩ f≡g) (⟨ext⟩ g≡h)
  ext-trans = Eq.good-ext-trans bad-ext

  cong-post-∘-ext :
    (f≡g : ∀ x → f x ≡ g x) →
    cong (h ∘_) (⟨ext⟩ f≡g) ≡ ⟨ext⟩ (cong h ∘ f≡g)
  cong-post-∘-ext = Eq.cong-post-∘-good-ext bad-ext bad-ext

  cong-pre-∘-ext :
    (f≡g : ∀ x → f x ≡ g x) →
    cong (_∘ h) (⟨ext⟩ f≡g) ≡ ⟨ext⟩ (f≡g ∘ h)
  cong-pre-∘-ext = Eq.cong-pre-∘-good-ext bad-ext bad-ext

  cong-∘-ext :
    {A : Type a} {B : Type b} {C : Type c} {f g : B → C}
    (f≡g : ∀ x → f x ≡ g x) →
    cong {B = (A → B) → (A → C)}
         (λ f → f ∘_) (⟨ext⟩ f≡g) ≡
    ⟨ext⟩ λ h → ⟨ext⟩ λ x → f≡g (h x)
  cong-∘-ext = Eq.cong-∘-good-ext bad-ext bad-ext bad-ext

------------------------------------------------------------------------
-- More isomorphisms and related properties

-- Split surjections expressed using equality are equivalent to split
-- surjections expressed using paths.

↠≃↠ :
  {A : Type a} {B : Type b} →
  (A ↠ B) ≃ (A PS.↠ B)
↠≃↠ = Eq.↔→≃
  (λ A↠B → record
     { logical-equivalence = _↠_.logical-equivalence A↠B
     ; right-inverse-of    = _↔_.to ≡↔≡ ∘ _↠_.right-inverse-of A↠B
     })
  (λ A↠B → record
     { logical-equivalence = PS._↠_.logical-equivalence A↠B
     ; right-inverse-of    = _↔_.from ≡↔≡ ∘ PS._↠_.right-inverse-of A↠B
     })
  (λ A↠B →
     cong (λ r → record
             { logical-equivalence = PS._↠_.logical-equivalence A↠B
             ; right-inverse-of    = r
             }) $
     ⟨ext⟩ λ _ → _↔_.right-inverse-of ≡↔≡ _)
  (λ A↠B →
     cong (λ r → record
             { logical-equivalence = _↠_.logical-equivalence A↠B
             ; right-inverse-of    = r
             }) $
     ⟨ext⟩ λ _ → _↔_.left-inverse-of ≡↔≡ _)

private

  -- Bijections expressed using paths can be converted into bijections
  -- expressed using equality.

  ↔→↔ : {A B : Type ℓ} → A PB.↔ B → A ↔ B
  ↔→↔ A↔B = record
    { surjection      = _≃_.from ↠≃↠ $ PB._↔_.surjection      A↔B
    ; left-inverse-of = _↔_.from ≡↔≡ ∘ PB._↔_.left-inverse-of A↔B
    }

-- Bijections expressed using equality are equivalent to bijections
-- expressed using paths.

↔≃↔ :
  {A : Type a} {B : Type b} →
  (A ↔ B) ≃ (A PB.↔ B)
↔≃↔ {A = A} {B = B} =
  A ↔ B                                                 ↔⟨ B.↔-as-Σ ⟩

  (∃ λ (f : A → B) → ∃ λ (f⁻¹ : B → A) →
    (∀ x → f (f⁻¹ x) ≡ x) × (∀ x → f⁻¹ (f x) ≡ x))      ↔⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                            (∀-cong ext λ _ → ≡↔≡)
                                                              ×-cong
                                                            (∀-cong ext λ _ → ≡↔≡)) ⟩
  (∃ λ (f : A → B) → ∃ λ (f⁻¹ : B → A) →
    (∀ x → f (f⁻¹ x) P.≡ x) × (∀ x → f⁻¹ (f x) P.≡ x))  ↔⟨ inverse $ ↔→↔ $ PB.↔-as-Σ ⟩□

  A PB.↔ B                                              □

-- H-level expressed using equality is isomorphic to H-level expressed
-- using paths.

H-level↔H-level : ∀ n → H-level n A ↔ PH.H-level n A
H-level↔H-level {A = A} zero =
  H-level 0 A                    ↔⟨⟩
  (∃ λ (x : A) → ∀ y → x ≡ y)    ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ≡↔≡) ⟩
  (∃ λ (x : A) → ∀ y → x P.≡ y)  ↔⟨⟩
  PH.H-level 0 A                 □

H-level↔H-level {A = A} (suc n) =
  H-level (suc n) A                 ↝⟨ inverse $ ≡↔+ _ ext ⟩
  (∀ x y → H-level n (x ≡ y))       ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → H-level-cong ext _ ≡↔≡) ⟩
  (∀ x y → H-level n (x P.≡ y))     ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → H-level↔H-level n) ⟩
  (∀ x y → PH.H-level n (x P.≡ y))  ↝⟨ ↔→↔ $ PF.≡↔+ _ P.ext ⟩
  PH.H-level (suc n) A              □

-- CP.Is-equivalence is isomorphic to PCP.Is-equivalence.

Is-equivalence-CP↔Is-equivalence-CP :
  CP.Is-equivalence f ↔ PCP.Is-equivalence f
Is-equivalence-CP↔Is-equivalence-CP {f = f} =
  CP.Is-equivalence f                         ↔⟨⟩
  (∀ y →   Contractible (∃ λ x → f x   ≡ y))  ↝⟨ (∀-cong ext λ _ → H-level-cong ext _ $ ∃-cong λ _ → ≡↔≡) ⟩
  (∀ y →   Contractible (∃ λ x → f x P.≡ y))  ↝⟨ (∀-cong ext λ _ → H-level↔H-level _) ⟩
  (∀ y → P.Contractible (∃ λ x → f x P.≡ y))  ↔⟨⟩
  PCP.Is-equivalence f                        □

-- Is-equivalence expressed using equality is isomorphic to
-- Is-equivalence expressed using paths.

Is-equivalence↔Is-equivalence :
  Is-equivalence f ↔ PE.Is-equivalence f
Is-equivalence↔Is-equivalence {f = f} =
  Is-equivalence f      ↝⟨ HA.Is-equivalence↔Is-equivalence-CP ext ⟩
  CP.Is-equivalence f   ↝⟨ Is-equivalence-CP↔Is-equivalence-CP ⟩
  PCP.Is-equivalence f  ↝⟨ inverse $ ↔→↔ $ PHA.Is-equivalence↔Is-equivalence-CP P.ext ⟩□
  PE.Is-equivalence f   □

-- The type of equivalences, expressed using equality, is isomorphic
-- to the type of equivalences, expressed using paths.

≃↔≃ :
  {A : Type a} {B : Type b} →
  A ≃ B ↔ A PE.≃ B
≃↔≃ {A = A} {B = B} =
  A ≃ B                ↝⟨ Eq.≃-as-Σ ⟩
  ∃ Is-equivalence     ↝⟨ (∃-cong λ _ → Is-equivalence↔Is-equivalence) ⟩
  ∃ PE.Is-equivalence  ↝⟨ inverse $ ↔→↔ PE.≃-as-Σ ⟩□
  A PE.≃ B             □

private

  -- ≃↔≃ computes in the "right" way.

  to-≃↔≃ :
    {A : Type a} {B : Type b} {A≃B : A ≃ B} →
    PE._≃_.logical-equivalence (_↔_.to ≃↔≃ A≃B) ≡
    _≃_.logical-equivalence A≃B
  to-≃↔≃ = refl _

  from-≃↔≃ :
    {A : Type a} {B : Type b} {A≃B : A PE.≃ B} →
    _≃_.logical-equivalence (_↔_.from ≃↔≃ A≃B) ≡
    PE._≃_.logical-equivalence A≃B
  from-≃↔≃ = refl _

-- The type of equivalences, expressed using "contractible preimages"
-- and equality, is isomorphic to the type of equivalences, expressed
-- using contractible preimages and paths.

≃-CP↔≃-CP :
  {A : Type a} {B : Type b} →
  A CP.≃ B ↔ A PCP.≃ B
≃-CP↔≃-CP {A = A} {B = B} =
  ∃ CP.Is-equivalence   ↝⟨ (∃-cong λ _ → Is-equivalence-CP↔Is-equivalence-CP) ⟩□
  ∃ PCP.Is-equivalence  □

-- The cong function for paths can be expressed in terms of the cong
-- function for equality.

cong≡cong :
  {A : Type a} {B : Type b} {f : A → B} {x y : A} {x≡y : x P.≡ y} →
  cong f (_↔_.from ≡↔≡ x≡y) ≡ _↔_.from ≡↔≡ (P.cong f x≡y)
cong≡cong {f = f} {x≡y = x≡y} = P.elim
  (λ x≡y → cong f (_↔_.from ≡↔≡ x≡y) ≡ _↔_.from ≡↔≡ (P.cong f x≡y))
  (λ x →
     cong f (_↔_.from ≡↔≡ P.refl)    ≡⟨ cong (cong f) from-≡↔≡-refl ⟩
     cong f (refl x)                 ≡⟨ cong-refl _ ⟩
     refl (f x)                      ≡⟨ sym $ from-≡↔≡-refl ⟩
     _↔_.from ≡↔≡ P.refl             ≡⟨ cong (_↔_.from ≡↔≡) $ sym $ _↔_.from ≡↔≡ $ P.cong-refl f ⟩∎
     _↔_.from ≡↔≡ (P.cong f P.refl)  ∎)
  x≡y

-- The sym function for paths can be expressed in terms of the sym
-- function for equality.

sym≡sym :
  {x≡y : x P.≡ y} →
  sym (_↔_.from ≡↔≡ x≡y) ≡ _↔_.from ≡↔≡ (P.sym x≡y)
sym≡sym {x≡y = x≡y} = P.elim₁
  (λ x≡y → sym (_↔_.from ≡↔≡ x≡y) ≡ _↔_.from ≡↔≡ (P.sym x≡y))
  (sym (_↔_.from ≡↔≡ P.refl)    ≡⟨ cong sym from-≡↔≡-refl ⟩
   sym (refl _)                 ≡⟨ sym-refl ⟩
   refl _                       ≡⟨ sym from-≡↔≡-refl ⟩
   _↔_.from ≡↔≡ P.refl          ≡⟨ cong (_↔_.from ≡↔≡) $ sym $ _↔_.from ≡↔≡ P.sym-refl ⟩∎
   _↔_.from ≡↔≡ (P.sym P.refl)  ∎)
  x≡y

-- The trans function for paths can be expressed in terms of the trans
-- function for equality.

trans≡trans :
  {x≡y : x P.≡ y} {y≡z : y P.≡ z} →
  trans (_↔_.from ≡↔≡ x≡y) (_↔_.from ≡↔≡ y≡z) ≡
  _↔_.from ≡↔≡ (P.trans x≡y y≡z)
trans≡trans {x≡y = x≡y} {y≡z = y≡z} = P.elim₁
  (λ x≡y → trans (_↔_.from ≡↔≡ x≡y) (_↔_.from ≡↔≡ y≡z) ≡
           _↔_.from ≡↔≡ (P.trans x≡y y≡z))
  (trans (_↔_.from ≡↔≡ P.refl) (_↔_.from ≡↔≡ y≡z)  ≡⟨ cong (flip trans _) from-≡↔≡-refl ⟩
   trans (refl _) (_↔_.from ≡↔≡ y≡z)               ≡⟨ trans-reflˡ _ ⟩
   _↔_.from ≡↔≡ y≡z                                ≡⟨ cong (_↔_.from ≡↔≡) $ sym $ _↔_.from ≡↔≡ $ P.trans-reflˡ _ ⟩∎
   _↔_.from ≡↔≡ (P.trans P.refl y≡z)               ∎)
  x≡y

-- The type of embeddings, expressed using equality, is isomorphic to
-- the type of embeddings, expressed using paths.

Embedding↔Embedding :
  {A : Type a} {B : Type b} →
  Embedding A B ↔ PM.Embedding A B
Embedding↔Embedding {A = A} {B = B} =
  Embedding A B                                   ↝⟨ Embedding-as-Σ ⟩
  (∃ λ f → ∀ x y → Is-equivalence (cong f))       ↔⟨ (∃-cong λ f → ∀-cong ext λ x → ∀-cong ext λ y →
                                                      Eq.⇔→≃ (Eq.propositional ext _) (Eq.propositional ext _)
                                                        (λ is → _≃_.is-equivalence $
                                                           Eq.with-other-function
                                                             (
      x P.≡ y                                                  ↔⟨ inverse ≡↔≡ ⟩
      x ≡ y                                                    ↝⟨ Eq.⟨ _ , is ⟩ ⟩
      f x ≡ f y                                                ↔⟨ ≡↔≡ ⟩□
      f x P.≡ f y                                              □)
                                                             (P.cong f)
                                                             (λ eq →
      _↔_.to ≡↔≡ (cong f (_↔_.from ≡↔≡ eq))                     ≡⟨ cong (_↔_.to ≡↔≡) cong≡cong ⟩
      _↔_.to ≡↔≡ (_↔_.from ≡↔≡ (P.cong f eq))                   ≡⟨ _↔_.right-inverse-of ≡↔≡ _ ⟩∎
      P.cong f eq                                               ∎))
                                                        (λ is → _≃_.is-equivalence $
                                                           Eq.with-other-function
                                                             (
      x ≡ y                                                    ↔⟨ ≡↔≡ ⟩
      x P.≡ y                                                  ↝⟨ Eq.⟨ _ , is ⟩ ⟩
      f x P.≡ f y                                              ↔⟨ inverse ≡↔≡ ⟩□
      f x ≡ f y                                                □)
                                                             (cong f)
                                                             (λ eq →
      _↔_.from ≡↔≡ (P.cong f (_↔_.to ≡↔≡ eq))                   ≡⟨ sym cong≡cong ⟩
      cong f (_↔_.from ≡↔≡ (_↔_.to ≡↔≡ eq))                     ≡⟨ cong (cong f) $ _↔_.left-inverse-of ≡↔≡ _ ⟩∎
      cong f eq                                                 ∎))) ⟩
  (∃ λ f → ∀ x y → Is-equivalence (P.cong f))     ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → Is-equivalence↔Is-equivalence) ⟩
  (∃ λ f → ∀ x y → PE.Is-equivalence (P.cong f))  ↝⟨ inverse $ ↔→↔ PM.Embedding-as-Σ ⟩□
  PM.Embedding A B                                □

-- The subst function for paths can be expressed in terms of the subst
-- function for equality.

subst≡subst :
  ∀ {P : A → Type p} {x≡y : x P.≡ y} {p} →
  subst P (_↔_.from ≡↔≡ x≡y) p ≡ P.subst P x≡y p
subst≡subst {P = P} {x≡y} = P.elim
  (λ x≡y → ∀ {p} → subst P (_↔_.from ≡↔≡ x≡y) p ≡ P.subst P x≡y p)
  (λ x {p} →
     subst P (_↔_.from ≡↔≡ P.refl) p  ≡⟨ cong (λ eq → subst P eq p) from-≡↔≡-refl ⟩
     subst P (refl x) p               ≡⟨ subst-refl _ _ ⟩
     p                                ≡⟨ sym $ _↔_.from ≡↔≡ $ P.subst-refl P _ ⟩∎
     P.subst P P.refl p               ∎)
  x≡y

-- A "computation" rule for subst≡subst.

subst≡subst-refl :
  ∀ {P : A → Type p} {p : P x} →
  subst≡subst {x≡y = P.refl} ≡
  trans (cong (λ eq → subst P eq p) from-≡↔≡-refl)
    (trans (subst-refl _ _) (sym $ _↔_.from ≡↔≡ $ P.subst-refl P _))
subst≡subst-refl {P = P} = cong (λ f → f {p = _}) $ _↔_.from ≡↔≡ $
  P.elim-refl
    (λ x≡y → ∀ {p} → subst P (_↔_.from ≡↔≡ x≡y) p ≡ P.subst P x≡y p)
    (λ _ → trans (cong (λ eq → subst P eq _) from-≡↔≡-refl)
             (trans (subst-refl _ _)
                (sym $ _↔_.from ≡↔≡ $ P.subst-refl P _)))

-- Some corollaries.

subst≡↔subst≡ :
  ∀ {eq : x P.≡ y} →
  subst B (_↔_.from ≡↔≡ eq) u ≡ v ↔
  P.subst B eq u P.≡ v
subst≡↔subst≡ {B = B} {u = u} {v = v} {eq = eq} =
  subst B (_↔_.from ≡↔≡ eq) u ≡ v  ↝⟨ ≡⇒↝ _ $ cong (_≡ _) subst≡subst ⟩
  P.subst B eq u ≡ v               ↝⟨ ≡↔≡ ⟩□
  P.subst B eq u P.≡ v             □

subst≡↔[]≡ :
  {eq : x P.≡ y} →
  subst B (_↔_.from ≡↔≡ eq) u ≡ v ↔
  P.[ (λ i → B (eq i)) ] u ≡ v
subst≡↔[]≡ {B = B} {u = u} {v = v} {eq = eq} =
  subst B (_↔_.from ≡↔≡ eq) u ≡ v  ↝⟨ subst≡↔subst≡ ⟩
  P.subst B eq u P.≡ v             ↝⟨ ↔→↔ $ PB.inverse $ P.heterogeneous↔homogeneous _ ⟩□
  P.[ (λ i → B (eq i)) ] u ≡ v     □

-- The dcong function for paths can be expressed using dcong for
-- equality (up to pointwise equality).

dcong≡dcong :
  {f : (x : A) → B x} {x≡y : x P.≡ y} →
  _↔_.to subst≡↔subst≡ (dcong f (_↔_.from ≡↔≡ x≡y)) ≡
  P.dcong f x≡y
dcong≡dcong {B = B} {f = f} {x≡y} = P.elim
  (λ x≡y → _↔_.to subst≡↔subst≡ (dcong f (_↔_.from ≡↔≡ x≡y)) ≡
           P.dcong f x≡y)
  (λ x →
     _↔_.to subst≡↔subst≡ (dcong f (_↔_.from ≡↔≡ P.refl))    ≡⟨⟩

     _↔_.to ≡↔≡ (_↔_.to (≡⇒↝ _ $ cong (_≡ _) subst≡subst) $
       dcong f (_↔_.from ≡↔≡ P.refl))                        ≡⟨ cong (_↔_.to ≡↔≡) $ lemma x ⟩

     _↔_.to ≡↔≡ (_↔_.from ≡↔≡ $ P.subst-refl B (f x))        ≡⟨ _↔_.right-inverse-of ≡↔≡ _ ⟩

     P.subst-refl B (f x)                                    ≡⟨ sym $ _↔_.from ≡↔≡ $ P.dcong-refl f ⟩∎

     P.dcong f P.refl                                        ∎)
  x≡y
  where
  lemma : ∀ _ → _
  lemma _ =
     _↔_.to (≡⇒↝ _ $ cong (_≡ _) subst≡subst)
       (dcong f (_↔_.from ≡↔≡ P.refl))                         ≡⟨ sym $ subst-in-terms-of-≡⇒↝ bijection _ _ _ ⟩

     subst (_≡ _) subst≡subst (dcong f (_↔_.from ≡↔≡ P.refl))  ≡⟨ cong (λ p → subst (_≡ _) p $ dcong f _) $ sym $ sym-sym _ ⟩

     subst (_≡ _) (sym $ sym subst≡subst)
       (dcong f (_↔_.from ≡↔≡ P.refl))                         ≡⟨ subst-trans _ ⟩

     trans (sym (subst≡subst {x≡y = P.refl}))
       (dcong f (_↔_.from ≡↔≡ P.refl))                         ≡⟨ cong (λ p → trans (sym p) (dcong f (_↔_.from ≡↔≡ P.refl)))
                                                                  subst≡subst-refl ⟩
     trans
       (sym $ trans (cong (λ eq → subst B eq _) from-≡↔≡-refl)
                (trans (subst-refl _ _)
                   (sym $ _↔_.from ≡↔≡ $ P.subst-refl B _)))
       (dcong f (_↔_.from ≡↔≡ P.refl))                         ≡⟨ elim₁ (λ {x} p →
                                                                           trans (sym $ trans (cong (λ eq → subst B eq _) p)
                                                                                (trans (subst-refl _ _)
                                                                                (sym $ _↔_.from ≡↔≡ $ P.subst-refl B _)))
                                                                             (dcong f x) ≡
                                                                           trans (sym $ trans (cong (λ eq → subst B eq _) (refl _))
                                                                                (trans (subst-refl _ _)
                                                                                (sym $ _↔_.from ≡↔≡ $ P.subst-refl B _)))
                                                                             (dcong f (refl _)))
                                                                        (refl _)
                                                                        from-≡↔≡-refl ⟩
     trans
       (sym $ trans (cong (λ eq → subst B eq _) (refl _))
                (trans (subst-refl _ _)
                   (sym $ _↔_.from ≡↔≡ $ P.subst-refl B _)))
       (dcong f (refl _))                                      ≡⟨ cong₂ (λ p → trans $ sym $ trans p $ trans (subst-refl _ _) $ sym $
                                                                                _↔_.from ≡↔≡ $ P.subst-refl B _)
                                                                    (cong-refl _)
                                                                    (dcong-refl _) ⟩
     trans
       (sym $ trans (refl _)
                (trans (subst-refl _ _)
                   (sym $ _↔_.from ≡↔≡ $ P.subst-refl B _)))
       (subst-refl B _)                                        ≡⟨ cong (λ p → trans (sym p) (subst-refl _ _)) $ trans-reflˡ _ ⟩

     trans
       (sym $ trans (subst-refl _ _)
                (sym $ _↔_.from ≡↔≡ $ P.subst-refl B _))
       (subst-refl B _)                                        ≡⟨ cong (λ p → trans p (subst-refl _ _)) $ sym-trans _ _ ⟩

     trans
       (trans (sym $ sym $ _↔_.from ≡↔≡ $ P.subst-refl B _)
              (sym $ subst-refl _ _))
       (subst-refl B _)                                        ≡⟨ trans-[trans-sym]- _ _ ⟩

     sym $ sym $ _↔_.from ≡↔≡ $ P.subst-refl B _               ≡⟨ sym-sym _ ⟩∎

     _↔_.from ≡↔≡ $ P.subst-refl B _                           ∎

-- A lemma relating dcong and hcong (for paths).

dcong≡hcong :
  {x≡y : x P.≡ y} (f : (x : A) → B x) →
  dcong f (_↔_.from ≡↔≡ x≡y) ≡ _↔_.from subst≡↔[]≡ (P.hcong f x≡y)
dcong≡hcong {x≡y = x≡y} f =
  dcong f (_↔_.from ≡↔≡ x≡y)                                     ≡⟨ sym $ _↔_.from-to (inverse subst≡↔subst≡) dcong≡dcong ⟩

  _↔_.from subst≡↔subst≡ (P.dcong f x≡y)                         ≡⟨ cong (_↔_.from subst≡↔subst≡) $ _↔_.from ≡↔≡ $ P.dcong≡hcong f ⟩

  _↔_.from subst≡↔subst≡
    (PB._↔_.to (P.heterogeneous↔homogeneous _) (P.hcong f x≡y))  ≡⟨⟩

  _↔_.from subst≡↔[]≡ (P.hcong f x≡y)                            ∎

-- Three corollaries, intended to be used in the implementation of
-- eliminators for HITs. For some examples, see Interval and
-- Quotient.HIT.

subst≡→[]≡ :
  {eq : x P.≡ y} →
  subst B (_↔_.from ≡↔≡ eq) u ≡ v →
  P.[ (λ i → B (eq i)) ] u ≡ v
subst≡→[]≡ = _↔_.to subst≡↔[]≡

dcong-subst≡→[]≡ :
  {eq₁ : x P.≡ y} {eq₂ : subst B (_↔_.from ≡↔≡ eq₁) (f x) ≡ f y} →
  P.hcong f eq₁ ≡ subst≡→[]≡ eq₂ →
  dcong f (_↔_.from ≡↔≡ eq₁) ≡ eq₂
dcong-subst≡→[]≡ {B = B} {f = f} {eq₁} {eq₂} hyp =
  dcong f (_↔_.from ≡↔≡ eq₁)                   ≡⟨ dcong≡hcong f ⟩
  _↔_.from subst≡↔[]≡ (P.hcong f eq₁)          ≡⟨ cong (_↔_.from subst≡↔[]≡) hyp ⟩
  _↔_.from subst≡↔[]≡ (_↔_.to subst≡↔[]≡ eq₂)  ≡⟨ _↔_.left-inverse-of subst≡↔[]≡ _ ⟩∎
  eq₂                                          ∎

cong-≡↔≡ :
  {eq₁ : x P.≡ y} {eq₂ : f x ≡ f y} →
  P.cong f eq₁ ≡ _↔_.to ≡↔≡ eq₂ →
  cong f (_↔_.from ≡↔≡ eq₁) ≡ eq₂
cong-≡↔≡ {f = f} {eq₁ = eq₁} {eq₂} hyp =
  cong f (_↔_.from ≡↔≡ eq₁)      ≡⟨ cong≡cong ⟩
  _↔_.from ≡↔≡ $ P.cong f eq₁    ≡⟨ cong (_↔_.from ≡↔≡) hyp ⟩
  _↔_.from ≡↔≡ $ _↔_.to ≡↔≡ eq₂  ≡⟨ _↔_.left-inverse-of ≡↔≡ _ ⟩∎
  eq₂                            ∎

------------------------------------------------------------------------
-- Univalence

-- CP.Univalence′ is pointwise equivalent to PCP.Univalence′.

Univalence′-CP≃Univalence′-CP :
  {A B : Type ℓ} →
  CP.Univalence′ A B ≃ PCP.Univalence′ A B
Univalence′-CP≃Univalence′-CP {A = A} {B = B} =
  ((A≃B : A CP.≃ B) →
   ∃ λ (x : ∃ λ A≡B → CP.≡⇒≃ A≡B ≡ A≃B) → ∀ y → x ≡ y)       ↔⟨⟩

  ((A≃B : ∃ λ (f : A → B) → CP.Is-equivalence f) →
   ∃ λ (x : ∃ λ A≡B → CP.≡⇒≃ A≡B ≡ A≃B) →
   ∀ y → x ≡ y)                                              ↝⟨ (Π-cong ext (∃-cong λ _ → Is-equivalence-CP↔Is-equivalence-CP) λ A≃B →
                                                                 Σ-cong (lemma₁ A≃B) λ _ →
                                                                 Π-cong ext (lemma₁ A≃B) λ _ →
                                                                 inverse $ Eq.≃-≡ (lemma₁ A≃B)) ⟩
  ((A≃B : ∃ λ (f : A → B) → PCP.Is-equivalence f) →
   ∃ λ (x : ∃ λ A≡B → PCP.≡⇒≃ A≡B ≡ A≃B) →
   ∀ y → x ≡ y)                                              ↔⟨⟩

  ((A≃B : A PCP.≃ B) →
   ∃ λ (x : ∃ λ A≡B → PCP.≡⇒≃ A≡B ≡ A≃B) → ∀ y → x ≡ y)      ↔⟨ Is-equivalence-CP↔Is-equivalence-CP ⟩□

  ((A≃B : A PCP.≃ B) →
   ∃ λ (x : ∃ λ A≡B → PCP.≡⇒≃ A≡B P.≡ A≃B) → ∀ y → x P.≡ y)  □
  where
  lemma₃ :
    (A≡B : A ≡ B) →
    _↔_.to ≃-CP↔≃-CP (CP.≡⇒≃ A≡B) ≡ PCP.≡⇒≃ (_↔_.to ≡↔≡ A≡B)
  lemma₃ = elim¹
    (λ A≡B → _↔_.to ≃-CP↔≃-CP (CP.≡⇒≃ A≡B) ≡ PCP.≡⇒≃ (_↔_.to ≡↔≡ A≡B))
    (_↔_.to ≃-CP↔≃-CP (CP.≡⇒≃ (refl _))  ≡⟨ cong (_↔_.to ≃-CP↔≃-CP) CP.≡⇒≃-refl ⟩
     _↔_.to ≃-CP↔≃-CP CP.id              ≡⟨ _↔_.from ≡↔≡ $ P.Σ-≡,≡→≡ P.refl (PCP.propositional P.ext _ _ _) ⟩
     PCP.id                              ≡⟨ sym $ _↔_.from ≡↔≡ PCP.≡⇒≃-refl ⟩
     PCP.≡⇒≃ P.refl                      ≡⟨ sym $ cong PCP.≡⇒≃ to-≡↔≡-refl ⟩∎
     PCP.≡⇒≃ (_↔_.to ≡↔≡ (refl _))       ∎)

  lemma₂ : ∀ _ _ → _ ≃ _
  lemma₂ A≡B (f , f-eq) =
    CP.≡⇒≃ A≡B ≡ (f , f-eq)                                ↝⟨ inverse $ Eq.≃-≡ (Eq.↔⇒≃ ≃-CP↔≃-CP) ⟩

    _↔_.to ≃-CP↔≃-CP (CP.≡⇒≃ A≡B) ≡
    (f , _↔_.to Is-equivalence-CP↔Is-equivalence-CP f-eq)  ↝⟨ ≡⇒≃ $ cong (_≡ (f , _↔_.to Is-equivalence-CP↔Is-equivalence-CP f-eq)) $
                                                              lemma₃ A≡B ⟩□
    PCP.≡⇒≃ (_↔_.to ≡↔≡ A≡B) ≡
    (f , _↔_.to Is-equivalence-CP↔Is-equivalence-CP f-eq)  □

  lemma₁ :
    ∀ A≃B →
    (∃ λ A≡B → CP.≡⇒≃ A≡B ≡ A≃B) ≃
    (∃ λ A≡B →
         PCP.≡⇒≃ A≡B ≡
         ( proj₁ A≃B
         , _↔_.to Is-equivalence-CP↔Is-equivalence-CP (proj₂ A≃B)
         ))
  lemma₁ A≃B = Σ-cong ≡↔≡ λ A≡B → lemma₂ A≡B A≃B

-- Univalence′ expressed using equality is equivalent to Univalence′
-- expressed using paths.

Univalence′≃Univalence′ :
  {A B : Type ℓ} →
  Univalence′ A B ≃ PU.Univalence′ A B
Univalence′≃Univalence′ {A = A} {B = B} =
  Univalence′ A B      ↝⟨ Univalence′≃Univalence′-CP ext ⟩
  CP.Univalence′ A B   ↝⟨ Univalence′-CP≃Univalence′-CP ⟩
  PCP.Univalence′ A B  ↝⟨ inverse $ _↔_.from ≃↔≃ $ PU.Univalence′≃Univalence′-CP P.ext ⟩□
  PU.Univalence′ A B   □

-- Univalence expressed using equality is equivalent to univalence
-- expressed using paths.

Univalence≃Univalence : Univalence ℓ ≃ PU.Univalence ℓ
Univalence≃Univalence {ℓ = ℓ} =
  ({A B : Type ℓ} → Univalence′ A B)     ↝⟨ implicit-∀-cong ext $ implicit-∀-cong ext Univalence′≃Univalence′ ⟩□
  ({A B : Type ℓ} → PU.Univalence′ A B)  □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- We define what it means to satisfy the universal property
-- of localisation and show that the localisation in Base satisfies
-- it. We will also show that the localisation is uniquely determined
-- by the universal property, and give sufficient criteria for
-- satisfying the universal property.

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.CommRing.Localisation.UniversalProperty where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Transport
open import Cubical.Functions.FunExtEquiv
open import Cubical.Functions.Surjection
open import Cubical.Functions.Embedding

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.RingSolver.ReflectionSolving
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Localisation.Base

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

open Iso

private
  variable
    ℓ ℓ' : Level

module _ (R' : CommRing {ℓ}) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClosedSubset R' S') where
 open isMultClosedSubset
 private R = fst R'
 open CommRingStr (snd R') hiding (is-set)
 open Theory (CommRing→Ring R')
 open RingHom

 hasLocUniversalProp : (A : CommRing {ℓ}) (φ : CommRingHom R' A)
                     → (∀ s → s ∈ S' → f φ s ∈ A ˣ)
                     → Type (ℓ-suc ℓ)
 hasLocUniversalProp A φ _ = (B : CommRing {ℓ}) (ψ : CommRingHom R' B)
                           → (∀ s → s ∈ S' → f ψ s ∈ B ˣ)
                           → ∃![ χ ∈ CommRingHom A B ] (f χ) ∘ (f φ) ≡ (f ψ)

 UniversalPropIsProp : (A : CommRing {ℓ}) (φ : CommRingHom R' A)
                     → (φS⊆Aˣ : ∀ s → s ∈ S' → f φ s ∈ A ˣ)
                     → isProp (hasLocUniversalProp A φ φS⊆Aˣ)
 UniversalPropIsProp A φ φS⊆Aˣ = isPropΠ3 (λ _ _ _ → isPropIsContr)

 -- S⁻¹R has the universal property
 module S⁻¹RUniversalProp where
  open Loc R' S' SMultClosedSubset
  _/1 : R → S⁻¹R
  r /1 = [ r , 1r , SMultClosedSubset .containsOne ]

  /1AsCommRingHom : CommRingHom R' S⁻¹RAsCommRing
  f /1AsCommRingHom = _/1
  pres1 /1AsCommRingHom = refl
  isHom+ /1AsCommRingHom r r' = cong [_] (≡-× (cong₂ (_+_) (sym (·Rid r)) (sym (·Rid r')))
                                         (Σ≡Prop (λ x → S' x .snd) (sym (·Lid 1r))))
  isHom· /1AsCommRingHom r r' = cong [_] (≡-× refl (Σ≡Prop (λ x → S' x .snd) (sym (·Lid 1r))))

  S⁻¹Rˣ = S⁻¹RAsCommRing ˣ
  S/1⊆S⁻¹Rˣ : ∀ s → s ∈ S' → (s /1) ∈ S⁻¹Rˣ
  S/1⊆S⁻¹Rˣ s s∈S' = [ 1r , s , s∈S' ] , eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path s)
   where
   path : ∀ s → 1r · (s · 1r) · 1r ≡ 1r · 1r · (1r  · s)
   path = solve R'

  S⁻¹RHasUniversalProp : hasLocUniversalProp S⁻¹RAsCommRing /1AsCommRingHom S/1⊆S⁻¹Rˣ
  S⁻¹RHasUniversalProp B' ψ ψS⊆Bˣ = (χ , funExt χcomp) , χunique
   where
   B = fst B'
   open CommRingStr (snd B') renaming  ( is-set to Bset ; _·_ to _·B_ ; 1r to 1b
                                       ; _+_ to _+B_
                                       ; ·Assoc to ·B-assoc ; ·-comm to ·B-comm
                                       ; ·Lid to ·B-lid ; ·Rid to ·B-rid
                                       ; ·Ldist+ to ·B-ldist-+)
   open Units B' renaming (Rˣ to Bˣ ; RˣMultClosed to BˣMultClosed ; RˣContainsOne to BˣContainsOne)
   open Theory (CommRing→Ring B') renaming (·-assoc2 to ·B-assoc2)
   open CommTheory B' renaming (·-commAssocl to ·B-commAssocl ; ·-commAssocSwap to ·B-commAssocSwap)

   χ : CommRingHom S⁻¹RAsCommRing B'
   f χ = SQ.rec Bset fχ fχcoh
    where
    fχ : R × S → B
    fχ (r , s , s∈S') = (f ψ r) ·B ((f ψ s) ⁻¹) ⦃ ψS⊆Bˣ s s∈S' ⦄
    fχcoh : (a b : R × S) → a ≈ b → fχ a ≡ fχ b
    fχcoh (r , s , s∈S') (r' , s' , s'∈S') ((u , u∈S') , p) = instancepath
     ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦃ ψS⊆Bˣ (u · s · s')
            (SMultClosedSubset .multClosed (SMultClosedSubset .multClosed u∈S' s∈S') s'∈S') ⦄
     ⦃ BˣMultClosed _ _ ⦃ ψS⊆Bˣ (u · s) (SMultClosedSubset .multClosed u∈S' s∈S') ⦄
                        ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦄
     ⦃ ψS⊆Bˣ (u · s) (SMultClosedSubset .multClosed u∈S' s∈S') ⦄
     where
     -- only a few indidividual steps can be solved by the ring solver yet
     instancepath : ⦃ _ : f ψ s ∈ Bˣ ⦄ ⦃ _ : f ψ s' ∈ Bˣ ⦄
                    ⦃ _ : f ψ (u · s · s') ∈ Bˣ ⦄ ⦃ _ : f ψ (u · s) ·B f ψ s' ∈ Bˣ ⦄
                    ⦃ _ : f ψ (u · s) ∈ Bˣ ⦄
                  → f ψ r ·B f ψ s ⁻¹ ≡ f ψ r' ·B f ψ s' ⁻¹
     instancepath = f ψ r ·B f ψ s ⁻¹

                  ≡⟨ sym (·B-rid _) ⟩

                    f ψ r ·B f ψ s ⁻¹ ·B 1b

                  ≡⟨ cong (f ψ r ·B f ψ s ⁻¹ ·B_) (sym (·-rinv _)) ⟩

                    f ψ r ·B f ψ s ⁻¹ ·B (f ψ (u · s · s') ·B f ψ (u · s · s') ⁻¹)

                  ≡⟨ ·B-assoc _ _ _ ⟩

                    f ψ r ·B f ψ s ⁻¹ ·B f ψ (u · s · s') ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (λ x → f ψ r ·B f ψ s ⁻¹ ·B x ·B f ψ (u · s · s') ⁻¹) (isHom· ψ _ _) ⟩

                    f ψ r ·B f ψ s ⁻¹ ·B (f ψ (u · s) ·B f ψ s') ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (_·B f ψ (u · s · s') ⁻¹) (·B-assoc _ _ _) ⟩

                    f ψ r ·B f ψ s ⁻¹ ·B f ψ (u · s) ·B f ψ s' ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (λ x → f ψ r ·B f ψ s ⁻¹ ·B x ·B f ψ s' ·B f ψ (u · s · s') ⁻¹)
                          (isHom· ψ _ _) ⟩

                    f ψ r ·B f ψ s ⁻¹ ·B (f ψ u ·B f ψ s) ·B f ψ s' ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (λ x → x ·B f ψ s' ·B f ψ (u · s · s') ⁻¹) (·B-commAssocSwap _ _ _ _) ⟩

                    f ψ r ·B f ψ u ·B (f ψ s ⁻¹ ·B f ψ s) ·B f ψ s' ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ (λ i → ·B-comm (f ψ r) (f ψ u) i ·B (·-linv (f ψ s) i)
                                                      ·B f ψ s' ·B f ψ (u · s · s') ⁻¹) ⟩

                    f ψ u ·B f ψ r ·B 1b ·B f ψ s' ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ (λ i → (·B-rid (sym (isHom· ψ u r) i) i) ·B f ψ s' ·B f ψ (u · s · s') ⁻¹) ⟩

                    f ψ (u · r) ·B f ψ s' ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (_·B f ψ (u · s · s') ⁻¹) (sym (isHom· ψ _ _)) ⟩

                    f ψ (u · r · s') ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (λ x → f ψ x ·B f ψ (u · s · s') ⁻¹) p ⟩

                    f ψ (u · r' · s) ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (_·B f ψ (u · s · s') ⁻¹) (isHom· ψ _ _) ⟩

                    f ψ (u · r') ·B f ψ s ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (λ x → x ·B f ψ s ·B f ψ (u · s · s') ⁻¹) (isHom· ψ _ _) ⟩

                    f ψ u ·B f ψ r' ·B f ψ s ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (_·B f ψ (u · s · s') ⁻¹) (sym (·B-assoc _ _ _)) ⟩

                    f ψ u ·B (f ψ r' ·B f ψ s) ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (_·B f ψ (u · s · s') ⁻¹) (·B-commAssocl _ _ _) ⟩

                    f ψ r' ·B (f ψ u ·B f ψ s) ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (λ x → f ψ r' ·B x ·B f ψ (u · s · s') ⁻¹) (sym (isHom· ψ _ _)) ⟩

                    f ψ r' ·B f ψ (u · s) ·B f ψ (u · s · s') ⁻¹

                  ≡⟨ cong (f ψ r' ·B f ψ (u · s) ·B_) (unitCong (isHom· ψ _ _)) ⟩

                    f ψ r' ·B f ψ (u · s) ·B (f ψ (u · s) ·B f ψ s') ⁻¹

                  ≡⟨ cong (f ψ r' ·B f ψ (u · s) ·B_) (⁻¹-dist-· _ _) ⟩

                    f ψ r' ·B f ψ (u · s) ·B (f ψ (u · s) ⁻¹ ·B f ψ s' ⁻¹)

                  ≡⟨ ·B-assoc2 _ _ _ _ ⟩

                    f ψ r' ·B (f ψ (u · s) ·B f ψ (u · s) ⁻¹) ·B f ψ s' ⁻¹

                  ≡⟨ cong (λ x → f ψ r' ·B x ·B f ψ s' ⁻¹) (·-rinv _) ⟩

                    f ψ r' ·B 1b ·B f ψ s' ⁻¹

                  ≡⟨ cong (_·B f ψ s' ⁻¹) (·B-rid _) ⟩

                    f ψ r' ·B f ψ s' ⁻¹ ∎

   pres1 χ = instancepres1χ ⦃ ψS⊆Bˣ 1r (SMultClosedSubset .containsOne) ⦄ ⦃ BˣContainsOne ⦄
    where
    instancepres1χ : ⦃ _ : f ψ 1r ∈ Bˣ ⦄ ⦃ _ : 1b ∈ Bˣ ⦄
                   → f ψ 1r ·B (f ψ 1r) ⁻¹ ≡ 1b
    instancepres1χ =  (λ i → (pres1 ψ i) ·B (unitCong (pres1 ψ) i))
                    ∙ (λ i → ·B-lid (1⁻¹≡1 i) i)

   isHom+ χ = elimProp2 (λ _ _ _ _ → Bset _ _ _ _) isHom+[]
    where
    isHom+[] : (a b : R × S) → f χ ([ a ] +ₗ [ b ]) ≡ (f χ [ a ]) +B (f χ [ b ])
    isHom+[] (r , s , s∈S') (r' , s' , s'∈S') = instancepath
     ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦃ ψS⊆Bˣ (s · s') (SMultClosedSubset .multClosed s∈S' s'∈S') ⦄
     ⦃ BˣMultClosed _ _ ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦄
     where
     -- only a few indidividual steps can be solved by the ring solver yet
     instancepath : ⦃ _ : f ψ s ∈ Bˣ ⦄ ⦃ _ : f ψ s' ∈ Bˣ ⦄
                    ⦃ _ : f ψ (s · s') ∈ Bˣ ⦄ ⦃ _ : f ψ s ·B f ψ s' ∈ Bˣ ⦄
                → f ψ (r · s' + r' · s) ·B f ψ (s · s') ⁻¹ ≡ f ψ r ·B f ψ s ⁻¹ +B f ψ r' ·B f ψ s' ⁻¹
     instancepath =
            f ψ (r · s' + r' · s) ·B f ψ (s · s') ⁻¹

          ≡⟨ (λ i → isHom+ ψ (r · s') (r' · s) i ·B unitCong (isHom· ψ s s') i) ⟩

            (f ψ (r · s') +B f ψ (r' · s)) ·B (f ψ s ·B f ψ s') ⁻¹

          ≡⟨ (λ i → (isHom· ψ r s' i +B isHom· ψ r' s i) ·B ⁻¹-dist-· (f ψ s) (f ψ s') i) ⟩

            (f ψ r ·B f ψ s' +B f ψ r' ·B f ψ s) ·B (f ψ s ⁻¹ ·B f ψ s' ⁻¹)

          ≡⟨ ·B-ldist-+ _ _ _ ⟩

            f ψ r ·B f ψ s' ·B (f ψ s ⁻¹ ·B f ψ s' ⁻¹) +B f ψ r' ·B f ψ s ·B (f ψ s ⁻¹ ·B f ψ s' ⁻¹)

          ≡⟨ (λ i → ·B-commAssocSwap (f ψ r) (f ψ s') (f ψ s ⁻¹) (f ψ s' ⁻¹) i
                 +B ·B-assoc2 (f ψ r') (f ψ s) (f ψ s ⁻¹) (f ψ s' ⁻¹) i) ⟩

            f ψ r ·B f ψ s ⁻¹ ·B (f ψ s' ·B f ψ s' ⁻¹) +B f ψ r' ·B (f ψ s ·B f ψ s ⁻¹) ·B f ψ s' ⁻¹

          ≡⟨ (λ i → f ψ r ·B f ψ s ⁻¹ ·B (·-rinv (f ψ s') i)
                 +B f ψ r' ·B (·-rinv (f ψ s) i) ·B f ψ s' ⁻¹) ⟩

            f ψ r ·B f ψ s ⁻¹ ·B 1b +B f ψ r' ·B 1b ·B f ψ s' ⁻¹

          ≡⟨ (λ i → ·B-rid (f ψ r ·B f ψ s ⁻¹) i +B ·B-rid (f ψ r') i ·B f ψ s' ⁻¹) ⟩

            f ψ r ·B f ψ s ⁻¹ +B f ψ r' ·B f ψ s' ⁻¹ ∎

   isHom· χ = elimProp2 (λ _ _ _ _ → Bset _ _ _ _) isHom·[]
    where
    isHom·[] : (a b : R × S) → f χ ([ a ] ·ₗ [ b ]) ≡ (f χ [ a ]) ·B (f χ [ b ])
    isHom·[] (r , s , s∈S') (r' , s' , s'∈S') = instancepath
     ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦃ ψS⊆Bˣ (s · s') (SMultClosedSubset .multClosed s∈S' s'∈S') ⦄
     ⦃ BˣMultClosed _ _ ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦄
     where
     -- only a indidividual steps can be solved by the ring solver yet
     instancepath : ⦃ _ : f ψ s ∈ Bˣ ⦄ ⦃ _ : f ψ s' ∈ Bˣ ⦄
                    ⦃ _ : f ψ (s · s') ∈ Bˣ ⦄ ⦃ _ : f ψ s ·B f ψ s' ∈ Bˣ ⦄
                  → f ψ (r · r') ·B f ψ (s · s') ⁻¹ ≡ (f ψ r ·B f ψ s ⁻¹) ·B (f ψ r' ·B f ψ s' ⁻¹)
     instancepath = f ψ (r · r') ·B f ψ (s · s') ⁻¹

                  ≡⟨ (λ i → isHom· ψ r r' i ·B unitCong (isHom· ψ s s') i) ⟩

                    f ψ r ·B f ψ r' ·B (f ψ s ·B f ψ s') ⁻¹

                  ≡⟨ cong (f ψ r ·B f ψ r' ·B_) (⁻¹-dist-· _ _) ⟩

                    f ψ r ·B f ψ r' ·B (f ψ s ⁻¹ ·B f ψ s' ⁻¹)

                  ≡⟨ ·B-commAssocSwap _ _ _ _ ⟩

                    f ψ r ·B f ψ s ⁻¹ ·B (f ψ r' ·B f ψ s' ⁻¹) ∎

   χcomp : (r : R) → f χ (r /1) ≡ f ψ r
   χcomp = instanceχcomp ⦃ ψS⊆Bˣ 1r (SMultClosedSubset .containsOne) ⦄ ⦃ Units.RˣContainsOne B' ⦄
    where
    instanceχcomp : ⦃ _ : f ψ 1r ∈ Bˣ ⦄ ⦃ _ : 1b ∈ Bˣ ⦄
                    (r : R) → f ψ r ·B (f ψ 1r) ⁻¹ ≡ f ψ r
    instanceχcomp r = f ψ r ·B (f ψ 1r) ⁻¹ ≡⟨ cong (f ψ r ·B_) (unitCong (pres1 ψ)) ⟩
                      f ψ r ·B 1b ⁻¹       ≡⟨ cong (f ψ r ·B_) 1⁻¹≡1 ⟩
                      f ψ r ·B 1b          ≡⟨ ·B-rid _ ⟩
                      f ψ r ∎

   χunique : (y : Σ[ χ' ∈ CommRingHom S⁻¹RAsCommRing B' ] f χ' ∘ _/1 ≡ f ψ)
           → (χ , funExt χcomp) ≡ y
   χunique (χ' , χ'/1≡ψ) = Σ≡Prop (λ x → isSetΠ (λ _ → Bset) _ _) (RingHom≡f _ _ fχ≡fχ')
    where
    open RingHomRespUnits {A' = S⁻¹RAsCommRing} {B' = B'} χ'
                          renaming (φ[x⁻¹]≡φ[x]⁻¹ to χ'[x⁻¹]≡χ'[x]⁻¹)

    []-path : (a : R × S) → f χ [ a ] ≡ f χ' [ a ]
    []-path (r , s , s∈S') = instancepath ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ S/1⊆S⁻¹Rˣ s s∈S' ⦄
                                          ⦃ RingHomRespInv _ ⦃ S/1⊆S⁻¹Rˣ s s∈S' ⦄ ⦄
     where
     open Units S⁻¹RAsCommRing renaming (_⁻¹ to _⁻¹ˡ ; inverseUniqueness to S⁻¹RInverseUniqueness)
                               hiding (unitCong)

     s-inv : ⦃ s/1∈S⁻¹Rˣ : s /1 ∈ S⁻¹Rˣ ⦄ → s /1 ⁻¹ˡ ≡ [ 1r , s , s∈S' ]
     s-inv ⦃ s/1∈S⁻¹Rˣ ⦄ = PathPΣ (S⁻¹RInverseUniqueness (s /1) s/1∈S⁻¹Rˣ
                           (_ , eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path s))) .fst
      where
      path : ∀ s → 1r · (s · 1r) · 1r ≡ 1r · 1r · (1r · s)
      path = solve R'

     ·ₗ-path : [ r , s , s∈S' ] ≡   [ r , 1r , SMultClosedSubset .containsOne ]
                                 ·ₗ [ 1r , s , s∈S' ]
     ·ₗ-path = cong [_] (≡-× (sym (·Rid r)) (Σ≡Prop (λ x → S' x .snd) (sym (·Lid s))))

     instancepath : ⦃ _ : f ψ s ∈ Bˣ ⦄ ⦃ _ : s /1 ∈ S⁻¹Rˣ ⦄ ⦃ _ : f χ' (s /1) ∈ Bˣ ⦄
                  → f ψ r ·B f ψ s ⁻¹ ≡ f χ' [ r , s , s∈S' ]
     instancepath = f ψ r ·B f ψ s ⁻¹

                  ≡⟨ cong (f ψ r ·B_) (unitCong (cong (λ φ → φ s) (sym χ'/1≡ψ))) ⟩

                    f ψ r ·B f χ' (s /1) ⁻¹

                  ≡⟨ cong (f ψ r ·B_) (sym (χ'[x⁻¹]≡χ'[x]⁻¹ _)) ⟩

                    f ψ r ·B f χ' (s /1 ⁻¹ˡ)

                  ≡⟨ cong (λ x → f ψ r ·B f χ' x) s-inv ⟩

                    f ψ r ·B f χ' [ 1r , s , s∈S' ]

                  ≡⟨ cong (_·B f χ' [ 1r , s , s∈S' ]) (cong (λ φ → φ r) (sym χ'/1≡ψ)) ⟩

                    f χ' [ r , 1r , SMultClosedSubset .containsOne ] ·B f χ' [ 1r , s , s∈S' ]

                  ≡⟨ sym (isHom· χ' _ _) ⟩

                    f χ' ([ r , 1r , SMultClosedSubset .containsOne ] ·ₗ [ 1r , s , s∈S' ])

                  ≡⟨ cong (f χ') (sym ·ₗ-path) ⟩

                    f χ' [ r , s , s∈S' ] ∎

    fχ≡fχ' : f χ ≡ f χ'
    fχ≡fχ' = funExt (SQ.elimProp (λ _ → Bset _ _) []-path)

 -- sufficient conditions for having the universal property
 -- used as API in the leanprover-community/mathlib
 -- Corollary 3.2 in Atiyah-McDonald
 open S⁻¹RUniversalProp
 open Loc R' S' SMultClosedSubset

 record PathToS⁻¹R (A' : CommRing {ℓ}) (φ : CommRingHom R' A') : Type ℓ where
  constructor
   pathtoS⁻¹R
  open Units A' renaming (Rˣ to Aˣ)
  open CommRingStr (snd A') renaming (is-set to Aset ; 0r to 0a ; _·_ to _·A_)
  field
   φS⊆Aˣ : ∀ s → s ∈ S' → f φ s ∈ Aˣ
   kerφ⊆annS : ∀ r → f φ r ≡ 0a → ∃[ s ∈ S ] (s .fst) · r ≡ 0r
   surχ : ∀ a → ∃[ x ∈ R × S ] f φ (x .fst) ·A (f φ (x .snd .fst) ⁻¹) ⦃ φS⊆Aˣ _ (x .snd .snd) ⦄ ≡ a

 S⁻¹RChar : (A' : CommRing {ℓ}) (φ : CommRingHom R' A')
          → PathToS⁻¹R A' φ
          → S⁻¹RAsCommRing ≡ A'
 S⁻¹RChar A' φ cond = CommRingPath S⁻¹RAsCommRing A' .fst
                    (S⁻¹R≃A , record { pres1 = pres1 χ ; isHom+ = isHom+ χ ; isHom· = isHom· χ })
  where
  open CommRingStr (snd A') renaming ( is-set to Aset ; 0r to 0a ; _·_ to _·A_ ; 1r to 1a
                                      ; ·Rid to ·A-rid)
  open Units A' renaming (Rˣ to Aˣ ; RˣInvClosed to AˣInvClosed)
  open PathToS⁻¹R ⦃...⦄
  private
   A = fst A'
   instance
    _ = cond
   χ = (S⁻¹RHasUniversalProp A' φ φS⊆Aˣ .fst .fst)
   open HomTheory χ

  S⁻¹R≃A : S⁻¹R ≃ A
  S⁻¹R≃A = f χ , isEmbedding×isSurjection→isEquiv (Embχ , Surχ)
   where
   Embχ : isEmbedding (f χ)
   Embχ = injEmbedding squash/ Aset (ker≡0→inj λ {x} → kerχ≡0 x)
    where
    kerχ≡0 : (r/s : S⁻¹R) → f χ r/s ≡ 0a → r/s ≡ 0ₗ
    kerχ≡0 = SQ.elimProp (λ _ → isPropΠ λ _ → squash/ _ _) kerχ≡[]
     where
     kerχ≡[] : (a : R × S) → f χ [ a ] ≡ 0a → [ a ] ≡ 0ₗ
     kerχ≡[] (r , s , s∈S') p = PT.rec (squash/ _ _) Σhelper
                                       (kerφ⊆annS r (UnitsAreNotZeroDivisors _ _ p))
      where
      instance
       _ : f φ s ∈ Aˣ
       _ = φS⊆Aˣ s s∈S'
       _ : f φ s ⁻¹ ∈ Aˣ
       _ = AˣInvClosed _

      Σhelper : Σ[ s ∈ S ] (s .fst) · r ≡ 0r → [ r , s , s∈S' ] ≡ 0ₗ
      Σhelper ((u , u∈S') , q) = eq/ _ _ ((u , u∈S') , path)
       where
       path : u · r · 1r ≡ u · 0r · s
       path = (λ i → ·Rid (q  i) i) ∙∙ sym (0LeftAnnihilates _)
                                    ∙∙ cong (_· s) (sym (0RightAnnihilates _))

   Surχ : isSurjection (f χ)
   Surχ a = PT.rec propTruncIsProp (λ x → PT.∣ [ x .fst ] , x .snd ∣) (surχ a)

max_stars_repo_name: L-TChen/cubical

max_issues_repo_name: L-TChen/cubical

max_forks_repo_name: L-TChen/cubical


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

import Light.Library.Relation.Decidable as Decidable
open import Light.Package using (Package)

module Light.Library.Relation.Binary.Decidable where

open import Light.Library.Relation.Binary using (Binary)
open import Light.Level using (Setω)

module _ ⦃ decidable‐package : Package record {Decidable} ⦄ where
      DecidableBinary : Setω
      DecidableBinary = ∀ {aℓ bℓ} (𝕒 : Set aℓ) (𝕓 : Set bℓ) → Binary 𝕒 𝕓

      DecidableSelfBinary : Setω
      DecidableSelfBinary = ∀ {aℓ} (𝕒 : Set aℓ) → Binary 𝕒 𝕒

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib