text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.Cospan where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category
open import Cubical.Data.Unit
open import Cubical.Data.Empty

open Category

data 𝟛 : Type ℓ-zero where
  ⓪ : 𝟛
  ① : 𝟛
  ② : 𝟛

CospanCat : Category ℓ-zero ℓ-zero
CospanCat .ob = 𝟛

CospanCat .Hom[_,_] ⓪ ① = Unit
CospanCat .Hom[_,_] ② ① = Unit
CospanCat .Hom[_,_] ⓪ ⓪ = Unit
CospanCat .Hom[_,_] ① ① = Unit
CospanCat .Hom[_,_] ② ② = Unit
CospanCat .Hom[_,_] _ _ = ⊥

CospanCat ._⋆_ {x = ⓪} {⓪} {⓪} f g = tt
CospanCat ._⋆_ {x = ①} {①} {①} f g = tt
CospanCat ._⋆_ {x = ②} {②} {②} f g = tt
CospanCat ._⋆_ {x = ⓪} {①} {①} f g = tt
CospanCat ._⋆_ {x = ②} {①} {①} f g = tt
CospanCat ._⋆_ {x = ⓪} {⓪} {①} f g = tt
CospanCat ._⋆_ {x = ②} {②} {①} f g = tt

CospanCat .id {⓪} = tt
CospanCat .id {①} = tt
CospanCat .id {②} = tt

CospanCat .⋆IdL {⓪} {①} _ = refl
CospanCat .⋆IdL {②} {①} _ = refl
CospanCat .⋆IdL {⓪} {⓪} _ = refl
CospanCat .⋆IdL {①} {①} _ = refl
CospanCat .⋆IdL {②} {②} _ = refl

CospanCat .⋆IdR {⓪} {①} _ = refl
CospanCat .⋆IdR {②} {①} _ = refl
CospanCat .⋆IdR {⓪} {⓪} _ = refl
CospanCat .⋆IdR {①} {①} _ = refl
CospanCat .⋆IdR {②} {②} _ = refl

CospanCat .⋆Assoc {⓪} {⓪} {⓪} {⓪} _ _ _ = refl
CospanCat .⋆Assoc {⓪} {⓪} {⓪} {①} _ _ _ = refl
CospanCat .⋆Assoc {⓪} {⓪} {①} {①} _ _ _ = refl
CospanCat .⋆Assoc {⓪} {①} {①} {①} _ _ _ = refl
CospanCat .⋆Assoc {①} {①} {①} {①} _ _ _ = refl
CospanCat .⋆Assoc {②} {②} {②} {②} _ _ _ = refl
CospanCat .⋆Assoc {②} {②} {②} {①} _ _ _ = refl
CospanCat .⋆Assoc {②} {②} {①} {①} _ _ _ = refl
CospanCat .⋆Assoc {②} {①} {①} {①} _ _ _ = refl

CospanCat .isSetHom {⓪} {⓪} = isSetUnit
CospanCat .isSetHom {⓪} {①} = isSetUnit
CospanCat .isSetHom {①} {①} = isSetUnit
CospanCat .isSetHom {②} {①} = isSetUnit
CospanCat .isSetHom {②} {②} = isSetUnit

max_stars_repo_name: mzeuner/cubical

max_issues_repo_name: mzeuner/cubical

max_forks_repo_name: mzeuner/cubical


text:
import      Lvl
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.InfiniteDimensional
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

open VectorSpace(vectorSpace)

open import Data.Tuple using (_⨯_ ; _,_)
open import Logic
open import Logic.Predicate
open import Numeral.CoordinateVector as Vec using () renaming (Vector to Vec)
open import Numeral.Finite
open import Numeral.Natural
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_ ; [∋]-binaryRelator)
import      Structure.Operator.Vector.FiniteDimensional as FiniteDimensional
open import Structure.Operator.Vector.LinearCombination ⦃ vectorSpace = vectorSpace ⦄
open import Syntax.Function

private variable ℓ ℓₗ : Lvl.Level
private variable n : ℕ

InfiniteDimensional = ∀{n} → ∃(vf ↦ FiniteDimensional.Spanning ⦃ vectorSpace = vectorSpace ⦄ {n}(vf))

-- TODO: Not sure if correct
-- This states that all finite sequences `vf` of length `n` (in terms of `Vec`) that consists of elements from the set `vs` satisfies `P`.
-- This can be used in infinite-dimensional vector spaces to define linear independence, span and basis by: `∃(n ↦ AllFiniteSubsets(n)(P)(vs))`
AllFiniteSubsets : (n : ℕ) → (Vec(n)(V) → Stmt{ℓ}) → (PredSet{ℓₗ}(V) → Stmt)
AllFiniteSubsets(n) P(vs) = (∀{vf : Vec(n)(V)} ⦃ distinct : Vec.Distinct(vf) ⦄ → (∀{i : 𝕟(n)} → (Vec.proj(vf)(i) ∈ vs)) → P(vf))

LinearlyIndependent : PredSet{ℓₗ}(V) → Stmt
LinearlyIndependent(vs) = ∃(n ↦ AllFiniteSubsets(n)(FiniteDimensional.LinearlyIndependent)(vs))

Spanning : PredSet{ℓₗ}(V) → Stmt
Spanning(vs) = ∃(n ↦ AllFiniteSubsets(n)(FiniteDimensional.Spanning)(vs))

-- Also called: Hamel basis (TODO: I think)
Basis : PredSet{ℓₗ}(V) → Stmt
Basis(vs) = ∃(n ↦ AllFiniteSubsets(n)(FiniteDimensional.Basis)(vs))

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:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Algebra.Category.Semigroupoid where

open import Core

-- A semigroupoid is a set of objects and morphisms between objects
-- together with an associative binary function that combines morphisms.

record Semigroupoid {c h r} : Set (lsuc (c ⊔ h ⊔ r)) where
  field
    Ob  : Set c
    Hom : Ob → Ob → Set h
    Eq  : ∀ {A B} → Equiv {r = r} (Hom A B)
    _∘_ : ∀ {A B C} → Hom B C → Hom A B → Hom A C

  infixl 6 _∘_

  open module MyEquiv {A} {B} = Equiv (Eq {A} {B}) public

  field
    ∘-cong :
      ∀ {A B C}
        {f1 f2 : Hom B C} {g1 g2 : Hom A B}
      → f1 ≈ f2 → g1 ≈ g2 → f1 ∘ g1 ≈ f2 ∘ g2

    assoc :
      ∀ {A B C D}
        (f : Hom C D) (g : Hom B C) (h : Hom A B)
      → (f ∘ g) ∘ h ≈ f ∘ (g ∘ h)

  Epic : ∀ {A B} → (f : Hom A B) → Set _
  Epic f = ∀ {C} {g1 g2 : Hom _ C} → g1 ∘ f ≈ g2 ∘ f → g1 ≈ g2

  Monic : ∀ {B C} → (f : Hom B C) → Set _
  Monic f = ∀ {A} {g1 g2 : Hom A _} → f ∘ g1 ≈ f ∘ g2 → g1 ≈ g2

  Unique : ∀ {A B} → (f : Hom A B) → Set _
  Unique f = ∀ g → f ≈ g

  IsProduct : ∀ A B AB → (fst : Hom AB A) (snd : Hom AB B) → Set _
  IsProduct A B AB fst snd =
    ∀ AB' (fst' : Hom AB' A) (snd' : Hom AB' B) →
    ∃ (λ (u : Hom AB' AB) → Unique u × (fst ∘ u ≈ fst') × (snd ∘ u ≈ snd'))

  record Product A B : Set (c ⊔ h ⊔ r) where
    field
      A×B  : Ob
      cfst : Hom A×B A
      csnd : Hom A×B B
      isProduct : IsProduct A B A×B cfst csnd

  record _bimonic_ A B : Set (c ⊔ h ⊔ r) where
    field
      to   : Hom A B
      from : Hom B A
      to-monic   : Monic to
      from-monic : Monic from

-- A semifunctor is a composition-preserving mapping from a semigroupoid
-- to another.

record Semifunctor
           {cc ch cr dc dh dr}
           (C : Semigroupoid {cc} {ch} {cr})
           (D : Semigroupoid {dc} {dh} {dr})
           : Set (cc ⊔ ch ⊔ cr ⊔ dc ⊔ dh ⊔ dr)
       where

  private
    module C = Semigroupoid C
    module D = Semigroupoid D

  field
    F   : C.Ob → D.Ob
    map : ∀ {A B} → C.Hom A B → D.Hom (F A) (F B)

    map-cong :
      ∀ {A B} {f g : C.Hom A B}
      → f C.≈ g
      → map f D.≈ map g

    ∘-preserving :
      ∀ {A B C}
        (f : C.Hom B C) (g : C.Hom A B)
      → map (f C.∘ g) D.≈ map f D.∘ map g

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
module par-swap.union-confluent where

open import par-swap
open import par-swap.properties
open import par-swap.confluent
open import par-swap.dpg

open import Data.Nat using (_+_ ;  _≤′_ ; _<′_ ; suc ; zero ; ≤′-refl ; ℕ)
open import Data.Nat.Properties.Simple using ( +-comm ; +-assoc)
open import Data.Nat.Properties using (s≤′s ; z≤′n)
open import Data.MoreNatProp using (≤′-trans ; suc≤′⇒≤′)
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Data.Empty

open import Induction.Nat using (<-rec)
open import Induction.Lexicographic using ()
open import Induction using ()
open import Induction.WellFounded using ()
open import Level using ()
open import Relation.Binary using (Rel)

open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Environment as Env
open import Esterel.Context
open import Esterel.Lang.Binding

open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; subst ; cong ; trans ;
         module ≡-Reasoning ; cong₂ ; subst₂ ; inspect)
open import sn-calculus
open import context-properties -- get view, E-views

open import binding-preserve using (sn⟶-maintains-binding ; sn⟶*-maintains-binding)
open import noetherian using (noetherian ; ∥_∥s)
open import sn-calculus-props

∥R-preserves-∥∥s : ∀ {p q} -> p ∥R q -> ∥ q ∥s ≡ ∥ p ∥s
∥R-preserves-∥∥s (∥Rstep{C}{p}{q} d≐C⟦p∥q⟧c)
  rewrite sym (unplugc d≐C⟦p∥q⟧c) = ∥∥par-sym p q C where

  ∥∥par-sym : ∀ p q C ->  ∥ C ⟦ q ∥ p ⟧c ∥s ≡ ∥ C ⟦ p ∥ q ⟧c ∥s
  ∥∥par-sym p q [] rewrite +-comm ∥ p ∥s ∥ q ∥s = refl
  ∥∥par-sym p q (_ ∷ C) with ∥∥par-sym p q C
  ∥∥par-sym p q (ceval (epar₁ _) ∷ C)    | R rewrite R = refl
  ∥∥par-sym p q (ceval (epar₂ _) ∷ C)    | R rewrite R = refl
  ∥∥par-sym p q (ceval (eseq _) ∷ C)     | R rewrite R = refl
  ∥∥par-sym p q (ceval (eloopˢ _) ∷ C)   | R rewrite R = refl
  ∥∥par-sym p q (ceval (esuspend _) ∷ C) | R rewrite R = refl
  ∥∥par-sym p q (ceval etrap ∷ C)        | R rewrite R = refl
  ∥∥par-sym p q (csignl _ ∷ C)           | R rewrite R = refl
  ∥∥par-sym p q (cpresent₁ _ _ ∷ C)      | R rewrite R = refl
  ∥∥par-sym p q (cpresent₂ _ _ ∷ C)      | R rewrite R = refl
  ∥∥par-sym p q (cloop ∷ C)              | R rewrite R = refl
  ∥∥par-sym p q (cloopˢ₂ _ ∷ C)          | R rewrite R = refl
  ∥∥par-sym p q (cseq₂ _ ∷ C)            | R rewrite R = refl
  ∥∥par-sym p q (cshared _ _ ∷ C)        | R rewrite R = refl
  ∥∥par-sym p q (cvar _ _ ∷ C)           | R rewrite R = refl
  ∥∥par-sym p q (cif₁ _ _ ∷ C)           | R rewrite R = refl
  ∥∥par-sym p q (cif₂ _ _ ∷ C)           | R rewrite R = refl
  ∥∥par-sym p q (cenv _ _ ∷ C)             | R rewrite R = refl

∥R*-preserves-∥∥s : ∀ {p q} -> p ∥R* q -> ∥ q ∥s ≡ ∥ p ∥s
∥R*-preserves-∥∥s ∥R0 = refl
∥R*-preserves-∥∥s (∥Rn p∥Rq p∥R*q) with ∥R*-preserves-∥∥s p∥R*q
... | x rewrite ∥R-preserves-∥∥s p∥Rq = x

module LexicographicLE {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
                       (RelA : Rel A ℓ₁)
                       (RelB : Rel B ℓ₂) where

  open import Level
  open import Relation.Binary
  open import Induction.WellFounded
  open import Data.Product
  open import Function
  open import Induction
  open import Relation.Unary

  data _<_ : Rel (Σ A \ _ → B) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    left  : ∀ {x₁ y₁ x₂ y₂} (x₁<x₂ : RelA x₁ x₂) → (x₁ , y₁) < (x₂ , y₂)
    right : ∀ {x₁ y₁ x₂ y₂} (y₁<y₂ : RelB y₁ y₂) → (x₁ ≡ x₂ ⊎ RelA x₁ x₂) →
            (x₁  , y₁) < (x₂  , y₂)

  mutual

    accessibleLE : ∀ {x y} →
                    Acc RelA x → WellFounded RelB →
                    Acc _<_ (x , y)
    accessibleLE accA wfB = acc (accessibleLE′ accA (wfB _) wfB)

    accessibleLE′ :
      ∀ {x y} →
      Acc RelA x → Acc RelB y →  WellFounded RelB →
      WfRec _<_ (Acc _<_) (x , y)
    accessibleLE′ (acc rsA) _    wfB ._ (left  x′<x) = accessibleLE (rsA _ x′<x) wfB
    accessibleLE′ accA (acc rsB) wfB .(_ , _) (right y′<y (inj₁ refl)) =
      acc (accessibleLE′ accA (rsB _ y′<y) wfB)
    accessibleLE′ (acc rsA) (acc rsB) wfB .(_ , _) (right y′<y (inj₂ x′<x)) =
      acc (accessibleLE′ (rsA _ x′<x) (rsB _ y′<y) wfB)

  wellFounded : WellFounded RelA → WellFounded RelB →
                 WellFounded _<_
  wellFounded wfA wfB p = accessibleLE (wfA (proj₁ p)) wfB

module _ where
  open LexicographicLE _<′_ _<′_ public
    renaming (_<_ to _<<′_;
              wellFounded to <<′-wellFounded;
              left to <<′-left;
              right to <<′-right)

module _ {ℓ} where
  open Induction.WellFounded.All
       (<<′-wellFounded Induction.Nat.<′-wellFounded Induction.Nat.<′-wellFounded) ℓ public
    renaming (wfRec-builder to <<′-rec-builder;
              wfRec to <<′-rec)

{-
  proof from _On the Power of Simple Diagrams_
  by Roberto Di Cosmo, RTA 1996 (lemma 7)
-}
∥R*-sn⟶*-commute : CB-COMMUTE _∥R*_ _sn⟶*_
∥R*-sn⟶*-commute = thm where
  redlen : ∀ {p q} -> p ∥R* q -> ℕ
  redlen ∥R0 = zero
  redlen (∥Rn p∥Rq p∥R*q) = suc (redlen p∥R*q)

  sharedtype : (ℕ × ℕ) -> Set
  sharedtype (sizeb , distab) =
     ∀ {a b c BV FV} ->
      CorrectBinding a BV FV ->
      (a∥R*b : a ∥R* b) ->
      a sn⟶* c ->
      redlen a∥R*b ≡ distab ->
      ∥ b ∥s ≡ sizeb ->
      ∃ \ {d -> b sn⟶* d × c ∥R* d}

  {- this proof is not working the way that
     Di Cosmo intended; it uses properties
     about ∥R* reduction directly -}
  composing-the-diagram-in-the-hypothesis-down :
    ∀ {p1 p2 p3 q1 q3} ->
    p1 sn⟶ p2 ->
    p2 sn⟶* p3 ->
    p1 ∥R* q1 ->
    p3 ∥R* q3 ->
    (∥ q3 ∥s) <′ (∥ q1 ∥s)
  composing-the-diagram-in-the-hypothesis-down = thm where

    thm-no-∥R* : ∀ {p1 p2 p3} ->
     p1 sn⟶ p2 ->
     p2 sn⟶* p3 ->
     ∥ p3 ∥s <′ ∥ p1 ∥s
    thm-no-∥R* p1sn⟶p2 rrefl = noetherian p1sn⟶p2
    thm-no-∥R* {p1}{p2}{p3} p1sn⟶p2 (rstep{q = r} p2sn⟶r rsn⟶*p3)
      with thm-no-∥R* p2sn⟶r rsn⟶*p3
    ... | ∥p3∥s<′∥p2∥s =
        ≤′-trans {y = ∥ p2 ∥s}
                 ∥p3∥s<′∥p2∥s
                 (suc≤′⇒≤′ ∥ p2 ∥s ∥ p1 ∥s (noetherian p1sn⟶p2))

    thm : ∀ {p1 p2 p3 q1 q3} ->
     p1 sn⟶ p2 ->
     p2 sn⟶* p3 ->
     p1 ∥R* q1 ->
     p3 ∥R* q3 ->
     (∥ q3 ∥s) <′ (∥ q1 ∥s)
    thm p1sn⟶p2 p2sn⟶*p3 p1∥R*q1 p3∥R*q3
      rewrite ∥R*-preserves-∥∥s p1∥R*q1
            | ∥R*-preserves-∥∥s p3∥R*q3 =
            thm-no-∥R* p1sn⟶p2 p2sn⟶*p3

  step : ∀ nm ->
          (∀ (nm′ : ℕ × ℕ) -> nm′ <<′ nm -> sharedtype nm′) ->
          sharedtype nm
  step (sizeb , distab) rec  CBa ∥R0 asn⟶*c redlena∥R*b≡distab ∥b∥s≡sizeb = _ , asn⟶*c , ∥R0
  step (sizeb , distab) rec CBa a∥R*b rrefl redlena∥R*b≡distab ∥b∥s≡sizeb = _ , rrefl , a∥R*b
  step (sizeb , distab) rec {a} {b} {c} CBa
       (∥Rn{q = a″} a∥Ra″ a″∥R*b)
       (rstep{q = a′} asn⟶a′ a′sn⟶*c)
       redlena∥R*b≡distab
       ∥b∥s≡sizeb rewrite sym redlena∥R*b≡distab
    with sn⟶-maintains-binding CBa asn⟶a′
  ... | (_ , CBa′ , _)
    with DPG a∥Ra″ asn⟶a′
  ... | (a‴ , gap) , a″sn⟶gap ,  gapsn⟶*a‴ , a′∥R*a‴
    with rec (sizeb , redlen a″∥R*b) (<<′-right (s≤′s ≤′-refl) (inj₁ refl))
             (∥R-maintains-binding CBa a∥Ra″)
             a″∥R*b  (rstep a″sn⟶gap gapsn⟶*a‴) refl ∥b∥s≡sizeb
  ... | (b′ , bsn⟶*b′ , a‴∥R*b′) rewrite sym ∥b∥s≡sizeb
    with composing-the-diagram-in-the-hypothesis-down a″sn⟶gap gapsn⟶*a‴ a″∥R*b a‴∥R*b′
  ... | ∥b′∥s<′∥b∥s
    with rec (∥ b′ ∥s , redlen (∥R*-concat a′∥R*a‴ a‴∥R*b′))
             (<<′-left ∥b′∥s<′∥b∥s)
             CBa′ (∥R*-concat a′∥R*a‴ a‴∥R*b′) a′sn⟶*c refl refl
  ... | ( d , b′sn⟶*d , c∥R*d) =  d , sn⟶*+ bsn⟶*b′ b′sn⟶*d , c∥R*d

  lemma7-commutation : ∀ (nm : ℕ × ℕ) -> sharedtype nm
  lemma7-commutation = <<′-rec _ step

  thm : CB-COMMUTE _∥R*_ _sn⟶*_
  thm {p}{q}{r} CBp p∥R*q psn⟶*r =
   lemma7-commutation (∥ q ∥s , redlen p∥R*q) CBp p∥R*q psn⟶*r refl refl

∥R*∪sn⟶*-confluent : CB-CONFLUENT _∥R*∪sn⟶*_
∥R*∪sn⟶*-confluent =
  \ { CBp p∥R*∪sn⟶*q p∥R*∪sn⟶*r ->
      hindley-rosen
       (redlen p∥R*∪sn⟶*q , redlen p∥R*∪sn⟶*r)
       CBp p∥R*∪sn⟶*q p∥R*∪sn⟶*r refl refl} where

  redlen : ∀ {p q} -> p ∥R*∪sn⟶* q -> ℕ
  redlen (∪∥R* _ r) = suc (redlen r)
  redlen (∪sn⟶* _ r) = suc (redlen r)
  redlen ∪refl = zero

  sharedtype : ℕ × ℕ -> Set
  sharedtype (n , m) = ∀ {p q r BV FV} ->
    CorrectBinding p BV FV ->
    (p∥R*∪sn⟶*q : p ∥R*∪sn⟶* q) ->
    (p∥R*∪sn⟶*r : p ∥R*∪sn⟶* r) ->
    n ≡ redlen p∥R*∪sn⟶*q ->
    m ≡ redlen p∥R*∪sn⟶*r ->
    ∃ λ {z → (q ∥R*∪sn⟶* z × r ∥R*∪sn⟶* z)}

  length-lemma : ∀ {a b}  (l : a ∥R*∪sn⟶* b) ->
      suc zero ≡ suc (redlen l) ⊎
      suc zero <′ suc (redlen l)
  length-lemma (∪∥R* p∥R*q l) = inj₂ (s≤′s (s≤′s z≤′n))
  length-lemma (∪sn⟶* psn⟶*q l) = inj₂ (s≤′s (s≤′s z≤′n))
  length-lemma ∪refl = inj₁ refl

  step : ∀ nm ->
          (∀ (nm′ : ℕ × ℕ) -> nm′ <<′ nm -> sharedtype nm′) ->
          sharedtype nm
  step (n , m) rec CBp (∪∥R* p∥R*q a) ∪refl n≡ m≡ = _ , ∪refl , ∪∥R* p∥R*q a
  step (n , m) rec CBp (∪sn⟶* psn⟶*q a) ∪refl n≡ m≡ =   _ , ∪refl , ∪sn⟶* psn⟶*q a
  step (n , m) rec CBp ∪refl (∪∥R* p∥R*q b) n≡ m≡ = _ , ∪∥R* p∥R*q b , ∪refl
  step (n , m) rec CBp ∪refl (∪sn⟶* psn⟶*q b) n≡ m≡ = _ , ∪sn⟶* psn⟶*q b , ∪refl
  step (n , m) rec CBp ∪refl ∪refl n≡ m≡ = _ , ∪refl , ∪refl

  step(n , m) rec {p}{q}{r} CBp
      (∪∥R* {_}{q₁} p∥R*q₁ q₁∥R*∪sn⟶*q)
      (∪∥R* {_}{r₁} p∥R*r₁ r₁∥R*∪sn⟶*r)
     n≡ m≡  rewrite n≡ | m≡
    with BVFVcorrect _ _ _ CBp
  ... | refl , refl
    with ∥R*-maintains-binding CBp p∥R*q₁
  ... | CBq₁
    with  BVFVcorrect _ _ _ CBq₁
  ... | refl , refl
    with ∥R*-maintains-binding CBp p∥R*r₁
  ... | CBr₁
    with  BVFVcorrect _ _ _ CBr₁
  ... | refl , refl
    with ∥R*-confluent CBp p∥R*q₁ p∥R*r₁
  ... | q₁r₁ , q₁∥R*q₁r₁ , r₁∥R*q₁r₁
    with rec (suc zero , redlen r₁∥R*∪sn⟶*r)
             (<<′-right ≤′-refl (length-lemma q₁∥R*∪sn⟶*q))
             CBr₁ (∪∥R* r₁∥R*q₁r₁ ∪refl) r₁∥R*∪sn⟶*r
             refl refl
  ... | q₁r₁r , q₁r₁∥R*∪sn⟶*q₁r₁r , r∥R*∪sn⟶*q₁r₁r
    with rec (redlen q₁∥R*∪sn⟶*q , suc (redlen q₁r₁∥R*∪sn⟶*q₁r₁r))
             (<<′-left ≤′-refl)
             CBq₁ q₁∥R*∪sn⟶*q (∪∥R* q₁∥R*q₁r₁ q₁r₁∥R*∪sn⟶*q₁r₁r)
             refl refl
  ... | qq₁r₁r , q∥R*∪sn⟶*qq₁r₁r , q₁r₁r∥R*∪sn⟶*qq₁r₁r
    = qq₁r₁r , q∥R*∪sn⟶*qq₁r₁r , ∥R*∪sn⟶*-concat r∥R*∪sn⟶*q₁r₁r q₁r₁r∥R*∪sn⟶*qq₁r₁r

  step (n , m) rec {p}{q}{r} CBp
    (∪∥R*{_}{q₁} p∥R*q₁ q₁∥R*∪sn⟶*q)
    (∪sn⟶*{_}{r₁} psn⟶*r₁  r₁∥R*∪sn⟶*r)
    n≡ m≡ rewrite n≡ | m≡
    with BVFVcorrect _ _ _ CBp
  ... | refl , refl
    with ∥R*-maintains-binding CBp p∥R*q₁
  ... | CBq₁
    with  BVFVcorrect _ _ _ CBq₁
  ... | refl , refl
    with sn⟶*-maintains-binding CBp psn⟶*r₁
  ... | (BVr₁ , FVr₁) , CBr₁
    with ∥R*-sn⟶*-commute CBp p∥R*q₁ psn⟶*r₁
  ... | q₁r₁ , q₁sn⟶*q₁r₁ , r₁∥R*q₁r₁
    with rec (suc zero , redlen r₁∥R*∪sn⟶*r)
             (<<′-right ≤′-refl (length-lemma q₁∥R*∪sn⟶*q))
             CBr₁ (∪∥R* r₁∥R*q₁r₁ ∪refl) r₁∥R*∪sn⟶*r
             refl refl
  ... | q₁r₁r , q₁r₁∥R*∪sn⟶*q₁r₁r , r∥R*∪sn⟶*q₁r₁r
     with rec (redlen q₁∥R*∪sn⟶*q , suc (redlen q₁r₁∥R*∪sn⟶*q₁r₁r))
             (<<′-left ≤′-refl)
             CBq₁ q₁∥R*∪sn⟶*q (∪sn⟶*  q₁sn⟶*q₁r₁  q₁r₁∥R*∪sn⟶*q₁r₁r)
             refl refl
  ... | qq₁r₁r , q∥R*∪sn⟶*qq₁r₁r , q₁r₁r∥R*∪sn⟶*qq₁r₁r
    =  qq₁r₁r , q∥R*∪sn⟶*qq₁r₁r , ∥R*∪sn⟶*-concat r∥R*∪sn⟶*q₁r₁r q₁r₁r∥R*∪sn⟶*qq₁r₁r

  step (n , m) rec {p}{q}{r} CBp
    (∪sn⟶*{_}{q₁} psn⟶*q₁ q₁∥R*∪sn⟶*q)
    (∪∥R*{_}{r₁} p∥R*r₁  r₁∥R*∪sn⟶*r)
    n≡ m≡ rewrite n≡ | m≡
    with BVFVcorrect _ _ _ CBp
  ... | refl , refl
    with sn⟶*-maintains-binding CBp psn⟶*q₁
  ... | (BVq₁ , FVq₁) , CBq₁
    with ∥R*-maintains-binding CBp p∥R*r₁
  ... | CBr₁
    with  BVFVcorrect _ _ _ CBr₁
  ... | refl , refl
    with ∥R*-sn⟶*-commute CBp p∥R*r₁ psn⟶*q₁
  ... | r₁q₁ , r₁sn⟶*r₁q₁ , q₁∥R*r₁q₁
    with rec (suc zero , redlen r₁∥R*∪sn⟶*r)
             (<<′-right ≤′-refl (length-lemma q₁∥R*∪sn⟶*q))
             CBr₁ (∪sn⟶* r₁sn⟶*r₁q₁ ∪refl) r₁∥R*∪sn⟶*r
             refl refl
  ... | r₁q₁r , r₁q₁∥R*∪sn⟶*r₁q₁r , r∥R*∪sn⟶*r₁q₁r
     with rec (redlen q₁∥R*∪sn⟶*q , suc (redlen r₁q₁∥R*∪sn⟶*r₁q₁r))
             (<<′-left ≤′-refl)
             CBq₁ q₁∥R*∪sn⟶*q (∪∥R*  q₁∥R*r₁q₁  r₁q₁∥R*∪sn⟶*r₁q₁r)
             refl refl
  ... | qq₁r₁r , q∥R*∪sn⟶*qq₁r₁r , q₁r₁r∥R*∪sn⟶*qq₁r₁r
    =  qq₁r₁r , q∥R*∪sn⟶*qq₁r₁r , ∥R*∪sn⟶*-concat r∥R*∪sn⟶*r₁q₁r q₁r₁r∥R*∪sn⟶*qq₁r₁r

  step (n , m) rec {p}{q}{r} CBp
    (∪sn⟶*{_}{q₁} psn⟶*q₁  q₁∥R*∪sn⟶*q)
    (∪sn⟶*{_}{r₁} psn⟶*r₁ r₁∥R*∪sn⟶*r)
    n≡ m≡ rewrite n≡ | m≡
    with BVFVcorrect _ _ _ CBp
  ... | refl , refl
    with sn⟶*-maintains-binding CBp psn⟶*q₁
  ... | (BVq₁ , FVq₁) , CBq₁
    with sn⟶*-maintains-binding CBp psn⟶*r₁
  ... | (BVr₁ , FVr₁) , CBr₁
    with sn⟶*-confluent CBp psn⟶*q₁ psn⟶*r₁
  ... | q₁r₁ , q₁sn⟶*q₁r₁ , r₁sn⟶*q₁r₁
    with rec (suc zero , redlen r₁∥R*∪sn⟶*r)
             (<<′-right ≤′-refl (length-lemma q₁∥R*∪sn⟶*q))
             CBr₁ (∪sn⟶* r₁sn⟶*q₁r₁ ∪refl) r₁∥R*∪sn⟶*r
             refl refl
  ... | q₁r₁r , q₁r₁∥R*∪sn⟶*q₁r₁r , r∥R*∪sn⟶*q₁r₁r
    with rec (redlen q₁∥R*∪sn⟶*q , suc (redlen q₁r₁∥R*∪sn⟶*q₁r₁r))
             (<<′-left ≤′-refl)
             CBq₁ q₁∥R*∪sn⟶*q (∪sn⟶* q₁sn⟶*q₁r₁ q₁r₁∥R*∪sn⟶*q₁r₁r)
             refl refl
  ... | qq₁r₁r , q∥R*∪sn⟶*qq₁r₁r , q₁r₁r∥R*∪sn⟶*qq₁r₁r
    = qq₁r₁r , q∥R*∪sn⟶*qq₁r₁r , ∥R*∪sn⟶*-concat r∥R*∪sn⟶*q₁r₁r q₁r₁r∥R*∪sn⟶*qq₁r₁r

  hindley-rosen : ∀ (nm : ℕ × ℕ) -> sharedtype nm
  hindley-rosen = <<′-rec _ step

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


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

module Definition.Conversion.EqRelInstance where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening using (_∷_⊆_; wkEq)
open import Definition.Conversion
open import Definition.Conversion.Reduction
open import Definition.Conversion.Universe
open import Definition.Conversion.Stability
open import Definition.Conversion.Soundness
open import Definition.Conversion.Lift
open import Definition.Conversion.Conversion
open import Definition.Conversion.Symmetry
open import Definition.Conversion.Transitivity
open import Definition.Conversion.Weakening
open import Definition.Typed.EqualityRelation
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.Reduction
open import Definition.Typed.Consequences.Inversion

open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Function

-- Algorithmic equality of neutrals with injected conversion.
record _⊢_~_∷_ (Γ : Con Term) (k l A : Term) : Set where
  inductive
  constructor ↑
  field
    {B} : Term
    A≡B : Γ ⊢ A ≡ B
    k~↑l : Γ ⊢ k ~ l ↑ B

-- Properties of algorithmic equality of neutrals with injected conversion.

~-var : ∀ {x A Γ} → Γ ⊢ var x ∷ A → Γ ⊢ var x ~ var x ∷ A
~-var x =
  let ⊢A = syntacticTerm x
  in  ↑ (refl ⊢A) (var-refl x PE.refl)

~-app : ∀ {f g a b F G Γ}
      → Γ ⊢ f ~ g ∷ Π F ▹ G
      → Γ ⊢ a [conv↑] b ∷ F
      → Γ ⊢ f ∘ a ~ g ∘ b ∷ G [ a ]
~-app (↑ A≡B x) x₁ =
  let _ , ⊢B = syntacticEq A≡B
      B′ , whnfB′ , D = whNorm ⊢B
      ΠFG≡B′ = trans A≡B (subset* (red D))
      H , E , B≡ΠHE = Π≡A ΠFG≡B′ whnfB′
      F≡H , G≡E = injectivity (PE.subst (λ x → _ ⊢ _ ≡ x) B≡ΠHE ΠFG≡B′)
      _ , ⊢f , _ = syntacticEqTerm (soundnessConv↑Term x₁)
  in  ↑ (substTypeEq G≡E (refl ⊢f))
        (app-cong (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x)
                            B≡ΠHE
                            ([~] _ (red D) whnfB′ x))
             (convConvTerm x₁ F≡H))

~-fst : ∀ {Γ p r F G}
      → Γ ⊢ p ~ r ∷ Σ F ▹ G
      → Γ ⊢ fst p ~ fst r ∷ F
~-fst (↑ A≡B p~r) =
  let _ , ⊢B = syntacticEq A≡B
      B′ , whnfB′ , D = whNorm ⊢B
      ΣFG≡B′ = trans A≡B (subset* (red D))
      H , E , B≡ΣHE = Σ≡A ΣFG≡B′ whnfB′
      F≡H , G≡E = Σ-injectivity (PE.subst (λ x → _ ⊢ _ ≡ x) B≡ΣHE ΣFG≡B′)
      p~r↓ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x)
                      B≡ΣHE
                      ([~] _ (red D) whnfB′ p~r)
  in  ↑ F≡H (fst-cong p~r↓)

~-snd : ∀ {Γ p r F G}
      → Γ ⊢ p ~ r ∷ Σ F ▹ G
      → Γ ⊢ snd p ~ snd r ∷ G [ fst p ]
~-snd (↑ A≡B p~r) =
  let ⊢ΣFG , ⊢B = syntacticEq A≡B
      B′ , whnfB′ , D = whNorm ⊢B
      ΣFG≡B′ = trans A≡B (subset* (red D))
      H , E , B≡ΣHE = Σ≡A ΣFG≡B′ whnfB′
      F≡H , G≡E = Σ-injectivity (PE.subst (λ x → _ ⊢ _ ≡ x) B≡ΣHE ΣFG≡B′)
      p~r↓ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x)
                      B≡ΣHE
                      ([~] _ (red D) whnfB′ p~r)
      ⊢F , ⊢G = syntacticΣ ⊢ΣFG
      _ , ⊢p , _ = syntacticEqTerm (soundness~↑ p~r)
      ⊢fst = fstⱼ ⊢F ⊢G (conv ⊢p (sym A≡B))
  in  ↑ (substTypeEq G≡E (refl ⊢fst)) (snd-cong p~r↓)

~-natrec : ∀ {z z′ s s′ n n′ F F′ Γ}
         → (Γ ∙ ℕ) ⊢ F [conv↑] F′ →
      Γ ⊢ z [conv↑] z′ ∷ (F [ zero ]) →
      Γ ⊢ s [conv↑] s′ ∷ (Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)) →
      Γ ⊢ n ~ n′ ∷ ℕ →
      Γ ⊢ natrec F z s n ~ natrec F′ z′ s′ n′ ∷ (F [ n ])
~-natrec x x₁ x₂ (↑ A≡B x₄) =
  let _ , ⊢B = syntacticEq A≡B
      B′ , whnfB′ , D = whNorm ⊢B
      ℕ≡B′ = trans A≡B (subset* (red D))
      B≡ℕ = ℕ≡A ℕ≡B′ whnfB′
      k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡ℕ
                      ([~] _ (red D) whnfB′ x₄)
      ⊢F , _ = syntacticEq (soundnessConv↑ x)
      _ , ⊢n , _ = syntacticEqTerm (soundness~↓ k~l′)
  in  ↑ (refl (substType ⊢F ⊢n))
        (natrec-cong x x₁ x₂ k~l′)

~-Emptyrec : ∀ {n n′ F F′ Γ}
         → Γ ⊢ F [conv↑] F′ →
      Γ ⊢ n ~ n′ ∷ Empty →
      Γ ⊢ Emptyrec F n ~ Emptyrec F′ n′ ∷ F
~-Emptyrec x (↑ A≡B x₄) =
  let _ , ⊢B = syntacticEq A≡B
      B′ , whnfB′ , D = whNorm ⊢B
      Empty≡B′ = trans A≡B (subset* (red D))
      B≡Empty = Empty≡A Empty≡B′ whnfB′
      k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡Empty
                      ([~] _ (red D) whnfB′ x₄)
      ⊢F , _ = syntacticEq (soundnessConv↑ x)
      _ , ⊢n , _ = syntacticEqTerm (soundness~↓ k~l′)
  in  ↑ (refl ⊢F)
        (Emptyrec-cong x k~l′)

~-sym : {k l A : Term} {Γ : Con Term} → Γ ⊢ k ~ l ∷ A → Γ ⊢ l ~ k ∷ A
~-sym (↑ A≡B x) =
  let ⊢Γ = wfEq A≡B
      B , A≡B′ , l~k = sym~↑ (reflConEq ⊢Γ) x
  in  ↑ (trans A≡B A≡B′) l~k

~-trans : {k l m A : Term} {Γ : Con Term}
        → Γ ⊢ k ~ l ∷ A → Γ ⊢ l ~ m ∷ A
        → Γ ⊢ k ~ m ∷ A
~-trans (↑ x x₁) (↑ x₂ x₃) =
  let ⊢Γ = wfEq x
      k~m , _ = trans~↑ x₁ x₃
  in  ↑ x k~m

~-wk : {k l A : Term} {ρ : Wk} {Γ Δ : Con Term} →
      ρ ∷ Δ ⊆ Γ →
      ⊢ Δ → Γ ⊢ k ~ l ∷ A → Δ ⊢ wk ρ k ~ wk ρ l ∷ wk ρ A
~-wk x x₁ (↑ x₂ x₃) = ↑ (wkEq x x₁ x₂) (wk~↑ x x₁ x₃)

~-conv : {k l A B : Term} {Γ : Con Term} →
      Γ ⊢ k ~ l ∷ A → Γ ⊢ A ≡ B → Γ ⊢ k ~ l ∷ B
~-conv (↑ x x₁) x₂ = ↑ (trans (sym x₂) x) x₁

~-to-conv : {k l A : Term} {Γ : Con Term} →
      Γ ⊢ k ~ l ∷ A → Γ ⊢ k [conv↑] l ∷ A
~-to-conv (↑ x x₁) = convConvTerm (lift~toConv↑ x₁) (sym x)

-- Algorithmic equality instance of the generic equality relation.
instance eqRelInstance : EqRelSet
eqRelInstance = record {
  _⊢_≅_ = _⊢_[conv↑]_;
  _⊢_≅_∷_ = _⊢_[conv↑]_∷_;
  _⊢_~_∷_ = _⊢_~_∷_;
  ~-to-≅ₜ = ~-to-conv;
  ≅-eq = soundnessConv↑;
  ≅ₜ-eq = soundnessConv↑Term;
  ≅-univ = univConv↑;
  ≅-sym = symConv;
  ≅ₜ-sym = symConvTerm;
  ~-sym = ~-sym;
  ≅-trans = transConv;
  ≅ₜ-trans = transConvTerm;
  ~-trans = ~-trans;
  ≅-conv = convConvTerm;
  ~-conv = ~-conv;
  ≅-wk = wkConv↑;
  ≅ₜ-wk = wkConv↑Term;
  ~-wk = ~-wk;
  ≅-red = λ x x₁ x₂ x₃ x₄ → reductionConv↑ x x₁ x₄;
  ≅ₜ-red = λ x x₁ x₂ x₃ x₄ x₅ x₆ → reductionConv↑Term x x₁ x₂ x₆;
  ≅-Urefl = liftConv ∘ᶠ U-refl;
  ≅-ℕrefl = liftConv ∘ᶠ ℕ-refl;
  ≅ₜ-ℕrefl = λ x → liftConvTerm (univ (ℕⱼ x) (ℕⱼ x) (ℕ-refl x));
  ≅-Emptyrefl = liftConv ∘ᶠ Empty-refl;
  ≅ₜ-Emptyrefl = λ x → liftConvTerm (univ (Emptyⱼ x) (Emptyⱼ x) (Empty-refl x));
  ≅-Unitrefl = liftConv ∘ᶠ Unit-refl;
  ≅ₜ-Unitrefl = λ ⊢Γ → liftConvTerm (univ (Unitⱼ ⊢Γ) (Unitⱼ ⊢Γ) (Unit-refl ⊢Γ));
  ≅ₜ-η-unit = λ [e] [e'] → let u , uWhnf , uRed = whNormTerm [e]
                               u' , u'Whnf , u'Red = whNormTerm [e']
                               [u] = ⊢u-redₜ uRed
                               [u'] = ⊢u-redₜ u'Red
                           in  [↑]ₜ Unit u u'
                               (red (idRed:*: (syntacticTerm [e])))
                               (redₜ uRed)
                               (redₜ u'Red)
                               Unitₙ uWhnf u'Whnf
                               (η-unit [u] [u'] uWhnf u'Whnf);
  ≅-Π-cong = λ x x₁ x₂ → liftConv (Π-cong x x₁ x₂);
  ≅ₜ-Π-cong = λ x x₁ x₂ → let _ , F∷U , H∷U = syntacticEqTerm (soundnessConv↑Term x₁)
                              _ , G∷U , E∷U = syntacticEqTerm (soundnessConv↑Term x₂)
                              ⊢Γ = wfTerm F∷U
                              F<>H = univConv↑ x₁
                              G<>E = univConv↑ x₂
                              F≡H = soundnessConv↑ F<>H
                              E∷U′ = stabilityTerm (reflConEq ⊢Γ ∙ F≡H) E∷U
                          in  liftConvTerm (univ (Πⱼ F∷U ▹ G∷U) (Πⱼ H∷U ▹ E∷U′)
                                                (Π-cong x F<>H G<>E));
  ≅-Σ-cong = λ x x₁ x₂ → liftConv (Σ-cong x x₁ x₂);
  ≅ₜ-Σ-cong = λ x x₁ x₂ → let _ , F∷U , H∷U = syntacticEqTerm (soundnessConv↑Term x₁)
                              _ , G∷U , E∷U = syntacticEqTerm (soundnessConv↑Term x₂)
                              ⊢Γ = wfTerm F∷U
                              F<>H = univConv↑ x₁
                              G<>E = univConv↑ x₂
                              F≡H = soundnessConv↑ F<>H
                              E∷U′ = stabilityTerm (reflConEq ⊢Γ ∙ F≡H) E∷U
                          in  liftConvTerm (univ (Σⱼ F∷U ▹ G∷U) (Σⱼ H∷U ▹ E∷U′)
                                                (Σ-cong x F<>H G<>E));
  ≅ₜ-zerorefl = liftConvTerm ∘ᶠ zero-refl;
  ≅-suc-cong = liftConvTerm ∘ᶠ suc-cong;
  ≅-η-eq = λ x x₁ x₂ x₃ x₄ x₅ → liftConvTerm (η-eq x₁ x₂ x₃ x₄ x₅);
  ≅-Σ-η = λ x x₁ x₂ x₃ x₄ x₅ x₆ x₇ → (liftConvTerm (Σ-η x₂ x₃ x₄ x₅ x₆ x₇));
  ~-var = ~-var;
  ~-app = ~-app;
  ~-fst = λ x x₁ x₂ → ~-fst x₂;
  ~-snd = λ x x₁ x₂ → ~-snd x₂;
  ~-natrec = ~-natrec;
  ~-Emptyrec = ~-Emptyrec }


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.DistLatticeSheaf where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Powerset
open import Cubical.Data.Sigma

open import Cubical.Relation.Binary.Poset

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.DistLattice.Basis

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Limits.Pullback
open import Cubical.Categories.Limits.Terminal
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Instances.CommRings
open import Cubical.Categories.Instances.Poset
open import Cubical.Categories.Instances.Semilattice
open import Cubical.Categories.Instances.Lattice
open import Cubical.Categories.Instances.DistLattice

private
  variable
    ℓ ℓ' ℓ'' : Level

module _ (L : DistLattice ℓ) (C : Category ℓ' ℓ'') (T : Terminal C) where
  open Category hiding (_⋆_)
  open Functor
  open Order (DistLattice→Lattice L)
  open DistLatticeStr (snd L)
  open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L))
  open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice L))
      using (∧≤RCancel ; ∧≤LCancel)
  open PosetStr (IndPoset .snd) hiding (_≤_)

  𝟙 : ob C
  𝟙 = terminalOb C T

  DLCat : Category ℓ ℓ
  DLCat = DistLatticeCategory L

  open Category DLCat

  -- C-valued presheaves on a distributive lattice
  DLPreSheaf : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
  DLPreSheaf = Functor (DLCat ^op) C

  hom-∨₁ : (x y : L .fst) → DLCat [ x , x ∨l y ]
  hom-∨₁ = ∨≤RCancel
    -- TODO: isn't the fixity of the operators a bit weird?

  hom-∨₂ : (x y : L .fst) → DLCat [ y , x ∨l y ]
  hom-∨₂ = ∨≤LCancel

  hom-∧₁ : (x y : L .fst) → DLCat [ x ∧l y , x ]
  hom-∧₁ _ _ = (≤m→≤j _ _ (∧≤RCancel _ _))

  hom-∧₂ : (x y : L .fst) → DLCat [ x ∧l y , y ]
  hom-∧₂ _ _ = (≤m→≤j _ _ (∧≤LCancel _ _))

  {-
     x ∧ y ----→   y
       |           |
       |    sq     |
       V           V
       x   ----→ x ∨ y
  -}
  sq : (x y : L .fst) → hom-∧₂ x y ⋆ hom-∨₂ x y ≡ hom-∧₁ x y ⋆ hom-∨₁ x y
  sq x y = is-prop-valued (x ∧l y) (x ∨l y) (hom-∧₂ x y ⋆ hom-∨₂ x y) (hom-∧₁ x y ⋆ hom-∨₁ x y)

  {-
    F(x ∨ y) ----→ F(y)
       |            |
       |     Fsq    |
       V            V
      F(x) ------→ F(x ∧ y)
  -}
  Fsq : (F : DLPreSheaf) (x y : L .fst)
      → F .F-hom (hom-∨₂ x y) ⋆⟨ C ⟩ F .F-hom (hom-∧₂ x y) ≡
        F .F-hom (hom-∨₁ x y) ⋆⟨ C ⟩ F .F-hom (hom-∧₁ x y)
  Fsq F x y = sym (F-seq F (hom-∨₂ x y) (hom-∧₂ x y))
           ∙∙ cong (F .F-hom) (sq x y)
           ∙∙ F-seq F (hom-∨₁ x y) (hom-∧₁ x y)

  isDLSheaf : (F : DLPreSheaf) → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
  isDLSheaf F = (F-ob F 0l ≡ 𝟙)
              × ((x y : L .fst) → isPullback C _ _ _ (Fsq F x y))

  -- TODO: might be better to define this as a record
  DLSheaf : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
  DLSheaf = Σ[ F ∈ DLPreSheaf ] isDLSheaf F

module Lemma1 (L : DistLattice ℓ) (C : Category ℓ' ℓ'') (T : Terminal C) (L' : ℙ (fst L)) (hB : IsBasis L L') where

  open Category hiding (_⋆_)
  open Functor
  open DistLatticeStr (snd L)
  open IsBasis hB

  isDLBasisSheaf : (F : DLPreSheaf L C T) → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
  isDLBasisSheaf F = (F-ob F 0l ≡ 𝟙 L C T)
                   × ((x y : L .fst) → x ∈ L' → y ∈ L' → isPullback C _ _ _ (Fsq L C T F x y))

  DLBasisSheaf : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
  DLBasisSheaf = Σ[ F ∈ DLPreSheaf L C T ] isDLBasisSheaf F

  -- To prove the statement we probably need that C is:
  -- 1. univalent
  -- 2. has finite limits (or pullbacks and a terminal object)
  -- 3. isGroupoid (C .ob)
  -- The last point is not strictly necessary, but we have to have some
  -- control over the hLevel as we want to write F(x) in terms of its
  -- basis cover which is information hidden under a prop truncation...
  -- Alternatively we just prove the statement for C = CommRingsCategory

  -- TODO: is unique existence expressed like this what we want?
  -- statement : (F' : DLBasisSheaf)
  --           → ∃![ F ∈ DLSheaf L C T ] ((x : fst L) → (x ∈ L') → CatIso C (F-ob (fst F) x) (F-ob (fst F') x)) -- TODO: if C is univalent the CatIso could be ≡?
  -- statement (F' , h1 , hPb) = ?

  -- It might be easier to prove all of these if we use the definition
  -- in terms of particular limits instead

  -- Scrap zone:

  -- -- Sublattices: upstream later
  -- record isSublattice (L' : ℙ (fst L)) : Type ℓ where
  --   field
  --     1l-closed  : 1l ∈ L'
  --     0l-closed  : 0l ∈ L'
  --     ∧l-closed  : {x y : fst L} → x ∈ L' → y ∈ L' → x ∧l y ∈ L'
  --     ∨l-closed  : {x y : fst L} → x ∈ L' → y ∈ L' → x ∨l y ∈ L'

  -- open isSublattice

  -- Sublattice : Type (ℓ-suc ℓ)
  -- Sublattice = Σ[ L' ∈ ℙ (fst L) ] isSublattice L'

  -- restrictDLSheaf : DLSheaf → Sublattice → DLSheaf
  -- F-ob (fst (restrictDLSheaf F (L' , HL'))) x = {!F-ob (fst F) x!} -- Hmm, not nice...
  -- F-hom (fst (restrictDLSheaf F L')) = {!!}
  -- F-id (fst (restrictDLSheaf F L')) = {!!}
  -- F-seq (fst (restrictDLSheaf F L')) = {!!}
  -- snd (restrictDLSheaf F L') = {!!}


text:
open import Prelude

module Implicits.Resolution.Scala.Type where

open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas.Type
open import Implicits.Substitutions.Type as TS using ()

-- predicate on types to limit them to non-rule types
-- (as those don't exist in Scala currently)

mutual
  data ScalaSimpleType {ν} : SimpleType ν → Set where
    tc   : (c : ℕ) → ScalaSimpleType (tc c)
    tvar : (n : Fin ν) → ScalaSimpleType (tvar n)
    _→'_ : ∀ {a b} → ScalaType a → ScalaType b → ScalaSimpleType (a →' b)

  data ScalaType {ν} : Type ν → Set where
    simpl : ∀ {τ} → ScalaSimpleType {ν} τ → ScalaType (simpl τ)
    ∀'    : ∀ {a} → ScalaType a → ScalaType (∀' a)

data ScalaRule {ν} : Type ν → Set where
  idef  : ∀ {a b} → ScalaType a → ScalaType b → ScalaRule (a ⇒ b)
  ival  : ∀ {a} → ScalaType a → ScalaRule a

ScalaICtx : ∀ {ν} → ICtx ν → Set
ScalaICtx Δ = All ScalaRule Δ

mutual

  weaken-scalastype : ∀ {ν} k {a : SimpleType (k N+ ν)} → ScalaSimpleType a →
                      ScalaType (a TS.simple/ (TS.wk TS.↑⋆ k))
  weaken-scalastype k (tc c) = simpl (tc c)
  weaken-scalastype k (tvar n) = Prelude.subst
    (λ z → ScalaType z)
    (sym $ var-/-wk-↑⋆ k n)
    (simpl (tvar (lift k suc n)))
  weaken-scalastype k (a →' b) = simpl ((weaken-scalatype k a) →' (weaken-scalatype k b))

  weaken-scalatype : ∀ {ν} k {a : Type (k N+ ν)} → ScalaType a → ScalaType (a TS./ TS.wk TS.↑⋆ k)
  weaken-scalatype k (simpl {τ} x) = weaken-scalastype k x
  weaken-scalatype k (∀' p) = ∀' (weaken-scalatype (suc k) p)

weaken-scalarule : ∀ {ν} k {a : Type (k N+ ν)} → ScalaRule a → ScalaRule (a TS./ (TS.wk TS.↑⋆ k))
weaken-scalarule k (idef x y) = idef (weaken-scalatype k x) (weaken-scalatype k y)
weaken-scalarule k (ival x) = ival (weaken-scalatype k x)

weaken-scalaictx : ∀ {ν} {Δ : ICtx ν} → ScalaICtx Δ → ScalaICtx (ictx-weaken Δ)
weaken-scalaictx All.[] = All.[]
weaken-scalaictx (px All.∷ ps) = weaken-scalarule zero px All.∷ weaken-scalaictx ps


text:
{-

This file contains:
  - The inductive family 𝕁 can be constructed by iteratively applying pushouts;
  - The special cases of 𝕁 n for n = 0, 1 and 2;
  - Connectivity of inclusion maps.

  Easy, almost direct consequences of the very definition.

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.James.Inductive.PushoutFormula where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed hiding (pt)

open import Cubical.Data.Nat
open import Cubical.Algebra.NatSolver.Reflection
open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.HITs.Wedge
open import Cubical.HITs.Pushout
open import Cubical.HITs.Pushout.PushoutProduct
open import Cubical.HITs.SequentialColimit
open import Cubical.HITs.James.Inductive.Base
  renaming (𝕁ames to 𝕁amesContruction ; 𝕁ames∞ to 𝕁ames∞Contruction)

open import Cubical.Homotopy.Connected

private
  variable
    ℓ : Level

module _
  (X∙@(X , x₀) : Pointed ℓ) where

  private
    𝕁ames  = 𝕁amesContruction  (X , x₀)
    𝕁ames∞ = 𝕁ames∞Contruction (X , x₀)

  𝕁amesPush : (n : ℕ) → Type ℓ
  𝕁amesPush n = Pushout {A = 𝕁ames n} {B = X × 𝕁ames n} {C = 𝕁ames (1 + n)} (λ xs → x₀ , xs) incl

  X→𝕁ames1 : X → 𝕁ames 1
  X→𝕁ames1 x = x ∷ []

  𝕁ames1→X : 𝕁ames 1 → X
  𝕁ames1→X (x ∷ []) = x
  𝕁ames1→X (incl []) = x₀
  𝕁ames1→X (unit [] i) = x₀

  X→𝕁ames1→X : (x : X) → 𝕁ames1→X (X→𝕁ames1 x) ≡ x
  X→𝕁ames1→X x = refl

  𝕁ames1→X→𝕁ames1 : (xs : 𝕁ames 1) → X→𝕁ames1 (𝕁ames1→X xs) ≡ xs
  𝕁ames1→X→𝕁ames1 (x ∷ []) = refl
  𝕁ames1→X→𝕁ames1 (incl []) i = unit [] (~ i)
  𝕁ames1→X→𝕁ames1 (unit [] i) j = unit [] (i ∨ ~ j)

  leftMap  : {n : ℕ} → 𝕁amesPush n → X × 𝕁ames (1 + n)
  leftMap  (inl (x , xs)) = x , incl xs
  leftMap  (inr ys) = x₀ , ys
  leftMap  (push xs i) = x₀ , incl xs

  rightMap : {n : ℕ} → 𝕁amesPush n → 𝕁ames (1 + n)
  rightMap (inl (x , xs)) = x ∷ xs
  rightMap (inr ys) = ys
  rightMap (push xs i) = unit xs (~ i)

  PushMap : {n : ℕ} → Pushout {A = 𝕁amesPush n} leftMap rightMap → 𝕁ames (2 + n)
  PushMap (inl (x , xs)) = x ∷ xs
  PushMap (inr ys) = incl ys
  PushMap (push (inl (x , xs)) i) = incl∷ x xs (~ i)
  PushMap (push (inr ys) i) = unit ys (~ i)
  PushMap (push (push xs i) j) = coh xs (~ i) (~ j)

  PushInv : {n : ℕ} → 𝕁ames (2 + n) → Pushout {A = 𝕁amesPush n} leftMap rightMap
  PushInv (x ∷ xs) = inl (x , xs)
  PushInv (incl xs) = inr xs
  PushInv (incl∷ x xs i) = push (inl (x , xs)) (~ i)
  PushInv (unit xs i) = push (inr xs) (~ i)
  PushInv (coh xs i j) = push (push xs (~ i)) (~ j)

  PushInvMapInv : {n : ℕ}(xs : 𝕁ames (2 + n)) → PushMap (PushInv xs) ≡ xs
  PushInvMapInv (x ∷ xs) = refl
  PushInvMapInv (incl xs) = refl
  PushInvMapInv (incl∷ x xs i) = refl
  PushInvMapInv (unit xs i) = refl
  PushInvMapInv (coh xs i j) = refl

  PushMapInvMap : {n : ℕ}(xs : Pushout {A = 𝕁amesPush n} leftMap rightMap) → PushInv (PushMap xs) ≡ xs
  PushMapInvMap (inl (x , xs)) = refl
  PushMapInvMap (inr ys) = refl
  PushMapInvMap (push (inl (x , xs)) i) = refl
  PushMapInvMap (push (inr ys) i) = refl
  PushMapInvMap (push (push xs i) j) = refl

  -- The special case 𝕁ames 2

  P0→X⋁X : 𝕁amesPush 0 → X∙ ⋁ X∙
  P0→X⋁X (inl (x , []))  = inl x
  P0→X⋁X (inr (x ∷ []))  = inr x
  P0→X⋁X (inr (incl [])) = inr x₀
  P0→X⋁X (inr (unit [] i)) = inr x₀
  P0→X⋁X (push [] i) = push tt i

  X⋁X→P0 : X∙ ⋁ X∙ → 𝕁amesPush 0
  X⋁X→P0 (inl x) = inl (x , [])
  X⋁X→P0 (inr x) = inr (x ∷ [])
  X⋁X→P0 (push tt i) = (push [] ∙ (λ i → inr (unit [] i))) i

  P0→X⋁X→P0 : (x : 𝕁amesPush 0) → X⋁X→P0 (P0→X⋁X x) ≡ x
  P0→X⋁X→P0 (inl (x , [])) = refl
  P0→X⋁X→P0 (inr (x ∷ [])) = refl
  P0→X⋁X→P0 (inr (incl [])) i = inr (unit [] (~ i))
  P0→X⋁X→P0 (inr (unit [] i)) j = inr (unit [] (i ∨ ~ j))
  P0→X⋁X→P0 (push [] i) j =
    hcomp (λ k → λ
      { (i = i0) → inl (x₀ , [])
      ; (i = i1) → inr (unit [] (~ j ∧ k))
      ; (j = i0) → compPath-filler (push []) (λ i → inr (unit [] i)) k i
      ; (j = i1) → push [] i })
    (push [] i)

  X⋁X→P0→X⋁X : (x : X∙ ⋁ X∙) → P0→X⋁X (X⋁X→P0 x) ≡ x
  X⋁X→P0→X⋁X (inl x) = refl
  X⋁X→P0→X⋁X (inr x) = refl
  X⋁X→P0→X⋁X (push tt i) j =
    hcomp (λ k → λ
      { (i = i0) → inl x₀
      ; (i = i1) → inr x₀
      ; (j = i0) → P0→X⋁X (compPath-filler (push []) refl k i)
      ; (j = i1) → push tt i })
    (push tt i)

  P0≃X⋁X : 𝕁amesPush 0 ≃ X∙ ⋁ X∙
  P0≃X⋁X = isoToEquiv (iso P0→X⋁X X⋁X→P0 X⋁X→P0→X⋁X P0→X⋁X→P0)

  -- The type family 𝕁ames can be constructed by iteratively using pushouts

  𝕁ames0≃ : 𝕁ames 0 ≃ Unit
  𝕁ames0≃ = isoToEquiv (iso (λ { [] → tt }) (λ { tt → [] }) (λ { tt → refl }) (λ { [] → refl }))

  𝕁ames1≃ : 𝕁ames 1 ≃ X
  𝕁ames1≃ = isoToEquiv (iso 𝕁ames1→X X→𝕁ames1 X→𝕁ames1→X 𝕁ames1→X→𝕁ames1)

  𝕁ames2+n≃ : (n : ℕ) → 𝕁ames (2 + n) ≃ Pushout leftMap rightMap
  𝕁ames2+n≃ n = isoToEquiv (iso PushInv PushMap PushMapInvMap PushInvMapInv)

  private
    left≃ : X × 𝕁ames 1 ≃ X × X
    left≃ = ≃-× (idEquiv _) 𝕁ames1≃

    lComm : (x : 𝕁amesPush 0) → left≃ .fst (leftMap x) ≡ ⋁↪ (P0→X⋁X x)
    lComm (inl (x , []))  = refl
    lComm (inr (x ∷ []))  = refl
    lComm (inr (incl [])) = refl
    lComm (inr (unit [] i)) = refl
    lComm (push [] i) = refl

    rComm : (x : 𝕁amesPush 0) → 𝕁ames1≃ .fst (rightMap x) ≡ fold⋁ (P0→X⋁X x)
    rComm (inl (x , []))  = refl
    rComm (inr (x ∷ []))  = refl
    rComm (inr (incl [])) = refl
    rComm (inr (unit [] i)) = refl
    rComm (push [] i) = refl

  𝕁ames2≃ : 𝕁ames 2 ≃ Pushout {A = X∙ ⋁ X∙} ⋁↪ fold⋁
  𝕁ames2≃ =
    compEquiv (𝕁ames2+n≃ 0)
      (pushoutEquiv _ _ _ _ P0≃X⋁X left≃ 𝕁ames1≃ (funExt lComm) (funExt rComm))

  -- The leftMap can be seen as pushout-product

  private
    Unit×-≃ : {A : Type ℓ} → A ≃ Unit × A
    Unit×-≃ = isoToEquiv (invIso lUnit×Iso)

    pt : Unit → X
    pt _ = x₀

  𝕁amesPush' : (n : ℕ) → Type ℓ
  𝕁amesPush' n = PushProd {X = Unit} {A = X} {Y = 𝕁ames n} {B = 𝕁ames (1 + n)} pt incl

  leftMap' : {n : ℕ} → 𝕁amesPush' n → X × 𝕁ames (1 + n)
  leftMap' = pt ×̂ incl

  𝕁amesPush→Push' : (n : ℕ) → 𝕁amesPush n → 𝕁amesPush' n
  𝕁amesPush→Push' n (inl x) = inr x
  𝕁amesPush→Push' n (inr x) = inl (tt , x)
  𝕁amesPush→Push' n (push x i) = push (tt , x) (~ i)

  𝕁amesPush'→Push : (n : ℕ) → 𝕁amesPush' n → 𝕁amesPush n
  𝕁amesPush'→Push n (inl (tt , x)) = inr x
  𝕁amesPush'→Push n (inr x) = inl x
  𝕁amesPush'→Push n (push (tt , x) i) = push x (~ i)

  𝕁amesPush≃ : (n : ℕ) → 𝕁amesPush n ≃ 𝕁amesPush' n
  𝕁amesPush≃ n = isoToEquiv
    (iso (𝕁amesPush→Push' n) (𝕁amesPush'→Push n)
         (λ { (inl x) → refl ; (inr x) → refl ; (push x i) → refl })
         (λ { (inl x) → refl ; (inr x) → refl ; (push x i) → refl }))

  ≃𝕁ames1 : X ≃ 𝕁ames 1
  ≃𝕁ames1 = isoToEquiv (iso X→𝕁ames1 𝕁ames1→X 𝕁ames1→X→𝕁ames1 X→𝕁ames1→X)

  ≃𝕁ames2+n : (n : ℕ) → Pushout leftMap rightMap ≃ 𝕁ames (2 + n)
  ≃𝕁ames2+n n = isoToEquiv (iso PushMap PushInv PushInvMapInv PushMapInvMap)

  -- The connectivity of inclusion

  private
    comp1 : (n : ℕ) → leftMap' ∘ 𝕁amesPush≃ n .fst ≡ leftMap
    comp1 n = funExt (λ { (inl x) → refl ; (inr x) → refl ; (push x i) → refl })

    comp2 : (n : ℕ) → ≃𝕁ames2+n n .fst ∘ inr ≡ incl
    comp2 n = funExt (λ _ → refl)

    comp3 : ≃𝕁ames1 .fst ∘ pt ∘ 𝕁ames0≃ .fst ≡ incl
    comp3 i [] = unit [] (~ i)

    isConnIncl0 :
        (n : ℕ) → isConnected (1 + n) X
      → isConnectedFun n (incl {X∙ = X∙} {n = 0})
    isConnIncl0 n conn =
      subst (isConnectedFun _) comp3
        (isConnectedComp _ _ _ (isEquiv→isConnected _ (≃𝕁ames1 .snd) _)
          (isConnectedComp _ _ _ (isConnectedPoint _ conn _)
            (isEquiv→isConnected _ (𝕁ames0≃ .snd) _)))

    isConnIncl-ind :
        (m n k : ℕ) → isConnected (1 + m) X
      → isConnectedFun n (incl {X∙ = X∙} {n = k})
      → isConnectedFun (m + n) (incl {X∙ = X∙} {n = 1 + k})
    isConnIncl-ind m n k connX connf =
      subst (isConnectedFun _) (comp2 _)
        (isConnectedComp _ _ _ (isEquiv→isConnected _ (≃𝕁ames2+n k .snd) _)
          (inrConnected _ _ _
            (subst (isConnectedFun _) (comp1 _)
              (isConnectedComp _ _ _
                (isConnected×̂ (isConnectedPoint _ connX _) connf)
                  (isEquiv→isConnected _ (𝕁amesPush≃ k .snd) _)))))

    nat-path : (n m k : ℕ) → (1 + (k + m)) · n ≡ k · n + (1 + m) · n
    nat-path = solve

  -- Connectivity results

  isConnectedIncl : (n : ℕ) → isConnected (1 + n) X
    → (m : ℕ) → isConnectedFun ((1 + m) · n) (incl {X∙ = X∙} {n = m})
  isConnectedIncl n conn 0 = subst (λ d → isConnectedFun d _) (sym (+-zero n)) (isConnIncl0 n conn)
  isConnectedIncl n conn (suc m) = isConnIncl-ind _ _ _ conn (isConnectedIncl n conn m)

  isConnectedIncl>n : (n : ℕ) → isConnected (1 + n) X
    → (m k : ℕ) → isConnectedFun ((1 + m) · n) (incl {X∙ = X∙} {n = k + m})
  isConnectedIncl>n n conn m k = isConnectedFunSubtr _ (k · n) _
    (subst (λ d → isConnectedFun d (incl {X∙ = X∙} {n = k + m}))
      (nat-path n m k) (isConnectedIncl n conn (k + m)))

  private
    inl∞ : (n : ℕ) → 𝕁ames n → 𝕁ames∞
    inl∞ _ = inl

  isConnectedInl : (n : ℕ) → isConnected (1 + n) X
    → (m : ℕ) → isConnectedFun ((1 + m) · n) (inl∞ m)
  isConnectedInl n conn m = isConnectedInl∞ _ _ _ (isConnectedIncl>n _ conn _)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module InstanceArgumentsBraces where

record T' : Set where

record T'' : Set where
  field a : T'

testT'' : T''
testT'' = record { a = record {}}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Prelude where

-- Booleans
data Bool : Set where
  tt : Bool
  ff : Bool

_||_ : Bool -> Bool -> Bool
tt || y = tt
ff || y = y

_&&_ : Bool -> Bool -> Bool
tt && y = y
ff && y = ff

if_then_else : {A : Set} -> Bool -> A -> A -> A
if tt then x else _ = x
if ff then _ else y = y

-- Eq "type class"
record Eq (A : Set) : Set where
  field
    _==_   : A -> A ->  Bool

open Eq {{...}} public

-- Function composition
_∘_ : ∀ {x y z : Set} -> (y -> z) -> (x -> y) -> (x -> z)
(f ∘ g) x = f (g x)

-- Product type
data _×_ (A B : Set) : Set where
    _,_ : A -> B -> A × B

uncurry : ∀ {x y z : Set} -> (x -> y -> z) -> (x × y) -> z
uncurry f (a , b) = f a b

-- Lists
data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

infixr 20 _::_
infixr 15 _++_

[_] : ∀ {A} -> A -> List A
[ x ] = x :: []

_++_ : ∀ {A} -> List A -> List A -> List A
[] ++ l = l
(x :: xs) ++ l = x :: (xs ++ l)

foldr : ∀ {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr f b [] = b
foldr f b (x :: xs) = f x (foldr f b xs)

map : ∀ {A B} -> (A -> B) -> List A -> List B
map f [] = []
map f (x :: xs) = f x :: map f xs

zip : ∀ {A B} -> List A -> List B -> List (A × B)
zip [] _                = []
zip _  []               = []
zip (x :: xs) (y :: ys) = (x , y) :: zip xs ys

-- Bottom type
-- data ⊥ : Set where

-- ¬ : Set -> Set
-- ¬ A = A -> ⊥

-- Decidable propositions and relations:
-- Rel : Set -> Set₁
-- Rel a = a -> a -> Set

-- data Dec (P : Set) : Set where
--   yes : (p : P) → Dec P
--   no : (¬p : ¬ P) → Dec P

-- Decidable : {a : Set} → Rel a → Set
-- Decidable _∼_ = forall x y → Dec (x ∼ y)

-- Natural numbers
data ℕ : Set where
  zero : ℕ
  suc  : ℕ -> ℕ

max_stars_repo_name: tuura/selective-theory-agda

max_issues_repo_name: tuura/selective-theory-agda

max_forks_repo_name: tuura/selective-theory-agda


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Inference(x : X) where
  import OutsideIn.TopLevel as TL
  import OutsideIn.TypeSchema as TS
  import OutsideIn.Expressions as E
  import OutsideIn.Environments as V
  import OutsideIn.Constraints as C
  import OutsideIn.Inference.Solver as S
  import OutsideIn.Inference.Prenexer as P
  import OutsideIn.Inference.Separator as SP
  import OutsideIn.Inference.ConstraintGen as CG

  open S(x)
  open P(x)
  open SP(x)
  open CG(x)
  open X(x)
  open TL(x)
  open TS(x)
  open E(x)
  open V(x)
  open C(x)

  private
    module PlusN-m {n} = Monad(PlusN-is-monad {n})
    module QC-f = Functor(qconstraint-is-functor)
    module Ax-f = Functor(axiomscheme-is-functor)
    module Exp-f {ev}{s} = Functor(expression-is-functor₂ {ev}{s})
    module TS-f {x} = Functor(type-schema-is-functor {x})
    module Type-m  = Monad(type-is-monad)
    module Type-f  = Functor(type-is-functor)

  open Type-m

  data _,_►_ {x ev : Set}⦃ eq : Eq x ⦄(Q : AxiomScheme x)(Γ : Environment ev x) : Program ev x → Set where
    Empty : Q , Γ ► end
    BindA : ∀ {r}{m}{e : Expression ev (x ⨁ m) r}{prog : Program (Ⓢ ev) x}{τ}{C : Constraint (x ⨁ m) Extended}{Qc}{f}{f′}
              {C′ : Constraint ((x ⨁ m) ⨁ f) Flat}{r}{C′′ : SeparatedConstraint ((x ⨁ m) ⨁ f) r}{θ : (x ⨁ m) ⨁ f → Type ((x ⨁ m) ⨁ f′)}
         → TS-f.map (PlusN-m.unit {m}) ∘ Γ ► e ∶ τ ↝ C
         → C prenex: f , C′
         → C′ separate: r , C′′
         → let eq′ = PlusN-eq {m} eq in Ax-f.map (PlusN-m.unit {m}) Q , Qc , f solv► C′′ ↝ f′ , ε , θ
         → Q , ⟨ ∀′ m · Qc ⇒ τ ⟩, Γ ► prog
         → Q , Γ ► bind₂ m · e  ∷ Qc ⇒ τ , prog
    Bind :  ∀{r}{e : Expression ev x r}{prog : Program (Ⓢ ev) x}{C : Constraint (Ⓢ x) Extended}{f}{C′ : Constraint (x ⨁ suc f) Flat}
             {r′}{C′′ : SeparatedConstraint (x ⨁ suc f) r′}{n}{θ : x ⨁ suc f → Type (x ⨁ n)}{Qr}
         → TS-f.map (suc) ∘ Γ ► Exp-f.map suc e ∶ unit zero  ↝ C
         → C prenex: f , C′
         → C′ separate: r′ , C′′
         → Q , ε , suc f solv► C′′ ↝ n , Qr , θ
         → Q , ⟨ ∀′ n · Qr ⇒ (θ (PlusN-m.unit {f} zero)) ⟩, Γ ► prog
         → Q , Γ ► bind₁ e , prog

  go :  {ev tv : Set}(Q : AxiomScheme tv)(Γ : Environment ev tv) → (eq : Eq tv) → (p : Program ev tv) → Ⓢ (Q , Γ ► p)
  go Q Γ eq (end) = suc Empty
  go {ev}{tv} Q Γ eq (bind₁ e , prog)
                       with genConstraint {ev}{Ⓢ tv} (TS-f.map suc ∘ Γ) (Exp-f.map suc e) (unit zero)
  ... | C , prf₁       with prenex C
  ... | f , C′ , prf₂  with separate C′
  ... | r , C′′ , prf₃ with solver eq (suc f) Q ε C′′
  ... | zero = zero
  ... | suc (m , Qr , θ , prf₄) with go Q (⟨ ∀′ m · Qr ⇒ (θ (PlusN-m.unit {f} zero)) ⟩, Γ) eq prog
  ... | zero = zero
  ... | suc prf₅ = suc (Bind prf₁ prf₂ prf₃ prf₄ prf₅)
  go Q Γ eq (bind₂ m · e ∷ Qc ⇒ τ , prog)
                       with genConstraint (TS-f.map (PlusN-m.unit {m}) ∘ Γ) e τ
  ... | C , prf₁       with prenex C
  ... | f , C′ , prf₂  with separate C′
  ... | r , C′′ , prf₃ with solver (PlusN-eq {m} eq) f (Ax-f.map (PlusN-m.unit {m}) Q) Qc C′′
  ... | zero = zero
  ... | suc (f′ , Qr , θ , prf₄) with is-ε Qr
  ... | no _ = zero
  ... | yes prf₄′                with go Q (⟨ ∀′ m · Qc ⇒ τ ⟩, Γ) eq prog
  ... | zero = zero
  ... | suc prf₅ = let
         eq′ =  PlusN-eq {m} eq
        in suc (BindA prf₁ prf₂ prf₃ (subst (λ Qr → Ax-f.map (PlusN-m.unit {m}) Q , Qc , f solv► C′′ ↝ f′ , Qr , θ  ) prf₄′ prf₄) prf₅)

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
postulate
  T     : Set
  pre   : (T → T) → T
  pre!_ : (T → T) → T
  _post : T → Set
  _+_   : T → T → T
  _>>=_ : T → (T → T) → T

infix 5 pre!_ _>>=_
infix 4 _post
infixl 3 _+_

-- add parens
test-1a : Set
test-1a = {!pre λ x → x!} post

-- no parens
test-1b : Set
test-1b = {!pre (λ x → x)!} post

-- add parens
test-1c : Set
test-1c = {!pre! λ x → x!} post

-- no parens
test-1d : Set
test-1d = {!pre! (λ x → x)!} post

-- add parens
test-1e : T → Set
test-1e e = {!e >>= λ x → x!} post

-- no parens
test-1f : T → Set
test-1f e = {!e >>= (λ x → x)!} post

-- add parens
test-2a : Set
test-2a = pre {!λ x → x!} post

-- add parens
test-2b : Set
test-2b = pre! {!λ x → x!} post

-- no parens
test-3a : T
test-3a = pre {!λ x → x!}

-- no parens
test-3b : T
test-3b = pre! {!λ x → x!}

-- no parens
test-4a : T → T
test-4a e = e + {!pre λ x → x!}

-- no parens
test-4b : T → T
test-4b e = e + {!pre! λ x → x!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

import sets.bool
import sets.empty
import sets.fin
import sets.nat
import sets.int
import sets.unit
import sets.vec
import sets.list

open import sets.properties
open import sets.finite

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
------------------------------------------------------------------------
-- Truncation, defined using a kind of Church encoding
------------------------------------------------------------------------

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

-- Partly following the HoTT book.

open import Equality

module H-level.Truncation.Church
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude
open import Logical-equivalence using (_⇔_)

open import Bijection eq as Bijection using (_↔_)
open Derived-definitions-and-properties eq
open import Embedding eq hiding (_∘_)
open import Equality.Decidable-UIP eq
import Equality.Groupoid eq as EG
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
import Equivalence.Half-adjoint eq as HA
open import Function-universe eq as F hiding (_∘_)
open import Groupoid eq
open import H-level eq as H-level
open import H-level.Closure eq
open import Nat eq
open import Preimage eq as Preimage using (_⁻¹_)
open import Surjection eq using (_↠_; Split-surjective)

-- Truncation.

∥_∥ : ∀ {a} → Type a → ℕ → (ℓ : Level) → Type (a ⊔ lsuc ℓ)
∥ A ∥ n ℓ = (P : Type ℓ) → H-level n P → (A → P) → P

-- If A is inhabited, then ∥ A ∥ n ℓ is also inhabited.

∣_∣ : ∀ {n ℓ a} {A : Type a} → A → ∥ A ∥ n ℓ
∣ x ∣ = λ _ _ f → f x

-- A special case of ∣_∣.

∣_∣₁ : ∀ {ℓ a} {A : Type a} → A → ∥ A ∥ 1 ℓ
∣ x ∣₁ = ∣_∣ {n = 1} x

-- The truncation produces types of the right h-level (assuming
-- extensionality).

truncation-has-correct-h-level :
  ∀ n {ℓ a} {A : Type a} →
  Extensionality (a ⊔ lsuc ℓ) (a ⊔ ℓ) →
  H-level n (∥ A ∥ n ℓ)
truncation-has-correct-h-level n {ℓ} {a} ext =
  Π-closure (lower-extensionality a            lzero ext) n λ _ →
  Π-closure (lower-extensionality (a ⊔ lsuc ℓ) lzero ext) n λ h →
  Π-closure (lower-extensionality (lsuc ℓ)     a     ext) n λ _ →
  h

-- Primitive "recursion" for truncated types.

rec :
  ∀ n {a b} {A : Type a} {B : Type b} →
  H-level n B →
  (A → B) → ∥ A ∥ n b → B
rec _ h f x = x _ h f

private

  -- The function rec computes in the right way.

  rec-∣∣ :
    ∀ {n a b} {A : Type a} {B : Type b}
    (h : H-level n B) (f : A → B) (x : A) →
    rec _ h f ∣ x ∣ ≡ f x
  rec-∣∣ _ _ _ = refl _

-- Map function.

∥∥-map : ∀ n {a b ℓ} {A : Type a} {B : Type b} →
         (A → B) →
         ∥ A ∥ n ℓ → ∥ B ∥ n ℓ
∥∥-map _ f x = λ P h g → x P h (g ∘ f)

-- The truncation operator preserves logical equivalences.

∥∥-cong-⇔ : ∀ {n a b ℓ} {A : Type a} {B : Type b} →
            A ⇔ B → ∥ A ∥ n ℓ ⇔ ∥ B ∥ n ℓ
∥∥-cong-⇔ A⇔B = record
  { to   = ∥∥-map _ (_⇔_.to   A⇔B)
  ; from = ∥∥-map _ (_⇔_.from A⇔B)
  }

-- The truncation operator preserves bijections (assuming
-- extensionality).

∥∥-cong : ∀ {k n a b ℓ} {A : Type a} {B : Type b} →
          Extensionality (a ⊔ b ⊔ lsuc ℓ) (a ⊔ b ⊔ ℓ) →
          A ↔[ k ] B → ∥ A ∥ n ℓ ↔[ k ] ∥ B ∥ n ℓ
∥∥-cong {k} {n} {a} {b} {ℓ} ext A↝B = from-bijection (record
  { surjection = record
    { logical-equivalence = record
      { to   = ∥∥-map _ (_↔_.to   A↔B)
      ; from = ∥∥-map _ (_↔_.from A↔B)
      }
    ; right-inverse-of = lemma (lower-extensionality a a ext) A↔B
    }
  ; left-inverse-of = lemma (lower-extensionality b b ext) (inverse A↔B)
  })
  where
  A↔B = from-isomorphism A↝B

  lemma :
    ∀ {c d} {C : Type c} {D : Type d} →
    Extensionality (d ⊔ lsuc ℓ) (d ⊔ ℓ) →
    (C↔D : C ↔ D) (∥d∥ : ∥ D ∥ n ℓ) →
    ∥∥-map _ (_↔_.to C↔D) (∥∥-map _ (_↔_.from C↔D) ∥d∥) ≡ ∥d∥
  lemma {d = d} ext C↔D ∥d∥ =
    apply-ext (lower-extensionality d        lzero ext) λ P →
    apply-ext (lower-extensionality _        lzero ext) λ h →
    apply-ext (lower-extensionality (lsuc ℓ) d     ext) λ g →

      ∥d∥ P h (g ∘ _↔_.to C↔D ∘ _↔_.from C↔D)  ≡⟨ cong (λ f → ∥d∥ P h (g ∘ f)) $
                                                    apply-ext (lower-extensionality (lsuc ℓ) ℓ ext)
                                                      (_↔_.right-inverse-of C↔D) ⟩∎
      ∥d∥ P h g                                ∎

-- The universe level can be decreased (unless it is zero).

with-lower-level :
  ∀ ℓ₁ {ℓ₂ a} n {A : Type a} →
  ∥ A ∥ n (ℓ₁ ⊔ ℓ₂) → ∥ A ∥ n ℓ₂
with-lower-level ℓ₁ _ x =
  λ P h f → lower (x (↑ ℓ₁ P) (↑-closure _ h) (lift ∘ f))

private

  -- The function with-lower-level computes in the right way.

  with-lower-level-∣∣ :
    ∀ {ℓ₁ ℓ₂ a n} {A : Type a} (x : A) →
    with-lower-level ℓ₁ {ℓ₂ = ℓ₂} n ∣ x ∣ ≡ ∣ x ∣
  with-lower-level-∣∣ _ = refl _

-- ∥_∥ is downwards closed in the h-level.

downwards-closed :
  ∀ {m n a ℓ} {A : Type a} →
  n ≤ m →
  ∥ A ∥ m ℓ → ∥ A ∥ n ℓ
downwards-closed n≤m x = λ P h f → x P (H-level.mono n≤m h) f

private

  -- The function downwards-closed computes in the right way.

  downwards-closed-∣∣ :
    ∀ {m n a ℓ} {A : Type a} (n≤m : n ≤ m) (x : A) →
    downwards-closed {ℓ = ℓ} n≤m ∣ x ∣ ≡ ∣ x ∣
  downwards-closed-∣∣ _ _ = refl _

-- The function rec can be used to define a kind of dependently typed
-- eliminator for the propositional truncation (assuming
-- extensionality).

prop-elim :
  ∀ {ℓ a p} {A : Type a} →
  Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a ⊔ p) →
  (P : ∥ A ∥ 1 ℓ → Type p) →
  (∀ x → Is-proposition (P x)) →
  ((x : A) → P ∣ x ∣₁) →
  ∥ A ∥ 1 (lsuc ℓ ⊔ a ⊔ p) → (x : ∥ A ∥ 1 ℓ) → P x
prop-elim {ℓ} {a} {p} ext P P-prop f =
  rec 1
      (Π-closure (lower-extensionality lzero (ℓ ⊔ a) ext) 1 P-prop)
      (λ x _ → subst P
                     (truncation-has-correct-h-level 1
                        (lower-extensionality lzero p ext) _ _)
                     (f x))

abstract

  -- The eliminator gives the right result, up to propositional
  -- equality, when applied to ∣ x ∣ and ∣ x ∣.

  prop-elim-∣∣ :
    ∀ {ℓ a p} {A : Type a}
    (ext : Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a ⊔ p))
    (P : ∥ A ∥ 1 ℓ → Type p)
    (P-prop : ∀ x → Is-proposition (P x))
    (f : (x : A) → P ∣ x ∣₁) (x : A) →
    prop-elim ext P P-prop f ∣ x ∣₁ ∣ x ∣₁ ≡ f x
  prop-elim-∣∣ _ _ P-prop _ _ = P-prop _ _ _

-- Nested truncations can sometimes be flattened.

flatten↠ :
  ∀ {m n a ℓ} {A : Type a} →
  Extensionality (a ⊔ lsuc ℓ) (a ⊔ ℓ) →
  m ≤ n →
  ∥ ∥ A ∥ m ℓ ∥ n (a ⊔ lsuc ℓ) ↠ ∥ A ∥ m ℓ
flatten↠ ext m≤n = record
  { logical-equivalence = record
    { to   = rec _
                 (H-level.mono m≤n
                    (truncation-has-correct-h-level _ ext))
                 F.id
    ; from = ∣_∣
    }
  ; right-inverse-of = refl
  }

flatten↔ :
  ∀ {a ℓ} {A : Type a} →
  Extensionality (lsuc (a ⊔ lsuc ℓ)) (lsuc (a ⊔ lsuc ℓ)) →
  (∥ ∥ A ∥ 1 ℓ ∥ 1       (a ⊔ lsuc ℓ) →
   ∥ ∥ A ∥ 1 ℓ ∥ 1 (lsuc (a ⊔ lsuc ℓ))) →
  ∥ ∥ A ∥ 1 ℓ ∥ 1 (a ⊔ lsuc ℓ) ↔ ∥ A ∥ 1 ℓ
flatten↔ ext resize = record
  { surjection      = flatten↠ {m = 1} ext′ ≤-refl
  ; left-inverse-of = λ x →
      prop-elim
        ext
        (λ x → ∣ rec 1
                     (H-level.mono (≤-refl {n = 1})
                        (truncation-has-correct-h-level 1 ext′))
                     F.id x ∣₁ ≡ x)
        (λ _ → ⇒≡ 1 $ truncation-has-correct-h-level
                        1 (lower-extensionality lzero _ ext))
        (λ _ → refl _)
        (resize x)
        x
  }
  where
  ext′ = lower-extensionality _ _ ext

-- Surjectivity.
--
-- I'm not quite sure what the universe level of the truncation should
-- be, so I've included it as a parameter.

Surjective : ∀ {a b} ℓ {A : Type a} {B : Type b} →
             (A → B) → Type (a ⊔ b ⊔ lsuc ℓ)
Surjective ℓ f = ∀ b → ∥ f ⁻¹ b ∥ 1 ℓ

-- The property Surjective ℓ f is a proposition (assuming
-- extensionality).

Surjective-propositional :
  ∀ {ℓ a b} {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (a ⊔ b ⊔ lsuc ℓ) (a ⊔ b ⊔ lsuc ℓ) →
  Is-proposition (Surjective ℓ f)
Surjective-propositional {ℓ} {a} ext =
  Π-closure (lower-extensionality (a ⊔ lsuc ℓ) lzero ext) 1 λ _ →
  truncation-has-correct-h-level 1
    (lower-extensionality lzero (lsuc ℓ) ext)

-- Split surjective functions are surjective.

Split-surjective→Surjective :
  ∀ {a b ℓ} {A : Type a} {B : Type b} {f : A → B} →
  Split-surjective f → Surjective ℓ f
Split-surjective→Surjective s = λ b → ∣ s b ∣₁

-- Being both surjective and an embedding is equivalent to being an
-- equivalence.
--
-- This is Corollary 4.6.4 from the first edition of the HoTT book
-- (the proof is perhaps not quite identical).

surjective×embedding≃equivalence :
  ∀ {a b} ℓ {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (lsuc (a ⊔ b ⊔ ℓ)) →
  (Surjective (a ⊔ b ⊔ ℓ) f × Is-embedding f) ≃ Is-equivalence f
surjective×embedding≃equivalence {a} {b} ℓ {f = f} ext =
  Eq.⇔→≃
    (×-closure 1 (Surjective-propositional ext)
                 (Is-embedding-propositional
                    (lower-extensionality _ _ ext)))
    (Eq.propositional (lower-extensionality _ _ ext) _)
    (λ (is-surj , is-emb) →
       _⇔_.from HA.Is-equivalence⇔Is-equivalence-CP $ λ y →
                                  $⟨ is-surj y ⟩
       ∥ f ⁻¹ y ∥ 1 (a ⊔ b ⊔ ℓ)   ↝⟨ with-lower-level ℓ 1 ⟩
       ∥ f ⁻¹ y ∥ 1 (a ⊔ b)       ↝⟨ rec 1
                                         (Contractible-propositional
                                            (lower-extensionality _ _ ext))
           (f ⁻¹ y                       ↝⟨ propositional⇒inhabited⇒contractible
                                              (embedding→⁻¹-propositional is-emb y) ⟩□
            Contractible (f ⁻¹ y)        □) ⟩□

       Contractible (f ⁻¹ y)      □)
    (λ is-eq →
         (λ y →                       $⟨ HA.inverse is-eq y
                                       , HA.right-inverse-of is-eq y
                                       ⟩
            f ⁻¹ y                    ↝⟨ ∣_∣₁ ⟩□
            ∥ f ⁻¹ y ∥ 1 (a ⊔ b ⊔ ℓ)  □)

       ,                  ($⟨ is-eq ⟩
         Is-equivalence f  ↝⟨ Embedding.is-embedding ∘ from-equivalence ∘ Eq.⟨ _ ,_⟩ ⟩□
         Is-embedding f    □))

-- If the underlying type has a certain h-level, then there is a split
-- surjection from corresponding truncations (if they are "big"
-- enough) to the type itself.

∥∥↠ : ∀ ℓ {a} {A : Type a} n →
      H-level n A → ∥ A ∥ n (a ⊔ ℓ) ↠ A
∥∥↠ ℓ _ h = record
  { logical-equivalence = record
    { to   = rec _ h F.id ∘ with-lower-level ℓ _
    ; from = ∣_∣
    }
  ; right-inverse-of = refl
  }

-- If the underlying type is a proposition, then propositional
-- truncations of the type are isomorphic to the type itself (if they
-- are "big" enough, and assuming extensionality).

∥∥↔ : ∀ ℓ {a} {A : Type a} →
      Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ ℓ) →
      Is-proposition A → ∥ A ∥ 1 (a ⊔ ℓ) ↔ A
∥∥↔ ℓ ext A-prop = record
  { surjection      = ∥∥↠ ℓ 1 A-prop
  ; left-inverse-of = λ _ →
      truncation-has-correct-h-level 1 ext _ _
  }

-- A simple isomorphism involving propositional truncation.

∥∥×↔ :
  ∀ {ℓ a} {A : Type a} →
  Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a) →
  ∥ A ∥ 1 ℓ × A ↔ A
∥∥×↔ {ℓ} {A = A} ext =
  ∥ A ∥ 1 ℓ × A  ↝⟨ ×-comm ⟩
  A × ∥ A ∥ 1 ℓ  ↝⟨ (drop-⊤-right λ a →
                     _⇔_.to contractible⇔↔⊤ $
                       propositional⇒inhabited⇒contractible
                         (truncation-has-correct-h-level 1 ext)
                         ∣ a ∣₁) ⟩□
  A              □

-- A variant of ∥∥×↔, introduced to ensure that the right-inverse-of
-- proof is, by definition, simple (see right-inverse-of-∥∥×≃ below).

∥∥×≃ :
  ∀ {ℓ a} {A : Type a} →
  Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a) →
  (∥ A ∥ 1 ℓ × A) ≃ A
∥∥×≃ ext = Eq.↔→≃
  proj₂
  (λ x → ∣ x ∣₁ , x)
  refl
  (λ _ → cong (_, _) (truncation-has-correct-h-level 1 ext _ _))

private

  right-inverse-of-∥∥×≃ :
    ∀ {ℓ a} {A : Type a}
    (ext : Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a)) (x : A) →
    _≃_.right-inverse-of (∥∥×≃ {ℓ = ℓ} ext) x ≡ refl x
  right-inverse-of-∥∥×≃ _ x = refl (refl x)

-- ∥_∥ commutes with _×_ (assuming extensionality and a resizing
-- function for the propositional truncation).

∥∥×∥∥↔∥×∥ :
  ∀ {a b} ℓ {A : Type a} {B : Type b} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →
  (∀ {x} {X : Type x} →
     ∥ X ∥ 1       (a ⊔ b ⊔ ℓ) →
     ∥ X ∥ 1 (lsuc (a ⊔ b ⊔ ℓ))) →
  let ℓ′ = a ⊔ b ⊔ ℓ in
  (∥ A ∥ 1 ℓ′ × ∥ B ∥ 1 ℓ′) ↔ ∥ A × B ∥ 1 ℓ′
∥∥×∥∥↔∥×∥ _ ext resize = record
  { surjection = record
    { logical-equivalence = record
      { from = λ p → ∥∥-map 1 proj₁ p , ∥∥-map 1 proj₂ p
      ; to   = λ { (x , y) →
                   rec 1
                       (truncation-has-correct-h-level 1 ext)
                       (λ x → rec 1
                                  (truncation-has-correct-h-level 1 ext)
                                  (λ y → ∣ x , y ∣₁)
                                  (resize y))
                       (resize x) }
      }
    ; right-inverse-of = λ _ → truncation-has-correct-h-level 1 ext _ _
    }
  ; left-inverse-of = λ _ →
      ×-closure 1
        (truncation-has-correct-h-level 1 ext)
        (truncation-has-correct-h-level 1 ext)
        _ _
  }

-- If A is merely inhabited (at a certain level), then the
-- propositional truncation of A (at the same level) is isomorphic to
-- the unit type (assuming extensionality).

inhabited⇒∥∥↔⊤ :
  ∀ {ℓ a} {A : Type a} →
  Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a) →
  ∥ A ∥ 1 ℓ → ∥ A ∥ 1 ℓ ↔ ⊤
inhabited⇒∥∥↔⊤ ext ∥a∥ =
  _⇔_.to contractible⇔↔⊤ $
    propositional⇒inhabited⇒contractible
      (truncation-has-correct-h-level 1 ext)
      ∥a∥

-- If A is not inhabited, then the propositional truncation of A is
-- isomorphic to the empty type.

not-inhabited⇒∥∥↔⊥ :
  ∀ {ℓ₁ ℓ₂ a} {A : Type a} →
  ¬ A → ∥ A ∥ 1 ℓ₁ ↔ ⊥ {ℓ = ℓ₂}
not-inhabited⇒∥∥↔⊥ {A = A} =
  ¬ A            ↝⟨ (λ ¬a ∥a∥ → rec 1 ⊥-propositional ¬a (with-lower-level _ 1 ∥a∥)) ⟩
  ¬ ∥ A ∥ 1 _    ↝⟨ inverse ∘ Bijection.⊥↔uninhabited ⟩□
  ∥ A ∥ 1 _ ↔ ⊥  □

-- The following two results come from "Generalizations of Hedberg's
-- Theorem" by Kraus, Escardó, Coquand and Altenkirch.

-- Types with constant endofunctions are "h-stable" (meaning that
-- "mere inhabitance" implies inhabitance).

constant-endofunction⇒h-stable :
  ∀ {a} {A : Type a} {f : A → A} →
  Constant f → ∥ A ∥ 1 a → A
constant-endofunction⇒h-stable {a} {A} {f} c =
  ∥ A ∥ 1 a                ↝⟨ rec 1 (fixpoint-lemma f c) (λ x → f x , c (f x) x) ⟩
  (∃ λ (x : A) → f x ≡ x)  ↝⟨ proj₁ ⟩□
  A                        □

-- Having a constant endofunction is logically equivalent to being
-- h-stable (assuming extensionality).

constant-endofunction⇔h-stable :
  ∀ {a} {A : Type a} →
  Extensionality (lsuc a) a →
  (∃ λ (f : A → A) → Constant f) ⇔ (∥ A ∥ 1 a → A)
constant-endofunction⇔h-stable ext = record
  { to = λ { (_ , c) → constant-endofunction⇒h-stable c }
  ; from = λ f → f ∘ ∣_∣₁ , λ x y →

      f ∣ x ∣₁  ≡⟨ cong f $ truncation-has-correct-h-level 1 ext _ _ ⟩∎
      f ∣ y ∣₁  ∎
  }

-- The following three lemmas were communicated to me by Nicolai
-- Kraus. (In slightly different form.) They are closely related to
-- Lemma 2.1 in his paper "The General Universal Property of the
-- Propositional Truncation".

-- A variant of ∥∥×≃.

drop-∥∥ :
  ∀ ℓ {a b} {A : Type a} {B : A → Type b} →
  Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →

  (∥ A ∥ 1 (a ⊔ ℓ) → ∀ x → B x)
    ↔
  (∀ x → B x)
drop-∥∥ ℓ {a} {b} {A} {B} ext =

  (∥ A ∥ 1 _ → ∀ x → B x)              ↝⟨ inverse currying ⟩

  ((p : ∥ A ∥ 1 _ × A) → B (proj₂ p))  ↝⟨ Π-cong (lower-extensionality lzero (a ⊔ ℓ) ext)
                                                 (∥∥×≃ (lower-extensionality lzero b ext))
                                                 (λ _ → F.id) ⟩□
  (∀ x → B x)                          □

-- Another variant of ∥∥×≃.

push-∥∥ :
  ∀ ℓ {a b c} {A : Type a} {B : A → Type b} {C : (∀ x → B x) → Type c} →
  Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ b ⊔ c ⊔ ℓ) →

  (∥ A ∥ 1 (a ⊔ ℓ) → ∃ λ (f : ∀ x → B x) → C f)
    ↔
  (∃ λ (f : ∀ x → B x) → ∥ A ∥ 1 (a ⊔ ℓ) → C f)

push-∥∥ ℓ {a} {b} {c} {A} {B} {C} ext =

  (∥ A ∥ 1 _ → ∃ λ (f : ∀ x → B x) → C f)                ↝⟨ ΠΣ-comm ⟩

  (∃ λ (f : ∥ A ∥ 1 _ → ∀ x → B x) → ∀ ∥x∥ → C (f ∥x∥))  ↝⟨ Σ-cong (drop-∥∥ ℓ (lower-extensionality lzero c ext)) (λ f →
                                                            ∀-cong (lower-extensionality lzero (a ⊔ b ⊔ ℓ) ext) λ ∥x∥ →
                                                            ≡⇒↝ _ $ cong C $ apply-ext (lower-extensionality _ (a ⊔ c ⊔ ℓ) ext) λ x →
      f ∥x∥ x                                                 ≡⟨ cong (λ ∥x∥ → f ∥x∥ x) $
                                                                 truncation-has-correct-h-level 1
                                                                   (lower-extensionality lzero (b ⊔ c) ext)
                                                                   _ _ ⟩
      f ∣ x ∣₁ x                                              ≡⟨ sym $ subst-refl _ _ ⟩∎

      subst B (refl x) (f ∣ x ∣₁ x)                           ∎) ⟩□

  (∃ λ (f : ∀ x → B x) → ∥ A ∥ 1 _ → C (λ x → f x))      □

-- This is an instance of a variant of Lemma 2.1 from "The General
-- Universal Property of the Propositional Truncation" by Kraus.

drop-∥∥₃ :
  ∀ ℓ {a b c d}
    {A : Type a} {B : A → Type b} {C : A → (∀ x → B x) → Type c}
    {D : A → (f : ∀ x → B x) → (∀ x → C x f) → Type d} →
  Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ b ⊔ c ⊔ d ⊔ ℓ) →

  (∥ A ∥ 1 (a ⊔ ℓ) →
   ∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)
    ↔
  (∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)

drop-∥∥₃ ℓ {b = b} {c} {A = A} {B} {C} {D} ext =
  (∥ A ∥ 1 _ →
   ∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)  ↝⟨ push-∥∥ ℓ ext ⟩

  (∃ λ (f : ∀ x → B x) →
   ∥ A ∥ 1 _ → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)            ↝⟨ (∃-cong λ _ →
                                                                     push-∥∥ ℓ (lower-extensionality lzero b ext)) ⟩
  (∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) →
   ∥ A ∥ 1 _ → ∀ x → D x f g)                                    ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                     drop-∥∥ ℓ (lower-extensionality lzero (b ⊔ c) ext)) ⟩□
  (∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)  □

-- Having a coherently constant function into a groupoid is equivalent
-- to having a function from a propositionally truncated type into the
-- groupoid (assuming extensionality). This result is Proposition 2.3
-- in "The General Universal Property of the Propositional Truncation"
-- by Kraus.

Coherently-constant :
  ∀ {a b} {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Coherently-constant f =
  ∃ λ (c : Constant f) →
  ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃

coherently-constant-function≃∥inhabited∥⇒inhabited :
  ∀ {a b} ℓ {A : Type a} {B : Type b} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →
  H-level 3 B →
  (∃ λ (f : A → B) → Coherently-constant f) ≃ (∥ A ∥ 1 (a ⊔ b ⊔ ℓ) → B)
coherently-constant-function≃∥inhabited∥⇒inhabited {a} {b} ℓ {A} {B}
                                                   ext B-groupoid =
  (∃ λ (f : A → B) → Coherently-constant f)               ↔⟨ inverse $ drop-∥∥₃ (b ⊔ ℓ) ext ⟩
  (∥ A ∥ 1 ℓ′ → ∃ λ (f : A → B) → Coherently-constant f)  ↝⟨ ∀-cong (lower-extensionality lzero ℓ ext) (inverse ∘ equivalence₂) ⟩□
  (∥ A ∥ 1 ℓ′ → B)                                        □
  where
  ℓ′ = a ⊔ b ⊔ ℓ

  rearrangement-lemma = λ a₀ →
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ ∃-comm ⟩

    (∃ λ (f : A → B) →
     ∃ λ (f₁ : B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) →
     ∃ λ (f₁ : B) →
     ∃ λ (c : Constant f) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-cong λ _ → ∃-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-cong λ _ → ∃-cong λ _ → ×-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (d₂ : (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂) →
     trans (c a₀ a₀) (c₁ a₀) ≡ c₂)                                     ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-cong λ _ → ∃-comm) ⟩□
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₂ : (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     trans (c a₀ a₀) (c₁ a₀) ≡ c₂)                                     □

  equivalence₁ : A → (B ≃ ∃ λ (f : A → B) → Coherently-constant f)
  equivalence₁ a₀ = Eq.↔⇒≃ (
    B                                                                    ↝⟨ (inverse $ drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 0 λ _ →
                                                                               singleton-contractible _) ⟩
    (∃ λ (f₁ : B) →
     (a : A) → ∃ λ (b : B) → b ≡ f₁)                                     ↝⟨ (∃-cong λ _ → ΠΣ-comm) ⟩

    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → (a : A) → f a ≡ f₁)                               ↝⟨ (∃-cong λ _ → ∃-cong λ _ → inverse $ drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               Π-closure (lower-extensionality _ ℓ       ext) 0 λ _ →
                                                                               Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 0 λ _ →
                                                                               singleton-contractible _) ⟩
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∀ a₁ a₂ → ∃ λ (c : f a₁ ≡ f a₂) → c ≡ trans (c₁ a₁) (sym (c₁ a₂)))  ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∀-cong (lower-extensionality _ ℓ       ext) λ _ →
                                                                             ∀-cong (lower-extensionality _ (a ⊔ ℓ) ext) λ _ →
                                                                             ∃-cong λ _ → ≡⇒↝ _ $ sym $ [trans≡]≡[≡trans-symʳ] _ _ _) ⟩
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∀ a₁ a₂ → ∃ λ (c : f a₁ ≡ f a₂) → trans c (c₁ a₂) ≡ c₁ a₁)          ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∀-cong (lower-extensionality _ ℓ ext) λ _ →
                                                                             ΠΣ-comm) ⟩
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∀ a₁ → ∃ λ (c : ∀ a₂ → f a₁ ≡ f a₂) →
            ∀ a₂ → trans (c a₂) (c₁ a₂) ≡ c₁ a₁)                         ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ΠΣ-comm) ⟩

    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) → ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁)   ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             inverse $ drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               other-singleton-contractible _) ⟩
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → trans (c a₀ a₀) (c₁ a₀) ≡ c₂)                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ c₁ → ∃-cong λ c → ∃-cong λ d₁ →
                                                                             ∃-cong λ _ → inverse $ drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               propositional⇒inhabited⇒contractible
                                                                                (Π-closure (lower-extensionality _ ℓ       ext) 1 λ _ →
                                                                                Π-closure (lower-extensionality _ ℓ       ext) 1 λ _ →
                                                                                Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 1 λ _ →
                                                                                B-groupoid)
                                                                                (λ a₁ a₂ a₃ →
         trans (c a₁ a₂) (c a₂ a₃)                                                  ≡⟨ cong₂ trans (≡⇒↝ implication
                                                                                ([trans≡]≡[≡trans-symʳ] _ _ _) (d₁ _ _))
                                                                                (≡⇒↝ implication
                                                                                ([trans≡]≡[≡trans-symʳ] _ _ _) (d₁ _ _)) ⟩
         trans (trans (c₁ a₁) (sym (c₁ a₂)))
               (trans (c₁ a₂) (sym (c₁ a₃)))                                        ≡⟨ sym $ trans-assoc _ _ _ ⟩

         trans (trans (trans (c₁ a₁) (sym (c₁ a₂))) (c₁ a₂))
               (sym (c₁ a₃))                                                        ≡⟨ cong (flip trans _) $ trans-[trans-sym]- _ _ ⟩

         trans (c₁ a₁) (sym (c₁ a₃))                                                ≡⟨ sym $ ≡⇒↝ implication
                                                                                ([trans≡]≡[≡trans-symʳ] _ _ _) (d₁ _ _) ⟩∎
         c a₁ a₃                                                                    ∎)) ⟩

    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃)                   ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ c₁ → ∃-cong λ c → ∃-cong λ d₁ →
                                                                             ∃-cong λ c₂ → ∃-cong λ d₃ → inverse $ drop-⊤-right λ d →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               propositional⇒inhabited⇒contractible
                                                                                (Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 1 λ _ →
                                                                                B-groupoid)
                                                                                (λ a →
         trans (c a₀ a) (c₁ a)                                                      ≡⟨ cong (λ x → trans x _) $ sym $ d _ _ _ ⟩
         trans (trans (c a₀ a₀) (c a₀ a)) (c₁ a)                                    ≡⟨ trans-assoc _ _ _ ⟩
         trans (c a₀ a₀) (trans (c a₀ a) (c₁ a))                                    ≡⟨ cong (trans _) $ d₁ _ _ ⟩
         trans (c a₀ a₀) (c₁ a₀)                                                    ≡⟨ d₃ ⟩∎
         c₂                                                                         ∎)) ⟩

    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                               ↝⟨ rearrangement-lemma a₀ ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₂ : (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     trans (c a₀ a₀) (c₁ a₀) ≡ c₂)                                       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∃-cong λ _ → ∃-cong λ d₂ → drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               propositional⇒inhabited⇒contractible
                                                                                (B-groupoid)
                                                                                (d₂ _)) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₂ : (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂) →
     ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁)                          ↝⟨ (∃-cong λ _ → ∃-cong λ c → ∃-cong λ d → ∃-cong λ _ → ∃-cong λ c₂ →
                                                                             ∃-cong λ c₁ → drop-⊤-right λ d₂ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               propositional⇒inhabited⇒contractible
                                                                                (Π-closure (lower-extensionality _ ℓ       ext) 1 λ _ →
                                                                                Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 1 λ _ →
                                                                                B-groupoid)
                                                                                (λ a₁ a₂ →
         trans (c a₁ a₂) (c₁ a₂)                                                    ≡⟨ cong₂ trans (sym $ d _ _ _)
                                                                                (≡⇒↝ implication
                                                                                ([trans≡]≡[≡trans-symˡ] _ _ _) (d₂ _)) ⟩
         trans (trans (c a₁ a₀) (c a₀ a₂)) (trans (sym (c a₀ a₂)) c₂)               ≡⟨ sym $ trans-assoc _ _ _ ⟩
         trans (trans (trans (c a₁ a₀) (c a₀ a₂)) (sym (c a₀ a₂))) c₂               ≡⟨ cong (flip trans _) $ trans-[trans]-sym _ _ ⟩
         trans (c a₁ a₀) c₂                                                         ≡⟨ cong (trans _) $ sym $ d₂ _ ⟩
         trans (c a₁ a₀) (trans (c a₀ a₁) (c₁ a₁))                                  ≡⟨ sym $ trans-assoc _ _ _ ⟩
         trans (trans (c a₁ a₀) (c a₀ a₁)) (c₁ a₁)                                  ≡⟨ cong (flip trans _) $ d _ _ _ ⟩
         trans (c a₁ a₁) (c₁ a₁)                                                    ≡⟨ cong (flip trans _) $
                                                                                Groupoid.idempotent⇒≡id (EG.groupoid _) (d _ _ _) ⟩
         trans (refl _) (c₁ a₁)                                                     ≡⟨ trans-reflˡ _ ⟩∎
         c₁ a₁                                                                      ∎)) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                               ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             inverse ΠΣ-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     (a : A) → ∃ λ (c₁ : f a ≡ f₁) → trans (c a₀ a) c₁ ≡ c₂)             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∀-cong (lower-extensionality _ (a ⊔ ℓ) ext) λ _ → ∃-cong λ _ →
                                                                             ≡⇒↝ _ $ [trans≡]≡[≡trans-symˡ] _ _ _) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     (a : A) → ∃ λ (c₁ : f a ≡ f₁) → c₁ ≡ trans (sym (c a₀ a)) c₂)       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 0 λ _ →
                                                                               singleton-contractible _) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → f a₀ ≡ f₁)                                           ↝⟨ (∃-cong λ _ → ∃-cong λ _ → drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               other-singleton-contractible _) ⟩□
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃)                   □)

  -- An alternative implementation of the forward component of the
  -- equivalence above (with shorter proofs).

  to : B → ∃ λ (f : A → B) → Coherently-constant f
  to b =
      (λ _ → b)
    , (λ _ _ → refl b)
    , (λ _ _ _ → trans-refl-refl)

  to-is-an-equivalence : A → Is-equivalence to
  to-is-an-equivalence a₀ =
    Eq.respects-extensional-equality
      (λ b →
         Σ-≡,≡→≡ (refl _) $
         Σ-≡,≡→≡
           (proj₁ (subst Coherently-constant
                         (refl _)
                         (proj₂ (_≃_.to (equivalence₁ a₀) b)))  ≡⟨ cong proj₁ $ subst-refl Coherently-constant _ ⟩

            (λ _ _ → trans (refl b) (sym (refl b)))             ≡⟨ (apply-ext (lower-extensionality _ ℓ       ext) λ _ →
                                                                    apply-ext (lower-extensionality _ (a ⊔ ℓ) ext) λ _ →
                                                                    trans-symʳ _) ⟩∎
            (λ _ _ → refl b)                                    ∎)
           ((Π-closure (lower-extensionality _ ℓ       ext) 1 λ _ →
             Π-closure (lower-extensionality _ ℓ       ext) 1 λ _ →
             Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 1 λ _ →
             B-groupoid) _ _))
      (_≃_.is-equivalence (equivalence₁ a₀))

  -- The forward component of the equivalence above does not depend on
  -- the value a₀ of type A, so it suffices to assume that A is merely
  -- inhabited.

  equivalence₂ :
    ∥ A ∥ 1 ℓ′ → (B ≃ ∃ λ (f : A → B) → Coherently-constant f)
  equivalence₂ ∥a∥ =
    Eq.⟨ to
       , rec 1
             (Eq.propositional (lower-extensionality _ ℓ ext) _)
             to-is-an-equivalence
             (with-lower-level ℓ 1 ∥a∥)
       ⟩

-- Having a constant function into a set is equivalent to having a
-- function from a propositionally truncated type into the set
-- (assuming extensionality). The statement of this result is that of
-- Proposition 2.2 in "The General Universal Property of the
-- Propositional Truncation" by Kraus, but it uses a different proof:
-- as observed by Kraus this result follows from Proposition 2.3.

constant-function≃∥inhabited∥⇒inhabited :
  ∀ {a b} ℓ {A : Type a} {B : Type b} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →
  Is-set B →
  (∃ λ (f : A → B) → Constant f) ≃ (∥ A ∥ 1 (a ⊔ b ⊔ ℓ) → B)
constant-function≃∥inhabited∥⇒inhabited {a} {b} ℓ {A} {B} ext B-set =
  (∃ λ (f : A → B) → Constant f)             ↔⟨ (∃-cong λ f → inverse $ drop-⊤-right λ c →
                                                 _⇔_.to contractible⇔↔⊤ $
                                                   Π-closure (lower-extensionality _ ℓ       ext) 0 λ _ →
                                                   Π-closure (lower-extensionality _ ℓ       ext) 0 λ _ →
                                                   Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 0 λ _ →
                                                   +⇒≡ B-set) ⟩
  (∃ λ (f : A → B) → Coherently-constant f)  ↝⟨ coherently-constant-function≃∥inhabited∥⇒inhabited ℓ ext (mono₁ 2 B-set) ⟩□
  (∥ A ∥ 1 (a ⊔ b ⊔ ℓ) → B)                  □

private

  -- One direction of the proposition above computes in the right way.

  to-constant-function≃∥inhabited∥⇒inhabited :
    ∀ {a b} ℓ {A : Type a} {B : Type b}
    (ext : Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ))
    (B-set : Is-set B)
    (f : ∃ λ (f : A → B) → Constant f) (x : A) →
    _≃_.to (constant-function≃∥inhabited∥⇒inhabited ℓ ext B-set)
      f ∣ x ∣₁ ≡ proj₁ f x
  to-constant-function≃∥inhabited∥⇒inhabited _ _ _ _ _ = refl _

-- The propositional truncation's universal property (defined using
-- extensionality).
--
-- As observed by Kraus this result follows from Proposition 2.2 in
-- his "The General Universal Property of the Propositional
-- Truncation".

universal-property :
  ∀ {a b} ℓ {A : Type a} {B : Type b} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →
  Is-proposition B →
  (∥ A ∥ 1 (a ⊔ b ⊔ ℓ) → B) ≃ (A → B)
universal-property {a = a} {b} ℓ {A} {B} ext B-prop =
  Eq.with-other-function
    ((∥ A ∥ 1 (a ⊔ b ⊔ ℓ) → B)       ↝⟨ inverse $ constant-function≃∥inhabited∥⇒inhabited ℓ ext (mono₁ 1 B-prop) ⟩
     (∃ λ (f : A → B) → Constant f)  ↔⟨ (drop-⊤-right λ _ →
                                         _⇔_.to contractible⇔↔⊤ $
                                         Π-closure (lower-extensionality _ ℓ       ext) 0 λ _ →
                                         Π-closure (lower-extensionality _ (a ⊔ ℓ) ext) 0 λ _ →
                                         +⇒≡ B-prop) ⟩□
     (A → B)                         □)

    (_∘ ∣_∣₁)

    (λ f → apply-ext (lower-extensionality _ (a ⊔ ℓ) ext) λ x →
       subst (const B) (refl x) (f ∣ x ∣₁)  ≡⟨ subst-refl _ _ ⟩∎
       f ∣ x ∣₁                             ∎)

private

  -- The universal property computes in the right way.

  to-universal-property :
    ∀ {a b} ℓ {A : Type a} {B : Type b}
    (ext : Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ))
    (B-prop : Is-proposition B)
    (f : ∥ A ∥ 1 (a ⊔ b ⊔ ℓ) → B) →
    _≃_.to (universal-property ℓ ext B-prop) f ≡ f ∘ ∣_∣₁
  to-universal-property _ _ _ _ = refl _

  from-universal-property :
    ∀ {a b} ℓ {A : Type a} {B : Type b}
    (ext : Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ))
    (B-prop : Is-proposition B)
    (f : A → B) (x : A) →
    _≃_.from (universal-property ℓ ext B-prop) f ∣ x ∣₁ ≡ f x
  from-universal-property _ _ _ _ _ = refl _

-- Some properties of an imagined "real" /propositional/ truncation.

module Real-propositional-truncation
  (∥_∥ʳ : ∀ {a} → Type a → Type a)
  (∣_∣ʳ : ∀ {a} {A : Type a} → A → ∥ A ∥ʳ)
  (truncation-is-proposition :
     ∀ {a} {A : Type a} → Is-proposition ∥ A ∥ʳ)
  (recʳ :
    ∀ {a b} {A : Type a} {B : Type b} →
    Is-proposition B →
    (A → B) → ∥ A ∥ʳ → B)
  where

  -- The function recʳ can be used to define a dependently typed
  -- eliminator (assuming extensionality).

  elimʳ :
    ∀ {a p} {A : Type a} →
    Extensionality a p →
    (P : ∥ A ∥ʳ → Type p) →
    (∀ x → Is-proposition (P x)) →
    ((x : A) → P ∣ x ∣ʳ) →
    (x : ∥ A ∥ʳ) → P x
  elimʳ {A = A} ext P P-prop f x =
    recʳ {A = A}
         {B = ∀ x → P x}
         (Π-closure ext 1 P-prop)
         (λ x _ → subst P
                        (truncation-is-proposition _ _)
                        (f x))
         x
         x

  -- The eliminator gives the right result, up to propositional
  -- equality, when applied to ∣ x ∣ʳ.

  elimʳ-∣∣ʳ :
    ∀ {a p} {A : Type a}
    (ext : Extensionality a p)
    (P : ∥ A ∥ʳ → Type p)
    (P-prop : ∀ x → Is-proposition (P x))
    (f : (x : A) → P ∣ x ∣ʳ)
    (x : A) →
    elimʳ ext P P-prop f ∣ x ∣ʳ ≡ f x
  elimʳ-∣∣ʳ ext P P-prop f x =
    P-prop _ _ _

  -- The "real" propositional truncation is isomorphic to the one
  -- defined above (assuming extensionality).

  isomorphic :
    ∀ {ℓ a} {A : Type a} →
    Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ ℓ) →
    ∥ A ∥ʳ ↔ ∥ A ∥ 1 (a ⊔ ℓ)
  isomorphic {ℓ} ext = record
    { surjection = record
      { logical-equivalence = record
        { to   = recʳ (truncation-has-correct-h-level 1 ext) ∣_∣₁
        ; from = lower {ℓ = ℓ} ∘
                 rec 1
                     (↑-closure 1 truncation-is-proposition)
                     (lift ∘ ∣_∣ʳ)
        }
      ; right-inverse-of = λ _ →
          truncation-has-correct-h-level 1 ext _ _
      }
    ; left-inverse-of = λ _ → truncation-is-proposition _ _
    }

-- The axiom of choice, in one of the alternative forms given in the
-- HoTT book (§3.8).
--
-- The HoTT book uses a "real" propositional truncation, rather than
-- the defined one used here. Note that I don't know if the universe
-- levels used below (b ⊔ ℓ and a ⊔ b ⊔ ℓ) make sense. However, in the
-- presence of a "real" propositional truncation (and extensionality)
-- they can be dropped (see Real-propositional-truncation.isomorphic).

Axiom-of-choice : (a b ℓ : Level) → Type (lsuc (a ⊔ b ⊔ ℓ))
Axiom-of-choice a b ℓ =
  {A : Type a} {B : A → Type b} →
  Is-set A → (∀ x → ∥ B x ∥ 1 (b ⊔ ℓ)) → ∥ (∀ x → B x) ∥ 1 (a ⊔ b ⊔ ℓ)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import lib.Basics
open import lib.types.Truncation
open import lib.types.Groupoid
open import lib.types.PathSet

module lib.groupoids.FundamentalPreGroupoid {i} (A : Type i) where

  fundamental-pregroupoid : PreGroupoid i i
  fundamental-pregroupoid = record
    { El = A
    ; Arr = _=₀_ {A = A}
    ; Arr-level = λ _ _ → Trunc-level
    ; groupoid-struct = record
      { ident = idp₀
      ; inv = !₀
      ; comp = _∙₀_
      ; unit-l = ∙₀-unit-l
      ; assoc = ∙₀-assoc
      ; inv-l = !₀-inv-l
      }
    }

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda