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

module Cubical.Data.Nat.Omniscience where

open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

open import Cubical.Data.Bool
  renaming (Bool to 𝟚; Bool→Type to ⟨_⟩)
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order.Recursive

open import Cubical.Relation.Nullary

open import Cubical.Axiom.Omniscience

variable
  ℓ : Level
  A : Type ℓ
  F : A → Type ℓ

module _ where
  open Minimal

  never-least→never : (∀ m → ¬ Least F m) → (∀ m → ¬ F m)
  never-least→never ¬LF = wf-elim (flip ∘ curry ∘ ¬LF)

  never→never-least : (∀ m → ¬ F m) → (∀ m → ¬ Least F m)
  never→never-least ¬F m (Fm , _) = ¬F m Fm

  ¬least-wlpo : (∀(P : ℕ → 𝟚) → Dec (∀ x → ¬ Least (⟨_⟩ ∘ P) x)) → WLPO ℕ
  ¬least-wlpo lwlpo P = mapDec never-least→never (_∘ never→never-least) (lwlpo P)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{- Category of categories -}
module CategoryTheory.Instances.Cat where

open import CategoryTheory.Categories
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans

-- Category of categories
ℂat : ∀{n} -> Category (lsuc n)
ℂat {n} = record
        { obj = Category n
        ; _~>_ = Functor
        ; id = I
        ; _∘_ = _◯_
        ; _≈_ = _⟺_
        ; id-left = id-left-ℂat
        ; id-right = id-right-ℂat
        ; ∘-assoc = λ {𝔸} {𝔹} {ℂ} {𝔻} {H} {G} {F} ->
                        ∘-assoc-ℂat {𝔸} {𝔹} {ℂ} {𝔻} {F} {G} {H}
        ; ≈-equiv = ⟺-equiv
        ; ≈-cong = ≈-cong-ℂat
        }
    where
        id-left-ℂat : {ℂ 𝔻 : Category n} {F : Functor ℂ 𝔻} -> (I ◯ F) ⟺ F
        id-left-ℂat {ℂ} {𝔻} {F} = record
            { to = record
                { at = λ A -> F.fmap ℂ.id
                ; nat-cond =  λ {A} {B} {f} ->
                    begin
                        F.fmap f ∘ F.fmap ℂ.id
                    ≈⟨ ≈-cong-right (F.fmap-id) ⟩
                        F.fmap f ∘ id
                    ≈⟨ id-comm ⟩
                        id ∘ Functor.fmap (I ◯ F) f
                    ≈⟨ ≈-cong-left (F.fmap-id [sym]) ⟩
                        F.fmap ℂ.id ∘ Functor.fmap (I ◯ F) f
                    ∎
                }
            ; from = record {
                at = λ A -> F.fmap ℂ.id
                ; nat-cond =  λ {A} {B} {f} ->
                    begin
                        Functor.fmap (I ◯ F) f ∘ F.fmap ℂ.id
                    ≈⟨ ≈-cong-right (F.fmap-id) ⟩
                        Functor.fmap (I ◯ F) f ∘ id
                    ≈⟨ id-comm ⟩
                        id ∘ F.fmap f
                    ≈⟨ ≈-cong-left (F.fmap-id [sym]) ⟩
                        F.fmap ℂ.id ∘ F.fmap f
                    ∎
                }
            ; iso1 = iso-proof
            ; iso2 = iso-proof }
            where
            open import Relation.Binary using (IsEquivalence)
            private module F = Functor F
            private module ℂ = Category ℂ
            open Category 𝔻

            iso-proof : ∀{A : ℂ.obj} -> F.fmap (ℂ.id {A}) ∘ F.fmap ℂ.id ≈ id
            iso-proof =
                begin
                    F.fmap ℂ.id ∘ F.fmap ℂ.id
                ≈⟨ ≈-cong F.fmap-id F.fmap-id ⟩
                    id ∘ id
                ≈⟨ id-left ⟩
                    id
                ∎

        id-right-ℂat : {ℂ 𝔻 : Category n} {F : Functor ℂ 𝔻} -> (F ◯ I) ⟺ F
        id-right-ℂat {ℂ} {𝔻} {F} = record
            { to = record
                { at = λ A -> F.fmap ℂ.id
                ; nat-cond =  λ {A} {B} {f} ->
                    begin
                        F.fmap f ∘ F.fmap ℂ.id
                    ≈⟨ ≈-cong-right (F.fmap-id) ⟩
                        F.fmap f ∘ id
                    ≈⟨ id-comm ⟩
                        id ∘ Functor.fmap (F ◯ I) f
                    ≈⟨ ≈-cong-left (F.fmap-id [sym]) ⟩
                        F.fmap ℂ.id ∘ Functor.fmap (F ◯ I) f
                    ∎
                }
            ; from = record {
                at = λ A -> F.fmap ℂ.id
                ; nat-cond =  λ {A} {B} {f} ->
                    begin
                        Functor.fmap (F ◯ I) f ∘ F.fmap ℂ.id
                    ≈⟨ ≈-cong-right (F.fmap-id) ⟩
                        Functor.fmap (F ◯ I) f ∘ id
                    ≈⟨ id-right ⟩
                        Functor.fmap (F ◯ I) f
                    ≈⟨ id-left [sym] ⟩
                        id ∘ F.fmap f
                    ≈⟨ ≈-cong-left (F.fmap-id [sym]) ⟩
                        F.fmap ℂ.id ∘ F.fmap f
                    ∎
                }
            ; iso1 = iso-proof
            ; iso2 = iso-proof }
            where
            open import Relation.Binary using (IsEquivalence)
            private module F = Functor F
            private module ℂ = Category ℂ
            open Category 𝔻

            iso-proof : ∀{A : ℂ.obj} -> F.fmap (ℂ.id {A}) ∘ F.fmap ℂ.id ≈ id
            iso-proof =
                begin
                    F.fmap ℂ.id ∘ F.fmap ℂ.id
                ≈⟨ ≈-cong F.fmap-id F.fmap-id ⟩
                    id ∘ id
                ≈⟨ id-left ⟩
                    id
                ∎

        ∘-assoc-ℂat : {𝔸 𝔹 ℂ 𝔻 : Category n} {F : Functor 𝔸 𝔹}
                      {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻}
                   -> (H ◯ G) ◯ F ⟺ H ◯ (G ◯ F)
        ∘-assoc-ℂat {𝔸} {𝔹} {ℂ} {𝔻} {F} {G} {H} = record
            { to = record
                { at = λ A -> Functor.fmap (H ◯ (G ◯ F)) 𝔸.id
                ; nat-cond = λ {A} {B} {f} ->
                    begin
                        Functor.fmap (H ◯ (G ◯ F)) f ∘ Functor.fmap (H ◯ (G ◯ F)) 𝔸.id
                    ≈⟨ ≈-cong-right (Functor.fmap-id (H ◯ (G ◯ F))) ⟩
                        Functor.fmap (H ◯ (G ◯ F)) f ∘ id
                    ≈⟨ id-comm ⟩
                        id ∘ Functor.fmap (H ◯ G ◯ F) f
                    ≈⟨ ≈-cong-left (Functor.fmap-id ((H ◯ G) ◯ F) [sym]) ⟩
                        Functor.fmap (H ◯ G ◯ F) 𝔸.id ∘ Functor.fmap (H ◯ G ◯ F) f
                    ∎
                }
            ; from = record
                { at = λ A -> Functor.fmap ((H ◯ G) ◯ F) 𝔸.id
                ; nat-cond = λ {A} {B} {f} ->
                    begin
                        Functor.fmap (H ◯ (G ◯ F)) f ∘ Functor.fmap ((H ◯ G) ◯ F) 𝔸.id
                    ≈⟨ ≈-cong-right (Functor.fmap-id ((H ◯ G) ◯ F)) ⟩
                        Functor.fmap (H ◯ (G ◯ F)) f ∘ id
                    ≈⟨ id-comm ⟩
                        id ∘ Functor.fmap (H ◯ G ◯ F) f
                    ≈⟨ ≈-cong-left (Functor.fmap-id ((H ◯ G) ◯ F) [sym]) ⟩
                        Functor.fmap (H ◯ G ◯ F) 𝔸.id ∘ Functor.fmap (H ◯ G ◯ F) f
                    ∎
                }
            ; iso1 = iso-proof

            ; iso2 = iso-proof
            }
            where
            open import Relation.Binary using (IsEquivalence)
            private module F = Functor F
            private module G = Functor G
            private module H = Functor H
            private module 𝔸 = Category 𝔸
            private module 𝔹 = Category 𝔹
            private module ℂ = Category ℂ
            open Category 𝔻

            iso-proof : ∀{A : 𝔸.obj}
                     ->  Functor.fmap ((H ◯ G) ◯ F) (𝔸.id {A}) ∘ Functor.fmap (H ◯ (G ◯ F)) 𝔸.id
                     ≈ id
            iso-proof =
                begin
                    Functor.fmap ((H ◯ G) ◯ F) 𝔸.id ∘ Functor.fmap (H ◯ (G ◯ F)) 𝔸.id
                ≈⟨ ≈-cong (Functor.fmap-id ((H ◯ G) ◯ F)) (Functor.fmap-id (H ◯ (G ◯ F))) ⟩
                    id ∘ id
                ≈⟨ id-left ⟩
                    id
                ∎

        ≈-cong-ℂat : {𝔸 𝔹 ℂ : Category n} {F F′ : Functor 𝔸 𝔹} {G G′ : Functor 𝔹 ℂ}
                  -> F ⟺ F′ -> G ⟺ G′ -> (G ◯ F) ⟺ (G′ ◯ F′)
        ≈-cong-ℂat {𝔸}{𝔹}{ℂ}{F}{F′}{G}{G′} F⟺F′ G⟺G′ = record
            { to = record
                { at = λ A -> at G⟺G′.to (F′.omap A) ∘ G.fmap (at F⟺F′.to A)
                ; nat-cond = λ {A} {B} {f} ->
                    begin
                        Functor.fmap (G′ ◯ F′) f ∘ (at G⟺G′.to (F′.omap A) ∘ G.fmap (at F⟺F′.to A))
                    ≈⟨ ∘-assoc [sym] ≈> ≈-cong-left (nat-cond (G⟺G′.to))⟩
                        (at G⟺G′.to (F′.omap B) ∘ Functor.fmap (G ◯ F′) f) ∘ G.fmap (at F⟺F′.to A)
                    ≈⟨ ∘-assoc ≈> ≈-cong-right (G.fmap-∘ [sym])⟩
                        at G⟺G′.to (F′.omap B) ∘ G.fmap (F′.fmap f 𝔹.∘ at F⟺F′.to A)
                    ≈⟨ ≈-cong-right (G.fmap-cong (nat-cond (F⟺F′.to))) ⟩
                        at G⟺G′.to (F′.omap B) ∘ G.fmap (at F⟺F′.to B 𝔹.∘ F.fmap f)
                    ≈⟨ ≈-cong-right (G.fmap-∘) ⟩
                        at G⟺G′.to (F′.omap B) ∘ (G.fmap (at F⟺F′.to B) ∘ Functor.fmap (G ◯ F) f)
                    ≈⟨ ∘-assoc [sym] ⟩
                        (at G⟺G′.to (F′.omap B) ∘ G.fmap (at F⟺F′.to B)) ∘ Functor.fmap (G ◯ F) f
                    ∎
                }
            ; from = record
                { at = λ A -> at G⟺G′.from (F.omap A) ∘ G′.fmap (at F⟺F′.from A)
                ; nat-cond = λ {A} {B} {f} ->
                    begin
                        Functor.fmap (G ◯ F) f ∘ (at G⟺G′.from (F.omap A) ∘ G′.fmap (at F⟺F′.from A))
                    ≈⟨ ∘-assoc [sym] ≈> ≈-cong-left (nat-cond (G⟺G′.from)) ⟩
                        (at G⟺G′.from (F.omap B) ∘ Functor.fmap (G′ ◯ F) f) ∘ G′.fmap (at F⟺F′.from A)
                    ≈⟨ ∘-assoc ≈> ≈-cong-right (G′.fmap-∘ [sym])⟩
                        at G⟺G′.from (F.omap B) ∘ G′.fmap (F.fmap f 𝔹.∘ at F⟺F′.from A)
                    ≈⟨ ≈-cong-right (G′.fmap-cong (nat-cond (F⟺F′.from))) ⟩
                        at G⟺G′.from (F.omap B) ∘ G′.fmap (at F⟺F′.from B 𝔹.∘ F′.fmap f)
                    ≈⟨ ≈-cong-right (G′.fmap-∘) ⟩
                        at G⟺G′.from (F.omap B) ∘ (G′.fmap (at F⟺F′.from B) ∘ Functor.fmap (G′ ◯ F′) f)
                    ≈⟨ ∘-assoc [sym] ⟩
                        (at G⟺G′.from (F.omap B) ∘ G′.fmap (at F⟺F′.from B)) ∘ Functor.fmap (G′ ◯ F′) f
                    ∎
                }
            ; iso1 = λ {A} ->
                begin
                    (at G⟺G′.from (F.omap A) ∘ G′.fmap (at F⟺F′.from A)) ∘
                    (at G⟺G′.to (F′.omap A) ∘ G.fmap (at F⟺F′.to A))
                ≈⟨ ≈-cong-left (nat-cond G⟺G′.from [sym]) ⟩
                    (G.fmap (at F⟺F′.from A) ∘ at G⟺G′.from ((F′.omap A))) ∘
                    (at G⟺G′.to (F′.omap A) ∘ G.fmap (at F⟺F′.to A))
                ≈⟨ ∘-assoc [sym] ≈> ≈-cong-left (∘-assoc) ⟩
                    (G.fmap (at F⟺F′.from A) ∘
                        (at G⟺G′.from ((F′.omap A)) ∘ at G⟺G′.to (F′.omap A))) ∘
                    G.fmap (at F⟺F′.to A)
                ≈⟨ ≈-cong-left (≈-cong-right (G⟺G′.iso1)) ⟩
                    (G.fmap (at F⟺F′.from A) ∘
                        id) ∘
                    G.fmap (at F⟺F′.to A)
                ≈⟨ ≈-cong-left (id-right) ⟩
                    G.fmap (at F⟺F′.from A) ∘
                    G.fmap (at F⟺F′.to A)
                ≈⟨ G.fmap-∘ [sym] ⟩
                    G.fmap (at F⟺F′.from A 𝔹.∘ at F⟺F′.to A)
                ≈⟨ G.fmap-cong (F⟺F′.iso1) ⟩
                    G.fmap 𝔹.id
                ≈⟨ G.fmap-id ⟩
                    id
                ∎
            ; iso2 = λ {A} ->
                begin
                    (at G⟺G′.to (F′.omap A) ∘ G.fmap (at F⟺F′.to A)) ∘
                    (at G⟺G′.from (F.omap A) ∘ G′.fmap (at F⟺F′.from A))
                ≈⟨ ≈-cong-left (nat-cond G⟺G′.to [sym]) ⟩
                    (G′.fmap (at F⟺F′.to A) ∘ at G⟺G′.to ((F.omap A))) ∘
                    (at G⟺G′.from (F.omap A) ∘ G′.fmap (at F⟺F′.from A))
                ≈⟨ ∘-assoc [sym] ≈> ≈-cong-left (∘-assoc) ⟩
                    (G′.fmap (at F⟺F′.to A) ∘
                        (at G⟺G′.to ((F.omap A)) ∘ at G⟺G′.from (F.omap A))) ∘
                    G′.fmap (at F⟺F′.from A)
                ≈⟨ ≈-cong-left (≈-cong-right (G⟺G′.iso2)) ⟩
                    (G′.fmap (at F⟺F′.to A) ∘
                        id) ∘
                    G′.fmap (at F⟺F′.from A)
                ≈⟨ ≈-cong-left (id-right) ⟩
                    G′.fmap (at F⟺F′.to A) ∘
                    G′.fmap (at F⟺F′.from A)
                ≈⟨ G′.fmap-∘ [sym] ⟩
                    G′.fmap (at F⟺F′.to A 𝔹.∘ at F⟺F′.from A)
                ≈⟨ G′.fmap-cong (F⟺F′.iso2) ⟩
                    G′.fmap 𝔹.id
                ≈⟨ G′.fmap-id ⟩
                    id
                ∎
            }
            where
            private module F = Functor F
            private module F′ = Functor F′
            private module G = Functor G
            private module G′ = Functor G′
            private module 𝔸 = Category 𝔸
            private module 𝔹 = Category 𝔹
            open Category ℂ
            open _⟹_
            open _⟺_
            private module F⟺F′ = _⟺_ F⟺F′
            private module G⟺G′ = _⟺_ G⟺G′

ext: agda

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module PartiallyAppliedConstructorInIndex where

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

data D : (Nat -> Nat) -> Set where
  c : D suc
  d : (x : Nat) -> D (plus x)
  e : D (\ x -> suc x)

f : D suc -> Nat
f c = zero
f e = suc zero

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


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

module Agda.Builtin.Bool where

data Bool : Set where
  false true : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN FALSE false #-}
{-# BUILTIN TRUE  true  #-}

{-# COMPILE UHC Bool = data __BOOL__ (__FALSE__ | __TRUE__) #-}

{-# COMPILE JS Bool  = function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-}
{-# COMPILE JS false = false #-}
{-# COMPILE JS true  = true  #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module _ where

q : ?
q = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Relator.Equals.Category where

import      Data.Tuple as Tuple
open import Functional as Fn using (_$_)
open import Functional.Dependent using () renaming (_∘_ to _∘ᶠ_)
open import Logic.Predicate
import      Lvl
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Categorical.Properties
import      Structure.Category.Functor as Category
open import Structure.Category.Monad
open import Structure.Category.NaturalTransformation
open import Structure.Category
open import Structure.Function
open import Structure.Groupoid
import      Structure.Groupoid.Functor as Groupoid
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Relator
open import Syntax.Transitivity
open import Type.Category.IntensionalFunctionsCategory
open import Type.Identity
open import Type

private variable ℓ : Lvl.Level
private variable T A B Obj : Type{ℓ}
private variable f g : A → B
private variable P : T → Type{ℓ}
private variable x y z : T
private variable p : Id x y
private variable _⟶_ : Obj → Obj → Type{ℓ}

-- The inhabitants of a type together with the the inhabitants of the identity type forms a groupoid.
-- An object is an inhabitant of a certain type, and a morphism is a proof of identity between two objects.
identityTypeGroupoid : Groupoid{Obj = T} (Id)
Groupoid._∘_ identityTypeGroupoid = Fn.swap(transitivity(Id))
Groupoid.id  identityTypeGroupoid = reflexivity(Id)
Groupoid.inv identityTypeGroupoid = symmetry(Id)
Morphism.Associativity.proof              (Groupoid.associativity identityTypeGroupoid) {x = _} {x = intro} {y = intro} {z = intro} = intro
Morphism.Identityₗ.proof     (Tuple.left  (Groupoid.identity      identityTypeGroupoid)) {f = intro} = intro
Morphism.Identityᵣ.proof     (Tuple.right (Groupoid.identity      identityTypeGroupoid)) {f = intro} = intro
Polymorphism.Inverterₗ.proof (Tuple.left  (Groupoid.inverter      identityTypeGroupoid)) {f = intro} = intro
Polymorphism.Inverterᵣ.proof (Tuple.right (Groupoid.inverter      identityTypeGroupoid)) {f = intro} = intro

identityTypeCategory : Category{Obj = T} (Id)
identityTypeCategory = Groupoid.category identityTypeGroupoid

-- TODO: Generalize and move this to Structure.Categorical.Proofs
inverse-of-identity : ∀{grp : Groupoid(_⟶_)}{x} → (Groupoid.inv grp (Groupoid.id grp {x}) ≡ Groupoid.id grp)
inverse-of-identity {grp = grp} =
  inv(id)      🝖[ Id ]-[ Morphism.identityᵣ(_∘_)(id) ]-sym
  inv(id) ∘ id 🝖[ Id ]-[ Morphism.inverseₗ(_∘_)(id)(id)(inv id) ]
  id           🝖[ Id ]-end
  where open Structure.Groupoid.Groupoid(grp)

idTransportFunctor : ∀{grp : Groupoid(_⟶_)} → Groupoid.Functor(identityTypeGroupoid)(grp) Fn.id
Groupoid.Functor.map (idTransportFunctor{_⟶_ = _⟶_}{grp = grp}) = sub₂(Id)(_⟶_) where instance _ = Groupoid.morphism-reflexivity grp
Groupoid.Functor.op-preserving (idTransportFunctor{grp = grp}) {f = intro} {g = intro} = symmetry(Id) (Morphism.Identityₗ.proof (Tuple.left (Groupoid.identity grp)))
Groupoid.Functor.inv-preserving (idTransportFunctor{_⟶_ = _⟶_}{grp = grp}) {f = intro} =
  sub₂(Id)(_⟶_) (symmetry(Id) (reflexivity(Id))) 🝖[ Id ]-[]
  sub₂(Id)(_⟶_) (reflexivity(Id))                🝖[ Id ]-[]
  id                                             🝖[ Id ]-[ inverse-of-identity{grp = grp} ]-sym
  inv(id)                                        🝖[ Id ]-[]
  inv(sub₂(Id)(_⟶_) (reflexivity(Id)))           🝖-end
  where
    instance _ = Groupoid.morphism-reflexivity grp
    open Structure.Groupoid.Groupoid(grp)
Groupoid.Functor.id-preserving idTransportFunctor = intro

-- A functor in the identity type groupoid is a function and a proof of it being a function (compatibility with the identity relation, or in other words, respecting the congruence property).
-- Note: It does not neccessarily have to be an endofunctor because different objects (types) can be chosen for the respective groupoids.
functionFunctor : Groupoid.Functor(identityTypeGroupoid)(identityTypeGroupoid) f
Groupoid.Functor.map (functionFunctor {f = f}) = congruence₁(f)
Groupoid.Functor.op-preserving  functionFunctor {f = intro} {g = intro} = intro
Groupoid.Functor.inv-preserving functionFunctor {f = intro}             = intro
Groupoid.Functor.id-preserving  functionFunctor                         = intro

-- A functor to the category of types is a predicate and a proof of it being a relation (having the substitution property).
predicateFunctor : Category.Functor(identityTypeCategory)(typeIntensionalFnCategory) P -- TODO: Is it possible to generalize so that the target (now `typeIntensionalFnCategory`) is more general? `idTransportFunctor` seems to be similar. Maybe on the on₂-category to the right?
Category.Functor.map (predicateFunctor{P = P}) = substitute₁(P)
Category.Functor.op-preserving predicateFunctor {x} {.x} {.x} {intro} {intro} = intro
Category.Functor.id-preserving predicateFunctor = intro

-- A natural transformation in the identity type groupoid between two functions (functors of the identity type groupoid) is a proof of them being extensionally identical.
extensionalFnNaturalTransformation : (p : ∀(x) → (f(x) ≡ g(x))) → NaturalTransformation([∃]-intro f ⦃ Groupoid.Functor.categoryFunctor functionFunctor ⦄) ([∃]-intro g ⦃ Groupoid.Functor.categoryFunctor functionFunctor ⦄) p
NaturalTransformation.natural (extensionalFnNaturalTransformation {f = f} {g = g} p) {x} {.x} {intro} =
  congruence₁(f) intro 🝖 p(x) 🝖-[ Morphism.Identityᵣ.proof (Tuple.right (Category.identity identityTypeCategory)) ]
  p(x)                        🝖-[ Morphism.Identityₗ.proof (Tuple.left  (Category.identity identityTypeCategory)) ]-sym
  p(x) 🝖 congruence₁(g) intro 🝖-end

open import Function.Equals
open import Function.Proofs
open import Structure.Function.Domain
open import Structure.Function.Multi
open import Structure.Setoid using (Equiv)

-- A monad in the identity type groupoid is an identity function and a proof of it being that and it being idempotent.
-- The proof that it behaves the same extensionally as an identity function should also preserve congruence.
-- TODO: Instead of (∀{x} → (p(f(x))) ≡ congruence₁(f) (p(x))) , use something like ⦃ preserv : Preserving₁(p)(f)(congruence₁(f)) ⦄ , but it does not work at the moment. Maybe something is dependent here?
identityFunctionMonad : ∀{T : Type{ℓ}}{f : T → T} → (p : ∀(x) → (x ≡ f(x))) → (∀{x} → (p(f(x))) ≡ congruence₁(f) (p(x))) → Monad(f) ⦃ Groupoid.Functor.categoryFunctor functionFunctor ⦄
∃.witness (Monad.Η (identityFunctionMonad p _)) = p
NaturalTransformation.natural (∃.proof (Monad.Η (identityFunctionMonad {f = f} p _))) {x}{.x}{intro} =
  Fn.id intro 🝖 p(x)          🝖[ Id ]-[]
  intro 🝖 p(x)                🝖[ Id ]-[]
  p(x)                        🝖[ Id ]-[ Morphism.Identityₗ.proof (Tuple.left  (Category.identity identityTypeCategory)) ]-sym
  p(x) 🝖 intro                🝖[ Id ]-[]
  p(x) 🝖 congruence₁(f) intro 🝖-end
∃.witness (Monad.Μ (identityFunctionMonad {f = f} p _)) x = symmetry(Id) (congruence₁(f) (p(x)))
NaturalTransformation.natural (∃.proof (Monad.Μ (identityFunctionMonad {f = f} p _))) {x}{.x}{intro} =
  (congruence₁(f) Fn.∘ congruence₁(f)) intro 🝖 symmetry(Id) (congruence₁(f) (p(x)))  🝖[ Id ]-[]
  congruence₁(f) (congruence₁(f) intro) 🝖 symmetry(Id) (congruence₁(f) (p(x)))       🝖[ Id ]-[]
  congruence₁(f) intro 🝖 symmetry(Id) (congruence₁(f) (p(x)))                        🝖[ Id ]-[]
  intro 🝖 symmetry(Id) (congruence₁(f) (p(x)))                                       🝖[ Id ]-[]
  symmetry(Id) (congruence₁(f) (p(x)))                                               🝖[ Id ]-[ Morphism.Identityₗ.proof (Tuple.left  (Category.identity identityTypeCategory)) ]-sym
  symmetry(Id) (congruence₁(f) (p(x))) 🝖 intro                                       🝖[ Id ]-[]
  symmetry(Id) (congruence₁(f) (p(x))) 🝖 congruence₁(f) intro                        🝖-end
_⊜_.proof (Monad.μ-functor-[∘]-commutativity (identityFunctionMonad {f = f} p preserv)) {x} = congruence₂ₗ(_🝖_)(symmetry(Id) (congruence₁(f) (p(x)))) $
  congruence₁(f) (symmetry(Id) (congruence₁(f) (p(x)))) 🝖[ Id ]-[ Groupoid.Functor.inv-preserving (functionFunctor{f = f}) {f = congruence₁(f) (p x)} ]
  symmetry(Id) (congruence₁(f) (congruence₁(f) (p(x)))) 🝖[ Id ]-[ congruence₁(symmetry(Id)) (congruence₁(congruence₁(f)) preserv) ]-sym
  symmetry(Id) (congruence₁(f) (p(f(x))))               🝖-end
_⊜_.proof (Monad.μ-functor-[∘]-identityₗ (identityFunctionMonad {f = f} p preserv)) {x} =
  congruence₁(f) (p(x)) 🝖 symmetry(Id) (congruence₁(f) (p(x))) 🝖[ Id ]-[ congruence₂(Groupoid._∘_ identityTypeGroupoid) (congruence₁(symmetry(Id)) preserv) preserv ]-sym
  p(f(x)) 🝖 symmetry(Id) (p(f(x)))                             🝖[ Id ]-[ Morphism.Inverseₗ.proof (Tuple.left(Groupoid.inverse identityTypeGroupoid {f = p(f x)})) ]
  intro{x = f(x)}                                              🝖-end
_⊜_.proof (Monad.μ-functor-[∘]-identityᵣ (identityFunctionMonad {f = f} p preserv)) {x} =
  p(f(x)) 🝖 symmetry(Id) (congruence₁(f) (p(x))) 🝖[ Id ]-[ congruence₂ᵣ(_🝖_)(p(f(x))) (congruence₁(symmetry(Id)) preserv) ]-sym
  p(f(x)) 🝖 symmetry(Id) (p(f(x)))               🝖[ Id ]-[ Morphism.Inverseₗ.proof (Tuple.left(Groupoid.inverse identityTypeGroupoid {f = p(f x)})) ]
  intro{x = f(x)}                                🝖-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module _ where

module M where

  infixr 3 _!_
  data D : Set₁ where
    _!_ : D → D → D

infixl 3 _!_
data E : Set₁ where
  _!_ : E → E → E

open M

postulate
  [_]E : E → Set
  [_]D : D → Set

fail : ∀ {d e} → [ (d ! d) ! d ]D → [ e ! (e ! e) ]E
fail x = x -- should use the right fixity for the overloaded constructor

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

module Instances where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ)
open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Foundations.Logic
open import Agda.Builtin.Equality  renaming (_≡_ to _≡ᵢ_; refl to reflₚ)

variable
  ℓ ℓ' ℓ'' : Level

-- hProp is just the propertie's target type A with ≡ for all inhabitants attached
_ : (hProp ℓ) ≡ (Σ[ A ∈ Type ℓ ] (∀(x y : A) → x ≡ y))
_ = refl

_ : (hProp ℓ) ≡ (Σ[ A ∈ Type ℓ ] isProp A)
_ = refl

-- PropRel is just the relation R with ≡ for all inhabitants of all target types R a b attached
PropRel' : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
PropRel' A B ℓ' = Σ[ R ∈ Rel A B ℓ' ] ∀ a b → isProp (R a b)

#-coerceₚ' : ∀{ℓ'} → {P Q : hProp ℓ'} → [ P ] → {{[ P ] ≡ [ Q ]}} → [ Q ]
#-coerceₚ' {ℓ} {[p] , p-isProp} {[q] , q-isProp} p {{ p≡q }} = transport p≡q p

path-to-id : ∀{ℓ} {A : Type ℓ} {x y : A} → x ≡ y → x ≡ᵢ y
path-to-id p = {!!}

-- just for the explanation
record PoorField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    F : Type ℓ
    0f 1f : F
    _#_ : Rel F F ℓ'
    #-isprop : ∀ x y → isProp (x # y)
    instance
      #-isprop' : ∀{x y} {p q : x # y} → p ≡ q -- could we use this in some way?

    -- #-rel : PropRel F F ℓ'

  _#ₚ_ : F → F → hProp ℓ'
  x #ₚ y = (x # y) , #-isprop x y

  -- NOTE: this creates a `Goal: fst #-rel ...` everywhere
  --       we might just separate the relation from the isprop
  --       i.e. directly define _#_ and #-isprop
  -- _#_      = fst #-rel
  -- #-isprop = snd #-rel

  -- NOTE: there is an email on the agda mailing list 08.11.18, 21:16 by Martin Escardo "I want implicit coercions in Agda"
  --       although this email thread is about more general coercions which are not straight forward, where hProp should be less of an issue
  #-coerce : ∀{ℓ x y} → ∀{p q} {R : x # y → Type ℓ} → R p → R q
  #-coerce {ℓ} {x} {y} {p} {q} {R} rp = transport (cong R (#-isprop x y p q))rp

  #-coerceₚ : ∀{ℓ x y} → ∀{p q} {R : [ x #ₚ y ] → Type ℓ} → R p → R q
  #-coerceₚ {ℓ} {x} {y} {p} {q} {R} rp = transport (cong R (#-isprop x y p q)) rp

  field
    _+_ _·_ : F → F → F
    _⁻¹ᶠ    : (x : F) → {{ x # 0f }} → F
    ·-rinv  : (x : F) → (p : x # 0f) → x · (_⁻¹ᶠ x {{p}}) ≡ 1f

   -- for the purposes of explanation we just assume two different proofs of `1 # 0`
    1#0     : 1f # 0f
    1#0'    : 1f # 0f

    -- maybe there is some clever way to define _⁻¹ᶠ in a way where it accepts different proofs
    _⁻¹ᶠ'   : (x : F) → {{ [ x #ₚ 0f ] }} → F
    ·-rinv' : (x : F) → (p : [ x #ₚ 0f ]) → x · (_⁻¹ᶠ' x {{p}}) ≡ 1f

    1#0ₚ     : [ 1f #ₚ 0f ]
    1#0ₚ'    : [ 1f #ₚ 0f ]

    _⁻¹ᶠ''   : (x : F) → {{ [ x #ₚ 0f ] }} → F

  -- infix  9 _⁻¹ᶠ
  -- infixl 7 _·_
  -- infixl 5 _+_
  -- infixl 4 _#_

module test-hProp (PF : PoorField {ℓ} {ℓ'}) where
  open PoorField PF

  -- of course, this works
  test0 : let instance _ = 1#0 in 1f · (1f ⁻¹ᶠ) ≡ 1f
  test0 = ·-rinv 1f 1#0

  -- now, we try passing in 1#0'
  test1 : let instance _ = 1#0 in 1f · (1f ⁻¹ᶠ) ≡ 1f
  -- ERROR:
  -- PoorField.1#0' /= PoorField.1#0
  -- when checking that the expression 1#0' has type fst #-rel 1f 0f
  test1 = ·-rinv 1f ( #-coerceₚ {_} {1f} {0f} {_} {_} {_} 1#0')

  -- #-coerce seems to have troubles resolving the R
  test2 : let instance _ = 1#0 in 1f · (1f ⁻¹ᶠ) ≡ 1f
  -- ERROR:
  -- Failed to solve the following constraints:
  -- _R_161 _q_160 =< (1f · (1f ⁻¹ᶠ)) ≡ 1f
  -- (1f · (1f ⁻¹ᶠ)) ≡ 1f =< _R_161 _p_159
  test2 = #-coerce (·-rinv 1f 1#0') -- this line is yellow in emacs

  -- it works when we give R explicitly
  test3 : let instance _ = 1#0 in 1f · (1f ⁻¹ᶠ) ≡ 1f
  test3 = #-coerce {R = λ r → 1f · (_⁻¹ᶠ 1f {{r}}) ≡ 1f} (·-rinv 1f 1#0')

  -- a different "result" of this consideration might be that Goals involving hProp-instances need to be formulated in a different way

  test4 : let instance _ = 1#0ₚ in 1f · (1f ⁻¹ᶠ') ≡ 1f
  test4 =   ·-rinv' 1f ( #-coerceₚ' 1#0ₚ' {{{!!}}} )

  test5 : let instance _ = 1#0ₚ in 1f · (1f ⁻¹ᶠ') ≡ 1f
  test5 with 1#0ₚ' | path-to-id {ℓ'} {x = 1#0ₚ} {y = 1#0ₚ'} (#-isprop 1f 0f 1#0ₚ 1#0ₚ')
  ... | .(PoorField.1#0ₚ PF) | reflₚ = {! ·-rinv' 1f 1#0ₚ' !}

-- when using Prop this would be less of an issue
-- but how does it interact with the hProp based cubical library?
record ImpredicativePoorField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    F : Type ℓ
    0f 1f : F
    _#_ : F → F → Prop ℓ'
    _+_ _·_ : F → F → F
    _⁻¹ᶠ    : (x : F) → {{ x # 0f }} → F
    ·-rinv  : (x : F) → (p : x # 0f) → x · (_⁻¹ᶠ x {{p}}) ≡ 1f

   -- for the purposes of explanation we just assume two different proofs of `1 # 0`
    1#0     : 1f # 0f
    1#0'    : 1f # 0f

module test-impredicative (PF : ImpredicativePoorField {ℓ} {ℓ'}) where
  open ImpredicativePoorField PF

  -- now, we try passing in 1#0'
  test1 : let instance _ = 1#0 in 1f · (1f ⁻¹ᶠ) ≡ 1f
  test1 = ·-rinv 1f 1#0' -- just works

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module Container.List where

open import Prelude

infixr 5 _∷_
data All {a b} {A : Set a} (P : A → Set b) : List A → Set (a ⊔ b) where
  []  : All P []
  _∷_ : ∀ {x xs} (p : P x) (ps : All P xs) → All P (x ∷ xs)

data Any {a b} {A : Set a} (P : A → Set b) : List A → Set (a ⊔ b) where
  instance
    zero : ∀ {x xs} (p : P x) → Any P (x ∷ xs)
    suc  : ∀ {x xs} (i : Any P xs) → Any P (x ∷ xs)

pattern zero! = zero refl

-- Literal overloading for Any
module _ {a b} {A : Set a} {P : A → Set b} where
  private
    AnyConstraint : List A → Nat → Set (a ⊔ b)
    AnyConstraint []        _      = ⊥′
    AnyConstraint (x ∷  _)  zero   = ⊤′ {a} × P x   -- hack to line up levels
    AnyConstraint (_ ∷ xs) (suc i) = AnyConstraint xs i

    natToIx : ∀ (xs : List A) n → {{_ : AnyConstraint xs n}} → Any P xs
    natToIx [] n {{}}
    natToIx (x ∷ xs)  zero {{_ , px}} = zero px
    natToIx (x ∷ xs) (suc n) = suc (natToIx xs n)

  instance
    NumberAny : ∀ {xs} → Number (Any P xs)
    Number.Constraint (NumberAny {xs}) = AnyConstraint xs
    fromNat {{NumberAny {xs}}} = natToIx xs

infix 3 _∈_
_∈_ : ∀ {a} {A : Set a} → A → List A → Set a
x ∈ xs = Any (_≡_ x) xs

forgetAny : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A} → Any P xs → Nat
forgetAny (zero _) = zero
forgetAny (suc  i) = suc (forgetAny i)

lookupAny : ∀ {a b} {A : Set a} {P Q : A → Set b} {xs} → All P xs → Any Q xs → Σ A (λ x → P x × Q x)
lookupAny (p ∷ ps) (zero q) = _ , p , q
lookupAny (p ∷ ps) (suc  i) = lookupAny ps i

lookup∈ : ∀ {a b} {A : Set a} {P : A → Set b} {xs x} → All P xs → x ∈ xs → P x
lookup∈ (p ∷ ps) (zero refl) = p
lookup∈ (p ∷ ps) (suc i)     = lookup∈ ps i

module _ {a b} {A : Set a} {P Q : A → Set b} (f : ∀ {x} → P x → Q x) where
  mapAll : ∀ {xs} → All P xs → All Q xs
  mapAll [] = []
  mapAll (x ∷ xs) = f x ∷ mapAll xs

  mapAny : ∀ {xs} → Any P xs → Any Q xs
  mapAny (zero x) = zero (f x)
  mapAny (suc i)  = suc (mapAny i)

traverseAll : ∀ {a b} {A : Set a} {B : A → Set a} {F : Set a → Set b}
                {{AppF : Applicative F}} →
                (∀ x → F (B x)) → (xs : List A) → F (All B xs)
traverseAll f []       = pure []
traverseAll f (x ∷ xs) = ⦇ f x ∷ traverseAll f xs ⦈

module _ {a b} {A : Set a} {P : A → Set b} where

  -- Append

  infixr 5 _++All_
  _++All_ : ∀ {xs ys} → All P xs → All P ys → All P (xs ++ ys)
  []       ++All qs = qs
  (p ∷ ps) ++All qs = p ∷ ps ++All qs

  -- Delete

  deleteIx : ∀ xs → Any P xs → List A
  deleteIx (_ ∷ xs) (zero _) = xs
  deleteIx (x ∷ xs) (suc  i) = x ∷ deleteIx xs i

  deleteAllIx : ∀ {c} {Q : A → Set c} {xs} → All Q xs → (i : Any P xs) → All Q (deleteIx xs i)
  deleteAllIx (q ∷ qs) (zero _) = qs
  deleteAllIx (q ∷ qs) (suc i)  = q ∷ deleteAllIx qs i

-- Equality --

module _ {a b} {A : Set a} {P : A → Set b} {{EqP : ∀ {x} → Eq (P x)}} where

  private
    z : ∀ {x xs} → P x → Any P (x ∷ xs)
    z = zero

    zero-inj : ∀ {x} {xs : List A} {p q : P x} → Any.zero {xs = xs} p ≡ z q → p ≡ q
    zero-inj refl = refl

    sucAny-inj : ∀ {x xs} {i j : Any P xs} → Any.suc {x = x} i ≡ Any.suc {x = x} j → i ≡ j
    sucAny-inj refl = refl

    cons-inj₁ : ∀ {x xs} {p q : P x} {ps qs : All P xs} → p All.∷ ps ≡ q ∷ qs → p ≡ q
    cons-inj₁ refl = refl

    cons-inj₂ : ∀ {x xs} {p q : P x} {ps qs : All P xs} → p All.∷ ps ≡ q ∷ qs → ps ≡ qs
    cons-inj₂ refl = refl

  instance
    EqAny : ∀ {xs} → Eq (Any P xs)
    _==_ {{EqAny}} (zero p) (zero q) = decEq₁ zero-inj   (p == q)
    _==_ {{EqAny}} (suc i)  (suc j)  = decEq₁ sucAny-inj (i == j)
    _==_ {{EqAny}} (zero _) (suc _)  = no λ ()
    _==_ {{EqAny}} (suc _)  (zero _) = no λ ()

    EqAll : ∀ {xs} → Eq (All P xs)
    _==_ {{EqAll}} []       []       = yes refl
    _==_ {{EqAll}} (x ∷ xs) (y ∷ ys) = decEq₂ cons-inj₁ cons-inj₂ (x == y) (xs == ys)

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
-- 2013-02-21 Andreas
-- ensure that constructor-headedness works also for abstract things
module Issue796 where

data U : Set where
  a b : U

data A : Set where
data B : Set where

abstract
  A' B' : Set

  A' = A
  B' = B  -- fails if changed to A.

  [_] : U → Set
  [_] a = A'
  [_] b = B'

  f : ∀ u → [ u ] → U
  f u _ = u

  postulate x : A'

  zzz = f _ x
  -- succeeds since [_] is constructor headed

max_forks_repo_name: Agda-zh/agda


text:
module Helper.CodeGeneration where

open import Agda.Primitive
open import Data.Nat
open import Data.Fin
open import Data.List
open import Function using (_∘_ ; _$_ ; _∋_)
open import Reflection

a : {A : Set} -> (x : A) -> Arg A
a x = arg (arg-info visible relevant) x

a1 : {A : Set} -> (x : A) -> Arg A
a1 x = arg (arg-info hidden relevant) x

t0 : Term -> Type
t0 t = el (lit 0) t

fin_term : (n : ℕ) -> Term
fin_term zero = con (quote Fin.zero) []
fin_term (suc fin) = con (quote Fin.suc) [ a (fin_term fin) ]

fin_pat : (n : ℕ) -> (l : Pattern) -> Pattern
fin_pat zero l = l
fin_pat (suc n) l = con (quote Fin.suc) [ a (fin_pat n l) ]

fin_type : (n : ℕ) -> Type
fin_type n = t0 (def (quote Fin) [ a (lit (nat n)) ])

-- Annotate terms with a type
_∋-t_ : Term -> Term -> Term
_∋-t_ ty term = def (quote _∋_) (a ty ∷ a term ∷ [])

cons : (n : Name) -> List Name
cons n with (definition n)
cons n | data-type d = reverse (constructors d)
cons n | _ = []

infer_type = el (lit 0) unknown

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


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

module Structure.Operator.Vector.Subspace.Proofs
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {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 Logic.Predicate
open import Logic.Propositional
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 ; _∈_ ; _∪_ ; ⋂ᵢ ; _⊇_ ; _⊆_)
open import Structure.Container.SetLike using (SetElement)
private open module SetLikeFunctionProperties{ℓ} = Structure.Container.SetLike.FunctionProperties{C = PredSet{ℓ}(V)}{E = V}(_∈_)
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Operator.Vector.LinearCombination        ⦃ vectorSpace = vectorSpace ⦄
open import Structure.Operator.Vector.LinearCombination.Proofs
open import Structure.Operator.Vector.Subspace                 ⦃ vectorSpace = vectorSpace ⦄
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable I : Type{ℓ}
private variable n : ℕ
private variable vf : Vec(n)(V)
private variable sf : Vec(n)(S)

-- TODO
[⋂ᵢ]-subspace : ∀{Vsf : I → PredSet{ℓ}(V)} → (∀{i} → Subspace(Vsf(i))) → Subspace(⋂ᵢ Vsf)
[∪]-subspace : ∀{Vₛ₁ Vₛ₂} → Subspace{ℓ₁}(Vₛ₁) → Subspace{ℓ₂}(Vₛ₂) → (((Vₛ₁ ⊇ Vₛ₂) ∨ (Vₛ₁ ⊆ Vₛ₂)) ↔ Subspace(Vₛ₁ ∪ Vₛ₂))


text:
module _ where

module Inner where

  private
    variable A : Set

open Inner

fail : A → A
fail x = x


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

open import Prelude
open import Categories

module Categories.Coequalizer {ℓ₁ ℓ₂} (C : Category ℓ₁ ℓ₂) where

open Category C

private
  variable
    h i : X ⟶ Y

record Coequalizer (f g : X ⟶ Y) : Type (ℓ₁ ℓ⊔ ℓ₂) where
  field
    {obj} : Ob
    arr   : Y ⟶ obj

    equality   : arr · f ≡ arr · g
    coequalize : ∀ {H} {h : Y ⟶ H} → h · f ≡ h · g → obj ⟶ H
    universal  : ∀ {H} {h : Y ⟶ H} {eq : h · f ≡ h · g} → h ≡ coequalize eq · arr
    unique     : ∀ {H} {h : Y ⟶ H} {i : obj ⟶ H} {eq : h · f ≡ h · g} → h ≡ i · arr → i ≡ coequalize eq

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The universe polymorphic unit type and ordering relation
------------------------------------------------------------------------

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

module Data.Unit.Polymorphic.Base where

open import Level

------------------------------------------------------------------------
-- A unit type defined as a record type

record ⊤ {ℓ : Level} : Set ℓ where
  constructor tt


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

open import Functions.Definition
open import Functions.Lemmas
open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Order
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas
open import Sets.Cardinality.Infinite.Definition
open import Sets.Cardinality.Finite.Lemmas
open import Numbers.Reals.Definition
open import Numbers.Rationals.Definition
open import Numbers.Integers.Definition
open import Sets.Cardinality.Infinite.Lemmas
open import Setoids.Setoids

module Sets.Cardinality.Infinite.Examples where

ℕIsInfinite : InfiniteSet ℕ
ℕIsInfinite n f bij = pigeonhole (le 0 refl) badInj
  where
    inv : ℕ → FinSet n
    inv = Invertible.inverse (bijectionImpliesInvertible bij)
    invInj : Injection inv
    invInj = Bijection.inj (invertibleImpliesBijection (inverseIsInvertible (bijectionImpliesInvertible bij)))
    bumpUp : FinSet n → FinSet (succ n)
    bumpUp = intoSmaller (le 0 refl)
    bumpUpInj : Injection bumpUp
    bumpUpInj = intoSmallerInj (le 0 refl)
    nextInj : Injection (toNat {succ n})
    nextInj = finsetInjectIntoℕ {succ n}
    bad : FinSet (succ n) → FinSet n
    bad a = (inv (toNat a))
    badInj : Injection bad
    badInj = injComp nextInj invInj

ℝIsInfinite : DedekindInfiniteSet ℝ
DedekindInfiniteSet.inj ℝIsInfinite n = injectionR (injectionQ (nonneg n))
DedekindInfiniteSet.isInjection ℝIsInfinite {x} {y} pr = nonnegInjective (injectionQInjective (injectionRInjective pr))


text:
module DeBruijn where

open import Prelude -- using (_∘_)       -- composition, identity
open import Data.Maybe
open import Logic.Identity renaming (subst to subst≡)
import Logic.ChainReasoning
module Chain = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans)
open Chain

-- untyped de Bruijn terms
data Lam (A : Set) : Set where
    var : A -> Lam A
    app : Lam A -> Lam A -> Lam A
    abs : Lam (Maybe A) -> Lam A

-- functoriality of Lam
lam : {A B : Set} -> (A -> B) -> Lam A -> Lam B
lam f (var a)     = var (f a)
lam f (app t1 t2) = app (lam f t1) (lam f t2)
lam f (abs r)     = abs (lam (fmap f) r)

-- lifting a substitution A -> Lam B under a binder
lift : {A B : Set} -> (A -> Lam B) -> Maybe A -> Lam (Maybe B)
lift f nothing  = var nothing
lift f (just a) = lam just (f a)

-- extensionality of lifting
liftExt : {A B : Set}(f g : A -> Lam B) ->
   ((a : A) -> f a ≡ g a) -> (t : Maybe A) -> lift f t ≡ lift g t
liftExt f g H nothing  = refl
liftExt f g H (just a) = cong (lam just) $ H a

-- simultaneous substitution
subst : {A B : Set} -> (A -> Lam B) -> Lam A -> Lam B
subst f (var a)     = f a
subst f (app t1 t2) = app (subst f t1) (subst f t2)
subst f (abs r)     = abs (subst (lift f) r)

-- extensionality of subst
substExt : {A B : Set}(f g : A -> Lam B) ->
   ((a : A) -> f a ≡ g a) -> (t : Lam A) -> subst f t ≡ subst g t
substExt f g H (var a)     = H a
substExt f g H (app t1 t2) =
  chain> subst f (app t1 t2)
     === app (subst f t1) (subst f t2)
       by refl
     === app (subst g t1) (subst f t2)
       by cong (\ x -> app x (subst f t2)) (substExt f g H t1)
     === app (subst g t1) (subst g t2)
       by cong (\ x -> app (subst g t1) x) (substExt f g H t2)
substExt f g H (abs r) =
  chain> subst f (abs r)
     === abs (subst (lift f) r)
       by refl
     === abs (subst (lift g) r)
       by cong abs (substExt (lift f) (lift g) (liftExt f g H) r)
     === subst g (abs r)
       by refl

-- Lemma: lift g ∘ fmap f = lift (g ∘ f)
liftLaw1 : {A B C : Set}(f : A -> B)(g : B -> Lam C)(t : Maybe A) ->
  lift g (fmap f t) ≡ lift (g ∘ f) t
liftLaw1 f g nothing =
  chain> lift g (fmap f nothing)
     === lift g nothing          by refl
     === var nothing             by refl
     === lift (g ∘ f) nothing    by refl
liftLaw1 f g (just a) =
  chain> lift g (fmap f (just a))
     === lift g (just (f a))     by refl
     === lam just (g (f a))      by refl
     === lift (g ∘ f) (just a)   by refl

-- Lemma: subst g (lam f t) = subst (g ∘ f) t
substLaw1 : {A B C : Set}(f : A -> B)(g : B -> Lam C)(t : Lam A) ->
  subst g (lam f t) ≡ subst (g ∘ f) t

substLaw1 f g (var a) = refl

substLaw1 f g (app t1 t2) =
  chain> subst g (lam f (app t1 t2))
     === subst g (app (lam f t1) (lam f t2))
       by refl
     === app (subst g (lam f t1)) (subst g (lam f t2))
       by refl
     === app (subst (g ∘ f) t1) (subst g (lam f t2))
       by cong (\ x -> app x (subst g (lam f t2))) (substLaw1 f g t1)
     === app (subst (g ∘ f) t1) (subst (g ∘ f) t2)
       by cong (\ x -> app (subst (g ∘ f) t1) x) (substLaw1 f g t2)

substLaw1 f g (abs r) =
  chain> subst g (lam f (abs r))
     === subst g (abs (lam (fmap f) r))
       by refl
     === abs (subst (lift g) (lam (fmap f) r))
       by refl
     === abs (subst (lift g ∘ fmap f) r)
       by cong abs (substLaw1 (fmap f) (lift g) r)
     === abs (subst (lift (g ∘ f)) r)
       by cong abs (substExt (lift g ∘ fmap f) (lift (g ∘ f)) (liftLaw1 f g) r)

-- Lemma: subst (lam f ∘ g) = lam f ∘ subst g
substLaw2 : {A B C : Set}(f : B -> C)(g : A -> Lam B)(t : Lam A) ->
  subst (lam f ∘ g) t ≡ lam f (subst g t)
substLaw2 f g (var a) = refl

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing where the natural numbers and some related
-- operations and properties are defined, and how they can be used
------------------------------------------------------------------------

module README.Nat where

-- The natural numbers and various arithmetic operations are defined
-- in Data.Nat.

open import Data.Nat

ex₁ : ℕ
ex₁ = 1 + 3

-- Propositional equality and some related properties can be found
-- in Relation.Binary.PropositionalEquality.

open import Relation.Binary.PropositionalEquality

ex₂ : 3 + 5 ≡ 2 * 4
ex₂ = refl

-- Data.Nat.Properties contains a number of properties about natural
-- numbers. Algebra defines what a commutative semiring is, among
-- other things.

open import Algebra
import Data.Nat.Properties as Nat
private
  module CS = CommutativeSemiring Nat.commutativeSemiring

ex₃ : ∀ m n → m * n ≡ n * m
ex₃ m n = CS.*-comm m n

-- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
-- provides some combinators for equational reasoning.

open ≡-Reasoning
open import Data.Product

ex₄ : ∀ m n → m * (n + 0) ≡ n * m
ex₄ m n = begin
  m * (n + 0)  ≡⟨ cong (_*_ m) (proj₂ CS.+-identity n) ⟩
  m * n        ≡⟨ CS.*-comm m n ⟩
  n * m        ∎

-- The module SemiringSolver in Data.Nat.Properties contains a solver
-- for natural number equalities involving variables, constants, _+_
-- and _*_.

open Nat.SemiringSolver

ex₅ : ∀ m n → m * (n + 0) ≡ n * m
ex₅ = solve 2 (λ m n → m :* (n :+ con 0)  :=  n :* m) refl


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

module Data.Nat.Base where

open import Agda.Builtin.Nat public
  using (_+_; _*_; zero; suc)
  renaming (Nat to ℕ; _-_ to _∸_)
import Agda.Builtin.Nat as Nat

open import Level
open import Data.Bool

data Ordering : ℕ → ℕ → Type₀ where
  less    : ∀ m k → Ordering m (suc (m + k))
  equal   : ∀ m   → Ordering m m
  greater : ∀ m k → Ordering (suc (m + k)) m

compare : ∀ m n → Ordering m n
compare zero    zero    = equal   zero
compare (suc m) zero    = greater zero m
compare zero    (suc n) = less    zero n
compare (suc m) (suc n) with compare m n
... | less    m k = less (suc m) k
... | equal   m   = equal (suc m)
... | greater n k = greater (suc n) k

nonZero : ℕ → Bool
nonZero (suc _) = true
nonZero zero    = false

_÷_ : (n m : ℕ) → { m≢0 : T (nonZero m) } → ℕ
_÷_ n (suc m) = Nat.div-helper 0 m n m

rem : (n m : ℕ) → { m≢0 : T (nonZero m) } → ℕ
rem n (suc m) = Nat.mod-helper 0 m n m


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Setoids.Setoids
open import Setoids.Subset
open import Graphs.Definition
open import Sets.FinSet.Definition
open import Numbers.Naturals.Semiring
open import Sets.EquivalenceRelations

module Graphs.CompleteGraph where

CompleteGraph : {a b : _} {V' : Set a} (V : Setoid {a} {b} V') → Graph b V
Graph._<->_ (CompleteGraph V) x y = ((Setoid._∼_ V x y) → False)
Graph.noSelfRelation (CompleteGraph V) x x!=x = x!=x (Equivalence.reflexive (Setoid.eq V))
Graph.symmetric (CompleteGraph V) x!=y y=x = x!=y ((Equivalence.symmetric (Setoid.eq V)) y=x)
Graph.wellDefined (CompleteGraph V) {x} {y} {r} {s} x=y r=s x!=r y=s = x!=r (transitive x=y (transitive y=s (symmetric r=s)))
  where
    open Setoid V
    open Equivalence eq

Kn : (n : ℕ) → Graph _ (reflSetoid (FinSet n))
Kn n = CompleteGraph (reflSetoid (FinSet n))

triangle : Graph _ (reflSetoid (FinSet 3))
triangle = Kn 3


text:
module Nat1 where

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

_+_ : ℕ → ℕ → ℕ
zero   + b = b
succ a + b = succ (a + b)

open import Equality
one   = succ zero
two   = succ one
three = succ two

0-is-id : ∀ (n : ℕ) → (n + zero) ≡ n
0-is-id zero     =
  begin
    (zero + zero) ≈ zero by definition
  ∎
0-is-id (succ y) =
  begin
    (succ y + zero) ≈ succ (y + zero) by definition
                    ≈ succ y          by cong succ (0-is-id y)
  ∎

+-assoc : ∀ (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
+-assoc zero     b c = definition
+-assoc (succ a) b c =
  begin ((succ a + b) + c)
               ≈ succ (a + b) + c by definition
               ≈ succ ((a + b) + c) by definition
               ≈ succ (a + (b + c)) by cong succ (+-assoc a b c)
               ≈ succ a + (b + c) by definition
  ∎
{-
+-assoc zero     b c     = definition
+-assoc (succ a) b c     =
  begin ((succ a + b) + c)
               ≈ succ (a + b)  + c   by definition
               ≈ succ ((a + b) + c)  by definition
               ≈ succ (a  + (b + c)) by cong succ (+-assoc a b c)
               ≈ succ a   + (b + c)  by definition
  ∎
-}

max_stars_repo_name: piyush-kurur/sample-code

max_issues_repo_name: piyush-kurur/sample-code

max_forks_repo_name: piyush-kurur/sample-code


text:
module Functor where

record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set where
  field
    refl  : ∀ {x} → x ≈ x
    sym   : ∀ {i j} → i ≈ j → j ≈ i
    trans : ∀ {i j k} → i ≈ j → j ≈ k → i ≈ k

record Setoid : Set₁ where
  infix 4 _≈_
  field
    Carrier       : Set
    _≈_           : Carrier → Carrier → Set
    isEquivalence : IsEquivalence _≈_

  open IsEquivalence isEquivalence public

infixr 0 _⟶_

record _⟶_ (From To : Setoid) : Set where
  infixl 5 _⟨$⟩_
  field
    _⟨$⟩_ : Setoid.Carrier From → Setoid.Carrier To
    cong  : ∀ {x y} →
            Setoid._≈_ From x y → Setoid._≈_ To (_⟨$⟩_ x) (_⟨$⟩_ y)

open _⟶_ public

id : ∀ {A} → A ⟶ A
id = record { _⟨$⟩_ = λ x → x; cong = λ x≈y → x≈y }

infixr 9 _∘_

_∘_ : ∀ {A B C} → B ⟶ C → A ⟶ B → A ⟶ C
f ∘ g = record
  { _⟨$⟩_ = λ x → f ⟨$⟩ (g ⟨$⟩ x)
  ; cong  = λ x≈y → cong f (cong g x≈y)
  }

_⇨_ : (To From : Setoid) → Setoid
From ⇨ To = record
  { Carrier       = From ⟶ To
  ; _≈_           = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
  ; isEquivalence = record
    { refl  = λ {f} → cong f
    ; sym   = λ f∼g x∼y → To.sym (f∼g (From.sym x∼y))
    ; trans = λ f∼g g∼h x∼y → To.trans (f∼g From.refl) (g∼h x∼y)
    }
  }
  where
  open module From = Setoid From using () renaming (_≈_ to _≈₁_)
  open module To   = Setoid To   using () renaming (_≈_ to _≈₂_)

record Functor (F : Setoid → Setoid) : Set₁ where
  field
    map : ∀ {A B} → (A ⇨ B) ⟶ (F A ⇨ F B)

    identity : ∀ {A} →
      let open Setoid (F A ⇨ F A) in
      map ⟨$⟩ id ≈ id

    composition : ∀ {A B C} (f : B ⟶ C) (g : A ⟶ B) →
      let open Setoid (F A ⇨ F C) in
      map ⟨$⟩ (f ∘ g) ≈ (map ⟨$⟩ f) ∘ (map ⟨$⟩ g)


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

open import HoTT
open import cohomology.FunctionOver
open import cohomology.Theory

{- Useful lemmas concerning the functorial action of C -}

module cohomology.Functor {i} (CT : CohomologyTheory i) where

open CohomologyTheory CT

open import cohomology.Unit CT
open import cohomology.BaseIndependence CT

CF-cst : (n : ℤ) {X Y : Ptd i} → CF-hom n (⊙cst {X = X} {Y = Y}) == cst-hom
CF-cst n {X} {Y} =
  CF-hom n (⊙cst {X = ⊙LU} ⊙∘ ⊙cst {X = X})
    =⟨ CF-comp n ⊙cst ⊙cst ⟩
  (CF-hom n (⊙cst {X = X})) ∘ᴳ (CF-hom n (⊙cst {X = ⊙LU}))
    =⟨ hom= (CF-hom n (⊙cst {X = ⊙LU})) cst-hom
            (contr-has-all-paths (→-level (C-Unit-is-contr n)) _ _)
       |in-ctx (λ w → CF-hom n (⊙cst {X = X} {Y = ⊙LU}) ∘ᴳ w) ⟩
  (CF-hom n (⊙cst {X = X} {Y = ⊙LU})) ∘ᴳ cst-hom
    =⟨ pre∘-cst-hom (CF-hom n (⊙cst {X = X} {Y = ⊙LU})) ⟩
  cst-hom ∎
  where
  ⊙LU = ⊙Lift {j = i} ⊙Unit

CF-inverse : (n : ℤ) {X Y : Ptd i} (f : fst (X ⊙→ Y)) (g : fst (Y ⊙→ X))
  → (∀ x → fst g (fst f x) == x)
  → (CF-hom n f) ∘ᴳ (CF-hom n g) == idhom _
CF-inverse n f g p = ! (CF-comp n g f) ∙ CF-λ= n p ∙ CF-ident n

CF-iso : (n : ℤ) {X Y : Ptd i} → X ⊙≃ Y → C n Y ≃ᴳ C n X
CF-iso n (f , ie) =
  (CF-hom n f ,
   is-eq _ (GroupHom.f (CF-hom n (⊙<– (f , ie))))
     (app= $ ap GroupHom.f $ CF-inverse n f _ $ <–-inv-l (fst f , ie))
     (app= $ ap GroupHom.f $ CF-inverse n _ f $ <–-inv-r (fst f , ie)))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import HoTT
open import homotopy.elims.CofPushoutSection

{- If f : X → Y is a section, then ΣY ≃ ΣX ∨ ΣCof(f) -}

module homotopy.SuspSectionDecomp
  {i j} {X : Ptd i} {Y : Ptd j} (⊙f : X ⊙→ Y)
  (g : de⊙ Y → de⊙ X) (inv : ∀ x → g (fst ⊙f x) == x)
  where

module SuspSectionDecomp where

  private
    f = fst ⊙f

  module Into = SuspRec {C = de⊙ (⊙Susp X ⊙∨ ⊙Susp (⊙Cofiber ⊙f))}
    (winl south)
    (winr south)
    (λ y → ! (ap winl (merid (g y))) ∙ wglue ∙ ap winr (merid (cfcod y)))

  into = Into.f

  module OutWinl = SuspRec south south
    (λ x → ! (merid (f x)) ∙ merid (pt Y))

  out-winr-glue : de⊙ (⊙Cofiber ⊙f) → south' (de⊙ Y) == south
  out-winr-glue = CofiberRec.f
    idp
    (λ y → ! (merid (f (g y))) ∙ merid y)
    (λ x → ! $
      ap (λ w → ! (merid (f w)) ∙ merid (f x))
         (inv x)
      ∙ !-inv-l (merid (f x)))

  module OutWinr = SuspRec south south out-winr-glue

  out-winl = OutWinl.f
  out-winr = OutWinr.f

  module Out = WedgeRec {X = ⊙Susp X} {Y = ⊙Susp (⊙Cofiber ⊙f)}
    out-winl out-winr idp

  out = Out.f

  out-into : ∀ σy → out (into σy) == σy
  out-into = Susp-elim
    (! (merid (pt Y)))
    idp
    (↓-∘=idf-from-square out into ∘ λ y →
      (ap (ap out) (Into.merid-β y)
       ∙ ap-∙ out (! (ap winl (merid (g y))))
                  (wglue ∙ ap winr (merid (cfcod y)))
       ∙ part₁ y
         ∙2 (ap-∙ out wglue (ap winr (merid (cfcod y)))
             ∙ Out.glue-β ∙2 part₂ y))
      ∙v⊡ square-lemma (merid (pt Y)) (merid (f (g y))) (merid y))
    where
    part₁ : (y : de⊙ Y) → ap out (! (ap winl (merid (g y))))
                       == ! (merid (pt Y)) ∙ merid (f (g y))
    part₁ y =
      ap-! out (ap winl (merid (g y)))
      ∙ ap ! (∘-ap out winl (merid (g y)))
      ∙ ap ! (OutWinl.merid-β (g y))
      ∙ !-∙ (! (merid (f (g y)))) (merid (pt Y))
      ∙ ap (λ w → ! (merid (pt Y)) ∙ w)
           (!-! (merid (f (g y))))

    part₂ : (y : de⊙ Y) → ap out (ap winr (merid (cfcod y)))
                       == ! (merid (f (g y))) ∙ merid y
    part₂ y =
      ∘-ap out winr (merid (cfcod y))
      ∙ OutWinr.merid-β (cfcod y)

    square-lemma : ∀ {i} {A : Type i} {x y z w : A}
      (p : x == y) (q : x == z) (r : x == w)
      → Square (! p) ((! p ∙ q) ∙ ! q ∙ r) r idp
    square-lemma idp idp idp = ids

  into-out : ∀ w → into (out w) == w
  into-out = Wedge-elim
    into-out-winl
    into-out-winr
    (↓-∘=idf-from-square into out $
      ap (ap into) Out.glue-β
      ∙v⊡ glue-square-lemma (! (ap winr (merid cfbase))) wglue)
    where
    {- Three path induction lemmas to simply some squares -}

    winl-square-lemma : ∀ {i} {A : Type i} {x y z w : A}
      (p q : x == y) (s : x == z) (r t u : z == w) (v : x == y)
      → p == q → r == t → r == u
      → Square (! r ∙ ! s) (! (! p ∙ s ∙ t) ∙ ! v ∙ s ∙ u) q (! r ∙ ! s ∙ v)
    winl-square-lemma idp .idp idp idp .idp .idp v idp idp idp =
      ∙-unit-r _ ∙v⊡ rt-square v

    winr-square-lemma : ∀ {i} {A : Type i} {x y z w : A}
      (p q u : x == y) (r t : z == w) (s : z == x)
      → p == q → r == t
      → Square (! p) (! (! r ∙ s ∙ q) ∙ ! t ∙ s ∙ u) u idp
    winr-square-lemma idp .idp u idp .idp idp idp idp = vid-square

    glue-square-lemma : ∀ {i} {A : Type i} {x y z : A}
      (p : x == y) (q : z == y)
      → Square (p ∙ ! q) idp q p
    glue-square-lemma idp idp = ids

    into-out-winl : ∀ σx → into (out (winl σx)) == winl σx
    into-out-winl = Susp-elim
      (! (ap winr (merid cfbase)) ∙ ! wglue)
      (! (ap winr (merid cfbase)) ∙ ! wglue
       ∙ ap winl (merid (g (pt Y))))
      (↓-='-from-square ∘ λ x →
        (ap-∘ into out-winl (merid x)
         ∙ ap (ap into) (OutWinl.merid-β x)
         ∙ ap-∙ into (! (merid (f x))) (merid (pt Y))
         ∙ (ap-! into (merid (f x))
            ∙ ap ! (Into.merid-β (f x)))
           ∙2 Into.merid-β (pt Y))
        ∙v⊡ winl-square-lemma
              (ap winl (merid (g (f x))))
              (ap winl (merid x))
              wglue
              (ap winr (merid cfbase))
              (ap winr (merid (cfcod (f x))))
              (ap winr (merid (cfcod (pt Y))))
              (ap winl (merid (g (pt Y))))
              (ap (ap winl ∘ merid) (inv x))
              (ap (ap winr ∘ merid) (cfglue x))
              (ap (ap winr ∘ merid)
                  (cfglue (pt X) ∙ ap cfcod (snd ⊙f))))

    into-out-winr : ∀ σκ → into (out (winr σκ)) == winr σκ
    into-out-winr = CofPushoutSection.elim {h = λ _ → unit} g inv
      (! (ap winr (merid cfbase)))
      (λ tt → idp)
      (λ tt → transport
        (λ κ → ! (ap winr (merid cfbase)) == idp
               [ (λ σκ → into (out (winr σκ)) == winr σκ) ↓ merid κ ])
        (! (cfglue (pt X)))
        (into-out-winr-coh (f (pt X))))
      into-out-winr-coh
      where
      into-out-winr-coh : (y : de⊙ Y)
        → ! (ap winr (merid cfbase)) == idp
          [ (λ σκ → into (out (winr σκ)) == winr σκ) ↓ merid (cfcod y) ]
      into-out-winr-coh y = ↓-='-from-square $
        (ap-∘ into out-winr (merid (cfcod y))
         ∙ ap (ap into) (OutWinr.merid-β (cfcod y))
         ∙ ap-∙ into (! (merid (f (g y)))) (merid y)
         ∙ (ap-! into (merid (f (g y)))
            ∙ ap ! (Into.merid-β (f (g y))))
           ∙2 Into.merid-β y)
        ∙v⊡ winr-square-lemma
              (ap winr (merid cfbase))
              (ap winr (merid (cfcod (f (g y)))))
              (ap winr (merid (cfcod y)))
              (ap winl (merid (g (f (g y)))))
              (ap winl (merid (g y)))
              wglue
              (ap (ap winr ∘ merid) (cfglue (g y)))
              (ap (ap winl ∘ merid) (inv (g y)))

  eq : Susp (de⊙ Y) ≃ ⊙Susp X ∨ ⊙Susp (⊙Cofiber ⊙f)
  eq = equiv into out into-out out-into

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

import      Lvl
open import Data
open import Data.Boolean.Stmt
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Comparisons.Proofs
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Order
open import Relator.Equals
open import Relator.Equals.Proofs

private variable d d₁ d₂ b a' b' : ℕ

inddiv-result-𝐒 : [ 𝐒 d , b ] a' div b' ≡ 𝐒([ d , b ] a' div b')
inddiv-result-𝐒 {d} {b} {𝟎}    {b'}   = [≡]-intro
inddiv-result-𝐒 {d} {b} {𝐒 a'} {𝟎}    = inddiv-result-𝐒 {𝐒 d} {b} {a'} {b}
inddiv-result-𝐒 {d} {b} {𝐒 a'} {𝐒 b'} = inddiv-result-𝐒 {d}{b}{a'}{b'}
{-# REWRITE inddiv-result-𝐒 #-}

inddiv-result : [ d , b ] a' div b' ≡ d + ([ 𝟎 , b ] a' div b')
inddiv-result {𝟎}              = [≡]-intro
inddiv-result {𝐒 d}{b}{a'}{b'} = [≡]-with(𝐒) (inddiv-result {d}{b}{a'}{b'})

inddiv-of-denominator : [ d , b ] b' div b' ≡ d
inddiv-of-denominator {d} {b} {𝟎}    = [≡]-intro
inddiv-of-denominator {d} {b} {𝐒 b'} = inddiv-of-denominator{d}{b}{b'}

inddiv-of-denominator-successor : [ d , b ] 𝐒 b' div b' ≡ 𝐒 d
inddiv-of-denominator-successor {d} {b} {𝟎}    = [≡]-intro
inddiv-of-denominator-successor {d} {b} {𝐒 b'} = inddiv-of-denominator-successor{d}{b}{b'}

inddiv-step-denominator : [ d , b ] (a' + b') div b' ≡ [ d , b ] a' div 𝟎
inddiv-step-denominator {_} {_} {_}  {𝟎}    = [≡]-intro
inddiv-step-denominator {d} {b} {a'} {𝐒 b'} = inddiv-step-denominator {d} {b} {a'} {b'}

inddiv-smaller : (a' ≤ b') → ([ d , b ] a' div b' ≡ d)
inddiv-smaller min = [≡]-intro
inddiv-smaller {d = d}{b} (succ {𝟎}   {𝟎}    p) = [≡]-intro
inddiv-smaller {d = d}{b} (succ {𝟎}   {𝐒 b'} p) = [≡]-intro
inddiv-smaller {d = d}{b} (succ {𝐒 a'}{𝐒 b'} p) = inddiv-smaller {d = d}{b} p

[⌊/⌋][⌊/⌋₀]-equality : ∀{a b} → ⦃ _ : IsTrue(positive?(b))⦄ → (a ⌊/⌋₀ b ≡ a ⌊/⌋ b)
[⌊/⌋][⌊/⌋₀]-equality {b = 𝐒 b} = [≡]-intro

[⌊/⌋]-of-0ₗ : ∀{n} → ⦃ _ : IsTrue(positive?(n))⦄ → (𝟎 ⌊/⌋ n ≡ 𝟎)
[⌊/⌋]-of-0ₗ {𝐒 n} = [≡]-intro

[⌊/⌋]-of-1ₗ : ∀{n} → ⦃ _ : IsTrue(positive?(n))⦄ → ⦃ _ : IsTrue(n ≢? 1)⦄ → (1 ⌊/⌋ n ≡ 𝟎)
[⌊/⌋]-of-1ₗ {𝐒 (𝐒 n)} = [≡]-intro

[⌊/⌋]-of-1ᵣ : ∀{m} → (m ⌊/⌋ 1 ≡ m)
[⌊/⌋]-of-1ᵣ {𝟎} = [≡]-intro
[⌊/⌋]-of-1ᵣ {𝐒 m} = [≡]-with(𝐒) ([⌊/⌋]-of-1ᵣ {m})

[⌊/⌋]-of-same : ∀{n} → ⦃ _ : IsTrue(positive?(n))⦄ → (n ⌊/⌋ n ≡ 1)
[⌊/⌋]-of-same {𝐒 n} = inddiv-of-denominator-successor {b' = n}

postulate [⌊/⌋]-positive : ∀{a b} ⦃ _ : Positive(a) ⦄ ⦃ _ : Positive(b) ⦄ → Positive(a ⌊/⌋ b)

{-
[⌊/⌋]-of-[+]ₗ : ∀{m n} → ⦃ _ : IsTrue(n ≢? 𝟎)⦄ → ((m + n) ⌊/⌋ n ≡ 𝐒(m ⌊/⌋ n))
[⌊/⌋]-of-[+]ₗ {_}   {𝐒 𝟎}     = [≡]-intro
[⌊/⌋]-of-[+]ₗ {𝟎}   {𝐒 (𝐒 n)} = [≡]-intro
[⌊/⌋]-of-[+]ₗ {𝐒 m} {𝐒 (𝐒 n)} = {![⌊/⌋]-of-[+]ₗ {m} {𝐒 (𝐒 n)}!}

[⌊/⌋]-is-0 : ∀{m n} → ⦃ _ : IsTrue(n ≢? 𝟎)⦄ → (m ⌊/⌋ n ≡ 𝟎) → (m ≡ 𝟎)
[⌊/⌋]-is-0 {𝟎}   {𝐒 n}    _ = [≡]-intro
[⌊/⌋]-is-0 {𝐒 m} {𝐒(𝐒 n)} p with [⌊/⌋]-is-0 {𝐒 m} {𝐒 n} {!!}
... | pp = {!!}
-}

postulate [⌊/⌋]-leₗ : ∀{a b} ⦃ _ : IsTrue(positive?(b))⦄ → (a ⌊/⌋ b ≤ a)

postulate [⌊/⌋]-ltₗ : ∀{a} ⦃ _ : IsTrue(positive?(a))⦄ {b} ⦃ b-proof : IsTrue(b >? 1)⦄ → ((a ⌊/⌋ b) ⦃ [<?]-positive-any {1}{b} ⦄ < a)

postulate [⌊/⌋]-zero : ∀{a b} ⦃ _ : IsTrue(positive?(b))⦄ → (a < b) → (a ⌊/⌋ b ≡ 𝟎)

postulate [⌊/⌋]-preserve-[<]ₗ : ∀{a b d} ⦃ _ : IsTrue(positive?(b))⦄ ⦃ _ : IsTrue(positive?(d))⦄ → (a < b) → (a ⌊/⌋ d < b)

postulate [⌊/⌋][+]-distributivityᵣ : ∀{a b c} ⦃ _ : IsTrue(positive?(c))⦄ → ((a + b) ⌊/⌋ c ≡ (a ⌊/⌋ c) + (b ⌊/⌋ c))


text:
{-# OPTIONS --without-K --rewriting --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Equality.Rewrite where

open import Agda.Builtin.Equality

{-# BUILTIN REWRITE _≡_ #-}


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Transitivity

module Oscar.Class.Transextensionality where

module Transextensionality
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ) (let infix 4 _∼̇_ ; _∼̇_ = _∼̇_)
  (transitivity : Transitivity.type _∼_)
  (let _∙_ : FlipTransitivity.type _∼_
       _∙_ g f = transitivity f g)
  = ℭLASS ((λ {x y} → _∼̇_ {x} {y}) , λ {x y z} → transitivity {x} {y} {z}) -- FIXME what other possibilities work here?
          (∀ {x y z} {f₁ f₂ : x ∼ y} {g₁ g₂ : y ∼ z} → f₁ ∼̇ f₂ → g₁ ∼̇ g₂ → g₁ ∙ f₁ ∼̇ g₂ ∙ f₂)

module Transextensionality!
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ) (let infix 4 _∼̇_ ; _∼̇_ = _∼̇_)
  ⦃ tr : Transitivity.class _∼_ ⦄
  = Transextensionality (_∼_) (λ {x y} → _∼̇_ {x} {y}) transitivity

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  {ℓ} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ}
  {transitivity : Transitivity.type _∼_}
  where
  transextensionality = Transextensionality.method _∼_ _∼̇_ transitivity


text:
module AocIO where
open import IO.Primitive public
open import Data.String as String
open import Data.List as List

postulate
  getLine : IO Costring
  getArgs : IO (List String)
  getProgName : IO String

{-# COMPILE GHC getLine = getLine #-}
{-# FOREIGN GHC import qualified Data.Text    as Text #-}
{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}
{-# FOREIGN GHC import System.Environment (getArgs, getProgName) #-}
{-# COMPILE GHC getArgs = fmap (map Text.pack) getArgs #-}
{-# COMPILE GHC getProgName = fmap Text.pack getProgName   #-}


text:
module Structure.Operator.Proofs where

import Lvl
open import Data
open import Data.Tuple
open import Functional hiding (id)
open import Function.Equals
import      Function.Names as Names
import      Lang.Vars.Structure.Operator
open        Lang.Vars.Structure.Operator.Select
open import Logic.IntroInstances
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Setoid.Uniqueness
open import Structure.Function.Domain
open import Structure.Function.Multi
open import Structure.Function
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Syntax.Type
open import Type

module One {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_▫_ : T → T → T} where
  open Lang.Vars.Structure.Operator.One ⦃ equiv = equiv ⦄ {_▫_ = _▫_}

  -- When an identity element exists and is the same for both sides, it is unique.
  unique-identity : Unique(Identity(_▫_))
  unique-identity{x₁}{x₂} (intro ⦃ intro identityₗ₁ ⦄ ⦃ intro identityᵣ₁ ⦄) (intro ⦃ intro identityₗ₂ ⦄ ⦃ intro identityᵣ₂ ⦄) =
    x₁      🝖-[ symmetry(_≡_) (identityₗ₂{x₁}) ]
    x₂ ▫ x₁ 🝖-[ identityᵣ₁{x₂} ]
    x₂      🝖-end

  -- An existing left identity is unique when the operator is commutative
  unique-identityₗ-by-commutativity : let _ = comm in Unique(Identityₗ(_▫_))
  unique-identityₗ-by-commutativity {x₁}{x₂} (intro identity₁) (intro identity₂) =
    x₁      🝖-[ symmetry(_≡_) (identity₂{x₁}) ]
    x₂ ▫ x₁ 🝖-[ commutativity(_▫_) {x₂}{x₁} ]
    x₁ ▫ x₂ 🝖-[ identity₁{x₂} ]
    x₂      🝖-end

  -- An existing right identity is unique when the operator is commutative
  unique-identityᵣ-by-commutativity : let _ = comm in Unique(Identityᵣ(_▫_))
  unique-identityᵣ-by-commutativity {x₁}{x₂} (intro identity₁) (intro identity₂) =
    x₁      🝖-[ symmetry(_≡_) (identity₂{x₁}) ]
    x₁ ▫ x₂ 🝖-[ commutativity(_▫_) {x₁}{x₂} ]
    x₂ ▫ x₁ 🝖-[ identity₁{x₂} ]
    x₂      🝖-end

  -- An existing left identity is unique when the operator is cancellable
  unique-identityₗ-by-cancellationᵣ : let _ = cancᵣ in Unique(Identityₗ(_▫_))
  unique-identityₗ-by-cancellationᵣ {x₁}{x₂} (intro identity₁) (intro identity₂) =
    cancellationᵣ(_▫_) {x₁}{x₁}{x₂} (
      x₁ ▫ x₁ 🝖-[ identity₁{x₁} ]
      x₁      🝖-[ symmetry(_≡_) (identity₂{x₁}) ]
      x₂ ▫ x₁ 🝖-end
    ) :of: (x₁ ≡ x₂)

  -- An existing left identity is unique when the operator is cancellable
  unique-identityᵣ-by-cancellationₗ : let _ = cancₗ in Unique(Identityᵣ(_▫_))
  unique-identityᵣ-by-cancellationₗ {x₁}{x₂} (intro identity₁) (intro identity₂) =
    cancellationₗ(_▫_) {x₂}{x₁}{x₂} (
      x₂ ▫ x₁ 🝖-[ identity₁{x₂} ]
      x₂      🝖-[ symmetry(_≡_) (identity₂{x₂}) ]
      x₂ ▫ x₂ 🝖-end
    ) :of: (x₁ ≡ x₂)

  -- When identities for both sides exists, they are the same
  unique-identities : ⦃ _ : Identityₗ(_▫_)(idₗ) ⦄ → ⦃ _ : Identityᵣ(_▫_)(idᵣ) ⦄ → (idₗ ≡ idᵣ)
  unique-identities {idₗ}{idᵣ} =
    idₗ       🝖-[ symmetry(_≡_) (identityᵣ(_▫_)(idᵣ)) ]
    idₗ ▫ idᵣ 🝖-[ identityₗ(_▫_)(idₗ) ]
    idᵣ       🝖-end

  -- When identities for both sides exists, they are the same
  identity-equivalence-by-commutativity : let _ = comm in Identityₗ(_▫_)(id) ↔ Identityᵣ(_▫_)(id)
  identity-equivalence-by-commutativity {id} = [↔]-intro l r where
    l : Identityₗ(_▫_)(id) ← Identityᵣ(_▫_)(id)
    Identityₗ.proof (l identᵣ) {x} = commutativity(_▫_) 🝖 identityᵣ(_▫_)(id) ⦃ identᵣ ⦄

    r : Identityₗ(_▫_)(id) → Identityᵣ(_▫_)(id)
    Identityᵣ.proof (r identₗ) {x} = commutativity(_▫_) 🝖 identityₗ(_▫_)(id) ⦃ identₗ ⦄

  -- Cancellation is possible when the operator is associative and have an inverse
  cancellationₗ-by-associativity-inverse : let _ = op , assoc , inverₗ in Cancellationₗ(_▫_)
  Cancellationₗ.proof(cancellationₗ-by-associativity-inverse {idₗ} {invₗ} ) {x}{a}{b} (xa≡xb) =
    a                🝖-[ symmetry(_≡_) (identityₗ(_▫_)(idₗ) {a}) ]
    idₗ ▫ a          🝖-[ congruence₂ₗ(_▫_)(a) (symmetry(_≡_) (inverseFunctionₗ(_▫_)(invₗ) {x})) ]
    (invₗ x ▫ x) ▫ a 🝖-[ associativity(_▫_) {invₗ(x)}{x}{a} ]
    invₗ x ▫ (x ▫ a) 🝖-[ congruence₂ᵣ(_▫_)(invₗ(x)) (xa≡xb) ]
    invₗ x ▫ (x ▫ b) 🝖-[ symmetry(_≡_) (associativity(_▫_) {invₗ(x)}{x}{b}) ]
    (invₗ x ▫ x) ▫ b 🝖-[ congruence₂ₗ(_▫_)(b) (inverseFunctionₗ(_▫_)(invₗ) {x}) ]
    idₗ ▫ b          🝖-[ identityₗ(_▫_)(idₗ){b} ]
    b                🝖-end
    -- TODO: This pattern of applying symmetric transitivity rules, make it a function

  -- Cancellation is possible when the operator is associative and have an inverse
  cancellationᵣ-by-associativity-inverse : let _ = op , assoc , inverᵣ in Cancellationᵣ(_▫_)
  Cancellationᵣ.proof(cancellationᵣ-by-associativity-inverse {idᵣ} {invᵣ} ) {x}{a}{b} (xa≡xb) =
    a                🝖-[ symmetry(_≡_) (identityᵣ(_▫_)(idᵣ)) ]
    a ▫ idᵣ          🝖-[ congruence₂ᵣ(_▫_)(_) (symmetry(_≡_) (inverseFunctionᵣ(_▫_)(invᵣ))) ]
    a ▫ (x ▫ invᵣ x) 🝖-[ symmetry(_≡_) (associativity(_▫_)) ]
    (a ▫ x) ▫ invᵣ x 🝖-[ congruence₂ₗ(_▫_)(_) (xa≡xb) ]
    (b ▫ x) ▫ invᵣ x 🝖-[ associativity(_▫_) ]
    b ▫ (x ▫ invᵣ x) 🝖-[ congruence₂ᵣ(_▫_)(_) (inverseFunctionᵣ(_▫_)(invᵣ)) ]
    b ▫ idᵣ          🝖-[ identityᵣ(_▫_)(idᵣ) ]
    b                🝖-end

  -- When something and something else's inverse is the identity element, they are equal
  equality-zeroₗ : let _ = op , assoc , select-inv(id)(ident)(inv)(inver) in ∀{x y} → (x ≡ y) ← (x ▫ inv(y) ≡ id)
  equality-zeroₗ {id}{inv} {x}{y} (proof) =
    x                🝖-[ symmetry(_≡_) (identity-right(_▫_)(id)) ]
    x ▫ id           🝖-[ symmetry(_≡_) (congruence₂ᵣ(_▫_)(x) (inverseFunction-left(_▫_)(inv))) ]
    x ▫ (inv(y) ▫ y) 🝖-[ symmetry(_≡_) (associativity(_▫_)) ]
    (x ▫ inv(y)) ▫ y 🝖-[ congruence₂ₗ(_▫_)(y) (proof) ]
    id ▫ y           🝖-[ identity-left(_▫_)(id) ]
    y                🝖-end

  equality-zeroᵣ : let _ = op , assoc , select-inv(id)(ident)(inv)(inver) in ∀{x y} → (x ≡ y) → (x ▫ inv(y) ≡ id)
  equality-zeroᵣ {id}{inv} {x}{y} (proof) =
    x ▫ inv(y) 🝖-[ congruence₂ₗ(_▫_)(inv(y)) proof ]
    y ▫ inv(y) 🝖-[ inverseFunctionᵣ(_▫_)(inv) ]
    id         🝖-end

  commuting-id : let _ = select-id(id)(ident) in ∀{x} → (id ▫ x ≡ x ▫ id)
  commuting-id {id} {x} =
    id ▫ x 🝖-[ identity-left(_▫_)(id) ]
    x      🝖-[ symmetry(_≡_) (identity-right(_▫_)(id)) ]
    x ▫ id 🝖-end

  squeezed-inverse : let _ = op , select-id(id)(ident) in ∀{a b x y} → (a ▫ b ≡ id) → ((x ▫ (a ▫ b)) ▫ y ≡ x ▫ y)
  squeezed-inverse {id} {a}{b}{x}{y} abid =
    (x ▫ (a ▫ b)) ▫ y 🝖-[ (congruence₂ₗ(_▫_)(_) ∘ congruence₂ᵣ(_▫_)(_)) abid ]
    (x ▫ id) ▫ y      🝖-[ congruence₂ₗ(_▫_)(_) (identity-right(_▫_)(id)) ]
    x ▫ y             🝖-end

  double-inverse : let _ = cancᵣ , select-inv(id)(ident)(inv)(inver) in ∀{x} → (inv(inv x) ≡ x)
  double-inverse {id}{inv} {x} =
    (cancellationᵣ(_▫_) $
      (
        inv(inv x) ▫ inv(x) 🝖-[ inverseFunction-left(_▫_)(inv) ]
        id                  🝖-[ inverseFunction-right(_▫_)(inv) ]-sym
        x ▫ inv(x)          🝖-end
      ) :of: (inv(inv x) ▫ inv(x) ≡ x ▫ inv(x))
    ) :of: (inv(inv x) ≡ x)

  double-inverseₗ-by-id : let _ = op , assoc , select-id(id)(ident) , select-invₗ(id)(Identity.left(ident))(invₗ)(inverₗ) in ∀{x} → (invₗ(invₗ x) ≡ x)
  double-inverseₗ-by-id {id}{inv} {x} =
    inv(inv(x))                🝖-[ symmetry(_≡_) (identityᵣ(_▫_)(id)) ]
    inv(inv(x)) ▫ id           🝖-[ congruence₂ᵣ(_▫_)(_) (symmetry(_≡_) (inverseFunctionₗ(_▫_)(inv))) ]
    inv(inv(x)) ▫ (inv(x) ▫ x) 🝖-[ symmetry(_≡_) (associativity(_▫_)) ]
    (inv(inv(x)) ▫ inv(x)) ▫ x 🝖-[ congruence₂ₗ(_▫_)(_) (inverseFunctionₗ(_▫_)(inv)) ]
    id ▫ x                     🝖-[ identityₗ(_▫_)(id) ]
    x                          🝖-end

  double-inverseᵣ-by-id : let _ = op , assoc , select-id(id)(ident) , select-invᵣ(id)(Identity.right(ident))(invᵣ)(inverᵣ) in ∀{x} → (invᵣ(invᵣ x) ≡ x)
  double-inverseᵣ-by-id {id}{inv} {x} =
    inv(inv(x))                🝖-[ identityₗ(_▫_)(id) ]-sym
    id ▫ inv(inv(x))           🝖-[ congruence₂ₗ(_▫_)(_) (inverseFunctionᵣ(_▫_)(inv)) ]-sym
    (x ▫ inv(x)) ▫ inv(inv(x)) 🝖-[ associativity(_▫_) ]
    x ▫ (inv(x) ▫ inv(inv(x))) 🝖-[ congruence₂ᵣ(_▫_)(_) (inverseFunctionᵣ(_▫_)(inv)) ]
    x ▫ id                     🝖-[ identityᵣ(_▫_)(id) ]
    x                          🝖-end

  {- double-complement-by-?
  inv(inv(x)) ▫ inv(x)
  ab
  inv(x) ▫ x
  -}

  inverse-equivalence-by-id : let _ = op , assoc , select-id(id)(ident) in InverseFunctionₗ(_▫_)(inv) ↔ InverseFunctionᵣ(_▫_)(inv)
  inverse-equivalence-by-id {id}{inv} = [↔]-intro l r where
    l : InverseFunctionₗ(_▫_)(inv) ← InverseFunctionᵣ(_▫_)(inv)
    InverseFunctionₗ.proof (l inverᵣ) {x} =
      inv(x) ▫ x           🝖-[ congruence₂ᵣ(_▫_)(_) (symmetry(_≡_) (double-inverseᵣ-by-id ⦃ inverᵣ = inverᵣ ⦄)) ]
      inv(x) ▫ inv(inv(x)) 🝖-[ inverseFunctionᵣ(_▫_)(inv) ⦃ inverᵣ ⦄ ]
      id                   🝖-end
    r : InverseFunctionₗ(_▫_)(inv) → InverseFunctionᵣ(_▫_)(inv)
    InverseFunctionᵣ.proof (r inverₗ) {x} =
      x ▫ inv(x)           🝖-[ congruence₂ₗ(_▫_)(_) (symmetry(_≡_) (double-inverseₗ-by-id ⦃ inverₗ = inverₗ ⦄)) ]
      inv(inv(x)) ▫ inv(x) 🝖-[ inverseFunctionₗ(_▫_)(inv) ⦃ inverₗ ⦄ ]
      id                   🝖-end

  {-
  complement-equivalence-by-id : let _ = op , assoc , select-abs(ab)(absorb) in ComplementFunctionₗ(_▫_)(inv) ↔ ComplementFunctionᵣ(_▫_)(inv)
  complement-equivalence-by-id {ab}{inv} = [↔]-intro l r where
    l : ComplementFunctionₗ(_▫_)(inv) ← ComplementFunctionᵣ(_▫_)(inv)
    ComplementFunctionₗ.proof (l absorbᵣ) {x} =
      inv(x) ▫ x           🝖-[ {!!} ]
      inv(x) ▫ inv(inv(x)) 🝖-[ {!!} ]
      ab                   🝖-end
    r : ComplementFunctionₗ(_▫_)(inv) → ComplementFunctionᵣ(_▫_)(inv)
    ComplementFunctionᵣ.proof (r absorbₗ) {x} =
      x ▫ inv(x)           🝖-[ {!!} ]
      inv(inv(x)) ▫ inv(x) 🝖-[ {!!} ]
      ab                   🝖-end
  -}

  cancellationₗ-by-group : let _ = op , assoc , select-invₗ(idₗ)(identₗ)(invₗ)(inverₗ) in Cancellationₗ(_▫_)
  Cancellationₗ.proof (cancellationₗ-by-group {id}{inv}) {a}{b}{c} abac =
    b                🝖-[ symmetry(_≡_) (identityₗ(_▫_)(id)) ]
    id ▫ b           🝖-[ congruence₂ₗ(_▫_)(_) (symmetry(_≡_) (inverseFunctionₗ(_▫_)(inv))) ]
    (inv(a) ▫ a) ▫ b 🝖-[ associativity(_▫_) ]
    inv(a) ▫ (a ▫ b) 🝖-[ congruence₂ᵣ(_▫_)(_) abac ]
    inv(a) ▫ (a ▫ c) 🝖-[ symmetry(_≡_) (associativity(_▫_)) ]
    (inv(a) ▫ a) ▫ c 🝖-[ congruence₂ₗ(_▫_)(_) (inverseFunctionₗ(_▫_)(inv)) ]
    id ▫ c           🝖-[ identityₗ(_▫_)(id) ]
    c                🝖-end

  cancellationᵣ-by-group : let _ = op , assoc , select-invᵣ(idᵣ)(identᵣ)(invᵣ)(inverᵣ) in Cancellationᵣ(_▫_)
  Cancellationᵣ.proof (cancellationᵣ-by-group {id}{inv}) {c}{a}{b} acbc =
    a                🝖-[ symmetry(_≡_) (identityᵣ(_▫_)(id)) ]
    a ▫ id           🝖-[ congruence₂ᵣ(_▫_)(_) (symmetry(_≡_) (inverseFunctionᵣ(_▫_)(inv))) ]
    a ▫ (c ▫ inv(c)) 🝖-[ symmetry(_≡_) (associativity(_▫_)) ]
    (a ▫ c) ▫ inv(c) 🝖-[ congruence₂ₗ(_▫_)(_) acbc ]
    (b ▫ c) ▫ inv(c) 🝖-[ associativity(_▫_) ]
    b ▫ (c ▫ inv(c)) 🝖-[ congruence₂ᵣ(_▫_)(_) (inverseFunctionᵣ(_▫_)(inv)) ]
    b ▫ id           🝖-[ identityᵣ(_▫_)(id) ]
    b                🝖-end

  inverse-distribution : let _ = op , assoc , select-inv(id)(ident)(inv)(inver) in ∀{x y} → (inv(x ▫ y) ≡ inv(y) ▫ inv(x))
  inverse-distribution {id}{inv} {x}{y} =
    (cancellationᵣ(_▫_) ⦃ cancellationᵣ-by-group ⦄
      ((
        inv(x ▫ y) ▫ (x ▫ y)         🝖-[ inverseFunction-left(_▫_)(inv) ]
        id                           🝖-[ symmetry(_≡_) (inverseFunction-left(_▫_)(inv)) ]
        inv(y) ▫ y                   🝖-[ symmetry(_≡_) (squeezed-inverse (inverseFunction-left(_▫_)(inv))) ]
        (inv(y) ▫ (inv(x) ▫ x)) ▫ y  🝖-[ congruence₂ₗ(_▫_)(_) (symmetry(_≡_) (associativity(_▫_))) ]
        ((inv(y) ▫ inv(x)) ▫ x) ▫ y  🝖-[ associativity(_▫_) ]
        (inv(y) ▫ inv(x)) ▫ (x ▫ y)  🝖-end
      ) :of: (inv(x ▫ y) ▫ (x ▫ y) ≡ (inv(y) ▫ inv(x)) ▫ (x ▫ y)))
    ) :of: (inv(x ▫ y) ≡ inv(y) ▫ inv(x))

  inverse-preserving : let _ = op , assoc , comm , select-inv(id)(ident)(inv)(inver) in Preserving₂(inv)(_▫_)(_▫_)
  Preserving.proof (inverse-preserving {id}{inv}) {x}{y} = inverse-distribution {id}{inv} {x}{y} 🝖 commutativity(_▫_)

  inverse-distribute-to-inverse : let _ = op , assoc , select-inv(id)(ident)(inv)(inver) in ∀{x y} → inv(inv x ▫ inv y) ≡ y ▫ x
  inverse-distribute-to-inverse {id}{inv} {x}{y} =
    inv(inv x ▫ inv y)      🝖-[ inverse-distribution ]
    inv(inv y) ▫ inv(inv x) 🝖-[ congruence₂ᵣ(_▫_)(_) (double-inverse ⦃ cancᵣ = cancellationᵣ-by-group ⦄) ]
    inv(inv y) ▫ x          🝖-[ congruence₂ₗ(_▫_)(_) (double-inverse ⦃ cancᵣ = cancellationᵣ-by-group ⦄) ]
    y ▫ x                   🝖-end

  inverse-preserving-to-inverse : let _ = op , assoc , comm , select-inv(id)(ident)(inv)(inver) in ∀{x y} → inv(inv x ▫ inv y) ≡ x ▫ y
  inverse-preserving-to-inverse {id}{inv} {x}{y} = inverse-distribute-to-inverse {id}{inv} {x}{y} 🝖 commutativity(_▫_)

  unique-inverseₗ-by-id : let _ = op , assoc , select-id(id)(ident) , select-invₗ(id)(Identity.left ident)(inv)(inverₗ) in ∀{x x⁻¹} → (x⁻¹ ▫ x ≡ id) → (x⁻¹ ≡ inv(x))
  unique-inverseₗ-by-id {id = id} {inv = inv} {x}{x⁻¹} inver-elem =
    x⁻¹                          🝖-[ identityᵣ(_▫_)(id) ]-sym
    x⁻¹ ▫ id                     🝖-[ congruence₂ᵣ(_▫_)(_) (inverseFunctionₗ(_▫_)(inv)) ]-sym
    x⁻¹ ▫ (inv(inv(x)) ▫ inv(x)) 🝖-[ associativity(_▫_) ]-sym
    (x⁻¹ ▫ inv(inv(x))) ▫ inv(x) 🝖-[ congruence₂ₗ(_▫_)(_) (congruence₂ᵣ(_▫_)(_) (double-inverseₗ-by-id)) ]
    (x⁻¹ ▫ x) ▫ inv(x)           🝖-[ congruence₂ₗ(_▫_)(_) inver-elem ]
    id ▫ inv(x)                  🝖-[ identityₗ(_▫_)(id) ]
    inv(x)                       🝖-end

  unique-inverseᵣ-by-id : let _ = op , assoc , select-id(id)(ident) , select-invᵣ(id)(Identity.right ident)(inv)(inverᵣ) in ∀{x x⁻¹} → (x ▫ x⁻¹ ≡ id) → (x⁻¹ ≡ inv(x))
  unique-inverseᵣ-by-id {id = id} {inv = inv} {x}{x⁻¹} inver-elem =
    x⁻¹                          🝖-[ identityₗ(_▫_)(id) ]-sym
    id ▫ x⁻¹                     🝖-[ congruence₂ₗ(_▫_)(_) (inverseFunctionᵣ(_▫_)(inv)) ]-sym
    (inv(x) ▫ inv(inv(x))) ▫ x⁻¹ 🝖-[ associativity(_▫_) ]
    inv(x) ▫ (inv(inv(x)) ▫ x⁻¹) 🝖-[ congruence₂ᵣ(_▫_)(_) (congruence₂ₗ(_▫_)(_) double-inverseᵣ-by-id) ]
    inv(x) ▫ (x ▫ x⁻¹)           🝖-[ congruence₂ᵣ(_▫_)(_) inver-elem ]
    inv(x) ▫ id                  🝖-[ identityᵣ(_▫_)(id) ]
    inv(x)                       🝖-end

  unique-inverseFunctionₗ-by-id : let _ = op , assoc , select-id(id)(ident) in Unique(InverseFunctionₗ(_▫_))
  unique-inverseFunctionₗ-by-id {id = id} {x = inv₁} {inv₂} inverse₁ inverse₂ = intro \{x} → unique-inverseₗ-by-id ⦃ inverₗ = inverse₂ ⦄ (inverseFunctionₗ(_▫_)(inv₁) ⦃ inverse₁ ⦄)

  unique-inverseFunctionᵣ-by-id : let _ = op , assoc , select-id(id)(ident) in Unique(InverseFunctionᵣ(_▫_))
  unique-inverseFunctionᵣ-by-id {id = id} {x = inv₁} {inv₂} inverse₁ inverse₂ = intro \{x} → unique-inverseᵣ-by-id ⦃ inverᵣ = inverse₂ ⦄ (inverseFunctionᵣ(_▫_)(inv₁) ⦃ inverse₁ ⦄)

  unique-inverses : let _ = op , assoc , select-id(id)(ident) in ⦃ _ : InverseFunctionₗ(_▫_)(invₗ) ⦄ → ⦃ _ : InverseFunctionᵣ(_▫_)(invᵣ) ⦄ → (invₗ ≡ invᵣ)
  unique-inverses {id} {invₗ} {invᵣ} = intro \{x} →
    (
      invₗ(x)                 🝖-[ symmetry(_≡_) (identityᵣ(_▫_)(id)) ]
      invₗ(x) ▫ id            🝖-[ congruence₂ᵣ(_▫_)(_) (symmetry(_≡_) (inverseFunctionᵣ(_▫_)(invᵣ))) ]
      invₗ(x) ▫ (x ▫ invᵣ(x)) 🝖-[ symmetry(_≡_) (associativity(_▫_)) ]
      (invₗ(x) ▫ x) ▫ invᵣ(x) 🝖-[ congruence₂ₗ(_▫_)(_) (inverseFunctionₗ(_▫_)(invₗ)) ]
      id ▫ invᵣ(x)            🝖-[ identityₗ(_▫_)(id) ]
      invᵣ(x)                 🝖-end
    )

  absorber-equivalence-by-commutativity : let _ = comm in Absorberₗ(_▫_)(ab) ↔ Absorberᵣ(_▫_)(ab)
  absorber-equivalence-by-commutativity {ab} = [↔]-intro l r where
    r : Absorberₗ(_▫_)(ab) → Absorberᵣ(_▫_)(ab)
    Absorberᵣ.proof (r absoₗ) {x} =
      x ▫ ab 🝖-[ commutativity(_▫_) ]
      ab ▫ x 🝖-[ absorberₗ(_▫_)(ab) ⦃ absoₗ ⦄ ]
      ab     🝖-end

    l : Absorberₗ(_▫_)(ab) ← Absorberᵣ(_▫_)(ab)
    Absorberₗ.proof (l absoᵣ) {x} =
      ab ▫ x 🝖-[ commutativity(_▫_) ]
      x ▫ ab 🝖-[ absorberᵣ(_▫_)(ab) ⦃ absoᵣ ⦄ ]
      ab     🝖-end

  inverse-propertyₗ-by-groupₗ : let _ = op , assoc , select-invₗ(id)(identₗ)(inv)(inverₗ) in InversePropertyₗ(_▫_)(inv)
  InverseOperatorₗ.proof (inverse-propertyₗ-by-groupₗ {id = id}{inv = inv}) {x} {y} =
    inv(x) ▫ (x ▫ y) 🝖-[ associativity(_▫_) ]-sym
    (inv(x) ▫ x) ▫ y 🝖-[ congruence₂ₗ(_▫_)(y) (inverseFunctionₗ(_▫_)(inv)) ]
    id ▫ y           🝖-[ identityₗ(_▫_)(id) ]
    y                🝖-end

  inverse-propertyᵣ-by-groupᵣ : let _ = op , assoc , select-invᵣ(id)(identᵣ)(inv)(inverᵣ) in InversePropertyᵣ(_▫_)(inv)
  InverseOperatorᵣ.proof (inverse-propertyᵣ-by-groupᵣ {id = id}{inv = inv}) {x} {y} =
    (x ▫ y) ▫ inv(y) 🝖-[ associativity(_▫_) ]
    x ▫ (y ▫ inv(y)) 🝖-[ congruence₂ᵣ(_▫_)(x) (inverseFunctionᵣ(_▫_)(inv)) ]
    x ▫ id           🝖-[ identityᵣ(_▫_)(id) ]
    x                🝖-end

  standard-inverse-operatorₗ-by-involuting-inverse-propₗ : let _ = op , select-invol(inv)(invol) , select-invPropₗ(inv)(inverPropₗ) in InverseOperatorₗ(x ↦ y ↦ inv(x) ▫ y)(_▫_)
  InverseOperatorₗ.proof (standard-inverse-operatorₗ-by-involuting-inverse-propₗ {inv = inv}) {x} {y} =
    x ▫ (inv x ▫ y)            🝖-[ congruence₂ₗ(_▫_)((inv x ▫ y)) (involution(inv)) ]-sym
    inv(inv(x)) ▫ (inv x ▫ y)  🝖-[ inversePropₗ(_▫_)(inv) ]
    y                          🝖-end

  standard-inverse-inverse-operatorₗ-by-inverse-propₗ : let _ = select-invPropₗ(inv)(inverPropₗ) in InverseOperatorₗ(_▫_)(x ↦ y ↦ inv(x) ▫ y)
  InverseOperatorₗ.proof (standard-inverse-inverse-operatorₗ-by-inverse-propₗ {inv = inv}) {x} {y} = inversePropₗ(_▫_)(inv)

  standard-inverse-operatorᵣ-by-involuting-inverse-propᵣ : let _ = op , select-invol(inv)(invol) , select-invPropᵣ(inv)(inverPropᵣ) in InverseOperatorᵣ(x ↦ y ↦ x ▫ inv(y))(_▫_)
  InverseOperatorᵣ.proof (standard-inverse-operatorᵣ-by-involuting-inverse-propᵣ {inv = inv}) {x} {y} =
    (x ▫ inv y) ▫ y           🝖-[ congruence₂ᵣ(_▫_)((x ▫ inv y)) (involution(inv)) ]-sym
    (x ▫ inv y) ▫ inv(inv(y)) 🝖-[ inversePropᵣ(_▫_)(inv) ]
    x                         🝖-end

  standard-inverse-inverse-operatorᵣ-by-inverse-propᵣ : let _ = select-invPropᵣ(inv)(inverPropᵣ) in InverseOperatorᵣ(_▫_)(x ↦ y ↦ x ▫ inv(y))
  InverseOperatorᵣ.proof (standard-inverse-inverse-operatorᵣ-by-inverse-propᵣ {inv = inv}) {x} {y} = inversePropᵣ(_▫_)(inv)

  inverseᵣ-by-assoc-inv-propᵣ : let _ = op , assoc , select-idₗ(id)(identₗ) , select-invPropᵣ(inv)(inverPropᵣ) in InverseFunctionᵣ(_▫_) ⦃ [∃]-intro(id) ⦃ identᵣ ⦄ ⦄ (inv)
  InverseFunctionᵣ.proof (inverseᵣ-by-assoc-inv-propᵣ {id = id} {inv = inv}) {x} =
    x ▫ inv x        🝖-[ identityₗ(_▫_)(id) ]-sym
    id ▫ (x ▫ inv x) 🝖-[ associativity(_▫_) ]-sym
    (id ▫ x) ▫ inv x 🝖-[ inversePropᵣ(_▫_)(inv) ]
    id               🝖-end

  zero-when-redundant-addition : let _ = select-idₗ(id)(identₗ) , cancᵣ in ∀{x} → (x ≡ x ▫ x) → (x ≡ id)
  zero-when-redundant-addition {id = id} {x} p = cancellationᵣ(_▫_) $ symmetry(_≡_) $
    id ▫ x 🝖-[ identityₗ(_▫_)(id) ]
    x      🝖-[ p ]
    x ▫ x  🝖-end

module OneTypeTwoOp {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_▫₁_ _▫₂_ : T → T → T} where
  open Lang.Vars.Structure.Operator.OneTypeTwoOp ⦃ equiv = equiv ⦄ {_▫₁_ = _▫₁_} {_▫₂_ = _▫₂_}

  absorptionₗ-by-abs-com-dist-id : let _ = op₁ , op₂ , distriₗ , select-absₗ(id)(absorbₗ₂) , select-idᵣ(id)(identᵣ₁) in Absorptionₗ(_▫₂_)(_▫₁_)
  Absorptionₗ.proof (absorptionₗ-by-abs-com-dist-id {id = id}) {x}{y} =
    x ▫₂ (x ▫₁ y)         🝖-[ congruence₂ₗ(_▫₂_)(_) (identityᵣ(_▫₁_)(id)) ]-sym
    (x ▫₁ id) ▫₂ (x ▫₁ y) 🝖-[ distributivityₗ(_▫₁_)(_▫₂_) ]-sym
    x ▫₁ (id ▫₂ y)        🝖-[ congruence₂ᵣ(_▫₁_)(_) (absorberₗ(_▫₂_)(id)) ]
    x ▫₁ id               🝖-[ identityᵣ(_▫₁_)(id) ]
    x                     🝖-end

  absorptionᵣ-by-abs-com-dist-id : let _ = op₁ , op₂ , distriᵣ , select-absᵣ(id)(absorbᵣ₂) , select-idₗ(id)(identₗ₁) in Absorptionᵣ(_▫₂_)(_▫₁_)
  Absorptionᵣ.proof (absorptionᵣ-by-abs-com-dist-id {id = id}) {x}{y} =
    (x ▫₁ y) ▫₂ y         🝖-[ congruence₂ᵣ(_▫₂_)(_) (identityₗ(_▫₁_)(id)) ]-sym
    (x ▫₁ y) ▫₂ (id ▫₁ y) 🝖-[ distributivityᵣ(_▫₁_)(_▫₂_) ]-sym
    (x ▫₂ id) ▫₁ y        🝖-[ congruence₂ₗ(_▫₁_)(_) (absorberᵣ(_▫₂_)(id)) ]
    id ▫₁ y               🝖-[ identityₗ(_▫₁_)(id) ]
    y                     🝖-end

  distributivity-equivalence-by-commutativity : let _ = op₂ , comm₁ in Distributivityₗ(_▫₁_)(_▫₂_) ↔ Distributivityᵣ(_▫₁_)(_▫₂_)
  distributivity-equivalence-by-commutativity = [↔]-intro l r where
    l : Distributivityₗ(_▫₁_)(_▫₂_) ← Distributivityᵣ(_▫₁_)(_▫₂_)
    Distributivityₗ.proof (l distriᵣ) {x}{y}{z} =
      x ▫₁ (y ▫₂ z)        🝖-[ commutativity(_▫₁_) ]
      (y ▫₂ z) ▫₁ x        🝖-[ distributivityᵣ(_▫₁_)(_▫₂_) ⦃ distriᵣ ⦄ ]
      (y ▫₁ x) ▫₂ (z ▫₁ x) 🝖-[ congruence₂ₗ(_▫₂_)(_) (commutativity(_▫₁_)) ]
      (x ▫₁ y) ▫₂ (z ▫₁ x) 🝖-[ congruence₂ᵣ(_▫₂_)(_) (commutativity(_▫₁_)) ]
      (x ▫₁ y) ▫₂ (x ▫₁ z) 🝖-end

    r : Distributivityₗ(_▫₁_)(_▫₂_) → Distributivityᵣ(_▫₁_)(_▫₂_)
    Distributivityᵣ.proof (r distriₗ) {x}{y}{z} =
      (x ▫₂ y) ▫₁ z        🝖-[ commutativity(_▫₁_) ]
      z ▫₁ (x ▫₂ y)        🝖-[ distributivityₗ(_▫₁_)(_▫₂_) ⦃ distriₗ ⦄ ]
      (z ▫₁ x) ▫₂ (z ▫₁ y) 🝖-[ congruence₂ₗ(_▫₂_)(_) (commutativity(_▫₁_)) ]
      (x ▫₁ z) ▫₂ (z ▫₁ y) 🝖-[ congruence₂ᵣ(_▫₂_)(_) (commutativity(_▫₁_)) ]
      (x ▫₁ z) ▫₂ (y ▫₁ z) 🝖-end

  absorption-equivalence-by-commutativity : let _ = op₁ , comm₁ , comm₂ in Absorptionₗ(_▫₁_)(_▫₂_) ↔ Absorptionᵣ(_▫₁_)(_▫₂_)
  absorption-equivalence-by-commutativity = [↔]-intro l r where
    r : Absorptionₗ(_▫₁_)(_▫₂_) → Absorptionᵣ(_▫₁_)(_▫₂_)
    Absorptionᵣ.proof (r absorpₗ) {x}{y} =
      (x ▫₂ y) ▫₁ y 🝖-[ commutativity(_▫₁_) ]
      y ▫₁ (x ▫₂ y) 🝖-[ congruence₂ᵣ(_▫₁_)(_) (commutativity(_▫₂_)) ]
      y ▫₁ (y ▫₂ x) 🝖-[ absorptionₗ(_▫₁_)(_▫₂_) ⦃ absorpₗ ⦄ {y}{x} ]
      y             🝖-end

    l : Absorptionₗ(_▫₁_)(_▫₂_) ← Absorptionᵣ(_▫₁_)(_▫₂_)
    Absorptionₗ.proof (l absorpᵣ) {x}{y} =
      x ▫₁ (x ▫₂ y) 🝖-[ commutativity(_▫₁_) ]
      (x ▫₂ y) ▫₁ x 🝖-[ congruence₂ₗ(_▫₁_)(_) (commutativity(_▫₂_)) ]
      (y ▫₂ x) ▫₁ x 🝖-[ absorptionᵣ(_▫₁_)(_▫₂_) ⦃ absorpᵣ ⦄ {y}{x} ]
      x             🝖-end

  absorberₗ-by-absorptionₗ-identityₗ : let _ = absorpₗ , select-idₗ(id)(identₗ₁) in Absorberₗ(_▫₂_)(id)
  Absorberₗ.proof (absorberₗ-by-absorptionₗ-identityₗ {id}) {x} =
    id ▫₂ x         🝖-[ identityₗ(_▫₁_)(id) ]-sym
    id ▫₁ (id ▫₂ x) 🝖-[ absorptionₗ(_▫₁_)(_▫₂_) ]
    id              🝖-end

  absorberᵣ-by-absorptionᵣ-identityᵣ : let _ = absorpᵣ , select-idᵣ(id)(identᵣ₁) in Absorberᵣ(_▫₂_)(id)
  Absorberᵣ.proof (absorberᵣ-by-absorptionᵣ-identityᵣ {id}) {x} =
    x ▫₂ id         🝖-[ identityᵣ(_▫₁_)(id) ]-sym
    (x ▫₂ id) ▫₁ id 🝖-[ absorptionᵣ(_▫₁_)(_▫₂_) ]
    id              🝖-end

module Two {ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂} {A : Type{ℓ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ {_▫₁_ : A → A → A} {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ {_▫₂_ : B → B → B} where
  open Lang.Vars.Structure.Operator.Two ⦃ equiv-A = equiv-A ⦄ {_▫₁_ = _▫₁_} ⦃ equiv-B = equiv-B ⦄ {_▫₂_ = _▫₂_}

  module _ {θ : A → B} ⦃ func : Function ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (θ) ⦄ ⦃ preserv : Preserving₂ ⦃ equiv-B ⦄ (θ)(_▫₁_)(_▫₂_) ⦄ where
    preserving-identityₗ : let _ = cancᵣ₂ , select-idₗ(id₁)(identₗ₁) , select-idₗ(id₂)(identₗ₂) in (θ(id₁) ≡ id₂)
    preserving-identityₗ {id₁}{id₂} = cancellationᵣ(_▫₂_) $
      θ(id₁) ▫₂ θ(id₁) 🝖-[ preserving₂(θ)(_▫₁_)(_▫₂_) ]-sym
      θ(id₁ ▫₁ id₁)    🝖-[ congruence₁(θ) (identityₗ(_▫₁_)(id₁)) ]
      θ(id₁)           🝖-[ identityₗ(_▫₂_)(id₂) ]-sym
      id₂ ▫₂ θ(id₁)    🝖-end

    preserving-inverseₗ : let _ = cancᵣ₂ , select-invₗ(id₁)(identₗ₁)(inv₁)(inverₗ₁) , select-invₗ(id₂)(identₗ₂)(inv₂)(inverₗ₂) in ∀{x} → (θ(inv₁(x)) ≡ inv₂(θ(x)))
    preserving-inverseₗ {id₁}{inv₁}{id₂}{inv₂} {x} = cancellationᵣ(_▫₂_) $
      θ(inv₁ x) ▫₂ θ(x)  🝖-[ preserving₂(θ)(_▫₁_)(_▫₂_) ]-sym
      θ(inv₁ x ▫₁ x)     🝖-[ congruence₁(θ) (inverseFunctionₗ(_▫₁_)(inv₁)) ]
      θ(id₁)             🝖-[ preserving-identityₗ ]
      id₂                🝖-[ inverseFunctionₗ(_▫₂_)(inv₂) ]-sym
      inv₂(θ(x)) ▫₂ θ(x) 🝖-end

    preserving-identityᵣ : let _ = cancₗ₂ , select-idᵣ(id₁)(identᵣ₁) , select-idᵣ(id₂)(identᵣ₂) in (θ(id₁) ≡ id₂)
    preserving-identityᵣ {id₁}{id₂} = cancellationₗ(_▫₂_) $
      θ(id₁) ▫₂ θ(id₁) 🝖-[ preserving₂(θ)(_▫₁_)(_▫₂_) ]-sym
      θ(id₁ ▫₁ id₁)    🝖-[ congruence₁(θ) (identityᵣ(_▫₁_)(id₁)) ]
      θ(id₁)           🝖-[ identityᵣ(_▫₂_)(id₂) ]-sym
      θ(id₁) ▫₂ id₂    🝖-end

    preserving-inverseᵣ : let _ = cancₗ₂ , select-invᵣ(id₁)(identᵣ₁)(inv₁)(inverᵣ₁) , select-invᵣ(id₂)(identᵣ₂)(inv₂)(inverᵣ₂) in ∀{x} → (θ(inv₁(x)) ≡ inv₂(θ(x)))
    preserving-inverseᵣ {id₁}{inv₁}{id₂}{inv₂} {x} = cancellationₗ(_▫₂_) $
      θ(x) ▫₂ θ(inv₁(x)) 🝖-[ preserving₂(θ)(_▫₁_)(_▫₂_) ]-sym
      θ(x ▫₁ inv₁(x))    🝖-[ congruence₁(θ) (inverseFunctionᵣ(_▫₁_)(inv₁)) ]
      θ(id₁)             🝖-[ preserving-identityᵣ ]
      id₂                🝖-[ inverseFunctionᵣ(_▫₂_)(inv₂) ]-sym
      θ(x) ▫₂ inv₂(θ(x)) 🝖-end

    injective-kernel : let _ = op₁ , op₂ , assoc₁ , assoc₂ , cancₗ₂ , select-inv(id₁)(ident₁)(inv₁)(inver₁) , select-inv(id₂)(ident₂)(inv₂)(inver₂) in Injective(θ) ↔ (∀{a} → (θ(a) ≡ id₂) → (a ≡ id₁))
    injective-kernel {id₁}{inv₁}{id₂}{inv₂} = [↔]-intro l (\inj → r ⦃ inj ⦄) where
      l : Injective(θ) ← (∀{a} → (θ(a) ≡ id₂) → (a ≡ id₁))
      Injective.proof(l(proof)) {a}{b} (θa≡θb) =
        One.equality-zeroₗ(
          proof(
            θ (a ▫₁ inv₁(b))   🝖-[ preserving₂(θ)(_▫₁_)(_▫₂_) ]
            θ(a) ▫₂ θ(inv₁(b)) 🝖-[ congruence₂ᵣ(_▫₂_)(θ(a)) preserving-inverseᵣ ]
            θ(a) ▫₂ inv₂(θ(b)) 🝖-[ One.equality-zeroᵣ(θa≡θb) ]
            id₂                🝖-end
          ) :of: (a ▫₁ inv₁(b) ≡ id₁)
        ) :of: (a ≡ b)

      r : ⦃ _ : Injective(θ) ⦄ → (∀{a} → (θ(a) ≡ id₂) → (a ≡ id₁))
      r {a} (θa≡id) = injective(θ) $
        θ(a)   🝖-[ θa≡id ]
        id₂    🝖-[ preserving-identityᵣ ]-sym
        θ(id₁) 🝖-end


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Unit.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat
open import Cubical.Data.Unit.Base
open import Cubical.Data.Prod.Base

open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

isContr⊤ : isContr ⊤
isContr⊤ = tt , λ {tt → refl}

isProp⊤ : isProp ⊤
isProp⊤ _ _ i = tt -- definitionally equal to: isContr→isProp isContrUnit

isSet⊤ : isSet ⊤
isSet⊤ = isProp→isSet isProp⊤

isOfHLevel⊤ : (n : HLevel) → isOfHLevel n ⊤
isOfHLevel⊤ n = isContr→isOfHLevel n isContr⊤

diagonal-unit : ⊤ ≡ ⊤ × ⊤
diagonal-unit = isoToPath (iso (λ x → tt , tt) (λ x → tt) (λ {(tt , tt) i → tt , tt}) λ {tt i → tt})

fibId : ∀ {ℓ} (A : Type ℓ) → (fiber (λ (x : A) → tt) tt) ≡ A
fibId A = isoToPath
            (iso fst
                 (λ a → a , refl)
                 (λ _ → refl)
                 (λ a i → fst a
                         , isOfHLevelSuc 1 isProp⊤ _ _ (snd a) refl i))


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

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

variable
  a p         : Level
  A           : Set a
  P           : A → Set p
  x y : A

refl : x ≡ x
refl {x = x} = λ _ → x

data 𝕊¹ : Set where
  base : 𝕊¹
  loop : base ≡ base

g : Bool → I → 𝕊¹
g true i = base
g false i = loop i

_ : g false i0 ≡ base
_ = refl

_ : g true i0 ≡ base
_ = refl

-- non-unique solutions, should not solve either of the metas.
_ : g _ _ ≡ base
_ = refl

h : Bool → base ≡ base
h true = \ _ → base
h false = loop

_ : h false i0 ≡ base
_ = refl

_ : h true i0 ≡ base
_ = refl

-- non-unique solutions, should not solve either of the metas.
_ : h _ _ ≡ base
_ = refl

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --cubical --safe #-}
open import Agda.Builtin.Cubical.Path

data Circle1 : Set where
  base1 : Circle1
  loop : base1 ≡ base1

data Circle2 : Set where
  base2 : Circle2
  loop : base2 ≡ base2

test : base2 ≡ base2
test = loop


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

{-
  This file lists some basic facts about equivalences
  that have to be put in a separate file due to dependency.
-}

open import Types
open import Functions
open import Paths
open import HLevel
open import Equivalences
open import Univalence
open import HLevelBis

module EquivalenceLemmas where

  equiv-eq : ∀ {i} {A B : Set i} {f g : A ≃ B} → π₁ f ≡ π₁ g → f ≡ g
  equiv-eq p = Σ-eq p $ prop-has-all-paths (is-equiv-is-prop _) _ _


text:
{-# OPTIONS --copatterns --allow-unsolved-metas #-}

module Issue942  where

record Sigma (A : Set)(P : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : P fst
open Sigma

postulate
  A : Set
  x : A
  P Q : A → Set
  Px : P x
  f  : ∀ {x} → P x → Q x

ex : Sigma A Q
ex = record
       { fst = x
       ; snd = f {!!} -- goal: P x
       }

ex' : Sigma A Q
ex' = x , f {!!} -- goal: P x

ex'' : Sigma A Q
fst ex'' = x
snd ex'' = f {!!} -- goal: P (fst ex'')

-- should termination check


text:
open import Relation.Binary.Core

module InsertSort.Impl2 {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Data.Sum
open import OList _≤_

insert : {b : Bound}{x : A} → LeB b (val x) → OList b → OList b
insert {b} {x} b≤x onil = :< b≤x onil
insert {b} {x} b≤x (:< {x = y} b≤y ys)
  with tot≤ x y
... | inj₁ x≤y = :< b≤x (:< (lexy x≤y) ys)
... | inj₂ y≤x = :< b≤y (insert (lexy y≤x) ys)

insertSort : List A → OList bot
insertSort [] = onil
insertSort (x ∷ xs) = insert {bot} {x} lebx (insertSort xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting